============================== Prover9 =============================== Prover9 (32) version Aug-2007, Aug 2007. Process 17982 was started by mccune on cleo, Tue Aug 7 10:21:07 2007 The command was "/home/mccune/LADR/bin/prover9 -f MOL-base.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MOL-base.in assign(max_seconds,7200). assign(max_weight,60). assign(new_constants,1). set(lex_order_vars). set(restrict_denials). formulas(sos). f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x # label(MOL_SS). end_of_list. formulas(goals). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS). f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(MOD_SS). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS) # label(non_clause) # label(goal). [goal]. 2 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(MOD_SS) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. f(c4,f(c6,f(c4,f(c5,c5)))) != f(c4,f(c5,f(c4,f(c6,c6)))) # answer(MOD_SS). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 2). % (Horn set with more than one neg. clause) Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, 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): 4 f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. restricted denial: (wt=19): 5 f(c4,f(c6,f(c4,f(c5,c5)))) != f(c4,f(c5,f(c4,f(c6,c6)))) # answer(MOD_SS). [deny(2)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 4 f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. 5 f(c4,f(c6,f(c4,f(c5,c5)))) != f(c4,f(c5,f(c4,f(c6,c6)))) # answer(MOD_SS). [deny(2)]. end_of_list. formulas(sos). 3 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). 3 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): 3 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(MOL_SS). [assumption]. given #2 (A,wt=57): 6 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(y,w)))) = y. [para(3(a,1),3(a,1,2,1))]. given #3 (T,wt=9): 13 f(f(x,y),f(y,y)) = y. [para(6(a,1),6(a,1,2,2))]. given #4 (T,wt=11): 22 f(f(x,f(y,y)),y) = f(y,y). [para(13(a,1),13(a,1,2))]. given #5 (T,wt=13): 10 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(6(a,1),3(a,1,2,2))]. given #6 (T,wt=11): 34 f(f(f(x,x),y),x) = f(x,x). [para(10(a,1),13(a,1,1)),rewrite([10(7)]),flip(a)]. given #7 (A,wt=53): 7 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),f(f(z,x),v5)))) = f(z,x). [para(3(a,1),3(a,1,2,2,1,1,1,1))]. given #8 (T,wt=9): 42 f(f(x,y),f(x,x)) = x. [para(13(a,1),34(a,1,1,1)),rewrite([13(6)])]. given #9 (T,wt=13): 57 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(3(a,1),42(a,1,1))]. given #10 (T,wt=13): 63 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(42(a,1),42(a,1,1))]. given #11 (T,wt=15): 24 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(16),rewrite([22(7)])]. given #12 (A,wt=57): 8 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),y),f(y,w)))) = y. [para(3(a,1),3(a,1,2,2,1,1,1))]. given #13 (T,wt=15): 87 f(f(x,y),f(y,f(f(y,y),f(z,y)))) = y. [para(57(a,1),24(a,1,2,2,2))]. given #14 (T,wt=17): 83 f(x,f(f(x,x),f(x,f(f(x,x),y)))) = f(x,x). [para(13(a,1),24(a,1,1)),rewrite([42(4)])]. given #15 (T,wt=17): 104 f(x,f(f(x,x),f(x,f(y,f(x,x))))) = f(x,x). [para(13(a,1),87(a,1,1)),rewrite([42(4)])]. given #16 (T,wt=21): 19 f(f(x,f(y,y)),f(f(y,y),f(y,f(f(y,y),z)))) = f(y,y). [para(13(a,1),3(a,1,2,2,1)),rewrite([13(5)])]. given #17 (A,wt=35): 9 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(3(a,1),3(a,1,2,2,2))]. given #18 (T,wt=21): 39 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x. [para(34(a,1),3(a,1,2,2,1,1))]. given #19 (T,wt=21): 84 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x. [para(24(a,1),34(a,1)),flip(a)]. given #20 (T,wt=13): 167 f(x,f(f(x,x),f(x,y))) = f(x,x). [para(84(a,1),13(a,1,1)),rewrite([84(9)]),flip(a)]. given #21 (T,wt=13): 177 f(f(x,x),f(x,f(f(x,x),y))) = x. [para(13(a,1),167(a,1,2,1)),rewrite([42(8)])]. given #22 (A,wt=35): 11 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(x,z)))),x),f(x,u)))) = x. [para(3(a,1),6(a,1,2,2,1,1,1))]. given #23 (T,wt=13): 180 f(x,f(f(x,x),f(y,x))) = f(x,x). [para(57(a,1),167(a,1,2,2))]. given #24 (T,wt=13): 186 f(f(x,x),f(x,f(y,f(x,x)))) = x. [para(57(a,1),177(a,1,2,2))]. given #25 (T,wt=21): 159 f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x)) = x. [para(39(a,1),57(a,1,2,1)),rewrite([39(16),39(18)])]. given #26 (T,wt=21): 160 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x. [para(57(a,1),39(a,1,2,2,2))]. given #27 (A,wt=31): 14 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(13(a,1),3(a,1,1)),rewrite([13(3)])]. given #28 (T,wt=21): 176 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)). [para(3(a,1),167(a,1,2,2))]. given #29 (T,wt=21): 179 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)). [para(42(a,1),167(a,1,2,2))]. given #30 (T,wt=21): 216 f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(x,x)) = x. [para(57(a,1),159(a,1,1,2,2))]. given #31 (T,wt=23): 156 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [para(13(a,1),39(a,1,1)),rewrite([42(3),42(5)])]. given #32 (A,wt=33): 15 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(13(a,1),3(a,1,2,1,1))]. given #33 (T,wt=23): 184 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(177(a,1),3(a,1,2,2,1,1,1)),rewrite([177(6)])]. given #34 (T,wt=23): 208 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(x,z)))) = x. [para(186(a,1),3(a,1,2,2,1,1,1)),rewrite([186(6)])]. given #35 (T,wt=23): 213 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))),x) = f(x,x). [para(13(a,1),159(a,1,1,1,1)),rewrite([42(5),42(11)])]. given #36 (T,wt=23): 221 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [para(13(a,1),160(a,1,1)),rewrite([42(3),42(5)])]. given #37 (A,wt=37): 17 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(13(a,1),3(a,1,2,2,1,1,1,1))]. given #38 (T,wt=23): 252 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x). [para(13(a,1),216(a,1,1,1,1)),rewrite([42(5),42(11)])]. given #39 (T,wt=23): 273 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(57(a,1),184(a,1,2,2,2))]. given #40 (T,wt=17): 309 f(f(x,x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(57(a,1),273(a,1,2))]. given #41 (T,wt=17): 317 f(f(x,x),f(f(x,f(x,f(y,f(x,x)))),x)) = x. [para(57(a,1),309(a,1,2,1,2,2))]. given #42 (A,wt=25): 18 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(13(a,1),3(a,1,2,2,1,1,1))]. given #43 (T,wt=19): 346 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(216(a,1),18(a,1,2,2,1)),rewrite([13(4),42(3),57(6)])]. given #44 (T,wt=19): 347 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(252(a,1),18(a,1,2,2,1)),rewrite([22(3),57(8)])]. given #45 (T,wt=19): 352 f(f(f(f(x,x),x),f(x,f(f(x,x),y))),x) = f(x,x). [para(346(a,1),57(a,1,2,1)),rewrite([346(14),42(9),346(14)])]. given #46 (T,wt=19): 353 f(x,f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(57(a,1),346(a,1,2,2,2))]. given #47 (A,wt=29): 25 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(22(a,1),3(a,1,1))]. given #48 (T,wt=19): 365 f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)) = x. [para(347(a,1),57(a,1,2,1)),rewrite([347(14),347(16)])]. given #49 (T,wt=19): 366 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(57(a,1),347(a,1,2,2,2))]. given #50 (T,wt=19): 372 f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x) = f(x,x). [para(57(a,1),352(a,1,1,2,2))]. given #51 (T,wt=19): 393 f(f(f(x,f(x,x)),f(f(x,x),f(y,x))),f(x,x)) = x. [para(57(a,1),365(a,1,1,2,2))]. given #52 (A,wt=49): 26 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(22(a,1),3(a,1,2,2,1,1,1,1))]. given #53 (T,wt=21): 316 f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x))) = f(x,x). [para(13(a,1),309(a,1,1)),rewrite([42(5)])]. given #54 (T,wt=21): 325 f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x))) = f(x,x). [para(13(a,1),317(a,1,1)),rewrite([42(5)])]. given #55 (T,wt=21): 333 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(x,y)))) = x. [para(34(a,1),18(a,1,2,2,1)),rewrite([42(6)])]. given #56 (T,wt=19): 418 f(f(f(f(x,x),x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(333(a,1),57(a,1,2,1)),rewrite([333(15),333(17)])]. given #57 (A,wt=25): 27 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(22(a,1),3(a,1,2,2,1,1,1))]. given #58 (T,wt=19): 427 f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),x) = f(x,x). [para(13(a,1),418(a,1,1,1,1)),rewrite([42(5),42(9)])]. given #59 (T,wt=19): 430 f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(57(a,1),418(a,1,1,2,2))]. given #60 (T,wt=19): 447 f(f(f(x,f(x,x)),f(x,f(y,f(x,x)))),x) = f(x,x). [para(57(a,1),427(a,1,1,2,2))]. given #61 (T,wt=21): 419 f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(y,x)))) = x. [para(57(a,1),333(a,1,2,2,2))]. given #62 (A,wt=29): 37 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(34(a,1),3(a,1,1))]. given #63 (T,wt=21): 449 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y))))) = x. [para(427(a,1),179(a,1,1)),rewrite([427(8),427(9),42(4),427(16),427(17),42(12)])]. given #64 (T,wt=21): 459 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,f(y,f(x,x)))))) = x. [para(447(a,1),179(a,1,1)),rewrite([447(8),447(9),42(4),447(16),447(17),42(12)])]. given #65 (T,wt=23): 280 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(z,x)))) = x. [para(57(a,1),208(a,1,2,2,2))]. given #66 (T,wt=23): 336 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(f(x,x),y)))) = f(x,x). [para(42(a,1),18(a,1,2,2,1)),rewrite([42(5)])]. given #67 (A,wt=49): 38 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(34(a,1),3(a,1,2,2,1,1,1,1))]. given #68 (T,wt=23): 423 f(x,f(f(x,x),f(f(f(x,x),x),f(f(x,x),f(x,y))))) = f(x,x). [para(333(a,1),176(a,1,1)),rewrite([333(9),333(9),333(18),333(18)])]. given #69 (T,wt=23): 435 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))),f(x,x)) = x. [para(27(a,1),57(a,1,2,1)),rewrite([27(19),27(21)])]. given #70 (T,wt=23): 454 f(x,f(f(x,x),f(f(f(x,x),x),f(f(x,x),f(y,x))))) = f(x,x). [para(430(a,1),179(a,1,1)),rewrite([430(8),430(8),430(17),430(17)])]. given #71 (T,wt=23): 462 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(y,f(x,x))))) = f(x,x). [para(13(a,1),419(a,1,1,1)),rewrite([42(5),42(7)])]. given #72 (A,wt=49): 41 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),y),f(f(f(y,y),y),f(y,z)))),f(f(f(y,y),y),f(f(f(y,y),y),f(y,z)))),y),f(y,u)))) = y. [para(34(a,1),6(a,1,2,2,1,1,1,2,2,1,1)),rewrite([34(15)])]. given #73 (T,wt=23): 528 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x))),f(x,x)) = x. [para(57(a,1),435(a,1,1,2,2))]. given #74 (T,wt=25): 52 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(34(a,1),7(a,1,1)),rewrite([42(3),42(3)])]. given #75 (T,wt=25): 68 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(57(a,1),3(a,1,2,2,2))]. given #76 (T,wt=25): 69 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(3(a,1),57(a,1,2,1)),rewrite([3(20),3(22)])]. given #77 (A,wt=49): 43 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),x))) = f(z,x). [para(3(a,1),7(a,1,2,2,2))]. given #78 (T,wt=19): 673 f(f(f(f(x,x),x),f(f(x,x),x)),x) = f(f(x,x),x). [para(43(a,1),186(a,1,2,2)),rewrite([666(13),34(14),42(11)]),flip(a)]. given #79 (T,wt=21): 678 f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(13(a,1),673(a,1,1,1,1)),rewrite([42(5),42(10)])]. given #80 (T,wt=25): 338 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(18(a,1),57(a,1,2,1)),rewrite([18(20),18(22)])]. given #81 (T,wt=25): 340 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(57(a,1),18(a,1,2,2,2))]. given #82 (A,wt=53): 45 f(f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),w)))) = f(y,x). [para(13(a,1),7(a,1,1,1,2,1,1,1))]. given #83 (T,wt=25): 437 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(57(a,1),27(a,1,2,2,2))]. given #84 (T,wt=25): 523 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(13(a,1),435(a,1,1,1,1)),rewrite([42(12)])]. given #85 (T,wt=25): 543 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(13(a,1),528(a,1,1,1,1)),rewrite([42(12)])]. given #86 (T,wt=25): 544 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(13(a,1),528(a,1,1,2,1,1,1))]. given #87 (A,wt=31): 53 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(x,z)),y),y),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(42(a,1),3(a,1,1)),rewrite([42(3)])]. given #88 (T,wt=25): 554 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(52(a,1),57(a,1,2,1)),rewrite([52(20),42(12),52(20)])]. given #89 (T,wt=25): 555 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(57(a,1),52(a,1,2,2,2))]. given #90 (T,wt=25): 563 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(68(a,1),57(a,1,2,1)),rewrite([68(20),68(22)])]. given #91 (T,wt=25): 651 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(57(a,1),69(a,1,1,2,1,1,1,1))]. given #92 (A,wt=37): 54 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),f(f(x,y),u)))) = f(x,y). [para(42(a,1),3(a,1,2,2,1,1,1,1))]. given #93 (T,wt=25): 772 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(57(a,1),554(a,1,1,2,2))]. given #94 (T,wt=25): 806 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(57(a,1),563(a,1,1,2,1,1,1,1))]. given #95 (T,wt=27): 55 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(42(a,1),3(a,1,2,2,1,1))]. given #96 (T,wt=21): 891 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(22(a,1),55(a,1,2,2,1)),rewrite([57(9)])]. given #97 (A,wt=35): 56 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(42(a,1),3(a,1,2,2,2))]. given #98 (T,wt=21): 919 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(57(a,1),891(a,1,2,2,2))]. given #99 (T,wt=23): 890 f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(13(a,1),55(a,1,2,2,1)),rewrite([42(5),57(8)])]. given #100 (T,wt=23): 989 f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(13(a,1),919(a,1,1,1)),rewrite([42(6),42(7)])]. given #101 (T,wt=27): 315 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(309(a,1),3(a,1,2,2,1,1,1)),rewrite([309(8)])]. given #102 (A,wt=55): 59 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),w)))) = f(y,x). [para(42(a,1),7(a,1,1,1,2,1,1))]. given #103 (T,wt=27): 324 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(317(a,1),3(a,1,2,2,1,1,1)),rewrite([317(8)])]. given #104 (T,wt=27): 443 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(27(a,1),176(a,1,1)),rewrite([27(11),27(11),27(22),27(22)])]. given #105 (T,wt=27): 551 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(528(a,1),179(a,1,1)),rewrite([528(10),528(10),528(21),528(21)])]. given #106 (T,wt=27): 562 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(42(a,1),68(a,1,2,2,1,1))]. given #107 (A,wt=51): 61 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),f(x,x)),f(f(x,f(z,x)),f(f(z,x),w)))) = f(z,x). [para(42(a,1),7(a,1,2,2,1,1))]. given #108 (T,wt=27): 601 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,f(f(x,x),y))),x)),x),f(z,x)))) = x. [para(309(a,1),68(a,1,2,2,1,1,1)),rewrite([309(8)])]. given #109 (T,wt=21): 1082 f(f(x,x),f(f(x,f(f(x,f(x,f(f(x,x),y))),x)),x)) = x. [para(57(a,1),601(a,1,2))]. given #110 (T,wt=21): 1089 f(f(x,x),f(f(x,f(f(x,f(x,f(y,f(x,x)))),x)),x)) = x. [para(57(a,1),1082(a,1,2,1,2,1,2,2))]. given #111 (T,wt=27): 603 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,f(y,f(x,x)))),x)),x),f(z,x)))) = x. [para(317(a,1),68(a,1,2,2,1,1,1)),rewrite([317(8)])]. given #112 (A,wt=49): 62 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),z))) = f(z,x). [para(42(a,1),7(a,1,2,2,2))]. given #113 (T,wt=27): 648 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(42(a,1),69(a,1,1,2,1,1))]. given #114 (T,wt=27): 695 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(13(a,1),338(a,1,1,1,1)),rewrite([42(13)])]. given #115 (T,wt=27): 741 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(523(a,1),179(a,1,1)),rewrite([523(11),523(12),42(4),523(22),523(23),42(15)])]. given #116 (T,wt=27): 747 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(13(a,1),543(a,1,1,2,1,1,1))]. given #117 (A,wt=49): 64 f(f(x,y),f(f(f(x,y),z),f(f(f(f(f(f(f(x,y),f(x,y)),y),z),z),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),u)))) = f(f(x,y),f(x,y)). [para(57(a,1),3(a,1,1)),rewrite([42(8)])]. given #118 (T,wt=27): 754 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(543(a,1),179(a,1,1)),rewrite([543(11),543(12),42(4),543(22),543(23),42(15)])]. given #119 (T,wt=27): 804 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(42(a,1),563(a,1,1,2,1,1))]. given #120 (T,wt=27): 828 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(42(a,1),651(a,1,1,2,1,1))]. given #121 (T,wt=27): 871 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(42(a,1),806(a,1,1,2,1,1))]. given #122 (A,wt=45): 65 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(57(a,1),3(a,1,2,1))]. given #123 (T,wt=29): 247 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(3(a,1),176(a,1,1)),rewrite([3(11),3(11),3(23),3(23)])]. given #124 (T,wt=29): 261 f(f(f(x,y),f(f(f(f(f(f(x,x),z),y),y),f(x,x)),f(f(x,x),u))),x) = f(x,x). [para(15(a,1),57(a,1,2,1)),rewrite([15(26),42(14),15(26)])]. given #125 (T,wt=29): 345 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(18(a,1),176(a,1,1)),rewrite([18(11),18(11),18(23),18(23)])]. given #126 (T,wt=29): 359 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,x)),f(f(x,x),f(x,y)))),x),f(x,z)))) = x. [para(347(a,1),3(a,1,2,2,1,1,1)),rewrite([347(9)])]. given #127 (A,wt=31): 66 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u)))) = y. [para(57(a,1),3(a,1,2,2,1,1,1,1))]. given #128 (T,wt=29): 385 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(57(a,1),25(a,1,2,2,2))]. given #129 (T,wt=29): 395 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,x)),f(f(x,x),f(y,x)))),x),f(x,z)))) = x. [para(366(a,1),3(a,1,2,2,1,1,1)),rewrite([366(9)])]. given #130 (T,wt=29): 470 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(57(a,1),37(a,1,2,2,2))]. given #131 (T,wt=29): 588 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(68(a,1),176(a,1,1)),rewrite([68(11),68(11),68(23),68(23)])]. given #132 (A,wt=45): 67 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(57(a,1),3(a,1,2,2,1,1,1))]. given #133 (T,wt=29): 607 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,x)),f(f(x,x),f(x,y)))),x),f(z,x)))) = x. [para(347(a,1),68(a,1,2,2,1,1,1)),rewrite([347(9)])]. given #134 (T,wt=23): 1348 f(f(x,x),f(f(x,f(f(x,f(x,x)),f(f(x,x),f(x,y)))),x)) = x. [para(57(a,1),607(a,1,2))]. given #135 (T,wt=23): 1357 f(f(x,x),f(f(x,f(f(x,f(x,x)),f(f(x,x),f(y,x)))),x)) = x. [para(57(a,1),1348(a,1,2,1,2,2,2))]. given #136 (T,wt=27): 1355 f(x,f(f(f(x,x),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x))) = f(x,x). [para(13(a,1),1348(a,1,1)),rewrite([42(5),42(6)])]. given #137 (A,wt=57): 70 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),y),f(y,w)))) = y. [para(57(a,1),6(a,1,2,2,1,1,1,2,2,2)),rewrite([57(22)])]. given #138 (T,wt=27): 1371 f(x,f(f(f(x,x),f(f(f(x,x),x),f(x,f(y,f(x,x))))),f(x,x))) = f(x,x). [para(13(a,1),1357(a,1,1)),rewrite([42(5),42(6)])]. given #139 (T,wt=29): 612 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,x)),f(f(x,x),f(y,x)))),x),f(z,x)))) = x. [para(366(a,1),68(a,1,2,2,1,1,1)),rewrite([366(9)])]. given #140 (T,wt=29): 659 f(f(f(x,f(f(f(x,x),x),f(f(x,x),f(x,y)))),f(x,f(f(x,x),z))),x) = f(x,x). [para(333(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(16),42(14)])]. given #141 (T,wt=29): 661 f(f(f(x,f(f(f(x,x),x),f(f(x,x),f(y,x)))),f(x,f(f(x,x),z))),x) = f(x,x). [para(419(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(16),42(14)])]. given #142 (A,wt=57): 71 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(w,y)))) = y. [para(57(a,1),6(a,1,2,2,2))]. given #143 (T,wt=29): 675 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(673(a,1),3(a,1,1)),rewrite([57(10)])]. given #144 (T,wt=29): 684 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(673(a,1),68(a,1,1)),rewrite([57(10)])]. given #145 (T,wt=29): 712 f(x,f(f(x,x),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(z,x))))) = f(x,x). [para(340(a,1),176(a,1,1)),rewrite([340(11),340(11),340(23),340(23)])]. given #146 (T,wt=29): 801 f(f(f(x,y),f(f(f(f(f(f(x,x),z),y),y),f(x,x)),f(u,f(x,x)))),x) = f(x,x). [para(13(a,1),563(a,1,1,1,1)),rewrite([42(14)])]. given #147 (A,wt=53): 72 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),f(f(z,x),v5)))) = f(z,x). [para(57(a,1),7(a,1,1,1,2,2))]. given #148 (T,wt=29): 814 f(f(f(x,f(f(f(x,x),x),f(f(x,x),f(x,y)))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(333(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(16),42(14)])]. given #149 (T,wt=29): 816 f(f(f(x,f(f(f(x,x),x),f(f(x,x),f(y,x)))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(419(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(16),42(14)])]. given #150 (T,wt=29): 826 f(f(f(x,y),f(f(f(f(f(z,f(x,x)),y),y),f(x,x)),f(f(x,x),u))),x) = f(x,x). [para(13(a,1),651(a,1,1,1,1)),rewrite([42(14)])]. given #151 (T,wt=29): 836 f(x,f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(x,u))))) = f(x,x). [para(651(a,1),179(a,1,1)),rewrite([651(11),651(11),651(23),651(23)])]. given #152 (A,wt=53): 73 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),w),f(f(f(f(x,w),w),f(z,x)),f(v5,f(z,x))))) = f(z,x). [para(57(a,1),7(a,1,2,2,2))]. given #153 (T,wt=29): 870 f(f(f(x,y),f(f(f(f(f(z,f(x,x)),y),y),f(x,x)),f(u,f(x,x)))),x) = f(x,x). [para(13(a,1),806(a,1,1,1,1)),rewrite([42(14)])]. given #154 (T,wt=29): 878 f(x,f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(u,x))))) = f(x,x). [para(806(a,1),179(a,1,1)),rewrite([806(11),806(11),806(23),806(23)])]. given #155 (T,wt=29): 924 f(f(f(x,f(f(x,f(x,x)),f(f(x,x),f(x,y)))),f(x,f(f(x,x),z))),x) = f(x,x). [para(891(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(16),42(14)])]. given #156 (T,wt=29): 925 f(f(f(x,f(f(x,f(x,x)),f(f(x,x),f(x,y)))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(891(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(16),42(14)])]. given #157 (A,wt=37): 74 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(7(a,1),57(a,1,2,1)),rewrite([7(37),7(40)])]. given #158 (T,wt=29): 994 f(f(f(x,f(f(x,f(x,x)),f(f(x,x),f(y,x)))),f(x,f(f(x,x),z))),x) = f(x,x). [para(919(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(16),42(14)])]. given #159 (T,wt=29): 995 f(f(f(x,f(f(x,f(x,x)),f(f(x,x),f(y,x)))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(919(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(16),42(14)])]. given #160 (T,wt=29): 1088 f(x,f(f(f(x,x),f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x))),f(x,x))) = f(x,x). [para(13(a,1),1082(a,1,1)),rewrite([42(6)])]. given #161 (T,wt=29): 1100 f(x,f(f(f(x,x),f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x))),f(x,x))) = f(x,x). [para(13(a,1),1089(a,1,1)),rewrite([42(6)])]. given #162 (A,wt=49): 75 f(f(x,y),f(f(f(x,y),z),f(f(f(f(f(f(f(x,y),f(x,y)),x),z),z),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),u)))) = f(f(x,y),f(x,y)). [para(63(a,1),3(a,1,1)),rewrite([42(8)])]. given #163 (T,wt=29): 1140 f(f(x,x),f(x,f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,x)),f(f(x,x),z))))) = x. [para(695(a,1),179(a,1,1)),rewrite([695(12),695(13),42(4),695(24),695(25),42(16)])]. given #164 (T,wt=29): 1151 f(f(x,x),f(x,f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,x)),f(z,f(x,x)))))) = x. [para(747(a,1),179(a,1,1)),rewrite([747(12),747(13),42(4),747(24),747(25),42(16)])]. given #165 (T,wt=31): 77 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x. [para(63(a,1),3(a,1,2,2,1,1,1,1))]. given #166 (T,wt=31): 93 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))),x),f(x,z)))) = x. [para(34(a,1),8(a,1,2,1,2,2,1,1)),rewrite([39(10),34(6)])]. given #167 (A,wt=45): 76 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(63(a,1),3(a,1,2,1))]. given #168 (T,wt=31): 219 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))),x),f(x,z)))) = x. [para(160(a,1),3(a,1,2,2,1,1,1)),rewrite([160(10)])]. given #169 (T,wt=31): 227 f(x,f(f(y,x),f(f(f(f(y,x),f(f(y,x),f(y,x))),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(13(a,1),14(a,1,2,2,1,1,1)),rewrite([57(4)])]. given #170 (T,wt=31): 232 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(z,x)),y),y),f(x,x)),f(u,f(x,x))))) = f(x,x). [para(57(a,1),14(a,1,2,2,2))]. given #171 (T,wt=31): 239 f(x,f(f(x,x),f(f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(177(a,1),14(a,1,2,2,1,1,1)),rewrite([42(4),167(4),42(6)])]. given #172 (A,wt=45): 78 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(63(a,1),3(a,1,2,2,1,1,1))]. given #173 (T,wt=31): 243 f(x,f(f(x,x),f(f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(186(a,1),14(a,1,2,2,1,1,1)),rewrite([42(4),180(4),42(6)])]. given #174 (T,wt=31): 257 f(f(x,f(y,y)),f(f(y,f(x,x)),f(f(f(x,f(x,x)),f(y,y)),f(f(y,y),z)))) = f(y,y). [para(13(a,1),15(a,1,2,2,1,1,1))]. given #175 (T,wt=31): 258 f(f(f(x,x),f(y,y)),f(f(y,x),f(f(f(f(x,x),x),f(y,y)),f(f(y,y),z)))) = f(y,y). [para(22(a,1),15(a,1,2,2,1,1,1))]. given #176 (T,wt=31): 270 f(f(x,x),f(x,f(f(x,y),f(f(f(f(f(f(x,x),z),y),y),f(x,x)),f(f(x,x),u))))) = x. [para(15(a,1),176(a,1,1)),rewrite([15(15),15(16),42(4),15(28),15(29),42(17)])]. given #177 (A,wt=57): 90 f(f(x,y),f(f(f(y,y),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z)))),f(f(f(x,f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z)))),y),f(y,u)))) = y. [para(13(a,1),8(a,1,2,1,2,2,1,1,1)),rewrite([13(18)])]. given #178 (T,wt=31): 308 f(x,f(f(x,x),f(f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x)),f(z,f(x,x))))) = f(x,x). [para(13(a,1),273(a,1,1)),rewrite([42(6)])]. given #179 (T,wt=31): 335 f(x,f(f(x,y),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(42(a,1),18(a,1,1)),rewrite([42(3),63(4)])]. given #180 (T,wt=31): 486 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y))))),x),f(x,z)))) = x. [para(449(a,1),3(a,1,2,2,1,1,1)),rewrite([449(10)])]. given #181 (T,wt=31): 493 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,f(x,x)),f(x,f(y,f(x,x)))))),x),f(x,z)))) = x. [para(459(a,1),3(a,1,2,2,1,1,1)),rewrite([459(10)])]. given #182 (A,wt=59): 92 f(f(x,f(y,y)),f(f(y,f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z)))),f(f(f(x,f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z)))),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(22(a,1),8(a,1,2,1,2,2,1,1,1)),rewrite([42(5),22(16)])]. given #183 (T,wt=31): 501 f(x,f(f(x,x),f(f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x)),f(z,f(x,x))))) = f(x,x). [para(13(a,1),280(a,1,1)),rewrite([42(6)])]. given #184 (T,wt=31): 560 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(x,z)),y),y),f(x,x)),f(u,f(x,x))))) = f(x,x). [para(42(a,1),68(a,1,1)),rewrite([42(3)])]. given #185 (T,wt=31): 566 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(u,y)))) = y. [para(57(a,1),68(a,1,2,2,1,1,1,1))]. given #186 (T,wt=31): 570 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))) = x. [para(63(a,1),68(a,1,2,2,1,1,1,1))]. given #187 (A,wt=43): 94 f(f(f(x,x),x),f(f(f(x,x),f(f(x,y),f(f(f(f(f(f(x,x),x),y),y),f(x,x)),f(f(x,x),z)))),f(f(x,x),f(x,u)))) = x. [para(34(a,1),8(a,1,2,2,1)),rewrite([42(6)])]. given #188 (T,wt=31): 574 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))),x),f(z,x)))) = x. [para(39(a,1),68(a,1,2,2,1,1,1)),rewrite([39(10)])]. given #189 (T,wt=25): 1847 f(f(x,x),f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))),x)) = x. [para(57(a,1),574(a,1,2))]. given #190 (T,wt=25): 1857 f(f(x,x),f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))),x)) = x. [para(57(a,1),1847(a,1,2,1,2,2,2))]. given #191 (T,wt=31): 587 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))),x),f(z,x)))) = x. [para(160(a,1),68(a,1,2,2,1,1,1)),rewrite([160(10)])]. given #192 (A,wt=41): 95 f(f(x,f(x,x)),f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,f(x,x)),y),y),x),f(x,z)))),f(x,f(f(x,x),u)))) = f(x,x). [para(42(a,1),8(a,1,2,2,1)),rewrite([42(5)])]. given #193 (T,wt=31): 630 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y))))),x),f(z,x)))) = x. [para(449(a,1),68(a,1,2,2,1,1,1)),rewrite([449(10)])]. given #194 (T,wt=25): 1892 f(f(x,x),f(f(x,f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y))))),x)) = x. [para(57(a,1),630(a,1,2))]. given #195 (T,wt=25): 1900 f(f(x,x),f(f(x,f(x,f(f(x,f(x,x)),f(x,f(y,f(x,x)))))),x)) = x. [para(57(a,1),1892(a,1,2,1,2,2,2,2))]. given #196 (T,wt=31): 632 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,f(x,x)),f(x,f(y,f(x,x)))))),x),f(z,x)))) = x. [para(459(a,1),68(a,1,2,2,1,1,1)),rewrite([459(10)])]. given #197 (A,wt=57): 96 f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(x,x)) = x. [para(8(a,1),57(a,1,2,1)),rewrite([8(52),8(54)])]. given #198 (T,wt=31): 662 f(f(f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(336(a,1),69(a,1,1,2,1,1,1)),rewrite([34(17)])]. given #199 (T,wt=31): 663 f(f(f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(x,x))))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(462(a,1),69(a,1,1,2,1,1,1)),rewrite([34(17)])]. given #200 (T,wt=31): 701 f(x,f(f(y,x),f(f(f(f(y,x),f(f(y,x),f(y,x))),f(x,x)),f(z,f(x,x))))) = f(x,x). [para(13(a,1),340(a,1,1)),rewrite([42(3),57(4)])]. given #201 (T,wt=31): 702 f(f(x,f(y,y)),f(f(y,f(x,x)),f(f(f(x,f(x,x)),f(y,y)),f(z,f(y,y))))) = f(y,y). [para(13(a,1),340(a,1,2,1,1))]. given #202 (A,wt=57): 97 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))),y),f(y,w)))) = y. [para(57(a,1),8(a,1,2,1,2,2,2)),rewrite([57(22)])]. given #203 (T,wt=31): 705 f(x,f(f(x,y),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(x,x)),f(z,f(x,x))))) = f(x,x). [para(42(a,1),340(a,1,1)),rewrite([42(3),63(4)])]. given #204 (T,wt=31): 723 f(f(f(x,x),f(y,y)),f(f(y,x),f(f(f(f(x,x),x),f(y,y)),f(z,f(y,y))))) = f(y,y). [para(13(a,1),437(a,1,2,1,1))]. given #205 (T,wt=31): 738 f(f(f(x,y),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(y,y)),f(f(y,y),z))),y) = f(y,y). [para(57(a,1),523(a,1,1,1)),rewrite([42(8)])]. given #206 (T,wt=31): 739 f(f(f(x,y),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(x,x)),f(f(x,x),z))),x) = f(x,x). [para(63(a,1),523(a,1,1,1)),rewrite([42(8)])]. given #207 (A,wt=57): 98 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),y),f(w,y)))) = y. [para(57(a,1),8(a,1,2,2,2))]. given #208 (T,wt=31): 751 f(f(f(x,y),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(y,y)),f(z,f(y,y)))),y) = f(y,y). [para(57(a,1),543(a,1,1,1)),rewrite([42(8)])]. given #209 (T,wt=31): 752 f(f(f(x,y),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(x,x)),f(z,f(x,x)))),x) = f(x,x). [para(63(a,1),543(a,1,1,1)),rewrite([42(8)])]. given #210 (T,wt=31): 817 f(f(f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(336(a,1),563(a,1,1,2,1,1,1)),rewrite([34(17)])]. given #211 (T,wt=31): 818 f(f(f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(x,x))))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(462(a,1),563(a,1,1,2,1,1,1)),rewrite([34(17)])]. given #212 (A,wt=41): 128 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,w),u),u),y),f(y,v5)))))) = y. [para(3(a,1),9(a,1,1,2)),rewrite([3(12),3(12),3(14),3(17),3(30)])]. given #213 (T,wt=31): 901 f(x,f(f(x,x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))))) = f(x,x). [para(55(a,1),176(a,1,1)),rewrite([55(12),55(12),55(25),55(25)])]. given #214 (T,wt=31): 1003 f(f(f(f(x,x),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(890(a,1),69(a,1,1,2,1,1,1)),rewrite([34(17)])]. given #215 (T,wt=31): 1004 f(f(f(f(x,x),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(890(a,1),563(a,1,1,2,1,1,1)),rewrite([34(17)])]. given #216 (T,wt=31): 1013 f(f(f(f(x,x),f(f(f(x,x),x),f(x,f(y,f(x,x))))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(989(a,1),69(a,1,1,2,1,1,1)),rewrite([34(17)])]. given #217 (A,wt=33): 129 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). [para(13(a,1),9(a,1,2,2,1,1,1,1))]. given #218 (T,wt=31): 1014 f(f(f(f(x,x),f(f(f(x,x),x),f(x,f(y,f(x,x))))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(989(a,1),563(a,1,1,2,1,1,1)),rewrite([34(17)])]. given #219 (T,wt=31): 1054 f(x,f(f(x,x),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(z,x))))) = f(x,x). [para(562(a,1),176(a,1,1)),rewrite([562(12),562(12),562(25),562(25)])]. given #220 (T,wt=31): 1087 f(f(x,x),f(x,f(f(f(x,f(f(x,f(f(x,f(x,f(f(x,x),y))),x)),x)),x),f(x,z)))) = x. [para(1082(a,1),3(a,1,2,2,1,1,1)),rewrite([1082(10)])]. given #221 (T,wt=31): 1096 f(f(x,x),f(x,f(f(f(x,f(f(x,f(f(x,f(x,f(f(x,x),y))),x)),x)),x),f(z,x)))) = x. [para(1082(a,1),68(a,1,2,2,1,1,1)),rewrite([1082(10)])]. given #222 (A,wt=33): 130 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(13(a,1),9(a,1,2,2,1,1,1))]. given #223 (T,wt=15): 2218 f(f(x,f(x,x)),f(x,f(f(x,x),y))) = x. [para(18(a,1),130(a,1,2,2,1)),rewrite([42(3),42(6),42(10),42(13),42(16),42(19),42(27),177(27),22(23),42(9),42(3),42(6)]),flip(a)]. given #224 (T,wt=15): 2220 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x. [para(346(a,1),130(a,1,1)),rewrite([890(25),177(21),22(17),42(3)]),flip(a)]. given #225 (T,wt=15): 2224 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x. [para(353(a,1),130(a,1,1)),rewrite([989(25),186(21),22(17),42(3)]),flip(a)]. given #226 (T,wt=15): 2232 f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. [para(462(a,1),130(a,1,2,2,1)),rewrite([186(27),22(23),42(9)]),flip(a)]. given #227 (A,wt=45): 131 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(22(a,1),9(a,1,1))]. given #228 (T,wt=17): 2222 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x). [para(347(a,1),130(a,1,1)),rewrite([42(16),42(18),891(23),167(18),13(16)]),flip(a)]. given #229 (T,wt=17): 2226 f(f(x,f(x,x)),f(f(x,x),f(y,x))) = f(x,x). [para(366(a,1),130(a,1,1)),rewrite([42(16),42(18),919(23),180(18),13(16)]),flip(a)]. given #230 (T,wt=17): 2229 f(f(f(x,x),x),f(f(x,x),f(x,y))) = f(x,x). [para(27(a,1),130(a,1,2,2,1)),rewrite([42(4),42(4),42(8),34(6),42(7),42(11),42(11),42(15),34(13),42(14),42(17),42(17),42(21),34(19),42(20),42(24),42(25),42(27),34(25),42(26),167(26),13(24),34(9),42(4),42(4),42(8),34(6),42(7)]),flip(a)]. given #231 (T,wt=17): 2238 f(f(f(x,x),x),f(f(x,x),f(y,x))) = f(x,x). [para(437(a,1),130(a,1,2,2,1)),rewrite([42(4),42(4),42(8),34(6),42(7),42(11),42(11),42(15),34(13),42(14),42(17),42(17),42(21),34(19),42(20),42(24),42(25),42(27),34(25),42(26),180(26),13(24),34(9),42(4),42(4),42(8),34(6),42(7)]),flip(a)]. given #232 (A,wt=45): 132 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)). [para(22(a,1),9(a,1,2,2,1,1,1,1))]. given #233 (T,wt=23): 2302 f(f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z))),x) = f(x,x). [para(2218(a,1),651(a,1,1,2,1,1,1)),rewrite([42(3),42(10),42(11)])]. given #234 (T,wt=23): 2304 f(f(f(x,f(x,f(f(x,x),y))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(2218(a,1),806(a,1,1,2,1,1,1)),rewrite([42(3),42(10),42(11)])]. given #235 (T,wt=23): 2358 f(f(f(x,f(x,f(y,f(x,x)))),f(x,f(f(x,x),z))),x) = f(x,x). [para(2224(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(10),42(11)])]. given #236 (T,wt=23): 2362 f(f(f(x,f(x,f(y,f(x,x)))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(2224(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(10),42(11)])]. given #237 (A,wt=33): 133 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(22(a,1),9(a,1,2,2,1,1,1))]. given #238 (T,wt=25): 2197 f(f(x,x),f(f(x,f(f(x,f(f(x,f(x,f(f(x,x),y))),x)),x)),x)) = x. [para(57(a,1),1096(a,1,2))]. given #239 (T,wt=25): 2268 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [back_rewrite(1437),rewrite([2220(8)])]. given #240 (T,wt=19): 2632 f(f(f(x,x),x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(57(a,1),2268(a,1,2))]. given #241 (T,wt=15): 2679 f(f(x,f(x,f(f(x,x),y))),x) = f(x,x). [para(2632(a,1),129(a,1,2,2,1)),rewrite([309(7),13(14)]),flip(a)]. given #242 (A,wt=45): 134 f(f(f(x,y),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(f(f(x,y),f(f(f(x,y),f(x,y)),u)),z),z),f(x,y)),y))) = f(x,y). [para(34(a,1),9(a,1,1))]. given #243 (T,wt=15): 2685 f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). [para(57(a,1),2679(a,1,1,2,2))]. given #244 (T,wt=17): 2680 f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(2632(a,1),132(a,1,2,2,1)),rewrite([42(5),316(8),42(6),42(13),42(21),22(19),42(3),42(5)]),flip(a)]. given #245 (T,wt=17): 2688 f(f(x,x),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(2679(a,1),179(a,1,1)),rewrite([2679(6),2679(7),42(4),2679(12),2679(13),42(10)])]. given #246 (T,wt=17): 2740 f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(13(a,1),2685(a,1,1,2,2,2)),rewrite([42(10)])]. given #247 (A,wt=43): 135 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)),y))) = f(f(x,x),y). [para(34(a,1),9(a,1,2,2,1,1,1,1))]. given #248 (T,wt=15): 2828 f(f(x,f(f(x,x),x)),x) = f(f(x,x),x). [para(673(a,1),135(a,1,2,1)),rewrite([34(8),34(10),13(7)])]. given #249 (T,wt=17): 2744 f(f(x,x),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(2685(a,1),179(a,1,1)),rewrite([2685(6),2685(7),42(4),2685(12),2685(13),42(10)])]. given #250 (T,wt=19): 2835 f(f(f(x,x),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(13(a,1),2828(a,1,1,2,1)),rewrite([42(9)])]. given #251 (T,wt=21): 2770 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))) = f(x,x). [para(2680(a,1),179(a,1,1)),rewrite([2680(7),2680(7),2680(15),2680(15)])]. given #252 (A,wt=37): 136 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(34(a,1),9(a,1,2,2,1,1))]. given #253 (T,wt=21): 2809 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))) = f(x,x). [para(2740(a,1),179(a,1,1)),rewrite([2740(7),2740(7),2740(15),2740(15)])]. given #254 (T,wt=23): 2702 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(2679(a,1),648(a,1,1,2,1)),rewrite([2684(11)])]. given #255 (T,wt=23): 2703 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(2679(a,1),804(a,1,1,2,1)),rewrite([2684(11)])]. given #256 (T,wt=23): 2758 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(2685(a,1),648(a,1,1,2,1)),rewrite([2741(11)])]. given #257 (A,wt=59): 137 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),w),f(f(f(f(z,w),w),f(y,z)),f(f(y,z),v5)))))) = f(y,z). [para(7(a,1),9(a,1,1,2)),rewrite([7(26),7(27),7(30),7(34),7(51)])]. given #258 (T,wt=23): 2759 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(2685(a,1),804(a,1,1,2,1)),rewrite([2741(11)])]. given #259 (T,wt=25): 2313 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(2218(a,1),836(a,1,2,2,2,1,1,1)),rewrite([42(4),42(4),42(11),42(14)])]. given #260 (T,wt=25): 2314 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(2218(a,1),878(a,1,2,2,2,1,1,1)),rewrite([42(4),42(4),42(11),42(14)])]. given #261 (T,wt=25): 2369 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(2224(a,1),247(a,1,2,2,2,1,1,1)),rewrite([42(4),42(4),42(11),42(14)])]. given #262 (A,wt=33): 138 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),y))) = f(x,y). [para(42(a,1),9(a,1,2,2,1,1,1,1))]. given #263 (T,wt=25): 2370 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(2224(a,1),588(a,1,2,2,2,1,1,1)),rewrite([42(4),42(4),42(11),42(14)])]. given #264 (T,wt=25): 2446 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(2222(a,1),69(a,1,1,2,1,1,1)),rewrite([34(11)])]. given #265 (T,wt=25): 2452 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(2222(a,1),563(a,1,1,2,1,1,1)),rewrite([34(11)])]. given #266 (T,wt=25): 2478 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(2226(a,1),69(a,1,1,2,1,1,1)),rewrite([34(11)])]. given #267 (A,wt=41): 139 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(42(a,1),9(a,1,2,2,1,1))]. given #268 (T,wt=21): 3135 f(f(f(f(x,x),f(x,y)),f(f(x,x),x)),x) = f(f(x,x),x). [para(2229(a,1),139(a,1,2,1,2,1)),rewrite([2229(18),42(14),673(12),2229(14),34(13),13(10)])]. given #269 (T,wt=21): 3136 f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),x) = f(f(x,x),x). [para(2238(a,1),139(a,1,2,1,2,1)),rewrite([2238(18),42(14),673(12),2238(14),34(13),13(10)])]. given #270 (T,wt=23): 3133 f(f(f(x,f(f(x,x),y)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(2218(a,1),139(a,1,2,1,2,1)),rewrite([2218(17),678(13),2218(14),42(13),22(9)])]. given #271 (T,wt=23): 3134 f(f(f(x,f(y,f(x,x))),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(2232(a,1),139(a,1,2,1,2,1)),rewrite([2232(17),678(13),2232(14),42(13),22(9)])]. given #272 (A,wt=37): 140 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(9(a,1),57(a,1,2,1)),rewrite([9(28),9(31)])]. given #273 (T,wt=25): 2484 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(2226(a,1),563(a,1,1,2,1,1,1)),rewrite([34(11)])]. given #274 (T,wt=25): 2776 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(2680(a,1),648(a,1,1,2,1)),rewrite([42(3),2768(12),42(12)])]. given #275 (T,wt=25): 2777 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(2680(a,1),804(a,1,1,2,1)),rewrite([42(3),2768(12),42(12)])]. given #276 (T,wt=25): 2815 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(2740(a,1),648(a,1,1,2,1)),rewrite([42(3),2808(12),42(12)])]. given #277 (A,wt=45): 141 f(f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(x,f(y,z)),u),u),f(y,z)),z))) = f(y,z). [para(57(a,1),9(a,1,2,2,1,1,1,1))]. given #278 (T,wt=25): 2816 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(2740(a,1),804(a,1,1,2,1)),rewrite([42(3),2808(12),42(12)])]. given #279 (T,wt=25): 2843 f(f(f(x,x),x),f(f(x,f(x,f(f(x,x),x))),f(f(x,x),f(x,y)))) = x. [para(2828(a,1),55(a,1,1)),rewrite([2684(13),2679(11)])]. given #280 (T,wt=21): 3315 f(f(x,f(x,f(f(x,x),x))),f(f(x,x),f(x,y))) = f(x,x). [para(2843(a,1),133(a,1,2,2,1)),rewrite([167(32),13(30),34(11)]),flip(a)]. given #281 (T,wt=21): 3320 f(f(x,f(x,f(f(x,x),x))),f(f(x,x),f(y,x))) = f(x,x). [para(57(a,1),3315(a,1,2,2))]. given #282 (A,wt=45): 142 f(f(f(f(f(x,y),z),f(f(x,y),z)),f(x,y)),f(f(f(f(x,y),f(x,y)),u),f(f(f(f(f(f(x,y),z),u),u),f(x,y)),y))) = f(x,y). [para(63(a,1),9(a,1,2,2,1,1,1,1))]. given #283 (T,wt=23): 3317 f(f(f(x,x),f(f(x,x),f(x,f(x,x)))),f(x,f(f(x,x),y))) = x. [para(13(a,1),3315(a,1,1,2,2,1)),rewrite([42(9),42(13)])]. given #284 (T,wt=23): 3323 f(f(f(x,x),f(f(x,x),f(x,f(x,x)))),f(x,f(y,f(x,x)))) = x. [para(13(a,1),3320(a,1,1,2,2,1)),rewrite([42(9),42(13)])]. given #285 (T,wt=25): 3151 f(f(x,x),f(f(f(x,x),f(f(x,x),x)),f(f(f(x,x),x),f(x,y)))) = x. [para(3136(a,1),3(a,1,2,2,1))]. given #286 (T,wt=25): 3156 f(x,f(f(x,f(x,f(x,x))),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [para(3136(a,1),14(a,1,2,2,1)),rewrite([42(3),42(6)])]. given #287 (A,wt=59): 154 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),w),f(f(f(f(f(f(y,z),v5),w),w),f(y,z)),z))))) = f(y,z). [para(9(a,1),9(a,1,1,2)),rewrite([9(17),9(18),9(21),9(25),9(42)])]. given #288 (T,wt=25): 3159 f(f(x,x),f(f(f(x,x),f(f(x,x),x)),f(f(f(x,x),x),f(y,x)))) = x. [para(3136(a,1),68(a,1,2,2,1))]. given #289 (T,wt=11): 3398 f(f(x,x),f(f(x,x),x)) = x. [para(13(a,1),3159(a,1,2))]. given #290 (T,wt=11): 3413 f(x,f(x,f(x,x))) = f(x,x). [para(678(a,1),3159(a,1,2,2,2)),rewrite([42(3),42(3),42(3),42(6),13(9)])]. given #291 (T,wt=17): 3399 f(f(x,x),f(x,f(f(f(x,x),x),f(y,x)))) = x. [para(3159(a,1),57(a,1,2,1)),rewrite([3398(4),3398(10),167(13),42(7),3398(5)]),flip(a)]. given #292 (A,wt=49): 155 f(x,f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))))) = f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))). [para(39(a,1),13(a,1,1))]. given #293 (T,wt=17): 3444 f(f(x,x),f(x,f(f(f(x,x),x),f(x,y)))) = x. [back_rewrite(3151),rewrite([3398(5)])]. given #294 (T,wt=21): 3458 f(x,f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [back_rewrite(3170),rewrite([3413(3)])]. given #295 (T,wt=21): 3459 f(x,f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [back_rewrite(3156),rewrite([3413(3)])]. given #296 (T,wt=27): 2312 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(2218(a,1),66(a,1,2,2,1,1,1)),rewrite([678(7),42(5),42(12)])]. given #297 (A,wt=37): 158 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)),x))) = f(x,y). [para(42(a,1),39(a,1,2,2,2))]. given #298 (T,wt=19): 3639 f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z))) = x. [para(2312(a,1),130(a,1,2,2,1)),rewrite([177(33),22(29),42(11)]),flip(a)]. given #299 (T,wt=19): 3665 f(f(x,f(x,f(y,f(x,x)))),f(x,f(f(x,x),z))) = x. [para(57(a,1),3639(a,1,1,2,2))]. given #300 (T,wt=19): 3666 f(f(x,f(x,f(f(x,x),y))),f(x,f(z,f(x,x)))) = x. [para(57(a,1),3639(a,1,2,2))]. given #301 (T,wt=19): 3730 f(f(x,f(x,f(y,f(x,x)))),f(x,f(z,f(x,x)))) = x. [para(57(a,1),3665(a,1,2,2))]. given #302 (A,wt=41): 161 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))),x),f(x,z)))),x),f(x,u)))) = x. [para(39(a,1),8(a,1,2,1,2,2,1,1,1)),rewrite([39(11),93(15),39(10),39(10)])]. given #303 (T,wt=23): 3663 f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,x),f(x,z))) = f(x,x). [para(13(a,1),3639(a,1,1,2,2,1)),rewrite([42(9)])]. given #304 (T,wt=23): 3729 f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,x),f(x,z))) = f(x,x). [para(13(a,1),3665(a,1,1,2,2,2)),rewrite([42(9)])]. given #305 (T,wt=23): 3734 f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,x),f(z,x))) = f(x,x). [para(13(a,1),3666(a,1,1,2,2,1)),rewrite([42(9)])]. given #306 (T,wt=23): 3739 f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,x),f(z,x))) = f(x,x). [para(13(a,1),3730(a,1,1,2,2,2)),rewrite([42(9)])]. given #307 (A,wt=37): 162 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(39(a,1),9(a,1,1,2)),rewrite([39(10),39(10),39(12),39(15),39(26)])]. given #308 (T,wt=27): 2708 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(2679(a,1),901(a,1,2,2,2,1)),rewrite([2684(12)])]. given #309 (T,wt=27): 2709 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(2679(a,1),1054(a,1,2,2,2,1)),rewrite([2684(12)])]. given #310 (T,wt=27): 2764 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(2685(a,1),901(a,1,2,2,2,1)),rewrite([2741(12)])]. given #311 (T,wt=27): 2765 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(2685(a,1),1054(a,1,2,2,2,1)),rewrite([2741(12)])]. given #312 (A,wt=55): 163 f(f(f(x,y),f(x,y)),f(f(x,y),f(f(f(f(x,y),f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(x,y),z)))),f(x,y)),y))) = f(x,y). [para(39(a,1),9(a,1,2,2,1,1,1)),rewrite([39(21)])]. given #313 (T,wt=27): 2782 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(2680(a,1),901(a,1,2,2,2,1)),rewrite([42(4),42(4),2768(13),42(15)])]. given #314 (T,wt=27): 2783 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(2680(a,1),1054(a,1,2,2,2,1)),rewrite([42(4),42(4),2768(13),42(15)])]. given #315 (T,wt=27): 2785 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(2688(a,1),3(a,1,2,2,1,1,1)),rewrite([2688(8)])]. given #316 (T,wt=27): 2792 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(2688(a,1),68(a,1,2,2,1,1,1)),rewrite([2688(8)])]. given #317 (A,wt=43): 171 f(x,f(f(x,x),f(f(f(f(x,x),f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,x),z)))),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(84(a,1),8(a,1,1)),rewrite([167(4),167(5),42(3),167(4),167(5),42(3),167(5),167(6),42(4),167(7),167(9),52(10),167(5),167(6),167(7),42(5),167(7),167(8),42(6),167(9),167(11),167(16),167(18),167(23)])]. given #318 (T,wt=21): 3987 f(f(x,x),f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),x)) = x. [para(57(a,1),2792(a,1,2))]. given #319 (T,wt=21): 4007 f(f(x,x),f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),x)) = x. [para(57(a,1),3987(a,1,2,1,2,2,2,2))]. given #320 (T,wt=27): 2821 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(2740(a,1),901(a,1,2,2,2,1)),rewrite([42(4),42(4),2808(13),42(15)])]. given #321 (T,wt=27): 2822 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(2740(a,1),1054(a,1,2,2,2,1)),rewrite([42(4),42(4),2808(13),42(15)])]. given #322 (A,wt=55): 173 f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),z),f(f(f(f(f(x,x),z),z),f(f(x,x),f(x,y))),f(f(f(x,x),f(x,y)),u)))) = f(f(x,x),f(x,y)). [para(167(a,1),3(a,1,1)),rewrite([34(13)])]. given #323 (T,wt=27): 2862 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(2744(a,1),3(a,1,2,2,1,1,1)),rewrite([2744(8)])]. given #324 (T,wt=27): 2869 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(2744(a,1),68(a,1,2,2,1,1,1)),rewrite([2744(8)])]. given #325 (T,wt=27): 3410 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x),f(x,z)))) = x. [para(3159(a,1),52(a,1,2,1)),rewrite([3398(6),3399(8),3398(5),42(10),42(11),42(15)])]. given #326 (T,wt=27): 3412 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x),f(z,x)))) = x. [para(3159(a,1),68(a,1,2,2,1,1,1)),rewrite([3398(6),3399(8),3398(5)])]. given #327 (A,wt=33): 174 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,f(f(y,y),z))),f(y,f(f(y,y),z))),y),f(y,u)))) = y. [para(167(a,1),3(a,1,2,1)),rewrite([42(4),42(5),42(9)])]. given #328 (T,wt=21): 4088 f(f(x,x),f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x)) = x. [para(57(a,1),3412(a,1,2))]. given #329 (T,wt=27): 3438 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(x,x),x),f(x,y)))),x),f(z,x)))) = x. [back_rewrite(3172),rewrite([3398(5)])]. given #330 (T,wt=21): 4159 f(f(x,x),f(f(x,f(x,f(f(f(x,x),x),f(x,y)))),x)) = x. [para(57(a,1),3438(a,1,2))]. given #331 (T,wt=27): 3442 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(x,x),x),f(x,y)))),x),f(x,z)))) = x. [back_rewrite(3154),rewrite([3398(5)])]. given #332 (A,wt=51): 175 f(f(x,y),f(f(f(y,y),f(f(f(y,x),f(y,x)),f(f(y,x),z))),f(f(f(f(f(y,x),f(y,x)),f(f(f(y,x),f(y,x)),f(f(y,x),z))),y),f(y,u)))) = y. [para(167(a,1),3(a,1,2,2,1,1,1))]. given #333 (T,wt=27): 3650 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,f(f(x,x),y)))))) = f(x,x). [para(2679(a,1),158(a,1,1,1)),rewrite([2679(6),42(3),2679(5),2679(6),42(3),2679(5),2679(7),2679(8),42(5),2679(7),2679(16)])]. given #334 (T,wt=27): 3651 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,f(y,f(x,x))))))) = f(x,x). [para(2685(a,1),158(a,1,1,1)),rewrite([2685(6),42(3),2685(5),2685(6),42(3),2685(5),2685(7),2685(8),42(5),2685(7),2685(16)])]. given #335 (T,wt=27): 3676 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(3639(a,1),52(a,1,2,2,1,1))]. given #336 (T,wt=27): 3683 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(3639(a,1),554(a,1,1,2,1,1))]. given #337 (A,wt=49): 181 f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),z),f(f(f(f(f(x,x),z),z),f(f(x,x),f(x,y))),f(x,y)))) = f(f(x,x),f(x,y)). [para(167(a,1),9(a,1,1)),rewrite([34(13)])]. given #338 (T,wt=27): 3684 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(3639(a,1),555(a,1,2,2,1,1))]. given #339 (T,wt=27): 3689 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(3639(a,1),772(a,1,1,2,1,1))]. given #340 (T,wt=27): 3750 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(3730(a,1),52(a,1,2,2,1,1))]. given #341 (T,wt=27): 3757 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(3730(a,1),554(a,1,1,2,1,1))]. given #342 (A,wt=53): 182 f(f(x,f(y,z)),f(f(y,z),f(f(f(f(f(f(y,z),x),f(f(y,z),f(f(f(y,z),f(y,z)),u))),f(f(y,z),f(f(f(y,z),f(y,z)),u))),f(y,z)),z))) = f(y,z). [para(167(a,1),9(a,1,2,1)),rewrite([42(9),42(12),42(19)])]. given #343 (T,wt=27): 3758 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(3730(a,1),555(a,1,2,2,1,1))]. given #344 (T,wt=27): 3763 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(3730(a,1),772(a,1,1,2,1,1))]. given #345 (T,wt=27): 3806 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(3663(a,1),3(a,1,2,2,1,1))]. given #346 (T,wt=27): 3815 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(3663(a,1),68(a,1,2,2,1,1))]. given #347 (A,wt=51): 183 f(x,f(f(f(f(x,f(f(x,x),y)),f(x,f(f(x,x),y))),z),f(f(f(f(x,z),z),f(x,f(f(x,x),y))),f(f(x,f(f(x,x),y)),u)))) = f(x,f(f(x,x),y)). [para(177(a,1),3(a,1,1)),rewrite([42(13)])]. given #348 (T,wt=27): 3816 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(3663(a,1),69(a,1,1,2,1,1))]. given #349 (T,wt=27): 3817 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(3663(a,1),563(a,1,1,2,1,1))]. given #350 (T,wt=27): 3831 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(3739(a,1),3(a,1,2,2,1,1))]. given #351 (T,wt=27): 3834 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(3739(a,1),68(a,1,2,2,1,1))]. given #352 (A,wt=47): 188 f(x,f(f(f(f(x,f(f(x,x),y)),f(x,f(f(x,x),y))),z),f(f(f(f(x,z),z),f(x,f(f(x,x),y))),f(f(x,x),y)))) = f(x,f(f(x,x),y)). [para(177(a,1),9(a,1,1)),rewrite([42(13)])]. given #353 (T,wt=27): 3835 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(3739(a,1),69(a,1,1,2,1,1))]. given #354 (T,wt=27): 3836 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(3739(a,1),563(a,1,1,2,1,1))]. given #355 (T,wt=27): 4210 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,f(f(x,x),y))))),x) = f(x,x). [para(3650(a,1),57(a,1,2,1)),rewrite([3650(22),42(13),3650(22)])]. given #356 (T,wt=27): 4231 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,f(y,f(x,x)))))),x) = f(x,x). [para(3651(a,1),57(a,1,2,1)),rewrite([3651(22),42(13),3651(22)])]. given #357 (A,wt=45): 190 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(x,z)))),x),f(x,u)))),x),f(x,w)))) = x. [para(11(a,1),3(a,1,2,2,1,1,1)),rewrite([11(17)])]. given #358 (T,wt=29): 2436 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)). [para(3(a,1),2222(a,1,2,2))]. given #359 (T,wt=29): 2438 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)). [para(42(a,1),2222(a,1,2,2))]. given #360 (T,wt=19): 4525 f(f(f(x,x),x),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(2679(a,1),2438(a,1,1,1)),rewrite([2679(6),2679(7),42(4),2679(7),2679(8),42(5),2679(13),2679(14),42(11)])]. given #361 (T,wt=19): 4526 f(f(f(x,x),x),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(2685(a,1),2438(a,1,1,1)),rewrite([2685(6),2685(7),42(4),2685(7),2685(8),42(5),2685(13),2685(14),42(11)])]. given #362 (A,wt=57): 191 f(f(f(x,y),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(f(f(x,y),f(x,y)),z),z),f(x,y)),y))),f(x,y)),f(f(x,y),u)))) = f(x,y). [para(3(a,1),11(a,1,2,2,1,1,2,2,2))]. given #363 (T,wt=25): 4527 f(f(x,f(x,x)),f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))) = f(x,x). [para(2680(a,1),2438(a,1,1,1)),rewrite([2680(7),2680(7),2680(9),2680(9),2680(17),2680(17)])]. given #364 (T,wt=25): 4528 f(f(x,f(x,x)),f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))) = f(x,x). [para(2740(a,1),2438(a,1,1,1)),rewrite([2740(7),2740(7),2740(9),2740(9),2740(17),2740(17)])]. given #365 (T,wt=27): 4551 f(f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(f(x,x),z))),x) = f(x,x). [para(4525(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(14),42(13)])]. given #366 (T,wt=27): 4555 f(f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(4525(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(14),42(13)])]. given #367 (A,wt=57): 192 f(f(f(x,y),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(f(f(x,y),f(x,y)),z),z),f(x,y)),f(f(x,y),u)))),f(x,y)),y))) = f(x,y). [para(3(a,1),11(a,1,2,2,2))]. given #368 (T,wt=27): 4578 f(f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(x,f(f(x,x),z))),x) = f(x,x). [para(4526(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(14),42(13)])]. given #369 (T,wt=27): 4582 f(f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(4526(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(14),42(13)])]. given #370 (T,wt=29): 2502 f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)). [para(3(a,1),2229(a,1,2,2))]. given #371 (T,wt=29): 2504 f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)). [para(42(a,1),2229(a,1,2,2))]. given #372 (A,wt=55): 193 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(x,f(x,f(f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(x,z)))),x),f(x,u)))),x),f(x,w)))),x),f(x,v5)))) = x. [para(6(a,1),11(a,1,2,2,1,1,2,1)),rewrite([3(13),11(17),3(12)])]. Demod_limit: f(f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w)))),f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w)))),v5),f(f(f(f(f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w)))),v5),v5),f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w)))),x))),f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w)))),f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),v6)))),f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w)))),f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),v7)))),f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w)))),f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))),v8)))) = f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,w))). [para(96(a,1),193(a,1,2,2,1,1,2,2,1,1,2,2,1,1,2,2,2))]. Demod_limit (steps=-1, size=1053). The most recent kept clause is 4791. From here on, a short message will be printed for each 100 times the limit is hit. given #373 (T,wt=19): 4776 f(f(x,f(x,x)),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(2679(a,1),2504(a,1,1,1,1)),rewrite([2679(6),42(3),2679(5),2679(7),2679(8),42(5),2679(13),2679(14),42(11)])]. given #374 (T,wt=19): 4777 f(f(x,f(x,x)),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(2685(a,1),2504(a,1,1,1,1)),rewrite([2685(6),42(3),2685(5),2685(7),2685(8),42(5),2685(13),2685(14),42(11)])]. given #375 (T,wt=25): 4778 f(f(f(x,x),x),f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))) = f(x,x). [para(2680(a,1),2504(a,1,1,1,1)),rewrite([2680(7),2680(8),2680(9),2680(9),2680(17),2680(17)])]. given #376 (T,wt=25): 4779 f(f(f(x,x),x),f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))) = f(x,x). [para(2740(a,1),2504(a,1,1,1,1)),rewrite([2740(7),2740(8),2740(9),2740(9),2740(17),2740(17)])]. given #377 (A,wt=57): 194 f(f(f(x,y),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(f(f(x,y),f(x,y)),z),z),f(x,y)),x))),f(x,y)),f(f(x,y),u)))) = f(x,y). [para(42(a,1),11(a,1,2,2,1,1,2,2,2))]. given #378 (T,wt=27): 4810 f(f(f(x,f(x,f(x,f(f(x,x),y)))),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(4776(a,1),139(a,1,2,1,2,1)),rewrite([4776(21),678(15),4776(18),3413(13),42(13),22(11)])]. given #379 (T,wt=27): 4830 f(f(f(x,f(x,f(x,f(y,f(x,x))))),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(4777(a,1),139(a,1,2,1,2,1)),rewrite([4777(21),678(15),4777(18),3413(13),42(13),22(11)])]. given #380 (T,wt=29): 2696 f(f(f(x,f(f(x,x),y)),x),f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(x,z)))) = x. [para(2679(a,1),55(a,1,2,2,1)),rewrite([2684(15)])]. given #381 (T,wt=29): 2700 f(f(f(x,f(f(x,x),y)),x),f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(z,x)))) = x. [para(2679(a,1),562(a,1,2,2,1)),rewrite([2684(15)])]. given #382 (A,wt=57): 195 f(f(f(x,y),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(f(f(x,y),f(x,y)),z),z),f(x,y)),f(f(x,y),u)))),f(x,y)),x))) = f(x,y). [para(42(a,1),11(a,1,2,2,2))]. given #383 (T,wt=29): 2701 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(x,f(x,f(f(x,x),z)))))) = f(x,x). [para(2679(a,1),62(a,1,1,2)),rewrite([69(15),2679(5),2679(6),42(3),2679(8),2679(17)])]. given #384 (T,wt=25): 5012 f(x,f(f(x,x),f(f(x,f(x,x)),f(x,f(x,f(f(x,x),y)))))) = f(x,x). [para(3134(a,1),2701(a,1,2,2,1)),rewrite([3413(3)])]. given #385 (T,wt=25): 5014 f(f(x,x),f(x,f(f(f(x,x),x),f(f(x,x),f(f(x,x),f(x,y)))))) = x. [para(3398(a,1),2701(a,1,2,1)),rewrite([3398(5),42(7),2828(5),42(8),42(14)])]. given #386 (T,wt=25): 5057 f(x,f(f(x,x),f(f(x,f(x,x)),f(x,f(x,f(y,f(x,x))))))) = f(x,x). [para(57(a,1),5012(a,1,2,2,2,2,2))]. given #387 (A,wt=45): 196 f(f(x,x),f(x,f(f(f(x,f(f(y,f(x,x)),f(f(f(f(y,f(x,x)),f(f(y,f(x,x)),f(y,f(x,x)))),x),f(x,z)))),x),f(x,u)))) = x. [para(57(a,1),11(a,1,2,2,1,1,2,1)),rewrite([57(10)])]. given #388 (T,wt=25): 5067 f(f(x,x),f(x,f(f(f(x,x),x),f(f(x,x),f(f(x,x),f(y,x)))))) = x. [para(57(a,1),5014(a,1,2,2,2,2,2))]. given #389 (T,wt=29): 2752 f(f(f(x,f(y,f(x,x))),x),f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,z)))) = x. [para(2685(a,1),55(a,1,2,2,1)),rewrite([2741(15)])]. given #390 (T,wt=29): 2756 f(f(f(x,f(y,f(x,x))),x),f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(z,x)))) = x. [para(2685(a,1),562(a,1,2,2,1)),rewrite([2741(15)])]. given #391 (T,wt=29): 2757 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(x,f(x,f(z,f(x,x))))))) = f(x,x). [para(2685(a,1),62(a,1,1,2)),rewrite([69(15),2685(5),2685(6),42(3),2685(8),2685(17)])]. given #392 (A,wt=35): 197 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(z,x)))),x),f(x,u)))) = x. [para(57(a,1),11(a,1,2,2,1,1,2,2,2))]. given #393 (T,wt=29): 2766 f(f(f(f(x,y),f(x,y)),f(f(f(x,y),f(x,y)),y)),f(f(x,y),f(x,y))) = f(x,y). [para(3(a,1),2680(a,1,1,2,2))]. given #394 (T,wt=29): 2769 f(f(f(f(x,y),f(x,y)),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))) = f(x,y). [para(42(a,1),2680(a,1,1,2,2))]. given #395 (T,wt=19): 5321 f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),x) = f(x,x). [para(2679(a,1),2769(a,1,1,1,1)),rewrite([2679(6),42(3),2679(5),2679(6),42(3),2679(11),2679(12),42(9),2679(12)])]. given #396 (T,wt=19): 5322 f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),x) = f(x,x). [para(2685(a,1),2769(a,1,1,1,1)),rewrite([2685(6),42(3),2685(5),2685(6),42(3),2685(11),2685(12),42(9),2685(12)])]. given #397 (A,wt=35): 198 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(x,z)))),x),f(u,x)))) = x. [para(57(a,1),11(a,1,2,2,2))]. given #398 (T,wt=21): 5340 f(f(x,x),f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))) = x. [para(5321(a,1),179(a,1,1)),rewrite([5321(8),5321(9),42(4),5321(16),5321(17),42(12)])]. given #399 (T,wt=21): 5364 f(f(x,x),f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))) = x. [para(5322(a,1),179(a,1,1)),rewrite([5322(8),5322(9),42(4),5322(16),5322(17),42(12)])]. given #400 (T,wt=23): 5357 f(f(f(x,x),x),f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))) = x. [para(5321(a,1),2438(a,1,1,1)),rewrite([5321(8),5321(9),42(4),5321(9),5321(10),42(5),5321(17),5321(18),42(13)])]. given #401 (T,wt=23): 5358 f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))) = x. [para(5321(a,1),2504(a,1,1,1,1)),rewrite([5321(8),42(3),5321(7),5321(9),5321(10),42(5),5321(17),5321(18),42(13)])]. given #402 (A,wt=45): 199 f(f(x,x),f(x,f(f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),f(f(f(x,x),y),f(f(x,x),y))),x),f(x,z)))),x),f(x,u)))) = x. [para(63(a,1),11(a,1,2,2,1,1,2,1)),rewrite([63(10)])]. given #403 (T,wt=23): 5361 f(f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))),x) = f(x,x). [para(5321(a,1),2769(a,1,1,1,1)),rewrite([5321(8),42(3),5321(7),5321(8),42(3),5321(15),5321(16),42(11),5321(16)])]. given #404 (T,wt=23): 5381 f(f(f(x,x),x),f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))) = x. [para(5322(a,1),2438(a,1,1,1)),rewrite([5322(8),5322(9),42(4),5322(9),5322(10),42(5),5322(17),5322(18),42(13)])]. given #405 (T,wt=23): 5382 f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))) = x. [para(5322(a,1),2504(a,1,1,1,1)),rewrite([5322(8),42(3),5322(7),5322(9),5322(10),42(5),5322(17),5322(18),42(13)])]. given #406 (T,wt=23): 5385 f(f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))),x) = f(x,x). [para(5322(a,1),2769(a,1,1,1,1)),rewrite([5322(8),42(3),5322(7),5322(8),42(3),5322(15),5322(16),42(11),5322(16)])]. given #407 (A,wt=55): 200 f(f(x,x),f(f(f(f(f(x,x),f(y,x)),f(f(x,x),f(y,x))),z),f(f(f(f(f(x,x),z),z),f(f(x,x),f(y,x))),f(f(f(x,x),f(y,x)),u)))) = f(f(x,x),f(y,x)). [para(180(a,1),3(a,1,1)),rewrite([34(13)])]. given #408 (T,wt=25): 5323 f(f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))),f(x,x)) = x. [para(2680(a,1),2769(a,1,1,1,1)),rewrite([2680(7),2680(8),2680(8),2680(16),2680(16),2680(18)])]. given #409 (T,wt=25): 5324 f(f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))),f(x,x)) = x. [para(2740(a,1),2769(a,1,1,1,1)),rewrite([2740(7),2740(8),2740(8),2740(16),2740(16),2740(18)])]. given #410 (T,wt=25): 5462 f(f(x,x),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))))) = x. [para(5361(a,1),179(a,1,1)),rewrite([5361(10),5361(11),42(4),5361(20),5361(21),42(14)])]. given #411 (T,wt=25): 5511 f(f(x,x),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))))) = x. [para(5385(a,1),179(a,1,1)),rewrite([5385(10),5385(11),42(4),5385(20),5385(21),42(14)])]. given #412 (A,wt=33): 201 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,f(z,f(y,y)))),f(y,f(z,f(y,y)))),y),f(y,u)))) = y. [para(180(a,1),3(a,1,2,1)),rewrite([42(4),42(5),42(9)])]. given #413 (T,wt=27): 5347 f(f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(5321(a,1),648(a,1,1,2,1)),rewrite([5339(15)])]. given #414 (T,wt=27): 5348 f(f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(5321(a,1),804(a,1,1,2,1)),rewrite([5339(15)])]. given #415 (T,wt=27): 5371 f(f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(5322(a,1),648(a,1,1,2,1)),rewrite([5363(15)])]. given #416 (T,wt=27): 5372 f(f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(5322(a,1),804(a,1,1,2,1)),rewrite([5363(15)])]. given #417 (A,wt=51): 202 f(f(x,y),f(f(f(y,y),f(f(f(y,x),f(y,x)),f(z,f(y,x)))),f(f(f(f(f(y,x),f(y,x)),f(f(f(y,x),f(y,x)),f(z,f(y,x)))),y),f(y,u)))) = y. [para(180(a,1),3(a,1,2,2,1,1,1))]. given #418 (T,wt=27): 5477 f(f(f(x,x),x),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))))) = x. [para(5361(a,1),2438(a,1,1,1)),rewrite([5361(10),5361(11),42(4),5361(11),5361(12),42(5),5361(21),5361(22),42(15)])]. given #419 (T,wt=27): 5478 f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))))) = x. [para(5361(a,1),2504(a,1,1,1,1)),rewrite([5361(10),42(3),5361(9),5361(11),5361(12),42(5),5361(21),5361(22),42(15)])]. given #420 (T,wt=27): 5481 f(f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))))),x) = f(x,x). [para(5361(a,1),2769(a,1,1,1,1)),rewrite([5361(10),42(3),5361(9),5361(10),42(3),5361(19),5361(20),42(13),5361(20)])]. given #421 (T,wt=27): 5526 f(f(f(x,x),x),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))))) = x. [para(5385(a,1),2438(a,1,1,1)),rewrite([5385(10),5385(11),42(4),5385(11),5385(12),42(5),5385(21),5385(22),42(15)])]. given #422 (A,wt=49): 204 f(f(x,x),f(f(f(f(f(x,x),f(y,x)),f(f(x,x),f(y,x))),z),f(f(f(f(f(x,x),z),z),f(f(x,x),f(y,x))),f(y,x)))) = f(f(x,x),f(y,x)). [para(180(a,1),9(a,1,1)),rewrite([34(13)])]. given #423 (T,wt=27): 5527 f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))))) = x. [para(5385(a,1),2504(a,1,1,1,1)),rewrite([5385(10),42(3),5385(9),5385(11),5385(12),42(5),5385(21),5385(22),42(15)])]. given #424 (T,wt=27): 5530 f(f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))))),x) = f(x,x). [para(5385(a,1),2769(a,1,1,1,1)),rewrite([5385(10),42(3),5385(9),5385(10),42(3),5385(19),5385(20),42(13),5385(20)])]. given #425 (T,wt=29): 3277 f(f(f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))),f(f(x,x),x)),x) = f(f(x,x),x). [para(2828(a,1),141(a,1,2,2,1,1,1)),rewrite([673(16),34(15),34(17),13(14)])]. given #426 (T,wt=29): 3440 f(f(f(x,y),f(x,y)),f(f(x,y),f(f(f(f(x,y),f(x,y)),f(x,y)),x))) = f(x,y). [back_rewrite(3163),rewrite([3398(12)])]. given #427 (A,wt=53): 205 f(f(x,f(y,z)),f(f(y,z),f(f(f(f(f(f(y,z),x),f(f(y,z),f(u,f(f(y,z),f(y,z))))),f(f(y,z),f(u,f(f(y,z),f(y,z))))),f(y,z)),z))) = f(y,z). [para(180(a,1),9(a,1,2,1)),rewrite([42(9),42(12),42(19)])]. given #428 (T,wt=29): 3441 f(f(f(x,y),f(x,y)),f(f(x,y),f(f(f(f(x,y),f(x,y)),f(x,y)),y))) = f(x,y). [back_rewrite(3155),rewrite([3398(12)])]. given #429 (T,wt=29): 3451 f(f(f(f(x,x),x),f(f(x,x),x)),f(f(f(x,x),x),f(x,f(x,x)))) = f(f(x,x),x). [back_rewrite(969),rewrite([3398(11)])]. given #430 (T,wt=29): 3453 f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(x,f(f(f(x,x),x),y)))) = f(f(x,x),x). [back_rewrite(682),rewrite([3398(9)])]. given #431 (T,wt=25): 5871 f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(x,f(x,x)))) = f(f(x,x),x). [para(34(a,1),3453(a,1,2,2,2))]. given #432 (A,wt=51): 207 f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),z),f(f(f(f(x,z),z),f(x,f(y,f(x,x)))),f(f(x,f(y,f(x,x))),u)))) = f(x,f(y,f(x,x))). [para(186(a,1),3(a,1,1)),rewrite([42(13)])]. given #433 (T,wt=27): 5880 f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),f(f(x,x),x))) = f(x,f(x,x)). [para(13(a,1),5871(a,1,1,2,1)),rewrite([42(7),42(10),42(13)])]. given #434 (T,wt=29): 3466 f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(x,f(x,x)),f(f(x,x),x))) = f(x,f(x,x)). [back_rewrite(971),rewrite([3413(10)])]. given #435 (T,wt=29): 3472 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(y,y),y)),f(f(y,y),y)),y),f(y,z)))) = y. [para(3398(a,1),3(a,1,2,1))]. given #436 (T,wt=29): 3484 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(y,y),y)),f(f(y,y),y)),y),f(z,y)))) = y. [para(3398(a,1),68(a,1,2,1))]. given #437 (A,wt=47): 209 f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),z),f(f(f(f(x,z),z),f(x,f(y,f(x,x)))),f(y,f(x,x))))) = f(x,f(y,f(x,x))). [para(186(a,1),9(a,1,1)),rewrite([42(13)])]. given #438 (T,wt=23): 5967 f(f(x,y),f(f(f(f(y,x),f(f(y,y),y)),f(f(y,y),y)),y)) = y. [para(57(a,1),3484(a,1,2))]. given #439 (T,wt=23): 6111 f(f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)),x) = f(x,x). [para(5967(a,1),129(a,1,2,2,1)),rewrite([13(33),34(12)]),flip(a)]. given #440 (T,wt=23): 6112 f(f(f(f(f(x,x),x),f(x,f(x,x))),f(x,f(x,x))),f(x,x)) = x. [para(5967(a,1),130(a,1,2,2,1)),rewrite([42(5),42(8),42(16),42(19),42(26),42(29),42(37),22(35),42(13),42(5),42(8)]),flip(a)]. given #441 (T,wt=25): 6158 f(f(x,x),f(x,f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)))) = x. [para(6111(a,1),179(a,1,1)),rewrite([6111(10),6111(11),42(4),6111(20),6111(21),42(14)])]. given #442 (A,wt=57): 211 f(f(f(f(f(x,x),x),f(x,y)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(x,x)),f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(f(x,x),x),z)))) = f(f(x,x),x). [para(159(a,1),3(a,1,2,2,1,1,1))]. given #443 (T,wt=27): 6048 f(f(x,x),f(f(f(f(x,f(y,f(x,x))),f(f(x,x),x)),f(f(x,x),x)),x)) = x. [para(22(a,1),5967(a,1,1))]. given #444 (T,wt=27): 6050 f(f(f(x,x),x),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)),x)) = x. [para(22(a,1),5967(a,1,2,1,1)),rewrite([673(6)])]. given #445 (T,wt=23): 6230 f(f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)),x) = f(x,x). [para(6050(a,1),129(a,1,2,2,1)),rewrite([13(33),34(12)]),flip(a)]. given #446 (T,wt=23): 6231 f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,f(x,x))),f(x,x)) = x. [para(6050(a,1),132(a,1,2,2,1)),rewrite([42(3),42(5),42(8),42(14),42(16),42(19),42(24),42(26),42(29),42(37),22(35),42(13),42(3),42(5),42(8)]),flip(a)]. given #447 (A,wt=37): 212 f(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(f(x,y),f(x,y))) = f(x,y). [para(3(a,1),159(a,1,1,2,2))]. given #448 (T,wt=25): 6240 f(f(x,x),f(x,f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)))) = x. [para(6230(a,1),179(a,1,1)),rewrite([6230(10),6230(11),42(4),6230(20),6230(21),42(14)])]. given #449 (T,wt=27): 6051 f(f(x,x),f(f(f(f(x,f(f(x,x),y)),f(f(x,x),x)),f(f(x,x),x)),x)) = x. [para(34(a,1),5967(a,1,1))]. given #450 (T,wt=27): 6167 f(f(f(x,x),x),f(x,f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)))) = x. [para(6111(a,1),2438(a,1,1,1)),rewrite([6111(10),6111(11),42(4),6111(11),6111(12),42(5),6111(21),6111(22),42(15)])]. given #451 (T,wt=27): 6168 f(f(x,f(x,x)),f(x,f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)))) = x. [para(6111(a,1),2504(a,1,1,1,1)),rewrite([6111(10),42(3),6111(9),6111(11),6111(12),42(5),6111(21),6111(22),42(15)])]. given #452 (A,wt=37): 215 f(f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,y)),x)),f(f(x,y),f(x,y))) = f(x,y). [para(42(a,1),159(a,1,1,2,2))]. given #453 (T,wt=27): 6171 f(f(x,f(x,f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)))),x) = f(x,x). [para(6111(a,1),2769(a,1,1,1,1)),rewrite([6111(10),42(3),6111(9),6111(10),42(3),6111(19),6111(20),42(13),6111(20)])]. given #454 (T,wt=27): 6178 f(x,f(f(x,x),f(f(f(f(x,x),x),f(x,f(x,x))),f(x,f(x,x))))) = f(x,x). [para(6112(a,1),179(a,1,1)),rewrite([6112(10),6112(10),6112(21),6112(21)])]. given #455 (T,wt=27): 6250 f(f(f(x,x),x),f(x,f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)))) = x. [para(6230(a,1),2438(a,1,1,1)),rewrite([6230(10),6230(11),42(4),6230(11),6230(12),42(5),6230(21),6230(22),42(15)])]. given #456 (T,wt=27): 6251 f(f(x,f(x,x)),f(x,f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)))) = x. [para(6230(a,1),2504(a,1,1,1,1)),rewrite([6230(10),42(3),6230(9),6230(11),6230(12),42(5),6230(21),6230(22),42(15)])]. given #457 (A,wt=51): 217 f(f(f(f(f(x,x),x),f(x,y)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(x,x)),f(f(f(x,f(x,x)),f(f(x,x),x)),x))) = f(f(x,x),x). [para(159(a,1),9(a,1,2,2,1,1,1))]. given #458 (T,wt=27): 6254 f(f(x,f(x,f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)))),x) = f(x,x). [para(6230(a,1),2769(a,1,1,1,1)),rewrite([6230(10),42(3),6230(9),6230(10),42(3),6230(19),6230(20),42(13),6230(20)])]. given #459 (T,wt=27): 6261 f(x,f(f(x,x),f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,f(x,x))))) = f(x,x). [para(6231(a,1),179(a,1,1)),rewrite([6231(10),6231(10),6231(21),6231(21)])]. given #460 (T,wt=29): 3610 f(f(x,x),f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))))) = x. [para(155(a,1),3444(a,1,2,2,2))]. given #461 (T,wt=29): 3652 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(f(x,x),f(x,y)))))) = x. [para(2680(a,1),158(a,1,1,1)),rewrite([2680(7),2680(8),2680(8),2680(9),2680(10),2680(10),2680(11),2680(20)])]. given #462 (A,wt=49): 218 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),y),f(f(f(y,y),y),f(z,y)))),f(f(f(y,y),y),f(f(f(y,y),y),f(z,y)))),y),f(y,u)))) = y. [para(160(a,1),3(a,1,2,1))]. given #463 (T,wt=29): 3653 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(f(x,x),f(y,x)))))) = x. [para(2740(a,1),158(a,1,1,1)),rewrite([2740(7),2740(8),2740(8),2740(9),2740(10),2740(10),2740(11),2740(20)])]. given #464 (T,wt=29): 4133 f(x,f(f(f(x,x),f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x))))),f(x,x))) = f(x,x). [para(13(a,1),4088(a,1,1)),rewrite([42(5)])]. given #465 (T,wt=29): 4172 f(x,f(f(f(x,x),f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y)))),f(x,x))) = f(x,x). [para(13(a,1),4159(a,1,1)),rewrite([42(5)])]. given #466 (T,wt=29): 4439 f(f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(f(x,x),f(x,y))))),f(x,x)) = x. [para(13(a,1),4210(a,1,1,1,2)),rewrite([42(6),42(9),42(16)])]. given #467 (A,wt=49): 220 f(x,f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))))) = f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))). [para(160(a,1),13(a,1,1))]. given #468 (T,wt=29): 4442 f(f(f(f(x,x),x),f(f(f(x,x),x),f(f(x,x),f(f(x,x),f(y,x))))),f(x,x)) = x. [para(13(a,1),4231(a,1,1,1,2)),rewrite([42(6),42(9),42(16)])]. given #469 (T,wt=29): 4503 f(f(f(x,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(258(a,1),2436(a,1,1,1)),rewrite([258(14),258(15),42(4),258(15),258(16),42(5),258(26),258(27),42(16)])]. given #470 (T,wt=29): 4507 f(f(f(x,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(723(a,1),2436(a,1,1,1)),rewrite([723(14),723(15),42(4),723(15),723(16),42(5),723(26),723(27),42(16)])]. given #471 (T,wt=29): 4534 f(f(f(x,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(2776(a,1),2438(a,1,1,1)),rewrite([2776(11),2776(12),42(4),2776(12),2776(13),42(5),2776(23),2776(24),42(16)])]. given #472 (A,wt=41): 222 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))),x),f(x,z)))),x),f(x,u)))) = x. [para(160(a,1),8(a,1,2,1,2,2,1,1,1)),rewrite([160(11),219(15),160(10),160(10)])]. given #473 (T,wt=29): 4535 f(f(f(x,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(2777(a,1),2438(a,1,1,1)),rewrite([2777(11),2777(12),42(4),2777(12),2777(13),42(5),2777(23),2777(24),42(16)])]. given #474 (T,wt=29): 4536 f(f(f(x,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(2815(a,1),2438(a,1,1,1)),rewrite([2815(11),2815(12),42(4),2815(12),2815(13),42(5),2815(23),2815(24),42(16)])]. given #475 (T,wt=29): 4537 f(f(f(x,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(2816(a,1),2438(a,1,1,1)),rewrite([2816(11),2816(12),42(4),2816(12),2816(13),42(5),2816(23),2816(24),42(16)])]. given #476 (T,wt=29): 4560 f(f(x,x),f(x,f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(f(x,x),z))))) = x. [para(4525(a,1),247(a,1,2,2,2,1,1,1)),rewrite([42(4),42(4),42(15),42(16)])]. given #477 (A,wt=37): 223 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(u,y)))))) = y. [para(160(a,1),9(a,1,1,2)),rewrite([160(10),160(10),160(12),160(15),160(26)])]. given #478 (T,wt=29): 4561 f(f(x,x),f(x,f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(z,f(x,x)))))) = x. [para(4525(a,1),588(a,1,2,2,2,1,1,1)),rewrite([42(4),42(4),42(15),42(16)])]. given #479 (T,wt=29): 4587 f(f(x,x),f(x,f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(x,f(f(x,x),z))))) = x. [para(4526(a,1),247(a,1,2,2,2,1,1,1)),rewrite([42(4),42(4),42(15),42(16)])]. given #480 (T,wt=29): 4588 f(f(x,x),f(x,f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(x,f(z,f(x,x)))))) = x. [para(4526(a,1),588(a,1,2,2,2,1,1,1)),rewrite([42(4),42(4),42(15),42(16)])]. given #481 (T,wt=29): 4758 f(f(x,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(258(a,1),2502(a,1,1,1,1)),rewrite([258(14),42(3),258(13),258(15),258(16),42(5),258(26),258(27),42(16)])]. given #482 (A,wt=55): 224 f(f(f(x,y),f(x,y)),f(f(x,y),f(f(f(f(x,y),f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,y)),f(z,f(x,y))))),f(x,y)),y))) = f(x,y). [para(160(a,1),9(a,1,2,2,1,1,1)),rewrite([160(21)])]. given #483 (T,wt=29): 4762 f(f(x,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(723(a,1),2502(a,1,1,1,1)),rewrite([723(14),42(3),723(13),723(15),723(16),42(5),723(26),723(27),42(16)])]. given #484 (T,wt=29): 4784 f(f(x,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(2776(a,1),2504(a,1,1,1,1)),rewrite([2776(11),42(3),2776(10),2776(12),2776(13),42(5),2776(23),2776(24),42(16)])]. given #485 (T,wt=29): 4785 f(f(x,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(2777(a,1),2504(a,1,1,1,1)),rewrite([2777(11),42(3),2777(10),2777(12),2777(13),42(5),2777(23),2777(24),42(16)])]. given #486 (T,wt=29): 4786 f(f(x,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(2815(a,1),2504(a,1,1,1,1)),rewrite([2815(11),42(3),2815(10),2815(12),2815(13),42(5),2815(23),2815(24),42(16)])]. given #487 (A,wt=53): 226 f(f(x,y),f(y,f(f(f(f(f(f(f(x,y),f(x,y)),f(z,f(x,y))),f(y,y)),f(y,y)),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),u)))) = f(f(x,y),f(x,y)). [para(13(a,1),14(a,1,2,1))]. given #488 (T,wt=27): 6870 f(f(x,y),f(f(f(f(y,x),f(y,f(f(y,y),z))),f(y,f(f(y,y),z))),y)) = y. [para(226(a,1),174(a,1,2,2)),rewrite([57(23)])]. given #489 (T,wt=27): 6881 f(f(x,y),f(f(f(f(y,x),f(y,f(z,f(y,y)))),f(y,f(z,f(y,y)))),y)) = y. [para(226(a,1),201(a,1,2,2)),rewrite([57(23)])]. given #490 (T,wt=29): 4787 f(f(x,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(2816(a,1),2504(a,1,1,1,1)),rewrite([2816(11),42(3),2816(10),2816(12),2816(13),42(5),2816(23),2816(24),42(16)])]. given #491 (T,wt=29): 4845 f(f(f(f(x,x),f(f(x,x),f(f(x,x),f(x,y)))),f(f(x,x),x)),x) = f(f(x,x),x). [para(4778(a,1),139(a,1,2,1,2,1)),rewrite([4778(26),42(18),673(16),4778(22),3398(16),13(14)])]. given #492 (A,wt=53): 228 f(f(x,y),f(x,f(f(f(f(f(f(f(x,y),f(x,y)),f(z,f(x,y))),f(x,x)),f(x,x)),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),u)))) = f(f(x,y),f(x,y)). [para(42(a,1),14(a,1,2,1))]. given #493 (T,wt=29): 4858 f(f(f(f(x,x),f(f(x,x),f(f(x,x),f(y,x)))),f(f(x,x),x)),x) = f(f(x,x),x). [para(4779(a,1),139(a,1,2,1,2,1)),rewrite([4779(26),42(18),673(16),4779(22),3398(16),13(14)])]. given #494 (T,wt=29): 4950 f(f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(x,f(x,f(f(x,x),z))))),x) = f(x,x). [para(2701(a,1),57(a,1,2,1)),rewrite([2701(24),42(14),2701(24)])]. given #495 (T,wt=29): 5132 f(f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(x,f(x,f(z,f(x,x)))))),x) = f(x,x). [para(2757(a,1),57(a,1,2,1)),rewrite([2757(24),42(14),2757(24)])]. given #496 (T,wt=29): 5294 f(f(x,f(x,f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(f(x,x),z))))),x) = f(x,x). [para(258(a,1),2766(a,1,1,1,1)),rewrite([258(14),42(3),258(13),258(14),42(3),258(24),258(25),42(14),258(25)])]. given #497 (A,wt=41): 229 f(x,f(f(x,f(f(f(x,x),f(y,x)),f(f(x,x),f(y,x)))),f(f(f(f(x,x),f(y,x)),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(42(a,1),14(a,1,2,2,1,1))]. given #498 (T,wt=29): 5298 f(f(x,f(x,f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(z,f(x,x)))))),x) = f(x,x). [para(723(a,1),2766(a,1,1,1,1)),rewrite([723(14),42(3),723(13),723(14),42(3),723(24),723(25),42(14),723(25)])]. given #499 (T,wt=29): 5325 f(f(x,f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,f(f(x,x),z))))),x) = f(x,x). [para(2776(a,1),2769(a,1,1,1,1)),rewrite([2776(11),42(3),2776(10),2776(11),42(3),2776(21),2776(22),42(14),2776(22)])]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 63 (0.00 of 54.94 sec). given #500 (T,wt=29): 5326 f(f(x,f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,f(z,f(x,x)))))),x) = f(x,x). [para(2777(a,1),2769(a,1,1,1,1)),rewrite([2777(11),42(3),2777(10),2777(11),42(3),2777(21),2777(22),42(14),2777(22)])]. given #501 (T,wt=29): 5327 f(f(x,f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,f(f(x,x),z))))),x) = f(x,x). [para(2815(a,1),2769(a,1,1,1,1)),rewrite([2815(11),42(3),2815(10),2815(11),42(3),2815(21),2815(22),42(14),2815(22)])]. given #502 (A,wt=43): 231 f(x,f(f(y,x),f(f(f(f(f(f(x,x),f(z,x)),f(f(y,x),f(y,x))),f(f(y,x),f(y,x))),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(57(a,1),14(a,1,2,1))]. given #503 (T,wt=29): 5328 f(f(x,f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,f(z,f(x,x)))))),x) = f(x,x). [para(2816(a,1),2769(a,1,1,1,1)),rewrite([2816(11),42(3),2816(10),2816(11),42(3),2816(21),2816(22),42(14),2816(22)])]. given #504 (T,wt=29): 5386 f(f(x,x),f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(x,z)))),x)) = x. [para(57(a,1),198(a,1,2))]. given #505 (T,wt=29): 5406 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))))) = f(x,x). [para(13(a,1),5340(a,1,1)),rewrite([42(8)])]. given #506 (T,wt=29): 5419 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))))) = f(x,x). [para(13(a,1),5364(a,1,1)),rewrite([42(8)])]. given #507 (A,wt=43): 233 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(z,x)),f(f(x,y),f(x,y))),f(f(x,y),f(x,y))),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(63(a,1),14(a,1,2,1))]. given #508 (T,wt=29): 5687 f(f(x,x),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))))))) = x. [para(5481(a,1),179(a,1,1)),rewrite([5481(12),5481(13),42(4),5481(24),5481(25),42(16)])]. given #509 (T,wt=29): 5729 f(f(x,x),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))))))) = x. [para(5530(a,1),179(a,1,1)),rewrite([5530(12),5530(13),42(4),5530(24),5530(25),42(16)])]. given #510 (T,wt=29): 5750 f(f(x,x),f(x,f(f(f(x,x),x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))))) = x. [para(216(a,1),3440(a,1,1,1)),rewrite([216(9),216(10),216(10),216(10),216(11),216(22)])]. given #511 (T,wt=29): 5798 f(x,f(f(x,x),f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(f(x,x),y)))))))) = f(x,x). [para(5321(a,1),3440(a,1,1,1)),rewrite([5321(8),42(3),5321(7),5321(8),5321(9),42(4),5321(8),5321(19)])]. given #512 (A,wt=53): 235 f(f(x,x),f(x,f(f(f(f(f(x,f(y,f(x,x))),f(f(f(x,x),x),f(f(f(x,x),x),f(x,z)))),f(f(f(x,x),x),f(f(f(x,x),x),f(x,z)))),x),f(x,u)))) = x. [para(39(a,1),14(a,1,2,1)),rewrite([42(4),42(23),42(24),42(28)])]. given #513 (T,wt=29): 5799 f(x,f(f(x,x),f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(y,f(x,x))))))))) = f(x,x). [para(5322(a,1),3440(a,1,1,1)),rewrite([5322(8),42(3),5322(7),5322(8),5322(9),42(4),5322(8),5322(19)])]. given #514 (T,wt=29): 5872 f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(x,f(y,f(f(x,x),x))))) = f(f(x,x),x). [para(57(a,1),3453(a,1,2,2,2))]. given #515 (T,wt=29): 6045 f(x,f(f(f(f(f(x,x),f(y,x)),f(x,f(x,x))),f(x,f(x,x))),f(x,x))) = f(x,x). [para(13(a,1),5967(a,1,1)),rewrite([42(6),42(9)])]. given #516 (T,wt=29): 6053 f(x,f(f(f(f(f(x,x),f(x,y)),f(x,f(x,x))),f(x,f(x,x))),f(x,x))) = f(x,x). [para(42(a,1),5967(a,1,1)),rewrite([42(6),42(9)])]. given #517 (A,wt=41): 236 f(x,f(f(x,x),f(f(f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(39(a,1),14(a,1,2,2,1,1,1)),rewrite([42(3),42(5),156(9),42(5),42(7)])]. given #518 (T,wt=29): 6056 f(f(f(f(x,y),f(x,y)),y),f(f(f(f(x,y),f(f(y,y),y)),f(f(y,y),y)),y)) = y. [para(57(a,1),5967(a,1,2,1,1,1))]. given #519 (T,wt=29): 6058 f(f(f(f(x,y),f(x,y)),x),f(f(f(f(x,y),f(f(x,x),x)),f(f(x,x),x)),x)) = x. [para(63(a,1),5967(a,1,2,1,1,1))]. given #520 (T,wt=29): 6398 f(f(x,x),f(x,f(x,f(x,f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)))))) = x. [para(6171(a,1),179(a,1,1)),rewrite([6171(12),6171(13),42(4),6171(24),6171(25),42(16)])]. given #521 (T,wt=29): 6437 f(f(x,x),f(x,f(x,f(x,f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)))))) = x. [para(6254(a,1),179(a,1,1)),rewrite([6254(12),6254(13),42(4),6254(24),6254(25),42(16)])]. given #522 (A,wt=43): 237 f(x,f(f(x,x),f(f(f(f(f(f(x,x),f(y,x)),f(f(x,x),f(x,z))),f(f(x,x),f(x,z))),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(167(a,1),14(a,1,2,1))]. given #523 (T,wt=29): 6879 f(f(x,x),f(f(x,f(f(f(x,x),y),f(f(f(f(f(x,x),y),y),x),f(z,x)))),x)) = x. [para(226(a,1),197(a,1,2,2)),rewrite([57(25)])]. given #524 (T,wt=31): 1173 f(x,f(f(x,x),f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),x),f(x,z))))) = f(x,x). [para(828(a,1),179(a,1,1)),rewrite([828(12),828(12),828(25),828(25)])]. given #525 (T,wt=31): 1178 f(x,f(f(x,x),f(f(f(x,x),f(f(y,x),f(y,x))),f(f(f(y,x),x),f(z,x))))) = f(x,x). [para(871(a,1),179(a,1,1)),rewrite([871(12),871(12),871(25),871(25)])]. given #526 (T,wt=31): 1239 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y. [para(42(a,1),66(a,1,2,2,1,1,1))]. given #527 (A,wt=37): 238 f(f(x,x),f(x,f(f(f(f(f(x,f(y,f(x,x))),f(x,f(f(x,x),z))),f(x,f(f(x,x),z))),x),f(x,u)))) = x. [para(177(a,1),14(a,1,2,1)),rewrite([42(4),42(15),42(16),42(20)])]. given #528 (T,wt=31): 1321 f(f(x,x),f(x,f(f(x,y),f(f(f(f(f(f(x,x),z),y),y),f(x,x)),f(u,f(x,x)))))) = x. [para(13(a,1),588(a,1,2,1)),rewrite([42(4),42(17)])]. given #529 (T,wt=31): 1500 f(f(x,x),f(x,f(f(x,y),f(f(f(f(f(z,f(x,x)),y),y),f(x,x)),f(f(x,x),u))))) = x. [para(826(a,1),179(a,1,1)),rewrite([826(13),826(14),42(4),826(26),826(27),42(17)])]. given #530 (T,wt=31): 1532 f(f(x,x),f(x,f(f(x,y),f(f(f(f(f(z,f(x,x)),y),y),f(x,x)),f(u,f(x,x)))))) = x. [para(870(a,1),179(a,1,1)),rewrite([870(13),870(14),42(4),870(26),870(27),42(17)])]. given #531 (T,wt=31): 1618 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(13(a,1),77(a,1,2,2,1,1,1))]. given #532 (A,wt=49): 240 f(f(x,x),f(x,f(f(f(x,f(x,f(f(f(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),f(x,w)))),x),f(x,v5)))) = x. [para(14(a,1),11(a,1,2,2,1,1,2,1)),rewrite([42(4),42(7),42(12),42(13),25(14),42(6),42(11),42(12)])]. given #533 (T,wt=31): 1746 f(f(f(f(x,y),f(x,y)),y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(z,y)))) = y. [para(42(a,1),566(a,1,2,2,1,1,1))]. given #534 (T,wt=31): 1781 f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [para(13(a,1),570(a,1,2,2,1,1,1))]. given #535 (T,wt=31): 1855 f(x,f(f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y)))),f(x,x))) = f(x,x). [para(13(a,1),1847(a,1,1)),rewrite([42(4),42(6)])]. given #536 (T,wt=31): 1865 f(x,f(f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))),f(x,x))) = f(x,x). [para(13(a,1),1857(a,1,1)),rewrite([42(4),42(6)])]. given #537 (A,wt=43): 241 f(x,f(f(x,x),f(f(f(f(f(f(x,x),f(y,x)),f(f(x,x),f(z,x))),f(f(x,x),f(z,x))),f(x,x)),f(f(x,x),u)))) = f(x,x). [para(180(a,1),14(a,1,2,1))]. given #538 (T,wt=31): 2174 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x). [para(42(a,1),129(a,1,2,2,1,1))]. given #539 (T,wt=31): 3038 f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),y))) = f(x,y). [para(42(a,1),138(a,1,2,2,1,1))]. given #540 (T,wt=31): 3146 f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),x),x)) = f(f(x,x),f(x,y)). [para(3135(a,1),56(a,1,2,2,1,1,1)),rewrite([2229(6),34(12),2680(16)])]. given #541 (T,wt=31): 3162 f(f(x,x),f(f(f(f(f(x,x),f(y,x)),f(f(x,x),f(y,x))),x),x)) = f(f(x,x),f(y,x)). [para(3136(a,1),56(a,1,2,2,1,1,1)),rewrite([2238(6),34(12),2740(16)])]. given #542 (A,wt=37): 242 f(f(x,x),f(x,f(f(f(f(f(x,f(y,f(x,x))),f(x,f(z,f(x,x)))),f(x,f(z,f(x,x)))),x),f(x,u)))) = x. [para(186(a,1),14(a,1,2,1)),rewrite([42(4),42(15),42(16),42(20)])]. given #543 (T,wt=31): 4132 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x)),x),f(x,z)))) = x. [para(4088(a,1),3(a,1,2,2,1,1,1)),rewrite([4088(10)])]. given #544 (T,wt=25): 7670 f(f(x,x),f(f(x,f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x)),x)) = x. [para(226(a,1),4132(a,1,2,2)),rewrite([57(21)])]. given #545 (T,wt=31): 4140 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x)),x),f(z,x)))) = x. [para(4088(a,1),68(a,1,2,2,1,1,1)),rewrite([4088(10)])]. given #546 (T,wt=31): 4170 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,f(f(f(x,x),x),f(x,y)))),x)),x),f(x,z)))) = x. [para(4159(a,1),3(a,1,2,2,1,1,1)),rewrite([4159(10)])]. given #547 (A,wt=53): 244 f(f(x,x),f(x,f(f(f(f(f(x,f(y,f(x,x))),f(f(f(x,x),x),f(f(f(x,x),x),f(z,x)))),f(f(f(x,x),x),f(f(f(x,x),x),f(z,x)))),x),f(x,u)))) = x. [para(160(a,1),14(a,1,2,1)),rewrite([42(4),42(23),42(24),42(28)])]. given #548 (T,wt=25): 7713 f(f(x,x),f(f(x,f(f(x,f(x,f(f(f(x,x),x),f(x,y)))),x)),x)) = x. [para(226(a,1),4170(a,1,2,2)),rewrite([57(21)])]. given #549 (T,wt=31): 4181 f(f(x,x),f(x,f(f(f(x,f(f(x,f(x,f(f(f(x,x),x),f(x,y)))),x)),x),f(z,x)))) = x. [para(4159(a,1),68(a,1,2,2,1,1,1)),rewrite([4159(10)])]. given #550 (T,wt=31): 4485 f(f(x,f(x,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(27(a,1),2436(a,1,1,1)),rewrite([27(11),27(11),27(13),27(13),27(24),27(24)])]. given #551 (T,wt=31): 4489 f(f(x,f(x,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(437(a,1),2436(a,1,1,1)),rewrite([437(11),437(11),437(13),437(13),437(24),437(24)])]. given #552 (A,wt=41): 245 f(x,f(f(x,x),f(f(f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(160(a,1),14(a,1,2,2,1,1,1)),rewrite([42(3),42(5),221(9),42(5),42(7)])]. given #553 (T,wt=31): 4502 f(f(f(x,x),x),f(x,f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,x)),f(f(x,x),z))))) = x. [para(257(a,1),2436(a,1,1,1)),rewrite([257(14),257(15),42(4),257(15),257(16),42(5),257(27),257(28),42(17)])]. given #554 (T,wt=31): 4506 f(f(f(x,x),x),f(x,f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,x)),f(z,f(x,x)))))) = x. [para(702(a,1),2436(a,1,1,1)),rewrite([702(14),702(15),42(4),702(15),702(16),42(5),702(27),702(28),42(17)])]. given #555 (T,wt=31): 4529 f(f(x,f(x,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(2702(a,1),2438(a,1,1,1)),rewrite([2702(10),2702(10),2702(12),2702(12),2702(23),2702(23)])]. given #556 (T,wt=31): 4530 f(f(x,f(x,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(2703(a,1),2438(a,1,1,1)),rewrite([2703(10),2703(10),2703(12),2703(12),2703(23),2703(23)])]. given #557 (A,wt=43): 246 f(f(x,y),f(f(f(y,y),f(f(f(y,x),f(y,x)),x)),f(f(f(f(f(y,x),f(y,x)),f(f(f(y,x),f(y,x)),x)),y),f(y,z)))) = y. [para(176(a,1),3(a,1,2,2,1,1,1))]. given #558 (T,wt=31): 4531 f(f(x,f(x,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(2758(a,1),2438(a,1,1,1)),rewrite([2758(10),2758(10),2758(12),2758(12),2758(23),2758(23)])]. given #559 (T,wt=31): 4532 f(f(x,f(x,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(2759(a,1),2438(a,1,1,1)),rewrite([2759(10),2759(10),2759(12),2759(12),2759(23),2759(23)])]. given #560 (T,wt=31): 4544 f(f(x,f(x,x)),f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(f(x,x),z)))) = f(x,x). [para(4525(a,1),3(a,1,2,2,1,1,1)),rewrite([42(5),42(16)])]. given #561 (T,wt=23): 7901 f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(f(x,x),z))) = x. [para(4544(a,1),130(a,1,2,2,1)),rewrite([177(39),22(35),42(13)]),flip(a)]. given #562 (A,wt=45): 248 f(f(x,y),f(f(f(x,y),f(x,y)),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)). [para(7(a,1),176(a,1,1)),rewrite([7(25),7(26),7(42),7(43)])]. given #563 (T,wt=23): 7904 f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(x,f(f(x,x),z))) = x. [para(57(a,1),7901(a,1,1,2,2,2,2))]. given #564 (T,wt=23): 7905 f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(z,f(x,x)))) = x. [para(57(a,1),7901(a,1,2,2))]. given #565 (T,wt=23): 7957 f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(x,f(z,f(x,x)))) = x. [para(57(a,1),7904(a,1,2,2))]. given #566 (T,wt=31): 4741 f(f(f(x,x),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(27(a,1),2502(a,1,1,1,1)),rewrite([27(11),27(12),27(13),27(13),27(24),27(24)])]. given #567 (A,wt=45): 249 f(f(x,y),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),u),z),z),f(x,y)),y)))) = f(f(x,y),f(x,y)). [para(9(a,1),176(a,1,1)),rewrite([9(16),9(17),9(33),9(34)])]. given #568 (T,wt=31): 4745 f(f(f(x,x),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(437(a,1),2502(a,1,1,1,1)),rewrite([437(11),437(12),437(13),437(13),437(24),437(24)])]. given #569 (T,wt=31): 4757 f(f(x,f(x,x)),f(x,f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,x)),f(f(x,x),z))))) = x. [para(257(a,1),2502(a,1,1,1,1)),rewrite([257(14),42(3),257(13),257(15),257(16),42(5),257(27),257(28),42(17)])]. given #570 (T,wt=31): 4761 f(f(x,f(x,x)),f(x,f(f(x,f(y,y)),f(f(f(y,f(y,y)),f(x,x)),f(z,f(x,x)))))) = x. [para(702(a,1),2502(a,1,1,1,1)),rewrite([702(14),42(3),702(13),702(15),702(16),42(5),702(27),702(28),42(17)])]. given #571 (T,wt=31): 4780 f(f(f(x,x),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(2702(a,1),2504(a,1,1,1,1)),rewrite([2702(10),2702(11),2702(12),2702(12),2702(23),2702(23)])]. given #572 (A,wt=43): 250 f(f(x,y),f(f(f(y,y),f(f(f(y,x),f(y,x)),y)),f(f(f(f(f(y,x),f(y,x)),f(f(f(y,x),f(y,x)),y)),y),f(y,z)))) = y. [para(179(a,1),3(a,1,2,2,1,1,1))]. given #573 (T,wt=31): 4781 f(f(f(x,x),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(2703(a,1),2504(a,1,1,1,1)),rewrite([2703(10),2703(11),2703(12),2703(12),2703(23),2703(23)])]. given #574 (T,wt=31): 4782 f(f(f(x,x),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(2758(a,1),2504(a,1,1,1,1)),rewrite([2758(10),2758(11),2758(12),2758(12),2758(23),2758(23)])]. given #575 (T,wt=31): 4783 f(f(f(x,x),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(2759(a,1),2504(a,1,1,1,1)),rewrite([2759(10),2759(11),2759(12),2759(12),2759(23),2759(23)])]. given #576 (T,wt=31): 5019 f(x,f(f(x,f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(x,f(x,f(f(x,x),z)))))) = f(x,x). [para(3639(a,1),2701(a,1,2,2,1,1))]. given #577 (A,wt=57): 251 f(f(f(f(f(x,x),x),f(y,x)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(x,x)),f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(f(x,x),x),z)))) = f(f(x,x),x). [para(216(a,1),3(a,1,2,2,1,1,1))]. given #578 (T,wt=31): 5020 f(x,f(f(x,f(x,f(y,f(x,x)))),f(f(x,f(x,x)),f(x,f(x,f(f(x,x),z)))))) = f(x,x). [para(3730(a,1),2701(a,1,2,2,1,1))]. given #579 (T,wt=31): 5199 f(x,f(f(x,f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(x,f(x,f(z,f(x,x))))))) = f(x,x). [para(3639(a,1),2757(a,1,2,2,1,1))]. given #580 (T,wt=31): 5200 f(x,f(f(x,f(x,f(y,f(x,x)))),f(f(x,f(x,x)),f(x,f(x,f(z,f(x,x))))))) = f(x,x). [para(3730(a,1),2757(a,1,2,2,1,1))]. given #581 (T,wt=31): 5274 f(f(f(x,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)) = x. [para(27(a,1),2766(a,1,1,1,1)),rewrite([27(11),27(12),27(12),27(23),27(23),27(25)])]. given #582 (A,wt=51): 253 f(f(f(f(f(x,x),x),f(y,x)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(x,x)),f(f(f(x,f(x,x)),f(f(x,x),x)),x))) = f(f(x,x),x). [para(216(a,1),9(a,1,2,2,1,1,1))]. Demod_limit hit 100 times. given #583 (T,wt=31): 5278 f(f(f(x,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)) = x. [para(437(a,1),2766(a,1,1,1,1)),rewrite([437(11),437(12),437(12),437(23),437(23),437(25)])]. given #584 (T,wt=31): 5293 f(f(x,f(x,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(257(a,1),2766(a,1,1,1,1)),rewrite([257(14),42(3),257(13),257(14),42(3),257(25),257(26),42(15),257(26)])]. given #585 (T,wt=31): 5297 f(f(x,f(x,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(702(a,1),2766(a,1,1,1,1)),rewrite([702(14),42(3),702(13),702(14),42(3),702(25),702(26),42(15),702(26)])]. given #586 (T,wt=31): 5308 f(f(f(x,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)) = x. [para(2696(a,1),2766(a,1,1,1,1)),rewrite([2696(13),2696(14),2696(14),2696(25),2696(25),2696(27)])]. given #587 (A,wt=57): 254 f(f(x,x),f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))))) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))). [para(156(a,1),13(a,1,1))]. given #588 (T,wt=31): 5309 f(f(f(x,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)) = x. [para(2700(a,1),2766(a,1,1,1,1)),rewrite([2700(13),2700(14),2700(14),2700(25),2700(25),2700(27)])]. given #589 (T,wt=31): 5310 f(f(f(x,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)) = x. [para(2752(a,1),2766(a,1,1,1,1)),rewrite([2752(13),2752(14),2752(14),2752(25),2752(25),2752(27)])]. given #590 (T,wt=31): 5311 f(f(f(x,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)) = x. [para(2756(a,1),2766(a,1,1,1,1)),rewrite([2756(13),2756(14),2756(14),2756(25),2756(25),2756(27)])]. given #591 (T,wt=31): 5352 f(x,f(f(x,x),f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(f(x,x),f(x,z))))) = f(x,x). [para(5321(a,1),901(a,1,2,2,2,1)),rewrite([5339(16)])]. given #592 (A,wt=45): 255 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,f(y,y)),f(f(y,f(y,y)),f(f(y,y),u)))))) = f(y,y). [para(156(a,1),9(a,1,1,2)),rewrite([156(11),156(12),42(5),156(12),156(16),156(29)])]. given #593 (T,wt=31): 5353 f(x,f(f(x,x),f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(f(x,x),f(z,x))))) = f(x,x). [para(5321(a,1),1054(a,1,2,2,2,1)),rewrite([5339(16)])]. given #594 (T,wt=31): 5354 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(f(x,x),y)))))))) = f(x,x). [para(5321(a,1),158(a,1,1,1)),rewrite([5321(8),42(3),5321(7),5321(8),42(3),5321(7),5321(9),5321(10),42(5),5321(9),5321(20)])]. given #595 (T,wt=31): 5376 f(x,f(f(x,x),f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(f(x,x),f(x,z))))) = f(x,x). [para(5322(a,1),901(a,1,2,2,2,1)),rewrite([5363(16)])]. given #596 (T,wt=31): 5377 f(x,f(f(x,x),f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(f(x,x),f(z,x))))) = f(x,x). [para(5322(a,1),1054(a,1,2,2,2,1)),rewrite([5363(16)])]. given #597 (A,wt=55): 256 f(f(x,f(f(y,z),f(y,z))),f(z,f(f(f(f(f(f(f(y,z),f(y,z)),x),f(z,z)),f(z,z)),f(f(y,z),f(y,z))),f(f(f(y,z),f(y,z)),u)))) = f(f(y,z),f(y,z)). [para(13(a,1),15(a,1,2,1))]. given #598 (T,wt=31): 5378 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(y,f(x,x))))))))) = f(x,x). [para(5322(a,1),158(a,1,1,1)),rewrite([5322(8),42(3),5322(7),5322(8),42(3),5322(7),5322(9),5322(10),42(5),5322(9),5322(20)])]. given #599 (T,wt=31): 5436 f(f(f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))),f(x,f(f(x,x),z))),x) = f(x,x). [para(5357(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(18),42(15)])]. given #600 (T,wt=31): 5437 f(f(f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(5357(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(18),42(15)])]. given #601 (T,wt=31): 5456 f(f(f(x,f(x,f(x,f(x,f(x,f(f(x,x),y)))))),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(5358(a,1),139(a,1,2,1,2,1)),rewrite([5358(25),678(17),5358(22),3413(15),42(15),22(13)])]. given #602 (A,wt=55): 259 f(f(x,f(f(y,z),f(y,z))),f(y,f(f(f(f(f(f(f(y,z),f(y,z)),x),f(y,y)),f(y,y)),f(f(y,z),f(y,z))),f(f(f(y,z),f(y,z)),u)))) = f(f(y,z),f(y,z)). [para(42(a,1),15(a,1,2,1))]. given #603 (T,wt=31): 5469 f(f(f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(5361(a,1),648(a,1,1,2,1)),rewrite([5461(19)])]. given #604 (T,wt=31): 5470 f(f(f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(5361(a,1),804(a,1,1,2,1)),rewrite([5461(19)])]. given #605 (T,wt=31): 5487 f(f(f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))),f(x,f(f(x,x),z))),x) = f(x,x). [para(5381(a,1),69(a,1,1,2,1,1,1)),rewrite([42(3),42(18),42(15)])]. given #606 (T,wt=31): 5488 f(f(f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(5381(a,1),563(a,1,1,2,1,1,1)),rewrite([42(3),42(18),42(15)])]. given #607 (A,wt=39): 260 f(f(x,f(y,y)),f(f(y,f(f(f(y,y),x),f(f(y,y),x))),f(f(f(f(y,y),x),f(y,y)),f(f(y,y),z)))) = f(y,y). [para(42(a,1),15(a,1,2,2,1,1))]. given #608 (T,wt=31): 5507 f(f(f(x,f(x,f(x,f(x,f(x,f(y,f(x,x))))))),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(5382(a,1),139(a,1,2,1,2,1)),rewrite([5382(25),678(17),5382(22),3413(15),42(15),22(13)])]. given #609 (T,wt=31): 5518 f(f(f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(5385(a,1),648(a,1,1,2,1)),rewrite([5510(19)])]. given #610 (T,wt=31): 5519 f(f(f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(5385(a,1),804(a,1,1,2,1)),rewrite([5510(19)])]. given #611 (T,wt=31): 5694 f(f(f(x,x),x),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))))))) = x. [para(5481(a,1),2438(a,1,1,1)),rewrite([5481(12),5481(13),42(4),5481(13),5481(14),42(5),5481(25),5481(26),42(17)])]. given #612 (A,wt=45): 262 f(f(x,f(y,y)),f(f(z,y),f(f(f(f(f(f(y,y),x),f(f(z,y),f(z,y))),f(f(z,y),f(z,y))),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(57(a,1),15(a,1,2,1))]. given #613 (T,wt=31): 5695 f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))))))) = x. [para(5481(a,1),2504(a,1,1,1,1)),rewrite([5481(12),42(3),5481(11),5481(13),5481(14),42(5),5481(25),5481(26),42(17)])]. given #614 (T,wt=31): 5698 f(f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))))))),x) = f(x,x). [para(5481(a,1),2769(a,1,1,1,1)),rewrite([5481(12),42(3),5481(11),5481(12),42(3),5481(23),5481(24),42(15),5481(24)])]. given #615 (T,wt=31): 5736 f(f(f(x,x),x),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))))))) = x. [para(5530(a,1),2438(a,1,1,1)),rewrite([5530(12),5530(13),42(4),5530(13),5530(14),42(5),5530(25),5530(26),42(17)])]. given #616 (T,wt=31): 5737 f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))))))) = x. [para(5530(a,1),2504(a,1,1,1,1)),rewrite([5530(12),42(3),5530(11),5530(13),5530(14),42(5),5530(25),5530(26),42(17)])]. given #617 (A,wt=43): 263 f(f(f(f(x,f(y,y)),f(x,f(y,y))),f(y,y)),f(f(y,z),f(f(f(f(f(x,f(y,y)),z),z),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(57(a,1),15(a,1,2,2,1,1,1,1))]. given #618 (T,wt=31): 5740 f(f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))))))),x) = f(x,x). [para(5530(a,1),2769(a,1,1,1,1)),rewrite([5530(12),42(3),5530(11),5530(12),42(3),5530(23),5530(24),42(15),5530(24)])]. given #619 (T,wt=31): 5752 f(f(x,x),f(x,f(f(f(x,x),x),f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z)))))) = x. [para(435(a,1),3440(a,1,1,1)),rewrite([435(10),435(11),435(11),435(11),435(12),435(24)])]. given #620 (T,wt=31): 5753 f(f(x,x),f(x,f(f(f(x,x),x),f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x)))))) = x. [para(528(a,1),3440(a,1,1,1)),rewrite([528(10),528(11),528(11),528(11),528(12),528(24)])]. given #621 (T,wt=31): 5779 f(f(x,x),f(x,f(f(f(x,x),x),f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(x,z)))))) = x. [para(2702(a,1),3440(a,1,1,1)),rewrite([2702(10),2702(11),2702(11),2702(11),2702(12),2702(24)])]. given #622 (A,wt=33): 264 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(u,f(y,y))))) = f(y,y). [para(57(a,1),15(a,1,2,2,2))]. given #623 (T,wt=31): 5780 f(f(x,x),f(x,f(f(f(x,x),x),f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(z,x)))))) = x. [para(2703(a,1),3440(a,1,1,1)),rewrite([2703(10),2703(11),2703(11),2703(11),2703(12),2703(24)])]. given #624 (T,wt=31): 5781 f(f(x,x),f(x,f(f(f(x,x),x),f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,z)))))) = x. [para(2758(a,1),3440(a,1,1,1)),rewrite([2758(10),2758(11),2758(11),2758(11),2758(12),2758(24)])]. given #625 (T,wt=31): 5782 f(f(x,x),f(x,f(f(f(x,x),x),f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(z,x)))))) = x. [para(2759(a,1),3440(a,1,1,1)),rewrite([2759(10),2759(11),2759(11),2759(11),2759(12),2759(24)])]. given #626 (T,wt=31): 6047 f(f(x,f(y,y)),f(f(f(f(f(y,y),x),f(y,f(y,y))),f(y,f(y,y))),f(y,y))) = f(y,y). [para(13(a,1),5967(a,1,2,1,1,2,1)),rewrite([42(10)])]. given #627 (A,wt=45): 265 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),f(f(y,z),f(y,z))),f(f(y,z),f(y,z))),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(63(a,1),15(a,1,2,1))]. given #628 (T,wt=31): 6113 f(f(x,x),f(f(f(f(x,f(x,f(x,f(f(x,x),y)))),f(f(x,x),x)),f(f(x,x),x)),x)) = x. [para(2679(a,1),5967(a,1,1))]. given #629 (T,wt=31): 6114 f(f(x,x),f(f(f(f(x,f(x,f(x,f(y,f(x,x))))),f(f(x,x),x)),f(f(x,x),x)),x)) = x. [para(2685(a,1),5967(a,1,1))]. given #630 (T,wt=31): 6117 f(f(f(x,x),x),f(f(f(f(x,f(x,f(f(x,x),x))),f(f(x,x),x)),f(f(x,x),x)),x)) = x. [para(2828(a,1),5967(a,1,1))]. given #631 (T,wt=27): 8865 f(f(f(f(x,f(x,f(f(x,x),x))),f(f(x,x),x)),f(f(x,x),x)),x) = f(x,x). [para(6117(a,1),129(a,1,2,2,1)),rewrite([13(39),34(14)]),flip(a)]. given #632 (A,wt=43): 266 f(f(f(f(f(x,x),y),f(f(x,x),y)),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),u)))) = f(x,x). [para(63(a,1),15(a,1,2,2,1,1,1,1))]. given #633 (T,wt=29): 8868 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),x))),f(f(x,x),x)),f(f(x,x),x)))) = x. [para(8865(a,1),179(a,1,1)),rewrite([8865(12),8865(13),42(4),8865(24),8865(25),42(16)])]. given #634 (T,wt=31): 6187 f(f(x,f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,f(x,x))),f(x,f(x,x))))) = f(x,x). [para(6112(a,1),2438(a,1,1,1)),rewrite([6112(10),6112(10),6112(12),6112(12),6112(23),6112(23)])]. given #635 (T,wt=31): 6188 f(f(f(x,x),x),f(f(x,x),f(f(f(f(x,x),x),f(x,f(x,x))),f(x,f(x,x))))) = f(x,x). [para(6112(a,1),2504(a,1,1,1,1)),rewrite([6112(10),6112(11),6112(12),6112(12),6112(23),6112(23)])]. given #636 (T,wt=31): 6191 f(f(f(x,x),f(f(x,x),f(f(f(f(x,x),x),f(x,f(x,x))),f(x,f(x,x))))),f(x,x)) = x. [para(6112(a,1),2769(a,1,1,1,1)),rewrite([6112(10),6112(11),6112(11),6112(22),6112(22),6112(24)])]. given #637 (A,wt=51): 267 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,u),f(f(f(f(f(f(y,y),w),u),u),f(y,y)),f(f(y,y),v5)))))) = f(y,y). [para(15(a,1),9(a,1,1,2)),rewrite([15(16),15(17),42(5),15(17),15(21),15(37)])]. given #638 (T,wt=31): 6193 f(f(x,x),f(x,f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,f(x,x))),f(x,f(x,x)))))) = x. [para(6112(a,1),3440(a,1,1,1)),rewrite([6112(10),6112(11),6112(11),6112(11),6112(12),6112(24)])]. given #639 (T,wt=31): 6271 f(f(x,f(x,x)),f(f(x,x),f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,f(x,x))))) = f(x,x). [para(6231(a,1),2438(a,1,1,1)),rewrite([6231(10),6231(10),6231(12),6231(12),6231(23),6231(23)])]. given #640 (T,wt=31): 6272 f(f(f(x,x),x),f(f(x,x),f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,f(x,x))))) = f(x,x). [para(6231(a,1),2504(a,1,1,1,1)),rewrite([6231(10),6231(11),6231(12),6231(12),6231(23),6231(23)])]. given #641 (T,wt=31): 6275 f(f(f(x,x),f(f(x,x),f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,f(x,x))))),f(x,x)) = x. [para(6231(a,1),2769(a,1,1,1,1)),rewrite([6231(10),6231(11),6231(11),6231(22),6231(22),6231(24)])]. given #642 (A,wt=45): 268 f(f(x,f(y,y)),f(f(y,y),f(f(f(f(f(f(y,y),x),f(f(y,y),f(y,z))),f(f(y,y),f(y,z))),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(167(a,1),15(a,1,2,1))]. given #643 (T,wt=31): 6277 f(f(x,x),f(x,f(f(f(x,x),x),f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,f(x,x)))))) = x. [para(6231(a,1),3440(a,1,1,1)),rewrite([6231(10),6231(11),6231(11),6231(11),6231(12),6231(24)])]. given #644 (T,wt=31): 6381 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(f(x,x),y))))))),x) = f(x,x). [para(5321(a,1),215(a,1,1,1,1,1)),rewrite([5321(8),42(3),5321(7),5321(9),5321(10),42(5),5321(9),5321(19),5321(20),42(15),5321(20)])]. given #645 (T,wt=31): 6382 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(y,f(x,x)))))))),x) = f(x,x). [para(5322(a,1),215(a,1,1,1,1,1)),rewrite([5322(8),42(3),5322(7),5322(9),5322(10),42(5),5322(9),5322(19),5322(20),42(15),5322(20)])]. given #646 (T,wt=31): 6406 f(f(f(x,x),x),f(x,f(x,f(x,f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)))))) = x. [para(6171(a,1),2438(a,1,1,1)),rewrite([6171(12),6171(13),42(4),6171(13),6171(14),42(5),6171(25),6171(26),42(17)])]. given #647 (A,wt=45): 269 f(f(x,f(y,y)),f(f(y,y),f(f(f(f(f(f(y,y),x),f(f(y,y),f(z,y))),f(f(y,y),f(z,y))),f(y,y)),f(f(y,y),u)))) = f(y,y). [para(180(a,1),15(a,1,2,1))]. given #648 (T,wt=31): 6407 f(f(x,f(x,x)),f(x,f(x,f(x,f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)))))) = x. [para(6171(a,1),2504(a,1,1,1,1)),rewrite([6171(12),42(3),6171(11),6171(13),6171(14),42(5),6171(25),6171(26),42(17)])]. given #649 (T,wt=31): 6410 f(f(x,f(x,f(x,f(x,f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)))))),x) = f(x,x). [para(6171(a,1),2769(a,1,1,1,1)),rewrite([6171(12),42(3),6171(11),6171(12),42(3),6171(23),6171(24),42(15),6171(24)])]. given #650 (T,wt=31): 6445 f(f(f(x,x),x),f(x,f(x,f(x,f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)))))) = x. [para(6254(a,1),2438(a,1,1,1)),rewrite([6254(12),6254(13),42(4),6254(13),6254(14),42(5),6254(25),6254(26),42(17)])]. given #651 (T,wt=31): 6446 f(f(x,f(x,x)),f(x,f(x,f(x,f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)))))) = x. [para(6254(a,1),2504(a,1,1,1,1)),rewrite([6254(12),42(3),6254(11),6254(13),6254(14),42(5),6254(25),6254(26),42(17)])]. given #652 (A,wt=57): 285 f(f(f(f(x,f(x,x)),f(f(x,x),y)),f(x,f(x,x))),f(f(f(f(x,f(x,x)),f(x,f(x,x))),x),f(f(f(f(x,x),x),f(x,f(x,x))),f(f(x,f(x,x)),z)))) = f(x,f(x,x)). [para(213(a,1),3(a,1,2,2,1,1,1))]. given #653 (T,wt=31): 6449 f(f(x,f(x,f(x,f(x,f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)))))),x) = f(x,x). [para(6254(a,1),2769(a,1,1,1,1)),rewrite([6254(12),42(3),6254(11),6254(12),42(3),6254(23),6254(24),42(15),6254(24)])]. given #654 (T,wt=31): 6888 f(f(x,x),f(f(f(f(x,f(y,f(x,x))),f(x,f(f(x,x),z))),f(x,f(f(x,x),z))),x)) = x. [para(22(a,1),6870(a,1,1))]. given #655 (T,wt=31): 6890 f(f(x,x),f(f(f(f(x,f(f(x,x),y)),f(x,f(f(x,x),z))),f(x,f(f(x,x),z))),x)) = x. [para(34(a,1),6870(a,1,1))]. given #656 (T,wt=31): 6976 f(f(x,x),f(f(f(f(x,f(y,f(x,x))),f(x,f(z,f(x,x)))),f(x,f(z,f(x,x)))),x)) = x. [para(22(a,1),6881(a,1,1))]. given #657 (A,wt=53): 286 f(f(f(f(x,f(x,x)),f(f(x,x),y)),f(x,f(x,x))),f(f(f(f(x,f(x,x)),f(x,f(x,x))),x),f(f(f(f(x,x),x),f(x,f(x,x))),f(x,x)))) = f(x,f(x,x)). [para(213(a,1),9(a,1,2,2,1,1,1))]. given #658 (T,wt=31): 6978 f(f(x,x),f(f(f(f(x,f(f(x,x),y)),f(x,f(z,f(x,x)))),f(x,f(z,f(x,x)))),x)) = x. [para(34(a,1),6881(a,1,1))]. given #659 (T,wt=31): 7099 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(x,f(x,f(f(x,x),z))))),x) = f(x,x). [para(3639(a,1),4950(a,1,1,2,1,1))]. given #660 (T,wt=31): 7100 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,f(x,x)),f(x,f(x,f(f(x,x),z))))),x) = f(x,x). [para(3730(a,1),4950(a,1,1,2,1,1))]. given #661 (T,wt=31): 7112 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(x,f(x,f(z,f(x,x)))))),x) = f(x,x). [para(3639(a,1),5132(a,1,1,2,1,1))]. given #662 (A,wt=57): 287 f(f(x,x),f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))))) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))). [para(221(a,1),13(a,1,1))]. given #663 (T,wt=31): 7113 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,f(x,x)),f(x,f(x,f(z,f(x,x)))))),x) = f(x,x). [para(3730(a,1),5132(a,1,1,2,1,1))]. given #664 (T,wt=31): 7118 f(f(x,x),f(x,f(x,f(x,f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(f(x,x),z))))))) = x. [para(5294(a,1),179(a,1,1)),rewrite([5294(13),5294(14),42(4),5294(26),5294(27),42(17)])]. given #665 (T,wt=31): 7154 f(f(x,x),f(x,f(x,f(x,f(f(x,y),f(f(f(f(y,y),y),f(x,x)),f(z,f(x,x)))))))) = x. [para(5298(a,1),179(a,1,1)),rewrite([5298(13),5298(14),42(4),5298(26),5298(27),42(17)])]. given #666 (T,wt=31): 7177 f(f(x,x),f(x,f(x,f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,f(f(x,x),z))))))) = x. [para(5325(a,1),179(a,1,1)),rewrite([5325(13),5325(14),42(4),5325(26),5325(27),42(17)])]. given #667 (A,wt=45): 288 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,f(y,y)),f(f(y,f(y,y)),f(u,f(y,y))))))) = f(y,y). [para(221(a,1),9(a,1,1,2)),rewrite([221(11),221(12),42(5),221(12),221(16),221(29)])]. given #668 (T,wt=31): 7200 f(f(x,x),f(x,f(x,f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,f(z,f(x,x)))))))) = x. [para(5326(a,1),179(a,1,1)),rewrite([5326(13),5326(14),42(4),5326(26),5326(27),42(17)])]. given #669 (T,wt=31): 7221 f(f(x,x),f(x,f(x,f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,f(f(x,x),z))))))) = x. [para(5327(a,1),179(a,1,1)),rewrite([5327(13),5327(14),42(4),5327(26),5327(27),42(17)])]. given #670 (T,wt=31): 7248 f(f(x,x),f(x,f(x,f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,f(z,f(x,x)))))))) = x. [para(5328(a,1),179(a,1,1)),rewrite([5328(13),5328(14),42(4),5328(26),5328(27),42(17)])]. given #671 (T,wt=31): 7297 f(f(x,x),f(f(x,f(x,f(f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x),f(x,z)))),x)) = x. [para(3399(a,1),5386(a,1,2,1,2,1)),rewrite([3399(8)])]. given #672 (A,wt=55): 289 f(f(f(f(x,y),f(x,y)),f(z,f(x,y))),f(f(f(f(z,f(x,y)),f(z,f(x,y))),f(y,y)),f(f(f(y,f(y,y)),f(z,f(x,y))),f(f(z,f(x,y)),u)))) = f(z,f(x,y)). [para(13(a,1),17(a,1,2,2,1,1,1))]. given #673 (T,wt=31): 7299 f(f(x,x),f(f(x,f(x,f(f(f(x,f(x,f(f(f(x,x),x),f(x,y)))),x),f(x,z)))),x)) = x. [para(3444(a,1),5386(a,1,2,1,2,1)),rewrite([3444(8)])]. given #674 (T,wt=31): 7300 f(f(x,x),f(f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(f(f(x,x),x),f(x,z)))),x)) = x. [para(3639(a,1),5386(a,1,2,1,2,2,1,1)),rewrite([42(6)])]. given #675 (T,wt=31): 7301 f(f(x,x),f(f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(f(f(x,x),x),f(x,z)))),x)) = x. [para(3730(a,1),5386(a,1,2,1,2,2,1,1)),rewrite([42(6)])]. given #676 (T,wt=31): 7447 f(f(x,x),f(f(x,f(x,f(f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x),f(z,x)))),x)) = x. [para(3399(a,1),6879(a,1,2,1,2,1)),rewrite([3399(8)])]. given #677 (A,wt=45): 290 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),x),f(f(f(x,x),f(y,f(x,x))),f(f(y,f(x,x)),z)))) = f(y,f(x,x)). [para(34(a,1),17(a,1,2,2,1,1)),rewrite([42(3)])]. given #678 (T,wt=11): 9276 f(f(x,x),x) = f(x,f(x,x)). [para(2218(a,1),290(a,1,2,2,2)),rewrite([3413(3),34(12),13(9)])]. given #679 (T,wt=11): 9409 f(f(x,x),f(x,f(x,x))) = x. [back_rewrite(8980),rewrite([9276(3),9276(13),9278(14),9276(5),63(7)])]. given #680 (T,wt=17): 9406 f(f(x,x),f(x,f(f(x,f(x,x)),f(y,x)))) = x. [back_rewrite(8987),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #681 (T,wt=17): 9408 f(f(x,x),f(x,f(f(x,f(x,x)),f(x,y)))) = x. [back_rewrite(8984),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #682 (A,wt=55): 292 f(f(f(f(x,y),f(x,y)),f(z,f(x,y))),f(f(f(f(z,f(x,y)),f(z,f(x,y))),f(x,x)),f(f(f(x,f(x,x)),f(z,f(x,y))),f(f(z,f(x,y)),u)))) = f(z,f(x,y)). [para(42(a,1),17(a,1,2,2,1,1,1))]. given #683 (T,wt=19): 10340 f(f(f(x,f(x,x)),f(x,f(x,x))),x) = f(x,f(x,x)). [back_rewrite(6360),rewrite([9276(2),9276(4),9276(7),9276(9),9276(11),9276(14),9276(15),9288(17),22(8),9276(8),9409(9),9276(8)])]. given #684 (T,wt=21): 9278 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = x. [para(2679(a,1),290(a,1,1,2)),rewrite([42(3),42(6),2680(8),42(6),2680(8),9276(3),42(9),2680(11),9276(5),42(10),2680(12),42(14),2680(16)])]. given #685 (T,wt=21): 9397 f(f(x,x),f(f(x,f(x,f(f(x,f(x,x)),f(y,x)))),x)) = x. [back_rewrite(8997),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #686 (T,wt=21): 9398 f(f(x,x),f(f(x,f(x,f(f(x,f(x,x)),f(x,y)))),x)) = x. [back_rewrite(8996),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #687 (A,wt=35): 293 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x). [para(42(a,1),17(a,1,2,2,1,1))]. given #688 (T,wt=21): 11252 f(f(f(f(x,x),f(y,x)),f(x,f(x,x))),x) = f(x,f(x,x)). [back_rewrite(3136),rewrite([9276(5),9276(9)])]. given #689 (T,wt=21): 11253 f(f(f(f(x,x),f(x,y)),f(x,f(x,x))),x) = f(x,f(x,x)). [back_rewrite(3135),rewrite([9276(5),9276(9)])]. given #690 (T,wt=21): 11297 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = x. [back_rewrite(2859),rewrite([9276(2),3413(3),9276(3),3413(4),42(3),9276(3),9276(5)])]. given #691 (T,wt=21): 11300 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(x,x)) = x. [back_rewrite(2853),rewrite([9276(3),3413(4),9276(4),3413(5),42(4),9276(2),9276(4)])]. given #692 (A,wt=33): 294 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)),y))) = f(y,x). [para(42(a,1),17(a,1,2,2,2))]. given #693 (T,wt=21): 11301 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x)) = x. [back_rewrite(2852),rewrite([9276(3),3413(4),9276(4),3413(5),42(4),9276(2),9276(4)])]. given #694 (T,wt=23): 10382 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)). [back_rewrite(6278),rewrite([9276(10),3413(11),10340(6),9276(10)]),flip(a)]. given #695 (T,wt=23): 10499 f(f(x,y),f(f(f(f(y,x),f(y,f(y,y))),f(y,f(y,y))),y)) = y. [back_rewrite(5967),rewrite([9276(4),9276(7)])]. given #696 (T,wt=23): 11590 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [back_rewrite(528),rewrite([9276(4)])]. given #697 (A,wt=49): 295 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(f(z,x),f(z,x))),f(f(f(f(z,x),f(f(z,x),f(z,x))),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(57(a,1),17(a,1,2,2,1,1,1))]. given #698 (T,wt=23): 11605 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [back_rewrite(435),rewrite([9276(4)])]. given #699 (T,wt=25): 9400 f(f(x,x),f(x,f(f(x,f(x,x)),f(f(x,x),f(f(x,x),f(y,x)))))) = x. [back_rewrite(8994),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #700 (T,wt=25): 9401 f(f(x,x),f(x,f(f(x,f(x,x)),f(f(x,x),f(f(x,x),f(x,y)))))) = x. [back_rewrite(8993),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #701 (T,wt=25): 9410 f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(x,f(x,x)))))) = f(x,f(x,x)). [back_rewrite(8971),rewrite([9276(9),9278(10),9276(2),3413(3),9276(3),9276(5),9276(11)])]. given #702 (A,wt=37): 296 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(u,f(y,x))))) = f(y,x). [para(57(a,1),17(a,1,2,2,2))]. given #703 (T,wt=25): 9411 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)). [back_rewrite(8970),rewrite([9276(9),9278(10),9276(2),3413(3),9276(3),9276(5),9276(11)])]. given #704 (T,wt=25): 9786 f(f(x,x),f(f(x,f(f(x,f(x,f(f(x,f(x,x)),f(x,y)))),x)),x)) = x. [back_rewrite(7713),rewrite([9276(3)])]. given #705 (T,wt=25): 9826 f(f(x,x),f(f(x,f(f(x,f(x,f(f(x,f(x,x)),f(y,x)))),x)),x)) = x. [back_rewrite(7670),rewrite([9276(3)])]. given #706 (T,wt=25): 10329 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(6434),rewrite([9276(2),9276(4),9276(7),9276(8),221(9),9409(4)])]. given #707 (A,wt=49): 297 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(f(x,z),f(x,z))),f(f(f(f(x,z),f(f(x,z),f(x,z))),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(63(a,1),17(a,1,2,2,1,1,1))]. given #708 (T,wt=25): 10331 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(6432),rewrite([9276(2),9276(4),9276(7),9276(8),221(9),9409(4)])]. given #709 (T,wt=25): 11425 f(f(x,x),f(f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))),x)) = x. [back_rewrite(1857),rewrite([9276(3),9276(5)])]. given #710 (T,wt=25): 11432 f(f(x,x),f(f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))),x)) = x. [back_rewrite(1847),rewrite([9276(3),9276(5)])]. given #711 (T,wt=25): 11581 f(f(f(x,y),f(f(f(y,f(y,y)),f(x,x)),f(z,f(x,x)))),x) = f(x,x). [back_rewrite(543),rewrite([9276(3)])]. given #712 (A,wt=55): 298 f(f(f(x,x),f(y,x)),f(f(y,x),f(f(f(f(x,f(f(y,x),f(f(f(y,x),f(y,x)),z))),f(f(y,x),f(f(f(y,x),f(y,x)),z))),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(167(a,1),17(a,1,2,1)),rewrite([42(10),42(11),42(18)])]. given #713 (T,wt=25): 11593 f(f(f(x,y),f(f(f(y,f(y,y)),f(x,x)),f(f(x,x),z))),x) = f(x,x). [back_rewrite(523),rewrite([9276(3)])]. given #714 (T,wt=25): 11603 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(x,f(x,x)),y),f(z,y)))) = y. [back_rewrite(437),rewrite([9276(6)])]. given #715 (T,wt=25): 11623 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(x,f(x,x)),y),f(y,z)))) = y. [back_rewrite(27),rewrite([9276(6)])]. given #716 (T,wt=25): 11658 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(y,x),y),y),y),f(y,z)))) = y. [para(9276(a,1),3(a,1,2,1))]. given #717 (A,wt=49): 299 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(f(x,x),f(x,z))),f(f(f(f(x,x),f(f(x,x),f(x,z))),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(167(a,1),17(a,1,2,2,1,1,1))]. given #718 (T,wt=25): 11674 f(f(x,y),f(f(y,f(y,y)),f(f(f(f(f(y,x),y),y),y),f(z,y)))) = y. [para(9276(a,1),68(a,1,2,1))]. given #719 (T,wt=25): 11676 f(f(f(x,f(x,x)),f(f(f(f(f(x,y),x),x),x),f(x,z))),f(x,x)) = x. [para(9276(a,1),69(a,1,1,1))]. given #720 (T,wt=25): 11684 f(f(f(x,f(x,x)),f(f(f(f(f(x,y),x),x),x),f(z,x))),f(x,x)) = x. [para(9276(a,1),563(a,1,1,1))]. given #721 (T,wt=25): 11685 f(f(f(x,f(x,x)),f(f(f(f(f(y,x),x),x),x),f(x,z))),f(x,x)) = x. [para(9276(a,1),651(a,1,1,1))]. given #722 (A,wt=57): 300 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),f(x,f(f(x,x),z))),f(f(f(x,f(x,f(f(x,x),z))),f(y,f(x,x))),f(f(y,f(x,x)),u)))) = f(y,f(x,x)). [para(177(a,1),17(a,1,2,2,1,1,1)),rewrite([42(3)])]. given #723 (T,wt=25): 11687 f(f(f(x,f(x,x)),f(f(f(f(f(y,x),x),x),x),f(z,x))),f(x,x)) = x. [para(9276(a,1),806(a,1,1,1))]. given #724 (T,wt=27): 9281 f(f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(x,z))),f(x,x)) = x. [para(3683(a,1),290(a,2)),rewrite([42(5),42(9),9276(7),42(10),42(18),42(22),9276(20),42(23),42(30),42(34),9276(32),42(35),42(45),42(49),9276(47),42(50),42(58),42(62),9276(60),42(63),290(69),42(15)])]. given #725 (T,wt=27): 9282 f(f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(z,x))),f(x,x)) = x. [para(3689(a,1),290(a,2)),rewrite([42(5),42(9),9276(7),42(10),42(18),42(22),9276(20),42(23),42(30),42(34),9276(32),42(35),42(45),42(49),9276(47),42(50),42(58),42(62),9276(60),42(63),290(69),42(15)])]. given #726 (T,wt=27): 9283 f(f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,f(x,x)),f(x,z))),f(x,x)) = x. [para(3757(a,1),290(a,2)),rewrite([42(5),42(9),9276(7),42(10),42(18),42(22),9276(20),42(23),42(30),42(34),9276(32),42(35),42(45),42(49),9276(47),42(50),42(58),42(62),9276(60),42(63),290(69),42(15)])]. given #727 (A,wt=55): 301 f(f(f(x,x),f(y,x)),f(f(y,x),f(f(f(f(x,f(f(y,x),f(z,f(f(y,x),f(y,x))))),f(f(y,x),f(z,f(f(y,x),f(y,x))))),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(180(a,1),17(a,1,2,1)),rewrite([42(10),42(11),42(18)])]. given #728 (T,wt=27): 9284 f(f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,f(x,x)),f(z,x))),f(x,x)) = x. [para(3763(a,1),290(a,2)),rewrite([42(5),42(9),9276(7),42(10),42(18),42(22),9276(20),42(23),42(30),42(34),9276(32),42(35),42(45),42(49),9276(47),42(50),42(58),42(62),9276(60),42(63),290(69),42(15)])]. given #729 (T,wt=27): 9404 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,f(x,x)),f(x,y)))),x),f(z,x)))) = x. [back_rewrite(8990),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #730 (T,wt=27): 9405 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,f(x,x)),f(y,x)))),x),f(x,z)))) = x. [back_rewrite(8989),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #731 (T,wt=27): 9407 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,f(x,x)),f(x,y)))),x),f(x,z)))) = x. [back_rewrite(8985),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3)])]. given #732 (A,wt=49): 302 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(f(x,x),f(z,x))),f(f(f(f(x,x),f(f(x,x),f(z,x))),f(y,x)),f(f(y,x),u)))) = f(y,x). [para(180(a,1),17(a,1,2,2,1,1,1))]. given #733 (T,wt=27): 10458 f(f(x,x),f(f(f(f(x,f(f(x,x),y)),f(x,f(x,x))),f(x,f(x,x))),x)) = x. [back_rewrite(6051),rewrite([9276(6),9276(9)])]. given #734 (T,wt=27): 10460 f(f(x,x),f(f(f(f(x,f(y,f(x,x))),f(x,f(x,x))),f(x,f(x,x))),x)) = x. [back_rewrite(6048),rewrite([9276(6),9276(9)])]. given #735 (T,wt=27): 11056 f(f(x,x),f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,f(x,x)),f(z,x)))) = x. [back_rewrite(3834),rewrite([9276(8)])]. given #736 (T,wt=27): 11058 f(f(x,x),f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,f(x,x)),f(x,z)))) = x. [back_rewrite(3831),rewrite([9276(8)])]. given #737 (A,wt=57): 303 f(f(x,f(y,f(x,x))),f(f(f(f(y,f(x,x)),f(y,f(x,x))),f(x,f(z,f(x,x)))),f(f(f(x,f(x,f(z,f(x,x)))),f(y,f(x,x))),f(f(y,f(x,x)),u)))) = f(y,f(x,x)). [para(186(a,1),17(a,1,2,2,1,1,1)),rewrite([42(3)])]. given #738 (T,wt=27): 11065 f(f(x,x),f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(z,x)))) = x. [back_rewrite(3815),rewrite([9276(8)])]. given #739 (T,wt=27): 11067 f(f(x,x),f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(x,z)))) = x. [back_rewrite(3806),rewrite([9276(8)])]. given #740 (T,wt=27): 11203 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,f(x,x)),f(y,x)))),x),f(z,x)))) = x. [back_rewrite(3412),rewrite([9276(3)])]. given #741 (T,wt=27): 11541 f(f(x,x),f(x,f(f(x,y),f(f(f(y,f(y,y)),f(x,x)),f(z,f(x,x)))))) = x. [back_rewrite(754),rewrite([9276(4)])]. given #742 (A,wt=35): 331 f(f(x,x),f(f(y,f(x,x)),f(f(f(f(y,f(x,x)),f(f(y,f(x,x)),f(y,f(x,x)))),x),f(x,z)))) = x. [para(22(a,1),18(a,1,1)),rewrite([57(8)])]. given #743 (T,wt=27): 11549 f(f(x,x),f(x,f(f(x,y),f(f(f(y,f(y,y)),f(x,x)),f(f(x,x),z))))) = x. [back_rewrite(741),rewrite([9276(4)])]. given #744 (T,wt=27): 11576 f(x,f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x))))) = f(x,x). [back_rewrite(551),rewrite([9276(5)])]. given #745 (T,wt=27): 11599 f(x,f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))))) = f(x,x). [back_rewrite(443),rewrite([9276(5)])]. given #746 (T,wt=27): 11775 f(f(f(f(x,x),f(y,f(y,y))),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [para(10340(a,1),96(a,1,1,1,2,2,2)),rewrite([42(12),22(21),42(10),42(20),10340(32),22(29),42(18),9276(12),10382(12)])]. given #747 (A,wt=35): 332 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,x),y),f(f(f(x,x),y),f(f(x,x),y))),x),f(x,z)))) = x. [para(34(a,1),18(a,1,1)),rewrite([63(8)])]. given #748 (T,wt=27): 11857 f(f(f(f(x,x),f(y,f(y,y))),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [para(10382(a,1),11590(a,1,1,2,1,1))]. given #749 (T,wt=29): 9285 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),f(f(x,x),f(x,y))))),f(x,x)) = x. [para(4210(a,1),290(a,2)),rewrite([42(4),9276(2),42(6),9276(4),42(9),42(18),9276(16),42(20),9276(18),42(23),42(31),9276(29),42(33),9276(31),42(36),42(47),9276(45),42(49),9276(47),42(52),42(61),9276(59),42(63),9276(61),42(66),290(74),42(16)])]. given #750 (T,wt=29): 9286 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),f(f(x,x),f(y,x))))),f(x,x)) = x. [para(4231(a,1),290(a,2)),rewrite([42(4),9276(2),42(6),9276(4),42(9),42(18),9276(16),42(20),9276(18),42(23),42(31),9276(29),42(33),9276(31),42(36),42(47),9276(45),42(49),9276(47),42(52),42(61),9276(59),42(63),9276(61),42(66),290(74),42(16)])]. given #751 (T,wt=29): 9399 f(f(x,x),f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))))) = x. [back_rewrite(8995),rewrite([9276(3),9276(11),3413(12),63(7),3413(4),9276(3),9