============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11678 was started by mccune on cleo.thornwood, Sat Aug 12 21:22:12 2006 The command was "/home/mccune/bin/prover9 -f dist-both.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dist-both.in assign(order,kbo). set(lex_order_vars). assign(max_weight,50). list(weights). weight(x = y) = (weight(x) + weight(y)) + depth(x = y). end_of_list. formulas(sos). f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). f(f(x,w,y),w,z) = f(x,w,f(y,w,z)) # label(associativity). end_of_list. set(restrict_denials). formulas(sos). f(f(A,B,C),D,E) != f(f(A,D,E),f(B,D,E),f(C,D,E)) | f(f(A,B,C),D,E) != f(A,f(B,D,E),f(C,D,E)) # answer(dist_both). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(x,x,y) = x # label(majority). [assumption]. f(x,y,z) = f(z,x,y) # label(2a). [assumption]. f(x,y,z) = f(x,z,y) # label(2b). [assumption]. f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. f(f(A,B,C),D,E) != f(f(A,D,E),f(B,D,E),f(C,D,E)) | f(f(A,B,C),D,E) != f(A,f(B,D,E),f(C,D,E)) # answer(dist_both). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Function symbol KB weights: A=1. B=1. C=1. D=1. E=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ A, B, C, D, E, f ]). Skipping inverse_order, because term ordering is KBO. 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, 2). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 f(x,x,y) = x # label(majority). [assumption]. 2 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 3 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. 5 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(4),rewrite(2(2),2(2),2(3,R),3(3)),rewrite(2(1,R),3(1),3(3),2(4,R),3(4))]. 7 f(f(A,D,E),f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) | f(A,f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) # answer(dist_both). [copy(6),rewrite(2(7),2(7),2(28),2(28)),flip(a),flip(b)]. end_of_list. formulas(demodulators). 1 f(x,x,y) = x # label(majority). [assumption]. 2 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. % (lex-dep) 3 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 1 f(x,x,y) = x # label(majority). [assumption]. given #2 (I,wt=10): 2 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. given #3 (I,wt=10): 3 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. given #4 (I,wt=17): 5 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(4),rewrite(2(2),2(2),2(3,R),3(3)),rewrite(2(1,R),3(1),3(3),2(4,R),3(4))]. given #5 (I,wt=0): 7 f(f(A,D,E),f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) | f(A,f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) # answer(dist_both). [copy(6),rewrite(2(7),2(7),2(28),2(28)),flip(a),flip(b)]. given #6 (A,wt=7): 8 f(x,y,y) = y. [para(2(a,1),1(a,1))]. given #7 (F,wt=14): 12 f(x,y,f(x,z,y)) = f(x,z,y). [para(8(a,1),5(a,1,3)),flip(a)]. given #8 (F,wt=14): 13 f(x,y,f(x,y,z)) = f(x,y,z). [para(8(a,1),5(a,1)),rewrite(3(3),12(3)),flip(a)]. given #9 (T,wt=17): 9 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(5(a,1),2(a,2)),rewrite(3(2),2(3,R),3(3)),flip(a)]. given #10 (T,wt=17): 10 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(2(a,1),5(a,1,3)),rewrite(2(1,R),3(1))]. given #11 (A,wt=24): 11 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(5(a,1),5(a,1,3))]. given #12 (F,wt=17): 17 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(9(a,1),2(a,2)),rewrite(3(2),2(3,R),3(3))]. given #13 (F,wt=17): 18 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(2(a,1),9(a,1)),rewrite(2(2),2(2),3(3))]. given #14 (T,wt=17): 24 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)). [para(2(a,1),10(a,1)),rewrite(2(2),2(2),3(3))]. given #15 (T,wt=21): 14 f(x,y,f(x,z,f(x,u,y))) = f(x,z,f(x,u,y)). [para(12(a,1),5(a,1,3)),flip(a)]. given #16 (A,wt=21): 15 f(x,y,f(x,z,f(x,y,u))) = f(x,z,f(x,y,u)). [para(12(a,1),5(a,2,3)),rewrite(3(1),3(4))]. given #17 (F,wt=21): 22 f(x,y,f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(9(a,2),13(a,1,3))]. given #18 (F,wt=21): 66 f(x,y,f(z,x,f(x,y,u))) = f(z,x,f(x,y,u)). [para(12(a,1),17(a,1,3)),rewrite(2(1),2(3),2(5,R),3(5)),flip(a)]. given #19 (T,wt=21): 115 f(x,y,f(z,y,f(x,y,u))) = f(z,y,f(x,y,u)). [para(66(a,1),2(a,2)),rewrite(2(1,R),3(1),3(3),2(4,R),3(4))]. given #20 (T,wt=24): 19 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))). [para(9(a,2),5(a,1,3))]. given #21 (A,wt=24): 21 f(x,f(y,z,u),f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(9(a,2),12(a,1,3))]. given #22 (F,wt=21): 125 f(x,y,f(z,u,f(x,z,u))) = f(x,y,f(x,z,u)). [para(8(a,1),19(a,1,3)),rewrite(3(4),88(6)),flip(a)]. given #23 (F,wt=14): 198 f(x,y,f(z,x,y)) = f(z,x,y). [para(125(a,1),8(a,1)),rewrite(3(4),125(4),8(3)),flip(a)]. given #24 (T,wt=21): 208 f(x,y,f(z,x,f(x,u,y))) = f(z,x,f(x,u,y)). [para(198(a,1),17(a,1,3)),rewrite(2(1),2(3),2(5,R),3(5)),flip(a)]. given #25 (T,wt=24): 23 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para(9(a,1),9(a,1,3)),rewrite(2(1,R),3(1),2(6,R),3(6))]. given #26 (A,wt=24): 25 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,z,u))). [para(10(a,2),5(a,1,3))]. given #27 (F,wt=24): 26 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,v,z))). [para(10(a,1),5(a,2,3)),flip(a)]. given #28 (F,wt=24): 31 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,z,f(x,y,u))). [para(9(a,2),10(a,1,3)),flip(a)]. given #29 (T,wt=20): 362 f(x,f(y,x,z),f(y,x,u)) = f(y,x,f(x,u,z)). [para(18(a,2),31(a,2)),rewrite(8(2),3(2)),flip(a)]. given #30 (T,wt=24): 33 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,y,v))). [para(11(a,1),2(a,2)),rewrite(3(3),2(5,R),3(5)),flip(a)]. given #31 (A,wt=24): 34 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(x,y,v))). [para(11(a,2),2(a,2)),rewrite(3(3),2(4,R),3(4))]. given #32 (F,wt=21): 496 f(x,y,f(x,z,f(u,x,y))) = f(u,x,f(x,z,y)). [para(12(a,1),34(a,1,3)),flip(a)]. given #33 (F,wt=20): 567 f(x,f(y,x,z),f(x,u,z)) = f(y,x,f(x,u,z)). [para(496(a,1),10(a,1)),rewrite(3(4)),flip(a)]. given #34 (T,wt=20): 595 f(x,f(y,x,z),f(x,z,u)) = f(y,x,f(x,z,u)). [para(567(a,1),2(a,2)),rewrite(3(2),2(3),3(4))]. given #35 (T,wt=20): 596 f(x,f(x,y,z),f(u,x,z)) = f(u,x,f(x,y,z)). [para(567(a,1),3(a,1)),flip(a)]. given #36 (A,wt=31): 35 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,u,f(x,y,f(x,v,f(x,z,w)))). [para(11(a,1),5(a,1,3))]. given #37 (F,wt=20): 631 f(x,f(x,y,z),f(u,x,y)) = f(u,x,f(x,y,z)). [para(595(a,1),3(a,1)),flip(a)]. given #38 (F,wt=18): 778 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para(631(a,1),33(a,1,3)),rewrite(2(4,R),8(4),2(3,R),8(3),2(5),3(5),2(6,R),3(6),432(6),3(3),50(6),3(4),13(4),13(5)),flip(a)]. given #39 (T,wt=17): 808 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(18(a,2),778(a,2)),rewrite(3(3),801(5))]. given #40 (T,wt=17): 840 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(808(a,1),2(a,2)),rewrite(3(2),2(3)),flip(a)]. given #41 (A,wt=24): 36 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,z,f(x,y,v))). [para(11(a,1),5(a,1))]. given #42 (F,wt=17): 864 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(840(a,1),2(a,2)),rewrite(3(2),2(3))]. given #43 (F,wt=17): 889 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(840(a,2),31(a,2)),rewrite(3(2),387(3),778(3)),flip(a)]. given #44 (T,wt=17): 892 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(31(a,2),840(a,2)),rewrite(2(2),387(3),778(3),2(2,R),3(2),2(3,R),3(3)),flip(a)]. given #45 (T,wt=17): 997 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(2(a,1),889(a,1,2)),rewrite(2(2),2(4))]. given #46 (A,wt=31): 37 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,y,f(x,z,f(x,u,w)))). [para(11(a,2),5(a,1,3))]. given #47 (F,wt=17): 999 f(x,f(y,z,x),f(y,z,u)) = f(y,z,x). [para(889(a,1),3(a,1)),flip(a)]. given #48 (F,wt=17): 1000 f(x,f(x,y,z),f(y,z,u)) = f(x,y,z). [para(889(a,1),3(a,2)),rewrite(2(1),2(4))]. given #49 (T,wt=17): 1068 f(x,f(y,x,z),f(y,z,u)) = f(y,x,z). [para(892(a,1),3(a,1)),flip(a)]. given #50 (T,wt=17): 1099 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(997(a,1),2(a,2)),rewrite(2(2),2(2),2(3),2(4),2(4))]. given #51 (A,wt=24): 38 f(x,y,f(x,z,f(x,u,v))) = f(x,y,f(x,u,f(x,z,v))). [para(11(a,2),5(a,1))]. given #52 (F,wt=18): 784 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [back_rewrite(259),rewrite(2(1,R),3(1),2(2,R),3(2),778(3),2(3,R),3(3),2(4,R),3(4)),flip(a)]. given #53 (F,wt=18): 786 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [back_rewrite(140),rewrite(2(1,R),3(1),2(2,R),3(2),2(5,R),3(5),2(6,R),3(6),784(6))]. given #54 (T,wt=18): 787 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [back_rewrite(156),rewrite(2(2,R),3(2),786(3),2(4,R),3(4)),flip(a)]. given #55 (T,wt=18): 791 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [back_rewrite(234),rewrite(3(1),2(5,R),3(5),784(6))]. given #56 (A,wt=28): 43 f(x,y,f(x,z,f(x,u,f(x,v,y)))) = f(x,z,f(x,u,f(x,v,y))). [para(12(a,1),11(a,1,3,3)),flip(a)]. given #57 (F,wt=18): 793 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [back_rewrite(256),rewrite(787(4),387(3),778(3)),flip(a)]. given #58 (F,wt=17): 1661 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(840(a,2),793(a,2)),rewrite(3(3),1650(5)),flip(a)]. given #59 (T,wt=17): 1668 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(1661(a,1),2(a,2)),rewrite(3(2),2(3))]. given #60 (T,wt=17): 1754 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(1668(a,1),793(a,2)),rewrite(3(3),1662(5))]. given #61 (A,wt=28): 44 f(x,y,f(x,z,f(x,u,f(x,y,v)))) = f(x,y,f(x,z,f(x,u,v))). [para(11(a,2),13(a,1,3))]. given #62 (F,wt=18): 795 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [back_rewrite(381),rewrite(791(4)),flip(a)]. given #63 (F,wt=18): 877 f(x,y,f(z,u,f(x,z,y))) = f(x,z,y). [para(840(a,2),19(a,2,3)),rewrite(2(2,R),3(2),786(3),3(2)),flip(a)]. given #64 (T,wt=18): 957 f(x,y,f(z,u,f(x,u,y))) = f(x,u,y). [para(13(a,1),864(a,1,3)),rewrite(8(3),632(5),115(4)),flip(a)]. given #65 (T,wt=18): 979 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u). [para(864(a,1),23(a,2,3)),rewrite(3(1),3(4),2(5,R),3(5),877(6))]. given #66 (A,wt=31): 45 f(x,y,f(z,u,f(x,z,f(z,v,w)))) = f(x,z,f(x,y,f(z,v,f(z,u,w)))). [para(11(a,1),9(a,1,3)),rewrite(2(2,R),3(2),2(8,R),3(8))]. given #67 (F,wt=18): 998 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(2(a,2),889(a,1,2)),rewrite(2(2),3(2),387(3),2(4),3(4))]. given #68 (F,wt=18): 1538 f(x,y,f(z,u,f(z,x,y))) = f(z,x,y). [para(2(a,1),791(a,1)),rewrite(2(1),2(3),2(3),2(4))]. given #69 (T,wt=18): 1848 f(x,y,f(z,u,f(u,x,y))) = f(u,x,y). [para(2(a,1),957(a,1)),rewrite(2(1,R),3(1),2(3),2(3),2(4,R),3(4))]. given #70 (T,wt=20): 1002 f(f(x,y,z),f(x,z,u),f(x,y,z)) = f(x,y,z). [para(12(a,1),889(a,1,3)),rewrite(12(6))]. given #71 (A,wt=31): 46 f(x,y,f(z,u,f(z,v,f(x,z,w)))) = f(x,z,f(x,y,f(z,u,f(z,v,w)))). [para(11(a,2),9(a,1,3)),rewrite(2(1,R),3(1),2(8,R),3(8))]. given #72 (F,wt=20): 1003 f(f(x,y,z),f(x,y,u),f(x,y,z)) = f(x,y,z). [para(13(a,1),889(a,1,3)),rewrite(13(6))]. given #73 (F,wt=20): 1026 f(f(x,y,z),f(y,z,u),f(x,y,z)) = f(x,y,z). [para(198(a,1),889(a,1,3)),rewrite(198(6))]. given #74 (T,wt=21): 881 f(x,f(y,x,z),f(z,u,f(y,x,z))) = f(y,x,z). [para(198(a,1),840(a,1,3)),rewrite(2(3,R),8(3),3(4)),flip(a)]. given #75 (T,wt=21): 976 f(x,f(y,x,z),f(u,z,f(y,x,z))) = f(y,x,z). [para(198(a,1),864(a,1,3)),rewrite(8(3)),flip(a)]. given #76 (A,wt=31): 47 f(x,y,f(x,z,f(u,v,f(x,u,w)))) = f(x,u,f(x,y,f(x,z,f(u,v,w)))). [para(9(a,2),11(a,1,3,3))]. given #77 (F,wt=21): 978 f(x,y,f(x,f(x,y,z),f(u,y,z))) = f(x,y,z). [para(864(a,1),23(a,1)),rewrite(13(3),8(3)),flip(a)]. given #78 (F,wt=21): 1005 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(9(a,1),889(a,1,2)),rewrite(2(3),2(5))]. given #79 (T,wt=21): 1014 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(18(a,1),889(a,1,2)),rewrite(2(3),2(5))]. given #80 (T,wt=21): 1294 f(x,f(x,y,z),f(y,u,f(y,z,v))) = f(x,y,z). [para(5(a,1),999(a,1,3)),rewrite(2(1),2(5))]. given #81 (A,wt=31): 48 f(x,y,f(x,z,f(u,v,f(x,u,w)))) = f(x,z,f(x,u,f(x,y,f(u,v,w)))). [para(9(a,2),11(a,2,3,3)),flip(a)]. given #82 (F,wt=21): 1677 f(x,f(y,z,x),f(z,u,f(y,z,x))) = f(y,z,x). [para(198(a,1),1661(a,1,3)),rewrite(2(3,R),8(3),3(4)),flip(a)]. given #83 (F,wt=21): 1708 f(x,f(y,z,x),f(u,y,f(y,z,x))) = f(y,z,x). [para(12(a,1),1668(a,1,3)),rewrite(8(3)),flip(a)]. given #84 (T,wt=21): 1709 f(x,f(y,x,z),f(u,y,f(y,x,z))) = f(y,x,z). [para(13(a,1),1668(a,1,3)),rewrite(8(3)),flip(a)]. given #85 (T,wt=21): 1720 f(x,f(y,z,x),f(u,z,f(y,z,x))) = f(y,z,x). [para(198(a,1),1668(a,1,3)),rewrite(8(3)),flip(a)]. given #86 (A,wt=24): 50 f(x,f(x,y,z),f(x,u,v)) = f(x,y,f(x,u,f(x,v,z))). [para(11(a,1),10(a,1)),flip(a)]. given #87 (F,wt=21): 2687 f(x,y,f(x,f(x,y,z),f(y,u,z))) = f(x,y,z). [para(2(a,1),978(a,1,3)),rewrite(2(1,R),3(1),2(3,R))]. given #88 (F,wt=21): 2719 f(x,f(y,z,f(z,u,v)),f(z,u,x)) = f(z,u,x). [para(1005(a,1),2(a,2)),rewrite(2(3),2(3),2(4),2(5),2(5))]. given #89 (T,wt=21): 2744 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(1005(a,1),14(a,1,3)),rewrite(3(1),13(2),2(2,R),3(2),2(3,R),3(3),3(4)),flip(a)]. given #90 (T,wt=21): 2745 f(x,f(y,z,f(u,z,v)),f(x,u,z)) = f(x,u,z). [para(1005(a,1),14(a,2)),rewrite(2(1,R),3(1),3(3),15(5),3(5))]. given #91 (A,wt=31): 51 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,z,f(x,y,f(x,v,f(x,u,w)))). [para(11(a,2),10(a,1,3)),rewrite(50(8))]. given #92 (F,wt=21): 2851 f(x,f(y,z,f(z,u,v)),f(z,v,x)) = f(z,v,x). [para(1014(a,1),2(a,2)),rewrite(2(3),2(3),2(4),2(5),2(5))]. given #93 (F,wt=21): 2921 f(x,f(y,z,x),f(y,u,f(y,z,v))) = f(y,z,x). [para(2(a,1),1294(a,1)),rewrite(2(3),2(3),2(4,R),2(5),2(5))]. given #94 (T,wt=21): 3411 f(x,f(y,z,f(y,u,v)),f(y,u,x)) = f(y,u,x). [para(2719(a,1),2(a,1)),rewrite(2(4,R),3(4),2(5,R)),flip(a)]. given #95 (T,wt=22): 788 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [back_rewrite(541),rewrite(2(3,R),3(3),2(7,R),3(7),784(8))]. given #96 (A,wt=24): 52 f(x,y,f(x,z,f(x,u,v))) = f(x,y,f(x,v,f(x,z,u))). [para(11(a,2),10(a,2)),rewrite(3(2),3(4)),flip(a)]. given #97 (F,wt=18): 3859 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(997(a,1),788(a,2)),rewrite(3(6),2(7,R),3(7),3828(9),3(2))]. given #98 (F,wt=18): 3971 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y). [para(2(a,1),3859(a,1)),rewrite(2(1),2(3),2(3),3(4))]. given #99 (T,wt=21): 3834 f(x,y,f(z,f(x,z,u),f(y,z,v))) = f(x,y,z). [para(18(a,2),788(a,1,3))]. given #100 (T,wt=21): 4034 f(x,y,f(z,f(z,y,u),f(x,z,v))) = f(x,z,y). [para(3834(a,1),2(a,2)),rewrite(2(1,R),3(1),3(4),2(5),2(5))]. given #101 (A,wt=31): 53 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,w,f(x,y,f(x,z,f(x,u,v)))). [para(10(a,2),11(a,1,3,3))]. given #102 (F,wt=21): 4035 f(x,y,f(z,f(x,z,u),f(z,y,v))) = f(x,z,y). [para(3834(a,1),3(a,2)),rewrite(2(2,R),3(2),3(4),3(5))]. given #103 (F,wt=21): 4036 f(x,y,f(z,f(y,z,u),f(x,z,v))) = f(x,y,z). [para(3(a,1),3834(a,1,3))]. given #104 (T,wt=22): 789 f(x,y,f(z,u,f(x,z,f(y,z,v)))) = f(x,y,z). [back_rewrite(479),rewrite(2(1,R),3(1),2(7,R),3(7),784(8))]. given #105 (T,wt=22): 798 f(x,y,f(x,z,f(y,u,f(y,z,v)))) = f(x,y,z). [para(5(a,1),778(a,1,3,3))]. given #106 (A,wt=31): 54 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,u,f(x,y,f(x,w,f(x,z,v)))). [para(10(a,1),11(a,2,3,3))]. given #107 (F,wt=22): 800 f(x,y,f(x,z,f(z,u,f(y,z,v)))) = f(x,y,z). [para(9(a,2),778(a,1,3,3))]. given #108 (F,wt=22): 1008 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [para(10(a,2),889(a,1,2)),rewrite(2(3),387(4),2(5))]. given #109 (T,wt=22): 1462 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z). [para(5(a,1),784(a,1,3,3)),rewrite(2(3,R),3(3),3(5))]. given #110 (T,wt=22): 1512 f(x,y,f(z,u,f(y,z,f(x,z,v)))) = f(x,y,z). [para(11(a,1),787(a,1,3)),rewrite(2(1,R),3(1),2(2,R),3(2),2(5),2(5))]. given #111 (A,wt=24): 55 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,v,f(x,y,z))). [para(10(a,1),11(a,2,3))]. given #112 (F,wt=22): 1523 f(x,y,f(z,u,f(y,u,f(x,u,v)))) = f(x,y,u). [para(34(a,2),787(a,1,3)),rewrite(2(1,R),3(1),2(2,R),3(2),2(5),2(5))]. given #113 (F,wt=22): 1803 f(x,y,f(z,u,f(x,u,f(y,u,v)))) = f(x,y,u). [para(34(a,2),795(a,1,3)),rewrite(2(1,R),3(1),2(2,R),3(2),2(5),2(5))]. given #114 (T,wt=22): 1898 f(x,y,f(z,y,f(x,u,f(x,z,v)))) = f(x,z,y). [para(45(a,1),17(a,2)),rewrite(2(2,R),3(2),2(3,R),3(3),786(4),2(4,R),3(4),2(5,R),3(5)),flip(a)]. given #115 (T,wt=22): 1979 f(x,y,f(z,x,f(y,u,f(z,y,v)))) = f(z,x,y). [para(45(a,1),840(a,2)),rewrite(2(3),387(4),778(4),2(2,R),3(2),2(4,R),3(4)),flip(a)]. given #116 (A,wt=38): 56 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,v,f(x,y,f(x,z,f(x,w,f(x,u,v6))))). [para(11(a,1),11(a,1,3,3))]. given #117 (F,wt=21): 5122 f(x,f(y,z,f(u,y,v)),f(u,x,y)) = f(u,x,y). [para(1979(a,1),808(a,1)),flip(a)]. given #118 (F,wt=21): 5243 f(x,f(y,x,z),f(z,u,f(y,z,v))) = f(y,x,z). [para(5122(a,1),3(a,1)),flip(a)]. given #119 (T,wt=22): 2177 f(x,y,f(z,y,f(x,u,f(z,x,v)))) = f(z,x,y). [para(46(a,1),17(a,1)),rewrite(778(4)),flip(a)]. given #120 (T,wt=22): 2189 f(x,y,f(z,x,f(z,u,f(z,y,v)))) = f(z,x,y). [para(46(a,1),115(a,1,3)),rewrite(2(3,R),3(3),2(4,R),3(4),784(4),13(2),2(2,R),3(2),2(5,R),3(5)),flip(a)]. given #121 (A,wt=31): 57 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,y,f(x,u,f(x,z,w)))). [para(11(a,1),11(a,1,3))]. given #122 (F,wt=21): 5415 f(x,f(y,z,f(y,u,v)),f(y,x,u)) = f(y,x,u). [para(2189(a,1),808(a,1)),flip(a)]. given #123 (F,wt=21): 5617 f(x,f(y,x,z),f(y,u,f(y,z,v))) = f(y,x,z). [para(5415(a,1),3(a,1)),flip(a)]. given #124 (T,wt=22): 2728 f(x,y,f(x,z,f(z,u,f(z,y,v)))) = f(x,z,y). [para(1005(a,1),10(a,1)),rewrite(2(3,R),3(3),3(4)),flip(a)]. given #125 (T,wt=22): 2730 f(x,y,f(x,z,f(u,z,f(y,z,v)))) = f(x,y,z). [para(10(a,1),1005(a,1)),rewrite(2(1,R),3(1),3(3),3(5))]. given #126 (A,wt=38): 58 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,w,f(x,y,f(x,z,f(x,u,f(x,v,v6))))). [para(11(a,2),11(a,1,3,3))]. given #127 (F,wt=22): 3470 f(x,y,f(z,y,f(z,u,f(z,x,v)))) = f(z,x,y). [para(2719(a,1),1661(a,1)),rewrite(2(3,R),3(3)),flip(a)]. given #128 (F,wt=22): 3495 f(x,y,f(x,z,f(y,u,f(z,y,v)))) = f(x,z,y). [para(2744(a,1),10(a,1)),rewrite(3(4)),flip(a)]. given #129 (T,wt=22): 3882 f(x,y,f(x,z,f(u,y,f(y,z,v)))) = f(x,y,z). [para(1005(a,1),788(a,2)),rewrite(3(8),2(9,R),3(9),3828(11),3(3))]. given #130 (T,wt=22): 3885 f(x,y,f(x,z,f(u,y,f(y,v,z)))) = f(x,y,z). [para(1014(a,1),788(a,2)),rewrite(3(8),2(9,R),3(9),3828(11),3(3))]. given #131 (A,wt=38): 59 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,u,f(x,y,f(x,w,f(x,z,f(x,v,v6))))). [para(11(a,1),11(a,2,3,3))]. given #132 (F,wt=22): 4132 f(x,y,f(z,u,f(x,z,f(z,y,v)))) = f(x,z,y). [para(2744(a,1),3834(a,2)),rewrite(2(1,R),3(1),3(3),3(4),3(5),2(6,R),3(6),3(8),2(9),4068(11),3(5))]. given #133 (F,wt=22): 4407 f(x,y,f(z,u,f(z,y,f(x,z,v)))) = f(x,z,y). [para(789(a,1),2(a,2)),rewrite(2(2,R),3(2),3(4),2(5),2(5))]. given #134 (T,wt=22): 4408 f(x,y,f(z,u,f(z,x,f(z,y,v)))) = f(z,x,y). [para(2(a,1),789(a,1)),rewrite(2(1,R),3(1),2(2,R),3(2),2(4),2(4),2(5))]. given #135 (T,wt=22): 4439 f(x,y,f(z,u,f(z,v,f(x,y,z)))) = f(x,y,z). [para(840(a,2),789(a,1,3,3))]. given #136 (A,wt=31): 60 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,u,f(x,v,f(x,y,f(x,z,w)))). [para(11(a,1),11(a,2,3))]. given #137 (F,wt=21): 6052 f(x,y,f(z,f(x,y,z),f(z,u,v))) = f(x,y,z). [para(10(a,1),4439(a,1,3))]. given #138 (F,wt=21): 6190 f(x,y,f(z,f(x,z,y),f(z,u,v))) = f(x,z,y). [para(6052(a,1),2(a,2)),rewrite(2(1),2(1),3(4),2(5),2(5))]. given #139 (T,wt=22): 4972 f(x,y,f(z,u,f(x,u,f(u,y,v)))) = f(x,u,y). [para(1523(a,1),2(a,2)),rewrite(2(1,R),3(1),3(4),2(5),2(5))]. given #140 (T,wt=22): 4973 f(x,y,f(z,u,f(u,x,f(u,y,v)))) = f(u,x,y). [para(2(a,1),1523(a,1)),rewrite(2(1,R),3(1),2(2,R),3(2),2(4),3(4),2(5),3(5))]. given #141 (A,wt=38): 61 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,u,f(x,y,f(x,v,f(x,w,f(x,z,v6))))). [para(11(a,2),11(a,2,3,3))]. given #142 (F,wt=22): 4974 f(x,y,f(z,u,f(u,y,f(x,u,v)))) = f(x,u,y). [para(1523(a,1),3(a,2)),rewrite(2(2,R),3(2),3(4),3(5))]. given #143 (F,wt=22): 4995 f(x,y,f(z,u,f(u,v,f(x,y,u)))) = f(x,y,u). [para(840(a,2),1523(a,1,3,3)),rewrite(2(1,R),3(1))]. given #144 (T,wt=22): 5045 f(x,y,f(x,z,f(u,y,f(z,y,v)))) = f(x,z,y). [para(1803(a,1),786(a,2)),rewrite(3(7),1502(9))]. given #145 (T,wt=21): 6497 f(x,y,f(y,z,f(u,x,y))) = f(y,z,f(u,x,y)). [para(1099(a,1),5045(a,1,3)),rewrite(2(2),2(2),2(4),2(4),2(6,R),3(6),198(6),2(5),2(5),2(7),3(7),12(7))]. given #146 (A,wt=31): 62 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,z,f(x,y,f(x,u,w)))). [para(11(a,2),11(a,2,3)),flip(a)]. given #147 (F,wt=18): 6530 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(1099(a,1),6497(a,2)),rewrite(2(1),2(2),2(2),22(4),3(2),2(4),2(4))]. given #148 (F,wt=22): 5161 f(x,y,f(z,y,f(u,x,f(z,x,v)))) = f(z,x,y). [para(1803(a,1),1979(a,2)),rewrite(2(2,R),3(2),2(5,R),3(5),2(8,R),3(8),3(10),2(11,R),3(11),2(12,R),3(12),5109(13),2(5),2(5))]. given #149 (T,wt=22): 5363 f(x,y,f(z,y,f(z,u,f(x,z,v)))) = f(x,z,y). [para(2177(a,1),17(a,1)),flip(a)]. given #150 (T,wt=22): 5690 f(x,y,f(x,z,f(u,z,f(z,y,v)))) = f(x,z,y). [para(2730(a,1),14(a,1,3)),rewrite(2(1,R),3(1),3(3),1005(4),2(2,R),3(2)),flip(a)]. given #151 (A,wt=24): 63 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,u,v))). [para(5(a,1),17(a,1,3)),rewrite(2(1,R),3(1),2(6,R),3(6))]. given #152 (F,wt=17): 6743 f(x,f(x,y,z),f(u,y,z)) = f(x,y,z). [para(997(a,1),63(a,2,3)),rewrite(2(3),2(3),3859(4),997(3),2(4,R)),flip(a)]. given #153 (F,wt=17): 6893 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x). [para(2(a,1),6743(a,1)),rewrite(2(2),2(2),2(3,R),2(4),2(4))]. given #154 (T,wt=20): 6752 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)). [para(1099(a,1),63(a,2,3)),rewrite(2(3),3(3),877(5),2(4),2(5,R)),flip(a)]. given #155 (T,wt=21): 6800 f(x,f(x,y,z),f(u,y,f(y,z,v))) = f(x,y,z). [para(1005(a,1),63(a,2,3)),rewrite(2(5),2(5),3882(6),1005(4),2(5,R)),flip(a)]. given #156 (A,wt=24): 64 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,u,v))). [para(5(a,1),17(a,2,3)),rewrite(2(2,R),3(2),2(6,R),3(6)),flip(a)]. given #157 (F,wt=21): 6803 f(x,f(x,y,z),f(u,y,f(y,v,z))) = f(x,y,z). [para(1014(a,1),63(a,2,3)),rewrite(2(5),2(5),3885(6),1014(4),2(5,R)),flip(a)]. given #158 (F,wt=17): 7111 f(x,f(x,y,z),f(y,u,z)) = f(x,y,z). [para(6803(a,1),3971(a,1,3)),rewrite(387(3),998(3)),flip(a)]. given #159 (T,wt=17): 7129 f(x,f(y,z,x),f(y,u,z)) = f(y,z,x). [para(2(a,1),7111(a,1)),rewrite(2(2),2(2),2(3,R),2(4),2(4))]. given #160 (T,wt=21): 6982 f(x,f(y,z,x),f(u,y,f(y,z,v))) = f(y,z,x). [para(2(a,1),6800(a,1)),rewrite(2(3),2(3),2(4,R),2(5),2(5))]. given #161 (A,wt=24): 65 f(x,f(y,z,u),f(y,z,f(x,z,u))) = f(x,z,f(y,z,u)). [para(17(a,1),12(a,1,3))]. given #162 (F,wt=21): 7027 f(x,y,f(y,f(x,y,z),f(u,x,z))) = f(x,y,z). [para(1668(a,1),64(a,1)),rewrite(2(3,R),3(3),13(3),8(3),2(3,R),3(3)),flip(a)]. given #163 (F,wt=21): 7077 f(x,f(y,z,x),f(u,y,f(y,v,z))) = f(y,z,x). [para(2(a,1),6803(a,1)),rewrite(2(3),2(3),2(4,R),2(5),2(5))]. given #164 (T,wt=21): 7349 f(x,y,f(y,f(x,y,z),f(x,u,z))) = f(x,y,z). [para(2(a,1),7027(a,1,3)),rewrite(2(1,R),3(1),2(3,R))]. given #165 (T,wt=22): 6043 f(x,y,f(z,u,f(z,v,f(x,z,y)))) = f(x,z,y). [para(4439(a,1),2(a,2)),rewrite(2(1),2(1),3(4),2(5),2(5))]. given #166 (A,wt=24): 67 f(x,y,f(z,u,f(y,u,v))) = f(y,u,f(x,y,f(z,u,v))). [para(9(a,1),17(a,1,3)),rewrite(2(1,R),3(1),2(6,R),3(6))]. given #167 (F,wt=20): 7539 f(x,f(y,z,x),f(z,x,u)) = f(y,x,f(z,x,u)). [para(889(a,1),67(a,2,3)),rewrite(2(3),3(3),115(4),12(4),2(4),2(5,R)),flip(a)]. given #168 (F,wt=20): 7547 f(x,f(y,x,z),f(u,y,x)) = f(x,z,f(u,y,x)). [para(67(a,1),1099(a,1)),rewrite(2(3),2(3),2(6),3(6),6918(6),2(5,R),3(5),12(5),2(5),2(5),6497(6))]. given #169 (T,wt=20): 7548 f(x,f(y,z,x),f(u,z,x)) = f(y,x,f(u,z,x)). [para(1099(a,1),67(a,2,3)),rewrite(2(3),3(3),957(5),2(4),2(5,R)),flip(a)]. given #170 (T,wt=22): 6044 f(x,y,f(z,u,f(z,v,f(z,x,y)))) = f(z,x,y). [para(2(a,1),4439(a,1)),rewrite(2(1),2(4),2(4),2(5))]. given #171 (A,wt=24): 68 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(y,z,f(x,z,u))). [para(17(a,1),10(a,1,3)),flip(a)]. given #172 (F,wt=20): 8100 f(x,f(y,x,z),f(y,u,x)) = f(y,x,f(u,x,z)). [para(840(a,2),68(a,2)),rewrite(8(2),3(2)),flip(a)]. given #173 (F,wt=21): 8293 f(x,y,f(z,f(x,y,z),f(x,z,u))) = f(x,y,z). [para(68(a,2),6044(a,1,3)),rewrite(2(1),2(1),2(2),2(5),2(5))]. given #174 (T,wt=22): 6448 f(x,y,f(z,u,f(u,v,f(x,u,y)))) = f(x,u,y). [para(4995(a,1),2(a,2)),rewrite(2(1),2(1),3(4),2(5),2(5))]. given #175 (T,wt=22): 6449 f(x,y,f(z,u,f(u,v,f(u,x,y)))) = f(u,x,y). [para(2(a,1),4995(a,1)),rewrite(2(1),2(4),2(4),2(5))]. given #176 (A,wt=24): 69 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,v,u))). [para(10(a,1),17(a,2,3)),rewrite(2(2,R),3(2),2(6,R),3(6)),flip(a)]. given #177 (F,wt=22): 6535 f(x,y,f(y,z,f(u,z,f(x,z,v)))) = f(x,y,z). [para(2719(a,1),6497(a,2)),rewrite(2(1,R),3(1),2(3),2(3),22(5),3(3),2(5),2(5))]. given #178 (F,wt=22): 6657 f(x,y,f(z,x,f(u,y,f(z,y,v)))) = f(z,x,y). [para(2(a,1),5161(a,1)),rewrite(2(4),3(4),3(5))]. given #179 (T,wt=22): 7535 f(x,y,f(z,u,f(z,y,f(z,x,v)))) = f(z,x,y). [para(36(a,1),67(a,2,3)),rewrite(778(4)),flip(a)]. given #180 (T,wt=22): 8305 f(x,y,f(z,u,f(x,u,f(u,v,y)))) = f(x,u,y). [back_rewrite(4123),rewrite(8192(11))]. given #181 (A,wt=31): 70 f(x,y,f(x,z,f(u,v,f(x,v,w)))) = f(x,v,f(x,y,f(x,z,f(u,v,w)))). [para(17(a,1),11(a,1,3,3))]. given #182 (F,wt=22): 8575 f(x,y,f(z,u,f(u,x,f(u,v,y)))) = f(u,x,y). [para(2(a,1),8305(a,1)),rewrite(2(2,R),3(2),2(4),2(4),2(5,R),3(5))]. given #183 (F,wt=24): 75 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,v,u))). [para(18(a,2),5(a,2,3)),flip(a)]. given #184 (T,wt=24): 76 f(x,f(y,z,u),f(y,u,f(x,y,z))) = f(x,y,f(y,z,u)). [para(18(a,2),12(a,1,3))]. given #185 (T,wt=24): 80 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,v,f(x,y,u))). [para(18(a,2),17(a,2,3)),rewrite(2(2,R),3(2),2(6,R),3(6))]. given #186 (A,wt=31): 71 f(x,y,f(z,u,f(y,z,f(z,v,w)))) = f(y,z,f(x,y,f(z,v,f(z,u,w)))). [para(11(a,1),17(a,1,3)),rewrite(2(2,R),3(2),2(8,R),3(8))]. given #187 (F,wt=24): 83 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,u,z))). [para(5(a,1),24(a,2,3)),rewrite(50(3),3(1),3(4))]. given #188 (F,wt=24): 84 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,y,z))). [para(10(a,1),24(a,2,3)),rewrite(50(3),3(1),3(4))]. given #189 (T,wt=24): 85 f(x,y,f(x,z,f(x,u,v))) = f(x,y,f(x,v,f(x,u,z))). [para(24(a,1),11(a,1)),rewrite(50(3),3(1),3(4))]. given #190 (T,wt=24): 90 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(x,z,f(z,u,v))). [para(9(a,2),14(a,2,3)),rewrite(14(5)),flip(a)]. given #191 (A,wt=31): 72 f(x,y,f(z,u,f(z,v,f(y,z,w)))) = f(y,z,f(x,y,f(z,u,f(z,v,w)))). [para(11(a,2),17(a,1,3)),rewrite(2(1,R),3(1),2(8,R),3(8))]. given #192 (F,wt=21): 9289 f(x,f(y,z,f(u,y,v)),f(u,y,x)) = f(u,y,x). [para(72(a,1),808(a,1)),rewrite(2(3,R),3(3),778(4),2(4)),flip(a)]. given #193 (F,wt=21): 9325 f(x,f(y,z,x),f(z,u,f(y,z,v))) = f(y,z,x). [para(9289(a,1),3(a,1)),flip(a)]. given #194 (T,wt=24): 98 f(x,y,f(z,u,f(x,u,v))) = f(x,y,f(x,u,f(z,u,v))). [para(17(a,1),14(a,2,3)),rewrite(14(5)),flip(a)]. given #195 (T,wt=24): 100 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(x,z,f(z,v,u))). [para(18(a,2),14(a,2,3)),rewrite(14(5)),flip(a)]. given #196 (A,wt=31): 73 f(x,y,f(z,u,f(z,x,f(z,v,w)))) = f(z,x,f(x,y,f(z,v,f(z,u,w)))). [para(11(a,1),17(a,2,3)),rewrite(2(3,R),3(3),2(8,R),3(8)),flip(a)]. given #197 (F,wt=24): 101 f(x,y,f(y,z,f(y,u,v))) = f(x,y,f(y,u,f(y,z,v))). [para(5(a,1),22(a,2,3)),rewrite(22(4))]. given #198 (F,wt=24): 104 f(x,y,f(z,u,f(y,z,v))) = f(x,y,f(y,z,f(z,u,v))). [para(9(a,2),22(a,2,3)),rewrite(22(4)),flip(a)]. given #199 (T,wt=24): 106 f(x,y,f(y,z,f(y,u,v))) = f(x,y,f(y,v,f(y,z,u))). [para(10(a,1),22(a,2,3)),rewrite(22(4))]. given #200 (T,wt=24): 113 f(x,y,f(z,u,f(y,z,v))) = f(x,y,f(y,z,f(z,v,u))). [para(18(a,2),22(a,2,3)),rewrite(22(4)),flip(a)]. given #201 (A,wt=31): 74 f(x,y,f(z,u,f(z,v,f(z,x,w)))) = f(z,x,f(x,y,f(z,u,f(z,v,w)))). [para(11(a,2),17(a,2,3)),rewrite(2(3,R),3(3),2(8,R),3(8)),flip(a)]. given #202 (F,wt=24): 118 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,x,f(z,u,v))). [para(5(a,1),115(a,1,3,3)),rewrite(2(3,R),3(3),96(4),2(6,R),3(6))]. given #203 (F,wt=18): 9972 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z). [para(1668(a,1),118(a,1)),rewrite(2(3,R),3(3),13(3),8(3),2(3,R),3(3),362(5),3(3)),flip(a)]. given #204 (T,wt=18): 9979 f(x,y,f(x,z,f(u,z,y))) = f(x,z,y). [para(9972(a,1),496(a,2)),rewrite(2(3,R),3(3),14(5),2(4,R),3(4))]. given #205 (T,wt=24): 123 f(x,y,f(z,u,f(z,y,v))) = f(z,y,f(x,y,f(z,u,v))). [para(19(a,1),2(a,2)),rewrite(2(1,R),3(1),3(3),2(5,R),3(5),2(6,R),3(6))]. given #206 (A,wt=31): 78 f(x,y,f(x,z,f(u,v,f(x,u,w)))) = f(x,z,f(x,u,f(x,y,f(u,w,v)))). [para(18(a,2),11(a,2,3,3)),flip(a)]. given #207 (F,wt=24): 126 f(x,f(y,z,u),f(y,z,f(y,x,u))) = f(y,z,f(y,x,u)). [para(8(a,1),19(a,1)),rewrite(2(1,R),3(1),2(3,R),3(3),3(6),2(7,R),3(7),96(7)),flip(a)]. given #208 (F,wt=21): 10159 f(x,y,f(z,x,f(u,x,y))) = f(z,x,f(u,x,y)). [para(198(a,1),126(a,1,2)),rewrite(2(3,R),3(3),877(5),2(4,R),3(4)),flip(a)]. given #209 (T,wt=21): 10188 f(x,f(y,z,f(u,z,v)),f(u,x,z)) = f(u,x,z). [para(2745(a,1),126(a,1,3)),rewrite(3(3),2(4,R),3(4),3(5),9982(5),6657(4),12(2),2(4,R),3(4)),flip(a)]. given #210 (T,wt=24): 162 f(x,f(y,z,u),f(y,z,f(y,u,x))) = f(y,x,f(y,z,u)). [para(21(a,1),2(a,2)),rewrite(2(2),2(2),2(4),2(6,R),3(6))]. given #211 (A,wt=31): 79 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,z,f(x,y,f(x,w,f(x,u,v)))). [para(11(a,2),18(a,2,3)),rewrite(2(3,R),3(3),50(4),3(5),2(8,R),3(8)),flip(a)]. given #212 (F,wt=17): 10268 f(x,f(y,z,u),f(y,u,x)) = f(y,u,x). [para(998(a,1),162(a,1,3)),rewrite(2(2),2(2),2(3),2(3),8(4),2(3),2(3)),flip(a)]. given #213 (F,wt=20): 10345 f(x,f(y,z,x),f(z,u,x)) = f(y,x,f(z,u,x)). [para(10268(a,1),67(a,2,3)),rewrite(2(3),3(3),957(5),2(4),2(5,R)),flip(a)]. given #214 (T,wt=21): 10282 f(x,f(y,z,f(y,u,v)),f(y,v,x)) = f(y,v,x). [para(1008(a,1),162(a,1,3)),rewrite(2(3),2(3),2(4),2(4),8(5),2(4),2(4)),flip(a)]. given #215 (T,wt=21): 10341 f(x,y,f(y,z,f(x,u,y))) = f(y,z,f(x,u,y)). [para(10268(a,1),5045(a,1,3)),rewrite(2(2),2(2),2(4),2(4),2(6,R),3(6),198(6),2(5),2(5),2(7),3(7),12(7))]. given #216 (A,wt=31): 86 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,u,f(x,y,f(x,z,w)))). [para(11(a,1),24(a,2,3)),rewrite(50(4)),flip(a)]. given #217 (F,wt=22): 10386 f(x,y,f(z,u,f(x,z,f(z,v,y)))) = f(x,z,y). [para(10282(a,1),998(a,2)),rewrite(2(3),2(6),2(7,R),9979(9),9982(4),2(5))]. given #218 (F,wt=22): 10410 f(x,y,f(y,z,f(x,u,f(x,v,z)))) = f(x,y,z). [para(2851(a,1),10341(a,2)),rewrite(2(2,R),3(2),3(3),22(5),3(3),3(5))]. given #219 (T,wt=22): 10415 f(x,y,f(z,u,f(z,x,f(z,v,y)))) = f(z,x,y). [para(2(a,1),10386(a,1)),rewrite(2(2,R),3(2),2(4),2(4),2(5,R),3(5))]. given #220 (T,wt=22): 10436 f(x,y,f(x,z,f(z,u,f(z,v,y)))) = f(x,z,y). [para(10410(a,1),496(a,2)),rewrite(2(5,R),3(5),14(7),2(5,R),3(5))]. given #221 (A,wt=31): 87 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,u,f(x,y,f(x,v,f(x,w,z)))). [para(11(a,2),24(a,2,3)),rewrite(50(4),3(5))]. given #222 (F,wt=24): 163 f(x,f(y,z,u),f(z,u,f(x,y,z))) = f(x,z,f(y,z,u)). [para(2(a,1),21(a,1,2)),rewrite(3(2),2(5))]. given #223 (F,wt=20): 10474 f(x,f(y,z,x),f(u,y,x)) = f(u,x,f(y,z,x)). [para(12(a,1),163(a,1,2)),rewrite(7146(5),12(5))]. given #224 (T,wt=20): 10541 f(x,f(y,z,x),f(y,x,u)) = f(x,u,f(y,z,x)). [para(10474(a,1),2(a,2)),rewrite(2(2),2(2),2(3),2(5,R),3(5))]. given #225 (T,wt=24): 164 f(x,f(y,z,u),f(y,u,f(x,z,u))) = f(x,u,f(y,z,u)). [para(2(a,2),21(a,1,2)),rewrite(3(2),2(3,R),3(3),2(5),2(5))]. given #226 (A,wt=28): 88 f(x,y,f(x,z,f(y,u,f(x,y,v)))) = f(x,z,f(y,u,f(x,y,v))). [para(14(a,1),9(a,1,3)),rewrite(2(1),2(4),2(7,R),3(7)),flip(a)]. given #227 (F,wt=24): 203 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,y,u))). [para(125(a,1),24(a,2,3)),rewrite(198(2),50(3),3(1))]. given #228 (F,wt=24): 209 f(x,y,f(z,u,f(z,y,v))) = f(x,y,f(z,y,f(z,u,v))). [para(19(a,1),198(a,1,3)),rewrite(2(1,R),3(1),2(4,R),3(4),2(5,R),3(5),170(6),2(4,R),3(4),2(6,R),3(6)),flip(a)]. given #229 (T,wt=24): 213 f(x,y,f(z,u,f(u,y,v))) = f(u,y,f(x,y,f(z,u,v))). [para(23(a,1),2(a,2)),rewrite(2(1,R),3(1),3(3),2(5,R),3(5),2(6,R),3(6))]. given #230 (T,wt=24): 214 f(x,y,f(z,u,f(u,x,v))) = f(u,x,f(x,y,f(z,u,v))). [para(2(a,1),23(a,1)),rewrite(2(1,R),3(1),2(3),2(3),2(6,R),3(6))]. given #231 (A,wt=31): 89 f(x,f(y,z,u),f(x,v,f(y,z,f(x,y,u)))) = f(x,v,f(x,y,f(y,z,u))). [para(9(a,2),14(a,1,3,3))]. given #232 (F,wt=24): 257 f(x,y,f(z,u,f(u,y,v))) = f(x,y,f(u,y,f(z,u,v))). [para(23(a,1),198(a,1,3)),rewrite(2(1,R),3(1),2(4,R),3(4),2(5,R),3(5),181(6),2(4,R),3(4),2(6,R),3(6)),flip(a)]. given #233 (F,wt=24): 261 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,v,y))). [para(25(a,1),2(a,2)),rewrite(3(3),2(5,R),3(5)),flip(a)]. given #234 (T,wt=24): 313 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,z,f(y,u,x))). [para(31(a,1),2(a,2)),rewrite(2(2),2(3),2(4),2(4))]. given #235 (T,wt=20): 10759 f(f(x,y,z),f(z,u,v),f(x,y,z)) = f(x,y,z). [para(999(a,1),313(a,1,3)),rewrite(7985(10))]. given #236 (A,wt=35): 91 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,y))))) = f(x,z,f(x,u,f(x,v,f(x,w,y)))). [para(14(a,1),11(a,1,3,3)),flip(a)]. given #237 (F,wt=20): 10761 f(f(x,y,z),f(y,u,v),f(x,y,z)) = f(x,y,z). [para(1068(a,1),313(a,1,3)),rewrite(7986(10))]. given #238 (F,wt=20): 10842 f(f(x,y,z),f(x,u,v),f(x,y,z)) = f(x,y,z). [para(313(a,1),209(a,2)),rewrite(3(4),1(6),12(5),13(5)),flip(a)]. given #239 (T,wt=24): 314 f(x,f(y,z,u),f(v,y,x)) = f(v,x,f(y,z,f(y,x,u))). [para(31(a,2),2(a,2)),rewrite(2(1,R),3(1),3(3),2(5),2(5)),flip(a)]. given #240 (T,wt=17): 11016 f(x,f(y,x,z),f(u,y,z)) = f(y,x,z). [para(314(a,2),6497(a,1,3)),rewrite(2(2,R),3(2),2(4),2(4),13(4),7140(5),2(6,R),3(6),2(7,R),3(7),3618(7),1848(6))]. given #241 (A,wt=35): 92 f(x,y,f(x,z,f(x,u,f(x,v,f(x,y,w))))) = f(x,z,f(x,v,f(x,y,f(x,u,w)))). [para(11(a,1),14(a,1,3,3)),rewrite(50(7),3(5),50(5),3(3),14(3),13(4))]. given #242 (F,wt=17): 11017 f(x,f(y,z,u),f(z,x,u)) = f(z,x,u). [para(314(a,2),6497(a,2)),rewrite(2(4,R),3(4),2(5,R),3(5),3618(5),1848(4),8(3),2(2,R),3(2),2(4),2(4),13(4)),flip(a)]. given #243 (F,wt=20): 11010 f(f(x,y,z),f(u,v,w),f(x,y,z)) = f(x,y,z). [para(314(a,1),47(a,2,3)),rewrite(2(5),2(5),12(5),13(5),2(5,R),8(5),3(9),1(11),2(7,R),8(7))]. given #244 (T,wt=24): 316 f(x,f(y,z,u),f(x,u,v)) = f(x,v,f(y,u,f(x,z,u))). [para(2(a,2),31(a,1,2)),rewrite(3(2),3(4),2(5,R),3(5))]. given #245 (T,wt=17): 11208 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(316(a,2),22(a,2)),rewrite(3(1),795(3),13(2),3(2),3(3)),flip(a)]. given #246 (A,wt=31): 93 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,y,f(x,w,f(x,z,f(x,u,v)))). [para(11(a,2),14(a,1,3,3)),rewrite(3(3),50(7),3(5),50(5),3(3),15(3),15(4),15(5))]. given #247 (F,wt=17): 11218 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(316(a,2),208(a,1,3)),rewrite(2(3),9558(5),6530(6),2(4,R),3(4))]. given #248 (F,wt=17): 11219 f(x,f(y,z,u),f(y,x,u)) = f(y,x,u). [para(316(a,2),208(a,2)),rewrite(6530(4),2(2,R),3(2),11218(3),2(3)),flip(a)]. given #249 (T,wt=17): 11249 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(316(a,2),864(a,1)),rewrite(12(3),12(6),8(6))]. given #250 (T,wt=18): 11468 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y). [back_rewrite(11186),rewrite(11218(3)),flip(a)]. given #251 (A,wt=31): 94 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,y,f(x,v,f(x,z,f(x,u,w)))). [para(11(a,1),14(a,2,3)),rewrite(14(7))]. given #252 (F,wt=20): 11247 f(x,f(y,z,x),f(y,u,x)) = f(y,x,f(u,z,x)). [para(840(a,2),316(a,2)),rewrite(8(2),3(2)),flip(a)]. given #253 (F,wt=21): 11178 f(x,y,f(z,y,f(x,u,y))) = f(x,y,f(z,u,y)). [para(8(a,1),316(a,1,3)),rewrite(3(2)),flip(a)]. given #254 (T,wt=21): 11318 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(316(a,2),3411(a,1,2)),rewrite(11087(3),13(2),2(3),2(5))]. given #255 (T,wt=21): 11475 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [back_rewrite(11307),rewrite(2(1),3(3),3(5))]. given #256 (A,wt=28): 95 f(x,y,f(z,x,f(y,u,f(x,y,v)))) = f(z,x,f(y,u,f(x,y,v))). [para(14(a,1),17(a,1,3)),rewrite(2(1),2(4),2(7,R),3(7)),flip(a)]. given #257 (F,wt=21): 11477 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(10(a,2),11208(a,1,2))]. given #258 (F,wt=21): 11480 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(18(a,1),11208(a,1,2))]. given #259 (T,wt=21): 11884 f(x,f(y,z,f(y,u,v)),f(y,x,v)) = f(y,x,v). [para(11477(a,1),126(a,1,3)),rewrite(3(3),2(4,R),3(4),3(5),11087(5),10211(4),10410(4),2(4,R),3(4)),flip(a)]. given #260 (T,wt=22): 11871 f(x,y,f(z,u,f(z,y,f(z,v,x)))) = f(z,x,y). [para(11477(a,1),787(a,2)),rewrite(2(3),2(3),2(4),2(4),3(7),11003(9),3(2),2(5),2(5))]. given #261 (A,wt=28): 96 f(x,y,f(y,z,f(x,u,f(x,y,v)))) = f(y,z,f(x,u,f(x,y,v))). [para(14(a,1),17(a,2,3)),rewrite(3(1),2(3,R),3(3),3(5),2(7,R),3(7))]. given #262 (F,wt=24): 457 f(x,y,f(z,y,f(y,u,v))) = f(z,y,f(y,u,f(x,y,v))). [para(33(a,1),2(a,2)),rewrite(3(3),2(4,R),3(4))]. given #263 (F,wt=24): 493 f(x,y,f(y,z,f(y,u,v))) = f(y,u,f(y,z,f(x,y,v))). [para(34(a,2),5(a,1))]. given #264 (T,wt=24): 500 f(x,f(y,x,z),f(x,u,v)) = f(y,x,f(x,u,f(x,v,z))). [para(34(a,2),10(a,1)),flip(a)]. given #265 (T,wt=24): 501 f(x,y,f(y,z,f(y,u,v))) = f(y,u,f(y,v,f(x,y,z))). [para(10(a,1),34(a,1,3))]. given #266 (A,wt=31): 97 f(x,f(y,z,u),f(x,v,f(y,z,f(x,z,u)))) = f(x,v,f(x,z,f(y,z,u))). [para(17(a,1),14(a,1,3,3))]. given #267 (F,wt=22): 12255 f(x,y,f(x,z,f(u,z,f(z,v,y)))) = f(x,z,y). [para(8305(a,1),97(a,1,3)),rewrite(11480(4)),flip(a)]. given #268 (F,wt=24): 503 f(x,y,f(y,z,f(y,u,v))) = f(y,v,f(y,z,f(x,y,u))). [para(10(a,2),34(a,1,3))]. given #269 (T,wt=24): 517 f(x,y,f(y,z,f(y,u,v))) = f(y,v,f(y,u,f(x,y,z))). [para(24(a,1),34(a,1,3))]. given #270 (T,wt=24): 570 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,v,f(z,x,u))). [para(496(a,1),17(a,2,3)),rewrite(2(1),2(1),2(3,R),3(3),96(4),3(4),2(5,R),3(5),2(6,R),3(6))]. given #271 (A,wt=31): 99 f(x,f(y,z,u),f(x,v,f(y,u,f(x,y,z)))) = f(x,v,f(x,y,f(y,z,u))). [para(18(a,2),14(a,1,3,3))]. given #272 (F,wt=22): 12381 f(x,y,f(z,u,f(y,u,f(x,z,u)))) = f(x,y,u). [para(570(a,1),8575(a,1,3)),rewrite(2(1),3(1),2(2,R),3(2),2(5),2(5))]. given #273 (F,wt=18): 12402 f(x,y,f(z,y,f(x,u,z))) = f(x,z,y). [para(12381(a,1),3(a,2)),rewrite(2(2,R),3(2),6497(3),3(3),3(4))]. given #274 (T,wt=18): 12424 f(x,y,f(z,y,f(z,u,x))) = f(z,x,y). [para(12381(a,1),4035(a,2)),rewrite(2(2,R),3(2),6497(3),2(5,R),3(5),6497(6),3(6),4322(8),3(4))]. given #275 (T,wt=24): 669 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(z,v,f(x,z,u))). [para(496(a,1),596(a,1,3)),rewrite(2(1),3(1),2(4),2(5,R),3(5),3(6),594(6),2(4),3(4),2(7,R),3(7),88(7))]. given #276 (A,wt=28): 103 f(x,y,f(y,z,f(y,u,f(x,y,v)))) = f(x,y,f(y,z,f(y,u,v))). [para(9(a,2),22(a,1,3,3))]. given #277 (F,wt=24): 792 f(x,y,f(x,f(z,y,u),f(x,v,z))) = f(x,v,f(x,z,y)). [back_rewrite(407),rewrite(787(3)),flip(a)]. given #278 (F,wt=21): 12575 f(x,f(y,z,f(u,v,y)),f(x,u,y)) = f(x,u,y). [para(998(a,1),792(a,2)),rewrite(3(3),2060(6))]. given #279 (T,wt=21): 12592 f(x,f(y,z,f(u,v,y)),f(x,v,y)) = f(x,v,y). [para(3859(a,1),792(a,2)),rewrite(3(3),1100(6))]. given #280 (T,wt=21): 12648 f(x,f(y,z,f(u,y,v)),f(x,y,v)) = f(x,y,v). [para(9979(a,1),792(a,2)),rewrite(3(3),3(4),1100(6))]. given #281 (A,wt=35): 107 f(x,y,f(x,z,f(x,u,f(y,v,f(x,y,w))))) = f(x,z,f(x,u,f(x,y,f(y,v,w)))). [para(22(a,1),11(a,1,3,3)),flip(a)]. given #282 (F,wt=21): 12699 f(x,f(y,z,f(u,v,z)),f(x,v,z)) = f(x,v,z). [para(2(a,2),12592(a,1,2)),rewrite(3(2))]. given #283 (F,wt=21): 12711 f(x,f(y,z,f(u,z,v)),f(x,z,v)) = f(x,z,v). [para(2(a,2),12648(a,1,2)),rewrite(3(2))]. given #284 (T,wt=24): 824 f(x,f(y,z,u),f(x,v,f(x,y,z))) = f(x,v,f(x,y,z)). [para(778(a,1),25(a,1,3)),flip(a)]. given #285 (T,wt=24): 825 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,u,y))). [para(25(a,1),778(a,2)),rewrite(3(5),632(6),50(6),3(4),805(7))]. given #286 (A,wt=31): 108 f(x,y,f(x,z,f(u,v,f(x,u,w)))) = f(x,z,f(x,y,f(x,u,f(u,v,w)))). [para(22(a,1),11(a,2,3,3)),rewrite(88(4))]. given #287 (F,wt=24): 832 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(z,x,f(x,y,v))). [para(33(a,2),778(a,2)),rewrite(3(5),801(7))]. given #288 (F,wt=24): 837 f(x,y,f(z,x,f(x,u,v))) = f(x,y,f(x,u,f(z,x,v))). [para(34(a,1),778(a,2)),rewrite(3(5),801(7))]. given #289 (T,wt=24): 872 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(x,z,f(v,z,u))). [para(840(a,2),14(a,2,3)),rewrite(14(5)),flip(a)]. given #290 (T,wt=24): 897 f(x,y,f(z,u,f(x,v,z))) = f(x,z,f(x,y,f(v,z,u))). [para(840(a,2),496(a,2,3)),rewrite(2(3,R),3(3),14(5),2(6,R),3(6)),flip(a)]. given #291 (A,wt=35): 109 f(x,y,f(y,z,f(x,u,f(x,v,f(x,y,w))))) = f(x,y,f(y,z,f(x,u,f(x,v,w)))). [para(11(a,2),22(a,1,3,3))]. given #292 (F,wt=24): 964 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(x,u,f(z,v,u))). [para(864(a,1),14(a,2,3)),rewrite(14(5)),flip(a)]. given #293 (F,wt=24): 990 f(x,y,f(z,u,f(x,v,u))) = f(x,u,f(x,y,f(z,v,u))). [para(864(a,1),496(a,2,3)),rewrite(2(3,R),3(3),14(5),2(6,R),3(6)),flip(a)]. given #294 (T,wt=24): 1041 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,z,f(y,x,u))). [para(31(a,2),889(a,2)),rewrite(2(1,R),3(1),2(4,R),3(4),889(7),2(5)),flip(a)]. given #295 (T,wt=24): 1059 f(x,y,f(x,f(z,u,v),f(y,z,u))) = f(x,y,f(z,u,v)). [para(889(a,1),778(a,1,3,3)),rewrite(2(2))]. given #296 (A,wt=28): 111 f(x,y,f(z,x,f(x,u,f(x,y,v)))) = f(z,x,f(x,y,f(x,u,v))). [para(22(a,1),17(a,1,3)),rewrite(2(2,R),3(2),2(4,R),3(4),2(7,R),3(7)),flip(a)]. given #297 (F,wt=21): 13090 f(x,y,f(z,f(x,y,z),f(u,v,w))) = f(x,y,z). [para(1059(a,1),6052(a,1,3))]. given #298 (F,wt=21): 13176 f(x,y,f(z,f(x,z,y),f(u,v,w))) = f(x,z,y). [para(13090(a,1),2(a,2)),rewrite(2(1),2(1),3(4),2(5),2(5))]. given #299 (T,wt=24): 1060 f(f(x,y,z),f(x,y,f(y,z,u)),f(x,z,v)) = f(x,y,z). [para(778(a,1),889(a,1,3)),rewrite(2(1,R),3(1),3(4),2(5),2(6,R),3(6),793(8))]. given #300 (T,wt=24): 1063 f(x,f(y,z,x),f(u,f(y,z,v),f(y,z,x))) = f(y,z,x). [para(889(a,1),840(a,1,3)),rewrite(2(3,R),8(3),2(5)),flip(a)]. given #301 (A,wt=28): 116 f(x,y,f(x,z,f(u,y,f(x,y,v)))) = f(x,z,f(u,y,f(x,y,v))). [para(66(a,1),9(a,1,3)),rewrite(2(1,R),3(1),2(4,R),3(4),2(7,R),3(7)),flip(a)]. given #302 (F,wt=24): 1067 f(x,f(y,z,u),f(x,u,f(y,z,v))) = f(x,u,f(y,z,v)). [para(889(a,1),889(a,1,2)),rewrite(2(3),2(6))]. given #303 (F,wt=24): 1084 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,z,f(x,y,u))). [para(31(a,2),892(a,2)),rewrite(3(3),2(6,R),3(6),387(7),998(7),2(5,R),3(5)),flip(a)]. given #304 (T,wt=24): 1093 f(x,f(y,x,z),f(u,f(y,z,v),f(y,x,z))) = f(y,x,z). [para(892(a,1),840(a,1,3)),rewrite(2(3,R),8(3),2(5)),flip(a)]. given #305 (T,wt=24): 1096 f(f(x,y,z),f(x,y,u),f(u,v,f(x,y,u))) = f(x,y,u). [para(889(a,1),892(a,1,3)),rewrite(3(3),3(5),889(8))]. given #306 (A,wt=28): 117 f(x,y,f(z,x,f(u,y,f(x,y,v)))) = f(z,x,f(u,y,f(x,y,v))). [para(66(a,1),17(a,1,3)),rewrite(2(1,R),3(1),2(4,R),3(4),2(7,R),3(7)),flip(a)]. given #307 (F,wt=24): 1100 f(x,f(y,z,u),f(x,v,f(x,z,u))) = f(x,v,f(x,z,u)). [para(997(a,1),5(a,2,3))]. given #308 (F,wt=24): 1136 f(x,f(y,z,u),f(x,u,f(x,z,v))) = f(x,v,f(x,z,u)). [para(997(a,1),26(a,2,3)),rewrite(3(2))]. given #309 (T,wt=24): 1151 f(x,y,f(x,f(z,x,u),f(y,u,v))) = f(z,x,f(x,y,u)). [para(997(a,1),34(a,1,3)),rewrite(2(3),2(3),387(6)),flip(a)]. given #310 (T,wt=24): 1175 f(x,y,f(x,f(z,u,v),f(y,u,v))) = f(x,y,f(z,u,v)). [para(997(a,1),778(a,1,3,3))]. given #311 (A,wt=35): 120 f(x,y,f(x,z,f(x,u,f(v,y,f(x,y,w))))) = f(x,z,f(x,u,f(v,y,f(x,y,w)))). [para(115(a,1),11(a,1,3,3)),flip(a)]. given #312 (F,wt=24): 1179 f(x,y,f(x,f(y,z,u),f(x,v,z))) = f(x,v,f(x,y,z)). [para(997(a,1),36(a,1,3)),rewrite(2(3),2(3)),flip(a)]. low water: id=8297, wt=44 given #313 (F,wt=24): 1184 f(f(x,y,z),f(y,z,u),f(u,v,f(y,z,u))) = f(y,z,u). [para(997(a,1),892(a,1,3)),rewrite(2(2),2(2),3(3),2(4),2(4),3(5),2(7),2(7),1099(8))]. low water: id=8519, wt=43 given #314 (T,wt=24): 1300 f(x,f(y,z,x),f(u,f(y,z,x),f(y,z,v))) = f(y,z,x). [para(999(a,1),17(a,1,3)),rewrite(8(3)),flip(a)]. low water: id=8961, wt=42 given #315 (T,wt=24): 1337 f(f(x,y,z),f(x,z,u),f(x,y,f(y,z,v))) = f(x,y,z). [para(778(a,1),999(a,1,2)),rewrite(2(1,R),3(1),3(3),2(5,R),2(6,R),3(6),793(8))]. given #316 (A,wt=31): 121 f(x,y,f(z,u,f(z,x,f(z,v,w)))) = f(x,y,f(z,x,f(z,v,f(z,u,w)))). [para(11(a,1),115(a,1,3,3)),rewrite(2(4,R),3(4),96(5),2(8,R),3(8))]. given #317 (F,wt=24): 1338 f(f(x,y,z),f(x,y,u),f(z,v,f(x,y,z))) = f(x,y,z). [para(999(a,1),808(a,1,3)),rewrite(2(3,R),8(3),3(5)),flip(a)]. low water: id=9239, wt=41 low water: id=9583, wt=40 given #318 (F,wt=24): 1371 f(f(x,y,z),f(y,z,u),f(x,v,f(x,y,z))) = f(x,y,z). [para(1000(a,1),808(a,1,3)),rewrite(2(3,R),8(3),3(5)),flip(a)]. given #319 (T,wt=24): 1375 f(x,f(y,x,z),f(u,f(y,x,z),f(y,z,v))) = f(y,x,z). [para(1068(a,1),17(a,1,3)),rewrite(8(3)),flip(a)]. given #320 (T,wt=24): 1390 f(f(x,y,z),f(x,z,u),f(y,v,f(x,y,z))) = f(x,y,z). [para(1068(a,1),808(a,1,3)),rewrite(2(3,R),8(3),3(5)),flip(a)]. given #321 (A,wt=31): 124 f(x,y,f(z,u,f(x,v,f(x,z,w)))) = f(x,z,f(x,y,f(z,u,f(x,v,w)))). [para(5(a,1),19(a,1,3,3))]. low water: id=11161, wt=39 given #322 (F,wt=24): 1417 f(f(x,y,z),f(x,y,u),f(v,u,f(x,y,u))) = f(x,y,u). [para(999(a,1),1099(a,1,3)),rewrite(3(5),999(8))]. low water: id=11470, wt=38 given #323 (F,wt=24): 1490 f(f(x,y,z),f(x,y,f(x,z,u)),f(y,z,v)) = f(x,y,z). [para(784(a,1),889(a,1,3)),rewrite(2(1,R),3(1),2(3,R),3(3),2(4),2(4),2(5),2(6,R),3(6),787(8),3(6))]. given #324 (T,wt=24): 1491 f(x,y,f(y,f(x,z,u),f(z,u,v))) = f(x,y,f(z,u,v)). [para(889(a,1),784(a,1,3,3)),rewrite(2(2),2(3,R),3(6))]. given #325 (T,wt=21): 14355 f(x,y,f(z,f(y,z,u),f(x,v,z))) = f(x,y,z). [para(1523(a,1),1491(a,1,3)),rewrite(3(2),6530(3),2(4,R),6497(5)),flip(a)]. given #326 (A,wt=31): 127 f(x,y,f(z,u,f(x,z,f(u,v,w)))) = f(x,z,f(x,y,f(u,v,f(z,u,w)))). [para(19(a,1),9(a,1,3)),rewrite(2(2,R),3(2),2(8,R),3(8))]. given #327 (F,wt=24): 1495 f(x,y,f(y,f(x,z,u),f(v,z,u))) = f(x,y,f(v,z,u)). [para(997(a,1),784(a,1,3,3)),rewrite(2(3,R),3(6))]. given #328 (F,wt=24): 1498 f(f(x,y,z),f(y,z,u),f(x,y,f(x,z,v))) = f(x,y,z). [para(784(a,1),999(a,1,2)),rewrite(2(1,R),3(1),2(3),2(3),2(4,R),3(4),2(5,R),2(6,R),3(6),787(8),3(6))]. given #329 (T,wt=24): 1508 f(x,y,f(y,f(z,u,v),f(x,z,u))) = f(x,y,f(z,u,v)). [para(889(a,1),786(a,1,3,3)),rewrite(2(2))]. given #330 (T,wt=24): 1510 f(x,y,f(y,f(z,u,v),f(x,u,v))) = f(x,y,f(z,u,v)). [para(997(a,1),786(a,1,3,3))]. given #331 (A,wt=31): 129 f(x,y,f(z,u,f(x,z,f(z,v,w)))) = f(x,z,f(x,y,f(z,w,f(z,u,v)))). [para(10(a,1),19(a,2,3,3))]. given #332 (F,wt=24): 1542 f(x,f(y,z,f(x,u,y)),f(x,v,u)) = f(x,v,f(x,u,y)). [para(791(a,1),10(a,1,3)),flip(a)]. given #333 (F,wt=24): 1581 f(f(x,y,z),f(x,u,f(x,y,z)),f(y,z,v)) = f(x,y,z). [para(791(a,1),889(a,1,3)),rewrite(2(1),2(4),2(5),2(6),1538(8))]. given #334 (T,wt=24): 1663 f(x,f(y,z,u),f(x,v,f(y,z,v))) = f(x,v,f(y,z,u)). [para(889(a,1),793(a,1,3,3))]. given #335 (T,wt=24): 1664 f(x,f(y,z,u),f(x,v,f(z,u,v))) = f(x,v,f(y,z,u)). [para(997(a,1),793(a,1,3,3)),rewrite(2(2),2(2))]. given #336 (A,wt=38): 130 f(x,y,f(x,z,f(x,u,f(v,w,f(x,v,v6))))) = f(x,z,f(x,u,f(x,v,f(x,y,f(v,w,v6))))). [para(19(a,1),11(a,1,3,3)),flip(a)]. given #337 (F,wt=24): 1693 f(x,f(y,z,u),f(x,u,v)) = f(x,v,f(z,u,f(x,y,u))). [para(1661(a,1),808(a,2,3)),rewrite(2(2,R),3(2),2(4))]. given #338 (F,wt=24): 1697 f(f(x,y,z),f(x,u,y),f(u,v,f(x,u,y))) = f(x,u,y). [para(892(a,1),1661(a,1,3)),rewrite(2(3,R),8(3),3(5)),flip(a)]. given #339 (T,wt=24): 1698 f(f(x,y,z),f(u,x,y),f(u,v,f(u,x,y))) = f(u,x,y). [para(997(a,1),1661(a,1,3)),rewrite(2(3,R),8(3),2(2),2(2),3(5)),flip(a)]. given #340 (T,wt=24): 1713 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(x,u,f(v,z,u))). [para(1668(a,1),14(a,2,3)),rewrite(14(5)),flip(a)]. given #341 (A,wt=38): 131 f(x,y,f(x,z,f(x,u,f(v,w,f(x,v,v6))))) = f(x,v,f(x,y,f(x,z,f(x,u,f(v,w,v6))))). [para(19(a,2),11(a,1,3,3))]. given #342 (F,wt=24): 1737 f(x,y,f(z,u,f(x,v,u))) = f(x,u,f(x,y,f(v,z,u))). [para(1668(a,1),496(a,2,3)),rewrite(2(3,R),3(3),14(5),2(6,R),3(6)),flip(a)]. given #343 (F,wt=24): 1745 f(f(x,y,z),f(x,u,y),f(v,u,f(x,u,y))) = f(x,u,y). [para(892(a,1),1668(a,1,3)),rewrite(8(3)),flip(a)]. given #344 (T,wt=24): 1746 f(f(x,y,z),f(u,x,y),f(v,u,f(u,x,y))) = f(u,x,y). [para(997(a,1),1668(a,1,3)),rewrite(8(3),2(2),2(2)),flip(a)]. given #345 (T,wt=24): 1802 f(x,y,f(z,y,f(y,u,v))) = f(x,y,f(y,u,f(z,y,v))). [para(33(a,1),795(a,2)),rewrite(3(5),2(6,R),3(6),1650(7),2(4,R),3(4))]. given #346 (A,wt=38): 132 f(x,y,f(x,z,f(x,u,f(v,w,f(x,v,v6))))) = f(x,u,f(x,y,f(x,v,f(x,z,f(v,w,v6))))). [para(19(a,1),11(a,2,3,3))]. given #347 (F,wt=24): 1804 f(x,f(y,z,u),f(y,z,f(z,u,x))) = f(z,x,f(y,z,u)). [para(567(a,1),795(a,1,3)),rewrite(3(2),2(4,R),3(4),3(6))]. given #348 (F,wt=24): 1876 f(f(x,y,z),f(u,x,f(x,y,z)),f(y,z,v)) = f(x,y,z). [para(957(a,1),889(a,1,3)),rewrite(2(1,R),3(1),2(4,R),3(4),2(5),2(6,R),3(6),1848(8))]. given #349 (T,wt=24): 1881 f(f(x,y,z),f(y,z,u),f(v,x,f(x,y,z))) = f(x,y,z). [para(957(a,1),999(a,1,2)),rewrite(2(1,R),3(1),2(3,R),3(3),2(5,R),2(6,R),3(6),1848(8))]. given #350 (T,wt=24): 2060 f(x,f(y,z,u),f(x,v,f(x,y,u))) = f(x,v,f(x,y,u)). [para(998(a,1),43(a,1,3,3)),rewrite(998(7))]. given #351 (A,wt=38): 133 f(x,y,f(x,z,f(x,u,f(v,w,f(x,v,v6))))) = f(x,z,f(x,v,f(x,y,f(x,u,f(v,w,v6))))). [para(19(a,2),11(a,2,3,3)),flip(a)]. given #352 (F,wt=24): 3991 f(f(x,y,z),f(x,y,f(y,u,z)),f(x,z,v)) = f(x,y,z). [para(3859(a,1),889(a,1,3)),rewrite(2(1),3(4),2(5),2(6),3971(8))]. given #353 (F,wt=24): 3994 f(f(x,y,z),f(x,z,u),f(x,y,f(y,v,z))) = f(x,y,z). [para(3859(a,1),999(a,1,2)),rewrite(2(1),3(3),2(5,R),2(6),3971(8))]. given #354 (T,wt=24): 4713 f(x,y,f(x,f(z,u,v),f(y,z,v))) = f(x,y,f(z,u,v)). [para(998(a,1),1008(a,1,3,3))]. given #355 (T,wt=24): 4796 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(x,y,f(z,x,v))). [para(34(a,1),1512(a,2)),rewrite(3(7),632(8),50(8),3(6),2(9,R),3(9),4793(10))]. given #356 (A,wt=31): 134 f(x,y,f(x,z,f(u,v,f(x,u,w)))) = f(x,u,f(x,z,f(x,y,f(u,v,w)))). [para(19(a,2),11(a,2,3)),flip(a)]. given #357 (F,wt=24): 5110 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(z,x,f(x,y,u))). [para(25(a,1),1979(a,2)),rewrite(3(7),2(8,R),3(8),2(9,R),3(9),387(10),3(9),4638(10),2(5,R),3(5))]. given #358 (F,wt=24): 5111 f(x,y,f(z,x,f(x,u,v))) = f(x,y,f(x,v,f(z,x,u))). [para(26(a,2),1979(a,2)),rewrite(3(7),2(8,R),3(8),2(9,R),3(9),387(10),3(9),4638(10),2(4,R),3(4))]. given #359 (T,wt=24): 5154 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,v,f(x,y,u))). [para(52(a,1),1979(a,2)),rewrite(3(7),2(8,R),3(8),2(9,R),3(9),387(10),3(9),4638(10),2(6,R),3(6))]. given #360 (T,wt=24): 5160 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(x,v,f(z,x,y))). [para(55(a,1),1979(a,2)),rewrite(3(7),2(8,R),3(8),2(9,R),3(9),387(10),3(9),4638(10),2(4,R),3(4))]. given #361 (A,wt=38): 135 f(x,y,f(z,u,f(x,v,f(x,z,f(x,w,v6))))) = f(x,z,f(x,y,f(z,u,f(x,w,f(x,v,v6))))). [para(11(a,1),19(a,1,3,3))]. given #362 (F,wt=24): 5814 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(z,x,f(x,u,y))). [para(25(a,1),3470(a,2)),rewrite(2(5,R),3(5),50(7),5808(8),2(5,R),3(5))]. given #363 (F,wt=24): 5857 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,v,f(x,u,y))). [para(52(a,1),3470(a,2)),rewrite(2(5,R),3(5),50(7),5808(8),2(6,R),3(6))]. given #364 (T,wt=24): 6019 f(x,f(y,z,f(x,u,y)),f(v,x,u)) = f(x,y,f(v,x,u)). [para(997(a,1),4408(a,1,3,3)),rewrite(2(2),2(2),2(4,R),2(6))]. given #365 (T,wt=24): 6371 f(x,f(y,z,f(x,u,z)),f(v,x,u)) = f(x,z,f(v,x,u)). [para(997(a,1),4973(a,1,3,3)),rewrite(2(2),2(2),2(4,R),2(6))]. given #366 (A,wt=38): 136 f(x,y,f(z,u,f(x,v,f(x,w,f(x,z,v6))))) = f(x,z,f(x,y,f(z,u,f(x,v,f(x,w,v6))))). [para(11(a,2),19(a,1,3,3))]. given #367 (F,wt=24): 6676 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,v,u))). [para(2(a,1),63(a,1,3)),rewrite(2(2),2(2),3(4))]. given #368 (F,wt=24): 6778 f(x,f(y,z,u),f(y,u,f(y,x,z))) = f(y,x,f(y,z,u)). [para(1002(a,1),63(a,2,3)),rewrite(2(4),2(4),13(4),1766(5),2(7,R),50(7),3(5),13(6))]. given #369 (T,wt=24): 6915 f(f(x,y,z),f(y,z,u),f(v,u,f(y,z,u))) = f(y,z,u). [para(6743(a,1),1099(a,1,3)),rewrite(2(2),2(2),2(4),2(4),3(5),2(6),2(6),6893(8))]. given #370 (T,wt=24): 7141 f(f(x,y,z),f(x,z,u),f(u,v,f(x,z,u))) = f(x,z,u). [para(7111(a,1),889(a,1,3)),rewrite(2(2),2(2),3(3),2(4),2(4),3(5),2(6),2(6),7129(8))]. given #371 (A,wt=38): 137 f(x,y,f(z,u,f(x,z,f(z,v,f(z,w,v6))))) = f(x,z,f(x,y,f(z,w,f(z,u,f(z,v,v6))))). [para(11(a,1),19(a,2,3,3))]. given #372 (F,wt=24): 7142 f(f(x,y,z),f(x,z,u),f(v,u,f(x,z,u))) = f(x,z,u). [para(7111(a,1),1099(a,1,3)),rewrite(2(2),2(2),2(4),2(4),3(5),2(6),2(6),7129(8))]. given #373 (F,wt=24): 7152 f(x,f(y,z,u),f(x,v,f(y,u,v))) = f(x,v,f(y,z,u)). [para(7111(a,1),3971(a,1,3,3)),rewrite(2(2),2(2))]. given #374 (T,wt=24): 7161 f(x,y,f(y,f(z,u,v),f(x,z,v))) = f(x,y,f(z,u,v)). [para(7111(a,1),6530(a,1,3,3))]. given #375 (T,wt=24): 7164 f(x,f(y,z,u),f(y,z,f(z,x,u))) = f(z,x,f(y,z,u)). [para(2(a,1),65(a,1)),rewrite(2(1,R),3(1),2(4),2(4),2(6,R),3(6))]. given #376 (A,wt=38): 138 f(x,y,f(z,u,f(x,z,f(z,v,f(z,w,v6))))) = f(x,z,f(x,y,f(z,v,f(z,w,f(z,u,v6))))). [para(11(a,2),19(a,2,3,3))]. given #377 (F,wt=24): 7167 f(x,y,f(z,u,f(z,y,v))) = f(x,y,f(z,y,f(z,v,u))). [para(10(a,1),65(a,2,3)),rewrite(65(6)),flip(a)]. given #378 (F,wt=24): 7171 f(x,y,f(z,y,f(y,u,v))) = f(x,y,f(y,v,f(z,y,u))). [para(18(a,2),65(a,2,3)),rewrite(65(6))]. given #379 (T,wt=24): 7420 f(x,y,f(y,f(x,z,u),f(z,v,u))) = f(x,y,f(z,v,u)). [para(7111(a,1),7349(a,1,3,3)),rewrite(3(4),22(5))]. given #380 (T,wt=24): 7530 f(x,f(y,z,u),f(v,x,z)) = f(v,x,f(y,z,f(x,z,u))). [para(67(a,2),808(a,1)),flip(a)]. given #381 (A,wt=31): 139 f(x,y,f(z,u,f(y,z,f(u,v,w)))) = f(y,z,f(x,y,f(u,v,f(z,u,w)))). [para(19(a,1),17(a,1,3)),rewrite(2(2,R),3(2),2(8,R),3(8))]. given #382 (F,wt=24): 7765 f(x,f(y,z,f(x,u,y)),f(x,u,v)) = f(x,u,f(x,y,v)). [para(791(a,1),7547(a,1,2)),rewrite(2(1,R),3(1),2(2),3(2),50(3),3(1),13(3),2(3,R),3(3),2(5),3(5)),flip(a)]. given #383 (F,wt=24): 7819 f(x,f(y,z,u),f(y,u,f(y,z,x))) = f(y,z,f(y,u,x)). [para(7547(a,1),63(a,2,3)),rewrite(2(1,R),3(1),2(2,R),3(2),2(3),3(3),795(4),3(2),50(3),3(1),13(3),2(3,R),3(3),2(4),3(4),2(6,R),3(6)),flip(a)]. given #384 (T,wt=18): 15406 f(x,y,f(z,y,f(u,z,x))) = f(z,x,y). [para(3859(a,1),7819(a,1,3)),rewrite(2(2),3(2),2(3),2(3),8(4),2(3,R),3(3),2(4,R),3(4)),flip(a)]. given #385 (T,wt=18): 15450 f(x,y,f(z,y,f(u,x,z))) = f(x,z,y). [para(9979(a,1),7819(a,1,3)),rewrite(2(2),2(2),2(3),2(3),8(4),2(3,R),3(3),2(4,R),3(4)),flip(a)]. given #386 (A,wt=31): 141 f(x,y,f(z,u,f(y,v,f(y,z,w)))) = f(y,z,f(x,y,f(z,u,f(y,v,w)))). [para(19(a,2),17(a,1,3)),rewrite(2(1,R),3(1),2(8,R),3(8))]. given #387 (F,wt=22): 15410 f(x,y,f(z,y,f(z,u,f(z,v,x)))) = f(z,x,y). [para(1008(a,1),7819(a,1,3)),rewrite(2(3),3(3),2(4),2(4),8(5),2(4,R),3(4),2(5,R),3(5)),flip(a)]. given #388 (F,wt=22): 15422 f(x,y,f(z,y,f(u,x,f(x,z,v)))) = f(x,z,y). [para(2730(a,1),7819(a,1,3)),rewrite(2(1,R),3(1),2(3),2(3),2(4),3(4),8(5),2(2,R),3(2),2(4,R),3(4),2(5,R),3(5)),flip(a)]. given #389 (T,wt=22): 15425 f(x,y,f(z,y,f(u,z,f(z,x,v)))) = f(z,x,y). [para(3882(a,1),7819(a,1,3)),rewrite(2(3),3(3),2(4),2(4),8(5),2(4,R),3(4),2(5,R),3(5)),flip(a)]. given #390 (T,wt=22): 15426 f(x,y,f(z,y,f(u,z,f(z,v,x)))) = f(z,x,y). [para(3885(a,1),7819(a,1,3)),rewrite(2(3),3(3),2(4),2(4),8(5),2(4,R),3(4),2(5,R),3(5)),flip(a)]. given #391 (A,wt=31): 142 f(x,y,f(z,u,f(z,x,f(u,v,w)))) = f(z,x,f(x,y,f(u,v,f(z,u,w)))). [para(19(a,1),17(a,2,3)),rewrite(2(3,R),3(3),2(8,R),3(8)),flip(a)]. given #392 (F,wt=22): 15454 f(x,y,f(z,y,f(x,u,f(x,v,z)))) = f(x,z,y). [para(10436(a,1),7819(a,1,3)),rewrite(2(3),2(3),2(4),2(4),8(5),2(4,R),3(4),2(5,R),3(5)),flip(a)]. given #393 (F,wt=22): 15469 f(x,y,f(z,y,f(u,x,f(x,v,z)))) = f(x,z,y). [para(12255(a,1),7819(a,1,3)),rewrite(2(3),2(3),2(4),2(4),8(5),2(4,R),3(4),2(5,R),3(5)),flip(a)]. given #394 (T,wt=22): 15539 f(x,y,f(z,x,f(z,u,f(z,v,y)))) = f(z,x,y). [para(2(a,1),15410(a,1)),rewrite(2(4),3(4),3(5))]. given #395 (T,wt=24): 7941 f(x,y,f(x,f(z,u,v),f(z,y,u))) = f(x,y,f(z,u,v)). [back_rewrite(1095),rewrite(7721(4))]. given #396 (A,wt=31): 144 f(x,y,f(z,u,f(x,v,f(z,x,w)))) = f(z,x,f(x,y,f(z,u,f(x,v,w)))). [para(19(a,2),17(a,2,3)),rewrite(2(3,R),3(3),2(8,R),3(8)),flip(a)]. given #397 (F,wt=24): 8021 f(x,f(y,z,u),f(z,x,v)) = f(x,v,f(y,z,f(z,u,x))). [para(68(a,1),2(a,2)),rewrite(2(2),2(3),2(4),2(4))]. low water: id=13316, wt=37 given #398 (F,wt=24): 8022 f(x,f(y,z,u),f(v,z,x)) = f(v,x,f(y,z,f(z,x,u))). [para(68(a,2),2(a,2)),rewrite(2(1,R),3(1),3(3),2(5),2(5)),flip(a)]. given #399 (T,wt=24): 8106 f(x,f(y,z,u),f(z,x,v)) = f(x,v,f(y,z,f(z,x,u))). [para(68(a,2),889(a,2)),rewrite(2(1,R),3(1),2(4,R),3(4),889(7),2(5)),flip(a)]. given #400 (T,wt=24): 8454 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,x,f(z,v,u))). [para(69(a,2),1002(a,2)),rewrite(3(6),2107(10)),flip(a)]. given #401 (A,wt=31): 145 f(x,y,f(z,u,f(x,z,f(u,v,w)))) = f(x,z,f(x,y,f(u,w,f(z,u,v)))). [para(18(a,2),19(a,2,3,3))]. given #402 (F,wt=24): 8823 f(x,f(y,x,z),f(x,u,v)) = f(y,x,f(x,u,f(x,z,v))). [para(80(a,2),10(a,1)),flip(a)]. given #403 (F,wt=24): 8863 f(x,y,f(x,f(y,z,u),f(v,x,z))) = f(v,x,f(x,y,z)). [para(778(a,1),80(a,1,3)),flip(a)]. given #404 (T,wt=24): 8882 f(x,y,f(x,f(z,y,u),f(v,x,z))) = f(v,x,f(x,z,y)). [para(793(a,1),80(a,1,3)),flip(a)]. given #405 (T,wt=24): 8985 f(x,y,f(z,u,f(y,z,v))) = f(x,y,f(z,v,f(y,z,u))). [para(840(a,1),71(a,1,3,3)),rewrite(2(1),2(1),2(2,R),3(2),13(2),2(4),95(7))]. given #406 (A,wt=35): 149 f(x,y,f(x,z,f(y,u,f(x,v,f(x,y,w))))) = f(x,z,f(y,u,f(x,v,f(x,y,w)))). [para(14(a,1),19(a,1,3,3)),rewrite(3(1),3(5)),flip(a)]. given #407 (F,wt=24): 9040 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,z,y))). [para(2(a,1),84(a,1)),rewrite(2(3),2(3),3(4))]. given #408 (F,wt=24): 9101 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(x,u,f(z,x,y))). [para(84(a,1),1979(a,2)),rewrite(3(7),2(8,R),3(8),2(9,R),3(9),387(10),3(9),4638(10),2(4,R),3(4))]. given #409 (T,wt=24): 9109 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(x,y,f(z,x,u))). [para(84(a,1),3470(a,2)),rewrite(2(5,R),3(5),50(7),5808(8),2(4,R),3(4))]. given #410 (T,wt=24): 9401 f(x,y,f(z,u,f(u,x,v))) = f(x,y,f(u,x,f(z,u,v))). [para(2(a,1),98(a,1)),rewrite(2(1,R),3(1),2(3),2(3),2(5,R),3(5))]. given #411 (A,wt=31): 150 f(x,y,f(x,z,f(z,u,f(z,v,w)))) = f(x,z,f(x,y,f(z,v,f(z,u,w)))). [para(14(a,1),19(a,2,3,3)),rewrite(3(1),111(4),3(5))]. given #412 (F,wt=24): 9436 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(v,z,f(x,z,u))). [para(840(a,2),98(a,2,3)),flip(a)]. given #413 (F,wt=22): 15724 f(x,y,f(z,x,f(y,u,f(z,v,y)))) = f(z,x,y). [para(9436(a,2),67(a,2,3)),rewrite(1523(4)),flip(a)]. given #414 (T,wt=24): 10174 f(x,f(y,z,u),f(v,x,f(y,z,x))) = f(v,x,f(y,z,x)). [para(889(a,1),126(a,1,2)),rewrite(2(4,R),3(4),877(6),2(5,R),3(5)),flip(a)]. given #415 (T,wt=24): 10176 f(x,f(y,z,u),f(v,x,f(y,x,z))) = f(v,x,f(y,x,z)). [para(892(a,1),126(a,1,2)),rewrite(2(4,R),3(4),877(6),2(5,R),3(5)),flip(a)]. given #416 (A,wt=35): 151 f(x,y,f(y,z,f(x,u,f(y,v,f(x,y,w))))) = f(x,y,f(y,z,f(x,u,f(y,v,w)))). [para(19(a,2),22(a,1,3,3))]. given #417 (F,wt=24): 10177 f(x,f(y,z,x),f(u,x,f(y,z,v))) = f(u,x,f(y,z,x)). [para(999(a,1),126(a,1,2)),rewrite(2(4,R),3(4),784(6),2(5,R),3(5)),flip(a)]. given #418 (F,wt=24): 10178 f(x,f(y,x,z),f(u,x,f(y,z,v))) = f(u,x,f(y,x,z)). [para(1068(a,1),126(a,1,2)),rewrite(2(4,R),3(4),784(6),2(5,R),3(5)),flip(a)]. given #419 (T,wt=24): 10254 f(x,f(y,z,x),f(x,u,f(y,z,v))) = f(x,u,f(y,z,x)). [para(889(a,1),162(a,1,3,3)),rewrite(889(6)),flip(a)]. given #420 (T,wt=24): 10255 f(x,f(y,x,z),f(x,u,f(y,z,v))) = f(x,u,f(y,x,z)). [para(892(a,1),162(a,1,3,3)),rewrite(889(6)),flip(a)]. given #421 (A,wt=35): 153 f(x,y,f(x,z,f(y,u,f(y,v,f(x,y,w))))) = f(x,z,f(y,u,f(x,y,f(y,v,w)))). [para(22(a,1),19(a,1,3,3)),flip(a)]. given #422 (F,wt=24): 10257 f(x,f(y,z,u),f(x,v,f(y,z,x))) = f(x,v,f(y,z,x)). [para(999(a,1),162(a,1,3,3)),rewrite(8(6)),flip(a)]. given #423 (F,wt=24): 10290 f(x,f(y,z,u),f(x,v,f(z,u,x))) = f(x,v,f(z,u,x)). [para(6893(a,1),162(a,1,3,3)),rewrite(8(6)),flip(a)]. given #424 (T,wt=24): 10292 f(x,f(y,z,u),f(x,v,f(y,u,x))) = f(x,v,f(y,u,x)). [para(7129(a,1),162(a,1,3,3)),rewrite(8(6)),flip(a)]. given #425 (T,wt=24): 10473 f(x,f(y,z,u),f(z,u,f(y,z,x))) = f(z,x,f(y,z,u)). [para(163(a,1),2(a,2)),rewrite(2(2),2(2),2(4),2(6,R),3(6))]. given #426 (A,wt=31): 154 f(x,y,f(x,z,f(u,v,f(z,u,w)))) = f(x,z,f(x,y,f(z,u,f(u,v,w)))). [para(22(a,1),19(a,2,3,3)),rewrite(95(4))]. given #427 (F,wt=24): 10482 f(f(x,y,z),f(x,y,u),f(v,z,f(x,y,z))) = f(x,y,z). [para(999(a,1),163(a,1,2)),rewrite(10341(7),999(9),8(8))]. given #428 (F,wt=24): 10483 f(f(x,y,z),f(x,z,u),f(v,y,f(x,y,z))) = f(x,y,z). [para(1068(a,1),163(a,1,2)),rewrite(10341(7),1068(9),8(8))]. given #429 (T,wt=24): 10567 f(x,f(y,z,u),f(y,u,f(z,u,x))) = f(u,x,f(y,z,u)). [para(164(a,1),2(a,2)),rewrite(2(2),2(2),2(4),2(6,R),3(6))]. given #430 (T,wt=24): 10622 f(x,y,f(z,u,f(y,v,z))) = f(x,y,f(v,z,f(y,z,u))). [para(595(a,1),209(a,1,3)),rewrite(2(1,R),3(1),2(4),3(5),2(6,R),3(6),10341(6)),flip(a)]. given #431 (A,wt=31): 155 f(x,y,f(z,u,f(z,x,f(u,v,w)))) = f(x,y,f(z,x,f(u,v,f(z,u,w)))). [para(19(a,1),115(a,1,3,3)),rewrite(2(4,R),3(4),96(5),2(8,R),3(8))]. given #432 (F,wt=22): 15838 f(x,y,f(x,z,f(y,u,f(z,v,y)))) = f(x,z,y). [para(10622(a,2),23(a,2,3)),rewrite(1803(4)),flip(a)]. given #433 (F,wt=24): 10652 f(x,y,f(x,f(y,z,u),f(z,u,v))) = f(x,y,f(z,u,v)). [back_rewrite(1530),rewrite(2(1),10642(4))]. given #434 (T,wt=21): 15866 f(x,y,f(z,f(x,z,u),f(y,v,z))) = f(x,y,z). [para(1523(a,1),10652(a,1,3)),rewrite(3(2),998(3),2(4,R),6497(5)),flip(a)]. given #435 (T,wt=24): 10719 f(x,f(y,z,u),f(v,y,x)) = f(v,x,f(y,z,f(y,u,x))). [para(313(a,2),2(a,2)),rewrite(3(3),2(5)),flip(a)]. given #436 (A,wt=31): 157 f(x,y,f(z,u,f(z,v,f(x,z,w)))) = f(x,y,f(z,u,f(x,z,f(z,v,w)))). [para(115(a,1),19(a,1,3,3)),rewrite(2(2,R),3(2),2(6,R),3(6),153(9))]. given #437 (F,wt=24): 10968 f(x,f(y,z,u),f(y,v,x)) = f(v,x,f(y,z,f(y,u,x))). [para(314(a,1),2(a,2)),rewrite(2(2,R),3(2),2(3),3(4))]. given #438 (F,wt=24): 10969 f(x,f(y,x,z),f(z,u,v)) = f(y,x,f(z,u,f(x,z,v))). [para(314(a,1),3(a,1)),rewrite(2(1,R),3(1),3(4)),flip(a)]. given #439 (T,wt=24): 11087 f(x,f(x,y,z),f(u,v,w)) = f(x,y,f(x,z,f(u,v,w))). [para(11010(a,1),63(a,2,3)),rewrite(2(4),2(4),11086(6),2(6,R)),flip(a)]. given #440 (T,wt=24): 11093 f(x,f(y,z,u),f(x,v,w)) = f(x,v,f(x,w,f(y,z,u))). [para(11010(a,1),123(a,2,3)),rewrite(3(4),11086(6)),flip(a)]. given #441 (A,wt=38): 158 f(x,y,f(z,u,f(x,v,f(x,z,f(v,w,v6))))) = f(x,z,f(x,y,f(z,u,f(v,w,f(x,v,v6))))). [para(19(a,1),19(a,1,3,3))]. given #442 (F,wt=24): 11094 f(x,f(y,x,z),f(u,v,w)) = f(y,x,f(x,z,f(u,v,w))). [para(11010(a,1),213(a,1)),rewrite(3(2),3(6),2(10),3(10),11088(10),12(8)),flip(a)]. given #443 (F,wt=24): 11172 f(x,f(y,z,u),f(u,x,v)) = f(x,v,f(y,u,f(z,u,x))). [para(316(a,1),2(a,2)),rewrite(2(2,R),3(2),2(3),2(4),2(4))]. given #444 (T,wt=24): 11173 f(x,f(y,z,u),f(x,y,v)) = f(x,v,f(y,z,f(x,y,u))). [para(2(a,1),316(a,1,2)),rewrite(3(4),2(5,R),3(5))]. given #445 (T,wt=21): 16527 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(11173(a,2),10386(a,1))]. given #446 (A,wt=38): 159 f(x,y,f(z,u,f(x,v,f(z,w,f(x,z,v6))))) = f(x,z,f(x,y,f(z,u,f(x,v,f(z,w,v6))))). [para(19(a,2),19(a,1,3,3))]. given #447 (F,wt=24): 11174 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(z,u,f(x,y,z))). [para(2(a,2),316(a,1,2)),rewrite(2(5,R),3(5))]. given #448 (F,wt=24): 11175 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(y,z,f(x,z,u))). [para(316(a,2),3(a,2)),rewrite(3(1),3(3),3(4)),flip(a)]. given #449 (T,wt=24): 11180 f(x,f(y,z,u),f(x,v,u)) = f(x,v,f(y,u,f(x,z,u))). [para(316(a,2),13(a,1,3)),rewrite(3(2),15(4))]. given #450 (T,wt=24): 11204 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,u,v))). [para(14(a,1),316(a,1,2)),rewrite(3(5),12(6),11087(9),11087(8),10211(7),11160(8))]. given #451 (A,wt=38): 160 f(x,y,f(z,u,f(x,z,f(v,w,f(z,v,v6))))) = f(x,z,f(x,y,f(z,v,f(z,u,f(v,w,v6))))). [para(19(a,1),19(a,2,3,3))]. given #452 (F,wt=24): 11312 f(x,f(y,z,u),f(x,z,f(y,v,u))) = f(x,z,f(y,v,u)). [para(316(a,2),2851(a,1,2)),rewrite(3(2),11218(3),2(3),2(6))]. given #453 (F,wt=21): 16857 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(2719(a,1),11312(a,1,3)),rewrite(2(2,R),3(2),2(3),2(4),3(5),11087(5),2728(4),13(2),2(3,R),3(3),2(4)),flip(a)]. given #454 (T,wt=24): 11370 f(x,f(y,z,u),f(x,y,f(z,v,u))) = f(x,y,f(z,v,u)). [para(316(a,2),7077(a,1,3)),rewrite(2(2),2(4),11219(5),3(4),2(6))]. given #455 (T,wt=24): 11372 f(x,y,f(z,u,f(y,v,u))) = f(y,u,f(x,y,f(z,v,u))). [para(316(a,2),67(a,1,3)),rewrite(8(2),3(2),12(5))]. given #456 (A,wt=38): 161 f(x,y,f(z,u,f(x,z,f(z,v,f(u,w,v6))))) = f(x,z,f(x,y,f(z,v,f(u,w,f(z,u,v6))))). [para(19(a,2),19(a,2,3,3))]. given #457 (F,wt=22): 17062 f(x,y,f(z,u,f(x,z,f(v,z,y)))) = f(x,z,y). [para(1100(a,1),11372(a,2,3)),rewrite(2(5,R),11087(6),16110(6),2(4,R),3(4),1569(6),9979(3),15991(6),2(4,R),16314(4)),flip(a)]. given #458 (F,wt=24): 11384 f(x,y,f(x,f(y,z,u),f(x,v,u))) = f(x,v,f(x,y,u)). [para(316(a,2),69(a,2,3)),rewrite(2(2,R),3(2),11219(3),3(4),2(6,R),3(6)),flip(a)]. given #459 (T,wt=24): 11489 f(x,f(y,z,u),f(x,y,f(v,x,z))) = f(v,x,f(x,y,z)). [para(11208(a,1),34(a,1,3)),flip(a)]. given #460 (T,wt=24): 11495 f(x,y,f(x,f(y,z,u),f(x,z,v))) = f(x,v,f(x,y,z)). [para(11208(a,1),36(a,2,3)),rewrite(3(2))]. given #461 (A,wt=34): 166 f(x,f(y,z,f(x,u,v)),f(y,z,f(x,u,f(x,y,v)))) = f(x,y,f(y,z,f(x,u,v))). [para(5(a,1),21(a,1,3,3))]. given #462 (F,wt=24): 11497 f(x,f(y,z,u),f(x,y,f(z,u,v))) = f(x,y,f(z,u,v)). [para(11208(a,1),889(a,1,2)),rewrite(2(3),2(6))]. given #463 (F,wt=24): 11498 f(x,f(y,z,u),f(x,z,f(y,u,v))) = f(x,z,f(y,u,v)). [para(892(a,1),11208(a,1,2))]. given #464 (T,wt=24): 11503 f(x,y,f(x,f(z,u,y),f(z,u,v))) = f(x,y,f(z,u,v)). [para(11208(a,1),787(a,1,3,3)),rewrite(2(2),2(2),2(3,R),3(3),2(4,R),11087(4),2(6))]. given #465 (T,wt=24): 11534 f(x,f(y,z,f(u,x,z)),f(u,x,v)) = f(x,z,f(u,x,v)). [para(11208(a,1),8575(a,1,3,3)),rewrite(2(2),2(2),2(4,R),2(6))]. given #466 (A,wt=34): 170 f(x,f(y,z,f(y,u,v)),f(y,u,f(x,u,f(y,z,v)))) = f(x,u,f(y,u,f(y,z,v))). [para(9(a,2),21(a,1,2)),rewrite(2(1,R),3(1),2(5,R),3(5),2(8,R),3(8))]. given #467 (F,wt=24): 11535 f(x,f(y,z,u),f(x,z,f(v,x,y))) = f(v,x,f(x,y,z)). [para(11208(a,1),80(a,1,3)),flip(a)]. given #468 (F,wt=24): 11551 f(x,f(y,z,u),f(v,x,f(x,y,z))) = f(v,x,f(x,y,z)). [para(11208(a,1),126(a,1,2)),rewrite(2(4,R),3(4),877(6),2(5,R),3(5)),flip(a)]. given #469 (T,wt=24): 11558 f(x,f(y,z,f(u,x,y)),f(u,x,v)) = f(x,y,f(u,x,v)). [para(11208(a,1),10415(a,1,3,3)),rewrite(2(2),2(2),2(4,R),2(6))]. given #470 (T,wt=24): 11579 f(x,f(y,z,u),f(x,u,f(x,y,v))) = f(x,v,f(x,y,u)). [para(11218(a,1),26(a,2,3)),rewrite(3(2))]. given #471 (A,wt=34): 173 f(x,f(y,z,f(x,u,v)),f(y,z,f(x,v,f(x,y,u)))) = f(x,y,f(y,z,f(x,u,v))). [para(10(a,1),21(a,1,3,3))]. given #472 (F,wt=24): 11588 f(x,y,f(x,f(z,u,y),f(z,v,u))) = f(x,y,f(z,v,u)). [para(11218(a,1),787(a,1,3,3)),rewrite(2(2),2(2),2(3,R),3(3),2(4,R),11087(4),2(6))]. given #473 (F,wt=24): 11617 f(x,f(y,z,f(u,x,z)),f(u,v,x)) = f(x,z,f(u,v,x)). [para(11218(a,1),8575(a,1,3,3)),rewrite(2(2),2(2),2(4,R),2(6))]. given #474 (T,wt=24): 11630 f(x,f(y,z,f(u,x,y)),f(u,v,x)) = f(x,y,f(u,v,x)). [para(11218(a,1),10415(a,1,3,3)),rewrite(2(2),2(2),2(4,R),2(6))]. given #475 (T,wt=24): 11645 f(x,f(y,z,u),f(x,y,f(v,z,u))) = f(x,y,f(v,z,u)). [para(11249(a,1),999(a,1,3)),rewrite(2(2),3(4),2(6))]. given #476 (A,wt=38): 175 f(x,f(y,z,u),f(x,v,f(x,w,f(y,z,f(x,y,u))))) = f(x,v,f(x,w,f(x,y,f(y,z,u)))). [para(21(a,1),11(a,1,3,3)),flip(a)]. given #477 (F,wt=24): 11649 f(x,y,f(x,f(z,u,y),f(v,z,u))) = f(x,y,f(v,z,u)). [para(11249(a,1),787(a,1,3,3)),rewrite(2(2),2(2),2(3,R),3(3),2(4,R),11087(4),2(6))]. given #478 (F,wt=24): 11661 f(x,f(y,z,f(u,x,z)),f(v,u,x)) = f(x,z,f(v,u,x)). [para(11249(a,1),8575(a,1,3,3)),rewrite(2(2),2(2),2(4,R),2(6))]. given #479 (T,wt=24): 11679 f(x,f(y,z,f(u,x,y)),f(v,u,x)) = f(x,y,f(v,u,x)). [para(11249(a,1),10415(a,1,3,3)),rewrite(2(2),2(2),2(4,R),2(6))]. given #480 (T,wt=24): 11692 f(f(x,y,z),f(x,y,f(x,u,z)),f(y,z,v)) = f(x,y,z). [para(11468(a,1),889(a,1,3)),rewrite(2(5),11468(8))]. given #481 (A,wt=44): 177 f(x,f(y,z,f(x,u,f(x,v,w))),f(y,z,f(x,v,f(x,y,f(x,u,w))))) = f(x,y,f(y,z,f(x,u,f(x,v,w)))). [para(11(a,1),21(a,1,3,3))]. given #482 (F,wt=24): 11693 f(f(x,y,z),f(y,z,u),f(x,y,f(x,v,z))) = f(x,y,z). [para(11468(a,1),999(a,1,2)),rewrite(2(5,R),11468(8))]. given #483 (F,wt=24): 11746 f(x,y,f(z,x,f(u,x,v))) = f(x,y,f(x,v,f(z,u,x))). [para(11247(a,1),126(a,2,3)),rewrite(3(2),3(5),10541(6),10563(7),2(4),2(4)),flip(a)]. given #484 (T,wt=24): 11930 f(x,f(y,z,f(y,u,x)),f(y,u,f(u,x,v))) = f(y,u,x). [para(1803(a,1),11871(a,1,3,3)),rewrite(2(1,R),3(1),3(3),2(5,R),2(6,R),3(6),3(8),793(8))]. given #485 (T,wt=24): 11933 f(x,f(y,z,f(u,y,x)),f(u,y,f(u,x,v))) = f(u,y,x). [para(4973(a,1),11871(a,1,3,3)),rewrite(2(5,R),3(8),795(8))]. given #486 (A,wt=44): 179 f(x,f(y,z,f(x,u,f(x,v,w))),f(y,z,f(x,u,f(x,v,f(x,y,w))))) = f(x,y,f(y,z,f(x,u,f(x,v,w)))). [para(11(a,2),21(a,1,3,3))]. given #487 (F,wt=24): 11934 f(x,f(y,z,f(u,y,x)),f(u,v,f(u,y,x))) = f(u,y,x). [para(4995(a,1),11871(a,1,3,3)),rewrite(2(1),2(3),2(5,R),2(6),3(8),1538(8))]. given #488 (F,wt=24): 11939 f(x,f(y,z,f(y,u,x)),f(y,u,f(u,v,x))) = f(y,u,x). [para(8305(a,1),11871(a,1,3,3)),rewrite(2(5,R),3(8),3971(8))]. given #489 (T,wt=24): 11941 f(x,f(y,z,f(u,y,x)),f(u,y,f(u,v,x))) = f(u,y,x). [para(8575(a,1),11871(a,1,3,3)),rewrite(2(5,R),3(8),11468(8))]. given #490 (T,wt=21): 17623 f(x,y,f(z,f(x,u,z),f(z,y,v))) = f(x,z,y). [para(1096(a,1),11941(a,1,2,3)),rewrite(2(1),2(3),2(4),2(5,R),8(5),2(5),2(7),2(9,R),15450(11),2(5),16372(5),2(3,R),3(3),4972(4),2(3),2(4),15991(6),3(3),2(4,R)),flip(a)]. given #491 (A,wt=34): 181 f(x,f(y,z,f(z,u,v)),f(z,u,f(x,u,f(y,z,v)))) = f(x,u,f(z,u,f(y,z,v))). [para(17(a,1),21(a,1,2)),rewrite(2(1,R),3(1),2(5,R),3(5),2(8,R),3(8))]. given #492 (F,wt=21): 17628 f(x,y,f(z,f(x,u,z),f(y,z,v))) = f(x,y,z). [para(2(a,2),17623(a,1,3)),rewrite(2(2,R),3(2),2(3),3(5))]. given #493 (F,wt=22): 17638 f(x,y,f(y,z,f(z,u,f(x,v,z)))) = f(x,y,z). [para(17623(a,1),1737(a,2,3)),rewrite(2(2,R),3(2),2(3,R),3(3),12981(6),2(2),2(2),2(5,R),3(5),3(6),11208(7))]. given #494 (T,wt=22): 17647 f(x,y,f(z,y,f(u,z,f(x,z,v)))) = f(x,z,y). [para(23(a,1),181(a,1,3,3)),rewrite(795(7),3(5),11087(5),4974(4),13(2)),flip(a)]. given #495 (T,wt=24): 11991 f(x,y,f(y,f(x,z,u),f(y,z,v))) = f(y,v,f(x,y,z)). [para(892(a,1),493(a,2,3)),rewrite(3(2))]. given #496 (A,wt=34): 182 f(x,f(y,z,f(z,u,v)),f(z,v,f(x,z,f(y,z,u)))) = f(x,z,f(z,v,f(y,z,u))). [para(18(a,1),21(a,1,2))]. given #497 (F,wt=24): 12041 f(x,y,f(y,f(x,z,u),f(y,u,v))) = f(y,v,f(x,y,u)). [para(11017(a,1),493(a,2,3)),rewrite(2(1,R),3(1),3(2))]. given #498 (F,wt=21): 17796 f(x,f(y,z,f(u,v,y)),f(u,x,y)) = f(u,x,y). [para(778(a,1),12041(a,1,3)),rewrite(3(2),6530(3),2(3),2(3)),flip(a)]. given #499 (T,wt=22): 17804 f(x,y,f(z,u,f(y,z,f(x,v,z)))) = f(x,y,z). [para(1523(a,1),12041(a,1,3)),rewrite(3(2),6530(3),2(4,R),16314(4),3(6),16314(6),95(6)),flip(a)]. given #500 (T,wt=24): 12336 f(x,y,f(z,u,f(z,v,y))) = f(x,y,f(z,v,f(z,y,u))). [para(570(a,1),2(a,2)),rewrite(3(3),3(4),2(6,R),3(6)),flip(a)]. given #501 (A,wt=44): 194 f(x,f(y,z,f(u,v,f(x,u,w))),f(y,z,f(x,u,f(x,y,f(u,v,w))))) = f(x,y,f(y,z,f(u,v,f(x,u,w)))). [para(19(a,1),21(a,1,3,3))]. given #502 (F,wt=24): 12337 f(x,y,f(z,u,f(z,v,x))) = f(x,y,f(z,v,f(z,x,u))). [para(2(a,1),570(a,1)),rewrite(2(3),2(3),3(4)),flip(a)]. given #503 (F,wt=24): 12368 f(x,y,f(z,u,f(z,v,y))) = f(z,y,f(x,y,f(z,v,u))). [para(570(a,1),1979(a,2)),rewrite(3(7),2(8,R),3(8),2(9,R),3(9),5106(10),3(4),2(6,R),3(6)),flip(a)]. given #504 (T,wt=24): 12386 f(x,y,f(z,u,f(y,v,z))) = f(y,z,f(x,y,f(v,z,u))). [para(570(a,1),213(a,1,3)),rewrite(2(1),3(1),6497(3),2(4,R),3(4),13(5),2(6,R),3(6))]. given #505 (T,wt=24): 12407 f(x,y,f(y,f(x,z,u),f(y,v,u))) = f(y,v,f(x,y,u)). [para(12381(a,1),17(a,2,3)),rewrite(2(4,R),3(4),8053(4),3(2),2(6,R),3(6))]. given #506 (A,wt=44): 196 f(x,f(y,z,f(x,u,f(y,v,w))),f(y,z,f(x,u,f(y,v,f(x,y,w))))) = f(x,y,f(y,z,f(x,u,f(y,v,w)))). [para(19(a,2),21(a,1,3,3))]. given #507 (F,wt=24): 12420 f(x,f(y,z,f(x,u,y)),f(z,v,f(x,y,z))) = f(x,y,z). [para(12381(a,1),877(a,1,3,3)),rewrite(2(2,R),3(2),6497(3),3(3),2(7,R),3(7),6497(8),12402(8))]. given #508 (F,wt=24): 12513 f(x,f(y,z,u),f(x,y,v)) = f(x,v,f(y,u,f(x,y,z))). [para(669(a,1),31(a,2)),rewrite(3(2))]. given #509 (T,wt=24): 12572 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(v,u,f(x,z,u))). [para(1668(a,1),792(a,2,3)),rewrite(3(3),3(4),12553(6))]. given #510 (T,wt=24): 12652 f(x,f(y,z,u),f(z,x,f(y,x,v))) = f(x,v,f(y,z,x)). [para(792(a,1),126(a,2)),rewrite(2(2),2(3,R),3(3),2(5),2(7,R),3(7),7164(8),2(5),2(5))]. given #511 (A,wt=41): 201 f(x,y,f(z,f(x,u,f(x,v,w)),f(x,u,f(x,v,f(x,z,w))))) = f(x,y,f(x,z,f(x,u,f(x,v,w)))). [para(11(a,2),125(a,1,3,3))]. given #512 (F,wt=24): 12664 f(x,f(y,z,f(y,x,u)),f(x,u,v)) = f(y,x,f(x,u,v)). [para(792(a,1),213(a,2,3)),rewrite(2(1,R),3(1),2(2,R),3(2),3(3),2(4,R),998(6),2(3,R),3(3),3(4),2(6,R)),flip(a)]. given #513 (F,wt=24): 12708 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,u,w))). [para(72(a,1),12592(a,1,2)),rewrite(2(5,R),10779(5),998(5),13(3),11209(6)),flip(a)]. given #514 (T,wt=24): 12815 f(x,f(y,z,u),f(v,x,f(v,y,z))) = f(v,x,f(y,z,u)). [para(824(a,1),213(a,2,3)),rewrite(1508(5),12(4)),flip(a)]. given #515 (T,wt=23): 18024 f(f(x,y,z),f(u,x,y),f(u,x,z)) = f(x,z,f(u,x,y)). [para(1804(a,1),12815(a,2)),rewrite(2(5),2(5),889(6),3(5),18010(5))]. given #516 (A,wt=31): 215 f(x,y,f(x,z,f(u,v,f(x,v,w)))) = f(x,z,f(x,v,f(x,y,f(u,v,w)))). [para(23(a,1),5(a,2,3))]. given #517 (F,wt=23): 18029 f(f(x,y,z),f(u,x,y),f(u,y,z)) = f(y,z,f(u,x,y)). [para(10567(a,1),12815(a,2)),rewrite(2(5),2(5),10268(6),3(5),18011(5))]. given #518 (F,wt=18): 18175 f(x,y,f(z,x,f(u,z,y))) = f(z,x,y). [para(7167(a,1),18029(a,2)),rewrite(3(2),2(4,R),3(4),3(6),13(6),2(6),11247(6),13(3),8(3),2(3),2(5,R),3(5),16314(5),13(4)),flip(a)]. given #519 (T,wt=21): 18184 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(1462(a,1),18175(a,2)),rewrite(2(1,R),3(1),2(4,R),3(4),2(7,R),3(7),2(8,R),3(8),15453(8),11087(6),1539(6),2(5),2(5))]. given #520 (T,wt=23): 18051 f(f(x,y,z),f(x,y,u),f(x,z,u)) = f(x,y,f(x,z,u)). [para(18024(a,1),2(a,1)),rewrite(2(1,R),3(1),2(3),2(3),3(4),2(5,R),3(5)),flip(a)]. given #521 (A,wt=31): 216 f(x,y,f(z,u,f(x,v,f(x,u,w)))) = f(x,u,f(x,y,f(z,u,f(x,v,w)))). [para(5(a,1),23(a,1,3,3))]. given #522 (F,wt=23): 18052 f(f(x,y,z),f(x,y,u),f(y,z,u)) = f(y,u,f(x,y,z)). [para(18024(a,1),2(a,2))]. given #523 (F,wt=23): 18053 f(f(x,y,z),f(y,z,u),f(x,y,u)) = f(x,y,f(y,z,u)). [para(2(a,1),18024(a,1,1)),rewrite(2(2),2(2),2(3),3(3),2(5),2(5),2(6,R),3(6))]. given #524 (T,wt=23): 18054 f(f(x,y,z),f(x,z,u),f(y,z,u)) = f(y,z,f(x,z,u)). [para(2(a,2),18024(a,1,1)),rewrite(2(2),3(2),2(3),3(3),2(5),3(5),2(6,R),3(6))]. given #525 (T,wt=23): 18055 f(f(x,y,z),f(x,y,u),f(x,u,z)) = f(x,y,f(x,u,z)). [para(18024(a,1),3(a,1)),rewrite(2(1,R),3(1),3(3),2(4),2(4),2(5,R),3(5)),flip(a)]. given #526 (A,wt=31): 217 f(x,y,f(z,u,f(x,u,f(z,v,w)))) = f(x,u,f(x,y,f(z,v,f(z,u,w)))). [para(5(a,1),23(a,2,3,3))]. given #527 (F,wt=23): 18056 f(f(x,y,z),f(x,z,u),f(x,y,u)) = f(x,z,f(x,y,u)). [para(18024(a,1),3(a,2)),rewrite(2(2),2(2),2(3),2(3),2(5),2(5))]. given #528 (F,wt=23): 18090 f(f(x,y,z),f(u,x,z),f(u,x,y)) = f(x,y,f(u,x,z)). [para(18024(a,1),889(a,2)),rewrite(3(2),2(4),3(5),1099(9))]. given #529 (T,wt=23): 18133 f(f(x,y,z),f(y,z,u),f(x,z,u)) = f(x,z,f(y,z,u)). [para(2(a,1),18029(a,1,1)),rewrite(2(2),2(2),2(3),3(3),2(5),2(5),2(6,R),3(6))]. given #530 (T,wt=23): 18167 f(f(x,y,z),f(x,u,z),f(x,y,u)) = f(x,y,f(x,u,z)). [para(18029(a,1),11010(a,1,1)),rewrite(2(1),2(4),2(4),2(5),2(6),2(6),18129(8),11010(6),2(3),2(3),2(4),2(5),2(5)),flip(a)]. given #531 (A,wt=31): 220 f(x,y,f(z,u,f(u,v,f(x,u,w)))) = f(x,u,f(x,y,f(z,u,f(u,v,w)))). [para(9(a,2),23(a,1,3,3))]. given #532 (F,wt=23): 18170 f(f(x,y,z),f(x,y,u),f(y,u,z)) = f(y,u,f(x,y,z)). [para(18029(a,1),12402(a,2)),rewrite(2(2),2(2),2(3),2(3),2(4),2(4),2(6),2(6),2(7,R),15406(9),2(5),2(5))]. given #533 (F,wt=23): 18199 f(f(x,y,z),f(x,u,y),f(x,u,z)) = f(x,u,f(x,y,z)). [para(18051(a,1),2(a,1)),flip(a)]. given #534 (T,wt=23): 18238 f(f(x,y,z),f(x,u,z),f(x,u,y)) = f(x,u,f(x,y,z)). [para(18052(a,1),3(a,1)),rewrite(2(1,R),3(1),2(3,R),3(3),3(4),2(5),2(5)),flip(a)]. given #535 (T,wt=23): 18272 f(f(x,y,z),f(y,u,z),f(x,y,u)) = f(x,y,f(y,u,z)). [para(18053(a,1),889(a,2)),rewrite(3(3),2(4),3(6),1099(9),3(5))]. given #536 (A,wt=31): 221 f(x,y,f(z,u,f(x,u,f(u,v,w)))) = f(x,u,f(x,y,f(u,v,f(z,u,w)))). [para(9(a,2),23(a,2,3,3))]. given #537 (F,wt=23): 18290 f(f(x,y,z),f(x,u,y),f(u,y,z)) = f(u,y,f(x,y,z)). [para(18054(a,1),12(a,1,3)),rewrite(18012(5),18054(8))]. given #538 (F,wt=24): 12874 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(z,y,f(x,y,v))). [para(832(a,1),2(a,2)),rewrite(3(3),2(4,R),3(4))]. given #539 (T,wt=24): 12958 f(x,y,f(x,f(z,y,u),f(x,v,u))) = f(x,v,f(x,y,u)). [para(12(a,1),990(a,1,3,3)),rewrite(8(3),11087(7),11179(6),3(4)),flip(a)]. given #540 (T,wt=24): 12968 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,v,u))). [para(496(a,1),990(a,2,3,3)),rewrite(2(1,R),3(1),2(3,R),3(3),11087(6),11087(5),10211(4),11160(5),2(4,R),3(4),2(7,R),3(7),11427(9))]. given #541 (A,wt=31): 222 f(x,y,f(x,z,f(u,v,f(x,v,w)))) = f(x,z,f(x,y,f(x,v,f(u,v,w)))). [para(23(a,2),10(a,1,3)),rewrite(50(8))]. given #542 (F,wt=24): 12982 f(x,y,f(x,f(z,u,y),f(x,v,u))) = f(x,v,f(x,u,y)). [para(68(a,2),990(a,2,3)),rewrite(13(3),8(3),11087(7),43(7)),flip(a)]. given #543 (F,wt=24): 13020 f(x,y,f(x,f(z,u,v),f(z,u,y))) = f(x,y,f(z,u,v)). [para(2(a,1),1059(a,1)),rewrite(2(2),2(2),2(4),2(4))]. given #544 (T,wt=24): 13022 f(x,f(y,z,u),f(x,v,f(v,y,z))) = f(x,v,f(y,z,u)). [para(1059(a,1),5(a,1)),flip(a)]. given #545 (T,wt=24): 13023 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))). [para(5(a,1),1059(a,1,3,2)),rewrite(2805(5))]. given #546 (A,wt=31): 223 f(x,y,f(z,u,f(x,u,f(z,v,w)))) = f(x,u,f(x,y,f(z,w,f(z,u,v)))). [para(10(a,1),23(a,2,3,3))]. given #547 (F,wt=24): 13034 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,w,u))). [para(18(a,1),1059(a,1,3,2)),rewrite(2890(5)),flip(a)]. given #548 (F,wt=24): 13036 f(x,f(y,z,u),f(y,v,f(x,z,v))) = f(x,v,f(y,z,u)). [para(1059(a,1),19(a,2)),rewrite(3(2),2(3,R),3(3))]. given #549 (T,wt=24): 13075 f(x,f(y,z,u),f(v,y,f(x,v,z))) = f(x,v,f(y,z,u)). [para(1059(a,1),47(a,2,3)),rewrite(88(5),13(7))]. given #550 (T,wt=24): 13099 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,u,f(x,y,z))). [para(68(a,2),1059(a,1,3)),rewrite(3(3),3(4),22(4),3(2),11495(5),3(5))]. given #551 (A,wt=38): 224 f(x,y,f(x,z,f(x,u,f(v,w,f(x,w,v6))))) = f(x,w,f(x,y,f(x,z,f(x,u,f(v,w,v6))))). [para(23(a,2),11(a,1,3,3))]. given #552 (F,wt=24): 13105 f(x,f(y,z,u),f(z,v,f(x,y,v))) = f(x,v,f(y,z,u)). [para(1059(a,1),75(a,2)),rewrite(3(2),2(3,R),3(3))]. given #553 (F,wt=24): 13128 f(x,f(y,z,u),f(y,x,f(z,u,v))) = f(y,x,f(z,u,v)). [para(1059(a,1),162(a,1,3)),rewrite(2(3,R),3(3),2(5,R),3(5),8(6),2(5,R),3(5)),flip(a)]. given #554 (T,wt=21): 18588 f(x,f(y,z,x),f(y,u,f(y,v,z))) = f(y,z,x). [para(11884(a,1),13128(a,1,3)),rewrite(2(3,R),8(3),3(3),2(4,R),3(7),10282(8))]. given #555 (T,wt=24): 13325 f(f(x,y,z),f(x,u,y),f(x,u,f(u,y,v))) = f(x,u,y). [para(1060(a,1),2(a,1)),flip(a)]. given #556 (A,wt=38): 225 f(x,y,f(x,z,f(x,u,f(v,w,f(x,w,v6))))) = f(x,u,f(x,y,f(x,w,f(x,z,f(v,w,v6))))). [para(23(a,1),11(a,2,3,3))]. given #557 (F,wt=24): 13326 f(f(x,y,z),f(y,z,f(x,z,u)),f(x,y,v)) = f(x,y,z). [para(2(a,1),1060(a,1,1)),rewrite(2(2,R),3(2),2(4,R),3(4),2(6))]. given #558 (F,wt=24): 13327 f(f(x,y,z),f(x,y,u),f(x,u,f(y,u,v))) = f(x,y,u). [para(2(a,1),1060(a,1)),rewrite(3(2),2(3,R),3(3),3(6))]. given #559 (T,wt=24): 13328 f(f(x,y,z),f(x,z,f(x,y,u)),f(y,z,v)) = f(x,y,z). [para(2(a,2),1060(a,1,1)),rewrite(2(3,R),3(3),2(4,R),3(4),2(6),2(6))]. given #560 (T,wt=24): 13329 f(f(x,y,z),f(x,z,f(y,z,u)),f(x,y,v)) = f(x,y,z). [para(3(a,1),1060(a,1,1)),rewrite(2(2,R),3(2),3(6))]. given #561 (A,wt=38): 226 f(x,y,f(z,u,f(x,v,f(x,u,f(x,w,v6))))) = f(x,u,f(x,y,f(z,u,f(x,w,f(x,v,v6))))). [para(11(a,1),23(a,1,3,3))]. given #562 (F,wt=24): 13332 f(f(x,y,z),f(y,z,f(x,y,u)),f(x,z,v)) = f(x,y,z). [para(9(a,2),1060(a,1,2))]. given #563 (F,wt=24): 13336 f(f(x,y,z),f(y,u,f(x,y,z)),f(x,z,v)) = f(x,y,z). [para(18(a,2),1060(a,1,2))]. given #564 (T,wt=24): 13447 f(x,f(y,z,u),f(u,x,f(y,z,v))) = f(u,x,f(y,z,v)). [para(1067(a,1),2(a,2)),rewrite(2(3,R),3(3),2(4),2(6,R),3(6))]. given #565 (T,wt=24): 13541 f(f(x,y,z),f(z,u,f(x,y,z)),f(x,y,v)) = f(x,y,z). [para(1096(a,1),2(a,1)),rewrite(2(6)),flip(a)]. given #566 (A,wt=38): 227 f(x,y,f(z,u,f(x,v,f(x,w,f(x,u,v6))))) = f(x,u,f(x,y,f(z,u,f(x,v,f(x,w,v6))))). [para(11(a,2),23(a,1,3,3))]. given #567 (F,wt=24): 13555 f(f(x,y,z),f(x,y,u),f(y,u,f(x,u,v))) = f(x,y,u). [para(1661(a,1),1096(a,1,3))]. given #568 (F,wt=24): 13645 f(x,f(y,z,u),f(v,x,f(x,z,u))) = f(v,x,f(x,z,u)). [para(1100(a,1),67(a,1,3)),rewrite(11249(3),11249(6)),flip(a)]. given #569 (T,wt=24): 13654 f(x,f(y,z,u),f(v,x,f(v,z,u))) = f(v,x,f(y,z,u)). [para(1100(a,1),213(a,2,3)),rewrite(1510(5),12(4)),flip(a)]. given #570 (T,wt=24): 13663 f(x,f(y,z,u),f(u,x,f(z,x,v))) = f(x,v,f(z,u,x)). [para(1136(a,1),2(a,2)),rewrite(2(2,R),3(2),2(3,R),3(3),2(4),2(5),2(5))]. given #571 (A,wt=38): 228 f(x,y,f(z,u,f(x,u,f(z,v,f(z,w,v6))))) = f(x,u,f(x,y,f(z,w,f(z,u,f(z,v,v6))))). [para(11(a,1),23(a,2,3,3))]. given #572 (F,wt=24): 13703 f(x,f(y,z,f(y,u,x)),f(v,u,x)) = f(y,x,f(v,u,x)). [para(1136(a,1),67(a,2,3)),rewrite(2(4,R),3971(6),2(6,R)),flip(a)]. given #573 (F,wt=24): 13706 f(x,f(y,z,x),f(x,u,f(v,y,z))) = f(x,u,f(y,z,x)). [para(72(a,1),1136(a,1)),rewrite(2(3,R),3(3),2(4,R),3(4),13663(5),2(4,R),11087(4),6893(3),2(4),2(4),2(5),2(5),3(6)),flip(a)]. low water: id=16936, wt=36 given #574 (T,wt=24): 13709 f(x,y,f(x,f(z,u,y),f(x,u,v))) = f(x,v,f(x,u,y)). [para(1136(a,1),123(a,2,3)),rewrite(15(6),1100(8))]. given #575 (T,wt=22): 18830 f(x,y,f(x,z,f(z,u,f(y,v,z)))) = f(x,y,z). [para(1523(a,1),13709(a,1,3)),rewrite(2(1),3(2),998(3),2(2),2(4,R),16314(4),3(5),3(6),11087(6),22(5)),flip(a)]. given #576 (A,wt=38): 229 f(x,y,f(z,u,f(x,u,f(z,v,f(z,w,v6))))) = f(x,u,f(x,y,f(z,v,f(z,w,f(z,u,v6))))). [para(11(a,2),23(a,2,3,3))]. given #577 (F,wt=24): 13718 f(x,f(y,z,x),f(u,v,f(u,z,x))) = f(u,x,f(y,z,x)). [para(1136(a,1),213(a,2,3)),rewrite(793(6)),flip(a)]. given #578 (F,wt=24): 13795 f(x,y,f(x,f(z,u,v),f(u,v,y))) = f(x,y,f(z,u,v)). [para(2(a,1),1175(a,1)),rewrite(2(2),2(2),2(4),2(4))]. given #579 (T,wt=24): 13796 f(x,f(y,z,u),f(x,v,f(v,z,u))) = f(x,v,f(y,z,u)). [para(1175(a,1),5(a,1)),flip(a)]. given #580 (T,wt=24): 13811 f(x,f(y,z,u),f(z,v,f(x,u,v))) = f(x,v,f(y,z,u)). [para(1175(a,1),19(a,2)),rewrite(3(2),2(3,R),3(3))]. given #581 (A,wt=31): 230 f(x,y,f(z,u,f(z,x,f(v,u,w)))) = f(z,x,f(x,y,f(v,u,f(z,u,w)))). [para(23(a,1),17(a,2,3)),rewrite(2(3,R),3(3),2(8,R),3(8)),flip(a)]. given #582 (F,wt=24): 13826 f(x,f(y,z,u),f(x,u,f(v,y,z))) = f(x,u,f(v,y,z)). [para(1175(a,1),877(a,1,3,3)),rewrite(2(2),2(2),11087(7),1569(7),2(6),2(6),13795(8))]. given #583 (F,wt=24): 13830 f(x,f(y,z,u),f(v,z,f(x,v,u))) = f(x,v,f(y,z,u)). [para(1175(a,1),47(a,2,3)),rewrite(88(5),13(7))]. given #584 (T,wt=24): 13857 f(x,f(y,z,u),f(u,v,f(x,z,v))) = f(x,v,f(y,z,u)). [para(1175(a,1),75(a,2)),rewrite(3(2),2(3,R),3(3))]. given #585 (T,wt=24): 13867 f(x,y,f(x,f(y,z,u),f(v,z,u))) = f(x,y,f(v,z,u)). [para(1175(a,1),214(a,2,3)),rewrite(2(4,R),12(5),2(8,R),3(8),12(8))]. given #586 (A,wt=31): 233 f(x,y,f(z,u,f(x,u,f(u,v,w)))) = f(x,u,f(x,y,f(u,w,f(z,u,v)))). [para(18(a,2),23(a,2,3,3))]. given #587 (F,wt=24): 13904 f(x,f(y,z,u),f(y,x,f(z,x,v))) = f(x,v,f(y,z,x)). [para(1179(a,1),126(a,2)),rewrite(2(2),2(3,R),3(3),2(5),2(7,R),3(7),7164(8),2(5),2(5))]. given #588 (F,wt=24): 13914 f(f(x,y,z),f(y,z,u),f(y,u,f(z,u,v))) = f(y,z,u). [para(840(a,1),1184(a,1,3))]. given #589 (T,wt=24): 13917 f(f(x,y,z),f(y,z,u),f(z,u,f(y,u,v))) = f(y,z,u). [para(1661(a,1),1184(a,1,3))]. given #590 (T,wt=24): 13980 f(f(x,y,z),f(x,y,u),f(y,z,f(x,z,v))) = f(x,y,z). [para(2(a,1),1337(a,1,1)),rewrite(2(2,R),3(2),2(3,R),3(3),2(6))]. given #591 (A,wt=35): 238 f(x,y,f(x,z,f(u,y,f(x,v,f(x,y,w))))) = f(x,z,f(u,y,f(x,v,f(x,y,w)))). [para(14(a,1),23(a,1,3,3)),rewrite(3(1),3(5)),flip(a)]. given #592 (F,wt=24): 13981 f(f(x,y,z),f(y,z,u),f(x,z,f(x,y,v))) = f(x,y,z). [para(2(a,2),1337(a,1,1)),rewrite(2(2,R),3(2),2(4,R),3(4),2(6),2(6))]. given #593 (F,wt=24): 13982 f(f(x,y,z),f(x,y,u),f(x,z,f(y,z,v))) = f(x,y,z). [para(3(a,1),1337(a,1,1)),rewrite(2(3,R),3(3),3(6))]. given #594 (T,wt=24): 13983 f(f(x,y,z),f(x,z,u),f(y,z,f(x,y,v))) = f(x,y,z). [para(9(a,2),1337(a,1,3))]. given #595 (T,wt=24): 14364 f(x,f(y,z,u),f(v,x,u)) = f(v,x,f(y,u,f(x,z,u))). [para(316(a,2),1491(a,1,3)),rewrite(10429(5))]. given #596 (A,wt=35): 241 f(x,y,f(x,z,f(u,y,f(y,v,f(x,y,w))))) = f(x,z,f(u,y,f(x,y,f(y,v,w)))). [para(22(a,1),23(a,1,3,3)),flip(a)]. given #597 (F,wt=24): 14405 f(x,y,f(z,u,f(v,u,w))) = f(x,y,f(v,u,f(z,u,w))). [para(9(a,1),1495(a,2,3)),rewrite(2(4,R),3(4),7420(6),2(4,R),3(4))]. given #598 (F,wt=24): 14420 f(x,y,f(z,u,f(v,w,z))) = f(x,y,f(v,z,f(w,z,u))). [para(808(a,1),1495(a,2,3)),rewrite(2(4,R),3(4),7420(6),2(4)),flip(a)]. given #599 (T,wt=24): 14422 f(x,y,f(z,u,f(v,w,u))) = f(x,y,f(v,u,f(z,w,u))). [para(840(a,1),1495(a,2,3)),rewrite(2(4,R),3(4),7420(6),2(4))]. given #600 (T,wt=24): 14426 f(x,y,f(z,u,f(v,w,u))) = f(x,y,f(w,u,f(z,v,u))). [para(1661(a,1),1495(a,2,3)),rewrite(2(4,R),3(4),7420(6),2(4))]. given #601 (A,wt=31): 245 f(x,y,f(x,z,f(u,y,f(y,v,w)))) = f(x,y,f(x,z,f(y,v,f(u,y,w)))). [para(115(a,1),23(a,2,3,3)),rewrite(2(2,R),3(2),242(5),2(6,R),3(6))]. given #602 (F,wt=24): 14436 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,u,f(x,y,z))). [para(98(a,1),1495(a,1,3)),rewrite(2(3),2(3),3274(5),13(5),11999(5),2(5,R),3(5))]. given #603 (F,wt=24): 14518 f(x,f(y,z,u),f(v,y,f(v,x,z))) = f(v,x,f(y,z,u)). [para(1508(a,1),124(a,2,3)),rewrite(96(5),13(7))]. given #604 (T,wt=24): 14544 f(x,f(y,z,u),f(v,z,f(v,x,u))) = f(v,x,f(y,z,u)). [para(1510(a,1),124(a,2,3)),rewrite(96(5),13(7))]. given #605 (T,wt=24): 14762 f(x,f(y,z,u),f(u,x,v)) = f(x,v,f(z,u,f(y,u,x))). [para(1693(a,1),2(a,2)),rewrite(2(2,R),3(2),2(3),2(4),2(4))]. given #606 (A,wt=38): 246 f(x,y,f(z,u,f(x,z,f(v,w,f(z,w,v6))))) = f(x,z,f(x,y,f(z,w,f(z,u,f(v,w,v6))))). [para(23(a,1),19(a,2,3,3))]. given #607 (F,wt=24): 14763 f(x,f(y,z,u),f(x,v,u)) = f(x,v,f(z,u,f(x,y,u))). [para(1693(a,2),13(a,1,3)),rewrite(3(2),15(4))]. given #608 (F,wt=24): 14793 f(x,y,f(z,u,f(y,v,u))) = f(x,y,f(y,u,f(v,z,u))). [para(1693(a,1),162(a,1,3)),rewrite(3(2),2(5,R),3(5),14780(6),3(5),2(6,R),3(6))]. given #609 (T,wt=24): 14804 f(x,f(y,z,u),f(v,z,f(x,v,y))) = f(x,v,f(y,z,u)). [para(1067(a,1),1693(a,1)),rewrite(3(4),2(5,R),3(5)),flip(a)]. given #610 (T,wt=24): 14805 f(x,f(y,z,u),f(v,x,u)) = f(v,x,f(z,u,f(x,y,u))). [para(1693(a,2),1491(a,1,3)),rewrite(10429(5))]. given #611 (A,wt=38): 248 f(x,y,f(z,u,f(x,v,f(x,u,f(v,w,v6))))) = f(x,u,f(x,y,f(z,u,f(v,w,f(x,v,v6))))). [para(19(a,1),23(a,1,3,3))]. given #612 (F,wt=24): 14845 f(x,f(y,z,x),f(u,f(v,y,z),f(y,z,x))) = f(y,z,x). [para(1510(a,1),1698(a,1,3)),rewrite(2(2),2(2),2(3),2(5),2(5),1099(6),1(6),2(5),3(5),2(7),2(7),1099(8))]. given #613 (F,wt=21): 19153 f(x,y,f(z,y,f(u,x,y))) = f(z,y,f(u,x,y)). [para(979(a,1),14845(a,1,3)),rewrite(3(2),3(4),3(7),2(8),1(8),3(4)),flip(a)]. given #614 (T,wt=22): 19150 f(x,y,f(z,u,f(x,u,f(v,u,y)))) = f(x,u,y). [para(14845(a,1),3(a,2)),rewrite(2(2),2(4),3(5),11087(5),15989(5),2(3,R),3(3),2(5))]. given #615 (T,wt=24): 14880 f(x,f(y,z,u),f(v,x,f(z,u,x))) = f(v,x,f(z,u,x)). [para(6893(a,1),1804(a,1,3,3)),rewrite(8(6)),flip(a)]. given #616 (A,wt=38): 250 f(x,y,f(z,u,f(x,v,f(u,w,f(x,u,v6))))) = f(x,u,f(x,y,f(z,u,f(x,v,f(u,w,v6))))). [para(19(a,2),23(a,1,3,3))]. given #617 (F,wt=24): 14881 f(x,f(y,z,u),f(v,x,f(y,u,x))) = f(v,x,f(y,u,x)). [para(7129(a,1),1804(a,1,3,3)),rewrite(8(6)),flip(a)]. given #618 (F,wt=24): 14885 f(x,f(y,z,u),f(v,x,f(y,z,v))) = f(v,x,f(y,z,u)). [para(1491(a,1),1804(a,1,3)),rewrite(2(2),2(2),889(6),2(4),2(4)),flip(a)]. given #619 (T,wt=24): 14886 f(x,f(y,z,u),f(v,x,f(z,u,v))) = f(v,x,f(y,z,u)). [para(1495(a,1),1804(a,1,3)),rewrite(2(2),2(2),889(6),2(4),2(4)),flip(a)]. given #620 (T,wt=24): 14890 f(f(x,y,z),f(u,x,y),f(z,v,f(x,y,z))) = f(x,y,z). [para(1664(a,1),1876(a,1,2)),rewrite(2(3,R),6893(3),2(4,R),8(4),3(4),2(8,R),6893(8))]. given #621 (A,wt=38): 251 f(x,y,f(z,u,f(x,u,f(v,w,f(z,v,v6))))) = f(x,u,f(x,y,f(z,v,f(z,u,f(v,w,v6))))). [para(19(a,1),23(a,2,3,3))]. given #622 (F,wt=24): 14892 f(f(x,y,z),f(z,u,f(x,y,z)),f(v,x,y)) = f(x,y,z). [para(1664(a,1),1881(a,1,3)),rewrite(2(3,R),6893(3),3(3),2(6,R),8(6),2(8,R),6893(8))]. given #623 (F,wt=24): 14918 f(x,f(y,z,u),f(v,x,f(x,y,u))) = f(v,x,f(x,y,u)). [para(2060(a,1),67(a,1,3)),rewrite(11218(3),11218(6)),flip(a)]. given #624 (T,wt=24): 14925 f(x,f(y,z,u),f(v,x,f(v,y,u))) = f(v,x,f(y,z,u)). [para(2060(a,1),213(a,2,3)),rewrite(7161(5),12(4)),flip(a)]. given #625 (T,wt=24): 14951 f(x,y,f(x,f(z,u,v),f(z,v,y))) = f(x,y,f(z,u,v)). [para(2(a,1),4713(a,1)),rewrite(2(2),2(2),2(4),2(4))]. given #626 (A,wt=38): 253 f(x,y,f(z,u,f(x,u,f(z,v,f(u,w,v6))))) = f(x,u,f(x,y,f(z,v,f(u,w,f(z,u,v6))))). [para(19(a,2),23(a,2,3,3))]. given #627 (F,wt=24): 14952 f(x,f(y,z,u),f(x,v,f(v,y,u))) = f(x,v,f(y,z,u)). [para(4713(a,1),5(a,1)),flip(a)]. given #628 (F,wt=24): 14960 f(x,f(y,z,u),f(y,v,f(x,u,v))) = f(x,v,f(y,z,u)). [para(4713(a,1),19(a,2)),rewrite(3(2),2(3,R),3(3))]. given #629 (T,wt=24): 14974 f(x,f(y,z,u),f(x,u,f(y,v,z))) = f(x,u,f(y,v,z)). [para(4713(a,1),877(a,1,3,3)),rewrite(2(2),2(2),11087(7),14772(6),3(5),12843(7),2(6),2(6),14951(8))]. given #630 (T,wt=24): 14978 f(x,f(y,z,u),f(v,y,f(x,v,u))) = f(x,v,f(y,z,u)). [para(4713(a,1),47(a,2,3)),rewrite(88(5),13(7))]. given #631 (A,wt=44): 254 f(x,f(y,z,f(u,v,f(x,v,w))),f(y,z,f(x,v,f(x,y,f(u,v,w))))) = f(x,y,f(y,z,f(u,v,f(x,v,w)))). [para(23(a,1),21(a,1,3,3))]. given #632 (F,wt=24): 14983 f(x,f(y,z,u),f(u,v,f(x,y,v))) = f(x,v,f(y,z,u)). [para(4713(a,1),75(a,2)),rewrite(3(2),2(3,R),3(3))]. low water: id=17411, wt=35 given #633 (F,wt=24): 14988 f(x,y,f(x,f(y,z,u),f(z,v,u))) = f(x,y,f(z,v,u)). [para(4713(a,1),214(a,2,3)),rewrite(2(4,R),12(5),2(8,R),3(8),12(8))]. given #634 (T,wt=24): 15010 f(x,f(y,z,x),f(u,f(y,v,z),f(y,z,x))) = f(y,z,x). [para(4713(a,1),1746(a,1,3)),rewrite(2(2),2(2),2(3),2(5),2(5),10268(6),1(6),2(5),3(5),2(7),2(7),10268(8))]. given #635 (T,wt=24): 15012 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(x,y,f(z,y,v))). [para(4796(a,1),2(a,2)),rewrite(3(3),2(5,R),3(5))]. given #636 (A,wt=38): 260 f(x,y,f(z,u,f(x,u,f(v,w,f(z,w,v6))))) = f(x,u,f(x,y,f(z,w,f(z,u,f(v,w,v6))))). [para(23(a,1),23(a,2,3,3))]. given #637 (F,wt=24): 15028 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(z,y,f(x,y,u))). [para(5110(a,1),2(a,2)),rewrite(3(3),2(4,R),3(4))]. given #638 (F,wt=24): 15046 f(x,y,f(z,y,f(y,u,v))) = f(z,y,f(y,v,f(x,y,u))). [para(5154(a,1),2(a,2)),rewrite(3(3),2(4,R),3(4))]. given #639 (T,wt=24): 15056 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(y,v,f(x,z,y))). [para(5160(a,1),2(a,2)),rewrite(3(3),2(4))]. given #640 (T,wt=24): 15074 f(x,y,f(x,f(z,u,y),f(x,v,z))) = f(x,v,f(x,z,y)). [para(316(a,2),5160(a,1,3)),rewrite(2(2),11219(3),2(4),2(4)),flip(a)]. given #641 (A,wt=31): 262 f(x,f(y,z,u),f(x,v,f(x,w,y))) = f(x,v,f(x,w,f(y,z,f(x,y,u)))). [para(9(a,2),25(a,1,3,3)),flip(a)]. given #642 (F,wt=24): 15101 f(x,f(y,z,f(z,x,u)),f(x,u,v)) = f(z,x,f(x,u,v)). [para(6371(a,1),2(a,2)),rewrite(2(1),2(3),2(3),2(4),2(5),2(5),2(6,R),3(6))]. given #643 (F,wt=24): 15103 f(x,f(y,z,u),f(x,u,f(x,v,y))) = f(x,u,f(x,v,y)). [para(6371(a,1),12(a,2)),rewrite(2(1,R),3(1),2(4,R),3(4),13723(5),2(2,R),3(2),14(6),2(5,R),3(5))]. given #644 (T,wt=24): 15143 f(x,y,f(z,u,f(z,y,v))) = f(z,y,f(x,y,f(z,v,u))). [para(6676(a,2),2(a,2)),rewrite(3(3),2(4,R),3(4)),flip(a)]. given #645 (T,wt=24): 15168 f(x,y,f(y,f(z,x,u),f(z,y,v))) = f(y,v,f(z,x,y)). [para(792(a,1),6778(a,1,3)),rewrite(2(2),2(3),2(4),2(4),12651(6),2(6),2(7),12652(8))]. given #646 (A,wt=38): 263 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,v6,f(x,y,f(x,z,f(x,u,f(x,v,w))))). [para(25(a,2),11(a,1,3,3))]. given #647 (F,wt=24): 15185 f(f(x,y,z),f(x,z,u),f(x,u,f(z,u,v))) = f(x,z,u). [para(840(a,1),7141(a,1,3))]. given #648 (F,wt=24): 15187 f(f(x,y,z),f(x,z,u),f(z,u,f(x,u,v))) = f(x,z,u). [para(1661(a,1),7141(a,1,3))]. given #649 (T,wt=24): 15224 f(f(x,y,z),f(x,u,y),f(z,v,f(x,y,z))) = f(x,y,z). [para(7152(a,1),1876(a,1,2)),rewrite(2(3,R),7129(3),2(4,R),8(4),3(4),2(8,R),7129(8))]. given #650 (T,wt=24): 15225 f(f(x,y,z),f(z,u,f(x,y,z)),f(x,v,y)) = f(x,y,z). [para(7152(a,1),1881(a,1,3)),rewrite(2(3,R),7129(3),3(3),2(6,R),8(6),2(8,R),7129(8))]. given #651 (A,wt=38): 264 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,u,f(x,y,f(x,v6,f(x,z,f(x,v,w))))). [para(25(a,1),11(a,2,3,3))]. given #652 (F,wt=24): 15234 f(x,f(y,z,u),f(v,y,f(v,x,u))) = f(v,x,f(y,z,u)). [para(7161(a,1),124(a,2,3)),rewrite(96(5),13(7))]. given #653 (F,wt=24): 15253 f(x,f(y,z,u),f(v,x,f(y,u,v))) = f(v,x,f(y,z,u)). [para(7161(a,1),7164(a,1,3)),rewrite(2(2),2(2),889(6),2(4),2(4)),flip(a)]. given #654 (T,wt=24): 15271 f(x,y,f(x,z,f(y,u,v))) = f(x,z,f(x,y,f(z,u,v))). [back_rewrite(12932),rewrite(15268(4),15268(7))]. given #655 (T,wt=23): 19473 f(x,f(y,z,u),f(x,v,y)) = f(x,f(v,z,u),f(x,v,y)). [para(15271(a,1),1136(a,1,3)),rewrite(16805(5)),flip(a)]. given #656 (A,wt=31): 265 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,u,f(x,w,f(x,y,f(x,z,v)))). [para(25(a,1),11(a,2,3))]. given #657 (F,wt=23): 19570 f(x,f(y,z,u),f(x,v,u)) = f(x,f(v,y,z),f(x,v,u)). [para(19473(a,1),2(a,1)),rewrite(2(5),2(5),2(6,R)),flip(a)]. given #658 (F,wt=23): 19571 f(x,f(y,z,u),f(v,x,u)) = f(x,f(v,y,z),f(v,x,u)). [para(19473(a,1),2(a,2)),rewrite(2(2),2(3),2(4),2(4),2(5)),flip(a)]. given #659 (T,wt=23): 19572 f(x,f(y,z,u),f(x,v,u)) = f(x,f(y,v,z),f(x,v,u)). [para(2(a,1),19473(a,1,2)),rewrite(3(2),2(4),3(4),3(5)),flip(a)]. given #660 (T,wt=23): 19573 f(x,f(y,z,u),f(x,v,u)) = f(x,f(y,z,v),f(x,v,u)). [para(2(a,2),19473(a,1,2)),rewrite(3(2),2(4),2(4),3(5)),flip(a)]. given #661 (A,wt=31): 266 f(x,y,f(z,u,f(z,x,f(z,v,w)))) = f(z,x,f(x,y,f(z,v,f(z,w,u)))). [para(25(a,1),17(a,2,3)),rewrite(2(3,R),3(3),2(8,R),3(8)),flip(a)]. given #662 (F,wt=23): 19793 f(x,f(y,z,u),f(v,x,u)) = f(x,f(y,z,v),f(v,x,u)). [para(19570(a,1),2(a,2)),rewrite(2(2),2(3),2(4),2(4),2(5)),flip(a)]. given #663 (F,wt=23): 19906 f(x,f(y,z,u),f(v,u,x)) = f(x,f(y,z,v),f(v,u,x)). [para(19571(a,1),2(a,2)),rewrite(2(2),2(3),2(4),2(4),2(5)),flip(a)]. given #664 (T,wt=23): 19907 f(x,f(y,z,u),f(v,x,y)) = f(x,f(v,z,u),f(v,x,y)). [para(2(a,1),19571(a,1)),rewrite(2(2),2(3,R))]. given #665 (T,wt=23): 19933 f(x,f(y,z,u),f(v,x,u)) = f(x,f(y,v,z),f(v,x,u)). [para(19572(a,2),2(a,2)),rewrite(2(2,R),3(2),2(3),2(5,R),3(5)),flip(a)]. given #666 (A,wt=31): 267 f(x,f(y,z,u),f(x,v,f(x,w,z))) = f(x,v,f(x,w,f(y,z,f(x,z,u)))). [para(17(a,1),25(a,1,3,3)),flip(a)]. given #667 (F,wt=23): 19942 f(x,f(y,z,u),f(x,v,z)) = f(x,f(v,y,u),f(x,v,z)). [para(19572(a,1),14(a,1,3)),rewrite(3(2),15(4),2(4),3(5))]. given #668 (F,wt=23): 20017 f(x,f(y,z,u),f(v,y,x)) = f(x,f(v,z,u),f(v,y,x)). [para(2(a,1),19906(a,1)),rewrite(2(2),2(3,R),2(4))]. given #669 (T,wt=23): 20030 f(x,f(y,z,u),f(v,u,x)) = f(x,f(v,y,z),f(v,u,x)). [para(19907(a,1),2(a,2)),rewrite(2(2),2(3),2(4),2(4),2(5)),flip(a)]. given #670 (T,wt=23): 20068 f(x,f(y,z,u),f(x,v,z)) = f(x,f(y,v,u),f(x,v,z)). [para(778(a,1),19942(a,1,3)),rewrite(2(1,R),3(1),3(3),3(4),3(5),11087(5),16748(5),3(1),2(4,R),3(4),2(5,R),3(5),793(7)),flip(a)]. given #671 (A,wt=31): 268 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,y,f(x,u,f(x,w,z)))). [para(25(a,1),18(a,2,3)),rewrite(2(3,R),3(3),50(4),2(8,R),3(8)),flip(a)]. given #672 (F,wt=24): 15286 f(x,f(y,z,u),f(z,v,x)) = f(v,x,f(y,z,f(z,u,x))). [para(7530(a,1),2(a,2)),rewrite(2(2),2(3),2(4),2(4))]. given #673 (F,wt=24): 15355 f(x,f(y,z,f(z,x,u)),f(y,v,f(y,z,x))) = f(y,z,x). [para(7765(a,1),6657(a,1,3)),rewrite(2(1),2(4,R),3(4),66(5),2(5,R),2(6),3(8),1538(8))]. given #674 (T,wt=24): 15361 f(x,f(y,z,f(u,y,x)),f(u,x,f(u,y,v))) = f(u,y,x). [para(7765(a,1),213(a,2,3)),rewrite(3(1),3(3),3(5),3971(7),877(3),3(2)),flip(a)]. given #675 (T,wt=22): 20144 f(x,y,f(z,u,f(x,z,f(y,v,z)))) = f(x,y,z). [para(15361(a,1),11370(a,1,3)),rewrite(2(1),3(1),2(3,R),3(3),2(4,R),16314(4),496(3),2(4),3(4),3(5),11087(5),20012(5),2(5),3(5),2(7,R),3(7),2(8,R),3(8),16107(9),797(9),11218(7))]. given #676 (A,wt=31): 269 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,u,f(x,y,f(x,w,z)))). [para(25(a,1),24(a,2,3)),rewrite(50(4)),flip(a)]. given #677 (F,wt=24): 15384 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,u,f(y,z,x))). [para(18(a,2),7819(a,2,3)),rewrite(2(2),2(5,R),3(5),1804(6),2(4),2(4))]. given #678 (F,wt=24): 15393 f(x,f(y,z,u),f(z,x,v)) = f(x,v,f(z,u,f(y,z,x))). [para(840(a,2),7819(a,2,3)),rewrite(2(2),2(5,R),3(5),1804(6),2(4),2(4))]. given #679 (T,wt=24): 15394 f(x,f(y,z,u),f(x,v,f(y,x,z))) = f(x,v,f(y,x,z)). [para(892(a,1),7819(a,1,3,3)),rewrite(3(3),889(6)),flip(a)]. given #680 (T,wt=24): 15395 f(x,f(y,z,f(y,x,u)),f(z,x,v)) = f(x,v,f(y,z,x)). [para(784(a,1),7819(a,2,3)),rewrite(2(1,R),3(1),2(3),2(4,R),3(4),2(7,R),3(7),1804(8),2(5),2(5))]. given #681 (A,wt=38): 273 f(x,y,f(z,u,f(x,z,f(z,v,f(z,w,v6))))) = f(x,z,f(x,y,f(z,v6,f(z,u,f(z,v,w))))). [para(25(a,1),19(a,2,3,3))]. given #682 (F,wt=24): 15396 f(x,f(y,z,f(z,x,u)),f(y,x,v)) = f(x,v,f(y,z,x)). [para(786(a,1),7819(a,2,3)),rewrite(2(1,R),3(1),2(3),2(4,R),3(4),2(7,R),3(7),1804(8),2(5),2(5))]. given #683 (F,wt=24): 15399 f(x,y,f(z,x,f(u,x,v))) = f(x,y,f(x,v,f(u,z,x))). [para(1661(a,1),7819(a,2,3)),rewrite(7819(6)),flip(a)]. given #684 (T,wt=24): 15434 f(x,f(y,z,x),f(x,u,f(y,v,z))) = f(x,u,f(y,z,x)). [para(7129(a,1),7819(a,1,3,3)),rewrite(3(3),8(6)),flip(a)]. given #685 (T,wt=24): 15449 f(x,f(y,z,f(z,u,x)),f(y,x,v)) = f(x,v,f(y,z,x)). [para(9972(a,1),7819(a,2,3)),rewrite(2(1),2(3),2(4),2(7,R),3(7),1804(8),2(5),2(5))]. given #686 (A,wt=44): 276 f(x,f(y,z,f(x,u,f(x,v,w))),f(y,z,f(x,w,f(x,y,f(x,u,v))))) = f(x,y,f(y,z,f(x,u,f(x,v,w)))). [para(25(a,1),21(a,1,3,3))]. given #687 (F,wt=24): 15472 f(x,f(y,z,f(z,u,x)),f(u,x,v)) = f(x,v,f(z,u,x)). [para(12381(a,1),7819(a,2,3)),rewrite(2(1),2(1),2(2,R),3(2),22(3),2(3),2(4),2(4),2(5,R),3(5),22(6),2(7,R),3(7),1804(8),2(5),3(5))]. given #688 (F,wt=24): 15474 f(x,f(y,z,f(y,u,x)),f(z,x,v)) = f(x,v,f(y,z,x)). [para(12424(a,1),7819(a,2,3)),rewrite(2(3),2(7,R),3(7),1804(8),3(5))]. given #689 (T,wt=24): 15589 f(x,f(y,z,u),f(z,x,f(y,u,v))) = f(z,x,f(y,u,v)). [para(7941(a,1),162(a,1,3)),rewrite(2(3,R),3(3),2(5,R),3(5),8(6),2(5,R),3(5)),flip(a)]. given #690 (T,wt=24): 15594 f(x,f(y,z,u),f(v,x,f(y,v,z))) = f(v,x,f(y,z,u)). [para(7941(a,1),7819(a,1,3)),rewrite(2(3),2(5,R),3(5),8(6),2(5,R),3(5)),flip(a)]. given #691 (A,wt=38): 279 f(x,y,f(z,u,f(x,u,f(z,v,f(z,w,v6))))) = f(x,u,f(x,y,f(z,v6,f(z,u,f(z,v,w))))). [para(25(a,1),23(a,2,3,3))]. given #692 (F,wt=24): 15605 f(x,f(y,z,u),f(v,z,x)) = f(v,x,f(y,z,f(z,u,x))). [para(8021(a,2),2(a,2)),rewrite(3(3),2(5)),flip(a)]. given #693 (F,wt=24): 15607 f(x,y,f(z,u,f(u,v,y))) = f(x,y,f(u,y,f(z,u,v))). [para(8021(a,2),198(a,1,3)),rewrite(2(4),8772(6),2(6,R),3(6)),flip(a)]. given #694 (T,wt=24): 15665 f(x,f(y,z,f(z,x,u)),f(v,y,f(y,z,x))) = f(y,z,x). [para(6371(a,1),8882(a,2)),rewrite(2(1),2(3),2(6),2(8),1(8),2(6),15101(6),2(5,R),2(6),2(8),2(8),1848(8),2(7,R),3(7),13(7))]. given #695 (T,wt=22): 20248 f(x,y,f(z,u,f(v,z,f(x,z,y)))) = f(x,z,y). [para(11489(a,1),15665(a,1,3)),rewrite(3(2),3(5),3(6),2(7,R),3(7),11087(7),1869(6),15(5),2(7),2(7),13(7),8(7),2(6),16115(6),115(3),3(7),2(8,R),3(8),11087(8),957(7),13(6))]. given #696 (A,wt=31): 281 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,y,f(x,z,f(x,w,u)))). [para(26(a,2),5(a,2,3)),flip(a)]. given #697 (F,wt=22): 20252 f(x,y,f(z,u,f(v,z,f(x,y,z)))) = f(x,y,z). [para(2(a,1),20248(a,1,3)),rewrite(3(1),2(3),2(3),3(5))]. given #698 (F,wt=22): 20253 f(x,y,f(z,u,f(v,u,f(x,y,u)))) = f(x,y,u). [para(2(a,2),20248(a,1,3)),rewrite(3(1),3(3),3(5))]. given #699 (T,wt=22): 20257 f(x,y,f(z,u,f(v,u,f(x,u,y)))) = f(x,u,y). [para(20248(a,1),13826(a,1,3)),rewrite(3(3),3(5),11087(5),19682(5),2(1,R),8(1),12(2),2(4,R),3(4)),flip(a)]. given #700 (T,wt=24): 15670 f(x,y,f(z,u,f(z,v,x))) = f(z,x,f(x,y,f(z,v,u))). [para(8985(a,1),2719(a,2)),rewrite(2(1,R),3(1),2(3,R),3(3),2(5,R),3(5),2(7,R),3(7),6821(8),2(4),2(4),2(6,R),3(6)),flip(a)]. given #701 (A,wt=31): 283 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,w,f(x,y,f(x,u,f(x,z,v)))). [para(26(a,1),10(a,1,3)),rewrite(50(8))]. given #702 (F,wt=24): 15682 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(y,u,f(x,z,y))). [para(9101(a,1),2(a,2)),rewrite(3(3),2(4))]. given #703 (F,wt=24): 15690 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(x,y,f(z,y,u))). [para(9109(a,1),2(a,2)),rewrite(3(3),2(5,R),3(5))]. given #704 (T,wt=24): 15731 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(z,u,f(x,y,z))). [para(9436(a,2),1175(a,2)),rewrite(11385(5),15(5),11495(5))]. given #705 (T,wt=24): 15758 f(x,y,f(y,f(x,z,u),f(y,v,z))) = f(x,y,f(y,v,z)). [para(68(a,2),151(a,2,3)),rewrite(784(3),22(3)),flip(a)]. given #706 (A,wt=38): 284 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,v,f(x,y,f(x,z,f(x,v6,f(x,u,w))))). [para(26(a,1),11(a,1,3,3))]. given #707 (F,wt=24): 15776 f(x,f(y,z,x),f(u,v,f(z,x,u))) = f(x,u,f(y,z,x)). [para(1136(a,1),10177(a,1,3)),rewrite(2(3,R),3(3),2(4),2(4),13647(6),2(7,R),3(7),198(8))]. given #708 (F,wt=24): 15826 f(f(x,y,z),f(u,x,y),f(v,z,f(x,y,z))) = f(x,y,z). [para(6893(a,1),10567(a,1,3,3)),rewrite(8(6),3(5),6915(5)),flip(a)]. given #709 (T,wt=24): 15827 f(f(x,y,z),f(x,u,y),f(v,z,f(x,y,z))) = f(x,y,z). [para(7129(a,1),10567(a,1,3,3)),rewrite(8(6),3(5),7142(5)),flip(a)]. given #710 (T,wt=24): 15834 f(x,y,f(z,u,f(y,v,u))) = f(x,y,f(v,u,f(y,z,u))). [para(2(a,2),10622(a,1,3)),rewrite(3(2),3(4))]. low water: id=18045, wt=34 given #711 (A,wt=38): 285 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,u,f(x,y,f(x,v,f(x,v6,f(x,z,w))))). [para(26(a,2),11(a,2,3,3))]. given #712 (F,wt=24): 15839 f(x,y,f(z,u,f(v,z,x))) = f(z,x,f(x,y,f(v,z,u))). [para(10622(a,2),2719(a,2)),rewrite(2(1,R),3(1),2(3,R),3(3),2(5,R),3(5),2(7,R),3(7),7586(8),2(4),2(4),2(6,R),3(6)),flip(a)]. given #713 (F,wt=24): 15845 f(x,f(y,z,u),f(v,x,z)) = f(v,x,f(z,u,f(x,y,z))). [para(10622(a,2),1510(a,2)),rewrite(11385(5),15(5),11991(5))]. given #714 (T,wt=24): 15903 f(x,f(y,z,u),f(y,v,x)) = f(v,x,f(y,z,f(y,x,u))). [para(2(a,1),10968(a,1)),rewrite(2(3,R),3(4))]. given #715 (T,wt=24): 15918 f(x,f(y,z,x),f(z,u,v)) = f(y,x,f(z,u,f(z,x,v))). [para(10969(a,2),3(a,2)),rewrite(2(1,R),3(1),3(3),3(4)),flip(a)]. given #716 (A,wt=31): 286 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,z,f(x,y,f(x,w,u)))). [para(26(a,2),11(a,2,3)),flip(a)]. given #717 (F,wt=24): 15976 f(x,f(y,z,x),f(z,u,v)) = f(y,x,f(z,v,f(z,u,x))). [para(10969(a,2),1664(a,2)),rewrite(2(1,R),3(1),2(3,R),3(3),3(4),15809(6),15846(6),3(4)),flip(a)]. given #718 (F,wt=24): 15978 f(x,f(y,z,x),f(z,u,v)) = f(y,x,f(z,x,f(z,u,v))). [para(10969(a,2),7152(a,2)),rewrite(2(1,R),3(1),2(3,R),3(3),3(4),13(4),15809(5),10466(5),3(4)),flip(a)]. given #719 (T,wt=24): 16036 f(x,y,f(x,z,f(u,x,v))) = f(x,v,f(x,y,f(u,x,z))). [back_rewrite(1705),rewrite(2(1),2(4),15991(8),11087(5),15917(4),3(2),793(3),2(4))]. given #720 (T,wt=24): 16171 f(x,f(y,z,u),f(y,x,f(x,v,z))) = f(y,x,f(x,v,z)). [back_rewrite(13711),rewrite(3(3),3(4),1348(6),3(3),3(4)),flip(a)]. given #721 (A,wt=38): 287 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,u,f(x,y,f(x,w,f(x,v,f(x,z,v6))))). [para(11(a,1),26(a,2,3,3)),rewrite(50(4))]. given #722 (F,wt=24): 16219 f(x,y,f(x,f(z,y,u),f(x,z,v))) = f(x,v,f(x,z,y)). [para(786(a,1),11093(a,2,3)),rewrite(3(3),16111(4))]. given #723 (F,wt=24): 16220 f(x,y,f(x,f(y,z,u),f(x,u,v))) = f(x,v,f(x,y,u)). [para(791(a,1),11093(a,2,3)),rewrite(3(1),3(3),16107(4),3(5))]. given #724 (T,wt=24): 16222 f(x,y,f(x,f(z,y,u),f(x,u,v))) = f(x,v,f(x,y,u)). [para(957(a,1),11093(a,2,3)),rewrite(3(3),16111(4))]. given #725 (T,wt=24): 16314 f(x,f(y,x,z),f(u,v,w)) = f(x,z,f(y,x,f(u,v,w))). [para(11094(a,2),789(a,2)),rewrite(3(7),15991(8),2(7,R),3(7),15993(8)),flip(a)]. given #726 (A,wt=38): 288 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,u,f(x,y,f(x,z,f(x,w,f(x,v6,v))))). [para(11(a,2),26(a,2,3,3)),rewrite(50(4),3(6))]. given #727 (F,wt=24): 16823 f(x,y,f(z,u,f(v,x,u))) = f(x,y,f(v,u,f(x,z,u))). [para(11204(a,2),10567(a,2)),rewrite(2(5),11087(6),15989(6),3(3),2(4,R),3(4),16072(6),15991(4),3(1),3(5),2(7,R),3(7),16672(7),2(4)),flip(a)]. given #728 (F,wt=24): 16843 f(x,f(y,z,u),f(x,v,f(y,v,z))) = f(x,v,f(y,z,u)). [para(11312(a,1),778(a,2)),rewrite(3(2),3(5),2(7),11087(8),15989(8),1569(7),3(5))]. given #729 (T,wt=24): 16885 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(u,z,v))). [para(11312(a,1),70(a,2,3)),rewrite(3(2),14979(5),3(4)),flip(a)]. given #730 (T,wt=24): 16890 f(x,y,f(x,f(z,y,u),f(z,u,v))) = f(x,y,f(z,u,v)). [para(11312(a,1),123(a,2,3)),rewrite(3(3),15(6),3(6),11498(8))]. given #731 (A,wt=31): 289 f(x,y,f(z,u,f(y,z,f(z,v,w)))) = f(y,z,f(x,y,f(z,w,f(z,u,v)))). [para(26(a,1),17(a,1,3)),rewrite(2(2,R),3(2),2(8,R),3(8))]. given #732 (F,wt=24): 16897 f(x,f(y,z,u),f(v,y,x)) = f(v,x,f(y,u,f(y,x,z))). [para(314(a,2),11312(a,2)),rewrite(13(2),16055(5),16095(4),3(4)),flip(a)]. given #733 (F,wt=24): 16939 f(x,f(y,z,u),f(v,u,f(x,v,y))) = f(x,v,f(y,z,u)). [para(11312(a,1),11174(a,1)),rewrite(3(4)),flip(a)]. given #734 (T,wt=21): 20559 f(x,f(y,z,f(u,z,v)),f(u,z,x)) = f(u,z,x). [para(16939(a,1),15012(a,1,3)),rewrite(8(4),8(3),2(6),198(7),15991(6),2(6,R),3(6),10541(6)),flip(a)]. given #735 (T,wt=24): 16987 f(x,f(y,z,u),f(v,y,f(v,z,x))) = f(v,x,f(y,z,u)). [para(11370(a,1),1979(a,2)),rewrite(3(2),2(3,R),3(3),3(5),2(6,R),3(6),3(7),2(8,R),3(8),3(9),2(10,R),3(10),5114(12),3(5),2(6,R),3(6))]. given #736 (A,wt=31): 290 f(x,y,f(z,u,f(z,v,f(z,x,w)))) = f(z,x,f(x,y,f(z,u,f(z,w,v)))). [para(26(a,2),17(a,2,3)),rewrite(2(3,R),3(3),2(8,R),3(8)),flip(a)]. given #737 (F,wt=24): 17000 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(z,u,v))). [para(11370(a,1),70(a,2,3)),rewrite(3(2),13832(5),3(4)),flip(a)]. given #738 (F,wt=24): 17045 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(z,w,f(v,z,u))). [para(6497(a,1),11372(a,2,3,3)),rewrite(2(1),2(1),2(3),2(3),16020(6),2(2),16314(4),979(3),2(4),2(4),2(6),2(6),198(9))]. given #739 (T,wt=24): 17067 f(x,f(y,z,f(y,x,u)),f(z,v,f(y,z,x))) = f(y,z,x). [para(6019(a,1),11372(a,2,3)),rewrite(3(1),3(3),2(5),2(5),877(5),2(4,R),3(4),16107(5),1539(5),11218(3),3(2),2(4),2(4),2(6,R)),flip(a)]. given #740 (T,wt=24): 17068 f(x,f(y,z,f(y,x,u)),f(v,z,f(y,z,x))) = f(y,z,x). [para(6371(a,1),11372(a,2,3)),rewrite(3(1),3(3),2(5),2(5),957(5),2(4,R),3(4),16111(5),1539(5),11249(3),3(2),2(4),2(4),2(6,R)),flip(a)]. given #741 (A,wt=31): 294 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,u,f(x,y,f(x,w,f(x,v,z)))). [para(26(a,2),24(a,2,3)),rewrite(50(4),3(5))]. given #742 (F,wt=22): 20607 f(x,y,f(z,u,f(x,z,f(v,y,z)))) = f(x,y,z). [para(17068(a,1),12(a,1,3)),rewrite(2(1),3(1),2(3),3(3),3(4),11087(4),957(3),13(2),2(2,R),3(2),2(3,R),3(3),2(4),3(4),20555(6),16314(4)),flip(a)]. given #743 (F,wt=24): 17109 f(x,f(y,z,f(y,x,u)),f(x,v,u)) = f(x,u,f(y,x,v)). [para(11384(a,1),213(a,2,3)),rewrite(3(3),2(4,R),15991(5),807(5),2(6,R)),flip(a)]. given #744 (T,wt=24): 17212 f(x,y,f(x,f(y,z,u),f(v,x,u))) = f(v,x,f(x,y,u)). [para(6019(a,1),166(a,2,3)),rewrite(3(1),16107(4),3(5),13(8),16107(8),8(9),22(7))]. given #745 (T,wt=24): 17213 f(x,y,f(x,f(z,y,u),f(v,x,u))) = f(v,x,f(x,y,u)). [para(6371(a,1),166(a,2,3)),rewrite(3(1),16111(4),3(5),13(8),16111(8),8(9),22(7))]. given #746 (A,wt=31): 297 f(x,y,f(z,u,f(z,x,f(z,v,w)))) = f(z,x,f(x,y,f(z,w,f(z,u,v)))). [para(26(a,1),22(a,1,3,3)),rewrite(96(5))]. given #747 (F,wt=24): 17264 f(x,f(y,z,f(y,u,x)),f(u,v,f(y,u,x))) = f(y,u,x). [para(11534(a,1),63(a,1)),rewrite(2(1),2(1),2(2,R),3(2),2(3),2(3),2(4,R),3(4),17254(5),2(2),2(2),2(3,R),3(3),2(4),2(4),2(5,R),3(5),2(6,R),3(6),16107(7),3(4),11495(7),2(6,R)),flip(a)]. given #748 (F,wt=24): 17270 f(x,f(y,z,f(u,z,x)),f(u,z,f(u,x,v))) = f(u,z,x). [para(11534(a,1),123(a,2,3)),rewrite(2(1),2(1),2(3),2(3),3(5),2(6,R),3(6),3971(7),957(3),2(2),2(2),2(4,R),3(4)),flip(a)]. given #749 (T,wt=24): 17274 f(x,f(y,z,f(z,u,x)),f(z,u,f(u,x,v))) = f(z,u,x). [para(11534(a,1),95(a,1,3)),rewrite(2(1),2(3),2(5),2(5),15402(6),2(5,R),3(5),793(5),2(4),2(4),16314(4),66(3),1848(3),2(2),2(4),2(6),2(6),15402(7)),flip(a)]. given #750 (T,wt=24): 17304 f(x,f(y,z,f(y,u,x)),f(u,x,v)) = f(y,x,f(u,x,v)). [para(11535(a,1),67(a,2,3)),rewrite(2(3),2(3),2(4,R),3971(6),2(5,R),3(5),2(6,R)),flip(a)]. given #751 (A,wt=31): 299 f(x,y,f(z,u,f(z,x,f(z,v,w)))) = f(x,y,f(z,x,f(z,w,f(z,u,v)))). [para(26(a,1),115(a,1,3,3)),rewrite(2(4,R),3(4),96(5),2(8,R),3(8))]. given #752 (F,wt=24): 17352 f(x,f(y,z,u),f(u,x,f(y,x,v))) = f(x,v,f(y,u,x)). [para(11579(a,1),2(a,2)),rewrite(2(2,R),3(2),2(3,R),3(3),2(4),2(5),2(5))]. given #753 (F,wt=24): 17366 f(x,f(y,z,f(y,u,x)),f(u,v,x)) = f(y,x,f(u,v,x)). [para(11579(a,1),67(a,2,3)),rewrite(2(4,R),3971(6),2(6,R)),flip(a)]. given #754 (T,wt=24): 17370 f(x,y,f(x,f(z,u,y),f(x,z,v))) = f(x,v,f(x,z,y)). [para(11579(a,1),123(a,2,3)),rewrite(15(6),2060(8))]. given #755 (T,wt=24): 17372 f(x,f(y,z,x),f(u,v,f(u,y,x))) = f(u,x,f(y,z,x)). [para(11579(a,1),213(a,2,3)),rewrite(793(6)),flip(a)]. given #756 (A,wt=38): 300 f(x,y,f(z,u,f(x,v,f(x,z,f(x,w,v6))))) = f(x,z,f(x,y,f(z,u,f(x,v6,f(x,v,w))))). [para(26(a,1),19(a,1,3,3))]. given #757 (F,wt=24): 17457 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(u,v,z))). [para(11649(a,1),134(a,2,3)),rewrite(3(2),2(3,R),3(3),13077(5),2(4),2(4))]. given #758 (F,wt=24): 17665 f(x,y,f(z,x,f(u,x,v))) = f(u,x,f(x,v,f(z,x,y))). [para(8022(a,1),181(a,1,2)),rewrite(3(2),2(4,R),3(4),1804(4),2(5),1(5),2(5,R),16314(5),16038(6),2(2),12(3),16314(3),2(6),1(6),2(5),2(5))]. given #759 (T,wt=24): 17670 f(x,f(y,z,f(x,u,z)),f(u,z,f(x,v,u))) = f(x,u,z). [para(11661(a,1),181(a,1,3,3)),rewrite(2(1,R),3(1),2(3),979(3),2(3,R),3(3),2(5),11881(7),12424(5),3(4),11087(4),957(3),13(2),2(2,R),3(2),2(4,R),3(4),2(6),11617(7)),flip(a)]. given #760 (T,wt=24): 17672 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,u,f(y,x,z))). [para(69(a,2),17628(a,2)),rewrite(3(8),16115(9),16340(7),2(2,R),3(2),4779(6))]. given #761 (A,wt=38): 301 f(x,y,f(z,u,f(x,z,f(z,v,f(z,w,v6))))) = f(x,z,f(x,y,f(z,v,f(z,v6,f(z,u,w))))). [para(26(a,2),19(a,2,3,3))]. given #762 (F,wt=24): 17673 f(x,y,f(x,z,f(u,x,v))) = f(x,v,f(x,z,f(u,x,y))). [para(80(a,1),17628(a,2)),rewrite(3(8),16115(9),16340(7),2(2,R),3(2),11087(5),4794(6))]. given #763 (F,wt=24): 17686 f(x,f(y,z,u),f(y,x,f(v,z,u))) = f(y,x,f(v,z,u)). [para(1510(a,1),17647(a,2)),rewrite(2(8,R),3(8),11087(9),15996(10),5363(7))]. given #764 (T,wt=24): 17687 f(x,f(y,z,u),f(y,x,f(z,v,u))) = f(y,x,f(z,v,u)). [para(7161(a,1),17647(a,2)),rewrite(2(8,R),3(8),11087(9),15996(10),5363(7))]. given #765 (T,wt=24): 17764 f(x,f(y,z,u),f(x,z,f(y,x,v))) = f(x,v,f(y,x,z)). [para(11534(a,1),11991(a,2)),rewrite(1868(6))]. given #766 (A,wt=31): 303 f(x,y,f(x,f(y,z,u),f(x,v,w))) = f(x,v,f(x,w,f(y,z,f(x,y,u)))). [para(19(a,2),26(a,2,3))]. given #767 (F,wt=24): 17778 f(x,y,f(y,z,f(u,y,v))) = f(u,y,f(y,v,f(x,y,z))). [para(10541(a,1),182(a,1,3)),rewrite(3(1),3(5),16314(6),1073(7),3(4),16314(6),22(7))]. given #768 (F,wt=24): 17806 f(x,f(y,z,u),f(x,v,f(y,x,u))) = f(x,v,f(y,x,u)). [para(12041(a,1),67(a,2,3)),rewrite(13(5),12041(4)),flip(a)]. given #769 (T,wt=24): 17810 f(x,f(y,z,u),f(y,x,f(u,x,v))) = f(x,v,f(y,u,x)). [para(12041(a,1),7164(a,1,3)),rewrite(2(2,R),3(2),3(4),17134(6),2(4,R),3(4)),flip(a)]. given #770 (T,wt=24): 17811 f(x,f(y,z,u),f(x,u,f(y,x,v))) = f(x,v,f(y,x,u)). [para(11534(a,1),12041(a,2)),rewrite(1868(6))]. given #771 (A,wt=44): 305 f(x,f(y,z,f(x,u,f(x,v,w))),f(y,z,f(x,u,f(x,w,f(x,y,v))))) = f(x,y,f(y,z,f(x,u,f(x,v,w)))). [para(26(a,2),21(a,1,3,3))]. given #772 (F,wt=24): 17839 f(x,y,f(z,u,f(z,v,x))) = f(z,x,f(x,y,f(z,u,v))). [para(2(a,1),12368(a,1)),rewrite(2(3),3(3),3(4),2(5,R),3(5))]. given #773 (F,wt=24): 17840 f(x,y,f(z,u,f(z,v,y))) = f(z,y,f(x,y,f(z,u,v))). [para(12368(a,1),3(a,2)),rewrite(3(3),3(4))]. given #774 (T,wt=24): 17911 f(x,f(y,z,u),f(v,u,f(x,v,z))) = f(x,v,f(y,z,u)). [para(11645(a,1),12513(a,1)),flip(a)]. given #775 (T,wt=24): 17922 f(x,f(y,z,u),f(y,x,f(x,z,v))) = f(x,v,f(y,x,z)). [para(2(a,1),12652(a,1)),rewrite(2(1,R),3(1),2(3,R),3(3),2(4,R),2(5),2(5))]. given #776 (A,wt=38): 306 f(x,y,f(z,u,f(x,v,f(x,u,f(x,w,v6))))) = f(x,u,f(x,y,f(z,u,f(x,v6,f(x,v,w))))). [para(26(a,1),23(a,1,3,3))]. given #777 (F,wt=24): 17935 f(x,y,f(y,f(x,z,u),f(z,y,v))) = f(y,v,f(x,z,y)). [para(12652(a,1),182(a,1,3)),rewrite(2(1,R),3(1),2(4,R),3(4),3(6),17210(6),2(3,R),3(3)),flip(a)]. given #778 (F,wt=24): 17956 f(x,f(y,z,f(y,x,u)),f(u,v,f(y,x,u))) = f(y,x,u). [para(12664(a,1),117(a,1,3)),rewrite(2(5),2(5),17344(6),791(5),2(4),2(4),2921(4),2(6),2(6),17344(7)),flip(a)]. given #779 (T,wt=24): 17965 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(x,z,f(y,u,v))). [back_rewrite(16286),rewrite(17949(5),15272(4)),flip(a)]. given #780 (T,wt=24): 18035 f(x,f(y,z,u),f(v,z,f(v,x,y))) = f(v,x,f(y,z,u)). [para(12815(a,1),11204(a,1)),flip(a)]. given #781 (A,wt=38): 307 f(x,y,f(z,u,f(x,u,f(z,v,f(z,w,v6))))) = f(x,u,f(x,y,f(z,v,f(z,v6,f(z,u,w))))). [para(26(a,2),23(a,2,3,3))]. given #782 (F,wt=24): 18118 f(f(x,y,z),f(x,y,u),f(x,u,f(y,z,u))) = f(x,y,u). [para(18024(a,1),63(a,2,3)),rewrite(2(2),2(2),2(3),2(3),2(4),3(4),2(5,R),3(5),11178(5),2(3,R),3(3),2(6),2(6),2(7),2(7),2(9,R),3(9),2921(9))]. given #783 (F,wt=24): 18140 f(x,y,f(x,f(z,y,u),f(z,x,v))) = f(x,v,f(z,x,y)). [para(778(a,1),18029(a,1,1)),rewrite(2(2),2(2),2(5,R),3(5),18114(6),2(5),2(5),16111(6)),flip(a)]. given #784 (T,wt=24): 18188 f(x,f(y,z,u),f(y,x,f(x,u,v))) = f(x,v,f(y,x,u)). [para(18175(a,1),1804(a,1,3,3)),rewrite(2(1,R),3(1),2(3),2(3),2(5,R),3(5),16037(6),11468(3),12(2),2(3,R),3(3),2(5),2(5),16314(6)),flip(a)]. given #785 (T,wt=24): 18312 f(x,y,f(y,z,f(u,y,v))) = f(y,z,f(y,v,f(u,x,y))). [para(139(a,1),18054(a,2)),rewrite(2(3,R),3(3),13(4),2(5,R),3(5),1771(7),16314(4),12(3),11087(3),2(7,R),3(7),7174(7)),flip(a)]. given #786 (A,wt=38): 309 f(x,y,f(x,z,f(x,u,f(v,w,f(x,w,v6))))) = f(x,z,f(x,u,f(x,w,f(x,y,f(v,w,v6))))). [para(23(a,2),26(a,2,3,3)),rewrite(3(3),50(4)),flip(a)]. given #787 (F,wt=24): 18335 f(x,f(y,z,f(y,x,u)),f(x,z,v)) = f(x,v,f(y,x,z)). [para(787(a,1),18056(a,1,1)),rewrite(3(4),3(6),18214(6)),flip(a)]. given #788 (F,wt=24): 18338 f(f(x,y,z),f(x,z,u),f(x,u,f(y,z,u))) = f(x,z,u). [para(18056(a,1),11372(a,2,3)),rewrite(2(4),2(4),11178(5),2(9,R),3(9),999(9))]. given #789 (T,wt=24): 18366 f(x,y,f(y,z,f(u,y,v))) = f(y,z,f(y,v,f(x,u,y))). [para(139(a,1),18133(a,2)),rewrite(2(3,R),3(3),13(4),2(5,R),3(5),1770(7),16314(4),198(3),11087(3),2(7,R),3(7),7174(7)),flip(a)]. given #790 (T,wt=24): 18487 f(x,f(y,z,u),f(y,v,f(z,v,x))) = f(v,x,f(y,z,u)). [para(13036(a,1),2(a,2)),rewrite(2(2),2(2),2(4),2(6,R),3(6))]. given #791 (A,wt=38): 310 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,u,f(x,y,f(x,v6,f(x,v,f(x,z,w))))). [para(25(a,1),26(a,2,3,3)),rewrite(50(4))]. given #792 (F,wt=24): 18488 f(x,f(y,z,u),f(y,v,f(v,x,z))) = f(v,x,f(y,z,u)). [para(2(a,1),13036(a,1)),rewrite(2(1),2(4,R),2(6,R),3(6))]. given #793 (F,wt=24): 18490 f(x,f(y,z,u),f(y,v,f(x,v,z))) = f(x,v,f(y,z,u)). [para(13036(a,1),12(a,1,3)),rewrite(3(1),16111(5),11498(4),13(3),3(4)),flip(a)]. given #794 (T,wt=24): 18502 f(x,f(y,z,u),f(y,v,f(z,x,v))) = f(x,v,f(y,z,u)). [para(13036(a,1),892(a,2)),rewrite(2(2,R),3(2),3(4),2(6,R),3(6),11219(9))]. given #795 (T,wt=24): 18508 f(x,f(y,z,f(x,u,z)),f(y,u,v)) = f(x,z,f(y,u,v)). [para(13036(a,1),998(a,2)),rewrite(2(7,R),9979(9))]. given #796 (A,wt=38): 311 f(x,y,f(x,z,f(x,u,f(x,v,f(x,w,v6))))) = f(x,u,f(x,y,f(x,z,f(x,v6,f(x,w,v))))). [para(26(a,2),26(a,2,3,3)),rewrite(50(4),3(6))]. given #797 (F,wt=22): 21000 f(x,y,f(z,u,f(y,z,f(v,x,z)))) = f(x,y,z). [para(18508(a,1),6657(a,1,3)),rewrite(2(1),2(5,R),3(5),2(6,R),20999(6),16314(3),2(5),3(7),1848(7))]. given #798 (F,wt=24): 18541 f(x,f(y,z,u),f(z,v,f(y,v,x))) = f(v,x,f(y,z,u)). [para(13105(a,1),2(a,2)),rewrite(2(2),2(2),2(4),2(6,R),3(6))]. given #799 (T,wt=24): 18545 f(x,f(y,z,u),f(z,v,f(y,x,v))) = f(x,v,f(y,z,u)). [para(13105(a,1),892(a,2)),rewrite(2(2,R),3(2),3(4),2(6,R),3(6),11219(9))]. given #800 (T,wt=24): 18549 f(x,f(y,z,f(x,u,z)),f(u,y,v)) = f(x,z,f(u,y,v)). [para(13105(a,1),998(a,2)),rewrite(2(7,R),9979(9))]. given #801 (A,wt=31): 312 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,w,f(x,y,f(x,u,z)))). [para(26(a,2),26(a,2,3)),rewrite(50(3),3(1)),flip(a)]. given #802 (F,wt=24): 18586 f(x,f(y,z,u),f(y,u,f(x,z,v))) = f(y,u,f(x,z,v)). [back_rewrite(18433),rewrite(2(2,R),3(2),13105(4),2(3,R),3(3)),flip(a)]. given #803 (F,wt=23): 21103 f(f(x,y,z),f(u,x,v),f(u,v,y)) = f(u,v,f(x,y,z)). [para(18586(a,1),12815(a,2)),rewrite(2(2,R),3(2),2(5),2(5),10268(6),3(5),18011(5),2(5,R),3(5))]. given #804 (T,wt=23): 21121 f(f(x,y,z),f(u,z,v),f(x,y,u)) = f(x,y,f(u,z,v)). [para(21103(a,1),2(a,1)),rewrite(3(5)),flip(a)]. given #805 (T,wt=23): 21122 f(f(x,y,z),f(x,z,u),f(y,u,v)) = f(x,z,f(y,u,v)). [para(21103(a,1),2(a,2))]. given #806 (A,wt=31): 318 f(x,f(y,z,u),f(x,v,f(x,y,w))) = f(x,v,f(x,w,f(y,z,f(x,y,u)))). [para(31(a,1),5(a,2,3)),rewrite(3(2))]. given #807 (F,wt=20): 21272 f(x,f(y,z,u),f(y,v,z)) = f(y,z,f(v,u,x)). [para(21122(a,1),1175(a,2)),rewrite(2(6),2(6),21147(7),8323(5))]. given #808 (F,wt=20): 21283 f(x,f(y,z,u),f(y,z,v)) = f(y,z,f(v,u,x)). [para(21122(a,1),13654(a,2)),rewrite(2(2,R),3(2),3(3),3(5),2(6),2(6),1042(7),18804(6),2(4,R),3(4))]. given #809 (T,wt=20): 21370 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [back_rewrite(21132),rewrite(2(5,R),3(5),21304(6),3(4))]. ============================== PROOF ================================= % Proof 1 at 564.19 (+ 1.15) seconds: dist_both. % Length of proof is 175. % Level of proof is 33. % Maximum clause weight is 44. % Given clauses 809. 1 f(x,x,y) = x # label(majority). [assumption]. 2 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 3 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. 4 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. 5 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(4),rewrite(2(2),2(2),2(3,R),3(3)),rewrite(2(1,R),3(1),3(3),2(4,R),3(4))]. 6 f(f(A,B,C),D,E) != f(f(A,D,E),f(B,D,E),f(C,D,E)) | f(f(A,B,C),D,E) != f(A,f(B,D,E),f(C,D,E)) # answer(dist_both). [assumption]. 7 f(f(A,D,E),f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) | f(A,f(B,D,E),f(C,D,E)) != f(D,E,f(A,B,C)) # answer(dist_both). [copy(6),rewrite(2(7),2(7),2(28),2(28)),flip(a),flip(b)]. 8 f(x,y,y) = y. [para(2(a,1),1(a,1))]. 9 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(5(a,1),2(a,2)),rewrite(3(2),2(3,R),3(3)),flip(a)]. 10 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(2(a,1),5(a,1,3)),rewrite(2(1,R),3(1))]. 11 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(5(a,1),5(a,1,3))]. 12 f(x,y,f(x,z,y)) = f(x,z,y). [para(8(a,1),5(a,1,3)),flip(a)]. 13 f(x,y,f(x,y,z)) = f(x,y,z). [para(8(a,1),5(a,1)),rewrite(3(3),12(3)),flip(a)]. 14 f(x,y,f(x,z,f(x,u,y))) = f(x,z,f(x,u,y)). [para(12(a,1),5(a,1,3)),flip(a)]. 15 f(x,y,f(x,z,f(x,y,u))) = f(x,z,f(x,y,u)). [para(12(a,1),5(a,2,3)),rewrite(3(1),3(4))]. 17 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(9(a,1),2(a,2)),rewrite(3(2),2(3,R),3(3))]. 18 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(2(a,1),9(a,1)),rewrite(2(2),2(2),3(3))]. 19 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))). [para(9(a,2),5(a,1,3))]. 21 f(x,f(y,z,u),f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(9(a,2),12(a,1,3))]. 22 f(x,y,f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(9(a,2),13(a,1,3))]. 23 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para(9(a,1),9(a,1,3)),rewrite(2(1,R),3(1),2(6,R),3(6))]. 25 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,z,u))). [para(10(a,2),5(a,1,3))]. 26 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,v,z))). [para(10(a,1),5(a,2,3)),flip(a)]. 31 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,z,f(x,y,u))). [para(9(a,2),10(a,1,3)),flip(a)]. 33 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,y,v))). [para(11(a,1),2(a,2)),rewrite(3(3),2(5,R),3(5)),flip(a)]. 34 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(x,y,v))). [para(11(a,2),2(a,2)),rewrite(3(3),2(4,R),3(4))]. 47 f(x,y,f(x,z,f(u,v,f(x,u,w)))) = f(x,u,f(x,y,f(x,z,f(u,v,w)))). [para(9(a,2),11(a,1,3,3))]. 50 f(x,f(x,y,z),f(x,u,v)) = f(x,y,f(x,u,f(x,v,z))). [para(11(a,1),10(a,1)),flip(a)]. 63 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,u,v))). [para(5(a,1),17(a,1,3)),rewrite(2(1,R),3(1),2(6,R),3(6))]. 66 f(x,y,f(z,x,f(x,y,u))) = f(z,x,f(x,y,u)). [para(12(a,1),17(a,1,3)),rewrite(2(1),2(3),2(5,R),3(5)),flip(a)]. 67 f(x,y,f(z,u,f(y,u,v))) = f(y,u,f(x,y,f(z,u,v))). [para(9(a,1),17(a,1,3)),rewrite(2(1,R),3(1),2(6,R),3(6))]. 75 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,v,u))). [para(18(a,2),5(a,2,3)),flip(a)]. 88 f(x,y,f(x,z,f(y,u,f(x,y,v)))) = f(x,z,f(y,u,f(x,y,v))). [para(14(a,1),9(a,1,3)),rewrite(2(1),2(4),2(7,R),3(7)),flip(a)]. 96 f(x,y,f(y,z,f(x,u,f(x,y,v)))) = f(y,z,f(x,u,f(x,y,v))). [para(14(a,1),17(a,2,3)),rewrite(3(1),2(3,R),3(3),3(5),2(7,R),3(7))]. 100 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(x,z,f(z,v,u))). [para(18(a,2),14(a,2,3)),rewrite(14(5)),flip(a)]. 115 f(x,y,f(z,y,f(x,y,u))) = f(z,y,f(x,y,u)). [para(66(a,1),2(a,2)),rewrite(2(1,R),3(1),3(3),2(4,R),3(4))]. 125 f(x,y,f(z,u,f(x,z,u))) = f(x,y,f(x,z,u)). [para(8(a,1),19(a,1,3)),rewrite(3(4),88(6)),flip(a)]. 126 f(x,f(y,z,u),f(y,z,f(y,x,u))) = f(y,z,f(y,x,u)). [para(8(a,1),19(a,1)),rewrite(2(1,R),3(1),2(3,R),3(3),3(6),2(7,R),3(7),96(7)),flip(a)]. 140 f(x,y,f(z,y,f(z,x,u))) = f(z,x,f(z,y,f(x,y,u))). [para(19(a,1),17(a,1)),flip(a)]. 156 f(x,y,f(z,y,f(x,z,u))) = f(z,y,f(x,z,f(x,y,u))). [para(19(a,1),115(a,1,3)),rewrite(2(2,R),3(2),2(3,R),3(3),88(4),2(4,R),3(4),2(6,R),3(6))]. 162 f(x,f(y,z,u),f(y,z,f(y,u,x))) = f(y,x,f(y,z,u)). [para(21(a,1),2(a,2)),rewrite(2(2),2(2),2(4),2(6,R),3(6))]. 163 f(x,f(y,z,u),f(z,u,f(x,y,z))) = f(x,z,f(y,z,u)). [para(2(a,1),21(a,1,2)),rewrite(3(2),2(5))]. 194 f(x,f(y,z,f(u,v,f(x,u,w))),f(y,z,f(x,u,f(x,y,f(u,v,w))))) = f(x,y,f(y,z,f(u,v,f(x,u,w)))). [para(19(a,1),21(a,1,3,3))]. 198 f(x,y,f(z,x,y)) = f(z,x,y). [para(125(a,1),8(a,1)),rewrite(3(4),125(4),8(3)),flip(a)]. 208 f(x,y,f(z,x,f(x,u,y))) = f(z,x,f(x,u,y)). [para(198(a,1),17(a,1,3)),rewrite(2(1),2(3),2(5,R),3(5)),flip(a)]. 213 f(x,y,f(z,u,f(u,y,v))) = f(u,y,f(x,y,f(z,u,v))). [para(23(a,1),2(a,2)),rewrite(2(1,R),3(1),3(3),2(5,R),3(5),2(6,R),3(6))]. 234 f(x,y,f(z,u,f(x,z,y))) = f(x,z,f(z,y,f(x,y,u))). [para(18(a,2),23(a,2,3)),flip(a)]. 256 f(x,f(y,z,u),f(y,z,f(x,z,f(x,y,u)))) = f(x,z,f(x,y,f(y,z,u))). [para(21(a,1),23(a,2,3))]. 259 f(x,y,f(z,x,f(z,y,u))) = f(z,x,f(z,y,f(x,y,u))). [para(23(a,1),208(a,2)),rewrite(2(4,R),3(4),14(5),2(5,R),3(5)),flip(a)]. 314 f(x,f(y,z,u),f(v,y,x)) = f(v,x,f(y,z,f(y,x,u))). [para(31(a,2),2(a,2)),rewrite(2(1,R),3(1),3(3),2(5),2(5)),flip(a)]. 316 f(x,f(y,z,u),f(x,u,v)) = f(x,v,f(y,u,f(x,z,u))). [para(2(a,2),31(a,1,2)),rewrite(3(2),3(4),2(5,R),3(5))]. 326 f(x,y,f(z,f(x,y,u),f(x,v,f(x,y,u)))) = f(x,f(x,y,u),f(z,v,f(x,y,u))). [para(13(a,1),31(a,1,3)),rewrite(2(2),2(2),3(4),3(7),2(8,R),3(8)),flip(a)]. 362 f(x,f(y,x,z),f(y,x,u)) = f(y,x,f(x,u,z)). [para(18(a,2),31(a,2)),rewrite(8(2),3(2)),flip(a)]. 381 f(x,y,f(z,f(x,y,u),f(x,y,z))) = f(y,z,f(x,y,f(x,z,u))). [para(31(a,2),115(a,1,3)),rewrite(2(2),3(2),2(5,R),3(5),2(7,R),3(7))]. 387 f(x,f(y,z,u),f(x,y,v)) = f(x,y,f(x,v,f(y,z,u))). [para(31(a,2),19(a,1)),rewrite(3(2))]. 432 f(x,f(x,y,z),f(y,u,f(x,y,v))) = f(x,y,f(x,z,f(y,u,v))). [para(5(a,1),362(a,1,3)),rewrite(2(1,R),3(1),2(2,R),3(2),3(6),2(7,R),3(7))]. 496 f(x,y,f(x,z,f(u,x,y))) = f(u,x,f(x,z,y)). [para(12(a,1),34(a,1,3)),flip(a)]. 541 f(x,y,f(z,y,f(z,u,f(x,z,v)))) = f(x,z,f(z,y,f(x,y,f(z,u,v)))). [para(34(a,1),23(a,2,3)),flip(a)]. 567 f(x,f(y,x,z),f(x,u,z)) = f(y,x,f(x,u,z)). [para(496(a,1),10(a,1)),rewrite(3(4)),flip(a)]. 595 f(x,f(y,x,z),f(x,z,u)) = f(y,x,f(x,z,u)). [para(567(a,1),2(a,2)),rewrite(3(2),2(3),3(4))]. 631 f(x,f(x,y,z),f(u,x,y)) = f(u,x,f(x,y,z)). [para(595(a,1),3(a,1)),flip(a)]. 632 f(x,f(x,y,z),f(u,v,f(x,y,z))) = f(x,z,f(x,y,f(u,v,f(x,y,z)))). [para(595(a,1),19(a,2)),rewrite(2(1),2(1),2(2),2(2),3(3),2(4,R),3(4),326(5),2(5),2(5),2(6),2(6),2(8,R),3(8))]. 778 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para(631(a,1),33(a,1,3)),rewrite(2(4,R),8(4),2(3,R),8(3),2(5),3(5),2(6,R),3(6),432(6),3(3),50(6),3(4),13(4),13(5)),flip(a)]. 784 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [back_rewrite(259),rewrite(2(1,R),3(1),2(2,R),3(2),778(3),2(3,R),3(3),2(4,R),3(4)),flip(a)]. 786 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [back_rewrite(140),rewrite(2(1,R),3(1),2(2,R),3(2),2(5,R),3(5),2(6,R),3(6),784(6))]. 787 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [back_rewrite(156),rewrite(2(2,R),3(2),786(3),2(4,R),3(4)),flip(a)]. 788 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [back_rewrite(541),rewrite(2(3,R),3(3),2(7,R),3(7),784(8))]. 791 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [back_rewrite(234),rewrite(3(1),2(5,R),3(5),784(6))]. 793 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [back_rewrite(256),rewrite(787(4),387(3),778(3)),flip(a)]. 795 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [back_rewrite(381),rewrite(791(4)),flip(a)]. 801 f(x,y,f(x,f(y,z,u),f(y,v,f(y,z,u)))) = f(y,z,f(x,y,u)). [para(9(a,2),778(a,2)),rewrite(3(3))]. 808 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(18(a,2),778(a,2)),rewrite(3(3),801(5))]. 824 f(x,f(y,z,u),f(x,v,f(x,y,z))) = f(x,v,f(x,y,z)). [para(778(a,1),25(a,1,3)),flip(a)]. 840 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(808(a,1),2(a,2)),rewrite(3(2),2(3)),flip(a)]. 844 f(f(x,y,z),f(x,y,f(x,z,u)),f(u,v,f(x,y,z))) = f(v,f(x,y,z),f(x,u,f(x,y,z))). [para(21(a,1),808(a,2,3)),rewrite(2(2),2(2),3(5),2(9,R),3(9),2(10,R),3(10))]. 864 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(840(a,1),2(a,2)),rewrite(3(2),2(3))]. 889 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(840(a,2),31(a,2)),rewrite(3(2),387(3),778(3)),flip(a)]. 892 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(31(a,2),840(a,2)),rewrite(2(2),387(3),778(3),2(2,R),3(2),2(3,R),3(3)),flip(a)]. 957 f(x,y,f(z,u,f(x,u,y))) = f(x,u,y). [para(13(a,1),864(a,1,3)),rewrite(8(3),632(5),115(4)),flip(a)]. 963 f(x,f(y,z,u),f(y,v,f(y,z,u))) = f(v,f(y,z,u),f(y,u,f(x,y,z))). [para(18(a,2),864(a,2,3)),rewrite(2(3,R),3(3))]. 997 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(2(a,1),889(a,1,2)),rewrite(2(2),2(4))]. 998 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(2(a,2),889(a,1,2)),rewrite(2(2),3(2),387(3),2(4),3(4))]. 1004 f(x,f(y,z,u),f(v,f(y,z,x),f(y,z,u))) = f(v,f(y,z,x),f(y,z,u)). [para(889(a,1),9(a,1,3)),rewrite(2(3,R),2(7,R)),flip(a)]. 1005 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(9(a,1),889(a,1,2)),rewrite(2(3),2(5))]. 1014 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(18(a,1),889(a,1,2)),rewrite(2(3),2(5))]. 1042 f(f(x,y,z),f(x,y,u),f(u,v,f(x,y,z))) = f(v,f(x,y,u),f(x,y,z)). [para(889(a,1),362(a,1,2)),rewrite(3(4),2(9,R),1004(10))]. 1059 f(x,y,f(x,f(z,u,v),f(y,z,u))) = f(x,y,f(z,u,v)). [para(889(a,1),778(a,1,3,3)),rewrite(2(2))]. 1067 f(x,f(y,z,u),f(x,u,f(y,z,v))) = f(x,u,f(y,z,v)). [para(889(a,1),889(a,1,2)),rewrite(2(3),2(6))]. 1068 f(x,f(y,x,z),f(y,z,u)) = f(y,x,z). [para(892(a,1),3(a,1)),flip(a)]. 1084 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,z,f(x,y,u))). [para(31(a,2),892(a,2)),rewrite(3(3),2(6,R),3(6),387(7),998(7),2(5,R),3(5)),flip(a)]. 1099 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(997(a,1),2(a,2)),rewrite(2(2),2(2),2(3),2(4),2(4))]. 1100 f(x,f(y,z,u),f(x,v,f(x,z,u))) = f(x,v,f(x,z,u)). [para(997(a,1),5(a,2,3))]. 1127 f(x,f(y,z,u),f(v,f(x,z,u),f(y,z,u))) = f(v,f(x,z,u),f(y,z,u)). [para(997(a,1),21(a,1,3,3)),rewrite(2(3,R),2(6,R),8(7),2(7,R)),flip(a)]. 1136 f(x,f(y,z,u),f(x,u,f(x,z,v))) = f(x,v,f(x,z,u)). [para(997(a,1),26(a,2,3)),rewrite(3(2))]. 1162 f(x,f(y,z,f(z,u,v)),f(x,f(y,z,u),f(z,u,v))) = f(x,f(y,z,u),f(z,u,v)). [para(595(a,1),997(a,1,2))]. 1502 f(x,y,f(y,f(z,u,f(x,u,v)),f(x,w,f(z,u,f(x,u,v))))) = f(x,u,f(x,y,f(z,u,v))). [para(23(a,1),786(a,2)),rewrite(3(5))]. 1508 f(x,y,f(y,f(z,u,v),f(x,z,u))) = f(x,y,f(z,u,v)). [para(889(a,1),786(a,1,3,3)),rewrite(2(2))]. 1510 f(x,y,f(y,f(z,u,v),f(x,u,v))) = f(x,y,f(z,u,v)). [para(997(a,1),786(a,1,3,3))]. 1650 f(x,f(y,z,u),f(x,z,f(z,v,f(y,z,u)))) = f(y,z,f(x,z,u)). [para(17(a,1),793(a,2)),rewrite(3(3))]. 1661 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(840(a,2),793(a,2)),rewrite(3(3),1650(5)),flip(a)]. 1662 f(x,f(y,z,u),f(x,u,f(u,v,f(y,z,u)))) = f(y,u,f(x,z,u)). [para(864(a,1),793(a,2)),rewrite(3(3))]. 1664 f(x,f(y,z,u),f(x,v,f(z,u,v))) = f(x,v,f(y,z,u)). [para(997(a,1),793(a,1,3,3)),rewrite(2(2),2(2))]. 1668 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(1661(a,1),2(a,2)),rewrite(3(2),2(3))]. 1754 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(1668(a,1),793(a,2)),rewrite(3(3),1662(5))]. 1771 f(f(x,y,z),f(x,z,u),f(y,v,f(x,z,u))) = f(v,f(x,z,u),f(x,y,z)). [para(1068(a,1),1754(a,2,3))]. 1803 f(x,y,f(z,u,f(x,u,f(y,u,v)))) = f(x,y,u). [para(34(a,2),795(a,1,3)),rewrite(2(1,R),3(1),2(2,R),3(2),2(5),2(5))]. 1804 f(x,f(y,z,u),f(y,z,f(z,u,x))) = f(z,x,f(y,z,u)). [para(567(a,1),795(a,1,3)),rewrite(3(2),2(4,R),3(4),3(6))]. 1848 f(x,y,f(z,u,f(u,x,y))) = f(u,x,y). [para(2(a,1),957(a,1)),rewrite(2(1,R),3(1),2(3),2(3),2(4,R),3(4))]. 2513 f(x,f(y,z,f(x,y,u)),f(x,v,w)) = f(x,y,f(x,v,f(x,w,f(y,z,u)))). [para(47(a,1),10(a,1)),flip(a)]. 2745 f(x,f(y,z,f(u,z,v)),f(x,u,z)) = f(x,u,z). [para(1005(a,1),14(a,2)),rewrite(2(1,R),3(1),3(3),15(5),3(5))]. 3618 f(x,f(y,x,z),f(u,y,f(y,x,v))) = f(x,z,f(u,y,f(y,x,v))). [para(2745(a,1),795(a,1,3)),rewrite(2(1,R),3(1),2(3),3(3),2(4,R),2(5,R),3(5),2(7))]. 3828 f(x,y,f(y,f(x,z,u),f(v,f(x,z,u),f(x,w,f(x,z,u))))) = f(x,z,f(x,y,u)). [para(5(a,1),788(a,2)),rewrite(3(4),2(5,R),3(5))]. 3859 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(997(a,1),788(a,2)),rewrite(3(6),2(7,R),3(7),3828(9),3(2))]. 3885 f(x,y,f(x,z,f(u,y,f(y,v,z)))) = f(x,y,z). [para(1014(a,1),788(a,2)),rewrite(3(8),2(9,R),3(9),3828(11),3(3))]. 5045 f(x,y,f(x,z,f(u,y,f(z,y,v)))) = f(x,z,y). [para(1803(a,1),786(a,2)),rewrite(3(7),1502(9))]. 6497 f(x,y,f(y,z,f(u,x,y))) = f(y,z,f(u,x,y)). [para(1099(a,1),5045(a,1,3)),rewrite(2(2),2(2),2(4),2(4),2(6,R),3(6),198(6),2(5),2(5),2(7),3(7),12(7))]. 6530 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(1099(a,1),6497(a,2)),rewrite(2(1),2(2),2(2),22(4),3(2),2(4),2(4))]. 6743 f(x,f(x,y,z),f(u,y,z)) = f(x,y,z). [para(997(a,1),63(a,2,3)),rewrite(2(3),2(3),3859(4),997(3),2(4,R)),flip(a)]. 6803 f(x,f(x,y,z),f