============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11624 was started by mccune on cleo.thornwood, Sat Aug 12 21:15:08 2006 The command was "/home/mccune/bin/prover9 -f pair.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file pair.in assign(new_constants,1). formulas(sos). f(x,y) = f(y,x). f(f(x,y),f(x,f(y,z))) = x. f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer"). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(x,y) = f(y,x). [assumption]. f(f(x,y),f(x,f(y,z))) = x. [assumption]. f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer"). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ a, b, c, f ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). % Operation f is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 f(x,y) = f(y,x). [assumption]. 2 f(f(x,y),f(x,f(y,z))) = x. [assumption]. 4 f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(b,b)),f(a,f(c,c))) # answer("Sheffer"). [copy(3),rewrite(1(25),1(30)),flip(c)]. end_of_list. formulas(demodulators). 1 f(x,y) = f(y,x). [assumption]. % (lex-dep) 2 f(f(x,y),f(x,f(y,z))) = x. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 1 f(x,y) = f(y,x). [assumption]. given #2 (I,wt=11): 2 f(f(x,y),f(x,f(y,z))) = x. [assumption]. given #3 (I,wt=43): 4 f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(b,b)),f(a,f(c,c))) # answer("Sheffer"). [copy(3),rewrite(1(25),1(30)),flip(c)]. given #4 (T,wt=11): 5 f(f(x,y),f(y,f(x,z))) = y. [para(1(a,1),2(a,1,1))]. given #5 (T,wt=11): 6 f(f(x,y),f(x,f(z,y))) = x. [para(1(a,1),2(a,1,2,2))]. given #6 (A,wt=11): 7 f(f(x,y),f(f(y,z),x)) = x. [para(1(a,1),2(a,1,2))]. given #7 (F,wt=11): 9 f(x,f(x,f(x,y))) = f(x,y). [para(2(a,1),2(a,1,2)),rewrite(1(2),1(3))]. given #8 (F,wt=34): 38 f(a,f(b,f(b,b))) != f(a,a) | f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(b,b)),f(a,f(c,c))) # answer("Sheffer"). [back_rewrite(4),rewrite(35(7)),xx(a)]. given #9 (T,wt=9): 35 f(f(x,x),f(x,y)) = x. [para(9(a,1),2(a,1,2))]. given #10 (T,wt=9): 39 f(f(x,y),f(x,x)) = x. [para(35(a,1),1(a,1)),flip(a)]. given #11 (A,wt=17): 8 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [para(2(a,1),2(a,1,1))]. given #12 (F,wt=9): 40 f(f(x,x),f(y,x)) = x. [para(1(a,1),35(a,1,2))]. given #13 (F,wt=9): 45 f(f(x,y),f(y,y)) = y. [para(1(a,1),39(a,1,1))]. given #14 (T,wt=11): 10 f(f(x,f(y,z)),f(y,x)) = x. [para(5(a,1),1(a,1)),flip(a)]. given #15 (T,wt=11): 11 f(f(x,y),f(y,f(z,x))) = y. [para(1(a,1),5(a,1,2,2))]. given #16 (A,wt=11): 12 f(f(x,y),f(f(x,z),y)) = y. [para(1(a,1),5(a,1,2))]. given #17 (F,wt=11): 14 f(x,f(x,f(y,x))) = f(y,x). [para(5(a,1),2(a,1,2)),rewrite(1(2),1(3))]. given #18 (F,wt=11): 16 f(f(f(x,y),z),f(z,x)) = z. [para(2(a,1),5(a,1,2,2))]. given #19 (T,wt=11): 18 f(f(f(x,y),z),f(z,y)) = z. [para(5(a,1),5(a,1,2,2))]. given #20 (T,wt=11): 19 f(f(x,y),f(f(z,y),x)) = x. [para(1(a,1),6(a,1,2))]. given #21 (A,wt=17): 13 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x). [para(5(a,1),2(a,1,1))]. given #22 (F,wt=11): 31 f(f(x,f(y,z)),f(z,x)) = x. [para(5(a,1),7(a,1,2,1))]. given #23 (F,wt=11): 44 f(x,f(f(x,x),y)) = f(x,x). [para(35(a,1),6(a,1,2)),rewrite(1(3))]. given #24 (T,wt=11): 61 f(x,f(y,f(x,x))) = f(x,x). [para(40(a,1),5(a,1,2)),rewrite(1(3))]. given #25 (T,wt=11): 70 f(f(x,y),f(f(z,x),y)) = y. [para(1(a,1),11(a,1,2))]. given #26 (A,wt=19): 15 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(2(a,1),5(a,1,1))]. given #27 (F,wt=11): 200 f(x,f(y,f(x,y))) = f(x,x). [para(31(a,1),15(a,1,2)),flip(a)]. given #28 (F,wt=11): 205 f(x,f(y,f(y,x))) = f(x,x). [para(1(a,1),200(a,1,2,2))]. given #29 (T,wt=13): 22 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(2(a,1),6(a,1,2)),rewrite(1(4))]. given #30 (T,wt=13): 25 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(5(a,1),6(a,1,2)),rewrite(1(4))]. given #31 (A,wt=19): 17 f(x,f(f(x,f(y,z)),f(f(y,x),u))) = f(x,f(y,z)). [para(5(a,1),5(a,1,1))]. given #32 (F,wt=13): 27 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(6(a,1),6(a,1,2)),rewrite(1(4))]. given #33 (F,wt=13): 30 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(7(a,1),5(a,1,2)),rewrite(1(4))]. given #34 (T,wt=13): 74 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(5(a,1),11(a,1,2)),rewrite(1(4))]. given #35 (T,wt=13): 76 f(x,f(f(y,x),f(z,y))) = f(y,x). [para(11(a,1),6(a,1,2)),rewrite(1(4))]. given #36 (A,wt=17): 20 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [para(6(a,1),2(a,1,1))]. given #37 (F,wt=13): 78 f(x,f(f(y,z),f(x,z))) = f(x,z). [para(6(a,1),11(a,1,2)),rewrite(1(4))]. given #38 (F,wt=13): 84 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(11(a,1),11(a,1,2)),rewrite(1(4))]. given #39 (T,wt=15): 32 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(5(a,1),7(a,1,2)),rewrite(1(3),1(4))]. given #40 (T,wt=11): 569 f(x,f(y,y)) = f(x,f(y,x)). [para(200(a,1),32(a,1,2))]. given #41 (A,wt=17): 21 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(2(a,1),6(a,1,1))]. given #42 (F,wt=34): 582 f(a,f(b,f(b,b))) != f(a,a) | f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(a,b)),f(a,f(a,c))) # answer("Sheffer"). [back_rewrite(38),rewrite(569(27),1(26),569(32),1(31))]. given #43 (F,wt=11): 587 f(f(x,x),y) = f(y,f(x,y)). [para(569(a,1),1(a,1)),flip(a)]. given #44 (T,wt=11): 588 f(x,f(y,y)) = f(x,f(x,y)). [para(1(a,1),569(a,2,2))]. given #45 (T,wt=11): 602 f(x,f(f(y,y),x)) = f(x,y). [para(35(a,1),569(a,1,2)),flip(a)]. given #46 (A,wt=19): 23 f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)). [para(6(a,1),5(a,1,1))]. given #47 (F,wt=11): 740 f(f(x,x),y) = f(y,f(y,x)). [para(1(a,1),587(a,2,2))]. given #48 (F,wt=11): 825 f(x,f(x,f(y,y))) = f(x,y). [para(588(a,2),9(a,1,2))]. given #49 (T,wt=15): 42 f(x,f(f(x,y),f(f(x,x),z))) = f(x,y). [para(35(a,1),5(a,1,1))]. given #50 (T,wt=15): 46 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(39(a,1),6(a,1,1))]. given #51 (A,wt=17): 24 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x). [para(5(a,1),6(a,1,1))]. given #52 (F,wt=15): 47 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z). [para(39(a,1),7(a,1,1))]. given #53 (F,wt=15): 52 f(f(x,y),f(x,f(f(x,f(y,z)),u))) = x. [para(8(a,1),6(a,1,2)),rewrite(1(6))]. given #54 (T,wt=15): 60 f(x,f(f(y,x),f(f(x,x),z))) = f(y,x). [para(40(a,1),5(a,1,1))]. given #55 (T,wt=15): 63 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x). [para(45(a,1),6(a,1,1))]. given #56 (A,wt=17): 26 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y). [para(6(a,1),6(a,1,1))]. given #57 (F,wt=15): 64 f(x,f(f(f(x,x),y),f(z,x))) = f(z,x). [para(45(a,1),7(a,1,1))]. given #58 (F,wt=15): 79 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(11(a,1),7(a,1,2)),rewrite(1(3),1(4))]. given #59 (T,wt=15): 90 f(x,f(y,f(f(y,z),x))) = f(f(y,z),x). [para(12(a,1),7(a,1,2)),rewrite(1(3),1(4))]. given #60 (T,wt=15): 106 f(x,f(y,f(f(z,y),x))) = f(f(z,y),x). [para(18(a,1),6(a,1,2)),rewrite(1(3),1(4))]. given #61 (A,wt=17): 28 f(x,f(f(x,y),f(f(f(y,z),x),u))) = f(x,y). [para(7(a,1),2(a,1,1))]. given #62 (F,wt=15): 109 f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z). [para(39(a,1),18(a,1,2)),rewrite(1(5))]. given #63 (F,wt=15): 112 f(x,f(f(y,f(x,x)),f(z,x))) = f(z,x). [para(45(a,1),18(a,1,2)),rewrite(1(5))]. given #64 (T,wt=15): 124 f(f(x,y),f(y,f(f(y,f(x,z)),u))) = y. [para(13(a,1),6(a,1,2)),rewrite(1(6))]. given #65 (T,wt=15): 172 f(f(x,f(f(x,y),z)),f(x,f(y,u))) = x. [para(15(a,1),6(a,1,2))]. given #66 (A,wt=19): 29 f(x,f(f(f(y,z),x),f(f(x,y),u))) = f(f(y,z),x). [para(7(a,1),5(a,1,1))]. given #67 (F,wt=15): 197 f(f(x,f(y,z)),f(x,f(f(x,y),u))) = x. [para(15(a,1),31(a,1,1)),rewrite(1(5))]. given #68 (F,wt=15): 209 f(f(x,f(y,f(z,y))),f(x,f(z,z))) = x. [para(200(a,1),6(a,1,2,2))]. given #69 (T,wt=15): 219 f(f(f(x,f(y,x)),z),f(z,f(y,y))) = z. [para(200(a,1),11(a,1,2,2))]. given #70 (T,wt=15): 226 f(f(f(x,x),y),f(y,f(z,f(x,z)))) = y. [para(200(a,1),18(a,1,1,1))]. given #71 (A,wt=17): 33 f(x,f(f(x,y),f(z,f(f(y,u),x)))) = f(x,y). [para(7(a,1),6(a,1,1))]. given #72 (F,wt=15): 229 f(f(x,f(y,f(z,y))),f(f(z,z),x)) = x. [para(200(a,1),19(a,1,2,1))]. given #73 (F,wt=15): 234 f(f(x,f(y,y)),f(f(z,f(y,z)),x)) = x. [para(200(a,1),31(a,1,1,2))]. given #74 (T,wt=15): 237 f(f(f(x,f(y,x)),z),f(f(y,y),z)) = z. [para(200(a,1),70(a,1,2,1))]. given #75 (T,wt=15): 242 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x. [para(205(a,1),6(a,1,2,2))]. given #76 (A,wt=21): 48 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v))) = x. [para(8(a,1),2(a,1,1))]. given #77 (F,wt=15): 248 f(f(f(x,f(x,y)),z),f(z,f(y,y))) = z. [para(205(a,1),11(a,1,2,2))]. given #78 (F,wt=15): 253 f(f(f(x,x),y),f(y,f(z,f(z,x)))) = y. [para(205(a,1),18(a,1,1,1))]. given #79 (T,wt=15): 255 f(f(x,f(y,f(y,z))),f(f(z,z),x)) = x. [para(205(a,1),19(a,1,2,1))]. given #80 (T,wt=15): 259 f(f(x,f(y,y)),f(f(z,f(z,y)),x)) = x. [para(205(a,1),31(a,1,1,2))]. given #81 (A,wt=31): 49 f(f(x,y),f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v))) = f(f(x,y),f(f(x,f(y,z)),u)). [para(8(a,1),5(a,1,1))]. given #82 (F,wt=15): 263 f(f(f(x,f(x,y)),z),f(f(y,y),z)) = z. [para(205(a,1),70(a,1,2,1))]. given #83 (F,wt=15): 269 f(f(x,y),f(x,f(f(x,f(z,y)),u))) = x. [para(6(a,1),22(a,1,2,1)),rewrite(6(10))]. given #84 (T,wt=15): 271 f(f(x,y),f(x,f(f(f(y,z),x),u))) = x. [para(7(a,1),22(a,1,2,1)),rewrite(7(10))]. given #85 (T,wt=15): 274 f(f(x,f(y,z)),f(x,f(f(y,x),u))) = x. [para(10(a,1),22(a,1,2,1)),rewrite(10(10))]. given #86 (A,wt=21): 50 f(f(x,y),f(y,f(f(f(x,y),f(f(y,f(x,z)),u)),v))) = y. [para(5(a,1),8(a,1,2,1)),rewrite(5(13))]. given #87 (F,wt=15): 276 f(f(x,y),f(y,f(f(y,f(z,x)),u))) = y. [para(11(a,1),22(a,1,2,1)),rewrite(11(10))]. given #88 (F,wt=15): 278 f(f(x,y),f(y,f(f(f(x,z),y),u))) = y. [para(12(a,1),22(a,1,2,1)),rewrite(12(10))]. given #89 (T,wt=15): 279 f(f(f(x,y),z),f(z,f(f(z,x),u))) = z. [para(16(a,1),22(a,1,2,1)),rewrite(16(10))]. given #90 (T,wt=15): 281 f(f(f(x,y),z),f(z,f(f(z,y),u))) = z. [para(18(a,1),22(a,1,2,1)),rewrite(18(10))]. given #91 (A,wt=21): 51 f(f(x,y),f(x,f(z,f(f(x,y),f(f(x,f(y,u)),v))))) = x. [para(8(a,1),6(a,1,1))]. given #92 (F,wt=15): 282 f(f(x,y),f(x,f(f(f(z,y),x),u))) = x. [para(19(a,1),22(a,1,2,1)),rewrite(19(10))]. given #93 (F,wt=15): 285 f(f(x,f(y,z)),f(x,f(f(z,x),u))) = x. [para(31(a,1),22(a,1,2,1)),rewrite(31(10))]. given #94 (T,wt=15): 287 f(f(x,y),f(y,f(f(f(z,x),y),u))) = y. [para(70(a,1),22(a,1,2,1)),rewrite(70(10))]. given #95 (T,wt=15): 294 f(f(x,f(y,z)),f(x,f(f(x,z),u))) = x. [para(6(a,1),25(a,1,2,1)),rewrite(6(10))]. given #96 (A,wt=21): 53 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(z,y)),u)),v))) = x. [para(6(a,1),8(a,1,2,1)),rewrite(6(13))]. given #97 (F,wt=15): 300 f(f(f(x,y),z),f(z,f(f(x,z),u))) = z. [para(12(a,1),25(a,1,2,1)),rewrite(12(10))]. given #98 (F,wt=15): 305 f(f(f(x,y),z),f(z,f(f(y,z),u))) = z. [para(70(a,1),25(a,1,2,1)),rewrite(70(10))]. given #99 (T,wt=15): 314 f(f(x,f(f(y,x),z)),f(x,f(y,u))) = x. [para(17(a,1),6(a,1,2))]. given #100 (T,wt=15): 344 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x. [para(2(a,1),27(a,1,2,1)),rewrite(2(10))]. given #101 (A,wt=39): 54 f(f(f(x,y),z),f(x,f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)))) = f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)). [para(8(a,1),7(a,1,2)),rewrite(1(8),1(11))]. given #102 (F,wt=15): 345 f(f(x,y),f(y,f(z,f(y,f(x,u))))) = y. [para(5(a,1),27(a,1,2,1)),rewrite(5(10))]. given #103 (F,wt=15): 347 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x. [para(6(a,1),27(a,1,2,1)),rewrite(6(10))]. given #104 (T,wt=15): 349 f(f(x,y),f(x,f(z,f(f(y,u),x)))) = x. [para(7(a,1),27(a,1,2,1)),rewrite(7(10))]. given #105 (T,wt=15): 352 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. [para(10(a,1),27(a,1,2,1)),rewrite(10(10))]. given #106 (A,wt=21): 55 f(f(x,y),f(x,f(f(f(x,y),f(f(f(y,z),x),u)),v))) = x. [para(7(a,1),8(a,1,2,1)),rewrite(7(13))]. given #107 (F,wt=15): 354 f(f(x,y),f(y,f(z,f(y,f(u,x))))) = y. [para(11(a,1),27(a,1,2,1)),rewrite(11(10))]. given #108 (F,wt=15): 356 f(f(x,y),f(y,f(z,f(f(x,u),y)))) = y. [para(12(a,1),27(a,1,2,1)),rewrite(12(10))]. given #109 (T,wt=15): 357 f(f(f(x,y),z),f(z,f(u,f(z,x)))) = z. [para(16(a,1),27(a,1,2,1)),rewrite(16(10))]. given #110 (T,wt=15): 359 f(f(f(x,y),z),f(z,f(u,f(z,y)))) = z. [para(18(a,1),27(a,1,2,1)),rewrite(18(10))]. given #111 (A,wt=23): 56 f(f(x,y),f(f(f(x,y),f(y,z)),f(x,u))) = f(f(x,y),f(y,z)). [para(7(a,1),8(a,1,2,2,1))]. given #112 (F,wt=15): 360 f(f(x,y),f(x,f(z,f(f(u,y),x)))) = x. [para(19(a,1),27(a,1,2,1)),rewrite(19(10))]. given #113 (F,wt=15): 363 f(f(x,f(y,z)),f(x,f(u,f(z,x)))) = x. [para(31(a,1),27(a,1,2,1)),rewrite(31(10))]. given #114 (T,wt=15): 365 f(f(x,y),f(y,f(z,f(f(u,x),y)))) = y. [para(70(a,1),27(a,1,2,1)),rewrite(70(10))]. given #115 (T,wt=15): 420 f(f(x,f(y,z)),f(x,f(u,f(x,y)))) = x. [para(2(a,1),76(a,1,2,1)),rewrite(2(10))]. given #116 (A,wt=19): 58 f(f(x,y),f(x,f(f(f(x,y),f(f(x,x),z)),u))) = x. [para(39(a,1),8(a,1,2,1)),rewrite(39(11))]. given #117 (F,wt=15): 422 f(f(x,f(y,z)),f(x,f(u,f(x,z)))) = x. [para(6(a,1),76(a,1,2,1)),rewrite(6(10))]. given #118 (F,wt=15): 428 f(f(f(x,y),z),f(z,f(u,f(x,z)))) = z. [para(12(a,1),76(a,1,2,1)),rewrite(12(10))]. given #119 (T,wt=15): 433 f(f(f(x,y),z),f(z,f(u,f(y,z)))) = z. [para(70(a,1),76(a,1,2,1)),rewrite(70(10))]. given #120 (T,wt=15): 581 f(x,f(f(x,f(y,z)),f(y,y))) = f(x,x). [back_rewrite(568),rewrite(569(6,R))]. given #121 (A,wt=27): 59 f(x,f(f(x,y),f(f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v)),w))) = f(x,y). [para(8(a,1),8(a,1,2,1)),rewrite(8(17))]. given #122 (F,wt=23): 7997 f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(a,b)),f(a,f(a,c))) # answer("Sheffer"). [back_unit_del(582),unit_del(a,7931)]. given #123 (F,wt=11): 7931 f(x,f(y,f(y,y))) = f(x,x). [para(13(a,1),581(a,1,2,1)),rewrite(5859(5))]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(8088)]. NOTE: New Function symbol precedence: lex([ a, b, c, c_0, f ]). given #124 (T,wt=7): 8179 f(x,f(x,x)) = c_0. [new_symbol(8088)]. given #125 (T,wt=7): 8417 f(f(c_0,c_0),x) = c_0. [back_rewrite(8073),rewrite(8179(2),8179(3),8179(6))]. given #126 (A,wt=19): 62 f(f(x,x),f(f(f(x,x),y),f(x,z))) = f(f(x,x),y). [para(40(a,1),8(a,1,2,2,1))]. given #127 (F,wt=19): 8325 f(f(a,f(a,b)),f(a,f(a,c))) != f(c_0,f(a,f(b,c))) # answer("Sheffer"). [back_rewrite(8176),rewrite(8179(7),1(7)),flip(a)]. given #128 (F,wt=7): 8419 f(c_0,f(c_0,x)) = x. [back_rewrite(8071),rewrite(8179(2),8179(3))]. given #129 (T,wt=7): 8421 f(x,f(c_0,c_0)) = c_0. [back_rewrite(8067),rewrite(8179(2),8179(3),8179(6))]. given #130 (T,wt=7): 8423 f(c_0,f(x,x)) = x. [back_rewrite(8065),rewrite(8179(2))]. given #131 (A,wt=19): 65 f(f(x,y),f(y,f(f(f(x,y),f(f(y,y),z)),u))) = y. [para(45(a,1),8(a,1,2,1)),rewrite(45(11))]. given #132 (F,wt=7): 8425 f(c_0,f(x,c_0)) = x. [back_rewrite(8063),rewrite(8179(2),8179(3))]. given #133 (F,wt=7): 8446 f(c_0,x) = f(x,x). [back_rewrite(8021),rewrite(8179(2))]. given #134 (T,wt=7): 8455 f(x,c_0) = f(x,x). [back_rewrite(7931),rewrite(8179(2))]. given #135 (T,wt=7): 9471 f(x,f(x,c_0)) = c_0. [para(8179(a,1),9(a,1,2,2)),rewrite(8179(5))]. given #136 (A,wt=19): 66 f(x,f(f(x,f(y,z)),f(u,f(y,x)))) = f(x,f(y,z)). [para(10(a,1),6(a,1,1))]. given #137 (F,wt=7): 9496 f(x,f(c_0,x)) = c_0. [para(8417(a,1),587(a,1)),flip(a)]. given #138 (F,wt=9): 8442 f(f(x,y),f(y,c_0)) = y. [back_rewrite(8037),rewrite(8179(3))]. given #139 (T,wt=9): 8443 f(f(x,c_0),f(y,x)) = x. [back_rewrite(8035),rewrite(8179(2))]. given #140 (T,wt=9): 8444 f(f(x,y),f(x,c_0)) = x. [back_rewrite(8031),rewrite(8179(3))]. given #141 (A,wt=19): 67 f(x,f(f(f(y,x),z),f(x,f(y,u)))) = f(x,f(y,u)). [para(10(a,1),7(a,1,1))]. given #142 (F,wt=9): 8445 f(f(x,c_0),f(x,y)) = x. [back_rewrite(8029),rewrite(8179(2))]. given #143 (F,wt=9): 9470 f(f(x,y),f(c_0,x)) = x. [para(8179(a,1),7(a,1,2,1))]. given #144 (T,wt=9): 9473 f(f(x,y),f(c_0,y)) = y. [para(8179(a,1),12(a,1,2,1))]. given #145 (T,wt=9): 9474 f(f(c_0,x),f(x,y)) = x. [para(8179(a,1),16(a,1,1,1))]. given #146 (A,wt=23): 68 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v))) = x. [para(10(a,1),8(a,1,2,1)),rewrite(10(14))]. given #147 (F,wt=9): 9505 f(f(c_0,x),f(y,x)) = x. [back_rewrite(9490),rewrite(9502(9),9502(11))]. given #148 (F,wt=11): 8366 f(x,f(c_0,f(y,f(y,x)))) = c_0. [back_rewrite(8128),rewrite(8179(4),1(4),8179(7))]. given #149 (T,wt=11): 8382 f(x,f(c_0,f(y,f(x,y)))) = c_0. [back_rewrite(8111),rewrite(8179(4),1(4),8179(7))]. given #150 (T,wt=11): 8402 f(f(x,c_0),y) = f(f(x,x),y). [back_rewrite(8089),rewrite(8179(2))]. given #151 (A,wt=25): 69 f(f(x,f(y,z)),f(f(y,f(x,f(y,z))),f(x,u))) = f(y,f(x,f(y,z))). [para(10(a,1),8(a,1,2,2,1)),rewrite(1(5),1(11))]. given #152 (F,wt=11): 8404 f(f(x,c_0),y) = f(y,f(x,x)). [back_rewrite(8086),rewrite(8179(2))]. given #153 (F,wt=11): 8416 f(x,f(x,f(y,c_0))) = f(x,y). [back_rewrite(8074),rewrite(8179(2))]. given #154 (T,wt=11): 8418 f(f(x,c_0),y) = f(y,f(y,x)). [back_rewrite(8072),rewrite(8179(2))]. given #155 (T,wt=11): 8422 f(x,f(y,c_0)) = f(x,f(x,y)). [back_rewrite(8066),rewrite(8179(2))]. given #156 (A,wt=17): 71 f(x,f(f(y,x),f(f(x,f(z,y)),u))) = f(y,x). [para(11(a,1),2(a,1,1))]. given #157 (F,wt=11): 8424 f(f(x,c_0),y) = f(y,f(x,y)). [back_rewrite(8064),rewrite(8179(2))]. given #158 (F,wt=11): 8426 f(x,f(y,c_0)) = f(x,f(y,x)). [back_rewrite(8061),rewrite(8179(2))]. given #159 (T,wt=11): 8429 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(8057),rewrite(8179(3),1(3))]. given #160 (T,wt=11): 8430 f(x,f(c_0,f(y,x))) = f(y,x). [back_rewrite(8056),rewrite(8179(3),1(3))]. given #161 (A,wt=19): 72 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)). [para(2(a,1),11(a,1,1))]. given #162 (F,wt=11): 8431 f(x,f(y,c_0)) = f(x,f(y,y)). [back_rewrite(8054),rewrite(8179(2))]. given #163 (F,wt=11): 8433 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_rewrite(8051),rewrite(8179(4),1(4),8179(7))]. given #164 (T,wt=11): 8434 f(x,f(y,f(x,c_0))) = f(x,x). [back_rewrite(8050),rewrite(8179(2))]. given #165 (T,wt=11): 8435 f(x,f(f(x,c_0),y)) = f(x,x). [back_rewrite(8049),rewrite(8179(2))]. given #166 (A,wt=19): 73 f(x,f(f(x,f(y,z)),f(f(z,x),u))) = f(x,f(y,z)). [para(11(a,1),5(a,1,1))]. given #167 (F,wt=11): 8439 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(8041),rewrite(8179(4),1(4),8179(7))]. given #168 (F,wt=11): 9472 f(x,f(c_0,f(f(x,x),y))) = c_0. [para(8179(a,1),8(a,1,2,1)),rewrite(44(4),8179(7))]. given #169 (T,wt=11): 9475 f(x,f(c_0,f(y,f(x,x)))) = c_0. [para(8179(a,1),27(a,1,2,1)),rewrite(8179(7))]. given #170 (T,wt=11): 9476 f(x,f(y,f(c_0,x))) = f(c_0,x). [para(8179(a,1),90(a,1,2,2,1)),rewrite(8179(6))]. given #171 (A,wt=17): 75 f(x,f(f(y,x),f(z,f(x,f(u,y))))) = f(y,x). [para(11(a,1),6(a,1,1))]. given #172 (F,wt=11): 9494 f(x,f(c_0,f(f(x,c_0),y))) = c_0. [para(8417(a,1),8(a,1,2,2,1,2)),rewrite(8421(4),8421(10))]. given #173 (F,wt=11): 9495 f(x,f(c_0,f(y,f(x,c_0)))) = c_0. [para(8417(a,1),21(a,1,2,2,2,2)),rewrite(8421(4),8421(10))]. given #174 (T,wt=11): 9497 f(x,f(c_0,f(f(c_0,x),y))) = c_0. [para(8417(a,1),28(a,1,2,2,1,1)),rewrite(8421(4),8421(10))]. given #175 (T,wt=11): 9498 f(x,f(c_0,f(y,f(c_0,x)))) = c_0. [para(8417(a,1),33(a,1,2,2,2,1)),rewrite(8421(4),8421(10))]. given #176 (A,wt=19): 77 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)). [para(6(a,1),11(a,1,1))]. given #177 (F,wt=11): 9535 f(x,f(f(c_0,x),y)) = f(c_0,x). [para(8419(a,1),25(a,1,2,2))]. given #178 (F,wt=11): 9629 f(x,f(c_0,y)) = f(x,f(y,y)). [para(8446(a,1),15(a,1,2,1,2)),rewrite(8415(7)),flip(a)]. low water: id=7153, wt=37 low water: id=7351, wt=35 given #179 (T,wt=11): 9631 f(x,f(c_0,y)) = f(x,f(y,x)). [para(8446(a,2),569(a,1,2))]. low water: id=9834, wt=33 given #180 (T,wt=11): 9633 f(f(c_0,x),y) = f(y,f(x,y)). [para(8446(a,2),587(a,1,1))]. low water: id=10489, wt=31 given #181 (A,wt=19): 80 f(x,f(f(f(y,z),x),f(u,f(x,y)))) = f(f(y,z),x). [para(7(a,1),11(a,1,1))]. given #182 (F,wt=11): 9634 f(x,f(c_0,y)) = f(x,f(x,y)). [para(8446(a,2),588(a,1,2))]. given #183 (F,wt=11): 9636 f(f(c_0,x),y) = f(y,f(y,x)). [para(8446(a,2),740(a,1,1))]. given #184 (T,wt=11): 9637 f(x,f(x,f(c_0,y))) = f(x,y). [para(8446(a,2),825(a,1,2,2))]. given #185 (T,wt=11): 9643 f(f(c_0,x),y) = f(f(x,x),y). [para(8446(a,1),90(a,1,2,2,1)),rewrite(8430(5)),flip(a)]. low water: id=11241, wt=29 given #186 (A,wt=21): 81 f(f(x,y),f(y,f(f(f(x,y),f(f(y,f(z,x)),u)),v))) = y. [para(11(a,1),8(a,1,2,1)),rewrite(11(13))]. given #187 (F,wt=11): 9644 f(f(x,x),y) = f(y,f(c_0,x)). [para(8446(a,2),90(a,1,2,2,1)),rewrite(9535(4)),flip(a)]. given #188 (F,wt=11): 9645 f(f(c_0,x),y) = f(y,f(x,x)). [para(8446(a,2),90(a,2,1)),rewrite(44(3)),flip(a)]. given #189 (T,wt=11): 10377 f(f(x,y),f(c_0,f(y,x))) = c_0. [para(569(a,2),8366(a,1,2,2,2)),rewrite(825(5))]. given #190 (T,wt=11): 10599 f(f(x,x),y) = f(y,f(x,c_0)). [para(8402(a,1),1(a,1))]. given #191 (A,wt=31): 82 f(f(x,y),f(f(f(x,y),f(f(x,f(y,z)),u)),f(v,x))) = f(f(x,y),f(f(x,f(y,z)),u)). [para(8(a,1),11(a,1,1))]. given #192 (F,wt=11): 13437 f(f(c_0,f(x,y)),f(y,x)) = c_0. [para(10377(a,1),1(a,1)),flip(a)]. given #193 (F,wt=13): 8452 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [back_rewrite(7953),rewrite(8179(7))]. low water: id=11646, wt=27 given #194 (T,wt=13): 8453 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [back_rewrite(7948),rewrite(8179(7))]. given #195 (T,wt=13): 9502 f(f(c_0,x),f(f(c_0,f(x,y)),z)) = x. [para(8417(a,1),54(a,1,1,1)),rewrite(8417(9),8417(11),8417(13),1(4),8419(4),8417(4),8417(6)),flip(a)]. given #196 (A,wt=19): 83 f(x,f(f(x,f(y,z)),f(u,f(z,x)))) = f(x,f(y,z)). [para(11(a,1),11(a,1,1))]. given #197 (F,wt=13): 9533 f(f(x,c_0),f(f(c_0,f(x,y)),z)) = x. [para(13(a,1),8419(a,1,2)),rewrite(8425(4)),flip(a)]. given #198 (F,wt=13): 9538 f(f(c_0,x),f(f(c_0,f(y,x)),z)) = x. [para(20(a,1),8419(a,1,2)),rewrite(8419(4)),flip(a)]. given #199 (T,wt=13): 9540 f(f(c_0,x),f(y,f(c_0,f(x,z)))) = x. [para(21(a,1),8419(a,1,2)),rewrite(8419(4)),flip(a)]. given #200 (T,wt=13): 9542 f(f(x,c_0),f(y,f(c_0,f(x,z)))) = x. [para(24(a,1),8419(a,1,2)),rewrite(8425(4)),flip(a)]. given #201 (A,wt=17): 85 f(x,f(f(y,x),f(f(f(y,z),x),u))) = f(y,x). [para(12(a,1),2(a,1,1))]. given #202 (F,wt=13): 9545 f(f(c_0,x),f(y,f(c_0,f(z,x)))) = x. [para(26(a,1),8419(a,1,2)),rewrite(8419(4)),flip(a)]. given #203 (F,wt=13): 9666 f(f(x,x),f(f(c_0,f(x,y)),z)) = x. [para(8446(a,1),49(a,2,1)),rewrite(9502(9),5(6)),flip(a)]. given #204 (T,wt=13): 11760 f(f(x,c_0),f(f(c_0,f(y,x)),z)) = x. [para(71(a,1),8419(a,1,2)),rewrite(8425(4)),flip(a)]. given #205 (T,wt=13): 11818 f(f(x,y),f(y,x)) = f(c_0,f(x,y)). [para(8424(a,2),205(a,1,2,2)),rewrite(9631(5,R),8425(5),8446(6,R))]. given #206 (A,wt=19): 86 f(x,f(f(f(x,y),z),f(x,f(y,u)))) = f(x,f(y,u)). [para(2(a,1),12(a,1,1))]. given #207 (F,wt=13): 12119 f(f(x,f(c_0,f(y,z))),f(y,c_0)) = y. [para(24(a,1),8430(a,1,2)),rewrite(9542(14))]. given #208 (F,wt=13): 12350 f(f(x,c_0),f(y,f(c_0,f(z,x)))) = x. [para(75(a,1),8419(a,1,2)),rewrite(8425(4)),flip(a)]. given #209 (T,wt=13): 12372 f(f(x,f(c_0,f(y,z))),f(z,c_0)) = z. [para(75(a,1),8430(a,1,2)),rewrite(12350(14))]. given #210 (T,wt=13): 13285 f(f(c_0,x),f(y,f(y,f(x,z)))) = x. [para(9636(a,1),49(a,2,2)),rewrite(9502(9),5(6)),flip(a)]. given #211 (A,wt=19): 87 f(x,f(f(f(y,z),x),f(f(y,x),u))) = f(f(y,z),x). [para(12(a,1),5(a,1,1))]. given #212 (F,wt=13): 13534 f(f(x,x),f(f(y,x),f(z,x))) = c_0. [para(1(a,1),8452(a,1,2,2))]. given #213 (F,wt=13): 13535 f(f(x,x),f(f(x,y),f(z,x))) = c_0. [para(1(a,1),8452(a,1,2))]. given #214 (T,wt=13): 13562 f(f(x,c_0),f(f(y,x),f(x,z))) = c_0. [para(8452(a,1),90(a,1,2,2)),rewrite(1(6),8452(11))]. given #215 (T,wt=13): 13571 f(f(c_0,x),f(f(y,x),f(x,z))) = c_0. [para(8446(a,2),8452(a,1,1))]. given #216 (A,wt=17): 88 f(x,f(f(y,x),f(z,f(f(y,u),x)))) = f(y,x). [para(12(a,1),6(a,1,1))]. given #217 (F,wt=13): 13617 f(f(x,c_0),f(f(x,y),f(x,z))) = c_0. [para(8453(a,1),90(a,1,2,2)),rewrite(1(6),8453(11))]. given #218 (F,wt=13): 13629 f(f(c_0,x),f(f(x,y),f(x,z))) = c_0. [para(8446(a,2),8453(a,1,1))]. given #219 (T,wt=13): 13685 f(f(x,c_0),f(y,f(y,f(x,z)))) = x. [para(9636(a,1),9533(a,1,2))]. given #220 (T,wt=13): 13689 f(f(x,x),f(f(c_0,f(y,x)),z)) = x. [para(9538(a,1),14(a,1,2,2)),rewrite(1(9),569(10,R),1(6),9538(13))]. given #221 (A,wt=19): 89 f(x,f(f(f(x,y),z),f(x,f(u,y)))) = f(x,f(u,y)). [para(6(a,1),12(a,1,1))]. given #222 (F,wt=13): 13743 f(f(c_0,x),f(y,f(y,f(z,x)))) = x. [para(9636(a,1),9538(a,1,2))]. given #223 (F,wt=13): 13776 f(f(x,x),f(y,f(c_0,f(x,z)))) = x. [para(8446(a,1),9540(a,1,1))]. given #224 (T,wt=13): 13824 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(8446(a,1),9545(a,1,1))]. given #225 (T,wt=13): 13849 f(f(x,x),f(y,f(y,f(x,z)))) = x. [para(9636(a,1),9666(a,1,2))]. given #226 (A,wt=19): 91 f(x,f(f(f(x,y),z),f(f(y,u),x))) = f(f(y,u),x). [para(7(a,1),12(a,1,1))]. given #227 (F,wt=13): 13850 f(f(x,c_0),f(y,f(y,f(z,x)))) = x. [para(9636(a,1),11760(a,1,2))]. given #228 (F,wt=13): 13913 f(f(x,f(x,f(y,z))),f(y,c_0)) = y. [para(9634(a,1),12119(a,1,1))]. given #229 (T,wt=13): 13931 f(f(x,f(x,f(y,z))),f(z,c_0)) = z. [para(9634(a,1),12372(a,1,1))]. given #230 (T,wt=13): 13935 f(f(x,f(x,f(y,z))),f(c_0,y)) = y. [para(13285(a,1),1(a,1)),flip(a)]. given #231 (A,wt=21): 92 f(f(x,y),f(y,f(f(f(x,y),f(f(f(x,z),y),u)),v))) = y. [para(12(a,1),8(a,1,2,1)),rewrite(12(13))]. given #232 (F,wt=13): 13942 f(f(x,f(x,f(y,z))),f(y,y)) = y. [para(13285(a,1),14(a,1,2,2)),rewrite(1(7),569(8,R),13285(11))]. given #233 (F,wt=13): 14011 f(f(x,c_0),f(f(y,x),f(z,x))) = c_0. [para(13534(a,1),90(a,1,2,2)),rewrite(1(6),13534(11))]. given #234 (T,wt=13): 14020 f(f(c_0,x),f(f(y,x),f(z,x))) = c_0. [para(8446(a,2),13534(a,1,1))]. given #235 (T,wt=13): 14058 f(f(x,c_0),f(f(x,y),f(z,x))) = c_0. [para(13535(a,1),90(a,1,2,2)),rewrite(1(6),13535(11))]. given #236 (A,wt=23): 93 f(f(x,y),f(f(f(x,y),f(x,z)),f(y,u))) = f(f(x,y),f(x,z)). [para(12(a,1),8(a,1,2,2,1))]. given #237 (F,wt=13): 14067 f(f(c_0,x),f(f(x,y),f(z,x))) = c_0. [para(8446(a,2),13535(a,1,1))]. given #238 (F,wt=13): 14113 f(f(x,x),f(y,f(y,f(z,x)))) = x. [para(9636(a,1),13689(a,1,2))]. given #239 (T,wt=13): 14118 f(f(x,f(x,f(y,z))),f(c_0,z)) = z. [para(13743(a,1),1(a,1)),flip(a)]. given #240 (T,wt=13): 14122 f(f(x,f(x,f(y,z))),f(z,z)) = z. [para(13743(a,1),14(a,1,2,2)),rewrite(1(7),569(8,R),13743(11))]. given #241 (A,wt=31): 94 f(f(x,y),f(f(x,z),f(f(x,y),f(f(x,f(y,u)),v)))) = f(f(x,y),f(f(x,f(y,u)),v)). [para(8(a,1),12(a,1,1))]. given #242 (F,wt=15): 589 f(f(x,f(y,x)),f(x,f(f(y,y),z))) = x. [para(569(a,1),2(a,1,1))]. given #243 (F,wt=15): 594 f(f(x,f(y,x)),f(x,f(z,f(y,y)))) = x. [para(569(a,1),6(a,1,1))]. given #244 (T,wt=15): 595 f(f(x,f(y,y)),f(x,f(z,f(y,z)))) = x. [para(569(a,1),6(a,1,2,2))]. given #245 (T,wt=15): 596 f(f(x,f(y,z)),f(x,f(z,f(y,y)))) = x. [para(569(a,2),6(a,1,2,2))]. given #246 (A,wt=19): 95 f(x,f(f(f(y,z),x),f(u,f(y,x)))) = f(f(y,z),x). [para(12(a,1),11(a,1,1))]. given #247 (F,wt=15): 598 f(f(x,f(y,x)),f(f(f(y,y),z),x)) = x. [para(569(a,1),7(a,1,1))]. given #248 (F,wt=15): 613 f(f(f(x,y),z),f(z,f(y,f(x,x)))) = z. [para(569(a,2),11(a,1,2,2))]. given #249 (T,wt=15): 624 f(f(f(x,f(y,y)),z),f(z,f(y,z))) = z. [para(569(a,1),18(a,1,2))]. low water: id=12382, wt=25 given #250 (T,wt=15): 625 f(f(f(x,f(y,y)),z),f(z,f(y,x))) = z. [para(569(a,2),18(a,1,1,1))]. given #251 (A,wt=19): 96 f(x,f(f(f(y,x),z),f(x,f(u,y)))) = f(x,f(u,y)). [para(11(a,1),12(a,1,1))]. given #252 (F,wt=15): 629 f(f(x,f(y,x)),f(f(z,f(y,y)),x)) = x. [para(569(a,1),19(a,1,1))]. given #253 (F,wt=15): 631 f(f(x,f(y,z)),f(f(z,f(y,y)),x)) = x. [para(569(a,2),19(a,1,2,1))]. given #254 (T,wt=15): 638 f(f(x,f(y,f(z,z))),f(f(z,y),x)) = x. [para(569(a,2),31(a,1,1,2))]. given #255 (T,wt=15): 641 f(f(f(x,x),y),f(f(z,f(x,z)),y)) = y. [para(569(a,1),70(a,1,2,1))]. given #256 (A,wt=19): 97 f(x,f(f(f(y,x),z),f(f(y,u),x))) = f(f(y,u),x). [para(12(a,1),12(a,1,1))]. given #257 (F,wt=15): 644 f(f(f(x,y),z),f(f(y,f(x,x)),z)) = z. [para(569(a,2),70(a,1,2,1))]. given #258 (F,wt=15): 646 f(x,f(y,f(z,z))) = f(x,f(y,f(z,y))). [para(569(a,1),15(a,1,2,1,2)),rewrite(15(7)),flip(a)]. given #259 (T,wt=15): 774 f(f(x,f(y,f(z,z))),f(x,f(z,x))) = x. [para(587(a,1),31(a,1,2))]. given #260 (T,wt=15): 780 f(x,f(f(y,y),z)) = f(x,f(z,f(y,z))). [para(587(a,1),15(a,1,2,1,2)),rewrite(487(8)),flip(a)]. given #261 (A,wt=23): 101 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(z,x),u)),v))) = z. [para(16(a,1),8(a,1,2,1)),rewrite(16(14))]. given #262 (F,wt=15): 820 f(f(x,f(y,y)),f(x,f(z,f(z,y)))) = x. [para(588(a,1),6(a,1,2,2))]. given #263 (F,wt=15): 850 f(f(f(x,x),y),f(f(z,f(z,x)),y)) = y. [para(588(a,1),70(a,1,2,1))]. given #264 (T,wt=15): 854 f(x,f(y,f(z,z))) = f(x,f(y,f(y,z))). [para(588(a,1),15(a,1,2,1,2)),rewrite(15(7)),flip(a)]. given #265 (T,wt=15): 897 f(f(x,f(f(y,y),z)),f(x,f(z,y))) = x. [para(602(a,1),6(a,1,2,2))]. given #266 (A,wt=19): 102 f(x,f(f(f(y,z),x),f(f(x,z),u))) = f(f(y,z),x). [para(18(a,1),2(a,1,1))]. given #267 (F,wt=15): 915 f(f(f(f(x,x),y),z),f(f(y,x),z)) = z. [para(602(a,1),70(a,1,2,1))]. given #268 (F,wt=15): 944 f(f(x,f(f(x,y),z)),f(x,f(u,y))) = x. [para(23(a,1),6(a,1,2))]. given #269 (T,wt=15): 1038 f(x,f(f(y,y),z)) = f(x,f(z,f(z,y))). [para(740(a,1),15(a,1,2,1,2)),rewrite(489(8)),flip(a)]. given #270 (T,wt=15): 1095 f(x,f(f(x,y),f(z,f(x,z)))) = f(x,y). [para(587(a,1),42(a,1,2,2))]. given #271 (A,wt=17): 103 f(x,f(f(x,y),f(f(f(z,y),x),u))) = f(x,y). [para(18(a,1),5(a,1,1))]. low water: id=13246, wt=23 given #272 (F,wt=15): 1098 f(x,f(f(x,y),f(z,f(z,x)))) = f(x,y). [para(740(a,1),42(a,1,2,2))]. given #273 (F,wt=15): 1124 f(f(x,f(y,f(x,f(z,u)))),f(z,x)) = x. [para(24(a,1),6(a,1,2))]. given #274 (T,wt=15): 1207 f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z). [para(587(a,1),47(a,1,2,1))]. given #275 (T,wt=15): 1210 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z). [para(740(a,1),47(a,1,2,1))]. given #276 (A,wt=17): 104 f(x,f(f(y,f(x,f(z,u))),f(z,x))) = f(z,x). [para(5(a,1),18(a,1,2)),rewrite(1(6))]. given #277 (F,wt=15): 1311 f(x,f(f(y,x),f(z,f(x,z)))) = f(y,x). [para(587(a,1),60(a,1,2,2))]. given #278 (F,wt=15): 1317 f(x,f(f(y,x),f(z,f(z,x)))) = f(y,x). [para(740(a,1),60(a,1,2,2))]. given #279 (T,wt=15): 1492 f(x,f(f(y,f(x,y)),f(z,x))) = f(z,x). [para(587(a,1),64(a,1,2,1))]. given #280 (T,wt=15): 1495 f(x,f(f(y,f(y,x)),f(z,x))) = f(z,x). [para(740(a,1),64(a,1,2,1))]. given #281 (A,wt=19): 105 f(x,f(f(f(y,z),x),f(u,f(x,z)))) = f(f(y,z),x). [para(18(a,1),6(a,1,1))]. given #282 (F,wt=15): 1550 f(x,f(f(y,y),f(f(y,z),x))) = f(x,x). [para(90(a,1),200(a,1,2,2)),rewrite(1(6),569(6,R),1(4))]. given #283 (F,wt=15): 1568 f(f(x,f(y,y)),z) = f(f(x,f(y,x)),z). [para(569(a,1),90(a,1,2,2,1)),rewrite(90(5)),flip(a)]. given #284 (T,wt=15): 1574 f(f(f(x,x),y),z) = f(f(y,f(x,y)),z). [para(587(a,1),90(a,1,2,2,1)),rewrite(437(6)),flip(a)]. given #285 (T,wt=15): 1577 f(f(x,f(y,y)),z) = f(f(x,f(x,y)),z). [para(588(a,1),90(a,1,2,2,1)),rewrite(90(5)),flip(a)]. given #286 (A,wt=19): 107 f(x,f(f(f(x,y),z),f(f(u,y),x))) = f(f(u,y),x). [para(18(a,1),7(a,1,1))]. given #287 (F,wt=15): 1582 f(f(f(x,x),y),z) = f(f(y,f(y,x)),z). [para(740(a,1),90(a,1,2,2,1)),rewrite(439(6)),flip(a)]. given #288 (F,wt=15): 1607 f(x,f(f(y,y),f(f(z,y),x))) = f(x,x). [para(106(a,1),200(a,1,2,2)),rewrite(1(6),569(6,R),1(4))]. given #289 (T,wt=15): 1868 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [para(1(a,1),172(a,1,1,2))]. given #290 (T,wt=15): 1869 f(f(x,f(f(x,y),z)),f(f(y,u),x)) = x. [para(1(a,1),172(a,1,2))]. given #291 (A,wt=17): 108 f(x,f(f(y,f(f(z,u),x)),f(x,z))) = f(x,z). [para(7(a,1),18(a,1,2)),rewrite(1(6))]. given #292 (F,wt=15): 1950 f(x,f(y,f(x,f(f(x,y),z)))) = f(x,x). [para(172(a,1),79(a,1,2)),flip(a)]. given #293 (F,wt=15): 1954 f(f(x,f(f(x,y),z)),f(f(u,y),x)) = x. [para(106(a,1),172(a,1,2))]. given #294 (T,wt=15): 2151 f(f(x,f(y,f(z,y))),f(x,f(z,x))) = x. [para(569(a,1),209(a,1,2))]. given #295 (T,wt=15): 2157 f(f(x,f(y,f(z,y))),f(x,f(x,z))) = x. [para(588(a,1),209(a,1,2))]. given #296 (A,wt=23): 110 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(z,y),u)),v))) = z. [para(18(a,1),8(a,1,2,1)),rewrite(18(14))]. given #297 (F,wt=15): 2251 f(f(f(x,f(y,x)),z),f(z,f(y,z))) = z. [para(569(a,1),219(a,1,2))]. given #298 (F,wt=15): 2259 f(f(f(x,f(y,x)),z),f(z,f(z,y))) = z. [para(588(a,1),219(a,1,2))]. given #299 (T,wt=15): 2379 f(f(x,f(y,x)),f(x,f(z,f(y,z)))) = x. [para(587(a,1),226(a,1,1))]. given #300 (T,wt=15): 2389 f(f(x,f(x,y)),f(x,f(z,f(y,z)))) = x. [para(740(a,1),226(a,1,1))]. given #301 (A,wt=39): 111 f(f(f(x,y),z),f(y,f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)))) = f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)). [para(8(a,1),18(a,1,1)),rewrite(1(10))]. given #302 (F,wt=15): 2629 f(f(x,f(y,x)),f(f(z,f(y,z)),x)) = x. [para(569(a,1),234(a,1,1))]. given #303 (F,wt=15): 2634 f(f(x,f(x,y)),f(f(z,f(y,z)),x)) = x. [para(588(a,1),234(a,1,1))]. given #304 (T,wt=15): 2827 f(f(x,f(y,f(y,z))),f(x,f(z,x))) = x. [para(569(a,1),242(a,1,2))]. given #305 (T,wt=15): 2833 f(f(x,f(y,f(y,z))),f(x,f(x,z))) = x. [para(588(a,1),242(a,1,2))]. given #306 (A,wt=19): 113 f(x,f(f(y,f(z,x)),f(x,f(z,u)))) = f(x,f(z,u)). [para(10(a,1),18(a,1,2)),rewrite(1(6))]. given #307 (F,wt=15): 3026 f(f(f(x,f(x,y)),z),f(z,f(y,z))) = z. [para(569(a,1),248(a,1,2))]. given #308 (F,wt=15): 3034 f(f(f(x,f(x,y)),z),f(z,f(z,y))) = z. [para(588(a,1),248(a,1,2))]. given #309 (T,wt=15): 3151 f(f(x,f(y,x)),f(x,f(z,f(z,y)))) = x. [para(587(a,1),253(a,1,1))]. given #310 (T,wt=15): 3161 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x. [para(740(a,1),253(a,1,1))]. given #311 (A,wt=17): 114 f(x,f(f(x,y),f(z,f(f(u,y),x)))) = f(x,y). [para(18(a,1),11(a,1,1))]. given #312 (F,wt=15): 3282 f(f(x,f(y,x)),f(f(z,f(z,y)),x)) = x. [para(569(a,1),259(a,1,1))]. given #313 (F,wt=15): 3287 f(f(x,f(x,y)),f(f(z,f(z,y)),x)) = x. [para(588(a,1),259(a,1,1))]. given #314 (T,wt=15): 3861 f(f(x,f(f(y,x),z)),f(f(y,u),x)) = x. [para(274(a,1),106(a,1,2,2)),rewrite(274(12))]. given #315 (T,wt=15): 4834 f(f(x,f(f(y,x),z)),f(x,f(u,y))) = x. [para(285(a,1),1(a,1)),flip(a)]. given #316 (A,wt=17): 115 f(x,f(f(y,f(x,f(z,u))),f(u,x))) = f(u,x). [para(11(a,1),18(a,1,2)),rewrite(1(6))]. given #317 (F,wt=15): 4926 f(f(x,f(f(y,x),z)),f(f(u,y),x)) = x. [para(285(a,1),106(a,1,2,2)),rewrite(285(12))]. given #318 (F,wt=15): 5635 f(f(x,f(y,f(z,x))),f(x,f(z,u))) = x. [para(1(a,1),314(a,1,1,2))]. given #319 (T,wt=15): 5676 f(x,f(y,f(x,f(f(y,x),z)))) = f(x,x). [para(314(a,1),79(a,1,2)),flip(a)]. given #320 (T,wt=15): 6114 f(f(x,f(y,f(x,f(z,u)))),f(u,x)) = x. [para(347(a,1),106(a,1,2,2)),rewrite(347(12))]. given #321 (A,wt=19): 116 f(x,f(f(y,f(x,z)),f(f(z,u),x))) = f(f(z,u),x). [para(16(a,1),18(a,1,2)),rewrite(1(6))]. given #322 (F,wt=15): 6384 f(f(x,f(y,f(z,x))),f(f(z,u),x)) = x. [para(352(a,1),106(a,1,2,2)),rewrite(352(12))]. given #323 (F,wt=15): 6781 f(f(x,f(y,f(x,z))),f(f(z,u),x)) = x. [para(357(a,1),1(a,1)),flip(a)]. given #324 (T,wt=15): 6965 f(f(x,f(y,f(x,z))),f(f(u,z),x)) = x. [para(359(a,1),1(a,1)),flip(a)]. given #325 (T,wt=15): 7352 f(f(x,f(y,f(z,x))),f(x,f(u,z))) = x. [para(363(a,1),1(a,1)),flip(a)]. given #326 (A,wt=19): 117 f(x,f(f(y,f(x,z)),f(f(u,z),x))) = f(f(u,z),x). [para(18(a,1),18(a,1,2)),rewrite(1(6))]. given #327 (F,wt=15): 7404 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x. [para(23(a,1),363(a,1,2))]. given #328 (F,wt=15): 7414 f(f(x,f(y,f(z,x))),f(f(u,z),x)) = x. [para(363(a,1),106(a,1,2,2)),rewrite(363(12))]. given #329 (T,wt=15): 7915 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x). [para(1(a,1),581(a,1,2))]. given #330 (T,wt=15): 7921 f(x,f(y,f(x,f(f(y,y),z)))) = f(x,x). [para(35(a,1),581(a,1,2,2)),rewrite(1(4))]. given #331 (A,wt=21): 118 f(f(x,y),f(x,f(f(f(x,y),f(f(f(z,y),x),u)),v))) = x. [para(19(a,1),8(a,1,2,1)),rewrite(19(13))]. given #332 (F,wt=15): 7941 f(x,f(y,f(x,f(z,f(y,z))))) = f(x,x). [para(587(a,1),581(a,1,2,1,2)),rewrite(35(6),1(4))]. given #333 (F,wt=15): 7944 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x). [para(740(a,1),581(a,1,2,1,2)),rewrite(35(6),1(4))]. given #334 (T,wt=15): 8326 f(x,f(f(x,f(y,z)),f(y,c_0))) = f(x,x). [back_rewrite(8175),rewrite(8179(4))]. given #335 (T,wt=15): 8335 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [back_rewrite(8166),rewrite(8179(3),8179(5),1(5),8179(10))]. given #336 (A,wt=23): 119 f(f(x,y),f(f(f(x,y),f(z,y)),f(x,u))) = f(f(x,y),f(z,y)). [para(19(a,1),8(a,1,2,2,1))]. given #337 (F,wt=15): 8341 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [back_rewrite(8159),rewrite(8179(3),8179(5),1(5),8179(10))]. given #338 (F,wt=15): 8355 f(f(x,x),f(c_0,f(f(c_0,f(y,x)),z))) = c_0. [back_rewrite(8142),rewrite(8179(3),8179(5),1(5),8179(10))]. given #339 (T,wt=15): 8362 f(f(x,x),f(c_0,f(f(c_0,f(x,y)),z))) = c_0. [back_rewrite(8134),rewrite(8179(3),8179(5),1(5),8179(10))]. given #340 (T,wt=15): 8365 f(f(f(x,f(x,y)),z),f(f(y,c_0),z)) = z. [back_rewrite(8129),rewrite(8179(5))]. given #341 (A,wt=17): 120 f(x,f(f(y,f(f(z,u),x)),f(x,u))) = f(x,u). [para(19(a,1),18(a,1,2)),rewrite(1(6))]. given #342 (F,wt=15): 8371 f(f(x,f(y,c_0)),f(f(z,f(z,y)),x)) = x. [back_rewrite(8123),rewrite(8179(2))]. given #343 (F,wt=15): 8373 f(f(x,f(y,f(y,z))),f(f(z,c_0),x)) = x. [back_rewrite(8121),rewrite(8179(5))]. given #344 (T,wt=15): 8376 f(f(f(x,c_0),y),f(y,f(z,f(z,x)))) = y. [back_rewrite(8118),rewrite(8179(2))]. given #345 (T,wt=15): 8377 f(f(f(x,f(x,y)),z),f(z,f(y,c_0))) = z. [back_rewrite(8116),rewrite(8179(5))]. given #346 (A,wt=23): 121 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v))) = x. [para(2(a,1),13(a,1,2,1)),rewrite(2(14))]. given #347 (F,wt=15): 8379 f(f(x,f(y,f(y,z))),f(x,f(z,c_0))) = x. [back_rewrite(8114),rewrite(8179(5))]. given #348 (F,wt=15): 8380 f(f(f(x,f(y,x)),z),f(f(y,c_0),z)) = z. [back_rewrite(8113),rewrite(8179(5))]. given #349 (T,wt=15): 8384 f(f(x,f(y,c_0)),f(f(z,f(y,z)),x)) = x. [back_rewrite(8109),rewrite(8179(2))]. given #350 (T,wt=15): 8386 f(f(x,f(y,f(z,y))),f(f(z,c_0),x)) = x. [back_rewrite(8107),rewrite(8179(5))]. given #351 (A,wt=31): 122 f(f(x,y),f(f(f(x,y),f(f(y,f(x,z)),u)),f(y,v))) = f(f(x,y),f(f(y,f(x,z)),u)). [para(13(a,1),5(a,1,1))]. given #352 (F,wt=15): 8392 f(f(f(x,c_0),y),f(y,f(z,f(x,z)))) = y. [back_rewrite(8101),rewrite(8179(2))]. given #353 (F,wt=15): 8393 f(f(f(x,f(y,x)),z),f(z,f(y,c_0))) = z. [back_rewrite(8099),rewrite(8179(5))]. given #354 (T,wt=15): 8395 f(f(x,f(y,f(z,y))),f(x,f(z,c_0))) = x. [back_rewrite(8097),rewrite(8179(5))]. given #355 (T,wt=15): 8398 f(x,f(f(y,f(x,c_0)),f(z,x))) = f(z,x). [back_rewrite(8093),rewrite(8179(2))]. given #356 (A,wt=21): 123 f(f(x,y),f(y,f(z,f(f(x,y),f(f(y,f(x,u)),v))))) = y. [para(13(a,1),6(a,1,1))]. given #357 (F,wt=15): 8400 f(x,f(f(y,f(x,c_0)),f(x,z))) = f(x,z). [back_rewrite(8091),rewrite(8179(2))]. given #358 (F,wt=15): 8406 f(x,f(f(f(x,c_0),y),f(z,x))) = f(z,x). [back_rewrite(8084),rewrite(8179(2))]. given #359 (T,wt=15): 8408 f(x,f(f(y,x),f(z,f(x,c_0)))) = f(y,x). [back_rewrite(8082),rewrite(8179(3))]. given #360 (T,wt=15): 8410 f(x,f(f(y,x),f(f(x,c_0),z))) = f(y,x). [back_rewrite(8080),rewrite(8179(3))]. given #361 (A,wt=23): 125 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(x,z),u)),v))) = x. [para(6(a,1),13(a,1,2,1)),rewrite(6(14))]. given #362 (F,wt=15): 8412 f(x,f(f(f(x,c_0),y),f(x,z))) = f(x,z). [back_rewrite(8078),rewrite(8179(2))]. given #363 (F,wt=15): 8414 f(x,f(f(x,y),f(z,f(x,c_0)))) = f(x,y). [back_rewrite(8076),rewrite(8179(3))]. given #364 (T,wt=15): 8415 f(x,f(f(x,y),f(f(x,c_0),z))) = f(x,y). [back_rewrite(8075),rewrite(8179(3))]. given #365 (T,wt=15): 8456 f(x,f(y,f(c_0,f(f(x,x),z)))) = f(x,x). [back_rewrite(4647),rewrite(8179(2))]. given #366 (A,wt=39): 126 f(f(x,f(y,z)),f(y,f(f(x,f(y,z)),f(f(f(y,z),f(x,u)),v)))) = f(f(x,f(y,z)),f(f(f(y,z),f(x,u)),v)). [para(13(a,1),7(a,1,2)),rewrite(1(8),1(11))]. given #367 (F,wt=15): 8480 f(x,f(f(c_0,f(f(x,x),y)),z)) = f(x,x). [back_rewrite(2945),rewrite(8179(2))]. given #368 (F,wt=15): 8647 f(f(f(x,y),z),f(f(c_0,f(y,x)),z)) = z. [back_rewrite(3499),rewrite(8446(5,R))]. given #369 (T,wt=15): 8655 f(f(x,f(y,z)),f(f(c_0,f(z,y)),x)) = x. [back_rewrite(3234),rewrite(8446(5,R))]. given #370 (T,wt=15): 8661 f(f(f(c_0,f(x,y)),z),f(z,f(y,x))) = z. [back_rewrite(3147),rewrite(8446(3,R))]. given #371 (A,wt=23): 127 f(f(x,y),f(f(f(y,z),f(x,y)),f(x,u))) = f(f(y,z),f(x,y)). [para(7(a,1),13(a,1,2,2,1))]. given #372 (F,wt=15): 8828 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y). [back_rewrite(1785),rewrite(8426(7,R),1(5))]. given #373 (F,wt=15): 8829 f(f(f(x,x),y),f(c_0,f(z,x))) = f(z,x). [back_rewrite(1753),rewrite(8426(7,R),1(5))]. given #374 (T,wt=15): 8835 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(1493),rewrite(8426(7,R),1(5))]. given #375 (T,wt=15): 8840 f(f(f(x,x),y),f(c_0,f(x,z))) = f(x,z). [back_rewrite(1208),rewrite(8426(7,R),1(5))]. given #376 (A,wt=27): 129 f(x,f(f(y,x),f(f(x,f(f(f(y,x),f(f(x,f(y,z)),u)),v)),w))) = f(y,x). [para(13(a,1),8(a,1,2,1)),rewrite(13(17))]. given #377 (F,wt=15): 8851 f(f(x,x),f(y,c_0)) = f(f(y,y),f(x,c_0)). [back_rewrite(810),rewrite(8426(4,R),8426(8,R))]. given #378 (F,wt=15): 8859 f(f(x,y),f(z,c_0)) = f(f(z,z),f(x,y)). [back_rewrite(784),rewrite(8426(4,R))]. given #379 (T,wt=15): 8871 f(x,f(f(y,x),f(c_0,f(z,y)))) = f(x,x). [back_rewrite(540),rewrite(8426(5,R),1(4))]. low water: id=15984, wt=21 given #380 (T,wt=15): 8872 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x). [back_rewrite(515),rewrite(8426(5,R),1(4))]. given #381 (A,wt=37): 130 f(f(f(x,y),f(f(x,f(y,z)),u)),f(f(x,y),f(f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v)),w))) = f(x,y). [para(8(a,1),13(a,1,2,1)),rewrite(8(22))]. given #382 (F,wt=15): 8873 f(x,f(f(y,x),f(c_0,f(y,z)))) = f(x,x). [back_rewrite(408),rewrite(8426(5,R),1(4))]. given #383 (F,wt=15): 8874 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x). [back_rewrite(388),rewrite(8426(5,R),1(4))]. given #384 (T,wt=15): 8983 f(f(x,f(c_0,f(y,z))),f(f(z,y),x)) = x. [back_rewrite(3284),rewrite(8446(3,R))]. given #385 (T,wt=15): 9477 f(x,f(f(x,y),f(f(c_0,x),z))) = f(x,y). [para(8179(a,1),28(a,1,2,2,1,1))]. given #386 (A,wt=19): 131 f(f(x,x),f(f(y,f(x,x)),f(x,z))) = f(y,f(x,x)). [para(40(a,1),13(a,1,2,2,1))]. given #387 (F,wt=15): 9479 f(x,f(f(x,y),f(z,f(c_0,x)))) = f(x,y). [para(8179(a,1),33(a,1,2,2,2,1))]. given #388 (F,wt=15): 9534 f(f(c_0,f(x,y)),f(f(c_0,x),z)) = f(x,y). [para(15(a,1),8419(a,1,2)),rewrite(8419(5)),flip(a)]. given #389 (T,wt=15): 9536 f(f(c_0,f(x,y)),f(f(x,c_0),z)) = f(x,y). [para(17(a,1),8419(a,1,2)),rewrite(8419(5)),flip(a)]. given #390 (T,wt=15): 9541 f(f(c_0,f(x,y)),f(f(c_0,y),z)) = f(x,y). [para(23(a,1),8419(a,1,2)),rewrite(8419(5)),flip(a)]. given #391 (A,wt=31): 132 f(f(x,y),f(f(f(x,y),f(f(y,f(x,z)),u)),f(v,y))) = f(f(x,y),f(f(y,f(x,z)),u)). [para(13(a,1),11(a,1,1))]. given #392 (F,wt=15): 9543 f(x,f(c_0,f(f(c_0,f(f(c_0,x),y)),z))) = c_0. [para(8419(a,1),52(a,1,1))]. given #393 (F,wt=15): 9549 f(x,f(c_0,f(f(c_0,f(y,f(c_0,x))),z))) = c_0. [para(8419(a,1),269(a,1,1))]. given #394 (T,wt=15): 9552 f(x,f(c_0,f(y,f(c_0,f(f(c_0,x),z))))) = c_0. [para(8419(a,1),344(a,1,1))]. given #395 (T,wt=15): 9553 f(x,f(c_0,f(y,f(c_0,f(z,f(c_0,x)))))) = c_0. [para(8419(a,1),347(a,1,1))]. given #396 (A,wt=23): 133 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(z,x),u)),v))) = x. [para(11(a,1),13(a,1,2,1)),rewrite(11(14))]. given #397 (F,wt=15): 9558 f(x,f(c_0,f(f(c_0,f(f(x,x),y)),z))) = c_0. [para(8423(a,1),52(a,1,1))]. given #398 (F,wt=15): 9560 f(x,f(c_0,f(f(c_0,f(y,f(x,x))),z))) = c_0. [para(8423(a,1),269(a,1,1))]. given #399 (T,wt=15): 9563 f(x,f(c_0,f(y,f(c_0,f(f(x,x),z))))) = c_0. [para(8423(a,1),344(a,1,1))]. given #400 (T,wt=15): 9564 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0. [para(8423(a,1),347(a,1,1))]. given #401 (A,wt=31): 134 f(f(x,y),f(f(y,z),f(f(x,y),f(f(y,f(x,u)),v)))) = f(f(x,y),f(f(y,f(x,u)),v)). [para(13(a,1),12(a,1,1))]. given #402 (F,wt=15): 9620 f(x,f(c_0,f(f(c_0,f(f(x,c_0),y)),z))) = c_0. [para(8425(a,1),52(a,1,1))]. given #403 (F,wt=15): 9623 f(x,f(c_0,f(f(c_0,f(y,f(x,c_0))),z))) = c_0. [para(8425(a,1),269(a,1,1))]. given #404 (T,wt=15): 9626 f(x,f(c_0,f(y,f(c_0,f(f(x,c_0),z))))) = c_0. [para(8425(a,1),344(a,1,1))]. given #405 (T,wt=15): 9627 f(x,f(c_0,f(y,f(c_0,f(z,f(x,c_0)))))) = c_0. [para(8425(a,1),347(a,1,1))]. given #406 (A,wt=23): 135 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(x,z),u)),v))) = z. [para(12(a,1),13(a,1,2,1)),rewrite(12(14))]. given #407 (F,wt=15): 9638 f(x,f(f(f(c_0,x),y),f(x,z))) = f(x,z). [para(8446(a,2),47(a,1,2,1,1))]. given #408 (F,wt=15): 9639 f(x,f(f(y,x),f(f(c_0,x),z))) = f(y,x). [para(8446(a,2),60(a,1,2,2,1))]. given #409 (T,wt=15): 9640 f(x,f(f(y,x),f(z,f(c_0,x)))) = f(y,x). [para(8446(a,2),63(a,1,2,2,2))]. given #410 (T,wt=15): 9642 f(x,f(f(f(c_0,x),y),f(z,x))) = f(z,x). [para(8446(a,2),64(a,1,2,1,1))]. given #411 (A,wt=23): 136 f(f(x,y),f(f(f(x,z),f(x,y)),f(y,u))) = f(f(x,z),f(x,y)). [para(12(a,1),13(a,1,2,2,1))]. given #412 (F,wt=15): 9646 f(x,f(f(y,f(c_0,x)),f(x,z))) = f(x,z). [para(8446(a,2),109(a,1,2,1,2))]. given #413 (F,wt=15): 9647 f(x,f(f(y,f(c_0,x)),f(z,x))) = f(z,x). [para(8446(a,2),112(a,1,2,1,2))]. given #414 (T,wt=15): 9648 f(f(x,f(y,f(z,y))),f(x,f(c_0,z))) = x. [para(8446(a,2),209(a,1,2,2))]. given #415 (T,wt=15): 9649 f(f(f(x,f(y,x)),z),f(z,f(c_0,y))) = z. [para(8446(a,2),219(a,1,2,2))]. given #416 (A,wt=39): 138 f(f(x,f(y,z)),f(z,f(f(x,f(y,z)),f(f(f(y,z),f(x,u)),v)))) = f(f(x,f(y,z)),f(f(f(y,z),f(x,u)),v)). [para(13(a,1),18(a,1,1)),rewrite(1(10))]. given #417 (F,wt=15): 9650 f(f(f(c_0,x),y),f(y,f(z,f(x,z)))) = y. [para(8446(a,2),226(a,1,1,1))]. given #418 (F,wt=15): 9651 f(f(x,f(y,f(z,y))),f(f(c_0,z),x)) = x. [para(8446(a,2),229(a,1,2,1))]. given #419 (T,wt=15): 9652 f(f(x,f(c_0,y)),f(f(z,f(y,z)),x)) = x. [para(8446(a,2),234(a,1,1,2))]. given #420 (T,wt=15): 9654 f(f(f(x,f(y,x)),z),f(f(c_0,y),z)) = z. [para(8446(a,2),237(a,1,2,1))]. given #421 (A,wt=23): 139 f(f(x,y),f(f(f(z,y),f(x,y)),f(x,u))) = f(f(z,y),f(x,y)). [para(19(a,1),13(a,1,2,2,1))]. given #422 (F,wt=15): 9655 f(f(x,f(y,f(y,z))),f(x,f(c_0,z))) = x. [para(8446(a,2),242(a,1,2,2))]. given #423 (F,wt=15): 9657 f(f(f(x,f(x,y)),z),f(z,f(c_0,y))) = z. [para(8446(a,2),248(a,1,2,2))]. given #424 (T,wt=15): 9658 f(f(f(c_0,x),y),f(y,f(z,f(z,x)))) = y. [para(8446(a,2),253(a,1,1,1))]. given #425 (T,wt=15): 9659 f(f(x,f(y,f(y,z))),f(f(c_0,z),x)) = x. [para(8446(a,2),255(a,1,2,1))]. given #426 (A,wt=37): 140 f(f(f(x,y),f(f(y,f(x,z)),u)),f(f(x,y),f(f(f(f(x,y),f(f(y,f(x,z)),u)),f(y,v)),w))) = f(x,y). [para(13(a,1),13(a,1,2,1)),rewrite(13(22))]. given #427 (F,wt=15): 9660 f(f(x,f(c_0,y)),f(f(z,f(z,y)),x)) = x. [para(8446(a,2),259(a,1,1,2))]. given #428 (F,wt=15): 9667 f(f(f(x,f(x,y)),z),f(f(c_0,y),z)) = z. [para(8446(a,2),263(a,1,2,1))]. given #429 (T,wt=15): 9852 f(f(x,x),f(c_0,y)) = f(f(y,y),f(x,c_0)). [back_rewrite(8849),rewrite(9634(4,R))]. given #430 (T,wt=15): 9986 f(f(x,x),f(c_0,y)) = f(f(y,y),f(c_0,x)). [back_rewrite(1062),rewrite(9634(4,R),9634(8,R))]. given #431 (A,wt=25): 141 f(f(x,f(y,z)),f(f(z,f(x,f(y,z))),f(x,u))) = f(z,f(x,f(y,z))). [para(31(a,1),8(a,1,2,2,1)),rewrite(1(5),1(11))]. given #432 (F,wt=15): 9991 f(f(x,y),f(c_0,z)) = f(f(z,z),f(x,y)). [back_rewrite(1042),rewrite(9634(4,R))]. given #433 (F,wt=15): 10085 f(f(c_0,f(x,y)),f(z,f(x,c_0))) = f(x,y). [para(66(a,1),8419(a,1,2)),rewrite(8419(5)),flip(a)]. given #434 (T,wt=15): 10194 f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x). [para(354(a,1),67(a,1,2)),flip(a)]. given #435 (T,wt=15): 10197 f(f(f(x,c_0),y),f(c_0,f(x,z))) = f(x,z). [para(67(a,1),8419(a,1,2)),rewrite(8419(5)),flip(a)]. given #436 (A,wt=19): 142 f(x,f(f(y,f(z,x)),f(x,f(u,z)))) = f(x,f(u,z)). [para(31(a,1),18(a,1,2)),rewrite(1(6))]. given #437 (F,wt=15): 10330 f(x,f(f(c_0,f(f(c_0,x),y)),z)) = f(c_0,x). [para(9505(a,1),49(a,1)),rewrite(8419(6)),flip(a)]. given #438 (F,wt=15): 10335 f(f(x,f(y,z)),f(c_0,f(x,f(x,y)))) = c_0. [para(2(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #439 (T,wt=15): 10337 f(f(x,f(y,z)),f(c_0,f(x,f(y,x)))) = c_0. [para(5(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #440 (T,wt=15): 10339 f(f(x,f(y,z)),f(c_0,f(x,f(x,z)))) = c_0. [para(6(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #441 (A,wt=19): 144 f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y). [para(44(a,1),11(a,1,1))]. given #442 (F,wt=15): 10341 f(f(f(x,y),z),f(c_0,f(z,f(z,x)))) = c_0. [para(7(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #443 (F,wt=15): 10344 f(f(x,y),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(10(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #444 (T,wt=15): 10346 f(f(x,f(y,z)),f(c_0,f(x,f(z,x)))) = c_0. [para(11(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #445 (T,wt=15): 10348 f(f(f(x,y),z),f(c_0,f(z,f(x,z)))) = c_0. [para(12(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #446 (A,wt=19): 145 f(f(x,x),f(f(x,y),f(f(x,x),z))) = f(f(x,x),z). [para(44(a,1),12(a,1,1))]. given #447 (F,wt=15): 10349 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0. [para(16(a,1),8366(a,1,2,2,2)),rewrite(1(5),9631(5,R))]. given #448 (F,wt=15): 10351 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0. [para(18(a,1),8366(a,1,2,2,2)),rewrite(1(5),9631(5,R))]. given #449 (T,wt=15): 10352 f(f(f(x,y),z),f(c_0,f(z,f(z,y)))) = c_0. [para(19(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #450 (T,wt=15): 10355 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(31(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #451 (A,wt=25): 147 f(f(f(x,x),y),f(f(x,x),f(f(f(f(x,x),y),f(x,z)),u))) = f(x,x). [para(44(a,1),13(a,1,2,1)),rewrite(44(13))]. given #452 (F,wt=15): 10357 f(f(f(x,y),z),f(c_0,f(z,f(y,z)))) = c_0. [para(70(a,1),8366(a,1,2,2,2)),rewrite(1(5))]. given #453 (F,wt=15): 10361 f(x,f(c_0,f(f(c_0,f(y,f(y,x))),z))) = c_0. [para(8366(a,1),22(a,1,2,1)),rewrite(8366(13))]. given #454 (T,wt=15): 10363 f(f(c_0,f(x,f(x,y))),f(c_0,f(y,z))) = c_0. [para(8366(a,1),25(a,1,2,1)),rewrite(8366(13))]. given #455 (T,wt=15): 10366 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0. [para(8366(a,1),27(a,1,2,1)),rewrite(8366(13))]. given #456 (A,wt=19): 149 f(f(x,x),f(f(y,f(x,x)),f(z,x))) = f(y,f(x,x)). [para(61(a,1),11(a,1,1))]. given #457 (F,wt=15): 10370 f(f(c_0,f(x,f(x,y))),f(c_0,f(z,y))) = c_0. [para(8366(a,1),76(a,1,2,1)),rewrite(8366(13))]. given #458 (F,wt=15): 10412 f(f(x,f(y,f(z,y))),f(c_0,f(x,z))) = c_0. [para(226(a,1),8366(a,1,2,2,2)),rewrite(1(7),9631(7,R),8423(7))]. given #459 (T,wt=15): 10414 f(f(f(x,f(y,x)),z),f(c_0,f(z,y))) = c_0. [para(234(a,1),8366(a,1,2,2,2)),rewrite(1(7),825(7))]. given #460 (T,wt=15): 10422 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0. [para(253(a,1),8366(a,1,2,2,2)),rewrite(1(7),9631(7,R),8423(7))]. given #461 (A,wt=19): 150 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)). [para(61(a,1),12(a,1,1))]. given #462 (F,wt=15): 10423 f(f(f(x,f(x,y)),z),f(c_0,f(z,y))) = c_0. [para(259(a,1),8366(a,1,2,2,2)),rewrite(1(7),825(7))]. given #463 (F,wt=15): 10496 f(f(x,y),f(c_0,f(x,f(x,f(y,z))))) = c_0. [para(2(a,1),8382(a,1,2,2,2)),rewrite(1(5))]. given #464 (T,wt=15): 10499 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0. [para(6(a,1),8382(a,1,2,2,2)),rewrite(1(5))]. given #465 (T,wt=15): 10504 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(12(a,1),8382(a,1,2,2,2)),rewrite(1(5),9631(5,R))]. given #466 (A,wt=25): 152 f(f(x,f(y,y)),f(f(y,y),f(f(f(x,f(y,y)),f(y,z)),u))) = f(y,y). [para(61(a,1),13(a,1,2,1)),rewrite(61(13))]. given #467 (F,wt=15): 10508 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(70(a,1),8382(a,1,2,2,2)),rewrite(1(5),9631(5,R))]. given #468 (F,wt=15): 10512 f(x,f(c_0,f(f(c_0,f(y,f(x,y))),z))) = c_0. [para(8382(a,1),22(a,1,2,1)),rewrite(8382(13))]. given #469 (T,wt=15): 10513 f(x,f(c_0,f(f(x,y),f(c_0,f(y,z))))) = c_0. [para(22(a,1),8382(a,1,2,2,2)),rewrite(1(6),9634(6,R))]. given #470 (T,wt=15): 10514 f(f(c_0,f(x,f(y,x))),f(c_0,f(y,z))) = c_0. [para(8382(a,1),25(a,1,2,1)),rewrite(8382(13))]. given #471 (A,wt=17): 153 f(x,f(f(y,x),f(f(f(z,y),x),u))) = f(y,x). [para(70(a,1),2(a,1,1))]. given #472 (F,wt=15): 10515 f(x,f(c_0,f(f(y,x),f(c_0,f(y,z))))) = c_0. [para(25(a,1),8382(a,1,2,2,2)),rewrite(1(6),9634(6,R))]. given #473 (F,wt=15): 10517 f(x,f(c_0,f(y,f(c_0,f(z,f(x,z)))))) = c_0. [para(8382(a,1),27(a,1,2,1)),rewrite(8382(13))]. given #474 (T,wt=15): 10518 f(x,f(c_0,f(f(x,y),f(c_0,f(z,y))))) = c_0. [para(27(a,1),8382(a,1,2,2,2)),rewrite(1(6),9634(6,R))]. given #475 (T,wt=15): 10519 f(f(c_0,f(x,f(y,x))),f(c_0,f(z,y))) = c_0. [para(8382(a,1),76(a,1,2,1)),rewrite(8382(13))]. given #476 (A,wt=19): 154 f(x,f(f(y,f(x,z)),f(x,f(z,u)))) = f(x,f(z,u)). [para(2(a,1),70(a,1,1))]. given #477 (F,wt=15): 10520 f(x,f(c_0,f(f(y,x),f(c_0,f(z,y))))) = c_0. [para(76(a,1),8382(a,1,2,2,2)),rewrite(1(6),9634(6,R))]. given #478 (F,wt=15): 10533 f(x,f(c_0,f(f(y,y),f(f(y,z),x)))) = c_0. [para(90(a,1),8382(a,1,2,2,2)),rewrite(1(7),569(7,R),1(5))]. given #479 (T,wt=15): 10534 f(x,f(c_0,f(f(y,y),f(f(z,y),x)))) = c_0. [para(106(a,1),8382(a,1,2,2,2)),rewrite(1(7),569(7,R),1(5))]. given #480 (T,wt=15): 10631 f(f(f(x,x),y),f(f(f(x,c_0),z),y)) = y. [para(8402(a,1),12(a,1,1))]. given #481 (A,wt=19): 155 f(x,f(f(f(y,z),x),f(f(z,x),u))) = f(f(y,z),x). [para(70(a,1),5(a,1,1))]. given #482 (F,wt=15): 10650 f(f(f(x,x),y),f(f(z,f(x,c_0)),y)) = y. [para(8402(a,1),70(a,1,1))]. given #483 (F,wt=15): 10660 f(x,f(f(y,c_0),z)) = f(x,f(f(y,y),z)). [para(8402(a,1),15(a,2,2)),rewrite(15(10))]. given #484 (T,wt=15): 10705 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(y,y)). [para(8402(a,1),569(a,1)),rewrite(8426(9,R)),flip(a)]. given #485 (T,wt=15): 10706 f(f(x,c_0),f(y,y)) = f(f(x,x),f(y,c_0)). [para(8402(a,2),569(a,1)),rewrite(8426(8,R))]. given #486 (A,wt=17): 156 f(x,f(f(y,x),f(z,f(f(u,y),x)))) = f(y,x). [para(70(a,1),6(a,1,1))]. given #487 (F,wt=15): 10719 f(f(x,c_0),f(c_0,y)) = f(f(x,x),f(y,y)). [para(8402(a,1),588(a,1)),rewrite(9634(9,R)),flip(a)]. given #488 (F,wt=15): 10720 f(f(x,c_0),f(y,y)) = f(f(x,x),f(c_0,y)). [para(8402(a,2),588(a,1)),rewrite(9634(8,R))]. given #489 (T,wt=15): 10773 f(f(f(x,c_0),y),z) = f(f(f(x,x),y),z). [para(8402(a,2),90(a,1,2,2,1)),rewrite(10772(7))]. given #490 (T,wt=15): 11117 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,y))). [para(8404(a,2),15(a,1,2,1,2)),rewrite(23(8))]. given #491 (A,wt=19): 157 f(x,f(f(y,f(x,z)),f(x,f(u,z)))) = f(x,f(u,z)). [para(6(a,1),70(a,1,1))]. given #492 (F,wt=15): 11124 f(f(x,c_0),f(y,c_0)) = f(f(y,y),f(x,x)). [para(8404(a,1),569(a,1)),rewrite(8426(9,R)),flip(a)]. given #493 (F,wt=15): 11128 f(f(x,c_0),f(c_0,y)) = f(f(y,y),f(x,x)). [para(8404(a,1),588(a,1)),rewrite(9634(9,R)),flip(a)]. given #494 (T,wt=15): 11142 f(f(f(x,c_0),y),z) = f(f(y,f(x,x)),z). [para(8404(a,1),90(a,1,2,2,1)),rewrite(10777(7)),flip(a)]. given #495 (T,wt=15): 11214 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(c_0,x)). [para(8404(a,1),56(a,1,2,1)),rewrite(10756(9))]. given #496 (A,wt=21): 158 f(f(x,y),f(y,f(f(f(x,y),f(f(f(z,x),y),u)),v))) = y. [para(70(a,1),8(a,1,2,1)),rewrite(70(13))]. given #497 (F,wt=15): 11247 f(f(x,c_0),f(y,y)) = f(f(y,c_0),f(x,x)). [para(8404(a,2),8402(a,2))]. given #498 (F,wt=15): 11251 f(f(x,f(y,z)),f(x,f(y,f(z,c_0)))) = x. [para(8416(a,1),6(a,1,2,2)),rewrite(1(7))]. given #499 (T,wt=15): 11254 f(f(f(x,f(y,c_0)),z),f(z,f(x,y))) = z. [para(8416(a,1),11(a,1,2,2))]. given #500 (T,wt=15): 11256 f(f(f(x,y),z),f(z,f(x,f(y,c_0)))) = z. [para(8416(a,1),18(a,1,1,1))]. given #501 (A,wt=23): 159 f(f(x,y),f(f(f(x,y),f(z,x)),f(y,u))) = f(f(x,y),f(z,x)). [para(70(a,1),8(a,1,2,2,1))]. given #502 (F,wt=15): 11258 f(f(x,f(y,f(z,c_0))),f(f(y,z),x)) = x. [para(8416(a,1),19(a,1,2,1))]. given #503 (F,wt=15): 11260 f(f(x,f(y,z)),f(f(y,f(z,c_0)),x)) = x. [para(8416(a,1),31(a,1,1,2))]. given #504 (T,wt=15): 11262 f(f(f(x,y),z),f(f(x,f(y,c_0)),z)) = z. [para(8416(a,1),70(a,1,2,1)),rewrite(1(7))]. given #505 (T,wt=15): 11307 f(f(f(f(x,c_0),y),z),f(z,f(z,x))) = z. [para(8416(a,1),357(a,1,2,2))]. given #506 (A,wt=31): 160 f(f(x,y),f(f(z,x),f(f(x,y),f(f(x,f(y,u)),v)))) = f(f(x,y),f(f(x,f(y,u)),v)). [para(8(a,1),70(a,1,1))]. given #507 (F,wt=15): 11309 f(f(f(x,f(y,c_0)),z),f(z,f(z,y))) = z. [para(8416(a,1),359(a,1,2,2))]. given #508 (F,wt=15): 11315 f(f(x,f(f(y,c_0),z)),f(x,f(x,y))) = x. [para(8416(a,1),420(a,1,2,2))]. given #509 (T,wt=15): 11317 f(f(x,f(y,f(z,c_0))),f(x,f(x,z))) = x. [para(8416(a,1),422(a,1,2,2))]. given #510 (T,wt=15): 11326 f(f(x,f(x,y)),f(x,f(f(y,c_0),z))) = x. [para(8418(a,1),5(a,1,1))]. given #511 (A,wt=19): 161 f(x,f(f(f(y,z),x),f(u,f(z,x)))) = f(f(y,z),x). [para(70(a,1),11(a,1,1))]. given #512 (F,wt=15): 11332 f(f(x,f(y,z)),f(x,f(f(z,c_0),y))) = x. [para(8418(a,2),6(a,1,2,2))]. given #513 (F,wt=15): 11347 f(f(f(x,y),z),f(z,f(f(y,c_0),x))) = z. [para(8418(a,2),11(a,1,2,2))]. given #514 (T,wt=15): 11349 f(f(x,f(x,y)),f(f(f(y,c_0),z),x)) = x. [para(8418(a,1),12(a,1,1))]. given #515 (T,wt=15): 11354 f(f(f(f(x,c_0),y),z),f(z,f(y,x))) = z. [para(8418(a,2),18(a,1,1,1))]. given #516 (A,wt=19): 162 f(x,f(f(f(y,x),z),f(f(u,y),x))) = f(f(u,y),x). [para(70(a,1),12(a,1,1))]. given #517 (F,wt=15): 11356 f(f(x,f(y,z)),f(f(f(z,c_0),y),x)) = x. [para(8418(a,2),19(a,1,2,1))]. given #518 (F,wt=15): 11365 f(f(x,f(f(y,c_0),z)),f(f(z,y),x)) = x. [para(8418(a,2),31(a,1,1,2))]. given #519 (T,wt=15): 11369 f(f(f(x,y),z),f(f(f(y,c_0),x),z)) = z. [para(8418(a,2),70(a,1,2,1))]. given #520 (T,wt=15): 11374 f(x,f(f(y,c_0),z)) = f(x,f(z,f(z,y))). [para(8418(a,2),15(a,1,2,1,2)),rewrite(23(8))]. given #521 (A,wt=19): 163 f(x,f(f(y,f(z,x)),f(f(z,u),x))) = f(f(z,u),x). [para(12(a,1),70(a,1,1))]. given #522 (F,wt=15): 11460 f(f(f(x,c_0),y),z) = f(f(y,f(y,x)),z). [para(8418(a,2),90(a,1,2,2,1)),rewrite(106(6))]. given #523 (F,wt=15): 11653 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(c_0,y)). [para(8418(a,1),8404(a,2)),rewrite(9634(9,R))]. given #524 (T,wt=15): 11661 f(x,f(y,f(z,c_0))) = f(x,f(y,f(y,z))). [para(8422(a,1),15(a,1,2,1,2)),rewrite(15(7)),flip(a)]. given #525 (T,wt=15): 11674 f(f(x,f(y,c_0)),z) = f(f(x,f(x,y)),z). [para(8422(a,1),90(a,1,2,2,1)),rewrite(90(5)),flip(a)]. given #526 (A,wt=23): 164 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(y,z),u)),v))) = z. [para(70(a,1),13(a,1,2,1)),rewrite(70(14))]. given #527 (F,wt=15): 11711 f(f(x,c_0),f(c_0,y)) = f(f(x,x),f(y,c_0)). [para(8422(a,1),8402(a,1)),rewrite(9634(6,R))]. given #528 (F,wt=15): 11717 f(f(x,c_0),f(c_0,y)) = f(f(y,c_0),f(x,x)). [para(8422(a,1),8404(a,1)),rewrite(9634(6,R))]. given #529 (T,wt=15): 11815 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,z))). [para(8424(a,2),15(a,1,2,1,2)),rewrite(23(8))]. given #530 (T,wt=15): 11872 f(f(f(x,c_0),y),z) = f(f(y,f(x,y)),z). [para(8424(a,2),90(a,1,2,2,1)),rewrite(106(6))]. given #531 (A,wt=23): 165 f(f(x,y),f(f(f(z,x),f(x,y)),f(y,u))) = f(f(z,x),f(x,y)). [para(70(a,1),13(a,1,2,2,1))]. given #532 (F,wt=15): 12017 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,y))). [para(8426(a,1),15(a,1,2,1,2)),rewrite(15(7)),flip(a)]. given #533 (F,wt=15): 12044 f(f(x,f(y,c_0)),z) = f(f(x,f(y,x)),z). [para(8426(a,1),90(a,1,2,2,1)),rewrite(90(5)),flip(a)]. given #534 (T,wt=15): 12115 f(f(f(c_0,x),y),f(c_0,f(x,z))) = f(x,z). [para(15(a,1),8430(a,1,2)),rewrite(9534(14))]. given #535 (T,wt=15): 12118 f(f(f(c_0,x),y),f(c_0,f(z,x))) = f(z,x). [para(23(a,1),8430(a,1,2)),rewrite(9541(14))]. given #536 (A,wt=31): 166 f(f(x,y),f(f(z,y),f(f(x,y),f(f(y,f(x,u)),v)))) = f(f(x,y),f(f(y,f(x,u)),v)). [para(13(a,1),70(a,1,1))]. given #537 (F,wt=15): 12133 f(f(x,f(y,c_0)),f(c_0,f(y,z))) = f(y,z). [para(66(a,1),8430(a,1,2)),rewrite(10085(14))]. given #538 (F,wt=15): 12148 f(f(c_0,f(x,y)),f(z,f(c_0,x))) = f(x,y). [para(72(a,1),8419(a,1,2)),rewrite(8419(5)),flip(a)]. given #539 (T,wt=15): 12157 f(f(x,f(c_0,y)),f(c_0,f(y,z))) = f(y,z). [para(72(a,1),8430(a,1,2)),rewrite(12148(14))]. given #540 (T,wt=15): 12159 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,z))). [para(8431(a,1),15(a,1,2,1,2)),rewrite(15(7)),flip(a)]. given #541 (A,wt=19): 167 f(f(x,x),f(f(y,x),f(f(x,x),z))) = f(f(x,x),z). [para(44(a,1),70(a,1,1))]. given #542 (F,wt=15): 12167 f(f(x,f(y,c_0)),z) = f(f(x,f(y,y)),z). [para(8431(a,1),90(a,1,2,2,1)),rewrite(90(5)),flip(a)]. given #543 (F,wt=15): 12252 f(f(c_0,f(x,y)),f(f(y,c_0),z)) = f(x,y). [para(73(a,1),8419(a,1,2)),rewrite(8419(5)),flip(a)]. given #544 (T,wt=15): 12263 f(f(f(x,c_0),y),f(c_0,f(z,x))) = f(z,x). [para(73(a,1),8430(a,1,2)),rewrite(12252(14))]. given #545 (T,wt=15): 12425 f(f(f(x,x),y),f(f(f(c_0,x),z),y)) = y. [para(9497(a,1),237(a,1,1,1,2)),rewrite(1(7),8419(7),1(7))]. given #546 (A,wt=19): 168 f(f(x,x),f(f(y,x),f(z,f(x,x)))) = f(z,f(x,x)). [para(61(a,1),70(a,1,1))]. given #547 (F,wt=15): 12480 f(f(c_0,f(x,y)),f(z,f(c_0,y))) = f(x,y). [para(77(a,1),8419(a,1,2)),rewrite(8419(5)),flip(a)]. given #548 (F,wt=15): 12486 f(f(x,f(c_0,y)),f(c_0,f(z,y))) = f(z,y). [para(77(a,1),8430(a,1,2)),rewrite(12480(14))]. given #549 (T,wt=15): 12513 f(f(f(x,x),y),f(f(z,f(c_0,x)),y)) = y. [para(9629(a,2),70(a,1,2,1))]. given #550 (T,wt=15): 12514 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,z))). [para(9629(a,1),15(a,1,2,1,2)),rewrite(15(7)),flip(a)]. given #551 (A,wt=19): 169 f(x,f(f(y,f(z,x)),f(f(u,z),x))) = f(f(u,z),x). [para(70(a,1),70(a,1,1))]. given #552 (F,wt=15): 12543 f(f(c_0,x),f(y,c_0)) = f(f(y,y),f(x,x)). [para(9629(a,1),587(a,1)),rewrite(8426(9,R)),flip(a)]. given #553 (F,wt=15): 12546 f(f(c_0,x),f(c_0,y)) = f(f(y,y),f(x,x)). [para(9629(a,1),740(a,1)),rewrite(9634(9,R)),flip(a)]. given #554 (T,wt=15): 12559 f(f(x,f(c_0,y)),z) = f(f(x,f(y,y)),z). [para(9629(a,1),90(a,1,2,2,1)),rewrite(90(5)),flip(a)]. given #555 (T,wt=15): 12693 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,x)). [para(9629(a,1),8404(a,1)),flip(a)]. given #556 (A,wt=33): 170 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(x,y),u)),f(x,v))) = f(f(x,f(y,z)),f(f(x,y),u)). [para(15(a,1),5(a,1,1))]. given #557 (F,wt=15): 12694 f(f(c_0,x),f(c_0,y)) = f(f(y,c_0),f(x,x)). [para(9629(a,1),8418(a,1)),rewrite(9634(10,R)),flip(a)]. given #558 (F,wt=15): 12738 f(f(f(x,y),z),f(f(y,f(c_0,x)),z)) = z. [para(9631(a,2),70(a,1,2,1))]. given #559 (T,wt=15): 12739 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,y))). [para(9631(a,1),15(a,1,2,1,2)),rewrite(15(7)),flip(a)]. given #560 (T,wt=15): 12793 f(f(x,f(c_0,y)),z) = f(f(x,f(y,x)),z). [para(9631(a,1),90(a,1,2,2,1)),rewrite(90(5)),flip(a)]. given #561 (A,wt=23): 171 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(f(x,y),v))))) = x. [para(15(a,1),6(a,1,1))]. given #562 (F,wt=15): 12920 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,c_0)). [para(9631(a,1),8404(a,1)),rewrite(8426(6,R)),flip(a)]. given #563 (F,wt=15): 12948 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,z))). [para(9633(a,2),15(a,1,2,1,2)),rewrite(23(8))]. given #564 (T,wt=15): 12982 f(f(f(c_0,x),y),z) = f(f(y,f(x,y)),z). [para(9633(a,2),90(a,1,2,2,1)),rewrite(106(6))]. given #565 (T,wt=15): 13064 f(f(c_0,x),f(y,c_0)) = f(f(c_0,y),f(x,x)). [para(9633(a,1),9629(a,1)),rewrite(8426(6,R))]. given #566 (A,wt=31): 173 f(f(x,y),f(f(f(x,y),f(f(x,f(z,y)),u)),f(x,v))) = f(f(x,y),f(f(x,f(z,y)),u)). [para(6(a,1),15(a,1,2,2,1))]. given #567 (F,wt=15): 13108 f(x,f(y,f(c_0,z))) = f(x,f(y,f(y,z))). [para(9634(a,1),15(a,1,2,1,2)),rewrite(15(7)),flip(a)]. given #568 (F,wt=15): 13147 f(f(x,f(c_0,y)),z) = f(f(x,f(x,y)),z). [para(9634(a,1),90(a,1,2,2,1)),rewrite(90(5)),flip(a)]. given #569 (T,wt=15): 13267 f(x,f(f(c_0,y),z)) = f(x,f(z,f(z,y))). [para(9636(a,2),15(a,1,2,1,2)),rewrite(23(8))]. given #570 (T,wt=15): 13280 f(f(f(c_0,x),y),z) = f(f(y,f(y,x)),z). [para(9636(a,2),90(a,1,2,2,1)),rewrite(106(6))]. given #571 (A,wt=41): 174 f(f(f(x,y),f(z,u)),f(x,f(f(f(x,y),f(z,u)),f(f(f(x,y),z),v)))) = f(f(f(x,y),f(z,u)),f(f(f(x,y),z),v)). [para(15(a,1),7(a,1,2)),rewrite(1(8),1(12))]. given #572 (F,wt=15): 13311 f(f(c_0,f(x,y)),f(z,f(y,c_0))) = f(x,y). [para(363(a,1),9637(a,1,2)),rewrite(1(5),8419(5)),flip(a)]. given #573 (F,wt=15): 13329 f(x,f(f(c_0,y),z)) = f(x,f(f(y,y),z)). [para(9643(a,1),15(a,2,2)),rewrite(15(10))]. given #574 (T,wt=15): 13343 f(f(c_0,x),f(y,c_0)) = f(f(x,x),f(y,y)). [para(9643(a,1),569(a,1)),rewrite(8426(9,R)),flip(a)]. given #575 (T,wt=15): 13344 f(f(c_0,x),f(y,y)) = f(f(x,x),f(y,c_0)). [para(9643(a,2),569(a,1)),rewrite(8426(8,R))]. given #576 (A,wt=17): 175 f(f(x,y),f(x,f(f(f(x,y),f(y,z)),u))) = x. [para(7(a,1),15(a,1,2,1)),rewrite(7(11))]. given #577 (F,wt=15): 13345 f(f(c_0,x),f(c_0,y)) = f(f(x,x),f(y,y)). [para(9643(a,1),588(a,1)),rewrite(9634(9,R)),flip(a)]. given #578 (F,wt=15): 13346 f(f(c_0,x),f(y,y)) = f(f(x,x),f(c_0,y)). [para(9643(a,2),588(a,1)),rewrite(9634(8,R))]. given #579 (T,wt=15): 13364 f(f(f(c_0,x),y),z) = f(f(f(x,x),y),z). [para(9643(a,2),90(a,1,2,2,1)),rewrite(12981(7))]. given #580 (T,wt=15): 13406 f(f(c_0,x),f(c_0,y)) = f(f(x,x),f(y,c_0)). [para(9643(a,1),8422(a,1)),rewrite(9634(10,R)),flip(a)]. given #581 (A,wt=31): 176 f(f(x,y),f(f(f(x,y),f(f(f(y,z),x),u)),f(x,v))) = f(f(x,y),f(f(f(y,z),x),u)). [para(7(a,1),15(a,1,2,2,1))]. given #582 (F,wt=15): 13407 f(f(c_0,x),f(y,c_0)) = f(f(x,x),f(c_0,y)). [para(9643(a,2),8422(a,1)),rewrite(9634(9,R))]. given #583 (F,wt=15): 13421 f(x,f(f(y,y),z)) = f(x,f(z,f(c_0,y))). [para(9644(a,2),15(a,1,2,1,2)),rewrite(23(7))]. given #584 (T,wt=15): 13422 f(f(f(x,x),y),z) = f(f(y,f(c_0,x)),z). [para(9644(a,1),90(a,1,2,2,1)),rewrite(12984(7)),flip(a)]. given #585 (T,wt=15): 13431 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,y))). [para(9645(a,2),15(a,1,2,1,2)),rewrite(23(8))]. given #586 (A,wt=27): 178 f(f(x,y),f(f(f(x,y),f(f(x,x),z)),f(x,u))) = f(f(x,y),f(f(x,x),z)). [para(39(a,1),15(a,1,2,2,1))]. given #587 (F,wt=15): 13432 f(f(f(c_0,x),y),z) = f(f(y,f(x,x)),z). [para(9645(a,1),90(a,1,2,2,1)),rewrite(13367(7)),flip(a)]. given #588 (F,wt=15): 13436 f(f(c_0,x),f(y,y)) = f(f(c_0,y),f(x,x)). [para(9645(a,1),9629(a,1))]. given #589 (T,wt=15): 13446 f(f(x,y),f(c_0,f(f(c_0,f(y,x)),z))) = c_0. [para(10377(a,1),22(a,1,2,1)),rewrite(10377(13))]. given #590 (T,wt=15): 13448 f(f(x,y),f(c_0,f(z,f(c_0,f(y,x))))) = c_0. [para(10377(a,1),27(a,1,2,1)),rewrite(10377(13))]. given #591 (A,wt=31): 179 f(x,f(f(x,f(y,z)),f(f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v)),w))) = f(x,f(y,z)). [para(15(a,1),8(a,1,2,1)),rewrite(15(18))]. given #592 (F,wt=15): 13457 f(f(x,f(c_0,f(y,z))),f(x,f(z,y))) = x. [para(10377(a,1),242(a,1,1,2,2)),rewrite(1(3),8446(11,R),8419(9))]. given #593 (F,wt=15): 13458 f(f(f(c_0,f(x,y)),z),f(f(y,x),z)) = z. [para(10377(a,1),263(a,1,1,1,2)),rewrite(1(3),8446(11,R),8419(9))]. given #594 (T,wt=15): 13488 f(x,f(f(y,y),z)) = f(x,f(z,f(y,c_0))). [para(10599(a,1),15(a,1,2,1,2)),rewrite(12164(9)),flip(a)]. given #595 (T,wt=15): 13489 f(f(f(x,x),y),z) = f(f(y,f(x,c_0)),z). [para(10599(a,1),90(a,1,2,2,1)),rewrite(10776(7)),flip(a)]. given #596 (A,wt=39): 180 f(x,f(f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v)),f(f(x,y),w))) = f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v)). [para(8(a,1),15(a,1,2,2,1))]. given #597 (F,wt=15): 13493 f(x,f(f(c_0,f(f(x,c_0),y)),z)) = f(x,c_0). [para(82(a,1),9505(a,1)),rewrite(8425(4))]. given #598 (F,wt=15): 13495 f(f(c_0,f(f(x,x),y)),f(y,f(x,y))) = c_0. [para(569(a,1),13437(a,1,2))]. given #599 (T,wt=15): 13496 f(f(c_0,f(x,f(y,y))),f(x,f(y,x))) = c_0. [para(569(a,2),13437(a,1,1,2)),rewrite(1(6))]. given #600 (T,wt=15): 13499 f(f(c_0,f(f(x,x),y)),f(y,f(y,x))) = c_0. [para(588(a,1),13437(a,1,2))]. given #601 (A,wt=27): 181 f(f(x,y),f(f(f(x,y),f(f(y,y),z)),f(y,u))) = f(f(x,y),f(f(y,y),z)). [para(45(a,1),15(a,1,2,2,1))]. given #602 (F,wt=15): 13500 f(f(c_0,f(x,f(y,y))),f(x,f(x,y))) = c_0. [para(588(a,2),13437(a,1,1,2)),rewrite(1(6))]. given #603 (F,wt=15): 13502 f(f(c_0,f(f(x,x),y)),f(y,f(x,c_0))) = c_0. [para(8402(a,1),13437(a,1,1,2))]. given #604 (T,wt=15): 13503 f(f(c_0,f(x,f(y,c_0))),f(f(y,y),x)) = c_0. [para(8402(a,1),13437(a,1,2))]. given #605 (T,wt=15): 13504 f(f(c_0,f(f(x,c_0),y)),f(y,f(x,x))) = c_0. [para(8402(a,2),13437(a,1,1,2))]. given #606 (A,wt=19): 182 f(f(x,f(y,z)),f(x,f(f(y,f(x,f(y,z))),u))) = x. [para(10(a,1),15(a,1,2,1)),rewrite(1(5),10(12))]. given #607 (F,wt=15): 13505 f(f(c_0,f(x,f(y,y))),f(f(y,c_0),x)) = c_0. [para(8402(a,2),13437(a,1,2))]. given #608 (F,wt=15): 13506 f(f(c_0,f(x,f(y,y))),f(x,f(y,c_0))) = c_0. [para(8404(a,1),13437(a,1,1,2))]. given #609 (T,wt=15): 13507 f(f(c_0,f(x,f(y,c_0))),f(x,f(y,y))) = c_0. [para(8404(a,1),13437(a,1,2))]. given #610 (T,wt=15): 13508 f(f(c_0,f(f(x,c_0),y)),f(f(x,x),y)) = c_0. [para(8404(a,2),13437(a,1,1,2))]. given #611 (A,wt=33): 183 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(y,x),u)),f(x,v))) = f(f(x,f(y,z)),f(f(y,x),u)). [para(10(a,1),15(a,1,2,2,1))]. given #612 (F,wt=15): 13509 f(f(c_0,f(f(x,x),y)),f(f(x,c_0),y)) = c_0. [para(8404(a,2),13437(a,1,2))]. given #613 (F,wt=15): 13511 f(f(c_0,f(x,f(y,c_0))),f(x,f(x,y))) = c_0. [para(8418(a,1),13437(a,1,2))]. given #614 (T,wt=15): 13512 f(f(c_0,f(f(x,c_0),y)),f(y,f(y,x))) = c_0. [para(8418(a,2),13437(a,1,1,2)),rewrite(1(7))]. given #615 (T,wt=15): 13515 f(f(c_0,f(x,f(y,c_0))),f(x,f(y,x))) = c_0. [para(8424(a,1),13437(a,1,2))]. given #616 (A,wt=33): 184 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(x,y),u)),f(v,x))) = f(f(x,f(y,z)),f(f(x,y),u)). [para(15(a,1),11(a,1,1))]. given #617 (F,wt=15): 13516 f(f(c_0,f(f(x,c_0),y)),f(y,f(x,y))) = c_0. [para(8424(a,2),13437(a,1,1,2)),rewrite(1(7))]. given #618 (F,wt=15): 13518 f(f(c_0,f(x,f(y,y))),f(f(c_0,y),x)) = c_0. [para(9629(a,1),13437(a,1,1,2))]. given #619 (T,wt=15): 13519 f(f(c_0,f(f(c_0,x),y)),f(y,f(x,x))) = c_0. [para(9629(a,1),13437(a,1,2))]. given #620 (T,wt=15): 13520 f(f(c_0,f(x,f(c_0,y))),f(f(y,y),x)) = c_0. [para(9629(a,2),13437(a,1,1,2))]. given #621 (A,wt=31): 185 f(f(x,y),f(f(f(x,y),f(f(y,f(z,x)),u)),f(y,v))) = f(f(x,y),f(f(y,f(z,x)),u)). [para(11(a,1),15(a,1,2,2,1))]. given #622 (F,wt=15): 13521 f(f(c_0,f(f(x,x),y)),f(y,f(c_0,x))) = c_0. [para(9629(a,2),13437(a,1,2))]. given #623 (F,wt=15): 13523 f(f(c_0,f(f(c_0,x),y)),f(y,f(x,y))) = c_0. [para(9631(a,1),13437(a,1,2))]. given #624 (T,wt=15): 13524 f(f(c_0,f(x,f(c_0,y))),f(x,f(y,x))) = c_0. [para(9631(a,2),13437(a,1,1,2)),rewrite(1(7))]. given #625 (T,wt=15): 13527 f(f(c_0,f(f(c_0,x),y)),f(y,f(y,x))) = c_0. [para(9634(a,1),13437(a,1,2))]. given #626 (A,wt=33): 186 f(f(x,f(y,z)),f(f(x,u),f(f(x,f(y,z)),f(f(x,y),v)))) = f(f(x,f(y,z)),f(f(x,y),v)). [para(15(a,1),12(a,1,1))]. given #627 (F,wt=15): 13528 f(f(c_0,f(x,f(c_0,y))),f(x,f(x,y))) = c_0. [para(9634(a,2),13437(a,1,1,2)),rewrite(1(7))]. given #628 (F,wt=15): 13530 f(f(c_0,f(x,f(c_0,y))),f(x,f(y,y))) = c_0. [para(9644(a,1),13437(a,1,1,2))]. given #629 (T,wt=15): 13531 f(f(c_0,f(x,f(y,y))),f(x,f(c_0,y))) = c_0. [para(9644(a,1),13437(a,1,2))]. given #630 (T,wt=15): 13532 f(f(c_0,f(f(x,x),y)),f(f(c_0,x),y)) = c_0. [para(9644(a,2),13437(a,1,1,2))]. given #631 (A,wt=17): 187 f(f(x,y),f(y,f(f(f(x,y),f(x,z)),u))) = y. [para(12(a,1),15(a,1,2,1)),rewrite(12(11))]. given #632 (F,wt=15): 13533 f(f(c_0,f(f(c_0,x),y)),f(f(x,x),y)) = c_0. [para(9644(a,2),13437(a,1,2))]. given #633 (F,wt=15): 13538 f(f(c_0,f(x,y)),f(x,f(z,f(x,y)))) = c_0. [para(2(a,1),8452(a,1,2,2)),rewrite(8446(3,R),1(6))]. given #634 (T,wt=15): 13539 f(f(c_0,f(x,y)),f(y,f(z,f(x,y)))) = c_0. [para(5(a,1),8452(a,1,2,2)),rewrite(8446(3,R),1(6))]. given #635 (T,wt=15): 13543 f(x,f(f(y,f(x,x)),f(f(x,x),z))) = c_0. [para(35(a,1),8452(a,1,1))]. given #636 (A,wt=31): 188 f(f(x,y),f(f(f(x,y),f(f(f(x,z),y),u)),f(y,v))) = f(f(x,y),f(f(f(x,z),y),u)). [para(12(a,1),15(a,1,2,2,1))]. given #637 (F,wt=15): 13544 f(f(c_0,f(x,y)),f(x,f(f(x,y),z))) = c_0. [para(35(a,1),8452(a,1,2,1)),rewrite(8446(3,R))]. given #638 (F,wt=15): 13545 f(f(c_0,f(x,y)),f(y,f(f(x,y),z))) = c_0. [para(40(a,1),8452(a,1,2,1)),rewrite(8446(3,R))]. given #639 (T,wt=15): 13553 f(x,f(f(y,f(x,y)),f(f(x,x),z))) = c_0. [para(569(a,1),8452(a,1,2,1)),rewrite(8446(3,R),8423(3))]. given #640 (T,wt=15): 13555 f(x,f(f(y,f(x,x)),f(z,f(x,z)))) = c_0. [para(587(a,1),8452(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #641 (A,wt=33): 190 f(f(f(x,y),z),f(f(f(f(x,y),z),f(f(z,x),u)),f(z,v))) = f(f(f(x,y),z),f(f(z,x),u)). [para(16(a,1),15(a,1,2,2,1))]. given #642 (F,wt=15): 13557 f(x,f(f(y,f(y,x)),f(f(x,x),z))) = c_0. [para(588(a,1),8452(a,1,2,1)),rewrite(8446(3,R),8423(3))]. given #643 (F,wt=15): 13559 f(x,f(f(y,f(x,x)),f(z,f(z,x)))) = c_0. [para(740(a,1),8452(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #644 (T,wt=15): 13572 f(x,f(f(y,f(x,c_0)),f(f(x,c_0),z))) = c_0. [para(8444(a,1),8452(a,1,1))]. given #645 (T,wt=15): 13573 f(x,f(f(y,f(c_0,x)),f(f(c_0,x),z))) = c_0. [para(9473(a,1),8452(a,1,1))]. given #646 (A,wt=41): 191 f(f(f(x,y),f(z,u)),f(y,f(f(f(x,y),f(z,u)),f(f(f(x,y),z),v)))) = f(f(f(x,y),f(z,u)),f(f(f(x,y),z),v)). [para(15(a,1),18(a,1,1)),rewrite(1(11))]. given #647 (F,wt=15): 13574 f(x,f(f(y,f(x,c_0)),f(f(x,x),z))) = c_0. [para(8402(a,1),8452(a,1,2,2)),rewrite(8446(5,R),8425(4))]. given #648 (F,wt=15): 13575 f(x,f(f(y,f(x,x)),f(f(x,c_0),z))) = c_0. [para(8402(a,2),8452(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #649 (T,wt=15): 13576 f(x,f(f(y,f(x,c_0)),f(z,f(x,x)))) = c_0. [para(8404(a,1),8452(a,1,2,2)),rewrite(8446(5,R),8425(4))]. given #650 (T,wt=15): 13577 f(x,f(f(f(x,c_0),y),f(f(x,x),z))) = c_0. [para(8404(a,2),8452(a,1,2,1)),rewrite(8446(3,R),8423(3))]. given #651 (A,wt=33): 192 f(f(f(x,y),z),f(f(f(f(x,y),z),f(f(z,y),u)),f(z,v))) = f(f(f(x,y),z),f(f(z,y),u)). [para(18(a,1),15(a,1,2,2,1))]. given #652 (F,wt=15): 13579 f(x,f(f(y,f(x,c_0)),f(z,f(z,x)))) = c_0. [para(8418(a,1),8452(a,1,2,2)),rewrite(8446(5,R),8425(4))]. given #653 (F,wt=15): 13581 f(x,f(f(y,f(y,x)),f(f(x,c_0),z))) = c_0. [para(8422(a,1),8452(a,1,2,1)),rewrite(8446(5,R),8425(4))]. given #654 (T,wt=15): 13583 f(x,f(f(y,f(x,c_0)),f(z,f(x,z)))) = c_0. [para(8424(a,1),8452(a,1,2,2)),rewrite(8446(5,R),8425(4))]. given #655 (T,wt=15): 13585 f(x,f(f(y,f(x,y)),f(f(x,c_0),z))) = c_0. [para(8426(a,1),8452(a,1,2,1)),rewrite(8446(5,R),8425(4))]. given #656 (A,wt=17): 193 f(f(x,y),f(x,f(f(f(x,y),f(z,y)),u))) = x. [para(19(a,1),15(a,1,2,1)),rewrite(19(11))]. given #657 (F,wt=15): 13589 f(x,f(f(y,f(x,x)),f(f(c_0,x),z))) = c_0. [para(9629(a,1),8452(a,1,2,1)),rewrite(8446(5,R),8419(4))]. given #658 (F,wt=15): 13590 f(x,f(f(y,f(c_0,x)),f(f(x,x),z))) = c_0. [para(9629(a,2),8452(a,1,2,1)),rewrite(8446(3,R),8423(3))]. given #659 (T,wt=15): 13591 f(x,f(f(y,f(x,y)),f(f(c_0,x),z))) = c_0. [para(9631(a,1),8452(a,1,2,1)),rewrite(8446(5,R),8419(4))]. given #660 (T,wt=15): 13593 f(x,f(f(y,f(c_0,x)),f(z,f(x,z)))) = c_0. [para(9633(a,1),8452(a,1,2,2)),rewrite(8446(5,R),8419(4))]. given #661 (A,wt=31): 194 f(f(x,y),f(f(f(x,y),f(f(f(z,y),x),u)),f(x,v))) = f(f(x,y),f(f(f(z,y),x),u)). [para(19(a,1),15(a,1,2,2,1))]. given #662 (F,wt=15): 13595 f(x,f(f(y,f(y,x)),f(f(c_0,x),z))) = c_0. [para(9634(a,1),8452(a,1,2,1)),rewrite(8446(5,R),8419(4))]. given #663 (F,wt=15): 13597 f(x,f(f(y,f(c_0,x)),f(z,f(z,x)))) = c_0. [para(9636(a,1),8452(a,1,2,2)),rewrite(8446(5,R),8419(4))]. given #664 (T,wt=15): 13600 f(x,f(f(y,f(x,x)),f(z,f(c_0,x)))) = c_0. [para(9644(a,1),8452(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #665 (T,wt=15): 13601 f(x,f(f(f(x,x),y),f(f(c_0,x),z))) = c_0. [para(9644(a,2),8452(a,1,2,1)),rewrite(8446(5,R),8419(4))]. given #666 (A,wt=41): 195 f(f(f(x,f(y,z)),f(f(x,y),u)),f(f(x,f(y,z)),f(f(f(f(x,f(y,z)),f(f(x,y),u)),f(x,v)),w))) = f(x,f(y,z)). [para(15(a,1),13(a,1,2,1)),rewrite(15(23))]. given #667 (F,wt=15): 13602 f(x,f(f(y,f(c_0,x)),f(z,f(x,x)))) = c_0. [para(9645(a,1),8452(a,1,2,2)),rewrite(8446(5,R),8419(4))]. given #668 (F,wt=15): 13603 f(x,f(f(f(c_0,x),y),f(f(x,x),z))) = c_0. [para(9645(a,2),8452(a,1,2,1)),rewrite(8446(3,R),8423(3))]. given #669 (T,wt=15): 13604 f(x,f(f(y,f(x,x)),f(z,f(x,c_0)))) = c_0. [para(10599(a,1),8452(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #670 (T,wt=15): 13605 f(x,f(f(f(x,x),y),f(f(x,c_0),z))) = c_0. [para(10599(a,2),8452(a,1,2,1)),rewrite(8446(5,R),8425(4))]. given #671 (A,wt=39): 196 f(x,f(f(x,f(f(f(y,x),f(f(x,f(y,z)),u)),v)),f(f(y,x),w))) = f(x,f(f(f(y,x),f(f(x,f(y,z)),u)),v)). [para(13(a,1),15(a,1,2,2,1))]. given #672 (F,wt=15): 13609 f(x,f(f(f(x,x),y),f(f(x,x),z))) = c_0. [para(35(a,1),8453(a,1,1))]. given #673 (F,wt=15): 13615 f(x,f(f(f(x,x),y),f(z,f(x,z)))) = c_0. [para(587(a,1),8453(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #674 (T,wt=15): 13616 f(x,f(f(f(x,x),y),f(z,f(z,x)))) = c_0. [para(740(a,1),8453(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #675 (T,wt=15): 13630 f(x,f(f(f(x,c_0),y),f(f(x,c_0),z))) = c_0. [para(8444(a,1),8453(a,1,1))]. given #676 (A,wt=19): 198 f(f(x,f(y,z)),f(x,f(f(z,f(x,f(y,z))),u))) = x. [para(31(a,1),15(a,1,2,1)),rewrite(1(5),31(12))]. given #677 (F,wt=15): 13631 f(x,f(f(f(c_0,x),y),f(f(c_0,x),z))) = c_0. [para(9473(a,1),8453(a,1,1))]. given #678 (F,wt=15): 13632 f(x,f(f(f(x,c_0),y),f(z,f(x,x)))) = c_0. [para(8404(a,1),8453(a,1,2,2)),rewrite(8446(5,R),8425(4))]. given #679 (T,wt=15): 13633 f(x,f(f(f(x,c_0),y),f(z,f(z,x)))) = c_0. [para(8418(a,1),8453(a,1,2,2)),rewrite(8446(5,R),8425(4))]. given #680 (T,wt=15): 13634 f(x,f(f(f(x,c_0),y),f(z,f(x,z)))) = c_0. [para(8424(a,1),8453(a,1,2,2)),rewrite(8446(5,R),8425(4))]. given #681 (A,wt=33): 199 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(z,x),u)),f(x,v))) = f(f(x,f(y,z)),f(f(z,x),u)). [para(31(a,1),15(a,1,2,2,1))]. given #682 (F,wt=15): 13635 f(x,f(f(f(c_0,x),y),f(z,f(x,z)))) = c_0. [para(9633(a,1),8453(a,1,2,2)),rewrite(8446(5,R),8419(4))]. given #683 (F,wt=15): 13636 f(x,f(f(f(c_0,x),y),f(z,f(z,x)))) = c_0. [para(9636(a,1),8453(a,1,2,2)),rewrite(8446(5,R),8419(4))]. given #684 (T,wt=15): 13637 f(x,f(f(f(x,x),y),f(z,f(c_0,x)))) = c_0. [para(9644(a,1),8453(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #685 (T,wt=15): 13638 f(x,f(f(f(c_0,x),y),f(z,f(x,x)))) = c_0. [para(9645(a,1),8453(a,1,2,2)),rewrite(8446(5,R),8419(4))]. given #686 (A,wt=33): 201 f(f(x,f(y,z)),f(f(u,x),f(f(x,f(y,z)),f(f(x,y),v)))) = f(f(x,f(y,z)),f(f(x,y),v)). [para(15(a,1),70(a,1,1))]. given #687 (F,wt=15): 13639 f(x,f(f(f(x,x),y),f(z,f(x,c_0)))) = c_0. [para(10599(a,1),8453(a,1,2,2)),rewrite(8446(3,R),8423(3))]. given #688 (F,wt=15): 13640 f(f(x,y),f(x,f(f(c_0,f(y,z)),u))) = x. [para(9502(a,1),6(a,1,2,2)),rewrite(1(7))]. given #689 (T,wt=15): 13642 f(f(f(f(c_0,f(x,y)),z),u),f(u,x)) = u. [para(9502(a,1),11(a,1,2,2))]. given #690 (T,wt=15): 13643 f(f(x,y),f(y,f(f(c_0,f(x,z)),u))) = y. [para(9502(a,1),18(a,1,1,1))]. given #691 (A,wt=17): 202 f(f(x,y),f(y,f(f(f(x,y),f(z,x)),u))) = y. [para(70(a,1),15(a,1,2,1)),rewrite(70(11))]. given #692 (F,wt=15): 13645 f(f(x,f(f(c_0,f(y,z)),u)),f(y,x)) = x. [para(9502(a,1),19(a,1,2,1))]. given #693 (F,wt=15): 13646 f(f(x,y),f(f(f(c_0,f(y,z)),u),x)) = x. [para(9502(a,1),31(a,1,1,2))]. given #694 (T,wt=15): 13647 f(f(x,y),f(f(f(c_0,f(x,z)),u),y)) = y. [para(9502(a,1),70(a,1,2,1)),rewrite(1(7))]. given #695 (T,wt=15): 13648 f(x,f(f(c_0,f(y,f(x,y))),z)) = f(x,x). [para(587(a,1),9502(a,1,2,1,2)),rewrite(8423(3))]. given #696 (A,wt=31): 203 f(f(x,y),f(f(f(x,y),f(f(f(z,x),y),u)),f(y,v))) = f(f(x,y),f(f(f(z,x),y),u)). [para(70(a,1),15(a,1,2,2,1))]. given #697 (F,wt=15): 13650 f(x,f(f(c_0,f(y,f(y,x))),z)) = f(x,x). [para(740(a,1),9502(a,1,2,1,2)),rewrite(8423(3))]. given #698 (F,wt=15): 13666 f(f(x,y),f(x,f(z,f(c_0,f(y,u))))) = x. [para(9502(a,1),363(a,1,2,2)),rewrite(1(7))]. given #699 (T,wt=15): 13670 f(f(f(x,f(c_0,f(y,z))),u),f(u,y)) = u. [para(9502(a,1),433(a,1,2,2))]. given #700 (T,wt=15): 13672 f(x,f(f(c_0,f(y,f(x,x))),z)) = f(x,c_0). [para(8404(a,1),9502(a,1,2,1,2)),rewrite(8425(4))]. given #701 (A,wt=41): 204 f(x,f(f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v)),f(f(x,f(y,z)),w))) = f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v)). [para(15(a,1),15(a,1,2,2,1))]. given #702 (F,wt=15): 13675 f(x,f(f(c_0,f(y,f(c_0,x))),z)) = f(x,x). [para(9644(a,1),9502(a,1,2,1,2)),rewrite(8423(3))]. given #703 (F,wt=15): 13676 f(x,f(f(c_0,f(y,f(x,c_0))),z)) = f(x,x). [para(10599(a,1),9502(a,1,2,1,2)),rewrite(8423(3))]. given #704 (T,wt=15): 13683 f(f(x,f(y,c_0)),f(c_0,f(z,y))) = f(z,y). [para(83(a,1),8430(a,1,2)),rewrite(13311(14))]. given #705 (T,wt=15): 13686 f(f(x,y),f(x,f(f(c_0,f(z,y)),u))) = x. [para(9538(a,1),6(a,1,2,2)),rewrite(1(7))]. given #706 (A,wt=19): 207 f(f(x,x),f(f(y,f(x,y)),f(x,z))) = f(y,f(x,y)). [para(200(a,1),5(a,1,1))]. given #707 (F,wt=15): 13688 f(f(f(f(c_0,f(x,y)),z),u),f(u,y)) = u. [para(9538(a,1),11(a,1,2,2))]. given #708 (F,wt=15): 13690 f(f(x,y),f(y,f(f(c_0,f(z,x)),u))) = y. [para(9538(a,1),18(a,1,1,1))]. given #709 (T,wt=15): 13692 f(f(x,f(f(c_0,f(y,z)),u)),f(z,x)) = x. [para(9538(a,1),19(a,1,2,1))]. given #710 (T,wt=15): 13693 f(f(x,y),f(f(f(c_0,f(z,y)),u),x)) = x. [para(9538(a,1),31(a,1,1,2))]. given #711 (A,wt=19): 218 f(f(x,x),f(f(y,f(x,y)),f(z,x))) = f(y,f(x,y)). [para(200(a,1),11(a,1,1))]. given #712 (F,wt=15): 13696 f(f(x,y),f(f(f(c_0,f(z,x)),u),y)) = y. [para(9538(a,1),70(a,1,2,1)),rewrite(1(7))]. given #713 (F,wt=15): 13722 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x. [para(9538(a,1),363(a,1,2,2)),rewrite(1(7))]. given #714 (T,wt=15): 13726 f(f(f(x,f(c_0,f(y,z))),u),f(u,z)) = u. [para(9538(a,1),433(a,1,2,2))]. given #715 (T,wt=15): 13748 f(f(x,y),f(y,f(z,f(c_0,f(x,u))))) = y. [para(9540(a,1),18(a,1,1,1))]. given #716 (A,wt=19): 221 f(f(x,x),f(f(x,y),f(z,f(x,z)))) = f(z,f(x,z)). [para(200(a,1),12(a,1,1))]. given #717 (F,wt=15): 13750 f(f(x,f(y,f(c_0,f(z,u)))),f(z,x)) = x. [para(9540(a,1),19(a,1,2,1))]. given #718 (F,wt=15): 13751 f(f(x,y),f(f(z,f(c_0,f(y,u))),x)) = x. [para(9540(a,1),31(a,1,1,2))]. given #719 (T,wt=15): 13752 f(f(x,y),f(f(z,f(c_0,f(x,u))),y)) = y. [para(9540(a,1),70(a,1,2,1)),rewrite(1(7))]. given #720 (T,wt=15): 13753 f(x,f(y,f(c_0,f(f(x,c_0),z)))) = f(x,c_0). [para(569(a,2),9540(a,1,1)),rewrite(8423(3))]. given #721 (A,wt=25): 232 f(f(x,f(y,x)),f(f(y,y),f(f(f(x,f(y,x)),f(y,z)),u))) = f(y,y). [para(200(a,1),13(a,1,2,1)),rewrite(200(13))]. given #722 (F,wt=15): 13754 f(x,f(y,f(c_0,f(z,f(x,z))))) = f(x,x). [para(587(a,1),9540(a,1,2,2,2)),rewrite(8423(3))]. given #723 (F,wt=15): 13755 f(x,f(y,f(c_0,f(f(c_0,x),z)))) = f(c_0,x). [para(588(a,2),9540(a,1,1)),rewrite(8423(3))]. given #724 (T,wt=15): 13757 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x). [para(740(a,1),9540(a,1,2,2,2)),rewrite(8423(3))]. given #725 (T,wt=15): 13778 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,c_0). [para(8404(a,1),9540(a,1,2,2,2)),rewrite(8425(4))]. given #726 (A,wt=19): 236 f(f(x,x),f(f(y,x),f(z,f(x,z)))) = f(z,f(x,z)). [para(200(a,1),70(a,1,1))]. given #727 (F,wt=15): 13781 f(x,f(y,f(c_0,f(z,f(c_0,x))))) = f(x,x). [para(9644(a,1),9540(a,1,2,2,2)),rewrite(8423(3))]. given #728 (F,wt=15): 13782 f(x,f(y,f(c_0,f(z,f(x,c_0))))) = f(x,x). [para(10599(a,1),9540(a,1,2,2,2)),rewrite(8423(3))]. given #729 (T,wt=15): 13789 f(f(x,y),f(y,f(z,f(c_0,f(u,x))))) = y. [para(9545(a,1),18(a,1,1,1))]. given #730 (T,wt=15): 13791 f(f(x,f(y,f(c_0,f(z,u)))),f(u,x)) = x. [para(9545(a,1),19(a,1,2,1))]. given #731 (A,wt=19): 241 f(f(x,x),f(f(y,f(y,x)),f(x,z))) = f(y,f(y,x)). [para(205(a,1),5(a,1,1))]. given #732 (F,wt=15): 13792 f(f(x,y),f(f(z,f(c_0,f(u,y))),x)) = x. [para(9545(a,1),31(a,1,1,2))]. given #733 (F,wt=15): 13795 f(f(x,y),f(f(z,f(c_0,f(u,x))),y)) = y. [para(9545(a,1),70(a,1,2,1)),rewrite(1(7))]. given #734 (T,wt=15): 13846 f(f(c_0,f(x,y)),f(f(x,x),z)) = f(x,y). [para(9666(a,1),32(a,1,2)),rewrite(1(4),8429(4)),flip(a)]. given #735 (T,wt=15): 13847 f(f(c_0,f(x,y)),f(z,f(x,x))) = f(x,y). [para(9666(a,1),79(a,1,2)),rewrite(1(4),8429(4)),flip(a)]. given #736 (A,wt=19): 247 f(f(x,x),f(f(y,f(y,x)),f(z,x))) = f(y,f(y,x)). [para(205(a,1),11(a,1,1))]. given #737 (F,wt=15): 13905 f(f(c_0,f(x,y)),f(f(y,x),z)) = f(x,y). [para(11818(a,1),9538(a,1,2,1,2)),rewrite(8419(8))]. given #738 (F,wt=15): 13906 f(f(c_0,f(x,y)),f(z,f(y,x))) = f(x,y). [para(11818(a,1),9545(a,1,2,2,2)),rewrite(8419(8))]. given #739 (T,wt=15): 13909 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x). [para(354(a,1),86(a,1,2)),flip(a)]. given #740 (T,wt=15): 13934 f(f(x,f(y,z)),f(c_0,f(z,y))) = f(z,y). [para(11818(a,1),12372(a,1,1,2,2)),rewrite(8419(5),1(5))]. given #741 (A,wt=19): 249 f(f(x,x),f(f(x,y),f(z,f(z,x)))) = f(z,f(z,x)). [para(205(a,1),12(a,1,1))]. given #742 (F,wt=15): 13936 f(f(c_0,f(x,y)),f(z,f(z,x))) = f(x,y). [para(2(a,1),13285(a,1,2,2,2))]. given #743 (F,wt=15): 13937 f(f(c_0,f(x,y)),f(z,f(z,y))) = f(x,y). [para(5(a,1),13285(a,1,2,2,2))]. given #744 (T,wt=15): 13938 f(f(x,y),f(x,f(z,f(z,f(y,u))))) = x. [para(13285(a,1),6(a,1,2,2)),rewrite(1(6))]. given #745 (T,wt=15): 13940 f(f(f(x,f(x,f(y,z))),u),f(u,y)) = u. [para(13285(a,1),11(a,1,2,2))]. given #746 (A,wt=25): 257 f(f(x,f(x,y)),f(f(y,y),f(f(f(x,f(x,y)),f(y,z)),u))) = f(y,y). [para(205(a,1),13(a,1,2,1)),rewrite(205(13))]. given #747 (F,wt=15): 13941 f(f(c_0,f(x,y)),f(z,f(x,z))) = f(x,y). [para(12(a,1),13285(a,1,2,2)),rewrite(1(5))]. given #748 (F,wt=15): 13943 f(f(x,y),f(y,f(z,f(z,f(x,u))))) = y. [para(13285(a,1),18(a,1,1,1))]. given #749 (T,wt=15): 13945 f(f(x,f(y,f(y,f(z,u)))),f(z,x)) = x. [para(13285(a,1),19(a,1,2,1))]. given #750 (T,wt=15): 13946 f(f(x,y),f(f(z,f(z,f(y,u))),x)) = x. [para(13285(a,1),31(a,1,1,2))]. given #751 (A,wt=19): 262 f(f(x,x),f(f(y,x),f(z,f(z,x)))) = f(z,f(z,x)). [para(205(a,1),70(a,1,1))]. given #752 (F,wt=15): 13947 f(f(x,y),f(f(z,f(z,f(x,u))),y)) = y. [para(13285(a,1),70(a,1,2,1)),rewrite(1(6))]. given #753 (F,wt=15): 13948 f(f(c_0,f(x,y)),f(z,f(y,z))) = f(x,y). [para(70(a,1),13285(a,1,2,2)),rewrite(1(5))]. given #754 (T,wt=15): 13949 f(x,f(y,f(y,f(f(x,x),z)))) = f(x,x). [para(569(a,1),13285(a,1,1)),rewrite(8425(4))]. given #755 (T,wt=15): 13950 f(x,f(y,f(y,f(f(x,c_0),z)))) = f(x,c_0). [para(569(a,2),13285(a,1,1)),rewrite(8423(3))]. given #756 (A,wt=17): 268 f(f(x,y),f(x,f(z,f(f(x,y),f(y,u))))) = x. [para(22(a,1),6(a,1,1))]. given #757 (F,wt=15): 13951 f(x,f(y,f(y,f(z,f(x,z))))) = f(x,x). [para(587(a,1),13285(a,1,2,2,2)),rewrite(8423(3))]. given #758 (F,wt=15): 13952 f(x,f(y,f(y,f(f(c_0,x),z)))) = f(c_0,x). [para(588(a,2),13285(a,1,1)),rewrite(8423(3))]. given #759 (T,wt=15): 13954 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x). [para(740(a,1),13285(a,1,2,2,2)),rewrite(8423(3))]. given #760 (T,wt=15): 13974 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,c_0). [para(8404(a,1),13285(a,1,2,2,2)),rewrite(8425(4))]. given #761 (A,wt=27): 270 f(f(f(x,y),z),f(x,f(f(f(x,y),z),f(z,u)))) = f(f(f(x,y),z),f(z,u)). [para(22(a,1),7(a,1,2)),rewrite(1(5),1(8))]. given #762 (F,wt=15): 13979 f(x,f(y,f(y,f(z,f(c_0,x))))) = f(x,x). [para(9644(a,1),13285(a,1,2,2,2)),rewrite(8423(3))]. given #763 (F,wt=15): 13980 f(x,f(y,f(y,f(z,f(x,c_0))))) = f(x,x). [para(10599(a,1),13285(a,1,2,2,2)),rewrite(8423(3))]. given #764 (T,wt=15): 13990 f(x,f(f(y,f(x,x)),f(z,f(x,x)))) = c_0. [para(35(a,1),13534(a,1,1))]. given #765 (T,wt=15): 14000 f(x,f(f(y,f(x,y)),f(z,f(x,x)))) = c_0. [para(569(a,1),13534(a,1,2,1)),rewrite(8446(3,R),8423(3))]. given #766 (A,wt=23): 272 f(x,f(f(x,y),f(f(x,f(f(f(x,y),f(y,z)),u)),v))) = f(x,y). [para(22(a,1),8(a,1,2,1)),rewrite(22(13))]. given #767 (F,wt=15): 14005 f(x,f(f(y,f(y,x)),f(z,f(x,x)))) = c_0. [para(588(a,1),13534(a,1,2,1)),rewrite(8446(3,R),8423(3))]. given #768 (F,wt=15): 14021 f(x,f(f(y,f(x,c_0)),f(z,f(x,c_0)))) = c_0. [para(8444(a,1),13534(a,1,1))]. given #769 (T,wt=15): 14022 f(x,f(f(y,f(c_0,x)),f(z,f(c_0,x)))) = c_0. [para(9473(a,1),13534(a,1,1))]. given #770 (T,wt=15): 14026 f(x,f(f(y,f(y,x)),f(z,f(x,c_0)))) = c_0. [para(8422(a,1),13534(a,1,2,1)),rewrite(8446(5,R),8425(4))]. given #771 (A,wt=23): 273 f(x,f(f(x,y),f(f(f(x,y),f(f(x,f(y,z)),u)),v))) = f(x,y). [para(8(a,1),22(a,1,2,1)),rewrite(8(15))]. given #772 (F,wt=15): 14031 f(x,f(f(y,f(x,y)),f(z,f(x,c_0)))) = c_0. [para(8426(a,1),13534(a,1,2,1)),rewrite(8446(5,R),8425(4))]. given #773 (F,wt=15): 14036 f(x,f(f(y,f(x,y)),f(z,f(c_0,x)))) = c_0. [para(9631(a,1),13534(a,1,2,1)),rewrite(8446(5,R),8419(4))]. given #774 (T,wt=15): 14041 f(x,f(f(y,f(y,x)),f(z,f(c_0,x)))) = c_0. [para(9634(a,1),13534(a,1,2,1)),rewrite(8446(5,R),8419(4))]. given #775 (T,wt=15): 14050 f(x,f(f(f(x,x),y),f(z,f(x,x)))) = c_0. [para(35(a,1),13535(a,1,1))]. given #776 (A,wt=23): 275 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,x))) = f(f(x,y),f(y,z)). [para(22(a,1),11(a,1,1))]. given #777 (F,wt=15): 14068 f(x,f(f(f(x,c_0),y),f(z,f(x,c_0)))) = c_0. [para(8444(a,1),13535(a,1,1))]. given #778 (F,wt=15): 14069 f(x,f(f(f(c_0,x),y),f(z,f(c_0,x)))) = c_0. [para(9473(a,1),13535(a,1,1))]. given #779 (T,wt=15): 14110 f(f(c_0,f(x,y)),f(f(y,y),z)) = f(x,y). [para(13689(a,1),32(a,1,2)),rewrite(1(4),8430(4)),flip(a)]. given #780 (T,wt=15): 14111 f(f(c_0,f(x,y)),f(z,f(y,y))) = f(x,y). [para(13689(a,1),79(a,1,2)),rewrite(1(4),8430(4)),flip(a)]. given #781 (A,wt=23): 277 f(f(x,y),f(f(x,z),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)). [para(22(a,1),12(a,1,1))]. given #782 (F,wt=15): 14119 f(f(x,y),f(x,f(z,f(z,f(u,y))))) = x. [para(13743(a,1),6(a,1,2,2)),rewrite(1(6))]. given #783 (F,wt=15): 14121 f(f(f(x,f(x,f(y,z))),u),f(u,z)) = u. [para(13743(a,1),11(a,1,2,2))]. given #784 (T,wt=15): 14123 f(f(x,y),f(y,f(z,f(z,f(u,x))))) = y. [para(13743(a,1),18(a,1,1,1))]. given #785 (T,wt=15): 14125 f(f(x,f(y,f(y,f(z,u)))),f(u,x)) = x. [para(13743(a,1),19(a,1,2,1))]. given #786 (A,wt=27): 280 f(f(f(x,y),z),f(y,f(f(f(x,y),z),f(z,u)))) = f(f(f(x,y),z),f(z,u)). [para(22(a,1),18(a,1,1)),rewrite(1(7))]. given #787 (F,wt=15): 14126 f(f(x,y),f(f(z,f(z,f(u,y))),x)) = x. [para(13743(a,1),31(a,1,1,2))]. given #788 (F,wt=15): 14127 f(f(x,y),f(f(z,f(z,f(u,x))),y)) = y. [para(13743(a,1),70(a,1,2,1)),rewrite(1(6))]. given #789 (T,wt=15): 14183 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(13849(a,1),588(a,2,2)),rewrite(8446(8,R),1(9),8179(9))]. given #790 (T,wt=15): 14190 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z). [para(2(a,1),13913(a,1,1,2,2)),rewrite(1(5))]. given #791 (A,wt=29): 283 f(f(f(x,y),f(y,z)),f(f(x,y),f(f(f(f(x,y),f(y,z)),f(x,u)),v))) = f(x,y). [para(22(a,1),13(a,1,2,1)),rewrite(22(16))]. given #792 (F,wt=15): 14191 f(f(x,f(x,y)),f(c_0,f(z,y))) = f(z,y). [para(5(a,1),13913(a,1,1,2,2)),rewrite(1(5))]. given #793 (F,wt=15): 14192 f(f(x,f(y,x)),f(c_0,f(y,z))) = f(y,z). [para(12(a,1),13913(a,1,1,2)),rewrite(1(2),1(5))]. given #794 (T,wt=15): 14193 f(f(x,f(y,x)),f(c_0,f(z,y))) = f(z,y). [para(70(a,1),13913(a,1,1,2)),rewrite(1(2),1(5))]. given #795 (T,wt=15): 14262 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(14113(a,1),588(a,2,2)),rewrite(8446(8,R),1(9),8179(9))]. given #796 (A,wt=23): 284 f(x,f(f(y,x),f(f(f(y,x),f(f(x,f(y,z)),u)),v))) = f(y,x). [para(13(a,1),22(a,1,2,1)),rewrite(13(15))]. given #797 (F,wt=15): 14278 f(f(x,f(f(y,y),z)),f(c_0,f(y,x))) = c_0. [para(589(a,1),8366(a,1,2,2,2)),rewrite(1(7),14(7))]. given #798 (F,wt=15): 14303 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0. [para(594(a,1),8366(a,1,2,2,2)),rewrite(1(7),14(7))]. given #799 (T,wt=15): 14358 f(f(x,f(y,z)),f(x,f(f(y,y),u))) = x. [para(42(a,1),596(a,1,1,2)),rewrite(1(8),145(8))]. given #800 (T,wt=15): 14359 f(f(x,f(y,z)),f(x,f(u,f(y,y)))) = x. [para(46(a,1),596(a,1,1,2)),rewrite(1(8),150(8))]. given #801 (A,wt=23): 286 f(f(x,y),f(f(z,x),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)). [para(22(a,1),70(a,1,1))]. given #802 (F,wt=15): 14360 f(f(x,f(y,z)),f(x,f(f(z,z),u))) = x. [para(60(a,1),596(a,1,1,2)),rewrite(1(8),167(8))]. given #803 (F,wt=15): 14361 f(f(x,f(y,z)),f(x,f(u,f(z,z)))) = x. [para(63(a,1),596(a,1,1,2)),rewrite(1(8),168(8))]. given #804 (T,wt=15): 14366 f(f(x,f(f(y,y),z)),f(x,f(y,u))) = x. [para(62(a,1),596(a,1,1,2)),rewrite(8446(10,R),8423(10),1(8),47(8))]. given #805 (T,wt=15): 14400 f(f(c_0,f(x,y)),f(f(f(x,x),z),y)) = c_0. [para(598(a,1),8366(a,1,2,2,2)),rewrite(1(7),14(7),1(7))]. given #806 (A,wt=31): 288 f(x,f(f(x,f(f(f(x,y),f(y,z)),u)),f(f(x,y),v))) = f(x,f(f(f(x,y),f(y,z)),u)). [para(22(a,1),15(a,1,2,2,1))]. given #807 (F,wt=15): 14419 f(f(f(x,y),z),f(z,f(f(x,x),u))) = z. [para(42(a,1),613(a,1,1,1)),rewrite(1(8),145(8))]. given #808 (F,wt=15): 14420 f(f(f(x,y),z),f(z,f(u,f(x,x)))) = z. [para(46(a,1),613(a,1,1,1)),rewrite(1(8),150(8))]. given #809 (T,wt=15): 14421 f(f(f(x,y),z),f(z,f(f(y,y),u))) = z. [para(60(a,1),613(a,1,1,1)),rewrite(1(8),167(8))]. given #810 (T,wt=15): 14422 f(f(f(x,y),z),f(z,f(u,f(y,y)))) = z. [para(63(a,1),613(a,1,1,1)),rewrite(1(8),168(8))]. given #811 (A,wt=27): 289 f(x,f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(x,y),u)),v))) = f(x,f(y,z)). [para(15(a,1),22(a,1,2,1)),rewrite(15(16))]. given #812 (F,wt=15): 14425 f(f(f(f(x,x),y),z),f(z,f(x,u))) = z. [para(62(a,1),613(a,1,1,1)),rewrite(8446(10,R),8423(10),1(8),47(8))]. given #813 (F,wt=15): 14446 f(f(c_0,f(x,y)),f(f(z,f(x,x)),y)) = c_0. [para(624(a,1),8382(a,1,2,2,2)),rewrite(1(7),14(7),1(7))]. given #814 (T,wt=15): 14476 f(f(f(x,f(y,y)),z),f(z,f(y,u))) = z. [para(46(a,1),625(a,1,2,2)),rewrite(1(6),150(6))]. given #815 (T,wt=15): 14477 f(f(f(f(x,x),y),z),f(z,f(u,x))) = z. [para(60(a,1),625(a,1,2,2)),rewrite(1(6),167(6))]. given #816 (A,wt=19): 292 f(x,f(f(x,y),f(f(f(x,y),f(y,z)),u))) = f(x,y). [para(22(a,1),22(a,1,2,1)),rewrite(22(11))]. given #817 (F,wt=15): 14478 f(f(f(x,f(y,y)),z),f(z,f(u,y))) = z. [para(63(a,1),625(a,1,2,2)),rewrite(1(6),168(6))]. given #818 (F,wt=15): 14512 f(f(x,f(y,z)),f(f(f(y,y),u),x)) = x. [para(42(a,1),631(a,1,1,2)),rewrite(1(8),145(8))]. given #819 (T,wt=15): 14513 f(f(x,f(y,z)),f(f(u,f(y,y)),x)) = x. [para(46(a,1),631(a,1,1,2)),rewrite(1(8),150(8))]. given #820 (T,wt=15): 14514 f(f(x,f(y,z)),f(f(f(z,z),u),x)) = x. [para(60(a,1),631(a,1,1,2)),rewrite(1(8),167(8))]. given #821 (A,wt=17): 293 f(f(x,y),f(y,f(z,f(f(x,y),f(x,u))))) = y. [para(25(a,1),6(a,1,1))]. given #822 (F,wt=15): 14515 f(f(x,f(y,z)),f(f(u,f(z,z)),x)) = x. [para(63(a,1),631(a,1,1,2)),rewrite(1(8),168(8))]. given #823 (F,wt=15): 14516 f(f(x,f(f(y,y),z)),f(f(y,u),x)) = x. [para(62(a,1),631(a,1,1,2)),rewrite(8446(10,R),8423(10),1(8),47(8))]. given #824 (T,wt=15): 14529 f(f(x,f(y,f(z,z))),f(f(z,u),x)) = x. [para(46(a,1),638(a,1,2,1)),rewrite(1(6),150(6))]. given #825 (T,wt=15): 14530 f(f(x,f(f(y,y),z)),f(f(u,y),x)) = x. [para(60(a,1),638(a,1,2,1)),rewrite(1(6),167(6))]. given #826 (A,wt=27): 295 f(f(x,f(y,z)),f(y,f(f(x,f(y,z)),f(x,u)))) = f(f(x,f(y,z)),f(x,u)). [para(25(a,1),7(a,1,2)),rewrite(1(5),1(8))]. given #827 (F,wt=15): 14531 f(f(x,f(y,f(z,z))),f(f(u,z),x)) = x. [para(63(a,1),638(a,1,2,1)),rewrite(1(6),168(6))]. given #828 (F,wt=15): 14569 f(f(f(x,y),z),f(f(f(x,x),u),z)) = z. [para(42(a,1),644(a,1,1,1)),rewrite(1(8),145(8))]. given #829 (T,wt=15): 14570 f(f(f(x,y),z),f(f(u,f(x,x)),z)) = z. [para(46(a,1),644(a,1,1,1)),rewrite(1(8),150(8))]. given #830 (T,wt=15): 14571 f(f(f(x,y),z),f(f(f(y,y),u),z)) = z. [para(60(a,1),644(a,1,1,1)),rewrite(1(8),167(8))]. given #831 (A,wt=23): 296 f(x,f(f(y,x),f(f(x,f(f(f(y,x),f(y,z)),u)),v))) = f(y,x). [para(25(a,1),8(a,1,2,1)),rewrite(25(13))]. given #832 (F,wt=15): 14572 f(f(f(x,y),z),f(f(u,f(y,y)),z)) = z. [para(63(a,1),644(a,1,1,1)),rewrite(1(8),168(8))]. given #833 (F,wt=15): 14573 f(f(f(f(x,x),y),z),f(f(x,u),z)) = z. [para(62(a,1),644(a,1,1,1)),rewrite(8446(10,R),8423(10),1(8),47(8))]. given #834 (T,wt=15): 14578 f(f(x,f(y,y)),z) = f(z,f(x,f(y,x))). [para(646(a,1),1(a,1)),flip(a)]. given #835 (T,wt=15): 14579 f(f(x,f(y,x)),z) = f(z,f(x,f(y,y))). [para(646(a,2),1(a,1)),flip(a)]. given #836 (A,wt=23): 297 f(f(f(x,y),f(f(x,f(y,z)),u)),f(f(x,y),f(x,v))) = f(x,y). [para(8(a,1),25(a,1,2,1)),rewrite(8(15))]. given #837 (F,wt=15): 14664 f(f(f(x,x),y),z) = f(z,f(y,f(x,y))). [para(780(a,1),1(a,1)),flip(a)]. given #838 (F,wt=15): 14665 f(f(x,f(y,x)),z) = f(z,f(f(y,y),x)). [para(780(a,2),1(a,1)),flip(a)]. given #839 (T,wt=15): 14769 f(f(x,f(y,y)),z) = f(z,f(x,f(x,y))). [para(854(a,1),1(a,1)),flip(a)]. given #840 (T,wt=15): 14770 f(f(x,f(x,y)),z) = f(z,f(x,f(y,y))). [para(854(a,2),1(a,1)),flip(a)]. given #841 (A,wt=23): 298 f(f(x,y),f(f(f(x,y),f(x,z)),f(u,y))) = f(f(x,y),f(x,z)). [para(25(a,1),11(a,1,1))]. given #842 (F,wt=15): 14862 f(f(x,f(f(y,y),z)),f(x,f(u,y))) = x. [para(46(a,1),897(a,1,1,2)),rewrite(8446(8,R),8423(8),1(8),64(8))]. given #843 (F,wt=15): 14865 f(f(x,f(y,f(z,z))),f(x,f(z,u))) = x. [para(60(a,1),897(a,1,1,2)),rewrite(8446(8,R),8423(8),1(8),109(8))]. given #844 (T,wt=15): 14866 f(f(x,f(y,f(z,z))),f(x,f(u,z))) = x. [para(63(a,1),897(a,1,1,2)),rewrite(8446(8,R),8423(8),1(8),112(8))]. given #845 (T,wt=15): 14926 f(f(f(f(x,x),y),z),f(f(u,x),z)) = z. [para(46(a,1),915(a,1,1,1)),rewrite(8446(8,R),8423(8),1(8),64(8))]. given #846 (A,wt=23): 299 f(f(x,y),f(f(y,z),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)). [para(25(a,1),12(a,1,1))]. given #847 (F,wt=15): 14927 f(f(f(x,f(y,y)),z),f(f(y,u),z)) = z. [para(60(a,1),915(a,1,1,1)),rewrite(8446(8,R),8423(8),1(8),109(8))]. given #848 (F,wt=15): 14928 f(f(f(x,f(y,y)),z),f(f(u,y),z)) = z. [para(63(a,1),915(a,1,1,1)),rewrite(8446(8,R),8423(8),1(8),112(8))]. given #849 (T,wt=15): 14969 f(f(f(x,x),y),z) = f(z,f(y,f(y,x))). [para(1038(a,1),1(a,1)),flip(a)]. given #850 (T,wt=15): 14970 f(f(x,f(x,y)),z) = f(z,f(f(y,y),x)). [para(1038(a,2),1(a,1)),flip(a)]. given #851 (A,wt=27): 301 f(f(x,f(y,z)),f(z,f(f(x,f(y,z)),f(x,u)))) = f(f(x,f(y,z)),f(x,u)). [para(25(a,1),18(a,1,1)),rewrite(1(7))]. given #852 (F,wt=15): 15195 f(x,f(f(c_0,f(y,z)),f(y,x))) = f(x,x). [para(2(a,1),1550(a,1,2,2,1)),rewrite(8446(3,R))]. given #853 (F,wt=15): 15196 f(x,f(f(c_0,f(y,z)),f(z,x))) = f(x,x). [para(5(a,1),1550(a,1,2,2,1)),rewrite(8446(3,R))]. given #854 (T,wt=15): 15198 f(x,f(y,f(f(f(y,y),z),x))) = f(x,x). [para(35(a,1),1550(a,1,2,1))]. given #855 (T,wt=15): 15204 f(x,f(y,f(f(z,f(y,z)),x))) = f(x,x). [para(587(a,1),1550(a,1,2,2,1)),rewrite(8446(3,R),8423(3))]. given #856 (A,wt=29): 302 f(f(f(x,y),f(x,z)),f(f(x,y),f(f(f(f(x,y),f(x,z)),f(y,u)),v))) = f(x,y). [para(25(a,1),13(a,1,2,1)),rewrite(25(16))]. given #857 (F,wt=15): 15205 f(x,f(y,f(f(z,f(z,y)),x))) = f(x,x). [para(740(a,1),1550(a,1,2,2,1)),rewrite(8446(3,R),8423(3))]. given #858 (F,wt=15): 15214 f(x,f(f(c_0,y),f(f(y,z),x))) = f(x,x). [para(8446(a,2),1550(a,1,2,1))]. given #859 (T,wt=15): 15215 f(x,f(f(y,c_0),f(f(y,z),x))) = f(x,x). [para(8455(a,2),1550(a,1,2,1))]. given #860 (T,wt=15): 15216 f(x,f(y,f(f(f(y,c_0),z),x))) = f(x,x). [para(8444(a,1),1550(a,1,2,1))]. given #861 (A,wt=23): 303 f(f(f(x,y),f(f(y,f(x,z)),u)),f(f(x,y),f(y,v))) = f(x,y). [para(13(a,1),25(a,1,2,1)),rewrite(13(15))]. given #862 (F,wt=15): 15217 f(x,f(y,f(f(f(c_0,y),z),x))) = f(x,x). [para(9473(a,1),1550(a,1,2,1))]. given #863 (F,wt=15): 15219 f(x,f(y,f(f(z,f(y,y)),x))) = f(x,x). [para(8404(a,1),1550(a,1,2,2,1)),rewrite(8446(5,R),8425(4))]. given #864 (T,wt=15): 15224 f(x,f(y,f(f(z,f(c_0,y)),x))) = f(x,x). [para(9644(a,1),1550(a,1,2,2,1)),rewrite(8446(3,R),8423(3))]. given #865 (T,wt=15): 15227 f(x,f(y,f(f(z,f(y,c_0)),x))) = f(x,x). [para(10599(a,1),1550(a,1,2,2,1)),rewrite(8446(3,R),8423(3))]. given #866 (A,wt=23): 304 f(f(x,y),f(f(z,y),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)). [para(25(a,1),70(a,1,1))]. given #867 (F,wt=15): 15397 f(x,f(f(y,y),f(x,f(z,y)))) = f(x,x). [para(1(a,1),1607(a,1,2,2))]. given #868 (F,wt=15): 15414 f(x,f(f(c_0,y),f(f(z,y),x))) = f(x,x). [para(8446(a,2),1607(a,1,2,1))]. given #869 (T,wt=15): 15415 f(x,f(f(y,c_0),f(f(z,y),x))) = f(x,x). [para(8455(a,2),1607(a,1,2,1))]. given #870 (T,wt=15): 15532 f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)). [para(1950(a,1),32(a,1,2)),flip(a)]. given #871 (A,wt=31): 306 f(x,f(f(x,f(f(f(y,x),f(y,z)),u)),f(f(y,x),v))) = f(x,f(f(f(y,x),f(y,z)),u)). [para(25(a,1),15(a,1,2,2,1))]. given #872 (F,wt=15): 15569 f(x,f(f(c_0,f(y,z)),f(x,y))) = f(x,x). [para(12119(a,1),1950(a,1,2,2,2))]. given #873 (F,wt=15): 15570 f(x,f(f(c_0,f(y,z)),f(x,z))) = f(x,x). [para(12372(a,1),1950(a,1,2,2,2))]. given #874 (T,wt=15): 15637 f(f(x,f(y,f(z,y))),f(c_0,f(z,x))) = c_0. [para(2151(a,1),8382(a,1,2,2,2)),rewrite(1(7),14(7))]. given #875 (T,wt=15): 15724 f(f(c_0,f(x,y)),f(f(z,f(x,z)),y)) = c_0. [para(2251(a,1),8382(a,1,2,2,2)),rewrite(1(7),14(7),1(7))]. given #876 (A,wt=27): 307 f(f(f(x,f(y,z)),f(f(x,y),u)),f(f(x,f(y,z)),f(x,v))) = f(x,f(y,z)). [para(15(a,1),25(a,1,2,1)),rewrite(15(16))]. given #877 (F,wt=15): 15865 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0. [para(2827(a,1),8382(a,1,2,2,2)),rewrite(1(7),14(7))]. given #878 (F,wt=15): 15973 f(f(c_0,f(x,y)),f(f(z,f(z,x)),y)) = c_0. [para(3026(a,1),8382(a,1,2,2,2)),rewrite(1(7),14(7),1(7))]. given #879 (T,wt=15): 16058 f(x,f(y,f(f(x,y),z))) = f(x,f(y,y)). [para(5676(a,1),32(a,1,2)),flip(a)]. given #880 (T,wt=15): 16223 f(x,f(c_0,f(f(y,y),f(x,f(y,z))))) = c_0. [para(7915(a,1),588(a,2,2)),rewrite(8446(9,R),8179(9))]. given #881 (A,wt=19): 310 f(x,f(f(y,x),f(f(f(y,x),f(y,z)),u))) = f(y,x). [para(25(a,1),22(a,1,2,1)),rewrite(25(11))]. given #882 (F,wt=15): 16224 f(x,f(f(c_0,y),f(x,f(y,z)))) = f(x,x). [para(8446(a,2),7915(a,1,2,1))]. given #883 (F,wt=15): 16225 f(x,f(f(y,c_0),f(x,f(y,z)))) = f(x,x). [para(8455(a,2),7915(a,1,2,1))]. given #884 (T,wt=15): 16226 f(x,f(y,f(x,f(f(y,c_0),z)))) = f(x,x). [para(8444(a,1),7915(a,1,2,1))]. given #885 (T,wt=15): 16228 f(x,f(y,f(x,f(f(c_0,y),z)))) = f(x,x). [para(9473(a,1),7915(a,1,2,1))]. given #886 (A,wt=19): 311 f(f(f(x,y),f(y,z)),f(f(x,y),f(x,u))) = f(x,y). [para(22(a,1),25(a,1,2,1)),rewrite(22(11))]. given #887 (F,wt=15): 16229 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x). [para(8404(a,1),7915(a,1,2,2,2)),rewrite(8446(5,R),8425(4))]. given #888 (F,wt=15): 16230 f(x,f(y,f(x,f(z,f(c_0,y))))) = f(x,x). [para(9644(a,1),7915(a,1,2,2,2)),rewrite(8446(3,R),8423(3))]. given #889 (T,wt=15): 16231 f(x,f(f(x,f(y,z)),f(c_0,y))) = f(x,x). [para(9644(a,1),7915(a,1,2))]. given #890 (T,wt=15): 16232 f(x,f(y,f(x,f(z,f(y,c_0))))) = f(x,x). [para(10599(a,1),7915(a,1,2,2,2)),rewrite(8446(3,R),8423(3))]. given #891 (A,wt=19): 312 f(f(f(x,y),f(x,z)),f(f(x,y),f(y,u))) = f(x,y). [para(25(a,1),25(a,1,2,1)),rewrite(25(11))]. given #892 (F,wt=15): 16257 f(x,f(y,f(f(x,x),z))) = f(x,f(y,y)). [para(7921(a,1),32(a,1,2)),flip(a)]. given #893 (F,wt=15): 16271 f(x,f(y,f(c_0,f(f(x,y),z)))) = f(x,x). [para(7921(a,1),89(a,1)),rewrite(8446(6,R),1(6)),flip(a)]. given #894 (T,wt=15): 16272 f(x,f(y,f(c_0,f(f(y,x),z)))) = f(x,x). [para(7921(a,1),96(a,1)),rewrite(8446(6,R),1(6)),flip(a)]. given #895 (T,wt=15): 16298 f(x,f(y,f(z,f(x,z)))) = f(x,f(y,y)). [para(7941(a,1),32(a,1,2)),flip(a)]. given #896 (A,wt=23): 313 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(f(y,x),v))))) = x. [para(17(a,1),6(a,1,1))]. given #897 (F,wt=15): 16311 f(x,f(y,f(y,f(f(y,x),z)))) = f(x,x). [para(7941(a,1),67(a,1)),rewrite(1(4)),flip(a)]. given #898 (F,wt=15): 16314 f(x,f(f(y,c_0),f(x,f(z,y)))) = f(x,x). [para(8402(a,1),7941(a,1,2,2,2,2)),rewrite(9631(5,R),8423(5))]. given #899 (T,wt=15): 16319 f(x,f(f(c_0,y),f(x,f(z,y)))) = f(x,x). [para(9636(a,1),7941(a,1,2,2,2,2)),rewrite(9(5))]. given #900 (T,wt=15): 16321 f(x,f(f(x,f(y,z)),f(c_0,z))) = f(x,x). [para(9644(a,1),7941(a,1,2)),rewrite(9631(3,R),8423(3))]. given #901 (A,wt=33): 315 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(x,z),u)),f(x,v))) = f(f(x,f(y,z)),f(f(x,z),u)). [para(6(a,1),17(a,1,2,2,1))]. given #902 (F,wt=15): 16323 f(x,f(f(y,z),f(x,f(z,y)))) = f(x,x). [para(10377(a,1),7941(a,1,2,2,2,2)),rewrite(1(6),8419(6))]. given #903 (F,wt=15): 16324 f(x,f(f(x,f(y,z)),f(z,c_0))) = f(x,x). [para(10599(a,1),7941(a,1,2)),rewrite(9631(3,R),8423(3))]. given #904 (T,wt=15): 16326 f(x,f(y,f(y,f(f(x,y),z)))) = f(x,x). [para(7941(a,1),86(a,1)),rewrite(1(4)),flip(a)]. given #905 (T,wt=15): 16334 f(x,f(y,f(y,f(z,f(y,x))))) = f(x,x). [para(7941(a,1),113(a,1)),rewrite(1(4)),flip(a)]. given #906 (A,wt=41): 316 f(f(f(x,y),f(z,u)),f(x,f(f(f(x,y),f(z,u)),f(f(z,f(x,y)),v)))) = f(f(f(x,y),f(z,u)),f(f(z,f(x,y)),v)). [para(17(a,1),7(a,1,2)),rewrite(1(8),1(12))]. given #907 (F,wt=15): 16347 f(x,f(y,f(z,f(z,x)))) = f(x,f(y,y)). [para(7944(a,1),32(a,1,2)),flip(a)]. given #908 (F,wt=15): 16382 f(x,f(c_0,f(f(x,f(y,z)),f(y,c_0)))) = c_0. [para(8326(a,1),588(a,2,2)),rewrite(8446(11,R),8179(10))]. given #909 (T,wt=15): 16545 f(f(f(x,y),z),f(z,f(f(y,x),u))) = z. [para(8647(a,1),15(a,1,2,1)),rewrite(1(8),13905(8),8647(13))]. given #910 (T,wt=15): 16566 f(f(f(x,y),z),f(z,f(u,f(y,x)))) = z. [para(8647(a,1),66(a,1,2,1)),rewrite(13905(8),8647(13))]. given #911 (A,wt=17): 317 f(f(x,y),f(x,f(f(f(y,z),f(x,y)),u))) = x. [para(7(a,1),17(a,1,2,1)),rewrite(7(11))]. given #912 (F,wt=15): 16567 f(f(f(x,y),z),f(f(f(y,x),u),z)) = z. [para(8647(a,1),67(a,1,2,2)),rewrite(13905(8),8647(13))]. given #913 (F,wt=15): 16569 f(f(f(x,y),z),f(c_0,f(z,f(y,x)))) = c_0. [para(8647(a,1),8382(a,1,2,2,2)),rewrite(1(8),9631(8,R),8419(8))]. given #914 (T,wt=15): 16614 f(f(f(x,y),z),f(f(u,f(y,x)),z)) = z. [para(8647(a,1),113(a,1,2,2)),rewrite(13905(8),8647(13))]. given #915 (T,wt=15): 16622 f(f(x,f(y,z)),f(x,f(f(z,y),u))) = x. [para(8655(a,1),15(a,1,2,1)),rewrite(13934(8),8655(13))]. given #916 (A,wt=31): 318 f(x,f(f(x,f(y,z)),f(f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v)),w))) = f(x,f(y,z)). [para(17(a,1),8(a,1,2,1)),rewrite(17(18))]. given #917 (F,wt=15): 16635 f(f(x,f(y,z)),f(x,f(u,f(z,y)))) = x. [para(8655(a,1),66(a,1,2,1)),rewrite(13906(8),8655(13))]. given #918 (F,wt=15): 16636 f(f(x,f(y,z)),f(f(f(z,y),u),x)) = x. [para(8655(a,1),67(a,1,2,2)),rewrite(13906(8),8655(13))]. given #919 (T,wt=15): 16638 f(f(x,f(y,z)),f(c_0,f(x,f(z,y)))) = c_0. [para(8655(a,1),8382(a,1,2,2,2)),rewrite(1(8),9631(8,R),8419(8))]. given #920 (T,wt=15): 16672 f(f(x,f(y,z)),f(f(u,f(z,y)),x)) = x. [para(8655(a,1),113(a,1,2,2)),rewrite(13906(8),8655(13))]. given #921 (A,wt=49): 319 f(f(f(x,y),f(f(x,f(y,z)),u)),f(f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v)),f(f(x,y),w))) = f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v)). [para(8(a,1),17(a,1,2,2,1))]. given #922 (F,wt=15): 16879 f(f(x,y),f(z,c_0)) = f(f(z,z),f(y,x)). [para(1(a,1),8859(a,1,1))]. given #923 (F,wt=15): 16932 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0. [para(8871(a,1),112(a,1,2)),rewrite(8446(10,R),8419(8),8446(12,R),8419(10),8446(8,R),6(8),8446(8,R),8419(6)),flip(a)]. given #924 (T,wt=15): 17034 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x. [para(8452(a,1),8872(a,1,2,1)),rewrite(8419(9),8446(9,R),8423(9))]. given #925 (T,wt=15): 17035 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x. [para(8453(a,1),8872(a,1,2,1)),rewrite(8419(9),8446(9,R),8423(9))]. given #926 (A,wt=33): 320 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(y,x),u)),f(v,x))) = f(f(x,f(y,z)),f(f(y,x),u)). [para(17(a,1),11(a,1,1))]. given #927 (F,wt=15): 17038 f(f(x,x),f(y,f(f(z,x),f(u,x)))) = x. [para(13534(a,1),8872(a,1,2,1)),rewrite(8419(9),8446(9,R),8423(9))]. given #928 (F,wt=15): 17039 f(f(x,x),f(y,f(f(x,z),f(u,x)))) = x. [para(13535(a,1),8872(a,1,2,1)),rewrite(8419(9),8446(9,R),8423(9))]. given #929 (T,wt=15): 17040 f(f(x,c_0),f(y,f(f(z,x),f(x,u)))) = x. [para(13562(a,1),8872(a,1,2,1)),rewrite(8419(10),8446(12,R),8425(11))]. given #930 (T,wt=15): 17041 f(f(c_0,x),f(y,f(f(z,x),f(x,u)))) = x. [para(13571(a,1),8872(a,1,2,1)),rewrite(8419(10),8446(12,R),8419(11))]. given #931 (A,wt=33): 321 f(f(x,f(y,z)),f(f(x,u),f(f(x,f(y,z)),f(f(y,x),v)))) = f(f(x,f(y,z)),f(f(y,x),v)). [para(17(a,1),12(a,1,1))]. given #932 (F,wt=15): 17042 f(f(x,c_0),f(y,f(f(x,z),f(x,u)))) = x. [para(13617(a,1),8872(a,1,2,1)),rewrite(8419(10),8446(12,R),8425(11))]. given #933 (F,wt=15): 17043 f(f(c_0,x),f(y,f(f(x,z),f(x,u)))) = x. [para(13629(a,1),8872(a,1,2,1)),rewrite(8419(10),8446(12,R),8419(11))]. given #934 (T,wt=15): 17045 f(f(x,c_0),f(y,f(f(z,x),f(u,x)))) = x. [para(14011(a,1),8872(a,1,2,1)),rewrite(8419(10),8446(12,R),8425(11))]. given #935 (T,wt=15): 17046 f(f(c_0,x),f(y,f(f(z,x),f(u,x)))) = x. [para(14020(a,1),8872(a,1,2,1)),rewrite(8419(10),8446(12,R),8419(11))]. given #936 (A,wt=33): 323 f(f(f(x,y),z),f(f(f(f(x,y),z),f(f(x,z),u)),f(z,v))) = f(f(f(x,y),z),f(f(x,z),u)). [para(12(a,1),17(a,1,2,2,1))]. given #937 (F,wt=15): 17047 f(f(x,c_0),f(y,f(f(x,z),f(u,x)))) = x. [para(14058(a,1),8872(a,1,2,1)),rewrite(8419(10),8446(12,R),8425(11))]. given #938 (F,wt=15): 17048 f(f(c_0,x),f(y,f(f(x,z),f(u,x)))) = x. [para(14067(a,1),8872(a,1,2,1)),rewrite(8419(10),8446(12,R),8419(11))]. given #939 (T,wt=15): 17070 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0. [para(8873(a,1),112(a,1,2)),rewrite(8446(10,R),8419(8),8446(12,R),8419(10),8446(8,R),6(8),8446(8,R),8419(6)),flip(a)]. given #940 (T,wt=15): 17104 f(f(x,x),f(f(f(y,x),f(x,z)),u)) = x. [para(8452(a,1),8874(a,1,2,1)),rewrite(8419(9),8446(9,R),8423(9))]. given #941 (A,wt=41): 324 f(f(f(x,y),f(z,u)),f(y,f(f(f(x,y),f(z,u)),f(f(z,f(x,y)),v)))) = f(f(f(x,y),f(z,u)),f(f(z,f(x,y)),v)). [para(17(a,1),18(a,1,1)),rewrite(1(11))]. given #942 (F,wt=15): 17105 f(f(x,x),f(f(f(x,y),f(x,z)),u)) = x. [para(8453(a,1),8874(a,1,2,1)),rewrite(8419(9),8446(9,R),8423(9))]. given #943 (F,wt=15): 17106 f(f(x,x),f(f(f(y,x),f(z,x)),u)) = x. [para(13534(a,1),8874(a,1,2,1)),rewrite(8419(9),8446(9,R),8423(9))]. given #944 (T,wt=15): 17107 f(f(x,x),f(f(f(x,y),f(z,x)),u)) = x. [para(13535(a,1),8874(a,1,2,1)),rewrite(8419(9),8446(9,R),8423(9))]. given #945 (T,wt=15): 17108 f(f(x,c_0),f(f(f(y,x),f(x,z)),u)) = x. [para(13562(a,1),8874(a,1,2,1)),rewrite(8419(10),8446(12,R),8425(11))]. given #946 (A,wt=41): 326 f(f(f(x,f(y,z)),f(f(y,x),u)),f(f(x,f(y,z)),f(f(f(f(x,f(y,z)),f(f(y,x),u)),f(x,v)),w))) = f(x,f(y,z)). [para(17(a,1),13(a,1,2,1)),rewrite(17(23))]. given #947 (F,wt=15): 17109 f(f(c_0,x),f(f(f(y,x),f(x,z)),u)) = x. [para(13571(a,1),8874(a,1,2,1)),rewrite(8419(10),8446(12,R),8419(11))]. given #948 (F,wt=15): 17110 f(f(x,c_0),f(f(f(x,y),f(x,z)),u)) = x. [para(13617(a,1),8874(a,1,2,1)),rewrite(8419(10),8446(12,R),8425(11))]. given #949 (T,wt=15): 17111 f(f(c_0,x),f(f(f(x,y),f(x,z)),u)) = x. [para(13629(a,1),8874(a,1,2,1)),rewrite(8419(10),8446(12,R),8419(11))]. given #950 (T,wt=15): 17112 f(f(x,c_0),f(f(f(y,x),f(z,x)),u)) = x. [para(14011(a,1),8874(a,1,2,1)),rewrite(8419(10),8446(12,R),8425(11))]. given #951 (A,wt=49): 327 f(f(f(x,y),f(f(y,f(x,z)),u)),f(f(f(f(x,y),f(f(y,f(x,z)),u)),f(y,v)),f(f(x,y),w))) = f(f(f(x,y),f(f(y,f(x,z)),u)),f(y,v)). [para(13(a,1),17(a,1,2,2,1))]. given #952 (F,wt=15): 17113 f(f(c_0,x),f(f(f(y,x),f(z,x)),u)) = x. [para(14020(a,1),8874(a,1,2,1)),rewrite(8419(10),8446(12,R),8419(11))]. given #953 (F,wt=15): 17114 f(f(x,c_0),f(f(f(x,y),f(z,x)),u)) = x. [para(14058(a,1),8874(a,1,2,1)),rewrite(8419(10),8446(12,R),8425(11))]. given #954 (T,wt=15): 17115 f(f(c_0,x),f(f(f(x,y),f(z,x)),u)) = x. [para(14067(a,1),8874(a,1,2,1)),rewrite(8419(10),8446(12,R),8419(11))]. given #955 (T,wt=15): 17176 f(f(x,f(f(c_0,y),z)),f(x,f(y,u))) = x. [para(9534(a,1),6(a,1,2,2))]. given #956 (A,wt=33): 330 f(f(x,f(y,z)),f(f(u,x),f(f(x,f(y,z)),f(f(y,x),v)))) = f(f(x,f(y,z)),f(f(y,x),v)). [para(17(a,1),70(a,1,1))]. given #957 (F,wt=15): 17177 f(f(f(f(c_0,x),y),z),f(z,f(x,u))) = z. [para(9534(a,1),11(a,1,2,2))]. given #958 (F,wt=15): 17178 f(f(f(x,y),z),f(z,f(f(c_0,x),u))) = z. [para(9534(a,1),18(a,1,1,1))]. given #959 (T,wt=15): 17179 f(f(x,f(f(c_0,y),z)),f(f(y,u),x)) = x. [para(9534(a,1),19(a,1,2,1))]. given #960 (T,wt=15): 17180 f(f(x,f(y,z)),f(f(f(c_0,y),u),x)) = x. [para(9534(a,1),31(a,1,1,2))]. given #961 (A,wt=33): 332 f(f(f(x,y),z),f(f(f(f(x,y),z),f(f(y,z),u)),f(z,v))) = f(f(f(x,y),z),f(f(y,z),u)). [para(70(a,1),17(a,1,2,2,1))]. given #962 (F,wt=15): 17181 f(f(f(f(c_0,x),y),z),f(f(x,u),z)) = z. [para(9534(a,1),70(a,1,2,1))]. given #963 (F,wt=15): 17197 f(f(x,f(y,f(c_0,z))),f(x,f(z,u))) = x. [para(9534(a,1),363(a,1,2,2))]. given #964 (T,wt=15): 17201 f(f(f(x,f(c_0,y)),z),f(z,f(y,u))) = z. [para(9534(a,1),433(a,1,2,2))]. given #965 (T,wt=15): 17212 f(f(x,f(y,z)),f(x,f(f(c_0,y),u))) = x. [para(9534(a,1),5635(a,1,1,2))]. given #966 (A,wt=41): 333 f(x,f(f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v)),f(f(x,f(y,z)),w))) = f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v)). [para(17(a,1),15(a,1,2,2,1))]. given #967 (F,wt=15): 17216 f(f(x,f(y,z)),f(x,f(u,f(c_0,y)))) = x. [para(9534(a,1),7352(a,1,1,2))]. given #968 (F,wt=15): 17220 f(f(x,f(y,z)),f(f(u,f(c_0,y)),x)) = x. [para(9534(a,1),7414(a,1,1,2))]. given #969 (T,wt=15): 17227 f(f(x,f(f(y,c_0),z)),f(x,f(y,u))) = x. [para(9536(a,1),6(a,1,2,2))]. given #970 (T,wt=15): 17228 f(f(f(f(x,c_0),y),z),f(z,f(x,u))) = z. [para(9536(a,1),11(a,1,2,2))]. given #971 (A,wt=51): 334 f(f(f(x,f(y,z)),f(f(x,y),u)),f(f(f(f(x,f(y,z)),f(f(x,y),u)),f(x,v)),f(f(x,f(y,z)),w))) = f(f(f(x,f(y,z)),f(f(x,y),u)),f(x,v)). [para(15(a,1),17(a,1,2,2,1))]. given #972 (F,wt=15): 17229 f(f(f(x,y),z),f(z,f(f(x,c_0),u))) = z. [para(9536(a,1),18(a,1,1,1))]. given #973 (F,wt=15): 17230 f(f(x,f(f(y,c_0),z)),f(f(y,u),x)) = x. [para(9536(a,1),19(a,1,2,1))]. given #974 (T,wt=15): 17231 f(f(x,f(y,z)),f(f(f(y,c_0),u),x)) = x. [para(9536(a,1),31(a,1,1,2))]. given #975 (T,wt=15): 17232 f(f(f(f(x,c_0),y),z),f(f(x,u),z)) = z. [para(9536(a,1),70(a,1,2,1))]. given #976 (A,wt=27): 339 f(x,f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(y,x),u)),v))) = f(x,f(y,z)). [para(17(a,1),22(a,1,2,1)),rewrite(17(16))]. given #977 (F,wt=15): 17247 f(f(x,f(y,f(z,c_0))),f(x,f(z,u))) = x. [para(9536(a,1),363(a,1,2,2))]. given #978 (F,wt=15): 17251 f(f(f(x,f(y,c_0)),z),f(z,f(y,u))) = z. [para(9536(a,1),433(a,1,2,2))]. given #979 (T,wt=15): 17257 f(f(x,f(y,z)),f(x,f(f(y,c_0),u))) = x. [para(9536(a,1),5635(a,1,1,2))]. given #980 (T,wt=15): 17260 f(f(x,f(y,z)),f(x,f(u,f(y,c_0)))) = x. [para(9536(a,1),7352(a,1,1,2))]. given #981 (A,wt=37): 340 f(f(f(x,y),f(y,z)),f(f(f(f(x,y),f(y,z)),f(x,u)),f(f(x,y),v))) = f(f(f(x,y),f(y,z)),f(x,u)). [para(22(a,1),17(a,1,2,2,1))]. given #982 (F,wt=15): 17263 f(f(x,f(y,z)),f(f(u,f(y,c_0)),x)) = x. [para(9536(a,1),7414(a,1,1,2))]. given #983 (F,wt=15): 17266 f(f(x,f(f(c_0,y),z)),f(x,f(u,y))) = x. [para(9541(a,1),6(a,1,2,2))]. given #984 (T,wt=15): 17267 f(f(f(f(c_0,x),y),z),f(z,f(u,x))) = z. [para(9541(a,1),11(a,1,2,2))]. given #985 (T,wt=15): 17268 f(f(f(x,y),z),f(z,f(f(c_0,y),u))) = z. [para(9541(a,1),18(a,1,1,1))]. given #986 (A,wt=27): 341 f(f(f(x,f(y,z)),f(f(y,x),u)),f(f(x,f(y,z)),f(x,v))) = f(x,f(y,z)). [para(17(a,1),25(a,1,2,1)),rewrite(17(16))]. given #987 (F,wt=15): 17269 f(f(x,f(f(c_0,y),z)),f(f(u,y),x)) = x. [para(9541(a,1),19(a,1,2,1))]. given #988 (F,wt=15): 17270 f(f(x,f(y,z)),f(f(f(c_0,z),u),x)) = x. [para(9541(a,1),31(a,1,1,2))]. given #989 (T,wt=15): 17271 f(f(f(f(c_0,x),y),z),f(f(u,x),z)) = z. [para(9541(a,1),70(a,1,2,1))]. given #990 (T,wt=15): 17287 f(f(x,f(y,f(c_0,z))),f(x,f(u,z))) = x. [para(9541(a,1),363(a,1,2,2))]. given #991 (A,wt=37): 342 f(f(f(x,y),f(x,z)),f(f(f(f(x,y),f(x,z)),f(y,u)),f(f(x,y),v))) = f(f(f(x,y),f(x,z)),f(y,u)). [para(25(a,1),17(a,1,2,2,1))]. given #992 (F,wt=15): 17291 f(f(f(x,f(c_0,y)),z),f(z,f(u,y))) = z. [para(9541(a,1),433(a,1,2,2))]. given #993 (F,wt=15): 17298 f(f(x,f(y,z)),f(x,f(f(c_0,z),u))) = x. [para(9541(a,1),5635(a,1,1,2))]. given #994 (T,wt=15): 17301 f(f(x,f(y,z)),f(x,f(u,f(c_0,z)))) = x. [para(9541(a,1),7352(a,1,1,2))]. given #995 (T,wt=15): 17304 f(f(x,f(y,z)),f(f(u,f(c_0,z)),x)) = x. [para(9541(a,1),7414(a,1,1,2))]. given #996 (A,wt=51): 343 f(f(f(x,f(y,z)),f(f(y,x),u)),f(f(f(f(x,f(y,z)),f(f(y,x),u)),f(x,v)),f(f(x,f(y,z)),w))) = f(f(f(x,f(y,z)),f(f(y,x),u)),f(x,v)). [para(17(a,1),17(a,1,2,2,1))]. given #997 (F,wt=15): 17323 f(x,f(c_0,f(y,f(y,f(f(c_0,x),z))))) = c_0. [para(9636(a,1),9543(a,1,2,2))]. given #998 (F,wt=15): 17355 f(x,f(c_0,f(y,f(y,f(z,f(c_0,x)))))) = c_0. [para(9636(a,1),9549(a,1,2,2))]. given #999 (T,wt=15): 17445 f(x,f(c_0,f(y,f(y,f(f(x,x),z))))) = c_0. [para(9636(a,1),9558(a,1,2,2))]. given #1000 (T,wt=15): 17468 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0. [para(9636(a,1),9560(a,1,2,2))]. given #1001 (A,wt=27): 348 f(f(f(x,y),z),f(x,f(f(f(x,y),z),f(u,z)))) = f(f(f(x,y),z),f(u,z)). [para(27(a,1),7(a,1,2)),rewrite(1(5),1(8))]. given #1002 (F,wt=15): 17544 f(x,f(c_0,f(y,f(y,f(f(x,c_0),z))))) = c_0. [para(9636(a,1),9620(a,1,2,2))]. given #1003 (F,wt=15): 17570 f(x,f(c_0,f(y,f(y,f(z,f(x,c_0)))))) = c_0. [para(9636(a,1),9623(a,1,2,2))]. given #1004 (T,wt=15): 17808 f(f(x,y),f(c_0,z)) = f(f(z,z),f(y,x)). [para(1(a,1),9991(a,1,1))]. given #1005 (T,wt=15): 17845 f(f(f(x,y),z),f(z,f(u,f(x,c_0)))) = z. [para(10085(a,1),18(a,1,1,1))]. given #1006 (A,wt=23): 350 f(x,f(f(x,y),f(f(x,f(f(f(x,y),f(z,y)),u)),v))) = f(x,y). [para(27(a,1),8(a,1,2,1)),rewrite(27(13))]. given #1007 (F,wt=15): 17846 f(f(x,f(y,f(z,c_0))),f(f(z,u),x)) = x. [para(10085(a,1),19(a,1,2,1))]. given #1008 (F,wt=15): 17847 f(f(f(x,f(y,c_0)),z),f(f(y,u),z)) = z. [para(10085(a,1),70(a,1,2,1))]. given #1009 (T,wt=15): 17895 f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)). [para(10194(a,1),32(a,1,2)),flip(a)]. given #1010 (T,wt=15): 17940 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x). [para(142(a,1),7921(a,1)),rewrite(8446(5,R),1(5))]. given #1011 (A,wt=23): 351 f(x,f(f(x,y),f(z,f(f(x,y),f(f(x,f(y,u)),v))))) = f(x,y). [para(8(a,1),27(a,1,2,1)),rewrite(8(15))]. given #1012 (F,wt=15): 17943 f(f(c_0,f(x,f(x,y))),f(x,f(y,z))) = c_0. [para(10335(a,1),1(a,1)),flip(a)]. given #1013 (F,wt=15): 17948 f(f(c_0,f(x,y)),f(x,f(f(y,x),z))) = c_0. [para(569(a,2),10335(a,1,2,2,2)),rewrite(825(7),1(7))]. given #1014 (T,wt=15): 17951 f(f(x,f(f(y,y),z)),f(c_0,f(x,y))) = c_0. [para(588(a,1),10335(a,1,2,2,2)),rewrite(9(7))]. given #1015 (T,wt=15): 17952 f(f(x,f(y,z)),f(c_0,f(x,f(y,y)))) = c_0. [para(588(a,2),10335(a,1,2,2))]. given #1016 (A,wt=23): 353 f(f(x,y),f(f(f(x,y),f(z,y)),f(u,x))) = f(f(x,y),f(z,y)). [para(27(a,1),11(a,1,1))]. given #1017 (F,wt=15): 17954 f(f(x,f(y,z)),f(c_0,f(f(y,y),x))) = c_0. [para(740(a,2),10335(a,1,2,2))]. given #1018 (F,wt=15): 17956 f(x,f(c_0,f(y,f(f(z,f(y,z)),x)))) = c_0. [para(237(a,1),10335(a,1,1)),rewrite(1(9),569(10,R),8446(7,R),8423(7),1(5))]. given #1019 (T,wt=15): 17958 f(x,f(c_0,f(y,f(f(z,f(z,y)),x)))) = c_0. [para(263(a,1),10335(a,1,1)),rewrite(1(9),569(10,R),8446(7,R),8423(7),1(5))]. given #1020 (T,wt=15): 17961 f(f(x,f(f(y,c_0),z)),f(c_0,f(x,y))) = c_0. [para(8402(a,2),10335(a,1,1,2)),rewrite(825(8))]. given #1021 (A,wt=23): 355 f(f(x,y),f(f(x,z),f(f(x,y),f(u,y)))) = f(f(x,y),f(u,y)). [para(27(a,1),12(a,1,1))]. given #1022 (F,wt=15): 17962 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0. [para(8404(a,1),10335(a,1,1,2)),rewrite(8416(8))]. given #1023 (F,wt=15): 17965 f(f(x,f(y,z)),f(c_0,f(f(y,c_0),x))) = c_0. [para(8418(a,2),10335(a,1,2,2))]. given #1024 (T,wt=15): 17966 f(f(x,f(y,z)),f(c_0,f(x,f(y,c_0)))) = c_0. [para(8422(a,2),10335(a,1,2,2))]. given #1025 (T,wt=15): 17968 f(f(x,f(f(y,c_0),z)),f(c_0,f(y,x))) = c_0. [para(8426(a,1),10335(a,1,2,2,2)),rewrite(14(8))]. given #1026 (A,wt=27): 358 f(f(f(x,y),z),f(y,f(f(f(x,y),z),f(u,z)))) = f(f(f(x,y),z),f(u,z)). [para(27(a,1),18(a,1,1)),rewrite(1(7))]. given #1027 (F,wt=15): 17971 f(f(x,f(f(c_0,y),z)),f(c_0,f(x,y))) = c_0. [para(9629(a,1),10335(a,1,2,2,2)),rewrite(825(8))]. given #1028 (F,wt=15): 17972 f(f(x,f(f(c_0,y),z)),f(c_0,f(y,x))) = c_0. [para(9631(a,1),10335(a,1,2,2,2)),rewrite(14(8))]. given #1029 (T,wt=15): 17974 f(f(x,f(y,z)),f(c_0,f(x,f(c_0,y)))) = c_0. [para(9634(a,2),10335(a,1,2,2))]. given #1030 (T,wt=15): 17976 f(f(x,f(y,z)),f(c_0,f(f(c_0,y),x))) = c_0. [para(9636(a,2),10335(a,1,2,2))]. given #1031 (A,wt=29): 361 f(f(f(x,y),f(z,y)),f(f(x,y),f(f(f(f(x,y),f(z,y)),f(x,u)),v))) = f(x,y). [para(27(a,1),13(a,1,2,1)),rewrite(27(16))]. given #1032 (F,wt=15): 17979 f(f(x,f(y,f(c_0,z))),f(c_0,f(x,z))) = c_0. [para(9644(a,1),10335(a,1,1,2)),rewrite(825(8))]. given #1033 (F,wt=15): 17981 f(f(x,f(y,f(z,c_0))),f(c_0,f(x,z))) = c_0. [para(10599(a,1),10335(a,1,1,2)),rewrite(825(8))]. given #1034 (T,wt=15): 18017 f(f(c_0,f(x,f(y,x))),f(x,f(y,z))) = c_0. [para(10337(a,1),1(a,1)),flip(a)]. given #1035 (T,wt=15): 18046 f(f(c_0,f(x,f(x,y))),f(x,f(z,y))) = c_0. [para(10339(a,1),1(a,1)),flip(a)]. given #1036 (A,wt=23): 362 f(x,f(f(y,x),f(z,f(f(y,x),f(f(x,f(y,u)),v))))) = f(y,x). [para(13(a,1),27(a,1,2,1)),rewrite(13(15))]. given #1037 (F,wt=15): 18053 f(f(x,f(y,f(z,x))),f(c_0,f(x,z))) = c_0. [para(569(a,2),10339(a,1,2,2,2)),rewrite(825(7))]. given #1038 (F,wt=15): 18058 f(f(x,f(y,z)),f(c_0,f(x,f(z,z)))) = c_0. [para(588(a,2),10339(a,1,2,2))]. given #1039 (T,wt=15): 18060 f(f(x,f(y,z)),f(c_0,f(f(z,z),x))) = c_0. [para(740(a,2),10339(a,1,2,2))]. given #1040 (T,wt=15): 18073 f(f(x,f(y,z)),f(c_0,f(f(z,c_0),x))) = c_0. [para(8418(a,2),10339(a,1,2,2))]. given #1041 (A,wt=23): 364 f(f(x,y),f(f(z,x),f(f(x,y),f(u,y)))) = f(f(x,y),f(u,y)). [para(27(a,1),70(a,1,1))]. given #1042 (F,wt=15): 18075 f(f(x,f(y,z)),f(c_0,f(x,f(z,c_0)))) = c_0. [para(8422(a,2),10339(a,1,2,2))]. given #1043 (F,wt=15): 18078 f(f(x,f(y,f(z,c_0))),f(c_0,f(z,x))) = c_0. [para(8426(a,1),10339(a,1,2,2,2)),rewrite(14(8))]. given #1044 (T,wt=15): 18081 f(f(x,f(y,f(c_0,z))),f(c_0,f(z,x))) = c_0. [para(9631(a,1),10339(a,1,2,2,2)),rewrite(14(8))]. given #1045 (T,wt=15): 18087 f(f(x,f(y,z)),f(c_0,f(x,f(c_0,z)))) = c_0. [para(9634(a,2),10339(a,1,2,2))]. given #1046 (A,wt=31): 366 f(x,f(f(x,f(f(f(x,y),f(z,y)),u)),f(f(x,y),v))) = f(x,f(f(f(x,y),f(z,y)),u)). [para(27(a,1),15(a,1,2,2,1))]. given #1047 (F,wt=15): 18090 f(f(x,f(y,z)),f(c_0,f(f(c_0,z),x))) = c_0. [para(9636(a,2),10339(a,1,2,2))]. given #1048 (F,wt=15): 18110 f(f(c_0,f(x,f(x,y))),f(f(y,z),x)) = c_0. [para(10341(a,1),1(a,1)),flip(a)]. given #1049 (T,wt=15): 18111 f(f(f(f(x,x),y),z),f(c_0,f(z,x))) = c_0. [para(588(a,1),10341(a,1,2,2,2)),rewrite(9(7))]. given #1050 (T,wt=15): 18112 f(f(f(x,y),z),f(c_0,f(z,f(x,x)))) = c_0. [para(588(a,2),10341(a,1,2,2))]. given #1051 (A,wt=27): 367 f(x,f(f(x,f(y,z)),f(u,f(f(x,f(y,z)),f(f(x,y),v))))) = f(x,f(y,z)). [para(15(a,1),27(a,1,2,1)),rewrite(15(16))]. given #1052 (F,wt=15): 18113 f(f(f(x,y),z),f(c_0,f(f(x,x),z))) = c_0. [para(740(a,2),10341(a,1,2,2))]. given #1053 (F,wt=15): 18114 f(f(f(f(x,c_0),y),z),f(c_0,f(z,x))) = c_0. [para(8402(a,2),10341(a,1,1,1)),rewrite(825(8))]. given #1054 (T,wt=15): 18115 f(f(f(x,f(y,y)),z),f(c_0,f(z,y))) = c_0. [para(8404(a,1),10341(a,1,1,1)),rewrite(8416(8))]. given #1055 (T,wt=15): 18116 f(f(f(x,y),z),f(c_0,f(f(x,c_0),z))) = c_0. [para(8418(a,2),10341(a,1,2,2))]. given #1056 (A,wt=21): 369 f(x,f(f(x,f(y,f(z,y))),f(z,z))) = f(x,f(y,f(z,y))). [para(200(a,1),27(a,1,2,2))]. given #1057 (F,wt=15): 18117 f(f(f(x,y),z),f(c_0,f(z,f(x,c_0)))) = c_0. [para(8422(a,2),10341(a,1,2,2))]. given #1058 (F,wt=15): 18118 f(f(c_0,f(x,y)),f(f(f(x,c_0),z),y)) = c_0. [para(8426(a,1),10341(a,1,2,2,2)),rewrite(14(8),1(8))]. given #1059 (T,wt=15): 18119 f(f(f(f(c_0,x),y),z),f(c_0,f(z,x))) = c_0. [para(9629(a,1),10341(a,1,2,2,2)),rewrite(825(8))]. given #1060 (T,wt=15): 18120 f(f(c_0,f(x,y)),f(f(f(c_0,x),z),y)) = c_0. [para(9631(a,1),10341(a,1,2,2,2)),rewrite(14(8),1(8))]. given #1061 (A,wt=21): 371 f(x,f(f(x,f(y,f(y,z))),f(z,z))) = f(x,f(y,f(y,z))). [para(205(a,1),27(a,1,2,2))]. given #1062 (F,wt=15): 18121 f(f(f(x,y),z),f(c_0,f(z,f(c_0,x)))) = c_0. [para(9634(a,2),10341(a,1,2,2))]. given #1063 (F,wt=15): 18122 f(f(f(x,y),z),f(c_0,f(f(c_0,x),z))) = c_0. [para(9636(a,2),10341(a,1,2,2))]. given #1064 (T,wt=15): 18123 f(f(f(x,f(c_0,y)),z),f(c_0,f(z,y))) = c_0. [para(9644(a,1),10341(a,1,1,1)),rewrite(825(8))]. given #1065 (T,wt=15): 18124 f(f(f(x,f(y,c_0)),z),f(c_0,f(z,y))) = c_0. [para(10599(a,1),10341(a,1,1,1)),rewrite(825(8))]. given #1066 (A,wt=19): 372 f(x,f(f(x,y),f(f(f(x,y),f(z,y)),u))) = f(x,y). [para(27(a,1),22(a,1,2,1)),rewrite(27(11))]. given #1067 (F,wt=15): 18125 f(f(c_0,f(x,f(x,f(y,z)))),f(y,x)) = c_0. [para(10344(a,1),1(a,1)),flip(a)]. given #1068 (F,wt=15): 18126 f(f(x,y),f(c_0,f(f(c_0,f(x,z)),y))) = c_0. [para(740(a,2),10344(a,1,2,2)),rewrite(8446(5,R))]. given #1069 (T,wt=15): 18127 f(f(c_0,f(x,f(y,x))),f(x,f(z,y))) = c_0. [para(10346(a,1),1(a,1)),flip(a)]. given #1070 (T,wt=15): 18128 f(f(c_0,f(x,f(y,x))),f(f(y,z),x)) = c_0. [para(10348(a,1),1(a,1)),flip(a)]. given #1071 (A,wt=19): 373 f(x,f(f(x,y),f(z,f(f(x,y),f(y,u))))) = f(x,y). [para(22(a,1),27(a,1,2,1)),rewrite(22(11))]. given #1072 (F,wt=15): 18129 f(f(x,y),f(c_0,f(f(c_0,f(y,z)),x))) = c_0. [para(1(a,1),10349(a,1,2,2))]. given #1073 (F,wt=15): 18131 f(f(x,y),f(c_0,f(f(c_0,f(z,y)),x))) = c_0. [para(1(a,1),10351(a,1,2,2))]. given #1074 (T,wt=15): 18132 f(f(c_0,f(x,y)),f(f(z,f(x,c_0)),y)) = c_0. [para(113(a,1),10351(a,1,2)),rewrite(1(8))]. given #1075 (T,wt=15): 18134 f(f(c_0,f(x,f(x,y))),f(f(z,y),x)) = c_0. [para(10352(a,1),1(a,1)),flip(a)]. given #1076 (A,wt=19): 374 f(f(f(x,y),f(z,y)),f(f(x,y),f(x,u))) = f(x,y). [para(27(a,1),25(a,1,2,1)),rewrite(27(11))]. given #1077 (F,wt=15): 18135 f(f(f(x,y),z),f(c_0,f(z,f(y,y)))) = c_0. [para(588(a,2),10352(a,1,2,2))]. given #1078 (F,wt=15): 18136 f(f(f(x,y),z),f(c_0,f(f(y,y),z))) = c_0. [para(740(a,2),10352(a,1,2,2))]. given #1079 (T,wt=15): 18137 f(f(f(x,y),z),f(c_0,f(f(y,c_0),z))) = c_0. [para(8418(a,2),10352(a,1,2,2))]. given #1080 (T,wt=15): 18138 f(f(f(x,y),z),f(c_0,f(z,f(y,c_0)))) = c_0. [para(8422(a,2),10352(a,1,2,2))]. given #1081 (A,wt=19): 375 f(x,f(f(y,x),f(z,f(f(y,x),f(y,u))))) = f(y,x). [para(25(a,1),27(a,1,2,1)),rewrite(25(11))]. given #1082 (F,wt=15): 18139 f(f(c_0,f(x,y)),f(f(z,f(c_0,x)),y)) = c_0. [para(9631(a,1),10352(a,1,2,2,2)),rewrite(14(8),1(8))]. given #1083 (F,wt=15): 18140 f(f(f(x,y),z),f(c_0,f(z,f(c_0,y)))) = c_0. [para(9634(a,2),10352(a,1,2,2))]. given #1084 (T,wt=15): 18141 f(f(f(x,y),z),f(c_0,f(f(c_0,y),z))) = c_0. [para(9636(a,2),10352(a,1,2,2))]. given #1085 (T,wt=15): 18143 f(f(c_0,f(x,f(x,f(y,z)))),f(z,x)) = c_0. [para(10355(a,1),1(a,1)),flip(a)]. given #1086 (A,wt=37): 376 f(f(f(x,y),f(z,y)),f(f(f(f(x,y),f(z,y)),f(x,u)),f(f(x,y),v))) = f(f(f(x,y),f(z,y)),f(x,u)). [para(27(a,1),17(a,1,2,2,1))]. given #1087 (F,wt=15): 18144 f(f(x,y),f(c_0,f(f(c_0,f(z,x)),y))) = c_0. [para(740(a,2),10355(a,1,2,2)),rewrite(8446(5,R))]. given #1088 (F,wt=15): 18145 f(f(c_0,f(x,f(y,x))),f(f(z,y),x)) = c_0. [para(10357(a,1),1(a,1)),flip(a)]. given #1089 (T,wt=15): 18146 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0. [para(9636(a,1),10361(a,1,2,2))]. given #1090 (T,wt=15): 18147 f(f(x,f(y,z)),f(x,f(u,f(u,y)))) = x. [para(10363(a,1),209(a,1,1,2,2)),rewrite(1(5),8419(5),8446(11,R),8419(8))]. given #1091 (A,wt=27): 377 f(x,f(f(x,f(y,z)),f(u,f(f(x,f(y,z)),f(f(y,x),v))))) = f(x,f(y,z)). [para(17(a,1),27(a,1,2,1)),rewrite(17(16))]. given #1092 (F,wt=15): 18148 f(f(f(x,y),z),f(z,f(u,f(u,x)))) = z. [para(10363(a,1),219(a,1,1,1,2)),rewrite(1(5),8419(5),8446(11,R),8419(8))]. given #1093 (F,wt=15): 18149 f(f(f(x,f(x,y)),z),f(z,f(y,u))) = z. [para(10363(a,1),226(a,1,2,2,2)),rewrite(8446(9,R),8419(6),1(8),8419(8))]. given #1094 (T,wt=15): 18150 f(f(x,f(y,z)),f(f(u,f(u,y)),x)) = x. [para(10363(a,1),229(a,1,1,2,2)),rewrite(1(5),8419(5),8446(11,R),8419(8))]. given #1095 (T,wt=15): 18151 f(f(x,f(y,f(y,z))),f(f(z,u),x)) = x. [para(10363(a,1),234(a,1,2,1,2)),rewrite(8446(9,R),8419(6),1(8),8419(8))]. given #1096 (A,wt=19): 378 f(x,f(f(x,y),f(z,f(f(x,y),f(u,y))))) = f(x,y). [para(27(a,1),27(a,1,2,1)),rewrite(27(11))]. given #1097 (F,wt=15): 18152 f(f(f(x,y),z),f(f(u,f(u,x)),z)) = z. [para(10363(a,1),237(a,1,1,1,2)),rewrite(1(5),8419(5),8446(11,R),8419(8))]. given #1098 (F,wt=15): 18153 f(f(x,f(y,f(y,z))),f(x,f(z,u))) = x. [para(10363(a,1),242(a,1,1,2,2)),rewrite(1(6),8419(6),8446(10,R),8419(8))]. given #1099 (T,wt=15): 18154 f(f(f(x,f(x,y)),z),f(f(y,u),z)) = z. [para(10363(a,1),263(a,1,1,1,2)),rewrite(1(6),8419(6),8446(10,R),8419(8))]. given #1100 (T,wt=15): 18155 f(x,f(c_0,f(y,f(y,f(z,f(x,z)))))) = c_0. [para(200(a,1),10370(a,1,2,2)),rewrite(8423(9),1(7))]. given #1101 (A,wt=27): 380 f(f(f(x,y),z),f(x,f(f(z,u),f(f(x,y),z)))) = f(f(z,u),f(f(x,y),z)). [para(30(a,1),7(a,1,2)),rewrite(1(5),1(8))]. given #1102 (F,wt=15): 18156 f(f(x,f(y,z)),f(x,f(u,f(u,z)))) = x. [para(10370(a,1),209(a,1,1,2,2)),rewrite(1(5),8419(5),8446(11,R),8419(8))]. given #1103 (F,wt=15): 18157 f(f(f(x,y),z),f(z,f(u,f(u,y)))) = z. [para(10370(a,1),219(a,1,1,1,2)),rewrite(1(5),8419(5),8446(11,R),8419(8))]. given #1104 (T,wt=15): 18158 f(f(f(x,f(x,y)),z),f(z,f(u,y))) = z. [para(10370(a,1),226(a,1,2,2,2)),rewrite(8446(9,R),8419(6),1(8),8419(8))]. given #1105 (T,wt=15): 18159 f(f(x,f(y,z)),f(f(u,f(u,z)),x)) = x. [para(10370(a,1),229(a,1,1,2,2)),rewrite(1(5),8419(5),8446(11,R),8419(8))]. given #1106 (A,wt=23): 381 f(x,f(f(x,y),f(f(x,f(f(f(y,z),f(x,y)),u)),v))) = f(x,y). [para(30(a,1),8(a,1,2,1)),rewrite(30(13))]. given #1107 (F,wt=15): 18160 f(f(x,f(y,f(y,z))),f(f(u,z),x)) = x. [para(10370(a,1),234(a,1,2,1,2)),rewrite(8446(9,R),8419(6),1(8),8419(8))]. given #1108 (F,wt=15): 18161 f(f(f(x,y),z),f(f(u,f(u,y)),z)) = z. [para(10370(a,1),237(a,1,1,1,2)),rewrite(1(5),8419(5),8446(11,R),8419(8))]. given #1109 (T,wt=15): 18162 f(f(c_0,f(x,f(x,f(y,z)))),f(z,y)) = c_0. [para(11818(a,1),10370(a,1,2,2)),rewrite(8419(10))]. given #1110 (T,wt=15): 18163 f(f(x,f(y,f(y,z))),f(x,f(u,z))) = x. [para(10370(a,1),595(a,1,2,2,2)),rewrite(8446(9,R),8419(6),1(8),8419(8))]. given #1111 (A,wt=23): 382 f(f(x,y),f(f(f(y,z),f(x,y)),f(u,x))) = f(f(y,z),f(x,y)). [para(30(a,1),11(a,1,1))]. given #1112 (F,wt=15): 18164 f(f(f(x,f(x,y)),z),f(f(u,y),z)) = z. [para(10370(a,1),641(a,1,2,1,2)),rewrite(8446(9,R),8419(6),1(8),8419(8))]. given #1113 (F,wt=15): 18165 f(f(c_0,f(x,y)),f(x,f(z,f(y,z)))) = c_0. [para(10412(a,1),1(a,1)),flip(a)]. given #1114 (T,wt=15): 1817