============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4468 was started by mccune on cleo.thornwood, Wed Nov 22 12:06:20 2006 The command was "/home/mccune/bin/prover9 -f MOL-M.in MOL-M-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MOL-M.in assign(max_weight,60). assign(new_constants,1). set(lex_order_vars). set(restrict_denials). assign(max_hours,1). % assign(max_hours, 1) -> assign(max_seconds, 3600). assign(age_part,1). assign(false_part,4). assign(true_part,4). formulas(sos). f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x # label(MOL_SS). end_of_list. formulas(goals). f(x,f(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(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. f(c1,f(c3,f(c1,f(c2,c2)))) != f(c1,f(c2,f(c1,f(c3,c3)))) # answer(MOD_SS). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, f ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). 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 (F,wt=35): 7 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z). [para(2(a,1),2(a,1,2,2,2))]. given #3 (F,wt=41): 8 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y. [para(2(a,1),7(a,1,1,2)),rewrite(2(12),2(12),2(14),2(17),2(30))]. given #4 (F,wt=13): 12 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(2(a,1),8(a,1,2,2))]. given #5 (F,wt=9): 20 f(f(x,y),f(y,y)) = y. [para(2(a,1),12(a,1,2,1))]. given #6 (T,wt=11): 46 f(f(x,f(y,y)),y) = f(y,y). [para(20(a,1),7(a,1,2,2,1)),rewrite(20(5),20(5))]. given #7 (T,wt=11): 55 f(f(f(x,x),y),x) = f(x,x). [para(12(a,1),20(a,1,1)),rewrite(12(7)),flip(a)]. given #8 (T,wt=9): 77 f(f(x,y),f(x,x)) = x. [para(20(a,1),55(a,1,1,1)),rewrite(20(6))]. given #9 (T,wt=13): 82 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(2(a,1),77(a,1,1))]. given #10 (A,wt=57): 4 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(y,v)))) = y. [para(2(a,1),2(a,1,2,1))]. given #11 (F,wt=33): 44 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(false). [para(20(a,1),7(a,1,2,2,1,1,1,1))]. given #12 (F,wt=45): 62 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),z),f(f(f(f(f(x,x),z),z),f(y,f(x,x))),f(x,x)))) = f(y,f(x,x)) # label(false). [para(46(a,1),7(a,1,2,2,1,1,1,1))]. given #13 (F,wt=13): 91 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(77(a,1),77(a,1,1))]. given #14 (F,wt=15): 57 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(37),rewrite(46(7))]. given #15 (T,wt=15): 139 f(f(x,y),f(y,f(f(y,y),f(z,y)))) = y. [para(82(a,1),57(a,1,2,2,2))]. given #16 (T,wt=17): 135 f(x,f(f(x,x),f(x,f(f(x,x),y)))) = f(x,x). [para(20(a,1),57(a,1,1)),rewrite(77(4))]. given #17 (T,wt=17): 156 f(x,f(f(x,x),f(x,f(y,f(x,x))))) = f(x,x). [para(20(a,1),139(a,1,1)),rewrite(77(4))]. given #18 (T,wt=21): 40 f(f(x,f(y,y)),f(f(y,y),f(y,f(f(y,y),z)))) = f(y,y). [para(20(a,1),2(a,1,2,2,1)),rewrite(20(5))]. given #19 (A,wt=53): 5 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),f(f(z,x),w)))) = f(z,x). [para(2(a,1),2(a,1,2,2,1,1,1,1))]. given #20 (F,wt=21): 69 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x. [para(55(a,1),2(a,1,2,2,1,1))]. given #21 (F,wt=21): 136 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x. [para(57(a,1),55(a,1)),flip(a)]. given #22 (F,wt=13): 219 f(x,f(f(x,x),f(x,y))) = f(x,x). [para(136(a,1),20(a,1,1)),rewrite(136(9)),flip(a)]. given #23 (F,wt=13): 230 f(f(x,x),f(x,f(f(x,x),y))) = x. [para(20(a,1),219(a,1,2,1)),rewrite(77(8))]. given #24 (T,wt=13): 233 f(x,f(f(x,x),f(y,x))) = f(x,x). [para(82(a,1),219(a,1,2,2))]. given #25 (T,wt=13): 244 f(f(x,x),f(x,f(y,f(x,x)))) = x. [para(82(a,1),230(a,1,2,2))]. given #26 (T,wt=19): 261 f(f(f(f(x,x),x),f(f(x,x),x)),x) = f(f(x,x),x). [para(44(a,1),244(a,1,2,2)),rewrite(173(13),55(14),77(11)),flip(a)]. given #27 (T,wt=21): 210 f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x)) = x. [para(69(a,1),82(a,1,2,1)),rewrite(69(16),69(18))]. given #28 (A,wt=57): 6 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),y),f(y,v)))) = y. [para(2(a,1),2(a,1,2,2,1,1,1))]. given #29 (F,wt=21): 211 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x. [para(82(a,1),69(a,1,2,2,2))]. given #30 (F,wt=21): 226 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)). [para(2(a,1),219(a,1,2,2))]. given #31 (F,wt=21): 232 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)). [para(77(a,1),219(a,1,2,2))]. given #32 (F,wt=21): 262 f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(62(a,1),244(a,1,2,2)),rewrite(77(3),77(5),77(10),77(12),174(15),77(8),77(10),77(15),55(15),77(11),77(5),77(7)),flip(a)]. given #33 (T,wt=21): 275 f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(x,x)) = x. [para(82(a,1),210(a,1,1,2,2))]. given #34 (T,wt=23): 207 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [para(20(a,1),69(a,1,1)),rewrite(77(3),77(5))]. given #35 (T,wt=23): 239 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(230(a,1),2(a,1,2,2,1,1,1)),rewrite(230(6))]. given #36 (T,wt=23): 257 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(x,z)))) = x. [para(244(a,1),2(a,1,2,2,1,1,1)),rewrite(244(6))]. given #37 (A,wt=49): 9 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),x))) = f(z,x). [para(2(a,1),7(a,1,2,2,1,1,1,1))]. given #38 (F,wt=23): 272 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))),x) = f(x,x). [para(20(a,1),210(a,1,1,1,1)),rewrite(77(5),77(11))]. given #39 (F,wt=23): 292 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [para(20(a,1),211(a,1,1)),rewrite(77(3),77(5))]. given #40 (F,wt=23): 312 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x). [para(20(a,1),275(a,1,1,1,1)),rewrite(77(5),77(11))]. given #41 (F,wt=23): 320 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(82(a,1),239(a,1,2,2,2))]. given #42 (T,wt=17): 347 f(f(x,x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(82(a,1),320(a,1,2))]. given #43 (T,wt=17): 356 f(f(x,x),f(f(x,f(x,f(y,f(x,x)))),x)) = x. [para(82(a,1),347(a,1,2,1,2,2))]. given #44 (T,wt=21): 355 f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x))) = f(x,x). [para(20(a,1),347(a,1,1)),rewrite(77(5))]. given #45 (T,wt=21): 364 f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x))) = f(x,x). [para(20(a,1),356(a,1,1)),rewrite(77(5))]. given #46 (A,wt=59): 10 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(f(f(y,z),w),v),v),f(y,z)),z))))) = f(y,z). [para(7(a,1),7(a,1,1,2)),rewrite(7(17),7(18),7(21),7(25),7(42))]. given #47 (F,wt=23): 327 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(z,x)))) = x. [para(82(a,1),257(a,1,2,2,2))]. given #48 (F,wt=25): 39 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y. [para(20(a,1),2(a,1,2,2,1,1,1))]. given #49 (F,wt=19): 404 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(275(a,1),39(a,1,2,2,1)),rewrite(20(4),77(3),82(6))]. given #50 (F,wt=19): 405 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(312(a,1),39(a,1,2,2,1)),rewrite(46(3),82(8))]. given #51 (T,wt=19): 412 f(f(f(f(x,x),x),f(x,f(f(x,x),y))),x) = f(x,x). [para(404(a,1),82(a,1,2,1)),rewrite(404(14),77(9),404(14))]. given #52 (T,wt=19): 413 f(x,f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(82(a,1),404(a,1,2,2,2))]. given #53 (T,wt=19): 426 f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)) = x. [para(405(a,1),82(a,1,2,1)),rewrite(405(14),405(16))]. given #54 (T,wt=19): 427 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(82(a,1),405(a,1,2,2,2))]. given #55 (A,wt=59): 11 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(z,v),v),f(y,z)),f(f(y,z),w)))))) = f(y,z). [para(2(a,1),8(a,1,2,2,2,2,1,1,1,1))]. given #56 (F,wt=19): 430 f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x) = f(x,x). [para(82(a,1),412(a,1,1,2,2))]. given #57 (F,wt=19): 439 f(f(f(x,f(x,x)),f(f(x,x),f(y,x))),f(x,x)) = x. [para(82(a,1),426(a,1,1,2,2))]. given #58 (F,wt=21): 392 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(x,y)))) = x. [para(55(a,1),39(a,1,2,2,1)),rewrite(77(6))]. given #59 (F,wt=19): 476 f(f(f(f(x,x),x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(392(a,1),82(a,1,2,1)),rewrite(392(15),392(17))]. given #60 (T,wt=19): 487 f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),x) = f(x,x). [para(20(a,1),476(a,1,1,1,1)),rewrite(77(5),77(9))]. given #61 (T,wt=19): 490 f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(82(a,1),476(a,1,1,2,2))]. given #62 (T,wt=19): 498 f(f(f(x,f(x,x)),f(x,f(y,f(x,x)))),x) = f(x,x). [para(82(a,1),487(a,1,1,2,2))]. given #63 (T,wt=21): 477 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(y,x)))) = x. [para(82(a,1),392(a,1,2,2,2))]. given #64 (A,wt=57): 13 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(f(f(y,y),w),f(f(f(f(f(y,v6),w),w),y),f(y,v7)))))))) = y. [para(8(a,1),7(a,1,1,2)),rewrite(8(20),8(20),8(22),8(25),8(46))]. given #65 (F,wt=21): 499 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y))))) = x. [para(487(a,1),232(a,1,1)),rewrite(487(8),487(9),77(4),487(16),487(17),77(12))]. given #66 (F,wt=21): 513 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(y,f(x,x)))))) = x. [para(498(a,1),232(a,1,1)),rewrite(498(8),498(9),77(4),498(16),498(17),77(12))]. given #67 (F,wt=23): 395 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(f(x,x),y)))) = f(x,x). [para(77(a,1),39(a,1,2,2,1)),rewrite(77(5))]. given #68 (F,wt=23): 479 f(x,f(f(x,x),f(f(f(x,x),x),f(f(x,x),f(x,y))))) = f(x,x). [para(392(a,1),226(a,1,1)),rewrite(392(9),392(9),392(18),392(18))]. given #69 (T,wt=23): 506 f(x,f(f(x,x),f(f(f(x,x),x),f(f(x,x),f(y,x))))) = f(x,x). [para(490(a,1),232(a,1,1)),rewrite(490(8),490(8),490(17),490(17))]. given #70 (T,wt=23): 520 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(y,f(x,x))))) = f(x,x). [para(20(a,1),477(a,1,1,1)),rewrite(77(5),77(7))]. given #71 (T,wt=25): 60 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(f(x,x),x),y),f(y,z)))) = y. [para(46(a,1),2(a,1,2,2,1,1,1))]. given #72 (T,wt=23): 577 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))),f(x,x)) = x. [para(60(a,1),82(a,1,2,1)),rewrite(60(19),60(21))]. given #73 (A,wt=31): 35 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(z,x)),y),y),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(20(a,1),2(a,1,1)),rewrite(20(3))]. given #74 (F,wt=23): 594 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x))),f(x,x)) = x. [para(82(a,1),577(a,1,1,2,2))]. given #75 (F,wt=25): 96 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y. [para(82(a,1),2(a,1,2,2,2))]. given #76 (F,wt=25): 97 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = x. [para(2(a,1),82(a,1,2,1)),rewrite(2(20),2(22))]. given #77 (F,wt=25): 190 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(20(a,1),5(a,1,2,1,1)),rewrite(97(11))]. given #78 (T,wt=25): 397 f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [para(39(a,1),82(a,1,2,1)),rewrite(39(20),39(22))]. given #79 (T,wt=25): 399 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(z,y)))) = y. [para(82(a,1),39(a,1,2,2,2))]. given #80 (T,wt=25): 579 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(f(x,x),x),y),f(z,y)))) = y. [para(82(a,1),60(a,1,2,2,2))]. given #81 (T,wt=25): 589 f(f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(20(a,1),577(a,1,1,1,1)),rewrite(77(12))]. given #82 (A,wt=33): 36 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(20(a,1),2(a,1,2,1,1))]. given #83 (F,wt=25): 640 f(f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(z,f(x,x)))),x) = f(x,x). [para(20(a,1),594(a,1,1,1,1)),rewrite(77(12))]. given #84 (F,wt=25): 641 f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [para(20(a,1),594(a,1,1,2,1,1,1))]. given #85 (F,wt=25): 658 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x))),f(x,x)) = x. [para(96(a,1),82(a,1,2,1)),rewrite(96(20),96(22))]. given #86 (F,wt=25): 668 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(z,f(x,x))))) = f(x,x). [para(69(a,1),96(a,1,2,2,1,1,1,1)),rewrite(210(9),77(3))]. given #87 (T,wt=25): 747 f(f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(x,u))),f(x,x)) = x. [para(82(a,1),97(a,1,1,2,1,1,1,1))]. given #88 (T,wt=25): 749 f(f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(69(a,1),97(a,1,1,2,1,1,1,1)),rewrite(77(3),77(12))]. given #89 (T,wt=25): 856 f(f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(u,x))),f(x,x)) = x. [para(82(a,1),658(a,1,1,2,1,1,1,1))]. given #90 (T,wt=25): 858 f(f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(z,f(x,x)))),x) = f(x,x). [para(69(a,1),658(a,1,1,2,1,1,1,1)),rewrite(77(3),77(12))]. given #91 (A,wt=37): 38 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(20(a,1),2(a,1,2,2,1,1,1,1))]. given #92 (F,wt=27): 80 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y. [para(77(a,1),2(a,1,2,2,1,1))]. given #93 (F,wt=21): 969 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(46(a,1),80(a,1,2,2,1)),rewrite(82(9))]. given #94 (F,wt=21): 1005 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(82(a,1),969(a,1,2,2,2))]. given #95 (F,wt=23): 967 f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(20(a,1),80(a,1,2,2,1)),rewrite(77(5),82(8))]. given #96 (T,wt=23): 1017 f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(20(a,1),1005(a,1,1,1)),rewrite(77(6),77(7))]. given #97 (T,wt=27): 350 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,f(f(x,x),y))),x)),x),f(x,z)))) = x. [para(347(a,1),2(a,1,2,2,1,1,1)),rewrite(347(8))]. given #98 (T,wt=27): 359 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,f(y,f(x,x)))),x)),x),f(x,z)))) = x. [para(356(a,1),2(a,1,2,2,1,1,1)),rewrite(356(8))]. given #99 (T,wt=27): 583 f(x,f(f(x,x),f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))))) = f(x,x). [para(60(a,1),226(a,1,1)),rewrite(60(11),60(11),60(22),60(22))]. given #100 (A,wt=33): 45 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z). [para(20(a,1),7(a,1,2,2,1,1,1))]. given #101 (F,wt=15): 1071 f(f(x,f(x,x)),f(x,f(f(x,x),y))) = x. [para(39(a,1),45(a,1,2,2,1)),rewrite(77(3),77(6),77(10),77(13),77(16),77(19),77(27),230(27),46(23),77(9),77(3),77(6)),flip(a)]. given #102 (F,wt=15): 1073 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x. [para(404(a,1),45(a,1,1)),rewrite(967(25),230(21),46(17),77(3)),flip(a)]. given #103 (F,wt=15): 1077 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x. [para(413(a,1),45(a,1,1)),rewrite(1017(25),244(21),46(17),77(3)),flip(a)]. given #104 (F,wt=15): 1083 f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. [para(520(a,1),45(a,1,2,2,1)),rewrite(244(27),46(23),77(9)),flip(a)]. given #105 (T,wt=17): 1075 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x). [para(405(a,1),45(a,1,1)),rewrite(77(16),77(18),969(23),219(18),20(16)),flip(a)]. given #106 (T,wt=17): 1079 f(f(x,f(x,x)),f(f(x,x),f(y,x))) = f(x,x). [para(427(a,1),45(a,1,1)),rewrite(77(16),77(18),1005(23),233(18),20(16)),flip(a)]. given #107 (T,wt=17): 1085 f(f(f(x,x),x),f(f(x,x),f(x,y))) = f(x,x). [para(60(a,1),45(a,1,2,2,1)),rewrite(77(4),77(4),77(8),55(6),77(7),77(11),77(11),77(15),55(13),77(14),77(17),77(17),77(21),55(19),77(20),77(24),77(25),77(27),55(25),77(26),219(26),20(24),55(9),77(4),77(4),77(8),55(6),77(7)),flip(a)]. given #108 (T,wt=17): 1091 f(f(f(x,x),x),f(f(x,x),f(y,x))) = f(x,x). [para(579(a,1),45(a,1,2,2,1)),rewrite(77(4),77(4),77(8),55(6),77(7),77(11),77(11),77(15),55(13),77(14),77(17),77(17),77(21),55(19),77(20),77(24),77(25),77(27),55(25),77(26),233(26),20(24),55(9),77(4),77(4),77(8),55(6),77(7)),flip(a)]. given #109 (A,wt=49): 47 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(z,x)),y),y),f(x,x)),f(f(x,u),f(f(f(f(f(f(x,x),v),u),u),f(x,x)),f(f(x,x),w)))))) = f(x,x). [para(20(a,1),8(a,1,1)),rewrite(20(3),20(11))]. given #110 (F,wt=23): 1120 f(f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z))),x) = f(x,x). [para(1071(a,1),747(a,1,1,2,1,1,1)),rewrite(77(3),77(10),77(11))]. given #111 (F,wt=23): 1122 f(f(f(x,f(x,f(f(x,x),y))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(1071(a,1),856(a,1,1,2,1,1,1)),rewrite(77(3),77(10),77(11))]. given #112 (F,wt=23): 1156 f(f(f(x,f(x,f(y,f(x,x)))),f(x,f(f(x,x),z))),x) = f(x,x). [para(1077(a,1),97(a,1,1,2,1,1,1)),rewrite(77(3),77(10),77(11))]. given #113 (F,wt=23): 1159 f(f(f(x,f(x,f(y,f(x,x)))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(1077(a,1),658(a,1,1,2,1,1,1)),rewrite(77(3),77(10),77(11))]. given #114 (T,wt=25): 1103 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(1071(a,1),2(a,1,2,2,1,1,1)),rewrite(230(7))]. given #115 (T,wt=25): 1113 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(1071(a,1),96(a,1,2,2,1,1,1)),rewrite(230(7))]. given #116 (T,wt=19): 1327 f(f(f(x,x),x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(82(a,1),1113(a,1,2))]. given #117 (T,wt=15): 1340 f(f(x,f(x,f(f(x,x),y))),x) = f(x,x). [para(1327(a,1),44(a,1,2,2,1)),rewrite(347(7),20(14)),flip(a)]. given #118 (A,wt=51): 48 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,u),f(f(f(f(f(f(y,y),v),u),u),f(y,y)),f(f(y,y),w)))))) = f(y,y). [para(20(a,1),8(a,1,2,1,1)),rewrite(20(12))]. given #119 (F,wt=15): 1349 f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). [para(82(a,1),1340(a,1,1,2,2))]. given #120 (F,wt=17): 1341 f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(1327(a,1),62(a,1,2,2,1)),rewrite(77(5),355(8),77(6),77(13),77(21),46(19),77(3),77(5)),flip(a)]. given #121 (F,wt=17): 1351 f(f(x,x),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(1340(a,1),232(a,1,1)),rewrite(1340(6),1340(7),77(4),1340(12),1340(13),77(10))]. given #122 (F,wt=17): 1375 f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(20(a,1),1349(a,1,1,2,2,2)),rewrite(77(10))]. given #123 (T,wt=17): 1378 f(f(x,x),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(1349(a,1),232(a,1,1)),rewrite(1349(6),1349(7),77(4),1349(12),1349(13),77(10))]. given #124 (T,wt=21): 1392 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))) = f(x,x). [para(1341(a,1),232(a,1,1)),rewrite(1341(7),1341(7),1341(15),1341(15))]. given #125 (T,wt=21): 1409 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))) = f(x,x). [para(1375(a,1),232(a,1,1)),rewrite(1375(7),1375(7),1375(15),1375(15))]. given #126 (T,wt=25): 1202 f(f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(1075(a,1),97(a,1,1,2,1,1,1)),rewrite(55(11))]. given #127 (A,wt=41): 50 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(20(a,1),8(a,1,2,2,1,1,1))]. given #128 (F,wt=25): 1206 f(f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(1075(a,1),658(a,1,1,2,1,1,1)),rewrite(55(11))]. given #129 (F,wt=25): 1225 f(f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(1079(a,1),97(a,1,1,2,1,1,1)),rewrite(55(11))]. given #130 (F,wt=25): 1229 f(f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(1079(a,1),658(a,1,1,2,1,1,1)),rewrite(55(11))]. given #131 (F,wt=25): 1294 f(f(x,x),f(x,f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z))))) = x. [para(1120(a,1),232(a,1,1)),rewrite(1120(10),1120(11),77(4),1120(20),1120(21),77(14))]. given #132 (T,wt=25): 1300 f(f(x,x),f(x,f(f(x,f(x,f(f(x,x),y))),f(x,f(z,f(x,x)))))) = x. [para(1122(a,1),232(a,1,1)),rewrite(1122(10),1122(11),77(4),1122(20),1122(21),77(14))]. given #133 (T,wt=25): 1306 f(f(x,x),f(x,f(f(x,f(x,f(y,f(x,x)))),f(x,f(f(x,x),z))))) = x. [para(1156(a,1),232(a,1,1)),rewrite(1156(10),1156(11),77(4),1156(20),1156(21),77(14))]. given #134 (T,wt=25): 1312 f(f(x,x),f(x,f(f(x,f(x,f(y,f(x,x)))),f(x,f(z,f(x,x)))))) = x. [para(1159(a,1),232(a,1,1)),rewrite(1159(10),1159(11),77(4),1159(20),1159(21),77(14))]. given #135 (T,wt=27): 647 f(x,f(f(x,x),f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x))))) = f(x,x). [para(594(a,1),232(a,1,1)),rewrite(594(10),594(10),594(21),594(21))]. given #136 (A,wt=41): 52 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),f(u,u)),f(f(f(u,f(u,u)),y),f(y,v)))))) = y. [para(20(a,1),8(a,1,2,2,2,2,1,1,1))]. given #137 (F,wt=27): 657 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(z,y)))) = y. [para(77(a,1),96(a,1,2,2,1,1))]. given #138 (F,wt=27): 744 f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(x,x)) = x. [para(77(a,1),97(a,1,1,2,1,1))]. given #139 (F,wt=23): 1605 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(1340(a,1),744(a,1,1,2,1)),rewrite(1348(11))]. given #140 (F,wt=23): 1606 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(1349(a,1),744(a,1,1,2,1)),rewrite(1376(11))]. given #141 (T,wt=23): 1614 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(82(a,1),1605(a,1,1,2,2))]. given #142 (T,wt=23): 1623 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(82(a,1),1606(a,1,1,2,2))]. given #143 (T,wt=25): 1607 f(f(f(f(x,x),f(f(x,x),f(x,y))),f(x,f(f(x,x),z))),x) = f(x,x). [para(1341(a,1),744(a,1,1,2,1)),rewrite(77(3),1390(12),77(12))]. given #144 (T,wt=25): 1608 f(f(f(f(x,x),f(f(x,x),f(y,x))),f(x,f(f(x,x),z))),x) = f(x,x). [para(1375(a,1),744(a,1,1,2,1)),rewrite(77(3),1408(12),77(12))]. given #145 (A,wt=29): 58 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,f(z,f(x,x))),y),y),x),f(x,u)))) = x. [para(46(a,1),2(a,1,1))]. given #146 (F,wt=25): 1628 f(f(f(f(x,x),f(f(x,x),f(x,y))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(20(a,1),1614(a,1,1,1,2,2,1)),rewrite(77(8),77(12))]. given #147 (F,wt=25): 1634 f(f(f(f(x,x),f(f(x,x),f(y,x))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(20(a,1),1623(a,1,1,1,2,2,2)),rewrite(77(8),77(12))]. given #148 (F,wt=27): 770 f(f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(20(a,1),397(a,1,1,1,1)),rewrite(77(13))]. given #149 (F,wt=27): 816 f(f(x,x),f(x,f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(f(x,x),z))))) = x. [para(589(a,1),232(a,1,1)),rewrite(589(11),589(12),77(4),589(22),589(23),77(15))]. given #150 (T,wt=27): 836 f(f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,x)),f(z,f(x,x)))),x) = f(x,x). [para(20(a,1),640(a,1,1,2,1,1,1))]. given #151 (T,wt=27): 842 f(f(x,x),f(x,f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(z,f(x,x)))))) = x. [para(640(a,1),232(a,1,1)),rewrite(640(11),640(12),77(4),640(22),640(23),77(15))]. given #152 (T,wt=27): 854 f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(z,x))),f(x,x)) = x. [para(77(a,1),658(a,1,1,2,1,1))]. given #153 (T,wt=27): 898 f(f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),x),f(x,z))),f(x,x)) = x. [para(77(a,1),747(a,1,1,2,1,1))]. given #154 (A,wt=49): 59 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),z),f(f(f(f(f(x,x),z),z),f(y,f(x,x))),f(f(y,f(x,x)),u)))) = f(y,f(x,x)). [para(46(a,1),2(a,1,2,2,1,1,1,1))]. given #155 (F,wt=27): 928 f(f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),x),f(z,x))),f(x,x)) = x. [para(77(a,1),856(a,1,1,2,1,1))]. given #156 (F,wt=27): 1127 f(f(x,f(x,x)),f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z)))) = f(x,x). [para(1073(a,1),2(a,1,2,2,1,1,1)),rewrite(77(5),77(12))]. given #157 (F,wt=19): 1719 f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z))) = x. [para(1127(a,1),45(a,1,2,2,1)),rewrite(230(33),46(29),77(11)),flip(a)]. given #158 (F,wt=19): 1729 f(f(x,f(x,f(y,f(x,x)))),f(x,f(f(x,x),z))) = x. [para(82(a,1),1719(a,1,1,2,2))]. given #159 (T,wt=19): 1730 f(f(x,f(x,f(f(x,x),y))),f(x,f(z,f(x,x)))) = x. [para(82(a,1),1719(a,1,2,2))]. given #160 (T,wt=19): 1755 f(f(x,f(x,f(y,f(x,x)))),f(x,f(z,f(x,x)))) = x. [para(82(a,1),1729(a,1,2,2))]. given #161 (T,wt=23): 1728 f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,x),f(x,z))) = f(x,x). [para(20(a,1),1719(a,1,1,2,2,1)),rewrite(77(9))]. given #162 (T,wt=23): 1754 f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,x),f(x,z))) = f(x,x). [para(20(a,1),1729(a,1,1,2,2,2)),rewrite(77(9))]. given #163 (A,wt=45): 61 f(f(f(x,y),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(f(f(x,y),f(u,f(f(x,y),f(x,y)))),z),z),f(x,y)),y))) = f(x,y). [para(46(a,1),7(a,1,1))]. given #164 (F,wt=23): 1758 f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,x),f(z,x))) = f(x,x). [para(20(a,1),1730(a,1,1,2,2,1)),rewrite(77(9))]. given #165 (F,wt=23): 1765 f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,x),f(z,x))) = f(x,x). [para(20(a,1),1755(a,1,1,2,2,2)),rewrite(77(9))]. given #166 (F,wt=27): 1397 f(f(x,x),f(x,f(f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),x),f(x,z)))) = x. [para(1351(a,1),2(a,1,2,2,1,1,1)),rewrite(1351(8))]. given #167 (F,wt=27): 1406 f(f(x,x),f(x,f(f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),x),f(z,x)))) = x. [para(1351(a,1),96(a,1,2,2,1,1,1)),rewrite(1351(8))]. given #168 (T,wt=21): 1856 f(f(x,x),f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),x)) = x. [para(82(a,1),1406(a,1,2))]. given #169 (T,wt=21): 1866 f(f(x,x),f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),x)) = x. [para(82(a,1),1856(a,1,2,1,2,2,2,2))]. given #170 (T,wt=27): 1414 f(f(x,x),f(x,f(f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),x),f(x,z)))) = x. [para(1378(a,1),2(a,1,2,2,1,1,1)),rewrite(1378(8))]. given #171 (T,wt=27): 1423 f(f(x,x),f(x,f(f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),x),f(z,x)))) = x. [para(1378(a,1),96(a,1,2,2,1,1,1)),rewrite(1378(8))]. given #172 (A,wt=33): 63 f(f(f(x,x),f(y,z)),f(f(f(f(y,z),f(y,z)),x),f(f(f(f(x,x),x),f(y,z)),z))) = f(y,z). [para(46(a,1),7(a,1,2,2,1,1,1))]. given #173 (F,wt=27): 1615 f(x,f(f(x,x),f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(x,z))))) = f(x,x). [para(1605(a,1),232(a,1,1)),rewrite(1605(10),1605(10),1605(21),1605(21))]. given #174 (F,wt=27): 1624 f(x,f(f(x,x),f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,z))))) = f(x,x). [para(1606(a,1),232(a,1,1)),rewrite(1606(10),1606(10),1606(21),1606(21))]. given #175 (F,wt=27): 1630 f(x,f(f(x,x),f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(z,x))))) = f(x,x). [para(1614(a,1),232(a,1,1)),rewrite(1614(10),1614(10),1614(21),1614(21))]. given #176 (F,wt=27): 1636 f(x,f(f(x,x),f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(z,x))))) = f(x,x). [para(1623(a,1),232(a,1,1)),rewrite(1623(10),1623(10),1623(21),1623(21))]. given #177 (T,wt=27): 1643 f(f(x,x),f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,f(f(x,x),z))))) = x. [para(1607(a,1),232(a,1,1)),rewrite(1607(11),1607(12),77(4),1607(22),1607(23),77(15))]. given #178 (T,wt=27): 1648 f(f(x,x),f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,f(f(x,x),z))))) = x. [para(1608(a,1),232(a,1,1)),rewrite(1608(11),1608(12),77(4),1608(22),1608(23),77(15))]. given #179 (T,wt=27): 1664 f(f(x,x),f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,f(z,f(x,x)))))) = x. [para(1628(a,1),232(a,1,1)),rewrite(1628(11),1628(12),77(4),1628(22),1628(23),77(15))]. given #180 (T,wt=27): 1669 f(f(x,x),f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,f(z,f(x,x)))))) = x. [para(1634(a,1),232(a,1,1)),rewrite(1634(11),1634(12),77(4),1634(22),1634(23),77(15))]. given #181 (A,wt=45): 64 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,f(z,f(x,x))),y),y),x),f(f(f(x,x),u),f(f(f(f(f(x,v),u),u),x),f(x,w)))))) = x. [para(46(a,1),8(a,1,1))]. given #182 (F,wt=27): 1739 f(x,f(f(x,f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(f(x,x),z)))) = f(x,x). [para(1719(a,1),190(a,1,2,2,1,1))]. given #183 (F,wt=27): 1742 f(x,f(f(x,f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(z,f(x,x))))) = f(x,x). [para(1719(a,1),668(a,1,2,2,1,1))]. given #184 (F,wt=27): 1745 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(1719(a,1),749(a,1,1,2,1,1))]. given #185 (F,wt=27): 1748 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(z,f(x,x)))),x) = f(x,x). [para(1719(a,1),858(a,1,1,2,1,1))]. given #186 (T,wt=27): 1774 f(x,f(f(x,f(x,f(y,f(x,x)))),f(f(x,f(x,x)),f(f(x,x),z)))) = f(x,x). [para(1755(a,1),190(a,1,2,2,1,1))]. given #187 (T,wt=27): 1777 f(x,f(f(x,f(x,f(y,f(x,x)))),f(f(x,f(x,x)),f(z,f(x,x))))) = f(x,x). [para(1755(a,1),668(a,1,2,2,1,1))]. given #188 (T,wt=27): 1780 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(1755(a,1),749(a,1,1,2,1,1))]. given #189 (T,wt=27): 1783 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,f(x,x)),f(z,f(x,x)))),x) = f(x,x). [para(1755(a,1),858(a,1,1,2,1,1))]. given #190 (A,wt=41): 65 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(f(x,x),x),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(46(a,1),8(a,1,2,2,1,1,1))]. given #191 (F,wt=27): 1789 f(f(x,x),f(f(f(x,x),f(f(x,x),f(x,y))),f(f(f(x,x),x),f(x,z)))) = x. [para(1728(a,1),2(a,1,2,2,1,1))]. given #192 (F,wt=27): 1804 f(f(x,x),f(f(f(x,x),f(f(x,x),f(x,y))),f(f(f(x,x),x),f(z,x)))) = x. [para(1728(a,1),96(a,1,2,2,1,1))]. given #193 (F,wt=27): 1805 f(f(f(f(x,x),f(f(x,x),f(x,y))),f(f(f(x,x),x),f(x,z))),f(x,x)) = x. [para(1728(a,1),97(a,1,1,2,1,1))]. given #194 (F,wt=27): 1806 f(f(f(f(x,x),f(f(x,x),f(x,y))),f(f(f(x,x),x),f(z,x))),f(x,x)) = x. [para(1728(a,1),658(a,1,1,2,1,1))]. given #195 (T,wt=27): 1831 f(f(x,x),f(f(f(x,x),f(f(x,x),f(y,x))),f(f(f(x,x),x),f(x,z)))) = x. [para(1765(a,1),2(a,1,2,2,1,1))]. given #196 (T,wt=27): 1840 f(f(x,x),f(f(f(x,x),f(f(x,x),f(y,x))),f(f(f(x,x),x),f(z,x)))) = x. [para(1765(a,1),96(a,1,2,2,1,1))]. given #197 (T,wt=27): 1841 f(f(f(f(x,x),f(f(x,x),f(y,x))),f(f(f(x,x),x),f(x,z))),f(x,x)) = x. [para(1765(a,1),97(a,1,1,2,1,1))]. given #198 (T,wt=27): 1842 f(f(f(f(x,x),f(f(x,x),f(y,x))),f(f(f(x,x),x),f(z,x))),f(x,x)) = x. [para(1765(a,1),658(a,1,1,2,1,1))]. given #199 (A,wt=39): 66 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(u,u),u),y),f(y,v)))))) = y. [para(46(a,1),8(a,1,2,2,2,2,1,1,1))]. given #200 (F,wt=29): 67 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,f(f(x,x),z)),y),y),x),f(x,u)))) = x. [para(55(a,1),2(a,1,1))]. given #201 (F,wt=29): 263 f(f(f(x,x),x),f(f(f(x,x),y),f(f(f(f(f(f(x,x),x),y),y),x),f(x,z)))) = x. [para(261(a,1),2(a,1,1)),rewrite(82(10))]. given #202 (F,wt=29): 295 f(x,f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))))) = f(x,x). [para(2(a,1),226(a,1,1)),rewrite(2(11),2(11),2(23),2(23))]. given #203 (F,wt=29): 403 f(x,f(f(x,x),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))))) = f(x,x). [para(39(a,1),226(a,1,1)),rewrite(39(11),39(11),39(23),39(23))]. given #204 (T,wt=29): 651 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(u,x)))) = x. [para(46(a,1),96(a,1,1))]. given #205 (T,wt=29): 653 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(u,x)))) = x. [para(55(a,1),96(a,1,1))]. given #206 (T,wt=29): 678 f(f(f(x,x),x),f(f(f(x,x),y),f(f(f(f(f(f(x,x),x),y),y),x),f(z,x)))) = x. [para(261(a,1),96(a,1,1)),rewrite(82(10))]. given #207 (T,wt=29): 684 f(x,f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x))))) = f(x,x). [para(96(a,1),226(a,1,1)),rewrite(96(11),96(11),96(23),96(23))]. given #208 (A,wt=49): 68 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),z),f(f(f(f(f(x,x),z),z),f(f(x,x),y)),f(f(f(x,x),y),u)))) = f(f(x,x),y). [para(55(a,1),2(a,1,2,2,1,1,1,1))]. given #209 (F,wt=45): 2271 f(f(x,f(f(x,x),y)),f(f(f(f(f(x,x),y),f(f(x,x),y)),z),f(f(f(f(f(x,x),z),z),f(f(x,x),y)),f(x,x)))) = f(f(x,x),y) # label(false). [para(55(a,1),68(a,1,2,2,2))]. given #210 (F,wt=27): 2288 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(2277),rewrite(2285(3))]. given #211 (F,wt=25): 2356 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),2288(a,1,2,1,1,1)),rewrite(2(12),2(17),2(22))]. given #212 (F,wt=25): 2364 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(77(a,1),2288(a,1,2,1,1,1)),rewrite(77(4),77(9),77(14))]. given #213 (T,wt=9): 2285 f(f(x,x),f(x,y)) = x. [para(1073(a,1),2271(a,1,2,2,1)),rewrite(77(4),219(4),77(5),77(8),77(13),46(11),77(3),77(4)),flip(a)]. given #214 (T,wt=9): 2286 f(f(x,x),f(y,x)) = x. [para(1077(a,1),2271(a,1,2,2,1)),rewrite(2285(4),233(4),2285(5),2285(8),2285(13),46(11),2285(3),2285(4)),flip(a)]. given #215 (T,wt=11): 2386 f(x,f(f(x,x),y)) = f(x,x). [para(1073(a,1),2288(a,1,2,2,1)),rewrite(20(10)),flip(a)]. given #216 (T,wt=11): 2387 f(x,f(y,f(x,x))) = f(x,x). [para(1077(a,1),2288(a,1,2,2,1)),rewrite(20(10)),flip(a)]. given #217 (A,wt=37): 73 f(f(f(x,y),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,y)),y))) = f(x,y). [para(55(a,1),7(a,1,2,2,1,1))]. given #218 (F,wt=27): 2353 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(false). [back_rewrite(44),rewrite(2286(3))]. given #219 (F,wt=33): 2359 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(46(a,1),2288(a,1,2,1,1,1)),rewrite(46(6),2285(5),46(10),46(17))]. given #220 (F,wt=57): 2449 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(2356(a,1),2356(a,1,2,2,1,1,1))]. given #221 (F,wt=57): 2482 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(2364(a,1),2364(a,1,2,2,1,1,1))]. given #222 (T,wt=13): 2484 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(2(a,1),2285(a,1,2))]. given #223 (T,wt=13): 2489 f(f(f(x,y),f(x,y)),x) = f(x,y). [para(77(a,1),2285(a,1,2))]. given #224 (T,wt=19): 2405 f(x,f(f(x,f(x,x)),f(f(x,x),x))) = f(x,f(x,x)). [back_rewrite(2375),rewrite(2387(5))]. given #225 (T,wt=21): 2371 f(f(x,x),f(f(f(x,x),x),f(x,f(x,x)))) = f(f(x,x),x). [para(261(a,1),2288(a,1,2,1)),rewrite(55(6),2286(7))]. given #226 (A,wt=37): 75 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))))) = x. [para(55(a,1),8(a,1,2,2,1,1))]. given #227 (F,wt=35): 2750 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(2482(a,1),2484(a,2)),rewrite(2705(12),2705(28),2705(44),2484(48))]. given #228 (F,wt=35): 2789 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(2449(a,1),2489(a,2)),rewrite(2777(12),2777(28),2489(35))]. given #229 (F,wt=41): 2842 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(2(a,1),2750(a,1,1)),rewrite(2(17),2(21),2(26))]. given #230 (F,wt=41): 2846 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(77(a,1),2750(a,1,1)),rewrite(77(9),77(13),77(18))]. given #231 (T,wt=21): 2509 f(x,f(f(x,y),f(f(f(f(x,x),x),f(x,y)),y))) = f(x,y). [para(2285(a,1),45(a,1,1)),rewrite(2285(6),2489(4),2285(5))]. given #232 (T,wt=21): 2598 f(x,f(f(y,x),f(f(f(f(x,x),x),f(y,x)),x))) = f(y,x). [para(2286(a,1),45(a,1,1)),rewrite(2285(6),2484(4),2285(5))]. given #233 (T,wt=21): 2743 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,y)),x))) = f(x,y). [para(2484(a,1),2288(a,1,2,1))]. given #234 (T,wt=21): 2785 f(x,f(f(x,y),f(f(f(f(x,x),x),f(x,y)),x))) = f(x,y). [para(2489(a,1),2288(a,1,2,1))]. given #235 (A,wt=37): 76 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),y),f(f(f(y,y),y),f(y,u)))))) = y. [para(55(a,1),8(a,1,2,2,2,2,1,1))]. given #236 (F,wt=45): 2984 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(2750(a,1),2743(a,1,2,1)),rewrite(2750(17),2750(32),2750(37))]. given #237 (F,wt=45): 2985 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(2789(a,1),2743(a,1,2,1)),rewrite(2789(17),2789(32),2789(37))]. given #238 (F,wt=51): 2844 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(20(a,1),2750(a,1,2,2,1,1,2,1,1))]. given #239 (F,wt=51): 2861 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(20(a,1),2789(a,1,2,2,1,1,2,1,1))]. given #240 (T,wt=21): 2786 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),x))) = f(y,x). [para(2489(a,1),2353(a,1,2,1))]. given #241 (T,wt=23): 2725 f(f(x,x),f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z)))) = x. [para(60(a,1),2484(a,1,1,1)),rewrite(60(11),60(21))]. given #242 (T,wt=23): 2729 f(f(x,x),f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x)))) = x. [para(579(a,1),2484(a,1,1,1)),rewrite(579(11),579(21))]. given #243 (T,wt=25): 2350 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(115),rewrite(2286(3))]. given #244 (A,wt=35): 81 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),y))) = f(y,z). [para(77(a,1),2(a,1,2,2,2))]. given #245 (F,wt=55): 2858 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(2750(a,1),2750(a,1,2,2,1,1,2,2,1,1,1)),rewrite(2285(17))]. given #246 (F,wt=55): 2878 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(2789(a,1),2789(a,1,2,2,1,1,2,2,1,1,1)),rewrite(2285(17))]. given #247 (F,wt=55): 2986 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(2842(a,1),2743(a,1,2,1)),rewrite(2842(19),2842(38),2842(43))]. given #248 (F,wt=55): 2987 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(2846(a,1),2743(a,1,2,1)),rewrite(2846(19),2846(38),2846(43))]. given #249 (T,wt=25): 2366 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(77(a,1),2288(a,1,2,2,1,1))]. given #250 (T,wt=25): 2380 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(36(a,1),2288(a,1,2,2,1)),rewrite(77(6),77(17),2285(29),46(27),77(3),77(5)),flip(a)]. given #251 (T,wt=25): 2396 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(2297),rewrite(2386(3))]. given #252 (T,wt=25): 2397 f(f(x,x),f(f(f(x,x),x),f(x,f(y,f(f(x,x),x))))) = f(f(x,x),x). [back_rewrite(2292),rewrite(2386(3))]. given #253 (A,wt=41): 84 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(f(y,z),x),f(f(y,z),x))),f(f(f(f(y,z),x),f(y,z)),z))) = f(y,z). [para(77(a,1),7(a,1,2,2,1,1))]. given #254 (F,wt=25): 2400 f(x,f(f(x,f(x,x)),f(f(x,x),f(y,f(x,f(x,x)))))) = f(x,f(x,x)). [back_rewrite(1581),rewrite(2386(3),2285(4),2387(5))]. given #255 (F,wt=25): 2403 f(x,f(f(x,f(x,x)),f(f(x,x),f(f(x,f(x,x)),y)))) = f(x,f(x,x)). [back_rewrite(1125),rewrite(2386(3),2285(4),2387(5))]. given #256 (F,wt=25): 2455 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(20(a,1),2364(a,1,2,2,1,1,1))]. given #257 (F,wt=49): 3377 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(2455(a,1),81(a,1,2,2,1,1,1,1))]. Demod_limit: f(f(f(f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y)))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(y,y)),f(f(x,f(y,f(y,y))),f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y)))),y))),f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y)))),y)),f(f(f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y)))),y),f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y)))),y)),u),f(f(f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y)))),u),u),f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y)))),y)),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))))) = f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z),f(f(f(f(f(y,f(y,y)),z),z),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y))))),f(x,f(y,f(y,y)))),f(y,f(y,y)))),y). [para(2986(a,1),3377(a,1,1,1,2,1))]. Demod_limit (steps=-1, size=1049). The most recent kept clause is 3390. From here on, a short message will be printed for each 100 times the limit is hit. given #258 (T,wt=25): 2483 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(2285(a,1),2(a,1,2,1))]. given #259 (T,wt=19): 3414 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y. [para(2387(a,1),2483(a,1,2,2)),rewrite(82(15))]. given #260 (T,wt=15): 3482 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y). [para(2359(a,1),3414(a,1,2,1,1)),rewrite(2285(3),77(5),77(9),46(7),77(4))]. given #261 (T,wt=15): 3523 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x). [para(82(a,1),3482(a,1,2,2)),rewrite(82(9))]. given #262 (A,wt=43): 86 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(77(a,1),8(a,1,2,2,1,1))]. given #263 (F,wt=39): 3486 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(2750(a,1),3414(a,1,2,1,1))]. given #264 (F,wt=39): 3649 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(82(a,1),3486(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(2484(4),82(11),82(16))]. given #265 (F,wt=39): 3652 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(91(a,1),3486(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(2489(4),91(11),91(16))]. given #266 (F,wt=47): 3677 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(3482(a,1),3486(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(3482(16),3482(21))]. given #267 (T,wt=19): 3449 f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y. [para(82(a,1),3414(a,1,2,1,1,1)),rewrite(2484(4))]. given #268 (T,wt=19): 3450 f(f(x,y),f(f(f(f(y,x),f(z,y)),f(z,y)),y)) = y. [para(82(a,1),3414(a,1,2,1,1,2)),rewrite(82(8))]. given #269 (T,wt=19): 3451 f(f(x,y),f(f(f(f(x,y),f(x,z)),f(x,z)),x)) = x. [para(91(a,1),3414(a,1,2,1,1,1)),rewrite(2489(4))]. given #270 (T,wt=19): 3454 f(f(f(f(x,f(x,x)),f(x,y)),f(x,y)),x) = f(x,x). [para(3414(a,1),60(a,1,2,2,1)),rewrite(2286(9),2484(16),3226(18)),flip(a)]. given #271 (A,wt=59): 87 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(y,v),v),f(y,z)),f(f(y,z),w)))))) = f(y,z). [para(77(a,1),8(a,1,2,2,2,2,1,1,1,1))]. given #272 (F,wt=43): 3858 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(3652(a,1),3450(a,1,2,1,1))]. given #273 (F,wt=43): 3928 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(82(a,1),3858(a,1,2,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(2484(4),82(11),82(16))]. given #274 (F,wt=43): 3929 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(91(a,1),3858(a,1,2,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(2489(4),91(11),91(16))]. given #275 (F,wt=47): 3679 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(3523(a,1),3486(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(3523(16),3523(21))]. given #276 (T,wt=19): 3566 f(f(x,x),f(f(f(x,x),x),f(x,y))) = f(f(x,x),x). [para(3482(a,1),2396(a,1,2,2))]. given #277 (T,wt=19): 3751 f(f(x,y),f(f(f(f(x,y),f(z,y)),f(z,y)),y)) = y. [para(82(a,1),3449(a,1,2,1,1,2)),rewrite(82(8))]. given #278 (T,wt=19): 3766 f(f(f(f(f(x,x),x),f(x,y)),f(x,y)),x) = f(x,x). [para(3449(a,1),63(a,1,2,2,1)),rewrite(2286(9),2484(16),20(9)),flip(a)]. given #279 (T,wt=19): 3794 f(f(x,y),f(f(f(f(x,y),f(z,x)),f(z,x)),x)) = x. [para(91(a,1),3450(a,1,2,1,1,1)),rewrite(2489(4))]. given #280 (A,wt=43): 88 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),f(f(y,u),f(y,u))),f(f(f(y,u),y),f(y,v)))))) = y. [para(77(a,1),8(a,1,2,2,2,2,1,1))]. given #281 (F,wt=47): 3971 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(3929(a,1),3450(a,1,2,1,1))]. given #282 (F,wt=47): 4085 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(3928(a,1),3751(a,1,2,1,1))]. given #283 (F,wt=47): 4135 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(3929(a,1),3794(a,1,2,1,1))]. given #284 (F,wt=49): 3383 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(82(a,1),3377(a,1,1,1,2,2)),rewrite(2285(8),2286(3),2285(10),82(13),82(15),82(16),82(21),82(26))]. given #285 (T,wt=19): 3797 f(f(f(f(x,f(x,x)),f(y,x)),f(y,x)),x) = f(x,x). [para(3450(a,1),60(a,1,2,2,1)),rewrite(2286(9),2484(16),3227(18)),flip(a)]. given #286 (T,wt=19): 3906 f(x,f(f(f(x,f(x,x)),f(x,y)),f(x,y))) = f(x,x). [para(3454(a,1),2489(a,1,1,1)),rewrite(3454(8),2285(3),3454(14))]. given #287 (T,wt=19): 3996 f(x,f(f(x,f(x,x)),f(f(x,x),y))) = f(x,f(x,x)). [para(20(a,1),3566(a,1,1)),rewrite(2285(3),2285(9))]. given #288 (T,wt=19): 3999 f(f(x,x),f(f(f(x,x),x),f(y,x))) = f(f(x,x),x). [para(82(a,1),3566(a,1,2,2))]. given #289 (A,wt=59): 89 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(f(f(y,z),w),v),v),f(y,z)),y))))) = f(y,z). [para(77(a,1),8(a,1,2,2,2,2,2))]. given #290 (F,wt=49): 3384 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(91(a,1),3377(a,1,1,1,2,2)),rewrite(2285(8),2285(3),2285(10),91(13),91(15),91(16),91(21),91(26))]. given #291 (F,wt=49): 3499 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(2984(a,1),3414(a,1,2,1,1))]. given #292 (F,wt=49): 3643 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(20(a,1),3486(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(2286(3),20(14),20(19))]. given #293 (F,wt=49): 3646 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(77(a,1),3486(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(2285(3),77(14),77(19))]. given #294 (T,wt=19): 4063 f(f(f(f(f(x,x),x),f(y,x)),f(y,x)),x) = f(x,x). [para(3751(a,1),63(a,1,2,2,1)),rewrite(2286(9),2484(16),20(9)),flip(a)]. given #295 (T,wt=19): 4094 f(x,f(f(f(f(x,x),x),f(x,y)),f(x,y))) = f(x,x). [para(3766(a,1),2489(a,1,1,1)),rewrite(3766(8),2285(3),3766(14))]. given #296 (T,wt=19): 4218 f(x,f(f(f(x,f(x,x)),f(y,x)),f(y,x))) = f(x,x). [para(3797(a,1),2489(a,1,1,1)),rewrite(3797(8),2285(3),3797(14))]. given #297 (T,wt=19): 4239 f(x,f(f(x,f(x,x)),f(y,f(x,x)))) = f(x,f(x,x)). [para(82(a,1),3996(a,1,2,2))]. given #298 (A,wt=45): 93 f(f(x,y),f(f(z,f(y,y)),f(f(f(f(f(y,x),f(f(z,f(y,y)),f(z,f(y,y)))),f(f(z,f(y,y)),f(z,f(y,y)))),y),f(y,u)))) = y. [para(82(a,1),2(a,1,2,1))]. given #299 (F,wt=49): 3705 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(3649(a,1),2743(a,1,2,1)),rewrite(3649(19),3649(36),3649(41))]. given #300 (F,wt=49): 3730 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(3652(a,1),2743(a,1,2,1)),rewrite(3652(19),3652(36),3652(41))]. given #301 (F,wt=49): 3775 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(2985(a,1),3449(a,1,2,1,1))]. given #302 (F,wt=49): 3887 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(2984(a,1),3451(a,1,2,1,1))]. given #303 (T,wt=19): 4355 f(x,f(f(f(f(x,x),x),f(y,x)),f(y,x))) = f(x,x). [para(4063(a,1),2489(a,1,1,1)),rewrite(4063(8),2285(3),4063(14))]. given #304 (T,wt=21): 3522 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y). [para(20(a,1),3482(a,1,2,1,1))]. given #305 (T,wt=21): 3576 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)). [para(20(a,1),3523(a,1,2,1,1))]. given #306 (T,wt=23): 3437 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),3414(a,1,2,1,1,2)),rewrite(2(16))]. given #307 (A,wt=45): 95 f(f(x,y),f(f(f(y,y),f(f(z,f(y,x)),f(z,f(y,x)))),f(f(f(f(z,f(y,x)),f(f(z,f(y,x)),f(z,f(y,x)))),y),f(y,u)))) = y. [para(82(a,1),2(a,1,2,2,1,1,1))]. given #308 (F,wt=51): 3940 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(3482(a,1),3858(a,1,2,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(3482(16),3482(21))]. given #309 (F,wt=51): 3941 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(3523(a,1),3858(a,1,2,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(3523(16),3523(21))]. given #310 (F,wt=51): 4175 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(3971(a,1),3751(a,1,2,1,1))]. given #311 (F,wt=51): 4193 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(4085(a,1),3751(a,1,2,1,1))]. given #312 (T,wt=15): 4566 f(x,f(f(f(x,y),y),f(x,y))) = f(x,y). [para(77(a,1),3437(a,1,2,1,1,1)),rewrite(2285(3))]. given #313 (T,wt=23): 3443 f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x). [para(20(a,1),3414(a,1,2,1,1,1)),rewrite(2286(3))]. given #314 (T,wt=15): 4863 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x). [para(77(a,1),3443(a,1,2,1,1,2)),rewrite(77(4))]. given #315 (T,wt=11): 4935 f(f(x,x),x) = f(x,f(x,x)). [para(55(a,1),4863(a,1,2,1)),rewrite(2285(5))]. given #316 (A,wt=37): 99 f(f(f(f(f(x,y),f(x,y)),z),f(f(f(f(f(f(x,y),u),z),z),f(x,y)),y)),f(f(x,y),f(x,y))) = f(x,y). [para(7(a,1),82(a,1,2,1)),rewrite(7(28),7(31))]. given #317 (F,wt=35): 4792 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(2288(a,1),4566(a,1,2,1,1)),rewrite(2288(23),2288(26))]. given #318 (F,wt=29): 6077 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),4792(a,1,2,1,1)),rewrite(2(12),2(12),2(17),2(22),2(24))]. given #319 (F,wt=29): 6081 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(77(a,1),4792(a,1,2,1,1)),rewrite(77(4),77(4),77(9),77(14),77(16))]. given #320 (F,wt=33): 6165 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(6077(a,1),3751(a,1,2,1,1))]. given #321 (T,wt=15): 5028 f(x,f(f(x,f(x,x)),f(y,x))) = f(y,x). [para(4863(a,1),3482(a,1,2,2)),rewrite(4935(2),4863(10))]. given #322 (T,wt=15): 5030 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y). [para(3482(a,1),4863(a,1,2,2)),rewrite(4935(2),4935(6),3750(13),4935(3)),flip(a)]. given #323 (T,wt=19): 5043 f(f(x,x),f(f(x,f(x,x)),f(y,x))) = f(x,f(x,x)). [para(4863(a,1),3566(a,1,2,2)),rewrite(4935(3),4935(8))]. given #324 (T,wt=19): 5045 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)). [para(3566(a,1),4863(a,1,2,2)),rewrite(4935(2),4935(6),4935(14),3863(16),4935(5)),flip(a)]. given #325 (A,wt=41): 101 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(v,y),u),u),y),f(y,w)))))) = y. [para(82(a,1),8(a,1,2,2,2,2,1,1,1,1))]. given #326 (F,wt=33): 6227 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(6081(a,1),3450(a,1,2,1,1))]. given #327 (F,wt=33): 6234 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(6081(a,1),3794(a,1,2,1,1))]. given #328 (F,wt=35): 4794 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(2353(a,1),4566(a,1,2,1,1)),rewrite(2353(23),2353(26))]. given #329 (F,wt=37): 6295 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(6165(a,1),3751(a,1,2,1,1))]. given #330 (T,wt=19): 6008 f(f(x,y),f(f(f(y,x),f(f(y,x),f(y,x))),y)) = y. [para(4935(a,1),3414(a,1,2,1))]. given #331 (T,wt=19): 6016 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = x. [para(4935(a,1),3451(a,1,2,1))]. given #332 (T,wt=19): 6023 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),y)) = y. [para(4935(a,1),3751(a,1,2,1))]. given #333 (T,wt=21): 4936 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = x. [para(4863(a,1),69(a,1,2,2,2)),rewrite(4935(3),4935(5))]. given #334 (A,wt=41): 102 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(w,y)))))) = y. [para(82(a,1),8(a,1,2,2,2,2,2))]. given #335 (F,wt=37): 6409 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(6227(a,1),3751(a,1,2,1,1))]. given #336 (F,wt=37): 6473 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(6234(a,1),3794(a,1,2,1,1))]. given #337 (F,wt=39): 6146 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(6077(a,1),2743(a,1,2,1)),rewrite(6077(14),6077(26),6077(31))]. given #338 (F,wt=39): 6216 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(6081(a,1),2743(a,1,2,1)),rewrite(6081(14),6081(26),6081(31))]. given #339 (T,wt=21): 4938 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(x,x)) = x. [para(4863(a,1),210(a,1,1,2,2)),rewrite(4935(2),4935(4))]. given #340 (T,wt=21): 4939 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = x. [para(210(a,1),4863(a,1,2,2)),rewrite(4935(4),4935(6),4935(12),4935(14),2286(20),4935(2),4935(4),4937(9)),flip(a)]. given #341 (T,wt=21): 5000 f(x,f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),y))) = f(x,y). [para(2509(a,1),4863(a,1,2,2)),rewrite(4935(3),4935(10),3868(19),4935(4)),flip(a)]. given #342 (T,wt=21): 5002 f(x,f(f(y,x),f(f(f(x,f(x,x)),f(y,x)),x))) = f(y,x). [para(2598(a,1),4863(a,1,2,2)),rewrite(4935(3),4935(10),3863(19),4935(4)),flip(a)]. given #343 (A,wt=41): 103 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(f(f(x,x),u),f(f(f(f(f(x,v),u),u),x),f(x,w))))),f(x,x)) = x. [para(8(a,1),82(a,1,2,1)),rewrite(8(36),8(38))]. given #344 (F,wt=41): 4796 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(2359(a,1),4566(a,1,2,1,1)),rewrite(2359(29),2359(32))]. given #345 (F,wt=41): 6079 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(55(a,1),4792(a,1,2,1,1)),rewrite(55(6),55(7),2285(6),55(11),55(18),55(21))]. given #346 (F,wt=41): 6423 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(4566(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(4566(16))]. given #347 (F,wt=41): 6427 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(4863(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(4863(16))]. given #348 (T,wt=21): 5006 f(x,f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),x))) = f(x,y). [para(2785(a,1),4863(a,1,2,2)),rewrite(4935(3),4935(10),3868(19),4935(4)),flip(a)]. given #349 (T,wt=21): 5956 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x)) = x. [back_rewrite(4937),rewrite(4939(18))]. given #350 (T,wt=23): 3447 f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y). [para(77(a,1),3414(a,1,2,1,1,1)),rewrite(2285(3))]. given #351 (T,wt=23): 3448 f(f(x,f(y,z)),f(f(f(f(f(y,z),x),y),y),f(y,z))) = f(y,z). [para(77(a,1),3414(a,1,2,1,1,2)),rewrite(77(8))]. given #352 (A,wt=57): 108 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),y),f(y,v)))) = y. [para(82(a,1),4(a,1,2,2,1,1,1,2,2,2)),rewrite(82(22))]. given #353 (F,wt=41): 6434 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(5028(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(5028(16))]. given #354 (F,wt=41): 6435 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(5030(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(5030(16))]. given #355 (F,wt=41): 6557 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(6295(a,1),3751(a,1,2,1,1))]. given #356 (F,wt=41): 6857 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(6409(a,1),3751(a,1,2,1,1))]. given #357 (T,wt=23): 3746 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),3449(a,1,2,1,1,2)),rewrite(2(16))]. given #358 (T,wt=23): 3750 f(f(x,f(y,z)),f(f(f(f(x,f(y,z)),y),y),f(y,z))) = f(y,z). [para(77(a,1),3449(a,1,2,1,1,2)),rewrite(77(8))]. given #359 (T,wt=23): 3764 f(f(f(f(x,f(x,x)),f(f(x,x),y)),f(f(x,x),y)),f(x,x)) = x. [para(3449(a,1),45(a,1,2,2,1)),rewrite(2387(11),2484(24),2285(14),46(12),2285(3)),flip(a)]. given #360 (T,wt=23): 3791 f(x,f(f(f(x,f(y,f(z,x))),f(y,f(z,x))),f(z,x))) = f(z,x). [para(20(a,1),3450(a,1,2,1,1,1)),rewrite(2286(3))]. given #361 (A,wt=57): 109 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(v,y)))) = y. [para(82(a,1),4(a,1,2,2,2))]. given #362 (F,wt=41): 6907 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(6473(a,1),3794(a,1,2,1,1))]. given #363 (F,wt=43): 4791 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(4566(a,1),2288(a,1,2,2,1,1,1))]. given #364 (F,wt=43): 4793 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(4566(a,1),2353(a,1,2,2,1,1,1))]. given #365 (F,wt=43): 4983 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(4863(a,1),2288(a,1,2,2,1,1,1))]. given #366 (T,wt=23): 3793 f(x,f(f(f(x,f(y,f(x,z))),f(y,f(x,z))),f(x,z))) = f(x,z). [para(77(a,1),3450(a,1,2,1,1,1)),rewrite(2285(3))]. given #367 (T,wt=23): 3863 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),3451(a,1,2,1,1,2)),rewrite(2(16))]. given #368 (T,wt=23): 3868 f(f(f(x,y),z),f(f(f(f(f(x,y),z),x),x),f(x,y))) = f(x,y). [para(77(a,1),3451(a,1,2,1,1,2)),rewrite(77(8))]. given #369 (T,wt=23): 3899 f(f(x,y),f(f(y,f(f(f(f(y,x),f(y,z)),f(y,z)),y)),y)) = y. [para(3451(a,1),3450(a,1,2,1,1))]. given #370 (A,wt=55): 110 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(z,v),v),f(y,z)),z))))) = f(y,z). [para(44(a,1),7(a,1,1,2)),rewrite(44(16),44(17),44(20),44(24),44(39))]. given #371 (F,wt=43): 4986 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(4863(a,1),2353(a,1,2,2,1,1,1))]. given #372 (F,wt=43): 6107 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(4792(a,1),4566(a,1,2,1,1)),rewrite(4792(31),4792(34))]. given #373 (F,wt=43): 6186 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(6077(a,1),6077(a,1,2,1,2,2,1,1,1)),rewrite(2286(14))]. given #374 (F,wt=43): 6251 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(6081(a,1),6081(a,1,2,1,2,2,1,1,1)),rewrite(2286(14))]. given #375 (T,wt=23): 4061 f(f(f(f(x,f(x,x)),f(y,f(x,x))),f(y,f(x,x))),f(x,x)) = x. [para(3751(a,1),45(a,1,2,2,1)),rewrite(2387(11),2484(24),2285(14),46(12),2285(3)),flip(a)]. given #376 (T,wt=23): 4081 f(f(x,y),f(f(y,f(f(f(f(x,y),f(y,z)),f(y,z)),y)),y)) = y. [para(3449(a,1),3751(a,1,2,1,1))]. given #377 (T,wt=23): 4083 f(f(x,y),f(f(y,f(f(f(f(y,x),f(z,y)),f(z,y)),y)),y)) = y. [para(3450(a,1),3751(a,1,2,1,1))]. given #378 (T,wt=23): 4087 f(f(x,y),f(f(y,f(f(f(f(x,y),f(z,y)),f(z,y)),y)),y)) = y. [para(3751(a,1),3751(a,1,2,1,1))]. given #379 (A,wt=33): 116 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(44(a,1),82(a,1,2,1)),rewrite(44(25),44(28))]. given #380 (F,wt=43): 6275 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(2286(a,1),6165(a,1,1)),rewrite(2286(9),2286(13))]. given #381 (F,wt=43): 6282 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(6165(a,1),2743(a,1,2,1)),rewrite(6165(16),6165(30),6165(35))]. given #382 (F,wt=43): 6460 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(6234(a,1),2743(a,1,2,1)),rewrite(6234(16),6234(30),6234(35))]. given #383 (F,wt=43): 6575 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(6008(a,1),7(a,1,2,2,1,1,1,1))]. given #384 (T,wt=23): 4132 f(f(x,y),f(f(x,f(f(f(f(x,y),f(x,z)),f(x,z)),x)),x)) = x. [para(3451(a,1),3794(a,1,2,1,1))]. given #385 (T,wt=23): 4136 f(f(x,y),f(f(x,f(f(f(f(x,y),f(z,x)),f(z,x)),x)),x)) = x. [para(3794(a,1),3794(a,1,2,1,1))]. given #386 (T,wt=23): 4363 f(f(x,x),f(f(f(x,f(x,x)),f(f(x,x),y)),f(f(x,x),y))) = x. [para(20(a,1),4094(a,1,2,1,1,1)),rewrite(2285(13))]. given #387 (T,wt=23): 4470 f(f(x,x),f(f(f(x,f(x,x)),f(y,f(x,x))),f(y,f(x,x)))) = x. [para(20(a,1),4355(a,1,2,1,1,1)),rewrite(2285(13))]. given #388 (A,wt=45): 120 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(91(a,1),2(a,1,2,1))]. given #389 (F,wt=43): 6686 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(6016(a,1),81(a,1,2,2,1,1,1,1))]. given #390 (F,wt=43): 6721 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(6023(a,1),7(a,1,2,2,1,1,1,1))]. given #391 (F,wt=43): 6985 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(6216(a,1),3414(a,1,2,1,1))]. given #392 (F,wt=45): 6865 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(4566(a,1),6409(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(4566(16))]. given #393 (T,wt=23): 4854 f(x,f(f(f(x,y),f(f(f(x,y),y),f(x,y))),f(x,y))) = f(x,y). [para(4566(a,1),4566(a,1,2,1,1)),rewrite(4566(11),4566(14))]. given #394 (T,wt=23): 4944 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [para(4863(a,1),577(a,1,1,2,2)),rewrite(4935(4))]. given #395 (T,wt=23): 4945 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [para(577(a,1),4863(a,1,2,2)),rewrite(4935(6),4935(15),2286(22),4935(4)),flip(a)]. given #396 (T,wt=23): 5013 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [para(4863(a,1),2725(a,1,2,2,2)),rewrite(4935(5))]. given #397 (A,wt=45): 122 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(91(a,1),2(a,1,2,2,1,1,1))]. given #398 (F,wt=45): 6867 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(4863(a,1),6409(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(4863(16))]. given #399 (F,wt=45): 6873 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(5028(a,1),6409(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(5028(16))]. given #400 (F,wt=45): 6874 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(5030(a,1),6409(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(5030(16))]. given #401 (F,wt=45): 7384 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(6557(a,1),3751(a,1,2,1,1))]. given #402 (T,wt=23): 5014 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(2725(a,1),4863(a,1,2,2)),rewrite(4935(4),4935(12),4945(18),46(11),4945(10),4935(5)),flip(a)]. given #403 (T,wt=23): 5065 f(x,f(f(f(y,x),f(f(f(x,y),y),f(y,x))),f(y,x))) = f(y,x). [para(4863(a,1),4566(a,1,2,1,1)),rewrite(4863(11),4863(14))]. given #404 (T,wt=23): 5089 f(x,f(f(f(y,x),f(f(x,f(x,x)),f(y,x))),f(y,x))) = f(y,x). [back_rewrite(4828),rewrite(4935(3))]. given #405 (T,wt=23): 5090 f(x,f(f(f(x,y),f(f(x,f(x,x)),f(x,y))),f(x,y))) = f(x,y). [back_rewrite(4827),rewrite(4935(3))]. given #406 (A,wt=53): 188 f(f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),v)))) = f(y,x). [para(20(a,1),5(a,1,1,1,2,1,1,1))]. given #407 (F,wt=45): 7412 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(6857(a,1),3751(a,1,2,1,1))]. given #408 (F,wt=45): 7590 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(6907(a,1),3794(a,1,2,1,1))]. given #409 (F,wt=47): 4831 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(4566(a,1),3486(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(4566(16),4566(21))]. given #410 (F,wt=47): 5034 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(4863(a,1),3486(a,1,2,1,2,2,1,1,2,2,1,1,1,1)),rewrite(4863(16),4863(21))]. given #411 (T,wt=23): 6632 f(f(x,y),f(f(y,f(f(f(y,x),f(f(y,x),f(y,x))),y)),y)) = y. [para(6008(a,1),3751(a,1,2,1,1))]. given #412 (T,wt=23): 6698 f(f(x,y),f(f(x,f(f(f(x,y),f(f(x,y),f(x,y))),x)),x)) = x. [para(6016(a,1),3794(a,1,2,1,1))]. given #413 (T,wt=23): 6753 f(f(x,y),f(f(y,f(f(f(x,y),f(f(x,y),f(x,y))),y)),y)) = y. [para(6023(a,1),3751(a,1,2,1,1))]. given #414 (T,wt=25): 2506 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y)))) = y. [para(2285(a,1),96(a,1,2,1))]. given #415 (A,wt=55): 192 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),v)))) = f(y,x). [para(77(a,1),5(a,1,1,1,2,1,1))]. given #416 (F,wt=47): 5035 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(4863(a,1),3677(a,1,1,1,2)),rewrite(4935(2),4863(12),4863(16),4863(21))]. given #417 (F,wt=47): 5036 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(3677(a,1),4863(a,1,2,2)),rewrite(4935(34),4935(40),3751(46),4935(2)),flip(a)]. given #418 (F,wt=47): 6310 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(6165(a,1),6077(a,1,2,1,2,2,1,1,1)),rewrite(2286(16))]. given #419 (F,wt=47): 6311 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(6077(a,1),6165(a,1,2,1,2,1,2,2,1,1,1)),rewrite(2286(14))]. given #420 (T,wt=25): 2527 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(u,y)))) = y. [back_rewrite(661),rewrite(2484(4))]. given #421 (T,wt=25): 2530 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(94),rewrite(2484(4))]. given #422 (T,wt=25): 2573 f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))) = x. [back_rewrite(665),rewrite(2489(4))]. given #423 (T,wt=25): 2580 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(121),rewrite(2489(4))]. given #424 (A,wt=51): 194 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),f(x,x)),f(f(x,f(z,x)),f(f(z,x),v)))) = f(z,x). [para(77(a,1),5(a,1,2,2,1,1))]. given #425 (F,wt=47): 6391 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(2743(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2743(22))]. given #426 (F,wt=47): 6392 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(2786(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(2786(22))]. given #427 (F,wt=47): 6431 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(6227(a,1),6077(a,1,2,1,2,2,1,1,1)),rewrite(2286(16))]. given #428 (F,wt=47): 6432 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(6081(a,1),6227(a,1,2,1,2,1,2,2,1,1,1)),rewrite(2286(14))]. given #429 (T,wt=25): 2581 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(2286(a,1),2(a,1,2,1))]. given #430 (T,wt=25): 2595 f(f(x,y),f(y,f(f(f(f(f(y,x),f(z,y)),f(z,y)),y),f(u,y)))) = y. [para(2286(a,1),96(a,1,2,1))]. given #431 (T,wt=25): 2705 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),2484(a,1,1,1)),rewrite(2(11),2(22))]. given #432 (T,wt=25): 2720 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(39(a,1),2484(a,1,1,1)),rewrite(39(11),39(22))]. given #433 (A,wt=49): 195 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),z))) = f(z,x). [para(77(a,1),5(a,1,2,2,2))]. given #434 (F,wt=47): 6487 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(6234(a,1),6081(a,1,2,1,2,2,1,1,1)),rewrite(2286(16))]. given #435 (F,wt=47): 6488 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(6081(a,1),6234(a,1,2,1,2,1,2,2,1,1,1)),rewrite(2286(14))]. given #436 (F,wt=47): 7011 f(f(f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),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(5000(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(5000(22))]. given #437 (F,wt=47): 7019 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(5002(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(5002(22))]. given #438 (T,wt=25): 2727 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x)))) = x. [para(96(a,1),2484(a,1,1,1)),rewrite(96(11),96(22))]. given #439 (T,wt=25): 2728 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(399(a,1),2484(a,1,1,1)),rewrite(399(11),399(22))]. given #440 (T,wt=25): 2776 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(x,u)))) = x. [para(747(a,1),2489(a,1,1,1)),rewrite(747(11),747(22))]. given #441 (T,wt=25): 2777 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(u,x)))) = x. [para(856(a,1),2489(a,1,1,1)),rewrite(856(11),856(22))]. given #442 (A,wt=37): 196 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),82(a,1,2,1)),rewrite(5(37),5(40))]. given #443 (F,wt=47): 7130 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(5006(a,1),6227(a,1,2,1,2,1,2,2,1,1,1,1)),rewrite(5006(22))]. given #444 (F,wt=47): 8217 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(6460(a,1),3414(a,1,2,1,1))]. given #445 (F,wt=47): 8898 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(6632(a,1),7(a,1,2,2,1,1,1,1))]. given #446 (F,wt=47): 9039 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(6698(a,1),81(a,1,2,2,1,1,1,1))]. given #447 (T,wt=25): 3195 f(f(f(x,x),y),f(f(f(f(f(x,f(x,x)),y),y),x),f(x,z))) = f(x,x). [para(20(a,1),2380(a,1,2,1,1,1,1,1)),rewrite(2285(9),2285(10))]. given #448 (T,wt=21): 10614 f(f(f(f(f(f(x,f(x,x)),y),y),x),f(x,z)),x) = f(x,x). [para(3195(a,1),82(a,1,2,1)),rewrite(3195(18),2285(10),3195(18))]. given #449 (T,wt=15): 10677 f(f(f(f(x,f(x,x)),y),y),x) = f(x,x). [para(2387(a,1),10614(a,1,1)),rewrite(2484(12))]. given #450 (T,wt=15): 10706 f(f(f(f(x,f(x,x)),y),y),f(x,x)) = x. [para(20(a,1),10677(a,1,1,1,1,2)),rewrite(4935(2),2285(9))]. given #451 (A,wt=53): 197 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),f(f(z,x),w)))) = f(z,x). [para(82(a,1),5(a,1,1,1,2,2))]. given #452 (F,wt=47): 9084 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(6753(a,1),7(a,1,2,2,1,1,1,1))]. given #453 (F,wt=49): 4795 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(4566(a,1),2359(a,1,2,1))]. given #454 (F,wt=49): 4988 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(4863(a,1),2359(a,1,2,1))]. given #455 (F,wt=49): 5050 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(3383(a,1),4863(a,2)),rewrite(4935(25),4935(37),4935(49),4863(68))]. given #456 (T,wt=11): 10878 f(x,f(x,f(x,y))) = f(x,y). [back_rewrite(7663),rewrite(10806(8))]. given #457 (T,wt=11): 10879 f(x,f(x,f(y,x))) = f(y,x). [back_rewrite(7560),rewrite(10806(8))]. given #458 (T,wt=11): 11022 f(f(x,y),f(f(x,y),y)) = y. [para(2(a,1),10878(a,1,2,2)),rewrite(2(15))]. given #459 (T,wt=11): 11032 f(f(x,y),f(f(x,y),x)) = x. [para(77(a,1),10878(a,1,2,2)),rewrite(77(7))]. given #460 (A,wt=53): 198 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),f(w,f(z,x))))) = f(z,x). [para(82(a,1),5(a,1,2,2,2))]. given #461 (F,wt=35): 11451 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(11022(a,1),7(a,1,2,2,1,1,1,1))]. given #462 (F,wt=35): 11648 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(11032(a,1),81(a,1,2,2,1,1,1,1))]. given #463 (F,wt=41): 11140 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(10878(a,1),6409(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(10878(12))]. given #464 (F,wt=41): 11349 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(10879(a,1),6409(a,1,2,1,2,1,2,1,2,2,1,1,1,1)),rewrite(10879(12))]. given #465 (T,wt=15): 11515 f(f(x,y),f(f(y,f(f(x,y),y)),y)) = y. [para(11022(a,1),3751(a,1,2,1,1))]. given #466 (T,wt=15): 11661 f(f(x,y),f(f(y,f(f(y,x),y)),y)) = y. [para(11032(a,1),3450(a,1,2,1,1))]. given #467 (T,wt=15): 11665 f(f(x,y),f(f(x,f(f(x,y),x)),x)) = x. [para(11032(a,1),3794(a,1,2,1,1))]. given #468 (T,wt=15): 11751 f(f(f(x,f(x,x)),y),y) = f(x,f(x,x)). [para(10677(a,1),11032(a,1,1)),rewrite(10677(6),10806(7),4935(2)),flip(a)]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(12459)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c_0, f ]). NOTE: sn=99, num_tables=183 NOTE: updating interpretation 1: c_0=1. given #469 (A,wt=47): 205 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(y,u),u),f(y,y)),f(f(y,y),v)))))) = f(y,y). [para(69(a,1),8(a,1,2,2,2,2,1,1,1,1)),rewrite(77(5),77(12))]. given #470 (F,wt=23): 13303 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(12550),rewrite(12616(9))]. given #471 (F,wt=23): 13306 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(12542),rewrite(12616(9))]. given #472 (F,wt=23): 13364 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(12374),rewrite(12616(9))]. given #473 (F,wt=25): 14531 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(13156),rewrite(13294(2),2285(3),2285(3),13294(3,R))]. given #474 (T,wt=7): 12616 f(x,f(x,x)) = c_0. [new_symbol(12459)]. given #475 (T,wt=7): 13294 f(c_0,x) = f(x,x). [back_rewrite(12565),rewrite(12616(4),12616(5),12616(8),13282(8),12798(5),12616(3)),flip(a)]. given #476 (T,wt=7): 13330 f(x,f(c_0,c_0)) = c_0. [back_rewrite(12480),rewrite(12616(2),12616(3),12616(4),2386(6),12616(6))]. given #477 (T,wt=7): 13333 f(c_0,f(x,x)) = x. [back_rewrite(12475),rewrite(12616(2),12616(5),13294(5),12616(5),13294(5),4935(5),12616(5),13294(5),2727(14),55(4))]. given #478 (A,wt=43): 242 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,z),f(f(f(f(f(f(x,x),u),z),z),f(x,x)),f(f(x,x),v)))))) = f(x,x). [para(230(a,1),8(a,1,2,2,1,1,1,1)),rewrite(77(5),77(3),77(8))]. given #479 (F,wt=23): 16727 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(13294(a,2),96(a,1,2,2))]. given #480 (F,wt=23): 16744 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(13294(a,2),2527(a,1,2,2))]. given #481 (F,wt=23): 16745 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(13294(a,2),2573(a,1,2,2))]. given #482 (F,wt=25): 14536 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(13139),rewrite(13294(2),2285(3),2286(3),13294(3,R))]. given #483 (T,wt=7): 13352 f(f(c_0,c_0),x) = c_0. [back_rewrite(12416),rewrite(12616(2),12616(3),12616(6))]. given #484 (T,wt=7): 13353 f(x,c_0) = f(x,x). [back_rewrite(12412),rewrite(12616(2))]. given #485 (T,wt=7): 13354 f(f(x,x),c_0) = x. [back_rewrite(12410),rewrite(12616(3))]. given #486 (T,wt=7): 14396 f(f(x,x),x) = c_0. [back_rewrite(4935),rewrite(12616(4))]. given #487 (A,wt=57): 280 f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,v))),f(x,x)) = x. [para(6(a,1),82(a,1,2,1)),rewrite(6(52),6(54))]. given #488 (F,wt=25): 16238 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),13303(a,1,1)),rewrite(13294(3,R),2(15))]. given #489 (F,wt=25): 16244 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(77(a,1),13303(a,1,1)),rewrite(13294(3,R),77(7))]. given #490 (F,wt=25): 16796 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(20(a,1),16727(a,1,2,2,2,1,1,1)),rewrite(2286(3),13294(3,R))]. given #491 (F,wt=25): 16798 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(77(a,1),16727(a,1,2,2,2,1,1,1)),rewrite(2285(3),13294(3,R))]. given #492 (T,wt=11): 13428 f(x,f(f(f(x,y),y),c_0)) = c_0. [back_rewrite(11761),rewrite(12616(4),12616(7))]. given #493 (T,wt=11): 13472 f(x,f(f(f(x,x),y),c_0)) = c_0. [back_rewrite(10975),rewrite(12616(4),12616(7))]. given #494 (T,wt=11): 13474 f(f(f(f(x,x),y),c_0),x) = c_0. [back_rewrite(10973),rewrite(12616(4),12616(7))]. given #495 (T,wt=11): 13486 f(x,f(f(y,f(x,x)),c_0)) = c_0. [back_rewrite(10958),rewrite(12616(4),12616(7))]. given #496 (A,wt=57): 281 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))),y),f(y,v)))) = y. [para(82(a,1),6(a,1,2,1,2,2,2)),rewrite(82(22))]. given #497 (F,wt=27): 16286 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(13303(a,1),4566(a,1,2,1,1)),rewrite(13303(22),13303(24))]. given #498 (F,wt=27): 16423 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(13306(a,1),4566(a,1,2,1,1)),rewrite(13306(22),13306(24))]. given #499 (F,wt=27): 16563 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(13364(a,1),4566(a,1,2,1,1)),rewrite(13364(22),13364(24))]. given #500 (F,wt=27): 16638 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(10878(a,1),13364(a,1,2,2,1,1,1,1))]. given #501 (T,wt=11): 13488 f(f(f(x,f(y,y)),c_0),y) = c_0. [back_rewrite(10956),rewrite(12616(4),12616(7))]. given #502 (T,wt=11): 13494 f(f(x,x),f(f(y,x),c_0)) = c_0. [back_rewrite(10947),rewrite(12616(4),12616(7))]. given #503 (T,wt=11): 13498 f(f(f(x,y),c_0),f(y,y)) = c_0. [back_rewrite(10943),rewrite(12616(3),12616(7))]. given #504 (T,wt=11): 13515 f(f(x,x),f(f(x,y),c_0)) = c_0. [back_rewrite(10920),rewrite(12616(4),12616(7))]. given #505 (A,wt=37): 13177 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(10941),rewrite(12615(6),12616(3),12616(7))]. given #506 (F,wt=23): 19384 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(18956),rewrite(19221(3),10878(3),19222(5),19222(8),19304(8),19222(8),19222(11),19304(11),19222(6))]. given #507 (F,wt=23): 19857 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(17074),rewrite(19222(5),19222(8),19304(8),19222(9),19222(12),19304(12),19222(7))]. given #508 (F,wt=23): 19875 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(16988),rewrite(19222(5),19222(8),19304(8),19222(9),19222(12),19304(12),19222(7))]. given #509 (F,wt=23): 19889 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(16890),rewrite(19222(3),19222(5),19304(5),19222(2),19222(4),19304(4),19222(7))]. given #510 (T,wt=11): 13519 f(f(f(x,y),c_0),f(x,x)) = c_0. [back_rewrite(10916),rewrite(12616(3),12616(7))]. given #511 (T,wt=11): 14382 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(5045),rewrite(12616(3),12616(7))]. given #512 (T,wt=11): 14383 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_rewrite(5043),rewrite(12616(3),12616(7))]. given #513 (T,wt=11): 14387 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(5030),rewrite(12616(2))]. given #514 (A,wt=37): 13178 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(10914),rewrite(12615(6),12616(3),12616(7))]. given #515 (F,wt=25): 19752 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(17838),rewrite(19222(6),19222(8),19304(8),19222(5),19222(7),19304(7),19222(9),19222(11),19304(11),19222(8),19222(10),19304(10),19222(7))]. given #516 (F,wt=25): 19767 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(17738),rewrite(19222(6),19222(8),19304(8),19222(5),19222(7),19304(7),19222(9),19222(11),19304(11),19222(8),19222(10),19304(10),19222(7))]. given #517 (F,wt=25): 19833 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(17154),rewrite(19222(9),19222(14),19304(14),19222(10),19222(15),19304(15),19222(6))]. given #518 (F,wt=25): 19924 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(16681),rewrite(19222(9),19222(14),19304(14),19222(10),19222(15),19304(15),19222(6))]. given #519 (T,wt=11): 14389 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(5028),rewrite(12616(2))]. given #520 (T,wt=11): 14429 f(x,f(c_0,f(y,f(x,x)))) = c_0. [back_rewrite(4239),rewrite(12616(2),12616(7))]. given #521 (T,wt=11): 14431 f(x,f(c_0,f(f(x,x),y))) = c_0. [back_rewrite(3996),rewrite(12616(2),12616(7))]. given #522 (T,wt=11): 14553 f(c_0,f(c_0,f(x,y))) = f(x,y). [back_rewrite(12898),rewrite(13263(8),13294(4,R))]. given #523 (A,wt=37): 13234 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(2605),rewrite(12615(6),12616(3))]. given #524 (F,wt=27): 23517 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). [para(19857(a,1),19857(a,1,2,2,2,1,2)),rewrite(21945(12),19222(13),14387(15))]. given #525 (F,wt=27): 23523 f(f(x,y),f(y,f(f(f(f(y,y),z),f(c_0,f(f(z,f(f(x,y),z)),y))),y))) = y # label(false). [para(19875(a,1),19875(a,1,2,2,2,1,2)),rewrite(21944(12),19222(13),14387(15))]. given #526 (F,wt=27): 23529 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). [para(19857(a,1),19889(a,1,2,2,2,1,2)),rewrite(21945(12),19222(13),14387(15))]. given #527 (F,wt=27): 23659 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(21405),rewrite(23534(13))]. given #528 (T,wt=11): 15971 f(f(c_0,f(x,y)),x) = f(x,y). [back_rewrite(2489),rewrite(13294(3,R))]. given #529 (T,wt=11): 15973 f(f(c_0,f(x,y)),y) = f(x,y). [back_rewrite(2484),rewrite(13294(3,R))]. given #530 (T,wt=11): 18298 f(f(c_0,f(f(x,x),y)),x) = c_0. [para(13353(a,1),13474(a,1,1)),rewrite(13294(5,R))]. given #531 (T,wt=11): 19049 f(f(c_0,f(x,f(y,y))),y) = c_0. [para(13353(a,1),13488(a,1,1)),rewrite(13294(5,R))]. given #532 (A,wt=37): 13235 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(2518),rewrite(12615(6),12616(3))]. given #533 (F,wt=27): 23660 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(21402),rewrite(23534(13))]. given #534 (F,wt=27): 23663 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(21399),rewrite(23534(13))]. given #535 (F,wt=27): 24082 f(f(x,y),f(c_0,f(f(f(f(y,y),z),f(c_0,f(f(z,f(f(y,x),z)),y))),y))) = c_0 # label(false). [para(19857(a,1),23659(a,1,2,2,2,2,2,1,2)),rewrite(21945(13),19222(14),14387(16),10879(14))]. given #536 (F,wt=27): 24142 f(f(x,y),f(c_0,f(f(f(f(y,y),z),f(c_0,f(f(z,f(f(x,y),z)),y))),y))) = c_0 # label(false). [para(19875(a,1),23660(a,1,2,2,2,2,2,1,2)),rewrite(21944(13),19222(14),14387(16),10879(14))]. given #537 (T,wt=11): 19101 f(f(c_0,f(x,y)),f(x,x)) = c_0. [para(2285(a,1),13494(a,1,2,1)),rewrite(13294(3,R),13353(5))]. given #538 (T,wt=11): 19102 f(f(c_0,f(x,y)),f(y,y)) = c_0. [para(2286(a,1),13494(a,1,2,1)),rewrite(13294(3,R),13353(5))]. given #539 (T,wt=11): 19221 f(f(x,y),x) = f(x,f(x,y)). [back_rewrite(14873),rewrite(19101(6),14389(5))]. given #540 (T,wt=11): 19222 f(f(x,y),y) = f(y,f(x,y)). [back_rewrite(14830),rewrite(19101(6),14389(5))]. given #541 (A,wt=31): 13470 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(10977),rewrite(13294(3,R),12616(5))]. given #542 (F,wt=29): 19909 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(16815),rewrite(19222(3),19222(5),19304(5),19222(10))]. given #543 (F,wt=29): 21790 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(17044),rewrite(19222(8))]. given #544 (F,wt=29): 21829 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(16969),rewrite(19222(8))]. given #545 (F,wt=29): 21914 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(16795),rewrite(19222(8))]. given #546 (T,wt=11): 19228 f(f(x,y),f(x,f(x,y))) = x. [back_rewrite(14621),rewrite(19101(5),19221(4),10878(4),15971(4),19221(3),10878(4),19221(3))]. given #547 (T,wt=11): 19304 f(f(x,y),f(y,f(x,y))) = y. [back_rewrite(14625),rewrite(19102(5),19221(4),10879(4),15973(4),19222(3),10879(4),19222(3))]. given #548 (T,wt=11): 19419 f(f(x,y),f(y,f(y,x))) = y. [back_rewrite(18904),rewrite(19221(4),19221(5),10878(5),19221(4),19164(8),19221(3))]. given #549 (T,wt=11): 19696 f(x,f(c_0,f(y,f(x,y)))) = c_0. [back_rewrite(18120),rewrite(19222(4),19221(7),14553(7))]. given #550 (A,wt=31): 13471 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(10976),rewrite(13294(3,R),12616(5))]. given #551 (F,wt=29): 23655 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(21411),rewrite(23534(14))]. given #552 (F,wt=29): 23665 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(21397),rewrite(23534(14))]. given #553 (F,wt=29): 23667 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(21395),rewrite(23534(11),23534(15))]. given #554 (F,wt=29): 23669 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(21393),rewrite(23534(11),23534(15))]. given #555 (T,wt=11): 21388 f(f(c_0,f(x,f(y,x))),y) = c_0. [back_rewrite(18121),rewrite(19222(3))]. given #556 (T,wt=11): 23245 f(f(x,y),f(c_0,f(x,y))) = c_0. [back_rewrite(14294),rewrite(21751(9),19102(5)),flip(a)]. given #557 (T,wt=11): 23534 f(f(x,y),c_0) = f(c_0,f(x,y)). [para(14382(a,1),2286(a,1,2)),rewrite(13294(7,R),14553(5))]. given #558 (T,wt=11): 23776 f(f(x,y),f(c_0,f(y,x))) = c_0. [back_rewrite(19697),rewrite(23534(4))]. given #559 (A,wt=35): 13477 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(10968),rewrite(13294(3,R),12616(5),13294(17,R))]. given #560 (F,wt=27): 24681 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). [para(19857(a,1),21388(a,1,1,2,2)),rewrite(24268(11))]. given #561 (F,wt=27): 24683 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). [para(19875(a,1),21388(a,1,1,2,2)),rewrite(24269(11))]. given #562 (F,wt=27): 24684 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). [para(19889(a,1),21388(a,1,1,2,2)),rewrite(24268(11))]. given #563 (F,wt=27): 24717 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(19857(a,1),23776(a,1,1))]. given #564 (T,wt=11): 24707 f(f(c_0,f(x,y)),f(y,x)) = c_0. [para(19419(a,1),21388(a,1,1,2,2)),rewrite(19221(4),10878(4))]. given #565 (T,wt=11): 24716 f(f(x,y),f(x,f(y,x))) = x. [para(23776(a,1),19857(a,1,2,2,2,1,2)),rewrite(14383(6),19221(8),14553(8),19222(5),14553(7))]. given #566 (T,wt=13): 20715 f(x,f(f(x,y),f(y,x))) = f(x,y). [back_rewrite(11855),rewrite(19221(2),19222(4),19228(4),19222(4),19222(6),19304(6),19222(3),19222(5),19304(5))]. given #567 (T,wt=15): 16159 f(f(x,f(y,z)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(13161),rewrite(15971(7),13294(5,R))]. given #568 (A,wt=39): 13478 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(10966),rewrite(13294(3,R),12616(5),13294(19,R))]. given #569 (F,wt=27): 24719 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(19875(a,1),23776(a,1,1))]. given #570 (F,wt=27): 24721 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(19889(a,1),23776(a,1,1))]. given #571 (F,wt=27): 24891 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(24717(a,1),21388(a,1,1,2,2)),rewrite(19221(16),14553(16))]. given #572 (F,wt=27): 24899 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(19875(a,1),24707(a,1,2))]. given #573 (T,wt=15): 19231 f(x,f(c_0,f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(14590),rewrite(19221(2),10878(3),19221(2),19222(4),19228(4),19101(5))]. given #574 (T,wt=15): 20687 f(x,f(f(y,f(x,y)),f(y,x))) = f(y,x). [back_rewrite(11996),rewrite(19222(2),10879(3),19222(2),19222(4),19304(4),19222(2))]. given #575 (T,wt=15): 23246 f(f(f(x,y),z),f(c_0,f(x,y))) = f(x,y). [back_rewrite(14136),rewrite(23245(10),15973(7),13294(5,R))]. given #576 (T,wt=15): 24314 f(f(c_0,f(f(c_0,f(x,y)),z)),f(x,y)) = c_0. [para(23659(a,1),13470(a,1,2,1,1,2)),rewrite(13294(8,R),2285(11),13294(5,R),23659(20),23534(8),14389(12),23659(22))]. given #577 (A,wt=31): 13484 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(10960),rewrite(13294(3,R),12616(5))]. given #578 (F,wt=27): 24901 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(19889(a,1),24707(a,1,2))]. given #579 (F,wt=29): 24688 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). [para(19752(a,1),21388(a,1,1,2,2)),rewrite(24273(14))]. given #580 (F,wt=29): 24690 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). [para(19767(a,1),21388(a,1,1,2,2)),rewrite(24275(14))]. given #581 (F,wt=29): 24692 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). [para(19833(a,1),21388(a,1,1,2,2)),rewrite(24277(13))]. given #582 (T,wt=15): 24318 f(f(c_0,f(f(x,y),z)),f(c_0,f(x,y))) = c_0. [para(19101(a,1),13470(a,1,2,1,1,2)),rewrite(13294(14,R),14553(12),2285(11),13294(11,R),14553(9),19101(11),23534(8),14389(14),19101(13))]. given #583 (T,wt=15): 24755 f(x,f(c_0,f(f(x,f(x,y)),f(y,x)))) = c_0. [para(19419(a,1),23776(a,1,1))]. given #584 (T,wt=15): 24756 f(f(f(x,f(x,y)),f(y,x)),f(x,x)) = c_0. [para(19419(a,1),23776(a,1,2,2)),rewrite(13294(6))]. given #585 (T,wt=15): 24893 f(x,f(c_0,f(f(x,f(y,x)),f(x,y)))) = c_0. [para(23776(a,1),24717(a,1,2,2,1,2,2,1,2)),rewrite(14383(6),19221(8),14553(8),19222(5),14553(7))]. given #586 (A,wt=31): 13485 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(10959),rewrite(13294(3,R),12616(5))]. given #587 (F,wt=29): 24695 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). [para(19924(a,1),21388(a,1,1,2,2)),rewrite(24279(13))]. given #588 (F,wt=29): 24726 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(19752(a,1),23776(a,1,1))]. given #589 (F,wt=29): 24729 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(19767(a,1),23776(a,1,1))]. given #590 (F,wt=29): 24732 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(19833(a,1),23776(a,1,1))]. given #591 (T,wt=15): 24933 f(f(x,x),f(f(x,f(x,y)),f(y,x))) = c_0. [para(19419(a,1),24707(a,1,1,2)),rewrite(13294(2))]. given #592 (T,wt=15): 24934 f(f(c_0,f(f(x,f(x,y)),f(y,x))),x) = c_0. [para(19419(a,1),24707(a,1,2))]. given #593 (T,wt=15): 24982 f(f(f(x,f(y,x)),f(x,y)),f(x,x)) = c_0. [para(24716(a,1),23776(a,1,2,2)),rewrite(13294(6))]. given #594 (T,wt=15): 24985 f(f(x,x),f(f(x,f(y,x)),f(x,y))) = c_0. [para(24716(a,1),24707(a,1,1,2)),rewrite(13294(2))]. given #595 (A,wt=35): 13491 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(10951),rewrite(13294(3,R),12616(5),13294(17,R))]. given #596 (F,wt=29): 24735 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(19924(a,1),23776(a,1,1))]. given #597 (F,wt=29): 24906 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(19752(a,1),24707(a,1,2))]. given #598 (F,wt=29): 24909 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(19767(a,1),24707(a,1,2))]. given #599 (F,wt=29): 24912 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(19833(a,1),24707(a,1,2))]. given #600 (T,wt=15): 24986 f(f(c_0,f(f(x,f(y,x)),f(x,y))),x) = c_0. [para(24716(a,1),24707(a,1,2))]. given #601 (T,wt=15): 25062 f(f(c_0,f(x,y)),f(f(x,y),z)) = f(x,y). [para(16159(a,1),2386(a,1,2,1)),rewrite(13294(13,R),14553(11))]. given #602 (T,wt=15): 25063 f(f(c_0,f(x,y)),f(z,f(x,y))) = f(x,y). [para(16159(a,1),2387(a,1,2,2)),rewrite(13294(13,R),14553(11))]. given #603 (T,wt=15): 25068 f(f(x,y),f(c_0,f(f(c_0,f(x,y)),z))) = c_0. [para(16159(a,1),14382(a,1,1))]. given #604 (A,wt=39): 13492 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(10949),rewrite(13294(3,R),12616(5),13294(19,R))]. given #605 (F,wt=29): 24915 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(19924(a,1),24707(a,1,2))]. given #606 (F,wt=29): 24952 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(19752(a,1),24716(a,1,1))]. given #607 (F,wt=29): 24954 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(19767(a,1),24716(a,1,1))]. given #608 (F,wt=29): 24956 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(19833(a,1),24716(a,1,1))]. given #609 (T,wt=15): 25069 f(f(c_0,f(x,f(y,z))),f(c_0,f(y,z))) = c_0. [para(16159(a,1),14382(a,1,2,2)),rewrite(13294(5,R))]. given #610 (T,wt=15): 25070 f(f(x,y),f(c_0,f(z,f(c_0,f(x,y))))) = c_0. [para(16159(a,1),14383(a,1,1))]. given #611 (T,wt=15): 25073 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,y)))) = c_0. [para(16159(a,1),14429(a,1,2,2,2))]. given #612 (T,wt=15): 25074 f(f(c_0,f(x,y)),f(c_0,f(f(x,y),z))) = c_0. [para(16159(a,1),14431(a,1,2,2,1))]. given #613 (A,wt=37): 13499 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(10942),rewrite(13294(6,R),12616(7))]. given #614 (F,wt=29): 24958 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(19924(a,1),24716(a,1,1))]. given #615 (F,wt=29): 25613 f(f(c_0,f(x,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(2285(a,1),24692(a,1,1,2,1)),rewrite(2285(5),13294(3),2285(9))]. given #616 (F,wt=29): 25615 f(f(c_0,f(x,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(2286(a,1),24692(a,1,1,2,1)),rewrite(2286(5),13294(3),2286(9))]. given #617 (F,wt=29): 25936 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(24726(a,1),19889(a,1,2,2,2,1,2)),rewrite(14383(17),19221(19),14553(19),19222(16),14553(18))]. given #618 (T,wt=15): 25080 f(f(c_0,f(x,f(c_0,f(y,z)))),f(y,z)) = c_0. [para(16159(a,1),19102(a,1,2))]. given #619 (T,wt=15): 25268 f(f(f(x,f(x,y)),y),f(c_0,f(x,y))) = c_0. [para(19231(a,1),14383(a,1,2,2)),rewrite(13294(11,R),14553(7))]. given #620 (T,wt=15): 25297 f(f(c_0,f(x,y)),f(f(x,f(x,y)),y)) = c_0. [para(19231(a,1),19102(a,1,1,2)),rewrite(13294(14,R),14553(10))]. given #621 (T,wt=15): 27082 f(f(f(x,f(x,y)),y),x) = f(x,f(x,y)). [para(25268(a,1),19857(a,1,2,2,2,1,2)),rewrite(13294(8,R),25069(11),19221(10),14553(10),19228(9),13294(6),13333(6))]. given #622 (A,wt=37): 13520 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(10915),rewrite(13294(6,R),12616(7))]. given #623 (F,wt=29): 25943 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(24726(a,1),23659(a,1,2,2,2,2,2,1,2)),rewrite(14383(18),19221(20),14553(20),19222(17),14553(19),10879(16))]. given #624 (F,wt=29): 25961 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(24726(a,1),24684(a,1,1,2,2,2,2,1,2)),rewrite(14383(17),19221(19),14553(19),19222(16),14553(18),10879(15))]. given #625 (F,wt=29): 26025 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(2285(a,1),24732(a,1,1)),rewrite(2285(5),13294(3),2285(9))]. given #626 (F,wt=29): 26027 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(2286(a,1),24732(a,1,1)),rewrite(2286(5),13294(3),2286(9))]. given #627 (T,wt=15): 27084 f(f(f(x,f(x,y)),y),f(y,f(x,y))) = y. [para(25268(a,1),19875(a,1,2,2,2,1,2)),rewrite(14383(8),19221(10),14553(10),19222(7),14553(9))]. given #628 (T,wt=15): 27086 f(f(x,f(y,f(y,x))),y) = f(y,f(y,x)). [para(25268(a,1),19889(a,1,2,2,2,1,2)),rewrite(13294(8,R),25069(11),19221(10),14553(10),19228(9),13294(6),13333(6))]. given #629 (T,wt=15): 27096 f(f(x,f(y,f(y,x))),f(c_0,f(y,x))) = c_0. [para(25268(a,1),23659(a,1,2,2,2,2,2,1,2)),rewrite(13294(11,R),25069(14),19221(13),14553(13),19228(12),13294(9),13333(9),19221(7),10878(7))]. given #630 (T,wt=15): 27111 f(f(c_0,f(x,y)),f(y,f(x,f(x,y)))) = c_0. [para(25268(a,1),24684(a,1,1,2,2,2,2,1,2)),rewrite(13294(8,R),25069(11),19221(10),14553(10),19228(9),13294(6),13333(6),19221(4),10878(4))]. given #631 (A,wt=45): 14499 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(f(x,f(y,y)),u))),f(c_0,f(x,f(y,y)))) = f(x,f(y,y)). [back_rewrite(10519),rewrite(13294(5,R),13294(21,R))]. given #632 (F,wt=29): 26283 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(24735(a,1),19889(a,1,2,2,2,1,2)),rewrite(14383(16),19221(18),14553(18),19222(15),14553(17))]. given #633 (F,wt=29): 26286 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(24735(a,1),23659(a,1,2,2,2,2,2,1,2)),rewrite(14383(17),19221(19),14553(19),19222(16),14553(18),10879(15))]. given #634 (F,wt=29): 26298 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(24735(a,1),24684(a,1,1,2,2,2,2,1,2)),rewrite(14383(16),19221(18),14553(18),19222(15),14553(17),10879(14))]. given #635 (F,wt=29): 26409 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(2285(a,1),24912(a,1,1,2,1,1,1,2)),rewrite(13294(3),2285(9),2285(16))]. given #636 (T,wt=15): 27237 f(f(x,f(f(x,f(x,y)),y)),f(x,y)) = x. [para(27082(a,1),24716(a,1,2,2)),rewrite(10878(7))]. given #637 (T,wt=15): 27681 f(f(x,f(y,f(x,f(x,y)))),f(x,y)) = x. [para(27086(a,1),24716(a,1,2,2)),rewrite(10878(7))]. given #638 (T,wt=15): 27749 f(f(x,f(y,f(y,x))),f(x,f(y,x))) = x. [para(27096(a,1),19857(a,1,2,2,2,1,2)),rewrite(14383(8),19221(10),14553(10),19222(7),14553(9))]. given #639 (T,wt=17): 19248 f(f(x,y),f(c_0,f(f(y,f(x,y)),f(y,z)))) = y. [back_rewrite(15856),rewrite(19102(5),19221(4),10879(4),15973(4),19222(4))]. given #640 (A,wt=45): 14500 f(f(f(f(c_0,f(x,f(y,y))),f(y,z)),f(f(f(y,f(y,z)),f(x,f(y,y))),f(f(x,f(y,y)),u))),f(c_0,f(x,f(y,y)))) = f(x,f(y,y)). [back_rewrite(10518),rewrite(13294(5,R),13294(21,R))]. given #641 (F,wt=29): 26411 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(2286(a,1),24912(a,1,1,2,1,1,1,2)),rewrite(13294(3),2286(9),2286(16))]. given #642 (F,wt=31): 19886 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(16894),rewrite(19222(3),19221(8),10879(8),19222(11))]. given #643 (F,wt=31): 23241 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(19760),rewrite(21505(16))]. given #644 (F,wt=31): 23242 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(19775),rewrite(21559(16))]. given #645 (T,wt=15): 28455 f(f(f(x,f(y,x)),f(x,z)),f(x,x)) = c_0. [para(19248(a,1),14383(a,1,2,2)),rewrite(13294(13,R),14553(8),13294(6))]. given #646 (T,wt=13): 28879 f(f(f(x,y),f(x,z)),f(x,x)) = c_0. [para(19221(a,1),28455(a,1,1,1,2)),rewrite(10878(3))]. given #647 (T,wt=13): 28881 f(f(f(x,y),f(y,z)),f(y,y)) = c_0. [para(19222(a,1),28455(a,1,1,1,2)),rewrite(10879(3))]. given #648 (T,wt=13): 28928 f(f(f(x,y),f(z,x)),f(x,x)) = c_0. [para(10879(a,1),28879(a,1,1,2))]. given #649 (A,wt=41): 14504 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(8144),rewrite(13294(5,R),13294(19,R))]. given #650 (F,wt=31): 23315 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(20043),rewrite(22418(15))]. given #651 (F,wt=31): 23332 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(20045),rewrite(22420(15))]. given #652 (F,wt=31): 23645 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(21421),rewrite(23534(5),14553(6),23534(10),14553(11),23534(13),14553(14),23534(17),14553(18))]. given #653 (F,wt=31): 23650 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(21416),rewrite(23534(7),23534(13),23534(18),14553(19))]. given #654 (T,wt=13): 28952 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(28879(a,1),21388(a,1,1,2,2)),rewrite(23534(4),13333(4),13294(2))]. given #655 (T,wt=13): 28992 f(f(f(x,y),f(z,y)),f(y,y)) = c_0. [para(10879(a,1),28881(a,1,1,2))]. given #656 (T,wt=13): 29021 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [para(28881(a,1),21388(a,1,1,2,2)),rewrite(23534(4),13333(4),13294(2))]. given #657 (T,wt=13): 29022 f(f(x,x),f(f(x,y),f(z,x))) = c_0. [para(28881(a,1),24684(a,1,1,2,2,2,2,1,2)),rewrite(13294(5,R),19102(7),23534(7),13333(7),14553(8),19304(5),13294(2))]. given #658 (A,wt=41): 14505 f(f(f(f(c_0,f(x,f(y,y))),f(y,z)),f(f(f(y,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(8143),rewrite(13294(5,R),13294(19,R))]. given #659 (F,wt=31): 23651 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(21415),rewrite(23534(7),23534(14),14553(15),23534(14))]. given #660 (F,wt=31): 23652 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(21414),rewrite(23534(7),23534(13),23534(18),14553(19))]. given #661 (F,wt=31): 23653 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(21413),rewrite(23534(7),23534(14),14553(15),23534(14))]. given #662 (F,wt=31): 23654 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(21412),rewrite(23534(7),23534(13),14553(14))]. % Operation f is commutative; C redundancy checks enabled. given #663 (T,wt=7): 29777 f(x,y) = f(y,x). [para(19222(a,1),23654(a,1,2,2,1)),rewrite(25073(8),19304(5),14389(4))]. given #664 (T,wt=11): 29789 f(x,f(c_0,f(y,f(y,x)))) = c_0. [para(21388(a,1),23654(a,2)),rewrite(29777(2),29777(7),29777(10),29777(14),29777(17),29777(22),29777(25),29777(28),29777(31),29777(32),29777(34),29777(37),29788(37),29777(26),25060(26),14389(12))]. given #665 (T,wt=13): 29986 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [back_rewrite(28992),rewrite(29777(2),29777(5))]. given #666 (T,wt=13): 31432 f(f(c_0,c_0),f(f(x,x),f(y,z))) = c_0. [para(14553(a,1),29986(a,1,2,2)),rewrite(13353(5))]. given #667 (A,wt=19): 19230 f(x,f(c_0,f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y). [back_rewrite(14592),rewrite(19221(2),10878(3),19221(2),19222(4),19228(4),19101(5))]. given #668 (F,wt=23): 29823 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(23654(a,1),19886(a,1,1,1,1,2)),rewrite(29777(12),29777(13),29777(14),29777(16),29777(28),29777(29),29777(30),29777(31),29785(31),29777(18),29792(18),29777(15),29785(15),29777(3),29777(16),29777(17),29777(18),29777(19),29785(19),29777(6),29777(8))]. given #669 (F,wt=23): 30023 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(28714),rewrite(29777(2),29777(5),19228(5),29777(2),29777(3),29777(6),19228(6),29777(4),19228(4),29777(3),29777(6),29777(8))]. given #670 (F,wt=25): 29858 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(29693),rewrite(29777(4),29777(10),29777(12),29777(14),29777(15),29777(16),29831(16),29777(2),2285(3),29777(2),29777(4),29777(8),29777(9),29777(13))]. given #671 (F,wt=25): 30042 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(28669),rewrite(29777(4),29777(5),19304(5),29777(2),29777(3),29777(4),19304(4),29777(2),29777(4),29777(8),29777(9),19304(9),29777(8),29777(9),29777(13))]. given #672 (T,wt=11): 31449 f(x,f(c_0,f(y,x))) = f(y,x). [para(30023(a,1),2285(a,1,2)),rewrite(13353(3,R),29777(3),29777(4))]. given #673 (T,wt=11): 31450 f(f(x,x),f(c_0,f(y,x))) = c_0. [para(30023(a,1),14382(a,1,2,2)),rewrite(13353(3,R),29777(3),29777(5),13353(5),29777(5))]. given #674 (T,wt=11): 31452 f(x,f(x,f(y,x))) = f(y,x). [para(30023(a,1),19228(a,1,2,2)),rewrite(30023(11),29777(2))]. given #675 (T,wt=13): 31434 f(f(c_0,c_0),f(f(x,y),f(z,u))) = c_0. [para(16159(a,1),31432(a,1,2,1))]. given #676 (A,wt=17): 23189 f(x,f(f(x,y),f(c_0,f(z,f(x,x))))) = f(x,x). [back_rewrite(11051),rewrite(19228(5),12616(3))]. given #677 (F,wt=25): 30868 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(23456),rewrite(29777(2),29777(4),29777(6),29777(8),29777(11),29777(14),30866(14),29777(4),29777(8),29777(9))]. given #678 (F,wt=25): 31373 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(19830),rewrite(29777(4),29777(8),29777(9),29777(14),29777(18),29777(19),29777(21),29777(24),30028(24),29777(11))]. given #679 (F,wt=25): 31422 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(31050),rewrite(29777(6),29777(8),31279(21),29777(11))]. given #680 (F,wt=25): 31460 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(29858(a,1),29777(a,2)),rewrite(29777(7),29777(9),29777(12))]. given #681 (T,wt=13): 31436 f(x,f(c_0,f(f(x,x),f(y,y)))) = c_0. [para(2387(a,1),19230(a,1,2,2,1)),rewrite(12616(4),13353(4),12616(8))]. given #682 (T,wt=13): 31475 f(f(c_0,c_0),f(x,f(c_0,f(y,z)))) = c_0. [para(25070(a,1),31450(a,1,2,2)),rewrite(13353(13,R),29777(8),14553(8),29777(8))]. given #683 (T,wt=13): 31513 f(x,f(c_0,f(f(x,x),f(y,z)))) = c_0. [para(16159(a,1),31436(a,1,2,2,2))]. given #684 (T,wt=15): 29054 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0. [para(77(a,1),28928(a,1,1,1)),rewrite(13294(6,R))]. given #685 (A,wt=21): 23487 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(20459),rewrite(23245(6))]. given #686 (F,wt=19): 31525 f(f(x,y),f(c_0,f(x,f(f(x,y),f(z,f(x,z)))))) = c_0 # label(false). [para(30868(a,1),29054(a,1,1))]. given #687 (F,wt=19): 31526 f(f(x,y),f(c_0,f(y,f(f(x,y),f(z,f(y,z)))))) = c_0 # label(false). [para(31373(a,1),29054(a,1,1))]. given #688 (F,wt=19): 31552 f(x,f(c_0,f(f(x,y),f(x,f(z,f(z,f(x,y))))))) = c_0 # label(false). [para(20(a,1),31525(a,1,1)),rewrite(29777(2),29777(3),29777(5),2285(5),29777(3),29777(4))]. given #689 (F,wt=19): 31553 f(x,f(c_0,f(f(y,x),f(x,f(z,f(z,f(y,x))))))) = c_0 # label(false). [para(20(a,1),31525(a,1,2,2,2,1)),rewrite(20(3),29777(4))]. given #690 (T,wt=15): 29481 f(x,f(f(y,f(x,x)),f(z,f(x,x)))) = c_0. [para(13499(a,1),29021(a,1,2,2)),rewrite(13294(3,R),13333(3))]. given #691 (T,wt=15): 29987 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0. [back_rewrite(28989),rewrite(29777(3))]. given #692 (T,wt=15): 30030 f(x,f(y,f(x,f(y,x)))) = f(x,f(y,x)). [back_rewrite(28703),rewrite(29777(1),29777(3),29777(5),29777(8),19228(8),29777(1),29777(4),29777(5))]. given #693 (T,wt=15): 30033 f(f(x,f(y,x)),f(x,f(y,f(y,x)))) = x. [back_rewrite(28697),rewrite(29777(9),29777(10),19304(10),29777(3),29777(6))]. given #694 (A,wt=21): 23491 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(20431),rewrite(23245(6))]. given #695 (F,wt=25): 31467 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(30042(a,1),29777(a,2)),rewrite(29777(7),29777(9),29777(12))]. given #696 (F,wt=25): 31492 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(20(a,1),30868(a,1,2,1,2,2)),rewrite(29777(3),13353(3),20(7),29777(6),20(14))]. given #697 (F,wt=15): 31674 f(f(x,y),f(x,f(z,f(z,f(x,y))))) = x # label(false). [para(31492(a,1),30023(a,1,2,2,2,2,2)),rewrite(29777(3),29777(4),29777(10),29777(11),29777(12),29777(17),29777(18),13353(23,R),29777(18),14387(19),29777(17),29777(18),29777(23),29777(24),29777(25),29982(25),29777(19),31478(19),29777(11),30895(11),29777(1),29777(2)),flip(a)]. given #698 (F,wt=15): 31684 f(x,f(f(x,y),f(z,f(x,z)))) = f(x,y) # label(false). [para(20(a,1),31674(a,1,1)),rewrite(29777(1),29777(2),29777(4),2285(4),29777(2),29777(6))]. given #699 (T,wt=15): 30259 f(f(x,f(x,y)),f(x,f(y,f(x,y)))) = x. [back_rewrite(27765),rewrite(29777(1),29777(4),29777(6),13294(7,R),29777(6),14387(6),29777(4),29777(6))]. given #700 (T,wt=15): 30355 f(x,f(y,f(x,f(x,y)))) = f(x,f(x,y)). [back_rewrite(27248),rewrite(29777(1),29777(5),29777(6),19304(6),29777(3),29777(4),29777(5))]. given #701 (T,wt=13): 31774 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(31513(a,1),30355(a,1,2,2,2)),rewrite(13353(7),29777(7),14387(7),31513(10),13353(6))]. given #702 (T,wt=15): 31228 f(x,f(c_0,f(y,f(x,f(x,y))))) = f(x,y). [back_rewrite(21214),rewrite(29777(2),29777(4),29777(6),29777(7),29777(8),29777(11),30895(11),29777(4))]. given #703 (A,wt=17): 23905 f(f(c_0,f(x,f(y,y))),f(c_0,f(y,f(z,z)))) = c_0. [back_rewrite(19039),rewrite(23534(4))]. given #704 (F,wt=15): 31685 f(x,f(f(y,x),f(z,f(x,z)))) = f(y,x) # label(false). [para(20(a,1),31674(a,1,2,2,2,2)),rewrite(20(3),29777(2))]. given #705 (F,wt=15): 31688 f(f(x,y),f(y,f(z,f(z,f(x,y))))) = y # label(false). [para(29777(a,1),31674(a,1,1)),rewrite(29777(2))]. given #706 (F,wt=19): 31686 f(f(x,y),f(c_0,f(x,f(x,f(z,f(z,f(x,y))))))) = c_0 # label(false). [para(31674(a,1),19696(a,1,2,2,2)),rewrite(29777(7))]. given #707 (F,wt=19): 31689 f(f(x,f(y,f(y,f(x,z)))),f(c_0,f(x,f(x,z)))) = c_0 # label(false). [para(31674(a,1),29789(a,1,2,2,2)),rewrite(29777(7))]. given #708 (T,wt=15): 31419 f(x,f(c_0,f(y,f(x,f(y,x))))) = f(y,x). [back_rewrite(30865),rewrite(29777(2),29777(6),29777(7),29777(10),29777(11),30890(19),29777(6),29777(7))]. given #709 (T,wt=15): 31719 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(14429(a,1),31684(a,1,2,2,2)),rewrite(29777(7),14553(7))]. given #710 (T,wt=15): 31801 f(f(c_0,f(x,f(y,y))),f(c_0,f(y,z))) = c_0. [para(20(a,1),23905(a,1,2,2,2))]. given #711 (T,wt=15): 31802 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(20(a,1),23905(a,1,2,2)),rewrite(13353(4,R),29777(4),29777(8),13353(8),29777(8))]. given #712 (A,wt=21): 23970 f(f(x,y),f(c_0,f(y,f(z,f(y,f(x,y)))))) = f(y,f(x,y)). [back_rewrite(20387),rewrite(23890(9))]. given #713 (F,wt=19): 31720 f(x,f(c_0,f(f(x,y),f(f(x,y),f(z,f(x,z)))))) = c_0 # label(false). [para(31684(a,1),19696(a,1,2,2,2)),rewrite(29777(7))]. given #714 (F,wt=19): 31724 f(f(c_0,f(x,f(x,y))),f(f(x,y),f(z,f(x,z)))) = c_0 # label(false). [para(31684(a,1),29789(a,1,2,2,2)),rewrite(29777(9))]. given #715 (F,wt=19): 31823 f(f(c_0,f(x,f(y,x))),f(f(y,x),f(z,f(x,z)))) = c_0 # label(false). [para(31685(a,1),29789(a,1,2,2,2)),rewrite(29777(9))]. given #716 (F,wt=19): 31839 f(f(x,y),f(c_0,f(y,f(y,f(z,f(z,f(x,y))))))) = c_0 # label(false). [para(31688(a,1),19696(a,1,2,2,2)),rewrite(29777(7))]. given #717 (T,wt=15): 31818 f(f(x,y),f(y,f(z,f(c_0,f(x,y))))) = y. [back_rewrite(30749),rewrite(31802(16),29777(10),14553(10),10878(8))]. given #718 (T,wt=15): 31893 f(f(x,y),f(x,f(z,f(c_0,f(x,y))))) = x. [para(19228(a,1),31719(a,1,2,1)),rewrite(13353(4,R),29777(4),19228(11))]. given #719 (T,wt=15): 31910 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,y)))) = c_0. [para(20(a,1),31801(a,1,1,2,2)),rewrite(29777(6))]. given #720 (T,wt=15): 31911 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(19228(a,1),31801(a,1,2,2)),rewrite(13353(4,R),29777(4),29777(8),13353(8),29777(8))]. given #721 (A,wt=21): 23972 f(f(x,y),f(c_0,f(x,f(z,f(x,f(x,y)))))) = f(x,f(x,y)). [back_rewrite(20369),rewrite(23891(9))]. given #722 (F,wt=19): 31860 f(x,f(c_0,f(f(y,x),f(f(y,x),f(z,f(x,z)))))) = c_0 # label(false). [para(20(a,1),31686(a,1,2,2,2,2,2,2)),rewrite(20(3),29777(4))]. given #723 (F,wt=19): 31869 f(f(x,f(y,f(y,f(x,f(x,z))))),f(c_0,f(x,z))) = c_0 # label(false). [para(10878(a,1),31689(a,1,2,2))]. given #724 (F,wt=19): 31879 f(f(c_0,f(x,y)),f(f(x,f(x,y)),f(z,f(x,z)))) = c_0 # label(false). [para(30033(a,1),31689(a,1,1,2,2,2)),rewrite(29777(1),29777(3),29777(7),29777(9),29777(11),30259(14),29777(9),10878(9),29777(9))]. given #725 (F,wt=19): 31996 f(f(x,x),f(f(y,x),f(z,f(z,f(x,f(y,x)))))) = c_0 # label(false). [para(23970(a,1),31689(a,1,1,2,2,2)),rewrite(23970(16),19304(11),29777(8),13353(8),29777(8))]. given #726 (T,wt=15): 31915 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,x)))) = c_0. [para(31801(a,1),29777(a,1)),flip(a)]. given #727 (T,wt=15): 31944 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0. [para(20(a,1),31802(a,1,1))]. given #728 (T,wt=15): 31991 f(f(x,y),f(y,f(z,f(y,f(x,y))))) = y. [para(23970(a,1),30355(a,1,2,2,2)),rewrite(19304(11),29777(8),14387(8),23970(15),19304(10))]. given #729 (T,wt=15): 32142 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x). [para(20(a,1),31893(a,1,2,2,2,2)),rewrite(20(3),29777(3),13353(3))]. given #730 (A,wt=31): 24498 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(19304(a,1),21829(a,1,2,2,2,1)),rewrite(19222(11))]. given #731 (F,wt=19): 32028 f(f(x,f(y,f(y,f(z,x)))),f(c_0,f(x,f(z,x)))) = c_0 # label(false). [para(20(a,1),31724(a,1,1,2,2)),rewrite(29777(3),20(7),29777(6),29777(9))]. given #732 (F,wt=19): 32041 f(f(c_0,f(x,y)),f(f(y,f(x,y)),f(z,f(y,z)))) = c_0 # label(false). [para(31452(a,1),31724(a,1,1,2))]. given #733 (F,wt=19): 32060 f(f(x,x),f(f(x,f(y,x)),f(z,f(z,f(y,x))))) = c_0 # label(false). [para(23970(a,1),31724(a,1,1,2,2)),rewrite(19304(5),29777(2),13353(2),23970(9),29777(5))]. given #734 (F,wt=19): 32064 f(f(x,x),f(f(x,y),f(z,f(z,f(x,f(x,y)))))) = c_0 # label(false). [para(10878(a,1),31823(a,1,1,2,2)),rewrite(29777(5),19228(5),29777(2),13353(2),10878(4),29777(5))]. given #735 (T,wt=15): 32146 f(f(x,y),f(x,f(z,f(x,f(x,y))))) = x. [para(23970(a,1),31893(a,1,2,2)),rewrite(29777(1),29777(5),10878(7),29777(6))]. given #736 (T,wt=15): 32380 f(f(c_0,c_0),f(x,f(y,f(c_0,f(z,x))))) = c_0. [para(31802(a,1),32028(a,1,1,2,2)),rewrite(29777(7),13333(7),29777(5),23245(17),29777(9))]. given #737 (T,wt=15): 32385 f(f(c_0,c_0),f(x,f(y,f(c_0,f(x,z))))) = c_0. [para(31911(a,1),32028(a,1,1,2,2)),rewrite(29777(7),13333(7),29777(5),23245(17),29777(9))]. given #738 (T,wt=15): 32473 f(f(x,f(x,y)),f(x,f(z,f(x,y)))) = x. [para(10878(a,1),32146(a,1,2,2,2))]. given #739 (A,wt=17): 25061 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [para(16159(a,1),2286(a,1,1))]. given #740 (F,wt=19): 32065 f(f(x,x),f(f(x,f(x,y)),f(z,f(z,f(x,y))))) = c_0 # label(false). [para(19228(a,1),31823(a,1,1,2)),rewrite(29777(2),13353(2),29777(5))]. given #741 (F,wt=19): 32400 f(f(x,f(y,f(y,f(x,f(z,x))))),f(c_0,f(z,x))) = c_0 # label(false). [para(31452(a,1),32041(a,1,1,2)),rewrite(31452(8),29777(7),19304(7),29777(6),29777(9))]. given #742 (F,wt=23): 32238 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(20(a,1),31996(a,1,1))]. given #743 (F,wt=23): 32351 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(24498(a,1),31879(a,1,1,2)),rewrite(13333(3),32343(16),29777(4),29777(7),29777(9))]. given #744 (T,wt=17): 28468 f(f(x,f(x,y)),f(c_0,f(f(x,y),f(x,z)))) = x. [para(19221(a,1),19248(a,1,1)),rewrite(19221(5),10878(6))]. given #745 (T,wt=15): 32564 f(f(x,x),f(c_0,f(f(x,y),f(x,z)))) = x. [para(28468(a,1),31449(a,1,2,2)),rewrite(29777(7),13353(7),29777(7),28468(15))]. given #746 (T,wt=17): 29821 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,y))))) = y. [para(23654(a,1),19248(a,1,2,2,2)),rewrite(29777(6))]. given #747 (T,wt=17): 29911 f(f(x,f(x,y)),f(f(z,x),f(x,y))) = f(x,y). [back_rewrite(29427),rewrite(29777(2),29777(4),29777(7),29777(9),19228(9),29777(2),29777(4),29777(6),29777(7))]. given #748 (A,wt=31): 27660 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(27086(a,1),21790(a,1,2,2,2,1,2)),rewrite(10878(11),19222(11))]. given #749 (F,wt=25): 31504 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(31373(a,1),29777(a,2)),rewrite(29777(6),29777(8),29777(11))]. given #750 (F,wt=15): 32717 f(x,f(f(y,f(y,x)),f(z,x))) = f(z,x) # label(false). [para(31504(a,1),30023(a,1,2,2,2,2,2)),rewrite(13353(21,R),29777(17),14387(18),29777(24),32634(24),29777(17),13353(17),29777(17),2285(17),29777(11),31504(11)),flip(a)]. given #751 (F,wt=15): 32721 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z) # label(false). [para(32717(a,1),29777(a,2)),rewrite(29777(3),29777(5),29777(6))]. given #752 (F,wt=19): 32722 f(f(c_0,f(x,f(x,y))),f(f(z,f(z,x)),f(x,y))) = c_0 # label(false). [para(32717(a,1),29789(a,1,2,2,2)),rewrite(29777(3),29777(6),29777(9))]. given #753 (T,wt=15): 32634 f(f(x,f(y,x)),f(x,f(z,f(y,x)))) = x. [para(20(a,1),29911(a,1,1,2)),rewrite(29777(2),20(7),29777(5),20(9))]. given #754 (T,wt=17): 29921 f(f(x,f(y,x)),f(f(y,x),f(x,z))) = f(y,x). [back_rewrite(29378),rewrite(29777(2),29777(4),29777(6),13294(7,R),29777(7),14387(7),29777(6))]. given #755 (T,wt=17): 29977 f(f(x,f(x,y)),f(f(x,z),f(x,y))) = f(x,y). [back_rewrite(29101),rewrite(29777(2),29777(4),29777(7),29777(9),19228(9),29777(2),29777(4),29777(6),29777(7))]. given #756 (T,wt=17): 29982 f(f(x,f(x,y)),f(f(x,y),f(x,z))) = f(x,y). [back_rewrite(29068),rewrite(29777(2),29777(4),29777(6),13294(7,R),29777(7),14387(7),29777(6))]. given #757 (A,wt=29): 29787 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(23654(a,1),23669(a,1,2,2,1)),rewrite(29777(15),29777(16),29777(17),29785(18),29777(6),29777(21),29777(22),29777(23),29785(24),29777(11))]. given #758 (F,wt=27): 29790 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). [para(23654(a,1),24681(a,1,1,2,2,2,2,1,2,1)),rewrite(29777(3),29777(6),29777(8),29777(24),29777(25),29777(26),29785(27),29777(14))]. given #759 (F,wt=27): 30575 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(25373),rewrite(29777(5),29777(9),19228(9),29777(4),29777(9),29777(13),19228(13),29777(8),29777(9))]. given #760 (F,wt=27): 31445 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(29823(a,1),29789(a,1,2,2,2)),rewrite(29777(12),29777(14))]. given #761 (F,wt=27): 31728 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(31684(a,1),30023(a,1,2,2,2,2,2)),rewrite(13353(9,R),29777(8),19696(9),29777(11),14553(13))]. given #762 (T,wt=17): 30856 f(x,f(c_0,f(f(y,y),f(c_0,f(z,f(x,z)))))) = c_0. [back_rewrite(23548),rewrite(29777(7))]. given #763 (T,wt=15): 33023 f(x,f(c_0,f(y,f(c_0,f(z,f(x,z)))))) = c_0. [para(20(a,1),30856(a,1,2,2,1))]. given #764 (T,wt=15): 33080 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0. [para(33023(a,1),29777(a,1)),rewrite(29777(4),29777(9)),flip(a)]. given #765 (T,wt=15): 33138 f(f(c_0,f(x,f(x,y))),f(c_0,f(y,z))) = c_0. [para(19696(a,1),33080(a,1,2,2,2,2,2)),rewrite(29777(2),13353(8),13333(8),29777(6))]. given #766 (A,wt=23): 29812 f(x,f(f(y,f(x,y)),f(x,f(y,f(x,y))))) = f(x,f(y,f(x,y))). [para(25069(a,1),23654(a,1,2,1)),rewrite(29777(8),14387(10))]. given #767 (F,wt=27): 31827 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(31685(a,1),30023(a,1,2,2,2,2,2)),rewrite(13353(9,R),29777(8),19696(9),29777(11),14553(13))]. given #768 (F,wt=27): 32724 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(32717(a,1),29823(a,1,2,2,2,2,2)),rewrite(29777(3),13353(9,R),29777(8),29789(9),29777(9),14553(13))]. given #769 (F,wt=27): 32933 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(10878(a,1),31445(a,1,1,2))]. given #770 (F,wt=27): 32940 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(31452(a,1),31445(a,1,1,2))]. given #771 (T,wt=15): 33173 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(20(a,1),33138(a,1,2,2)),rewrite(29777(7),13353(7),29777(7))]. given #772 (T,wt=15): 33174 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(19228(a,1),33138(a,1,2,2)),rewrite(29777(7),13353(7),29777(7))]. given #773 (T,wt=15): 33178 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,z)))) = c_0. [para(33138(a,1),29777(a,1)),rewrite(29777(6)),flip(a)]. given #774 (T,wt=15): 33374 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0. [para(20(a,1),33173(a,1,1))]. given #775 (A,wt=45): 29820 f(f(c_0,f(x,f(y,y))),f(f(f(y,z),f(c_0,f(x,f(y,y)))),f(f(u,f(x,f(y,y))),f(f(x,f(y,y)),f(y,f(y,z)))))) = f(x,f(y,y)). [para(23654(a,1),14499(a,1,1,2,2)),rewrite(29777(5),29777(6),29777(7),29777(11),29777(14),29777(15),29777(21))]. given #776 (F,wt=27): 33084 f(x,f(f(y,f(x,y)),f(x,f(c_0,f(z,f(z,y)))))) = f(x,f(c_0,f(z,f(z,y)))) # label(false). [para(33023(a,1),29858(a,1,2,1)),rewrite(29777(4),29777(10),14553(12),29777(11))]. given #777 (F,wt=29): 29855 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(29701),rewrite(29777(6),29777(11),29777(18),29777(19),29777(24),29777(25),29777(27),29777(29),29777(31),29840(31),29777(16))]. given #778 (F,wt=29): 30044 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(28657),rewrite(29777(2),29777(6),19228(6),29777(6),29777(7),29777(10))]. given #779 (F,wt=29): 31461 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(29858(a,1),29789(a,1,2,2,2)),rewrite(29777(7),29777(9),29777(16))]. given #780 (T,wt=15): 33411 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,z)))) = c_0. [para(20(a,1),33174(a,1,2,2,2,2)),rewrite(13353(3,R),29777(3),29777(5))]. given #781 (T,wt=17): 30912 f(x,f(f(y,x),f(c_0,f(z,f(x,x))))) = f(x,x). [back_rewrite(23218),rewrite(29777(4),29777(7))]. given #782 (T,wt=17): 30935 f(x,f(f(x,y),f(y,f(z,f(x,y))))) = f(x,y).