============================== Prover9 =============================== Prover9 (32) version 22-May-2007, May 2007. Process 28145 was started by mccune on cleo, Tue May 22 15:06:05 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(non_clause) # 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(non_clause) # 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(non_clause) # 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. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 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(hyper_resolution) -> set(pos_hyper_resolution). % 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): 30 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(17(a,1),5(a,2)),rewrite([6(2),5(3,R),6(3)]),flip(a)]. given #13 (T,wt=17): 31 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)). [para(17(a,1),6(a,2)),rewrite([6(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): 28 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): 25 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): 27 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),25(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): 29 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,u,f(x,y,f(x,v,z))). [para(17(a,1),8(a,2,3)),flip(a)]. given #26 (T,wt=24): 33 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 #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=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 #29 (T,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 #30 (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 #31 (T,wt=21): 474 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): 628 f(x,f(y,x,z),f(x,u,z)) = f(y,x,f(x,u,z)). [para(474(a,1),17(a,1)),rewrite([6(4)]),flip(a)]. given #33 (T,wt=20): 654 f(x,f(y,x,z),f(x,z,u)) = f(y,x,f(x,z,u)). [para(628(a,1),5(a,2)),rewrite([6(2),5(3),6(4)])]. given #34 (T,wt=20): 655 f(x,f(x,y,z),f(u,x,z)) = f(u,x,f(x,y,z)). [para(628(a,1),6(a,1)),flip(a)]. given #35 (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 #36 (T,wt=20): 695 f(x,f(x,y,z),f(u,x,y)) = f(u,x,f(x,y,z)). [para(654(a,1),6(a,1)),flip(a)]. given #37 (T,wt=18): 803 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [para(695(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),696(6),28(5),6(3),57(6),6(4),20(5),22(5)]),flip(a)]. given #38 (T,wt=17): 828 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(30(a,2),803(a,2)),rewrite([6(3),392(5),6(4),820(5)])]. given #39 (T,wt=17): 874 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(828(a,1),5(a,2)),rewrite([6(2),5(3)]),flip(a)]. given #40 (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 #41 (T,wt=17): 897 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(874(a,1),5(a,2)),rewrite([6(2),5(3)])]. given #42 (T,wt=17): 922 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(874(a,2),38(a,2)),rewrite([6(2),392(3),813(3)]),flip(a)]. given #43 (T,wt=17): 933 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(874(a,2),803(a,2)),rewrite([6(3),826(5)]),flip(a)]. given #44 (T,wt=17): 1057 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(38(a,2),897(a,2)),rewrite([5(1,R),6(1),5(2,R),6(2),696(4),28(3),6(1),803(3),6(2),5(3,R),6(3),5(4),20(4)]),flip(a)]. given #45 (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 #46 (T,wt=17): 1071 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(5(a,1),922(a,1,2)),rewrite([5(2),5(4)])]. given #47 (T,wt=17): 1073 f(x,f(y,z,x),f(y,z,u)) = f(y,z,x). [para(922(a,1),6(a,1)),flip(a)]. given #48 (T,wt=17): 1074 f(x,f(x,y,z),f(y,z,u)) = f(x,y,z). [para(922(a,1),6(a,2)),rewrite([5(1),5(4)])]. given #49 (T,wt=17): 1149 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(933(a,1),5(a,2)),rewrite([6(2),5(3)])]. given #50 (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 #51 (T,wt=17): 1181 f(x,f(y,x,z),f(y,z,u)) = f(y,x,z). [para(1057(a,1),6(a,1)),flip(a)]. given #52 (T,wt=17): 1253 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(1071(a,1),5(a,2)),rewrite([5(2),5(2),5(3),5(4),5(4)])]. given #53 (T,wt=17): 1469 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(1149(a,1),803(a,2)),rewrite([6(3),1063(5)])]. given #54 (T,wt=18): 812 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para(803(a,1),5(a,2)),rewrite([5(1,R),6(1),6(3),5(4)])]. given #55 (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 #56 (T,wt=18): 813 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para(5(a,1),803(a,1,3,3)),rewrite([5(1),6(1),6(4)])]. given #57 (T,wt=18): 827 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [para(30(a,2),803(a,1,3)),rewrite([6(1),6(4)])]. given #58 (T,wt=18): 866 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [back_rewrite(360),rewrite([5(2),392(3),813(3),5(2,R),6(2),5(3,R),6(3)]),flip(a)]. given #59 (T,wt=18): 868 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [back_rewrite(239),rewrite([6(1),827(3),5(3,R),6(3)]),flip(a)]. given #60 (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 #61 (T,wt=18): 871 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [back_rewrite(385),rewrite([827(4)]),flip(a)]. given #62 (T,wt=18): 910 f(x,y,f(z,u,f(x,z,y))) = f(x,z,y). [para(874(a,2),25(a,2,3)),rewrite([5(2,R),6(2),812(3),6(2)]),flip(a)]. given #63 (T,wt=18): 1030 f(x,y,f(z,u,f(x,u,y))) = f(x,u,y). [para(20(a,1),897(a,1,3)),rewrite([15(3),696(5),122(4)]),flip(a)]. given #64 (T,wt=18): 1051 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u). [para(897(a,1),29(a,2,3)),rewrite([6(1),6(4),5(5,R),6(5),910(6)])]. given #65 (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 #66 (T,wt=18): 1072 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(5(a,2),922(a,1,2)),rewrite([5(2),6(2),392(3),5(4),6(4)])]. given #67 (T,wt=18): 1634 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(1071(a,1),812(a,2)),rewrite([6(5),1607(7),6(2)])]. given #68 (T,wt=18): 1669 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y). [para(827(a,1),19(a,1,3)),rewrite([6(1),6(3),6(4),696(4),28(3),6(4),910(6)])]. given #69 (T,wt=18): 1713 f(x,y,f(z,u,f(z,x,y))) = f(z,x,y). [para(827(a,1),922(a,2)),rewrite([5(1),5(4),922(7),5(4)])]. given #70 (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 #71 (T,wt=18): 1982 f(x,y,f(z,u,f(u,x,y))) = f(u,x,y). [para(1030(a,1),922(a,2)),rewrite([5(1,R),6(1),5(4,R),6(4),922(7),5(4,R),6(4)])]. given #72 (T,wt=20): 1076 f(f(x,y,z),f(x,z,u),f(x,y,z)) = f(x,y,z). [para(19(a,1),922(a,1,3)),rewrite([19(6)])]. given #73 (T,wt=20): 1077 f(f(x,y,z),f(x,y,u),f(x,y,z)) = f(x,y,z). [para(20(a,1),922(a,1,3)),rewrite([20(6)])]. given #74 (T,wt=20): 1101 f(f(x,y,z),f(y,z,u),f(x,y,z)) = f(x,y,z). [para(205(a,1),922(a,1,3)),rewrite([205(6)])]. given #75 (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 #76 (T,wt=21): 914 f(x,f(y,x,z),f(z,u,f(y,x,z))) = f(y,x,z). [para(205(a,1),874(a,1,3)),rewrite([5(3,R),15(3),6(4)]),flip(a)]. given #77 (T,wt=21): 1048 f(x,f(y,x,z),f(u,z,f(y,x,z))) = f(y,x,z). [para(205(a,1),897(a,1,3)),rewrite([15(3)]),flip(a)]. given #78 (T,wt=21): 1050 f(x,y,f(x,f(x,y,z),f(u,y,z))) = f(x,y,z). [para(897(a,1),29(a,1)),rewrite([20(3),15(3)]),flip(a)]. given #79 (T,wt=21): 1079 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(16(a,1),922(a,1,2)),rewrite([5(3),5(5)])]. given #80 (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 #81 (T,wt=21): 1088 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(30(a,1),922(a,1,2)),rewrite([5(3),5(5)])]. given #82 (T,wt=21): 1150 f(x,f(y,z,x),f(y,u,f(y,z,x))) = f(y,z,x). [para(19(a,1),933(a,1,3)),rewrite([5(3,R),15(3),6(4)]),flip(a)]. given #83 (T,wt=17): 3270 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x). [para(1050(a,1),1150(a,1,3)),rewrite([5(2),5(2),5(5),5(5),6(6),1332(6),4(4),5(2),5(2)]),flip(a)]. given #84 (T,wt=17): 3273 f(x,f(x,y,z),f(u,y,z)) = f(x,y,z). [para(3270(a,1),19(a,1,3)),rewrite([5(2),1071(3),5(2)]),flip(a)]. given #85 (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 #86 (T,wt=21): 1151 f(x,f(y,x,z),f(y,u,f(y,x,z))) = f(y,x,z). [para(20(a,1),933(a,1,3)),rewrite([5(3,R),15(3),6(4)]),flip(a)]. given #87 (T,wt=21): 1159 f(x,f(y,z,x),f(z,u,f(y,z,x))) = f(y,z,x). [para(205(a,1),933(a,1,3)),rewrite([5(3,R),15(3),6(4)]),flip(a)]. given #88 (T,wt=21): 1349 f(x,f(x,y,z),f(y,u,f(y,z,v))) = f(x,y,z). [para(8(a,1),1073(a,1,3)),rewrite([5(1),5(5)])]. given #89 (T,wt=21): 1435 f(x,f(y,z,x),f(u,y,f(y,z,x))) = f(y,z,x). [para(19(a,1),1149(a,1,3)),rewrite([15(3)]),flip(a)]. given #90 (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 #91 (T,wt=21): 1436 f(x,f(y,x,z),f(u,y,f(y,x,z))) = f(y,x,z). [para(20(a,1),1149(a,1,3)),rewrite([15(3)]),flip(a)]. given #92 (T,wt=21): 1447 f(x,f(y,z,x),f(u,z,f(y,z,x))) = f(y,z,x). [para(205(a,1),1149(a,1,3)),rewrite([15(3)]),flip(a)]. given #93 (T,wt=21): 2830 f(x,y,f(x,f(x,y,z),f(y,u,z))) = f(x,y,z). [para(5(a,1),1050(a,1,3)),rewrite([5(1,R),6(1),5(3,R)])]. given #94 (T,wt=21): 2861 f(x,f(y,z,f(z,u,v)),f(z,u,x)) = f(z,u,x). [para(1079(a,1),5(a,2)),rewrite([5(3),5(3),5(4),5(5),5(5)])]. given #95 (A,wt=31): 60 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 #96 (T,wt=21): 2884 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(1079(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 #97 (T,wt=21): 2885 f(x,f(y,z,f(u,z,v)),f(x,u,z)) = f(x,u,z). [para(1079(a,1),21(a,2)),rewrite([5(1,R),6(1),6(3),22(5),6(5)])]. given #98 (T,wt=21): 3114 f(x,f(y,z,f(z,u,v)),f(z,v,x)) = f(z,v,x). [para(1088(a,1),5(a,2)),rewrite([5(3),5(3),5(4),5(5),5(5)])]. given #99 (T,wt=21): 3475 f(x,f(y,x,z),f(y,x,f(y,z,u))) = f(y,x,z). [para(1349(a,1),122(a,1,3)),rewrite([5(1,R),6(1),5(2,R),6(2),15(3),5(2,R),6(2),5(3,R),6(3),57(5),6(3),20(4)]),flip(a)]. given #100 (A,wt=24): 61 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 #101 (T,wt=21): 3521 f(x,f(y,z,x),f(y,u,f(y,z,v))) = f(y,z,x). [para(1349(a,1),1253(a,2)),rewrite([5(3),5(3),5(5),5(5),1253(9),5(5),5(5)])]. given #102 (T,wt=21): 3627 f(x,f(y,z,f(y,u,v)),f(y,u,x)) = f(y,u,x). [para(2861(a,1),5(a,1)),rewrite([5(4,R),6(4),5(5,R)]),flip(a)]. given #103 (T,wt=21): 3998 f(x,y,f(y,z,f(x,u,y))) = f(x,y,f(u,y,z)). [para(474(a,1),3475(a,1,2)),rewrite([5(1),5(3),6(5),5(6,R),6(6),2997(7),6(5),1938(5),20(3),20(3),5(3),5(5,R),6(5)]),flip(a)]. given #104 (T,wt=22): 816 f(x,y,f(x,z,f(z,u,f(y,z,v)))) = f(x,y,z). [para(8(a,1),803(a,1,3,3)),rewrite([5(1,R),6(1),6(5)])]. given #105 (A,wt=31): 62 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 #106 (T,wt=21): 4305 f(x,y,f(z,f(y,z,u),f(x,z,v))) = f(x,y,z). [para(30(a,2),816(a,1,3))]. given #107 (T,wt=21): 4461 f(x,y,f(z,f(x,z,u),f(z,y,v))) = f(x,z,y). [para(4305(a,1),5(a,2)),rewrite([5(2,R),6(2),6(4),5(5),5(5)])]. given #108 (T,wt=21): 4462 f(x,y,f(z,f(z,y,u),f(x,z,v))) = f(x,z,y). [para(4305(a,1),6(a,2)),rewrite([5(1,R),6(1),6(4),6(5)])]. given #109 (T,wt=21): 4463 f(x,y,f(z,f(x,z,u),f(y,z,v))) = f(x,y,z). [para(6(a,1),4305(a,1,3))]. given #110 (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 #111 (T,wt=22): 819 f(x,y,f(x,z,f(y,u,f(y,z,v)))) = f(x,y,z). [para(16(a,2),803(a,1,3,3)),rewrite([5(1,R),6(1),6(5)])]. given #112 (T,wt=22): 853 f(x,y,f(z,u,f(x,z,f(y,z,v)))) = f(x,y,z). [para(40(a,2),803(a,1,3)),rewrite([5(1,R),6(1),6(5)])]. given #113 (T,wt=22): 859 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [para(41(a,1),803(a,1,3)),rewrite([5(3,R),6(3),6(5)])]. given #114 (T,wt=22): 1082 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [para(17(a,2),922(a,1,2)),rewrite([5(3),392(4),5(5)])]. given #115 (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 #116 (T,wt=22): 1606 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z). [para(8(a,1),812(a,1,3,3))]. given #117 (T,wt=22): 1726 f(x,y,f(z,u,f(y,z,f(x,z,v)))) = f(x,y,z). [para(18(a,1),866(a,1,3)),rewrite([5(1,R),6(1),5(2,R),6(2),5(5),5(5)])]. given #118 (T,wt=22): 1738 f(x,y,f(z,u,f(y,u,f(x,u,v)))) = f(x,y,u). [para(41(a,2),866(a,1,3)),rewrite([5(1,R),6(1),5(2,R),6(2),5(5),5(5)])]. given #119 (T,wt=22): 1775 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),812(4),5(4,R),6(4),5(5,R),6(5)]),flip(a)]. given #120 (A,wt=38): 65 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 #121 (T,wt=22): 1856 f(x,y,f(z,x,f(y,u,f(z,y,v)))) = f(z,x,y). [para(52(a,1),874(a,2)),rewrite([5(3),392(4),813(4),5(2,R),6(2),5(4,R),6(4)]),flip(a)]. given #122 (T,wt=21): 5467 f(x,f(y,z,f(u,y,v)),f(u,x,y)) = f(u,x,y). [para(1856(a,1),828(a,1)),flip(a)]. given #123 (T,wt=21): 5512 f(x,f(y,x,z),f(z,u,f(y,z,v))) = f(y,x,z). [para(5467(a,1),6(a,1)),flip(a)]. given #124 (T,wt=22): 1905 f(x,y,f(z,u,f(x,u,f(y,u,v)))) = f(x,y,u). [para(41(a,2),871(a,1,3)),rewrite([5(1,R),6(1),5(2,R),6(2),5(5),5(5)])]. given #125 (A,wt=31): 66 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 #126 (T,wt=22): 2013 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([813(4)]),flip(a)]. given #127 (T,wt=22): 2026 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),868(4),20(2),5(2,R),6(2),5(5,R),6(5)]),flip(a)]. given #128 (T,wt=21): 5800 f(x,f(y,z,f(y,u,v)),f(y,x,u)) = f(y,x,u). [para(2026(a,1),828(a,1)),flip(a)]. given #129 (T,wt=21): 5854 f(x,f(y,x,z),f(y,u,f(y,z,v))) = f(y,x,z). [para(5800(a,1),6(a,1)),flip(a)]. given #130 (A,wt=38): 67 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 #131 (T,wt=22): 2870 f(x,y,f(x,z,f(z,u,f(z,y,v)))) = f(x,z,y). [para(1079(a,1),17(a,1)),rewrite([5(3,R),6(3),6(4)]),flip(a)]. given #132 (T,wt=22): 2966 f(x,y,f(x,z,f(u,y,f(y,z,v)))) = f(x,y,z). [para(1079(a,1),812(a,2)),rewrite([6(7),1607(9),6(3)])]. given #133 (T,wt=22): 3164 f(x,y,f(x,z,f(u,y,f(y,v,z)))) = f(x,y,z). [para(1088(a,1),812(a,2)),rewrite([6(7),1607(9),6(3)])]. given #134 (T,wt=22): 3678 f(x,y,f(z,y,f(z,u,f(z,x,v)))) = f(z,x,y). [para(2861(a,1),933(a,1)),rewrite([5(3,R),6(3)]),flip(a)]. given #135 (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 #136 (T,wt=22): 3815 f(x,y,f(x,z,f(y,u,f(z,y,v)))) = f(x,z,y). [para(2884(a,1),17(a,1)),rewrite([6(4)]),flip(a)]. given #137 (T,wt=22): 3937 f(x,y,f(x,z,f(u,z,f(y,z,v)))) = f(x,y,z). [para(2885(a,1),8(a,2)),rewrite([6(3)])]. given #138 (T,wt=22): 4085 f(x,y,f(z,u,f(z,v,f(x,y,z)))) = f(x,y,z). [para(61(a,1),866(a,1,3)),rewrite([5(1),6(1),5(5),5(5)])]. given #139 (T,wt=21): 6221 f(x,y,f(z,f(x,y,z),f(z,u,v))) = f(x,y,z). [para(17(a,1),4085(a,1,3))]. given #140 (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 #141 (T,wt=21): 6311 f(x,y,f(z,f(x,z,y),f(z,u,v))) = f(x,z,y). [para(6221(a,1),5(a,2)),rewrite([5(1),5(1),6(4),5(5),5(5)])]. given #142 (T,wt=22): 4557 f(x,y,f(z,u,f(x,z,f(z,y,v)))) = f(x,z,y). [para(2884(a,1),4305(a,2)),rewrite([5(1,R),6(1),6(3),5(4,R),6(4),6(6),5(7),6(8),6(9),4491(11),6(5)])]. given #143 (T,wt=22): 4872 f(x,y,f(z,u,f(z,y,f(x,z,v)))) = f(x,z,y). [para(853(a,1),5(a,2)),rewrite([5(2,R),6(2),6(4),5(5),5(5)])]. given #144 (T,wt=22): 4906 f(x,y,f(z,u,f(z,x,f(z,y,v)))) = f(z,x,y). [para(853(a,1),922(a,2)),rewrite([5(1,R),6(1),5(2,R),6(2),5(5,R),6(5),5(6,R),6(6),922(9),5(5)])]. given #145 (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 #146 (T,wt=20): 6720 f(x,f(y,x,z),f(y,x,u)) = f(y,x,f(x,u,z)). [para(70(a,1),17(a,1)),rewrite([5(2,R),6(2),20(3),5(4,R),6(4)]),flip(a)]. given #147 (T,wt=20): 6802 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)). [para(1253(a,1),70(a,2,3)),rewrite([5(3),6(3),910(5),5(4),5(5,R)]),flip(a)]. given #148 (T,wt=21): 6861 f(x,f(x,y,z),f(u,y,f(y,z,v))) = f(x,y,z). [para(1079(a,1),70(a,2,3)),rewrite([5(5),5(5),2966(6),1079(4),5(5,R)]),flip(a)]. given #149 (T,wt=21): 6870 f(x,f(x,y,z),f(u,y,f(y,v,z))) = f(x,y,z). [para(1088(a,1),70(a,2,3)),rewrite([5(5),5(5),3164(6),1088(4),5(5,R)]),flip(a)]. given #150 (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 #151 (T,wt=17): 7121 f(x,f(x,y,z),f(y,u,z)) = f(x,y,z). [para(6870(a,1),1669(a,1,3)),rewrite([392(3),1072(3)]),flip(a)]. given #152 (T,wt=17): 7301 f(x,f(y,z,x),f(y,u,z)) = f(y,z,x). [para(7121(a,1),1253(a,2)),rewrite([5(2),5(2),5(4),5(4),1253(7),5(4),5(4)])]. given #153 (T,wt=21): 7078 f(x,f(y,z,x),f(u,y,f(y,z,v))) = f(y,z,x). [para(6861(a,1),922(a,1,3)),rewrite([5(3),5(3),6(4),5(5),5(5),6(6),2954(6),5(2),5(2)]),flip(a)]. given #154 (T,wt=21): 7113 f(x,f(y,z,x),f(u,y,f(y,v,z))) = f(y,z,x). [para(6870(a,1),922(a,1,3)),rewrite([5(3),5(3),6(4),5(5),5(5),6(6),3158(6),5(2),5(2)]),flip(a)]. given #155 (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 #156 (T,wt=21): 7177 f(x,y,f(y,f(x,y,z),f(u,x,z))) = f(x,y,z). [para(71(a,1),1469(a,2)),rewrite([20(3),15(3),5(3,R),6(3)]),flip(a)]. given #157 (T,wt=18): 7553 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(6(a,1),7177(a,1,3)),rewrite([5(1,R),6(1),28(4),6(2)])]. given #158 (T,wt=21): 7552 f(x,y,f(y,f(x,y,z),f(x,u,z))) = f(x,y,z). [para(5(a,1),7177(a,1,3)),rewrite([5(1,R),6(1),5(3,R)])]. given #159 (T,wt=22): 5283 f(x,y,f(z,u,f(x,u,f(u,y,v)))) = f(x,u,y). [para(1738(a,1),5(a,2)),rewrite([5(1,R),6(1),6(4),5(5),5(5)])]. given #160 (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 #161 (T,wt=20): 7772 f(x,f(y,z,x),f(z,x,u)) = f(y,x,f(z,x,u)). [para(922(a,1),74(a,2,3)),rewrite([5(3),6(3),122(4),19(4),5(4),5(5,R)]),flip(a)]. given #162 (T,wt=20): 7788 f(x,f(y,z,x),f(u,z,x)) = f(y,x,f(u,z,x)). [para(1253(a,1),74(a,2,3)),rewrite([5(3),6(3),1030(5),5(4),5(5,R)]),flip(a)]. given #163 (T,wt=20): 7955 f(x,f(y,x,z),f(u,y,x)) = f(u,x,f(y,x,z)). [para(7772(a,1),205(a,1,3)),rewrite([1604(5),7772(6)])]. given #164 (T,wt=22): 5284 f(x,y,f(z,u,f(u,y,f(x,u,v)))) = f(x,u,y). [para(1738(a,1),6(a,2)),rewrite([5(2,R),6(2),6(4),6(5)])]. given #165 (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 #166 (T,wt=22): 5305 f(x,y,f(z,u,f(u,v,f(x,y,u)))) = f(x,y,u). [para(874(a,2),1738(a,1,3,3)),rewrite([5(1,R),6(1)])]. given #167 (T,wt=22): 5310 f(x,y,f(z,u,f(u,x,f(u,y,v)))) = f(u,x,y). [para(1738(a,1),922(a,2)),rewrite([5(1,R),6(1),5(2,R),6(2),5(4,R),6(4),5(5,R),6(5),5(6,R),6(6),5(8,R),6(8),922(9),5(5),6(5)])]. given #168 (T,wt=22): 5647 f(x,y,f(x,z,f(u,y,f(z,y,v)))) = f(x,z,y). [para(1905(a,1),812(a,2)),rewrite([6(7),1618(9)])]. given #169 (T,wt=21): 8713 f(x,y,f(y,z,f(u,x,y))) = f(y,z,f(u,x,y)). [para(1253(a,1),5647(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 #170 (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 #171 (T,wt=21): 8825 f(x,y,f(z,f(x,y,z),f(x,z,u))) = f(x,y,z). [para(827(a,1),76(a,2,3)),rewrite([5(2,R),6(2),5(6,R),6(6),19(6)])]. given #172 (T,wt=22): 5663 f(x,y,f(z,y,f(u,x,f(z,x,v)))) = f(z,x,y). [para(1905(a,1),1856(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),5453(13),5(5),5(5)])]. given #173 (T,wt=22): 5748 f(x,y,f(z,y,f(z,u,f(x,z,v)))) = f(x,z,y). [para(2013(a,1),24(a,1)),flip(a)]. given #174 (T,wt=22): 6205 f(x,y,f(x,z,f(u,z,f(z,y,v)))) = f(x,z,y). [para(3937(a,1),21(a,1,3)),rewrite([5(1,R),6(1),6(3),1079(4),5(2,R),6(2)]),flip(a)]. given #175 (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 #176 (T,wt=22): 6213 f(x,y,f(z,u,f(z,v,f(x,z,y)))) = f(x,z,y). [para(4085(a,1),5(a,2)),rewrite([5(1),5(1),6(4),5(5),5(5)])]. given #177 (T,wt=22): 6261 f(x,y,f(z,u,f(z,v,f(z,x,y)))) = f(z,x,y). [para(4085(a,1),922(a,2)),rewrite([5(1),5(5),922(9),5(5)])]. given #178 (T,wt=22): 7757 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([813(4)]),flip(a)]. given #179 (T,wt=22): 7949 f(x,y,f(z,x,f(u,y,f(z,y,v)))) = f(z,x,y). [back_rewrite(5339),rewrite([7900(10)])]. given #180 (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 #181 (T,wt=22): 8635 f(x,y,f(z,u,f(x,u,f(u,v,y)))) = f(x,u,y). [back_rewrite(4361),rewrite([8369(11)])]. given #182 (T,wt=22): 8636 f(x,y,f(z,u,f(u,v,f(x,u,y)))) = f(x,u,y). [para(5305(a,1),5(a,2)),rewrite([5(1),5(1),6(4),5(5),5(5)])]. given #183 (T,wt=22): 8653 f(x,y,f(z,u,f(u,v,f(u,x,y)))) = f(u,x,y). [para(5305(a,1),922(a,2)),rewrite([5(1),5(5),922(9),5(5)])]. given #184 (T,wt=22): 8746 f(x,y,f(y,z,f(u,z,f(x,z,v)))) = f(x,y,z). [para(2861(a,1),8713(a,2)),rewrite([5(1,R),6(1),5(3),5(3),28(5),6(3),5(5),5(5)])]. given #185 (A,wt=31): 79 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 #186 (T,wt=22): 9577 f(x,y,f(z,u,f(u,x,f(u,v,y)))) = f(u,x,y). [para(8635(a,1),922(a,2)),rewrite([5(2,R),6(2),5(6,R),6(6),922(9),5(5,R),6(5)])]. given #187 (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(30(a,2),8(a,2,3)),flip(a)]. given #188 (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(30(a,2),19(a,1,3))]. given #189 (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(30(a,2),24(a,2,3)),rewrite([5(2,R),6(2),5(6,R),6(6)])]. given #190 (A,wt=31): 80 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): 10204 f(x,f(y,z,f(u,y,v)),f(u,y,x)) = f(u,y,x). [para(80(a,1),828(a,1)),rewrite([5(3,R),6(3),813(4),5(4)]),flip(a)]. given #192 (T,wt=21): 10352 f(x,f(y,z,x),f(z,u,f(y,z,v))) = f(y,z,x). [para(10204(a,1),6(a,1)),flip(a)]. given #193 (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 #194 (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 #195 (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)]. given #196 (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 #197 (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 #198 (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 #199 (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(30(a,2),21(a,2,3)),rewrite([21(5)]),flip(a)]. given #200 (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(30(a,2),18(a,2,3,3)),flip(a)]. Low Water (keep, True_semantics): wt=50 given #201 (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),28(a,2,3)),rewrite([28(4)])]. given #202 (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),28(a,2,3)),rewrite([28(4)]),flip(a)]. given #203 (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),28(a,2,3)),rewrite([28(4)])]. given #204 (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(30(a,2),28(a,2,3)),rewrite([28(4)]),flip(a)]. given #205 (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),30(a,2,3)),rewrite([5(3,R),6(3),57(4),6(5),5(8,R),6(8)]),flip(a)]. Low Water (keep, True_semantics): wt=48 given #206 (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 #207 (T,wt=18): 12288 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z). [para(125(a,1),1469(a,2)),rewrite([20(3),15(3),5(3,R),6(3),6720(5),6(3)]),flip(a)]. given #208 (T,wt=18): 12377 f(x,y,f(x,z,f(u,z,y))) = f(x,z,y). [para(12288(a,1),474(a,2)),rewrite([5(3,R),6(3),21(5),5(4,R),6(4)])]. given #209 (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(25(a,1),5(a,2)),rewrite([5(1,R),6(1),6(3),5(5,R),6(5),5(6,R),6(6)])]. given #210 (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 #211 (T,wt=24): 168 f(x,f(y,z,u),f(y,z,f(y,u,x))) = f(y,x,f(y,z,u)). [para(27(a,1),5(a,2)),rewrite([5(2),5(2),5(4),5(6,R),6(6)])]. given #212 (T,wt=17): 12860 f(x,f(y,z,u),f(y,u,x)) = f(y,u,x). [para(1072(a,1),168(a,1,3)),rewrite([5(2),5(2),5(3),5(3),15(4),5(3),5(3)]),flip(a)]. given #213 (T,wt=20): 13017 f(x,f(y,z,x),f(z,u,x)) = f(y,x,f(z,u,x)). [para(12860(a,1),74(a,2,3)),rewrite([5(3),6(3),1030(5),5(4),5(5,R)]),flip(a)]. given #214 (T,wt=20): 13058 f(x,f(y,x,z),f(y,u,x)) = f(x,z,f(y,u,x)). [para(13017(a,1),922(a,2)),rewrite([5(2),5(2),6(3),5(4),5(4),12860(7),5(5,R),6(5)])]. given #215 (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)])]. Low Water (keep, True_semantics): wt=47 given #216 (T,wt=21): 12886 f(x,f(y,z,f(y,u,v)),f(y,v,x)) = f(y,v,x). [para(1082(a,1),168(a,1,3)),rewrite([5(3),5(3),5(4),5(4),15(5),5(4),5(4)]),flip(a)]. given #217 (T,wt=22): 13299 f(x,y,f(z,u,f(x,z,f(z,v,y)))) = f(x,z,y). [para(12886(a,1),1072(a,2)),rewrite([5(3),5(6),5(7,R),12377(9),12388(4),5(5)])]. given #218 (T,wt=22): 13374 f(x,y,f(z,u,f(z,x,f(z,v,y)))) = f(z,x,y). [para(13299(a,1),922(a,2)),rewrite([5(2,R),6(2),5(6,R),6(6),922(9),5(5,R),6(5)])]. given #219 (T,wt=24): 169 f(x,f(y,z,u),f(z,u,f(x,y,z))) = f(x,z,f(y,z,u)). [para(5(a,1),27(a,1,2)),rewrite([6(2),5(5)])]. given #220 (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)]. given #221 (T,wt=20): 13411 f(x,f(y,z,x),f(u,y,x)) = f(u,x,f(y,z,x)). [para(19(a,1),169(a,1,2)),rewrite([7298(5),19(5)])]. given #222 (T,wt=20): 13645 f(x,f(y,z,x),f(y,x,u)) = f(x,u,f(y,z,x)). [para(13411(a,1),5(a,2)),rewrite([5(2),5(2),5(3),5(5,R),6(5)])]. given #223 (T,wt=24): 170 f(x,f(y,z,u),f(y,u,f(x,z,u))) = f(x,u,f(y,z,u)). [para(5(a,2),27(a,1,2)),rewrite([6(2),5(3,R),6(3),5(5),5(5)])]. given #224 (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 #225 (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))]. Low Water (keep, True_semantics): wt=46 given #226 (T,wt=22): 14064 f(x,y,f(x,z,f(z,u,f(z,v,y)))) = f(x,z,y). [para(13299(a,1),96(a,1,3)),rewrite([392(4),1082(4)]),flip(a)]. 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(25(a,1),205(a,1,3)),rewrite([5(1,R),6(1),5(4,R),6(4),5(5,R),6(5),176(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(29(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): 262 f(x,y,f(z,u,f(u,y,v))) = f(x,y,f(u,y,f(z,u,v))). [para(29(a,1),205(a,1,3)),rewrite([5(1,R),6(1),5(4,R),6(4),5(5,R),6(5),187(6),5(4,R),6(4),5(6,R),6(6)]),flip(a)]. given #230 (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 #231 (T,wt=24): 298 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,v,y))). [para(33(a,1),5(a,2)),rewrite([6(3),5(5,R),6(5)]),flip(a)]. given #232 (T,wt=24): 318 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 #233 (T,wt=20): 14579 f(f(x,y,z),f(z,u,v),f(x,y,z)) = f(x,y,z). [para(1073(a,1),318(a,1,3)),rewrite([9279(10)])]. given #234 (T,wt=20): 14587 f(f(x,y,z),f(y,u,v),f(x,y,z)) = f(x,y,z). [para(1181(a,1),318(a,1,3)),rewrite([9281(10)])]. given #235 (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 #236 (T,wt=20): 14739 f(f(x,y,z),f(x,u,v),f(x,y,z)) = f(x,y,z). [para(318(a,1),216(a,2)),rewrite([6(4),4(6),19(5),20(5)]),flip(a)]. given #237 (T,wt=24): 319 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 #238 (T,wt=17): 15126 f(x,f(y,x,z),f(u,y,z)) = f(y,x,z). [para(319(a,2),8713(a,1,3)),rewrite([5(2,R),6(2),5(4),5(4),20(4),7293(5),5(6,R),6(6),5(7,R),6(7),3946(7),1982(6)])]. given #239 (T,wt=17): 15127 f(x,f(y,z,u),f(z,x,u)) = f(z,x,u). [para(319(a,2),8713(a,2)),rewrite([5(4,R),6(4),5(5,R),6(5),3946(5),1982(4),15(3),5(2,R),6(2),5(4),5(4),20(4)]),flip(a)]. given #240 (A,wt=31): 100 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 #241 (T,wt=18): 15203 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y). [back_rewrite(5760),rewrite([15103(9)])]. given #242 (T,wt=20): 15075 f(f(x,y,z),f(u,v,w),f(x,y,z)) = f(x,y,z). [para(319(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 #243 (T,wt=22): 15202 f(x,y,f(z,u,f(z,y,f(z,v,x)))) = f(z,x,y). [back_rewrite(13295),rewrite([15067(9),6(2)])]. given #244 (T,wt=17): 15690 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(15202(a,1),922(a,1,2)),rewrite([5(2),5(4)])]. given #245 (A,wt=31): 101 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): 15715 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(15202(a,1),2885(a,1,2))]. given #247 (T,wt=17): 15740 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(15202(a,1),5467(a,1,2)),rewrite([5(2,R),6(2),5(4,R),6(4)])]. given #248 (T,wt=21): 15713 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(15202(a,1),2861(a,1,2,3)),rewrite([5(1,R),6(1),5(3),5(5)])]. given #249 (T,wt=21): 15719 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(15202(a,1),3627(a,1,2,3)),rewrite([5(1,R),6(1),5(3),5(5)])]. given #250 (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 #251 (T,wt=21): 15848 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(2861(a,1),15690(a,2)),rewrite([5(3),5(7),15690(9),5(5)])]. given #252 (T,wt=21): 15854 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(3627(a,1),15690(a,2)),rewrite([5(3),5(7),15690(9),5(5)])]. given #253 (T,wt=24): 321 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 #254 (T,wt=17): 16415 f(x,f(y,z,u),f(y,x,u)) = f(y,x,u). [para(321(a,2),30(a,2)),rewrite([5(2,R),6(2),15715(3),5(3)]),flip(a)]. given #255 (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 #256 (T,wt=21): 16396 f(x,y,f(z,y,f(x,u,y))) = f(x,y,f(z,u,y)). [para(15(a,1),321(a,1,3)),rewrite([6(2)]),flip(a)]. given #257 (T,wt=24): 436 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 #258 (T,wt=24): 471 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 #259 (T,wt=24): 478 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 #260 (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 #261 (T,wt=22): 17521 f(x,y,f(x,z,f(u,z,f(z,v,y)))) = f(x,z,y). [para(8635(a,1),104(a,1,3)),rewrite([15713(4)]),flip(a)]. given #262 (T,wt=24): 479 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 #263 (T,wt=24): 482 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 #264 (T,wt=24): 495 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 #265 (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(30(a,2),21(a,1,3,3))]. given #266 (T,wt=24): 630 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,v,f(z,x,u))). [para(474(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 #267 (T,wt=22): 18288 f(x,y,f(z,u,f(y,u,f(x,z,u)))) = f(x,y,u). [para(630(a,1),9577(a,1,3)),rewrite([5(1),6(1),5(2,R),6(2),5(5),5(5)])]. given #268 (T,wt=18): 18382 f(x,y,f(z,y,f(x,u,z))) = f(x,z,y). [para(18288(a,1),6(a,2)),rewrite([5(2,R),6(2),8713(3),6(3),6(4)])]. given #269 (T,wt=18): 18417 f(x,y,f(z,y,f(z,u,x))) = f(z,x,y). [para(18288(a,1),4461(a,2)),rewrite([5(2,R),6(2),8713(3),5(5,R),6(5),8713(6),6(6),4572(8),6(4)])]. given #270 (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),28(a,1,3,3))]. given #271 (T,wt=24): 738 f(x,y,f(z,u,f(x,z,v))) = f(x,y,f(z,v,f(x,z,u))). [para(474(a,1),655(a,1,3)),rewrite([5(1),6(1),5(4),5(5,R),6(5),6(6),653(6),5(4),6(4),5(7,R),6(7),95(7)])]. given #272 (T,wt=24): 847 f(x,f(y,z,u),f(x,v,f(x,y,z))) = f(x,v,f(x,y,z)). [para(803(a,1),33(a,1,3)),rewrite([6(4)]),flip(a)]. given #273 (T,wt=24): 854 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(z,x,f(x,y,v))). [para(40(a,2),803(a,2)),rewrite([6(5),392(7),6(6),820(7)])]. given #274 (T,wt=24): 860 f(x,y,f(z,x,f(x,u,v))) = f(x,y,f(x,u,f(z,x,v))). [para(41(a,1),803(a,2)),rewrite([6(5),392(7),6(6),820(7)])]. given #275 (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(28(a,1),18(a,1,3,3)),flip(a)]. given #276 (T,wt=24): 872 f(x,y,f(x,f(z,y,u),f(x,v,z))) = f(x,v,f(x,z,y)). [back_rewrite(411),rewrite([866(3)]),flip(a)]. Low Water (keep, True_semantics): wt=44 given #277 (T,wt=21): 19083 f(x,f(y,z,f(u,v,y)),f(x,u,y)) = f(x,u,y). [para(1072(a,1),872(a,2)),rewrite([6(3),2175(6)])]. given #278 (T,wt=21): 19086 f(x,f(y,z,f(u,v,y)),f(x,v,y)) = f(x,v,y). [para(1634(a,1),872(a,2)),rewrite([6(3),1254(6)])]. given #279 (T,wt=21): 19329 f(x,f(y,z,f(u,v,z)),f(x,v,z)) = f(x,v,z). [para(5(a,2),19086(a,1,2)),rewrite([6(2)])]. given #280 (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(28(a,1),18(a,2,3,3)),rewrite([95(4)])]. given #281 (T,wt=24): 905 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(x,z,f(v,z,u))). [para(874(a,2),21(a,2,3)),rewrite([21(5)]),flip(a)]. given #282 (T,wt=24): 929 f(x,y,f(z,u,f(x,v,z))) = f(x,z,f(x,y,f(v,z,u))). [para(874(a,2),474(a,2,3)),rewrite([5(3,R),6(3),21(5),5(6,R),6(6)]),flip(a)]. given #283 (T,wt=24): 1037 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(x,u,f(z,v,u))). [para(897(a,1),21(a,2,3)),rewrite([21(5)]),flip(a)]. given #284 (T,wt=24): 1062 f(x,y,f(z,u,f(x,v,u))) = f(x,u,f(x,y,f(z,v,u))). [para(897(a,1),474(a,2,3)),rewrite([5(3,R),6(3),21(5),5(6,R),6(6)]),flip(a)]. given #285 (A,wt=31): 116 f(x,y,f(y,z,f(y,u,f(y,v,w)))) = f(x,y,f(y,v,f(y,z,f(y,u,w)))). [para(18(a,1),28(a,2,3)),rewrite([28(5)])]. given #286 (T,wt=24): 1105 f(x,y,f(z,u,f(u,x,v))) = f(u,x,f(x,y,f(z,u,v))). [para(29(a,1),922(a,2)),rewrite([5(1,R),6(1),5(4,R),6(4),922(7),5(6,R),6(6)])]. given #287 (T,wt=24): 1119 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,z,f(y,x,u))). [para(38(a,2),922(a,2)),rewrite([5(1,R),6(1),5(4,R),6(4),922(7),5(5)]),flip(a)]. given #288 (T,wt=24): 1136 f(x,f(y,z,u),f(x,v,f(y,z,v))) = f(x,v,f(y,z,u)). [para(922(a,1),803(a,1,3,3))]. given #289 (T,wt=24): 1138 f(f(x,y,z),f(x,y,f(y,z,u)),f(x,z,v)) = f(x,y,z). [para(803(a,1),922(a,1,3)),rewrite([5(5),803(8)])]. given #290 (A,wt=35): 117 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),28(a,1,3,3))]. given #291 (T,wt=24): 1142 f(x,f(y,z,x),f(u,f(y,z,v),f(y,z,x))) = f(y,z,x). [para(922(a,1),874(a,1,3)),rewrite([5(3,R),15(3),5(5)]),flip(a)]. given #292 (T,wt=24): 1148 f(x,f(y,z,u),f(x,u,f(y,z,v))) = f(x,u,f(y,z,v)). [para(922(a,1),922(a,1,2)),rewrite([5(3),5(6)])]. given #293 (T,wt=24): 1176 f(x,f(y,z,u),f(x,u,v)) = f(x,v,f(z,u,f(x,y,u))). [para(933(a,1),828(a,2,3)),rewrite([5(2,R),6(2),5(4)])]. Low Water (keep, True_semantics): wt=43 given #294 (T,wt=24): 1179 f(f(x,y,z),f(x,y,u),f(u,v,f(x,y,u))) = f(x,y,u). [para(922(a,1),933(a,1,3)),rewrite([5(3,R),15(3),6(5)]),flip(a)]. 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(28(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): 1197 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,z,f(x,y,u))). [para(38(a,2),1057(a,2)),rewrite([6(3),5(6,R),6(6),392(7),1072(7),5(5,R),6(5)]),flip(a)]. given #297 (T,wt=24): 1208 f(x,f(y,x,z),f(u,f(y,z,v),f(y,x,z))) = f(y,x,z). [para(1057(a,1),874(a,1,3)),rewrite([5(3,R),15(3),5(5)]),flip(a)]. given #298 (T,wt=24): 1212 f(f(x,y,z),f(x,u,y),f(u,v,f(x,u,y))) = f(x,u,y). [para(1057(a,1),933(a,1,3)),rewrite([5(3,R),15(3),6(5)]),flip(a)]. given #299 (T,wt=24): 1254 f(x,f(y,z,u),f(x,v,f(x,z,u))) = f(x,v,f(x,z,u)). [para(1071(a,1),8(a,2,3))]. 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): 1286 f(x,f(y,z,u),f(x,u,f(x,z,v))) = f(x,v,f(x,z,u)). [para(1071(a,1),32(a,2,3)),rewrite([6(2)])]. given #302 (T,wt=24): 1301 f(x,y,f(x,f(z,x,u),f(y,u,v))) = f(z,x,f(x,y,u)). [para(1071(a,1),41(a,1,3)),rewrite([5(3),5(3),392(6)]),flip(a)]. Low Water (keep, True_semantics): wt=42 given #303 (T,wt=24): 1323 f(x,y,f(x,f(y,z,u),f(x,v,z))) = f(x,v,f(x,y,z)). [para(1071(a,1),43(a,1,3)),rewrite([5(3),5(3)]),flip(a)]. given #304 (T,wt=24): 1329 f(x,f(y,z,u),f(x,v,f(z,u,v))) = f(x,v,f(y,z,u)). [para(1071(a,1),803(a,1,3,3)),rewrite([5(2),5(2)])]. 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): 1341 f(x,y,f(x,f(z,u,v),f(y,z,u))) = f(x,y,f(z,u,v)). [para(1071(a,1),922(a,1,2)),rewrite([5(2),5(2),5(3),392(4),5(5),5(5),5(6)])]. given #307 (T,wt=21): 21782 f(x,y,f(z,f(x,y,z),f(u,v,w))) = f(x,y,z). [para(1341(a,1),6221(a,1,3))]. given #308 (T,wt=21): 21842 f(x,y,f(z,f(x,z,y),f(u,v,w))) = f(x,z,y). [para(21782(a,1),5(a,2)),rewrite([5(1),5(1),6(4),5(5),5(5)])]. Low Water (keep, True_semantics): wt=41 given #309 (T,wt=24): 1342 f(f(x,y,z),f(u,x,y),f(u,v,f(u,x,y))) = f(u,x,y). [para(1071(a,1),933(a,1,3)),rewrite([5(3,R),15(3),5(2),5(2),6(5)]),flip(a)]. 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): 1344 f(f(x,y,z),f(y,z,u),f(u,v,f(y,z,u))) = f(y,z,u). [para(1071(a,1),1057(a,1,3)),rewrite([5(2),5(2),6(3),5(4),5(4),6(5),5(7),5(7),1253(8)])]. given #312 (T,wt=24): 1355 f(x,f(y,z,x),f(u,f(y,z,x),f(y,z,v))) = f(y,z,x). [para(1073(a,1),24(a,1,3)),rewrite([15(3)]),flip(a)]. given #313 (T,wt=24): 1393 f(f(x,y,z),f(x,z,u),f(x,y,f(y,z,v))) = f(x,y,z). [para(803(a,1),1073(a,1,2)),rewrite([5(5,R),803(8)])]. given #314 (T,wt=24): 1394 f(f(x,y,z),f(x,y,u),f(z,v,f(x,y,z))) = f(x,y,z). [para(1073(a,1),828(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): 1404 f(x,y,f(x,f(z,u,v),f(y,u,v))) = f(x,y,f(z,u,v)). [para(1071(a,1),1073(a,1,3)),rewrite([5(2),6(4),392(4),5(6)])]. given #317 (T,wt=24): 1430 f(f(x,y,z),f(y,z,u),f(x,v,f(x,y,z))) = f(x,y,z). [para(1074(a,1),828(a,1,3)),rewrite([5(3,R),15(3),6(5)]),flip(a)]. given #318 (T,wt=24): 1440 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(x,u,f(v,z,u))). [para(1149(a,1),21(a,2,3)),rewrite([21(5)]),flip(a)]. Low Water (keep, True_semantics): wt=40 given #319 (T,wt=24): 1463 f(x,y,f(z,u,f(x,v,u))) = f(x,u,f(x,y,f(v,z,u))). [para(1149(a,1),474(a,2,3)),rewrite([5(3,R),6(3),21(5),5(6,R),6(6)]),flip(a)]. 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),25(a,1,3,3))]. given #321 (T,wt=24): 1474 f(f(x,y,z),f(x,y,u),f(v,u,f(x,y,u))) = f(x,y,u). [para(922(a,1),1149(a,1,3)),rewrite([15(3)]),flip(a)]. given #322 (T,wt=24): 1475 f(f(x,y,z),f(x,u,y),f(v,u,f(x,u,y))) = f(x,u,y). [para(1057(a,1),1149(a,1,3)),rewrite([15(3)]),flip(a)]. given #323 (T,wt=24): 1478 f(f(x,y,z),f(u,x,y),f(v,u,f(u,x,y))) = f(u,x,y). [para(1071(a,1),1149(a,1,3)),rewrite([15(3),5(2),5(2)]),flip(a)]. given #324 (T,wt=24): 1541 f(x,f(y,x,z),f(u,f(y,x,z),f(y,z,v))) = f(y,x,z). [para(1181(a,1),24(a,1,3)),rewrite([15(3)]),flip(a)]. given #325 (A,wt=31): 133 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(25(a,1),16(a,1,3)),rewrite([5(2,R),6(2),5(8,R),6(8)])]. given #326 (T,wt=24): 1557 f(f(x,y,z),f(x,z,u),f(y,v,f(x,y,z))) = f(x,y,z). [para(1181(a,1),828(a,1,3)),rewrite([5(3,R),15(3),6(5)]),flip(a)]. given #327 (T,wt=24): 1630 f(x,y,f(y,f(z,u,v),f(x,z,u))) = f(x,y,f(z,u,v)). [para(922(a,1),812(a,1,3,3)),rewrite([5(2)])]. given #328 (T,wt=24): 1633 f(x,y,f(y,f(z,u,v),f(x,u,v))) = f(x,y,f(z,u,v)). [para(1071(a,1),812(a,1,3,3))]. given #329 (T,wt=24): 1661 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,u,y))). [para(33(a,1),813(a,2)),rewrite([6(5),696(6),57(6),6(4),1200(7)])]. given #330 (A,wt=31): 135 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),25(a,2,3,3))]. given #331 (T,wt=24): 1671 f(x,f(y,z,f(x,u,y)),f(x,v,u)) = f(x,v,f(x,u,y)). [para(827(a,1),17(a,1,3)),flip(a)]. given #332 (T,wt=24): 1724 f(f(x,y,z),f(x,u,f(x,y,z)),f(y,z,v)) = f(x,y,z). [back_rewrite(1712),rewrite([1713(8)])]. given #333 (T,wt=24): 1750 f(f(x,y,z),f(x,y,f(x,z,u)),f(y,z,v)) = f(x,y,z). [para(866(a,1),922(a,1,3)),rewrite([5(3,R),6(3),6(4),5(5),866(8),6(6)])]. Low Water (keep, True_semantics): wt=39 given #334 (T,wt=24): 1757 f(f(x,y,z),f(y,z,u),f(x,y,f(x,z,v))) = f(x,y,z). [para(866(a,1),1073(a,1,2)),rewrite([6(3),5(4,R),6(4),5(5,R),866(8),6(6)])]. given #335 (A,wt=38): 136 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(25(a,1),18(a,1,3,3)),flip(a)]. given #336 (T,wt=24): 1766 f(x,y,f(y,f(x,z,u),f(z,u,v))) = f(x,y,f(z,u,v)). [para(922(a,1),868(a,1,3,3)),rewrite([5(2),5(3,R),6(6)])]. given #337 (T,wt=21): 23737 f(x,y,f(z,f(y,z,u),f(x,v,z))) = f(x,y,z). [para(1738(a,1),1766(a,1,3)),rewrite([6(2),7553(3),5(4,R),8713(5)]),flip(a)]. Low Water (keep, True_semantics): wt=38 given #338 (T,wt=24): 1769 f(x,y,f(y,f(x,z,u),f(v,z,u))) = f(x,y,f(v,z,u)). [para(1071(a,1),868(a,1,3,3)),rewrite([5(3,R),6(6)])]. given #339 (T,wt=24): 1906 f(x,f(y,z,u),f(y,z,f(z,u,x))) = f(z,x,f(y,z,u)). [para(628(a,1),871(a,1,3)),rewrite([6(2),5(4,R),6(4),6(6)])]. given #340 (A,wt=38): 137 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(25(a,1),18(a,2,3,3))]. given #341 (T,wt=24): 1987 f(f(x,y,z),f(y,z,u),f(v,x,f(x,y,z))) = f(x,y,z). [para(1030(a,1),1073(a,1,2)),rewrite([5(1,R),6(1),5(3,R),6(3),5(5,R),5(6,R),6(6),1982(8)])]. given #342 (T,wt=24): 1998 f(f(x,y,z),f(u,x,f(x,y,z)),f(y,z,v)) = f(x,y,z). [para(1051(a,1),922(a,1,3)),rewrite([5(1),5(4),5(5),5(6),1982(8)])]. given #343 (T,wt=24): 2175 f(x,f(y,z,u),f(x,v,f(x,y,u))) = f(x,v,f(x,y,u)). [para(1072(a,1),50(a,1,3,3)),rewrite([1072(7)])]. given #344 (T,wt=24): 2206 f(f(x,y,z),f(x,y,f(y,u,z)),f(x,z,v)) = f(x,y,z). [para(1634(a,1),922(a,1,3)),rewrite([5(1),6(4),5(5),5(6),1669(8)])]. given #345 (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(25(a,2),18(a,1,3,3))]. given #346 (T,wt=24): 2209 f(f(x,y,z),f(x,z,u),f(x,y,f(y,v,z))) = f(x,y,z). [para(1634(a,1),1073(a,1,2)),rewrite([5(1),6(3),5(5,R),5(6),1669(8)])]. given #347 (T,wt=24): 3301 f(f(x,y,z),f(y,z,u),f(v,u,f(y,z,u))) = f(y,z,u). [para(3270(a,1),1253(a,1,3)),rewrite([6(5),3270(8)])]. given #348 (T,wt=24): 4003 f(x,y,f(x,f(y,z,u),f(z,u,v))) = f(x,y,f(z,u,v)). [para(922(a,1),3475(a,1,3,3)),rewrite([5(2,R),6(2),5(3),5(4,R),6(4),57(5),20(5),5(6,R),6(6)])]. given #349 (T,wt=21): 24059 f(x,y,f(z,f(x,z,u),f(y,v,z))) = f(x,y,z). [para(1738(a,1),4003(a,1,3)),rewrite([6(2),1072(3),5(4,R),8713(5)]),flip(a)]. given #350 (A,wt=38): 139 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(25(a,2),18(a,2,3,3)),flip(a)]. given #351 (T,wt=24): 4005 f(x,y,f(x,f(y,z,u),f(v,z,u))) = f(x,y,f(v,z,u)). [para(1071(a,1),3475(a,1,3,3)),rewrite([5(2,R),6(2),5(4,R),6(4),57(5),20(5),5(6,R),6(6)])]. given #352 (T,wt=24): 4278 f(x,y,f(z,u,f(y,v,u))) = f(x,y,f(y,u,f(v,z,u))). [para(933(a,1),3998(a,2,3)),rewrite([6(2),28(4),6(2),5(4)]),flip(a)]. given #353 (T,wt=24): 5019 f(x,y,f(x,f(z,u,v),f(y,z,v))) = f(x,y,f(z,u,v)). [para(1072(a,1),1082(a,1,3,3))]. given #354 (T,wt=24): 5247 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(x,y,f(z,x,v))). [para(41(a,1),1726(a,2)),rewrite([6(7),696(8),57(8),6(6),5(9,R),6(9),5244(10)])]. given #355 (A,wt=31): 140 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(25(a,2),18(a,2,3)),flip(a)]. given #356 (T,wt=24): 5454 f(x,y,f(z,x,f(x,u,v))) = f(x,y,f(x,v,f(z,x,u))). [para(32(a,2),1856(a,2)),rewrite([6(7),5(8,R),6(8),5(9,R),6(9),392(10),6(9),4302(10),5(4,R),6(4)])]. given #357 (T,wt=24): 5455 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(z,x,f(x,y,u))). [para(33(a,1),1856(a,2)),rewrite([6(7),5(8,R),6(8),5(9,R),6(9),392(10),6(9),4302(10),5(5,R),6(5)])]. given #358 (T,wt=24): 5459 f(x,y,f(z,y,f(y,u,v))) = f(x,y,f(y,u,f(z,y,v))). [para(40(a,1),1856(a,2)),rewrite([6(7),5(8,R),6(8),5(9,R),6(9),5448(10),5(4,R),6(4)])]. given #359 (T,wt=24): 5496 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,v,f(x,y,u))). [para(59(a,1),1856(a,2)),rewrite([6(7),5(8,R),6(8),5(9,R),6(9),392(10),6(9),4302(10),5(6,R),6(6)])]. given #360 (A,wt=38): 141 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),25(a,1,3,3))]. given #361 (T,wt=24): 5502 f(x,y,f(z,x,f(x,u,v))) = f(x,u,f(x,v,f(z,x,y))). [para(61(a,1),1856(a,2)),rewrite([6(7),5(8,R),6(8),5(9,R),6(9),392(10),6(9),4302(10),5(4,R),6(4)])]. given #362 (T,wt=21): 24356 f(x,y,f(z,x,f(u,x,y))) = f(z,x,f(u,x,y)). [para(5502(a,2),1469(a,2)),rewrite([4(3),6(2),5(4),122(5)]),flip(a)]. given #363 (T,wt=24): 6071 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(z,x,f(x,u,y))). [para(33(a,1),3678(a,2)),rewrite([5(5,R),6(5),57(7),6065(8),5(5,R),6(5)])]. given #364 (T,wt=24): 6107 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,v,f(x,u,y))). [para(59(a,1),3678(a,2)),rewrite([5(5,R),6(5),57(7),6065(8),5(6,R),6(6)])]. given #365 (A,wt=38): 142 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),25(a,2,3,3))]. given #366 (T,wt=24): 6694 f(x,f(y,z,f(x,u,y)),f(v,x,u)) = f(x,y,f(v,x,u)). [para(1071(a,1),4906(a,1,3,3)),rewrite([5(2),5(2),5(4,R),5(6)])]. given #367 (T,wt=24): 6719 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 #368 (T,wt=24): 6840 f(x,f(y,z,u),f(y,u,f(y,x,z))) = f(y,x,f(y,z,u)). [para(1076(a,1),70(a,2,3)),rewrite([5(4),5(4),20(4),1598(5),5(7,R),57(7),6(5),20(6)])]. given #369 (T,wt=24): 7307 f(x,f(y,z,u),f(x,v,f(y,u,v))) = f(x,v,f(y,z,u)). [para(7121(a,1),1669(a,1,3,3)),rewrite([5(2),5(2)])]. given #370 (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),25(a,1,3,3))]. given #371 (T,wt=24): 7334 f(f(x,y,z),f(x,z,u),f(u,v,f(x,z,u))) = f(x,z,u). [back_rewrite(7294),rewrite([7301(8)])]. given #372 (T,wt=24): 7335 f(f(x,y,z),f(x,z,u),f(v,u,f(x,z,u))) = f(x,z,u). [para(7301(a,1),1253(a,1,3)),rewrite([6(5),7301(8)])]. given #373 (T,wt=24): 7338 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 #374 (T,wt=24): 7343 f(x,y,f(z,y,f(y,u,v))) = f(x,y,f(y,v,f(z,y,u))). [para(30(a,2),72(a,2,3)),rewrite([72(6)])]. given #375 (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,v,f(z,w,f(z,u,v6))))). [para(18(a,2),25(a,2,3,3))]. given #376 (T,wt=24): 7405 f(x,f(y,z,u),f(y,z,f(z,x,u))) = f(z,x,f(y,z,u)). [para(72(a,1),922(a,1,3)),rewrite([5(1,R),6(1),6(4),5(6,R),6(6),2455(7),5(4,R),6(4)]),flip(a)]. given #377 (T,wt=24): 7671 f(x,y,f(y,f(z,u,v),f(x,z,v))) = f(x,y,f(z,u,v)). [para(7121(a,1),7553(a,1,3,3))]. given #378 (T,wt=24): 7681 f(x,y,f(y,f(x,z,u),f(z,v,u))) = f(x,y,f(z,v,u)). [para(7121(a,1),7552(a,1,3,3)),rewrite([6(4),28(5)])]. given #379 (T,wt=24): 7761 f(x,f(y,z,u),f(v,x,z)) = f(v,x,f(y,z,f(x,z,u))). [para(74(a,2),828(a,1)),flip(a)]. given #380 (A,wt=31): 145 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(25(a,1),24(a,1,3)),rewrite([5(2,R),6(2),5(8,R),6(8)])]. given #381 (T,wt=24): 8102 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 #382 (T,wt=24): 8103 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 #383 (T,wt=24): 8219 f(x,f(y,z,u),f(z,x,v)) = f(x,v,f(y,z,f(z,x,u))). [para(75(a,2),922(a,2)),rewrite([5(1,R),6(1),5(4,R),6(4),922(7),5(5)]),flip(a)]. given #384 (T,wt=24): 8330 f(x,y,f(x,f(z,u,v),f(z,y,u))) = f(x,y,f(z,u,v)). [para(75(a,2),1088(a,1,2)),rewrite([392(3),813(3),8150(4)])]. given #385 (A,wt=31): 147 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(25(a,1),24(a,2,3)),rewrite([5(3,R),6(3),5(8,R),6(8)]),flip(a)]. given #386 (T,wt=24): 8849 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,x,f(z,v,u))). [para(76(a,2),1076(a,2)),rewrite([6(6),2446(10)]),flip(a)]. given #387 (T,wt=24): 9417 f(x,y,f(z,u,f(y,z,v))) = f(x,y,f(z,v,f(y,z,u))). [para(874(a,1),78(a,1,3,3)),rewrite([5(1),5(1),5(2,R),6(2),20(2),5(4),102(7)])]. given #388 (T,wt=24): 9821 f(x,f(y,z,u),f(y,u,f(y,z,x))) = f(y,x,f(y,z,u)). [para(83(a,1),5(a,2)),rewrite([5(2),5(2),5(4),5(6,R),6(6)])]. given #389 (T,wt=24): 9937 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 #390 (A,wt=31): 149 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(25(a,2),24(a,1,3)),rewrite([5(1,R),6(1),5(8,R),6(8)])]. given #391 (T,wt=24): 9988 f(x,y,f(x,f(z,y,u),f(v,x,z))) = f(v,x,f(x,z,y)). [para(803(a,1),87(a,1,3)),flip(a)]. given #392 (T,wt=24): 10010 f(x,y,f(x,f(y,z,u),f(v,x,z))) = f(v,x,f(x,y,z)). [para(813(a,1),87(a,1,3)),flip(a)]. given #393 (T,wt=24): 10494 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,z,y))). [para(91(a,1),6(a,2)),rewrite([6(3),6(4)])]. given #394 (T,wt=24): 10617 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(x,u,f(z,x,y))). [para(91(a,1),1856(a,2)),rewrite([6(7),5(8,R),6(8),5(9,R),6(9),392(10),6(9),4302(10),5(4,R),6(4)])]. given #395 (A,wt=31): 150 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(25(a,2),24(a,2,3)),rewrite([5(3,R),6(3),5(8,R),6(8)]),flip(a)]. given #396 (T,wt=24): 10630 f(x,y,f(z,x,f(x,u,v))) = f(x,v,f(x,y,f(z,x,u))). [para(91(a,1),3678(a,2)),rewrite([5(5,R),6(5),57(7),6065(8),5(4,R),6(4)])]. given #397 (T,wt=24): 11098 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(v,z,f(x,z,u))). [para(874(a,2),105(a,2,3)),flip(a)]. given #398 (T,wt=22): 25239 f(x,y,f(z,x,f(y,u,f(z,v,y)))) = f(z,x,y). [para(11098(a,2),74(a,2,3)),rewrite([1738(4)]),flip(a)]. given #399 (T,wt=24): 11105 f(x,y,f(z,u,f(u,x,v))) = f(x,y,f(u,x,f(z,u,v))). [para(105(a,1),922(a,2)),rewrite([5(1,R),6(1),5(4,R),6(4),922(7),5(5,R),6(5)])]. given #400 (A,wt=31): 151 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(30(a,2),25(a,2,3,3))]. given #401 (T,wt=24): 12844 f(x,f(y,z,x),f(x,u,f(y,z,v))) = f(x,u,f(y,z,x)). [para(922(a,1),168(a,1,3,3)),rewrite([922(6)]),flip(a)]. given #402 (T,wt=24): 12849 f(x,f(y,z,u),f(x,v,f(y,z,x))) = f(x,v,f(y,z,x)). [para(1073(a,1),168(a,1,3,3)),rewrite([15(6)]),flip(a)]. given #403 (T,wt=24): 12870 f(x,f(y,z,u),f(x,v,f(z,u,x))) = f(x,v,f(z,u,x)). [para(3270(a,1),168(a,1,3,3)),rewrite([15(6)]),flip(a)]. given #404 (T,wt=24): 12912 f(x,f(y,z,u),f(x,v,f(y,u,x))) = f(x,v,f(y,u,x)). [para(7301(a,1),168(a,1,3,3)),rewrite([15(6)]),flip(a)]. given #405 (A,wt=35): 155 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),25(a,1,3,3)),rewrite([6(1),6(5)]),flip(a)]. given #406 (T,wt=24): 13409 f(x,f(y,z,u),f(z,u,f(y,z,x))) = f(z,x,f(y,z,u)). [para(169(a,1),5(a,2)),rewrite([5(2),5(2),5(4),5(6,R),6(6)])]. given #407 (T,wt=24): 14290 f(x,y,f(z,u,f(y,v,z))) = f(x,y,f(v,z,f(y,z,u))). [para(828(a,1),262(a,2,3)),rewrite([5(1,R),6(1),5(4)]),flip(a)]. given #408 (T,wt=22): 25376 f(x,y,f(x,z,f(y,u,f(z,v,y)))) = f(x,z,y). [para(14290(a,2),29(a,2,3)),rewrite([1905(4)]),flip(a)]. given #409 (T,wt=24): 14514 f(x,f(y,z,u),f(v,y,x)) = f(v,x,f(y,z,f(y,u,x))). [para(318(a,2),5(a,2)),rewrite([6(3),5(5)]),flip(a)]. given #410 (A,wt=31): 156 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),25(a,2,3,3)),rewrite([6(1),118(4),6(5)])]. given #411 (T,wt=24): 15009 f(x,f(y,z,u),f(y,v,x)) = f(v,x,f(y,z,f(y,u,x))). [para(319(a,1),5(a,2)),rewrite([5(2,R),6(2),5(3),6(4)])]. given #412 (T,wt=24): 15010 f(x,f(y,x,z),f(z,u,v)) = f(y,x,f(z,u,f(x,z,v))). [para(319(a,1),6(a,1)),rewrite([5(1,R),6(1),6(4)]),flip(a)]. given #413 (T,wt=24): 15252 f(f(x,y,z),f(x,y,f(x,u,z)),f(y,z,v)) = f(x,y,z). [para(15203(a,1),922(a,1,3)),rewrite([5(5),15203(8)])]. given #414 (T,wt=24): 15254 f(f(x,y,z),f(y,z,u),f(x,y,f(x,v,z))) = f(x,y,z). [para(15203(a,1),1073(a,1,2)),rewrite([5(5,R),15203(8)])]. 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(25(a,2),28(a,1,3,3))]. given #416 (T,wt=24): 15317 f(x,f(x,y,z),f(u,v,w)) = f(x,y,f(x,z,f(u,v,w))). [para(15075(a,1),111(a,2)),rewrite([5(3,R),5(6),5(6),5(8),5(8),15316(8),5(6,R)]),flip(a)]. given #417 (T,wt=24): 15322 f(x,f(y,z,u),f(x,v,w)) = f(x,v,f(x,w,f(y,z,u))). [para(15075(a,1),130(a,2,3)),rewrite([6(4),15293(6),15317(3)]),flip(a)]. given #418 (T,wt=24): 15324 f(x,f(y,x,z),f(u,v,w)) = f(y,x,f(x,z,f(u,v,w))). [para(15075(a,1),220(a,1)),rewrite([6(2),6(6),5(10),6(10),15297(10),19(8)]),flip(a)]. given #419 (T,wt=22): 26538 f(x,y,f(z,u,f(x,z,f(y,v,z)))) = f(x,y,z). [back_rewrite(23124),rewrite([5(2,R),6(2),26355(3),5(4),5(4),25905(6),921(5),15317(4),25551(4),6(1),5(2,R),6(2),24109(5),5(5),5(5)])]. given #420 (A,wt=35): 159 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(28(a,1),25(a,1,3,3)),flip(a)]. given #421 (T,wt=21): 26666 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(26538(a,1),38(a,2)),rewrite([5(1),6(3),6(5)])]. given #422 (T,wt=21): 26694 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(5(a,1),26666(a,1,2,3)),rewrite([5(1,R),6(1)])]. given #423 (T,wt=24): 15657 f(x,f(y,z,u),f(x,y,v)) = f(x,v,f(y,z,f(x,y,u))). [back_rewrite(15475),rewrite([15633(7)])]. given #424 (T,wt=24): 15685 f(x,f(y,z,f(u,x,y)),f(u,x,v)) = f(x,y,f(u,x,v)). [para(803(a,1),15202(a,1,3,3)),rewrite([5(2),5(2),5(4,R),5(6)])]. given #425 (A,wt=31): 160 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(28(a,1),25(a,2,3,3)),rewrite([102(4)])]. given #426 (T,wt=24): 15702 f(x,f(y,z,f(u,x,y)),f(u,v,x)) = f(x,y,f(u,v,x)). [para(1669(a,1),15202(a,1,3,3)),rewrite([5(2),5(2),5(4,R),5(6)])]. given #427 (T,wt=24): 15743 f(x,f(y,z,f(y,u,x)),f(y,u,f(u,x,v))) = f(y,u,x). [para(1905(a,1),15202(a,1,3,3)),rewrite([5(1,R),6(1),6(3),5(5,R),5(6,R),6(6),6(8),803(8)])]. given #428 (T,wt=22): 27256 f(x,y,f(z,u,f(x,z,f(v,z,y)))) = f(x,z,y). [para(3301(a,1),15743(a,1,3)),rewrite([5(3),5(4),15690(4),5(3,R),5(4),6(5),15317(5),25908(5),5(3,R),6(3),5(6),5(7),15690(7)])]. given #429 (T,wt=24): 15763 f(x,f(y,z,f(u,y,x)),f(u,v,f(u,y,x))) = f(u,y,x). [para(5305(a,1),15202(a,1,3,3)),rewrite([5(1),5(3),5(5,R),5(6),6(8),1713(8)])]. given #430 (A,wt=31): 161 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(25(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): 15764 f(x,f(y,z,f(u,y,x)),f(u,y,f(u,x,v))) = f(u,y,x). [para(5310(a,1),15202(a,1,3,3)),rewrite([5(5,R),6(8),871(8)])]. given #432 (T,wt=24): 15772 f(x,f(y,z,f(y,u,x)),f(y,u,f(u,v,x))) = f(y,u,x). [para(8635(a,1),15202(a,1,3,3)),rewrite([5(5,R),6(8),1669(8)])]. given #433 (T,wt=24): 15773 f(x,f(y,z,f(u,y,x)),f(u,y,f(u,v,x))) = f(u,y,x). [para(9577(a,1),15202(a,1,3,3)),rewrite([5(5,R),6(8),15203(8)])]. given #434 (T,wt=24): 15787 f(x,f(y,z,f(u,x,y)),f(v,u,x)) = f(x,y,f(v,u,x)). [para(12377(a,1),15202(a,1,3,3)),rewrite([5(2),5(2),5(4,R),5(6)])]. given #435 (A,wt=31): 163 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),25(a,1,3,3)),rewrite([5(2,R),6(2),5(6,R),6(6),159(9)])]. given #436 (T,wt=24): 15822 f(x,f(y,z,u),f(x,y,f(v,x,z))) = f(v,x,f(x,y,z)). [para(15690(a,1),41(a,1,3)),rewrite([5(3),5(3)]),flip(a)]. given #437 (T,wt=24): 15828 f(x,f(y,z,u),f(x,y,f(z,u,v))) = f(x,y,f(z,u,v)). [para(15690(a,1),922(a,1,2)),rewrite([5(2),5(2),5(3),5(5),5(5),5(6)])]. given #438 (T,wt=24): 15832 f(x,f(y,z,u),f(x,y,f(v,z,u))) = f(x,y,f(v,z,u)). [para(15690(a,1),1073(a,1,3)),rewrite([5(2),6(4),5(6)])]. given #439 (T,wt=24): 15840 f(x,y,f(x,f(z,u,y),f(v,z,u))) = f(x,y,f(v,z,u)). [para(15690(a,1),866(a,1,3,3)),rewrite([5(2),5(2),5(3,R),6(3),5(4,R),15317(4),5(6)])]. given #440 (A,wt=38): 164 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(25(a,1),25(a,1,3,3))]. given #441 (T,wt=24): 15885 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(y,z,f(x,z,u))). [para(75(a,1),15690(a,2)),rewrite([6(2),6(5),15690(7)])]. given #442 (T,wt=24): 15887 f(x,f(y,z,f(x,u,z)),f(v,x,u)) = f(x,z,f(v,x,u)). [para(15690(a,1),5310(a,1,3,3)),rewrite([5(2),5(2),5(4,R),5(6)])]. given #443 (T,wt=24): 15891 f(x,f(y,z,f(u,x,z)),f(v,u,x)) = f(x,z,f(v,u,x)). [para(15690(a,1),9577(a,1,3,3)),rewrite([5(2),5(2),5(4,R),5(6)])]. given #444 (T,wt=24): 15892 f(x,f(y,z,u),f(x,z,f(v,x,y))) = f(v,x,f(x,y,z)). [para(15690(a,1),87(a,1,3)),rewrite([5(3),5(3)]),flip(a)]. given #445 (A,wt=38): 165 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(25(a,1),25(a,2,3,3))]. given #446 (T,wt=24): 15977 f(x,f(y,z,u),f(x,u,f(x,y,v))) = f(x,v,f(x,y,u)). [para(15715(a,1),32(a,2,3)),rewrite([6(2)])]. given #447 (T,wt=24): 15989 f(x,f(y,z,u),f(x,y,f(z,v,u))) = f(x,y,f(z,v,u)). [para(15715(a,1),1073(a,1,3)),rewrite([5(2),6(4),5(6)])]. given #448 (T,wt=24): 15991 f(x,f(y,z,u),f(x,z,f(y,u,v))) = f(x,z,f(y,u,v)). [para(1181(a,1),15715(a,1,2))]. given #449 (T,wt=24): 15994 f(x,y,f(x,f(z,u,y),f(z,v,u))) = f(x,y,f(z,v,u)). [para(15715(a,1),866(a,1,3,3)),rewrite([5(2),5(2),5(3,R),6(3),5(4,R),15317(4),5(6)])]. given #450 (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(25(a,2),25(a,1,3,3))]. given #451 (T,wt=24): 16047 f(x,f(y,z,f(u,x,z)),f(u,v,x)) = f(x,z,f(u,v,x)). [para(15715(a,1),9577(a,1,3,3)),rewrite([5(2),5(2),5(4,R),5(6)])]. given #452 (T,wt=24): 16083 f(x,y,f(x,f(z,u,y),f(z,u,v))) = f(x,y,f(z,u,v)). [para(15740(a,1),866(a,1,3,3)),rewrite([5(2),5(2),5(3,R),6(3),5(4,R),15317(4),5(6)])]. given #453 (T,wt=24): 16098 f(x,f(y,z,f(u,x,z)),f(u,x,v)) = f(x,z,f(u,x,v)). [para(15740(a,1),9577(a,1,3,3)),rewrite([5(2),5(2),5(4,R),5(6)])]. given #454 (T,wt=24): 16392 f(x,f(y,z,u),f(u,x,v)) = f(x,v,f(y,u,f(z,u,x))). [para(321(a,1),5(a,2)),rewrite([5(2,R),6(2),5(3),5(4),5(4)])]. given #455 (A,wt=38): 167 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(25(a,2),25(a,2,3,3))]. given #456 (T,wt=24): 16393 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(z,u,f(x,y,z))). [para(5(a,2),321(a,1,2)),rewrite([5(5,R),6(5)])]. given #457 (T,wt=21): 28284 f(x,f(y,z,f(u,z,v)),f(x,z,v)) = f(x,z,v). [para(16393(a,2),2861(a,1,2)),rewrite([15(2),6(2),5(3),5(5)])]. given #458 (T,wt=24): 16398 f(x,f(y,z,u),f(x,v,u)) = f(x,v,f(y,u,f(x,z,u))). [para(321(a,2),20(a,1,3)),rewrite([6(2),22(4)])]. given #459 (T,wt=24): 16422 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))). [para(22(a,1),321(a,1,2)),rewrite([6(5),19(6),15317(9),15317(8),243(8),15211(8)])]. given #460 (A,wt=34): 172 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),27(a,1,3,3))]. given #461 (T,wt=21): 28518 f(x,f(y,z,f(y,u,v)),f(y,x,v)) = f(y,x,v). [para(3114(a,1),172(a,2,3)),rewrite([5(2,R),6(2),6(3),5(6,R),6(6),15(7),6(7),15(9),6(5),20(6)])]. given #462 (T,wt=21): 28530 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(5(a,1),28518(a,1,2,3)),rewrite([5(1,R),6(1),5(3,R),6(3),5(5,R),6(5)])]. given #463 (T,wt=22): 28534 f(x,y,f(y,z,f(x,u,f(x,v,z)))) = f(x,y,z). [para(28518(a,1),103(a,2)),rewrite([20(5),6(5),26355(5),51(4),28(5),20(6)])]. given #464 (T,wt=24): 16554 f(x,f(y,z,u),f(x,z,f(y,v,u))) = f(x,z,f(y,v,u)). [para(321(a,2),3114(a,1,2)),rewrite([6(2),15715(3),5(3),5(6)])]. given #465 (A,wt=34): 176 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),27(a,1,2)),rewrite([5(1,R),6(1),5(5,R),6(5),5(8,R),6(8)])]. given #466 (T,wt=24): 16636 f(x,y,f(z,u,f(y,v,u))) = f(y,u,f(x,y,f(z,v,u))). [para(321(a,2),74(a,1,3)),rewrite([15(2),6(2),19(5)])]. given #467 (T,wt=21): 28667 f(x,f(y,z,f(u,z,v)),f(u,x,z)) = f(u,x,z). [para(8746(a,1),16636(a,2,3)),rewrite([19(6),8746(4)]),flip(a)]. given #468 (T,wt=24): 16651 f(x,y,f(x,f(y,z,u),f(x,v,u))) = f(x,v,f(x,y,u)). [para(321(a,2),76(a,2,3)),rewrite([5(2,R),6(2),16415(3),6(4),5(6,R),6(6)]),flip(a)]. given #469 (T,wt=24): 17148 f(x,y,f(y,f(x,z,u),f(y,u,v))) = f(y,v,f(x,y,u)). [para(15127(a,1),471(a,2,3)),rewrite([5(1,R),6(1),6(2)])]. given #470 (A,wt=34): 179 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),27(a,1,3,3))]. given #471 (T,wt=21): 28818 f(x,f(y,z,f(u,v,y)),f(u,x,y)) = f(u,x,y). [para(813(a,1),17148(a,1,3)),rewrite([6(2),7553(3),5(3),5(3)]),flip(a)]. given #472 (T,wt=22): 28830 f(x,y,f(z,u,f(y,z,f(x,v,z)))) = f(x,y,z). [para(1738(a,1),17148(a,1,3)),rewrite([6(2),7553(3),5(4,R),26355(4),6(6),26355(6),102(6)]),flip(a)]. given #473 (T,wt=22): 28833 f(x,y,f(y,z,f(z,u,f(x,v,z)))) = f(x,y,z). [para(1905(a,1),17148(a,1,3)),rewrite([6(2),7553(3),5(3),5(3),6(6),26355(6),73(6)]),flip(a)]. given #474 (T,wt=24): 17657 f(x,y,f(x,z,f(u,x,v))) = f(x,v,f(x,y,f(u,x,z))). [para(479(a,1),812(a,2)),rewrite([6(5),15317(6),15317(5),16914(7)]),flip(a)]. given #475 (A,wt=38): 181 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(27(a,1),18(a,1,3,3)),flip(a)]. given #476 (T,wt=24): 17912 f(x,f(y,z,u),f(v,x,f(x,y,z))) = f(v,x,f(x,y,z)). [para(7078(a,1),482(a,1,3)),rewrite([5(1),5(4),15317(6),474(6),6(4)]),flip(a)]. given #477 (T,wt=24): 18003 f(x,y,f(x,z,f(u,x,v))) = f(x,v,f(x,z,f(u,x,y))). [para(495(a,1),812(a,2)),rewrite([6(5),15317(6),15317(5),16914(7)])]. given #478 (T,wt=24): 18155 f(x,y,f(z,u,f(z,v,y))) = f(x,y,f(z,v,f(z,y,u))). [para(630(a,1),5(a,2)),rewrite([6(3),6(4),5(6,R),6(6)]),flip(a)]. given #479 (T,wt=24): 18196 f(x,y,f(z,u,f(z,v,x))) = f(x,y,f(z,v,f(z,x,u))). [para(630(a,1),922(a,2)),rewrite([922(7),6(4)]),flip(a)]. given #480 (A,wt=44): 183 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),27(a,1,3,3))]. given #481 (T,wt=24): 18247 f(x,y,f(z,u,f(z,v,y))) = f(z,y,f(x,y,f(z,v,u))). [para(630(a,1),1856(a,2)),rewrite([6(7),5(8,R),6(8),5(9,R),6(9),5450(10),6(4),5(6,R),6(6)]),flip(a)]. given #482 (T,wt=24): 18339 f(x,y,f(z,u,f(y,v,z))) = f(y,z,f(x,y,f(v,z,u))). [para(630(a,1),220(a,1,3)),rewrite([5(1),6(1),8713(3),5(4,R),6(4),20(5),5(6,R),6(6)])]. given #483 (T,wt=24): 18386 f(x,y,f(y,f(x,z,u),f(y,v,u))) = f(y,v,f(x,y,u)). [para(18288(a,1),24(a,2,3)),rewrite([5(4,R),6(4),8145(4),6(2),5(6,R),6(6)])]. given #484 (T,wt=24): 18407 f(x,f(y,z,f(x,u,y)),f(z,v,f(x,y,z))) = f(x,y,z). [para(18288(a,1),910(a,1,3,3)),rewrite([5(2,R),6(2),8713(3),6(3),5(7,R),6(7),8713(8),18382(8)])]. given #485 (A,wt=44): 185 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),27(a,1,3,3))]. given #486 (T,wt=24): 18644 f(x,f(y,z,u),f(x,y,v)) = f(x,v,f(y,u,f(x,y,z))). [para(738(a,1),38(a,2)),rewrite([6(2)])]. given #487 (T,wt=24): 18846 f(x,f(y,z,u),f(v,x,f(v,y,z))) = f(v,x,f(y,z,u)). [para(847(a,1),220(a,2,3)),rewrite([1630(5),19(4)]),flip(a)]. given #488 (T,wt=23): 29279 f(f(x,y,z),f(u,x,y),f(u,x,z)) = f(x,z,f(u,x,y)). [para(1906(a,1),18846(a,2)),rewrite([5(5),5(5),922(6),6(5),29261(5)])]. given #489 (T,wt=23): 29307 f(f(x,y,z),f(u,x,y),f(u,y,z)) = f(y,z,f(u,x,y)). [back_rewrite(23880),rewrite([29260(5)])]. given #490 (A,wt=34): 187 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),27(a,1,2)),rewrite([5(1,R),6(1),5(5,R),6(5),5(8,R),6(8)])]. given #491 (T,wt=18): 29585 f(x,y,f(z,x,f(u,z,y))) = f(z,x,y). [para(7338(a,1),29307(a,2)),rewrite([6(2),5(4,R),6(4),6(6),20(6),5(6),19929(6),15317(4),1030(3),20(2),5(3),5(5,R),6(5),26355(5),20(4)]),flip(a)]. given #492 (T,wt=22): 29609 f(x,y,f(z,y,f(u,z,f(x,z,v)))) = f(x,z,y). [para(29(a,1),187(a,1,3,3)),rewrite([871(7),6(5),15317(5),5284(4),20(2)]),flip(a)]. given #493 (T,wt=23): 29313 f(f(x,y,z),f(x,y,u),f(x,z,u)) = f(x,y,f(x,z,u)). [para(29279(a,1),5(a,1)),rewrite([5(1,R),6(1),5(3),5(3),6(4),5(5,R),6(5)]),flip(a)]. given #494 (T,wt=23): 29314 f(f(x,y,z),f(x,y,u),f(y,z,u)) = f(y,u,f(x,y,z)). [para(29279(a,1),5(a,2))]. given #495 (A,wt=44): 200 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(25(a,1),27(a,1,3,3))]. given #496 (T,wt=23): 29315 f(f(x,y,z),f(y,z,u),f(x,y,u)) = f(x,y,f(y,z,u)). [para(5(a,1),29279(a,1,1)),rewrite([5(2),5(2),5(3),6(3),5(5),5(5),5(6,R),6(6)])]. given #497 (T,wt=23): 29316 f(f(x,y,z),f(x,z,u),f(y,z,u)) = f(y,z,f(x,z,u)). [para(5(a,2),29279(a,1,1)),rewrite([5(2),6(2),5(3),6(3),5(5),6(5),5(6,R),6(6)])]. given #498 (T,wt=23): 29317 f(f(x,y,z),f(x,y,u),f(x,u,z)) = f(x,y,f(x,u,z)). [para(29279(a,1),6(a,1)),rewrite([5(1,R),6(1),6(3),5(4),5(4),5(5,R),6(5)]),flip(a)]. given #499 (T,wt=23): 29318 f(f(x,y,z),f(x,z,u),f(x,y,u)) = f(x,z,f(x,y,u)). [para(29279(a,1),6(a,2)),rewrite([5(2),5(2),5(3),5(3),5(5),5(5)])]. given #500 (A,wt=44): 202 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(25(a,2),27(a,1,3,3))]. given #501 (T,wt=23): 29358 f(f(x,y,z),f(u,x,z),f(u,x,y)) = f(x,y,f(u,x,z)). [para(29279(a,1),922(a,2)),rewrite([6(2),5(4),6(5),1253(9)])]. given #502 (T,wt=23): 29495 f(f(x,y,z),f(y,z,u),f(x,z,u)) = f(x,z,f(y,z,u)). [para(5(a,1),29307(a,1,1)),rewrite([5(2),5(2),5(3),6(3),5(5),5(5),5(6,R),6(6)])]. given #503 (T,wt=23): 29565 f(f(x,y,z),f(x,u,z),f(x,y,u)) = f(x,y,f(x,u,z)). [para(29307(a,1),15075(a,1,1)),rewrite([5(1),5(4),5(4),5(5),5(6),5(6),29463(8),15270(6),5(3),5(3),5(4),5(5),5(5)]),flip(a)]. given #504 (T,wt=23): 29663 f(f(x,y,z),f(x,u,y),f(x,u,z)) = f(x,u,f(x,y,z)). [para(29313(a,1),5(a,1)),flip(a)]. given #505 (A,wt=41): 208 f(x,y,f(z,f(x,u,f(x,v,w)),f(x,u,f(x,v,f(x,z,w))))) = f(x,y,f(x,z,f(x,u,f(x,v,w)))). [para(18(a,2),132(a,1,3,3))]. given #506 (T,wt=23): 29728 f(f(x,y,z),f(x,u,z),f(x,u,y)) = f(x,u,f(x,y,z)). [para(29314(a,1),6(a,1)),rewrite([5(1,R),6(1),5(3,R),6(3),6(4),5(5),5(5)]),flip(a)]. given #507 (T,wt=23): 29737 f(f(x,y,z),f(x,y,u),f(y,u,z)) = f(y,z,f(x,y,u)). [para(29314(a,1),205(a,1,3)),rewrite([6(2),25677(5),205(2),19(2),6(5)]),flip(a)]. given #508 (T,wt=23): 29870 f(f(x,y,z),f(y,u,z),f(x,y,u)) = f(x,y,f(y,u,z)). [para(29315(a,1),922(a,2)),rewrite([6(3),5(4),6(6),1253(9),6(5)])]. given #509 (T,wt=23): 29948 f(f(x,y,z),f(x,u,y),f(u,y,z)) = f(u,y,f(x,y,z)). [para(29316(a,1),19(a,1,3)),rewrite([29259(5),29316(8)])]. given #510 (A,wt=31): 221 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(29(a,1),8(a,2,3))]. given #511 (T,wt=24): 18876 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(z,y,f(x,y,v))). [para(854(a,1),5(a,2)),rewrite([6(3),5(4,R),6(4)])]. given #512 (T,wt=24): 19226 f(x,f(y,z,f(y,x,u)),f(x,u,v)) = f(y,x,f(x,u,v)). [para(872(a,1),220(a,2,3)),rewrite([5(1,R),6(1),5(2,R),6(2),6(3),5(4,R),1072(6),5(3,R),6(3),6(4),5(6,R)]),flip(a)]. given #513 (T,wt=24): 19355 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,u,w))). [para(80(a,1),19086(a,1,2)),rewrite([5(5,R),14606(5),1072(5),20(3),16426(6)]),flip(a)]. given #514 (T,wt=24): 19577 f(x,y,f(z,u,f(v,u,w))) = f(x,y,f(v,u,f(z,u,w))). [para(72(a,1),1037(a,2,3,3)),rewrite([16879(7),4249(6),5(3,R),6(3),1634(5),6(8),16882(8)])]. given #515 (A,wt=31): 222 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),29(a,1,3,3))]. given #516 (T,wt=24): 19587 f(x,y,f(x,f(z,y,u),f(x,v,u))) = f(x,v,f(x,y,u)). [para(19(a,1),1062(a,1,3,3)),rewrite([15(3),15317(7),16397(6),6(4)]),flip(a)]. given #517 (T,wt=21): 30451 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(19587(a,1),847(a,1)),rewrite([6(2),813(3),5(3)]),flip(a)]. given #518 (T,wt=24): 19632 f(x,y,f(x,f(z,u,y),f(x,v,u))) = f(x,v,f(x,u,y)). [para(75(a,2),1062(a,2,3)),rewrite([20(3),15(3),15317(7),50(7)]),flip(a)]. given #519 (T,wt=24): 19785 f(x,f(y,z,u),f(x,v,f(v,y,z))) = f(x,v,f(y,z,u)). [para(1136(a,1),5(a,1)),rewrite([5(3),5(6,R)]),flip(a)]. given #520 (A,wt=31): 223 f(x,y,f(z,u,f(x,u,f(z,v,w)))) = f(x,u,f(x,y,f(z,v,f(z,u,w)))). [para(8(a,1),29(a,2,3,3))]. given #521 (T,wt=24): 19793 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,u,v))). [para(17(a,1),1136(a,2,3)),rewrite([1136(5)])]. given #522 (T,wt=24): 19799 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,w,u))). [para(30(a,1),1136(a,1,2)),rewrite([3153(5)]),flip(a)]. given #523 (T,wt=24): 19829 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,v,u))). [para(474(a,1),1136(a,2,3)),rewrite([5(1),5(1),22(3),3529(5),6(4),5(5,R),6(5)])]. given #524 (T,wt=24): 19843 f(x,f(y,z,u),f(y,v,f(x,z,v))) = f(x,v,f(y,z,u)). [para(897(a,1),1136(a,1,3))]. given #525 (A,wt=31): 225 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),29(a,1,3,3))]. given #526 (T,wt=24): 19852 f(x,f(y,z,u),f(z,v,f(x,y,v))) = f(x,v,f(y,z,u)). [para(1149(a,1),1136(a,1,3))]. given #527 (T,wt=24): 19904 f(x,y,f(x,f(z,u,v),f(z,u,y))) = f(x,y,f(z,u,v)). [para(1136(a,1),859(a,2)),rewrite([6(9),5(10,R),6(10),4944(12)])]. given #528 (T,wt=24): 19990 f(x,f(y,z,u),f(u,x,f(y,z,v))) = f(u,x,f(y,z,v)). [para(1136(a,1),168(a,1,3)),rewrite([5(3),5(5,R),6(5),15(6),5(5)]),flip(a)]. given #529 (T,wt=21): 30870 f(x,f(y,z,x),f(y,u,f(y,v,z))) = f(y,z,x). [para(19086(a,1),19990(a,1,3)),rewrite([5(1),5(3,R),15(3),5(3),6(3),5(4,R),5(5),5(7),6(7),12886(8)])]. given #530 (A,wt=31): 226 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),29(a,2,3,3))]. given #531 (T,wt=24): 20063 f(f(x,y,z),f(x,u,y),f(x,u,f(u,y,v))) = f(x,u,y). [para(1138(a,1),5(a,1)),flip(a)]. given #532 (T,wt=24): 20064 f(f(x,y,z),f(y,z,f(x,z,u)),f(x,y,v)) = f(x,y,z). [para(5(a,1),1138(a,1,1)),rewrite([5(2,R),6(2),5(4,R),6(4),5(6)])]. given #533 (T,wt=24): 20065 f(f(x,y,z),f(x,z,f(x,y,u)),f(y,z,v)) = f(x,y,z). [para(5(a,2),1138(a,1,1)),rewrite([5(3,R),6(3),5(4,R),6(4),5(6),5(6)])]. given #534 (T,wt=24): 20066 f(f(x,y,z),f(x,z,f(y,z,u)),f(x,y,v)) = f(x,y,z). [para(6(a,1),1138(a,1,1)),rewrite([5(2,R),6(2),6(6)])]. given #535 (A,wt=31): 227 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(29(a,2),17(a,1,3)),rewrite([57(8)])]. Low Water (keep, True_semantics): wt=37 given #536 (T,wt=24): 20074 f(f(x,y,z),f(y,z,f(x,y,u)),f(x,z,v)) = f(x,y,z). [para(16(a,2),1138(a,1,2))]. given #537 (T,wt=24): 20469 f(x,f(y,z,u),f(v,y,f(x,v,z))) = f(x,v,f(y,z,u)). [para(1148(a,1),4461(a,2)),rewrite([5(3),5(4),6(5),5(6),5(9),15317(11),15352(11)])]. given #538 (T,wt=24): 20483 f(x,f(y,z,u),f(y,v,f(z,v,x))) = f(v,x,f(y,z,u)). [para(1148(a,1),2013(a,2)),rewrite([5(3,R),6(3),5(5,R),6(5),6(8),5(9,R),6(9),16597(11),5(6,R),6(6)])]. given #539 (T,wt=24): 20502 f(x,f(y,z,x),f(u,x,f(y,z,v))) = f(u,x,f(y,z,x)). [para(1148(a,1),74(a,2,3)),rewrite([5(4,R),922(4),19(4),5(6,R),6(6)]),flip(a)]. given #540 (A,wt=31): 228 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),29(a,2,3,3))]. given #541 (T,wt=24): 20583 f(x,f(y,z,u),f(u,x,v)) = f(x,v,f(z,u,f(y,u,x))). [para(1176(a,1),5(a,2)),rewrite([5(2,R),6(2),5(3),5(4),5(4)])]. given #542 (T,wt=24): 20585 f(x,f(y,z,u),f(x,v,u)) = f(x,v,f(z,u,f(x,y,u))). [para(1176(a,2),20(a,1,3)),rewrite([6(2),22(4)])]. given #543 (T,wt=24): 20653 f(x,y,f(z,u,f(x,v,u))) = f(x,y,f(v,u,f(x,z,u))). [para(1176(a,1),1072(a,2)),rewrite([5(5,R),15317(6),16529(7)])]. given #544 (T,wt=24): 20775 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,u,f(x,y,z))). [para(1176(a,1),872(a,2)),rewrite([5(1,R),6(1),5(2),6(3),19692(5),822(5),6(4),5(5,R),6(5)])]. given #545 (A,wt=38): 229 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(29(a,1),18(a,2,3,3))]. given #546 (T,wt=24): 20789 f(f(x,y,z),f(z,u,f(x,y,z)),f(x,y,v)) = f(x,y,z). [para(1179(a,1),5(a,1)),rewrite([5(6)]),flip(a)]. given #547 (T,wt=24): 20811 f(f(x,y,z),f(x,y,u),f(x,u,f(y,u,v))) = f(x,y,u). [para(874(a,1),1179(a,1,3))]. given #548 (T,wt=24): 20815 f(f(x,y,z),f(x,y,u),f(y,u,f(x,u,v))) = f(x,y,u). [para(933(a,1),1179(a,1,3))]. given #549 (T,wt=24): 21153 f(x,f(y,z,u),f(v,x,f(x,z,u))) = f(v,x,f(x,z,u)). [para(1254(a,1),74(a,1,3)),rewrite([15690(3),15690(6)]),flip(a)]. given #550 (A,wt=38): 230 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(29(a,2),18(a,1,3,3))]. given #551 (T,wt=18): 31526 f(x,y,f(z,y,f(u,x,z))) = f(x,z,y). [para(21153(a,1),71(a,2)),rewrite([5(3),5(4,R),6(4),5(5,R),6(5),24356(5),5(5),5(5),5(6,R),3270(6)])]. given #552 (T,wt=24): 21167 f(x,f(y,z,u),f(v,x,f(v,z,u))) = f(v,x,f(y,z,u)). [para(1254(a,1),220(a,2,3)),rewrite([1633(5),19(4)]),flip(a)]. given #553 (T,wt=24): 21190 f(x,f(y,z,u),f(u,x,f(z,x,v))) = f(x,v,f(z,u,x)). [para(1286(a,1),5(a,2)),rewrite([5(2,R),6(2),5(3,R),6(3),5(4),5(5),5(5)])]. given #554 (T,wt=24): 21278 f(x,f(y,z,f(y,u,x)),f(v,u,x)) = f(y,x,f(v,u,x)). [para(1286(a,1),74(a,2,3)),rewrite([5(4,R),1669(6),5(6,R)]),flip(a)]. given #555 (A,wt=38): 231 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),29(a,1,3,3))]. given #556 (T,wt=24): 21313 f(x,f(y,z,x),f(u,v,f(u,z,x))) = f(u,x,f(y,z,x)). [para(1286(a,1),220(a,2,3)),rewrite([803(6)]),flip(a)]. given #557 (T,wt=22): 32049 f(x,y,f(z,x,f(z,u,f(z,v,y)))) = f(z,x,y). [para(19226(a,1),21313(a,2)),rewrite([1713(5),1713(6),31597(6),5(4,R),15317(4),51(4),1713(7),20(6)])]. given #558 (T,wt=24): 21562 f(x,f(y,z,u),f(x,v,f(v,z,u))) = f(x,v,f(y,z,u)). [para(1329(a,1),5(a,1)),rewrite([5(3),5(6,R)]),flip(a)]. given #559 (T,wt=24): 21598 f(x,f(y,z,u),f(z,v,f(x,u,v))) = f(x,v,f(y,z,u)). [para(897(a,1),1329(a,1,3))]. given #560 (A,wt=38): 232 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),29(a,2,3,3))]. given #561 (T,wt=24): 21600 f(x,f(y,z,u),f(u,v,f(x,z,v))) = f(x,v,f(y,z,u)). [para(1149(a,1),1329(a,1,3))]. given #562 (T,wt=24): 21667 f(x,y,f(x,f(z,u,v),f(u,v,y))) = f(x,y,f(z,u,v)). [para(1329(a,1),130(a,2,3)),rewrite([22(6),19(8)])]. given #563 (T,wt=24): 21698 f(x,f(y,z,u),f(x,u,f(v,y,z))) = f(x,u,f(v,y,z)). [para(1329(a,1),1062(a,2,3)),rewrite([19(5),1329(4)]),flip(a)]. given #564 (T,wt=24): 21804 f(x,f(y,z,u),f(y,x,f(z,u,v))) = f(y,x,f(z,u,v)). [para(1341(a,1),168(a,1,3)),rewrite([5(3,R),6(3),5(5,R),6(5),15(6),5(5,R),6(5)]),flip(a)]. given #565 (A,wt=38): 233 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),29(a,1,3,3))]. given #566 (T,wt=24): 22135 f(f(x,y,z),f(y,z,u),f(y,u,f(z,u,v))) = f(y,z,u). [para(874(a,1),1344(a,1,3))]. given #567 (T,wt=24): 22136 f(f(x,y,z),f(y,z,u),f(z,u,f(y,u,v))) = f(y,z,u). [para(933(a,1),1344(a,1,3))]. given #568 (T,wt=24): 22164 f(x,f(y,z,x),f(u,f(v,y,z),f(y,z,x))) = f(y,z,x). [para(1344(a,1),16396(a,2)),rewrite([5(6,R),10036(8)])]. given #569 (T,wt=21): 32386 f(x,y,f(z,y,f(u,x,y))) = f(z,y,f(u,x,y)). [para(1051(a,1),22164(a,1,3)),rewrite([6(2),6(4),6(7),5(8),4(8),6(4)]),flip(a)]. given #570 (A,wt=38): 234 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),29(a,2,3,3))]. given #571 (T,wt=22): 32381 f(x,y,f(z,u,f(x,u,f(v,u,y)))) = f(x,u,y). [para(22164(a,1),6(a,2)),rewrite([5(2),5(4),6(5),15317(5),25551(5),5(3,R),6(3),5(5)])]. given #572 (T,wt=24): 22281 f(f(x,y,z),f(x,y,u),f(y,z,f(x,z,v))) = f(x,y,z). [para(5(a,1),1393(a,1,1)),rewrite([5(2,R),6(2),5(3,R),6(3),5(6)])]. given #573 (T,wt=24): 22282 f(f(x,y,z),f(y,z,u),f(x,z,f(x,y,v))) = f(x,y,z). [para(5(a,2),1393(a,1,1)),rewrite([5(2,R),6(2),5(4,R),6(4),5(6),5(6)])]. given #574 (T,wt=24): 22283 f(f(x,y,z),f(x,y,u),f(x,z,f(y,z,v))) = f(x,y,z). [para(6(a,1),1393(a,1,1)),rewrite([5(3,R),6(3),6(6)])]. given #575 (A,wt=31): 235 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(29(a,1),24(a,2,3)),rewrite([5(3,R),6(3),5(8,R),6(8)]),flip(a)]. given #576 (T,wt=24): 22289 f(f(x,y,z),f(x,z,u),f(y,z,f(x,y,v))) = f(x,y,z). [para(16(a,2),1393(a,1,3))]. given #577 (T,wt=24): 22466 f(f(x,y,z),f(x,y,u),f(v,z,f(x,y,z))) = f(x,y,z). [para(1394(a,1),8713(a,1,3)),rewrite([15(3),5(5,R),6(5)]),flip(a)]. given #578 (T,wt=24): 22576 f(x,f(y,z,u),f(v,z,f(x,v,u))) = f(x,v,f(y,z,u)). [para(1404(a,1),54(a,2,3)),rewrite([95(5),20(7)])]. given #579 (T,wt=24): 23006 f(f(x,y,z),f(x,z,u),f(v,y,f(x,y,z))) = f(x,y,z). [para(1557(a,1),8713(a,1,3)),rewrite([15(3),5(5,R),6(5)]),flip(a)]. given #580 (A,wt=31): 238 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(30(a,2),29(a,2,3,3))]. given #581 (T,wt=24): 23075 f(x,f(y,z,u),f(v,x,z)) = f(v,x,f(z,u,f(x,y,z))). [para(321(a,2),1630(a,1,3)),rewrite([6(3),3998(4),17148(5),6(5)])]. given #582 (T,wt=24): 23093 f(x,f(y,z,u),f(v,y,f(v,x,z))) = f(v,x,f(y,z,u)). [para(1630(a,1),131(a,2,3)),rewrite([103(5),20(7)])]. given #583 (T,wt=24): 23175 f(x,f(y,z,u),f(v,z,f(v,x,u))) = f(v,x,f(y,z,u)). [para(1633(a,1),131(a,2,3)),rewrite([103(5),20(7)])]. given #584 (T,wt=24): 23764 f(x,f(y,z,u),f(v,x,u)) = f(v,x,f(y,u,f(x,z,u))). [para(321(a,2),1766(a,1,3)),rewrite([13392(5)])]. given #585 (A,wt=35): 243 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),29(a,1,3,3)),rewrite([6(1),6(5)]),flip(a)]. given #586 (T,wt=20): 32787 f(x,f(y,z,x),f(y,u,x)) = f(y,x,f(u,z,x)). [para(23764(a,2),828(a,1)),rewrite([5(2,R),15(2),6(2),5(4)]),flip(a)]. given #587 (T,wt=24): 23777 f(x,f(y,z,u),f(v,x,u)) = f(v,x,f(z,u,f(x,y,u))). [para(1176(a,2),1766(a,1,3)),rewrite([13392(5)])]. given #588 (T,wt=24): 23813 f(x,y,f(z,u,f(v,w,z))) = f(x,y,f(v,z,f(w,z,u))). [para(828(a,1),1769(a,2,3)),rewrite([5(4,R),6(4),7681(6),5(4)]),flip(a)]. given #589 (T,wt=24): 23815 f(x,y,f(z,u,f(v,w,u))) = f(x,y,f(v,u,f(z,w,u))). [para(874(a,1),1769(a,2,3)),rewrite([5(4,R),6(4),7681(6),5(4)])]. given #590 (A,wt=35): 246 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(28(a,1),29(a,1,3,3)),flip(a)]. given #591 (T,wt=24): 23817 f(x,y,f(z,u,f(v,w,u))) = f(x,y,f(w,u,f(z,v,u))). [para(933(a,1),1769(a,2,3)),rewrite([5(4,R),6(4),7681(6),5(4)])]. given #592 (T,wt=24): 23862 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,u,f(x,y,z))). [para(1037(a,1),1769(a,1,3)),rewrite([6(1),5(3),6(3),2997(5),20(5),17022(5),6(4),5(5,R),6(5)])]. given #593 (T,wt=24): 23874 f(x,f(y,z,u),f(v,x,f(y,z,x))) = f(v,x,f(y,z,x)). [para(1073(a,1),1906(a,1,3,3)),rewrite([15(6)]),flip(a)]. given #594 (T,wt=24): 23877 f(x,f(y,z,u),f(v,x,f(z,u,x))) = f(v,x,f(z,u,x)). [para(3270(a,1),1906(a,1,3,3)),rewrite([15(6)]),flip(a)]. given #595 (A,wt=31): 250 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),29(a,2,3,3)),rewrite([5(2,R),6(2),247(5),5(6,R),6(6)])]. given #596 (T,wt=24): 23881 f(x,f(y,z,u),f(v,x,f(y,u,x))) = f(v,x,f(y,u,x)). [para(7301(a,1),1906(a,1,3,3)),rewrite([15(6)]),flip(a)]. given #597 (T,wt=24): 23891 f(x,f(y,z,u),f(v,x,f(y,z,v))) = f(v,x,f(y,z,u)). [para(1766(a,1),1906(a,1,3)),rewrite([5(2),5(2),922(6),5(4),5(4)]),flip(a)]. given #598 (T,wt=24): 23892 f(x,f(y,z,u),f(v,x,f(z,u,v))) = f(v,x,f(y,z,u)). [para(1769(a,1),1906(a,1,3)),rewrite([5(2),5(2),922(6),5(4),5(4)]),flip(a)]. given #599 (T,wt=24): 23899 f(f(x,y,z),f(z,u,f(x,y,z)),f(v,x,y)) = f(x,y,z). [para(1329(a,1),1987(a,1,3)),rewrite([5(3,R),3270(3),6(3),5(6,R),15(6),5(8,R),3270(8)])]. given #600 (A,wt=38): 251 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(29(a,1),25(a,2,3,3))]. given #601 (T,wt=24): 23908 f(f(x,y,z),f(u,x,y),f(z,v,f(x,y,z))) = f(x,y,z). [para(1329(a,1),1998(a,1,2)),rewrite([5(3,R),3270(3),5(4,R),15(4),6(4),5(8,R),3270(8)])]. given #602 (T,wt=24): 23940 f(x,f(y,z,u),f(v,x,f(x,y,u))) = f(v,x,f(x,y,u)). [para(2175(a,1),74(a,1,3)),rewrite([15715(3),15715(6)]),flip(a)]. given #603 (T,wt=24): 23950 f(x,f(y,z,u),f(v,x,f(v,y,u))) = f(v,x,f(y,z,u)). [para(2175(a,1),220(a,2,3)),rewrite([7671(5),19(4)]),flip(a)]. given #604 (T,wt=24): 24118 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(z,u,v))). [para(4005(a,1),54(a,2,3)),rewrite([6(2),5(3,R),6(3),21598(4),5(4),5(4)]),flip(a)]. Low Water (displace, True_semantics): id=20570, wt=43 given #605 (A,wt=38): 253 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(25(a,1),29(a,1,3,3))]. given #606 (T,wt=23): 33126 f(x,f(y,z,u),f(x,v,y)) = f(x,f(v,z,u),f(x,v,y)). [para(24118(a,1),1286(a,1,3)),rewrite([27477(5),5(4)]),flip(a)]. Low Water (displace, True_semantics): id=21188, wt=42 Low Water (displace, True_semantics): id=21984, wt=41 Low Water (displace, True_semantics): id=22752, wt=40 given #607 (T,wt=23): 33212 f(x,f(y,z,u),f(x,v,u)) = f(x,f(v,y,z),f(x,v,u)). [para(33126(a,1),5(a,1)),rewrite([5(5),5(5),5(6,R)]),flip(a)]. Low Water (displace, True_semantics): id=27037, wt=39 given #608 (T,wt=23): 33213 f(x,f(y,z,u),f(v,x,u)) = f(x,f(v,y,z),f(v,x,u)). [para(33126(a,1),5(a,2)),rewrite([5(2),5(3),5(4),5(4),5(5)]),flip(a)]. Low Water (displace, True_semantics): id=27383, wt=38 given #609 (T,wt=23): 33214 f(x,f(y,z,u),f(x,v,u)) = f(x,f(y,v,z),f(x,v,u)). [para(5(a,1),33126(a,1,2)),rewrite([6(2),5(4),6(4),6(5)]),flip(a)]. given #610 (A,wt=38): 255 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(25(a,1),29(a,2,3,3))]. given #611 (T,wt=23): 33215 f(x,f(y,z,u),f(x,v,u)) = f(x,f(y,z,v),f(x,v,u)). [para(5(a,2),33126(a,1,2)),rewrite([6(2),5(4),5(4),6(5)]),flip(a)]. given #612 (T,wt=23): 33578 f(x,f(y,z,u),f(v,x,u)) = f(x,f(y,z,v),f(v,x,u)). [para(33212(a,1),5(a,2)),rewrite([5(2),5(3),5(4),5(4),5(5)]),flip(a)]. given #613 (T,wt=23): 33767 f(x,f(y,z,u),f(v,u,x)) = f(x,f(y,z,v),f(v,u,x)). [para(33213(a,1),5(a,2)),rewrite([5(2),5(3),5(4),5(4),5(5)]),flip(a)]. given #614 (T,wt=23): 33776 f(x,f(y,z,u),f(v,x,y)) = f(x,f(v,z,u),f(v,x,y)). [para(33213(a,1),922(a,2)),rewrite([5(2),6(3),5(4),12860(7)])]. given #615 (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(25(a,2),29(a,1,3,3))]. given #616 (T,wt=23): 33849 f(x,f(y,z,u),f(v,x,u)) = f(x,f(y,v,z),f(v,x,u)). [para(33214(a,2),5(a,2)),rewrite([5(2,R),6(2),5(3),5(5,R),6(5)]),flip(a)]. given #617 (T,wt=23): 33861 f(x,f(y,z,u),f(x,v,z)) = f(x,f(v,y,u),f(x,v,z)). [para(33214(a,1),21(a,1,3)),rewrite([6(2),22(4),5(4),6(5)])]. given #618 (T,wt=23): 34028 f(x,f(y,z,u),f(v,y,x)) = f(x,f(v,z,u),f(v,y,x)). [para(33767(a,1),922(a,2)),rewrite([5(2),6(3),5(4),12860(7),5(4)])]. given #619 (T,wt=23): 34063 f(x,f(y,z,u),f(v,u,x)) = f(x,f(v,y,z),f(v,u,x)). [para(33776(a,1),5(a,2)),rewrite([5(2),5(3),5(4),5(4),5(5)]),flip(a)]. given #620 (A,wt=38): 258 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(25(a,2),29(a,2,3,3))]. given #621 (T,wt=23): 34128 f(x,f(y,z,u),f(x,v,z)) = f(x,f(y,v,u),f(x,v,z)). [para(803(a,1),33861(a,1,3)),rewrite([6(3),6(5),15317(5),28467(5),6(1),5(4,R),6(4),803(7)]),flip(a)]. given #622 (T,wt=24): 24183 f(x,y,f(x,z,f(y,u,v))) = f(x,z,f(x,y,f(z,u,v))). [back_rewrite(7713),rewrite([24159(4),24159(7)])]. given #623 (T,wt=24): 24185 f(x,y,f(x,f(z,u,v),f(z,v,y))) = f(x,y,f(z,u,v)). [para(5019(a,1),6(a,2)),rewrite([5(2),5(2),6(4)])]. given #624 (T,wt=24): 24186 f(x,f(y,z,u),f(x,v,f(v,y,u))) = f(x,v,f(y,z,u)). [para(5019(a,1),8(a,1)),flip(a)]. given #625 (A,wt=44): 259 f(x,f(y,z,f(u,v,f(x,v,w))),f(y,z,f(x,v,f(x,y,f(u,v,w))))) = f(x,y,f(y,z,f(u,v,f(x,v,w)))). [para(29(a,1),27(a,1,3,3))]. given #626 (T,wt=24): 24194 f(x,f(y,z,u),f(y,v,f(x,u,v))) = f(x,v,f(y,z,u)). [para(5019(a,1),25(a,2)),rewrite([6(2),5(3,R),6(3)])]. given #627 (T,wt=24): 24211 f(x,f(y,z,u),f(x,u,f(y,v,z))) = f(x,u,f(y,v,z)). [para(5019(a,1),910(a,1,3,3)),rewrite([5(2),5(2),15317(7),1700(7),5(6),5(6),24185(8)])]. given #628 (T,wt=24): 24214 f(x,f(y,z,u),f(v,y,f(x,v,u))) = f(x,v,f(y,z,u)). [para(5019(a,1),54(a,2,3)),rewrite([95(5),20(7)])]. given #629 (T,wt=24): 24236 f(x,f(y,z,u),f(u,v,f(x,y,v))) = f(x,v,f(y,z,u)). [para(5019(a,1),82(a,2)),rewrite([6(2),5(3,R),6(3)])]. given #630 (A,wt=38): 265 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(29(a,1),29(a,2,3,3))]. given #631 (T,wt=24): 24263 f(x,y,f(x,f(y,z,u),f(z,v,u))) = f(x,y,f(z,v,u)). [para(5019(a,1),1105(a,2,3)),rewrite([5(4,R),19(5),5(8,R),6(8),19(8)])]. given #632 (T,wt=24): 24273 f(x,f(y,z,x),f(u,f(y,v,z),f(y,z,x))) = f(y,z,x). [para(5019(a,1),1478(a,1,3)),rewrite([5(2),5(2),5(3),5(5),5(5),12860(6),4(6),5(5),6(5),5(7),5(7),12860(8)])]. given #633 (T,wt=24): 24278 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(x,y,f(z,y,v))). [para(5247(a,1),5(a,2)),rewrite([6(3),5(5,R),6(5)])]. given #634 (T,wt=24): 24307 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(z,y,f(x,y,u))). [para(5455(a,1),5(a,2)),rewrite([6(3),5(4,R),6(4)])]. given #635 (A,wt=31): 266 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(32(a,2),8(a,2,3)),flip(a)]. given #636 (T,wt=24): 24319 f(x,y,f(y,z,f(u,y,v))) = f(u,y,f(y,z,f(x,y,v))). [para(5459(a,1),169(a,2)),rewrite([15317(5),16964(6)])]. given #637 (T,wt=24): 24322 f(x,y,f(z,y,f(y,u,v))) = f(z,y,f(y,v,f(x,y,u))). [para(5496(a,1),5(a,2)),rewrite([6(3),5(4,R),6(4)])]. given #638 (T,wt=24): 24348 f(x,y,f(z,y,f(y,u,v))) = f(y,u,f(y,v,f(x,z,y))). [para(5502(a,1),5(a,2)),rewrite([6(3),5(4)])]. given #639 (T,wt=24): 24378 f(x,y,f(x,f(z,u,y),f(x,v,z))) = f(x,v,f(x,z,y)). [para(321(a,2),5502(a,1,3)),rewrite([5(2),16415(3),5(4),5(4)]),flip(a)]. given #640 (A,wt=31): 268 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(32(a,1),17(a,1,3)),rewrite([57(8)])]. given #641 (T,wt=24): 24433 f(x,y,f(z,u,f(z,y,v))) = f(z,y,f(x,y,f(z,v,u))). [para(6719(a,2),5(a,2)),rewrite([6(3),5(4,R),6(4)]),flip(a)]. given #642 (T,wt=24): 24563 f(f(x,y,z),f(z,u,f(x,y,z)),f(x,v,y)) = f(x,y,z). [para(7307(a,1),1987(a,1,3)),rewrite([5(3,R),7301(3),6(3),5(6,R),15(6),5(8,R),7301(8)])]. given #643 (T,wt=24): 24564 f(f(x,y,z),f(x,u,y),f(z,v,f(x,y,z))) = f(x,y,z). [para(7307(a,1),1998(a,1,2)),rewrite([5(3,R),7301(3),5(4,R),15(4),6(4),5(8,R),7301(8)])]. given #644 (T,wt=24): 24599 f(f(x,y,z),f(x,z,u),f(x,u,f(z,u,v))) = f(x,z,u). [para(874(a,1),7334(a,1,3))]. given #645 (A,wt=38): 269 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(32(a,1),18(a,1,3,3))]. given #646 (T,wt=24): 24600 f(f(x,y,z),f(x,z,u),f(z,u,f(x,u,v))) = f(x,z,u). [para(933(a,1),7334(a,1,3))]. given #647 (T,wt=24): 24660 f(x,y,f(y,z,f(u,y,v))) = f(u,y,f(y,v,f(x,y,z))). [para(7343(a,1),169(a,2)),rewrite([15317(5),16964(6)])]. given #648 (T,wt=24): 24743 f(x,f(y,z,u),f(v,y,f(v,x,u))) = f(v,x,f(y,z,u)). [para(7671(a,1),131(a,2,3)),rewrite([103(5),20(7)])]. given #649 (T,wt=24): 24749 f(x,f(y,z,u),f(v,x,f(y,u,v))) = f(v,x,f(y,z,u)). [para(7671(a,1),7405(a,1,3)),rewrite([5(2),5(2),922(6),5(4),5(4)]),flip(a)]. given #650 (A,wt=38): 270 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(32(a,2),18(a,2,3,3))]. given #651 (T,wt=24): 24778 f(x,f(y,z,u),f(z,v,x)) = f(v,x,f(y,z,f(z,u,x))). [para(7761(a,1),5(a,2)),rewrite([5(2),5(3),5(4),5(4)])]. given #652 (T,wt=24): 24890 f(x,f(y,z,u),f(v,z,x)) = f(v,x,f(y,z,f(z,u,x))). [para(8102(a,2),5(a,2)),rewrite([6(3),5(5)]),flip(a)]. given #653 (T,wt=24): 24898 f(x,y,f(z,u,f(u,v,y))) = f(x,y,f(u,y,f(z,u,v))). [para(8102(a,2),205(a,1,3)),rewrite([5(4),9850(6),5(6,R),6(6)]),flip(a)]. given #654 (T,wt=24): 24984 f(x,f(y,z,u),f(z,x,f(y,u,v))) = f(z,x,f(y,u,v)). [para(8330(a,1),168(a,1,3)),rewrite([5(3,R),6(3),5(5,R),6(5),15(6),5(5,R),6(5)]),flip(a)]. given #655 (A,wt=31): 271 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(32(a,2),18(a,2,3)),flip(a)]. given #656 (T,wt=24): 25022 f(x,y,f(z,u,f(z,v,x))) = f(z,x,f(x,y,f(z,v,u))). [para(9417(a,1),2861(a,2)),rewrite([5(1,R),6(1),5(3,R),6(3),5(5,R),6(5),5(7,R),6(7),6889(8),5(4),5(4),5(6,R),6(6)]),flip(a)]. given #657 (T,wt=24): 25147 f(x,f(y,z,f(z,x,u)),f(y,v,f(y,z,x))) = f(y,z,x). [para(6694(a,1),9988(a,2)),rewrite([5(1),5(3),5(6),5(8),4(8),5(6),19226(6),5(5,R),5(6),5(8),5(8),1713(8),5(7,R),6(7),20(7)])]. given #658 (T,wt=24): 25161 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(y,u,f(x,z,y))). [para(10617(a,1),5(a,2)),rewrite([6(3),5(4)])]. given #659 (T,wt=24): 25169 f(x,f(y,z,u),f(x,u,f(x,v,y))) = f(x,v,f(x,y,u)). [para(321(a,2),10617(a,1,3)),rewrite([5(2),16415(3),5(4),5(4)]),flip(a)]. given #660 (A,wt=38): 272 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),32(a,2,3,3)),rewrite([57(4)])]. given #661 (T,wt=24): 25201 f(x,y,f(z,y,f(y,u,v))) = f(y,v,f(x,y,f(z,y,u))). [para(10630(a,1),5(a,2)),rewrite([6(3),5(5,R),6(5)])]. given #662 (T,wt=24): 25252 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(z,u,f(x,y,z))). [para(11098(a,2),1404(a,2)),rewrite([19722(5),20(5),822(5)])]. given #663 (T,wt=24): 25344 f(x,f(y,z,u),f(y,x,f(x,z,v))) = f(x,v,f(y,x,z)). [para(866(a,1),13409(a,1,3,3)),rewrite([5(3,R),6(3),6(4),25200(6),5(5,R),6(5),25078(6)]),flip(a)]. given #664 (T,wt=24): 25362 f(x,y,f(z,x,f(u,x,v))) = f(u,x,f(x,y,f(z,x,v))). [para(5247(a,1),13409(a,2)),rewrite([5(4),15317(5),16964(6),5(5,R),6(5)]),flip(a)]. given #665 (A,wt=38): 273 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),32(a,2,3,3)),rewrite([57(4),6(6)])]. given #666 (T,wt=24): 25363 f(x,y,f(z,x,f(u,x,v))) = f(z,x,f(x,v,f(u,x,y))). [para(5455(a,1),13409(a,2)),rewrite([5(4),15317(5),16964(6),5(4,R),6(4)]),flip(a)]. given #667 (T,wt=24): 25365 f(x,y,f(y,z,f(u,y,v))) = f(y,z,f(y,v,f(u,x,y))). [para(5502(a,1),13409(a,2)),rewrite([5(4),15317(5),16964(6),5(4)])]. given #668 (T,wt=24): 25367 f(x,y,f(y,z,f(u,y,v))) = f(y,v,f(y,z,f(u,x,y))). [para(10617(a,1),13409(a,2)),rewrite([5(4),15317(5),16964(6),5(4)])]. given #669 (T,wt=24): 25368 f(x,y,f(z,x,f(u,x,v))) = f(u,x,f(x,v,f(z,x,y))). [para(10630(a,1),13409(a,2)),rewrite([5(4),15317(5),16964(6),5(5,R),6(5)]),flip(a)]. given #670 (A,wt=31): 274 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(18(a,2),32(a,2,3)),rewrite([57(3),6(1)]),flip(a)]. given #671 (T,wt=24): 25369 f(x,y,f(z,u,f(y,v,u))) = f(x,y,f(v,u,f(y,z,u))). [para(5(a,2),14290(a,1,3)),rewrite([6(2),6(4)])]. given #672 (T,wt=24): 25382 f(x,y,f(z,u,f(v,z,x))) = f(z,x,f(x,y,f(v,z,u))). [para(14290(a,2),2861(a,2)),rewrite([5(1,R),6(1),5(3,R),6(3),5(5,R),6(5),5(7,R),6(7),7856(8),5(4),5(4),5(6,R),6(6)]),flip(a)]. given #673 (T,wt=24): 25418 f(x,f(y,z,u),f(y,v,x)) = f(v,x,f(y,z,f(y,x,u))). [para(15009(a,1),922(a,2)),rewrite([6(3),12860(7),6(4)])]. given #674 (T,wt=24): 25438 f(x,f(y,z,x),f(z,u,v)) = f(y,x,f(z,u,f(z,x,v))). [para(15010(a,2),6(a,2)),rewrite([5(1,R),6(1),6(3),6(4)]),flip(a)]. given #675 (A,wt=31): 275 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(32(a,1),24(a,1,3)),rewrite([5(2,R),6(2),5(8,R),6(8)])]. given #676 (T,wt=24): 25503 f(x,f(y,z,x),f(z,u,v)) = f(z,x,f(y,x,f(z,u,v))). [para(15010(a,2),1329(a,2)),rewrite([5(1,R),6(1),5(3,R),6(3),6(4),19691(6),21644(6),6(4)]),flip(a)]. given #677 (T,wt=24): 25514 f(x,f(y,z,x),f(z,u,v)) = f(y,x,f(z,x,f(z,u,v))). [para(15010(a,2),7307(a,2)),rewrite([5(1,R),6(1),5(3,R),6(3),6(4),20(4),19691(5),14114(5),6(4)]),flip(a)]. given #678 (T,wt=24): 25761 f(x,f(y,z,x),f(x,u,f(v,y,z))) = f(x,u,f(y,z,x)). [back_rewrite(21114),rewrite([25562(9),18417(6),6(3)])]. given #679 (T,wt=24): 25788 f(x,f(y,z,u),f(y,x,f(x,u,v))) = f(x,v,f(y,x,u)). [back_rewrite(25106),rewrite([25676(6),15203(3),19(2)]),flip(a)]. given #680 (A,wt=31): 276 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(32(a,2),24(a,2,3)),rewrite([5(3,R),6(3),5(8,R),6(8)]),flip(a)]. given #681 (T,wt=24): 25803 f(x,f(y,z,f(z,x,u)),f(x,u,v)) = f(x,v,f(z,x,u)). [back_rewrite(12859),rewrite([25676(6),1982(3),19(2)]),flip(a)]. given #682 (T,wt=22): 35183 f(x,y,f(z,u,f(v,z,f(z,x,y)))) = f(z,x,y). [para(25803(a,1),21278(a,2)),rewrite([1982(5),1982(7),5(6),31587(6),73(3),6(8),26355(8),73(7),1982(7)])]. given #683 (T,wt=22): 35190 f(x,y,f(z,u,f(v,z,f(x,y,z)))) = f(x,y,z). [para(5(a,1),35183(a,1,3)),rewrite([5(1),5(1),5(3),5(3),5(5),5(5)])]. given #684 (T,wt=22): 35191 f(x,y,f(z,u,f(v,u,f(x,y,u)))) = f(x,y,u). [para(5(a,2),35183(a,1,3)),rewrite([5(1),5(1),6(3),5(5),5(5)])]. given #685 (A,wt=31): 278 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(32(a,2),30(a,2,3)),rewrite([5(3,R),6(3),57(4),6(5),5(8,R),6(8)])]. given #686 (T,wt=22): 35198 f(x,y,f(z,u,f(v,u,f(x,u,y)))) = f(x,u,y). [para(35183(a,1),21698(a,1,3)),rewrite([5(1,R),6(1),6(3),5(4,R),6(4),6(5),15317(5),33342(5),5(1,R),15(1),19(2),5(2,R),6(2),5(4,R),6(4)]),flip(a)]. given #687 (T,wt=24): 25894 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([868(3),28(3)]),flip(a)]. given #688 (T,wt=24): 26103 f(x,y,f(x,f(y,z,u),f(x,z,v))) = f(x,v,f(x,y,z)). [para(803(a,1),15322(a,2,3)),rewrite([6(3),15317(4)])]. given #689 (T,wt=24): 26112 f(x,y,f(x,f(z,y,u),f(x,z,v))) = f(x,v,f(x,z,y)). [para(812(a,1),15322(a,2,3)),rewrite([6(3),25909(4)])]. given #690 (A,wt=31): 280 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(32(a,2),31(a,2,3)),rewrite([57(4),6(5)])]. given #691 (T,wt=24): 26113 f(x,y,f(x,f(y,z,u),f(x,u,v))) = f(x,v,f(x,y,u)). [para(827(a,1),15322(a,2,3)),rewrite([6(1),6(3),25905(4),6(5)])]. given #692 (T,wt=24): 26115 f(x,y,f(x,f(z,y,u),f(x,u,v))) = f(x,v,f(x,y,u)). [para(1030(a,1),15322(a,2,3)),rewrite([6(3),25909(4)])]. given #693 (T,wt=24): 26221 f(x,f(y,z,u),f(x,y,f(x,z,v))) = f(x,v,f(x,y,z)). [para(15322(a,2),1301(a,1)),rewrite([5(2),5(2),5(6,R),6(6)])]. given #694 (T,wt=24): 26355 f(x,f(y,x,z),f(u,v,w)) = f(x,z,f(y,x,f(u,v,w))). [para(15324(a,2),853(a,2)),rewrite([6(7),25535(8),5(7,R),6(7),25555(8)]),flip(a)]. given #695 (A,wt=31): 283 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(32(a,1),28(a,1,3,3)),rewrite([103(5)])]. given #696 (T,wt=24): 26866 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,u,f(y,z,x))). [para(15657(a,1),319(a,2)),rewrite([5(2,R),6(2),4(4),5(3),6(5),5(6),5(6),15317(8),25562(7),5(5,R),6(5),205(5)])]. given #697 (T,wt=24): 26951 f(x,f(y,z,f(y,u,x)),f(u,x,v)) = f(y,x,f(u,x,v)). [para(15685(a,1),5(a,2)),rewrite([5(1),5(4),5(6,R),6(6)])]. given #698 (T,wt=24): 26952 f(x,f(y,z,u),f(x,y,f(x,u,v))) = f(x,v,f(x,y,u)). [para(15685(a,1),20(a,1,3)),rewrite([5(1),5(1),5(3,R),6(3),25905(5),22(5),5(5),5(5),5(7,R),6(7),25905(8),26113(8)])]. given #699 (T,wt=24): 26992 f(x,f(y,z,f(y,u,x)),f(u,v,f(y,u,x))) = f(y,u,x). [para(15685(a,1),70(a,1)),rewrite([5(1),5(1),5(3),5(3),5(4,R),6(4),4009(5),5(2),5(2),5(4),5(4),5(6,R),6(6),25905(7),6(4),26103(7),5(6,R)]),flip(a)]. given #700 (A,wt=31): 285 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(32(a,1),122(a,1,3,3)),rewrite([5(4,R),6(4),103(5),5(8,R),6(8)])]. given #701 (T,wt=24): 26994 f(x,f(y,z,f(y,x,u)),f(z,v,f(y,z,x))) = f(y,z,x). [para(15685(a,1),70(a,2,3)),rewrite([5(1),5(1),5(3),5(3),5(5),5(5),5(6,R),6(6),1669(7),910(3),5(2),5(2),5(4,R),6(4),5(6,R)]),flip(a)]. given #702 (T,wt=24): 27081 f(x,y,f(y,f(x,z,u),f(y,z,v))) = f(y,v,f(x,y,z)). [para(160(a,1),479(a,2)),rewrite([5(1,R),6(1),6(2),5(6,R),6(6),25174(8)])]. given #703 (T,wt=24): 27487 f(x,f(y,z,u),f(y,x,f(z,x,v))) = f(x,v,f(y,z,x)). [para(15822(a,1),5(a,2)),rewrite([5(2),6(2),5(3,R),6(3),5(4),5(5),5(5),5(6,R),6(6)])]. Low Water (displace, True_semantics): id=32180, wt=37 given #704 (T,wt=24): 27488 f(x,f(y,z,u),f(x,y,f(x,v,z))) = f(x,v,f(x,y,z)). [para(15822(a,1),19(a,1,3)),rewrite([5(1,R),6(1),5(4,R),6(4),15317(5),15317(4),21(3),20(3),22(3),5(4,R),6(4)]),flip(a)]. Low Water (keep, True_semantics): wt=36 given #705 (A,wt=38): 286 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(32(a,1),25(a,1,3,3))]. given #706 (T,wt=24): 27601 f(x,f(y,z,u),f(v,y,f(v,z,x))) = f(v,x,f(y,z,u)). [para(15828(a,1),866(a,2)),rewrite([5(3,R),6(3),5(5,R),6(5),6(7),26355(8),26820(9),5(6,R),6(6)])]. given #707 (T,wt=24): 27610 f(x,f(y,z,u),f(v,z,f(x,v,y))) = f(x,v,f(y,z,u)). [para(15828(a,1),1606(a,2)),rewrite([6(7),25553(9),15317(6),25652(8),1775(5)])]. given #708 (T,wt=24): 27740 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(u,v,z))). [para(15840(a,1),140(a,2,3)),rewrite([6(2),5(3,R),6(3),21772(5),5(4),5(4)])]. given #709 (T,wt=24): 27872 f(x,f(y,z,f(z,u,x)),f(u,x,v)) = f(z,x,f(u,x,v)). [para(15891(a,1),5(a,2)),rewrite([5(1),5(3),5(3),5(4),5(5),5(5),5(6,R),6(6)])]. given #710 (A,wt=38): 287 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(32(a,2),25(a,2,3,3))]. given #711 (T,wt=24): 27897 f(x,f(y,z,f(y,x,u)),f(v,z,f(y,z,x))) = f(y,z,x). [para(15891(a,1),74(a,2,3)),rewrite([5(1),5(1),5(3),5(3),5(5),6(5),1030(5),5(4,R),6(4),25909(5),1667(5),15690(3),5(2),5(2),5(4),6(4),5(6,R)]),flip(a)]. given #712 (T,wt=22): 35624 f(x,y,f(z,u,f(x,z,f(v,y,z)))) = f(x,y,z). [para(27897(a,1),19(a,1,3)),rewrite([5(1),6(1),5(3),6(3),6(4),15317(4),1030(3),20(2),5(2,R),6(2),5(3,R),6(3),5(4),6(4),35578(6),26355(4)]),flip(a)]. given #713 (T,wt=22): 35633 f(x,y,f(x,z,f(y,u,f(v,z,y)))) = f(x,z,y). [para(27897(a,1),7307(a,2)),rewrite([5(1),6(1),5(3,R),6(3),5(4,R),6(4),5(5),6(5),5(6,R),6(6),5(7,R),6(7),1098(9),30641(7),35578(4),5(5),6(5)])]. given #714 (T,wt=24): 27899 f(x,f(y,z,f(u,z,x)),f(u,z,f(u,x,v))) = f(u,z,x). [para(15891(a,1),220(a,2,3)),rewrite([5(1),5(1),5(3),5(3),5(5),1030(5),5(4,R),6(4),25909(5),1667(5),15690(3),5(2),5(2),5(4),6(4)]),flip(a)]. given #715 (A,wt=31): 289 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(25(a,2),32(a,2,3))]. given #716 (T,wt=22): 35662 f(x,y,f(z,u,f(v,z,f(x,z,y)))) = f(x,z,y). [para(27899(a,1),15740(a,1,3)),rewrite([5(1),6(1),5(3,R),6(3),5(4,R),6(4),5(5),5(6),6(6),6(7),15317(7),34333(7),6(3),122(3),5(3,R),6(3),5(5),6(5),5(7,R),6(7),5(8,R),6(8),25909(9),818(9),15690(7)])]. given #717 (T,wt=22): 35670 f(x,y,f(z,y,f(x,u,f(x,v,z)))) = f(x,z,y). [para(15891(a,1),27899(a,1,3)),rewrite([6(1),6(3),5(5),1030(5),6(4),31593(4),6(1),5(2,R),6(2),5(4,R),15(4),5(4,R),15(4),6(4),6(5),5(7),1030(7)])]. given #718 (T,wt=22): 35675 f(x,y,f(z,u,f(u,y,f(u,x,v)))) = f(u,x,y). [para(19843(a,1),27899(a,1,2)),rewrite([5(1,R),6(1),5(3,R),6(3),5(4,R),6(4),15(5),5(4,R),6(4),5(5,R),6(5),6(7),26355(8),7855(7),27831(7),31543(6),26355(4),15317(4),501(4),5(5,R),6(5),5(6,R),6(6),26355(8),73(7),1982(7)])]. given #719 (T,wt=24): 27908 f(x,f(y,z,u),f(z,x,f(y,x,v))) = f(x,v,f(y,z,x)). [para(15892(a,1),5(a,2)),rewrite([5(2),6(2),5(3,R),6(3),5(4),5(5),5(5),5(6,R),6(6)])]. given #720 (A,wt=44): 291 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(32(a,2),27(a,1,3,3))]. given #721 (T,wt=24): 27966 f(x,f(y,z,u),f(u,x,f(y,x,v))) = f(x,v,f(y,u,x)). [para(15977(a,1),5(a,2)),rewrite([5(2,R),6(2),5(3,R),6(3),5(4),5(5),5(5)])]. given #722 (T,wt=24): 27995 f(x,f(y,z,f(y,u,x)),f(u,v,x)) = f(y,x,f(u,v,x)). [para(15977(a,1),74(a,2,3)),rewrite([5(4,R),1669(6),5(6,R)]),flip(a)]. given #723 (T,wt=24): 28002 f(x,y,f(x,f(z,u,y),f(x,z,v))) = f(x,v,f(x,z,y)). [para(15977(a,1),130(a,2,3)),rewrite([22(6),2175(8)])]. given #724 (T,wt=24): 28004 f(x,f(y,z,x),f(u,v,f(u,y,x))) = f(u,x,f(y,z,x)). [para(15977(a,1),220(a,2,3)),rewrite([803(6)]),flip(a)]. given #725 (A,wt=38): 292 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(32(a,1),29(a,1,3,3))]. given #726 (T,wt=24): 28066 f(x,f(y,z,u),f(x,v,f(y,v,z))) = f(x,v,f(y,z,u)). [para(15991(a,1),812(a,2)),rewrite([6(7),25535(8),5(5,R),26355(5),1700(7)])]. given #727 (T,wt=24): 28086 f(x,y,f(x,f(z,y,u),f(z,u,v))) = f(x,y,f(z,u,v)). [para(15991(a,1),130(a,2,3)),rewrite([22(6),15991(8)])]. given #728 (T,wt=24): 28176 f(x,f(y,z,f(z,u,x)),f(z,u,f(u,x,v))) = f(z,u,x). [para(16098(a,1),102(a,1,3)),rewrite([5(1),5(3),5(5),5(5),27831(6),5(5,R),6(5),803(5),5(4),5(4),26355(4),73(3),1982(3),5(2),5(4),5(6),5(6),27831(7)]),flip(a)]. given #729 (T,wt=24): 28216 f(x,f(y,z,u),f(x,y,f(x,v,u))) = f(x,v,f(x,y,u)). [para(16392(a,2),5455(a,1,3)),rewrite([5(2),6(2),16415(3),5(3),5(5,R),6(5)]),flip(a)]. given #730 (A,wt=38): 293 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(32(a,2),29(a,2,3,3))]. given #731 (T,wt=24): 28233 f(x,f(y,z,u),f(z,x,v)) = f(x,v,f(z,u,f(y,z,x))). [para(16393(a,1),5(a,2)),rewrite([5(2,R),6(2),5(3),5(4),5(4)])]. given #732 (T,wt=24): 28527 f(x,y,f(x,f(y,z,u),f(v,x,u))) = f(v,x,f(x,y,u)). [para(6694(a,1),172(a,2,3)),rewrite([6(1),25905(4),6(5),20(8),25905(8),15(9),28(7)])]. given #733 (T,wt=24): 28529 f(x,y,f(x,f(z,y,u),f(v,x,u))) = f(v,x,f(x,y,u)). [para(15887(a,1),172(a,2,3)),rewrite([6(1),25909(4),6(5),20(8),25909(8),15(9),28(7)])]. given #734 (T,wt=24): 28560 f(x,f(y,z,u),f(y,x,v)) = f(x,v,f(y,u,f(y,x,z))). [para(76(a,2),28534(a,2)),rewrite([15317(7),25944(7),5(4,R),6(4),825(6)])]. given #735 (A,wt=38): 295 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(29(a,2),32(a,2,3,3)),rewrite([6(3),57(4)]),flip(a)]. given #736 (T,wt=24): 28566 f(x,f(y,z,u),f(y,x,f(v,z,u))) = f(y,x,f(v,z,u)). [para(1633(a,1),28534(a,2)),rewrite([15317(9),25944(9),5(6,R),6(6),825(8)])]. given #737 (T,wt=24): 28570 f(x,f(y,z,u),f(y,x,f(z,v,u))) = f(y,x,f(z,v,u)). [para(7671(a,1),28534(a,2)),rewrite([15317(9),25944(9),5(6,R),6(6),825(8)])]. given #738 (T,wt=24): 28590 f(x,y,f(x,z,f(u,v,y))) = f(x,z,f(x,y,f(u,z,v))). [para(16554(a,1),77(a,2,3)),rewrite([6(2),24215(5),6(4)]),flip(a)]. given #739 (T,wt=24): 28611 f(x,f(y,z,u),f(v,u,f(x,v,y))) = f(x,v,f(y,z,u)). [para(16554(a,1),16393(a,1)),rewrite([6(4)]),flip(a)]. given #740 (A,wt=38): 296 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(32(a,2),32(a,2,3,3)),rewrite([57(4),6(6)])]. given #741 (T,wt=21): 35925 f(x,f(y,z,f(u,z,v)),f(u,z,x)) = f(u,z,x). [para(28611(a,1),18876(a,1,3)),rewrite([15(4),15(3),5(6),25535(7),29346(7),15(3),5(6,R),6(6),13645(6)]),flip(a)]. given #742 (T,wt=24): 28663 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(z,w,f(v,z,u))). [para(8713(a,1),16636(a,2,3,3)),rewrite([5(1),5(1),5(3),5(3),25538(6),5(2),26355(4),1051(3),5(4),5(4),5(6),5(6),205(9)])]. given #743 (T,wt=24): 28779 f(x,f(y,z,f(y,x,u)),f(x,v,u)) = f(x,u,f(y,x,v)). [para(16651(a,1),220(a,2,3)),rewrite([6(3),5(4,R),25535(5),825(5),5(6,R)]),flip(a)]. given #744 (T,wt=24): 28811 f(x,y,f(x,f(z,y,u),f(v,x,z))) = f(x,y,f(v,x,z)). [para(803(a,1),17148(a,1,3,3)),rewrite([6(2),17148(4),5(3,R),6(3),15317(6)]),flip(a)]. given #745 (A,wt=31): 297 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(32(a,2),32(a,2,3)),rewrite([57(3),6(1)]),flip(a)]. given #746 (T,wt=24): 28816 f(x,f(y,z,u),f(x,u,f(y,x,v))) = f(x,v,f(y,x,u)). [para(17148(a,1),812(a,2)),rewrite([6(7),15317(8),15317(7),16914(9)])]. given #747 (T,wt=24): 28838 f(x,f(y,z,u),f(x,v,f(y,x,u))) = f(x,v,f(y,x,u)). [para(17148(a,1),74(a,2,3)),rewrite([20(5),17148(4)]),flip(a)]. given #748 (T,wt=24): 29030 f(x,y,f(z,u,f(z,v,y))) = f(z,y,f(x,y,f(z,u,v))). [para(18247(a,1),6(a,2)),rewrite([6(3),6(4)])]. given #749 (T,wt=24): 29045 f(x,y,f(z,u,f(z,v,x))) = f(z,x,f(x,y,f(z,u,v))). [para(18247(a,1),922(a,2)),rewrite([5(3,R),6(3),5(6,R),6(6),922(7),6(4),5(5,R),6(5)])]. given #750 (A,wt=31): 299 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),33(a,1,3,3)),flip(a)]. given #751 (T,wt=24): 29432 f(f(x,y,z),f(x,y,u),f(x,u,f(y,z,u))) = f(x,y,u). [para(29279(a,1),70(a,2,3)),rewrite([5(2),5(2),5(3),5(3),5(4),6(4),5(5,R),6(5),16396(5),5(3,R),6(3),5(6),5(6),5(7),5(7),5(9,R),6(9),3521(9)])]. given #752 (T,wt=24): 29531 f(x,y,f(x,f(z,y,u),f(z,x,v))) = f(x,v,f(z,x,y)). [para(813(a,1),29307(a,1,1)),rewrite([5(2),5(2),5(5,R),6(5),29388(6),5(5),5(5),25909(6)]),flip(a)]. given #753 (T,wt=24): 29633 f(x,f(y,z,f(x,u,z)),f(u,z,f(x,v,u))) = f(x,u,z). [para(15891(a,1),187(a,1,3,3)),rewrite([5(1,R),6(1),5(3),1051(3),5(3,R),6(3),5(5),16307(7),18417(5),6(4),15317(4),1030(3),20(2),5(2,R),6(2),5(4,R),6(4),5(6),16047(7)]),flip(a)]. given #754 (T,wt=24): 29678 f(x,f(y,z,u),f(x,v,f(y,x,z))) = f(x,v,f(y,x,z)). [para(1057(a,1),29313(a,1,1)),rewrite([6(3),6(5),922(6),6(5)]),flip(a)]. given #755 (A,wt=38): 300 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(33(a,1),18(a,2,3,3))]. given #756 (T,wt=24): 29683 f(x,f(y,z,f(y,x,u)),f(x,z,v)) = f(x,v,f(y,x,z)). [para(866(a,1),29313(a,1,1)),rewrite([6(5),29381(6),6(7),25174(8)])]. given #757 (T,wt=24): 29711 f(x,y,f(x,f(z,u,y),f(x,u,v))) = f(x,v,f(x,u,y)). [para(1286(a,1),29313(a,2)),rewrite([6(2),6(8),29313(8)])]. given #758 (T,wt=24): 29748 f(x,f(y,z,f(z,x,u)),f(y,x,v)) = f(x,v,f(y,z,x)). [para(803(a,1),29314(a,1,1)),rewrite([6(5),29518(6),803(7)])]. given #759 (T,wt=24): 29758 f(x,f(y,z,f(y,x,u)),f(z,x,v)) = f(x,v,f(y,z,x)). [para(871(a,1),29314(a,1,1)),rewrite([6(5),29536(6),871(7)])]. given #760 (A,wt=31): 301 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(33(a,1),18(a,2,3))]. given #761 (T,wt=24): 29759 f(x,f(y,z,f(u,y,x)),f(u,x,v)) = f(x,v,f(u,y,x)). [para(910(a,1),29314(a,1,1)),rewrite([6(5),29539(6),910(7)])]. given #762 (T,wt=24): 29880 f(x,f(y,z,u),f(x,u,f(v,x,y))) = f(v,x,f(x,y,u)). [para(1030(a,1),29315(a,2,3)),rewrite([6(2),1051(4),6(3),29760(6),6(5)])]. given #763 (T,wt=24): 30069 f(f(x,y,z),f(x,z,u),f(x,u,f(y,z,u))) = f(x,z,u). [para(29318(a,1),16636(a,2,3)),rewrite([5(4),5(4),16396(5),5(9,R),6(9),1073(9)])]. given #764 (T,wt=24): 30158 f(x,y,f(y,z,f(u,y,v))) = f(y,z,f(y,v,f(x,u,y))). [para(145(a,1),29495(a,2)),rewrite([5(3,R),6(3),20(4),5(5,R),6(5),1604(7),26355(4),205(3),15317(3),5(7,R),6(7),7347(7)]),flip(a)]. given #765 (A,wt=38): 302 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(33(a,2),18(a,1,3,3))]. given #766 (T,wt=24): 30370 f(x,f(y,z,f(y,x,u)),f(u,v,f(y,x,u))) = f(y,x,u). [para(19226(a,1),4278(a,1)),rewrite([5(3),6(3),27027(4),813(3),5(6),5(6),5(7,R),26355(7),1713(6)]),flip(a)]. given #767 (T,wt=24): 30610 f(x,f(y,z,u),f(y,v,f(x,v,z))) = f(x,v,f(y,z,u)). [para(19843(a,1),19(a,1,3)),rewrite([6(1),25909(5),15991(4),20(3),6(4)]),flip(a)]. given #768 (T,wt=24): 30630 f(x,f(y,z,u),f(y,v,f(v,x,z))) = f(v,x,f(y,z,u)). [para(19843(a,1),922(a,2)),rewrite([5(1),6(4),5(6),12860(9),5(6,R),6(6)])]. given #769 (T,wt=24): 30634 f(x,f(y,z,u),f(y,v,f(z,x,v))) = f(x,v,f(y,z,u)). [para(19843(a,1),1057(a,2)),rewrite([5(2,R),6(2),6(4),5(6,R),6(6),16415(9)])]. given #770 (A,wt=31): 303 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(33(a,1),24(a,2,3)),rewrite([5(3,R),6(3),5(8,R),6(8)]),flip(a)]. given #771 (T,wt=24): 30647 f(x,f(y,z,f(x,u,z)),f(y,u,v)) = f(x,z,f(y,u,v)). [para(19843(a,1),1072(a,2)),rewrite([5(7,R),12377(9)])]. given #772 (T,wt=24): 30754 f(x,f(y,z,u),f(z,v,f(y,v,x))) = f(v,x,f(y,z,u)). [para(19852(a,1),5(a,2)),rewrite([5(2),5(2),5(4),5(6,R),6(6)])]. given #773 (T,wt=24): 30766 f(x,f(y,z,u),f(z,v,f(y,x,v))) = f(x,v,f(y,z,u)). [para(19852(a,1),1057(a,2)),rewrite([5(2,R),6(2),6(4),5(6,R),6(6),16415(9)])]. given #774 (T,wt=24): 30775 f(x,f(y,z,f(x,u,z)),f(u,y,v)) = f(x,z,f(u,y,v)). [para(19852(a,1),1072(a,2)),rewrite([5(7,R),12377(9)])]. given #775 (A,wt=31): 304 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),33(a,1,3,3)),flip(a)]. given #776 (T,wt=24): 30820 f(f(x,y,z),f(u,x,y),f(v,z,f(x,y,z))) = f(x,y,z). [para(3301(a,1),19852(a,2)),rewrite([5(7,R),20706(9)])]. given #777 (T,wt=24): 30822 f(f(x,y,z),f(x,u,y),f(v,z,f(x,y,z))) = f(x,y,z). [para(7335(a,1),19852(a,2)),rewrite([5(7,R),20706(9)])]. given #778 (T,wt=24): 30843 f(x,f(y,z,u),f(y,u,f(x,z,v))) = f(y,u,f(x,z,v)). [back_rewrite(30316),rewrite([5(2,R),6(2),19852(4),5(3,R),6(3)]),flip(a)]. given #779 (T,wt=23): 36512 f(f(x,y,z),f(u,x,v),f(u,v,y)) = f(u,v,f(x,y,z)). [para(30843(a,1),18846(a,2)),rewrite([5(2,R),6(2),5(5),5(5),12860(6),6(5),29260(5),5(5,R),6(5)])]. given #780 (A,wt=31): 305 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(33(a,1),30(a,2,3)),rewrite([5(3,R),6(3),57(4),5(8,R),6(8)]),flip(a)]. given #781 (T,wt=20): 36550 f(x,f(y,z,u),f(y,z,v)) = f(y,z,f(v,u,x)). [para(36512(a,1),5(a,1)),rewrite([6(5),35620(6)]),flip(a)]. given #782 (T,wt=20): 36623 f(x,f(y,z,u),f(y,v,z)) = f(y,z,f(v,u,x)). [para(36512(a,1),18417(a,2)),rewrite([5(7,R),31526(9),33841(4)])]. given #783 (T,wt=20): 36664 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(z,v,x)). [para(36512(a,1),23175(a,2)),rewrite([5(6),26355(6),5(7,R),6(7),31541(7),474(5),6(3),33838(6)])]. given #784 (T,wt=20): 36884 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [back_rewrite(36560),rewrite([6(2),6(4),5(5,R),6(5),36648(6)])]. ============================== PROOF ================================= % Proof 1 at 654.51 (+ 0.85) seconds: dist_both. % Length of proof is 235. % Level of proof is 31. % Maximum clause weight is 46. % Given clauses 784. 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(non_clause) # 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,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))). [para(16(a,2),8(a,1,3))]. 27 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))]. 28 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))]. 29 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)])]. 30 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(17(a,1),5(a,2)),rewrite([6(2),5(3,R),6(3)]),flip(a)]. 32 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)]. 33 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)])]. 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))]. 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)]. 61 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))]. 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)])]. 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)]. 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)]. 87 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,v,f(x,y,u))). [para(30(a,2),24(a,2,3)),rewrite([5(2,R),6(2),5(6,R),6(6)])]. 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)]. 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)])]. 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)]. 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),28(a,2,3)),rewrite([28(4)]),flip(a)]. 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),28(a,2,3)),rewrite([28(4)])]. 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)])]. 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)])]. 132 f(x,y,f(z,u,f(x,z,u))) = f(x,y,f(x,z,u)). [para(15(a,1),25(a,1,3)),rewrite([6(4),95(6)]),flip(a)]. 168 f(x,f(y,z,u),f(y,z,f(y,u,x))) = f(y,x,f(y,z,u)). [para(27(a,1),5(a,2)),rewrite([5(2),5(2),5(4),5(6,R),6(6)])]. 187 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),27(a,1,2)),rewrite([5(1,R),6(1),5(5,R),6(5),5(8,R),6(8)])]. 200 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(25(a,1),27(a,1,3,3))]. 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)]. 220 f(x,y,f(z,u,f(u,y,v))) = f(u,y,f(x,y,f(z,u,v))). [para(29(a,1),5(a,2)),rewrite([5(1,R),6(1),6(3),5(5,R),6(5),5(6,R),6(6)])]. 262 f(x,y,f(z,u,f(u,y,v))) = f(x,y,f(u,y,f(z,u,v))). [para(29(a,1),205(a,1,3)),rewrite([5(1,R),6(1),5(4,R),6(4),5(5,R),6(5),187(6),5(4,R),6(4),5(6,R),6(6)]),flip(a)]. 318 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)])]. 319 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)]. 321 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)])]. 331 f(x,y,f(z,f(x,y,u),f(x,v,f(x,y,u)))) = f(x,f(x,y,u),f(z,v,f(x,y,u))). [para(20(a,1),38(a,1,3)),rewrite([5(2),5(2),6(4),6(7),5(8,R),6(8)]),flip(a)]. 360 f(x,f(y,z,u),f(y,z,x)) = f(y,z,f(z,x,f(y,x,u))). [para(38(a,2),24(a,2)),rewrite([5(1,R),6(1),5(2,R),6(2),5(5),6(5)]),flip(a)]. 385 f(x,y,f(z,f(x,y,u),f(x,y,z))) = f(y,z,f(x,y,f(x,z,u))). [para(38(a,2),122(a,1,3)),rewrite([5(2),6(2),5(5,R),6(5),5(7,R),6(7)])]. 392 f(x,f(y,z,u),f(x,y,v)) = f(x,y,f(x,v,f(y,z,u))). [para(38(a,2),25(a,1)),rewrite([6(2)])]. 474 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)]. 628 f(x,f(y,x,z),f(x,u,z)) = f(y,x,f(x,u,z)). [para(474(a,1),17(a,1)),rewrite([6(4)]),flip(a)]. 630 f(x,y,f(z,u,f(z,x,v))) = f(x,y,f(z,v,f(z,x,u))). [para(474(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)])]. 654 f(x,f(y,x,z),f(x,z,u)) = f(y,x,f(x,z,u)). [para(628(a,1),5(a,2)),rewrite([6(2),5(3),6(4)])]. 695 f(x,f(x,y,z),f(u,x,y)) = f(u,x,f(x,y,z)). [para(654(a,1),6(a,1)),flip(a)]. 696 f(x,f(x,y,z),f(u,v,f(x,y,z))) = f(x,z,f(x,y,f(u,v,f(x,y,z)))). [para(654(a,1),25(a,2)),rewrite([5(1),5(1),5(2),5(2),6(3),5(4,R),6(4),331(5),5(5),5(5),5(6),5(6),5(8,R),6(8)])]. 803 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [para(695(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),696(6),28(5),6(3),57(6),6(4),20(5),22(5)]),flip(a)]. 812 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para(803(a,1),5(a,2)),rewrite([5(1,R),6(1),6(3),5(4)])]. 813 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para(5(a,1),803(a,1,3,3)),rewrite([5(1),6(1),6(4)])]. 814 f(x,y,f(x,z,f(x,u,f(u,y,v)))) = f(x,z,f(x,u,y)). [para(803(a,1),8(a,1,3)),flip(a)]. 816 f(x,y,f(x,z,f(z,u,f(y,z,v)))) = f(x,y,z). [para(8(a,1),803(a,1,3,3)),rewrite([5(1,R),6(1),6(5)])]. 820 f(x,y,f(x,f(y,z,u),f(y,v,f(y,z,u)))) = f(y,z,f(x,y,u)). [para(16(a,2),803(a,2)),rewrite([6(3),392(5),6(4)])]. 826 f(x,f(y,z,u),f(x,z,f(z,v,f(y,z,u)))) = f(y,z,f(x,z,u)). [para(24(a,1),803(a,2)),rewrite([6(3)])]. 827 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [para(30(a,2),803(a,1,3)),rewrite([6(1),6(4)])]. 828 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(30(a,2),803(a,2)),rewrite([6(3),392(5),6(4),820(5)])]. 847 f(x,f(y,z,u),f(x,v,f(x,y,z))) = f(x,v,f(x,y,z)). [para(803(a,1),33(a,1,3)),rewrite([6(4)]),flip(a)]. 866 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [back_rewrite(360),rewrite([5(2),392(3),813(3),5(2,R),6(2),5(3,R),6(3)]),flip(a)]. 871 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [back_rewrite(385),rewrite([827(4)]),flip(a)]. 874 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(828(a,1),5(a,2)),rewrite([6(2),5(3)]),flip(a)]. 897 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(874(a,1),5(a,2)),rewrite([6(2),5(3)])]. 922 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(874(a,2),38(a,2)),rewrite([6(2),392(3),813(3)]),flip(a)]. 933 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(874(a,2),803(a,2)),rewrite([6(3),826(5)]),flip(a)]. 1030 f(x,y,f(z,u,f(x,u,y))) = f(x,u,y). [para(20(a,1),897(a,1,3)),rewrite([15(3),696(5),122(4)]),flip(a)]. 1036 f(x,f(y,z,u),f(y,v,f(y,z,u))) = f(v,f(y,z,u),f(y,u,f(x,y,z))). [para(30(a,2),897(a,2,3)),rewrite([5(3,R),6(3)])]. 1050 f(x,y,f(x,f(x,y,z),f(u,y,z))) = f(x,y,z). [para(897(a,1),29(a,1)),rewrite([20(3),15(3)]),flip(a)]. 1057 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(38(a,2),897(a,2)),rewrite([5(1,R),6(1),5(2,R),6(2),696(4),28(3),6(1),803(3),6(2),5(3,R),6(3),5(4),20(4)]),flip(a)]. 1063 f(x,f(y,z,u),f(x,u,f(u,v,f(y,z,u)))) = f(y,u,f(x,z,u)). [para(897(a,1),803(a,2)),rewrite([6(3)])]. 1071 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(5(a,1),922(a,1,2)),rewrite([5(2),5(4)])]. 1072 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(5(a,2),922(a,1,2)),rewrite([5(2),6(2),392(3),5(4),6(4)])]. 1073 f(x,f(y,z,x),f(y,z,u)) = f(y,z,x). [para(922(a,1),6(a,1)),flip(a)]. 1079 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(16(a,1),922(a,1,2)),rewrite([5(3),5(5)])]. 1082 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [para(17(a,2),922(a,1,2)),rewrite([5(3),392(4),5(5)])]. 1088 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(30(a,1),922(a,1,2)),rewrite([5(3),5(5)])]. 1101 f(f(x,y,z),f(y,z,u),f(x,y,z)) = f(x,y,z). [para(205(a,1),922(a,1,3)),rewrite([205(6)])]. 1136 f(x,f(y,z,u),f(x,v,f(y,z,v))) = f(x,v,f(y,z,u)). [para(922(a,1),803(a,1,3,3))]. 1140 f(f(x,y,z),f(x,y,u),f(u,v,f(x,y,z))) = f(v,f(x,y,u),f(x,y,z)). [para(922(a,1),828(a,2,3)),rewrite([6(4),5(8,R)])]. 1142 f(x,f(y,z,x),f(u,f(y,z,v),f(y,z,x))) = f(y,z,x). [para(922(a,1),874(a,1,3)),rewrite([5(3,R),15(3),5(5)]),flip(a)]. 1148 f(x,f(y,z,u),f(x,u,f(y,z,v))) = f(x,u,f(y,z,v)). [para(922(a,1),922(a,1,2)),rewrite([5(3),5(6)])]. 1149 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(933(a,1),5(a,2)),rewrite([6(2),5(3)])]. 1150 f(x,f(y,z,x),f(y,u,f(y,z,x))) = f(y,z,x). [para(19(a,1),933(a,1,3)),rewrite([5(3,R),15(3),6(4)]),flip(a)]. 1176 f(x,f(y,z,u),f(x,u,v)) = f(x,v,f(z,u,f(x,y,u))). [para(933(a,1),828(a,2,3)),rewrite([5(2,R),6(2),5(4)])]. 1181 f(x,f(y,x,z),f(y,z,u)) = f(y,x,z). [para(1057(a,1),6(a,1)),flip(a)]. 1197 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,z,f(x,y,u))). [para(38(a,2),1057(a,2)),rewrite([6(3),5(6,R),6(6),392(7),1072(7),5(5,R),6(5)]),flip(a)]. 1253 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(1071(a,1),5(a,2)),rewrite([5(2),5(2),5(3),5(4),5(4)])]. 1254 f(x,f(y,z,u),f(x,v,f(x,z,u))) = f(x,v,f(x,z,u)). [para(1071(a,1),8(a,2,3))]. 1286 f(x,f(y,z,u),f(x,u,f(x,z,v))) = f(x,v,f(x,z,u)). [para(1071(a,1),32(a,2,3)),rewrite([6(2)])]. 1321 f(x,f(y,z,f(z,u,v)),f(x,f(y,z,u),f(z,u,v))) = f(x,f(y,z,u),f(z,u,v)). [para(654(a,1),1071(a,1,2))]. 1329 f(x,f(y,z,u),f(x,v,f(z,u,v))) = f(x,v,f(y,z,u)). [para(1071(a,1),803(a,1,3,3)),rewrite([5(2),5(2)])]. 1332 f(f(x,y,z),f(y,z,u),f(u,v,f(x,y,z))) = f(v,f(y,z,u),f(x,y,z)). [para(1071(a,1),828(a,2,3)),rewrite([5(2),5(2),6(4),5(7),5(7),5(8,R)])]. 1341 f(x,y,f(x,f(z,u,v),f(y,z,u))) = f(x,y,f(z,u,v)). [para(1071(a,1),922(a,1,2)),rewrite([5(2),5(2),5(3),392(4),5(5),5(5),5(6)])]. 1344 f(f(x,y,z),f(y,z,u),f(u,v,f(y,z,u))) = f(y,z,u). [para(1071(a,1),1057(a,1,3)),rewrite([5(2),5(2),6(3),5(4),5(4),6(5),5(7),5(7),1253(8)])]. 1349 f(x,f(x,y,z),f(y,u,f(y,z,v))) = f(x,y,z). [para(8(a,1),1073(a,1,3)),rewrite([5(1),5(5)])]. 1404 f(x,y,f(x,f(z,u,v),f(y,u,v))) = f(x,y,f(z,u,v)). [para(1071(a,1),1073(a,1,3)),rewrite([5(2),6(4),392(4),5(6)])]. 1469 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(1149(a,1),803(a,2)),rewrite([6(3),1063(5)])]. 1605 f(f(x,y,z),f(x,z,u),f(y,v,f(x,z,u))) = f(v,f(x,z,u),f(x,y,z)). [para(1181(a,1),1469(a,2,3))]. 1618 f(x,y,f(y,f(z,u,f(x,u,v)),f(x,w,f(z,u,f(x,u,v))))) = f(x,u,f(x,y,f(z,u,v))). [para(29(a,1),812(a,2)),rewrite([6(5)])]. 1630 f(x,y,f(y,f(z,u,v),f(x,z,u))) = f(x,y,f(z,u,v)). [para(922(a,1),812(a,1,3,3)),rewrite([5(2)])]. 1856 f(x,y,f(z,x,f(y,u