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

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

% Reading from file sh1.in

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

formulas(sos).
f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).
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(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).  [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).

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
2 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).  [assumption].
3 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).
2 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).  [assumption].
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=15): 2 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).  [assumption].

given #2 (I,wt=43): 3 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)].

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

given #4 (T,wt=25): 5 f(f(f(x,f(y,z)),f(f(u,f(x,f(y,z))),f(x,f(y,z)))),f(u,x)) = u.  [para(2(a,1),2(a,1,2,2))].

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

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

given #7 (T,wt=11): 36 f(x,f(f(x,x),x)) = f(x,x).  [para(15(a,1),4(a,1,2)),rewrite([15(8)]),flip(a)].

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

given #9 (F,wt=34): 61 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").  [back_rewrite(3),rewrite([51(7)]),xx(a)].

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

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

given #12 (T,wt=13): 60 f(f(x,f(f(y,x),x)),f(y,y)) = y.  [back_rewrite(39),rewrite([50(4),50(9)])].

given #13 (T,wt=15): 47 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x).  [back_rewrite(35),rewrite([36(3),36(4),36(8)])].

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

given #15 (T,wt=15): 48 f(f(x,f(f(f(y,y),x),x)),y) = f(y,y).  [back_rewrite(33),rewrite([36(3),36(8)])].

given #16 (T,wt=15): 58 f(f(x,x),f(x,f(y,f(f(x,y),y)))) = x.  [para(36(a,1),15(a,1,1))].

given #17 (T,wt=17): 55 f(f(f(x,y),f(x,y)),f(f(x,y),x)) = f(x,y).  [para(36(a,1),13(a,1,1))].

given #18 (T,wt=17): 131 f(x,f(f(f(f(y,x),f(y,x)),x),x)) = f(y,x).  [para(48(a,1),6(a,1,1,2,1)),rewrite([36(7),51(7)]),flip(a)].

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

given #20 (T,wt=9): 163 f(f(x,x),f(y,x)) = x.  [para(131(a,1),2(a,1,2)),rewrite([36(3)])].

given #21 (T,wt=9): 264 f(f(x,y),f(y,y)) = y.  [back_rewrite(184),rewrite([256(4),256(7),262(7)])].

given #22 (T,wt=9): 280 f(f(x,x),f(x,y)) = x.  [back_rewrite(244),rewrite([269(4)])].

given #23 (T,wt=9): 324 f(f(x,y),f(x,x)) = x.  [back_rewrite(89),rewrite([269(3),269(8),269(9),298(13),298(7),298(7),298(9)])].

given #24 (A,wt=11): 169 f(x,f(y,f(x,x))) = f(x,x).  [para(131(a,1),4(a,1,2)),rewrite([36(3),36(4),50(4),36(3),36(6)])].

given #25 (T,wt=11): 250 f(f(x,y),f(y,f(x,y))) = y.  [para(163(a,1),131(a,1,2,1,1,1)),rewrite([163(4),163(4),163(7)])].

given #26 (T,wt=11): 258 f(x,f(f(x,x),y)) = f(x,x).  [back_rewrite(239),rewrite([250(4)])].

given #27 (T,wt=11): 263 f(f(x,f(y,y)),y) = f(y,y).  [back_rewrite(187),rewrite([256(7),256(13),262(12)])].

given #28 (T,wt=11): 269 f(x,f(f(y,x),x)) = f(y,x).  [back_rewrite(131),rewrite([256(4)])].

given #29 (A,wt=19): 237 f(f(x,x),f(f(x,f(x,x)),f(y,x))) = f(x,f(x,x)).  [para(163(a,1),4(a,1,1,1)),rewrite([163(4),36(3),165(4),163(6),165(9)])].

given #30 (T,wt=11): 297 f(x,f(f(x,y),x)) = f(x,y).  [back_rewrite(181),rewrite([269(3),269(4),240(4),269(6)])].

given #31 (T,wt=11): 299 f(f(x,f(y,z)),f(x,z)) = x.  [back_rewrite(171),rewrite([269(6)])].

given #32 (T,wt=11): 321 f(f(x,f(y,z)),f(x,y)) = x.  [back_rewrite(94),rewrite([269(3),269(4),269(6),269(6)])].

given #33 (T,wt=11): 333 f(f(f(x,x),y),x) = f(x,x).  [back_rewrite(48),rewrite([269(4)])].

given #34 (A,wt=13): 256 f(f(f(x,y),f(x,y)),y) = f(x,y).  [para(163(a,1),163(a,1,2))].

given #35 (T,wt=11): 338 f(f(x,y),f(x,f(y,z))) = x.  [back_rewrite(38),rewrite([298(6),298(6),298(7),269(3),269(4),269(9),269(10),298(14)])].

given #36 (T,wt=11): 353 f(f(x,y),f(x,f(z,y))) = x.  [back_rewrite(2),rewrite([269(3)])].

given #37 (T,wt=11): 374 f(f(x,y),x) = f(x,f(x,y)).  [para(299(a,1),269(a,1,2))].

given #38 (T,wt=11): 380 f(x,f(x,f(y,x))) = f(y,x).  [back_rewrite(363),rewrite([374(3)])].

given #39 (A,wt=15): 281 f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)).  [back_rewrite(243),rewrite([269(6),269(5),269(10)])].

% Operation f is commutative; C redundancy checks enabled.

given #40 (F,wt=34): 451 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(61),rewrite([421(16),421(21)]),flip(b)].

given #41 (T,wt=7): 421 f(x,y) = f(y,x).  [para(264(a,1),281(a,1,1,1,2)),rewrite([264(3),264(4)])].

given #42 (T,wt=11): 381 f(x,f(x,f(x,y))) = f(x,y).  [back_rewrite(326),rewrite([374(2),374(3)])].

given #43 (T,wt=11): 427 f(x,f(y,f(x,y))) = f(x,x).  [para(321(a,1),281(a,1,1)),flip(a)].

given #44 (T,wt=11): 453 f(f(x,y),f(y,f(x,z))) = y.  [para(421(a,1),338(a,1,1))].

given #45 (A,wt=19): 291 f(f(f(x,y),f(z,x)),f(f(x,y),f(y,u))) = f(x,y).  [back_rewrite(217),rewrite([269(4),269(7),269(6),269(7),269(8),269(10),269(10),269(10)])].

given #46 (T,wt=11): 454 f(f(x,y),f(f(y,z),x)) = x.  [para(421(a,1),338(a,1,2))].

given #47 (T,wt=11): 455 f(f(x,y),f(y,f(z,x))) = y.  [para(421(a,1),353(a,1,1))].

given #48 (T,wt=11): 456 f(f(x,y),f(f(z,y),x)) = x.  [para(421(a,1),353(a,1,2))].

given #49 (T,wt=11): 464 f(x,f(y,f(y,x))) = f(x,x).  [para(421(a,1),427(a,1,2,2))].

given #50 (A,wt=19): 301 f(f(x,x),f(f(f(x,x),y),f(x,z))) = f(f(x,x),y).  [back_rewrite(128),rewrite([269(5),269(6),269(10)])].

given #51 (T,wt=11): 466 f(f(f(x,y),z),f(z,y)) = z.  [para(264(a,1),453(a,1,2,2))].

given #52 (T,wt=11): 467 f(f(f(x,y),z),f(z,x)) = z.  [para(324(a,1),453(a,1,2,2))].

given #53 (T,wt=11): 471 f(f(x,f(y,z)),f(y,x)) = x.  [para(453(a,1),421(a,1)),flip(a)].

given #54 (T,wt=11): 472 f(f(x,y),f(f(x,z),y)) = y.  [para(421(a,1),453(a,1,2))].

given #55 (A,wt=25): 304 f(f(f(x,x),y),f(f(x,x),f(z,f(f(f(x,x),y),f(u,x))))) = f(x,x).  [back_rewrite(125),rewrite([269(4),269(8),269(10),298(12),269(7)])].

given #56 (T,wt=11): 504 f(f(x,f(y,z)),f(z,x)) = x.  [para(264(a,1),454(a,1,2,1))].

given #57 (T,wt=11): 519 f(f(x,y),f(f(z,x),y)) = y.  [para(421(a,1),455(a,1,2))].

given #58 (T,wt=13): 356 f(x,f(f(x,y),f(z,y))) = f(x,y).  [back_rewrite(282),rewrite([298(6)])].

given #59 (T,wt=13): 399 f(x,f(f(x,y),f(y,z))) = f(x,y).  [para(338(a,1),299(a,1,1))].

given #60 (A,wt=19): 307 f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y).  [back_rewrite(122),rewrite([269(5),269(10)])].

given #61 (T,wt=13): 470 f(x,f(f(y,x),f(y,z))) = f(y,x).  [para(453(a,1),353(a,1,2)),rewrite([421(4)])].

given #62 (T,wt=13): 480 f(x,f(f(y,x),f(z,y))) = f(y,x).  [para(264(a,1),291(a,1,2)),rewrite([421(4)])].

given #63 (T,wt=13): 513 f(x,f(f(y,z),f(x,y))) = f(x,y).  [para(454(a,1),453(a,1,2)),rewrite([421(4)])].

given #64 (T,wt=13): 518 f(x,f(f(y,z),f(x,z))) = f(x,z).  [para(353(a,1),455(a,1,2)),rewrite([421(4)])].

given #65 (A,wt=21): 310 f(f(x,y),f(x,f(z,f(f(x,y),f(f(x,f(u,y)),v))))) = x.  [back_rewrite(115),rewrite([269(3),269(6),269(8),269(9),269(12),298(13),298(7),269(4),269(7),298(15)])].

given #66 (T,wt=13): 525 f(x,f(f(y,z),f(y,x))) = f(y,x).  [para(453(a,1),455(a,1,2)),rewrite([421(4)])].

given #67 (T,wt=13): 531 f(x,f(f(y,z),f(z,x))) = f(z,x).  [para(455(a,1),455(a,1,2)),rewrite([421(4)])].

given #68 (T,wt=15): 322 f(x,f(f(x,y),f(f(x,x),z))) = f(x,y).  [back_rewrite(93),rewrite([269(3),269(5),269(8)])].

given #69 (T,wt=15): 327 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y).  [back_rewrite(84),rewrite([269(3),269(8)])].

given #70 (A,wt=23): 312 f(f(x,y),f(f(f(x,y),f(z,y)),f(u,x))) = f(f(x,y),f(z,y)).  [back_rewrite(108),rewrite([269(3),269(5),269(8),269(11),269(14)])].

given #71 (T,wt=15): 330 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x.  [back_rewrite(65),rewrite([298(6),269(9),269(9),298(10)])].

given #72 (T,wt=15): 359 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x.  [back_rewrite(277),rewrite([298(13),298(7),298(12)])].

given #73 (T,wt=15): 360 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x.  [back_rewrite(276),rewrite([298(4),298(10)])].

given #74 (T,wt=15): 392 f(x,f(f(y,x),f(f(x,x),z))) = f(y,x).  [para(264(a,1),338(a,1,1))].

given #75 (A,wt=23): 314 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,x))) = f(f(x,y),f(y,z)).  [back_rewrite(106),rewrite([269(3),269(4),269(5),269(6),269(8),269(8),269(10),269(11),269(12),269(14),269(14)])].

given #76 (T,wt=15): 402 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x).  [para(264(a,1),353(a,1,1))].

given #77 (T,wt=15): 429 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)).  [para(281(a,1),256(a,2)),rewrite([421(3),421(4),421(7),421(8),421(10),356(10)])].

given #78 (T,wt=11): 1380 f(x,f(y,y)) = f(x,f(x,y)).  [para(464(a,1),429(a,1,2))].

given #79 (T,wt=11): 1415 f(x,f(x,f(y,y))) = f(x,y).  [para(163(a,1),1380(a,1,2)),flip(a)].

given #80 (A,wt=23): 316 f(f(x,y),f(f(f(x,y),f(z,y)),f(x,u))) = f(f(x,y),f(z,y)).  [back_rewrite(104),rewrite([269(3),269(5),269(8),269(7),269(11),269(14)])].

given #81 (F,wt=34): 1398 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(451),rewrite([1380(27),1380(32)])].

given #82 (T,wt=11): 1422 f(f(x,x),y) = f(y,f(y,x)).  [para(1380(a,1),421(a,1)),flip(a)].

given #83 (T,wt=11): 1423 f(x,f(y,y)) = f(x,f(y,x)).  [para(421(a,1),1380(a,2,2))].

given #84 (T,wt=11): 1547 f(x,f(f(y,y),x)) = f(x,y).  [para(421(a,1),1415(a,1,2))].

given #85 (T,wt=11): 1647 f(f(x,x),y) = f(y,f(x,y)).  [para(421(a,1),1422(a,2,2))].

given #86 (A,wt=19): 317 f(f(f(x,y),f(z,x)),f(f(x,y),f(u,y))) = f(x,y).  [back_rewrite(103),rewrite([269(4),269(7),269(7),269(10),269(10)])].

given #87 (T,wt=15): 441 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)).  [back_rewrite(387),rewrite([421(3)])].

given #88 (T,wt=15): 442 f(f(x,y),f(x,f(f(x,f(z,y)),u))) = x.  [back_rewrite(354),rewrite([421(6)])].

given #89 (T,wt=15): 445 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x.  [back_rewrite(328),rewrite([421(6)])].

given #90 (T,wt=15): 461 f(f(x,f(y,f(z,y))),f(x,f(z,z))) = x.  [para(427(a,1),353(a,1,2,2))].

given #91 (A,wt=19): 325 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,x)))))) = x.  [back_rewrite(88),rewrite([269(3),269(7),269(8),298(11),269(4)])].

given #92 (T,wt=15): 503 f(x,f(f(f(x,x),y),f(z,x))) = f(z,x).  [para(264(a,1),454(a,1,1))].

given #93 (T,wt=15): 505 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z).  [para(324(a,1),454(a,1,1))].

given #94 (T,wt=15): 522 f(f(f(x,f(y,x)),z),f(z,f(y,y))) = z.  [para(427(a,1),455(a,1,2,2))].

given #95 (T,wt=15): 532 f(x,f(f(y,f(x,x)),f(z,x))) = f(z,x).  [para(264(a,1),456(a,1,1))].

given #96 (A,wt=17): 334 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y).  [back_rewrite(45),rewrite([269(3),269(5),298(6),269(3),269(4),269(6),269(9)])].

given #97 (T,wt=15): 533 f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z).  [para(324(a,1),456(a,1,1))].

given #98 (T,wt=15): 538 f(f(x,f(y,f(z,y))),f(f(z,z),x)) = x.  [para(427(a,1),456(a,1,2,1))].

given #99 (T,wt=15): 545 f(x,f(y,f(f(y,z),x))) = f(f(y,z),x).  [para(454(a,1),456(a,1,2)),rewrite([421(3),421(4)])].

given #100 (T,wt=15): 549 f(x,f(y,f(f(z,y),x))) = f(f(z,y),x).  [para(456(a,1),456(a,1,2)),rewrite([421(3),421(4)])].

given #101 (A,wt=19): 336 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)).  [back_rewrite(42),rewrite([298(4),269(6),269(6),269(12)])].

given #102 (T,wt=15): 554 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x.  [para(464(a,1),353(a,1,2,2))].

given #103 (T,wt=15): 565 f(f(f(x,f(x,y)),z),f(z,f(y,y))) = z.  [para(464(a,1),455(a,1,2,2))].

given #104 (T,wt=15): 567 f(f(x,f(y,f(y,z))),f(f(z,z),x)) = x.  [para(464(a,1),456(a,1,2,1))].

given #105 (T,wt=15): 581 f(f(f(x,x),y),f(y,f(z,f(x,z)))) = y.  [para(427(a,1),466(a,1,1,1))].

given #106 (A,wt=21): 339 f(f(x,y),f(x,f(f(f(x,y),f(z,f(x,f(u,y)))),v))) = x.  [back_rewrite(37),rewrite([269(3),269(8),269(9),298(13),298(7),269(4),269(9),298(15)])].

given #107 (T,wt=15): 586 f(f(f(x,x),y),f(y,f(z,f(z,x)))) = y.  [para(464(a,1),466(a,1,1,1))].

given #108 (T,wt=15): 636 f(f(x,f(y,y)),f(f(z,f(y,z)),x)) = x.  [para(427(a,1),504(a,1,1,2))].

given #109 (T,wt=15): 639 f(f(x,f(y,y)),f(f(z,f(z,y)),x)) = x.  [para(464(a,1),504(a,1,1,2))].

given #110 (T,wt=15): 648 f(f(f(x,f(y,x)),z),f(f(y,y),z)) = z.  [para(427(a,1),519(a,1,2,1))].

given #111 (A,wt=17): 340 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y).  [back_rewrite(32),rewrite([298(6),269(3),269(6),269(9)])].

given #112 (T,wt=15): 656 f(f(f(x,f(x,y)),z),f(f(y,y),z)) = z.  [para(464(a,1),519(a,1,2,1))].

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

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

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

given #116 (A,wt=17): 342 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y).  [back_rewrite(30),rewrite([269(3),269(5),298(6),269(3),269(4),269(9)])].

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

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

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

given #120 (T,wt=15): 676 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x.  [para(471(a,1),356(a,1,2,1)),rewrite([471(10)])].

given #121 (A,wt=23): 345 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(v,f(x,y)))))) = x.  [back_rewrite(26),rewrite([269(6),269(11),269(13),298(14),298(6),269(8),298(14)])].

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

given #123 (T,wt=15): 681 f(f(x,f(y,z)),f(x,f(u,f(z,x)))) = x.  [para(504(a,1),356(a,1,2,1)),rewrite([504(10)])].

given #124 (T,wt=15): 683 f(f(x,y),f(y,f(z,f(f(u,x),y)))) = y.  [para(519(a,1),356(a,1,2,1)),rewrite([519(10)])].

given #125 (T,wt=15): 686 f(f(x,y),f(x,f(f(x,f(y,z)),u))) = x.  [para(338(a,1),399(a,1,2,1)),rewrite([338(10)])].

given #126 (A,wt=19): 348 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)).  [back_rewrite(17),rewrite([298(4),269(6),269(12)])].

given #127 (T,wt=15): 690 f(f(x,y),f(y,f(f(y,f(x,z)),u))) = y.  [para(453(a,1),399(a,1,2,1)),rewrite([453(10)])].

given #128 (T,wt=15): 693 f(f(x,y),f(x,f(f(f(y,z),x),u))) = x.  [para(454(a,1),399(a,1,2,1)),rewrite([454(10)])].

given #129 (T,wt=15): 694 f(f(x,y),f(y,f(f(y,f(z,x)),u))) = y.  [para(455(a,1),399(a,1,2,1)),rewrite([455(10)])].

given #130 (T,wt=15): 696 f(f(x,y),f(x,f(f(f(z,y),x),u))) = x.  [para(456(a,1),399(a,1,2,1)),rewrite([456(10)])].

given #131 (A,wt=21): 350 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,f(v,y))))))) = x.  [back_rewrite(7),rewrite([269(3),269(8),269(9),298(13),298(7),269(4),298(15)])].

given #132 (T,wt=15): 699 f(f(f(x,y),z),f(z,f(f(z,y),u))) = z.  [para(466(a,1),399(a,1,2,1)),rewrite([466(10)])].

given #133 (T,wt=15): 700 f(f(f(x,y),z),f(z,f(f(z,x),u))) = z.  [para(467(a,1),399(a,1,2,1)),rewrite([467(10)])].

given #134 (T,wt=15): 701 f(f(x,f(y,z)),f(x,f(f(y,x),u))) = x.  [para(471(a,1),399(a,1,2,1)),rewrite([471(10)])].

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

given #136 (A,wt=17): 352 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y).  [back_rewrite(4),rewrite([298(6),269(3),269(9)])].

given #137 (T,wt=15): 706 f(f(x,f(y,z)),f(x,f(f(z,x),u))) = x.  [para(504(a,1),399(a,1,2,1)),rewrite([504(10)])].

given #138 (T,wt=15): 707 f(f(x,y),f(y,f(f(f(z,x),y),u))) = y.  [para(519(a,1),399(a,1,2,1)),rewrite([519(10)])].

given #139 (T,wt=15): 729 f(f(x,f(y,z)),f(x,f(f(x,y),u))) = x.  [para(338(a,1),470(a,1,2,1)),rewrite([338(10)])].

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

given #141 (A,wt=19): 355 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)).  [back_rewrite(283),rewrite([298(4)])].

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

given #143 (T,wt=15): 746 f(f(f(x,y),z),f(z,f(f(y,z),u))) = z.  [para(519(a,1),470(a,1,2,1)),rewrite([519(10)])].

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

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

given #146 (A,wt=23): 357 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(v,f(x,z)))))) = x.  [back_rewrite(279),rewrite([298(14),298(6),298(14)])].

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

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

given #149 (T,wt=15): 1043 f(f(x,f(y,f(z,x))),f(x,f(z,u))) = x.  [para(421(a,1),330(a,1,1,2,2))].

given #150 (T,wt=15): 1044 f(f(x,f(f(x,y),z)),f(x,f(y,u))) = x.  [para(421(a,1),330(a,1,1,2))].

given #151 (A,wt=17): 358 f(f(x,y),f(x,f(z,f(f(x,y),f(u,y))))) = x.  [back_rewrite(278),rewrite([298(9),298(7),298(13)])].

given #152 (T,wt=15): 1045 f(f(x,f(y,f(x,z))),f(f(z,u),x)) = x.  [para(421(a,1),330(a,1,2))].

given #153 (T,wt=15): 1089 f(f(x,f(y,f(x,f(z,u)))),f(z,x)) = x.  [para(525(a,1),330(a,1,2))].

given #154 (T,wt=15): 1091 f(f(x,f(y,f(x,f(z,u)))),f(u,x)) = x.  [para(531(a,1),330(a,1,2))].

given #155 (T,wt=15): 1168 f(f(x,f(y,f(z,x))),f(x,f(u,z))) = x.  [para(421(a,1),360(a,1,1,2,2))].

given #156 (A,wt=19): 395 f(f(x,x),f(f(y,f(x,x)),f(x,z))) = f(y,f(x,x)).  [para(263(a,1),338(a,1,1))].

given #157 (T,wt=15): 1169 f(f(x,f(f(x,y),z)),f(x,f(u,y))) = x.  [para(421(a,1),360(a,1,1,2))].

given #158 (T,wt=15): 1170 f(f(x,f(y,f(x,z))),f(f(u,z),x)) = x.  [para(421(a,1),360(a,1,2))].

given #159 (T,wt=15): 1394 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x).  [para(330(a,1),429(a,1,2)),flip(a)].

given #160 (T,wt=15): 1418 f(f(x,f(x,y)),f(x,f(f(y,y),z))) = x.  [para(1380(a,1),338(a,1,1))].

given #161 (A,wt=19): 401 f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)).  [para(299(a,1),338(a,1,1))].

Low Water (keep, True_semantics): wt=91

Low Water (keep, True_semantics): wt=69

given #162 (T,wt=15): 1419 f(f(x,f(x,y)),f(x,f(z,f(y,y)))) = x.  [para(1380(a,1),353(a,1,1))].

given #163 (T,wt=15): 1420 f(f(x,f(y,y)),f(x,f(z,f(z,y)))) = x.  [para(1380(a,1),353(a,1,2,2))].

given #164 (T,wt=15): 1421 f(f(x,f(y,z)),f(x,f(y,f(z,z)))) = x.  [para(1380(a,2),353(a,1,2,2))].

given #165 (T,wt=11): 11507 f(x,f(y,f(y,y))) = f(x,x).  [para(1421(a,1),1421(a,1,2)),rewrite([421(2),421(6),353(6),421(3)]),flip(a)].

Low Water (keep, True_semantics): wt=57

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

given #166 (A,wt=19): 404 f(f(x,x),f(f(y,f(x,x)),f(z,x))) = f(y,f(x,x)).  [para(263(a,1),353(a,1,1))].

given #167 (F,wt=19): 12508 f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) != f(c_0,f(c1,f(c2,c3))) # answer("Sheffer").  [back_rewrite(11508),rewrite([11808(11,R)]),flip(a)].

given #168 (T,wt=7): 11683 f(x,f(x,x)) = c_0.  [new_symbol(11548)].

given #169 (T,wt=7): 11777 f(c_0,f(x,x)) = x.  [back_rewrite(11575),rewrite([11683(2)])].

given #170 (T,wt=7): 11778 f(c_0,f(x,c_0)) = x.  [back_rewrite(11574),rewrite([11683(2),11683(3)])].

given #171 (T,wt=7): 11782 f(f(c_0,c_0),x) = c_0.  [back_rewrite(11570),rewrite([11683(2),11683(3),11683(6)])].

given #172 (A,wt=29): 423 f(f(f(x,y),f(z,u)),f(y,f(u,f(f(x,y),f(z,u))))) = f(u,f(f(x,y),f(z,u))).  [para(281(a,1),299(a,1,1)),rewrite([421(7),421(8),421(13)])].

Low Water (keep, True_semantics): wt=53

Low Water (keep, True_semantics): wt=51

given #173 (T,wt=7): 11783 f(c_0,f(c_0,x)) = x.  [back_rewrite(11569),rewrite([11683(2),11683(3)])].

given #174 (T,wt=7): 11787 f(x,f(c_0,c_0)) = c_0.  [back_rewrite(11565),rewrite([11683(2),11683(3),11683(6)])].

given #175 (T,wt=7): 11808 f(c_0,x) = f(x,x).  [back_rewrite(11538),rewrite([11683(2),11683(4),11683(5),11787(6),421(4),11777(4)])].

given #176 (T,wt=7): 11826 f(x,c_0) = f(x,x).  [back_rewrite(11507),rewrite([11683(2)])].

given #177 (A,wt=25): 424 f(f(x,f(y,z)),f(f(z,f(x,f(y,z))),f(u,x))) = f(z,f(x,f(y,z))).  [para(281(a,1),299(a,1,2)),rewrite([421(3),421(8),421(11)])].

given #178 (T,wt=7): 13684 f(x,f(x,c_0)) = c_0.  [para(11683(a,1),381(a,1,2,2)),rewrite([11683(5)])].

given #179 (T,wt=7): 13701 f(x,f(c_0,x)) = c_0.  [para(11777(a,1),338(a,1,2)),rewrite([421(3)])].

given #180 (T,wt=9): 11822 f(f(x,y),f(x,c_0)) = x.  [back_rewrite(11515),rewrite([11683(3)])].

given #181 (T,wt=9): 11823 f(f(x,c_0),f(x,y)) = x.  [back_rewrite(11514),rewrite([11683(2)])].

given #182 (A,wt=29): 425 f(f(f(x,y),f(z,u)),f(x,f(u,f(f(x,y),f(z,u))))) = f(u,f(f(x,y),f(z,u))).  [para(281(a,1),321(a,1,1)),rewrite([421(7),421(8),421(13)])].

Low Water (keep, True_semantics): wt=49

given #183 (T,wt=9): 11824 f(f(x,y),f(y,c_0)) = y.  [back_rewrite(11513),rewrite([11683(3)])].

given #184 (T,wt=9): 11825 f(f(x,c_0),f(y,x)) = x.  [back_rewrite(11510),rewrite([11683(2)])].

given #185 (T,wt=9): 13686 f(f(x,y),f(c_0,x)) = x.  [para(11683(a,1),454(a,1,2,1))].

given #186 (T,wt=9): 13687 f(f(c_0,x),f(x,y)) = x.  [para(11683(a,1),467(a,1,1,1))].

given #187 (A,wt=25): 426 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(281(a,1),321(a,1,2)),rewrite([421(3),421(8),421(11)])].

given #188 (T,wt=9): 13688 f(f(x,y),f(c_0,y)) = y.  [para(11683(a,1),472(a,1,2,1))].

given #189 (T,wt=9): 13703 f(f(c_0,x),f(y,x)) = x.  [para(11777(a,1),472(a,1,2,1))].

given #190 (T,wt=11): 11741 f(x,f(c_0,f(y,f(y,x)))) = c_0.  [back_rewrite(11615),rewrite([11683(4),421(4),11683(7)])].

given #191 (T,wt=11): 11744 f(x,f(c_0,f(y,f(x,y)))) = c_0.  [back_rewrite(11612),rewrite([11683(4),421(4),11683(7)])].

given #192 (A,wt=27): 433 f(f(x,f(f(y,x),f(z,u))),f(u,f(f(y,x),f(z,u)))) = f(f(y,x),f(z,u)).  [para(281(a,1),281(a,1,1,1)),rewrite([421(4),421(8),421(13),421(15),429(15)])].

Low Water (keep, True_semantics): wt=47

Low Water (keep, True_semantics): wt=45

given #193 (T,wt=11): 11761 f(f(x,c_0),y) = f(y,f(x,x)).  [back_rewrite(11594),rewrite([11683(2)])].

given #194 (T,wt=11): 11776 f(f(x,c_0),y) = f(y,f(x,y)).  [back_rewrite(11576),rewrite([11683(2)])].

given #195 (T,wt=11): 11780 f(x,f(y,c_0)) = f(x,f(y,x)).  [back_rewrite(11572),rewrite([11683(2)])].

given #196 (T,wt=11): 11781 f(f(x,c_0),y) = f(y,f(y,x)).  [back_rewrite(11571),rewrite([11683(2)])].

Low Water (keep, True_semantics): wt=39

given #197 (A,wt=27): 443 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)).  [back_rewrite(332),rewrite([421(5),421(8)])].

given #198 (T,wt=11): 11785 f(x,f(x,f(y,c_0))) = f(x,y).  [back_rewrite(11567),rewrite([11683(2)])].

given #199 (T,wt=11): 11786 f(x,f(y,c_0)) = f(x,f(x,y)).  [back_rewrite(11566),rewrite([11683(2)])].

given #200 (T,wt=11): 11788 f(x,f(y,c_0)) = f(x,f(y,y)).  [back_rewrite(11564),rewrite([11683(2)])].

given #201 (T,wt=11): 11800 f(x,f(c_0,f(y,x))) = f(y,x).  [back_rewrite(11549),rewrite([11683(3),421(3)])].

given #202 (A,wt=27): 444 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)).  [back_rewrite(329),rewrite([421(5),421(8)])].

Low Water (keep, True_semantics): wt=37

given #203 (T,wt=11): 11803 f(x,f(c_0,f(x,y))) = f(x,y).  [back_rewrite(11544),rewrite([11683(3),421(3)])].

given #204 (T,wt=11): 11805 f(f(x,x),f(c_0,f(y,x))) = c_0.  [back_rewrite(11541),rewrite([11683(4),421(4),11683(7)])].

given #205 (T,wt=11): 11812 f(f(x,x),f(c_0,f(x,y))) = c_0.  [back_rewrite(11533),rewrite([11683(4),421(4),11683(7)])].

given #206 (T,wt=11): 11814 f(f(x,c_0),y) = f(f(x,x),y).  [back_rewrite(11529),rewrite([11683(2)])].

given #207 (A,wt=25): 446 f(f(x,f(y,z)),f(f(y,f(x,f(y,z))),f(u,x))) = f(y,f(x,f(y,z))).  [back_rewrite(313),rewrite([421(5),421(11)])].

Low Water (keep, True_semantics): wt=35

given #208 (T,wt=11): 11820 f(x,f(f(x,c_0),y)) = f(x,x).  [back_rewrite(11517),rewrite([11683(2)])].

given #209 (T,wt=11): 11821 f(x,f(y,f(x,c_0))) = f(x,x).  [back_rewrite(11516),rewrite([11683(2)])].

given #210 (T,wt=11): 13612 f(x,f(c_0,f(y,f(x,x)))) = c_0.  [para(1415(a,1),404(a,1,2,1)),rewrite([11808(3,R),11777(3),421(2),11683(2),11808(9,R),11777(9),421(7),11683(7)])].

given #211 (T,wt=11): 13689 f(x,f(c_0,f(f(x,x),y))) = c_0.  [para(11683(a,1),399(a,1,2,1)),rewrite([11683(7)])].

given #212 (A,wt=23): 449 f(f(x,f(y,f(x,z))),f(f(y,f(x,z)),f(u,y))) = f(y,f(x,z)).  [back_rewrite(293),rewrite([421(7),421(8)])].

given #213 (T,wt=11): 13697 f(x,f(y,f(c_0,x))) = f(c_0,x).  [para(11683(a,1),545(a,1,2,2,1)),rewrite([11683(6)])].

given #214 (T,wt=11): 13704 f(x,f(f(c_0,x),y)) = f(c_0,x).  [para(11777(a,1),470(a,1,2,2))].

given #215 (T,wt=11): 13710 f(x,f(c_0,f(y,f(x,c_0)))) = c_0.  [para(11777(a,1),325(a,1,1)),rewrite([11777(4),11787(5)])].

given #216 (T,wt=11): 13719 f(x,f(c_0,f(f(x,c_0),y))) = c_0.  [para(11777(a,1),701(a,1,1))].

given #217 (A,wt=17): 468 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x).  [para(453(a,1),338(a,1,1))].

given #218 (T,wt=11): 13720 f(x,f(c_0,f(f(c_0,x),y))) = c_0.  [para(11777(a,1),729(a,1,1))].

given #219 (T,wt=11): 14148 f(f(c_0,x),y) = f(f(x,x),y).  [para(11808(a,2),301(a,2,1)),rewrite([301(6)]),flip(a)].

given #220 (T,wt=11): 14160 f(x,f(c_0,y)) = f(x,f(y,y)).  [para(11808(a,1),429(a,1,2,2,2)),rewrite([169(3)]),flip(a)].

given #221 (T,wt=11): 14161 f(x,f(c_0,y)) = f(x,f(x,y)).  [para(11808(a,2),1380(a,1,2))].

Low Water (keep, True_semantics): wt=33

given #222 (A,wt=17): 469 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x).  [para(453(a,1),353(a,1,1))].

given #223 (T,wt=11): 14162 f(x,f(x,f(c_0,y))) = f(x,y).  [para(11808(a,2),1415(a,1,2,2))].

given #224 (T,wt=11): 14163 f(f(c_0,x),y) = f(y,f(y,x)).  [para(11808(a,2),1422(a,1,1))].

given #225 (T,wt=11): 14164 f(x,f(c_0,y)) = f(x,f(y,x)).  [para(11808(a,2),1423(a,1,2))].

given #226 (T,wt=11): 14165 f(f(c_0,x),y) = f(y,f(x,y)).  [para(11808(a,2),1647(a,1,1))].

Low Water (keep, True_semantics): wt=31

given #227 (A,wt=19): 474 f(f(x,x),f(f(y,f(x,y)),f(x,z))) = f(y,f(x,y)).  [para(427(a,1),453(a,1,1))].

given #228 (T,wt=11): 14175 f(f(x,x),y) = f(y,f(c_0,x)).  [para(11808(a,2),545(a,1,2,2,1)),rewrite([13704(4)]),flip(a)].

given #229 (T,wt=11): 14176 f(f(c_0,x),y) = f(y,f(x,x)).  [para(11808(a,2),545(a,2,1)),rewrite([258(3)]),flip(a)].

given #230 (T,wt=11): 15032 f(f(x,y),f(c_0,f(y,x))) = c_0.  [para(1423(a,2),11741(a,1,2,2,2)),rewrite([1415(5)])].

given #231 (T,wt=11): 16335 f(f(x,x),y) = f(y,f(x,c_0)).  [para(11780(a,2),1647(a,2))].

given #232 (A,wt=19): 475 f(x,f(f(x,f(y,z)),f(f(y,x),u))) = f(x,f(y,z)).  [para(453(a,1),453(a,1,1))].

given #233 (T,wt=11): 20437 f(f(c_0,f(x,y)),f(y,x)) = c_0.  [para(14164(a,1),1421(a,1)),rewrite([14411(9),421(7),338(7)])].

given #234 (T,wt=13): 11923 f(f(x,x),f(y,f(c_0,f(z,x)))) = x.  [back_rewrite(2820),rewrite([11683(3)])].

given #235 (T,wt=13): 13702 f(f(x,y),f(y,x)) = f(c_0,f(x,y)).  [para(291(a,1),11777(a,1,2)),flip(a)].

given #236 (T,wt=13): 14132 f(f(c_0,x),f(f(c_0,f(x,y)),z)) = x.  [para(334(a,1),11783(a,1,2)),rewrite([11783(4)]),flip(a)].

given #237 (A,wt=23): 477 f(f(x,f(f(y,x),z)),f(f(f(y,x),z),f(z,u))) = f(f(y,x),z).  [para(163(a,1),291(a,1,1,2)),rewrite([421(3)])].

given #238 (T,wt=13): 14136 f(f(c_0,x),f(f(c_0,f(y,x)),z)) = x.  [para(340(a,1),11783(a,1,2)),rewrite([11783(4)]),flip(a)].

given #239 (T,wt=13): 14138 f(f(c_0,x),f(y,f(c_0,f(x,z)))) = x.  [para(342(a,1),11783(a,1,2)),rewrite([11783(4)]),flip(a)].

given #240 (T,wt=13): 14143 f(f(c_0,x),f(y,f(c_0,f(z,x)))) = x.  [para(352(a,1),11783(a,1,2)),rewrite([11783(4)]),flip(a)].

given #241 (T,wt=13): 15389 f(f(x,x),f(f(y,x),f(z,x))) = c_0.  [para(433(a,1),11683(a,1,2)),rewrite([421(8),1423(8,R),421(5)])].

given #242 (A,wt=23): 479 f(f(x,f(y,f(z,x))),f(f(y,f(z,x)),f(u,y))) = f(y,f(z,x)).  [para(264(a,1),291(a,1,2,2)),rewrite([421(7),421(8)])].

given #243 (T,wt=13): 18606 f(f(x,c_0),f(f(c_0,f(x,y)),z)) = x.  [para(468(a,1),11783(a,1,2)),rewrite([11778(4)]),flip(a)].

given #244 (T,wt=13): 19835 f(f(x,c_0),f(y,f(c_0,f(x,z)))) = x.  [para(469(a,1),11783(a,1,2)),rewrite([11778(4)]),flip(a)].

given #245 (T,wt=13): 19855 f(f(x,f(c_0,f(y,z))),f(y,c_0)) = y.  [para(469(a,1),11800(a,1,2)),rewrite([19835(14)])].

given #246 (T,wt=13): 19896 f(f(x,c_0),f(y,f(c_0,f(z,x)))) = x.  [para(669(a,1),14162(a,1,2)),rewrite([421(4),11778(4)]),flip(a)].

given #247 (A,wt=23): 482 f(f(x,f(f(x,y),z)),f(f(f(x,y),z),f(z,u))) = f(f(x,y),z).  [para(280(a,1),291(a,1,1,2)),rewrite([421(3)])].

given #248 (T,wt=13): 19906 f(f(x,c_0),f(f(c_0,f(y,x)),z)) = x.  [para(694(a,1),14162(a,1,2)),rewrite([421(4),11778(4)]),flip(a)].

given #249 (T,wt=13): 21248 f(f(x,x),f(y,f(c_0,f(x,z)))) = x.  [para(421(a,1),11923(a,1,2,2,2))].

given #250 (T,wt=13): 21249 f(f(x,x),f(f(c_0,f(y,x)),z)) = x.  [para(421(a,1),11923(a,1,2))].

given #251 (T,wt=13): 21336 f(f(x,x),f(y,f(y,f(z,x)))) = x.  [para(14161(a,1),11923(a,1,2))].

given #252 (A,wt=29): 485 f(f(x,y),f(f(f(x,y),f(z,x)),f(f(f(x,y),f(y,u)),v))) = f(f(x,y),f(z,x)).  [para(291(a,1),338(a,1,1))].

given #253 (T,wt=13): 21344 f(f(x,f(c_0,f(y,z))),f(z,c_0)) = z.  [para(11923(a,1),16335(a,1)),flip(a)].

given #254 (T,wt=13): 21446 f(f(x,x),f(f(c_0,f(x,y)),z)) = x.  [para(14132(a,1),380(a,1,2,2)),rewrite([421(9),1423(10,R),421(6),14132(13)])].

given #255 (T,wt=13): 21503 f(f(c_0,x),f(y,f(y,f(x,z)))) = x.  [para(14163(a,1),14132(a,1,2))].

given #256 (T,wt=13): 21643 f(f(c_0,x),f(y,f(y,f(z,x)))) = x.  [para(14163(a,1),14136(a,1,2))].

given #257 (A,wt=19): 486 f(f(x,f(y,f(x,z))),f(x,f(f(x,f(z,u)),v))) = x.  [para(338(a,1),291(a,1,1,1)),rewrite([338(7),338(12)])].

given #258 (T,wt=13): 21709 f(f(x,x),f(f(x,y),f(z,x))) = c_0.  [para(421(a,1),15389(a,1,2,1))].

given #259 (T,wt=13): 21710 f(f(x,x),f(f(y,x),f(x,z))) = c_0.  [para(421(a,1),15389(a,1,2,2))].

Low Water (keep, True_semantics): wt=29

given #260 (T,wt=13): 21754 f(f(x,c_0),f(f(y,x),f(z,x))) = c_0.  [para(15389(a,1),545(a,1,2,2)),rewrite([421(6),15389(11)])].

given #261 (T,wt=13): 21775 f(f(c_0,x),f(f(y,x),f(z,x))) = c_0.  [para(11808(a,2),15389(a,1,1))].

given #262 (A,wt=29): 487 f(f(x,y),f(f(f(x,y),f(z,x)),f(u,f(f(x,y),f(y,v))))) = f(f(x,y),f(z,x)).  [para(291(a,1),353(a,1,1))].

given #263 (T,wt=13): 21875 f(f(x,c_0),f(y,f(y,f(x,z)))) = x.  [para(14163(a,1),18606(a,1,2))].

given #264 (T,wt=13): 21889 f(f(x,f(x,f(y,z))),f(y,c_0)) = y.  [para(14161(a,1),19855(a,1,1))].

given #265 (T,wt=13): 21899 f(f(x,c_0),f(y,f(y,f(z,x)))) = x.  [para(14161(a,1),19896(a,1,2))].

given #266 (T,wt=13): 21963 f(f(x,x),f(y,f(y,f(x,z)))) = x.  [para(14161(a,1),21248(a,1,2))].

given #267 (A,wt=23): 488 f(f(x,y),f(f(f(x,y),f(z,x)),f(y,u))) = f(f(x,y),f(z,x)).  [para(291(a,1),353(a,1,2)),rewrite([421(7)])].

given #268 (T,wt=13): 21986 f(f(x,f(x,f(y,z))),f(z,z)) = z.  [para(21336(a,1),380(a,1,2,2)),rewrite([421(7),1423(8,R),21336(10)])].

given #269 (T,wt=13): 22106 f(f(x,f(x,f(y,z))),f(c_0,z)) = z.  [para(21336(a,1),11800(a,1,2,2)),rewrite([21336(11)])].

given #270 (T,wt=13): 22118 f(f(x,f(x,f(y,z))),f(z,c_0)) = z.  [para(21336(a,1),16335(a,1)),flip(a)].

given #271 (T,wt=13): 22223 f(f(x,f(x,f(y,z))),f(y,y)) = y.  [para(21503(a,1),380(a,1,2,2)),rewrite([421(7),1423(8,R),21503(11)])].

given #272 (A,wt=19): 489 f(f(x,f(y,f(x,z))),f(x,f(f(x,f(u,z)),v))) = x.  [para(353(a,1),291(a,1,1,1)),rewrite([353(7),353(12)])].

given #273 (T,wt=13): 22224 f(f(x,f(x,f(y,z))),f(c_0,y)) = y.  [para(21503(a,1),421(a,1)),flip(a)].

given #274 (T,wt=13): 22434 f(f(x,x),f(f(x,y),f(x,z))) = c_0.  [para(421(a,1),21709(a,1,2,2))].

given #275 (T,wt=13): 22468 f(f(x,c_0),f(f(x,y),f(z,x))) = c_0.  [para(21709(a,1),545(a,1,2,2)),rewrite([421(6),21709(11)])].

given #276 (T,wt=13): 22490 f(f(c_0,x),f(f(x,y),f(z,x))) = c_0.  [para(11808(a,2),21709(a,1,1))].

given #277 (A,wt=19): 491 f(f(f(x,y),f(y,z)),f(f(x,y),f(u,x))) = f(x,y).  [para(291(a,1),421(a,1)),flip(a)].

given #278 (T,wt=13): 22552 f(f(x,c_0),f(f(y,x),f(x,z))) = c_0.  [para(21710(a,1),545(a,1,2,2)),rewrite([421(6),21710(11)])].

Low Water (keep, True_semantics): wt=27

given #279 (T,wt=13): 22570 f(f(c_0,x),f(f(y,x),f(x,z))) = c_0.  [para(11808(a,2),21710(a,1,1))].

given #280 (T,wt=13): 22941 f(f(x,c_0),f(f(x,y),f(x,z))) = c_0.  [para(22434(a,1),545(a,1,2,2)),rewrite([421(6),22434(11)])].

given #281 (T,wt=13): 22959 f(f(c_0,x),f(f(x,y),f(x,z))) = c_0.  [para(11808(a,2),22434(a,1,1))].

given #282 (A,wt=19): 492 f(f(f(x,y),f(z,y)),f(f(y,x),f(x,u))) = f(y,x).  [para(421(a,1),291(a,1,1,1))].

given #283 (T,wt=15): 1436 f(f(x,f(x,y)),f(f(f(y,y),z),x)) = x.  [para(1380(a,1),454(a,1,1))].

given #284 (T,wt=15): 1442 f(f(f(x,y),z),f(z,f(x,f(y,y)))) = z.  [para(1380(a,2),455(a,1,2,2))].

given #285 (T,wt=15): 1444 f(f(x,f(x,y)),f(f(z,f(y,y)),x)) = x.  [para(1380(a,1),456(a,1,1))].

given #286 (T,wt=15): 1446 f(f(x,f(y,z)),f(f(y,f(z,z)),x)) = x.  [para(1380(a,2),456(a,1,2,1))].

given #287 (A,wt=19): 493 f(f(f(x,y),f(x,z)),f(f(x,y),f(y,u))) = f(x,y).  [para(421(a,1),291(a,1,1,2))].

given #288 (T,wt=15): 1451 f(f(f(x,f(y,y)),z),f(z,f(z,y))) = z.  [para(1380(a,1),466(a,1,2))].

given #289 (T,wt=15): 1452 f(f(f(x,f(y,y)),z),f(z,f(x,y))) = z.  [para(1380(a,2),466(a,1,1,1))].

given #290 (T,wt=15): 1455 f(f(f(f(x,x),y),z),f(z,f(z,x))) = z.  [para(1380(a,1),467(a,1,2))].

given #291 (T,wt=15): 1470 f(f(x,f(y,f(z,z))),f(f(y,z),x)) = x.  [para(1380(a,2),504(a,1,1,2))].

given #292 (A,wt=19): 494 f(f(f(x,y),f(y,z)),f(f(y,z),f(z,u))) = f(y,z).  [para(421(a,1),291(a,1,1))].

given #293 (T,wt=15): 1473 f(f(f(x,x),y),f(f(z,f(z,x)),y)) = y.  [para(1380(a,1),519(a,1,2,1))].

given #294 (T,wt=15): 1476 f(f(f(x,y),z),f(f(x,f(y,y)),z)) = z.  [para(1380(a,2),519(a,1,2,1))].

given #295 (T,wt=15): 1482 f(x,f(f(x,y),f(z,f(z,x)))) = f(x,y).  [para(1380(a,1),307(a,1,2,2)),rewrite([280(3),280(3),280(8)])].

given #296 (T,wt=15): 1541 f(x,f(f(y,x),f(z,f(z,x)))) = f(y,x).  [para(1380(a,1),402(a,1,2,2))].

given #297 (A,wt=19): 495 f(f(f(x,y),f(z,x)),f(f(y,x),f(y,u))) = f(x,y).  [para(421(a,1),291(a,1,2,1))].

given #298 (T,wt=15): 1543 f(x,f(y,f(z,z))) = f(x,f(y,f(y,z))).  [para(1380(a,1),429(a,1,2,2,2)),rewrite([808(6)]),flip(a)].

given #299 (T,wt=15): 1646 f(f(x,f(y,z)),f(x,f(f(z,z),y))) = x.  [para(1422(a,2),353(a,1,2,2))].

given #300 (T,wt=15): 1658 f(f(f(x,y),z),f(z,f(f(y,y),x))) = z.  [para(1422(a,2),455(a,1,2,2))].

given #301 (T,wt=15): 1659 f(f(x,f(y,z)),f(f(f(z,z),y),x)) = x.  [para(1422(a,2),456(a,1,2,1))].

given #302 (A,wt=19): 496 f(f(f(x,y),f(z,x)),f(f(y,u),f(x,y))) = f(x,y).  [para(421(a,1),291(a,1,2))].

given #303 (T,wt=15): 1663 f(f(f(f(x,x),y),z),f(z,f(y,x))) = z.  [para(1422(a,2),466(a,1,1,1))].

given #304 (T,wt=15): 1670 f(f(x,f(f(y,y),z)),f(x,f(x,y))) = x.  [para(1422(a,1),471(a,1,2))].

given #305 (T,wt=15): 1681 f(f(x,f(y,f(z,z))),f(x,f(x,z))) = x.  [para(1422(a,1),504(a,1,2))].

given #306 (T,wt=15): 1682 f(f(x,f(f(y,y),z)),f(f(z,y),x)) = x.  [para(1422(a,2),504(a,1,1,2))].

given #307 (A,wt=31): 499 f(f(f(x,x),f(f(y,f(x,y)),z)),f(f(f(y,f(x,y)),z),f(z,u))) = f(f(y,f(x,y)),z).  [para(427(a,1),291(a,1,1,2)),rewrite([421(5)])].

given #308 (T,wt=15): 1686 f(f(f(x,y),z),f(f(f(y,y),x),z)) = z.  [para(1422(a,2),519(a,1,2,1))].

given #309 (T,wt=15): 1740 f(x,f(f(y,y),z)) = f(x,f(z,f(z,y))).  [para(1422(a,1),429(a,1,2,2,2)),rewrite([441(5)]),flip(a)].

given #310 (T,wt=15): 1812 f(x,f(f(x,y),f(z,f(x,z)))) = f(x,y).  [para(1423(a,1),307(a,1,2,2)),rewrite([280(3),280(3),280(8)])].

Low Water (keep, True_semantics): wt=25

given #311 (T,wt=15): 1881 f(x,f(f(y,x),f(z,f(x,z)))) = f(y,x).  [para(1423(a,1),402(a,1,2,2))].

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

given #312 (A,wt=29): 500 f(f(x,y),f(f(f(x,y),f(y,z)),f(f(f(x,y),f(u,x)),v))) = f(f(x,y),f(y,z)).  [para(291(a,1),453(a,1,1))].

given #313 (T,wt=15): 1884 f(x,f(y,f(z,z))) = f(x,f(y,f(z,y))).  [para(1423(a,1),429(a,1,2,2,2)),rewrite([801(6)]),flip(a)].

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

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

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

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

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

given #314 (T,wt=15): 1898 f(f(x,f(f(y,y),z)),f(x,f(z,y))) = x.  [para(1547(a,1),353(a,1,2,2))].

given #315 (T,wt=15): 1907 f(f(f(f(x,x),y),z),f(f(y,x),z)) = z.  [para(1547(a,1),519(a,1,2,1))].

given #316 (T,wt=15): 2037 f(x,f(f(y,y),z)) = f(x,f(z,f(y,z))).  [para(1647(a,1),429(a,1,2,2,2)),rewrite([441(5)]),flip(a)].

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

given #317 (A,wt=19): 501 f(f(x,f(y,f(z,x))),f(x,f(f(x,f(z,u)),v))) = x.  [para(453(a,1),291(a,1,1,1)),rewrite([453(7),453(12)])].

given #318 (T,wt=15): 2427 f(f(x,f(y,f(z,y))),f(x,f(x,z))) = x.  [para(1380(a,1),461(a,1,2))].

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

given #319 (T,wt=15): 2530 f(x,f(f(y,f(y,x)),f(z,x))) = f(z,x).  [para(1422(a,1),503(a,1,2,1))].

given #320 (T,wt=15): 2532 f(x,f(f(y,f(x,y)),f(z,x))) = f(z,x).  [para(1647(a,1),503(a,1,2,1))].

given #321 (T,wt=15): 2563 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z).  [para(1422(a,1),505(a,1,2,1))].

given #322 (A,wt=31): 502 f(f(f(x,y),f(z,f(f(x,y),f(u,x)))),f(f(x,y),f(f(f(x,y),f(y,v)),w))) = f(x,y).  [para(291(a,1),291(a,1,1,1)),rewrite([291(13),291(20)])].

given #323 (T,wt=15): 2565 f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z).  [para(1647(a,1),505(a,1,2,1))].

given #324 (T,wt=15): 2642 f(f(f(x,f(y,x)),z),f(z,f(z,y))) = z.  [para(1380(a,1),522(a,1,2))].

given #325 (T,wt=15): 2946 f(x,f(f(y,y),f(f(y,z),x))) = f(x,x).  [para(545(a,1),427(a,1,2,2)),rewrite([421(6),1423(6,R),421(4)])].

given #326 (T,wt=15): 2976 f(f(x,f(y,y)),z) = f(f(x,f(x,y)),z).  [para(1380(a,1),545(a,1,2,2,1)),rewrite([545(5)]),flip(a)].

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

given #327 (A,wt=17): 506 f(x,f(f(x,y),f(f(f(y,z),x),u))) = f(x,y).  [para(454(a,1),338(a,1,1))].

given #328 (T,wt=15): 2979 f(f(f(x,x),y),z) = f(f(y,f(y,x)),z).  [para(1422(a,1),545(a,1,2,2,1)),rewrite([765(6)]),flip(a)].

given #329 (T,wt=15): 2981 f(f(x,f(y,y)),z) = f(f(x,f(y,x)),z).  [para(1423(a,1),545(a,1,2,2,1)),rewrite([545(5)]),flip(a)].

given #330 (T,wt=15): 2986 f(f(f(x,x),y),z) = f(f(y,f(x,y)),z).  [para(1647(a,1),545(a,1,2,2,1)),rewrite([758(6)]),flip(a)].

given #331 (T,wt=15): 3008 f(x,f(f(y,y),f(f(z,y),x))) = f(x,x).  [para(549(a,1),427(a,1,2,2)),rewrite([421(6),1423(6,R),421(4)])].

given #332 (A,wt=17): 507 f(x,f(f(x,y),f(z,f(f(y,u),x)))) = f(x,y).  [para(454(a,1),353(a,1,1))].

given #333 (T,wt=15): 3218 f(f(x,f(y,f(y,z))),f(x,f(x,z))) = x.  [para(1380(a,1),554(a,1,2))].

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

given #334 (T,wt=15): 3223 f(f(x,f(y,f(y,z))),f(x,f(z,x))) = x.  [para(1423(a,1),554(a,1,2))].

given #335 (T,wt=15): 3312 f(f(f(x,f(x,y)),z),f(z,f(z,y))) = z.  [para(1380(a,1),565(a,1,2))].

Low Water (keep, True_semantics): wt=23

given #336 (T,wt=15): 3321 f(f(f(x,f(x,y)),z),f(z,f(y,z))) = z.  [para(1423(a,1),565(a,1,2))].

given #337 (A,wt=19): 512 f(x,f(f(f(y,z),x),f(f(x,y),u))) = f(f(y,z),x).  [para(454(a,1),453(a,1,1))].

given #338 (T,wt=15): 3514 f(f(x,f(x,y)),f(x,f(z,f(y,z)))) = x.  [para(1422(a,1),581(a,1,1))].

given #339 (T,wt=15): 3749 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x.  [para(1422(a,1),586(a,1,1))].

given #340 (T,wt=15): 3755 f(f(x,f(y,x)),f(x,f(z,f(z,y)))) = x.  [para(1647(a,1),586(a,1,1))].

given #341 (T,wt=15): 3822 f(f(x,f(x,y)),f(f(z,f(y,z)),x)) = x.  [para(1380(a,1),636(a,1,1))].

given #342 (A,wt=19): 514 f(f(x,f(y,f(x,z))),f(x,f(f(f(z,u),x),v))) = x.  [para(454(a,1),291(a,1,1,1)),rewrite([454(7),454(12)])].

given #343 (T,wt=15): 3888 f(f(x,f(x,y)),f(f(z,f(z,y)),x)) = x.  [para(1380(a,1),639(a,1,1))].

given #344 (T,wt=15): 3894 f(f(x,f(y,x)),f(f(z,f(z,y)),x)) = x.  [para(1423(a,1),639(a,1,1))].

given #345 (T,wt=15): 5288 f(f(x,f(y,f(z,x))),f(f(z,u),x)) = x.  [para(676(a,1),549(a,1,2,2)),rewrite([676(12)])].

given #346 (T,wt=15): 5732 f(f(x,f(y,f(z,x))),f(f(u,z),x)) = x.  [para(681(a,1),549(a,1,2,2)),rewrite([681(12)])].

given #347 (A,wt=29): 515 f(f(x,y),f(f(f(f(x,y),f(y,z)),u),f(f(x,y),f(v,x)))) = f(f(x,y),f(v,x)).  [para(291(a,1),454(a,1,1))].

given #348 (T,wt=15): 6998 f(f(x,f(f(x,y),z)),f(f(u,y),x)) = x.  [para(699(a,1),421(a,1)),flip(a)].

given #349 (T,wt=15): 7211 f(f(x,f(f(x,y),z)),f(f(y,u),x)) = x.  [para(700(a,1),421(a,1)),flip(a)].

given #350 (T,wt=15): 7413 f(f(x,f(f(y,x),z)),f(x,f(y,u))) = x.  [para(701(a,1),421(a,1)),flip(a)].

given #351 (T,wt=15): 7503 f(f(x,f(f(y,x),z)),f(f(y,u),x)) = x.  [para(701(a,1),549(a,1,2,2)),rewrite([701(12)])].

given #352 (A,wt=17): 516 f(x,f(f(y,x),f(f(x,f(z,y)),u))) = f(y,x).  [para(455(a,1),338(a,1,1))].

given #353 (T,wt=15): 7868 f(f(x,f(f(y,x),z)),f(x,f(u,y))) = x.  [para(706(a,1),421(a,1)),flip(a)].

given #354 (T,wt=15): 7957 f(f(x,f(f(y,x),z)),f(f(u,y),x)) = x.  [para(706(a,1),549(a,1,2,2)),rewrite([706(12)])].

given #355 (T,wt=15): 9584 f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x).  [para(1043(a,1),429(a,1,2)),flip(a)].

given #356 (T,wt=15): 9704 f(x,f(y,f(x,f(f(x,y),z)))) = f(x,x).  [para(1044(a,1),429(a,1,2)),flip(a)].

given #357 (A,wt=17): 517 f(x,f(f(y,x),f(z,f(x,f(u,y))))) = f(y,x).  [para(455(a,1),353(a,1,1))].

given #358 (T,wt=15): 10652 f(x,f(y,f(z,f(y,x)))) = f(x,f(y,y)).  [para(1394(a,1),441(a,1,2)),flip(a)].

given #359 (T,wt=15): 11685 f(f(x,f(y,z)),f(x,f(y,f(z,c_0)))) = x.  [back_rewrite(11680),rewrite([11683(4)])].

given #360 (T,wt=15): 11687 f(f(x,f(y,c_0)),f(x,f(z,f(z,y)))) = x.  [back_rewrite(11678),rewrite([11683(2)])].

given #361 (T,wt=15): 11688 f(f(x,f(x,y)),f(x,f(z,f(y,c_0)))) = x.  [back_rewrite(11677),rewrite([11683(4)])].

given #362 (A,wt=19): 521 f(f(x,x),f(f(y,f(x,y)),f(z,x))) = f(y,f(x,y)).  [para(427(a,1),455(a,1,1))].

given #363 (T,wt=15): 11690 f(f(x,f(x,y)),f(x,f(f(y,c_0),z))) = x.  [back_rewrite(11675),rewrite([11683(4)])].

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

given #364 (T,wt=15): 11717 f(f(x,x),f(c_0,f(f(c_0,f(y,x)),z))) = c_0.  [back_rewrite(11647),rewrite([11683(3),11683(5),421(5),11683(10)])].

given #365 (T,wt=15): 11720 f(f(x,x),f(c_0,f(f(c_0,f(x,y)),z))) = c_0.  [back_rewrite(11643),rewrite([11683(3),11683(5),421(5),11683(10)])].

given #366 (T,wt=15): 11729 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0.  [back_rewrite(11631),rewrite([11683(3),11683(5),421(5),11683(10)])].

given #367 (A,wt=19): 523 f(x,f(f(x,f(y,z)),f(f(z,x),u))) = f(x,f(y,z)).  [para(455(a,1),453(a,1,1))].

given #368 (T,wt=15): 11732 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0.  [back_rewrite(11627),rewrite([11683(3),11683(5),421(5),11683(10)])].

given #369 (T,wt=15): 11740 f(f(f(x,f(x,y)),z),f(f(y,c_0),z)) = z.  [back_rewrite(11616),rewrite([11683(5)])].

given #370 (T,wt=15): 11745 f(f(x,f(y,c_0)),f(f(z,f(z,y)),x)) = x.  [back_rewrite(11611),rewrite([11683(2)])].

given #371 (T,wt=15): 11751 f(f(f(x,c_0),y),f(y,f(z,f(z,x)))) = y.  [back_rewrite(11605),rewrite([11683(2)])].

given #372 (A,wt=19): 524 f(x,f(f(x,f(y,z)),f(u,f(y,x)))) = f(x,f(y,z)).  [para(453(a,1),455(a,1,1))].

given #373 (T,wt=15): 11756 f(f(x,f(y,f(y,z))),f(f(z,c_0),x)) = x.  [back_rewrite(11600),rewrite([11683(5)])].

given #374 (T,wt=15): 11758 f(f(f(x,f(x,y)),z),f(z,f(y,c_0))) = z.  [back_rewrite(11597),rewrite([11683(5)])].

given #375 (T,wt=15): 11759 f(f(x,f(y,f(y,z))),f(x,f(z,c_0))) = x.  [back_rewrite(11596),rewrite([11683(5)])].

given #376 (T,wt=15): 11765 f(x,f(f(y,f(x,c_0)),f(x,z))) = f(x,z).  [back_rewrite(11589),rewrite([11683(2)])].

given #377 (A,wt=19): 526 f(f(x,f(y,f(z,x))),f(x,f(f(x,f(u,z)),v))) = x.  [para(455(a,1),291(a,1,1,1)),rewrite([455(7),455(12)])].

given #378 (T,wt=15): 11766 f(x,f(f(y,f(x,c_0)),f(z,x))) = f(z,x).  [back_rewrite(11588),rewrite([11683(2)])].

given #379 (T,wt=15): 11770 f(x,f(f(f(x,c_0),y),f(x,z))) = f(x,z).  [back_rewrite(11584),rewrite([11683(2)])].

given #380 (T,wt=15): 11771 f(x,f(f(f(x,c_0),y),f(z,x))) = f(z,x).  [back_rewrite(11583),rewrite([11683(2)])].

given #381 (T,wt=15): 11790 f(x,f(f(y,x),f(z,f(x,c_0)))) = f(y,x).  [back_rewrite(11562),rewrite([11683(3)])].

given #382 (A,wt=29): 527 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,f(f(x,y),f(v,x))))) = f(f(x,y),f(y,z)).  [para(291(a,1),455(a,1,1))].

given #383 (T,wt=15): 11792 f(x,f(f(y,x),f(f(x,c_0),z))) = f(y,x).  [back_rewrite(11559),rewrite([11683(3)])].

given #384 (T,wt=15): 11795 f(x,f(f(x,y),f(z,f(x,c_0)))) = f(x,y).  [back_rewrite(11554),rewrite([11683(3)])].

given #385 (T,wt=15): 11796 f(x,f(f(x,y),f(f(x,c_0),z))) = f(x,y).  [back_rewrite(11553),rewrite([11683(3)])].

given #386 (T,wt=15): 11857 f(x,f(f(y,f(x,x)),f(z,f(x,x)))) = c_0.  [back_rewrite(10664),rewrite([11683(8)])].

given #387 (A,wt=23): 528 f(f(x,y),f(f(y,z),f(f(x,y),f(u,x)))) = f(f(x,y),f(u,x)).  [para(291(a,1),455(a,1,2)),rewrite([421(7)])].

given #388 (T,wt=15): 11858 f(x,f(f(f(x,x),y),f(z,f(x,x)))) = c_0.  [back_rewrite(10659),rewrite([11683(8)])].

given #389 (T,wt=15): 11897 f(x,f(f(c_0,f(y,f(x,x))),z)) = f(x,x).  [back_rewrite(3692),rewrite([11683(2)])].

given #390 (T,wt=15): 11921 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,x).  [back_rewrite(2843),rewrite([11683(2)])].

given #391 (T,wt=15): 11922 f(x,f(y,f(c_0,f(f(x,x),z)))) = f(x,x).  [back_rewrite(2828),rewrite([11683(2)])].

given #392 (A,wt=19): 529 f(x,f(f(f(y,z),x),f(u,f(x,y)))) = f(f(y,z),x).  [para(454(a,1),455(a,1,1))].

given #393 (T,wt=15): 12035 f(f(f(x,x),y),f(c_0,f(z,x))) = f(z,x).  [back_rewrite(2839),rewrite([11780(7,R),421(5)])].

given #394 (T,wt=15): 12037 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y).  [back_rewrite(2707),rewrite([11780(7,R),421(5)])].

given #395 (T,wt=15): 12044 f(f(f(x,x),y),f(c_0,f(x,z))) = f(x,z).  [back_rewrite(2564),rewrite([11780(7,R),421(5)])].

given #396 (T,wt=15): 12045 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z).  [back_rewrite(2531),rewrite([11780(7,R),421(5)])].

given #397 (A,wt=19): 530 f(x,f(f(x,f(y,z)),f(u,f(z,x)))) = f(x,f(y,z)).  [para(455(a,1),455(a,1,1))].

given #398 (T,wt=15): 12055 f(f(x,x),f(y,c_0)) = f(f(y,y),f(x,c_0)).  [back_rewrite(2047),rewrite([11780(4,R),11780(8,R)])].

given #399 (T,wt=15): 12056 f(f(x,y),f(z,c_0)) = f(f(z,z),f(x,y)).  [back_rewrite(2039),rewrite([11780(4,R)])].

given #400 (T,wt=15): 12087 f(x,f(f(y,x),f(c_0,f(z,y)))) = f(x,x).  [back_rewrite(912),rewrite([11780(5,R),421(4)])].

given #401 (T,wt=15): 12088 f(x,f(f(y,x),f(c_0,f(y,z)))) = f(x,x).  [back_rewrite(886),rewrite([11780(5,R),421(4)])].

given #402 (A,wt=17): 534 f(x,f(f(x,y),f(f(f(z,y),x),u))) = f(x,y).  [para(456(a,1),338(a,1,1))].

given #403 (T,wt=15): 12089 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x).  [back_rewrite(800),rewrite([11780(5,R),421(4)])].

given #404 (T,wt=15): 12090 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x).  [back_rewrite(781),rewrite([11780(5,R),421(4)])].

given #405 (T,wt=15): 12343 f(f(x,f(c_0,f(y,z))),f(f(z,y),x)) = x.  [back_rewrite(3896),rewrite([11808(3,R)])].

given #406 (T,wt=15): 12388 f(f(f(x,y),z),f(z,f(c_0,f(y,x)))) = z.  [back_rewrite(3322),rewrite([11808(5,R)])].

given #407 (A,wt=17): 535 f(x,f(f(x,y),f(z,f(f(u,y),x)))) = f(x,y).  [para(456(a,1),353(a,1,1))].

given #408 (T,wt=15): 12831 f(f(f(x,y),z),f(f(c_0,f(y,x)),z)) = z.  [back_rewrite(4227),rewrite([11808(5,R)])].

given #409 (T,wt=15): 12870 f(f(f(c_0,f(x,y)),z),f(z,f(y,x))) = z.  [back_rewrite(3753),rewrite([11808(3,R)])].

given #410 (T,wt=15): 12909 f(f(x,f(y,z)),f(f(c_0,f(z,y)),x)) = x.  [back_rewrite(3424),rewrite([11808(5,R)])].

given #411 (T,wt=15): 13706 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0.  [para(11777(a,1),359(a,1,1))].

given #412 (A,wt=19): 540 f(x,f(f(f(y,z),x),f(f(x,z),u))) = f(f(y,z),x).  [para(456(a,1),453(a,1,1))].

given #413 (T,wt=15): 13708 f(x,f(c_0,f(f(c_0,f(y,f(x,x))),z))) = c_0.  [para(11777(a,1),442(a,1,1))].

given #414 (T,wt=15): 13709 f(x,f(c_0,f(y,f(c_0,f(f(x,x),z))))) = c_0.  [para(11777(a,1),445(a,1,1))].

given #415 (T,wt=15): 13717 f(x,f(c_0,f(f(c_0,f(f(x,x),y)),z))) = c_0.  [para(11777(a,1),686(a,1,1))].

given #416 (T,wt=15): 13954 f(x,f(c_0,f(y,f(c_0,f(z,f(x,c_0)))))) = c_0.  [para(11778(a,1),359(a,1,1))].

given #417 (A,wt=17): 541 f(x,f(f(y,f(x,f(z,u))),f(z,x))) = f(z,x).  [para(453(a,1),456(a,1,1))].

given #418 (T,wt=15): 13958 f(x,f(c_0,f(f(c_0,f(y,f(x,c_0))),z))) = c_0.  [para(11778(a,1),442(a,1,1))].

given #419 (T,wt=15): 13959 f(x,f(c_0,f(y,f(c_0,f(f(x,c_0),z))))) = c_0.  [para(11778(a,1),445(a,1,1))].

given #420 (T,wt=15): 13965 f(x,f(c_0,f(f(c_0,f(f(x,c_0),y)),z))) = c_0.  [para(11778(a,1),686(a,1,1))].

given #421 (T,wt=15): 14128 f(x,f(c_0,f(y,f(c_0,f(z,f(c_0,x)))))) = c_0.  [para(11783(a,1),359(a,1,1))].

given #422 (A,wt=19): 542 f(f(x,f(y,f(x,z))),f(x,f(f(f(u,z),x),v))) = x.  [para(456(a,1),291(a,1,1,1)),rewrite([456(7),456(12)])].

given #423 (T,wt=15): 14129 f(x,f(c_0,f(f(c_0,f(y,f(c_0,x))),z))) = c_0.  [para(11783(a,1),442(a,1,1))].

given #424 (T,wt=15): 14130 f(x,f(c_0,f(y,f(c_0,f(f(c_0,x),z))))) = c_0.  [para(11783(a,1),445(a,1,1))].

given #425 (T,wt=15): 14133 f(f(c_0,f(x,y)),f(f(c_0,x),z)) = f(x,y).  [para(336(a,1),11783(a,1,2)),rewrite([11783(5)]),flip(a)].

given #426 (T,wt=15): 14139 f(x,f(c_0,f(f(c_0,f(f(c_0,x),y)),z))) = c_0.  [para(11783(a,1),686(a,1,1))].

given #427 (A,wt=29): 543 f(f(x,y),f(f(z,f(f(x,y),f(y,u))),f(f(x,y),f(v,x)))) = f(f(x,y),f(v,x)).  [para(291(a,1),456(a,1,1))].

given #428 (T,wt=15): 14140 f(f(c_0,f(x,y)),f(z,f(c_0,x))) = f(x,y).  [para(348(a,1),11783(a,1,2)),rewrite([11783(5)]),flip(a)].

given #429 (T,wt=15): 14144 f(f(c_0,f(x,y)),f(z,f(c_0,y))) = f(x,y).  [para(355(a,1),11783(a,1,2)),rewrite([11783(5)]),flip(a)].

given #430 (T,wt=15): 14145 f(f(c_0,f(x,y)),f(f(c_0,y),z)) = f(x,y).  [para(401(a,1),11783(a,1,2)),rewrite([11783(5)]),flip(a)].

given #431 (T,wt=15): 14155 f(x,f(f(x,y),f(f(c_0,x),z))) = f(x,y).  [para(11808(a,2),322(a,1,2,2,1))].

given #432 (A,wt=17): 544 f(x,f(f(y,f(f(z,u),x)),f(x,z))) = f(x,z).  [para(454(a,1),456(a,1,1))].

given #433 (T,wt=15): 14156 f(x,f(f(x,y),f(z,f(c_0,x)))) = f(x,y).  [para(11808(a,2),327(a,1,2,2,2))].

given #434 (T,wt=15): 14157 f(x,f(f(y,x),f(f(c_0,x),z))) = f(y,x).  [para(11808(a,2),392(a,1,2,2,1))].

given #435 (T,wt=15): 14159 f(x,f(f(y,x),f(z,f(c_0,x)))) = f(y,x).  [para(11808(a,2),402(a,1,2,2,2))].

given #436 (T,wt=15): 14167 f(f(x,f(y,f(z,y))),f(x,f(c_0,z))) = x.  [para(11808(a,2),461(a,1,2,2))].

given #437 (A,wt=19): 546 f(x,f(f(f(y,z),x),f(u,f(x,z)))) = f(f(y,z),x).  [para(456(a,1),455(a,1,1))].

given #438 (T,wt=15): 14169 f(x,f(f(f(c_0,x),y),f(z,x))) = f(z,x).  [para(11808(a,2),503(a,1,2,1,1))].

given #439 (T,wt=15): 14170 f(x,f(f(f(c_0,x),y),f(x,z))) = f(x,z).  [para(11808(a,2),505(a,1,2,1,1))].

given #440 (T,wt=15): 14171 f(f(f(x,f(y,x)),z),f(z,f(c_0,y))) = z.  [para(11808(a,2),522(a,1,2,2))].

given #441 (T,wt=15): 14172 f(x,f(f(y,f(c_0,x)),f(z,x))) = f(z,x).  [para(11808(a,2),532(a,1,2,1,2))].

given #442 (A,wt=17): 547 f(x,f(f(y,f(x,f(z,u))),f(u,x))) = f(u,x).  [para(455(a,1),456(a,1,1))].

given #443 (T,wt=15): 14173 f(x,f(f(y,f(c_0,x)),f(x,z))) = f(x,z).  [para(11808(a,2),533(a,1,2,1,2))].

given #444 (T,wt=15): 14174 f(f(x,f(y,f(z,y))),f(f(c_0,z),x)) = x.  [para(11808(a,2),538(a,1,2,1))].

given #445 (T,wt=15): 14178 f(f(x,f(y,f(y,z))),f(x,f(c_0,z))) = x.  [para(11808(a,2),554(a,1,2,2))].

given #446 (T,wt=15): 14179 f(f(f(x,f(x,y)),z),f(z,f(c_0,y))) = z.  [para(11808(a,2),565(a,1,2,2))].

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

given #448 (T,wt=15): 14180 f(f(x,f(y,f(y,z))),f(f(c_0,z),x)) = x.  [para(11808(a,2),567(a,1,2,1))].

given #449 (T,wt=15): 14181 f(f(f(c_0,x),y),f(y,f(z,f(x,z)))) = y.  [para(11808(a,2),581(a,1,1,1))].

given #450 (T,wt=15): 14182 f(f(f(c_0,x),y),f(y,f(z,f(z,x)))) = y.  [para(11808(a,2),586(a,1,1,1))].

given #451 (T,wt=15): 14183 f(f(x,f(c_0,y)),f(f(z,f(y,z)),x)) = x.  [para(11808(a,2),636(a,1,1,2))].

given #452 (A,wt=19): 558 f(f(x,x),f(f(y,f(y,x)),f(x,z))) = f(y,f(y,x)).  [para(464(a,1),453(a,1,1))].

given #453 (T,wt=15): 14184 f(f(x,f(c_0,y)),f(f(z,f(z,y)),x)) = x.  [para(11808(a,2),639(a,1,1,2))].

given #454 (T,wt=15): 14185 f(f(f(x,f(y,x)),z),f(f(c_0,y),z)) = z.  [para(11808(a,2),648(a,1,2,1))].

given #455 (T,wt=15): 14186 f(f(f(x,f(x,y)),z),f(f(c_0,y),z)) = z.  [para(11808(a,2),656(a,1,2,1))].

given #456 (T,wt=15): 14200 f(f(x,f(c_0,y)),f(x,f(z,f(z,y)))) = x.  [para(11808(a,2),1420(a,1,1,2))].

given #457 (A,wt=31): 560 f(f(f(x,x),f(f(y,f(y,x)),z)),f(f(f(y,f(y,x)),z),f(z,u))) = f(f(y,f(y,x)),z).  [para(464(a,1),291(a,1,1,2)),rewrite([421(5)])].

given #458 (T,wt=15): 14219 f(f(x,x),f(c_0,y)) = f(f(y,y),f(x,c_0)).  [back_rewrite(12074),rewrite([14161(4,R)])].

given #459 (T,wt=15): 14419 f(f(x,x),f(c_0,y)) = f(f(y,y),f(c_0,x)).  [back_rewrite(1744),rewrite([14161(4,R),14161(8,R)])].

given #460 (T,wt=15): 14420 f(f(x,y),f(c_0,z)) = f(f(z,z),f(x,y)).  [back_rewrite(1742),rewrite([14161(4,R)])].

given #461 (T,wt=15): 14980 f(f(x,f(y,z)),f(c_0,f(x,f(y,x)))) = c_0.  [para(453(a,1),11741(a,1,2,2,2)),rewrite([421(5)])].

given #462 (A,wt=19): 564 f(f(x,x),f(f(y,f(y,x)),f(z,x))) = f(y,f(y,x)).  [para(464(a,1),455(a,1,1))].

given #463 (T,wt=15): 14984 f(f(f(x,y),z),f(c_0,f(z,f(z,x)))) = c_0.  [para(454(a,1),11741(a,1,2,2,2)),rewrite([421(5)])].

given #464 (T,wt=15): 14986 f(f(x,f(y,z)),f(c_0,f(x,f(z,x)))) = c_0.  [para(455(a,1),11741(a,1,2,2,2)),rewrite([421(5)])].

given #465 (T,wt=15): 14988 f(f(f(x,y),z),f(c_0,f(z,f(z,y)))) = c_0.  [para(456(a,1),11741(a,1,2,2,2)),rewrite([421(5)])].

given #466 (T,wt=15): 14991 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0.  [para(466(a,1),11741(a,1,2,2,2)),rewrite([421(5),14164(5,R)])].

given #467 (A,wt=25): 572 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(301(a,1),338(a,1,1))].

given #468 (T,wt=15): 14992 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0.  [para(467(a,1),11741(a,1,2,2,2)),rewrite([421(5),14164(5,R)])].

given #469 (T,wt=15): 14993 f(f(x,y),f(c_0,f(y,f(y,f(x,z))))) = c_0.  [para(471(a,1),11741(a,1,2,2,2)),rewrite([421(5)])].

given #470 (T,wt=15): 14995 f(f(f(x,y),z),f(c_0,f(z,f(x,z)))) = c_0.  [para(472(a,1),11741(a,1,2,2,2)),rewrite([421(5)])].

given #471 (T,wt=15): 14997 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0.  [para(504(a,1),11741(a,1,2,2,2)),rewrite([421(5)])].

given #472 (A,wt=25): 573 f(f(f(x,x),y),f(f(x,x),f(z,f(f(f(x,x),y),f(x,u))))) = f(x,x).  [para(301(a,1),353(a,1,1))].

given #473 (T,wt=15): 14999 f(f(f(x,y),z),f(c_0,f(z,f(y,z)))) = c_0.  [para(519(a,1),11741(a,1,2,2,2)),rewrite([421(5)])].

given #474 (T,wt=15): 15000 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0.  [para(11741(a,1),356(a,1,2,1)),rewrite([11741(13)])].

given #475 (T,wt=15): 15057 f(f(x,f(y,f(z,y))),f(c_0,f(x,z))) = c_0.  [para(581(a,1),11741(a,1,2,2,2)),rewrite([421(7),14164(7,R),11777(7)])].

given #476 (T,wt=15): 15060 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0.  [para(586(a,1),11741(a,1,2,2,2)),rewrite([421(7),14164(7,R),11777(7)])].

given #477 (A,wt=19): 574 f(f(x,x),f(f(x,y),f(f(x,x),z))) = f(f(x,x),z).  [para(421(a,1),301(a,1,2))].

given #478 (T,wt=15): 15061 f(f(f(x,f(y,x)),z),f(c_0,f(z,y))) = c_0.  [para(636(a,1),11741(a,1,2,2,2)),rewrite([421(7),1415(7)])].

given #479 (T,wt=15): 15062 f(f(f(x,f(x,y)),z),f(c_0,f(z,y))) = c_0.  [para(639(a,1),11741(a,1,2,2,2)),rewrite([421(7),1415(7)])].

given #480 (T,wt=15): 15067 f(f(f(x,c_0),y),f(f(z,f(z,x)),y)) = y.  [para(11741(a,1),656(a,1,1,1,2)),rewrite([11808(12,R),11783(9)])].

given #481 (T,wt=15): 15157 f(f(x,f(f(y,y),z)),f(c_0,f(x,y))) = c_0.  [para(1418(a,1),11741(a,1,2,2,2)),rewrite([421(7),381(7)])].

given #482 (A,wt=31): 576 f(f(f(x,x),y),f(f(f(f(x,x),y),f(x,z)),f(f(x,x),u))) = f(f(f(x,x),y),f(x,z)).  [para(301(a,1),453(a,1,1))].

given #483 (T,wt=15): 15160 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0.  [para(1419(a,1),11741(a,1,2,2,2)),rewrite([421(7),381(7)])].

given #484 (T,wt=15): 15167 f(f(x,y),f(c_0,f(x,f(x,f(y,z))))) = c_0.  [para(338(a,1),11744(a,1,2,2,2)),rewrite([421(5)])].

given #485 (T,wt=15): 15168 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0.  [para(353(a,1),11744(a,1,2,2,2)),rewrite([421(5)])].

given #486 (T,wt=15): 15175 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0.  [para(472(a,1),11744(a,1,2,2,2)),rewrite([421(5),14164(5,R)])].

given #487 (A,wt=31): 579 f(f(f(x,x),y),f(f(f(f(x,x),y),f(x,z)),f(u,f(x,x)))) = f(f(f(x,x),y),f(x,z)).  [para(301(a,1),455(a,1,1))].

given #488 (T,wt=15): 15178 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0.  [para(519(a,1),11744(a,1,2,2,2)),rewrite([421(5),14164(5,R)])].

given #489 (T,wt=15): 15179 f(x,f(c_0,f(y,f(c_0,f(z,f(x,z)))))) = c_0.  [para(11744(a,1),356(a,1,2,1)),rewrite([11744(13)])].

given #490 (T,wt=15): 15180 f(x,f(c_0,f(f(x,y),f(c_0,f(z,y))))) = c_0.  [para(356(a,1),11744(a,1,2,2,2)),rewrite([421(6),14161(6,R)])].

given #491 (T,wt=15): 15182 f(x,f(c_0,f(f(x,y),f(c_0,f(y,z))))) = c_0.  [para(399(a,1),11744(a,1,2,2,2)),rewrite([421(6),14161(6,R)])].

given #492 (A,wt=19): 583 f(f(x,f(y,f(f(z,u),x))),f(x,f(f(x,u),v))) = x.  [para(466(a,1),291(a,1,1,1)),rewrite([466(8),466(12)])].

given #493 (T,wt=15): 15184 f(x,f(c_0,f(f(y,x),f(c_0,f(y,z))))) = c_0.  [para(470(a,1),11744(a,1,2,2,2)),rewrite([421(6),14161(6,R)])].

given #494 (T,wt=15): 15186 f(x,f(c_0,f(f(y,x),f(c_0,f(z,y))))) = c_0.  [para(480(a,1),11744(a,1,2,2,2)),rewrite([421(6),14161(6,R)])].

given #495 (T,wt=15): 15405 f(f(x,f(y,y)),f(x,f(f(y,c_0),z))) = x.  [para(11761(a,2),353(a,1,2,2))].

given #496 (T,wt=15): 15420 f(f(x,f(y,y)),f(x,f(z,f(y,c_0)))) = x.  [para(11761(a,1),455(a,1,1))].

given #497 (A,wt=19): 584 f(x,f(f(f(x,y),z),f(f(u,y),x))) = f(f(u,y),x).  [para(466(a,1),454(a,1,1))].

given #498 (T,wt=15): 15423 f(f(f(x,x),y),f(y,f(f(x,c_0),z))) = y.  [para(11761(a,2),455(a,1,2,2))].

given #499 (T,wt=15): 15425 f(f(x,f(y,y)),f(f(f(y,c_0),z),x)) = x.  [para(11761(a,2),456(a,1,2,1))].

given #500 (T,wt=15): 15428 f(f(f(f(x,c_0),y),z),f(z,f(x,x))) = z.  [para(11761(a,2),466(a,1,1,1))].

given #501 (T,wt=15): 15439 f(f(x,f(y,f(z,c_0))),f(x,f(z,z))) = x.  [para(11761(a,1),504(a,1,2))].

given #502 (A,wt=19): 585 f(x,f(f(y,f(x,z)),f(f(u,z),x))) = f(f(u,z),x).  [para(466(a,1),456(a,1,1))].

given #503 (T,wt=15): 15440 f(f(x,f(f(y,c_0),z)),f(f(y,y),x)) = x.  [para(11761(a,2),504(a,1,1,2))].

given #504 (T,wt=15): 15442 f(f(x,f(y,y)),f(f(z,f(y,c_0)),x)) = x.  [para(11761(a,1),519(a,1,1))].

given #505 (T,wt=15): 15443 f(f(f(x,x),y),f(f(f(x,c_0),z),y)) = y.  [para(11761(a,2),519(a,1,2,1))].

given #506 (T,wt=15): 15498 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(c_0,x)).  [para(11761(a,1),314(a,1,2,1)),rewrite([14451(9)])].

given #507 (A,wt=19): 589 f(f(x,f(y,f(f(z,u),x))),f(x,f(f(x,z),v))) = x.  [para(467(a,1),291(a,1,1,1)),rewrite([467(8),467(12)])].

given #508 (T,wt=15): 15505 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,y))).  [para(11761(a,1),429(a,1,2,2,2)),rewrite([441(5)]),flip(a)].

given #509 (T,wt=15): 15508 f(f(x,c_0),f(c_0,y)) = f(f(y,y),f(x,x)).  [para(11761(a,1),1380(a,1)),rewrite([14161(9,R)]),flip(a)].

given #510 (T,wt=15): 15521 f(f(x,c_0),f(y,y)) = f(f(x,x),f(c_0,y)).  [para(11761(a,2),1422(a,1)),rewrite([14161(8,R)])].

given #511 (T,wt=15): 15522 f(f(x,c_0),f(y,c_0)) = f(f(y,y),f(x,x)).  [para(11761(a,1),1423(a,1)),rewrite([11780(9,R)]),flip(a)].

given #512 (A,wt=19): 590 f(x,f(f(f(x,y),z),f(f(y,u),x))) = f(f(y,u),x).  [para(467(a,1),454(a,1,1))].

given #513 (T,wt=15): 15524 f(f(x,c_0),f(y,y)) = f(f(x,x),f(y,c_0)).  [para(11761(a,2),1647(a,1)),rewrite([11780(8,R)])].

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

given #515 (T,wt=15): 15833 f(f(x,f(f(y,c_0),z)),f(x,f(z,y))) = x.  [para(11761(a,2),1421(a,1,1,2)),rewrite([11808(7,R),11777(7)])].

given #516 (T,wt=15): 15834 f(f(x,f(y,z)),f(x,f(f(z,c_0),y))) = x.  [para(11761(a,2),1421(a,1,2,2))].

given #517 (A,wt=19): 591 f(x,f(f(y,f(x,z)),f(f(z,u),x))) = f(f(z,u),x).  [para(467(a,1),456(a,1,1))].

given #518 (T,wt=15): 15888 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(y,y)).  [para(11761(a,1),11761(a,2))].

given #519 (T,wt=15): 15909 f(f(f(x,y),z),f(z,f(f(x,c_0),y))) = z.  [para(11776(a,2),455(a,1,2,2))].

given #520 (T,wt=15): 15911 f(f(x,f(y,z)),f(f(f(y,c_0),z),x)) = x.  [para(11776(a,2),456(a,1,2,1))].

given #521 (T,wt=15): 15916 f(f(f(f(x,c_0),y),z),f(z,f(x,y))) = z.  [para(11776(a,2),466(a,1,1,1))].

given #522 (A,wt=19): 593 f(f(x,f(y,f(x,f(z,u)))),f(x,f(f(z,x),v))) = x.  [para(471(a,1),291(a,1,1,1)),rewrite([471(8),471(12)])].

given #523 (T,wt=15): 15929 f(f(x,f(f(y,c_0),z)),f(f(y,z),x)) = x.  [para(11776(a,2),504(a,1,1,2))].

given #524 (T,wt=15): 15934 f(f(f(x,y),z),f(f(f(x,c_0),y),z)) = z.  [para(11776(a,2),519(a,1,2,1))].

given #525 (T,wt=15): 16004 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,z))).  [para(11776(a,1),429(a,1,2,2,2)),rewrite([441(5)]),flip(a)].

given #526 (T,wt=15): 16042 f(f(f(x,c_0),y),z) = f(f(y,f(x,y)),z).  [para(11776(a,1),545(a,2,1)),rewrite([545(8)])].

given #527 (A,wt=19): 594 f(x,f(f(f(y,x),z),f(x,f(y,u)))) = f(x,f(y,u)).  [para(471(a,1),454(a,1,1))].

given #528 (T,wt=15): 16210 f(f(x,f(c_0,f(y,z))),f(x,f(z,y))) = x.  [para(11776(a,2),1420(a,1,2,2,2)),rewrite([11808(3,R),14164(8,R),11778(8)])].

given #529 (T,wt=15): 16256 f(f(x,c_0),f(y,y)) = f(f(y,c_0),f(x,x)).  [back_rewrite(15895),rewrite([16006(5)])].

given #530 (T,wt=15): 16327 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,y))).  [para(11780(a,1),429(a,2,2)),rewrite([429(8)])].

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

given #532 (A,wt=19): 595 f(x,f(f(y,f(z,x)),f(x,f(z,u)))) = f(x,f(z,u)).  [para(471(a,1),456(a,1,1))].

given #533 (T,wt=15): 16368 f(f(f(x,f(y,c_0)),z),f(f(y,y),z)) = z.  [para(11780(a,2),648(a,1,1,1))].

given #534 (T,wt=15): 16615 f(x,f(f(y,c_0),z)) = f(x,f(z,f(z,y))).  [para(11781(a,1),429(a,1,2,2,2)),rewrite([441(5)]),flip(a)].

given #535 (T,wt=15): 16667 f(f(f(x,c_0),y),z) = f(f(y,f(y,x)),z).  [para(11781(a,1),545(a,2,1)),rewrite([545(8)])].

given #536 (T,wt=15): 16935 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(c_0,y)).  [para(11781(a,1),11761(a,2)),rewrite([14161(9,R)])].

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

given #537 (A,wt=19): 596 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)).  [para(169(a,1),472(a,1,1))].

given #538 (T,wt=15): 17238 f(x,f(y,f(z,c_0))) = f(x,f(y,f(y,z))).  [para(11786(a,1),429(a,2,2)),rewrite([429(8)])].

given #539 (T,wt=15): 17259 f(f(x,f(y,c_0)),z) = f(f(x,f(x,y)),z).  [para(11786(a,1),545(a,1,2,2,1)),rewrite([545(5)]),flip(a)].

given #540 (T,wt=15): 17370 f(f(x,c_0),f(c_0,y)) = f(f(y,c_0),f(x,x)).  [para(11786(a,1),11761(a,1)),rewrite([14161(6,R)])].

given #541 (T,wt=15): 17429 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,z))).  [para(11788(a,1),429(a,2,2)),rewrite([429(8)])].

given #542 (A,wt=17): 597 f(x,f(f(y,x),f(f(f(y,z),x),u))) = f(y,x).  [para(472(a,1),338(a,1,1))].

given #543 (T,wt=15): 17453 f(f(x,f(y,c_0)),z) = f(f(x,f(y,y)),z).  [para(11788(a,1),545(a,1,2,2,1)),rewrite([545(5)]),flip(a)].

given #544 (T,wt=15): 17588 f(f(f(c_0,x),y),f(c_0,f(x,z))) = f(x,z).  [para(336(a,1),11800(a,1,2)),rewrite([14133(14)])].

given #545 (T,wt=15): 17597 f(f(x,f(c_0,y)),f(c_0,f(y,z))) = f(y,z).  [para(348(a,1),11800(a,1,2)),rewrite([14140(14)])].

given #546 (T,wt=15): 17602 f(f(x,f(c_0,y)),f(c_0,f(z,y))) = f(z,y).  [para(355(a,1),11800(a,1,2)),rewrite([14144(14)])].

given #547 (A,wt=19): 598 f(x,f(f(f(x,y),z),f(x,f(y,u)))) = f(x,f(y,u)).  [para(338(a,1),472(a,1,1))].

given #548 (T,wt=15): 17607 f(f(f(c_0,x),y),f(c_0,f(z,x))) = f(z,x).  [para(401(a,1),11800(a,1,2)),rewrite([14145(14)])].

given #549 (T,wt=15): 17811 f(x,f(f(y,c_0),z)) = f(x,f(f(y,y),z)).  [para(11814(a,1),429(a,1,2,2,2)),rewrite([429(5)]),flip(a)].

given #550 (T,wt=15): 17814 f(f(x,c_0),f(c_0,y)) = f(f(x,x),f(y,y)).  [para(11814(a,1),1380(a,1)),rewrite([14161(9,R)]),flip(a)].

given #551 (T,wt=15): 17845 f(f(f(x,c_0),y),z) = f(f(f(x,x),y),z).  [para(11814(a,1),545(a,2,1)),rewrite([545(8)])].

given #552 (A,wt=17): 599 f(x,f(f(y,x),f(z,f(f(y,u),x)))) = f(y,x).  [para(472(a,1),353(a,1,1))].

given #553 (T,wt=15): 18078 f(f(x,c_0),f(c_0,y)) = f(f(x,x),f(y,c_0)).  [para(11814(a,1),11786(a,1)),rewrite([14161(10,R)]),flip(a)].

given #554 (T,wt=15): 18785 f(x,f(f(c_0,y),z)) = f(x,f(f(y,y),z)).  [para(14148(a,1),429(a,1,2,2,2)),rewrite([429(5)]),flip(a)].

given #555 (T,wt=15): 18788 f(f(c_0,x),f(c_0,y)) = f(f(x,x),f(y,y)).  [para(14148(a,1),1380(a,1)),rewrite([14161(9,R)]),flip(a)].

given #556 (T,wt=15): 18791 f(f(c_0,x),f(y,y)) = f(f(x,x),f(c_0,y)).  [para(14148(a,2),1380(a,1)),rewrite([14161(8,R)])].

given #557 (A,wt=19): 600 f(x,f(f(f(x,y),z),f(x,f(u,y)))) = f(x,f(u,y)).  [para(353(a,1),472(a,1,1))].

given #558 (T,wt=15): 18806 f(f(c_0,x),f(y,c_0)) = f(f(x,x),f(y,y)).  [para(14148(a,1),1423(a,1)),rewrite([11780(9,R)]),flip(a)].

given #559 (T,wt=15): 18808 f(f(c_0,x),f(y,y)) = f(f(x,x),f(y,c_0)).  [para(14148(a,2),1423(a,1)),rewrite([11780(8,R)])].

given #560 (T,wt=15): 18865 f(f(f(c_0,x),y),z) = f(f(f(x,x),y),z).  [para(14148(a,1),545(a,2,1)),rewrite([545(8)])].

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

given #561 (T,wt=15): 19230 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,x)).  [para(14148(a,2),11761(a,2)),flip(a)].

given #562 (A,wt=19): 602 f(f(x,x),f(f(x,y),f(z,f(x,z)))) = f(z,f(x,z)).  [para(427(a,1),472(a,1,1))].

given #563 (T,wt=15): 19243 f(f(c_0,x),f(c_0,y)) = f(f(x,x),f(y,c_0)).  [para(14148(a,1),11786(a,1)),rewrite([14161(10,R)]),flip(a)].

given #564 (T,wt=15): 19246 f(f(c_0,x),f(y,c_0)) = f(f(x,x),f(c_0,y)).  [para(14148(a,2),11786(a,1)),rewrite([14161(9,R)])].

given #565 (T,wt=15): 19319 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,z))).  [para(14160(a,1),429(a,1,2,2,2)),rewrite([18787(7)]),flip(a)].

given #566 (T,wt=15): 19326 f(f(c_0,x),f(c_0,y)) = f(f(y,y),f(x,x)).  [para(14160(a,1),1422(a,1)),rewrite([14161(9,R)]),flip(a)].

given #567 (A,wt=19): 603 f(x,f(f(f(y,z),x),f(f(y,x),u))) = f(f(y,z),x).  [para(472(a,1),453(a,1,1))].

given #568 (T,wt=15): 19329 f(f(c_0,x),f(y,c_0)) = f(f(y,y),f(x,x)).  [para(14160(a,1),1647(a,1)),rewrite([11780(9,R)]),flip(a)].

given #569 (T,wt=15): 19344 f(f(x,f(c_0,y)),z) = f(f(x,f(y,y)),z).  [para(14160(a,1),545(a,1,2,2,1)),rewrite([545(5)]),flip(a)].

given #570 (T,wt=15): 19466 f(f(c_0,x),f(c_0,y)) = f(f(y,c_0),f(x,x)).  [para(14160(a,1),11781(a,1)),rewrite([14161(10,R)]),flip(a)].

given #571 (T,wt=15): 19505 f(f(f(c_0,x),y),f(f(z,f(z,x)),y)) = y.  [para(14161(a,1),519(a,1,2,1))].

given #572 (A,wt=19): 604 f(f(x,f(y,f(z,x))),f(x,f(f(f(z,u),x),v))) = x.  [para(472(a,1),291(a,1,1,1)),rewrite([472(7),472(12)])].

given #573 (T,wt=15): 19557 f(x,f(y,f(c_0,z))) = f(x,f(y,f(y,z))).  [para(14161(a,1),429(a,2,2)),rewrite([429(8)])].

given #574 (T,wt=15): 19580 f(f(x,f(c_0,y)),z) = f(f(x,f(x,y)),z).  [para(14161(a,1),545(a,1,2,2,1)),rewrite([545(5)]),flip(a)].

given #575 (T,wt=15): 19991 f(x,f(f(c_0,y),z)) = f(x,f(z,f(z,y))).  [para(14163(a,1),429(a,1,2,2,2)),rewrite([441(5)]),flip(a)].

given #576 (T,wt=15): 20013 f(f(f(c_0,x),y),z) = f(f(y,f(y,x)),z).  [para(14163(a,1),545(a,2,1)),rewrite([545(8)])].

given #577 (A,wt=29): 605 f(f(x,y),f(f(f(f(x,y),f(z,x)),u),f(f(x,y),f(y,v)))) = f(f(x,y),f(y,v)).  [para(291(a,1),472(a,1,1))].

given #578 (T,wt=15): 20133 f(f(x,f(c_0,y)),f(x,f(z,f(y,z)))) = x.  [para(14164(a,1),353(a,1,2,2))].

given #579 (T,wt=15): 20169 f(f(f(c_0,x),y),f(f(z,f(x,z)),y)) = y.  [para(14164(a,1),519(a,1,2,1))].

given #580 (T,wt=15): 20229 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,y))).  [para(14164(a,1),429(a,2,2)),rewrite([429(8)])].

given #581 (T,wt=15): 20257 f(f(x,f(c_0,y)),z) = f(f(x,f(y,x)),z).  [para(14164(a,1),545(a,1,2,2,1)),rewrite([545(5)]),flip(a)].

given #582 (A,wt=19): 606 f(x,f(f(f(y,z),x),f(u,f(y,x)))) = f(f(y,z),x).  [para(472(a,1),455(a,1,1))].

given #583 (T,wt=15): 20445 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,c_0)).  [para(14164(a,1),11761(a,1)),rewrite([11780(6,R)]),flip(a)].

given #584 (T,wt=15): 20516 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,z))).  [para(14165(a,1),429(a,1,2,2,2)),rewrite([441(5)]),flip(a)].

given #585 (T,wt=15): 20540 f(f(f(c_0,x),y),z) = f(f(y,f(x,y)),z).  [para(14165(a,1),545(a,2,1)),rewrite([545(8)])].

given #586 (T,wt=15): 20674 f(f(c_0,x),f(y,c_0)) = f(f(c_0,y),f(x,x)).  [para(14165(a,2),14148(a,2)),rewrite([19464(5)])].

given #587 (A,wt=19): 607 f(x,f(f(f(y,x),z),f(x,f(u,y)))) = f(x,f(u,y)).  [para(455(a,1),472(a,1,1))].

given #588 (T,wt=15): 20702 f(f(x,f(y,x)),f(c_0,f(y,z))) = f(y,z).  [para(474(a,1),1423(a,2,2)),rewrite([11808(7,R),11777(7),421(5),2565(5),421(8),14161(8,R)]),flip(a)].

given #589 (T,wt=15): 20746 f(x,f(f(y,y),z)) = f(x,f(z,f(c_0,y))).  [para(14175(a,1),429(a,1,2,2,2)),rewrite([441(6)]),flip(a)].

given #590 (T,wt=15): 20754 f(f(f(x,x),y),z) = f(f(y,f(c_0,x)),z).  [para(14175(a,1),545(a,1,2,2,1)),rewrite([18868(7)]),flip(a)].

given #591 (T,wt=15): 20838 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,y))).  [para(14176(a,1),429(a,1,2,2,2)),rewrite([441(5)]),flip(a)].

given #592 (A,wt=19): 609 f(f(x,x),f(f(x,y),f(z,f(z,x)))) = f(z,f(z,x)).  [para(464(a,1),472(a,1,1))].

given #593 (T,wt=15): 20849 f(f(f(c_0,x),y),z) = f(f(y,f(x,x)),z).  [para(14176(a,1),545(a,1,2,2,1)),rewrite([18869(7)]),flip(a)].

given #594 (T,wt=15): 20929 f(f(c_0,x),f(y,y)) = f(f(c_0,y),f(x,x)).  [para(14176(a,2),14148(a,2))].

given #595 (T,wt=15): 20939 f(f(x,y),f(c_0,f(z,f(c_0,f(y,x))))) = c_0.  [para(15032(a,1),356(a,1,2,1)),rewrite([15032(13)])].

given #596 (T,wt=15): 21037 f(x,f(f(y,y),z)) = f(x,f(z,f(y,c_0))).  [para(16335(a,1),429(a,1,2,2,2)),rewrite([441(6)]),flip(a)].

given #597 (A,wt=19): 611 f(x,f(f(f(y,x),z),f(f(y,u),x))) = f(f(y,u),x).  [para(472(a,1),472(a,1,1))].

given #598 (T,wt=15): 21045 f(f(f(x,x),y),z) = f(f(y,f(x,c_0)),z).  [para(16335(a,1),545(a,1,2,2,1)),rewrite([15573(7)]),flip(a)].

given #599 (T,wt=15): 21158 f(x,f(y,f(x,f(f(y,x),z)))) = f(x,x).  [para(1089(a,1),475(a,1,2)),flip(a)].

given #600 (T,wt=15): 21176 f(f(f(x,c_0),y),f(c_0,f(x,z))) = f(x,z).  [para(475(a,1),11800(a,1,2)),rewrite([19909(14)])].

given #601 (T,wt=15): 21247 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x.  [para(11923(a,1),353(a,1,2,2)),rewrite([421(7)])].

given #602 (A,wt=33): 616 f(f(x,x),f(f(f(x,x),y),f(f(f(x,x),f(z,f(f(f(x,x),y),f(u,x)))),v))) = f(f(x,x),y).  [para(304(a,1),338(a,1,1))].

given #603 (T,wt=15): 21255 f(f(f(x,f(c_0,f(y,z))),u),f(u,z)) = u.  [para(11923(a,1),455(a,1,2,2))].

given #604 (T,wt=15): 21256 f(f(x,f(y,f(c_0,f(z,u)))),f(u,x)) = x.  [para(11923(a,1),456(a,1,2,1))].

given #605 (T,wt=15): 21258 f(f(x,y),f(y,f(z,f(c_0,f(u,x))))) = y.  [para(11923(a,1),466(a,1,1,1))].

given #606 (T,wt=15): 21260 f(f(x,y),f(f(z,f(c_0,f(u,y))),x)) = x.  [para(11923(a,1),504(a,1,1,2))].

given #607 (A,wt=33): 617 f(f(x,x),f(f(f(x,x),y),f(z,f(f(x,x),f(u,f(f(f(x,x),y),f(v,x))))))) = f(f(x,x),y).  [para(304(a,1),353(a,1,1))].

given #608 (T,wt=15): 21262 f(f(x,y),f(f(z,f(c_0,f(u,x))),y)) = y.  [para(11923(a,1),519(a,1,2,1)),rewrite([421(7)])].

given #609 (T,wt=15): 21271 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x).  [para(1380(a,1),11923(a,1,2,2,2)),rewrite([11808(3,R),11777(3)])].

given #610 (T,wt=15): 21275 f(x,f(y,f(c_0,f(z,f(x,z))))) = f(x,x).  [para(1423(a,1),11923(a,1,2,2,2)),rewrite([11808(3,R),11777(3)])].

given #611 (T,wt=15): 21322 f(x,f(y,f(c_0,f(z,f(x,c_0))))) = f(x,c_0).  [para(11822(a,1),11923(a,1,1))].

given #612 (A,wt=27): 618 f(f(x,x),f(f(f(x,x),y),f(z,f(f(f(x,x),y),f(u,x))))) = f(f(x,x),y).  [para(304(a,1),353(a,1,2)),rewrite([421(10)])].

given #613 (T,wt=15): 21323 f(x,f(y,f(c_0,f(z,f(c_0,x))))) = f(c_0,x).  [para(13688(a,1),11923(a,1,1))].

given #614 (T,wt=15): 21326 f(x,f(y,f(c_0,f(f(x,c_0),z)))) = f(x,x).  [para(11761(a,2),11923(a,1,2,2,2)),rewrite([11808(3,R),11777(3)])].

given #615 (T,wt=15): 21343 f(x,f(y,f(c_0,f(f(c_0,x),z)))) = f(x,x).  [para(14176(a,2),11923(a,1,2,2,2)),rewrite([11808(3,R),11777(3)])].

given #616 (T,wt=15): 21478 f(f(x,y),f(x,f(z,f(c_0,f(y,u))))) = x.  [para(14132(a,1),681(a,1,2,2)),rewrite([421(7)])].

given #617 (A,wt=25): 619 f(f(x,f(y,y)),f(f(y,y),f(z,f(f(x,f(y,y)),f(u,y))))) = f(y,y).  [para(380(a,1),304(a,1,1)),rewrite([380(9)])].

given #618 (T,wt=15): 21492 f(f(f(x,f(c_0,f(y,z))),u),f(u,y)) = u.  [para(14132(a,1),771(a,1,2,2))].

given #619 (T,wt=15): 21654 f(f(x,f(y,f(c_0,f(z,u)))),f(z,x)) = x.  [para(14138(a,1),456(a,1,2,1))].

given #620 (T,wt=15): 21655 f(f(x,y),f(y,f(z,f(c_0,f(x,u))))) = y.  [para(14138(a,1),466(a,1,1,1))].

given #621 (T,wt=15): 21657 f(f(x,y),f(f(z,f(c_0,f(y,u))),x)) = x.  [para(14138(a,1),504(a,1,1,2))].

given #622 (A,wt=25): 620 f(f(x,f(y,y)),f(f(y,y),f(z,f(f(f(y,y),x),f(u,y))))) = f(y,y).  [para(421(a,1),304(a,1,1))].

given #623 (T,wt=15): 21659 f(f(x,y),f(f(z,f(c_0,f(x,u))),y)) = y.  [para(14138(a,1),519(a,1,2,1)),rewrite([421(7)])].

given #624 (T,wt=15): 21732 f(x,f(f(y,f(y,x)),f(z,f(x,x)))) = c_0.  [para(1380(a,1),15389(a,1,2,1)),rewrite([11808(3,R),11777(3)])].

given #625 (T,wt=15): 21733 f(x,f(f(y,f(x,x)),f(z,f(z,x)))) = c_0.  [para(1380(a,1),15389(a,1,2,2)),rewrite([11808(3,R),11777(3)])].

given #626 (T,wt=15): 21740 f(x,f(f(y,f(x,y)),f(z,f(x,x)))) = c_0.  [para(1423(a,1),15389(a,1,2,1)),rewrite([11808(3,R),11777(3)])].

given #627 (A,wt=25): 621 f(f(f(x,x),y),f(f(x,x),f(z,f(f(y,f(x,x)),f(u,x))))) = f(x,x).  [para(421(a,1),304(a,1,2,2,2,1))].

given #628 (T,wt=15): 21741 f(x,f(f(y,f(x,x)),f(z,f(x,z)))) = c_0.  [para(1423(a,1),15389(a,1,2,2)),rewrite([11808(3,R),11777(3)])].

given #629 (T,wt=15): 21776 f(x,f(f(y,f(x,c_0)),f(z,f(x,c_0)))) = c_0.  [para(11822(a,1),15389(a,1,1))].

given #630 (T,wt=15): 21777 f(x,f(f(y,f(c_0,x)),f(z,f(c_0,x)))) = c_0.  [para(13688(a,1),15389(a,1,1))].

given #631 (T,wt=15): 21778 f(x,f(f(f(x,c_0),y),f(z,f(x,x)))) = c_0.  [para(11761(a,2),15389(a,1,2,1)),rewrite([11808(3,R),11777(3)])].

given #632 (A,wt=25): 622 f(f(f(x,x),y),f(f(x,x),f(z,f(f(u,x),f(f(x,x),y))))) = f(x,x).  [para(421(a,1),304(a,1,2,2,2))].

given #633 (T,wt=15): 21779 f(x,f(f(y,f(x,x)),f(f(x,c_0),z))) = c_0.  [para(11761(a,2),15389(a,1,2,2)),rewrite([11808(3,R),11777(3)])].

given #634 (T,wt=15): 21782 f(x,f(f(y,f(x,y)),f(z,f(x,c_0)))) = c_0.  [para(11780(a,1),15389(a,1,2,1)),rewrite([11808(5,R),11778(4)])].

given #635 (T,wt=15): 21783 f(x,f(f(y,f(x,c_0)),f(z,f(x,z)))) = c_0.  [para(11780(a,1),15389(a,1,2,2)),rewrite([11808(5,R),11778(4)])].

given #636 (T,wt=15): 21790 f(x,f(f(y,f(y,x)),f(z,f(x,c_0)))) = c_0.  [para(11786(a,1),15389(a,1,2,1)),rewrite([11808(5,R),11778(4)])].

given #637 (A,wt=25): 623 f(f(f(x,x),y),f(f(x,x),f(f(f(f(x,x),y),f(z,x)),u))) = f(x,x).  [para(421(a,1),304(a,1,2,2))].

given #638 (T,wt=15): 21791 f(x,f(f(y,f(x,c_0)),f(z,f(z,x)))) = c_0.  [para(11786(a,1),15389(a,1,2,2)),rewrite([11808(5,R),11778(4)])].

given #639 (T,wt=15): 21794 f(x,f(f(y,f(x,x)),f(z,f(x,c_0)))) = c_0.  [para(11788(a,1),15389(a,1,2,1)),rewrite([11808(5,R),11778(4)])].

given #640 (T,wt=15): 21795 f(x,f(f(y,f(x,c_0)),f(z,f(x,x)))) = c_0.  [para(11788(a,1),15389(a,1,2,2)),rewrite([11808(5,R),11778(4)])].

given #641 (T,wt=15): 21799 f(x,f(f(y,f(x,x)),f(z,f(c_0,x)))) = c_0.  [para(14160(a,1),15389(a,1,2,1)),rewrite([11808(5,R),11783(4)])].

given #642 (A,wt=43): 626 f(f(x,x),f(f(f(x,x),f(y,f(f(f(x,x),z),f(u,x)))),f(f(f(x,x),z),v))) = f(f(x,x),f(y,f(f(f(x,x),z),f(u,x)))).  [para(304(a,1),453(a,1,1))].

given #643 (T,wt=15): 21800 f(x,f(f(y,f(c_0,x)),f(z,f(x,x)))) = c_0.  [para(14160(a,1),15389(a,1,2,2)),rewrite([11808(5,R),11783(4)])].

given #644 (T,wt=15): 21801 f(x,f(f(y,f(y,x)),f(z,f(c_0,x)))) = c_0.  [para(14161(a,1),15389(a,1,2,1)),rewrite([11808(5,R),11783(4)])].

given #645 (T,wt=15): 21802 f(x,f(f(y,f(c_0,x)),f(z,f(z,x)))) = c_0.  [para(14161(a,1),15389(a,1,2,2)),rewrite([11808(5,R),11783(4)])].

given #646 (T,wt=15): 21809 f(x,f(f(y,f(x,y)),f(z,f(c_0,x)))) = c_0.  [para(14164(a,1),15389(a,1,2,1)),rewrite([11808(5,R),11783(4)])].

given #647 (A,wt=37): 627 f(f(f(x,x),f(y,f(f(x,x),z))),f(f(x,x),f(f(f(x,x),f(u,f(f(f(x,x),z),f(v,x)))),w))) = f(x,x).  [para(304(a,1),291(a,1,1,1)),rewrite([304(15),304(26)])].

given #648 (T,wt=15): 21810 f(x,f(f(y,f(c_0,x)),f(z,f(x,z)))) = c_0.  [para(14164(a,1),15389(a,1,2,2)),rewrite([11808(5,R),11783(4)])].

given #649 (T,wt=15): 21816 f(x,f(f(f(x,x),y),f(z,f(c_0,x)))) = c_0.  [para(14175(a,2),15389(a,1,2,1)),rewrite([11808(5,R),11783(4)])].

given #650 (T,wt=15): 21817 f(x,f(f(y,f(c_0,x)),f(f(x,x),z))) = c_0.  [para(14175(a,2),15389(a,1,2,2)),rewrite([11808(5,R),11783(4)])].

given #651 (T,wt=15): 21818 f(x,f(f(f(c_0,x),y),f(z,f(x,x)))) = c_0.  [para(14176(a,2),15389(a,1,2,1)),rewrite([11808(3,R),11777(3)])].

given #652 (A,wt=43): 629 f(f(x,x),f(f(f(x,x),f(y,f(f(f(x,x),z),f(u,x)))),f(v,f(f(x,x),z)))) = f(f(x,x),f(y,f(f(f(x,x),z),f(u,x)))).  [para(304(a,1),455(a,1,1))].

given #653 (T,wt=15): 21819 f(x,f(f(y,f(x,x)),f(f(c_0,x),z))) = c_0.  [para(14176(a,2),15389(a,1,2,2)),rewrite([11808(3,R),11777(3)])].

given #654 (T,wt=15): 21820 f(x,f(f(f(x,x),y),f(z,f(x,c_0)))) = c_0.  [para(16335(a,2),15389(a,1,2,1)),rewrite([11808(5,R),11778(4)])].

given #655 (T,wt=15): 21821 f(x,f(f(y,f(x,c_0)),f(f(x,x),z))) = c_0.  [para(16335(a,2),15389(a,1,2,2)),rewrite([11808(5,R),11778(4)])].

given #656 (T,wt=15): 21880 f(f(x,f(y,c_0)),f(c_0,f(y,z))) = f(y,z).  [para(19835(a,1),549(a,1,2)),rewrite([421(4),11803(4)]),flip(a)].

given #657 (A,wt=37): 630 f(f(x,x),f(y,f(f(x,x),f(z,f(f(f(x,x),y),f(u,x)))))) = f(f(x,x),f(z,f(f(f(x,x),y),f(u,x)))).  [para(304(a,1),456(a,1,2)),rewrite([421(8),421(10)])].

given #658 (T,wt=15): 21883 f(f(x,f(y,c_0)),f(c_0,f(z,y))) = f(z,y).  [para(531(a,1),19855(a,1,1,2)),rewrite([421(6)])].

given #659 (T,wt=15): 21897 f(f(f(x,c_0),y),f(c_0,f(z,x))) = f(z,x).  [para(19896(a,1),545(a,1,2)),rewrite([421(4),11800(4)]),flip(a)].

given #660 (T,wt=15): 21982 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,x).  [para(163(a,1),21336(a,1,1))].

given #661 (T,wt=15): 21985 f(f(x,y),f(x,f(z,f(z,f(u,y))))) = x.  [para(21336(a,1),353(a,1,2,2)),rewrite([421(6)])].

given #662 (A,wt=43): 635 f(f(x,x),f(f(f(f(x,x),y),z),f(f(x,x),f(u,f(f(f(x,x),y),f(v,x)))))) = f(f(x,x),f(u,f(f(f(x,x),y),f(v,x)))).  [para(304(a,1),472(a,1,1))].

given #663 (T,wt=15): 21993 f(f(f(x,f(x,f(y,z))),u),f(u,z)) = u.  [para(21336(a,1),455(a,1,2,2))].

given #664 (T,wt=15): 21995 f(f(x,f(y,f(y,f(z,u)))),f(u,x)) = x.  [para(21336(a,1),456(a,1,2,1))].

given #665 (T,wt=15): 21997 f(f(x,y),f(y,f(z,f(z,f(u,x))))) = y.  [para(21336(a,1),466(a,1,1,1))].

Low Water (keep, True_semantics): wt=21

given #666 (T,wt=15): 21999 f(f(x,y),f(f(z,f(z,f(u,y))),x)) = x.  [para(21336(a,1),504(a,1,1,2))].

given #667 (A,wt=19): 637 f(f(x,f(y,f(x,f(z,u)))),f(x,f(f(u,x),v))) = x.  [para(504(a,1),291(a,1,1,1)),rewrite([504(8),504(12)])].

given #668 (T,wt=15): 22001 f(f(x,y),f(f(z,f(z,f(u,x))),y)) = y.  [para(21336(a,1),519(a,1,2,1)),rewrite([421(6)])].

given #669 (T,wt=15): 22014 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0.  [para(21336(a,1),1380(a,2,2)),rewrite([11808(8,R),421(9),11683(9)])].

given #670 (T,wt=15): 22015 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x).  [para(1380(a,1),21336(a,1,2,2,2)),rewrite([11808(3,R),11777(3)])].

given #671 (T,wt=15): 22020 f(x,f(y,f(y,f(z,f(x,z))))) = f(x,x).  [para(1423(a,1),21336(a,1,2,2,2)),rewrite([11808(3,R),11777(3)])].

given #672 (A,wt=19): 638 f(x,f(f(y,f(z,x)),f(x,f(u,z)))) = f(x,f(u,z)).  [para(504(a,1),456(a,1,1))].

given #673 (T,wt=15): 22094 f(x,f(y,f(y,f(z,f(x,c_0))))) = f(x,c_0).  [para(11822(a,1),21336(a,1,1))].

given #674 (T,wt=15): 22095 f(x,f(y,f(y,f(z,f(c_0,x))))) = f(c_0,x).  [para(13688(a,1),21336(a,1,1))].

given #675 (T,wt=15): 22098 f(x,f(y,f(y,f(f(x,c_0),z)))) = f(x,x).  [para(11761(a,2),21336(a,1,2,2,2)),rewrite([11808(3,R),11777(3)])].

given #676 (T,wt=15): 22116 f(x,f(y,f(y,f(f(x,x),z)))) = f(c_0,x).  [para(14175(a,2),21336(a,1,2,2,2)),rewrite([11808(5,R),11783(4)])].

given #677 (A,wt=19): 640 f(f(x,x),f(f(y,x),f(z,f(x,x)))) = f(z,f(x,x)).  [para(169(a,1),519(a,1,1))].

given #678 (T,wt=15): 22117 f(x,f(y,f(y,f(f(c_0,x),z)))) = f(x,x).  [para(14176(a,2),21336(a,1,2,2,2)),rewrite([11808(3,R),11777(3)])].

given #679 (T,wt=15): 22201 f(f(x,f(y,z)),f(c_0,f(z,y))) = f(z,y).  [para(13702(a,1),21344(a,1,1,2,2)),rewrite([11783(5),421(5)])].

given #680 (T,wt=15): 22203 f(f(x,f(y,z)),f(x,f(u,f(z,y)))) = x.  [back_rewrite(21407),rewrite([22201(8)])].

given #681 (T,wt=15): 22222 f(f(x,y),f(x,f(z,f(z,f(y,u))))) = x.  [para(21503(a,1),353(a,1,2,2)),rewrite([421(6)])].

given #682 (A,wt=19): 641 f(f(x,x),f(f(y,x),f(f(x,x),z))) = f(f(x,x),z).  [para(258(a,1),519(a,1,1))].

given #683 (T,wt=15): 22227 f(f(f(x,f(x,f(y,z))),u),f(u,y)) = u.  [para(21503(a,1),455(a,1,2,2))].

given #684 (T,wt=15): 22228 f(f(x,f(y,f(y,f(z,u)))),f(z,x)) = x.  [para(21503(a,1),456(a,1,2,1))].

given #685 (T,wt=15): 22230 f(f(x,y),f(y,f(z,f(z,f(x,u))))) = y.  [para(21503(a,1),466(a,1,1,1))].

given #686 (T,wt=15): 22232 f(f(x,y),f(f(z,f(z,f(y,u))),x)) = x.  [para(21503(a,1),504(a,1,1,2))].

given #687 (A,wt=17): 642 f(x,f(f(y,x),f(f(f(z,y),x),u))) = f(y,x).  [para(519(a,1),338(a,1,1))].

given #688 (T,wt=15): 22234 f(f(x,y),f(f(z,f(z,f(x,u))),y)) = y.  [para(21503(a,1),519(a,1,2,1)),rewrite([421(6)])].

given #689 (T,wt=15): 22454 f(x,f(f(f(x,x),y),f(z,f(z,x)))) = c_0.  [para(1380(a,1),21709(a,1,2,2)),rewrite([11808(3,R),11777(3)])].

given #690 (T,wt=15): 22458 f(x,f(f(f(x,x),y),f(z,f(x,z)))) = c_0.  [para(1423(a,1),21709(a,1,2,2)),rewrite([11808(3,R),11777(3)])].

given #691 (T,wt=15): 22491 f(x,f(f(f(x,c_0),y),f(z,f(x,c_0)))) = c_0.  [para(11822(a,1),21709(a,1,1))].

given #692 (A,wt=19): 643 f(x,f(f(y,f(x,z)),f(x,f(z,u)))) = f(x,f(z,u)).  [para(338(a,1),519(a,1,1))].

given #693 (T,wt=15): 22492 f(x,f(f(f(c_0,x),y),f(z,f(c_0,x)))) = c_0.  [para(13688(a,1),21709(a,1,1))].

given #694 (T,wt=15): 22493 f(x,f(f(f(x,x),y),f(f(x,c_0),z))) = c_0.  [para(11761(a,2),21709(a,1,2,2)),rewrite([11808(3,R),11777(3)])].

given #695 (T,wt=15): 22494 f(x,f(f(f(x,c_0),y),f(z,f(x,z)))) = c_0.  [para(11780(a,1),21709(a,1,2,2)),rewrite([11808(5,R),11778(4)])].

given #696 (T,wt=15): 22498 f(x,f(f(f(x,c_0),y),f(z,f(z,x)))) = c_0.  [para(11786(a,1),21709(a,1,2,2)),rewrite([11808(5,R),11778(4)])].

given #697 (A,wt=17): 644 f(x,f(f(y,x),f(z,f(f(u,y),x)))) = f(y,x).  [para(519(a,1),353(a,1,1))].

given #698 (T,wt=15): 22503 f(x,f(f(f(c_0,x),y),f(z,f(z,x)))) = c_0.  [para(14161(a,1),21709(a,1,2,2)),rewrite([11808(5,R),11783(4)])].

given #699 (T,wt=15): 22507 f(x,f(f(f(c_0,x),y),f(z,f(x,z)))) = c_0.  [para(14164(a,1),21709(a,1,2,2)),rewrite([11808(5,R),11783(4)])].

given #700 (T,wt=15): 22510 f(x,f(f(f(c_0,x),y),f(f(x,x),z))) = c_0.  [para(14175(a,2),21709(a,1,2,2)),rewrite([11808(5,R),11783(4)])].

given #701 (T,wt=15): 22511 f(x,f(f(f(x,x),y),f(f(c_0,x),z))) = c_0.  [para(14176(a,2),21709(a,1,2,2)),rewrite([11808(3,R),11777(3)])].

given #702 (A,wt=19): 645 f(x,f(f(y,f(x,z)),f(x,f(u,z)))) = f(x,f(u,z)).  [para(353(a,1),519(a,1,1))].

given #703 (T,wt=15): 22512 f(x,f(f(f(x,c_0),y),f(f(x,x),z))) = c_0.  [para(16335(a,2),21709(a,1,2,2)),rewrite([11808(5,R),11778(4)])].

given #704 (T,wt=15): 22520 f(x,f(f(y,f(x,x)),f(f(x,x),z))) = c_0.  [para(163(a,1),21710(a,1,1))].

given #705 (T,wt=15): 22540 f(x,f(f(y,f(y,x)),f(f(x,x),z))) = c_0.  [para(1380(a,1),21710(a,1,2,1)),rewrite([11808(3,R),11777(3)])].

given #706 (T,wt=15): 22542 f(x,f(f(y,f(x,y)),f(f(x,x),z))) = c_0.  [para(1423(a,1),21710(a,1,2,1)),rewrite([11808(3,R),11777(3)])].

given #707 (A,wt=19): 647 f(f(x,x),f(f(y,x),f(z,f(x,z)))) = f(z,f(x,z)).  [para(427(a,1),519(a,1,1))].

given #708 (T,wt=15): 22571 f(x,f(f(y,f(x,c_0)),f(f(x,c_0),z))) = c_0.  [para(11822(a,1),21710(a,1,1))].

given #709 (T,wt=15): 22572 f(x,f(f(y,f(c_0,x)),f(f(c_0,x),z))) = c_0.  [para(13688(a,1),21710(a,1,1))].

given #710 (T,wt=15): 22574 f(x,f(f(y,f(x,y)),f(f(x,c_0),z))) = c_0.  [para(11780(a,1),21710(a,1,2,1)),rewrite([11808(5,R),11778(4)])].

given #711 (T,wt=15): 22577 f(x,f(f(y,f(y,x)),f(f(x,c_0),z))) = c_0.  [para(11786(a,1),21710(a,1,2,1)),rewrite([11808(5,R),11778(4)])].

given #712 (A,wt=19): 649 f(x,f(f(f(y,z),x),f(f(z,x),u))) = f(f(y,z),x).  [para(519(a,1),453(a,1,1))].

given #713 (T,wt=15): 22579 f(x,f(f(y,f(y,x)),f(f(c_0,x),z))) = c_0.  [para(14161(a,1),21710(a,1,2,1)),rewrite([11808(5,R),11783(4)])].

given #714 (T,wt=15): 22582 f(x,f(f(y,f(x,y)),f(f(c_0,x),z))) = c_0.  [para(14164(a,1),21710(a,1,2,1)),rewrite([11808(5,R),11783(4)])].

given #715 (T,wt=15): 22680 f(f(x,f(x,y)),f(c_0,f(z,y))) = f(z,y).  [para(264(a,1),21889(a,1,1,2,2)),rewrite([421(5)])].

given #716 (T,wt=15): 22681 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z).  [para(324(a,1),21889(a,1,1,2,2)),rewrite([421(5)])].

given #717 (A,wt=19): 650 f(f(x,f(y,f(z,x))),f(x,f(f(f(u,z),x),v))) = x.  [para(519(a,1),291(a,1,1,1)),rewrite([519(7),519(12)])].

given #718 (T,wt=15): 22682 f(f(x,f(y,x)),f(c_0,f(z,y))) = f(z,y).  [para(519(a,1),21889(a,1,1,2)),rewrite([421(2),421(5)])].

given #719 (T,wt=15): 22712 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0.  [para(21963(a,1),1380(a,2,2)),rewrite([11808(8,R),421(9),11683(9)])].

given #720 (T,wt=15): 22911 f(x,f(f(f(x,x),y),f(f(x,x),z))) = c_0.  [para(163(a,1),22434(a,1,1))].

given #721 (T,wt=15): 22960 f(x,f(f(f(x,c_0),y),f(f(x,c_0),z))) = c_0.  [para(11822(a,1),22434(a,1,1))].

given #722 (A,wt=29): 651 f(f(x,y),f(f(z,f(f(x,y),f(u,x))),f(f(x,y),f(y,v)))) = f(f(x,y),f(y,v)).  [para(291(a,1),519(a,1,1))].

given #723 (T,wt=15): 22961 f(x,f(f(f(c_0,x),y),f(f(c_0,x),z))) = c_0.  [para(13688(a,1),22434(a,1,1))].

given #724 (T,wt=15): 23511 f(f(f(f(x,x),y),z),f(c_0,f(z,x))) = c_0.  [para(1436(a,1),11741(a,1,2,2,2)),rewrite([421(7),381(7)])].

given #725 (T,wt=15): 23633 f(f(f(x,f(y,y)),z),f(c_0,f(z,y))) = c_0.  [para(1444(a,1),11741(a,1,2,2,2)),rewrite([421(7),381(7)])].

given #726 (T,wt=15): 24343 f(f(x,f(y,y)),z) = f(z,f(x,f(x,y))).  [para(1543(a,1),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #727 (A,wt=23): 652 f(f(x,y),f(f(z,x),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)).  [para(291(a,1),519(a,1,2)),rewrite([421(7)])].

given #728 (T,wt=15): 24344 f(f(x,f(x,y)),z) = f(z,f(x,f(y,y))).  [para(1543(a,2),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #729 (T,wt=15): 24630 f(f(x,f(y,z)),f(x,f(f(y,y),u))) = x.  [para(301(a,1),1646(a,1,2,2)),rewrite([421(5),505(5)])].

given #730 (T,wt=15): 24638 f(f(x,f(y,z)),f(x,f(f(z,z),u))) = x.  [para(307(a,1),1646(a,1,2,2)),rewrite([421(5),503(5)])].

given #731 (T,wt=15): 24650 f(f(x,f(y,z)),f(x,f(u,f(y,y)))) = x.  [para(392(a,1),1646(a,1,2,2)),rewrite([11808(5,R),11777(5),421(5),533(5)])].

given #732 (A,wt=19): 653 f(x,f(f(f(y,z),x),f(u,f(z,x)))) = f(f(y,z),x).  [para(519(a,1),455(a,1,1))].

given #733 (T,wt=15): 24652 f(f(x,f(y,z)),f(x,f(u,f(z,z)))) = x.  [para(402(a,1),1646(a,1,2,2)),rewrite([11808(5,R),11777(5),421(5),532(5)])].

given #734 (T,wt=15): 24726 f(f(x,f(y,z)),f(x,f(u,f(y,u)))) = x.  [para(474(a,1),1646(a,1,2,2)),rewrite([421(5),2565(5)])].

given #735 (T,wt=15): 24755 f(f(f(x,y),z),f(z,f(f(x,x),u))) = z.  [para(301(a,1),1658(a,1,2,2)),rewrite([421(5),505(5)])].

given #736 (T,wt=15): 24757 f(f(f(x,y),z),f(z,f(f(y,y),u))) = z.  [para(307(a,1),1658(a,1,2,2)),rewrite([421(5),503(5)])].

given #737 (A,wt=19): 655 f(f(x,x),f(f(y,x),f(z,f(z,x)))) = f(z,f(z,x)).  [para(464(a,1),519(a,1,1))].

given #738 (T,wt=15): 24762 f(f(f(x,y),z),f(z,f(u,f(x,x)))) = z.  [para(392(a,1),1658(a,1,2,2)),rewrite([11808(5,R),11777(5),421(5),533(5)])].

given #739 (T,wt=15): 24763 f(f(f(x,y),z),f(z,f(u,f(y,y)))) = z.  [para(402(a,1),1658(a,1,2,2)),rewrite([11808(5,R),11777(5),421(5),532(5)])].

given #740 (T,wt=15): 24801 f(f(f(x,y),z),f(z,f(u,f(x,u)))) = z.  [para(474(a,1),1658(a,1,2,2)),rewrite([421(5),2565(5)])].

given #741 (T,wt=15): 24819 f(f(x,f(y,z)),f(f(f(y,y),u),x)) = x.  [para(301(a,1),1659(a,1,2,1)),rewrite([421(5),505(5)])].

given #742 (A,wt=19): 658 f(x,f(f(f(y,x),z),f(f(u,y),x))) = f(f(u,y),x).  [para(519(a,1),472(a,1,1))].

given #743 (T,wt=15): 24824 f(f(x,f(y,z)),f(f(f(z,z),u),x)) = x.  [para(307(a,1),1659(a,1,2,1)),rewrite([421(5),503(5)])].

given #744 (T,wt=15): 24831 f(f(x,f(y,z)),f(f(u,f(y,y)),x)) = x.  [para(392(a,1),1659(a,1,2,1)),rewrite([11808(5,R),11777(5),421(5),533(5)])].

given #745 (T,wt=15): 24832 f(f(x,f(y,z)),f(f(u,f(z,z)),x)) = x.  [para(402(a,1),1659(a,1,2,1)),rewrite([11808(5,R),11777(5),421(5),532(5)])].

given #746 (T,wt=15): 24861 f(f(x,f(y,z)),f(f(u,f(y,u)),x)) = x.  [para(474(a,1),1659(a,1,2,1)),rewrite([421(5),2565(5)])].

given #747 (A,wt=19): 659 f(x,f(f(y,f(z,x)),f(f(z,u),x))) = f(f(z,u),x).  [para(472(a,1),519(a,1,1))].

given #748 (T,wt=15): 24883 f(f(f(f(x,x),y),z),f(z,f(x,u))) = z.  [para(301(a,1),1663(a,1,1,1)),rewrite([421(8),505(8)])].

given #749 (T,wt=15): 24884 f(f(f(f(x,x),y),z),f(z,f(u,x))) = z.  [para(307(a,1),1663(a,1,1,1)),rewrite([421(8),503(8)])].

given #750 (T,wt=15): 24889 f(f(f(x,f(y,y)),z),f(z,f(y,u))) = z.  [para(392(a,1),1663(a,1,1,1)),rewrite([11808(8,R),11777(8),421(8),533(8)])].

given #751 (T,wt=15): 24890 f(f(f(x,f(y,y)),z),f(z,f(u,y))) = z.  [para(402(a,1),1663(a,1,1,1)),rewrite([11808(8,R),11777(8),421(8),532(8)])].

given #752 (A,wt=43): 660 f(f(x,x),f(f(y,f(f(x,x),z)),f(f(x,x),f(u,f(f(f(x,x),z),f(v,x)))))) = f(f(x,x),f(u,f(f(f(x,x),z),f(v,x)))).  [para(304(a,1),519(a,1,1))].

given #753 (T,wt=15): 24911 f(f(f(x,f(y,x)),z),f(z,f(y,u))) = z.  [para(474(a,1),1663(a,1,1,1)),rewrite([421(8),2565(8)])].

given #754 (T,wt=15): 24946 f(f(x,f(f(y,y),z)),f(f(y,u),x)) = x.  [para(301(a,1),1682(a,1,1,2)),rewrite([421(8),505(8)])].

given #755 (T,wt=15): 24947 f(f(x,f(f(y,y),z)),f(f(u,y),x)) = x.  [para(307(a,1),1682(a,1,1,2)),rewrite([421(8),503(8)])].

given #756 (T,wt=15): 24952 f(f(x,f(y,f(z,z))),f(f(z,u),x)) = x.  [para(392(a,1),1682(a,1,1,2)),rewrite([11808(8,R),11777(8),421(8),533(8)])].

given #757 (A,wt=19): 661 f(x,f(f(y,f(z,x)),f(f(u,z),x))) = f(f(u,z),x).  [para(519(a,1),519(a,1,1))].

given #758 (T,wt=15): 24953 f(f(x,f(y,f(z,z))),f(f(u,z),x)) = x.  [para(402(a,1),1682(a,1,1,2)),rewrite([11808(8,R),11777(8),421(8),532(8)])].

given #759 (T,wt=15): 24969 f(f(x,f(y,f(z,y))),f(f(z,u),x)) = x.  [para(474(a,1),1682(a,1,1,2)),rewrite([421(8),2565(8)])].

given #760 (T,wt=15): 25014 f(f(f(x,y),z),f(f(f(x,x),u),z)) = z.  [para(301(a,1),1686(a,1,2,1)),rewrite([421(5),505(5)])].

given #761 (T,wt=15): 25019 f(f(f(x,y),z),f(f(f(y,y),u),z)) = z.  [para(307(a,1),1686(a,1,2,1)),rewrite([421(5),503(5)])].

given #762 (A,wt=17): 662 f(f(x,y),f(x,f(f(f(x,y),f(z,y)),u))) = x.  [para(356(a,1),338(a,1,1))].

given #763 (T,wt=15): 25026 f(f(f(x,y),z),f(f(u,f(x,x)),z)) = z.  [para(392(a,1),1686(a,1,2,1)),rewrite([11808(5,R),11777(5),421(5),533(5)])].

given #764 (T,wt=15): 25027 f(f(f(x,y),z),f(f(u,f(y,y)),z)) = z.  [para(402(a,1),1686(a,1,2,1)),rewrite([11808(5,R),11777(5),421(5),532(5)])].

given #765 (T,wt=15): 25064 f(f(f(x,y),z),f(f(u,f(x,u)),z)) = z.  [para(474(a,1),1686(a,1,2,1)),rewrite([421(5),2565(5)])].

given #766 (T,wt=15): 25084 f(f(f(x,x),y),z) = f(z,f(y,f(y,x))).  [para(1740(a,1),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #767 (A,wt=25): 666 f(f(f(x,y),f(z,x)),f(f(x,y),f(f(f(x,y),f(u,y)),v))) = f(x,y).  [para(356(a,1),291(a,1,1,1)),rewrite([356(7),356(14)])].

given #768 (T,wt=15): 25085 f(f(x,f(x,y)),z) = f(z,f(f(y,y),x)).  [para(1740(a,2),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #769 (T,wt=15): 25441 f(f(x,f(y,y)),z) = f(z,f(x,f(y,x))).  [para(1884(a,1),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #770 (T,wt=15): 25442 f(f(x,f(y,x)),z) = f(z,f(x,f(y,y))).  [para(1884(a,2),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #771 (T,wt=15): 25646 f(f(x,f(f(y,y),z)),f(x,f(y,u))) = x.  [para(301(a,1),1898(a,1,1,2)),rewrite([421(8),505(8)])].

given #772 (A,wt=25): 667 f(f(f(x,y),f(z,x)),f(f(x,y),f(u,f(f(x,y),f(y,v))))) = f(x,y).  [para(291(a,1),356(a,1,2,1)),rewrite([291(17)])].

given #773 (T,wt=15): 25647 f(f(x,f(f(y,y),z)),f(x,f(u,y))) = x.  [para(307(a,1),1898(a,1,1,2)),rewrite([421(8),503(8)])].

given #774 (T,wt=15): 25648 f(f(x,f(y,f(z,z))),f(x,f(z,u))) = x.  [para(392(a,1),1898(a,1,1,2)),rewrite([11808(8,R),11777(8),421(8),533(8)])].

given #775 (T,wt=15): 25649 f(f(x,f(y,f(z,z))),f(x,f(u,z))) = x.  [para(402(a,1),1898(a,1,1,2)),rewrite([11808(8,R),11777(8),421(8),532(8)])].

given #776 (T,wt=15): 25652 f(f(x,f(y,f(z,y))),f(x,f(z,u))) = x.  [para(474(a,1),1898(a,1,1,2)),rewrite([421(8),2565(8)])].

given #777 (A,wt=21): 672 f(x,f(f(x,f(y,f(y,z))),f(z,z))) = f(x,f(y,f(y,z))).  [para(464(a,1),356(a,1,2,2))].

given #778 (T,wt=15): 25662 f(f(f(f(x,x),y),z),f(f(x,u),z)) = z.  [para(301(a,1),1907(a,1,1,1)),rewrite([421(8),505(8)])].

given #779 (T,wt=15): 25663 f(f(f(f(x,x),y),z),f(f(u,x),z)) = z.  [para(307(a,1),1907(a,1,1,1)),rewrite([421(8),503(8)])].

given #780 (T,wt=15): 25664 f(f(f(x,f(y,y)),z),f(f(y,u),z)) = z.  [para(392(a,1),1907(a,1,1,1)),rewrite([11808(8,R),11777(8),421(8),533(8)])].

given #781 (T,wt=15): 25665 f(f(f(x,f(y,y)),z),f(f(u,y),z)) = z.  [para(402(a,1),1907(a,1,1,1)),rewrite([11808(8,R),11777(8),421(8),532(8)])].

given #782 (A,wt=27): 673 f(f(x,x),f(f(f(x,x),y),f(z,f(f(f(x,x),y),f(x,u))))) = f(f(x,x),y).  [para(301(a,1),356(a,1,2,1)),rewrite([301(16)])].

given #783 (T,wt=15): 25673 f(f(f(x,f(y,x)),z),f(f(y,u),z)) = z.  [para(474(a,1),1907(a,1,1,1)),rewrite([421(8),2565(8)])].

given #784 (T,wt=15): 25692 f(f(f(x,x),y),z) = f(z,f(y,f(x,y))).  [para(2037(a,1),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #785 (T,wt=15): 25693 f(f(x,f(y,x)),z) = f(z,f(f(y,y),x)).  [para(2037(a,2),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #786 (T,wt=15): 26284 f(x,f(y,f(f(f(y,y),z),x))) = f(x,x).  [para(163(a,1),2946(a,1,2,1))].

given #787 (A,wt=23): 677 f(f(x,y),f(f(x,z),f(f(x,y),f(u,y)))) = f(f(x,y),f(u,y)).  [para(356(a,1),472(a,1,1))].

given #788 (T,wt=15): 26287 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x).  [para(421(a,1),2946(a,1,2,2))].

given #789 (T,wt=15): 26303 f(x,f(y,f(f(z,f(z,y)),x))) = f(x,x).  [para(1422(a,1),2946(a,1,2,2,1)),rewrite([11808(3,R),11777(3)])].

given #790 (T,wt=15): 26305 f(x,f(y,f(f(z,f(y,z)),x))) = f(x,x).  [para(1647(a,1),2946(a,1,2,2,1)),rewrite([11808(3,R),11777(3)])].

given #791 (T,wt=15): 26334 f(x,f(f(c_0,y),f(f(y,z),x))) = f(x,x).  [para(11808(a,2),2946(a,1,2,1))].

given #792 (A,wt=31): 680 f(f(f(x,x),y),f(f(x,x),f(z,f(f(x,x),f(u,f(f(f(x,x),y),f(v,x))))))) = f(x,x).  [para(304(a,1),356(a,1,2,1)),rewrite([304(23)])].

given #793 (T,wt=15): 26335 f(x,f(f(y,c_0),f(f(y,z),x))) = f(x,x).  [para(11826(a,2),2946(a,1,2,1))].

given #794 (T,wt=15): 26338 f(x,f(y,f(f(f(y,c_0),z),x))) = f(x,x).  [para(11822(a,1),2946(a,1,2,1))].

given #795 (T,wt=15): 26340 f(x,f(y,f(f(f(c_0,y),z),x))) = f(x,x).  [para(13688(a,1),2946(a,1,2,1))].

given #796 (T,wt=15): 26347 f(x,f(y,f(f(z,f(c_0,y)),x))) = f(x,x).  [para(14175(a,1),2946(a,1,2,2,1)),rewrite([11808(3,R),11777(3)])].

given #797 (A,wt=23): 682 f(f(x,y),f(f(z,x),f(f(x,y),f(u,y)))) = f(f(x,y),f(u,y)).  [para(356(a,1),519(a,1,1))].

given #798 (T,wt=15): 26350 f(x,f(y,f(f(z,f(y,c_0)),x))) = f(x,x).  [para(16335(a,1),2946(a,1,2,2,1)),rewrite([11808(3,R),11777(3)])].

given #799 (T,wt=15): 26932 f(x,f(f(y,y),f(x,f(z,y)))) = f(x,x).  [para(421(a,1),3008(a,1,2,2))].

given #800 (T,wt=15): 26983 f(x,f(f(c_0,y),f(f(z,y),x))) = f(x,x).  [para(11808(a,2),3008(a,1,2,1))].

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

given #801 (T,wt=15): 26984 f(x,f(f(y,c_0),f(f(z,y),x))) = f(x,x).  [para(11826(a,2),3008(a,1,2,1))].

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

given #803 (T,wt=15): 27235 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0.  [para(3223(a,1),11744(a,1,2,2,2)),rewrite([421(7),380(7)])].

given #804 (T,wt=15): 27586 f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)).  [para(9584(a,1),441(a,1,2)),flip(a)].

given #805 (T,wt=15): 27641 f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)).  [para(9704(a,1),441(a,1,2)),flip(a)].

given #806 (T,wt=15): 27700 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(x,y).  [para(360(a,1),10652(a,1,2)),rewrite([11808(8,R)]),flip(a)].

given #807 (A,wt=17): 685 f(f(x,y),f(x,f(f(f(x,y),f(y,z)),u))) = x.  [para(399(a,1),338(a,1,1))].

given #808 (T,wt=15): 27715 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y).  [para(1168(a,1),10652(a,1,2)),rewrite([11808(8,R)]),flip(a)].

given #809 (T,wt=15): 27716 f(x,f(c_0,f(y,f(f(y,x),z)))) = f(x,y).  [para(1169(a,1),10652(a,1,2)),rewrite([11808(8,R)]),flip(a)].

given #810 (T,wt=15): 27718 f(f(x,f(y,f(x,z))),f(c_0,f(z,x))) = c_0.  [para(10652(a,1),11741(a,1,2,2,2)),rewrite([1415(7)])].

given #811 (T,wt=15): 27771 f(x,f(c_0,f(y,f(f(x,y),z)))) = f(x,y).  [para(7868(a,1),10652(a,1,2)),rewrite([11808(8,R)]),flip(a)].

given #812 (A,wt=17): 687 f(f(x,y),f(x,f(z,f(f(x,y),f(y,u))))) = x.  [para(399(a,1),353(a,1,1))].

given #813 (T,wt=15): 27843 f(f(x,f(y,f(z,c_0))),f(c_0,f(x,z))) = c_0.  [para(11688(a,1),11741(a,1,2,2,2)),rewrite([421(8),381(8)])].

given #814 (T,wt=15): 27873 f(f(x,f(f(y,c_0),z)),f(c_0,f(x,y))) = c_0.  [para(11690(a,1),11741(a,1,2,2,2)),rewrite([421(8),381(8)])].

given #815 (T,wt=15): 28360 f(f(x,y),f(z,c_0)) = f(f(z,z),f(y,x)).  [para(421(a,1),12056(a,1,1))].

given #816 (T,wt=15): 28411 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0.  [para(12087(a,1),532(a,1,2)),rewrite([11808(10,R),11783(8),11808(12,R),11783(10),11808(8,R),353(8),11808(8,R),11783(6)]),flip(a)].

given #817 (A,wt=23): 689 f(f(x,y),f(f(f(x,y),f(y,z)),f(x,u))) = f(f(x,y),f(y,z)).  [para(399(a,1),453(a,1,1))].

given #818 (T,wt=15): 28465 f(x,f(f(y,z),f(f(z,y),x))) = f(x,x).  [para(13702(a,1),12087(a,1,2,2,2)),rewrite([11783(7),421(4)])].

given #819 (T,wt=15): 28503 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0.  [para(12088(a,1),532(a,1,2)),rewrite([11808(10,R),11783(8),11808(12,R),11783(10),11808(8,R),353(8),11808(8,R),11783(6)]),flip(a)].

given #820 (T,wt=15): 28551 f(x,f(f(x,f(y,z)),f(c_0,z))) = f(x,x).  [para(163(a,1),12089(a,1,2,2,2))].

given #821 (T,wt=15): 28552 f(x,f(f(x,f(y,z)),f(c_0,y))) = f(x,x).  [para(280(a,1),12089(a,1,2,2,2))].

given #822 (A,wt=25): 691 f(f(f(x,y),f(z,x)),f(f(x,y),f(f(f(x,y),f(y,u)),v))) = f(x,y).  [para(399(a,1),291(a,1,1,1)),rewrite([399(7),399(14)])].

given #823 (T,wt=15): 28553 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x).  [para(169(a,1),12089(a,1,2,2,2)),rewrite([11777(6),421(4)])].

given #824 (T,wt=15): 28554 f(x,f(y,f(x,f(f(y,y),z)))) = f(x,x).  [para(258(a,1),12089(a,1,2,2,2)),rewrite([11777(6),421(4)])].

given #825 (T,wt=15): 28557 f(x,f(y,f(x,f(z,f(y,z))))) = f(x,x).  [para(427(a,1),12089(a,1,2,2,2)),rewrite([11777(6),421(4)])].

given #826 (T,wt=15): 28560 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x).  [para(464(a,1),12089(a,1,2,2,2)),rewrite([11777(6),421(4)])].

given #827 (A,wt=27): 692 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(399(a,1),454(a,1,2)),rewrite([421(5),421(8)])].

given #828 (T,wt=15): 28568 f(x,f(f(x,f(y,z)),f(y,c_0))) = f(x,x).  [para(470(a,1),12089(a,1,2,2))].

given #829 (T,wt=15): 28571 f(x,f(f(x,f(y,z)),f(z,c_0))) = f(x,x).  [para(480(a,1),12089(a,1,2,2))].

given #830 (T,wt=15): 28610 f(x,f(y,f(x,f(f(y,c_0),z)))) = f(x,x).  [para(11820(a,1),12089(a,1,2,2,2)),rewrite([11777(7),421(5)])].

given #831 (T,wt=15): 28611 f(x,f(y,f(x,f(z,f(y,c_0))))) = f(x,x).  [para(11821(a,1),12089(a,1,2,2,2)),rewrite([11777(7),421(5)])].

given #832 (A,wt=27): 695 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(399(a,1),456(a,1,2)),rewrite([421(5),421(8)])].

given #833 (T,wt=15): 28612 f(x,f(y,f(x,f(z,f(c_0,y))))) = f(x,x).  [para(13697(a,1),12089(a,1,2,2,2)),rewrite([11783(8),421(5)])].

given #834 (T,wt=15): 28613 f(x,f(y,f(x,f(f(c_0,y),z)))) = f(x,x).  [para(13704(a,1),12089(a,1,2,2,2)),rewrite([11783(8),421(5)])].

given #835 (T,wt=15): 28627 f(f(x,x),f(y,f(f(z,x),f(u,x)))) = x.  [para(15389(a,1),12089(a,1,2,1)),rewrite([11783(9),11808(9,R),11777(9)])].

given #836 (T,wt=15): 28630 f(f(x,x),f(y,f(f(x,z),f(u,x)))) = x.  [para(21709(a,1),12089(a,1,2,1)),rewrite([11783(9),11808(9,R),11777(9)])].

given #837 (A,wt=27): 698 f(f(x,x),f(f(f(x,x),y),f(f(f(f(x,x),y),f(x,z)),u))) = f(f(x,x),y).  [para(301(a,1),399(a,1,2,1)),rewrite([301(16)])].

given #838 (T,wt=15): 28631 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x.  [para(21710(a,1),12089(a,1,2,1)),rewrite([11783(9),11808(9,R),11777(9)])].

given #839 (T,wt=15): 28632 f(f(x,c_0),f(y,f(f(z,x),f(u,x)))) = x.  [para(21754(a,1),12089(a,1,2,1)),rewrite([11783(10),11808(12,R),11778(11)])].

given #840 (T,wt=15): 28633 f(f(c_0,x),f(y,f(f(z,x),f(u,x)))) = x.  [para(21775(a,1),12089(a,1,2,1)),rewrite([11783(10),11808(12,R),11783(11)])].

given #841 (T,wt=15): 28634 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x.  [para(22434(a,1),12089(a,1,2,1)),rewrite([11783(9),11808(9,R),11777(9)])].

given #842 (A,wt=23): 702 f(f(x,y),f(f(x,z),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)).  [para(399(a,1),472(a,1,1))].

given #843 (T,wt=15): 28635 f(f(x,c_0),f(y,f(f(x,z),f(u,x)))) = x.  [para(22468(a,1),12089(a,1,2,1)),rewrite([11783(10),11808(12,R),11778(11)])].

given #844 (T,wt=15): 28636 f(f(c_0,x),f(y,f(f(x,z),f(u,x)))) = x.  [para(22490(a,1),12089(a,1,2,1)),rewrite([11783(10),11808(12,R),11783(11)])].

given #845 (T,wt=15): 28637 f(f(x,c_0),f(y,f(f(z,x),f(x,u)))) = x.  [para(22552(a,1),12089(a,1,2,1)),rewrite([11783(10),11808(12,R),11778(11)])].

given #846 (T,wt=15): 28638 f(f(c_0,x),f(y,f(f(z,x),f(x,u)))) = x.  [para(22570(a,1),12089(a,1,2,1)),rewrite([11783(10),11808(12,R),11783(11)])].

given #847 (A,wt=31): 705 f(f(f(x,x),y),f(f(x,x),f(f(f(x,x),f(z,f(f(f(x,x),y),f(u,x)))),v))) = f(x,x).  [para(304(a,1),399(a,1,2,1)),rewrite([304(23)])].

given #848 (T,wt=15): 28639 f(f(x,c_0),f(y,f(f(x,z),f(x,u)))) = x.  [para(22941(a,1),12089(a,1,2,1)),rewrite([11783(10),11808(12,R),11778(11)])].

given #849 (T,wt=15): 28640 f(f(c_0,x),f(y,f(f(x,z),f(x,u)))) = x.  [para(22959(a,1),12089(a,1,2,1)),rewrite([11783(10),11808(12,R),11783(11)])].

given #850 (T,wt=15): 28694 f(f(x,x),f(f(f(y,x),f(z,x)),u)) = x.  [para(15389(a,1),12090(a,1,2,1)),rewrite([11783(9),11808(9,R),11777(9)])].

given #851 (T,wt=15): 28695 f(f(x,x),f(f(f(x,y),f(z,x)),u)) = x.  [para(21709(a,1),12090(a,1,2,1)),rewrite([11783(9),11808(9,R),11777(9)])].

given #852 (A,wt=19): 708 f(x,f(f(x,y),f(z,f(f(x,y),f(y,u))))) = f(x,y).  [para(399(a,1),356(a,1,2,1)),rewrite([399(11)])].

given #853 (T,wt=15): 28696 f(f(x,x),f(f(f(y,x),f(x,z)),u)) = x.  [para(21710(a,1),12090(a,1,2,1)),rewrite([11783(9),11808(9,R),11777(9)])].

given #854 (T,wt=15): 28697 f(f(x,c_0),f(f(f(y,x),f(z,x)),u)) = x.  [para(21754(a,1),12090(a,1,2,1)),rewrite([11783(10),11808(12,R),11778(11)])].

given #855 (T,wt=15): 28698 f(f(c_0,x),f(f(f(y,x),f(z,x)),u)) = x.  [para(21775(a,1),12090(a,1,2,1)),rewrite([11783(10),11808(12,R),11783(11)])].

given #856 (T,wt=15): 28699 f(f(x,x),f(f(f(x,y),f(x,z)),u)) = x.  [para(22434(a,1),12090(a,1,2,1)),rewrite([11783(9),11808(9,R),11777(9)])].

given #857 (A,wt=19): 709 f(x,f(f(x,y),f(f(f(x,y),f(z,y)),u))) = f(x,y).  [para(356(a,1),399(a,1,2,1)),rewrite([356(11)])].

given #858 (T,wt=15): 28700 f(f(x,c_0),f(f(f(x,y),f(z,x)),u)) = x.  [para(22468(a,1),12090(a,1,2,1)),rewrite([11783(10),11808(12,R),11778(11)])].

given #859 (T,wt=15): 28701 f(f(c_0,x),f(f(f(x,y),f(z,x)),u)) = x.  [para(22490(a,1),12090(a,1,2,1)),rewrite([11783(10),11808(12,R),11783(11)])].

given #860 (T,wt=15): 28702 f(f(x,c_0),f(f(f(y,x),f(x,z)),u)) = x.  [para(22552(a,1),12090(a,1,2,1)),rewrite([11783(10),11808(12,R),11778(11)])].

given #861 (T,wt=15): 28703 f(f(c_0,x),f(f(f(y,x),f(x,z)),u)) = x.  [para(22570(a,1),12090(a,1,2,1)),rewrite([11783(10),11808(12,R),11783(11)])].

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

given #863 (T,wt=15): 28704 f(f(x,c_0),f(f(f(x,y),f(x,z)),u)) = x.  [para(22941(a,1),12090(a,1,2,1)),rewrite([11783(10),11808(12,R),11778(11)])].

given #864 (T,wt=15): 28705 f(f(c_0,x),f(f(f(x,y),f(x,z)),u)) = x.  [para(22959(a,1),12090(a,1,2,1)),rewrite([11783(10),11808(12,R),11783(11)])].

given #865 (T,wt=15): 28754 f(f(f(x,y),z),f(c_0,f(z,f(y,x)))) = c_0.  [para(12343(a,1),11741(a,1,2,2,2)),rewrite([421(8),14162(8)])].

given #866 (T,wt=15): 28823 f(f(f(x,y),z),f(z,f(u,f(y,x)))) = z.  [para(12388(a,1),355(a,1,2,1)),rewrite([421(8),21648(8),12388(13)])].

given #867 (A,wt=27): 726 f(f(x,x),f(f(f(x,x),y),f(f(f(f(x,x),y),f(z,x)),u))) = f(f(x,x),y).  [para(307(a,1),399(a,1,2,1)),rewrite([307(16)])].

given #868 (T,wt=15): 28824 f(f(f(x,y),z),f(z,f(f(y,x),u))) = z.  [para(12388(a,1),401(a,1,2,1)),rewrite([421(8),21648(8),28823(13)])].

given #869 (T,wt=15): 28914 f(f(x,f(y,z)),f(c_0,f(x,f(z,y)))) = c_0.  [para(12870(a,1),11741(a,1,2,2,2)),rewrite([421(8),14164(8,R),11783(8)])].

given #870 (T,wt=15): 28950 f(f(x,f(y,z)),f(x,f(f(z,y),u))) = x.  [para(12870(a,1),512(a,1,2,1)),rewrite([22201(8),12870(13)])].

given #871 (T,wt=15): 28991 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0.  [para(14161(a,1),13706(a,1,2,2))].

given #872 (A,wt=23): 733 f(f(x,y),f(f(f(x,y),f(x,z)),f(y,u))) = f(f(x,y),f(x,z)).  [para(470(a,1),453(a,1,1))].

given #873 (T,wt=15): 29031 f(x,f(c_0,f(y,f(y,f(f(x,x),z))))) = c_0.  [para(14161(a,1),13709(a,1,2,2))].

given #874 (T,wt=15): 29063 f(x,f(c_0,f(y,f(y,f(z,f(x,c_0)))))) = c_0.  [para(14161(a,1),13954(a,1,2,2))].

given #875 (T,wt=15): 29096 f(x,f(c_0,f(y,f(y,f(f(x,c_0),z))))) = c_0.  [para(14161(a,1),13959(a,1,2,2))].

given #876 (T,wt=15): 29132 f(x,f(c_0,f(y,f(y,f(z,f(c_0,x)))))) = c_0.  [para(14161(a,1),14128(a,1,2,2))].

given #877 (A,wt=25): 734 f(f(f(x,y),f(z,y)),f(f(x,y),f(f(f(x,y),f(x,u)),v))) = f(x,y).  [para(470(a,1),291(a,1,1,1)),rewrite([470(7),470(14)])].

given #878 (T,wt=15): 29173 f(x,f(c_0,f(y,f(y,f(f(c_0,x),z))))) = c_0.  [para(14161(a,1),14130(a,1,2,2))].

given #879 (T,wt=15): 29184 f(f(x,f(f(c_0,y),z)),f(x,f(y,u))) = x.  [para(14133(a,1),353(a,1,2,2))].

given #880 (T,wt=15): 29185 f(f(f(f(c_0,x),y),z),f(z,f(x,u))) = z.  [para(14133(a,1),455(a,1,2,2))].

given #881 (T,wt=15): 29186 f(f(x,f(f(c_0,y),z)),f(f(y,u),x)) = x.  [para(14133(a,1),456(a,1,2,1))].

given #882 (A,wt=25): 735 f(f(f(x,y),f(y,z)),f(f(x,y),f(f(f(x,y),f(u,x)),v))) = f(x,y).  [para(291(a,1),470(a,1,2,1)),rewrite([291(17)])].

given #883 (T,wt=15): 29187 f(f(f(x,y),z),f(z,f(f(c_0,x),u))) = z.  [para(14133(a,1),466(a,1,1,1))].

given #884 (T,wt=15): 29188 f(f(x,f(y,z)),f(f(f(c_0,y),u),x)) = x.  [para(14133(a,1),504(a,1,1,2))].

given #885 (T,wt=15): 29189 f(f(f(f(c_0,x),y),z),f(f(x,u),z)) = z.  [para(14133(a,1),519(a,1,2,1))].

given #886 (T,wt=15): 29203 f(f(x,f(y,f(c_0,z))),f(x,f(z,u))) = x.  [para(14133(a,1),681(a,1,2,2))].

given #887 (A,wt=27): 736 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(470(a,1),454(a,1,2)),rewrite([421(5),421(8)])].

given #888 (T,wt=15): 29214 f(f(f(x,f(c_0,y)),z),f(z,f(y,u))) = z.  [para(14133(a,1),771(a,1,2,2))].

given #889 (T,wt=15): 29215 f(f(x,f(y,z)),f(x,f(f(c_0,y),u))) = x.  [para(14133(a,1),1043(a,1,1,2))].

given #890 (T,wt=15): 29217 f(f(x,f(y,z)),f(x,f(u,f(c_0,y)))) = x.  [para(14133(a,1),1168(a,1,1,2))].

given #891 (T,wt=15): 29228 f(f(x,f(y,z)),f(f(u,f(c_0,y)),x)) = x.  [para(14133(a,1),5732(a,1,1,2))].

given #892 (A,wt=23): 737 f(f(x,y),f(f(f(x,y),f(x,z)),f(u,y))) = f(f(x,y),f(x,z)).  [para(470(a,1),455(a,1,1))].

given #893 (T,wt=15): 29261 f(f(x,f(y,f(c_0,z))),f(f(z,u),x)) = x.  [para(14140(a,1),456(a,1,2,1))].

given #894 (T,wt=15): 29262 f(f(f(x,y),z),f(z,f(u,f(c_0,x)))) = z.  [para(14140(a,1),466(a,1,1,1))].

given #895 (T,wt=15): 29263 f(f(f(x,f(c_0,y)),z),f(f(y,u),z)) = z.  [para(14140(a,1),519(a,1,2,1))].

given #896 (T,wt=15): 29308 f(f(x,f(y,f(c_0,z))),f(x,f(u,z))) = x.  [para(14144(a,1),353(a,1,2,2))].

given #897 (A,wt=27): 738 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(470(a,1),456(a,1,2)),rewrite([421(5),421(8)])].

given #898 (T,wt=15): 29309 f(f(f(x,f(c_0,y)),z),f(z,f(u,y))) = z.  [para(14144(a,1),455(a,1,2,2))].

given #899 (T,wt=15): 29310 f(f(x,f(y,f(c_0,z))),f(f(u,z),x)) = x.  [para(14144(a,1),456(a,1,2,1))].

given #900 (T,wt=15): 29311 f(f(f(x,y),z),f(z,f(u,f(c_0,y)))) = z.  [para(14144(a,1),466(a,1,1,1))].

given #901 (T,wt=15): 29312 f(f(x,f(y,z)),f(f(u,f(c_0,z)),x)) = x.  [para(14144(a,1),504(a,1,1,2))].

given #902 (A,wt=23): 741 f(f(x,y),f(f(y,z),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)).  [para(470(a,1),472(a,1,1))].

given #903 (T,wt=15): 29313 f(f(f(x,f(c_0,y)),z),f(f(u,y),z)) = z.  [para(14144(a,1),519(a,1,2,1))].

given #904 (T,wt=15): 29318 f(f(x,f(y,z)),f(x,f(f(c_0,z),u))) = x.  [para(14144(a,1),330(a,1,1,2))].

given #905 (T,wt=15): 29320 f(f(x,f(y,z)),f(x,f(u,f(c_0,z)))) = x.  [para(14144(a,1),360(a,1,1,2))].

given #906 (T,wt=15): 29329 f(f(f(f(c_0,x),y),z),f(z,f(u,x))) = z.  [para(14144(a,1),675(a,1,2,2))].

given #907 (A,wt=31): 744 f(f(f(x,x),f(y,f(f(f(x,x),z),f(u,x)))),f(f(x,x),f(f(f(x,x),z),v))) = f(x,x).  [para(304(a,1),470(a,1,2,1)),rewrite([304(23)])].

given #908 (T,wt=15): 29342 f(f(x,f(f(c_0,y),z)),f(x,f(u,y))) = x.  [para(14144(a,1),754(a,1,2,2))].

given #909 (T,wt=15): 29345 f(f(x,f(y,z)),f(f(f(c_0,z),u),x)) = x.  [para(14144(a,1),1045(a,1,1,2))].

given #910 (T,wt=15): 29373 f(f(x,f(f(c_0,y),z)),f(f(u,y),x)) = x.  [para(14145(a,1),456(a,1,2,1))].

given #911 (T,wt=15): 29374 f(f(f(x,y),z),f(z,f(f(c_0,y),u))) = z.  [para(14145(a,1),466(a,1,1,1))].

given #912 (A,wt=23): 745 f(f(x,y),f(f(z,y),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)).  [para(470(a,1),519(a,1,1))].

given #913 (T,wt=15): 29375 f(f(f(f(c_0,x),y),z),f(f(u,x),z)) = z.  [para(14145(a,1),519(a,1,2,1))].

given #914 (T,wt=15): 29750 f(f(x,y),f(c_0,z)) = f(f(z,z),f(y,x)).  [para(421(a,1),14420(a,1,1))].

given #915 (T,wt=15): 29786 f(f(x,f(y,z)),f(c_0,f(x,f(x,y)))) = c_0.  [para(421(a,1),14980(a,1,2,2,2))].

given #916 (T,wt=15): 29800 f(f(x,f(y,z)),f(c_0,f(x,f(y,y)))) = c_0.  [para(1423(a,2),14980(a,1,2,2))].

given #917 (A,wt=19): 747 f(x,f(f(y,x),f(z,f(f(y,x),f(y,u))))) = f(y,x).  [para(470(a,1),356(a,1,2,1)),rewrite([470(11)])].

given #918 (T,wt=15): 29802 f(f(x,f(f(y,y),z)),f(c_0,f(y,x))) = c_0.  [para(1647(a,1),14980(a,1,2,2,2)),rewrite([380(7)])].

given #919 (T,wt=15): 29803 f(f(x,f(y,z)),f(c_0,f(f(y,y),x))) = c_0.  [para(1647(a,2),14980(a,1,2,2))].

given #920 (T,wt=15): 29804 f(x,f(c_0,f(y,f(x,f(z,f(z,y)))))) = c_0.  [para(567(a,1),14980(a,1,1)),rewrite([11780(10,R),421(7),11777(7),421(5)])].

given #921 (T,wt=15): 29815 f(f(x,f(f(y,c_0),z)),f(c_0,f(y,x))) = c_0.  [para(11776(a,1),14980(a,1,2,2,2)),rewrite([380(8)])].

given #922 (A,wt=19): 748 f(f(f(x,y),f(z,y)),f(f(x,y),f(x,u))) = f(x,y).  [para(356(a,1),470(a,1,2,1)),rewrite([356(11)])].

given #923 (T,wt=15): 29816 f(f(x,f(y,z)),f(c_0,f(f(y,c_0),x))) = c_0.  [para(11776(a,2),14980(a,1,2,2))].

given #924 (T,wt=15): 29817 f(f(x,f(y,z)),f(c_0,f(x,f(y,c_0)))) = c_0.  [para(11780(a,2),14980(a,1,2,2))].

given #925 (T,wt=15): 29826 f(f(x,f(f(c_0,y),z)),f(c_0,f(x,y))) = c_0.  [para(14148(a,1),14980(a,1,2,2,2)),rewrite([14164(8,R),11777(8)])].

given #926 (T,wt=15): 29831 f(f(x,f(y,z)),f(c_0,f(x,f(c_0,y)))) = c_0.  [para(14164(a,2),14980(a,1,2,2))].

given #927 (A,wt=19): 749 f(x,f(f(y,x),f(f(f(y,x),f(y,z)),u))) = f(y,x).  [para(470(a,1),399(a,1,2,1)),rewrite([470(11)])].

given #928 (T,wt=15): 29833 f(f(x,f(f(c_0,y),z)),f(c_0,f(y,x))) = c_0.  [para(14165(a,1),14980(a,1,2,2,2)),rewrite([380(8)])].

given #929 (T,wt=15): 29834 f(f(x,f(y,z)),f(c_0,f(f(c_0,y),x))) = c_0.  [para(14165(a,2),14980(a,1,2,2))].

given #930 (T,wt=15): 29835 f(f(x,f(y,f(c_0,z))),f(c_0,f(x,z))) = c_0.  [para(14175(a,1),14980(a,1,1,2)),rewrite([14164(8,R),11777(8)])].

given #931 (T,wt=15): 29864 f(x,f(c_0,f(y,f(x,f(z,f(y,z)))))) = c_0.  [para(14174(a,1),14980(a,1,1)),rewrite([11780(11,R),421(8),11783(8),421(5)])].

given #932 (A,wt=19): 750 f(f(f(x,y),f(y,z)),f(f(x,y),f(x,u))) = f(x,y).  [para(399(a,1),470(a,1,2,1)),rewrite([399(11)])].

given #933 (T,wt=15): 29889 f(f(f(x,y),z),f(c_0,f(z,f(x,x)))) = c_0.  [para(1380(a,2),14984(a,1,2,2))].

given #934 (T,wt=15): 29894 f(f(f(x,y),z),f(c_0,f(f(x,x),z))) = c_0.  [para(1422(a,2),14984(a,1,2,2))].

given #935 (T,wt=15): 29908 f(f(f(x,y),z),f(c_0,f(f(x,c_0),z))) = c_0.  [para(11781(a,2),14984(a,1,2,2))].

given #936 (T,wt=15): 29910 f(f(f(f(x,c_0),y),z),f(c_0,f(z,x))) = c_0.  [para(11785(a,1),14984(a,1,2,2))].

given #937 (A,wt=25): 759 f(f(f(x,y),f(z,y)),f(f(x,y),f(f(f(x,y),f(u,x)),v))) = f(x,y).  [para(480(a,1),291(a,1,1,1)),rewrite([480(7),480(14)])].

given #938 (T,wt=15): 29913 f(f(f(x,y),z),f(c_0,f(z,f(x,c_0)))) = c_0.  [para(11786(a,2),14984(a,1,2,2))].

given #939 (T,wt=15): 29918 f(f(f(f(c_0,x),y),z),f(c_0,f(z,x))) = c_0.  [para(14148(a,2),14984(a,1,1,1)),rewrite([1415(8)])].

given #940 (T,wt=15): 29921 f(f(f(x,y),z),f(c_0,f(z,f(c_0,x)))) = c_0.  [para(14161(a,2),14984(a,1,2,2))].

given #941 (T,wt=15): 29924 f(f(f(x,y),z),f(c_0,f(f(c_0,x),z))) = c_0.  [para(14163(a,2),14984(a,1,2,2))].

given #942 (A,wt=25): 760 f(f(f(x,y),f(y,z)),f(f(x,y),f(u,f(f(x,y),f(v,x))))) = f(x,y).  [para(291(a,1),480(a,1,2,1)),rewrite([291(17)])].

given #943 (T,wt=15): 29928 f(f(f(x,f(c_0,y)),z),f(c_0,f(z,y))) = c_0.  [para(14175(a,1),14984(a,1,1,1)),rewrite([1415(8)])].

given #944 (T,wt=15): 29932 f(f(f(x,f(y,c_0)),z),f(c_0,f(z,y))) = c_0.  [para(16335(a,1),14984(a,1,1,1)),rewrite([1415(8)])].

given #945 (T,wt=15): 29954 f(f(x,f(y,z)),f(c_0,f(x,f(x,z)))) = c_0.  [para(421(a,1),14986(a,1,2,2,2))].

given #946 (T,wt=15): 29968 f(f(x,f(y,z)),f(c_0,f(x,f(z,z)))) = c_0.  [para(1423(a,2),14986(a,1,2,2))].

given #947 (A,wt=27): 761 f(f(x,f(y,z)),f(y,f(f(x,f(y,z)),f(u,x)))) = f(f(x,f(y,z)),f(u,x)).  [para(480(a,1),454(a,1,2)),rewrite([421(5),421(8)])].

given #948 (T,wt=15): 29970 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0.  [para(1647(a,1),14986(a,1,2,2,2)),rewrite([380(7)])].

given #949 (T,wt=15): 29972 f(f(x,f(y,z)),f(c_0,f(f(z,z),x))) = c_0.  [para(1647(a,2),14986(a,1,2,2))].

given #950 (T,wt=15): 29992 f(f(x,f(y,f(z,c_0))),f(c_0,f(z,x))) = c_0.  [para(11776(a,1),14986(a,1,2,2,2)),rewrite([380(8)])].

given #951 (T,wt=15): 29994 f(f(x,f(y,z)),f(c_0,f(f(z,c_0),x))) = c_0.  [para(11776(a,2),14986(a,1,2,2))].

given #952 (A,wt=23): 762 f(f(x,y),f(f(f(x,y),f(z,x)),f(u,y))) = f(f(x,y),f(z,x)).  [para(480(a,1),455(a,1,1))].

given #953 (T,wt=15): 29996 f(f(x,f(y,z)),f(c_0,f(x,f(z,c_0)))) = c_0.  [para(11780(a,2),14986(a,1,2,2))].

given #954 (T,wt=15): 30018 f(f(x,f(y,z)),f(c_0,f(x,f(c_0,z)))) = c_0.  [para(14164(a,2),14986(a,1,2,2))].

given #955 (T,wt=15): 30020 f(f(x,f(y,f(c_0,z))),f(c_0,f(z,x))) = c_0.  [para(14165(a,1),14986(a,1,2,2,2)),rewrite([380(8)])].

given #956 (T,wt=15): 30022 f(f(x,f(y,z)),f(c_0,f(f(c_0,z),x))) = c_0.  [para(14165(a,2),14986(a,1,2,2))].

given #957 (A,wt=27): 763 f(f(x,f(y,z)),f(z,f(f(x,f(y,z)),f(u,x)))) = f(f(x,f(y,z)),f(u,x)).  [para(480(a,1),456(a,1,2)),rewrite([421(5),421(8)])].

given #958 (T,wt=15): 30059 f(f(f(x,y),z),f(c_0,f(z,f(y,y)))) = c_0.  [para(1380(a,2),14988(a,1,2,2))].

given #959 (T,wt=15): 30064 f(f(f(x,y),z),f(c_0,f(f(y,y),z))) = c_0.  [para(1422(a,2),14988(a,1,2,2))].

given #960 (T,wt=15): 30068 f(f(x,f(y,f(z,x))),f(c_0,f(x,z))) = c_0.  [para(1423(a,2),14988(a,1,2,2,2)),rewrite([421(3),1415(7)])].

given #961 (T,wt=15): 30078 f(f(f(x,y),z),f(c_0,f(f(y,c_0),z))) = c_0.  [para(11781(a,2),14988(a,1,2,2))].

given #962 (A,wt=21): 765 f(x,f(f(y,y),f(f(z,f(z,y)),x))) = f(f(z,f(z,y)),x).  [para(464(a,1),480(a,1,2,2)),rewrite([421(5)])].

given #963 (T,wt=15): 30084 f(f(f(x,y),z),f(c_0,f(z,f(y,c_0)))) = c_0.  [para(11786(a,2),14988(a,1,2,2))].

given #964 (T,wt=15): 30092 f(f(f(x,y),z),f(c_0,f(z,f(c_0,y)))) = c_0.  [para(14161(a,2),14988(a,1,2,2))].

given #965 (T,wt=15): 30097 f(f(f(x,y),z),f(c_0,f(f(c_0,y),z))) = c_0.  [para(14163(a,2),14988(a,1,2,2))].

given #966 (T,wt=15): 30231 f(f(c_0,f(x,y)),z) = f(x,f(c_0,f(y,z))).  [para(14992(a,1),464(a,1,2,2)),rewrite([421(9),421(10),28533(10),28475(7),11808(17,R),11783(12)])].

given #967 (A,wt=31): 769 f(f(f(x,x),f(y,f(f(f(x,x),z),f(u,x)))),f(f(x,x),f(v,f(f(x,x),z)))) = f(x,x).  [para(304(a,1),480(a,1,2,1)),rewrite([304(23)])].

given #968 (T,wt=15): 30253 f(x,f(c_0,f(y,f(c_0,f(f(y,x),z))))) = c_0.  [para(11741(a,1),14992(a,1,1)),rewrite([30231(8),11783(12)])].

given #969 (T,wt=15): 30254 f(x,f(c_0,f(y,f(c_0,f(f(x,y),z))))) = c_0.  [para(11744(a,1),14992(a,1,1)),rewrite([30231(8),11783(12)])].

given #970 (T,wt=15): 30324 f(x,f(c_0,f(y,f(c_0,f(z,f(y,x)))))) = c_0.  [back_rewrite(29949),rewrite([30231(8),30231(9),14162(7)])].

given #971 (T,wt=15): 30481 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))).  [back_rewrite(28709),rewrite([30231(7),17173(7),30231(8)])].

given #972 (A,wt=23): 770 f(f(x,y),f(f(z,y),f(f(x,y),f(u,x)))) = f(f(x,y),f(u,x)).  [para(480(a,1),519(a,1,1))].

given #973 (T,wt=15): 30496 f(x,f(c_0,f(y,z))) = f(y,f(c_0,f(x,z))).  [back_rewrite(28533),rewrite([30231(7),17171(7),30231(8)])].

given #974 (T,wt=15): 30579 f(x,f(y,f(c_0,f(z,f(x,y))))) = f(x,x).  [back_rewrite(27617),rewrite([30231(5)])].

given #975 (T,wt=15): 30595 f(x,f(c_0,f(y,f(z,f(z,x))))) = f(x,y).  [back_rewrite(27304),rewrite([30231(9),14162(7)])].

given #976 (T,wt=15): 30601 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x).  [back_rewrite(27004),rewrite([30231(7),30231(8),14162(6)])].

given #977 (A,wt=19): 772 f(x,f(f(y,x),f(z,f(f(y,x),f(u,y))))) = f(y,x).  [para(480(a,1),356(a,1,2,1)),rewrite([480(11)])].

given #978 (T,wt=15): 30745 f(x,f(c_0,f(y,f(y,f(f(x,y),z))))) = c_0.  [back_rewrite(22430),rewrite([30231(7)])].

given #979 (T,wt=15): 30751 f(x,f(c_0,f(y,f(f(x,x),z)))) = f(x,y).  [back_rewrite(22210),rewrite([30231(6)])].

given #980 (T,wt=15): 30752 f(x,f(c_0,f(y,f(z,f(x,x))))) = f(x,y).  [back_rewrite(22209),rewrite([30231(6)])].

given #981 (T,wt=15): 30784 f(x,f(c_0,f(y,f(z,f(x,z))))) = f(x,y).  [back_rewrite(21988),rewrite([30231(6)])].

given #982 (A,wt=19): 773 f(f(f(x,y),f(z,y)),f(f(x,y),f(u,x))) = f(x,y).  [para(356(a,1),480(a,1,2,1)),rewrite([356(11)])].

given #983 (T,wt=15): 30806 f(x,f(c_0,f(y,f(y,f(z,f(x,y)))))) = c_0.  [back_rewrite(21705),rewrite([30231(7)])].

given #984 (T,wt=15): 30816 f(x,f(y,f(c_0,f(f(x,y),z)))) = f(x,x).  [back_rewrite(21469),rewrite([30231(5)])].

given #985 (T,wt=15): 30817 f(x,f(y,f(c_0,f(f(y,x),z)))) = f(x,x).  [back_rewrite(21467),rewrite([30231(5)])].

given #986 (T,wt=15): 30836 f(f(x,f(c_0,f(y,z))),f(f(y,x),z)) = z.  [back_rewrite(20960),rewrite([30231(4)])].

given #987 (A,wt=19): 774 f(x,f(f(y,x),f(f(f(y,x),f(z,y)),u))) = f(y,x).  [para(480(a,1),399(a,1,2,1)),rewrite([480(11)])].

given #988 (T,wt=15): 30841 f(x,f(c_0,f(y,f(f(x,c_0),z)))) = f(x,y).  [back_rewrite(19909),rewrite([30231(7)])].

given #989 (T,wt=15): 30842 f(x,f(c_0,f(y,f(z,f(x,c_0))))) = f(x,y).  [back_rewrite(19898),rewrite([30231(7)])].

given #990 (T,wt=15): 30856 f(x,f(c_0,f(y,f(z,f(c_0,x))))) = f(x,y).  [back_rewrite(14140),rewrite([30231(7)])].

given #991 (T,wt=15): 30857 f(x,f(c_0,f(y,f(f(c_0,x),z)))) = f(x,y).  [back_rewrite(14133),rewrite([30231(7)])].

given #992 (A,wt=19): 777 f(f(f(x,y),f(x,z)),f(f(x,y),f(u,y))) = f(x,y).  [para(470(a,1),480(a,1,2,1)),rewrite([470(11)])].

given #993 (T,wt=15): 31033 f(f(x,f(y,z)),f(z,f(c_0,f(y,x)))) = x.  [back_rewrite(12909),rewrite([30231(6)])].

given #994 (T,wt=15): 31055 f(f(x,f(c_0,f(y,z))),f(z,f(y,x))) = z.  [back_rewrite(12870),rewrite([30231(4)])].

given #995 (T,wt=15): 31533 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0.  [para(14161(a,1),15000(a,1,2,2))].

given #996 (T,wt=15): 31565 f(f(x,f(y,f(z,y))),f(c_0,f(z,x))) = c_0.  [para(421(a,1),15057(a,1,2,2))].

given #997 (A,wt=23): 782 f(f(x,y),f(f(f(y,z),f(x,y)),f(x,u))) = f(f(y,z),f(x,y)).  [para(513(a,1),453(a,1,1))].

given #998 (T,wt=15): 31657 f(f(x,f(y,z)),f(c_0,f(f(z,y),x))) = c_0.  [para(12343(a,1),15057(a,1,1)),rewrite([22201(9)])].

given #999 (T,wt=15): 31759 f(f(f(x,y),z),f(c_0,f(f(y,x),z))) = c_0.  [para(12343(a,1),15060(a,1,1)),rewrite([421(9),30231(9),27716(9)])].

given #1000 (T,wt=15): 31795 f(x,f(c_0,f(y,f(y,f(z,f(x,z)))))) = c_0.  [para(11741(a,1),15061(a,1,1)),rewrite([421(9),11783(11)])].

given #1001 (T,wt=15): 31844 f(x,f(c_0,f(y,f(c_0,f(z,f(x,y)))))) = c_0.  [para(14991(a,1),15061(a,1,1)),rewrite([421(10),11783(12)])].

given #1002 (A,wt=25): 783 f(f(f(x,y),f(z,x)),f(f(x,y),f(f(f(y,u),f(x,y)),v))) = f(x,y).  [para(513(a,1),291(a,1,1,1)),rewrite([513(7),513(14)])].

given #1003 (T,wt=15): 31900 f(x,f(c_0,f(y,f(x,f(z,f(y,c_0)))))) = c_0.  [para(11688(a,1),15062(a,1,1)),rewrite([421(6)])].

given #1004 (T,wt=15): 31902 f(x,f(c_0,f(y,f(x,f(f(y,c_0),z))))) = c_0.  [para(11690(a,1),15062(a,1,1)),rewrite([421(6)])].

given #1005 (T,wt=15): 31915 f(f(x,f(c_0,f(y,z))),f(f(x,y),z)) = z.  [para(380(a,1),15067(a,1,2,1)),rewrite([421(3),30231(4)])].

Low Water (keep, True_semantics): wt=19

given #1006 (T,wt=15): 31930 f(x,f(c_0,f(y,f(x,f(f(y,y),z))))) = c_0.  [para(15157(a,1),421(a,1)),rewrite([30231(8)]),flip(a)].

given #1007 (A,wt=27): 784 f(f(f(x,y),z),f(x,f(f(z,u),f(f(x,y),z)))) = f(f(z,u),f(f(x,y),z)).  [para(513(a,1),454(a,1,2)),rewrite([421(5),421(8)])].

given #1008 (T,wt=15): 31934 f(x,f(c_0,f(y,f(x,f(z,f(y,y)))))) = c_0.  [para(504(a,1),15157(a,1,1)),rewrite([421(5)])].

given #1009 (T,wt=15): 32065 f(x,f(c_0,f(y,f(y,f(f(y,x),z))))) = c_0.  [para(15167(a,1),15062(a,1,1)),rewrite([421(9),11783(11)])].

given #1010 (T,wt=15): 32096 f(x,f(c_0,f(y,f(y,f(z,f(y,x)))))) = c_0.  [para(15168(a,1),15062(a,1,1)),rewrite([421(9),11783(11)])].

given #1011 (T,wt=15): 32101 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))).  [para(15175(a,1),464(a,1,2,2)),rewrite([421(9),30231(10),30231(8),17171(8),17173(7),11808(17,R),11783(12)])].

given #1012 (A,wt=23): 785 f(f(x,y),f(f(f(y,z),f(x,y)),f(u,x))) = f(f(y,z),f(x,y)).  [para(513(a,1),455(a,1,1))].

given #1013 (T,wt=15): 32184 f(x,f(c_0,f(f(x,f(y,z)),f(c_0,z)))) = c_0.  [para(163(a,1),15180(a,1,2,2,2,2))].

given #1014 (T,wt=15): 32185 f(x,f(c_0,f(f(x,f(y,z)),f(c_0,y)))) = c_0.  [para(280(a,1),15180(a,1,2,2,2,2))].

given #1015 (T,wt=15): 32204 f(x,f(c_0,f(f(x,f(y,z)),f(y,c_0)))) = c_0.  [para(470(a,1),15180(a,1,2,2,2))].

given #1016 (T,wt=15): 32207 f(x,f(c_0,f(f(x,f(y,z)),f(z,c_0)))) = c_0.  [para(480(a,1),15180(a,1,2,2,2))].

given #1017 (A,wt=27): 786 f(f(f(x,y),z),f(y,f(f(z,u),f(f(x,y),z)))) = f(f(z,u),f(f(x,y),z)).  [para(513(a,1),456(a,1,2)),rewrite([421(5),421(8)])].

given #1018 (T,wt=15): 32259 f(x,f(c_0,f(y,f(x,f(z,f(c_0,y)))))) = c_0.  [para(13697(a,1),15180(a,1,2,2,2,2)),rewrite([11783(9),421(6)])].

given #1019 (T,wt=15): 32260 f(x,f(c_0,f(y,f(x,f(f(c_0,y),z))))) = c_0.  [para(13704(a,1),15180(a,1,2,2,2,2)),rewrite([11783(9),421(6)])].

given #1020 (T,wt=15): 32481 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))).  [para(584(a,1),14163(a,1,1)),rewrite([421(3),30231(4),421(10),17607(11)])].

given #1021 (T,wt=15): 32484 f(f(f(x,y),z),f(f(f(y,x),u),z)) = z.  [para(12343(a,1),584(a,1,2,2)),rewrite([421(8),30231(8),27716(8),12343(13)])].

given #1022 (A,wt=23): 788 f(f(x,y),f(f(x,z),f(f(y,u),f(x,y)))) = f(f(y,u),f(x,y)).  [para(513(a,1),472(a,1,1))].

given #1023 (T,wt=15): 32558 f(f(f(x,y),z),f(f(u,f(y,x)),z)) = z.  [para(12343(a,1),585(a,1,2,2)),rewrite([421(8),30231(8),27716(8),12343(13)])].

given #1024 (T,wt=15): 32609 f(f(f(x,c_0),y),z) = f(z,f(y,f(x,x))).  [para(15505(a,1),380(a,2)),rewrite([11780(11,R),14161(10,R),11778(7)])].

given #1025 (T,wt=15): 32610 f(f(x,f(y,y)),z) = f(z,f(f(y,c_0),x)).  [para(15505(a,2),380(a,2)),rewrite([11780(8,R),14161(8,R),11778(6)])].

given #1026 (T,wt=15): 32683 f(f(c_0,x),f(y,y)) = f(f(x,c_0),f(c_0,y)).  [para(15508(a,2),14176(a,2))].

given #1027 (A,wt=23): 790 f(f(x,y),f(f(z,x),f(f(y,u),f(x,y)))) = f(f(y,u),f(x,y)).  [para(513(a,1),519(a,1,1))].

given #1028 (T,wt=15): 32741 f(f(c_0,x),f(y,y)) = f(f(x,c_0),f(y,c_0)).  [para(15522(a,2),14176(a,2))].

given #1029 (T,wt=15): 32817 f(f(x,f(f(y,c_0),z)),f(x,f(y,u))) = x.  [para(322(a,1),15833(a,1,1,2)),rewrite([11808(12,R),11778(11),421(10),11770(10)])].

given #1030 (T,wt=15): 32818 f(f(x,f(f(y,c_0),z)),f(x,f(u,y))) = x.  [para(327(a,1),15833(a,1,1,2)),rewrite([11808(12,R),11778(11),421(10),11771(10)])].

given #1031 (T,wt=15): 32819 f(f(x,f(y,f(z,c_0))),f(x,f(z,u))) = x.  [para(392(a,1),15833(a,1,1,2)),rewrite([11808(12,R),11778(11),421(10),11765(10)])].

given #1032 (A,wt=19): 791 f(x,f(f(x,y),f(z,f(f(y,u),f(x,y))))) = f(x,y).  [para(513(a,1),356(a,1,2,1)),rewrite([513(11)])].

given #1033 (T,wt=15): 32820 f(f(x,f(y,f(z,c_0))),f(x,f(u,z))) = x.  [para(402(a,1),15833(a,1,1,2)),rewrite([11808(12,R),11778(11),421(10),11766(10)])].

given #1034 (T,wt=15): 32844 f(f(x,f(y,z)),f(x,f(f(y,c_0),u))) = x.  [para(322(a,1),15834(a,1,2,2)),rewrite([11808(8,R),11778(7),421(6),11770(6)])].

given #1035 (T,wt=15): 32845 f(f(x,f(y,z)),f(x,f(f(z,c_0),u))) = x.  [para(327(a,1),15834(a,1,2,2)),rewrite([11808(8,R),11778(7),421(6),11771(6)])].

given #1036 (T,wt=15): 32846 f(f(x,f(y,z)),f(x,f(u,f(y,c_0)))) = x.  [para(392(a,1),15834(a,1,2,2)),rewrite([11808(8,R),11778(7),421(6),11765(6)])].

given #1037 (A,wt=19): 793 f(x,f(f(x,y),f(f(f(y,z),f(x,y)),u))) = f(x,y).  [para(513(a,1),399(a,1,2,1)),rewrite([513(11)])].

given #1038 (T,wt=15): 32847 f(f(x,f(y,z)),f(x,f(u,f(z,c_0)))) = x.  [para(402(a,1),15834(a,1,2,2)),rewrite([11808(8,R),11778(7),421(6),11766(6)])].

given #1039 (T,wt=15): 32890 f(f(f(x,y),z),f(z,f(f(x,c_0),u))) = z.  [para(322(a,1),15909(a,1,2,2)),rewrite([11808(8,R),11778(7),11770(6)])].

given #1040 (T,wt=15): 32891 f(f(f(x,y),z),f(z,f(f(y,c_0),u))) = z.  [para(327(a,1),15909(a,1,2,2)),rewrite([11808(8,R),11778(7),11771(6)])].

given #1041 (T,wt=15): 32892 f(f(f(x,y),z),f(z,f(u,f(x,c_0)))) = z.  [para(392(a,1),15909(a,1,2,2)),rewrite([11808(8,R),11778(7),11765(6)])].

given #1042 (A,wt=19): 796 f(f(f(x,y),f(z,x)),f(f(z,x),f(z,u))) = f(z,x).  [para(513(a,1),470(a,1,2,1)),rewrite([513(11)])].

given #1043 (T,wt=15): 32893 f(f(f(x,y),z),f(z,f(u,f(y,c_0)))) = z.  [para(402(a,1),15909(a,1,2,2)),rewrite([11808(8,R),11778(7),11766(6)])].

given #1044 (T,wt=15): 32912 f(f(f(x,f(y,x)),z),f(z,f(u,y))) = z.  [para(521(a,1),15909(a,1,1,1)),rewrite([421(6),11777(6),2532(8)])].

given #1045 (T,wt=15): 32914 f(f(f(x,f(x,y)),z),f(z,f(y,u))) = z.  [para(558(a,1),15909(a,1,1,1)),rewrite([421(6),11777(6),2563(8)])].

given #1046 (T,wt=15): 32916 f(f(f(x,f(x,y)),z),f(z,f(u,y))) = z.  [para(564(a,1),15909(a,1,1,1)),rewrite([421(6),11777(6),2530(8)])].

given #1047 (A,wt=19): 797 f(f(f(x,y),f(z,x)),f(f(z,x),f(u,z))) = f(z,x).  [para(513(a,1),480(a,1,2,1)),rewrite([513(11)])].

given #1048 (T,wt=15): 32932 f(f(x,f(y,z)),f(f(f(y,c_0),u),x)) = x.  [para(322(a,1),15911(a,1,2,1)),rewrite([11808(8,R),11778(7),11770(6)])].

given #1049 (T,wt=15): 32933 f(f(x,f(y,z)),f(f(f(z,c_0),u),x)) = x.  [para(327(a,1),15911(a,1,2,1)),rewrite([11808(8,R),11778(7),11771(6)])].

given #1050 (T,wt=15): 32934 f(f(x,f(y,z)),f(f(u,f(y,c_0)),x)) = x.  [para(392(a,1),15911(a,1,2,1)),rewrite([11808(8,R),11778(7),11765(6)])].

given #1051 (T,wt=15): 32935 f(f(x,f(y,z)),f(f(u,f(z,c_0)),x)) = x.  [para(402(a,1),15911(a,1,2,1)),rewrite([11808(8,R),11778(7),11766(6)])].

given #1052 (A,wt=23): 802 f(f(x,y),f(f(f(z,y),f(x,y)),f(x,u))) = f(f(z,y),f(x,y)).  [para(518(a,1),453(a,1,1))].

given #1053 (T,wt=15): 32946 f(f(x,f(y,f(z,y))),f(f(u,z),x)) = x.  [para(521(a,1),15911(a,1,1,2)),rewrite([421(6),11777(6),2532(8)])].

given #1054 (T,wt=15): 32948 f(f(x,f(y,f(y,z))),f(f(z,u),x)) = x.  [para(558(a,1),15911(a,1,1,2)),rewrite([421(6),11777(6),2563(8)])].

given #1055 (T,wt=15): 32950 f(f(x,f(y,f(y,z))),f(f(u,z),x)) = x.  [para(564(a,1),15911(a,1,1,2)),rewrite([421(6),11777(6),2530(8)])].

given #1056 (T,wt=15): 32965 f(f(f(f(x,c_0),y),z),f(z,f(x,u))) = z.  [para(322(a,1),15916(a,1,1,1)),rewrite([11