============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 14349 was started by mccune on cleo.thornwood, Mon Jun 19 18:21:52 2006 The command was "/home/mccune/bin/prover9 -f BA2.in BA2-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file BA2.in assign(new_constants,1). assign(age_part,1). assign(false_part,4). assign(true_part,1). assign(max_minutes,10). % assign(max_minutes, 10) -> assign(max_seconds, 600). clauses(sos). f(x,y) = f(y,x) # label(commutativity). f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). 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. % Reading from file BA2-interp.outx terms(interpretations). interpretation(6,[number = 1,seconds = 0],[function(c1,[0]),function(c2,[2]),function(c3,[1]),function(f(_,_),[3,3,1,1,1,1,3,4,5,0,1,2,1,5,5,1,1,1,1,0,1,0,1,1,1,1,1,1,1,1,1,2,1,1,1,2])]). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(x,y) = f(y,x) # label(commutativity). [input]. 2 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [input]. 3 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"). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ a, b, c, f ]). After inverse_order: Function symbol precedence: lex([ a, b, c, f ]). 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; redundancy checks enabled. not interpretable: a % Clause contains symbol not in interpretation: % 0 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),demod(4(25),4(30)),flip(c)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 4 f(x,y) = f(y,x) # label(commutativity). [input]. 5 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [input]. 6 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),demod(4(25),4(30)),flip(c)]. end_of_list. clauses(demodulators). 4 f(x,y) = f(y,x) # label(commutativity). [input]. % (lex-dep) 5 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 4 f(x,y) = f(y,x) # label(commutativity). [input]. given #2 (I,wt=11): 5 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [input]. given #3 (I,wt=43): 6 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),demod(4(25),4(30)),flip(c)]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(a,1,1))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(a,1,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(a,1))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(b,1,2,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(b,1,2)),demod(4(15))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(b,1)),demod(4(16))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(b,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,1,1,2)),demod(4(24))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,1,1)),demod(4(25))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,1,2,2)),demod(4(29))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,1,2)),demod(4(30))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,1))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,2,1,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,2,1)),demod(4(36))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,2,2,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,2,2)),demod(4(41))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),6(c,2)),demod(4(42))]. given #4 (F,wt=11): 7 f(f(x,y),f(y,f(x,z))) = y # label(false). [para(4(a,1),5(a,1,1))]. given #5 (F,wt=11): 8 f(f(x,y),f(x,f(z,y))) = x # label(false). [para(4(a,1),5(a,1,2,2))]. given #6 (T,wt=11): 11 f(x,f(x,f(x,y))) = f(x,y). [para(5(a,1),5(a,1,2)),demod(4(2),4(3))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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_demod(6),demod(31(7)),xx(a)]. given #7 (A,wt=11): 9 f(f(x,y),f(f(y,z),x)) = x # label(false). [para(4(a,1),5(a,1,2))]. given #8 (F,wt=11): 12 f(f(x,f(y,z)),f(y,x)) = x # label(false). [para(7(a,1),4(a,1)),flip(a)]. given #9 (F,wt=11): 13 f(f(x,y),f(y,f(z,x))) = y # label(false). [para(4(a,1),7(a,1,2,2))]. given #10 (F,wt=11): 14 f(f(x,y),f(f(x,z),y)) = y # label(false). [para(4(a,1),7(a,1,2))]. given #11 (F,wt=11): 18 f(f(f(x,y),z),f(z,x)) = z # label(false). [para(5(a,1),7(a,1,2,2))]. given #12 (T,wt=9): 31 f(f(x,x),f(x,y)) = x. [para(11(a,1),5(a,1,2))]. given #13 (A,wt=17): 10 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [para(5(a,1),5(a,1,1))]. given #14 (F,wt=11): 20 f(f(f(x,y),z),f(z,y)) = z # label(false). [para(7(a,1),7(a,1,2,2))]. given #15 (F,wt=11): 21 f(f(x,y),f(f(z,y),x)) = x # label(false). [para(4(a,1),8(a,1,2))]. given #16 (F,wt=11): 37 f(f(x,f(y,z)),f(z,x)) = x # label(false). [para(7(a,1),9(a,1,2,1))]. given #17 (F,wt=11): 44 f(f(x,y),f(f(z,x),y)) = y # label(false). [para(4(a,1),13(a,1,2))]. given #18 (T,wt=9): 42 f(f(x,y),f(x,x)) = x. [para(11(a,1),12(a,1,1))]. given #19 (A,wt=17): 15 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x). [para(7(a,1),5(a,1,1))]. given #20 (F,wt=9): 67 f(f(x,x),f(y,x)) = x. [para(4(a,1),31(a,1,2))]. given #21 (F,wt=9): 127 f(f(x,y),f(y,y)) = y. [para(4(a,1),42(a,1,1))]. given #22 (F,wt=11): 16 f(x,f(x,f(y,x))) = f(y,x). [para(7(a,1),5(a,1,2)),demod(4(2),4(3))]. given #23 (F,wt=11): 71 f(x,f(f(x,x),y)) = f(x,x). [para(31(a,1),8(a,1,2)),demod(4(3))]. given #24 (T,wt=11): 73 f(x,f(y,f(x,x))) = f(x,x). [para(31(a,1),13(a,1,2)),demod(4(3))]. given #25 (A,wt=19): 17 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(5(a,1),7(a,1,1))]. given #26 (F,wt=11): 196 f(x,f(y,f(x,y))) = f(x,x) # label(false). [para(37(a,1),17(a,1,2)),flip(a)]. given #27 (F,wt=11): 206 f(x,f(y,f(y,x))) = f(x,x) # label(false). [para(4(a,1),196(a,1,2,2))]. given #28 (F,wt=15): 210 f(f(x,f(y,f(z,y))),f(x,f(z,z))) = x # label(false). [para(196(a,1),8(a,1,2,2))]. given #29 (F,wt=15): 216 f(f(f(x,f(y,x)),z),f(z,f(y,y))) = z # label(false). [para(196(a,1),13(a,1,2,2))]. given #30 (T,wt=13): 24 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(5(a,1),8(a,1,2)),demod(4(4))]. given #31 (A,wt=19): 19 f(x,f(f(x,f(y,z)),f(f(y,x),u))) = f(x,f(y,z)). [para(7(a,1),7(a,1,1))]. given #32 (F,wt=15): 223 f(f(f(x,x),y),f(y,f(z,f(x,z)))) = y # label(false). [para(196(a,1),20(a,1,1,1))]. given #33 (F,wt=15): 226 f(f(x,f(y,f(z,y))),f(f(z,z),x)) = x # label(false). [para(196(a,1),21(a,1,2,1))]. given #34 (F,wt=15): 229 f(f(x,f(y,y)),f(f(z,f(y,z)),x)) = x # label(false). [para(196(a,1),37(a,1,1,2))]. given #35 (F,wt=15): 232 f(f(f(x,f(y,x)),z),f(f(y,y),z)) = z # label(false). [para(196(a,1),44(a,1,2,1))]. given #36 (T,wt=13): 27 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(7(a,1),8(a,1,2)),demod(4(4))]. given #37 (A,wt=17): 22 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [para(8(a,1),5(a,1,1))]. given #38 (F,wt=15): 243 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x # label(false). [para(206(a,1),8(a,1,2,2))]. given #39 (F,wt=15): 247 f(f(f(x,f(x,y)),z),f(z,f(y,y))) = z # label(false). [para(206(a,1),13(a,1,2,2))]. given #40 (F,wt=15): 252 f(f(f(x,x),y),f(y,f(z,f(z,x)))) = y # label(false). [para(206(a,1),20(a,1,1,1))]. given #41 (F,wt=15): 254 f(f(x,f(y,f(y,z))),f(f(z,z),x)) = x # label(false). [para(206(a,1),21(a,1,2,1))]. given #42 (T,wt=13): 29 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(8(a,1),8(a,1,2)),demod(4(4))]. given #43 (A,wt=17): 23 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(5(a,1),8(a,1,1))]. given #44 (F,wt=15): 256 f(f(x,f(y,y)),f(f(z,f(z,y)),x)) = x # label(false). [para(206(a,1),37(a,1,1,2))]. given #45 (F,wt=15): 258 f(f(f(x,f(x,y)),z),f(f(y,y),z)) = z # label(false). [para(206(a,1),44(a,1,2,1))]. given #46 (F,wt=15): 269 f(f(x,f(y,y)),f(x,f(z,f(y,z)))) = x # label(false). [para(210(a,1),4(a,1)),flip(a)]. given #47 (F,wt=15): 290 f(f(x,y),f(x,f(z,f(f(y,y),z)))) = x # label(false). [para(31(a,1),210(a,1,2,2)),demod(4(6))]. given #48 (T,wt=13): 36 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(9(a,1),7(a,1,2)),demod(4(4))]. given #49 (A,wt=19): 25 f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)). [para(8(a,1),7(a,1,1))]. given #50 (F,wt=15): 330 f(f(f(x,f(f(y,y),x)),z),f(z,y)) = z # label(false). [para(31(a,1),216(a,1,2,2))]. given #51 (F,wt=15): 425 f(f(f(x,x),y),f(f(z,f(x,z)),y)) = y # label(false). [para(4(a,1),223(a,1,2))]. given #52 (F,wt=15): 443 f(f(x,y),f(y,f(z,f(f(x,x),z)))) = y # label(false). [para(31(a,1),223(a,1,1,1))]. given #53 (F,wt=15): 487 f(f(x,f(y,f(f(z,z),y))),f(z,x)) = x # label(false). [para(31(a,1),226(a,1,2,1))]. given #54 (T,wt=13): 48 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(7(a,1),13(a,1,2)),demod(4(4))]. given #55 (A,wt=17): 26 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x). [para(7(a,1),8(a,1,1))]. given #56 (F,wt=15): 519 f(f(x,y),f(f(z,f(f(y,y),z)),x)) = x # label(false). [para(31(a,1),229(a,1,1,2))]. given #57 (F,wt=15): 560 f(f(x,y),f(f(z,f(f(x,x),z)),y)) = y # label(false). [para(31(a,1),232(a,1,2,1)),demod(4(6))]. given #58 (F,wt=15): 700 f(f(x,f(y,y)),f(x,f(z,f(z,y)))) = x # label(false). [para(243(a,1),4(a,1)),flip(a)]. given #59 (F,wt=15): 714 f(f(x,y),f(x,f(z,f(z,f(y,y))))) = x # label(false). [para(31(a,1),243(a,1,2,2)),demod(4(6))]. given #60 (T,wt=13): 50 f(x,f(f(y,x),f(z,y))) = f(y,x). [para(13(a,1),8(a,1,2)),demod(4(4))]. given #61 (A,wt=17): 28 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y). [para(8(a,1),8(a,1,1))]. given #62 (F,wt=15): 762 f(f(f(x,f(x,f(y,y))),z),f(z,y)) = z # label(false). [para(31(a,1),247(a,1,2,2))]. given #63 (F,wt=15): 805 f(f(f(x,x),y),f(f(z,f(z,x)),y)) = y # label(false). [para(4(a,1),252(a,1,2))]. given #64 (F,wt=15): 818 f(f(x,y),f(y,f(z,f(z,f(x,x))))) = y # label(false). [para(31(a,1),252(a,1,1,1))]. given #65 (F,wt=15): 866 f(f(x,f(y,f(y,f(z,z)))),f(z,x)) = x # label(false). [para(31(a,1),254(a,1,2,1))]. given #66 (T,wt=13): 52 f(x,f(f(y,z),f(x,z))) = f(x,z). [para(8(a,1),13(a,1,2)),demod(4(4))]. given #67 (A,wt=34): 33 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_demod(6),demod(31(7)),xx(a)]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(a,1,2,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(a,1,2)),demod(4(6))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(a,1)),demod(4(7))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(a,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,1,1,2)),demod(4(15))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,1,1)),demod(4(16))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,1,2,2)),demod(4(20))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,1,2)),demod(4(21))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,1))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,2,1,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,2,1)),demod(4(27))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,2,2,2))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,2,2)),demod(4(32))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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"). [para(4(a,1),33(b,2)),demod(4(33))]. given #68 (F,wt=15): 1010 f(f(x,y),f(f(z,f(z,f(y,y))),x)) = x # label(false). [para(31(a,1),256(a,1,1,2))]. given #69 (F,wt=15): 1039 f(f(x,y),f(f(z,f(z,f(x,x))),y)) = y # label(false). [para(31(a,1),258(a,1,2,1)),demod(4(6))]. given #70 (F,wt=17): 383 f(x,f(f(x,y),f(f(x,y),f(y,z)))) = f(x,x) # label(false). [para(24(a,1),196(a,1,2,2)),demod(4(5))]. given #71 (F,wt=17): 620 f(x,f(f(y,x),f(f(y,x),f(y,z)))) = f(x,x) # label(false). [para(27(a,1),196(a,1,2,2)),demod(4(5))]. given #72 (T,wt=13): 56 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(13(a,1),13(a,1,2)),demod(4(4))]. given #73 (A,wt=17): 34 f(x,f(f(x,y),f(f(f(y,z),x),u))) = f(x,y). [para(9(a,1),5(a,1,1))]. given #74 (F,wt=17): 906 f(x,f(f(x,y),f(f(x,y),f(z,y)))) = f(x,x) # label(false). [para(29(a,1),196(a,1,2,2)),demod(4(5))]. given #75 (F,wt=17): 1114 f(x,f(f(x,y),f(z,f(f(y,y),z)))) = f(x,y) # label(false). [para(290(a,1),8(a,1,2)),demod(4(6))]. given #76 (F,wt=17): 1121 f(x,f(f(y,f(f(z,z),y)),f(x,z))) = f(x,z) # label(false). [para(290(a,1),13(a,1,2)),demod(4(6))]. given #77 (F,wt=17): 1210 f(x,f(f(x,y),f(f(y,z),f(x,y)))) = f(x,x) # label(false). [para(36(a,1),196(a,1,2,2)),demod(4(5))]. given #78 (T,wt=15): 38 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(7(a,1),9(a,1,2)),demod(4(3),4(4))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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_demod(33),demod(3043(27),4(26),3043(32),4(31))]. given #79 (A,wt=19): 35 f(x,f(f(f(y,z),x),f(f(x,y),u))) = f(f(y,z),x). [para(9(a,1),7(a,1,1))]. given #80 (F,wt=11): 3043 f(x,f(y,y)) = f(x,f(y,x)) # label(false). [para(196(a,1),38(a,1,2))]. given #81 (F,wt=11): 3258 f(f(x,x),y) = f(y,f(x,y)) # label(false). [para(3043(a,1),4(a,1)),flip(a)]. given #82 (F,wt=11): 3259 f(x,f(y,y)) = f(x,f(x,y)) # label(false). [para(4(a,1),3043(a,2,2))]. given #83 (F,wt=11): 3286 f(x,f(f(y,y),x)) = f(x,y) # label(false). [para(31(a,1),3043(a,1,2)),flip(a)]. given #84 (T,wt=15): 53 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(13(a,1),9(a,1,2)),demod(4(3),4(4))]. given #85 (A,wt=17): 39 f(x,f(f(x,y),f(z,f(f(y,u),x)))) = f(x,y). [para(9(a,1),8(a,1,1))]. given #86 (F,wt=11): 3557 f(f(x,x),y) = f(y,f(y,x)) # label(false). [para(4(a,1),3258(a,2,2))]. given #87 (F,wt=11): 3707 f(x,f(x,f(y,y))) = f(x,y) # label(false). [para(3259(a,2),11(a,1,2))]. given #88 (F,wt=15): 3108 f(x,f(f(y,y),f(f(z,y),x))) = f(x,x) # label(false). [back_demod(2462),demod(3043(6,R),4(4))]. not interpretable: a % Clause contains symbol not in interpretation: % 0 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(3112),unit_del(a,4368)]. given #89 (F,wt=15): 3109 f(x,f(f(y,y),f(f(y,z),x))) = f(x,x) # label(false). [back_demod(2460),demod(3043(6,R),4(4))]. given #90 (T,wt=11): 4368 f(x,f(y,f(y,y))) = f(x,x). [para(3108(a,1),383(a,1,2,2)),demod(3928(8),3043(6),4(3),73(3))]. NOTE: New constant: 0 f(x,f(x,x)) = c_0. [new_symbol(4595)]. NOTE: New Function symbol precedence: lex([ a, b, c, c_0, f ]). NOTE: sn=112, num_tables=202 NOTE: updating interpretation 1: c_0=1. not interpretable: a % Clause contains symbol not in interpretation: % 0 f(f(a,f(a,b)),f(a,f(a,c))) != f(c_0,f(a,f(b,c))) # answer("Sheffer"). [back_demod(4438),demod(4730(11,R)),flip(a)]. given #91 (A,wt=19): 41 f(x,f(f(x,f(y,z)),f(u,f(y,x)))) = f(x,f(y,z)). [para(12(a,1),8(a,1,1))]. given #92 (F,wt=11): 4657 f(x,f(x,f(y,c_0))) = f(x,y) # label(false). [back_demod(4644),demod(4650(2))]. given #93 (F,wt=11): 4659 f(f(x,c_0),y) = f(y,f(y,x)) # label(false). [back_demod(4642),demod(4650(2))]. given #94 (F,wt=11): 4663 f(x,f(f(y,c_0),x)) = f(x,y) # label(false). [back_demod(4638),demod(4650(2))]. given #95 (F,wt=11): 4665 f(x,f(y,c_0)) = f(x,f(x,y)) # label(false). [back_demod(4636),demod(4650(2))]. given #96 (T,wt=7): 4650 f(x,f(x,x)) = c_0. [new_symbol(4595)]. given #97 (A,wt=19): 43 f(x,f(f(f(y,x),z),f(x,f(y,u)))) = f(x,f(y,u)). [para(12(a,1),9(a,1,1))]. given #98 (F,wt=11): 4667 f(f(x,c_0),y) = f(y,f(x,y)) # label(false). [back_demod(4634),demod(4650(2))]. given #99 (F,wt=11): 4669 f(x,f(y,c_0)) = f(x,f(y,x)) # label(false). [back_demod(4632),demod(4650(2))]. given #100 (F,wt=11): 5595 f(x,f(x,f(c_0,y))) = f(x,y) # label(false). [para(4(a,1),4657(a,1,2,2))]. given #101 (F,wt=11): 5665 f(f(c_0,x),y) = f(y,f(y,x)) # label(false). [para(4(a,1),4659(a,1,1))]. given #102 (T,wt=7): 4658 f(f(c_0,c_0),x) = c_0. [back_demod(4643),demod(4650(2),4650(3),4650(6))]. given #103 (A,wt=17): 45 f(x,f(f(y,x),f(f(x,f(z,y)),u))) = f(y,x). [para(13(a,1),5(a,1,1))]. given #104 (F,wt=11): 5934 f(x,f(c_0,y)) = f(x,f(x,y)) # label(false). [para(4663(a,1),17(a,1,2)),demod(4(4),5595(4)),flip(a)]. given #105 (F,wt=11): 6525 f(f(c_0,x),y) = f(y,f(x,y)) # label(false). [para(4(a,1),4667(a,1,1))]. given #106 (F,wt=11): 6682 f(x,f(c_0,y)) = f(x,f(y,x)) # label(false). [para(4(a,1),4669(a,1,2))]. given #107 (F,wt=15): 3266 f(f(x,f(y,z)),f(x,f(z,f(y,y)))) = x # label(false). [para(3043(a,2),8(a,1,2,2))]. given #108 (T,wt=7): 4660 f(c_0,f(c_0,x)) = x. [back_demod(4641),demod(4650(2),4650(3))]. given #109 (A,wt=19): 46 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)). [para(5(a,1),13(a,1,1))]. given #110 (F,wt=15): 3276 f(f(f(x,y),z),f(z,f(y,f(x,x)))) = z # label(false). [para(3043(a,2),13(a,1,2,2))]. given #111 (F,wt=15): 3291 f(f(f(x,f(y,y)),z),f(z,f(y,x))) = z # label(false). [para(3043(a,2),20(a,1,1,1))]. given #112 (F,wt=15): 3297 f(f(x,f(y,z)),f(f(z,f(y,y)),x)) = x # label(false). [para(3043(a,2),21(a,1,2,1))]. given #113 (F,wt=15): 3301 f(f(x,f(y,f(z,z))),f(f(z,y),x)) = x # label(false). [para(3043(a,2),37(a,1,1,2))]. given #114 (T,wt=7): 4664 f(x,f(c_0,c_0)) = c_0. [back_demod(4637),demod(4650(2),4650(3),4650(6))]. given #115 (A,wt=19): 47 f(x,f(f(x,f(y,z)),f(f(z,x),u))) = f(x,f(y,z)). [para(13(a,1),7(a,1,1))]. given #116 (F,wt=15): 3306 f(f(f(x,y),z),f(f(y,f(x,x)),z)) = z # label(false). [para(3043(a,2),44(a,1,2,1))]. given #117 (F,wt=15): 3314 f(x,f(y,f(z,z))) = f(x,f(y,f(z,y))) # label(false). [para(3043(a,1),17(a,1,2,1,2)),demod(17(7)),flip(a)]. given #118 (F,wt=15): 3319 f(f(x,f(y,f(z,y))),f(x,f(z,x))) = x # label(false). [para(3043(a,1),210(a,1,2))]. given #119 (F,wt=15): 3323 f(f(f(x,f(y,x)),z),f(z,f(y,z))) = z # label(false). [para(3043(a,1),216(a,1,2))]. given #120 (T,wt=7): 4666 f(c_0,f(x,x)) = x. [back_demod(4635),demod(4650(2))]. given #121 (A,wt=17): 49 f(x,f(f(y,x),f(z,f(x,f(u,y))))) = f(y,x). [para(13(a,1),8(a,1,1))]. given #122 (F,wt=15): 3338 f(f(x,f(y,x)),f(f(z,f(y,z)),x)) = x # label(false). [para(3043(a,1),229(a,1,1))]. given #123 (F,wt=15): 3355 f(f(x,f(y,f(y,z))),f(x,f(z,x))) = x # label(false). [para(3043(a,1),243(a,1,2))]. given #124 (F,wt=15): 3358 f(f(f(x,f(x,y)),z),f(z,f(y,z))) = z # label(false). [para(3043(a,1),247(a,1,2))]. given #125 (F,wt=15): 3372 f(f(x,f(y,x)),f(f(z,f(z,y)),x)) = x # label(false). [para(3043(a,1),256(a,1,1))]. given #126 (T,wt=7): 4668 f(c_0,f(x,c_0)) = x. [back_demod(4633),demod(4650(2),4650(3))]. given #127 (A,wt=19): 51 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)). [para(8(a,1),13(a,1,1))]. given #128 (F,wt=15): 3380 f(f(x,f(y,x)),f(x,f(z,f(y,z)))) = x # label(false). [para(3043(a,1),269(a,1,1))]. given #129 (F,wt=15): 3405 f(f(x,f(y,x)),f(x,f(z,f(z,y)))) = x # label(false). [para(3043(a,1),700(a,1,1))]. given #130 (F,wt=15): 3470 f(f(x,f(y,y)),z) = f(f(x,f(y,x)),z) # label(false). [para(3043(a,1),35(a,1,2,1,1)),demod(35(7)),flip(a)]. given #131 (F,wt=15): 3477 f(x,f(f(y,y),f(x,f(z,y)))) = f(x,x) # label(false). [back_demod(3103),demod(3286(4))]. given #132 (T,wt=7): 4730 f(c_0,x) = f(x,x). [back_demod(4539),demod(4650(2))]. given #133 (A,wt=19): 54 f(x,f(f(f(y,z),x),f(u,f(x,y)))) = f(f(y,z),x). [para(9(a,1),13(a,1,1))]. given #134 (F,wt=15): 3561 f(f(x,f(y,z)),f(x,f(f(y,y),z))) = x # label(false). [para(3258(a,2),8(a,1,2,2))]. given #135 (F,wt=15): 3570 f(f(f(x,y),z),f(z,f(f(x,x),y))) = z # label(false). [para(3258(a,2),13(a,1,2,2))]. given #136 (F,wt=15): 3576 f(f(x,f(f(y,x),z)),f(f(y,y),x)) = x # label(false). [para(3258(a,2),18(a,1,2)),demod(4(3))]. given #137 (F,wt=15): 3579 f(f(f(f(x,x),y),z),f(z,f(x,y))) = z # label(false). [para(3258(a,2),20(a,1,1,1))]. given #138 (T,wt=7): 4746 f(x,c_0) = f(x,x). [back_demod(4371),demod(4650(4),4650(5),4(6),4658(6))]. given #139 (A,wt=19): 55 f(x,f(f(x,f(y,z)),f(u,f(z,x)))) = f(x,f(y,z)). [para(13(a,1),13(a,1,1))]. given #140 (F,wt=15): 3581 f(f(x,f(y,f(z,x))),f(f(z,z),x)) = x # label(false). [para(3258(a,2),20(a,1,2)),demod(4(3))]. given #141 (F,wt=15): 3582 f(f(x,f(y,z)),f(f(f(y,y),z),x)) = x # label(false). [para(3258(a,2),21(a,1,2,1))]. given #142 (F,wt=15): 3587 f(f(x,f(f(y,y),z)),f(f(y,z),x)) = x # label(false). [para(3258(a,2),37(a,1,1,2))]. given #143 (F,wt=15): 3590 f(f(f(x,y),z),f(f(f(x,x),y),z)) = z # label(false). [para(3258(a,2),44(a,1,2,1))]. given #144 (T,wt=7): 5612 f(x,f(c_0,x)) = c_0. [para(4657(a,1),210(a,1,1)),demod(4666(5),4(3))]. given #145 (A,wt=17): 57 f(x,f(f(y,x),f(f(f(y,z),x),u))) = f(y,x). [para(14(a,1),5(a,1,1))]. given #146 (F,wt=15): 3594 f(x,f(f(y,y),z)) = f(x,f(z,f(y,z))) # label(false). [para(3258(a,1),17(a,1,2,1,2)),demod(270(8)),flip(a)]. given #147 (F,wt=15): 3698 f(f(f(x,x),y),z) = f(f(y,f(x,y)),z) # label(false). [para(3258(a,1),35(a,1,2,1,1)),demod(315(8)),flip(a)]. given #148 (F,wt=15): 3706 f(f(x,f(y,z)),f(x,f(y,f(z,z)))) = x # label(false). [para(3259(a,2),8(a,1,2,2))]. given #149 (F,wt=15): 3714 f(f(f(x,y),z),f(z,f(x,f(y,y)))) = z # label(false). [para(3259(a,2),13(a,1,2,2))]. given #150 (T,wt=7): 5640 f(x,f(x,c_0)) = c_0. [para(4657(a,1),38(a,1,2)),demod(4650(2)),flip(a)]. given #151 (A,wt=19): 58 f(x,f(f(f(x,y),z),f(x,f(y,u)))) = f(x,f(y,u)). [para(5(a,1),14(a,1,1))]. given #152 (F,wt=15): 3723 f(f(f(x,f(y,y)),z),f(z,f(x,y))) = z # label(false). [para(3259(a,2),20(a,1,1,1))]. given #153 (F,wt=15): 3728 f(f(x,f(y,z)),f(f(y,f(z,z)),x)) = x # label(false). [para(3259(a,2),21(a,1,2,1))]. given #154 (F,wt=15): 3730 f(f(x,f(y,f(z,z))),f(f(y,z),x)) = x # label(false). [para(3259(a,2),37(a,1,1,2))]. given #155 (F,wt=15): 3734 f(f(f(x,y),z),f(f(x,f(y,y)),z)) = z # label(false). [para(3259(a,2),44(a,1,2,1))]. given #156 (T,wt=9): 4717 f(f(x,y),f(y,c_0)) = y. [back_demod(4573),demod(4650(3))]. given #157 (A,wt=19): 59 f(x,f(f(f(y,z),x),f(f(y,x),u))) = f(f(y,z),x). [para(14(a,1),7(a,1,1))]. given #158 (F,wt=15): 3737 f(x,f(y,f(z,z))) = f(x,f(y,f(y,z))) # label(false). [para(3259(a,1),17(a,1,2,1,2)),demod(17(7)),flip(a)]. given #159 (F,wt=15): 3740 f(f(x,f(y,f(z,y))),f(x,f(x,z))) = x # label(false). [para(3259(a,1),210(a,1,2))]. given #160 (F,wt=15): 3743 f(f(f(x,f(y,x)),z),f(z,f(z,y))) = z # label(false). [para(3259(a,1),216(a,1,2))]. given #161 (F,wt=15): 3754 f(f(x,f(x,y)),f(f(z,f(y,z)),x)) = x # label(false). [para(3259(a,1),229(a,1,1))]. given #162 (T,wt=9): 4718 f(f(x,c_0),f(y,x)) = x. [back_demod(4571),demod(4650(2))]. given #163 (A,wt=17): 60 f(x,f(f(y,x),f(z,f(f(y,u),x)))) = f(y,x). [para(14(a,1),8(a,1,1))]. given #164 (F,wt=15): 3768 f(f(x,f(y,f(y,z))),f(x,f(x,z))) = x # label(false). [para(3259(a,1),243(a,1,2))]. given #165 (F,wt=15): 3770 f(f(f(x,f(x,y)),z),f(z,f(z,y))) = z # label(false). [para(3259(a,1),247(a,1,2))]. given #166 (F,wt=15): 3780 f(f(x,f(x,y)),f(f(z,f(z,y)),x)) = x # label(false). [para(3259(a,1),256(a,1,1))]. given #167 (F,wt=15): 3786 f(f(x,f(x,y)),f(x,f(z,f(y,z)))) = x # label(false). [para(3259(a,1),269(a,1,1))]. given #168 (T,wt=9): 4720 f(f(x,y),f(x,c_0)) = x. [back_demod(4568),demod(4650(3))]. given #169 (A,wt=19): 61 f(x,f(f(f(x,y),z),f(x,f(u,y)))) = f(x,f(u,y)). [para(8(a,1),14(a,1,1))]. given #170 (F,wt=15): 3801 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x # label(false). [para(3259(a,1),700(a,1,1))]. given #171 (F,wt=15): 3844 f(f(x,f(y,y)),z) = f(f(x,f(x,y)),z) # label(false). [para(3259(a,1),35(a,1,2,1,1)),demod(35(7)),flip(a)]. given #172 (F,wt=15): 3872 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x) # label(false). [back_demod(2715),demod(3707(9),4(4))]. given #173 (F,wt=15): 3873 f(x,f(y,f(x,f(z,f(y,z))))) = f(x,x) # label(false). [back_demod(2713),demod(3707(9),4(4))]. given #174 (T,wt=9): 4726 f(f(x,c_0),f(x,y)) = x. [back_demod(4554),demod(4650(2))]. given #175 (A,wt=15): 62 f(x,f(y,f(f(y,z),x))) = f(f(y,z),x). [para(14(a,1),9(a,1,2)),demod(4(3),4(4))]. given #176 (F,wt=15): 3875 f(f(x,f(f(y,y),z)),f(x,f(z,y))) = x # label(false). [para(3286(a,1),8(a,1,2,2))]. given #177 (F,wt=15): 3878 f(f(f(f(x,x),y),z),f(z,f(y,x))) = z # label(false). [para(3286(a,1),13(a,1,2,2))]. given #178 (F,wt=15): 3882 f(f(f(x,y),z),f(z,f(f(y,y),x))) = z # label(false). [para(3286(a,1),20(a,1,1,1))]. given #179 (F,wt=15): 3884 f(f(x,f(f(y,y),z)),f(f(z,y),x)) = x # label(false). [para(3286(a,1),21(a,1,2,1))]. given #180 (T,wt=9): 5599 f(f(c_0,x),f(x,y)) = x. [para(9(a,1),4657(a,1,2)),demod(4(4),4660(4)),flip(a)]. given #181 (A,wt=19): 63 f(x,f(f(f(x,y),z),f(f(y,u),x))) = f(f(y,u),x). [para(9(a,1),14(a,1,1))]. given #182 (F,wt=15): 3886 f(f(x,f(y,z)),f(f(f(z,z),y),x)) = x # label(false). [para(3286(a,1),37(a,1,1,2))]. given #183 (F,wt=15): 3888 f(f(f(f(x,x),y),z),f(f(y,x),z)) = z # label(false). [para(3286(a,1),44(a,1,2,1))]. given #184 (F,wt=15): 4151 f(f(x,f(y,z)),f(x,f(f(z,z),y))) = x # label(false). [para(3557(a,2),8(a,1,2,2))]. given #185 (F,wt=15): 4163 f(f(f(x,y),z),f(f(f(y,y),x),z)) = z # label(false). [para(3557(a,2),44(a,1,2,1))]. given #186 (T,wt=9): 5606 f(f(c_0,x),f(y,x)) = x. [para(21(a,1),4657(a,1,2)),demod(4(4),4660(4)),flip(a)]. given #187 (A,wt=19): 64 f(x,f(f(f(y,z),x),f(u,f(y,x)))) = f(f(y,z),x). [para(14(a,1),13(a,1,1))]. given #188 (F,wt=15): 4166 f(x,f(f(y,y),z)) = f(x,f(z,f(z,y))) # label(false). [para(3557(a,1),17(a,1,2,1,2)),demod(674(8)),flip(a)]. given #189 (F,wt=15): 4227 f(f(f(x,x),y),z) = f(f(y,f(y,x)),z) # label(false). [para(3557(a,1),35(a,1,2,1,1)),demod(750(8)),flip(a)]. given #190 (F,wt=15): 4271 f(x,f(y,f(f(z,f(y,y)),x))) = f(x,x) # label(false). [para(31(a,1),3108(a,1,2,1))]. given #191 (F,wt=15): 4389 f(x,f(y,f(f(z,f(y,z)),x))) = f(x,x) # label(false). [para(3043(a,1),3108(a,1,2,2,1)),demod(31(3))]. given #192 (T,wt=9): 5952 f(f(x,y),f(c_0,x)) = x. [para(4663(a,1),256(a,1,2,1)),demod(4730(5,R),4668(4),4(4),5640(4))]. given #193 (A,wt=19): 65 f(x,f(f(f(y,x),z),f(x,f(u,y)))) = f(x,f(u,y)). [para(13(a,1),14(a,1,1))]. given #194 (F,wt=15): 4397 f(x,f(y,f(f(z,f(z,y)),x))) = f(x,x) # label(false). [para(3259(a,1),3108(a,1,2,2,1)),demod(31(3))]. given #195 (F,wt=15): 4439 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x) # label(false). [para(4(a,1),3109(a,1,2,2))]. given #196 (F,wt=15): 4448 f(x,f(y,f(f(f(y,y),z),x))) = f(x,x) # label(false). [para(31(a,1),3109(a,1,2,1))]. given #197 (F,wt=15): 4654 f(x,f(f(y,c_0),f(f(y,z),x))) = f(x,x) # label(false). [back_demod(4647),demod(4650(2))]. given #198 (T,wt=9): 5971 f(f(x,y),f(c_0,y)) = y. [para(4663(a,1),805(a,1,2,1)),demod(4730(5,R),4668(4),4(4),5640(4))]. given #199 (A,wt=19): 66 f(x,f(f(f(y,x),z),f(f(y,u),x))) = f(f(y,u),x). [para(14(a,1),14(a,1,1))]. given #200 (F,wt=15): 4655 f(x,f(f(y,c_0),f(f(z,y),x))) = f(x,x) # label(false). [back_demod(4646),demod(4650(2))]. given #201 (F,wt=15): 4673 f(f(f(x,c_0),y),f(f(z,f(z,x)),y)) = y # label(false). [back_demod(4625),demod(4650(2))]. low water: id=8905, wt=45 low water: id=9039, wt=43 given #202 (F,wt=15): 4676 f(f(x,f(y,c_0)),f(x,f(z,f(z,y)))) = x # label(false). [back_demod(4621),demod(4650(2))]. low water: id=9363, wt=41 given #203 (F,wt=15): 4678 f(f(f(x,c_0),y),f(f(z,f(x,z)),y)) = y # label(false). [back_demod(4619),demod(4650(2))]. given #204 (T,wt=11): 4671 f(f(x,c_0),y) = f(f(x,x),y). [back_demod(4630),demod(4650(2))]. low water: id=9691, wt=39 low water: id=9197, wt=37 low water: id=10021, wt=35 given #205 (A,wt=15): 69 f(x,f(f(x,y),f(f(x,x),z))) = f(x,y). [para(31(a,1),7(a,1,1))]. given #206 (F,wt=15): 4681 f(f(x,f(y,c_0)),f(x,f(z,f(y,z)))) = x # label(false). [back_demod(4616),demod(4650(2))]. given #207 (F,wt=15): 4682 f(f(f(x,f(x,y)),z),f(f(y,c_0),z)) = z # label(false). [back_demod(4615),demod(4650(5))]. given #208 (F,wt=15): 4684 f(f(x,f(y,c_0)),f(f(z,f(z,y)),x)) = x # label(false). [back_demod(4613),demod(4650(2))]. given #209 (F,wt=15): 4688 f(f(x,f(y,f(y,z))),f(f(z,c_0),x)) = x # label(false). [back_demod(4608),demod(4650(5))]. given #210 (T,wt=11): 4683 f(x,f(c_0,f(y,f(y,x)))) = c_0. [back_demod(4614),demod(4650(4),4(4),4650(7))]. given #211 (A,wt=15): 72 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(31(a,1),13(a,1,1))]. given #212 (F,wt=15): 4691 f(f(f(x,c_0),y),f(y,f(z,f(z,x)))) = y # label(false). [back_demod(4605),demod(4650(2))]. given #213 (F,wt=15): 4692 f(f(f(x,f(x,y)),z),f(z,f(y,c_0))) = z # label(false). [back_demod(4603),demod(4650(5))]. given #214 (F,wt=15): 4693 f(f(x,f(y,f(y,z))),f(x,f(z,c_0))) = x # label(false). [back_demod(4601),demod(4650(5))]. given #215 (F,wt=15): 4696 f(f(f(x,f(y,x)),z),f(f(y,c_0),z)) = z # label(false). [back_demod(4598),demod(4650(5))]. given #216 (T,wt=11): 4687 f(x,f(c_0,f(x,y))) = f(x,y). [back_demod(4609),demod(4650(3),4(3))]. given #217 (A,wt=15): 74 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z). [para(31(a,1),14(a,1,1))]. given #218 (F,wt=15): 4700 f(f(x,f(y,c_0)),f(f(z,f(y,z)),x)) = x # label(false). [back_demod(4593),demod(4650(2))]. given #219 (F,wt=15): 4702 f(f(x,f(y,f(z,y))),f(f(z,c_0),x)) = x # label(false). [back_demod(4590),demod(4650(5))]. given #220 (F,wt=15): 4707 f(f(f(x,c_0),y),f(y,f(z,f(x,z)))) = y # label(false). [back_demod(4585),demod(4650(2))]. given #221 (F,wt=15): 4709 f(f(f(x,f(y,x)),z),f(z,f(y,c_0))) = z # label(false). [back_demod(4582),demod(4650(5))]. given #222 (T,wt=11): 4695 f(x,f(c_0,f(y,x))) = f(y,x). [back_demod(4599),demod(4650(3),4(3))]. given #223 (A,wt=21): 75 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v))) = x. [para(10(a,1),5(a,1,1))]. given #224 (F,wt=15): 4711 f(f(x,f(y,f(z,y))),f(x,f(z,c_0))) = x # label(false). [back_demod(4579),demod(4650(5))]. given #225 (F,wt=15): 4938 f(x,f(f(y,x),f(c_0,f(z,y)))) = f(x,x) # label(false). [back_demod(2525),demod(4669(5,R),4(4))]. given #226 (F,wt=15): 4945 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x) # label(false). [back_demod(2241),demod(4669(5,R),4(4))]. given #227 (F,wt=15): 4952 f(x,f(f(y,x),f(c_0,f(y,z)))) = f(x,x) # label(false). [back_demod(1539),demod(4669(5,R),4(4))]. given #228 (T,wt=11): 4698 f(x,f(c_0,f(y,f(x,y)))) = c_0. [back_demod(4596),demod(4650(4),4(4),4650(7))]. given #229 (A,wt=31): 76 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(10(a,1),7(a,1,1))]. given #230 (F,wt=13): 14591 f(f(c_0,x),f(y,f(y,f(x,z)))) = x # label(false). [para(5665(a,1),76(a,2,2)),demod(7681(9),7(6)),flip(a)]. given #231 (F,wt=13): 14594 f(f(x,f(x,f(y,z))),f(c_0,y)) = y # label(false). [para(14591(a,1),4(a,1)),flip(a)]. given #232 (F,wt=13): 14595 f(f(x,c_0),f(y,f(y,f(x,z)))) = x # label(false). [para(4(a,1),14591(a,1,1))]. given #233 (F,wt=13): 14596 f(f(c_0,x),f(y,f(y,f(z,x)))) = x # label(false). [para(4(a,1),14591(a,1,2,2,2))]. given #234 (T,wt=11): 4714 f(x,f(y,c_0)) = f(x,f(y,y)). [back_demod(4576),demod(4650(2))]. given #235 (A,wt=21): 77 f(f(x,y),f(y,f(f(f(x,y),f(f(y,f(x,z)),u)),v))) = y. [para(7(a,1),10(a,1,2,1)),demod(7(13))]. given #236 (F,wt=13): 14607 f(f(x,f(x,f(y,z))),f(y,y)) = y # label(false). [para(14591(a,1),16(a,1,2,2)),demod(4(7),3043(8,R),14591(11))]. given #237 (F,wt=13): 14623 f(f(x,x),f(y,f(y,f(x,z)))) = x # label(false). [para(4730(a,1),14591(a,1,1))]. given #238 (F,wt=13): 14642 f(f(x,f(x,f(y,z))),f(c_0,z)) = z # label(false). [para(4(a,1),14594(a,1,1,2,2))]. given #239 (F,wt=13): 14643 f(f(x,f(x,f(y,z))),f(y,c_0)) = y # label(false). [para(4(a,1),14594(a,1,2))]. given #240 (T,wt=11): 4715 f(x,f(y,f(x,c_0))) = f(x,x). [back_demod(4575),demod(4650(2))]. given #241 (A,wt=21): 78 f(f(x,y),f(x,f(z,f(f(x,y),f(f(x,f(y,u)),v))))) = x. [para(10(a,1),8(a,1,1))]. given #242 (F,wt=13): 14664 f(f(x,c_0),f(y,f(y,f(z,x)))) = x # label(false). [para(4(a,1),14595(a,1,2,2,2))]. given #243 (F,wt=13): 14684 f(f(x,f(x,f(y,z))),f(z,z)) = z # label(false). [para(14596(a,1),16(a,1,2,2)),demod(4(7),3043(8,R),14596(11))]. given #244 (F,wt=13): 14703 f(f(x,x),f(y,f(y,f(z,x)))) = x # label(false). [para(4730(a,1),14596(a,1,1))]. given #245 (F,wt=13): 14752 f(f(x,f(x,f(y,z))),f(z,c_0)) = z # label(false). [para(4(a,1),14642(a,1,2))]. given #246 (T,wt=11): 4716 f(x,f(f(x,c_0),y)) = f(x,x). [back_demod(4574),demod(4650(2))]. given #247 (A,wt=15): 79 f(f(x,y),f(x,f(f(x,f(y,z)),u))) = x. [para(10(a,1),8(a,1,2)),demod(4(6))]. given #248 (F,wt=15): 4959 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x) # label(false). [back_demod(1210),demod(4669(5,R),4(4))]. given #249 (F,wt=15): 4989 f(x,f(f(c_0,f(y,z)),f(z,x))) = f(x,x) # label(false). [back_demod(4264),demod(4730(3,R))]. given #250 (F,wt=15): 4990 f(x,f(f(c_0,f(y,z)),f(x,z))) = f(x,x) # label(false). [back_demod(4221),demod(4730(3,R))]. given #251 (F,wt=15): 4991 f(x,f(f(c_0,f(y,z)),f(y,x))) = f(x,x) # label(false). [back_demod(4212),demod(4730(3,R))]. given #252 (T,wt=11): 4722 f(f(x,x),f(c_0,f(y,x))) = c_0. [back_demod(4565),demod(4650(4),4(4),4650(7))]. given #253 (A,wt=21): 80 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(z,y)),u)),v))) = x. [para(8(a,1),10(a,1,2,1)),demod(8(13))]. given #254 (F,wt=15): 4993 f(x,f(f(c_0,f(y,z)),f(x,y))) = f(x,x) # label(false). [back_demod(3695),demod(4730(3,R))]. given #255 (F,wt=15): 4996 f(f(f(x,y),z),f(f(c_0,f(y,x)),z)) = z # label(false). [back_demod(3629),demod(4730(5,R))]. low water: id=10445, wt=33 given #256 (F,wt=15): 4998 f(f(x,f(y,z)),f(f(c_0,f(z,y)),x)) = x # label(false). [back_demod(3620),demod(4730(5,R))]. given #257 (F,wt=15): 4999 f(f(f(c_0,f(x,y)),z),f(z,f(y,x))) = z # label(false). [back_demod(3618),demod(4730(3,R))]. given #258 (T,wt=11): 4727 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_demod(4551),demod(4650(4),4(4),4650(7))]. given #259 (A,wt=39): 82 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(10(a,1),9(a,1,2)),demod(4(8),4(11))]. given #260 (F,wt=15): 5135 f(f(x,f(c_0,f(y,z))),f(f(z,y),x)) = x # label(false). [back_demod(3626),demod(4730(3,R))]. given #261 (F,wt=15): 5136 f(f(f(x,y),z),f(z,f(c_0,f(y,x)))) = z # label(false). [back_demod(3615),demod(4730(5,R))]. given #262 (F,wt=15): 5597 f(f(x,f(y,z)),f(x,f(y,f(z,c_0)))) = x # label(false). [para(4657(a,1),8(a,1,2,2)),demod(4(7))]. given #263 (F,wt=15): 5601 f(f(f(x,f(y,c_0)),z),f(z,f(x,y))) = z # label(false). [para(4657(a,1),13(a,1,2,2))]. given #264 (T,wt=11): 5632 f(f(x,c_0),y) = f(y,f(x,x)). [para(4657(a,1),50(a,1,2)),demod(4(4),4716(4)),flip(a)]. given #265 (A,wt=21): 83 f(f(x,y),f(x,f(f(f(x,y),f(f(f(y,z),x),u)),v))) = x. [para(9(a,1),10(a,1,2,1)),demod(9(13))]. given #266 (F,wt=15): 5603 f(f(f(x,y),z),f(z,f(x,f(y,c_0)))) = z # label(false). [para(4657(a,1),20(a,1,1,1))]. given #267 (F,wt=15): 5605 f(f(x,f(y,f(z,c_0))),f(f(y,z),x)) = x # label(false). [para(4657(a,1),21(a,1,2,1))]. given #268 (F,wt=15): 5607 f(f(x,f(y,z)),f(f(y,f(z,c_0)),x)) = x # label(false). [para(4657(a,1),37(a,1,1,2))]. given #269 (F,wt=15): 5609 f(f(f(x,y),z),f(f(x,f(y,c_0)),z)) = z # label(false). [para(4657(a,1),44(a,1,2,1)),demod(4(7))]. given #270 (T,wt=11): 5721 f(x,f(c_0,f(f(x,x),y))) = c_0. [para(71(a,1),4659(a,2,2)),demod(4(4),4(5),4650(7))]. given #271 (A,wt=23): 84 f(f(x,y),f(f(f(x,y),f(y,z)),f(x,u))) = f(f(x,y),f(y,z)). [para(9(a,1),10(a,1,2,2,1))]. low water: id=10806, wt=31 given #272 (F,wt=15): 5675 f(f(x,f(y,z)),f(x,f(f(z,c_0),y))) = x # label(false). [para(4659(a,2),8(a,1,2,2))]. given #273 (F,wt=15): 5689 f(f(f(x,y),z),f(z,f(f(y,c_0),x))) = z # label(false). [para(4659(a,2),13(a,1,2,2))]. given #274 (F,wt=15): 5701 f(f(f(f(x,c_0),y),z),f(z,f(y,x))) = z # label(false). [para(4659(a,2),20(a,1,1,1))]. given #275 (F,wt=15): 5704 f(f(x,f(y,z)),f(f(f(z,c_0),y),x)) = x # label(false). [para(4659(a,2),21(a,1,2,1))]. given #276 (T,wt=11): 5722 f(x,f(c_0,f(y,f(x,x)))) = c_0. [para(73(a,1),4659(a,2,2)),demod(4(4),4(5),4650(7))]. given #277 (A,wt=23): 85 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v))) = x. [para(12(a,1),10(a,1,2,1)),demod(12(14))]. given #278 (F,wt=15): 5709 f(f(x,f(f(y,c_0),z)),f(f(z,y),x)) = x # label(false). [para(4659(a,2),37(a,1,1,2))]. given #279 (F,wt=15): 5713 f(f(f(x,y),z),f(f(f(y,c_0),x),z)) = z # label(false). [para(4659(a,2),44(a,1,2,1))]. given #280 (F,wt=15): 5727 f(x,f(f(y,c_0),z)) = f(x,f(z,f(z,y))) # label(false). [para(4659(a,2),17(a,1,2,1,2)),demod(25(8))]. given #281 (F,wt=15): 5893 f(f(f(x,c_0),y),z) = f(f(y,f(y,x)),z) # label(false). [para(4659(a,2),35(a,1,2,1,1)),demod(94(8))]. given #282 (T,wt=11): 5936 f(f(x,x),y) = f(y,f(x,c_0)). [para(4663(a,1),210(a,1,1)),demod(4(4),4715(4),5632(6,R),8(7))]. given #283 (A,wt=25): 86 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(12(a,1),10(a,1,2,2,1)),demod(4(5),4(11))]. given #284 (F,wt=15): 5912 f(x,f(y,f(f(z,f(y,c_0)),x))) = f(x,x) # label(false). [para(4659(a,1),3108(a,1,2,1)),demod(4(5),5640(5),4(4),4668(4))]. given #285 (F,wt=15): 5915 f(x,f(y,f(f(f(y,c_0),z),x))) = f(x,x) # label(false). [para(4659(a,1),3109(a,1,2,1)),demod(4(5),5640(5),4(4),4668(4))]. given #286 (F,wt=15): 5925 f(f(x,f(f(y,c_0),z)),f(x,f(z,y))) = x # label(false). [para(4663(a,1),8(a,1,2,2))]. given #287 (F,wt=15): 5931 f(f(f(f(x,c_0),y),z),f(f(y,x),z)) = z # label(false). [para(4663(a,1),44(a,1,2,1))]. given #288 (T,wt=11): 6402 f(x,f(y,f(c_0,x))) = f(x,x). [para(4650(a,1),3108(a,1,2,2,1)),demod(4730(3,R),4666(3))]. given #289 (A,wt=31): 87 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(10(a,1),13(a,1,1))]. given #290 (F,wt=15): 6340 f(x,f(y,f(z,c_0))) = f(x,f(y,f(y,z))) # label(false). [para(4665(a,1),17(a,1,2,1,2)),demod(17(7)),flip(a)]. low water: id=11537, wt=29 given #291 (F,wt=15): 6349 f(f(x,f(y,f(z,c_0))),f(x,f(z,z))) = x # label(false). [para(4665(a,2),243(a,1,1,2))]. given #292 (F,wt=15): 6350 f(f(f(x,f(y,c_0)),z),f(z,f(y,y))) = z # label(false). [para(4665(a,2),247(a,1,1,1))]. given #293 (F,wt=15): 6353 f(f(f(x,x),y),f(y,f(z,f(x,c_0)))) = y # label(false). [para(4665(a,2),252(a,1,2,2))]. given #294 (T,wt=11): 6872 f(x,f(f(c_0,x),y)) = f(c_0,x). [para(5595(a,1),21(a,1)),demod(4(4))]. given #295 (A,wt=21): 88 f(f(x,y),f(y,f(f(f(x,y),f(f(y,f(z,x)),u)),v))) = y. [para(13(a,1),10(a,1,2,1)),demod(13(13))]. given #296 (F,wt=15): 6354 f(f(x,f(y,f(z,c_0))),f(f(z,z),x)) = x # label(false). [para(4665(a,2),254(a,1,1,2))]. given #297 (F,wt=15): 6359 f(f(x,f(y,y)),f(f(z,f(y,c_0)),x)) = x # label(false). [para(4665(a,2),256(a,1,2,1))]. given #298 (F,wt=15): 6361 f(f(f(x,f(y,c_0)),z),f(f(y,y),z)) = z # label(false). [para(4665(a,2),258(a,1,1,1))]. given #299 (F,wt=15): 6368 f(f(x,f(y,y)),f(x,f(z,f(y,c_0)))) = x # label(false). [para(4665(a,2),700(a,1,2,2))]. given #300 (T,wt=11): 6890 f(x,f(c_0,y)) = f(x,f(y,y)). [para(5595(a,1),29(a,1,2)),demod(4(4),6402(4)),flip(a)]. given #301 (A,wt=31): 89 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(10(a,1),14(a,1,1))]. given #302 (F,wt=15): 6374 f(f(f(x,x),y),f(f(z,f(x,c_0)),y)) = y # label(false). [para(4665(a,2),805(a,1,2,1))]. given #303 (F,wt=15): 6377 f(f(x,f(y,c_0)),z) = f(f(x,f(x,y)),z) # label(false). [para(4665(a,1),35(a,1,2,1,1)),demod(35(7)),flip(a)]. low water: id=11955, wt=27 given #304 (F,wt=15): 6569 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,z))) # label(false). [para(4667(a,2),17(a,1,2,1,2)),demod(25(8))]. given #305 (F,wt=15): 6630 f(f(x,f(c_0,f(y,z))),f(x,f(z,y))) = x # label(false). [para(4667(a,2),700(a,1,2,2,2)),demod(4730(3,R),4663(8))]. given #306 (T,wt=11): 7076 f(f(c_0,x),y) = f(y,f(x,x)). [para(5665(a,2),3259(a,2)),flip(a)]. given #307 (A,wt=21): 90 f(f(x,y),f(y,f(f(f(x,y),f(f(f(x,z),y),u)),v))) = y. [para(14(a,1),10(a,1,2,1)),demod(14(13))]. given #308 (F,wt=15): 6640 f(f(f(c_0,f(x,y)),z),f(f(y,x),z)) = z # label(false). [para(4667(a,2),805(a,1,2,1,2)),demod(4730(3,R),4663(8))]. given #309 (F,wt=15): 6657 f(f(f(x,c_0),y),z) = f(f(y,f(x,y)),z) # label(false). [para(4667(a,2),35(a,1,2,1,1)),demod(94(8))]. given #310 (F,wt=15): 6684 f(f(x,f(y,z)),f(x,f(z,f(y,c_0)))) = x # label(false). [para(4669(a,2),8(a,1,2,2))]. given #311 (F,wt=15): 6688 f(f(f(x,y),z),f(z,f(y,f(x,c_0)))) = z # label(false). [para(4669(a,2),13(a,1,2,2))]. given #312 (T,wt=11): 7083 f(f(c_0,x),y) = f(f(x,x),y). [para(5665(a,2),3557(a,2)),flip(a)]. given #313 (A,wt=23): 91 f(f(x,y),f(f(f(x,y),f(x,z)),f(y,u))) = f(f(x,y),f(x,z)). [para(14(a,1),10(a,1,2,2,1))]. given #314 (F,wt=15): 6693 f(f(f(x,f(y,c_0)),z),f(z,f(y,x))) = z # label(false). [para(4669(a,2),20(a,1,1,1))]. given #315 (F,wt=15): 6695 f(f(x,f(y,z)),f(f(z,f(y,c_0)),x)) = x # label(false). [para(4669(a,2),21(a,1,2,1))]. given #316 (F,wt=15): 6698 f(f(x,f(y,f(z,c_0))),f(f(z,y),x)) = x # label(false). [para(4669(a,2),37(a,1,1,2))]. given #317 (F,wt=15): 6700 f(f(f(x,y),z),f(f(y,f(x,c_0)),z)) = z # label(false). [para(4669(a,2),44(a,1,2,1))]. given #318 (T,wt=11): 7117 f(x,f(c_0,f(f(x,c_0),y))) = c_0. [para(4658(a,1),10(a,1,2,2,1,2)),demod(4664(4),4664(10))]. given #319 (A,wt=23): 92 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(z,x),u)),v))) = z. [para(18(a,1),10(a,1,2,1)),demod(18(14))]. given #320 (F,wt=15): 6702 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,y))) # label(false). [para(4669(a,1),17(a,1,2,1,2)),demod(17(7)),flip(a)]. given #321 (F,wt=15): 6743 f(f(x,f(y,c_0)),z) = f(f(x,f(y,x)),z) # label(false). [para(4669(a,1),35(a,1,2,1,1)),demod(35(7)),flip(a)]. given #322 (F,wt=15): 6863 f(f(x,f(y,z)),f(x,f(y,f(c_0,z)))) = x # label(false). [para(5595(a,1),8(a,1,2,2)),demod(4(7))]. given #323 (F,wt=15): 6866 f(f(f(x,f(c_0,y)),z),f(z,f(x,y))) = z # label(false). [para(5595(a,1),13(a,1,2,2))]. given #324 (T,wt=11): 7118 f(x,f(c_0,f(y,f(x,c_0)))) = c_0. [para(4658(a,1),23(a,1,2,2,2,2)),demod(4664(4),4664(10))]. given #325 (A,wt=27): 93 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(10(a,1),10(a,1,2,1)),demod(10(17))]. given #326 (F,wt=15): 6869 f(f(f(x,y),z),f(z,f(x,f(c_0,y)))) = z # label(false). [para(5595(a,1),20(a,1,1,1))]. given #327 (F,wt=15): 6871 f(f(x,f(y,f(c_0,z))),f(f(y,z),x)) = x # label(false). [para(5595(a,1),21(a,1,2,1))]. given #328 (F,wt=15): 6873 f(f(x,f(y,z)),f(f(y,f(c_0,z)),x)) = x # label(false). [para(5595(a,1),37(a,1,1,2))]. given #329 (F,wt=15): 6875 f(f(f(x,y),z),f(f(x,f(c_0,y)),z)) = z # label(false). [para(5595(a,1),44(a,1,2,1)),demod(4(7))]. given #330 (T,wt=11): 7119 f(x,f(c_0,f(f(c_0,x),y))) = c_0. [para(4658(a,1),34(a,1,2,2,1,1)),demod(4664(4),4664(10))]. given #331 (A,wt=19): 94 f(x,f(f(f(y,z),x),f(f(x,z),u))) = f(f(y,z),x). [para(20(a,1),5(a,1,1))]. given #332 (F,wt=15): 6925 f(f(x,f(c_0,y)),f(x,f(z,f(z,y)))) = x # label(false). [para(5665(a,1),5(a,1,2,2))]. given #333 (F,wt=15): 6927 f(f(f(c_0,x),y),f(y,f(z,f(z,x)))) = y # label(false). [para(5665(a,1),7(a,1,2,2))]. given #334 (F,wt=15): 6930 f(f(x,f(y,z)),f(x,f(f(c_0,z),y))) = x # label(false). [para(5665(a,2),8(a,1,2,2))]. given #335 (F,wt=15): 6932 f(f(x,f(c_0,y)),f(f(z,f(z,y)),x)) = x # label(false). [para(5665(a,1),9(a,1,2,1))]. given #336 (T,wt=11): 7120 f(x,f(c_0,f(y,f(c_0,x)))) = c_0. [para(4658(a,1),39(a,1,2,2,2,1)),demod(4664(4),4664(10))]. given #337 (A,wt=17): 95 f(x,f(f(x,y),f(f(f(z,y),x),u))) = f(x,y). [para(20(a,1),7(a,1,1))]. given #338 (F,wt=15): 6934 f(f(x,f(y,f(y,z))),f(f(c_0,z),x)) = x # label(false). [para(5665(a,1),12(a,1,1,2))]. given #339 (F,wt=15): 6939 f(f(f(x,y),z),f(z,f(f(c_0,y),x))) = z # label(false). [para(5665(a,2),13(a,1,2,2))]. given #340 (F,wt=15): 6941 f(f(f(c_0,x),y),f(f(z,f(z,x)),y)) = y # label(false). [para(5665(a,1),14(a,1,2,1))]. given #341 (F,wt=15): 6943 f(f(f(x,f(x,y)),z),f(z,f(c_0,y))) = z # label(false). [para(5665(a,1),18(a,1,1,1))]. given #342 (T,wt=11): 7291 f(f(x,x),y) = f(y,f(c_0,x)). [para(5934(a,2),3557(a,2))]. given #343 (A,wt=17): 96 f(x,f(f(y,f(x,f(z,u))),f(z,x))) = f(z,x). [para(7(a,1),20(a,1,2)),demod(4(6))]. given #344 (F,wt=15): 6951 f(f(f(f(c_0,x),y),z),f(z,f(y,x))) = z # label(false). [para(5665(a,2),20(a,1,1,1))]. given #345 (F,wt=15): 6953 f(f(x,f(y,f(x,z))),f(f(c_0,z),x)) = x # label(false). [para(5665(a,2),20(a,1,2)),demod(4(3))]. given #346 (F,wt=15): 6954 f(f(x,f(y,z)),f(f(f(c_0,z),y),x)) = x # label(false). [para(5665(a,2),21(a,1,2,1))]. given #347 (F,wt=15): 6957 f(f(x,f(f(c_0,y),z)),f(f(z,y),x)) = x # label(false). [para(5665(a,2),37(a,1,1,2))]. given #348 (T,wt=11): 7674 f(f(c_0,f(x,y)),f(y,x)) = c_0. [para(3266(a,1),5934(a,1)),demod(5007(10),3707(7)),flip(a)]. given #349 (A,wt=19): 97 f(x,f(f(f(y,z),x),f(u,f(x,z)))) = f(f(y,z),x). [para(20(a,1),8(a,1,1))]. given #350 (F,wt=15): 6961 f(f(f(x,y),z),f(f(f(c_0,y),x),z)) = z # label(false). [para(5665(a,2),44(a,1,2,1))]. given #351 (F,wt=15): 6971 f(x,f(f(c_0,y),z)) = f(x,f(z,f(z,y))) # label(false). [para(5665(a,2),17(a,1,2,1,2)),demod(25(8))]. given #352 (F,wt=15): 7070 f(f(f(c_0,x),y),z) = f(f(y,f(y,x)),z) # label(false). [para(5665(a,2),35(a,1,2,1,1)),demod(94(8))]. low water: id=12881, wt=25 given #353 (F,wt=15): 7084 f(x,f(y,f(f(z,f(c_0,y)),x))) = f(x,x) # label(false). [para(5665(a,1),3108(a,1,2,1)),demod(4(5),5612(5),4(4),4660(4))]. given #354 (T,wt=11): 14190 f(f(x,y),f(c_0,f(y,x))) = c_0. [para(3043(a,2),4683(a,1,2,2,2)),demod(3707(5))]. given #355 (A,wt=15): 98 f(x,f(y,f(f(z,y),x))) = f(f(z,y),x). [para(20(a,1),8(a,1,2)),demod(4(3),4(4))]. given #356 (F,wt=15): 7087 f(x,f(y,f(f(f(c_0,y),z),x))) = f(x,x) # label(false). [para(5665(a,1),3109(a,1,2,1)),demod(4(5),5612(5),4(4),4660(4))]. given #357 (F,wt=15): 7251 f(x,f(y,f(c_0,z))) = f(x,f(y,f(y,z))) # label(false). [para(5934(a,1),17(a,1,2,1,2)),demod(17(7)),flip(a)]. given #358 (F,wt=15): 7259 f(f(x,f(y,f(c_0,z))),f(x,f(z,z))) = x # label(false). [para(5934(a,2),243(a,1,1,2))]. given #359 (F,wt=15): 7260 f(f(f(x,f(c_0,y)),z),f(z,f(y,y))) = z # label(false). [para(5934(a,2),247(a,1,1,1))]. given #360 (T,wt=13): 6506 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [para(3108(a,1),43(a,1,2)),demod(127(4),127(5),4730(4,R),4727(5),127(6)),flip(a)]. given #361 (A,wt=19): 99 f(x,f(f(f(x,y),z),f(f(u,y),x))) = f(f(u,y),x). [para(20(a,1),9(a,1,1))]. given #362 (F,wt=15): 7263 f(f(f(x,x),y),f(y,f(z,f(c_0,x)))) = y # label(false). [para(5934(a,2),252(a,1,2,2))]. given #363 (F,wt=15): 7264 f(f(x,f(y,f(c_0,z))),f(f(z,z),x)) = x # label(false). [para(5934(a,2),254(a,1,1,2))]. given #364 (F,wt=15): 7269 f(f(x,f(y,y)),f(f(z,f(c_0,y)),x)) = x # label(false). [para(5934(a,2),256(a,1,2,1))]. given #365 (F,wt=15): 7271 f(f(f(x,f(c_0,y)),z),f(f(y,y),z)) = z # label(false). [para(5934(a,2),258(a,1,1,1))]. given #366 (T,wt=13): 6509 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(3109(a,1),43(a,1,2)),demod(42(4),42(5),4730(4,R),4727(5),42(6)),flip(a)]. given #367 (A,wt=17): 100 f(x,f(f(y,f(f(z,u),x)),f(x,z))) = f(x,z). [para(9(a,1),20(a,1,2)),demod(4(6))]. given #368 (F,wt=15): 7278 f(f(x,f(y,y)),f(x,f(z,f(c_0,y)))) = x # label(false). [para(5934(a,2),700(a,1,2,2))]. given #369 (F,wt=15): 7284 f(f(f(x,x),y),f(f(z,f(c_0,x)),y)) = y # label(false). [para(5934(a,2),805(a,1,2,1))]. given #370 (F,wt=15): 7287 f(f(x,f(c_0,y)),z) = f(f(x,f(x,y)),z) # label(false). [para(5934(a,1),35(a,1,2,1,1)),demod(35(7)),flip(a)]. given #371 (F,wt=15): 7303 f(f(x,f(c_0,y)),f(x,f(z,f(y,z)))) = x # label(false). [para(6525(a,1),5(a,1,2,2))]. given #372 (T,wt=13): 6574 f(f(x,y),f(y,x)) = f(c_0,f(x,y)). [para(4667(a,2),206(a,1,2,2)),demod(4663(5),4730(6,R))]. given #373 (A,wt=19): 101 f(x,f(f(y,f(z,x)),f(x,f(z,u)))) = f(x,f(z,u)). [para(12(a,1),20(a,1,2)),demod(4(6))]. given #374 (F,wt=15): 7306 f(f(f(c_0,x),y),f(y,f(z,f(x,z)))) = y # label(false). [para(6525(a,1),7(a,1,2,2))]. given #375 (F,wt=15): 7313 f(f(x,f(c_0,y)),f(f(z,f(y,z)),x)) = x # label(false). [para(6525(a,1),9(a,1,2,1))]. given #376 (F,wt=15): 7315 f(f(x,f(y,f(z,y))),f(f(c_0,z),x)) = x # label(false). [para(6525(a,1),12(a,1,1,2))]. given #377 (F,wt=15): 7323 f(f(f(c_0,x),y),f(f(z,f(x,z)),y)) = y # label(false). [para(6525(a,1),14(a,1,2,1))]. given #378 (T,wt=13): 7681 f(f(c_0,x),f(f(c_0,f(x,y)),z)) = x. [para(10(a,1),4660(a,1,2)),demod(4660(4)),flip(a)]. given #379 (A,wt=17): 102 f(x,f(f(x,y),f(z,f(f(u,y),x)))) = f(x,y). [para(20(a,1),13(a,1,1))]. given #380 (F,wt=15): 7325 f(f(f(x,f(y,x)),z),f(z,f(c_0,y))) = z # label(false). [para(6525(a,1),18(a,1,1,1))]. given #381 (F,wt=15): 7328 f(f(x,f(f(y,x),z)),f(f(c_0,y),x)) = x # label(false). [para(6525(a,2),18(a,1,2)),demod(4(3))]. given #382 (F,wt=15): 7337 f(f(x,f(y,f(z,x))),f(f(c_0,z),x)) = x # label(false). [para(6525(a,2),20(a,1,2)),demod(4(3))]. given #383 (F,wt=15): 7357 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,z))) # label(false). [para(6525(a,2),17(a,1,2,1,2)),demod(25(8))]. low water: id=13702, wt=23 given #384 (T,wt=13): 7682 f(f(x,c_0),f(f(c_0,f(x,y)),z)) = x. [para(15(a,1),4660(a,1,2)),demod(4668(4)),flip(a)]. given #385 (A,wt=17): 103 f(x,f(f(y,f(x,f(z,u))),f(u,x))) = f(u,x). [para(13(a,1),20(a,1,2)),demod(4(6))]. given #386 (F,wt=15): 7457 f(f(f(c_0,x),y),z) = f(f(y,f(x,y)),z) # label(false). [para(6525(a,2),35(a,1,2,1,1)),demod(94(8))]. given #387 (F,wt=15): 7490 f(f(x,f(y,z)),f(x,f(z,f(c_0,y)))) = x # label(false). [para(6682(a,2),8(a,1,2,2))]. given #388 (F,wt=15): 7494 f(f(f(x,y),z),f(z,f(y,f(c_0,x)))) = z # label(false). [para(6682(a,2),13(a,1,2,2))]. given #389 (F,wt=15): 7502 f(f(f(x,f(c_0,y)),z),f(z,f(y,x))) = z # label(false). [para(6682(a,2),20(a,1,1,1))]. given #390 (T,wt=13): 7687 f(f(c_0,x),f(f(c_0,f(y,x)),z)) = x. [para(22(a,1),4660(a,1,2)),demod(4660(4)),flip(a)]. given #391 (A,wt=19): 104 f(x,f(f(y,f(x,z)),f(f(z,u),x))) = f(f(z,u),x). [para(18(a,1),20(a,1,2)),demod(4(6))]. given #392 (F,wt=15): 7505 f(f(x,f(y,z)),f(f(z,f(c_0,y)),x)) = x # label(false). [para(6682(a,2),21(a,1,2,1))]. given #393 (F,wt=15): 7508 f(f(x,f(y,f(c_0,z))),f(f(z,y),x)) = x # label(false). [para(6682(a,2),37(a,1,1,2))]. given #394 (F,wt=15): 7510 f(f(f(x,y),z),f(f(y,f(c_0,x)),z)) = z # label(false). [para(6682(a,2),44(a,1,2,1))]. given #395 (F,wt=15): 7512 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,y))) # label(false). [para(6682(a,1),17(a,1,2,1,2)),demod(17(7)),flip(a)]. given #396 (T,wt=13): 7689 f(f(c_0,x),f(y,f(c_0,f(x,z)))) = x. [para(23(a,1),4660(a,1,2)),demod(4660(4)),flip(a)]. given #397 (A,wt=23): 105 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(z,y),u)),v))) = z. [para(20(a,1),10(a,1,2,1)),demod(20(14))]. given #398 (F,wt=15): 7553 f(f(x,f(c_0,y)),z) = f(f(x,f(y,x)),z) # label(false). [para(6682(a,1),35(a,1,2,1,1)),demod(35(7)),flip(a)]. given #399 (F,wt=15): 7572 f(f(x,f(y,f(z,z))),f(x,f(z,y))) = x # label(false). [para(3266(a,1),4(a,1)),flip(a)]. given #400 (F,wt=15): 7669 f(f(x,f(f(c_0,y),z)),f(x,f(z,y))) = x # label(false). [para(5665(a,1),3266(a,1,2,2,2)),demod(4(9),5612(9),4(8),4660(8))]. given #401 (F,wt=15): 7913 f(f(f(x,f(y,x)),z),f(z,f(x,y))) = z # label(false). [para(3258(a,1),3276(a,1,1,1)),demod(4730(6,R),4666(6))]. given #402 (T,wt=13): 7692 f(f(x,c_0),f(y,f(c_0,f(x,z)))) = x. [para(26(a,1),4660(a,1,2)),demod(4668(4)),flip(a)]. given #403 (A,wt=39): 106 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(10(a,1),20(a,1,1)),demod(4(10))]. given #404 (F,wt=15): 7963 f(f(f(x,f(y,y)),z),f(f(y,x),z)) = z # label(false). [para(4(a,1),3291(a,1,2))]. given #405 (F,wt=15): 8077 f(f(f(x,f(x,y)),z),f(z,f(y,x))) = z # label(false). [para(3259(a,1),3291(a,1,1,1))]. given #406 (F,wt=15): 8151 f(f(x,f(y,f(z,y))),f(f(y,z),x)) = x # label(false). [para(3258(a,1),3297(a,1,1,2)),demod(4730(6,R),4666(6))]. given #407 (F,wt=15): 8215 f(f(x,f(y,f(y,z))),f(f(z,y),x)) = x # label(false). [para(3259(a,1),3301(a,1,1,2))]. given #408 (T,wt=13): 7694 f(f(c_0,x),f(y,f(c_0,f(z,x)))) = x. [para(28(a,1),4660(a,1,2)),demod(4660(4)),flip(a)]. given #409 (A,wt=19): 107 f(x,f(f(y,f(x,z)),f(f(u,z),x))) = f(f(u,z),x). [para(20(a,1),20(a,1,2)),demod(4(6))]. given #410 (F,wt=15): 8492 f(f(f(f(c_0,x),y),z),f(f(y,x),z)) = z # label(false). [para(5665(a,1),3306(a,1,2,1,2)),demod(4(9),5612(9),4(8),4660(8))]. given #411 (F,wt=15): 8508 f(f(x,f(y,y)),z) = f(z,f(x,f(y,x))) # label(false). [para(3314(a,1),4(a,1)),flip(a)]. given #412 (F,wt=15): 8509 f(f(x,f(y,x)),z) = f(z,f(x,f(y,y))) # label(false). [para(3314(a,2),4(a,1)),flip(a)]. given #413 (F,wt=15): 8911 f(f(c_0,f(x,f(y,x))),f(f(y,c_0),x)) = c_0 # label(false). [para(3319(a,1),6682(a,1)),demod(6531(12)),flip(a)]. given #414 (T,wt=13): 7698 f(f(x,c_0),f(f(c_0,f(y,x)),z)) = x. [para(45(a,1),4660(a,1,2)),demod(4668(4)),flip(a)]. given #415 (A,wt=21): 108 f(f(x,y),f(x,f(f(f(x,y),f(f(f(z,y),x),u)),v))) = x. [para(21(a,1),10(a,1,2,1)),demod(21(13))]. given #416 (F,wt=15): 8912 f(f(x,f(y,f(z,y))),f(x,f(c_0,z))) = x # label(false). [para(6682(a,2),3319(a,1,2))]. given #417 (F,wt=15): 9037 f(f(f(x,f(y,x)),z),f(f(c_0,y),z)) = z # label(false). [para(6525(a,2),3323(a,1,2))]. given #418 (F,wt=15): 9356 f(f(x,f(y,f(y,z))),f(x,f(c_0,z))) = x # label(false). [para(6682(a,2),3355(a,1,2))]. given #419 (F,wt=15): 9480 f(f(f(x,f(x,y)),z),f(f(c_0,y),z)) = z # label(false). [para(6525(a,2),3358(a,1,2))]. given #420 (T,wt=13): 9177 f(f(x,c_0),f(y,f(c_0,f(z,x)))) = x. [para(49(a,1),4660(a,1,2)),demod(4668(4)),flip(a)]. given #421 (A,wt=23): 109 f(f(x,y),f(f(f(x,y),f(z,y)),f(x,u))) = f(f(x,y),f(z,y)). [para(21(a,1),10(a,1,2,2,1))]. given #422 (F,wt=15): 10039 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x) # label(false). [para(31(a,1),3477(a,1,2,1))]. given #423 (F,wt=15): 10081 f(x,f(y,f(x,f(z,f(y,c_0))))) = f(x,x) # label(false). [para(4659(a,1),3477(a,1,2,1)),demod(4(5),5640(5),4(4),4668(4))]. given #424 (F,wt=15): 10088 f(x,f(y,f(x,f(z,f(c_0,y))))) = f(x,x) # label(false). [para(5665(a,1),3477(a,1,2,1)),demod(4(5),5612(5),4(4),4660(4))]. given #425 (F,wt=15): 10113 f(x,f(f(c_0,y),f(f(z,y),x))) = f(x,x) # label(false). [para(4730(a,2),3108(a,1,2,1))]. given #426 (T,wt=13): 12985 f(f(x,x),f(f(x,y),f(z,x))) = c_0. [para(3477(a,1),61(a,1,2)),demod(67(4),67(5),4730(4,R),4727(5),67(5)),flip(a)]. given #427 (A,wt=17): 110 f(x,f(f(y,f(f(z,u),x)),f(x,u))) = f(x,u). [para(21(a,1),20(a,1,2)),demod(4(6))]. given #428 (F,wt=15): 10114 f(x,f(f(c_0,y),f(f(y,z),x))) = f(x,x) # label(false). [para(4730(a,2),3109(a,1,2,1))]. given #429 (F,wt=15): 10117 f(x,f(f(c_0,y),f(x,f(z,y)))) = f(x,x) # label(false). [para(4730(a,2),3477(a,1,2,1))]. given #430 (F,wt=15): 10291 f(f(x,f(y,f(y,z))),f(x,f(z,y))) = x # label(false). [para(3557(a,1),3561(a,1,1,2)),demod(4730(6,R),4666(6))]. given #431 (F,wt=15): 10644 f(x,f(f(y,c_0),f(x,f(z,y)))) = f(x,x) # label(false). [para(4746(a,2),3477(a,1,2,1))]. given #432 (T,wt=13): 13882 f(f(x,c_0),f(f(x,y),f(x,z))) = c_0. [para(4654(a,1),43(a,1,2)),demod(4720(6),4720(7),4730(5,R),7(6),4720(8)),flip(a)]. given #433 (A,wt=23): 111 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(z,x),u)),v))) = x. [para(37(a,1),10(a,1,2,1)),demod(37(14))]. given #434 (F,wt=15): 10974 f(f(f(x,f(x,y)),z),f(f(y,x),z)) = z # label(false). [para(3557(a,1),3590(a,1,1,1)),demod(4730(6,R),4666(6))]. given #435 (F,wt=15): 11094 f(f(f(x,x),y),z) = f(z,f(y,f(x,y))) # label(false). [para(3594(a,1),4(a,1)),flip(a)]. given #436 (F,wt=15): 11095 f(f(x,f(y,x)),z) = f(z,f(f(y,y),x)) # label(false). [para(3594(a,2),4(a,1)),flip(a)]. given #437 (F,wt=15): 11584 f(f(x,f(y,f(z,c_0))),f(x,f(z,y))) = x # label(false). [para(4669(a,2),3706(a,1,1,2)),demod(4730(7,R),4695(8))]. given #438 (T,wt=13): 13900 f(f(x,c_0),f(f(y,x),f(x,z))) = c_0. [para(4655(a,1),43(a,1,2)),demod(4717(6),4717(7),4730(5,R),7(6),4717(8)),flip(a)]. given #439 (A,wt=25): 112 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(37(a,1),10(a,1,2,2,1)),demod(4(5),4(11))]. given #440 (F,wt=15): 11589 f(f(x,f(y,f(c_0,z))),f(x,f(z,y))) = x # label(false). [para(6682(a,2),3706(a,1,1,2)),demod(4730(7,R),4695(8))]. given #441 (F,wt=15): 11935 f(f(f(x,f(y,c_0)),z),f(f(y,x),z)) = z # label(false). [para(4669(a,2),3734(a,1,1,1)),demod(4730(7,R),4695(8))]. given #442 (F,wt=15): 11937 f(f(f(x,f(c_0,y)),z),f(f(y,x),z)) = z # label(false). [para(6682(a,2),3734(a,1,1,1)),demod(4730(7,R),4695(8))]. given #443 (F,wt=15): 12003 f(f(x,f(y,y)),z) = f(z,f(x,f(x,y))) # label(false). [para(3737(a,1),4(a,1)),flip(a)]. given #444 (T,wt=13): 14383 f(f(x,f(c_0,f(y,z))),f(y,c_0)) = y. [para(26(a,1),4695(a,1,2)),demod(7692(14))]. given #445 (A,wt=19): 113 f(x,f(f(y,f(z,x)),f(x,f(u,z)))) = f(x,f(u,z)). [para(37(a,1),20(a,1,2)),demod(4(6))]. given #446 (F,wt=15): 12004 f(f(x,f(x,y)),z) = f(z,f(x,f(y,y))) # label(false). [para(3737(a,2),4(a,1)),flip(a)]. given #447 (F,wt=15): 13184 f(x,f(y,f(z,f(z,x)))) = f(x,f(y,y)) # label(false). [para(3872(a,1),38(a,1,2)),flip(a)]. given #448 (F,wt=15): 13186 f(x,f(f(y,z),f(x,f(z,y)))) = f(x,x) # label(false). [para(3043(a,2),3872(a,1,2,2,2,2)),demod(3707(4))]. given #449 (F,wt=15): 13192 f(x,f(y,f(x,f(f(y,y),z)))) = f(x,x) # label(false). [para(3557(a,2),3872(a,1,2,2,2))]. given #450 (T,wt=13): 14387 f(f(x,f(c_0,f(y,z))),f(z,c_0)) = z. [para(49(a,1),4695(a,1,2)),demod(9177(14))]. given #451 (A,wt=17): 114 f(x,f(f(y,x),f(f(f(z,y),x),u))) = f(y,x). [para(44(a,1),5(a,1,1))]. given #452 (F,wt=15): 13196 f(x,f(y,f(x,f(f(y,c_0),z)))) = f(x,x) # label(false). [para(4659(a,2),3872(a,1,2,2,2))]. given #453 (F,wt=15): 13197 f(x,f(y,f(y,f(f(y,x),z)))) = f(x,x) # label(false). [para(3872(a,1),43(a,1)),flip(a)]. given #454 (F,wt=15): 13198 f(x,f(f(y,c_0),f(x,f(y,z)))) = f(x,x) # label(false). [para(4669(a,1),3872(a,1,2,2,2,2)),demod(16(5))]. given #455 (F,wt=15): 13200 f(x,f(y,f(x,f(f(c_0,y),z)))) = f(x,x) # label(false). [para(5665(a,2),3872(a,1,2,2,2))]. given #456 (T,wt=13): 14592 f(f(x,x),f(f(c_0,f(x,y)),z)) = x. [para(5665(a,1),76(a,2)),demod(7681(9),7(6),4(9),3043(10,R),4(6)),flip(a)]. given #457 (A,wt=19): 115 f(x,f(f(y,f(x,z)),f(x,f(z,u)))) = f(x,f(z,u)). [para(5(a,1),44(a,1,1))]. given #458 (F,wt=15): 13202 f(x,f(f(c_0,y),f(x,f(y,z)))) = f(x,x) # label(false). [para(6682(a,1),3872(a,1,2,2,2,2)),demod(16(5))]. given #459 (F,wt=15): 13234 f(x,f(y,f(y,f(f(x,y),z)))) = f(x,x) # label(false). [para(3872(a,1),58(a,1)),flip(a)]. given #460 (F,wt=15): 13268 f(x,f(y,f(z,f(x,z)))) = f(x,f(y,y)) # label(false). [para(3873(a,1),38(a,1,2)),flip(a)]. given #461 (F,wt=15): 13717 f(f(f(x,x),y),z) = f(z,f(y,f(y,x))) # label(false). [para(4166(a,1),4(a,1)),flip(a)]. given #462 (T,wt=13): 14745 f(f(x,x),f(y,f(c_0,f(x,z)))) = x. [para(4(a,1),14623(a,1,2,2)),demod(6682(4,R))]. given #463 (A,wt=19): 116 f(x,f(f(f(y,z),x),f(f(z,x),u))) = f(f(y,z),x). [para(44(a,1),7(a,1,1))]. given #464 (F,wt=15): 13718 f(f(x,f(x,y)),z) = f(z,f(f(y,y),x)) # label(false). [para(4166(a,2),4(a,1)),flip(a)]. given #465 (F,wt=15): 13766 f(x,f(f(y,f(x,x)),z)) = f(x,f(z,z)) # label(false). [para(4271(a,1),53(a,1,2)),flip(a)]. given #466 (F,wt=15): 13772 f(x,f(y,f(c_0,f(f(x,y),z)))) = f(x,x) # label(false). [para(4271(a,1),63(a,1)),demod(4730(6,R),4(7)),flip(a)]. given #467 (F,wt=15): 13799 f(x,f(c_0,f(y,f(f(z,f(y,z)),x)))) = c_0 # label(false). [para(4389(a,1),3259(a,2,2)),demod(4730(9,R),4650(9))]. given #468 (T,wt=13): 14797 f(f(x,x),f(f(c_0,f(y,x)),z)) = x. [para(3557(a,2),14684(a,1,1)),demod(4730(3,R),4(6))]. given #469 (A,wt=17): 117 f(x,f(f(y,x),f(z,f(f(u,y),x)))) = f(y,x). [para(44(a,1),8(a,1,1))]. given #470 (F,wt=15): 13800 f(x,f(f(y,f(x,y)),z)) = f(x,f(z,z)) # label(false). [para(4389(a,1),53(a,1,2)),flip(a)]. given #471 (F,wt=15): 13829 f(x,f(f(y,z),f(f(z,y),x))) = f(x,x) # label(false). [para(3043(a,2),4397(a,1,2,2,1,2)),demod(3707(4))]. given #472 (F,wt=15): 13830 f(x,f(c_0,f(y,f(f(z,f(z,y)),x)))) = c_0 # label(false). [para(4397(a,1),3259(a,2,2)),demod(4730(9,R),4650(9))]. given #473 (F,wt=15): 13831 f(x,f(f(y,f(y,x)),z)) = f(x,f(z,z)) # label(false). [para(4397(a,1),53(a,1,2)),flip(a)]. given #474 (T,wt=13): 14803 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(4(a,1),14703(a,1,2,2)),demod(6682(4,R))]. given #475 (A,wt=19): 118 f(x,f(f(y,f(x,z)),f(x,f(u,z)))) = f(x,f(u,z)). [para(8(a,1),44(a,1,1))]. given #476 (F,wt=15): 13856 f(x,f(f(f(x,x),y),z)) = f(x,f(z,z)) # label(false). [para(4448(a,1),53(a,1,2)),flip(a)]. given #477 (F,wt=15): 13886 f(x,f(y,f(c_0,f(f(y,x),z)))) = f(x,x) # label(false). [para(66(a,1),4271(a,1)),demod(4730(5,R),4(6))]. given #478 (F,wt=15): 14124 f(f(f(x,f(c_0,y)),z),f(f(y,c_0),z)) = z # label(false). [para(5934(a,2),4682(a,1,1,1))]. given #479 (F,wt=15): 14154 f(f(x,f(y,f(c_0,z))),f(f(z,c_0),x)) = x # label(false). [para(5934(a,2),4688(a,1,1,2))]. given #480 (T,wt=13): 16288 f(f(x,x),f(f(y,x),f(z,x))) = c_0. [para(4(a,1),6506(a,1,2,2))]. given #481 (A,wt=19): 119 f(x,f(f(f(y,z),x),f(u,f(z,x)))) = f(f(y,z),x). [para(44(a,1),13(a,1,1))]. given #482 (F,wt=15): 14155 f(f(x,y),f(c_0,f(y,f(y,f(x,z))))) = c_0 # label(false). [para(12(a,1),4683(a,1,2,2,2)),demod(4(5))]. given #483 (F,wt=15): 14156 f(f(f(x,y),z),f(c_0,f(z,f(x,z)))) = c_0 # label(false). [para(14(a,1),4683(a,1,2,2,2)),demod(4(5))]. given #484 (F,wt=15): 14161 f(f(f(x,y),z),f(c_0,f(z,f(z,y)))) = c_0 # label(false). [para(21(a,1),4683(a,1,2,2,2)),demod(4(5))]. given #485 (F,wt=15): 14162 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0 # label(false). [para(37(a,1),4683(a,1,2,2,2)),demod(4(5))]. given #486 (T,wt=13): 16332 f(f(c_0,x),f(f(y,x),f(x,z))) = c_0. [para(4730(a,2),6506(a,1,1))]. given #487 (A,wt=19): 120 f(x,f(f(f(y,x),z),f(f(u,y),x))) = f(f(u,y),x). [para(44(a,1),14(a,1,1))]. given #488 (F,wt=15): 14163 f(f(f(x,y),z),f(c_0,f(z,f(y,z)))) = c_0 # label(false). [para(44(a,1),4683(a,1,2,2,2)),demod(4(5))]. given #489 (F,wt=15): 14167 f(f(x,f(y,f(z,y))),f(c_0,f(x,z))) = c_0 # label(false). [para(223(a,1),4683(a,1,2,2,2)),demod(4(7),6682(7,R),4666(7))]. given #490 (F,wt=15): 14168 f(f(f(x,f(y,x)),z),f(c_0,f(z,y))) = c_0 # label(false). [para(229(a,1),4683(a,1,2,2,2)),demod(4(7),3707(7))]. given #491 (F,wt=15): 14173 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0 # label(false). [para(252(a,1),4683(a,1,2,2,2)),demod(4(7),6682(7,R),4666(7))]. given #492 (T,wt=13): 16388 f(f(c_0,x),f(f(x,y),f(x,z))) = c_0. [para(4730(a,2),6509(a,1,1))]. given #493 (A,wt=19): 121 f(x,f(f(y,f(z,x)),f(f(z,u),x))) = f(f(z,u),x). [para(14(a,1),44(a,1,1))]. given #494 (F,wt=15): 14178 f(f(f(x,f(x,y)),z),f(c_0,f(z,y))) = c_0 # label(false). [para(256(a,1),4683(a,1,2,2,2)),demod(4(7),3707(7))]. given #495 (F,wt=15): 14208 f(f(c_0,f(x,y)),f(f(z,f(x,z)),y)) = c_0 # label(false). [para(3338(a,1),4683(a,1,2,2,2)),demod(4(7),16(7),4(7))]. given #496 (F,wt=15): 14211 f(f(c_0,f(x,y)),f(f(z,f(z,x)),y)) = c_0 # label(false). [para(3372(a,1),4683(a,1,2,2,2)),demod(4(7),16(7),4(7))]. given #497 (F,wt=15): 14212 f(f(x,f(y,f(z,y))),f(c_0,f(z,x))) = c_0 # label(false). [para(3380(a,1),4683(a,1,2,2,2)),demod(4(7),16(7))]. given #498 (T,wt=13): 16454 f(f(x,c_0),f(f(x,y),f(z,x))) = c_0. [para(4654(a,1),101(a,1,2)),demod(4720(6),4720(7),4730(5,R),13(6),4720(8)),flip(a)]. given #499 (A,wt=21): 123 f(f(x,y),f(y,f(f(f(x,y),f(f(f(z,x),y),u)),v))) = y. [para(44(a,1),10(a,1,2,1)),demod(44(13))]. given #500 (F,wt=15): 14213 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0 # label(false). [para(3405(a,1),4683(a,1,2,2,2)),demod(4(7),16(7))]. given #501 (F,wt=15): 14306 f(f(f(x,f(c_0,y)),z),f(z,f(y,c_0))) = z # label(false). [para(5934(a,2),4692(a,1,1,1))]. given #502 (F,wt=15): 14312 f(f(x,f(y,f(c_0,z))),f(x,f(z,c_0))) = x # label(false). [para(5934(a,2),4693(a,1,1,2))]. given #503 (F,wt=15): 14336 f(x,f(y,f(y,f(f(x,x),z)))) = f(x,x) # label(false). [para(74(a,1),3872(a,1))]. given #504 (T,wt=13): 16455 f(f(x,c_0),f(f(y,x),f(z,x))) = c_0. [para(4655(a,1),101(a,1,2)),demod(4717(6),4717(7),4730(5,R),13(6),4717(8)),flip(a)]. given #505 (A,wt=23): 124 f(f(x,y),f(f(f(x,y),f(z,x)),f(y,u))) = f(f(x,y),f(z,x)). [para(44(a,1),10(a,1,2,2,1))]. given #506 (F,wt=15): 14474 f(x,f(f(x,f(y,z)),f(c_0,z))) = f(x,x) # label(false). [para(12(a,1),4945(a,1,2,2,2))]. given #507 (F,wt=15): 14476 f(x,f(f(x,f(y,z)),f(c_0,y))) = f(x,x) # label(false). [para(18(a,1),4945(a,1,2,2,2))]. given #508 (F,wt=15): 14482 f(x,f(f(x,f(y,z)),f(y,c_0))) = f(x,x) # label(false). [para(27(a,1),4945(a,1,2,2))]. given #509 (F,wt=15): 14487 f(x,f(f(x,f(y,z)),f(z,c_0))) = f(x,x) # label(false). [para(50(a,1),4945(a,1,2,2))]. given #510 (T,wt=13): 17015 f(f(c_0,x),f(f(y,x),f(z,x))) = c_0. [para(10113(a,1),101(a,1,2)),demod(5971(6),5971(7),4730(5,R),8(6),5971(8)),flip(a)]. given #511 (A,wt=31): 125 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(10(a,1),44(a,1,1))]. given #512 (F,wt=15): 14523 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x) # label(false). [para(4683(a,1),4945(a,1,2,1)),demod(4660(9))]. given #513 (F,wt=15): 14550 f(f(x,y),f(c_0,f(x,f(x,f(y,z))))) = c_0 # label(false). [para(5(a,1),4698(a,1,2,2,2)),demod(4(5))]. given #514 (F,wt=15): 14551 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0 # label(false). [para(8(a,1),4698(a,1,2,2,2)),demod(4(5))]. given #515 (F,wt=15): 14587 f(x,f(y,f(c_0,f(z,f(x,z))))) = f(x,x) # label(false). [para(4698(a,1),4945(a,1,2,1)),demod(4660(9))]. given #516 (T,wt=13): 17041 f(f(c_0,x),f(f(x,y),f(z,x))) = c_0. [para(4730(a,2),12985(a,1,1))]. given #517 (A,wt=19): 126 f(x,f(f(y,f(z,x)),f(f(u,z),x))) = f(f(u,z),x). [para(44(a,1),44(a,1,1))]. given #518 (F,wt=15): 14597 f(f(c_0,f(x,y)),f(z,f(z,x))) = f(x,y) # label(false). [para(5(a,1),14591(a,1,2,2,2))]. given #519 (F,wt=15): 14598 f(f(c_0,f(x,y)),f(z,f(z,y))) = f(x,y) # label(false). [para(7(a,1),14591(a,1,2,2,2))]. given #520 (F,wt=15): 14601 f(f(c_0,f(x,y)),f(z,f(x,z))) = f(x,y) # label(false). [para(14(a,1),14591(a,1,2,2)),demod(4(5))]. given #521 (F,wt=15): 14606 f(f(c_0,f(x,y)),f(z,f(y,z))) = f(x,y) # label(false). [para(44(a,1),14591(a,1,2,2)),demod(4(5))]. given #522 (T,wt=15): 132 f(f(x,y),f(y,f(f(y,f(x,z)),u))) = y. [para(15(a,1),8(a,1,2)),demod(4(6))]. given #523 (A,wt=19): 128 f(f(x,y),f(x,f(f(f(x,y),f(f(x,x),z)),u))) = x. [para(42(a,1),10(a,1,2,1)),demod(42(11))]. given #524 (F,wt=15): 14608 f(x,f(y,f(y,f(z,f(x,z))))) = f(x,x) # label(false). [para(226(a,1),14591(a,1,2,2)),demod(4666(3),4(4))]. given #525 (F,wt=15): 14609 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x) # label(false). [para(254(a,1),14591(a,1,2,2)),demod(4666(3),4(4))]. given #526 (F,wt=15): 14611 f(x,f(y,f(y,f(f(x,c_0),z)))) = f(x,c_0) # label(false). [para(3043(a,2),14591(a,1,1)),demod(4666(3))]. given #527 (F,wt=15): 14613 f(x,f(y,f(y,f(f(c_0,x),z)))) = f(c_0,x) # label(false). [para(3259(a,2),14591(a,1,1)),demod(4666(3))]. given #528 (T,wt=15): 173 f(f(x,f(f(x,y),z)),f(x,f(y,u))) = x. [para(17(a,1),8(a,1,2))]. given #529 (A,wt=23): 129 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v))) = x. [para(5(a,1),15(a,1,2,1)),demod(5(14))]. given #530 (F,wt=15): 14644 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z) # label(false). [para(5(a,1),14594(a,1,1,2,2))]. given #531 (F,wt=15): 14645 f(f(x,f(x,y)),f(c_0,f(z,y))) = f(z,y) # label(false). [para(7(a,1),14594(a,1,1,2,2))]. given #532 (F,wt=15): 14646 f(f(x,f(y,x)),f(c_0,f(y,z))) = f(y,z) # label(false). [para(14(a,1),14594(a,1,1,2)),demod(4(2))]. given #533 (F,wt=15): 14647 f(f(x,f(y,x)),f(c_0,f(z,y))) = f(z,y) # label(false). [para(44(a,1),14594(a,1,1,2)),demod(4(2))]. given #534 (T,wt=15): 193 f(f(x,f(y,z)),f(x,f(f(x,y),u))) = x. [para(17(a,1),37(a,1,1)),demod(4(5))]. given #535 (A,wt=31): 130 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(15(a,1),7(a,1,1))]. given #536 (F,wt=15): 14688 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,x) # label(false). [para(3043(a,1),14596(a,1,1)),demod(4668(4))]. given #537 (F,wt=15): 14689 f(x,f(y,f(y,f(z,f(x,c_0))))) = f(x,c_0) # label(false). [para(3043(a,2),14596(a,1,1)),demod(4666(3))]. given #538 (F,wt=15): 14691 f(x,f(y,f(y,f(z,f(c_0,x))))) = f(c_0,x) # label(false). [para(3259(a,2),14596(a,1,1)),demod(4666(3))]. given #539 (F,wt=15): 14887 f(x,f(f(c_0,f(y,f(y,x))),z)) = f(x,x) # label(false). [para(4683(a,1),4959(a,1,2,1)),demod(4660(9))]. given #540 (T,wt=15): 362 f(f(x,y),f(x,f(f(x,f(z,y)),u))) = x. [para(8(a,1),24(a,1,2,1)),demod(8(10))]. given #541 (A,wt=21): 131 f(f(x,y),f(y,f(z,f(f(x,y),f(f(y,f(x,u)),v))))) = y. [para(15(a,1),8(a,1,1))]. given #542 (F,wt=15): 14888 f(x,f(f(c_0,f(y,f(x,y))),z)) = f(x,x) # label(false). [para(4698(a,1),4959(a,1,2,1)),demod(4660(9))]. given #543 (F,wt=15): 15223 f(f(f(x,c_0),y),z) = f(z,f(y,f(y,x))) # label(false). [para(5727(a,1),4(a,1)),flip(a)]. given #544 (F,wt=15): 15224 f(f(x,f(x,y)),z) = f(z,f(f(y,c_0),x)) # label(false). [para(5727(a,2),4(a,1)),flip(a)]. given #545 (F,wt=15): 15315 f(x,f(f(y,f(x,c_0)),z)) = f(x,f(z,z)) # label(false). [para(5912(a,1),53(a,1,2)),flip(a)]. given #546 (T,wt=15): 364 f(f(x,y),f(x,f(f(f(y,z),x),u))) = x. [para(9(a,1),24(a,1,2,1)),demod(9(10))]. given #547 (A,wt=23): 133 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(x,z),u)),v))) = x. [para(8(a,1),15(a,1,2,1)),demod(8(14))]. given #548 (F,wt=15): 15335 f(x,f(f(f(x,c_0),y),z)) = f(x,f(z,z)) # label(false). [para(5915(a,1),53(a,1,2)),flip(a)]. given #549 (F,wt=15): 15364 f(f(x,f(y,c_0)),z) = f(z,f(x,f(x,y))) # label(false). [para(6340(a,1),4(a,1)),flip(a)]. given #550 (F,wt=15): 15365 f(f(x,f(x,y)),z) = f(z,f(x,f(y,c_0))) # label(false). [para(6340(a,2),4(a,1)),flip(a)]. given #551 (F,wt=15): 15402 f(f(x,f(y,f(z,c_0))),f(x,f(c_0,z))) = x # label(false). [para(4730(a,2),6349(a,1,2,2))]. given #552 (T,wt=15): 365 f(f(x,f(y,z)),f(x,f(f(y,x),u))) = x. [para(12(a,1),24(a,1,2,1)),demod(12(10))]. given #553 (A,wt=39): 135 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(15(a,1),9(a,1,2)),demod(4(8),4(11))]. given #554 (F,wt=15): 15424 f(f(f(x,f(y,c_0)),z),f(z,f(c_0,y))) = z # label(false). [para(4730(a,2),6350(a,1,2,2))]. given #555 (F,wt=15): 15444 f(f(x,f(y,f(z,c_0))),f(f(c_0,z),x)) = x # label(false). [para(4730(a,2),6354(a,1,2,1))]. given #556 (F,wt=15): 15451 f(f(f(x,f(y,c_0)),z),f(f(c_0,y),z)) = z # label(false). [para(4730(a,2),6361(a,1,2,1))]. given #557 (F,wt=15): 15454 f(f(x,f(c_0,y)),f(x,f(z,f(y,y)))) = x # label(false). [para(6890(a,1),8(a,1,2,2))]. given #558 (T,wt=15): 367 f(f(x,y),f(y,f(f(y,f(z,x)),u))) = y. [para(13(a,1),24(a,1,2,1)),demod(13(10))]. given #559 (A,wt=23): 136 f(f(x,y),f(f(f(y,z),f(x,y)),f(x,u))) = f(f(y,z),f(x,y)). [para(9(a,1),15(a,1,2,2,1))]. given #560 (F,wt=15): 15459 f(f(f(c_0,x),y),f(y,f(z,f(x,x)))) = y # label(false). [para(6890(a,1),13(a,1,2,2))]. given #561 (F,wt=15): 15463 f(f(f(x,f(y,y)),z),f(z,f(c_0,y))) = z # label(false). [para(6890(a,1),20(a,1,1,1))]. given #562 (F,wt=15): 15465 f(f(x,f(c_0,y)),f(f(z,f(y,y)),x)) = x # label(false). [para(6890(a,1),21(a,1,2,1))]. given #563 (F,wt=15): 15467 f(f(x,f(y,f(z,z))),f(f(c_0,z),x)) = x # label(false). [para(6890(a,1),37(a,1,1,2))]. given #564 (T,wt=15): 369 f(f(x,y),f(y,f(f(f(x,z),y),u))) = y. [para(14(a,1),24(a,1,2,1)),demod(14(10))]. given #565 (A,wt=31): 137 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(15(a,1),13(a,1,1))]. given #566 (F,wt=15): 15470 f(f(f(c_0,x),y),f(f(z,f(x,x)),y)) = y # label(false). [para(6890(a,1),44(a,1,2,1))]. given #567 (F,wt=15): 15556 f(f(f(x,c_0),y),z) = f(z,f(y,f(x,y))) # label(false). [para(6569(a,1),4(a,1)),flip(a)]. given #568 (F,wt=15): 15557 f(f(x,f(y,x)),z) = f(z,f(f(y,c_0),x)) # label(false). [para(6569(a,2),4(a,1)),flip(a)]. given #569 (F,wt=15): 15596 f(f(f(x,f(y,y)),z),f(f(c_0,y),z)) = z # label(false). [para(7076(a,2),20(a,1,2))]. given #570 (T,wt=15): 370 f(f(f(x,y),z),f(z,f(f(z,x),u))) = z. [para(18(a,1),24(a,1,2,1)),demod(18(10))]. given #571 (A,wt=31): 138 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(15(a,1),14(a,1,1))]. given #572 (F,wt=15): 15757 f(f(x,f(y,c_0)),z) = f(z,f(x,f(y,x))) # label(false). [para(6702(a,1),4(a,1)),flip(a)]. given #573 (F,wt=15): 15758 f(f(x,f(y,x)),z) = f(z,f(x,f(y,c_0))) # label(false). [para(6702(a,2),4(a,1)),flip(a)]. given #574 (F,wt=15): 15930 f(f(x,f(y,f(z,z))),f(x,f(c_0,z))) = x # label(false). [para(7291(a,1),37(a,1,2))]. given #575 (F,wt=15): 15986 f(f(c_0,f(x,f(y,x))),f(x,f(y,y))) = c_0 # label(false). [para(3043(a,2),7674(a,1,2)),demod(4(3))]. given #576 (T,wt=15): 374 f(f(f(x,y),z),f(z,f(f(z,y),u))) = z. [para(20(a,1),24(a,1,2,1)),demod(20(10))]. given #577 (A,wt=23): 139 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(x,z),u)),v))) = z. [para(14(a,1),15(a,1,2,1)),demod(14(14))]. given #578 (F,wt=15): 15988 f(f(c_0,f(x,f(x,y))),f(x,f(y,y))) = c_0 # label(false). [para(3259(a,2),7674(a,1,2)),demod(4(3))]. given #579 (F,wt=15): 15989 f(f(c_0,f(x,f(x,y))),f(x,f(y,c_0))) = c_0 # label(false). [para(4659(a,1),7674(a,1,1,2))]. given #580 (F,wt=15): 15990 f(f(c_0,f(x,f(x,y))),f(f(y,c_0),x)) = c_0 # label(false). [para(4659(a,2),7674(a,1,2)),demod(4(3))]. given #581 (F,wt=15): 15991 f(f(c_0,f(x,f(y,x))),f(x,f(y,c_0))) = c_0 # label(false). [para(4667(a,1),7674(a,1,1,2))]. given #582 (T,wt=15): 375 f(f(x,y),f(x,f(f(f(z,y),x),u))) = x. [para(21(a,1),24(a,1,2,1)),demod(21(10))]. given #583 (A,wt=23): 140 f(f(x,y),f(f(f(x,z),f(x,y)),f(y,u))) = f(f(x,z),f(x,y)). [para(14(a,1),15(a,1,2,2,1))]. given #584 (F,wt=15): 15993 f(f(c_0,f(x,f(x,y))),f(x,f(c_0,y))) = c_0 # label(false). [para(5665(a,1),7674(a,1,1,2))]. given #585 (F,wt=15): 15995 f(f(c_0,f(x,f(y,x))),f(x,f(c_0,y))) = c_0 # label(false). [para(6525(a,1),7674(a,1,1,2))]. given #586 (F,wt=15): 16051 f(f(f(c_0,x),y),z) = f(z,f(y,f(y,x))) # label(false). [para(6971(a,1),4(a,1)),flip(a)]. given #587 (F,wt=15): 16052 f(f(x,f(x,y)),z) = f(z,f(f(c_0,y),x)) # label(false). [para(6971(a,2),4(a,1)),flip(a)]. given #588 (T,wt=15): 376 f(f(x,f(y,z)),f(x,f(f(z,x),u))) = x. [para(37(a,1),24(a,1,2,1)),demod(37(10))]. given #589 (A,wt=27): 141 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(15(a,1),10(a,1,2,1)),demod(15(17))]. given #590 (F,wt=15): 16124 f(x,f(f(y,f(c_0,x)),z)) = f(x,f(z,z)) # label(false). [para(7084(a,1),53(a,1,2)),flip(a)]. given #591 (F,wt=15): 16202 f(x,f(f(f(c_0,x),y),z)) = f(x,f(z,z)) # label(false). [para(7087(a,1),53(a,1,2)),flip(a)]. given #592 (F,wt=15): 16217 f(f(x,f(c_0,y)),z) = f(z,f(x,f(x,y))) # label(false). [para(7251(a,1),4(a,1)),flip(a)]. given #593 (F,wt=15): 16218 f(f(x,f(x,y)),z) = f(z,f(x,f(c_0,y))) # label(false). [para(7251(a,2),4(a,1)),flip(a)]. given #594 (T,wt=15): 378 f(f(x,y),f(y,f(f(f(z,x),y),u))) = y. [para(44(a,1),24(a,1,2,1)),demod(44(10))]. given #595 (A,wt=37): 142 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(10(a,1),15(a,1,2,1)),demod(10(22))]. given #596 (F,wt=15): 16446 f(x,f(f(x,f(y,z)),f(z,y))) = f(x,x) # label(false). [para(6574(a,1),4945(a,1,2,2,2)),demod(4660(7))]. given #597 (F,wt=15): 16449 f(x,f(y,f(y,f(z,f(y,x))))) = f(x,x) # label(false). [para(101(a,1),3872(a,1))]. given #598 (F,wt=15): 16565 f(f(f(c_0,x),y),z) = f(z,f(y,f(x,y))) # label(false). [para(7357(a,1),4(a,1)),flip(a)]. given #599 (F,wt=15): 16566 f(f(x,f(y,x)),z) = f(z,f(f(c_0,y),x)) # label(false). [para(7357(a,2),4(a,1)),flip(a)]. given #600 (T,wt=15): 392 f(f(x,f(f(y,x),z)),f(x,f(y,u))) = x. [para(19(a,1),8(a,1,2))]. given #601 (A,wt=39): 143 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(15(a,1),20(a,1,1)),demod(4(10))]. given #602 (F,wt=15): 16695 f(x,f(y,f(c_0,f(z,f(x,y))))) = f(x,x) # label(false). [para(104(a,1),4271(a,1)),demod(4730(5,R),4(6))]. given #603 (F,wt=15): 16696 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x) # label(false). [para(104(a,1),4389(a,1)),demod(4(3),4(5))]. given #604 (F,wt=15): 16710 f(f(x,f(c_0,y)),z) = f(z,f(x,f(y,x))) # label(false). [para(7512(a,1),4(a,1)),flip(a)]. given #605 (F,wt=15): 16711 f(f(x,f(y,x)),z) = f(z,f(x,f(c_0,y))) # label(false). [para(7512(a,2),4(a,1)),flip(a)]. given #606 (T,wt=15): 606 f(f(x,f(y,z)),f(x,f(f(x,z),u))) = x. [para(8(a,1),27(a,1,2,1)),demod(8(10))]. given #607 (A,wt=23): 144 f(f(x,y),f(f(f(z,y),f(x,y)),f(x,u))) = f(f(z,y),f(x,y)). [para(21(a,1),15(a,1,2,2,1))]. given #608 (F,wt=15): 16961 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x) # label(false). [para(10039(a,1),101(a,1)),demod(4730(6,R)),flip(a)]. given #609 (F,wt=15): 17229 f(x,f(y,f(x,f(f(y,x),z)))) = f(x,x) # label(false). [para(79(a,1),113(a,1,2)),demod(4(5)),flip(a)]. given #610 (F,wt=15): 17286 f(x,f(y,f(z,f(z,x)))) = f(x,f(y,x)) # label(false). [para(13184(a,2),3043(a,1))]. given #611 (F,wt=15): 17290 f(x,f(c_0,f(y,f(z,f(z,x))))) = f(x,y) # label(false). [para(13184(a,1),3259(a,2,2)),demod(4730(7,R),3707(9))]. given #612 (T,wt=15): 610 f(f(f(x,y),z),f(z,f(f(x,z),u))) = z. [para(14(a,1),27(a,1,2,1)),demod(14(10))]. given #613 (A,wt=31): 145 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(15(a,1),44(a,1,1))]. given #614 (F,wt=15): 17304 f(x,f(c_0,f(y,f(z,f(x,z))))) = f(x,y) # label(false). [para(3740(a,1),13184(a,1,2)),demod(4730(8,R)),flip(a)]. given #615 (F,wt=15): 17305 f(x,f(c_0,f(f(y,f(x,y)),z))) = f(x,z) # label(false). [para(3743(a,1),13184(a,1,2)),demod(4730(8,R)),flip(a)]. given #616 (F,wt=15): 17306 f(x,f(c_0,f(f(y,f(y,x)),z))) = f(x,z) # label(false). [para(3770(a,1),13184(a,1,2)),demod(4730(8,R)),flip(a)]. given #617 (F,wt=15): 17477 f(x,f(y,f(z,f(x,z)))) = f(x,f(y,x)) # label(false). [para(13268(a,2),3043(a,1))]. given #618 (T,wt=15): 615 f(f(f(x,y),z),f(z,f(f(y,z),u))) = z. [para(44(a,1),27(a,1,2,1)),demod(44(10))]. given #619 (A,wt=23): 146 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(y,z),u)),v))) = z. [para(44(a,1),15(a,1,2,1)),demod(44(14))]. given #620 (F,wt=15): 17483 f(x,f(c_0,f(y,z))) = f(x,f(x,f(z,y))) # label(false). [para(5135(a,1),13268(a,1,2)),demod(15077(9),15077(10),4730(6,R)),flip(a)]. given #621 (F,wt=15): 17516 f(x,f(f(y,f(x,x)),z)) = f(x,f(x,z)) # label(false). [para(13766(a,1),11(a,1,2,2)),demod(3707(3)),flip(a)]. given #622 (F,wt=15): 17525 f(x,f(y,f(z,f(x,x)))) = f(x,f(y,c_0)) # label(false). [para(16(a,1),13766(a,1,2)),demod(4669(10,R),4669(15,R),4730(15,R),17522(12))]. given #623 (F,wt=15): 17707 f(x,f(f(y,f(x,y)),z)) = f(x,f(x,z)) # label(false). [para(13800(a,1),11(a,1,2,2)),demod(3707(3)),flip(a)]. given #624 (T,wt=15): 882 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x. [para(5(a,1),29(a,1,2,1)),demod(5(10))]. given #625 (A,wt=23): 147 f(f(x,y),f(f(f(z,x),f(x,y)),f(y,u))) = f(f(z,x),f(x,y)). [para(44(a,1),15(a,1,2,2,1))]. given #626 (F,wt=15): 17834 f(x,f(f(y,f(y,x)),z)) = f(x,f(x,z)) # label(false). [para(13831(a,1),11(a,1,2,2)),demod(3707(3)),flip(a)]. given #627 (F,wt=15): 17890 f(x,f(f(f(x,x),y),z)) = f(x,f(x,z)) # label(false). [para(13856(a,1),11(a,1,2,2)),demod(3707(3)),flip(a)]. given #628 (F,wt=15): 17897 f(x,f(y,f(f(x,x),z))) = f(x,f(y,c_0)) # label(false). [para(16(a,1),13856(a,1,2)),demod(4669(10,R),4669(15,R),4730(15,R),17517(12))]. given #629 (F,wt=15): 18026 f(f(c_0,f(x,f(x,f(y,z)))),f(y,x)) = c_0 # label(false). [para(14155(a,1),4(a,1)),flip(a)]. given #630 (T,wt=15): 883 f(f(x,y),f(y,f(z,f(y,f(x,u))))) = y. [para(7(a,1),29(a,1,2,1)),demod(7(10))]. given #631 (A,wt=37): 148 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(15(a,1),15(a,1,2,1)),demod(15(22))]. given #632 (F,wt=15): 18027 f(f(f(x,y),z),f(c_0,f(z,f(z,x)))) = c_0 # label(false). [para(5(a,1),14155(a,1,2,2,2,2))]. given #633 (F,wt=15): 18082 f(f(c_0,f(x,f(y,x))),f(f(y,z),x)) = c_0 # label(false). [para(14156(a,1),4(a,1)),flip(a)]. given #634 (F,wt=15): 18150 f(f(c_0,f(x,f(x,y))),f(f(z,y),x)) = c_0 # label(false). [para(14161(a,1),4(a,1)),flip(a)]. given #635 (F,wt=15): 18194 f(f(c_0,f(x,f(x,f(y,z)))),f(z,x)) = c_0 # label(false). [para(14162(a,1),4(a,1)),flip(a)]. given #636 (T,wt=15): 885 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x. [para(8(a,1),29(a,1,2,1)),demod(8(10))]. given #637 (A,wt=19): 154 f(f(x,y),f(y,f(f(f(x,y),f(f(y,y),z)),u))) = y. [para(67(a,1),15(a,1,2,1)),demod(67(11))]. given #638 (F,wt=15): 18287 f(f(c_0,f(x,f(y,x))),f(f(z,y),x)) = c_0 # label(false). [para(14163(a,1),4(a,1)),flip(a)]. given #639 (F,wt=15): 18314 f(f(c_0,f(x,y)),f(x,f(z,f(y,z)))) = c_0 # label(false). [para(14167(a,1),4(a,1)),flip(a)]. given #640 (F,wt=15): 18477 f(f(c_0,f(x,y)),f(f(z,f(y,z)),x)) = c_0 # label(false). [para(14168(a,1),4(a,1)),flip(a)]. given #641 (F,wt=15): 18530 f(f(c_0,f(x,y)),f(x,f(z,f(z,y)))) = c_0 # label(false). [para(14173(a,1),4(a,1)),flip(a)]. given #642 (T,wt=15): 887 f(f(x,y),f(x,f(z,f(f(y,u),x)))) = x. [para(9(a,1),29(a,1,2,1)),demod(9(10))]. given #643 (A,wt=25): 164 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(71(a,1),15(a,1,2,1)),demod(71(13))]. given #644 (F,wt=15): 18635 f(f(c_0,f(x,y)),f(f(z,f(z,y)),x)) = c_0 # label(false). [para(14178(a,1),4(a,1)),flip(a)]. given #645 (F,wt=15): 18658 f(f(c_0,f(x,y)),f(y,f(z,f(x,z)))) = c_0 # label(false). [para(4(a,1),14208(a,1,2))]. given #646 (F,wt=15): 18679 f(f(c_0,f(x,y)),f(y,f(z,f(z,x)))) = c_0 # label(false). [para(4(a,1),14211(a,1,2))]. given #647 (F,wt=15): 18809 f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x) # label(false). [para(362(a,1),113(a,1,2)),demod(4(5)),flip(a)]. given #648 (T,wt=15): 888 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. [para(12(a,1),29(a,1,2,1)),demod(12(10))]. given #649 (A,wt=25): 170 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(73(a,1),15(a,1,2,1)),demod(73(13))]. given #650 (F,wt=15): 18810 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x) # label(false). [para(362(a,1),118(a,1,2)),demod(4(5)),flip(a)]. given #651 (F,wt=15): 18820 f(x,f(f(y,f(x,c_0)),z)) = f(x,f(x,z)) # label(false). [para(15315(a,1),11(a,1,2,2)),demod(3707(3)),flip(a)]. given #652 (F,wt=15): 18822 f(x,f(y,f(z,f(x,c_0)))) = f(x,f(y,c_0)) # label(false). [para(16(a,1),15315(a,1,2)),demod(4669(13,R),4669(19,R),4730(18,R),17572(14))]. given #653 (F,wt=15): 18824 f(x,f(f(f(x,c_0),y),z)) = f(x,f(x,z)) # label(false). [para(15335(a,1),11(a,1,2,2)),demod(3707(3)),flip(a)]. given #654 (T,wt=15): 890 f(f(x,y),f(y,f(z,f(y,f(u,x))))) = y. [para(13(a,1),29(a,1,2,1)),demod(13(10))]. given #655 (A,wt=33): 171 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(17(a,1),7(a,1,1))]. given #656 (F,wt=15): 18825 f(x,f(y,f(f(x,c_0),z))) = f(x,f(y,c_0)) # label(false). [para(16(a,1),15335(a,1,2)),demod(4669(13,R),4669(19,R),4730(18,R),18821(14))]. given #657 (F,wt=15): 18962 f(x,f(f(y,f(c_0,x)),z)) = f(x,f(x,z)) # label(false). [para(16124(a,1),11(a,1,2,2)),demod(3707(3)),flip(a)]. given #658 (F,wt=15): 18964 f(x,f(y,f(z,f(c_0,x)))) = f(x,f(y,c_0)) # label(false). [para(16(a,1),16124(a,1,2)),demod(4669(13,R),4669(19,R),4730(18,R),17578(14))]. given #659 (F,wt=15): 18971 f(x,f(f(f(c_0,x),y),z)) = f(x,f(x,z)) # label(false). [para(16202(a,1),11(a,1,2,2)),demod(3707(3)),flip(a)]. given #660 (T,wt=15): 892 f(f(x,y),f(y,f(z,f(f(x,u),y)))) = y. [para(14(a,1),29(a,1,2,1)),demod(14(10))]. given #661 (A,wt=23): 172 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(f(x,y),v))))) = x. [para(17(a,1),8(a,1,1))]. given #662 (F,wt=15): 18978 f(x,f(y,f(f(c_0,x),z))) = f(x,f(y,c_0)) # label(false). [para(16(a,1),16202(a,1,2)),demod(4669(13,R),4669(19,R),4730(18,R),18963(14))]. given #663 (F,wt=15): 19122 f(x,f(y,f(f(x,y),z))) = f(x,f(y,y)) # label(false). [para(17229(a,1),38(a,1,2)),flip(a)]. given #664 (F,wt=15): 19144 f(x,f(y,f(f(y,x),z))) = f(x,f(c_0,y)) # label(false). [para(18(a,1),17290(a,1,2,2)),demod(4(6)),flip(a)]. given #665 (F,wt=15): 19447 f(f(c_0,f(x,y)),z) = f(z,f(z,f(y,x))) # label(false). [para(17483(a,1),4(a,1)),flip(a)]. given #666 (T,wt=15): 893 f(f(f(x,y),z),f(z,f(u,f(z,x)))) = z. [para(18(a,1),29(a,1,2,1)),demod(18(10))]. given #667 (A,wt=31): 174 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(8(a,1),17(a,1,2,2,1))]. given #668 (F,wt=15): 19777 f(f(c_0,f(x,f(x,y))),f(f(y,z),x)) = c_0 # label(false). [para(5(a,1),18026(a,1,1,2,2,2))]. given #669 (F,wt=15): 19974 f(f(c_0,f(x,f(y,x))),f(x,f(y,z))) = c_0 # label(false). [para(4(a,1),18082(a,1,2))]. given #670 (F,wt=15): 20010 f(f(c_0,f(x,f(x,y))),f(x,f(z,y))) = c_0 # label(false). [para(4(a,1),18150(a,1,2))]. given #671 (F,wt=15): 20105 f(f(c_0,f(x,f(y,x))),f(x,f(z,y))) = c_0 # label(false). [para(4(a,1),18287(a,1,2))]. given #672 (T,wt=15): 897 f(f(f(x,y),z),f(z,f(u,f(z,y)))) = z. [para(20(a,1),29(a,1,2,1)),demod(20(10))]. given #673 (A,wt=41): 176 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(17(a,1),9(a,1,2)),demod(4(8),4(12))]. given #674 (F,wt=15): 20111 f(f(c_0,f(x,f(x,y))),f(x,f(y,z))) = c_0 # label(false). [para(17(a,1),18314(a,1,2))]. given #675 (F,wt=15): 20132 f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)) # label(false). [para(18809(a,1),38(a,1,2)),flip(a)]. given #676 (F,wt=15): 20139 f(x,f(y,f(z,f(y,x)))) = f(x,f(y,y)) # label(false). [para(18810(a,1),38(a,1,2)),flip(a)]. given #677 (F,wt=15): 20229 f(x,f(f(y,y),z)) = f(x,f(f(y,x),z)) # label(false). [para(13772(a,1),20132(a,1,2,2)),demod(4(6),19240(6),4730(12,R),4660(9))]. given #678 (T,wt=15): 898 f(f(x,y),f(x,f(z,f(f(u,y),x)))) = x. [para(21(a,1),29(a,1,2,1)),demod(21(10))]. given #679 (A,wt=17): 177 f(f(x,y),f(x,f(f(f(x,y),f(y,z)),u))) = x. [para(9(a,1),17(a,1,2,1)),demod(9(11))]. given #680 (F,wt=15): 20230 f(x,f(f(y,y),z)) = f(x,f(f(x,y),z)) # label(false). [para(13886(a,1),20132(a,1,2,2)),demod(4(6),19239(6),4730(12,R),4660(9))]. given #681 (F,wt=15): 20231 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,x))) # label(false). [para(16695(a,1),20132(a,1,2,2)),demod(7076(6,R),19159(7),4730(13,R),4660(10))]. given #682 (F,wt=15): 20232 f(x,f(f(c_0,y),z)) = f(x,f(z,f(x,y))) # label(false). [para(16961(a,1),20132(a,1,2,2)),demod(7076(6,R),19158(7),4730(13,R),4660(10))]. given #683 (F,wt=15): 20233 f(f(f(x,x),y),z) = f(z,f(f(x,z),y)) # label(false). [para(20229(a,1),4(a,1)),flip(a)]. given #684 (T,wt=15): 899 f(f(x,f(y,z)),f(x,f(u,f(z,x)))) = x. [para(37(a,1),29(a,1,2,1)),demod(37(10))]. given #685 (A,wt=31): 178 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(9(a,1),17(a,1,2,2,1))]. given #686 (F,wt=15): 20234 f(x,f(f(y,x),z)) = f(x,f(z,f(y,y))) # label(false). [para(4(a,1),20229(a,1,2)),flip(a)]. given #687 (F,wt=15): 20235 f(x,f(f(y,y),z)) = f(x,f(z,f(y,x))) # label(false). [para(4(a,1),20229(a,2,2))]. given #688 (F,wt=15): 20236 f(x,f(f(f(y,y),x),z)) = f(x,f(y,z)) # label(false). [para(31(a,1),20229(a,1,2,1)),flip(a)]. given #689 (F,wt=15): 20239 f(x,f(f(y,x),z)) = f(x,f(z,f(y,z))) # label(false). [para(3258(a,1),20229(a,1,2)),flip(a)]. given #690 (T,wt=15): 901 f(f(x,y),f(y,f(z,f(f(u,x),y)))) = y. [para(44(a,1),29(a,1,2,1)),demod(44(10))]. given #691 (A,wt=19): 179 f(f(x,f(y,z)),f(x,f(f(y,f(x,f(y,z))),u))) = x. [para(12(a,1),17(a,1,2,1)),demod(4(5),12(12))]. given #692 (F,wt=15): 20240 f(x,f(f(x,f(y,x)),z)) = f(x,f(y,z)) # label(false). [para(3258(a,1),20229(a,2,2,1)),demod(4730(3,R),4666(3)),flip(a)]. given #693 (F,wt=15): 20241 f(x,f(f(y,x),z)) = f(x,f(z,f(z,y))) # label(false). [para(3557(a,1),20229(a,1,2)),flip(a)]. given #694 (F,wt=15): 20242 f(x,f(f(x,f(x,y)),z)) = f(x,f(y,z)) # label(false). [para(3557(a,1),20229(a,2,2,1)),demod(4730(3,R),4666(3)),flip(a)]. given #695 (F,wt=15): 20247 f(x,f(f(c_0,y),z)) = f(x,f(f(y,x),z)) # label(false). [para(4730(a,2),20229(a,1,2,1))]. given #696 (T,wt=15): 1242 f(f(x,f(f(x,y),z)),f(x,f(u,y))) = x. [para(25(a,1),8(a,1,2))]. given #697 (A,wt=33): 183 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(17(a,1),14(a,1,1))]. given #698 (F,wt=15): 20248 f(x,f(f(y,c_0),z)) = f(x,f(f(y,x),z)) # label(false). [para(4746(a,2),20229(a,1,2,1))]. given #699 (F,wt=15): 20260 f(x,f(f(y,x),z)) = f(x,f(z,f(y,c_0))) # label(false). [para(5936(a,1),20229(a,1,2)),flip(a)]. given #700 (F,wt=15): 20262 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,x))) # label(false). [para(6693(a,1),20229(a,1,2)),demod(12(13),4(9),20261(9))]. given #701 (F,wt=15): 20263 f(x,f(f(y,x),z)) = f(x,f(z,f(c_0,y))) # label(false). [para(7291(a,1),20229(a,1,2)),flip(a)]. given #702 (T,wt=15): 1585 f(f(x,f(y,f(x,f(z,u)))),f(z,x)) = x. [para(26(a,1),8(a,1,2))]. given #703 (A,wt=41): 189 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(17(a,1),20(a,1,1)),demod(4(11))]. given #704 (F,wt=15): 20266 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,x))) # label(false). [para(7502(a,1),20229(a,1,2)),demod(37(13),4(9),20264(9))]. given #705 (F,wt=15): 20268 f(f(x,f(y,x)),z) = f(z,f(f(y,z),x)) # label(false). [para(20229(a,1),11095(a,2))]. given #706 (F,wt=15): 20274 f(f(x,f(x,y)),z) = f(z,f(f(y,z),x)) # label(false). [para(20229(a,1),13718(a,2))]. given #707 (F,wt=15): 20388 f(f(f(x,x),y),z) = f(z,f(f(z,x),y)) # label(false). [para(20230(a,1),4(a,1)),flip(a)]. given #708 (T,wt=15): 1869 f(f(x,f(y,z)),f(x,f(u,f(x,y)))) = x. [para(5(a,1),50(a,1,2,1)),demod(5(10))]. given #709 (A,wt=33): 197 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(17(a,1),44(a,1,1))]. given #710 (F,wt=15): 20389 f(x,f(f(x,y),z)) = f(x,f(z,f(y,y))) # label(false). [para(4(a,1),20230(a,1,2)),flip(a)]. given #711 (F,wt=15): 20390 f(x,f(f(y,y),z)) = f(x,f(z,f(x,y))) # label(false). [para(4(a,1),20230(a,2,2))]. given #712 (F,wt=15): 20426 f(x,f(f(x,y),z)) = f(x,f(z,f(y,z))) # label(false). [para(3258(a,1),20230(a,1,2)),flip(a)]. given #713 (F,wt=15): 20434 f(x,f(f(x,y),z)) = f(x,f(z,f(z,y))) # label(false). [para(3557(a,1),20230(a,1,2)),flip(a)]. given #714 (T,wt=15): 1871 f(f(x,f(y,z)),f(x,f(u,f(x,z)))) = x. [para(8(a,1),50(a,1,2,1)),demod(8(10))]. given #715 (A,wt=41): 201 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(17(a,1),15(a,1,2,1)),demod(17(23))]. given #716 (F,wt=15): 20437 f(x,f(f(y,c_0),z)) = f(x,f(f(x,y),z)) # label(false). [para(4657(a,1),20230(a,2,2,1)),demod(4730(7,R),20432(7))]. given #717 (F,wt=15): 20442 f(x,f(f(c_0,y),z)) = f(x,f(f(x,y),z)) # label(false). [para(5595(a,1),20230(a,2,2,1)),demod(4730(7,R),20432(7))]. given #718 (F,wt=15): 20504 f(x,f(f(x,y),z)) = f(x,f(z,f(y,c_0))) # label(false). [para(5936(a,1),20230(a,1,2)),flip(a)]. given #719 (F,wt=15): 20524 f(x,f(f(x,y),z)) = f(x,f(z,f(c_0,y))) # label(false). [para(7291(a,1),20230(a,1,2)),flip(a)]. given #720 (T,wt=15): 1874 f(f(f(x,y),z),f(z,f(u,f(x,z)))) = z. [para(14(a,1),50(a,1,2,1)),demod(14(10))]. given #721 (A,wt=25): 279 f(x,f(f(f(x,f(y,y)),z),f(x,f(u,f(y,u))))) = f(x,f(u,f(y,u))). [para(210(a,1),9(a,1,1))]. given #722 (F,wt=15): 20541 f(f(x,f(y,x)),z) = f(z,f(f(z,y),x)) # label(false). [para(20230(a,1),11095(a,2))]. given #723 (F,wt=15): 20549 f(f(x,f(x,y)),z) = f(z,f(f(z,y),x)) # label(false). [para(20230(a,1),13718(a,2))]. given #724 (F,wt=15): 20679 f(f(c_0,f(x,y)),z) = f(y,f(y,f(x,z))) # label(false). [back_demod(16661),demod(20425(5)),flip(a)]. given #725 (F,wt=15): 20685 f(x,f(c_0,f(y,z))) = f(y,f(y,f(x,z))) # label(false). [back_demod(19265),demod(20679(7),16745(6),20679(8))]. given #726 (T,wt=15): 1879 f(f(f(x,y),z),f(z,f(u,f(y,z)))) = z. [para(44(a,1),50(a,1,2,1)),demod(44(10))]. given #727 (A,wt=21): 285 f(x,f(f(y,y),f(x,f(z,f(y,z))))) = f(x,f(z,f(y,z))) # label(false). [para(210(a,1),13(a,1,2)),demod(4(6))]. given #728 (F,wt=15): 20686 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [back_demod(19163),demod(20679(7),16843(6),20679(8))]. given #729 (F,wt=15): 20722 f(x,f(y,f(y,f(x,z)))) = f(x,f(y,z)) # label(false). [back_demod(20432),demod(20679(4))]. given #730 (F,wt=15): 20797 f(x,f(x,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [back_demod(19447),demod(20679(4))]. given #731 (F,wt=15): 21099 f(x,f(x,f(y,z))) = f(y,f(y,f(x,z))) # label(false). [back_demod(5116),demod(20722(7),20679(6),21080(5))]. given #732 (T,wt=15): 3149 f(f(x,f(f(x,y),z)),f(f(y,u),x)) = x. [para(35(a,1),8(a,1,2))]. given #733 (A,wt=21): 289 f(x,f(f(y,y),f(x,f(f(y,x),z)))) = f(x,f(f(y,x),z)). [para(18(a,1),210(a,1,1)),demod(4(3),4(5),4(9))]. given #734 (F,wt=15): 21149 f(f(f(c_0,x),y),z) = f(z,f(y,f(x,z))) # label(false). [para(20231(a,1),4(a,1)),flip(a)]. given #735 (F,wt=15): 21150 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,x))) # label(false). [para(4(a,1),20231(a,1,2,1))]. given #736 (F,wt=15): 21184 f(f(x,f(x,f(y,z))),f(f(x,y),z)) = z # label(false). [para(20231(a,2),805(a,1,2,1)),demod(4730(3,R),20679(4),6682(7,R),4660(7))]. given #737 (F,wt=15): 21202 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))) # label(false). [para(5665(a,1),20231(a,1,2)),flip(a)]. given #738 (T,wt=15): 3726 f(f(x,f(x,y)),f(f(z,f(y,y)),x)) = x. [para(3259(a,1),21(a,1,1))]. given #739 (A,wt=29): 291 f(f(x,f(y,f(z,y))),f(x,f(f(f(x,f(y,f(z,y))),f(f(x,f(z,z)),u)),v))) = x. [para(210(a,1),10(a,1,2,1)),demod(210(19))]. given #740 (F,wt=15): 21207 f(x,f(y,f(z,y))) = f(x,f(y,f(z,x))) # label(false). [para(6525(a,1),20231(a,1,2))]. given #741 (F,wt=15): 21254 f(x,f(y,f(z,z))) = f(x,f(y,f(z,x))) # label(false). [para(7076(a,1),20231(a,1,2))]. given #742 (F,wt=15): 21272 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label(false). [para(20231(a,2),7263(a,1,2,2)),demod(4730(3,R),20679(4),4(7),4660(7))]. given #743 (F,wt=15): 21321 f(f(x,f(y,z)),f(y,f(y,f(z,x)))) = x # label(false). [para(20231(a,2),15467(a,1,1,2)),demod(5599(4),20679(6))]. given #744 (T,wt=15): 4866 f(f(x,x),f(y,c_0)) = f(f(y,y),f(x,c_0)). [back_demod(3701),demod(4669(4,R),4669(8,R))]. given #745 (A,wt=25): 294 f(x,f(f(y,f(x,f(z,z))),f(x,f(u,f(z,u))))) = f(x,f(u,f(z,u))). [para(210(a,1),20(a,1,2)),demod(4(8))]. given #746 (F,wt=15): 21323 f(f(x,f(x,y)),z) = f(z,f(x,f(y,z))) # label(false). [para(20231(a,1),16052(a,2))]. given #747 (F,wt=15): 21325 f(f(x,f(y,x)),z) = f(z,f(x,f(y,z))) # label(false). [para(20231(a,1),16566(a,2))]. given #748 (F,wt=15): 21364 f(x,f(y,f(x,f(c_0,z)))) = f(x,f(y,z)) # label(false). [back_demod(15937),demod(21280(4)),flip(a)]. given #749 (F,wt=15): 21367 f(x,f(y,f(x,f(z,c_0)))) = f(x,f(y,z)) # label(false). [back_demod(15301),demod(21280(4)),flip(a)]. given #750 (T,wt=15): 4880 f(f(x,y),f(z,c_0)) = f(f(z,z),f(x,y)). [back_demod(3596),demod(4669(4,R))]. given #751 (A,wt=27): 306 f(f(x,f(y,y)),f(x,f(f(f(x,f(y,y)),f(f(x,f(z,f(y,z))),u)),v))) = x. [para(210(a,1),15(a,1,2,1)),demod(210(18))]. given #752 (F,wt=15): 21368 f(x,f(y,f(x,f(z,z)))) = f(x,f(y,z)) # label(false). [back_demod(15300),demod(21282(5)),flip(a)]. given #753 (F,wt=15): 21369 f(f(f(c_0,x),y),z) = f(z,f(y,f(z,x))) # label(false). [para(20232(a,1),4(a,1)),flip(a)]. given #754 (F,wt=15): 21370 f(x,f(f(y,c_0),z)) = f(x,f(z,f(x,y))) # label(false). [para(4(a,1),20232(a,1,2,1))]. given #755 (F,wt=15): 21371 f(x,f(y,f(c_0,z))) = f(x,f(y,f(x,z))) # label(false). [para(4(a,1),20232(a,1,2))]. given #756 (T,wt=15): 5454 f(f(x,f(y,f(z,x))),f(x,f(z,u))) = x. [para(41(a,1),8(a,1,2))]. given #757 (A,wt=29): 331 f(f(f(x,f(y,x)),z),f(z,f(f(f(f(x,f(y,x)),z),f(f(z,f(y,y)),u)),v))) = z. [para(216(a,1),10(a,1,2,1)),demod(216(19))]. given #758 (F,wt=15): 21413 f(f(x,f(x,f(y,z))),f(f(y,x),z)) = z # label(false). [para(20232(a,2),805(a,1,2,1)),demod(4730(3,R),20679(4),6682(7,R),4660(7))]. given #759 (F,wt=15): 21432 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))) # label(false). [para(5665(a,1),20232(a,1,2))]. given #760 (F,wt=15): 21435 f(x,f(y,f(z,y))) = f(x,f(y,f(x,z))) # label(false). [para(6525(a,1),20232(a,1,2))]. given #761 (F,wt=15): 21478 f(x,f(y,f(z,z))) = f(x,f(y,f(x,z))) # label(false). [para(7076(a,1),20232(a,1,2))]. given #762 (T,wt=15): 5711 f(f(x,f(x,y)),f(f(z,f(y,c_0)),x)) = x. [para(4659(a,1),44(a,1,1))]. given #763 (A,wt=51): 333 f(f(f(x,f(y,x)),z),f(f(y,y),f(f(f(x,f(y,x)),z),f(f(f(x,f(y,x)),f(z,u)),v)))) = f(f(f(x,f(y,x)),z),f(f(f(x,f(y,x)),f(z,u)),v)). [para(10(a,1),216(a,1,1)),demod(4(14))]. given #764 (F,wt=15): 21488 f(f(x,f(x,f(y,z))),f(z,f(y,x))) = z # label(false). [para(20232(a,2),7263(a,1,2,2)),demod(4730(3,R),20679(4),4(7),4660(7))]. given #765 (F,wt=15): 21519 f(f(x,f(y,z)),f(z,f(z,f(y,x)))) = x # label(false). [para(20232(a,2),15467(a,1,1,2)),demod(5606(4),20679(6))]. given #766 (F,wt=15): 21520 f(f(x,f(x,y)),z) = f(z,f(x,f(z,y))) # label(false). [para(20232(a,1),16052(a,2))]. given #767 (F,wt=15): 21521 f(f(x,f(y,x)),z) = f(z,f(x,f(z,y))) # label(false). [para(20232(a,1),16566(a,2))]. given #768 (T,wt=15): 5994 f(f(x,c_0),f(c_0,y)) = f(f(y,y),f(c_0,x)). [back_demod(5897),demod(5934(6,R),5934(9,R))]. given #769 (A,wt=27): 343 f(f(x,f(y,y)),f(x,f(f(f(x,f(y,y)),f(f(f(z,f(y,z)),x),u)),v))) = x. [para(216(a,1),15(a,1,2,1)),demod(216(18))]. given #770 (F,wt=15): 21543 f(x,f(y,f(y,f(z,x)))) = f(x,f(y,z)) # label(false). [para(17483(a,2),20232(a,2,2)),demod(20679(4),5595(9))]. given #771 (F,wt=15): 21568 f(f(x,f(y,y)),z) = f(z,f(f(y,z),x)) # label(false). [para(4(a,1),20233(a,1,1))]. given #772 (F,wt=15): 21569 f(f(f(x,x),y),z) = f(z,f(y,f(x,z))) # label(false). [para(4(a,1),20233(a,2,2))]. given #773 (F,wt=15): 21628 f(f(f(c_0,x),y),z) = f(z,f(f(x,z),y)) # label(false). [para(4730(a,2),20233(a,1,1,1))]. given #774 (T,wt=15): 6079 f(f(x,x),f(c_0,y)) = f(f(y,y),f(x,c_0)). [back_demod(4865),demod(5934(4,R))]. given #775 (A,wt=51): 345 f(f(x,f(y,f(z,y))),f(f(z,z),f(f(x,f(y,f(z,y))),f(f(f(y,f(z,y)),f(x,u)),v)))) = f(f(x,f(y,f(z,y))),f(f(f(y,f(z,y)),f(x,u)),v)). [para(15(a,1),216(a,1,1)),demod(4(14))]. given #776 (F,wt=15): 21629 f(f(f(x,c_0),y),z) = f(z,f(f(x,z),y)) # label(false). [para(4746(a,2),20233(a,1,1,1))]. given #777 (F,wt=15): 21635 f(f(x,f(y,y)),z) = f(z,f(x,f(y,z))) # label(false). [para(3723(a,1),20233(a,1,1)),demod(4(10),5(10),4(7),20259(7))]. given #778 (F,wt=15): 21665 f(f(x,f(y,c_0)),z) = f(z,f(x,f(y,z))) # label(false). [para(5605(a,1),20233(a,1,1)),demod(5(13),4(9),20261(9))]. given #779 (F,wt=15): 21668 f(f(x,f(y,c_0)),z) = f(z,f(f(y,z),x)) # label(false). [para(5936(a,1),20233(a,1,1))]. given #780 (T,wt=15): 6088 f(f(x,x),f(c_0,y)) = f(f(y,y),f(c_0,x)). [back_demod(4230),demod(5934(4,R),5934(8,R))]. given #781 (A,wt=53): 352 f(f(f(x,f(y,x)),f(z,u)),f(f(y,y),f(f(f(x,f(y,x)),f(z,u)),f(f(f(x,f(y,x)),z),v)))) = f(f(f(x,f(y,x)),f(z,u)),f(f(f(x,f(y,x)),z),v)). [para(17(a,1),216(a,1,1)),demod(4(15))]. given #782 (F,wt=15): 21681 f(f(x,f(c_0,y)),z) = f(z,f(x,f(y,z))) # label(false). [para(6871(a,1),20233(a,1,1)),demod(8(13),4(9),20264(9))]. given #783 (F,wt=15): 21684 f(f(x,f(c_0,y)),z) = f(z,f(f(y,z),x)) # label(false). [para(7291(a,1),20233(a,1,1))]. given #784 (F,wt=15): 21839 f(f(x,f(x,f(y,z))),f(y,f(x,z))) = y # label(false). [para(5665(a,1),178(a,2)),demod(4(7),20679(8),14591(8),7(6),4(3),20679(4),4(6),20679(7),4(7),20722(7)),flip(a)]. given #785 (F,wt=15): 21915 f(x,f(y,f(x,f(z,x)))) = f(x,f(y,z)) # label(false). [para(11094(a,1),20234(a,1,2)),demod(4730(7,R),4666(7))]. given #786 (T,wt=15): 6098 f(f(x,y),f(c_0,z)) = f(f(z,z),f(x,y)). [back_demod(4167),demod(5934(4,R))]. given #787 (A,wt=27): 363 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(24(a,1),9(a,1,2)),demod(4(5),4(8))]. given #788 (F,wt=15): 21917 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)) # label(false). [para(13717(a,1),20234(a,1,2)),demod(4730(7,R),4666(7))]. given #789 (F,wt=15): 22058 f(x,f(x,f(y,z))) = f(z,f(z,f(y,x))) # label(false). [para(20236(a,1),5665(a,1,1)),demod(20679(4),4(6),4666(6))]. given #790 (F,wt=15): 22059 f(x,f(c_0,f(y,z))) = f(z,f(z,f(y,x))) # label(false). [para(20236(a,1),6525(a,1,1)),demod(20679(4),4(6),4666(6),6682(6,R)),flip(a)]. given #791 (F,wt=15): 22629 f(x,f(c_0,f(y,z))) = f(y,f(y,f(z,x))) # label(false). [para(14642(a,1),1242(a,1,2)),demod(4(7),21543(7),4(8),22603(8),19122(6),4730(3,R))]. given #792 (T,wt=15): 6575 f(f(x,c_0),f(y,y)) = f(f(y,c_0),f(x,x)). [para(206(a,1),4667(a,2,2)),demod(5898(5),5651(8),206(9))]. given #793 (A,wt=23): 368 f(f(x,y),f(f(x,z),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)). [para(24(a,1),14(a,1,1))]. given #794 (F,wt=15): 22830 f(x,f(y,f(z,c_0))) = f(x,f(y,f(x,z))) # label(false). [para(4(a,1),20262(a,2,2,2))]. given #795 (F,wt=15): 23258 f(f(x,f(y,y)),z) = f(z,f(f(z,y),x)) # label(false). [para(4(a,1),20388(a,1,1))]. given #796 (F,wt=15): 23259 f(f(f(x,x),y),z) = f(z,f(y,f(z,x))) # label(false). [para(4(a,1),20388(a,2,2))]. given #797 (F,wt=15): 23290 f(f(f(c_0,x),y),z) = f(z,f(f(z,x),y)) # label(false). [para(4730(a,2),20388(a,1,1,1))]. given #798 (T,wt=15): 7072 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,x)). [para(5665(a,1),3043(a,2)),demod(4(11),6402(11),5651(9),6402(10))]. given #799 (A,wt=27): 373 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(24(a,1),20(a,1,1)),demod(4(7))]. given #800 (F,wt=15): 23291 f(f(f(x,c_0),y),z) = f(z,f(f(z,x),y)) # label(false). [para(4746(a,2),20388(a,1,1,1))]. given #801 (F,wt=15): 23295 f(f(x,f(y,c_0)),z) = f(z,f(x,f(z,y))) # label(false). [para(5605(a,1),20388(a,1,1)),demod(5(13),4(9),21367(9))]. given #802 (F,wt=15): 23296 f(f(x,f(y,c_0)),z) = f(z,f(f(z,y),x)) # label(false). [para(5936(a,1),20388(a,1,1))]. given #803 (F,wt=15): 23301 f(f(x,f(c_0,y)),z) = f(z,f(x,f(z,y))) # label(false). [para(6871(a,1),20388(a,1,1)),demod(8(13),4(9),21364(9))]. given #804 (T,wt=15): 7073 f(f(x,c_0),f(y,y)) = f(f(x,x),f(c_0,y)). [para(5665(a,1),3258(a,2)),demod(4(11),6402(11),5651(9),6402(10)),flip(a)]. given #805 (A,wt=23): 377 f(f(x,y),f(f(z,x),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)). [para(24(a,1),44(a,1,1))]. given #806 (F,wt=15): 23302 f(f(x,f(c_0,y)),z) = f(z,f(f(z,y),x)) # label(false). [para(7291(a,1),20388(a,1,1))]. given #807 (F,wt=15): 23396 f(x,f(y,f(c_0,f(z,x)))) = f(x,f(y,z)) # label(false). [para(8509(a,1),20389(a,1,2)),demod(21368(4),4730(5,R)),flip(a)]. given #808 (F,wt=15): 23398 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)) # label(false). [para(12004(a,1),20389(a,1,2)),demod(21368(4),4730(5,R)),flip(a)]. given #809 (F,wt=15): 23987 f(f(x,f(y,z)),f(y,f(y,f(x,z)))) = x # label(false). [para(20685(a,1),8(a,1,2))]. given #810 (T,wt=15): 7094 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(c_0,x)). [para(5665(a,1),4659(a,2,2)),demod(7075(10)),flip(a)]. given #811 (A,wt=29): 379 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(24(a,1),15(a,1,2,1)),demod(24(16))]. given #812 (F,wt=15): 23990 f(f(x,f(y,z)),f(y,f(c_0,f(x,z)))) = x # label(false). [para(20685(a,2),8(a,1,2))]. given #813 (F,wt=15): 23995 f(f(f(x,y),z),f(x,f(x,f(z,y)))) = z # label(false). [para(20685(a,1),13(a,1,2))]. given #814 (F,wt=15): 23997 f(f(f(x,y),z),f(x,f(c_0,f(z,y)))) = z # label(false). [para(20685(a,2),13(a,1,2))]. given #815 (F,wt=15): 24013 f(f(x,f(x,f(y,z))),f(f(x,z),y)) = y # label(false). [para(20685(a,1),37(a,1,1))]. given #816 (T,wt=15): 7697 f(f(f(x,c_0),y),f(c_0,f(x,z))) = f(x,z). [para(43(a,1),4660(a,1,2)),demod(4660(5)),flip(a)]. given #817 (A,wt=35): 388 f(f(f(x,f(y,x)),z),f(f(y,y),f(f(f(x,f(y,x)),z),f(z,u)))) = f(f(f(x,f(y,x)),z),f(z,u)). [para(24(a,1),216(a,1,1)),demod(4(10))]. given #818 (F,wt=15): 24015 f(f(x,f(c_0,f(y,z))),f(f(x,z),y)) = y # label(false). [para(20685(a,2),37(a,1,1))]. given #819 (F,wt=15): 24022 f(f(x,f(c_0,f(y,z))),f(y,f(x,z))) = y # label(false). [para(20685(a,2),3728(a,1,1)),demod(4730(7,R),4(9),5595(9))]. given #820 (F,wt=15): 24148 f(f(x,f(y,z)),f(z,f(z,f(x,y)))) = x # label(false). [para(20686(a,1),8(a,1,2))]. given #821 (F,wt=15): 24149 f(f(x,f(y,z)),f(y,f(c_0,f(z,x)))) = x # label(false). [para(20686(a,2),8(a,1,2))]. given #822 (T,wt=15): 7701 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [para(46(a,1),8(a,1,2))]. given #823 (A,wt=23): 391 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(f(y,x),v))))) = x. [para(19(a,1),8(a,1,1))]. given #824 (F,wt=15): 24150 f(f(f(x,y),z),f(y,f(y,f(z,x)))) = z # label(false). [para(20686(a,1),13(a,1,2))]. given #825 (F,wt=15): 24151 f(f(x,f(c_0,f(y,z))),f(f(x,y),z)) = z # label(false). [para(20686(a,2),13(a,1,2)),demod(4(7))]. given #826 (F,wt=15): 24152 f(f(x,f(x,f(y,z))),f(f(z,x),y)) = y # label(false). [para(20686(a,1),37(a,1,1))]. given #827 (F,wt=15): 24153 f(f(x,f(c_0,f(y,z))),f(z,f(x,y))) = z # label(false). [para(20686(a,2),3728(a,1,1)),demod(4730(7,R),4(9),5595(9))]. given #828 (T,wt=15): 8246 f(f(x,f(f(y,x),z)),f(x,f(u,y))) = x. [para(47(a,1),8(a,1,2))]. given #829 (A,wt=41): 394 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(19(a,1),9(a,1,2)),demod(4(8),4(12))]. given #830 (F,wt=15): 24163 f(f(x,f(x,f(y,z))),f(y,f(z,x))) = y # label(false). [para(20797(a,1),3728(a,1,1)),demod(4730(6,R),4(8),5595(8))]. given #831 (F,wt=15): 24166 f(f(f(x,c_0),y),z) = f(z,f(y,f(x,z))) # label(false). [para(4(a,1),21149(a,1,1,1))]. given #832 (F,wt=15): 24167 f(f(x,f(c_0,f(y,z))),f(f(y,x),z)) = z # label(false). [para(20685(a,2),21184(a,1,1))]. given #833 (F,wt=15): 24168 f(f(x,f(c_0,f(y,z))),f(f(z,x),y)) = y # label(false). [para(20686(a,2),21184(a,1,1))]. given #834 (T,wt=15): 8736 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,y))). [para(4667(a,2),3314(a,2,2)),flip(a)]. given #835 (A,wt=33): 397 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(19(a,1),14(a,1,1))]. given #836 (F,wt=15): 24169 f(f(x,f(c_0,f(y,z))),f(z,f(y,x))) = z # label(false). [para(20685(a,2),21272(a,1,1))]. given #837 (F,wt=15): 24170 f(f(x,f(c_0,f(y,z))),f(y,f(z,x))) = y # label(false). [para(20686(a,2),21272(a,1,1))]. given #838 (F,wt=15): 24171 f(f(x,f(y,z)),f(z,f(c_0,f(y,x)))) = x # label(false). [para(20685(a,2),21321(a,1,2))]. given #839 (F,wt=15): 24172 f(f(x,f(y,z)),f(z,f(c_0,f(x,y)))) = x # label(false). [para(20686(a,2),21321(a,1,2))]. given #840 (T,wt=15): 8739 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,z))). [para(4669(a,2),3314(a,2,2)),flip(a)]. given #841 (A,wt=41): 402 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(19(a,1),20(a,1,1)),demod(4(11))]. given #842 (F,wt=15): 24176 f(f(x,f(y,y)),z) = f(z,f(x,f(z,y))) # label(false). [para(8508(a,2),21364(a,2)),demod(23396(5)),flip(a)]. given #843 (F,wt=15): 24177 f(f(f(x,c_0),y),z) = f(z,f(y,f(z,x))) # label(false). [para(15223(a,2),21364(a,2)),demod(23398(5)),flip(a)]. given #844 (F,wt=15): 24201 f(f(f(x,y),z),f(y,f(c_0,f(z,x)))) = z # label(false). [para(22629(a,2),13(a,1,2))]. given #845 (F,wt=17): 3262 f(f(x,f(y,x)),f(f(y,y),f(x,z))) = f(y,y) # label(false). [para(3043(a,1),7(a,1,1))]. given #846 (T,wt=15): 8753 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,y))). [para(6525(a,2),3314(a,2,2)),flip(a)]. given #847 (A,wt=33): 404 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(19(a,1),44(a,1,1))]. given #848 (F,wt=17): 3263 f(f(x,f(y,y)),f(f(y,x),f(x,z))) = f(y,x) # label(false). [para(3043(a,2),7(a,1,1))]. given #849 (F,wt=17): 3274 f(f(x,f(y,x)),f(f(y,y),f(z,x))) = f(y,y) # label(false). [para(3043(a,1),13(a,1,1))]. given #850 (F,wt=17): 3275 f(f(x,f(y,y)),f(f(y,x),f(z,x))) = f(y,x) # label(false). [para(3043(a,2),13(a,1,1))]. given #851 (F,wt=17): 3278 f(f(x,f(y,x)),f(f(x,z),f(y,y))) = f(y,y) # label(false). [para(3043(a,1),14(a,1,1))]. given #852 (T,wt=15): 8754 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,z))). [para(6682(a,2),3314(a,2,2)),flip(a)]. given #853 (A,wt=41): 407 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(19(a,1),15(a,1,2,1)),demod(19(23))]. given #854 (F,wt=17): 3280 f(f(x,f(y,y)),f(f(x,z),f(y,x))) = f(y,x) # label(false). [para(3043(a,2),14(a,1,1))]. given #855 (F,wt=17): 3300 f(f(f(x,x),f(y,z)),f(z,f(x,z))) = f(x,x) # label(false). [para(3043(a,1),37(a,1,2))]. given #856 (F,wt=17): 3303 f(f(x,f(y,x)),f(f(z,x),f(y,y))) = f(y,y) # label(false). [para(3043(a,1),44(a,1,1))]. given #857 (F,wt=17): 3305 f(f(x,f(y,y)),f(f(z,x),f(y,x))) = f(y,x) # label(false). [para(3043(a,2),44(a,1,1))]. given #858 (T,wt=15): 9059 f(f(x,f(y,f(x,f(z,u)))),f(u,x)) = x. [para(49(a,1),8(a,1,2))]. given #859 (A,wt=53): 420 f(f(f(x,f(y,x)),f(z,u)),f(f(y,y),f(f(f(x,f(y,x)),f(z,u)),f(f(z,f(x,f(y,x))),v)))) = f(f(f(x,f(y,x)),f(z,u)),f(f(z,f(x,f(y,x))),v)). [para(19(a,1),216(a,1,1)),demod(4(15))]. given #860 (F,wt=17): 3559 f(f(f(x,x),y),f(f(x,y),f(y,z))) = f(x,y) # label(false). [para(3258(a,2),7(a,1,1))]. given #861 (F,wt=17): 3568 f(f(f(x,y),f(y,z)),f(f(x,x),y)) = f(x,y) # label(false). [para(3258(a,2),12(a,1,2))]. given #862 (F,wt=17): 3569 f(f(f(x,x),y),f(f(x,y),f(z,y))) = f(x,y) # label(false). [para(3258(a,2),13(a,1,1))]. given #863 (F,wt=17): 3572 f(f(f(x,x),y),f(f(y,z),f(x,y))) = f(x,y) # label(false). [para(3258(a,2),14(a,1,1))]. given #864 (T,wt=15): 9552 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x. [para(51(a,1),8(a,1,2))]. given #865 (A,wt=25): 440 f(x,f(f(f(f(y,y),x),z),f(x,f(u,f(y,u))))) = f(x,f(u,f(y,u))). [para(223(a,1),14(a,1,1))]. given #866 (F,wt=17): 3574 f(f(f(x,y),f(z,z)),f(x,f(z,x))) = f(z,z) # label(false). [para(3258(a,1),18(a,1,2))]. given #867 (F,wt=17): 3578 f(f(f(x,y),f(z,z)),f(y,f(z,y))) = f(z,z) # label(false). [para(3258(a,1),20(a,1,2))]. given #868 (F,wt=17): 3588 f(f(f(x,y),f(z,y)),f(f(x,x),y)) = f(x,y) # label(false). [para(3258(a,2),37(a,1,2))]. given #869 (F,wt=17): 3589 f(f(f(x,x),y),f(f(z,y),f(x,y))) = f(x,y) # label(false). [para(3258(a,2),44(a,1,1))]. given #870 (T,wt=15): 9958 f(f(f(x,c_0),y),z) = f(f(y,f(x,x)),z). [para(4667(a,2),3470(a,2,1)),flip(a)]. given #871 (A,wt=21): 449 f(x,f(f(y,y),f(x,f(z,f(y,x))))) = f(x,f(z,f(y,x))). [para(20(a,1),223(a,1,2)),demod(4(4),4(6),4(9))]. given #872 (F,wt=17): 3703 f(f(x,f(x,y)),f(f(y,y),f(x,z))) = f(y,y) # label(false). [para(3259(a,1),7(a,1,1))]. given #873 (F,wt=17): 3704 f(f(x,f(y,y)),f(f(x,y),f(x,z))) = f(x,y) # label(false). [para(3259(a,2),7(a,1,1))]. given #874 (F,wt=17): 3712 f(f(x,f(x,y)),f(f(y,y),f(z,x))) = f(y,y) # label(false). [para(3259(a,1),13(a,1,1))]. given #875 (F,wt=17): 3713 f(f(x,f(y,y)),f(f(x,y),f(z,x))) = f(x,y) # label(false). [para(3259(a,2),13(a,1,1))]. given #876 (T,wt=15): 9959 f(f(x,f(y,c_0)),z) = f(f(x,f(y,y)),z). [para(4669(a,2),3470(a,2,1)),flip(a)]. given #877 (A,wt=25): 453 f(x,f(f(y,f(f(z,z),x)),f(x,f(u,f(z,u))))) = f(x,f(u,f(z,u))). [para(223(a,1),44(a,1,1))]. given #878 (F,wt=17): 3715 f(f(x,f(x,y)),f(f(x,z),f(y,y))) = f(y,y) # label(false). [para(3259(a,1),14(a,1,1))]. given #879 (F,wt=17): 3717 f(f(x,f(y,y)),f(f(x,z),f(x,y))) = f(x,y) # label(false). [para(3259(a,2),14(a,1,1))]. given #880 (F,wt=17): 3729 f(f(f(x,x),f(y,z)),f(z,f(z,x))) = f(x,x) # label(false). [para(3259(a,1),37(a,1,2))]. given #881 (F,wt=17): 3731 f(f(x,f(x,y)),f(f(z,x),f(y,y))) = f(y,y) # label(false). [para(3259(a,1),44(a,1,1))]. given #882 (T,wt=15): 9974 f(f(f(c_0,x),y),z) = f(f(y,f(x,x)),z). [para(6525(a,2),3470(a,2,1)),flip(a)]. given #883 (A,wt=29): 456 f(f(x,f(y,f(z,y))),f(x,f(f(f(x,f(y,f(z,y))),f(f(f(z,z),x),u)),v))) = x. [para(223(a,1),15(a,1,2,1)),demod(223(19))]. given #884 (F,wt=17): 3733 f(f(x,f(y,y)),f(f(z,x),f(x,y))) = f(x,y) # label(false). [para(3259(a,2),44(a,1,1))]. given #885 (F,wt=17): 3902 f(f(f(x,x),y),f(f(y,x),f(y,z))) = f(y,x) # label(false). [para(3286(a,1),27(a,1,2,1)),demod(3286(9))]. given #886 (F,wt=17): 3927 f(f(f(x,x),y),f(f(y,z),f(y,x))) = f(y,x) # label(false). [para(3286(a,1),48(a,1,2,2)),demod(3286(9))]. given #887 (F,wt=17): 3932 f(f(f(x,x),y),f(f(y,x),f(z,y))) = f(y,x) # label(false). [para(3286(a,1),50(a,1,2,1)),demod(3286(9))]. given #888 (T,wt=15): 9975 f(f(x,f(c_0,y)),z) = f(f(x,f(y,y)),z). [para(6682(a,2),3470(a,2,1)),flip(a)]. given #889 (A,wt=25): 498 f(f(x,f(y,f(z,y))),f(x,f(f(f(x,f(y,f(z,y))),f(z,z)),u))) = x. [para(226(a,1),17(a,1,2,1)),demod(226(17))]. given #890 (F,wt=17): 3944 f(f(f(x,x),y),f(f(z,y),f(y,x))) = f(y,x) # label(false). [para(3286(a,1),56(a,1,2,2)),demod(3286(9))]. given #891 (F,wt=17): 4155 f(f(f(x,y),f(x,z)),f(f(y,y),x)) = f(x,y) # label(false). [para(3557(a,2),12(a,1,2))]. given #892 (F,wt=17): 4162 f(f(f(x,y),f(z,x)),f(f(y,y),x)) = f(x,y) # label(false). [para(3557(a,2),37(a,1,2))]. given #893 (F,wt=17): 4882 f(f(f(x,y),f(z,c_0)),f(y,f(z,z))) = f(z,z) # label(false). [back_demod(3585),demod(4669(4,R))]. given #894 (T,wt=15): 10118 f(f(x,f(y,f(x,z))),f(f(z,u),x)) = x. [para(54(a,1),8(a,1,2))]. given #895 (A,wt=25): 506 f(f(x,f(y,f(z,y))),f(x,f(f(f(z,z),f(x,f(y,f(z,y)))),u))) = x. [para(226(a,1),19(a,1,2,1)),demod(226(17))]. given #896 (F,wt=17): 4883 f(f(f(x,y),f(z,c_0)),f(x,f(z,z))) = f(z,z) # label(false). [back_demod(3566),demod(4669(4,R))]. given #897 (F,wt=17): 4907 f(f(x,f(y,y)),f(f(z,x),f(y,c_0))) = f(y,y) # label(false). [back_demod(3304),demod(4669(6,R))]. given #898 (F,wt=17): 4908 f(f(f(x,x),y),f(f(z,y),f(x,c_0))) = f(x,x) # label(false). [back_demod(3296),demod(4669(6,R))]. given #899 (F,wt=17): 4909 f(f(f(x,y),f(z,c_0)),f(f(z,z),y)) = f(z,z) # label(false). [back_demod(3289),demod(4669(4,R))]. given #900 (T,wt=15): 10645 f(f(x,f(y,f(z,x))),f(x,f(u,z))) = x. [para(55(a,1),8(a,1,2))]. given #901 (A,wt=23): 530 f(f(x,f(y,y)),f(x,f(f(f(x,f(y,y)),f(z,f(y,z))),u))) = x. [para(229(a,1),17(a,1,2,1)),demod(229(16))]. given #902 (F,wt=17): 4910 f(f(f(x,y),f(z,c_0)),f(f(z,z),x)) = f(z,z) # label(false). [back_demod(3282),demod(4669(4,R))]. given #903 (F,wt=17): 4911 f(f(x,f(y,y)),f(f(x,z),f(y,c_0))) = f(y,y) # label(false). [back_demod(3279),demod(4669(6,R))]. given #904 (F,wt=17): 4912 f(f(f(x,x),y),f(f(y,z),f(x,c_0))) = f(x,x) # label(false). [back_demod(3269),demod(4669(6,R))]. given #905 (F,wt=17): 5142 f(f(x,y),f(c_0,f(y,f(z,x)))) = f(y,f(x,y)) # label(false). [back_demod(3302),demod(4730(6,R))]. given #906 (T,wt=15): 11270 f(x,f(f(y,c_0),z)) = f(x,f(f(y,y),z)). [para(4667(a,2),3594(a,2,2)),flip(a)]. given #907 (A,wt=23): 539 f(f(x,f(y,y)),f(x,f(f(f(z,f(y,z)),f(x,f(y,y))),u))) = x. [para(229(a,1),19(a,1,2,1)),demod(229(16))]. given #908 (F,wt=17): 5144 f(f(x,y),f(c_0,f(f(z,y),x))) = f(x,f(x,y)) # label(false). [back_demod(3294),demod(4730(6,R))]. given #909 (F,wt=17): 5145 f(f(x,y),f(c_0,f(f(y,z),x))) = f(x,f(x,y)) # label(false). [back_demod(3285),demod(4730(6,R))]. given #910 (F,wt=17): 5147 f(f(x,y),f(c_0,f(y,f(x,z)))) = f(y,f(x,y)) # label(false). [back_demod(3273),demod(4730(6,R))]. given #911 (F,wt=17): 5318 f(f(x,y),f(y,f(y,f(z,x)))) = f(c_0,f(x,y)) # label(false). [back_demod(217),demod(4730(8,R))]. given #912 (T,wt=15): 11273 f(x,f(f(y,y),z)) = f(x,f(z,f(y,c_0))). [para(4669(a,2),3594(a,2,2))]. given #913 (A,wt=29): 561 f(f(f(x,f(y,x)),z),f(z,f(f(f(f(x,f(y,x)),z),f(f(f(y,y),z),u)),v))) = z. [para(232(a,1),10(a,1,2,1)),demod(232(19))]. given #914 (F,wt=17): 5321 f(f(x,y),f(x,f(x,f(z,y)))) = f(c_0,f(x,y)) # label(false). [back_demod(211),demod(4730(8,R))]. given #915 (F,wt=17): 5322 f(f(x,y),f(y,f(y,f(x,z)))) = f(c_0,f(x,y)) # label(false). [back_demod(209),demod(4730(8,R))]. given #916 (F,wt=17): 5323 f(f(x,y),f(x,f(x,f(y,z)))) = f(c_0,f(x,y)) # label(false). [back_demod(207),demod(4730(8,R))]. given #917 (F,wt=17): 5618 f(f(x,f(y,c_0)),f(f(x,y),f(x,z))) = f(x,y) # label(false). [para(4657(a,1),27(a,1,2,1)),demod(4657(11))]. given #918 (T,wt=15): 11281 f(x,f(f(c_0,y),z)) = f(x,f(f(y,y),z)). [para(6525(a,2),3594(a,2,2)),flip(a)]. given #919 (A,wt=43): 564 f(f(f(x,x),y),f(f(z,f(x,z)),f(f(f(x,x),y),f(f(f(x,x),f(y,u)),v)))) = f(f(f(x,x),y),f(f(f(x,x),f(y,u)),v)). [para(10(a,1),232(a,1,2)),demod(4(13))]. given #920 (F,wt=17): 5627 f(f(x,f(y,c_0)),f(f(x,z),f(x,y))) = f(x,y) # label(false). [para(4657(a,1),48(a,1,2,2)),demod(4657(11))]. given #921 (F,wt=17): 5630 f(f(x,f(y,c_0)),f(f(x,y),f(z,x))) = f(x,y) # label(false). [para(4657(a,1),50(a,1,2,1)),demod(4657(11))]. given #922 (F,wt=17): 5637 f(f(x,f(y,c_0)),f(f(z,x),f(x,y))) = f(x,y) # label(false). [para(4657(a,1),56(a,1,2,2)),demod(4657(11))]. given #923 (F,wt=17): 5666 f(f(x,f(x,y)),f(f(y,c_0),f(x,z))) = f(y,c_0) # label(false). [para(4659(a,1),5(a,1,1))]. given #924 (T,wt=15): 11282 f(x,f(f(y,y),z)) = f(x,f(z,f(c_0,y))). [para(6682(a,2),3594(a,2,2))]. given #925 (A,wt=43): 575 f(f(x,f(y,y)),f(f(z,f(y,z)),f(f(x,f(y,y)),f(f(f(y,y),f(x,u)),v)))) = f(f(x,f(y,y)),f(f(f(y,y),f(x,u)),v)). [para(15(a,1),232(a,1,2)),demod(4(13))]. given #926 (F,wt=17): 5668 f(f(x,y),f(c_0,f(x,f(y,z)))) = f(x,f(x,y)) # label(false). [para(5(a,1),4659(a,2,2)),demod(4(4),4(6),4(8))]. given #927 (F,wt=17): 5671 f(f(f(x,c_0),y),f(f(y,x),f(y,z))) = f(y,x) # label(false). [para(4659(a,2),7(a,1,1))]. given #928 (F,wt=17): 5673 f(f(x,f(x,y)),f(f(y,c_0),f(z,x))) = f(y,c_0) # label(false). [para(4659(a,1),8(a,1,1))]. given #929 (F,wt=17): 5676 f(f(x,y),f(c_0,f(x,f(z,y)))) = f(x,f(x,y)) # label(false). [para(8(a,1),4659(a,2,2)),demod(4(4),4(6),4(8))]. given #930 (T,wt=15): 11465 f(f(f(x,c_0),y),z) = f(f(f(x,x),y),z). [para(4667(a,2),3698(a,2,1)),flip(a)]. given #931 (A,wt=25): 577 f(f(f(x,f(y,x)),z),f(z,f(f(f(y,y),f(f(x,f(y,x)),z)),u))) = z. [para(232(a,1),17(a,1,2,1)),demod(4(8),232(17))]. given #932 (F,wt=17): 5680 f(f(x,f(x,y)),f(f(x,z),f(y,c_0))) = f(y,c_0) # label(false). [para(4659(a,1),9(a,1,1))]. given #933 (F,wt=17): 5685 f(f(f(x,y),f(x,z)),f(f(y,c_0),x)) = f(x,y) # label(false). [para(4659(a,2),12(a,1,2))]. given #934 (F,wt=17): 5688 f(f(f(x,c_0),y),f(f(y,x),f(z,y))) = f(y,x) # label(false). [para(4659(a,2),13(a,1,1))]. given #935 (F,wt=17): 5692 f(f(f(x,c_0),y),f(f(y,z),f(y,x))) = f(y,x) # label(false). [para(4659(a,2),14(a,1,1))]. given #936 (T,wt=15): 11466 f(f(f(x,x),y),z) = f(f(y,f(x,c_0)),z). [para(4669(a,2),3698(a,2,1))]. given #937 (A,wt=45): 580 f(f(f(x,x),f(y,z)),f(f(u,f(x,u)),f(f(f(x,x),f(y,z)),f(f(f(x,x),y),v)))) = f(f(f(x,x),f(y,z)),f(f(f(x,x),y),v)). [para(17(a,1),232(a,1,2)),demod(4(14))]. given #938 (F,wt=17): 5693 f(f(x,y),f(c_0,f(f(x,z),y))) = f(y,f(x,y)) # label(false). [para(14(a,1),4659(a,2,2)),demod(4(4),4(6),4(8))]. given #939 (F,wt=17): 5700 f(f(x,f(x,y)),f(f(z,x),f(y,c_0))) = f(y,c_0) # label(false). [para(4659(a,1),20(a,1,2)),demod(4(7))]. given #940 (F,wt=17): 5710 f(f(f(x,y),f(z,x)),f(f(y,c_0),x)) = f(x,y) # label(false). [para(4659(a,2),37(a,1,2))]. given #941 (F,wt=17): 5712 f(f(f(x,c_0),y),f(f(z,y),f(y,x))) = f(y,x) # label(false). [para(4659(a,2),44(a,1,1))]. given #942 (T,wt=15): 11467 f(f(f(c_0,x),y),z) = f(f(f(x,x),y),z). [para(6525(a,2),3698(a,2,1)),flip(a)]. given #943 (A,wt=45): 595 f(f(f(x,x),f(y,z)),f(f(u,f(x,u)),f(f(f(x,x),f(y,z)),f(f(y,f(x,x)),v)))) = f(f(f(x,x),f(y,z)),f(f(y,f(x,x)),v)). [para(19(a,1),232(a,1,2)),demod(4(14))]. given #944 (F,wt=17): 5714 f(f(x,y),f(c_0,f(f(z,x),y))) = f(y,f(x,y)) # label(false). [para(44(a,1),4659(a,2,2)),demod(4(4),4(6),4(8))]. given #945 (F,wt=17): 6100 f(f(f(x,y),f(c_0,z)),f(y,f(z,z))) = f(z,z) # label(false). [back_demod(4160),demod(5934(4,R))]. given #946 (F,wt=17): 6101 f(f(f(x,y),f(c_0,z)),f(x,f(z,z))) = f(z,z) # label(false). [back_demod(4153),demod(5934(4,R))]. given #947 (F,wt=17): 6159 f(f(x,f(y,y)),f(f(z,x),f(c_0,y))) = f(y,y) # label(false). [back_demod(3732),demod(5934(6,R))]. given #948 (T,wt=15): 11468 f(f(f(x,x),y),z) = f(f(y,f(c_0,x)),z). [para(6682(a,2),3698(a,2,1))]. given #949 (A,wt=27): 607 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(27(a,1),9(a,1,2)),demod(4(5),4(8))]. given #950 (F,wt=17): 6160 f(f(f(x,x),y),f(f(z,y),f(c_0,x))) = f(x,x) # label(false). [back_demod(3727),demod(5934(6,R))]. given #951 (F,wt=17): 6161 f(f(f(x,y),f(c_0,z)),f(f(z,z),y)) = f(z,z) # label(false). [back_demod(3721),demod(5934(4,R))]. given #952 (F,wt=17): 6162 f(f(f(x,y),f(c_0,z)),f(f(z,z),x)) = f(z,z) # label(false). [back_demod(3718),demod(5934(4,R))]. given #953 (F,wt=17): 6163 f(f(x,f(y,y)),f(f(x,z),f(c_0,y))) = f(y,y) # label(false). [back_demod(3716),demod(5934(6,R))]. given #954 (T,wt=15): 11742 f(f(f(c_0,x),y),f(c_0,f(x,z))) = f(x,z). [para(58(a,1),4660(a,1,2)),demod(4660(5)),flip(a)]. given #955 (A,wt=23): 609 f(f(x,y),f(f(y,z),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)). [para(27(a,1),14(a,1,1))]. given #956 (F,wt=17): 6164 f(f(f(x,x),y),f(f(y,z),f(c_0,x))) = f(x,x) # label(false). [back_demod(3709),demod(5934(6,R))]. given #957 (F,wt=17): 6331 f(f(f(x,c_0),f(y,z)),f(y,f(y,x))) = f(x,c_0) # label(false). [para(4665(a,1),12(a,1,2))]. given #958 (F,wt=17): 6338 f(f(f(x,c_0),f(y,z)),f(z,f(z,x))) = f(x,c_0) # label(false). [para(4665(a,1),37(a,1,2))]. given #959 (F,wt=17): 6526 f(f(x,f(y,x)),f(f(y,c_0),f(x,z))) = f(y,c_0) # label(false). [para(4667(a,1),5(a,1,1))]. given #960 (T,wt=15): 11981 f(f(x,f(f(y,x),z)),f(f(y,u),x)) = x. [para(59(a,1),8(a,1,2))]. given #961 (A,wt=23): 612 f(f(f(x,y),f(f(x,f(y,z)),u)),f(f(x,y),f(x,v))) = f(x,y). [para(10(a,1),27(a,1,2,1)),demod(10(15))]. given #962 (F,wt=17): 6528 f(f(f(x,c_0),y),f(f(x,y),f(y,z))) = f(x,y) # label(false). [para(4667(a,2),7(a,1,1))]. given #963 (F,wt=17): 6529 f(f(x,f(y,x)),f(f(y,c_0),f(z,x))) = f(y,c_0) # label(false). [para(4667(a,1),8(a,1,1))]. given #964 (F,wt=17): 6532 f(f(x,f(y,x)),f(f(x,z),f(y,c_0))) = f(y,c_0) # label(false). [para(4667(a,1),9(a,1,1))]. given #965 (F,wt=17): 6535 f(f(f(x,y),f(y,z)),f(f(x,c_0),y)) = f(x,y) # label(false). [para(4667(a,2),12(a,1,2))]. given #966 (T,wt=15): 12978 f(f(f(c_0,x),y),f(c_0,f(z,x))) = f(z,x). [para(61(a,1),4660(a,1,2)),demod(4660(5)),flip(a)]. given #967 (A,wt=27): 613 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(27(a,1),20(a,1,1)),demod(4(7))]. given #968 (F,wt=17): 6537 f(f(f(x,c_0),y),f(f(x,y),f(z,y))) = f(x,y) # label(false). [para(4667(a,2),13(a,1,1))]. given #969 (F,wt=17): 6540 f(f(f(x,c_0),y),f(f(y,z),f(x,y))) = f(x,y) # label(false). [para(4667(a,2),14(a,1,1))]. given #970 (F,wt=17): 6541 f(f(f(x,y),f(z,c_0)),f(x,f(z,x))) = f(z,c_0) # label(false). [para(4667(a,1),18(a,1,2))]. given #971 (F,wt=17): 6548 f(f(f(x,y),f(z,c_0)),f(y,f(z,y))) = f(z,c_0) # label(false). [para(4667(a,1),20(a,1,2))]. given #972 (T,wt=15): 13714 f(f(x,f(y,f(z,x))),f(f(z,u),x)) = x. [para(64(a,1),8(a,1,2))]. given #973 (A,wt=23): 614 f(f(x,y),f(f(z,y),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)). [para(27(a,1),44(a,1,1))]. given #974 (F,wt=17): 6552 f(f(x,f(y,x)),f(f(z,x),f(y,c_0))) = f(y,c_0) # label(false). [para(4667(a,1),21(a,1,1))]. given #975 (F,wt=17): 6557 f(f(f(x,y),f(z,y)),f(f(x,c_0),y)) = f(x,y) # label(false). [para(4667(a,2),37(a,1,2))]. given #976 (F,wt=17): 6559 f(f(f(x,c_0),y),f(f(z,y),f(x,y))) = f(x,y) # label(false). [para(4667(a,2),44(a,1,1))]. given #977 (F,wt=17): 6683 f(f(x,f(y,c_0)),f(f(y,x),f(x,z))) = f(y,x) # label(false). [para(4669(a,2),7(a,1,1))]. given #978 (T,wt=15): 13810 f(f(f(x,c_0),y),f(c_0,f(z,x))) = f(z,x). [para(65(a,1),4660(a,1,2)),demod(4660(5)),flip(a)]. given #979 (A,wt=29): 616 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(27(a,1),15(a,1,2,1)),demod(27(16))]. given #980 (F,wt=17): 6686 f(f(f(x,c_0),f(y,z)),f(y,f(x,y))) = f(x,c_0) # label(false). [para(4669(a,1),12(a,1,2))]. given #981 (F,wt=17): 6687 f(f(x,f(y,c_0)),f(f(y,x),f(z,x))) = f(y,x) # label(false). [para(4669(a,2),13(a,1,1))]. given #982 (F,wt=17): 6689 f(f(x,f(y,c_0)),f(f(x,z),f(y,x))) = f(y,x) # label(false). [para(4669(a,2),14(a,1,1))]. given #983 (F,wt=17): 6697 f(f(f(x,c_0),f(y,z)),f(z,f(x,z))) = f(x,c_0) # label(false). [para(4669(a,1),37(a,1,2))]. given #984 (T,wt=15): 14007 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(y,y)). [para(4671(a,1),3043(a,1)),demod(4669(9,R)),flip(a)]. given #985 (A,wt=23): 617 f(f(f(x,y),f(f(y,f(x,z)),u)),f(f(x,y),f(y,v))) = f(x,y). [para(15(a,1),27(a,1,2,1)),demod(15(15))]. given #986 (F,wt=17): 6699 f(f(x,f(y,c_0)),f(f(z,x),f(y,x))) = f(y,x) # label(false). [para(4669(a,2),44(a,1,1))]. given #987 (F,wt=17): 6884 f(f(x,f(c_0,y)),f(f(x,y),f(x,z))) = f(x,y) # label(false). [para(5595(a,1),27(a,1,2,1)),demod(5595(11))]. given #988 (F,wt=17): 6896 f(f(x,f(c_0,y)),f(f(x,z),f(x,y))) = f(x,y) # label(false). [para(5595(a,1),48(a,1,2,2)),demod(5595(11))]. given #989 (F,wt=17): 6900 f(f(x,f(c_0,y)),f(f(x,y),f(z,x))) = f(x,y) # label(false). [para(5595(a,1),50(a,1,2,1)),demod(5595(11))]. given #990 (T,wt=15): 14008 f(f(x,c_0),f(y,y)) = f(f(x,x),f(y,c_0)). [para(4671(a,2),3043(a,1)),demod(4669(8,R))]. given #991 (A,wt=27): 619 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(17(a,1),27(a,1,2,1)),demod(17(16))]. given #992 (F,wt=17): 6907 f(f(x,f(c_0,y)),f(f(z,x),f(x,y))) = f(x,y) # label(false). [para(5595(a,1),56(a,1,2,2)),demod(5595(11))].