============================== Prover9 =============================== Prover9 (32) version Aug-2007, Aug 2007. Process 17624 was started by mccune on cleo, Tue Aug 7 10:07:39 2007 The command was "/home/mccune/LADR/bin/prover9 -f MOL-A.in MOL-A-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MOL-A.in assign(max_seconds,120). assign(max_weight,60). assign(new_constants,1). set(lex_order_vars). set(restrict_denials). formulas(sos). f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x # label(MOL_SS). end_of_list. formulas(goals). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS). end_of_list. % Reading from file MOL-A-interp.outx list(interpretations). interpretation(8,[number = 1,seconds = 0],[function(A,[2]),function(B,[4]),function(C,[6]),function(f(_,_),[1,1,1,1,1,1,1,1,1,0,3,2,5,4,7,6,1,3,3,1,3,1,7,1,1,2,1,2,1,4,1,2,1,5,3,1,5,1,5,1,1,4,1,4,1,4,1,6,1,7,7,1,5,1,7,1,1,6,1,2,1,6,1,6])]). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, f ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). not interpretable: c1 % Clause contains symbol not in interpretation: % f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. restricted denial: (wt=19): 3 f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 3 f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. end_of_list. formulas(sos). 2 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. end_of_list. formulas(demodulators). 2 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=25): 2 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. given #2 (A,wt=57): 4 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(y,w)))) = y. [para(2(a,1),2(a,1,2,1))]. given #3 (T,wt=9): 11 f(f(x,y),f(y,y)) = y. [para(4(a,1),4(a,1,2,2))]. given #4 (T,wt=11): 20 f(f(x,f(y,y)),y) = f(y,y). [para(11(a,1),11(a,1,2))]. given #5 (T,wt=13): 8 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(4(a,1),2(a,1,2,2))]. given #6 (T,wt=11): 32 f(f(f(x,x),y),x) = f(x,x). [para(8(a,1),11(a,1,1)),rewrite([8(7)]),flip(a)]. given #7 (A,wt=53): 5 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),f(f(z,x),v5)))) = f(z,x). [para(2(a,1),2(a,1,2,2,1,1,1,1))]. given #8 (T,wt=9): 40 f(f(x,y),f(x,x)) = x. [para(11(a,1),32(a,1,1,1)),rewrite([11(6)])]. given #9 (T,wt=13): 55 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(2(a,1),40(a,1,1))]. given #10 (T,wt=13): 61 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(40(a,1),40(a,1,1))]. given #11 (T,wt=15): 22 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(14),rewrite([20(7)])]. given #12 (A,wt=57): 6 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),y),f(y,w)))) = y. [para(2(a,1),2(a,1,2,2,1,1,1))]. given #13 (F,wt=27): 53 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(false). [para(40(a,1),2(a,1,2,2,1,1))]. given #14 (F,wt=27): 113 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(z,y)))) = y # label(false). [para(55(a,1),53(a,1,2,2,2))]. given #15 (F,wt=33): 112 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(y,z)))) = y # label(false). [para(55(a,1),53(a,1,2,1,2,1)),rewrite([55(10),55(13)])]. given #16 (F,wt=33): 114 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z)))) = x # label(false). [para(61(a,1),53(a,1,2,1,2,1)),rewrite([61(10),61(13)])]. given #17 (T,wt=15): 85 f(f(x,y),f(y,f(f(y,y),f(z,y)))) = y. [para(55(a,1),22(a,1,2,2,2))]. given #18 (T,wt=17): 81 f(x,f(f(x,x),f(x,f(f(x,x),y)))) = f(x,x). [para(11(a,1),22(a,1,1)),rewrite([40(4)])]. given #19 (T,wt=17): 159 f(x,f(f(x,x),f(x,f(y,f(x,x))))) = f(x,x). [para(11(a,1),85(a,1,1)),rewrite([40(4)])]. given #20 (T,wt=21): 17 f(f(x,f(y,y)),f(f(y,y),f(y,f(f(y,y),z)))) = f(y,y). [para(11(a,1),2(a,1,2,2,1)),rewrite([11(5)])]. given #21 (A,wt=35): 7 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z). [para(2(a,1),2(a,1,2,2,2))]. given #22 (F,wt=33): 134 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(z,y)))) = y # label(false). [para(55(a,1),113(a,1,2,1,2,1)),rewrite([55(10),55(13)])]. given #23 (F,wt=33): 135 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(z,x)))) = x # label(false). [para(61(a,1),113(a,1,2,1,2,1)),rewrite([61(10),61(13)])]. given #24 (F,wt=33): 192 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(false). [para(11(a,1),7(a,1,2,2,1,1,1,1))]. given #25 (F,wt=31): 238 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [para(40(a,1),192(a,1,2,2,1,1))]. given #26 (T,wt=21): 37 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x. [para(32(a,1),2(a,1,2,2,1,1))]. given #27 (T,wt=21): 82 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x. [para(22(a,1),32(a,1)),flip(a)]. given #28 (T,wt=13): 259 f(x,f(f(x,x),f(x,y))) = f(x,x). [para(82(a,1),11(a,1,1)),rewrite([82(9)]),flip(a)]. given #29 (T,wt=13): 272 f(f(x,x),f(x,f(f(x,x),y))) = x. [para(11(a,1),259(a,1,2,1)),rewrite([40(8)])]. given #30 (A,wt=35): 9 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(x,z)))),x),f(x,u)))) = x. [para(2(a,1),4(a,1,2,2,1,1,1))]. given #31 (F,wt=35): 100 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x) # label(false). [para(11(a,1),53(a,1,2,1,2,1)),rewrite([11(9),11(11)])]. given #32 (F,wt=35): 109 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),f(f(x,y),z)))) = f(x,y) # label(false). [para(40(a,1),53(a,1,2,1,2,1)),rewrite([40(9),40(11)])]. given #33 (F,wt=31): 309 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),x))) = f(x,y) # label(false). [para(40(a,1),109(a,1,2,2,2))]. given #34 (F,wt=35): 123 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [para(11(a,1),113(a,1,2,1,2,1)),rewrite([11(9),11(11)])]. given #35 (T,wt=13): 275 f(x,f(f(x,x),f(y,x))) = f(x,x). [para(55(a,1),259(a,1,2,2))]. given #36 (T,wt=13): 283 f(f(x,x),f(x,f(y,f(x,x)))) = x. [para(55(a,1),272(a,1,2,2))]. given #37 (T,wt=19): 340 f(f(f(f(x,x),x),f(f(x,x),x)),x) = f(f(x,x),x). [para(192(a,1),283(a,1,2,2)),rewrite([246(13),32(14),40(11)]),flip(a)]. given #38 (T,wt=21): 104 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(20(a,1),53(a,1,2,2,1)),rewrite([55(9)])]. given #39 (A,wt=31): 12 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(z,x)),y),y),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(11(a,1),2(a,1,1)),rewrite([11(3)])]. given #40 (F,wt=35): 132 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y) # label(false). [para(40(a,1),113(a,1,2,1,2,1)),rewrite([40(9),40(11)])]. given #41 (F,wt=39): 99 f(f(x,f(y,y)),f(f(y,f(f(f(y,y),x),f(f(y,y),x))),f(f(f(f(y,y),x),f(y,y)),f(f(y,y),z)))) = f(y,y) # label(false). [para(11(a,1),53(a,1,2,1,1))]. given #42 (F,wt=39): 122 f(f(x,f(y,y)),f(f(y,f(f(f(y,y),x),f(f(y,y),x))),f(f(f(f(y,y),x),f(y,y)),f(z,f(y,y))))) = f(y,y) # label(false). [para(11(a,1),113(a,1,2,1,1))]. given #43 (F,wt=41): 97 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(f(y,z),x),f(f(y,z),x))),f(f(f(f(y,z),x),f(y,z)),z))) = f(y,z) # label(false). [para(2(a,1),53(a,1,2,2,2))]. given #44 (T,wt=15): 364 f(f(x,f(f(x,x),x)),x) = f(f(x,x),x). [para(104(a,1),109(a,1,2,2,2)),rewrite([40(3),40(11),340(9),32(10),11(7)])]. given #45 (T,wt=19): 358 f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)) = x. [para(104(a,1),55(a,1,2,1)),rewrite([104(15),104(17)])]. given #46 (T,wt=19): 415 f(f(f(x,x),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(11(a,1),364(a,1,1,2,1)),rewrite([40(9)])]. given #47 (T,wt=19): 428 f(f(f(f(x,x),x),f(x,f(f(x,x),y))),x) = f(x,x). [para(11(a,1),358(a,1,1,1,2)),rewrite([40(5),40(9)])]. given #48 (A,wt=33): 13 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(11(a,1),2(a,1,2,1,1))]. given #49 (F,wt=39): 407 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(f(f(y,y),y),f(f(f(y,y),y),f(y,z)))))) = y # label(false). [para(37(a,1),97(a,1,1,2)),rewrite([37(10),37(10),37(11),37(12),37(15),37(16),37(27)])]. given #50 (F,wt=39): 468 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(f(f(y,y),y),f(f(f(y,y),y),f(z,y)))))) = y # label(false). [para(55(a,1),407(a,1,2,2,2,2,2))]. given #51 (F,wt=41): 110 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(f(y,z),x),f(f(y,z),x))),f(f(f(f(y,z),x),f(y,z)),y))) = f(y,z) # label(false). [para(40(a,1),53(a,1,2,2,2))]. given #52 (F,wt=41): 236 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),x),f(f(f(x,x),f(y,f(x,x))),f(x,x)))) = f(y,f(x,x)) # label(false). [para(32(a,1),192(a,1,2,2,1,1)),rewrite([40(3)])]. given #53 (T,wt=19): 432 f(f(f(x,f(x,x)),f(f(x,x),f(y,x))),f(x,x)) = x. [para(55(a,1),358(a,1,1,2,2))]. given #54 (T,wt=19): 437 f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x) = f(x,x). [para(55(a,1),428(a,1,1,2,2))]. given #55 (T,wt=19): 451 f(f(f(x,x),f(f(x,x),x)),f(x,x)) = f(f(x,x),x). [para(13(a,1),123(a,1,2))]. given #56 (T,wt=15): 519 f(f(x,f(x,f(x,x))),x) = f(x,f(x,x)). [para(11(a,1),451(a,1,1,1)),rewrite([40(3),40(6),40(7)])]. given #57 (A,wt=37): 15 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(11(a,1),2(a,1,2,2,1,1,1,1))]. given #58 (F,wt=41): 308 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),x),f(f(f(x,x),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y) # label(false). [para(32(a,1),109(a,1,2,2,2)),rewrite([40(3),40(11)])]. given #59 (F,wt=45): 103 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),x),f(f(f(x,x),f(y,f(x,x))),f(f(y,f(x,x)),z)))) = f(y,f(x,x)) # label(false). [para(20(a,1),53(a,1,2,1,2,1)),rewrite([20(12),40(11),20(12)])]. given #60 (F,wt=45): 106 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),x),f(f(f(x,x),f(f(x,x),y)),f(f(f(x,x),y),z)))) = f(f(x,x),y) # label(false). [para(32(a,1),53(a,1,2,1,2,1)),rewrite([32(12),40(11),32(12)])]. given #61 (F,wt=45): 127 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),x),f(f(f(x,x),f(y,f(x,x))),f(z,f(y,f(x,x)))))) = f(y,f(x,x)) # label(false). [para(20(a,1),113(a,1,2,1,2,1)),rewrite([20(12),40(11),20(12)])]. given #62 (T,wt=21): 124 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x. [para(11(a,1),113(a,1,2,1,2))]. given #63 (T,wt=21): 128 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(20(a,1),113(a,1,2,2,1)),rewrite([55(9)])]. given #64 (T,wt=21): 252 f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x)) = x. [para(37(a,1),55(a,1,2,1)),rewrite([37(16),37(18)])]. given #65 (T,wt=21): 271 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)). [para(2(a,1),259(a,1,2,2))]. given #66 (A,wt=25): 16 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y. [para(11(a,1),2(a,1,2,2,1,1,1))]. given #67 (F,wt=45): 130 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),x),f(f(f(x,x),f(f(x,x),y)),f(z,f(f(x,x),y))))) = f(f(x,x),y) # label(false). [para(32(a,1),113(a,1,2,1,2,1)),rewrite([32(12),40(11),32(12)])]. given #68 (F,wt=45): 195 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),z),f(f(f(f(f(x,x),z),z),f(y,f(x,x))),f(x,x)))) = f(y,f(x,x)) # label(false). [para(20(a,1),7(a,1,2,2,1,1,1,1))]. given #69 (F,wt=45): 467 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(f(f(y,y),y),f(f(f(y,y),y),f(y,z)))))) = y # label(false). [para(55(a,1),407(a,1,2,1,2,1)),rewrite([55(10),55(13)])]. given #70 (F,wt=45): 469 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,z)))))) = x # label(false). [para(61(a,1),407(a,1,2,1,2,1)),rewrite([61(10),61(13)])]. given #71 (T,wt=21): 274 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)). [para(40(a,1),259(a,1,2,2))]. given #72 (T,wt=21): 342 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(y,x)))) = x. [back_rewrite(224),rewrite([340(6)])]. given #73 (T,wt=19): 637 f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(342(a,1),55(a,1,2,1)),rewrite([342(15),342(17)])]. given #74 (T,wt=19): 648 f(f(f(x,f(x,x)),f(x,f(y,f(x,x)))),x) = f(x,x). [para(11(a,1),637(a,1,1,1,1)),rewrite([40(5),40(9)])]. given #75 (A,wt=29): 23 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,f(z,f(x,x))),y),y),x),f(x,u)))) = x. [para(20(a,1),2(a,1,1))]. given #76 (F,wt=45): 489 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(f(f(y,y),y),f(f(f(y,y),y),f(z,y)))))) = y # label(false). [para(55(a,1),468(a,1,2,1,2,1)),rewrite([55(10),55(13)])]. given #77 (F,wt=45): 490 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(f(f(x,x),x),f(f(f(x,x),x),f(z,x)))))) = x # label(false). [para(61(a,1),468(a,1,2,1,2,1)),rewrite([61(10),61(13)])]. given #78 (F,wt=47): 621 f(f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [para(16(a,1),97(a,1,2,1,2,1)),rewrite([16(25),16(27)])]. given #79 (F,wt=47): 669 f(f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(z,x))),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [para(55(a,1),621(a,1,1,1,2,2))]. given #80 (T,wt=19): 650 f(f(f(x,f(x,x)),f(x,f(f(x,x),x))),x) = f(x,x). [para(451(a,1),637(a,1,1,2,2)),rewrite([40(3),40(5),40(9)])]. given #81 (T,wt=21): 343 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(x,y)))) = x. [back_rewrite(144),rewrite([340(6)])]. given #82 (T,wt=19): 681 f(f(f(f(x,x),x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(343(a,1),55(a,1,2,1)),rewrite([343(15),343(17)])]. given #83 (T,wt=19): 693 f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),x) = f(x,x). [para(11(a,1),681(a,1,1,1,1)),rewrite([40(5),40(9)])]. given #84 (A,wt=49): 24 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),z),f(f(f(f(f(x,x),z),z),f(y,f(x,x))),f(f(y,f(x,x)),u)))) = f(y,f(x,x)). [para(20(a,1),2(a,1,2,2,1,1,1,1))]. given #85 (F,wt=49): 143 f(f(f(f(x,f(y,y)),f(x,f(y,y))),f(y,y)),f(f(y,f(f(x,f(y,y)),f(x,f(y,y)))),f(f(f(x,f(y,y)),f(y,y)),f(f(y,y),z)))) = f(y,y) # label(false). [para(11(a,1),112(a,1,2,1,1))]. given #86 (F,wt=49): 150 f(f(f(f(f(x,x),y),f(f(x,x),y)),f(x,x)),f(f(x,f(f(f(x,x),y),f(f(x,x),y))),f(f(f(f(x,x),y),f(x,x)),f(f(x,x),z)))) = f(x,x) # label(false). [para(11(a,1),114(a,1,2,1,1))]. given #87 (F,wt=49): 223 f(f(f(f(x,f(y,y)),f(x,f(y,y))),f(y,y)),f(f(y,f(f(x,f(y,y)),f(x,f(y,y)))),f(f(f(x,f(y,y)),f(y,y)),f(z,f(y,y))))) = f(y,y) # label(false). [para(11(a,1),134(a,1,2,1,1))]. given #88 (F,wt=49): 231 f(f(f(f(f(x,x),y),f(f(x,x),y)),f(x,x)),f(f(x,f(f(f(x,x),y),f(f(x,x),y))),f(f(f(f(x,x),y),f(x,x)),f(z,f(x,x))))) = f(x,x) # label(false). [para(11(a,1),135(a,1,2,1,1))]. given #89 (T,wt=21): 347 f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(11(a,1),340(a,1,1,1,1)),rewrite([40(5),40(10)])]. given #90 (T,wt=21): 562 f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(x,x)) = x. [para(124(a,1),55(a,1,2,1)),rewrite([124(16),124(18)])]. given #91 (T,wt=19): 718 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(562(a,1),16(a,1,2,2,1)),rewrite([11(4),40(3),55(6)])]. given #92 (T,wt=19): 720 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(11(a,1),718(a,1,2,1,1)),rewrite([40(7),40(11)])]. given #93 (A,wt=25): 25 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(f(x,x),x),y),f(y,z)))) = y. [para(20(a,1),2(a,1,2,2,1,1,1))]. given #94 (F,wt=49): 401 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [para(53(a,1),97(a,1,2,1,2,1)),rewrite([53(27),53(29)])]. given #95 (F,wt=49): 403 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(z,x))),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [para(113(a,1),97(a,1,2,1,2,1)),rewrite([113(27),113(29)])]. given #96 (F,wt=51): 141 f(f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(x,f(y,z)),f(x,f(y,z)))),f(f(f(x,f(y,z)),f(y,z)),z))) = f(y,z) # label(false). [para(2(a,1),112(a,1,2,2,2))]. given #97 (F,wt=51): 146 f(f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(x,f(y,z)),f(x,f(y,z)))),f(f(f(x,f(y,z)),f(y,z)),y))) = f(y,z) # label(false). [para(40(a,1),112(a,1,2,2,2))]. given #98 (T,wt=19): 721 f(x,f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(55(a,1),718(a,1,2,2,2))]. given #99 (T,wt=19): 732 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(55(a,1),720(a,1,2,2,2))]. given #100 (T,wt=21): 657 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(y,f(x,x)))))) = x. [para(648(a,1),274(a,1,1)),rewrite([648(8),648(9),40(4),648(16),648(17),40(12)])]. given #101 (T,wt=21): 702 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y))))) = x. [para(693(a,1),274(a,1,1)),rewrite([693(8),693(9),40(4),693(16),693(17),40(12)])]. given #102 (A,wt=29): 35 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,f(f(x,x),z)),y),y),x),f(x,u)))) = x. [para(32(a,1),2(a,1,1))]. given #103 (F,wt=51): 149 f(f(f(f(f(x,y),z),f(f(x,y),z)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(f(f(x,y),z),f(f(x,y),z))),f(f(f(f(x,y),z),f(x,y)),y))) = f(x,y) # label(false). [para(2(a,1),114(a,1,2,2,2))]. given #104 (F,wt=51): 153 f(f(f(f(f(x,y),z),f(f(x,y),z)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(f(f(x,y),z),f(f(x,y),z))),f(f(f(f(x,y),z),f(x,y)),x))) = f(x,y) # label(false). [para(40(a,1),114(a,1,2,2,2))]. given #105 (F,wt=51): 459 f(f(x,f(y,y)),f(f(y,f(f(f(y,y),x),f(f(y,y),x))),f(f(f(f(y,y),x),f(y,y)),f(f(y,f(y,y)),f(f(y,f(y,y)),f(f(y,y),z)))))) = f(y,y) # label(false). [para(11(a,1),407(a,1,2,1,1)),rewrite([40(15),40(17)])]. given #106 (F,wt=51): 481 f(f(x,f(y,y)),f(f(y,f(f(f(y,y),x),f(f(y,y),x))),f(f(f(f(y,y),x),f(y,y)),f(f(y,f(y,y)),f(f(y,f(y,y)),f(z,f(y,y))))))) = f(y,y) # label(false). [para(11(a,1),468(a,1,2,1,1)),rewrite([40(15),40(17)])]. given #107 (T,wt=23): 101 f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(11(a,1),53(a,1,2,2,1)),rewrite([40(5),55(8)])]. given #108 (T,wt=23): 125 f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(11(a,1),113(a,1,2,2,1)),rewrite([40(5),55(8)])]. given #109 (T,wt=23): 142 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [para(11(a,1),112(a,1,1,1,1)),rewrite([11(3),40(3),40(3),11(3),11(3),11(5)])]. given #110 (T,wt=23): 222 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [para(11(a,1),134(a,1,1,1,1)),rewrite([11(3),40(3),40(3),11(3),11(3),11(5)])]. given #111 (A,wt=49): 36 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),z),f(f(f(f(f(x,x),z),z),f(f(x,x),y)),f(f(f(x,x),y),u)))) = f(f(x,x),y). [para(32(a,1),2(a,1,2,2,1,1,1,1))]. given #112 (F,wt=45): 858 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),z),f(f(f(f(f(x,x),z),z),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y) # label(false). [para(32(a,1),36(a,1,2,2,2))]. given #113 (F,wt=25): 888 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),x))) = f(x,y) # label(false). [back_rewrite(309),rewrite([869(3)])]. given #114 (F,wt=25): 921 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(238),rewrite([870(3)])]. given #115 (F,wt=27): 875 f(x,f(f(f(f(x,y),f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),x))) = f(x,y) # label(false). [back_rewrite(863),rewrite([869(3)])]. given #116 (T,wt=9): 869 f(f(x,x),f(x,y)) = x. [para(428(a,1),858(a,1,2,2)),rewrite([40(4),259(4),40(5),40(8),40(13),20(11),40(3),40(4)]),flip(a)]. given #117 (T,wt=9): 870 f(f(x,x),f(y,x)) = x. [para(437(a,1),858(a,1,2,2)),rewrite([869(4),275(4),869(5),869(8),869(13),20(11),869(3),869(4)]),flip(a)]. given #118 (T,wt=11): 880 f(f(x,x),x) = f(x,f(x,x)). [back_rewrite(688),rewrite([869(5),32(3),870(4)]),flip(a)]. given #119 (T,wt=11): 1077 f(x,f(f(x,x),y)) = f(x,x). [para(11(a,1),869(a,1,1))]. given #120 (A,wt=49): 41 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),x))) = f(z,x). [para(2(a,1),5(a,1,2,2,2))]. given #121 (F,wt=25): 1052 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))) = y # label(false). [para(2(a,1),875(a,1,2,1,1,1)),rewrite([2(12),2(17),2(22)])]. given #122 (F,wt=25): 1185 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(y,x),y),y),y),f(y,z)))) = y # label(false). [para(880(a,1),2(a,1,2,1))]. given #123 (F,wt=25): 1232 f(f(x,y),f(y,f(f(f(f(f(x,y),f(y,z)),f(y,z)),y),f(x,y)))) = y # label(false). [para(869(a,1),1052(a,1,2,1))]. given #124 (F,wt=25): 1233 f(f(x,y),f(y,f(f(f(f(f(x,y),f(z,y)),f(z,y)),y),f(x,y)))) = y # label(false). [para(870(a,1),1052(a,1,2,1))]. given #125 (T,wt=11): 1154 f(x,f(y,f(x,x))) = f(x,x). [para(11(a,1),870(a,1,1))]. given #126 (T,wt=13): 1076 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(2(a,1),869(a,1,2))]. given #127 (T,wt=13): 1082 f(f(f(x,y),f(x,y)),x) = f(x,y). [para(40(a,1),869(a,1,2))]. given #128 (T,wt=21): 887 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = x. [back_rewrite(313),rewrite([869(4),869(4),880(3),869(7),880(5),869(12)])]. given #129 (A,wt=53): 43 f(f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),w)))) = f(y,x). [para(11(a,1),5(a,1,1,1,2,1,1,1))]. given #130 (F,wt=25): 1234 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(x,y),y),y),y),f(x,y)))) = y # label(false). [para(880(a,1),1052(a,1,2,1))]. given #131 (F,wt=25): 1243 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(x,y),y),y),y),f(y,z)))) = y # label(false). [para(55(a,1),1185(a,1,2,2,1,1,1,1)),rewrite([1076(4)])]. given #132 (F,wt=25): 1244 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(y,x),y),y),y),f(z,y)))) = y # label(false). [para(55(a,1),1185(a,1,2,2,2))]. given #133 (F,wt=25): 1245 f(f(x,y),f(f(x,f(x,x)),f(f(f(f(f(x,y),x),x),x),f(x,z)))) = x # label(false). [para(61(a,1),1185(a,1,2,2,1,1,1,1)),rewrite([1082(4)])]. given #134 (T,wt=21): 892 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = x. [back_rewrite(266),rewrite([869(4),869(4),880(3),869(7),880(5),869(8),869(12)])]. given #135 (T,wt=21): 982 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(x,x)) = x. [back_rewrite(562),rewrite([880(2),880(4)])]. given #136 (T,wt=21): 1024 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x)) = x. [back_rewrite(252),rewrite([880(2),880(4)])]. given #137 (T,wt=21): 1318 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,y)),x))) = f(x,y). [para(1076(a,1),875(a,1,2,1))]. given #138 (A,wt=25): 50 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(32(a,1),5(a,1,1)),rewrite([40(3),40(3)])]. given #139 (F,wt=25): 1340 f(f(x,y),f(x,f(f(f(f(f(x,y),f(x,z)),f(x,z)),x),f(x,y)))) = x # label(false). [para(1082(a,1),1232(a,1,1)),rewrite([1082(5),1082(11)])]. given #140 (F,wt=25): 1341 f(f(x,y),f(x,f(f(f(f(f(x,y),f(z,x)),f(z,x)),x),f(x,y)))) = x # label(false). [para(1082(a,1),1233(a,1,1)),rewrite([1082(5),1082(11)])]. given #141 (F,wt=25): 1381 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(x,y),y),y),y),f(z,y)))) = y # label(false). [para(55(a,1),1243(a,1,2,2,2))]. given #142 (F,wt=25): 1401 f(f(x,y),f(f(x,f(x,x)),f(f(f(f(f(x,y),x),x),x),f(z,x)))) = x # label(false). [para(61(a,1),1244(a,1,2,2,1,1,1,1)),rewrite([1082(4)])]. given #143 (T,wt=21): 1446 f(x,f(f(y,x),f(x,f(f(x,f(x,x)),f(y,x))))) = f(y,x). [back_rewrite(1115),rewrite([1443(6),1444(8)])]. given #144 (T,wt=21): 1455 f(x,f(f(x,y),f(x,f(f(x,f(x,x)),f(x,y))))) = f(x,y). [back_rewrite(1196),rewrite([1453(6),1454(8)])]. given #145 (T,wt=23): 576 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))),x) = f(x,x). [para(11(a,1),252(a,1,1,1,1)),rewrite([40(5),40(11)])]. given #146 (T,wt=23): 716 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x). [para(11(a,1),562(a,1,1,1,1)),rewrite([40(5),40(11)])]. given #147 (A,wt=35): 54 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),y))) = f(y,z). [para(40(a,1),2(a,1,2,2,2))]. given #148 (F,wt=27): 924 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(192),rewrite([870(3)])]. given #149 (F,wt=27): 1100 f(f(x,y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(y,z)))) = y # label(false). [para(869(a,1),143(a,1,1,1,1,2)),rewrite([869(4),869(6),1076(4),869(5),869(6),869(9),869(10),869(11),869(15)])]. given #150 (F,wt=27): 1101 f(f(x,y),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z)))) = x # label(false). [para(869(a,1),150(a,1,1,1,1,1)),rewrite([869(4),869(6),1082(4),869(5),869(6),869(9),869(10),869(11),869(15)])]. given #151 (F,wt=27): 1102 f(f(x,y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(z,y)))) = y # label(false). [para(869(a,1),223(a,1,1,1,1,2)),rewrite([869(4),869(6),1076(4),869(5),869(6),869(9),869(10),869(11),869(15)])]. given #152 (T,wt=21): 1642 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),x))) = f(y,x). [para(1082(a,1),924(a,1,2,1))]. given #153 (T,wt=23): 959 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [back_rewrite(738),rewrite([880(4)])]. given #154 (T,wt=23): 1447 f(f(f(x,f(x,x)),f(y,x)),x) = f(x,f(f(x,f(x,x)),f(y,x))). [back_rewrite(1443),rewrite([1444(12)])]. given #155 (T,wt=23): 1456 f(f(f(x,f(x,x)),f(x,y)),x) = f(x,f(f(x,f(x,x)),f(x,y))). [back_rewrite(1453),rewrite([1454(12)])]. given #156 (A,wt=55): 57 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),w)))) = f(y,x). [para(40(a,1),5(a,1,1,1,2,1,1))]. given #157 (F,wt=27): 1103 f(f(x,y),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(z,x)))) = x # label(false). [para(869(a,1),231(a,1,1,1,1,1)),rewrite([869(4),869(6),1082(4),869(5),869(6),869(9),869(10),869(11),869(15)])]. given #158 (F,wt=29): 894 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y) # label(false). [back_rewrite(132),rewrite([869(3)])]. given #159 (F,wt=29): 895 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),f(f(x,y),z)))) = f(x,y) # label(false). [back_rewrite(109),rewrite([869(3)])]. given #160 (F,wt=29): 925 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [back_rewrite(123),rewrite([870(3)])]. given #161 (T,wt=23): 1697 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [para(55(a,1),959(a,1,1,2,2))]. given #162 (T,wt=23): 1702 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(959(a,1),1082(a,1,1,1)),rewrite([959(10),959(20)])]. given #163 (T,wt=23): 1785 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [para(1697(a,1),1082(a,1,1,1)),rewrite([1697(10),1697(20)])]. given #164 (T,wt=25): 66 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y. [para(55(a,1),2(a,1,2,2,2))]. given #165 (A,wt=51): 59 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),f(x,x)),f(f(x,f(z,x)),f(f(z,x),w)))) = f(z,x). [para(40(a,1),5(a,1,2,2,1,1))]. given #166 (F,wt=29): 926 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x) # label(false). [back_rewrite(100),rewrite([870(3)])]. given #167 (F,wt=29): 1110 f(x,f(f(x,y),f(f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y)),x))) = f(x,y) # label(false). [para(869(a,1),875(a,1,2,1))]. given #168 (F,wt=29): 1170 f(x,f(f(x,y),f(f(f(f(x,f(z,f(x,y))),f(z,f(x,y))),f(x,y)),x))) = f(x,y) # label(false). [para(870(a,1),875(a,1,2,1))]. given #169 (F,wt=29): 1271 f(x,f(f(y,x),f(f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x)),x))) = f(y,x) # label(false). [para(870(a,1),1232(a,1,1)),rewrite([870(4),870(12)])]. given #170 (T,wt=25): 67 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = x. [para(2(a,1),55(a,1,2,1)),rewrite([2(20),2(22)])]. given #171 (T,wt=25): 611 f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [para(16(a,1),55(a,1,2,1)),rewrite([16(20),16(22)])]. given #172 (T,wt=25): 613 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(z,y)))) = y. [para(55(a,1),16(a,1,2,2,2))]. given #173 (T,wt=25): 889 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(307),rewrite([869(3)])]. given #174 (A,wt=49): 60 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),z))) = f(z,x). [para(40(a,1),5(a,1,2,2,2))]. given #175 (F,wt=29): 1282 f(x,f(f(y,x),f(f(f(f(x,f(z,f(y,x))),f(z,f(y,x))),f(y,x)),x))) = f(y,x) # label(false). [para(870(a,1),1233(a,1,1)),rewrite([870(4),870(12)])]. given #176 (F,wt=29): 1299 f(f(x,f(y,z)),f(f(y,z),f(f(f(f(f(f(y,z),x),z),z),f(y,z)),z))) = f(y,z) # label(false). [para(1076(a,1),7(a,1,2,1))]. given #177 (F,wt=29): 1620 f(f(x,f(y,z)),f(f(y,z),f(f(f(f(f(f(y,z),x),y),y),f(y,z)),y))) = f(y,z) # label(false). [para(1082(a,1),54(a,1,2,1))]. given #178 (F,wt=29): 2062 f(f(x,f(y,z)),f(f(y,z),f(f(f(f(f(x,f(y,z)),z),z),f(y,z)),z))) = f(y,z) # label(false). [para(55(a,1),1299(a,1,2,2,1,1,1,1)),rewrite([1076(7)])]. given #179 (T,wt=21): 2061 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,y)),y))) = f(x,y). [para(40(a,1),1299(a,1,2,2,1,1,1,1)),rewrite([869(3)])]. given #180 (T,wt=21): 2096 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),y))) = f(y,x). [para(11(a,1),1620(a,1,2,2,1,1,1,1)),rewrite([870(3)])]. given #181 (T,wt=25): 891 f(f(x,y),f(y,f(f(f(f(y,x),f(f(y,x),f(y,x))),y),f(y,z)))) = y. [back_rewrite(270),rewrite([869(8),869(4),869(10),880(6)])]. given #182 (T,wt=19): 2232 f(f(x,y),f(f(f(y,x),f(f(y,x),f(y,x))),y)) = y. [para(1154(a,1),891(a,1,2,2)),rewrite([55(15)])]. given #183 (A,wt=45): 63 f(f(x,y),f(f(z,f(y,y)),f(f(f(f(f(y,x),f(f(z,f(y,y)),f(z,f(y,y)))),f(f(z,f(y,y)),f(z,f(y,y)))),y),f(y,u)))) = y. [para(55(a,1),2(a,1,2,1))]. given #184 (F,wt=25): 2134 f(f(x,y),f(y,f(f(f(f(f(x,y),f(y,z)),f(y,z)),y),f(y,z)))) = y # label(false). [para(869(a,1),2062(a,1,1,2)),rewrite([869(4),869(4),869(9),869(14)])]. given #185 (F,wt=25): 2135 f(f(x,y),f(y,f(f(f(f(f(x,y),f(z,y)),f(z,y)),y),f(z,y)))) = y # label(false). [para(870(a,1),2062(a,1,1,2)),rewrite([870(4),870(4),870(9),870(14)])]. given #186 (F,wt=25): 2475 f(f(x,y),f(x,f(f(f(f(f(x,y),f(x,z)),f(x,z)),x),f(x,z)))) = x # label(false). [para(1082(a,1),2134(a,1,1)),rewrite([1082(5)])]. given #187 (F,wt=25): 2502 f(f(x,y),f(x,f(f(f(f(f(x,y),f(z,x)),f(z,x)),x),f(z,x)))) = x # label(false). [para(1082(a,1),2135(a,1,1)),rewrite([1082(5)])]. given #188 (T,wt=15): 2277 f(x,f(f(x,f(x,x)),f(y,x))) = f(y,x). [para(11(a,1),2232(a,1,2,1,1)),rewrite([870(3),11(3),11(3)])]. given #189 (T,wt=15): 2280 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y). [para(40(a,1),2232(a,1,2,1,1)),rewrite([869(3),40(3),40(3)])]. given #190 (T,wt=15): 2370 f(f(f(x,f(x,x)),f(y,x)),x) = f(y,x). [back_rewrite(1447),rewrite([2277(10)])]. given #191 (T,wt=15): 2401 f(f(f(x,f(x,x)),f(x,y)),x) = f(x,y). [back_rewrite(1456),rewrite([2280(10)])]. given #192 (A,wt=45): 65 f(f(x,y),f(f(f(y,y),f(f(z,f(y,x)),f(z,f(y,x)))),f(f(f(f(z,f(y,x)),f(f(z,f(y,x)),f(z,f(y,x)))),y),f(y,u)))) = y. [para(55(a,1),2(a,1,2,2,1,1,1))]. given #193 (F,wt=27): 2361 f(x,f(f(f(f(x,f(x,x)),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(1712),rewrite([2277(11),2277(16)])]. given #194 (F,wt=27): 2393 f(x,f(f(f(f(x,f(x,x)),f(x,y)),f(x,x)),f(f(x,f(x,y)),x))) = f(x,y) # label(false). [back_rewrite(1726),rewrite([2280(11),2280(16)])]. given #195 (F,wt=29): 2063 f(f(f(x,y),z),f(f(x,y),f(f(f(f(f(f(x,y),z),y),y),f(x,y)),y))) = f(x,y) # label(false). [para(61(a,1),1299(a,1,2,2,1,1,1,1)),rewrite([1082(7)])]. given #196 (F,wt=29): 2097 f(f(x,f(y,z)),f(f(y,z),f(f(f(f(f(x,f(y,z)),y),y),f(y,z)),y))) = f(y,z) # label(false). [para(55(a,1),1620(a,1,2,2,1,1,1,1)),rewrite([1076(7)])]. given #197 (T,wt=17): 2369 f(f(x,f(x,x)),f(y,x)) = f(f(y,x),f(y,x)). [back_rewrite(1448),rewrite([2277(5),2277(6)]),flip(a)]. given #198 (T,wt=15): 2730 f(x,f(f(y,f(y,y)),f(x,y))) = f(x,y). [para(2369(a,2),61(a,1,2))]. given #199 (T,wt=15): 2808 f(f(f(x,f(x,x)),f(y,x)),y) = f(y,x). [para(2369(a,2),1082(a,1,1))]. given #200 (T,wt=17): 2400 f(f(x,f(x,x)),f(x,y)) = f(f(x,y),f(x,y)). [back_rewrite(1457),rewrite([2280(5),2280(6)]),flip(a)]. given #201 (A,wt=57): 68 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),y),f(y,w)))) = y. [para(55(a,1),4(a,1,2,2,1,1,1,2,2,2)),rewrite([55(22)])]. given #202 (F,wt=11): 2959 f(f(x,f(y,x)),x) = f(y,x) # label(false). [back_rewrite(2681),rewrite([2953(5),2952(10),2730(11),2277(7)])]. given #203 (F,wt=11): 3353 f(f(f(x,y),x),f(x,y)) = x # label(false). [para(869(a,1),2959(a,1,1,2)),rewrite([869(7)])]. given #204 (F,wt=11): 3354 f(f(f(x,y),y),f(x,y)) = y # label(false). [para(870(a,1),2959(a,1,1,2)),rewrite([870(7)])]. given #205 (F,wt=11): 3360 f(f(x,f(x,y)),x) = f(x,y) # label(false). [para(1082(a,1),2959(a,1,1,2)),rewrite([1082(7)])]. given #206 (T,wt=13): 3365 f(x,f(f(x,y),f(y,x))) = f(x,y). [para(1318(a,1),2959(a,1,1,2)),rewrite([3354(5),3354(10),3353(9),3354(6)]),flip(a)]. given #207 (T,wt=15): 3102 f(x,f(f(y,f(y,y)),f(y,x))) = f(y,x). [para(2400(a,2),55(a,1,2))]. given #208 (T,wt=15): 3165 f(f(f(x,f(x,x)),f(x,y)),y) = f(x,y). [para(2400(a,2),1076(a,1,1))]. given #209 (T,wt=17): 2793 f(f(f(x,y),f(f(x,y),f(x,y))),x) = f(x,x). [para(869(a,1),2369(a,1,2)),rewrite([869(9),869(9)])]. given #210 (A,wt=57): 69 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(w,y)))) = y. [para(55(a,1),4(a,1,2,2,2))]. given #211 (F,wt=11): 3528 f(f(x,y),f(y,f(x,y))) = y # label(false). [para(2959(a,1),3353(a,1,1))]. given #212 (F,wt=11): 3529 f(x,f(f(x,y),x)) = f(x,y) # label(false). [para(3353(a,1),3353(a,1,1))]. given #213 (F,wt=11): 3601 f(x,f(f(y,x),x)) = f(y,x) # label(false). [para(3354(a,1),3353(a,1,1))]. given #214 (F,wt=11): 3702 f(f(x,y),f(x,f(x,y))) = x # label(false). [para(3360(a,1),3353(a,1,1))]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(4128)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c_0, f ]). NOTE: sn=96, num_tables=180 NOTE: updating interpretation 1: c_0=1. not interpretable: c1 % Clause contains symbol not in interpretation: % f(c1,f(c_0,f(c2,c3))) != f(c2,f(c_0,f(c1,c3))) # answer(A_SS). [back_rewrite(3),rewrite([4509(8,R),4534(6),4509(15,R),4534(13)])]. restricted denial: (wt=15): 5472 f(c1,f(c_0,f(c2,c3))) != f(c2,f(c_0,f(c1,c3))) # answer(A_SS). [back_rewrite(3),rewrite([4509(8,R),4534(6),4509(15,R),4534(13)])]. given #215 (T,wt=7): 4301 f(x,f(x,x)) = c_0. [new_symbol(4128)]. given #216 (T,wt=7): 4509 f(x,c_0) = f(x,x). [back_rewrite(4161),rewrite([4301(2)])]. given #217 (T,wt=7): 4519 f(c_0,f(x,x)) = x. [back_rewrite(4150),rewrite([4301(2)])]. given #218 (T,wt=7): 4538 f(c_0,x) = f(x,x). [back_rewrite(4127),rewrite([4301(2)])]. given #219 (A,wt=27): 3411 f(x,f(f(y,x),f(f(f(f(x,y),f(f(x,y),f(y,x))),f(y,x)),x))) = f(y,x). [back_rewrite(2056),rewrite([3354(4),3354(7),3354(10),3354(15)])]. given #220 (F,wt=11): 4209 f(x,f(x,f(y,x))) = f(y,x) # label(false). [back_rewrite(2963),rewrite([4123(7),2402(8)])]. given #221 (F,wt=11): 4998 f(x,f(x,f(x,y))) = f(x,y) # label(false). [back_rewrite(4472),rewrite([4509(3,R),4534(3),4729(5),4537(6)])]. given #222 (F,wt=11): 5821 f(f(x,y),f(y,f(y,x))) = y # label(false). [back_rewrite(2814),rewrite([5474(3),5474(4),4998(4),5474(3)])]. given #223 (F,wt=17): 4091 f(f(x,y),f(y,f(f(y,f(y,x)),f(y,z)))) = y # label(false). [para(3702(a,1),2(a,1,2,2,1,1,1)),rewrite([869(5),3360(5)])]. given #224 (T,wt=7): 4819 f(x,f(c_0,c_0)) = c_0. [back_rewrite(2864),rewrite([4301(2),4509(5,R),4534(5),4619(6),4301(6)])]. given #225 (T,wt=7): 4990 f(f(c_0,c_0),x) = c_0. [back_rewrite(4395),rewrite([4470(5)])]. given #226 (T,wt=11): 4470 f(f(x,y),f(c_0,f(x,y))) = c_0. [back_rewrite(4219),rewrite([4301(3),4301(7)])]. given #227 (T,wt=11): 4534 f(f(x,y),c_0) = f(c_0,f(x,y)). [back_rewrite(4133),rewrite([4301(2),4301(6)]),flip(a)]. given #228 (A,wt=31): 3415 f(x,f(f(x,y),f(f(f(f(x,y),f(f(x,y),f(y,x))),f(x,x)),f(f(x,x),z)))) = f(x,x). [back_rewrite(1501),rewrite([3354(7)])]. given #229 (F,wt=17): 4116 f(f(x,y),f(y,f(f(y,f(y,x)),f(z,y)))) = y # label(false). [para(3702(a,1),66(a,1,2,2,1,1,1)),rewrite([869(5),3360(5)])]. given #230 (F,wt=17): 5000 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(z,y)))) = y # label(false). [back_rewrite(4374),rewrite([4509(5,R),4534(5),4619(6)])]. given #231 (F,wt=17): 5001 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(y,z)))) = y # label(false). [back_rewrite(4373),rewrite([4509(5,R),4534(5),4619(6)])]. given #232 (F,wt=17): 5074 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(z,x)))) = x # label(false). [back_rewrite(3691),rewrite([4509(8,R),4534(7),4756(8)])]. given #233 (T,wt=11): 4537 f(c_0,f(c_0,f(x,y))) = f(x,y). [back_rewrite(4129),rewrite([4301(2),4301(5),4534(5)])]. given #234 (T,wt=11): 4619 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_rewrite(3766),rewrite([4301(2),4538(2),4301(3),4301(4),4538(4),4301(5),4534(5),4519(5),4301(7)])]. given #235 (T,wt=11): 4719 f(f(c_0,f(x,y)),y) = f(x,y). [back_rewrite(3165),rewrite([4301(2)])]. given #236 (T,wt=11): 4729 f(f(c_0,f(x,y)),f(x,x)) = c_0. [back_rewrite(3124),rewrite([4301(3),4534(3),4301(5),4301(6),4513(8),4509(7,R),4534(7),4301(9),4534(9),4537(9),40(7),4538(5),4301(7)])]. given #237 (A,wt=41): 4093 f(f(x,y),f(f(f(y,y),f(x,f(f(x,f(x,y)),f(x,z)))),f(f(f(x,f(x,f(f(x,f(x,y)),f(x,z)))),y),f(y,u)))) = y. [para(3702(a,1),6(a,1,2,1,2,2,1,1,1)),rewrite([869(6),3360(6),869(12),3702(12),3360(12)])]. given #238 (F,wt=17): 5075 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(x,z)))) = x # label(false). [back_rewrite(3689),rewrite([4509(8,R),4534(7),4756(8)])]. given #239 (F,wt=17): 5087 f(f(x,y),f(c_0,f(f(x,f(x,y)),f(z,x)))) = x # label(false). [back_rewrite(3664),rewrite([4998(5),4998(6),4509(5,R),4534(5),4756(6)])]. given #240 (F,wt=17): 5089 f(f(x,y),f(c_0,f(f(x,f(x,y)),f(x,z)))) = x # label(false). [back_rewrite(3661),rewrite([4998(5),4998(6),4509(5,R),4534(5),4756(6)])]. given #241 (F,wt=17): 5098 f(f(x,y),f(y,f(f(y,f(x,y)),f(z,y)))) = y # label(false). [back_rewrite(3646),rewrite([4509(5,R),4534(5),4619(6),4989(4),4509(11,R),4534(11),4619(12),4989(10),4509(14,R),4534(9),4537(9)])]. given #242 (T,wt=11): 4738 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(3102),rewrite([4301(2)])]. given #243 (T,wt=11): 4756 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(3063),rewrite([4301(2),4538(2),4301(3),4301(4),4538(4),4301(5),4534(5),4519(5),4301(4),4509(4),4301(5),4534(5),4519(5),4301(7)])]. given #244 (T,wt=11): 4812 f(f(c_0,f(x,y)),f(y,y)) = c_0. [back_rewrite(2962),rewrite([4301(3),4534(3),4301(7)])]. given #245 (T,wt=11): 4825 f(f(c_0,f(x,y)),x) = f(x,y). [back_rewrite(2808),rewrite([4301(2)])]. given #246 (A,wt=25): 4100 f(f(x,f(y,z)),f(f(y,z),f(f(f(y,z),f(f(y,z),x)),z))) = f(y,z) # label(false). [para(3702(a,1),7(a,1,2,2,1,1,1)),rewrite([869(10),3360(11)])]. given #247 (F,wt=17): 5100 f(f(x,y),f(y,f(f(y,f(x,y)),f(y,z)))) = y # label(false). [back_rewrite(3644),rewrite([4509(5,R),4534(5),4619(6),4989(4),4509(11,R),4534(11),4619(12),4989(10),4509(14,R),4534(9),4537(9)])]. given #248 (F,wt=17): 5168 f(f(x,f(y,x)),f(c_0,f(f(y,x),f(z,x)))) = x # label(false). [back_rewrite(3379),rewrite([4509(8,R),4534(7),4756(8)])]. given #249 (F,wt=17): 5170 f(f(x,f(y,x)),f(c_0,f(f(y,x),f(x,z)))) = x # label(false). [back_rewrite(3376),rewrite([4509(8,R),4534(7),4756(8)])]. given #250 (F,wt=17): 5489 f(f(x,y),f(c_0,f(f(y,f(y,x)),f(y,z)))) = y # label(false). [back_rewrite(4735),rewrite([4756(6),5474(4)])]. given #251 (T,wt=11): 4831 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(2730),rewrite([4301(2)])]. given #252 (T,wt=11): 4989 f(f(x,y),y) = f(y,f(x,y)). [back_rewrite(3599),rewrite([4822(4),4362(6),3601(5),4509(5,R),4534(5),4739(6)]),flip(a)]. given #253 (T,wt=11): 5474 f(f(x,y),x) = f(x,f(x,y)). [back_rewrite(4532),rewrite([4534(4),4989(9),3702(9),4538(6),4729(6),4738(5)])]. given #254 (T,wt=11): 6246 f(x,f(c_0,f(y,f(x,x)))) = c_0. [para(11(a,1),4619(a,1,1))]. given #255 (A,wt=25): 4111 f(f(x,f(y,z)),f(f(y,z),f(f(f(y,z),f(f(y,z),x)),y))) = f(y,z) # label(false). [para(3702(a,1),54(a,1,2,2,1,1,1)),rewrite([869(10),3360(11)])]. given #256 (F,wt=17): 5490 f(f(x,y),f(c_0,f(f(y,f(y,x)),f(z,y)))) = y # label(false). [back_rewrite(4732),rewrite([4756(6),5474(4)])]. given #257 (F,wt=11): 6596 f(f(x,f(x,y)),f(y,x)) = x # label(false). [para(5490(a,1),4738(a,1)),flip(a)]. given #258 (F,wt=17): 5494 f(x,f(f(x,y),f(c_0,f(f(x,x),z)))) = f(x,x) # label(false). [back_rewrite(3961),rewrite([5474(4),3702(5),4301(3)])]. given #259 (F,wt=17): 5499 f(x,f(f(y,x),f(c_0,f(f(x,x),z)))) = f(x,x) # label(false). [back_rewrite(4040),rewrite([4989(4),3528(5),4301(3)])]. given #260 (T,wt=11): 6247 f(f(c_0,f(f(x,x),y)),x) = c_0. [para(1077(a,1),4619(a,1,2,2)),rewrite([4509(5,R),4534(4),4519(7)])]. given #261 (T,wt=11): 6248 f(f(c_0,f(x,f(y,y))),y) = c_0. [para(1154(a,1),4619(a,1,2,2)),rewrite([4509(5,R),4534(4),4519(7)])]. given #262 (T,wt=11): 6261 f(x,f(c_0,f(f(x,x),y))) = c_0. [para(32(a,1),4729(a,1,1,2)),rewrite([4519(3),4509(5,R),4534(4)])]. given #263 (T,wt=13): 6231 f(f(x,y),f(y,x)) = f(c_0,f(x,y)). [back_rewrite(6185),rewrite([6210(6),4825(9),4989(10),3702(10),4509(3,R),4534(3)]),flip(a)]. % Operation f is commutative; C redundancy checks enabled. given #264 (A,wt=21): 4360 f(f(x,y),f(c_0,f(y,f(z,f(y,f(x,y)))))) = f(y,f(x,y)). [back_rewrite(4179),rewrite([4209(3),4301(3)])]. given #265 (F,wt=11): 7102 f(x,f(x,f(y,x))) = f(y,x) # label(false). [para(4360(a,1),3702(a,1,2,2)),rewrite([4360(8),3528(6),6737(3)])]. given #266 (F,wt=17): 6086 f(f(x,f(x,y)),f(x,f(f(x,y),f(x,z)))) = x # label(false). [para(4998(a,1),4091(a,1,2,2,1)),rewrite([5474(2)])]. given #267 (F,wt=17): 6649 f(x,f(f(x,y),f(c_0,f(z,f(x,x))))) = f(x,x) # label(false). [para(4209(a,1),5494(a,1,2,2,2))]. given #268 (F,wt=17): 6686 f(f(x,x),f(f(y,f(x,x)),f(c_0,f(x,z)))) = x # label(false). [para(11(a,1),5499(a,1,2,2,2,1)),rewrite([4509(11,R),4534(11),4519(11)])]. given #269 (T,wt=7): 6737 f(x,y) = f(y,x). [para(6231(a,1),870(a,1,2)),rewrite([4509(3,R),4534(3),6736(7)])]. given #270 (T,wt=11): 7089 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(4719),rewrite([6737(4)])]. given #271 (T,wt=13): 6354 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(5075(a,1),4812(a,1,1,2)),rewrite([4538(2),4509(12,R),5474(8),4537(8)])]. given #272 (T,wt=13): 6812 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [back_rewrite(6457),rewrite([6737(5)])]. given #273 (A,wt=19): 4488 f(x,f(c_0,f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y) # label(false). [back_rewrite(4185),rewrite([4301(2)])]. given #274 (F,wt=17): 6817 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,y))))) = y # label(false). [back_rewrite(6431),rewrite([6737(3),6737(6),3702(6),4509(4,R),6737(4),4537(5),6737(5),6737(6)])]. given #275 (F,wt=17): 6876 f(f(x,y),f(c_0,f(f(x,z),f(x,f(x,y))))) = x # label(false). [back_rewrite(6153),rewrite([6737(2),6737(5),6737(8),6737(11),6737(13),6737(14),6737(15),6745(15),6737(8),6319(8),6737(2),6737(5),6737(7),6737(8)]),flip(a)]. given #276 (F,wt=17): 6994 f(f(x,y),f(x,f(f(x,z),f(x,f(x,y))))) = x # label(false). [back_rewrite(5664),rewrite([6737(4),6737(5)])]. given #277 (F,wt=17): 7078 f(f(x,y),f(y,f(f(y,z),f(y,f(x,y))))) = y # label(false). [back_rewrite(5100),rewrite([6737(5)])]. given #278 (T,wt=11): 7148 f(f(x,x),f(c_0,f(y,x))) = c_0. [para(6817(a,1),4756(a,1,2,2)),rewrite([4509(3,R),6737(3),6737(5),4509(5),6737(5)])]. given #279 (T,wt=13): 7111 f(x,f(c_0,f(f(x,x),f(y,z)))) = c_0. [para(4537(a,1),6086(a,1,2,2,2)),rewrite([6737(3),4509(3),4519(3),6737(3),4509(3)])]. given #280 (T,wt=13): 7127 f(f(c_0,c_0),f(f(x,y),f(z,z))) = c_0. [para(4537(a,1),6354(a,1,2,1)),rewrite([6737(6),4509(6)])]. given #281 (T,wt=13): 7128 f(f(c_0,c_0),f(f(x,x),f(y,z))) = c_0. [para(4537(a,1),6354(a,1,2,2)),rewrite([6737(5),4509(5)])]. given #282 (A,wt=17): 4702 f(f(c_0,f(x,y)),f(c_0,f(f(x,y),f(z,z)))) = c_0. [back_rewrite(3219),rewrite([4301(2),4301(5),4301(6),4513(8),4509(7,R),4534(7),4301(9),4534(9),4537(9),4301(7),4509(7),4301(11)])]. given #283 (F,wt=19): 5691 f(f(x,f(x,y)),f(c_0,f(x,f(z,f(x,y))))) = f(x,y) # label(false). [back_rewrite(4490),rewrite([5474(2),4989(7),3702(7)])]. given #284 (F,wt=17): 7158 f(f(x,f(y,x)),f(c_0,f(f(y,x),f(x,z)))) = x # label(false). [para(11(a,1),5691(a,1,1,2)),rewrite([6737(2),11(7),6737(5),11(11)])]. given #285 (F,wt=19): 7103 f(x,f(c_0,f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [para(4360(a,1),5075(a,1,1,2)),rewrite([3528(4),4360(9),6737(5)])]. given #286 (F,wt=19): 7147 f(f(x,f(y,x)),f(c_0,f(x,f(z,f(y,x))))) = f(y,x) # label(false). [para(6817(a,1),5075(a,1,1,2)),rewrite([6737(2),6817(11),6737(5)])]. given #287 (T,wt=13): 7130 f(f(c_0,c_0),f(f(x,y),f(x,z))) = c_0. [para(6354(a,1),7089(a,1,2,2)),rewrite([6737(7),6354(12)])]. given #288 (T,wt=13): 7138 f(f(c_0,c_0),f(f(x,y),f(y,z))) = c_0. [para(6812(a,1),7089(a,1,2,2)),rewrite([6737(7),6812(12)])]. given #289 (T,wt=15): 4745 f(f(x,f(y,z)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(3092),rewrite([4301(4)])]. given #290 (T,wt=13): 7227 f(f(c_0,c_0),f(f(x,y),f(z,u))) = c_0. [para(4745(a,1),7127(a,1,2,2))]. given #291 (A,wt=17): 4720 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [back_rewrite(3164),rewrite([4301(3),4509(9,R),4534(9)])]. given #292 (F,wt=21): 7084 f(f(x,y),f(x,f(c_0,f(z,f(c_0,f(x,y)))))) = f(c_0,f(x,y)) # label(false). [back_rewrite(5012),rewrite([6737(6)])]. given #293 (F,wt=17): 7231 f(x,f(f(y,x),f(c_0,f(z,f(x,x))))) = f(x,x) # label(false). [para(11(a,1),7084(a,1,2,2,2,2,2)),rewrite([11(3),6737(4),4509(4),11(11),6737(9),4509(9)])]. given #294 (F,wt=21): 7086 f(f(x,y),f(y,f(c_0,f(z,f(c_0,f(x,y)))))) = f(c_0,f(x,y)) # label(false). [back_rewrite(5005),rewrite([6737(6)])]. given #295 (F,wt=21): 7116 f(f(c_0,f(x,y)),f(f(y,y),f(z,f(c_0,f(x,y))))) = f(x,y) # label(false). [para(11(a,1),6686(a,1,2,2,2)),rewrite([4509(3,R),6737(3),4509(6,R),6737(6),6737(9),4509(9),6737(9)])]. given #296 (T,wt=15): 6319 f(f(x,x),f(c_0,f(f(x,y),f(x,z)))) = x. [para(5075(a,1),4719(a,1,1,2)),rewrite([4538(2),5075(15)])]. given #297 (T,wt=15): 6368 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,y)))) = c_0. [para(4100(a,1),4729(a,1,1,2)),rewrite([4509(8,R),4534(7)])]. given #298 (T,wt=15): 6823 f(f(x,x),f(c_0,f(f(y,x),f(x,z)))) = x. [back_rewrite(6415),rewrite([6737(3),6737(7)])]. given #299 (T,wt=15): 7010 f(f(x,x),f(c_0,f(y,f(y,f(x,x))))) = c_0. [back_rewrite(5597),rewrite([6737(4)])]. given #300 (A,wt=23): 4790 f(f(c_0,f(x,y)),f(c_0,f(f(y,f(x,y)),f(z,f(x,y))))) = f(x,y). [back_rewrite(2994),rewrite([4509(3,R),4534(3),4301(5)])]. given #301 (F,wt=21): 7118 f(f(c_0,f(x,y)),f(f(x,x),f(z,f(c_0,f(x,y))))) = f(x,y) # label(false). [para(3702(a,1),6686(a,1,2,2,2)),rewrite([4509(3,R),6737(3),4509(6,R),6737(6),6737(9),4509(9),6737(9)])]. given #302 (F,wt=17): 7330 f(f(x,x),f(f(y,f(x,x)),f(c_0,f(z,x)))) = x # label(false). [para(11(a,1),7118(a,1,2,2,2,2)),rewrite([11(4),6737(2),4509(2),4509(4,R),6737(4),6737(6),4509(6),6737(7),11(11)])]. given #303 (F,wt=23): 6522 f(f(c_0,f(f(x,y),f(x,z))),f(x,f(c_0,f(f(x,y),f(x,z))))) = x # label(false). [back_rewrite(6306),rewrite([6505(11)])]. given #304 (F,wt=23): 6523 f(x,f(x,f(c_0,f(f(x,y),f(x,z))))) = f(c_0,f(f(x,y),f(x,z))) # label(false). [back_rewrite(6305),rewrite([6505(6)])]. given #305 (T,wt=11): 7313 f(x,f(c_0,f(y,f(x,y)))) = c_0. [para(11(a,1),7010(a,1,1)),rewrite([4509(4,R),6737(4),4519(4),6737(2)])]. given #306 (T,wt=11): 7374 f(x,f(c_0,f(y,f(y,x)))) = c_0. [para(7313(a,1),7102(a,1,2,2)),rewrite([6737(2),6737(6),6737(10),4537(10),6737(7),4470(7),6737(3)]),flip(a)]. given #307 (T,wt=13): 7387 f(f(c_0,c_0),f(x,f(c_0,f(y,z)))) = c_0. [para(4720(a,1),7374(a,1,2,2,2)),rewrite([4470(10),6737(8)])]. given #308 (T,wt=15): 7110 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). [para(869(a,1),6086(a,1,2,2,2)),rewrite([6737(3),6737(7),6737(8),1154(8),4509(7,R),6737(7),4519(7),6737(5)])]. given #309 (A,wt=23): 5292 f(f(c_0,f(x,y)),f(c_0,f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y). [back_rewrite(1753),rewrite([4509(3,R),4534(3),4509(6,R),4534(6),4729(8)])]. given #310 (F,wt=23): 6538 f(f(c_0,f(f(x,y),f(y,z))),f(y,f(c_0,f(f(x,y),f(y,z))))) = y # label(false). [back_rewrite(6442),rewrite([6507(11)])]. given #311 (F,wt=23): 6821 f(f(x,f(y,z)),f(f(y,z),f(z,f(z,f(x,f(y,z)))))) = f(y,z) # label(false). [back_rewrite(6422),rewrite([6737(5),6737(9),3702(9),4509(6,R),6737(5),4537(6),6737(5),6737(8)])]. given #312 (F,wt=19): 7417 f(f(x,y),f(y,f(f(y,z),f(f(x,y),f(y,z))))) = y # label(false). [para(869(a,1),6821(a,1,1,2)),rewrite([869(4),869(6),6737(5),869(11)])]. given #313 (F,wt=19): 7455 f(f(x,y),f(x,f(f(x,z),f(f(x,y),f(x,z))))) = x # label(false). [para(7417(a,1),4537(a,1,2,2)),rewrite([6737(3),4509(3),4519(3),6737(1),6737(3)]),flip(a)]. given #314 (T,wt=15): 7123 f(x,f(f(y,f(x,x)),f(z,f(x,x)))) = c_0. [para(11(a,1),6354(a,1,1)),rewrite([6737(2),6737(4)])]. given #315 (T,wt=15): 7124 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0. [para(11(a,1),6354(a,1,2,1)),rewrite([4509(3,R),6737(3),6737(5),6737(7)])]. given #316 (T,wt=15): 7125 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0. [para(3702(a,1),6354(a,1,2,1)),rewrite([4509(3,R),6737(3),6737(5),6737(7)])]. given #317 (T,wt=15): 7133 f(f(x,y),f(c_0,f(z,f(c_0,f(x,y))))) = c_0. [para(4470(a,1),6812(a,1,2,1)),rewrite([4509(7,R),6737(5),4537(5),6737(6)])]. given #318 (A,wt=21): 5974 f(f(x,y),f(c_0,f(x,f(z,f(x,f(x,y)))))) = f(x,f(x,y)). [back_rewrite(4505),rewrite([4998(3)])]. given #319 (F,wt=19): 7457 f(f(x,y),f(x,f(f(x,z),f(f(x,z),f(x,y))))) = x # label(false). [para(7417(a,1),7102(a,1,2,2)),rewrite([6737(2),6737(4),6737(8),6737(10),6737(13),3702(14),6737(1),6737(3),6737(5)]),flip(a)]. given #320 (F,wt=23): 6822 f(f(x,f(y,z)),f(f(y,z),f(y,f(y,f(x,f(y,z)))))) = f(y,z) # label(false). [back_rewrite(6421),rewrite([6737(5),6737(9),3702(9),4509(6,R),6737(5),4537(6),6737(5),6737(8)])]. given #321 (F,wt=19): 7508 f(f(x,y),f(y,f(f(z,y),f(f(x,y),f(z,y))))) = y # label(false). [para(11(a,1),6822(a,1,2,1)),rewrite([11(3),11(6),6737(5),11(11)])]. given #322 (F,wt=23): 6884 f(f(x,f(y,z)),f(c_0,f(y,f(f(y,z),f(x,f(y,z)))))) = f(y,z) # label(false). [back_rewrite(6055),rewrite([6737(8),6368(10),6737(6),6737(8)])]. given #323 (T,wt=15): 7205 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [back_rewrite(6917),rewrite([7190(5)])]. given #324 (T,wt=15): 7391 f(f(c_0,c_0),f(x,f(f(y,z),f(y,u)))) = c_0. [para(6523(a,1),7387(a,1,2,2,2)),rewrite([4537(10)])]. given #325 (T,wt=15): 7566 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(y,x). [para(7205(a,1),7102(a,1,2,2)),rewrite([6737(2),6737(7),6737(11),6737(12),7161(13),6737(3)]),flip(a)]. given #326 (T,wt=15): 7606 f(f(c_0,c_0),f(x,f(f(y,z),f(u,u)))) = c_0. [para(4537(a,1),7391(a,1,2,2,1)),rewrite([6737(6),4509(6)])]. given #327 (A,wt=19): 6303 f(c_0,f(f(x,y),f(x,z))) = f(x,f(f(x,y),f(x,z))). [para(5075(a,1),11(a,1,1)),rewrite([4509(11,R),5474(7),4537(7)]),flip(a)]. given #328 (F,wt=13): 7581 f(f(x,x),f(y,f(c_0,f(x,z)))) = x # label(false). [para(7116(a,1),7205(a,1,2,2,2)),rewrite([6737(4),6737(7),6737(8),4720(8),4537(6),869(3),6737(3)]),flip(a)]. given #329 (F,wt=15): 7601 f(f(x,y),f(x,f(z,f(c_0,f(x,y))))) = x # label(false). [back_rewrite(7335),rewrite([7581(11),6737(6),7581(13)])]. given #330 (F,wt=15): 7632 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y) # label(false). [para(7330(a,1),7566(a,1,2,2,2)),rewrite([6737(7),1154(7),4519(6),6737(4),7089(4)]),flip(a)]. given #331 (F,wt=15): 7728 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,x) # label(false). [para(11(a,1),7581(a,1,1)),rewrite([6737(3)])]. given #332 (T,wt=13): 7719 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(6303(a,2),7566(a,1,2,2)),rewrite([6737(4),6737(5),4537(7),6737(5)])]. given #333 (T,wt=13): 7784 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(7111(a,1),7601(a,1,2,2)),rewrite([6737(6),4519(6),6737(4)])]. given #334 (T,wt=15): 7652 f(f(c_0,c_0),f(x,f(f(y,z),f(u,w)))) = c_0. [para(4745(a,1),7606(a,1,2,2,2))]. given #335 (T,wt=15): 7718 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(6303(a,1),7205(a,1,2)),rewrite([7157(5),4831(6)])]. given #336 (A,wt=19): 6439 f(c_0,f(f(x,y),f(y,z))) = f(y,f(f(x,y),f(y,z))). [para(5170(a,1),11(a,1,1)),rewrite([4509(11,R),5474(7),4537(7)]),flip(a)]. given #337 (F,wt=15): 7730 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z) # label(false). [para(3702(a,1),7581(a,1,2,2,2)),rewrite([4509(3,R),6737(3),6737(5),4509(5),6737(6)])]. given #338 (F,wt=13): 7971 f(f(x,x),f(y,f(c_0,f(z,x)))) = x # label(false). [para(11(a,1),7730(a,1,2,2)),rewrite([4509(3,R),6737(3),6737(6),4509(6),6737(6),11(9)])]. given #339 (F,wt=15): 7763 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y) # label(false). [back_rewrite(7164),rewrite([7730(8),6737(4),7730(11)])]. given #340 (F,wt=15): 7764 f(f(x,y),f(y,f(z,f(z,f(x,y))))) = y # label(false). [back_rewrite(7088),rewrite([7730(10)])]. given #341 (T,wt=13): 7921 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(11(a,1),7718(a,1,2,2,2)),rewrite([6737(3),11(7)])]. given #342 (T,wt=15): 7736 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(7581(a,1),7148(a,1,2,2)),rewrite([4509(9,R),6737(6),6737(8),4509(8),6737(8)])]. given #343 (T,wt=15): 7747 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x. [para(6523(a,1),7581(a,1,2,2,2)),rewrite([4537(8)])]. given #344 (T,wt=15): 7753 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0. [para(7581(a,1),7125(a,1,1,2))]. given #345 (A,wt=45): 6519 f(x,f(f(c_0,f(f(x,y),f(x,z))),f(f(x,f(c_0,f(f(x,y),f(x,z)))),f(u,f(c_0,f(f(x,y),f(x,z))))))) = f(c_0,f(f(x,y),f(x,z))). [back_rewrite(6344),rewrite([6505(11)])]. given #346 (F,wt=15): 7779 f(f(x,y),f(x,f(z,f(z,f(x,y))))) = x # label(false). [back_rewrite(7077),rewrite([6737(3),6737(4),7746(9),6737(10),6737(13),6737(15),7019(21),6737(10),4831(10)])]. given #347 (F,wt=15): 7781 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x) # label(false). [para(11(a,1),7601(a,1,2,2,2,2)),rewrite([11(3),6737(3),4509(3)])]. given #348 (F,wt=15): 7782 f(f(x,y),f(y,f(z,f(c_0,f(x,y))))) = y # label(false). [para(7102(a,1),7601(a,1,1)),rewrite([7102(5)])]. given #349 (F,wt=15): 7786 f(f(x,f(x,y)),f(x,f(z,f(x,y)))) = x # label(false). [para(5691(a,1),7601(a,1,2,2)),rewrite([6737(6)])]. given #350 (T,wt=15): 7806 f(f(c_0,f(x,f(y,y))),f(c_0,f(y,z))) = c_0. [para(7632(a,1),4756(a,1,2,2)),rewrite([4509(5,R),6737(4),6737(6)])]. given #351 (T,wt=15): 7820 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x. [para(7158(a,1),7632(a,1,2,2)),rewrite([4509(11,R),6737(7),4537(7),6737(6),4509(6),6737(6),7158(14)])]. given #352 (T,wt=15): 7831 f(f(c_0,c_0),f(x,f(y,f(c_0,f(z,u))))) = c_0. [para(7133(a,1),7632(a,1,2,2)),rewrite([4509(13,R),6737(8),4537(8),6737(9),7133(17)])]. given #353 (T,wt=15): 7851 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0. [para(7728(a,1),7148(a,1,2,2)),rewrite([4509(11,R),6737(7),4519(10),6737(8)])]. given #354 (A,wt=51): 6741 f(f(x,f(y,y)),f(f(y,f(x,f(f(x,z),f(x,f(x,f(y,y)))))),f(f(u,f(y,y)),f(f(y,y),f(x,f(x,f(f(x,z),f(x,f(x,f(y,y)))))))))) = f(y,y). [para(6231(a,1),4093(a,1,2,1,1)),rewrite([4519(5),6737(7),6737(14),6737(18),6737(20),6737(21)])]. given #355 (F,wt=15): 7867 f(f(x,y),f(y,f(z,f(y,f(x,y))))) = y # label(false). [para(3528(a,1),7719(a,1,2,1)),rewrite([6737(4),3528(10)])]. given #356 (F,wt=15): 7868 f(f(x,y),f(x,f(z,f(x,f(x,y))))) = x # label(false). [para(3702(a,1),7719(a,1,2,1)),rewrite([6737(4),3702(10)])]. given #357 (F,wt=15): 8014 f(x,f(f(x,y),f(z,f(x,z)))) = f(x,y) # label(false). [para(869(a,1),7764(a,1,1)),rewrite([869(4),6737(2)])]. given #358 (F,wt=15): 8152 f(x,f(f(y,x),f(z,f(x,z)))) = f(y,x) # label(false). [para(11(a,1),7779(a,1,2,2,2,2)),rewrite([11(3),6737(2)])]. given #359 (T,wt=15): 7866 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(11(a,1),7719(a,1,2,2)),rewrite([6737(3)])]. given #360 (T,wt=15): 7894 f(x,f(c_0,f(y,f(c_0,f(z,f(x,z)))))) = c_0. [para(7313(a,1),7719(a,1,2,1)),rewrite([6737(6),7313(13)])]. given #361 (T,wt=15): 7982 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(7971(a,1),7148(a,1,2,2)),rewrite([4509(9,R),6737(6),6737(8),4509(8),6737(8)])]. given #362 (T,wt=15): 8061 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,y)))) = c_0. [para(11(a,1),7736(a,1,2,2,2,2)),rewrite([4509(3,R),6737(3),6737(6),4509(6)])]. given #363 (A,wt=39): 6742 f(f(x,y),f(f(c_0,f(y,f(x,f(x,f(f(x,z),f(x,f(x,y))))))),f(f(y,y),f(x,f(f(x,z),f(x,f(x,y))))))) = y # label(false). [para(6231(a,1),4093(a,1,2,2)),rewrite([6737(6),6737(13),6737(16),6737(18)])]. given #364 (F,wt=15): 8224 f(f(x,y),f(x,f(x,f(c_0,f(y,z))))) = x # label(false). [para(7581(a,1),7786(a,1,2,2)),rewrite([6737(7)])]. given #365 (F,wt=15): 8228 f(f(x,y),f(x,f(x,f(c_0,f(z,y))))) = x # label(false). [para(7971(a,1),7786(a,1,2,2)),rewrite([6737(7)])]. given #366 (F,wt=15): 8511 f(f(x,f(y,z)),f(x,f(x,f(z,z)))) = x # label(false). [para(11(a,1),8224(a,1,2,2,2,2)),rewrite([6737(4),4509(4)])]. given #367 (F,wt=15): 8513 f(f(x,f(x,f(y,y))),f(x,f(y,z))) = x # label(false). [para(3702(a,1),8224(a,1,2,2,2,2)),rewrite([6737(4),4509(4),6737(6)])]. given #368 (T,wt=15): 8062 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,x)))) = c_0. [para(3702(a,1),7736(a,1,2,2,2,2)),rewrite([4509(3,R),6737(3),6737(6),4509(6)])]. given #369 (T,wt=15): 8107 f(f(x,f(y,z)),f(c_0,f(x,f(z,z)))) = c_0. [para(11(a,1),7753(a,1,2,2,2,2)),rewrite([6737(5),4509(5)])]. given #370 (T,wt=15): 8109 f(f(x,f(y,z)),f(c_0,f(x,f(y,y)))) = c_0. [para(3702(a,1),7753(a,1,2,2,2,2)),rewrite([6737(5),4509(5)])]. given #371 (T,wt=15): 8114 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(6737(a,1),7753(a,1,1))]. given #372 (A,wt=49): 6785 f(f(x,f(x,y)),f(f(x,y),f(f(f(x,x),f(y,f(f(y,z),f(y,f(x,y))))),f(f(x,u),f(x,f(y,f(y,f(f(y,z),f(y,f(x,y)))))))))) = f(x,y). [back_rewrite(6621),rewrite([6737(1),6737(4),6737(7),6737(10),6737(13),6737(16),6737(18),6737(20),6737(21),6737(23)])]. given #373 (F,wt=15): 8518 f(f(x,y),f(y,f(y,f(c_0,f(x,z))))) = y # label(false). [para(6737(a,1),8224(a,1,1))]. given #374 (F,wt=15): 8549 f(f(x,f(x,y)),f(x,f(z,f(y,y)))) = x # label(false). [para(6741(a,1),8224(a,1,2,2,2,2)),rewrite([4519(6),6737(6)])]. given #375 (F,wt=15): 8601 f(x,f(y,f(y,f(x,x)))) = f(x,f(y,y)) # label(false). [para(8513(a,1),7205(a,1,2,2)),rewrite([6737(2),4509(2)]),flip(a)]. given #376 (F,wt=15): 8720 f(f(x,f(y,z)),f(x,f(x,f(y,y)))) = x # label(false). [para(3702(a,1),8518(a,1,2,2,2,2)),rewrite([6737(2),6737(4),4509(4)])]. given #377 (T,wt=15): 8133 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0. [para(7632(a,1),7753(a,1,2,2)),rewrite([6737(3),6737(5)])]. given #378 (T,wt=15): 8291 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0. [para(6741(a,1),7753(a,1,2,2,2,2)),rewrite([4519(7)])]. given #379 (T,wt=15): 8402 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0. [para(7894(a,1),7102(a,1,2,2)),rewrite([6737(3),6737(10),6737(16),4537(16),6737(13),4470(13),6737(4)]),flip(a)]. given #380 (T,wt=15): 8417 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0. [para(7894(a,1),7730(a,1)),rewrite([6737(5)]),flip(a)]. given #381 (A,wt=47): 6789 f(f(x,f(c_0,f(f(y,z),f(z,u)))),f(c_0,f(z,f(f(c_0,f(f(y,z),f(z,u))),f(x,f(c_0,f(f(y,z),f(z,u)))))))) = f(c_0,f(f(y,z),f(z,u))). [back_rewrite(6605),rewrite([6737(18),6737(20)])]. given #382 (F,wt=15): 8754 f(f(x,f(y,f(z,z))),f(x,f(z,x))) = x # label(false). [para(6741(a,1),8518(a,1,2,2,2,2)),rewrite([6737(3),4519(6),6737(4)])]. given #383 (F,wt=15): 8781 f(x,f(f(x,f(x,y)),f(y,y))) = f(x,x) # label(false). [para(8549(a,1),7718(a,1,2)),flip(a)]. given #384 (F,wt=17): 7533 f(f(x,y),f(c_0,f(f(z,y),f(y,f(x,y))))) = y # label(false). [para(11(a,1),6884(a,1,2,2,2,1)),rewrite([11(3),11(6),11(11)])]. given #385 (F,wt=17): 7620 f(f(x,y),f(c_0,f(z,f(x,x)))) = f(z,f(x,x)) # label(false). [para(6649(a,1),7566(a,1,2,2,2)),rewrite([6737(8),869(8),6737(6),4509(6),6737(6),7089(6)]),flip(a)]. given #386 (T,wt=15): 8653 f(f(c_0,f(x,f(x,y))),f(c_0,f(y,z))) = c_0. [para(7313(a,1),8114(a,1,1)),rewrite([6737(4),7653(12)])]. given #387 (T,wt=15): 8928 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(11(a,1),8417(a,1,2,2,2,2,2)),rewrite([6737(3)])]. given #388 (T,wt=15): 8932 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,z)))) = c_0. [para(7581(a,1),8417(a,1,2,2,2,2)),rewrite([6737(5)])]. given #389 (T,wt=15): 8935 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,z)))) = c_0. [para(7971(a,1),8417(a,1,2,2,2,2)),rewrite([6737(5)])]. given #390 (A,wt=57): 6794 f(f(c_0,f(f(x,f(x,y)),f(z,f(x,y)))),f(f(x,y),f(f(f(x,x),f(y,f(f(y,u),f(y,f(x,y))))),f(f(x,w),f(x,f(y,f(y,f(f(y,u),f(y,f(x,y)))))))))) = f(x,y). [back_rewrite(6588),rewrite([6737(2),6737(5),6737(8),6737(11),6737(14),6737(16),6737(18),6737(19),6737(21),6737(23),6737(27),6737(28)])]. given #391 (F,wt=17): 7676 f(f(x,f(x,y)),f(f(x,y),f(x,z))) = f(x,y) # label(false). [para(6303(a,2),5691(a,1,2,2)),rewrite([6737(7),4537(9)])]. given #392 (F,wt=15): 9238 f(f(x,f(y,x)),f(x,f(z,f(y,x)))) = x # label(false). [para(11(a,1),7676(a,1,1,2)),rewrite([6737(2),11(5),6737(4),11(9)])]. given #393 (F,wt=17): 7787 f(f(x,f(y,x)),f(f(y,x),f(x,z))) = f(y,x) # label(false). [para(7158(a,1),7601(a,1,2,2)),rewrite([6737(5),6737(6)])]. given #394 (F,wt=17): 7799 f(f(x,y),f(c_0,f(z,f(y,y)))) = f(z,f(y,y)) # label(false). [para(11(a,1),7632(a,1,1,2))]. given #395 (T,wt=15): 9104 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(11(a,1),8653(a,1,2,2)),rewrite([6737(7),4509(7),6737(7)])]. given #396 (T,wt=17): 7226 f(f(c_0,f(x,y)),f(c_0,f(f(x,y),f(z,u)))) = c_0. [para(4745(a,1),7111(a,1,2,2,1))]. given #397 (T,wt=17): 7385 f(f(c_0,f(x,y)),f(x,f(f(x,y),f(x,z)))) = c_0. [para(6086(a,1),7374(a,1,2,2,2)),rewrite([6737(8),4998(8),6737(8)])]. given #398 (T,wt=17): 7752 f(f(x,x),f(f(x,y),f(z,f(c_0,f(x,u))))) = c_0. [para(7581(a,1),7124(a,1,1,2,2)),rewrite([6737(5),6737(6),7581(13),6737(8),4509(8),6737(8)])]. given #399 (A,wt=39): 6808 f(f(x,y),f(x,f(f(z,f(c_0,f(x,y))),f(f(c_0,f(x,y)),f(x,f(x,f(f(x,u),f(x,f(x,y))))))))) = f(c_0,f(x,y)). [back_rewrite(6499),rewrite([6737(5),6737(11),6737(15),6737(16)])]. given #400 (F,wt=17): 7869 f(x,f(f(x,y),f(z,f(x,f(x,y))))) = f(x,y) # label(false). [para(4998(a,1),7719(a,1,2,1)),rewrite([6737(4),4998(9)])]. given #401 (F,wt=17): 8020 f(f(x,f(x,y)),f(f(x,z),f(x,y))) = f(x,y) # label(false). [para(6354(a,1),7764(a,1,2,2,2)),rewrite([6737(7),4519(7),6737(5),6737(6)])]. given #402 (F,wt=17): 8021 f(f(x,f(x,y)),f(f(z,x),f(x,y))) = f(x,y) # label(false). [para(6812(a,1),7764(a,1,2,2,2)),rewrite([6737(7),4519(7),6737(5),6737(6)])]. given #403 (F,wt=17): 8308 f(x,f(f(y,x),f(z,f(x,f(y,x))))) = f(y,x) # label(false). [para(7921(a,1),7867(a,1,2,2,2)),rewrite([6737(2),6737(4),3528(4),6737(3)])]. given #404 (T,wt=13): 9468 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(8020(a,1),7089(a,1,2,2)),rewrite([6737(7),8098(7),8020(10)])]. given #405 (T,wt=13): 9478 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(8021(a,1),7089(a,1,2,2)),rewrite([6737(7),8251(7),8021(10)])]. given #406 (T,wt=13): 9519 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(9468(a,1),4537(a,1,2,2)),rewrite([4537(5),6737(4)]),flip(a)]. given #407 (T,wt=17): 7841 f(f(x,x),f(y,f(c_0,f(z,f(c_0,f(x,u)))))) = x. [para(7581(a,1),7632(a,1,2,2)),rewrite([4509(9,R),6737(6),6737(9),4509(9),6737(9),7581(15)])]. given #408 (A,wt=47): 6809 f(f(c_0,f(x,f(y,f(c_0,f(f(z,x),f(x,u)))))),f(f(c_0,f(f(z,x),f(x,u))),f(y,f(c_0,f(f(z,x),f(x,u)))))) = f(c_0,f(f(z,x),f(x,u))). [back_rewrite(6467),rewrite([6737(20),6737(22)])]. given #409 (F,wt=17): 8586 f(f(x,f(x,y)),f(c_0,f(f(x,z),f(x,y)))) = x # label(false). [para(6303(a,2),8511(a,1,1)),rewrite([4509(8,R),6737(8),4831(9),6737(8)])]. given #410 (F,wt=17): 8590 f(f(x,f(x,y)),f(c_0,f(f(z,x),f(x,y)))) = x # label(false). [para(6439(a,2),8511(a,1,1)),rewrite([4509(8,R),6737(8),4831(9),6737(8)])]. given #411 (F,wt=17): 8777 f(f(x,x),f(y,f(x,y))) = f(f(x,x),f(y,y)) # label(false). [para(8549(a,1),7566(a,1,2,2)),rewrite([6737(3),4509(3),6737(4),6737(7)]),flip(a)]. given #412 (F,wt=17): 8818 f(x,f(f(y,y),f(f(x,x),f(y,y)))) = f(x,y) # label(false). [para(11(a,1),8601(a,2,2)),rewrite([6737(4)])]. given #413 (T,wt=17): 7873 f(f(x,x),f(c_0,f(y,f(f(x,z),f(x,u))))) = c_0. [para(6354(a,1),7719(a,1,2,1)),rewrite([6737(6),6354(13)])]. given #414 (T,wt=17): 7881 f(x,f(c_0,f(y,f(c_0,f(f(x,x),f(z,u)))))) = c_0. [para(7111(a,1),7719(a,1,2,1)),rewrite([6737(7),7111(15)])]. given #415 (T,wt=17): 7893 f(x,f(c_0,f(f(x,y),f(f(x,y),f(y,z))))) = c_0. [para(7719(a,1),7313(a,1,2,2,2)),rewrite([6737(6)])]. given #416 (T,wt=17): 7895 f(f(c_0,f(x,f(x,y))),f(f(x,y),f(y,z))) = c_0. [para(7719(a,1),7374(a,1,2,2,2)),rewrite([6737(8)])]. given #417 (A,wt=23): 6810 f(f(x,y),f(y,f(f(y,f(x,y)),f(c_0,f(f(y,z),f(y,u)))))) = y. [back_rewrite(6464),rewrite([6737(2),6737(5)])]. given #418 (F,wt=17): 9037 f(f(x,f(x,y)),f(y,y)) = f(f(x,x),f(y,y)) # label(false). [para(8781(a,1),7205(a,1,2,2,2)),rewrite([6737(6),7995(8)]),flip(a)]. given #419 (F,wt=17): 9064 f(f(x,y),f(c_0,f(f(z,x),f(x,f(x,y))))) = x # label(false). [para(7533(a,1),7102(a,1,2,2)),rewrite([6737(3),6737(9),6737(13),8237(14),6737(1),6737(4)]),flip(a)]. given #420 (F,wt=17): 9773 f(f(c_0,f(x,y)),f(f(x,x),f(z,z))) = f(x,y) # label(false). [para(8777(a,1),7620(a,1,1)),rewrite([4509(7,R),6737(7),4519(7),6737(5),6737(7),4509(10,R),6737(10),4519(10),6737(8)])]. given #421 (F,wt=17): 10061 f(f(c_0,f(x,y)),f(f(z,z),f(x,x))) = f(x,y) # label(false). [para(9037(a,1),7632(a,1,1)),rewrite([6737(5),6737(7),6737(8)])]. given #422 (T,wt=17): 7916 f(f(c_0,f(x,y)),f(f(x,y),f(z,u))) = f(x,y). [para(4745(a,1),7784(a,1,2,1)),rewrite([4509(14,R),6737(12),4537(12)])]. given #423 (T,wt=17): 7918 f(x,f(f(y,f(x,x)),f(f(x,x),f(z,u)))) = c_0. [para(7784(a,1),7124(a,1,1,2,2)),rewrite([6737(6),7784(11),4519(9),6737(7)])]. given #424 (T,wt=17): 7920 f(x,f(y,f(c_0,f(f(x,x),f(z,u))))) = f(x,x). [para(7784(a,1),7632(a,1,2,2)),rewrite([4509(7,R),6737(5),4519(9),6737(7),7784(11)])]. given #425 (T,wt=17): 7988 f(f(x,x),f(f(x,y),f(z,f(c_0,f(u,x))))) = c_0. [para(7971(a,1),7124(a,1,1,2,2)),rewrite([6737(5),6737(6),7971(13),6737(8),4509(8),6737(8)])]. given #426 (A,wt=33): 6815 f(f(x,f(y,z)),f(f(u,f(c_0,f(y,z))),f(y,f(f(y,z),f(u,f(u,f(x,f(y,z)))))))) = f(y,z). [back_rewrite(6433),rewrite([6737(5),6737(9),3702(9),4509(6,R),6737(5),4537(6),6737(6),6737(9),6737(12),6737(13)])]. given #427 (F,wt=17): 10115 f(f(c_0,f(x,y)),f(f(y,y),f(z,z))) = f(x,y) # label(false). [para(7102(a,1),9773(a,1,1,2)),rewrite([7102(10)])]. given #428 (F,wt=19): 7600 f(x,f(c_0,f(y,f(c_0,f(x,z))))) = f(y,f(c_0,f(x,z))) # label(false). [back_rewrite(7442),rewrite([7581(12),6737(7)])]. given #429 (F,wt=15): 10456 f(f(x,y),f(x,f(y,f(c_0,f(x,z))))) = x # label(false). [para(7600(a,1),8224(a,1,2,2))]. given #430 (F,wt=15): 10463 f(f(x,y),f(y,f(x,f(c_0,f(y,z))))) = y # label(false). [para(7600(a,1),8518(a,1,2,2))]. given #431 (T,wt=15): 10464 f(f(c_0,f(x,f(x,y))),f(c_0,f(z,y))) = c_0. [para(8935(a,1),7600(a,1,2,2)),rewrite([4819(4),6737(6),6737(9)]),flip(a)]. given #432 (T,wt=15): 10606 f(f(c_0,f(x,y)),f(c_0,f(z,f(z,y)))) = c_0. [para(10464(a,1),7600(a,1,2,2)),rewrite([4819(4),6737(9)]),flip(a)]. given #433 (T,wt=17): 7992 f(f(x,x),f(y,f(c_0,f(z,f(c_0,f(u,x)))))) = x. [para(7971(a,1),7632(a,1,2,2)),rewrite([4509(9,R),6737(6),6737(9),4509(9),6737(9),7971(15)])]. given #434 (T,wt=17): 8027 f(f(c_0,f(x,y)),f(f(z,u),f(x,y))) = f(x,y). [para(7227(a,1),7764(a,1,2,2,2)),rewrite([6737(9),4301(9),6737(6),6737(7)])]. given #435 (A,wt=33): 6816 f(f(x,f(y,z)),f(f(u,f(c_0,f(y,z))),f(z,f(f(y,z),f(u,f(u,f(x,f(y,z)))))))) = f(y,z). [back_rewrite(6432),rewrite([6737(5),6737(9),3702(9),4509(6,R),6737(5),4537(6),6737(6),6737(9),6737(12),6737(13)])]. given #436 (F,wt=19): 7630 f(x,f(c_0,f(y,f(c_0,f(z,x))))) = f(y,f(c_0,f(z,x))) # label(false). [para(7086(a,1),7566(a,1,2,2,2)),rewrite([7089(11),6737(10),7089(10)]),flip(a)]. given #437 (F,wt=19): 7645 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)) # label(false). [back_rewrite(7162),rewrite([7620(8),7620(12)])]. given #438 (F,wt=19): 7729 f(x,f(x,f(y,f(c_0,f(x,z))))) = f(y,f(c_0,f(x,z))) # label(false). [para(7581(a,1),3528(a,1,1)),rewrite([7581(10),6737(5)])]. given #439 (F,wt=19): 7731 f(f(x,f(c_0,f(y,z))),f(y,f(x,f(c_0,f(y,z))))) = y # label(false). [para(7581(a,1),7102(a,1,2,2)),rewrite([6737(9),7581(16)])]. given #440 (T,wt=15): 10906 f(x,f(c_0,f(y,f(c_0,f(z,f(x,y)))))) = c_0. [para(7729(a,1),7893(a,1,2,2)),rewrite([6737(4)])]. given #441 (T,wt=15): 10938 f(x,f(c_0,f(y,f(c_0,f(z,f(y,x)))))) = c_0. [para(10906(a,1),7102(a,1,2,2)),rewrite([6737(3),6737(10),6737(16),4537(16),6737(13),4470(13),6737(4)]),flip(a)]. given #442 (T,wt=15): 10956 f(x,f(c_0,f(y,f(x,f(z,f(y,y)))))) = c_0. [para(7730(a,1),10906(a,1,2,2))]. given #443 (T,wt=15): 11039 f(x,f(c_0,f(f(y,y),f(x,f(y,z))))) = c_0. [para(11(a,1),10956(a,1,2,2,2,2,2)),rewrite([6737(3)])]. given #444 (A,wt=33): 6820 f(f(x,f(y,y)),f(f(y,z),f(f(u,f(y,y)),f(f(y,y),f(z,f(z,f(x,f(y,y)))))))) = f(y,y). [back_rewrite(6424),rewrite([6737(5),6737(9),3702(9),4509(6,R),6737(5),4537(6),6737(6),6737(9),6737(11),6737(12)])]. given #445 (F,wt=19): 7758 f(f(c_0,f(x,y)),f(c_0,f(x,z))) = f(z,f(c_0,f(x,y))) # label(false). [para(7581(a,1),7566(a,1,2,2,2)),rewrite([6737(5)])]. given #446 (F,wt=15): 11205 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))) # label(false). [para(7758(a,2),7102(a,1,2,2)),rewrite([11204(13),11203(12),11204(7)])]. ============================== PROOF ================================= % Proof 1 at 18.99 (+ 0.08) seconds: A_SS. % Length of proof is 263. % Level of proof is 49. % Maximum clause weight is 57. % Given clauses 446. 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS) # label(non_clause) # label(goal). [goal]. 2 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. 3 f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. 4 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(y,w)))) = y. [para(2(a,1),2(a,1,2,1))]. 5 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),f(f(z,x),v5)))) = f(z,x). [para(2(a,1),2(a,1,2,2,1,1,1,1))]. 7 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z). [para(2(a,1),2(a,1,2,2,2))]. 8 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(4(a,1),2(a,1,2,2))]. 11 f(f(x,y),f(y,y)) = y. [para(4(a,1),4(a,1,2,2))]. 13 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(11(a,1),2(a,1,2,1,1))]. 14 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,y)),f(y,y)),y),f(y,z)))) = y. [para(11(a,1),2(a,1,2,1))]. 20 f(f(x,f(y,y)),y) = f(y,y). [para(11(a,1),11(a,1,2))]. 22 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(14),rewrite([20(7)])]. 32 f(f(f(x,x),y),x) = f(x,x). [para(8(a,1),11(a,1,1)),rewrite([8(7)]),flip(a)]. 36 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),z),f(f(f(f(f(x,x),z),z),f(f(x,x),y)),f(f(f(x,x),y),u)))) = f(f(x,x),y). [para(32(a,1),2(a,1,2,2,1,1,1,1))]. 37 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x. [para(32(a,1),2(a,1,2,2,1,1))]. 40 f(f(x,y),f(x,x)) = x. [para(11(a,1),32(a,1,1,1)),rewrite([11(6)])]. 50 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(32(a,1),5(a,1,1)),rewrite([40(3),40(3)])]. 53 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(false). [para(40(a,1),2(a,1,2,2,1,1))]. 54 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),y))) = f(y,z). [para(40(a,1),2(a,1,2,2,2))]. 55 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(2(a,1),40(a,1,1))]. 57 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),w)))) = f(y,x). [para(40(a,1),5(a,1,1,1,2,1,1))]. 59 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),f(x,x)),f(f(x,f(z,x)),f(f(z,x),w)))) = f(z,x). [para(40(a,1),5(a,1,2,2,1,1))]. 61 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(40(a,1),40(a,1,1))]. 82 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x. [para(22(a,1),32(a,1)),flip(a)]. 85 f(f(x,y),f(y,f(f(y,y),f(z,y)))) = y. [para(55(a,1),22(a,1,2,2,2))]. 97 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(f(y,z),x),f(f(y,z),x))),f(f(f(f(y,z),x),f(y,z)),z))) = f(y,z) # label(false). [para(2(a,1),53(a,1,2,2,2))]. 104 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(20(a,1),53(a,1,2,2,1)),rewrite([55(9)])]. 109 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),f(f(x,y),z)))) = f(x,y) # label(false). [para(40(a,1),53(a,1,2,1,2,1)),rewrite([40(9),40(11)])]. 110 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(f(y,z),x),f(f(y,z),x))),f(f(f(f(y,z),x),f(y,z)),y))) = f(y,z) # label(false). [para(40(a,1),53(a,1,2,2,2))]. 112 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(y,z)))) = y # label(false). [para(55(a,1),53(a,1,2,1,2,1)),rewrite([55(10),55(13)])]. 113 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(z,y)))) = y # label(false). [para(55(a,1),53(a,1,2,2,2))]. 114 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z)))) = x # label(false). [para(61(a,1),53(a,1,2,1,2,1)),rewrite([61(10),61(13)])]. 123 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [para(11(a,1),113(a,1,2,1,2,1)),rewrite([11(9),11(11)])]. 124 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x. [para(11(a,1),113(a,1,2,1,2))]. 132 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y) # label(false). [para(40(a,1),113(a,1,2,1,2,1)),rewrite([40(9),40(11)])]. 134 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(z,y)))) = y # label(false). [para(55(a,1),113(a,1,2,1,2,1)),rewrite([55(10),55(13)])]. 135 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(z,x)))) = x # label(false). [para(61(a,1),113(a,1,2,1,2,1)),rewrite([61(10),61(13)])]. 144 f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(x,x),x),f(f(x,x),f(x,y)))) = x. [para(32(a,1),112(a,1,2,2,1)),rewrite([61(13)])]. 150 f(f(f(f(f(x,x),y),f(f(x,x),y)),f(x,x)),f(f(x,f(f(f(x,x),y),f(f(x,x),y))),f(f(f(f(x,x),y),f(x,x)),f(f(x,x),z)))) = f(x,x) # label(false). [para(11(a,1),114(a,1,2,1,1))]. 159 f(x,f(f(x,x),f(x,f(y,f(x,x))))) = f(x,x). [para(11(a,1),85(a,1,1)),rewrite([40(4)])]. 192 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(false). [para(11(a,1),7(a,1,2,2,1,1,1,1))]. 223 f(f(f(f(x,f(y,y)),f(x,f(y,y))),f(y,y)),f(f(y,f(f(x,f(y,y)),f(x,f(y,y)))),f(f(f(x,f(y,y)),f(y,y)),f(z,f(y,y))))) = f(y,y) # label(false). [para(11(a,1),134(a,1,2,1,1))]. 231 f(f(f(f(f(x,x),y),f(f(x,x),y)),f(x,x)),f(f(x,f(f(f(x,x),y),f(f(x,x),y))),f(f(f(f(x,x),y),f(x,x)),f(z,f(x,x))))) = f(x,x) # label(false). [para(11(a,1),135(a,1,2,1,1))]. 235 f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(f(x,x),x),f(f(x,x),x)),x)) = f(f(f(x,x),x),f(f(f(f(x,x),x),f(f(x,x),x)),x)). [para(192(a,1),20(a,1,1)),flip(a)]. 238 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [para(40(a,1),192(a,1,2,2,1,1))]. 242 f(f(f(x,x),x),f(f(f(f(x,x),x),f(f(x,x),x)),x)) = f(f(f(x,x),x),f(f(x,x),x)). [para(192(a,1),159(a,1,2,2,2)),rewrite([235(19),32(24),40(21),32(9),235(18)]),flip(a)]. 246 f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(f(x,x),x),f(f(x,x),x)),x)) = f(f(f(x,x),x),f(f(x,x),x)). [back_rewrite(235),rewrite([242(22)])]. 249 f(x,f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))))) = f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))). [para(37(a,1),11(a,1,1))]. 252 f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x)) = x. [para(37(a,1),55(a,1,2,1)),rewrite([37(16),37(18)])]. 259 f(x,f(f(x,x),f(x,y))) = f(x,x). [para(82(a,1),11(a,1,1)),rewrite([82(9)]),flip(a)]. 266 f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),x),f(f(f(x,x),f(f(x,x),f(x,y))),f(z,f(f(x,x),f(x,y)))))) = f(f(x,x),f(x,y)). [para(82(a,1),134(a,1,1,1)),rewrite([259(4),259(12),259(13),40(11),259(13)])]. 270 f(f(x,y),f(f(f(y,y),f(f(f(y,x),f(y,x)),f(f(y,x),z))),f(f(f(f(f(y,x),f(y,x)),f(f(f(y,x),f(y,x)),f(f(y,x),z))),y),f(y,u)))) = y. [para(259(a,1),2(a,1,2,2,1,1,1))]. 272 f(f(x,x),f(x,f(f(x,x),y))) = x. [para(11(a,1),259(a,1,2,1)),rewrite([40(8)])]. 275 f(x,f(f(x,x),f(y,x))) = f(x,x). [para(55(a,1),259(a,1,2,2))]. 283 f(f(x,x),f(x,f(y,f(x,x)))) = x. [para(55(a,1),272(a,1,2,2))]. 307 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),y))) = f(x,y). [para(2(a,1),109(a,1,2,2,2))]. 313 f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),x),f(f(f(x,x),f(f(x,x),f(x,y))),f(x,y)))) = f(f(x,x),f(x,y)). [para(109(a,1),109(a,1,2,2,2)),rewrite([40(3),259(4),40(11)])]. 340 f(f(f(f(x,x),x),f(f(x,x),x)),x) = f(f(x,x),x). [para(192(a,1),283(a,1,2,2)),rewrite([246(13),32(14),40(11)]),flip(a)]. 343 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(x,y)))) = x. [back_rewrite(144),rewrite([340(6)])]. 358 f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)) = x. [para(104(a,1),55(a,1,2,1)),rewrite([104(15),104(17)])]. 428 f(f(f(f(x,x),x),f(x,f(f(x,x),y))),x) = f(x,x). [para(11(a,1),358(a,1,1,1,2)),rewrite([40(5),40(9)])]. 437 f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x) = f(x,x). [para(55(a,1),428(a,1,1,2,2))]. 561 f(x,f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))))) = f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))). [para(124(a,1),11(a,1,1))]. 562 f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(x,x)) = x. [para(124(a,1),55(a,1,2,1)),rewrite([124(16),124(18)])]. 688 f(f(f(f(f(x,x),x),f(f(x,x),f(x,y))),f(f(x,x),x)),f(x,x)) = f(f(x,x),x). [para(343(a,1),110(a,1,2,1,2,1)),rewrite([343(23),343(25),40(21),20(17)])]. 858 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),z),f(f(f(f(f(x,x),z),z),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y) # label(false). [para(32(a,1),36(a,1,2,2,2))]. 863 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),x))) = f(x,y) # label(false). [para(11(a,1),858(a,1,1,2,1)),rewrite([40(6),40(7),40(10),40(12),40(14),40(17)])]. 869 f(f(x,x),f(x,y)) = x. [para(428(a,1),858(a,1,2,2)),rewrite([40(4),259(4),40(5),40(8),40(13),20(11),40(3),40(4)]),flip(a)]. 870 f(f(x,x),f(y,x)) = x. [para(437(a,1),858(a,1,2,2)),rewrite([869(4),275(4),869(5),869(8),869(13),20(11),869(3),869(4)]),flip(a)]. 875 f(x,f(f(f(f(x,y),f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),x))) = f(x,y) # label(false). [back_rewrite(863),rewrite([869(3)])]. 880 f(f(x,x),x) = f(x,f(x,x)). [back_rewrite(688),rewrite([869(5),32(3),870(4)]),flip(a)]. 887 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = x. [back_rewrite(313),rewrite([869(4),869(4),880(3),869(7),880(5),869(12)])]. 889 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(307),rewrite([869(3)])]. 891 f(f(x,y),f(y,f(f(f(f(y,x),f(f(y,x),f(y,x))),y),f(y,z)))) = y. [back_rewrite(270),rewrite([869(8),869(4),869(10),880(6)])]. 892 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = x. [back_rewrite(266),rewrite([869(4),869(4),880(3),869(7),880(5),869(8),869(12)])]. 894 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y) # label(false). [back_rewrite(132),rewrite([869(3)])]. 921 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(238),rewrite([870(3)])]. 924 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(192),rewrite([870(3)])]. 925 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [back_rewrite(123),rewrite([870(3)])]. 982 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(x,x)) = x. [back_rewrite(562),rewrite([880(2),880(4)])]. 983 f(x,f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))))) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))). [back_rewrite(561),rewrite([880(2),880(4),880(9),880(11),880(18),880(20)])]. 1024 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x)) = x. [back_rewrite(252),rewrite([880(2),880(4)])]. 1026 f(x,f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))))) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))). [back_rewrite(249),rewrite([880(2),880(4),880(9),880(11),880(18),880(20)])]. 1052 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))) = y # label(false). [para(2(a,1),875(a,1,2,1,1,1)),rewrite([2(12),2(17),2(22)])]. 1067 f(f(x,y),f(f(f(f(f(x,f(x,x)),y),y),f(x,x)),f(f(x,x),z))) = x. [para(13(a,1),875(a,1,2,2,1)),rewrite([40(6),880(4),40(17),880(15),869(29),20(27),40(3),40(5),880(3)]),flip(a)]. 1076 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(2(a,1),869(a,1,2))]. 1082 f(f(f(x,y),f(x,y)),x) = f(x,y). [para(40(a,1),869(a,1,2))]. 1101 f(f(x,y),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z)))) = x # label(false). [para(869(a,1),150(a,1,1,1,1,1)),rewrite([869(4),869(6),1082(4),869(5),869(6),869(9),869(10),869(11),869(15)])]. 1102 f(f(x,y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(z,y)))) = y # label(false). [para(869(a,1),223(a,1,1,1,1,2)),rewrite([869(4),869(6),1076(4),869(5),869(6),869(9),869(10),869(11),869(15)])]. 1103 f(f(x,y),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(z,x)))) = x # label(false). [para(869(a,1),231(a,1,1,1,1,1)),rewrite([869(4),869(6),1082(4),869(5),869(6),869(9),869(10),869(11),869(15)])]. 1110 f(x,f(f(x,y),f(f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y)),x))) = f(x,y) # label(false). [para(869(a,1),875(a,1,2,1))]. 1154 f(x,f(y,f(x,x))) = f(x,x). [para(11(a,1),870(a,1,1))]. 1185 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(y,x),y),y),y),f(y,z)))) = y # label(false). [para(880(a,1),2(a,1,2,1))]. 1232 f(f(x,y),f(y,f(f(f(f(f(x,y),f(y,z)),f(y,z)),y),f(x,y)))) = y # label(false). [para(869(a,1),1052(a,1,2,1))]. 1244 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(y,x),y),y),y),f(z,y)))) = y # label(false). [para(55(a,1),1185(a,1,2,2,2))]. 1245 f(f(x,y),f(f(x,f(x,x)),f(f(f(f(f(x,y),x),x),x),f(x,z)))) = x # label(false). [para(61(a,1),1185(a,1,2,2,1,1,1,1)),rewrite([1082(4)])]. 1271 f(x,f(f(y,x),f(f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x)),x))) = f(y,x) # label(false). [para(870(a,1),1232(a,1,1)),rewrite([870(4),870(12)])]. 1299 f(f(x,f(y,z)),f(f(y,z),f(f(f(f(f(f(y,z),x),z),z),f(y,z)),z))) = f(y,z) # label(false). [para(1076(a,1),7(a,1,2,1))]. 1318 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,y)),x))) = f(x,y). [para(1076(a,1),875(a,1,2,1))]. 1342 f(f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))),x) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))). [para(887(a,1),870(a,1,2))]. 1401 f(f(x,y),f(f(x,f(x,x)),f(f(f(f(f(x,y),x),x),x),f(z,x)))) = x # label(false). [para(61(a,1),1244(a,1,2,2,1,1,1,1)),rewrite([1082(4)])]. 1441 f(f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))),x) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))). [para(892(a,1),870(a,1,2))]. 1442 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = f(f(x,f(x,x)),f(y,x)). [para(982(a,1),1052(a,1,2,2,1,1,1)),rewrite([1154(35)])]. 1443 f(f(f(x,f(x,x)),f(y,x)),x) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))). [back_rewrite(1441),rewrite([1442(15)])]. 1444 f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))) = f(x,f(f(x,f(x,x)),f(y,x))). [back_rewrite(983),rewrite([1442(15)]),flip(a)]. 1447 f(f(f(x,f(x,x)),f(y,x)),x) = f(x,f(f(x,f(x,x)),f(y,x))). [back_rewrite(1443),rewrite([1444(12)])]. 1448 f(f(x,f(f(x,f(x,x)),f(y,x))),f(x,f(f(x,f(x,x)),f(y,x)))) = f(f(x,f(x,x)),f(y,x)). [back_rewrite(1442),rewrite([1444(7),1444(12)])]. 1452 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = f(f(x,f(x,x)),f(x,y)). [para(1024(a,1),1052(a,1,2,2,1,1,1)),rewrite([1154(35)])]. 1453 f(f(f(x,f(x,x)),f(x,y)),x) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))). [back_rewrite(1342),rewrite([1452(15)])]. 1454 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))) = f(x,f(f(x,f(x,x)),f(x,y))). [back_rewrite(1026),rewrite([1452(15)]),flip(a)]. 1456 f(f(f(x,f(x,x)),f(x,y)),x) = f(x,f(f(x,f(x,x)),f(x,y))). [back_rewrite(1453),rewrite([1454(12)])]. 1457 f(f(x,f(f(x,f(x,x)),f(x,y))),f(x,f(f(x,f(x,x)),f(x,y)))) = f(f(x,f(x,x)),f(x,y)). [back_rewrite(1452),rewrite([1454(7),1454(12)])]. 1620 f(f(x,f(y,z)),f(f(y,z),f(f(f(f(f(f(y,z),x),y),y),f(y,z)),y))) = f(y,z) # label(false). [para(1082(a,1),54(a,1,2,1))]. 1642 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),x))) = f(y,x). [para(1082(a,1),924(a,1,2,1))]. 1681 f(f(f(f(x,y),f(f(f(f(y,x),x),f(x,y)),y)),y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(f(x,y),y),f(z,y)))) = y # label(false). [para(1642(a,1),113(a,1,2,1,2,1)),rewrite([1642(18),1642(21)])]. 1712 f(x,f(f(f(f(x,f(x,x)),f(y,x)),f(x,x)),f(f(x,f(x,f(f(x,f(x,x)),f(y,x)))),x))) = f(x,f(f(x,f(x,x)),f(y,x))) # label(false). [para(1447(a,1),921(a,1,2,1,1,1)),rewrite([1447(10),1448(11),1447(11),1447(20)])]. 1736 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(1082(a,1),57(a,1,2,1))]. 2063 f(f(f(x,y),z),f(f(x,y),f(f(f(f(f(f(x,y),z),y),y),f(x,y)),y))) = f(x,y) # label(false). [para(61(a,1),1299(a,1,2,2,1,1,1,1)),rewrite([1082(7)])]. 2096 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),y))) = f(y,x). [para(11(a,1),1620(a,1,2,2,1,1,1,1)),rewrite([870(3)])]. 2232 f(f(x,y),f(f(f(y,x),f(f(y,x),f(y,x))),y)) = y. [para(1154(a,1),891(a,1,2,2)),rewrite([55(15)])]. 2277 f(x,f(f(x,f(x,x)),f(y,x))) = f(y,x). [para(11(a,1),2232(a,1,2,1,1)),rewrite([870(3),11(3),11(3)])]. 2278 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)). [para(20(a,1),2232(a,1,2,1,1)),rewrite([1154(3),20(5),20(6),869(5),880(3)])]. 2280 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y). [para(40(a,1),2232(a,1,2,1,1)),rewrite([869(3),40(3),40(3)])]. 2361 f(x,f(f(f(f(x,f(x,x)),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(1712),rewrite([2277(11),2277(16)])]. 2369 f(f(x,f(x,x)),f(y,x)) = f(f(y,x),f(y,x)). [back_rewrite(1448),rewrite([2277(5),2277(6)]),flip(a)]. 2371 f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))) = f(y,x). [back_rewrite(1444),rewrite([2277(12)])]. 2400 f(f(x,f(x,x)),f(x,y)) = f(f(x,y),f(x,y)). [back_rewrite(1457),rewrite([2280(5),2280(6)]),flip(a)]. 2401 f(f(f(x,f(x,x)),f(x,y)),x) = f(x,y). [back_rewrite(1456),rewrite([2280(10)])]. 2402 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))) = f(x,y). [back_rewrite(1454),rewrite([2280(12)])]. 2681 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),f(f(f(f(x,f(x,x)),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))))) = f(y,x) # label(false). [para(2361(a,1),889(a,1,2,1,1,1)),rewrite([2361(12),2361(16),2361(31)])]. 2730 f(x,f(f(y,f(y,y)),f(x,y))) = f(x,y). [para(2369(a,2),61(a,1,2))]. 2793 f(f(f(x,y),f(f(x,y),f(x,y))),x) = f(x,x). [para(869(a,1),2369(a,1,2)),rewrite([869(9),869(9)])]. 2808 f(f(f(x,f(x,x)),f(y,x)),y) = f(y,x). [para(2369(a,2),1082(a,1,1))]. 2843 f(f(x,y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(y,f(y,y)),f(f(x,y),y)))) = y # label(false). [para(2369(a,2),1102(a,1,2,2))]. 2862 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(f(x,y),f(f(x,y),f(x,y))),f(x,f(x,y))))) = f(x,y) # label(false). [para(2369(a,2),894(a,1,2,2))]. 2870 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(f(y,x),f(f(y,x),f(y,x))),f(x,f(y,x))))) = f(y,x) # label(false). [para(2369(a,2),925(a,1,2,2))]. 2890 f(f(x,x),f(f(x,f(x,x)),f(y,x))) = f(x,f(x,x)). [para(2369(a,1),59(a,1,2,2,2)),rewrite([869(3),880(3),1067(11),1154(3),869(9),1082(7),869(7),55(7)])]. 2896 f(f(f(f(x,f(x,x)),f(f(y,x),f(y,x))),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(2369(a,1),1271(a,1,2,2,1,1,2)),rewrite([2890(9),2278(16)])]. 2931 f(f(f(x,f(x,x)),f(f(y,x),f(y,x))),f(x,f(x,x))) = f(f(x,f(x,x)),f(y,x)). [para(2369(a,1),2401(a,1,1,2)),rewrite([2402(8)])]. 2940 f(f(f(x,y),f(x,y)),f(f(y,f(y,y)),f(f(f(f(f(f(y,f(y,y)),f(x,y)),f(y,y)),f(y,y)),f(y,f(y,y))),f(y,y)))) = f(y,f(y,y)). [para(2369(a,1),2063(a,1,1))]. 2952 f(f(f(x,f(x,x)),f(y,x)),f(x,x)) = f(x,f(x,x)). [back_rewrite(2896),rewrite([2931(9)])]. 2953 f(f(f(x,y),f(x,y)),f(y,y)) = f(y,f(y,y)). [back_rewrite(2940),rewrite([2952(11),40(9),1154(8),869(8),20(6)])]. 2959 f(f(x,f(y,x)),x) = f(y,x) # label(false). [back_rewrite(2681),rewrite([2953(5),2952(10),2730(11),2277(7)])]. 2963 f(x,f(f(x,f(x,x)),f(f(f(y,x),f(f(y,x),f(y,x))),f(x,f(y,x))))) = f(y,x) # label(false). [back_rewrite(2870),rewrite([2953(5)])]. 3063 f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),f(f(f(f(f(f(x,f(x,x)),y),f(x,f(x,x))),f(x,f(x,x))),f(x,f(x,x))),x))) = f(x,f(x,x)). [para(2730(a,1),1245(a,1,2,2)),rewrite([2402(11)])]. 3092 f(f(x,f(y,z)),f(f(y,f(y,y)),f(y,z))) = f(y,z). [para(2400(a,2),11(a,1,2))]. 3101 f(f(f(x,y),z),f(f(x,f(x,x)),f(x,y))) = f(x,y). [para(2400(a,2),40(a,1,2))]. 3102 f(x,f(f(y,f(y,y)),f(y,x))) = f(y,x). [para(2400(a,2),55(a,1,2))]. 3124 f(f(f(x,y),f(x,f(x,x))),f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,f(x,x))),f(x,x)))) = f(x,f(x,x)). [para(2400(a,1),97(a,1,2,2,1,1)),rewrite([3092(18)])]. 3154 f(f(f(x,f(x,x)),f(x,y)),f(x,y)) = f(f(x,y),f(f(x,y),f(x,y))). [para(2400(a,2),880(a,1,1))]. 3164 f(f(x,y),f(z,f(f(x,f(x,x)),f(x,y)))) = f(f(x,y),f(x,y)). [para(2400(a,2),1154(a,1,2,2))]. 3165 f(f(f(x,f(x,x)),f(x,y)),y) = f(x,y). [para(2400(a,2),1076(a,1,1))]. 3305 f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)) = f(f(x,f(x,x)),f(f(x,f(x,x)),y)). [para(2400(a,1),2400(a,1,1,2)),rewrite([2402(8)]),flip(a)]. 3306 f(f(x,f(x,x)),f(f(x,y),f(x,y))) = f(x,y). [para(2400(a,1),2400(a,1,2)),rewrite([2402(8),3092(15)])]. 3331 f(f(x,y),f(f(f(y,y),f(f(y,f(y,f(x,y))),f(y,f(y,f(x,y))))),f(f(f(y,f(y,f(x,y))),y),f(y,z)))) = y # label(false). [para(2959(a,1),53(a,1,1))]. 3336 f(f(x,f(x,f(y,x))),f(f(f(y,x),f(f(y,x),f(y,x))),f(f(f(y,x),f(x,f(y,x))),f(z,f(x,f(y,x)))))) = f(x,f(y,x)). [para(2959(a,1),113(a,1,2,1,2,1)),rewrite([2959(12),2953(12),2959(11)])]. 3353 f(f(f(x,y),x),f(x,y)) = x # label(false). [para(869(a,1),2959(a,1,1,2)),rewrite([869(7)])]. 3354 f(f(f(x,y),y),f(x,y)) = y # label(false). [para(870(a,1),2959(a,1,1,2)),rewrite([870(7)])]. 3360 f(f(x,f(x,y)),x) = f(x,y) # label(false). [para(1082(a,1),2959(a,1,1,2)),rewrite([1082(7)])]. 3365 f(x,f(f(x,y),f(y,x))) = f(x,y). [para(1318(a,1),2959(a,1,1,2)),rewrite([3354(5),3354(10),3353(9),3354(6)]),flip(a)]. 3379 f(f(x,f(y,x)),f(f(f(x,x),f(f(x,f(y,x)),f(x,f(y,x)))),f(f(y,x),f(z,x)))) = x # label(false). [para(2959(a,1),1103(a,1,2,2,1))]. 3426 f(f(x,y),f(f(f(y,y),f(f(y,f(y,f(x,y))),f(y,f(y,f(x,y))))),f(f(y,f(x,y)),f(y,z)))) = y # label(false). [back_rewrite(3331),rewrite([3360(14)])]. 3504 f(f(f(x,y),x),f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,f(x,y)),f(x,y)),f(z,f(x,y))))) = f(x,y). [para(3353(a,1),1401(a,1,2,2,1,1,1))]. 3528 f(f(x,y),f(y,f(x,y))) = y # label(false). [para(2959(a,1),3353(a,1,1))]. 3536 f(f(x,f(x,f(y,x))),f(f(f(y,x),f(f(y,x),f(y,x))),f(x,f(z,f(x,f(y,x)))))) = f(x,f(y,x)). [back_rewrite(3336),rewrite([3528(12)])]. 3599 f(f(f(x,y),f(f(x,y),y)),f(f(f(x,y),y),f(f(f(f(y,f(x,y)),f(x,y)),f(f(x,y),y)),f(x,y)))) = f(f(x,y),y). [para(3354(a,1),1620(a,1,2,2,1,1,1,1))]. 3601 f(x,f(f(y,x),x)) = f(y,x) # label(false). [para(3354(a,1),3353(a,1,1))]. 3661 f(f(x,y),f(f(f(x,x),f(f(x,f(x,f(x,y))),f(x,f(x,f(x,y))))),f(f(x,f(x,y)),f(x,z)))) = x # label(false). [para(3360(a,1),53(a,1,1)),rewrite([3360(14)])]. 3664 f(f(x,y),f(f(f(x,x),f(f(x,f(x,f(x,y))),f(x,f(x,f(x,y))))),f(f(x,f(x,y)),f(z,x)))) = x # label(false). [para(3360(a,1),113(a,1,1)),rewrite([3360(14)])]. 3689 f(f(x,f(x,y)),f(f(f(x,x),f(f(x,f(x,y)),f(x,f(x,y)))),f(f(x,y),f(x,z)))) = x # label(false). [para(3360(a,1),1101(a,1,2,2,1))]. 3691 f(f(x,f(x,y)),f(f(f(x,x),f(f(x,f(x,y)),f(x,f(x,y)))),f(f(x,y),f(z,x)))) = x # label(false). [para(3360(a,1),1103(a,1,2,2,1))]. 3702 f(f(x,y),f(x,f(x,y))) = x # label(false). [para(3360(a,1),3353(a,1,1))]. 3728 f(f(x,y),f(f(f(x,y),f(y,x)),f(f(f(f(f(f(f(x,y),f(y,x)),x),f(x,y)),f(x,y)),f(f(x,y),f(y,x))),f(x,y)))) = f(f(x,y),f(y,x)). [para(3365(a,1),1620(a,1,1))]. 3766 f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),f(x,f(f(f(x,f(x,x)),y),f(x,f(x,x)))))) = f(x,f(x,x)). [para(3102(a,1),1101(a,1,2,2)),rewrite([3305(15),869(15)])]. 3812 f(x,f(f(x,y),f(f(x,y),f(x,y)))) = f(x,x). [para(2793(a,1),1082(a,1,1,1)),rewrite([2793(7),869(3),2793(12)])]. 3818 f(f(f(x,f(x,x)),f(f(x,y),f(f(x,y),f(x,y)))),f(x,y)) = f(f(x,y),f(f(x,y),f(x,y))). [para(2793(a,1),1110(a,1,2,2,1,1,1,2)),rewrite([40(9),2793(12),2277(18)])]. 3829 f(f(f(x,y),f(f(x,y),f(x,y))),f(x,x)) = x. [para(2793(a,1),2400(a,1,2)),rewrite([3306(17),2793(13),2793(14),869(10)])]. 3834 f(f(f(x,y),y),f(f(x,y),y)) = f(f(y,f(y,y)),f(f(x,y),y)). [para(3354(a,1),2793(a,1,1,1)),rewrite([3354(4),3354(4)]),flip(a)]. 3934 f(f(x,y),f(f(f(y,f(x,y)),f(x,y)),f(f(f(y,f(y,f(x,y))),f(f(y,f(x,y)),f(x,y))),f(y,f(x,y))))) = f(f(y,f(x,y)),f(x,y)). [para(3528(a,1),2096(a,1,2,2,1,1,1))]. 4040 f(x,f(f(y,x),f(f(f(f(y,x),f(f(y,x),x)),f(x,x)),f(f(x,x),z)))) = f(x,x) # label(false). [para(3601(a,1),50(a,1,2,1)),rewrite([3601(4)])]. 4104 f(x,f(f(f(f(x,f(x,y)),f(x,f(x,y))),f(f(f(x,y),f(f(x,y),f(x,y))),f(f(x,f(x,y)),f(x,y)))),f(f(x,y),x))) = f(x,f(x,y)). [para(3702(a,1),110(a,1,1)),rewrite([3834(14),3354(23)])]. 4123 f(f(x,y),f(f(x,y),f(x,y))) = f(y,f(y,y)). [para(2369(a,1),3702(a,1,1)),rewrite([2371(10),880(5)])]. 4127 f(f(x,f(x,x)),y) = f(y,y). [para(3702(a,1),2400(a,1,2)),rewrite([4123(5),3702(7),3702(7)])]. 4128 f(x,f(x,x)) = f(y,f(y,y)). [para(2400(a,1),3702(a,1,1)),rewrite([2402(10),880(5),4123(5)])]. 4129 f(f(f(x,f(x,x)),f(x,y)),f(y,f(y,y))) = f(x,y). [para(2400(a,2),3702(a,1,1)),rewrite([4123(9)])]. 4133 f(f(x,f(x,x)),f(x,y)) = f(f(x,y),f(y,f(y,y))). [para(3165(a,1),3702(a,1,1)),rewrite([3165(10),3154(7),4123(6)]),flip(a)]. 4136 f(x,f(f(f(f(x,f(x,y)),f(x,f(x,y))),f(f(y,f(y,y)),f(f(x,f(x,y)),f(x,y)))),f(f(x,y),x))) = f(x,f(x,y)). [back_rewrite(4104),rewrite([4123(10)])]. 4150 f(f(x,f(x,x)),f(y,y)) = y. [back_rewrite(3829),rewrite([4123(5)])]. 4157 f(f(f(x,f(x,x)),f(y,f(y,y))),f(x,y)) = f(y,f(y,y)). [back_rewrite(3818),rewrite([4123(7),4123(12)])]. 4161 f(x,f(y,f(y,y))) = f(x,x). [back_rewrite(3812),rewrite([4123(5)])]. 4179 f(f(x,f(x,f(y,x))),f(f(x,f(x,x)),f(x,f(z,f(x,f(y,x)))))) = f(x,f(y,x)). [back_rewrite(3536),rewrite([4123(8)])]. 4183 f(f(f(x,y),x),f(f(y,f(y,y)),f(f(f(x,f(x,y)),f(x,y)),f(z,f(x,y))))) = f(x,y). [back_rewrite(3504),rewrite([4123(7)])]. 4209 f(x,f(x,f(y,x))) = f(y,x) # label(false). [back_rewrite(2963),rewrite([4123(7),2402(8)])]. 4216 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(y,f(y,y)),f(x,f(x,y))))) = f(x,y) # label(false). [back_rewrite(2862),rewrite([4123(10)])]. 4301 f(x,f(x,x)) = c_0. [new_symbol(4128)]. 4360 f(f(x,y),f(c_0,f(y,f(z,f(y,f(x,y)))))) = f(y,f(x,y)). [back_rewrite(4179),rewrite([4209(3),4301(3)])]. 4362 f(f(x,f(y,x)),f(y,x)) = x # label(false). [back_rewrite(3934),rewrite([4209(8),3601(11),40(11),3528(4)]),flip(a)]. 4373 f(f(x,y),f(f(f(y,y),f(f(x,y),f(x,y))),f(f(y,f(x,y)),f(y,z)))) = y # label(false). [back_rewrite(3426),rewrite([4209(5),4209(6)])]. 4472 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(c_0,f(x,f(x,y))))) = f(x,y) # label(false). [back_rewrite(4216),rewrite([4301(7)])]. 4490 f(f(f(x,y),x),f(c_0,f(f(f(x,f(x,y)),f(x,y)),f(z,f(x,y))))) = f(x,y). [back_rewrite(4183),rewrite([4301(4)])]. 4509 f(x,c_0) = f(x,x). [back_rewrite(4161),rewrite([4301(2)])]. 4513 f(f(c_0,c_0),f(x,y)) = c_0. [back_rewrite(4157),rewrite([4301(2),4301(3),4301(7)])]. 4519 f(c_0,f(x,x)) = x. [back_rewrite(4150),rewrite([4301(2)])]. 4532 f(x,f(f(f(f(x,f(x,y)),c_0),f(c_0,f(f(x,f(x,y)),f(x,y)))),f(f(x,y),x))) = f(x,f(x,y)). [back_rewrite(4136),rewrite([4509(5,R),4301(6)])]. 4534 f(f(x,y),c_0) = f(c_0,f(x,y)). [back_rewrite(4133),rewrite([4301(2),4301(6)]),flip(a)]. 4537 f(c_0,f(c_0,f(x,y))) = f(x,y). [back_rewrite(4129),rewrite([4301(2),4301(5),4534(5)])]. 4538 f(c_0,x) = f(x,x). [back_rewrite(4127),rewrite([4301(2)])]. 4619 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_rewrite(3766),rewrite([4301(2),4538(2),4301(3),4301(4),4538(4),4301(5),4534(5),4519(5),4301(7)])]. 4719 f(f(c_0,f(x,y)),y) = f(x,y). [back_rewrite(3165),rewrite([4301(2)])]. 4720 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [back_rewrite(3164),rewrite([4301(3),4509(9,R),4534(9)])]. 4729 f(f(c_0,f(x,y)),f(x,x)) = c_0. [back_rewrite(3124),rewrite([4301(3),4534(3),4301(5),4301(6),4513(8),4509(7,R),4534(7),4301(9),4534(9),4537(9),40(7),4538(5),4301(7)])]. 4738 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(3102),rewrite([4301(2)])]. 4739 f(f(f(x,y),z),f(c_0,f(x,y))) = f(x,y). [back_rewrite(3101),rewrite([4301(4)])]. 4756 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(3063),rewrite([4301(2),4538(2),4301(3),4301(4),4538(4),4301(5),4534(5),4519(5),4301(4),4509(4),4301(5),4534(5),4519(5),4301(7)])]. 4822 f(f(x,y),f(f(x,y),y)) = y # label(false). [back_rewrite(2843),rewrite([4509(5,R),4534(5),4619(6),4301(4),4537(7)])]. 4825 f(f(c_0,f(x,y)),x) = f(x,y). [back_rewrite(2808),rewrite([4301(2)])]. 4989 f(f(x,y),y) = f(y,f(x,y)). [back_rewrite(3599),rewrite([4822(4),4362(6),3601(5),4509(5,R),4534(5),4739(6)]),flip(a)]. 4998 f(x,f(x,f(x,y))) = f(x,y) # label(false). [back_rewrite(4472),rewrite([4509(3,R),4534(3),4729(5),4537(6)])]. 5001 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(y,z)))) = y # label(false). [back_rewrite(4373),rewrite([4509(5,R),4534(5),4619(6)])]. 5074 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(z,x)))) = x # label(false). [back_rewrite(3691),rewrite([4509(8,R),4534(7),4756(8)])]. 5075 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(x,z)))) = x # label(false). [back_rewrite(3689),rewrite([4509(8,R),4534(7),4756(8)])]. 5087 f(f(x,y),f(c_0,f(f(x,f(x,y)),f(z,x)))) = x # label(false). [back_rewrite(3664),rewrite([4998(5),4998(6),4509(5,R),4534(5),4756(6)])]. 5089 f(f(x,y),f(c_0,f(f(x,f(x,y)),f(x,z)))) = x # label(false). [back_rewrite(3661),rewrite([4998(5),4998(6),4509(5,R),4534(5),4756(6)])]. 5168 f(f(x,f(y,x)),f(c_0,f(f(y,x),f(z,x)))) = x # label(false). [back_rewrite(3379),rewrite([4509(8,R),4534(7),4756(8)])]. 5303 f(f(f(c_0,f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(y,x),f(f(f(y,f(x,y)),f(y,x)),f(f(y,x),u)))) = f(y,x). [back_rewrite(1736),rewrite([4509(4,R),4534(4),4756(5),4989(11)])]. 5312 f(f(f(f(x,y),f(f(f(x,f(y,x)),f(x,y)),y)),y),f(c_0,f(f(y,f(x,y)),f(z,y)))) = y # label(false). [back_rewrite(1681),rewrite([4989(3),4509(12,R),4534(12),4619(13),4989(11)])]. 5472 f(c1,f(c_0,f(c2,c3))) != f(c2,f(c_0,f(c1,c3))) # answer(A_SS). [back_rewrite(3),rewrite([4509(8,R),4534(6),4509(15,R),4534(13)])]. 5474 f(f(x,y),x) = f(x,f(x,y)). [back_rewrite(4532),rewrite([4534(4),4989(9),3702(9),4538(6),4729(6),4738(5)])]. 5499 f(x,f(f(y,x),f(c_0,f(f(x,x),z)))) = f(x,x) # label(false). [back_rewrite(4040),rewrite([4989(4),3528(5),4301(3)])]. 5691 f(f(x,f(x,y)),f(c_0,f(x,f(z,f(x,y))))) = f(x,y) # label(false). [back_rewrite(4490),rewrite([5474(2),4989(7),3702(7)])]. 5748 f(f(x,y),f(f(f(x,y),f(y,x)),f(f(f(f(x,y),f(f(f(f(x,y),f(y,x)),x),f(x,y))),f(f(x,y),f(y,x))),f(x,y)))) = f(f(x,y),f(y,x)). [back_rewrite(3728),rewrite([4989(12)])]. 5992 f(f(f(c_0,f(f(x,f(x,y)),f(x,z))),f(y,x)),f(f(y,x),f(f(f(y,f(x,y)),f(y,x)),f(f(y,x),u)))) = f(y,x). [back_rewrite(5303),rewrite([5474(3)])]. 6152 f(f(f(x,f(y,x)),f(x,z)),x) = f(c_0,f(f(x,f(y,x)),f(x,z))). [para(5001(a,1),870(a,1,2)),rewrite([4509(13,R),5474(8),4537(8)])]. 6153 f(f(c_0,f(f(x,f(y,x)),f(x,z))),f(f(f(c_0,f(f(x,f(y,x)),f(x,z))),f(y,x)),x)) = f(f(c_0,f(f(x,f(y,x)),f(x,z))),f(y,x)). [para(5001(a,1),3365(a,1,2,2))]. 6185 f(f(x,y),f(f(f(x,y),f(f(f(f(x,y),f(y,x)),x),f(x,y))),f(f(x,y),f(y,x)))) = f(f(x,y),f(y,x)). [back_rewrite(5748),rewrite([6152(18),4738(19)])]. 6210 f(f(f(x,y),f(z,x)),x) = f(c_0,f(f(x,y),f(z,x))). [para(5074(a,1),870(a,1,2)),rewrite([4509(11,R),5474(7),4537(7)])]. 6231 f(f(x,y),f(y,x)) = f(c_0,f(x,y)). [back_rewrite(6185),rewrite([6210(6),4825(9),4989(10),3702(10),4509(3,R),4534(3)]),flip(a)]. 6319 f(f(x,x),f(c_0,f(f(x,y),f(x,z)))) = x. [para(5075(a,1),4719(a,1,1,2)),rewrite([4538(2),5075(15)])]. 6388 f(f(f(x,y),f(z,y)),y) = f(c_0,f(f(x,y),f(z,y))). [para(5168(a,1),870(a,1,2)),rewrite([4509(11,R),5474(7),4537(7)])]. 6431 f(f(c_0,f(f(x,y),f(f(f(x,f(y,x)),f(x,y)),y))),f(c_0,f(f(y,f(x,y)),f(z,y)))) = y # label(false). [back_rewrite(5312),rewrite([6388(8)])]. 6686 f(f(x,x),f(f(y,f(x,x)),f(c_0,f(x,z)))) = x # label(false). [para(11(a,1),5499(a,1,2,2,2,1)),rewrite([4509(11,R),4534(11),4519(11)])]. 6736 f(f(c_0,f(x,y)),f(c_0,f(y,x))) = f(y,x). [para(6231(a,1),11(a,1,1)),rewrite([4509(6,R),4534(6)])]. 6737 f(x,y) = f(y,x). [para(6231(a,1),870(a,1,2)),rewrite([4509(3,R),4534(3),6736(7)])]. 6744 f(c_0,f(f(x,y),f(c_0,f(f(x,z),f(x,f(x,y)))))) = f(x,x) # label(false). [para(5087(a,1),6231(a,2,2)),rewrite([6737(5),6737(6),6737(12),6737(13),6737(16),4509(17,R),6737(10),6737(12),4509(12)])]. 6745 f(x,f(f(x,y),f(c_0,f(f(x,z),f(x,f(x,y)))))) = f(x,x) # label(false). [para(5089(a,1),6231(a,1,1)),rewrite([6737(5),6737(8),6737(16),6744(19)])]. 6817 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,y))))) = y # label(false). [back_rewrite(6431),rewrite([6737(3),6737(6),3702(6),4509(4,R),6737(4),4537(5),6737(5),6737(6)])]. 6876 f(f(x,y),f(c_0,f(f(x,z),f(x,f(x,y))))) = x # label(false). [back_rewrite(6153),rewrite([6737(2),6737(5),6737(8),6737(11),6737(13),6737(14),6737(15),6745(15),6737(8),6319(8),6737(2),6737(5),6737(7),6737(8)]),flip(a)]. 6917 f(x,f(f(x,y),f(y,f(z,f(x,y))))) = f(x,y). [back_rewrite(5992),rewrite([6737(5),6737(7),6737(8),6876(8),6737(1),6737(4),6737(5),3528(5),6737(2),6737(3),6737(7)])]. 7102 f(x,f(x,f(y,x))) = f(y,x) # label(false). [para(4360(a,1),3702(a,1,2,2)),rewrite([4360(8),3528(6),6737(3)])]. 7116 f(f(c_0,f(x,y)),f(f(y,y),f(z,f(c_0,f(x,y))))) = f(x,y) # label(false). [para(11(a,1),6686(a,1,2,2,2)),rewrite([4509(3,R),6737(3),4509(6,R),6737(6),6737(9),4509(9),6737(9)])]. 7147 f(f(x,f(y,x)),f(c_0,f(x,f(z,f(y,x))))) = f(y,x) # label(false). [para(6817(a,1),5075(a,1,1,2)),rewrite([6737(2),6817(11),6737(5)])]. 7161 f(f(c_0,f(x,f(y,f(x,z)))),f(f(x,z),f(c_0,f(x,f(y,f(x,z)))))) = f(x,z) # label(false). [para(5691(a,1),7102(a,1,2,2)),rewrite([6737(12),5691(21)])]. 7190 f(f(x,y),f(y,f(z,f(x,y)))) = f(c_0,f(y,f(z,f(x,y)))). [para(7147(a,1),11(a,1,1)),rewrite([4509(12,R),6737(8),4537(8)])]. 7205 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [back_rewrite(6917),rewrite([7190(5)])]. 7566 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(y,x). [para(7205(a,1),7102(a,1,2,2)),rewrite([6737(2),6737(7),6737(11),6737(12),7161(13),6737(3)]),flip(a)]. 7581 f(f(x,x),f(y,f(c_0,f(x,z)))) = x # label(false). [para(7116(a,1),7205(a,1,2,2,2)),rewrite([6737(4),6737(7),6737(8),4720(8),4537(6),869(3),6737(3)]),flip(a)]. 7729 f(x,f(x,f(y,f(c_0,f(x,z))))) = f(y,f(c_0,f(x,z))) # label(false). [para(7581(a,1),3528(a,1,1)),rewrite([7581(10),6737(5)])]. 7758 f(f(c_0,f(x,y)),f(c_0,f(x,z))) = f(z,f(c_0,f(x,y))) # label(false). [para(7581(a,1),7566(a,1,2,2,2)),rewrite([6737(5)])]. 11203 f(f(c_0,f(x,y)),f(f(c_0,f(x,y)),f(y,f(c_0,f(x,z))))) = f(f(c_0,f(x,y)),f(c_0,f(x,z))) # label(false). [para(7758(a,1),7102(a,1,2,2)),rewrite([6737(19)])]. 11204 f(f(c_0,f(x,y)),f(c_0,f(x,z))) = f(y,f(c_0,f(x,z))) # label(false). [para(7758(a,1),7102(a,2)),rewrite([6737(13),4998(15)])]. 11205 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))) # label(false). [para(7758(a,2),7102(a,1,2,2)),rewrite([11204(13),11203(12),11204(7)])]. 11802 f(x,f(c_0,f(y,z))) = f(y,f(c_0,f(x,z))) # label(false). [para(11205(a,1),4998(a,1,2,2)),rewrite([6737(2),7729(6),6737(6)])]. 11803 $F # answer(A_SS). [resolve(11802,a,5472,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=446. Generated=239201. Kept=11801. proofs=1. Usable=143. Sos=2762. Demods=2844. Limbo=3, Disabled=8894. Hints=0. Weight_deleted=43215. Literals_deleted=0. Forward_subsumed=184185. Back_subsumed=1323. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=11662 (3 lex), Back_demodulated=7569. Back_unit_deleted=0. Demod_attempts=12176907. Demod_rewrites=1275501. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=12.00. User_CPU=18.99, System_CPU=0.08, Wall_clock=19. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 17624 exit (max_proofs) Tue Aug 7 10:07:58 2007