============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 28195 was started by mccune on cleo, Fri Apr 13 10:01:05 2007 The command was "/home/mccune/bin/prover9 -f MOL-M.in MOL-M-interp.out13". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MOL-M.in assign(max_seconds,3600). assign(max_weight,60). assign(new_constants,1). set(lex_order_vars). set(restrict_denials). formulas(sos). f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x # label(MOL_SS). end_of_list. formulas(goals). f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(MOD_SS). end_of_list. % Reading from file MOL-M-interp.out13 list(interpretations). interpretation(10,[number = 1,seconds = 0],[function(A,[2]),function(B,[3]),function(C,[4]),function(f(_,_),[1,1,1,1,1,1,1,1,1,1,1,0,5,9,6,2,4,8,7,3,1,5,5,1,6,1,7,6,7,1,1,9,1,9,1,1,1,1,1,1,1,6,6,1,6,1,1,6,1,1,1,2,1,1,1,2,2,2,1,1,1,4,7,1,1,2,4,2,7,1,1,8,6,1,6,2,2,8,1,1,1,7,7,1,1,1,7,1,7,1,1,3,1,1,1,1,1,1,1,3])]). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(MOD_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(c3,f(c1,f(c2,c2)))) != f(c1,f(c2,f(c1,f(c3,c3)))) # answer(MOD_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). not interpretable: c1 % Clause contains symbol not in interpretation: % f(c1,f(c3,f(c1,f(c2,c2)))) != f(c1,f(c2,f(c1,f(c3,c3)))) # answer(MOD_SS). [deny(1)]. restricted denial: (wt=19): 3 f(c1,f(c3,f(c1,f(c2,c2)))) != f(c1,f(c2,f(c1,f(c3,c3)))) # answer(MOD_SS). [deny(1)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 3 f(c1,f(c3,f(c1,f(c2,c2)))) != f(c1,f(c2,f(c1,f(c3,c3)))) # answer(MOD_SS). [deny(1)]. end_of_list. formulas(sos). 2 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. end_of_list. formulas(demodulators). 2 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=25): 2 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. given #2 (A,wt=57): 4 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(y,v)))) = y. [para(2(a,1),2(a,1,2,1))]. given #3 (T,wt=9): 11 f(f(x,y),f(y,y)) = y. [para(4(a,1),4(a,1,2,2))]. given #4 (T,wt=11): 20 f(f(x,f(y,y)),y) = f(y,y). [para(11(a,1),11(a,1,2))]. given #5 (T,wt=13): 8 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(4(a,1),2(a,1,2,2))]. given #6 (T,wt=11): 32 f(f(f(x,x),y),x) = f(x,x). [para(8(a,1),11(a,1,1)),rewrite(8(7)),flip(a)]. given #7 (A,wt=53): 5 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),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 #8 (T,wt=9): 40 f(f(x,y),f(x,x)) = x. [para(11(a,1),32(a,1,1,1)),rewrite(11(6))]. given #9 (T,wt=13): 55 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(2(a,1),40(a,1,1))]. given #10 (T,wt=13): 61 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(40(a,1),40(a,1,1))]. given #11 (T,wt=15): 22 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(14),rewrite(20(7))]. given #12 (A,wt=57): 6 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),y),f(y,v)))) = y. [para(2(a,1),2(a,1,2,2,1,1,1))]. given #13 (T,wt=15): 85 f(f(x,y),f(y,f(f(y,y),f(z,y)))) = y. [para(55(a,1),22(a,1,2,2,2))]. given #14 (T,wt=17): 81 f(x,f(f(x,x),f(x,f(f(x,x),y)))) = f(x,x). [para(11(a,1),22(a,1,1)),rewrite(40(4))]. given #15 (T,wt=17): 102 f(x,f(f(x,x),f(x,f(y,f(x,x))))) = f(x,x). [para(11(a,1),85(a,1,1)),rewrite(40(4))]. given #16 (T,wt=21): 17 f(f(x,f(y,y)),f(f(y,y),f(y,f(f(y,y),z)))) = f(y,y). [para(11(a,1),2(a,1,2,2,1)),rewrite(11(5))]. given #17 (A,wt=35): 7 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z). [para(2(a,1),2(a,1,2,2,2))]. given #18 (F,wt=33): 127 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(false). [para(11(a,1),7(a,1,2,2,1,1,1,1))]. given #19 (F,wt=45): 130 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),z),f(f(f(f(f(x,x),z),z),f(y,f(x,x))),f(x,x)))) = f(y,f(x,x)) # label(false). [para(20(a,1),7(a,1,2,2,1,1,1,1))]. given #20 (T,wt=21): 37 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x. [para(32(a,1),2(a,1,2,2,1,1))]. given #21 (T,wt=21): 82 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x. [para(22(a,1),32(a,1)),flip(a)]. given #22 (T,wt=13): 182 f(x,f(f(x,x),f(x,y))) = f(x,x). [para(82(a,1),11(a,1,1)),rewrite(82(9)),flip(a)]. given #23 (T,wt=13): 193 f(f(x,x),f(x,f(f(x,x),y))) = x. [para(11(a,1),182(a,1,2,1)),rewrite(40(8))]. given #24 (A,wt=35): 9 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(x,z)))),x),f(x,u)))) = x. [para(2(a,1),4(a,1,2,2,1,1,1))]. given #25 (T,wt=13): 196 f(x,f(f(x,x),f(y,x))) = f(x,x). [para(55(a,1),182(a,1,2,2))]. given #26 (T,wt=13): 205 f(f(x,x),f(x,f(y,f(x,x)))) = x. [para(55(a,1),193(a,1,2,2))]. given #27 (T,wt=19): 234 f(f(f(f(x,x),x),f(f(x,x),x)),x) = f(f(x,x),x). [para(127(a,1),205(a,1,2,2)),rewrite(165(13),32(14),40(11)),flip(a)]. given #28 (T,wt=21): 174 f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x)) = x. [para(37(a,1),55(a,1,2,1)),rewrite(37(16),37(18))]. given #29 (A,wt=31): 12 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(z,x)),y),y),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(11(a,1),2(a,1,1)),rewrite(11(3))]. given #30 (T,wt=21): 175 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x. [para(55(a,1),37(a,1,2,2,2))]. given #31 (T,wt=21): 192 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)). [para(2(a,1),182(a,1,2,2))]. given #32 (T,wt=21): 195 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)). [para(40(a,1),182(a,1,2,2))]. given #33 (T,wt=21): 235 f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(130(a,1),205(a,1,2,2)),rewrite(40(3),40(5),40(10),40(12),169(15),40(8),40(10),40(15),32(15),40(11),40(5),40(7)),flip(a)]. given #34 (A,wt=33): 13 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(11(a,1),2(a,1,2,1,1))]. given #35 (T,wt=21): 246 f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(x,x)) = x. [para(55(a,1),174(a,1,1,2,2))]. given #36 (T,wt=23): 171 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [para(11(a,1),37(a,1,1)),rewrite(40(3),40(5))]. given #37 (T,wt=23): 203 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(193(a,1),2(a,1,2,2,1,1,1)),rewrite(193(6))]. given #38 (T,wt=23): 231 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(x,z)))) = x. [para(205(a,1),2(a,1,2,2,1,1,1)),rewrite(205(6))]. given #39 (A,wt=37): 15 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(11(a,1),2(a,1,2,2,1,1,1,1))]. given #40 (T,wt=23): 243 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))),x) = f(x,x). [para(11(a,1),174(a,1,1,1,1)),rewrite(40(5),40(11))]. given #41 (T,wt=23): 270 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [para(11(a,1),175(a,1,1)),rewrite(40(3),40(5))]. given #42 (T,wt=23): 302 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x). [para(11(a,1),246(a,1,1,1,1)),rewrite(40(5),40(11))]. given #43 (T,wt=23): 308 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(55(a,1),203(a,1,2,2,2))]. given #44 (A,wt=25): 16 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y. [para(11(a,1),2(a,1,2,2,1,1,1))]. given #45 (T,wt=17): 344 f(f(x,x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(55(a,1),308(a,1,2))]. given #46 (T,wt=17): 369 f(f(x,x),f(f(x,f(x,f(y,f(x,x)))),x)) = x. [para(55(a,1),344(a,1,2,1,2,2))]. given #47 (T,wt=19): 364 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(246(a,1),16(a,1,2,2,1)),rewrite(11(4),40(3),55(6))]. given #48 (T,wt=19): 365 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(302(a,1),16(a,1,2,2,1)),rewrite(20(3),55(8))]. given #49 (A,wt=29): 23 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,f(z,f(x,x))),y),y),x),f(x,u)))) = x. [para(20(a,1),2(a,1,1))]. given #50 (T,wt=19): 387 f(f(f(f(x,x),x),f(x,f(f(x,x),y))),x) = f(x,x). [para(364(a,1),55(a,1,2,1)),rewrite(364(14),40(9),364(14))]. given #51 (T,wt=19): 388 f(x,f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(55(a,1),364(a,1,2,2,2))]. given #52 (T,wt=19): 401 f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)) = x. [para(365(a,1),55(a,1,2,1)),rewrite(365(14),365(16))]. given #53 (T,wt=19): 402 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(55(a,1),365(a,1,2,2,2))]. given #54 (A,wt=49): 24 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),z),f(f(f(f(f(x,x),z),z),f(y,f(x,x))),f(f(y,f(x,x)),u)))) = f(y,f(x,x)). [para(20(a,1),2(a,1,2,2,1,1,1,1))]. given #55 (T,wt=19): 414 f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x) = f(x,x). [para(55(a,1),387(a,1,1,2,2))]. given #56 (T,wt=19): 427 f(f(f(x,f(x,x)),f(f(x,x),f(y,x))),f(x,x)) = x. [para(55(a,1),401(a,1,1,2,2))]. given #57 (T,wt=21): 351 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(x,y)))) = x. [para(32(a,1),16(a,1,2,2,1)),rewrite(40(6))]. given #58 (T,wt=19): 442 f(f(f(f(x,x),x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(351(a,1),55(a,1,2,1)),rewrite(351(15),351(17))]. given #59 (A,wt=25): 25 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(f(x,x),x),y),f(y,z)))) = y. [para(20(a,1),2(a,1,2,2,1,1,1))]. given #60 (T,wt=19): 451 f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),x) = f(x,x). [para(11(a,1),442(a,1,1,1,1)),rewrite(40(5),40(9))]. given #61 (T,wt=19): 454 f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(55(a,1),442(a,1,1,2,2))]. given #62 (T,wt=19): 471 f(f(f(x,f(x,x)),f(x,f(y,f(x,x)))),x) = f(x,x). [para(55(a,1),451(a,1,1,2,2))]. given #63 (T,wt=21): 368 f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x))) = f(x,x). [para(11(a,1),344(a,1,1)),rewrite(40(5))]. given #64 (A,wt=29): 35 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,f(f(x,x),z)),y),y),x),f(x,u)))) = x. [para(32(a,1),2(a,1,1))]. given #65 (T,wt=21): 377 f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x))) = f(x,x). [para(11(a,1),369(a,1,1)),rewrite(40(5))]. given #66 (T,wt=21): 443 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(y,x)))) = x. [para(55(a,1),351(a,1,2,2,2))]. given #67 (T,wt=21): 473 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y))))) = x. [para(451(a,1),195(a,1,1)),rewrite(451(8),451(9),40(4),451(16),451(17),40(12))]. given #68 (T,wt=21): 483 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(y,f(x,x)))))) = x. [para(471(a,1),195(a,1,1)),rewrite(471(8),471(9),40(4),471(16),471(17),40(12))]. given #69 (A,wt=49): 36 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),z),f(f(f(f(f(x,x),z),z),f(f(x,x),y)),f(f(f(x,x),y),u)))) = f(f(x,x),y). [para(32(a,1),2(a,1,2,2,1,1,1,1))]. given #70 (F,wt=45): 529 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),z),f(f(f(f(f(x,x),z),z),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y) # label(false). [para(32(a,1),36(a,1,2,2,2))]. given #71 (F,wt=27): 546 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(535),rewrite(543(3))]. given #72 (F,wt=25): 579 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))) = y # label(false). [para(2(a,1),546(a,1,2,1,1,1)),rewrite(2(12),2(17),2(22))]. given #73 (F,wt=25): 587 f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))) = x # label(false). [para(40(a,1),546(a,1,2,1,1,1)),rewrite(40(4),40(9),40(14))]. given #74 (T,wt=9): 543 f(f(x,x),f(x,y)) = x. [para(387(a,1),529(a,1,2,2)),rewrite(40(4),182(4),40(5),40(8),40(13),20(11),40(3),40(4)),flip(a)]. given #75 (T,wt=9): 544 f(f(x,x),f(y,x)) = x. [para(414(a,1),529(a,1,2,2)),rewrite(543(4),196(4),543(5),543(8),543(13),20(11),543(3),543(4)),flip(a)]. given #76 (T,wt=11): 604 f(x,f(f(x,x),y)) = f(x,x). [para(387(a,1),546(a,1,2,2)),rewrite(11(10)),flip(a)]. given #77 (T,wt=11): 607 f(x,f(y,f(x,x))) = f(x,x). [para(414(a,1),546(a,1,2,2)),rewrite(11(10)),flip(a)]. given #78 (A,wt=49): 39 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),y),f(f(f(y,y),y),f(y,z)))),f(f(f(y,y),y),f(f(f(y,y),y),f(y,z)))),y),f(y,u)))) = y. [para(32(a,1),4(a,1,2,2,1,1,1,2,2,1,1)),rewrite(32(15))]. given #79 (F,wt=27): 576 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(127),rewrite(544(3))]. given #80 (F,wt=33): 582 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(x,f(y,y)),z),z),f(y,y)),f(x,f(y,y))))) = f(y,y) # label(false). [para(20(a,1),546(a,1,2,1,1,1)),rewrite(20(6),543(5),20(10),20(17))]. given #81 (F,wt=57): 635 f(f(x,y),f(f(f(y,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))) = y # label(false). [para(579(a,1),579(a,1,2,2,1,1,1))]. given #82 (F,wt=57): 655 f(f(x,y),f(f(f(x,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))) = x # label(false). [para(587(a,1),587(a,1,2,2,1,1,1))]. given #83 (T,wt=13): 657 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(2(a,1),543(a,1,2))]. given #84 (T,wt=13): 662 f(f(f(x,y),f(x,y)),x) = f(x,y). [para(40(a,1),543(a,1,2))]. given #85 (T,wt=19): 613 f(x,f(f(x,f(x,x)),f(f(x,x),x))) = f(x,f(x,x)). [back_rewrite(598),rewrite(607(5))]. given #86 (T,wt=21): 594 f(f(x,x),f(f(f(x,x),x),f(x,f(x,x)))) = f(f(x,x),x). [para(234(a,1),546(a,1,2,1)),rewrite(32(6),544(7))]. given #87 (A,wt=49): 41 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),x))) = f(z,x). [para(2(a,1),5(a,1,2,2,2))]. given #88 (F,wt=35): 771 f(f(x,y),f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))) = y # label(false). [para(657(a,1),635(a,1,1)),rewrite(657(8),657(12),767(12),657(7),657(11),657(16))]. given #89 (F,wt=35): 774 f(f(x,y),f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))) = x # label(false). [para(655(a,1),657(a,2)),rewrite(753(12),753(28),753(44),657(48))]. given #90 (F,wt=41): 825 f(x,f(f(x,y),f(f(f(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)),x))) = f(x,y) # label(false). [para(543(a,1),771(a,1,1)),rewrite(543(9),543(13),543(18))]. given #91 (F,wt=41): 826 f(x,f(f(y,x),f(f(f(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)),x))) = f(y,x) # label(false). [para(544(a,1),771(a,1,1)),rewrite(544(9),544(13),544(18))]. given #92 (T,wt=21): 764 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,y)),x))) = f(x,y). [para(657(a,1),546(a,1,2,1))]. given #93 (T,wt=21): 768 f(x,f(f(y,x),f(f(f(f(x,x),x),f(y,x)),x))) = f(y,x). [para(657(a,1),576(a,1,2,1))]. given #94 (T,wt=21): 785 f(x,f(f(x,y),f(f(f(f(x,x),x),f(x,y)),x))) = f(x,y). [para(662(a,1),546(a,1,2,1))]. given #95 (T,wt=21): 787 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),x))) = f(y,x). [para(662(a,1),576(a,1,2,1))]. given #96 (A,wt=53): 43 f(f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),v)))) = f(y,x). [para(11(a,1),5(a,1,1,1,2,1,1,1))]. given #97 (F,wt=45): 824 f(f(x,y),f(y,f(f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))),y),f(x,y)))) = y # label(false). [para(771(a,1),579(a,1,2,2,1,1,1)),rewrite(543(17))]. given #98 (F,wt=45): 877 f(f(x,y),f(x,f(f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x),f(x,y)))) = x # label(false). [para(774(a,1),764(a,1,2,1)),rewrite(774(17),774(32),774(37))]. given #99 (F,wt=51): 813 f(f(x,f(y,y)),f(f(y,y),f(f(f(f(y,y),f(f(y,z),f(f(f(f(f(x,f(y,y)),z),z),f(y,y)),f(x,f(y,y))))),f(y,y)),f(x,f(y,y))))) = f(y,y) # label(false). [para(11(a,1),771(a,1,2,2,1,1,2,1,1))]. given #100 (F,wt=51): 833 f(f(f(x,x),y),f(f(x,x),f(f(f(f(x,x),f(f(x,z),f(f(f(f(f(f(x,x),y),z),z),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),y)))) = f(x,x) # label(false). [para(11(a,1),774(a,1,2,2,1,1,2,1,1))]. given #101 (T,wt=23): 459 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))),f(x,x)) = x. [para(25(a,1),55(a,1,2,1)),rewrite(25(19),25(21))]. given #102 (T,wt=23): 763 f(f(x,x),f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z)))) = x. [para(25(a,1),657(a,1,1,1)),rewrite(25(11),25(21))]. given #103 (T,wt=23): 940 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x))),f(x,x)) = x. [para(55(a,1),459(a,1,1,2,2))]. given #104 (T,wt=23): 949 f(f(x,x),f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x)))) = x. [para(55(a,1),763(a,1,2,2,2))]. given #105 (A,wt=25): 50 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(32(a,1),5(a,1,1)),rewrite(40(3),40(3))]. given #106 (F,wt=55): 831 f(f(x,y),f(y,f(f(f(y,f(y,f(f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))),y),f(x,y)))),y),f(x,y)))) = y # label(false). [para(771(a,1),771(a,1,2,2,1,1,2,2,1,1,1)),rewrite(543(17))]. given #107 (F,wt=55): 845 f(f(x,y),f(x,f(f(f(x,f(x,f(f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x),f(x,y)))),x),f(x,y)))) = x # label(false). [para(774(a,1),774(a,1,2,2,1,1,2,2,1,1,1)),rewrite(543(17))]. given #108 (F,wt=55): 878 f(x,f(f(x,y),f(f(f(f(x,y),f(f(x,y),f(f(f(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)),x))),f(x,y)),x))) = f(x,y) # label(false). [para(825(a,1),764(a,1,2,1)),rewrite(825(19),825(38),825(43))]. Demod_limit: f(f(f(f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x)))),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(x,x)),f(f(f(x,f(x,x)),y),f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x)))),u))),f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x)))))),f(f(f(f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x)))))),v),f(f(f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x)))),v),v),f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x)))))),f(f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),w)))) = f(x,f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y)),z),f(f(f(f(f(x,f(x,x)),z),z),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))),f(f(x,f(x,x)),y)),f(x,f(x,x))))). [para(878(a,1),43(a,1,1,1,2,1))]. Demod_limit (steps=-1, size=1053). The most recent kept clause is 995. From here on, a short message will be printed for each 100 times the limit is hit. given #109 (F,wt=55): 879 f(x,f(f(y,x),f(f(f(f(y,x),f(f(y,x),f(f(f(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)),x))),f(y,x)),x))) = f(y,x) # label(false). [para(826(a,1),764(a,1,2,1)),rewrite(826(19),826(38),826(43))]. given #110 (T,wt=25): 66 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y. [para(55(a,1),2(a,1,2,2,2))]. given #111 (T,wt=25): 67 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = x. [para(2(a,1),55(a,1,2,1)),rewrite(2(20),2(22))]. given #112 (T,wt=25): 356 f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [para(16(a,1),55(a,1,2,1)),rewrite(16(20),16(22))]. given #113 (T,wt=25): 358 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(z,y)))) = y. [para(55(a,1),16(a,1,2,2,2))]. given #114 (A,wt=27): 53 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y. [para(40(a,1),2(a,1,2,2,1,1))]. given #115 (T,wt=25): 461 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(55(a,1),25(a,1,2,2,2))]. given #116 (T,wt=25): 568 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(z,f(x,x))))) = f(x,x). [back_rewrite(255),rewrite(544(4))]. given #117 (T,wt=25): 573 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x). [back_rewrite(157),rewrite(544(3))]. given #118 (T,wt=25): 589 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),x))) = f(x,y). [para(40(a,1),546(a,1,2,2,1,1))]. given #119 (A,wt=35): 54 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),y))) = f(y,z). [para(40(a,1),2(a,1,2,2,2))]. given #120 (T,wt=25): 599 f(f(x,y),f(f(f(f(f(f(x,x),x),y),y),f(x,x)),f(f(x,x),z))) = x. [para(13(a,1),546(a,1,2,2,1)),rewrite(40(6),40(17),543(29),20(27),40(3),40(5)),flip(a)]. given #121 (T,wt=25): 609 f(f(x,x),f(f(f(x,x),x),f(x,f(f(f(x,x),x),y)))) = f(f(x,x),x). [back_rewrite(555),rewrite(604(3))]. given #122 (T,wt=25): 621 f(f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(z,x))),f(x,x)) = x. [para(579(a,1),55(a,1,2,1)),rewrite(579(20),579(22))]. given #123 (T,wt=25): 640 f(f(x,y),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,y)))) = x. [para(11(a,1),587(a,1,2,2,1,1,1))]. given #124 (A,wt=55): 57 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),v)))) = f(y,x). [para(40(a,1),5(a,1,1,1,2,1,1))]. given #125 (F,wt=49): 1278 f(f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,y))),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(640(a,1),54(a,1,2,2,1,1,1,1))]. given #126 (F,wt=49): 1293 f(f(f(x,f(f(f(f(f(y,x),f(y,x)),f(y,x)),x),f(y,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(55(a,1),1278(a,1,1,1,2,2)),rewrite(543(8),544(3),543(10),55(13),55(15),55(16),55(21),55(26))]. given #127 (F,wt=49): 1294 f(f(f(x,f(f(f(f(f(x,y),f(x,y)),f(x,y)),x),f(x,y))),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(61(a,1),1278(a,1,1,1,2,2)),rewrite(543(8),543(3),543(10),61(13),61(15),61(16),61(21),61(26))]. given #128 (F,wt=53): 1291 f(f(f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,f(y,y))),f(y,y))),f(y,y)),f(f(y,z),f(f(f(f(f(x,f(y,y)),z),z),f(y,y)),f(x,f(y,y))))) = f(y,y) # label(false). [para(20(a,1),1278(a,1,1,1,2,2)),rewrite(657(7),20(13),20(15),20(16),543(15),20(20),20(27))]. given #129 (T,wt=25): 656 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(y,u)))) = y. [para(543(a,1),2(a,1,2,1))]. given #130 (T,wt=19): 1330 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y. [para(607(a,1),656(a,1,2,2)),rewrite(55(15))]. given #131 (T,wt=15): 1383 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y). [para(582(a,1),1330(a,1,2,1,1)),rewrite(543(3),40(5),40(9),20(7),40(4))]. given #132 (T,wt=15): 1427 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x). [para(55(a,1),1383(a,1,2,2)),rewrite(55(9))]. given #133 (A,wt=51): 59 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),f(x,x)),f(f(x,f(z,x)),f(f(z,x),v)))) = f(z,x). [para(40(a,1),5(a,1,2,2,1,1))]. given #134 (F,wt=39): 1388 f(f(x,y),f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y),f(y,x)))),y)) = y # label(false). [para(774(a,1),1330(a,1,2,1,1))]. given #135 (F,wt=39): 1516 f(f(x,y),f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))),y)) = y # label(false). [para(55(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(657(4),55(11),55(16))]. given #136 (F,wt=39): 1519 f(f(x,y),f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)) = x # label(false). [para(61(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(662(4),61(11),61(16))]. given #137 (F,wt=47): 1543 f(f(f(f(f(x,x),x),f(x,y)),x),f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)) = x # label(false). [para(1383(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(1383(16),1383(21))]. given #138 (T,wt=19): 1368 f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y. [para(55(a,1),1330(a,1,2,1,1,1)),rewrite(657(4))]. given #139 (T,wt=19): 1369 f(f(x,y),f(f(f(f(y,x),f(z,y)),f(z,y)),y)) = y. [para(55(a,1),1330(a,1,2,1,1,2)),rewrite(55(8))]. given #140 (T,wt=19): 1370 f(f(x,y),f(f(f(f(x,y),f(x,z)),f(x,z)),x)) = x. [para(61(a,1),1330(a,1,2,1,1,1)),rewrite(662(4))]. given #141 (T,wt=19): 1378 f(f(f(f(x,f(x,x)),f(x,y)),f(x,y)),x) = f(x,x). [para(1330(a,1),25(a,1,2,2,1)),rewrite(544(9),657(16),1212(18)),flip(a)]. given #142 (A,wt=49): 60 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),z))) = f(z,x). [para(40(a,1),5(a,1,2,2,2))]. given #143 (F,wt=43): 1703 f(f(x,y),f(f(y,f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y),f(y,x)))),y)),y)) = y # label(false). [para(1519(a,1),1369(a,1,2,1,1))]. given #144 (F,wt=43): 1772 f(f(x,y),f(f(y,f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))),y)),y)) = y # label(false). [para(55(a,1),1703(a,1,2,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(657(4),55(11),55(16))]. given #145 (F,wt=43): 1773 f(f(x,y),f(f(x,f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)),x)) = x # label(false). [para(61(a,1),1703(a,1,2,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(662(4),61(11),61(16))]. given #146 (F,wt=47): 1545 f(f(f(f(f(x,x),x),f(y,x)),x),f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x),f(y,x)))),x)) = x # label(false). [para(1427(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(1427(16),1427(21))]. given #147 (T,wt=19): 1455 f(f(x,x),f(f(f(x,x),x),f(x,y))) = f(f(x,x),x). [para(1383(a,1),609(a,1,2,2))]. given #148 (T,wt=19): 1614 f(f(x,y),f(f(f(f(x,y),f(z,y)),f(z,y)),y)) = y. [para(55(a,1),1368(a,1,2,1,1,2)),rewrite(55(8))]. given #149 (T,wt=19): 1620 f(f(f(f(f(x,x),x),f(x,y)),f(x,y)),x) = f(x,x). [para(1368(a,1),576(a,1,2,2,1)),rewrite(657(16),11(9)),flip(a)]. given #150 (T,wt=19): 1649 f(f(x,y),f(f(f(f(x,y),f(z,x)),f(z,x)),x)) = x. [para(61(a,1),1369(a,1,2,1,1,1)),rewrite(662(4))]. given #151 (A,wt=45): 63 f(f(x,y),f(f(z,f(y,y)),f(f(f(f(f(y,x),f(f(z,f(y,y)),f(z,f(y,y)))),f(f(z,f(y,y)),f(z,f(y,y)))),y),f(y,u)))) = y. [para(55(a,1),2(a,1,2,1))]. given #152 (F,wt=47): 1813 f(f(x,y),f(f(y,f(f(y,f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y),f(y,x)))),y)),y)),y)) = y # label(false). [para(1773(a,1),1369(a,1,2,1,1))]. given #153 (F,wt=47): 1895 f(f(x,y),f(f(y,f(f(y,f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))),y)),y)),y)) = y # label(false). [para(1772(a,1),1614(a,1,2,1,1))]. given #154 (F,wt=47): 1940 f(f(x,y),f(f(x,f(f(x,f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)),x)),x)) = x # label(false). [para(1773(a,1),1649(a,1,2,1,1))]. given #155 (F,wt=49): 1397 f(f(x,y),f(f(y,f(y,f(f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y),f(y,x)))),y),f(y,x)))),y)) = y # label(false). [para(877(a,1),1330(a,1,2,1,1))]. given #156 (T,wt=19): 1655 f(f(f(f(x,f(x,x)),f(y,x)),f(y,x)),x) = f(x,x). [para(1369(a,1),25(a,1,2,2,1)),rewrite(544(9),657(16),1213(18)),flip(a)]. given #157 (T,wt=19): 1745 f(x,f(f(f(x,f(x,x)),f(x,y)),f(x,y))) = f(x,x). [para(1378(a,1),662(a,1,1,1)),rewrite(1378(8),543(3),1378(14))]. given #158 (T,wt=19): 1832 f(x,f(f(x,f(x,x)),f(f(x,x),y))) = f(x,f(x,x)). [para(11(a,1),1455(a,1,1)),rewrite(543(3),543(9))]. given #159 (T,wt=19): 1836 f(f(x,x),f(f(f(x,x),x),f(y,x))) = f(f(x,x),x). [para(55(a,1),1455(a,1,2,2))]. given #160 (A,wt=45): 65 f(f(x,y),f(f(f(y,y),f(f(z,f(y,x)),f(z,f(y,x)))),f(f(f(f(z,f(y,x)),f(f(z,f(y,x)),f(z,f(y,x)))),y),f(y,u)))) = y. [para(55(a,1),2(a,1,2,2,1,1,1))]. given #161 (F,wt=49): 1510 f(x,f(f(f(y,x),f(f(y,x),f(f(f(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)),x))),f(y,x))) = f(y,x) # label(false). [para(11(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(544(3),11(14),11(19))]. given #162 (F,wt=49): 1513 f(x,f(f(f(x,y),f(f(x,y),f(f(f(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)),x))),f(x,y))) = f(x,y) # label(false). [para(40(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(543(3),40(14),40(19))]. given #163 (F,wt=49): 1566 f(f(x,y),f(y,f(f(f(y,f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))),y)),y),f(x,y)))) = y # label(false). [para(1516(a,1),764(a,1,2,1)),rewrite(1516(19),1516(36),1516(41))]. given #164 (F,wt=49): 1594 f(f(x,y),f(x,f(f(f(x,f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)),x),f(x,y)))) = x # label(false). [para(1519(a,1),764(a,1,2,1)),rewrite(1519(19),1519(36),1519(41))]. given #165 (T,wt=19): 1870 f(f(f(f(f(x,x),x),f(y,x)),f(y,x)),x) = f(x,x). [para(1614(a,1),576(a,1,2,2,1)),rewrite(657(16),11(9)),flip(a)]. given #166 (T,wt=19): 1904 f(x,f(f(f(f(x,x),x),f(x,y)),f(x,y))) = f(x,x). [para(1620(a,1),662(a,1,1,1)),rewrite(1620(8),543(3),1620(14))]. given #167 (T,wt=19): 2012 f(x,f(f(f(x,f(x,x)),f(y,x)),f(y,x))) = f(x,x). [para(1655(a,1),662(a,1,1,1)),rewrite(1655(8),543(3),1655(14))]. given #168 (T,wt=19): 2026 f(x,f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). [para(55(a,1),1832(a,1,2,2))]. given #169 (A,wt=57): 68 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),y),f(y,v)))) = y. [para(55(a,1),4(a,1,2,2,1,1,1,2,2,2)),rewrite(55(22))]. given #170 (F,wt=49): 1626 f(f(x,y),f(f(y,f(y,f(f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))),y),f(x,y)))),y)) = y # label(false). [para(824(a,1),1368(a,1,2,1,1))]. given #171 (F,wt=49): 1720 f(f(x,y),f(f(x,f(x,f(f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x),f(x,y)))),x)) = x # label(false). [para(877(a,1),1370(a,1,2,1,1))]. given #172 (F,wt=51): 1783 f(f(f(f(f(x,x),x),f(x,y)),x),f(f(x,f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)),x)) = x # label(false). [para(1383(a,1),1703(a,1,2,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(1383(16),1383(21))]. given #173 (F,wt=51): 1784 f(f(f(f(f(x,x),x),f(y,x)),x),f(f(x,f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x),f(y,x)))),x)),x)) = x # label(false). [para(1427(a,1),1703(a,1,2,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(1427(16),1427(21))]. given #174 (T,wt=19): 2132 f(x,f(f(f(f(x,x),x),f(y,x)),f(y,x))) = f(x,x). [para(1870(a,1),662(a,1,1,1)),rewrite(1870(8),543(3),1870(14))]. given #175 (T,wt=21): 1426 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y). [para(11(a,1),1383(a,1,2,1,1))]. given #176 (T,wt=21): 1464 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)). [para(11(a,1),1427(a,1,2,1,1))]. given #177 (T,wt=23): 1360 f(f(x,f(y,z)),f(f(f(f(f(y,z),x),z),z),f(y,z))) = f(y,z). [para(2(a,1),1330(a,1,2,1,1,2)),rewrite(2(16))]. given #178 (A,wt=57): 69 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(v,y)))) = y. [para(55(a,1),4(a,1,2,2,2))]. given #179 (F,wt=51): 1965 f(f(x,y),f(f(y,f(f(y,f(f(y,f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y),f(y,x)))),y)),y)),y)),y)) = y # label(false). [para(1813(a,1),1614(a,1,2,1,1))]. given #180 (F,wt=51): 1982 f(f(x,y),f(f(y,f(f(y,f(f(y,f(f(y,f(y,f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y),f(x,y)))),y)),y)),y)),y)) = y # label(false). [para(1895(a,1),1614(a,1,2,1,1))]. given #181 (F,wt=51): 1995 f(f(x,y),f(f(x,f(f(x,f(f(x,f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)),x)),x)),x)) = x # label(false). [para(1940(a,1),1649(a,1,2,1,1))]. given #182 (F,wt=53): 1532 f(f(f(f(x,y),f(f(f(f(x,y),y),f(x,y)),x)),x),f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)) = x # label(false). [para(764(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(764(22),764(27))]. given #183 (T,wt=15): 2257 f(x,f(f(f(x,y),y),f(x,y))) = f(x,y). [para(40(a,1),1360(a,1,2,1,1,1)),rewrite(543(3))]. given #184 (T,wt=23): 1362 f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x). [para(11(a,1),1330(a,1,2,1,1,1)),rewrite(544(3))]. given #185 (T,wt=15): 2487 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x). [para(40(a,1),1362(a,1,2,1,1,2)),rewrite(40(4))]. given #186 (T,wt=11): 2546 f(f(x,x),x) = f(x,f(x,x)). [para(32(a,1),2487(a,1,2,1)),rewrite(543(5))]. given #187 (A,wt=53): 70 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x))),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(55(a,1),5(a,1,1,1,2,2))]. given #188 (F,wt=35): 2409 f(x,f(f(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))) = f(x,y) # label(false). [para(546(a,1),2257(a,1,2,1,1)),rewrite(546(23),546(26))]. given #189 (F,wt=29): 3233 f(f(x,y),f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)) = y # label(false). [para(2(a,1),2409(a,1,2,1,1)),rewrite(2(12),2(12),2(17),2(22),2(24))]. given #190 (F,wt=29): 3237 f(f(x,y),f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)) = x # label(false). [para(40(a,1),2409(a,1,2,1,1)),rewrite(40(4),40(4),40(9),40(14),40(16))]. given #191 (F,wt=33): 3308 f(f(x,y),f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)) = y # label(false). [para(3233(a,1),1614(a,1,2,1,1))]. given #192 (T,wt=15): 2615 f(x,f(f(x,f(x,x)),f(y,x))) = f(y,x). [para(2487(a,1),1383(a,1,2,2)),rewrite(2546(2),2487(10))]. given #193 (T,wt=15): 2617 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y). [para(1383(a,1),2487(a,1,2,2)),rewrite(2546(2),2546(6),1613(13),2546(3)),flip(a)]. given #194 (T,wt=19): 2629 f(f(x,x),f(f(x,f(x,x)),f(y,x))) = f(x,f(x,x)). [para(2487(a,1),1455(a,1,2,2)),rewrite(2546(3),2546(8))]. given #195 (T,wt=19): 2631 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)). [para(1455(a,1),2487(a,1,2,2)),rewrite(2546(2),2546(6),2546(14),1708(16),2546(5)),flip(a)]. given #196 (A,wt=53): 71 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(w,f(z,x))))) = f(z,x). [para(55(a,1),5(a,1,2,2,2))]. given #197 (F,wt=33): 3363 f(f(x,y),f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y)),y)) = y # label(false). [para(3237(a,1),1369(a,1,2,1,1))]. given #198 (F,wt=33): 3370 f(f(x,y),f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)) = x # label(false). [para(3237(a,1),1649(a,1,2,1,1))]. given #199 (F,wt=35): 2412 f(x,f(f(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))) = f(y,x) # label(false). [para(576(a,1),2257(a,1,2,1,1)),rewrite(576(23),576(26))]. given #200 (F,wt=37): 3424 f(f(x,y),f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)),y)) = y # label(false). [para(3308(a,1),1614(a,1,2,1,1))]. given #201 (T,wt=19): 3170 f(f(x,y),f(f(f(y,x),f(f(y,x),f(y,x))),y)) = y. [para(2546(a,1),1330(a,1,2,1))]. given #202 (T,wt=19): 3179 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = x. [para(2546(a,1),1370(a,1,2,1))]. given #203 (T,wt=19): 3189 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),y)) = y. [para(2546(a,1),1614(a,1,2,1))]. given #204 (T,wt=21): 2548 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = x. [para(2487(a,1),37(a,1,2,2,2)),rewrite(2546(3),2546(5))]. given #205 (A,wt=37): 72 f(f(f(f(f(x,y),f(x,y)),z),f(f(f(f(y,z),z),f(x,y)),f(f(x,y),u))),f(f(x,y),f(x,y))) = f(x,y). [para(5(a,1),55(a,1,2,1)),rewrite(5(37),5(40))]. given #206 (F,wt=37): 3502 f(f(x,y),f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y)),y)),y)) = y # label(false). [para(3363(a,1),1614(a,1,2,1,1))]. given #207 (F,wt=37): 3562 f(f(x,y),f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)),x)) = x # label(false). [para(3370(a,1),1649(a,1,2,1,1))]. given #208 (F,wt=39): 3284 f(f(x,y),f(y,f(f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y),f(x,y)))) = y # label(false). [para(3233(a,1),764(a,1,2,1)),rewrite(3233(14),3233(26),3233(31))]. given #209 (F,wt=39): 3348 f(f(x,y),f(x,f(f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x),f(x,y)))) = x # label(false). [para(3237(a,1),764(a,1,2,1)),rewrite(3237(14),3237(26),3237(31))]. given #210 (T,wt=21): 2550 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(x,x)) = x. [para(2487(a,1),174(a,1,1,2,2)),rewrite(2546(2),2546(4))]. given #211 (T,wt=21): 2551 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = x. [para(174(a,1),2487(a,1,2,2)),rewrite(2546(4),2546(6),2546(12),2546(14),544(20),2546(2),2546(4),2549(9)),flip(a)]. given #212 (T,wt=21): 2575 f(x,f(f(y,x),f(f(f(x,f(x,x)),f(y,x)),x))) = f(y,x). [para(768(a,1),2487(a,1,2,2)),rewrite(2546(3),2546(10),1708(19),2546(4)),flip(a)]. given #213 (T,wt=21): 2577 f(x,f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),x))) = f(x,y). [para(785(a,1),2487(a,1,2,2)),rewrite(2546(3),2546(10),1711(19),2546(4)),flip(a)]. given #214 (A,wt=45): 74 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(y,y),z))),f(f(f(y,y),z),f(f(y,y),z))),y),f(y,u)))) = y. [para(61(a,1),2(a,1,2,1))]. given #215 (F,wt=41): 2414 f(f(x,f(y,y)),f(f(f(y,y),f(f(y,z),f(f(f(f(f(x,f(y,y)),z),z),f(y,y)),f(x,f(y,y))))),f(y,y))) = f(y,y) # label(false). [para(582(a,1),2257(a,1,2,1,1)),rewrite(582(29),582(32))]. given #216 (F,wt=41): 3235 f(f(f(x,x),y),f(f(f(x,x),f(f(x,z),f(f(f(f(f(f(x,x),y),z),z),f(x,x)),f(f(x,x),y)))),f(x,x))) = f(x,x) # label(false). [para(32(a,1),2409(a,1,2,1,1)),rewrite(32(6),32(7),543(6),32(11),32(18),32(21))]. given #217 (F,wt=41): 3516 f(f(f(f(f(x,y),y),f(x,y)),x),f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)) = x # label(false). [para(2257(a,1),3363(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2257(16))]. given #218 (F,wt=41): 3520 f(f(f(f(f(x,y),y),f(y,x)),x),f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x)),x)) = x # label(false). [para(2487(a,1),3363(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2487(16))]. given #219 (T,wt=21): 3129 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x)) = x. [back_rewrite(2549),rewrite(2551(18))]. given #220 (T,wt=23): 1366 f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y). [para(40(a,1),1330(a,1,2,1,1,1)),rewrite(543(3))]. given #221 (T,wt=23): 1367 f(f(x,f(y,z)),f(f(f(f(f(y,z),x),y),y),f(y,z))) = f(y,z). [para(40(a,1),1330(a,1,2,1,1,2)),rewrite(40(8))]. given #222 (T,wt=23): 1611 f(f(x,f(y,z)),f(f(f(f(x,f(y,z)),z),z),f(y,z))) = f(y,z). [para(2(a,1),1368(a,1,2,1,1,2)),rewrite(2(16))]. given #223 (A,wt=45): 76 f(f(x,y),f(f(f(y,y),f(f(f(y,x),z),f(f(y,x),z))),f(f(f(f(f(y,x),z),f(f(f(y,x),z),f(f(y,x),z))),y),f(y,u)))) = y. [para(61(a,1),2(a,1,2,2,1,1,1))]. given #224 (F,wt=41): 3527 f(f(f(f(x,f(x,x)),f(y,x)),x),f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x)),x)) = x # label(false). [para(2615(a,1),3363(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2615(16))]. given #225 (F,wt=41): 3528 f(f(f(f(x,f(x,x)),f(x,y)),x),f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)) = x # label(false). [para(2617(a,1),3363(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2617(16))]. given #226 (F,wt=41): 3640 f(f(x,y),f(f(y,f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)),y)),y)) = y # label(false). [para(3424(a,1),1614(a,1,2,1,1))]. given #227 (F,wt=41): 3899 f(f(x,y),f(f(y,f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y)),y)),y)),y)) = y # label(false). [para(3502(a,1),1614(a,1,2,1,1))]. given #228 (T,wt=23): 1613 f(f(x,f(y,z)),f(f(f(f(x,f(y,z)),y),y),f(y,z))) = f(y,z). [para(40(a,1),1368(a,1,2,1,1,2)),rewrite(40(8))]. given #229 (T,wt=23): 1636 f(f(f(f(x,f(x,x)),f(f(x,x),y)),f(f(x,x),y)),f(x,x)) = x. [para(1368(a,1),640(a,1,2,2,1)),rewrite(20(11),657(24),20(23),543(14),20(12),543(3)),flip(a)]. given #230 (T,wt=23): 1646 f(x,f(f(f(x,f(y,f(z,x))),f(y,f(z,x))),f(z,x))) = f(z,x). [para(11(a,1),1369(a,1,2,1,1,1)),rewrite(544(3))]. given #231 (T,wt=23): 1648 f(x,f(f(f(x,f(y,f(x,z))),f(y,f(x,z))),f(x,z))) = f(x,z). [para(40(a,1),1369(a,1,2,1,1,1)),rewrite(543(3))]. given #232 (A,wt=57): 88 f(f(x,y),f(f(f(y,y),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z)))),f(f(f(x,f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z)))),y),f(y,u)))) = y. [para(11(a,1),6(a,1,2,1,2,2,1,1,1)),rewrite(11(18))]. given #233 (F,wt=41): 3948 f(f(x,y),f(f(x,f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)),x)),x)) = x # label(false). [para(3562(a,1),1649(a,1,2,1,1))]. given #234 (F,wt=43): 2408 f(x,f(f(f(f(x,y),f(x,y)),f(f(f(x,z),z),f(x,z))),f(f(f(f(x,z),f(f(f(x,z),z),f(x,z))),f(x,y)),x))) = f(x,y) # label(false). [para(2257(a,1),546(a,1,2,2,1,1,1))]. given #235 (F,wt=43): 2411 f(x,f(f(f(f(y,x),f(y,x)),f(f(f(x,z),z),f(x,z))),f(f(f(f(x,z),f(f(f(x,z),z),f(x,z))),f(y,x)),x))) = f(y,x) # label(false). [para(2257(a,1),576(a,1,2,2,1,1,1))]. given #236 (F,wt=43): 2557 f(x,f(f(f(f(x,y),f(x,y)),f(f(f(x,z),z),f(z,x))),f(f(f(f(z,x),f(f(f(x,z),z),f(z,x))),f(x,y)),x))) = f(x,y) # label(false). [para(2487(a,1),546(a,1,2,2,1,1,1))]. given #237 (T,wt=23): 1708 f(f(f(x,y),z),f(f(f(f(f(x,y),z),y),y),f(x,y))) = f(x,y). [para(2(a,1),1370(a,1,2,1,1,2)),rewrite(2(16))]. given #238 (T,wt=23): 1711 f(f(f(x,y),z),f(f(f(f(f(x,y),z),x),x),f(x,y))) = f(x,y). [para(40(a,1),1370(a,1,2,1,1,2)),rewrite(40(8))]. given #239 (T,wt=23): 1738 f(f(x,y),f(f(y,f(f(f(f(y,x),f(y,z)),f(y,z)),y)),y)) = y. [para(1370(a,1),1369(a,1,2,1,1))]. given #240 (T,wt=23): 1885 f(f(f(f(x,f(x,x)),f(y,f(x,x))),f(y,f(x,x))),f(x,x)) = x. [para(1614(a,1),640(a,1,2,2,1)),rewrite(20(11),657(24),20(23),543(14),20(12),543(3)),flip(a)]. given #241 (A,wt=57): 94 f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,v))),f(x,x)) = x. [para(6(a,1),55(a,1,2,1)),rewrite(6(52),6(54))]. given #242 (F,wt=43): 2563 f(x,f(f(f(f(y,x),f(y,x)),f(f(f(x,z),z),f(z,x))),f(f(f(f(z,x),f(f(f(x,z),z),f(z,x))),f(y,x)),x))) = f(y,x) # label(false). [para(2487(a,1),576(a,1,2,2,1,1,1))]. given #243 (F,wt=43): 3260 f(x,f(f(f(x,y),f(f(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))),f(x,y))) = f(x,y) # label(false). [para(2409(a,1),2257(a,1,2,1,1)),rewrite(2409(31),2409(34))]. given #244 (F,wt=43): 3328 f(f(x,y),f(f(y,f(y,f(f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y),f(x,y)))),y)) = y # label(false). [para(3233(a,1),3233(a,1,2,1,2,2,1,1,1)),rewrite(544(14))]. given #245 (F,wt=43): 3386 f(f(x,y),f(f(x,f(x,f(f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x),f(x,y)))),x)) = x # label(false). [para(3237(a,1),3237(a,1,2,1,2,2,1,1,1)),rewrite(544(14))]. given #246 (T,wt=23): 1891 f(f(x,y),f(f(y,f(f(f(f(x,y),f(y,z)),f(y,z)),y)),y)) = y. [para(1368(a,1),1614(a,1,2,1,1))]. given #247 (T,wt=23): 1893 f(f(x,y),f(f(y,f(f(f(f(y,x),f(z,y)),f(z,y)),y)),y)) = y. [para(1369(a,1),1614(a,1,2,1,1))]. given #248 (T,wt=23): 1897 f(f(x,y),f(f(y,f(f(f(f(x,y),f(z,y)),f(z,y)),y)),y)) = y. [para(1614(a,1),1614(a,1,2,1,1))]. given #249 (T,wt=23): 1936 f(f(x,y),f(f(x,f(f(f(f(x,y),f(x,z)),f(x,z)),x)),x)) = x. [para(1370(a,1),1649(a,1,2,1,1))]. given #250 (A,wt=57): 95 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(u,x)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))),y),f(y,v)))) = y. [para(55(a,1),6(a,1,2,1,2,2,2)),rewrite(55(22))]. given #251 (F,wt=43): 3401 f(x,f(f(f(y,x),f(f(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))),f(y,x))) = f(y,x) # label(false). [para(544(a,1),3308(a,1,1)),rewrite(544(9),544(13))]. given #252 (F,wt=43): 3408 f(f(x,y),f(y,f(f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)),y),f(x,y)))) = y # label(false). [para(3308(a,1),764(a,1,2,1)),rewrite(3308(16),3308(30),3308(35))]. given #253 (F,wt=43): 3548 f(f(x,y),f(x,f(f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)),x),f(x,y)))) = x # label(false). [para(3370(a,1),764(a,1,2,1)),rewrite(3370(16),3370(30),3370(35))]. given #254 (F,wt=43): 3658 f(f(f(f(f(x,y),f(f(x,y),f(x,y))),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(3170(a,1),7(a,1,2,2,1,1,1,1))]. given #255 (T,wt=23): 1941 f(f(x,y),f(f(x,f(f(f(f(x,y),f(z,x)),f(z,x)),x)),x)) = x. [para(1649(a,1),1649(a,1,2,1,1))]. given #256 (T,wt=23): 2139 f(f(x,x),f(f(f(x,f(x,x)),f(f(x,x),y)),f(f(x,x),y))) = x. [para(11(a,1),1904(a,1,2,1,1,1)),rewrite(543(13))]. given #257 (T,wt=23): 2209 f(f(x,x),f(f(f(x,f(x,x)),f(y,f(x,x))),f(y,f(x,x)))) = x. [para(11(a,1),2132(a,1,2,1,1,1)),rewrite(543(13))]. given #258 (T,wt=23): 2482 f(x,f(f(f(x,y),f(f(f(x,y),y),f(x,y))),f(x,y))) = f(x,y). [para(2257(a,1),2257(a,1,2,1,1)),rewrite(2257(11),2257(14))]. given #259 (A,wt=57): 96 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(v,y)))) = y. [para(55(a,1),6(a,1,2,2,2))]. given #260 (F,wt=43): 3751 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)),z),f(f(f(f(x,z),z),f(x,y)),x))) = f(x,y) # label(false). [para(3179(a,1),54(a,1,2,2,1,1,1,1))]. given #261 (F,wt=43): 3789 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)),z),f(f(f(f(y,z),z),f(x,y)),y))) = f(x,y) # label(false). [para(3189(a,1),7(a,1,2,2,1,1,1,1))]. given #262 (F,wt=43): 4025 f(f(x,y),f(f(y,f(y,f(f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y)),y),f(y,x)))),y)) = y # label(false). [para(3348(a,1),1330(a,1,2,1,1))]. given #263 (F,wt=45): 3907 f(f(f(f(f(x,y),y),f(x,y)),x),f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)),x)) = x # label(false). [para(2257(a,1),3502(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2257(16))]. given #264 (T,wt=23): 2581 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [para(2487(a,1),459(a,1,1,2,2)),rewrite(2546(4))]. given #265 (T,wt=23): 2582 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [para(459(a,1),2487(a,1,2,2)),rewrite(2546(6),2546(15),544(22),2546(4)),flip(a)]. given #266 (T,wt=23): 2584 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [para(2487(a,1),763(a,1,2,2,2)),rewrite(2546(5))]. given #267 (T,wt=23): 2585 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(763(a,1),2487(a,1,2,2)),rewrite(2546(4),2546(12),2582(18),20(11),2582(10),2546(5)),flip(a)]. given #268 (A,wt=41): 126 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 #269 (F,wt=45): 3909 f(f(f(f(f(x,y),y),f(y,x)),x),f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x)),x)),x)) = x # label(false). [para(2487(a,1),3502(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2487(16))]. given #270 (F,wt=45): 3915 f(f(f(f(x,f(x,x)),f(y,x)),x),f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x)),x)),x)) = x # label(false). [para(2615(a,1),3502(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2615(16))]. given #271 (F,wt=45): 3916 f(f(f(f(x,f(x,x)),f(x,y)),x),f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)),x)) = x # label(false). [para(2617(a,1),3502(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2617(16))]. given #272 (F,wt=45): 4407 f(f(x,y),f(f(y,f(f(y,f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)),y)),y)),y)) = y # label(false). [para(3640(a,1),1614(a,1,2,1,1))]. given #273 (T,wt=23): 2648 f(x,f(f(f(y,x),f(f(f(x,y),y),f(y,x))),f(y,x))) = f(y,x). [para(2487(a,1),2257(a,1,2,1,1)),rewrite(2487(11),2487(14))]. given #274 (T,wt=23): 2666 f(x,f(f(f(y,x),f(f(x,f(x,x)),f(y,x))),f(y,x))) = f(y,x). [back_rewrite(2460),rewrite(2546(3))]. given #275 (T,wt=23): 2667 f(x,f(f(f(x,y),f(f(x,f(x,x)),f(x,y))),f(x,y))) = f(x,y). [back_rewrite(2459),rewrite(2546(3))]. given #276 (T,wt=23): 3701 f(f(x,y),f(f(y,f(f(f(y,x),f(f(y,x),f(y,x))),y)),y)) = y. [para(3170(a,1),1614(a,1,2,1,1))]. given #277 (A,wt=33): 128 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(11(a,1),7(a,1,2,2,1,1,1))]. given #278 (F,wt=45): 4435 f(f(x,y),f(f(y,f(f(y,f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y)),y)),y)),y)),y)) = y # label(false). [para(3899(a,1),1614(a,1,2,1,1))]. given #279 (F,wt=45): 4597 f(f(x,y),f(f(x,f(f(x,f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)),x)),x)),x)) = x # label(false). [para(3948(a,1),1649(a,1,2,1,1))]. given #280 (F,wt=47): 2462 f(f(f(f(f(x,y),y),f(x,y)),x),f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)) = x # label(false). [para(2257(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(2257(16),2257(21))]. given #281 (F,wt=47): 2620 f(f(f(f(f(x,y),y),f(y,x)),x),f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x),f(y,x)))),x)) = x # label(false). [para(2487(a,1),1388(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(2487(16),2487(21))]. given #282 (T,wt=21): 5795 f(x,f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),y))) = f(x,y). [para(543(a,1),128(a,1,1)),rewrite(543(6),662(4),543(5),2546(3))]. given #283 (T,wt=23): 3764 f(f(x,y),f(f(x,f(f(f(x,y),f(f(x,y),f(x,y))),x)),x)) = x. [para(3179(a,1),1649(a,1,2,1,1))]. given #284 (T,wt=23): 3820 f(f(x,y),f(f(y,f(f(f(x,y),f(f(x,y),f(x,y))),y)),y)) = y. [para(3189(a,1),1614(a,1,2,1,1))]. given #285 (T,wt=25): 674 f(f(x,y),f(y,f(f(f(f(f(x,y),f(y,z)),f(y,z)),y),f(x,y)))) = y. [para(543(a,1),579(a,1,2,1))]. given #286 (A,wt=59): 135 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(5(a,1),7(a,1,1,2)),rewrite(5(26),5(27),5(30),5(34),5(51))]. given #287 (F,wt=47): 2621 f(f(f(f(x,f(x,x)),f(y,x)),x),f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x),f(y,x)))),x)) = x # label(false). [para(2487(a,1),1543(a,1,1,1,2)),rewrite(2546(2),2487(12),2487(16),2487(21))]. given #288 (F,wt=47): 2622 f(f(f(f(x,f(x,x)),f(x,y)),x),f(f(x,f(x,f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x),f(x,y)))),x)) = x # label(false). [para(1543(a,1),2487(a,1,2,2)),rewrite(2546(34),2546(40),1614(46),2546(2)),flip(a)]. given #289 (F,wt=47): 3439 f(f(x,y),f(f(y,f(y,f(f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)),y),f(x,y)))),y)) = y # label(false). [para(3308(a,1),3233(a,1,2,1,2,2,1,1,1)),rewrite(544(16))]. given #290 (F,wt=47): 3440 f(f(x,y),f(f(y,f(f(y,f(y,f(f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y),f(x,y)))),y)),y)) = y # label(false). [para(3233(a,1),3308(a,1,2,1,2,1,2,2,1,1,1)),rewrite(544(14))]. given #291 (T,wt=25): 679 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u)))) = y. [back_rewrite(64),rewrite(657(4))]. given #292 (T,wt=25): 691 f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x. [back_rewrite(75),rewrite(662(4))]. given #293 (T,wt=25): 692 f(f(x,y),f(y,f(f(f(f(f(y,x),f(z,y)),f(z,y)),y),f(y,u)))) = y. [para(544(a,1),2(a,1,2,1))]. given #294 (T,wt=25): 703 f(f(x,y),f(y,f(f(f(f(f(x,y),f(z,y)),f(z,y)),y),f(x,y)))) = y. [para(544(a,1),579(a,1,2,1))]. given #295 (A,wt=41): 137 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). [para(40(a,1),7(a,1,2,2,1,1))]. given #296 (F,wt=47): 3484 f(f(f(f(x,y),f(f(f(f(x,y),y),f(x,y)),x)),x),f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)) = x # label(false). [para(764(a,1),3363(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(764(22))]. given #297 (F,wt=47): 3485 f(f(f(f(x,y),f(f(f(f(y,x),x),f(x,y)),y)),y),f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)) = y # label(false). [para(787(a,1),3363(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(787(22))]. given #298 (F,wt=47): 3524 f(f(x,y),f(f(y,f(y,f(f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y)),y)),y),f(x,y)))),y)) = y # label(false). [para(3363(a,1),3233(a,1,2,1,2,2,1,1,1)),rewrite(544(16))]. given #299 (F,wt=47): 3525 f(f(x,y),f(f(y,f(f(y,f(y,f(f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y)),y),f(y,x)))),y)),y)) = y # label(false). [para(3237(a,1),3363(a,1,2,1,2,1,2,2,1,1,1)),rewrite(544(14))]. given #300 (T,wt=25): 753 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))) = x. [para(2(a,1),657(a,1,1,1)),rewrite(2(11),2(22))]. given #301 (T,wt=25): 762 f(f(x,x),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(16(a,1),657(a,1,1,1)),rewrite(16(11),16(22))]. given #302 (T,wt=25): 767 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(z,x)))) = x. [para(579(a,1),657(a,1,1,1)),rewrite(579(11),579(22))]. given #303 (T,wt=25): 954 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(11(a,1),940(a,1,1,2,1,1,1))]. given #304 (A,wt=37): 138 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),55(a,1,2,1)),rewrite(7(28),7(31))]. given #305 (F,wt=47): 3576 f(f(x,y),f(f(x,f(x,f(f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)),x),f(x,y)))),x)) = x # label(false). [para(3370(a,1),3237(a,1,2,1,2,2,1,1,1)),rewrite(544(16))]. given #306 (F,wt=47): 3577 f(f(x,y),f(f(x,f(f(x,f(x,f(f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x),f(x,y)))),x)),x)) = x # label(false). [para(3237(a,1),3370(a,1,2,1,2,1,2,2,1,1,1)),rewrite(544(14))]. given #307 (F,wt=47): 3629 f(f(x,y),f(y,f(f(f(y,f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)),y)),y),f(x,y)))) = y # label(false). [para(3424(a,1),764(a,1,2,1)),rewrite(3424(18),3424(34),3424(39))]. given #308 (F,wt=47): 4050 f(f(f(f(x,y),f(f(f(y,f(y,y)),f(x,y)),y)),y),f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(x,y)))),y)),y)) = y # label(false). [para(2575(a,1),3363(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2575(22))]. given #309 (T,wt=25): 963 f(f(x,x),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [para(11(a,1),949(a,1,2,2,1,1,1))]. given #310 (T,wt=25): 971 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(50(a,1),55(a,1,2,1)),rewrite(50(20),543(12),50(20))]. given #311 (T,wt=25): 1003 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(66(a,1),55(a,1,2,1)),rewrite(66(20),66(22))]. given #312 (T,wt=25): 1005 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(u,y)))) = y. [para(55(a,1),66(a,1,2,2,1,1,1,1)),rewrite(657(4))]. given #313 (A,wt=59): 152 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 #314 (F,wt=47): 4053 f(f(f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),x)),x),f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)) = x # label(false). [para(2577(a,1),3363(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2577(22))]. given #315 (F,wt=47): 5164 f(f(x,y),f(f(y,f(y,f(f(f(y,f(f(y,f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,x)))),y)),y)),y),f(y,x)))),y)) = y # label(false). [para(3548(a,1),1330(a,1,2,1,1))]. given #316 (F,wt=47): 5670 f(f(f(f(x,f(f(f(x,y),f(f(x,y),f(x,y))),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(3701(a,1),7(a,1,2,2,1,1,1,1))]. given #317 (F,wt=47): 5985 f(f(f(f(x,f(f(f(x,y),f(f(x,y),f(x,y))),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(3764(a,1),54(a,1,2,2,1,1,1,1))]. given #318 (T,wt=25): 1008 f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))) = x. [para(61(a,1),66(a,1,2,2,1,1,1,1)),rewrite(662(4))]. given #319 (T,wt=25): 1018 f(f(f(x,x),y),f(f(f(f(f(x,f(x,x)),y),y),x),f(z,x))) = f(x,x). [para(66(a,1),546(a,1,2,2,1)),rewrite(32(7),32(17),604(27),11(26),32(3),32(6)),flip(a)]. given #320 (T,wt=15): 7557 f(f(f(f(x,f(x,x)),y),y),x) = f(x,x). [para(1018(a,1),1885(a,1,1,1,2)),rewrite(7510(16),11(8),7510(13),32(3),7510(13),20(3)),flip(a)]. given #321 (T,wt=15): 7559 f(f(f(f(x,f(x,x)),y),y),f(x,x)) = x. [para(11(a,1),7557(a,1,1,1,1,2)),rewrite(2546(2),543(9))]. given #322 (A,wt=33): 158 f(f(f(f(f(x,y),f(x,y)),z),f(f(f(f(y,z),z),f(x,y)),y)),f(f(x,y),f(x,y))) = f(x,y). [para(127(a,1),55(a,1,2,1)),rewrite(127(25),127(28))]. given #323 (F,wt=47): 6031 f(f(f(f(x,f(f(f(y,x),f(f(y,x),f(y,x))),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(3820(a,1),7(a,1,2,2,1,1,1,1))]. given #324 (F,wt=49): 2413 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(x,f(y,y)),f(f(f(y,z),z),f(y,z))),f(f(f(y,z),z),f(y,z))),f(y,y)),f(x,f(y,y))))) = f(y,y) # label(false). [para(2257(a,1),582(a,1,2,1))]. given #325 (F,wt=49): 2565 f(f(x,f(y,y)),f(f(z,y),f(f(f(f(f(x,f(y,y)),f(f(f(y,z),z),f(z,y))),f(f(f(y,z),z),f(z,y))),f(y,y)),f(x,f(y,y))))) = f(y,y) # label(false). [para(2487(a,1),582(a,1,2,1))]. given #326 (F,wt=49): 2609 f(f(f(x,f(f(f(f(y,x),f(f(y,x),f(y,x))),x),f(y,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(1293(a,1),2487(a,2)),rewrite(2546(25),2546(37),2546(49),2487(68))]. given #327 (T,wt=11): 7716 f(x,f(x,f(x,y))) = f(x,y). [back_rewrite(4566),rewrite(7648(8))]. given #328 (T,wt=11): 7717 f(x,f(x,f(y,x))) = f(y,x). [back_rewrite(4530),rewrite(7648(8))]. given #329 (T,wt=11): 7848 f(f(x,y),f(f(x,y),y)) = y. [para(2(a,1),7716(a,1,2,2)),rewrite(2(15))]. given #330 (T,wt=11): 7850 f(f(x,y),f(f(x,y),x)) = x. [para(40(a,1),7716(a,1,2,2)),rewrite(40(7))]. given #331 (A,wt=55): 164 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)),z))))) = f(y,z). [para(127(a,1),7(a,1,1,2)),rewrite(127(16),127(17),127(20),127(24),127(39))]. given #332 (F,wt=35): 8188 f(f(f(f(x,y),y),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(y,z),z),f(x,y)),y))) = f(x,y) # label(false). [para(7848(a,1),7(a,1,2,2,1,1,1,1))]. given #333 (F,wt=35): 8351 f(f(f(f(x,y),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(7850(a,1),54(a,1,2,2,1,1,1,1))]. given #334 (F,wt=41): 7917 f(f(f(x,f(x,y)),x),f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,y)))),x)),x)),x)) = x # label(false). [para(7716(a,1),3502(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(7716(12))]. given #335 (F,wt=41): 8090 f(f(f(x,f(y,x)),x),f(f(x,f(f(x,f(f(x,f(f(f(x,x),z),f(f(f(f(f(y,x),z),z),x),f(y,x)))),x)),x)),x)) = x # label(false). [para(7717(a,1),3502(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(7717(12))]. given #336 (T,wt=15): 8239 f(f(x,y),f(f(y,f(f(x,y),y)),y)) = y. [para(7848(a,1),1614(a,1,2,1,1))]. given #337 (T,wt=15): 8363 f(f(x,y),f(f(y,f(f(y,x),y)),y)) = y. [para(7850(a,1),1369(a,1,2,1,1))]. given #338 (T,wt=15): 8366 f(f(x,y),f(f(x,f(f(x,y),x)),x)) = x. [para(7850(a,1),1649(a,1,2,1,1))]. given #339 (T,wt=15): 8448 f(f(f(x,f(x,x)),y),y) = f(x,f(x,x)). [para(7557(a,1),7850(a,1,1)),rewrite(7557(6),7648(7),2546(2)),flip(a)]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(9090)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c_0, f ]). NOTE: sn=96, num_tables=179 NOTE: updating interpretation 1: c_0=1. given #340 (A,wt=29): 291 f(f(f(x,y),f(f(f(f(f(f(x,x),z),y),y),f(x,x)),f(f(x,x),u))),x) = f(x,x). [para(13(a,1),55(a,1,2,1)),rewrite(13(26),40(14),13(26))]. given #341 (F,wt=23): 9841 f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),c_0))) = x # label(false). [back_rewrite(9198),rewrite(9232(9))]. given #342 (F,wt=23): 9845 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),c_0))) = y # label(false). [back_rewrite(9192),rewrite(9232(9))]. given #343 (F,wt=23): 9910 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),c_0))) = y # label(false). [back_rewrite(9046),rewrite(9232(9))]. given #344 (F,wt=25): 10906 f(x,f(f(f(c_0,f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),x))) = f(x,y) # label(false). [back_rewrite(9732),rewrite(9850(2),543(3),543(3),9850(3,R))]. given #345 (T,wt=7): 9232 f(x,f(x,x)) = c_0. [new_symbol(9090)]. given #346 (T,wt=7): 9850 f(c_0,x) = f(x,x). [back_rewrite(9182),rewrite(9232(4),9232(5),9232(8),9838(8),9421(5),9232(3)),flip(a)]. given #347 (T,wt=7): 9861 f(c_0,f(x,x)) = x. [back_rewrite(9150),rewrite(9232(2),9232(5),9850(5),9232(5),9850(5),2546(5),9232(5),9850(5),753(14),32(4))]. given #348 (T,wt=7): 9883 f(x,f(c_0,c_0)) = c_0. [back_rewrite(9106),rewrite(9232(2),9232(3),9232(4),604(6),9232(6))]. given #349 (A,wt=33): 294 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(u,f(y,y))))) = f(y,y). [para(55(a,1),13(a,1,2,2,2))]. given #350 (F,wt=23): 12699 f(f(x,y),f(f(f(y,y),z),f(c_0,f(f(f(f(y,x),z),z),y)))) = y # label(false). [para(9850(a,2),66(a,1,2,2))]. given #351 (F,wt=23): 12730 f(f(x,y),f(f(f(y,y),z),f(c_0,f(f(f(f(x,y),z),z),y)))) = y # label(false). [para(9850(a,2),1005(a,1,2,2))]. given #352 (F,wt=23): 12732 f(f(x,y),f(f(f(x,x),z),f(c_0,f(f(f(f(x,y),z),z),x)))) = x # label(false). [para(9850(a,2),1008(a,1,2,2))]. given #353 (F,wt=25): 10913 f(x,f(f(f(c_0,f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(9711),rewrite(9850(2),543(3),544(3),9850(3,R))]. given #354 (T,wt=7): 9913 f(f(c_0,c_0),x) = c_0. [back_rewrite(9029),rewrite(9232(2),9232(3),9232(6))]. given #355 (T,wt=7): 9914 f(x,c_0) = f(x,x). [back_rewrite(9025),rewrite(9232(2))]. given #356 (T,wt=7): 9915 f(f(x,x),c_0) = x. [back_rewrite(9023),rewrite(9232(3))]. given #357 (T,wt=7): 10812 f(f(x,x),x) = c_0. [back_rewrite(2546),rewrite(9232(4))]. given #358 (A,wt=51): 297 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(13(a,1),7(a,1,1,2)),rewrite(13(16),13(17),40(5),13(17),13(21),13(37))]. given #359 (F,wt=25): 12290 f(x,f(f(f(c_0,f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),c_0))) = f(y,x) # label(false). [para(2(a,1),9841(a,1,1)),rewrite(9850(3,R),2(15))]. given #360 (F,wt=25): 12295 f(x,f(f(f(c_0,f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),c_0))) = f(x,y) # label(false). [para(40(a,1),9841(a,1,1)),rewrite(9850(3,R),40(7))]. given #361 (F,wt=25): 12811 f(x,f(f(f(c_0,f(y,x)),z),f(c_0,f(f(f(x,z),z),f(y,x))))) = f(y,x) # label(false). [para(11(a,1),12699(a,1,2,2,2,1,1,1)),rewrite(544(3),9850(3,R))]. given #362 (F,wt=25): 12813 f(x,f(f(f(c_0,f(x,y)),z),f(c_0,f(f(f(x,z),z),f(x,y))))) = f(x,y) # label(false). [para(40(a,1),12699(a,1,2,2,2,1,1,1)),rewrite(543(3),9850(3,R))]. given #363 (T,wt=11): 9912 f(f(f(f(x,y),y),c_0),x) = c_0. [back_rewrite(9030),rewrite(9232(4),9232(7))]. given #364 (T,wt=11): 9978 f(x,f(f(f(x,y),y),c_0)) = c_0. [back_rewrite(8457),rewrite(9232(4),9232(7))]. given #365 (T,wt=11): 10023 f(x,f(f(f(x,x),y),c_0)) = c_0. [back_rewrite(7788),rewrite(9232(4),9232(7))]. given #366 (T,wt=11): 10025 f(f(f(f(x,x),y),c_0),x) = c_0. [back_rewrite(7786),rewrite(9232(4),9232(7))]. given #367 (A,wt=55): 661 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,f(f(z,x),v)),f(f(z,x),v)),f(z,x)),f(f(z,x),w)))) = f(z,x). [para(543(a,1),5(a,1,2,1))]. given #368 (F,wt=27): 12327 f(f(x,y),f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),c_0))),x)) = x # label(false). [para(9841(a,1),2257(a,1,2,1,1)),rewrite(9841(22),9841(24))]. given #369 (F,wt=27): 12433 f(f(x,y),f(f(y,f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),c_0))),y)) = y # label(false). [para(9845(a,1),2257(a,1,2,1,1)),rewrite(9845(22),9845(24))]. given #370 (F,wt=27): 12548 f(f(x,y),f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),c_0))),y)) = y # label(false). [para(9910(a,1),2257(a,1,2,1,1)),rewrite(9910(22),9910(24))]. given #371 (F,wt=27): 12608 f(f(f(x,f(x,y)),x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),c_0))) = x # label(false). [para(7716(a,1),9910(a,1,2,2,1,1,1,1))]. given #372 (T,wt=11): 10034 f(x,f(f(y,f(x,x)),c_0)) = c_0. [back_rewrite(7774),rewrite(9232(4),9232(7))]. given #373 (T,wt=11): 10036 f(f(f(x,f(y,y)),c_0),y) = c_0. [back_rewrite(7772),rewrite(9232(4),9232(7))]. given #374 (T,wt=11): 10042 f(f(x,x),f(f(y,x),c_0)) = c_0. [back_rewrite(7763),rewrite(9232(4),9232(7))]. given #375 (T,wt=11): 10046 f(f(f(x,y),c_0),f(y,y)) = c_0. [back_rewrite(7759),rewrite(9232(3),9232(7))]. given #376 (A,wt=37): 9753 f(f(x,x),f(f(f(c_0,f(f(x,x),y)),f(c_0,f(z,x))),f(f(f(z,x),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y). [back_rewrite(7757),rewrite(9231(6),9232(3),9232(7))]. given #377 (F,wt=23): 15356 f(f(x,y),f(f(f(x,x),z),f(f(f(z,f(f(x,y),z)),x),c_0))) = x # label(false). [back_rewrite(14825),rewrite(15201(3),7716(3),15202(5),15202(8),15257(8),15202(8),15202(11),15257(11),15202(6))]. given #378 (F,wt=23): 15820 f(f(x,y),f(f(f(x,x),z),f(c_0,f(f(z,f(f(x,y),z)),x)))) = x # label(false). [back_rewrite(13050),rewrite(15202(5),15202(8),15257(8),15202(9),15202(12),15257(12),15202(7))]. given #379 (F,wt=23): 15838 f(f(x,y),f(f(f(y,y),z),f(c_0,f(f(z,f(f(x,y),z)),y)))) = y # label(false). [back_rewrite(12981),rewrite(15202(5),15202(8),15257(8),15202(9),15202(12),15257(12),15202(7))]. given #380 (F,wt=23): 15849 f(f(x,y),f(f(f(y,y),z),f(c_0,f(f(z,f(f(y,x),z)),y)))) = y # label(false). [back_rewrite(12898),rewrite(15202(3),15202(5),15257(5),15202(2),15202(4),15257(4),15202(7))]. given #381 (T,wt=11): 10055 f(f(x,x),f(f(x,y),c_0)) = c_0. [back_rewrite(7746),rewrite(9232(4),9232(7))]. given #382 (T,wt=11): 10059 f(f(f(x,y),c_0),f(x,x)) = c_0. [back_rewrite(7742),rewrite(9232(3),9232(7))]. given #383 (T,wt=11): 10801 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(2631),rewrite(9232(3),9232(7))]. given #384 (T,wt=11): 10802 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_rewrite(2629),rewrite(9232(3),9232(7))]. given #385 (A,wt=37): 9754 f(f(x,x),f(f(f(c_0,f(f(x,x),y)),f(c_0,f(x,z))),f(f(f(x,z),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y). [back_rewrite(7740),rewrite(9231(6),9232(3),9232(7))]. given #386 (F,wt=25): 15716 f(x,f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(x,z)),f(x,y))))) = f(x,y) # label(false). [back_rewrite(13792),rewrite(15202(6),15202(8),15257(8),15202(5),15202(7),15257(7),15202(9),15202(11),15257(11),15202(8),15202(10),15257(10),15202(7))]. given #387 (F,wt=25): 15731 f(x,f(f(f(c_0,f(y,x)),z),f(c_0,f(f(z,f(x,z)),f(y,x))))) = f(y,x) # label(false). [back_rewrite(13696),rewrite(15202(6),15202(8),15257(8),15202(5),15202(7),15257(7),15202(9),15202(11),15257(11),15202(8),15202(10),15257(10),15202(7))]. given #388 (F,wt=25): 15801 f(x,f(f(f(c_0,f(y,x)),z),f(f(f(z,f(x,z)),f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(13110),rewrite(15202(9),15202(14),15257(14),15202(10),15202(15),15257(15),15202(6))]. given #389 (F,wt=25): 15893 f(x,f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),x))) = f(x,y) # label(false). [back_rewrite(12652),rewrite(15202(9),15202(14),15257(14),15202(10),15202(15),15257(15),15202(6))]. given #390 (T,wt=11): 10806 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(2617),rewrite(9232(2))]. given #391 (T,wt=11): 10808 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(2615),rewrite(9232(2))]. given #392 (T,wt=11): 10827 f(x,f(c_0,f(y,f(x,x)))) = c_0. [back_rewrite(2026),rewrite(9232(2),9232(7))]. given #393 (T,wt=11): 10828 f(x,f(c_0,f(f(x,x),y))) = c_0. [back_rewrite(1832),rewrite(9232(2),9232(7))]. given #394 (A,wt=37): 9813 f(f(x,x),f(f(f(c_0,f(f(x,x),y)),f(z,x)),f(f(f(x,f(z,x)),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y). [back_rewrite(702),rewrite(9231(6),9232(3))]. given #395 (F,wt=27): 18985 f(f(x,y),f(y,f(f(f(f(y,y),z),f(c_0,f(f(z,f(f(y,x),z)),y))),y))) = y # label(false). [back_rewrite(18973),rewrite(18981(9))]. given #396 (F,wt=27): 18986 f(f(x,y),f(x,f(f(f(f(x,x),z),f(c_0,f(f(z,f(f(x,y),z)),x))),x))) = x # label(false). [back_rewrite(18962),rewrite(18981(9))]. given #397 (F,wt=27): 19081 f(f(c_0,f(x,f(f(f(x,x),y),f(c_0,f(f(y,f(f(x,z),y)),x))))),f(z,x)) = c_0 # label(false). [back_rewrite(17210),rewrite(18981(12))]. given #398 (F,wt=27): 19082 f(f(c_0,f(x,f(f(f(x,x),y),f(c_0,f(f(y,f(f(z,x),y)),x))))),f(z,x)) = c_0 # label(false). [back_rewrite(17209),rewrite(18981(12))]. given #399 (T,wt=11): 10928 f(c_0,f(c_0,f(x,y))) = f(x,y). [back_rewrite(9506),rewrite(9823(8),9850(4,R))]. given #400 (T,wt=11): 12090 f(f(c_0,f(x,y)),x) = f(x,y). [back_rewrite(662),rewrite(9850(3,R))]. given #401 (T,wt=11): 12093 f(f(c_0,f(x,y)),y) = f(x,y). [back_rewrite(657),rewrite(9850(3,R))]. given #402 (T,wt=11): 14338 f(f(c_0,f(f(x,x),y)),x) = c_0. [para(9914(a,1),10025(a,1,1)),rewrite(9850(5,R))]. given #403 (A,wt=37): 9814 f(f(x,x),f(f(f(c_0,f(f(x,x),y)),f(x,z)),f(f(f(x,f(x,z)),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y). [back_rewrite(673),rewrite(9231(6),9232(3))]. given #404 (F,wt=27): 19083 f(f(c_0,f(x,f(f(f(x,x),y),f(c_0,f(f(y,f(f(x,z),y)),x))))),f(x,z)) = c_0 # label(false). [back_rewrite(17208),rewrite(18981(12))]. given #405 (F,wt=27): 19152 f(f(x,y),f(c_0,f(y,f(f(f(y,y),z),f(c_0,f(f(z,f(f(y,x),z)),y)))))) = c_0 # label(false). [back_rewrite(17120),rewrite(18981(13))]. given #406 (F,wt=27): 19153 f(f(x,y),f(c_0,f(y,f(f(f(y,y),z),f(c_0,f(f(z,f(f(x,y),z)),y)))))) = c_0 # label(false). [back_rewrite(17117),rewrite(18981(13))]. given #407 (F,wt=27): 19156 f(f(x,y),f(c_0,f(x,f(f(f(x,x),z),f(c_0,f(f(z,f(f(x,y),z)),x)))))) = c_0 # label(false). [back_rewrite(17114),rewrite(18981(13))]. given #408 (T,wt=11): 15058 f(f(c_0,f(x,f(y,y))),y) = c_0. [para(9914(a,1),10036(a,1,1)),rewrite(9850(5,R))]. given #409 (T,wt=11): 15093 f(f(c_0,f(x,y)),f(x,x)) = c_0. [para(543(a,1),10042(a,1,2,1)),rewrite(9850(3,R),9914(5))]. given #410 (T,wt=11): 15094 f(f(c_0,f(x,y)),f(y,y)) = c_0. [para(544(a,1),10042(a,1,2,1)),rewrite(9850(3,R),9914(5))]. given #411 (T,wt=11): 15201 f(f(x,y),x) = f(x,f(x,y)). [back_rewrite(11203),rewrite(15093(6),10808(5))]. given #412 (A,wt=41): 10013 f(f(f(f(c_0,f(x,f(y,y))),f(c_0,f(y,z))),f(f(f(y,z),f(x,f(y,y))),f(y,y))),f(c_0,f(x,f(y,y)))) = f(x,f(y,y)). [back_rewrite(7810),rewrite(9850(5,R),9232(6),9850(20,R))]. given #413 (F,wt=29): 15869 f(f(f(f(x,y),f(y,x)),x),f(f(f(x,x),z),f(c_0,f(f(z,f(f(x,y),z)),x)))) = x # label(false). [back_rewrite(12819),rewrite(15202(3),15202(5),15257(5),15202(10))]. given #414 (F,wt=29): 17518 f(f(f(x,x),y),f(f(x,z),f(c_0,f(f(z,f(f(f(x,x),y),z)),f(x,x))))) = f(x,x) # label(false). [back_rewrite(13028),rewrite(15202(8))]. given #415 (F,wt=29): 17554 f(f(x,f(y,y)),f(f(y,z),f(c_0,f(f(z,f(f(x,f(y,y)),z)),f(y,y))))) = f(y,y) # label(false). [back_rewrite(12965),rewrite(15202(8))]. given #416 (F,wt=29): 17657 f(f(x,f(y,y)),f(f(y,z),f(c_0,f(f(z,f(f(f(y,y),x),z)),f(y,y))))) = f(y,y) # label(false). [back_rewrite(12756),rewrite(15202(8))]. given #417 (T,wt=11): 15202 f(f(x,y),y) = f(y,f(x,y)). [back_rewrite(11168),rewrite(15093(6),10808(5))]. given #418 (T,wt=11): 15207 f(f(x,y),f(x,f(x,y))) = x. [back_rewrite(10982),rewrite(15093(5),15201(4),7716(4),12090(4),15201(3),7716(4),15201(3))]. given #419 (T,wt=11): 15257 f(f(x,y),f(y,f(x,y))) = y. [back_rewrite(10983),rewrite(15094(5),15201(4),7717(4),12093(4),15202(3),7717(4),15202(3))]. given #420 (T,wt=11): 15388 f(f(x,y),f(y,f(y,x))) = y. [back_rewrite(14777),rewrite(15201(4),15201(5),7716(5),15201(4),15160(8),15201(3))]. given #421 (A,wt=41): 10014 f(f(f(f(c_0,f(x,f(y,y))),f(c_0,f(z,y))),f(f(f(z,y),f(x,f(y,y))),f(y,y))),f(c_0,f(x,f(y,y)))) = f(x,f(y,y)). [back_rewrite(7809),rewrite(9850(5,R),9232(6),9850(20,R))]. given #422 (F,wt=29): 19079 f(f(c_0,f(f(x,y),f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),x)))),x) = c_0 # label(false). [back_rewrite(17212),rewrite(18981(14))]. given #423 (F,wt=29): 19085 f(f(c_0,f(f(x,y),f(f(f(c_0,f(x,y)),z),f(f(f(z,f(y,z)),f(x,y)),y)))),y) = c_0 # label(false). [back_rewrite(17206),rewrite(18981(14))]. given #424 (F,wt=29): 19088 f(f(c_0,f(f(x,y),f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(y,z)),f(x,y)))))),y) = c_0 # label(false). [back_rewrite(17202),rewrite(18981(11),18981(15))]. given #425 (F,wt=29): 19090 f(f(c_0,f(f(x,y),f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(x,z)),f(x,y)))))),x) = c_0 # label(false). [back_rewrite(17200),rewrite(18981(11),18981(15))]. given #426 (T,wt=11): 15683 f(x,f(c_0,f(y,f(x,y)))) = c_0. [back_rewrite(13969),rewrite(15202(4),15201(7),10928(7))]. given #427 (T,wt=11): 17205 f(f(c_0,f(x,f(y,x))),y) = c_0. [back_rewrite(13946),rewrite(15202(3))]. given #428 (T,wt=11): 18693 f(f(x,y),f(c_0,f(x,y))) = c_0. [back_rewrite(10738),rewrite(17485(9),15094(5)),flip(a)]. given #429 (T,wt=11): 18981 f(f(x,y),c_0) = f(c_0,f(x,y)). [para(10801(a,1),544(a,1,2)),rewrite(9850(7,R),10928(5))]. given #430 (A,wt=35): 10017 f(f(f(f(c_0,f(x,y)),f(c_0,f(z,f(y,y)))),f(f(f(z,f(y,y)),f(x,y)),y)),f(c_0,f(x,y))) = f(x,y). [back_rewrite(7806),rewrite(9850(3,R),9232(5),9850(17,R))]. given #431 (F,wt=29): 19148 f(x,f(c_0,f(f(x,y),f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),x))))) = c_0 # label(false). [back_rewrite(17126),rewrite(18981(14))]. given #432 (F,wt=29): 19158 f(x,f(c_0,f(f(y,x),f(f(f(c_0,f(y,x)),z),f(f(f(z,f(x,z)),f(y,x)),x))))) = c_0 # label(false). [back_rewrite(17112),rewrite(18981(14))]. given #433 (F,wt=29): 19161 f(x,f(c_0,f(f(y,x),f(f(f(c_0,f(y,x)),z),f(c_0,f(f(z,f(x,z)),f(y,x))))))) = c_0 # label(false). [back_rewrite(17109),rewrite(18981(11),18981(15))]. given #434 (F,wt=29): 19163 f(x,f(c_0,f(f(x,y),f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(x,z)),f(x,y))))))) = c_0 # label(false). [back_rewrite(17107),rewrite(18981(11),18981(15))]. given #435 (T,wt=11): 19240 f(f(c_0,f(x,y)),f(y,x)) = c_0. [back_rewrite(15684),rewrite(18981(3))]. given #436 (T,wt=11): 19279 f(f(x,y),f(c_0,f(y,x))) = c_0. [back_rewrite(15632),rewrite(18981(4))]. given #437 (T,wt=11): 20347 f(f(x,y),f(x,f(y,x))) = x. [para(19279(a,1),15820(a,1,2,2,2,1,2)),rewrite(10802(6),15201(8),10928(8),15202(5),10928(7))]. given #438 (T,wt=13): 16508 f(x,f(f(x,y),f(y,x))) = f(x,y). [back_rewrite(8555),rewrite(15201(2),15202(4),15207(4),15202(4),15202(6),15257(6),15202(3),15202(5),15257(5))]. given #439 (A,wt=35): 10018 f(f(f(f(c_0,f(x,y)),f(c_0,f(f(y,y),z))),f(f(f(f(y,y),z),f(x,y)),y)),f(c_0,f(x,y))) = f(x,y). [back_rewrite(7805),rewrite(9850(3,R),9232(5),9850(17,R))]. given #440 (F,wt=27): 20301 f(f(c_0,f(f(f(f(x,x),y),f(c_0,f(f(y,f(f(x,z),y)),x))),f(x,z))),x) = c_0 # label(false). [para(15820(a,1),19240(a,1,2))]. given #441 (F,wt=27): 20303 f(f(c_0,f(f(f(f(x,x),y),f(c_0,f(f(y,f(f(z,x),y)),x))),f(z,x))),x) = c_0 # label(false). [para(15838(a,1),19240(a,1,2))]. given #442 (F,wt=27): 20305 f(f(c_0,f(f(f(f(x,x),y),f(c_0,f(f(y,f(f(x,z),y)),x))),f(z,x))),x) = c_0 # label(false). [para(15849(a,1),19240(a,1,2))]. given #443 (F,wt=27): 20348 f(x,f(c_0,f(f(f(f(x,x),y),f(c_0,f(f(y,f(f(x,z),y)),x))),f(x,z)))) = c_0 # label(false). [para(15820(a,1),19279(a,1,1))]. given #444 (T,wt=15): 12185 f(f(x,f(y,z)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(9736),rewrite(12090(7),9850(5,R))]. given #445 (T,wt=15): 15209 f(x,f(c_0,f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(10949),rewrite(15201(2),7716(3),15201(2),15202(4),15207(4),15093(5))]. given #446 (T,wt=15): 16486 f(x,f(f(y,f(x,y)),f(y,x))) = f(y,x). [back_rewrite(8676),rewrite(15202(2),7717(3),15202(2),15202(4),15257(4),15202(2))]. given #447 (T,wt=15): 18696 f(f(f(x,y),z),f(c_0,f(x,y))) = f(x,y). [back_rewrite(10299),rewrite(18693(10),12093(7),9850(5,R))]. given #448 (A,wt=31): 10020 f(x,f(f(f(c_0,f(x,y)),f(c_0,f(f(x,x),z))),f(f(f(f(x,x),z),f(x,y)),x))) = f(x,y). [back_rewrite(7791),rewrite(9850(3,R),9232(5))]. given #449 (F,wt=27): 20350 f(x,f(c_0,f(f(f(f(x,x),y),f(c_0,f(f(y,f(f(z,x),y)),x))),f(z,x)))) = c_0 # label(false). [para(15838(a,1),19279(a,1,1))]. given #450 (F,wt=27): 20352 f(x,f(c_0,f(f(f(f(x,x),y),f(c_0,f(f(y,f(f(x,z),y)),x))),f(z,x)))) = c_0 # label(false). [para(15849(a,1),19279(a,1,1))]. given #451 (F,wt=29): 20310 f(f(c_0,f(f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(x,z)),f(x,y)))),x)),f(x,y)) = c_0 # label(false). [para(15716(a,1),19240(a,1,2))]. given #452 (F,wt=29): 20313 f(f(c_0,f(f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(y,z)),f(x,y)))),y)),f(x,y)) = c_0 # label(false). [para(15731(a,1),19240(a,1,2))]. given #453 (T,wt=15): 20335 f(f(x,x),f(f(x,f(x,y)),f(y,x))) = c_0. [para(15388(a,1),19240(a,1,1,2)),rewrite(9850(2))]. given #454 (T,wt=15): 20336 f(f(c_0,f(f(x,f(x,y)),f(y,x))),x) = c_0. [para(15388(a,1),19240(a,1,2))]. given #455 (T,wt=15): 20384 f(x,f(c_0,f(f(x,f(x,y)),f(y,x)))) = c_0. [para(15388(a,1),19279(a,1,1))]. given #456 (T,wt=15): 20385 f(f(f(x,f(x,y)),f(y,x)),f(x,x)) = c_0. [para(15388(a,1),19279(a,1,2,2)),rewrite(9850(6))]. given #457 (A,wt=31): 10021 f(x,f(f(f(c_0,f(y,x)),f(c_0,f(f(x,x),z))),f(f(f(f(x,x),z),f(y,x)),x))) = f(y,x). [back_rewrite(7790),rewrite(9850(3,R),9232(5))]. given #458 (F,wt=29): 20316 f(f(c_0,f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(y,z)),f(x,y)),y)),y)),f(x,y)) = c_0 # label(false). [para(15801(a,1),19240(a,1,2))]. given #459 (F,wt=29): 20319 f(f(c_0,f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),x)),x)),f(x,y)) = c_0 # label(false). [para(15893(a,1),19240(a,1,2))]. given #460 (F,wt=29): 20357 f(f(x,y),f(c_0,f(f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(x,z)),f(x,y)))),x))) = c_0 # label(false). [para(15716(a,1),19279(a,1,1))]. given #461 (F,wt=29): 20360 f(f(x,y),f(c_0,f(f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(y,z)),f(x,y)))),y))) = c_0 # label(false). [para(15731(a,1),19279(a,1,1))]. given #462 (T,wt=15): 20439 f(f(x,x),f(f(x,f(y,x)),f(x,y))) = c_0. [para(20347(a,1),19240(a,1,1,2)),rewrite(9850(2))]. given #463 (T,wt=15): 20440 f(f(c_0,f(f(x,f(y,x)),f(x,y))),x) = c_0. [para(20347(a,1),19240(a,1,2))]. given #464 (T,wt=15): 20441 f(x,f(c_0,f(f(x,f(y,x)),f(x,y)))) = c_0. [para(20347(a,1),19279(a,1,1))]. given #465 (T,wt=15): 20442 f(f(f(x,f(y,x)),f(x,y)),f(x,x)) = c_0. [para(20347(a,1),19279(a,1,2,2)),rewrite(9850(6))]. given #466 (A,wt=39): 10028 f(f(f(f(c_0,f(x,y)),f(c_0,f(f(y,y),z))),f(f(f(f(y,y),z),f(x,y)),f(f(x,y),u))),f(c_0,f(x,y))) = f(x,y). [back_rewrite(7783),rewrite(9850(3,R),9232(5),9850(19,R))]. given #467 (F,wt=29): 20363 f(f(x,y),f(c_0,f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(y,z)),f(x,y)),y)),y))) = c_0 # label(false). [para(15801(a,1),19279(a,1,1))]. given #468 (F,wt=29): 20366 f(f(x,y),f(c_0,f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),x)),x))) = c_0 # label(false). [para(15893(a,1),19279(a,1,1))]. given #469 (F,wt=29): 20405 f(f(x,y),f(x,f(f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(x,z)),f(x,y)))),x))) = x # label(false). [para(15716(a,1),20347(a,1,1))]. given #470 (F,wt=29): 20407 f(f(x,y),f(y,f(f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(y,z)),f(x,y)))),y))) = y # label(false). [para(15731(a,1),20347(a,1,1))]. given #471 (T,wt=15): 20677 f(f(c_0,f(x,y)),f(f(x,y),z)) = f(x,y). [para(12185(a,1),604(a,1,2,1)),rewrite(9850(13,R),10928(11))]. given #472 (T,wt=15): 20678 f(f(c_0,f(x,y)),f(z,f(x,y))) = f(x,y). [para(12185(a,1),607(a,1,2,2)),rewrite(9850(13,R),10928(11))]. given #473 (T,wt=15): 20683 f(f(x,y),f(c_0,f(f(c_0,f(x,y)),z))) = c_0. [para(12185(a,1),10801(a,1,1))]. given #474 (T,wt=15): 20684 f(f(c_0,f(x,f(y,z))),f(c_0,f(y,z))) = c_0. [para(12185(a,1),10801(a,1,2,2)),rewrite(9850(5,R))]. given #475 (A,wt=31): 10031 f(x,f(f(f(c_0,f(x,y)),f(c_0,f(z,f(x,x)))),f(f(f(z,f(x,x)),f(x,y)),x))) = f(x,y). [back_rewrite(7777),rewrite(9850(3,R),9232(5))]. given #476 (F,wt=29): 20409 f(f(x,y),f(y,f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(y,z)),f(x,y)),y)),y))) = y # label(false). [para(15801(a,1),20347(a,1,1))]. given #477 (F,wt=29): 20411 f(f(x,y),f(x,f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),x)),x))) = x # label(false). [para(15893(a,1),20347(a,1,1))]. given #478 (F,wt=29): 21333 f(f(c_0,f(f(f(f(x,x),y),f(f(f(y,f(f(x,z),y)),x),f(x,z))),f(x,z))),x) = c_0 # label(false). [para(543(a,1),20316(a,1,1,2,1,1,1,2)),rewrite(9850(3),543(9),543(16))]. given #479 (F,wt=29): 21335 f(f(c_0,f(f(f(f(x,x),y),f(f(f(y,f(f(z,x),y)),x),f(z,x))),f(z,x))),x) = c_0 # label(false). [para(544(a,1),20316(a,1,1,2,1,1,1,2)),rewrite(9850(3),544(9),544(16))]. given #480 (T,wt=15): 20685 f(f(x,y),f(c_0,f(z,f(c_0,f(x,y))))) = c_0. [para(12185(a,1),10802(a,1,1))]. given #481 (T,wt=15): 20688 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,y)))) = c_0. [para(12185(a,1),10827(a,1,2,2,2))]. given #482 (T,wt=15): 20689 f(f(c_0,f(x,y)),f(c_0,f(f(x,y),z))) = c_0. [para(12185(a,1),10828(a,1,2,2,1))]. given #483 (T,wt=15): 20693 f(f(c_0,f(f(x,y),z)),f(c_0,f(x,y))) = c_0. [para(12185(a,1),14338(a,1,1,2,1))]. given #484 (A,wt=31): 10032 f(x,f(f(f(c_0,f(y,x)),f(c_0,f(z,f(x,x)))),f(f(f(z,f(x,x)),f(y,x)),x))) = f(y,x). [back_rewrite(7776),rewrite(9850(3,R),9232(5))]. given #485 (F,wt=29): 21414 f(f(x,y),f(y,f(f(f(f(c_0,f(y,x)),z),f(c_0,f(f(z,f(y,z)),f(y,x)))),y))) = y # label(false). [para(20357(a,1),15849(a,1,2,2,2,1,2)),rewrite(10802(17),15201(19),10928(19),15202(16),10928(18))]. given #486 (F,wt=29): 21421 f(f(c_0,f(f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(x,z)),f(x,y)))),x)),f(y,x)) = c_0 # label(false). [para(20357(a,1),19081(a,1,1,2,2,2,2,1,2)),rewrite(10802(17),15201(19),10928(19),15202(16),10928(18),7717(15))]. given #487 (F,wt=29): 21425 f(f(x,y),f(c_0,f(f(f(f(c_0,f(y,x)),z),f(c_0,f(f(z,f(y,z)),f(y,x)))),y))) = c_0 # label(false). [para(20357(a,1),19152(a,1,2,2,2,2,2,1,2)),rewrite(10802(18),15201(20),10928(20),15202(17),10928(19),7717(16))]. given #488 (F,wt=29): 21736 f(x,f(c_0,f(f(f(f(x,x),y),f(f(f(y,f(f(x,z),y)),x),f(x,z))),f(x,z)))) = c_0 # label(false). [para(543(a,1),20363(a,1,1)),rewrite(543(5),9850(3),543(9))]. given #489 (T,wt=15): 20699 f(f(c_0,f(f(c_0,f(x,y)),z)),f(x,y)) = c_0. [para(12185(a,1),15093(a,1,2))]. given #490 (T,wt=15): 20700 f(f(c_0,f(x,f(c_0,f(y,z)))),f(y,z)) = c_0. [para(12185(a,1),15094(a,1,2))]. given #491 (T,wt=15): 20744 f(f(f(x,f(x,y)),y),f(c_0,f(x,y))) = c_0. [para(15209(a,1),10802(a,1,2,2)),rewrite(9850(11,R),10928(7))]. given #492 (T,wt=15): 20782 f(f(c_0,f(x,y)),f(f(x,f(x,y)),y)) = c_0. [para(15209(a,1),15094(a,1,1,2)),rewrite(9850(14,R),10928(10))]. given #493 (A,wt=39): 10039 f(f(f(f(c_0,f(x,y)),f(c_0,f(z,f(y,y)))),f(f(f(z,f(y,y)),f(x,y)),f(f(x,y),u))),f(c_0,f(x,y))) = f(x,y). [back_rewrite(7769),rewrite(9850(3,R),9232(5),9850(19,R))]. given #494 (F,wt=29): 21738 f(x,f(c_0,f(f(f(f(x,x),y),f(f(f(y,f(f(z,x),y)),x),f(z,x))),f(z,x)))) = c_0 # label(false). [para(544(a,1),20363(a,1,1)),rewrite(544(5),9850(3),544(9))]. given #495 (F,wt=29): 21788 f(f(x,y),f(y,f(f(f(f(c_0,f(y,x)),z),f(f(f(z,f(y,z)),f(y,x)),y)),y))) = y # label(false). [para(20366(a,1),15849(a,1,2,2,2,1,2)),rewrite(10802(16),15201(18),10928(18),15202(15),10928(17))]. given #496 (F,wt=29): 21792 f(f(c_0,f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),x)),x)),f(y,x)) = c_0 # label(false). [para(20366(a,1),19081(a,1,1,2,2,2,2,1,2)),rewrite(10802(16),15201(18),10928(18),15202(15),10928(17),7717(14))]. given #497 (F,wt=29): 21796 f(f(x,y),f(c_0,f(f(f(f(c_0,f(y,x)),z),f(f(f(z,f(y,z)),f(y,x)),y)),y))) = c_0 # label(false). [para(20366(a,1),19152(a,1,2,2,2,2,2,1,2)),rewrite(10802(17),15201(19),10928(19),15202(16),10928(18),7717(15))]. given #498 (T,wt=15): 22618 f(f(f(x,f(x,y)),y),x) = f(x,f(x,y)). [para(20744(a,1),15820(a,1,2,2,2,1,2)),rewrite(9850(8,R),20684(11),15201(10),10928(10),15207(9),9850(6),9861(6))]. given #499 (T,wt=15): 22620 f(f(f(x,f(x,y)),y),f(y,f(x,y))) = y. [para(20744(a,1),15838(a,1,2,2,2,1,2)),rewrite(10802(8),15201(10),10928(10),15202(7),10928(9))]. given #500 (T,wt=15): 22622 f(f(x,f(y,f(y,x))),y) = f(y,f(y,x)). [para(20744(a,1),15849(a,1,2,2,2,1,2)),rewrite(9850(8,R),20684(11),15201(10),10928(10),15207(9),9850(6),9861(6))]. given #501 (T,wt=15): 22633 f(f(c_0,f(x,y)),f(y,f(x,f(x,y)))) = c_0. [para(20744(a,1),19081(a,1,1,2,2,2,2,1,2)),rewrite(9850(8,R),20684(11),15201(10),10928(10),15207(9),9850(6),9861(6),15201(4),7716(4))]. given #502 (A,wt=37): 10047 f(f(x,x),f(f(f(c_0,f(y,f(x,x))),f(c_0,f(z,x))),f(f(f(z,x),f(y,f(x,x))),f(x,x)))) = f(y,f(x,x)). [back_rewrite(7758),rewrite(9850(6,R),9232(7))]. given #503 (F,wt=31): 15847 f(f(f(f(x,f(y,x)),f(x,y)),y),f(f(f(y,y),z),f(c_0,f(f(z,f(f(x,y),z)),y)))) = y # label(false). [back_rewrite(12900),rewrite(15202(3),15201(8),7717(8),15202(11))]. given #504 (F,wt=31): 18689 f(x,f(f(x,y),f(f(f(f(c_0,f(x,y)),z),f(c_0,f(f(z,f(x,z)),f(x,y)))),x))) = f(x,y) # label(false). [back_rewrite(15724),rewrite(17253(16))]. given #505 (F,wt=31): 18690 f(x,f(f(y,x),f(f(f(f(c_0,f(y,x)),z),f(c_0,f(f(z,f(x,z)),f(y,x)))),x))) = f(y,x) # label(false). [back_rewrite(15739),rewrite(17303(16))]. given #506 (F,wt=31): 18761 f(x,f(f(x,y),f(f(f(f(c_0,f(x,y)),z),f(f(f(z,f(x,z)),f(x,y)),x)),x))) = f(x,y) # label(false). [back_rewrite(15977),rewrite(18062(15))]. given #507 (T,wt=15): 22635 f(f(x,f(y,f(y,x))),f(c_0,f(y,x))) = c_0. [para(20744(a,1),19152(a,1,2,2,2,2,2,1,2)),rewrite(9850(11,R),20684(14),15201(13),10928(13),15207(12),9850(9),9861(9),15201(7),7716(7))]. given #508 (T,wt=15): 23057 f(f(x,f(f(x,f(x,y)),y)),f(x,y)) = x. [para(22618(a,1),20347(a,1,2,2)),rewrite(7716(7))]. given #509 (T,wt=15): 23262 f(f(x,f(y,f(x,f(x,y)))),f(x,y)) = x. [para(22622(a,1),20347(a,1,2,2)),rewrite(7716(7))]. given #510 (T,wt=15): 23699 f(f(x,f(y,f(y,x))),f(x,f(y,x))) = x. [para(22635(a,1),15820(a,1,2,2,2,1,2)),rewrite(10802(8),15201(10),10928(10),15202(7),10928(9))]. given #511 (A,wt=37): 10060 f(f(x,x),f(f(f(c_0,f(y,f(x,x))),f(c_0,f(x,z))),f(f(f(x,z),f(y,f(x,x))),f(x,x)))) = f(y,f(x,x)). [back_rewrite(7741),rewrite(9850(6,R),9232(7))]. given #512 (F,wt=31): 18775 f(x,f(f(y,x),f(f(f(f(c_0,f(y,x)),z),f(f(f(z,f(x,z)),f(y,x)),x)),x))) = f(y,x) # label(false). [back_rewrite(15978),rewrite(18063(15))]. given #513 (F,wt=31): 19074 f(f(f(x,f(f(y,f(z,f(x,z))),x)),f(z,f(x,z))),f(y,f(z,f(x,z)))) = f(z,f(x,z)) # label(false). [back_rewrite(17217),rewrite(18981(5),10928(6),18981(10),10928(11),18981(13),10928(14),18981(17),10928(18))]. given #514 (F,wt=31): 19143 f(f(x,y),f(f(f(c_0,f(z,f(f(y,y),z))),f(f(x,y),f(c_0,f(z,f(f(y,y),z))))),y)) = y # label(false). [back_rewrite(17131),rewrite(18981(7),18981(13),18981(18),10928(19))]. given #515 (F,wt=31): 19144 f(f(x,y),f(f(f(y,y),f(c_0,f(z,f(f(x,y),z)))),f(c_0,f(f(z,f(f(x,y),z)),y)))) = y # label(false). [back_rewrite(17130),rewrite(18981(7),18981(14),10928(15),18981(14))]. given #516 (T,wt=17): 15217 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(y,z)))) = y. [back_rewrite(11989),rewrite(15094(5),15201(4),7717(4),12093(4),15202(4))]. given #517 (T,wt=15): 24288 f(f(f(x,f(y,x)),f(x,z)),f(x,x)) = c_0. [para(15217(a,1),10802(a,1,2,2)),rewrite(9850(13,R),10928(8),9850(6))]. given #518 (T,wt=13): 24454 f(f(f(x,y),f(x,z)),f(x,x)) = c_0. [para(15201(a,1),24288(a,1,1,1,2)),rewrite(7716(3))]. given #519 (T,wt=13): 24461 f(f(f(x,y),f(y,z)),f(y,y)) = c_0. [para(15202(a,1),24288(a,1,1,1,2)),rewrite(7717(3))]. given #520 (A,wt=41): 10874 f(f(f(f(c_0,f(x,f(y,y))),f(z,y)),f(f(f(y,f(z,y)),f(x,f(y,y))),f(y,y))),f(c_0,f(x,f(y,y)))) = f(x,f(y,y)). [back_rewrite(7798),rewrite(9850(5,R),9850(19,R))]. given #521 (F,wt=31): 19145 f(f(x,y),f(f(f(c_0,f(z,f(f(y,y),z))),f(f(y,x),f(c_0,f(z,f(f(y,y),z))))),y)) = y # label(false). [back_rewrite(17129),rewrite(18981(7),18981(13),18981(18),10928(19))]. given #522 (F,wt=31): 19146 f(f(x,y),f(f(f(y,y),f(c_0,f(z,f(f(y,x),z)))),f(c_0,f(f(z,f(f(y,x),z)),y)))) = y # label(false). [back_rewrite(17128),rewrite(18981(7),18981(14),10928(15),18981(14))]. given #523 (F,wt=31): 19147 f(x,f(f(f(c_0,f(x,y)),f(c_0,f(z,f(x,z)))),f(f(f(z,f(x,z)),f(x,y)),x))) = f(x,y) # label(false). [back_rewrite(17127),rewrite(18981(7),18981(13),10928(14))]. % Operation f is commutative; C redundancy checks enabled. given #524 (F,wt=23): 24836 f(f(x,y),f(f(z,f(x,x)),f(c_0,f(x,f(z,f(z,f(x,y))))))) = x # label(false). [para(19147(a,1),15847(a,1,1,1,1,2)),rewrite(24796(12),24796(13),24796(14),24796(16),24796(28),24796(29),24796(30),24796(31),24803(31),24796(18),24808(18),24796(15),24803(15),24796(3),24796(16),24796(17),24796(18),24796(19),24803(19),24796(6),24796(8))]. given #525 (T,wt=7): 24796 f(x,y) = f(y,x). [para(15202(a,1),19147(a,1,2,2,1)),rewrite(20688(8),15257(5),10808(4))]. given #526 (T,wt=11): 24805 f(x,f(c_0,f(y,f(y,x)))) = c_0. [para(17205(a,1),19147(a,2)),rewrite(24796(2),24796(7),24796(10),24796(14),24796(17),24796(22),24796(25),24796(28),24796(31),24796(32),24796(34),24796(37),24804(37),24796(26),20675(26),10808(12))]. given #527 (T,wt=13): 24507 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(24454(a,1),19081(a,1,1,2,2,2,2,1,2)),rewrite(9850(5,R),15093(7),18981(7),9861(7),10928(8),15207(5),9850(2))]. given #528 (T,wt=13): 24936 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [back_rewrite(24559),rewrite(24796(2),24796(5))]. given #529 (A,wt=17): 18649 f(x,f(f(x,y),f(c_0,f(z,f(x,x))))) = f(x,x). [back_rewrite(7880),rewrite(15207(5),9232(3))]. given #530 (F,wt=23): 25164 f(f(x,y),f(f(z,f(y,y)),f(c_0,f(y,f(z,f(z,f(x,y))))))) = y # label(false). [back_rewrite(23493),rewrite(24796(2),24796(5),15207(5),24796(2),24796(3),24796(6),15207(6),24796(4),15207(4),24796(3),24796(6),24796(8))]. given #531 (F,wt=25): 24878 f(x,f(f(y,f(c_0,f(x,z))),f(c_0,f(f(x,z),f(y,f(x,y)))))) = f(x,z) # label(false). [back_rewrite(24711),rewrite(24796(4),24796(10),24796(12),24796(14),24796(15),24796(16),24849(16),24796(2),543(3),24796(2),24796(4),24796(8),24796(9),24796(13))]. given #532 (F,wt=25): 25178 f(x,f(f(y,f(c_0,f(z,x))),f(c_0,f(f(z,x),f(y,f(x,y)))))) = f(z,x) # label(false). [back_rewrite(23451),rewrite(24796(4),24796(5),15257(5),24796(2),24796(3),24796(4),15257(4),24796(2),24796(4),24796(8),24796(9),15257(9),24796(8),24796(9),24796(13))]. given #533 (F,wt=25): 25838 f(x,f(f(y,f(c_0,f(x,z))),f(x,f(f(x,z),f(y,f(x,y)))))) = f(x,z) # label(false). [back_rewrite(18900),rewrite(24796(2),24796(4),24796(6),24796(8),24796(11),24796(14),25835(14),24796(4),24796(8),24796(9))]. given #534 (T,wt=11): 26375 f(x,f(c_0,f(y,x))) = f(y,x). [para(25164(a,1),543(a,1,2)),rewrite(9914(3,R),24796(3),24796(4))]. given #535 (T,wt=11): 26376 f(f(x,x),f(c_0,f(y,x))) = c_0. [para(25164(a,1),10801(a,1,2,2)),rewrite(9914(3,R),24796(3),24796(5),9914(5),24796(5))]. given #536 (T,wt=11): 26378 f(x,f(x,f(y,x))) = f(y,x). [para(25164(a,1),15207(a,1,2,2)),rewrite(25164(11),24796(2))]. given #537 (T,wt=13): 26362 f(f(c_0,c_0),f(f(x,y),f(z,z))) = c_0. [para(10928(a,1),24507(a,1,2,1)),rewrite(24796(6),9914(6))]. given #538 (A,wt=21): 18936 f(f(x,y),f(y,f(c_0,f(z,f(c_0,f(x,y)))))) = f(c_0,f(x,y)). [back_rewrite(16291),rewrite(18693(6))]. given #539 (F,wt=25): 26292 f(x,f(f(y,f(c_0,f(z,x))),f(x,f(f(z,x),f(y,f(x,y)))))) = f(z,x) # label(false). [back_rewrite(15798),rewrite(24796(4),24796(8),24796(9),24796(14),24796(18),24796(19),24796(21),24796(24),25168(24),24796(11))]. given #540 (F,wt=25): 26348 f(x,f(f(y,f(c_0,f(x,z))),f(x,f(f(y,f(y,x)),f(x,z))))) = f(x,z) # label(false). [back_rewrite(25998),rewrite(24796(6),24796(8),26211(21),24796(11))]. given #541 (F,wt=25): 26386 f(x,f(f(y,f(c_0,f(x,z))),f(c_0,f(f(y,f(y,x)),f(x,z))))) = f(x,z) # label(false). [para(24878(a,1),24796(a,2)),rewrite(24796(7),24796(9),24796(12))]. given #542 (F,wt=25): 26393 f(x,f(f(y,f(c_0,f(z,x))),f(c_0,f(f(y,f(y,x)),f(z,x))))) = f(z,x) # label(false). [para(25178(a,1),24796(a,2)),rewrite(24796(7),24796(9),24796(12))]. given #543 (T,wt=13): 26409 f(f(c_0,c_0),f(x,f(c_0,f(y,z)))) = c_0. [para(20685(a,1),26376(a,1,2,2)),rewrite(9914(13,R),24796(8),10928(8),24796(8))]. given #544 (T,wt=13): 26414 f(f(c_0,c_0),f(f(x,y),f(z,u))) = c_0. [para(12185(a,1),26362(a,1,2,2))]. given #545 (T,wt=15): 24917 f(x,f(f(y,f(x,x)),f(z,f(x,x)))) = c_0. [back_rewrite(24615),rewrite(24796(6))]. given #546 (T,wt=15): 24937 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0. [back_rewrite(24558),rewrite(24796(3))]. given #547 (A,wt=21): 18939 f(f(x,y),f(x,f(c_0,f(z,f(c_0,f(x,y)))))) = f(c_0,f(x,y)). [back_rewrite(16267),rewrite(18693(6))]. given #548 (F,wt=19): 26458 f(f(x,y),f(c_0,f(x,f(f(x,y),f(z,f(x,z)))))) = c_0 # label(false). [para(25838(a,1),24937(a,1,1))]. given #549 (F,wt=19): 26459 f(f(x,y),f(c_0,f(y,f(f(x,y),f(z,f(y,z)))))) = c_0 # label(false). [para(26292(a,1),24937(a,1,1))]. given #550 (F,wt=19): 26471 f(x,f(c_0,f(f(x,y),f(x,f(z,f(z,f(x,y))))))) = c_0 # label(false). [para(11(a,1),26458(a,1,1)),rewrite(24796(2),24796(3),24796(5),543(5),24796(3),24796(4))]. given #551 (F,wt=19): 26472 f(x,f(c_0,f(f(y,x),f(x,f(z,f(z,f(y,x))))))) = c_0 # label(false). [para(11(a,1),26458(a,1,2,2,2,1)),rewrite(11(3),24796(4))]. given #552 (T,wt=15): 24938 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0. [back_rewrite(24556),rewrite(24796(3))]. given #553 (T,wt=15): 25084 f(f(x,f(x,y)),f(x,f(y,f(x,y)))) = x. [back_rewrite(23994),rewrite(24796(1),24796(4),15207(4),24796(5),24796(8),15207(8),24796(5),24796(6),24796(7),24796(10),15207(10))]. given #554 (T,wt=15): 25165 f(x,f(y,f(x,f(y,x)))) = f(x,f(y,x)). [back_rewrite(23491),rewrite(24796(1),24796(3),24796(5),24796(8),15207(8),24796(1),24796(4),24796(5))]. given #555 (T,wt=15): 25169 f(f(x,f(y,x)),f(x,f(y,f(y,x)))) = x. [back_rewrite(23484),rewrite(24796(9),24796(10),15257(10),24796(3),24796(6))]. given #556 (A,wt=17): 19404 f(f(c_0,f(x,f(y,y))),f(c_0,f(y,f(z,z)))) = c_0. [back_rewrite(15043),rewrite(18981(4))]. given #557 (F,wt=25): 26397 f(f(x,y),f(f(z,f(y,y)),f(f(x,y),f(y,f(z,f(z,f(x,y))))))) = y # label(false). [para(11(a,1),25838(a,1,2,1,2,2)),rewrite(24796(3),9914(3),11(7),24796(6),11(14))]. given #558 (F,wt=15): 26605 f(f(x,y),f(x,f(z,f(z,f(x,y))))) = x # label(false). [para(26397(a,1),25164(a,1,2,2,2,2,2)),rewrite(24796(3),24796(4),24796(10),24796(11),24796(12),24796(17),24796(18),9914(23,R),24796(18),10806(19),24796(17),24796(18),24796(23),24796(24),24796(25),24947(25),24796(19),26446(19),24796(11),25866(11),24796(1),24796(2)),flip(a)]. given #559 (F,wt=15): 26613 f(x,f(f(x,y),f(z,f(x,z)))) = f(x,y) # label(false). [para(11(a,1),26605(a,1,1)),rewrite(24796(1),24796(2),24796(4),543(4),24796(2),24796(6))]. given #560 (F,wt=15): 26614 f(x,f(f(y,x),f(z,f(x,z)))) = f(y,x) # label(false). [para(11(a,1),26605(a,1,2,2,2,2)),rewrite(11(3),24796(2))]. given #561 (T,wt=13): 26576 f(x,f(c_0,f(f(x,x),f(y,y)))) = c_0. [para(607(a,1),19404(a,1,1,2)),rewrite(9861(3))]. given #562 (T,wt=13): 26703 f(x,f(c_0,f(f(x,x),f(y,z)))) = c_0. [para(12185(a,1),26576(a,1,2,2,2))]. given #563 (T,wt=15): 25242 f(x,f(y,f(x,f(x,y)))) = f(x,f(x,y)). [back_rewrite(23067),rewrite(24796(1),24796(5),24796(6),15257(6),24796(3),24796(4),24796(5))]. given #564 (T,wt=13): 26716 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(26703(a,1),25242(a,1,2,2,2)),rewrite(9914(7),24796(7),10806(7),26703(10),9914(6))]. given #565 (A,wt=31): 19968 f(f(x,f(y,y)),f(f(y,f(z,f(x,f(y,y)))),f(c_0,f(f(y,y),f(x,f(y,y)))))) = f(y,y). [para(15257(a,1),17554(a,1,2,2,2,1)),rewrite(15202(11))]. given #566 (F,wt=15): 26618 f(f(x,y),f(y,f(z,f(z,f(x,y))))) = y # label(false). [para(24796(a,1),26605(a,1,1)),rewrite(24796(2))]. given #567 (F,wt=19): 26615 f(f(x,y),f(c_0,f(x,f(x,f(z,f(z,f(x,y))))))) = c_0 # label(false). [para(26605(a,1),15683(a,1,2,2,2)),rewrite(24796(7))]. given #568 (F,wt=19): 26619 f(f(x,f(y,f(y,f(x,z)))),f(c_0,f(x,f(x,z)))) = c_0 # label(false). [para(26605(a,1),24805(a,1,2,2,2)),rewrite(24796(7))]. given #569 (F,wt=19): 26650 f(x,f(c_0,f(f(x,y),f(f(x,y),f(z,f(x,z)))))) = c_0 # label(false). [para(26613(a,1),15683(a,1,2,2,2)),rewrite(24796(7))]. given #570 (T,wt=15): 25479 f(x,f(c_0,f(y,f(x,f(x,y))))) = f(x,y). [back_rewrite(20901),rewrite(24796(2),24796(6),24796(7),15257(7),24796(4),24796(7))]. given #571 (T,wt=15): 26354 f(x,f(c_0,f(y,f(x,f(y,x))))) = f(y,x). [back_rewrite(26302),rewrite(24796(2),24796(6),24796(9),24796(10),26179(13),24796(6),24796(7))]. given #572 (T,wt=15): 26574 f(f(c_0,f(x,f(y,y))),f(c_0,f(y,z))) = c_0. [para(11(a,1),19404(a,1,2,2,2))]. given #573 (T,wt=15): 26575 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(11(a,1),19404(a,1,2,2)),rewrite(9914(4,R),24796(4),24796(8),9914(8),24796(8))]. given #574 (A,wt=17): 20676 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [para(12185(a,1),544(a,1,1))]. given #575 (F,wt=19): 26654 f(f(c_0,f(x,f(x,y))),f(f(x,y),f(z,f(x,z)))) = c_0 # label(false). [para(26613(a,1),24805(a,1,2,2,2)),rewrite(24796(9))]. given #576 (F,wt=19): 26690 f(f(c_0,f(x,f(y,x))),f(f(y,x),f(z,f(x,z)))) = c_0 # label(false). [para(26614(a,1),24805(a,1,2,2,2)),rewrite(24796(9))]. given #577 (F,wt=19): 26742 f(f(x,y),f(c_0,f(y,f(y,f(z,f(z,f(x,y))))))) = c_0 # label(false). [para(26618(a,1),15683(a,1,2,2,2)),rewrite(24796(7))]. given #578 (F,wt=19): 26759 f(x,f(c_0,f(f(y,x),f(f(y,x),f(z,f(x,z)))))) = c_0 # label(false). [para(11(a,1),26615(a,1,2,2,2,2,2,2)),rewrite(11(3),24796(4))]. given #579 (T,wt=15): 26594 f(f(x,y),f(y,f(z,f(c_0,f(x,y))))) = y. [back_rewrite(25720),rewrite(26575(16),24796(10),10928(10),7716(8))]. given #580 (T,wt=15): 26649 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(10827(a,1),26613(a,1,2,2,2)),rewrite(24796(7),10928(7))]. given #581 (T,wt=15): 26839 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,y)))) = c_0. [para(11(a,1),26574(a,1,1,2,2)),rewrite(24796(6))]. given #582 (T,wt=15): 26840 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(15207(a,1),26574(a,1,2,2)),rewrite(9914(4,R),24796(4),24796(8),9914(8),24796(8))]. given #583 (A,wt=31): 23242 f(f(f(x,x),f(y,f(y,f(x,x)))),f(f(x,y),f(c_0,f(f(x,x),f(y,f(x,x)))))) = f(x,x). [para(22622(a,1),17518(a,1,2,2,2,1,2)),rewrite(7716(11),15202(11))]. given #584 (F,wt=19): 26767 f(f(x,f(y,f(y,f(x,f(x,z))))),f(c_0,f(x,z))) = c_0 # label(false). [para(7716(a,1),26619(a,1,2,2))]. given #585 (F,wt=19): 26776 f(f(c_0,f(x,y)),f(f(x,f(x,y)),f(z,f(x,z)))) = c_0 # label(false). [para(25084(a,1),26619(a,1,1,2,2,2)),rewrite(24796(3),25084(14),24796(9),7716(9),24796(9))]. given #586 (F,wt=19): 26893 f(f(x,f(y,f(y,f(z,x)))),f(c_0,f(x,f(z,x)))) = c_0 # label(false). [para(11(a,1),26654(a,1,1,2,2)),rewrite(24796(3),11(7),24796(6),24796(9))]. given #587 (F,wt=19): 26907 f(f(c_0,f(x,y)),f(f(y,f(x,y)),f(z,f(y,z)))) = c_0 # label(false). [para(26378(a,1),26654(a,1,1,2))]. given #588 (T,wt=15): 26844 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,x)))) = c_0. [para(26574(a,1),24836(a,1,2,2,2,2,2)),rewrite(24796(11),543(11),24796(12),10928(12),10928(10))]. given #589 (T,wt=15): 26861 f(f(x,y),f(x,f(z,f(c_0,f(x,y))))) = x. [back_rewrite(25715),rewrite(26840(16),24796(10),10928(10),7716(8))]. given #590 (T,wt=15): 26871 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0. [para(11(a,1),26575(a,1,1))]. given #591 (T,wt=15): 27143 f(f(c_0,c_0),f(x,f(y,f(c_0,f(z,x))))) = c_0. [para(26575(a,1),26893(a,1,1,2,2)),rewrite(24796(7),9861(7),24796(5),18693(17),24796(9))]. given #592 (A,wt=25): 23394 f(f(c_0,f(x,f(x,y))),f(x,f(f(x,f(x,y)),f(y,f(x,f(x,y)))))) = c_0. [para(22622(a,1),22633(a,1,1,2)),rewrite(22622(11),15202(10))]. given #593 (F,wt=19): 26927 f(f(x,x),f(f(x,y),f(z,f(z,f(x,f(x,y)))))) = c_0 # label(false). [para(7716(a,1),26690(a,1,1,2,2)),rewrite(24796(5),15207(5),24796(2),9914(2),7716(4),24796(5))]. given #594 (F,wt=19): 26928 f(f(x,x),f(f(x,f(x,y)),f(z,f(z,f(x,y))))) = c_0 # label(false). [para(15207(a,1),26690(a,1,1,2)),rewrite(24796(2),9914(2),24796(5))]. given #595 (F,wt=19): 27076 f(f(x,x),f(f(y,x),f(z,f(z,f(x,f(y,x)))))) = c_0 # label(false). [para(11(a,1),26767(a,1,1,2,2,2,2)),rewrite(24796(3),11(10),24796(8),9914(8),24796(8))]. given #596 (F,wt=19): 27084 f(f(x,x),f(f(x,f(y,x)),f(z,f(z,f(y,x))))) = c_0 # label(false). [para(11(a,1),26776(a,1,2,1,2)),rewrite(11(4),24796(2),9914(2),24796(3),24796(5))]. given #597 (T,wt=15): 27148 f(f(c_0,c_0),f(x,f(y,f(c_0,f(x,z))))) = c_0. [para(26840(a,1),26893(a,1,1,2,2)),rewrite(24796(7),9861(7),24796(5),18693(17),24796(9))]. given #598 (T,wt=15): 27189 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x). [para(11(a,1),26861(a,1,2,2,2,2)),rewrite(11(3),24796(3),9914(3))]. given #599 (T,wt=17): 24306 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(x,z)))) = x. [para(15201(a,1),15217(a,1,1)),rewrite(15201(5),7716(6))]. given #600 (T,wt=15): 27347 f(f(x,x),f(c_0,f(f(x,y),f(x,z)))) = x. [para(24306(a,1),26375(a,1,2,2)),rewrite(24796(7),9914(7),24796(7),24306(15))]. given #601 (A,wt=29): 24807 f(x,f(c_0,f(f(x,y),f(f(z,f(c_0,f(x,y))),f(c_0,f(f(x,y),f(z,f(x,z)))))))) = c_0 # label(false). [para(19147(a,1),19163(a,1,2,2,1)),rewrite(24796(15),24796(16),24796(17),24803(18),24796(6),24796(21),24796(22),24796(23),24803(24),24796(11))]. given #602 (F,wt=19): 27163 f(f(x,f(y,f(y,f(x,f(z,x))))),f(c_0,f(z,x))) = c_0 # label(false). [para(26378(a,1),26907(a,1,1,2)),rewrite(26378(8),24796(7),15257(7),24796(6),24796(9))]. given #603 (F,wt=23): 27152 f(x,f(f(y,f(y,f(z,f(x,x)))),f(f(x,x),f(z,f(x,x))))) = c_0 # label(false). [para(607(a,1),26907(a,1,1,2)),rewrite(9861(3),607(5),24796(4),24796(7),24796(9))]. given #604 (F,wt=23): 27226 f(x,f(f(y,f(x,x)),f(z,f(z,f(f(x,x),f(y,f(x,x))))))) = c_0 # label(false). [para(11(a,1),26927(a,1,1)),rewrite(24796(2),24796(5))]. given #605 (F,wt=25): 26437 f(x,f(f(y,f(c_0,f(z,x))),f(x,f(f(y,f(y,x)),f(z,x))))) = f(z,x) # label(false). [para(26292(a,1),24796(a,2)),rewrite(24796(6),24796(8),24796(11))]. given #606 (T,wt=17): 24844 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,y))))) = y. [para(19147(a,1),15217(a,1,2,2,2)),rewrite(24796(6))]. given #607 (T,wt=17): 24916 f(f(x,f(x,y)),f(f(z,x),f(x,y))) = f(x,y). [back_rewrite(24616),rewrite(24796(4),24796(9),15207(9),24796(6))]. given #608 (T,wt=15): 27498 f(f(x,f(y,x)),f(x,f(z,f(y,x)))) = x. [para(11(a,1),24916(a,1,1,2)),rewrite(24796(2),11(7),24796(5),11(9))]. given #609 (T,wt=15): 27502 f(f(x,f(x,y)),f(x,f(z,f(x,y)))) = x. [para(15207(a,1),24916(a,1,1,2)),rewrite(24796(2),15207(8),24796(5),15207(10))]. given #610 (A,wt=59): 24825 f(f(c_0,f(x,y)),f(f(f(c_0,f(x,y)),f(f(z,f(c_0,f(x,y))),f(f(x,y),f(u,f(x,y))))),f(f(c_0,f(z,f(c_0,f(x,y)))),f(c_0,f(f(x,y),f(u,f(x,y))))))) = f(z,f(c_0,f(x,y))). [para(20677(a,1),19147(a,1,2,1,2,2,2)),rewrite(24796(8),24796(12),24796(14),24796(18),24796(23),24796(24),12185(24),24796(20),24796(24),24796(25),24796(29),24796(30),24796(35))]. given #611 (F,wt=27): 24852 f(f(x,y),f(c_0,f(x,f(f(z,f(x,x)),f(c_0,f(x,f(z,f(z,f(x,y))))))))) = c_0 # label(false). [back_rewrite(24791),rewrite(24796(12),24796(13),24796(14),24796(15),24803(15),24796(4),24796(7),24796(9))]. given #612 (F,wt=27): 25481 f(f(x,y),f(c_0,f(y,f(f(z,f(y,y)),f(c_0,f(y,f(z,f(z,f(x,y))))))))) = c_0 # label(false). [back_rewrite(20861),rewrite(24796(5),24796(9),15207(9),24796(4),24796(9),24796(13),15207(13),24796(8),24796(9))]. given #613 (F,wt=27): 26360 f(f(c_0,f(x,f(x,y))),f(f(z,f(x,x)),f(c_0,f(x,f(z,f(z,f(x,y))))))) = c_0 # label(false). [para(24836(a,1),24805(a,1,2,2,2)),rewrite(24796(12),24796(14))]. given #614 (F,wt=27): 26658 f(f(f(x,y),f(z,f(x,z))),f(f(x,f(x,y)),f(z,f(x,z)))) = f(z,f(x,z)) # label(false). [para(26613(a,1),25164(a,1,2,2,2,2,2)),rewrite(9914(9,R),24796(8),15683(9),24796(11),10928(13))]. given #615 (T,wt=15): 27512 f(f(x,y),f(x,f(z,f(x,f(x,y))))) = x. [para(25084(a,1),24916(a,1,1,2)),rewrite(24796(3),7716(3),25084(10),24796(5),25084(12))]. given #616 (T,wt=15): 27564 f(f(x,y),f(y,f(z,f(y,f(x,y))))) = y. [para(26378(a,1),27502(a,1,1))]. given #617 (T,wt=17): 24927 f(f(x,f(y,x)),f(f(y,x),f(x,z))) = f(y,x). [back_rewrite(24578),rewrite(24796(6),9850(7,R),24796(7),10806(7),24796(6))]. given #618 (T,wt=17): 24934 f(f(x,f(x,y)),f(f(x,z),f(x,y))) = f(x,y). [back_rewrite(24565),rewrite(24796(2),24796(4),24796(6),24796(7))]. given #619 (A,wt=23): 24829 f(x,f(f(y,f(x,y)),f(x,f(y,f(x,y))))) = f(x,f(y,f(x,y))). [para(20684(a,1),19147(a,1,2,1)),rewrite(24796(8),10806(10))]. given #620 (F,wt=27): 26693 f(f(f(x,y),f(z,f(y,z))),f(f(y,f(x,y)),f(z,f(y,z)))) = f(z,f(y,z)) # label(false). [para(26614(a,1),25164(a,1,2,2,2,2,2)),rewrite(9914(9,R),24796(8),15683(9),24796(11),10928(13))]. given #621 (F,wt=27): 27613 f(f(c_0,f(x,y)),f(f(z,f(x,x)),f(c_0,f(x,f(z,f(z,f(x,f(x,y)))))))) = c_0 # label(false). [para(7716(a,1),26360(a,1,1,2))]. given #622 (F,wt=27): 27620 f(f(c_0,f(x,y)),f(f(z,f(y,y)),f(c_0,f(y,f(z,f(z,f(y,f(x,y)))))))) = c_0 # label(false). [para(26378(a,1),26360(a,1,1,2))]. given #623 (F,wt=27): 27636 f(f(f(x,f(x,y)),f(y,z)),f(f(x,f(x,y)),f(y,f(y,z)))) = f(x,f(x,y)) # label(false). [para(26658(a,1),10928(a,1,2,2)),rewrite(24796(3),10928(6),24796(4),24796(6),24796(9),24796(11)),flip(a)]. given #624 (T,wt=17): 24947 f(f(x,f(x,y)),f(f(x,y),f(x,z))) = f(x,y). [back_rewrite(24515),rewrite(24796(6),9850(7,R),24796(7),10806(7),24796(6))]. given #625 (T,wt=17): 25808 f(f(c_0,f(x,f(x,y))),f(c_0,f(y,f(z,z)))) = c_0. [back_rewrite(19066),rewrite(24796(2))]. given #626 (T,wt=15): 27955 f(f(c_0,f(x,f(x,y))),f(c_0,f(y,z))) = c_0. [para(11(a,1),25808(a,1,2,2,2))]. given #627 (T,wt=15): 27956 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(11(a,1),25808(a,1,2,2)),rewrite(24796(7),9914(7),24796(7))]. given #628 (A,wt=53): 24847 f(f(f(x,y),f(y,z)),f(f(f(y,y),f(c_0,f(u,f(f(x,y),f(y,z))))),f(f(f(x,y),f(y,z)),f(y,f(u,f(f(x,y),f(y,z))))))) = f(u,f(f(x,y),f(y,z))). [para(24461(a,1),19147(a,1,2,1,2,2,2)),rewrite(24796(8),24796(13),9861(13),24796(11),9914(11),24796(11),24796(17),24576(17),24796(14),9861(14),24796(15),24796(20),24796(26))]. given #629 (F,wt=19): 27964 f(x,f(f(y,f(x,y)),f(x,f(z,z)))) = f(x,f(z,z)) # label(false). [para(25808(a,1),26348(a,1,2,1)),rewrite(24796(3),24796(7),24796(10),15683(10),24796(7),10928(7),10806(9))]. given #630 (F,wt=19): 28094 f(f(c_0,f(x,f(x,y))),f(f(z,f(z,x)),f(x,y))) = c_0 # label(false). [para(26386(a,1),27956(a,1,2,2,2)),rewrite(9914(13,R),24796(8),10928(8),24796(9))]. given #631 (F,wt=15): 28198 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z) # label(false). [para(28094(a,1),25164(a,1,2,2,2,2,2)),rewrite(9914(11,R),24796(11),24796(12),20688(12),24796(13),10928(13),15207(10),24796(7),9914(7),9861(7),24796(5))]. given #632 (F,wt=23): 28133 f(x,f(c_0,f(f(x,f(y,y)),f(f(z,f(x,z)),f(x,f(y,y)))))) = c_0 # label(false). [para(27964(a,1),15683(a,1,2,2,2)),rewrite(24796(9))]. given #633 (T,wt=15): 28014 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(15207(a,1),27955(a,1,2,2)),rewrite(24796(7),9914(7),24796(7))]. given #634 (T,wt=15): 28016 f(x,f(c_0,f(y,f(c_0,f(z,f(x,z)))))) = c_0. [para(15683(a,1),27955(a,1,1,2,2)),rewrite(9914(3),9861(3),24796(6))]. given #635 (T,wt=15): 28019 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,z)))) = c_0. [para(27955(a,1),24836(a,1,2,2,2,2,2)),rewrite(24796(5),24796(11),543(11),24796(8),24796(12),10928(12),10928(10))]. given #636 (T,wt=15): 28082 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0. [para(11(a,1),27956(a,1,1))]. given #637 (A,wt=31): 24848 f(f(x,y),f(x,f(f(c_0,f(z,f(z,f(x,x)))),f(f(x,y),f(c_0,f(z,f(z,f(x,x)))))))) = x # label(false). [para(19147(a,1),19145(a,1,2,1,2,1)),rewrite(24796(12),24796(13),24796(14),24796(15),24803(15),24796(4),24796(10),24796(15))]. given #638 (F,wt=29): 24881 f(x,f(c_0,f(f(y,x),f(f(z,f(c_0,f(y,x))),f(c_0,f(f(y,x),f(z,f(x,z)))))))) = c_0 # label(false). [back_rewrite(24705),rewrite(24796(6),24796(11),24796(18),24796(19),24796(24),24796(25),24796(27),24796(29),24796(31),24865(31),24796(16))]. given #639 (F,wt=29): 25180 f(f(x,f(y,y)),f(f(y,z),f(c_0,f(f(y,y),f(z,f(z,f(x,f(y,y)))))))) = f(y,y) # label(false). [back_rewrite(23439),rewrite(24796(2),24796(6),15207(6),24796(6),24796(7),24796(10))]. given #640 (F,wt=29): 26387 f(f(c_0,f(x,f(x,y))),f(f(z,f(c_0,f(x,y))),f(c_0,f(f(z,f(z,x)),f(x,y))))) = c_0 # label(false). [para(24878(a,1),24805(a,1,2,2,2)),rewrite(24796(7),24796(9),24796(16))]. given #641 (F,wt=27): 28505 f(f(c_0,f(x,f(y,x))),f(f(z,f(x,x)),f(c_0,f(x,f(z,f(z,f(y,x))))))) = c_0 # label(false). [para(11(a,1),26387(a,1,1,2,2)),rewrite(24796(3),11(8),24796(6),9914(6),11(13),24796(11))]. given #642 (T,wt=15): 28122 f(f(c_0,c_0),f(x,f(f(y,z),f(z,u)))) = c_0. [para(24847(a,1),26414(a,1,2))]. given #643 (T,wt=15): 28292 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,z)))) = c_0. [para(11(a,1),28014(a,1,2,2,2,2)),rewrite(9914(3,R),24796(3),24796(5))]. given #644 (T,wt=15): 28299 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0. [para(28016(a,1),24836(a,1,2,2,2,2,2)),rewrite(24796(3),9883(11),9914(12),9861(12),24796(10),9914(10),9861(10),24796(8))]. given #645 (T,wt=15): 28554 f(f(c_0,c_0),f(x,f(f(y,y),f(z,u)))) = c_0. [para(10928(a,1),28122(a,1,2,2,2)),rewrite(9914(5))]. given #646 (A,wt=43): 24857 f(f(x,y),f(f(c_0,f(y,f(x,f(c_0,f(f(x,z),f(x,f(x,y))))))),f(f(y,y),f(c_0,f(x,f(c_0,f(f(x,z),f(x,f(x,y))))))))) = y. [back_rewrite(24776),rewrite(24796(5),24796(8),24796(15),24796(18),24796(21),24796(23))]. given #647 (F,wt=29): 26394 f(f(c_0,f(x,f(y,x))),f(f(z,f(c_0,f(y,x))),f(c_0,f(f(z,f(z,x)),f(y,x))))) = c_0 # label(false). [para(25178(a,1),24805(a,1,2,2,2)),rewrite(24796(7),24796(9),24796(16))]. given #648 (F,wt=29): 26438 f(f(c_0,f(x,f(y,x))),f(f(z,f(c_0,f(y,x))),f(x,f(f(z,f(z,x)),f(y,x))))) = c_0 # label(false). [para(26292(a,1),24805(a,1,2,2,2)),rewrite(24796(6),24796(8),24796(15))]. given #649 (F,wt=15): 28698 f(x,f(f(y,f(y,x)),f(z,x))) = f(z,x) # label(false). [para(26438(a,1),26618(a,1,2,2,2)),rewrite(24796(21),10928(21),24796(18),27498(18),24796(11),26437(11)),flip(a)]. given #650 (F,wt=29): 27610 f(f(c_0,f(x,f(y,x))),f(f(z,f(c_0,f(y,x))),f(c_0,f(f(y,x),f(z,f(x,z)))))) = c_0 # label(false). [para(11(a,1),26360(a,1,1,2,2)),rewrite(24796(3),9914(7,R),24796(7),11(13),24796(11))]. given #651 (T,wt=15): 28642 f(f(c_0,c_0),f(x,f(f(y,z),f(u,v)))) = c_0. [para(12185(a,1),28554(a,1,2,2,1))]. given #652 (T,wt=17): 25875 f(x,f(f(y,x),f(c_0,f(z,f(x,x))))) = f(x,x). [back_rewrite(18672),rewrite(24796(4),24796(7))]. given #653 (T,wt=17): 25889 f(x,f(f(x,y),f(y,f(z,f(x,y))))) = f(x,y). [back_rewrite(18611),rewrite(24796(2),24796(4),24796(6),24796(8),24796(10),24796(11),25866(11),24796(1),24796(4),24796(5),15257(5),24796(2),24796(3),24796(7))]. given #654 (T,wt=17): 26244 f(f(x,y),f(c_0,f(f(x,z),f(x,f(x,y))))) = x. [back_rewrite(16216),rewrite(24796(5),24796(6))]. given #655 (A,wt=55): 24871 f(f(x,y),f(f(c_0,f(y,f(f(z,f(x,y)),f(c_0,f(z,f(f(x,y),f(z,f(x,y)))))))),f(f(y,y),f(c_0,f(f(z,f(x,y)),f(c_0,f(z,f(f(x,y),f(z,f(x,y)))))))))) = y. [back_rewrite(24730),rewrite(24796(4),24796(5),24796(7),24796(8),24796(9),24796(11),24796(17),24796(18),24796(20),24796(21),24796(22),24796(24),24796(27),24796(29))]. given #656 (F,wt=29): 27614 f(f(c_0,f(x,f(x,y))),f(f(z,f(c_0,f(x,y))),f(c_0,f(f(x,y),f(z,f(x,z)))))) = c_0 # label(false). [para(15207(a,1),26360(a,1,1,2,2)),rewrite(24796(3),9914(7,R),24796(7),15207(14),24796(11))]. given #657 (F,wt=29): 27857 f(f(x,x),f(f(y,f(c_0,f(x,z))),f(c_0,f(f(x,z),f(y,f(y,f(x,f(x,z)))))))) = c_0 # label(false). [para(11(a,1),27613(a,1,1,2)),rewrite(24796(2),9914(2),24796(2),24796(3),9914(4,R),24796(4),24796(7),24796(8),24796(9),24796(11),543(11),24796(9))]. given #658 (F,wt=29): 27860 f(f(x,x),f(f(y,f(c_0,f(z,x))),f(c_0,f(f(z,x),f(y,f(y,f(x,f(z,x)))))))) = c_0 # label(false). [para(11(a,1),27613(a,1,2,2,2,2,2,2,2)),rewrite(11(4),24796(2),9914(2),9914(4,R),24796(4),24796(9))]. given #659 (F,wt=31): 26621 f(f(x,f(y,f(y,f(x,z)))),f(f(x,f(x,z)),f(y,f(y,f(x,z))))) = f(y,f(y,f(x,z))) # label(false). [para(26605(a,1),25164(a,1,2,2,2,2,2)),rewrite(9914(12,R),24796(10),24805(11),24796(11),24796(12),10928(14))]. given #660 (T,wt=17): 26367 f(f(x,x),f(f(y,f(x,x)),f(c_0,f(x,z)))) = x. [para(11(a,1),18649(a,1,2,2,2,2)),rewrite(24796(3),24796(5),9914(11,R),24796(11),9861(11))]. given #661 (T,wt=17): 26446 f(f(c_0,f(x,y)),f(f(x,y),f(z,u))) = f(x,y). [para(26414(a,1),24836(a,1,2,2,2,2,2)),rewrite(9914(9,R),24796(9),543(10),24796(11),9232(11),24796(8),10928(9),24796(7))]. given #662 (T,wt=17): 26447 f(f(c_0,f(x,y)),f(f(z,u),f(x,y))) = f(x,y). [para(26414(a,1),25164(a,1,2,2,2,2,2)),rewrite(9914(9,R),24796(9),543(10),24796(11),9232(11),24796(8),10928(9),24796(7))]. given #663 (T,wt=17): 26462 f(f(c_0,f(x,y)),f(c_0,f(f(x,y),f(z,u)))) = c_0. [para(26414(a,1),24937(a,1,1,2)),rewrite(24796(3))]. given #664 (A,wt=41): 24890 f(x,f(f(y,x),f(f(x,f(y,x)),f(x,f(f(c_0,f(z,f(z,f(x,x)))),f(f(y,x),f(c_0,f(z,f(z,f(x,x)))))))))) = f(y,x). [back_rewrite(24687),rewrite(24796(4),24796(7),24796(10),24796(15),24796(18),24796(20))]. given #665 (F,wt=31): 26819 f(f(c_0,f(x,f(y,f(x,y)))),f(f(x,y),f(z,f(z,f(c_0,f(x,f(y,f(x,y)))))))) = f(x,y) # label(false). [para(25479(a,1),26614(a,1,2,1)),rewrite(24796(2),24796(6),24796(8),24796(12),24796(17),26354(21))]. given #666 (F,wt=23): 29089 f(f(c_0,f(x,f(y,f(x,y)))),f(f(x,y),f(z,f(x,z)))) = f(x,y) # label(false). [para(27955(a,1),26819(a,1,2,2,2)),rewrite(24796(8),24796(12),10928(12))]. given #667 (F,wt=23): 29105 f(f(c_0,f(x,f(y,f(y,x)))),f(f(y,x),f(z,f(x,z)))) = f(y,x) # label(false). [para(24796(a,1),29089(a,1,1,2)),rewrite(24796(2),24796(4),24796(6),24796(11))]. given #668 (F,wt=27): 29106 f(f(f(x,y),f(z,f(x,z))),f(c_0,f(f(x,y),f(c_0,f(x,f(y,f(x,y))))))) = c_0 # label(false). [para(29089(a,1),24805(a,1,2,2,2)),rewrite(24796(12))]. given #669 (T,wt=17): 26709 f(x,f(f(x,y),f(f(x,x),f(z,u)))) = f(x,y). [para(26703(a,1),26613(a,1,2,2,2)),rewrite(24796(8),10928(8))]. given #670 (T,wt=17): 26721 f(x,f(f(y,f(x,x)),f(f(x,x),f(z,u)))) = c_0. [para(26716(a,1),24938(a,1,1,2,2)),rewrite(24796(6),26716(11),9861(9),24796(7))]. given #671 (T,wt=17): 26884 f(f(c_0,f(x,y)),f(c_0,f(f(x,x),f(z,u)))) = c_0. [para(26716(a,1),26575(a,1,2,2,2,2)),rewrite(9914(7,R),24796(5),9861(9),24796(7),24796(9))]. given #672 (T,wt=17): 27030 f(x,f(c_0,f(y,f(c_0,f(f(x,x),f(z,u)))))) = c_0. [para(26716(a,1),26839(a,1,1,2)),rewrite(9861(3),9914(8,R),24796(6))]. given #673 (A,wt=41): 24894 f(f(x,y),f(f(x,f(x,y)),f(x,f(f(c_0,f(z,f(z,f(x,x)))),f(f(x,y),f(c_0,f(z,f(z,f(x,x))))))))) = f(x,f(x,y)). [back_rewrite(24679),rewrite(24796(3),24796(9),24796(14),24796(15),24796(17),24796(18),24796(19),24796(20))]. given #674 (F,wt=27): 29218 f(f(f(x,y),f(z,f(y,z))),f(c_0,f(f(x,y),f(c_0,f(y,f(x,f(x,y))))))) = c_0 # label(false). [para(29105(a,1),24805(a,1,2,2,2)),rewrite(24796(12))]. given #675 (F,wt=27): 29257 f(f(f(x,f(x,y)),f(y,z)),f(c_0,f(f(y,z),f(c_0,f(y,f(z,f(y,z))))))) = c_0 # label(false). [para(24796(a,1),29106(a,1,1)),rewrite(24796(1))]. given #676 (F,wt=19): 29510 f(f(c_0,f(x,y)),f(f(z,f(z,x)),f(x,f(x,y)))) = c_0 # label(false). [para(15207(a,1),29257(a,1,2,2,2,2,2)),rewrite(9861(11),24796(9),7716(9),24796(9))]. given #677 (F,wt=19): 29536 f(f(x,x),f(f(y,f(y,f(x,z))),f(x,f(x,z)))) = c_0 # label(false). [para(24844(a,1),29257(a,1,2,2)),rewrite(24796(5),24796(8),9914(8),24796(8))]. given #678 (T,wt=17): 27361 f(f(c_0,f(x,f(y,y))),f(f(y,z),f(y,u))) = c_0. [para(24306(a,1),26575(a,1,2,2,2,2)),rewrite(9914(11,R),24796(7),10928(7),24796(6),9914(6),24796(8))]. given #679 (T,wt=17): 27367 f(f(x,x),f(c_0,f(y,f(f(x,z),f(x,u))))) = c_0. [para(24306(a,1),26839(a,1,1,2)),rewrite(24796(2),9914(2),9914(13,R),24796(9),10928(9))]. given #680 (T,wt=17): 27516 f(f(x,f(x,y)),f(x,f(f(x,y),f(x,z)))) = x. [para(24916(a,1),25242(a,1,2,2,2)),rewrite(24796(3),24796(5),24796(9),15207(9),24796(6),24796(12),24796(14),24947(15),24796(11),15207(11))]. given #681 (T,wt=17): 27534 f(x,f(f(x,y),f(z,f(x,f(x,y))))) = f(x,y). [para(24916(a,1),24916(a,1,1,2)),rewrite(24796(4),15207(4),24796(6),24796(8),24947(9),24796(5),24796(9),24796(11),24947(12))]. given #682 (A,wt=55): 24897 f(f(x,y),f(y,f(f(c_0,f(f(z,f(y,y)),f(c_0,f(z,f(f(y,y),f(z,f(y,y))))))),f(f(x,y),f(c_0,f(f(z,f(y,y)),f(c_0,f(z,f(f(y,y),f(z,f(y,y))))))))))) = y. [back_rewrite(24658),rewrite(24796(4),24796(8),24796(10),24796(14),24796(17),24796(21),24796(23),24796(29))]. given #683 (F,wt=31): 26820 f(f(x,y),f(f(z,f(z,f(x,y))),f(c_0,f(y,f(x,f(x,y)))))) = f(c_0,f(y,f(x,f(x,y)))) # label(false). [para(25479(a,1),26618(a,1,1)),rewrite(25479(12),24796(10))]. given #684 (F,wt=31): 26837 f(f(x,y),f(f(z,f(z,f(x,y))),f(c_0,f(x,f(y,f(x,y)))))) = f(c_0,f(x,f(y,f(x,y)))) # label(false). [para(26354(a,1),26618(a,1,1)),rewrite(26354(12),24796(10))]. given #685 (F,wt=31): 26954 f(f(f(x,y),f(z,f(x,z))),f(c_0,f(f(z,f(x,z)),f(f(x,f(x,y)),f(z,f(x,z)))))) = c_0 # label(false). [para(26613(a,1),26742(a,1,2,2,2,2,2)),rewrite(24796(12))]. given #686 (F,wt=31): 26956 f(f(f(x,y),f(z,f(y,z))),f(c_0,f(f(z,f(y,z)),f(f(y,f(x,y)),f(z,f(y,z)))))) = c_0 # label(false). [para(26614(a,1),26742(a,1,2,2,2,2,2)),rewrite(24796(12))]. given #687 (T,wt=17): 27705 f(x,f(f(y,x),f(z,f(x,f(y,x))))) = f(y,x). [para(11(a,1),27512(a,1,2,2,2,2)),rewrite(11(3),24796(3))]. given #688 (T,wt=17): 28106 f(f(c_0,f(x,f(y,x))),f(f(y,z),f(y,u))) = c_0. [para(24306(a,1),27956(a,1,2,2,2,2)),rewrite(9914(11,R),24796(7),10928(7),24796(5),24796(8))]. given #689 (T,wt=17): 28591 f(f(c_0,f(x,y)),f(c_0,f(f(y,y),f(z,u)))) = c_0. [para(26703(a,1),28292(a,1,2,2,2)),rewrite(24796(11),10928(11))]. given #690 (T,wt=17): 28592 f(x,f(c_0,f(y,f(y,f(f(x,x),f(z,u)))))) = c_0. [para(26716(a,1),28292(a,1,1,2)),rewrite(9861(3),24796(5))]. given #691 (A,wt=47): 24898 f(f(x,f(c_0,f(y,z))),f(f(c_0,f(y,z)),f(f(c_0,f(u,f(u,f(y,z)))),f(f(x,f(c_0,f(y,z))),f(c_0,f(u,f(u,f(y,z)))))))) = f(c_0,f(y,z)). [back_rewrite(24657),rewrite(24796(7),24796(13),24796(16),24796(24))]. given #692 (F,wt=31): 27119 f(f(f(x,f(x,y)),f(z,f(x,z))),f(c_0,f(f(z,f(x,z)),f(f(x,y),f(z,f(x,z)))))) = c_0 # label(false). [para(26776(a,1),26742(a,1,2,2,2,2,2)),rewrite(24796(15),10928(15),24796(12))]. given #693 (F,wt=31): 27138 f(f(f(x,f(x,y)),f(y,f(y,z))),f(c_0,f(f(x,f(x,y)),f(f(x,f(x,y)),f(y,z))))) = c_0 # label(false). [para(26613(a,1),26893(a,1,1,2,2)),rewrite(24796(1),24796(7),24796(10),24796(12))]. given #694 (F,wt=31): 27151 f(f(f(x,f(x,y)),f(y,z)),f(c_0,f(f(x,f(x,y)),f(f(x,f(x,y)),f(y,f(y,z)))))) = c_0 # label(false). [para(26776(a,1),26893(a,1,1,2,2)),rewrite(24796(1),24796(7),10928(7),24796(6),24796(10),24796(12))]. given #695 (F,wt=31): 27271 f(f(x,f(y,f(x,y))),f(f(x,y),f(z,f(z,f(f(x,y),f(c_0,f(x,f(y,f(x,y))))))))) = c_0 # label(false). [para(25479(a,1),27076(a,1,2,1)),rewrite(24796(2),24796(7),9914(11,R),24796(7),10928(7),24796(4),24796(6),24796(11),26354(15),24796(11))]. given #696 (T,wt=17): 28617 f(f(c_0,f(x,f(y,y))),f(f(z,y),f(y,u))) = c_0. [para(24936(a,1),28299(a,1,2,2,2,2,2)),rewrite(24796(8),9861(8),24796(6),9914(6),24796(8))]. given #697 (T,wt=17): 29632 f(f(c_0,c_0),f(x,f(y,f(f(x,z),f(x,u))))) = c_0. [para(27367(a,1),26893(a,1,1,2,2)),rewrite(24796(7),9861(7),24796(5),18693(17),24796(9))]. given #698 (T,wt=17): 29648 f(f(c_0,f(x,y)),f(x,f(f(x,y),f(x,z)))) = c_0. [para(27516(a,1),24805(a,1,2,2,2)),rewrite(24796(8),7716(8),24796(8))]. given #699 (T,wt=17): 29944 f(f(c_0,f(x,f(x,y))),f(f(y,z),f(y,u))) = c_0. [para(28106(a,1),7716(a,1,2,2)),rewrite(24796(2),24796(6),24796(10),10928(10),24796(7),18693(7),24796(3)),flip(a)]. given #700 (A,wt=27): 24915 f(f(x,y),f(x,f(f(f(z,x),f(x,u)),f(f(x,y),f(f(z,x),f(x,u)))))) = x. [back_rewrite(24617),rewrite(24796(4),24796(10),24796(11),24796(12))]. given #701 (F,wt=31): 27288 f(f(c_0,f(x,f(x,y))),f(f(y,f(y,z)),f(f(x,f(x,y)),f(f(x,f(x,y)),f(y,z))))) = c_0 # label(false). [para(26613(a,1),27084(a,1,2,2,2)),rewrite(24796(1),24796(3),9914(5,R),24796(4),24796(5),24796(8),24796(10),24796(14))]. given #702 (F,wt=31): 27292 f(f(x,f(y,f(x,y))),f(f(z,f(z,f(x,y))),f(f(x,y),f(c_0,f(x,f(y,f(x,y))))))) = c_0 # label(false). [para(25479(a,1),27084(a,1,2,1,2)),rewrite(24796(2),24796(7),9914(11,R),24796(7),10928(7),24796(5),24796(9),24796(10),24796(12),26354(16),24796(14))]. given #703 (F,wt=31): 27299 f(f(c_0,f(x,f(x,y))),f(f(y,z),f(f(x,f(x,y)),f(f(x,f(x,y)),f(y,f(y,z)))))) = c_0 # label(false). [para(26776(a,1),27084(a,1,2,2,2)),rewrite(24796(1),24796(3),9914(5,R),24796(4),24796(5),24796(9),24796(11),24796(17),10928(17),24796(14))]. given #704 (F,wt=31): 27628 f(f(c_0,f(x,y)),f(f(z,f(c_0,f(x,f(x,y)))),f(c_0,f(f(x,f(x,y)),f(z,f(x,z)))))) = c_0 # label(false). [para(24306(a,1),26360(a,1,1,2,2)),rewrite(24796(4),7716(4),9914(8,R),24796(7),24306(19),24796(12))]. given #705 (T,wt=17): 30094 f(f(c_0,c_0),f(x,f(x,f(f(y,y),f(z,u))))) = c_0. [para(28592(a,1),20685(a,1,2,2)),rewrite(24796(9))]. given #706 (T,wt=15): 30663 f(f(c_0,c_0),f(x,f(x,f(c_0,f(y,z))))) = c_0. [para(9883(a,1),30094(a,1,2,2,2,1))]. given #707 (T,wt=17): 30311 f(f(c_0,f(x,y)),f(y,f(f(x,y),f(y,z)))) = c_0. [para(24796(a,1),29648(a,1,1,2)),rewrite(24796(4))]. given #708 (T,wt=15): 30672 f(f(c_0,c_0),f(x,f(y,f(c_0,f(z,u))))) = c_0. [para(26409(a,1),30311(a,1,1,2)),rewrite(26409(15),24796(13),26375(15))]. given #709 (A,wt=25): 24920 f(f(x,f(y,f(y,x))),f(f(y,x),f(z,f(c_0,f(x,f(y,f(y,x))))))) = c_0. [back_rewrite(24598),rewrite(24796(5),24796(7),24796(11),24796(12))]. given #710 (F,wt=31): 27630 f(f(x,x),f(f(y,f(c_0,f(x,f(x,z)))),f(c_0,f(f(x,f(x,z)),f(y,f(y,f(x,z))))))) = c_0 # label(false). [para(24916(a,1),26360(a,1,1,2,2)),rewrite(24796(5),15207(5),24796(2),9914(2),9914(6,R),24796(5),24796(12),24796(14),24947(15))]. given #711 (F,wt=31): 27632 f(f(x,f(y,f(y,f(z,x)))),f(f(x,f(z,x)),f(y,f(y,f(z,x))))) = f(y,f(y,f(z,x))) # label(false). [para(11(a,1),26658(a,1,2,1,2)),rewrite(11(3),24796(2),24796(6),24796(8),24796(13))]. given #712 (F,wt=23): 30792 f(f(x,x),f(f(x,x),f(f(y,f(y,f(z,x))),f(x,f(z,x))))) = x # label(false). [para(27084(a,1),27632(a,2,2)),rewrite(24796(11),24796(23),24796(32),26621(36),24796(13),9861(13))]. given #713 (F,wt=19): 30816 f(f(x,x),f(f(y,f(y,f(z,x))),f(x,f(z,x)))) = c_0 # label(false). [para(30792(a,1),24805(a,1,2,2)),rewrite(24796(8),9914(8),24796(8))]. given #714 (T,wt=17): 30699 f(f(c_0,c_0),f(x,f(y,f(f(z,u),f(v,w))))) = c_0. [para(28642(a,1),30311(a,1,1,2)),rewrite(28642(15),24796(13),26375(15))]. given #715 (T,wt=17): 30714 f(f(c_0,c_0),f(x,f(y,f(z,f(c_0,f(u,v)))))) = c_0. [para(30672(a,1),30311(a,1,1,2)),rewrite(30672(17),24796(15),26375(17))]. given #716 (T,wt=19): 24953 f(f(x,y),f(f(x,z),f(x,f(x,y)))) = f(x,f(x,y)). [back_rewrite(24457),rewrite(24796(1),24796(4),24796(6),9850(9,R),24796(7),24796(9),10808(9),24796(5),24796(6),24796(7))]. given #717 (T,wt=19): 24999 f(f(x,f(x,y)),f(c_0,f(x,f(z,f(x,y))))) = f(x,y). [back_rewrite(24320),rewrite(24796(1),24796(4),24796(5),24796(9))]. given #718 (A,wt=21): 24921 f(f(x,y),f(f(z,f(c_0,f(x,y))),f(u,f(c_0,f(x,y))))) = c_0. [back_rewrite(24597),rewrite(24796(8),24796(11))]. given #719 (F,wt=31): 27877 f(f(c_0,f(x,y)),f(f(z,f(c_0,f(y,f(x,y)))),f(c_0,f(f(y,f(x,y)),f(z,f(y,z)))))) = c_0 # label(false). [para(24927(a,1),27613(a,1,1,2)),rewrite(9914(8,R),24796(7),24927(19),24796(15),15257(15),24796(12))]. given #720 (F,wt=31): 27880 f(f(x,x),f(f(y,f(c_0,f(x,f(z,x)))),f(c_0,f(f(x,f(z,x)),f(y,f(y,f(z,x))))))) = c_0 # label(false). [para(15257(a,1),27620(a,1,2,2,2,2,2,2,2)),rewrite(15257(5),24796(2),9914(2),9914(6,R),24796(5),24796(12),26378(12))]. given #721 (F,wt=31): 27900 f(f(x,f(y,f(y,f(z,x)))),f(f(y,f(y,f(z,x))),f(x,f(z,x)))) = f(y,f(y,f(z,x))) # label(false). [para(11(a,1),27636(a,1,1,2)),rewrite(24796(4),11(11),24796(9))]. given #722 (F,wt=31): 27902 f(f(x,f(y,f(y,f(x,z)))),f(f(y,f(y,f(x,z))),f(x,f(x,z)))) = f(y,f(y,f(x,z))) # label(false). [para(15207(a,1),27636(a,1,1,2)),rewrite(24796(4),15207(12),24796(9))]. given #723 (T,wt=17): 30879 f(f(x,f(y,x)),f(c_0,f(f(y,x),f(x,z)))) = x. [para(11(a,1),24999(a,1,1,2)),rewrite(24796(2),11(7),24796(5),11(11))]. given #724 (T,wt=15): 31038 f(f(x,x),f(c_0,f(f(y,x),f(x,z)))) = x. [para(30879(a,1),26375(a,1,2,2)),rewrite(24796(7),9914(7),24796(7),30879(15))]. given #725 (T,wt=17): 31062 f(f(c_0,f(x,f(y,x))),f(f(z,y),f(y,u))) = c_0. [para(30879(a,1),27956(a,1,2,2,2,2)),rewrite(9914(11,R),24796(7),10928(7),24796(5),24796(8))]. given #726 (T,wt=19): 25181 f(f(x,y),f(f(x,f(y,y)),f(c_0,f(y,f(x,y))))) = y. [back_rewrite(23437),rewrite(24796(1),24796(4),15207(4),24796(3))]. given #727 (A,wt=51): 24922 f(f(f(x,y),f(y,z)),f(c_0,f(f(u,f(f(x,y),f(y,z))),f(f(c_0,f(y,f(u,f(f(x,y),f(y,z))))),f(f(y,y),f(c_0,f(u,f(f(x,y),f(y,z))))))))) = c_0. [back_rewrite(24592),rewrite(24796(8),24796(13),24796(16),24796(21),24796(24))]. given #728 (F,wt=27): 31183 f(f(c_0,f(x,y)),f(x,f(z,f(z,f(f(y,f(x,x)),f(c_0,f(x,f(x,y)))))))) = c_0 # label(false). [para(25181(a,1),29218(a,1,1,1)),rewrite(24796(4),24796(8),24796(12),24796(16),25631(20),24796(16),24796(20),24796(21),24796(25),25631(29),24796(21),24796(22),20676(22),10928(17),7716(14),24796(14))]. given #729 (F,wt=27): 31221 f(f(x,f(x,y)),f(x,f(z,f(z,f(f(y,f(x,x)),f(c_0,f(x,f(x,y)))))))) = x # label(false). [para(31183(a,1),24836(a,1,2,2,2,2,2)),rewrite(24796(15),10801(15),24796(17),10928(17),10928(16),24796(13))]. given #730 (F,wt=29): 31282 f(f(x,y),f(x,f(z,f(z,f(f(c_0,f(x,y)),f(f(x,x),f(y,f(x,f(x,y))))))))) = x # label(false). [para(25165(a,1),31221(a,1,1,2)),rewrite(24796(1),7716(3),24796(2),24796(6),24796(8),25242(11),7716(10),24796(10))]. given #731 (F,wt=29): 31327 f(f(x,y),f(y,f(z,f(z,f(f(c_0,f(x,y)),f(f(y,y),f(x,f(y,f(x,y))))))))) = y # label(false). [para(24796(a,1),31282(a,1,1)),rewrite(24796(3),24796(6))]. given #732 (T,wt=19): 25495 f(x,f(c_0,f(f(x,y),f(c_0,f(y,f(x,f(x,y))))))) = c_0. [back_rewrite(20805),rewrite(24796(6),24796(10))]. given #733 (T,wt=19): 25631 f(f(x,y),f(f(y,f(x,x)),f(c_0,f(x,f(x,y))))) = x. [back_rewrite(19900),rewrite(24796(2),9850(3,R),24796(4),10806(4),24796(3))]. given #734 (T,wt=19): 25868 f(f(x,y),f(x,f(f(x,z),f(f(x,y),f(x,z))))) = x. [back_rewrite(18754),rewrite(24796(5),24796(9),24796(10),24796(12),25838(12),9850(3,R),24796(4),10806(4),24796(7))]. given #735 (T,wt=19): 26163 f(x,f(c_0,f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y). [back_rewrite(16970),rewrite(24796(2),24796(4),24796(6),24796(8),24796(11),25866(11),24796(5))]. given #736 (A,wt=49): 24926 f(f(c_0,f(f(x,y),f(c_0,f(f(x,x),f(y,f(y,f(z,f(x,x)))))))),f(f(x,x),f(u,f(f(x,y),f(c_0,f(f(x,x),f(y,f(y,f(z,f(x,x)))))))))) = c_0. [back_rewrite(24582),rewrite(24796(6),24796(9),24796(12),24796(19),24796(22),24796(26))]. given #737 (F,wt=31): 28140 f(x,f(f(y,f(c_0,f(x,f(z,z)))),f(c_0,f(f(y,f(x,y)),f(x,f(z,z)))))) = f(x,f(z,z)) # label(false). [para(27964(a,1),24878(a,1,2,1,2,2)),rewrite(24796(11),26613(12),24796(11),24796(19),26613(20))]. given #738 (F,wt=31): 28316 f(x,f(c_0,f(f(x,f(c_0,f(y,f(y,z)))),f(f(z,f(x,z)),f(x,f(c_0,f(y,f(y,z)))))))) = c_0 # label(false). [para(28016(a,1),24807(a,1,2,2,2,1)),rewrite(24796(3),24796(10),24796(16),10928(18))]. given #739 (F,wt=31): 28536 f(f(c_0,f(x,f(x,f(c_0,f(y,f(y,z)))))),f(f(z,f(x,z)),f(x,f(c_0,f(y,f(y,z)))))) = c_0 # label(false). [para(28016(a,1),26387(a,1,2,1)),rewrite(24796(3),24796(11),24796(14),10928(20))]. given #740 (F,wt=31): 28877 f(f(x,x),f(f(x,y),f(f(c_0,f(z,f(x,z))),f(f(x,f(x,y)),f(c_0,f(z,f(x,z))))))) = c_0 # label(false). [para(27955(a,1),27857(a,1,2,1)),rewrite(24796(6),24796(10),24796(15),10928(19))]. given #741 (T,wt=19): 26179 f(f(x,y),f(y,f(f(y,z),f(f(x,y),f(y,z))))) = y. [back_rewrite(16847),rewrite(24796(2),24796(5),15207(5),9850(3,R),24796(4),10808(4),24796(7))]. given #742 (T,wt=19): 26448 f(f(c_0,f(x,y)),f(f(z,f(x,y)),f(u,f(x,y)))) = c_0. [para(12185(a,1),24917(a,1,2,1,2)),rewrite(9914(12,R),24796(10),10928(10))]. given #743 (T,wt=19): 26560 f(x,f(c_0,f(f(x,f(x,y)),f(y,f(x,f(x,y)))))) = c_0. [para(25165(a,1),15683(a,1,2,2,2)),rewrite(24796(2),24796(5),24796(7))]. given #744 (T,wt=19): 26583 f(x,f(f(y,f(x,x)),f(x,f(z,z)))) = f(x,f(z,z)). [para(19404(a,1),26348(a,1,2,1)),rewrite(24796(10),10827(10),24796(7),10928(7),10806(9))]. given #745 (A,wt=49): 24931 f(f(c_0,f(f(x,f(c_0,f(y,z))),f(c_0,f(f(y,z),f(x,f(z,x)))))),f(f(y,z),f(u,f(f(x,f(c_0,f(y,z))),f(c_0,f(f(y,z),f(x,f(z,x)))))))) = c_0. [back_rewrite(24569),rewrite(24796(5),24796(10),24796(13),24796(19),24796(24),24796(28))]. given #746 (F,wt=31): 28907 f(f(x,x),f(f(x,y),f(f(c_0,f(z,f(y,z))),f(f(x,f(x,y)),f(c_0,f(z,f(y,z))))))) = c_0 # label(false). [para(27955(a,1),27860(a,1,2,1)),rewrite(24796(4),24796(6),24796(10),24796(13),24796(15),10928(19))]. given #747 (F,wt=31): 29060 f(f(c_0,f(x,f(y,f(y,x)))),f(f(y,x),f(z,f(z,f(c_0,f(x,f(y,f(y,x)))))))) = f(y,x) # label(false). [para(24796(a,1),26819(a,1,1,2)),rewrite(24796(2),24796(4),24796(6),24796(8),24796(16))]. given #748 (F,wt=31): 29134 f(f(f(x,y),f(z,f(x,z))),f(c_0,f(x,f(f(x,y),f(c_0,f(y,f(x,f(x,y)))))))) = f(x,y) # label(false). [para(25479(a,1),29089(a,1,1,2,2,2)),rewrite(24796(8),25479(16),24796(15),25479(21))]. given #749 (F,wt=31): 29763 f(f(x,f(y,f(y,x))),f(f(y,x),f(z,f(z,f(f(y,x),f(c_0,f(x,f(y,f(y,x))))))))) = c_0 # label(false). [para(26820(a,1),26767(a,1,1,2,2,2,2)),rewrite(26820(23),10928(18),24796(15))]. given #750 (T,wt=19): 26648 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)). [para(10801(a,1),26613(a,1,2,2,2)),rewrite(24796(3),24796(8),10928(8),24796(5),24796(8))]. given #751 (T,wt=19): 26720 f(f(x,x),f(f(c_0,f(x,y)),f(f(x,x),f(z,u)))) = x. [para(26716(a,1),18936(a,1,1)),rewrite(26716(10),9861(8),24796(6),24796(8),26716(14),9861(12))]. given #752 (T,wt=17): 32366 f(f(c_0,f(x,y)),f(f(x,x),f(z,u))) = f(x,y). [para(26720(a,1),25889(a,1,2,2,2)),rewrite(24796(14),26716(14),24796(12),26720(12),24796(4),10806(4)),flip(a)]. given #753 (T,wt=15): 32455 f(f(x,x),f(f(y,z),f(c_0,f(x,u)))) = x. [para(11(a,1),32366(a,1,1,2)),rewrite(24796(2),9914(2),24796(2),24796(3),9914(4,R),24796(4),24796(6),24796(8),24796(10),543(10))]. given #754 (A,wt=49): 24933 f(f(c_0,f(f(x,f(c_0,f(y,z))),f(c_0,f(f(y,z),f(x,