============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4443 was started by mccune on cleo.thornwood, Wed Nov 22 12:05:38 2006 The command was "/home/mccune/bin/prover9 -f MOL-A.in MOL-A-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MOL-A.in assign(max_weight,60). assign(new_constants,1). set(lex_order_vars). set(restrict_denials). assign(max_minutes,10). % assign(max_minutes, 10) -> assign(max_seconds, 600). assign(age_part,1). assign(false_part,4). assign(true_part,4). 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(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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 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). 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 (F,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 #3 (F,wt=41): 8 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y. [para(2(a,1),7(a,1,1,2)),rewrite(2(12),2(12),2(14),2(17),2(30))]. given #4 (F,wt=13): 12 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(2(a,1),8(a,1,2,2))]. given #5 (F,wt=9): 20 f(f(x,y),f(y,y)) = y. [para(2(a,1),12(a,1,2,1))]. given #6 (T,wt=11): 46 f(f(x,f(y,y)),y) = f(y,y). [para(20(a,1),7(a,1,2,2,1)),rewrite(20(5),20(5))]. given #7 (T,wt=11): 55 f(f(f(x,x),y),x) = f(x,x). [para(12(a,1),20(a,1,1)),rewrite(12(7)),flip(a)]. given #8 (T,wt=9): 77 f(f(x,y),f(x,x)) = x. [para(20(a,1),55(a,1,1,1)),rewrite(20(6))]. given #9 (T,wt=13): 82 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(2(a,1),77(a,1,1))]. given #10 (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,v)))) = y. [para(2(a,1),2(a,1,2,1))]. given #11 (F,wt=27): 80 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(77(a,1),2(a,1,2,2,1,1))]. given #12 (F,wt=27): 128 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(82(a,1),80(a,1,2,2,2))]. given #13 (F,wt=33): 44 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(20(a,1),7(a,1,2,2,1,1,1,1))]. given #14 (F,wt=31): 157 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(77(a,1),44(a,1,2,2,1,1))]. given #15 (T,wt=13): 91 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(77(a,1),77(a,1,1))]. given #16 (T,wt=15): 57 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(37),rewrite(46(7))]. given #17 (T,wt=15): 184 f(f(x,y),f(y,f(f(y,y),f(z,y)))) = y. [para(82(a,1),57(a,1,2,2,2))]. given #18 (T,wt=17): 180 f(x,f(f(x,x),f(x,f(f(x,x),y)))) = f(x,x). [para(20(a,1),57(a,1,1)),rewrite(77(4))]. given #19 (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)),v),f(f(f(f(x,v),v),f(z,x)),f(f(z,x),w)))) = f(z,x). [para(2(a,1),2(a,1,2,2,1,1,1,1))]. given #20 (F,wt=33): 127 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(82(a,1),80(a,1,2,1,2,1)),rewrite(82(10),82(13))]. given #21 (F,wt=33): 148 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(82(a,1),128(a,1,2,1,2,1)),rewrite(82(10),82(13))]. given #22 (F,wt=33): 168 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(91(a,1),80(a,1,2,1,2,1)),rewrite(91(10),91(13))]. given #23 (F,wt=33): 169 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(91(a,1),128(a,1,2,1,2,1)),rewrite(91(10),91(13))]. given #24 (T,wt=17): 205 f(x,f(f(x,x),f(x,f(y,f(x,x))))) = f(x,x). [para(20(a,1),184(a,1,1)),rewrite(77(4))]. given #25 (T,wt=21): 40 f(f(x,f(y,y)),f(f(y,y),f(y,f(f(y,y),z)))) = f(y,y). [para(20(a,1),2(a,1,2,2,1)),rewrite(20(5))]. given #26 (T,wt=21): 69 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x. [para(55(a,1),2(a,1,2,2,1,1))]. given #27 (T,wt=21): 119 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(46(a,1),80(a,1,2,2,1)),rewrite(82(9))]. given #28 (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,v)))) = y. [para(2(a,1),2(a,1,2,2,1,1,1))]. given #29 (F,wt=35): 115 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(20(a,1),80(a,1,2,1,2,1)),rewrite(20(9),20(11))]. given #30 (F,wt=35): 124 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(77(a,1),80(a,1,2,1,2,1)),rewrite(77(9),77(11))]. given #31 (F,wt=31): 325 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(77(a,1),124(a,1,2,2,2))]. given #32 (F,wt=35): 137 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(20(a,1),128(a,1,2,1,2,1)),rewrite(20(9),20(11))]. given #33 (T,wt=15): 328 f(f(x,f(f(x,x),x)),x) = f(f(x,x),x). [para(119(a,1),124(a,1,2,2,2)),rewrite(77(3),77(11),55(14),20(11))]. given #34 (T,wt=19): 300 f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)) = x. [para(119(a,1),82(a,1,2,1)),rewrite(119(15),119(17))]. given #35 (T,wt=19): 345 f(f(f(x,x),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(20(a,1),328(a,1,1,2,1)),rewrite(77(9))]. given #36 (T,wt=19): 357 f(f(f(f(x,x),x),f(x,f(f(x,x),y))),x) = f(x,x). [para(20(a,1),300(a,1,1,1,2)),rewrite(77(5),77(9))]. given #37 (A,wt=49): 9 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)),v),f(f(f(f(x,v),v),f(z,x)),x))) = f(z,x). [para(2(a,1),7(a,1,2,2,1,1,1,1))]. given #38 (F,wt=35): 146 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(77(a,1),128(a,1,2,1,2,1)),rewrite(77(9),77(11))]. given #39 (F,wt=39): 114 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(20(a,1),80(a,1,2,1,1))]. given #40 (F,wt=39): 136 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(20(a,1),128(a,1,2,1,1))]. given #41 (F,wt=41): 84 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(77(a,1),7(a,1,2,2,1,1))]. given #42 (T,wt=19): 360 f(f(f(x,f(x,x)),f(f(x,x),f(y,x))),f(x,x)) = x. [para(82(a,1),300(a,1,1,2,2))]. given #43 (T,wt=13): 414 f(x,f(f(x,x),f(x,y))) = f(x,x). [para(57(a,1),360(a,1,1,2,2)),rewrite(181(13),181(14),20(7),181(9)),flip(a)]. given #44 (T,wt=13): 415 f(x,f(f(x,x),f(y,x))) = f(x,x). [para(184(a,1),360(a,1,1,2,2)),rewrite(207(13),207(14),20(7),207(9)),flip(a)]. given #45 (T,wt=13): 416 f(f(x,x),f(x,f(f(x,x),y))) = x. [para(180(a,1),360(a,1,1,2,2)),rewrite(270(16),270(18),77(10),46(8),270(12),77(3)),flip(a)]. given #46 (A,wt=59): 10 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)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(f(f(y,z),w),v),v),f(y,z)),z))))) = f(y,z). [para(7(a,1),7(a,1,1,2)),rewrite(7(17),7(18),7(21),7(25),7(42))]. given #47 (F,wt=39): 406 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(69(a,1),84(a,1,1,2)),rewrite(69(10),69(10),69(11),69(12),69(15),69(16),69(27))]. given #48 (F,wt=39): 491 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(82(a,1),406(a,1,2,2,2,2,2))]. given #49 (F,wt=41): 125 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(77(a,1),80(a,1,2,2,2))]. given #50 (F,wt=41): 155 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(55(a,1),44(a,1,2,2,1,1)),rewrite(77(3))]. given #51 (T,wt=13): 442 f(f(x,x),f(x,f(y,f(x,x)))) = x. [para(20(a,1),415(a,1,2,1)),rewrite(77(8))]. given #52 (T,wt=19): 373 f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x) = f(x,x). [para(82(a,1),357(a,1,1,2,2))]. given #53 (T,wt=19): 539 f(f(f(f(x,x),x),f(f(x,x),x)),x) = f(f(x,x),x). [para(44(a,1),442(a,1,2,2)),rewrite(263(13),55(14),77(11)),flip(a)]. given #54 (T,wt=21): 138 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x. [para(20(a,1),128(a,1,2,1,2))]. given #55 (A,wt=59): 11 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)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(z,v),v),f(y,z)),f(f(y,z),w)))))) = f(y,z). [para(2(a,1),8(a,1,2,2,2,2,1,1,1,1))]. given #56 (F,wt=41): 324 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(55(a,1),124(a,1,2,2,2)),rewrite(77(3),77(11))]. given #57 (F,wt=45): 62 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(46(a,1),7(a,1,2,2,1,1,1,1))]. given #58 (F,wt=45): 118 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(46(a,1),80(a,1,2,1,2,1)),rewrite(46(12),77(11),46(12))]. given #59 (F,wt=45): 121 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(55(a,1),80(a,1,2,1,2,1)),rewrite(55(12),77(11),55(12))]. given #60 (T,wt=21): 142 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(46(a,1),128(a,1,2,2,1)),rewrite(82(9))]. given #61 (T,wt=21): 287 f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x)) = x. [para(69(a,1),82(a,1,2,1)),rewrite(69(16),69(18))]. given #62 (T,wt=21): 421 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)). [para(2(a,1),414(a,1,2,2))]. given #63 (T,wt=21): 426 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)). [para(77(a,1),414(a,1,2,2))]. given #64 (A,wt=57): 13 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(f(f(y,y),w),f(f(f(f(f(y,v6),w),w),y),f(y,v7)))))))) = y. [para(8(a,1),7(a,1,1,2)),rewrite(8(20),8(20),8(22),8(25),8(46))]. given #65 (F,wt=45): 141 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(46(a,1),128(a,1,2,1,2,1)),rewrite(46(12),77(11),46(12))]. given #66 (F,wt=45): 144 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(55(a,1),128(a,1,2,1,2,1)),rewrite(55(12),77(11),55(12))]. given #67 (F,wt=45): 490 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(82(a,1),406(a,1,2,1,2,1)),rewrite(82(10),82(13))]. given #68 (F,wt=45): 492 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(91(a,1),406(a,1,2,1,2,1)),rewrite(91(10),91(13))]. given #69 (T,wt=15): 663 f(f(x,f(x,f(x,x))),x) = f(x,f(x,x)). [para(2(a,1),141(a,1,2))]. given #70 (T,wt=19): 675 f(f(f(x,x),f(f(x,x),x)),f(x,x)) = f(f(x,x),x). [para(20(a,1),663(a,1,1,2,2)),rewrite(77(10))]. given #71 (T,wt=21): 542 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(y,x)))) = x. [back_rewrite(247),rewrite(539(6))]. given #72 (T,wt=19): 704 f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(542(a,1),82(a,1,2,1)),rewrite(542(15),542(17))]. given #73 (A,wt=31): 35 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(20(a,1),2(a,1,1)),rewrite(20(3))]. given #74 (F,wt=45): 510 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(82(a,1),491(a,1,2,1,2,1)),rewrite(82(10),82(13))]. given #75 (F,wt=45): 511 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(91(a,1),491(a,1,2,1,2,1)),rewrite(91(10),91(13))]. given #76 (F,wt=49): 237 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(20(a,1),127(a,1,2,1,1))]. given #77 (F,wt=49): 246 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(20(a,1),148(a,1,2,1,1))]. given #78 (T,wt=19): 717 f(f(f(x,f(x,x)),f(x,f(y,f(x,x)))),x) = f(x,x). [para(20(a,1),704(a,1,1,1,1)),rewrite(77(5),77(9))]. given #79 (T,wt=19): 721 f(f(f(x,f(x,x)),f(x,f(f(x,x),x))),x) = f(x,x). [para(675(a,1),704(a,1,1,2,2)),rewrite(77(3),77(5),77(9))]. given #80 (T,wt=21): 543 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(x,y)))) = x. [back_rewrite(238),rewrite(539(6))]. given #81 (T,wt=19): 769 f(f(f(f(x,x),x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(543(a,1),82(a,1,2,1)),rewrite(543(15),543(17))]. given #82 (A,wt=33): 36 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(20(a,1),2(a,1,2,1,1))]. given #83 (F,wt=49): 253 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(20(a,1),168(a,1,2,1,1))]. given #84 (F,wt=49): 257 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(20(a,1),169(a,1,2,1,1))]. given #85 (F,wt=49): 396 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(80(a,1),84(a,1,2,1,2,1)),rewrite(80(27),80(29))]. given #86 (F,wt=49): 398 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(128(a,1),84(a,1,2,1,2,1)),rewrite(128(27),128(29))]. given #87 (T,wt=19): 783 f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),x) = f(x,x). [para(20(a,1),769(a,1,1,1,1)),rewrite(77(5),77(9))]. given #88 (T,wt=21): 554 f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(20(a,1),539(a,1,1,1,1)),rewrite(77(5),77(10))]. given #89 (T,wt=21): 565 f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(x,x)) = x. [para(138(a,1),82(a,1,2,1)),rewrite(138(16),138(18))]. given #90 (T,wt=21): 644 f(f(x,x),f(x,f(f(f(x,x),x),f(x,f(f(x,x),y))))) = x. [para(357(a,1),426(a,1,1)),rewrite(357(8),357(9),77(4),357(16),357(17),77(12))]. given #91 (A,wt=37): 38 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(20(a,1),2(a,1,2,2,1,1,1,1))]. given #92 (F,wt=51): 234 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),127(a,1,2,2,2))]. given #93 (F,wt=51): 240 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(77(a,1),127(a,1,2,2,2))]. given #94 (F,wt=51): 252 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),168(a,1,2,2,2))]. given #95 (F,wt=51): 256 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(77(a,1),168(a,1,2,2,2))]. given #96 (T,wt=21): 645 f(f(x,x),f(x,f(f(f(x,x),x),f(x,f(y,f(x,x)))))) = x. [para(373(a,1),426(a,1,1)),rewrite(373(8),373(9),77(4),373(16),373(17),77(12))]. given #97 (T,wt=21): 754 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(y,f(x,x)))))) = x. [para(717(a,1),426(a,1,1)),rewrite(717(8),717(9),77(4),717(16),717(17),77(12))]. given #98 (T,wt=21): 814 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y))))) = x. [para(783(a,1),426(a,1,1)),rewrite(783(8),783(9),77(4),783(16),783(17),77(12))]. given #99 (T,wt=23): 116 f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(20(a,1),80(a,1,2,2,1)),rewrite(77(5),82(8))]. given #100 (A,wt=25): 39 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(20(a,1),2(a,1,2,2,1,1,1))]. given #101 (F,wt=47): 923 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(39(a,1),84(a,1,2,1,2,1)),rewrite(39(25),39(27))]. given #102 (F,wt=47): 934 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(82(a,1),923(a,1,1,1,2,2))]. given #103 (F,wt=51): 482 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(20(a,1),406(a,1,2,1,1)),rewrite(77(15),77(17))]. given #104 (F,wt=51): 502 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(20(a,1),491(a,1,2,1,1)),rewrite(77(15),77(17))]. given #105 (T,wt=19): 930 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(565(a,1),39(a,1,2,2,1)),rewrite(20(4),77(3),82(6))]. given #106 (T,wt=19): 951 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(20(a,1),930(a,1,2,1,1)),rewrite(77(7),77(11))]. given #107 (T,wt=19): 952 f(x,f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(82(a,1),930(a,1,2,2,2))]. given #108 (T,wt=19): 962 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(82(a,1),951(a,1,2,2,2))]. given #109 (A,wt=33): 45 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z). [para(20(a,1),7(a,1,2,2,1,1,1))]. given #110 (F,wt=55): 933 f(f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))),f(f(y,y),x)),f(f(f(f(f(y,y),x),f(f(y,y),x)),f(x,x)),f(f(x,f(f(y,y),x)),x))) = f(f(y,y),x) # label(false). [para(20(a,1),923(a,1,1,1,1,2)),rewrite(77(6))]. given #111 (F,wt=55): 935 f(f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x))),f(f(y,y),x)),f(f(f(f(f(y,y),x),f(f(y,y),x)),f(x,x)),f(f(x,f(f(y,y),x)),x))) = f(f(y,y),x) # label(false). [para(20(a,1),934(a,1,1,1,1,2)),rewrite(77(6))]. given #112 (F,wt=59): 399 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)),f(f(f(f(y,z),f(y,z)),f(z,z)),f(f(z,f(y,z)),z))))) = f(y,z) # label(false). [para(157(a,1),84(a,1,1,2)),rewrite(157(15),157(16),157(18),157(20),157(24),157(26),157(40))]. given #113 (F,wt=49): 1024 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(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))))) = f(y,x) # label(false). [para(20(a,1),399(a,1,2,1,2,1)),rewrite(20(9),20(11))]. given #114 (T,wt=15): 983 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x. [para(80(a,1),45(a,1,2,2,1)),rewrite(77(3),82(6),20(6),930(7),77(4),82(7),20(7),77(10),82(13),20(13),20(21),416(21),46(17),77(3),77(3),82(6),20(6)),flip(a)]. given #115 (T,wt=15): 985 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x. [para(128(a,1),45(a,1,2,2,1)),rewrite(77(3),82(6),20(6),952(7),77(4),82(7),20(7),77(10),82(13),20(13),20(21),442(21),46(17),77(3),77(3),82(6),20(6)),flip(a)]. given #116 (T,wt=15): 1016 f(f(x,f(x,x)),f(x,f(f(x,x),y))) = x. [para(39(a,1),45(a,1,2,2,1)),rewrite(77(3),77(6),77(10),77(13),77(16),77(19),77(27),416(27),46(23),77(9),77(3),77(6)),flip(a)]. given #117 (T,wt=15): 1058 f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. [para(82(a,1),1016(a,1,2,2))]. given #118 (A,wt=49): 47 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,u),f(f(f(f(f(f(x,x),v),u),u),f(x,x)),f(f(x,x),w)))))) = f(x,x). [para(20(a,1),8(a,1,1)),rewrite(20(3),20(11))]. Demod_limit: f(f(f(f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w))))),f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w)))))),f(x,x)),f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w))))),v6))),f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w))))))),f(f(f(f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w)))))),f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w))))))),f(f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w))))),f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w))))))),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w))))),f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w))))))),f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w)))))))) = f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(z,f(x,f(x,x)))),y),y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),u),f(f(f(f(f(f(f(x,f(x,x)),f(x,f(x,x))),v),u),u),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(x,f(x,x))),w)))))). [para(47(a,1),923(a,1,1,1,2,1))]. Demod_limit (steps=-1, size=1179). The most recent kept clause is 1097. From here on, a short message will be printed for each 100 times the limit is hit. given #119 (F,wt=59): 408 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)),f(f(f(f(y,z),f(y,z)),f(y,y)),f(f(y,f(y,z)),y))))) = f(y,z) # label(false). [para(325(a,1),84(a,1,1,2)),rewrite(325(15),325(16),325(18),325(20),325(24),325(26),325(40))]. given #120 (F,wt=49): 1103 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(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),x))))) = f(x,y) # label(false). [para(77(a,1),408(a,1,2,1,2,1)),rewrite(77(9),77(11))]. given #121 (F,wt=59): 483 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(f(f(y,x),f(y,x)),f(y,x)),f(f(f(f(y,x),f(y,x)),f(y,x)),f(f(y,x),z)))))) = f(y,x) # label(false). [para(20(a,1),406(a,1,2,1,2,1)),rewrite(20(9),20(11))]. given #122 (F,wt=55): 1107 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(f(f(y,x),f(y,x)),f(y,x)),f(f(f(f(y,x),f(y,x)),f(y,x)),x))))) = f(y,x) # label(false). [para(2(a,1),483(a,1,2,2,2,2,2))]. given #123 (T,wt=17): 1017 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x). [para(951(a,1),45(a,1,1)),rewrite(77(16),77(18),119(23),414(18),20(16)),flip(a)]. given #124 (T,wt=17): 1018 f(f(x,f(x,x)),f(f(x,x),f(y,x))) = f(x,x). [para(962(a,1),45(a,1,1)),rewrite(77(16),77(18),142(23),415(18),20(16)),flip(a)]. given #125 (T,wt=17): 1057 f(f(f(x,x),x),f(f(x,x),f(x,y))) = f(x,x). [para(20(a,1),1016(a,1,1,2)),rewrite(77(6))]. given #126 (T,wt=17): 1074 f(f(f(x,x),x),f(f(x,x),f(y,x))) = f(x,x). [para(20(a,1),1058(a,1,1,2)),rewrite(77(6))]. given #127 (A,wt=51): 48 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,u),f(f(f(f(f(f(y,y),v),u),u),f(y,y)),f(f(y,y),w)))))) = f(y,y). [para(20(a,1),8(a,1,2,1,1)),rewrite(20(12))]. given #128 (F,wt=59): 488 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(f(f(x,y),f(x,y)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(x,y),z)))))) = f(x,y) # label(false). [para(77(a,1),406(a,1,2,1,2,1)),rewrite(77(9),77(11))]. given #129 (F,wt=55): 1176 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(f(f(x,y),f(x,y)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,y)),x))))) = f(x,y) # label(false). [para(77(a,1),488(a,1,2,2,2,2,2))]. given #130 (F,wt=59): 503 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(f(f(y,x),f(y,x)),f(y,x)),f(f(f(f(y,x),f(y,x)),f(y,x)),f(z,f(y,x))))))) = f(y,x) # label(false). [para(20(a,1),491(a,1,2,1,2,1)),rewrite(20(9),20(11))]. given #131 (F,wt=59): 508 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(f(f(x,y),f(x,y)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,y)),f(z,f(x,y))))))) = f(x,y) # label(false). [para(77(a,1),491(a,1,2,1,2,1)),rewrite(77(9),77(11))]. given #132 (T,wt=21): 1125 f(f(f(f(x,x),f(x,y)),f(x,f(x,x))),x) = f(x,f(x,x)). [para(1017(a,1),125(a,1,2,1,2,1)),rewrite(1017(18),77(14),1017(18),55(17),20(14))]. given #133 (T,wt=21): 1140 f(f(f(f(x,x),f(y,x)),f(x,f(x,x))),x) = f(x,f(x,x)). [para(1018(a,1),125(a,1,2,1,2,1)),rewrite(1018(18),77(14),1018(18),55(17),20(14))]. given #134 (T,wt=21): 1154 f(f(f(f(x,x),f(x,y)),f(f(x,x),x)),x) = f(f(x,x),x). [para(1057(a,1),84(a,1,2,1,2,1)),rewrite(1057(18),77(14),539(12),1057(14),55(13),20(10))]. given #135 (T,wt=21): 1163 f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),x) = f(f(x,x),x). [para(1074(a,1),84(a,1,2,1,2,1)),rewrite(1074(18),77(14),539(12),1074(14),55(13),20(10))]. given #136 (A,wt=41): 50 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(20(a,1),8(a,1,2,2,1,1,1))]. given #137 (F,wt=23): 236 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [para(20(a,1),127(a,1,1,1,1)),rewrite(20(3),77(3),77(3),20(3),20(3),20(5))]. given #138 (F,wt=23): 245 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [para(20(a,1),148(a,1,1,1,1)),rewrite(20(3),77(3),77(3),20(3),20(3),20(5))]. given #139 (F,wt=23): 453 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(416(a,1),2(a,1,2,2,1,1,1)),rewrite(416(6))]. given #140 (F,wt=23): 532 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(x,z)))) = x. [para(442(a,1),2(a,1,2,2,1,1,1)),rewrite(442(6))]. given #141 (T,wt=23): 610 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))),x) = f(x,x). [para(20(a,1),287(a,1,1,1,1)),rewrite(77(5),77(11))]. given #142 (T,wt=23): 822 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x). [para(20(a,1),565(a,1,1,1,1)),rewrite(77(5),77(11))]. given #143 (T,wt=23): 1040 f(f(f(x,f(f(x,x),y)),f(f(x,x),x)),f(x,x)) = f(f(x,x),x). [para(983(a,1),125(a,1,2,1,2,1)),rewrite(983(17),983(19),77(18),46(14))]. given #144 (T,wt=23): 1050 f(f(f(x,f(y,f(x,x))),f(f(x,x),x)),f(x,x)) = f(f(x,x),x). [para(985(a,1),125(a,1,2,1,2,1)),rewrite(985(17),985(19),77(18),46(14))]. given #145 (A,wt=41): 52 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),f(u,u)),f(f(f(u,f(u,u)),y),f(y,v)))))) = y. [para(20(a,1),8(a,1,2,2,2,2,1,1,1))]. given #146 (F,wt=23): 1063 f(f(f(x,f(f(x,x),y)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(1016(a,1),84(a,1,2,1,2,1)),rewrite(1016(17),554(13),1016(14),77(13),46(9))]. given #147 (F,wt=23): 1079 f(f(f(x,f(y,f(x,x))),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(1058(a,1),84(a,1,2,1,2,1)),rewrite(1058(17),554(13),1058(14),77(13),46(9))]. given #148 (F,wt=23): 1260 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(82(a,1),453(a,1,2,2,2))]. given #149 (F,wt=17): 1336 f(f(x,x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(82(a,1),1260(a,1,2))]. given #150 (T,wt=17): 1348 f(f(x,x),f(f(x,f(x,f(y,f(x,x)))),x)) = x. [para(82(a,1),1336(a,1,2,1,2,2))]. given #151 (T,wt=21): 1347 f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x))) = f(x,x). [para(20(a,1),1336(a,1,1)),rewrite(77(5))]. given #152 (T,wt=21): 1363 f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x))) = f(x,x). [para(20(a,1),1348(a,1,1)),rewrite(77(5))]. given #153 (T,wt=23): 1268 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(z,x)))) = x. [para(82(a,1),532(a,1,2,2,2))]. given #154 (A,wt=29): 58 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(46(a,1),2(a,1,1))]. given #155 (F,wt=25): 60 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(46(a,1),2(a,1,2,2,1,1,1))]. given #156 (F,wt=23): 1403 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))),f(x,x)) = x. [para(60(a,1),82(a,1,2,1)),rewrite(60(19),60(21))]. given #157 (F,wt=23): 1428 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x))),f(x,x)) = x. [para(82(a,1),1403(a,1,1,2,2))]. given #158 (F,wt=25): 96 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(82(a,1),2(a,1,2,2,2))]. given #159 (T,wt=25): 97 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),82(a,1,2,1)),rewrite(2(20),2(22))]. given #160 (T,wt=23): 1573 f(f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z))),x) = f(x,x). [para(983(a,1),97(a,1,1,2,1,1,1)),rewrite(77(3),77(10),77(11))]. given #161 (T,wt=23): 1574 f(f(f(x,f(x,f(y,f(x,x)))),f(x,f(f(x,x),z))),x) = f(x,x). [para(985(a,1),97(a,1,1,2,1,1,1)),rewrite(77(3),77(10),77(11))]. given #162 (T,wt=23): 1585 f(f(f(x,f(x,f(f(x,x),y))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(82(a,1),1573(a,1,1,2,2))]. given #163 (A,wt=49): 59 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(46(a,1),2(a,1,2,2,1,1,1,1))]. given #164 (F,wt=23): 1594 f(f(f(x,f(x,f(y,f(x,x)))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(82(a,1),1574(a,1,1,2,2))]. given #165 (F,wt=25): 225 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(20(a,1),5(a,1,2,1,1)),rewrite(97(11))]. given #166 (F,wt=25): 915 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(39(a,1),82(a,1,2,1)),rewrite(39(20),39(22))]. given #167 (F,wt=25): 917 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(82(a,1),39(a,1,2,2,2))]. given #168 (T,wt=25): 1052 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(1016(a,1),2(a,1,2,2,1,1,1)),rewrite(416(7))]. given #169 (T,wt=25): 1069 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(x,z)))) = x. [para(1058(a,1),2(a,1,2,2,1,1,1)),rewrite(442(7))]. given #170 (T,wt=25): 1182 f(f(x,x),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,y)))) = x. [para(1125(a,1),2(a,1,2,2,1))]. given #171 (T,wt=11): 1699 f(f(x,x),f(x,f(x,x))) = x. [para(20(a,1),1182(a,1,2))]. given #172 (A,wt=45): 61 f(f(f(x,y),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(f(f(x,y),f(u,f(f(x,y),f(x,y)))),z),z),f(x,y)),y))) = f(x,y). [para(46(a,1),7(a,1,1))]. given #173 (F,wt=29): 1751 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,f(y,y))),f(y,f(y,y))),y),f(y,z)))) = y # label(false). [para(1699(a,1),2(a,1,2,1))]. given #174 (F,wt=29): 1780 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,f(y,y))),f(y,f(y,y))),y),f(z,y)))) = y # label(false). [para(1699(a,1),96(a,1,2,1))]. given #175 (F,wt=23): 1860 f(f(x,y),f(f(f(f(y,x),f(y,f(y,y))),f(y,f(y,y))),y)) = y # label(false). [para(82(a,1),1780(a,1,2))]. given #176 (F,wt=29): 1911 f(f(f(f(x,y),f(x,y)),y),f(f(f(f(x,y),f(y,f(y,y))),f(y,f(y,y))),y)) = y # label(false). [para(82(a,1),1860(a,1,2,1,1,1))]. given #177 (T,wt=11): 1755 f(x,f(f(x,x),x)) = f(x,x). [para(20(a,1),1699(a,1,1)),rewrite(77(4))]. given #178 (T,wt=17): 1703 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,y)))) = x. [para(1182(a,1),82(a,1,2,1)),rewrite(1699(4),1699(10),414(13),77(7),1699(5)),flip(a)]. given #179 (T,wt=17): 1704 f(f(x,x),f(x,f(f(x,f(x,x)),f(y,x)))) = x. [para(82(a,1),1182(a,1,2,2,2)),rewrite(1699(5))]. given #180 (T,wt=19): 1711 f(f(f(x,f(x,x)),f(x,f(x,x))),x) = f(x,f(x,x)). [para(1016(a,1),1182(a,1,2,2,2)),rewrite(1699(19),822(16),77(9))]. given #181 (A,wt=33): 63 f(f(f(x,x),f(y,z)),f(f(f(f(y,z),f(y,z)),x),f(f(f(f(x,x),x),f(y,z)),z))) = f(y,z). [para(46(a,1),7(a,1,2,2,1,1,1))]. given #182 (F,wt=29): 1918 f(f(f(f(x,y),f(x,y)),x),f(f(f(f(x,y),f(x,f(x,x))),f(x,f(x,x))),x)) = x # label(false). [para(91(a,1),1860(a,1,2,1,1,1))]. given #183 (F,wt=31): 1902 f(f(x,f(y,y)),f(f(f(f(f(y,y),x),f(f(y,y),y)),f(f(y,y),y)),f(y,y))) = f(y,y) # label(false). [para(20(a,1),1860(a,1,2,1,1,2,2)),rewrite(77(11))]. given #184 (F,wt=35): 1816 f(f(f(f(x,y),f(x,y)),y),f(y,f(f(f(f(f(x,y),f(y,f(y,y))),f(y,f(y,y))),y),f(y,z)))) = y # label(false). [para(82(a,1),1751(a,1,2,2,1,1,1,1))]. given #185 (F,wt=35): 1819 f(f(f(f(x,y),f(x,y)),x),f(x,f(f(f(f(f(x,y),f(x,f(x,x))),f(x,f(x,x))),x),f(x,z)))) = x # label(false). [para(91(a,1),1751(a,1,2,2,1,1,1,1))]. given #186 (T,wt=21): 1712 f(f(f(f(x,x),x),f(f(x,x),x)),f(x,x)) = f(f(x,x),x). [para(1057(a,1),1182(a,1,2,2,2)),rewrite(1699(19),565(17),55(8))]. given #187 (T,wt=21): 1767 f(x,f(f(x,x),f(f(f(x,x),x),f(f(x,x),y)))) = f(x,x). [para(1699(a,1),35(a,1,2,2,1,1,1)),rewrite(77(4),1755(3),77(6),675(7))]. given #188 (T,wt=21): 1864 f(x,f(f(x,x),f(f(f(x,x),x),f(y,f(x,x))))) = f(x,x). [para(69(a,1),1780(a,1,2,2,1,1,1,1)),rewrite(287(9),77(5),1755(4),77(6),675(7))]. given #189 (T,wt=23): 1916 f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,f(x,x))),x) = f(x,x). [para(1860(a,1),44(a,1,2,2,1)),rewrite(20(33),55(12)),flip(a)]. given #190 (A,wt=45): 64 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(f(f(x,x),u),f(f(f(f(f(x,v),u),u),x),f(x,w)))))) = x. [para(46(a,1),8(a,1,1))]. given #191 (F,wt=35): 1859 f(f(f(f(x,y),f(x,y)),y),f(y,f(f(f(f(f(x,y),f(y,f(y,y))),f(y,f(y,y))),y),f(z,y)))) = y # label(false). [para(82(a,1),1780(a,1,2,2,1,1,1,1))]. given #192 (F,wt=35): 1863 f(f(f(f(x,y),f(x,y)),x),f(x,f(f(f(f(f(x,y),f(x,f(x,x))),f(x,f(x,x))),x),f(z,x)))) = x # label(false). [para(91(a,1),1780(a,1,2,2,1,1,1,1))]. given #193 (F,wt=41): 1811 f(f(x,f(y,y)),f(f(y,y),f(f(f(f(f(f(y,y),x),f(f(y,y),y)),f(f(y,y),y)),f(y,y)),f(f(y,y),z)))) = f(y,y) # label(false). [para(20(a,1),1751(a,1,2,2,1,1,1,2,2)),rewrite(77(12))]. given #194 (F,wt=41): 1853 f(f(x,f(y,y)),f(f(y,y),f(f(f(f(f(f(y,y),x),f(f(y,y),y)),f(f(y,y),y)),f(y,y)),f(z,f(y,y))))) = f(y,y) # label(false). [para(20(a,1),1780(a,1,2,2,1,1,1,2,2)),rewrite(77(12))]. given #195 (T,wt=23): 1922 f(f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)),f(x,x)) = x. [para(1860(a,1),62(a,1,2,2,1)),rewrite(77(4),77(6),77(9),77(15),77(17),77(20),77(25),77(27),77(30),77(37),46(35),77(13),77(4),77(6),77(9)),flip(a)]. given #196 (T,wt=25): 1212 f(f(x,x),f(f(f(x,x),f(f(x,x),x)),f(f(f(x,x),x),f(x,y)))) = x. [para(1163(a,1),2(a,1,2,2,1))]. given #197 (T,wt=25): 1223 f(x,f(f(x,f(x,f(x,x))),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [para(1163(a,1),35(a,1,2,2,1)),rewrite(77(3),77(6))]. given #198 (T,wt=25): 1405 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(f(x,x),x),y),f(z,y)))) = y. [para(82(a,1),60(a,1,2,2,2))]. given #199 (A,wt=41): 65 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(f(x,x),x),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(46(a,1),8(a,1,2,2,1,1,1))]. given #200 (F,wt=41): 1901 f(f(f(x,x),f(y,x)),f(f(f(x,f(f(y,x),f(f(y,x),f(y,x)))),f(f(y,x),f(f(y,x),f(y,x)))),f(y,x))) = f(y,x) # label(false). [para(20(a,1),1860(a,1,2,1,1,1))]. given #201 (F,wt=41): 1909 f(f(f(x,x),f(x,y)),f(f(f(x,f(f(x,y),f(f(x,y),f(x,y)))),f(f(x,y),f(f(x,y),f(x,y)))),f(x,y))) = f(x,y) # label(false). [para(77(a,1),1860(a,1,2,1,1,1))]. given #202 (F,wt=41): 1956 f(f(f(f(x,f(y,y)),f(x,f(y,y))),f(y,y)),f(f(f(f(x,f(y,y)),f(f(y,y),y)),f(f(y,y),y)),f(y,y))) = f(y,y) # label(false). [para(20(a,1),1911(a,1,2,1,1,2,2)),rewrite(77(16))]. given #203 (F,wt=41): 1961 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(f(x,x),x)),f(f(f(f(x,x),f(f(x,x),x)),f(y,x)),x))) = f(y,x) # label(false). [para(1755(a,1),44(a,1,2,2,1,1,1))]. given #204 (T,wt=25): 1423 f(f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(20(a,1),1403(a,1,1,1,1)),rewrite(77(12))]. given #205 (T,wt=25): 1439 f(f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(z,f(x,x)))),x) = f(x,x). [para(20(a,1),1428(a,1,1,1,1)),rewrite(77(12))]. given #206 (T,wt=25): 1440 f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [para(20(a,1),1428(a,1,1,2,1,1,1))]. given #207 (T,wt=25): 1460 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x))),f(x,x)) = x. [para(96(a,1),82(a,1,2,1)),rewrite(96(20),96(22))]. given #208 (A,wt=39): 66 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(u,u),u),y),f(y,v)))))) = y. [para(46(a,1),8(a,1,2,2,2,2,1,1,1))]. given #209 (F,wt=41): 2049 f(f(f(f(f(x,x),y),f(f(x,x),y)),f(x,x)),f(f(f(f(f(x,x),y),f(f(x,x),x)),f(f(x,x),x)),f(x,x))) = f(x,x) # label(false). [para(20(a,1),1918(a,1,2,1,1,2,2)),rewrite(77(16))]. given #210 (F,wt=41): 2128 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(f(y,y),y),f(f(y,y),y)),f(f(y,y),y))))) = y # label(false). [para(1922(a,1),125(a,1,1,2)),rewrite(1922(11),1922(11),1922(12),1922(13),1922(16),1922(17),1922(29))]. given #211 (F,wt=43): 2138 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),f(f(y,y),y)),f(f(f(y,y),y),f(y,z)))))) = y # label(false). [para(1212(a,1),84(a,1,1,2)),rewrite(1212(12),1212(12),1212(13),1212(14),1212(17),1212(18),1212(31))]. given #212 (F,wt=43): 2374 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),f(f(y,y),y)),f(f(f(y,y),y),f(z,y)))))) = y # label(false). [para(82(a,1),2138(a,1,2,2,2,2,2))]. given #213 (T,wt=25): 1475 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(z,f(x,x))))) = f(x,x). [para(69(a,1),96(a,1,2,2,1,1,1,1)),rewrite(287(9),77(3))]. given #214 (T,wt=25): 1514 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(1016(a,1),96(a,1,2,2,1,1,1)),rewrite(416(7))]. given #215 (T,wt=19): 2448 f(f(f(x,x),x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(82(a,1),1514(a,1,2))]. given #216 (T,wt=15): 2470 f(f(x,f(x,f(f(x,x),y))),x) = f(x,x). [para(2448(a,1),44(a,1,2,2,1)),rewrite(1336(7),20(14)),flip(a)]. given #217 (A,wt=29): 67 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(55(a,1),2(a,1,1))]. given #218 (F,wt=43): 2499 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(y,f(y,f(f(y,y),z)))))) = f(y,y) # label(false). [para(2470(a,1),125(a,1,1,2)),rewrite(2470(7),2470(8),77(5),2470(7),2470(9),2470(13),2470(15),2470(24))]. given #219 (F,wt=35): 2548 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(f(y,y),f(f(y,y),f(y,z)))))) = y # label(false). [para(20(a,1),2499(a,1,1,2)),rewrite(77(5),77(6),77(9),77(10),77(13),77(19))]. given #220 (F,wt=35): 2590 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(f(y,y),f(f(y,y),f(z,y)))))) = y # label(false). [para(82(a,1),2548(a,1,2,2,2,2,2))]. given #221 (F,wt=41): 2589 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(y,y),f(f(y,y),f(y,z)))))) = y # label(false). [para(82(a,1),2548(a,1,2,1,2,1)),rewrite(82(10),82(13))]. given #222 (T,wt=15): 2484 f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). [para(82(a,1),2470(a,1,1,2,2))]. given #223 (T,wt=17): 2472 f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(2448(a,1),62(a,1,2,2,1)),rewrite(77(5),1347(8),77(6),77(13),77(21),46(19),77(3),77(5)),flip(a)]. given #224 (T,wt=17): 2503 f(f(x,x),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(2470(a,1),426(a,1,1)),rewrite(2470(6),2470(7),77(4),2470(12),2470(13),77(10))]. given #225 (T,wt=17): 2673 f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(20(a,1),2484(a,1,1,2,2,2)),rewrite(77(10))]. given #226 (A,wt=49): 68 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(55(a,1),2(a,1,2,2,1,1,1,1))]. given #227 (F,wt=41): 2591 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(x,x),f(f(x,x),f(x,z)))))) = x # label(false). [para(91(a,1),2548(a,1,2,1,2,1)),rewrite(91(10),91(13))]. given #228 (F,wt=41): 2629 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(y,y),f(f(y,y),f(z,y)))))) = y # label(false). [para(82(a,1),2590(a,1,2,1,2,1)),rewrite(82(10),82(13))]. given #229 (F,wt=41): 2630 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(x,x),f(f(x,x),f(z,x)))))) = x # label(false). [para(91(a,1),2590(a,1,2,1,2,1)),rewrite(91(10),91(13))]. given #230 (F,wt=43): 2554 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(y,f(y,f(z,f(y,y))))))) = f(y,y) # label(false). [para(82(a,1),2499(a,1,2,2,2,2,2))]. given #231 (T,wt=17): 2693 f(f(x,x),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(2484(a,1),426(a,1,1)),rewrite(2484(6),2484(7),77(4),2484(12),2484(13),77(10))]. given #232 (T,wt=19): 2568 f(f(f(x,x),x),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(2499(a,1),45(a,1,2,2,1)),rewrite(82(6),20(6),82(15),20(15),82(23),20(23),20(33),2503(35),46(29),77(11),82(6),20(6)),flip(a)]. given #233 (T,wt=19): 2833 f(f(f(x,x),x),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(2554(a,1),45(a,1,2,2,1)),rewrite(82(6),20(6),82(15),20(15),82(23),20(23),20(33),2693(35),46(29),77(11),82(6),20(6)),flip(a)]. given #234 (T,wt=21): 2739 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))) = f(x,x). [para(2472(a,1),426(a,1,1)),rewrite(2472(7),2472(7),2472(15),2472(15))]. given #235 (A,wt=45): 71 f(f(f(x,y),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(f(f(x,y),f(f(f(x,y),f(x,y)),u)),z),z),f(x,y)),y))) = f(x,y). [para(55(a,1),7(a,1,1))]. given #236 (F,wt=45): 1968 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(f(x,x),x)),f(f(f(f(x,x),f(f(x,x),x)),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(false). [para(1755(a,1),38(a,1,2,2,1,1,1))]. given #237 (F,wt=45): 2791 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(55(a,1),68(a,1,2,2,2))]. given #238 (F,wt=25): 3047 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(325),rewrite(2962(3))]. given #239 (F,wt=25): 3127 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(157),rewrite(2963(3))]. given #240 (T,wt=9): 2962 f(f(x,x),f(x,y)) = x. [para(983(a,1),2791(a,1,2,2,1)),rewrite(77(4),414(4),77(5),77(8),77(13),46(11),77(3),77(4)),flip(a)]. given #241 (T,wt=9): 2963 f(f(x,x),f(y,x)) = x. [para(985(a,1),2791(a,1,2,2,1)),rewrite(2962(4),415(4),2962(5),2962(8),2962(13),46(11),2962(3),2962(4)),flip(a)]. given #242 (T,wt=11): 2989 f(f(x,x),x) = f(x,f(x,x)). [back_rewrite(2737),rewrite(2962(5),2963(4),2962(6)),flip(a)]. given #243 (T,wt=11): 3545 f(x,f(f(x,x),y)) = f(x,x). [para(20(a,1),2962(a,1,1))]. given #244 (A,wt=35): 81 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(77(a,1),2(a,1,2,2,2))]. given #245 (F,wt=23): 3603 f(f(x,y),f(f(f(f(x,y),f(y,f(y,y))),f(y,f(y,y))),y)) = y # label(false). [back_rewrite(1911),rewrite(3541(4))]. given #246 (F,wt=23): 3657 f(f(x,y),f(f(f(f(x,y),f(x,f(x,x))),f(x,f(x,x))),x)) = x # label(false). [back_rewrite(1918),rewrite(3547(4))]. given #247 (F,wt=25): 3712 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(2989(a,1),2(a,1,2,1))]. given #248 (F,wt=25): 3737 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(2989(a,1),96(a,1,2,1))]. given #249 (T,wt=11): 3680 f(x,f(y,f(x,x))) = f(x,x). [para(20(a,1),2963(a,1,1))]. given #250 (T,wt=13): 3541 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(2(a,1),2962(a,1,2))]. given #251 (T,wt=13): 3547 f(f(f(x,y),f(x,y)),x) = f(x,y). [para(77(a,1),2962(a,1,2))]. given #252 (T,wt=21): 3043 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = x. [back_rewrite(435),rewrite(2962(4),2962(4),2989(3),2962(7),2989(5),2962(12))]. given #253 (A,wt=43): 86 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),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(77(a,1),8(a,1,2,2,1,1))]. given #254 (F,wt=25): 3808 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(82(a,1),3712(a,1,2,2,1,1,1,1)),rewrite(3541(4))]. given #255 (F,wt=25): 3811 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(91(a,1),3712(a,1,2,2,1,1,1,1)),rewrite(3547(4))]. given #256 (F,wt=25): 3841 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(82(a,1),3737(a,1,2,2,1,1,1,1)),rewrite(3541(4))]. given #257 (F,wt=25): 3844 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(91(a,1),3737(a,1,2,2,1,1,1,1)),rewrite(3547(4))]. given #258 (T,wt=21): 3045 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = x. [back_rewrite(429),rewrite(2962(4),2962(4),2989(3),2962(7),2989(5),2962(8),2962(12))]. given #259 (T,wt=21): 3450 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(x,x)) = x. [back_rewrite(565),rewrite(2989(2),2989(4))]. given #260 (T,wt=21): 3480 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x)) = x. [back_rewrite(287),rewrite(2989(2),2989(4))]. given #261 (T,wt=21): 3573 f(x,f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),y))) = f(x,y). [para(2962(a,1),45(a,1,1)),rewrite(2962(6),3547(4),2962(5),2989(3))]. given #262 (A,wt=59): 87 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)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(y,v),v),f(y,z)),f(f(y,z),w)))))) = f(y,z). [para(77(a,1),8(a,1,2,2,2,2,1,1,1,1))]. given #263 (F,wt=27): 2968 f(x,f(f(f(f(x,y),f(x,y)),f(x,f(x,x))),f(f(x,f(x,y)),x))) = f(x,y) # label(false). [para(1902(a,1),2791(a,1,2,2,1,1,1)),rewrite(2962(4),2962(3),2962(3),2962(4),2962(6),1755(6),2963(7),2962(10),1755(10),2963(11),2962(10),2962(9),2962(11),2962(14))]. given #264 (F,wt=27): 2975 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(2956),rewrite(2962(3))]. given #265 (F,wt=27): 3090 f(x,f(f(f(f(y,x),f(y,x)),f(x,f(x,x))),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(1961),rewrite(2963(3),2989(5),2989(9),2962(10))]. given #266 (F,wt=27): 3132 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(44),rewrite(2963(3))]. given #267 (T,wt=21): 3600 f(x,f(f(y,x),f(f(f(x,f(x,x)),f(y,x)),x))) = f(y,x). [back_rewrite(3044),rewrite(3541(4))]. given #268 (T,wt=21): 4172 f(x,f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),x))) = f(x,y). [para(2989(a,1),2975(a,1,2,2,1,1)),rewrite(3547(4))]. given #269 (T,wt=21): 4180 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,y)),x))) = f(x,y). [para(3541(a,1),2975(a,1,2,1))]. given #270 (T,wt=21): 4214 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),x))) = f(y,x). [para(3547(a,1),3132(a,1,2,1))]. given #271 (A,wt=43): 88 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),f(f(y,u),f(y,u))),f(f(f(y,u),y),f(y,v)))))) = y. [para(77(a,1),8(a,1,2,2,2,2,1,1))]. given #272 (F,wt=27): 3564 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(2962(a,1),237(a,1,1,1,1,2)),rewrite(2962(4),2962(6),3541(4),2962(5),2962(6),2962(9),2962(10),2962(11),2962(15))]. given #273 (F,wt=27): 3565 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(2962(a,1),246(a,1,1,1,1,2)),rewrite(2962(4),2962(6),3541(4),2962(5),2962(6),2962(9),2962(10),2962(11),2962(15))]. given #274 (F,wt=27): 3566 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(2962(a,1),253(a,1,1,1,1,1)),rewrite(2962(4),2962(6),3547(4),2962(5),2962(6),2962(9),2962(10),2962(11),2962(15))]. given #275 (F,wt=27): 3567 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(2962(a,1),257(a,1,1,1,1,1)),rewrite(2962(4),2962(6),3547(4),2962(5),2962(6),2962(9),2962(10),2962(11),2962(15))]. given #276 (T,wt=23): 3374 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [back_rewrite(1428),rewrite(2989(4))]. given #277 (T,wt=23): 3393 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [back_rewrite(1403),rewrite(2989(4))]. given #278 (T,wt=23): 4019 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)). [para(3811(a,1),39(a,1,2,2)),rewrite(245(9),3576(20),46(12),82(7)),flip(a)]. given #279 (T,wt=23): 4411 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [para(3374(a,1),3547(a,1,1,1)),rewrite(3374(10),3374(20))]. given #280 (A,wt=59): 89 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)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(f(f(y,z),w),v),v),f(y,z)),y))))) = f(y,z). [para(77(a,1),8(a,1,2,2,2,2,2))]. given #281 (F,wt=29): 3049 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(146),rewrite(2962(3))]. given #282 (F,wt=29): 3050 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(124),rewrite(2962(3))]. given #283 (F,wt=29): 3130 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(137),rewrite(2963(3))]. given #284 (F,wt=29): 3131 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(115),rewrite(2963(3))]. given #285 (T,wt=23): 4414 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(3393(a,1),3547(a,1,1,1)),rewrite(3393(10),3393(20))]. given #286 (T,wt=25): 1565 f(f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(x,u))),f(x,x)) = x. [para(82(a,1),97(a,1,1,2,1,1,1,1))]. given #287 (T,wt=25): 1567 f(f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(69(a,1),97(a,1,1,2,1,1,1,1)),rewrite(77(3),77(12))]. given #288 (T,wt=25): 2246 f(f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(u,x))),f(x,x)) = x. [para(82(a,1),1460(a,1,1,2,1,1,1,1))]. given #289 (A,wt=45): 93 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(82(a,1),2(a,1,2,1))]. given #290 (F,wt=29): 3604 f(f(x,y),f(y,f(f(f(f(f(x,y),f(y,f(y,y))),f(y,f(y,y))),y),f(z,y)))) = y # label(false). [back_rewrite(1859),rewrite(3541(4))]. given #291 (F,wt=29): 3605 f(f(x,y),f(y,f(f(f(f(f(x,y),f(y,f(y,y))),f(y,f(y,y))),y),f(y,z)))) = y # label(false). [back_rewrite(1816),rewrite(3541(4))]. given #292 (F,wt=29): 3658 f(f(x,y),f(x,f(f(f(f(f(x,y),f(x,f(x,x))),f(x,f(x,x))),x),f(z,x)))) = x # label(false). [back_rewrite(1863),rewrite(3547(4))]. given #293 (F,wt=29): 3659 f(f(x,y),f(x,f(f(f(f(f(x,y),f(x,f(x,x))),f(x,f(x,x))),x),f(x,z)))) = x # label(false). [back_rewrite(1819),rewrite(3547(4))]. given #294 (T,wt=25): 2248 f(f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(z,f(x,x)))),x) = f(x,x). [para(69(a,1),1460(a,1,1,2,1,1,1,1)),rewrite(77(3),77(12))]. given #295 (T,wt=25): 3018 f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(x,f(x,x)))))) = f(x,f(x,x)). [back_rewrite(1872),rewrite(2962(3),2989(2),2970(3),2989(3),2989(5),2989(7),2989(9),245(12),2989(6),2962(7),2989(5),2989(11))]. given #296 (T,wt=25): 3020 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)). [back_rewrite(1826),rewrite(2962(3),2989(2),2970(3),2989(3),2989(5),2989(7),2989(9),245(12),2989(6),2962(7),2989(5),2989(11))]. given #297 (T,wt=25): 3024 f(f(x,y),f(y,f(f(f(f(y,x),f(f(y,x),f(y,x))),y),f(z,y)))) = y. [back_rewrite(1483),rewrite(2962(8),2962(4),2962(10),2989(6))]. given #298 (A,wt=45): 95 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(82(a,1),2(a,1,2,2,1,1,1))]. given #299 (F,wt=29): 3885 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(3541(a,1),7(a,1,2,1))]. given #300 (F,wt=29): 3966 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(3547(a,1),81(a,1,2,1))]. given #301 (F,wt=29): 4168 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(2962(a,1),2975(a,1,2,1))]. given #302 (F,wt=25): 4913 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(2(a,1),4168(a,1,2,1)),rewrite(2(13),2(15),2(17),2(22))]. given #303 (T,wt=19): 4747 f(f(x,y),f(f(f(y,x),f(f(y,x),f(y,x))),y)) = y. [para(82(a,1),3024(a,1,2))]. given #304 (T,wt=15): 4975 f(x,f(f(x,f(x,x)),f(y,x))) = f(y,x). [para(20(a,1),4747(a,1,2,1,1)),rewrite(2963(3),20(3),20(3))]. given #305 (T,wt=15): 4978 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y). [para(77(a,1),4747(a,1,2,1,1)),rewrite(2962(3),77(3),77(3))]. given #306 (T,wt=19): 4979 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),y)) = y. [para(82(a,1),4747(a,1,2,1,1)),rewrite(3541(4),82(6),82(7))]. given #307 (A,wt=37): 99 f(f(f(f(f(x,y),f(x,y)),z),f(f(f(f(f(f(x,y),u),z),z),f(x,y)),y)),f(f(x,y),f(x,y))) = f(x,y). [para(7(a,1),82(a,1,2,1)),rewrite(7(28),7(31))]. given #308 (F,wt=21): 5206 f(x,f(f(y,x),f(f(x,f(y,x)),f(x,f(x,x))))) = f(y,x) # label(false). [back_rewrite(4890),rewrite(5201(7),5201(8),5201(15))]. given #309 (F,wt=21): 5210 f(x,f(f(x,y),f(f(x,f(x,y)),f(x,f(x,x))))) = f(x,y) # label(false). [back_rewrite(4885),rewrite(5202(7),5202(8),5202(15))]. given #310 (F,wt=25): 4916 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(77(a,1),4168(a,1,2,1)),rewrite(77(5),77(7),77(9),77(14))]. given #311 (F,wt=25): 4947 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(82(a,1),4913(a,1,2,2,1,1,1,2)),rewrite(82(8))]. given #312 (T,wt=19): 4984 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = x. [para(91(a,1),4747(a,1,2,1,1)),rewrite(3547(4),91(6),91(7))]. given #313 (T,wt=19): 5136 f(f(x,x),f(f(x,f(x,x)),f(y,x))) = f(x,f(x,x)). [para(4975(a,1),3020(a,1,2,2))]. given #314 (T,wt=19): 5192 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)). [para(4978(a,1),3020(a,1,2,2))]. given #315 (T,wt=19): 5201 f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))) = f(y,x). [back_rewrite(5030),rewrite(5182(10),4975(5)),flip(a)]. given #316 (A,wt=41): 101 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(v,y),u),u),y),f(y,w)))))) = y. [para(82(a,1),8(a,1,2,2,2,2,1,1,1,1))]. given #317 (F,wt=17): 5629 f(x,f(f(y,x),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [para(3090(a,1),5201(a,1,2,2)),rewrite(5620(6),5620(11),5620(16),5620(23),5620(28),5620(33),5611(37),5620(7)),flip(a)]. given #318 (F,wt=17): 5746 f(f(x,y),f(x,f(f(f(x,y),x),f(x,y)))) = x # label(false). [para(2962(a,1),5629(a,1,2,1)),rewrite(2962(5),2962(10))]. given #319 (F,wt=17): 5747 f(f(x,y),f(y,f(f(f(x,y),y),f(x,y)))) = y # label(false). [para(2963(a,1),5629(a,1,2,1)),rewrite(2963(5),2963(10))]. given #320 (F,wt=17): 5749 f(x,f(f(x,y),f(f(x,f(x,y)),x))) = f(x,y) # label(false). [para(3547(a,1),5629(a,1,2,1)),rewrite(3547(5),3547(10))]. given #321 (T,wt=17): 5589 f(f(x,f(x,x)),f(f(y,x),f(y,x))) = f(y,x). [para(5201(a,1),91(a,1,2,1)),rewrite(5201(10),5201(13))]. given #322 (T,wt=17): 5596 f(f(x,f(x,x)),f(y,x)) = f(f(y,x),f(y,x)). [para(5201(a,1),45(a,1,1)),rewrite(5202(24),5201(23),3680(21)),flip(a)]. given #323 (T,wt=15): 5944 f(x,f(f(y,f(y,y)),f(x,y))) = f(x,y). [para(5596(a,2),91(a,1,2))]. given #324 (T,wt=15): 5960 f(f(f(x,f(x,x)),f(y,x)),x) = f(y,x). [para(5596(a,2),84(a,1,1)),rewrite(2962(14),2989(9),2989(14),5612(16))]. given #325 (A,wt=41): 102 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(w,y)))))) = y. [para(82(a,1),8(a,1,2,2,2,2,2))]. given #326 (F,wt=11): 6232 f(f(x,y),f(f(x,y),y)) = y # label(false). [back_rewrite(6101),rewrite(6193(6),5201(9))]. given #327 (F,wt=11): 6315 f(x,f(x,f(x,y))) = f(x,y) # label(false). [back_rewrite(6130),rewrite(6211(5),5201(14))]. given #328 (F,wt=11): 6425 f(x,f(x,f(y,x))) = f(y,x) # label(false). [back_rewrite(6138),rewrite(6221(5),5201(14))]. given #329 (F,wt=11): 6732 f(f(x,y),f(f(x,y),x)) = x # label(false). [para(3547(a,1),6232(a,1,1)),rewrite(3547(5))]. given #330 (T,wt=11): 7286 f(f(x,f(x,x)),y) = f(y,y). [back_rewrite(6146),rewrite(6956(26),6956(17),6956(5))]. given #331 (T,wt=11): 7308 f(f(x,f(x,x)),f(y,y)) = y. [back_rewrite(5905),rewrite(6956(26),6956(17),6956(5))]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(9584)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c_0, f ]). NOTE: sn=98, num_tables=183 NOTE: updating interpretation 1: c_0=1. restricted denial: (wt=15): 10847 f(c1,f(f(c2,c3),c_0)) != f(c2,f(f(c1,c3),c_0)) # answer(A_SS). [back_rewrite(3),rewrite(10248(8,R),10248(15,R))]. given #332 (T,wt=7): 9654 f(x,f(x,x)) = c_0. [new_symbol(9584)]. given #333 (T,wt=7): 9694 f(f(x,x),c_0) = x. [back_rewrite(9548),rewrite(9654(3))]. given #334 (A,wt=21): 5673 f(x,f(f(y,x),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x) # label(false). [back_rewrite(3086),rewrite(5620(6))]. given #335 (F,wt=11): 7257 f(f(x,f(y,x)),x) = f(y,x) # label(false). [back_rewrite(6226),rewrite(6956(5),4975(7))]. given #336 (F,wt=11): 7900 f(f(x,f(x,y)),x) = f(x,y) # label(false). [para(7286(a,1),2975(a,1,2,2,1,1)),rewrite(7267(5),2962(5),7732(7))]. given #337 (F,wt=11): 8888 f(f(x,y),f(y,f(x,y))) = y # label(false). [back_rewrite(6232),rewrite(8165(3))]. given #338 (F,wt=11): 10867 f(f(x,y),f(x,f(x,y))) = x # label(false). [para(7900(a,1),6732(a,1,2)),rewrite(8165(4))]. given #339 (T,wt=7): 9695 f(x,f(c_0,c_0)) = c_0. [back_rewrite(9547),rewrite(9654(2),9654(3),9654(6))]. given #340 (T,wt=7): 10229 f(f(c_0,c_0),x) = c_0. [back_rewrite(7993),rewrite(9654(2),9654(3),9654(6))]. given #341 (T,wt=7): 10248 f(x,c_0) = f(x,x). [back_rewrite(7882),rewrite(9654(2))]. given #342 (T,wt=7): 10250 f(c_0,x) = f(x,x). [back_rewrite(7880),rewrite(9654(2),9654(4),10248(4))]. given #343 (A,wt=17): 5674 f(x,f(f(y,x),f(f(x,f(y,x)),y))) = f(y,x). [back_rewrite(3057),rewrite(5620(6))]. given #344 (F,wt=11): 11074 f(f(x,y),f(y,f(y,x))) = y # label(false). [back_rewrite(8899),rewrite(10866(3))]. given #345 (F,wt=15): 9671 f(f(x,y),f(f(c_0,f(f(y,x),c_0)),y)) = y # label(false). [back_rewrite(9586),rewrite(9654(4),9654(6),8165(6))]. given #346 (F,wt=15): 9672 f(f(x,y),f(f(c_0,f(f(x,y),c_0)),y)) = y # label(false). [back_rewrite(9583),rewrite(9654(4),9654(6),8165(6))]. given #347 (F,wt=15): 9673 f(f(x,y),f(f(c_0,f(f(x,y),c_0)),x)) = x # label(false). [back_rewrite(9581),rewrite(9654(4),9654(6),8165(6))]. given #348 (T,wt=7): 10270 f(c_0,f(x,x)) = x. [back_rewrite(7308),rewrite(9654(2))]. given #349 (T,wt=11): 8165 f(f(x,y),y) = f(y,f(x,y)). [back_rewrite(6696),rewrite(7994(15),6956(8),8028(9),7308(6)),flip(a)]. given #350 (T,wt=11): 9680 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_rewrite(9569),rewrite(9654(3),9654(7))]. given #351 (T,wt=11): 9681 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(9568),rewrite(9654(3),9654(7))]. given #352 (A,wt=21): 5675 f(x,f(f(y,x),f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [back_rewrite(3055),rewrite(5620(6))]. restricted denial: (wt=15): 11306 f(c1,f(c_0,f(c2,c3))) != f(c2,f(c_0,f(c1,c3))) # answer(A_SS). [back_rewrite(10847),rewrite(11197(6),11197(13))]. given #353 (F,wt=15): 11734 f(f(x,y),f(f(c_0,f(c_0,f(x,y))),x)) = x # label(false). [back_rewrite(9673),rewrite(11197(5))]. given #354 (F,wt=15): 11735 f(f(x,y),f(f(c_0,f(c_0,f(x,y))),y)) = y # label(false). [back_rewrite(9672),rewrite(11197(5))]. given #355 (F,wt=15): 11736 f(f(x,y),f(f(c_0,f(c_0,f(y,x))),y)) = y # label(false). [back_rewrite(9671),rewrite(11197(5))]. given #356 (F,wt=17): 8528 f(f(x,y),f(y,f(f(y,f(x,y)),f(z,y)))) = y # label(false). [back_rewrite(7629),rewrite(8165(3),7257(4),8165(3))]. given #357 (T,wt=11): 10249 f(f(c_0,f(x,y)),x) = f(x,y). [back_rewrite(7881),rewrite(9654(2))]. given #358 (T,wt=11): 10254 f(f(c_0,f(x,y)),y) = f(x,y). [back_rewrite(7780),rewrite(9654(2))]. given #359 (T,wt=11): 10260 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(7747),rewrite(9654(2))]. given #360 (T,wt=11): 10263 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(7732),rewrite(9654(2))]. given #361 (A,wt=27): 8343 f(x,f(f(y,x),f(f(f(y,x),f(f(f(y,f(x,y)),f(y,x)),x)),x))) = f(y,x). [back_rewrite(8097),rewrite(8165(4))]. given #362 (F,wt=17): 9591 f(f(x,y),f(y,f(f(y,f(x,y)),f(y,z)))) = y # label(false). [back_rewrite(8893),rewrite(9563(8))]. given #363 (F,wt=17): 9683 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(y,z)))) = y # label(false). [back_rewrite(9566),rewrite(9654(3))]. given #364 (F,wt=17): 9697 f(x,f(f(y,x),f(c_0,f(f(x,x),z)))) = f(x,x) # label(false). [back_rewrite(9540),rewrite(9654(3))]. given #365 (F,wt=17): 9698 f(x,f(f(y,x),f(c_0,f(z,f(x,x))))) = f(x,x) # label(false). [back_rewrite(9538),rewrite(9654(3))]. given #366 (T,wt=11): 10331 f(x,f(c_0,f(f(x,x),y))) = c_0. [back_rewrite(5529),rewrite(9654(2),9654(7))]. given #367 (T,wt=11): 10334 f(x,f(c_0,f(y,f(x,x)))) = c_0. [back_rewrite(5471),rewrite(9654(2),9654(7))]. given #368 (T,wt=11): 10864 f(f(x,y),f(c_0,f(x,y))) = c_0. [back_rewrite(10318),rewrite(10839(6))]. given #369 (T,wt=11): 10866 f(f(x,y),x) = f(x,f(x,y)). [para(6315(a,1),7900(a,1,1))]. given #370 (A,wt=39): 8359 f(f(x,f(y,z)),f(f(y,z),f(f(f(y,z),f(f(f(z,f(f(f(y,z),x),z)),f(y,z)),z)),f(x,f(y,z))))) = f(y,z) # label(false). [back_rewrite(8081),rewrite(8165(8))]. given #371 (F,wt=17): 9699 f(f(f(x,y),f(c_0,f(f(y,y),z))),y) = f(y,y) # label(false). [back_rewrite(9535),rewrite(9654(3))]. given #372 (F,wt=17): 9700 f(f(f(x,y),f(c_0,f(z,f(y,y)))),y) = f(y,y) # label(false). [back_rewrite(9533),rewrite(9654(3))]. given #373 (F,wt=17): 10868 f(f(x,y),f(c_0,f(f(x,f(x,y)),f(z,x)))) = x # label(false). [back_rewrite(10863),rewrite(10866(4))]. given #374 (F,wt=17): 10909 f(f(x,y),f(c_0,f(f(y,f(y,x)),f(z,y)))) = y # label(false). [back_rewrite(10759),rewrite(10866(4))]. given #375 (T,wt=11): 11169 f(f(c_0,f(x,f(y,y))),y) = c_0. [para(3680(a,1),9680(a,1,2,2)),rewrite(10248(5,R),10265(4),10270(7))]. given #376 (T,wt=11): 11197 f(f(x,y),c_0) = f(c_0,f(x,y)). [para(9680(a,1),5675(a,1,2,2,2)),rewrite(10864(9),9695(8))]. given #377 (T,wt=11): 11201 f(f(c_0,f(f(x,x),y)),x) = c_0. [back_rewrite(11168),rewrite(11197(4))]. given #378 (T,wt=11): 11655 f(f(c_0,f(x,y)),f(y,y)) = c_0. [back_rewrite(10274),rewrite(11197(3))]. given #379 (A,wt=35): 8361 f(x,f(f(x,y),f(f(f(x,y),f(f(f(f(f(x,y),z),f(x,f(f(x,y),z))),f(x,y)),x)),x))) = f(x,y) # label(false). [back_rewrite(8079),rewrite(8165(8))]. given #380 (F,wt=11): 11961 f(f(x,f(x,y)),f(y,x)) = x # label(false). [para(10909(a,1),10263(a,1)),flip(a)]. given #381 (F,wt=17): 11032 f(f(x,y),f(c_0,f(f(y,f(y,x)),f(y,z)))) = y # label(false). [back_rewrite(9684),rewrite(10866(4))]. given #382 (F,wt=17): 11033 f(f(x,y),f(c_0,f(f(x,f(x,y)),f(x,z)))) = x # label(false). [back_rewrite(9682),rewrite(10866(4))]. given #383 (F,wt=17): 11042 f(f(x,y),f(x,f(f(x,f(x,y)),f(x,z)))) = x # label(false). [back_rewrite(9653),rewrite(10866(3))]. given #384 (T,wt=11): 11656 f(f(c_0,f(x,y)),f(x,x)) = c_0. [back_rewrite(10264),rewrite(11197(3))]. given #385 (T,wt=11): 11742 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(10249(a,1),6315(a,1,2,2)),rewrite(8165(8),10864(8),10866(5),10249(9))]. given #386 (T,wt=13): 9223 f(x,f(f(x,y),f(y,x))) = f(x,y). [back_rewrite(4180),rewrite(8165(3),8165(5),8888(5))]. given #387 (T,wt=15): 10271 f(x,f(c_0,f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(7263),rewrite(9654(2))]. given #388 (A,wt=31): 8362 f(f(x,y),f(y,f(f(y,f(f(f(f(y,z),f(f(x,y),f(y,z))),y),f(x,y))),f(x,y)))) = y # label(false). [back_rewrite(8078),rewrite(8165(6))]. given #389 (F,wt=17): 11101 f(f(x,y),f(x,f(f(x,f(x,y)),f(z,x)))) = x # label(false). [back_rewrite(8267),rewrite(10866(3))]. given #390 (F,wt=17): 11111 f(f(x,y),f(y,f(f(y,f(y,x)),f(z,y)))) = y # label(false). [back_rewrite(7663),rewrite(10866(3))]. given #391 (F,wt=17): 11114 f(f(x,y),f(y,f(f(y,f(y,x)),f(y,z)))) = y # label(false). [back_rewrite(7636),rewrite(10866(3))]. given #392 (F,wt=17): 11127 f(f(f(x,y),f(c_0,f(z,f(x,x)))),x) = f(x,x) # label(false). [back_rewrite(6843),rewrite(10867(5),9654(3))]. given #393 (T,wt=15): 10275 f(x,f(c_0,f(f(x,f(y,x)),y))) = f(y,x). [back_rewrite(7258),rewrite(9654(2))]. given #394 (T,wt=15): 10353 f(f(x,x),f(c_0,f(y,f(f(x,x),y)))) = c_0. [back_rewrite(10174),rewrite(10248(2),10250(3),10265(6))]. given #395 (T,wt=11): 12305 f(x,f(c_0,f(y,f(x,y)))) = c_0. [para(20(a,1),10353(a,1,1)),rewrite(10248(4,R),11197(4),10270(4))]. given #396 (T,wt=11): 12313 f(f(c_0,f(x,f(y,x))),y) = c_0. [back_rewrite(10627),rewrite(12305(6),10229(4),10263(8),12305(10))]. given #397 (A,wt=31): 8363 f(f(x,y),f(y,f(f(y,f(f(f(f(y,z),f(f(y,x),f(y,z))),y),f(y,x))),f(y,u)))) = y. [back_rewrite(8075),rewrite(8165(6))]. given #398 (F,wt=17): 11129 f(f(f(x,y),f(c_0,f(f(x,x),z))),x) = f(x,x) # label(false). [back_rewrite(6837),rewrite(10867(5),9654(3))]. given #399 (F,wt=17): 11131 f(x,f(f(x,y),f(c_0,f(z,f(x,x))))) = f(x,x) # label(false). [back_rewrite(6812),rewrite(10867(5),9654(3))]. given #400 (F,wt=17): 11133 f(x,f(f(x,y),f(c_0,f(f(x,x),z)))) = f(x,x) # label(false). [back_rewrite(6803),rewrite(10867(5),9654(3))]. given #401 (F,wt=17): 11138 f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z)))) = x # label(false). [para(8888(a,1),5673(a,1,2,1)),rewrite(8888(8),10866(5),6425(5),8888(7),8888(11))]. given #402 (T,wt=11): 12315 f(f(x,y),f(c_0,f(y,x))) = c_0. [para(11074(a,1),12305(a,1,2,2,2)),rewrite(10866(5),6315(5))]. given #403 (T,wt=11): 12338 f(f(c_0,f(x,y)),f(y,x)) = c_0. [para(11074(a,1),12313(a,1,1,2,2)),rewrite(10866(4),6315(4))]. given #404 (T,wt=15): 11773 f(f(c_0,f(x,y)),f(f(x,y),z)) = f(x,y). [para(10260(a,1),5673(a,1,2,1)),rewrite(10260(11),8165(9),10864(9),10260(9),10260(9),10260(10))]. given #405 (T,wt=15): 11774 f(f(c_0,f(x,y)),f(z,f(x,y))) = f(x,y). [para(10260(a,1),5675(a,1,2,1)),rewrite(10260(11),8165(9),10864(9),10260(9),10263(9),10260(10))]. given #406 (A,wt=47): 8364 f(f(x,f(y,z)),f(f(y,z),f(f(f(y,z),f(f(f(f(f(y,z),u),f(f(f(y,z),x),f(f(y,z),u))),f(y,z)),f(f(y,z),x))),z))) = f(y,z). [back_rewrite(8074),rewrite(8165(12))]. given #407 (F,wt=17): 11140 f(f(x,f(x,y)),f(x,f(f(x,y),f(x,z)))) = x # label(false). [para(10867(a,1),5673(a,1,2,1)),rewrite(10867(8),10866(5),6315(5),10867(7),10867(11))]. given #408 (F,wt=17): 11185 f(f(x,f(y,x)),f(x,f(f(y,x),f(z,x)))) = x # label(false). [para(8888(a,1),5675(a,1,2,1)),rewrite(8888(8),10866(5),6425(5),8888(7),8888(11))]. given #409 (F,wt=17): 11187 f(f(x,f(x,y)),f(x,f(f(x,y),f(z,x)))) = x # label(false). [para(10867(a,1),5675(a,1,2,1)),rewrite(10867(8),10866(5),6315(5),10867(7),10867(11))]. given #410 (F,wt=17): 11746 f(f(f(f(x,y),f(y,x)),x),f(x,f(x,y))) = x # label(false). [back_rewrite(11720),rewrite(11742(9),10866(6))]. given #411 (T,wt=15): 11805 f(f(f(x,f(y,x)),f(x,z)),f(x,x)) = c_0. [para(9683(a,1),9680(a,1,2,2)),rewrite(10248(13,R),10866(8),11742(8),10250(6))]. given #412 (T,wt=13): 12749 f(f(f(x,y),f(y,z)),f(y,y)) = c_0. [para(8165(a,1),11805(a,1,1,1,2)),rewrite(6425(3))]. given #413 (T,wt=13): 12754 f(f(f(x,y),f(x,z)),f(x,x)) = c_0. [para(10866(a,1),11805(a,1,1,1,2)),rewrite(6315(3))]. given #414 (T,wt=13): 12771 f(f(f(x,y),f(z,y)),f(y,y)) = c_0. [para(6425(a,1),12749(a,1,1,2))]. given #415 (A,wt=47): 8365 f(f(x,y),f(y,f(f(y,f(f(f(f(y,z),f(f(y,x),f(y,z))),y),f(y,x))),f(f(f(y,y),u),f(f(f(u,f(f(y,v),u)),y),f(y,w)))))) = y. [back_rewrite(8073),rewrite(8165(6),8165(15))]. given #416 (F,wt=17): 11793 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(z,y)))) = y # label(false). [para(6425(a,1),9683(a,1,2,2,2))]. given #417 (F,wt=17): 11804 f(f(x,f(y,x)),f(c_0,f(f(y,x),f(x,z)))) = x # label(false). [para(8165(a,1),9683(a,1,1)),rewrite(8165(5),6425(6))]. given #418 (F,wt=17): 11842 f(f(x,x),f(f(y,f(x,x)),f(c_0,f(x,z)))) = x # label(false). [para(20(a,1),9697(a,1,2,2,2,1)),rewrite(10248(11,R),11197(11),10270(11))]. given #419 (F,wt=17): 11860 f(f(x,x),f(f(y,f(x,x)),f(c_0,f(z,x)))) = x # label(false). [para(20(a,1),9698(a,1,2,2,2,2)),rewrite(10248(11,R),11197(11),10270(11))]. given #420 (T,wt=13): 12784 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [para(12749(a,1),9223(a,1,2,1)),rewrite(10263(11),12749(10))]. given #421 (T,wt=13): 12796 f(f(f(x,y),f(z,x)),f(x,x)) = c_0. [para(6425(a,1),12754(a,1,1,2))]. given #422 (T,wt=13): 12804 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(12754(a,1),9223(a,1,2,1)),rewrite(10263(11),12754(10))]. given #423 (T,wt=13): 12822 f(f(x,x),f(f(y,x),f(z,x))) = c_0. [para(12771(a,1),9223(a,1,2,1)),rewrite(10263(11),12771(10))]. given #424 (A,wt=31): 8367 f(f(x,y),f(y,f(f(y,f(f(f(f(y,z),f(f(y,x),f(y,z))),y),f(y,x))),f(u,y)))) = y. [back_rewrite(8071),rewrite(8165(6))]. given #425 (F,wt=17): 11883 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(x,z)))) = x # label(false). [para(10866(a,1),9683(a,1,1)),rewrite(10866(5),6315(6))]. given #426 (F,wt=17): 11902 f(f(f(x,f(y,y)),f(c_0,f(y,z))),f(y,y)) = y # label(false). [para(20(a,1),9699(a,1,1,2,2,1)),rewrite(10248(11,R),11197(11),10270(11))]. given #427 (F,wt=17): 11908 f(f(f(x,f(y,y)),f(c_0,f(z,y))),f(y,y)) = y # label(false). [para(20(a,1),9700(a,1,1,2,2,2)),rewrite(10248(11,R),11197(11),10270(11))]. given #428 (F,wt=17): 11914 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(z,x)))) = x # label(false). [para(6315(a,1),10868(a,1,2,2,1))]. given #429 (T,wt=13): 13152 f(f(x,x),f(f(x,y),f(z,x))) = c_0. [para(12796(a,1),9223(a,1,2,1)),rewrite(10263(11),12796(10))]. given #430 (T,wt=13): 13446 f(f(x,y),f(y,x)) = f(c_0,f(x,y)). [back_rewrite(12109),rewrite(13347(7),10864(9)),flip(a)]. % Operation f is commutative; C redundancy checks enabled. given #431 (T,wt=7): 13468 f(x,y) = f(y,x). [para(13446(a,1),2963(a,1,2)),rewrite(10248(3,R),11197(3),13467(7))]. given #432 (T,wt=11): 13626 f(x,f(c_0,f(y,f(y,x)))) = c_0. [back_rewrite(12313),rewrite(13468(2),13468(5))]. given #433 (A,wt=21): 9701 f(f(x,y),f(c_0,f(y,f(z,f(y,f(x,y)))))) = f(y,f(x,y)). [back_rewrite(9532),rewrite(9654(3))]. given #434 (F,wt=11): 13942 f(x,f(x,f(y,x))) = f(y,x) # label(false). [para(9701(a,1),10867(a,1,2,2)),rewrite(9701(8),8888(6),13468(3))]. given #435 (F,wt=17): 13561 f(f(x,y),f(c_0,f(f(x,z),f(x,f(x,y))))) = x # label(false). [back_rewrite(12904),rewrite(13468(2),13468(4),13468(5),13468(8),13468(10),13468(11),13468(13),13468(14),13468(15),13473(15),13468(8),13259(8),13468(2),13468(4),13468(5),13468(7),13468(8)),flip(a)]. given #436 (F,wt=17): 13651 f(f(x,y),f(x,f(f(x,z),f(x,f(x,y))))) = x # label(false). [back_rewrite(12225),rewrite(13468(4),13468(6),13644(6),13468(5))]. given #437 (F,wt=17): 13653 f(f(x,y),f(y,f(f(y,z),f(y,f(x,y))))) = y # label(false). [back_rewrite(12209),rewrite(13468(3),13468(6),10867(6),10248(4,R),13468(4),13468(5),10263(5),10248(3,R),13468(3),13468(4),10263(4),13468(5))]. given #438 (T,wt=11): 13857 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(10254),rewrite(13468(4))]. given #439 (T,wt=11): 13961 f(f(x,x),f(c_0,f(y,x))) = c_0. [para(13653(a,1),9681(a,1,2,2)),rewrite(10248(3,R),13468(3),13468(5),10248(5),13468(5))]. given #440 (T,wt=13): 13586 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [back_rewrite(12771),rewrite(13468(2),13468(5))]. given #441 (T,wt=13): 13938 f(x,f(c_0,f(f(x,x),f(y,y)))) = c_0. [para(20(a,1),9701(a,1,1)),rewrite(13468(4),13468(6),2962(6),13468(4),9654(4),10248(4),13468(8),13468(10),2962(10),13468(8),9654(8))]. given #442 (A,wt=19): 10272 f(x,f(c_0,f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y) # label(false). [back_rewrite(7262),rewrite(9654(2))]. given #443 (F,wt=17): 13655 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,y))))) = y # label(false). [back_rewrite(12150),rewrite(13468(6),13468(9),10263(11))]. given #444 (F,wt=19): 11935 f(f(x,f(x,y)),f(c_0,f(x,f(z,f(x,y))))) = f(x,y) # label(false). [para(10866(a,1),10868(a,1,1)),rewrite(10866(6),10867(7))]. given #445 (F,wt=17): 13985 f(f(x,f(y,x)),f(c_0,f(f(y,x),f(x,z)))) = x # label(false). [para(20(a,1),11935(a,1,1,2)),rewrite(13468(2),20(7),13468(5),20(11))]. given #446 (F,wt=19): 13589 f(f(x,f(y,x)),f(x,f(c_0,f(y,f(x,f(y,x)))))) = x # label(false). [back_rewrite(12730),rewrite(13468(5),13468(7),13478(8),13468(9),10260(9),13468(9))]. given #447 (T,wt=13): 13962 f(f(c_0,c_0),f(f(x,y),f(x,z))) = c_0. [para(12804(a,1),13857(a,1,2,2)),rewrite(13468(7),12804(12))]. given #448 (T,wt=13): 13967 f(f(c_0,c_0),f(f(x,x),f(y,z))) = c_0. [para(11742(a,1),13586(a,1,2,2)),rewrite(10248(5))]. given #449 (T,wt=13): 13969 f(f(c_0,c_0),f(f(x,y),f(y,z))) = c_0. [para(13586(a,1),13857(a,1,2,2)),rewrite(13468(7),13586(12))]. given #450 (T,wt=13): 13997 f(x,f(c_0,f(f(x,x),f(y,z)))) = c_0. [para(11742(a,1),13985(a,1,2,2,2)),rewrite(10248(3),10270(3),10248(3))]. given #451 (A,wt=21): 11298 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(10881),rewrite(11197(5),10864(6),11197(5),11197(12))]. given #452 (F,wt=17): 14019 f(x,f(f(y,x),f(c_0,f(z,f(x,x))))) = f(x,x) # label(false). [para(20(a,1),11298(a,1,2,2,2,2,2)),rewrite(20(3),13468(4),10248(4),20(11),13468(9),10248(9))]. given #453 (F,wt=19): 13949 f(x,f(c_0,f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [para(9701(a,1),11883(a,1,1,2)),rewrite(8888(4),9701(9),13468(5))]. given #454 (F,wt=19): 13956 f(f(x,f(y,x)),f(c_0,f(x,f(z,f(y,x))))) = f(y,x) # label(false). [para(9701(a,1),13561(a,1,2,2,2,2)),rewrite(9701(8),13468(5),8888(9),13468(6))]. given #455 (F,wt=21): 11600 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(10406),rewrite(11197(5),11197(12))]. given #456 (T,wt=13): 14006 f(f(c_0,c_0),f(f(x,y),f(z,z))) = c_0. [para(11742(a,1),13962(a,1,2,1)),rewrite(13468(6),10248(6))]. given #457 (T,wt=15): 11897 f(f(x,f(y,z)),f(c_0,f(y,z))) = f(y,z). [para(8359(a,1),10260(a,1,2,2)),rewrite(8359(23))]. given #458 (T,wt=13): 14107 f(f(c_0,c_0),f(f(x,y),f(z,u))) = c_0. [para(11897(a,1),13967(a,1,2,1))]. given #459 (T,wt=15): 12081 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,y)))) = c_0. [para(8359(a,1),11656(a,1,1,2)),rewrite(10248(8,R),11197(7))]. given #460 (A,wt=23): 11645 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(10305),rewrite(11197(3))]. given #461 (F,wt=21): 13510 f(f(c_0,f(x,y)),f(f(x,x),f(z,f(c_0,f(x,y))))) = f(x,y) # label(false). [back_rewrite(13318),rewrite(13468(6),13468(10))]. given #462 (F,wt=17): 14129 f(f(x,x),f(f(y,f(x,x)),f(c_0,f(z,x)))) = x # label(false). [para(20(a,1),13510(a,1,2,2,2,2)),rewrite(20(4),13468(2),10248(2),10248(4,R),13468(4),13468(6),10248(6),13468(7),20(11))]. given #463 (F,wt=21): 13512 f(f(c_0,f(x,y)),f(f(y,y),f(z,f(c_0,f(x,y))))) = f(x,y) # label(false). [back_rewrite(13315),rewrite(13468(6),13468(10))]. given #464 (F,wt=23): 13027 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(12958),rewrite(12963(11))]. given #465 (T,wt=15): 12561 f(f(x,y),f(c_0,f(z,f(c_0,f(x,y))))) = c_0. [para(11774(a,1),9680(a,1,1))]. given #466 (T,wt=13): 14193 f(f(c_0,c_0),f(x,f(c_0,f(y,z)))) = c_0. [para(12561(a,1),13961(a,1,2,2)),rewrite(10248(13,R),13468(8),11742(8),13468(8))]. given #467 (T,wt=15): 12809 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0. [para(2962(a,1),12771(a,1,1,1)),rewrite(10248(6,R),11197(6))]. given #468 (T,wt=15): 13173 f(x,f(f(y,f(x,x)),f(z,f(x,x)))) = c_0. [para(20(a,1),12822(a,1,1))]. given #469 (A,wt=23): 11653 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(10287),rewrite(11197(3))]. given #470 (F,wt=23): 13312 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(13252),rewrite(13255(6))]. given #471 (F,wt=23): 13314 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(13250),rewrite(13255(11))]. given #472 (F,wt=23): 13515 f(f(c_0,f(x,f(y,f(x,z)))),f(f(x,z),f(y,f(x,z)))) = f(x,z) # label(false). [back_rewrite(13248),rewrite(13468(3),13468(7),13468(8),13468(10))]. given #473 (F,wt=17): 14220 f(f(x,f(x,y)),f(c_0,f(f(z,x),f(x,y)))) = x # label(false). [para(20(a,1),13515(a,1,1,2,2,2)),rewrite(13468(3),20(8),20(8),13468(6),13468(8),20(11))]. given #474 (T,wt=15): 13259 f(f(x,x),f(c_0,f(f(x,y),f(x,z)))) = x. [para(11883(a,1),10254(a,1,1,2)),rewrite(10250(2),11883(15))]. given #475 (T,wt=15): 13583 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0. [back_rewrite(12792),rewrite(13468(2),13468(3))]. given #476 (T,wt=15): 13996 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x). [para(2962(a,1),13985(a,1,2,2,2)),rewrite(13468(8),3680(8),10270(7),13468(5))]. given #477 (T,wt=15): 14000 f(f(x,x),f(c_0,f(f(y,x),f(x,z)))) = x. [para(13985(a,1),13857(a,1,2,2)),rewrite(13468(7),10248(7),13468(7),13985(15))]. given #478 (A,wt=17): 11775 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [para(10260(a,1),8528(a,1,1)),rewrite(10260(11),8165(9),10864(9),10263(11))]. given #479 (F,wt=17): 14222 f(f(x,f(x,y)),f(c_0,f(f(x,z),f(x,y)))) = x # label(false). [para(10867(a,1),13515(a,1,1,2,2,2)),rewrite(13468(3),10867(9),10867(9),13468(6),13468(8),10867(12))]. given #480 (F,wt=19): 14243 f(f(x,y),f(x,f(x,f(c_0,f(z,f(c_0,f(x,y))))))) = x # label(false). [para(11600(a,1),14220(a,1,2,2)),rewrite(13468(3),13468(11),11742(13),13468(10))]. given #481 (F,wt=15): 14276 f(f(x,y),f(x,f(z,f(x,f(x,y))))) = x # label(false). [para(9701(a,1),14243(a,1,2,2,2,2)),rewrite(13468(1),13468(6),10260(9),6315(7),13468(6))]. given #482 (F,wt=15): 14279 f(f(x,f(x,y)),f(x,f(z,f(x,y)))) = x # label(false). [para(11935(a,1),14243(a,1,2,2,2,2)),rewrite(10260(7),13468(6))]. given #483 (T,wt=13): 14281 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(13997(a,1),14243(a,1,2,2,2,2)),rewrite(9695(9),13468(6),10270(6),13468(4))]. given #484 (T,wt=15): 14081 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [back_rewrite(13907),rewrite(14062(5))]. given #485 (T,wt=15): 14214 f(f(c_0,c_0),f(x,f(f(y,z),f(y,u)))) = c_0. [para(13312(a,1),14193(a,1,2,2,2)),rewrite(11742(10))]. given #486 (T,wt=15): 14329 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(y,x). [para(14081(a,1),13468(a,2)),rewrite(13468(2),13468(6),13468(7))]. given #487 (A,wt=47): 11875 f(f(f(x,y),f(c_0,f(z,f(y,y)))),f(f(y,y),f(c_0,f(u,f(c_0,f(f(x,y),f(c_0,f(z,f(y,y))))))))) = f(c_0,f(f(x,y),f(c_0,f(z,f(y,y))))). [para(9698(a,1),9698(a,1,2,1)),rewrite(10248(21,R),11197(16),10248(33,R),11197(28))]. given #488 (F,wt=13): 14341 f(f(x,x),f(y,f(c_0,f(x,z)))) = x # label(false). [para(13510(a,1),14081(a,1,2,2,2)),rewrite(13468(8),11775(8),11742(6),2962(3)),flip(a)]. given #489 (F,wt=15): 14292 f(f(x,y),f(y,f(z,f(y,f(x,y))))) = y # label(false). [para(13468(a,1),14276(a,1,1)),rewrite(13468(2))]. given #490 (F,wt=15): 14352 f(f(x,y),f(x,f(z,f(c_0,f(x,y))))) = x # label(false). [back_rewrite(14143),rewrite(14341(11),13468(6),14341(13))]. given #491 (F,wt=15): 14381 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y) # label(false). [para(14129(a,1),14329(a,1,2,2,2)),rewrite(13468(7),3680(7),10270(6),13468(4),13857(4)),flip(a)]. given #492 (T,wt=15): 14355 f(f(c_0,c_0),f(x,f(f(y,z),f(u,u)))) = c_0. [para(11742(a,1),14214(a,1,2,2,1)),rewrite(13468(6),10248(6))]. given #493 (T,wt=15): 14414 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(14341(a,1),13961(a,1,2,2)),rewrite(10248(9,R),13468(6),13468(8),10248(8),13468(8))]. given #494 (T,wt=15): 14430 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0. [para(14341(a,1),12809(a,1,1,2))]. given #495 (T,wt=15): 14431 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x. [para(13312(a,1),14341(a,1,2,2,2)),rewrite(11742(8))]. given #496 (A,wt=21): 12642 f(f(x,f(x,y)),f(c_0,f(x,f(x,f(f(x,y),f(x,z)))))) = c_0. [para(11140(a,1),12305(a,1,2,2,2)),rewrite(10866(8))]. given #497 (F,wt=15): 14389 f(f(x,y),f(y,f(z,f(c_0,f(x,y))))) = y # label(false). [para(14329(a,1),14243(a,1,1)),rewrite(14329(9),14379(8))]. given #498 (F,wt=15): 14394 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y) # label(false). [back_rewrite(14270),rewrite(14368(7))]. given #499 (F,wt=15): 14410 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,x) # label(false). [para(20(a,1),14341(a,1,1)),rewrite(13468(3))]. given #500 (F,wt=15): 14412 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z) # label(false). [para(10867(a,1),14341(a,1,2,2,2)),rewrite(10248(3,R),13468(3),13468(5),10248(5),13468(6))]. given #501 (T,wt=15): 14511 f(f(c_0,f(x,f(y,y))),f(c_0,f(y,z))) = c_0. [para(14381(a,1),9681(a,1,2,2)),rewrite(10248(5,R),13468(4),13468(6))]. given #502 (T,wt=15): 14524 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x. [para(13985(a,1),14381(a,1,2,2)),rewrite(10248(11,R),13468(7),11742(7),13468(6),10248(6),13468(6),13985(14))]. given #503 (T,wt=15): 14527 f(f(c_0,c_0),f(x,f(y,f(c_0,f(z,u))))) = c_0. [para(12561(a,1),14381(a,1,2,2)),rewrite(10248(13,R),13468(8),11742(8),13468(9),12561(17))]. given #504 (T,wt=15): 14548 f(f(c_0,c_0),f(x,f(f(y,z),f(u,v)))) = c_0. [para(11897(a,1),14355(a,1,2,2,2))]. given #505 (A,wt=19): 12953 f(c_0,f(f(x,y),f(y,z))) = f(y,f(f(x,y),f(y,z))). [para(11804(a,1),20(a,1,1)),rewrite(10248(11,R),10866(7),11742(7)),flip(a)]. given #506 (F,wt=13): 14708 f(f(x,x),f(y,f(c_0,f(z,x)))) = x # label(false). [para(20(a,1),14412(a,1,2,2)),rewrite(10248(3,R),13468(3),13468(6),10248(6),13468(6),20(9))]. given #507 (F,wt=15): 14438 f(f(x,y),f(x,f(x,f(c_0,f(y,z))))) = x # label(false). [para(14341(a,1),14279(a,1,2,2)),rewrite(13468(7))]. given #508 (F,wt=15): 14441 f(f(x,y),f(y,f(z,f(z,f(x,y))))) = y # label(false). [back_rewrite(13860),rewrite(14412(10))]. given #509 (F,wt=15): 14443 f(f(x,y),f(x,f(z,f(z,f(x,y))))) = x # label(false). [back_rewrite(13735),rewrite(13468(3),13468(4),14432(9),13468(10),13468(13),13468(15),13704(21),13468(10),10260(10))]. given #510 (T,wt=13): 14797 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(12953(a,2),14329(a,1,2,2)),rewrite(13468(4),13468(5),11742(7),13468(5))]. given #511 (T,wt=13): 14938 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(14797(a,1),6315(a,1,2,2)),rewrite(6315(3),13468(3)),flip(a)]. given #512 (T,wt=15): 14549 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0. [para(20(a,1),14414(a,1,1)),rewrite(13468(4))]. given #513 (T,wt=15): 14550 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,y)))) = c_0. [para(20(a,1),14414(a,1,2,2,2,2)),rewrite(10248(3,R),13468(3),13468(6),10248(6))]. given #514 (A,wt=21): 13190 f(f(x,y),f(f(z,f(c_0,f(x,y))),f(u,f(c_0,f(x,y))))) = c_0. [para(11774(a,1),12822(a,1,1))]. given #515 (F,wt=15): 14497 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x) # label(false). [para(20(a,1),14352(a,1,2,2,2,2)),rewrite(20(3),13468(3),10248(3))]. given #516 (F,wt=15): 14846 f(f(x,y),f(x,f(x,f(c_0,f(z,y))))) = x # label(false). [para(14708(a,1),14279(a,1,2,2)),rewrite(13468(7))]. given #517 (F,wt=15): 14861 f(f(x,f(y,z)),f(x,f(x,f(z,z)))) = x # label(false). [para(20(a,1),14438(a,1,2,2,2,2)),rewrite(13468(4),10248(4))]. given #518 (F,wt=15): 14864 f(f(x,f(x,f(y,y))),f(x,f(y,z))) = x # label(false). [para(10867(a,1),14438(a,1,2,2,2,2)),rewrite(13468(4),10248(4),13468(6))]. given #519 (T,wt=15): 14551 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,x)))) = c_0. [para(10867(a,1),14414(a,1,2,2,2,2)),rewrite(10248(3,R),13468(3),13468(6),10248(6))]. given #520 (T,wt=15): 14562 f(f(x,f(y,z)),f(c_0,f(x,f(z,z)))) = c_0. [para(20(a,1),14430(a,1,2,2,2,2)),rewrite(13468(5),10248(5))]. given #521 (T,wt=15): 14565 f(f(x,f(y,z)),f(c_0,f(x,f(y,y)))) = c_0. [para(10867(a,1),14430(a,1,2,2,2,2)),rewrite(13468(5),10248(5))]. given #522 (T,wt=15): 14566 f(x,f(c_0,f(y,f(c_0,f(z,f(x,z)))))) = c_0. [para(12305(a,1),14430(a,1,1)),rewrite(13468(8),11742(12))]. given #523 (A,wt=23): 13193 f(f(f(x,y),f(y,z)),f(y,f(u,f(c_0,f(f(x,y),f(y,z)))))) = c_0. [para(11804(a,1),12822(a,1,2,1)),rewrite(10248(11,R),10866(7),11742(7))]. given #524 (F,wt=15): 14867 f(f(x,y),f(y,f(y,f(c_0,f(x,z))))) = y # label(false). [para(13468(a,1),14438(a,1,1))]. given #525 (F,wt=15): 14895 f(x,f(f(x,y),f(z,f(x,z)))) = f(x,y) # label(false). [para(2962(a,1),14441(a,1,1)),rewrite(2962(4),13468(2))]. given #526 (F,wt=15): 14927 f(x,f(f(y,x),f(z,f(x,z)))) = f(y,x) # label(false). [para(20(a,1),14443(a,1,2,2,2,2)),rewrite(20(3),13468(2))]. given #527 (F,wt=15): 15031 f(f(x,f(x,y)),f(x,f(z,f(y,y)))) = x # label(false). [para(3680(a,1),14846(a,1,2,2,2,2)),rewrite(10270(6),13468(6))]. given #528 (T,wt=15): 14569 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(13468(a,1),14430(a,1,1))]. given #529 (T,wt=15): 14597 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0. [para(14381(a,1),14430(a,1,2,2)),rewrite(13468(3),13468(5))]. given #530 (T,wt=15): 14719 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(20(a,1),14511(a,1,2,2)),rewrite(10248(4,R),13468(4),13468(8),10248(8),13468(8))]. given #531 (T,wt=15): 14796 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(12953(a,1),14081(a,1,2)),rewrite(13468(1),13468(2),13984(5),10260(6),13468(5))]. given #532 (A,wt=19): 13245 f(c_0,f(f(x,y),f(x,z))) = f(x,f(f(x,y),f(x,z))). [para(11883(a,1),20(a,1,1)),rewrite(10248(11,R),10866(7),11742(7)),flip(a)]. given #533 (F,wt=15): 15066 f(x,f(y,f(y,f(x,x)))) = f(x,f(y,y)) # label(false). [para(14864(a,1),14081(a,1,2,2)),rewrite(13468(2),10248(2)),flip(a)]. given #534 (F,wt=15): 15140 f(f(x,f(y,z)),f(x,f(x,f(y,y)))) = x # label(false). [para(10867(a,1),14867(a,1,2,2,2,2)),rewrite(13468(2),13468(4),10248(4))]. given #535 (F,wt=15): 15421 f(x,f(f(x,f(x,y)),f(y,y))) = f(x,x) # label(false). [para(15031(a,1),14796(a,1,2)),flip(a)]. given #536 (F,wt=17): 14273 f(f(x,f(x,y)),f(f(x,y),f(x,z))) = f(x,y) # label(false). [para(11883(a,1),14243(a,1,2,2,2,2)),rewrite(13468(7),10248(7),13468(7),2962(7),13468(5),13468(6))]. given #537 (T,wt=15): 14985 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(14797(a,1),14797(a,1,2)),rewrite(13468(3))]. given #538 (T,wt=15): 15079 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0. [para(20(a,1),14562(a,1,2,2,2))]. given #539 (T,wt=15): 15101 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0. [para(14566(a,1),13468(a,1)),rewrite(13468(4),13468(9)),flip(a)]. given #540 (T,wt=15): 15115 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0. [para(14566(a,1),14412(a,1)),rewrite(13468(5)),flip(a)]. given #541 (A,wt=45): 13257 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))). [para(11883(a,1),8528(a,1,1)),rewrite(11883(18),13255(11))]. given #542 (F,wt=15): 15511 f(f(x,f(y,x)),f(x,f(z,f(y,x)))) = x # label(false). [para(20(a,1),14273(a,1,1,2)),rewrite(13468(2),20(5),13468(4),20(9))]. given #543 (F,wt=17): 14280 f(f(x,f(y,x)),f(f(y,x),f(x,z))) = f(y,x) # label(false). [para(13985(a,1),14243(a,1,2,2,2,2)),rewrite(13468(7),10248(7),20(7),13468(5),13468(6))]. given #544 (F,wt=17): 14289 f(x,f(f(x,y),f(z,f(x,f(x,y))))) = f(x,y) # label(false). [para(20(a,1),14276(a,1,1)),rewrite(13468(1),13468(2),13468(3),13468(5),2962(5),13468(3),13468(7))]. given #545 (F,wt=17): 14290 f(x,f(f(y,x),f(z,f(x,f(y,x))))) = f(y,x) # label(false). [para(20(a,1),14276(a,1,2,2,2,2)),rewrite(20(3),13468(3))]. given #546 (T,wt=15): 15323 f(f(c_0,f(x,f(x,y))),f(c_0,f(y,z))) = c_0. [para(12305(a,1),14569(a,1,1)),rewrite(13468(4),14751(12))]. given #547 (T,wt=15): 15597 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(20(a,1),15115(a,1,2,2,2,2,2)),rewrite(13468(3))]. given #548 (T,wt=15): 15601 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,z)))) = c_0. [para(14341(a,1),15115(a,1,2,2,2,2)),rewrite(13468(5))]. given #549 (T,wt=15): 15606 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,z)))) = c_0. [para(14708(a,1),15115(a,1,2,2,2,2)),rewrite(13468(5))]. given #550 (A,wt=23): 13310 f(f(f(x,y),f(x,z)),f(x,f(u,f(c_0,f(f(x,y),f(x,z)))))) = c_0. [para(11883(a,1),12822(a,1,2,1)),rewrite(10248(11,R),10866(7),11742(7))]. given #551 (F,wt=17): 14368 f(f(x,y),f(c_0,f(z,f(x,x)))) = f(z,f(x,x)) # label(false). [para(11131(a,1),14329(a,1,2,2,2)),rewrite(13468(8),2962(8),13468(6),10248(6),13468(6),13857(6)),flip(a)]. given #552 (F,wt=17): 14506 f(f(x,y),f(c_0,f(z,f(y,y)))) = f(z,f(y,y)) # label(false). [para(20(a,1),14381(a,1,1,2))]. given #553 (F,wt=17): 14633 f(f(x,f(x,y)),f(f(x,z),f(x,y))) = f(x,y) # label(false). [para(14431(a,1),14292(a,1,2,2)),rewrite(13468(5),13468(6))]. given #554 (F,wt=17): 14654 f(f(x,f(x,y)),f(f(z,x),f(x,y))) = f(x,y) # label(false). [para(13985(a,1),14389(a,1,2,2)),rewrite(13468(5),13468(6))]. given #555 (T,wt=13): 15897 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(14633(a,1),13857(a,1,2,2)),rewrite(13468(7),14631(7),14633(10))]. given #556 (T,wt=13): 15903 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(14654(a,1),13857(a,1,2,2)),rewrite(13468(7),14742(7),14654(10))]. given #557 (T,wt=13): 15916 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(15897(a,1),11742(a,1,2,2)),rewrite(11742(5),13468(4)),flip(a)]. given #558 (T,wt=15): 15723 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(20(a,1),15323(a,1,2,2)),rewrite(13468(7),10248(7),13468(7))]. given #559 (A,wt=47): 13497 f(f(x,f(c_0,f(f(y,z),f(y,u)))),f(c_0,f(y,f(f(c_0,f(f(y,z),f(y,u))),f(x,f(c_0,f(f(y,z),f(y,u)))))))) = f(c_0,f(f(y,z),f(y,u))). [back_rewrite(13410),rewrite(13468(3),13468(10),13468(15),13468(20),13468(25))]. given #560 (F,wt=17): 15284 f(f(x,x),f(y,f(x,y))) = f(f(x,x),f(y,y)) # label(false). [para(15031(a,1),14329(a,1,2,2)),rewrite(13468(3),10248(3),13468(4),13468(7)),flip(a)]. given #561 (F,wt=17): 15441 f(x,f(f(y,y),f(f(x,x),f(y,y)))) = f(x,y) # label(false). [para(20(a,1),15066(a,2,2)),rewrite(13468(4))]. given #562 (F,wt=17): 15492 f(f(x,f(x,y)),f(y,y)) = f(f(x,x),f(y,y)) # label(false). [para(15421(a,1),14081(a,1,2,2,2)),rewrite(13468(6),14847(8)),flip(a)]. given #563 (F,wt=17): 16087 f(f(c_0,f(x,y)),f(f(x,x),f(z,z))) = f(x,y) # label(false). [para(15284(a,1),14368(a,1,1)),rewrite(10248(7,R),13468(7),10270(7),13468(5),13468(7),10248(10,R),13468(10),10270(10),13468(8))]. given #564 (T,wt=17): 13934 f(f(c_0,f(x,y)),f(x,f(f(x,y),f(x,z)))) = c_0. [para(11140(a,1),13626(a,1,2,2,2)),rewrite(13468(8),6315(8),13468(8))]. given #565 (T,wt=17): 14108 f(f(c_0,f(x,y)),f(c_0,f(f(x,y),f(z,u)))) = c_0. [para(11897(a,1),13997(a,1,2,2,1))]. given #566 (T,wt=17): 14316 f(f(c_0,f(x,y)),f(f(x,y),f(z,u))) = f(x,y). [para(11897(a,1),14281(a,1,2,1)),rewrite(10248(14,R),13468(12),11742(12))]. given #567 (T,wt=17): 14319 f(x,f(f(y,f(x,x)),f(f(x,x),f(z,u)))) = c_0. [para(14281(a,1),13583(a,1,1,2,2)),rewrite(13468(6),14281(11),10270(9),13468(7))]. given #568 (A,wt=49): 13500 f(f(c_0,f(f(x,y),f(z,f(c_0,f(y,f(x,f(x,y))))))),f(f(c_0,f(y,f(x,f(x,y)))),f(z,f(c_0,f(y,f(x,f(x,y))))))) = f(c_0,f(y,f(x,f(x,y)))) # label(false). [back_rewrite(13390),rewrite(13468(2),13468(4),13468(7),13468(9),13468(11),13468(15),13468(17),13468(19),13468(20),13468(21),13468(23),13468(25),13468(27))]. given #569 (F,wt=17): 16201 f(f(c_0,f(x,y)),f(f(z,z),f(x,x))) = f(x,y) # label(false). [para(15492(a,1),14381(a,1,1)),rewrite(13468(5),13468(7),13468(8))]. given #570 (F,wt=17): 16241 f(f(c_0,f(x,y)),f(f(y,y),f(z,z))) = f(x,y) # label(false). [para(13468(a,1),16087(a,1,1,2)),rewrite(13468(8))]. given #571 (F,wt=19): 14378 f(x,f(c_0,f(y,f(c_0,f(x,z))))) = f(y,f(c_0,f(x,z))) # label(false). [para(11298(a,1),14329(a,1,2,2,2)),rewrite(10260(11),13468(10),13857(10)),flip(a)]. given #572 (F,wt=15): 16417 f(f(x,y),f(x,f(y,f(c_0,f(x,z))))) = x # label(false). [para(14378(a,1),14438(a,1,2,2))]. given #573 (T,wt=15): 16426 f(f(c_0,f(x,f(x,y))),f(c_0,f(z,y))) = c_0. [para(15606(a,1),14378(a,1,2,2)),rewrite(9695(4),13468(6),13468(9)),flip(a)]. given #574 (T,wt=15): 16501 f(f(c_0,f(x,y)),f(c_0,f(z,f(z,y)))) = c_0. [para(16426(a,1),14378(a,1,2,2)),rewrite(9695(4),13468(9)),flip(a)]. given #575 (T,wt=17): 14436 f(f(x,x),f(f(x,y),f(z,f(c_0,f(x,u))))) = c_0. [para(14341(a,1),13583(a,1,1,2,2)),rewrite(13468(5),13468(6),14341(13),13468(8),10248(8),13468(8))]. given #576 (T,wt=17): 14538 f(x,f(y,f(c_0,f(f(x,x),f(z,u))))) = f(x,x). [para(14281(a,1),14381(a,1,2,2)),rewrite(10248(7,R),13468(5),10270(9),13468(7),14281(11))]. given #577 (A,wt=23): 13516 f(f(c_0,f(x,f(y,f(z,x)))),f(f(z,x),f(y,f(z,x)))) = f(z,x) # label(false). [back_rewrite(13246),rewrite(13468(3),13468(7),13468(8),13468(10))]. given #578 (F,wt=15): 16421 f(f(x,y),f(y,f(x,f(c_0,f(y,z))))) = y # label(false). [para(14378(a,1),14867(a,1,2,2))]. given #579 (F,wt=15): 16597 f(f(x,f(y,f(z,z))),f(x,f(z,x))) = x # label(false). [para(14381(a,1),16421(a,1,2,2)),rewrite(13468(3),13468(4))]. given #580 (F,wt=19): 14379 f(x,f(c_0,f(y,f(c_0,f(z,x))))) = f(y,f(c_0,f(z,x))) # label(false). [para(11600(a,1),14329(a,1,2,2,2)),rewrite(13857(11),13468(10),13857(10)),flip(a)]. given #581 (F,wt=19): 14395 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)) # label(false). [back_rewrite(13988),rewrite(14368(8),14368(12))]. given #582 (T,wt=17): 14543 f(f(x,x),f(y,f(c_0,f(z,f(c_0,f(x,u)))))) = x. [para(14341(a,1),14381(a,1,2,2)),rewrite(10248(9,R),13468(6),13468(9),10248(9),13468(9),14341(15))]. given #583 (T,wt=17): 14555 f(f(c_0,f(x,f(y,y))),f(f(z,y),f(y,u))) = c_0. [para(13027(a,1),14414(a,1,2,2,2,2)),rewrite(10248(11,R),13468(7),11742(7),13468(6),10248(6),13468(8))]. given #584 (T,wt=17): 14556 f(f(x,x),f(c_0,f(y,f(f(x,z),f(x,u))))) = c_0. [para(13312(a,1),14414(a,1,2,2,2,2)),rewrite(11742(9))]. given #585 (T,wt=17): 14557 f(f(c_0,f(x,f(y,y))),f(f(y,z),f(y,u))) = c_0. [para(13314(a,1),14414(a,1,2,2,2,2)),rewrite(10248(11,R),13468(7),11742(7),13468(6),10248(6),13468(8))]. given #586 (A,wt=47): 13541 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(13022),rewrite(13468(20))]. given #587 (F,wt=19): 14411 f(x,f(x,f(y,f(c_0,f(x,z))))) = f(y,f(c_0,f(x,z))) # label(false). [para(14341(a,1),8888(a,1,1)),rewrite(14341(10),13468(5))]. given #588 (F,wt=19): 14413 f(f(x,f(c_0,f(y,z))),f(y,f(x,f(c_0,f(y,z))))) = y # label(false). [para(14341(a,1),13942(a,1,2,2)),rewrite(13468(9),14341(16))]. given #589 (F,wt=19): 14440 f(f(c_0,f(x,y)),f(c_0,f(x,z))) = f(z,f(c_0,f(x,y))) # label(false). [para(14341(a,1),14329(a,1,2,2,2)),rewrite(13468(5))]. given #590 (F,wt=15): 16912 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))) # label(false). [para(14440(a,2),13468(a,2)),rewrite(13468(4),16911(11))]. ============================== PROOF ================================= % Proof 1 at 40.89 (+ 0.12) seconds: A_SS. % Length of proof is 315. % Level of proof is 59. % Maximum clause weight is 59. % Given clauses 590. 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS) # 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)]. 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)),v),f(f(f(f(x,v),v),f(z,x)),f(f(z,x),w)))) = 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),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y. [para(2(a,1),7(a,1,1,2)),rewrite(2(12),2(12),2(14),2(17),2(30))]. 12 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(2(a,1),8(a,1,2,2))]. 20 f(f(x,y),f(y,y)) = y. [para(2(a,1),12(a,1,2,1))]. 37 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(20(a,1),2(a,1,2,1))]. 38 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(20(a,1),2(a,1,2,2,1,1,1,1))]. 39 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(20(a,1),2(a,1,2,2,1,1,1))]. 40 f(f(x,f(y,y)),f(f(y,y),f(y,f(f(y,y),z)))) = f(y,y). [para(20(a,1),2(a,1,2,2,1)),rewrite(20(5))]. 45 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z). [para(20(a,1),7(a,1,2,2,1,1,1))]. 46 f(f(x,f(y,y)),y) = f(y,y). [para(20(a,1),7(a,1,2,2,1)),rewrite(20(5),20(5))]. 55 f(f(f(x,x),y),x) = f(x,x). [para(12(a,1),20(a,1,1)),rewrite(12(7)),flip(a)]. 57 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(37),rewrite(46(7))]. 60 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(46(a,1),2(a,1,2,2,1,1,1))]. 62 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(46(a,1),7(a,1,2,2,1,1,1,1))]. 68 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(55(a,1),2(a,1,2,2,1,1,1,1))]. 69 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x. [para(55(a,1),2(a,1,2,2,1,1))]. 77 f(f(x,y),f(x,x)) = x. [para(20(a,1),55(a,1,1,1)),rewrite(20(6))]. 80 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(77(a,1),2(a,1,2,2,1,1))]. 82 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(2(a,1),77(a,1,1))]. 84 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(77(a,1),7(a,1,2,2,1,1))]. 91 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(77(a,1),77(a,1,1))]. 96 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(82(a,1),2(a,1,2,2,2))]. 97 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),82(a,1,2,1)),rewrite(2(20),2(22))]. 119 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(46(a,1),80(a,1,2,2,1)),rewrite(82(9))]. 124 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(77(a,1),80(a,1,2,1,2,1)),rewrite(77(9),77(11))]. 125 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(77(a,1),80(a,1,2,2,2))]. 127 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(82(a,1),80(a,1,2,1,2,1)),rewrite(82(10),82(13))]. 128 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(82(a,1),80(a,1,2,2,2))]. 137 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(20(a,1),128(a,1,2,1,2,1)),rewrite(20(9),20(11))]. 138 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x. [para(20(a,1),128(a,1,2,1,2))]. 146 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(77(a,1),128(a,1,2,1,2,1)),rewrite(77(9),77(11))]. 148 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(82(a,1),128(a,1,2,1,2,1)),rewrite(82(10),82(13))]. 169 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(91(a,1),128(a,1,2,1,2,1)),rewrite(91(10),91(13))]. 180 f(x,f(f(x,x),f(x,f(f(x,x),y)))) = f(x,x). [para(20(a,1),57(a,1,1)),rewrite(77(4))]. 181 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x. [para(57(a,1),55(a,1)),flip(a)]. 184 f(f(x,y),f(y,f(f(y,y),f(z,y)))) = y. [para(82(a,1),57(a,1,2,2,2))]. 207 f(f(x,f(f(x,x),f(y,x))),f(x,f(f(x,x),f(y,x)))) = x. [para(184(a,1),55(a,1)),flip(a)]. 237 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(20(a,1),127(a,1,2,1,1))]. 245 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [para(20(a,1),148(a,1,1,1,1)),rewrite(20(3),77(3),77(3),20(3),20(3),20(5))]. 246 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(20(a,1),148(a,1,2,1,1))]. 257 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(20(a,1),169(a,1,2,1,1))]. 270 f(f(f(x,x),f(x,f(f(x,x),y))),f(f(x,x),f(x,f(f(x,x),y)))) = f(x,x). [para(40(a,1),55(a,1)),flip(a)]. 287 f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x)) = x. [para(69(a,1),82(a,1,2,1)),rewrite(69(16),69(18))]. 300 f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)) = x. [para(119(a,1),82(a,1,2,1)),rewrite(119(15),119(17))]. 325 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(77(a,1),124(a,1,2,2,2))]. 360 f(f(f(x,f(x,x)),f(f(x,x),f(y,x))),f(x,x)) = x. [para(82(a,1),300(a,1,1,2,2))]. 414 f(x,f(f(x,x),f(x,y))) = f(x,x). [para(57(a,1),360(a,1,1,2,2)),rewrite(181(13),181(14),20(7),181(9)),flip(a)]. 415 f(x,f(f(x,x),f(y,x))) = f(x,x). [para(184(a,1),360(a,1,1,2,2)),rewrite(207(13),207(14),20(7),207(9)),flip(a)]. 416 f(f(x,x),f(x,f(f(x,x),y))) = x. [para(180(a,1),360(a,1,1,2,2)),rewrite(270(16),270(18),77(10),46(8),270(12),77(3)),flip(a)]. 429 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(414(a,1),128(a,1,1)),rewrite(55(12),55(13),77(11),55(13))]. 435 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(414(a,1),84(a,1,1)),rewrite(55(12),55(13),77(11),55(13))]. 442 f(f(x,x),f(x,f(y,f(x,x)))) = x. [para(20(a,1),415(a,1,2,1)),rewrite(77(8))]. 453 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(416(a,1),2(a,1,2,2,1,1,1)),rewrite(416(6))]. 565 f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(x,x)) = x. [para(138(a,1),82(a,1,2,1)),rewrite(138(16),138(18))]. 822 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x). [para(20(a,1),565(a,1,1,1,1)),rewrite(77(5),77(11))]. 923 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(39(a,1),84(a,1,2,1,2,1)),rewrite(39(25),39(27))]. 930 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(565(a,1),39(a,1,2,2,1)),rewrite(20(4),77(3),82(6))]. 951 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(20(a,1),930(a,1,2,1,1)),rewrite(77(7),77(11))]. 952 f(x,f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(82(a,1),930(a,1,2,2,2))]. 983 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x. [para(80(a,1),45(a,1,2,2,1)),rewrite(77(3),82(6),20(6),930(7),77(4),82(7),20(7),77(10),82(13),20(13),20(21),416(21),46(17),77(3),77(3),82(6),20(6)),flip(a)]. 985 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x. [para(128(a,1),45(a,1,2,2,1)),rewrite(77(3),82(6),20(6),952(7),77(4),82(7),20(7),77(10),82(13),20(13),20(21),442(21),46(17),77(3),77(3),82(6),20(6)),flip(a)]. 1016 f(f(x,f(x,x)),f(x,f(f(x,x),y))) = x. [para(39(a,1),45(a,1,2,2,1)),rewrite(77(3),77(6),77(10),77(13),77(16),77(19),77(27),416(27),46(23),77(9),77(3),77(6)),flip(a)]. 1017 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x). [para(951(a,1),45(a,1,1)),rewrite(77(16),77(18),119(23),414(18),20(16)),flip(a)]. 1057 f(f(f(x,x),x),f(f(x,x),f(x,y))) = f(x,x). [para(20(a,1),1016(a,1,1,2)),rewrite(77(6))]. 1125 f(f(f(f(x,x),f(x,y)),f(x,f(x,x))),x) = f(x,f(x,x)). [para(1017(a,1),125(a,1,2,1,2,1)),rewrite(1017(18),77(14),1017(18),55(17),20(14))]. 1182 f(f(x,x),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(x,y)))) = x. [para(1125(a,1),2(a,1,2,2,1))]. 1260 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(82(a,1),453(a,1,2,2,2))]. 1336 f(f(x,x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(82(a,1),1260(a,1,2))]. 1347 f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x))) = f(x,x). [para(20(a,1),1336(a,1,1)),rewrite(77(5))]. 1403 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))),f(x,x)) = x. [para(60(a,1),82(a,1,2,1)),rewrite(60(19),60(21))]. 1483 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(u,y)))) = y. [para(414(a,1),96(a,1,2,2,1,1,1))]. 1514 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(1016(a,1),96(a,1,2,2,1,1,1)),rewrite(416(7))]. 1567 f(f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(69(a,1),97(a,1,1,2,1,1,1,1)),rewrite(77(3),77(12))]. 1699 f(f(x,x),f(x,f(x,x))) = x. [para(20(a,1),1182(a,1,2))]. 1751 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,f(y,y))),f(y,f(y,y))),y),f(y,z)))) = y # label(false). [para(1699(a,1),2(a,1,2,1))]. 1755 f(x,f(f(x,x),x)) = f(x,x). [para(20(a,1),1699(a,1,1)),rewrite(77(4))]. 1780 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,f(y,y))),f(y,f(y,y))),y),f(z,y)))) = y # label(false). [para(1699(a,1),96(a,1,2,1))]. 1826 f(f(f(f(x,x),f(x,y)),f(f(x,x),x)),f(f(f(x,x),x),f(f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),x)))),f(f(x,x),x)),f(f(f(x,x),x),z)))) = f(f(x,x),x). [para(1057(a,1),1751(a,1,2,2,1,1,1,1)),rewrite(138(18))]. 1860 f(f(x,y),f(f(f(f(y,x),f(y,f(y,y))),f(y,f(y,y))),y)) = y # label(false). [para(82(a,1),1780(a,1,2))]. 1902 f(f(x,f(y,y)),f(f(f(f(f(y,y),x),f(f(y,y),y)),f(f(y,y),y)),f(y,y))) = f(y,y) # label(false). [para(20(a,1),1860(a,1,2,1,1,2,2)),rewrite(77(11))]. 1968 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(f(x,x),x)),f(f(f(f(x,x),f(f(x,x),x)),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(false). [para(1755(a,1),38(a,1,2,2,1,1,1))]. 2448 f(f(f(x,x),x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(82(a,1),1514(a,1,2))]. 2472 f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(2448(a,1),62(a,1,2,2,1)),rewrite(77(5),1347(8),77(6),77(13),77(21),46(19),77(3),77(5)),flip(a)]. 2737 f(f(f(x,x),f(f(x,x),f(f(x,x),f(x,y)))),f(x,x)) = f(f(x,x),f(f(x,x),f(x,y))). [para(2472(a,1),125(a,1,2,1,2,1)),rewrite(2472(25),2472(27),77(28),46(21))]. 2791 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(55(a,1),68(a,1,2,2,2))]. 2951 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(f(x,x),x)),f(f(f(f(x,x),f(f(x,x),x)),f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [para(82(a,1),1968(a,1,2,2,2))]. 2956 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(20(a,1),2791(a,1,1,2,1)),rewrite(77(6),77(7),77(10),77(12),77(14),77(17))]. 2962 f(f(x,x),f(x,y)) = x. [para(983(a,1),2791(a,1,2,2,1)),rewrite(77(4),414(4),77(5),77(8),77(13),46(11),77(3),77(4)),flip(a)]. 2963 f(f(x,x),f(y,x)) = x. [para(985(a,1),2791(a,1,2,2,1)),rewrite(2962(4),415(4),2962(5),2962(8),2962(13),46(11),2962(3),2962(4)),flip(a)]. 2966 f(x,f(f(f(f(x,f(x,f(x,x))),f(x,f(x,f(x,x)))),y),f(f(f(f(x,y),y),f(x,f(x,f(x,x)))),x))) = f(x,f(x,f(x,x))). [para(1902(a,1),2791(a,1,1,2)),rewrite(2962(3),2962(3),2962(3),1755(3),2963(4),2962(6),2962(6),1755(6),2963(7),2962(11),2962(13),2962(13),1755(13),2963(14),2962(17),2962(20),2962(20),1755(20),2963(21))]. 2970 f(x,f(x,f(x,x))) = f(x,x). [para(1902(a,1),2791(a,2)),rewrite(2962(4),2962(4),1755(4),2963(5),2962(5),2962(3),2962(3),1755(3),2963(4),2962(6),2962(6),1755(6),2963(7),2962(11),2962(13),2962(13),1755(13),2963(14),2962(17),2966(17))]. 2975 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(2956),rewrite(2962(3))]. 2989 f(f(x,x),x) = f(x,f(x,x)). [back_rewrite(2737),rewrite(2962(5),2963(4),2962(6)),flip(a)]. 3020 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)). [back_rewrite(1826),rewrite(2962(3),2989(2),2970(3),2989(3),2989(5),2989(7),2989(9),245(12),2989(6),2962(7),2989(5),2989(11))]. 3024 f(f(x,y),f(y,f(f(f(f(y,x),f(f(y,x),f(y,x))),y),f(z,y)))) = y. [back_rewrite(1483),rewrite(2962(8),2962(4),2962(10),2989(6))]. 3043 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = x. [back_rewrite(435),rewrite(2962(4),2962(4),2989(3),2962(7),2989(5),2962(12))]. 3045 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = x. [back_rewrite(429),rewrite(2962(4),2962(4),2989(3),2962(7),2989(5),2962(8),2962(12))]. 3047 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(325),rewrite(2962(3))]. 3049 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(146),rewrite(2962(3))]. 3055 f(x,f(f(f(f(y,x),f(y,x)),f(x,f(x,x))),f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [back_rewrite(2951),rewrite(2963(3),2989(5),2989(9),2962(10))]. 3130 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(137),rewrite(2963(3))]. 3393 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [back_rewrite(1403),rewrite(2989(4))]. 3450 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(x,x)) = x. [back_rewrite(565),rewrite(2989(2),2989(4))]. 3480 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x)) = x. [back_rewrite(287),rewrite(2989(2),2989(4))]. 3541 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(2(a,1),2962(a,1,2))]. 3547 f(f(f(x,y),f(x,y)),x) = f(x,y). [para(77(a,1),2962(a,1,2))]. 3549 f(f(f(f(f(f(x,y),f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),f(f(x,y),u))),x),f(f(f(x,x),v),f(f(f(f(f(x,y),v),v),x),f(x,w)))) = x. [para(2962(a,1),5(a,1,1,2)),rewrite(77(7),2962(16),2962(16),2962(21),2962(22),2962(26))]. 3564 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(2962(a,1),237(a,1,1,1,1,2)),rewrite(2962(4),2962(6),3541(4),2962(5),2962(6),2962(9),2962(10),2962(11),2962(15))]. 3565 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(2962(a,1),246(a,1,1,1,1,2)),rewrite(2962(4),2962(6),3541(4),2962(5),2962(6),2962(9),2962(10),2962(11),2962(15))]. 3567 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(2962(a,1),257(a,1,1,1,1,1)),rewrite(2962(4),2962(6),3547(4),2962(5),2962(6),2962(9),2962(10),2962(11),2962(15))]. 3571 f(f(f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),f(f(x,y),z))),x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,y)))) = x # label(false). [para(2962(a,1),923(a,1,1,2)),rewrite(2962(6),3547(4),2962(5),2989(3),2962(13),2962(13),2962(19),2962(24))]. 3576 f(f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))),f(x,x)) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))). [para(822(a,1),2962(a,1,2))]. 3680 f(x,f(y,f(x,x))) = f(x,x). [para(20(a,1),2963(a,1,1))]. 3712 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(2989(a,1),2(a,1,2,1))]. 3737 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(2989(a,1),96(a,1,2,1))]. 3808 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(82(a,1),3712(a,1,2,2,1,1,1,1)),rewrite(3541(4))]. 3811 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(91(a,1),3712(a,1,2,2,1,1,1,1)),rewrite(3547(4))]. 3841 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(82(a,1),3737(a,1,2,2,1,1,1,1)),rewrite(3541(4))]. 3943 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(z,x),f(f(f(f(x,z),z),f(z,x)),f(f(z,x),v)))) = f(z,x). [para(3547(a,1),5(a,1,2,1))]. 4019 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)). [para(3811(a,1),39(a,1,2,2)),rewrite(245(9),3576(20),46(12),82(7)),flip(a)]. 4180 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,y)),x))) = f(x,y). [para(3541(a,1),2975(a,1,2,1))]. 4343 f(f(f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),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),v)))) = f(y,x). [para(3564(a,1),2(a,1,2,2,1,1,1,1))]. 4414 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(3393(a,1),3547(a,1,1,1)),rewrite(3393(10),3393(20))]. 4747 f(f(x,y),f(f(f(y,x),f(f(y,x),f(y,x))),y)) = y. [para(82(a,1),3024(a,1,2))]. 4975 f(x,f(f(x,f(x,x)),f(y,x))) = f(y,x). [para(20(a,1),4747(a,1,2,1,1)),rewrite(2963(3),20(3),20(3))]. 4978 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y). [para(77(a,1),4747(a,1,2,1,1)),rewrite(2962(3),77(3),77(3))]. 4979 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),y)) = y. [para(82(a,1),4747(a,1,2,1,1)),rewrite(3541(4),82(6),82(7))]. 4984 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = x. [para(91(a,1),4747(a,1,2,1,1)),rewrite(3547(4),91(6),91(7))]. 5024 f(x,f(f(x,f(x,x)),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))). [para(3043(a,1),4747(a,1,1)),rewrite(3480(9),3480(9),3480(9))]. 5030 f(x,f(f(x,f(x,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))). [para(3045(a,1),4747(a,1,1)),rewrite(3450(9),3450(9),3450(9))]. 5126 f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,f(x,x))))) = f(y,f(x,f(x,x))). [para(4019(a,1),4975(a,1,2,1))]. 5136 f(f(x,x),f(f(x,f(x,x)),f(y,x))) = f(x,f(x,x)). [para(4975(a,1),3020(a,1,2,2))]. 5182 f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,f(x,x)),y))) = f(f(x,f(x,x)),y). [para(4019(a,1),4978(a,1,2,1))]. 5192 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)). [para(4978(a,1),3020(a,1,2,2))]. 5201 f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))) = f(y,x). [back_rewrite(5030),rewrite(5182(10),4975(5)),flip(a)]. 5202 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))) = f(x,y). [back_rewrite(5024),rewrite(5182(10),4978(5)),flip(a)]. 5246 f(f(f(f(f(x,y),f(f(x,y),f(x,y))),y),f(x,y)),f(f(f(f(x,y),f(x,y)),f(y,y)),f(f(y,f(x,y)),y))) = f(x,y) # label(false). [para(4979(a,1),84(a,1,2,1,2,1)),rewrite(4979(19),4979(21))]. 5247 f(f(f(f(f(x,y),f(f(x,y),f(x,y))),y),f(x,y)),f(f(f(f(x,y),f(x,y)),f(y,y)),f(f(y,f(x,y)),x))) = f(x,y). [para(4979(a,1),125(a,1,2,1,2,1)),rewrite(4979(19),4979(21))]. 5271 f(x,f(f(x,f(x,x)),f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),x),f(x,z))))) = f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),x),f(x,z))). [para(3564(a,1),4979(a,1,1)),rewrite(3564(12),3564(12),3564(12))]. 5272 f(x,f(f(x,f(x,x)),f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),x),f(z,x))))) = f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),x),f(z,x))). [para(3565(a,1),4979(a,1,1)),rewrite(3565(12),3565(12),3565(12))]. 5440 f(f(f(f(f(x,y),f(f(x,y),f(x,y))),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(4984(a,1),84(a,1,2,1,2,1)),rewrite(4984(19),4984(21))]. 5499 f(f(f(x,y),f(x,y)),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = f(f(x,y),f(f(x,y),f(x,y))). [para(2962(a,1),5136(a,1,2,2))]. 5500 f(f(f(x,y),f(x,y)),f(f(f(x,y),f(f(x,y),f(x,y))),y)) = f(f(x,y),f(f(x,y),f(x,y))). [para(2963(a,1),5136(a,1,2,2))]. 5589 f(f(x,f(x,x)),f(f(y,x),f(y,x))) = f(y,x). [para(5201(a,1),91(a,1,2,1)),rewrite(5201(10),5201(13))]. 5596 f(f(x,f(x,x)),f(y,x)) = f(f(y,x),f(y,x)). [para(5201(a,1),45(a,1,1)),rewrite(5202(24),5201(23),3680(21)),flip(a)]. 5609 f(f(x,f(x,x)),f(f(f(f(y,x),f(y,x)),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(x,f(x,x)),f(y,x)),f(x,f(x,x))))) = f(y,x). [para(5201(a,1),3047(a,1,2,1,1,1)),rewrite(5201(10),5201(20),5201(27))]. 5620 f(f(f(x,y),f(x,y)),f(y,f(y,y))) = f(x,y). [para(5201(a,1),3547(a,1,1,1)),rewrite(5201(8),5201(13))]. 5675 f(x,f(f(y,x),f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x) # label(false). [back_rewrite(3055),rewrite(5620(6))]. 5885 f(f(x,y),f(f(f(f(y,f(y,y)),f(y,f(y,y))),f(f(x,y),f(x,y))),f(f(f(x,y),f(y,f(y,y))),y))) = f(y,f(y,y)). [para(5589(a,1),125(a,1,2,1,2,1)),rewrite(5620(6),5589(13),5589(16))]. 5905 f(f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))))),f(x,x)) = x. [para(4414(a,1),5589(a,1,2,1)),rewrite(4414(36),4414(38))]. 5931 f(f(f(x,y),f(x,y)),f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)). [para(5596(a,1),77(a,1,1))]. 6046 f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(y,x),f(y,x))) = f(x,f(x,x)). [para(5596(a,1),2962(a,1,2))]. 6047 f(f(f(x,y),f(f(x,y),f(x,y))),x) = f(x,x). [para(2962(a,1),5596(a,1,2)),rewrite(2962(9),2962(9))]. 6048 f(f(f(x,y),f(f(x,y),f(x,y))),y) = f(y,y). [para(2963(a,1),5596(a,1,2)),rewrite(2963(9),2963(9))]. 6049 f(f(f(x,f(x,x)),f(y,x)),f(y,x)) = f(f(y,x),f(f(y,x),f(y,x))). [para(5596(a,2),2989(a,1,1))]. 6050 f(f(x,y),f(f(y,f(y,y)),f(x,y))) = f(f(x,y),f(f(x,y),f(x,y))). [para(5596(a,2),2989(a,2,2)),rewrite(2989(5)),flip(a)]. 6101 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(5596(a,2),3565(a,1,2,2))]. 6130 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(5596(a,2),3049(a,1,2,2))]. 6138 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(5596(a,2),3130(a,1,2,2))]. 6146 f(f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))))),x) = f(x,x). [para(4414(a,1),5596(a,1,2)),rewrite(4414(37),4414(37))]. 6193 f(f(x,x),f(f(y,x),f(y,x))) = f(x,f(x,x)). [para(5596(a,1),5136(a,1,2))]. 6199 f(f(f(x,y),f(f(y,f(y,y)),f(x,y))),f(f(f(x,y),f(f(x,y),f(x,y))),f(z,f(x,y)))) = f(z,f(x,y)). [para(5596(a,2),5201(a,1,1,2))]. 6203 f(f(f(x,y),f(f(y,f(y,y)),f(x,y))),f(z,f(x,y))) = f(f(z,f(x,y)),f(z,f(x,y))). [para(5596(a,2),5596(a,1,1,2))]. 6204 f(f(f(x,f(x,x)),f(y,x)),f(x,f(x,x))) = f(y,x). [back_rewrite(5609),rewrite(5931(11),5126(13))]. 6208 f(f(x,y),f(f(y,f(y,y)),f(f(f(x,y),f(y,f(y,y))),y))) = f(y,f(y,y)). [back_rewrite(5885),rewrite(6046(10))]. 6211 f(f(f(x,y),f(x,y)),f(x,x)) = f(f(x,y),f(f(x,y),f(x,y))). [back_rewrite(5499),rewrite(6047(9))]. 6216 f(x,f(f(f(x,y),f(f(x,y),f(x,y))),f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(5440),rewrite(6047(6),2962(3),6211(5))]. 6221 f(f(f(x,y),f(x,y)),f(y,y)) = f(f(x,y),f(f(x,y),f(x,y))). [back_rewrite(5500),rewrite(6048(9))]. 6225 f(x,f(f(f(y,x),f(f(y,x),f(y,x))),f(f(x,f(y,x)),y))) = f(y,x). [back_rewrite(5247),rewrite(6048(6),2963(3),6221(5))]. 6226 f(x,f(f(f(y,x),f(f(y,x),f(y,x))),f(f(x,f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(5246),rewrite(6048(6),2963(3),6221(5))]. 6232 f(f(x,y),f(f(x,y),y)) = y # label(false). [back_rewrite(6101),rewrite(6193(6),5201(9))]. 6244 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(f(y,x),x),f(z,x))))) = f(f(x,f(x,x)),f(f(f(y,x),x),f(z,x))). [back_rewrite(5272),rewrite(6193(7),6193(16))]. 6245 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(f(y,x),x),f(x,z))))) = f(f(x,f(x,x)),f(f(f(y,x),x),f(x,z))). [back_rewrite(5271),rewrite(6193(7),6193(16))]. 6277 f(f(f(f(x,f(x,x)),f(f(f(y,x),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),v)))) = f(y,x). [back_rewrite(4343),rewrite(6193(5))]. 6315 f(x,f(x,f(x,y))) = f(x,y) # label(false). [back_rewrite(6130),rewrite(6211(5),5201(14))]. 6425 f(x,f(x,f(y,x))) = f(y,x) # label(false). [back_rewrite(6138),rewrite(6221(5),5201(14))]. 6696 f(x,f(f(f(f(f(y,x),x),f(f(y,x),x)),f(f(f(f(y,x),x),f(y,x)),f(f(f(y,x),x),f(y,x)))),f(f(f(f(f(y,x),x),f(y,x)),f(f(y,x),x)),f(y,x)))) = f(f(y,x),x). [para(6232(a,1),125(a,1,1))]. 6732 f(f(x,y),f(f(x,y),x)) = x # label(false). [para(3547(a,1),6232(a,1,1)),rewrite(3547(5))]. 6878 f(f(x,y),f(f(f(f(y,f(x,y)),f(y,f(x,y))),f(f(f(y,f(x,y)),y),f(f(y,f(x,y)),y))),f(f(f(f(y,f(x,y)),y),f(y,f(x,y))),f(z,f(y,f(x,y)))))) = f(y,f(x,y)). [para(6425(a,1),128(a,1,1))]. 6945 f(f(f(x,y),f(f(f(f(x,y),f(y,f(x,y))),f(y,y)),f(f(y,y),z))),y) = f(y,y) # label(false). [para(6425(a,1),1567(a,1,1,1)),rewrite(6425(4))]. 6956 f(f(x,y),f(f(x,y),f(x,y))) = f(y,f(y,y)). [para(5136(a,1),6425(a,1,2,2)),rewrite(6204(11),6049(6),5136(11))]. 7257 f(f(x,f(y,x)),x) = f(y,x) # label(false). [back_rewrite(6226),rewrite(6956(5),4975(7))]. 7258 f(x,f(f(x,f(x,x)),f(f(x,f(y,x)),y))) = f(y,x). [back_rewrite(6225),rewrite(6956(5))]. 7260 f(f(f(x,y),f(x,y)),f(y,y)) = f(y,f(y,y)). [back_rewrite(6221),rewrite(6956(10))]. 7263 f(x,f(f(y,f(y,y)),f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(6216),rewrite(6956(5))]. 7267 f(f(f(x,y),f(x,y)),f(x,x)) = f(y,f(y,y)). [back_rewrite(6211),rewrite(6956(10))]. 7271 f(f(f(x,y),f(f(y,f(y,y)),f(x,y))),f(f(y,f(y,y)),f(z,f(x,y)))) = f(z,f(x,y)). [back_rewrite(6199),rewrite(6956(11))]. 7286 f(f(x,f(x,x)),y) = f(y,y). [back_rewrite(6146),rewrite(6956(26),6956(17),6956(5))]. 7298 f(f(x,y),f(f(y,f(y,y)),f(x,y))) = f(y,f(y,y)). [back_rewrite(6050),rewrite(6956(11))]. 7308 f(f(x,f(x,x)),f(y,y)) = y. [back_rewrite(5905),rewrite(6956(26),6956(17),6956(5))]. 7471 f(f(x,y),f(f(y,f(y,y)),f(f(f(x,y),f(y,f(x,y))),f(z,f(y,f(x,y)))))) = f(y,f(x,y)). [back_rewrite(6878),rewrite(7257(9),7257(10),7260(10),6956(6),7257(6))]. 7483 f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(z,x)))) = f(y,f(z,x)). [back_rewrite(7271),rewrite(7298(6))]. 7492 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(z,f(z,z)),f(x,f(y,z))). [back_rewrite(6203),rewrite(7298(6)),flip(a)]. 7525 f(f(x,f(x,x)),f(f(f(y,x),x),f(z,x))) = f(x,f(f(f(y,x),x),f(z,x))). [back_rewrite(6244),rewrite(7483(10)),flip(a)]. 7629 f(f(x,y),f(y,f(f(f(f(f(x,y),y),y),y),f(z,y)))) = y # label(false). [back_rewrite(3841),rewrite(7525(10))]. 7636 f(f(x,y),f(y,f(f(f(y,x),y),f(y,z)))) = y # label(false). [para(6732(a,1),2(a,1,2,2,1,1,1)),rewrite(2963(5),7257(5))]. 7728 f(f(x,y),f(f(z,f(z,z)),y)) = y. [para(7286(a,2),20(a,1,2))]. 7732 f(x,f(f(y,f(y,y)),f(z,x))) = f(z,x). [para(7286(a,2),82(a,1,2))]. 7738 f(f(f(x,f(x,x)),y),f(y,z)) = y. [para(7286(a,2),80(a,1,1)),rewrite(2962(7),2989(5),2989(7),5202(10))]. 7747 f(x,f(f(y,f(y,y)),f(x,z))) = f(x,z). [para(7286(a,2),91(a,1,2))]. 7780 f(f(f(x,f(x,x)),f(y,z)),z) = f(y,z). [para(7286(a,2),84(a,1,1)),rewrite(2962(14),2989(9),6956(9),2989(11),6956(11),7257(9),77(8))]. 7826 f(f(x,y),f(f(f(f(f(f(y,x),y),y),y),f(z,y)),f(f(f(f(f(y,x),y),y),y),f(z,y)))) = y # label(false). [para(7286(a,1),96(a,1,2)),rewrite(2962(5),2962(6),2962(11),2962(12))]. 7856 f(x,f(f(y,f(y,y)),x)) = f(x,f(x,x)). [para(7286(a,2),2989(a,2,2)),rewrite(2989(2)),flip(a)]. 7880 f(f(x,f(x,x)),y) = f(y,f(x,f(x,x))). [para(7286(a,1),3547(a,1,1,1)),rewrite(2963(5)),flip(a)]. 7881 f(f(f(x,f(x,x)),f(y,z)),y) = f(y,z). [para(7286(a,2),3547(a,1,1))]. 7882 f(x,f(y,f(y,y))) = f(x,x). [para(7286(a,1),3547(a,2)),rewrite(7728(7))]. 7890 f(f(x,y),f(f(y,f(f(z,f(z,z)),y)),f(f(f(f(f(x,y),y),y),y),f(y,u)))) = y. [para(7286(a,2),3808(a,1,2,1,2))]. 7900 f(f(x,f(x,y)),x) = f(x,y) # label(false). [para(7286(a,1),2975(a,1,2,2,1,1)),rewrite(7267(5),2962(5),7732(7))]. 7920 f(f(x,y),f(f(f(f(z,f(z,z)),x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(u,x)))) = x. [para(7286(a,2),3567(a,1,2,1,1))]. 7992 f(f(x,x),f(f(x,f(f(y,f(y,y)),x)),f(z,x))) = f(x,f(x,x)). [para(7286(a,2),5136(a,1,2,1,2))]. 7994 f(f(x,x),f(f(x,y),f(x,y))) = f(x,f(x,x)). [para(7286(a,1),5192(a,1,2))]. 8021 f(f(f(x,f(x,x)),y),f(f(y,y),f(x,f(x,x)))) = f(x,f(x,x)). [para(7286(a,1),6732(a,1,2,1))]. 8028 f(f(f(x,y),x),f(x,y)) = x # label(false). [back_rewrite(3571),rewrite(7738(8),3547(4),7994(6),7732(9))]. 8165 f(f(x,y),y) = f(y,f(x,y)). [back_rewrite(6696),rewrite(7994(15),6956(8),8028(9),7308(6)),flip(a)]. 8439 f(f(x,y),f(f(y,f(f(z,f(z,z)),y)),f(f(y,f(x,y)),f(y,u)))) = y. [back_rewrite(7890),rewrite(8165(7),7257(8),8165(7))]. 8468 f(f(x,y),f(f(f(f(y,x),y),f(z,y)),f(f(f(y,x),y),f(z,y)))) = y # label(false). [back_rewrite(7826),rewrite(8165(4),7257(5),8165(8),7257(9))]. 8528 f(f(x,y),f(y,f(f(y,f(x,y)),f(z,y)))) = y # label(false). [back_rewrite(7629),rewrite(8165(3),7257(4),8165(3))]. 8873 f(f(f(f(x,f(x,x)),f(f(x,f(y,x)),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(u,f(x,u)),f(y,x)),f(f(y,x),v)))) = f(y,x). [back_rewrite(6277),rewrite(8165(4),8165(15))]. 8883 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,f(y,x)),f(x,z))))) = f(f(x,f(x,x)),f(f(x,f(y,x)),f(x,z))). [back_rewrite(6245),rewrite(8165(6),8165(15))]. 8888 f(f(x,y),f(y,f(x,y))) = y # label(false). [back_rewrite(6232),rewrite(8165(3))]. 9223 f(x,f(f(x,y),f(y,x))) = f(x,y). [back_rewrite(4180),rewrite(8165(3),8165(5),8888(5))]. 9261 f(f(f(f(f(x,x),y),f(f(f(y,f(f(x,z),y)),x),f(x,u))),f(z,x)),f(f(z,x),f(f(f(z,f(x,z)),f(z,x)),f(f(z,x),v)))) = f(z,x). [back_rewrite(3943),rewrite(8165(5),8165(14))]. 9368 f(f(f(f(f(f(x,y),f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),f(f(x,y),u))),x),f(f(f(x,x),v),f(f(f(v,f(f(x,y),v)),x),f(x,w)))) = x. [back_rewrite(3549),rewrite(8165(6),8165(18))]. 9532 f(f(x,y),f(f(y,f(y,y)),f(y,f(z,f(y,f(x,y)))))) = f(y,f(x,y)). [back_rewrite(7471),rewrite(8888(7))]. 9535 f(f(f(x,y),f(f(y,f(y,y)),f(f(y,y),z))),y) = f(y,y) # label(false). [back_rewrite(6945),rewrite(8888(5))]. 9547 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)). [para(7308(a,1),77(a,1,1))]. 9548 f(f(x,x),f(y,f(y,y))) = x. [para(7308(a,1),3547(a,1,1,1)),rewrite(7308(4),7308(8))]. 9549 f(f(x,f(x,x)),f(f(x,f(x,x)),y)) = y. [para(7308(a,1),6315(a,1,2,2)),rewrite(7308(10))]. 9560 f(x,f(f(y,f(y,y)),x)) = f(y,f(y,y)). [back_rewrite(8021),rewrite(9548(7),8165(4))]. 9563 f(f(x,f(x,x)),f(f(x,f(y,x)),f(x,z))) = f(x,f(f(x,f(y,x)),f(x,z))). [back_rewrite(8883),rewrite(9549(10)),flip(a)]. 9566 f(f(x,y),f(f(z,f(z,z)),f(f(y,f(x,y)),f(y,u)))) = y. [back_rewrite(8439),rewrite(9560(5))]. 9569 f(f(x,x),f(f(y,f(y,y)),f(z,x))) = f(x,f(x,x)). [back_rewrite(7992),rewrite(9560(5))]. 9584 f(x,f(x,x)) = f(y,f(y,y)). [back_rewrite(7856),rewrite(9560(4))]. 9602 f(f(f(x,f(f(x,f(y,x)),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(u,f(x,u)),f(y,x)),f(f(y,x),v)))) = f(y,x). [back_rewrite(8873),rewrite(9563(7))]. 9654 f(x,f(x,x)) = c_0. [new_symbol(9584)]. 9680 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_rewrite(9569),rewrite(9654(3),9654(7))]. 9683 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(y,z)))) = y # label(false). [back_rewrite(9566),rewrite(9654(3))]. 9695 f(x,f(c_0,c_0)) = c_0. [back_rewrite(9547),rewrite(9654(2),9654(3),9654(6))]. 9699 f(f(f(x,y),f(c_0,f(f(y,y),z))),y) = f(y,y) # label(false). [back_rewrite(9535),rewrite(9654(3))]. 9701 f(f(x,y),f(c_0,f(y,f(z,f(y,f(x,y)))))) = f(y,f(x,y)). [back_rewrite(9532),rewrite(9654(3))]. 10228 f(f(x,x),f(f(x,y),f(x,y))) = c_0. [back_rewrite(7994),rewrite(9654(7))]. 10245 f(f(x,y),f(f(f(c_0,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(z,x)))) = x # label(false). [back_rewrite(7920),rewrite(9654(3))]. 10248 f(x,c_0) = f(x,x). [back_rewrite(7882),rewrite(9654(2))]. 10249 f(f(c_0,f(x,y)),x) = f(x,y). [back_rewrite(7881),rewrite(9654(2))]. 10250 f(c_0,x) = f(x,x). [back_rewrite(7880),rewrite(9654(2),9654(4),10248(4))]. 10254 f(f(c_0,f(x,y)),y) = f(x,y). [back_rewrite(7780),rewrite(9654(2))]. 10260 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(7747),rewrite(9654(2))]. 10263 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(7732),rewrite(9654(2))]. 10265 f(f(x,f(y,z)),c_0) = f(c_0,f(x,f(y,z))). [back_rewrite(7492),rewrite(10248(5,R),9654(6))]. 10270 f(c_0,f(x,x)) = x. [back_rewrite(7308),rewrite(9654(2))]. 10271 f(x,f(c_0,f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(7263),rewrite(9654(2))]. 10275 f(x,f(c_0,f(f(x,f(y,x)),y))) = f(y,x). [back_rewrite(7258),rewrite(9654(2))]. 10318 f(f(x,y),f(c_0,f(f(f(x,y),c_0),y))) = c_0. [back_rewrite(6208),rewrite(9654(3),9654(5),9654(10))]. 10346 f(f(x,y),f(f(f(x,x),f(f(x,y),c_0)),f(f(f(x,y),x),f(z,x)))) = x # label(false). [back_rewrite(10245),rewrite(10250(3),10248(5,R))]. 10347 f(f(x,x),f(f(x,y),c_0)) = c_0. [back_rewrite(10228),rewrite(10248(4,R))]. 10514 f(f(f(x,f(f(x,f(y,x)),f(x,z))),f(y,x)),f(f(f(f(y,x),c_0),u),f(f(f(u,f(x,u)),f(y,x)),f(f(y,x),v)))) = f(y,x). [back_rewrite(9602),rewrite(10248(10,R))]. 10579 f(f(f(f(f(f(x,y),c_0),z),f(f(f(z,f(x,z)),f(x,y)),f(f(x,y),u))),x),f(f(f(x,x),v),f(f(f(v,f(f(x,y),v)),x),f(x,w)))) = x. [back_rewrite(9368),rewrite(10248(3,R))]. 10759 f(f(x,y),f(c_0,f(f(f(y,x),y),f(z,y)))) = y # label(false). [back_rewrite(8468),rewrite(10248(10,R),10265(7))]. 10839 f(f(f(x,y),c_0),y) = f(x,y). [back_rewrite(3541),rewrite(10248(3,R))]. 10847 f(c1,f(f(c2,c3),c_0)) != f(c2,f(f(c1,c3),c_0)) # answer(A_SS). [back_rewrite(3),rewrite(10248(8,R),10248(15,R))]. 10863 f(f(x,y),f(c_0,f(f(f(x,y),x),f(z,x)))) = x # label(false). [back_rewrite(10346),rewrite(10347(6))]. 10864 f(f(x,y),f(c_0,f(x,y))) = c_0. [back_rewrite(10318),rewrite(10839(6))]. 10866 f(f(x,y),x) = f(x,f(x,y)). [para(6315(a,1),7900(a,1,1))]. 10868 f(f(x,y),f(c_0,f(f(x,f(x,y)),f(z,x)))) = x # label(false). [back_rewrite(10863),rewrite(10866(4))]. 10909 f(f(x,y),f(c_0,f(f(y,f(y,x)),f(z,y)))) = y # label(false). [back_rewrite(10759),rewrite(10866(4))]. 11114 f(f(x,y),f(y,f(f(y,f(y,x)),f(y,z)))) = y # label(false). [back_rewrite(7636),rewrite(10866(3))]. 11197 f(f(x,y),c_0) = f(c_0,f(x,y)). [para(9680(a,1),5675(a,1,2,2,2)),rewrite(10864(9),9695(8))]. 11306 f(c1,f(c_0,f(c2,c3))) != f(c2,f(c_0,f(c1,c3))) # answer(A_SS). [back_rewrite(10847),rewrite(11197(6),11197(13))]. 11480 f(f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),f(f(x,y),u))),x),f(f(f(x,x),v),f(f(f(v,f(f(x,y),v)),x),f(x,w)))) = x. [back_rewrite(10579),rewrite(11197(3))]. 11522 f(f(f(x,f(f(x,f(y,x)),f(x,z))),f(y,x)),f(f(f(c_0,f(y,x)),u),f(f(f(u,f(x,u)),f(y,x)),f(f(y,x),v)))) = f(y,x). [back_rewrite(10514),rewrite(11197(10))]. 11742 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(10249(a,1),6315(a,1,2,2)),rewrite(8165(8),10864(8),10866(5),10249(9))]. 11775 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [para(10260(a,1),8528(a,1,1)),rewrite(10260(11),8165(9),10864(9),10263(11))]. 11793 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(z,y)))) = y # label(false). [para(6425(a,1),9683(a,1,2,2,2))]. 11883 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(x,z)))) = x # label(false). [para(10866(a,1),9683(a,1,1)),rewrite(10866(5),6315(6))]. 11902 f(f(f(x,f(y,y)),f(c_0,f(y,z))),f(y,y)) = y # label(false). [para(20(a,1),9699(a,1,1,2,2,1)),rewrite(10248(11,R),11197(11),10270(11))]. 11914 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(z,x)))) = x # label(false). [para(6315(a,1),10868(a,1,2,2,1))]. 11961 f(f(x,f(x,y)),f(y,x)) = x # label(false). [para(10909(a