============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27709 was started by mccune on cleo, Fri Apr 13 09:43:04 2007 The command was "/home/mccune/bin/prover9 -f dist-both.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dist-both.in assign(max_seconds,3600). 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(goals). f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # label(dist_long). f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_short). f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) & f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_both). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # label(dist_long) # label(goal). [goal]. 2 f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_short) # label(goal). [goal]. 3 f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) & f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_both) # label(goal). [goal]. ============================== 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(c1,c4,c5),f(c2,c4,c5),f(c3,c4,c5)) != f(f(c1,c2,c3),c4,c5) # label(dist_long). [deny(1)]. f(f(c6,c7,c8),c9,c10) != f(c6,f(c7,c9,c10),f(c8,c9,c10)) # label(dist_short). [deny(2)]. f(f(c11,c14,c15),f(c12,c14,c15),f(c13,c14,c15)) != f(f(c11,c12,c13),c14,c15) | f(f(c11,c12,c13),c14,c15) != f(c11,f(c12,c14,c15),f(c13,c14,c15)) # label(dist_both). [deny(3)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label dist_long to answer in negative clause % copying label dist_short to answer in negative clause % copying label dist_both to answer in negative clause % assign(max_proofs, 3). % (Horn set with more than one neg. clause) Term ordering decisions: Function symbol KB weights: c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. c7=1. c8=1. c9=1. c10=1. c11=1. c12=1. c13=1. c14=1. c15=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, 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). restricted denial: (wt=23): 10 f(f(c1,c4,c5),f(c2,c4,c5),f(c3,c4,c5)) != f(c4,c5,f(c1,c2,c3)) # answer(dist_long). [copy(9),rewrite(5(20),5(20))]. restricted denial: (wt=20): 12 f(c6,f(c7,c9,c10),f(c8,c9,c10)) != f(c9,c10,f(c6,c7,c8)) # answer(dist_short). [copy(11),rewrite(5(7),5(7)),flip(a)]. restricted denial: (wt=43): 14 f(f(c11,c14,c15),f(c12,c14,c15),f(c13,c14,c15)) != f(c14,c15,f(c11,c12,c13)) | f(c11,f(c12,c14,c15),f(c13,c14,c15)) != f(c14,c15,f(c11,c12,c13)) # answer(dist_both). [copy(13),rewrite(5(20),5(20),5(28),5(28)),flip(b)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 10 f(f(c1,c4,c5),f(c2,c4,c5),f(c3,c4,c5)) != f(c4,c5,f(c1,c2,c3)) # answer(dist_long). [copy(9),rewrite(5(20),5(20))]. 12 f(c6,f(c7,c9,c10),f(c8,c9,c10)) != f(c9,c10,f(c6,c7,c8)) # answer(dist_short). [copy(11),rewrite(5(7),5(7)),flip(a)]. 14 f(f(c11,c14,c15),f(c12,c14,c15),f(c13,c14,c15)) != f(c14,c15,f(c11,c12,c13)) | f(c11,f(c12,c14,c15),f(c13,c14,c15)) != f(c14,c15,f(c11,c12,c13)) # answer(dist_both). [copy(13),rewrite(5(20),5(20),5(28),5(28)),flip(b)]. end_of_list. formulas(sos). 4 f(x,x,y) = x # label(majority). [assumption]. 5 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 6 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. 8 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(7),rewrite(5(2),5(2),5(3,R),6(3)),rewrite(5(1,R),6(1),6(3),5(4,R),6(4))]. end_of_list. formulas(demodulators). 4 f(x,x,y) = x # label(majority). [assumption]. 5 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. % (lex-dep) 6 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): 4 f(x,x,y) = x # label(majority). [assumption]. given #2 (I,wt=10): 5 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. given #3 (I,wt=10): 6 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. given #4 (I,wt=17): 8 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(7),rewrite(5(2),5(2),5(3,R),6(3)),rewrite(5(1,R),6(1),6(3),5(4,R),6(4))]. given #5 (A,wt=7): 15 f(x,y,y) = y. [para(5(a,1),4(a,1))]. given #6 (T,wt=14): 19 f(x,y,f(x,z,y)) = f(x,z,y). [para(15(a,1),8(a,1,3)),flip(a)]. given #7 (T,wt=14): 20 f(x,y,f(x,y,z)) = f(x,y,z). [para(15(a,1),8(a,1)),rewrite(6(3),19(3)),flip(a)]. given #8 (T,wt=17): 16 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(8(a,1),5(a,2)),rewrite(6(2),5(3,R),6(3)),flip(a)]. given #9 (T,wt=17): 17 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(5(a,1),8(a,1,3)),rewrite(5(1,R),6(1))]. given #10 (A,wt=24): 18 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(8(a,1),8(a,1,3))]. given #11 (T,wt=17): 24 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(16(a,1),5(a,2)),rewrite(6(2),5(3,R),6(3))]. given #12 (T,wt=17): 25 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(5(a,1),16(a,1)),rewrite(5(2),5(2),6(3))]. given #13 (T,wt=17): 31 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)). [para(5(a,1),17(a,1)),rewrite(5(2),5(2),6(3))]. given #14 (T,wt=21): 21 f(x,y,f(x,z,f(x,u,y))) = f(x,z,f(x,u,y)). [para(19(a,1),8(a,1,3)),flip(a)]. given #15 (A,wt=21): 22 f(x,y,f(x,z,f(x,y,u))) = f(x,z,f(x,y,u)). [para(19(a,1),8(a,2,3)),rewrite(6(1),6(4))]. given #16 (T,wt=21): 29 f(x,y,f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(16(a,2),20(a,1,3))]. given #17 (T,wt=21): 73 f(x,y,f(z,x,f(x,y,u))) = f(z,x,f(x,y,u)). [para(19(a,1),24(a,1,3)),rewrite(5(1),5(3),5(5,R),6(5)),flip(a)]. given #18 (T,wt=21): 122 f(x,y,f(z,y,f(x,y,u))) = f(z,y,f(x,y,u)). [para(73(a,1),5(a,2)),rewrite(5(1,R),6(1),6(3),5(4,R),6(4))]. given #19 (T,wt=24): 26 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))). [para(16(a,2),8(a,1,3))]. given #20 (A,wt=24): 28 f(x,f(y,z,u),f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(16(a,2),19(a,1,3))]. given #21 (T,wt=21): 132 f(x,y,f(z,u,f(x,z,u))) = f(x,y,f(x,z,u)). [para(15(a,1),26(a,1,3)),rewrite(6(4),95(6)),flip(a)]. given #22 (T,wt=14): 205 f(x,y,f(z,x,y)) = f(z,x,y). [para(132(a,1),15(a,1)),rewrite(6(4),132(4),15(3)),flip(a)]. given #23 (T,wt=21): 215 f(x,y,f(z,x,f(x,u,y))) = f(z,x,f(x,u,y)). [para(205(a,1),24(a,1,3)),rewrite(5(1),5(3),5(5,R),6(5)),flip(a)]. given #24 (T,wt=24): 30 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para(16(a,1),16(a,1,3)),rewrite(5(1,R),6(1),5(6,R),6(6))]. given #25 (A,wt=24): 32 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,z,u))). [para(17(a,2),8(a,1,3))]. given #26 (T,wt=24): 33 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,v,z))). [para(17(a,1),8(a,2,3)),flip(a)]. given #27 (T,wt=24): 38 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,z,f(x,y,u))). [para(16(a,2),17(a,1,3)),flip(a)]. given #28 (T,wt=20): 369 f(x,f(y,x,z),f(y,x,u)) = f(y,x,f(x,u,z)). [para(25(a,2),38(a,2)),rewrite(15(2),6(2)),flip(a)]. given #29 (T,wt=24): 40 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,y,v))). [para(18(a,1),5(a,2)),rewrite(6(3),5(5,R),6(5)),flip(a)]. given #30 (A,wt=24): 41 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(x,y,v))). [para(18(a,2),5(a,2)),rewrite(6(3),5(4,R),6(4))]. given #31 (T,wt=21): 503 f(x,y,f(x,z,f(u,x,y))) = f(u,x,f(x,z,y)). [para(19(a,1),41(a,1,3)),flip(a)]. given #32 (T,wt=20): 574 f(x,f(y,x,z),f(x,u,z)) = f(y,x,f(x,u,z)). [para(503(a,1),17(a,1)),rewrite(6(4)),flip(a)]. given #33 (T,wt=20): 602 f(x,f(y,x,z),f(x,z,u)) = f(y,x,f(x,z,u)). [para(574(a,1),5(a,2)),rewrite(6(2),5(3),6(4))]. given #34 (T,wt=20): 603 f(x,f(x,y,z),f(u,x,z)) = f(u,x,f(x,y,z)). [para(574(a,1),6(a,1)),flip(a)]. given #35 (A,wt=31): 42 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(18(a,1),8(a,1,3))]. given #36 (T,wt=20): 638 f(x,f(x,y,z),f(u,x,y)) = f(u,x,f(x,y,z)). [para(602(a,1),6(a,1)),flip(a)]. given #37 (T,wt=18): 785 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para(638(a,1),40(a,1,3)),rewrite(5(4,R),15(4),5(3,R),15(3),5(5),6(5),5(6,R),6(6),439(6),6(3),57(6),6(4),20(4),20(5)),flip(a)]. given #38 (T,wt=17): 815 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(25(a,2),785(a,2)),rewrite(6(3),808(5))]. given #39 (T,wt=17): 847 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(815(a,1),5(a,2)),rewrite(6(2),5(3)),flip(a)]. given #40 (A,wt=24): 43 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,z,f(x,y,v))). [para(18(a,1),8(a,1))]. given #41 (T,wt=17): 871 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(847(a,1),5(a,2)),rewrite(6(2),5(3))]. given #42 (T,wt=17): 896 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(847(a,2),38(a,2)),rewrite(6(2),394(3),785(3)),flip(a)]. given #43 (T,wt=17): 899 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(38(a,2),847(a,2)),rewrite(5(2),394(3),785(3),5(2,R),6(2),5(3,R),6(3)),flip(a)]. given #44 (T,wt=17): 1004 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(5(a,1),896(a,1,2)),rewrite(5(2),5(4))]. given #45 (A,wt=31): 44 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(18(a,2),8(a,1,3))]. given #46 (T,wt=17): 1006 f(x,f(y,z,x),f(y,z,u)) = f(y,z,x). [para(896(a,1),6(a,1)),flip(a)]. given #47 (T,wt=17): 1007 f(x,f(x,y,z),f(y,z,u)) = f(x,y,z). [para(896(a,1),6(a,2)),rewrite(5(1),5(4))]. given #48 (T,wt=17): 1075 f(x,f(y,x,z),f(y,z,u)) = f(y,x,z). [para(899(a,1),6(a,1)),flip(a)]. given #49 (T,wt=17): 1106 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(1004(a,1),5(a,2)),rewrite(5(2),5(2),5(3),5(4),5(4))]. given #50 (A,wt=24): 45 f(x,y,f(x,z,f(x,u,v))) = f(x,y,f(x,u,f(x,z,v))). [para(18(a,2),8(a,1))]. given #51 (T,wt=18): 791 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [back_rewrite(266),rewrite(5(1,R),6(1),5(2,R),6(2),785(3),5(3,R),6(3),5(4,R),6(4)),flip(a)]. given #52 (T,wt=18): 793 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [back_rewrite(147),rewrite(5(1,R),6(1),5(2,R),6(2),5(5,R),6(5),5(6,R),6(6),791(6))]. given #53 (T,wt=18): 794 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [back_rewrite(163),rewrite(5(2,R),6(2),793(3),5(4,R),6(4)),flip(a)]. given #54 (T,wt=18): 798 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [back_rewrite(241),rewrite(6(1),5(5,R),6(5),791(6))]. given #55 (A,wt=28): 50 f(x,y,f(x,z,f(x,u,f(x,v,y)))) = f(x,z,f(x,u,f(x,v,y))). [para(19(a,1),18(a,1,3,3)),flip(a)]. given #56 (T,wt=18): 800 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [back_rewrite(263),rewrite(794(4),394(3),785(3)),flip(a)]. given #57 (T,wt=17): 1668 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(847(a,2),800(a,2)),rewrite(6(3),1657(5)),flip(a)]. given #58 (T,wt=17): 1675 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(1668(a,1),5(a,2)),rewrite(6(2),5(3))]. given #59 (T,wt=17): 1761 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(1675(a,1),800(a,2)),rewrite(6(3),1669(5))]. given #60 (A,wt=28): 51 f(x,y,f(x,z,f(x,u,f(x,y,v)))) = f(x,y,f(x,z,f(x,u,v))). [para(18(a,2),20(a,1,3))]. given #61 (T,wt=18): 802 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [back_rewrite(388),rewrite(798(4)),flip(a)]. given #62 (T,wt=18): 884 f(x,y,f(z,u,f(x,z,y))) = f(x,z,y). [para(847(a,2),26(a,2,3)),rewrite(5(2,R),6(2),793(3),6(2)),flip(a)]. given #63 (T,wt=18): 964 f(x,y,f(z,u,f(x,u,y))) = f(x,u,y). [para(20(a,1),871(a,1,3)),rewrite(15(3),639(5),122(4)),flip(a)]. given #64 (T,wt=18): 986 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u). [para(871(a,1),30(a,2,3)),rewrite(6(1),6(4),5(5,R),6(5),884(6))]. given #65 (A,wt=31): 52 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(18(a,1),16(a,1,3)),rewrite(5(2,R),6(2),5(8,R),6(8))]. given #66 (T,wt=18): 1005 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(5(a,2),896(a,1,2)),rewrite(5(2),6(2),394(3),5(4),6(4))]. given #67 (T,wt=18): 1545 f(x,y,f(z,u,f(z,x,y))) = f(z,x,y). [para(5(a,1),798(a,1)),rewrite(5(1),5(3),5(3),5(4))]. given #68 (T,wt=18): 1855 f(x,y,f(z,u,f(u,x,y))) = f(u,x,y). [para(5(a,1),964(a,1)),rewrite(5(1,R),6(1),5(3),5(3),5(4,R),6(4))]. given #69 (T,wt=20): 1009 f(f(x,y,z),f(x,z,u),f(x,y,z)) = f(x,y,z). [para(19(a,1),896(a,1,3)),rewrite(19(6))]. given #70 (A,wt=31): 53 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(18(a,2),16(a,1,3)),rewrite(5(1,R),6(1),5(8,R),6(8))]. given #71 (T,wt=20): 1010 f(f(x,y,z),f(x,y,u),f(x,y,z)) = f(x,y,z). [para(20(a,1),896(a,1,3)),rewrite(20(6))]. given #72 (T,wt=20): 1033 f(f(x,y,z),f(y,z,u),f(x,y,z)) = f(x,y,z). [para(205(a,1),896(a,1,3)),rewrite(205(6))]. given #73 (T,wt=21): 888 f(x,f(y,x,z),f(z,u,f(y,x,z))) = f(y,x,z). [para(205(a,1),847(a,1,3)),rewrite(5(3,R),15(3),6(4)),flip(a)]. given #74 (T,wt=21): 983 f(x,f(y,x,z),f(u,z,f(y,x,z))) = f(y,x,z). [para(205(a,1),871(a,1,3)),rewrite(15(3)),flip(a)]. given #75 (A,wt=31): 54 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(16(a,2),18(a,1,3,3))]. given #76 (T,wt=21): 985 f(x,y,f(x,f(x,y,z),f(u,y,z))) = f(x,y,z). [para(871(a,1),30(a,1)),rewrite(20(3),15(3)),flip(a)]. given #77 (T,wt=21): 1012 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(16(a,1),896(a,1,2)),rewrite(5(3),5(5))]. given #78 (T,wt=21): 1021 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(25(a,1),896(a,1,2)),rewrite(5(3),5(5))]. given #79 (T,wt=21): 1301 f(x,f(x,y,z),f(y,u,f(y,z,v))) = f(x,y,z). [para(8(a,1),1006(a,1,3)),rewrite(5(1),5(5))]. given #80 (A,wt=31): 55 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(16(a,2),18(a,2,3,3)),flip(a)]. given #81 (T,wt=21): 1684 f(x,f(y,z,x),f(z,u,f(y,z,x))) = f(y,z,x). [para(205(a,1),1668(a,1,3)),rewrite(5(3,R),15(3),6(4)),flip(a)]. given #82 (T,wt=21): 1715 f(x,f(y,z,x),f(u,y,f(y,z,x))) = f(y,z,x). [para(19(a,1),1675(a,1,3)),rewrite(15(3)),flip(a)]. given #83 (T,wt=21): 1716 f(x,f(y,x,z),f(u,y,f(y,x,z))) = f(y,x,z). [para(20(a,1),1675(a,1,3)),rewrite(15(3)),flip(a)]. given #84 (T,wt=21): 1727 f(x,f(y,z,x),f(u,z,f(y,z,x))) = f(y,z,x). [para(205(a,1),1675(a,1,3)),rewrite(15(3)),flip(a)]. given #85 (A,wt=24): 57 f(x,f(x,y,z),f(x,u,v)) = f(x,y,f(x,u,f(x,v,z))). [para(18(a,1),17(a,1)),flip(a)]. given #86 (T,wt=21): 2694 f(x,y,f(x,f(x,y,z),f(y,u,z))) = f(x,y,z). [para(5(a,1),985(a,1,3)),rewrite(5(1,R),6(1),5(3,R))]. given #87 (T,wt=21): 2726 f(x,f(y,z,f(z,u,v)),f(z,u,x)) = f(z,u,x). [para(1012(a,1),5(a,2)),rewrite(5(3),5(3),5(4),5(5),5(5))]. given #88 (T,wt=21): 2751 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(1012(a,1),21(a,1,3)),rewrite(6(1),20(2),5(2,R),6(2),5(3,R),6(3),6(4)),flip(a)]. given #89 (T,wt=21): 2752 f(x,f(y,z,f(u,z,v)),f(x,u,z)) = f(x,u,z). [para(1012(a,1),21(a,2)),rewrite(5(1,R),6(1),6(3),22(5),6(5))]. given #90 (A,wt=31): 58 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(18(a,2),17(a,1,3)),rewrite(57(8))]. given #91 (T,wt=21): 2858 f(x,f(y,z,f(z,u,v)),f(z,v,x)) = f(z,v,x). [para(1021(a,1),5(a,2)),rewrite(5(3),5(3),5(4),5(5),5(5))]. given #92 (T,wt=21): 2928 f(x,f(y,z,x),f(y,u,f(y,z,v))) = f(y,z,x). [para(5(a,1),1301(a,1)),rewrite(5(3),5(3),5(4,R),5(5),5(5))]. given #93 (T,wt=21): 3418 f(x,f(y,z,f(y,u,v)),f(y,u,x)) = f(y,u,x). [para(2726(a,1),5(a,1)),rewrite(5(4,R),6(4),5(5,R)),flip(a)]. given #94 (T,wt=22): 795 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [back_rewrite(548),rewrite(5(3,R),6(3),5(7,R),6(7),791(8))]. given #95 (A,wt=24): 59 f(x,y,f(x,z,f(x,u,v))) = f(x,y,f(x,v,f(x,z,u))). [para(18(a,2),17(a,2)),rewrite(6(2),6(4)),flip(a)]. given #96 (T,wt=18): 3866 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(1004(a,1),795(a,2)),rewrite(6(6),5(7,R),6(7),3835(9),6(2))]. given #97 (T,wt=18): 3978 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y). [para(5(a,1),3866(a,1)),rewrite(5(1),5(3),5(3),6(4))]. given #98 (T,wt=21): 3841 f(x,y,f(z,f(x,z,u),f(y,z,v))) = f(x,y,z). [para(25(a,2),795(a,1,3))]. given #99 (T,wt=21): 4041 f(x,y,f(z,f(z,y,u),f(x,z,v))) = f(x,z,y). [para(3841(a,1),5(a,2)),rewrite(5(1,R),6(1),6(4),5(5),5(5))]. given #100 (A,wt=31): 60 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(17(a,2),18(a,1,3,3))]. given #101 (T,wt=21): 4042 f(x,y,f(z,f(x,z,u),f(z,y,v))) = f(x,z,y). [para(3841(a,1),6(a,2)),rewrite(5(2,R),6(2),6(4),6(5))]. given #102 (T,wt=21): 4043 f(x,y,f(z,f(y,z,u),f(x,z,v))) = f(x,y,z). [para(6(a,1),3841(a,1,3))]. given #103 (T,wt=22): 796 f(x,y,f(z,u,f(x,z,f(y,z,v)))) = f(x,y,z). [back_rewrite(486),rewrite(5(1,R),6(1),5(7,R),6(7),791(8))]. given #104 (T,wt=22): 805 f(x,y,f(x,z,f(y,u,f(y,z,v)))) = f(x,y,z). [para(8(a,1),785(a,1,3,3))]. given #105 (A,wt=31): 61 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(17(a,1),18(a,2,3,3))]. given #106 (T,wt=22): 807 f(x,y,f(x,z,f(z,u,f(y,z,v)))) = f(x,y,z). [para(16(a,2),785(a,1,3,3))]. given #107 (T,wt=22): 1015 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [para(17(a,2),896(a,1,2)),rewrite(5(3),394(4),5(5))]. given #108 (T,wt=22): 1469 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z). [para(8(a,1),791(a,1,3,3)),rewrite(5(3,R),6(3),6(5))]. given #109 (T,wt=22): 1519 f(x,y,f(z,u,f(y,z,f(x,z,v)))) = f(x,y,z). [para(18(a,1),794(a,1,3)),rewrite(5(1,R),6(1),5(2,R),6(2),5(5),5(5))]. given #110 (A,wt=24): 62 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,v,f(x,y,z))). [para(17(a,1),18(a,2,3))]. given #111 (T,wt=22): 1530 f(x,y,f(z,u,f(y,u,f(x,u,v)))) = f(x,y,u). [para(41(a,2),794(a,1,3)),rewrite(5(1,R),6(1),5(2,R),6(2),5(5),5(5))]. given #112 (T,wt=22): 1810 f(x,y,f(z,u,f(x,u,f(y,u,v)))) = f(x,y,u). [para(41(a,2),802(a,1,3)),rewrite(5(1,R),6(1),5(2,R),6(2),5(5),5(5))]. given #113 (T,wt=22): 1905 f(x,y,f(z,y,f(x,u,f(x,z,v)))) = f(x,z,y). [para(52(a,1),24(a,2)),rewrite(5(2,R),6(2),5(3,R),6(3),793(4),5(4,R),6(4),5(5,R),6(5)),flip(a)]. given #114 (T,wt=22): 1986 f(x,y,f(z,x,f(y,u,f(z,y,v)))) = f(z,x,y). [para(52(a,1),847(a,2)),rewrite(5(3),394(4),785(4),5(2,R),6(2),5(4,R),6(4)),flip(a)]. given #115 (A,wt=38): 63 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(18(a,1),18(a,1,3,3))]. given #116 (T,wt=21): 5129 f(x,f(y,z,f(u,y,v)),f(u,x,y)) = f(u,x,y). [para(1986(a,1),815(a,1)),flip(a)]. given #117 (T,wt=21): 5250 f(x,f(y,x,z),f(z,u,f(y,z,v))) = f(y,x,z). [para(5129(a,1),6(a,1)),flip(a)]. given #118 (T,wt=22): 2184 f(x,y,f(z,y,f(x,u,f(z,x,v)))) = f(z,x,y). [para(53(a,1),24(a,1)),rewrite(785(4)),flip(a)]. given #119 (T,wt=22): 2196 f(x,y,f(z,x,f(z,u,f(z,y,v)))) = f(z,x,y). [para(53(a,1),122(a,1,3)),rewrite(5(3,R),6(3),5(4,R),6(4),791(4),20(2),5(2,R),6(2),5(5,R),6(5)),flip(a)]. given #120 (A,wt=31): 64 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(18(a,1),18(a,1,3))]. given #121 (T,wt=21): 5422 f(x,f(y,z,f(y,u,v)),f(y,x,u)) = f(y,x,u). [para(2196(a,1),815(a,1)),flip(a)]. given #122 (T,wt=21): 5624 f(x,f(y,x,z),f(y,u,f(y,z,v))) = f(y,x,z). [para(5422(a,1),6(a,1)),flip(a)]. given #123 (T,wt=22): 2735 f(x,y,f(x,z,f(z,u,f(z,y,v)))) = f(x,z,y). [para(1012(a,1),17(a,1)),rewrite(5(3,R),6(3),6(4)),flip(a)]. given #124 (T,wt=22): 2737 f(x,y,f(x,z,f(u,z,f(y,z,v)))) = f(x,y,z). [para(17(a,1),1012(a,1)),rewrite(5(1,R),6(1),6(3),6(5))]. given #125 (A,wt=38): 65 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(18(a,2),18(a,1,3,3))]. given #126 (T,wt=22): 3477 f(x,y,f(z,y,f(z,u,f(z,x,v)))) = f(z,x,y). [para(2726(a,1),1668(a,1)),rewrite(5(3,R),6(3)),flip(a)]. given #127 (T,wt=22): 3502 f(x,y,f(x,z,f(y,u,f(z,y,v)))) = f(x,z,y). [para(2751(a,1),17(a,1)),rewrite(6(4)),flip(a)]. given #128 (T,wt=22): 3889 f(x,y,f(x,z,f(u,y,f(y,z,v)))) = f(x,y,z). [para(1012(a,1),795(a,2)),rewrite(6(8),5(9,R),6(9),3835(11),6(3))]. given #129 (T,wt=22): 3892 f(x,y,f(x,z,f(u,y,f(y,v,z)))) = f(x,y,z). [para(1021(a,1),795(a,2)),rewrite(6(8),5(9,R),6(9),3835(11),6(3))]. given #130 (A,wt=38): 66 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(18(a,1),18(a,2,3,3))]. given #131 (T,wt=22): 4139 f(x,y,f(z,u,f(x,z,f(z,y,v)))) = f(x,z,y). [para(2751(a,1),3841(a,2)),rewrite(5(1,R),6(1),6(3),6(4),6(5),5(6,R),6(6),6(8),5(9),4075(11),6(5))]. given #132 (T,wt=22): 4414 f(x,y,f(z,u,f(z,y,f(x,z,v)))) = f(x,z,y). [para(796(a,1),5(a,2)),rewrite(5(2,R),6(2),6(4),5(5),5(5))]. given #133 (T,wt=22): 4415 f(x,y,f(z,u,f(z,x,f(z,y,v)))) = f(z,x,y). [para(5(a,1),796(a,1)),rewrite(5(1,R),6(1),5(2,R),6(2),5(4),5(4),5(5))]. given #134 (T,wt=22): 4446 f(x,y,f(z,u,f(z,v,f(x,y,z)))) = f(x,y,z). [para(847(a,2),796(a,1,3,3))]. given #135 (A,wt=31): 67 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(18(a,1),18(a,2,3))]. given #136 (T,wt=21): 6085 f(x,y,f(z,f(x,y,z),f(z,u,v))) = f(x,y,z). [para(17(a,1),4446(a,1,3))]. given #137 (T,wt=21): 6252 f(x,y,f(z,f(x,z,y),f(z,u,v))) = f(x,z,y). [para(6085(a,1),5(a,2)),rewrite(5(1),5(1),6(4),5(5),5(5))]. given #138 (T,wt=22): 4979 f(x,y,f(z,u,f(x,u,f(u,y,v)))) = f(x,u,y). [para(1530(a,1),5(a,2)),rewrite(5(1,R),6(1),6(4),5(5),5(5))]. given #139 (T,wt=22): 4980 f(x,y,f(z,u,f(u,x,f(u,y,v)))) = f(u,x,y). [para(5(a,1),1530(a,1)),rewrite(5(1,R),6(1),5(2,R),6(2),5(4),6(4),5(5),6(5))]. given #140 (A,wt=38): 68 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(18(a,2),18(a,2,3,3))]. given #141 (T,wt=22): 4981 f(x,y,f(z,u,f(u,y,f(x,u,v)))) = f(x,u,y). [para(1530(a,1),6(a,2)),rewrite(5(2,R),6(2),6(4),6(5))]. given #142 (T,wt=22): 5002 f(x,y,f(z,u,f(u,v,f(x,y,u)))) = f(x,y,u). [para(847(a,2),1530(a,1,3,3)),rewrite(5(1,R),6(1))]. given #143 (T,wt=22): 5052 f(x,y,f(x,z,f(u,y,f(z,y,v)))) = f(x,z,y). [para(1810(a,1),793(a,2)),rewrite(6(7),1509(9))]. given #144 (T,wt=21): 6597 f(x,y,f(y,z,f(u,x,y))) = f(y,z,f(u,x,y)). [para(1106(a,1),5052(a,1,3)),rewrite(5(2),5(2),5(4),5(4),5(6,R),6(6),205(6),5(5),5(5),5(7),6(7),19(7))]. given #145 (A,wt=31): 69 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(18(a,2),18(a,2,3)),flip(a)]. given #146 (T,wt=18): 6632 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(1106(a,1),6597(a,2)),rewrite(5(1),5(2),5(2),29(4),6(2),5(4),5(4))]. given #147 (T,wt=22): 5168 f(x,y,f(z,y,f(u,x,f(z,x,v)))) = f(z,x,y). [para(1810(a,1),1986(a,2)),rewrite(5(2,R),6(2),5(5,R),6(5),5(8,R),6(8),6(10),5(11,R),6(11),5(12,R),6(12),5116(13),5(5),5(5))]. given #148 (T,wt=22): 5370 f(x,y,f(z,y,f(z,u,f(x,z,v)))) = f(x,z,y). [para(2184(a,1),24(a,1)),flip(a)]. given #149 (T,wt=22): 5697 f(x,y,f(x,z,f(u,z,f(z,y,v)))) = f(x,z,y). [para(2737(a,1),21(a,1,3)),rewrite(5(1,R),6(1),6(3),1012(4),5(2,R),6(2)),flip(a)]. given #150 (A,wt=24): 70 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,u,v))). [para(8(a,1),24(a,1,3)),rewrite(5(1,R),6(1),5(6,R),6(6))]. given #151 (T,wt=17): 6921 f(x,f(x,y,z),f(u,y,z)) = f(x,y,z). [para(1004(a,1),70(a,2,3)),rewrite(5(3),5(3),3866(4),1004(3),5(4,R)),flip(a)]. given #152 (T,wt=17): 7099 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x). [para(5(a,1),6921(a,1)),rewrite(5(2),5(2),5(3,R),5(4),5(4))]. given #153 (T,wt=20): 6930 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)). [para(1106(a,1),70(a,2,3)),rewrite(5(3),6(3),884(5),5(4),5(5,R)),flip(a)]. given #154 (T,wt=21): 6988 f(x,f(x,y,z),f(u,y,f(y,z,v))) = f(x,y,z). [para(1012(a,1),70(a,2,3)),rewrite(5(5),5(5),3889(6),1012(4),5(5,R)),flip(a)]. given #155 (A,wt=24): 71 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,u,v))). [para(8(a,1),24(a,2,3)),rewrite(5(2,R),6(2),5(6,R),6(6)),flip(a)]. given #156 (T,wt=21): 6992 f(x,f(x,y,z),f(u,y,f(y,v,z))) = f(x,y,z). [para(1021(a,1),70(a,2,3)),rewrite(5(5),5(5),3892(6),1021(4),5(5,R)),flip(a)]. given #157 (T,wt=17): 7401 f(x,f(x,y,z),f(y,u,z)) = f(x,y,z). [para(6992(a,1),3978(a,1,3)),rewrite(394(3),1005(3)),flip(a)]. given #158 (T,wt=17): 7420 f(x,f(y,z,x),f(y,u,z)) = f(y,z,x). [para(5(a,1),7401(a,1)),rewrite(5(2),5(2),5(3,R),5(4),5(4))]. given #159 (T,wt=21): 7216 f(x,f(y,z,x),f(u,y,f(y,z,v))) = f(y,z,x). [para(5(a,1),6988(a,1)),rewrite(5(3),5(3),5(4,R),5(5),5(5))]. given #160 (A,wt=24): 72 f(x,f(y,z,u),f(y,z,f(x,z,u))) = f(x,z,f(y,z,u)). [para(24(a,1),19(a,1,3))]. given #161 (T,wt=21): 7268 f(x,y,f(y,f(x,y,z),f(u,x,z))) = f(x,y,z). [para(1675(a,1),71(a,1)),rewrite(5(3,R),6(3),20(3),15(3),5(3,R),6(3)),flip(a)]. given #162 (T,wt=21): 7365 f(x,f(y,z,x),f(u,y,f(y,v,z))) = f(y,z,x). [para(5(a,1),6992(a,1)),rewrite(5(3),5(3),5(4,R),5(5),5(5))]. given #163 (T,wt=21): 7689 f(x,y,f(y,f(x,y,z),f(x,u,z))) = f(x,y,z). [para(5(a,1),7268(a,1,3)),rewrite(5(1,R),6(1),5(3,R))]. given #164 (T,wt=22): 6076 f(x,y,f(z,u,f(z,v,f(x,z,y)))) = f(x,z,y). [para(4446(a,1),5(a,2)),rewrite(5(1),5(1),6(4),5(5),5(5))]. given #165 (A,wt=24): 74 f(x,y,f(z,u,f(y,u,v))) = f(y,u,f(x,y,f(z,u,v))). [para(16(a,1),24(a,1,3)),rewrite(5(1,R),6(1),5(6,R),6(6))]. given #166 (T,wt=20): 7888 f(x,f(y,z,x),f(z,x,u)) = f(y,x,f(z,x,u)). [para(896(a,1),74(a,2,3)),rewrite(5(3),6(3),122(4),19(4),5(4),5(5,R)),flip(a)]. given #167 (T,wt=20): 7901 f(x,f(y,x,z),f(u,y,x)) = f(x,z,f(u,y,x)). [para(74(a,1),1106(a,1)),rewrite(5(3),5(3),5(6),6(6),7128(6),5(5,R),6(5),19(5),5(5),5(5),6597(6))]. given #168 (T,wt=20): 7902 f(x,f(y,z,x),f(u,z,x)) = f(y,x,f(u,z,x)). [para(1106(a,1),74(a,2,3)),rewrite(5(3),6(3),964(5),5(4),5(5,R)),flip(a)]. given #169 (T,wt=22): 6077 f(x,y,f(z,u,f(z,v,f(z,x,y)))) = f(z,x,y). [para(5(a,1),4446(a,1)),rewrite(5(1),5(4),5(4),5(5))]. given #170 (A,wt=24): 75 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(y,z,f(x,z,u))). [para(24(a,1),17(a,1,3)),flip(a)]. given #171 (T,wt=20): 8547 f(x,f(y,x,z),f(y,u,x)) = f(y,x,f(u,x,z)). [para(847(a,2),75(a,2)),rewrite(15(2),6(2)),flip(a)]. given #172 (T,wt=21): 8829 f(x,y,f(z,f(x,y,z),f(x,z,u))) = f(x,y,z). [para(75(a,2),6077(a,1,3)),rewrite(5(1),5(1),5(2),5(5),5(5))]. given #173 (T,wt=22): 6542 f(x,y,f(z,u,f(u,v,f(x,u,y)))) = f(x,u,y). [para(5002(a,1),5(a,2)),rewrite(5(1),5(1),6(4),5(5),5(5))]. given #174 (T,wt=22): 6543 f(x,y,f(z,u,f(u,v,f(u,x,y)))) = f(u,x,y). [para(5(a,1),5002(a,1)),rewrite(5(1),5(4),5(4),5(5))]. given #175 (A,wt=24): 76 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,v,u))). [para(17(a,1),24(a,2,3)),rewrite(5(2,R),6(2),5(6,R),6(6)),flip(a)]. given #176 (T,wt=22): 6638 f(x,y,f(y,z,f(u,z,f(x,z,v)))) = f(x,y,z). [para(2726(a,1),6597(a,2)),rewrite(5(1,R),6(1),5(3),5(3),29(5),6(3),5(5),5(5))]. given #177 (T,wt=22): 6828 f(x,y,f(z,x,f(u,y,f(z,y,v)))) = f(z,x,y). [para(5(a,1),5168(a,1)),rewrite(5(4),6(4),6(5))]. given #178 (T,wt=22): 7884 f(x,y,f(z,u,f(z,y,f(z,x,v)))) = f(z,x,y). [para(43(a,1),74(a,2,3)),rewrite(785(4)),flip(a)]. given #179 (T,wt=22): 8843 f(x,y,f(z,u,f(x,u,f(u,v,y)))) = f(x,u,y). [back_rewrite(4130),rewrite(8687(11))]. given #180 (A,wt=31): 77 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(24(a,1),18(a,1,3,3))]. given #181 (T,wt=22): 9180 f(x,y,f(z,u,f(u,x,f(u,v,y)))) = f(u,x,y). [para(5(a,1),8843(a,1)),rewrite(5(2,R),6(2),5(4),5(4),5(5,R),6(5))]. given #182 (T,wt=24): 82 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,v,u))). [para(25(a,2),8(a,2,3)),flip(a)]. given #183 (T,wt=24): 83 f(x,f(y,z,u),f(y,u,f(x,y,z))) = f(x,y,f(y,z,u)). [para(25(a,2),19(a,1,3))]. given #184 (T,wt=24): 87 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,v,f(x,y,u))). [para(25(a,2),24(a,2,3)),rewrite(5(2,R),6(2),5(6,R),6(6))]. given #185 (A,wt=31): 78 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(18(a,1),24(a,1,3)),rewrite(5(2,R),6(2),5(8,R),6(8))]. given #186 (T,wt=24): 90 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,u,z))). [para(8(a,1),31(a,2,3)),rewrite(57(3),6(1),6(4))]. given #187 (T,wt=24): 91 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,y,z))). [para(17(a,1),31(a,2,3)),rewrite(57(3),6(1),6(4))]. given #188 (T,wt=24): 92 f(x,y,f(x,z,f(x,u,v))) = f(x,y,f(x,v,f(x,u,z))). [para(31(a,1),18(a,1)),rewrite(57(3),6(1),6(4))]. given #189 (T,wt=24): 97 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(x,z,f(z,u,v))). [para(16(a,2),21(a,2,3)),rewrite(21(5)),flip(a)]. given #190 (A,wt=31): 79 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(18(a,2),24(a,1,3)),rewrite(5(1,R),6(1),5(8,R),6(8))]. given #191 (T,wt=21): 10556 f(x,f(y,z,f(u,y,v)),f(u,y,x)) = f(u,y,x). [para(79(a,1),815(a,1)),rewrite(5(3,R),6(3),785(4),5(4)),flip(a)]. given #192 (T,wt=21): 10713 f(x,f(y,z,x),f(z,u,f(y,z,v))) = f(y,z,x). [para(10556(a,1),6(a,1)),flip(a)]. given #193 (T,wt=24): 105 f(x,y,f(z,u,f(x,u,v))) = f(x,y,f(x,u,f(z,u,v))). [para(24(a,1),21(a,2,3)),rewrite(21(5)),flip(a)]. given #194 (T,wt=24): 107 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(x,z,f(z,v,u))). [para(25(a,2),21(a,2,3)),rewrite(21(5)),flip(a)]. given #195 (A,wt=31): 80 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(18(a,1),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. given #196 (T,wt=24): 108 f(x,y,f(y,z,f(y,u,v))) = f(x,y,f(y,u,f(y,z,v))). [para(8(a,1),29(a,2,3)),rewrite(29(4))]. Low Water (keep, True_semantics): wt=50 given #197 (T,wt=24): 111 f(x,y,f(z,u,f(y,z,v))) = f(x,y,f(y,z,f(z,u,v))). [para(16(a,2),29(a,2,3)),rewrite(29(4)),flip(a)]. given #198 (T,wt=24): 113 f(x,y,f(y,z,f(y,u,v))) = f(x,y,f(y,v,f(y,z,u))). [para(17(a,1),29(a,2,3)),rewrite(29(4))]. given #199 (T,wt=24): 120 f(x,y,f(z,u,f(y,z,v))) = f(x,y,f(y,z,f(z,v,u))). [para(25(a,2),29(a,2,3)),rewrite(29(4)),flip(a)]. given #200 (A,wt=31): 81 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(18(a,2),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. Low Water (keep, True_semantics): wt=49 given #201 (T,wt=24): 125 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,x,f(z,u,v))). [para(8(a,1),122(a,1,3,3)),rewrite(5(3,R),6(3),103(4),5(6,R),6(6))]. given #202 (T,wt=18): 12063 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z). [para(1675(a,1),125(a,1)),rewrite(5(3,R),6(3),20(3),15(3),5(3,R),6(3),369(5),6(3)),flip(a)]. Low Water (keep, True_semantics): wt=48 given #203 (T,wt=18): 12149 f(x,y,f(x,z,f(u,z,y))) = f(x,z,y). [para(12063(a,1),503(a,2)),rewrite(5(3,R),6(3),21(5),5(4,R),6(4))]. given #204 (T,wt=24): 130 f(x,y,f(z,u,f(z,y,v))) = f(z,y,f(x,y,f(z,u,v))). [para(26(a,1),5(a,2)),rewrite(5(1,R),6(1),6(3),5(5,R),6(5),5(6,R),6(6))]. given #205 (A,wt=31): 85 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(25(a,2),18(a,2,3,3)),flip(a)]. given #206 (T,wt=24): 133 f(x,f(y,z,u),f(y,z,f(y,x,u))) = f(y,z,f(y,x,u)). [para(15(a,1),26(a,1)),rewrite(5(1,R),6(1),5(3,R),6(3),6(6),5(7,R),6(7),103(7)),flip(a)]. given #207 (T,wt=21): 12539 f(x,y,f(z,x,f(u,x,y))) = f(z,x,f(u,x,y)). [para(205(a,1),133(a,1,2)),rewrite(5(3,R),6(3),884(5),5(4,R),6(4)),flip(a)]. given #208 (T,wt=21): 12586 f(x,f(y,z,f(u,z,v)),f(u,x,z)) = f(u,x,z). [para(2752(a,1),133(a,1,3)),rewrite(6(3),5(4,R),6(4),6(5),12160(5),6828(4),19(2),5(4,R),6(4)),flip(a)]. given #209 (T,wt=24): 169 f(x,f(y,z,u),f(y,z,f(y,u,x))) = f(y,x,f(y,z,u)). [para(28(a,1),5(a,2)),rewrite(5(2),5(2),5(4),5(6,R),6(6))]. given #210 (A,wt=31): 86 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(18(a,2),25(a,2,3)),rewrite(5(3,R),6(3),57(4),6(5),5(8,R),6(8)),flip(a)]. given #211 (T,wt=17): 12727 f(x,f(y,z,u),f(y,u,x)) = f(y,u,x). [para(1005(a,1),169(a,1,3)),rewrite(5(2),5(2),5(3),5(3),15(4),5(3),5(3)),flip(a)]. given #212 (T,wt=20): 12961 f(x,f(y,z,x),f(z,u,x)) = f(y,x,f(z,u,x)). [para(12727(a,1),74(a,2,3)),rewrite(5(3),6(3),964(5),5(4),5(5,R)),flip(a)]. given #213 (T,wt=21): 12752 f(x,f(y,z,f(y,u,v)),f(y,v,x)) = f(y,v,x). [para(1015(a,1),169(a,1,3)),rewrite(5(3),5(3),5(4),5(4),15(5),5(4),5(4)),flip(a)]. Low Water (keep, True_semantics): wt=47 given #214 (T,wt=21): 12957 f(x,y,f(y,z,f(x,u,y))) = f(y,z,f(x,u,y)). [para(12727(a,1),5052(a,1,3)),rewrite(5(2),5(2),5(4),5(4),5(6,R),6(6),205(6),5(5),5(5),5(7),6(7),19(7))]. given #215 (A,wt=31): 93 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(18(a,1),31(a,2,3)),rewrite(57(4)),flip(a)]. given #216 (T,wt=22): 13048 f(x,y,f(z,u,f(x,z,f(z,v,y)))) = f(x,z,y). [para(12752(a,1),1005(a,2)),rewrite(5(3),5(6),5(7,R),12149(9),12160(4),5(5))]. given #217 (T,wt=22): 13121 f(x,y,f(y,z,f(x,u,f(x,v,z)))) = f(x,y,z). [para(2858(a,1),12957(a,2)),rewrite(5(2,R),6(2),6(3),29(5),6(3),6(5))]. given #218 (T,wt=22): 13296 f(x,y,f(z,u,f(z,x,f(z,v,y)))) = f(z,x,y). [para(5(a,1),13048(a,1)),rewrite(5(2,R),6(2),5(4),5(4),5(5,R),6(5))]. given #219 (T,wt=22): 13342 f(x,y,f(x,z,f(z,u,f(z,v,y)))) = f(x,z,y). [para(13121(a,1),503(a,2)),rewrite(5(5,R),6(5),21(7),5(5,R),6(5))]. given #220 (A,wt=31): 94 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(18(a,2),31(a,2,3)),rewrite(57(4),6(5))]. given #221 (T,wt=24): 170 f(x,f(y,z,u),f(z,u,f(x,y,z))) = f(x,z,f(y,z,u)). [para(5(a,1),28(a,1,2)),rewrite(6(2),5(5))]. given #222 (T,wt=20): 13589 f(x,f(y,z,x),f(u,y,x)) = f(u,x,f(y,z,x)). [para(19(a,1),170(a,1,2)),rewrite(7441(5),19(5))]. given #223 (T,wt=20): 13734 f(x,f(y,z,x),f(y,x,u)) = f(x,u,f(y,z,x)). [para(13589(a,1),5(a,2)),rewrite(5(2),5(2),5(3),5(5,R),6(5))]. given #224 (T,wt=24): 171 f(x,f(y,z,u),f(y,u,f(x,z,u))) = f(x,u,f(y,z,u)). [para(5(a,2),28(a,1,2)),rewrite(6(2),5(3,R),6(3),5(5),5(5))]. given #225 (A,wt=28): 95 f(x,y,f(x,z,f(y,u,f(x,y,v)))) = f(x,z,f(y,u,f(x,y,v))). [para(21(a,1),16(a,1,3)),rewrite(5(1),5(4),5(7,R),6(7)),flip(a)]. Low Water (keep, True_semantics): wt=46 given #226 (T,wt=24): 210 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,y,u))). [para(132(a,1),31(a,2,3)),rewrite(205(2),57(3),6(1))]. given #227 (T,wt=24): 216 f(x,y,f(z,u,f(z,y,v))) = f(x,y,f(z,y,f(z,u,v))). [para(26(a,1),205(a,1,3)),rewrite(5(1,R),6(1),5(4,R),6(4),5(5,R),6(5),177(6),5(4,R),6(4),5(6,R),6(6)),flip(a)]. given #228 (T,wt=24): 220 f(x,y,f(z,u,f(u,y,v))) = f(u,y,f(x,y,f(z,u,v))). [para(30(a,1),5(a,2)),rewrite(5(1,R),6(1),6(3),5(5,R),6(5),5(6,R),6(6))]. Low Water (keep, True_semantics): wt=45 given #229 (T,wt=24): 221 f(x,y,f(z,u,f(u,x,v))) = f(u,x,f(x,y,f(z,u,v))). [para(5(a,1),30(a,1)),rewrite(5(1,R),6(1),5(3),5(3),5(6,R),6(6))]. given #230 (A,wt=31): 96 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(16(a,2),21(a,1,3,3))]. given #231 (T,wt=24): 264 f(x,y,f(z,u,f(u,y,v))) = f(x,y,f(u,y,f(z,u,v))). [para(30(a,1),205(a,1,3)),rewrite(5(1,R),6(1),5(4,R),6(4),5(5,R),6(5),188(6),5(4,R),6(4),5(6,R),6(6)),flip(a)]. given #232 (T,wt=24): 268 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,v,y))). [para(32(a,1),5(a,2)),rewrite(6(3),5(5,R),6(5)),flip(a)]. given #233 (T,wt=24): 320 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,z,f(y,u,x))). [para(38(a,1),5(a,2)),rewrite(5(2),5(3),5(4),5(4))]. given #234 (T,wt=20): 14699 f(f(x,y,z),f(z,u,v),f(x,y,z)) = f(x,y,z). [para(1006(a,1),320(a,1,3)),rewrite(8417(10))]. given #235 (A,wt=35): 98 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(21(a,1),18(a,1,3,3)),flip(a)]. given #236 (T,wt=20): 14701 f(f(x,y,z),f(y,u,v),f(x,y,z)) = f(x,y,z). [para(1075(a,1),320(a,1,3)),rewrite(8418(10))]. given #237 (T,wt=20): 14858 f(f(x,y,z),f(x,u,v),f(x,y,z)) = f(x,y,z). [para(320(a,1),216(a,2)),rewrite(6(4),4(6),19(5),20(5)),flip(a)]. given #238 (T,wt=24): 321 f(x,f(y,z,u),f(v,y,x)) = f(v,x,f(y,z,f(y,x,u))). [para(38(a,2),5(a,2)),rewrite(5(1,R),6(1),6(3),5(5),5(5)),flip(a)]. given #239 (T,wt=17): 15275 f(x,f(y,x,z),f(u,y,z)) = f(y,x,z). [para(321(a,2),6597(a,1,3)),rewrite(5(2,R),6(2),5(4),5(4),20(4),7433(5),5(6,R),6(6),5(7,R),6(7),3625(7),1855(6))]. given #240 (A,wt=35): 99 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(18(a,1),21(a,1,3,3)),rewrite(57(7),6(5),57(5),6(3),21(3),20(4))]. given #241 (T,wt=17): 15276 f(x,f(y,z,u),f(z,x,u)) = f(z,x,u). [para(321(a,2),6597(a,2)),rewrite(5(4,R),6(4),5(5,R),6(5),3625(5),1855(4),15(3),5(2,R),6(2),5(4),5(4),20(4)),flip(a)]. given #242 (T,wt=18): 15371 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y). [back_rewrite(5381),rewrite(15268(9))]. given #243 (T,wt=20): 15244 f(f(x,y,z),f(u,v,w),f(x,y,z)) = f(x,y,z). [para(321(a,1),54(a,2,3)),rewrite(5(5),5(5),19(5),20(5),5(5,R),15(5),6(9),4(11),5(7,R),15(7))]. given #244 (T,wt=22): 15370 f(x,y,f(z,u,f(z,y,f(z,v,x)))) = f(z,x,y). [back_rewrite(13044),rewrite(15230(9),6(2))]. given #245 (A,wt=31): 100 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(18(a,2),21(a,1,3,3)),rewrite(6(3),57(7),6(5),57(5),6(3),22(3),22(4),22(5))]. given #246 (T,wt=17): 15801 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(15370(a,1),896(a,1,2)),rewrite(5(2),5(4))]. given #247 (T,wt=17): 15824 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(15370(a,1),2752(a,1,2))]. given #248 (T,wt=17): 15852 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(15370(a,1),5129(a,1,2)),rewrite(5(2,R),6(2),5(4,R),6(4))]. given #249 (T,wt=17): 16077 f(x,f(y,z,u),f(y,x,u)) = f(y,x,u). [para(15801(a,1),133(a,1,3)),rewrite(5(1,R),6(1),6(2),5(3,R),6(3),6(4),15462(4),785(4),5(2,R),6(2),5(3,R),6(3)),flip(a)]. given #250 (A,wt=31): 101 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(18(a,1),21(a,2,3)),rewrite(21(7))]. given #251 (T,wt=21): 15823 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(15370(a,1),2726(a,1,2,3)),rewrite(5(1,R),6(1),5(3),5(5))]. given #252 (T,wt=21): 15827 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(15370(a,1),3418(a,1,2,3)),rewrite(5(1,R),6(1),5(3),5(5))]. given #253 (T,wt=21): 16009 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(2726(a,1),15801(a,2)),rewrite(5(3),5(7),15801(9),5(5))]. given #254 (T,wt=21): 16013 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(3418(a,1),15801(a,2)),rewrite(5(3),5(7),15801(9),5(5))]. given #255 (A,wt=28): 102 f(x,y,f(z,x,f(y,u,f(x,y,v)))) = f(z,x,f(y,u,f(x,y,v))). [para(21(a,1),24(a,1,3)),rewrite(5(1),5(4),5(7,R),6(7)),flip(a)]. given #256 (T,wt=21): 16360 f(x,f(y,z,f(y,u,v)),f(y,x,v)) = f(y,x,v). [para(15823(a,1),133(a,1,3)),rewrite(5(2,R),6(2),6(3),5(4,R),6(4),6(5),15462(5),12628(4),13121(4),5(3,R),6(3),5(4,R),6(4)),flip(a)]. given #257 (T,wt=24): 323 f(x,f(y,z,u),f(x,u,v)) = f(x,v,f(y,u,f(x,z,u))). [para(5(a,2),38(a,1,2)),rewrite(6(2),6(4),5(5,R),6(5))]. given #258 (T,wt=20): 16618 f(x,f(y,z,x),f(y,u,x)) = f(y,x,f(u,z,x)). [para(847(a,2),323(a,2)),rewrite(15(2),6(2)),flip(a)]. given #259 (T,wt=21): 16537 f(x,y,f(z,y,f(x,u,y))) = f(x,y,f(z,u,y)). [para(15(a,1),323(a,1,3)),rewrite(6(2)),flip(a)]. given #260 (A,wt=28): 103 f(x,y,f(y,z,f(x,u,f(x,y,v)))) = f(y,z,f(x,u,f(x,y,v))). [para(21(a,1),24(a,2,3)),rewrite(6(1),5(3,R),6(3),6(5),5(7,R),6(7))]. given #261 (T,wt=24): 464 f(x,y,f(z,y,f(y,u,v))) = f(z,y,f(y,u,f(x,y,v))). [para(40(a,1),5(a,2)),rewrite(6(3),5(4,R),6(4))]. given #262 (T,wt=24): 500 f(x,y,f(y,z,f(y,u,v))) = f(y,u,f(y,z,f(x,y,v))). [para(41(a,2),8(a,1))]. given #263 (T,wt=24): 507 f(x,f(y,x,z),f(x,u,v)) = f(y,x,f(x,u,f(x,v,z))). [para(41(a,2),17(a,1)),flip(a)]. given #264 (T,wt=24): 508 f(x,y,f(y,z,f(y,u,v))) = f(y,u,f(y,v,f(x,y,z))). [para(17(a,1),41(a,1,3))]. given #265 (A,wt=31): 104 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(24(a,1),21(a,1,3,3))]. given #266 (T,wt=22): 17932 f(x,y,f(x,z,f(u,z,f(z,v,y)))) = f(x,z,y). [para(8843(a,1),104(a,1,3)),rewrite(15823(4)),flip(a)]. given #267 (T,wt=24): 510 f(x,y,f(y,z,f(y,u,v))) = f(y,v,f(y,z,f(x,y,u))). [para(17(a,2),41(a,1,3))]. given #268 (T,wt=24): 524 f(x,y,f(y,z,f(y,u,v))) = f(y,v,f(y,u,f(x,y,z))). [para(31(a,1),41(a,1,3))]. given #269 (T,wt=24): 577 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,v,f(z,x,u))). [para(503(a,1),24(a,2,3)),rewrite(5(1),5(1),5(3,R),6(3),103(4),6(4),5(5,R),6(5),5(6,R),6(6))]. given #270 (A,wt=31): 106 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(25(a,2),21(a,1,3,3))]. given #271 (T,wt=22): 18416 f(x,y,f(z,u,f(y,u,f(x,z,u)))) = f(x,y,u). [para(577(a,1),9180(a,1,3)),rewrite(5(1),6(1),5(2,R),6(2),5(5),5(5))]. given #272 (T,wt=18): 18567 f(x,y,f(z,y,f(x,u,z))) = f(x,z,y). [para(18416(a,1),6(a,2)),rewrite(5(2,R),6(2),6597(3),6(3),6(4))]. given #273 (T,wt=18): 18598 f(x,y,f(z,y,f(z,u,x))) = f(z,x,y). [para(18416(a,1),4042(a,2)),rewrite(5(2,R),6(2),6597(3),5(5,R),6(5),6597(6),6(6),4329(8),6(4))]. given #274 (T,wt=24): 676 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(z,v,f(x,z,u))). [para(503(a,1),603(a,1,3)),rewrite(5(1),6(1),5(4),5(5,R),6(5),6(6),601(6),5(4),6(4),5(7,R),6(7),95(7))]. given #275 (A,wt=28): 110 f(x,y,f(y,z,f(y,u,f(x,y,v)))) = f(x,y,f(y,z,f(y,u,v))). [para(16(a,2),29(a,1,3,3))]. given #276 (T,wt=24): 799 f(x,y,f(x,f(z,y,u),f(x,v,z))) = f(x,v,f(x,z,y)). [back_rewrite(414),rewrite(794(3)),flip(a)]. Low Water (keep, True_semantics): wt=44 given #277 (T,wt=21): 18936 f(x,f(y,z,f(u,v,y)),f(x,u,y)) = f(x,u,y). [para(1005(a,1),799(a,2)),rewrite(6(3),2067(6))]. given #278 (T,wt=21): 18961 f(x,f(y,z,f(u,v,y)),f(x,v,y)) = f(x,v,y). [para(3866(a,1),799(a,2)),rewrite(6(3),1107(6))]. given #279 (T,wt=21): 19195 f(x,f(y,z,f(u,v,z)),f(x,v,z)) = f(x,v,z). [para(5(a,2),18961(a,1,2)),rewrite(6(2))]. given #280 (A,wt=35): 114 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(29(a,1),18(a,1,3,3)),flip(a)]. given #281 (T,wt=24): 831 f(x,f(y,z,u),f(x,v,f(x,y,z))) = f(x,v,f(x,y,z)). [para(785(a,1),32(a,1,3)),flip(a)]. given #282 (T,wt=24): 832 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,u,y))). [para(32(a,1),785(a,2)),rewrite(6(5),639(6),57(6),6(4),812(7))]. given #283 (T,wt=24): 839 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(z,x,f(x,y,v))). [para(40(a,2),785(a,2)),rewrite(6(5),808(7))]. given #284 (T,wt=24): 844 f(x,y,f(z,x,f(x,u,v))) = f(x,y,f(x,u,f(z,x,v))). [para(41(a,1),785(a,2)),rewrite(6(5),808(7))]. given #285 (A,wt=31): 115 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(29(a,1),18(a,2,3,3)),rewrite(95(4))]. given #286 (T,wt=24): 879 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(x,z,f(v,z,u))). [para(847(a,2),21(a,2,3)),rewrite(21(5)),flip(a)]. given #287 (T,wt=24): 904 f(x,y,f(z,u,f(x,v,z))) = f(x,z,f(x,y,f(v,z,u))). [para(847(a,2),503(a,2,3)),rewrite(5(3,R),6(3),21(5),5(6,R),6(6)),flip(a)]. given #288 (T,wt=24): 971 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(x,u,f(z,v,u))). [para(871(a,1),21(a,2,3)),rewrite(21(5)),flip(a)]. given #289 (T,wt=24): 997 f(x,y,f(z,u,f(x,v,u))) = f(x,u,f(x,y,f(z,v,u))). [para(871(a,1),503(a,2,3)),rewrite(5(3,R),6(3),21(5),5(6,R),6(6)),flip(a)]. given #290 (A,wt=35): 116 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(18(a,2),29(a,1,3,3))]. given #291 (T,wt=24): 1048 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,z,f(y,x,u))). [para(38(a,2),896(a,2)),rewrite(5(1,R),6(1),5(4,R),6(4),896(7),5(5)),flip(a)]. given #292 (T,wt=24): 1066 f(x,y,f(x,f(z,u,v),f(y,z,u))) = f(x,y,f(z,u,v)). [para(896(a,1),785(a,1,3,3)),rewrite(5(2))]. Low Water (keep, True_semantics): wt=43 given #293 (T,wt=21): 20067 f(x,y,f(z,f(x,y,z),f(u,v,w))) = f(x,y,z). [para(1066(a,1),6085(a,1,3))]. given #294 (T,wt=21): 20196 f(x,y,f(z,f(x,z,y),f(u,v,w))) = f(x,z,y). [para(20067(a,1),5(a,2)),rewrite(5(1),5(1),6(4),5(5),5(5))]. given #295 (A,wt=28): 118 f(x,y,f(z,x,f(x,u,f(x,y,v)))) = f(z,x,f(x,y,f(x,u,v))). [para(29(a,1),24(a,1,3)),rewrite(5(2,R),6(2),5(4,R),6(4),5(7,R),6(7)),flip(a)]. given #296 (T,wt=24): 1067 f(f(x,y,z),f(x,y,f(y,z,u)),f(x,z,v)) = f(x,y,z). [para(785(a,1),896(a,1,3)),rewrite(5(1,R),6(1),6(4),5(5),5(6,R),6(6),800(8))]. given #297 (T,wt=24): 1070 f(x,f(y,z,x),f(u,f(y,z,v),f(y,z,x))) = f(y,z,x). [para(896(a,1),847(a,1,3)),rewrite(5(3,R),15(3),5(5)),flip(a)]. given #298 (T,wt=24): 1074 f(x,f(y,z,u),f(x,u,f(y,z,v))) = f(x,u,f(y,z,v)). [para(896(a,1),896(a,1,2)),rewrite(5(3),5(6))]. given #299 (T,wt=24): 1091 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,z,f(x,y,u))). [para(38(a,2),899(a,2)),rewrite(6(3),5(6,R),6(6),394(7),1005(7),5(5,R),6(5)),flip(a)]. given #300 (A,wt=28): 123 f(x,y,f(x,z,f(u,y,f(x,y,v)))) = f(x,z,f(u,y,f(x,y,v))). [para(73(a,1),16(a,1,3)),rewrite(5(1,R),6(1),5(4,R),6(4),5(7,R),6(7)),flip(a)]. given #301 (T,wt=24): 1100 f(x,f(y,x,z),f(u,f(y,z,v),f(y,x,z))) = f(y,x,z). [para(899(a,1),847(a,1,3)),rewrite(5(3,R),15(3),5(5)),flip(a)]. given #302 (T,wt=24): 1103 f(f(x,y,z),f(x,y,u),f(u,v,f(x,y,u))) = f(x,y,u). [para(896(a,1),899(a,1,3)),rewrite(6(3),6(5),896(8))]. given #303 (T,wt=24): 1107 f(x,f(y,z,u),f(x,v,f(x,z,u))) = f(x,v,f(x,z,u)). [para(1004(a,1),8(a,2,3))]. given #304 (T,wt=24): 1143 f(x,f(y,z,u),f(x,u,f(x,z,v))) = f(x,v,f(x,z,u)). [para(1004(a,1),33(a,2,3)),rewrite(6(2))]. Low Water (keep, True_semantics): wt=42 given #305 (A,wt=28): 124 f(x,y,f(z,x,f(u,y,f(x,y,v)))) = f(z,x,f(u,y,f(x,y,v))). [para(73(a,1),24(a,1,3)),rewrite(5(1,R),6(1),5(4,R),6(4),5(7,R),6(7)),flip(a)]. given #306 (T,wt=24): 1158 f(x,y,f(x,f(z,x,u),f(y,u,v))) = f(z,x,f(x,y,u)). [para(1004(a,1),41(a,1,3)),rewrite(5(3),5(3),394(6)),flip(a)]. given #307 (T,wt=24): 1182 f(x,y,f(x,f(z,u,v),f(y,u,v))) = f(x,y,f(z,u,v)). [para(1004(a,1),785(a,1,3,3))]. given #308 (T,wt=24): 1186 f(x,y,f(x,f(y,z,u),f(x,v,z))) = f(x,v,f(x,y,z)). [para(1004(a,1),43(a,1,3)),rewrite(5(3),5(3)),flip(a)]. given #309 (T,wt=24): 1191 f(f(x,y,z),f(y,z,u),f(u,v,f(y,z,u))) = f(y,z,u). [para(1004(a,1),899(a,1,3)),rewrite(5(2),5(2),6(3),5(4),5(4),6(5),5(7),5(7),1106(8))]. given #310 (A,wt=35): 127 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(122(a,1),18(a,1,3,3)),flip(a)]. given #311 (T,wt=24): 1307 f(x,f(y,z,x),f(u,f(y,z,x),f(y,z,v))) = f(y,z,x). [para(1006(a,1),24(a,1,3)),rewrite(15(3)),flip(a)]. Low Water (keep, True_semantics): wt=41 given #312 (T,wt=24): 1344 f(f(x,y,z),f(x,z,u),f(x,y,f(y,z,v))) = f(x,y,z). [para(785(a,1),1006(a,1,2)),rewrite(5(1,R),6(1),6(3),5(5,R),5(6,R),6(6),800(8))]. given #313 (T,wt=24): 1345 f(f(x,y,z),f(x,y,u),f(z,v,f(x,y,z))) = f(x,y,z). [para(1006(a,1),815(a,1,3)),rewrite(5(3,R),15(3),6(5)),flip(a)]. given #314 (T,wt=24): 1378 f(f(x,y,z),f(y,z,u),f(x,v,f(x,y,z))) = f(x,y,z). [para(1007(a,1),815(a,1,3)),rewrite(5(3,R),15(3),6(5)),flip(a)]. given #315 (A,wt=31): 128 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(18(a,1),122(a,1,3,3)),rewrite(5(4,R),6(4),103(5),5(8,R),6(8))]. given #316 (T,wt=24): 1382 f(x,f(y,x,z),f(u,f(y,x,z),f(y,z,v))) = f(y,x,z). [para(1075(a,1),24(a,1,3)),rewrite(15(3)),flip(a)]. given #317 (T,wt=24): 1397 f(f(x,y,z),f(x,z,u),f(y,v,f(x,y,z))) = f(x,y,z). [para(1075(a,1),815(a,1,3)),rewrite(5(3,R),15(3),6(5)),flip(a)]. given #318 (T,wt=24): 1424 f(f(x,y,z),f(x,y,u),f(v,u,f(x,y,u))) = f(x,y,u). [para(1006(a,1),1106(a,1,3)),rewrite(6(5),1006(8))]. given #319 (T,wt=24): 1497 f(f(x,y,z),f(x,y,f(x,z,u)),f(y,z,v)) = f(x,y,z). [para(791(a,1),896(a,1,3)),rewrite(5(1,R),6(1),5(3,R),6(3),5(4),5(4),5(5),5(6,R),6(6),794(8),6(6))]. given #320 (A,wt=31): 131 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(8(a,1),26(a,1,3,3))]. given #321 (T,wt=24): 1498 f(x,y,f(y,f(x,z,u),f(z,u,v))) = f(x,y,f(z,u,v)). [para(896(a,1),791(a,1,3,3)),rewrite(5(2),5(3,R),6(6))]. Low Water (keep, True_semantics): wt=40 given #322 (T,wt=21): 22663 f(x,y,f(z,f(y,z,u),f(x,v,z))) = f(x,y,z). [para(1530(a,1),1498(a,1,3)),rewrite(6(2),6632(3),5(4,R),6597(5)),flip(a)]. given #323 (T,wt=24): 1502 f(x,y,f(y,f(x,z,u),f(v,z,u))) = f(x,y,f(v,z,u)). [para(1004(a,1),791(a,1,3,3)),rewrite(5(3,R),6(6))]. given #324 (T,wt=24): 1505 f(f(x,y,z),f(y,z,u),f(x,y,f(x,z,v))) = f(x,y,z). [para(791(a,1),1006(a,1,2)),rewrite(5(1,R),6(1),5(3),5(3),5(4,R),6(4),5(5,R),5(6,R),6(6),794(8),6(6))]. given #325 (A,wt=31): 134 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(26(a,1),16(a,1,3)),rewrite(5(2,R),6(2),5(8,R),6(8))]. given #326 (T,wt=24): 1515 f(x,y,f(y,f(z,u,v),f(x,z,u))) = f(x,y,f(z,u,v)). [para(896(a,1),793(a,1,3,3)),rewrite(5(2))]. given #327 (T,wt=24): 1517 f(x,y,f(y,f(z,u,v),f(x,u,v))) = f(x,y,f(z,u,v)). [para(1004(a,1),793(a,1,3,3))]. given #328 (T,wt=24): 1549 f(x,f(y,z,f(x,u,y)),f(x,v,u)) = f(x,v,f(x,u,y)). [para(798(a,1),17(a,1,3)),flip(a)]. given #329 (T,wt=24): 1588 f(f(x,y,z),f(x,u,f(x,y,z)),f(y,z,v)) = f(x,y,z). [para(798(a,1),896(a,1,3)),rewrite(5(1),5(4),5(5),5(6),1545(8))]. given #330 (A,wt=31): 136 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(17(a,1),26(a,2,3,3))]. Low Water (keep, True_semantics): wt=39 given #331 (T,wt=24): 1670 f(x,f(y,z,u),f(x,v,f(y,z,v))) = f(x,v,f(y,z,u)). [para(896(a,1),800(a,1,3,3))]. given #332 (T,wt=24): 1671 f(x,f(y,z,u),f(x,v,f(z,u,v))) = f(x,v,f(y,z,u)). [para(1004(a,1),800(a,1,3,3)),rewrite(5(2),5(2))]. given #333 (T,wt=24): 1700 f(x,f(y,z,u),f(x,u,v)) = f(x,v,f(z,u,f(x,y,u))). [para(1668(a,1),815(a,2,3)),rewrite(5(2,R),6(2),5(4))]. given #334 (T,wt=24): 1704 f(f(x,y,z),f(x,u,y),f(u,v,f(x,u,y))) = f(x,u,y). [para(899(a,1),1668(a,1,3)),rewrite(5(3,R),15(3),6(5)),flip(a)]. Low Water (keep, True_semantics): wt=38 given #335 (A,wt=38): 137 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(26(a,1),18(a,1,3,3)),flip(a)]. given #336 (T,wt=24): 1705 f(f(x,y,z),f(u,x,y),f(u,v,f(u,x,y))) = f(u,x,y). [para(1004(a,1),1668(a,1,3)),rewrite(5(3,R),15(3),5(2),5(2),6(5)),flip(a)]. given #337 (T,wt=24): 1720 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(x,u,f(v,z,u))). [para(1675(a,1),21(a,2,3)),rewrite(21(5)),flip(a)]. given #338 (T,wt=24): 1744 f(x,y,f(z,u,f(x,v,u))) = f(x,u,f(x,y,f(v,z,u))). [para(1675(a,1),503(a,2,3)),rewrite(5(3,R),6(3),21(5),5(6,R),6(6)),flip(a)]. given #339 (T,wt=24): 1752 f(f(x,y,z),f(x,u,y),f(v,u,f(x,u,y))) = f(x,u,y). [para(899(a,1),1675(a,1,3)),rewrite(15(3)),flip(a)]. given #340 (A,wt=38): 138 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(26(a,2),18(a,1,3,3))]. given #341 (T,wt=24): 1753 f(f(x,y,z),f(u,x,y),f(v,u,f(u,x,y))) = f(u,x,y). [para(1004(a,1),1675(a,1,3)),rewrite(15(3),5(2),5(2)),flip(a)]. given #342 (T,wt=24): 1809 f(x,y,f(z,y,f(y,u,v))) = f(x,y,f(y,u,f(z,y,v))). [para(40(a,1),802(a,2)),rewrite(6(5),5(6,R),6(6),1657(7),5(4,R),6(4))]. given #343 (T,wt=24): 1811 f(x,f(y,z,u),f(y,z,f(z,u,x))) = f(z,x,f(y,z,u)). [para(574(a,1),802(a,1,3)),rewrite(6(2),5(4,R),6(4),6(6))]. given #344 (T,wt=24): 1883 f(f(x,y,z),f(u,x,f(x,y,z)),f(y,z,v)) = f(x,y,z). [para(964(a,1),896(a,1,3)),rewrite(5(1,R),6(1),5(4,R),6(4),5(5),5(6,R),6(6),1855(8))]. given #345 (A,wt=38): 139 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(26(a,1),18(a,2,3,3))]. given #346 (T,wt=24): 1888 f(f(x,y,z),f(y,z,u),f(v,x,f(x,y,z))) = f(x,y,z). [para(964(a,1),1006(a,1,2)),rewrite(5(1,R),6(1),5(3,R),6(3),5(5,R),5(6,R),6(6),1855(8))]. given #347 (T,wt=24): 2067 f(x,f(y,z,u),f(x,v,f(x,y,u))) = f(x,v,f(x,y,u)). [para(1005(a,1),50(a,1,3,3)),rewrite(1005(7))]. given #348 (T,wt=24): 3998 f(f(x,y,z),f(x,y,f(y,u,z)),f(x,z,v)) = f(x,y,z). [para(3866(a,1),896(a,1,3)),rewrite(5(1),6(4),5(5),5(6),3978(8))]. given #349 (T,wt=24): 4001 f(f(x,y,z),f(x,z,u),f(x,y,f(y,v,z))) = f(x,y,z). [para(3866(a,1),1006(a,1,2)),rewrite(5(1),6(3),5(5,R),5(6),3978(8))]. given #350 (A,wt=38): 140 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(26(a,2),18(a,2,3,3)),flip(a)]. given #351 (T,wt=24): 4720 f(x,y,f(x,f(z,u,v),f(y,z,v))) = f(x,y,f(z,u,v)). [para(1005(a,1),1015(a,1,3,3))]. given #352 (T,wt=24): 4803 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(x,y,f(z,x,v))). [para(41(a,1),1519(a,2)),rewrite(6(7),639(8),57(8),6(6),5(9,R),6(9),4800(10))]. given #353 (T,wt=24): 5117 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(z,x,f(x,y,u))). [para(32(a,1),1986(a,2)),rewrite(6(7),5(8,R),6(8),5(9,R),6(9),394(10),6(9),4645(10),5(5,R),6(5))]. given #354 (T,wt=24): 5118 f(x,y,f(z,x,f(x,u,v))) = f(x,y,f(x,v,f(z,x,u))). [para(33(a,2),1986(a,2)),rewrite(6(7),5(8,R),6(8),5(9,R),6(9),394(10),6(9),4645(10),5(4,R),6(4))]. given #355 (A,wt=31): 141 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(26(a,2),18(a,2,3)),flip(a)]. given #356 (T,wt=24): 5161 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,v,f(x,y,u))). [para(59(a,1),1986(a,2)),rewrite(6(7),5(8,R),6(8),5(9,R),6(9),394(10),6(9),4645(10),5(6,R),6(6))]. given #357 (T,wt=24): 5167 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(x,v,f(z,x,y))). [para(62(a,1),1986(a,2)),rewrite(6(7),5(8,R),6(8),5(9,R),6(9),394(10),6(9),4645(10),5(4,R),6(4))]. given #358 (T,wt=24): 5833 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(z,x,f(x,u,y))). [para(32(a,1),3477(a,2)),rewrite(5(5,R),6(5),57(7),5827(8),5(5,R),6(5))]. given #359 (T,wt=24): 5876 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,v,f(x,u,y))). [para(59(a,1),3477(a,2)),rewrite(5(5,R),6(5),57(7),5827(8),5(6,R),6(6))]. given #360 (A,wt=38): 142 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(18(a,1),26(a,1,3,3))]. given #361 (T,wt=24): 6052 f(x,f(y,z,f(x,u,y)),f(v,x,u)) = f(x,y,f(v,x,u)). [para(1004(a,1),4415(a,1,3,3)),rewrite(5(2),5(2),5(4,R),5(6))]. given #362 (T,wt=24): 6453 f(x,f(y,z,f(x,u,z)),f(v,x,u)) = f(x,z,f(v,x,u)). [para(1004(a,1),4980(a,1,3,3)),rewrite(5(2),5(2),5(4,R),5(6))]. given #363 (T,wt=24): 6853 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,v,u))). [para(5(a,1),70(a,1,3)),rewrite(5(2),5(2),6(4))]. given #364 (T,wt=24): 7125 f(f(x,y,z),f(y,z,u),f(v,u,f(y,z,u))) = f(y,z,u). [para(6921(a,1),1106(a,1,3)),rewrite(5(2),5(2),5(4),5(4),6(5),5(6),5(6),7099(8))]. given #365 (A,wt=38): 143 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(18(a,2),26(a,1,3,3))]. given #366 (T,wt=24): 7434 f(f(x,y,z),f(x,z,u),f(u,v,f(x,z,u))) = f(x,z,u). [para(7401(a,1),896(a,1,3)),rewrite(5(2),5(2),6(3),5(4),5(4),6(5),5(6),5(6),7420(8))]. given #367 (T,wt=24): 7437 f(f(x,y,z),f(x,z,u),f(v,u,f(x,z,u))) = f(x,z,u). [para(7401(a,1),1106(a,1,3)),rewrite(5(2),5(2),5(4),5(4),6(5),5(6),5(6),7420(8))]. given #368 (T,wt=24): 7456 f(x,f(y,z,u),f(x,v,f(y,u,v))) = f(x,v,f(y,z,u)). [para(7401(a,1),3978(a,1,3,3)),rewrite(5(2),5(2))]. given #369 (T,wt=24): 7472 f(x,y,f(y,f(z,u,v),f(x,z,v))) = f(x,y,f(z,u,v)). [para(7401(a,1),6632(a,1,3,3))]. given #370 (A,wt=38): 144 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(18(a,1),26(a,2,3,3))]. given #371 (T,wt=24): 7475 f(x,f(y,z,u),f(y,z,f(z,x,u))) = f(z,x,f(y,z,u)). [para(5(a,1),72(a,1)),rewrite(5(1,R),6(1),5(4),5(4),5(6,R),6(6))]. given #372 (T,wt=24): 7478 f(x,y,f(z,u,f(z,y,v))) = f(x,y,f(z,y,f(z,v,u))). [para(17(a,1),72(a,2,3)),rewrite(72(6)),flip(a)]. given #373 (T,wt=24): 7482 f(x,y,f(z,y,f(y,u,v))) = f(x,y,f(y,v,f(z,y,u))). [para(25(a,2),72(a,2,3)),rewrite(72(6))]. given #374 (T,wt=24): 7760 f(x,y,f(y,f(x,z,u),f(z,v,u))) = f(x,y,f(z,v,u)). [para(7401(a,1),7689(a,1,3,3)),rewrite(6(4),29(5))]. given #375 (A,wt=38): 145 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(18(a,2),26(a,2,3,3))]. given #376 (T,wt=24): 7879 f(x,f(y,z,u),f(v,x,z)) = f(v,x,f(y,z,f(x,z,u))). [para(74(a,2),815(a,1)),flip(a)]. given #377 (T,wt=24): 8193 f(x,f(y,z,f(x,u,y)),f(x,u,v)) = f(x,u,f(x,y,v)). [para(798(a,1),7901(a,1,2)),rewrite(5(1,R),6(1),5(2),6(2),57(3),6(1),20(3),5(3,R),6(3),5(5),6(5)),flip(a)]. given #378 (T,wt=24): 8248 f(x,f(y,z,u),f(y,u,f(y,z,x))) = f(y,z,f(y,u,x)). [para(7901(a,1),70(a,2,3)),rewrite(5(1,R),6(1),5(2,R),6(2),5(3),6(3),802(4),6(2),57(3),6(1),20(3),5(3,R),6(3),5(4),6(4),5(6,R),6(6)),flip(a)]. given #379 (T,wt=18): 24883 f(x,y,f(z,y,f(u,z,x))) = f(z,x,y). [para(3866(a,1),8248(a,1,3)),rewrite(5(2),6(2),5(3),5(3),15(4),5(3,R),6(3),5(4,R),6(4)),flip(a)]. given #380 (A,wt=31): 146 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(26(a,1),24(a,1,3)),rewrite(5(2,R),6(2),5(8,R),6(8))]. given #381 (T,wt=18): 24936 f(x,y,f(z,y,f(u,x,z))) = f(x,z,y). [para(12149(a,1),8248(a,1,3)),rewrite(5(2),5(2),5(3),5(3),15(4),5(3,R),6(3),5(4,R),6(4)),flip(a)]. given #382 (T,wt=22): 24888 f(x,y,f(z,y,f(z,u,f(z,v,x)))) = f(z,x,y). [para(1015(a,1),8248(a,1,3)),rewrite(5(3),6(3),5(4),5(4),15(5),5(4,R),6(4),5(5,R),6(5)),flip(a)]. given #383 (T,wt=22): 24898 f(x,y,f(z,y,f(u,x,f(x,z,v)))) = f(x,z,y). [para(2737(a,1),8248(a,1,3)),rewrite(5(1,R),6(1),5(3),5(3),5(4),6(4),15(5),5(2,R),6(2),5(4,R),6(4),5(5,R),6(5)),flip(a)]. given #384 (T,wt=22): 24900 f(x,y,f(z,y,f(u,z,f(z,x,v)))) = f(z,x,y). [para(3889(a,1),8248(a,1,3)),rewrite(5(3),6(3),5(4),5(4),15(5),5(4,R),6(4),5(5,R),6(5)),flip(a)]. given #385 (A,wt=31): 148 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(26(a,2),24(a,1,3)),rewrite(5(1,R),6(1),5(8,R),6(8))]. given #386 (T,wt=22): 24901 f(x,y,f(z,y,f(u,z,f(z,v,x)))) = f(z,x,y). [para(3892(a,1),8248(a,1,3)),rewrite(5(3),6(3),5(4),5(4),15(5),5(4,R),6(4),5(5,R),6(5)),flip(a)]. given #387 (T,wt=22): 24942 f(x,y,f(z,y,f(x,u,f(x,v,z)))) = f(x,z,y). [para(13342(a,1),8248(a,1,3)),rewrite(5(3),5(3),5(4),5(4),15(5),5(4,R),6(4),5(5,R),6(5)),flip(a)]. given #388 (T,wt=22): 24958 f(x,y,f(z,y,f(u,x,f(x,v,z)))) = f(x,z,y). [para(17932(a,1),8248(a,1,3)),rewrite(5(3),5(3),5(4),5(4),15(5),5(4,R),6(4),5(5,R),6(5)),flip(a)]. given #389 (T,wt=22): 25096 f(x,y,f(z,x,f(z,u,f(z,v,y)))) = f(z,x,y). [para(5(a,1),24888(a,1)),rewrite(5(4),6(4),6(5))]. given #390 (A,wt=31): 149 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(26(a,1),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. given #391 (T,wt=24): 8373 f(x,y,f(x,f(z,u,v),f(z,y,u))) = f(x,y,f(z,u,v)). [back_rewrite(1102),rewrite(8148(4))]. given #392 (T,wt=24): 8454 f(x,f(y,z,u),f(z,x,v)) = f(x,v,f(y,z,f(z,u,x))). [para(75(a,1),5(a,2)),rewrite(5(2),5(3),5(4),5(4))]. given #393 (T,wt=24): 8455 f(x,f(y,z,u),f(v,z,x)) = f(v,x,f(y,z,f(z,x,u))). [para(75(a,2),5(a,2)),rewrite(5(1,R),6(1),6(3),5(5),5(5)),flip(a)]. given #394 (T,wt=24): 8553 f(x,f(y,z,u),f(z,x,v)) = f(x,v,f(y,z,f(z,x,u))). [para(75(a,2),896(a,2)),rewrite(5(1,R),6(1),5(4,R),6(4),896(7),5(5)),flip(a)]. given #395 (A,wt=31): 151 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(26(a,2),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. given #396 (T,wt=24): 9018 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,x,f(z,v,u))). [para(76(a,2),1009(a,2)),rewrite(6(6),2114(10)),flip(a)]. given #397 (T,wt=24): 9647 f(x,f(y,x,z),f(x,u,v)) = f(y,x,f(x,u,f(x,z,v))). [para(87(a,2),17(a,1)),flip(a)]. given #398 (T,wt=24): 9696 f(x,y,f(x,f(y,z,u),f(v,x,z))) = f(v,x,f(x,y,z)). [para(785(a,1),87(a,1,3)),flip(a)]. given #399 (T,wt=24): 9721 f(x,y,f(x,f(z,y,u),f(v,x,z))) = f(v,x,f(x,z,y)). [para(800(a,1),87(a,1,3)),flip(a)]. given #400 (A,wt=31): 152 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(25(a,2),26(a,2,3,3))]. given #401 (T,wt=24): 9899 f(x,y,f(z,u,f(y,z,v))) = f(x,y,f(z,v,f(y,z,u))). [para(847(a,1),78(a,1,3,3)),rewrite(5(1),5(1),5(2,R),6(2),20(2),5(4),102(7))]. given #402 (T,wt=24): 10057 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,z,y))). [para(5(a,1),91(a,1)),rewrite(5(3),5(3),6(4))]. given #403 (T,wt=24): 10164 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(x,u,f(z,x,y))). [para(91(a,1),1986(a,2)),rewrite(6(7),5(8,R),6(8),5(9,R),6(9),394(10),6(9),4645(10),5(4,R),6(4))]. given #404 (T,wt=24): 10182 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(x,y,f(z,x,u))). [para(91(a,1),3477(a,2)),rewrite(5(5,R),6(5),57(7),5827(8),5(4,R),6(4))]. given #405 (A,wt=35): 156 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(21(a,1),26(a,1,3,3)),rewrite(6(1),6(5)),flip(a)]. given #406 (T,wt=24): 10853 f(x,y,f(z,u,f(u,x,v))) = f(x,y,f(u,x,f(z,u,v))). [para(5(a,1),105(a,1)),rewrite(5(1,R),6(1),5(3),5(3),5(5,R),6(5))]. given #407 (T,wt=24): 10898 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(v,z,f(x,z,u))). [para(847(a,2),105(a,2,3)),flip(a)]. given #408 (T,wt=22): 25544 f(x,y,f(z,x,f(y,u,f(z,v,y)))) = f(z,x,y). [para(10898(a,2),74(a,2,3)),rewrite(1530(4)),flip(a)]. given #409 (T,wt=24): 12560 f(x,f(y,z,u),f(v,x,f(y,z,x))) = f(v,x,f(y,z,x)). [para(896(a,1),133(a,1,2)),rewrite(5(4,R),6(4),884(6),5(5,R),6(5)),flip(a)]. given #410 (A,wt=31): 157 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(21(a,1),26(a,2,3,3)),rewrite(6(1),118(4),6(5))]. given #411 (T,wt=24): 12562 f(x,f(y,z,u),f(v,x,f(y,x,z))) = f(v,x,f(y,x,z)). [para(899(a,1),133(a,1,2)),rewrite(5(4,R),6(4),884(6),5(5,R),6(5)),flip(a)]. given #412 (T,wt=24): 12563 f(x,f(y,z,x),f(u,x,f(y,z,v))) = f(u,x,f(y,z,x)). [para(1006(a,1),133(a,1,2)),rewrite(5(4,R),6(4),791(6),5(5,R),6(5)),flip(a)]. given #413 (T,wt=24): 12564 f(x,f(y,x,z),f(u,x,f(y,z,v))) = f(u,x,f(y,x,z)). [para(1075(a,1),133(a,1,2)),rewrite(5(4,R),6(4),791(6),5(5,R),6(5)),flip(a)]. given #414 (T,wt=24): 12709 f(x,f(y,z,x),f(x,u,f(y,z,v))) = f(x,u,f(y,z,x)). [para(896(a,1),169(a,1,3,3)),rewrite(896(6)),flip(a)]. given #415 (A,wt=35): 158 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(26(a,2),29(a,1,3,3))]. given #416 (T,wt=24): 12714 f(x,f(y,z,u),f(x,v,f(y,z,x))) = f(x,v,f(y,z,x)). [para(1006(a,1),169(a,1,3,3)),rewrite(15(6)),flip(a)]. given #417 (T,wt=24): 12779 f(x,f(y,z,u),f(x,v,f(z,u,x))) = f(x,v,f(z,u,x)). [para(7099(a,1),169(a,1,3,3)),rewrite(15(6)),flip(a)]. given #418 (T,wt=24): 12782 f(x,f(y,z,u),f(x,v,f(y,u,x))) = f(x,v,f(y,u,x)). [para(7420(a,1),169(a,1,3,3)),rewrite(15(6)),flip(a)]. given #419 (T,wt=24): 13587 f(x,f(y,z,u),f(z,u,f(y,z,x))) = f(z,x,f(y,z,u)). [para(170(a,1),5(a,2)),rewrite(5(2),5(2),5(4),5(6,R),6(6))]. given #420 (A,wt=35): 160 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(29(a,1),26(a,1,3,3)),flip(a)]. given #421 (T,wt=24): 13623 f(f(x,y,z),f(x,y,u),f(v,z,f(x,y,z))) = f(x,y,z). [para(1006(a,1),170(a,1,2)),rewrite(12957(7),1006(9),15(8))]. given #422 (T,wt=24): 13624 f(f(x,y,z),f(x,z,u),f(v,y,f(x,y,z))) = f(x,y,z). [para(1075(a,1),170(a,1,2)),rewrite(12957(7),1075(9),15(8))]. given #423 (T,wt=24): 14140 f(x,y,f(z,u,f(y,v,z))) = f(x,y,f(v,z,f(y,z,u))). [para(602(a,1),216(a,1,3)),rewrite(5(1,R),6(1),5(4),6(5),5(6,R),6(6),12957(6)),flip(a)]. given #424 (T,wt=22): 25701 f(x,y,f(x,z,f(y,u,f(z,v,y)))) = f(x,z,y). [para(14140(a,2),30(a,2,3)),rewrite(1810(4)),flip(a)]. given #425 (A,wt=31): 161 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(29(a,1),26(a,2,3,3)),rewrite(102(4))]. given #426 (T,wt=24): 14302 f(x,y,f(x,f(y,z,u),f(z,u,v))) = f(x,y,f(z,u,v)). [back_rewrite(1537),rewrite(5(1),14275(4))]. given #427 (T,wt=21): 25751 f(x,y,f(z,f(x,z,u),f(y,v,z))) = f(x,y,z). [para(1530(a,1),14302(a,1,3)),rewrite(6(2),1005(3),5(4,R),6597(5)),flip(a)]. given #428 (T,wt=24): 14640 f(x,f(y,z,u),f(v,y,x)) = f(v,x,f(y,z,f(y,u,x))). [para(320(a,2),5(a,2)),rewrite(6(3),5(5)),flip(a)]. given #429 (T,wt=24): 15181 f(x,f(y,z,u),f(y,v,x)) = f(v,x,f(y,z,f(y,u,x))). [para(321(a,1),5(a,2)),rewrite(5(2,R),6(2),5(3),6(4))]. given #430 (A,wt=31): 162 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(26(a,1),122(a,1,3,3)),rewrite(5(4,R),6(4),103(5),5(8,R),6(8))]. given #431 (T,wt=24): 15182 f(x,f(y,x,z),f(z,u,v)) = f(y,x,f(z,u,f(x,z,v))). [para(321(a,1),6(a,1)),rewrite(5(1,R),6(1),6(4)),flip(a)]. given #432 (T,wt=24): 15421 f(f(x,y,z),f(x,y,f(x,u,z)),f(y,z,v)) = f(x,y,z). [para(15371(a,1),896(a,1,3)),rewrite(5(5),15371(8))]. given #433 (T,wt=24): 15422 f(f(x,y,z),f(y,z,u),f(x,y,f(x,v,z))) = f(x,y,z). [para(15371(a,1),1006(a,1,2)),rewrite(5(5,R),15371(8))]. given #434 (T,wt=24): 15462 f(x,f(x,y,z),f(u,v,w)) = f(x,y,f(x,z,f(u,v,w))). [para(15244(a,1),70(a,2,3)),rewrite(5(4),5(4),15461(6),5(6,R)),flip(a)]. given #435 (A,wt=31): 164 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(122(a,1),26(a,1,3,3)),rewrite(5(2,R),6(2),5(6,R),6(6),160(9))]. given #436 (T,wt=24): 15489 f(x,f(y,z,u),f(x,v,w)) = f(x,v,f(x,w,f(y,z,u))). [para(15244(a,1),130(a,2,3)),rewrite(6(4),15461(6)),flip(a)]. given #437 (T,wt=24): 15491 f(x,f(y,x,z),f(u,v,w)) = f(y,x,f(x,z,f(u,v,w))). [para(15244(a,1),220(a,1)),rewrite(6(2),6(6),5(10),6(10),15466(10),19(8)),flip(a)]. given #438 (T,wt=24): 15773 f(x,f(y,z,u),f(x,y,v)) = f(x,v,f(y,z,f(x,y,u))). [back_rewrite(15610),rewrite(15751(7))]. given #439 (T,wt=21): 27138 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(15773(a,2),13048(a,1))]. given #440 (A,wt=38): 165 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(26(a,1),26(a,1,3,3))]. given #441 (T,wt=24): 15812 f(x,f(y,z,f(u,x,y)),f(u,x,v)) = f(x,y,f(u,x,v)). [para(800(a,1),15370(a,1,3,3)),rewrite(5(2),5(2),5(4,R),5(6))]. given #442 (T,wt=24): 15831 f(x,f(y,z,f(u,x,y)),f(u,v,x)) = f(x,y,f(u,v,x)). [para(3978(a,1),15370(a,1,3,3)),rewrite(5(2),5(2),5(4,R),5(6))]. given #443 (T,wt=24): 15847 f(x,f(y,z,f(y,u,x)),f(y,u,f(u,x,v))) = f(y,u,x). [para(1810(a,1),15370(a,1,3,3)),rewrite(5(1,R),6(1),6(3),5(5,R),5(6,R),6(6),6(8),800(8))]. given #444 (T,wt=22): 27495 f(x,y,f(z,u,f(x,z,f(v,z,y)))) = f(x,z,y). [para(7125(a,1),15847(a,1,3)),rewrite(5(3),5(4),15801(4),5(3,R),5(4),6(5),15462(5),26267(5),5(3,R),6(3),5(6),5(7),15801(7))]. given #445 (A,wt=38): 166 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(26(a,2),26(a,1,3,3))]. given #446 (T,wt=24): 15864 f(x,f(y,z,f(u,y,x)),f(u,y,f(u,x,v))) = f(u,y,x). [para(4980(a,1),15370(a,1,3,3)),rewrite(5(5,R),6(8),802(8))]. given #447 (T,wt=24): 15867 f(x,f(y,z,f(u,y,x)),f(u,v,f(u,y,x))) = f(u,y,x). [para(5002(a,1),15370(a,1,3,3)),rewrite(5(1),5(3),5(5,R),5(6),6(8),1545(8))]. given #448 (T,wt=24): 15885 f(x,f(y,z,f(y,u,x)),f(y,u,f(u,v,x))) = f(y,u,x). [para(8843(a,1),15370(a,1,3,3)),rewrite(5(5,R),6(8),3978(8))]. given #449 (T,wt=24): 15888 f(x,f(y,z,f(u,y,x)),f(u,y,f(u,v,x))) = f(u,y,x). [para(9180(a,1),15370(a,1,3,3)),rewrite(5(5,R),6(8),15371(8))]. given #450 (A,wt=38): 167 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(26(a,1),26(a,2,3,3))]. given #451 (T,wt=21): 27685 f(x,y,f(z,f(x,u,z),f(z,y,v))) = f(x,z,y). [para(1103(a,1),15888(a,1,2,3)),rewrite(5(1),5(3),5(4),5(5,R),15(5),5(5),5(7),5(9,R),24936(11),5(5),26972(5),5(3,R),6(3),4979(4),5(3),5(4),25932(6),6(3),5(4,R)),flip(a)]. given #452 (T,wt=21): 27700 f(x,y,f(z,f(x,u,z),f(y,z,v))) = f(x,y,z). [para(5(a,2),27685(a,1,3)),rewrite(5(2,R),6(2),5(3),6(5))]. given #453 (T,wt=22): 27714 f(x,y,f(y,z,f(z,u,f(x,v,z)))) = f(x,y,z). [para(27685(a,1),1744(a,2,3)),rewrite(5(2,R),6(2),5(3,R),6(3),19825(6),5(2),5(2),5(5,R),6(5),6(6),15852(7))]. given #454 (T,wt=24): 15899 f(x,f(y,z,f(u,x,y)),f(v,u,x)) = f(x,y,f(v,u,x)). [para(12149(a,1),15370(a,1,3,3)),rewrite(5(2),5(2),5(4,R),5(6))]. given #455 (A,wt=38): 168 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(26(a,2),26(a,2,3,3))]. given #456 (T,wt=24): 15984 f(x,f(y,z,u),f(x,y,f(v,x,z))) = f(v,x,f(x,y,z)). [para(15801(a,1),41(a,1,3)),rewrite(5(3),5(3)),flip(a)]. given #457 (T,wt=24): 15990 f(x,f(y,z,u),f(x,y,f(z,u,v))) = f(x,y,f(z,u,v)). [para(15801(a,1),896(a,1,2)),rewrite(5(2),5(2),5(3),5(5),5(5),5(6))]. given #458 (T,wt=24): 15993 f(x,f(y,z,u),f(x,y,f(v,z,u))) = f(x,y,f(v,z,u)). [para(15801(a,1),1006(a,1,3)),rewrite(5(2),6(4),5(6))]. given #459 (T,wt=24): 15998 f(x,y,f(x,f(z,u,y),f(v,z,u))) = f(x,y,f(v,z,u)). [para(15801(a,1),794(a,1,3,3)),rewrite(5(2),5(2),5(3,R),6(3),5(4,R),15462(4),5(6))]. given #460 (A,wt=34): 173 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(8(a,1),28(a,1,3,3))]. given #461 (T,wt=24): 16051 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(y,z,f(x,z,u))). [para(75(a,1),15801(a,2)),rewrite(6(2),6(5),15801(7))]. given #462 (T,wt=24): 16052 f(x,f(y,z,f(u,x,z)),f(v,u,x)) = f(x,z,f(v,u,x)). [para(15801(a,1),9180(a,1,3,3)),rewrite(5(2),5(2),5(4,R),5(6))]. given #463 (T,wt=24): 16053 f(x,f(y,z,u),f(x,z,f(v,x,y))) = f(v,x,f(x,y,z)). [para(15801(a,1),87(a,1,3)),rewrite(5(3),5(3)),flip(a)]. given #464 (T,wt=24): 16076 f(x,f(y,z,u),f(v,x,f(x,y,z))) = f(v,x,f(x,y,z)). [para(15801(a,1),133(a,1,2)),rewrite(5(2),5(2),5(4,R),6(4),884(6),5(3),5(3),5(5,R),6(5)),flip(a)]. given #465 (A,wt=34): 177 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(16(a,2),28(a,1,2)),rewrite(5(1,R),6(1),5(5,R),6(5),5(8,R),6(8))]. given #466 (T,wt=24): 16112 f(x,f(y,z,u),f(x,y,f(z,v,u))) = f(x,y,f(z,v,u)). [para(15824(a,1),1006(a,1,3)),rewrite(5(2),6(4),5(6))]. given #467 (T,wt=24): 16113 f(x,f(y,z,u),f(x,z,f(y,u,v))) = f(x,z,f(y,u,v)). [para(1075(a,1),15824(a,1,2))]. given #468 (T,wt=24): 16115 f(x,y,f(x,f(z,u,y),f(z,v,u))) = f(x,y,f(z,v,u)). [para(15824(a,1),794(a,1,3,3)),rewrite(5(2),5(2),5(3,R),6(3),5(4,R),15462(4),5(6))]. given #469 (T,wt=24): 16169 f(x,f(y,z,f(u,x,z)),f(u,v,x)) = f(x,z,f(u,v,x)). [para(15824(a,1),9180(a,1,3,3)),rewrite(5(2),5(2),5(4,R),5(6))]. given #470 (A,wt=34): 180 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(17(a,1),28(a,1,3,3))]. given #471 (T,wt=24): 16208 f(x,y,f(x,f(z,u,y),f(z,u,v))) = f(x,y,f(z,u,v)). [para(15852(a,1),794(a,1,3,3)),rewrite(5(2),5(2),5(3,R),6(3),5(4,R),15462(4),5(6))]. given #472 (T,wt=22): 28413 f(x,y,f(z,u,f(x,z,f(y,v,z)))) = f(x,y,z). [para(1530(a,1),16208(a,1,3)),rewrite(5(1),6(2),1005(3),5(2),5(4,R),6597(5),26526(5)),flip(a)]. given #473 (T,wt=24): 16222 f(x,f(y,z,f(u,x,z)),f(u,x,v)) = f(x,z,f(u,x,v)). [para(15852(a,1),9180(a,1,3,3)),rewrite(5(2),5(2),5(4,R),5(6))]. given #474 (T,wt=24): 16533 f(x,f(y,z,u),f(u,x,v)) = f(x,v,f(y,u,f(z,u,x))). [para(323(a,1),5(a,2)),rewrite(5(2,R),6(2),5(3),5(4),5(4))]. given #475 (A,wt=38): 182 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(28(a,1),18(a,1,3,3)),flip(a)]. given #476 (T,wt=24): 16534 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(z,u,f(x,y,z))). [para(5(a,2),323(a,1,2)),rewrite(5(5,R),6(5))]. given #477 (T,wt=21): 28529 f(x,f(y,z,f(u,z,v)),f(x,z,v)) = f(x,z,v). [para(16534(a,2),2726(a,1,2)),rewrite(15(2),6(2),5(3),5(5))]. given #478 (T,wt=24): 16539 f(x,f(y,z,u),f(x,v,u)) = f(x,v,f(y,u,f(x,z,u))). [para(323(a,2),20(a,1,3)),rewrite(6(2),22(4))]. given #479 (T,wt=24): 16560 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,u,v))). [para(21(a,1),323(a,1,2)),rewrite(6(5),19(6),15462(9),15462(8),12628(7),15751(8))]. given #480 (A,wt=44): 184 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(18(a,1),28(a,1,3,3))]. given #481 (T,wt=24): 16693 f(x,f(y,z,u),f(x,z,f(y,v,u))) = f(x,z,f(y,v,u)). [para(323(a,2),2858(a,1,2)),rewrite(6(2),15824(3),5(3),5(6))]. given #482 (T,wt=21): 28823 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(2726(a,1),16693(a,1,3)),rewrite(5(2,R),6(2),5(3),5(4),6(5),15462(5),2735(4),20(2),5(3,R),6(3),5(4)),flip(a)]. given #483 (T,wt=24): 16780 f(x,y,f(z,u,f(y,v,u))) = f(y,u,f(x,y,f(z,v,u))). [para(323(a,2),74(a,1,3)),rewrite(15(2),6(2),19(5))]. given #484 (T,wt=24): 16803 f(x,y,f(x,f(y,z,u),f(x,v,u))) = f(x,v,f(x,y,u)). [para(323(a,2),76(a,2,3)),rewrite(5(2,R),6(2),16077(3),6(4),5(6,R),6(6)),flip(a)]. given #485 (A,wt=44): 186 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(18(a,2),28(a,1,3,3))]. given #486 (T,wt=24): 16974 f(x,y,f(z,x,f(u,x,v))) = f(x,y,f(x,v,f(z,u,x))). [para(16618(a,1),133(a,2,3)),rewrite(6(2),6(5),13734(6),13793(7),5(4),5(4)),flip(a)]. given #487 (T,wt=24): 17196 f(x,y,f(y,f(x,z,u),f(y,z,v))) = f(y,v,f(x,y,z)). [para(899(a,1),500(a,2,3)),rewrite(6(2))]. given #488 (T,wt=24): 17333 f(x,y,f(y,f(x,z,u),f(y,u,v))) = f(y,v,f(x,y,u)). [para(15276(a,1),500(a,2,3)),rewrite(5(1,R),6(1),6(2))]. given #489 (T,wt=21): 29131 f(x,f(y,z,f(u,v,y)),f(u,x,y)) = f(u,x,y). [para(785(a,1),17333(a,1,3)),rewrite(6(2),6632(3),5(3),5(3)),flip(a)]. given #490 (A,wt=34): 188 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(24(a,1),28(a,1,2)),rewrite(5(1,R),6(1),5(5,R),6(5),5(8,R),6(8))]. given #491 (T,wt=22): 29140 f(x,y,f(z,u,f(y,z,f(x,v,z)))) = f(x,y,z). [para(1530(a,1),17333(a,1,3)),rewrite(6(2),6632(3),5(4,R),6(6),26526(6),25880(6),102(6)),flip(a)]. given #492 (T,wt=22): 29179 f(x,y,f(z,y,f(u,z,f(x,z,v)))) = f(x,z,y). [para(30(a,1),188(a,1,3,3)),rewrite(802(7),6(5),15462(5),4981(4),20(2)),flip(a)]. given #493 (T,wt=24): 17683 f(x,y,f(x,z,f(u,x,v))) = f(x,v,f(x,y,f(u,x,z))). [para(508(a,1),793(a,2)),rewrite(6(5),15462(6),15462(5),17106(7)),flip(a)]. given #494 (T,wt=24): 18188 f(x,y,f(x,z,f(u,x,v))) = f(x,v,f(x,z,f(u,x,y))). [para(524(a,1),793(a,2)),rewrite(6(5),15462(6),15462(5),17106(7))]. given #495 (A,wt=44): 201 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(26(a,1),28(a,1,3,3))]. given #496 (T,wt=24): 18283 f(x,y,f(z,u,f(z,v,y))) = f(x,y,f(z,v,f(z,y,u))). [para(577(a,1),5(a,2)),rewrite(6(3),6(4),5(6,R),6(6)),flip(a)]. given #497 (T,wt=24): 18284 f(x,y,f(z,u,f(z,v,x))) = f(x,y,f(z,v,f(z,x,u))). [para(5(a,1),577(a,1)),rewrite(5(3),5(3),6(4)),flip(a)]. given #498 (T,wt=24): 18371 f(x,y,f(z,u,f(z,v,y))) = f(z,y,f(x,y,f(z,v,u))). [para(577(a,1),1986(a,2)),rewrite(6(7),5(8,R),6(8),5(9,R),6(9),5113(10),6(4),5(6,R),6(6)),flip(a)]. given #499 (T,wt=24): 18471 f(x,y,f(z,u,f(y,v,z))) = f(y,z,f(x,y,f(v,z,u))). [para(577(a,1),220(a,1,3)),rewrite(5(1),6(1),6597(3),5(4,R),6(4),20(5),5(6,R),6(6))]. given #500 (A,wt=44): 203 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(26(a,2),28(a,1,3,3))]. given #501 (T,wt=24): 18571 f(x,y,f(y,f(x,z,u),f(y,v,u))) = f(y,v,f(x,y,u)). [para(18416(a,1),24(a,2,3)),rewrite(5(4,R),6(4),8488(4),6(2),5(6,R),6(6))]. given #502 (T,wt=24): 18591 f(x,f(y,z,f(x,u,y)),f(z,v,f(x,y,z))) = f(x,y,z). [para(18416(a,1),884(a,1,3,3)),rewrite(5(2,R),6(2),6597(3),6(3),5(7,R),6(7),6597(8),18567(8))]. given #503 (T,wt=24): 18761 f(x,f(y,z,u),f(x,y,v)) = f(x,v,f(y,u,f(x,y,z))). [para(676(a,1),38(a,2)),rewrite(6(2))]. given #504 (T,wt=24): 18928 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(v,u,f(x,z,u))). [para(1675(a,1),799(a,2,3)),rewrite(6(3),6(4),18882(6),18902(6))]. given #505 (A,wt=31): 222 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(30(a,1),8(a,2,3))]. given #506 (T,wt=24): 19077 f(x,f(y,z,u),f(z,x,f(y,x,v))) = f(x,v,f(y,z,x)). [para(799(a,1),133(a,2)),rewrite(5(2),5(3,R),6(3),5(5),5(7,R),6(7),7475(8),5(5),5(5))]. given #507 (T,wt=24): 19100 f(x,f(y,z,f(y,x,u)),f(x,u,v)) = f(y,x,f(x,u,v)). [para(799(a,1),220(a,2,3)),rewrite(5(1,R),6(1),5(2,R),6(2),6(3),5(4,R),1005(6),5(3,R),6(3),6(4),5(6,R)),flip(a)]. given #508 (T,wt=24): 19221 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,u,w))). [para(79(a,1),18961(a,1,2)),rewrite(5(5,R),14730(5),1005(5),20(3),16565(6)),flip(a)]. given #509 (T,wt=24): 19342 f(x,f(y,x,f(y,z,u)),f(z,u,v)) = f(y,x,f(z,u,v)). [para(831(a,1),74(a,2,3)),rewrite(5(4,R),1498(5),19(4),5(6,R)),flip(a)]. given #510 (A,wt=31): 223 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(8(a,1),30(a,1,3,3))]. given #511 (T,wt=21): 29700 f(x,f(y,z,x),f(y,u,f(y,v,z))) = f(y,z,x). [para(16360(a,1),19342(a,2)),rewrite(5(5,R),15(5),5(5),4(5),6(3),5(4,R),6(5))]. given #512 (T,wt=21): 29783 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(18961(a,1),29700(a,1,2)),rewrite(5(3),5(3),4(7),5(2),5(2)),flip(a)]. given #513 (T,wt=24): 19365 f(x,f(y,z,u),f(v,x,f(v,y,z))) = f(v,x,f(y,z,u)). [para(831(a,1),220(a,2,3)),rewrite(1515(5),19(4)),flip(a)]. given #514 (T,wt=23): 29827 f(x,f(y,z,u),f(z,u,v)) = f(v,f(y,z,u),f(z,u,x)). [para(15801(a,1),19365(a,1,3)),rewrite(5(3),5(3),29693(4))]. given #515 (A,wt=31): 224 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(8(a,1),30(a,2,3,3))]. given #516 (T,wt=21): 29888 f(x,y,f(z,y,f(u,x,y))) = f(z,y,f(u,x,y)). [para(29827(a,1),16(a,1)),rewrite(15(2),6(2),5(4)),flip(a)]. given #517 (T,wt=18): 30382 f(x,y,f(z,x,f(u,z,y))) = f(z,x,y). [para(9018(a,1),29888(a,2)),rewrite(5(4,R),6(4),29680(5),6(3),20(3),1855(4),15(3),5(3),25837(5),6(3),20(4)),flip(a)]. given #518 (T,wt=21): 30258 f(x,y,f(z,f(y,u,z),f(x,z,v))) = f(x,y,z). [para(29827(a,1),27495(a,1,3)),rewrite(5(1),5(2),5(2),15(3),5(3),6(5))]. given #519 (T,wt=23): 29828 f(x,f(y,z,u),f(y,u,v)) = f(v,f(y,z,u),f(y,u,x)). [para(15824(a,1),19365(a,1,3)),rewrite(5(3),5(3),29695(4))]. given #520 (A,wt=31): 227 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(16(a,2),30(a,1,3,3))]. given #521 (T,wt=21): 30545 f(x,f(y,z,f(u,z,v)),f(u,z,x)) = f(u,z,x). [para(29828(a,1),6828(a,1)),rewrite(6(3),25932(4),15(5),5(5),6(5),13734(5),19(6))]. given #522 (T,wt=23): 29829 f(x,f(y,z,u),f(y,z,v)) = f(v,f(y,z,u),f(y,z,x)). [para(15852(a,1),19365(a,1,3)),rewrite(5(3),5(3),29696(4))]. Low Water (keep, True_semantics): wt=37 given #523 (T,wt=23): 29872 f(x,f(y,z,u),f(v,z,u)) = f(v,f(y,z,u),f(z,u,x)). [para(29827(a,1),5(a,1)),rewrite(5(4),5(6,R)),flip(a)]. given #524 (T,wt=23): 29873 f(x,f(y,z,u),f(v,y,u)) = f(v,f(y,z,u),f(y,u,x)). [para(5(a,1),29827(a,1,2)),rewrite(5(2,R),6(2),5(4),5(5),6(5)),flip(a)]. given #525 (A,wt=31): 228 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(16(a,2),30(a,2,3,3))]. given #526 (T,wt=23): 29874 f(x,f(y,z,u),f(v,y,z)) = f(v,f(y,z,u),f(y,z,x)). [para(5(a,2),29827(a,1,2)),rewrite(5(4),5(4),5(5)),flip(a)]. given #527 (T,wt=23): 29875 f(x,f(y,z,u),f(v,z,u)) = f(y,f(v,z,u),f(z,u,x)). [para(29827(a,1),6(a,1)),rewrite(5(4)),flip(a)]. given #528 (T,wt=23): 29876 f(x,f(y,z,u),f(v,y,z)) = f(v,f(y,z,x),f(y,z,u)). [para(29827(a,1),6(a,2)),rewrite(5(2),5(2),5(4),5(4),5(5)),flip(a)]. given #529 (T,wt=23): 29885 f(x,f(y,z,u),f(y,v,z)) = f(u,f(y,v,z),f(y,z,x)). [para(19(a,1),29827(a,2,3)),rewrite(5(2),5(2),29695(4),5(4),5(4)),flip(a)]. Low Water (displace, True_semantics): id=19160, wt=44 Low Water (displace, True_semantics): id=19932, wt=43 Low Water (displace, True_semantics): id=20971, wt=42 given #530 (A,wt=31): 229 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(30(a,2),17(a,1,3)),rewrite(57(8))]. given #531 (T,wt=23): 29886 f(x,f(y,z,u),f(y,z,v)) = f(v,f(y,z,x),f(y,z,u)). [para(20(a,1),29827(a,2,3)),rewrite(5(2),5(2),29696(4),5(4),5(4))]. given #532 (T,wt=23): 29931 f(x,f(y,z,u),f(v,y,z)) = f(u,f(v,y,z),f(y,z,x)). [para(205(a,1),29827(a,2,3)),rewrite(5(2),5(2),29693(4),5(4),5(4)),flip(a)]. given #533 (T,wt=23): 30000 f(x,f(y,z,u),f(v,z,u)) = f(v,f(z,u,x),f(y,z,u)). [para(29827(a,1),1005(a,2)),rewrite(5(5,R),12149(7),5(5)),flip(a)]. given #534 (T,wt=22): 32365 f(x,y,f(z,y,f(z,u,f(x,v,z)))) = f(x,z,y). [para(30000(a,1),7434(a,1,3)),rewrite(15(3),5(3),5(3),31854(5),15462(3))]. given #535 (A,wt=31): 230 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(17(a,1),30(a,2,3,3))]. given #536 (T,wt=23): 30106 f(f(x,y,z),f(y,z,u),f(x,z,u)) = f(x,z,f(y,z,u)). [para(29827(a,1),170(a,1)),rewrite(5(3))]. given #537 (T,wt=23): 30415 f(x,f(y,z,u),f(z,v,u)) = f(y,f(z,v,u),f(z,u,x)). [para(29828(a,1),6(a,1)),rewrite(5(4)),flip(a)]. given #538 (T,wt=23): 30490 f(x,f(y,z,u),f(v,y,u)) = f(v,f(y,u,x),f(y,z,u)). [para(29828(a,1),1005(a,2)),rewrite(5(5,R),12149(7),5(5)),flip(a)]. given #539 (T,wt=23): 30743 f(x,f(y,z,u),f(z,u,v)) = f(y,f(z,u,v),f(z,u,x)). [para(29829(a,1),6(a,1)),rewrite(5(4)),flip(a)]. given #540 (A,wt=38): 231 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(30(a,2),18(a,1,3,3))]. given #541 (T,wt=22): 32583 f(x,y,f(x,z,f(y,u,f(v,z,y)))) = f(x,z,y). [para(30743(a,2),3889(a,1)),rewrite(5(3),5(3),31948(4),5(1),4(4),5(5),5(5),15462(5),22(5),6(6),20(6))]. given #542 (T,wt=23): 30979 f(x,f(y,z,u),f(v,y,z)) = f(u,f(y,z,x),f(v,y,z)). [para(29829(a,1),4720(a,2)),rewrite(5(4),5(4),25958(5),30208(5),5(5))]. given #543 (T,wt=23): 31098 f(x,f(y,z,u),f(v,y,z)) = f(v,f(x,y,z),f(y,z,u)). [para(29872(a,1),6(a,2)),rewrite(5(2),5(2),5(4),5(4),5(5)),flip(a)]. given #544 (T,wt=23): 31101 f(x,f(y,z,u),f(v,y,z)) = f(v,f(y,z,u),f(x,y,z)). [para(29872(a,1),19(a,2)),rewrite(5(2),5(2),19(5),5(4),5(4),5(5))]. given #545 (A,wt=38): 232 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(30(a,1),18(a,2,3,3))]. given #546 (T,wt=23): 31153 f(x,f(y,z,u),f(v,y,u)) = f(v,f(y,z,u),f(x,y,u)). [para(29872(a,1),1074(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),1074(6),5(4,R),6(4),5(5))]. given #547 (T,wt=23): 31172 f(x,f(y,z,u),f(v,z,u)) = f(v,f(y,z,u),f(x,z,u)). [para(29872(a,1),16113(a,2)),rewrite(6(2),1074(6),5(5))]. given #548 (T,wt=23): 31254 f(x,f(y,z,u),f(v,y,z)) = f(v,f(y,x,z),f(y,z,u)). [para(5(a,1),29875(a,1,2)),rewrite(5(2),6(2),5(4),6(4),5(5),6(5)),flip(a)]. given #549 (T,wt=23): 31255 f(x,f(y,z,u),f(z,u,v)) = f(y,f(x,z,u),f(z,u,v)). [para(29875(a,2),6(a,1)),rewrite(5(2),5(2),5(4),5(5),5(5))]. given #550 (A,wt=38): 233 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(18(a,1),30(a,1,3,3))]. given #551 (T,wt=22): 32998 f(x,y,f(z,y,f(z,u,f(v,z,x)))) = f(z,x,y). [back_rewrite(21759),rewrite(32940(5),5(3,R),15462(3))]. given #552 (T,wt=23): 31256 f(x,f(y,z,u),f(z,u,v)) = f(y,f(z,u,x),f(z,u,v)). [para(29875(a,2),6(a,2)),rewrite(5(2),5(2),5(5),5(5)),flip(a)]. given #553 (T,wt=23): 31306 f(x,f(y,z,u),f(y,v,z)) = f(u,f(y,z,x),f(y,v,z)). [para(785(a,1),29875(a,2,3)),rewrite(5(1,R),6(1),5(3),5(3),5(4),5(4),29955(5),5(4),5(4),6(5))]. given #554 (T,wt=23): 31338 f(x,f(y,z,u),f(v,z,u)) = f(y,f(z,u,x),f(v,z,u)). [para(29875(a,2),1005(a,2)),rewrite(5(5,R),12149(7)),flip(a)]. given #555 (A,wt=38): 234 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(18(a,2),30(a,1,3,3))]. given #556 (T,wt=23): 31399 f(x,f(y,z,u),f(v,z,u)) = f(v,f(z,x,u),f(y,z,u)). [para(29875(a,1),1074(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),1074(6),5(5)),flip(a)]. given #557 (T,wt=23): 31433 f(x,f(y,z,u),f(v,z,u)) = f(v,f(x,z,u),f(y,z,u)). [para(29875(a,1),16113(a,2)),rewrite(6(2),1074(6),5(5)),flip(a)]. given #558 (T,wt=23): 31643 f(x,f(y,z,u),f(y,z,v)) = f(u,f(y,z,x),f(y,z,v)). [para(29876(a,2),19365(a,2)),rewrite(5(4),5(4),896(5),29696(4),5(5),5(5))]. given #559 (T,wt=23): 31743 f(x,f(y,z,u),f(z,v,u)) = f(y,f(z,u,x),f(z,v,u)). [para(29885(a,2),1005(a,2)),rewrite(5(5,R),12149(7),5(4)),flip(a)]. given #560 (A,wt=38): 235 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(18(a,1),30(a,2,3,3))]. given #561 (T,wt=23): 32360 f(x,f(y,z,u),f(v,y,u)) = f(v,f(x,y,u),f(y,z,u)). [para(30000(a,1),1074(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),1074(6),5(4),5(5,R),6(5))]. given #562 (T,wt=23): 32407 f(f(x,y,z),f(x,z,u),f(y,z,u)) = f(x,z,f(y,z,u)). [para(30106(a,1),6(a,2))]. given #563 (T,wt=23): 32488 f(f(x,y,z),f(u,x,y),f(u,y,z)) = f(u,y,f(x,y,z)). [para(30106(a,1),18567(a,2)),rewrite(5(7,R),24883(9))]. given #564 (T,wt=22): 33385 f(x,y,f(z,u,f(u,y,f(u,x,v)))) = f(u,x,y). [para(1006(a,1),32488(a,1,3)),rewrite(5(5,R),6(5),5(7),25837(7),15(5),13623(5),33100(6)),flip(a)]. given #565 (A,wt=38): 236 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(18(a,2),30(a,2,3,3))]. given #566 (T,wt=22): 33386 f(x,y,f(z,u,f(z,y,f(v,z,x)))) = f(z,x,y). [para(1106(a,1),32488(a,1,2)),rewrite(5(3),6(6),32965(7),5(5),5(5),15462(5),31248(4),6(1),1856(4),802(3),5(5),33001(6),5(4,R),6(4)),flip(a)]. given #567 (T,wt=23): 32528 f(x,f(y,z,u),f(v,y,u)) = f(v,f(y,x,u),f(y,z,u)). [para(30415(a,1),1074(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),1074(6),5(5)),flip(a)]. given #568 (T,wt=23): 32666 f(x,f(y,z,u),f(z,u,v)) = f(y,f(z,x,u),f(z,u,v)). [para(5(a,2),30979(a,1,2)),rewrite(5(2),6(2),5(4),6(4),5(5),6(5)),flip(a)]. given #569 (T,wt=23): 32844 f(x,f(y,z,u),f(y,u,v)) = f(z,f(y,u,v),f(y,u,x)). [para(31254(a,2),5(a,2)),rewrite(5(3),5(5),5(5))]. given #570 (A,wt=31): 237 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(30(a,1),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. given #571 (T,wt=23): 32863 f(x,f(y,z,u),f(v,y,z)) = f(v,f(y,z,u),f(y,x,z)). [para(31254(a,2),1005(a,2)),rewrite(5(5,R),12149(7)),flip(a)]. given #572 (T,wt=23): 32882 f(x,f(y,z,u),f(v,y,z)) = f(u,f(v,y,z),f(y,x,z)). [para(31254(a,2),1182(a,2)),rewrite(5(4),5(4),32171(5),5(2),32529(5)),flip(a)]. given #573 (T,wt=23): 32897 f(x,f(y,z,u),f(y,u,v)) = f(z,f(y,u,x),f(y,u,v)). [para(31254(a,2),19365(a,2)),rewrite(5(4),5(4),12727(5),29695(4),5(5),5(5))]. given #574 (T,wt=23): 33252 f(x,f(y,z,u),f(v,z,u)) = f(y,f(z,x,u),f(v,z,u)). [para(31338(a,1),1074(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),1074(6),5(4)),flip(a)]. given #575 (A,wt=31): 240 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(25(a,2),30(a,2,3,3))]. given #576 (T,wt=23): 33255 f(x,f(y,z,u),f(v,z,u)) = f(y,f(x,z,u),f(v,z,u)). [para(31338(a,1),16113(a,2)),rewrite(6(2),1074(6),5(4))]. given #577 (T,wt=23): 33309 f(x,f(y,z,u),f(z,v,u)) = f(y,f(z,x,u),f(z,v,u)). [para(31743(a,1),1074(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),1074(6),5(4)),flip(a)]. given #578 (T,wt=23): 33328 f(f(x,y,z),f(u,x,y),f(u,x,z)) = f(u,x,f(x,y,z)). [para(32407(a,1),5(a,1)),rewrite(5(1,R),6(1),5(3,R),6(3),6(4)),flip(a)]. given #579 (T,wt=23): 33353 f(f(x,y,z),f(u,x,z),f(u,x,y)) = f(u,x,f(x,y,z)). [para(32488(a,1),6(a,1)),rewrite(5(1,R),6(1),5(3,R),6(3),6(5)),flip(a)]. given #580 (A,wt=35): 245 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(21(a,1),30(a,1,3,3)),rewrite(6(1),6(5)),flip(a)]. given #581 (T,wt=23): 33516 f(x,f(y,z,u),f(z,u,v)) = f(y,f(z,u,v),f(z,x,u)). [para(32666(a,2),1005(a,2)),rewrite(5(5,R),12149(7)),flip(a)]. given #582 (T,wt=23): 33536 f(x,f(y,z,u),f(z,v,u)) = f(v,f(y,z,u),f(z,u,x)). [para(32666(a,2),1182(a,2)),rewrite(5(4),5(4),32171(5),5(2),32529(5))]. given #583 (T,wt=22): 33821 f(x,y,f(y,z,f(u,x,f(x,z,v)))) = f(x,y,z). [para(33536(a,2),3889(a,1)),rewrite(5(3),5(3),32965(4),4(5),5(5),6(5),25331(5),73(5),6(6),205(6))]. given #584 (T,wt=22): 33822 f(x,y,f(z,u,f(v,u,f(x,y,u)))) = f(x,y,u). [para(33536(a,1),4446(a,1,3)),rewrite(5(4),4(4),6(3))]. given #585 (A,wt=35): 248 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(29(a,1),30(a,1,3,3)),flip(a)]. given #586 (T,wt=22): 33862 f(x,y,f(z,u,f(v,z,f(x,y,z)))) = f(x,y,z). [para(5(a,1),33822(a,1,3)),rewrite(5(3),6(3))]. given #587 (T,wt=23): 33612 f(x,f(y,z,u),f(y,v,z)) = f(v,f(y,z,u),f(y,z,x)). [para(32863(a,2),896(a,2)),rewrite(6(3),12727(7),5(5),5(5))]. given #588 (T,wt=23): 33618 f(x,f(y,z,u),f(v,y,u)) = f(z,f(y,u,x),f(v,y,u)). [para(32863(a,2),1671(a,2)),rewrite(32043(5),5(3,R),6(3),32532(5))]. given #589 (T,wt=23): 33626 f(x,f(y,z,u),f(y,v,z)) = f(v,f(y,z,x),f(y,z,u)). [para(32882(a,2),896(a,2)),rewrite(5(2),5(2),6(3),5(4),5(4),12727(7),5(5),5(5))]. given #590 (A,wt=31): 252 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(122(a,1),30(a,2,3,3)),rewrite(5(2,R),6(2),249(5),5(6,R),6(6))]. given #591 (T,wt=23): 33631 f(x,f(y,z,u),f(z,v,u)) = f(y,f(z,v,u),f(z,x,u)). [para(32882(a,2),1074(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),1074(6),5(4),5(5,R),6(5)),flip(a)]. given #592 (T,wt=23): 33632 f(x,f(y,z,u),f(v,y,u)) = f(z,f(v,y,u),f(y,u,x)). [para(32882(a,2),1671(a,2)),rewrite(5(2),5(2),5(3),5(3),32043(5),5(3,R),6(3),32532(5),5(4),5(5),5(5))]. given #593 (T,wt=23): 33802 f(f(x,y,z),f(x,u,y),f(x,u,z)) = f(x,z,f(x,u,y)). [para(33353(a,1),18567(a,2)),rewrite(5(2),5(2),5(3),5(3),5(4),5(4),5(6),5(6),5(7,R),24883(9),5(6,R),6(6))]. given #594 (T,wt=23): 33832 f(x,f(y,z,u),f(v,y,u)) = f(v,f(y,z,u),f(y,x,u)). [para(33536(a,1),1074(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),1074(6),5(4,R),6(4),5(5)),flip(a)]. given #595 (A,wt=38): 253 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(30(a,1),26(a,2,3,3))]. given #596 (T,wt=23): 33892 f(f(x,y,z),f(x,u,z),f(x,u,y)) = f(x,y,f(x,u,z)). [para(33802(a,1),896(a,2)),rewrite(6(2),5(4),6(5),1106(9))]. given #597 (T,wt=24): 19499 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(z,y,f(x,y,v))). [para(839(a,1),5(a,2)),rewrite(6(3),5(4,R),6(4))]. given #598 (T,wt=24): 19770 f(x,y,f(z,u,f(v,u,w))) = f(x,y,f(v,u,f(z,u,w))). [para(72(a,1),971(a,2,3,3)),rewrite(16986(7),6604(6),986(5),6(8),16987(8))]. given #599 (T,wt=24): 19780 f(x,y,f(x,f(z,y,u),f(x,v,u))) = f(x,v,f(x,y,u)). [para(19(a,1),997(a,1,3,3)),rewrite(15(3),15462(7),16538(6),6(4)),flip(a)]. Low Water (displace, True_semantics): id=21790, wt=41 given #600 (A,wt=38): 255 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(26(a,1),30(a,1,3,3))]. given #601 (T,wt=24): 19796 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,v,u))). [para(503(a,1),997(a,2,3,3)),rewrite(5(1,R),6(1),5(3,R),6(3),15462(6),15462(5),12628(4),15751(5),5(4,R),6(4),5(7,R),6(7),16867(9))]. given #602 (T,wt=24): 19828 f(x,y,f(x,f(z,u,y),f(x,v,u))) = f(x,v,f(x,u,y)). [para(75(a,2),997(a,2,3)),rewrite(20(3),15(3),15462(7),50(7)),flip(a)]. given #603 (T,wt=24): 19944 f(x,y,f(x,f(z,u,v),f(z,u,y))) = f(x,y,f(z,u,v)). [para(5(a,1),1066(a,1)),rewrite(5(2),5(2),5(4),5(4))]. given #604 (T,wt=24): 19946 f(x,f(y,z,u),f(x,v,f(v,y,z))) = f(x,v,f(y,z,u)). [para(1066(a,1),8(a,1)),flip(a)]. given #605 (A,wt=38): 257 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(26(a,2),30(a,1,3,3))]. given #606 (T,wt=24): 19947 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))). [para(8(a,1),1066(a,1,3,2)),rewrite(2812(5))]. given #607 (T,wt=24): 19960 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,w,u))). [para(25(a,1),1066(a,1,3,2)),rewrite(2897(5)),flip(a)]. given #608 (T,wt=24): 19967 f(x,f(y,z,u),f(y,v,f(x,z,v))) = f(x,v,f(y,z,u)). [para(1066(a,1),26(a,2)),rewrite(6(2),5(3,R),6(3))]. given #609 (T,wt=24): 20034 f(x,f(y,z,u),f(v,y,f(x,v,z))) = f(x,v,f(y,z,u)). [para(1066(a,1),54(a,2,3)),rewrite(95(5),20(7))]. Low Water (displace, True_semantics): id=22530, wt=40 given #610 (A,wt=38): 258 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(26(a,1),30(a,2,3,3))]. given #611 (T,wt=24): 20060 f(x,f(y,z,u),f(v,z,f(v,x,y))) = f(v,x,f(y,z,u)). [para(1066(a,1),2184(a,2)),rewrite(5(7,R),6(7),15462(9),19704(10),5(6,R),6(6))]. given #612 (T,wt=23): 34330 f(x,f(y,z,u),f(x,v,z)) = f(x,f(v,y,u),f(x,v,z)). [para(20060(a,1),255(a,2,3)),rewrite(5(2),5(2),5(3,R),6(3),22(5),794(5),6(4),15462(4),32545(4),5(1,R),6(1),6(2),5(5),5(5),5(6,R),6(6),27174(7),6(4),6(5))]. Low Water (displace, True_semantics): id=23210, wt=39 Low Water (displace, True_semantics): id=27231, wt=38 given #613 (T,wt=23): 34333 f(x,f(y,z,u),f(x,v,u)) = f(x,f(v,y,z),f(x,v,u)). [para(34330(a,1),5(a,1)),rewrite(6(5),5(6,R)),flip(a)]. given #614 (T,wt=23): 34334 f(x,f(y,z,u),f(x,v,u)) = f(x,f(y,v,z),f(x,v,u)). [para(34330(a,2),5(a,1)),rewrite(6(2),6(4),5(5),5(5),5(6,R)),flip(a)]. given #615 (A,wt=38): 260 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(26(a,2),30(a,2,3,3))]. given #616 (T,wt=23): 34335 f(x,f(y,z,u),f(v,x,u)) = f(x,f(y,v,z),f(v,x,u)). [para(34330(a,1),5(a,2)),rewrite(5(2),5(3),5(4),5(4),5(5)),flip(a)]. given #617 (T,wt=23): 34336 f(x,f(y,z,u),f(v,x,u)) = f(x,f(v,y,z),f(v,x,u)). [para(34330(a,2),5(a,2)),rewrite(5(2,R),6(2),5(3),6(4),5(5,R),6(5)),flip(a)]. given #618 (T,wt=23): 34337 f(x,f(y,z,u),f(x,v,u)) = f(x,f(y,z,v),f(x,v,u)). [para(5(a,1),34330(a,1,2)),rewrite(6(2),5(4),6(4),6(5)),flip(a)]. given #619 (T,wt=23): 34338 f(x,f(y,z,u),f(x,v,y)) = f(x,f(v,z,u),f(x,v,y)). [para(5(a,1),34330(a,1)),rewrite(5(2,R),6(2),5(3,R))]. given #620 (A,wt=38): 267 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(30(a,1),30(a,2,3,3))]. given #621 (T,wt=23): 34434 f(x,f(y,z,u),f(x,v,z)) = f(x,f(y,v,u),f(x,v,z)). [para(785(a,1),34330(a,1,3)),rewrite(5(1,R),6(1),6(3),6(4),6(5),15462(5),28722(5),6(1),5(4,R),6(4),5(5,R),6(5),800(7)),flip(a)]. given #622 (T,wt=23): 34813 f(x,f(y,z,u),f(v,x,u)) = f(x,f(y,z,v),f(v,x,u)). [para(34333(a,1),5(a,2)),rewrite(5(2),5(3),5(4),5(4),5(5)),flip(a)]. given #623 (T,wt=23): 35042 f(x,f(y,z,u),f(v,u,x)) = f(x,f(y,z,v),f(v,u,x)). [para(34335(a,1),5(a,2)),rewrite(5(2),5(3),6(4),5(5)),flip(a)]. given #624 (T,wt=23): 35043 f(x,f(y,z,u),f(v,x,y)) = f(x,f(v,z,u),f(v,x,y)). [para(5(a,1),34335(a,1)),rewrite(5(2),5(3,R),5(4,R),6(4))]. given #625 (A,wt=31): 269 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(16(a,2),32(a,1,3,3)),flip(a)]. given #626 (T,wt=23): 35356 f(x,f(y,z,u),f(v,y,x)) = f(x,f(v,z,u),f(v,y,x)). [para(5(a,1),35042(a,1)),rewrite(5(2),5(3,R),5(4))]. given #627 (T,wt=23): 35405 f(x,f(y,z,u),f(v,u,x)) = f(x,f(v,y,z),f(v,u,x)). [para(35043(a,1),5(a,2)),rewrite(5(2),5(3),5(4),5(4),5(5)),flip(a)]. given #628 (T,wt=24): 20089 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,u,f(x,y,z))). [para(75(a,2),1066(a,1,3)),rewrite(6(3),6(4),29(4),6(2),16207(5),6(5))]. given #629 (T,wt=24): 20096 f(x,f(y,z,u),f(z,v,f(x,y,v))) = f(x,v,f(y,z,u)). [para(1066(a,1),82(a,2)),rewrite(6(2),5(3,R),6(3))]. Low Water (keep, True_semantics): wt=36 given #630 (A,wt=38): 270 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(32(a,2),18(a,1,3,3))]. given #631 (T,wt=24): 20130 f(x,f(y,z,u),f(y,x,f(z,u,v))) = f(y,x,f(z,u,v)). [para(1066(a,1),169(a,1,3)),rewrite(5(3,R),6(3),5(5,R),6(5),15(6),5(5,R),6(5)),flip(a)]. given #632 (T,wt=24): 20490 f(f(x,y,z),f(y,z,f(x,z,u)),f(x,y,v)) = f(x,y,z). [para(5(a,1),1067(a,1,1)),rewrite(5(2,R),6(2),5(4,R),6(4),5(6))]. given #633 (T,wt=24): 20492 f(f(x,y,z),f(x,z,f(x,y,u)),f(y,z,v)) = f(x,y,z). [para(5(a,2),1067(a,1,1)),rewrite(5(3,R),6(3),5(4,R),6(4),5(6),5(6))]. given #634 (T,wt=24): 20493 f(f(x,y,z),f(x,z,f(y,z,u)),f(x,y,v)) = f(x,y,z). [para(6(a,1),1067(a,1,1)),rewrite(5(2,R),6(2),6(6))]. given #635 (A,wt=38): 271 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(32(a,1),18(a,2,3,3))]. given #636 (T,wt=24): 20500 f(f(x,y,z),f(y,z,f(x,y,u)),f(x,z,v)) = f(x,y,z). [para(16(a,2),1067(a,1,2))]. given #637 (T,wt=24): 20770 f(x,f(y,z,u),f(u,x,f(y,z,v))) = f(u,x,f(y,z,v)). [para(1074(a,1),5(a,2)),rewrite(5(3,R),6(3),5(4),5(6,R),6(6))]. given #638 (T,wt=24): 20836 f(x,f(y,z,u),f(y,v,f(z,v,x))) = f(v,x,f(y,z,u)). [para(1074(a,1),1986(a,2)),rewrite(5(3,R),6(3),5(6,R),6(6),5(8,R),6(8),6(9),5(10,R),6(10),16733(12),5(6,R),6(6))]. given #639 (T,wt=24): 21165 f(x,f(y,z,u),f(v,x,f(x,z,u))) = f(v,x,f(x,z,u)). [para(1107(a,1),74(a,1,3)),rewrite(15801(3),15801(6)),flip(a)]. given #640 (A,wt=31): 272 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(32(a,1),18(a,2,3))]. given #641 (T,wt=24): 21177 f(x,f(y,z,u),f(v,x,f(v,z,u))) = f(v,x,f(y,z,u)). [para(1107(a,1),220(a,2,3)),rewrite(1517(5),19(4)),flip(a)]. given #642 (T,wt=24): 21191 f(x,f(y,z,u),f(u,x,f(z,x,v))) = f(x,v,f(z,u,x)). [para(1143(a,1),5(a,2)),rewrite(5(2,R),6(2),5(3,R),6(3),5(4),5(5),5(5))]. given #643 (T,wt=24): 21280 f(x,f(y,z,f(y,u,x)),f(v,u,x)) = f(y,x,f(v,u,x)). [para(1143(a,1),74(a,2,3)),rewrite(5(4,R),3978(6),5(6,R)),flip(a)]. given #644 (T,wt=24): 21292 f(x,f(y,z,x),f(x,u,f(v,y,z))) = f(x,u,f(y,z,x)). [para(79(a,1),1143(a,1)),rewrite(5(3,R),6(3),5(4,R),6(4),21191(5),5(4,R),15462(4),7099(3),5(4),5(4),5(5),5(5),6(6)),flip(a)]. given #645 (A,wt=31): 273 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(32(a,1),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. given #646 (T,wt=24): 21318 f(x,f(y,z,x),f(u,v,f(u,z,x))) = f(u,x,f(y,z,x)). [para(1143(a,1),220(a,2,3)),rewrite(800(6)),flip(a)]. given #647 (T,wt=24): 21513 f(x,y,f(x,f(z,u,v),f(u,v,y))) = f(x,y,f(z,u,v)). [para(5(a,1),1182(a,1)),rewrite(5(2),5(2),5(4),5(4))]. given #648 (T,wt=24): 21514 f(x,f(y,z,u),f(x,v,f(v,z,u))) = f(x,v,f(y,z,u)). [para(1182(a,1),8(a,1)),flip(a)]. given #649 (T,wt=24): 21535 f(x,f(y,z,u),f(z,v,f(x,u,v))) = f(x,v,f(y,z,u)). [para(1182(a,1),26(a,2)),rewrite(6(2),5(3,R),6(3))]. given #650 (A,wt=31): 274 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(24(a,1),32(a,1,3,3)),flip(a)]. given #651 (T,wt=22): 36308 f(x,y,f(z,u,f(x,z,f(v,y,z)))) = f(x,y,z). [para(20490(a,1),21535(a,1,3)),rewrite(6(2),6(4),15462(4),964(3),20(2),6(5),32283(6),35667(4)),flip(a)]. given #652 (T,wt=24): 21569 f(x,f(y,z,u),f(x,u,f(v,y,z))) = f(x,u,f(v,y,z)). [para(1182(a,1),884(a,1,3,3)),rewrite(5(2),5(2),15462(7),1576(7),5(6),5(6),21513(8))]. given #653 (T,wt=22): 36360 f(x,y,f(z,u,f(v,u,f(x,u,y)))) = f(x,u,y). [para(33862(a,1),21569(a,1,3)),rewrite(6(1),6(3),6(4),6(5),15462(5),34502(5),15(1),19(2),6(2),5(4,R),6(4)),flip(a)]. given #654 (T,wt=24): 21578 f(x,f(y,z,u),f(v,z,f(x,v,u))) = f(x,v,f(y,z,u)). [para(1182(a,1),54(a,2,3)),rewrite(95(5),20(7))]. given #655 (A,wt=31): 275 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(32(a,1),25(a,2,3)),rewrite(5(3,R),6(3),57(4),5(8,R),6(8)),flip(a)]. given #656 (T,wt=24): 21596 f(x,f(y,z,u),f(v,u,f(v,x,z))) = f(v,x,f(y,z,u)). [para(1182(a,1),2184(a,2)),rewrite(5(7,R),6(7),15462(9),19704(10),5(6,R),6(6))]. given #657 (T,wt=24): 21623 f(x,f(y,z,u),f(u,v,f(x,z,v))) = f(x,v,f(y,z,u)). [para(1182(a,1),82(a,2)),rewrite(6(2),5(3,R),6(3))]. Low Water (displace, True_semantics): id=31076, wt=37 given #658 (T,wt=21): 36512 f(x,y,f(z,f(x,u,z),f(y,v,z))) = f(x,y,z). [para(4446(a,1),21623(a,2)),rewrite(6(1),6(4),5(7,R),26273(8),36139(8),6(4),27254(7),6(5))]. given #659 (T,wt=24): 21646 f(x,y,f(x,f(y,z,u),f(v,z,u))) = f(x,y,f(v,z,u)). [para(1182(a,1),221(a,2,3)),rewrite(5(4,R),19(5),5(8,R),6(8),19(8))]. given #660 (A,wt=31): 276 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(32(a,1),31(a,2,3)),rewrite(57(4)),flip(a)]. given #661 (T,wt=24): 21719 f(x,f(y,z,u),f(y,x,f(z,x,v))) = f(x,v,f(y,z,x)). [para(1186(a,1),133(a,2)),rewrite(5(2),5(3,R),6(3),5(5),5(7,R),6(7),7475(8),5(5),5(5))]. given #662 (T,wt=24): 21913 f(f(x,y,z),f(y,z,u),f(x,z,f(x,y,v))) = f(x,y,z). [para(5(a,2),1344(a,1,1)),rewrite(5(2,R),6(2),5(4,R),6(4),5(6),5(6))]. given #663 (T,wt=24): 21919 f(f(x,y,z),f(x,z,u),f(y,z,f(x,y,v))) = f(x,y,z). [para(16(a,2),1344(a,1,3))]. given #664 (T,wt=24): 22693 f(x,f(y,z,u),f(v,x,u)) = f(v,x,f(y,u,f(x,z,u))). [para(323(a,2),1498(a,1,3)),rewrite(13318(5))]. given #665 (A,wt=38): 280 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(32(a,1),26(a,2,3,3))]. given #666 (T,wt=24): 22751 f(x,y,f(z,u,f(v,w,z))) = f(x,y,f(v,z,f(w,z,u))). [para(815(a,1),1502(a,2,3)),rewrite(5(4,R),6(4),7760(6),5(4)),flip(a)]. given #667 (T,wt=24): 22753 f(x,y,f(z,u,f(v,w,u))) = f(x,y,f(v,u,f(z,w,u))). [para(847(a,1),1502(a,2,3)),rewrite(5(4,R),6(4),7760(6),5(4))]. given #668 (T,wt=24): 22759 f(x,y,f(z,u,f(v,w,u))) = f(x,y,f(w,u,f(z,v,u))). [para(1668(a,1),1502(a,2,3)),rewrite(5(4,R),6(4),7760(6),5(4))]. given #669 (T,wt=24): 22840 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,u,f(x,y,z))). [para(971(a,1),1502(a,1,3)),rewrite(6(1),5(3),6(3),3281(5),20(5),17208(5),6(4),5(5,R),6(5))]. given #670 (A,wt=38): 286 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(32(a,1),30(a,2,3,3))]. given #671 (T,wt=24): 23040 f(x,f(y,z,u),f(v,y,f(v,x,z))) = f(v,x,f(y,z,u)). [para(1515(a,1),131(a,2,3)),rewrite(103(5),20(7))]. given #672 (T,wt=24): 23115 f(x,f(y,z,u),f(v,z,f(v,x,u))) = f(v,x,f(y,z,u)). [para(1517(a,1),131(a,2,3)),rewrite(103(5),20(7))]. given #673 (T,wt=24): 23577 f(x,f(y,z,u),f(u,x,v)) = f(x,v,f(z,u,f(y,u,x))). [para(1700(a,1),5(a,2)),rewrite(5(2,R),6(2),5(3),5(4),5(4))]. given #674 (T,wt=24): 23579 f(x,f(y,z,u),f(x,v,u)) = f(x,v,f(z,u,f(x,y,u))). [para(1700(a,2),20(a,1,3)),rewrite(6(2),22(4))]. given #675 (A,wt=31): 288 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(33(a,2),8(a,2,3)),flip(a)]. given #676 (T,wt=24): 23691 f(x,y,f(z,u,f(y,v,u))) = f(x,y,f(y,u,f(v,z,u))). [para(1700(a,1),169(a,1,3)),rewrite(6(2),5(5,R),6(5),23638(6),6(5),5(6,R),6(6))]. given #677 (T,wt=24): 23739 f(x,f(y,z,u),f(v,z,f(x,v,y))) = f(x,v,f(y,z,u)). [para(1074(a,1),1700(a,1)),rewrite(6(4),5(5,R),6(5)),flip(a)]. given #678 (T,wt=24): 23741 f(x,f(y,z,u),f(v,x,u)) = f(v,x,f(z,u,f(x,y,u))). [para(1700(a,2),1498(a,1,3)),rewrite(13318(5))]. given #679 (T,wt=24): 23878 f(x,f(y,z,u),f(v,x,f(z,u,x))) = f(v,x,f(z,u,x)). [para(7099(a,1),1811(a,1,3,3)),rewrite(15(6)),flip(a)]. given #680 (A,wt=31): 290 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(33(a,1),17(a,1,3)),rewrite(57(8))]. given #681 (T,wt=24): 23879 f(x,f(y,z,u),f(v,x,f(y,u,x))) = f(v,x,f(y,u,x)). [para(7420(a,1),1811(a,1,3,3)),rewrite(15(6)),flip(a)]. given #682 (T,wt=24): 23887 f(x,f(y,z,u),f(v,x,f(y,z,v))) = f(v,x,f(y,z,u)). [para(1498(a,1),1811(a,1,3)),rewrite(5(2),5(2),896(6),5(4),5(4)),flip(a)]. given #683 (T,wt=24): 23888 f(x,f(y,z,u),f(v,x,f(z,u,v))) = f(v,x,f(y,z,u)). [para(1502(a,1),1811(a,1,3)),rewrite(5(2),5(2),896(6),5(4),5(4)),flip(a)]. given #684 (T,wt=24): 23909 f(f(x,y,z),f(u,x,y),f(z,v,f(x,y,z))) = f(x,y,z). [para(1671(a,1),1883(a,1,2)),rewrite(5(3,R),7099(3),5(4,R),15(4),6(4),5(8,R),7099(8))]. given #685 (A,wt=38): 291 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(33(a,1),18(a,1,3,3))]. given #686 (T,wt=24): 23916 f(f(x,y,z),f(z,u,f(x,y,z)),f(v,x,y)) = f(x,y,z). [para(1671(a,1),1888(a,1,3)),rewrite(5(3,R),7099(3),6(3),5(6,R),15(6),5(8,R),7099(8))]. given #687 (T,wt=24): 23949 f(x,f(y,z,u),f(v,x,f(x,y,u))) = f(v,x,f(x,y,u)). [para(2067(a,1),74(a,1,3)),rewrite(15824(3),15824(6)),flip(a)]. given #688 (T,wt=24): 23958 f(x,f(y,z,u),f(v,x,f(v,y,u))) = f(v,x,f(y,z,u)). [para(2067(a,1),220(a,2,3)),rewrite(7472(5),19(4)),flip(a)]. given #689 (T,wt=24): 24041 f(x,y,f(x,f(z,u,v),f(z,v,y))) = f(x,y,f(z,u,v)). [para(5(a,1),4720(a,1)),rewrite(5(2),5(2),5(4),5(4))]. given #690 (A,wt=38): 292 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(33(a,2),18(a,2,3,3))]. given #691 (T,wt=24): 24042 f(x,f(y,z,u),f(x,v,f(v,y,u))) = f(x,v,f(y,z,u)). [para(4720(a,1),8(a,1)),flip(a)]. given #692 (T,wt=24): 24050 f(x,f(y,z,u),f(y,v,f(x,u,v))) = f(x,v,f(y,z,u)). [para(4720(a,1),26(a,2)),rewrite(6(2),5(3,R),6(3))]. given #693 (T,wt=24): 24067 f(x,f(y,z,u),f(x,u,f(y,v,z))) = f(x,u,f(y,v,z)). [para(4720(a,1),884(a,1,3,3)),rewrite(5(2),5(2),15462(7),23597(6),6(5),19427(7),5(6),5(6),24041(8))]. given #694 (T,wt=24): 24071 f(x,f(y,z,u),f(v,y,f(x,v,u))) = f(x,v,f(y,z,u)). [para(4720(a,1),54(a,2,3)),rewrite(95(5),20(7))]. given #695 (A,wt=31): 293 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(33(a,2),18(a,2,3)),flip(a)]. given #696 (T,wt=24): 24083 f(x,f(y,z,u),f(v,u,f(v,x,y))) = f(v,x,f(y,z,u)). [para(4720(a,1),2184(a,2)),rewrite(5(7,R),6(7),15462(9),19704(10),5(6,R),6(6))]. given #697 (T,wt=24): 24098 f(x,f(y,z,u),f(u,v,f(x,y,v))) = f(x,v,f(y,z,u)). [para(4720(a,1),82(a,2)),rewrite(6(2),5(3,R),6(3))]. given #698 (T,wt=24): 24108 f(x,y,f(x,f(y,z,u),f(z,v,u))) = f(x,y,f(z,v,u)). [para(4720(a,1),221(a,2,3)),rewrite(5(4,R),19(5),5(8,R),6(8),19(8))]. given #699 (T,wt=24): 24144 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(x,y,f(z,y,v))). [para(4803(a,1),5(a,2)),rewrite(6(3),5(5,R),6(5))]. given #700 (A,wt=38): 294 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(18(a,1),33(a,2,3,3)),rewrite(57(4))]. given #701 (T,wt=24): 24157 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(z,y,f(x,y,u))). [para(5117(a,1),5(a,2)),rewrite(6(3),5(4,R),6(4))]. given #702 (T,wt=24): 24195 f(x,y,f(z,y,f(y,u,v))) = f(z,y,f(y,v,f(x,y,u))). [para(5161(a,1),5(a,2)),rewrite(6(3),5(4,R),6(4))]. given #703 (T,wt=22): 37181 f(x,y,f(z,x,f(z,u,f(v,z,y)))) = f(z,x,y). [para(7365(a,1),24195(a,1,3)),rewrite(15(3),6(4),6(6),35143(7),5(4),5(4),36221(7),205(4),15462(4)),flip(a)]. given #704 (T,wt=22): 37188 f(x,y,f(z,u,f(v,z,f(x,z,y)))) = f(x,z,y). [para(20060(a,1),24195(a,1,3)),rewrite(5(4,R),15(4),15(3),5(5),6(5),6(7),26972(8),122(5),33481(7)),flip(a)]. given #705 (A,wt=38): 295 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(18(a,2),33(a,2,3,3)),rewrite(57(4),6(6))]. given #706 (T,wt=24): 24209 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(y,v,f(x,z,y))). [para(5167(a,1),5(a,2)),rewrite(6(3),5(4))]. given #707 (T,wt=24): 24243 f(x,y,f(x,f(z,u,y),f(x,v,z))) = f(x,v,f(x,z,y)). [para(323(a,2),5167(a,1,3)),rewrite(5(2),16077(3),5(4),5(4)),flip(a)]. given #708 (T,wt=24): 24363 f(x,y,f(z,u,f(z,y,v))) = f(z,y,f(x,y,f(z,v,u))). [para(6853(a,2),5(a,2)),rewrite(6(3),5(4,R),6(4)),flip(a)]. given #709 (T,wt=24): 24549 f(f(x,y,z),f(x,u,y),f(z,v,f(x,y,z))) = f(x,y,z). [para(7456(a,1),1883(a,1,2)),rewrite(5(3,R),7420(3),5(4,R),15(4),6(4),5(8,R),7420(8))]. given #710 (A,wt=31): 296 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(33(a,1),24(a,1,3)),rewrite(5(2,R),6(2),5(8,R),6(8))]. given #711 (T,wt=24): 24550 f(f(x,y,z),f(z,u,f(x,y,z)),f(x,v,y)) = f(x,y,z). [para(7456(a,1),1888(a,1,3)),rewrite(5(3,R),7420(3),6(3),5(6,R),15(6),5(8,R),7420(8))]. given #712 (T,wt=24): 24598 f(x,f(y,z,u),f(v,y,f(v,x,u))) = f(v,x,f(y,z,u)). [para(7472(a,1),131(a,2,3)),rewrite(103(5),20(7))]. given #713 (T,wt=24): 24636 f(x,f(y,z,u),f(v,x,f(y,u,v))) = f(v,x,f(y,z,u)). [para(7472(a,1),7475(a,1,3)),rewrite(5(2),5(2),896(6),5(4),5(4)),flip(a)]. given #714 (T,wt=24): 24664 f(x,y,f(x,z,f(y,u,v))) = f(x,z,f(x,y,f(z,u,v))). [back_rewrite(19732),rewrite(24658(4),24658(7))]. given #715 (A,wt=31): 297 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(33(a,2),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. given #716 (T,wt=24): 24707 f(x,f(y,z,u),f(z,v,x)) = f(v,x,f(y,z,f(z,u,x))). [para(7879(a,1),5(a,2)),rewrite(5(2),5(3),5(4),5(4))]. given #717 (T,wt=24): 24811 f(x,f(y,z,f(u,y,x)),f(u,x,f(u,y,v))) = f(u,y,x). [para(8193(a,1),220(a,2,3)),rewrite(6(1),6(3),6(5),3978(7),884(3),6(2)),flip(a)]. given #718 (T,wt=24): 24856 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,u,f(y,z,x))). [para(25(a,2),8248(a,2,3)),rewrite(5(2),5(5,R),6(5),1811(6),5(4),5(4))]. given #719 (T,wt=24): 24871 f(x,f(y,z,u),f(z,x,v)) = f(x,v,f(z,u,f(y,z,x))). [para(847(a,2),8248(a,2,3)),rewrite(5(2),5(5,R),6(5),1811(6),5(4),5(4))]. given #720 (A,wt=31): 299 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,z,f(x,y,f(x,w,f(x,v,u)))). [para(33(a,2),25(a,2,3)),rewrite(5(3,R),6(3),57(4),6(5),5(8,R),6(8))]. given #721 (T,wt=24): 24872 f(x,f(y,z,u),f(x,v,f(y,x,z))) = f(x,v,f(y,x,z)). [para(899(a,1),8248(a,1,3,3)),rewrite(6(3),896(6)),flip(a)]. given #722 (T,wt=24): 24873 f(x,f(y,z,f(y,x,u)),f(z,x,v)) = f(x,v,f(y,z,x)). [para(791(a,1),8248(a,2,3)),rewrite(5(1,R),6(1),5(3),5(4,R),6(4),5(7,R),6(7),1811(8),5(5),5(5))]. given #723 (T,wt=24): 24874 f(x,f(y,z,f(z,x,u)),f(y,x,v)) = f(x,v,f(y,z,x)). [para(793(a,1),8248(a,2,3)),rewrite(5(1,R),6(1),5(3),5(4,R),6(4),5(7,R),6(7),1811(8),5(5),5(5))]. given #724 (T,wt=24): 24877 f(x,y,f(z,x,f(u,x,v))) = f(x,y,f(x,v,f(u,z,x))). [para(1668(a,1),8248(a,2,3)),rewrite(8248(6)),flip(a)]. given #725 (A,wt=31): 301 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(33(a,2),31(a,2,3)),rewrite(57(4),6(5))]. given #726 (T,wt=24): 24914 f(x,f(y,z,x),f(x,u,f(y,v,z))) = f(x,u,f(y,z,x)). [para(7420(a,1),8248(a,1,3,3)),rewrite(6(3),15(6)),flip(a)]. given #727 (T,wt=24): 24935 f(x,f(y,z,f(z,u,x)),f(y,x,v)) = f(x,v,f(y,z,x)). [para(12063(a,1),8248(a,2,3)),rewrite(5(1),5(3),5(4),5(7,R),6(7),1811(8),5(5),5(5))]. given #728 (T,wt=24): 24961 f(x,f(y,z,f(z,u,x)),f(u,x,v)) = f(x,v,f(z,u,x)). [para(18416(a,1),8248(a,2,3)),rewrite(5(1),5(1),5(2,R),6(2),29(3),5(3),5(4),5(4),5(5,R),6(5),29(6),5(7,R),6(7),1811(8),5(5),6(5))]. given #729 (T,wt=24): 24963 f(x,f(y,z,f(y,u,x)),f(z,x,v)) = f(x,v,f(y,z,x)). [para(18598(a,1),8248(a,2,3)),rewrite(5(3),5(7,R),6(7),1811(8),6(5))]. given #730 (A,wt=31): 304 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(33(a,1),29(a,1,3,3)),rewrite(103(5))]. given #731 (T,wt=24): 25193 f(x,f(y,z,u),f(z,x,f(y,u,v))) = f(z,x,f(y,u,v)). [para(8373(a,1),169(a,1,3)),rewrite(5(3,R),6(3),5(5,R),6(5),15(6),5(5,R),6(5)),flip(a)]. given #732 (T,wt=24): 25199 f(x,f(y,z,u),f(v,x,f(y,v,z))) = f(v,x,f(y,z,u)). [para(8373(a,1),8248(a,1,3)),rewrite(5(3),5(5,R),6(5),15(6),5(5,R),6(5)),flip(a)]. given #733 (T,wt=24): 25200 f(x,f(y,z,u),f(v,z,x)) = f(v,x,f(y,z,f(z,u,x))). [para(8454(a,2),5(a,2)),rewrite(6(3),5(5)),flip(a)]. given #734 (T,wt=24): 25208 f(x,y,f(z,u,f(u,v,y))) = f(x,y,f(u,y,f(z,u,v))). [para(8454(a,2),205(a,1,3)),rewrite(5(4),9561(6),5(6,R),6(6)),flip(a)]. given #735 (A,wt=31): 306 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(33(a,1),122(a,1,3,3)),rewrite(5(4,R),6(4),103(5),5(8,R),6(8))]. given #736 (T,wt=24): 25357 f(x,y,f(x,f(y,z,u),f(x,u,v))) = f(x,v,f(x,y,u)). [para(5(a,1),9696(a,1,3,2)),rewrite(5(1,R),6(1),5(2),5(2),5(6,R),6(6))]. given #737 (T,wt=24): 25358 f(x,y,f(x,f(y,z,u),f(x,z,v))) = f(x,v,f(x,y,z)). [para(5(a,1),9696(a,1,3,3)),rewrite(5(2),5(6,R),6(6))]. given #738 (T,wt=24): 25380 f(x,y,f(x,f(z,y,u),f(x,z,v))) = f(x,v,f(x,z,y)). [para(5(a,1),9721(a,1)),rewrite(5(2),5(2),5(4),5(4),5(6,R),6(6))]. given #739 (T,wt=24): 25436 f(x,y,f(z,u,f(z,v,x))) = f(z,x,f(x,y,f(z,v,u))). [para(9899(a,1),2726(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),5(5,R),6(5),5(7,R),6(7),7014(8),5(4),5(4),5(6,R),6(6)),flip(a)]. given #740 (A,wt=38): 307 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(33(a,1),26(a,1,3,3))]. given #741 (T,wt=24): 25480 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(y,u,f(x,z,y))). [para(10164(a,1),5(a,2)),rewrite(6(3),5(4))]. given #742 (T,wt=24): 25496 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(x,y,f(z,y,u))). [para(10182(a,1),5(a,2)),rewrite(6(3),5(5,R),6(5))]. given #743 (T,wt=24): 25556 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(z,u,f(x,y,z))). [para(10898(a,2),1182(a,2)),rewrite(23897(5),20(5),803(5))]. given #744 (T,wt=24): 25626 f(x,f(y,z,x),f(u,v,f(z,x,u))) = f(x,u,f(y,z,x)). [para(1143(a,1),12563(a,1,3)),rewrite(5(3,R),6(3),5(4),5(4),21167(6),5(7,R),6(7),205(8))]. given #745 (A,wt=38): 308 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(33(a,2),26(a,2,3,3))]. given #746 (T,wt=24): 25652 f(x,y,f(y,f(x,z,u),f(y,v,z))) = f(x,y,f(y,v,z)). [para(75(a,2),158(a,2,3)),rewrite(791(3),29(3)),flip(a)]. given #747 (T,wt=24): 25668 f(x,f(y,z,u),f(y,x,f(x,z,v))) = f(x,v,f(y,x,z)). [para(791(a,1),13587(a,1,3,3)),rewrite(5(1,R),6(1),5(3,R),6(3),5(4),5(4),24997(6),5(3,R),6(3),5(5,R),6(5),25331(6)),flip(a)]. given #748 (T,wt=24): 25679 f(x,f(y,z,u),f(y,x,f(x,u,v))) = f(x,v,f(y,x,u)). [para(18598(a,1),13587(a,1,3,3)),rewrite(5(3,R),6(3),6(4),25009(6),5(5,R),6(5),25331(6)),flip(a)]. given #749 (T,wt=24): 25692 f(x,f(y,z,u),f(y,x,f(x,v,z))) = f(y,x,f(x,v,z)). [back_rewrite(21303),rewrite(6(3),6(4),1355(6),6(3),6(4)),flip(a)]. given #750 (A,wt=31): 310 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(26(a,2),33(a,2,3))]. given #751 (T,wt=24): 25694 f(x,y,f(z,u,f(y,v,u))) = f(x,y,f(v,u,f(y,z,u))). [para(5(a,2),14140(a,1,3)),rewrite(6(2),6(4))]. given #752 (T,wt=24): 25706 f(x,y,f(z,u,f(v,z,x))) = f(z,x,f(x,y,f(v,z,u))). [para(14140(a,2),2726(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),5(5,R),6(5),5(7,R),6(7),7972(8),5(4),5(4),5(6,R),6(6)),flip(a)]. given #753 (T,wt=24): 25717 f(x,f(y,z,u),f(v,x,z)) = f(v,x,f(z,u,f(x,y,z))). [para(14140(a,2),1517(a,2)),rewrite(23897(5),20(5),17208(5))]. given #754 (T,wt=24): 25790 f(x,f(y,z,u),f(y,v,x)) = f(v,x,f(y,z,f(y,x,u))). [para(5(a,1),15181(a,1)),rewrite(5(3,R),6(4))]. given #755 (A,wt=44): 312 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(33(a,2),28(a,1,3,3))]. given #756 (T,wt=24): 25838 f(x,f(y,z,x),f(z,u,v)) = f(y,x,f(z,u,f(z,x,v))). [para(15182(a,2),6(a,2)),rewrite(5(1,R),6(1),6(3),6(4)),flip(a)]. given #757 (T,wt=24): 25908 f(x,f(y,z,x),f(z,u,v)) = f(y,x,f(z,x,f(z,u,v))). [para(15182(a,2),7456(a,2)),rewrite(5(1,R),6(1),5(3,R),6(3),6(4),20(4),25726(5),13448(5),6(4)),flip(a)]. given #758 (T,wt=24): 26342 f(x,y,f(x,f(z,u,y),f(x,u,v))) = f(x,v,f(x,u,y)). [para(1143(a,1),15462(a,2)),rewrite(6(2),15462(4))]. given #759 (T,wt=24): 26404 f(x,f(y,z,u),f(x,z,f(x,u,v))) = f(x,v,f(x,z,u)). [back_rewrite(24356),rewrite(26268(8),20197(8))]. given #760 (A,wt=38): 313 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(33(a,1),30(a,1,3,3))]. given #761 (T,wt=24): 26421 f(x,y,f(x,z,f(z,u,v))) = f(x,y,f(x,z,f(y,u,v))). [back_rewrite(25926),rewrite(26312(5),24666(4)),flip(a)]. given #762 (T,wt=24): 26527 f(x,y,f(x,f(z,y,u),f(x,u,v))) = f(x,v,f(x,y,u)). [para(964(a,1),15489(a,2,3)),rewrite(6(3),26268(4))]. given #763 (T,wt=24): 26623 f(x,f(y,z,u),f(x,y,f(x,z,v))) = f(x,v,f(x,y,z)). [para(15489(a,2),1158(a,1)),rewrite(5(2),5(2),5(6,R),6(6))]. given #764 (T,wt=24): 27290 f(x,f(y,z,u),f(x,v,f(x,y,z))) = f(x,v,f(x,y,z)). [para(12560(a,1),27138(a,1,3)),rewrite(5(3),5(4,R),6(4),5(5,R),5(6,R),6(6),5(7),5(8,R),6(8),6(9),15462(9),15462(8),19311(9),5(4),5(5,R),6(5)),flip(a)]. given #765 (A,wt=38): 314 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(33(a,2),30(a,2,3,3))]. given #766 (T,wt=24): 27311 f(x,f(y,z,f(y,u,x)),f(u,x,v)) = f(y,x,f(u,x,v)). [para(15812(a,1),5(a,2)),rewrite(5(1),5(4),5(6,R),6(6))]. given #767 (T,wt=24): 27313 f(x,f(y,z,u),f(x,y,f(x,u,v))) = f(x,v,f(x,y,u)). [para(15812(a,1),20(a,1,3)),rewrite(5(1),5(1),5(3,R),6(3),26264(5),22(5),5(5),5(5),5(7,R),6(7),26264(8),25357(8))]. given #768 (T,wt=24): 27315 f(x,f(y,z,u),f(x,v,f(x,y,u))) = f(x,y,f(x,u,v)). [para(15812(a,1),785(a,2)),rewrite(5(1),5(1),5(3,R),6(3),5(4),5(4),5(6,R),6(6),5(7),15462(8),25948(8),884(5),26264(6),1551(6),5(5,R),6(5))]. given #769 (T,wt=24): 27378 f(x,f(y,z,u),f(x,z,f(x,y,v))) = f(x,v,f(x,y,z)). [para(15831(a,1),12714(a,2)),rewrite(5(2,R),6(2),5(4),25555(5),801(5),5(5))]. given #770 (A,wt=38): 316 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(30(a,2),33(a,2,3,3)),rewrite(6(3),57(4)),flip(a)]. given #771 (T,wt=24): 27719 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,u,f(y,x,z))). [para(76(a,2),27700(a,2)),rewrite(6(8),26276(9),26271(7),6(2),5(4,R),6(4),814(6))]. given #772 (T,wt=24): 27771 f(x,f(y,z,u),f(x,y,f(x,v,z))) = f(x,v,f(x,y,z)). [para(5(a,1),15984(a,1)),rewrite(5(1,R),6(1),5(4,R),5(6,R),6(6))]. given #773 (T,wt=24): 27781 f(x,f(y,z,u),f(x,z,f(x,v,y))) = f(x,v,f(x,y,z)). [para(15984(a,1),21(a,1,3)),rewrite(5(1,R),6(1),6(2),5(3,R),6(3),15462(4),22(3),20(3),5(3,R),6(3),5(4,R),6(4)),flip(a)]. given #774 (T,wt=24): 27897 f(x,f(y,z,u),f(v,y,f(v,z,x))) = f(v,x,f(y,z,u)). [para(15990(a,1),794(a,2)),rewrite(5(3,R),6(3),5(5,R),6(5),6(7),25331(8),27085(9),5(6,R),6(6))]. given #775 (A,wt=38): 317 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(32(a,1),33(a,2,3,3)),rewrite(57(4))]. given #776 (T,wt=24): 27975 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(z,u,v))). [para(15993(a,1),54(a,2,3)),rewrite(6(2),5(3,R),6(3),21580(5),5(4),5(4)),flip(a)]. given #777 (T,wt=24): 28089 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(u,v,z))). [para(15998(a,1),141(a,2,3)),rewrite(6(2),5(3,R),6(3),20037(5),5(4),5(4))]. given #778 (T,wt=24): 28112 f(x,y,f(x,f(y,z,u),f(v,x,u))) = f(v,x,f(x,y,u)). [para(6052(a,1),173(a,2,3)),rewrite(6(1),26264(4),6(5),20(8),26264(8),15(9),29(7))]. given #779 (T,wt=24): 28113 f(x,y,f(x,f(z,y,u),f(v,x,u))) = f(v,x,f(x,y,u)). [para(6453(a,1),173(a,2,3)),rewrite(6(1),26268(4),6(5),20(8),26268(8),15(9),29(7))]. given #780 (A,wt=38): 318 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(33(a,2),33(a,2,3,3)),rewrite(57(4),6(6))]. given #781 (T,wt=24): 28175 f(x,f(y,z,f(y,x,u)),f(v,z,f(y,z,x))) = f(y,z,x). [para(16052(a,1),74(a,2,3)),rewrite(5(1),5(1),5(3),5(3),5(5),6(5),964(5),5(4,R),6(4),26268(5),1546(5),15801(3),5(2),5(2),5(4),6(4),5(6,R)),flip(a)]. given #782 (T,wt=24): 28177 f(x,f(y,z,f(u,z,x)),f(u,z,f(u,x,v))) = f(u,z,x). [para(16052(a,1),220(a,2,3)),rewrite(5(1),5(1),5(3),5(3),5(5),964(5),5(4,R),6(4),26268(5),1546(5),15801(3),5(2),5(2),5(4),6(4)),flip(a)]. Low Water (keep, True_semantics): wt=35 given #783 (T,wt=22): 38506 f(x,y,f(x,z,f(u,y,f(v,z,y)))) = f(x,z,y). [para(15899(a,1),28177(a,1,3)),rewrite(6(1),6(3),5(5),884(5),6(4),31948(4),5(1),5(2,R),6(2),5(4,R),15(4),5(4,R),15(4),6(4),6(5),5(7),884(7))]. given #784 (T,wt=24): 28186 f(x,f(y,z,f(z,x,u)),f(u,v,f(z,x,u))) = f(z,x,u). [para(16052(a,1),1158(a,2)),rewrite(5(1),5(3),5(5),5(7),4(7),5(6,R),5(7,R),6(7),26526(7),1855(5),5(6),5(8),5(8),1855(8),5(7,R),6(7),19(7))]. given #785 (A,wt=31): 319 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(33(a,2),33(a,2,3)),rewrite(57(3),6(1)),flip(a)]. given #786 (T,wt=24): 28199 f(x,y,f(y,f(z,x,u),f(z,y,v))) = f(y,v,f(z,x,y)). [para(16053(a,1),205(a,1,3)),rewrite(5(2),6(2),5(3,R),6(3),5(4),5(4),5(5,R),6(5),19076(6),5(6),6(6),5(7,R),6(7),19077(8))]. given #787 (T,wt=24): 28283 f(x,f(y,z,u),f(x,y,f(x,v,u))) = f(x,y,f(x,v,u)). [para(12782(a,1),177(a,1,3,3)),rewrite(5(2),15824(3),5(4),27315(6),6(3),15462(5),15462(4),21(3),20(3),22(3),5(5),27315(7),6(4)),flip(a)]. given #788 (T,wt=24): 28315 f(x,f(y,z,u),f(x,v,f(y,v,z))) = f(x,v,f(y,z,u)). [para(16113(a,1),785(a,2)),rewrite(5(7),15462(8),25948(8),1576(7))]. given #789 (T,wt=24): 28328 f(x,f(y,z,u),f(y,v,f(v,z,x))) = f(v,x,f(y,z,u)). [para(16113(a,1),2184(a,2)),rewrite(5(3,R),6(3),5(5,R),6(5),6(8),5(9,R),6(9),8729(11),5(6,R),6(6))]. given #790 (A,wt=31): 326 f(x,y,f(x,f(z,u,v),f(x,w,z))) = f(x,w,f(x,y,f(z,u,f(x,z,v)))). [para(38(a,2),8(a,2,3)),flip(a)]. given #791 (T,wt=24): 28337 f(x,y,f(x,f(z,y,u),f(z,u,v))) = f(x,y,f(z,u,v)). [para(16113(a,1),130(a,2,3)),rewrite(22(6),16113(8))]. given #792 (T,wt=24): 28833 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(u,z,v))). [para(16693(a,1),77(a,2,3)),rewrite(6(2),24072(5),6(4)),flip(a)]. given #793 (T,wt=24): 28855 f(x,f(y,z,u),f(v,u,f(x,v,y))) = f(x,v,f(y,z,u)). [para(16693(a,1),16534(a,1)),rewrite(6(4)),flip(a)]. given #794 (T,wt=24): 29033 f(x,f(y,z,u),f(x,z,f(y,x,v))) = f(x,v,f(y,x,z)). [para(17196(a,1),793(a,2)),rewrite(6(7),15462(8),15462(7),17106(9))]. given #795 (A,wt=37): 334 f(x,f(y,z,u),f(v,f(y,x,w),f(y,z,u))) = f(v,f(y,z,u),f(x,w,f(y,z,f(y,u,x)))). [para(38(a,1),16(a,1,3)),rewrite(5(2),5(2),5(5,R),6(5),5(8),5(9,R)),flip(a)]. given #796 (T,wt=24): 29132 f(x,f(y,z,u),f(x,u,f(y,x,v))) = f(x,v,f(y,x,u)). [para(17333(a,1),793(a,2)),rewrite(6(7),15462(8),15462(7),17106(9))]. given #797 (T,wt=24): 29141 f(x,f(y,z,u),f(x,v,f(y,x,u))) = f(x,v,f(y,x,u)). [para(17333(a,1),74(a,2,3)),rewrite(20(5),17333(4)),flip(a)]. given #798 (T,wt=24): 29148 f(x,f(y,z,u),f(y,x,f(u,x,v))) = f(x,v,f(y,u,x)). [para(17333(a,1),7475(a,1,3)),rewrite(5(2,R),6(2),6(4),27802(6),5(4,R),6(4)),flip(a)]. given #799 (T,wt=24): 29206 f(x,f(y,z,f(x,u,z)),f(u,z,f(x,v,u))) = f(x,u,z). [para(16052(a,1),188(a,1,3,3)),rewrite(5(1,R),6(1),5(3),986(3),5(3,R),6(3),5(5),16445(7),18598(5),6(4),15462(4),964(3),20(2),5(2,R),6(2),5(4,R),6(4),5(6),16169(7)),flip(a)]. given #800 (A,wt=38): 344 f(x,f(y,z,u),f(x,v,f(x,w,f(x,v6,y)))) = f(x,v,f(x,w,f(x,v6,f(y,z,f(x,y,u))))). [para(38(a,1),18(a,1,3,3)),flip(a)]. given #801 (T,wt=22): 38745 f(x,y,f(x,z,f(u,y,f(z,v,y)))) = f(x,z,y). [para(24935(a,1),29206(a,1,3)),rewrite(3978(5),6(4),32806(4),4(5),6(4),3978(7))]. given #802 (T,wt=24): 29215 f(x,f(y,z,u),f(y,x,f(v,z,u))) = f(y,x,f(v,z,u)). [para(1517(a,1),29179(a,2)),rewrite(5(8,R),6(8),15462(9),25959(10),5370(7))]. given #803 (T,wt=24): 29216 f(x,f(y,z,u),f(y,x,f(z,v,u))) = f(y,x,f(z,v,u)). [para(7472(a,1),29179(a,2)),rewrite(5(8,R),6(8),15462(9),25959(10),5370(7))]. given #804 (T,wt=24): 29320 f(x,y,f(z,u,f(z,v,x))) = f(z,x,f(x,y,f(z,u,v))). [para(5(a,1),18371(a,1)),rewrite(5(3),6(3),6(4),5(5,R),6(5))]. given #805 (A,wt=38): 350 f(x,y,f(x,z,f(x,f(u,v,w),f(x,v6,u)))) = f(x,z,f(x,v6,f(x,y,f(u,v,f(x,u,w))))). [para(38(a,2),18(a,2,3,3)),flip(a)]. given #806 (T,wt=24): 29321 f(x,y,f(z,u,f(z,v,y))) = f(z,y,f(x,y,f(z,u,v))). [para(18371(a,1),6(a,2)),rewrite(6(3),6(4))]. given #807 (T,wt=24): 29507 f(x,f(y,z,u),f(v,u,f(x,v,z))) = f(x,v,f(y,z,u)). [para(15993(a,1),18761(a,1)),flip(a)]. given #808 (T,wt=24): 29619 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(x,z,f(y,u,v))). [back_rewrite(27300),rewrite(29590(5),24666(4)),flip(a)]. given #809 (T,wt=24): 29702 f(x,y,f(z,u,f(v,u,x))) = f(x,y,f(u,x,f(z,v,u))). [para(323(a,1),19342(a,2)),rewrite(4(3),5(3),4(3),5(2,R),6(2),5(3,R),25893(3),5(4),5(4)),flip(a)]. given #810 (A,wt=37): 358 f(x,f(y,z,u),f(v,f(y,z,u),f(y,x,w))) = f(v,f(y,z,u),f(x,w,f(y,z,f(y,u,x)))). [para(38(a,1),24(a,1,3)),rewrite(5(2),5(2),5(8)),flip(a)]. given #811 (T,wt=24): 29715 f(x,y,f(z,u,f(v,u,x))) = f(x,y,f(u,x,f(v,z,u))). [para(1700(a,1),19342(a,2)),rewrite(4(3),5(3),4(3),5(2,R),6(2),5(3,R),25893(3),5(4),5(4)),flip(a)]. given #812 (T,wt=24): 30172 f(x,y,f(z,f(x,u,v),f(y,u,v))) = f(x,y,f(z,u,v)). [para(29827(a,1),1498(a,1,3)),rewrite(5(2),5(5))]. given #813 (T,wt=24): 30246 f(x,y,f(z,f(y,u,v),f(x,u,v))) = f(x,y,f(z,u,v)). [para(29827(a,1),14302(a,1,3)),rewrite(5(2),5(5))]. given #814 (T,wt=24): 30286 f(x,f(y,z,x),f(x,u,v)) = f(x,u,f(y,x,f(z,x,v))). [para(16974(a,2),29827(a,2)),rewrite(5(2,R),6(2),5(3),4(3),5(3),5(4,R),6(4),15462(7),12539(6))]. Low Water (displace, True_semantics): id=36281, wt=36 given #815 (A,wt=37): 361 f(x,f(y,z,u),f(v,f(y,z,u),f(x,y,w))) = f(v,f(y,z,u),f(x,w,f(y,z,f(x,y,u)))). [para(38(a,1),24(a,2,3)),rewrite(6(3))]. given #816 (T,wt=24): 31062 f(x,f(y,z,x),f(x,u,v)) = f(y,x,f(z,x,f(x,u,v))). [para(16974(a,2),29829(a,2)),rewrite(5(3),4(3),5(3),15462(7),24943(7))]. given #817 (T,wt=24): 31111 f(x,f(y,z,u),f(x,z,f(v,x,u))) = f(v,x,f(x,z,u)). [para(29872(a,1),41(a,1,3)),rewrite(5(2),15801(3)),flip(a)]. given #818 (T,wt=24): 31134 f(x,f(y,z,u),f(x,u,f(v,x,y))) = f(x,u,f(v,x,y)). [para(29872(a,1),4980(a,1,3,3)),rewrite(1106(4),5(4,R),29069(4),5(1,R),6(1),5(6))]. given #819 (T,wt=24): 31139 f(x,f(y,z,u),f(x,u,f(v,x,z))) = f(v,x,f(x,z,u)). [para(29872(a,1),87(a,1,3)),rewrite(5(2),15801(3)),flip(a)]. given #820 (A,wt=31): 362 f(x,y,f(z,f(u,v,w),f(z,x,u))) = f(z,x,f(x,y,f(u,v,f(z,u,w)))). [para(38(a,2),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. given #821 (T,wt=24): 31147 f(x,y,f(x,f(z,u,y),f(v,x,u))) = f(v,x,f(x,u,y)). [para(29872(a,1),510(a,1,3)),rewrite(5(2),15801(3)),flip(a)]. given #822 (T,wt=24): 31191 f(x,f(y,z,u),f(x,y,f(v,x,u))) = f(v,x,f(x,y,u)). [para(29873(a,1),41(a,1,3)),rewrite(5(2),15824(3)),flip(a)]. given #823 (T,wt=24): 31297 f(x,y,f(z,f(u,v,y),f(x,u,v))) = f(x,y,f(z,u,v)). [para(29875(a,1),26(a,2,3)),rewrite(6(2),5(3,R),6(3),21535(4),5(3),5(3),5(4)),flip(a)]. given #824 (T,wt=24): 31490 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(z,y,f(x,y,v))). [para(29876(a,2),26(a,1)),rewrite(5(1,R),6(1),5(3),5(3),6(4),25959(4),5(4),5(7,R),6(7),31248(7))]. given #825 (A,wt=31): 364 f(x,f(y,z,f(z,u,v)),f(x,u,w)) = f(x,w,f(z,u,f(x,u,f(y,z,v)))). [para(24(a,1),38(a,1,2)),rewrite(5(1,R),6(1),6(3),5(7,R),6(7))]. given #826 (T,wt=24): 31953 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(y,u,f(x,y,v))). [back_rewrite(27033),rewrite(31937(5),103(4),31952(7))]. given #827 (T,wt=24): 31974 f(x,y,f(z,u,f(v,y,z))) = f(x,y,f(y,z,f(v,x,u))). [back_rewrite(26717),rewrite(31948(4),5(1),5(5,R),6(5),31937(7),5(4,R),6(4))]. given #828 (T,wt=24): 31978 f(x,y,f(z,u,f(y,v,z))) = f(x,y,f(y,z,f(x,v,u))). [back_rewrite(6889),rewrite(31948(4),6(1),20(4),31937(7))]. given #829 (T,wt=24): 31996 f(x,y,f(z,u,f(v,z,x))) = f(z,x,f(y,u,f(v,x,y))). [back_rewrite(8179),rewrite(31948(4),5(1),31947(7),5(4)),flip(a)]. given #830 (A,wt=44): 379 f(x,f(y,z,u),f(v,f(y,z,u),f(x,w,f(y,z,f(x,y,u))))) = f(x,f(y,z,u),f(v,f(x,y,w),f(y,z,u))). [para(38(a,1),29(a,1,3,3)),rewrite(5(6,R),6(6),6(10),5(11,R))]. given #831 (T,wt=24): 32004 f(x,y,f(z,u,f(y,z,v))) = f(x,y,f(y,z,f(x,u,v))). [back_rewrite(31265),rewrite(5(3,R),6(3),30875(4),31949(4),6(1),31948(7)),flip(a)]. given #832 (T,wt=24): 32041 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(y,v,f(x,y,u))). [back_rewrite(18584),rewrite(6(1),6(3),31948(6),5(3),5(4,R),6(4),25932(4),5(2,R),6(2),32006(4),6(5),31947(7)),flip(a)]. given #833 (T,wt=24): 32044 f(x,y,f(z,u,f(v,u,x))) = f(u,x,f(x,y,f(z,v,u))). [back_rewrite(16737),rewrite(31948(8),29680(8),26264(6),6(3),31952(8),15371(6)),flip(a)]. given #834 (T,wt=24): 32060 f(x,y,f(z,u,f(u,v,x))) = f(u,x,f(x,y,f(z,u,v))). [back_rewrite(8727),rewrite(31948(8),29680(8),26264(6),6(3),31952(8),15371(6)),flip(a)]. given #835 (A,wt=44): 392 f(x,f(y,z,u),f(x,v,f(w,f(x,y,v6),f(y,z,u)))) = f(x,v,f(w,f(y,z,u),f(x,v6,f(y,z,f(x,y,u))))). [para(38(a,1),26(a,1,3,3)),rewrite(5(5,R),6(5),6(9),5(10,R)),flip(a)]. given #836 (T,wt=24): 32078 f(x,y,f(z,u,f(y,u,v))) = f(x,y,f(y,u,f(z,x,v))). [back_rewrite(31092),rewrite(31952(4),5(2,R),6(2),31949(7),5(4,R),6(4))]. ============================== PROOF ================================= % Proof 1 at 745.23 (+ 1.29) seconds: dist_both. % Length of proof is 324. % Level of proof is 41. % Maximum clause weight is 44. % Given clauses 836. 3 f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) & f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_both) # label(goal). [goal]. 4 f(x,x,y) = x # label(majority). [assumption]. 5 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 6 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. 7 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. 8 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(7),rewrite(5(2),5(2),5(3,R),6(3)),rewrite(5(1,R),6(1),6(3),5(4,R),6(4))]. 13 f(f(c11,c14,c15),f(c12,c14,c15),f(c13,c14,c15)) != f(f(c11,c12,c13),c14,c15) | f(f(c11,c12,c13),c14,c15) != f(c11,f(c12,c14,c15),f(c13,c14,c15)) # label(dist_both) # answer(dist_both). [deny(3)]. 14 f(f(c11,c14,c15),f(c12,c14,c15),f(c13,c14,c15)) != f(c14,c15,f(c11,c12,c13)) | f(c11,f(c12,c14,c15),f(c13,c14,c15)) != f(c14,c15,f(c11,c12,c13)) # answer(dist_both). [copy(13),rewrite(5(20),5(20),5(28),5(28)),flip(b)]. 15 f(x,y,y) = y. [para(5(a,1),4(a,1))]. 16 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(8(a,1),5(a,2)),rewrite(6(2),5(3,R),6(3)),flip(a)]. 17 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(5(a,1),8(a,1,3)),rewrite(5(1,R),6(1))]. 18 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(8(a,1),8(a,1,3))]. 19 f(x,y,f(x,z,y)) = f(x,z,y). [para(15(a,1),8(a,1,3)),flip(a)]. 20 f(x,y,f(x,y,z)) = f(x,y,z). [para(15(a,1),8(a,1)),rewrite(6(3),19(3)),flip(a)]. 21 f(x,y,f(x,z,f(x,u,y))) = f(x,z,f(x,u,y)). [para(19(a,1),8(a,1,3)),flip(a)]. 22 f(x,y,f(x,z,f(x,y,u))) = f(x,z,f(x,y,u)). [para(19(a,1),8(a,2,3)),rewrite(6(1),6(4))]. 24 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(16(a,1),5(a,2)),rewrite(6(2),5(3,R),6(3))]. 25 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(5(a,1),16(a,1)),rewrite(5(2),5(2),6(3))]. 26 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))). [para(16(a,2),8(a,1,3))]. 28 f(x,f(y,z,u),f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(16(a,2),19(a,1,3))]. 29 f(x,y,f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(16(a,2),20(a,1,3))]. 30 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para(16(a,1),16(a,1,3)),rewrite(5(1,R),6(1),5(6,R),6(6))]. 32 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,z,u))). [para(17(a,2),8(a,1,3))]. 38 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,z,f(x,y,u))). [para(16(a,2),17(a,1,3)),flip(a)]. 40 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,y,v))). [para(18(a,1),5(a,2)),rewrite(6(3),5(5,R),6(5)),flip(a)]. 41 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(x,y,v))). [para(18(a,2),5(a,2)),rewrite(6(3),5(4,R),6(4))]. 52 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(18(a,1),16(a,1,3)),rewrite(5(2,R),6(2),5(8,R),6(8))]. 53 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(18(a,2),16(a,1,3)),rewrite(5(1,R),6(1),5(8,R),6(8))]. 54 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(16(a,2),18(a,1,3,3))]. 55 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(16(a,2),18(a,2,3,3)),flip(a)]. 57 f(x,f(x,y,z),f(x,u,v)) = f(x,y,f(x,u,f(x,v,z))). [para(18(a,1),17(a,1)),flip(a)]. 70 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,u,v))). [para(8(a,1),24(a,1,3)),rewrite(5(1,R),6(1),5(6,R),6(6))]. 73 f(x,y,f(z,x,f(x,y,u))) = f(z,x,f(x,y,u)). [para(19(a,1),24(a,1,3)),rewrite(5(1),5(3),5(5,R),6(5)),flip(a)]. 74 f(x,y,f(z,u,f(y,u,v))) = f(y,u,f(x,y,f(z,u,v))). [para(16(a,1),24(a,1,3)),rewrite(5(1,R),6(1),5(6,R),6(6))]. 75 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(y,z,f(x,z,u))). [para(24(a,1),17(a,1,3)),flip(a)]. 76 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,v,u))). [para(17(a,1),24(a,2,3)),rewrite(5(2,R),6(2),5(6,R),6(6)),flip(a)]. 78 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(18(a,1),24(a,1,3)),rewrite(5(2,R),6(2),5(8,R),6(8))]. 81 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(18(a,2),24(a,2,3)),rewrite(5(3,R),6(3),5(8,R),6(8)),flip(a)]. 95 f(x,y,f(x,z,f(y,u,f(x,y,v)))) = f(x,z,f(y,u,f(x,y,v))). [para(21(a,1),16(a,1,3)),rewrite(5(1),5(4),5(7,R),6(7)),flip(a)]. 102 f(x,y,f(z,x,f(y,u,f(x,y,v)))) = f(z,x,f(y,u,f(x,y,v))). [para(21(a,1),24(a,1,3)),rewrite(5(1),5(4),5(7,R),6(7)),flip(a)]. 103 f(x,y,f(y,z,f(x,u,f(x,y,v)))) = f(y,z,f(x,u,f(x,y,v))). [para(21(a,1),24(a,2,3)),rewrite(6(1),5(3,R),6(3),6(5),5(7,R),6(7))]. 113 f(x,y,f(y,z,f(y,u,v))) = f(x,y,f(y,v,f(y,z,u))). [para(17(a,1),29(a,2,3)),rewrite(29(4))]. 116 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(18(a,2),29(a,1,3,3))]. 122 f(x,y,f(z,y,f(x,y,u))) = f(z,y,f(x,y,u)). [para(73(a,1),5(a,2)),rewrite(5(1,R),6(1),6(3),5(4,R),6(4))]. 123 f(x,y,f(x,z,f(u,y,f(x,y,v)))) = f(x,z,f(u,y,f(x,y,v))). [para(73(a,1),16(a,1,3)),rewrite(5(1,R),6(1),5(4,R),6(4),5(7,R),6(7)),flip(a)]. 125 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,x,f(z,u,v))). [para(8(a,1),122(a,1,3,3)),rewrite(5(3,R),6(3),103(4),5(6,R),6(6))]. 131 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(8(a,1),26(a,1,3,3))]. 132 f(x,y,f(z,u,f(x,z,u))) = f(x,y,f(x,z,u)). [para(15(a,1),26(a,1,3)),rewrite(6(4),95(6)),flip(a)]. 133 f(x,f(y,z,u),f(y,z,f(y,x,u))) = f(y,z,f(y,x,u)). [para(15(a,1),26(a,1)),rewrite(5(1,R),6(1)