============================== Prover9 =============================== Prover9 (64) version 2009-02A, February 2009. Process 1150 was started by veroff on proof, Sat May 7 08:59:26 2011 The command was "prover9 -f IL.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file IL.in clear(auto_inference). set(hyper_resolution). % set(hyper_resolution) -> set(pos_hyper_resolution). formulas(sos). -P(x) | -P(i(x,y)) | P(y). P(i(x,i(y,x))) # label("A1"). P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) # label("A2"). P(i(k(x,y),x)) # label("A3"). P(i(k(x,y),y)) # label("A4"). P(i(i(x,y),i(i(x,z),i(x,k(y,z))))) # label("A5"). P(i(x,a(x,y))) # label("A6"). P(i(x,a(y,x))) # label("A7"). P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) # label("A8"). P(i(i(x,n(y)),i(y,n(x)))) # label("A9"). P(i(n(x),i(x,y))) # label("A10"). end_of_list. formulas(goals). P(i(i(x,y),i(a(x,z),a(y,z)))) # label("H334"). P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(x,z),a(y,z)),a(k(x,y),z)))) # label("HIF4"). P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(x),n(y)),n(a(x,y))))) # label("HIF5"). end_of_list. formulas(hints). P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(x),n(y)),n(a(x,y))))). P(i(x,i(y,x))). P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). P(i(k(x,y),x)). P(i(k(x,y),y)). P(i(i(x,y),i(i(x,z),i(x,k(y,z))))). P(i(x,a(x,y))). P(i(x,a(y,x))). P(i(i(x,y),i(i(z,y),i(a(x,z),y)))). P(i(i(x,n(y)),i(y,n(x)))). P(i(n(x),i(x,y))). P(i(x,i(y,i(z,y)))). P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))). P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))). P(i(x,i(k(y,z),y))). P(i(i(k(x,i(y,z)),y),i(k(x,i(y,z)),z))). P(i(x,i(k(y,z),z))). P(i(i(x,y),i(x,k(i(z,x),y)))). P(i(x,i(y,a(y,z)))). P(i(x,i(y,a(z,y)))). P(i(x,i(i(y,n(z)),i(z,n(y))))). P(i(x,i(n(y),i(y,z)))). P(i(i(x,y),i(x,i(z,y)))). P(i(i(x,y),i(x,a(y,z)))). P(i(i(x,y),i(x,a(z,y)))). P(i(i(x,n(y)),i(x,i(y,z)))). P(i(x,a(a(y,x),z))). P(i(x,a(a(x,y),z))). P(i(x,a(y,i(z,x)))). P(i(i(x,i(y,i(z,u))),i(a(i(y,n(z)),x),i(y,i(z,u))))). P(i(x,k(i(y,x),i(z,x)))). P(i(i(x,i(y,n(z))),i(x,i(z,n(y))))). P(i(i(x,i(y,i(z,u))),i(x,i(i(y,z),i(y,u))))). P(i(k(x,i(x,y)),y)). P(i(x,i(k(y,i(y,z)),z))). P(i(i(x,k(y,i(y,z))),i(x,z))). P(i(x,x)). P(i(x,n(n(x)))). P(i(i(x,y),i(x,k(x,y)))). P(i(x,i(n(x),y))). P(i(i(x,i(n(y),z)),i(a(y,x),i(n(y),z)))). P(i(a(x,y),i(n(x),y))). P(i(x,i(a(y,z),i(n(y),z)))). P(i(i(x,a(y,z)),i(x,i(n(y),z)))). P(i(x,i(n(a(x,y)),z))). P(i(x,i(n(a(y,x)),z))). P(i(x,i(y,n(n(a(x,z)))))). P(i(x,i(y,i(n(a(z,x)),u)))). P(i(i(x,y),i(x,n(n(a(x,z)))))). P(i(i(x,y),i(n(a(x,z)),n(x)))). P(i(n(a(x,y)),n(x))). P(i(i(n(a(x,y)),z),i(n(a(x,y)),k(n(x),z)))). P(i(i(x,y),i(i(z,x),i(z,y)))). P(i(i(x,y),i(x,n(n(y))))). P(i(x,n(n(a(y,x))))). P(i(i(x,y),i(n(y),n(x)))). P(i(n(a(x,y)),n(y))). P(i(n(a(x,y)),k(n(x),n(y)))). P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))). P(i(i(k(x,y),i(y,z)),i(k(x,y),z))). P(i(i(k(x,y),i(x,z)),i(k(x,y),z))). P(i(i(x,i(i(y,x),z)),i(x,z))). P(a(x,i(y,i(i(z,i(i(u,z),w)),i(z,w))))). P(i(x,i(i(k(y,z),i(y,u)),i(k(y,z),u)))). P(i(i(x,y),i(k(x,z),y))). P(i(a(i(x,n(y)),i(x,i(i(z,x),i(y,u)))),i(x,i(y,u)))). P(i(i(i(x,y),z),i(y,z))). P(i(x,i(y,k(y,x)))). P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))). P(i(i(x,i(y,z)),i(y,i(x,z)))). P(i(i(x,y),i(i(y,z),i(x,z)))). P(i(n(x),i(a(x,y),y))). P(i(n(x),i(n(y),n(a(x,y))))). P(i(i(i(k(x,y),z),u),i(i(x,z),u))). P(i(i(x,i(y,z)),i(k(x,y),z))). P(i(k(n(x),n(y)),n(a(x,y)))). P(i(x,k(x,i(k(n(y),n(z)),n(a(y,z)))))). P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(z),n(u)),n(a(z,u))))). P(i(i(x,y),i(a(x,z),a(y,z)))). P(i(i(x,a(y,z)),i(a(z,x),a(y,z)))). P(i(a(x,y),a(y,x))). P(i(i(a(x,y),z),i(a(y,x),z))). P(i(i(i(x,a(y,z)),u),i(i(x,y),u))). P(i(i(x,i(a(y,z),u)),i(x,i(a(z,y),u)))). P(i(i(x,y),i(a(z,x),a(y,z)))). P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(x,z),a(y,z)),a(k(x,y),z)))). P(i(i(k(x,y),z),i(k(x,y),k(y,z)))). P(i(i(k(x,y),z),i(k(x,y),k(x,z)))). P(i(i(i(x,y),i(x,z)),i(i(x,y),i(x,k(y,z))))). P(i(i(x,k(y,z)),i(x,y))). P(i(i(x,k(y,z)),i(x,z))). P(i(x,i(y,i(z,x)))). P(i(k(x,k(y,z)),y)). P(i(i(k(x,k(y,z)),u),i(k(x,k(y,z)),k(y,u)))). P(i(k(x,k(y,z)),z)). P(i(k(x,y),a(x,z))). P(i(k(x,y),k(y,x))). P(i(k(x,k(y,z)),k(x,z))). P(i(a(x,k(y,z)),a(y,x))). P(i(x,i(a(y,z),a(z,y)))). P(i(i(x,a(y,z)),i(x,a(z,y)))). P(i(k(x,k(y,i(x,z))),z)). P(i(k(i(x,y),x),y)). P(i(x,i(y,i(z,z)))). P(i(x,i(y,y))). P(i(k(i(x,y),x),k(x,y))). P(i(i(x,y),i(x,k(y,x)))). P(i(x,k(i(y,y),x))). P(i(x,i(i(y,z),i(y,k(z,y))))). P(i(i(i(x,x),y),y)). P(i(k(x,k(y,i(x,z))),k(y,z))). P(i(i(x,i(y,z)),i(x,i(i(u,y),i(u,z))))). P(i(i(x,i(i(y,y),z)),i(x,z))). P(i(i(x,k(i(y,z),y)),i(x,k(y,z)))). P(i(i(x,k(y,z)),i(x,k(z,y)))). P(i(i(x,i(x,y)),i(x,y))). P(i(x,i(y,k(x,y)))). P(i(x,i(i(y,z),i(y,k(x,z))))). P(i(i(x,y),i(x,i(z,k(y,z))))). P(i(i(x,y),i(x,k(i(z,i(u,i(w,w))),y)))). P(i(x,i(i(k(y,z),i(z,u)),i(k(y,z),u)))). P(i(a(x,k(y,z)),k(i(u,i(w,i(v5,v5))),a(y,x)))). P(i(i(x,y),i(k(z,x),y))). P(i(a(x,k(y,z)),k(a(y,x),i(u,i(w,w))))). P(i(x,k(x,i(y,n(n(y)))))). P(i(x,i(i(x,y),y))). P(i(i(i(x,a(x,y)),z),z)). P(i(i(x,i(i(y,a(y,z)),u)),i(x,u))). P(i(i(i(x,k(x,y)),z),i(y,z))). P(i(i(i(k(x,y),z),u),i(i(y,z),u))). P(i(x,i(i(k(y,x),z),i(y,z)))). P(i(i(k(x,y),z),i(y,i(x,z)))). P(i(i(k(x,y),z),i(i(y,x),i(y,z)))). P(i(i(x,a(y,z)),i(a(x,y),a(y,z)))). P(i(i(x,i(k(x,y),z)),i(k(x,y),z))). P(i(i(x,i(y,i(z,u))),i(x,i(k(y,z),u)))). P(i(i(x,y),i(k(z,x),k(z,y)))). P(i(k(x,i(y,i(z,u))),k(x,i(k(y,z),u)))). P(i(k(x,i(y,i(i(z,a(z,u)),w))),k(x,i(y,w)))). P(i(k(x,i(y,i(z,u))),k(x,i(z,i(y,u))))). P(i(k(x,i(y,k(z,u))),k(x,i(y,k(u,z))))). P(i(k(x,i(y,a(z,u))),k(x,i(y,a(u,z))))). P(i(k(x,i(y,k(z,u))),k(x,i(y,z)))). P(i(k(x,i(y,a(z,u))),k(x,i(a(u,y),a(z,u))))). P(i(i(k(x,y),z),i(x,i(y,z)))). P(i(x,i(y,a(z,k(x,y))))). P(i(i(k(x,y),z),i(i(x,y),i(x,z)))). P(i(x,k(x,i(y,i(z,a(u,k(y,z))))))). P(i(i(x,i(y,a(z,u))),i(x,i(a(y,z),a(z,u))))). P(i(k(x,i(y,i(k(y,z),u))),k(x,i(k(y,z),u)))). P(i(i(x,k(y,i(x,z))),i(x,k(y,z)))). P(i(i(x,y),i(x,k(y,i(z,i(u,a(w,k(z,u)))))))). P(i(i(x,y),i(k(x,z),k(y,z)))). P(i(k(i(a(x,y),z),u),k(i(a(y,x),z),u))). P(i(i(x,k(y,i(z,i(u,w)))),i(x,k(y,i(k(z,u),w))))). P(i(i(x,k(y,i(z,i(u,w)))),i(x,k(y,i(u,i(z,w)))))). P(i(i(x,k(y,i(z,i(i(u,a(u,w)),v5)))),i(x,k(y,i(z,v5))))). P(i(i(x,k(y,i(z,a(u,w)))),i(x,k(y,i(a(w,z),a(u,w)))))). P(i(k(x,i(y,i(z,a(u,w)))),k(x,i(y,i(a(z,u),a(u,w)))))). P(i(k(x,i(y,z)),k(x,i(y,k(z,i(u,i(w,a(v5,k(u,w))))))))). P(i(k(x,i(y,k(z,i(u,i(w,v5))))),k(x,i(y,k(z,i(k(u,w),v5)))))). P(i(k(x,i(y,k(z,i(u,i(w,v5))))),k(x,i(y,k(z,i(w,i(u,v5))))))). P(i(a(x,k(y,z)),k(a(y,x),i(u,i(w,a(w,v5)))))). P(i(a(x,k(y,z)),k(a(y,x),i(k(u,w),a(w,v5))))). P(i(a(x,k(y,z)),k(a(y,x),i(a(u,k(w,v5)),a(v5,u))))). P(i(a(x,k(y,z)),k(a(y,x),a(z,x)))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,n(n(u))))). P(i(i(x,k(y,i(z,i(u,a(w,v5))))),i(x,k(y,i(z,i(a(u,w),a(w,v5))))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(v5,a(v6,k(w,v5)))))))). P(i(k(x,i(y,k(z,i(u,i(w,a(v5,v6)))))),k(x,i(y,k(z,i(u,i(a(w,v5),a(v5,v6)))))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(v5,a(v6,k(v5,w)))))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(a(v5,v6),a(v6,k(v5,w)))))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(a(w,v5),i(v6,a(v5,k(w,v6)))))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(a(w,v5),i(a(v6,v5),a(v5,k(w,v6)))))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6))))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6))),n(n(u)))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6)))))). P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(k(a(u,w),a(v5,w)),a(w,k(u,v5))))). P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(u,w),a(v5,w)),a(w,k(u,v5))))). P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(u,w),a(v5,w)),a(k(u,v5),w)))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 P(i(i(x,y),i(a(x,z),a(y,z)))) # label("H334") # label(non_clause) # label(goal). [goal]. 2 P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(x,z),a(y,z)),a(k(x,y),z)))) # label("HIF4") # label(non_clause) # label(goal). [goal]. 3 P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(x),n(y)),n(a(x,y))))) # label("HIF5") # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -P(x) | -P(i(x,y)) | P(y). [assumption]. P(i(x,i(y,x))) # label("A1"). [assumption]. P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) # label("A2"). [assumption]. P(i(k(x,y),x)) # label("A3"). [assumption]. P(i(k(x,y),y)) # label("A4"). [assumption]. P(i(i(x,y),i(i(x,z),i(x,k(y,z))))) # label("A5"). [assumption]. P(i(x,a(x,y))) # label("A6"). [assumption]. P(i(x,a(y,x))) # label("A7"). [assumption]. P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) # label("A8"). [assumption]. P(i(i(x,n(y)),i(y,n(x)))) # label("A9"). [assumption]. P(i(n(x),i(x,y))) # label("A10"). [assumption]. -P(i(i(c1,c2),i(a(c1,c3),a(c2,c3)))) # label("H334"). [deny(1)]. -P(k(i(a(k(c4,c5),c6),k(a(c4,c6),a(c5,c6))),i(k(a(c4,c6),a(c5,c6)),a(k(c4,c5),c6)))) # label("HIF4"). [deny(2)]. -P(k(i(n(a(c7,c8)),k(n(c7),n(c8))),i(k(n(c7),n(c8)),n(a(c7,c8))))) # label("HIF5"). [deny(3)]. end_of_list. formulas(demodulators). end_of_list. % 180 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label "H334" to answer in negative clause % copying label "HIF4" to answer in negative clause % copying label "HIF5" to answer in negative clause % assign(max_proofs, 3). % (Horn set with more than one neg. clause) Term ordering decisions: Predicate symbol precedence: predicate_order([ P ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, c8, i, a, k, n ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_process settings: (no changes). kept: 4 -P(x) | -P(i(x,y)) | P(y). [assumption]. kept: 5 P(i(x,i(y,x))) # label("A1"). [assumption]. kept: 6 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) # label("A2"). [assumption]. kept: 7 P(i(k(x,y),x)) # label("A3"). [assumption]. kept: 8 P(i(k(x,y),y)) # label("A4"). [assumption]. kept: 9 P(i(i(x,y),i(i(x,z),i(x,k(y,z))))) # label("A5"). [assumption]. kept: 10 P(i(x,a(x,y))) # label("A6"). [assumption]. kept: 11 P(i(x,a(y,x))) # label("A7"). [assumption]. kept: 12 P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) # label("A8"). [assumption]. kept: 13 P(i(i(x,n(y)),i(y,n(x)))) # label("A9"). [assumption]. kept: 14 P(i(n(x),i(x,y))) # label("A10"). [assumption]. kept: 15 -P(i(i(c1,c2),i(a(c1,c3),a(c2,c3)))) # label("H334") # answer("H334"). [deny(1)]. kept: 16 -P(k(i(a(k(c4,c5),c6),k(a(c4,c6),a(c5,c6))),i(k(a(c4,c6),a(c5,c6)),a(k(c4,c5),c6)))) # label("HIF4") # answer("HIF4"). [deny(2)]. kept: 17 -P(k(i(n(a(c7,c8)),k(n(c7),n(c8))),i(k(n(c7),n(c8)),n(a(c7,c8))))) # label("HIF5") # answer("HIF5"). [deny(3)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 4 -P(x) | -P(i(x,y)) | P(y). [assumption]. 5 P(i(x,i(y,x))) # label("A1"). [assumption]. 6 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) # label("A2"). [assumption]. 7 P(i(k(x,y),x)) # label("A3"). [assumption]. 8 P(i(k(x,y),y)) # label("A4"). [assumption]. 9 P(i(i(x,y),i(i(x,z),i(x,k(y,z))))) # label("A5"). [assumption]. 10 P(i(x,a(x,y))) # label("A6"). [assumption]. 11 P(i(x,a(y,x))) # label("A7"). [assumption]. 12 P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) # label("A8"). [assumption]. 13 P(i(i(x,n(y)),i(y,n(x)))) # label("A9"). [assumption]. 14 P(i(n(x),i(x,y))) # label("A10"). [assumption]. 15 -P(i(i(c1,c2),i(a(c1,c3),a(c2,c3)))) # label("H334") # answer("H334"). [deny(1)]. 16 -P(k(i(a(k(c4,c5),c6),k(a(c4,c6),a(c5,c6))),i(k(a(c4,c6),a(c5,c6)),a(k(c4,c5),c6)))) # label("HIF4") # answer("HIF4"). [deny(2)]. 17 -P(k(i(n(a(c7,c8)),k(n(c7),n(c8))),i(k(n(c7),n(c8)),n(a(c7,c8))))) # label("HIF5") # answer("HIF5"). [deny(3)]. end_of_list. formulas(demodulators). end_of_list. % 180 hints (180 processed, 0 redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=8): 4 -P(x) | -P(i(x,y)) | P(y). [assumption]. given #2 (I,wt=6): 5 P(i(x,i(y,x))) # label("A1"). [assumption]. given #3 (I,wt=14): 6 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) # label("A2"). [assumption]. given #4 (I,wt=6): 7 P(i(k(x,y),x)) # label("A3"). [assumption]. given #5 (I,wt=6): 8 P(i(k(x,y),y)) # label("A4"). [assumption]. given #6 (I,wt=14): 9 P(i(i(x,y),i(i(x,z),i(x,k(y,z))))) # label("A5"). [assumption]. given #7 (I,wt=6): 10 P(i(x,a(x,y))) # label("A6"). [assumption]. given #8 (I,wt=6): 11 P(i(x,a(y,x))) # label("A7"). [assumption]. given #9 (I,wt=14): 12 P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) # label("A8"). [assumption]. given #10 (I,wt=10): 13 P(i(i(x,n(y)),i(y,n(x)))) # label("A9"). [assumption]. given #11 (I,wt=7): 14 P(i(n(x),i(x,y))) # label("A10"). [assumption]. given #12 (I,wt=12): 15 -P(i(i(c1,c2),i(a(c1,c3),a(c2,c3)))) # label("H334") # answer("H334"). [deny(1)]. given #13 (I,wt=28): 16 -P(k(i(a(k(c4,c5),c6),k(a(c4,c6),a(c5,c6))),i(k(a(c4,c6),a(c5,c6)),a(k(c4,c5),c6)))) # label("HIF4") # answer("HIF4"). [deny(2)]. given #14 (I,wt=22): 17 -P(k(i(n(a(c7,c8)),k(n(c7),n(c8))),i(k(n(c7),n(c8)),n(a(c7,c8))))) # label("HIF5") # answer("HIF5"). [deny(3)]. given #15 (H,wt=8): 18 P(i(x,i(y,i(z,y)))). [hyper(4,a,5,a,b,5,a)]. given #16 (H,wt=8): 23 P(i(x,i(k(y,z),y))). [hyper(4,a,7,a,b,5,a)]. given #17 (H,wt=8): 25 P(i(x,i(k(y,z),z))). [hyper(4,a,8,a,b,5,a)]. given #18 (H,wt=8): 40 P(i(x,i(y,a(y,z)))). [hyper(4,a,10,a,b,5,a)]. given #19 (H,wt=8): 50 P(i(x,i(y,a(z,y)))). [hyper(4,a,11,a,b,5,a)]. given #20 (H,wt=9): 77 P(i(x,i(n(y),i(y,z)))). [hyper(4,a,14,a,b,5,a)]. given #21 (H,wt=10): 82 P(i(i(x,y),i(x,i(z,y)))). [hyper(4,a,18,a,b,6,a)]. given #22 (H,wt=8): 124 P(i(x,i(y,i(z,x)))). [hyper(4,a,5,a,b,82,a)]. given #23 (H,wt=10): 88 P(i(i(x,k(y,z)),i(x,y))). [hyper(4,a,23,a,b,6,a)]. given #24 (H,wt=8): 149 P(i(k(x,k(y,z)),y)). [hyper(4,a,8,a,b,88,a)]. given #25 (H,wt=10): 94 P(i(i(x,k(y,z)),i(x,z))). [hyper(4,a,25,a,b,6,a)]. given #26 (H,wt=8): 170 P(i(k(x,k(y,z)),z)). [hyper(4,a,8,a,b,94,a)]. given #27 (H,wt=10): 100 P(i(i(x,y),i(x,a(y,z)))). [hyper(4,a,40,a,b,6,a)]. given #28 (H,wt=8): 207 P(i(x,a(a(y,x),z))). [hyper(4,a,11,a,b,100,a)]. given #29 (H,wt=8): 208 P(i(x,a(a(x,y),z))). [hyper(4,a,10,a,b,100,a)]. given #30 (H,wt=8): 211 P(i(k(x,y),a(x,z))). [hyper(4,a,7,a,b,100,a)]. given #31 (H,wt=10): 106 P(i(i(x,y),i(x,a(z,y)))). [hyper(4,a,50,a,b,6,a)]. given #32 (H,wt=8): 324 P(i(x,a(y,i(z,x)))). [hyper(4,a,5,a,b,106,a)]. given #33 (H,wt=11): 112 P(i(i(x,n(y)),i(x,i(y,z)))). [hyper(4,a,77,a,b,6,a)]. given #34 (H,wt=12): 30 P(i(i(x,y),i(x,k(i(z,x),y)))). [hyper(4,a,5,a,b,9,a)]. given #35 (H,wt=10): 415 P(i(x,k(i(y,x),i(z,x)))). [hyper(4,a,5,a,b,30,a)]. given #36 (H,wt=12): 71 P(i(x,i(i(y,n(z)),i(z,n(y))))). [hyper(4,a,13,a,b,5,a)]. given #37 (H,wt=14): 27 P(i(i(k(x,y),z),i(k(x,y),k(y,z)))). [hyper(4,a,8,a,b,9,a)]. given #38 (H,wt=8): 502 P(i(k(x,y),k(y,x))). [hyper(4,a,7,a,b,27,a)]. given #39 (H,wt=14): 28 P(i(i(k(x,y),z),i(k(x,y),k(x,z)))). [hyper(4,a,7,a,b,9,a)]. given #40 (H,wt=10): 540 P(i(k(x,k(y,z)),k(x,z))). [hyper(4,a,170,a,b,28,a)]. given #41 (H,wt=14): 52 P(i(i(x,a(y,z)),i(a(z,x),a(y,z)))). [hyper(4,a,11,a,b,12,a)]. given #42 (H,wt=8): 593 P(i(a(x,y),a(y,x))). [hyper(4,a,10,a,b,52,a)]. given #43 (H,wt=10): 587 P(i(a(x,k(y,z)),a(y,x))). [hyper(4,a,211,a,b,52,a)]. given #44 (H,wt=10): 625 P(i(x,i(a(y,z),a(z,y)))). [hyper(4,a,593,a,b,5,a)]. given #45 (H,wt=12): 653 P(i(i(x,a(y,z)),i(x,a(z,y)))). [hyper(4,a,625,a,b,6,a)]. given #46 (H,wt=14): 483 P(i(i(x,i(y,n(z))),i(x,i(z,n(y))))). [hyper(4,a,71,a,b,6,a)]. given #47 (H,wt=16): 21 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))). [hyper(4,a,6,a,b,5,a)]. given #48 (H,wt=16): 24 P(i(i(k(x,i(y,z)),y),i(k(x,i(y,z)),z))). [hyper(4,a,8,a,b,6,a)]. given #49 (H,wt=8): 722 P(i(k(x,i(x,y)),y)). [hyper(4,a,7,a,b,24,a)]. given #50 (H,wt=10): 762 P(i(x,i(k(y,i(y,z)),z))). [hyper(4,a,722,a,b,5,a)]. given #51 (H,wt=12): 777 P(i(i(x,k(y,i(y,z))),i(x,z))). [hyper(4,a,762,a,b,6,a)]. given #52 (H,wt=4): 781 P(i(x,x)). [hyper(4,a,415,a,b,777,a)]. given #53 (H,wt=6): 811 P(i(x,n(n(x)))). [hyper(4,a,781,a,b,13,a)]. given #54 (H,wt=6): 817 P(i(x,i(y,y))). [hyper(4,a,781,a,b,5,a)]. given #55 (H,wt=7): 872 P(i(x,i(n(x),y))). [hyper(4,a,811,a,b,112,a)]. given #56 (H,wt=8): 780 P(i(k(i(x,y),x),y)). [hyper(4,a,502,a,b,777,a)]. given #57 (H,wt=8): 806 P(i(x,i(y,i(z,z)))). [hyper(4,a,781,a,b,124,a)]. given #58 (H,wt=10): 779 P(i(k(x,k(y,i(x,z))),z)). [hyper(4,a,540,a,b,777,a)]. given #59 (H,wt=10): 815 P(i(i(x,y),i(x,k(x,y)))). [hyper(4,a,781,a,b,9,a)]. given #60 (H,wt=10): 986 P(i(k(i(x,y),x),k(x,y))). [hyper(4,a,780,a,b,27,a)]. given #61 (H,wt=16): 961 P(i(i(x,i(n(y),z)),i(a(y,x),i(n(y),z)))). [hyper(4,a,872,a,b,12,a)]. given #62 (H,wt=9): 1152 P(i(a(x,y),i(n(x),y))). [hyper(4,a,5,a,b,961,a)]. given #63 (H,wt=11): 1190 P(i(x,i(a(y,z),i(n(y),z)))). [hyper(4,a,1152,a,b,5,a)]. given #64 (H,wt=13): 1207 P(i(i(x,a(y,z)),i(x,i(n(y),z)))). [hyper(4,a,1190,a,b,6,a)]. given #65 (H,wt=9): 1214 P(i(x,i(n(a(x,y)),z))). [hyper(4,a,208,a,b,1207,a)]. given #66 (H,wt=9): 1215 P(i(x,i(n(a(y,x)),z))). [hyper(4,a,207,a,b,1207,a)]. given #67 (H,wt=10): 1304 P(i(x,i(y,n(n(a(x,z)))))). [hyper(4,a,1214,a,b,483,a)]. given #68 (H,wt=11): 1397 P(i(x,i(y,i(n(a(z,x)),u)))). [hyper(4,a,1215,a,b,82,a)]. given #69 (H,wt=12): 1491 P(i(i(x,y),i(x,n(n(a(x,z)))))). [hyper(4,a,1304,a,b,6,a)]. given #70 (H,wt=12): 1590 P(i(i(x,y),i(n(a(x,z)),n(x)))). [hyper(4,a,1491,a,b,483,a)]. given #71 (H,wt=8): 1607 P(i(n(a(x,y)),n(x))). [hyper(4,a,1397,a,b,1590,a)]. given #72 (H,wt=17): 1651 P(i(i(n(a(x,y)),z),i(n(a(x,y)),k(n(x),z)))). [hyper(4,a,1607,a,b,9,a)]. given #73 (H,wt=18): 31 P(i(i(i(x,y),i(x,z)),i(i(x,y),i(x,k(y,z))))). [hyper(4,a,9,a,b,6,a)]. given #74 (H,wt=10): 1712 P(i(i(x,y),i(x,k(y,x)))). [hyper(4,a,817,a,b,31,a)]. given #75 (H,wt=8): 1776 P(i(x,k(i(y,y),x))). [hyper(4,a,817,a,b,1712,a)]. given #76 (H,wt=8): 1930 P(i(i(i(x,x),y),y)). [hyper(4,a,1776,a,b,777,a)]. given #77 (H,wt=12): 1850 P(i(x,i(i(y,z),i(y,k(z,y))))). [hyper(4,a,1712,a,b,5,a)]. given #78 (H,wt=18): 166 P(i(i(k(x,k(y,z)),u),i(k(x,k(y,z)),k(y,u)))). [hyper(4,a,149,a,b,9,a)]. given #79 (H,wt=12): 2020 P(i(k(x,k(y,i(x,z))),k(y,z))). [hyper(4,a,779,a,b,166,a)]. given #80 (H,wt=18): 711 P(i(i(x,i(y,i(z,u))),i(x,i(i(y,z),i(y,u))))). [hyper(4,a,21,a,b,6,a)]. given #81 (H,wt=12): 2128 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(4,a,5,a,b,711,a)]. given #82 (H,wt=10): 2170 P(i(i(x,y),i(x,n(n(y))))). [hyper(4,a,811,a,b,2128,a)]. given #83 (H,wt=8): 2297 P(i(x,n(n(a(y,x))))). [hyper(4,a,11,a,b,2170,a)]. given #84 (H,wt=8): 2432 P(i(n(a(x,y)),n(y))). [hyper(4,a,2297,a,b,13,a)]. given #85 (H,wt=10): 2314 P(i(i(x,y),i(n(y),n(x)))). [hyper(4,a,2170,a,b,483,a)]. given #86 (H,wt=11): 2443 P(i(n(a(x,y)),k(n(x),n(y)))). [hyper(4,a,2432,a,b,1651,a)]. given #87 (H,wt=12): 2157 P(i(i(x,i(i(y,y),z)),i(x,z))). [hyper(4,a,1930,a,b,2128,a)]. given #88 (H,wt=10): 2599 P(i(i(x,i(x,y)),i(x,y))). [hyper(4,a,6,a,b,2157,a)]. given #89 (H,wt=12): 2178 P(i(i(x,k(y,z)),i(x,k(z,y)))). [hyper(4,a,502,a,b,2128,a)]. given #90 (H,wt=14): 2166 P(i(i(x,k(i(y,z),y)),i(x,k(y,z)))). [hyper(4,a,986,a,b,2128,a)]. given #91 (H,wt=14): 2531 P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))). [hyper(4,a,2314,a,b,2128,a)]. given #92 (H,wt=16): 2155 P(i(i(x,i(y,z)),i(x,i(i(u,y),i(u,z))))). [hyper(4,a,2128,a,b,2128,a)]. given #93 (H,wt=20): 19 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))). [hyper(4,a,6,a,b,6,a)]. given #94 (H,wt=12): 2931 P(i(i(x,i(i(y,x),z)),i(x,z))). [hyper(4,a,18,a,b,19,a)]. given #95 (H,wt=8): 2964 P(i(x,i(y,k(x,y)))). [hyper(4,a,1850,a,b,2931,a)]. given #96 (H,wt=12): 3080 P(i(x,i(i(y,z),i(y,k(x,z))))). [hyper(4,a,2964,a,b,2155,a)]. given #97 (H,wt=12): 3081 P(i(i(x,y),i(x,i(z,k(y,z))))). [hyper(4,a,2964,a,b,2128,a)]. given #98 (H,wt=14): 2927 P(i(i(k(x,y),i(y,z)),i(k(x,y),z))). [hyper(4,a,25,a,b,19,a)]. given #99 (H,wt=14): 2929 P(i(i(k(x,y),i(x,z)),i(k(x,y),z))). [hyper(4,a,23,a,b,19,a)]. given #100 (H,wt=16): 2985 P(a(x,i(y,i(i(z,i(i(u,z),w)),i(z,w))))). [hyper(4,a,2931,a,b,324,a)]. given #101 (H,wt=16): 3144 P(i(i(x,y),i(x,k(i(z,i(u,i(w,w))),y)))). [hyper(4,a,806,a,b,3080,a)]. given #102 (H,wt=16): 3388 P(i(x,i(i(k(y,z),i(z,u)),i(k(y,z),u)))). [hyper(4,a,2927,a,b,5,a)]. given #103 (H,wt=10): 3582 P(i(i(x,y),i(k(z,x),y))). [hyper(4,a,3388,a,b,2931,a)]. given #104 (H,wt=16): 3429 P(i(x,i(i(k(y,z),i(y,u)),i(k(y,z),u)))). [hyper(4,a,2929,a,b,5,a)]. given #105 (H,wt=10): 3712 P(i(i(x,y),i(k(x,z),y))). [hyper(4,a,3429,a,b,2931,a)]. given #106 (H,wt=18): 3499 P(i(a(x,k(y,z)),k(i(u,i(w,i(v5,v5))),a(y,x)))). [hyper(4,a,587,a,b,3144,a)]. given #107 (H,wt=16): 3849 P(i(a(x,k(y,z)),k(a(y,x),i(u,i(w,w))))). [hyper(4,a,3499,a,b,2166,a)]. given #108 (H,wt=21): 380 P(i(i(x,i(y,i(z,u))),i(a(i(y,n(z)),x),i(y,i(z,u))))). [hyper(4,a,112,a,b,12,a)]. given #109 (H,wt=21): 3912 P(i(a(i(x,n(y)),i(x,i(i(z,x),i(y,u)))),i(x,i(y,u)))). [hyper(4,a,2931,a,b,380,a)]. given #110 (H,wt=10): 3990 P(i(i(i(x,y),z),i(y,z))). [hyper(4,a,2985,a,b,3912,a)]. given #111 (H,wt=8): 4041 P(i(x,i(y,k(y,x)))). [hyper(4,a,815,a,b,3990,a)]. given #112 (H,wt=10): 4135 P(i(x,k(x,i(y,n(n(y)))))). [hyper(4,a,811,a,b,4041,a)]. given #113 (H,wt=14): 4063 P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))). [hyper(4,a,3990,a,b,2128,a)]. given #114 (H,wt=12): 4409 P(i(i(x,i(y,z)),i(y,i(x,z)))). [hyper(4,a,6,a,b,4063,a)]. given #115 (H,wt=8): 4480 P(i(x,i(i(x,y),y))). [hyper(4,a,781,a,b,4409,a)]. given #116 (H,wt=9): 4477 P(i(n(x),i(a(x,y),y))). [hyper(4,a,1152,a,b,4409,a)]. given #117 (H,wt=10): 4651 P(i(i(i(x,a(x,y)),z),z)). [hyper(4,a,10,a,b,4480,a)]. given #118 (H,wt=11): 4707 P(i(n(x),i(n(y),n(a(x,y))))). [hyper(4,a,4477,a,b,2531,a)]. given #119 (H,wt=12): 4472 P(i(i(x,y),i(i(y,z),i(x,z)))). [hyper(4,a,2128,a,b,4409,a)]. given #120 (H,wt=12): 4848 P(i(i(i(x,k(x,y)),z),i(y,z))). [hyper(4,a,4041,a,b,4472,a)]. given #121 (H,wt=12): 4904 P(i(i(a(x,y),z),i(a(y,x),z))). [hyper(4,a,593,a,b,4472,a)]. given #122 (H,wt=12): 4989 P(i(x,i(i(k(y,x),z),i(y,z)))). [hyper(4,a,4472,a,b,4848,a)]. given #123 (H,wt=12): 5249 P(i(i(k(x,y),z),i(y,i(x,z)))). [hyper(4,a,4989,a,b,4409,a)]. given #124 (H,wt=14): 4759 P(i(i(x,i(i(y,a(y,z)),u)),i(x,u))). [hyper(4,a,4651,a,b,2128,a)]. given #125 (H,wt=14): 4852 P(i(i(i(k(x,y),z),u),i(i(x,z),u))). [hyper(4,a,3712,a,b,4472,a)]. given #126 (H,wt=12): 5439 P(i(i(x,i(y,z)),i(k(x,y),z))). [hyper(4,a,2927,a,b,4852,a)]. given #127 (H,wt=11): 5533 P(i(k(n(x),n(y)),n(a(x,y)))). [hyper(4,a,4707,a,b,5439,a)]. given #128 (H,wt=14): 4853 P(i(i(i(k(x,y),z),u),i(i(y,z),u))). [hyper(4,a,3582,a,b,4472,a)]. given #129 (H,wt=12): 5715 P(i(i(x,y),i(k(z,x),k(z,y)))). [hyper(4,a,28,a,b,4853,a)]. given #130 (H,wt=14): 4920 P(i(i(i(x,a(y,z)),u),i(i(x,y),u))). [hyper(4,a,100,a,b,4472,a)]. given #131 (H,wt=12): 5950 P(i(i(x,y),i(a(z,x),a(y,z)))). [hyper(4,a,52,a,b,4920,a)]. given #132 (H,wt=14): 5342 P(i(i(k(x,y),z),i(i(y,x),i(y,z)))). [hyper(4,a,5249,a,b,711,a)]. given #133 (H,wt=12): 6193 P(i(i(k(x,y),z),i(x,i(y,z)))). [hyper(4,a,5342,a,b,4063,a)]. given #134 (H,wt=10): 6255 P(i(x,i(y,a(z,k(x,y))))). [hyper(4,a,11,a,b,6193,a)]. given #135 (H,wt=14): 5376 P(i(i(x,a(y,z)),i(a(x,y),a(y,z)))). [hyper(4,a,12,a,b,4759,a)]. given #136 (H,wt=14): 5440 P(i(i(x,i(k(x,y),z)),i(k(x,y),z))). [hyper(4,a,2599,a,b,4852,a)]. given #137 (H,wt=14): 5853 P(i(k(x,i(y,k(z,u))),k(x,i(y,z)))). [hyper(4,a,88,a,b,5715,a)]. given #138 (H,wt=14): 6292 P(i(i(k(x,y),z),i(i(x,y),i(x,z)))). [hyper(4,a,6193,a,b,711,a)]. given #139 (H,wt=14): 6452 P(i(x,k(x,i(y,i(z,a(u,k(y,z))))))). [hyper(4,a,6255,a,b,4041,a)]. given #140 (H,wt=14): 6676 P(i(i(x,k(y,i(x,z))),i(x,k(y,z)))). [hyper(4,a,2020,a,b,6292,a)]. given #141 (H,wt=15): 5624 P(i(x,k(x,i(k(n(y),n(z)),n(a(y,z)))))). [hyper(4,a,5533,a,b,4041,a)]. -------- Proof 1 -------- "HIF5". ============================== PROOF ================================= % Proof 1 at 0.24 (+ 0.01) seconds: "HIF5". % Length of proof is 81. % Level of proof is 20. % Maximum clause weight is 22. % Given clauses 141. 3 P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(x),n(y)),n(a(x,y))))) # label("HIF5") # label(non_clause) # label(goal). [goal]. 4 -P(x) | -P(i(x,y)) | P(y). [assumption]. 5 P(i(x,i(y,x))) # label("A1"). [assumption]. 6 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) # label("A2"). [assumption]. 7 P(i(k(x,y),x)) # label("A3"). [assumption]. 8 P(i(k(x,y),y)) # label("A4"). [assumption]. 9 P(i(i(x,y),i(i(x,z),i(x,k(y,z))))) # label("A5"). [assumption]. 10 P(i(x,a(x,y))) # label("A6"). [assumption]. 11 P(i(x,a(y,x))) # label("A7"). [assumption]. 12 P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) # label("A8"). [assumption]. 13 P(i(i(x,n(y)),i(y,n(x)))) # label("A9"). [assumption]. 14 P(i(n(x),i(x,y))) # label("A10"). [assumption]. 17 -P(k(i(n(a(c7,c8)),k(n(c7),n(c8))),i(k(n(c7),n(c8)),n(a(c7,c8))))) # label("HIF5") # answer("HIF5"). [deny(3)]. 18 P(i(x,i(y,i(z,y)))). [hyper(4,a,5,a,b,5,a)]. 19 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))). [hyper(4,a,6,a,b,6,a)]. 21 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))). [hyper(4,a,6,a,b,5,a)]. 23 P(i(x,i(k(y,z),y))). [hyper(4,a,7,a,b,5,a)]. 24 P(i(i(k(x,i(y,z)),y),i(k(x,i(y,z)),z))). [hyper(4,a,8,a,b,6,a)]. 25 P(i(x,i(k(y,z),z))). [hyper(4,a,8,a,b,5,a)]. 30 P(i(i(x,y),i(x,k(i(z,x),y)))). [hyper(4,a,5,a,b,9,a)]. 40 P(i(x,i(y,a(y,z)))). [hyper(4,a,10,a,b,5,a)]. 50 P(i(x,i(y,a(z,y)))). [hyper(4,a,11,a,b,5,a)]. 71 P(i(x,i(i(y,n(z)),i(z,n(y))))). [hyper(4,a,13,a,b,5,a)]. 77 P(i(x,i(n(y),i(y,z)))). [hyper(4,a,14,a,b,5,a)]. 82 P(i(i(x,y),i(x,i(z,y)))). [hyper(4,a,18,a,b,6,a)]. 100 P(i(i(x,y),i(x,a(y,z)))). [hyper(4,a,40,a,b,6,a)]. 106 P(i(i(x,y),i(x,a(z,y)))). [hyper(4,a,50,a,b,6,a)]. 112 P(i(i(x,n(y)),i(x,i(y,z)))). [hyper(4,a,77,a,b,6,a)]. 207 P(i(x,a(a(y,x),z))). [hyper(4,a,11,a,b,100,a)]. 208 P(i(x,a(a(x,y),z))). [hyper(4,a,10,a,b,100,a)]. 324 P(i(x,a(y,i(z,x)))). [hyper(4,a,5,a,b,106,a)]. 380 P(i(i(x,i(y,i(z,u))),i(a(i(y,n(z)),x),i(y,i(z,u))))). [hyper(4,a,112,a,b,12,a)]. 415 P(i(x,k(i(y,x),i(z,x)))). [hyper(4,a,5,a,b,30,a)]. 483 P(i(i(x,i(y,n(z))),i(x,i(z,n(y))))). [hyper(4,a,71,a,b,6,a)]. 711 P(i(i(x,i(y,i(z,u))),i(x,i(i(y,z),i(y,u))))). [hyper(4,a,21,a,b,6,a)]. 722 P(i(k(x,i(x,y)),y)). [hyper(4,a,7,a,b,24,a)]. 762 P(i(x,i(k(y,i(y,z)),z))). [hyper(4,a,722,a,b,5,a)]. 777 P(i(i(x,k(y,i(y,z))),i(x,z))). [hyper(4,a,762,a,b,6,a)]. 781 P(i(x,x)). [hyper(4,a,415,a,b,777,a)]. 811 P(i(x,n(n(x)))). [hyper(4,a,781,a,b,13,a)]. 815 P(i(i(x,y),i(x,k(x,y)))). [hyper(4,a,781,a,b,9,a)]. 872 P(i(x,i(n(x),y))). [hyper(4,a,811,a,b,112,a)]. 961 P(i(i(x,i(n(y),z)),i(a(y,x),i(n(y),z)))). [hyper(4,a,872,a,b,12,a)]. 1152 P(i(a(x,y),i(n(x),y))). [hyper(4,a,5,a,b,961,a)]. 1190 P(i(x,i(a(y,z),i(n(y),z)))). [hyper(4,a,1152,a,b,5,a)]. 1207 P(i(i(x,a(y,z)),i(x,i(n(y),z)))). [hyper(4,a,1190,a,b,6,a)]. 1214 P(i(x,i(n(a(x,y)),z))). [hyper(4,a,208,a,b,1207,a)]. 1215 P(i(x,i(n(a(y,x)),z))). [hyper(4,a,207,a,b,1207,a)]. 1304 P(i(x,i(y,n(n(a(x,z)))))). [hyper(4,a,1214,a,b,483,a)]. 1397 P(i(x,i(y,i(n(a(z,x)),u)))). [hyper(4,a,1215,a,b,82,a)]. 1491 P(i(i(x,y),i(x,n(n(a(x,z)))))). [hyper(4,a,1304,a,b,6,a)]. 1590 P(i(i(x,y),i(n(a(x,z)),n(x)))). [hyper(4,a,1491,a,b,483,a)]. 1607 P(i(n(a(x,y)),n(x))). [hyper(4,a,1397,a,b,1590,a)]. 1651 P(i(i(n(a(x,y)),z),i(n(a(x,y)),k(n(x),z)))). [hyper(4,a,1607,a,b,9,a)]. 2128 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(4,a,5,a,b,711,a)]. 2170 P(i(i(x,y),i(x,n(n(y))))). [hyper(4,a,811,a,b,2128,a)]. 2297 P(i(x,n(n(a(y,x))))). [hyper(4,a,11,a,b,2170,a)]. 2314 P(i(i(x,y),i(n(y),n(x)))). [hyper(4,a,2170,a,b,483,a)]. 2432 P(i(n(a(x,y)),n(y))). [hyper(4,a,2297,a,b,13,a)]. 2443 P(i(n(a(x,y)),k(n(x),n(y)))). [hyper(4,a,2432,a,b,1651,a)]. 2531 P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))). [hyper(4,a,2314,a,b,2128,a)]. 2927 P(i(i(k(x,y),i(y,z)),i(k(x,y),z))). [hyper(4,a,25,a,b,19,a)]. 2929 P(i(i(k(x,y),i(x,z)),i(k(x,y),z))). [hyper(4,a,23,a,b,19,a)]. 2931 P(i(i(x,i(i(y,x),z)),i(x,z))). [hyper(4,a,18,a,b,19,a)]. 2985 P(a(x,i(y,i(i(z,i(i(u,z),w)),i(z,w))))). [hyper(4,a,2931,a,b,324,a)]. 3429 P(i(x,i(i(k(y,z),i(y,u)),i(k(y,z),u)))). [hyper(4,a,2929,a,b,5,a)]. 3712 P(i(i(x,y),i(k(x,z),y))). [hyper(4,a,3429,a,b,2931,a)]. 3912 P(i(a(i(x,n(y)),i(x,i(i(z,x),i(y,u)))),i(x,i(y,u)))). [hyper(4,a,2931,a,b,380,a)]. 3990 P(i(i(i(x,y),z),i(y,z))). [hyper(4,a,2985,a,b,3912,a)]. 4041 P(i(x,i(y,k(y,x)))). [hyper(4,a,815,a,b,3990,a)]. 4063 P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))). [hyper(4,a,3990,a,b,2128,a)]. 4409 P(i(i(x,i(y,z)),i(y,i(x,z)))). [hyper(4,a,6,a,b,4063,a)]. 4472 P(i(i(x,y),i(i(y,z),i(x,z)))). [hyper(4,a,2128,a,b,4409,a)]. 4477 P(i(n(x),i(a(x,y),y))). [hyper(4,a,1152,a,b,4409,a)]. 4707 P(i(n(x),i(n(y),n(a(x,y))))). [hyper(4,a,4477,a,b,2531,a)]. 4852 P(i(i(i(k(x,y),z),u),i(i(x,z),u))). [hyper(4,a,3712,a,b,4472,a)]. 5439 P(i(i(x,i(y,z)),i(k(x,y),z))). [hyper(4,a,2927,a,b,4852,a)]. 5533 P(i(k(n(x),n(y)),n(a(x,y)))). [hyper(4,a,4707,a,b,5439,a)]. 5624 P(i(x,k(x,i(k(n(y),n(z)),n(a(y,z)))))). [hyper(4,a,5533,a,b,4041,a)]. 7035 P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(z),n(u)),n(a(z,u))))). [hyper(4,a,2443,a,b,5624,a)]. 7036 $F # answer("HIF5"). [resolve(7035,a,17,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 17 given #142 (H,wt=16): 5102 P(i(i(x,i(a(y,z),u)),i(x,i(a(z,y),u)))). [hyper(4,a,4904,a,b,2128,a)]. -------- Proof 2 -------- "H334". ============================== PROOF ================================= % Proof 2 at 0.24 (+ 0.01) seconds: "H334". % Length of proof is 37. % Level of proof is 12. % Maximum clause weight is 21. % Given clauses 142. 1 P(i(i(x,y),i(a(x,z),a(y,z)))) # label("H334") # label(non_clause) # label(goal). [goal]. 4 -P(x) | -P(i(x,y)) | P(y). [assumption]. 5 P(i(x,i(y,x))) # label("A1"). [assumption]. 6 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) # label("A2"). [assumption]. 10 P(i(x,a(x,y))) # label("A6"). [assumption]. 11 P(i(x,a(y,x))) # label("A7"). [assumption]. 12 P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) # label("A8"). [assumption]. 14 P(i(n(x),i(x,y))) # label("A10"). [assumption]. 15 -P(i(i(c1,c2),i(a(c1,c3),a(c2,c3)))) # label("H334") # answer("H334"). [deny(1)]. 18 P(i(x,i(y,i(z,y)))). [hyper(4,a,5,a,b,5,a)]. 19 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))). [hyper(4,a,6,a,b,6,a)]. 21 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))). [hyper(4,a,6,a,b,5,a)]. 40 P(i(x,i(y,a(y,z)))). [hyper(4,a,10,a,b,5,a)]. 50 P(i(x,i(y,a(z,y)))). [hyper(4,a,11,a,b,5,a)]. 52 P(i(i(x,a(y,z)),i(a(z,x),a(y,z)))). [hyper(4,a,11,a,b,12,a)]. 77 P(i(x,i(n(y),i(y,z)))). [hyper(4,a,14,a,b,5,a)]. 100 P(i(i(x,y),i(x,a(y,z)))). [hyper(4,a,40,a,b,6,a)]. 106 P(i(i(x,y),i(x,a(z,y)))). [hyper(4,a,50,a,b,6,a)]. 112 P(i(i(x,n(y)),i(x,i(y,z)))). [hyper(4,a,77,a,b,6,a)]. 324 P(i(x,a(y,i(z,x)))). [hyper(4,a,5,a,b,106,a)]. 380 P(i(i(x,i(y,i(z,u))),i(a(i(y,n(z)),x),i(y,i(z,u))))). [hyper(4,a,112,a,b,12,a)]. 593 P(i(a(x,y),a(y,x))). [hyper(4,a,10,a,b,52,a)]. 711 P(i(i(x,i(y,i(z,u))),i(x,i(i(y,z),i(y,u))))). [hyper(4,a,21,a,b,6,a)]. 2128 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(4,a,5,a,b,711,a)]. 2931 P(i(i(x,i(i(y,x),z)),i(x,z))). [hyper(4,a,18,a,b,19,a)]. 2985 P(a(x,i(y,i(i(z,i(i(u,z),w)),i(z,w))))). [hyper(4,a,2931,a,b,324,a)]. 3912 P(i(a(i(x,n(y)),i(x,i(i(z,x),i(y,u)))),i(x,i(y,u)))). [hyper(4,a,2931,a,b,380,a)]. 3990 P(i(i(i(x,y),z),i(y,z))). [hyper(4,a,2985,a,b,3912,a)]. 4063 P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))). [hyper(4,a,3990,a,b,2128,a)]. 4409 P(i(i(x,i(y,z)),i(y,i(x,z)))). [hyper(4,a,6,a,b,4063,a)]. 4472 P(i(i(x,y),i(i(y,z),i(x,z)))). [hyper(4,a,2128,a,b,4409,a)]. 4904 P(i(i(a(x,y),z),i(a(y,x),z))). [hyper(4,a,593,a,b,4472,a)]. 4920 P(i(i(i(x,a(y,z)),u),i(i(x,y),u))). [hyper(4,a,100,a,b,4472,a)]. 5102 P(i(i(x,i(a(y,z),u)),i(x,i(a(z,y),u)))). [hyper(4,a,4904,a,b,2128,a)]. 5950 P(i(i(x,y),i(a(z,x),a(y,z)))). [hyper(4,a,52,a,b,4920,a)]. 7180 P(i(i(x,y),i(a(x,z),a(y,z)))). [hyper(4,a,5950,a,b,5102,a)]. 7181 $F # answer("H334"). [resolve(7180,a,15,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 15 given #143 (H,wt=12): 7180 P(i(i(x,y),i(a(x,z),a(y,z)))). [hyper(4,a,5950,a,b,5102,a)]. given #144 (H,wt=16): 5592 P(i(i(x,i(y,i(z,u))),i(x,i(k(y,z),u)))). [hyper(4,a,5439,a,b,2128,a)]. given #145 (H,wt=12): 7476 P(i(i(x,y),i(k(x,z),k(y,z)))). [hyper(4,a,3081,a,b,5592,a)]. given #146 (H,wt=16): 5769 P(i(k(x,i(y,i(z,u))),k(x,i(k(y,z),u)))). [hyper(4,a,5439,a,b,5715,a)]. given #147 (H,wt=16): 5782 P(i(k(x,i(y,i(z,u))),k(x,i(z,i(y,u))))). [hyper(4,a,4409,a,b,5715,a)]. given #148 (H,wt=16): 5805 P(i(k(x,i(y,k(z,u))),k(x,i(y,k(u,z))))). [hyper(4,a,2178,a,b,5715,a)]. given #149 (H,wt=16): 5833 P(i(k(x,i(y,a(z,u))),k(x,i(y,a(u,z))))). [hyper(4,a,653,a,b,5715,a)]. given #150 (H,wt=16): 7597 P(i(k(i(a(x,y),z),u),k(i(a(y,x),z),u))). [hyper(4,a,4904,a,b,7476,a)]. given #151 (H,wt=18): 5776 P(i(k(x,i(y,i(i(z,a(z,u)),w))),k(x,i(y,w)))). [hyper(4,a,4759,a,b,5715,a)]. given #152 (H,wt=18): 5855 P(i(k(x,i(y,a(z,u))),k(x,i(a(u,y),a(z,u))))). [hyper(4,a,52,a,b,5715,a)]. given #153 (H,wt=18): 6542 P(i(i(x,i(y,a(z,u))),i(x,i(a(y,z),a(z,u))))). [hyper(4,a,5376,a,b,2128,a)]. given #154 (H,wt=18): 6570 P(i(k(x,i(y,i(k(y,z),u))),k(x,i(k(y,z),u)))). [hyper(4,a,5440,a,b,5715,a)]. given #155 (H,wt=18): 6903 P(i(i(x,y),i(x,k(y,i(z,i(u,a(w,k(z,u)))))))). [hyper(4,a,6452,a,b,2128,a)]. given #156 (H,wt=20): 7792 P(i(i(x,k(y,i(z,i(u,w)))),i(x,k(y,i(k(z,u),w))))). [hyper(4,a,5769,a,b,2128,a)]. given #157 (H,wt=20): 7846 P(i(i(x,k(y,i(z,i(u,w)))),i(x,k(y,i(u,i(z,w)))))). [hyper(4,a,5782,a,b,2128,a)]. given #158 (H,wt=22): 7035 P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(z),n(u)),n(a(z,u))))). [hyper(4,a,2443,a,b,5624,a)]. given #159 (H,wt=22): 8059 P(i(i(x,k(y,i(z,i(i(u,a(u,w)),v5)))),i(x,k(y,i(z,v5))))). [hyper(4,a,5776,a,b,2128,a)]. given #160 (H,wt=18): 8674 P(i(a(x,k(y,z)),k(a(y,x),i(u,i(w,a(w,v5)))))). [hyper(4,a,3849,a,b,8059,a)]. given #161 (H,wt=18): 8745 P(i(a(x,k(y,z)),k(a(y,x),i(k(u,w),a(w,v5))))). [hyper(4,a,8674,a,b,7792,a)]. given #162 (H,wt=22): 8112 P(i(i(x,k(y,i(z,a(u,w)))),i(x,k(y,i(a(w,z),a(u,w)))))). [hyper(4,a,5855,a,b,2128,a)]. given #163 (H,wt=20): 8844 P(i(a(x,k(y,z)),k(a(y,x),i(a(u,k(w,v5)),a(v5,u))))). [hyper(4,a,8745,a,b,8112,a)]. given #164 (H,wt=14): 8924 P(i(a(x,k(y,z)),k(a(y,x),a(z,x)))). [hyper(4,a,8844,a,b,6676,a)]. given #165 (H,wt=20): 8984 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,n(n(u))))). [hyper(4,a,8924,a,b,4135,a)]. given #166 (H,wt=22): 8189 P(i(k(x,i(y,i(z,a(u,w)))),k(x,i(y,i(a(z,u),a(u,w)))))). [hyper(4,a,6542,a,b,5715,a)]. given #167 (H,wt=22): 8440 P(i(k(x,i(y,z)),k(x,i(y,k(z,i(u,i(w,a(v5,k(u,w))))))))). [hyper(4,a,6903,a,b,5715,a)]. given #168 (H,wt=24): 8516 P(i(k(x,i(y,k(z,i(u,i(w,v5))))),k(x,i(y,k(z,i(k(u,w),v5)))))). [hyper(4,a,7792,a,b,5715,a)]. given #169 (H,wt=24): 8591 P(i(k(x,i(y,k(z,i(u,i(w,v5))))),k(x,i(y,k(z,i(w,i(u,v5))))))). [hyper(4,a,7846,a,b,5715,a)]. given #170 (H,wt=26): 9077 P(i(i(x,k(y,i(z,i(u,a(w,v5))))),i(x,k(y,i(z,i(a(u,w),a(w,v5))))))). [hyper(4,a,8189,a,b,2128,a)]. given #171 (H,wt=30): 9103 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(v5,a(v6,k(w,v5)))))))). [hyper(4,a,8984,a,b,8440,a)]. given #172 (H,wt=30): 9296 P(i(k(x,i(y,k(z,i(u,i(w,a(v5,v6)))))),k(x,i(y,k(z,i(u,i(a(w,v5),a(v5,v6)))))))). [hyper(4,a,9077,a,b,5715,a)]. given #173 (H,wt=30): 9346 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(v5,a(v6,k(v5,w)))))))). [hyper(4,a,9103,a,b,8591,a)]. given #174 (H,wt=32): 9433 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(a(v5,v6),a(v6,k(v5,w)))))))). [hyper(4,a,9346,a,b,9296,a)]. given #175 (H,wt=32): 9467 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(a(w,v5),i(v6,a(v5,k(w,v6)))))))). [hyper(4,a,9433,a,b,8591,a)]. given #176 (H,wt=34): 9500 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(a(w,v5),i(a(v6,v5),a(v5,k(w,v6)))))))). [hyper(4,a,9467,a,b,9296,a)]. given #177 (H,wt=34): 9535 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6))))))). [hyper(4,a,9500,a,b,8516,a)]. given #178 (H,wt=34): 9571 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6))),n(n(u)))))). [hyper(4,a,9535,a,b,5805,a)]. given #179 (H,wt=30): 9602 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6)))))). [hyper(4,a,9571,a,b,5853,a)]. given #180 (H,wt=28): 9632 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(k(a(u,w),a(v5,w)),a(w,k(u,v5))))). [hyper(4,a,9602,a,b,6570,a)]. given #181 (H,wt=28): 9664 P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(u,w),a(v5,w)),a(w,k(u,v5))))). [hyper(4,a,9632,a,b,7597,a)]. -------- Proof 3 -------- "HIF4". ============================== PROOF ================================= % Proof 3 at 0.35 (+ 0.02) seconds: "HIF4". % Length of proof is 150. % Level of proof is 30. % Maximum clause weight is 34. % Given clauses 181. 2 P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(x,z),a(y,z)),a(k(x,y),z)))) # label("HIF4") # label(non_clause) # label(goal). [goal]. 4 -P(x) | -P(i(x,y)) | P(y). [assumption]. 5 P(i(x,i(y,x))) # label("A1"). [assumption]. 6 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) # label("A2"). [assumption]. 7 P(i(k(x,y),x)) # label("A3"). [assumption]. 8 P(i(k(x,y),y)) # label("A4"). [assumption]. 9 P(i(i(x,y),i(i(x,z),i(x,k(y,z))))) # label("A5"). [assumption]. 10 P(i(x,a(x,y))) # label("A6"). [assumption]. 11 P(i(x,a(y,x))) # label("A7"). [assumption]. 12 P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) # label("A8"). [assumption]. 13 P(i(i(x,n(y)),i(y,n(x)))) # label("A9"). [assumption]. 14 P(i(n(x),i(x,y))) # label("A10"). [assumption]. 16 -P(k(i(a(k(c4,c5),c6),k(a(c4,c6),a(c5,c6))),i(k(a(c4,c6),a(c5,c6)),a(k(c4,c5),c6)))) # label("HIF4") # answer("HIF4"). [deny(2)]. 18 P(i(x,i(y,i(z,y)))). [hyper(4,a,5,a,b,5,a)]. 19 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))). [hyper(4,a,6,a,b,6,a)]. 21 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))). [hyper(4,a,6,a,b,5,a)]. 23 P(i(x,i(k(y,z),y))). [hyper(4,a,7,a,b,5,a)]. 24 P(i(i(k(x,i(y,z)),y),i(k(x,i(y,z)),z))). [hyper(4,a,8,a,b,6,a)]. 25 P(i(x,i(k(y,z),z))). [hyper(4,a,8,a,b,5,a)]. 27 P(i(i(k(x,y),z),i(k(x,y),k(y,z)))). [hyper(4,a,8,a,b,9,a)]. 28 P(i(i(k(x,y),z),i(k(x,y),k(x,z)))). [hyper(4,a,7,a,b,9,a)]. 30 P(i(i(x,y),i(x,k(i(z,x),y)))). [hyper(4,a,5,a,b,9,a)]. 31 P(i(i(i(x,y),i(x,z)),i(i(x,y),i(x,k(y,z))))). [hyper(4,a,9,a,b,6,a)]. 40 P(i(x,i(y,a(y,z)))). [hyper(4,a,10,a,b,5,a)]. 50 P(i(x,i(y,a(z,y)))). [hyper(4,a,11,a,b,5,a)]. 52 P(i(i(x,a(y,z)),i(a(z,x),a(y,z)))). [hyper(4,a,11,a,b,12,a)]. 77 P(i(x,i(n(y),i(y,z)))). [hyper(4,a,14,a,b,5,a)]. 82 P(i(i(x,y),i(x,i(z,y)))). [hyper(4,a,18,a,b,6,a)]. 88 P(i(i(x,k(y,z)),i(x,y))). [hyper(4,a,23,a,b,6,a)]. 94 P(i(i(x,k(y,z)),i(x,z))). [hyper(4,a,25,a,b,6,a)]. 100 P(i(i(x,y),i(x,a(y,z)))). [hyper(4,a,40,a,b,6,a)]. 106 P(i(i(x,y),i(x,a(z,y)))). [hyper(4,a,50,a,b,6,a)]. 112 P(i(i(x,n(y)),i(x,i(y,z)))). [hyper(4,a,77,a,b,6,a)]. 124 P(i(x,i(y,i(z,x)))). [hyper(4,a,5,a,b,82,a)]. 149 P(i(k(x,k(y,z)),y)). [hyper(4,a,8,a,b,88,a)]. 166 P(i(i(k(x,k(y,z)),u),i(k(x,k(y,z)),k(y,u)))). [hyper(4,a,149,a,b,9,a)]. 170 P(i(k(x,k(y,z)),z)). [hyper(4,a,8,a,b,94,a)]. 211 P(i(k(x,y),a(x,z))). [hyper(4,a,7,a,b,100,a)]. 324 P(i(x,a(y,i(z,x)))). [hyper(4,a,5,a,b,106,a)]. 380 P(i(i(x,i(y,i(z,u))),i(a(i(y,n(z)),x),i(y,i(z,u))))). [hyper(4,a,112,a,b,12,a)]. 415 P(i(x,k(i(y,x),i(z,x)))). [hyper(4,a,5,a,b,30,a)]. 502 P(i(k(x,y),k(y,x))). [hyper(4,a,7,a,b,27,a)]. 540 P(i(k(x,k(y,z)),k(x,z))). [hyper(4,a,170,a,b,28,a)]. 587 P(i(a(x,k(y,z)),a(y,x))). [hyper(4,a,211,a,b,52,a)]. 593 P(i(a(x,y),a(y,x))). [hyper(4,a,10,a,b,52,a)]. 625 P(i(x,i(a(y,z),a(z,y)))). [hyper(4,a,593,a,b,5,a)]. 653 P(i(i(x,a(y,z)),i(x,a(z,y)))). [hyper(4,a,625,a,b,6,a)]. 711 P(i(i(x,i(y,i(z,u))),i(x,i(i(y,z),i(y,u))))). [hyper(4,a,21,a,b,6,a)]. 722 P(i(k(x,i(x,y)),y)). [hyper(4,a,7,a,b,24,a)]. 762 P(i(x,i(k(y,i(y,z)),z))). [hyper(4,a,722,a,b,5,a)]. 777 P(i(i(x,k(y,i(y,z))),i(x,z))). [hyper(4,a,762,a,b,6,a)]. 779 P(i(k(x,k(y,i(x,z))),z)). [hyper(4,a,540,a,b,777,a)]. 780 P(i(k(i(x,y),x),y)). [hyper(4,a,502,a,b,777,a)]. 781 P(i(x,x)). [hyper(4,a,415,a,b,777,a)]. 806 P(i(x,i(y,i(z,z)))). [hyper(4,a,781,a,b,124,a)]. 811 P(i(x,n(n(x)))). [hyper(4,a,781,a,b,13,a)]. 815 P(i(i(x,y),i(x,k(x,y)))). [hyper(4,a,781,a,b,9,a)]. 817 P(i(x,i(y,y))). [hyper(4,a,781,a,b,5,a)]. 986 P(i(k(i(x,y),x),k(x,y))). [hyper(4,a,780,a,b,27,a)]. 1712 P(i(i(x,y),i(x,k(y,x)))). [hyper(4,a,817,a,b,31,a)]. 1776 P(i(x,k(i(y,y),x))). [hyper(4,a,817,a,b,1712,a)]. 1850 P(i(x,i(i(y,z),i(y,k(z,y))))). [hyper(4,a,1712,a,b,5,a)]. 1930 P(i(i(i(x,x),y),y)). [hyper(4,a,1776,a,b,777,a)]. 2020 P(i(k(x,k(y,i(x,z))),k(y,z))). [hyper(4,a,779,a,b,166,a)]. 2128 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(4,a,5,a,b,711,a)]. 2155 P(i(i(x,i(y,z)),i(x,i(i(u,y),i(u,z))))). [hyper(4,a,2128,a,b,2128,a)]. 2157 P(i(i(x,i(i(y,y),z)),i(x,z))). [hyper(4,a,1930,a,b,2128,a)]. 2166 P(i(i(x,k(i(y,z),y)),i(x,k(y,z)))). [hyper(4,a,986,a,b,2128,a)]. 2178 P(i(i(x,k(y,z)),i(x,k(z,y)))). [hyper(4,a,502,a,b,2128,a)]. 2599 P(i(i(x,i(x,y)),i(x,y))). [hyper(4,a,6,a,b,2157,a)]. 2927 P(i(i(k(x,y),i(y,z)),i(k(x,y),z))). [hyper(4,a,25,a,b,19,a)]. 2929 P(i(i(k(x,y),i(x,z)),i(k(x,y),z))). [hyper(4,a,23,a,b,19,a)]. 2931 P(i(i(x,i(i(y,x),z)),i(x,z))). [hyper(4,a,18,a,b,19,a)]. 2964 P(i(x,i(y,k(x,y)))). [hyper(4,a,1850,a,b,2931,a)]. 2985 P(a(x,i(y,i(i(z,i(i(u,z),w)),i(z,w))))). [hyper(4,a,2931,a,b,324,a)]. 3080 P(i(x,i(i(y,z),i(y,k(x,z))))). [hyper(4,a,2964,a,b,2155,a)]. 3081 P(i(i(x,y),i(x,i(z,k(y,z))))). [hyper(4,a,2964,a,b,2128,a)]. 3144 P(i(i(x,y),i(x,k(i(z,i(u,i(w,w))),y)))). [hyper(4,a,806,a,b,3080,a)]. 3388 P(i(x,i(i(k(y,z),i(z,u)),i(k(y,z),u)))). [hyper(4,a,2927,a,b,5,a)]. 3429 P(i(x,i(i(k(y,z),i(y,u)),i(k(y,z),u)))). [hyper(4,a,2929,a,b,5,a)]. 3499 P(i(a(x,k(y,z)),k(i(u,i(w,i(v5,v5))),a(y,x)))). [hyper(4,a,587,a,b,3144,a)]. 3582 P(i(i(x,y),i(k(z,x),y))). [hyper(4,a,3388,a,b,2931,a)]. 3712 P(i(i(x,y),i(k(x,z),y))). [hyper(4,a,3429,a,b,2931,a)]. 3849 P(i(a(x,k(y,z)),k(a(y,x),i(u,i(w,w))))). [hyper(4,a,3499,a,b,2166,a)]. 3912 P(i(a(i(x,n(y)),i(x,i(i(z,x),i(y,u)))),i(x,i(y,u)))). [hyper(4,a,2931,a,b,380,a)]. 3990 P(i(i(i(x,y),z),i(y,z))). [hyper(4,a,2985,a,b,3912,a)]. 4041 P(i(x,i(y,k(y,x)))). [hyper(4,a,815,a,b,3990,a)]. 4063 P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))). [hyper(4,a,3990,a,b,2128,a)]. 4135 P(i(x,k(x,i(y,n(n(y)))))). [hyper(4,a,811,a,b,4041,a)]. 4409 P(i(i(x,i(y,z)),i(y,i(x,z)))). [hyper(4,a,6,a,b,4063,a)]. 4472 P(i(i(x,y),i(i(y,z),i(x,z)))). [hyper(4,a,2128,a,b,4409,a)]. 4480 P(i(x,i(i(x,y),y))). [hyper(4,a,781,a,b,4409,a)]. 4651 P(i(i(i(x,a(x,y)),z),z)). [hyper(4,a,10,a,b,4480,a)]. 4759 P(i(i(x,i(i(y,a(y,z)),u)),i(x,u))). [hyper(4,a,4651,a,b,2128,a)]. 4848 P(i(i(i(x,k(x,y)),z),i(y,z))). [hyper(4,a,4041,a,b,4472,a)]. 4852 P(i(i(i(k(x,y),z),u),i(i(x,z),u))). [hyper(4,a,3712,a,b,4472,a)]. 4853 P(i(i(i(k(x,y),z),u),i(i(y,z),u))). [hyper(4,a,3582,a,b,4472,a)]. 4904 P(i(i(a(x,y),z),i(a(y,x),z))). [hyper(4,a,593,a,b,4472,a)]. 4989 P(i(x,i(i(k(y,x),z),i(y,z)))). [hyper(4,a,4472,a,b,4848,a)]. 5249 P(i(i(k(x,y),z),i(y,i(x,z)))). [hyper(4,a,4989,a,b,4409,a)]. 5342 P(i(i(k(x,y),z),i(i(y,x),i(y,z)))). [hyper(4,a,5249,a,b,711,a)]. 5376 P(i(i(x,a(y,z)),i(a(x,y),a(y,z)))). [hyper(4,a,12,a,b,4759,a)]. 5439 P(i(i(x,i(y,z)),i(k(x,y),z))). [hyper(4,a,2927,a,b,4852,a)]. 5440 P(i(i(x,i(k(x,y),z)),i(k(x,y),z))). [hyper(4,a,2599,a,b,4852,a)]. 5592 P(i(i(x,i(y,i(z,u))),i(x,i(k(y,z),u)))). [hyper(4,a,5439,a,b,2128,a)]. 5715 P(i(i(x,y),i(k(z,x),k(z,y)))). [hyper(4,a,28,a,b,4853,a)]. 5769 P(i(k(x,i(y,i(z,u))),k(x,i(k(y,z),u)))). [hyper(4,a,5439,a,b,5715,a)]. 5776 P(i(k(x,i(y,i(i(z,a(z,u)),w))),k(x,i(y,w)))). [hyper(4,a,4759,a,b,5715,a)]. 5782 P(i(k(x,i(y,i(z,u))),k(x,i(z,i(y,u))))). [hyper(4,a,4409,a,b,5715,a)]. 5805 P(i(k(x,i(y,k(z,u))),k(x,i(y,k(u,z))))). [hyper(4,a,2178,a,b,5715,a)]. 5833 P(i(k(x,i(y,a(z,u))),k(x,i(y,a(u,z))))). [hyper(4,a,653,a,b,5715,a)]. 5853 P(i(k(x,i(y,k(z,u))),k(x,i(y,z)))). [hyper(4,a,88,a,b,5715,a)]. 5855 P(i(k(x,i(y,a(z,u))),k(x,i(a(u,y),a(z,u))))). [hyper(4,a,52,a,b,5715,a)]. 6193 P(i(i(k(x,y),z),i(x,i(y,z)))). [hyper(4,a,5342,a,b,4063,a)]. 6255 P(i(x,i(y,a(z,k(x,y))))). [hyper(4,a,11,a,b,6193,a)]. 6292 P(i(i(k(x,y),z),i(i(x,y),i(x,z)))). [hyper(4,a,6193,a,b,711,a)]. 6452 P(i(x,k(x,i(y,i(z,a(u,k(y,z))))))). [hyper(4,a,6255,a,b,4041,a)]. 6542 P(i(i(x,i(y,a(z,u))),i(x,i(a(y,z),a(z,u))))). [hyper(4,a,5376,a,b,2128,a)]. 6570 P(i(k(x,i(y,i(k(y,z),u))),k(x,i(k(y,z),u)))). [hyper(4,a,5440,a,b,5715,a)]. 6676 P(i(i(x,k(y,i(x,z))),i(x,k(y,z)))). [hyper(4,a,2020,a,b,6292,a)]. 6903 P(i(i(x,y),i(x,k(y,i(z,i(u,a(w,k(z,u)))))))). [hyper(4,a,6452,a,b,2128,a)]. 7476 P(i(i(x,y),i(k(x,z),k(y,z)))). [hyper(4,a,3081,a,b,5592,a)]. 7597 P(i(k(i(a(x,y),z),u),k(i(a(y,x),z),u))). [hyper(4,a,4904,a,b,7476,a)]. 7792 P(i(i(x,k(y,i(z,i(u,w)))),i(x,k(y,i(k(z,u),w))))). [hyper(4,a,5769,a,b,2128,a)]. 7846 P(i(i(x,k(y,i(z,i(u,w)))),i(x,k(y,i(u,i(z,w)))))). [hyper(4,a,5782,a,b,2128,a)]. 8059 P(i(i(x,k(y,i(z,i(i(u,a(u,w)),v5)))),i(x,k(y,i(z,v5))))). [hyper(4,a,5776,a,b,2128,a)]. 8112 P(i(i(x,k(y,i(z,a(u,w)))),i(x,k(y,i(a(w,z),a(u,w)))))). [hyper(4,a,5855,a,b,2128,a)]. 8189 P(i(k(x,i(y,i(z,a(u,w)))),k(x,i(y,i(a(z,u),a(u,w)))))). [hyper(4,a,6542,a,b,5715,a)]. 8440 P(i(k(x,i(y,z)),k(x,i(y,k(z,i(u,i(w,a(v5,k(u,w))))))))). [hyper(4,a,6903,a,b,5715,a)]. 8516 P(i(k(x,i(y,k(z,i(u,i(w,v5))))),k(x,i(y,k(z,i(k(u,w),v5)))))). [hyper(4,a,7792,a,b,5715,a)]. 8591 P(i(k(x,i(y,k(z,i(u,i(w,v5))))),k(x,i(y,k(z,i(w,i(u,v5))))))). [hyper(4,a,7846,a,b,5715,a)]. 8674 P(i(a(x,k(y,z)),k(a(y,x),i(u,i(w,a(w,v5)))))). [hyper(4,a,3849,a,b,8059,a)]. 8745 P(i(a(x,k(y,z)),k(a(y,x),i(k(u,w),a(w,v5))))). [hyper(4,a,8674,a,b,7792,a)]. 8844 P(i(a(x,k(y,z)),k(a(y,x),i(a(u,k(w,v5)),a(v5,u))))). [hyper(4,a,8745,a,b,8112,a)]. 8924 P(i(a(x,k(y,z)),k(a(y,x),a(z,x)))). [hyper(4,a,8844,a,b,6676,a)]. 8984 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,n(n(u))))). [hyper(4,a,8924,a,b,4135,a)]. 9077 P(i(i(x,k(y,i(z,i(u,a(w,v5))))),i(x,k(y,i(z,i(a(u,w),a(w,v5))))))). [hyper(4,a,8189,a,b,2128,a)]. 9103 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(v5,a(v6,k(w,v5)))))))). [hyper(4,a,8984,a,b,8440,a)]. 9296 P(i(k(x,i(y,k(z,i(u,i(w,a(v5,v6)))))),k(x,i(y,k(z,i(u,i(a(w,v5),a(v5,v6)))))))). [hyper(4,a,9077,a,b,5715,a)]. 9346 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(v5,a(v6,k(v5,w)))))))). [hyper(4,a,9103,a,b,8591,a)]. 9433 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(a(v5,v6),a(v6,k(v5,w)))))))). [hyper(4,a,9346,a,b,9296,a)]. 9467 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(a(w,v5),i(v6,a(v5,k(w,v6)))))))). [hyper(4,a,9433,a,b,8591,a)]. 9500 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(a(w,v5),i(a(v6,v5),a(v5,k(w,v6)))))))). [hyper(4,a,9467,a,b,9296,a)]. 9535 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6))))))). [hyper(4,a,9500,a,b,8516,a)]. 9571 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6))),n(n(u)))))). [hyper(4,a,9535,a,b,5805,a)]. 9602 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6)))))). [hyper(4,a,9571,a,b,5853,a)]. 9632 P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(k(a(u,w),a(v5,w)),a(w,k(u,v5))))). [hyper(4,a,9602,a,b,6570,a)]. 9664 P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(u,w),a(v5,w)),a(w,k(u,v5))))). [hyper(4,a,9632,a,b,7597,a)]. 9697 P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(u,w),a(v5,w)),a(k(u,v5),w)))). [hyper(4,a,9664,a,b,5833,a)]. 9698 $F # answer("HIF4"). [resolve(9697,a,16,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=181. Generated=14482. Kept=9692. proofs=3. Usable=177. Sos=9480. Demods=0. Limbo=4, Disabled=44. Hints=180. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=4790. Back_subsumed=28. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=1. Megabytes=18.30. User_CPU=0.35, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 3 proofs. ------ process 1150 exit (max_proofs) ------  Process 1150 exit (max_proofs) Sat May 7 08:59:27 2011