============================== NewAuto =============================== NewAuto (32) version June-2006A, June 2006. Process 19148 was started by veroff on lunar, Sat Jun 24 06:23:23 2006 The command was "/nfs/faculty/veroff/PROVER/LADR/prover9.src/newauto -f BA.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file BA.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(order,kbo). set(lex_order_vars). assign(lex_dep_demod_lim,0). assign(max_megs,750). assign(sos_limit,20000). assign(demod_step_limit,200). assign(demod_size_limit,100000). clear(print_kept). clear(print_given). clauses(sos). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). end_of_list. clauses(goals). f(x,y) = f(y,x) # label("Commutativity"). end_of_list. clauses(assumptions). f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). f(c2,c1) != f(c1,c2) # label("Commutativity"). end_of_list. ============================== end of process goals ================== *********************************************** AUTO SKETCHES ITERATION 1 *********************************************** Starting a search with 17 assumptions: clauses(assumptions_active). f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Child search process 19149 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 2 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 3 f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). [input]. 4 f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). [input]. 5 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 6 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 7 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 8 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 9 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 10 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 11 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 12 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 13 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 14 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 15 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 16 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 17 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 18 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 19 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Term ordering decisions: Function symbol KB weights: c1=1. c2=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Reasonable options, based on the structure of the clauses: (nothing changed) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 20 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 21 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 22 f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). [input]. 23 f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). [input]. 24 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 25 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 26 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 27 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 28 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 29 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 30 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 31 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 32 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 33 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 34 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 35 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 36 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 37 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 38 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). 20 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 22 f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). [input]. 23 f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). [input]. 24 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 25 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 26 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 27 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 28 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 29 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 30 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 31 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 32 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 33 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 34 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 35 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 36 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 37 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 38 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- % Operation f is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 1.02 (+ 0.02) seconds. % Length of proof is 35. % Level of proof is 12. % Maximum clause weight is 37. % Given clauses 52. 20 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 21 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 23 f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). [input]. 24 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 27 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 28 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 30 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 31 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 32 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 33 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 36 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 39 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(20(a,1),20(a,1,1,2,1))]. 41 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(20(a,1),20(a,1,2))]. 51 f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. [para(23(a,1),20(a,1,1,2))]. 947 f(f(f(x,f(x,x)),x),f(x,x)) = x. [para(20(a,1),51(a,1,2,2))]. 1092 f(x,f(x,f(x,x))) = f(x,x). [para(23(a,1),947(a,1,1,1,2)),demod(36(8),23(7)),flip(a)]. 1138 f(f(x,x),f(x,f(x,y))) = x. [para(1092(a,1),23(a,1,1))]. 1139 f(f(x,x),f(x,x)) = x. [para(1092(a,1),23(a,1,2)),demod(1092(3))]. 1141 f(f(x,x),f(x,f(y,x))) = x. [para(1092(a,1),24(a,1,1))]. 1143 f(f(f(x,x),x),f(x,x)) = x. [para(1092(a,1),24(a,1,2)),demod(1138(5))]. 1148 f(f(x,f(x,x)),x) = f(x,x). [para(1092(a,1),27(a,1,1,2)),demod(1139(5))]. 1152 f(f(x,f(f(x,x),x)),f(x,x)) = x. [para(1092(a,1),28(a,1,2))]. 1157 f(f(x,f(x,x)),f(x,x)) = x. [para(1092(a,1),30(a,1,2)),demod(1143(4))]. 1178 f(x,f(f(x,x),x)) = f(x,x). [para(1092(a,1),39(a,1,2,2)),demod(1092(5),1157(4),1152(5)),flip(a)]. 1224 f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. [para(1139(a,1),33(a,1,1,1))]. 1579 f(f(x,x),f(x,f(y,f(f(x,y),y)))) = x. [para(41(a,1),1141(a,1,2,2))]. 1586 f(f(x,x),x) = f(x,f(x,x)). [para(1157(a,1),20(a,1,2)),demod(1148(3),1178(3))]. 1886 f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(y,f(x,x)). [para(1224(a,1),27(a,1,1,2)),demod(1148(3),1148(6))]. 1895 f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). [para(1224(a,1),31(a,1,1,1)),demod(1138(10))]. 2587 f(f(x,f(y,y)),f(x,y)) = x. [para(1579(a,1),28(a,1,2,2)),demod(1886(6))]. 2633 f(f(x,y),f(x,f(y,y))) = x. [para(20(a,1),2587(a,1,1,2)),demod(1586(3),1092(4))]. 2677 f(f(x,x),y) = f(y,f(x,x)). [para(2587(a,1),32(a,1,2)),demod(1895(5))]. 2820 f(x,f(f(x,x),x)) = f(x,x). [para(1139(a,1),2633(a,1,1)),demod(1139(4))]. 2967 f(x,y) = f(y,x). [para(20(a,1),2677(a,1,1)),demod(2820(4),2820(5),1139(4))]. 2968 $F. [resolve(2967,a,21,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=7039. Kept=2948. proofs=1. Usable=45. Sos=2545. Demods=2592. Denials=0. Limbo=7, Disabled=369. Hints=0. Weight_deleted=129. Literals_deleted=0. Forward_subsumed=3962. Back_subsumed=151. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2942 (0 lex), Back_demodulated=199. Back_unit_deleted=0. Demod_attempts=179986. Demod_rewrites=11794. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=4.66. User_CPU=1.02, System_CPU=0.02, Wall_clock=3. ============================== end of statistics ===================== ------ process 19149 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 19149 exit (max_proofs) Sat Jun 24 06:23:26 2006 Successful proof using the following 9 assumptions: clauses(assumptions_in_proof). f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). end_of_list. Including 59 new hint clauses: clauses(new_hints). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). f(c2,c1) != f(c1,c2) # label("Commutativity"). f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. f(f(f(x,f(x,x)),x),f(x,x)) = x. f(f(f(f(x,f(x,f(x,x))),x),f(x,f(x,f(x,x)))),f(f(x,f(x,f(x,x))),f(x,f(x,f(x,x))))) = f(x,f(x,f(x,x))). f(x,f(f(x,f(x,f(x,x))),f(x,f(x,f(x,x))))) = f(x,f(x,f(x,x))). f(x,x) = f(x,f(x,f(x,x))). f(x,f(x,f(x,x))) = f(x,x). f(f(x,x),f(x,f(x,y))) = x. f(f(x,f(x,f(x,x))),f(x,x)) = x. f(f(x,x),f(x,x)) = x. f(f(x,x),f(x,f(y,x))) = x. f(f(f(x,x),f(f(x,x),f(x,f(x,x)))),f(x,x)) = x. f(f(f(x,x),x),f(x,x)) = x. f(f(x,f(x,x)),f(f(x,x),f(x,x))) = f(x,x). f(f(x,f(x,x)),x) = f(x,x). f(f(x,f(f(x,x),x)),f(x,x)) = x. f(f(f(f(f(x,x),x),f(x,x)),f(x,x)),f(x,x)) = x. f(f(x,f(x,x)),f(x,x)) = x. f(f(f(x,f(x,x)),f(x,f(x,f(x,x)))),f(f(x,f(f(x,x),x)),f(x,x))) = f(x,f(f(x,x),x)). f(f(f(x,f(x,x)),f(x,x)),f(f(x,f(f(x,x),x)),f(x,x))) = f(x,f(f(x,x),x)). f(x,f(f(x,f(f(x,x),x)),f(x,x))) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(f(x,x),x)). f(x,f(f(x,x),x)) = f(x,x). f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. f(f(x,x),f(x,f(y,f(f(x,y),y)))) = x. f(f(x,f(f(f(x,f(x,x)),x),x)),x) = f(x,f(x,x)). f(f(x,f(f(x,x),x)),x) = f(x,f(x,x)). f(f(x,x),x) = f(x,f(x,x)). f(f(f(x,f(x,x)),x),f(f(y,f(x,x)),f(f(x,f(x,x)),x))) = f(y,f(x,x)). f(f(x,x),f(f(y,f(x,x)),f(f(x,f(x,x)),x))) = f(y,f(x,x)). f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(y,f(x,x)). f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,f(x,f(y,f(x,x)))))) = f(x,x). f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(x,f(y,y)),f(x,y)) = x. f(f(x,y),f(x,f(y,f(f(y,y),y)))) = x. f(f(x,y),f(x,f(y,f(y,f(y,y))))) = x. f(f(x,y),f(x,f(y,y))) = x. f(f(f(x,f(x,f(y,f(x,x)))),x),y) = f(y,f(x,x)). f(f(x,x),y) = f(y,f(x,x)). f(x,f(f(x,x),f(f(x,x),f(x,x)))) = f(x,x). f(x,f(f(x,x),x)) = f(x,x). f(x,y) = f(y,f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))). f(x,y) = f(y,f(f(x,x),f(x,f(f(x,x),x)))). f(x,y) = f(y,f(f(x,x),f(x,x))). f(x,y) = f(y,x). $F. end_of_list. Attempt to eliminate one assumption: f(f(x,f(x,f(x,y))),f(y,f(x,z))) = y # label("C1/A1"). *********************************************** AUTO SKETCHES ITERATION 2 *********************************************** Starting a search with 16 assumptions: clauses(assumptions_active). f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Child search process 19150 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 2 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 3 f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). [input]. 4 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 5 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 6 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 7 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 8 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 9 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 10 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 11 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 12 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 13 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 14 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 15 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 16 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 17 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 18 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). end_of_list. % 59 hints input. Predicate elimination: (none). Term ordering decisions: Function symbol KB weights: c1=1. c2=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Reasonable options, based on the structure of the clauses: (nothing changed) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 78 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 79 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 80 f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). [input]. 81 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 82 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 83 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 84 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 85 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 86 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 87 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 88 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 89 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 90 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 91 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 92 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 93 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 94 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 95 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). 78 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 80 f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). [input]. 81 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 82 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 83 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 84 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 85 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 86 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 87 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 88 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 89 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 90 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 91 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 92 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 93 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 94 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 95 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(denials). end_of_list. % 59 hints processed (3 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- % Operation f is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 0.94 (+ 0.01) seconds. % Length of proof is 44. % Level of proof is 12. % Maximum clause weight is 81. % Given clauses 45. 78 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 79 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 80 f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). [input]. 81 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 84 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 85 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 88 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 89 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 90 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 95 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. 96 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(78(a,1),78(a,1,1,2,1))]. 98 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(78(a,1),78(a,1,2))]. 99 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(f(z,f(x,z)),z),f(u,f(x,f(y,z))))) = f(f(z,f(x,z)),z). [para(80(a,1),78(a,1,1,2,1))]. 108 f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. [para(81(a,1),78(a,1,1,2))]. 913 f(f(f(x,f(x,x)),x),f(x,x)) = x. [para(78(a,1),108(a,1,2,2))]. 953 f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. [para(913(a,1),78(a,1,2,2))]. 1024 f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). [para(85(a,1),96(a,1,2))]. 1084 f(f(f(x,y),f(f(z,f(x,y)),f(x,y))),f(z,x)) = z. [para(953(a,1),78(a,1,2,2))]. 1094 f(f(f(x,y),f(f(x,y),f(z,f(x,y)))),f(z,x)) = z. [para(953(a,1),81(a,1,2,2))]. 1555 f(f(x,f(x,x)),x) = f(x,f(f(x,x),x)). [para(95(a,1),99(a,1,2)),demod(1024(7)),flip(a)]. 1561 f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,f(f(x,x),x)),f(x,x))),f(x,x)). [para(913(a,1),99(a,1,2,1,1,2)),demod(1555(3),1555(9),1555(12),1555(24),1555(34))]. 1653 f(f(x,f(f(x,x),x)),f(x,x)) = x. [back_demod(913),demod(1555(3))]. 1658 f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),x),f(x,x)). [back_demod(1561),demod(1653(36))]. 1660 f(x,f(f(x,x),x)) = f(x,x). [para(78(a,1),1653(a,1,1,2,1)),demod(85(8),78(7)),flip(a)]. 1663 f(f(f(x,x),x),x) = f(x,x). [para(1653(a,1),80(a,1,2)),demod(1660(3),1660(3),1660(6))]. 1669 f(f(f(x,x),x),f(x,x)) = x. [para(1653(a,1),84(a,1,1,2)),demod(1660(3),1660(5),1660(5))]. 1677 f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. [para(1653(a,1),90(a,1,1,1)),demod(1660(3),1660(5))]. 1709 f(f(f(x,x),f(f(x,x),x)),f(f(x,x),x)) = f(x,x). [para(1653(a,1),1094(a,1,1,2,2)),demod(1660(7),1660(10))]. 1715 f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(x,f(z,f(f(x,x),f(y,f(x,x)))))) = f(f(x,x),f(x,x)). [para(1653(a,1),99(a,1,2,1,1,2)),demod(1660(3),1660(7),1660(8),1669(15),1660(14),1660(22),1555(25),1660(25))]. 1720 f(f(x,x),f(x,x)) = x. [back_demod(1658),demod(1660(3),1660(7),1660(8),1669(15),1660(14),1715(18),1669(7))]. 1765 f(f(x,f(x,x)),x) = f(x,x). [back_demod(1555),demod(1660(6))]. 1776 f(f(x,x),f(x,f(y,x))) = x. [para(1660(a,1),78(a,1,1))]. 1783 f(f(x,x),f(x,f(x,y))) = x. [para(1660(a,1),85(a,1,1))]. 1833 f(f(x,x),x) = f(x,f(x,x)). [para(1669(a,1),1084(a,1,1,2,1)),demod(1783(4),1663(3)),flip(a)]. 1873 f(x,f(x,f(x,x))) = f(x,x). [back_demod(1709),demod(1833(3),1783(4),1833(2))]. 2054 f(f(x,x),f(x,f(y,f(f(x,y),y)))) = x. [para(98(a,1),1776(a,1,2,2))]. 2335 f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(y,f(x,x)). [para(1677(a,1),84(a,1,1,2)),demod(1765(3),1765(6))]. 2343 f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). [para(1677(a,1),88(a,1,1,1)),demod(1783(10))]. 2491 f(f(x,f(y,y)),f(x,y)) = x. [para(2054(a,1),85(a,1,2,2)),demod(2335(6))]. 2543 f(f(x,y),f(x,f(y,y))) = x. [para(78(a,1),2491(a,1,1,2)),demod(1833(3),1873(4))]. 2583 f(f(x,x),y) = f(y,f(x,x)). [para(2491(a,1),89(a,1,2)),demod(2343(5))]. 2734 f(x,f(f(x,x),x)) = f(x,x). [para(1720(a,1),2543(a,1,1)),demod(1720(4))]. 2764 f(x,y) = f(y,x). [para(78(a,1),2583(a,1,1)),demod(2734(4),2734(5),1720(4))]. 2765 $F. [resolve(2764,a,79,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=45. Generated=5918. Kept=2687. proofs=1. Usable=37. Sos=2126. Demods=2166. Denials=0. Limbo=7, Disabled=534. Hints=59. Weight_deleted=135. Literals_deleted=0. Forward_subsumed=3096. Back_subsumed=198. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2682 (0 lex), Back_demodulated=318. Back_unit_deleted=0. Demod_attempts=152530. Demod_rewrites=9595. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.98. User_CPU=0.94, System_CPU=0.01, Wall_clock=6. ============================== end of statistics ===================== ------ process 19150 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 19150 exit (max_proofs) Sat Jun 24 06:23:29 2006 Successful proof using the following 8 assumptions: clauses(assumptions_in_proof). f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Including 94 new hint clauses: clauses(new_hints). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). f(c2,c1) != f(c1,c2) # label("Commutativity"). f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(f(z,f(x,z)),z),f(u,f(x,f(y,z))))) = f(f(z,f(x,z)),z). f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. f(f(f(x,f(x,x)),x),f(x,x)) = x. f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). f(f(f(x,y),f(f(z,f(x,y)),f(x,y))),f(z,x)) = z. f(f(f(x,y),f(f(x,y),f(z,f(x,y)))),f(z,x)) = z. f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(f(x,f(x,x)),x). f(x,f(f(x,x),x)) = f(f(x,f(x,x)),x). f(f(x,f(x,x)),x) = f(x,f(f(x,x),x)). f(f(f(f(f(x,f(x,x)),x),f(y,f(x,x))),f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(f(x,f(x,x)),x),f(y,f(x,x)))))) = f(f(f(x,x),f(f(f(x,f(x,x)),x),f(x,x))),f(x,x)). f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(f(x,f(x,x)),x),f(y,f(x,x)))))) = f(f(f(x,x),f(f(f(x,f(x,x)),x),f(x,x))),f(x,x)). f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(f(x,f(x,x)),x),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(f(x,f(x,x)),x),f(y,f(x,x)))))) = f(f(f(x,x),f(f(f(x,f(x,x)),x),f(x,x))),f(x,x)). f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(f(x,f(x,x)),x),f(y,f(x,x)))))) = f(f(f(x,x),f(f(f(x,f(x,x)),x),f(x,x))),f(x,x)). f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),f(f(f(x,f(x,x)),x),f(x,x))),f(x,x)). f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,f(f(x,x),x)),f(x,x))),f(x,x)). f(f(x,f(f(x,x),x)),f(x,x)) = x. f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),x),f(x,x)). f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))) = f(x,f(f(x,x),x)). f(x,f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(f(x,x),x)). f(x,f(f(x,x),x)) = f(x,x). f(f(f(x,f(f(x,f(f(x,x),x)),x)),x),x) = f(x,f(f(x,x),x)). f(f(f(x,f(f(x,x),x)),x),x) = f(x,f(f(x,x),x)). f(f(f(x,x),x),x) = f(x,f(f(x,x),x)). f(f(f(x,x),x),x) = f(x,x). f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,f(f(x,x),x)),x))) = x. f(f(f(x,x),x),f(x,f(f(x,f(f(x,x),x)),x))) = x. f(f(f(x,x),x),f(x,f(f(x,x),x))) = x. f(f(f(x,x),x),f(x,x)) = x. f(f(x,f(x,f(f(x,x),x))),f(x,f(y,f(x,f(f(x,x),x))))) = x. f(f(x,f(x,x)),f(x,f(y,f(x,f(f(x,x),x))))) = x. f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. f(f(f(x,x),f(f(x,x),x)),f(f(x,f(f(x,x),x)),x)) = f(x,f(f(x,x),x)). f(f(f(x,x),f(f(x,x),x)),f(f(x,x),x)) = f(x,f(f(x,x),x)). f(f(f(x,x),f(f(x,x),x)),f(f(x,x),x)) = f(x,x). f(f(f(f(x,f(f(x,x),x)),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,f(f(x,x),x)),f(x,x))),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,f(f(x,x),x)),f(x,x))),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,f(f(x,x),x)),f(x,x))),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,f(f(x,x),x)),f(x,x))),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(x,f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,f(f(x,x),x)),f(x,x))),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(x,f(z,f(f(x,x),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,f(f(x,x),x)),f(x,x))),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(x,f(z,f(f(x,x),f(y,f(x,x)))))) = f(f(f(x,x),f(f(x,x),f(x,x))),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(x,f(z,f(f(x,x),f(y,f(x,x)))))) = f(f(x,x),f(f(f(x,x),f(x,x)),f(x,x))). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(x,f(z,f(f(x,x),f(y,f(x,x)))))) = f(f(x,x),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),x),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,f(f(x,x),x)),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),x),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(f(f(f(x,x),x),f(x,x)),f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),x),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(x,f(z,f(f(x,f(f(x,x),x)),f(y,f(x,x)))))) = f(f(f(x,x),x),f(x,x)). f(f(f(f(x,x),f(y,f(x,x))),f(f(x,x),f(f(x,x),f(y,f(x,x))))),f(x,f(z,f(f(x,x),f(y,f(x,x)))))) = f(f(f(x,x),x),f(x,x)). f(f(x,x),f(x,x)) = f(f(f(x,x),x),f(x,x)). f(f(x,x),f(x,x)) = x. f(f(x,f(x,x)),x) = f(x,x). f(f(x,x),f(x,f(y,x))) = x. f(f(x,x),f(x,f(x,y))) = x. f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),x). f(x,f(f(f(x,x),x),x)) = f(f(x,x),x). f(x,f(x,x)) = f(f(x,x),x). f(f(x,x),x) = f(x,f(x,x)). f(f(f(x,x),f(x,f(x,x))),f(f(x,x),x)) = f(x,x). f(x,f(f(x,x),x)) = f(x,x). f(x,f(x,f(x,x))) = f(x,x). f(f(x,x),f(x,f(y,f(f(x,y),y)))) = x. f(f(f(x,f(x,x)),x),f(f(y,f(x,x)),f(f(x,f(x,x)),x))) = f(y,f(x,x)). f(f(x,x),f(f(y,f(x,x)),f(f(x,f(x,x)),x))) = f(y,f(x,x)). f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(y,f(x,x)). f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,f(x,f(y,f(x,x)))))) = f(x,x). f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(x,f(y,y)),f(x,y)) = x. f(f(x,y),f(x,f(y,f(f(y,y),y)))) = x. f(f(x,y),f(x,f(y,f(y,f(y,y))))) = x. f(f(x,y),f(x,f(y,y))) = x. f(f(f(x,f(x,f(y,f(x,x)))),x),y) = f(y,f(x,x)). f(f(x,x),y) = f(y,f(x,x)). f(x,f(f(x,x),f(f(x,x),f(x,x)))) = f(x,x). f(x,f(f(x,x),x)) = f(x,x). f(x,y) = f(y,f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))). f(x,y) = f(y,f(f(x,x),f(x,f(f(x,x),x)))). f(x,y) = f(y,f(f(x,x),f(x,x))). f(x,y) = f(y,x). $F. end_of_list. Attempt to eliminate one assumption: f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y # label("Sh2/A14_m"). *********************************************** AUTO SKETCHES ITERATION 3 *********************************************** Starting a search with 15 assumptions: clauses(assumptions_active). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Child search process 19152 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 2 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 3 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 4 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 5 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 6 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 7 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 8 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 9 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 10 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 11 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 12 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 13 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 14 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 15 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 16 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 17 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). end_of_list. % 153 hints input. Predicate elimination: (none). Term ordering decisions: Function symbol KB weights: c1=1. c2=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Reasonable options, based on the structure of the clauses: (nothing changed) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 171 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 172 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 173 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 174 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 175 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 176 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 177 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 178 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 179 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 180 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 181 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 182 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 183 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 184 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 185 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 186 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 187 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). 171 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 173 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 174 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 175 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 176 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 177 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 178 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 179 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 180 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 181 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 182 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 183 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 184 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 185 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 186 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 187 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(denials). end_of_list. % 153 hints processed (49 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- % Operation f is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 0.76 (+ 0.00) seconds. % Length of proof is 38. % Level of proof is 11. % Maximum clause weight is 37. % Given clauses 43. 171 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 172 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 173 f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). [input]. 174 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 175 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 176 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 177 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 179 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 180 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 181 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 183 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 188 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(171(a,1),171(a,1,1,2,1))]. 190 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(171(a,1),171(a,1,2))]. 192 f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. [para(173(a,1),171(a,1,1,2))]. 194 f(f(f(x,f(y,z)),f(f(x,f(y,z)),x)),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(171(a,1),173(a,1,1,2,2))]. 927 f(f(f(x,f(x,x)),x),f(x,x)) = x. [para(171(a,1),192(a,1,2,2))]. 965 f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. [para(927(a,1),171(a,1,2,2))]. 990 f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. [para(927(a,1),183(a,1,1,1))]. 1034 f(f(x,f(x,x)),f(f(f(x,f(x,x)),f(x,x)),f(y,f(x,x)))) = f(f(x,f(x,x)),f(x,x)). [para(965(a,1),179(a,1,1,1))]. 1116 f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). [para(177(a,1),188(a,1,1))]. 1118 f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). [para(177(a,1),188(a,1,2))]. 1392 f(x,f(f(x,x),x)) = f(x,x). [para(177(a,1),1118(a,1,1)),flip(a)]. 1452 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). [back_demod(1116),demod(1392(3),1392(4),1392(8))]. 1457 f(f(x,f(x,x)),f(x,x)) = x. [back_demod(990),demod(1452(7))]. 1459 f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. [back_demod(1034),demod(1457(6),1457(10))]. 1461 f(f(x,x),f(x,f(y,x))) = x. [para(1392(a,1),171(a,1,1))]. 1462 f(f(x,x),f(x,x)) = x. [para(1392(a,1),171(a,1,2)),demod(1392(3))]. 1464 f(f(x,f(x,x)),x) = f(x,x). [para(1392(a,1),175(a,1,1,2)),demod(1462(5))]. 1471 f(f(x,x),f(x,f(x,y))) = x. [para(1392(a,1),177(a,1,1))]. 1727 f(f(x,x),f(x,f(y,f(f(x,y),y)))) = x. [para(190(a,1),1461(a,1,2,2))]. 1866 f(f(f(x,y),f(f(x,y),x)),x) = f(x,x). [para(1471(a,1),174(a,1,2)),demod(1462(5))]. 2096 f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(y,f(x,x)). [para(1459(a,1),176(a,1,1,2)),demod(1464(3),1464(6))]. 2105 f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). [para(1459(a,1),180(a,1,1,1)),demod(1471(10))]. 2234 f(f(x,f(y,y)),f(x,y)) = x. [para(1727(a,1),177(a,1,2,2)),demod(2096(6))]. 2328 f(f(x,x),y) = f(y,f(x,x)). [para(2234(a,1),181(a,1,2)),demod(2105(5))]. 2410 f(x,f(f(x,x),x)) = f(x,x). [para(177(a,1),194(a,1,2)),demod(1866(7)),flip(a)]. 2623 f(x,y) = f(y,x). [para(171(a,1),2328(a,1,1)),demod(2410(4),2410(5),1462(4))]. 2624 $F. [resolve(2623,a,172,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=43. Generated=5183. Kept=2453. proofs=1. Usable=36. Sos=2049. Demods=2089. Denials=0. Limbo=7, Disabled=377. Hints=153. Weight_deleted=107. Literals_deleted=0. Forward_subsumed=2623. Back_subsumed=177. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2449 (0 lex), Back_demodulated=183. Back_unit_deleted=0. Demod_attempts=130206. Demod_rewrites=7832. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=4.00. User_CPU=0.76, System_CPU=0.00, Wall_clock=8. ============================== end of statistics ===================== ------ process 19152 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 19152 exit (max_proofs) Sat Jun 24 06:23:31 2006 Successful proof using the following 9 assumptions: clauses(assumptions_in_proof). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). end_of_list. Including 55 new hint clauses: clauses(new_hints). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). f(c2,c1) != f(c1,c2) # label("Commutativity"). f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. f(f(f(x,f(y,z)),f(f(x,f(y,z)),x)),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). f(f(f(x,f(x,x)),x),f(x,x)) = x. f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. f(f(x,f(x,x)),f(f(f(x,f(x,x)),f(x,x)),f(y,f(x,x)))) = f(f(x,f(x,x)),f(x,x)). f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(f(x,x),x)). f(x,f(f(x,x),x)) = f(x,x). f(x,f(f(x,x),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). f(f(x,f(x,x)),f(x,x)) = x. f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = f(f(x,f(x,x)),f(x,x)). f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. f(f(x,x),f(x,f(y,x))) = x. f(f(x,f(f(x,x),x)),f(x,x)) = x. f(f(x,x),f(x,x)) = x. f(f(x,f(x,x)),f(f(x,x),f(x,x))) = f(x,x). f(f(x,f(x,x)),x) = f(x,x). f(f(x,x),f(x,f(x,y))) = x. f(f(x,x),f(x,f(y,f(f(x,y),y)))) = x. f(f(f(x,y),f(f(x,y),f(f(x,x),f(x,x)))),x) = f(x,x). f(f(f(x,y),f(f(x,y),x)),x) = f(x,x). f(f(f(x,f(x,x)),x),f(f(y,f(x,x)),f(f(x,f(x,x)),x))) = f(y,f(x,x)). f(f(x,x),f(f(y,f(x,x)),f(f(x,f(x,x)),x))) = f(y,f(x,x)). f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(y,f(x,x)). f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,f(x,f(y,f(x,x)))))) = f(x,x). f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(x,f(y,y)),f(x,y)) = x. f(f(f(x,f(x,f(y,f(x,x)))),x),y) = f(y,f(x,x)). f(f(x,x),y) = f(y,f(x,x)). f(f(f(x,f(y,x)),f(f(x,f(y,x)),x)),x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(f(x,x),x)). f(x,f(f(x,x),x)) = f(x,x). f(x,y) = f(y,f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))). f(x,y) = f(y,f(f(x,x),f(x,f(f(x,x),x)))). f(x,y) = f(y,f(f(x,x),f(x,x))). f(x,y) = f(y,x). $F. end_of_list. Attempt to eliminate one assumption: f(f(x,f(x,f(y,x))),f(y,f(z,x))) = y # label("C2/A4 (Wald 1)"). *********************************************** AUTO SKETCHES ITERATION 4 *********************************************** Starting a search with 14 assumptions: clauses(assumptions_active). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Child search process 19154 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 2 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 3 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 4 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 5 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 6 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 7 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 8 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 9 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 10 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 11 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 12 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 13 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 14 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 15 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 16 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). end_of_list. % 208 hints input. Predicate elimination: (none). Term ordering decisions: Function symbol KB weights: c1=1. c2=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Reasonable options, based on the structure of the clauses: (nothing changed) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 225 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 226 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 227 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 228 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 229 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 230 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 231 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 232 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 233 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 234 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 235 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 236 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 237 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 238 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 239 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 240 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). 225 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 227 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 228 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 229 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 230 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 231 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 232 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 233 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 234 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 235 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 236 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 237 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 238 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 239 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 240 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(denials). end_of_list. % 208 hints processed (89 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. -------- Proof 1 -------- % Operation f is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 0.47 (+ 0.00) seconds. % Length of proof is 55. % Level of proof is 16. % Maximum clause weight is 39. % Given clauses 27. 225 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 226 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 227 f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). [input]. 229 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 230 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 233 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 234 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 235 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 236 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 238 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 240 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. 241 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(225(a,1),225(a,1,1,2,1))]. 243 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(225(a,1),225(a,1,2))]. 245 f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. [para(227(a,1),225(a,1,1,2))]. 294 f(f(f(x,y),f(f(f(x,f(f(z,x),x)),f(x,y)),f(x,y))),z) = f(x,f(f(z,x),x)). [para(230(a,1),225(a,1,2))]. 910 f(f(f(x,f(x,x)),x),f(x,x)) = x. [para(225(a,1),245(a,1,2,2))]. 947 f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. [para(910(a,1),225(a,1,2,2))]. 948 f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). [para(225(a,1),910(a,1,1,1,2)),demod(225(15))]. 971 f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. [para(910(a,1),236(a,1,1,1))]. 1025 f(f(f(x,f(x,f(f(x,x),f(f(y,f(x,x)),f(x,x))))),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). [para(947(a,1),234(a,1,2))]. 1063 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),f(f(x,f(x,x)),f(x,x))),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). [para(947(a,1),947(a,1,1,2,1))]. 1067 f(f(f(x,f(f(x,x),x)),x),x) = f(x,f(f(x,x),x)). [para(225(a,1),971(a,1,1,2)),demod(225(14),225(17),225(13))]. 1073 f(f(f(x,f(x,x)),x),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x))) = f(f(x,x),f(x,f(x,x))). [para(971(a,1),229(a,1,1,2))]. 1087 f(f(f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). [para(971(a,1),235(a,1,2))]. 1106 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),x)) = f(z,f(f(x,z),z)). [para(225(a,1),241(a,1,2,2))]. 1127 f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). [para(230(a,1),241(a,1,1))]. 1184 f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = x. [para(241(a,1),910(a,1,1,1,2)),demod(230(8),230(12),230(13),230(13),230(15))]. 1188 f(f(x,f(x,x)),f(x,x)) = x. [para(241(a,1),971(a,1,2,2,1)),demod(230(8),230(8),230(8),230(10),230(13),230(13),230(13),230(8),230(12))]. 1192 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),x). [back_demod(1063),demod(1188(9),1188(13))]. 1197 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). [para(1188(a,1),225(a,1,1,2,1))]. 1211 f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))) = f(x,x). [para(1188(a,1),233(a,1,1,1))]. 1229 f(f(x,x),x) = f(x,f(x,x)). [back_demod(1087),demod(1197(10),1211(7))]. 1236 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(x,f(x,x)). [back_demod(1192),demod(1229(6),1229(10))]. 1238 f(f(f(x,f(x,f(x,f(x,x)))),x),f(x,x)) = x. [back_demod(1184),demod(1229(2))]. 1243 f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(x,f(x,x)))))) = f(x,f(x,f(x,x))). [back_demod(1127),demod(1229(2),1229(5),1229(11))]. 1245 f(f(f(x,f(x,f(x,x))),x),x) = f(x,f(x,f(x,x))). [back_demod(1067),demod(1229(2),1229(7))]. 1246 f(x,f(x,f(x,x))) = f(x,x). [back_demod(948),demod(1229(2),1229(6),238(8),1229(3)),flip(a)]. 1265 f(f(x,x),f(x,f(x,x))) = x. [back_demod(1073),demod(1236(11),240(6)),flip(a)]. 1266 f(f(x,f(x,x)),x) = f(x,x). [back_demod(1245),demod(1246(3),1229(2),1246(6))]. 1267 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). [back_demod(1243),demod(1246(3),1246(4),1246(8))]. 1270 f(f(x,x),f(x,x)) = x. [back_demod(1238),demod(1246(3),1266(3))]. 1329 f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(f(x,x),y). [back_demod(1025),demod(1267(7),1266(3)),flip(a)]. 1384 f(f(x,y),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). [para(1270(a,1),241(a,1,2,2)),demod(1265(9))]. 1385 f(f(x,x),f(x,f(y,x))) = x. [para(1229(a,1),225(a,1,1,2)),demod(1246(3))]. 1412 f(f(x,y),f(x,f(f(f(x,y),f(x,y)),y))) = x. [para(1229(a,1),238(a,1,1,1)),demod(1188(9))]. 1544 f(x,f(f(y,x),x)) = f(x,y). [para(1266(a,1),243(a,1,1,1)),demod(1266(7),1266(9),1329(9),1385(5)),flip(a)]. 1621 f(f(x,y),y) = f(y,f(x,y)). [back_demod(1384),demod(1544(5),1544(6),1544(6))]. 1685 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(z,f(x,z))),x)) = f(z,f(z,f(x,z))). [back_demod(1106),demod(1621(8),1621(13))]. 1772 f(f(f(x,y),f(f(x,y),f(f(x,f(x,f(z,x))),f(x,y)))),z) = f(x,f(x,f(z,x))). [back_demod(294),demod(1621(3),1621(8),1621(12))]. 1808 f(x,f(x,f(y,x))) = f(x,y). [back_demod(1544),demod(1621(2))]. 2143 f(f(f(x,y),f(x,z)),z) = f(x,z). [back_demod(1772),demod(1808(5),1808(7),1808(7))]. 2214 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(x,f(z,x))) = f(z,x). [back_demod(1685),demod(1808(9),1621(8),1808(12))]. 2291 f(f(x,y),f(x,f(x,y))) = x. [back_demod(1412),demod(2143(5))]. 2409 f(x,y) = f(y,x). [back_demod(2214),demod(2291(6),1808(3))]. 2410 $F. [resolve(2409,a,226,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=27. Generated=3244. Kept=2185. proofs=1. Usable=11. Sos=709. Demods=836. Denials=0. Limbo=118, Disabled=1362. Hints=208. Weight_deleted=21. Literals_deleted=0. Forward_subsumed=1038. Back_subsumed=106. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2180 (0 lex), Back_demodulated=1240. Back_unit_deleted=0. Demod_attempts=66212. Demod_rewrites=4839. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=2.41. User_CPU=0.47, System_CPU=0.00, Wall_clock=10. ============================== end of statistics ===================== ------ process 19154 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 19154 exit (max_proofs) Sat Jun 24 06:23:33 2006 Successful proof using the following 9 assumptions: clauses(assumptions_in_proof). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Including 110 new hint clauses: clauses(new_hints). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). f(c2,c1) != f(c1,c2) # label("Commutativity"). f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. f(f(f(x,y),f(f(f(x,f(f(z,x),x)),f(x,y)),f(x,y))),z) = f(x,f(f(z,x),x)). f(f(f(x,f(x,x)),x),f(x,x)) = x. f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))) = f(x,f(f(x,x),x)). f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. f(f(f(x,f(x,f(f(x,x),f(f(y,f(x,x)),f(x,x))))),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),f(f(x,f(x,x)),f(x,x))),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). f(f(f(x,f(f(x,x),x)),x),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))))))) = f(x,f(f(x,x),x)). f(f(f(x,f(f(x,x),x)),x),f(f(x,f(f(x,x),x)),f(x,f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))))))) = f(x,f(f(x,x),x)). f(f(f(x,f(f(x,x),x)),x),f(f(x,f(f(x,x),x)),f(x,f(f(x,f(f(x,x),x)),x)))) = f(x,f(f(x,x),x)). f(f(f(x,f(f(x,x),x)),x),x) = f(x,f(f(x,x),x)). f(f(f(x,f(x,x)),x),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x))) = f(f(x,x),f(x,f(x,x))). f(f(f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),x)) = f(z,f(f(x,z),z)). f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(f(f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = x. f(f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,x))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,x)) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,x)) = x. f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))) = f(x,x). f(f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). f(f(x,x),x) = f(x,f(x,x)). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(f(x,x),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(x,f(x,x)). f(f(f(x,f(x,f(x,f(x,x)))),x),f(x,x)) = x. f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(x,f(x,x)))))) = f(x,f(f(x,x),x)). f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(x,f(x,x)))))) = f(x,f(x,f(x,x))). f(f(f(x,f(x,f(x,x))),x),x) = f(x,f(f(x,x),x)). f(f(f(x,f(x,f(x,x))),x),x) = f(x,f(x,f(x,x))). f(f(f(f(x,f(x,f(x,x))),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). f(f(f(f(x,f(x,f(x,x))),x),f(x,f(x,f(x,x)))),x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(x,f(x,x))). f(x,f(x,f(x,x))) = f(x,x). f(f(f(x,f(x,x)),x),f(x,f(x,x))) = f(f(x,x),f(x,f(x,x))). x = f(f(x,x),f(x,f(x,x))). f(f(x,x),f(x,f(x,x))) = x. f(f(f(x,x),x),x) = f(x,f(x,f(x,x))). f(f(x,f(x,x)),x) = f(x,f(x,f(x,x))). f(f(x,f(x,x)),x) = f(x,x). f(x,f(f(x,x),f(y,f(x,f(x,f(x,x)))))) = f(x,f(x,f(x,x))). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,f(x,f(x,x))). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). f(f(f(x,f(x,x)),x),f(x,x)) = x. f(f(x,x),f(x,x)) = x. f(f(f(x,f(x,x)),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(x,x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(f(x,x),y). f(f(f(f(x,y),f(x,y)),f(f(x,y),f(f(x,y),f(x,y)))),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,y),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,f(x,f(x,x))),f(x,f(y,x))) = x. f(f(x,x),f(x,f(y,x))) = x. f(f(f(f(x,y),f(f(x,y),f(x,y))),f(f(x,y),f(x,y))),f(x,f(f(f(x,y),f(x,y)),y))) = x. f(f(x,y),f(x,f(f(f(x,y),f(x,y)),y))) = x. f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(f(x,f(x,x)),x)),f(f(x,f(x,x)),x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(x,x)),f(f(x,f(x,x)),x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(x,x)),f(x,x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(x,f(f(y,x),x))),y) = f(x,f(f(y,x),x)). f(x,y) = f(x,f(f(y,x),x)). f(x,f(f(y,x),x)) = f(x,y). f(f(x,y),f(f(y,f(x,y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,y),y) = f(y,f(f(f(x,y),y),y)). f(f(x,y),y) = f(y,f(x,y)). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(z,f(x,z))),x)) = f(z,f(f(x,z),z)). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(z,f(x,z))),x)) = f(z,f(z,f(x,z))). f(f(f(x,y),f(f(f(x,f(x,f(z,x))),f(x,y)),f(x,y))),z) = f(x,f(f(z,x),x)). f(f(f(x,y),f(f(x,y),f(f(x,f(x,f(z,x))),f(x,y)))),z) = f(x,f(f(z,x),x)). f(f(f(x,y),f(f(x,y),f(f(x,f(x,f(z,x))),f(x,y)))),z) = f(x,f(x,f(z,x))). f(x,f(x,f(y,x))) = f(x,y). f(f(f(x,y),f(f(x,y),f(f(x,z),f(x,y)))),z) = f(x,f(x,f(z,x))). f(f(f(x,y),f(x,z)),z) = f(x,f(x,f(z,x))). f(f(f(x,y),f(x,z)),z) = f(x,z). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,x),x)) = f(z,f(z,f(x,z))). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(x,f(z,x))) = f(z,f(z,f(x,z))). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(x,f(z,x))) = f(z,x). f(f(x,y),f(x,f(x,y))) = x. f(x,f(x,f(z,x))) = f(z,x). f(x,y) = f(y,x). $F. end_of_list. Attempt to eliminate one assumption: f(f(x,f(x,f(y,y))),f(y,f(z,x))) = y # label("C3/A6"). *********************************************** AUTO SKETCHES ITERATION 5 *********************************************** Starting a search with 13 assumptions: clauses(assumptions_active). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Child search process 19155 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 2 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 3 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 4 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 5 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 6 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 7 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 8 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 9 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 10 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 11 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 12 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 13 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 14 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 15 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). end_of_list. % 318 hints input. Predicate elimination: (none). Term ordering decisions: Function symbol KB weights: c1=1. c2=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Reasonable options, based on the structure of the clauses: (nothing changed) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 334 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 335 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 336 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 337 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 338 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 339 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 340 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 341 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 342 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 343 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 344 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 345 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 346 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 347 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 348 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). 334 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 336 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 337 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 338 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 339 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 340 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 341 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 342 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 343 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 344 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 345 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 346 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 347 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 348 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(denials). end_of_list. % 318 hints processed (121 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. -------- Proof 1 -------- % Operation f is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 0.58 (+ 0.00) seconds. % Length of proof is 56. % Level of proof is 17. % Maximum clause weight is 35. % Given clauses 28. 334 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 335 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 336 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). [input]. 337 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 338 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 340 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 341 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 342 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 343 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 344 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 346 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 348 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. 349 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(334(a,1),334(a,1,1,2,1))]. 351 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(334(a,1),334(a,1,2))]. 353 f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. [para(336(a,1),334(a,1,1,2))]. 876 f(f(f(x,f(x,f(y,f(f(x,y),y)))),x),x) = f(y,f(f(x,y),y)). [para(334(a,1),348(a,1,2))]. 944 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),x)) = f(z,f(f(x,z),z)). [para(334(a,1),349(a,1,2,2))]. 962 f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). [para(338(a,1),349(a,1,1))]. 1018 f(f(f(x,f(x,x)),x),f(x,x)) = x. [para(334(a,1),353(a,1,2,2))]. 1057 f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). [para(349(a,1),353(a,1,2,2)),demod(334(10),334(15))]. 1059 f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. [para(1018(a,1),334(a,1,2,2))]. 1081 f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. [para(1018(a,1),344(a,1,1,1))]. 1094 f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = x. [para(349(a,1),1018(a,1,1,1,2)),demod(338(8),338(12),338(13),338(13),338(15))]. 1162 f(f(f(x,f(x,f(f(x,x),f(f(y,f(x,x)),f(x,x))))),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). [para(1059(a,1),342(a,1,2))]. 1206 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(f(x,x),x))),x),x)) = f(f(x,f(x,f(f(x,x),x))),x). [para(1094(a,1),1059(a,1,1,2,1))]. 1208 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),f(f(x,f(x,x)),f(x,x))),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). [para(1059(a,1),1059(a,1,1,2,1))]. 1232 f(f(f(f(x,y),x),x),f(y,f(z,f(f(x,z),z)))) = y. [para(351(a,1),340(a,1,2,2))]. 1288 f(f(f(x,f(x,x)),x),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x))) = f(f(x,x),f(x,f(x,x))). [para(1081(a,1),337(a,1,1,2))]. 1302 f(f(f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). [para(1081(a,1),343(a,1,2))]. 1316 f(f(f(x,f(x,f(x,f(x,x)))),x),x) = f(x,f(x,x)). [para(1081(a,1),348(a,1,2))]. 1319 f(f(x,f(x,x)),f(x,x)) = x. [para(349(a,1),1081(a,1,2,2,1)),demod(338(8),338(8),338(8),338(10),338(13),338(13),338(13),338(8),338(12))]. 1321 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),x). [back_demod(1208),demod(1319(9),1319(13))]. 1325 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). [para(1319(a,1),334(a,1,1,2,1))]. 1338 f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))) = f(x,x). [para(1319(a,1),341(a,1,1,1))]. 1358 f(f(x,x),x) = f(x,f(x,x)). [back_demod(1302),demod(1325(10),1338(7))]. 1365 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(x,f(x,x)). [back_demod(1321),demod(1358(6),1358(10))]. 1370 f(f(f(x,x),f(x,f(x,x))),f(x,f(x,x))) = f(f(x,f(x,f(x,f(x,x)))),x). [back_demod(1206),demod(1358(6),1316(10),1358(9))]. 1401 f(x,f(x,f(x,x))) = f(x,x). [back_demod(1057),demod(1358(2),1358(6),346(8),1358(3)),flip(a)]. 1403 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). [back_demod(962),demod(1358(2),1401(3),1358(3),1401(4),1358(7),1401(8))]. 1421 f(f(x,x),f(x,f(x,x))) = x. [back_demod(1288),demod(1365(11),348(6)),flip(a)]. 1425 f(f(x,f(x,x)),x) = f(x,x). [back_demod(1370),demod(1421(4),1401(3),1401(4)),flip(a)]. 1433 f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(f(x,x),y). [back_demod(1162),demod(1403(7),1425(3)),flip(a)]. 1492 f(f(x,x),f(x,x)) = x. [back_demod(1018),demod(1425(3))]. 1547 f(f(x,y),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). [para(1492(a,1),349(a,1,2,2)),demod(1421(9))]. 1548 f(f(x,x),f(x,f(y,x))) = x. [para(1358(a,1),334(a,1,1,2)),demod(1401(3))]. 1741 f(x,f(f(y,x),x)) = f(x,y). [para(1425(a,1),351(a,1,1,1)),demod(1425(7),1425(9),1433(9),1548(5)),flip(a)]. 1768 f(f(x,y),y) = f(y,f(x,y)). [back_demod(1547),demod(1741(5),1741(6),1741(6))]. 1825 f(f(x,f(f(x,y),x)),f(y,f(z,f(z,f(x,z))))) = y. [back_demod(1232),demod(1768(3),1768(5))]. 1905 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(z,f(x,z))),x)) = f(z,f(z,f(x,z))). [back_demod(944),demod(1768(8),1768(13))]. 1910 f(x,f(f(x,f(x,f(y,f(y,f(x,y))))),x)) = f(y,f(y,f(x,y))). [back_demod(876),demod(1768(2),1768(7),1768(9))]. 2011 f(x,f(x,f(y,x))) = f(x,y). [back_demod(1741),demod(1768(2))]. 2438 f(x,f(f(x,y),x)) = f(y,x). [back_demod(1910),demod(2011(3),2011(3),2011(6))]. 2443 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(x,f(z,x))) = f(z,x). [back_demod(1905),demod(2011(9),1768(8),2011(12))]. 2511 f(f(x,y),f(x,f(z,y))) = x. [back_demod(1825),demod(2438(3),2011(4))]. 2692 f(x,y) = f(y,x). [back_demod(2443),demod(2511(6),2011(3))]. 2693 $F. [resolve(2692,a,335,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=28. Generated=3642. Kept=2359. proofs=1. Usable=11. Sos=674. Demods=864. Denials=0. Limbo=181, Disabled=1507. Hints=318. Weight_deleted=66. Literals_deleted=0. Forward_subsumed=1217. Back_subsumed=113. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2354 (0 lex), Back_demodulated=1379. Back_unit_deleted=0. Demod_attempts=85741. Demod_rewrites=6134. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=2.88. User_CPU=0.58, System_CPU=0.00, Wall_clock=12. ============================== end of statistics ===================== ------ process 19155 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 19155 exit (max_proofs) Sat Jun 24 06:23:35 2006 Successful proof using the following 10 assumptions: clauses(assumptions_in_proof). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Including 112 new hint clauses: clauses(new_hints). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). f(c2,c1) != f(c1,c2) # label("Commutativity"). f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. f(f(f(x,f(x,f(y,f(f(x,y),y)))),x),x) = f(y,f(f(x,y),y)). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),x)) = f(z,f(f(x,z),z)). f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(f(f(x,f(x,x)),x),f(x,x)) = x. f(f(f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))) = f(x,f(f(x,x),x)). f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))) = f(x,f(f(x,x),x)). f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. f(f(f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = x. f(f(f(x,f(x,f(f(x,x),f(f(y,f(x,x)),f(x,x))))),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(f(x,x),x))),x),x)) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),f(f(x,f(x,x)),f(x,x))),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). f(f(f(f(x,y),x),x),f(y,f(z,f(f(x,z),z)))) = y. f(f(f(x,f(x,x)),x),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x))) = f(f(x,x),f(x,f(x,x))). f(f(f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). f(f(f(x,f(x,f(x,f(x,x)))),x),x) = f(x,f(x,x)). f(f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,x))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,x)) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,x)) = x. f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))) = f(x,x). f(f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). f(f(x,x),x) = f(x,f(x,x)). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(f(x,x),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(x,f(x,x)). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(x,f(x,x)))),x),x)) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,x),f(x,f(x,x))),f(x,f(x,x))) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,x),f(x,f(x,x))),f(x,f(x,x))) = f(f(x,f(x,f(x,f(x,x)))),x). f(f(f(f(x,f(x,f(x,x))),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). f(f(f(f(x,f(x,f(x,x))),x),f(x,f(x,f(x,x)))),x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(x,f(x,x))). f(x,f(x,f(x,x))) = f(x,x). f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,f(x,f(x,x)))))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,f(x,f(x,x))). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). f(f(f(x,f(x,x)),x),f(x,f(x,x))) = f(f(x,x),f(x,f(x,x))). x = f(f(x,x),f(x,f(x,x))). f(f(x,x),f(x,f(x,x))) = x. f(x,f(x,f(x,x))) = f(f(x,f(x,f(x,f(x,x)))),x). f(x,x) = f(f(x,f(x,f(x,f(x,x)))),x). f(x,x) = f(f(x,f(x,x)),x). f(f(x,f(x,x)),x) = f(x,x). f(f(f(x,f(x,x)),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(x,x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(f(x,x),y). f(f(x,x),f(x,x)) = x. f(f(f(f(x,y),f(x,y)),f(f(x,y),f(f(x,y),f(x,y)))),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,y),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,f(x,f(x,x))),f(x,f(y,x))) = x. f(f(x,x),f(x,f(y,x))) = x. f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(f(x,f(x,x)),x)),f(f(x,f(x,x)),x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(x,x)),f(f(x,f(x,x)),x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(x,x)),f(x,x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(x,f(f(y,x),x))),y) = f(x,f(f(y,x),x)). f(x,y) = f(x,f(f(y,x),x)). f(x,f(f(y,x),x)) = f(x,y). f(f(x,y),f(f(y,f(x,y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,y),y) = f(y,f(f(f(x,y),y),y)). f(f(x,y),y) = f(y,f(x,y)). f(f(x,f(f(x,y),x)),f(y,f(z,f(f(x,z),z)))) = y. f(f(x,f(f(x,y),x)),f(y,f(z,f(z,f(x,z))))) = y. f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(z,f(x,z))),x)) = f(z,f(f(x,z),z)). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(z,f(x,z))),x)) = f(z,f(z,f(x,z))). f(f(f(x,f(x,f(y,f(y,f(x,y))))),x),x) = f(y,f(f(x,y),y)). f(x,f(f(x,f(x,f(y,f(y,f(x,y))))),x)) = f(y,f(f(x,y),y)). f(x,f(f(x,f(x,f(y,f(y,f(x,y))))),x)) = f(y,f(y,f(x,y))). f(x,f(x,f(y,x))) = f(x,y). f(x,f(f(x,f(x,f(y,x))),x)) = f(y,f(y,f(x,y))). f(x,f(f(x,y),x)) = f(y,f(y,f(x,y))). f(x,f(f(x,y),x)) = f(y,x). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,x),x)) = f(z,f(z,f(x,z))). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(x,f(z,x))) = f(z,f(z,f(x,z))). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(x,f(z,x))) = f(z,x). f(f(y,x),f(y,f(z,f(z,f(x,z))))) = y. f(f(x,y),f(x,f(z,y))) = x. f(x,f(x,f(z,x))) = f(z,x). f(x,y) = f(y,x). $F. end_of_list. Attempt to eliminate one assumption: f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label("C4/A7"). *********************************************** AUTO SKETCHES ITERATION 6 *********************************************** Starting a search with 12 assumptions: clauses(assumptions_active). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Child search process 19156 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 2 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 3 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 4 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 5 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 6 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 7 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 8 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 9 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 10 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 11 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 12 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 13 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 14 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). end_of_list. % 430 hints input. Predicate elimination: (none). Term ordering decisions: Function symbol KB weights: c1=1. c2=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Reasonable options, based on the structure of the clauses: (nothing changed) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 445 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 446 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 447 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 448 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 449 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 450 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 451 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 452 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 453 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 454 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 455 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 456 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 457 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 458 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). 445 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 447 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 448 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 449 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 450 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 451 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 452 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 453 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 454 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 455 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 456 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 457 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 458 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(denials). end_of_list. % 430 hints processed (209 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. -------- Proof 1 -------- % Operation f is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 0.44 (+ 0.02) seconds. % Length of proof is 53. % Level of proof is 17. % Maximum clause weight is 29. % Given clauses 27. 445 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 446 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 447 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). [input]. 448 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 451 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 452 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 453 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 454 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 456 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 458 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. 459 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(445(a,1),445(a,1,1,2,1))]. 461 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(445(a,1),445(a,1,2))]. 463 f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. [para(447(a,1),445(a,1,1,2))]. 477 f(f(x,f(f(f(y,f(f(x,y),y)),x),x)),x) = f(y,f(f(x,y),y)). [para(445(a,1),448(a,1,2))]. 564 f(f(f(x,y),f(f(f(f(y,f(y,z)),y),f(x,y)),f(x,y))),z) = f(f(y,f(y,z)),y). [para(452(a,1),445(a,1,2))]. 679 f(f(f(f(f(x,y),f(f(y,f(y,z)),y)),z),z),z) = f(f(y,f(y,z)),y). [para(452(a,1),454(a,1,2))]. 958 f(f(f(x,f(x,x)),x),f(x,x)) = x. [para(445(a,1),463(a,1,2,2))]. 1004 f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). [para(448(a,1),459(a,1,1))]. 1059 f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). [para(459(a,1),463(a,1,2,2)),demod(445(10),445(15))]. 1064 f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. [para(958(a,1),445(a,1,2,2))]. 1082 f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. [para(958(a,1),454(a,1,1,1))]. 1095 f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = x. [para(459(a,1),958(a,1,1,1,2)),demod(448(8),448(12),448(13),448(13),448(15))]. 1153 f(f(f(x,f(x,f(f(x,x),f(f(y,f(x,x)),f(x,x))))),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). [para(1064(a,1),452(a,1,2))]. 1197 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(f(x,x),x))),x),x)) = f(f(x,f(x,f(f(x,x),x))),x). [para(1095(a,1),1064(a,1,1,2,1))]. 1199 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),f(f(x,f(x,x)),f(x,x))),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). [para(1064(a,1),1064(a,1,1,2,1))]. 1205 f(f(f(x,f(x,x)),x),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x))) = f(f(x,x),f(x,f(x,x))). [para(1082(a,1),447(a,1,1,2))]. 1219 f(f(f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). [para(1082(a,1),453(a,1,2))]. 1233 f(f(f(x,f(x,f(x,f(x,x)))),x),x) = f(x,f(x,x)). [para(1082(a,1),458(a,1,2))]. 1236 f(f(x,f(x,x)),f(x,x)) = x. [para(459(a,1),1082(a,1,2,2,1)),demod(448(8),448(8),448(8),448(10),448(13),448(13),448(13),448(8),448(12))]. 1237 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),x). [back_demod(1199),demod(1236(9),1236(13))]. 1307 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). [para(1236(a,1),445(a,1,1,2,1))]. 1317 f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))) = f(x,x). [para(1236(a,1),451(a,1,1,1))]. 1337 f(f(x,x),x) = f(x,f(x,x)). [back_demod(1219),demod(1307(10),1317(7))]. 1345 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(x,f(x,x)). [back_demod(1237),demod(1337(6),1337(10))]. 1349 f(f(f(x,x),f(x,f(x,x))),f(x,f(x,x))) = f(f(x,f(x,f(x,f(x,x)))),x). [back_demod(1197),demod(1337(6),1233(10),1337(9))]. 1377 f(x,f(x,f(x,x))) = f(x,x). [back_demod(1059),demod(1337(2),1337(6),456(8),1337(3)),flip(a)]. 1379 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). [back_demod(1004),demod(1337(2),1377(3),1337(3),1377(4),1337(7),1377(8))]. 1394 f(f(x,x),f(x,f(x,x))) = x. [back_demod(1205),demod(1345(11),458(6)),flip(a)]. 1398 f(f(x,f(x,x)),x) = f(x,x). [back_demod(1349),demod(1394(4),1377(3),1377(4)),flip(a)]. 1405 f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(f(x,x),y). [back_demod(1153),demod(1379(7),1398(3)),flip(a)]. 1458 f(f(x,x),f(x,x)) = x. [back_demod(958),demod(1398(3))]. 1509 f(f(x,y),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). [para(1458(a,1),459(a,1,2,2)),demod(1394(9))]. 1510 f(f(x,x),f(x,f(y,x))) = x. [para(1337(a,1),445(a,1,1,2)),demod(1377(3))]. 1685 f(x,f(f(y,x),x)) = f(x,y). [para(1398(a,1),461(a,1,1,1)),demod(1398(7),1398(9),1405(9),1510(5)),flip(a)]. 1712 f(f(x,y),y) = f(y,f(x,y)). [back_demod(1509),demod(1685(5),1685(6),1685(6))]. 1891 f(f(f(x,y),f(f(x,y),f(f(f(y,f(y,z)),y),f(x,y)))),z) = f(f(y,f(y,z)),y). [back_demod(564),demod(1712(8))]. 1918 f(f(x,f(x,f(f(y,f(y,f(x,y))),x))),x) = f(y,f(y,f(x,y))). [back_demod(477),demod(1712(2),1712(5),1712(9))]. 1935 f(x,f(x,f(y,x))) = f(x,y). [back_demod(1685),demod(1712(2))]. 2148 f(f(x,f(f(f(y,z),f(f(z,f(z,x)),z)),x)),x) = f(f(z,f(z,x)),z). [back_demod(679),demod(1712(7))]. 2260 f(f(x,f(x,y)),x) = f(y,x). [back_demod(1918),demod(1935(3),1712(2),1935(3),1935(6))]. 2284 f(f(f(x,y),f(z,y)),z) = f(z,y). [back_demod(1891),demod(2260(5),1935(7),2260(7))]. 2449 f(x,y) = f(y,x). [back_demod(2148),demod(2260(4),2284(4),2260(3),2260(4))]. 2450 $F. [resolve(2449,a,446,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=27. Generated=3158. Kept=2005. proofs=1. Usable=10. Sos=646. Demods=843. Denials=0. Limbo=189, Disabled=1173. Hints=430. Weight_deleted=67. Literals_deleted=0. Forward_subsumed=1086. Back_subsumed=62. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2000 (0 lex), Back_demodulated=1097. Back_unit_deleted=0. Demod_attempts=76449. Demod_rewrites=5442. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=2.72. User_CPU=0.44, System_CPU=0.02, Wall_clock=13. ============================== end of statistics ===================== ------ process 19156 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 19156 exit (max_proofs) Sat Jun 24 06:23:36 2006 Successful proof using the following 8 assumptions: clauses(assumptions_in_proof). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Including 109 new hint clauses: clauses(new_hints). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). f(c2,c1) != f(c1,c2) # label("Commutativity"). f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. f(f(x,f(f(f(y,f(f(x,y),y)),x),x)),x) = f(y,f(f(x,y),y)). f(f(f(x,y),f(f(f(f(y,f(y,z)),y),f(x,y)),f(x,y))),z) = f(f(y,f(y,z)),y). f(f(f(f(f(x,y),f(f(y,f(y,z)),y)),z),z),z) = f(f(y,f(y,z)),y). f(f(f(x,f(x,x)),x),f(x,x)) = x. f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(f(f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))) = f(x,f(f(x,x),x)). f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))) = f(x,f(f(x,x),x)). f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. f(f(f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = x. f(f(f(x,f(x,f(f(x,x),f(f(y,f(x,x)),f(x,x))))),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(f(x,x),x))),x),x)) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),f(f(x,f(x,x)),f(x,x))),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). f(f(f(x,f(x,x)),x),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x))) = f(f(x,x),f(x,f(x,x))). f(f(f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). f(f(f(x,f(x,f(x,f(x,x)))),x),x) = f(x,f(x,x)). f(f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,x))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,x)) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,x)) = x. f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),f(f(x,f(x,x)),f(x,x))). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,x),x),x)) = f(f(x,x),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))) = f(x,x). f(f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). f(f(x,x),x) = f(x,f(x,x)). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(f(x,x),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),x)) = f(x,f(x,x)). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(x,f(x,x)))),x),x)) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,x),f(x,f(x,x))),f(x,f(x,x))) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,x),f(x,f(x,x))),f(x,f(x,x))) = f(f(x,f(x,f(x,f(x,x)))),x). f(f(f(f(x,f(x,f(x,x))),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). f(f(f(f(x,f(x,f(x,x))),x),f(x,f(x,f(x,x)))),x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(x,f(x,x))). f(x,f(x,f(x,x))) = f(x,x). f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,f(x,f(x,x)))))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,f(f(x,x),x)). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,f(x,f(x,x))). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). f(f(f(x,f(x,x)),x),f(x,f(x,x))) = f(f(x,x),f(x,f(x,x))). x = f(f(x,x),f(x,f(x,x))). f(f(x,x),f(x,f(x,x))) = x. f(x,f(x,f(x,x))) = f(f(x,f(x,f(x,f(x,x)))),x). f(x,x) = f(f(x,f(x,f(x,f(x,x)))),x). f(x,x) = f(f(x,f(x,x)),x). f(f(x,f(x,x)),x) = f(x,x). f(f(f(x,f(x,x)),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(x,x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(f(x,x),y). f(f(x,x),f(x,x)) = x. f(f(f(f(x,y),f(x,y)),f(f(x,y),f(f(x,y),f(x,y)))),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,y),f(f(y,f(f(f(x,y),y),y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,f(x,f(x,x))),f(x,f(y,x))) = x. f(f(x,x),f(x,f(y,x))) = x. f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(f(x,f(x,x)),x)),f(f(x,f(x,x)),x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(x,x)),f(f(x,f(x,x)),x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(f(f(x,f(f(y,x),x)),f(x,x)),f(x,x))),y) = f(x,f(f(y,x),x)). f(f(f(x,x),f(x,f(f(y,x),x))),y) = f(x,f(f(y,x),x)). f(x,y) = f(x,f(f(y,x),x)). f(x,f(f(y,x),x)) = f(x,y). f(f(x,y),f(f(y,f(x,y)),f(x,y))) = f(y,f(f(f(x,y),y),y)). f(f(x,y),y) = f(y,f(f(f(x,y),y),y)). f(f(x,y),y) = f(y,f(x,y)). f(f(f(x,y),f(f(x,y),f(f(f(y,f(y,z)),y),f(x,y)))),z) = f(f(y,f(y,z)),y). f(f(x,f(f(f(y,f(y,f(x,y))),x),x)),x) = f(y,f(f(x,y),y)). f(f(x,f(x,f(f(y,f(y,f(x,y))),x))),x) = f(y,f(f(x,y),y)). f(f(x,f(x,f(f(y,f(y,f(x,y))),x))),x) = f(y,f(y,f(x,y))). f(x,f(x,f(y,x))) = f(x,y). f(f(x,f(f(f(y,z),f(f(z,f(z,x)),z)),x)),x) = f(f(z,f(z,x)),z). f(f(x,f(x,f(f(y,x),x))),x) = f(y,f(y,f(x,y))). f(f(x,f(x,f(x,f(y,x)))),x) = f(y,f(y,f(x,y))). f(f(x,f(x,y)),x) = f(y,f(y,f(x,y))). f(f(x,f(x,y)),x) = f(y,x). f(f(f(x,y),f(f(x,y),f(f(z,y),f(x,y)))),z) = f(f(y,f(y,z)),y). f(f(f(x,y),f(z,y)),z) = f(f(y,f(y,z)),y). f(f(f(x,y),f(z,y)),z) = f(z,y). f(f(x,f(f(f(y,z),f(x,z)),x)),x) = f(f(z,f(z,x)),z). f(f(x,f(x,z)),x) = f(f(z,f(z,x)),z). f(z,x) = f(f(z,f(z,x)),z). f(x,y) = f(y,x). $F. end_of_list. Attempt to eliminate one assumption: f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label("C5/A8 (Wald 2))"). *********************************************** AUTO SKETCHES ITERATION 7 *********************************************** Starting a search with 11 assumptions: clauses(assumptions_active). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Child search process 19157 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 2 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 3 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 4 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 5 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 6 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 7 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 8 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 9 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 10 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 11 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 12 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 13 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). end_of_list. % 539 hints input. Predicate elimination: (none). Term ordering decisions: Function symbol KB weights: c1=1. c2=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Reasonable options, based on the structure of the clauses: (nothing changed) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 553 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 554 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 555 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 556 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 557 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 558 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 559 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 560 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 561 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 562 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 563 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 564 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 565 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(demodulators). 553 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 555 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 556 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 557 f(f(f(f(x,y),x),x),f(y,f(z,x))) = y # label("C8/A12_m"). [input]. 558 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 559 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 560 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 561 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 562 f(f(f(f(x,y),x),x),f(y,f(x,z))) = y # label("C13/A20_m"). [input]. 563 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 564 f(f(f(x,f(y,z)),x),f(z,f(x,y))) = z # label("C15/A23_m"). [input]. 565 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. end_of_list. clauses(denials). end_of_list. % 539 hints processed (298 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. -------- Proof 1 -------- % Operation f is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 0.30 (+ 0.01) seconds. % Length of proof is 59. % Level of proof is 18. % Maximum clause weight is 43. % Given clauses 25. 553 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). [input]. 554 f(c2,c1) != f(c1,c2) # label("Commutativity"). [clausify]. 555 f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). [input]. 556 f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). [input]. 558 f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). [input]. 559 f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). [input]. 560 f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). [input]. 561 f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). [input]. 563 f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). [input]. 565 f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). [input]. 566 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(553(a,1),553(a,1,1,2,1))]. 568 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(553(a,1),553(a,1,2))]. 573 f(f(x,f(f(f(y,f(f(x,y),y)),x),x)),x) = f(y,f(f(x,y),y)). [para(553(a,1),555(a,1,2))]. 576 f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. [para(556(a,1),553(a,1,1,2))]. 699 f(f(f(f(f(x,y),f(y,f(f(z,y),y))),z),z),z) = f(y,f(f(z,y),y)). [para(553(a,1),561(a,1,2))]. 984 f(f(f(x,f(x,x)),x),f(x,x)) = x. [para(553(a,1),576(a,1,2,2))]. 1012 f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. [para(984(a,1),553(a,1,2,2))]. 1013 f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). [para(553(a,1),984(a,1,1,1,2)),demod(553(15))]. 1028 f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. [para(984(a,1),561(a,1,1,1))]. 1047 f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). [para(555(a,1),566(a,1,1))]. 1104 f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = x. [para(566(a,1),984(a,1,1,1,2)),demod(555(8),555(12),555(13),555(13),555(15))]. 1109 f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(f(x,x),x))),x),f(y,f(x,x)))) = f(f(x,f(x,f(f(x,x),x))),x). [para(1104(a,1),553(a,1,1,2,1))]. 1112 f(f(x,f(x,f(x,f(f(x,f(x,f(f(x,x),x))),x)))),x) = f(f(x,f(x,f(f(x,x),x))),x). [para(1104(a,1),556(a,1,2))]. 1127 f(f(f(x,f(f(f(x,f(x,f(f(x,x),x))),x),x)),x),x) = f(f(x,f(x,f(f(x,x),x))),x). [para(1104(a,1),563(a,1,2))]. 1137 f(f(f(f(x,y),f(x,y)),f(f(x,y),f(f(x,y),f(x,y)))),f(f(x,f(f(f(x,y),x),x)),f(x,y))) = f(x,f(f(f(x,y),x),x)). [para(555(a,1),1012(a,1,1,2,1))]. 1142 f(f(f(f(x,y),f(x,y)),f(f(x,y),f(f(x,y),f(x,y)))),f(f(y,f(y,f(y,f(x,y)))),f(x,y))) = f(y,f(y,f(y,f(x,y)))). [para(556(a,1),1012(a,1,1,2,1))]. 1158 f(f(f(x,f(x,f(f(x,x),f(f(y,f(x,x)),f(x,x))))),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). [para(1012(a,1),559(a,1,2))]. 1208 f(f(f(x,f(f(x,x),x)),x),x) = f(x,f(f(x,x),x)). [para(553(a,1),1028(a,1,1,2)),demod(553(14),553(17),553(13))]. 1220 f(f(f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). [para(1028(a,1),560(a,1,2))]. 1234 f(f(f(x,f(x,f(x,f(x,x)))),x),x) = f(x,f(x,x)). [para(1028(a,1),565(a,1,2))]. 1237 f(f(x,f(x,x)),f(x,x)) = x. [para(566(a,1),1028(a,1,2,2,1)),demod(555(8),555(8),555(8),555(10),555(13),555(13),555(13),555(8),555(12))]. 1242 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). [para(1237(a,1),553(a,1,1,2,1))]. 1250 f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))) = f(x,x). [para(1237(a,1),558(a,1,1,1))]. 1268 f(f(x,x),x) = f(x,f(x,x)). [back_demod(1220),demod(1242(10),1250(7))]. 1276 f(f(f(x,f(x,f(x,x))),x),x) = f(x,f(x,f(x,x))). [back_demod(1208),demod(1268(2),1268(7))]. 1287 f(f(x,f(x,f(x,f(x,x)))),x) = f(x,f(x,f(x,x))). [back_demod(1127),demod(1268(2),1234(6),1276(5),1268(5)),flip(a)]. 1298 f(f(x,f(x,f(x,f(x,f(x,f(x,x)))))),x) = f(x,f(x,f(x,x))). [back_demod(1112),demod(1268(2),1287(5),1268(9),1287(12))]. 1301 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,f(x,x))),f(y,f(x,x)))) = f(x,f(x,f(x,x))). [back_demod(1109),demod(1268(6),1287(9),1268(13),1287(16))]. 1302 f(f(x,f(x,f(x,x))),f(x,x)) = x. [back_demod(1104),demod(1268(2),1287(5))]. 1306 f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(x,f(x,x)))))) = f(x,f(x,f(x,x))). [back_demod(1047),demod(1268(2),1268(5),1268(11))]. 1307 f(x,f(x,f(x,x))) = f(x,x). [back_demod(1013),demod(1268(2),1268(6),563(8),1268(3)),flip(a)]. 1323 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). [back_demod(1306),demod(1307(3),1307(4),1307(8))]. 1325 f(f(x,x),f(x,x)) = x. [back_demod(1302),demod(1307(3))]. 1326 f(f(f(x,x),f(x,f(x,x))),f(f(x,x),f(y,f(x,x)))) = f(x,x). [back_demod(1301),demod(1307(7),1307(12))]. 1328 f(f(x,f(x,x)),x) = f(x,x). [back_demod(1298),demod(1307(3),1307(3),1307(6))]. 1337 f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(f(x,x),y). [back_demod(1158),demod(1323(7),1328(3)),flip(a)]. 1467 f(f(f(x,f(f(y,x),x)),f(f(f(y,f(f(z,y),y)),f(x,f(f(y,x),x))),f(x,f(f(y,x),x)))),z) = f(y,f(f(z,y),y)). [para(568(a,1),568(a,1,1,1)),demod(568(16),568(20))]. 1472 f(f(x,x),f(x,f(x,x))) = x. [para(566(a,1),1325(a,1,1)),demod(1268(2),1307(3),1268(3),1307(4),1268(4),1307(5),1268(7),1307(8),1268(8),1307(9),1326(10),1325(3),1268(2),1307(3),1268(3),1307(4)),flip(a)]. 1488 f(f(x,y),f(f(y,f(y,f(y,f(x,y)))),f(x,y))) = f(y,f(y,f(y,f(x,y)))). [back_demod(1142),demod(1472(9))]. 1489 f(f(x,y),f(f(x,f(f(f(x,y),x),x)),f(x,y))) = f(x,f(f(f(x,y),x),x)). [back_demod(1137),demod(1472(9))]. 1490 f(f(x,x),f(x,f(y,x))) = x. [para(1268(a,1),553(a,1,1,2)),demod(1307(3))]. 1556 f(x,f(f(y,x),x)) = f(x,y). [para(1328(a,1),568(a,1,1,1)),demod(1328(7),1328(9),1337(9),1490(5)),flip(a)]. 1568 f(f(x,y),x) = f(x,f(x,y)). [back_demod(1489),demod(1556(5),1556(6),1556(6))]. 1573 f(f(f(x,y),f(y,z)),z) = f(y,z). [back_demod(1467),demod(1556(3),1556(4),1556(5),1556(7),1556(7),1556(7))]. 1700 f(f(f(x,y),y),y) = f(x,y). [back_demod(699),demod(1556(4),1573(4),1556(6))]. 1726 f(x,f(x,f(y,x))) = f(y,x). [back_demod(573),demod(1556(3),1700(3),1568(3),1556(6))]. 1905 f(f(x,y),y) = f(y,f(x,y)). [back_demod(1488),demod(1726(4),1556(6),1726(5))]. 1999 f(x,y) = f(y,x). [back_demod(1556),demod(1905(2),1726(3))]. 2000 $F. [resolve(1999,a,554,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=25. Generated=2474. Kept=1447. proofs=1. Usable=5. Sos=371. Demods=468. Denials=0. Limbo=94, Disabled=989. Hints=539. Weight_deleted=22. Literals_deleted=0. Forward_subsumed=1005. Back_subsumed=69. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1442 (0 lex), Back_demodulated=907. Back_unit_deleted=0. Demod_attempts=53803. Demod_rewrites=4439. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=2.15. User_CPU=0.30, System_CPU=0.01, Wall_clock=14. ============================== end of statistics ===================== ------ process 19157 exit (max_proofs) ------  ============================== end of search ========================= Exiting with 1 proof. Process 19157 exit (max_proofs) Sat Jun 24 06:23:37 2006 Successful proof using the following 8 assumptions: clauses(assumptions_in_proof). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). end_of_list. Including 143 new hint clauses: clauses(new_hints). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1/A10"). f(c2,c1) != f(c1,c2) # label("Commutativity"). f(f(x,f(f(y,x),x)),f(y,f(x,z))) = y # label("C6/A9"). f(f(x,f(x,f(x,y))),f(y,f(z,x))) = y # label("C7/A2"). f(f(f(f(x,y),z),z),f(y,f(x,z))) = y # label("C9/A13_m"). f(f(f(x,f(x,y)),x),f(y,f(z,x))) = y # label("C10/A16_m"). f(f(f(x,f(y,y)),x),f(y,f(z,x))) = y # label("C11/A18_m"). f(f(f(f(x,y),z),z),f(y,f(z,x))) = y # label("C12/A19_m"). f(f(f(x,f(y,z)),x),f(y,f(x,z))) = y # label("C14/A21_m"). f(f(f(x,f(x,y)),x),f(y,f(x,z))) = y # label("C16/A24_m"). f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). f(f(x,f(f(f(y,f(f(x,y),y)),x),x)),x) = f(y,f(f(x,y),y)). f(f(f(x,f(x,x)),x),f(x,f(y,f(x,f(x,x))))) = x. f(f(f(f(f(x,y),f(y,f(f(z,y),y))),z),z),z) = f(y,f(f(z,y),y)). f(f(f(x,f(x,x)),x),f(x,x)) = x. f(f(f(x,x),f(f(y,f(x,x)),f(x,x))),f(y,x)) = y. f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))) = f(x,f(f(x,x),x)). f(f(f(f(x,f(f(x,x),x)),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). f(f(x,f(x,x)),f(x,f(f(x,x),f(x,f(x,x))))) = x. f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(f(f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(f(x,f(x,f(f(x,x),x))),x),f(x,x)) = x. f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(f(x,x),x))),x),f(y,f(x,x)))) = f(f(x,f(x,f(f(x,x),x))),x). f(f(x,f(x,f(x,f(f(x,f(x,f(f(x,x),x))),x)))),x) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,f(f(f(x,f(x,f(f(x,x),x))),x),x)),x),x) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(f(x,y),f(x,y)),f(f(x,y),f(f(x,y),f(x,y)))),f(f(x,f(f(f(x,y),x),x)),f(x,y))) = f(x,f(f(f(x,y),x),x)). f(f(f(f(x,y),f(x,y)),f(f(x,y),f(f(x,y),f(x,y)))),f(f(y,f(y,f(y,f(x,y)))),f(x,y))) = f(y,f(y,f(y,f(x,y)))). f(f(f(x,f(x,f(f(x,x),f(f(y,f(x,x)),f(x,x))))),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(f(x,f(f(x,x),x)),x),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))),f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))))))) = f(x,f(f(x,x),x)). f(f(f(x,f(f(x,x),x)),x),f(f(x,f(f(x,x),x)),f(x,f(f(x,f(f(x,x),x)),f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))))))) = f(x,f(f(x,x),x)). f(f(f(x,f(f(x,x),x)),x),f(f(x,f(f(x,x),x)),f(x,f(f(x,f(f(x,x),x)),x)))) = f(x,f(f(x,x),x)). f(f(f(x,f(f(x,x),x)),x),x) = f(x,f(f(x,x),x)). f(f(f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). f(f(f(x,f(x,f(x,f(x,x)))),x),x) = f(x,f(x,x)). f(f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,f(f(x,f(f(x,x),x)),f(x,f(x,x))))) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,x)) = f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))). f(f(x,f(x,x)),f(x,x)) = x. f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))) = f(x,x). f(f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))),x) = f(x,f(x,x)). f(f(x,x),x) = f(x,f(x,x)). f(f(f(x,f(x,f(x,x))),x),x) = f(x,f(f(x,x),x)). f(f(f(x,f(x,f(x,x))),x),x) = f(x,f(x,f(x,x))). f(f(f(x,f(f(f(x,f(x,f(x,f(x,x)))),x),x)),x),x) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,f(x,f(x,x))),x),x) = f(f(x,f(x,f(f(x,x),x))),x). f(x,f(x,f(x,x))) = f(f(x,f(x,f(f(x,x),x))),x). f(x,f(x,f(x,x))) = f(f(x,f(x,f(x,f(x,x)))),x). f(f(x,f(x,f(x,f(x,x)))),x) = f(x,f(x,f(x,x))). f(f(x,f(x,f(x,f(f(x,f(x,f(x,f(x,x)))),x)))),x) = f(f(x,f(x,f(f(x,x),x))),x). f(f(x,f(x,f(x,f(x,f(x,f(x,x)))))),x) = f(f(x,f(x,f(f(x,x),x))),x). f(f(x,f(x,f(x,f(x,f(x,f(x,x)))))),x) = f(f(x,f(x,f(x,f(x,x)))),x). f(f(x,f(x,f(x,f(x,f(x,f(x,x)))))),x) = f(x,f(x,f(x,x))). f(f(f(x,x),f(x,f(x,x))),f(f(f(x,f(x,f(x,f(x,x)))),x),f(y,f(x,x)))) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,f(x,x))),f(y,f(x,x)))) = f(f(x,f(x,f(f(x,x),x))),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,f(x,x))),f(y,f(x,x)))) = f(f(x,f(x,f(x,f(x,x)))),x). f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,f(x,x))),f(y,f(x,x)))) = f(x,f(x,f(x,x))). f(f(f(x,f(x,f(x,f(x,x)))),x),f(x,x)) = x. f(f(x,f(x,f(x,x))),f(x,x)) = x. f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(f(x,x),x))))) = f(x,f(f(x,x),x)). f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(x,f(x,x)))))) = f(x,f(f(x,x),x)). f(x,f(f(x,f(x,f(x,x))),f(y,f(x,f(x,f(x,x)))))) = f(x,f(x,f(x,x))). f(f(f(f(x,f(x,f(x,x))),x),f(x,f(f(x,x),x))),x) = f(x,f(f(x,x),x)). f(f(f(f(x,f(x,f(x,x))),x),f(x,f(x,f(x,x)))),x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(f(x,x),x)). f(x,x) = f(x,f(x,f(x,x))). f(x,f(x,f(x,x))) = f(x,x). f(x,f(f(x,x),f(y,f(x,f(x,f(x,x)))))) = f(x,f(x,f(x,x))). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,f(x,f(x,x))). f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). f(f(x,x),f(x,x)) = x. f(f(f(x,x),f(x,f(x,x))),f(f(x,x),f(y,f(x,x)))) = f(x,f(x,f(x,x))). f(f(f(x,x),f(x,f(x,x))),f(f(x,x),f(y,f(x,x)))) = f(x,x). f(f(x,f(x,f(x,f(x,x)))),x) = f(x,f(x,f(x,x))). f(f(x,f(x,x)),x) = f(x,f(x,f(x,x))). f(f(x,f(x,x)),x) = f(x,x). f(f(f(x,f(x,x)),x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(x,x),y) = f(f(x,x),f(f(y,f(x,x)),f(x,x))). f(f(x,x),f(f(y,f(x,x)),f(x,x))) = f(f(x,x),y). f(f(f(x,f(f(y,x)