============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 11562 was started by mccune on cleo.thornwood,
Sat Aug 12 21:08:40 2006
The command was "/home/mccune/bin/prover9 -f sh1.in".
============================== end of head ===========================

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

% Reading from file sh1.in

assign(new_constants,1).

formulas(sos).
f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).
f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer").
end_of_list.

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

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

% Formulas that are not ordinary clauses:

============================== end of process non-clausal formulas ===

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).  [assumption].
f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer").  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:  (no changes).

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ a, b, c, 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(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).
1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).  [assumption].
2 f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer").  [assumption].
end_of_list.

formulas(demodulators).
1 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): 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1).  [assumption].

given #2 (I,wt=43): 2 f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer").  [assumption].

given #3 (F,wt=25): 4 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(1(a,1),1(a,1,2,2))].

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

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

given #6 (A,wt=37): 3 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(1(a,1),1(a,1,1,2,1))].

given #7 (F,wt=11): 43 f(x,f(f(x,x),x)) = f(x,x).  [para(9(a,1),3(a,1,2)),rewrite(9(8)),flip(a)].

given #8 (F,wt=34): 57 f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer").  [back_rewrite(2),rewrite(49(7)),xx(a)].

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

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

given #11 (A,wt=29): 5 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(1(a,1),1(a,1,2))].

given #12 (F,wt=13): 45 f(f(x,f(f(y,x),x)),f(y,y)) = y.  [back_rewrite(40),rewrite(43(6))].

given #13 (F,wt=15): 44 f(x,f(f(x,x),f(y,f(x,x)))) = f(x,x).  [back_rewrite(42),rewrite(43(3),43(4),43(8))].

given #14 (T,wt=15): 46 f(f(x,f(f(f(y,y),x),x)),y) = f(y,y).  [back_rewrite(23),rewrite(43(3),43(8))].

given #15 (T,wt=15): 53 f(f(x,x),f(x,f(y,f(f(x,y),y)))) = x.  [para(43(a,1),9(a,1,1))].

given #16 (A,wt=31): 10 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),x)) = f(z,f(f(x,z),z)).  [para(1(a,1),4(a,1,1,2,1))].

given #17 (F,wt=17): 51 f(f(f(x,y),f(x,y)),f(f(x,y),x)) = f(x,y).  [para(43(a,1),7(a,1,1))].

given #18 (F,wt=17): 118 f(x,f(f(f(f(y,x),f(y,x)),x),x)) = f(y,x).  [para(46(a,1),5(a,1,1,2,1)),rewrite(43(7),49(7)),flip(a)].

given #19 (T,wt=9): 169 f(f(x,x),f(y,x)) = x.  [para(118(a,1),1(a,1,2)),rewrite(43(3))].

given #20 (T,wt=9): 266 f(f(x,y),f(y,y)) = y.  [back_rewrite(190),rewrite(252(4),252(7),263(7))].

given #21 (A,wt=11): 183 f(x,f(y,f(x,x))) = f(x,x).  [para(118(a,1),3(a,1,2)),rewrite(43(3),43(4),48(4),43(3),43(6))].

given #22 (F,wt=9): 277 f(f(x,x),f(x,y)) = x.  [back_rewrite(245),rewrite(271(4))].

given #23 (F,wt=9): 310 f(f(x,y),f(x,x)) = x.  [back_rewrite(91),rewrite(271(3),271(8),271(9),291(13),291(7),291(7),291(9))].

given #24 (T,wt=11): 248 f(f(x,x),x) = f(x,f(x,x)).  [para(169(a,1),10(a,1,1,1)),rewrite(169(4),43(3),171(4),184(5),171(5))].

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

given #26 (A,wt=19): 240 f(f(x,x),f(f(x,f(x,x)),f(y,x))) = f(x,f(x,x)).  [para(169(a,1),3(a,1,1,1)),rewrite(169(4),43(3),171(4),169(6),171(9))].

given #27 (F,wt=11): 261 f(x,f(f(x,x),y)) = f(x,x).  [back_rewrite(235),rewrite(250(4))].

given #28 (F,wt=11): 265 f(f(x,f(y,y)),y) = f(y,y).  [back_rewrite(191),rewrite(252(7),252(13),263(12))].

given #29 (T,wt=11): 271 f(x,f(f(y,x),x)) = f(y,x).  [back_rewrite(118),rewrite(252(4))].

given #30 (T,wt=11): 290 f(x,f(f(x,y),x)) = f(x,y).  [back_rewrite(189),rewrite(271(3),271(4),236(4),271(6))].

given #31 (A,wt=13): 252 f(f(f(x,y),f(x,y)),y) = f(x,y).  [para(169(a,1),169(a,1,2))].

given #32 (F,wt=11): 292 f(f(x,f(y,z)),f(x,z)) = x.  [back_rewrite(172),rewrite(271(6))].

given #33 (F,wt=11): 313 f(f(x,f(y,z)),f(x,y)) = x.  [back_rewrite(87),rewrite(271(3),271(4),271(6),271(6))].

given #34 (T,wt=11): 323 f(f(f(x,x),y),x) = f(x,x).  [back_rewrite(46),rewrite(271(4))].

given #35 (T,wt=11): 324 f(f(x,y),f(x,f(y,z))) = x.  [back_rewrite(39),rewrite(291(6),291(6),291(7),271(3),271(4),271(9),271(10),291(14))].

given #36 (A,wt=15): 270 f(f(x,y),f(y,f(z,f(f(x,y),y)))) = y.  [back_rewrite(166),rewrite(252(4),252(7),263(7),252(5))].

given #37 (F,wt=11): 343 f(f(x,y),f(x,f(z,y))) = x.  [back_rewrite(1),rewrite(271(3))].

given #38 (F,wt=11): 360 f(f(x,y),x) = f(x,f(x,y)).  [para(292(a,1),271(a,1,2))].

given #39 (T,wt=11): 365 f(x,f(x,f(y,x))) = f(y,x).  [back_rewrite(349),rewrite(360(3))].

given #40 (T,wt=11): 368 f(x,f(x,f(x,y))) = f(x,y).  [back_rewrite(316),rewrite(360(2),360(3))].

given #41 (A,wt=15): 278 f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)).  [back_rewrite(243),rewrite(271(6),271(5),271(10))].

% Operation f is commutative; C redundancy checks enabled.

given #42 (F,wt=34): 449 f(a,f(b,f(b,b))) != f(a,a) | f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(b,b)),f(a,f(c,c))) # answer("Sheffer").  [back_rewrite(57),rewrite(421(16),421(21)),flip(b)].

given #43 (F,wt=7): 421 f(x,y) = f(y,x).  [para(266(a,1),278(a,1,1,1,2)),rewrite(266(3),266(4))].

given #44 (T,wt=11): 429 f(x,f(y,f(x,y))) = f(x,x).  [para(313(a,1),278(a,1,1)),flip(a)].

given #45 (T,wt=11): 451 f(f(x,y),f(y,f(x,z))) = y.  [para(421(a,1),324(a,1,1))].

given #46 (A,wt=25): 294 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(116),rewrite(271(4),271(8),271(10),291(12),271(7))].

given #47 (F,wt=11): 452 f(f(x,y),f(f(y,z),x)) = x.  [para(421(a,1),324(a,1,2))].

given #48 (F,wt=11): 453 f(f(x,y),f(y,f(z,x))) = y.  [para(421(a,1),343(a,1,1))].

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

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

given #51 (A,wt=19): 297 f(f(x,x),f(f(f(x,x),y),f(x,z))) = f(f(x,x),y).  [back_rewrite(113),rewrite(271(5),271(6),271(10))].

given #52 (F,wt=11): 464 f(f(f(x,y),z),f(z,y)) = z.  [para(266(a,1),451(a,1,2,2))].

given #53 (F,wt=11): 465 f(f(f(x,y),z),f(z,x)) = z.  [para(310(a,1),451(a,1,2,2))].

given #54 (T,wt=11): 469 f(f(x,f(y,z)),f(y,x)) = x.  [para(451(a,1),421(a,1)),flip(a)].

given #55 (T,wt=11): 470 f(f(x,y),f(f(x,z),y)) = y.  [para(421(a,1),451(a,1,2))].

given #56 (A,wt=19): 301 f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y).  [back_rewrite(109),rewrite(271(5),271(10))].

given #57 (F,wt=11): 490 f(f(x,f(y,z)),f(z,x)) = x.  [para(266(a,1),452(a,1,2,1))].

given #58 (F,wt=11): 504 f(f(x,y),f(f(z,x),y)) = y.  [para(421(a,1),453(a,1,2))].

given #59 (T,wt=13): 347 f(x,f(f(x,y),f(z,y))) = f(x,y).  [back_rewrite(279),rewrite(291(6))].

given #60 (T,wt=13): 387 f(x,f(f(x,y),f(y,z))) = f(x,y).  [para(324(a,1),292(a,1,1))].

given #61 (A,wt=23): 302 f(f(x,y),f(f(f(x,y),f(z,y)),f(u,x))) = f(f(x,y),f(z,y)).  [back_rewrite(103),rewrite(271(3),271(5),271(8),271(11),271(14))].

given #62 (F,wt=13): 468 f(x,f(f(y,x),f(y,z))) = f(y,x).  [para(451(a,1),343(a,1,2)),rewrite(421(4))].

given #63 (F,wt=13): 499 f(x,f(f(y,z),f(x,y))) = f(x,y).  [para(452(a,1),451(a,1,2)),rewrite(421(4))].

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

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

given #66 (A,wt=23): 304 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,x))) = f(f(x,y),f(y,z)).  [back_rewrite(101),rewrite(271(3),271(4),271(5),271(6),271(8),271(8),271(10),271(11),271(12),271(14),271(14))].

given #67 (F,wt=13): 510 f(x,f(f(y,z),f(y,x))) = f(y,x).  [para(451(a,1),453(a,1,2)),rewrite(421(4))].

given #68 (F,wt=13): 514 f(x,f(f(y,z),f(z,x))) = f(z,x).  [para(453(a,1),453(a,1,2)),rewrite(421(4))].

given #69 (T,wt=15): 314 f(x,f(f(x,y),f(f(x,x),z))) = f(x,y).  [back_rewrite(86),rewrite(271(3),271(5),271(8))].

given #70 (T,wt=15): 317 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y).  [back_rewrite(80),rewrite(271(3),271(8))].

given #71 (A,wt=23): 306 f(f(x,y),f(f(f(x,y),f(z,y)),f(x,u))) = f(f(x,y),f(z,y)).  [back_rewrite(99),rewrite(271(3),271(5),271(8),271(7),271(11),271(14))].

given #72 (F,wt=15): 320 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x.  [back_rewrite(71),rewrite(291(6),271(9),271(9),291(10))].

given #73 (F,wt=15): 380 f(x,f(f(y,x),f(f(x,x),z))) = f(y,x).  [para(266(a,1),324(a,1,1))].

given #74 (T,wt=15): 396 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x).  [para(266(a,1),343(a,1,1))].

given #75 (T,wt=15): 424 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)).  [para(278(a,1),252(a,2)),rewrite(421(3),421(4),421(7),421(8),421(10),347(10))].

given #76 (A,wt=19): 307 f(f(f(x,y),f(z,x)),f(f(x,y),f(u,y))) = f(x,y).  [back_rewrite(98),rewrite(271(4),271(7),271(7),271(10),271(10))].

given #77 (F,wt=34): 1157 f(a,f(b,f(b,b))) != f(a,a) | f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(a,b)),f(a,f(a,c))) # answer("Sheffer").  [back_rewrite(449),rewrite(1141(27),1141(32))].

given #78 (F,wt=11): 1141 f(x,f(y,y)) = f(x,f(x,y)).  [para(462(a,1),424(a,1,2))].

given #79 (T,wt=11): 1227 f(x,f(x,f(y,y))) = f(x,y).  [para(169(a,1),1141(a,1,2)),flip(a)].

given #80 (T,wt=11): 1234 f(f(x,x),y) = f(y,f(y,x)).  [para(1141(a,1),421(a,1)),flip(a)].

given #81 (A,wt=19): 311 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,x)))))) = x.  [back_rewrite(90),rewrite(271(3),271(7),271(8),291(11),271(4))].

given #82 (F,wt=11): 1235 f(x,f(y,y)) = f(x,f(y,x)).  [para(421(a,1),1141(a,2,2))].

given #83 (F,wt=11): 1353 f(x,f(f(y,y),x)) = f(x,y).  [para(421(a,1),1227(a,1,2))].

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

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

given #86 (A,wt=21): 325 f(f(x,y),f(x,f(f(f(x,y),f(z,f(x,f(u,y)))),v))) = x.  [back_rewrite(38),rewrite(271(3),271(8),271(9),291(13),291(7),271(4),271(9),291(15))].

given #87 (F,wt=15): 442 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x.  [back_rewrite(328),rewrite(421(6))].

given #88 (F,wt=15): 445 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x.  [back_rewrite(318),rewrite(421(6))].

given #89 (T,wt=15): 459 f(f(x,f(y,f(z,y))),f(x,f(z,z))) = x.  [para(429(a,1),343(a,1,2,2))].

given #90 (T,wt=15): 489 f(x,f(f(f(x,x),y),f(z,x))) = f(z,x).  [para(266(a,1),452(a,1,1))].

given #91 (A,wt=23): 326 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(v,f(x,y)))))) = x.  [back_rewrite(37),rewrite(271(6),271(11),271(13),291(14),291(6),271(8),291(14))].

given #92 (F,wt=15): 491 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z).  [para(310(a,1),452(a,1,1))].

given #93 (F,wt=15): 507 f(f(f(x,f(y,x)),z),f(z,f(y,y))) = z.  [para(429(a,1),453(a,1,2,2))].

given #94 (T,wt=15): 515 f(x,f(f(y,f(x,x)),f(z,x))) = f(z,x).  [para(266(a,1),454(a,1,1))].

given #95 (T,wt=15): 516 f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z).  [para(310(a,1),454(a,1,1))].

given #96 (A,wt=21): 329 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,f(v,y))))))) = x.  [back_rewrite(31),rewrite(271(3),271(8),271(9),291(13),291(7),271(4),291(15))].

given #97 (F,wt=15): 521 f(f(x,f(y,f(z,y))),f(f(z,z),x)) = x.  [para(429(a,1),454(a,1,2,1))].

given #98 (F,wt=15): 527 f(x,f(y,f(f(y,z),x))) = f(f(y,z),x).  [para(452(a,1),454(a,1,2)),rewrite(421(3),421(4))].

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

given #100 (T,wt=15): 536 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x.  [para(462(a,1),343(a,1,2,2))].

given #101 (A,wt=17): 330 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y).  [back_rewrite(29),rewrite(271(3),271(5),291(6),271(3),271(4),271(6),271(9))].

given #102 (F,wt=15): 547 f(f(f(x,f(x,y)),z),f(z,f(y,y))) = z.  [para(462(a,1),453(a,1,2,2))].

given #103 (F,wt=15): 549 f(f(x,f(y,f(y,z))),f(f(z,z),x)) = x.  [para(462(a,1),454(a,1,2,1))].

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

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

given #106 (A,wt=19): 332 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)).  [back_rewrite(26),rewrite(291(4),271(6),271(6),271(12))].

given #107 (F,wt=15): 600 f(f(x,f(y,y)),f(f(z,f(y,z)),x)) = x.  [para(429(a,1),490(a,1,1,2))].

given #108 (F,wt=15): 602 f(f(x,f(y,y)),f(f(z,f(z,y)),x)) = x.  [para(462(a,1),490(a,1,1,2))].

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

given #110 (T,wt=15): 616 f(f(f(x,f(x,y)),z),f(f(y,y),z)) = z.  [para(462(a,1),504(a,1,2,1))].

given #111 (A,wt=17): 334 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y).  [back_rewrite(21),rewrite(291(6),271(3),271(6),271(9))].

given #112 (F,wt=15): 626 f(f(x,y),f(y,f(z,f(y,f(x,u))))) = y.  [para(451(a,1),347(a,1,2,1)),rewrite(451(10))].

given #113 (F,wt=15): 628 f(f(x,y),f(x,f(z,f(f(y,u),x)))) = x.  [para(452(a,1),347(a,1,2,1)),rewrite(452(10))].

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

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

given #116 (A,wt=17): 336 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y).  [back_rewrite(19),rewrite(271(3),271(5),291(6),271(3),271(4),271(9))].

given #117 (F,wt=15): 634 f(f(f(x,y),z),f(z,f(u,f(z,y)))) = z.  [para(464(a,1),347(a,1,2,1)),rewrite(464(10))].

given #118 (F,wt=15): 635 f(f(f(x,y),z),f(z,f(u,f(z,x)))) = z.  [para(465(a,1),347(a,1,2,1)),rewrite(465(10))].

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

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

given #121 (A,wt=19): 340 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)).  [back_rewrite(14),rewrite(291(4),271(6),271(12))].

given #122 (F,wt=15): 640 f(f(x,f(y,z)),f(x,f(u,f(z,x)))) = x.  [para(490(a,1),347(a,1,2,1)),rewrite(490(10))].

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

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

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

given #126 (A,wt=17): 342 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y).  [back_rewrite(3),rewrite(291(6),271(3),271(9))].

given #127 (F,wt=15): 650 f(f(x,y),f(y,f(f(y,f(x,z)),u))) = y.  [para(451(a,1),387(a,1,2,1)),rewrite(451(10))].

given #128 (F,wt=15): 653 f(f(x,y),f(x,f(f(f(y,z),x),u))) = x.  [para(452(a,1),387(a,1,2,1)),rewrite(452(10))].

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

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

given #131 (A,wt=19): 346 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)).  [back_rewrite(280),rewrite(291(4))].

given #132 (F,wt=15): 659 f(f(f(x,y),z),f(z,f(f(z,y),u))) = z.  [para(464(a,1),387(a,1,2,1)),rewrite(464(10))].

given #133 (F,wt=15): 660 f(f(f(x,y),z),f(z,f(f(z,x),u))) = z.  [para(465(a,1),387(a,1,2,1)),rewrite(465(10))].

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

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

given #136 (A,wt=19): 384 f(f(x,x),f(f(y,f(x,x)),f(x,z))) = f(y,f(x,x)).  [para(265(a,1),324(a,1,1))].

given #137 (F,wt=15): 666 f(f(x,f(y,z)),f(x,f(f(z,x),u))) = x.  [para(490(a,1),387(a,1,2,1)),rewrite(490(10))].

given #138 (F,wt=15): 668 f(f(x,y),f(y,f(f(f(z,x),y),u))) = y.  [para(504(a,1),387(a,1,2,1)),rewrite(504(10))].

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

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

given #141 (A,wt=19): 389 f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)).  [para(292(a,1),324(a,1,1))].

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

given #143 (F,wt=15): 731 f(f(f(x,y),z),f(z,f(f(y,z),u))) = z.  [para(504(a,1),468(a,1,2,1)),rewrite(504(10))].

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

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

given #146 (A,wt=19): 398 f(f(x,x),f(f(y,f(x,x)),f(z,x))) = f(y,f(x,x)).  [para(265(a,1),343(a,1,1))].

given #147 (F,wt=15): 769 f(f(f(x,y),z),f(z,f(u,f(x,z)))) = z.  [para(470(a,1),502(a,1,2,1)),rewrite(470(10))].

given #148 (F,wt=15): 773 f(f(f(x,y),z),f(z,f(u,f(y,z)))) = z.  [para(504(a,1),502(a,1,2,1)),rewrite(504(10))].

given #149 (T,wt=15): 1003 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x.  [para(365(a,1),320(a,1,2,2))].

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

given #151 (A,wt=29): 425 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(278(a,1),292(a,1,1)),rewrite(421(7),421(8),421(13))].

given #152 (F,wt=15): 1005 f(f(x,f(f(x,y),z)),f(x,f(y,u))) = x.  [para(421(a,1),320(a,1,1,2))].

given #153 (F,wt=15): 1006 f(f(x,f(y,f(x,z))),f(f(z,u),x)) = x.  [para(421(a,1),320(a,1,2))].

given #154 (T,wt=15): 1051 f(f(x,f(y,f(x,f(z,u)))),f(z,x)) = x.  [para(510(a,1),320(a,1,2))].

given #155 (T,wt=15): 1053 f(f(x,f(y,f(x,f(z,u)))),f(u,x)) = x.  [para(514(a,1),320(a,1,2))].

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

given #157 (F,wt=15): 1156 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x).  [para(320(a,1),424(a,1,2)),flip(a)].

given #158 (F,wt=15): 1230 f(f(x,f(x,y)),f(x,f(f(y,y),z))) = x.  [para(1141(a,1),324(a,1,1))].

given #159 (T,wt=15): 1231 f(f(x,f(x,y)),f(x,f(z,f(y,y)))) = x.  [para(1141(a,1),343(a,1,1))].

given #160 (T,wt=15): 1232 f(f(x,f(y,y)),f(x,f(z,f(z,y)))) = x.  [para(1141(a,1),343(a,1,2,2))].

given #161 (A,wt=29): 427 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(278(a,1),313(a,1,1)),rewrite(421(7),421(8),421(13))].

given #162 (F,wt=15): 1233 f(f(x,f(y,z)),f(x,f(y,f(z,z)))) = x.  [para(1141(a,2),343(a,1,2,2))].

given #163 (F,wt=23): 8903 f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(a,b)),f(a,f(a,c))) # answer("Sheffer").  [back_unit_del(1157),unit_del(a,8902)].

given #164 (T,wt=11): 8902 f(x,f(y,f(y,y))) = f(x,x).  [para(1233(a,1),1233(a,1,2)),rewrite(421(2),421(6),343(6),421(3)),flip(a)].

NOTE: New constant: f(x,f(x,x)) = c_0.  [new_symbol(8933)].
NOTE: New Function symbol precedence:  lex([ a, b, c, c_0, f ]).

given #165 (T,wt=7): 9064 f(x,f(x,x)) = c_0.  [new_symbol(8933)].

given #166 (A,wt=25): 428 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(278(a,1),313(a,1,2)),rewrite(421(3),421(8),421(11))].

given #167 (F,wt=19): 9066 f(f(a,f(a,b)),f(a,f(a,c))) != f(c_0,f(a,f(b,c))) # answer("Sheffer").  [back_rewrite(9061),rewrite(9064(7),421(7)),flip(a)].

given #168 (F,wt=7): 9154 f(c_0,f(x,x)) = x.  [back_rewrite(8962),rewrite(9064(2))].

given #169 (T,wt=7): 9156 f(c_0,f(x,c_0)) = x.  [back_rewrite(8960),rewrite(9064(2),9064(3))].

given #170 (T,wt=7): 9160 f(f(c_0,c_0),x) = c_0.  [back_rewrite(8955),rewrite(9064(2),9064(3),9064(6))].

given #171 (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(278(a,1),278(a,1,1,1)),rewrite(421(4),421(8),421(13),421(15),424(15))].

given #172 (F,wt=7): 9162 f(c_0,f(c_0,x)) = x.  [back_rewrite(8953),rewrite(9064(2),9064(3))].

given #173 (F,wt=7): 9164 f(x,f(c_0,c_0)) = c_0.  [back_rewrite(8951),rewrite(9064(2),9064(3),9064(6))].

given #174 (T,wt=7): 9188 f(c_0,x) = f(x,x).  [back_rewrite(8918),rewrite(9064(2),9064(4),9064(5),9164(6),421(4),9154(4))].

given #175 (T,wt=7): 9198 f(x,c_0) = f(x,x).  [back_rewrite(8902),rewrite(9064(2))].

given #176 (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(322),rewrite(421(5),421(8))].

given #177 (F,wt=7): 10575 f(x,f(x,c_0)) = c_0.  [para(9064(a,1),368(a,1,2,2)),rewrite(9064(5))].

given #178 (F,wt=7): 10617 f(x,f(c_0,x)) = c_0.  [para(9154(a,1),324(a,1,2)),rewrite(421(3))].

given #179 (T,wt=9): 9193 f(f(x,y),f(x,c_0)) = x.  [back_rewrite(8911),rewrite(9064(3))].

given #180 (T,wt=9): 9194 f(f(x,c_0),f(x,y)) = x.  [back_rewrite(8910),rewrite(9064(2))].

given #181 (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(319),rewrite(421(5),421(8))].

given #182 (F,wt=9): 9196 f(f(x,y),f(y,c_0)) = y.  [back_rewrite(8908),rewrite(9064(3))].

given #183 (F,wt=9): 9197 f(f(x,c_0),f(y,x)) = x.  [back_rewrite(8905),rewrite(9064(2))].

given #184 (T,wt=9): 10577 f(f(x,y),f(c_0,x)) = x.  [para(9064(a,1),452(a,1,2,1))].

given #185 (T,wt=9): 10578 f(f(c_0,x),f(x,y)) = x.  [para(9064(a,1),465(a,1,1,1))].

given #186 (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(303),rewrite(421(5),421(11))].

given #187 (F,wt=9): 10579 f(f(x,y),f(c_0,y)) = y.  [para(9064(a,1),470(a,1,2,1))].

given #188 (F,wt=9): 10618 f(f(c_0,x),f(y,x)) = x.  [para(9154(a,1),470(a,1,2,1))].

given #189 (T,wt=11): 9122 f(x,f(c_0,f(y,f(y,x)))) = c_0.  [back_rewrite(8997),rewrite(9064(4),421(4),9064(7))].

given #190 (T,wt=11): 9125 f(x,f(c_0,f(y,f(x,y)))) = c_0.  [back_rewrite(8994),rewrite(9064(4),421(4),9064(7))].

given #191 (A,wt=17): 466 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x).  [para(451(a,1),324(a,1,1))].

given #192 (F,wt=11): 9141 f(f(x,c_0),y) = f(y,f(x,x)).  [back_rewrite(8977),rewrite(9064(2))].

given #193 (F,wt=11): 9155 f(f(x,c_0),y) = f(y,f(x,y)).  [back_rewrite(8961),rewrite(9064(2))].

given #194 (T,wt=11): 9158 f(x,f(y,c_0)) = f(x,f(y,x)).  [back_rewrite(8958),rewrite(9064(2))].

given #195 (T,wt=11): 9161 f(f(x,c_0),y) = f(y,f(y,x)).  [back_rewrite(8954),rewrite(9064(2))].

given #196 (A,wt=17): 467 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x).  [para(451(a,1),343(a,1,1))].

given #197 (F,wt=11): 9163 f(x,f(x,f(y,c_0))) = f(x,y).  [back_rewrite(8952),rewrite(9064(2))].

given #198 (F,wt=11): 9165 f(x,f(y,c_0)) = f(x,f(x,y)).  [back_rewrite(8950),rewrite(9064(2))].

given #199 (T,wt=11): 9166 f(x,f(y,c_0)) = f(x,f(y,y)).  [back_rewrite(8949),rewrite(9064(2))].

given #200 (T,wt=11): 9174 f(x,f(c_0,f(y,x))) = f(y,x).  [back_rewrite(8941),rewrite(9064(3),421(3))].

given #201 (A,wt=19): 472 f(f(x,x),f(f(y,f(x,y)),f(x,z))) = f(y,f(x,y)).  [para(429(a,1),451(a,1,1))].

given #202 (F,wt=11): 9175 f(x,f(c_0,f(x,y))) = f(x,y).  [back_rewrite(8939),rewrite(9064(3),421(3))].

given #203 (F,wt=11): 9177 f(f(x,x),f(c_0,f(y,x))) = c_0.  [back_rewrite(8936),rewrite(9064(4),421(4),9064(7))].

given #204 (T,wt=11): 9182 f(f(x,x),f(c_0,f(x,y))) = c_0.  [back_rewrite(8929),rewrite(9064(4),421(4),9064(7))].

given #205 (T,wt=11): 9184 f(f(x,c_0),y) = f(f(x,x),y).  [back_rewrite(8925),rewrite(9064(2))].

given #206 (A,wt=19): 473 f(x,f(f(x,f(y,z)),f(f(y,x),u))) = f(x,f(y,z)).  [para(451(a,1),451(a,1,1))].

given #207 (F,wt=11): 9192 f(x,f(f(x,c_0),y)) = f(x,x).  [back_rewrite(8912),rewrite(9064(2))].

given #208 (F,wt=11): 9195 f(x,f(y,f(x,c_0))) = f(x,x).  [back_rewrite(8909),rewrite(9064(2))].

given #209 (T,wt=11): 10580 f(x,f(c_0,f(y,f(x,x)))) = c_0.  [para(9064(a,1),347(a,1,2,1)),rewrite(9064(7))].

given #210 (T,wt=11): 10581 f(x,f(c_0,f(f(x,x),y))) = c_0.  [para(9064(a,1),387(a,1,2,1)),rewrite(9064(7))].

given #211 (A,wt=33): 477 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(294(a,1),324(a,1,1))].

given #212 (F,wt=11): 10589 f(x,f(y,f(c_0,x))) = f(c_0,x).  [para(9064(a,1),527(a,1,2,2,1)),rewrite(9064(6))].

given #213 (F,wt=11): 10619 f(x,f(f(c_0,x),y)) = f(c_0,x).  [para(9154(a,1),468(a,1,2,2))].

given #214 (T,wt=11): 10621 f(x,f(c_0,f(y,f(x,c_0)))) = c_0.  [para(9154(a,1),311(a,1,1)),rewrite(9154(4),9164(5))].

given #215 (T,wt=11): 10635 f(x,f(c_0,f(f(x,c_0),y))) = c_0.  [para(9154(a,1),661(a,1,1))].

low water: id=7367, wt=37

low water: id=7485, wt=35

given #216 (A,wt=33): 478 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(294(a,1),343(a,1,1))].

given #217 (F,wt=11): 10636 f(x,f(c_0,f(f(c_0,x),y))) = c_0.  [para(9154(a,1),715(a,1,1))].

given #218 (F,wt=11): 10718 f(f(c_0,x),y) = f(f(x,x),y).  [para(9188(a,2),297(a,2,1)),rewrite(297(6)),flip(a)].

low water: id=10102, wt=33

low water: id=11161, wt=31

given #219 (T,wt=11): 10726 f(x,f(c_0,y)) = f(x,f(y,y)).  [para(9188(a,1),424(a,1,2,2,2)),rewrite(183(3)),flip(a)].

given #220 (T,wt=11): 10727 f(x,f(c_0,y)) = f(x,f(x,y)).  [para(9188(a,2),1141(a,1,2))].

given #221 (A,wt=27): 479 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(294(a,1),343(a,1,2)),rewrite(421(10))].

given #222 (F,wt=11): 10728 f(x,f(x,f(c_0,y))) = f(x,y).  [para(9188(a,2),1227(a,1,2,2))].

given #223 (F,wt=11): 10729 f(f(c_0,x),y) = f(y,f(y,x)).  [para(9188(a,2),1234(a,1,1))].

given #224 (T,wt=11): 10731 f(x,f(c_0,y)) = f(x,f(y,x)).  [para(9188(a,2),1235(a,1,2))].

low water: id=12122, wt=29

given #225 (T,wt=11): 10732 f(f(c_0,x),y) = f(y,f(x,y)).  [para(9188(a,2),1373(a,1,1))].

low water: id=12136, wt=27

given #226 (A,wt=25): 480 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(365(a,1),294(a,1,1)),rewrite(365(9))].

given #227 (F,wt=11): 10748 f(f(x,x),y) = f(y,f(c_0,x)).  [para(9188(a,2),527(a,1,2,2,1)),rewrite(10619(4)),flip(a)].

given #228 (F,wt=11): 10749 f(f(c_0,x),y) = f(y,f(x,x)).  [para(9188(a,2),527(a,2,1)),rewrite(261(3)),flip(a)].

given #229 (T,wt=11): 11467 f(f(x,y),f(c_0,f(y,x))) = c_0.  [para(1235(a,2),9122(a,1,2,2,2)),rewrite(1227(5))].

given #230 (T,wt=11): 12437 f(f(x,x),y) = f(y,f(x,c_0)).  [para(9158(a,2),1373(a,2))].

given #231 (A,wt=25): 481 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),294(a,1,1))].

given #232 (F,wt=11): 14280 f(f(c_0,f(x,y)),f(y,x)) = c_0.  [para(10731(a,1),1233(a,1)),rewrite(10948(9),421(7),324(7))].

given #233 (F,wt=13): 9269 f(f(x,x),f(y,f(c_0,f(z,x)))) = x.  [back_rewrite(2502),rewrite(9064(3))].

given #234 (T,wt=13): 10667 f(f(x,y),f(y,x)) = f(c_0,f(x,y)).  [para(387(a,1),433(a,1,2)),rewrite(502(4),9188(3,R)),flip(a)].

given #235 (T,wt=13): 10693 f(f(x,x),f(f(y,x),f(z,x))) = c_0.  [para(433(a,1),9064(a,1,2)),rewrite(421(8),1235(8,R),421(5))].

given #236 (A,wt=25): 482 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),294(a,1,2,2,2,1))].

given #237 (F,wt=13): 10700 f(f(c_0,x),f(f(c_0,f(x,y)),z)) = x.  [para(330(a,1),9162(a,1,2)),rewrite(9162(4)),flip(a)].

given #238 (F,wt=13): 10703 f(f(c_0,x),f(f(c_0,f(y,x)),z)) = x.  [para(334(a,1),9162(a,1,2)),rewrite(9162(4)),flip(a)].

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

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

given #241 (A,wt=25): 483 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(421(a,1),294(a,1,2,2,2,2))].

given #242 (F,wt=13): 11746 f(f(x,c_0),f(f(c_0,f(x,y)),z)) = x.  [para(466(a,1),9162(a,1,2)),rewrite(9156(4)),flip(a)].

given #243 (F,wt=13): 12853 f(f(x,c_0),f(y,f(c_0,f(x,z)))) = x.  [para(467(a,1),9162(a,1,2)),rewrite(9156(4)),flip(a)].

given #244 (T,wt=13): 13131 f(f(x,f(c_0,f(y,z))),f(y,c_0)) = y.  [para(467(a,1),9174(a,1,2)),rewrite(12853(14))].

given #245 (T,wt=13): 14055 f(f(x,c_0),f(y,f(c_0,f(z,x)))) = x.  [para(629(a,1),10728(a,1,2)),rewrite(421(4),9156(4)),flip(a)].

given #246 (A,wt=25): 484 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),294(a,1,2,2,2))].

given #247 (F,wt=13): 14059 f(f(x,c_0),f(f(c_0,f(y,x)),z)) = x.  [para(654(a,1),10728(a,1,2)),rewrite(421(4),9156(4)),flip(a)].

given #248 (F,wt=13): 14517 f(f(x,x),f(y,f(c_0,f(x,z)))) = x.  [para(421(a,1),9269(a,1,2,2,2))].

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

given #250 (T,wt=13): 14577 f(f(x,x),f(y,f(y,f(z,x)))) = x.  [para(10727(a,1),9269(a,1,2))].

given #251 (A,wt=25): 485 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),294(a,1,2,2))].

given #252 (F,wt=13): 14584 f(f(x,f(c_0,f(y,z))),f(z,c_0)) = z.  [para(9269(a,1),12437(a,1)),flip(a)].

given #253 (F,wt=13): 14654 f(f(x,x),f(f(x,y),f(z,x))) = c_0.  [para(421(a,1),10693(a,1,2,1))].

given #254 (T,wt=13): 14655 f(f(x,x),f(f(y,x),f(x,z))) = c_0.  [para(421(a,1),10693(a,1,2,2))].

given #255 (T,wt=13): 14685 f(f(x,c_0),f(f(y,x),f(z,x))) = c_0.  [para(10693(a,1),527(a,1,2,2)),rewrite(421(6),10693(11))].

given #256 (A,wt=43): 488 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(294(a,1),451(a,1,1))].

given #257 (F,wt=13): 14690 f(f(c_0,x),f(f(y,x),f(z,x))) = c_0.  [para(9188(a,2),10693(a,1,1))].

given #258 (F,wt=13): 14744 f(f(x,x),f(f(c_0,f(x,y)),z)) = x.  [para(10700(a,1),365(a,1,2,2)),rewrite(421(9),1235(10,R),421(6),10700(13))].

given #259 (T,wt=13): 14780 f(f(c_0,x),f(y,f(y,f(x,z)))) = x.  [para(10729(a,1),10700(a,1,2))].

given #260 (T,wt=13): 14829 f(f(c_0,x),f(y,f(y,f(z,x)))) = x.  [para(10729(a,1),10703(a,1,2))].

given #261 (A,wt=17): 492 f(x,f(f(x,y),f(f(f(y,z),x),u))) = f(x,y).  [para(452(a,1),324(a,1,1))].

given #262 (F,wt=13): 14860 f(f(x,c_0),f(y,f(y,f(x,z)))) = x.  [para(10729(a,1),11746(a,1,2))].

given #263 (F,wt=13): 14865 f(f(x,f(x,f(y,z))),f(y,c_0)) = y.  [para(10727(a,1),13131(a,1,1))].

given #264 (T,wt=13): 14867 f(f(x,c_0),f(y,f(y,f(z,x)))) = x.  [para(10727(a,1),14055(a,1,2))].

given #265 (T,wt=13): 14877 f(f(x,x),f(y,f(y,f(x,z)))) = x.  [para(10727(a,1),14517(a,1,2))].

low water: id=13112, wt=25

given #266 (A,wt=17): 493 f(x,f(f(x,y),f(z,f(f(y,u),x)))) = f(x,y).  [para(452(a,1),343(a,1,1))].

given #267 (F,wt=13): 14887 f(f(x,f(x,f(y,z))),f(z,z)) = z.  [para(14577(a,1),365(a,1,2,2)),rewrite(421(7),1235(8,R),14577(10))].

given #268 (F,wt=13): 14962 f(f(x,f(x,f(y,z))),f(c_0,z)) = z.  [para(14577(a,1),9174(a,1,2,2)),rewrite(14577(11))].

given #269 (T,wt=13): 14972 f(f(x,f(x,f(y,z))),f(z,c_0)) = z.  [para(14577(a,1),12437(a,1)),flip(a)].

given #270 (T,wt=13): 14997 f(f(x,x),f(f(x,y),f(x,z))) = c_0.  [para(421(a,1),14654(a,1,2,2))].

given #271 (A,wt=19): 498 f(x,f(f(f(y,z),x),f(f(x,y),u))) = f(f(y,z),x).  [para(452(a,1),451(a,1,1))].

given #272 (F,wt=13): 15019 f(f(x,c_0),f(f(x,y),f(z,x))) = c_0.  [para(14654(a,1),527(a,1,2,2)),rewrite(421(6),14654(11))].

given #273 (F,wt=13): 15023 f(f(c_0,x),f(f(x,y),f(z,x))) = c_0.  [para(9188(a,2),14654(a,1,1))].

given #274 (T,wt=13): 15065 f(f(x,c_0),f(f(y,x),f(x,z))) = c_0.  [para(14655(a,1),527(a,1,2,2)),rewrite(421(6),14655(11))].

given #275 (T,wt=13): 15069 f(f(c_0,x),f(f(y,x),f(x,z))) = c_0.  [para(9188(a,2),14655(a,1,1))].

given #276 (A,wt=17): 500 f(x,f(f(y,x),f(f(x,f(z,y)),u))) = f(y,x).  [para(453(a,1),324(a,1,1))].

given #277 (F,wt=13): 15102 f(f(x,f(x,f(y,z))),f(y,y)) = y.  [para(14780(a,1),365(a,1,2,2)),rewrite(421(7),1235(8,R),14780(11))].

given #278 (F,wt=13): 15103 f(f(x,f(x,f(y,z))),f(c_0,y)) = y.  [para(14780(a,1),421(a,1)),flip(a)].

given #279 (T,wt=13): 15246 f(f(x,c_0),f(f(x,y),f(x,z))) = c_0.  [para(14997(a,1),527(a,1,2,2)),rewrite(421(6),14997(11))].

given #280 (T,wt=13): 15250 f(f(c_0,x),f(f(x,y),f(x,z))) = c_0.  [para(9188(a,2),14997(a,1,1))].

given #281 (A,wt=17): 501 f(x,f(f(y,x),f(z,f(x,f(u,y))))) = f(y,x).  [para(453(a,1),343(a,1,1))].

given #282 (F,wt=15): 1247 f(f(x,f(x,y)),f(f(f(y,y),z),x)) = x.  [para(1141(a,1),452(a,1,1))].

given #283 (F,wt=15): 1253 f(f(f(x,y),z),f(z,f(x,f(y,y)))) = z.  [para(1141(a,2),453(a,1,2,2))].

given #284 (T,wt=15): 1255 f(f(x,f(x,y)),f(f(z,f(y,y)),x)) = x.  [para(1141(a,1),454(a,1,1))].

given #285 (T,wt=15): 1257 f(f(x,f(y,z)),f(f(y,f(z,z)),x)) = x.  [para(1141(a,2),454(a,1,2,1))].

given #286 (A,wt=19): 506 f(f(x,x),f(f(y,f(x,y)),f(z,x))) = f(y,f(x,y)).  [para(429(a,1),453(a,1,1))].

given #287 (F,wt=15): 1262 f(f(f(x,f(y,y)),z),f(z,f(z,y))) = z.  [para(1141(a,1),464(a,1,2))].

given #288 (F,wt=15): 1263 f(f(f(x,f(y,y)),z),f(z,f(x,y))) = z.  [para(1141(a,2),464(a,1,1,1))].

given #289 (T,wt=15): 1266 f(f(f(f(x,x),y),z),f(z,f(z,x))) = z.  [para(1141(a,1),465(a,1,2))].

given #290 (T,wt=15): 1273 f(x,f(f(x,y),f(z,f(z,x)))) = f(x,y).  [para(1141(a,1),301(a,1,2,2)),rewrite(277(3),277(3),277(8))].

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

given #292 (F,wt=15): 1276 f(f(x,f(y,f(z,z))),f(f(y,z),x)) = x.  [para(1141(a,2),490(a,1,1,2))].

given #293 (F,wt=15): 1279 f(f(f(x,x),y),f(f(z,f(z,x)),y)) = y.  [para(1141(a,1),504(a,1,2,1))].

given #294 (T,wt=15): 1282 f(f(f(x,y),z),f(f(x,f(y,y)),z)) = z.  [para(1141(a,2),504(a,1,2,1))].

given #295 (T,wt=15): 1338 f(x,f(f(y,x),f(z,f(z,x)))) = f(y,x).  [para(1141(a,1),396(a,1,2,2))].

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

given #297 (F,wt=15): 1340 f(x,f(y,f(z,z))) = f(x,f(y,f(y,z))).  [para(1141(a,1),424(a,1,2,2,2)),rewrite(793(6)),flip(a)].

low water: id=13875, wt=23

given #298 (F,wt=15): 1372 f(f(x,f(y,z)),f(x,f(f(z,z),y))) = x.  [para(1234(a,2),343(a,1,2,2))].

given #299 (T,wt=15): 1383 f(f(f(x,y),z),f(z,f(f(y,y),x))) = z.  [para(1234(a,2),453(a,1,2,2))].

given #300 (T,wt=15): 1384 f(f(x,f(y,z)),f(f(f(z,z),y),x)) = x.  [para(1234(a,2),454(a,1,2,1))].

given #301 (A,wt=43): 511 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(294(a,1),453(a,1,1))].

given #302 (F,wt=15): 1388 f(f(f(f(x,x),y),z),f(z,f(y,x))) = z.  [para(1234(a,2),464(a,1,1,1))].

given #303 (F,wt=15): 1395 f(f(x,f(f(y,y),z)),f(x,f(x,y))) = x.  [para(1234(a,1),469(a,1,2))].

given #304 (T,wt=15): 1402 f(f(x,f(y,f(z,z))),f(x,f(x,z))) = x.  [para(1234(a,1),490(a,1,2))].

given #305 (T,wt=15): 1403 f(f(x,f(f(y,y),z)),f(f(z,y),x)) = x.  [para(1234(a,2),490(a,1,1,2))].

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

given #307 (F,wt=15): 1407 f(f(f(x,y),z),f(f(f(y,y),x),z)) = z.  [para(1234(a,2),504(a,1,2,1))].

given #308 (F,wt=15): 1450 f(x,f(f(y,y),z)) = f(x,f(z,f(z,y))).  [para(1234(a,1),424(a,1,2,2,2)),rewrite(441(5)),flip(a)].

given #309 (T,wt=15): 1538 f(x,f(f(x,y),f(z,f(x,z)))) = f(x,y).  [para(1235(a,1),301(a,1,2,2)),rewrite(277(3),277(3),277(8))].

given #310 (T,wt=15): 1612 f(x,f(f(y,x),f(z,f(x,z)))) = f(y,x).  [para(1235(a,1),396(a,1,2,2))].

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

given #312 (F,wt=15): 1615 f(x,f(y,f(z,z))) = f(x,f(y,f(z,y))).  [para(1235(a,1),424(a,1,2,2,2)),rewrite(787(6)),flip(a)].

given #313 (F,wt=15): 1635 f(f(x,f(f(y,y),z)),f(x,f(z,y))) = x.  [para(1353(a,1),343(a,1,2,2))].

given #314 (T,wt=15): 1643 f(f(f(f(x,x),y),z),f(f(y,x),z)) = z.  [para(1353(a,1),504(a,1,2,1))].

given #315 (T,wt=15): 1752 f(x,f(f(y,y),z)) = f(x,f(z,f(y,z))).  [para(1373(a,1),424(a,1,2,2,2)),rewrite(441(5)),flip(a)].

given #316 (A,wt=17): 517 f(x,f(f(x,y),f(f(f(z,y),x),u))) = f(x,y).  [para(454(a,1),324(a,1,1))].

given #317 (F,wt=15): 2193 f(x,f(f(y,f(y,x)),f(z,x))) = f(z,x).  [para(1234(a,1),489(a,1,2,1))].

given #318 (F,wt=15): 2195 f(x,f(f(y,f(x,y)),f(z,x))) = f(z,x).  [para(1373(a,1),489(a,1,2,1))].

given #319 (T,wt=15): 2357 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z).  [para(1234(a,1),491(a,1,2,1))].

given #320 (T,wt=15): 2359 f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z).  [para(1373(a,1),491(a,1,2,1))].

given #321 (A,wt=17): 518 f(x,f(f(x,y),f(z,f(f(u,y),x)))) = f(x,y).  [para(454(a,1),343(a,1,1))].

given #322 (F,wt=15): 2765 f(x,f(f(y,y),f(f(y,z),x))) = f(x,x).  [para(527(a,1),429(a,1,2,2)),rewrite(421(6),1235(6,R),421(4))].

given #323 (F,wt=15): 2794 f(f(x,f(y,y)),z) = f(f(x,f(x,y)),z).  [para(1141(a,1),527(a,1,2,2,1)),rewrite(527(5)),flip(a)].

given #324 (T,wt=15): 2796 f(f(f(x,x),y),z) = f(f(y,f(y,x)),z).  [para(1234(a,1),527(a,1,2,2,1)),rewrite(766(6)),flip(a)].

given #325 (T,wt=15): 2798 f(f(x,f(y,y)),z) = f(f(x,f(y,x)),z).  [para(1235(a,1),527(a,1,2,2,1)),rewrite(527(5)),flip(a)].

given #326 (A,wt=19): 523 f(x,f(f(f(y,z),x),f(f(x,z),u))) = f(f(y,z),x).  [para(454(a,1),451(a,1,1))].

given #327 (F,wt=15): 2803 f(f(f(x,x),y),z) = f(f(y,f(x,y)),z).  [para(1373(a,1),527(a,1,2,2,1)),rewrite(759(6)),flip(a)].

given #328 (F,wt=15): 2826 f(x,f(f(y,y),f(f(z,y),x))) = f(x,x).  [para(531(a,1),429(a,1,2,2)),rewrite(421(6),1235(6,R),421(4))].

given #329 (T,wt=15): 2850 f(f(x,f(y,f(x,z))),f(f(u,z),x)) = x.  [para(531(a,1),320(a,1,2))].

given #330 (T,wt=15): 2924 f(f(x,f(y,f(y,z))),f(x,f(x,z))) = x.  [para(1141(a,1),536(a,1,2))].

given #331 (A,wt=17): 524 f(x,f(f(y,f(x,f(z,u))),f(z,x))) = f(z,x).  [para(451(a,1),454(a,1,1))].

given #332 (F,wt=15): 2929 f(f(x,f(y,f(y,z))),f(x,f(z,x))) = x.  [para(1235(a,1),536(a,1,2))].

given #333 (F,wt=15): 3113 f(f(f(x,f(x,y)),z),f(z,f(z,y))) = z.  [para(1141(a,1),547(a,1,2))].

given #334 (T,wt=15): 3121 f(f(f(x,f(x,y)),z),f(z,f(y,z))) = z.  [para(1235(a,1),547(a,1,2))].

given #335 (T,wt=15): 3368 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x.  [para(1234(a,1),567(a,1,1))].

given #336 (A,wt=37): 525 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(294(a,1),454(a,1,2)),rewrite(421(8),421(10))].

given #337 (F,wt=15): 3374 f(f(x,f(y,x)),f(x,f(z,f(z,y)))) = x.  [para(1373(a,1),567(a,1,1))].

given #338 (F,wt=15): 3614 f(f(x,f(x,y)),f(f(z,f(z,y)),x)) = x.  [para(1141(a,1),602(a,1,1))].

given #339 (T,wt=15): 3619 f(f(x,f(y,x)),f(f(z,f(z,y)),x)) = x.  [para(1235(a,1),602(a,1,1))].

given #340 (T,wt=15): 5009 f(f(x,f(y,f(z,x))),f(f(z,u),x)) = x.  [para(636(a,1),531(a,1,2,2)),rewrite(636(12))].

given #341 (A,wt=17): 526 f(x,f(f(y,f(f(z,u),x)),f(x,z))) = f(x,z).  [para(452(a,1),454(a,1,1))].

given #342 (F,wt=15): 5304 f(f(x,f(y,f(z,x))),f(x,f(u,z))) = x.  [para(640(a,1),421(a,1)),flip(a)].

given #343 (F,wt=15): 5393 f(f(x,f(y,f(z,x))),f(f(u,z),x)) = x.  [para(640(a,1),531(a,1,2,2)),rewrite(640(12))].

given #344 (T,wt=15): 6589 f(f(x,f(f(x,y),z)),f(x,f(u,y))) = x.  [para(346(a,1),635(a,1,2)),rewrite(421(3))].

given #345 (T,wt=15): 6612 f(f(x,f(f(x,y),z)),f(f(u,y),x)) = x.  [para(659(a,1),421(a,1)),flip(a)].

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

given #347 (F,wt=15): 6785 f(f(x,f(f(x,y),z)),f(f(y,u),x)) = x.  [para(660(a,1),421(a,1)),flip(a)].

given #348 (F,wt=15): 6948 f(f(x,f(f(y,x),z)),f(x,f(y,u))) = x.  [para(661(a,1),421(a,1)),flip(a)].

given #349 (T,wt=15): 7010 f(f(x,f(f(y,x),z)),f(f(y,u),x)) = x.  [para(661(a,1),531(a,1,2,2)),rewrite(661(12))].

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

given #351 (A,wt=17): 529 f(x,f(f(y,f(x,f(z,u))),f(u,x))) = f(u,x).  [para(453(a,1),454(a,1,1))].

given #352 (F,wt=15): 7255 f(f(x,f(f(y,x),z)),f(f(u,y),x)) = x.  [para(666(a,1),531(a,1,2,2)),rewrite(666(12))].

given #353 (F,wt=15): 8208 f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x).  [para(1004(a,1),424(a,1,2)),flip(a)].

given #354 (T,wt=15): 8279 f(x,f(y,f(x,f(f(x,y),z)))) = f(x,x).  [para(1005(a,1),424(a,1,2)),flip(a)].

given #355 (T,wt=15): 8556 f(x,f(y,f(z,f(y,x)))) = f(x,f(y,y)).  [para(1156(a,1),441(a,1,2)),flip(a)].

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

given #357 (F,wt=15): 9067 f(f(x,f(y,z)),f(x,f(y,f(z,c_0)))) = x.  [back_rewrite(9060),rewrite(9064(4))].

given #358 (F,wt=15): 9070 f(f(x,f(y,c_0)),f(x,f(z,f(z,y)))) = x.  [back_rewrite(9057),rewrite(9064(2))].

given #359 (T,wt=15): 9071 f(f(x,f(x,y)),f(x,f(z,f(y,c_0)))) = x.  [back_rewrite(9056),rewrite(9064(4))].

given #360 (T,wt=15): 9073 f(f(x,f(x,y)),f(x,f(f(y,c_0),z))) = x.  [back_rewrite(9054),rewrite(9064(4))].

given #361 (A,wt=19): 540 f(f(x,x),f(f(y,f(y,x)),f(x,z))) = f(y,f(y,x)).  [para(462(a,1),451(a,1,1))].

given #362 (F,wt=15): 9099 f(f(x,x),f(c_0,f(f(c_0,f(y,x)),z))) = c_0.  [back_rewrite(9028),rewrite(9064(3),9064(5),421(5),9064(10))].

given #363 (F,wt=15): 9104 f(f(x,x),f(c_0,f(f(c_0,f(x,y)),z))) = c_0.  [back_rewrite(9022),rewrite(9064(3),9064(5),421(5),9064(10))].

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

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

given #366 (A,wt=19): 546 f(f(x,x),f(f(y,f(y,x)),f(z,x))) = f(y,f(y,x)).  [para(462(a,1),453(a,1,1))].

given #367 (F,wt=15): 9121 f(f(f(x,f(x,y)),z),f(f(y,c_0),z)) = z.  [back_rewrite(8998),rewrite(9064(5))].

given #368 (F,wt=15): 9126 f(f(x,f(y,c_0)),f(f(z,f(z,y)),x)) = x.  [back_rewrite(8993),rewrite(9064(2))].

given #369 (T,wt=15): 9132 f(f(f(x,c_0),y),f(y,f(z,f(z,x)))) = y.  [back_rewrite(8987),rewrite(9064(2))].

given #370 (T,wt=15): 9136 f(f(x,f(y,f(y,z))),f(f(z,c_0),x)) = x.  [back_rewrite(8983),rewrite(9064(5))].

given #371 (A,wt=25): 556 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(297(a,1),324(a,1,1))].

given #372 (F,wt=15): 9138 f(f(f(x,f(x,y)),z),f(z,f(y,c_0))) = z.  [back_rewrite(8980),rewrite(9064(5))].

given #373 (F,wt=15): 9139 f(f(x,f(y,f(y,z))),f(x,f(z,c_0))) = x.  [back_rewrite(8979),rewrite(9064(5))].

given #374 (T,wt=15): 9145 f(x,f(f(y,f(x,c_0)),f(x,z))) = f(x,z).  [back_rewrite(8972),rewrite(9064(2))].

given #375 (T,wt=15): 9146 f(x,f(f(y,f(x,c_0)),f(z,x))) = f(z,x).  [back_rewrite(8971),rewrite(9064(2))].

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

given #377 (F,wt=15): 9149 f(x,f(f(f(x,c_0),y),f(x,z))) = f(x,z).  [back_rewrite(8968),rewrite(9064(2))].

given #378 (F,wt=15): 9152 f(x,f(f(f(x,c_0),y),f(z,x))) = f(z,x).  [back_rewrite(8965),rewrite(9064(2))].

given #379 (T,wt=15): 9168 f(x,f(f(y,x),f(z,f(x,c_0)))) = f(y,x).  [back_rewrite(8947),rewrite(9064(3))].

given #380 (T,wt=15): 9169 f(x,f(f(y,x),f(f(x,c_0),z))) = f(y,x).  [back_rewrite(8946),rewrite(9064(3))].

given #381 (A,wt=31): 559 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(297(a,1),451(a,1,1))].

given #382 (F,wt=15): 9170 f(x,f(f(x,y),f(z,f(x,c_0)))) = f(x,y).  [back_rewrite(8945),rewrite(9064(3))].

given #383 (F,wt=15): 9171 f(x,f(f(x,y),f(f(x,c_0),z))) = f(x,y).  [back_rewrite(8944),rewrite(9064(3))].

given #384 (T,wt=15): 9220 f(x,f(f(y,f(x,x)),f(z,f(x,x)))) = c_0.  [back_rewrite(8564),rewrite(9064(8))].

given #385 (T,wt=15): 9221 f(x,f(f(f(x,x),y),f(z,f(x,x)))) = c_0.  [back_rewrite(8561),rewrite(9064(8))].

given #386 (A,wt=31): 561 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(297(a,1),453(a,1,1))].

given #387 (F,wt=15): 9267 f(x,f(f(c_0,f(y,f(x,x))),z)) = f(x,x).  [back_rewrite(2526),rewrite(9064(2))].

given #388 (F,wt=15): 9268 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,x).  [back_rewrite(2523),rewrite(9064(2))].

given #389 (T,wt=15): 9368 f(f(f(x,x),y),f(c_0,f(z,x))) = f(z,x).  [back_rewrite(2524),rewrite(9158(7,R),421(5))].

given #390 (T,wt=15): 9369 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y).  [back_rewrite(2492),rewrite(9158(7,R),421(5))].

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

given #392 (F,wt=15): 9375 f(f(f(x,x),y),f(c_0,f(x,z))) = f(x,z).  [back_rewrite(2358),rewrite(9158(7,R),421(5))].

given #393 (F,wt=15): 9377 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z).  [back_rewrite(2194),rewrite(9158(7,R),421(5))].

given #394 (T,wt=15): 9387 f(f(x,x),f(y,c_0)) = f(f(y,y),f(x,c_0)).  [back_rewrite(1767),rewrite(9158(4,R),9158(8,R))].

given #395 (T,wt=15): 9388 f(f(x,y),f(z,c_0)) = f(f(z,z),f(x,y)).  [back_rewrite(1755),rewrite(9158(4,R))].

given #396 (A,wt=19): 566 f(x,f(f(y,f(x,z)),f(f(u,z),x))) = f(f(u,z),x).  [para(464(a,1),454(a,1,1))].

given #397 (F,wt=15): 9414 f(x,f(f(y,x),f(c_0,f(z,y)))) = f(x,x).  [back_rewrite(880),rewrite(9158(5,R),421(4))].

given #398 (F,wt=15): 9415 f(x,f(f(y,x),f(c_0,f(y,z)))) = f(x,x).  [back_rewrite(851),rewrite(9158(5,R),421(4))].

given #399 (T,wt=15): 9416 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x).  [back_rewrite(786),rewrite(9158(5,R),421(4))].

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

given #401 (A,wt=19): 570 f(x,f(f(f(x,y),z),f(f(y,u),x))) = f(f(y,u),x).  [para(465(a,1),452(a,1,1))].

given #402 (F,wt=15): 9599 f(f(x,f(c_0,f(y,z))),f(f(z,y),x)) = x.  [back_rewrite(3621),rewrite(9188(3,R))].

given #403 (F,wt=15): 9650 f(f(x,f(y,z)),f(x,f(c_0,f(z,y)))) = x.  [back_rewrite(2930),rewrite(9188(5,R))].

given #404 (T,wt=15): 9925 f(f(f(c_0,f(x,y)),z),f(z,f(y,x))) = z.  [back_rewrite(3372),rewrite(9188(3,R))].

given #405 (T,wt=15): 9958 f(f(x,f(y,z)),f(f(c_0,f(z,y)),x)) = x.  [back_rewrite(3223),rewrite(9188(5,R))].

given #406 (A,wt=19): 571 f(x,f(f(y,f(x,z)),f(f(z,u),x))) = f(f(z,u),x).  [para(465(a,1),454(a,1,1))].

given #407 (F,wt=15): 10623 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0.  [para(9154(a,1),442(a,1,1))].

given #408 (F,wt=15): 10624 f(x,f(c_0,f(y,f(c_0,f(f(x,x),z))))) = c_0.  [para(9154(a,1),445(a,1,1))].

given #409 (T,wt=15): 10632 f(x,f(c_0,f(f(c_0,f(f(x,x),y)),z))) = c_0.  [para(9154(a,1),645(a,1,1))].

given #410 (T,wt=15): 10633 f(x,f(c_0,f(f(c_0,f(y,f(x,x))),z))) = c_0.  [para(9154(a,1),647(a,1,1))].

given #411 (A,wt=19): 573 f(x,f(f(f(y,x),z),f(x,f(y,u)))) = f(x,f(y,u)).  [para(469(a,1),452(a,1,1))].

given #412 (F,wt=15): 10641 f(x,f(c_0,f(y,f(c_0,f(z,f(x,c_0)))))) = c_0.  [para(9156(a,1),442(a,1,1))].

given #413 (F,wt=15): 10642 f(x,f(c_0,f(y,f(c_0,f(f(x,c_0),z))))) = c_0.  [para(9156(a,1),445(a,1,1))].

given #414 (T,wt=15): 10648 f(x,f(c_0,f(f(c_0,f(f(x,c_0),y)),z))) = c_0.  [para(9156(a,1),645(a,1,1))].

given #415 (T,wt=15): 10649 f(x,f(c_0,f(f(c_0,f(y,f(x,c_0))),z))) = c_0.  [para(9156(a,1),647(a,1,1))].

given #416 (A,wt=19): 574 f(x,f(f(y,f(z,x)),f(x,f(z,u)))) = f(x,f(z,u)).  [para(469(a,1),454(a,1,1))].

given #417 (F,wt=15): 10695 f(x,f(c_0,f(y,f(c_0,f(z,f(c_0,x)))))) = c_0.  [para(9162(a,1),442(a,1,1))].

given #418 (F,wt=15): 10696 f(x,f(c_0,f(y,f(c_0,f(f(c_0,x),z))))) = c_0.  [para(9162(a,1),445(a,1,1))].

low water: id=16783, wt=21

given #419 (T,wt=15): 10701 f(f(c_0,f(x,y)),f(f(c_0,x),z)) = f(x,y).  [para(332(a,1),9162(a,1,2)),rewrite(9162(5)),flip(a)].

given #420 (T,wt=15): 10706 f(f(c_0,f(x,y)),f(z,f(c_0,x))) = f(x,y).  [para(340(a,1),9162(a,1,2)),rewrite(9162(5)),flip(a)].

given #421 (A,wt=19): 575 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)).  [para(183(a,1),470(a,1,1))].

given #422 (F,wt=15): 10707 f(x,f(c_0,f(f(c_0,f(f(c_0,x),y)),z))) = c_0.  [para(9162(a,1),645(a,1,1))].

given #423 (F,wt=15): 10708 f(x,f(c_0,f(f(c_0,f(y,f(c_0,x))),z))) = c_0.  [para(9162(a,1),647(a,1,1))].

given #424 (T,wt=15): 10711 f(f(c_0,f(x,y)),f(z,f(c_0,y))) = f(x,y).  [para(346(a,1),9162(a,1,2)),rewrite(9162(5)),flip(a)].

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

given #426 (A,wt=17): 576 f(x,f(f(y,x),f(f(f(y,z),x),u))) = f(y,x).  [para(470(a,1),324(a,1,1))].

given #427 (F,wt=15): 10722 f(x,f(f(x,y),f(f(c_0,x),z))) = f(x,y).  [para(9188(a,2),314(a,1,2,2,1))].

given #428 (F,wt=15): 10723 f(x,f(f(x,y),f(z,f(c_0,x)))) = f(x,y).  [para(9188(a,2),317(a,1,2,2,2))].

given #429 (T,wt=15): 10724 f(x,f(f(y,x),f(f(c_0,x),z))) = f(y,x).  [para(9188(a,2),380(a,1,2,2,1))].

given #430 (T,wt=15): 10725 f(x,f(f(y,x),f(z,f(c_0,x)))) = f(y,x).  [para(9188(a,2),396(a,1,2,2,2))].

given #431 (A,wt=19): 577 f(x,f(f(f(x,y),z),f(x,f(y,u)))) = f(x,f(y,u)).  [para(324(a,1),470(a,1,1))].

given #432 (F,wt=15): 10736 f(x,f(f(f(c_0,x),y),f(z,x))) = f(z,x).  [para(9188(a,2),489(a,1,2,1,1))].

given #433 (F,wt=15): 10742 f(x,f(f(f(c_0,x),y),f(x,z))) = f(x,z).  [para(9188(a,2),491(a,1,2,1,1))].

given #434 (T,wt=15): 10744 f(x,f(f(y,f(c_0,x)),f(z,x))) = f(z,x).  [para(9188(a,2),515(a,1,2,1,2))].

given #435 (T,wt=15): 10745 f(x,f(f(y,f(c_0,x)),f(x,z))) = f(x,z).  [para(9188(a,2),516(a,1,2,1,2))].

given #436 (A,wt=17): 578 f(x,f(f(y,x),f(z,f(f(y,u),x)))) = f(y,x).  [para(470(a,1),343(a,1,1))].

given #437 (F,wt=15): 10751 f(f(x,f(y,f(y,z))),f(x,f(c_0,z))) = x.  [para(9188(a,2),536(a,1,2,2))].

given #438 (F,wt=15): 10752 f(f(f(x,f(x,y)),z),f(z,f(c_0,y))) = z.  [para(9188(a,2),547(a,1,2,2))].

given #439 (T,wt=15): 10753 f(f(x,f(y,f(y,z))),f(f(c_0,z),x)) = x.  [para(9188(a,2),549(a,1,2,1))].

given #440 (T,wt=15): 10755 f(f(f(c_0,x),y),f(y,f(z,f(z,x)))) = y.  [para(9188(a,2),567(a,1,1,1))].

given #441 (A,wt=19): 579 f(x,f(f(f(x,y),z),f(x,f(u,y)))) = f(x,f(u,y)).  [para(343(a,1),470(a,1,1))].

given #442 (F,wt=15): 10759 f(f(x,f(c_0,y)),f(f(z,f(z,y)),x)) = x.  [para(9188(a,2),602(a,1,1,2))].

given #443 (F,wt=15): 10761 f(f(f(x,f(x,y)),z),f(f(c_0,y),z)) = z.  [para(9188(a,2),616(a,1,2,1))].

given #444 (T,wt=15): 10778 f(f(x,f(c_0,y)),f(x,f(z,f(z,y)))) = x.  [para(9188(a,2),1232(a,1,1,2))].

given #445 (T,wt=15): 10813 f(f(x,x),f(c_0,y)) = f(f(y,y),f(x,c_0)).  [back_rewrite(9401),rewrite(10727(4,R))].

given #446 (A,wt=19): 581 f(f(x,x),f(f(x,y),f(z,f(x,z)))) = f(z,f(x,z)).  [para(429(a,1),470(a,1,1))].

given #447 (F,wt=15): 10956 f(f(x,x),f(c_0,y)) = f(f(y,y),f(c_0,x)).  [back_rewrite(1461),rewrite(10727(4,R),10727(8,R))].

given #448 (F,wt=15): 10958 f(f(x,y),f(c_0,z)) = f(f(z,z),f(x,y)).  [back_rewrite(1453),rewrite(10727(4,R))].

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

given #450 (T,wt=15): 11418 f(f(x,f(y,z)),f(c_0,f(x,f(x,z)))) = c_0.  [para(343(a,1),9122(a,1,2,2,2)),rewrite(421(5))].

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

given #452 (F,wt=15): 11420 f(f(x,f(y,z)),f(c_0,f(x,f(y,x)))) = c_0.  [para(451(a,1),9122(a,1,2,2,2)),rewrite(421(5))].

given #453 (F,wt=15): 11423 f(f(f(x,y),z),f(c_0,f(z,f(z,x)))) = c_0.  [para(452(a,1),9122(a,1,2,2,2)),rewrite(421(5))].

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

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

given #456 (A,wt=43): 583 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(294(a,1),470(a,1,1))].

given #457 (F,wt=15): 11430 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0.  [para(464(a,1),9122(a,1,2,2,2)),rewrite(421(5),10731(5,R))].

given #458 (F,wt=15): 11431 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0.  [para(465(a,1),9122(a,1,2,2,2)),rewrite(421(5),10731(5,R))].

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

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

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

given #462 (F,wt=15): 11436 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0.  [para(490(a,1),9122(a,1,2,2,2)),rewrite(421(5))].

given #463 (F,wt=15): 11438 f(f(f(x,y),z),f(c_0,f(z,f(y,z)))) = c_0.  [para(504(a,1),9122(a,1,2,2,2)),rewrite(421(5))].

given #464 (T,wt=15): 11439 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0.  [para(9122(a,1),347(a,1,2,1)),rewrite(9122(13))].

given #465 (T,wt=15): 11492 f(f(x,f(y,f(z,y))),f(c_0,f(x,z))) = c_0.  [para(563(a,1),9122(a,1,2,2,2)),rewrite(421(7),10731(7,R),9154(7))].

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

given #467 (F,wt=15): 11493 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0.  [para(567(a,1),9122(a,1,2,2,2)),rewrite(421(7),10731(7,R),9154(7))].

given #468 (F,wt=15): 11496 f(f(f(x,f(y,x)),z),f(c_0,f(z,y))) = c_0.  [para(600(a,1),9122(a,1,2,2,2)),rewrite(421(7),1227(7))].

given #469 (T,wt=15): 11497 f(f(f(x,f(x,y)),z),f(c_0,f(z,y))) = c_0.  [para(602(a,1),9122(a,1,2,2,2)),rewrite(421(7),1227(7))].

given #470 (T,wt=15): 11500 f(f(f(x,c_0),y),f(f(z,f(z,x)),y)) = y.  [para(9122(a,1),616(a,1,1,1,2)),rewrite(9188(12,R),9162(9))].

given #471 (A,wt=19): 587 f(f(x,x),f(f(x,y),f(z,f(z,x)))) = f(z,f(z,x)).  [para(462(a,1),470(a,1,1))].

given #472 (F,wt=15): 11563 f(f(x,f(f(y,y),z)),f(c_0,f(x,y))) = c_0.  [para(1230(a,1),9122(a,1,2,2,2)),rewrite(421(7),368(7))].

given #473 (F,wt=15): 11564 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0.  [para(1231(a,1),9122(a,1,2,2,2)),rewrite(421(7),368(7))].

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

given #475 (T,wt=15): 11574 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0.  [para(343(a,1),9125(a,1,2,2,2)),rewrite(421(5))].

given #476 (A,wt=19): 589 f(x,f(f(f(y,x),z),f(f(y,u),x))) = f(f(y,u),x).  [para(470(a,1),470(a,1,1))].

given #477 (F,wt=15): 11580 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0.  [para(470(a,1),9125(a,1,2,2,2)),rewrite(421(5),10731(5,R))].

given #478 (F,wt=15): 11582 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0.  [para(504(a,1),9125(a,1,2,2,2)),rewrite(421(5),10731(5,R))].

given #479 (T,wt=15): 11583 f(x,f(c_0,f(y,f(c_0,f(z,f(x,z)))))) = c_0.  [para(9125(a,1),347(a,1,2,1)),rewrite(9125(13))].

given #480 (T,wt=15): 11584 f(x,f(c_0,f(f(x,y),f(c_0,f(z,y))))) = c_0.  [para(347(a,1),9125(a,1,2,2,2)),rewrite(421(6),10727(6,R))].

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

given #482 (F,wt=15): 11586 f(x,f(c_0,f(f(x,y),f(c_0,f(y,z))))) = c_0.  [para(387(a,1),9125(a,1,2,2,2)),rewrite(421(6),10727(6,R))].

given #483 (F,wt=15): 11590 f(x,f(c_0,f(f(y,x),f(c_0,f(y,z))))) = c_0.  [para(468(a,1),9125(a,1,2,2,2)),rewrite(421(6),10727(6,R))].

given #484 (T,wt=15): 11592 f(x,f(c_0,f(f(y,x),f(c_0,f(z,y))))) = c_0.  [para(502(a,1),9125(a,1,2,2,2)),rewrite(421(6),10727(6,R))].

given #485 (T,wt=15): 11612 f(x,f(c_0,f(f(y,y),f(f(z,y),x)))) = c_0.  [para(531(a,1),9125(a,1,2,2,2)),rewrite(421(7),1235(7,R),421(5))].

given #486 (A,wt=31): 593 f(f(f(x,x),y),f(f(f(f(x,x),y),f(z,x)),f(f(x,x),u))) = f(f(f(x,x),y),f(z,x)).  [para(301(a,1),451(a,1,1))].

given #487 (F,wt=15): 11758 f(f(x,f(y,y)),f(x,f(f(y,c_0),z))) = x.  [para(9141(a,2),343(a,1,2,2))].

given #488 (F,wt=15): 11769 f(f(x,f(y,y)),f(x,f(z,f(y,c_0)))) = x.  [para(9141(a,1),453(a,1,1))].

given #489 (T,wt=15): 11772 f(f(f(x,x),y),f(y,f(f(x,c_0),z))) = y.  [para(9141(a,2),453(a,1,2,2))].

given #490 (T,wt=15): 11774 f(f(x,f(y,y)),f(f(f(y,c_0),z),x)) = x.  [para(9141(a,2),454(a,1,2,1))].

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

given #492 (F,wt=15): 11777 f(f(f(f(x,c_0),y),z),f(z,f(x,x))) = z.  [para(9141(a,2),464(a,1,1,1))].

given #493 (F,wt=15): 11786 f(f(x,f(y,f(z,c_0))),f(x,f(z,z))) = x.  [para(9141(a,1),490(a,1,2))].

given #494 (T,wt=15): 11787 f(f(x,f(f(y,c_0),z)),f(f(y,y),x)) = x.  [para(9141(a,2),490(a,1,1,2))].

given #495 (T,wt=15): 11789 f(f(x,f(y,y)),f(f(z,f(y,c_0)),x)) = x.  [para(9141(a,1),504(a,1,1))].

given #496 (A,wt=19): 601 f(x,f(f(y,f(z,x)),f(x,f(u,z)))) = f(x,f(u,z)).  [para(490(a,1),454(a,1,1))].

given #497 (F,wt=15): 11790 f(f(f(x,x),y),f(f(f(x,c_0),z),y)) = y.  [para(9141(a,2),504(a,1,2,1))].

given #498 (F,wt=15): 11813 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(c_0,x)).  [para(9141(a,1),304(a,1,2,1)),rewrite(9091(9))].

given #499 (T,wt=15): 11824 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,y))).  [para(9141(a,1),424(a,1,2,2,2)),rewrite(441(5)),flip(a)].

given #500 (T,wt=15): 11833 f(f(x,c_0),f(c_0,y)) = f(f(y,y),f(x,x)).  [para(9141(a,1),1141(a,1)),rewrite(10727(9,R)),flip(a)].

given #501 (A,wt=17): 604 f(x,f(f(y,x),f(f(f(z,y),x),u))) = f(y,x).  [para(504(a,1),324(a,1,1))].

given #502 (F,wt=15): 11838 f(f(x,c_0),f(y,y)) = f(f(x,x),f(c_0,y)).  [para(9141(a,2),1234(a,1)),rewrite(10727(8,R))].

given #503 (F,wt=15): 11846 f(f(x,c_0),f(y,c_0)) = f(f(y,y),f(x,x)).  [para(9141(a,1),1235(a,1)),rewrite(9158(9,R)),flip(a)].

given #504 (T,wt=15): 11848 f(f(x,c_0),f(y,y)) = f(f(x,x),f(y,c_0)).  [para(9141(a,2),1373(a,1)),rewrite(9158(8,R))].

given #505 (T,wt=15): 11893 f(f(f(x,c_0),y),z) = f(f(y,f(x,x)),z).  [para(9141(a,2),527(a,1,2,2,1)),rewrite(531(6))].

given #506 (A,wt=19): 605 f(x,f(f(y,f(x,z)),f(x,f(z,u)))) = f(x,f(z,u)).  [para(324(a,1),504(a,1,1))].

given #507 (F,wt=15): 12128 f(f(x,f(f(y,c_0),z)),f(x,f(z,y))) = x.  [para(9141(a,2),1233(a,1,1,2)),rewrite(9188(7,R),9154(7))].

given #508 (F,wt=15): 12129 f(f(x,f(y,z)),f(x,f(f(z,c_0),y))) = x.  [para(9141(a,2),1233(a,1,2,2))].

given #509 (T,wt=15): 12142 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(y,y)).  [para(9141(a,2),9141(a,1))].

given #510 (T,wt=15): 12156 f(f(f(x,y),z),f(z,f(f(x,c_0),y))) = z.  [para(9155(a,2),453(a,1,2,2))].

given #511 (A,wt=17): 606 f(x,f(f(y,x),f(z,f(f(u,y),x)))) = f(y,x).  [para(504(a,1),343(a,1,1))].

given #512 (F,wt=15): 12158 f(f(x,f(y,z)),f(f(f(y,c_0),z),x)) = x.  [para(9155(a,2),454(a,1,2,1))].

given #513 (F,wt=15): 12163 f(f(f(f(x,c_0),y),z),f(z,f(x,y))) = z.  [para(9155(a,2),464(a,1,1,1))].

given #514 (T,wt=15): 12175 f(f(x,f(f(y,c_0),z)),f(f(y,z),x)) = x.  [para(9155(a,2),490(a,1,1,2))].

given #515 (T,wt=15): 12180 f(f(f(x,y),z),f(f(f(x,c_0),y),z)) = z.  [para(9155(a,2),504(a,1,2,1))].

given #516 (A,wt=19): 607 f(x,f(f(y,f(x,z)),f(x,f(u,z)))) = f(x,f(u,z)).  [para(343(a,1),504(a,1,1))].

given #517 (F,wt=15): 12230 f(x,f(f(y,c_0),z)) = f(x,f(z,f(y,z))).  [para(9155(a,1),424(a,1,2,2,2)),rewrite(441(5)),flip(a)].

given #518 (F,wt=15): 12253 f(f(f(x,c_0),y),z) = f(f(y,f(x,y)),z).  [para(9155(a,2),527(a,1,2,2,1)),rewrite(531(6))].

given #519 (T,wt=15): 12377 f(f(x,f(c_0,f(y,z))),f(x,f(z,y))) = x.  [para(9155(a,2),1232(a,1,2,2,2)),rewrite(9188(3,R),10731(8,R),9156(8))].

given #520 (T,wt=15): 12391 f(f(x,c_0),f(y,y)) = f(f(y,c_0),f(x,x)).  [back_rewrite(12149),rewrite(12232(5))].

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

given #522 (F,wt=15): 12434 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,y))).  [para(9158(a,1),424(a,2,2)),rewrite(424(8))].

given #523 (F,wt=15): 12445 f(f(x,f(y,c_0)),z) = f(f(x,f(y,x)),z).  [para(9158(a,1),527(a,1,2,2,1)),rewrite(527(5)),flip(a)].

given #524 (T,wt=15): 12453 f(f(f(x,f(y,c_0)),z),f(f(y,y),z)) = z.  [para(9158(a,2),610(a,1,1,1))].

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

given #526 (A,wt=43): 612 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(294(a,1),504(a,1,1))].

given #527 (F,wt=15): 12631 f(f(f(x,c_0),y),z) = f(f(y,f(y,x)),z).  [para(9161(a,2),527(a,1,2,2,1)),rewrite(531(6))].

given #528 (F,wt=15): 12810 f(f(x,c_0),f(y,c_0)) = f(f(x,x),f(c_0,y)).  [para(9161(a,1),9141(a,2)),rewrite(10727(9,R))].

given #529 (T,wt=15): 12944 f(x,f(y,f(z,c_0))) = f(x,f(y,f(y,z))).  [para(9165(a,2),424(a,1,2,2,2)),rewrite(12878(7))].

given #530 (T,wt=15): 12952 f(f(x,f(y,c_0)),z) = f(f(x,f(x,y)),z).  [para(9165(a,1),527(a,1,2,2,1)),rewrite(527(5)),flip(a)].

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

given #532 (F,wt=15): 13007 f(f(x,c_0),f(c_0,y)) = f(f(y,c_0),f(x,x)).  [para(9165(a,1),9141(a,1)),rewrite(10727(6,R))].

given #533 (F,wt=15): 13035 f(x,f(y,f(z,c_0))) = f(x,f(y,f(z,z))).  [para(9166(a,1),424(a,2,2)),rewrite(424(8))].

given #534 (T,wt=15): 13044 f(f(x,f(y,c_0)),z) = f(f(x,f(y,y)),z).  [para(9166(a,1),527(a,1,2,2,1)),rewrite(527(5)),flip(a)].

given #535 (T,wt=15): 13117 f(f(f(c_0,x),y),f(c_0,f(x,z))) = f(x,z).  [para(332(a,1),9174(a,1,2)),rewrite(10701(14))].

given #536 (A,wt=19): 618 f(x,f(f(f(y,x),z),f(f(u,y),x))) = f(f(u,y),x).  [para(504(a,1),470(a,1,1))].

given #537 (F,wt=15): 13122 f(f(x,f(c_0,y)),f(c_0,f(y,z))) = f(y,z).  [para(340(a,1),9174(a,1,2)),rewrite(10706(14))].

given #538 (F,wt=15): 13125 f(f(x,f(c_0,y)),f(c_0,f(z,y))) = f(z,y).  [para(346(a,1),9174(a,1,2)),rewrite(10711(14))].

given #539 (T,wt=15): 13128 f(f(f(c_0,x),y),f(c_0,f(z,x))) = f(z,x).  [para(389(a,1),9174(a,1,2)),rewrite(10712(14))].

given #540 (T,wt=15): 13135 f(f(x,f(y,x)),f(c_0,f(y,z))) = f(y,z).  [para(472(a,1),1235(a,2,2)),rewrite(9188(7,R),9154(7),421(5),2359(5),421(8),10727(8,R)),flip(a)].

given #541 (A,wt=19): 619 f(x,f(f(y,f(z,x)),f(f(z,u),x))) = f(f(z,u),x).  [para(470(a,1),504(a,1,1))].

given #542 (F,wt=15): 13205 f(x,f(f(y,c_0),z)) = f(x,f(f(y,y),z)).  [para(9184(a,1),424(a,1,2,2,2)),rewrite(424(5)),flip(a)].

given #543 (F,wt=15): 13208 f(f(x,c_0),f(c_0,y)) = f(f(x,x),f(y,y)).  [para(9184(a,1),1141(a,1)),rewrite(10727(9,R)),flip(a)].

given #544 (T,wt=15): 13223 f(f(f(x,c_0),y),z) = f(f(f(x,x),y),z).  [para(9184(a,2),527(a,1,2,2,1)),rewrite(11892(7))].

given #545 (T,wt=15): 13350 f(f(x,c_0),f(c_0,y)) = f(f(x,x),f(y,c_0)).  [para(9184(a,1),9165(a,1)),rewrite(10727(10,R)),flip(a)].

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

given #547 (F,wt=15): 13364 f(x,f(y,f(x,f(f(y,x),z)))) = f(x,x).  [para(1051(a,1),473(a,1,2)),flip(a)].

given #548 (F,wt=15): 13368 f(f(f(x,c_0),y),f(c_0,f(x,z))) = f(x,z).  [para(473(a,1),9174(a,1,2)),rewrite(13365(14))].

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

given #550 (T,wt=15): 13550 f(f(c_0,x),f(c_0,y)) = f(f(x,x),f(y,y)).  [para(10718(a,1),1141(a,1)),rewrite(10727(9,R)),flip(a)].

given #551 (A,wt=17): 622 f(f(x,y),f(x,f(f(f(x,y),f(z,y)),u))) = x.  [para(347(a,1),324(a,1,1))].

given #552 (F,wt=15): 13551 f(f(c_0,x),f(y,y)) = f(f(x,x),f(c_0,y)).  [para(10718(a,2),1141(a,1)),rewrite(10727(8,R))].

given #553 (F,wt=15): 13562 f(f(c_0,x),f(y,c_0)) = f(f(x,x),f(y,y)).  [para(10718(a,1),1235(a,1)),rewrite(9158(9,R)),flip(a)].

given #554 (T,wt=15): 13563 f(f(c_0,x),f(y,y)) = f(f(x,x),f(y,c_0)).  [para(10718(a,2),1235(a,1)),rewrite(9158(8,R))].

given #555 (T,wt=15): 13606 f(f(f(c_0,x),y),z) = f(f(f(x,x),y),z).  [para(10718(a,2),527(a,1,2,2,1)),rewrite(13605(7))].

given #556 (A,wt=17): 623 f(f(x,y),f(x,f(z,f(f(x,y),f(u,y))))) = x.  [para(347(a,1),343(a,1,1))].

given #557 (F,wt=15): 13866 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,x)).  [para(10718(a,2),9141(a,2)),flip(a)].

given #558 (F,wt=15): 13878 f(f(c_0,x),f(c_0,y)) = f(f(x,x),f(y,c_0)).  [para(10718(a,1),9165(a,1)),rewrite(10727(10,R)),flip(a)].

given #559 (T,wt=15): 13879 f(f(c_0,x),f(y,c_0)) = f(f(x,x),f(c_0,y)).  [para(10718(a,2),9165(a,1)),rewrite(10727(9,R))].

given #560 (T,wt=15): 13896 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,z))).  [para(10726(a,1),424(a,1,2,2,2)),rewrite(13549(7)),flip(a)].

given #561 (A,wt=21): 625 f(x,f(f(x,f(y,f(z,y))),f(z,z))) = f(x,f(y,f(z,y))).  [para(429(a,1),347(a,1,2,2))].

given #562 (F,wt=15): 13897 f(f(c_0,x),f(c_0,y)) = f(f(y,y),f(x,x)).  [para(10726(a,1),1234(a,1)),rewrite(10727(9,R)),flip(a)].

given #563 (F,wt=15): 13900 f(f(c_0,x),f(y,c_0)) = f(f(y,y),f(x,x)).  [para(10726(a,1),1373(a,1)),rewrite(9158(9,R)),flip(a)].

given #564 (T,wt=15): 13905 f(f(x,f(c_0,y)),z) = f(f(x,f(y,y)),z).  [para(10726(a,1),527(a,1,2,2,1)),rewrite(527(5)),flip(a)].

given #565 (T,wt=15): 13927 f(f(c_0,x),f(c_0,y)) = f(f(y,c_0),f(x,x)).  [para(10726(a,1),9161(a,1)),rewrite(10727(10,R)),flip(a)].

given #566 (A,wt=31): 627 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(294(a,1),347(a,1,2,1)),rewrite(294(23))].

given #567 (F,wt=15): 13946 f(f(f(c_0,x),y),f(f(z,f(z,x)),y)) = y.  [para(10727(a,1),504(a,1,2,1))].

given #568 (F,wt=15): 13974 f(x,f(y,f(c_0,z))) = f(x,f(y,f(y,z))).  [para(10727(a,1),424(a,2,2)),rewrite(424(8))].

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

given #570 (T,wt=15): 14103 f(x,f(f(c_0,y),z)) = f(x,f(z,f(z,y))).  [para(10729(a,1),424(a,1,2,2,2)),rewrite(441(5)),flip(a)].

given #571 (A,wt=21): 632 f(x,f(f(x,f(y,f(y,z))),f(z,z))) = f(x,f(y,f(y,z))).  [para(462(a,1),347(a,1,2,2))].

given #572 (F,wt=15): 14110 f(f(f(c_0,x),y),z) = f(f(y,f(y,x)),z).  [para(10729(a,2),527(a,1,2,2,1)),rewrite(531(6))].

given #573 (F,wt=15): 14205 f(x,f(y,f(c_0,z))) = f(x,f(y,f(z,y))).  [para(10731(a,1),424(a,2,2)),rewrite(424(8))].

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

given #575 (T,wt=15): 14283 f(f(c_0,x),f(y,y)) = f(f(y,c_0),f(x,c_0)).  [para(10731(a,1),9141(a,1)),rewrite(9158(6,R)),flip(a)].

given #576 (A,wt=27): 633 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(297(a,1),347(a,1,2,1)),rewrite(297(16))].

given #577 (F,wt=15): 14317 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,z))).  [para(10732(a,1),424(a,1,2,2,2)),rewrite(441(5)),flip(a)].

given #578 (F,wt=15): 14327 f(f(f(c_0,x),y),z) = f(f(y,f(x,y)),z).  [para(10732(a,2),527(a,1,2,2,1)),rewrite(531(6))].

given #579 (T,wt=15): 14360 f(f(c_0,x),f(y,c_0)) = f(f(c_0,y),f(x,x)).  [para(10732(a,2),10718(a,2)),rewrite(13925(5))].

given #580 (T,wt=15): 14372 f(x,f(f(y,y),z)) = f(x,f(z,f(c_0,y))).  [para(10748(a,1),424(a,1,2,2,2)),rewrite(441(6)),flip(a)].

given #581 (A,wt=23): 637 f(f(x,y),f(f(x,z),f(f(x,y),f(u,y)))) = f(f(x,y),f(u,y)).  [para(347(a,1),470(a,1,1))].

given #582 (F,wt=15): 14373 f(f(f(x,x),y),z) = f(f(y,f(c_0,x)),z).  [para(10748(a,1),527(a,1,2,2,1)),rewrite(13609(7)),flip(a)].

given #583 (F,wt=15): 14388 f(x,f(f(c_0,y),z)) = f(x,f(z,f(y,y))).  [para(10749(a,1),424(a,1,2,2,2)),rewrite(441(5)),flip(a)].

given #584 (T,wt=15): 14389 f(f(f(c_0,x),y),z) = f(f(y,f(x,x)),z).  [para(10749(a,1),527(a,1,2,2,1)),rewrite(13610(7)),flip(a)].

given #585 (T,wt=15): 14403 f(f(c_0,x),f(y,y)) = f(f(c_0,y),f(x,x)).  [para(10749(a,2),10718(a,2))].

given #586 (A,wt=23): 641 f(f(x,y),f(f(z,x),f(f(x,y),f(u,y)))) = f(f(x,y),f(u,y)).  [para(347(a,1),504(a,1,1))].

given #587 (F,wt=15): 14411 f(f(x,y),f(c_0,f(z,f(c_0,f(y,x))))) = c_0.  [para(11467(a,1),347(a,1,2,1)),rewrite(11467(13))].

given #588 (F,wt=15): 14455 f(x,f(f(y,y),z)) = f(x,f(z,f(y,c_0))).  [para(12437(a,1),424(a,1,2,2,2)),rewrite(441(6)),flip(a)].

given #589 (T,wt=15): 14456 f(f(f(x,x),y),z) = f(f(y,f(x,c_0)),z).  [para(12437(a,1),527(a,1,2,2,1)),rewrite(11894(7)),flip(a)].

given #590 (T,wt=15): 14516 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x.  [para(9269(a,1),343(a,1,2,2)),rewrite(421(7))].

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

given #592 (F,wt=15): 14521 f(f(f(x,f(c_0,f(y,z))),u),f(u,z)) = u.  [para(9269(a,1),453(a,1,2,2))].

given #593 (F,wt=15): 14522 f(f(x,f(y,f(c_0,f(z,u)))),f(u,x)) = x.  [para(9269(a,1),454(a,1,2,1))].

given #594 (T,wt=15): 14524 f(f(x,y),f(y,f(z,f(c_0,f(u,x))))) = y.  [para(9269(a,1),464(a,1,1,1))].

given #595 (T,wt=15): 14525 f(f(x,y),f(f(z,f(c_0,f(u,y))),x)) = x.  [para(9269(a,1),490(a,1,1,2))].

given #596 (A,wt=17): 644 f(f(x,y),f(x,f(f(f(x,y),f(y,z)),u))) = x.  [para(387(a,1),324(a,1,1))].

given #597 (F,wt=15): 14526 f(f(x,y),f(f(z,f(c_0,f(u,x))),y)) = y.  [para(9269(a,1),504(a,1,2,1)),rewrite(421(7))].

given #598 (F,wt=15): 14529 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x).  [para(1141(a,1),9269(a,1,2,2,2)),rewrite(9188(3,R),9154(3))].

given #599 (T,wt=15): 14533 f(x,f(y,f(c_0,f(z,f(x,z))))) = f(x,x).  [para(1235(a,1),9269(a,1,2,2,2)),rewrite(9188(3,R),9154(3))].

given #600 (T,wt=15): 14565 f(x,f(y,f(c_0,f(z,f(x,c_0))))) = f(x,c_0).  [para(9193(a,1),9269(a,1,1))].

given #601 (A,wt=17): 646 f(f(x,y),f(x,f(z,f(f(x,y),f(y,u))))) = x.  [para(387(a,1),343(a,1,1))].

given #602 (F,wt=15): 14566 f(x,f(y,f(c_0,f(z,f(c_0,x))))) = f(c_0,x).  [para(10579(a,1),9269(a,1,1))].

given #603 (F,wt=15): 14567 f(x,f(y,f(c_0,f(f(x,c_0),z)))) = f(x,x).  [para(9141(a,2),9269(a,1,2,2,2)),rewrite(9188(3,R),9154(3))].

given #604 (T,wt=15): 14582 f(x,f(y,f(c_0,f(f(x,x),z)))) = f(c_0,x).  [para(10748(a,2),9269(a,1,2,2,2)),rewrite(9188(5,R),9162(4))].

given #605 (T,wt=15): 14583 f(x,f(y,f(c_0,f(f(c_0,x),z)))) = f(x,x).  [para(10749(a,2),9269(a,1,2,2,2)),rewrite(9188(3,R),9154(3))].

given #606 (A,wt=23): 649 f(f(x,y),f(f(f(x,y),f(y,z)),f(x,u))) = f(f(x,y),f(y,z)).  [para(387(a,1),451(a,1,1))].

given #607 (F,wt=15): 14669 f(x,f(f(y,f(y,x)),f(z,f(x,x)))) = c_0.  [para(1141(a,1),10693(a,1,2,1)),rewrite(9188(3,R),9154(3))].

given #608 (F,wt=15): 14670 f(x,f(f(y,f(x,x)),f(z,f(z,x)))) = c_0.  [para(1141(a,1),10693(a,1,2,2)),rewrite(9188(3,R),9154(3))].

given #609 (T,wt=15): 14676 f(x,f(f(y,f(x,y)),f(z,f(x,x)))) = c_0.  [para(1235(a,1),10693(a,1,2,1)),rewrite(9188(3,R),9154(3))].

given #610 (T,wt=15): 14677 f(x,f(f(y,f(x,x)),f(z,f(x,z)))) = c_0.  [para(1235(a,1),10693(a,1,2,2)),rewrite(9188(3,R),9154(3))].

given #611 (A,wt=31): 651 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(294(a,1),387(a,1,2,1)),rewrite(294(23))].

given #612 (F,wt=15): 14691 f(x,f(f(y,f(x,c_0)),f(z,f(x,c_0)))) = c_0.  [para(9193(a,1),10693(a,1,1))].

given #613 (F,wt=15): 14692 f(x,f(f(y,f(c_0,x)),f(z,f(c_0,x)))) = c_0.  [para(10579(a,1),10693(a,1,1))].

given #614 (T,wt=15): 14693 f(x,f(f(f(x,c_0),y),f(z,f(x,x)))) = c_0.  [para(9141(a,2),10693(a,1,2,1)),rewrite(9188(3,R),9154(3))].

given #615 (T,wt=15): 14694 f(x,f(f(y,f(x,x)),f(f(x,c_0),z))) = c_0.  [para(9141(a,2),10693(a,1,2,2)),rewrite(9188(3,R),9154(3))].

given #616 (A,wt=27): 652 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(387(a,1),452(a,1,2)),rewrite(421(5),421(8))].

given #617 (F,wt=15): 14697 f(x,f(f(y,f(x,y)),f(z,f(x,c_0)))) = c_0.  [para(9158(a,1),10693(a,1,2,1)),rewrite(9188(5,R),9156(4))].

given #618 (F,wt=15): 14698 f(x,f(f(y,f(x,c_0)),f(z,f(x,z)))) = c_0.  [para(9158(a,1),10693(a,1,2,2)),rewrite(9188(5,R),9156(4))].

given #619 (T,wt=15): 14704 f(x,f(f(y,f(y,x)),f(z,f(x,c_0)))) = c_0.  [para(9165(a,1),10693(a,1,2,1)),rewrite(9188(5,R),9156(4))].

given #620 (T,wt=15): 14705 f(x,f(f(y,f(x,c_0)),f(z,f(z,x)))) = c_0.  [para(9165(a,1),10693(a,1,2,2)),rewrite(9188(5,R),9156(4))].

given #621 (A,wt=27): 655 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(387(a,1),454(a,1,2)),rewrite(421(5),421(8))].

given #622 (F,wt=15): 14708 f(x,f(f(y,f(x,x)),f(z,f(x,c_0)))) = c_0.  [para(9166(a,1),10693(a,1,2,1)),rewrite(9188(5,R),9156(4))].

given #623 (F,wt=15): 14709 f(x,f(f(y,f(x,c_0)),f(z,f(x,x)))) = c_0.  [para(9166(a,1),10693(a,1,2,2)),rewrite(9188(5,R),9156(4))].

given #624 (T,wt=15): 14712 f(x,f(f(y,f(x,x)),f(z,f(c_0,x)))) = c_0.  [para(10726(a,1),10693(a,1,2,1)),rewrite(9188(5,R),9162(4))].

given #625 (T,wt=15): 14713 f(x,f(f(y,f(c_0,x)),f(z,f(x,x)))) = c_0.  [para(10726(a,1),10693(a,1,2,2)),rewrite(9188(5,R),9162(4))].

given #626 (A,wt=27): 658 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(297(a,1),387(a,1,2,1)),rewrite(297(16))].

given #627 (F,wt=15): 14714 f(x,f(f(y,f(y,x)),f(z,f(c_0,x)))) = c_0.  [para(10727(a,1),10693(a,1,2,1)),rewrite(9188(5,R),9162(4))].

given #628 (F,wt=15): 14715 f(x,f(f(y,f(c_0,x)),f(z,f(z,x)))) = c_0.  [para(10727(a,1),10693(a,1,2,2)),rewrite(9188(5,R),9162(4))].

given #629 (T,wt=15): 14721 f(x,f(f(y,f(x,y)),f(z,f(c_0,x)))) = c_0.  [para(10731(a,1),10693(a,1,2,1)),rewrite(9188(5,R),9162(4))].

given #630 (T,wt=15): 14722 f(x,f(f(y,f(c_0,x)),f(z,f(x,z)))) = c_0.  [para(10731(a,1),10693(a,1,2,2)),rewrite(9188(5,R),9162(4))].

given #631 (A,wt=23): 662 f(f(x,y),f(f(x,z),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)).  [para(387(a,1),470(a,1,1))].

given #632 (F,wt=15): 14727 f(x,f(f(f(x,x),y),f(z,f(c_0,x)))) = c_0.  [para(10748(a,2),10693(a,1,2,1)),rewrite(9188(5,R),9162(4))].

given #633 (F,wt=15): 14728 f(x,f(f(y,f(c_0,x)),f(f(x,x),z))) = c_0.  [para(10748(a,2),10693(a,1,2,2)),rewrite(9188(5,R),9162(4))].

given #634 (T,wt=15): 14729 f(x,f(f(f(c_0,x),y),f(z,f(x,x)))) = c_0.  [para(10749(a,2),10693(a,1,2,1)),rewrite(9188(3,R),9154(3))].

given #635 (T,wt=15): 14730 f(x,f(f(y,f(x,x)),f(f(c_0,x),z))) = c_0.  [para(10749(a,2),10693(a,1,2,2)),rewrite(9188(3,R),9154(3))].

given #636 (A,wt=27): 665 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(301(a,1),387(a,1,2,1)),rewrite(301(16))].

given #637 (F,wt=15): 14731 f(x,f(f(f(x,x),y),f(z,f(x,c_0)))) = c_0.  [para(12437(a,2),10693(a,1,2,1)),rewrite(9188(5,R),9156(4))].

given #638 (F,wt=15): 14732 f(x,f(f(y,f(x,c_0)),f(f(x,x),z))) = c_0.  [para(12437(a,2),10693(a,1,2,2)),rewrite(9188(5,R),9156(4))].

given #639 (T,wt=15): 14764 f(f(x,y),f(x,f(z,f(c_0,f(y,u))))) = x.  [para(10700(a,1),640(a,1,2,2)),rewrite(421(7))].

given #640 (T,wt=15): 14778 f(f(f(x,f(c_0,f(y,z))),u),f(u,y)) = u.  [para(10700(a,1),773(a,1,2,2))].

given #641 (A,wt=23): 667 f(f(x,y),f(f(z,x),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)).  [para(387(a,1),504(a,1,1))].

given #642 (F,wt=15): 14834 f(f(x,f(y,f(c_0,f(z,u)))),f(z,x)) = x.  [para(10705(a,1),454(a,1,2,1))].

given #643 (F,wt=15): 14836 f(f(x,y),f(y,f(z,f(c_0,f(x,u))))) = y.  [para(10705(a,1),464(a,1,1,1))].

given #644 (T,wt=15): 14837 f(f(x,y),f(f(z,f(c_0,f(y,u))),x)) = x.  [para(10705(a,1),490(a,1,1,2))].

given #645 (T,wt=15): 14838 f(f(x,y),f(f(z,f(c_0,f(x,u))),y)) = y.  [para(10705(a,1),504(a,1,2,1)),rewrite(421(7))].

given #646 (A,wt=19): 669 f(x,f(f(x,y),f(z,f(f(x,y),f(y,u))))) = f(x,y).  [para(387(a,1),347(a,1,2,1)),rewrite(387(11))].

given #647 (F,wt=15): 14861 f(f(x,f(y,c_0)),f(c_0,f(y,z))) = f(y,z).  [para(12853(a,1),531(a,1,2)),rewrite(421(4),9175(4)),flip(a)].

given #648 (F,wt=15): 14862 f(f(x,f(y,c_0)),f(c_0,f(z,y))) = f(z,y).  [para(514(a,1),13131(a,1,1,2)),rewrite(421(6))].

given #649 (T,wt=15): 14866 f(f(f(x,c_0),y),f(c_0,f(z,x))) = f(z,x).  [para(14055(a,1),527(a,1,2)),rewrite(421(4),9174(4)),flip(a)].

given #650 (T,wt=15): 14883 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,x).  [para(169(a,1),14577(a,1,1))].

given #651 (A,wt=19): 670 f(x,f(f(x,y),f(f(f(x,y),f(z,y)),u))) = f(x,y).  [para(347(a,1),387(a,1,2,1)),rewrite(347(11))].

given #652 (F,wt=15): 14886 f(f(x,y),f(x,f(z,f(z,f(u,y))))) = x.  [para(14577(a,1),343(a,1,2,2)),rewrite(421(6))].

given #653 (F,wt=15): 14890 f(f(f(x,f(x,f(y,z))),u),f(u,z)) = u.  [para(14577(a,1),453(a,1,2,2))].

given #654 (T,wt=15): 14892 f(f(x,f(y,f(y,f(z,u)))),f(u,x)) = x.  [para(14577(a,1),454(a,1,2,1))].

given #655 (T,wt=15): 14894 f(f(x,y),f(y,f(z,f(z,f(u,x))))) = y.  [para(14577(a,1),464(a,1,1,1))].

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

given #657 (F,wt=15): 14895 f(f(x,y),f(f(z,f(z,f(u,y))),x)) = x.  [para(14577(a,1),490(a,1,1,2))].

given #658 (F,wt=15): 14896 f(f(x,y),f(f(z,f(z,f(u,x))),y)) = y.  [para(14577(a,1),504(a,1,2,1)),rewrite(421(6))].

given #659 (T,wt=15): 14903 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0.  [para(14577(a,1),1141(a,2,2)),rewrite(9188(8,R),421(9),9064(9))].

given #660 (T,wt=15): 14904 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x).  [para(1141(a,1),14577(a,1,2,2,2)),rewrite(9188(3,R),9154(3))].

given #661 (A,wt=29): 672 f(f(f(x,y),f(z,y)),f(f(x,y),f(f(f(f(x,y),f(z,y)),f(u,x)),v))) = f(x,y).  [para(302(a,1),324(a,1,1))].

given #662 (F,wt=15): 14908 f(x,f(y,f(y,f(z,f(x,z))))) = f(x,x).  [para(1235(a,1),14577(a,1,2,2,2)),rewrite(9188(3,R),9154(3))].

given #663 (F,wt=15): 14953 f(x,f(y,f(y,f(z,f(x,c_0))))) = f(x,c_0).  [para(9193(a,1),14577(a,1,1))].

given #664 (T,wt=15): 14954 f(x,f(y,f(y,f(z,f(c_0,x))))) = f(c_0,x).  [para(10579(a,1),14577(a,1,1))].

given #665 (T,wt=15): 14955 f(x,f(y,f(y,f(f(x,c_0),z)))) = f(x,x).  [para(9141(a,2),14577(a,1,2,2,2)),rewrite(9188(3,R),9154(3))].

given #666 (A,wt=27): 673 f(x,f(f(x,f(y,f(x,f(z,u)))),f(v,f(x,z)))) = f(x,f(y,f(x,f(z,u)))).  [para(324(a,1),302(a,1,1)),rewrite(324(4),324(12))].

given #667 (F,wt=15): 14970 f(x,f(y,f(y,f(f(x,x),z)))) = f(c_0,x).  [para(10748(a,2),14577(a,1,2,2,2)),rewrite(9188(5,R),9162(4))].

given #668 (F,wt=15): 14971 f(x,f(y,f(y,f(f(c_0,x),z)))) = f(x,x).  [para(10749(a,2),14577(a,1,2,2,2)),rewrite(9188(3,R),9154(3))].

given #669 (T,wt=15): 14992 f(f(x,f(y,z)),f(c_0,f(z,y))) = f(z,y).  [para(10667(a,1),14584(a,1,1,2,2)),rewrite(9162(5),421(5))].

given #670 (T,wt=15): 15009 f(x,f(f(f(x,x),y),f(z,f(z,x)))) = c_0.  [para(1141(a,1),14654(a,1,2,2)),rewrite(9188(3,R),9154(3))].

given #671 (A,wt=29): 675 f(f(f(x,y),f(z,y)),f(f(x,y),f(u,f(f(f(x,y),f(z,y)),f(v,x))))) = f(x,y).  [para(302(a,1),343(a,1,1))].

given #672 (F,wt=15): 15013 f(x,f(f(f(x,x),y),f(z,f(x,z)))) = c_0.  [para(1235(a,1),14654(a,1,2,2)),rewrite(9188(3,R),9154(3))].

given #673 (F,wt=15): 15024 f(x,f(f(f(x,c_0),y),f(z,f(x,c_0)))) = c_0.  [para(9193(a,1),14654(a,1,1))].

given #674 (T,wt=15): 15025 f(x,f(f(f(c_0,x),y),f(z,f(c_0,x)))) = c_0.  [para(10579(a,1),14654(a,1,1))].

given #675 (T,wt=15): 15026 f(x,f(f(f(x,x),y),f(f(x,c_0),z))) = c_0.  [para(9141(a,2),14654(a,1,2,2)),rewrite(9188(3,R),9154(3))].

given #676 (A,wt=27): 676 f(x,f(f(x,f(y,f(x,f(z,u)))),f(v,f(x,u)))) = f(x,f(y,f(x,f(z,u)))).  [para(343(a,1),302(a,1,1)),rewrite(343(4),343(12))].

given #677 (F,wt=15): 15028 f(x,f(f(f(x,c_0),y),f(z,f(x,z)))) = c_0.  [para(9158(a,1),14654(a,1,2,2)),rewrite(9188(5,R),9156(4))].

given #678 (F,wt=15): 15032 f(x,f(f(f(x,c_0),y),f(z,f(z,x)))) = c_0.  [para(9165(a,1),14654(a,1,2,2)),rewrite(9188(5,R),9156(4))].

given #679 (T,wt=15): 15036 f(x,f(f(f(c_0,x),y),f(z,f(z,x)))) = c_0.  [para(10727(a,1),14654(a,1,2,2)),rewrite(9188(5,R),9162(4))].

given #680 (T,wt=15): 15040 f(x,f(f(f(c_0,x),y),f(z,f(x,z)))) = c_0.  [para(10731(a,1),14654(a,1,2,2)),rewrite(9188(5,R),9162(4))].

given #681 (A,wt=23): 679 f(f(x,y),f(f(f(y,x),f(z,x)),f(u,y))) = f(f(y,x),f(z,x)).  [para(421(a,1),302(a,1,1))].

given #682 (F,wt=15): 15043 f(x,f(f(f(c_0,x),y),f(f(x,x),z))) = c_0.  [para(10748(a,2),14654(a,1,2,2)),rewrite(9188(5,R),9162(4))].

given #683 (F,wt=15): 15044 f(x,f(f(f(x,x),y),f(f(c_0,x),z))) = c_0.  [para(10749(a,2),14654(a,1,2,2)),rewrite(9188(3,R),9154(3))].

given #684 (T,wt=15): 15045 f(x,f(f(f(x,c_0),y),f(f(x,x),z))) = c_0.  [para(12437(a,2),14654(a,1,2,2)),rewrite(9188(5,R),9156(4))].

given #685 (T,wt=15): 15046 f(x,f(f(y,f(x,x)),f(f(x,x),z))) = c_0.  [para(169(a,1),14655(a,1,1))].

given #686 (A,wt=23): 680 f(f(x,y),f(f(f(y,x),f(z,y)),f(u,x))) = f(f(x,y),f(z,y)).  [para(421(a,1),302(a,1,2,1,1))].

given #687 (F,wt=15): 15058 f(x,f(f(y,f(y,x)),f(f(x,x),z))) = c_0.  [para(1141(a,1),14655(a,1,2,1)),rewrite(9188(3,R),9154(3))].

given #688 (F,wt=15): 15060 f(x,f(f(y,f(x,y)),f(f(x,x),z))) = c_0.  [para(1235(a,1),14655(a,1,2,1)),rewrite(9188(3,R),9154(3))].

given #689 (T,wt=15): 15070 f(x,f(f(y,f(x,c_0)),f(f(x,c_0),z))) = c_0.  [para(9193(a,1),14655(a,1,1))].

given #690 (T,wt=15): 15071 f(x,f(f(y,f(c_0,x)),f(f(c_0,x),z))) = c_0.  [para(10579(a,1),14655(a,1,1))].

given #691 (A,wt=23): 681 f(f(x,y),f(f(f(z,y),f(x,y)),f(u,x))) = f(f(x,y),f(z,y)).  [para(421(a,1),302(a,1,2,1))].

given #692 (F,wt=15): 15073 f(x,f(f(y,f(x,y)),f(f(x,c_0),z))) = c_0.  [para(9158(a,1),14655(a,1,2,1)),rewrite(9188(5,R),9156(4))].

given #693 (F,wt=15): 15075 f(x,f(f(y,f(y,x)),f(f(x,c_0),z))) = c_0.  [para(9165(a,1),14655(a,1,2,1)),rewrite(9188(5,R),9156(4))].

given #694 (T,wt=15): 15076 f(x,f(f(y,f(y,x)),f(f(c_0,x),z))) = c_0.  [para(10727(a,1),14655(a,1,2,1)),rewrite(9188(5,R),9162(4))].

given #695 (T,wt=15): 15078 f(x,f(f(y,f(x,y)),f(f(c_0,x),z))) = c_0.  [para(10731(a,1),14655(a,1,2,1)),rewrite(9188(5,R),9162(4))].

given #696 (A,wt=35): 683 f(f(x,f(y,f(z,y))),f(f(f(x,f(y,f(z,y))),f(z,z)),f(u,x))) = f(f(x,f(y,f(z,y))),f(z,z)).  [para(429(a,1),302(a,1,2,1,2)),rewrite(429(17))].

given #697 (F,wt=15): 15101 f(f(x,y),f(x,f(z,f(z,f(y,u))))) = x.  [para(14780(a,1),343(a,1,2,2)),rewrite(421(6))].

given #698 (F,wt=15): 15104 f(f(f(x,f(x,f(y,z))),u),f(u,y)) = u.  [para(14780(a,1),453(a,1,2,2))].

given #699 (T,wt=15): 15105 f(f(x,f(y,f(y,f(z,u)))),f(z,x)) = x.  [para(14780(a,1),454(a,1,2,1))].

given #700 (T,wt=15): 15107 f(f(x,y),f(y,f(z,f(z,f(x,u))))) = y.  [para(14780(a,1),464(a,1,1,1))].

given #701 (A,wt=35): 684 f(f(f(x,f(y,x)),z),f(f(y,y),f(f(f(x,f(y,x)),z),f(u,z)))) = f(f(f(x,f(y,x)),z),f(u,z)).  [para(429(a,1),302(a,1,2,2)),rewrite(421(10))].

given #702 (F,wt=15): 15108 f(f(x,y),f(f(z,f(z,f(y,u))),x)) = x.  [para(14780(a,1),490(a,1,1,2))].

given #703 (F,wt=15): 15109 f(f(x,y),f(f(z,f(z,f(x,u))),y)) = y.  [para(14780(a,1),504(a,1,2,1)),rewrite(421(6))].

given #704 (T,wt=15): 15161 f(f(x,f(x,y)),f(c_0,f(z,y))) = f(z,y).  [para(266(a,1),14865(a,1,1,2,2)),rewrite(421(5))].

given #705 (T,wt=15): 15162 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z).  [para(310(a,1),14865(a,1,1,2,2)),rewrite(421(5))].

given #706 (A,wt=37): 685 f(f(f(x,y),f(z,y)),f(f(f(f(x,y),f(z,y)),f(u,x)),f(f(x,y),v))) = f(f(f(x,y),f(z,y)),f(u,x)).  [para(302(a,1),451(a,1,1))].

given #707 (F,wt=15): 15163 f(f(x,f(y,x)),f(c_0,f(z,y))) = f(z,y).  [para(504(a,1),14865(a,1,1,2)),rewrite(421(2),421(5))].

given #708 (F,wt=15): 15174 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0.  [para(14877(a,1),1141(a,2,2)),rewrite(9188(8,R),421(9),9064(9))].

given #709 (T,wt=15): 15229 f(x,f(f(f(x,x),y),f(f(x,x),z))) = c_0.  [para(169(a,1),14997(a,1,1))].

given #710 (T,wt=15): 15251 f(x,f(f(f(x,c_0),y),f(f(x,c_0),z))) = c_0.  [para(9193(a,1),14997(a,1,1))].

given #711 (A,wt=27): 686 f(x,f(f(x,f(y,f(x,f(z,u)))),f(v,f(z,x)))) = f(x,f(y,f(x,f(z,u)))).  [para(451(a,1),302(a,1,1)),rewrite(451(4),451(12))].

given #712 (F,wt=15): 15252 f(x,f(f(f(c_0,x),y),f(f(c_0,x),z))) = c_0.  [para(10579(a,1),14997(a,1,1))].

given #713 (F,wt=15): 15334 f(f(f(f(x,x),y),z),f(c_0,f(z,x))) = c_0.  [para(1247(a,1),9122(a,1,2,2,2)),rewrite(421(7),368(7))].

given #714 (T,wt=15): 15380 f(f(f(x,f(y,y)),z),f(c_0,f(z,y))) = c_0.  [para(1255(a,1),9122(a,1,2,2,2)),rewrite(421(7),368(7))].

given #715 (T,wt=15): 15619 f(f(x,f(y,y)),z) = f(z,f(x,f(x,y))).  [para(1340(a,1),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #716 (A,wt=55): 687 f(f(x,x),f(f(f(x,x),f(y,f(f(x,x),f(z,f(f(f(x,x),u),f(v,x)))))),f(w,f(f(x,x),u)))) = f(f(x,x),f(y,f(f(x,x),f(z,f(f(f(x,x),u),f(v,x)))))).  [para(294(a,1),302(a,1,1)),rewrite(294(11),294(26))].

given #717 (F,wt=15): 15620 f(f(x,f(x,y)),z) = f(z,f(x,f(y,y))).  [para(1340(a,2),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #718 (F,wt=15): 15691 f(f(x,f(y,z)),f(x,f(f(y,y),u))) = x.  [para(297(a,1),1372(a,1,2,2)),rewrite(421(5),491(5))].

given #719 (T,wt=15): 15694 f(f(x,f(y,z)),f(x,f(f(z,z),u))) = x.  [para(301(a,1),1372(a,1,2,2)),rewrite(421(5),489(5))].

given #720 (T,wt=15): 15699 f(f(x,f(y,z)),f(x,f(u,f(y,y)))) = x.  [para(380(a,1),1372(a,1,2,2)),rewrite(9188(5,R),9154(5),421(5),516(5))].

given #721 (A,wt=27): 688 f(x,f(f(x,f(y,f(f(z,u),x))),f(v,f(x,z)))) = f(x,f(y,f(f(z,u),x))).  [para(452(a,1),302(a,1,1)),rewrite(452(4),452(12))].

given #722 (F,wt=15): 15700 f(f(x,f(y,z)),f(x,f(u,f(z,z)))) = x.  [para(396(a,1),1372(a,1,2,2)),rewrite(9188(5,R),9154(5),421(5),515(5))].

given #723 (F,wt=15): 15724 f(f(x,f(y,z)),f(x,f(u,f(y,u)))) = x.  [para(472(a,1),1372(a,1,2,2)),rewrite(421(5),2359(5))].

given #724 (T,wt=15): 15739 f(f(x,f(y,z)),f(x,f(u,f(z,u)))) = x.  [para(506(a,1),1372(a,1,2,2)),rewrite(421(5),2195(5))].

given #725 (T,wt=15): 15742 f(f(f(x,y),z),f(z,f(f(x,x),u))) = z.  [para(297(a,1),1383(a,1,2,2)),rewrite(421(5),491(5))].

given #726 (A,wt=37): 689 f(f(f(x,y),f(z,y)),f(f(f(f(x,y),f(z,y)),f(u,x)),f(v,f(x,y)))) = f(f(f(x,y),f(z,y)),f(u,x)).  [para(302(a,1),453(a,1,1))].

given #727 (F,wt=15): 15743 f(f(f(x,y),z),f(z,f(f(y,y),u))) = z.  [para(301(a,1),1383(a,1,2,2)),rewrite(421(5),489(5))].

given #728 (F,wt=15): 15744 f(f(f(x,y),z),f(z,f(u,f(x,x)))) = z.  [para(380(a,1),1383(a,1,2,2)),rewrite(9188(5,R),9154(5),421(5),516(5))].

given #729 (T,wt=15): 15745 f(f(f(x,y),z),f(z,f(u,f(y,y)))) = z.  [para(396(a,1),1383(a,1,2,2)),rewrite(9188(5,R),9154(5),421(5),515(5))].

given #730 (T,wt=15): 15753 f(f(f(x,y),z),f(z,f(u,f(x,u)))) = z.  [para(472(a,1),1383(a,1,2,2)),rewrite(421(5),2359(5))].

given #731 (A,wt=19): 690 f(f(f(x,y),f(y,z)),f(f(y,z),f(u,z))) = f(y,z).  [para(302(a,1),453(a,1,2))].

given #732 (F,wt=15): 15758 f(f(f(x,y),z),f(z,f(u,f(y,u)))) = z.  [para(506(a,1),1383(a,1,2,2)),rewrite(421(5),2195(5))].

given #733 (F,wt=15): 15759 f(f(x,f(y,z)),f(f(f(y,y),u),x)) = x.  [para(297(a,1),1384(a,1,2,1)),rewrite(421(5),491(5))].

given #734 (T,wt=15): 15762 f(f(x,f(y,z)),f(f(f(z,z),u),x)) = x.  [para(301(a,1),1384(a,1,2,1)),rewrite(421(5),489(5))].

given #735 (T,wt=15): 15763 f(f(x,f(y,z)),f(f(u,f(y,y)),x)) = x.  [para(380(a,1),1384(a,1,2,1)),rewrite(9188(5,R),9154(5),421(5),516(5))].

given #736 (A,wt=27): 691 f(x,f(f(x,f(y,f(x,f(z,u)))),f(v,f(u,x)))) = f(x,f(y,f(x,f(z,u)))).  [para(453(a,1),302(a,1,1)),rewrite(453(4),453(12))].

given #737 (F,wt=15): 15764 f(f(x,f(y,z)),f(f(u,f(z,z)),x)) = x.  [para(396(a,1),1384(a,1,2,1)),rewrite(9188(5,R),9154(5),421(5),515(5))].

given #738 (F,wt=15): 15770 f(f(x,f(y,z)),f(f(u,f(y,u)),x)) = x.  [para(472(a,1),1384(a,1,2,1)),rewrite(421(5),2359(5))].

given #739 (T,wt=15): 15771 f(f(x,f(y,z)),f(f(u,f(z,u)),x)) = x.  [para(506(a,1),1384(a,1,2,1)),rewrite(421(5),2195(5))].

given #740 (T,wt=15): 15774 f(f(f(f(x,x),y),z),f(z,f(x,u))) = z.  [para(297(a,1),1388(a,1,1,1)),rewrite(421(8),491(8))].

given #741 (A,wt=33): 692 f(f(f(x,y),f(z,y)),f(y,f(f(f(x,y),f(z,y)),f(u,x)))) = f(f(f(x,y),f(z,y)),f(u,x)).  [para(302(a,1),454(a,1,2)),rewrite(421(6),421(10))].

given #742 (F,wt=15): 15775 f(f(f(f(x,x),y),z),f(z,f(u,x))) = z.  [para(301(a,1),1388(a,1,1,1)),rewrite(421(8),489(8))].

given #743 (F,wt=15): 15776 f(f(f(x,f(y,y)),z),f(z,f(y,u))) = z.  [para(380(a,1),1388(a,1,1,1)),rewrite(9188(8,R),9154(8),421(8),516(8))].

given #744 (T,wt=15): 15777 f(f(f(x,f(y,y)),z),f(z,f(u,y))) = z.  [para(396(a,1),1388(a,1,1,1)),rewrite(9188(8,R),9154(8),421(8),515(8))].

given #745 (T,wt=15): 15788 f(f(f(x,f(y,x)),z),f(z,f(y,u))) = z.  [para(472(a,1),1388(a,1,1,1)),rewrite(421(8),2359(8))].

given #746 (A,wt=27): 693 f(x,f(f(x,f(y,f(f(z,u),x))),f(v,f(x,u)))) = f(x,f(y,f(f(z,u),x))).  [para(454(a,1),302(a,1,1)),rewrite(454(4),454(12))].

given #747 (F,wt=15): 15796 f(f(f(x,f(y,x)),z),f(z,f(u,y))) = z.  [para(506(a,1),1388(a,1,1,1)),rewrite(421(8),2195(8))].

given #748 (F,wt=15): 15805 f(f(x,f(f(y,y),z)),f(f(y,u),x)) = x.  [para(297(a,1),1403(a,1,1,2)),rewrite(421(8),491(8))].

given #749 (T,wt=15): 15806 f(f(x,f(f(y,y),z)),f(f(u,y),x)) = x.  [para(301(a,1),1403(a,1,1,2)),rewrite(421(8),489(8))].

given #750 (T,wt=15): 15807 f(f(x,f(y,f(z,z))),f(f(z,u),x)) = x.  [para(380(a,1),1403(a,1,1,2)),rewrite(9188(8,R),9154(8),421(8),516(8))].

given #751 (A,wt=35): 695 f(f(x,f(y,f(y,z))),f(f(f(x,f(y,f(y,z))),f(z,z)),f(u,x))) = f(f(x,f(y,f(y,z))),f(z,z)).  [para(462(a,1),302(a,1,2,1,2)),rewrite(462(17))].

given #752 (F,wt=15): 15808 f(f(x,f(y,f(z,z))),f(f(u,z),x)) = x.  [para(396(a,1),1403(a,1,1,2)),rewrite(9188(8,R),9154(8),421(8),515(8))].

given #753 (F,wt=15): 15814 f(f(x,f(y,f(z,y))),f(f(z,u),x)) = x.  [para(472(a,1),1403(a,1,1,2)),rewrite(421(8),2359(8))].

given #754 (T,wt=15): 15817 f(f(x,f(y,f(z,y))),f(f(u,z),x)) = x.  [para(506(a,1),1403(a,1,1,2)),rewrite(421(8),2195(8))].

given #755 (T,wt=15): 15833 f(f(f(x,y),z),f(f(f(x,x),u),z)) = z.  [para(297(a,1),1407(a,1,2,1)),rewrite(421(5),491(5))].

given #756 (A,wt=35): 696 f(f(f(x,f(x,y)),z),f(f(y,y),f(f(f(x,f(x,y)),z),f(u,z)))) = f(f(f(x,f(x,y)),z),f(u,z)).  [para(462(a,1),302(a,1,2,2)),rewrite(421(10))].

given #757 (F,wt=15): 15834 f(f(f(x,y),z),f(f(f(y,y),u),z)) = z.  [para(301(a,1),1407(a,1,2,1)),rewrite(421(5),489(5))].

given #758 (F,wt=15): 15835 f(f(f(x,y),z),f(f(u,f(x,x)),z)) = z.  [para(380(a,1),1407(a,1,2,1)),rewrite(9188(5,R),9154(5),421(5),516(5))].

given #759 (T,wt=15): 15836 f(f(f(x,y),z),f(f(u,f(y,y)),z)) = z.  [para(396(a,1),1407(a,1,2,1)),rewrite(9188(5,R),9154(5),421(5),515(5))].

given #760 (T,wt=15): 15840 f(f(f(x,y),z),f(f(u,f(x,u)),z)) = z.  [para(472(a,1),1407(a,1,2,1)),rewrite(421(5),2359(5))].

given #761 (A,wt=47): 697 f(f(f(x,x),y),f(f(f(f(x,x),y),f(z,f(f(f(x,x),y),f(x,u)))),f(v,f(x,x)))) = f(f(f(x,x),y),f(z,f(f(f(x,x),y),f(x,u)))).  [para(297(a,1),302(a,1,1)),rewrite(297(8),297(20))].

given #762 (F,wt=15): 15841 f(f(f(x,y),z),f(f(u,f(y,u)),z)) = z.  [para(506(a,1),1407(a,1,2,1)),rewrite(421(5),2195(5))].

given #763 (F,wt=15): 15850 f(f(f(x,x),y),z) = f(z,f(y,f(y,x))).  [para(1450(a,1),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #764 (T,wt=15): 15851 f(f(x,f(x,y)),z) = f(z,f(f(y,y),x)).  [para(1450(a,2),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #765 (T,wt=15): 15959 f(f(x,f(y,y)),z) = f(z,f(x,f(y,x))).  [para(1615(a,1),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #766 (A,wt=25): 698 f(x,f(f(x,f(y,f(x,z))),f(u,f(f(v,z),x)))) = f(x,f(y,f(x,z))).  [para(464(a,1),302(a,1,1)),rewrite(464(4),464(12))].

given #767 (F,wt=15): 15960 f(f(x,f(y,x)),z) = f(z,f(x,f(y,y))).  [para(1615(a,2),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #768 (F,wt=15): 16028 f(f(x,f(f(y,y),z)),f(x,f(y,u))) = x.  [para(297(a,1),1635(a,1,1,2)),rewrite(421(8),491(8))].

given #769 (T,wt=15): 16029 f(f(x,f(f(y,y),z)),f(x,f(u,y))) = x.  [para(301(a,1),1635(a,1,1,2)),rewrite(421(8),489(8))].

given #770 (T,wt=15): 16030 f(f(x,f(y,f(z,z))),f(x,f(z,u))) = x.  [para(380(a,1),1635(a,1,1,2)),rewrite(9188(8,R),9154(8),421(8),516(8))].

given #771 (A,wt=25): 699 f(x,f(f(x,f(y,f(x,z))),f(u,f(f(z,v),x)))) = f(x,f(y,f(x,z))).  [para(465(a,1),302(a,1,1)),rewrite(465(4),465(12))].

given #772 (F,wt=15): 16031 f(f(x,f(y,f(z,z))),f(x,f(u,z))) = x.  [para(396(a,1),1635(a,1,1,2)),rewrite(9188(8,R),9154(8),421(8),515(8))].

given #773 (F,wt=15): 16033 f(f(x,f(y,f(z,y))),f(x,f(z,u))) = x.  [para(472(a,1),1635(a,1,1,2)),rewrite(421(8),2359(8))].

given #774 (T,wt=15): 16034 f(f(x,f(y,f(z,y))),f(x,f(u,z))) = x.  [para(506(a,1),1635(a,1,1,2)),rewrite(421(8),2195(8))].

given #775 (T,wt=15): 16037 f(f(f(f(x,x),y),z),f(f(x,u),z)) = z.  [para(297(a,1),1643(a,1,1,1)),rewrite(421(8),491(8))].

given #776 (A,wt=25): 700 f(x,f(f(x,f(y,f(z,x))),f(u,f(x,f(z,v))))) = f(x,f(y,f(z,x))).  [para(469(a,1),302(a,1,1)),rewrite(469(4),469(12))].

given #777 (F,wt=15): 16038 f(f(f(f(x,x),y),z),f(f(u,x),z)) = z.  [para(301(a,1),1643(a,1,1,1)),rewrite(421(8),489(8))].

given #778 (F,wt=15): 16039 f(f(f(x,f(y,y)),z),f(f(y,u),z)) = z.  [para(380(a,1),1643(a,1,1,1)),rewrite(9188(8,R),9154(8),421(8),516(8))].

given #779 (T,wt=15): 16040 f(f(f(x,f(y,y)),z),f(f(u,y),z)) = z.  [para(396(a,1),1643(a,1,1,1)),rewrite(9188(8,R),9154(8),421(8),515(8))].

given #780 (T,wt=15): 16042 f(f(f(x,f(y,x)),z),f(f(y,u),z)) = z.  [para(472(a,1),1643(a,1,1,1)),rewrite(421(8),2359(8))].

given #781 (A,wt=37): 701 f(f(f(x,y),f(z,y)),f(f(f(x,y),u),f(f(f(x,y),f(z,y)),f(v,x)))) = f(f(f(x,y),f(z,y)),f(v,x)).  [para(302(a,1),470(a,1,1))].

given #782 (F,wt=15): 16043 f(f(f(x,f(y,x)),z),f(f(u,y),z)) = z.  [para(506(a,1),1643(a,1,1,1)),rewrite(421(8),2195(8))].

given #783 (F,wt=15): 16052 f(f(f(x,x),y),z) = f(z,f(y,f(x,y))).  [para(1752(a,1),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #784 (T,wt=15): 16053 f(f(x,f(y,x)),z) = f(z,f(f(y,y),x)).  [para(1752(a,2),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #785 (T,wt=15): 16172 f(x,f(y,f(f(f(y,y),z),x))) = f(x,x).  [para(169(a,1),2765(a,1,2,1))].

given #786 (A,wt=27): 702 f(x,f(f(x,f(y,f(f(z,u),x))),f(v,f(z,x)))) = f(x,f(y,f(f(z,u),x))).  [para(470(a,1),302(a,1,1)),rewrite(470(4),470(12))].

given #787 (F,wt=15): 16175 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x).  [para(421(a,1),2765(a,1,2,2))].

given #788 (F,wt=15): 16186 f(x,f(y,f(f(z,f(z,y)),x))) = f(x,x).  [para(1234(a,1),2765(a,1,2,2,1)),rewrite(9188(3,R),9154(3))].

given #789 (T,wt=15): 16188 f(x,f(y,f(f(z,f(y,z)),x))) = f(x,x).  [para(1373(a,1),2765(a,1,2,2,1)),rewrite(9188(3,R),9154(3))].

given #790 (T,wt=15): 16196 f(x,f(f(c_0,y),f(f(y,z),x))) = f(x,x).  [para(9188(a,2),2765(a,1,2,1))].

given #791 (A,wt=47): 704 f(f(f(x,x),y),f(f(f(f(x,x),y),f(z,f(f(f(x,x),y),f(u,x)))),f(v,f(x,x)))) = f(f(f(x,x),y),f(z,f(f(f(x,x),y),f(u,x)))).  [para(301(a,1),302(a,1,1)),rewrite(301(8),301(20))].

given #792 (F,wt=15): 16197 f(x,f(f(y,c_0),f(f(y,z),x))) = f(x,x).  [para(9198(a,2),2765(a,1,2,1))].

given #793 (F,wt=15): 16198 f(x,f(y,f(f(f(y,c_0),z),x))) = f(x,x).  [para(9193(a,1),2765(a,1,2,1))].

given #794 (T,wt=15): 16199 f(x,f(y,f(f(f(c_0,y),z),x))) = f(x,x).  [para(10579(a,1),2765(a,1,2,1))].

given #795 (T,wt=15): 16205 f(x,f(y,f(f(z,f(c_0,y)),x))) = f(x,x).  [para(10748(a,1),2765(a,1,2,2,1)),rewrite(9188(3,R),9154(3))].

given #796 (A,wt=19): 705 f(f(f(x,y),f(z,y)),f(f(u,x),f(x,y))) = f(x,y).  [para(302(a,1),490(a,1,1))].

given #797 (F,wt=15): 16208 f(x,f(y,f(f(z,f(y,c_0)),x))) = f(x,x).  [para(12437(a,1),2765(a,1,2,2,1)),rewrite(9188(3,R),9154(3))].

given #798 (F,wt=15): 16387 f(x,f(f(y,y),f(x,f(z,y)))) = f(x,x).  [para(421(a,1),2826(a,1,2,2))].

given #799 (T,wt=15): 16406 f(x,f(f(c_0,y),f(f(z,y),x))) = f(x,x).  [para(9188(a,2),2826(a,1,2,1))].

given #800 (T,wt=15): 16407 f(x,f(f(y,c_0),f(f(z,y),x))) = f(x,x).  [para(9198(a,2),2826(a,1,2,1))].

given #801 (A,wt=25): 706 f(x,f(f(x,f(y,f(z,x))),f(u,f(x,f(v,z))))) = f(x,f(y,f(z,x))).  [para(490(a,1),302(a,1,1)),rewrite(490(4),490(12))].

given #802 (F,wt=15): 16548 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0.  [para(2929(a,1),9125(a,1,2,2,2)),rewrite(421(7),365(7))].

given #803 (F,wt=15): 16897 f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)).  [para(8208(a,1),441(a,1,2)),flip(a)].

given #804 (T,wt=15): 16942 f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)).  [para(8279(a,1),441(a,1,2)),flip(a)].

given #805 (T,wt=15): 16976 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(x,y).  [para(8556(a,1),1141(a,2,2)),rewrite(9188(7,R),1227(9))].

given #806 (A,wt=37): 707 f(f(f(x,y),f(z,y)),f(f(u,f(x,y)),f(f(f(x,y),f(z,y)),f(v,x)))) = f(f(f(x,y),f(z,y)),f(v,x)).  [para(302(a,1),504(a,1,1))].

given #807 (F,wt=15): 16986 f(f(x,f(y,f(x,z))),f(c_0,f(z,x))) = c_0.  [para(8556(a,1),9122(a,1,2,2,2)),rewrite(1227(7))].

given #808 (F,wt=15): 17017 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y).  [para(5304(a,1),8556(a,1,2)),rewrite(9188(8,R)),flip(a)].

given #809 (T,wt=15): 17018 f(x,f(c_0,f(y,f(f(y,x),z)))) = f(x,y).  [para(6589(a,1),8556(a,1,2)),rewrite(9188(8,R)),flip(a)].

given #810 (T,wt=15): 17019 f(x,f(c_0,f(y,f(f(x,y),z)))) = f(x,y).  [para(7190(a,1),8556(a,1,2)),rewrite(9188(8,R)),flip(a)].

given #811 (A,wt=27): 708 f(x,f(f(x,f(y,f(f(z,u),x))),f(v,f(u,x)))) = f(x,f(y,f(f(z,u),x))).  [para(504(a,1),302(a,1,1)),rewrite(504(4),504(12))].

given #812 (F,wt=15): 17058 f(f(x,f(y,f(z,c_0))),f(c_0,f(x,z))) = c_0.  [para(9071(a,1),9122(a,1,2,2,2)),rewrite(421(8),368(8))].

given #813 (F,wt=15): 17075 f(f(x,f(f(y,c_0),z)),f(c_0,f(x,y))) = c_0.  [para(9073(a,1),9122(a,1,2,2,2)),rewrite(421(8),368(8))].

given #814 (T,wt=15): 17362 f(f(x,y),f(z,c_0)) = f(f(z,z),f(y,x)).  [para(421(a,1),9388(a,1,1))].

given #815 (T,wt=15): 17412 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0.  [para(9414(a,1),515(a,1,2)),rewrite(9188(10,R),9162(8),9188(12,R),9162(10),9188(8,R),343(8),9188(8,R),9162(6)),flip(a)].

given #816 (A,wt=33): 709 f(f(x,y),f(f(f(x,y),f(z,y)),f(u,f(f(f(x,y),f(z,y)),f(v,x))))) = f(f(x,y),f(z,y)).  [para(302(a,1),347(a,1,2,1)),rewrite(302(19))].

given #817 (F,wt=15): 17461 f(x,f(f(y,z),f(f(z,y),x))) = f(x,x).  [para(10667(a,1),9414(a,1,2,2,2)),rewrite(9162(7),421(4))].

given #818 (F,wt=15): 17487 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0.  [para(9415(a,1),515(a,1,2)),rewrite(9188(10,R),9162(8),9188(12,R),9162(10),9188(8,R),343(8),9188(8,R),9162(6)),flip(a)].

given #819 (T,wt=15): 17524 f(x,f(f(x,f(y,z)),f(c_0,z))) = f(x,x).  [para(169(a,1),9416(a,1,2,2,2))].

given #820 (T,wt=15): 17525 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x).  [para(183(a,1),9416(a,1,2,2,2)),rewrite(9154(6),421(4))].

given #821 (A,wt=35): 710 f(f(x,y),f(f(f(x,y),f(z,f(f(x,y),f(u,y)))),f(v,x))) = f(f(x,y),f(z,f(f(x,y),f(u,y)))).  [para(347(a,1),302(a,1,1)),rewrite(347(5),347(14))].

given #822 (F,wt=15): 17526 f(x,f(f(x,f(y,z)),f(c_0,y))) = f(x,x).  [para(277(a,1),9416(a,1,2,2,2))].

given #823 (F,wt=15): 17527 f(x,f(y,f(x,f(f(y,y),z)))) = f(x,x).  [para(261(a,1),9416(a,1,2,2,2)),rewrite(9154(6),421(4))].

given #824 (T,wt=15): 17528 f(x,f(y,f(x,f(z,f(y,z))))) = f(x,x).  [para(429(a,1),9416(a,1,2,2,2)),rewrite(9154(6),421(4))].

given #825 (T,wt=15): 17530 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x).  [para(462(a,1),9416(a,1,2,2,2)),rewrite(9154(6),421(4))].

given #826 (A,wt=33): 711 f(f(x,y),f(f(f(x,y),f(z,y)),f(f(f(f(x,y),f(z,y)),f(u,x)),v))) = f(f(x,y),f(z,y)).  [para(302(a,1),387(a,1,2,1)),rewrite(302(19))].

given #827 (F,wt=15): 17531 f(x,f(f(x,f(y,z)),f(y,c_0))) = f(x,x).  [para(468(a,1),9416(a,1,2,2))].

given #828 (F,wt=15): 17532 f(x,f(f(x,f(y,z)),f(z,c_0))) = f(x,x).  [para(502(a,1),9416(a,1,2,2))].

given #829 (T,wt=15): 17565 f(x,f(y,f(x,f(f(y,c_0),z)))) = f(x,x).  [para(9192(a,1),9416(a,1,2,2,2)),rewrite(9154(7),421(5))].

given #830 (T,wt=15): 17566 f(x,f(y,f(x,f(z,f(y,c_0))))) = f(x,x).  [para(9195(a,1),9416(a,1,2,2,2)),rewrite(9154(7),421(5))].

given #831 (A,wt=35): 712 f(f(x,y),f(f(f(x,y),f(z,f(f(x,y),f(y,u)))),f(v,x))) = f(f(x,y),f(z,f(f(x,y),f(y,u)))).  [para(387(a,1),302(a,1,1)),rewrite(387(5),387(14))].

given #832 (F,wt=15): 17567 f(x,f(y,f(x,f(z,f(c_0,y))))) = f(x,x).  [para(10589(a,1),9416(a,1,2,2,2)),rewrite(9162(8),421(5))].

given #833 (F,wt=15): 17568 f(x,f(y,f(x,f(f(c_0,y),z)))) = f(x,x).  [para(10619(a,1),9416(a,1,2,2,2)),rewrite(9162(8),421(5))].

given #834 (T,wt=15): 17576 f(x,f(f(x,f(y,z)),f(z,y))) = f(x,x).  [para(10667(a,1),9416(a,1,2,2,2)),rewrite(9162(7))].

given #835 (T,wt=15): 17577 f(f(x,x),f(y,f(f(z,x),f(u,x)))) = x.  [para(10693(a,1),9416(a,1,2,1)),rewrite(9162(9),9188(9,R),9154(9))].

given #836 (A,wt=57): 713 f(f(f(x,y),f(z,y)),f(f(f(f(x,y),f(z,y)),f(u,f(f(f(x,y),f(z,y)),f(v,x)))),f(w,f(x,y)))) = f(f(f(x,y),f(z,y)),f(u,f(f(f(x,y),f(z,y)),f(v,x)))).  [para(302(a,1),302(a,1,1)),rewrite(302(10),302(24))].

given #837 (F,wt=15): 17579 f(f(x,x),f(y,f(f(x,z),f(u,x)))) = x.  [para(14654(a,1),9416(a,1,2,1)),rewrite(9162(9),9188(9,R),9154(9))].

given #838 (F,wt=15): 17580 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x.  [para(14655(a,1),9416(a,1,2,1)),rewrite(9162(9),9188(9,R),9154(9))].

given #839 (T,wt=15): 17581 f(f(x,c_0),f(y,f(f(z,x),f(u,x)))) = x.  [para(14685(a,1),9416(a,1,2,1)),rewrite(9162(10),9188(12,R),9156(11))].

given #840 (T,wt=15): 17582 f(f(c_0,x),f(y,f(f(z,x),f(u,x)))) = x.  [para(14690(a,1),9416(a,1,2,1)),rewrite(9162(10),9188(12,R),9162(11))].

given #841 (A,wt=17): 714 f(f(x,y),f(y,f(f(f(x,y),f(x,z)),u))) = y.  [para(468(a,1),324(a,1,1))].

given #842 (F,wt=15): 17584 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x.  [para(14997(a,1),9416(a,1,2,1)),rewrite(9162(9),9188(9,R),9154(9))].

given #843 (F,wt=15): 17585 f(f(x,c_0),f(y,f(f(x,z),f(u,x)))) = x.  [para(15019(a,1),9416(a,1,2,1)),rewrite(9162(10),9188(12,R),9156(11))].

given #844 (T,wt=15): 17586 f(f(c_0,x),f(y,f(f(x,z),f(u,x)))) = x.  [para(15023(a,1),9416(a,1,2,1)),rewrite(9162(10),9188(12,R),9162(11))].

given #845 (T,wt=15): 17587 f(f(x,c_0),f(y,f(f(z,x),f(x,u)))) = x.  [para(15065(a,1),9416(a,1,2,1)),rewrite(9162(10),9188(12,R),9156(11))].

given #846 (A,wt=23): 719 f(f(x,y),f(f(f(x,y),f(x,z)),f(y,u))) = f(f(x,y),f(x,z)).  [para(468(a,1),451(a,1,1))].

given #847 (F,wt=15): 17588 f(f(c_0,x),f(y,f(f(z,x),f(x,u)))) = x.  [para(15069(a,1),9416(a,1,2,1)),rewrite(9162(10),9188(12,R),9162(11))].

given #848 (F,wt=15): 17590 f(f(x,c_0),f(y,f(f(x,z),f(x,u)))) = x.  [para(15246(a,1),9416(a,1,2,1)),rewrite(9162(10),9188(12,R),9156(11))].

given #849 (T,wt=15): 17591 f(f(c_0,x),f(y,f(f(x,z),f(x,u)))) = x.  [para(15250(a,1),9416(a,1,2,1)),rewrite(9162(10),9188(12,R),9162(11))].

given #850 (T,wt=15): 17624 f(f(x,x),f(f(f(y,x),f(z,x)),u)) = x.  [para(10693(a,1),9417(a,1,2,1)),rewrite(9162(9),9188(9,R),9154(9))].

given #851 (A,wt=31): 720 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(294(a,1),468(a,1,2,1)),rewrite(294(23))].

given #852 (F,wt=15): 17625 f(f(x,x),f(f(f(x,y),f(z,x)),u)) = x.  [para(14654(a,1),9417(a,1,2,1)),rewrite(9162(9),9188(9,R),9154(9))].

given #853 (F,wt=15): 17626 f(f(x,x),f(f(f(y,x),f(x,z)),u)) = x.  [para(14655(a,1),9417(a,1,2,1)),rewrite(9162(9),9188(9,R),9154(9))].

given #854 (T,wt=15): 17627 f(f(x,c_0),f(f(f(y,x),f(z,x)),u)) = x.  [para(14685(a,1),9417(a,1,2,1)),rewrite(9162(10),9188(12,R),9156(11))].

given #855 (T,wt=15): 17628 f(f(c_0,x),f(f(f(y,x),f(z,x)),u)) = x.  [para(14690(a,1),9417(a,1,2,1)),rewrite(9162(10),9188(12,R),9162(11))].

given #856 (A,wt=27): 721 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(468(a,1),452(a,1,2)),rewrite(421(5),421(8))].

given #857 (F,wt=15): 17629 f(f(x,x),f(f(f(x,y),f(x,z)),u)) = x.  [para(14997(a,1),9417(a,1,2,1)),rewrite(9162(9),9188(9,R),9154(9))].

given #858 (F,wt=15): 17630 f(f(x,c_0),f(f(f(x,y),f(z,x)),u)) = x.  [para(15019(a,1),9417(a,1,2,1)),rewrite(9162(10),9188(12,R),9156(11))].

given #859 (T,wt=15): 17631 f(f(c_0,x),f(f(f(x,y),f(z,x)),u)) = x.  [para(15023(a,1),9417(a,1,2,1)),rewrite(9162(10),9188(12,R),9162(11))].

given #860 (T,wt=15): 17632 f(f(x,c_0),f(f(f(y,x),f(x,z)),u)) = x.  [para(15065(a,1),9417(a,1,2,1)),rewrite(9162(10),9188(12,R),9156(11))].

given #861 (A,wt=23): 722 f(f(x,y),f(f(f(x,y),f(x,z)),f(u,y))) = f(f(x,y),f(x,z)).  [para(468(a,1),453(a,1,1))].

given #862 (F,wt=15): 17633 f(f(c_0,x),f(f(f(y,x),f(x,z)),u)) = x.  [para(15069(a,1),9417(a,1,2,1)),rewrite(9162(10),9188(12,R),9162(11))].

given #863 (F,wt=15): 17634 f(f(x,c_0),f(f(f(x,y),f(x,z)),u)) = x.  [para(15246(a,1),9417(a,1,2,1)),rewrite(9162(10),9188(12,R),9156(11))].

given #864 (T,wt=15): 17635 f(f(c_0,x),f(f(f(x,y),f(x,z)),u)) = x.  [para(15250(a,1),9417(a,1,2,1)),rewrite(9162(10),9188(12,R),9162(11))].

given #865 (T,wt=15): 17681 f(f(f(x,y),z),f(c_0,f(z,f(y,x)))) = c_0.  [para(9599(a,1),9122(a,1,2,2,2)),rewrite(421(8),10728(8))].

given #866 (A,wt=27): 723 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(468(a,1),454(a,1,2)),rewrite(421(5),421(8))].

given #867 (F,wt=15): 17717 f(f(f(x,y),z),f(z,f(f(y,x),u))) = z.  [para(9599(a,1),523(a,1,2,1)),rewrite(421(8),14833(8),9599(13))].

given #868 (F,wt=15): 17725 f(f(f(x,y),z),f(z,f(u,f(y,x)))) = z.  [para(9599(a,1),528(a,1,2,1)),rewrite(421(8),14833(8),9599(13))].

given #869 (T,wt=15): 17731 f(f(f(x,y),z),f(f(f(y,x),u),z)) = z.  [para(9599(a,1),565(a,1,2,2)),rewrite(421(8),14833(8),9599(13))].

given #870 (T,wt=15): 17734 f(f(f(x,y),z),f(f(u,f(y,x)),z)) = z.  [para(9599(a,1),566(a,1,2,2)),rewrite(421(8),14833(8),9599(13))].

given #871 (A,wt=23): 726 f(f(x,y),f(f(y,z),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)).  [para(468(a,1),470(a,1,1))].

given #872 (F,wt=15): 17741 f(f(x,f(y,z)),f(x,f(u,f(z,y)))) = x.  [para(9650(a,1),346(a,1,2,1)),rewrite(14992(8),9650(13))].

given #873 (F,wt=15): 17743 f(f(x,f(y,z)),f(x,f(f(z,y),u))) = x.  [para(9650(a,1),389(a,1,2,1)),rewrite(14992(8),17741(13))].

given #874 (T,wt=15): 17745 f(f(x,f(y,z)),f(c_0,f(x,f(z,y)))) = c_0.  [para(9650(a,1),9125(a,1,2,2,2)),rewrite(421(8),10728(8))].

given #875 (T,wt=15): 17821 f(f(x,f(y,z)),f(f(f(z,y),u),x)) = x.  [para(9925(a,1),570(a,1,2,2)),rewrite(14992(8),9925(13))].

given #876 (A,wt=23): 730 f(f(x,y),f(f(z,y),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)).  [para(468(a,1),504(a,1,1))].

given #877 (F,wt=15): 17852 f(f(x,f(y,z)),f(f(u,f(z,y)),x)) = x.  [para(9925(a,1),571(a,1,2,2)),rewrite(14992(8),9925(13))].

given #878 (F,wt=15): 17862 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0.  [para(10727(a,1),10623(a,1,2,2))].

given #879 (T,wt=15): 17878 f(x,f(c_0,f(y,f(y,f(f(x,x),z))))) = c_0.  [para(10727(a,1),10624(a,1,2,2))].

given #880 (T,wt=15): 17918 f(x,f(c_0,f(y,f(y,f(z,f(x,c_0)))))) = c_0.  [para(10727(a,1),10641(a,1,2,2))].

given #881 (A,wt=19): 732 f(x,f(f(y,x),f(z,f(f(y,x),f(y,u))))) = f(y,x).  [para(468(a,1),347(a,1,2,1)),rewrite(468(11))].

given #882 (F,wt=15): 17929 f(x,f(c_0,f(y,f(y,f(f(x,c_0),z))))) = c_0.  [para(10727(a,1),10642(a,1,2,2))].

given #883 (F,wt=15): 17975 f(x,f(c_0,f(y,f(y,f(z,f(c_0,x)))))) = c_0.  [para(10727(a,1),10695(a,1,2,2))].

given #884 (T,wt=15): 17993 f(x,f(c_0,f(y,f(y,f(f(c_0,x),z))))) = c_0.  [para(10727(a,1),10696(a,1,2,2))].

given #885 (T,wt=15): 18000 f(f(x,f(f(c_0,y),z)),f(x,f(y,u))) = x.  [para(10701(a,1),343(a,1,2,2))].

given #886 (A,wt=19): 733 f(f(f(x,y),f(z,y)),f(f(x,y),f(x,u))) = f(x,y).  [para(347(a,1),468(a,1,2,1)),rewrite(347(11))].

given #887 (F,wt=15): 18001 f(f(f(f(c_0,x),y),z),f(z,f(x,u))) = z.  [para(10701(a,1),453(a,1,2,2))].

given #888 (F,wt=15): 18002 f(f(x,f(f(c_0,y),z)),f(f(y,u),x)) = x.  [para(10701(a,1),454(a,1,2,1))].

given #889 (T,wt=15): 18003 f(f(f(x,y),z),f(z,f(f(c_0,x),u))) = z.  [para(10701(a,1),464(a,1,1,1))].

given #890 (T,wt=15): 18004 f(f(x,f(y,z)),f(f(f(c_0,y),u),x)) = x.  [para(10701(a,1),490(a,1,1,2))].

given #891 (A,wt=19): 734 f(x,f(f(y,x),f(f(f(y,x),f(y,z)),u))) = f(y,x).  [para(468(a,1),387(a,1,2,1)),rewrite(468(11))].

given #892 (F,wt=15): 18005 f(f(f(f(c_0,x),y),z),f(f(x,u),z)) = z.  [para(10701(a,1),504(a,1,2,1))].

given #893 (F,wt=15): 18013 f(f(x,f(y,f(c_0,z))),f(x,f(z,u))) = x.  [para(10701(a,1),640(a,1,2,2))].

given #894 (T,wt=15): 18025 f(f(f(x,f(c_0,y)),z),f(z,f(y,u))) = z.  [para(10701(a,1),773(a,1,2,2))].

given #895 (T,wt=15): 18027 f(f(x,f(y,z)),f(x,f(f(c_0,y),u))) = x.  [para(10701(a,1),1004(a,1,1,2))].

given #896 (A,wt=19): 735 f(f(f(x,y),f(y,z)),f(f(x,y),f(x,u))) = f(x,y).  [para(387(a,1),468(a,1,2,1)),rewrite(387(11))].

given #897 (F,wt=15): 18031 f(f(x,f(y,z)),f(x,f(u,f(c_0,y)))) = x.  [para(10701(a,1),5304(a,1,1,2))].

given #898 (F,wt=15): 18033 f(f(x,f(y,z)),f(f(u,f(c_0,y)),x)) = x.  [para(10701(a,1),5393(a,1,1,2))].

given #899 (T,wt=15): 18050 f(f(x,f(y,f(c_0,z))),f(f(z,u),x)) = x.  [para(10706(a,1),454(a,1,2,1))].

given #900 (T,wt=15): 18051 f(f(f(x,y),z),f(z,f(u,f(c_0,x)))) = z.  [para(10706(a,1),464(a,1,1,1))].

given #901 (A,wt=35): 736 f(f(x,y),f(f(f(x,y),f(z,f(f(x,y),f(x,u)))),f(v,y))) = f(f(x,y),f(z,f(f(x,y),f(x,u)))).  [para(468(a,1),302(a,1,1)),rewrite(468(5),468(14))].

given #902 (F,wt=15): 18052 f(f(f(x,f(c_0,y)),z),f(f(y,u),z)) = z.  [para(10706(a,1),504(a,1,2,1))].

given #903 (F,wt=15): 18127 f(f(x,f(y,f(c_0,z))),f(x,f(u,z))) = x.  [para(10711(a,1),343(a,1,2,2))].

given #904 (T,wt=15): 18128 f(f(f(x,f(c_0,y)),z),f(z,f(u,y))) = z.  [para(10711(a,1),453(a,1,2,2))].

given #905 (T,wt=15): 18129 f(f(x,f(y,f(c_0,z))),f(f(u,z),x)) = x.  [para(10711(a,1),454(a,1,2,1))].

given #906 (A,wt=33): 737 f(f(f(f(x,y),f(z,y)),f(u,x)),f(f(f(x,y),f(z,y)),f(f(x,y),v))) = f(f(x,y),f(z,y)).  [para(302(a,1),468(a,1,2,1)),rewrite(302(19))].

given #907 (F,wt=15): 18130 f(f(f(x,y),z),f(z,f(u,f(c_0,y)))) = z.  [para(10711(a,1),464(a,1,1,1))].

given #908 (F,wt=15): 18131 f(f(x,f(y,z)),f(f(u,f(c_0,z)),x)) = x.  [para(10711(a,1),490(a,1,1,2))].

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

given #910 (T,wt=15): 18133 f(f(x,f(y,z)),f(x,f(f(c_0,z),u))) = x.  [para(10711(a,1),320(a,1,1,2))].

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

given #912 (F,wt=15): 18140 f(f(f(f(c_0,x),y),z),f(z,f(u,x))) = z.  [para(10711(a,1),635(a,1,2,2))].

given #913 (F,wt=15): 18151 f(f(x,f(f(c_0,y),z)),f(x,f(u,y))) = x.  [para(10711(a,1),755(a,1,2,2))].

given #914 (T,wt=15): 18154 f(f(x,f(y,z)),f(x,f(u,f(c_0,z)))) = x.  [para(10711(a,1),1003(a,1,1,2))].

given #915 (T,wt=15): 18156 f(f(x,f(y,z)),f(f(f(c_0,z),u),x)) = x.  [para(10711(a,1),1006(a,1,1,2))].

given #916 (A,wt=23): 742 f(f(x,y),f(f(f(y,z),f(x,y)),f(x,u))) = f(f(y,z),f(x,y)).  [para(499(a,1),451(a,1,1))].

given #917 (F,wt=15): 18170 f(f(x,f(f(c_0,y),z)),f(f(u,y),x)) = x.  [para(10712(a,1),454(a,1,2,1))].

given #918 (F,wt=15): 18171 f(f(f(x,y),z),f(z,f(f(c_0,y),u))) = z.  [para(10712(a,1),464(a,1,1,1))].

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

given #920 (T,wt=15): 18298 f(f(x,y),f(c_0,z)) = f(f(z,z),f(y,x)).  [para(421(a,1),10958(a,1,1))].

given #921 (A,wt=27): 743 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(499(a,1),452(a,1,2)),rewrite(421(5),421(8))].

given #922 (F,wt=15): 18340 f(f(x,f(y,z)),f(c_0,f(x,f(y,y)))) = c_0.  [para(1141(a,2),11417(a,1,2,2))].

given #923 (F,wt=15): 18343 f(f(x,f(y,z)),f(c_0,f(f(y,y),x))) = c_0.  [para(1234(a,2),11417(a,1,2,2))].

given #924 (T,wt=15): 18344 f(f(x,f(f(y,y),z)),f(c_0,f(y,x))) = c_0.  [para(1235(a,1),11417(a,1,2,2,2)),rewrite(365(7))].

given #925 (T,wt=15): 18347 f(x,f(c_0,f(y,f(x,f(z,f(z,y)))))) = c_0.  [para(549(a,1),11417(a,1,1)),rewrite(10727(10,R),9154(7),421(5))].

given #926 (A,wt=23): 744 f(f(x,y),f(f(f(y,z),f(x,y)),f(u,x))) = f(f(y,z),f(x,y)).  [para(499(a,1),453(a,1,1))].

given #927 (F,wt=15): 18357 f(f(x,f(f(y,c_0),z)),f(c_0,f(y,x))) = c_0.  [para(9158(a,1),11417(a,1,2,2,2)),rewrite(365(8))].

given #928 (F,wt=15): 18359 f(f(x,f(y,z)),f(c_0,f(f(y,c_0),x))) = c_0.  [para(9161(a,2),11417(a,1,2,2))].

given #929 (T,wt=15): 18360 f(f(x,f(y,z)),f(c_0,f(x,f(y,c_0)))) = c_0.  [para(9165(a,2),11417(a,1,2,2))].

given #930 (T,wt=15): 18368 f(f(x,f(f(c_0,y),z)),f(c_0,f(x,y))) = c_0.  [para(10718(a,2),11417(a,1,1,2)),rewrite(1227(8))].

given #931 (A,wt=27): 745 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(499(a,1),454(a,1,2)),rewrite(421(5),421(8))].

given #932 (F,wt=15): 18369 f(f(x,f(y,z)),f(c_0,f(x,f(c_0,y)))) = c_0.  [para(10727(a,2),11417(a,1,2,2))].

given #933 (F,wt=15): 18371 f(f(x,f(y,z)),f(c_0,f(f(c_0,y),x))) = c_0.  [para(10729(a,2),11417(a,1,2,2))].

given #934 (T,wt=15): 18372 f(f(x,f(f(c_0,y),z)),f(c_0,f(y,x))) = c_0.  [para(10731(a,1),11417(a,1,2,2,2)),rewrite(365(8))].

given #935 (T,wt=15): 18374 f(f(x,f(y,f(c_0,z))),f(c_0,f(x,z))) = c_0.  [para(10748(a,1),11417(a,1,1,2)),rewrite(1227(8))].

given #936 (A,wt=23): 747 f(f(x,y),f(f(x,z),f(f(y,u),f(x,y)))) = f(f(y,u),f(x,y)).  [para(499(a,1),470(a,1,1))].

given #937 (F,wt=15): 18410 f(f(x,f(y,z)),f(c_0,f(x,f(z,z)))) = c_0.  [para(1141(a,2),11418(a,1,2,2))].

given #938 (F,wt=15): 18413 f(f(x,f(y,z)),f(c_0,f(f(z,z),x))) = c_0.  [para(1234(a,2),11418(a,1,2,2))].

given #939 (T,wt=15): 18414 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0.  [para(1235(a,1),11418(a,1,2,2,2)),rewrite(365(7))].

given #940 (T,wt=15): 18416 f(f(x,f(y,f(z,x))),f(c_0,f(x,z))) = c_0.  [para(1235(a,2),11418(a,1,2,2,2)),rewrite(1227(7))].

given #941 (A,wt=23): 748 f(f(x,y),f(f(z,x),f(f(y,u),f(x,y)))) = f(f(y,u),f(x,y)).  [para(499(a,1),504(a,1,1))].

given #942 (F,wt=15): 18430 f(f(x,f(y,f(z,c_0))),f(c_0,f(z,x))) = c_0.  [para(9158(a,1),11418(a,1,2,2,2)),rewrite(365(8))].

given #943 (F,wt=15): 18434 f(f(x,f(y,z)),f(c_0,f(f(z,c_0),x))) = c_0.  [para(9161(a,2),11418(a,1,2,2))].

given #944 (T,wt=15): 18435 f(f(x,f(y,z)),f(c_0,f(x,f(z,c_0)))) = c_0.  [para(9165(a,2),11418(a,1,2,2))].

given #945 (T,wt=15): 18444 f(f(x,f(y,z)),f(c_0,f(x,f(c_0,z)))) = c_0.  [para(10727(a,2),11418(a,1,2,2))].

given #946 (A,wt=19): 749 f(x,f(f(x,y),f(z,f(f(y,u),f(x,y))))) = f(x,y).  [para(499(a,1),347(a,1,2,1)),rewrite(499(11))].

given #947 (F,wt=15): 18448 f(f(x,f(y,z)),f(c_0,f(f(c_0,z),x))) = c_0.  [para(10729(a,2),11418(a,1,2,2))].

given #948 (F,wt=15): 18449 f(f(x,f(y,f(c_0,z))),f(c_0,f(z,x))) = c_0.  [para(10731(a,1),11418(a,1,2,2,2)),rewrite(365(8))].

given #949 (T,wt=15): 18507 f(f(f(x,y),z),f(c_0,f(z,f(x,x)))) = c_0.  [para(1141(a,2),11423(a,1,2,2))].

given #950 (T,wt=15): 18509 f(f(f(x,y),z),f(c_0,f(f(x,x),z))) = c_0.  [para(1234(a,2),11423(a,1,2,2))].

given #951 (A,wt=19): 750 f(x,f(f(x,y),f(f(f(y,z),f(x,y)),u))) = f(x,y).  [para(499(a,1),387(a,1,2,1)),rewrite(499(11))].

given #952 (F,wt=15): 18518 f(f(f(x,y),z),f(c_0,f(f(x,c_0),z))) = c_0.  [para(9161(a,2),11423(a,1,2,2))].

given #953 (F,wt=15): 18519 f(f(f(f(x,c_0),y),z),f(c_0,f(z,x))) = c_0.  [para(9163(a,1),11423(a,1,2,2))].

given #954 (T,wt=15): 18520 f(f(f(x,y),z),f(c_0,f(z,f(x,c_0)))) = c_0.  [para(9165(a,2),11423(a,1,2,2))].

given #955 (T,wt=15): 18521 f(f(f(f(c_0,x),y),z),f(c_0,f(z,x))) = c_0.  [para(10718(a,2),11423(a,1,1,1)),rewrite(1227(8))].

given #956 (A,wt=35): 752 f(f(x,y),f(f(f(x,y),f(z,f(f(y,u),f(x,y)))),f(v,x))) = f(f(x,y),f(z,f(f(y,u),f(x,y)))).  [para(499(a,1),302(a,1,1)),rewrite(499(5),499(14))].

given #957 (F,wt=15): 18522 f(f(f(x,y),z),f(c_0,f(z,f(c_0,x)))) = c_0.  [para(10727(a,2),11423(a,1,2,2))].

given #958 (F,wt=15): 18523 f(f(f(x,y),z),f(c_0,f(f(c_0,x),z))) = c_0.  [para(10729(a,2),11423(a,1,2,2))].

given #959 (T,wt=15): 18525 f(f(f(x,f(c_0,y)),z),f(c_0,f(z,y))) = c_0.  [para(10748(a,1),11423(a,1,1,1)),rewrite(1227(8))].

given #960 (T,wt=15): 18526 f(f(f(x,f(y,c_0)),z),f(c_0,f(z,y))) = c_0.  [para(12437(a,1),11423(a,1,1,1)),rewrite(1227(8))].

given #961 (A,wt=19): 753 f(f(f(x,y),f(z,x)),f(f(z,x),f(z,u))) = f(z,x).  [para(499(a,1),468(a,1,2,1)),rewrite(499(11))].

given #962 (F,wt=15): 18535 f(x,f(c_0,f(f(x,f(y,z)),f(z,y)))) = c_0.  [para(9925(a,1),11423(a,1,1)),rewrite(14992(9))].

given #963 (F,wt=15): 18586 f(f(f(x,y),z),f(c_0,f(z,f(y,y)))) = c_0.  [para(1141(a,2),11427(a,1,2,2))].

given #964 (T,wt=15): 18588 f(f(f(x,y),z),f(c_0,f(f(y,y),z))) = c_0.  [para(1234(a,2),11427(a,1,2,2))].

given #965 (T,wt=15): 18596 f(f(f(x,y),z),f(c_0,f(f(y,c_0),z))) = c_0.  [para(9161(a,2),11427(a,1,2,2))].

given #966 (A,wt=21): 759 f(x,f(f(y,y),f(f(z,f(y,z)),x))) = f(f(z,f(y,z)),x).  [para(429(a,1),502(a,1,2,2)),rewrite(421(5))].

given #967 (F,wt=15): 18599 f(f(f(x,y),z),f(c_0,f(z,f(y,c_0)))) = c_0.  [para(9165(a,2),11427(a,1,2,2))].

given #968 (F,wt=15): 18603 f(f(f(x,y),z),f(c_0,f(z,f(c_0,y)))) = c_0.  [para(10727(a,2),11427(a,1,2,2))].

given #969 (T,wt=15): 18606 f(f(f(x,y),z),f(c_0,f(f(c_0,y),z))) = c_0.  [para(10729(a,2),11427(a,1,2,2))].

given #970 (T,wt=15): 18708 f(f(c_0,f(x,y)),z) = f(x,f(c_0,f(y,z))).  [para(11431(a,1),462(a,1,2,2)),rewrite(421(9),421(10),17512(10),17472(7),9188(17,R),9162(12))].

given #971 (A,wt=23): 760 f(f(x,y),f(f(f(x,y),f(z,x)),f(y,u))) = f(f(x,y),f(z,x)).  [para(502(a,1),451(a,1,1))].

given #972 (F,wt=15): 18723 f(x,f(c_0,f(y,f(c_0,f(f(y,x),z))))) = c_0.  [para(9122(a,1),11431(a,1,1)),rewrite(18708(8),9162(12))].

given #973 (F,wt=15): 18724 f(x,f(c_0,f(y,f(c_0,f(f(x,y),z))))) = c_0.  [para(9125(a,1),11431(a,1,1)),rewrite(18708(8),9162(12))].

given #974 (T,wt=15): 18787 f(x,f(c_0,f(y,f(c_0,f(z,f(y,x)))))) = c_0.  [back_rewrite(18463),rewrite(18708(8),18708(9),10728(7))].

given #975 (T,wt=15): 18871 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))).  [back_rewrite(17637),rewrite(18708(7),12919(7),18708(8))].

given #976 (A,wt=31): 761 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(294(a,1),502(a,1,2,1)),rewrite(294(23))].

given #977 (F,wt=15): 18881 f(x,f(c_0,f(y,z))) = f(y,f(c_0,f(x,z))).  [back_rewrite(17512),rewrite(18708(7),12917(7),18708(8))].

given #978 (F,wt=15): 18916 f(x,f(y,f(c_0,f(z,f(x,y))))) = f(x,x).  [back_rewrite(16928),rewrite(18708(5))].

given #979 (T,wt=15): 18932 f(x,f(c_0,f(y,f(z,f(z,x))))) = f(x,y).  [back_rewrite(16621),rewrite(18708(9),10728(7))].

given #980 (T,wt=15): 18938 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x).  [back_rewrite(16425),rewrite(18708(7),18708(8),10728(6))].

given #981 (A,wt=27): 762 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(502(a,1),452(a,1,2)),rewrite(421(5),421(8))].

given #982 (F,wt=15): 19021 f(x,f(c_0,f(y,f(f(x,x),z)))) = f(x,y).  [back_rewrite(15097),rewrite(18708(6))].

given #983 (F,wt=15): 19022 f(x,f(c_0,f(y,f(z,f(x,x))))) = f(x,y).  [back_rewrite(15096),rewrite(18708(6))].

given #984 (T,wt=15): 19044 f(x,f(c_0,f(y,f(y,f(f(x,y),z))))) = c_0.  [back_rewrite(14993),rewrite(18708(7))].

given #985 (T,wt=15): 19065 f(x,f(c_0,f(y,f(z,f(x,z))))) = f(x,y).  [back_rewrite(14888),rewrite(18708(6))].

given #986 (A,wt=23): 763 f(f(x,y),f(f(f(x,y),f(z,x)),f(u,y))) = f(f(x,y),f(z,x)).  [para(502(a,1),453(a,1,1))].

given #987 (F,wt=15): 19069 f(x,f(y,f(c_0,f(f(x,y),z)))) = f(x,x).  [back_rewrite(14757),rewrite(18708(5))].

given #988 (F,wt=15): 19070 f(x,f(y,f(c_0,f(f(y,x),z)))) = f(x,x).  [back_rewrite(14755),rewrite(18708(5))].

given #989 (T,wt=15): 19093 f(x,f(c_0,f(y,f(y,f(z,f(x,y)))))) = c_0.  [back_rewrite(14650),rewrite(18708(7))].

given #990 (T,wt=15): 19103 f(f(x,f(c_0,f(y,z))),f(f(y,x),z)) = z.  [back_rewrite(14421),rewrite(18708(4))].

given #991 (A,wt=27): 764 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(502(a,1),454(a,1,2)),rewrite(421(5),421(8))].

given #992 (F,wt=15): 19105 f(x,f(c_0,f(y,f(z,f(x,c_0))))) = f(x,y).  [back_rewrite(14056),rewrite(18708(7))].

given #993 (F,wt=15): 19107 f(x,f(c_0,f(y,f(f(x,c_0),z)))) = f(x,y).  [back_rewrite(13365),rewrite(18708(7))].

given #994 (T,wt=15): 19126 f(x,f(c_0,f(y,f(z,f(c_0,x))))) = f(x,y).  [back_rewrite(10706),rewrite(18708(7))].

given #995 (T,wt=15): 19127 f(x,f(c_0,f(y,f(f(c_0,x),z)))) = f(x,y).  [back_rewrite(10701),rewrite(18708(7))].

given #996 (A,wt=21): 766 f(x,f(f(y,y),f(f(z,f(z,y)),x))) = f(f(z,f(z,y)),x).  [para(462(a,1),502(a,1,2,2)),rewrite(421(5))].

given #997 (F,wt=15): 19156 f(f(x,f(c_0,f(y,z))),f(z,f(y,x))) = z.  [back_rewrite(9925),rewrite(18708(4))].

given #998 (F,wt=15): 19258 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))).  [para(584(a,1),10729(a,1,1)),rewrite(421(3),18708(4),421(7),18708(11),19105(11))].

given #999 (T,wt=15): 19339 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0.  [para(10727(a,1),11439(a,1,2,2))].

given #1000 (T,wt=15): 19357 f(x,f(c_0,f(y,f(x,f(z,f(y,z)))))) = c_0.  [para(11492(a,1),421(a,1)),rewrite(18708(8)),flip(a)].

given #1001 (A,wt=23): 768 f(f(x,y),f(f(y,z),f(f(x,y),f(u,x)))) = f(f(x,y),f(u,x)).  [para(502(a,1),470(a,1,1))].

given #1002 (F,wt=15): 19358 f(f(x,f(y,f(z,y))),f(c_0,f(z,x))) = c_0.  [para(421(a,1),11492(a,1,2,2))].

given #1003 (F,wt=15): 19436 f(f(x,f(y,z)),f(c_0,f(f(z,y),x))) = c_0.  [para(9599(a,1),11492(a,1,1)),rewrite(14992(9))].

given #1004 (T,wt=15): 19524 f(f(f(x,y),z),f(c_0,f(f(y,x),z))) = c_0.  [para(9599(a,1),11493(a,1,1)),rewrite(421(9),18708(9),17018(9))].

given #1005 (T,wt=15): 19562 f(x,f(c_0,f(y,f(y,f(z,f(x,z)))))) = c_0.  [para(9122(a,1),11496(a,1,1)),rewrite(421(9),9162(11))].

given #1006 (A,wt=23): 772 f(f(x,y),f(f(z,y),f(f(x,y),f(u,x)))) = f(f(x,y),f(u,x)).  [para(502(a,1),504(a,1,1))].

given #1007 (F,wt=15): 19596 f(x,f(c_0,f(y,f(c_0,f(z,f(x,y)))))) = c_0.  [para(11430(a,1),11496(a,1,1)),rewrite(421(10),9162(12))].

given #1008 (F,wt=15): 19640 f(x,f(c_0,f(y,f(x,f(z,f(y,c_0)))))) = c_0.  [para(9071(a,1),11497(a,1,1)),rewrite(421(6))].

given #1009 (T,wt=15): 19642 f(x,f(c_0,f(y,f(x,f(f(y,c_0),z))))) = c_0.  [para(9073(a,1),11497(a,1,1)),rewrite(421(6))].

given #1010 (T,wt=15): 19660 f(f(x,f(c_0,f(y,z))),f(f(x,y),z)) = z.  [para(365(a,1),11500(a,1,2,1)),rewrite(421(3),18708(4))].

given #1011 (A,wt=19): 774 f(x,f(f(y,x),f(z,f(f(y,x),f(u,y))))) = f(y,x).  [para(502(a,1),347(a,1,2,1)),rewrite(502(11))].

given #1012 (F,wt=15): 19665 f(x,f(c_0,f(y,f(x,f(f(y,y),z))))) = c_0.  [para(11563(a,1),421(a,1)),rewrite(18708(8)),flip(a)].

given #1013 (F,wt=15): 19669 f(x,f(c_0,f(y,f(x,f(z,f(y,y)))))) = c_0.  [para(490(a,1),11563(a,1,1)),rewrite(421(5))].

given #1014 (T,wt=15): 19774 f(x,f(c_0,f(y,f(y,f(f(y,x),z))))) = c_0.  [para(11573(a,1),11497(a,1,1)),rewrite(421(9),9162(11))].

given #1015 (T,wt=15): 19781 f(x,f(c_0,f(y,f(y,f(z,f(y,x)))))) = c_0.  [para(11574(a,1),11497(a,1,1)),rewrite(421(9),9162(11))].

given #1016 (A,wt=19): 775 f(f(f(x,y),f(z,y)),f(f(x,y),f(u,x))) = f(x,y).  [para(347(a,1),502(a,1,2,1)),rewrite(347(11))].

given #1017 (F,wt=15): 19783 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))).  [para(11580(a,1),462(a,1,2,2)),rewrite(421(9),18708(10),18708(8),12917(8),12919(7),9188(17,R),9162(12))].

given #1018 (F,wt=15): 19849 f(x,f(c_0,f(f(x,f(y,z)),f(c_0,z)))) = c_0.  [para(169(a,1),11584(a,1,2,2,2,2))].

given #1019 (T,wt=15): 19850 f(x,f(c_0,f(f(x,f(y,z)),f(c_0,y)))) = c_0.  [para(277(a,1),11584(a,1,2,2,2,2))].

given #1020 (T,wt=15): 19865 f(x,f(c_0,f(f(x,f(y,z)),f(y,c_0)))) = c_0.  [para(468(a,1),11584(a,1,2,2,2))].

given #1021 (A,wt=19): 776 f(x,f(f(y,x),f(f(f(y,x),f(z,y)),u))) = f(y,x).  [para(502(a,1),387(a,1,2,1)),rewrite(502(11))].

given #1022 (F,wt=15): 19866 f(x,f(c_0,f(f(x,f(y,z)),f(z,c_0)))) = c_0.  [para(502(a,1),11584(a,1,2,2,2))].

given #1023 (F,wt=15): 19910 f(x,f(c_0,f(y,f(x,f(z,f(c_0,y)))))) = c_0.  [para(10589(a,1),11584(a,1,2,2,2,2)),rewrite(9162(9),421(6))].

given #1024 (T,wt=15): 19911 f(x,f(c_0,f(y,f(x,f(f(c_0,y),z))))) = c_0.  [para(10619(a,1),11584(a,1,2,2,2,2)),rewrite(9162(9),421(6))].

given #1025 (T,wt=15): 20089 f(x,f(c_0,f(f(y,y),f(x,f(z,y))))) = c_0.  [para(421(a,1),11612(a,1,2,2,2))].

given #1026 (A,wt=19): 777 f(f(f(x,y),f(y,z)),f(f(x,y),f(u,x))) = f(x,y).  [para(387(a,1),502(a,1,2,1)),rewrite(387(11))].

given #1027 (F,wt=15): 20204 f(f(f(x,c_0),y),z) = f(z,f(y,f(x,x))).  [para(11824(a,1),365(a,2)),rewrite(9158(11,R),10727(10,R),9156(7))].

given #1028 (F,wt=15): 20205 f(f(x,f(y,y)),z) = f(z,f(f(y,c_0),x)).  [para(11824(a,2),365(a,2)),rewrite(9158(8,R),10727(8,R),9156(6))].

given #1029 (T,wt=15): 20264 f(f(c_0,x),f(y,y)) = f(f(x,c_0),f(c_0,y)).  [para(11833(a,2),10749(a,2))].

given #1030 (T,wt=15): 20266 f(f(c_0,x),f(y,y)) = f(f(x,c_0),f(y,c_0)).  [para(11846(a,2),10749(a,2))].

given #1031 (A,wt=35): 778 f(f(x,y),f(f(f(x,y),f(z,f(f(x,y),f(u,x)))),f(v,y))) = f(f(x,y),f(z,f(f(x,y),f(u,x)))).  [para(502(a,1),302(a,1,1)),rewrite(502(5),502(14))].

given #1032 (F,wt=15): 20270 f(f(x,f(f(y,c_0),z)),f(x,f(y,u))) = x.  [para(314(a,1),12128(a,1,1,2)),rewrite(9188(12,R),9156(11),421(10),9149(10))].

given #1033 (F,wt=15): 20271 f(f(x,f(f(y,c_0),z)),f(x,f(u,y))) = x.  [para(317(a,1),12128(a,1,1,2)),rewrite(9188(12,R),9156(11),421(10),9152(10))].

given #1034 (T,wt=15): 20272 f(f(x,f(y,f(z,c_0))),f(x,f(z,u))) = x.  [para(380(a,1),12128(a,1,1,2)),rewrite(9188(12,R),9156(11),421(10),9145(10))].

given #1035 (T,wt=15): 20273 f(f(x,f(y,f(z,c_0))),f(x,f(u,z))) = x.  [para(396(a,1),12128(a,1,1,2)),rewrite(9188(12,R),9156(11),421(10),9146(10))].

given #1036 (A,wt=33): 779 f(f(f(f(x,y),f(z,y)),f(u,x)),f(f(f(x,y),f(z,y)),f(v,f(x,y)))) = f(f(x,y),f(z,y)).  [para(302(a,1),502(a,1,2,1)),rewrite(302(19))].

given #1037 (F,wt=15): 20276 f(f(x,f(y,z)),f(x,f(f(y,c_0),u))) = x.  [para(314(a,1),12129(a,1,2,2)),rewrite(9188(8,R),9156(7),421(6),9149(6))].

given #1038 (F,wt=15): 20277 f(f(x,f(y,z)),f(x,f(f(z,c_0),u))) = x.  [para(317(a,1),12129(a,1,2,2)),rewrite(9188(8,R),9156(7),421(6),9152(6))].

given #1039 (T,wt=15): 20278 f(f(x,f(y,z)),f(x,f(u,f(y,c_0)))) = x.  [para(380(a,1),12129(a,1,2,2)),rewrite(9188(8,R),9156(7),421(6),9145(6))].

given #1040 (T,wt=15): 20279 f(f(x,f(y,z)),f(x,f(u,f(z,c_0)))) = x.  [para(396(a,1),12129(a,1,2,2)),rewrite(9188(8,R),9156(7),421(6),9146(6))].

given #1041 (A,wt=19): 780 f(f(f(x,y),f(z,x)),f(f(x,y),f(y,u))) = f(x,y).  [para(502(a,1),468(a,1,2,1)),rewrite(502(11))].

given #1042 (F,wt=15): 20282 f(f(f(x,y),z),f(z,f(f(x,c_0),u))) = z.  [para(314(a,1),12156(a,1,2,2)),rewrite(9188(8,R),9156(7),9149(6))].

given #1043 (F,wt=15): 20283 f(f(f(x,y),z),f(z,f(f(y,c_0),u))) = z.  [para(317(a,1),12156(a,1,2,2)),rewrite(9188(8,R),9156(7),9152(6))].

given #1044 (T,wt=15): 20284 f(f(f(x,y),z),f(z,f(u,f(x,c_0)))) = z.  [para(380(a,1),12156(a,1,2,2)),rewrite(9188(8,R),9156(7),9145(6))].

given #1045 (T,wt=15): 20285 f(f(f(x,y),z),f(z,f(u,f(y,c_0)))) = z.  [para(396(a,1),12156(a,1,2,2)),rewrite(9188(8,R),9156(7),9146(6))].

given #1046 (A,wt=19): 781 f(f(f(x,y),f(x,z)),f(f(x,y),f(u,y))) = f(x,y).  [para(468(a,1),502(a,1,2,1)),rewrite(468(11))].

given #1047 (F,wt=15): 20286 f(f(f(x,f(x,y)),z),f(z,f(y,u))) = z.  [para(540(a,1),12156(a,1,1,1)),rewrite(421(6),9154(6),2357(8))].

given #1048 (F,wt=15): 20287 f(f(f(x,f(x,y)),z),f(z,f(u,y))) = z.  [para(546(a,1),12156(a,1,1,1)),rewrite(421(6),9154(6),2193(8))].

given #1049 (T,wt=15): 20290 f(f(x,f(y,z)),f(f(f(y,c_0),u),x)) = x.  [para(314(a,1),12158(a,1,2,1)),rewrite(9188(8,R),9156(7),9149(6))].

given #1050 (T,wt=15): 20291 f(f(x,f(y,z)),f(f(f(z,c_0),u),x)) = x.  [para(317(a,1),12158(a,1,2,1)),rewrite(9188(8,R),9156(7),9152(6))].

given #1051 (A,wt=19): 782 f(f(f(x,y),f(z,x)),f(f(z,x),f(u,z))) = f(z,x).  [para(499(a,1),502(a,1,2,1)),rewrite(499(11))].

given #1052 (F,wt=15): 20292 f(f(x,f(y,z)),f(f(u,f(y,c_0)),x)) = x.  [para(380(a,1),12158(a,1,2,1)),rewrite(9188(8,R),9156(7),9145(6))].

given #1053 (F,wt=15): 20293 f(f(x,f(y,z)),f(f(u,f(z,c_0)),x)) = x.  [para(396(a,1),12158(a,1,2,1)),rewrite(9188(8,R),9156(7),9146(6))].

given #1054 (T,wt=15): 20296 f(f(x,f(y,f(y,z))),f(f(z,u),x)) = x.  [para(540(a,1),12158(a,1,1,2)),rewrite(421(6),9154(6),2357(8))].

given #1055 (T,wt=15): 20297 f(f(x,f(y,f(y,z))),f(f(u,z),x)) = x.  [para(546(a,1),12158(a,1,1,2)),rewrite(421(6),9154(6),2193(8))].

given #1056 (A,wt=21): 787 f(x,f(f(y,y),f(x,f(z,f(y,z))))) = f(x,f(z,f(y,z))).  [para(429(a,1),503(a,1,2,1))].

given #1057 (F,wt=15): 20300 f(f(f(f(x,c_0),y),z),f(z,f(x,u))) = z.  [para(314(a,1),12163(a,1,1,1)),rewrite(9188(12,R),9156(11),9149(10))].

given #1058 (F,wt=15): 20301 f(f(f(f(x,c_0),y),z),f(z,f(u,x))) = z.  [para(317(a,1),12163(a,1,1,1)),rewrite(9188(12,R),9156(11),9152(10))].

given #1059 (T,wt=15): 20302 f(f(f(x,f(y,c_0)),z),f(z,f(y,u))) = z.  [para(380(a,1),12163(a,1,1,1)),rewrite(9188(12,R),9156(11),9145(10))].

given #1060 (T,wt=15): 20303 f(f(f(x,f(y,c_0)),z),f(z,f(u,y))) = z.  [para(396(a,1),12163(a,1,1,1)),rewrite(9188(12,R),9156(11),9146(10))].

given #1061 (A,wt=23): 788 f(f(x,y),f(f(f(z,y),f(x,y)),f(x,u))) = f(f(z,y),f(x,y)).  [para(503(a,1),451(a,1,1))].

given #1062 (F,wt=15): 20304 f(f(f(x,y),z),f(z,f(u,f(u,x)))) = z.  [para(540(a,1),12163(a,1,2,2)),rewrite(421(3),9154(3),2357(5))].

given #1063 (F,wt=15): 20305 f(f(f(x,y),z),f(z,f(u,f(u,y)))) = z.  [para(546(a,1),12163(a,1,2,2)),rewrite(421(3),9154(3),2193(5))].

given #1064 (T,wt=15): 20309 f(f(x,f(f(y,c_0),z)),f(f(y,u),x)) = x.  [para(314(a,1),12175(a,1,1,2)),rewrite(9188(12,R),9156(11),9149(10))].

given #1065 (T,wt=15): 20310 f(f(x,f(f(y,c_0),z)),f(f(u,y),x)) = x.  [para(317(a,1),12175(a,1,1,2)),rewrite(9188(12,R),9156(11),9152(10))].

given #1066 (A,wt=27): 790 f(f(f(x,y),z),f(x,f(f(u,z),f(f(x,y),z)))) = f(f(u,z),f(f(x,y),z)).  [para(503(a,1),452(a,1,2)),rewrite(421(5),421(8))].

given #1067 (F,wt=15): 20311 f(f(x,f(y,f(z,c_0))),f(f(z,u),x)) = x.  [para(380(a,1),12175(a,1,1,2)),rewrite(9188(12,R),9156(11),9145(10))].

given #1068 (F,wt=15): 20312 f(f(x,f(y,f(z,c_0))),f(f(u,z),x)) = x.  [para(396(a,1),12175(a,1,1,2)),rewrite(9188(12,R),9156(11),9146(10))].

given #1069 (T,wt=15): 20314 f(f(x,f(y,z)),f(f(u,f(u,y)),x)) = x.  [para(540(a,1),12175(a,1,2,1)),rewrite(421(3),9154(3),2357(5))].

given #1070 (T,wt=15): 20315 f(f(x,f(y,z)),f(f(u,f(u,z)),x)) = x.  [para(546(a,1),12175(a,1,2,1)),rewrite(421(3),9154(3),2193(5))].

given #1071 (A,wt=27): 791 f(f(f(x,y),z),f(y,f(f(u,z),f(f(x,y),z)))) = f(f(u,z),f(f(x,y),z)).  [para(503(a,1),454(a,1,2)),rewrite(421(5),421(8))].

given #1072 (F,wt=15): 20319 f(f(f(x,y),z),f(f(f(x,c_0),u),z)) = z.  [para(314(a,1),12180(a,1,2,1)),rewrite(9188(8,R),9156(7),9149(6))].

given #1073 (F,wt=15): 20320 f(f(f(x,y),z),f(f(f(y,c_0),u),z)) = z.  [para(317(a,1),12180(a,1,2,1)),rewrite(9188(8,R),9156(7),9152(6))].

given #1074 (T,wt=15): 20321 f(f(f(x,y),z),f(f(u,f(x,c_0)),z)) = z.  [para(380(a,1),12180(a,1,2,1)),rewrite(9188(8,R),9156(7),9145(6))].

given #1075 (T,wt=15): 20322 f(f(f(x,y),z),f(f(u,f(y,c_0)),z)) = z.  [para(396(a,1),12180(a,1,2,1)),rewrite(9188(8,R),9156(7),9146(6))].

given #1076 (A,wt=21): 793 f(x,f(f(y,y),f(x,f(z,f(z,y))))) = f(x,f(z,f(z,y))).  [para(462(a,1),503(a,1,2,1))].

given #1077 (F,wt=15): 20323 f(f(f(x,f(x,y)),z),f(f(y,u),z)) = z.  [para(540(a,1),12180(a,1,1,1)),rewrite(421(6),9154(6),2357(8))].

given #1078 (F,wt=15): 20324 f(f(f(x,f(x,y)),z),f(f(u,y),z)) = z.  [para(546(a,1),12180(a,1,1,1)),rewrite(421(6),9154(6),2193(8))].

given #1079 (T,wt=15): 20326