============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4529 was started by mccune on cleo.thornwood, Wed Nov 22 12:20:45 2006 The command was "/home/mccune/bin/prover9 -f MOL-base.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MOL-base.in assign(max_weight,60). assign(new_constants,1). set(lex_order_vars). set(restrict_denials). assign(max_hours,4). % assign(max_hours, 4) -> assign(max_seconds, 14400). 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(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(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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 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 (F,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 #3 (F,wt=41): 10 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y. [para(3(a,1),9(a,1,1,2)),rewrite(3(12),3(12),3(14),3(17),3(30))]. given #4 (T,wt=13): 14 f(f(x,y),f(f(f(y,y),z),y)) = y. [para(3(a,1),10(a,1,2,2))]. given #5 (T,wt=9): 22 f(f(x,y),f(y,y)) = y. [para(3(a,1),14(a,1,2,1))]. given #6 (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,v)))) = y. [para(3(a,1),3(a,1,2,1))]. given #7 (F,wt=11): 48 f(f(x,f(y,y)),y) = f(y,y). [para(22(a,1),9(a,1,2,2,1)),rewrite(22(5),22(5))]. given #8 (F,wt=11): 57 f(f(f(x,x),y),x) = f(x,x). [para(14(a,1),22(a,1,1)),rewrite(14(7)),flip(a)]. given #9 (T,wt=9): 82 f(f(x,y),f(x,x)) = x. [para(22(a,1),57(a,1,1,1)),rewrite(22(6))]. given #10 (T,wt=13): 88 f(x,f(f(y,x),f(y,x))) = f(y,x). [para(3(a,1),82(a,1,1))]. given #11 (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)),v),f(f(f(f(x,v),v),f(z,x)),f(f(z,x),w)))) = f(z,x). [para(3(a,1),3(a,1,2,2,1,1,1,1))]. given #12 (F,wt=13): 97 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(82(a,1),82(a,1,1))]. given #13 (F,wt=15): 59 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y. [back_rewrite(39),rewrite(48(7))]. given #14 (T,wt=15): 144 f(f(x,y),f(y,f(f(y,y),f(z,y)))) = y. [para(88(a,1),59(a,1,2,2,2))]. given #15 (T,wt=17): 117 f(x,f(f(x,x),f(x,f(f(x,x),y)))) = f(x,x). [para(22(a,1),7(a,1,2,2,1)),rewrite(103(11),82(3))]. given #16 (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,v)))) = y. [para(3(a,1),3(a,1,2,2,1,1,1))]. given #17 (F,wt=17): 160 f(x,f(f(x,x),f(x,f(y,f(x,x))))) = f(x,x). [para(22(a,1),144(a,1,1)),rewrite(82(4))]. given #18 (F,wt=21): 42 f(f(x,f(y,y)),f(f(y,y),f(y,f(f(y,y),z)))) = f(y,y). [para(22(a,1),3(a,1,2,2,1)),rewrite(22(5))]. given #19 (T,wt=21): 74 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x. [para(57(a,1),3(a,1,2,2,1,1))]. given #20 (T,wt=21): 141 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x. [para(59(a,1),57(a,1)),flip(a)]. given #21 (A,wt=49): 11 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),x))) = f(z,x). [para(3(a,1),9(a,1,2,2,1,1,1,1))]. given #22 (F,wt=13): 210 f(x,f(f(x,x),f(x,y))) = f(x,x). [para(141(a,1),22(a,1,1)),rewrite(141(9)),flip(a)]. given #23 (F,wt=13): 231 f(f(x,x),f(x,f(f(x,x),y))) = x. [para(22(a,1),210(a,1,2,1)),rewrite(82(8))]. given #24 (T,wt=13): 235 f(x,f(f(x,x),f(y,x))) = f(x,x). [para(88(a,1),210(a,1,2,2))]. given #25 (T,wt=13): 244 f(f(x,x),f(x,f(y,f(x,x)))) = x. [para(88(a,1),231(a,1,2,2))]. given #26 (A,wt=59): 12 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(f(f(y,z),w),v),v),f(y,z)),z))))) = f(y,z). [para(9(a,1),9(a,1,1,2)),rewrite(9(17),9(18),9(21),9(25),9(42))]. given #27 (F,wt=19): 260 f(f(f(f(x,x),x),f(f(x,x),x)),x) = f(f(x,x),x). [para(11(a,1),244(a,1,2,2)),rewrite(237(13),57(14),82(11)),flip(a)]. given #28 (F,wt=21): 201 f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x)) = x. [para(74(a,1),88(a,1,2,1)),rewrite(74(16),74(18))]. given #29 (T,wt=21): 202 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x. [para(88(a,1),74(a,1,2,2,2))]. given #30 (T,wt=21): 227 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)). [para(3(a,1),210(a,1,2,2))]. given #31 (A,wt=59): 13 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(z,v),v),f(y,z)),f(f(y,z),w)))))) = f(y,z). [para(3(a,1),10(a,1,2,2,2,2,1,1,1,1))]. given #32 (F,wt=21): 234 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)). [para(82(a,1),210(a,1,2,2))]. given #33 (F,wt=21): 278 f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(22(a,1),260(a,1,1,1,1)),rewrite(82(5),82(10))]. given #34 (T,wt=21): 285 f(f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))),f(x,x)) = x. [para(88(a,1),201(a,1,1,2,2))]. given #35 (T,wt=23): 198 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [para(22(a,1),74(a,1,1)),rewrite(82(3),82(5))]. given #36 (A,wt=57): 15 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(f(f(y,y),w),f(f(f(f(f(y,v6),w),w),y),f(y,v7)))))))) = y. [para(10(a,1),9(a,1,1,2)),rewrite(10(20),10(20),10(22),10(25),10(46))]. given #37 (F,wt=23): 239 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(231(a,1),3(a,1,2,2,1,1,1)),rewrite(231(6))]. given #38 (F,wt=23): 255 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(x,z)))) = x. [para(244(a,1),3(a,1,2,2,1,1,1)),rewrite(244(6))]. given #39 (T,wt=23): 282 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(f(x,x),y))),x) = f(x,x). [para(22(a,1),201(a,1,1,1,1)),rewrite(82(5),82(11))]. given #40 (T,wt=23): 292 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [para(22(a,1),202(a,1,1)),rewrite(82(3),82(5))]. given #41 (A,wt=31): 37 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(22(a,1),3(a,1,1)),rewrite(22(3))]. given #42 (F,wt=23): 327 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x). [para(22(a,1),285(a,1,1,1,1)),rewrite(82(5),82(11))]. given #43 (F,wt=23): 353 f(f(x,x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(88(a,1),239(a,1,2,2,2))]. given #44 (T,wt=17): 394 f(f(x,x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(88(a,1),353(a,1,2))]. given #45 (T,wt=17): 405 f(f(x,x),f(f(x,f(x,f(y,f(x,x)))),x)) = x. [para(88(a,1),394(a,1,2,1,2,2))]. given #46 (A,wt=33): 38 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(22(a,1),3(a,1,2,1,1))]. given #47 (F,wt=21): 404 f(x,f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x))) = f(x,x). [para(22(a,1),394(a,1,1)),rewrite(82(5))]. given #48 (F,wt=21): 416 f(x,f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x))) = f(x,x). [para(22(a,1),405(a,1,1)),rewrite(82(5))]. given #49 (T,wt=23): 360 f(f(x,x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(z,x)))) = x. [para(88(a,1),255(a,1,2,2,2))]. given #50 (T,wt=25): 41 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(22(a,1),3(a,1,2,2,1,1,1))]. given #51 (A,wt=37): 40 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(22(a,1),3(a,1,2,2,1,1,1,1))]. given #52 (F,wt=19): 462 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x). [para(285(a,1),41(a,1,2,2,1)),rewrite(22(4),82(3),88(6))]. given #53 (F,wt=19): 463 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x. [para(327(a,1),41(a,1,2,2,1)),rewrite(48(3),88(8))]. given #54 (T,wt=19): 485 f(f(f(f(x,x),x),f(x,f(f(x,x),y))),x) = f(x,x). [para(462(a,1),88(a,1,2,1)),rewrite(462(14),82(9),462(14))]. given #55 (T,wt=19): 486 f(x,f(f(f(x,x),x),f(x,f(y,f(x,x))))) = f(x,x). [para(88(a,1),462(a,1,2,2,2))]. given #56 (A,wt=33): 46 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(22(a,1),9(a,1,2,2,1,1,1,1))]. given #57 (F,wt=19): 502 f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)) = x. [para(463(a,1),88(a,1,2,1)),rewrite(463(14),463(16))]. given #58 (F,wt=19): 503 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(y,x)))) = x. [para(88(a,1),463(a,1,2,2,2))]. given #59 (T,wt=19): 509 f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x) = f(x,x). [para(88(a,1),485(a,1,1,2,2))]. given #60 (T,wt=19): 535 f(f(f(x,f(x,x)),f(f(x,x),f(y,x))),f(x,x)) = x. [para(88(a,1),502(a,1,1,2,2))]. given #61 (A,wt=33): 47 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(22(a,1),9(a,1,2,2,1,1,1))]. given #62 (F,wt=15): 564 f(f(x,f(x,x)),f(x,f(f(x,x),y))) = x. [para(41(a,1),47(a,1,2,2,1)),rewrite(82(3),82(6),82(10),82(13),82(16),82(19),82(27),231(27),48(23),82(9),82(3),82(6)),flip(a)]. given #63 (F,wt=15): 577 f(f(x,f(x,x)),f(x,f(y,f(x,x)))) = x. [para(88(a,1),564(a,1,2,2))]. given #64 (T,wt=17): 576 f(f(f(x,x),x),f(f(x,x),f(x,y))) = f(x,x). [para(22(a,1),564(a,1,1,2)),rewrite(82(6))]. given #65 (T,wt=17): 590 f(f(f(x,x),x),f(f(x,x),f(y,x))) = f(x,x). [para(22(a,1),577(a,1,1,2)),rewrite(82(6))]. given #66 (A,wt=49): 49 f(x,f(f(x,y),f(f(f(f(f(f(x,x),f(z,x)),y),y),f(x,x)),f(f(x,u),f(f(f(f(f(f(x,x),v),u),u),f(x,x)),f(f(x,x),w)))))) = f(x,x). [para(22(a,1),10(a,1,1)),rewrite(22(3),22(11))]. given #67 (F,wt=25): 65 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(48(a,1),3(a,1,2,2,1,1,1))]. given #68 (F,wt=23): 634 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))),f(x,x)) = x. [para(65(a,1),88(a,1,2,1)),rewrite(65(19),65(21))]. given #69 (T,wt=23): 654 f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(z,x))),f(x,x)) = x. [para(88(a,1),634(a,1,1,2,2))]. given #70 (T,wt=25): 102 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(88(a,1),3(a,1,2,2,2))]. given #71 (A,wt=51): 50 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,u),f(f(f(f(f(f(y,y),v),u),u),f(y,y)),f(f(y,y),w)))))) = f(y,y). [para(22(a,1),10(a,1,2,1,1)),rewrite(22(12))]. given #72 (F,wt=25): 103 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),88(a,1,2,1)),rewrite(3(20),3(22))]. given #73 (F,wt=25): 116 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(22(a,1),7(a,1,2,1,1)),rewrite(103(11))]. given #74 (T,wt=25): 455 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(41(a,1),88(a,1,2,1)),rewrite(41(20),41(22))]. given #75 (T,wt=25): 457 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(88(a,1),41(a,1,2,2,2))]. given #76 (A,wt=41): 52 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(22(a,1),10(a,1,2,2,1,1,1))]. given #77 (F,wt=25): 571 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(x,z)))) = x. [para(564(a,1),3(a,1,2,2,1,1,1)),rewrite(231(7))]. given #78 (F,wt=25): 585 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(y,f(x,x)))),x),f(x,z)))) = x. [para(577(a,1),3(a,1,2,2,1,1,1)),rewrite(244(7))]. given #79 (T,wt=25): 636 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(88(a,1),65(a,1,2,2,2))]. given #80 (T,wt=25): 649 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(22(a,1),634(a,1,1,1,1)),rewrite(82(12))]. given #81 (A,wt=41): 54 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),f(u,u)),f(f(f(u,f(u,u)),y),f(y,v)))))) = y. [para(22(a,1),10(a,1,2,2,2,2,1,1,1))]. given #82 (F,wt=25): 663 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(22(a,1),654(a,1,1,1,1)),rewrite(82(12))]. given #83 (F,wt=25): 664 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(22(a,1),654(a,1,1,2,1,1,1))]. given #84 (T,wt=25): 681 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(102(a,1),88(a,1,2,1)),rewrite(102(20),102(22))]. given #85 (T,wt=25): 691 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(74(a,1),102(a,1,2,2,1,1,1,1)),rewrite(201(9),82(3))]. given #86 (A,wt=35): 60 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 #87 (F,wt=25): 737 f(f(f(x,x),x),f(x,f(f(f(x,f(x,f(f(x,x),y))),x),f(z,x)))) = x. [para(564(a,1),102(a,1,2,2,1,1,1)),rewrite(231(7))]. given #88 (F,wt=19): 1010 f(f(f(x,x),x),f(f(x,f(x,f(f(x,x),y))),x)) = x. [para(88(a,1),737(a,1,2))]. given #89 (T,wt=15): 1028 f(f(x,f(x,f(f(x,x),y))),x) = f(x,x). [para(1010(a,1),46(a,1,2,2,1)),rewrite(394(7),22(14)),flip(a)]. given #90 (T,wt=15): 1036 f(f(x,f(x,f(y,f(x,x)))),x) = f(x,x). [para(88(a,1),1028(a,1,1,2,2))]. given #91 (A,wt=29): 63 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(48(a,1),3(a,1,1))]. given #92 (F,wt=17): 1034 f(f(f(x,x),f(f(x,x),f(x,y))),f(x,x)) = x. [para(22(a,1),1028(a,1,1,2,2,1)),rewrite(82(10))]. given #93 (F,wt=17): 1038 f(f(x,x),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(1028(a,1),234(a,1,1)),rewrite(1028(6),1028(7),82(4),1028(12),1028(13),82(10))]. given #94 (T,wt=17): 1052 f(f(f(x,x),f(f(x,x),f(y,x))),f(x,x)) = x. [para(22(a,1),1036(a,1,1,2,2,2)),rewrite(82(10))]. given #95 (T,wt=17): 1055 f(f(x,x),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(1036(a,1),234(a,1,1)),rewrite(1036(6),1036(7),82(4),1036(12),1036(13),82(10))]. given #96 (A,wt=49): 64 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(48(a,1),3(a,1,2,2,1,1,1,1))]. given #97 (F,wt=21): 1078 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))) = f(x,x). [para(1034(a,1),234(a,1,1)),rewrite(1034(7),1034(7),1034(15),1034(15))]. given #98 (F,wt=21): 1098 f(x,f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))) = f(x,x). [para(1052(a,1),234(a,1,1)),rewrite(1052(7),1052(7),1052(15),1052(15))]. given #99 (T,wt=25): 770 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(88(a,1),103(a,1,1,2,1,1,1,1))]. given #100 (T,wt=23): 1141 f(f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z))),x) = f(x,x). [para(564(a,1),770(a,1,1,2,1,1,1)),rewrite(82(3),82(10),82(11))]. given #101 (A,wt=45): 66 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(48(a,1),9(a,1,1))]. given #102 (F,wt=23): 1142 f(f(f(x,f(x,f(y,f(x,x)))),f(x,f(f(x,x),z))),x) = f(x,x). [para(577(a,1),770(a,1,1,2,1,1,1)),rewrite(82(3),82(10),82(11))]. given #103 (F,wt=23): 1153 f(f(f(x,f(x,f(f(x,x),y))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(88(a,1),1141(a,1,1,2,2))]. given #104 (T,wt=23): 1175 f(f(f(x,f(x,f(y,f(x,x)))),f(x,f(z,f(x,x)))),x) = f(x,x). [para(88(a,1),1142(a,1,1,2,2))]. given #105 (T,wt=25): 772 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(74(a,1),103(a,1,1,2,1,1,1,1)),rewrite(82(3),82(12))]. given #106 (A,wt=45): 67 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(48(a,1),9(a,1,2,2,1,1,1,1))]. given #107 (F,wt=25): 956 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(88(a,1),681(a,1,1,2,1,1,1,1))]. given #108 (F,wt=25): 958 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(74(a,1),681(a,1,1,2,1,1,1,1)),rewrite(82(3),82(12))]. given #109 (T,wt=25): 1143 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(576(a,1),770(a,1,1,2,1,1,1)),rewrite(57(11))]. given #110 (T,wt=25): 1144 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(590(a,1),770(a,1,1,2,1,1,1)),rewrite(57(11))]. given #111 (A,wt=33): 68 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(48(a,1),9(a,1,2,2,1,1,1))]. given #112 (F,wt=25): 1154 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(1141(a,1),234(a,1,1)),rewrite(1141(10),1141(11),82(4),1141(20),1141(21),82(14))]. given #113 (F,wt=25): 1176 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(1142(a,1),234(a,1,1)),rewrite(1142(10),1142(11),82(4),1142(20),1142(21),82(14))]. given #114 (T,wt=25): 1182 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(22(a,1),1153(a,1,1,1,2,2,1)),rewrite(82(9),82(14))]. given #115 (T,wt=25): 1184 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(1153(a,1),234(a,1,1)),rewrite(1153(10),1153(11),82(4),1153(20),1153(21),82(14))]. given #116 (A,wt=45): 69 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,f(z,f(x,x))),y),y),x),f(f(f(x,x),u),f(f(f(f(f(x,v),u),u),x),f(x,w)))))) = x. [para(48(a,1),10(a,1,1))]. given #117 (F,wt=25): 1190 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(22(a,1),1175(a,1,1,1,2,2,2)),rewrite(82(9),82(14))]. given #118 (F,wt=25): 1192 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(1175(a,1),234(a,1,1)),rewrite(1175(10),1175(11),82(4),1175(20),1175(21),82(14))]. given #119 (T,wt=27): 86 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(82(a,1),3(a,1,2,2,1,1))]. given #120 (T,wt=15): 1330 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x. [para(86(a,1),47(a,1,2,2,1)),rewrite(82(3),88(6),22(6),462(7),82(4),88(7),22(7),82(10),88(13),22(13),22(21),231(21),48(17),82(3),82(3),88(6),22(6)),flip(a)]. given #121 (A,wt=41): 70 f(f(f(x,x),y),f(f(f(y,y),x),f(f(f(f(x,x),x),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(48(a,1),10(a,1,2,2,1,1,1))]. given #122 (F,wt=15): 1359 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x. [para(88(a,1),1330(a,1,2,2))]. given #123 (F,wt=17): 1349 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x). [para(86(a,1),68(a,1,2,2,1)),rewrite(88(8),48(6),463(8),88(7),48(5),88(13),48(11),48(17),210(18),22(16),88(8),48(6)),flip(a)]. given #124 (T,wt=17): 1392 f(f(x,f(x,x)),f(f(x,x),f(y,x))) = f(x,x). [para(22(a,1),1359(a,1,1,1)),rewrite(82(6))]. given #125 (T,wt=27): 640 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(65(a,1),227(a,1,1)),rewrite(65(11),65(11),65(22),65(22))]. given #126 (A,wt=39): 71 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(u,u),u),y),f(y,v)))))) = y. [para(48(a,1),10(a,1,2,2,2,2,1,1,1))]. given #127 (F,wt=27): 671 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(654(a,1),234(a,1,1)),rewrite(654(10),654(10),654(21),654(21))]. given #128 (F,wt=27): 680 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(82(a,1),102(a,1,2,2,1,1))]. given #129 (T,wt=27): 767 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(82(a,1),103(a,1,1,2,1,1))]. given #130 (T,wt=23): 1589 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(1028(a,1),767(a,1,1,2,1)),rewrite(1035(11))]. given #131 (A,wt=29): 72 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(57(a,1),3(a,1,1))]. given #132 (F,wt=23): 1590 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(x,z))),f(x,x)) = x. [para(1036(a,1),767(a,1,1,2,1)),rewrite(1053(11))]. given #133 (F,wt=23): 1598 f(f(f(x,f(x,f(f(x,x),y))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(88(a,1),1589(a,1,1,2,2))]. given #134 (T,wt=23): 1624 f(f(f(x,f(x,f(y,f(x,x)))),f(f(x,x),f(z,x))),f(x,x)) = x. [para(88(a,1),1590(a,1,1,2,2))]. given #135 (T,wt=25): 1591 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(1034(a,1),767(a,1,1,2,1)),rewrite(82(3),1075(12),82(12))]. given #136 (A,wt=49): 73 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(57(a,1),3(a,1,2,2,1,1,1,1))]. given #137 (F,wt=25): 1592 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(1052(a,1),767(a,1,1,2,1)),rewrite(82(3),1096(12),82(12))]. given #138 (F,wt=25): 1630 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(22(a,1),1598(a,1,1,1,2,2,1)),rewrite(82(8),82(12))]. given #139 (T,wt=25): 1637 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(22(a,1),1624(a,1,1,1,2,2,2)),rewrite(82(8),82(12))]. given #140 (T,wt=27): 793 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(22(a,1),455(a,1,1,1,1)),rewrite(82(13))]. given #141 (A,wt=45): 76 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(57(a,1),9(a,1,1))]. given #142 (F,wt=27): 880 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(649(a,1),234(a,1,1)),rewrite(649(11),649(12),82(4),649(22),649(23),82(15))]. given #143 (F,wt=27): 933 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(22(a,1),663(a,1,1,2,1,1,1))]. given #144 (T,wt=27): 939 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(663(a,1),234(a,1,1)),rewrite(663(11),663(12),82(4),663(22),663(23),82(15))]. given #145 (T,wt=27): 954 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(82(a,1),681(a,1,1,2,1,1))]. given #146 (A,wt=43): 77 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(57(a,1),9(a,1,2,2,1,1,1,1))]. given #147 (F,wt=15): 1722 f(f(x,f(f(x,x),x)),x) = f(f(x,x),x). [para(260(a,1),77(a,1,2,1)),rewrite(57(8),57(10),22(7))]. given #148 (F,wt=19): 1731 f(f(f(x,x),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(22(a,1),1722(a,1,1,2,1)),rewrite(82(9))]. given #149 (T,wt=25): 1740 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(1722(a,1),86(a,1,1)),rewrite(1035(13),1028(11))]. given #150 (T,wt=21): 1784 f(f(x,f(x,f(f(x,x),x))),f(f(x,x),f(x,y))) = f(x,x). [para(1740(a,1),68(a,1,2,2,1)),rewrite(210(32),22(30),57(11)),flip(a)]. given #151 (A,wt=37): 78 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(57(a,1),9(a,1,2,2,1,1))]. given #152 (F,wt=21): 1790 f(f(x,f(x,f(f(x,x),x))),f(f(x,x),f(y,x))) = f(x,x). [para(88(a,1),1784(a,1,2,2))]. given #153 (F,wt=23): 1787 f(f(f(x,x),f(f(x,x),f(x,f(x,x)))),f(x,f(f(x,x),y))) = x. [para(22(a,1),1784(a,1,1,2,2,1)),rewrite(82(9),82(13))]. given #154 (T,wt=23): 1813 f(f(f(x,x),f(f(x,x),f(x,f(x,x)))),f(x,f(y,f(x,x)))) = x. [para(22(a,1),1790(a,1,1,2,2,1)),rewrite(82(9),82(13))]. given #155 (T,wt=27): 1083 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(1038(a,1),3(a,1,2,2,1,1,1)),rewrite(1038(8))]. given #156 (A,wt=45): 79 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(f(f(x,x),u),f(f(f(f(f(x,v),u),u),x),f(x,w)))))) = x. [para(57(a,1),10(a,1,1))]. given #157 (F,wt=27): 1093 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(1038(a,1),102(a,1,2,2,1,1,1)),rewrite(1038(8))]. given #158 (F,wt=21): 1833 f(f(x,x),f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),x)) = x. [para(88(a,1),1093(a,1,2))]. given #159 (T,wt=21): 1844 f(f(x,x),f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),x)) = x. [para(88(a,1),1833(a,1,2,1,2,2,2,2))]. given #160 (T,wt=27): 1103 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(1055(a,1),3(a,1,2,2,1,1,1)),rewrite(1055(8))]. given #161 (A,wt=37): 80 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))))) = x. [para(57(a,1),10(a,1,2,2,1,1))]. given #162 (F,wt=27): 1113 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(1055(a,1),102(a,1,2,2,1,1,1)),rewrite(1055(8))]. given #163 (F,wt=27): 1131 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(82(a,1),770(a,1,1,2,1,1))]. given #164 (T,wt=27): 1211 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(82(a,1),956(a,1,1,2,1,1))]. given #165 (T,wt=27): 1354 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(1330(a,1),3(a,1,2,2,1,1,1)),rewrite(82(5),82(12))]. given #166 (A,wt=37): 81 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(57(a,1),10(a,1,2,2,2,2,1,1))]. given #167 (F,wt=19): 1909 f(f(x,f(x,f(f(x,x),y))),f(x,f(f(x,x),z))) = x. [para(1354(a,1),47(a,1,2,2,1)),rewrite(231(33),48(29),82(11)),flip(a)]. given #168 (F,wt=19): 1997 f(f(x,f(x,f(y,f(x,x)))),f(x,f(f(x,x),z))) = x. [para(88(a,1),1909(a,1,1,2,2))]. given #169 (T,wt=19): 1998 f(f(x,f(x,f(f(x,x),y))),f(x,f(z,f(x,x)))) = x. [para(88(a,1),1909(a,1,2,2))]. given #170 (T,wt=19): 2033 f(f(x,f(x,f(y,f(x,x)))),f(x,f(z,f(x,x)))) = x. [para(88(a,1),1997(a,1,2,2))]. given #171 (A,wt=49): 83 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(57(a,1),6(a,1,2,2,1,1,1,2,2,1,1)),rewrite(57(15))]. given #172 (F,wt=23): 1996 f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,x),f(x,z))) = f(x,x). [para(22(a,1),1909(a,1,1,2,2,1)),rewrite(82(9))]. given #173 (F,wt=23): 2032 f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,x),f(x,z))) = f(x,x). [para(22(a,1),1997(a,1,1,2,2,2)),rewrite(82(9))]. given #174 (T,wt=23): 2036 f(f(f(x,x),f(f(x,x),f(x,y))),f(f(x,x),f(z,x))) = f(x,x). [para(22(a,1),1998(a,1,1,2,2,1)),rewrite(82(9))]. given #175 (T,wt=23): 2043 f(f(f(x,x),f(f(x,x),f(y,x))),f(f(x,x),f(z,x))) = f(x,x). [para(22(a,1),2033(a,1,1,2,2,2)),rewrite(82(9))]. given #176 (A,wt=31): 84 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(82(a,1),3(a,1,1)),rewrite(82(3))]. given #177 (F,wt=27): 1600 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(1589(a,1),234(a,1,1)),rewrite(1589(10),1589(10),1589(21),1589(21))]. given #178 (F,wt=27): 1626 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(1590(a,1),234(a,1,1)),rewrite(1590(10),1590(10),1590(21),1590(21))]. given #179 (T,wt=27): 1633 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(1598(a,1),234(a,1,1)),rewrite(1598(10),1598(10),1598(21),1598(21))]. given #180 (T,wt=27): 1640 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(1624(a,1),234(a,1,1)),rewrite(1624(10),1624(10),1624(21),1624(21))]. given #181 (A,wt=37): 85 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(82(a,1),3(a,1,2,2,1,1,1,1))]. given #182 (F,wt=27): 1647 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(1591(a,1),234(a,1,1)),rewrite(1591(11),1591(12),82(4),1591(22),1591(23),82(15))]. given #183 (F,wt=27): 1657 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(1592(a,1),234(a,1,1)),rewrite(1592(11),1592(12),82(4),1592(22),1592(23),82(15))]. given #184 (T,wt=27): 1665 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(1630(a,1),234(a,1,1)),rewrite(1630(11),1630(12),82(4),1630(22),1630(23),82(15))]. given #185 (T,wt=27): 1671 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(1637(a,1),234(a,1,1)),rewrite(1637(11),1637(12),82(4),1637(22),1637(23),82(15))]. given #186 (A,wt=35): 87 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),y))) = f(y,z). [para(82(a,1),3(a,1,2,2,2))]. given #187 (F,wt=27): 2008 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(1909(a,1),116(a,1,2,2,1,1))]. given #188 (F,wt=27): 2012 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(1909(a,1),691(a,1,2,2,1,1))]. given #189 (T,wt=27): 2018 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(1909(a,1),772(a,1,1,2,1,1))]. given #190 (T,wt=27): 2022 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(1909(a,1),958(a,1,1,2,1,1))]. given #191 (A,wt=33): 89 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(82(a,1),9(a,1,2,2,1,1,1,1))]. given #192 (F,wt=27): 2053 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(2033(a,1),116(a,1,2,2,1,1))]. given #193 (F,wt=27): 2057 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(2033(a,1),691(a,1,2,2,1,1))]. given #194 (T,wt=27): 2063 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(2033(a,1),772(a,1,1,2,1,1))]. given #195 (T,wt=27): 2067 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(2033(a,1),958(a,1,1,2,1,1))]. given #196 (A,wt=41): 90 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(82(a,1),9(a,1,2,2,1,1))]. given #197 (F,wt=21): 2380 f(f(f(f(x,x),f(x,y)),f(f(x,x),x)),x) = f(f(x,x),x). [para(576(a,1),90(a,1,2,1,2,1)),rewrite(576(18),82(14),260(12),576(14),57(13),22(10))]. given #198 (F,wt=21): 2381 f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),x) = f(f(x,x),x). [para(590(a,1),90(a,1,2,1,2,1)),rewrite(590(18),82(14),260(12),590(14),57(13),22(10))]. given #199 (T,wt=23): 2378 f(f(f(x,f(f(x,x),y)),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(564(a,1),90(a,1,2,1,2,1)),rewrite(564(17),278(13),564(14),82(13),48(9))]. given #200 (T,wt=23): 2379 f(f(f(x,f(y,f(x,x))),f(x,f(x,x))),f(x,x)) = f(x,f(x,x)). [para(577(a,1),90(a,1,2,1,2,1)),rewrite(577(17),278(13),577(14),82(13),48(9))]. given #201 (A,wt=49): 91 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,u),f(f(f(f(f(f(x,x),v),u),u),f(x,x)),f(f(x,x),w)))))) = f(x,x). [para(82(a,1),10(a,1,1)),rewrite(82(3),82(11))]. given #202 (F,wt=25): 2420 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(2381(a,1),3(a,1,2,2,1))]. given #203 (F,wt=25): 2431 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(2381(a,1),37(a,1,2,2,1)),rewrite(82(3),82(6))]. given #204 (T,wt=25): 2436 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(2381(a,1),102(a,1,2,2,1))]. given #205 (T,wt=11): 2491 f(f(x,x),f(f(x,x),x)) = x. [para(22(a,1),2436(a,1,2))]. given #206 (A,wt=43): 92 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(y,v)))))) = y. [para(82(a,1),10(a,1,2,2,1,1))]. given #207 (F,wt=11): 2498 f(x,f(x,f(x,x))) = f(x,x). [para(278(a,1),2436(a,1,2,2,2)),rewrite(82(3),82(3),82(3),82(6),22(9))]. given #208 (F,wt=17): 2493 f(f(x,x),f(x,f(f(f(x,x),x),f(y,x)))) = x. [para(2436(a,1),88(a,1,2,1)),rewrite(2491(4),2491(10),210(13),82(7),2491(5)),flip(a)]. given #209 (T,wt=17): 2535 f(f(x,x),f(x,f(f(f(x,x),x),f(x,y)))) = x. [back_rewrite(2420),rewrite(2491(5))]. given #210 (T,wt=21): 2546 f(x,f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x). [back_rewrite(2460),rewrite(2498(3))]. given #211 (A,wt=59): 93 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(y,v),v),f(y,z)),f(f(y,z),w)))))) = f(y,z). [para(82(a,1),10(a,1,2,2,2,2,1,1,1,1))]. given #212 (F,wt=21): 2548 f(x,f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y)))) = f(x,x). [back_rewrite(2431),rewrite(2498(3))]. given #213 (F,wt=27): 2084 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(1996(a,1),3(a,1,2,2,1,1))]. given #214 (T,wt=27): 2100 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(1996(a,1),102(a,1,2,2,1,1))]. given #215 (T,wt=27): 2102 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(1996(a,1),103(a,1,1,2,1,1))]. given #216 (A,wt=43): 94 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),f(f(y,u),f(y,u))),f(f(f(y,u),y),f(y,v)))))) = y. [para(82(a,1),10(a,1,2,2,2,2,1,1))]. given #217 (F,wt=27): 2105 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(1996(a,1),681(a,1,1,2,1,1))]. given #218 (F,wt=27): 2118 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(2043(a,1),3(a,1,2,2,1,1))]. given #219 (T,wt=27): 2128 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(2043(a,1),102(a,1,2,2,1,1))]. given #220 (T,wt=27): 2130 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(2043(a,1),103(a,1,1,2,1,1))]. given #221 (A,wt=59): 95 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(f(f(y,z),w),v),v),f(y,z)),y))))) = f(y,z). [para(82(a,1),10(a,1,2,2,2,2,2))]. given #222 (F,wt=27): 2133 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(2043(a,1),681(a,1,1,2,1,1))]. given #223 (F,wt=27): 2504 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(2436(a,1),102(a,1,2,2,1,1,1)),rewrite(2491(6),2493(8),2491(5))]. given #224 (T,wt=21): 2815 f(f(x,x),f(f(x,f(x,f(f(f(x,x),x),f(y,x)))),x)) = x. [para(88(a,1),2504(a,1,2))]. given #225 (T,wt=27): 2506 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(2436(a,1),116(a,1,2,1)),rewrite(2491(6),2493(8),2491(5),82(10),82(11),82(15))]. given #226 (A,wt=49): 98 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(88(a,1),3(a,1,1)),rewrite(82(8))]. given #227 (F,wt=27): 2522 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(2476),rewrite(2491(5))]. given #228 (F,wt=21): 2856 f(f(x,x),f(f(x,f(x,f(f(f(x,x),x),f(x,y)))),x)) = x. [para(88(a,1),2522(a,1,2))]. given #229 (T,wt=27): 2531 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(2427),rewrite(2491(5))]. given #230 (T,wt=29): 272 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(260(a,1),3(a,1,1)),rewrite(88(10))]. given #231 (A,wt=45): 99 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(88(a,1),3(a,1,2,1))]. given #232 (F,wt=29): 296 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),227(a,1,1)),rewrite(3(11),3(11),3(23),3(23))]. given #233 (F,wt=29): 426 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(38(a,1),88(a,1,2,1)),rewrite(38(26),82(14),38(26))]. given #234 (T,wt=29): 460 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(41(a,1),227(a,1,1)),rewrite(41(11),41(11),41(23),41(23))]. given #235 (T,wt=29): 597 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),576(a,1,2,2))]. given #236 (A,wt=31): 100 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(88(a,1),3(a,1,2,2,1,1,1,1))]. given #237 (F,wt=29): 602 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(82(a,1),576(a,1,2,2))]. given #238 (F,wt=19): 3045 f(f(x,f(x,x)),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(1028(a,1),602(a,1,1,1,1)),rewrite(1028(6),82(3),1028(5),1028(7),1028(8),82(5),1028(13),1028(14),82(11))]. given #239 (T,wt=19): 3046 f(f(x,f(x,x)),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(1036(a,1),602(a,1,1,1,1)),rewrite(1036(6),82(3),1036(5),1036(7),1036(8),82(5),1036(13),1036(14),82(11))]. given #240 (T,wt=25): 3047 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(1034(a,1),602(a,1,1,1,1)),rewrite(1034(7),1034(8),1034(9),1034(9),1034(17),1034(17))]. given #241 (A,wt=45): 101 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(88(a,1),3(a,1,2,2,1,1,1))]. given #242 (F,wt=25): 3048 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(1052(a,1),602(a,1,1,1,1)),rewrite(1052(7),1052(8),1052(9),1052(9),1052(17),1052(17))]. given #243 (F,wt=27): 3074 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(3045(a,1),770(a,1,1,2,1,1,1)),rewrite(82(3),82(14),82(13))]. given #244 (T,wt=27): 3076 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(3045(a,1),956(a,1,1,2,1,1,1)),rewrite(82(3),82(14),82(13))]. given #245 (T,wt=27): 3084 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(3045(a,1),90(a,1,2,1,2,1)),rewrite(3045(21),278(15),3045(18),2498(13),82(13),48(11))]. given #246 (A,wt=45): 104 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(88(a,1),9(a,1,2,2,1,1,1,1))]. given #247 (F,wt=27): 3099 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(3046(a,1),770(a,1,1,2,1,1,1)),rewrite(82(3),82(14),82(13))]. given #248 (F,wt=27): 3101 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(3046(a,1),956(a,1,1,2,1,1,1)),rewrite(82(3),82(14),82(13))]. given #249 (T,wt=27): 3109 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(3046(a,1),90(a,1,2,1,2,1)),rewrite(3046(21),278(15),3046(18),2498(13),82(13),48(11))]. given #250 (T,wt=29): 674 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(48(a,1),102(a,1,1))]. given #251 (A,wt=37): 105 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),88(a,1,2,1)),rewrite(9(28),9(31))]. given #252 (F,wt=29): 676 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),102(a,1,1))]. given #253 (F,wt=29): 701 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(260(a,1),102(a,1,1)),rewrite(88(10))]. given #254 (T,wt=29): 707 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(102(a,1),227(a,1,1)),rewrite(102(11),102(11),102(23),102(23))]. given #255 (T,wt=29): 813 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(457(a,1),227(a,1,1)),rewrite(457(11),457(11),457(23),457(23))]. given #256 (A,wt=47): 106 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(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y. [para(88(a,1),10(a,1,2,2,1,1,1,1))]. given #257 (F,wt=29): 951 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(22(a,1),681(a,1,1,1,1)),rewrite(82(14))]. given #258 (F,wt=29): 1073 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),1034(a,1,1,2,2))]. given #259 (T,wt=29): 1076 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(82(a,1),1034(a,1,1,2,2))]. given #260 (T,wt=19): 3460 f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),x) = f(x,x). [para(1028(a,1),1076(a,1,1,1,1)),rewrite(1028(6),82(3),1028(5),1028(6),82(3),1028(11),1028(12),82(9),1028(12))]. given #261 (A,wt=41): 107 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(v,y),u),u),y),f(y,w)))))) = y. [para(88(a,1),10(a,1,2,2,2,2,1,1,1,1))]. given #262 (F,wt=19): 3461 f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),x) = f(x,x). [para(1036(a,1),1076(a,1,1,1,1)),rewrite(1036(6),82(3),1036(5),1036(6),82(3),1036(11),1036(12),82(9),1036(12))]. given #263 (F,wt=21): 3492 f(f(x,x),f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))) = x. [para(3460(a,1),234(a,1,1)),rewrite(3460(8),3460(9),82(4),3460(16),3460(17),82(12))]. given #264 (T,wt=21): 3589 f(f(x,x),f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))) = x. [para(3461(a,1),234(a,1,1)),rewrite(3461(8),3461(9),82(4),3461(16),3461(17),82(12))]. given #265 (T,wt=23): 3509 f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))) = x. [para(3460(a,1),602(a,1,1,1,1)),rewrite(3460(8),82(3),3460(7),3460(9),3460(10),82(5),3460(17),3460(18),82(13))]. given #266 (A,wt=41): 108 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(w,y)))))) = y. [para(88(a,1),10(a,1,2,2,2,2,2))]. given #267 (F,wt=23): 3510 f(f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))),x) = f(x,x). [para(3460(a,1),1076(a,1,1,1,1)),rewrite(3460(8),82(3),3460(7),3460(8),82(3),3460(15),3460(16),82(11),3460(16))]. given #268 (F,wt=23): 3606 f(f(x,f(x,x)),f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))) = x. [para(3461(a,1),602(a,1,1,1,1)),rewrite(3461(8),82(3),3461(7),3461(9),3461(10),82(5),3461(17),3461(18),82(13))]. given #269 (T,wt=23): 3607 f(f(x,f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))),x) = f(x,x). [para(3461(a,1),1076(a,1,1,1,1)),rewrite(3461(8),82(3),3461(7),3461(8),82(3),3461(15),3461(16),82(11),3461(16))]. given #270 (T,wt=25): 3462 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(1034(a,1),1076(a,1,1,1,1)),rewrite(1034(7),1034(8),1034(8),1034(16),1034(16),1034(18))]. given #271 (A,wt=41): 109 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(f(f(x,x),u),f(f(f(f(f(x,v),u),u),x),f(x,w))))),f(x,x)) = x. [para(10(a,1),88(a,1,2,1)),rewrite(10(36),10(38))]. given #272 (F,wt=25): 3463 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(1052(a,1),1076(a,1,1,1,1)),rewrite(1052(7),1052(8),1052(8),1052(16),1052(16),1052(18))]. given #273 (F,wt=25): 3720 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(3510(a,1),234(a,1,1)),rewrite(3510(10),3510(11),82(4),3510(20),3510(21),82(14))]. given #274 (T,wt=25): 3753 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(3607(a,1),234(a,1,1)),rewrite(3607(10),3607(11),82(4),3607(20),3607(21),82(14))]. given #275 (T,wt=27): 3499 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(3460(a,1),767(a,1,1,2,1)),rewrite(3491(15))]. given #276 (A,wt=57): 110 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(u,y)))),y),f(y,v)))) = y. [para(88(a,1),6(a,1,2,2,1,1,1,2,2,2)),rewrite(88(22))]. given #277 (F,wt=27): 3500 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(3460(a,1),954(a,1,1,2,1)),rewrite(3491(15))]. given #278 (F,wt=27): 3596 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(3461(a,1),767(a,1,1,2,1)),rewrite(3588(15))]. given #279 (T,wt=27): 3597 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(3461(a,1),954(a,1,1,2,1)),rewrite(3588(15))]. given #280 (T,wt=27): 3733 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(3510(a,1),602(a,1,1,1,1)),rewrite(3510(10),82(3),3510(9),3510(11),3510(12),82(5),3510(21),3510(22),82(15))]. given #281 (A,wt=57): 111 f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(v,y)))) = y. [para(88(a,1),6(a,1,2,2,2))]. given #282 (F,wt=27): 3734 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(3510(a,1),1076(a,1,1,1,1)),rewrite(3510(10),82(3),3510(9),3510(10),82(3),3510(19),3510(20),82(13),3510(20))]. given #283 (F,wt=27): 3766 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(3607(a,1),602(a,1,1,1,1)),rewrite(3607(10),82(3),3607(9),3607(11),3607(12),82(5),3607(21),3607(22),82(15))]. given #284 (T,wt=27): 3767 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(3607(a,1),1076(a,1,1,1,1)),rewrite(3607(10),82(3),3607(9),3607(10),82(3),3607(19),3607(20),82(13),3607(20))]. given #285 (T,wt=29): 1129 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(22(a,1),770(a,1,1,1,1)),rewrite(82(14))]. given #286 (A,wt=53): 113 f(f(f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),v)))) = f(y,x). [para(22(a,1),7(a,1,1,1,2,1,1,1))]. given #287 (F,wt=29): 1138 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(770(a,1),234(a,1,1)),rewrite(770(11),770(11),770(23),770(23))]. given #288 (F,wt=29): 1210 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(22(a,1),956(a,1,1,1,1)),rewrite(82(14))]. given #289 (T,wt=29): 1217 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(956(a,1),234(a,1,1)),rewrite(956(11),956(11),956(23),956(23))]. given #290 (T,wt=29): 1341 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(1028(a,1),86(a,1,2,2,1)),rewrite(1035(15))]. given #291 (A,wt=55): 119 f(f(f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),x),f(x,z))),f(y,x)),f(f(f(f(y,x),f(y,x)),u),f(f(f(f(x,u),u),f(y,x)),f(f(y,x),v)))) = f(y,x). [para(82(a,1),7(a,1,1,1,2,1,1))]. given #292 (F,wt=29): 1343 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(1036(a,1),86(a,1,2,2,1)),rewrite(1053(15))]. given #293 (F,wt=29): 1413 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),1349(a,1,2,2))]. given #294 (T,wt=29): 1420 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(82(a,1),1349(a,1,2,2))]. given #295 (T,wt=19): 4039 f(f(f(x,x),x),f(x,f(x,f(x,f(f(x,x),y))))) = x. [para(1028(a,1),1420(a,1,1,1)),rewrite(1028(6),1028(7),82(4),1028(7),1028(8),82(5),1028(13),1028(14),82(11))]. given #296 (A,wt=51): 121 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),f(x,x)),f(f(x,f(z,x)),f(f(z,x),v)))) = f(z,x). [para(82(a,1),7(a,1,2,2,1,1))]. given #297 (F,wt=19): 4040 f(f(f(x,x),x),f(x,f(x,f(x,f(y,f(x,x)))))) = x. [para(1036(a,1),1420(a,1,1,1)),rewrite(1036(6),1036(7),82(4),1036(7),1036(8),82(5),1036(13),1036(14),82(11))]. given #298 (F,wt=23): 4063 f(f(f(x,x),x),f(x,f(x,f(x,f(x,f(x,f(f(x,x),y))))))) = x. [para(3460(a,1),1420(a,1,1,1)),rewrite(3460(8),3460(9),82(4),3460(9),3460(10),82(5),3460(17),3460(18),82(13))]. given #299 (T,wt=23): 4064 f(f(f(x,x),x),f(x,f(x,f(x,f(x,f(x,f(y,f(x,x)))))))) = x. [para(3461(a,1),1420(a,1,1,1)),rewrite(3461(8),3461(9),82(4),3461(9),3461(10),82(5),3461(17),3461(18),82(13))]. given #300 (T,wt=25): 4041 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(1034(a,1),1420(a,1,1,1)),rewrite(1034(7),1034(7),1034(9),1034(9),1034(17),1034(17))]. given #301 (A,wt=49): 122 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),z))) = f(z,x). [para(82(a,1),7(a,1,2,2,2))]. given #302 (F,wt=25): 4042 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(1052(a,1),1420(a,1,1,1)),rewrite(1052(7),1052(7),1052(9),1052(9),1052(17),1052(17))]. given #303 (F,wt=27): 4065 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(3510(a,1),1420(a,1,1,1)),rewrite(3510(10),3510(11),82(4),3510(11),3510(12),82(5),3510(21),3510(22),82(15))]. given #304 (T,wt=27): 4066 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(3607(a,1),1420(a,1,1,1)),rewrite(3607(10),3607(11),82(4),3607(11),3607(12),82(5),3607(21),3607(22),82(15))]. given #305 (T,wt=29): 1564 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(1028(a,1),680(a,1,2,2,1)),rewrite(1035(15))]. given #306 (A,wt=37): 123 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),88(a,1,2,1)),rewrite(7(37),7(40))]. given #307 (F,wt=29): 1566 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(1036(a,1),680(a,1,2,2,1)),rewrite(1053(15))]. given #308 (F,wt=29): 1677 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(793(a,1),234(a,1,1)),rewrite(793(12),793(13),82(4),793(24),793(25),82(16))]. given #309 (T,wt=29): 1702 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(933(a,1),234(a,1,1)),rewrite(933(12),933(13),82(4),933(24),933(25),82(16))]. given #310 (T,wt=29): 2526 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(2452),rewrite(2491(12))]. given #311 (A,wt=53): 124 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),f(f(z,x),w)))) = f(z,x). [para(88(a,1),7(a,1,1,1,2,2))]. given #312 (F,wt=25): 4381 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(1028(a,1),2526(a,1,1,1)),rewrite(1028(6),82(3),1028(5),1028(6),1028(7),82(4),1028(6),1028(15))]. given #313 (F,wt=25): 4382 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(1036(a,1),2526(a,1,1,1)),rewrite(1036(6),82(3),1036(5),1036(6),1036(7),82(4),1036(6),1036(15))]. given #314 (T,wt=25): 4383 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(1034(a,1),2526(a,1,1,1)),rewrite(1034(7),1034(8),1034(8),1034(8),1034(9),1034(18))]. given #315 (T,wt=25): 4384 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(1052(a,1),2526(a,1,1,1)),rewrite(1052(7),1052(8),1052(8),1052(8),1052(9),1052(18))]. given #316 (A,wt=53): 125 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),f(w,f(z,x))))) = f(z,x). [para(88(a,1),7(a,1,2,2,2))]. given #317 (F,wt=29): 2527 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. [back_rewrite(2450),rewrite(2491(5))]. given #318 (F,wt=29): 2534 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(2421),rewrite(2491(12))]. given #319 (T,wt=29): 2536 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(2223),rewrite(2491(11))]. given #320 (T,wt=29): 2537 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(1654),rewrite(2491(9))]. given #321 (A,wt=49): 126 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(97(a,1),3(a,1,1)),rewrite(82(8))]. given #322 (F,wt=25): 4520 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(57(a,1),2537(a,1,2,2,2))]. given #323 (F,wt=27): 4530 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(22(a,1),4520(a,1,1,2,1)),rewrite(82(7),82(10),82(13))]. given #324 (T,wt=29): 2549 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(2228),rewrite(2498(10))]. given #325 (T,wt=29): 2559 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(2491(a,1),3(a,1,2,1))]. given #326 (A,wt=45): 127 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(97(a,1),3(a,1,2,1))]. given #327 (F,wt=29): 2576 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(2491(a,1),102(a,1,2,1))]. given #328 (F,wt=23): 4654 f(f(x,y),f(f(f(f(y,x),f(f(y,y),y)),f(f(y,y),y)),y)) = y. [para(88(a,1),2576(a,1,2))]. given #329 (T,wt=23): 4742 f(f(f(f(x,f(x,x)),f(f(x,x),x)),f(f(x,x),x)),x) = f(x,x). [para(4654(a,1),46(a,1,2,2,1)),rewrite(22(33),57(12)),flip(a)]. given #330 (T,wt=23): 4743 f(f(f(f(f(x,x),x),f(x,f(x,x))),f(x,f(x,x))),f(x,x)) = x. [para(4654(a,1),47(a,1,2,2,1)),rewrite(82(5),82(8),82(16),82(19),82(26),82(29),82(37),48(35),82(13),82(5),82(8)),flip(a)]. given #331 (A,wt=31): 128 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(97(a,1),3(a,1,2,2,1,1,1,1))]. given #332 (F,wt=25): 4831 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(4742(a,1),234(a,1,1)),rewrite(4742(10),4742(11),82(4),4742(20),4742(21),82(14))]. given #333 (F,wt=27): 4729 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(48(a,1),4654(a,1,1))]. given #334 (T,wt=27): 4731 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(48(a,1),4654(a,1,2,1,1)),rewrite(260(6))]. given #335 (T,wt=23): 4921 f(f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),x)),x) = f(x,x). [para(4731(a,1),46(a,1,2,2,1)),rewrite(22(33),57(12)),flip(a)]. given #336 (A,wt=45): 129 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(97(a,1),3(a,1,2,2,1,1,1))]. given #337 (F,wt=23): 4922 f(f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,f(x,x))),f(x,x)) = x. [para(4731(a,1),67(a,1,2,2,1)),rewrite(82(3),82(5),82(8),82(14),82(16),82(19),82(24),82(26),82(29),82(37),48(35),82(13),82(3),82(5),82(8)),flip(a)]. given #338 (F,wt=25): 4935 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(4921(a,1),234(a,1,1)),rewrite(4921(10),4921(11),82(4),4921(20),4921(21),82(14))]. given #339 (T,wt=27): 4732 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(57(a,1),4654(a,1,1))]. given #340 (T,wt=27): 4839 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(4742(a,1),602(a,1,1,1,1)),rewrite(4742(10),82(3),4742(9),4742(11),4742(12),82(5),4742(21),4742(22),82(15))]. given #341 (A,wt=45): 130 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(97(a,1),9(a,1,2,2,1,1,1,1))]. given #342 (F,wt=27): 4840 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(4742(a,1),1076(a,1,1,1,1)),rewrite(4742(10),82(3),4742(9),4742(10),82(3),4742(19),4742(20),82(13),4742(20))]. given #343 (F,wt=27): 4843 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(4742(a,1),1420(a,1,1,1)),rewrite(4742(10),4742(11),82(4),4742(11),4742(12),82(5),4742(21),4742(22),82(15))]. given #344 (T,wt=27): 4851 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(4743(a,1),234(a,1,1)),rewrite(4743(10),4743(10),4743(21),4743(21))]. given #345 (T,wt=27): 4944 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(4921(a,1),602(a,1,1,1,1)),rewrite(4921(10),82(3),4921(9),4921(11),4921(12),82(5),4921(21),4921(22),82(15))]. given #346 (A,wt=47): 131 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(f(f(x,x),u),f(f(f(f(f(x,v),u),u),x),f(x,w)))))) = x. [para(97(a,1),10(a,1,2,2,1,1,1,1))]. given #347 (F,wt=27): 4945 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(4921(a,1),1076(a,1,1,1,1)),rewrite(4921(10),82(3),4921(9),4921(10),82(3),4921(19),4921(20),82(13),4921(20))]. given #348 (F,wt=27): 4948 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(4921(a,1),1420(a,1,1,1)),rewrite(4921(10),4921(11),82(4),4921(11),4921(12),82(5),4921(21),4921(22),82(15))]. given #349 (T,wt=27): 4956 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(4922(a,1),234(a,1,1)),rewrite(4922(10),4922(10),4922(21),4922(21))]. given #350 (T,wt=29): 2827 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(22(a,1),2815(a,1,1)),rewrite(82(5))]. given #351 (A,wt=57): 172 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(22(a,1),8(a,1,2,1,2,2,1,1,1)),rewrite(22(18))]. given #352 (F,wt=29): 2869 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(22(a,1),2856(a,1,1)),rewrite(82(5))]. given #353 (F,wt=29): 3043 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(649(a,1),602(a,1,1,1,1)),rewrite(649(11),82(3),649(10),649(12),649(13),82(5),649(23),649(24),82(16))]. given #354 (T,wt=29): 3044 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(663(a,1),602(a,1,1,1,1)),rewrite(663(11),82(3),663(10),663(12),663(13),82(5),663(23),663(24),82(16))]. given #355 (T,wt=29): 3054 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(1591(a,1),602(a,1,1,1,1)),rewrite(1591(11),82(3),1591(10),1591(12),1591(13),82(5),1591(23),1591(24),82(16))]. given #356 (A,wt=59): 174 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(48(a,1),8(a,1,2,1,2,2,1,1,1)),rewrite(82(5),48(16))]. given #357 (F,wt=29): 3055 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(1592(a,1),602(a,1,1,1,1)),rewrite(1592(11),82(3),1592(10),1592(12),1592(13),82(5),1592(23),1592(24),82(16))]. given #358 (F,wt=29): 3056 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(1630(a,1),602(a,1,1,1,1)),rewrite(1630(11),82(3),1630(10),1630(12),1630(13),82(5),1630(23),1630(24),82(16))]. given #359 (T,wt=29): 3057 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(1637(a,1),602(a,1,1,1,1)),rewrite(1637(11),82(3),1637(10),1637(12),1637(13),82(5),1637(23),1637(24),82(16))]. given #360 (T,wt=29): 3126 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(3047(a,1),90(a,1,2,1,2,1)),rewrite(3047(26),82(18),260(16),3047(22),2491(16),22(14))]. given #361 (A,wt=31): 175 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(57(a,1),8(a,1,2,1,2,2,1,1)),rewrite(74(10),57(6))]. given #362 (F,wt=29): 3143 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(3048(a,1),90(a,1,2,1,2,1)),rewrite(3048(26),82(18),260(16),3048(22),2491(16),22(14))]. given #363 (F,wt=29): 3146 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(3074(a,1),234(a,1,1)),rewrite(3074(12),3074(13),82(4),3074(24),3074(25),82(16))]. given #364 (T,wt=29): 3154 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(3076(a,1),234(a,1,1)),rewrite(3076(12),3076(13),82(4),3076(24),3076(25),82(16))]. given #365 (T,wt=29): 3180 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(1722(a,1),104(a,1,2,2,1,1,1)),rewrite(260(16),57(15),2491(16),22(14))]. given #366 (A,wt=57): 178 f(f(f(f(x,x),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),f(f(f(y,f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))),x),f(x,v))),f(x,x)) = x. [para(8(a,1),88(a,1,2,1)),rewrite(8(52),8(54))]. given #367 (F,wt=29): 3207 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(3099(a,1),234(a,1,1)),rewrite(3099(12),3099(13),82(4),3099(24),3099(25),82(16))]. given #368 (F,wt=29): 3215 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(3101(a,1),234(a,1,1)),rewrite(3101(12),3101(13),82(4),3101(24),3101(25),82(16))]. given #369 (T,wt=29): 3458 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(649(a,1),1076(a,1,1,1,1)),rewrite(649(11),82(3),649(10),649(11),82(3),649(21),649(22),82(14),649(22))]. given #370 (T,wt=29): 3459 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(663(a,1),1076(a,1,1,1,1)),rewrite(663(11),82(3),663(10),663(11),82(3),663(21),663(22),82(14),663(22))]. given #371 (A,wt=57): 179 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))),y),f(y,v)))) = y. [para(88(a,1),8(a,1,2,1,2,2,2)),rewrite(88(22))]. given #372 (F,wt=29): 3471 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(1591(a,1),1076(a,1,1,1,1)),rewrite(1591(11),82(3),1591(10),1591(11),82(3),1591(21),1591(22),82(14),1591(22))]. given #373 (F,wt=29): 3472 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(1592(a,1),1076(a,1,1,1,1)),rewrite(1592(11),82(3),1592(10),1592(11),82(3),1592(21),1592(22),82(14),1592(22))]. given #374 (T,wt=29): 3473 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(1630(a,1),1076(a,1,1,1,1)),rewrite(1630(11),82(3),1630(10),1630(11),82(3),1630(21),1630(22),82(14),1630(22))]. given #375 (T,wt=29): 3474 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(1637(a,1),1076(a,1,1,1,1)),rewrite(1637(11),82(3),1637(10),1637(11),82(3),1637(21),1637(22),82(14),1637(22))]. given #376 (A,wt=57): 180 f(f(x,y),f(f(f(y,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),f(f(f(x,f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))),y),f(v,y)))) = y. [para(88(a,1),8(a,1,2,2,2))]. given #377 (F,wt=29): 3610 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(22(a,1),3492(a,1,1)),rewrite(82(8))]. given #378 (F,wt=29): 3621 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(22(a,1),3589(a,1,1)),rewrite(82(8))]. given #379 (T,wt=29): 3870 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(3734(a,1),234(a,1,1)),rewrite(3734(12),3734(13),82(4),3734(24),3734(25),82(16))]. given #380 (T,wt=29): 3890 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(3767(a,1),234(a,1,1)),rewrite(3767(12),3767(13),82(4),3767(24),3767(25),82(16))]. given #381 (A,wt=55): 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)),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(74(a,1),9(a,1,2,2,1,1,1)),rewrite(74(21))]. given #382 (F,wt=29): 4037 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(649(a,1),1420(a,1,1,1)),rewrite(649(11),649(12),82(4),649(12),649(13),82(5),649(23),649(24),82(16))]. given #383 (F,wt=29): 4038 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(663(a,1),1420(a,1,1,1)),rewrite(663(11),663(12),82(4),663(12),663(13),82(5),663(23),663(24),82(16))]. given #384 (T,wt=29): 4046 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(1591(a,1),1420(a,1,1,1)),rewrite(1591(11),1591(12),82(4),1591(12),1591(13),82(5),1591(23),1591(24),82(16))]. given #385 (T,wt=29): 4047 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(1592(a,1),1420(a,1,1,1)),rewrite(1592(11),1592(12),82(4),1592(12),1592(13),82(5),1592(23),1592(24),82(16))]. given #386 (A,wt=47): 195 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(f(f(x,x),z),f(f(f(f(f(x,u),z),z),x),f(x,v)))))) = x. [para(74(a,1),10(a,1,2,2,1,1,1)),rewrite(74(10))]. given #387 (F,wt=29): 4048 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(1630(a,1),1420(a,1,1,1)),rewrite(1630(11),1630(12),82(4),1630(12),1630(13),82(5),1630(23),1630(24),82(16))]. given #388 (F,wt=29): 4049 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(1637(a,1),1420(a,1,1,1)),rewrite(1637(11),1637(12),82(4),1637(12),1637(13),82(5),1637(23),1637(24),82(16))]. given #389 (T,wt=29): 4211 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(1028(a,1),122(a,1,1,2)),rewrite(103(15),1028(5),1028(6),82(3),1028(8),1028(17))]. given #390 (T,wt=27): 5567 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(82(a,1),4211(a,1,2,2,1,1))]. given #391 (A,wt=47): 196 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,u),f(f(f(f(y,u),u),f(y,y)),f(f(y,y),v)))))) = f(y,y). [para(74(a,1),10(a,1,2,2,2,2,1,1,1,1)),rewrite(82(5),82(12))]. given #392 (F,wt=27): 5640 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(5567(a,1),88(a,1,2,1)),rewrite(5567(22),82(13),5567(22))]. given #393 (F,wt=27): 5641 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(88(a,1),5567(a,1,2,2,2,2,2))]. given #394 (T,wt=27): 5691 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(88(a,1),5640(a,1,1,2,2,2,2))]. given #395 (T,wt=29): 4212 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(1036(a,1),122(a,1,1,2)),rewrite(103(15),1036(5),1036(6),82(3),1036(8),1036(17))]. given #396 (A,wt=49): 197 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(74(a,1),22(a,1,1))]. given #397 (F,wt=29): 4373 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(285(a,1),2526(a,1,1,1)),rewrite(285(9),285(10),285(10),285(10),285(11),285(22))]. given #398 (F,wt=29): 4414 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(3460(a,1),2526(a,1,1,1)),rewrite(3460(8),82(3),3460(7),3460(8),3460(9),82(4),3460(8),3460(19))]. given #399 (T,wt=29): 4415 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(3461(a,1),2526(a,1,1,1)),rewrite(3461(8),82(3),3461(7),3461(8),3461(9),82(4),3461(8),3461(19))]. given #400 (T,wt=29): 4521 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(88(a,1),2537(a,1,2,2,2))]. given #401 (A,wt=37): 200 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(82(a,1),74(a,1,2,2,2))]. given #402 (F,wt=29): 4726 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(22(a,1),4654(a,1,1)),rewrite(82(6),82(9))]. given #403 (F,wt=29): 4734 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(82(a,1),4654(a,1,1)),rewrite(82(6),82(9))]. given #404 (T,wt=29): 4737 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(88(a,1),4654(a,1,2,1,1,1))]. given #405 (T,wt=29): 4739 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(97(a,1),4654(a,1,2,1,1,1))]. given #406 (A,wt=41): 204 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(74(a,1),8(a,1,2,1,2,2,1,1,1)),rewrite(74(11),175(15),74(10),74(10))]. given #407 (F,wt=29): 5032 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(4840(a,1),234(a,1,1)),rewrite(4840(12),4840(13),82(4),4840(24),4840(25),82(16))]. given #408 (F,wt=29): 5098 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(4945(a,1),234(a,1,1)),rewrite(4945(12),4945(13),82(4),4945(24),4945(25),82(16))]. given #409 (T,wt=29): 5565 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(57(a,1),4211(a,1,2,2,1,1)),rewrite(82(7),82(10),82(16))]. given #410 (T,wt=29): 5568 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(4211(a,1),88(a,1,2,1)),rewrite(4211(24),82(14),4211(24))]. given #411 (A,wt=43): 211 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(141(a,1),6(a,1,1)),rewrite(210(4),210(5),210(6),82(4),210(5),210(6),82(4),210(6),210(7),82(5),210(8),210(10),116(11),210(6),210(7),82(5),210(7),210(8),82(6),210(9),210(11),210(16),210(18),210(23))]. given #412 (F,wt=29): 5690 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(22(a,1),5640(a,1,1,1,2)),rewrite(82(6),82(9),82(16))]. given #413 (F,wt=29): 5694 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(22(a,1),5641(a,1,2,1,2)),rewrite(82(7),82(10),82(16))]. given #414 (T,wt=29): 5715 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(22(a,1),5691(a,1,1,1,2)),rewrite(82(6),82(9),82(16))]. given #415 (T,wt=29): 5722 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(4212(a,1),88(a,1,2,1)),rewrite(4212(24),82(14),4212(24))]. given #416 (A,wt=55): 215 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(z,v),v),f(y,z)),z))))) = f(y,z). [para(11(a,1),9(a,1,1,2)),rewrite(11(24),11(25),11(28),11(32),11(47))]. given #417 (F,wt=31): 287 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(202(a,1),3(a,1,2,2,1,1,1)),rewrite(202(10))]. given #418 (F,wt=31): 367 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(22(a,1),37(a,1,2,2,1,1,1)),rewrite(88(4))]. given #419 (T,wt=31): 373 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(88(a,1),37(a,1,2,2,2))]. given #420 (T,wt=31): 422 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(22(a,1),38(a,1,2,2,1,1,1))]. given #421 (A,wt=49): 216 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)),x))) = f(y,x). [para(22(a,1),11(a,1,1,1,2,1,1,1))]. given #422 (F,wt=31): 423 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(48(a,1),38(a,1,2,2,1,1,1))]. given #423 (F,wt=31): 434 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(38(a,1),227(a,1,1)),rewrite(38(15),38(16),82(4),38(28),38(29),82(17))]. given #424 (T,wt=31): 452 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(82(a,1),41(a,1,1)),rewrite(82(3),97(4))]. given #425 (T,wt=31): 521 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(82(a,1),46(a,1,2,2,1,1))]. given #426 (A,wt=57): 218 f(f(f(f(f(x,x),y),f(f(f(f(y,y),y),x),f(x,z))),f(f(y,y),x)),f(f(f(f(f(y,y),x),f(f(y,y),x)),u),f(f(f(f(x,u),u),f(f(y,y),x)),x))) = f(f(y,y),x). [para(48(a,1),11(a,1,1,1,2,1,1,1))]. Demod_limit: f(f(f(f(f(f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w))))),f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w)))))),x),f(f(f(f(x,x),x),f(f(x,x),x)),f(f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w))))),v6))),f(f(x,x),f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w))))))),f(f(f(f(f(x,x),f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w)))))),f(f(x,x),f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w))))))),v7),f(f(f(f(f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w))))),v7),v7),f(f(x,x),f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w))))))),f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w)))))))) = f(f(x,x),f(f(f(f(x,x),x),y),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),f(z,f(f(x,x),x))),y),y),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),u),f(f(f(f(f(f(f(f(x,x),x),f(f(x,x),x)),v),u),u),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(f(x,x),x)),w)))))). [para(49(a,1),218(a,1,1,1,2,1))]. Demod_limit (steps=-1, size=1001). The most recent kept clause is 6156. From here on, a short message will be printed for each 100 times the limit is hit. given #427 (F,wt=31): 678 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(82(a,1),102(a,1,1)),rewrite(82(3))]. given #428 (F,wt=31): 684 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(88(a,1),102(a,1,2,2,1,1,1,1))]. given #429 (T,wt=31): 688 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(97(a,1),102(a,1,2,2,1,1,1,1))]. given #430 (T,wt=31): 692 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(74(a,1),102(a,1,2,2,1,1,1)),rewrite(74(10))]. given #431 (A,wt=51): 219 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)),x))) = f(y,x). [para(82(a,1),11(a,1,1,1,2,1,1))]. given #432 (F,wt=25): 6274 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(88(a,1),692(a,1,2))]. given #433 (F,wt=25): 6300 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(88(a,1),6274(a,1,2,1,2,2,2))]. given #434 (T,wt=31): 706 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(202(a,1),102(a,1,2,2,1,1,1)),rewrite(202(10))]. given #435 (T,wt=31): 803 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(22(a,1),457(a,1,1)),rewrite(82(3),88(4))]. given #436 (A,wt=47): 220 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)),x))) = f(z,x). [para(82(a,1),11(a,1,2,2,1,1))]. given #437 (F,wt=31): 804 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(22(a,1),457(a,1,2,1,1))]. given #438 (F,wt=31): 807 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(82(a,1),457(a,1,1)),rewrite(82(3),97(4))]. given #439 (T,wt=31): 858 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(22(a,1),636(a,1,2,1,1))]. given #440 (T,wt=31): 878 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(88(a,1),649(a,1,1,1)),rewrite(82(8))]. given #441 (A,wt=33): 221 f(f(f(f(f(x,y),f(x,y)),z),f(f(f(f(y,z),z),f(x,y)),y)),f(f(x,y),f(x,y))) = f(x,y). [para(11(a,1),88(a,1,2,1)),rewrite(11(33),11(36))]. given #442 (F,wt=31): 879 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(97(a,1),649(a,1,1,1)),rewrite(82(8))]. given #443 (F,wt=31): 937 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(88(a,1),663(a,1,1,1)),rewrite(82(8))]. given #444 (T,wt=31): 938 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(97(a,1),663(a,1,1,1)),rewrite(82(8))]. given #445 (T,wt=31): 1327 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(86(a,1),227(a,1,1)),rewrite(86(12),86(12),86(25),86(25))]. given #446 (A,wt=49): 222 f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),x))) = f(z,x). [para(88(a,1),11(a,1,1,1,2,2))]. given #447 (F,wt=31): 1550 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(680(a,1),227(a,1,1)),rewrite(680(12),680(12),680(25),680(25))]. given #448 (F,wt=31): 1900 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(1131(a,1),234(a,1,1)),rewrite(1131(12),1131(12),1131(25),1131(25))]. given #449 (T,wt=31): 1904 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(1211(a,1),234(a,1,1)),rewrite(1211(12),1211(12),1211(25),1211(25))]. given #450 (T,wt=31): 2324 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(82(a,1),89(a,1,2,2,1,1))]. given #451 (A,wt=55): 224 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(210(a,1),3(a,1,1)),rewrite(57(13))]. given #452 (F,wt=31): 2418 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(2380(a,1),87(a,1,2,2,1,1,1)),rewrite(576(6),57(12),1034(16))]. given #453 (F,wt=31): 2451 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(2381(a,1),87(a,1,2,2,1,1,1)),rewrite(590(6),57(12),1052(16))]. given #454 (T,wt=31): 2528 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. [back_rewrite(2446),rewrite(2491(5))]. given #455 (T,wt=31): 2824 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(2815(a,1),3(a,1,2,2,1,1,1)),rewrite(2815(10))]. given #456 (A,wt=33): 225 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(210(a,1),3(a,1,2,1)),rewrite(82(4),82(5),82(9))]. given #457 (F,wt=31): 2832 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(2815(a,1),102(a,1,2,2,1,1,1)),rewrite(2815(10))]. given #458 (F,wt=25): 6645 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(88(a,1),2832(a,1,2))]. given #459 (T,wt=31): 2865 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(2856(a,1),3(a,1,2,2,1,1,1)),rewrite(2856(10))]. given #460 (T,wt=31): 2876 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(2856(a,1),102(a,1,2,2,1,1,1)),rewrite(2856(10))]. given #461 (A,wt=51): 226 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(210(a,1),3(a,1,2,2,1,1,1))]. given #462 (F,wt=25): 6695 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(88(a,1),2876(a,1,2))]. given #463 (F,wt=31): 2988 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(65(a,1),597(a,1,1,1,1)),rewrite(65(11),65(12),65(13),65(13),65(24),65(24))]. given #464 (T,wt=31): 2993 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(636(a,1),597(a,1,1,1,1)),rewrite(636(11),636(12),636(13),636(13),636(24),636(24))]. given #465 (T,wt=31): 3010 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(82(a,1),100(a,1,2,2,1,1,1))]. given #466 (A,wt=49): 228 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(210(a,1),9(a,1,1)),rewrite(57(13))]. given #467 (F,wt=31): 3050 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(1589(a,1),602(a,1,1,1,1)),rewrite(1589(10),1589(11),1589(12),1589(12),1589(23),1589(23))]. given #468 (F,wt=31): 3051 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(1590(a,1),602(a,1,1,1,1)),rewrite(1590(10),1590(11),1590(12),1590(12),1590(23),1590(23))]. given #469 (T,wt=31): 3052 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(1598(a,1),602(a,1,1,1,1)),rewrite(1598(10),1598(11),1598(12),1598(12),1598(23),1598(23))]. given #470 (T,wt=31): 3053 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(1624(a,1),602(a,1,1,1,1)),rewrite(1624(10),1624(11),1624(12),1624(12),1624(23),1624(23))]. given #471 (A,wt=53): 229 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(210(a,1),9(a,1,2,1)),rewrite(82(9),82(12),82(19))]. given #472 (F,wt=31): 3058 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(793(a,1),602(a,1,1,1,1)),rewrite(793(12),82(3),793(11),793(13),793(14),82(5),793(25),793(26),82(17))]. given #473 (F,wt=31): 3059 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(933(a,1),602(a,1,1,1,1)),rewrite(933(12),82(3),933(11),933(13),933(14),82(5),933(25),933(26),82(17))]. given #474 (T,wt=31): 3086 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(3045(a,1),100(a,1,2,2,1,1,1)),rewrite(278(7),82(5),82(16))]. given #475 (T,wt=23): 6863 f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(f(x,x),z))) = x. [para(3086(a,1),47(a,1,2,2,1)),rewrite(231(39),48(35),82(13)),flip(a)]. given #476 (A,wt=49): 230 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(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y. [para(210(a,1),10(a,1,2,1)),rewrite(82(4),82(5),82(9))]. given #477 (F,wt=23): 6874 f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(x,f(f(x,x),z))) = x. [para(88(a,1),6863(a,1,1,2,2,2,2))]. given #478 (F,wt=23): 6875 f(f(x,f(x,f(x,f(x,f(f(x,x),y))))),f(x,f(z,f(x,x)))) = x. [para(88(a,1),6863(a,1,2,2))]. given #479 (T,wt=23): 6882 f(f(x,f(x,f(x,f(x,f(y,f(x,x)))))),f(x,f(z,f(x,x)))) = x. [para(88(a,1),6874(a,1,2,2))]. given #480 (T,wt=31): 3363 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(22(a,1),707(a,1,2,1)),rewrite(82(4),82(17))]. given #481 (A,wt=57): 236 f(f(f(x,f(f(f(f(f(x,y),f(x,f(f(x,x),z))),f(x,f(f(x,x),z))),x),f(x,u))),f(y,x)),f(f(f(f(y,x),f(y,x)),v),f(f(f(f(x,v),v),f(y,x)),x))) = f(y,x). [para(210(a,1),11(a,1,1,1,1)),rewrite(82(3),82(4),82(8))]. given #482 (F,wt=31): 3429 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(65(a,1),1073(a,1,1,1,1)),rewrite(65(11),65(12),65(12),65(23),65(23),65(25))]. given #483 (F,wt=31): 3434 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(636(a,1),1073(a,1,1,1,1)),rewrite(636(11),636(12),636(12),636(23),636(23),636(25))]. given #484 (T,wt=31): 3467 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(1589(a,1),1076(a,1,1,1,1)),rewrite(1589(10),1589(11),1589(11),1589(22),1589(22),1589(24))]. given #485 (T,wt=31): 3468 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(1590(a,1),1076(a,1,1,1,1)),rewrite(1590(10),1590(11),1590(11),1590(22),1590(22),1590(24))]. given #486 (A,wt=51): 238 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(231(a,1),3(a,1,1)),rewrite(82(13))]. given #487 (F,wt=31): 3469 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(1598(a,1),1076(a,1,1,1,1)),rewrite(1598(10),1598(11),1598(11),1598(22),1598(22),1598(24))]. given #488 (F,wt=31): 3470 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(1624(a,1),1076(a,1,1,1,1)),rewrite(1624(10),1624(11),1624(11),1624(22),1624(22),1624(24))]. given #489 (T,wt=31): 3475 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(793(a,1),1076(a,1,1,1,1)),rewrite(793(12),82(3),793(11),793(12),82(3),793(23),793(24),82(15),793(24))]. given #490 (T,wt=31): 3476 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(933(a,1),1076(a,1,1,1,1)),rewrite(933(12),82(3),933(11),933(12),82(3),933(23),933(24),82(15),933(24))]. given #491 (A,wt=47): 240 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(231(a,1),9(a,1,1)),rewrite(82(13))]. given #492 (F,wt=31): 3634 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(3509(a,1),770(a,1,1,2,1,1,1)),rewrite(82(3),82(18),82(15))]. given #493 (F,wt=31): 3635 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(3509(a,1),956(a,1,1,2,1,1,1)),rewrite(82(3),82(18),82(15))]. given #494 (T,wt=31): 3639 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(3509(a,1),90(a,1,2,1,2,1)),rewrite(3509(25),278(17),3509(22),2498(15),82(15),48(13))]. given #495 (T,wt=31): 3727 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(3510(a,1),767(a,1,1,2,1)),rewrite(3719(19))]. given #496 (A,wt=43): 242 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,z),f(f(f(f(f(f(x,x),u),z),z),f(x,x)),f(f(x,x),v)))))) = f(x,x). [para(231(a,1),10(a,1,2,2,1,1,1,1)),rewrite(82(5),82(3),82(8))]. given #497 (F,wt=31): 3728 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(3510(a,1),954(a,1,1,2,1)),rewrite(3719(19))]. given #498 (F,wt=31): 3740 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(3606(a,1),770(a,1,1,2,1,1,1)),rewrite(82(3),82(18),82(15))]. given #499 (T,wt=31): 3741 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(3606(a,1),956(a,1,1,2,1,1,1)),rewrite(82(3),82(18),82(15))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 70 (0.00 of 60.92 sec). given #500 (T,wt=31): 3745 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(3606(a,1),90(a,1,2,1,2,1)),rewrite(3606(25),278(17),3606(22),2498(15),82(15),48(13))]. given #501 (A,wt=55): 246 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(235(a,1),3(a,1,1)),rewrite(57(13))]. given #502 (F,wt=31): 3760 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(3607(a,1),767(a,1,1,2,1)),rewrite(3752(19))]. given #503 (F,wt=31): 3761 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(3607(a,1),954(a,1,1,2,1)),rewrite(3752(19))]. given #504 (T,wt=31): 3820 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(3499(a,1),234(a,1,1)),rewrite(3499(12),3499(12),3499(25),3499(25))]. given #505 (T,wt=31): 3829 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(3500(a,1),234(a,1,1)),rewrite(3500(12),3500(12),3500(25),3500(25))]. given #506 (A,wt=33): 247 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(235(a,1),3(a,1,2,1)),rewrite(82(4),82(5),82(9))]. given #507 (F,wt=31): 3840 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(3596(a,1),234(a,1,1)),rewrite(3596(12),3596(12),3596(25),3596(25))]. given #508 (F,wt=31): 3848 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(3597(a,1),234(a,1,1)),rewrite(3597(12),3597(12),3597(25),3597(25))]. given #509 (T,wt=31): 3875 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(3734(a,1),602(a,1,1,1,1)),rewrite(3734(12),82(3),3734(11),3734(13),3734(14),82(5),3734(25),3734(26),82(17))]. given #510 (T,wt=31): 3876 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(3734(a,1),1076(a,1,1,1,1)),rewrite(3734(12),82(3),3734(11),3734(12),82(3),3734(23),3734(24),82(15),3734(24))]. given #511 (A,wt=51): 248 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(235(a,1),3(a,1,2,2,1,1,1))]. given #512 (F,wt=31): 3895 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(3767(a,1),602(a,1,1,1,1)),rewrite(3767(12),82(3),3767(11),3767(13),3767(14),82(5),3767(25),3767(26),82(17))]. given #513 (F,wt=31): 3896 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(3767(a,1),1076(a,1,1,1,1)),rewrite(3767(12),82(3),3767(11),3767(12),82(3),3767(23),3767(24),82(15),3767(24))]. given #514 (T,wt=31): 3904 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(1129(a,1),234(a,1,1)),rewrite(1129(13),1129(14),82(4),1129(26),1129(27),82(17))]. given #515 (T,wt=31): 3943 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(1210(a,1),234(a,1,1)),rewrite(1210(13),1210(14),82(4),1210(26),1210(27),82(17))]. given #516 (A,wt=49): 249 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(235(a,1),9(a,1,1)),rewrite(57(13))]. given #517 (F,wt=31): 4006 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(65(a,1),1413(a,1,1,1)),rewrite(65(11),65(11),65(13),65(13),65(24),65(24))]. given #518 (F,wt=31): 4011 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(636(a,1),1413(a,1,1,1)),rewrite(636(11),636(11),636(13),636(13),636(24),636(24))]. given #519 (T,wt=31): 4035 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(1341(a,1),1413(a,1,1,1)),rewrite(1341(13),1341(13),1341(15),1341(15),1341(26),1341(26))]. given #520 (T,wt=31): 4036 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(1343(a,1),1413(a,1,1,1)),rewrite(1343(13),1343(13),1343(15),1343(15),1343(26),1343(26))]. given #521 (A,wt=53): 250 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(235(a,1),9(a,1,2,1)),rewrite(82(9),82(12),82(19))]. given #522 (F,wt=31): 4044 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(1598(a,1),1420(a,1,1,1)),rewrite(1598(10),1598(10),1598(12),1598(12),1598(23),1598(23))]. given #523 (F,wt=31): 4045 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(1624(a,1),1420(a,1,1,1)),rewrite(1624(10),1624(10),1624(12),1624(12),1624(23),1624(23))]. given #524 (T,wt=31): 4050 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(793(a,1),1420(a,1,1,1)),rewrite(793(12),793(13),82(4),793(13),793(14),82(5),793(25),793(26),82(17))]. given #525 (T,wt=31): 4051 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(933(a,1),1420(a,1,1,1)),rewrite(933(12),933(13),82(4),933(13),933(14),82(5),933(25),933(26),82(17))]. given #526 (A,wt=49): 251 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(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y. [para(235(a,1),10(a,1,2,1)),rewrite(82(4),82(5),82(9))]. given #527 (F,wt=31): 4073 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(3734(a,1),1420(a,1,1,1)),rewrite(3734(12),3734(13),82(4),3734(13),3734(14),82(5),3734(25),3734(26),82(17))]. given #528 (F,wt=31): 4074 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(3767(a,1),1420(a,1,1,1)),rewrite(3767(12),3767(13),82(4),3767(13),3767(14),82(5),3767(25),3767(26),82(17))]. given #529 (T,wt=31): 4377 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(654(a,1),2526(a,1,1,1)),rewrite(654(10),654(11),654(11),654(11),654(12),654(24))]. given #530 (T,wt=31): 4388 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(1589(a,1),2526(a,1,1,1)),rewrite(1589(10),1589(11),1589(11),1589(11),1589(12),1589(24))]. given #531 (A,wt=57): 253 f(f(f(x,f(f(f(f(f(x,y),f(x,f(z,f(x,x)))),f(x,f(z,f(x,x)))),x),f(x,u))),f(y,x)),f(f(f(f(y,x),f(y,x)),v),f(f(f(f(x,v),v),f(y,x)),x))) = f(y,x). [para(235(a,1),11(a,1,1,1,1)),rewrite(82(3),82(4),82(8))]. given #532 (F,wt=31): 4389 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(1590(a,1),2526(a,1,1,1)),rewrite(1590(10),1590(11),1590(11),1590(11),1590(12),1590(24))]. given #533 (F,wt=31): 4390 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(1598(a,1),2526(a,1,1,1)),rewrite(1598(10),1598(11),1598(11),1598(11),1598(12),1598(24))]. given #534 (T,wt=31): 4391 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(1624(a,1),2526(a,1,1,1)),rewrite(1624(10),1624(11),1624(11),1624(11),1624(12),1624(24))]. given #535 (T,wt=31): 4728 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(22(a,1),4654(a,1,2,1,1,2,1)),rewrite(82(10))]. given #536 (A,wt=51): 254 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(244(a,1),3(a,1,1)),rewrite(82(13))]. given #537 (F,wt=31): 4760 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(1028(a,1),4654(a,1,1))]. given #538 (F,wt=31): 4761 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(1036(a,1),4654(a,1,1))]. given #539 (T,wt=31): 4786 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(1722(a,1),4654(a,1,1))]. given #540 (T,wt=27): 7621 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(4786(a,1),46(a,1,2,2,1)),rewrite(22(39),57(14)),flip(a)]. given #541 (A,wt=47): 256 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(244(a,1),9(a,1,1)),rewrite(82(13))]. given #542 (F,wt=29): 7627 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(7621(a,1),234(a,1,1)),rewrite(7621(12),7621(13),82(4),7621(24),7621(25),82(16))]. given #543 (F,wt=31): 4859 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(4743(a,1),602(a,1,1,1,1)),rewrite(4743(10),4743(11),4743(12),4743(12),4743(23),4743(23))]. given #544 (T,wt=31): 4860 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(4743(a,1),1076(a,1,1,1,1)),rewrite(4743(10),4743(11),4743(11),4743(22),4743(22),4743(24))]. given #545 (T,wt=31): 4861 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(4743(a,1),1420(a,1,1,1)),rewrite(4743(10),4743(10),4743(12),4743(12),4743(23),4743(23))]. given #546 (A,wt=57): 262 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(f(f(y,x),f(y,x)),u),f(f(f(f(f(f(y,x),v),u),u),f(y,x)),x))))) = f(y,x). [para(22(a,1),12(a,1,2,2,1,1,1,1))]. given #547 (F,wt=31): 4862 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(4743(a,1),2526(a,1,1,1)),rewrite(4743(10),4743(11),4743(11),4743(11),4743(12),4743(24))]. given #548 (F,wt=31): 4867 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(22(a,1),128(a,1,2,2,1,1,1))]. given #549 (T,wt=31): 4965 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(4922(a,1),602(a,1,1,1,1)),rewrite(4922(10),4922(11),4922(12),4922(12),4922(23),4922(23))]. given #550 (T,wt=31): 4966 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(4922(a,1),1076(a,1,1,1,1)),rewrite(4922(10),4922(11),4922(11),4922(22),4922(22),4922(24))]. given #551 (A,wt=57): 263 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)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),v),u),u),f(y,z)),z))))) = f(y,z). [para(22(a,1),12(a,1,2,2,1,1,1))]. given #552 (F,wt=31): 4967 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(4922(a,1),1420(a,1,1,1)),rewrite(4922(10),4922(10),4922(12),4922(12),4922(23),4922(23))]. given #553 (F,wt=31): 4968 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(4922(a,1),2526(a,1,1,1)),rewrite(4922(10),4922(11),4922(11),4922(11),4922(12),4922(24))]. given #554 (T,wt=31): 5038 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(4840(a,1),602(a,1,1,1,1)),rewrite(4840(12),82(3),4840(11),4840(13),4840(14),82(5),4840(25),4840(26),82(17))]. given #555 (T,wt=31): 5039 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(4840(a,1),1076(a,1,1,1,1)),rewrite(4840(12),82(3),4840(11),4840(12),82(3),4840(23),4840(24),82(15),4840(24))]. given #556 (A,wt=57): 264 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)),f(v,v)),f(f(f(v,f(v,v)),f(y,z)),z))))) = f(y,z). [para(22(a,1),12(a,1,2,2,2,2,1,1,1))]. given #557 (F,wt=31): 5040 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(4840(a,1),1420(a,1,1,1)),rewrite(4840(12),4840(13),82(4),4840(13),4840(14),82(5),4840(25),4840(26),82(17))]. given #558 (F,wt=31): 5104 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(4945(a,1),602(a,1,1,1,1)),rewrite(4945(12),82(3),4945(11),4945(13),4945(14),82(5),4945(25),4945(26),82(17))]. given #559 (T,wt=31): 5105 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(4945(a,1),1076(a,1,1,1,1)),rewrite(4945(12),82(3),4945(11),4945(12),82(3),4945(23),4945(24),82(15),4945(24))]. given #560 (T,wt=31): 5106 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(4945(a,1),1420(a,1,1,1)),rewrite(4945(12),4945(13),82(4),4945(13),4945(14),82(5),4945(25),4945(26),82(17))]. given #561 (A,wt=57): 265 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)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),v),u),u),f(y,z)),z))))) = f(y,z). [para(48(a,1),12(a,1,2,2,1,1,1))]. given #562 (F,wt=31): 5249 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(3458(a,1),234(a,1,1)),rewrite(3458(13),3458(14),82(4),3458(26),3458(27),82(17))]. given #563 (F,wt=31): 5263 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(3459(a,1),234(a,1,1)),rewrite(3459(13),3459(14),82(4),3459(26),3459(27),82(17))]. given #564 (T,wt=31): 5320 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(3471(a,1),234(a,1,1)),rewrite(3471(13),3471(14),82(4),3471(26),3471(27),82(17))]. given #565 (T,wt=31): 5334 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(3472(a,1),234(a,1,1)),rewrite(3472(13),3472(14),82(4),3472(26),3472(27),82(17))]. given #566 (A,wt=55): 266 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(v,v),v),f(y,z)),z))))) = f(y,z). [para(48(a,1),12(a,1,2,2,2,2,1,1,1))]. given #567 (F,wt=31): 5350 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(3473(a,1),234(a,1,1)),rewrite(3473(13),3473(14),82(4),3473(26),3473(27),82(17))]. given #568 (F,wt=31): 5364 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(3474(a,1),234(a,1,1)),rewrite(3474(13),3474(14),82(4),3474(26),3474(27),82(17))]. given #569 (T,wt=31): 5593 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(1909(a,1),4211(a,1,2,2,1,1))]. given #570 (T,wt=31): 5594 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(2033(a,1),4211(a,1,2,2,1,1))]. given #571 (A,wt=59): 267 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)),f(y,z)),f(f(f(f(y,z),f(y,z)),f(y,z)),z))))) = f(y,z). [para(57(a,1),12(a,1,2,2,2,2,1,1))]. given #572 (F,wt=31): 5747 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(1909(a,1),4212(a,1,2,2,1,1))]. given #573 (F,wt=31): 5748 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(2033(a,1),4212(a,1,2,2,1,1))]. given #574 (T,wt=31): 5897 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(3460(a,1),200(a,1,1,1)),rewrite(3460(8),82(3),3460(7),3460(8),82(3),3460(7),3460(9),3460(10),82(5),3460(9),3460(20))]. given #575 (T,wt=31): 5898 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(3461(a,1),200(a,1,1,1)),rewrite(3461(8),82(3),3461(7),3461(8),82(3),3461(7),3461(9),3461(10),82(5),3461(9),3461(20))]. given #576 (A,wt=57): 268 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(f(f(x,y),f(x,y)),u),f(f(f(f(f(f(x,y),v),u),u),f(x,y)),y))))) = f(x,y). [para(82(a,1),12(a,1,2,2,1,1,1,1))]. given #577 (F,wt=31): 5976 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(1909(a,1),5568(a,1,1,2,1,1))]. given #578 (F,wt=31): 5977 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(2033(a,1),5568(a,1,1,2,1,1))]. given #579 (T,wt=31): 6026 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(1909(a,1),5722(a,1,1,2,1,1))]. given #580 (T,wt=31): 6027 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(2033(a,1),5722(a,1,1,2,1,1))]. given #581 (A,wt=55): 269 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(y,v),v),f(y,z)),z))))) = f(y,z). [para(82(a,1),12(a,1,2,2,2,2,1,1,1,1))]. given #582 (F,wt=31): 6145 f(f(f(f(f(x,y),f(x,y)),f(y,y)),f(f(y,f(x,y)),y)),f(f(x,y),f(x,y))) = f(x,y). [para(521(a,1),88(a,1,2,1)),rewrite(521(23),521(26))]. given #583 (F,wt=31): 6180 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(82(a,1),684(a,1,2,2,1,1,1))]. given #584 (T,wt=31): 6225 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(22(a,1),688(a,1,2,2,1,1,1))]. given #585 (T,wt=31): 6298 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(22(a,1),6274(a,1,1)),rewrite(82(4),82(6))]. given #586 (A,wt=59): 270 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(f(w,f(y,z)),v),v),f(y,z)),z))))) = f(y,z). [para(88(a,1),12(a,1,2,2,2,2,1,1,1,1))]. given #587 (F,wt=31): 6322 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(22(a,1),6300(a,1,1)),rewrite(82(4),82(6))]. given #588 (F,wt=31): 6490 f(f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),y)),f(f(x,y),f(x,y))) = f(x,y). [para(2324(a,1),88(a,1,2,1)),rewrite(2324(23),2324(26))]. given #589 (T,wt=31): 6873 f(f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))),f(f(x,x),f(x,z))) = f(x,x). [para(22(a,1),6863(a,1,1,2,2,2,2,1)),rewrite(82(13))]. given #590 (T,wt=31): 6881 f(f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))),f(f(x,x),f(x,z))) = f(x,x). [para(22(a,1),6874(a,1,1,2,2,2,2,2)),rewrite(82(13))]. given #591 (A,wt=53): 271 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(f(f(y,y),y),f(f(f(y,y),y),f(y,w)))))))) = y. [para(74(a,1),12(a,1,1,2)),rewrite(74(10),74(10),74(12),74(15),74(16),74(16),74(18),74(21),74(34))]. given #592 (F,wt=31): 6883 f(f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(x,y))))),f(f(x,x),f(z,x))) = f(x,x). [para(22(a,1),6875(a,1,1,2,2,2,2,1)),rewrite(82(13))]. given #593 (F,wt=31): 6884 f(f(f(x,x),f(f(x,x),f(f(x,x),f(f(x,x),f(y,x))))),f(f(x,x),f(z,x))) = f(x,x). [para(22(a,1),6882(a,1,1,2,2,2,2,2)),rewrite(82(13))]. given #594 (T,wt=31): 7622 f(f(f(f(f(x,x),f(f(x,x),f(x,f(x,x)))),f(x,f(x,x))),f(x,f(x,x))),f(x,x)) = x. [para(4786(a,1),67(a,1,2,2,1)),rewrite(82(5),82(9),82(12),82(20),82(24),82(27),82(34),82(38),82(41),82(49),48(47),82(17),82(5),82(9),82(12)),flip(a)]. given #595 (T,wt=31): 7633 f(f(x,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(7621(a,1),602(a,1,1,1,1)),rewrite(7621(12),82(3),7621(11),7621(13),7621(14),82(5),7621(25),7621(26),82(17))]. given #596 (A,wt=45): 273 f(f(x,f(f(y,y),y)),f(f(f(y,y),y),f(f(f(f(f(f(f(y,y),y),x),y),y),f(f(y,y),y)),f(f(f(y,y),y),z)))) = f(f(y,y),y). [para(260(a,1),3(a,1,2,1))]. given #597 (F,wt=31): 7634 f(f(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) = f(x,x). [para(7621(a,1),1076(a,1,1,1,1)),rewrite(7621(12),82(3),7621(11),7621(12),82(3),7621(23),7621(24),82(15),7621(24))]. given #598 (F,wt=31): 7635 f(f(f(x,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(7621(a,1),1420(a,1,1,1)),rewrite(7621(12),7621(13),82(4),7621(13),7621(14),82(5),7621(25),7621(26),82(17))]. given #599 (T,wt=31): 8049 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(5897(a,1),88(a,1,2,1)),rewrite(5897(26),82(15),5897(26))]. given #600 (T,wt=31): 8071 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(5898(a,1),88(a,1,2,1)),rewrite(5898(26),82(15),5898(26))]. given #601 (A,wt=47): 275 f(f(f(f(x,y),f(x,y)),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(f(f(f(x,y),f(x,y)),f(x,y)),z),z),f(x,y)),y))) = f(x,y). [para(260(a,1),9(a,1,1)),rewrite(88(22))]. given #602 (F,wt=33): 319 f(f(x,f(x,x)),f(f(x,y),f(f(f(f(f(x,f(x,x)),y),y),f(x,x)),f(f(x,x),z)))) = f(x,x). [para(278(a,1),3(a,1,1)),rewrite(82(5),88(10))]. given #603 (F,wt=33): 429 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(88(a,1),38(a,1,2,2,2))]. given #604 (T,wt=33): 454 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)),y))) = f(y,z). [para(82(a,1),41(a,1,2,2,2))]. given #605 (T,wt=9): 8394 f(f(x,x),f(x,y)) = x. [para(210(a,1),454(a,1,1)),rewrite(1349(16),82(13),48(11),82(3)),flip(a)]. given #606 (A,wt=57): 303 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(f(f(y,y),v),f(f(f(f(f(y,w),v),v),y),f(y,v6))),u),u),y),f(y,v7)))))) = y. [para(3(a,1),13(a,1,1,2)),rewrite(3(12),3(12),3(14),3(17),3(18),3(18),3(31),3(32),3(38))]. given #607 (F,wt=9): 8396 f(f(x,x),f(y,x)) = x. [para(235(a,1),454(a,1,1)),rewrite(1392(16),8394(13),48(11),8394(3)),flip(a)]. given #608 (F,wt=11): 8395 f(x,f(f(x,x),y)) = f(x,x). [para(231(a,1),454(a,1,1)),rewrite(8394(10),8394(12),1330(14),22(10)),flip(a)]. given #609 (T,wt=11): 8397 f(x,f(y,f(x,x))) = f(x,x). [para(244(a,1),454(a,1,1)),rewrite(8394(10),8394(12),1359(14),22(10)),flip(a)]. given #610 (T,wt=11): 8888 f(f(x,x),x) = f(x,f(x,x)). [back_rewrite(4109),rewrite(8402(11),8397(3))]. given #611 (A,wt=57): 306 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)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(z,u),u),f(y,z)),f(f(y,z),v)))))) = f(y,z). [para(22(a,1),13(a,1,2,2,1,1,1))]. given #612 (F,wt=13): 8398 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(227(a,1),454(a,1,1)),rewrite(1413(26),8394(23),48(18),8394(7)),flip(a)]. given #613 (F,wt=13): 8400 f(f(f(x,y),f(x,y)),x) = f(x,y). [para(234(a,1),454(a,1,1)),rewrite(1420(26),8394(23),48(18),8394(7)),flip(a)]. given #614 (T,wt=21): 9188 f(x,f(f(y,x),f(f(f(x,f(x,x)),f(y,x)),x))) = f(y,x). [back_rewrite(8588),rewrite(8888(3))]. given #615 (T,wt=21): 9192 f(x,f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),y))) = f(x,y). [back_rewrite(8566),rewrite(8888(3))]. given #616 (A,wt=57): 310 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)),f(z,z)),f(f(z,f(y,z)),f(f(y,z),v)))))) = f(y,z). [para(82(a,1),13(a,1,2,2,2,2,1,1))]. given #617 (F,wt=21): 9628 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))),f(x,x)) = x. [back_rewrite(285),rewrite(8888(2),8888(4))]. given #618 (F,wt=21): 9637 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x)))) = x. [back_rewrite(202),rewrite(8888(3),8888(5))]. given #619 (T,wt=21): 9638 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x)) = x. [back_rewrite(201),rewrite(8888(2),8888(4))]. given #620 (T,wt=21): 9646 f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y)))) = x. [back_rewrite(74),rewrite(8888(3),8888(5))]. given #621 (A,wt=55): 311 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(z,v),v),f(y,z)),y))))) = f(y,z). [para(82(a,1),13(a,1,2,2,2,2,2))]. given #622 (F,wt=21): 9706 f(x,f(f(x,y),f(f(f(x,f(x,x)),f(x,y)),x))) = f(x,y). [para(8394(a,1),454(a,1,1)),rewrite(8394(6),8400(4),8394(5),8888(3))]. given #623 (F,wt=21): 9773 f(x,f(f(y,x),f(f(f(x,f(x,x)),f(y,x)),y))) = f(y,x). [para(8396(a,1),454(a,1,1)),rewrite(8394(6),8398(4),8394(5),8888(3))]. given #624 (T,wt=23): 9157 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)). [back_rewrite(8681),rewrite(8888(6),8398(11))]. given #625 (T,wt=23): 9216 f(f(x,y),f(f(f(f(x,y),f(x,f(x,x))),f(x,f(x,x))),x)) = x. [back_rewrite(8483),rewrite(8888(4),8888(7))]. given #626 (A,wt=59): 312 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),f(f(f(f(y,z),f(y,z)),v),f(f(f(f(z,v),v),f(y,z)),f(w,f(y,z))))))) = f(y,z). [para(88(a,1),13(a,1,2,2,2,2,2))]. given #627 (F,wt=23): 9217 f(f(x,y),f(f(f(f(x,y),f(y,f(y,y))),f(y,f(y,y))),y)) = y. [back_rewrite(8481),rewrite(8888(4),8888(7))]. given #628 (F,wt=23): 9233 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [back_rewrite(8414),rewrite(8888(5))]. given #629 (T,wt=23): 9235 f(f(x,x),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [back_rewrite(8412),rewrite(8888(5))]. given #630 (T,wt=23): 9397 f(f(x,y),f(f(f(f(y,x),f(y,f(y,y))),f(y,f(y,y))),y)) = y. [back_rewrite(4654),rewrite(8888(4),8888(7))]. given #631 (A,wt=39): 314 f(x,f(f(x,y),f(f(f(f(x,y),y),f(x,x)),f(f(x,z),f(f(f(f(x,z),z),f(x,x)),f(f(x,x),u)))))) = f(x,x). [para(74(a,1),13(a,1,2,2,1,1,1,1)),rewrite(201(9),82(3),82(8))]. given #632 (F,wt=23): 9601 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x))),f(x,x)) = x. [back_rewrite(654),rewrite(8888(4))]. given #633 (F,wt=23): 9610 f(f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z))),f(x,x)) = x. [back_rewrite(634),rewrite(8888(4))]. given #634 (T,wt=25): 8436 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))) = x. [para(296(a,1),454(a,1,1)),rewrite(8400(26),2610(26),8394(15),57(13),8394(3)),flip(a)]. given #635 (T,wt=25): 8437 f(f(x,x),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(460(a,1),454(a,1,1)),rewrite(8400(26),4004(26),8394(15),57(13),8394(3)),flip(a)]. given #636 (A,wt=45): 328 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(198(a,1),9(a,1,1,2)),rewrite(198(11),198(12),82(5),198(12),198(16),198(29))]. given #637 (F,wt=25): 8440 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u)))) = y. [para(100(a,1),454(a,2)),rewrite(8398(4),8398(16),8398(27),8398(43),8398(55),454(55))]. given #638 (F,wt=25): 8445 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(u,x)))) = x. [para(707(a,1),454(a,1,1)),rewrite(8400(26),4007(26),8394(15),57(13),8394(3)),flip(a)]. given #639 (T,wt=25): 8446 f(f(x,x),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [para(813(a,1),454(a,1,1)),rewrite(8400(26),4009(26),8394(15),57(13),8394(3)),flip(a)]. given #640 (T,wt=25): 8452 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(x,u)))) = x. [para(1138(a,1),454(a,1,1)),rewrite(8400(26),4028(26),8394(15),57(13),8394(3)),flip(a)]. given #641 (A,wt=57): 329 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(198(a,1),22(a,1,1))]. given #642 (F,wt=25): 8454 f(f(x,x),f(f(f(x,x),y),f(f(f(f(f(z,x),y),y),x),f(u,x)))) = x. [para(1217(a,1),454(a,1,1)),rewrite(8400(26),4043(26),8394(15),57(13),8394(3)),flip(a)]. given #643 (F,wt=25): 8469 f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x. [para(128(a,1),454(a,2)),rewrite(8400(4),8400(16),8400(27),8400(43),8400(55),454(55))]. given #644 (T,wt=25): 8486 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x). [para(521(a,1),454(a,2)),rewrite(8396(3),8396(14),8396(24),8396(39),8396(50),454(50))]. given #645 (T,wt=25): 8488 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(u,y)))) = y. [para(684(a,1),454(a,2)),rewrite(8398(4),8398(16),8398(27),8398(43),8398(55),454(55))]. given #646 (A,wt=57): 330 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(f(f(y,y),v),f(f(f(f(f(y,w),v),v),y),f(y,v6)))))))) = y. [para(22(a,1),15(a,1,2,2,1,1,1))]. given #647 (F,wt=25): 8489 f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(u,x)))) = x. [para(688(a,1),454(a,2)),rewrite(8400(4),8400(16),8400(27),8400(43),8400(55),454(55))]. given #648 (F,wt=25): 8494 f(x,f(f(f(f(x,y),f(x,y)),f(x,x)),f(f(x,f(x,y)),y))) = f(x,y). [para(2324(a,1),454(a,2)),rewrite(8394(3),8394(14),8394(24),8394(39),8394(50),454(50))]. given #649 (T,wt=25): 8504 f(f(x,y),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [para(4867(a,1),454(a,2)),rewrite(8400(4),8400(16),8400(27),8400(43),8400(55),454(55))]. given #650 (T,wt=25): 8506 f(f(x,y),f(f(f(x,x),f(y,y)),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [para(6225(a,1),454(a,2)),rewrite(8400(4),8400(16),8400(27),8400(43),8400(55),454(55))]. given #651 (A,wt=57): 332 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),f(u,u)),f(f(f(u,f(u,u)),y),f(f(f(y,y),v),f(f(f(f(f(y,w),v),v),y),f(y,v6)))))))) = y. [para(22(a,1),15(a,1,2,2,2,2,1,1,1))]. given #652 (F,wt=25): 8508 f(f(x,y),f(f(f(f(f(x,f(x,x)),y),y),f(x,x)),f(f(x,x),z))) = x. [para(319(a,1),454(a,1,2,2,1)),rewrite(8500(12),8394(29),48(27),8394(3)),flip(a)]. given #653 (F,wt=25): 8522 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(6203),rewrite(8394(4),8394(4),8394(4))]. given #654 (T,wt=25): 8529 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(5178),rewrite(8394(4),8397(5),22(4),8394(4))]. given #655 (T,wt=25): 8540 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(4249),rewrite(8396(5),8396(4),2498(3),8400(7),8394(7))]. given #656 (A,wt=57): 333 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(f(f(y,y),f(w,w)),f(f(f(w,f(w,w)),y),f(y,v6)))))))) = y. [para(22(a,1),15(a,1,2,2,2,2,2,2,1,1,1))]. given #657 (F,wt=25): 8541 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(4246),rewrite(8396(5),8396(4),2498(3),8400(7),8394(7))]. given #658 (F,wt=25): 9084 f(f(x,f(y,y)),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(x,z)))) = x. [back_rewrite(8807),rewrite(8888(6))]. given #659 (T,wt=25): 9103 f(f(x,f(y,y)),f(f(f(x,x),y),f(f(f(y,f(y,y)),x),f(z,x)))) = x. [back_rewrite(8776),rewrite(8888(6))]. given #660 (T,wt=25): 9187 f(x,f(f(y,x),f(f(f(x,f(x,x)),f(y,x)),f(f(y,x),z)))) = f(y,x). [back_rewrite(8589),rewrite(8888(3))]. given #661 (A,wt=59): 339 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(f(f(y,y),z),f(f(f(f(f(y,u),z),z),y),f(f(f(y,y),v),f(f(f(f(f(y,w),v),v),y),f(y,v6)))))))) = y. [para(82(a,1),15(a,1,2,2,1,1))]. given #662 (F,wt=15): 11076 f(x,f(f(x,f(x,x)),f(y,x))) = f(y,x). [para(8397(a,1),9187(a,1,2,2)),rewrite(88(11))]. given #663 (F,wt=15): 11142 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y). [para(8400(a,1),11076(a,1,2,2)),rewrite(8400(9))]. given #664 (T,wt=19): 11140 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = x. [para(8394(a,1),11076(a,1,2,2)),rewrite(8394(11))]. given #665 (T,wt=19): 11141 f(f(x,y),f(f(f(x,y),f(f(x,y),f(x,y))),y)) = y. [para(8396(a,1),11076(a,1,2,2)),rewrite(8396(11))]. given #666 (A,wt=59): 340 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),f(f(y,u),f(y,u))),f(f(f(y,u),y),f(f(f(y,y),v),f(f(f(f(f(y,w),v),v),y),f(y,v6)))))))) = y. [para(82(a,1),15(a,1,2,2,2,2,1,1))]. given #667 (F,wt=19): 11170 f(f(x,x),f(f(x,f(x,x)),f(y,x))) = f(x,f(x,x)). [para(11076(a,1),8541(a,1,2,2))]. given #668 (F,wt=19): 11254 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)). [para(11142(a,1),8541(a,1,2,2))]. given #669 (T,wt=19): 11328 f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,x))) = f(y,x). [para(9628(a,1),11140(a,1,1)),rewrite(9628(9),9628(9),9628(9),11226(10),11076(5)),flip(a)]. given #670 (T,wt=17): 11613 f(f(x,f(x,x)),f(f(y,x),f(y,x))) = f(y,x). [para(11328(a,1),97(a,1,2,1)),rewrite(11328(10),11328(13))]. given #671 (A,wt=59): 341 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(f(f(y,y),f(f(y,w),f(y,w))),f(f(f(y,w),y),f(y,v6)))))))) = y. [para(82(a,1),15(a,1,2,2,2,2,2,2,1,1))]. given #672 (F,wt=17): 11617 f(f(x,f(x,x)),f(y,x)) = f(f(y,x),f(y,x)). [para(11328(a,1),47(a,1,1)),rewrite(11329(24),11328(23),8397(21)),flip(a)]. given #673 (F,wt=15): 11759 f(x,f(f(y,f(y,y)),f(x,y))) = f(x,y). [para(11617(a,2),97(a,1,2))]. given #674 (T,wt=15): 11876 f(f(f(x,f(x,x)),f(y,x)),x) = f(y,x). [para(11617(a,2),90(a,1,1)),rewrite(8394(14),8888(9),8888(14),11659(16))]. given #675 (T,wt=15): 12012 f(f(f(x,f(x,x)),f(y,x)),y) = f(y,x). [para(11617(a,2),8400(a,1,1))]. given #676 (A,wt=57): 342 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(f(f(x,x),u),f(f(f(f(f(x,v),u),u),x),f(f(f(x,x),w),f(f(f(f(f(x,v6),w),w),x),f(x,v7))))))),f(x,x)) = x. [para(15(a,1),88(a,1,2,1)),rewrite(15(52),15(54))]. given #677 (F,wt=15): 12430 f(f(f(x,f(x,x)),f(x,y)),x) = f(x,y). [para(8400(a,1),11876(a,1,1,2)),rewrite(8400(9))]. given #678 (F,wt=17): 11660 f(f(f(x,y),f(x,y)),f(y,f(y,y))) = f(x,y). [para(11328(a,1),8400(a,1,1,1)),rewrite(11328(8),11328(13))]. given #679 (T,wt=17): 11687 f(x,f(f(y,x),f(f(x,f(y,x)),x))) = f(y,x). [back_rewrite(8559),rewrite(11660(6))]. given #680 (T,wt=17): 11709 f(f(f(x,y),f(f(x,y),f(x,y))),f(x,x)) = x. [para(8394(a,1),11613(a,1,2,1)),rewrite(8394(8),8394(10))]. given #681 (A,wt=57): 343 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(v,y),u),u),y),f(f(f(y,y),w),f(f(f(f(f(y,v6),w),w),y),f(y,v7)))))))) = y. [para(88(a,1),15(a,1,2,2,2,2,1,1,1,1))]. given #682 (F,wt=17): 11710 f(f(f(x,y),f(f(x,y),f(x,y))),f(y,y)) = y. [para(8396(a,1),11613(a,1,2,1)),rewrite(8396(8),8396(10))]. given #683 (F,wt=17): 11713 f(f(x,f(x,x)),f(f(x,y),f(x,y))) = f(x,y). [para(8400(a,1),11613(a,1,2,1)),rewrite(8400(7),8400(10))]. given #684 (T,wt=17): 12000 f(f(f(x,y),f(f(x,y),f(x,y))),x) = f(x,x). [para(8394(a,1),11617(a,1,2)),rewrite(8394(9),8394(9))]. given #685 (T,wt=11): 12722 f(f(x,f(x,x)),y) = f(y,y). [para(11076(a,1),12000(a,1,1,1)),rewrite(11076(6),11076(7),12715(5))]. given #686 (A,wt=57): 344 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(f(f(y,y),w),f(f(f(f(f(v6,y),w),w),y),f(y,v7)))))))) = y. [para(88(a,1),15(a,1,2,2,2,2,2,2,1,1,1,1))]. given #687 (F,wt=11): 12782 f(x,f(x,f(x,y))) = f(x,y). [back_rewrite(9203),rewrite(12715(5),8397(3),12715(6),8394(4))]. given #688 (F,wt=11): 12833 f(x,f(y,f(y,y))) = f(x,x). [back_rewrite(12510),rewrite(12715(8))]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(14306)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c_0, f ]). restricted denial: (wt=15): 15585 f(c1,f(f(c2,c3),c_0)) != f(c2,f(f(c1,c3),c_0)) # answer(A_SS). [back_rewrite(4),rewrite(14500(8,R),14500(15,R))]. given #689 (T,wt=7): 14371 f(x,f(x,x)) = c_0. [new_symbol(14306)]. given #690 (T,wt=7): 14500 f(x,c_0) = f(x,x). [back_rewrite(14215),rewrite(14371(3),14371(4),14404(5),8395(4),82(3),14371(3)),flip(a)]. given #691 (A,wt=57): 345 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(f(f(y,y),w),f(f(f(f(f(y,v6),w),w),y),f(v7,y)))))))) = y. [para(88(a,1),15(a,1,2,2,2,2,2,2,2))]. given #692 (F,wt=7): 14553 f(c_0,f(x,x)) = x. [back_rewrite(13941),rewrite(14371(2),14371(5),14403(5),14500(5),9978(22),57(4))]. given #693 (F,wt=7): 14873 f(x,f(c_0,c_0)) = c_0. [back_rewrite(12813),rewrite(14371(2),14371(3),14371(6))]. given #694 (T,wt=7): 14875 f(f(c_0,c_0),x) = c_0. [back_rewrite(12806),rewrite(14371(2),14371(3),14371(6))]. given #695 (T,wt=7): 15158 f(f(x,x),x) = c_0. [back_rewrite(8888),rewrite(14371(4))]. given #696 (A,wt=57): 709 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(f(f(y,y),v),f(f(f(f(f(y,w),v),v),y),f(v6,y))),u),u),y),f(y,v7)))))) = y. [para(102(a,1),13(a,1,1,2)),rewrite(102(12),102(12),102(14),102(17),102(18),102(18),102(31),102(32),102(38))]. given #697 (F,wt=7): 15175 f(c_0,x) = f(x,x). [back_rewrite(14403),rewrite(14500(4))]. given #698 (F,wt=7): 15591 f(f(x,x),c_0) = x. [back_rewrite(14745),rewrite(14783(14),15175(9),8396(10),57(8),14500(3,R))]. given #699 (T,wt=11): 12960 f(f(x,f(x,y)),x) = f(x,y). [back_rewrite(12226),rewrite(12715(5),11076(7))]. given #700 (T,wt=11): 13952 f(f(x,y),f(f(x,y),y)) = y. [para(3(a,1),12782(a,1,2,2)),rewrite(3(15))]. given #701 (A,wt=57): 751 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(v,y)))) = y. [para(102(a,1),102(a,1,2,2,1,1,1))]. given #702 (F,wt=11): 13960 f(x,f(x,f(y,x))) = f(y,x). [para(88(a,1),12782(a,1,2,2)),rewrite(88(7))]. given #703 (F,wt=11): 14441 f(f(c_0,f(x,y)),x) = f(x,y). [back_rewrite(14301),rewrite(14371(3),14403(3,R))]. restricted denial: (wt=15): 16561 f(c1,f(c_0,f(c2,c3))) != f(c2,f(c_0,f(c1,c3))) # answer(A_SS). [back_rewrite(15585),rewrite(16430(6),16430(13))]. given #704 (T,wt=11): 14442 f(f(c_0,f(x,y)),y) = f(x,y). [back_rewrite(14300),rewrite(14371(3),14403(3,R))]. given #705 (T,wt=11): 14530 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(14091),rewrite(14371(3),14403(3,R))]. given #706 (A,wt=47): 757 f(f(f(x,y),f(f(f(f(f(f(x,x),z),y),y),f(x,x)),f(f(x,u),f(f(f(f(f(f(x,x),v),u),u),f(x,x)),f(f(x,x),w))))),x) = f(x,x). [para(50(a,1),88(a,1,2,1)),rewrite(50(44),82(23),50(44))]. given #707 (F,wt=11): 14534 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(14079),rewrite(14371(3),14403(3,R))]. given #708 (F,wt=11): 14548 f(f(c_0,f(x,y)),f(y,y)) = c_0. [back_rewrite(13948),rewrite(14500(3,R),14403(3,R),14371(5),14403(5),14500(5),14371(7))]. given #709 (T,wt=11): 14564 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(13907),rewrite(14371(3),14403(3),14500(3),14371(3),14371(7))]. given #710 (T,wt=11): 14565 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_rewrite(13905),rewrite(14371(3),14403(3),14500(3),14371(3),14371(7))]. given #711 (A,wt=51): 758 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(v,f(y,y)),u),u),f(y,y)),f(f(y,y),w)))))) = f(y,y). [para(88(a,1),50(a,1,2,2,2,2,1,1,1,1))]. given #712 (F,wt=11): 14588 f(f(c_0,f(f(x,y),y)),x) = c_0. [back_rewrite(13776),rewrite(14371(4),14403(4,R),14371(7))]. given #713 (F,wt=11): 14783 f(f(x,y),f(c_0,f(x,y))) = c_0. [back_rewrite(13031),rewrite(14371(3),14371(7))]. given #714 (T,wt=11): 14785 f(f(c_0,f(x,y)),f(x,x)) = c_0. [back_rewrite(13007),rewrite(14500(3,R),14403(3,R),14371(7))]. given #715 (T,wt=11): 14874 f(c_0,f(c_0,f(x,y))) = f(x,y). [back_rewrite(12809),rewrite(14371(2),14371(3),14371(4),14500(8,R),14403(8,R),14711(16))]. given #716 (A,wt=51): 759 f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(f(y,u),f(f(f(f(f(f(y,y),v),u),u),f(y,y)),f(w,f(y,y))))))) = f(y,y). [para(88(a,1),50(a,1,2,2,2,2,2))]. given #717 (F,wt=11): 14999 f(x,f(c_0,f(f(x,x),y))) = c_0. [back_rewrite(11519),rewrite(14371(2),14371(7))]. given #718 (F,wt=11): 15043 f(x,f(c_0,f(y,f(x,x)))) = c_0. [back_rewrite(11423),rewrite(14371(2),14371(7))]. given #719 (T,wt=11): 15167 f(f(c_0,f(x,y)),f(x,y)) = c_0. [back_rewrite(14372),rewrite(14500(3,R),14403(3,R),14403(6,R),14403(8,R),14874(8))]. given #720 (T,wt=11): 15858 f(f(x,y),x) = f(x,f(x,y)). [para(12782(a,1),12960(a,1,1))]. given #721 (A,wt=21): 11686 f(x,f(f(y,x),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x). [back_rewrite(8560),rewrite(11660(6))]. given #722 (F,wt=11): 16188 f(f(x,y),f(x,f(x,y))) = x. [back_rewrite(13959),rewrite(15858(3))]. given #723 (F,wt=11): 16203 f(f(x,y),f(y,f(y,x))) = y. [back_rewrite(13190),rewrite(15858(3))]. given #724 (T,wt=11): 16430 f(f(x,y),c_0) = f(c_0,f(x,y)). [para(14441(a,1),82(a,1,1)),rewrite(14500(8,R),15858(6),14874(6),14500(3,R))]. given #725 (T,wt=11): 16899 f(f(c_0,f(x,f(y,y))),y) = c_0. [para(22(a,1),14548(a,1,2))]. given #726 (A,wt=21): 12528 f(x,f(f(x,y),f(f(x,f(x,y)),f(f(x,y),z)))) = f(x,y). [back_rewrite(8551),rewrite(12511(6))]. given #727 (F,wt=11): 16956 f(f(c_0,f(f(x,x),y)),x) = c_0. [para(57(a,1),14564(a,1,2,2)),rewrite(14500(5,R),16430(4),14553(7))]. given #728 (F,wt=11): 17267 f(f(x,y),y) = f(y,f(x,y)). [para(3(a,1),15858(a,1,1)),rewrite(3(14)),flip(a)]. given #729 (T,wt=11): 17394 f(f(x,y),f(y,f(x,y))) = y. [para(15858(a,1),8488(a,1,2,2)),rewrite(15858(3),14371(3),17267(4),15858(5),13960(5),17267(5),15858(6),13960(6),17267(5),14530(8))]. given #730 (T,wt=11): 17567 f(x,f(c_0,f(y,f(x,y)))) = c_0. [back_rewrite(17066),rewrite(17267(3))]. given #731 (A,wt=21): 12783 f(x,f(f(x,y),f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y). [back_rewrite(9202),rewrite(12715(6),12782(4),12715(7),8394(5))]. given #732 (F,wt=11): 18567 f(f(c_0,f(x,f(y,x))),y) = c_0. [back_rewrite(14588),rewrite(17267(3))]. given #733 (F,wt=11): 18956 f(f(x,y),f(c_0,f(y,x))) = c_0. [para(16203(a,1),17567(a,1,2,2,2)),rewrite(15858(5),12782(5))]. given #734 (T,wt=11): 18967 f(f(c_0,f(x,y)),f(y,x)) = c_0. [para(16203(a,1),18567(a,1,1,2,2)),rewrite(15858(4),12782(4))]. given #735 (T,wt=15): 14622 f(f(c_0,f(x,y)),f(c_0,f(f(x,y),z))) = c_0. [back_rewrite(13428),rewrite(14500(3,R),14403(3,R),14371(5),14371(10))]. given #736 (A,wt=15): 14623 f(f(c_0,f(x,y)),f(c_0,f(z,f(x,y)))) = c_0. [back_rewrite(13427),rewrite(14500(3,R),14403(3,R),14371(5),14371(10))]. given #737 (F,wt=15): 14786 f(x,f(c_0,f(f(x,f(x,y)),y))) = f(x,y). [back_rewrite(13006),rewrite(14371(2))]. given #738 (F,wt=15): 15611 f(f(x,f(y,z)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(14577),rewrite(15607(9))]. given #739 (T,wt=15): 15880 f(f(x,x),f(c_0,f(f(x,y),f(x,z)))) = x. [back_rewrite(15847),rewrite(15858(4),15858(5),12782(5))]. given #740 (T,wt=13): 19022 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(15880(a,1),14548(a,1,1,2)),rewrite(15175(2),14500(12,R),15858(8),14874(8))]. given #741 (A,wt=21): 14704 f(x,f(f(y,x),f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x). [back_rewrite(13154),rewrite(14371(3),14500(3),14371(4),14403(4,R),14553(4))]. given #742 (F,wt=13): 19023 f(f(f(x,y),f(x,z)),f(x,x)) = c_0. [para(15880(a,1),14565(a,1,2,2)),rewrite(14500(11,R),15858(7),14874(7),15175(5))]. given #743 (F,wt=13): 19042 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [para(13960(a,1),19022(a,1,2,1))]. given #744 (T,wt=13): 19043 f(f(x,x),f(f(x,y),f(z,x))) = c_0. [para(13960(a,1),19022(a,1,2,2))]. given #745 (T,wt=13): 19068 f(f(f(x,y),f(y,z)),f(y,y)) = c_0. [para(13960(a,1),19023(a,1,1,1))]. given #746 (A,wt=19): 14787 f(x,f(c_0,f(f(x,f(x,y)),f(z,f(x,y))))) = f(x,y). [back_rewrite(13005),rewrite(14371(2))]. given #747 (F,wt=13): 19069 f(f(f(x,y),f(z,x)),f(x,x)) = c_0. [para(13960(a,1),19023(a,1,1,2))]. given #748 (F,wt=13): 19079 f(f(x,x),f(f(y,x),f(z,x))) = c_0. [para(13960(a,1),19042(a,1,2,2))]. given #749 (T,wt=13): 19098 f(f(f(x,y),f(z,y)),f(y,y)) = c_0. [para(13960(a,1),19068(a,1,1,2))]. given #750 (T,wt=15): 15894 f(f(c_0,f(f(x,y),f(x,z))),f(x,x)) = x. [back_rewrite(15815),rewrite(15858(3),15858(4),12782(4))]. given #751 (A,wt=19): 14788 f(x,f(c_0,f(f(x,f(x,y)),f(f(x,y),z)))) = f(x,y). [back_rewrite(13004),rewrite(14371(2))]. given #752 (F,wt=15): 17249 f(f(c_0,f(x,y)),f(f(x,y),z)) = f(x,y). [para(15167(a,1),116(a,1,2,1)),rewrite(15167(9),14500(14,R),15858(12),14874(12),15167(9),14500(12,R),15858(10),14874(10),14874(9),14500(13,R),15858(11),14874(11))]. given #753 (F,wt=15): 17250 f(f(c_0,f(x,y)),f(z,f(x,y))) = f(x,y). [para(15167(a,1),691(a,1,2,1)),rewrite(15167(9),14500(14,R),15858(12),14874(12),15167(9),14500(12,R),15858(10),14874(10),14874(9),14500(13,R),15858(11),14874(11))]. given #754 (T,wt=15): 17251 f(f(f(x,y),z),f(c_0,f(x,y))) = f(x,y). [para(15167(a,1),770(a,1,1,2,1,1,1)),rewrite(14500(3,R),16430(3),15167(5),15167(6),14874(6),14500(5,R),16430(5))]. given #755 (T,wt=15): 18972 f(x,f(c_0,f(f(x,f(x,y)),f(y,x)))) = c_0. [para(16203(a,1),18956(a,1,1))]. given #756 (A,wt=19): 14789 f(x,f(c_0,f(f(x,f(y,x)),f(z,f(y,x))))) = f(y,x). [back_rewrite(13001),rewrite(14371(2))]. given #757 (F,wt=15): 18981 f(f(c_0,f(f(x,f(x,y)),f(y,x))),x) = c_0. [para(16203(a,1),18967(a,1,2))]. given #758 (F,wt=15): 18986 f(f(x,y),f(c_0,f(f(c_0,f(x,y)),z))) = c_0. [para(14874(a,1),14622(a,1,1))]. given #759 (T,wt=15): 18988 f(f(c_0,f(f(x,y),z)),f(c_0,f(x,y))) = c_0. [para(14622(a,1),18567(a,1,1,2,2)),rewrite(15858(7),14874(7))]. given #760 (T,wt=15): 18989 f(f(x,y),f(c_0,f(z,f(c_0,f(x,y))))) = c_0. [para(14874(a,1),14623(a,1,1))]. given #761 (A,wt=19): 14790 f(x,f(c_0,f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x). [back_rewrite(13000),rewrite(14371(2))]. given #762 (F,wt=15): 18991 f(f(c_0,f(x,f(y,z))),f(c_0,f(y,z))) = c_0. [para(14623(a,1),18567(a,1,1,2,2)),rewrite(15858(7),14874(7))]. given #763 (F,wt=15): 19008 f(f(c_0,f(x,f(c_0,f(y,z)))),f(y,z)) = c_0. [para(15611(a,1),14548(a,1,2))]. given #764 (T,wt=15): 19009 f(f(c_0,f(f(c_0,f(x,y)),z)),f(x,y)) = c_0. [para(15611(a,1),14785(a,1,2))]. given #765 (T,wt=15): 19020 f(f(x,x),f(c_0,f(f(y,x),f(x,z)))) = x. [para(13960(a,1),15880(a,1,2,2,1))]. given #766 (A,wt=19): 14794 f(f(c_0,f(f(x,f(x,y)),y)),f(c_0,f(x,y))) = f(x,y). [back_rewrite(12994),rewrite(14371(2),14371(7))]. given #767 (F,wt=15): 19021 f(f(x,x),f(c_0,f(f(x,y),f(z,x)))) = x. [para(13960(a,1),15880(a,1,2,2,2))]. given #768 (F,wt=15): 19035 f(x,f(f(f(x,x),y),f(f(x,x),z))) = c_0. [para(22(a,1),19022(a,1,1))]. given #769 (T,wt=15): 19036 f(f(c_0,f(x,y)),f(y,f(f(x,y),z))) = c_0. [para(22(a,1),19022(a,1,2,1)),rewrite(14500(3,R),16430(3))]. given #770 (T,wt=15): 19037 f(f(c_0,f(x,y)),f(f(f(x,y),z),y)) = c_0. [para(22(a,1),19022(a,1,2,2)),rewrite(14500(3,R),16430(3))]. given #771 (A,wt=33): 14802 f(f(f(x,y),f(f(f(f(x,y),f(c_0,f(f(x,f(x,y)),y))),f(x,x)),f(z,f(x,x)))),x) = f(x,x). [back_rewrite(12971),rewrite(14371(4))]. given #772 (F,wt=15): 19040 f(f(c_0,f(x,y)),f(x,f(f(x,y),z))) = c_0. [para(82(a,1),19022(a,1,2,1)),rewrite(14500(3,R),16430(3))]. given #773 (F,wt=15): 19041 f(f(c_0,f(x,y)),f(f(f(x,y),z),x)) = c_0. [para(82(a,1),19022(a,1,2,2)),rewrite(14500(3,R),16430(3))]. given #774 (T,wt=15): 19061 f(f(x,f(f(y,x),z)),f(c_0,f(y,x))) = c_0. [para(22(a,1),19023(a,1,1,1)),rewrite(14500(6,R),16430(6))]. given #775 (T,wt=15): 19062 f(f(f(f(x,y),z),y),f(c_0,f(x,y))) = c_0. [para(22(a,1),19023(a,1,1,2)),rewrite(14500(6,R),16430(6))]. given #