============================== NewAuto =============================== NewAuto (32) version June-2006A, June 2006. Process 27974 was started by veroff on lunar, Fri Jun 23 23:44:07 2006 The command was "/nfs/faculty/veroff/PROVER/LADR/prover9.src/newsax -f ec.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ec.in set(auto). % set(auto) -> set(auto_inference). % set(auto_inference) -> set(predicate_elim). % set(auto_inference) -> assign(eq_defs, unfold). % set(auto) -> set(auto_limits). % set(auto_limits) -> assign(max_weight, 100). % set(auto_limits) -> assign(sos_limit, 10000). assign(max_weight,50). assign(sos_limit,15000). assign(pick_given_ratio,4). % assign(pick_given_ratio, 4) -> assign(age_part, 1). % assign(pick_given_ratio, 4) -> assign(true_part, 4). % assign(pick_given_ratio, 4) -> assign(false_part, 0). clear(print_given). terms(weights). weight(e(x,x)) = 10. end_of_list. clauses(usable). - P(e(x,y)) | - P(x) | P(y). end_of_list. clauses(sos). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). end_of_list. clauses(assumptions). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. clauses(hints). P(e(x,x)). P(e(e(x,y),e(y,x))). P(e(e(x,y),e(e(y,z),e(x,z)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). P(e(x,e(e(e(x,y),e(z,y)),z))) # label("XCB"). end_of_list. ============================== end of input ========================== Try next SAX candidate: P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). *********************************************** AUTO SKETCHES ITERATION 1 *********************************************** Starting a search with 13 assumptions: clauses(assumptions_active). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27975 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 5 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 6 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 7 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 8 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 9 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 10 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 11 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 12 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 13 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 14 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 15 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 16 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 17 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 34 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 35 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 36 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 37 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 38 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 39 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 40 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 41 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 42 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 43 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 44 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 45 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 46 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 47 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 17 hints processed (0 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds. % Length of proof is 16. % Level of proof is 5. % Maximum clause weight is 31. % Given clauses 37. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 34 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 35 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 36 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 37 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 40 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 44 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 48 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,35,a,b,35,a)]. 80 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,40,a,b,36,a)]. 222 P(e(e(x,e(x,y)),y)). [hyper(1,a,44,a,b,48,a)]. 238 P(e(e(x,y),e(y,x))). [hyper(1,a,48,a,b,37,a)]. 241 - P(e(a,a)) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(34),unit_del(b,238)]. 271 P(e(x,x)). [hyper(1,a,44,a,b,222,a)]. 278 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(241),unit_del(a,271)]. 940 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,40,a,b,80,a)]. 941 $F. [resolve(940,a,278,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=37. Generated=1122. Kept=907. proofs=1. Usable=37. Sos=846. Demods=0. Denials=0. Limbo=21, Disabled=18. Hints=17. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=215. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.53. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ------ process 27975 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27975 exit (max_proofs) Fri Jun 23 23:44:08 2006 Successful proof using the following 5 assumptions: clauses(assumptions_in_proof). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). end_of_list. Including 22 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(y,x))). - P(e(a,a)) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). *********************************************** AUTO SKETCHES ITERATION 2 *********************************************** Starting a search with 12 assumptions: clauses(assumptions_active). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27976 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 5 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 6 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 7 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 8 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 9 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 10 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 11 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 12 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 13 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 14 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 15 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 39 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 55 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 56 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 57 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 58 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 59 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 60 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 61 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 62 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 63 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 64 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 65 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 66 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 67 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 68 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 39 hints processed (10 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 16. % Level of proof is 5. % Maximum clause weight is 0. % Given clauses 17. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 55 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 56 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 57 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 58 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 61 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 65 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 69 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,56,a,b,56,a)]. 101 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,61,a,b,57,a)]. 219 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,61,a,b,101,a)]. 238 - P(e(a,a)) | - P(e(e(a,b),e(b,a))). [back_unit_del(55),unit_del(c,219)]. 244 P(e(e(x,e(x,y)),y)). [hyper(1,a,65,a,b,69,a)]. 261 P(e(e(x,y),e(y,x))). [hyper(1,a,69,a,b,58,a)]. 263 - P(e(a,a)). [back_unit_del(238),unit_del(b,261)]. 268 P(e(x,x)). [hyper(1,a,65,a,b,244,a)]. 269 $F. [resolve(268,a,263,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=17. Generated=237. Kept=214. proofs=1. Usable=17. Sos=191. Demods=0. Denials=0. Limbo=4, Disabled=16. Hints=39. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=23. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.18. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ------ process 27976 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27976 exit (max_proofs) Fri Jun 23 23:44:08 2006 Successful proof using the following 4 assumptions: clauses(assumptions_in_proof). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). end_of_list. Including 22 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). - P(e(a,a)) | - P(e(e(a,b),e(b,a))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(y,x))). - P(e(a,a)). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). *********************************************** AUTO SKETCHES ITERATION 3 *********************************************** Starting a search with 11 assumptions: clauses(assumptions_active). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27977 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 5 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 6 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 7 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 8 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 9 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 10 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 11 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 12 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 13 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 14 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 61 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 76 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 77 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 78 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 79 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 80 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 81 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 82 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 83 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 84 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 85 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 86 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 87 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 88 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 61 hints processed (29 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 16. % Level of proof is 6. % Maximum clause weight is 0. % Given clauses 22. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 76 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 77 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 78 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 81 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 85 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 89 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,77,a,b,77,a)]. 214 P(e(e(x,e(x,y)),y)). [hyper(1,a,85,a,b,89,a)]. 229 P(e(e(x,y),e(y,x))). [hyper(1,a,89,a,b,78,a)]. 231 - P(e(a,a)) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(76),unit_del(b,229)]. 236 P(e(x,x)). [hyper(1,a,85,a,b,214,a)]. 242 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(231),unit_del(a,236)]. 270 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [hyper(1,a,89,a,b,229,a)]. 306 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,81,a,b,270,a)]. 358 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,81,a,b,306,a)]. 359 $F. [resolve(358,a,242,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=367. Kept=283. proofs=1. Usable=22. Sos=249. Demods=0. Denials=0. Limbo=9, Disabled=16. Hints=61. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=84. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.23. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ------ process 27977 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27977 exit (max_proofs) Fri Jun 23 23:44:08 2006 Successful proof using the following 3 assumptions: clauses(assumptions_in_proof). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). end_of_list. Including 23 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(y,x))). - P(e(a,a)) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(z,y)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). *********************************************** AUTO SKETCHES ITERATION 4 *********************************************** Starting a search with 10 assumptions: clauses(assumptions_active). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27978 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 5 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 6 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 7 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 8 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 9 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 10 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 11 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 12 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 13 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 84 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 98 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 99 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 100 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 101 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 102 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 103 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 104 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 105 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 106 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 107 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 108 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 109 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 84 hints processed (51 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 15. % Level of proof is 7. % Maximum clause weight is 0. % Given clauses 20. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 98 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 99 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 100 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 102 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 106 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 110 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,99,a,b,99,a)]. 215 P(e(e(x,e(x,y)),y)). [hyper(1,a,106,a,b,110,a)]. 234 P(e(x,x)). [hyper(1,a,106,a,b,215,a)]. 239 P(e(e(x,y),e(y,x))). [hyper(1,a,100,a,b,215,a)]. 240 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(98),unit_del(a,234),unit_del(b,239)]. 241 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [hyper(1,a,110,a,b,239,a)]. 296 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,102,a,b,241,a)]. 321 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,102,a,b,296,a)]. 322 $F. [resolve(321,a,240,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=20. Generated=293. Kept=224. proofs=1. Usable=20. Sos=193. Demods=0. Denials=0. Limbo=9, Disabled=14. Hints=84. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=69. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=0.21. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ------ process 27978 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27978 exit (max_proofs) Fri Jun 23 23:44:08 2006 Successful proof using the following 3 assumptions: clauses(assumptions_in_proof). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). end_of_list. Including 23 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(x,y),z)) | P(e(y,e(z,x))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(z,y)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). *********************************************** AUTO SKETCHES ITERATION 5 *********************************************** Starting a search with 9 assumptions: clauses(assumptions_active). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27979 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 5 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 6 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 7 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 8 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 9 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 10 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 11 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 12 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 107 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 120 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 121 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 122 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 123 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 124 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 125 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 126 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 127 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 128 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 129 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 130 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 107 hints processed (70 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 16. % Level of proof is 7. % Maximum clause weight is 0. % Given clauses 20. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 120 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 121 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 123 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 127 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 130 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. 131 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,121,a,b,121,a)]. 203 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [hyper(1,a,123,a,b,130,a)]. 238 P(e(e(x,e(x,y)),y)). [hyper(1,a,127,a,b,131,a)]. 252 P(e(e(x,y),e(y,x))). [hyper(1,a,203,a,b,238,a)]. 257 P(e(x,x)). [hyper(1,a,127,a,b,238,a)]. 262 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(120),unit_del(a,257),unit_del(b,252)]. 264 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [hyper(1,a,131,a,b,252,a)]. 322 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,123,a,b,264,a)]. 348 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,123,a,b,322,a)]. 349 $F. [resolve(348,a,262,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=20. Generated=294. Kept=229. proofs=1. Usable=20. Sos=198. Demods=0. Denials=0. Limbo=9, Disabled=13. Hints=107. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=65. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=0.24. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ------ process 27979 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27979 exit (max_proofs) Fri Jun 23 23:44:08 2006 Successful proof using the following 3 assumptions: clauses(assumptions_in_proof). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Including 25 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(e(x,y),z),e(y,e(z,x)))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(e(x,y),z)) | P(e(y,e(z,x))). P(e(e(x,y),e(y,x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(z,y)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). *********************************************** AUTO SKETCHES ITERATION 6 *********************************************** Starting a search with 8 assumptions: clauses(assumptions_active). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27980 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 5 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 6 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 7 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 8 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 9 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 10 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 11 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 132 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 144 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 145 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 146 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 147 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 148 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 149 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 150 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 151 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 152 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 153 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 132 hints processed (94 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.06 (+ 0.00) seconds. % Length of proof is 16. % Level of proof is 7. % Maximum clause weight is 20. % Given clauses 48. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 144 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 145 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 146 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 149 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 150 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 154 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,145,a,b,145,a)]. 157 P(e(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v)),e(v,x))). [hyper(1,a,146,a,b,145,a)]. 225 P(e(e(x,e(x,y)),y)). [hyper(1,a,150,a,b,154,a)]. 241 P(e(x,x)). [hyper(1,a,150,a,b,225,a)]. 246 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(144),unit_del(a,241)]. 253 P(e(e(x,y),e(y,x))). [hyper(1,a,145,a,b,241,a)]. 254 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(246),unit_del(a,253)]. 269 P(e(e(x,y),e(e(y,e(x,z)),z))). [hyper(1,a,253,a,b,149,a)]. 1540 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,157,a,b,269,a)]. 1541 $F. [resolve(1540,a,254,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=48. Generated=1712. Kept=1397. proofs=1. Usable=48. Sos=1326. Demods=0. Denials=0. Limbo=20, Disabled=13. Hints=132. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=315. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.94. User_CPU=0.06, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ------ process 27980 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27980 exit (max_proofs) Fri Jun 23 23:44:08 2006 Successful proof using the following 3 assumptions: clauses(assumptions_in_proof). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). end_of_list. Including 23 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(x) | P(e(e(y,e(x,z)),e(z,y))). P(e(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v)),e(v,x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(y,x)). P(e(e(x,y),e(e(y,e(x,z)),z))). - P(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v))) | P(e(v,x)). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). *********************************************** AUTO SKETCHES ITERATION 7 *********************************************** Starting a search with 7 assumptions: clauses(assumptions_active). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27981 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 5 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 6 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 7 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 8 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 9 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 10 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 155 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 166 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 167 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 168 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 169 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 170 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 171 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 172 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 173 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 174 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 155 hints processed (111 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.60 (+ 0.00) seconds. % Length of proof is 20. % Level of proof is 7. % Maximum clause weight is 20. % Given clauses 105. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 166 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 167 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 170 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 171 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 172 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 173 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 175 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,167,a,b,167,a)]. 198 P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). [hyper(1,a,172,a,b,171,a)]. 231 P(e(e(x,e(x,y)),y)). [hyper(1,a,171,a,b,175,a)]. 262 P(e(x,x)). [hyper(1,a,171,a,b,231,a)]. 267 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(166),unit_del(a,262)]. 274 P(e(e(x,y),e(y,x))). [hyper(1,a,167,a,b,262,a)]. 275 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(267),unit_del(a,274)]. 291 P(e(e(x,y),e(e(y,e(x,z)),z))). [hyper(1,a,274,a,b,170,a)]. 6077 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [hyper(1,a,198,a,b,173,a)]. 6082 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [hyper(1,a,6077,a,b,6077,a)]. 6331 P(e(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v)),e(v,x))). [hyper(1,a,6082,a,b,167,a)]. 6579 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,6331,a,b,291,a)]. 6580 $F. [resolve(6579,a,275,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=105. Generated=8554. Kept=6414. proofs=1. Usable=105. Sos=6205. Demods=0. Denials=0. Limbo=101, Disabled=12. Hints=155. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=2140. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=3.78. User_CPU=0.60, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ------ process 27981 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27981 exit (max_proofs) Fri Jun 23 23:44:09 2006 Successful proof using the following 4 assumptions: clauses(assumptions_in_proof). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). end_of_list. Including 30 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(x) | P(e(e(y,e(z,x)),e(z,y))). P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(y,x)). P(e(e(x,y),e(e(y,e(x,z)),z))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(e(x,y),z),e(y,e(z,x)))). - P(e(e(x,y),z)) | P(e(y,e(z,x))). P(e(x,e(e(y,e(x,z)),e(z,y)))). - P(x) | P(e(e(y,e(x,z)),e(z,y))). P(e(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v)),e(v,x))). - P(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v))) | P(e(v,x)). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). *********************************************** AUTO SKETCHES ITERATION 8 *********************************************** Starting a search with 6 assumptions: clauses(assumptions_active). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27982 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 5 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 6 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 7 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 8 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 9 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 185 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 195 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 196 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 197 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 198 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 199 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 200 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 201 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 202 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 185 hints processed (137 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 21. % Level of proof is 7. % Maximum clause weight is 0. % Given clauses 23. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 195 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 196 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 197 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 199 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 200 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 201 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 203 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,196,a,b,196,a)]. 220 P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). [hyper(1,a,200,a,b,199,a)]. 250 P(e(e(x,e(x,y)),y)). [hyper(1,a,199,a,b,203,a)]. 258 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [hyper(1,a,203,a,b,197,a)]. 264 P(e(x,x)). [hyper(1,a,199,a,b,250,a)]. 269 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(195),unit_del(a,264)]. 292 P(e(e(x,y),e(y,x))). [hyper(1,a,196,a,b,264,a)]. 293 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(269),unit_del(a,292)]. 312 P(e(e(x,y),e(e(y,e(x,z)),z))). [hyper(1,a,292,a,b,258,a)]. 407 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [hyper(1,a,220,a,b,201,a)]. 412 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [hyper(1,a,407,a,b,407,a)]. 499 P(e(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v)),e(v,x))). [hyper(1,a,412,a,b,196,a)]. 518 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,499,a,b,312,a)]. 519 $F. [resolve(518,a,293,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=23. Generated=399. Kept=324. proofs=1. Usable=23. Sos=280. Demods=0. Denials=0. Limbo=18, Disabled=11. Hints=185. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=75. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.37. User_CPU=0.01, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ------ process 27982 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27982 exit (max_proofs) Fri Jun 23 23:44:09 2006 Successful proof using the following 4 assumptions: clauses(assumptions_in_proof). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). end_of_list. Including 32 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(x) | P(e(e(y,e(z,x)),e(z,y))). P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(e(x,e(y,z)),z),e(y,x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(y,x)). P(e(e(x,y),e(e(y,e(x,z)),z))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(e(x,y),z),e(y,e(z,x)))). - P(e(e(x,y),z)) | P(e(y,e(z,x))). P(e(x,e(e(y,e(x,z)),e(z,y)))). - P(x) | P(e(e(y,e(x,z)),e(z,y))). P(e(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v)),e(v,x))). - P(e(x,e(e(e(y,z),e(e(u,z),e(y,u))),v))) | P(e(v,x)). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). *********************************************** AUTO SKETCHES ITERATION 9 *********************************************** Starting a search with 5 assumptions: clauses(assumptions_active). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27983 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 5 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 6 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 7 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 8 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 217 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 226 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 227 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 228 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 229 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 230 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 231 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 232 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 217 hints processed (168 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.08 (+ 0.00) seconds. % Length of proof is 23. % Level of proof is 9. % Maximum clause weight is 12. % Given clauses 53. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 226 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 227 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 228 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 229 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 230 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 231 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 233 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,227,a,b,227,a)]. 243 P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). [hyper(1,a,230,a,b,229,a)]. 268 P(e(e(x,e(x,y)),y)). [hyper(1,a,229,a,b,233,a)]. 280 P(e(x,x)). [hyper(1,a,229,a,b,268,a)]. 284 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(226),unit_del(a,280)]. 289 P(e(e(x,y),e(y,x))). [hyper(1,a,227,a,b,280,a)]. 290 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(284),unit_del(a,289)]. 308 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [hyper(1,a,233,a,b,289,a)]. 313 P(e(e(x,e(y,z)),e(e(z,y),x))). [hyper(1,a,227,a,b,289,a)]. 324 P(e(e(e(x,y),e(y,z)),e(x,z))). [hyper(1,a,289,a,b,308,a)]. 358 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [hyper(1,a,243,a,b,231,a)]. 361 P(e(e(x,e(y,z)),e(e(z,x),y))). [hyper(1,a,243,a,b,228,a)]. 1324 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,358,a,b,324,a)]. 1665 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [hyper(1,a,313,a,b,361,a)]. 1735 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,1665,a,b,1324,a)]. 1736 $F. [resolve(1735,a,290,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=53. Generated=2028. Kept=1510. proofs=1. Usable=53. Sos=1424. Demods=0. Denials=0. Limbo=30, Disabled=10. Hints=217. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=518. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=1.06. User_CPU=0.08, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27983 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27983 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 4 assumptions: clauses(assumptions_in_proof). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). end_of_list. Including 36 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(x) | P(e(e(y,e(z,x)),e(z,y))). P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(z,y)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(y,z)),e(e(z,y),x))). - P(e(x,y)) | P(e(y,x)). P(e(e(e(x,y),e(y,z)),e(x,z))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(e(x,y),z),e(y,e(z,x)))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(x,e(y,z)),e(e(z,x),y))). - P(e(e(x,y),z)) | P(e(y,e(z,x))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(x,e(y,z))) | P(e(e(z,y),x)). P(e(e(x,e(y,z)),e(z,e(x,y)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). *********************************************** AUTO SKETCHES ITERATION 10 *********************************************** Starting a search with 4 assumptions: clauses(assumptions_active). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27984 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 5 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 6 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 7 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 253 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 261 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 262 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 263 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 264 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 265 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 266 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 253 hints processed (199 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 22. % Level of proof is 9. % Maximum clause weight is 0. % Given clauses 23. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 261 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 262 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 263 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 264 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 265 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 267 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,262,a,b,262,a)]. 272 P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). [hyper(1,a,264,a,b,263,a)]. 292 P(e(e(x,e(x,y)),y)). [hyper(1,a,263,a,b,267,a)]. 302 P(e(x,x)). [hyper(1,a,263,a,b,292,a)]. 305 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(261),unit_del(a,302)]. 309 P(e(e(x,y),e(y,x))). [hyper(1,a,262,a,b,302,a)]. 310 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(305),unit_del(a,309)]. 311 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [hyper(1,a,267,a,b,309,a)]. 315 P(e(e(x,e(y,z)),e(e(z,y),x))). [hyper(1,a,262,a,b,309,a)]. 340 P(e(e(e(x,y),e(y,z)),e(x,z))). [hyper(1,a,309,a,b,311,a)]. 424 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [hyper(1,a,272,a,b,265,a)]. 431 P(e(e(x,e(y,z)),e(e(z,x),y))). [hyper(1,a,309,a,b,424,a)]. 439 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,424,a,b,340,a)]. 482 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [hyper(1,a,315,a,b,431,a)]. 582 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,482,a,b,439,a)]. 583 $F. [resolve(582,a,310,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=23. Generated=407. Kept=322. proofs=1. Usable=23. Sos=281. Demods=0. Denials=0. Limbo=15, Disabled=9. Hints=253. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=85. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.40. User_CPU=0.02, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27984 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27984 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 3 assumptions: clauses(assumptions_in_proof). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). end_of_list. Including 35 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(x) | P(e(e(y,e(z,x)),e(z,y))). P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(z,y)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(y,z)),e(e(z,y),x))). - P(e(x,y)) | P(e(y,x)). P(e(e(e(x,y),e(y,z)),e(x,z))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(e(x,y),z),e(y,e(z,x)))). - P(e(x,y)) | P(e(y,x)). P(e(e(x,e(y,z)),e(e(z,x),y))). - P(e(e(x,y),z)) | P(e(y,e(z,x))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(x,e(y,z))) | P(e(e(z,y),x)). P(e(e(x,e(y,z)),e(z,e(x,y)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). *********************************************** AUTO SKETCHES ITERATION 11 *********************************************** Starting a search with 3 assumptions: clauses(assumptions_active). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27985 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 5 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 6 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 288 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 295 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 296 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 297 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 298 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 299 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 288 hints processed (233 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds. % Length of proof is 15. % Level of proof is 8. % Maximum clause weight is 12. % Given clauses 37. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 295 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 296 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 297 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 300 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,296,a,b,296,a)]. 323 P(e(e(x,e(x,y)),y)). [hyper(1,a,300,a,b,297,a)]. 331 P(e(x,x)). [hyper(1,a,323,a,b,296,a)]. 332 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(295),unit_del(a,331)]. 336 P(e(e(x,y),e(y,x))). [hyper(1,a,296,a,b,331,a)]. 337 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(332),unit_del(a,336)]. 342 P(e(e(x,e(y,z)),e(e(z,y),x))). [hyper(1,a,296,a,b,336,a)]. 379 P(e(e(x,e(y,z)),e(x,e(z,y)))). [hyper(1,a,342,a,b,342,a)]. 382 P(e(e(x,y),e(e(x,z),e(y,z)))). [hyper(1,a,300,a,b,342,a)]. 935 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,379,a,b,382,a)]. 936 $F. [resolve(935,a,337,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=37. Generated=960. Kept=641. proofs=1. Usable=37. Sos=595. Demods=0. Denials=0. Limbo=6, Disabled=8. Hints=288. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=319. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.60. User_CPU=0.03, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27985 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27985 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 1 assumptions: clauses(assumptions_in_proof). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). end_of_list. Including 23 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,e(x,y)),y)). - P(e(x,e(x,y))) | P(y). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(y,z)),e(e(z,y),x))). - P(e(x,e(y,z))) | P(e(e(z,y),x)). P(e(e(x,e(y,z)),e(x,e(z,y)))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(y,z)))). - P(e(x,e(y,z))) | P(e(x,e(z,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). *********************************************** AUTO SKETCHES ITERATION 12 *********************************************** Starting a search with 2 assumptions: clauses(assumptions_active). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27986 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 5 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 311 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 317 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 318 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 319 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 320 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 311 hints processed (251 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 15. % Level of proof is 8. % Maximum clause weight is 8. % Given clauses 19. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 317 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 318 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 319 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 321 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,318,a,b,318,a)]. 335 P(e(e(e(x,y),y),x)). [hyper(1,a,321,a,b,319,a)]. 351 P(e(x,x)). [hyper(1,a,335,a,b,335,a)]. 357 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(317),unit_del(a,351)]. 361 P(e(e(x,y),e(y,x))). [hyper(1,a,318,a,b,351,a)]. 362 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(357),unit_del(a,361)]. 367 P(e(e(x,e(y,z)),e(e(z,y),x))). [hyper(1,a,318,a,b,361,a)]. 401 P(e(e(x,e(y,z)),e(x,e(z,y)))). [hyper(1,a,367,a,b,367,a)]. 405 P(e(e(x,y),e(e(x,z),e(y,z)))). [hyper(1,a,321,a,b,367,a)]. 480 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,401,a,b,405,a)]. 481 $F. [resolve(480,a,362,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=19. Generated=237. Kept=164. proofs=1. Usable=19. Sos=141. Demods=0. Denials=0. Limbo=1, Disabled=7. Hints=311. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=73. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.34. User_CPU=0.01, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27986 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27986 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 1 assumptions: clauses(assumptions_in_proof). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). end_of_list. Including 23 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(e(x,y),y),x)). - P(e(e(x,y),y)) | P(x). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(y,z)),e(e(z,y),x))). - P(e(x,e(y,z))) | P(e(e(z,y),x)). P(e(e(x,e(y,z)),e(x,e(z,y)))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(y,z)))). - P(e(x,e(y,z))) | P(e(x,e(z,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). *********************************************** AUTO SKETCHES ITERATION 13 *********************************************** Starting a search with 1 assumptions: clauses(assumptions_active). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27987 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 4 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 334 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 339 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 340 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 341 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 334 hints processed (271 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 18. % Level of proof is 9. % Maximum clause weight is 16. % Given clauses 20. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 339 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 340 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 341 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. 342 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,340,a,b,340,a)]. 344 P(e(e(x,e(e(y,z),e(e(z,u),y))),e(u,x))). [hyper(1,a,340,a,b,341,a)]. 350 P(e(e(x,y),e(x,y))). [hyper(1,a,342,a,b,340,a)]. 364 P(e(e(x,e(y,z)),e(e(y,z),x))). [hyper(1,a,340,a,b,350,a)]. 378 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [hyper(1,a,342,a,b,364,a)]. 411 P(e(x,x)). [hyper(1,a,344,a,b,341,a)]. 413 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(339),unit_del(a,411)]. 414 P(e(e(x,y),e(y,x))). [hyper(1,a,378,a,b,411,a)]. 417 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(413),unit_del(a,414)]. 422 P(e(e(x,e(y,z)),e(e(z,y),x))). [hyper(1,a,340,a,b,414,a)]. 463 P(e(e(x,e(y,z)),e(x,e(z,y)))). [hyper(1,a,422,a,b,422,a)]. 469 P(e(e(x,y),e(e(x,z),e(y,z)))). [hyper(1,a,342,a,b,422,a)]. 497 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,463,a,b,469,a)]. 498 $F. [resolve(497,a,417,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=20. Generated=253. Kept=159. proofs=1. Usable=18. Sos=127. Demods=0. Denials=0. Limbo=1, Disabled=16. Hints=334. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=94. Back_subsumed=11. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.35. User_CPU=0.01, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27987 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27987 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 1 assumptions: clauses(assumptions_in_proof). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Including 29 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(e(z,u),y))),e(u,x))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(x,y))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(y,z)),e(e(y,z),x))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(z,y)))). - P(e(x,e(e(y,z),e(e(z,u),y)))) | P(e(u,x)). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(x,z),e(z,y))). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(y,z)),e(e(z,y),x))). - P(e(x,e(y,z))) | P(e(e(z,y),x)). P(e(e(x,e(y,z)),e(x,e(z,y)))). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(e(x,z),e(y,z)))). - P(e(x,e(y,z))) | P(e(x,e(z,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). *********************************************** AUTO SKETCHES ITERATION 14 *********************************************** Starting a search with 0 assumptions: clauses(assumptions_active). end_of_list. Note: Attempt with no assumptions! Child search process 27988 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. end_of_list. clauses(demodulators). end_of_list. % 363 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 367 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 368 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 363 hints processed (292 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 17. % Level of proof is 11. % Maximum clause weight is 0. % Given clauses 18. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 367 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 368 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 369 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,368,a,b,368,a)]. 372 P(e(e(x,y),e(x,y))). [hyper(1,a,369,a,b,368,a)]. 373 P(e(e(x,e(y,z)),e(e(y,z),x))). [hyper(1,a,368,a,b,372,a)]. 375 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [hyper(1,a,369,a,b,373,a)]. 388 P(e(e(e(x,y),e(y,z)),e(x,z))). [hyper(1,a,373,a,b,375,a)]. 401 P(e(x,x)). [hyper(1,a,388,a,b,373,a)]. 403 - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(367),unit_del(a,401)]. 404 P(e(e(x,y),e(y,x))). [hyper(1,a,375,a,b,401,a)]. 406 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(403),unit_del(a,404)]. 409 P(e(e(x,e(y,z)),e(e(z,y),x))). [hyper(1,a,368,a,b,404,a)]. 448 P(e(e(x,e(y,z)),e(x,e(z,y)))). [hyper(1,a,409,a,b,409,a)]. 454 P(e(e(x,y),e(e(x,z),e(y,z)))). [hyper(1,a,369,a,b,409,a)]. 487 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,448,a,b,454,a)]. 488 $F. [resolve(487,a,406,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=18. Generated=212. Kept=121. proofs=1. Usable=16. Sos=95. Demods=0. Denials=0. Limbo=1, Disabled=11. Hints=363. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=91. Back_subsumed=7. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.34. User_CPU=0.01, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27988 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27988 exit (max_proofs) Fri Jun 23 23:44:10 2006 Proof is complete (no extra assumptions used). Autosketches completes after 14 iterations. SAX FOUND: P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). Try next SAX candidate: P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). *********************************************** AUTO SKETCHES ITERATION 1 *********************************************** Starting a search with 13 assumptions: clauses(assumptions_active). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27989 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 4 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 5 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 6 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 7 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 8 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 9 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 10 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 11 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 12 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 13 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 14 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 15 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 16 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 363 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 380 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 381 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 382 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 383 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 384 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 385 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 386 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 387 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 388 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 389 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 390 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 391 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 392 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 393 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 363 hints processed (292 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 16. % Level of proof is 5. % Maximum clause weight is 0. % Given clauses 22. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 380 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 381 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 382 P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). [input]. 386 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 390 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 395 P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). [hyper(1,a,382,a,b,382,a)]. 426 P(e(e(x,y),e(e(x,z),e(y,z)))). [hyper(1,a,386,a,b,382,a)]. 427 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,386,a,b,381,a)]. 597 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,386,a,b,427,a)]. 618 - P(e(a,a)) | - P(e(e(a,b),e(b,a))). [back_unit_del(380),unit_del(c,597)]. 691 P(e(e(x,e(x,y)),y)). [hyper(1,a,390,a,b,395,a)]. 701 P(e(e(x,y),e(y,x))). [hyper(1,a,395,a,b,426,a)]. 712 - P(e(a,a)). [back_unit_del(618),unit_del(b,701)]. 751 P(e(x,x)). [hyper(1,a,390,a,b,691,a)]. 752 $F. [resolve(751,a,712,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=413. Kept=372. proofs=1. Usable=22. Sos=341. Demods=0. Denials=0. Limbo=7, Disabled=17. Hints=363. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=41. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.49. User_CPU=0.02, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27989 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27989 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 4 assumptions: clauses(assumptions_in_proof). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). end_of_list. Including 23 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). - P(e(x,y)) | P(e(e(z,y),e(x,z))). P(e(e(x,e(e(y,z),e(u,y))),e(e(u,z),x))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(x,z),e(y,z)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). - P(e(a,a)) | - P(e(e(a,b),e(b,a))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,e(x,y)),y)). - P(e(x,e(e(y,z),e(u,y)))) | P(e(e(u,z),x)). P(e(e(x,y),e(y,x))). - P(e(a,a)). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(x,x)). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,y),e(e(z,y),e(x,z)))) # label("YQL"). *********************************************** AUTO SKETCHES ITERATION 2 *********************************************** Starting a search with 12 assumptions: clauses(assumptions_active). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27990 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 4 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 5 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 6 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 7 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 8 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 9 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 10 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 11 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 12 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 13 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 14 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 15 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 386 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 402 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 403 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 404 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 405 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 406 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 407 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 408 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 409 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 410 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 411 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 412 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 413 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 414 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 386 hints processed (314 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 17. % Level of proof is 5. % Maximum clause weight is 0. % Given clauses 22. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 402 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 403 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 405 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 407 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 409 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 411 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 412 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 437 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,407,a,b,403,a)]. 488 P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). [hyper(1,a,412,a,b,411,a)]. 542 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,407,a,b,437,a)]. 559 - P(e(a,a)) | - P(e(e(a,b),e(b,a))). [back_unit_del(402),unit_del(c,542)]. 662 P(e(e(x,e(y,z)),e(e(z,x),y))). [hyper(1,a,488,a,b,409,a)]. 683 P(e(e(e(x,y),e(y,z)),e(x,z))). [hyper(1,a,662,a,b,437,a)]. 747 P(e(x,x)). [hyper(1,a,683,a,b,662,a)]. 751 P(e(e(x,y),e(y,x))). [hyper(1,a,683,a,b,405,a)]. 754 $F. [back_unit_del(559),unit_del(a,747),unit_del(b,751)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=394. Kept=352. proofs=1. Usable=21. Sos=323. Demods=0. Denials=0. Limbo=7, Disabled=16. Hints=386. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=41. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.50. User_CPU=0.02, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27990 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27990 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 6 assumptions: clauses(assumptions_in_proof). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). end_of_list. Including 25 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(x) | P(e(e(y,e(z,x)),e(z,y))). P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). - P(e(a,a)) | - P(e(e(a,b),e(b,a))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(x,e(y,z)),e(e(z,x),y))). - P(e(x,e(y,z))) | P(e(e(z,x),y)). P(e(e(e(x,y),e(y,z)),e(x,z))). - P(e(e(x,y),e(y,z))) | P(e(x,z)). P(e(x,x)). - P(e(e(x,y),e(y,z))) | P(e(x,z)). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(b,a))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). *********************************************** AUTO SKETCHES ITERATION 3 *********************************************** Starting a search with 11 assumptions: clauses(assumptions_active). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27991 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 4 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 5 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 6 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 7 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 8 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 9 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 10 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 11 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 12 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 13 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 14 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 411 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 426 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 427 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 428 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 429 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 430 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 431 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 432 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 433 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 434 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 435 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 436 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 437 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 438 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 411 hints processed (335 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 17. % Level of proof is 5. % Maximum clause weight is 0. % Given clauses 22. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 426 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 427 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 429 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [input]. 431 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 433 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 435 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 436 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 461 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,431,a,b,427,a)]. 512 P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). [hyper(1,a,436,a,b,435,a)]. 566 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,431,a,b,461,a)]. 583 - P(e(a,a)) | - P(e(e(a,b),e(b,a))). [back_unit_del(426),unit_del(c,566)]. 686 P(e(e(x,e(y,z)),e(e(z,x),y))). [hyper(1,a,512,a,b,433,a)]. 707 P(e(e(e(x,y),e(y,z)),e(x,z))). [hyper(1,a,686,a,b,461,a)]. 771 P(e(x,x)). [hyper(1,a,707,a,b,686,a)]. 775 P(e(e(x,y),e(y,x))). [hyper(1,a,707,a,b,429,a)]. 778 $F. [back_unit_del(583),unit_del(a,771),unit_del(b,775)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=393. Kept=352. proofs=1. Usable=21. Sos=323. Demods=0. Denials=0. Limbo=7, Disabled=15. Hints=411. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=40. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.51. User_CPU=0.02, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27991 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27991 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 5 assumptions: clauses(assumptions_in_proof). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). end_of_list. Including 25 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(x) | P(e(e(y,e(z,x)),e(z,y))). P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). - P(e(a,a)) | - P(e(e(a,b),e(b,a))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(x,e(y,z)),e(e(z,x),y))). - P(e(x,e(y,z))) | P(e(e(z,x),y)). P(e(e(e(x,y),e(y,z)),e(x,z))). - P(e(e(x,y),e(y,z))) | P(e(x,z)). P(e(x,x)). - P(e(e(x,y),e(y,z))) | P(e(x,z)). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(b,a))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). *********************************************** AUTO SKETCHES ITERATION 4 *********************************************** Starting a search with 10 assumptions: clauses(assumptions_active). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27992 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 4 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 5 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 6 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 7 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 8 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 9 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 10 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 11 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 12 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 13 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 436 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 450 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 451 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 452 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 453 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 454 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 455 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 456 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 457 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 458 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 459 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 460 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 461 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 436 hints processed (359 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 18. % Level of proof is 5. % Maximum clause weight is 0. % Given clauses 22. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 450 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 451 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 454 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [input]. 456 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 458 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 459 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 461 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. 476 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,454,a,b,451,a)]. 520 P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). [hyper(1,a,459,a,b,458,a)]. 550 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [hyper(1,a,454,a,b,461,a)]. 570 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,454,a,b,476,a)]. 585 - P(e(a,a)) | - P(e(e(a,b),e(b,a))). [back_unit_del(450),unit_del(c,570)]. 710 P(e(e(x,e(y,z)),e(e(z,x),y))). [hyper(1,a,520,a,b,456,a)]. 732 P(e(e(e(x,y),e(y,z)),e(x,z))). [hyper(1,a,710,a,b,476,a)]. 795 P(e(x,x)). [hyper(1,a,732,a,b,710,a)]. 796 P(e(e(x,y),e(y,x))). [hyper(1,a,732,a,b,550,a)]. 802 $F. [back_unit_del(585),unit_del(a,795),unit_del(b,796)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=392. Kept=352. proofs=1. Usable=21. Sos=323. Demods=0. Denials=0. Limbo=7, Disabled=14. Hints=436. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=39. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=2. 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=2. Megabytes=0.53. User_CPU=0.02, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27992 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27992 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 5 assumptions: clauses(assumptions_in_proof). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Including 27 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(x) | P(e(e(y,e(z,x)),e(z,y))). P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(e(x,y),z),e(y,e(z,x)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). - P(e(a,a)) | - P(e(e(a,b),e(b,a))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(x,e(y,z)),e(e(z,x),y))). - P(e(x,e(y,z))) | P(e(e(z,x),y)). P(e(e(e(x,y),e(y,z)),e(x,z))). - P(e(e(x,y),e(y,z))) | P(e(x,z)). P(e(x,x)). - P(e(e(x,y),e(y,z))) | P(e(x,z)). P(e(e(x,y),e(y,x))). - P(e(e(a,b),e(b,a))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). *********************************************** AUTO SKETCHES ITERATION 5 *********************************************** Starting a search with 9 assumptions: clauses(assumptions_active). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Child search process 27993 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 2 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 3 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 4 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 5 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 6 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 7 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 8 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 9 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 10 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 11 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 12 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. % 463 hints input. Term ordering decisions: Relation symbol precedence: lex([ P ]). Function symbol precedence: lex([ a, b, c, e ]). After inverse_order: Function symbol precedence: lex([ a, b, c, e ]). Unfolding symbols: (none). Auto inference settings: % set(hyper_resolution). % (HNE depth_diff=1) Reasonable options, based on the structure of the clauses: % set(back_unit_deletion), because Horn and neg nonunits. % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). 1 - P(e(x,y)) | - P(x) | P(y). [input]. end_of_list. clauses(sos). 476 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 477 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 478 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 479 P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). [input]. 480 P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). [input]. 481 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 482 P(e(e(e(x,e(y,z)),z),e(y,x))) # label("PYO"). [input]. 483 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 484 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 485 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 486 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. % 463 hints processed (385 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds. % Length of proof is 23. % Level of proof is 7. % Maximum clause weight is 16. % Given clauses 35. 1 - P(e(x,y)) | - P(x) | P(y). [input]. 476 - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). [input]. 477 P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). [input]. 478 P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). [input]. 481 P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). [input]. 483 P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). [input]. 484 P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). [input]. 485 P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). [input]. 486 P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). [input]. 487 P(e(e(e(x,y),z),e(z,e(e(x,u),e(u,y))))). [hyper(1,a,477,a,b,477,a)]. 532 P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). [hyper(1,a,484,a,b,483,a)]. 580 P(e(e(e(x,y),e(y,e(z,x))),z)). [hyper(1,a,532,a,b,486,a)]. 581 P(e(e(e(x,y),z),e(y,e(z,x)))) # label("UM"). [hyper(1,a,532,a,b,485,a)]. 585 P(e(e(x,e(y,z)),e(e(z,x),y))). [hyper(1,a,532,a,b,481,a)]. 780 P(e(e(x,y),e(y,x))). [hyper(1,a,483,a,b,580,a)]. 787 P(e(x,x)). [hyper(1,a,580,a,b,487,a)]. 790 - P(e(e(a,b),e(e(b,c),e(a,c)))). [back_unit_del(476),unit_del(a,787),unit_del(b,780)]. 841 P(e(e(x,e(y,z)),e(e(z,y),x))). [hyper(1,a,478,a,b,780,a)]. 857 P(e(e(e(x,y),e(y,z)),e(x,z))). [hyper(1,a,780,a,b,477,a)]. 960 P(e(e(x,e(y,z)),e(z,e(x,y)))) # label("WN"). [hyper(1,a,841,a,b,585,a)]. 1019 P(e(e(x,y),e(e(z,y),e(z,x)))). [hyper(1,a,581,a,b,857,a)]. 1198 P(e(e(x,y),e(e(y,z),e(x,z)))). [hyper(1,a,960,a,b,1019,a)]. 1199 $F. [resolve(1198,a,790,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=35. Generated=932. Kept=723. proofs=1. Usable=35. Sos=685. Demods=0. Denials=0. Limbo=1, Disabled=13. Hints=463. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=209. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=0.75. User_CPU=0.03, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ------ process 27993 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 27993 exit (max_proofs) Fri Jun 23 23:44:10 2006 Successful proof using the following 6 assumptions: clauses(assumptions_in_proof). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). end_of_list. Including 36 new hint clauses: clauses(new_hints). - P(e(x,y)) | - P(x) | P(y). - P(e(a,a)) | - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). P(e(e(x,y),e(e(x,z),e(z,y)))) # label("YQF"). P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),y),e(z,x))) # label("PYM"). P(e(x,e(e(y,e(z,x)),e(z,y)))) # label("XGK"). P(e(x,e(e(y,z),e(e(x,z),y)))) # label("XHK"). P(e(x,e(e(y,z),e(e(z,x),y)))) # label("XHN"). - P(e(x,y)) | P(e(e(x,z),e(z,y))). P(e(e(e(x,y),z),e(z,e(e(x,u),e(u,y))))). - P(x) | P(e(e(y,e(z,x)),e(z,y))). P(e(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z)))),e(y,x))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(e(x,y),e(y,e(z,x))),z)). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(e(x,y),z),e(y,e(z,x)))). - P(e(x,e(y,e(e(e(z,e(u,v)),u),e(v,z))))) | P(e(y,x)). P(e(e(x,e(y,z)),e(e(z,x),y))). - P(e(e(x,e(y,z)),y)) | P(e(z,x)). P(e(e(x,y),e(y,x))). - P(e(e(x,y),e(y,e(z,x)))) | P(z). P(e(x,x)). - P(e(e(a,b),e(b,a))) | - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(e(a,b),e(e(b,c),e(a,c)))). - P(e(x,y)) | P(e(e(z,x),e(y,z))). P(e(e(x,e(y,z)),e(e(z,y),x))). - P(e(x,y)) | P(e(y,x)). P(e(e(e(x,y),e(y,z)),e(x,z))). - P(e(x,e(y,z))) | P(e(e(z,y),x)). P(e(e(x,e(y,z)),e(z,e(x,y)))). - P(e(e(x,y),z)) | P(e(y,e(z,x))). P(e(e(x,y),e(e(z,y),e(z,x)))). - P(e(x,e(y,z))) | P(e(z,e(x,y))). P(e(e(x,y),e(e(y,z),e(x,z)))). $F. end_of_list. Attempt to eliminate one assumption: P(e(e(x,y),e(e(z,x),e(y,z)))) # label("YQJ"). *********************************************** AUTO SKETCHES ITERATION 6 *********************************************** Starting a search with 8 assumptions: clauses(assumptions_active). P(e(x,e(e(y,e(x,z)),e(z,y)))) # label("XGF"). P(e(e(x,y),e(z,e(e(y,z),x)))) # label("YRM"). P(e(e(x,y),e(z,e(e(z,y),x)))) # label("YRO"). P(e(e(e(x,e(y,z)),z),e(y,