============================== Prover9 =============================== Prover9 (32) version Aug-2007, Aug 2007. Process 17639 was started by mccune on cleo, Tue Aug 7 10:07:58 2007 The command was "/home/mccune/LADR/bin/prover9 -f MOL-M.in MOL-M-interp.outx". ============================== 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.outx 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(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. f(c1,f(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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, f ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). not interpretable: c1 % Clause contains symbol not in interpretation: % f(c1,f(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,w)))) = y. [para(2(a,1),2(a,1,2,1))]. given #3 (T,wt=9): 11 f(f(x,y),f(y,y)) = y. [para(4(a,1),4(a,1,2,2))]. given #4 (T,wt=11): 20 f(f(x,f(y,y)),y) = f(y,y). [para(11(a,1),11(a,1,2))]. given #5 (T,wt=13): 8 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(4(a,1),2(a,1,2,2))]. given #6 (T,wt=11): 32 f(f(f(x,x),y),x) = f(x,x). [para(8(a,1),11(a,1,1)),rewrite([8(7)]),flip(a)]. given #7 (A,wt=53): 5 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),f(f(z,x),v5)))) = f(z,x). [para(2(a,1),2(a,1,2,2,1,1,1,1))]. given #8 (T,wt=9): 40 f(f(x,y),f(x,x)) = x. [para(11(a,1),32(a,1,1,1)),rewrite([11(6)])]. given #9 (T,wt=13): 55 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(2(a,1),40(a,1,1))]. given #10 (T,wt=13): 61 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(40(a,1),40(a,1,1))]. given #11 (T,wt=15): 22 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(14),rewrite([20(7)])]. given #12 (A,wt=57): 6 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),y),f(y,w)))) = y. [para(2(a,1),2(a,1,2,2,1,1,1))]. given #13 (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)),w),f(f(f(f(x,w),w),f(z,x)),x))) = f(z,x). [para(2(a,1),5(a,1,2,2,2))]. given #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),w)))) = 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)))))),w),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)))),w),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)))))),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))))),v5)))) = 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),w)))) = 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),w)))) = 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)),w),f(f(f(f(x,w),w),f(z,x)),z))) = f(z,x). [para(40(a,1),5(a,1,2,2,2))]. given #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,w)))) = 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(w,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)),w),f(f(f(f(x,w),w),f(z,x)),f(f(z,x),v5)))) = 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)),w),f(f(f(f(x,w),w),f(z,x)),f(v5,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,w))),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,w)))) = 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(w,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,w),u),u),y),f(y,v5)))))) = 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)),w),f(f(f(f(z,w),w),f(y,z)),f(f(y,z),v5)))))) = 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)),w),f(f(f(f(f(f(y,z),v5),w),w),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)),w),f(f(f(f(z,w),w),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: function_order([ c1, c2, c3, c_0, f ]). NOTE: sn=98, num_tables=180 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),w),u),u),f(y,y)),f(f(y,y),v5)))))) = 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),w)),f(f(z,x),w)),f(z,x)),f(f(z,x),v5)))) = 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,w)))) = 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(w,v5))))) = 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,w)))))) = 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(