============================== Prover9 ===============================
Prover9 (32) version 22-May-2007, May 2007.
Process 27933 was started by mccune on cleo,
Tue May 22 14:58:16 2007
The command was "/home/mccune/bin/prover9 -f pair.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file pair.in

assign(max_seconds,1800).
assign(new_constants,1).

formulas(sos).
f(x,y) = f(y,x).
f(f(x,y),f(x,f(y,z))) = x.
end_of_list.

formulas(goals).
f(f(x,x),f(x,x)) = x & f(x,f(y,f(y,y))) = f(x,x) & f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # answer("Sheffer").
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 f(f(x,x),f(x,x)) = x & f(x,f(y,f(y,y))) = f(x,x) & f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # answer("Sheffer") # 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,y) = f(y,x).  [assumption].
f(f(x,y),f(x,f(y,z))) = x.  [assumption].
f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # answer("Sheffer").  [deny(1)].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

No predicates eliminated.

============================== end predicate elimination =============

Auto_denials:  (no changes).

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ = ]).
Function symbol precedence:  function_order([ c1, c2, c3, f ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).
  % set(hyper_resolution).  % (nonunit Horn with equality)
    % set(hyper_resolution) -> set(pos_hyper_resolution).
  % set(neg_ur_resolution).  % (nonunit Horn with equality)
  % assign(para_lit_limit, 3).  % (nonunit Horn with equality)

Auto_process settings:
  % set(back_unit_deletion).  % (Horn set with negative nonunits)
    % set(back_unit_deletion) -> set(unit_deletion).

% Operation f is commutative; C redundancy checks enabled.

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
2 f(x,y) = f(y,x).  [assumption].
3 f(f(x,y),f(x,f(y,z))) = x.  [assumption].
5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer").  [copy(4),rewrite([2(25),2(30)]),flip(c)].
end_of_list.

formulas(demodulators).
2 f(x,y) = f(y,x).  [assumption].
        % (lex-dep)
3 f(f(x,y),f(x,f(y,z))) = x.  [assumption].
end_of_list.

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.00 seconds.

given #1 (I,wt=7): 2 f(x,y) = f(y,x).  [assumption].

given #2 (I,wt=11): 3 f(f(x,y),f(x,f(y,z))) = x.  [assumption].

given #3 (I,wt=43): 5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer").  [copy(4),rewrite([2(25),2(30)]),flip(c)].

given #4 (A,wt=11): 6 f(f(x,y),f(y,f(x,z))) = y.  [para(2(a,1),3(a,1,1))].

given #5 (T,wt=11): 7 f(f(x,y),f(x,f(z,y))) = x.  [para(2(a,1),3(a,1,2,2))].

given #6 (T,wt=11): 8 f(f(x,y),f(f(y,z),x)) = x.  [para(2(a,1),3(a,1,2))].

given #7 (T,wt=11): 10 f(x,f(x,f(x,y))) = f(x,y).  [para(3(a,1),3(a,1,2)),rewrite([2(2),2(3)])].

given #8 (T,wt=9): 36 f(f(x,x),f(x,y)) = x.  [para(10(a,1),3(a,1,2))].

given #9 (A,wt=17): 9 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y).  [para(3(a,1),3(a,1,1))].

given #10 (F,wt=34): 39 f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer").  [back_rewrite(5),rewrite([36(7)]),xx(a)].

given #11 (T,wt=9): 40 f(f(x,y),f(x,x)) = x.  [para(36(a,1),2(a,1)),flip(a)].

given #12 (T,wt=9): 41 f(f(x,x),f(y,x)) = x.  [para(2(a,1),36(a,1,2))].

given #13 (T,wt=9): 57 f(f(x,y),f(y,y)) = y.  [para(2(a,1),40(a,1,1))].

given #14 (T,wt=11): 11 f(f(x,f(y,z)),f(y,x)) = x.  [para(6(a,1),2(a,1)),flip(a)].

given #15 (A,wt=11): 12 f(f(x,y),f(y,f(z,x))) = y.  [para(2(a,1),6(a,1,2,2))].

given #16 (T,wt=11): 13 f(f(x,y),f(f(x,z),y)) = y.  [para(2(a,1),6(a,1,2))].

given #17 (T,wt=11): 15 f(x,f(x,f(y,x))) = f(y,x).  [para(6(a,1),3(a,1,2)),rewrite([2(2),2(3)])].

given #18 (T,wt=11): 17 f(f(f(x,y),z),f(z,x)) = z.  [para(3(a,1),6(a,1,2,2))].

given #19 (T,wt=11): 19 f(f(f(x,y),z),f(z,y)) = z.  [para(6(a,1),6(a,1,2,2))].

given #20 (A,wt=17): 14 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x).  [para(6(a,1),3(a,1,1))].

given #21 (T,wt=11): 20 f(f(x,y),f(f(z,y),x)) = x.  [para(2(a,1),7(a,1,2))].

given #22 (T,wt=11): 32 f(f(x,f(y,z)),f(z,x)) = x.  [para(6(a,1),8(a,1,2,1))].

given #23 (T,wt=11): 45 f(x,f(f(x,x),y)) = f(x,x).  [para(36(a,1),7(a,1,2)),rewrite([2(3)])].

given #24 (T,wt=11): 62 f(x,f(y,f(x,x))) = f(x,x).  [para(41(a,1),6(a,1,2)),rewrite([2(3)])].

given #25 (A,wt=19): 16 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)).  [para(3(a,1),6(a,1,1))].

given #26 (T,wt=11): 71 f(f(x,y),f(f(z,x),y)) = y.  [para(2(a,1),12(a,1,2))].

given #27 (T,wt=11): 184 f(x,f(y,f(x,y))) = f(x,x).  [para(32(a,1),16(a,1,2)),flip(a)].

given #28 (T,wt=11): 206 f(x,f(y,f(y,x))) = f(x,x).  [para(2(a,1),184(a,1,2,2))].

given #29 (T,wt=13): 23 f(x,f(f(x,y),f(y,z))) = f(x,y).  [para(3(a,1),7(a,1,2)),rewrite([2(4)])].

given #30 (A,wt=19): 18 f(x,f(f(x,f(y,z)),f(f(y,x),u))) = f(x,f(y,z)).  [para(6(a,1),6(a,1,1))].

given #31 (T,wt=13): 26 f(x,f(f(y,x),f(y,z))) = f(y,x).  [para(6(a,1),7(a,1,2)),rewrite([2(4)])].

given #32 (T,wt=13): 28 f(x,f(f(x,y),f(z,y))) = f(x,y).  [para(7(a,1),7(a,1,2)),rewrite([2(4)])].

given #33 (T,wt=13): 31 f(x,f(f(y,z),f(x,y))) = f(x,y).  [para(8(a,1),6(a,1,2)),rewrite([2(4)])].

given #34 (T,wt=13): 75 f(x,f(f(y,z),f(y,x))) = f(y,x).  [para(6(a,1),12(a,1,2)),rewrite([2(4)])].

given #35 (A,wt=17): 21 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y).  [para(7(a,1),3(a,1,1))].

given #36 (T,wt=13): 77 f(x,f(f(y,x),f(z,y))) = f(y,x).  [para(12(a,1),7(a,1,2)),rewrite([2(4)])].

given #37 (T,wt=13): 79 f(x,f(f(y,z),f(x,z))) = f(x,z).  [para(7(a,1),12(a,1,2)),rewrite([2(4)])].

given #38 (T,wt=13): 85 f(x,f(f(y,z),f(z,x))) = f(z,x).  [para(12(a,1),12(a,1,2)),rewrite([2(4)])].

given #39 (T,wt=15): 33 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)).  [para(6(a,1),8(a,1,2)),rewrite([2(3),2(4)])].

given #40 (A,wt=17): 22 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y).  [para(3(a,1),7(a,1,1))].

given #41 (F,wt=34): 583 f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) # answer("Sheffer").  [back_rewrite(39),rewrite([570(27),2(26),570(32),2(31)])].

given #42 (T,wt=11): 570 f(x,f(y,y)) = f(x,f(y,x)).  [para(184(a,1),33(a,1,2))].

given #43 (T,wt=11): 637 f(f(x,x),y) = f(y,f(x,y)).  [para(570(a,1),2(a,1)),flip(a)].

given #44 (T,wt=11): 638 f(x,f(y,y)) = f(x,f(x,y)).  [para(2(a,1),570(a,2,2))].

given #45 (T,wt=11): 652 f(x,f(f(y,y),x)) = f(x,y).  [para(36(a,1),570(a,1,2)),flip(a)].

given #46 (A,wt=19): 24 f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)).  [para(7(a,1),6(a,1,1))].

given #47 (T,wt=11): 741 f(f(x,x),y) = f(y,f(y,x)).  [para(2(a,1),637(a,2,2))].

given #48 (T,wt=11): 826 f(x,f(x,f(y,y))) = f(x,y).  [para(638(a,2),10(a,1,2))].

given #49 (T,wt=15): 43 f(x,f(f(x,y),f(f(x,x),z))) = f(x,y).  [para(36(a,1),6(a,1,1))].

given #50 (T,wt=15): 50 f(f(x,y),f(x,f(f(x,f(y,z)),u))) = x.  [para(9(a,1),7(a,1,2)),rewrite([2(6)])].

given #51 (A,wt=17): 25 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x).  [para(6(a,1),7(a,1,1))].

given #52 (T,wt=15): 58 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y).  [para(40(a,1),7(a,1,1))].

given #53 (T,wt=15): 59 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z).  [para(40(a,1),8(a,1,1))].

given #54 (T,wt=15): 61 f(x,f(f(y,x),f(f(x,x),z))) = f(y,x).  [para(41(a,1),6(a,1,1))].

given #55 (T,wt=15): 64 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x).  [para(57(a,1),7(a,1,1))].

given #56 (A,wt=17): 27 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y).  [para(7(a,1),7(a,1,1))].

given #57 (T,wt=15): 65 f(x,f(f(f(x,x),y),f(z,x))) = f(z,x).  [para(57(a,1),8(a,1,1))].

given #58 (T,wt=15): 80 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)).  [para(12(a,1),8(a,1,2)),rewrite([2(3),2(4)])].

given #59 (T,wt=15): 91 f(x,f(y,f(f(y,z),x))) = f(f(y,z),x).  [para(13(a,1),8(a,1,2)),rewrite([2(3),2(4)])].

given #60 (T,wt=15): 107 f(x,f(y,f(f(z,y),x))) = f(f(z,y),x).  [para(19(a,1),7(a,1,2)),rewrite([2(3),2(4)])].

given #61 (A,wt=17): 29 f(x,f(f(x,y),f(f(f(y,z),x),u))) = f(x,y).  [para(8(a,1),3(a,1,1))].

given #62 (T,wt=15): 112 f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z).  [para(40(a,1),19(a,1,2)),rewrite([2(5)])].

given #63 (T,wt=15): 113 f(x,f(f(y,f(x,x)),f(z,x))) = f(z,x).  [para(57(a,1),19(a,1,2)),rewrite([2(5)])].

given #64 (T,wt=15): 122 f(f(x,y),f(y,f(f(y,f(x,z)),u))) = y.  [para(14(a,1),7(a,1,2)),rewrite([2(6)])].

given #65 (T,wt=15): 156 f(f(x,f(f(x,y),z)),f(x,f(y,u))) = x.  [para(16(a,1),7(a,1,2))].

given #66 (A,wt=19): 30 f(x,f(f(f(y,z),x),f(f(x,y),u))) = f(f(y,z),x).  [para(8(a,1),6(a,1,1))].

given #67 (T,wt=15): 181 f(f(x,f(y,z)),f(x,f(f(x,y),u))) = x.  [para(16(a,1),32(a,1,1)),rewrite([2(5)])].

given #68 (T,wt=15): 210 f(f(x,f(y,f(z,y))),f(x,f(z,z))) = x.  [para(184(a,1),7(a,1,2,2))].

given #69 (T,wt=15): 220 f(f(f(x,f(y,x)),z),f(z,f(y,y))) = z.  [para(184(a,1),12(a,1,2,2))].

given #70 (T,wt=15): 227 f(f(f(x,x),y),f(y,f(z,f(x,z)))) = y.  [para(184(a,1),19(a,1,1,1))].

given #71 (A,wt=17): 34 f(x,f(f(x,y),f(z,f(f(y,u),x)))) = f(x,y).  [para(8(a,1),7(a,1,1))].

given #72 (T,wt=15): 232 f(f(x,f(y,f(z,y))),f(f(z,z),x)) = x.  [para(184(a,1),20(a,1,2,1))].

given #73 (T,wt=15): 235 f(f(x,f(y,y)),f(f(z,f(y,z)),x)) = x.  [para(184(a,1),32(a,1,1,2))].

given #74 (T,wt=15): 239 f(f(f(x,f(y,x)),z),f(f(y,y),z)) = z.  [para(184(a,1),71(a,1,2,1))].

given #75 (T,wt=15): 243 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x.  [para(206(a,1),7(a,1,2,2))].

given #76 (A,wt=21): 46 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v))) = x.  [para(9(a,1),3(a,1,1))].

given #77 (T,wt=15): 249 f(f(f(x,f(x,y)),z),f(z,f(y,y))) = z.  [para(206(a,1),12(a,1,2,2))].

given #78 (T,wt=15): 254 f(f(f(x,x),y),f(y,f(z,f(z,x)))) = y.  [para(206(a,1),19(a,1,1,1))].

given #79 (T,wt=15): 258 f(f(x,f(y,f(y,z))),f(f(z,z),x)) = x.  [para(206(a,1),20(a,1,2,1))].

given #80 (T,wt=15): 260 f(f(x,f(y,y)),f(f(z,f(z,y)),x)) = x.  [para(206(a,1),32(a,1,1,2))].

given #81 (A,wt=31): 47 f(f(x,y),f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v))) = f(f(x,y),f(f(x,f(y,z)),u)).  [para(9(a,1),6(a,1,1))].

given #82 (T,wt=15): 265 f(f(f(x,f(x,y)),z),f(f(y,y),z)) = z.  [para(206(a,1),71(a,1,2,1))].

given #83 (T,wt=15): 270 f(f(x,y),f(x,f(f(x,f(z,y)),u))) = x.  [para(7(a,1),23(a,1,2,1)),rewrite([7(10)])].

given #84 (T,wt=15): 272 f(f(x,y),f(x,f(f(f(y,z),x),u))) = x.  [para(8(a,1),23(a,1,2,1)),rewrite([8(10)])].

given #85 (T,wt=15): 275 f(f(x,f(y,z)),f(x,f(f(y,x),u))) = x.  [para(11(a,1),23(a,1,2,1)),rewrite([11(10)])].

given #86 (A,wt=21): 48 f(f(x,y),f(y,f(f(f(x,y),f(f(y,f(x,z)),u)),v))) = y.  [para(6(a,1),9(a,1,2,1)),rewrite([6(13)])].

given #87 (T,wt=15): 277 f(f(x,y),f(y,f(f(y,f(z,x)),u))) = y.  [para(12(a,1),23(a,1,2,1)),rewrite([12(10)])].

given #88 (T,wt=15): 279 f(f(x,y),f(y,f(f(f(x,z),y),u))) = y.  [para(13(a,1),23(a,1,2,1)),rewrite([13(10)])].

given #89 (T,wt=15): 280 f(f(f(x,y),z),f(z,f(f(z,x),u))) = z.  [para(17(a,1),23(a,1,2,1)),rewrite([17(10)])].

given #90 (T,wt=15): 282 f(f(f(x,y),z),f(z,f(f(z,y),u))) = z.  [para(19(a,1),23(a,1,2,1)),rewrite([19(10)])].

given #91 (A,wt=21): 49 f(f(x,y),f(x,f(z,f(f(x,y),f(f(x,f(y,u)),v))))) = x.  [para(9(a,1),7(a,1,1))].

given #92 (T,wt=15): 285 f(f(x,y),f(x,f(f(f(z,y),x),u))) = x.  [para(20(a,1),23(a,1,2,1)),rewrite([20(10)])].

given #93 (T,wt=15): 286 f(f(x,f(y,z)),f(x,f(f(z,x),u))) = x.  [para(32(a,1),23(a,1,2,1)),rewrite([32(10)])].

given #94 (T,wt=15): 290 f(f(x,y),f(y,f(f(f(z,x),y),u))) = y.  [para(71(a,1),23(a,1,2,1)),rewrite([71(10)])].

given #95 (T,wt=15): 295 f(f(x,f(f(y,x),z)),f(x,f(y,u))) = x.  [para(18(a,1),7(a,1,2))].

given #96 (A,wt=21): 51 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(z,y)),u)),v))) = x.  [para(7(a,1),9(a,1,2,1)),rewrite([7(13)])].

given #97 (T,wt=15): 324 f(f(x,f(y,z)),f(x,f(f(x,z),u))) = x.  [para(7(a,1),26(a,1,2,1)),rewrite([7(10)])].

given #98 (T,wt=15): 330 f(f(f(x,y),z),f(z,f(f(x,z),u))) = z.  [para(13(a,1),26(a,1,2,1)),rewrite([13(10)])].

given #99 (T,wt=15): 337 f(f(f(x,y),z),f(z,f(f(y,z),u))) = z.  [para(71(a,1),26(a,1,2,1)),rewrite([71(10)])].

given #100 (T,wt=15): 345 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x.  [para(3(a,1),28(a,1,2,1)),rewrite([3(10)])].

given #101 (A,wt=39): 52 f(f(f(x,y),z),f(x,f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)))) = f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)).  [para(9(a,1),8(a,1,2)),rewrite([2(8),2(11)])].

given #102 (T,wt=15): 346 f(f(x,y),f(y,f(z,f(y,f(x,u))))) = y.  [para(6(a,1),28(a,1,2,1)),rewrite([6(10)])].

given #103 (T,wt=15): 348 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x.  [para(7(a,1),28(a,1,2,1)),rewrite([7(10)])].

given #104 (T,wt=15): 350 f(f(x,y),f(x,f(z,f(f(y,u),x)))) = x.  [para(8(a,1),28(a,1,2,1)),rewrite([8(10)])].

given #105 (T,wt=15): 353 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x.  [para(11(a,1),28(a,1,2,1)),rewrite([11(10)])].

given #106 (A,wt=21): 53 f(f(x,y),f(x,f(f(f(x,y),f(f(f(y,z),x),u)),v))) = x.  [para(8(a,1),9(a,1,2,1)),rewrite([8(13)])].

given #107 (T,wt=15): 355 f(f(x,y),f(y,f(z,f(y,f(u,x))))) = y.  [para(12(a,1),28(a,1,2,1)),rewrite([12(10)])].

given #108 (T,wt=15): 357 f(f(x,y),f(y,f(z,f(f(x,u),y)))) = y.  [para(13(a,1),28(a,1,2,1)),rewrite([13(10)])].

given #109 (T,wt=15): 358 f(f(f(x,y),z),f(z,f(u,f(z,x)))) = z.  [para(17(a,1),28(a,1,2,1)),rewrite([17(10)])].

given #110 (T,wt=15): 360 f(f(f(x,y),z),f(z,f(u,f(z,y)))) = z.  [para(19(a,1),28(a,1,2,1)),rewrite([19(10)])].

given #111 (A,wt=23): 54 f(f(x,y),f(f(f(x,y),f(y,z)),f(x,u))) = f(f(x,y),f(y,z)).  [para(8(a,1),9(a,1,2,2,1))].

given #112 (T,wt=15): 363 f(f(x,y),f(x,f(z,f(f(u,y),x)))) = x.  [para(20(a,1),28(a,1,2,1)),rewrite([20(10)])].

given #113 (T,wt=15): 364 f(f(x,f(y,z)),f(x,f(u,f(z,x)))) = x.  [para(32(a,1),28(a,1,2,1)),rewrite([32(10)])].

given #114 (T,wt=15): 368 f(f(x,y),f(y,f(z,f(f(u,x),y)))) = y.  [para(71(a,1),28(a,1,2,1)),rewrite([71(10)])].

given #115 (T,wt=15): 472 f(f(x,f(y,z)),f(x,f(u,f(x,y)))) = x.  [para(3(a,1),77(a,1,2,1)),rewrite([3(10)])].

given #116 (A,wt=27): 56 f(x,f(f(x,y),f(f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v)),w))) = f(x,y).  [para(9(a,1),9(a,1,2,1)),rewrite([9(17)])].

given #117 (T,wt=15): 474 f(f(x,f(y,z)),f(x,f(u,f(x,z)))) = x.  [para(7(a,1),77(a,1,2,1)),rewrite([7(10)])].

given #118 (T,wt=15): 480 f(f(f(x,y),z),f(z,f(u,f(x,z)))) = z.  [para(13(a,1),77(a,1,2,1)),rewrite([13(10)])].

given #119 (T,wt=15): 487 f(f(f(x,y),z),f(z,f(u,f(y,z)))) = z.  [para(71(a,1),77(a,1,2,1)),rewrite([71(10)])].

given #120 (T,wt=15): 582 f(x,f(f(x,f(y,z)),f(y,y))) = f(x,x).  [back_rewrite(569),rewrite([570(6,R)])].

given #121 (A,wt=19): 60 f(f(x,y),f(x,f(f(f(x,y),f(f(x,x),z)),u))) = x.  [para(40(a,1),9(a,1,2,1)),rewrite([40(11)])].

given #122 (F,wt=23): 9201 f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) # answer("Sheffer").  [back_unit_del(583),unit_del(a,9101)].

given #123 (T,wt=11): 9101 f(x,f(y,f(y,y))) = f(x,x).  [para(14(a,1),582(a,1,2,1)),rewrite([5880(5)])].

NOTE: New constant: f(x,f(x,x)) = c_0.  [new_symbol(9354)].
NOTE: New Function symbol precedence:  function_order([ c1, c2, c3, c_0, f ]).

given #124 (T,wt=7): 9472 f(x,f(x,x)) = c_0.  [new_symbol(9354)].

given #125 (T,wt=7): 9749 f(f(c_0,c_0),x) = c_0.  [back_rewrite(9338),rewrite([9472(2),9472(3),9472(6)])].

given #126 (T,wt=7): 9750 f(c_0,f(c_0,x)) = x.  [back_rewrite(9337),rewrite([9472(2),9472(3)])].

given #127 (A,wt=19): 63 f(f(x,x),f(f(f(x,x),y),f(x,z))) = f(f(x,x),y).  [para(41(a,1),9(a,1,2,2,1))].

given #128 (F,wt=19): 9629 f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) != f(c_0,f(c1,f(c2,c3))) # answer("Sheffer").  [back_rewrite(9469),rewrite([9472(7),2(7)]),flip(a)].

given #129 (T,wt=7): 9753 f(x,f(c_0,c_0)) = c_0.  [back_rewrite(9332),rewrite([9472(2),9472(3),9472(6)])].

given #130 (T,wt=7): 9755 f(c_0,f(x,x)) = x.  [back_rewrite(9330),rewrite([9472(2)])].

given #131 (T,wt=7): 9756 f(c_0,f(x,c_0)) = x.  [back_rewrite(9329),rewrite([9472(2),9472(3)])].

given #132 (T,wt=7): 9778 f(c_0,x) = f(x,x).  [back_rewrite(9287),rewrite([9472(2)])].

given #133 (A,wt=19): 66 f(f(x,y),f(y,f(f(f(x,y),f(f(y,y),z)),u))) = y.  [para(57(a,1),9(a,1,2,1)),rewrite([57(11)])].

given #134 (T,wt=7): 9790 f(x,c_0) = f(x,x).  [back_rewrite(9101),rewrite([9472(2)])].

given #135 (T,wt=7): 11086 f(x,f(x,c_0)) = c_0.  [para(9472(a,1),10(a,1,2,2)),rewrite([9472(5)])].

given #136 (T,wt=7): 11112 f(x,f(c_0,x)) = c_0.  [para(9749(a,1),637(a,1)),flip(a)].

given #137 (T,wt=9): 9774 f(f(x,y),f(y,c_0)) = y.  [back_rewrite(9303),rewrite([9472(3)])].

given #138 (A,wt=19): 67 f(x,f(f(x,f(y,z)),f(u,f(y,x)))) = f(x,f(y,z)).  [para(11(a,1),7(a,1,1))].

given #139 (T,wt=9): 9775 f(f(x,c_0),f(y,x)) = x.  [back_rewrite(9301),rewrite([9472(2)])].

given #140 (T,wt=9): 9776 f(f(x,y),f(x,c_0)) = x.  [back_rewrite(9299),rewrite([9472(3)])].

given #141 (T,wt=9): 9777 f(f(x,c_0),f(x,y)) = x.  [back_rewrite(9295),rewrite([9472(2)])].

given #142 (T,wt=9): 11085 f(f(x,y),f(c_0,x)) = x.  [para(9472(a,1),8(a,1,2,1))].

given #143 (A,wt=19): 68 f(x,f(f(f(y,x),z),f(x,f(y,u)))) = f(x,f(y,u)).  [para(11(a,1),8(a,1,1))].

given #144 (T,wt=9): 11088 f(f(x,y),f(c_0,y)) = y.  [para(9472(a,1),13(a,1,2,1))].

given #145 (T,wt=9): 11089 f(f(c_0,x),f(x,y)) = x.  [para(9472(a,1),17(a,1,1,1))].

given #146 (T,wt=9): 11121 f(f(c_0,x),f(y,x)) = x.  [back_rewrite(11105),rewrite([11118(9),11118(11)])].

given #147 (T,wt=11): 9692 f(x,f(c_0,f(y,f(y,x)))) = c_0.  [back_rewrite(9399),rewrite([9472(4),2(4),9472(7)])].

given #148 (A,wt=23): 69 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v))) = x.  [para(11(a,1),9(a,1,2,1)),rewrite([11(14)])].

given #149 (T,wt=11): 9713 f(x,f(c_0,f(y,f(x,y)))) = c_0.  [back_rewrite(9377),rewrite([9472(4),2(4),9472(7)])].

given #150 (T,wt=11): 9733 f(f(x,c_0),y) = f(f(x,x),y).  [back_rewrite(9355),rewrite([9472(2)])].

given #151 (T,wt=11): 9735 f(f(x,c_0),y) = f(y,f(x,x)).  [back_rewrite(9352),rewrite([9472(2)])].

given #152 (T,wt=11): 9747 f(x,f(x,f(y,c_0))) = f(x,y).  [back_rewrite(9340),rewrite([9472(2)])].

given #153 (A,wt=25): 70 f(f(x,f(y,z)),f(f(y,f(x,f(y,z))),f(x,u))) = f(y,f(x,f(y,z))).  [para(11(a,1),9(a,1,2,2,1)),rewrite([2(5),2(11)])].

Low Water (keep, True_semantics): wt=61

Low Water (keep, True_semantics): wt=59

given #154 (T,wt=11): 9748 f(f(x,c_0),y) = f(y,f(y,x)).  [back_rewrite(9339),rewrite([9472(2)])].

given #155 (T,wt=11): 9752 f(x,f(y,c_0)) = f(x,f(x,y)).  [back_rewrite(9333),rewrite([9472(2)])].

Low Water (keep, True_semantics): wt=53

given #156 (T,wt=11): 9754 f(f(x,c_0),y) = f(y,f(x,y)).  [back_rewrite(9331),rewrite([9472(2)])].

Low Water (keep, True_semantics): wt=51

given #157 (T,wt=11): 9757 f(x,f(y,c_0)) = f(x,f(y,x)).  [back_rewrite(9328),rewrite([9472(2)])].

Low Water (keep, True_semantics): wt=49

given #158 (A,wt=17): 72 f(x,f(f(y,x),f(f(x,f(z,y)),u))) = f(y,x).  [para(12(a,1),3(a,1,1))].

Low Water (keep, True_semantics): wt=47

given #159 (T,wt=11): 9760 f(x,f(c_0,f(x,y))) = f(x,y).  [back_rewrite(9323),rewrite([9472(3),2(3)])].

given #160 (T,wt=11): 9761 f(x,f(c_0,f(y,x))) = f(y,x).  [back_rewrite(9322),rewrite([9472(3),2(3)])].

given #161 (T,wt=11): 9764 f(f(x,x),f(c_0,f(y,x))) = c_0.  [back_rewrite(9319),rewrite([9472(4),2(4),9472(7)])].

given #162 (T,wt=11): 9765 f(x,f(y,c_0)) = f(x,f(y,y)).  [back_rewrite(9317),rewrite([9472(2)])].

given #163 (A,wt=19): 73 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)).  [para(3(a,1),12(a,1,1))].

Low Water (keep, True_semantics): wt=45

given #164 (T,wt=11): 9766 f(x,f(y,f(x,c_0))) = f(x,x).  [back_rewrite(9316),rewrite([9472(2)])].

given #165 (T,wt=11): 9767 f(x,f(f(x,c_0),y)) = f(x,x).  [back_rewrite(9315),rewrite([9472(2)])].

given #166 (T,wt=11): 9771 f(f(x,x),f(c_0,f(x,y))) = c_0.  [back_rewrite(9307),rewrite([9472(4),2(4),9472(7)])].

given #167 (T,wt=11): 11087 f(x,f(c_0,f(f(x,x),y))) = c_0.  [para(9472(a,1),9(a,1,2,1)),rewrite([45(4),9472(7)])].

given #168 (A,wt=19): 74 f(x,f(f(x,f(y,z)),f(f(z,x),u))) = f(x,f(y,z)).  [para(12(a,1),6(a,1,1))].

Low Water (keep, True_semantics): wt=43

given #169 (T,wt=11): 11090 f(x,f(c_0,f(y,f(x,x)))) = c_0.  [para(9472(a,1),28(a,1,2,1)),rewrite([9472(7)])].

given #170 (T,wt=11): 11091 f(x,f(y,f(c_0,x))) = f(c_0,x).  [para(9472(a,1),91(a,1,2,2,1)),rewrite([9472(6)])].

given #171 (T,wt=11): 11110 f(x,f(c_0,f(f(x,c_0),y))) = c_0.  [para(9749(a,1),9(a,1,2,2,1,2)),rewrite([9753(4),9753(10)])].

given #172 (T,wt=11): 11111 f(x,f(c_0,f(y,f(x,c_0)))) = c_0.  [para(9749(a,1),22(a,1,2,2,2,2)),rewrite([9753(4),9753(10)])].

given #173 (A,wt=17): 76 f(x,f(f(y,x),f(z,f(x,f(u,y))))) = f(y,x).  [para(12(a,1),7(a,1,1))].

given #174 (T,wt=11): 11113 f(x,f(c_0,f(f(c_0,x),y))) = c_0.  [para(9749(a,1),29(a,1,2,2,1,1)),rewrite([9753(4),9753(10)])].

given #175 (T,wt=11): 11114 f(x,f(c_0,f(y,f(c_0,x)))) = c_0.  [para(9749(a,1),34(a,1,2,2,2,1)),rewrite([9753(4),9753(10)])].

given #176 (T,wt=11): 11125 f(x,f(f(c_0,x),y)) = f(c_0,x).  [para(9750(a,1),26(a,1,2,2))].

given #177 (T,wt=11): 11226 f(x,f(c_0,y)) = f(x,f(y,y)).  [para(9778(a,1),16(a,1,2,1,2)),rewrite([9746(7)]),flip(a)].

Low Water (keep, True_semantics): wt=41

given #178 (A,wt=19): 78 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)).  [para(7(a,1),12(a,1,1))].

Low Water (keep, True_semantics): wt=39

given #179 (T,wt=11): 11229 f(x,f(c_0,y)) = f(x,f(y,x)).  [para(9778(a,2),570(a,1,2))].

given #180 (T,wt=11): 11230 f(f(c_0,x),y) = f(y,f(x,y)).  [para(9778(a,2),637(a,1,1))].

given #181 (T,wt=11): 11231 f(x,f(c_0,y)) = f(x,f(x,y)).  [para(9778(a,2),638(a,1,2))].

given #182 (T,wt=11): 11233 f(f(c_0,x),y) = f(y,f(y,x)).  [para(9778(a,2),741(a,1,1))].

given #183 (A,wt=19): 81 f(x,f(f(f(y,z),x),f(u,f(x,y)))) = f(f(y,z),x).  [para(8(a,1),12(a,1,1))].

given #184 (T,wt=11): 11234 f(x,f(x,f(c_0,y))) = f(x,y).  [para(9778(a,2),826(a,1,2,2))].

Low Water (keep, True_semantics): wt=35

given #185 (T,wt=11): 11240 f(f(c_0,x),y) = f(f(x,x),y).  [para(9778(a,1),91(a,1,2,2,1)),rewrite([9761(5)]),flip(a)].

given #186 (T,wt=11): 11241 f(f(x,x),y) = f(y,f(c_0,x)).  [para(9778(a,2),91(a,1,2,2,1)),rewrite([11125(4)]),flip(a)].

given #187 (T,wt=11): 11242 f(f(c_0,x),y) = f(y,f(x,x)).  [para(9778(a,2),91(a,2,1)),rewrite([45(3)]),flip(a)].

given #188 (A,wt=21): 82 f(f(x,y),f(y,f(f(f(x,y),f(f(y,f(z,x)),u)),v))) = y.  [para(12(a,1),9(a,1,2,1)),rewrite([12(13)])].

given #189 (T,wt=11): 12376 f(f(x,y),f(c_0,f(y,x))) = c_0.  [para(570(a,2),9692(a,1,2,2,2)),rewrite([826(5)])].

given #190 (T,wt=11): 12855 f(f(x,x),y) = f(y,f(x,c_0)).  [para(9733(a,1),2(a,1))].

given #191 (T,wt=11): 18356 f(f(c_0,f(x,y)),f(y,x)) = c_0.  [para(12376(a,1),2(a,1)),flip(a)].

given #192 (T,wt=13): 9784 f(f(x,x),f(f(y,x),f(x,z))) = c_0.  [back_rewrite(9130),rewrite([9472(7)])].

given #193 (A,wt=31): 83 f(f(x,y),f(f(f(x,y),f(f(x,f(y,z)),u)),f(v,x))) = f(f(x,y),f(f(x,f(y,z)),u)).  [para(9(a,1),12(a,1,1))].

Low Water (keep, True_semantics): wt=33

given #194 (T,wt=13): 9785 f(f(x,x),f(f(x,y),f(x,z))) = c_0.  [back_rewrite(9124),rewrite([9472(7)])].

given #195 (T,wt=13): 11118 f(f(c_0,x),f(f(c_0,f(x,y)),z)) = x.  [para(9749(a,1),52(a,1,1,1)),rewrite([9749(9),9749(11),9749(13),2(4),9750(4),9749(4),9749(6)]),flip(a)].

given #196 (T,wt=13): 11122 f(f(x,c_0),f(f(c_0,f(x,y)),z)) = x.  [para(14(a,1),9750(a,1,2)),rewrite([9756(4)]),flip(a)].

given #197 (T,wt=13): 11127 f(f(c_0,x),f(f(c_0,f(y,x)),z)) = x.  [para(21(a,1),9750(a,1,2)),rewrite([9750(4)]),flip(a)].

given #198 (A,wt=19): 84 f(x,f(f(x,f(y,z)),f(u,f(z,x)))) = f(x,f(y,z)).  [para(12(a,1),12(a,1,1))].

given #199 (T,wt=13): 11129 f(f(c_0,x),f(y,f(c_0,f(x,z)))) = x.  [para(22(a,1),9750(a,1,2)),rewrite([9750(4)]),flip(a)].

given #200 (T,wt=13): 11132 f(f(x,c_0),f(y,f(c_0,f(x,z)))) = x.  [para(25(a,1),9750(a,1,2)),rewrite([9756(4)]),flip(a)].

given #201 (T,wt=13): 11134 f(f(c_0,x),f(y,f(c_0,f(z,x)))) = x.  [para(27(a,1),9750(a,1,2)),rewrite([9750(4)]),flip(a)].

given #202 (T,wt=13): 11260 f(f(x,x),f(f(c_0,f(x,y)),z)) = x.  [para(9778(a,1),47(a,2,1)),rewrite([11118(9),6(6)]),flip(a)].

given #203 (A,wt=17): 86 f(x,f(f(y,x),f(f(f(y,z),x),u))) = f(y,x).  [para(13(a,1),3(a,1,1))].

given #204 (T,wt=13): 14440 f(f(x,y),f(y,x)) = f(c_0,f(x,y)).  [para(9754(a,2),206(a,1,2,2)),rewrite([11229(5,R),9756(5),9778(6,R)])].

given #205 (T,wt=13): 15051 f(f(x,c_0),f(f(c_0,f(y,x)),z)) = x.  [para(72(a,1),9750(a,1,2)),rewrite([9756(4)]),flip(a)].

given #206 (T,wt=13): 15108 f(f(x,f(c_0,f(y,z))),f(y,c_0)) = y.  [para(25(a,1),9761(a,1,2)),rewrite([11132(14)])].

given #207 (T,wt=13): 15888 f(f(x,c_0),f(y,f(c_0,f(z,x)))) = x.  [para(76(a,1),9750(a,1,2)),rewrite([9756(4)]),flip(a)].

given #208 (A,wt=19): 87 f(x,f(f(f(x,y),z),f(x,f(y,u)))) = f(x,f(y,u)).  [para(3(a,1),13(a,1,1))].

given #209 (T,wt=13): 15918 f(f(x,f(c_0,f(y,z))),f(z,c_0)) = z.  [para(76(a,1),9761(a,1,2)),rewrite([15888(14)])].

given #210 (T,wt=13): 17363 f(f(c_0,x),f(y,f(y,f(x,z)))) = x.  [para(11233(a,1),47(a,2,2)),rewrite([11118(9),6(6)]),flip(a)].

given #211 (T,wt=13): 18570 f(f(x,x),f(f(y,x),f(z,x))) = c_0.  [para(2(a,1),9784(a,1,2,2))].

given #212 (T,wt=13): 18571 f(f(x,x),f(f(x,y),f(z,x))) = c_0.  [para(2(a,1),9784(a,1,2))].

given #213 (A,wt=19): 88 f(x,f(f(f(y,z),x),f(f(y,x),u))) = f(f(y,z),x).  [para(13(a,1),6(a,1,1))].

Low Water (keep, True_semantics): wt=31

given #214 (T,wt=13): 18609 f(f(x,c_0),f(f(y,x),f(x,z))) = c_0.  [para(9784(a,1),91(a,1,2,2)),rewrite([2(6),9784(11)])].

given #215 (T,wt=13): 18659 f(f(c_0,x),f(f(y,x),f(x,z))) = c_0.  [para(9778(a,2),9784(a,1,1))].

given #216 (T,wt=13): 18740 f(f(x,c_0),f(f(x,y),f(x,z))) = c_0.  [para(9785(a,1),91(a,1,2,2)),rewrite([2(6),9785(11)])].

given #217 (T,wt=13): 18778 f(f(c_0,x),f(f(x,y),f(x,z))) = c_0.  [para(9778(a,2),9785(a,1,1))].

given #218 (A,wt=17): 89 f(x,f(f(y,x),f(z,f(f(y,u),x)))) = f(y,x).  [para(13(a,1),7(a,1,1))].

given #219 (T,wt=13): 18859 f(f(x,c_0),f(y,f(y,f(x,z)))) = x.  [para(11233(a,1),11122(a,1,2))].

given #220 (T,wt=13): 18868 f(f(x,x),f(f(c_0,f(y,x)),z)) = x.  [para(11127(a,1),15(a,1,2,2)),rewrite([2(9),570(10,R),2(6),11127(13)])].

given #221 (T,wt=13): 18945 f(f(c_0,x),f(y,f(y,f(z,x)))) = x.  [para(11233(a,1),11127(a,1,2))].

given #222 (T,wt=13): 19108 f(f(x,x),f(y,f(c_0,f(x,z)))) = x.  [para(9778(a,1),11129(a,1,1))].

given #223 (A,wt=19): 90 f(x,f(f(f(x,y),z),f(x,f(u,y)))) = f(x,f(u,y)).  [para(7(a,1),13(a,1,1))].

given #224 (T,wt=13): 19188 f(f(x,x),f(y,f(c_0,f(z,x)))) = x.  [para(9778(a,1),11134(a,1,1))].

given #225 (T,wt=13): 19233 f(f(x,x),f(y,f(y,f(x,z)))) = x.  [para(11233(a,1),11260(a,1,2))].

given #226 (T,wt=13): 19463 f(f(x,c_0),f(y,f(y,f(z,x)))) = x.  [para(11233(a,1),15051(a,1,2))].

given #227 (T,wt=13): 19475 f(f(x,f(x,f(y,z))),f(y,c_0)) = y.  [para(11231(a,1),15108(a,1,1))].

given #228 (A,wt=19): 92 f(x,f(f(f(x,y),z),f(f(y,u),x))) = f(f(y,u),x).  [para(8(a,1),13(a,1,1))].

given #229 (T,wt=13): 19583 f(f(x,f(x,f(y,z))),f(z,c_0)) = z.  [para(11231(a,1),15918(a,1,1))].

given #230 (T,wt=13): 19590 f(f(x,f(x,f(y,z))),f(c_0,y)) = y.  [para(17363(a,1),2(a,1)),flip(a)].

given #231 (T,wt=13): 19600 f(f(x,f(x,f(y,z))),f(y,y)) = y.  [para(17363(a,1),15(a,1,2,2)),rewrite([2(7),570(8,R),17363(11)])].

given #232 (T,wt=13): 19701 f(f(x,c_0),f(f(y,x),f(z,x))) = c_0.  [para(18570(a,1),91(a,1,2,2)),rewrite([2(6),18570(11)])].

given #233 (A,wt=21): 93 f(f(x,y),f(y,f(f(f(x,y),f(f(f(x,z),y),u)),v))) = y.  [para(13(a,1),9(a,1,2,1)),rewrite([13(13)])].

given #234 (T,wt=13): 19735 f(f(c_0,x),f(f(y,x),f(z,x))) = c_0.  [para(9778(a,2),18570(a,1,1))].

given #235 (T,wt=13): 19792 f(f(x,c_0),f(f(x,y),f(z,x))) = c_0.  [para(18571(a,1),91(a,1,2,2)),rewrite([2(6),18571(11)])].

given #236 (T,wt=13): 19826 f(f(c_0,x),f(f(x,y),f(z,x))) = c_0.  [para(9778(a,2),18571(a,1,1))].

given #237 (T,wt=13): 20175 f(f(x,x),f(y,f(y,f(z,x)))) = x.  [para(11233(a,1),18868(a,1,2))].

given #238 (A,wt=23): 94 f(f(x,y),f(f(f(x,y),f(x,z)),f(y,u))) = f(f(x,y),f(x,z)).  [para(13(a,1),9(a,1,2,2,1))].

given #239 (T,wt=13): 20178 f(f(x,f(x,f(y,z))),f(c_0,z)) = z.  [para(18945(a,1),2(a,1)),flip(a)].

given #240 (T,wt=13): 20186 f(f(x,f(x,f(y,z))),f(z,z)) = z.  [para(18945(a,1),15(a,1,2,2)),rewrite([2(7),570(8,R),18945(11)])].

given #241 (T,wt=15): 639 f(f(x,f(y,x)),f(x,f(f(y,y),z))) = x.  [para(570(a,1),3(a,1,1))].

given #242 (T,wt=15): 644 f(f(x,f(y,x)),f(x,f(z,f(y,y)))) = x.  [para(570(a,1),7(a,1,1))].

given #243 (A,wt=31): 95 f(f(x,y),f(f(x,z),f(f(x,y),f(f(x,f(y,u)),v)))) = f(f(x,y),f(f(x,f(y,u)),v)).  [para(9(a,1),13(a,1,1))].

given #244 (T,wt=15): 645 f(f(x,f(y,y)),f(x,f(z,f(y,z)))) = x.  [para(570(a,1),7(a,1,2,2))].

given #245 (T,wt=15): 646 f(f(x,f(y,z)),f(x,f(z,f(y,y)))) = x.  [para(570(a,2),7(a,1,2,2))].

given #246 (T,wt=15): 648 f(f(x,f(y,x)),f(f(f(y,y),z),x)) = x.  [para(570(a,1),8(a,1,1))].

given #247 (T,wt=15): 663 f(f(f(x,y),z),f(z,f(y,f(x,x)))) = z.  [para(570(a,2),12(a,1,2,2))].

given #248 (A,wt=19): 96 f(x,f(f(f(y,z),x),f(u,f(y,x)))) = f(f(y,z),x).  [para(13(a,1),12(a,1,1))].

given #249 (T,wt=15): 674 f(f(f(x,f(y,y)),z),f(z,f(y,z))) = z.  [para(570(a,1),19(a,1,2))].

Low Water (keep, True_semantics): wt=29

given #250 (T,wt=15): 675 f(f(f(x,f(y,y)),z),f(z,f(y,x))) = z.  [para(570(a,2),19(a,1,1,1))].

given #251 (T,wt=15): 682 f(f(x,f(y,x)),f(f(z,f(y,y)),x)) = x.  [para(570(a,1),20(a,1,1))].

given #252 (T,wt=15): 684 f(f(x,f(y,z)),f(f(z,f(y,y)),x)) = x.  [para(570(a,2),20(a,1,2,1))].

given #253 (A,wt=19): 97 f(x,f(f(f(y,x),z),f(x,f(u,y)))) = f(x,f(u,y)).  [para(12(a,1),13(a,1,1))].

given #254 (T,wt=15): 688 f(f(x,f(y,f(z,z))),f(f(z,y),x)) = x.  [para(570(a,2),32(a,1,1,2))].

given #255 (T,wt=15): 690 f(x,f(y,f(z,z))) = f(x,f(y,f(z,y))).  [para(570(a,1),16(a,1,2,1,2)),rewrite([16(7)]),flip(a)].

given #256 (T,wt=15): 694 f(f(f(x,x),y),f(f(z,f(x,z)),y)) = y.  [para(570(a,1),71(a,1,2,1))].

given #257 (T,wt=15): 697 f(f(f(x,y),z),f(f(y,f(x,x)),z)) = z.  [para(570(a,2),71(a,1,2,1))].

given #258 (A,wt=19): 98 f(x,f(f(f(y,x),z),f(f(y,u),x))) = f(f(y,u),x).  [para(13(a,1),13(a,1,1))].

Low Water (keep, True_semantics): wt=27

given #259 (T,wt=15): 775 f(f(x,f(y,f(z,z))),f(x,f(z,x))) = x.  [para(637(a,1),32(a,1,2))].

given #260 (T,wt=15): 778 f(x,f(f(y,y),z)) = f(x,f(z,f(y,z))).  [para(637(a,1),16(a,1,2,1,2)),rewrite([455(8)]),flip(a)].

given #261 (T,wt=15): 821 f(f(x,f(y,y)),f(x,f(z,f(z,y)))) = x.  [para(638(a,1),7(a,1,2,2))].

given #262 (T,wt=15): 850 f(x,f(y,f(z,z))) = f(x,f(y,f(y,z))).  [para(638(a,1),16(a,1,2,1,2)),rewrite([16(7)]),flip(a)].

given #263 (A,wt=23): 102 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(z,x),u)),v))) = z.  [para(17(a,1),9(a,1,2,1)),rewrite([17(14)])].

given #264 (T,wt=15): 853 f(f(f(x,x),y),f(f(z,f(z,x)),y)) = y.  [para(638(a,1),71(a,1,2,1))].

given #265 (T,wt=15): 898 f(f(x,f(f(y,y),z)),f(x,f(z,y))) = x.  [para(652(a,1),7(a,1,2,2))].

given #266 (T,wt=15): 918 f(f(f(f(x,x),y),z),f(f(y,x),z)) = z.  [para(652(a,1),71(a,1,2,1))].

given #267 (T,wt=15): 945 f(f(x,f(f(x,y),z)),f(x,f(u,y))) = x.  [para(24(a,1),7(a,1,2))].

given #268 (A,wt=19): 103 f(x,f(f(f(y,z),x),f(f(x,z),u))) = f(f(y,z),x).  [para(19(a,1),3(a,1,1))].

given #269 (T,wt=15): 1038 f(x,f(f(y,y),z)) = f(x,f(z,f(z,y))).  [para(741(a,1),16(a,1,2,1,2)),rewrite([457(8)]),flip(a)].

given #270 (T,wt=15): 1096 f(x,f(f(x,y),f(z,f(x,z)))) = f(x,y).  [para(637(a,1),43(a,1,2,2))].

given #271 (T,wt=15): 1099 f(x,f(f(x,y),f(z,f(z,x)))) = f(x,y).  [para(741(a,1),43(a,1,2,2))].

given #272 (T,wt=15): 1164 f(f(x,f(y,f(x,f(z,u)))),f(z,x)) = x.  [para(25(a,1),7(a,1,2))].

given #273 (A,wt=17): 104 f(x,f(f(x,y),f(f(f(z,y),x),u))) = f(x,y).  [para(19(a,1),6(a,1,1))].

given #274 (T,wt=15): 1274 f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z).  [para(637(a,1),59(a,1,2,1))].

given #275 (T,wt=15): 1277 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z).  [para(741(a,1),59(a,1,2,1))].

given #276 (T,wt=15): 1312 f(x,f(f(y,x),f(z,f(x,z)))) = f(y,x).  [para(637(a,1),61(a,1,2,2))].

given #277 (T,wt=15): 1318 f(x,f(f(y,x),f(z,f(z,x)))) = f(y,x).  [para(741(a,1),61(a,1,2,2))].

given #278 (A,wt=17): 105 f(x,f(f(y,f(x,f(z,u))),f(z,x))) = f(z,x).  [para(6(a,1),19(a,1,2)),rewrite([2(6)])].

given #279 (T,wt=15): 1493 f(x,f(f(y,f(x,y)),f(z,x))) = f(z,x).  [para(637(a,1),65(a,1,2,1))].

given #280 (T,wt=15): 1496 f(x,f(f(y,f(y,x)),f(z,x))) = f(z,x).  [para(741(a,1),65(a,1,2,1))].

Low Water (keep, True_semantics): wt=25

given #281 (T,wt=15): 1551 f(x,f(f(y,y),f(f(y,z),x))) = f(x,x).  [para(91(a,1),184(a,1,2,2)),rewrite([2(6),570(6,R),2(4)])].

given #282 (T,wt=15): 1571 f(f(x,f(y,y)),z) = f(f(x,f(y,x)),z).  [para(570(a,1),91(a,1,2,2,1)),rewrite([91(5)]),flip(a)].

given #283 (A,wt=19): 106 f(x,f(f(f(y,z),x),f(u,f(x,z)))) = f(f(y,z),x).  [para(19(a,1),7(a,1,1))].

given #284 (T,wt=15): 1575 f(f(f(x,x),y),z) = f(f(y,f(x,y)),z).  [para(637(a,1),91(a,1,2,2,1)),rewrite([489(6)]),flip(a)].

Low Water (displace, True_semantics): id=13735, wt=55

Low Water (displace, True_semantics): id=14150, wt=53

Low Water (displace, True_semantics): id=14139, wt=51

given #285 (T,wt=15): 1578 f(f(x,f(y,y)),z) = f(f(x,f(x,y)),z).  [para(638(a,1),91(a,1,2,2,1)),rewrite([91(5)]),flip(a)].

Low Water (displace, True_semantics): id=14674, wt=49

Low Water (displace, True_semantics): id=13782, wt=47

Low Water (displace, True_semantics): id=15058, wt=45

Low Water (displace, True_semantics): id=15362, wt=43

given #286 (T,wt=15): 1583 f(f(f(x,x),y),z) = f(f(y,f(y,x)),z).  [para(741(a,1),91(a,1,2,2,1)),rewrite([491(6)]),flip(a)].

Low Water (displace, True_semantics): id=15929, wt=41

Low Water (displace, True_semantics): id=16219, wt=39

given #287 (T,wt=15): 1608 f(x,f(f(y,y),f(f(z,y),x))) = f(x,x).  [para(107(a,1),184(a,1,2,2)),rewrite([2(6),570(6,R),2(4)])].

given #288 (A,wt=19): 108 f(x,f(f(f(x,y),z),f(f(u,y),x))) = f(f(u,y),x).  [para(19(a,1),8(a,1,1))].

given #289 (T,wt=15): 1869 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x.  [para(2(a,1),156(a,1,1,2))].

Low Water (displace, True_semantics): id=16381, wt=37

Low Water (displace, True_semantics): id=17547, wt=35

given #290 (T,wt=15): 1870 f(f(x,f(f(x,y),z)),f(f(y,u),x)) = x.  [para(2(a,1),156(a,1,2))].

given #291 (T,wt=15): 1951 f(x,f(y,f(x,f(f(x,y),z)))) = f(x,x).  [para(156(a,1),80(a,1,2)),flip(a)].

Low Water (displace, True_semantics): id=18658, wt=33

given #292 (T,wt=15): 1955 f(f(x,f(f(x,y),z)),f(f(u,y),x)) = x.  [para(107(a,1),156(a,1,2))].

given #293 (A,wt=17): 109 f(x,f(f(y,f(f(z,u),x)),f(x,z))) = f(x,z).  [para(8(a,1),19(a,1,2)),rewrite([2(6)])].

given #294 (T,wt=15): 2154 f(f(x,f(y,f(z,y))),f(x,f(z,x))) = x.  [para(570(a,1),210(a,1,2))].

given #295 (T,wt=15): 2158 f(f(x,f(y,f(z,y))),f(x,f(x,z))) = x.  [para(638(a,1),210(a,1,2))].

Low Water (displace, True_semantics): id=19824, wt=31

given #296 (T,wt=15): 2255 f(f(f(x,f(y,x)),z),f(z,f(y,z))) = z.  [para(570(a,1),220(a,1,2))].

given #297 (T,wt=15): 2260 f(f(f(x,f(y,x)),z),f(z,f(z,y))) = z.  [para(638(a,1),220(a,1,2))].

given #298 (A,wt=23): 110 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(z,y),u)),v))) = z.  [para(19(a,1),9(a,1,2,1)),rewrite([19(14)])].

given #299 (T,wt=15): 2380 f(f(x,f(y,x)),f(x,f(z,f(y,z)))) = x.  [para(637(a,1),227(a,1,1))].

given #300 (T,wt=15): 2390 f(f(x,f(x,y)),f(x,f(z,f(y,z)))) = x.  [para(741(a,1),227(a,1,1))].

given #301 (T,wt=15): 2631 f(f(x,f(y,x)),f(f(z,f(y,z)),x)) = x.  [para(570(a,1),235(a,1,1))].

given #302 (T,wt=15): 2635 f(f(x,f(x,y)),f(f(z,f(y,z)),x)) = x.  [para(638(a,1),235(a,1,1))].

given #303 (A,wt=39): 111 f(f(f(x,y),z),f(y,f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)))) = f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)).  [para(9(a,1),19(a,1,1)),rewrite([2(10)])].

given #304 (T,wt=15): 2829 f(f(x,f(y,f(y,z))),f(x,f(z,x))) = x.  [para(570(a,1),243(a,1,2))].

given #305 (T,wt=15): 2834 f(f(x,f(y,f(y,z))),f(x,f(x,z))) = x.  [para(638(a,1),243(a,1,2))].

Low Water (displace, True_semantics): id=21362, wt=29

given #306 (T,wt=15): 3029 f(f(f(x,f(x,y)),z),f(z,f(y,z))) = z.  [para(570(a,1),249(a,1,2))].

given #307 (T,wt=15): 3035 f(f(f(x,f(x,y)),z),f(z,f(z,y))) = z.  [para(638(a,1),249(a,1,2))].

given #308 (A,wt=19): 114 f(x,f(f(y,f(z,x)),f(x,f(z,u)))) = f(x,f(z,u)).  [para(11(a,1),19(a,1,2)),rewrite([2(6)])].

given #309 (T,wt=15): 3152 f(f(x,f(y,x)),f(x,f(z,f(z,y)))) = x.  [para(637(a,1),254(a,1,1))].

given #310 (T,wt=15): 3162 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x.  [para(741(a,1),254(a,1,1))].

given #311 (T,wt=15): 3283 f(f(x,f(y,x)),f(f(z,f(z,y)),x)) = x.  [para(570(a,1),260(a,1,1))].

given #312 (T,wt=15): 3288 f(f(x,f(x,y)),f(f(z,f(z,y)),x)) = x.  [para(638(a,1),260(a,1,1))].

given #313 (A,wt=17): 115 f(x,f(f(x,y),f(z,f(f(u,y),x)))) = f(x,y).  [para(19(a,1),12(a,1,1))].

given #314 (T,wt=15): 3862 f(f(x,f(f(y,x),z)),f(f(y,u),x)) = x.  [para(275(a,1),107(a,1,2,2)),rewrite([275(12)])].

Low Water (keep, True_semantics): wt=23

given #315 (T,wt=15): 4835 f(f(x,f(f(y,x),z)),f(x,f(u,y))) = x.  [para(286(a,1),2(a,1)),flip(a)].

given #316 (T,wt=15): 4927 f(f(x,f(f(y,x),z)),f(f(u,y),x)) = x.  [para(286(a,1),107(a,1,2,2)),rewrite([286(12)])].

given #317 (T,wt=15): 5131 f(f(x,f(y,f(z,x))),f(x,f(z,u))) = x.  [para(2(a,1),295(a,1,1,2))].

given #318 (A,wt=17): 116 f(x,f(f(y,f(x,f(z,u))),f(u,x))) = f(u,x).  [para(12(a,1),19(a,1,2)),rewrite([2(6)])].

given #319 (T,wt=15): 5175 f(x,f(y,f(x,f(f(y,x),z)))) = f(x,x).  [para(295(a,1),80(a,1,2)),flip(a)].

given #320 (T,wt=15): 6286 f(f(x,f(y,f(x,f(z,u)))),f(u,x)) = x.  [para(348(a,1),107(a,1,2,2)),rewrite([348(12)])].

given #321 (T,wt=15): 6591 f(f(x,f(y,f(z,x))),f(f(z,u),x)) = x.  [para(353(a,1),107(a,1,2,2)),rewrite([353(12)])].

Low Water (displace, True_semantics): id=22099, wt=27

given #322 (T,wt=15): 7154 f(f(x,f(y,f(x,z))),f(f(z,u),x)) = x.  [para(358(a,1),2(a,1)),flip(a)].

given #323 (A,wt=19): 117 f(x,f(f(y,f(x,z)),f(f(z,u),x))) = f(f(z,u),x).  [para(17(a,1),19(a,1,2)),rewrite([2(6)])].

given #324 (T,wt=15): 7385 f(f(x,f(y,f(x,z))),f(f(u,z),x)) = x.  [para(360(a,1),2(a,1)),flip(a)].

given #325 (T,wt=15): 7949 f(f(x,f(y,f(z,x))),f(x,f(u,z))) = x.  [para(364(a,1),2(a,1)),flip(a)].

given #326 (T,wt=15): 8012 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x.  [para(24(a,1),364(a,1,2))].

given #327 (T,wt=15): 8033 f(f(x,f(y,f(z,x))),f(f(u,z),x)) = x.  [para(364(a,1),107(a,1,2,2)),rewrite([364(12)])].

given #328 (A,wt=19): 118 f(x,f(f(y,f(x,z)),f(f(u,z),x))) = f(f(u,z),x).  [para(19(a,1),19(a,1,2)),rewrite([2(6)])].

given #329 (T,wt=15): 9086 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x).  [para(2(a,1),582(a,1,2))].

given #330 (T,wt=15): 9092 f(x,f(y,f(x,f(f(y,y),z)))) = f(x,x).  [para(36(a,1),582(a,1,2,2)),rewrite([2(4)])].

given #331 (T,wt=15): 9114 f(x,f(y,f(x,f(z,f(y,z))))) = f(x,x).  [para(637(a,1),582(a,1,2,1,2)),rewrite([36(6),2(4)])].

given #332 (T,wt=15): 9118 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x).  [para(741(a,1),582(a,1,2,1,2)),rewrite([36(6),2(4)])].

given #333 (A,wt=23): 119 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v))) = x.  [para(3(a,1),14(a,1,2,1)),rewrite([3(14)])].

given #334 (T,wt=15): 9631 f(x,f(f(x,f(y,z)),f(y,c_0))) = f(x,x).  [back_rewrite(9467),rewrite([9472(4)])].

given #335 (T,wt=15): 9640 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0.  [back_rewrite(9458),rewrite([9472(3),9472(5),2(5),9472(10)])].

given #336 (T,wt=15): 9648 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0.  [back_rewrite(9449),rewrite([9472(3),9472(5),2(5),9472(10)])].

given #337 (T,wt=15): 9679 f(f(x,x),f(c_0,f(f(c_0,f(y,x)),z))) = c_0.  [back_rewrite(9415),rewrite([9472(3),9472(5),2(5),9472(10)])].

given #338 (A,wt=31): 120 f(f(x,y),f(f(f(x,y),f(f(y,f(x,z)),u)),f(y,v))) = f(f(x,y),f(f(y,f(x,z)),u)).  [para(14(a,1),6(a,1,1))].

given #339 (T,wt=15): 9686 f(f(x,x),f(c_0,f(f(c_0,f(x,y)),z))) = c_0.  [back_rewrite(9407),rewrite([9472(3),9472(5),2(5),9472(10)])].

given #340 (T,wt=15): 9691 f(f(f(x,f(x,y)),z),f(f(y,c_0),z)) = z.  [back_rewrite(9400),rewrite([9472(5)])].

given #341 (T,wt=15): 9702 f(f(x,f(y,c_0)),f(f(z,f(z,y)),x)) = x.  [back_rewrite(9389),rewrite([9472(2)])].

given #342 (T,wt=15): 9704 f(f(x,f(y,f(y,z))),f(f(z,c_0),x)) = x.  [back_rewrite(9387),rewrite([9472(5)])].

given #343 (A,wt=21): 121 f(f(x,y),f(y,f(z,f(f(x,y),f(f(y,f(x,u)),v))))) = y.  [para(14(a,1),7(a,1,1))].

given #344 (T,wt=15): 9707 f(f(f(x,c_0),y),f(y,f(z,f(z,x)))) = y.  [back_rewrite(9384),rewrite([9472(2)])].

given #345 (T,wt=15): 9708 f(f(f(x,f(x,y)),z),f(z,f(y,c_0))) = z.  [back_rewrite(9382),rewrite([9472(5)])].

given #346 (T,wt=15): 9710 f(f(x,f(y,f(y,z))),f(x,f(z,c_0))) = x.  [back_rewrite(9380),rewrite([9472(5)])].

given #347 (T,wt=15): 9711 f(f(f(x,f(y,x)),z),f(f(y,c_0),z)) = z.  [back_rewrite(9379),rewrite([9472(5)])].

given #348 (A,wt=23): 123 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(x,z),u)),v))) = x.  [para(7(a,1),14(a,1,2,1)),rewrite([7(14)])].

given #349 (T,wt=15): 9715 f(f(x,f(y,c_0)),f(f(z,f(y,z)),x)) = x.  [back_rewrite(9375),rewrite([9472(2)])].

given #350 (T,wt=15): 9717 f(f(x,f(y,f(z,y))),f(f(z,c_0),x)) = x.  [back_rewrite(9373),rewrite([9472(5)])].

given #351 (T,wt=15): 9723 f(f(f(x,c_0),y),f(y,f(z,f(x,z)))) = y.  [back_rewrite(9367),rewrite([9472(2)])].

given #352 (T,wt=15): 9724 f(f(f(x,f(y,x)),z),f(z,f(y,c_0))) = z.  [back_rewrite(9365),rewrite([9472(5)])].

given #353 (A,wt=39): 124 f(f(x,f(y,z)),f(y,f(f(x,f(y,z)),f(f(f(y,z),f(x,u)),v)))) = f(f(x,f(y,z)),f(f(f(y,z),f(x,u)),v)).  [para(14(a,1),8(a,1,2)),rewrite([2(8),2(11)])].

given #354 (T,wt=15): 9726 f(f(x,f(y,f(z,y))),f(x,f(z,c_0))) = x.  [back_rewrite(9363),rewrite([9472(5)])].

given #355 (T,wt=15): 9729 f(x,f(f(y,f(x,c_0)),f(z,x))) = f(z,x).  [back_rewrite(9359),rewrite([9472(2)])].

given #356 (T,wt=15): 9731 f(x,f(f(y,f(x,c_0)),f(x,z))) = f(x,z).  [back_rewrite(9357),rewrite([9472(2)])].

given #357 (T,wt=15): 9737 f(x,f(f(f(x,c_0),y),f(z,x))) = f(z,x).  [back_rewrite(9350),rewrite([9472(2)])].

given #358 (A,wt=23): 125 f(f(x,y),f(f(f(y,z),f(x,y)),f(x,u))) = f(f(y,z),f(x,y)).  [para(8(a,1),14(a,1,2,2,1))].

given #359 (T,wt=15): 9739 f(x,f(f(y,x),f(z,f(x,c_0)))) = f(y,x).  [back_rewrite(9348),rewrite([9472(3)])].

given #360 (T,wt=15): 9741 f(x,f(f(y,x),f(f(x,c_0),z))) = f(y,x).  [back_rewrite(9346),rewrite([9472(3)])].

given #361 (T,wt=15): 9743 f(x,f(f(f(x,c_0),y),f(x,z))) = f(x,z).  [back_rewrite(9344),rewrite([9472(2)])].

given #362 (T,wt=15): 9744 f(x,f(f(x,y),f(z,f(x,c_0)))) = f(x,y).  [back_rewrite(9343),rewrite([9472(3)])].

given #363 (A,wt=27): 127 f(x,f(f(y,x),f(f(x,f(f(f(y,x),f(f(x,f(y,z)),u)),v)),w))) = f(y,x).  [para(14(a,1),9(a,1,2,1)),rewrite([14(17)])].

given #364 (T,wt=15): 9746 f(x,f(f(x,y),f(f(x,c_0),z))) = f(x,y).  [back_rewrite(9341),rewrite([9472(3)])].

given #365 (T,wt=15): 9791 f(x,f(y,f(c_0,f(f(x,x),z)))) = f(x,x).  [back_rewrite(4648),rewrite([9472(2)])].

given #366 (T,wt=15): 9815 f(x,f(f(c_0,f(f(x,x),y)),z)) = f(x,x).  [back_rewrite(2946),rewrite([9472(2)])].

given #367 (T,wt=15): 10092 f(f(f(x,y),z),f(f(c_0,f(y,x)),z)) = z.  [back_rewrite(3502),rewrite([9778(5,R)])].

given #368 (A,wt=37): 128 f(f(f(x,y),f(f(x,f(y,z)),u)),f(f(x,y),f(f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v)),w))) = f(x,y).  [para(9(a,1),14(a,1,2,1)),rewrite([9(22)])].

given #369 (T,wt=15): 10101 f(f(x,f(y,z)),f(f(c_0,f(z,y)),x)) = x.  [back_rewrite(3235),rewrite([9778(5,R)])].

given #370 (T,wt=15): 10107 f(f(f(c_0,f(x,y)),z),f(z,f(y,x))) = z.  [back_rewrite(3150),rewrite([9778(3,R)])].

given #371 (T,wt=15): 10323 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y).  [back_rewrite(1786),rewrite([9757(7,R),2(5)])].

given #372 (T,wt=15): 10324 f(f(f(x,x),y),f(c_0,f(z,x))) = f(z,x).  [back_rewrite(1754),rewrite([9757(7,R),2(5)])].

given #373 (A,wt=19): 129 f(f(x,x),f(f(y,f(x,x)),f(x,z))) = f(y,f(x,x)).  [para(41(a,1),14(a,1,2,2,1))].

given #374 (T,wt=15): 10330 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z).  [back_rewrite(1494),rewrite([9757(7,R),2(5)])].

given #375 (T,wt=15): 10334 f(f(f(x,x),y),f(c_0,f(x,z))) = f(x,z).  [back_rewrite(1275),rewrite([9757(7,R),2(5)])].

given #376 (T,wt=15): 10345 f(f(x,x),f(y,c_0)) = f(f(y,y),f(x,c_0)).  [back_rewrite(815),rewrite([9757(4,R),9757(8,R)])].

given #377 (T,wt=15): 10354 f(f(x,y),f(z,c_0)) = f(f(z,z),f(x,y)).  [back_rewrite(781),rewrite([9757(4,R)])].

given #378 (A,wt=31): 130 f(f(x,y),f(f(f(x,y),f(f(y,f(x,z)),u)),f(v,y))) = f(f(x,y),f(f(y,f(x,z)),u)).  [para(14(a,1),12(a,1,1))].

given #379 (T,wt=15): 10366 f(x,f(f(y,x),f(c_0,f(z,y)))) = f(x,x).  [back_rewrite(541),rewrite([9757(5,R),2(4)])].

given #380 (T,wt=15): 10367 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x).  [back_rewrite(516),rewrite([9757(5,R),2(4)])].

given #381 (T,wt=15): 10368 f(x,f(f(y,x),f(c_0,f(y,z)))) = f(x,x).  [back_rewrite(409),rewrite([9757(5,R),2(4)])].

given #382 (T,wt=15): 10369 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x).  [back_rewrite(389),rewrite([9757(5,R),2(4)])].

given #383 (A,wt=23): 131 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(z,x),u)),v))) = x.  [para(12(a,1),14(a,1,2,1)),rewrite([12(14)])].

given #384 (T,wt=15): 10520 f(f(x,f(c_0,f(y,z))),f(f(z,y),x)) = x.  [back_rewrite(3285),rewrite([9778(3,R)])].

given #385 (T,wt=15): 11092 f(x,f(f(x,y),f(f(c_0,x),z))) = f(x,y).  [para(9472(a,1),29(a,1,2,2,1,1))].

given #386 (T,wt=15): 11094 f(x,f(f(x,y),f(z,f(c_0,x)))) = f(x,y).  [para(9472(a,1),34(a,1,2,2,2,1))].

given #387 (T,wt=15): 11123 f(f(c_0,f(x,y)),f(f(c_0,x),z)) = f(x,y).  [para(16(a,1),9750(a,1,2)),rewrite([9750(5)]),flip(a)].

given #388 (A,wt=31): 132 f(f(x,y),f(f(y,z),f(f(x,y),f(f(y,f(x,u)),v)))) = f(f(x,y),f(f(y,f(x,u)),v)).  [para(14(a,1),13(a,1,1))].

given #389 (T,wt=15): 11124 f(f(c_0,f(x,y)),f(f(x,c_0),z)) = f(x,y).  [para(18(a,1),9750(a,1,2)),rewrite([9750(5)]),flip(a)].

given #390 (T,wt=15): 11130 f(f(c_0,f(x,y)),f(f(c_0,y),z)) = f(x,y).  [para(24(a,1),9750(a,1,2)),rewrite([9750(5)]),flip(a)].

given #391 (T,wt=15): 11131 f(x,f(c_0,f(f(c_0,f(f(c_0,x),y)),z))) = c_0.  [para(9750(a,1),50(a,1,1))].

given #392 (T,wt=15): 11138 f(x,f(c_0,f(f(c_0,f(y,f(c_0,x))),z))) = c_0.  [para(9750(a,1),270(a,1,1))].

given #393 (A,wt=23): 133 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(x,z),u)),v))) = z.  [para(13(a,1),14(a,1,2,1)),rewrite([13(14)])].

given #394 (T,wt=15): 11141 f(x,f(c_0,f(y,f(c_0,f(f(c_0,x),z))))) = c_0.  [para(9750(a,1),345(a,1,1))].

given #395 (T,wt=15): 11142 f(x,f(c_0,f(y,f(c_0,f(z,f(c_0,x)))))) = c_0.  [para(9750(a,1),348(a,1,1))].

given #396 (T,wt=15): 11207 f(x,f(c_0,f(f(c_0,f(f(x,x),y)),z))) = c_0.  [para(9755(a,1),50(a,1,1))].

given #397 (T,wt=15): 11209 f(x,f(c_0,f(f(c_0,f(y,f(x,x))),z))) = c_0.  [para(9755(a,1),270(a,1,1))].

given #398 (A,wt=23): 134 f(f(x,y),f(f(f(x,z),f(x,y)),f(y,u))) = f(f(x,z),f(x,y)).  [para(13(a,1),14(a,1,2,2,1))].

given #399 (T,wt=15): 11212 f(x,f(c_0,f(y,f(c_0,f(f(x,x),z))))) = c_0.  [para(9755(a,1),345(a,1,1))].

given #400 (T,wt=15): 11213 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0.  [para(9755(a,1),348(a,1,1))].

given #401 (T,wt=15): 11217 f(x,f(c_0,f(f(c_0,f(f(x,c_0),y)),z))) = c_0.  [para(9756(a,1),50(a,1,1))].

given #402 (T,wt=15): 11220 f(x,f(c_0,f(f(c_0,f(y,f(x,c_0))),z))) = c_0.  [para(9756(a,1),270(a,1,1))].

given #403 (A,wt=39): 136 f(f(x,f(y,z)),f(z,f(f(x,f(y,z)),f(f(f(y,z),f(x,u)),v)))) = f(f(x,f(y,z)),f(f(f(y,z),f(x,u)),v)).  [para(14(a,1),19(a,1,1)),rewrite([2(10)])].

given #404 (T,wt=15): 11223 f(x,f(c_0,f(y,f(c_0,f(f(x,c_0),z))))) = c_0.  [para(9756(a,1),345(a,1,1))].

given #405 (T,wt=15): 11224 f(x,f(c_0,f(y,f(c_0,f(z,f(x,c_0)))))) = c_0.  [para(9756(a,1),348(a,1,1))].

given #406 (T,wt=15): 11235 f(x,f(f(f(c_0,x),y),f(x,z))) = f(x,z).  [para(9778(a,2),59(a,1,2,1,1))].

given #407 (T,wt=15): 11236 f(x,f(f(y,x),f(f(c_0,x),z))) = f(y,x).  [para(9778(a,2),61(a,1,2,2,1))].

given #408 (A,wt=21): 137 f(f(x,y),f(x,f(f(f(x,y),f(f(f(z,y),x),u)),v))) = x.  [para(19(a,1),14(a,1,2,1)),rewrite([19(13)])].

given #409 (T,wt=15): 11237 f(x,f(f(y,x),f(z,f(c_0,x)))) = f(y,x).  [para(9778(a,2),64(a,1,2,2,2))].

given #410 (T,wt=15): 11239 f(x,f(f(f(c_0,x),y),f(z,x))) = f(z,x).  [para(9778(a,2),65(a,1,2,1,1))].

given #411 (T,wt=15): 11243 f(x,f(f(y,f(c_0,x)),f(x,z))) = f(x,z).  [para(9778(a,2),112(a,1,2,1,2))].

given #412 (T,wt=15): 11244 f(x,f(f(y,f(c_0,x)),f(z,x))) = f(z,x).  [para(9778(a,2),113(a,1,2,1,2))].

given #413 (A,wt=37): 138 f(f(f(x,y),f(f(y,f(x,z)),u)),f(f(x,y),f(f(f(f(x,y),f(f(y,f(x,z)),u)),f(y,v)),w))) = f(x,y).  [para(14(a,1),14(a,1,2,1)),rewrite([14(22)])].

given #414 (T,wt=15): 11245 f(f(x,f(y,f(z,y))),f(x,f(c_0,z))) = x.  [para(9778(a,2),210(a,1,2,2))].

given #415 (T,wt=15): 11246 f(f(f(x,f(y,x)),z),f(z,f(c_0,y))) = z.  [para(9778(a,2),220(a,1,2,2))].

given #416 (T,wt=15): 11247 f(f(f(c_0,x),y),f(y,f(z,f(x,z)))) = y.  [para(9778(a,2),227(a,1,1,1))].

given #417 (T,wt=15): 11248 f(f(x,f(y,f(z,y))),f(f(c_0,z),x)) = x.  [para(9778(a,2),232(a,1,2,1))].

given #418 (A,wt=23): 139 f(f(x,y),f(f(f(x,y),f(z,y)),f(x,u))) = f(f(x,y),f(z,y)).  [para(20(a,1),9(a,1,2,2,1))].

given #419 (T,wt=15): 11249 f(f(x,f(c_0,y)),f(f(z,f(y,z)),x)) = x.  [para(9778(a,2),235(a,1,1,2))].

given #420 (T,wt=15): 11251 f(f(f(x,f(y,x)),z),f(f(c_0,y),z)) = z.  [para(9778(a,2),239(a,1,2,1))].

given #421 (T,wt=15): 11252 f(f(x,f(y,f(y,z))),f(x,f(c_0,z))) = x.  [para(9778(a,2),243(a,1,2,2))].

given #422 (T,wt=15): 11254 f(f(f(x,f(x,y)),z),f(z,f(c_0,y))) = z.  [para(9778(a,2),249(a,1,2,2))].

given #423 (A,wt=17): 140 f(x,f(f(y,f(f(z,u),x)),f(x,u))) = f(x,u).  [para(20(a,1),19(a,1,2)),rewrite([2(6)])].

given #424 (T,wt=15): 11255 f(f(f(c_0,x),y),f(y,f(z,f(z,x)))) = y.  [para(9778(a,2),254(a,1,1,1))].

given #425 (T,wt=15): 11256 f(f(x,f(y,f(y,z))),f(f(c_0,z),x)) = x.  [para(9778(a,2),258(a,1,2,1))].

given #426 (T,wt=15): 11257 f(f(x,f(c_0,y)),f(f(z,f(z,y)),x)) = x.  [para(9778(a,2),260(a,1,1,2))].

given #427 (T,wt=15): 11264 f(f(f(x,f(x,y)),z),f(f(c_0,y),z)) = z.  [para(9778(a,2),265(a,1,2,1))].

given #428 (A,wt=23): 141 f(f(x,y),f(f(f(z,y),f(x,y)),f(x,u))) = f(f(z,y),f(x,y)).  [para(20(a,1),14(a,1,2,2,1))].

given #429 (T,wt=15): 11456 f(f(x,x),f(c_0,y)) = f(f(y,y),f(x,c_0)).  [back_rewrite(10344),rewrite([11231(4,R)])].

given #430 (T,wt=15): 11625 f(f(x,x),f(c_0,y)) = f(f(y,y),f(c_0,x)).  [back_rewrite(1063),rewrite([11231(4,R),11231(8,R)])].

given #431 (T,wt=15): 11630 f(f(x,y),f(c_0,z)) = f(f(z,z),f(x,y)).  [back_rewrite(1041),rewrite([11231(4,R)])].

given #432 (T,wt=15): 12004 f(f(c_0,f(x,y)),f(z,f(x,c_0))) = f(x,y).  [para(67(a,1),9750(a,1,2)),rewrite([9750(5)]),flip(a)].

given #433 (A,wt=25): 142 f(f(x,f(y,z)),f(f(z,f(x,f(y,z))),f(x,u))) = f(z,f(x,f(y,z))).  [para(32(a,1),9(a,1,2,2,1)),rewrite([2(5),2(11)])].

given #434 (T,wt=15): 12244 f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x).  [para(355(a,1),68(a,1,2)),flip(a)].

given #435 (T,wt=15): 12270 f(f(f(x,c_0),y),f(c_0,f(x,z))) = f(x,z).  [para(68(a,1),9750(a,1,2)),rewrite([9750(5)]),flip(a)].

given #436 (T,wt=15): 12325 f(x,f(f(c_0,f(f(c_0,x),y)),z)) = f(c_0,x).  [para(11121(a,1),47(a,1)),rewrite([9750(6)]),flip(a)].

given #437 (T,wt=15): 12340 f(f(x,y),f(c_0,f(y,f(y,f(x,z))))) = c_0.  [para(11(a,1),9692(a,1,2,2,2)),rewrite([2(5)])].

given #438 (A,wt=19): 143 f(x,f(f(y,f(z,x)),f(x,f(u,z)))) = f(x,f(u,z)).  [para(32(a,1),19(a,1,2)),rewrite([2(6)])].

given #439 (T,wt=15): 12345 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0.  [para(17(a,1),9692(a,1,2,2,2)),rewrite([2(5),11229(5,R)])].

given #440 (T,wt=15): 12347 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0.  [para(19(a,1),9692(a,1,2,2,2)),rewrite([2(5),11229(5,R)])].

given #441 (T,wt=15): 12350 f(f(f(x,y),z),f(c_0,f(z,f(z,y)))) = c_0.  [para(20(a,1),9692(a,1,2,2,2)),rewrite([2(5)])].

Low Water (displace, True_semantics): id=24052, wt=25

given #442 (T,wt=15): 12351 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0.  [para(32(a,1),9692(a,1,2,2,2)),rewrite([2(5)])].

given #443 (A,wt=19): 145 f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y).  [para(45(a,1),12(a,1,1))].

given #444 (T,wt=15): 12355 f(f(f(x,y),z),f(c_0,f(z,f(y,z)))) = c_0.  [para(71(a,1),9692(a,1,2,2,2)),rewrite([2(5)])].

given #445 (T,wt=15): 12357 f(x,f(c_0,f(f(c_0,f(y,f(y,x))),z))) = c_0.  [para(9692(a,1),23(a,1,2,1)),rewrite([9692(13)])].

given #446 (T,wt=15): 12361 f(f(c_0,f(x,f(x,y))),f(c_0,f(y,z))) = c_0.  [para(9692(a,1),26(a,1,2,1)),rewrite([9692(13)])].

given #447 (T,wt=15): 12363 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0.  [para(9692(a,1),28(a,1,2,1)),rewrite([9692(13)])].

given #448 (A,wt=19): 146 f(f(x,x),f(f(x,y),f(f(x,x),z))) = f(f(x,x),z).  [para(45(a,1),13(a,1,1))].

given #449 (T,wt=15): 12369 f(f(c_0,f(x,f(x,y))),f(c_0,f(z,y))) = c_0.  [para(9692(a,1),77(a,1,2,1)),rewrite([9692(13)])].

given #450 (T,wt=15): 12410 f(f(x,f(y,f(z,y))),f(c_0,f(x,z))) = c_0.  [para(227(a,1),9692(a,1,2,2,2)),rewrite([2(7),11229(7,R),9755(7)])].

given #451 (T,wt=15): 12413 f(f(f(x,f(y,x)),z),f(c_0,f(z,y))) = c_0.  [para(235(a,1),9692(a,1,2,2,2)),rewrite([2(7),826(7)])].

given #452 (T,wt=15): 12421 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0.  [para(254(a,1),9692(a,1,2,2,2)),rewrite([2(7),11229(7,R),9755(7)])].

given #453 (A,wt=25): 148 f(f(f(x,x),y),f(f(x,x),f(f(f(f(x,x),y),f(x,z)),u))) = f(x,x).  [para(45(a,1),14(a,1,2,1)),rewrite([45(13)])].

given #454 (T,wt=15): 12422 f(f(f(x,f(x,y)),z),f(c_0,f(z,y))) = c_0.  [para(260(a,1),9692(a,1,2,2,2)),rewrite([2(7),826(7)])].

given #455 (T,wt=15): 12730 f(f(x,y),f(c_0,f(x,f(x,f(y,z))))) = c_0.  [para(3(a,1),9713(a,1,2,2,2)),rewrite([2(5)])].

given #456 (T,wt=15): 12733 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0.  [para(7(a,1),9713(a,1,2,2,2)),rewrite([2(5)])].

given #457 (T,wt=15): 12738 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0.  [para(13(a,1),9713(a,1,2,2,2)),rewrite([2(5),11229(5,R)])].

given #458 (A,wt=19): 150 f(f(x,x),f(f(y,f(x,x)),f(z,x))) = f(y,f(x,x)).  [para(62(a,1),12(a,1,1))].

given #459 (T,wt=15): 12744 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0.  [para(71(a,1),9713(a,1,2,2,2)),rewrite([2(5),11229(5,R)])].

given #460 (T,wt=15): 12746 f(x,f(c_0,f(f(c_0,f(y,f(x,y))),z))) = c_0.  [para(9713(a,1),23(a,1,2,1)),rewrite([9713(13)])].

given #461 (T,wt=15): 12747 f(x,f(c_0,f(f(x,y),f(c_0,f(y,z))))) = c_0.  [para(23(a,1),9713(a,1,2,2,2)),rewrite([2(6),11231(6,R)])].

given #462 (T,wt=15): 12750 f(f(c_0,f(x,f(y,x))),f(c_0,f(y,z))) = c_0.  [para(9713(a,1),26(a,1,2,1)),rewrite([9713(13)])].

given #463 (A,wt=19): 151 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)).  [para(62(a,1),13(a,1,1))].

given #464 (T,wt=15): 12751 f(x,f(c_0,f(f(y,x),f(c_0,f(y,z))))) = c_0.  [para(26(a,1),9713(a,1,2,2,2)),rewrite([2(6),11231(6,R)])].

given #465 (T,wt=15): 12752 f(x,f(c_0,f(y,f(c_0,f(z,f(x,z)))))) = c_0.  [para(9713(a,1),28(a,1,2,1)),rewrite([9713(13)])].

given #466 (T,wt=15): 12753 f(x,f(c_0,f(f(x,y),f(c_0,f(z,y))))) = c_0.  [para(28(a,1),9713(a,1,2,2,2)),rewrite([2(6),11231(6,R)])].

given #467 (T,wt=15): 12756 f(f(c_0,f(x,f(y,x))),f(c_0,f(z,y))) = c_0.  [para(9713(a,1),77(a,1,2,1)),rewrite([9713(13)])].

given #468 (A,wt=25): 153 f(f(x,f(y,y)),f(f(y,y),f(f(f(x,f(y,y)),f(y,z)),u))) = f(y,y).  [para(62(a,1),14(a,1,2,1)),rewrite([62(13)])].

given #469 (T,wt=15): 12757 f(x,f(c_0,f(f(y,x),f(c_0,f(z,y))))) = c_0.  [para(77(a,1),9713(a,1,2,2,2)),rewrite([2(6),11231(6,R)])].

given #470 (T,wt=15): 12768 f(x,f(c_0,f(f(y,y),f(f(y,z),x)))) = c_0.  [para(91(a,1),9713(a,1,2,2,2)),rewrite([2(7),570(7,R),2(5)])].

given #471 (T,wt=15): 12769 f(x,f(c_0,f(f(y,y),f(f(z,y),x)))) = c_0.  [para(107(a,1),9713(a,1,2,2,2)),rewrite([2(7),570(7,R),2(5)])].

given #472 (T,wt=15): 12887 f(f(f(x,x),y),f(f(f(x,c_0),z),y)) = y.  [para(9733(a,1),13(a,1,1))].

given #473 (A,wt=33): 154 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(x,y),u)),f(x,v))) = f(f(x,f(y,z)),f(f(x,y),u)).  [para(16(a,1),6(a,1,1))].

given #474 (T,wt=15): 12910 f(x,f(f(y,c_0),z)) = f(x,f(f(y,y),z)).  [para(9733(a,1),16(a,2,2)),rewrite([16(10)])].

given #475 (T,wt=15): 12915 f(f(f(x,x),y),f(f(z,f(x,c_0)),y)) = y.  [para(9733(a,1),71(a,1,1))].

given #476 (T,wt=15): 12969 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(y,y)).  [para(9733(a,1),570(a,1)),rewrite([9757(9,R)]),flip(a)].

given #477 (T,wt=15): 12971 f(f(x,c_0),f(y,y)) = f(f(x,x),f(y,c_0)).  [para(9733(a,2),570(a,1)),rewrite([9757(8,R)])].

Low Water (displace, True_semantics): id=26321, wt=23

given #478 (A,wt=23): 155 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(f(x,y),v))))) = x.  [para(16(a,1),7(a,1,1))].

given #479 (T,wt=15): 12975 f(f(x,c_0),f(c_0,y)) = f(f(x,x),f(y,y)).  [para(9733(a,1),638(a,1)),rewrite([11231(9,R)]),flip(a)].

given #480 (T,wt=15): 12978 f(f(x,c_0),f(y,y)) = f(f(x,x),f(c_0,y)).  [para(9733(a,2),638(a,1)),rewrite([11231(8,R)])].

given #481 (T,wt=15): 13029 f(f(f(x,c_0),y),z) = f(f(f(x,x),y),z).  [para(9733(a,1),91(a,2,1)),rewrite([91(8)])].

given #482 (T,wt=15): 13420 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,y))).  [para(9735(a,1),16(a,2,2)),rewrite([16(10)])].

given #483 (A,wt=31): 157 f(f(x,y),f(f(f(x,y),f(f(x,f(z,y)),u)),f(x,v))) = f(f(x,y),f(f(x,f(z,y)),u)).  [para(7(a,1),16(a,1,2,2,1))].

given #484 (T,wt=15): 13431 f(f(x,c_0),f(y,c_0)) = f(f(y,y),f(x,x)).  [para(9735(a,1),570(a,1)),rewrite([9757(9,R)]),flip(a)].

given #485 (T,wt=15): 13432 f(f(x,c_0),f(c_0,y)) = f(f(y,y),f(x,x)).  [para(9735(a,1),638(a,1)),rewrite([11231(9,R)]),flip(a)].

given #486 (T,wt=15): 13446 f(f(f(x,c_0),y),z) = f(f(y,f(x,x)),z).  [para(9735(a,1),91(a,1,2,2,1)),rewrite([13033(7)]),flip(a)].

given #487 (T,wt=15): 13561 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(c_0,x)).  [para(9735(a,1),54(a,1,2,1)),rewrite([13012(9)])].

given #488 (A,wt=41): 158 f(f(f(x,y),f(z,u)),f(x,f(f(f(x,y),f(z,u)),f(f(f(x,y),z),v)))) = f(f(f(x,y),f(z,u)),f(f(f(x,y),z),v)).  [para(16(a,1),8(a,1,2)),rewrite([2(8),2(12)])].

given #489 (T,wt=15): 13606 f(f(x,c_0),f(y,y)) = f(f(y,c_0),f(x,x)).  [para(9735(a,2),9733(a,2))].

given #490 (T,wt=15): 13608 f(f(x,f(y,z)),f(x,f(y,f(z,c_0)))) = x.  [para(9747(a,1),7(a,1,2,2)),rewrite([2(7)])].

given #491 (T,wt=15): 13611 f(f(f(x,f(y,c_0)),z),f(z,f(x,y))) = z.  [para(9747(a,1),12(a,1,2,2))].

given #492 (T,wt=15): 13613 f(f(f(x,y),z),f(z,f(x,f(y,c_0)))) = z.  [para(9747(a,1),19(a,1,1,1))].

given #493 (A,wt=17): 159 f(f(x,y),f(x,f(f(f(x,y),f(y,z)),u))) = x.  [para(8(a,1),16(a,1,2,1)),rewrite([8(11)])].

given #494 (T,wt=15): 13616 f(f(x,f(y,f(z,c_0))),f(f(y,z),x)) = x.  [para(9747(a,1),20(a,1,2,1))].

given #495 (T,wt=15): 13617 f(f(x,f(y,z)),f(f(y,f(z,c_0)),x)) = x.  [para(9747(a,1),32(a,1,1,2))].

given #496 (T,wt=15): 13619 f(f(f(x,y),z),f(f(x,f(y,c_0)),z)) = z.  [para(9747(a,1),71(a,1,2,1)),rewrite([2(7)])].

given #497 (T,wt=15): 13678 f(f(f(f(x,c_0),y),z),f(z,f(z,x))) = z.  [para(9747(a,1),358(a,1,2,2))].

given #498 (A,wt=31): 160 f(f(x,y),f(f(f(x,y),f(f(f(y,z),x),u)),f(x,v))) = f(f(x,y),f(f(f(y,z),x),u)).  [para(8(a,1),16(a,1,2,2,1))].

given #499 (T,wt=15): 13681 f(f(f(x,f(y,c_0)),z),f(z,f(z,y))) = z.  [para(9747(a,1),360(a,1,2,2))].

given #500 (T,wt=15): 13688 f(f(x,f(f(y,c_0),z)),f(x,f(x,y))) = x.  [para(9747(a,1),472(a,1,2,2))].

given #501 (T,wt=15): 13690 f(f(x,f(y,f(z,c_0))),f(x,f(x,z))) = x.  [para(9747(a,1),474(a,1,2,2))].

given #502 (T,wt=15): 13852 f(f(x,f(x,y)),f(x,f(f(y,c_0),z))) = x.  [para(9748(a,1),6(a,1,1))].

given #503 (A,wt=31): 162 f(x,f(f(x,f(y,z)),f(f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v)),w))) = f(x,f(y,z)).  [para(16(a,1),9(a,1,2,1)),rewrite([16(18)])].

given #504 (T,wt=15): 13858 f(f(x,f(y,z)),f(x,f(f(z,c_0),y))) = x.  [para(9748(a,2),7(a,1,2,2))].

given #505 (T,wt=15): 13873 f(f(f(x,y),z),f(z,f(f(y,c_0),x))) = z.  [para(9748(a,2),12(a,1,2,2))].

given #506 (T,wt=15): 13875 f(f(x,f(x,y)),f(f(f(y,c_0),z),x)) = x.  [para(9748(a,1),13(a,1,1))].

given #507 (T,wt=15): 13880 f(f(f(f(x,c_0),y),z),f(z,f(y,x))) = z.  [para(9748(a,2),19(a,1,1,1))].

given #508 (A,wt=39): 163 f(x,f(f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v)),f(f(x,y),w))) = f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v)).  [para(9(a,1),16(a,1,2,2,1))].

given #509 (T,wt=15): 13887 f(f(x,f(y,z)),f(f(f(z,c_0),y),x)) = x.  [para(9748(a,2),20(a,1,2,1))].

given #510 (T,wt=15): 13891 f(f(x,f(f(y,c_0),z)),f(f(z,y),x)) = x.  [para(9748(a,2),32(a,1,1,2))].

given #511 (T,wt=15): 13896 f(x,f(f(y,c_0),z)) = f(x,f(z,f(z,y))).  [para(9748(a,1),16(a,2,2)),rewrite([16(10)])].

given #512 (T,wt=15): 13900 f(f(f(x,y),z),f(f(f(y,c_0),x),z)) = z.  [para(9748(a,2),71(a,1,2,1))].

given #513 (A,wt=19): 166 f(f(x,f(y,z)),f(x,f(f(y,f(x,f(y,z))),u))) = x.  [para(11(a,1),16(a,1,2,1)),rewrite([2(5),11(12)])].

given #514 (T,wt=15): 13986 f(f(f(x,c_0),y),z) = f(f(y,f(y,x)),z).  [para(9748(a,1),91(a,2,1)),rewrite([91(8)])].

given #515 (T,wt=15): 14252 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(c_0,y)).  [para(9748(a,1),9735(a,2)),rewrite([11231(9,R)])].

given #516 (T,wt=15): 14269 f(x,f(y,f(z,c_0))) = f(x,f(y,f(y,z))).  [para(9752(a,1),16(a,1,2,1,2)),rewrite([16(7)]),flip(a)].

given #517 (T,wt=15): 14283 f(f(x,f(y,c_0)),z) = f(f(x,f(x,y)),z).  [para(9752(a,1),91(a,1,2,2,1)),rewrite([91(5)]),flip(a)].

given #518 (A,wt=33): 167 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(y,x),u)),f(x,v))) = f(f(x,f(y,z)),f(f(y,x),u)).  [para(11(a,1),16(a,1,2,2,1))].

given #519 (T,wt=15): 14387 f(f(x,c_0),f(c_0,y)) = f(f(x,x),f(y,c_0)).  [para(9752(a,1),9733(a,1)),rewrite([11231(6,R)])].

given #520 (T,wt=15): 14392 f(f(x,c_0),f(c_0,y)) = f(f(y,c_0),f(x,x)).  [para(9752(a,1),9735(a,1)),rewrite([11231(6,R)])].

given #521 (T,wt=15): 14433 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,z))).  [para(9754(a,1),16(a,2,2)),rewrite([16(10)])].

given #522 (T,wt=15): 14502 f(f(f(x,c_0),y),z) = f(f(y,f(x,y)),z).  [para(9754(a,1),91(a,2,1)),rewrite([91(8)])].

given #523 (A,wt=33): 168 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(x,y),u)),f(v,x))) = f(f(x,f(y,z)),f(f(x,y),u)).  [para(16(a,1),12(a,1,1))].

given #524 (T,wt=15): 14734 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,y))).  [para(9757(a,1),16(a,1,2,1,2)),rewrite([16(7)]),flip(a)].

given #525 (T,wt=15): 14765 f(f(x,f(y,c_0)),z) = f(f(x,f(y,x)),z).  [para(9757(a,1),91(a,1,2,2,1)),rewrite([91(5)]),flip(a)].

given #526 (T,wt=15): 15102 f(f(f(c_0,x),y),f(c_0,f(x,z))) = f(x,z).  [para(16(a,1),9761(a,1,2)),rewrite([11123(14)])].

given #527 (T,wt=15): 15106 f(f(f(c_0,x),y),f(c_0,f(z,x))) = f(z,x).  [para(24(a,1),9761(a,1,2)),rewrite([11130(14)])].

given #528 (A,wt=31): 169 f(f(x,y),f(f(f(x,y),f(f(y,f(z,x)),u)),f(y,v))) = f(f(x,y),f(f(y,f(z,x)),u)).  [para(12(a,1),16(a,1,2,2,1))].

given #529 (T,wt=15): 15123 f(f(x,f(y,c_0)),f(c_0,f(y,z))) = f(y,z).  [para(67(a,1),9761(a,1,2)),rewrite([12004(14)])].

given #530 (T,wt=15): 15165 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,z))).  [para(9765(a,1),16(a,1,2,1,2)),rewrite([16(7)]),flip(a)].

given #531 (T,wt=15): 15174 f(f(x,f(y,c_0)),z) = f(f(x,f(y,y)),z).  [para(9765(a,1),91(a,1,2,2,1)),rewrite([91(5)]),flip(a)].

given #532 (T,wt=15): 15361 f(f(c_0,f(x,y)),f(z,f(c_0,x))) = f(x,y).  [para(73(a,1),9750(a,1,2)),rewrite([9750(5)]),flip(a)].

given #533 (A,wt=33): 170 f(f(x,f(y,z)),f(f(x,u),f(f(x,f(y,z)),f(f(x,y),v)))) = f(f(x,f(y,z)),f(f(x,y),v)).  [para(16(a,1),13(a,1,1))].

given #534 (T,wt=15): 15386 f(f(x,f(c_0,y)),f(c_0,f(y,z))) = f(y,z).  [para(73(a,1),9761(a,1,2)),rewrite([15361(14)])].

given #535 (T,wt=15): 15574 f(f(c_0,f(x,y)),f(f(y,c_0),z)) = f(x,y).  [para(74(a,1),9750(a,1,2)),rewrite([9750(5)]),flip(a)].

given #536 (T,wt=15): 15601 f(f(f(x,c_0),y),f(c_0,f(z,x))) = f(z,x).  [para(74(a,1),9761(a,1,2)),rewrite([15574(14)])].

given #537 (T,wt=15): 15946 f(f(f(x,x),y),f(f(f(c_0,x),z),y)) = y.  [para(11113(a,1),239(a,1,1,1,2)),rewrite([2(7),9750(7),2(7)])].

given #538 (A,wt=17): 171 f(f(x,y),f(y,f(f(f(x,y),f(x,z)),u))) = y.  [para(13(a,1),16(a,1,2,1)),rewrite([13(11)])].

given #539 (T,wt=15): 16053 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,z))).  [para(11226(a,1),16(a,1,2,1,2)),rewrite([16(7)]),flip(a)].

given #540 (T,wt=15): 16058 f(f(f(x,x),y),f(f(z,f(c_0,x)),y)) = y.  [para(11226(a,2),71(a,1,2,1))].

given #541 (T,wt=15): 16089 f(f(c_0,x),f(y,c_0)) = f(f(y,y),f(x,x)).  [para(11226(a,1),637(a,1)),rewrite([9757(9,R)]),flip(a)].

given #542 (T,wt=15): 16094 f(f(c_0,x),f(c_0,y)) = f(f(y,y),f(x,x)).  [para(11226(a,1),741(a,1)),rewrite([11231(9,R)]),flip(a)].

given #543 (A,wt=31): 172 f(f(x,y),f(f(f(x,y),f(f(f(x,z),y),u)),f(y,v))) = f(f(x,y),f(f(f(x,z),y),u)).  [para(13(a,1),16(a,1,2,2,1))].

given #544 (T,wt=15): 16109 f(f(x,f(c_0,y)),z) = f(f(x,f(y,y)),z).  [para(11226(a,1),91(a,1,2,2,1)),rewrite([91(5)]),flip(a)].

given #545 (T,wt=15): 16295 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,x)).  [para(11226(a,1),9735(a,1)),flip(a)].

given #546 (T,wt=15): 16299 f(f(c_0,x),f(c_0,y)) = f(f(y,c_0),f(x,x)).  [para(11226(a,1),9748(a,1)),rewrite([11231(10,R)]),flip(a)].

given #547 (T,wt=15): 16399 f(f(c_0,f(x,y)),f(z,f(c_0,y))) = f(x,y).  [para(78(a,1),9750(a,1,2)),rewrite([9750(5)]),flip(a)].

given #548 (A,wt=33): 174 f(f(f(x,y),z),f(f(f(f(x,y),z),f(f(z,x),u)),f(z,v))) = f(f(f(x,y),z),f(f(z,x),u)).  [para(17(a,1),16(a,1,2,2,1))].

given #549 (T,wt=15): 16435 f(f(x,f(c_0,y)),f(c_0,f(z,y))) = f(z,y).  [para(78(a,1),9761(a,1,2)),rewrite([16399(14)])].

given #550 (T,wt=15): 16482 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,y))).  [para(11229(a,1),16(a,1,2,1,2)),rewrite([16(7)]),flip(a)].

given #551 (T,wt=15): 16488 f(f(f(x,y),z),f(f(y,f(c_0,x)),z)) = z.  [para(11229(a,2),71(a,1,2,1))].

given #552 (T,wt=15): 16553 f(f(x,f(c_0,y)),z) = f(f(x,f(y,x)),z).  [para(11229(a,1),91(a,1,2,2,1)),rewrite([91(5)]),flip(a)].

given #553 (A,wt=41): 175 f(f(f(x,y),f(z,u)),f(y,f(f(f(x,y),f(z,u)),f(f(f(x,y),z),v)))) = f(f(f(x,y),f(z,u)),f(f(f(x,y),z),v)).  [para(16(a,1),19(a,1,1)),rewrite([2(11)])].

given #554 (T,wt=15): 16743 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,c_0)).  [para(11229(a,1),9735(a,1)),rewrite([9757(6,R)]),flip(a)].

given #555 (T,wt=15): 16793 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,z))).  [para(11230(a,1),16(a,2,2)),rewrite([16(10)])].

given #556 (T,wt=15): 16843 f(f(f(c_0,x),y),z) = f(f(y,f(x,y)),z).  [para(11230(a,1),91(a,2,1)),rewrite([91(8)])].

given #557 (T,wt=15): 17040 f(f(c_0,x),f(y,c_0)) = f(f(c_0,y),f(x,x)).  [para(11230(a,1),11226(a,1)),rewrite([9757(6,R)])].

given #558 (A,wt=33): 176 f(f(f(x,y),z),f(f(f(f(x,y),z),f(f(z,y),u)),f(z,v))) = f(f(f(x,y),z),f(f(z,y),u)).  [para(19(a,1),16(a,1,2,2,1))].

given #559 (T,wt=15): 17070 f(x,f(y,f(c_0,z))) = f(x,f(y,f(y,z))).  [para(11231(a,1),16(a,1,2,1,2)),rewrite([16(7)]),flip(a)].

given #560 (T,wt=15): 17121 f(f(x,f(c_0,y)),z) = f(f(x,f(x,y)),z).  [para(11231(a,1),91(a,1,2,2,1)),rewrite([91(5)]),flip(a)].

given #561 (T,wt=15): 17311 f(x,f(f(c_0,y),z)) = f(x,f(z,f(z,y))).  [para(11233(a,1),16(a,2,2)),rewrite([16(10)])].

given #562 (T,wt=15): 17333 f(f(f(c_0,x),y),z) = f(f(y,f(y,x)),z).  [para(11233(a,1),91(a,2,1)),rewrite([91(8)])].

given #563 (A,wt=41): 177 f(f(f(x,f(y,z)),f(f(x,y),u)),f(f(x,f(y,z)),f(f(f(f(x,f(y,z)),f(f(x,y),u)),f(x,v)),w))) = f(x,f(y,z)).  [para(16(a,1),14(a,1,2,1)),rewrite([16(23)])].

given #564 (T,wt=15): 17625 f(f(c_0,f(x,y)),f(z,f(y,c_0))) = f(x,y).  [para(364(a,1),11234(a,1,2)),rewrite([2(5),9750(5)]),flip(a)].

given #565 (T,wt=15): 17665 f(x,f(f(c_0,y),z)) = f(x,f(f(y,y),z)).  [para(11240(a,1),16(a,1,2,1,2)),rewrite([16055(9)]),flip(a)].

given #566 (T,wt=15): 17699 f(f(c_0,x),f(y,c_0)) = f(f(x,x),f(y,y)).  [para(11240(a,1),570(a,1)),rewrite([9757(9,R)]),flip(a)].

given #567 (T,wt=15): 17700 f(f(c_0,x),f(y,y)) = f(f(x,x),f(y,c_0)).  [para(11240(a,1),570(a,2)),rewrite([16303(9)])].

given #568 (A,wt=39): 178 f(x,f(f(x,f(f(f(y,x),f(f(x,f(y,z)),u)),v)),f(f(y,x),w))) = f(x,f(f(f(y,x),f(f(x,f(y,z)),u)),v)).  [para(14(a,1),16(a,1,2,2,1))].

given #569 (T,wt=15): 17701 f(f(c_0,x),f(c_0,y)) = f(f(x,x),f(y,y)).  [para(11240(a,1),638(a,1)),rewrite([11231(9,R)]),flip(a)].

given #570 (T,wt=15): 17704 f(f(c_0,x),f(y,y)) = f(f(x,x),f(c_0,y)).  [para(11240(a,2),638(a,1)),rewrite([11231(8,R)])].

given #571 (T,wt=15): 17740 f(f(f(c_0,x),y),z) = f(f(f(x,x),y),z).  [para(11240(a,1),91(a,2,1)),rewrite([91(8)])].

given #572 (T,wt=15): 17986 f(f(c_0,x),f(c_0,y)) = f(f(x,x),f(y,c_0)).  [para(11240(a,1),9752(a,1)),rewrite([11231(10,R)]),flip(a)].

given #573 (A,wt=17): 179 f(f(x,y),f(x,f(f(f(x,y),f(z,y)),u))) = x.  [para(20(a,1),16(a,1,2,1)),rewrite([20(11)])].

given #574 (T,wt=15): 17989 f(f(c_0,x),f(y,c_0)) = f(f(x,x),f(c_0,y)).  [para(11240(a,2),9752(a,1)),rewrite([11231(9,R)])].

given #575 (T,wt=15): 18021 f(x,f(f(y,y),z)) = f(x,f(z,f(c_0,y))).  [para(11241(a,1),16(a,1,2,1,2)),rewrite([16093(9)]),flip(a)].

given #576 (T,wt=15): 18022 f(f(f(x,x),y),z) = f(f(y,f(c_0,x)),z).  [para(11241(a,1),91(a,1,2,2,1)),rewrite([16845(7)]),flip(a)].

given #577 (T,wt=15): 18103 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,y))).  [para(11242(a,1),16(a,2,2)),rewrite([16(10)])].

given #578 (A,wt=31): 180 f(f(x,y),f(f(f(x,y),f(f(f(z,y),x),u)),f(x,v))) = f(f(x,y),f(f(f(z,y),x),u)).  [para(20(a,1),16(a,1,2,2,1))].

given #579 (T,wt=15): 18109 f(f(f(c_0,x),y),z) = f(f(y,f(x,x)),z).  [para(11242(a,1),91(a,1,2,2,1)),rewrite([17743(7)]),flip(a)].

given #580 (T,wt=15): 18191 f(f(c_0,x),f(y,y)) = f(f(c_0,y),f(x,x)).  [para(11242(a,1),11226(a,1))].

given #581 (T,wt=15): 18367 f(f(x,y),f(c_0,f(f(c_0,f(y,x)),z))) = c_0.  [para(12376(a,1),23(a,1,2,1)),rewrite([12376(13)])].

given #582 (T,wt=15): 18370 f(f(x,y),f(c_0,f(z,f(c_0,f(y,x))))) = c_0.  [para(12376(a,1),28(a,1,2,1)),rewrite([12376(13)])].

given #583 (A,wt=19): 182 f(f(x,f(y,z)),f(x,f(f(z,f(x,f(y,z))),u))) = x.  [para(32(a,1),16(a,1,2,1)),rewrite([2(5),32(12)])].

given #584 (T,wt=15): 18385 f(f(x,f(c_0,f(y,z))),f(x,f(z,y))) = x.  [para(12376(a,1),243(a,1,1,2,2)),rewrite([2(3),9778(11,R),9750(9)])].

given #585 (T,wt=15): 18387 f(f(f(c_0,f(x,y)),z),f(f(y,x),z)) = z.  [para(12376(a,1),265(a,1,1,1,2)),rewrite([2(3),9778(11,R),9750(9)])].

given #586 (T,wt=15): 18430 f(f(x,f(y,x)),f(c_0,f(f(y,c_0),x))) = c_0.  [para(9754(a,2),12376(a,1,2,2)),rewrite([2(2)])].

Low Water (keep, True_semantics): wt=21

given #587 (T,wt=15): 18442 f(f(x,f(y,x)),f(c_0,f(f(c_0,y),x))) = c_0.  [para(11229(a,1),12376(a,1,1))].

given #588 (A,wt=33): 183 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(z,x),u)),f(x,v))) = f(f(x,f(y,z)),f(f(z,x),u)).  [para(32(a,1),16(a,1,2,2,1))].

given #589 (T,wt=15): 18453 f(x,f(f(y,y),z)) = f(x,f(z,f(y,c_0))).  [para(12855(a,1),16(a,1,2,1,2)),rewrite([15171(9)]),flip(a)].

given #590 (T,wt=15): 18454 f(f(f(x,x),y),z) = f(f(y,f(x,c_0)),z).  [para(12855(a,1),91(a,1,2,2,1)),rewrite([13032(7)]),flip(a)].

given #591 (T,wt=15): 18527 f(f(c_0,f(f(x,x),y)),f(y,f(x,y))) = c_0.  [para(570(a,1),18356(a,1,2))].

given #592 (T,wt=15): 18528 f(f(c_0,f(x,f(y,y))),f(x,f(y,x))) = c_0.  [para(570(a,2),18356(a,1,1,2)),rewrite([2(6)])].

given #593 (A,wt=41): 185 f(x,f(f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v)),f(f(x,f(y,z)),w))) = f(x,f(f(f(x,f(y,z)),f(f(x,y),u)),v)).  [para(16(a,1),16(a,1,2,2,1))].

given #594 (T,wt=15): 18529 f(f(c_0,f(x,f(y,x))),f(x,f(y,y))) = c_0.  [para(570(a,2),18356(a,1,2)),rewrite([2(3)])].

given #595 (T,wt=15): 18531 f(f(c_0,f(f(x,x),y)),f(y,f(y,x))) = c_0.  [para(638(a,1),18356(a,1,2))].

given #596 (T,wt=15): 18532 f(f(c_0,f(x,f(y,y))),f(x,f(x,y))) = c_0.  [para(638(a,2),18356(a,1,1,2)),rewrite([2(6)])].

given #597 (T,wt=15): 18533 f(f(c_0,f(x,f(x,y))),f(x,f(y,y))) = c_0.  [para(638(a,2),18356(a,1,2)),rewrite([2(3)])].

given #598 (A,wt=17): 186 f(x,f(f(y,x),f(f(f(z,y),x),u))) = f(y,x).  [para(71(a,1),3(a,1,1))].

given #599 (T,wt=15): 18537 f(f(c_0,f(f(x,x),y)),f(y,f(x,c_0))) = c_0.  [para(9733(a,1),18356(a,1,1,2))].

given #600 (T,wt=15): 18538 f(f(c_0,f(x,f(y,c_0))),f(f(y,y),x)) = c_0.  [para(9733(a,1),18356(a,1,2))].

given #601 (T,wt=15): 18539 f(f(c_0,f(f(x,c_0),y)),f(y,f(x,x))) = c_0.  [para(9733(a,2),18356(a,1,1,2))].

given #602 (T,wt=15): 18540 f(f(c_0,f(x,f(y,y))),f(f(y,c_0),x)) = c_0.  [para(9733(a,2),18356(a,1,2))].

given #603 (A,wt=19): 187 f(x,f(f(y,f(x,z)),f(x,f(z,u)))) = f(x,f(z,u)).  [para(3(a,1),71(a,1,1))].

given #604 (T,wt=15): 18541 f(f(c_0,f(x,f(y,y))),f(x,f(y,c_0))) = c_0.  [para(9735(a,1),18356(a,1,1,2))].

given #605 (T,wt=15): 18542 f(f(c_0,f(x,f(y,c_0))),f(x,f(y,y))) = c_0.  [para(9735(a,1),18356(a,1,2))].

given #606 (T,wt=15): 18543 f(f(c_0,f(f(x,c_0),y)),f(f(x,x),y)) = c_0.  [para(9735(a,2),18356(a,1,1,2))].

given #607 (T,wt=15): 18544 f(f(c_0,f(f(x,x),y)),f(f(x,c_0),y)) = c_0.  [para(9735(a,2),18356(a,1,2))].

given #608 (A,wt=19): 188 f(x,f(f(f(y,z),x),f(f(z,x),u))) = f(f(y,z),x).  [para(71(a,1),6(a,1,1))].

given #609 (T,wt=15): 18545 f(f(c_0,f(x,f(x,y))),f(x,f(y,c_0))) = c_0.  [para(9748(a,1),18356(a,1,1,2))].

given #610 (T,wt=15): 18546 f(f(c_0,f(x,f(y,c_0))),f(x,f(x,y))) = c_0.  [para(9748(a,1),18356(a,1,2))].

given #611 (T,wt=15): 18547 f(f(c_0,f(f(x,c_0),y)),f(y,f(y,x))) = c_0.  [para(9748(a,2),18356(a,1,1,2)),rewrite([2(7)])].

given #612 (T,wt=15): 18548 f(f(c_0,f(x,f(x,y))),f(f(y,c_0),x)) = c_0.  [para(9748(a,2),18356(a,1,2)),rewrite([2(3)])].

given #613 (A,wt=17): 189 f(x,f(f(y,x),f(z,f(f(u,y),x)))) = f(y,x).  [para(71(a,1),7(a,1,1))].

given #614 (T,wt=15): 18549 f(f(c_0,f(x,f(y,x))),f(x,f(y,c_0))) = c_0.  [para(9754(a,1),18356(a,1,1,2))].

given #615 (T,wt=15): 18550 f(f(c_0,f(x,f(y,c_0))),f(x,f(y,x))) = c_0.  [para(9754(a,1),18356(a,1,2))].

given #616 (T,wt=15): 18551 f(f(c_0,f(f(x,c_0),y)),f(y,f(x,y))) = c_0.  [para(9754(a,2),18356(a,1,1,2)),rewrite([2(7)])].

given #617 (T,wt=15): 18552 f(f(c_0,f(x,f(y,x))),f(f(y,c_0),x)) = c_0.  [para(9754(a,2),18356(a,1,2)),rewrite([2(3)])].

given #618 (A,wt=19): 190 f(x,f(f(y,f(x,z)),f(x,f(u,z)))) = f(x,f(u,z)).  [para(7(a,1),71(a,1,1))].

given #619 (T,wt=15): 18553 f(f(c_0,f(x,f(y,y))),f(f(c_0,y),x)) = c_0.  [para(11226(a,1),18356(a,1,1,2))].

given #620 (T,wt=15): 18554 f(f(c_0,f(f(c_0,x),y)),f(y,f(x,x))) = c_0.  [para(11226(a,1),18356(a,1,2))].

given #621 (T,wt=15): 18555 f(f(c_0,f(x,f(c_0,y))),f(f(y,y),x)) = c_0.  [para(11226(a,2),18356(a,1,1,2))].

given #622 (T,wt=15): 18556 f(f(c_0,f(f(x,x),y)),f(y,f(c_0,x))) = c_0.  [para(11226(a,2),18356(a,1,2))].

given #623 (A,wt=21): 191 f(f(x,y),f(y,f(f(f(x,y),f(f(f(z,x),y),u)),v))) = y.  [para(71(a,1),9(a,1,2,1)),rewrite([71(13)])].

given #624 (T,wt=15): 18559 f(f(c_0,f(f(c_0,x),y)),f(y,f(x,y))) = c_0.  [para(11229(a,1),18356(a,1,2))].

given #625 (T,wt=15): 18560 f(f(c_0,f(x,f(c_0,y))),f(x,f(y,x))) = c_0.  [para(11229(a,2),18356(a,1,1,2)),rewrite([2(7)])].

given #626 (T,wt=15): 18561 f(f(c_0,f(x,f(y,x))),f(x,f(c_0,y))) = c_0.  [para(11229(a,2),18356(a,1,2)),rewrite([2(3)])].

given #627 (T,wt=15): 18563 f(f(c_0,f(f(c_0,x),y)),f(y,f(y,x))) = c_0.  [para(11231(a,1),18356(a,1,2))].

given #628 (A,wt=23): 192 f(f(x,y),f(f(f(x,y),f(z,x)),f(y,u))) = f(f(x,y),f(z,x)).  [para(71(a,1),9(a,1,2,2,1))].

given #629 (T,wt=15): 18564 f(f(c_0,f(x,f(c_0,y))),f(x,f(x,y))) = c_0.  [para(11231(a,2),18356(a,1,1,2)),rewrite([2(7)])].

given #630 (T,wt=15): 18565 f(f(c_0,f(x,f(x,y))),f(x,f(c_0,y))) = c_0.  [para(11231(a,2),18356(a,1,2)),rewrite([2(3)])].

given #631 (T,wt=15): 18566 f(f(c_0,f(x,f(c_0,y))),f(x,f(y,y))) = c_0.  [para(11241(a,1),18356(a,1,1,2))].

given #632 (T,wt=15): 18567 f(f(c_0,f(x,f(y,y))),f(x,f(c_0,y))) = c_0.  [para(11241(a,1),18356(a,1,2))].

given #633 (A,wt=31): 193 f(f(x,y),f(f(z,x),f(f(x,y),f(f(x,f(y,u)),v)))) = f(f(x,y),f(f(x,f(y,u)),v)).  [para(9(a,1),71(a,1,1))].

given #634 (T,wt=15): 18568 f(f(c_0,f(f(x,x),y)),f(f(c_0,x),y)) = c_0.  [para(11241(a,2),18356(a,1,1,2))].

given #635 (T,wt=15): 18569 f(f(c_0,f(f(c_0,x),y)),f(f(x,x),y)) = c_0.  [para(11241(a,2),18356(a,1,2))].

given #636 (T,wt=15): 18574 f(f(c_0,f(x,y)),f(x,f(z,f(x,y)))) = c_0.  [para(3(a,1),9784(a,1,2,2)),rewrite([9778(3,R),2(6)])].

given #637 (T,wt=15): 18576 f(f(c_0,f(x,y)),f(y,f(z,f(x,y)))) = c_0.  [para(6(a,1),9784(a,1,2,2)),rewrite([9778(3,R),2(6)])].

given #638 (A,wt=19): 194 f(x,f(f(f(y,z),x),f(u,f(z,x)))) = f(f(y,z),x).  [para(71(a,1),12(a,1,1))].

given #639 (T,wt=15): 18580 f(x,f(f(y,f(x,x)),f(f(x,x),z))) = c_0.  [para(36(a,1),9784(a,1,1))].

given #640 (T,wt=15): 18581 f(f(c_0,f(x,y)),f(x,f(f(x,y),z))) = c_0.  [para(36(a,1),9784(a,1,2,1)),rewrite([9778(3,R)])].

given #641 (T,wt=15): 18583 f(f(c_0,f(x,y)),f(y,f(f(x,y),z))) = c_0.  [para(41(a,1),9784(a,1,2,1)),rewrite([9778(3,R)])].

given #642 (T,wt=15): 18597 f(x,f(f(y,f(x,y)),f(f(x,x),z))) = c_0.  [para(570(a,1),9784(a,1,2,1)),rewrite([9778(3,R),9755(3)])].

given #643 (A,wt=19): 195 f(x,f(f(f(y,x),z),f(f(u,y),x))) = f(f(u,y),x).  [para(71(a,1),13(a,1,1))].

given #644 (T,wt=15): 18599 f(x,f(f(y,f(x,x)),f(z,f(x,z)))) = c_0.  [para(637(a,1),9784(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #645 (T,wt=15): 18601 f(x,f(f(y,f(y,x)),f(f(x,x),z))) = c_0.  [para(638(a,1),9784(a,1,2,1)),rewrite([9778(3,R),9755(3)])].

given #646 (T,wt=15): 18603 f(x,f(f(y,f(x,x)),f(z,f(z,x)))) = c_0.  [para(741(a,1),9784(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #647 (T,wt=15): 18660 f(x,f(f(y,f(x,c_0)),f(f(x,c_0),z))) = c_0.  [para(9776(a,1),9784(a,1,1))].

given #648 (A,wt=19): 196 f(x,f(f(y,f(z,x)),f(f(z,u),x))) = f(f(z,u),x).  [para(13(a,1),71(a,1,1))].

given #649 (T,wt=15): 18661 f(x,f(f(y,f(c_0,x)),f(f(c_0,x),z))) = c_0.  [para(11088(a,1),9784(a,1,1))].

given #650 (T,wt=15): 18662 f(x,f(f(y,f(x,c_0)),f(f(x,x),z))) = c_0.  [para(9733(a,1),9784(a,1,2,2)),rewrite([9778(5,R),9756(4)])].

given #651 (T,wt=15): 18663 f(x,f(f(y,f(x,x)),f(f(x,c_0),z))) = c_0.  [para(9733(a,2),9784(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #652 (T,wt=15): 18664 f(x,f(f(y,f(x,c_0)),f(z,f(x,x)))) = c_0.  [para(9735(a,1),9784(a,1,2,2)),rewrite([9778(5,R),9756(4)])].

given #653 (A,wt=23): 197 f(f(f(x,y),z),f(z,f(f(f(f(x,y),z),f(f(y,z),u)),v))) = z.  [para(71(a,1),14(a,1,2,1)),rewrite([71(14)])].

given #654 (T,wt=15): 18665 f(x,f(f(f(x,c_0),y),f(f(x,x),z))) = c_0.  [para(9735(a,2),9784(a,1,2,1)),rewrite([9778(3,R),9755(3)])].

given #655 (T,wt=15): 18668 f(x,f(f(y,f(x,c_0)),f(z,f(z,x)))) = c_0.  [para(9748(a,1),9784(a,1,2,2)),rewrite([9778(5,R),9756(4)])].

given #656 (T,wt=15): 18670 f(x,f(f(y,f(y,x)),f(f(x,c_0),z))) = c_0.  [para(9752(a,1),9784(a,1,2,1)),rewrite([9778(5,R),9756(4)])].

given #657 (T,wt=15): 18672 f(x,f(f(y,f(x,c_0)),f(z,f(x,z)))) = c_0.  [para(9754(a,1),9784(a,1,2,2)),rewrite([9778(5,R),9756(4)])].

given #658 (A,wt=23): 198 f(f(x,y),f(f(f(z,x),f(x,y)),f(y,u))) = f(f(z,x),f(x,y)).  [para(71(a,1),14(a,1,2,2,1))].

given #659 (T,wt=15): 18674 f(x,f(f(y,f(x,y)),f(f(x,c_0),z))) = c_0.  [para(9757(a,1),9784(a,1,2,1)),rewrite([9778(5,R),9756(4)])].

given #660 (T,wt=15): 18680 f(x,f(f(y,f(x,x)),f(f(c_0,x),z))) = c_0.  [para(11226(a,1),9784(a,1,2,1)),rewrite([9778(5,R),9750(4)])].

given #661 (T,wt=15): 18681 f(x,f(f(y,f(c_0,x)),f(f(x,x),z))) = c_0.  [para(11226(a,2),9784(a,1,2,1)),rewrite([9778(3,R),9755(3)])].

given #662 (T,wt=15): 18682 f(x,f(f(y,f(x,y)),f(f(c_0,x),z))) = c_0.  [para(11229(a,1),9784(a,1,2,1)),rewrite([9778(5,R),9750(4)])].

given #663 (A,wt=31): 199 f(f(x,y),f(f(z,y),f(f(x,y),f(f(y,f(x,u)),v)))) = f(f(x,y),f(f(y,f(x,u)),v)).  [para(14(a,1),71(a,1,1))].

given #664 (T,wt=15): 18684 f(x,f(f(y,f(c_0,x)),f(z,f(x,z)))) = c_0.  [para(11230(a,1),9784(a,1,2,2)),rewrite([9778(5,R),9750(4)])].

given #665 (T,wt=15): 18686 f(x,f(f(y,f(y,x)),f(f(c_0,x),z))) = c_0.  [para(11231(a,1),9784(a,1,2,1)),rewrite([9778(5,R),9750(4)])].

given #666 (T,wt=15): 18688 f(x,f(f(y,f(c_0,x)),f(z,f(z,x)))) = c_0.  [para(11233(a,1),9784(a,1,2,2)),rewrite([9778(5,R),9750(4)])].

given #667 (T,wt=15): 18692 f(x,f(f(y,f(x,x)),f(z,f(c_0,x)))) = c_0.  [para(11241(a,1),9784(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #668 (A,wt=19): 200 f(f(x,x),f(f(y,x),f(f(x,x),z))) = f(f(x,x),z).  [para(45(a,1),71(a,1,1))].

given #669 (T,wt=15): 18693 f(x,f(f(f(x,x),y),f(f(c_0,x),z))) = c_0.  [para(11241(a,2),9784(a,1,2,1)),rewrite([9778(5,R),9750(4)])].

given #670 (T,wt=15): 18694 f(x,f(f(y,f(c_0,x)),f(z,f(x,x)))) = c_0.  [para(11242(a,1),9784(a,1,2,2)),rewrite([9778(5,R),9750(4)])].

given #671 (T,wt=15): 18695 f(x,f(f(f(c_0,x),y),f(f(x,x),z))) = c_0.  [para(11242(a,2),9784(a,1,2,1)),rewrite([9778(3,R),9755(3)])].

given #672 (T,wt=15): 18696 f(x,f(f(y,f(x,x)),f(z,f(x,c_0)))) = c_0.  [para(12855(a,1),9784(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #673 (A,wt=19): 201 f(f(x,x),f(f(y,x),f(z,f(x,x)))) = f(z,f(x,x)).  [para(62(a,1),71(a,1,1))].

given #674 (T,wt=15): 18697 f(x,f(f(f(x,x),y),f(f(x,c_0),z))) = c_0.  [para(12855(a,2),9784(a,1,2,1)),rewrite([9778(5,R),9756(4)])].

given #675 (T,wt=15): 18716 f(x,f(f(c_0,f(f(x,c_0),y)),z)) = f(x,c_0).  [para(83(a,1),11121(a,1)),rewrite([9756(4)])].

given #676 (T,wt=15): 18722 f(x,f(f(f(x,x),y),f(f(x,x),z))) = c_0.  [para(36(a,1),9785(a,1,1))].

given #677 (T,wt=15): 18735 f(x,f(f(f(x,x),y),f(z,f(x,z)))) = c_0.  [para(637(a,1),9785(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #678 (A,wt=17): 202 f(f(x,y),f(y,f(f(f(x,y),f(z,x)),u))) = y.  [para(71(a,1),16(a,1,2,1)),rewrite([71(11)])].

given #679 (T,wt=15): 18736 f(x,f(f(f(x,x),y),f(z,f(z,x)))) = c_0.  [para(741(a,1),9785(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #680 (T,wt=15): 18779 f(x,f(f(f(x,c_0),y),f(f(x,c_0),z))) = c_0.  [para(9776(a,1),9785(a,1,1))].

given #681 (T,wt=15): 18780 f(x,f(f(f(c_0,x),y),f(f(c_0,x),z))) = c_0.  [para(11088(a,1),9785(a,1,1))].

given #682 (T,wt=15): 18781 f(x,f(f(f(x,c_0),y),f(z,f(x,x)))) = c_0.  [para(9735(a,1),9785(a,1,2,2)),rewrite([9778(5,R),9756(4)])].

given #683 (A,wt=31): 203 f(f(x,y),f(f(f(x,y),f(f(f(z,x),y),u)),f(y,v))) = f(f(x,y),f(f(f(z,x),y),u)).  [para(71(a,1),16(a,1,2,2,1))].

given #684 (T,wt=15): 18782 f(x,f(f(f(x,c_0),y),f(z,f(z,x)))) = c_0.  [para(9748(a,1),9785(a,1,2,2)),rewrite([9778(5,R),9756(4)])].

given #685 (T,wt=15): 18783 f(x,f(f(f(x,c_0),y),f(z,f(x,z)))) = c_0.  [para(9754(a,1),9785(a,1,2,2)),rewrite([9778(5,R),9756(4)])].

given #686 (T,wt=15): 18786 f(x,f(f(f(c_0,x),y),f(z,f(x,z)))) = c_0.  [para(11230(a,1),9785(a,1,2,2)),rewrite([9778(5,R),9750(4)])].

given #687 (T,wt=15): 18787 f(x,f(f(f(c_0,x),y),f(z,f(z,x)))) = c_0.  [para(11233(a,1),9785(a,1,2,2)),rewrite([9778(5,R),9750(4)])].

given #688 (A,wt=33): 204 f(f(x,f(y,z)),f(f(u,x),f(f(x,f(y,z)),f(f(x,y),v)))) = f(f(x,f(y,z)),f(f(x,y),v)).  [para(16(a,1),71(a,1,1))].

given #689 (T,wt=15): 18789 f(x,f(f(f(x,x),y),f(z,f(c_0,x)))) = c_0.  [para(11241(a,1),9785(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #690 (T,wt=15): 18790 f(x,f(f(f(c_0,x),y),f(z,f(x,x)))) = c_0.  [para(11242(a,1),9785(a,1,2,2)),rewrite([9778(5,R),9750(4)])].

given #691 (T,wt=15): 18791 f(x,f(f(f(x,x),y),f(z,f(x,c_0)))) = c_0.  [para(12855(a,1),9785(a,1,2,2)),rewrite([9778(3,R),9755(3)])].

given #692 (T,wt=15): 18793 f(f(x,y),f(x,f(f(c_0,f(y,z)),u))) = x.  [para(11118(a,1),7(a,1,2,2)),rewrite([2(7)])].

given #693 (A,wt=19): 205 f(x,f(f(y,f(z,x)),f(f(u,z),x))) = f(f(u,z),x).  [para(71(a,1),71(a,1,1))].

given #694 (T,wt=15): 18796 f(f(f(f(c_0,f(x,y)),z),u),f(u,x)) = u.  [para(11118(a,1),12(a,1,2,2))].

given #695 (T,wt=15): 18798 f(f(x,y),f(y,f(f(c_0,f(x,z)),u))) = y.  [para(11118(a,1),19(a,1,1,1))].

given #696 (T,wt=15): 18801 f(f(x,f(f(c_0,f(y,z)),u)),f(y,x)) = x.  [para(11118(a,1),20(a,1,2,1))].

given #697 (T,wt=15): 18802 f(f(x,y),f(f(f(c_0,f(y,z)),u),x)) = x.  [para(11118(a,1),32(a,1,1,2))].

given #698 (A,wt=19): 208 f(f(x,x),f(f(y,f(x,y)),f(x,z))) = f(y,f(x,y)).  [para(184(a,1),6(a,1,1))].

given #699 (T,wt=15): 18804 f(f(x,y),f(f(f(c_0,f(x,z)),u),y)) = y.  [para(11118(a,1),71(a,1,2,1)),rewrite([2(7)])].

given #700 (T,wt=15): 18808 f(x,f(f(c_0,f(y,f(x,y))),z)) = f(x,x).  [para(637(a,1),11118(a,1,2,1,2)),rewrite([9755(3)])].

given #701 (T,wt=15): 18810 f(x,f(f(c_0,f(y,f(y,x))),z)) = f(x,x).  [para(741(a,1),11118(a,1,2,1,2)),rewrite([9755(3)])].

given #702 (T,wt=15): 18833 f(f(x,y),f(x,f(z,f(c_0,f(y,u))))) = x.  [para(11118(a,1),364(a,1,2,2)),rewrite([2(7)])].

given #703 (A,wt=19): 219 f(f(x,x),f(f(y,f(x,y)),f(z,x))) = f(y,f(x,y)).  [para(184(a,1),12(a,1,1))].

given #704 (T,wt=15): 18837 f(f(f(x,f(c_0,f(y,z))),u),f(u,y)) = u.  [para(11118(a,1),487(a,1,2,2))].

given #705 (T,wt=15): 18839 f(x,f(f(c_0,f(y,f(x,x))),z)) = f(x,c_0).  [para(9735(a,1),11118(a,1,2,1,2)),rewrite([9756(4)])].

given #706 (T,wt=15): 18846 f(x,f(f(c_0,f(y,f(c_0,x))),z)) = f(x,x).  [para(11241(a,1),11118(a,1,2,1,2)),rewrite([9755(3)])].

given #707 (T,wt=15): 18848 f(x,f(f(c_0,f(y,f(x,c_0))),z)) = f(x,x).  [para(12855(a,1),11118(a,1,2,1,2)),rewrite([9755(3)])].

given #708 (A,wt=19): 222 f(f(x,x),f(f(x,y),f(z,f(x,z)))) = f(z,f(x,z)).  [para(184(a,1),13(a,1,1))].

given #709 (T,wt=15): 18862 f(f(x,y),f(x,f(f(c_0,f(z,y)),u))) = x.  [para(11127(a,1),7(a,1,2,2)),rewrite([2(7)])].

given #710 (T,wt=15): 18866 f(f(f(f(c_0,f(x,y)),z),u),f(u,y)) = u.  [para(11127(a,1),12(a,1,2,2))].

given #711 (T,wt=15): 18869 f(f(x,y),f(y,f(f(c_0,f(z,x)),u))) = y.  [para(11127(a,1),19(a,1,1,1))].

given #712 (T,wt=15): 18873 f(f(x,f(f(c_0,f(y,z)),u)),f(z,x)) = x.  [para(11127(a,1),20(a,1,2,1))].

given #713 (A,wt=25): 230 f(f(x,f(y,x)),f(f(y,y),f(f(f(x,f(y,x)),f(y,z)),u))) = f(y,y).  [para(184(a,1),14(a,1,2,1)),rewrite([184(13)])].

given #714 (T,wt=15): 18874 f(f(x,y),f(f(f(c_0,f(z,y)),u),x)) = x.  [para(11127(a,1),32(a,1,1,2))].

given #715 (T,wt=15): 18879 f(f(x,y),f(f(f(c_0,f(z,x)),u),y)) = y.  [para(11127(a,1),71(a,1,2,1)),rewrite([2(7)])].

given #716 (T,wt=15): 18918 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x.  [para(11127(a,1),364(a,1,2,2)),rewrite([2(7)])].

given #717 (T,wt=15): 18922 f(f(f(x,f(c_0,f(y,z))),u),f(u,z)) = u.  [para(11127(a,1),487(a,1,2,2))].

given #718 (A,wt=19): 238 f(f(x,x),f(f(y,x),f(z,f(x,z)))) = f(z,f(x,z)).  [para(184(a,1),71(a,1,1))].

given #719 (T,wt=15): 19036 f(f(x,f(y,c_0)),f(c_0,f(z,y))) = f(z,y).  [para(84(a,1),9761(a,1,2)),rewrite([17625(14)])].

given #720 (T,wt=15): 19069 f(f(x,y),f(y,f(z,f(c_0,f(x,u))))) = y.  [para(11129(a,1),19(a,1,1,1))].

given #721 (T,wt=15): 19072 f(f(x,f(y,f(c_0,f(z,u)))),f(z,x)) = x.  [para(11129(a,1),20(a,1,2,1))].

given #722 (T,wt=15): 19073 f(f(x,y),f(f(z,f(c_0,f(y,u))),x)) = x.  [para(11129(a,1),32(a,1,1,2))].

given #723 (A,wt=19): 242 f(f(x,x),f(f(y,f(y,x)),f(x,z))) = f(y,f(y,x)).  [para(206(a,1),6(a,1,1))].

given #724 (T,wt=15): 19075 f(f(x,y),f(f(z,f(c_0,f(x,u))),y)) = y.  [para(11129(a,1),71(a,1,2,1)),rewrite([2(7)])].

given #725 (T,wt=15): 19078 f(x,f(y,f(c_0,f(f(x,c_0),z)))) = f(x,c_0).  [para(570(a,2),11129(a,1,1)),rewrite([9755(3)])].

given #726 (T,wt=15): 19079 f(x,f(y,f(c_0,f(z,f(x,z))))) = f(x,x).  [para(637(a,1),11129(a,1,2,2,2)),rewrite([9755(3)])].

given #727 (T,wt=15): 19080 f(x,f(y,f(c_0,f(f(c_0,x),z)))) = f(c_0,x).  [para(638(a,2),11129(a,1,1)),rewrite([9755(3)])].

given #728 (A,wt=19): 248 f(f(x,x),f(f(y,f(y,x)),f(z,x))) = f(y,f(y,x)).  [para(206(a,1),12(a,1,1))].

given #729 (T,wt=15): 19082 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x).  [para(741(a,1),11129(a,1,2,2,2)),rewrite([9755(3)])].

given #730 (T,wt=15): 19110 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,c_0).  [para(9735(a,1),11129(a,1,2,2,2)),rewrite([9756(4)])].

given #731 (T,wt=15): 19117 f(x,f(y,f(c_0,f(z,f(c_0,x))))) = f(x,x).  [para(11241(a,1),11129(a,1,2,2,2)),rewrite([9755(3)])].

given #732 (T,wt=15): 19119 f(x,f(y,f(c_0,f(z,f(x,c_0))))) = f(x,x).  [para(12855(a,1),11129(a,1,2,2,2)),rewrite([9755(3)])].

given #733 (A,wt=19): 250 f(f(x,x),f(f(x,y),f(z,f(z,x)))) = f(z,f(z,x)).  [para(206(a,1),13(a,1,1))].

given #734 (T,wt=15): 19137 f(f(x,y),f(y,f(z,f(c_0,f(u,x))))) = y.  [para(11134(a,1),19(a,1,1,1))].

given #735 (T,wt=15): 19141 f(f(x,f(y,f(c_0,f(z,u)))),f(u,x)) = x.  [para(11134(a,1),20(a,1,2,1))].

given #736 (T,wt=15): 19142 f(f(x,y),f(f(z,f(c_0,f(u,y))),x)) = x.  [para(11134(a,1),32(a,1,1,2))].

given #737 (T,wt=15): 19147 f(f(x,y),f(f(z,f(c_0,f(u,x))),y)) = y.  [para(11134(a,1),71(a,1,2,1)),rewrite([2(7)])].

given #738 (A,wt=25): 256 f(f(x,f(x,y)),f(f(y,y),f(f(f(x,f(x,y)),f(y,z)),u))) = f(y,y).  [para(206(a,1),14(a,1,2,1)),rewrite([206(13)])].

given #739 (T,wt=15): 19223 f(f(c_0,f(x,y)),f(f(x,x),z)) = f(x,y).  [para(11260(a,1),33(a,1,2)),rewrite([2(4),9760(4)]),flip(a)].

given #740 (T,wt=15): 19225 f(f(c_0,f(x,y)),f(z,f(x,x))) = f(x,y).  [para(11260(a,1),80(a,1,2)),rewrite([2(4),9760(4)]),flip(a)].

given #741 (T,wt=15): 19450 f(f(c_0,f(x,y)),f(f(y,x),z)) = f(x,y).  [para(14440(a,1),11127(a,1,2,1,2)),rewrite([9750(8)])].

given #742 (T,wt=15): 19453 f(f(c_0,f(x,y)),f(z,f(y,x))) = f(x,y).  [para(14440(a,1),11134(a,1,2,2,2)),rewrite([9750(8)])].

given #743 (A,wt=19): 264 f(f(x,x),f(f(y,x),f(z,f(z,x)))) = f(z,f(z,x)).  [para(206(a,1),71(a,1,1))].

given #744 (T,wt=15): 19525 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x).  [para(355(a,1),87(a,1,2)),flip(a)].

given #745 (T,wt=15): 19589 f(f(x,f(y,z)),f(c_0,f(z,y))) = f(z,y).  [para(14440(a,1),15918(a,1,1,2,2)),rewrite([9750(5),2(5)])].

given #746 (T,wt=15): 19591 f(f(c_0,f(x,y)),f(z,f(z,x))) = f(x,y).  [para(3(a,1),17363(a,1,2,2,2))].

given #747 (T,wt=15): 19593 f(f(c_0,f(x,y)),f(z,f(z,y))) = f(x,y).  [para(6(a,1),17363(a,1,2,2,2))].

given #748 (A,wt=17): 269 f(f(x,y),f(x,f(z,f(f(x,y),f(y,u))))) = x.  [para(23(a,1),7(a,1,1))].

given #749 (T,wt=15): 19594 f(f(x,y),f(x,f(z,f(z,f(y,u))))) = x.  [para(17363(a,1),7(a,1,2,2)),rewrite([2(6)])].

given #750 (T,wt=15): 19597 f(f(f(x,f(x,f(y,z))),u),f(u,y)) = u.  [para(17363(a,1),12(a,1,2,2))].

given #751 (T,wt=15): 19599 f(f(c_0,f(x,y)),f(z,f(x,z))) = f(x,y).  [para(13(a,1),17363(a,1,2,2)),rewrite([2(5)])].

given #752 (T,wt=15): 19601 f(f(x,y),f(y,f(z,f(z,f(x,u))))) = y.  [para(17363(a,1),19(a,1,1,1))].

Low Water (displace, True_semantics): id=33427, wt=21

given #753 (A,wt=27): 271 f(f(f(x,y),z),f(x,f(f(f(x,y),z),f(z,u)))) = f(f(f(x,y),z),f(z,u)).  [para(23(a,1),8(a,1,2)),rewrite([2(5),2(8)])].

given #754 (T,wt=15): 19604 f(f(x,f(y,f(y,f(z,u)))),f(z,x)) = x.  [para(17363(a,1),20(a,1,2,1))].

given #755 (T,wt=15): 19605 f(f(x,y),f(f(z,f(z,f(y,u))),x)) = x.  [para(17363(a,1),32(a,1,1,2))].

given #756 (T,wt=15): 19607 f(f(x,y),f(f(z,f(z,f(x,u))),y)) = y.  [para(17363(a,1),71(a,1,2,1)),rewrite([2(6)])].

given #757 (T,wt=15): 19608 f(f(c_0,f(x,y)),f(z,f(y,z))) = f(x,y).  [para(71(a,1),17363(a,1,2,2)),rewrite([2(5)])].

given #758 (A,wt=23): 273 f(x,f(f(x,y),f(f(x,f(f(f(x,y),f(y,z)),u)),v))) = f(x,y).  [para(23(a,1),9(a,1,2,1)),rewrite([23(13)])].

given #759 (T,wt=15): 19612 f(x,f(y,f(y,f(f(x,x),z)))) = f(x,x).  [para(570(a,1),17363(a,1,1)),rewrite([9756(4)])].

given #760 (T,wt=15): 19613 f(x,f(y,f(y,f(f(x,c_0),z)))) = f(x,c_0).  [para(570(a,2),17363(a,1,1)),rewrite([9755(3)])].

given #761 (T,wt=15): 19614 f(x,f(y,f(y,f(z,f(x,z))))) = f(x,x).  [para(637(a,1),17363(a,1,2,2,2)),rewrite([9755(3)])].

given #762 (T,wt=15): 19615 f(x,f(y,f(y,f(f(c_0,x),z)))) = f(c_0,x).  [para(638(a,2),17363(a,1,1)),rewrite([9755(3)])].

given #763 (A,wt=23): 274 f(x,f(f(x,y),f(f(f(x,y),f(f(x,f(y,z)),u)),v))) = f(x,y).  [para(9(a,1),23(a,1,2,1)),rewrite([9(15)])].

given #764 (T,wt=15): 19617 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x).  [para(741(a,1),17363(a,1,2,2,2)),rewrite([9755(3)])].

given #765 (T,wt=15): 19645 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,c_0).  [para(9735(a,1),17363(a,1,2,2,2)),rewrite([9756(4)])].

given #766 (T,wt=15): 19654 f(x,f(y,f(y,f(z,f(c_0,x))))) = f(x,x).  [para(11241(a,1),17363(a,1,2,2,2)),rewrite([9755(3)])].

given #767 (T,wt=15): 19656 f(x,f(y,f(y,f(z,f(x,c_0))))) = f(x,x).  [para(12855(a,1),17363(a,1,2,2,2)),rewrite([9755(3)])].

given #768 (A,wt=23): 276 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,x))) = f(f(x,y),f(y,z)).  [para(23(a,1),12(a,1,1))].

given #769 (T,wt=15): 19670 f(x,f(f(y,f(x,x)),f(z,f(x,x)))) = c_0.  [para(36(a,1),18570(a,1,1))].

given #770 (T,wt=15): 19687 f(x,f(f(y,f(x,y)),f(z,f(x,x)))) = c_0.  [para(570(a,1),18570(a,1,2,1)),rewrite([9778(3,R),9755(3)])].

given #771 (T,wt=15): 19692 f(x,f(f(y,f(y,x)),f(z,f(x,x)))) = c_0.  [para(638(a,1),18570(a,1,2,1)),rewrite([9778(3,R),9755(3)])].

given #772 (T,wt=15): 19736 f(x,f(f(y,f(x,c_0)),f(z,f(x,c_0)))) = c_0.  [para(9776(a,1),18570(a,1,1))].

given #773 (A,wt=23): 278 f(f(x,y),f(f(x,z),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)).  [para(23(a,1),13(a,1,1))].

given #774 (T,wt=15): 19737 f(x,f(f(y,f(c_0,x)),f(z,f(c_0,x)))) = c_0.  [para(11088(a,1),18570(a,1,1))].

given #775 (T,wt=15): 19741 f(x,f(f(y,f(y,x)),f(z,f(x,c_0)))) = c_0.  [para(9752(a,1),18570(a,1,2,1)),rewrite([9778(5,R),9756(4)])].

given #776 (T,wt=15): 19746 f(x,f(f(y,f(x,y)),f(z,f(x,c_0)))) = c_0.  [para(9757(a,1),18570(a,1,2,1)),rewrite([9778(5,R),9756(4)])].

given #777 (T,wt=15): 19753 f(x,f(f(y,f(x,y)),f(z,f(c_0,x)))) = c_0.  [para(11229(a,1),18570(a,1,2,1)),rewrite([9778(5,R),9750(4)])].

given #778 (A,wt=27): 281 f(f(f(x,y),z),f(y,f(f(f(x,y),z),f(z,u)))) = f(f(f(x,y),z),f(z,u)).  [para(23(a,1),19(a,1,1)),rewrite([2(7)])].

given #779 (T,wt=15): 19758 f(x,f(f(y,f(y,x)),f(z,f(c_0,x)))) = c_0.  [para(11231(a,1),18570(a,1,2,1)),rewrite([9778(5,R),9750(4)])].

given #780 (T,wt=15): 19774 f(x,f(f(f(x,x),y),f(z,f(x,x)))) = c_0.  [para(36(a,1),18571(a,1,1))].

given #781 (T,wt=15): 19827 f(x,f(f(f(x,c_0),y),f(z,f(x,c_0)))) = c_0.  [para(9776(a,1),18571(a,1,1))].

given #782 (T,wt=15): 19828 f(x,f(f(f(c_0,x),y),f(z,f(c_0,x)))) = c_0.  [para(11088(a,1),18571(a,1,1))].

given #783 (A,wt=29): 283 f(f(f(x,y),f(y,z)),f(f(x,y),f(f(f(f(x,y),f(y,z)),f(x,u)),v))) = f(x,y).  [para(23(a,1),14(a,1,2,1)),rewrite([23(16)])].

given #784 (T,wt=15): 20165 f(f(c_0,f(x,y)),f(f(y,y),z)) = f(x,y).  [para(18868(a,1),33(a,1,2)),rewrite([2(4),9761(4)]),flip(a)].

given #785 (T,wt=15): 20167 f(f(c_0,f(x,y)),f(z,f(y,y))) = f(x,y).  [para(18868(a,1),80(a,1,2)),rewrite([2(4),9761(4)]),flip(a)].

given #786 (T,wt=15): 20180 f(f(x,y),f(x,f(z,f(z,f(u,y))))) = x.  [para(18945(a,1),7(a,1,2,2)),rewrite([2(6)])].

given #787 (T,wt=15): 20184 f(f(f(x,f(x,f(y,z))),u),f(u,z)) = u.  [para(18945(a,1),12(a,1,2,2))].

given #788 (A,wt=23): 284 f(x,f(f(y,x),f(f(f(y,x),f(f(x,f(y,z)),u)),v))) = f(y,x).  [para(14(a,1),23(a,1,2,1)),rewrite([14(15)])].

given #789 (T,wt=15): 20187 f(f(x,y),f(y,f(z,f(z,f(u,x))))) = y.  [para(18945(a,1),19(a,1,1,1))].

given #790 (T,wt=15): 20191 f(f(x,f(y,f(y,f(z,u)))),f(u,x)) = x.  [para(18945(a,1),20(a,1,2,1))].

given #791 (T,wt=15): 20192 f(f(x,y),f(f(z,f(z,f(u,y))),x)) = x.  [para(18945(a,1),32(a,1,1,2))].

given #792 (T,wt=15): 20194 f(f(x,y),f(f(z,f(z,f(u,x))),y)) = y.  [para(18945(a,1),71(a,1,2,1)),rewrite([2(6)])].

given #793 (A,wt=31): 287 f(x,f(f(x,f(f(f(x,y),f(y,z)),u)),f(f(x,y),v))) = f(x,f(f(f(x,y),f(y,z)),u)).  [para(23(a,1),16(a,1,2,2,1))].

given #794 (T,wt=15): 20395 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0.  [para(19233(a,1),638(a,2,2)),rewrite([9778(8,R),2(9),9472(9)])].

given #795 (T,wt=15): 20422 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z).  [para(3(a,1),19475(a,1,1,2,2)),rewrite([2(5)])].

given #796 (T,wt=15): 20423 f(f(x,f(x,y)),f(c_0,f(z,y))) = f(z,y).  [para(6(a,1),19475(a,1,1,2,2)),rewrite([2(5)])].

given #797 (T,wt=15): 20424 f(f(x,f(y,x)),f(c_0,f(y,z))) = f(y,z).  [para(13(a,1),19475(a,1,1,2)),rewrite([2(2),2(5)])].

given #798 (A,wt=27): 288 f(x,f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(x,y),u)),v))) = f(x,f(y,z)).  [para(16(a,1),23(a,1,2,1)),rewrite([16(16)])].

given #799 (T,wt=15): 20425 f(f(x,f(y,x)),f(c_0,f(z,y))) = f(z,y).  [para(71(a,1),19475(a,1,1,2)),rewrite([2(2),2(5)])].

given #800 (T,wt=15): 20759 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0.  [para(20175(a,1),638(a,2,2)),rewrite([9778(8,R),2(9),9472(9)])].

given #801 (T,wt=15): 20891 f(f(x,f(f(y,y),z)),f(c_0,f(y,x))) = c_0.  [para(639(a,1),9692(a,1,2,2,2)),rewrite([2(7),15(7)])].

given #802 (T,wt=15): 20967 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0.  [para(644(a,1),9692(a,1,2,2,2)),rewrite([2(7),15(7)])].

given #803 (A,wt=23): 289 f(f(x,y),f(f(z,x),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)).  [para(23(a,1),71(a,1,1))].

given #804 (T,wt=15): 21095 f(f(x,f(y,z)),f(x,f(f(y,y),u))) = x.  [para(43(a,1),646(a,1,1,2)),rewrite([2(8),146(8)])].

given #805 (T,wt=15): 21098 f(f(x,f(y,z)),f(x,f(u,f(y,y)))) = x.  [para(58(a,1),646(a,1,1,2)),rewrite([2(8),151(8)])].

given #806 (T,wt=15): 21099 f(f(x,f(y,z)),f(x,f(f(z,z),u))) = x.  [para(61(a,1),646(a,1,1,2)),rewrite([2(8),200(8)])].

given #807 (T,wt=15): 21100 f(f(x,f(y,z)),f(x,f(u,f(z,z)))) = x.  [para(64(a,1),646(a,1,1,2)),rewrite([2(8),201(8)])].

given #808 (A,wt=19): 293 f(x,f(f(x,y),f(f(f(x,y),f(y,z)),u))) = f(x,y).  [para(23(a,1),23(a,1,2,1)),rewrite([23(11)])].

given #809 (T,wt=15): 21129 f(f(x,f(f(y,y),z)),f(x,f(y,u))) = x.  [para(63(a,1),646(a,1,1,2)),rewrite([9778(10,R),9755(10),2(8),59(8)])].

given #810 (T,wt=15): 21188 f(f(c_0,f(x,y)),f(f(f(x,x),z),y)) = c_0.  [para(648(a,1),9692(a,1,2,2,2)),rewrite([2(7),15(7),2(7)])].

given #811 (T,wt=15): 21247 f(f(f(x,y),z),f(z,f(f(x,x),u))) = z.  [para(43(a,1),663(a,1,1,1)),rewrite([2(8),146(8)])].

given #812 (T,wt=15): 21250 f(f(f(x,y),z),f(z,f(u,f(x,x)))) = z.  [para(58(a,1),663(a,1,1,1)),rewrite([2(8),151(8)])].

given #813 (A,wt=23): 294 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(f(y,x),v))))) = x.  [para(18(a,1),7(a,1,1))].

given #814 (T,wt=15): 21251 f(f(f(x,y),z),f(z,f(f(y,y),u))) = z.  [para(61(a,1),663(a,1,1,1)),rewrite([2(8),200(8)])].

given #815 (T,wt=15): 21252 f(f(f(x,y),z),f(z,f(u,f(y,y)))) = z.  [para(64(a,1),663(a,1,1,1)),rewrite([2(8),201(8)])].

given #816 (T,wt=15): 21286 f(f(f(f(x,x),y),z),f(z,f(x,u))) = z.  [para(63(a,1),663(a,1,1,1)),rewrite([9778(10,R),9755(10),2(8),59(8)])].

given #817 (T,wt=15): 21423 f(f(c_0,f(x,y)),f(f(z,f(x,x)),y)) = c_0.  [para(674(a,1),9713(a,1,2,2,2)),rewrite([2(7),15(7),2(7)])].

given #818 (A,wt=33): 296 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(x,z),u)),f(x,v))) = f(f(x,f(y,z)),f(f(x,z),u)).  [para(7(a,1),18(a,1,2,2,1))].

given #819 (T,wt=15): 21479 f(f(f(x,f(y,y)),z),f(z,f(y,u))) = z.  [para(58(a,1),675(a,1,2,2)),rewrite([2(6),151(6)])].

given #820 (T,wt=15): 21480 f(f(f(f(x,x),y),z),f(z,f(u,x))) = z.  [para(61(a,1),675(a,1,2,2)),rewrite([2(6),200(6)])].

given #821 (T,wt=15): 21481 f(f(f(x,f(y,y)),z),f(z,f(u,y))) = z.  [para(64(a,1),675(a,1,2,2)),rewrite([2(6),201(6)])].

given #822 (T,wt=15): 21548 f(f(x,f(y,z)),f(f(f(y,y),u),x)) = x.  [para(43(a,1),684(a,1,1,2)),rewrite([2(8),146(8)])].

given #823 (A,wt=41): 297 f(f(f(x,y),f(z,u)),f(x,f(f(f(x,y),f(z,u)),f(f(z,f(x,y)),v)))) = f(f(f(x,y),f(z,u)),f(f(z,f(x,y)),v)).  [para(18(a,1),8(a,1,2)),rewrite([2(8),2(12)])].

given #824 (T,wt=15): 21550 f(f(x,f(y,z)),f(f(u,f(y,y)),x)) = x.  [para(58(a,1),684(a,1,1,2)),rewrite([2(8),151(8)])].

given #825 (T,wt=15): 21551 f(f(x,f(y,z)),f(f(f(z,z),u),x)) = x.  [para(61(a,1),684(a,1,1,2)),rewrite([2(8),200(8)])].

given #826 (T,wt=15): 21552 f(f(x,f(y,z)),f(f(u,f(z,z)),x)) = x.  [para(64(a,1),684(a,1,1,2)),rewrite([2(8),201(8)])].

given #827 (T,wt=15): 21556 f(f(x,f(f(y,y),z)),f(f(y,u),x)) = x.  [para(63(a,1),684(a,1,1,2)),rewrite([9778(10,R),9755(10),2(8),59(8)])].

given #828 (A,wt=17): 298 f(f(x,y),f(x,f(f(f(y,z),f(x,y)),u))) = x.  [para(8(a,1),18(a,1,2,1)),rewrite([8(11)])].

given #829 (T,wt=15): 21629 f(f(x,f(y,f(z,z))),f(f(z,u),x)) = x.  [para(58(a,1),688(a,1,2,1)),rewrite([2(6),151(6)])].

given #830 (T,wt=15): 21630 f(f(x,f(f(y,y),z)),f(f(u,y),x)) = x.  [para(61(a,1),688(a,1,2,1)),rewrite([2(6),200(6)])].

given #831 (T,wt=15): 21631 f(f(x,f(y,f(z,z))),f(f(u,z),x)) = x.  [para(64(a,1),688(a,1,2,1)),rewrite([2(6),201(6)])].

given #832 (T,wt=15): 21646 f(f(x,f(y,y)),z) = f(z,f(x,f(y,x))).  [para(690(a,1),2(a,1)),flip(a)].

given #833 (A,wt=31): 299 f(x,f(f(x,f(y,z)),f(f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v)),w))) = f(x,f(y,z)).  [para(18(a,1),9(a,1,2,1)),rewrite([18(18)])].

given #834 (T,wt=15): 21647 f(f(x,f(y,x)),z) = f(z,f(x,f(y,y))).  [para(690(a,2),2(a,1)),flip(a)].

given #835 (T,wt=15): 22053 f(f(f(x,y),z),f(f(f(x,x),u),z)) = z.  [para(43(a,1),697(a,1,1,1)),rewrite([2(8),146(8)])].

given #836 (T,wt=15): 22055 f(f(f(x,y),z),f(f(u,f(x,x)),z)) = z.  [para(58(a,1),697(a,1,1,1)),rewrite([2(8),151(8)])].

given #837 (T,wt=15): 22056 f(f(f(x,y),z),f(f(f(y,y),u),z)) = z.  [para(61(a,1),697(a,1,1,1)),rewrite([2(8),200(8)])].

given #838 (A,wt=49): 300 f(f(f(x,y),f(f(x,f(y,z)),u)),f(f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v)),f(f(x,y),w))) = f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v)).  [para(9(a,1),18(a,1,2,2,1))].

given #839 (T,wt=15): 22057 f(f(f(x,y),z),f(f(u,f(y,y)),z)) = z.  [para(64(a,1),697(a,1,1,1)),rewrite([2(8),201(8)])].

given #840 (T,wt=15): 22086 f(f(f(f(x,x),y),z),f(f(x,u),z)) = z.  [para(63(a,1),697(a,1,1,1)),rewrite([9778(10,R),9755(10),2(8),59(8)])].

given #841 (T,wt=15): 22122 f(f(f(x,x),y),z) = f(z,f(y,f(x,y))).  [para(778(a,1),2(a,1)),flip(a)].

given #842 (T,wt=15): 22123 f(f(x,f(y,x)),z) = f(z,f(f(y,y),x)).  [para(778(a,2),2(a,1)),flip(a)].

given #843 (A,wt=33): 301 f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(y,x),u)),f(v,x))) = f(f(x,f(y,z)),f(f(y,x),u)).  [para(18(a,1),12(a,1,1))].

given #844 (T,wt=15): 22443 f(f(x,f(y,y)),z) = f(z,f(x,f(x,y))).  [para(850(a,1),2(a,1)),flip(a)].

given #845 (T,wt=15): 22444 f(f(x,f(x,y)),z) = f(z,f(x,f(y,y))).  [para(850(a,2),2(a,1)),flip(a)].

given #846 (T,wt=15): 22840 f(f(x,f(f(y,y),z)),f(x,f(u,y))) = x.  [para(58(a,1),898(a,1,1,2)),rewrite([9778(8,R),9755(8),2(8),65(8)])].

given #847 (T,wt=15): 22841 f(f(x,f(y,f(z,z))),f(x,f(z,u))) = x.  [para(61(a,1),898(a,1,1,2)),rewrite([9778(8,R),9755(8),2(8),112(8)])].

given #848 (A,wt=33): 302 f(f(x,f(y,z)),f(f(x,u),f(f(x,f(y,z)),f(f(y,x),v)))) = f(f(x,f(y,z)),f(f(y,x),v)).  [para(18(a,1),13(a,1,1))].

given #849 (T,wt=15): 22842 f(f(x,f(y,f(z,z))),f(x,f(u,z))) = x.  [para(64(a,1),898(a,1,1,2)),rewrite([9778(8,R),9755(8),2(8),113(8)])].

given #850 (T,wt=15): 22972 f(f(f(f(x,x),y),z),f(f(u,x),z)) = z.  [para(58(a,1),918(a,1,1,1)),rewrite([9778(8,R),9755(8),2(8),65(8)])].

given #851 (T,wt=15): 22973 f(f(f(x,f(y,y)),z),f(f(y,u),z)) = z.  [para(61(a,1),918(a,1,1,1)),rewrite([9778(8,R),9755(8),2(8),112(8)])].

given #852 (T,wt=15): 22974 f(f(f(x,f(y,y)),z),f(f(u,y),z)) = z.  [para(64(a,1),918(a,1,1,1)),rewrite([9778(8,R),9755(8),2(8),113(8)])].

given #853 (A,wt=17): 303 f(f(x,y),f(y,f(f(f(x,z),f(x,y)),u))) = y.  [para(13(a,1),18(a,1,2,1)),rewrite([13(11)])].

given #854 (T,wt=15): 23183 f(f(f(x,x),y),z) = f(z,f(y,f(y,x))).  [para(1038(a,1),2(a,1)),flip(a)].

given #855 (T,wt=15): 23184 f(f(x,f(x,y)),z) = f(z,f(f(y,y),x)).  [para(1038(a,2),2(a,1)),flip(a)].

given #856 (T,wt=15): 24098 f(x,f(f(c_0,f(y,z)),f(y,x))) = f(x,x).  [para(3(a,1),1551(a,1,2,2,1)),rewrite([9778(3,R)])].

given #857 (T,wt=15): 24099 f(x,f(f(c_0,f(y,z)),f(z,x))) = f(x,x).  [para(6(a,1),1551(a,1,2,2,1)),rewrite([9778(3,R)])].

given #858 (A,wt=33): 304 f(f(f(x,y),z),f(f(f(f(x,y),z),f(f(x,z),u)),f(z,v))) = f(f(f(x,y),z),f(f(x,z),u)).  [para(13(a,1),18(a,1,2,2,1))].

given #859 (T,wt=15): 24101 f(x,f(y,f(f(f(y,y),z),x))) = f(x,x).  [para(36(a,1),1551(a,1,2,1))].

given #860 (T,wt=15): 24107 f(x,f(y,f(f(z,f(y,z)),x))) = f(x,x).  [para(637(a,1),1551(a,1,2,2,1)),rewrite([9778(3,R),9755(3)])].

given #861 (T,wt=15): 24108 f(x,f(y,f(f(z,f(z,y)),x))) = f(x,x).  [para(741(a,1),1551(a,1,2,2,1)),rewrite([9778(3,R),9755(3)])].

given #862 (T,wt=15): 24141 f(x,f(f(c_0,y),f(f(y,z),x))) = f(x,x).  [para(9778(a,2),1551(a,1,2,1))].

given #863 (A,wt=41): 305 f(f(f(x,y),f(z,u)),f(y,f(f(f(x,y),f(z,u)),f(f(z,f(x,y)),v)))) = f(f(f(x,y),f(z,u)),f(f(z,f(x,y)),v)).  [para(18(a,1),19(a,1,1)),rewrite([2(11)])].

given #864 (T,wt=15): 24142 f(x,f(f(y,c_0),f(f(y,z),x))) = f(x,x).  [para(9790(a,2),1551(a,1,2,1))].

given #865 (T,wt=15): 24143 f(x,f(y,f(f(f(y,c_0),z),x))) = f(x,x).  [para(9776(a,1),1551(a,1,2,1))].

given #866 (T,wt=15): 24144 f(x,f(y,f(f(f(c_0,y),z),x))) = f(x,x).  [para(11088(a,1),1551(a,1,2,1))].

given #867 (T,wt=15): 24146 f(x,f(y,f(f(z,f(y,y)),x))) = f(x,x).  [para(9735(a,1),1551(a,1,2,2,1)),rewrite([9778(5,R),9756(4)])].

given #868 (A,wt=41): 306 f(f(f(x,f(y,z)),f(f(y,x),u)),f(f(x,f(y,z)),f(f(f(f(x,f(y,z)),f(f(y,x),u)),f(x,v)),w))) = f(x,f(y,z)).  [para(18(a,1),14(a,1,2,1)),rewrite([18(23)])].

given #869 (T,wt=15): 24152 f(x,f(y,f(f(z,f(c_0,y)),x))) = f(x,x).  [para(11241(a,1),1551(a,1,2,2,1)),rewrite([9778(3,R),9755(3)])].

given #870 (T,wt=15): 24155 f(x,f(y,f(f(z,f(y,c_0)),x))) = f(x,x).  [para(12855(a,1),1551(a,1,2,2,1)),rewrite([9778(3,R),9755(3)])].

given #871 (T,wt=15): 24718 f(x,f(f(y,y),f(x,f(z,y)))) = f(x,x).  [para(2(a,1),1608(a,1,2,2))].

given #872 (T,wt=15): 24757 f(x,f(f(c_0,y),f(f(z,y),x))) = f(x,x).  [para(9778(a,2),1608(a,1,2,1))].

Low Water (keep, True_semantics): wt=19

given #873 (A,wt=49): 307 f(f(f(x,y),f(f(y,f(x,z)),u)),f(f(f(f(x,y),f(f(y,f(x,z)),u)),f(y,v)),f(f(x,y),w))) = f(f(f(x,y),f(f(y,f(x,z)),u)),f(y,v)).  [para(14(a,1),18(a,1,2,2,1))].

given #874 (T,wt=15): 24758 f(x,f(f(y,c_0),f(f(z,y),x))) = f(x,x).  [para(9790(a,2),1608(a,1,2,1))].

given #875 (T,wt=15): 24987 f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)).  [para(1951(a,1),33(a,1,2)),flip(a)].

given #876 (T,wt=15): 25036 f(x,f(f(c_0,f(y,z)),f(x,y))) = f(x,x).  [para(15108(a,1),1951(a,1,2,2,2))].

given #877 (T,wt=15): 25037 f(x,f(f(c_0,f(y,z)),f(x,z))) = f(x,x).  [para(15918(a,1),1951(a,1,2,2,2))].

given #878 (A,wt=17): 308 f(f(x,y),f(x,f(f(f(z,y),f(x,y)),u))) = x.  [para(20(a,1),18(a,1,2,1)),rewrite([20(11)])].

given #879 (T,wt=15): 25193 f(f(x,f(y,f(z,y))),f(c_0,f(z,x))) = c_0.  [para(2154(a,1),9713(a,1,2,2,2)),rewrite([2(7),15(7)])].

given #880 (T,wt=15): 25396 f(f(c_0,f(x,y)),f(f(z,f(x,z)),y)) = c_0.  [para(2255(a,1),9713(a,1,2,2,2)),rewrite([2(7),15(7),2(7)])].

given #881 (T,wt=15): 25848 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0.  [para(2829(a,1),9713(a,1,2,2,2)),rewrite([2(7),15(7)])].

given #882 (T,wt=15): 26028 f(f(c_0,f(x,y)),f(f(z,f(z,x)),y)) = c_0.  [para(3029(a,1),9713(a,1,2,2,2)),rewrite([2(7),15(7),2(7)])].

given #883 (A,wt=41): 311 f(x,f(f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v)),f(f(x,f(y,z)),w))) = f(x,f(f(f(x,f(y,z)),f(f(y,x),u)),v)).  [para(18(a,1),16(a,1,2,2,1))].

given #884 (T,wt=15): 26362 f(x,f(y,f(f(x,y),z))) = f(x,f(y,y)).  [para(5175(a,1),33(a,1,2)),flip(a)].

given #885 (T,wt=15): 26561 f(x,f(c_0,f(f(y,y),f(x,f(y,z))))) = c_0.  [para(9086(a,1),638(a,2,2)),rewrite([9778(9,R),9472(9)])].

given #886 (T,wt=15): 26563 f(x,f(f(c_0,y),f(x,f(y,z)))) = f(x,x).  [para(9778(a,2),9086(a,1,2,1))].

given #887 (T,wt=15): 26564 f(x,f(f(y,c_0),f(x,f(y,z)))) = f(x,x).  [para(9790(a,2),9086(a,1,2,1))].

given #888 (A,wt=51): 312 f(f(f(x,f(y,z)),f(f(x,y),u)),f(f(f(f(x,f(y,z)),f(f(x,y),u)),f(x,v)),f(f(x,f(y,z)),w))) = f(f(f(x,f(y,z)),f(f(x,y),u)),f(x,v)).  [para(16(a,1),18(a,1,2,2,1))].

given #889 (T,wt=15): 26565 f(x,f(y,f(x,f(f(y,c_0),z)))) = f(x,x).  [para(9776(a,1),9086(a,1,2,1))].

given #890 (T,wt=15): 26567 f(x,f(y,f(x,f(f(c_0,y),z)))) = f(x,x).  [para(11088(a,1),9086(a,1,2,1))].

given #891 (T,wt=15): 26568 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x).  [para(9735(a,1),9086(a,1,2,2,2)),rewrite([9778(5,R),9756(4)])].

given #892 (T,wt=15): 26569 f(x,f(y,f(x,f(z,f(c_0,y))))) = f(x,x).  [para(11241(a,1),9086(a,1,2,2,2)),rewrite([9778(3,R),9755(3)])].

given #893 (A,wt=33): 313 f(f(x,f(y,z)),f(f(u,x),f(f(x,f(y,z)),f(f(y,x),v)))) = f(f(x,f(y,z)),f(f(y,x),v)).  [para(18(a,1),71(a,1,1))].

given #894 (T,wt=15): 26570 f(x,f(f(x,f(y,z)),f(c_0,y))) = f(x,x).  [para(11241(a,1),9086(a,1,2))].

given #895 (T,wt=15): 26571 f(x,f(y,f(x,f(z,f(y,c_0))))) = f(x,x).  [para(12855(a,1),9086(a,1,2,2,2)),rewrite([9778(3,R),9755(3)])].

given #896 (T,wt=15): 26596 f(x,f(y,f(f(x,x),z))) = f(x,f(y,y)).  [para(9092(a,1),33(a,1,2)),flip(a)].

given #897 (T,wt=15): 26615 f(x,f(y,f(c_0,f(f(x,y),z)))) = f(x,x).  [para(9092(a,1),90(a,1)),rewrite([9778(6,R),2(6)]),flip(a)].

given #898 (A,wt=17): 314 f(f(x,y),f(y,f(f(f(z,x),f(x,y)),u))) = y.  [para(71(a,1),18(a,1,2,1)),rewrite([71(11)])].

given #899 (T,wt=15): 26616 f(x,f(y,f(c_0,f(f(y,x),z)))) = f(x,x).  [para(9092(a,1),97(a,1)),rewrite([9778(6,R),2(6)]),flip(a)].

given #900 (T,wt=15): 26643 f(x,f(y,f(z,f(x,z)))) = f(x,f(y,y)).  [para(9114(a,1),33(a,1,2)),flip(a)].

given #901 (T,wt=15): 26660 f(x,f(y,f(y,f(f(y,x),z)))) = f(x,x).  [para(9114(a,1),68(a,1)),rewrite([2(4)]),flip(a)].

given #902 (T,wt=15): 26663 f(x,f(f(y,c_0),f(x,f(z,y)))) = f(x,x).  [para(9733(a,1),9114(a,1,2,2,2,2)),rewrite([11229(5,R),9755(5)])].

given #903 (A,wt=33): 315 f(f(f(x,y),z),f(f(f(f(x,y),z),f(f(y,z),u)),f(z,v))) = f(f(f(x,y),z),f(f(y,z),u)).  [para(71(a,1),18(a,1,2,2,1))].

given #904 (T,wt=15): 26669 f(x,f(f(c_0,y),f(x,f(z,y)))) = f(x,x).  [para(11233(a,1),9114(a,1,2,2,2,2)),rewrite([10(5)])].

given #905 (T,wt=15): 26671 f(x,f(f(x,f(y,z)),f(c_0,z))) = f(x,x).  [para(11241(a,1),9114(a,1,2)),rewrite([11229(3,R),9755(3)])].

given #906 (T,wt=15): 26673 f(x,f(f(y,z),f(x,f(z,y)))) = f(x,x).  [para(12376(a,1),9114(a,1,2,2,2,2)),rewrite([2(6),9750(6)])].

given #907 (T,wt=15): 26674 f(x,f(f(x,f(y,z)),f(z,c_0))) = f(x,x).  [para(12855(a,1),9114(a,1,2)),rewrite([11229(3,R),9755(3)])].

given #908 (A,wt=27): 320 f(x,f(f(x,f(y,z)),f(f(f(x,f(y,z)),f(f(y,x),u)),v))) = f(x,f(y,z)).  [para(18(a,1),23(a,1,2,1)),rewrite([18(16)])].

given #909 (T,wt=15): 26678 f(x,f(y,f(y,f(f(x,y),z)))) = f(x,x).  [para(9114(a,1),87(a,1)),rewrite([2(4)]),flip(a)].

given #910 (T,wt=15): 26698 f(x,f(y,f(y,f(z,f(y,x))))) = f(x,x).  [para(9114(a,1),114(a,1)),rewrite([2(4)]),flip(a)].

given #911 (T,wt=15): 26718 f(x,f(y,f(z,f(z,x)))) = f(x,f(y,y)).  [para(9118(a,1),33(a,1,2)),flip(a)].

given #912 (T,wt=15): 26759 f(x,f(c_0,f(f(x,f(y,z)),f(y,c_0)))) = c_0.  [para(9631(a,1),638(a,2,2)),rewrite([9778(11,R),9472(10)])].

given #913 (A,wt=37): 321 f(f(f(x,y),f(y,z)),f(f(f(f(x,y),f(y,z)),f(x,u)),f(f(x,y),v))) = f(f(f(x,y),f(y,z)),f(x,u)).  [para(23(a,1),18(a,1,2,2,1))].

given #914 (T,wt=15): 27018 f(f(f(x,y),z),f(z,f(f(y,x),u))) = z.  [para(10092(a,1),16(a,1,2,1)),rewrite([2(8),19450(8),10092(13)])].

given #915 (T,wt=15): 27046 f(f(f(x,y),z),f(z,f(u,f(y,x)))) = z.  [para(10092(a,1),67(a,1,2,1)),rewrite([19450(8),10092(13)])].

given #916 (T,wt=15): 27047 f(f(f(x,y),z),f(f(f(y,x),u),z)) = z.  [para(10092(a,1),68(a,1,2,2)),rewrite([19450(8),10092(13)])].

given #917 (T,wt=15): 27049 f(f(f(x,y),z),f(c_0,f(z,f(y,x)))) = c_0.  [para(10092(a,1),9713(a,1,2,2,2)),rewrite([2(8),11229(8,R),9750(8)])].

given #918 (A,wt=51): 322 f(f(f(x,f(y,z)),f(f(y,x),u)),f(f(f(f(x,f(y,z)),f(f(y,x),u)),f(x,v)),f(f(x,f(y,z)),w))) = f(f(f(x,f(y,z)),f(f(y,x),u)),f(x,v)).  [para(18(a,1),18(a,1,2,2,1))].

given #919 (T,wt=15): 27105 f(f(f(x,y),z),f(f(u,f(y,x)),z)) = z.  [para(10092(a,1),114(a,1,2,2)),rewrite([19450(8),10092(13)])].

given #920 (T,wt=15): 27115 f(f(x,f(y,z)),f(x,f(f(z,y),u))) = x.  [para(10101(a,1),16(a,1,2,1)),rewrite([19589(8),10101(13)])].

given #921 (T,wt=15): 27130 f(f(x,f(y,z)),f(x,f(u,f(z,y)))) = x.  [para(10101(a,1),67(a,1,2,1)),rewrite([19453(8),10101(13)])].

given #922 (T,wt=15): 27131 f(f(x,f(y,z)),f(f(f(z,y),u),x)) = x.  [para(10101(a,1),68(a,1,2,2)),rewrite([19453(8),10101(13)])].

given #923 (A,wt=17): 323 f(f(x,y),f(y,f(z,f(f(x,y),f(x,u))))) = y.  [para(26(a,1),7(a,1,1))].

given #924 (T,wt=15): 27133 f(f(x,f(y,z)),f(c_0,f(x,f(z,y)))) = c_0.  [para(10101(a,1),9713(a,1,2,2,2)),rewrite([2(8),11229(8,R),9750(8)])].

given #925 (T,wt=15): 27173 f(f(x,f(y,z)),f(f(u,f(z,y)),x)) = x.  [para(10101(a,1),114(a,1,2,2)),rewrite([19453(8),10101(13)])].

given #926 (T,wt=15): 27459 f(f(x,y),f(z,c_0)) = f(f(z,z),f(y,x)).  [para(2(a,1),10354(a,1,1))].

given #927 (T,wt=15): 27516 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0.  [para(10366(a,1),113(a,1,2)),rewrite([9778(10,R),9750(8),9778(12,R),9750(10),9778(8,R),7(8),9778(8,R),9750(6)]),flip(a)].

given #928 (A,wt=27): 325 f(f(x,f(y,z)),f(y,f(f(x,f(y,z)),f(x,u)))) = f(f(x,f(y,z)),f(x,u)).  [para(26(a,1),8(a,1,2)),rewrite([2(5),2(8)])].

given #929 (T,wt=15): 27566 f(x,f(f(y,z),f(f(z,y),x))) = f(x,x).  [para(14440(a,1),10366(a,1,2,2,2)),rewrite([9750(7),2(4)])].

given #930 (T,wt=15): 27641 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x.  [para(9784(a,1),10367(a,1,2,1)),rewrite([9750(9),9778(9,R),9755(9)])].

given #931 (T,wt=15): 27642 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x.  [para(9785(a,1),10367(a,1,2,1)),rewrite([9750(9),9778(9,R),9755(9)])].

given #932 (T,wt=15): 27645 f(f(x,x),f(y,f(f(z,x),f(u,x)))) = x.  [para(18570(a,1),10367(a,1,2,1)),rewrite([9750(9),9778(9,R),9755(9)])].

given #933 (A,wt=23): 326 f(x,f(f(y,x),f(f(x,f(f(f(y,x),f(y,z)),u)),v))) = f(y,x).  [para(26(a,1),9(a,1,2,1)),rewrite([26(13)])].

given #934 (T,wt=15): 27646 f(f(x,x),f(y,f(f(x,z),f(u,x)))) = x.  [para(18571(a,1),10367(a,1,2,1)),rewrite([9750(9),9778(9,R),9755(9)])].

given #935 (T,wt=15): 27647 f(f(x,c_0),f(y,f(f(z,x),f(x,u)))) = x.  [para(18609(a,1),10367(a,1,2,1)),rewrite([9750(10),9778(12,R),9756(11)])].

given #936 (T,wt=15): 27648 f(f(c_0,x),f(y,f(f(z,x),f(x,u)))) = x.  [para(18659(a,1),10367(a,1,2,1)),rewrite([9750(10),9778(12,R),9750(11)])].

given #937 (T,wt=15): 27649 f(f(x,c_0),f(y,f(f(x,z),f(x,u)))) = x.  [para(18740(a,1),10367(a,1,2,1)),rewrite([9750(10),9778(12,R),9756(11)])].

given #938 (A,wt=23): 327 f(f(f(x,y),f(f(x,f(y,z)),u)),f(f(x,y),f(x,v))) = f(x,y).  [para(9(a,1),26(a,1,2,1)),rewrite([9(15)])].

given #939 (T,wt=15): 27650 f(f(c_0,x),f(y,f(f(x,z),f(x,u)))) = x.  [para(18778(a,1),10367(a,1,2,1)),rewrite([9750(10),9778(12,R),9750(11)])].

given #940 (T,wt=15): 27652 f(f(x,c_0),f(y,f(f(z,x),f(u,x)))) = x.  [para(19701(a,1),10367(a,1,2,1)),rewrite([9750(10),9778(12,R),9756(11)])].

given #941 (T,wt=15): 27653 f(f(c_0,x),f(y,f(f(z,x),f(u,x)))) = x.  [para(19735(a,1),10367(a,1,2,1)),rewrite([9750(10),9778(12,R),9750(11)])].

given #942 (T,wt=15): 27654 f(f(x,c_0),f(y,f(f(x,z),f(u,x)))) = x.  [para(19792(a,1),10367(a,1,2,1)),rewrite([9750(10),9778(12,R),9756(11)])].

given #943 (A,wt=23): 328 f(f(x,y),f(f(f(x,y),f(x,z)),f(u,y))) = f(f(x,y),f(x,z)).  [para(26(a,1),12(a,1,1))].

given #944 (T,wt=15): 27655 f(f(c_0,x),f(y,f(f(x,z),f(u,x)))) = x.  [para(19826(a,1),10367(a,1,2,1)),rewrite([9750(10),9778(12,R),9750(11)])].

given #945 (T,wt=15): 27686 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0.  [para(10368(a,1),113(a,1,2)),rewrite([9778(10,R),9750(8),9778(12,R),9750(10),9778(8,R),7(8),9778(8,R),9750(6)]),flip(a)].

given #946 (T,wt=15): 27736 f(f(x,x),f(f(f(y,x),f(x,z)),u)) = x.  [para(9784(a,1),10369(a,1,2,1)),rewrite([9750(9),9778(9,R),9755(9)])].

given #947 (T,wt=15): 27737 f(f(x,x),f(f(f(x,y),f(x,z)),u)) = x.  [para(9785(a,1),10369(a,1,2,1)),rewrite([9750(9),9778(9,R),9755(9)])].

given #948 (A,wt=23): 329 f(f(x,y),f(f(y,z),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)).  [para(26(a,1),13(a,1,1))].

given #949 (T,wt=15): 27738 f(f(x,x),f(f(f(y,x),f(z,x)),u)) = x.  [para(18570(a,1),10369(a,1,2,1)),rewrite([9750(9),9778(9,R),9755(9)])].

given #950 (T,wt=15): 27739 f(f(x,x),f(f(f(x,y),f(z,x)),u)) = x.  [para(18571(a,1),10369(a,1,2,1)),rewrite([9750(9),9778(9,R),9755(9)])].

given #951 (T,wt=15): 27740 f(f(x,c_0),f(f(f(y,x),f(x,z)),u)) = x.  [para(18609(a,1),10369(a,1,2,1)),rewrite([9750(10),9778(12,R),9756(11)])].

given #952 (T,wt=15): 27741 f(f(c_0,x),f(f(f(y,x),f(x,z)),u)) = x.  [para(18659(a,1),10369(a,1,2,1)),rewrite([9750(10),9778(12,R),9750(11)])].

given #953 (A,wt=27): 331 f(f(x,f(y,z)),f(z,f(f(x,f(y,z)),f(x,u)))) = f(f(x,f(y,z)),f(x,u)).  [para(26(a,1),19(a,1,1)),rewrite([2(7)])].

given #954 (T,wt=15): 27742 f(f(x,c_0),f(f(f(x,y),f(x,z)),u)) = x.  [para(18740(a,1),10369(a,1,2,1)),rewrite([9750(10),9778(12,R),9756(11)])].

given #955 (T,wt=15): 27743 f(f(c_0,x),f(f(f(x,y),f(x,z)),u)) = x.  [para(18778(a,1),10369(a,1,2,1)),rewrite([9750(10),9778(12,R),9750(11)])].

given #956 (T,wt=15): 27744 f(f(x,c_0),f(f(f(y,x),f(z,x)),u)) = x.  [para(19701(a,1),10369(a,1,2,1)),rewrite([9750(10),9778(12,R),9756(11)])].

given #957 (T,wt=15): 27745 f(f(c_0,x),f(f(f(y,x),f(z,x)),u)) = x.  [para(19735(a,1),10369(a,1,2,1)),rewrite([9750(10),9778(12,R),9750(11)])].

given #958 (A,wt=29): 332 f(f(f(x,y),f(x,z)),f(f(x,y),f(f(f(f(x,y),f(x,z)),f(y,u)),v))) = f(x,y).  [para(26(a,1),14(a,1,2,1)),rewrite([26(16)])].

given #959 (T,wt=15): 27746 f(f(x,c_0),f(f(f(x,y),f(z,x)),u)) = x.  [para(19792(a,1),10369(a,1,2,1)),rewrite([9750(10),9778(12,R),9756(11)])].

given #960 (T,wt=15): 27747 f(f(c_0,x),f(f(f(x,y),f(z,x)),u)) = x.  [para(19826(a,1),10369(a,1,2,1)),rewrite([9750(10),9778(12,R),9750(11)])].

given #961 (T,wt=15): 27822 f(f(x,f(f(c_0,y),z)),f(x,f(y,u))) = x.  [para(11123(a,1),7(a,1,2,2))].

given #962 (T,wt=15): 27823 f(f(f(f(c_0,x),y),z),f(z,f(x,u))) = z.  [para(11123(a,1),12(a,1,2,2))].

given #963 (A,wt=23): 333 f(f(f(x,y),f(f(y,f(x,z)),u)),f(f(x,y),f(y,v))) = f(x,y).  [para(14(a,1),26(a,1,2,1)),rewrite([14(15)])].

given #964 (T,wt=15): 27824 f(f(f(x,y),z),f(z,f(f(c_0,x),u))) = z.  [para(11123(a,1),19(a,1,1,1))].

given #965 (T,wt=15): 27825 f(f(x,f(f(c_0,y),z)),f(f(y,u),x)) = x.  [para(11123(a,1),20(a,1,2,1))].

given #966 (T,wt=15): 27826 f(f(x,f(y,z)),f(f(f(c_0,y),u),x)) = x.  [para(11123(a,1),32(a,1,1,2))].

given #967 (T,wt=15): 27827 f(f(f(f(c_0,x),y),z),f(f(x,u),z)) = z.  [para(11123(a,1),71(a,1,2,1))].

given #968 (A,wt=31): 334 f(x,f(f(x,f(f(f(y,x),f(y,z)),u)),f(f(y,x),v))) = f(x,f(f(f(y,x),f(y,z)),u)).  [para(26(a,1),16(a,1,2,2,1))].

given #969 (T,wt=15): 27847 f(f(x,f(y,f(c_0,z))),f(x,f(z,u))) = x.  [para(11123(a,1),364(a,1,2,2))].

given #970 (T,wt=15): 27851 f(f(f(x,f(c_0,y)),z),f(z,f(y,u))) = z.  [para(11123(a,1),487(a,1,2,2))].

given #971 (T,wt=15): 27869 f(f(x,f(y,z)),f(x,f(f(c_0,y),u))) = x.  [para(11123(a,1),5131(a,1,1,2))].

given #972 (T,wt=15): 27873 f(f(x,f(y,z)),f(x,f(u,f(c_0,y)))) = x.  [para(11123(a,1),7949(a,1,1,2))].

given #973 (A,wt=27): 335 f(f(f(x,f(y,z)),f(f(x,y),u)),f(f(x,f(y,z)),f(x,v))) = f(x,f(y,z)).  [para(16(a,1),26(a,1,2,1)),rewrite([16(16)])].

given #974 (T,wt=15): 27876 f(f(x,f(y,z)),f(f(u,f(c_0,y)),x)) = x.  [para(11123(a,1),8033(a,1,1,2))].

given #975 (T,wt=15): 27885 f(f(x,f(f(y,c_0),z)),f(x,f(y,u))) = x.  [para(11124(a,1),7(a,1,2,2))].

given #976 (T,wt=15): 27886 f(f(f(f(x,c_0),y),z),f(z,f(x,u))) = z.  [para(11124(a,1),12(a,1,2,2))].

given #977 (T,wt=15): 27887 f(f(f(x,y),z),f(z,f(f(x,c_0),u))) = z.  [para(11124(a,1),19(a,1,1,1))].

given #978 (A,wt=23): 336 f(f(x,y),f(f(z,y),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)).  [para(26(a,1),71(a,1,1))].

given #979 (T,wt=15): 27888 f(f(x,f(f(y,c_0),z)),f(f(y,u),x)) = x.  [para(11124(a,1),20(a,1,2,1))].

given #980 (T,wt=15): 27889 f(f(x,f(y,z)),f(f(f(y,c_0),u),x)) = x.  [para(11124(a,1),32(a,1,1,2))].

given #981 (T,wt=15): 27890 f(f(f(f(x,c_0),y),z),f(f(x,u),z)) = z.  [para(11124(a,1),71(a,1,2,1))].

given #982 (T,wt=15): 27909 f(f(x,f(y,f(z,c_0))),f(x,f(z,u))) = x.  [para(11124(a,1),364(a,1,2,2))].

given #983 (A,wt=19): 340 f(x,f(f(y,x),f(f(f(y,x),f(y,z)),u))) = f(y,x).  [para(26(a,1),23(a,1,2,1)),rewrite([26(11)])].

given #984 (T,wt=15): 27913 f(f(f(x,f(y,c_0)),z),f(z,f(y,u))) = z.  [para(11124(a,1),487(a,1,2,2))].

given #985 (T,wt=15): 27926 f(f(x,f(y,z)),f(x,f(f(y,c_0),u))) = x.  [para(11124(a,1),5131(a,1,1,2))].

given #986 (T,wt=15): 27929 f(f(x,f(y,z)),f(x,f(u,f(y,c_0)))) = x.  [para(11124(a,1),7949(a,1,1,2))].

given #987 (T,wt=15): 27932 f(f(x,f(y,z)),f(f(u,f(y,c_0)),x)) = x.  [para(11124(a,1),8033(a,1,1,2))].

given #988 (A,wt=19): 341 f(f(f(x,y),f(y,z)),f(f(x,y),f(x,u))) = f(x,y).  [para(23(a,1),26(a,1,2,1)),rewrite([23(11)])].

given #989 (T,wt=15): 27935 f(f(x,f(f(c_0,y),z)),f(x,f(u,y))) = x.  [para(11130(a,1),7(a,1,2,2))].

given #990 (T,wt=15): 27936 f(f(f(f(c_0,x),y),z),f(z,f(u,x))) = z.  [para(11130(a,1),12(a,1,2,2))].

given #991 (T,wt=15): 27937 f(f(f(x,y),z),f(z,f(f(c_0,y),u))) = z.  [para(11130(a,1),19(a,1,1,1))].

given #992 (T,wt=15): 27938 f(f(x,f(f(c_0,y),z)),f(f(u,y),x)) = x.  [para(11130(a,1),20(a,1,2,1))].

given #993 (A,wt=37): 342 f(f(f(x,y),f(x,z)),f(f(f(f(x,y),f(x,z)),f(y,u)),f(f(x,y),v))) = f(f(f(x,y),f(x,z)),f(y,u)).  [para(26(a,1),18(a,1,2,2,1))].

given #994 (T,wt=15): 27939 f(f(x,f(y,z)),f(f(f(c_0,z),u),x)) = x.  [para(11130(a,1),32(a,1,1,2))].

given #995 (T,wt=15): 27940 f(f(f(f(c_0,x),y),z),f(f(u,x),z)) = z.  [para(11130(a,1),71(a,1,2,1))].

given #996 (T,wt=15): 27960 f(f(x,f(y,f(c_0,z))),f(x,f(u,z))) = x.  [para(11130(a,1),364(a,1,2,2))].

given #997 (T,wt=15): 27964 f(f(f(x,f(c_0,y)),z),f(z,f(u,y))) = z.  [para(11130(a,1),487(a,1,2,2))].

given #998 (A,wt=27): 343 f(f(f(x,f(y,z)),f(f(y,x),u)),f(f(x,f(y,z)),f(x,v))) = f(x,f(y,z)).  [para(18(a,1),26(a,1,2,1)),rewrite([18(16)])].

given #999 (T,wt=15): 27978 f(f(x,f(y,z)),f(x,f(f(c_0,z),u))) = x.  [para(11130(a,1),5131(a,1,1,2))].

given #1000 (T,wt=15): 27981 f(f(x,f(y,z)),f(x,f(u,f(c_0,z)))) = x.  [para(11130(a,1),7949(a,1,1,2))].

given #1001 (T,wt=15): 27984 f(f(x,f(y,z)),f(f(u,f(c_0,z)),x)) = x.  [para(11130(a,1),8033(a,1,1,2))].

given #1002 (T,wt=15): 28003 f(x,f(c_0,f(y,f(y,f(f(c_0,x),z))))) = c_0.  [para(11233(a,1),11131(a,1,2,2))].

given #1003 (A,wt=19): 344 f(f(f(x,y),f(x,z)),f(f(x,y),f(y,u))) = f(x,y).  [para(26(a,1),26(a,1,2,1)),rewrite([26(11)])].

given #1004 (T,wt=15): 28035 f(x,f(c_0,f(y,f(y,f(z,f(c_0,x)))))) = c_0.  [para(11233(a,1),11138(a,1,2,2))].

given #1005 (T,wt=15): 28126 f(x,f(c_0,f(y,f(y,f(f(x,x),z))))) = c_0.  [para(11233(a,1),11207(a,1,2,2))].

given #1006 (T,wt=15): 28149 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0.  [para(11233(a,1),11209(a,1,2,2))].

given #1007 (T,wt=15): 28226 f(x,f(c_0,f(y,f(y,f(f(x,c_0),z))))) = c_0.  [para(11233(a,1),11217(a,1,2,2))].

given #1008 (A,wt=27): 349 f(f(f(x,y),z),f(x,f(f(f(x,y),z),f(u,z)))) = f(f(f(x,y),z),f(u,z)).  [para(28(a,1),8(a,1,2)),rewrite([2(5),2(8)])].

given #1009 (T,wt=15): 28252 f(x,f(c_0,f(y,f(y,f(z,f(x,c_0)))))) = c_0.  [para(11233(a,1),11220(a,1,2,2))].

given #1010 (T,wt=15): 28597 f(f(x,y),f(c_0,z)) = f(f(z,z),f(y,x)).  [para(2(a,1),11630(a,1,1))].

given #1011 (T,wt=15): 28632 f(f(f(x,y),z),f(z,f(u,f(x,c_0)))) = z.  [para(12004(a,1),19(a,1,1,1))].

given #1012 (T,wt=15): 28633 f(f(x,f(y,f(z,c_0))),f(f(z,u),x)) = x.  [para(12004(a,1),20(a,1,2,1))].

given #1013 (A,wt=23): 351 f(x,f(f(x,y),f(f(x,f(f(f(x,y),f(z,y)),u)),v))) = f(x,y).  [para(28(a,1),9(a,1,2,1)),rewrite([28(13)])].

given #1014 (T,wt=15): 28634 f(f(f(x,f(y,c_0)),z),f(f(y,u),z)) = z.  [para(12004(a,1),71(a,1,2,1))].

given #1015 (T,wt=15): 28705 f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)).  [para(12244(a,1),33(a,1,2)),flip(a)].

given #1016 (T,wt=15): 28747 f(f(c_0,f(x,f(x,f(y,z)))),f(y,x)) = c_0.  [para(12340(a,1),2(a,1)),flip(a)].

given #1017 (T,wt=15): 28750 f(f(f(x,y),z),f(c_0,f(z,f(z,x)))) = c_0.  [para(3(a,1),12340(a,1,2,2,2,2))].

given #1018 (A,wt=23): 352 f(x,f(f(x,y),f(z,f(f(x,y),f(f(x,f(y,u)),v))))) = f(x,y).  [para(9(a,1),28(a,1,2,1)),rewrite([9(15)])].

given #1019 (T,wt=15): 28762 f(f(f(x,y),z),f(c_0,f(z,f(x,z)))) = c_0.  [para(75(a,1),12340(a,1,2,2,2))].

given #1020 (T,wt=15): 28773 f(f(x,y),f(c_0,f(f(c_0,f(x,z)),y))) = c_0.  [para(741(a,2),12340(a,1,2,2)),rewrite([9778(5,R)])].

given #1021 (T,wt=15): 28848 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x).  [para(143(a,1),9092(a,1)),rewrite([9778(5,R),2(5)])].

given #1022 (T,wt=15): 28852 f(f(x,y),f(c_0,f(f(c_0,f(y,z)),x))) = c_0.  [para(2(a,1),12345(a,1,2,2))].

given #1023 (A,wt=23): 354 f(f(x,y),f(f(f(x,y),f(z,y)),f(u,x))) = f(f(x,y),f(z,y)).  [para(28(a,1),12(a,1,1))].

given #1024 (T,wt=15): 28854 f(f(x,f(y,z)),f(c_0,f(x,f(c_0,y)))) = c_0.  [para(3(a,1),12345(a,1,2,2,2,2))].

given #1025 (T,wt=15): 28855 f(f(x,f(y,z)),f(c_0,f(x,f(c_0,z)))) = c_0.  [para(6(a,1),12345(a,1,2,2,2,2))].

given #1026 (T,wt=15): 28868 f(f(x,f(y,z)),f(c_0,f(x,f(y,c_0)))) = c_0.  [para(75(a,1),12345(a,1,2,2,2))].

given #1027 (T,wt=15): 28873 f(f(x,f(y,z)),f(c_0,f(x,f(z,c_0)))) = c_0.  [para(85(a,1),12345(a,1,2,2,2))].

given #1028 (A,wt=23): 356 f(f(x,y),f(f(x,z),f(f(x,y),f(u,y)))) = f(f(x,y),f(u,y)).  [para(28(a,1),13(a,1,1))].

given #1029 (T,wt=15): 28914 f(f(f(f(c_0,x),y),z),f(c_0,f(z,x))) = c_0.  [para(90(a,1),12345(a,1,2))].

given #1030 (T,wt=15): 28920 f(f(f(f(x,c_0),y),z),f(c_0,f(z,x))) = c_0.  [para(97(a,1),12345(a,1,2))].

given #1031 (T,wt=15): 28928 f(f(f(x,f(y,y)),z),f(c_0,f(z,y))) = c_0.  [para(10323(a,1),12345(a,1,2,2))].

given #1032 (T,wt=15): 28930 f(f(f(f(x,x),y),z),f(c_0,f(z,x))) = c_0.  [para(10324(a,1),12345(a,1,2,2))].

given #1033 (A,wt=27): 359 f(f(f(x,y),z),f(y,f(f(f(x,y),z),f(u,z)))) = f(f(f(x,y),z),f(u,z)).  [para(28(a,1),19(a,1,1)),rewrite([2(7)])].

given #1034 (T,wt=15): 28939 f(f(f(x,f(y,c_0)),z),f(c_0,f(z,y))) = c_0.  [para(143(a,1),12345(a,1,2))].

given #1035 (T,wt=15): 28940 f(f(x,y),f(c_0,f(f(c_0,f(z,y)),x))) = c_0.  [para(2(a,1),12347(a,1,2,2))].

given #1036 (T,wt=15): 28948 f(f(x,f(f(y,y),z)),f(c_0,f(x,y))) = c_0.  [para(45(a,1),12347(a,1,2,2,2,2)),rewrite([9755(7)])].

given #1037 (T,wt=15): 28949 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0.  [para(62(a,1),12347(a,1,2,2,2,2)),rewrite([9755(7)])].

given #1038 (A,wt=29): 361 f(f(f(x,y),f(z,y)),f(f(x,y),f(f(f(f(x,y),f(z,y)),f(x,u)),v))) = f(x,y).  [para(28(a,1),14(a,1,2,1)),rewrite([28(16)])].

given #1039 (T,wt=15): 28976 f(f(c_0,f(x,y)),f(f(f(x,c_0),z),y)) = c_0.  [para(68(a,1),12347(a,1,2)),rewrite([2(8)])].

given #1040 (T,wt=15): 28997 f(f(x,f(y,f(z,c_0))),f(c_0,f(x,z))) = c_0.  [para(9766(a,1),12347(a,1,2,2,2,2)),rewrite([9755(8)])].

given #1041 (T,wt=15): 28998 f(f(x,f(f(y,c_0),z)),f(c_0,f(x,y))) = c_0.  [para(9767(a,1),12347(a,1,2,2,2,2)),rewrite([9755(8)])].

given #1042 (T,wt=15): 28999 f(f(x,f(y,f(c_0,z))),f(c_0,f(x,z))) = c_0.  [para(11091(a,1),12347(a,1,2,2,2,2)),rewrite([9750(9)])].

given #1043 (A,wt=23): 362 f(x,f(f(y,x),f(z,f(f(y,x),f(f(x,f(y,u)),v))))) = f(y,x).  [para(14(a,1),28(a,1,2,1)),rewrite([14(15)])].

given #1044 (T,wt=15): 29000 f(f(x,f(f(c_0,y),z)),f(c_0,f(x,y))) = c_0.  [para(11125(a,1),12347(a,1,2,2,2,2)),rewrite([9750(9)])].

given #1045 (T,wt=15): 29024 f(f(c_0,f(x,y)),f(f(f(c_0,x),z),y)) = c_0.  [para(87(a,1),12347(a,1,2)),rewrite([2(8)])].

given #1046 (T,wt=15): 29030 f(f(c_0,f(x,y)),f(f(z,f(x,c_0)),y)) = c_0.  [para(114(a,1),12347(a,1,2)),rewrite([2(8)])].

given #1047 (T,wt=15): 29048 f(f(c_0,f(x,f(x,y))),f(f(z,y),x)) = c_0.  [para(12350(a,1),2(a,1)),flip(a)].

given #1048 (A,wt=31): 365 f(x,f(f(x,f(f(f(x,y),f(z,y)),u)),f(f(x,y),v))) = f(x,f(f(f(x,y),f(z,y)),u)).  [para(28(a,1),16(a,1,2,2,1))].

given #1049 (T,wt=15): 29049 f(f(x,f(y,z)),f(c_0,f(x,f(x,z)))) = c_0.  [para(2(a,1),12350(a,1,1))].

given #1050 (T,wt=15): 29067 f(f(x,f(y,f(z,x))),f(c_0,f(x,z))) = c_0.  [para(570(a,2),12350(a,1,2,2,2)),rewrite([2(3),826(7)])].

given #1051 (T,wt=15): 29073 f(f(f(x,y),z),f(c_0,f(z,f(y,y)))) = c_0.  [para(638(a,2),12350(a,1,2,2))].

given #1052 (T,wt=15): 29075 f(f(f(x,y),z),f(c_0,f(f(y,y),z))) = c_0.  [para(741(a,2),12350(a,1,2,2))].

given #1053 (A,wt=27): 366 f(x,f(f(x,f(y,z)),f(u,f(f(x,f(y,z)),f(f(x,y),v))))) = f(x,f(y,z)).  [para(16(a,1),28(a,1,2,1)),rewrite([16(16)])].

given #1054 (T,wt=15): 29082 f(x,f(c_0,f(y,f(f(z,f(y,z)),x)))) = c_0.  [para(235(a,1),12350(a,1,1)),rewrite([2(9),570(10,R),9778(7,R),9755(7),2(5)])].

given #1055 (T,wt=15): 29085 f(x,f(c_0,f(y,f(f(z,f(z,y)),x)))) = c_0.  [para(260(a,1),12350(a,1,1)),rewrite([2(9),570(10,R),9778(7,R),9755(7),2(5)])].

given #1056 (T,wt=15): 29108 f(f(f(x,y),z),f(c_0,f(f(y,c_0),z))) = c_0.  [para(9748(a,2),12350(a,1,2,2))].

given #1057 (T,wt=15): 29112 f(f(f(x,y),z),f(c_0,f(z,f(y,c_0)))) = c_0.  [para(9752(a,2),12350(a,1,2,2))].

given #1058 (A,wt=23): 367 f(f(x,y),f(f(z,x),f(f(x,y),f(u,y)))) = f(f(x,y),f(u,y)).  [para(28(a,1),71(a,1,1))].

given #1059 (T,wt=15): 29115 f(f(f(x,f(c_0,y)),z),f(c_0,f(z,y))) = c_0.  [para(11226(a,1),12350(a,1,2,2,2)),rewrite([826(8)])].

given #1060 (T,wt=15): 29117 f(f(c_0,f(x,y)),f(f(z,f(c_0,x)),y)) = c_0.  [para(11229(a,1),12350(a,1,2,2,2)),rewrite([15(8),2(8)])].

given #1061 (T,wt=15): 29123 f(f(f(x,y),z),f(c_0,f(z,f(c_0,y)))) = c_0.  [para(11231(a,2),12350(a,1,2,2))].

given #1062 (T,wt=15): 29126 f(f(f(x,y),z),f(c_0,f(f(c_0,y),z))) = c_0.  [para(11233(a,2),12350(a,1,2,2))].

given #1063 (A,wt=19): 373 f(x,f(f(x,y),f(f(f(x,y),f(z,y)),u))) = f(x,y).  [para(28(a,1),23(a,1,2,1)),rewrite([28(11)])].

given #1064 (T,wt=15): 29163 f(f(c_0,f(x,f(x,f(y,z)))),f(z,x)) = c_0.  [para(12351(a,1),2(a,1)),flip(a)].

given #1065 (T,wt=15): 29186 f(f(x,y),f(c_0,f(f(c_0,f(z,x)),y))) = c_0.  [para(741(a,2),12351(a,1,2,2)),rewrite([9778(5,R)])].

given #1066 (T,wt=15): 29242 f(f(c_0,f(x,f(y,x))),f(f(z,y),x)) = c_0.  [para(12355(a,1),2(a,1)),flip(a)].

given #1067 (T,wt=15): 29243 f(f(x,f(y,z)),f(c_0,f(x,f(z,x)))) = c_0.  [para(2(a,1),12355(a,1,1))].

given #1068 (A,wt=19): 374 f(x,f(f(x,y),f(z,f(f(x,y),f(y,u))))) = f(x,y).  [para(23(a,1),28(a,1,2,1)),rewrite([23(11)])].

given #1069 (T,wt=15): 29335 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0.  [para(11233(a,1),12357(a,1,2,2))].

given #1070 (T,wt=15): 29383 f(f(x,f(y,z)),f(x,f(u,f(u,y)))) = x.  [para(12361(a,1),210(a,1,1,2,2)),rewrite([2(5),9750(5),9778(11,R),9750(8)])].

given #1071 (T,wt=15): 29384 f(f(f(x,y),z),f(z,f(u,f(u,x)))) = z.  [para(12361(a,1),220(a,1,1,1,2)),rewrite([2(5),9750(5),9778(11,R),9750(8)])].

given #1072 (T,wt=15): 29385 f(f(f(x,f(x,y)),z),f(z,f(y,u))) = z.  [para(12361(a,1),227(a,1,2,2,2)),rewrite([9778(9,R),9750(6),2(8),9750(8)])].

given #1073 (A,wt=37): 375 f(f(f(x,y),f(z,y)),f(f(f(f(x,y),f(z,y)),f(x,u)),f(f(x,y),v))) = f(f(f(x,y),f(z,y)),f(x,u)).  [para(28(a,1),18(a,1,2,2,1))].

given #1074 (T,wt=15): 29387 f(f(x,f(y,z)),f(f(u,f(u,y)),x)) = x.  [para(12361(a,1),232(a,1,1,2,2)),rewrite([2(5),9750(5),9778(11,R),9750(8)])].

given #1075 (T,wt=15): 29388 f(f(x,f(y,f(y,z))),f(f(z,u),x)) = x.  [para(12361(a,1),235(a,1,2,1,2)),rewrite([9778(9,R),9750(6),2(8),9750(8)])].

given #1076 (T,wt=15): 29390 f(f(f(x,y),z),f(f(u,f(u,x)),z)) = z.  [para(12361(a,1),239(a,1,1,1,2)),rewrite([2(5),9750(5),9778(11,R),9750(8)])].

given #1077 (T,wt=15): 29391 f(f(x,f(y,f(y,z))),f(x,f(z,u))) = x.  [para(12361(a,1),243(a,1,1,2,2)),rewrite([2(6),9750(6),9778(10,R),9750(8)])].

given #1078 (A,wt=27): 376 f(x,f(f(x,f(y,z)),f(u,f(f(x,f(y,z)),f(f(y,x),v))))) = f(x,f(y,z)).  [para(18(a,1),28(a,1,2,1)),rewrite([18(16)])].

given #1079 (T,wt=15): 29394 f(f(f(x,f(x,y)),z),f(f(y,u),z)) = z.  [para(12361(a,1),265(a,1,1,1,2)),rewrite([2(6),9750(6),9778(10,R),9750(8)])].

given #1080 (T,wt=15): 29501 f(x,f(c_0,f(y,f(y,f(z,f(x,z)))))) = c_0.  [para(184(a,1),12369(a,1,2,2)),rewrite([9755(9),2(7)])].

given #1081 (T,wt=15): 29520 f(f(x,f(y,z)),f(x,f(u,f(u,z)))) = x.  [para(12369(a,1),210(a,1,1,2,2)),rewrite([2(5),9750(5),9778(11,R),9750(8)])].

given #1082 (T,wt=15): 29521 f(f(f(x,y),z),f(z,f(u,f(u,y)))) = z.  [para(12369(a,1),220(a,1,1,1,2)),rewrite([2(5),9750(5),9778(11,R),9750(8)])].

given #1083 (A,wt=19): 377 f(f(f(x,y),f(z,y)),f(f(x,y),f(x,u))) = f(x,y).  [para(28(a,1),26(a,1,2,1)),rewrite([28(11)])].

given #1084 (T,wt=15): 29522 f(f(f(x,f(x,y)),z),f(z,f(u,y))) = z.  [para(12369(a,1),227(a,1,2,2,2)),rewrite([9778(9,R),9750(6),2(8),9750(8)])].

given #1085 (T,wt=15): 29524 f(f(x,f(y,z)),f(f(u,f(u,z)),x)) = x.  [para(12369(