============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13065 was started by mccune on cleo.thornwood,
Mon Jun 19 16:40:45 2006
The command was "/home/mccune/bin/prover9 -f mol-hints.in".
============================== end of head ===========================

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

% Reading from file mol-hints.in

assign(new_constants,1).
clear(lex_dep_demod).
    % clear(lex_dep_demod) -> assign(lex_dep_demod_lim, 0).
assign(max_weight,0).

clauses(sos).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y.
end_of_list.

clauses(goals).
f(x,y) = f(y,x) # answer(comm).
f(x,f(x,x)) = f(y,f(y,y)) # answer(one).
f(f(x,x),f(x,y)) = x # answer(absorb).
f(x,f(x,f(x,y))) = f(x,y) # answer(oml).
f(x,f(f(y,z),f(y,z))) = f(z,f(f(y,x),f(y,x))) # answer(assoc).
f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(mod).
end_of_list.

clauses(hints).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).
f(f(X,X),f(X,Y)) != X # label(495).
f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z) # label(499).
f(f(x,y),f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),w),f(f(f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),x),w),w),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))))) = f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))) # label(500A).
f(f(x,y),f(f(f(y,f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),w),f(f(f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),x),w),w),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))))) = f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))) # label(500B).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))),x),z),z),f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))))) = f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))) # label(500C).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))))) = f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))) # label(500D).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = f(f(v,y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))) # label(500E).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y # label(500).
f(f(x,y),f(f(f(y,y),z),y)) = y # label(501).
f(f(x,y),f(y,y)) = y # label(502).
f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,y)),f(y,y)),y),f(y,z)))) = y # label(503).
f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(505).
f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(507).
f(f(x,f(y,y)),f(f(f(f(y,y),f(y,y)),y),f(y,y))) = f(y,y) # label(508A).
f(f(x,f(y,y)),f(f(y,y),f(y,y))) = f(y,y) # label(508B).
f(f(x,f(y,y)),y) = f(y,y) # label(508).
f(x,f(f(f(f(x,x),y),x),f(f(f(x,x),y),x))) = f(f(f(x,x),y),x) # label(510A).
f(x,x) = f(f(f(x,x),y),x) # label(510B).
f(f(f(x,x),y),x) = f(x,x) # label(510).
f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511).
f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512).
f(f(x,y),f(x,x)) = f(f(x,x),f(x,x)) # label(513A).
f(f(x,y),f(x,x)) = x # label(513).
f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(514).
f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515).
x = f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) # label(519A).
f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519).
f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520).
f(x,f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y))))) = f(x,f(f(x,x),f(x,y))) # label(521A).
f(x,x) = f(x,f(f(x,x),f(x,y))) # label(521B).
f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521).
f(x,f(f(f(f(x,x),f(x,x)),f(x,x)),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526A).
f(x,f(f(x,f(x,x)),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526B).
f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526).
f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),f(f(x,x),f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))))) = f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) # label(527A).
f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),f(f(x,x),f(x,x))) = f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) # label(527B).
f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) # label(527C).
f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x) # label(527).
f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y))) = f(y,z) # label(528).
f(f(f(x,f(x,x)),x),f(f(f(x,x),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,y)))) = x # label(529A).
f(f(x,x),f(f(f(x,x),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,y)))) = x # label(529B).
f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(529).
f(f(f(x,x),x),f(f(f(x,x),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,y)))) = x # label(532A).
f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(532).
f(x,f(f(f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(f(x,x),f(x,y)))),f(f(x,x),f(x,x))),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(f(x,f(x,x)),f(f(x,x),f(x,y)))),f(f(x,x),f(x,y))))) = f(f(x,f(x,x)),f(f(x,x),f(x,y))) # label(534A).
f(x,f(f(f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(f(x,x),f(x,y)))),x),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(f(x,f(x,x)),f(f(x,x),f(x,y)))),f(f(x,x),f(x,y))))) = f(f(x,f(x,x)),f(f(x,x),f(x,y))) # label(534B).
f(x,f(f(f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(f(x,x),f(x,y)))),x),f(f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))),f(f(x,x),f(x,y))))) = f(f(x,f(x,x)),f(f(x,x),f(x,y))) # label(534C).
f(x,f(f(f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(f(x,x),f(x,y)))),x),f(x,f(f(x,x),f(x,y))))) = f(f(x,f(x,x)),f(f(x,x),f(x,y))) # label(534D).
f(x,f(f(f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(f(x,f(x,x)),f(f(x,x),f(x,y)))),x),f(x,x))) = f(f(x,f(x,x)),f(f(x,x),f(x,y))) # label(534E).
f(x,x) = f(f(x,f(x,x)),f(f(x,x),f(x,y))) # label(534F).
f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534).
f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),f(x,x)),f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x)))) = f(f(x,x),f(x,y)) # label(539A).
f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),f(x,x)),f(f(x,x),f(x,x)))) = f(f(x,x),f(x,y)) # label(539B).
f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),f(x,x)),x)) = f(f(x,x),f(x,y)) # label(539C).
f(f(x,x),f(x,x)) = f(f(x,x),f(x,y)) # label(539D).
x = f(f(x,x),f(x,y)) # label(539E).
f(f(x,x),f(x,y)) = x # label(539).
$F # label(540).
f(X,f(X,X)) != f(Y,f(Y,Y)) # label(3).
f(Y,f(Y,Y)) != f(X,f(X,X)) # label(494).
f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(504).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y # label(517).
f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522).
f(f(x,x),f(x,f(f(x,x),y))) = f(f(x,x),f(x,x)) # label(523A).
f(f(x,x),f(x,f(f(x,x),y))) = x # label(523).
f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524).
f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525).
f(x,f(f(f(x,x),f(f(x,x),f(x,x))),f(f(f(x,x),f(x,x)),f(f(x,x),y)))) = f(x,x) # label(530A).
f(x,f(f(f(x,x),x),f(f(f(x,x),f(x,x)),f(f(x,x),y)))) = f(x,x) # label(530B).
f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x) # label(530).
f(f(x,f(x,x)),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(x,f(f(x,x),y)))) = f(x,x) # label(531A).
f(f(x,f(x,x)),f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(x,f(f(x,x),y)))) = f(x,x) # label(531B).
f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x) # label(531).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),f(f(f(x,f(x,x)),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,f(f(x,x),y))))) = f(f(f(x,x),x),f(x,f(f(x,x),y))) # label(535A).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),f(f(x,x),f(x,f(f(x,x),y))))) = f(f(f(x,x),x),f(x,f(f(x,x),y))) # label(535B).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),x)) = f(f(f(x,x),x),f(x,f(f(x,x),y))) # label(535C).
f(f(x,x),f(x,x)) = f(f(f(x,x),x),f(x,f(f(x,x),y))) # label(535D).
x = f(f(f(x,x),x),f(x,f(f(x,x),y))) # label(535E).
f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535).
f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536).
f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(537).
f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(538).
f(x,f(f(f(f(x,f(f(x,x),y)),f(x,f(f(x,x),y))),f(f(x,x),f(x,x))),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(x,f(f(x,x),y))),x))) = f(x,f(f(x,x),y)) # label(541A).
f(x,f(f(f(f(x,f(f(x,x),y)),f(x,f(f(x,x),y))),x),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(x,f(f(x,x),y))),x))) = f(x,f(f(x,x),y)) # label(541B).
f(x,f(f(f(f(x,f(f(x,x),y)),f(x,f(f(x,x),y))),x),f(f(f(f(x,x),x),f(x,f(f(x,x),y))),x))) = f(x,f(f(x,x),y)) # label(541C).
f(x,f(f(f(f(x,f(f(x,x),y)),f(x,f(f(x,x),y))),x),f(x,x))) = f(x,f(f(x,x),y)) # label(541D).
f(x,x) = f(x,f(f(x,x),y)) # label(541E).
f(x,f(f(x,x),y)) = f(x,x) # label(541).
f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),f(f(x,x),f(x,x))),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(x,f(y,f(x,x)))),x))) = f(x,f(y,f(x,x))) # label(542A).
f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(x,f(y,f(x,x)))),x))) = f(x,f(y,f(x,x))) # label(542B).
f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x))) = f(x,f(y,f(x,x))) # label(542C).
f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(x,x))) = f(x,f(y,f(x,x))) # label(542D).
f(x,x) = f(x,f(y,f(x,x))) # label(542E).
f(x,f(y,f(x,x))) = f(x,x) # label(542).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),y),f(f(f(x,y),f(x,y)),y)),f(f(x,y),f(x,y))),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)),f(f(x,y),f(x,y))))) = f(f(f(x,y),f(x,y)),y) # label(543A).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),y),f(f(f(x,y),f(x,y)),y)),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y))))) = f(f(f(x,y),f(x,y)),y) # label(543B).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),y),f(f(f(x,y),f(x,y)),y)),f(f(x,y),f(x,y))),f(x,y))) = f(f(f(x,y),f(x,y)),y) # label(543C).
f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y))) = f(f(f(x,y),f(x,y)),y) # label(543D).
f(x,y) = f(f(f(x,y),f(x,y)),y) # label(543E).
f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),x),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))))) = f(f(f(x,y),f(x,y)),x) # label(544A).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),x),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y))))) = f(f(f(x,y),f(x,y)),x) # label(544B).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),x),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))),f(x,y))) = f(f(f(x,y),f(x,y)),x) # label(544C).
f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y))) = f(f(f(x,y),f(x,y)),x) # label(544D).
f(x,y) = f(f(f(x,y),f(x,y)),x) # label(544E).
f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544).
f(f(x,y),f(f(f(y,y),f(y,y)),f(f(f(f(f(y,x),f(f(f(y,y),f(y,y)),z)),f(f(f(y,y),f(y,y)),z)),y),f(u,y)))) = y # label(546A).
f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),f(y,y)),z)),f(f(f(y,y),f(y,y)),z)),y),f(u,y)))) = y # label(546B).
f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(f(f(y,y),f(y,y)),z)),y),f(u,y)))) = y # label(546C).
f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y)))) = y # label(546).
f(f(x,x),f(y,x)) = f(f(x,x),f(x,x)) # label(548A).
f(f(x,x),f(y,x)) = x # label(548).
f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(550).
f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552).
f(f(f(x,x),f(y,x)),f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x) # label(553A).
f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x) # label(553).
f(x,f(f(f(x,x),f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u))))),f(y,x))) = f(y,x) # label(557A).
f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557).
f(f(x,x),f(f(f(f(x,x),f(x,x)),f(f(y,f(x,x)),x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558A).
f(f(x,x),f(f(x,f(f(y,f(x,x)),x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558B).
f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558).
f(x,f(f(f(x,y),f(f(y,x),f(y,y))),f(y,x))) = f(y,x) # label(559A).
f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559).
f(x,f(f(f(x,x),x),f(x,y))) = f(f(f(x,y),f(x,y)),x) # label(560A).
f(x,f(f(f(x,x),x),f(x,y))) = f(x,y) # label(560).
f(f(x,x),f(f(x,x),f(x,f(x,x)))) = f(x,f(x,x)) # label(561A).
f(f(x,x),x) = f(x,f(x,x)) # label(561).
f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562).
f(f(x,x),f(f(f(x,x),x),f(f(x,x),y))) = f(f(x,x),y) # label(563A).
f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563).
f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(564).
f(f(x,x),f(f(x,f(x,x)),f(f(f(x,x),f(x,f(x,x))),f(f(x,f(x,x)),y)))) = f(x,f(x,x)) # label(565A).
f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)) # label(565).
f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,f(x,x)),f(x,x)))) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) # label(567A).
f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),x)) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) # label(567B).
f(f(f(x,f(x,x)),f(x,f(x,x))),f(x,x)) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) # label(567C).
f(x,f(x,x)) = f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) # label(567D).
f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)) # label(567).
f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568).
f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(f(x,f(x,x)),f(x,f(x,x)))))) = f(y,f(f(x,f(x,x)),f(x,f(x,x)))) # label(570A).
f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(x,f(x,x)),f(x,f(x,x)))) = f(y,f(f(x,f(x,x)),f(x,f(x,x)))) # label(570B).
f(x,f(x,x)) = f(y,f(f(x,f(x,x)),f(x,f(x,x)))) # label(570C).
f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570).
f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(f(x,x),f(f(y,f(y,y)),f(y,f(y,y)))) # label(576A).
f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(y,f(y,y)) # label(576).
f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(x,f(x,x)) # label(577A).
f(x,f(x,x)) = f(y,f(y,y)) # label(577).
$F # label(578).
f(X,f(X,f(X,Y))) != f(X,Y) # label(496).
f(f(f(x,x),f(x,y)),f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y) # label(554A).
f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y) # label(554).
f(f(x,f(x,x)),f(y,y)) = y # label(574).
f(x,f(y,f(y,y))) = f(x,x) # label(575).
f(f(x,f(f(y,f(y,y)),f(x,x))),f(y,f(y,y))) = f(f(y,f(y,y)),f(x,x)) # label(594A).
f(f(x,x),f(y,f(y,y))) = f(f(y,f(y,y)),f(x,x)) # label(594B).
f(f(x,x),f(y,f(y,y))) = x # label(594).
f(x,f(f(f(x,x),f(f(x,y),f(f(x,y),f(x,y)))),f(x,y))) = f(x,y) # label(599A).
f(x,f(x,f(x,y))) = f(x,y) # label(599).
$F # label(600).
f(X,Y) != f(Y,X) # label(2).
f(Y,X) != f(X,Y) # label(493).
f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(506).
f(x,f(f(x,y),f(x,y))) = f(x,y) # label(516).
f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,f(f(z,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))))) = f(f(z,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))) # label(518A).
f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = f(f(z,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))) # label(518B).
f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = x # label(518).
f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(533).
f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(549).
f(f(x,f(x,x)),y) = f(y,y) # label(573).
f(x,f(f(y,f(y,y)),f(z,x))) = f(z,x) # label(581).
f(x,f(f(y,f(y,y)),f(x,z))) = f(x,z) # label(582).
f(f(f(x,f(x,x)),y),f(f(f(y,y),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),y),f(y,z)))) = y # label(583A).
f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),f(f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),y),f(y,z)))) = y # label(583B).
f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(583C).
f(f(f(x,f(x,x)),y),f(y,z)) = y # label(583).
f(f(x,x),f(f(x,y),f(x,y))) = f(x,f(x,x)) # label(590).
f(f(x,f(x,x)),f(f(y,f(y,y)),z)) = z # label(595).
f(f(x,y),f(f(f(f(y,x),f(y,x)),f(y,f(y,y))),y)) = y # label(597A).
f(f(x,y),f(f(y,x),y)) = y # label(597).
f(x,f(f(f(x,x),f(f(y,x),f(f(y,x),f(y,x)))),f(y,x))) = f(y,x) # label(598A).
f(x,f(x,f(y,x))) = f(y,x) # label(598).
f(f(f(x,f(x,x)),f(f(f(f(f(y,z),f(f(y,y),f(y,y))),f(f(y,y),f(y,y))),y),f(y,u))),f(y,y)) = y # label(607A).
f(f(f(x,f(x,x)),f(f(f(f(f(y,z),y),f(f(y,y),f(y,y))),y),f(y,u))),f(y,y)) = y # label(607B).
f(f(f(x,f(x,x)),f(f(f(f(f(y,z),y),y),y),f(y,u))),f(y,y)) = y # label(607).
f(f(x,y),f(f(f(x,f(x,y)),x),f(x,f(x,y)))) = f(x,f(x,y)) # label(616).
f(f(x,y),f(f(f(x,f(f(f(z,f(z,z)),x),f(x,y))),f(f(x,y),f(x,y))),f(f(f(x,y),f(f(f(z,f(z,z)),x),f(x,y))),f(x,y)))) = f(f(f(z,f(z,z)),x),f(x,y)) # label(620A).
f(f(x,y),f(f(f(x,x),f(f(x,y),f(x,y))),f(f(f(x,y),f(f(f(z,f(z,z)),x),f(x,y))),f(x,y)))) = f(f(f(z,f(z,z)),x),f(x,y)) # label(620B).
f(f(x,y),f(f(x,f(x,x)),f(f(f(x,y),f(f(f(z,f(z,z)),x),f(x,y))),f(x,y)))) = f(f(f(z,f(z,z)),x),f(x,y)) # label(620C).
f(f(x,y),f(f(x,f(x,x)),f(f(f(x,y),x),f(x,y)))) = f(f(f(z,f(z,z)),x),f(x,y)) # label(620D).
f(f(f(x,y),x),f(x,y)) = f(f(f(z,f(z,z)),x),f(x,y)) # label(620E).
f(f(f(x,y),x),f(x,y)) = x # label(620).
f(f(x,y),x) = f(x,f(x,y)) # label(623).
f(f(f(x,f(x,x)),f(f(f(f(y,f(y,z)),y),y),f(y,u))),f(y,y)) = y # label(626A).
f(f(f(x,f(x,x)),f(f(f(y,f(y,f(y,z))),y),f(y,u))),f(y,y)) = y # label(626B).
f(f(f(x,f(x,x)),f(f(f(y,z),y),f(y,u))),f(y,y)) = y # label(626C).
f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,y)) = y # label(626).
f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z)) = z # label(644).
f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z)) = z # label(646).
f(f(f(x,f(x,x)),f(f(y,f(y,y)),f(f(z,u),f(v,u)))),u) = f(f(y,f(y,y)),f(f(z,u),f(v,u))) # label(649A).
f(f(f(x,y),f(z,y)),y) = f(f(u,f(u,u)),f(f(x,y),f(z,y))) # label(649).
f(x,f(f(f(y,f(y,y)),f(f(z,x),f(u,x))),f(f(f(z,x),f(u,x)),x))) = f(f(f(z,x),f(u,x)),x) # label(664A).
f(x,f(f(y,x),f(z,x))) = f(f(f(y,x),f(z,x)),x) # label(664B).
f(f(f(x,y),f(z,y)),y) = f(y,f(f(x,y),f(z,y))) # label(664).
f(f(x,y),f(f(f(z,y),f(x,y)),y)) = f(f(z,y),f(x,y)) # label(666A).
f(f(x,y),f(y,f(f(z,y),f(x,y)))) = f(f(z,y),f(x,y)) # label(666).
f(f(x,y),f(y,f(f(y,z),f(x,y)))) = f(f(f(f(y,z),f(y,z)),y),f(x,y)) # label(668A).
f(f(x,y),f(y,f(f(y,z),f(x,y)))) = f(f(y,z),f(x,y)) # label(668).
f(x,f(f(x,y),f(f(z,f(x,y)),f(f(f(u,f(u,u)),x),f(x,y))))) = f(f(z,f(x,y)),f(f(f(u,f(u,u)),x),f(x,y))) # label(669A).
f(x,f(f(x,y),f(f(z,f(x,y)),x))) = f(f(z,f(x,y)),f(f(f(u,f(u,u)),x),f(x,y))) # label(669B).
f(x,f(f(x,y),f(f(z,f(x,y)),x))) = f(f(z,f(x,y)),x) # label(669).
f(x,f(f(x,y),f(y,x))) = f(f(f(y,y),f(x,y)),x) # label(670A).
f(x,f(f(x,y),f(y,x))) = f(y,x) # label(670).
f(f(x,y),f(x,y)) = f(f(y,x),f(x,y)) # label(671A).
f(f(x,y),f(y,x)) = f(f(y,x),f(y,x)) # label(671).
f(f(x,f(y,z)),f(f(z,y),f(y,z))) = f(y,z) # label(672).
f(f(f(x,y),f(x,y)),f(f(x,y),f(y,x))) = f(f(f(x,y),f(y,x)),f(f(x,y),f(y,x))) # label(674A).
f(x,y) = f(f(f(x,y),f(y,x)),f(f(x,y),f(y,x))) # label(674B).
f(x,y) = f(y,x) # label(674).
$F # label(675).
f(X,f(f(Y,Z),f(Y,Z))) != f(Z,f(f(Y,X),f(Y,X))) # label(497).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,f(f(x,y),f(x,y))),z),z),y),f(y,u)))) = y # label(551A).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u)))) = y # label(551).
f(f(f(f(x,y),f(x,y)),y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y # label(555A).
f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y # label(555).
f(f(x,y),f(f(f(f(x,y),f(z,y)),f(y,f(f(z,y),f(z,y)))),y)) = y # label(556A).
f(f(x,y),f(f(f(f(x,y),f(z,y)),f(z,y)),y)) = y # label(556).
f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(z,f(y,x))))) = f(y,x) # label(566).
f(f(x,y),f(f(z,f(z,z)),y)) = y # label(579).
f(f(x,y),f(f(z,f(z,z)),x)) = x # label(580).
f(f(x,y),f(f(f(y,y),z),f(f(u,f(u,u)),f(f(f(f(y,x),z),z),y)))) = y # label(585).
f(f(f(x,f(x,x)),f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),f(y,z)),z))) = f(y,z) # label(586A).
f(f(f(x,f(x,x)),f(y,z)),f(f(x,f(x,x)),f(f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),f(y,z)),z))) = f(y,z) # label(586B).
f(f(f(x,f(x,x)),f(y,z)),f(f(x,f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(586C).
f(f(f(x,f(x,x)),f(y,z)),z) = f(y,z) # label(586).
f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(f(z,f(z,z)),x)) # label(589A).
f(x,f(y,y)) = f(x,f(f(z,f(z,z)),y)) # label(589B).
f(x,f(f(y,f(y,y)),z)) = f(x,f(z,z)) # label(589).
f(x,f(f(f(f(y,x),f(y,x)),f(z,f(z,z))),f(f(f(f(x,x),f(z,f(z,z))),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(601A).
f(x,f(f(y,x),f(f(f(f(x,x),f(z,f(z,z))),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(601B).
f(x,f(f(y,x),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x) # label(601).
f(f(x,y),f(f(z,f(z,z)),f(f(f(f(f(y,x),f(f(y,y),f(y,y))),f(f(y,y),f(y,y))),y),f(u,y)))) = y # label(606A).
f(f(x,y),f(f(z,f(z,z)),f(f(f(f(f(y,x),y),f(f(y,y),f(y,y))),y),f(u,y)))) = y # label(606B).
f(f(x,y),f(f(z,f(z,z)),f(f(f(f(f(y,x),y),y),y),f(u,y)))) = y # label(606).
f(f(x,f(y,f(y,y))),f(z,f(z,z))) = x # label(613).
f(f(x,y),f(f(y,f(f(y,x),y)),y)) = y # label(615).
f(f(f(x,f(x,y)),x),f(f(x,y),x)) = x # label(617).
f(f(x,f(x,f(x,y))),f(f(x,y),x)) = x # label(624A).
f(f(x,y),f(f(x,y),x)) = x # label(624B).
f(f(x,y),f(x,f(x,y))) = x # label(624).
f(f(x,y),f(f(y,f(y,f(y,x))),y)) = y # label(625A).
f(f(x,y),f(f(y,x),y)) = y # label(625B).
f(f(x,y),f(y,f(y,x))) = y # label(625).
f(f(x,y),f(f(z,f(z,z)),f(f(f(f(y,f(y,x)),y),y),f(u,y)))) = y # label(627A).
f(f(x,y),f(f(z,f(z,z)),f(f(f(y,f(y,f(y,x))),y),f(u,y)))) = y # label(627B).
f(f(x,y),f(f(z,f(z,z)),f(f(f(y,x),y),f(u,y)))) = y # label(627C).
f(f(x,y),f(f(z,f(z,z)),f(f(y,f(y,x)),f(u,y)))) = y # label(627).
f(x,f(y,x)) = f(f(y,x),f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u))))) # label(628A).
f(x,f(y,x)) = f(f(y,x),x) # label(628B).
f(f(x,y),y) = f(y,f(x,y)) # label(628).
f(f(f(x,y),y),f(f(f(f(x,y),f(f(x,y),y)),f(x,y)),y)) = y # label(629A).
f(f(x,f(y,x)),f(f(f(f(y,x),f(f(y,x),x)),f(y,x)),x)) = x # label(629B).
f(f(x,f(y,x)),f(f(f(f(y,x),f(x,f(y,x))),f(y,x)),x)) = x # label(629C).
f(f(x,f(y,x)),f(f(f(y,x),f(f(y,x),f(x,f(y,x)))),x)) = x # label(629D).
f(f(x,f(y,x)),f(f(x,f(y,x)),x)) = x # label(629E).
f(f(x,f(y,x)),f(x,f(x,f(y,x)))) = x # label(629F).
f(f(x,f(y,x)),f(y,x)) = x # label(629G).
f(f(x,y),f(y,f(x,y))) = y # label(629).
f(f(x,y),f(f(f(y,y),x),f(f(f(f(x,f(x,y)),x),y),f(y,z)))) = y # label(630A).
f(f(x,y),f(f(f(y,y),x),f(f(f(x,f(x,f(x,y))),y),f(y,z)))) = y # label(630B).
f(f(x,y),f(f(f(y,y),x),f(f(f(x,y),y),f(y,z)))) = y # label(630C).
f(f(x,y),f(f(f(y,y),x),f(f(y,f(x,y)),f(y,z)))) = y # label(630).
f(f(x,y),f(f(f(y,y),z),f(f(u,f(u,u)),f(f(z,f(f(y,x),z)),y)))) = y # label(632).
f(x,f(f(y,x),f(f(f(y,f(x,y)),f(y,x)),f(z,f(y,x))))) = f(y,x) # label(633).
f(f(f(x,y),f(x,y)),f(x,f(f(x,y),f(x,x)))) = f(f(x,y),f(f(x,y),f(x,y))) # label(637A).
f(f(f(x,y),f(x,y)),f(x,x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(637).
f(f(x,f(y,x)),f(x,f(f(f(x,f(y,x)),f(f(y,x),f(x,f(y,x)))),f(f(f(y,x),f(x,f(y,x))),z)))) = f(f(y,x),f(x,f(y,x))) # label(640A).
f(f(x,f(y,x)),f(x,f(f(f(x,f(y,x)),x),f(f(f(y,x),f(x,f(y,x))),z)))) = f(f(y,x),f(x,f(y,x))) # label(640B).
f(f(x,f(y,x)),f(x,f(f(x,f(x,f(y,x))),f(f(f(y,x),f(x,f(y,x))),z)))) = f(f(y,x),f(x,f(y,x))) # label(640C).
f(f(x,f(y,x)),f(x,f(f(y,x),f(f(f(y,x),f(x,f(y,x))),z)))) = f(f(y,x),f(x,f(y,x))) # label(640D).
f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z)))) = f(f(y,x),f(x,f(y,x))) # label(640E).
f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z)))) = x # label(640).
x = f(f(x,f(x,y)),f(y,x)) # label(652A).
f(f(x,f(x,y)),f(y,x)) = x # label(652).
f(f(x,f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(x,x))),f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(f(y,f(y,y)),f(f(z,x),f(x,u))))) = f(f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(x,x)),f(f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(x,x)),f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(x,x)))) # label(658A).
f(f(x,x),f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(f(y,f(y,y)),f(f(z,x),f(x,u))))) = f(f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(x,x)),f(f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(x,x)),f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),f(x,x)))) # label(658B).
f(f(x,x),f(f(y,x),f(x,z))) = f(f(f(f(u,f(u,u)),f(f(y,x),f(x,z))),f(x,x)),f(f(f(f(u,f(u,u)),f(f(y,x),f(x,z))),f(x,x)),f(f(f(u,f(u,u)),f(f(y,x),f(x,z))),f(x,x)))) # label(658C).
f(f(x,x),f(f(y,x),f(x,z))) = f(x,f(f(f(f(u,f(u,u)),f(f(y,x),f(x,z))),f(x,x)),f(f(f(u,f(u,u)),f(f(y,x),f(x,z))),f(x,x)))) # label(658D).
f(f(x,x),f(f(y,x),f(x,z))) = f(x,f(x,f(f(f(u,f(u,u)),f(f(y,x),f(x,z))),f(x,x)))) # label(658E).
f(f(x,x),f(f(y,x),f(x,z))) = f(x,f(x,x)) # label(658).
f(f(x,x),f(f(y,x),f(z,f(z,z)))) = f(x,f(x,x)) # label(660).
f(f(x,y),f(x,f(f(z,x),f(f(f(x,y),f(x,y)),x)))) = f(f(z,x),f(f(f(x,y),f(x,y)),x)) # label(667A).
f(f(x,y),f(x,f(f(z,x),f(x,y)))) = f(f(z,x),f(f(f(x,y),f(x,y)),x)) # label(667B).
f(f(x,y),f(x,f(f(z,x),f(x,y)))) = f(f(z,x),f(x,y)) # label(667).
f(f(x,f(y,x)),f(x,f(f(x,y),f(x,y)))) = x # label(673A).
f(f(x,f(y,x)),f(x,y)) = x # label(673).
f(x,f(f(y,x),f(y,f(z,f(y,x))))) = f(y,x) # label(676).
f(f(x,y),f(x,f(y,x))) = x # label(677).
f(f(f(x,f(x,x)),f(y,z)),y) = f(z,y) # label(678).
f(f(f(x,f(x,x)),y),z) = f(z,f(y,y)) # label(679).
f(f(f(x,f(x,x)),f(f(y,f(y,y)),f(z,u))),f(u,z)) = f(f(y,f(y,y)),f(z,u)) # label(682A).
f(f(x,y),f(y,x)) = f(f(z,f(z,z)),f(x,y)) # label(682B).
f(f(x,f(x,x)),f(y,z)) = f(f(y,z),f(z,y)) # label(682).
f(f(x,f(y,z)),f(f(y,z),f(z,y))) = f(z,y) # label(686).
f(x,f(f(y,z),f(z,x))) = f(z,x) # label(689).
f(x,f(y,f(f(z,y),x))) = f(f(z,y),x) # label(690).
f(x,f(f(y,z),f(y,x))) = f(y,x) # label(691).
f(f(x,y),f(f(z,f(y,f(y,x))),y)) = f(f(y,f(y,x)),f(x,y)) # label(695A).
f(f(x,y),f(f(z,f(y,f(y,x))),y)) = y # label(695).
f(x,f(f(y,z),f(x,z))) = f(z,x) # label(696).
f(x,f(f(y,x),f(z,y))) = f(y,x) # label(697).
f(x,y) = f(f(f(x,z),f(x,y)),y) # label(701A).
f(f(f(x,y),f(x,z)),z) = f(x,z) # label(701).
f(x,f(f(y,x),f(y,z))) = f(y,x) # label(702).
f(x,f(y,f(x,f(z,y)))) = f(f(z,y),x) # label(703A).
f(f(x,y),z) = f(z,f(y,f(z,f(x,y)))) # label(703).
f(x,y) = f(f(f(z,x),f(y,x)),y) # label(704A).
f(f(f(x,y),f(z,y)),z) = f(y,z) # label(704).
f(x,f(f(x,y),f(z,y))) = f(y,x) # label(705).
f(f(f(x,y),f(z,y)),f(f(u,z),f(y,z))) = f(z,f(f(x,y),f(z,y))) # label(706A).
f(f(f(x,y),f(z,y)),f(f(u,z),f(y,z))) = f(y,z) # label(706).
f(x,f(f(f(y,z),x),z)) = f(f(y,z),x) # label(708).
f(f(x,f(y,x)),f(x,f(f(x,y),z))) = f(f(x,y),f(x,f(y,x))) # label(718A).
f(f(x,f(y,x)),f(x,f(f(x,y),z))) = x # label(718).
f(f(x,f(y,f(x,z))),y) = f(f(x,z),y) # label(722).
f(f(f(x,f(y,z)),f(f(y,f(y,z)),f(y,z))),f(y,f(y,z))) = y # label(723A).
f(f(f(x,f(y,z)),f(f(y,z),f(y,f(y,z)))),f(y,f(y,z))) = y # label(723B).
f(f(f(x,f(y,z)),y),f(y,f(y,z))) = y # label(723).
f(f(f(x,f(y,z)),f(f(z,f(z,y)),f(y,z))),f(z,f(z,y))) = z # label(724A).
f(f(f(x,f(y,z)),z),f(z,f(z,y))) = z # label(724).
f(f(f(x,y),f(z,y)),x) = f(y,x) # label(725).
f(x,f(f(x,f(y,z)),z)) = f(f(y,z),x) # label(726).
f(f(f(x,f(y,z)),z),x) = f(f(y,z),x) # label(728).
f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)) # label(731).
f(f(f(f(x,f(x,x)),y),z),u) = f(u,f(f(y,y),f(u,f(z,f(y,y))))) # label(732A).
f(f(f(f(x,f(x,x)),y),z),u) = f(u,f(z,f(y,y))) # label(732).
f(x,f(y,z)) = f(f(z,f(x,f(y,z))),x) # label(736A).
f(f(x,f(y,f(z,x))),y) = f(y,f(z,x)) # label(736).
f(x,y) = f(f(f(y,x),f(x,y)),f(z,f(y,x))) # label(740A).
f(f(f(x,y),f(y,x)),f(z,f(x,y))) = f(y,x) # label(740).
f(f(f(x,y),f(y,x)),f(z,f(y,x))) = f(x,y) # label(741).
f(x,f(f(f(y,z),x),f(u,f(z,y)))) = f(f(f(f(z,y),f(y,z)),f(u,f(z,y))),x) # label(743A).
f(x,f(f(f(y,z),x),f(u,f(z,y)))) = f(f(y,z),x) # label(743).
f(f(f(x,y),f(f(z,u),y)),f(f(f(u,z),f(z,u)),f(y,f(z,u)))) = f(y,f(z,u)) # label(745A).
f(f(f(x,y),f(f(z,u),y)),f(u,z)) = f(y,f(z,u)) # label(745).
f(f(f(f(x,f(x,x)),y),f(y,y)),f(f(z,f(z,z)),f(f(u,f(y,y)),f(f(y,y),v)))) = f(y,y) # label(748A).
f(x,f(f(y,f(y,y)),f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,x) # label(748).
f(f(x,y),f(f(f(z,f(z,z)),f(f(u,f(f(y,x),u)),y)),y)) = f(f(x,y),f(f(f(y,y),u),f(f(z,f(z,z)),f(f(u,f(f(y,x),u)),y)))) # label(759A).
f(f(x,y),f(f(z,f(f(y,x),z)),y)) = f(f(x,y),f(f(f(y,y),z),f(f(u,f(u,u)),f(f(z,f(f(y,x),z)),y)))) # label(759B).
f(f(x,y),f(f(z,f(f(y,x),z)),y)) = y # label(759).
f(f(f(f(x,f(x,x)),f(f(y,f(f(z,u),y)),z)),z),f(u,z)) = f(f(u,z),f(f(f(z,z),y),f(f(x,f(x,x)),f(f(y,f(f(z,u),y)),z)))) # label(760A).
f(f(f(x,f(f(y,z),x)),y),f(z,y)) = f(f(z,y),f(f(f(y,y),x),f(f(u,f(u,u)),f(f(x,f(f(y,z),x)),y)))) # label(760B).
f(f(f(x,f(f(y,z),x)),y),f(z,y)) = y # label(760).
f(f(f(x,x),f(x,y)),f(f(z,f(x,z)),f(x,y))) = f(x,y) # label(761A).
f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z) # label(761).
f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),y)) = f(f(f(u,f(f(y,x),u)),y),f(x,y)) # label(763A).
f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),y)) = y # label(763).
f(f(x,x),f(f(f(f(y,x),f(z,f(z,z))),f(x,f(x,x))),f(f(x,x),u))) = f(f(x,x),u) # label(765A).
f(f(x,x),f(f(y,x),f(f(x,x),z))) = f(f(x,x),z) # label(765).
f(x,f(f(y,f(x,x)),f(f(f(x,x),f(x,x)),z))) = f(f(f(x,x),f(x,x)),z) # label(772A).
f(x,f(f(y,f(x,x)),f(x,z))) = f(f(f(x,x),f(x,x)),z) # label(772B).
f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z) # label(772).
f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y) # label(774).
f(x,f(f(f(x,x),y),f(x,z))) = f(x,z) # label(775).
f(x,f(f(f(x,x),y),f(z,x))) = f(x,f(x,f(z,x))) # label(776A).
f(x,f(f(f(x,x),y),f(z,x))) = f(z,x) # label(776).
f(x,y) = f(f(f(f(y,y),z),f(x,y)),y) # label(779A).
f(f(f(f(x,x),y),f(z,x)),x) = f(z,x) # label(779).
f(f(x,y),f(f(f(y,y),f(f(f(y,y),z),f(x,y))),f(f(y,f(f(f(f(y,y),z),f(x,y)),y)),f(y,u)))) = y # label(781A).
f(f(x,y),f(f(f(y,y),z),f(f(y,f(f(f(f(y,y),z),f(x,y)),y)),f(y,u)))) = y # label(781B).
f(f(x,y),f(f(f(y,y),z),f(f(y,f(x,y)),f(y,u)))) = y # label(781).
f(f(x,x),f(f(f(x,x),y),f(f(z,f(z,z)),f(x,u)))) = x # label(783).
x = f(f(y,f(f(z,f(z,z)),f(x,u))),f(x,x)) # label(789A).
f(f(x,f(f(y,f(y,y)),f(z,u))),f(z,z)) = z # label(789).
f(f(x,f(y,y)),f(f(z,f(f(y,y),f(f(y,y),y))),f(z,f(f(y,y),f(f(y,y),y))))) = f(z,f(f(y,y),f(f(y,y),y))) # label(791A).
f(f(x,f(y,y)),f(f(z,f(f(y,y),f(y,f(y,y)))),f(z,f(f(y,y),f(f(y,y),y))))) = f(z,f(f(y,y),f(f(y,y),y))) # label(791B).
f(f(x,f(y,y)),f(f(z,y),f(z,f(f(y,y),f(f(y,y),y))))) = f(z,f(f(y,y),f(f(y,y),y))) # label(791C).
f(f(x,f(y,y)),f(f(z,y),f(z,f(f(y,y),f(y,f(y,y)))))) = f(z,f(f(y,y),f(f(y,y),y))) # label(791D).
f(f(x,f(y,y)),f(f(z,y),f(z,y))) = f(z,f(f(y,y),f(f(y,y),y))) # label(791E).
f(f(x,f(y,y)),f(f(z,y),f(z,y))) = f(z,f(f(y,y),f(y,f(y,y)))) # label(791F).
f(f(x,f(y,y)),f(f(z,y),f(z,y))) = f(z,y) # label(791).
f(f(x,y),f(f(z,f(y,y)),f(f(z,f(y,y)),f(f(x,y),f(x,y))))) = f(z,f(y,y)) # label(792A).
f(f(x,y),f(f(z,f(y,y)),f(x,y))) = f(z,f(y,y)) # label(792).
f(x,y) = f(f(f(x,y),f(x,y)),f(z,f(y,y))) # label(794A).
f(f(f(x,y),f(x,y)),f(z,f(y,y))) = f(x,y) # label(794).
f(x,f(f(f(f(y,y),z),x),f(u,y))) = f(f(f(y,y),z),x) # label(796).
f(f(f(x,x),f(x,f(f(y,f(y,y)),f(f(z,f(x,x)),f(f(x,x),u))))),f(v,f(f(f(y,f(y,y)),f(f(z,f(x,x)),f(f(x,x),u))),f(f(y,f(y,y)),f(f(z,f(x,x)),f(f(x,x),u)))))) = f(x,f(f(y,f(y,y)),f(f(z,f(x,x)),f(f(x,x),u)))) # label(797A).
f(f(f(x,x),f(x,x)),f(y,f(f(f(z,f(z,z)),f(f(u,f(x,x)),f(f(x,x),v))),f(f(z,f(z,z)),f(f(u,f(x,x)),f(f(x,x),v)))))) = f(x,f(f(z,f(z,z)),f(f(u,f(x,x)),f(f(x,x),v)))) # label(797B).
f(x,f(y,f(f(f(z,f(z,z)),f(f(u,f(x,x)),f(f(x,x),v))),f(f(z,f(z,z)),f(f(u,f(x,x)),f(f(x,x),v)))))) = f(x,f(f(z,f(z,z)),f(f(u,f(x,x)),f(f(x,x),v)))) # label(797C).
f(x,f(y,f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,f(f(v,f(v,v)),f(f(z,f(x,x)),f(f(x,x),u)))) # label(797D).
f(x,f(y,f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,x) # label(797).
f(f(x,f(y,x)),f(x,f(z,f(y,y)))) = x # label(798).
f(x,x) = f(f(f(x,f(y,x)),f(y,y)),x) # label(800A).
f(f(f(x,f(y,x)),f(y,y)),x) = f(x,x) # label(800).
f(f(x,x),f(f(y,f(y,y)),f(f(x,f(z,x)),f(z,z)))) = f(f(x,f(z,x)),f(z,z)) # label(801).
f(f(x,x),f(y,f(f(f(f(f(z,f(z,z)),x),f(x,x)),u),f(f(f(x,x),f(x,x)),v)))) = f(f(x,x),f(x,x)) # label(808A).
f(f(x,x),f(y,f(f(x,z),f(f(f(x,x),f(x,x)),u)))) = f(f(x,x),f(x,x)) # label(808B).
f(f(x,x),f(y,f(f(x,z),f(x,u)))) = f(f(x,x),f(x,x)) # label(808C).
f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x # label(808).
f(x,f(f(f(y,y),z),f(f(y,u),x))) = f(f(y,u),x) # label(817).
f(x,x) = f(f(y,f(f(z,f(f(x,f(y,y)),z)),x)),x) # label(822A).
f(f(x,f(f(y,f(f(z,f(x,x)),y)),z)),z) = f(z,z) # label(822).
f(x,f(y,y)) = f(f(f(z,f(f(y,f(x,x)),z)),y),x) # label(823A).
f(f(f(x,f(f(y,f(z,z)),x)),y),z) = f(z,f(y,y)) # label(823).
f(f(f(f(f(x,x),f(f(x,x),y)),f(x,x)),f(z,f(f(x,x),y))),x) = f(x,f(f(z,f(f(x,x),y)),f(z,f(f(x,x),y)))) # label(824A).
f(f(f(f(x,x),f(f(x,x),f(f(x,x),y))),f(z,f(f(x,x),y))),x) = f(x,f(f(z,f(f(x,x),y)),f(z,f(f(x,x),y)))) # label(824B).
f(f(f(f(x,x),y),f(z,f(f(x,x),y))),x) = f(x,f(f(z,f(f(x,x),y)),f(z,f(f(x,x),y)))) # label(824).
f(f(f(f(f(x,x),f(f(x,x),y)),f(x,x)),f(z,f(y,f(x,x)))),x) = f(x,f(f(z,f(y,f(x,x))),f(z,f(y,f(x,x))))) # label(825A).
f(f(f(f(x,x),f(f(x,x),f(f(x,x),y))),f(z,f(y,f(x,x)))),x) = f(x,f(f(z,f(y,f(x,x))),f(z,f(y,f(x,x))))) # label(825B).
f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x) = f(x,f(f(z,f(y,f(x,x))),f(z,f(y,f(x,x))))) # label(825).
f(f(f(x,f(f(y,f(z,z)),x)),f(x,f(y,f(z,z)))),z) = f(z,f(f(x,f(y,f(z,z))),f(x,f(y,f(z,z))))) # label(826A).
f(x,y) = f(y,f(f(x,f(z,f(y,y))),f(x,f(z,f(y,y))))) # label(826B).
f(x,f(f(y,f(z,f(x,x))),f(y,f(z,f(x,x))))) = f(y,x) # label(826).
f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x) = f(z,x) # label(827).
f(f(f(f(x,x),y),f(z,f(f(f(x,x),f(f(x,x),y)),f(x,x)))),x) = f(z,x) # label(828A).
f(f(f(f(x,x),y),f(z,f(f(x,x),f(f(x,x),f(f(x,x),y))))),x) = f(z,x) # label(828B).
f(f(f(f(x,x),y),f(z,f(f(x,x),y))),x) = f(z,x) # label(828C).
f(x,f(f(y,f(f(x,x),z)),f(y,f(f(x,x),z)))) = f(y,x) # label(828).
f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x) = f(f(f(u,z),f(f(y,f(x,x)),z)),x) # label(829A).
f(x,y) = f(f(f(z,x),f(f(u,f(y,y)),x)),y) # label(829B).
f(f(f(x,y),f(f(z,f(u,u)),y)),u) = f(y,u) # label(829).
f(f(f(f(x,x),y),f(z,f(f(x,x),y))),x) = f(z,x) # label(833).
f(f(f(x,y),f(z,y)),f(f(z,u),f(z,v))) = f(y,f(f(z,u),f(z,v))) # label(834).
f(f(f(f(x,x),y),f(z,f(f(x,x),y))),x) = f(f(f(z,u),f(z,f(f(x,x),y))),x) # label(836A).
f(x,y) = f(f(f(x,z),f(x,f(f(y,y),u))),y) # label(836B).
f(f(f(x,y),f(x,f(f(z,z),u))),z) = f(x,z) # label(836).
f(x,y) = f(y,f(f(x,z),f(x,f(f(y,y),u)))) # label(838A).
f(x,f(f(y,z),f(y,f(f(x,x),u)))) = f(y,x) # label(838).
f(f(f(x,y),f(z,y)),f(f(z,f(f(y,y),u)),f(z,v))) = f(y,f(f(z,v),f(z,f(f(y,y),u)))) # label(839A).
f(x,f(f(y,f(f(x,x),z)),f(y,u))) = f(x,f(f(y,u),f(y,f(f(x,x),z)))) # label(839B).
f(x,f(f(y,f(f(x,x),z)),f(y,u))) = f(y,x) # label(839).
f(f(x,x),f(f(y,f(z,x)),f(y,u))) = f(y,f(x,x)) # label(846).
f(f(x,x),f(f(y,z),f(z,f(u,x)))) = f(z,f(x,x)) # label(848).
f(f(x,x),f(f(y,z),f(z,f(u,x)))) = f(f(x,x),z) # label(850).
f(f(f(x,y),f(x,y)),f(f(z,u),f(x,u))) = f(f(f(x,y),f(x,y)),u) # label(851).
f(f(x,x),f(f(y,f(y,y)),f(f(z,x),u))) = f(f(x,x),u) # label(852).
f(f(x,x),f(f(y,f(y,y)),f(f(x,z),u))) = f(f(x,x),u) # label(853).
f(f(x,x),f(y,y)) = f(f(x,f(y,x)),f(y,y)) # label(855A).
f(f(x,f(y,x)),f(y,y)) = f(f(x,x),f(y,y)) # label(855).
f(f(f(x,y),f(f(x,z),f(x,y))),f(f(x,z),f(x,z))) = f(y,f(f(x,z),f(x,z))) # label(870A).
f(f(f(x,y),f(x,y)),f(f(x,z),f(x,z))) = f(y,f(f(x,z),f(x,z))) # label(870B).
f(f(f(x,y),f(x,y)),z) = f(y,f(f(x,z),f(x,z))) # label(870).
f(x,f(f(y,z),f(y,z))) = f(z,f(f(y,x),f(y,x))) # label(872).
$F # label(873).
f(X,f(Y,f(X,f(Z,Z)))) != f(X,f(Z,f(X,f(Y,Y)))) # label(7).
f(X,f(Z,f(X,f(Y,Y)))) != f(X,f(Y,f(X,f(Z,Z)))) # label(498).
f(x,f(y,f(f(y,z),x))) = f(f(y,z),x) # label(692).
f(f(f(x,y),f(y,f(z,u))),f(z,f(y,f(z,u)))) = f(f(z,u),f(f(x,y),f(y,f(z,u)))) # label(729A).
f(f(f(x,y),f(y,f(z,u))),f(z,f(y,f(z,u)))) = f(y,f(z,u)) # label(729).
f(f(x,f(f(y,f(y,y)),z)),u) = f(u,f(x,f(z,z))) # label(749).
f(f(f(x,x),f(x,f(y,z))),f(y,f(x,f(y,z)))) = f(x,f(y,z)) # label(754A).
f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)) # label(754).
f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z) # label(766).
f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x) = f(f(f(f(y,f(x,x)),z),f(u,z)),x) # label(830A).
f(x,y) = f(f(f(f(z,f(y,y)),x),f(u,x)),y) # label(830B).
f(f(f(f(x,f(y,y)),z),f(u,z)),y) = f(z,y) # label(830).
f(f(f(x,y),f(z,y)),f(f(x,u),f(x,v))) = f(y,f(f(x,u),f(x,v))) # label(835).
f(f(f(x,y),f(x,f(z,u))),f(z,z)) = f(x,f(z,z)) # label(837).
f(f(x,x),f(f(y,f(y,y)),f(f(z,x),f(u,v)))) = f(f(x,x),f(u,f(f(z,x),f(u,v)))) # label(854A).
f(f(x,x),f(y,z)) = f(f(x,x),f(y,f(f(u,x),f(y,z)))) # label(854B).
f(f(x,x),f(y,f(f(z,x),f(y,u)))) = f(f(x,x),f(y,u)) # label(854).
f(f(x,f(f(f(y,f(y,y)),z),x)),z) = f(f(x,x),f(f(f(y,f(y,y)),z),f(f(y,f(y,y)),z))) # label(856A).
f(f(x,f(f(f(y,f(y,y)),z),x)),z) = f(f(x,x),z) # label(856).
f(x,f(f(y,z),f(y,u))) = f(f(f(y,z),f(y,u)),f(f(y,x),f(v,x))) # label(917A).
f(f(f(x,y),f(x,z)),f(f(x,u),f(v,u))) = f(u,f(f(x,y),f(x,z))) # label(917).
f(f(f(x,y),f(x,z)),f(f(x,u),f(v,u))) = f(f(f(x,y),f(x,z)),u) # label(918).
f(f(f(x,y),f(x,f(f(x,z),u))),z) = f(x,f(f(x,z),f(x,z))) # label(921A).
f(f(f(x,y),f(x,f(f(x,z),u))),z) = f(z,x) # label(921).
f(f(x,f(x,y)),f(y,f(f(y,x),z))) = f(f(x,x),f(y,f(f(y,x),z))) # label(922).
f(x,f(f(y,y),f(x,f(f(x,y),z)))) = f(x,f(f(x,y),z)) # label(924).
f(x,f(f(y,y),f(x,z))) = f(x,f(f(x,y),f(x,z))) # label(926).
f(x,f(f(y,y),f(x,z))) = f(f(f(x,y),f(x,z)),x) # label(928A).
f(f(f(x,y),f(x,z)),x) = f(x,f(f(y,y),f(x,z))) # label(928).
f(x,f(f(x,y),f(z,z))) = f(x,f(f(x,z),f(x,y))) # label(929).
f(x,f(f(x,y),f(f(f(z,f(z,z)),u),f(f(z,f(z,z)),u)))) = f(x,f(f(x,y),f(x,f(u,u)))) # label(930A).
f(x,f(f(x,y),z)) = f(x,f(f(x,y),f(x,f(z,z)))) # label(930B).
f(x,f(f(x,y),f(x,f(z,z)))) = f(x,f(f(x,y),z)) # label(930).
f(f(f(x,f(x,x)),f(y,f(f(y,z),u))),y) = f(f(f(y,z),f(y,f(u,u))),y) # label(931A).
f(f(f(x,y),z),x) = f(f(f(x,y),f(x,f(z,z))),x) # label(931B).
f(f(f(x,y),z),x) = f(x,f(f(y,y),f(x,f(z,z)))) # label(931).
f(f(x,f(y,f(z,z))),y) = f(y,f(f(f(f(u,f(u,u)),z),f(f(u,f(u,u)),z)),f(y,f(x,x)))) # label(932A).
f(f(x,f(y,f(z,z))),y) = f(y,f(z,f(y,f(x,x)))) # label(932).
f(f(f(x,f(x,x)),f(y,f(z,f(y,f(u,u))))),y) = f(f(u,f(y,f(z,z))),y) # label(933A).
f(f(x,f(y,f(z,z))),y) = f(f(z,f(y,f(x,x))),y) # label(933B).
f(x,f(y,f(x,f(z,z)))) = f(f(y,f(x,f(z,z))),x) # label(933C).
f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # label(933).
end_of_list.

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

============================== PROCESS GOALS =========================

% Each goal clause was negated; the result (to be placed in sos):

clauses(negated_goals).
f(c2,c1) != f(c1,c2) # answer(comm).
f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one).
f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb).
f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml).
f(c11,f(f(c10,c9),f(c10,c9))) != f(c9,f(f(c10,c11),f(c10,c11))) # answer(assoc).
f(c12,f(c14,f(c12,f(c13,c13)))) != f(c12,f(c13,f(c12,f(c14,c14)))) # answer(mod).
end_of_list.

============================== end of process goals ==================

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y.  [input].
2 f(c2,c1) != f(c1,c2) # answer(comm).  [clausify].
3 f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one).  [clausify].
4 f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb).  [clausify].
5 f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml).  [clausify].
6 f(c11,f(f(c10,c9),f(c10,c9))) != f(c9,f(f(c10,c11),f(c10,c11))) # answer(assoc).  [clausify].
7 f(c12,f(c14,f(c12,f(c13,c13)))) != f(c12,f(c13,f(c12,f(c14,c14)))) # answer(mod).  [clausify].
end_of_list.

clauses(demodulators).
end_of_list.

% 486 hints input.

Predicate elimination: (none).

Auto_denials:
  % assign(max_proofs, 6).  % (Horn set with more than one neg. clause)
    % assign(max_proofs, 6) -> set(restrict_denials).

% Restrict denials; moving clauses to denials list:

clauses(denials).
2 f(c2,c1) != f(c1,c2) # answer(comm).  [clausify].
3 f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one).  [clausify].
4 f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb).  [clausify].
5 f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml).  [clausify].
6 f(c11,f(f(c10,c9),f(c10,c9))) != f(c9,f(f(c10,c11),f(c10,c11))) # answer(assoc).  [clausify].
7 f(c12,f(c14,f(c12,f(c13,c13)))) != f(c12,f(c13,f(c12,f(c14,c14)))) # answer(mod).  [clausify].
end_of_list.

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, f, Z, Y, X ]).
After inverse_order: Function symbol precedence:  lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, f, Z, Y, X ]).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).

Auto_process settings:  no changes.

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

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

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].
end_of_list.

clauses(demodulators).
494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].
end_of_list.

clauses(denials).
495 f(c2,c1) != f(c1,c2) # answer(comm).  [clausify].
496 f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one).  [clausify].
497 f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb).  [clausify].
498 f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml).  [clausify].
499 f(c9,f(f(c10,c11),f(c10,c11))) != f(c11,f(f(c10,c9),f(c10,c9))) # answer(assoc).  [copy(6),flip(a)].
500 f(c12,f(c14,f(c12,f(c13,c13)))) != f(c12,f(c13,f(c12,f(c14,c14)))) # answer(mod).  [clausify].
end_of_list.

% 486 hints processed (44 are redundant).

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

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

% Starting search at 0.04 seconds.

given #1 (I,wt=-975): 494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].

given #2 (F,wt=-965): 501 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z) # label(499).  [para(494(a,1),494(a,1,2,2,2))].

given #3 (F,wt=-959): 502 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y # label(500).  [para(494(a,1),501(a,1,1,2)),demod(494(12),494(12),494(14),494(17),494(30))].

given #4 (T,wt=-987): 503 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A).  [para(494(a,1),502(a,1,2,2))].

given #5 (T,wt=-991): 504 f(f(x,y),f(y,y)) = y # label(508B).  [para(494(a,1),503(a,1,2,1))].

given #6 (A,wt=-963): 506 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(504).  [para(504(a,1),494(a,1,2,2,1,1,1,1))].

given #7 (F,wt=-989): 510 f(f(x,f(y,y)),y) = f(y,y) # label(508).  [para(504(a,1),501(a,1,2,2,1)),demod(504(5),504(5))].

given #8 (F,wt=-989): 512 f(f(f(x,x),y),x) = f(x,x) # label(510B).  [para(503(a,1),504(a,1,1)),demod(503(7)),flip(a)].

given #9 (T,wt=-991): 515 f(f(x,y),f(x,x)) = x # label(513).  [para(504(a,1),512(a,1,1,1)),demod(504(6))].

given #10 (T,wt=-987): 517 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515).  [para(494(a,1),515(a,1,1))].

given #11 (A,wt=-975): 507 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(583A).  [para(504(a,1),494(a,1,2,2,1,1,1))].

given #12 (F,wt=-987): 518 f(x,f(f(x,y),f(x,y))) = f(x,y) # label(516).  [para(515(a,1),515(a,1,1))].

given #13 (F,wt=-985): 513 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511).  [back_demod(505),demod(510(7))].

given #14 (T,wt=-979): 514 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512).  [para(512(a,1),494(a,1,2,2,1,1))].

given #15 (T,wt=-979): 522 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A).  [para(513(a,1),512(a,1)),flip(a)].

given #16 (A,wt=-967): 508 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(506).  [para(504(a,1),501(a,1,2,2,1,1,1,1))].

given #17 (F,wt=-987): 524 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B).  [para(522(a,1),504(a,1,1)),demod(522(9)),flip(a)].

given #18 (F,wt=-987): 527 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523).  [para(504(a,1),524(a,1,2,1)),demod(515(8))].

given #19 (T,wt=-987): 529 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525).  [para(517(a,1),527(a,1,2,2))].

given #20 (T,wt=-979): 523 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520).  [para(517(a,1),514(a,1,2,2,2))].

given #21 (A,wt=-967): 509 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(504(a,1),501(a,1,2,2,1,1,1))].

given #22 (F,wt=-979): 526 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522).  [para(494(a,1),524(a,1,2,2))].

given #23 (F,wt=-979): 528 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524).  [para(515(a,1),524(a,1,2,2))].

given #24 (T,wt=-977): 530 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526).  [para(504(a,1),523(a,1,1)),demod(515(3),515(5))].

given #25 (T,wt=-977): 531 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x) # label(527).  [para(530(a,1),517(a,1,2,1)),demod(530(18),515(11),530(18))].

given #26 (A,wt=-973): 516 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(514).  [para(515(a,1),494(a,1,2,2,1,1))].

given #27 (F,wt=-985): 535 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E).  [para(516(a,1),509(a,1,2,2,1)),demod(515(3),517(6),504(6),515(10),517(13),504(13),515(16),517(19),504(19),504(27),527(27),510(23),515(9),515(3),517(6),504(6)),flip(a)].

given #28 (F,wt=-985): 537 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536).  [para(517(a,1),535(a,1,2,2))].

given #29 (T,wt=-983): 536 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F).  [para(504(a,1),535(a,1,1,1)),demod(515(6))].

given #30 (T,wt=-975): 519 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y # label(517).  [para(517(a,1),494(a,1,2,2,2))].

given #31 (A,wt=-975): 520 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = x # label(518).  [para(494(a,1),517(a,1,2,1)),demod(494(20),494(22))].

given #32 (F,wt=-971): 538 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(537).  [para(494(a,1),536(a,1,2,2))].

given #33 (F,wt=-971): 539 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(538).  [para(515(a,1),536(a,1,2,2))].

given #34 (T,wt=-969): 525 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(533).  [para(515(a,1),508(a,1,2,2,1,1))].

given #35 (T,wt=-967): 521 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y))) = f(y,z) # label(528).  [para(515(a,1),507(a,1,2,2,2))].

============================== PROOF =================================

% Proof 1 at 0.20 (+ 0.00) seconds: absorb.
% Length of proof is 23.
% Level of proof is 13.
% Maximum clause weight is 0.
% Given clauses 35.

494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].
497 f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb).  [clausify].
501 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z) # label(499).  [para(494(a,1),494(a,1,2,2,2))].
502 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y # label(500).  [para(494(a,1),501(a,1,1,2)),demod(494(12),494(12),494(14),494(17),494(30))].
503 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A).  [para(494(a,1),502(a,1,2,2))].
504 f(f(x,y),f(y,y)) = y # label(508B).  [para(494(a,1),503(a,1,2,1))].
505 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,y)),f(y,y)),y),f(y,z)))) = y # label(503).  [para(504(a,1),494(a,1,2,1))].
507 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(583A).  [para(504(a,1),494(a,1,2,2,1,1,1))].
509 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(504(a,1),501(a,1,2,2,1,1,1))].
510 f(f(x,f(y,y)),y) = f(y,y) # label(508).  [para(504(a,1),501(a,1,2,2,1)),demod(504(5),504(5))].
512 f(f(f(x,x),y),x) = f(x,x) # label(510B).  [para(503(a,1),504(a,1,1)),demod(503(7)),flip(a)].
513 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511).  [back_demod(505),demod(510(7))].
515 f(f(x,y),f(x,x)) = x # label(513).  [para(504(a,1),512(a,1,1,1)),demod(504(6))].
516 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(514).  [para(515(a,1),494(a,1,2,2,1,1))].
517 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515).  [para(494(a,1),515(a,1,1))].
521 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y))) = f(y,z) # label(528).  [para(515(a,1),507(a,1,2,2,2))].
522 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A).  [para(513(a,1),512(a,1)),flip(a)].
524 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B).  [para(522(a,1),504(a,1,1)),demod(522(9)),flip(a)].
527 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523).  [para(504(a,1),524(a,1,2,1)),demod(515(8))].
535 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E).  [para(516(a,1),509(a,1,2,2,1)),demod(515(3),517(6),504(6),515(10),517(13),504(13),515(16),517(19),504(19),504(27),527(27),510(23),515(9),515(3),517(6),504(6)),flip(a)].
536 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F).  [para(504(a,1),535(a,1,1,1)),demod(515(6))].
540 f(f(x,x),f(x,y)) = x # label(525).  [para(524(a,1),521(a,1,1)),demod(536(16),515(13),510(11),515(3)),flip(a)].
541 $F # answer(absorb).  [resolve(540,a,497,a)].

============================== end of proof ==========================

NOTE: Disabling denial clause 497.

given #36 (A,wt=-491): 540 f(f(x,x),f(x,y)) = x # label(525).  [para(524(a,1),521(a,1,1)),demod(536(16),515(13),510(11),515(3)),flip(a)].

given #37 (F,wt=-991): 547 f(f(x,x),f(y,x)) = x # label(548).  [para(517(a,1),540(a,1,2))].

given #38 (F,wt=-989): 542 f(x,f(f(x,x),y)) = f(x,x) # label(541E).  [para(527(a,1),521(a,1,1)),demod(540(10),540(12),535(14),504(10)),flip(a)].

given #39 (T,wt=-989): 543 f(x,f(y,f(x,x))) = f(x,x) # label(542E).  [para(529(a,1),521(a,1,1)),demod(540(10),540(12),537(14),504(10)),flip(a)].

given #40 (T,wt=-987): 544 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E).  [para(526(a,1),521(a,1,1)),demod(538(26),540(23),510(18),540(7)),flip(a)].

given #41 (A,wt=-987): 545 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E).  [para(528(a,1),521(a,1,1)),demod(539(26),540(23),510(18),540(7)),flip(a)].

given #42 (F,wt=-975): 548 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y)))) = y # label(546).  [para(540(a,1),519(a,1,2,1))].

given #43 (F,wt=-981): 553 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552).  [para(517(a,1),548(a,1,2))].

given #44 (T,wt=-981): 556 f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y # label(555).  [para(517(a,1),553(a,1,2,1,1,1)),demod(544(4))].

given #45 (T,wt=-981): 557 f(f(x,y),f(f(f(f(x,y),f(z,y)),f(z,y)),y)) = y # label(556).  [para(517(a,1),556(a,1,2,1,1,2)),demod(517(8))].

given #46 (A,wt=-475): 546 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(y,u)))) = y # label(503).  [para(540(a,1),494(a,1,2,1))].

given #47 (F,wt=-977): 554 f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x) # label(553).  [para(504(a,1),553(a,1,2,1,1,1)),demod(547(3))].

given #48 (F,wt=-985): 558 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557).  [para(494(a,1),554(a,1,2,1,1,2)),demod(494(12))].

given #49 (T,wt=-985): 560 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559).  [para(515(a,1),554(a,1,2,1,1,2)),demod(515(4))].

given #50 (T,wt=-989): 562 f(f(x,x),x) = f(x,f(x,x)) # label(561).  [para(512(a,1),560(a,1,2,1)),demod(540(5))].

given #51 (A,wt=-975): 549 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(549).  [back_demod(525),demod(547(3))].

given #52 (F,wt=-985): 563 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562).  [back_demod(561),demod(562(2))].

given #53 (F,wt=-979): 559 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558).  [para(510(a,1),554(a,1,2,1,1,2)),demod(540(4),510(4))].

given #54 (T,wt=-979): 564 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563).  [para(504(a,1),563(a,1,2,1,2)),demod(562(3))].

given #55 (T,wt=-977): 555 f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y) # label(554).  [para(515(a,1),553(a,1,2,1,1,1)),demod(540(3))].

given #56 (A,wt=-969): 550 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(550).  [back_demod(506),demod(547(3))].

given #57 (F,wt=-975): 552 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u)))) = y # label(551).  [para(544(a,1),494(a,1,1)),demod(517(7))].

given #58 (F,wt=-975): 565 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(564).  [para(545(a,1),550(a,1,2,1))].

given #59 (T,wt=-975): 566 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)) # label(565).  [para(512(a,1),565(a,1,2,2,1,1)),demod(540(7))].

given #60 (T,wt=-981): 569 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568).  [para(563(a,1),566(a,1,2,2))].

given #61 (A,wt=-225): 551 f(f(x,y),f(y,f(f(f(f(f(y,x),f(z,y)),f(z,y)),y),f(y,u)))) = y # label(503).  [para(547(a,1),494(a,1,2,1))].

given #62 (F,wt=-977): 568 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)) # label(567D).  [para(531(a,1),566(a,1,2,2,2)),demod(515(17),531(14),544(7)),flip(a)].

given #63 (F,wt=-981): 571 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C).  [para(568(a,1),559(a,1,2,1)),demod(543(14),540(11)),flip(a)].

============================== PROOF =================================

% Proof 2 at 0.42 (+ 0.00) seconds: one.
% Length of proof is 57.
% Level of proof is 22.
% Maximum clause weight is 0.
% Given clauses 63.

494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].
496 f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one).  [clausify].
501 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z) # label(499).  [para(494(a,1),494(a,1,2,2,2))].
502 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y # label(500).  [para(494(a,1),501(a,1,1,2)),demod(494(12),494(12),494(14),494(17),494(30))].
503 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A).  [para(494(a,1),502(a,1,2,2))].
504 f(f(x,y),f(y,y)) = y # label(508B).  [para(494(a,1),503(a,1,2,1))].
505 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,y)),f(y,y)),y),f(y,z)))) = y # label(503).  [para(504(a,1),494(a,1,2,1))].
506 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(504).  [para(504(a,1),494(a,1,2,2,1,1,1,1))].
507 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(583A).  [para(504(a,1),494(a,1,2,2,1,1,1))].
509 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(504(a,1),501(a,1,2,2,1,1,1))].
510 f(f(x,f(y,y)),y) = f(y,y) # label(508).  [para(504(a,1),501(a,1,2,2,1)),demod(504(5),504(5))].
512 f(f(f(x,x),y),x) = f(x,x) # label(510B).  [para(503(a,1),504(a,1,1)),demod(503(7)),flip(a)].
513 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511).  [back_demod(505),demod(510(7))].
514 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512).  [para(512(a,1),494(a,1,2,2,1,1))].
515 f(f(x,y),f(x,x)) = x # label(513).  [para(504(a,1),512(a,1,1,1)),demod(504(6))].
516 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(514).  [para(515(a,1),494(a,1,2,2,1,1))].
517 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515).  [para(494(a,1),515(a,1,1))].
519 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y # label(517).  [para(517(a,1),494(a,1,2,2,2))].
521 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y))) = f(y,z) # label(528).  [para(515(a,1),507(a,1,2,2,2))].
522 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A).  [para(513(a,1),512(a,1)),flip(a)].
523 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520).  [para(517(a,1),514(a,1,2,2,2))].
524 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B).  [para(522(a,1),504(a,1,1)),demod(522(9)),flip(a)].
526 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522).  [para(494(a,1),524(a,1,2,2))].
527 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523).  [para(504(a,1),524(a,1,2,1)),demod(515(8))].
528 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524).  [para(515(a,1),524(a,1,2,2))].
529 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525).  [para(517(a,1),527(a,1,2,2))].
530 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526).  [para(504(a,1),523(a,1,1)),demod(515(3),515(5))].
531 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x) # label(527).  [para(530(a,1),517(a,1,2,1)),demod(530(18),515(11),530(18))].
535 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E).  [para(516(a,1),509(a,1,2,2,1)),demod(515(3),517(6),504(6),515(10),517(13),504(13),515(16),517(19),504(19),504(27),527(27),510(23),515(9),515(3),517(6),504(6)),flip(a)].
536 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F).  [para(504(a,1),535(a,1,1,1)),demod(515(6))].
537 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536).  [para(517(a,1),535(a,1,2,2))].
538 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(537).  [para(494(a,1),536(a,1,2,2))].
539 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(538).  [para(515(a,1),536(a,1,2,2))].
540 f(f(x,x),f(x,y)) = x # label(525).  [para(524(a,1),521(a,1,1)),demod(536(16),515(13),510(11),515(3)),flip(a)].
543 f(x,f(y,f(x,x))) = f(x,x) # label(542E).  [para(529(a,1),521(a,1,1)),demod(540(10),540(12),537(14),504(10)),flip(a)].
544 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E).  [para(526(a,1),521(a,1,1)),demod(538(26),540(23),510(18),540(7)),flip(a)].
545 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E).  [para(528(a,1),521(a,1,1)),demod(539(26),540(23),510(18),540(7)),flip(a)].
547 f(f(x,x),f(y,x)) = x # label(548).  [para(517(a,1),540(a,1,2))].
548 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y)))) = y # label(546).  [para(540(a,1),519(a,1,2,1))].
550 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(550).  [back_demod(506),demod(547(3))].
553 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552).  [para(517(a,1),548(a,1,2))].
554 f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x) # label(553).  [para(504(a,1),553(a,1,2,1,1,1)),demod(547(3))].
558 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557).  [para(494(a,1),554(a,1,2,1,1,2)),demod(494(12))].
559 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558).  [para(510(a,1),554(a,1,2,1,1,2)),demod(540(4),510(4))].
560 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559).  [para(515(a,1),554(a,1,2,1,1,2)),demod(515(4))].
561 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y) # label(560).  [para(545(a,1),558(a,1,2,2)),demod(545(9))].
562 f(f(x,x),x) = f(x,f(x,x)) # label(561).  [para(512(a,1),560(a,1,2,1)),demod(540(5))].
563 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562).  [back_demod(561),demod(562(2))].
564 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563).  [para(504(a,1),563(a,1,2,1,2)),demod(562(3))].
565 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(564).  [para(545(a,1),550(a,1,2,1))].
566 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)) # label(565).  [para(512(a,1),565(a,1,2,2,1,1)),demod(540(7))].
568 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)) # label(567D).  [para(531(a,1),566(a,1,2,2,2)),demod(515(17),531(14),544(7)),flip(a)].
569 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568).  [para(563(a,1),566(a,1,2,2))].
571 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C).  [para(568(a,1),559(a,1,2,1)),demod(543(14),540(11)),flip(a)].
578 f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(y,f(y,y)) # label(576).  [para(571(a,1),564(a,1,2,2)),demod(571(14))].
579 f(x,f(x,x)) = f(y,f(y,y)) # label(577).  [para(571(a,1),569(a,1,2,2)),demod(578(7))].
580 $F # answer(one).  [resolve(579,a,496,a)].

============================== end of proof ==========================

NOTE: Disabling denial clause 496.

NOTE: New constant: 0 f(x,f(x,x)) = c_0.  [new_symbol(579)].
NOTE: New Function symbol precedence:  lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c_0, f, Z, Y, X ]).

given #64 (T,wt=-989): 574 f(f(x,f(x,x)),y) = f(y,y) # label(573).  [para(571(a,1),512(a,1,1))].

given #65 (T,wt=-989): 575 f(f(x,f(x,x)),f(y,y)) = y # label(574).  [para(571(a,1),515(a,1,1))].

given #66 (A,wt=-975): 567 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(z,f(y,x))))) = f(y,x) # label(566).  [para(517(a,1),565(a,1,2,2,2))].

given #67 (F,wt=-989): 576 f(f(x,x),f(y,f(y,y))) = x # label(594).  [para(571(a,1),540(a,1,2))].

given #68 (F,wt=-989): 577 f(x,f(y,f(y,y))) = f(x,x) # label(575).  [para(571(a,1),542(a,1,2))].

============================== PROOF =================================

% Proof 3 at 0.47 (+ 0.00) seconds: oml.
% Length of proof is 53.
% Level of proof is 21.
% Maximum clause weight is 0.
% Given clauses 68.

494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].
498 f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml).  [clausify].
501 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z) # label(499).  [para(494(a,1),494(a,1,2,2,2))].
502 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y # label(500).  [para(494(a,1),501(a,1,1,2)),demod(494(12),494(12),494(14),494(17),494(30))].
503 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A).  [para(494(a,1),502(a,1,2,2))].
504 f(f(x,y),f(y,y)) = y # label(508B).  [para(494(a,1),503(a,1,2,1))].
505 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,y)),f(y,y)),y),f(y,z)))) = y # label(503).  [para(504(a,1),494(a,1,2,1))].
506 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(504).  [para(504(a,1),494(a,1,2,2,1,1,1,1))].
507 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(583A).  [para(504(a,1),494(a,1,2,2,1,1,1))].
509 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(504(a,1),501(a,1,2,2,1,1,1))].
510 f(f(x,f(y,y)),y) = f(y,y) # label(508).  [para(504(a,1),501(a,1,2,2,1)),demod(504(5),504(5))].
512 f(f(f(x,x),y),x) = f(x,x) # label(510B).  [para(503(a,1),504(a,1,1)),demod(503(7)),flip(a)].
513 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511).  [back_demod(505),demod(510(7))].
514 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512).  [para(512(a,1),494(a,1,2,2,1,1))].
515 f(f(x,y),f(x,x)) = x # label(513).  [para(504(a,1),512(a,1,1,1)),demod(504(6))].
516 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(514).  [para(515(a,1),494(a,1,2,2,1,1))].
517 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515).  [para(494(a,1),515(a,1,1))].
519 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y # label(517).  [para(517(a,1),494(a,1,2,2,2))].
521 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y))) = f(y,z) # label(528).  [para(515(a,1),507(a,1,2,2,2))].
522 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A).  [para(513(a,1),512(a,1)),flip(a)].
523 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520).  [para(517(a,1),514(a,1,2,2,2))].
524 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B).  [para(522(a,1),504(a,1,1)),demod(522(9)),flip(a)].
526 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522).  [para(494(a,1),524(a,1,2,2))].
527 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523).  [para(504(a,1),524(a,1,2,1)),demod(515(8))].
528 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524).  [para(515(a,1),524(a,1,2,2))].
529 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525).  [para(517(a,1),527(a,1,2,2))].
530 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526).  [para(504(a,1),523(a,1,1)),demod(515(3),515(5))].
531 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x) # label(527).  [para(530(a,1),517(a,1,2,1)),demod(530(18),515(11),530(18))].
535 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E).  [para(516(a,1),509(a,1,2,2,1)),demod(515(3),517(6),504(6),515(10),517(13),504(13),515(16),517(19),504(19),504(27),527(27),510(23),515(9),515(3),517(6),504(6)),flip(a)].
536 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F).  [para(504(a,1),535(a,1,1,1)),demod(515(6))].
537 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536).  [para(517(a,1),535(a,1,2,2))].
538 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(537).  [para(494(a,1),536(a,1,2,2))].
539 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(538).  [para(515(a,1),536(a,1,2,2))].
540 f(f(x,x),f(x,y)) = x # label(525).  [para(524(a,1),521(a,1,1)),demod(536(16),515(13),510(11),515(3)),flip(a)].
542 f(x,f(f(x,x),y)) = f(x,x) # label(541E).  [para(527(a,1),521(a,1,1)),demod(540(10),540(12),535(14),504(10)),flip(a)].
543 f(x,f(y,f(x,x))) = f(x,x) # label(542E).  [para(529(a,1),521(a,1,1)),demod(540(10),540(12),537(14),504(10)),flip(a)].
544 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E).  [para(526(a,1),521(a,1,1)),demod(538(26),540(23),510(18),540(7)),flip(a)].
545 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E).  [para(528(a,1),521(a,1,1)),demod(539(26),540(23),510(18),540(7)),flip(a)].
547 f(f(x,x),f(y,x)) = x # label(548).  [para(517(a,1),540(a,1,2))].
548 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y)))) = y # label(546).  [para(540(a,1),519(a,1,2,1))].
550 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(550).  [back_demod(506),demod(547(3))].
553 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552).  [para(517(a,1),548(a,1,2))].
554 f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x) # label(553).  [para(504(a,1),553(a,1,2,1,1,1)),demod(547(3))].
555 f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y) # label(554).  [para(515(a,1),553(a,1,2,1,1,1)),demod(540(3))].
559 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558).  [para(510(a,1),554(a,1,2,1,1,2)),demod(540(4),510(4))].
565 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(564).  [para(545(a,1),550(a,1,2,1))].
566 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)) # label(565).  [para(512(a,1),565(a,1,2,2,1,1)),demod(540(7))].
568 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)) # label(567D).  [para(531(a,1),566(a,1,2,2,2)),demod(515(17),531(14),544(7)),flip(a)].
571 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C).  [para(568(a,1),559(a,1,2,1)),demod(543(14),540(11)),flip(a)].
576 f(f(x,x),f(y,f(y,y))) = x # label(594).  [para(571(a,1),540(a,1,2))].
577 f(x,f(y,f(y,y))) = f(x,x) # label(575).  [para(571(a,1),542(a,1,2))].
601 f(x,f(x,f(x,y))) = f(x,y) # label(599).  [para(577(a,1),555(a,1,2,1,1)),demod(576(7))].
602 $F # answer(oml).  [resolve(601,a,498,a)].

============================== end of proof ==========================

NOTE: Disabling denial clause 498.

given #69 (T,wt=-989): 579 f(x,f(x,x)) = f(y,f(y,y)) # label(577).  [para(571(a,1),569(a,1,2,2)),demod(578(7))].

given #70 (T,wt=-989): 599 f(f(x,y),f(f(y,x),y)) = y # label(597).  [para(577(a,1),553(a,1,2,1,1)),demod(576(7))].

given #71 (A,wt=-967): 570 f(f(f(x,y),f(x,y)),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(567B).  [para(515(a,1),569(a,1,2,2))].

given #72 (F,wt=-989): 600 f(x,f(x,f(y,x))) = f(y,x) # label(598).  [para(577(a,1),554(a,1,2,1,1)),demod(576(7))].

given #73 (F,wt=-989): 601 f(x,f(x,f(x,y))) = f(x,y) # label(599).  [para(577(a,1),555(a,1,2,1,1)),demod(576(7))].

given #74 (T,wt=-989): 616 f(f(x,y),f(f(x,y),x)) = x # label(629E).  [para(518(a,1),599(a,1,2,1)),demod(545(4))].

given #75 (T,wt=-987): 581 f(f(x,y),f(f(z,f(z,z)),y)) = y # label(579).  [para(574(a,2),504(a,1,2))].

given #76 (A,wt=-987): 582 f(f(x,y),f(f(z,f(z,z)),x)) = x # label(580).  [para(574(a,2),515(a,1,2))].

given #77 (F,wt=-987): 590 f(f(f(x,f(x,x)),y),f(y,z)) = y # label(583).  [para(574(a,2),540(a,1,1))].

given #78 (F,wt=-989): 629 f(f(x,y),x) = f(x,f(x,y)) # label(623).  [back_demod(624),demod(628(7))].

given #79 (T,wt=-989): 630 f(f(x,y),f(x,f(x,y))) = x # label(629F).  [back_demod(625),demod(629(3),601(3),629(3))].

given #80 (T,wt=-989): 631 f(f(x,y),f(y,f(y,x))) = y # label(625).  [back_demod(617),demod(629(3),601(4),629(3))].

given #81 (A,wt=-985): 583 f(x,f(f(y,f(y,y)),f(z,x))) = f(z,x) # label(581).  [para(574(a,2),517(a,1,2))].

given #82 (F,wt=-989): 634 f(f(x,y),y) = f(y,f(x,y)) # label(628B).  [para(494(a,1),629(a,1,1)),demod(494(14)),flip(a)].

given #83 (F,wt=-989): 635 f(f(x,y),f(y,f(x,y))) = y # label(629).  [para(629(a,1),557(a,1,2,1,1)),demod(634(2),634(5),629(8),600(8),629(5),600(5),634(4))].

given #84 (T,wt=-985): 586 f(x,f(f(y,f(y,y)),f(x,z))) = f(x,z) # label(582).  [para(574(a,2),518(a,1,2))].

given #85 (T,wt=-985): 587 f(f(f(x,f(x,x)),f(y,z)),z) = f(y,z) # label(586).  [para(574(a,1),509(a,1,2,1,2)),demod(571(13),571(14),586(13))].

given #86 (A,wt=-221): 585 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(f(z,f(z,z)),x)),y),f(y,u)))) = y # label(583A).  [para(574(a,2),507(a,1,2,2,1,1,2))].

given #87 (F,wt=-985): 592 f(x,f(f(y,f(y,y)),z)) = f(x,f(z,z)) # label(589B).  [para(574(a,2),559(a,2,2)),demod(583(7)),flip(a)].

given #88 (F,wt=-985): 597 f(f(x,f(x,x)),f(f(y,f(y,y)),z)) = z # label(595).  [para(574(a,2),575(a,1,2))].

given #89 (T,wt=-985): 598 f(x,f(f(y,x),f(z,f(z,z)))) = f(y,x) # label(577A).  [para(577(a,2),517(a,1,2))].

given #90 (T,wt=-985): 608 f(f(x,f(y,f(y,y))),f(z,f(z,z))) = x # label(613).  [para(577(a,2),576(a,1,1))].

given #91 (A,wt=-463): 588 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(f(u,f(u,u)),x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(574(a,2),509(a,1,2,2,1,1,2))].

given #92 (F,wt=-983): 593 f(f(x,x),f(f(x,y),f(x,y))) = f(x,f(x,x)) # label(590).  [para(574(a,1),569(a,1,2))].

given #93 (F,wt=-981): 641 f(x,f(f(y,f(y,y)),z)) = f(x,f(f(u,f(u,u)),z)) # label(576A).  [para(574(a,2),592(a,2,2))].

given #94 (T,wt=-979): 603 f(x,f(f(y,x),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x) # label(601).  [para(577(a,1),550(a,1,2,2,1,1,1)),demod(576(6),576(5))].

given #95 (T,wt=-983): 648 f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z)))) = x # label(640).  [para(635(a,1),603(a,1,2,1)),demod(635(8),629(5),600(5),635(7),635(11))].

given #96 (A,wt=-977): 594 f(f(f(x,f(x,x)),y),f(f(y,f(y,y)),f(y,z))) = f(y,f(y,y)) # label(567A).  [para(574(a,2),569(a,1,1))].

given #97 (F,wt=-981): 653 f(f(f(x,f(x,x)),f(x,f(x,x))),y) = f(z,f(z,z)) # label(567C).  [para(577(a,1),594(a,1,1)),demod(596(13),597(11),596(14))].

given #98 (F,wt=-979): 632 f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,y)) = y # label(626).  [back_demod(610),demod(629(4),629(5),601(5),629(4))].

given #99 (T,wt=-981): 655 f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z)) = z # label(644).  [para(600(a,1),632(a,1,1,2,1))].

given #100 (T,wt=-981): 657 f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z)) = z # label(646).  [para(517(a,1),655(a,1,1,2,2))].

given #101 (A,wt=-477): 595 f(f(x,x),f(f(x,f(f(y,f(y,y)),x)),f(x,z))) = f(x,f(x,x)) # label(567A).  [para(574(a,2),569(a,1,2,1,2))].

given #102 (F,wt=-979): 633 f(f(x,y),f(f(z,f(z,z)),f(f(y,f(y,x)),f(u,y)))) = y # label(627).  [back_demod(609),demod(629(5),629(6),601(6),629(5))].

given #103 (F,wt=-989): 663 f(f(x,f(x,y)),f(y,x)) = x # label(652A).  [para(633(a,1),583(a,1)),flip(a)].

given #104 (T,wt=-979): 636 f(f(x,y),f(f(f(y,y),x),f(f(y,f(x,y)),f(y,z)))) = y # label(630).  [para(629(a,1),552(a,1,2,2,1,1,1)),demod(629(6),601(6),634(5))].

given #105 (T,wt=-977): 618 f(f(f(x,y),f(x,y)),f(x,x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(637).  [para(574(a,1),570(a,1,2))].

given #106 (A,wt=-481): 596 f(x,f(f(y,f(y,y)),f(z,f(z,z)))) = f(z,f(z,z)) # label(576).  [para(574(a,2),571(a,1,2))].

given #107 (F,wt=-983): 664 f(f(x,x),f(f(y,x),f(x,z))) = f(x,f(x,x)) # label(658).  [para(655(a,1),618(a,1,1,1)),demod(655(8),581(14),655(13),655(13),655(13))].

given #108 (F,wt=-981): 667 f(f(x,x),f(f(y,x),f(z,f(z,z)))) = f(x,f(x,x)) # label(660).  [para(579(a,1),664(a,1,2,2))].

given #109 (T,wt=-977): 650 f(x,f(f(y,f(y,y)),f(f(x,f(y,f(y,y))),z))) = f(y,f(y,y)) # label(565A).  [para(575(a,1),648(a,1,2,2,2)),demod(607(6))].

given #110 (T,wt=-977): 660 f(f(f(x,y),f(z,y)),y) = f(f(u,f(u,u)),f(f(x,y),f(z,y))) # label(649).  [para(657(a,1),540(a,1,2)),demod(581(13))].

given #111 (A,wt=-227): 604 f(f(x,f(y,f(y,y))),f(f(x,f(x,x)),f(x,z))) = f(x,f(x,x)) # label(567A).  [para(577(a,2),569(a,1,1))].

given #112 (F,wt=-981): 670 f(f(f(x,y),f(z,y)),y) = f(y,f(f(x,y),f(z,y))) # label(664B).  [para(660(a,1),517(a,1,2,1)),demod(590(11)),flip(a)].

given #113 (F,wt=-979): 672 f(f(x,y),f(y,f(f(z,y),f(x,y)))) = f(f(z,y),f(x,y)) # label(666).  [para(660(a,2),583(a,1,2)),demod(670(5))].

given #114 (T,wt=-979): 673 f(x,f(f(x,y),f(f(z,f(x,y)),x))) = f(f(z,f(x,y)),x) # label(669).  [para(540(a,1),672(a,1,1)),demod(540(6),540(11))].

given #115 (T,wt=-987): 676 f(x,f(f(x,y),f(y,x))) = f(y,x) # label(670).  [para(547(a,1),673(a,1,2,2,1)),demod(547(7))].

given #116 (A,wt=-16): 606 f(f(x,f(x,x)),y) = f(y,f(z,f(z,z))) # label(594B).  [para(577(a,2),574(a,2))].

given #117 (F,wt=-979): 674 f(f(x,y),f(x,f(f(z,x),f(x,y)))) = f(f(z,x),f(x,y)) # label(667).  [para(545(a,1),672(a,1,1)),demod(545(6),545(11))].

given #118 (F,wt=-979): 675 f(f(x,y),f(y,f(f(y,z),f(x,y)))) = f(f(y,z),f(x,y)) # label(668).  [para(545(a,1),672(a,1,2,2,1)),demod(545(10))].

given #119 (T,wt=-985): 677 f(f(x,y),f(y,x)) = f(f(y,x),f(y,x)) # label(671A).  [para(676(a,1),675(a,1,2)),flip(a)].

% Operation f is commutative; redundancy checks enabled.

============================== PROOF =================================

% Proof 4 at 0.94 (+ 0.02) seconds: comm.
% Length of proof is 89.
% Level of proof is 34.
% Maximum clause weight is 0.
% Given clauses 119.

494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].
495 f(c2,c1) != f(c1,c2) # answer(comm).  [clausify].
501 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z) # label(499).  [para(494(a,1),494(a,1,2,2,2))].
502 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y # label(500).  [para(494(a,1),501(a,1,1,2)),demod(494(12),494(12),494(14),494(17),494(30))].
503 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A).  [para(494(a,1),502(a,1,2,2))].
504 f(f(x,y),f(y,y)) = y # label(508B).  [para(494(a,1),503(a,1,2,1))].
505 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,y)),f(y,y)),y),f(y,z)))) = y # label(503).  [para(504(a,1),494(a,1,2,1))].
506 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(504).  [para(504(a,1),494(a,1,2,2,1,1,1,1))].
507 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(583A).  [para(504(a,1),494(a,1,2,2,1,1,1))].
508 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(506).  [para(504(a,1),501(a,1,2,2,1,1,1,1))].
509 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(504(a,1),501(a,1,2,2,1,1,1))].
510 f(f(x,f(y,y)),y) = f(y,y) # label(508).  [para(504(a,1),501(a,1,2,2,1)),demod(504(5),504(5))].
512 f(f(f(x,x),y),x) = f(x,x) # label(510B).  [para(503(a,1),504(a,1,1)),demod(503(7)),flip(a)].
513 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511).  [back_demod(505),demod(510(7))].
514 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512).  [para(512(a,1),494(a,1,2,2,1,1))].
515 f(f(x,y),f(x,x)) = x # label(513).  [para(504(a,1),512(a,1,1,1)),demod(504(6))].
516 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(514).  [para(515(a,1),494(a,1,2,2,1,1))].
517 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515).  [para(494(a,1),515(a,1,1))].
519 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y # label(517).  [para(517(a,1),494(a,1,2,2,2))].
520 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = x # label(518).  [para(494(a,1),517(a,1,2,1)),demod(494(20),494(22))].
521 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y))) = f(y,z) # label(528).  [para(515(a,1),507(a,1,2,2,2))].
522 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A).  [para(513(a,1),512(a,1)),flip(a)].
523 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520).  [para(517(a,1),514(a,1,2,2,2))].
524 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B).  [para(522(a,1),504(a,1,1)),demod(522(9)),flip(a)].
525 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(533).  [para(515(a,1),508(a,1,2,2,1,1))].
526 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522).  [para(494(a,1),524(a,1,2,2))].
527 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523).  [para(504(a,1),524(a,1,2,1)),demod(515(8))].
528 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524).  [para(515(a,1),524(a,1,2,2))].
529 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525).  [para(517(a,1),527(a,1,2,2))].
530 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526).  [para(504(a,1),523(a,1,1)),demod(515(3),515(5))].
531 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x) # label(527).  [para(530(a,1),517(a,1,2,1)),demod(530(18),515(11),530(18))].
535 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E).  [para(516(a,1),509(a,1,2,2,1)),demod(515(3),517(6),504(6),515(10),517(13),504(13),515(16),517(19),504(19),504(27),527(27),510(23),515(9),515(3),517(6),504(6)),flip(a)].
536 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F).  [para(504(a,1),535(a,1,1,1)),demod(515(6))].
537 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536).  [para(517(a,1),535(a,1,2,2))].
538 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(537).  [para(494(a,1),536(a,1,2,2))].
539 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(538).  [para(515(a,1),536(a,1,2,2))].
540 f(f(x,x),f(x,y)) = x # label(525).  [para(524(a,1),521(a,1,1)),demod(536(16),515(13),510(11),515(3)),flip(a)].
542 f(x,f(f(x,x),y)) = f(x,x) # label(541E).  [para(527(a,1),521(a,1,1)),demod(540(10),540(12),535(14),504(10)),flip(a)].
543 f(x,f(y,f(x,x))) = f(x,x) # label(542E).  [para(529(a,1),521(a,1,1)),demod(540(10),540(12),537(14),504(10)),flip(a)].
544 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E).  [para(526(a,1),521(a,1,1)),demod(538(26),540(23),510(18),540(7)),flip(a)].
545 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E).  [para(528(a,1),521(a,1,1)),demod(539(26),540(23),510(18),540(7)),flip(a)].
547 f(f(x,x),f(y,x)) = x # label(548).  [para(517(a,1),540(a,1,2))].
548 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y)))) = y # label(546).  [para(540(a,1),519(a,1,2,1))].
549 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(549).  [back_demod(525),demod(547(3))].
550 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(550).  [back_demod(506),demod(547(3))].
553 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552).  [para(517(a,1),548(a,1,2))].
554 f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x) # label(553).  [para(504(a,1),553(a,1,2,1,1,1)),demod(547(3))].
555 f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y) # label(554).  [para(515(a,1),553(a,1,2,1,1,1)),demod(540(3))].
558 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557).  [para(494(a,1),554(a,1,2,1,1,2)),demod(494(12))].
559 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558).  [para(510(a,1),554(a,1,2,1,1,2)),demod(540(4),510(4))].
560 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559).  [para(515(a,1),554(a,1,2,1,1,2)),demod(515(4))].
561 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y) # label(560).  [para(545(a,1),558(a,1,2,2)),demod(545(9))].
562 f(f(x,x),x) = f(x,f(x,x)) # label(561).  [para(512(a,1),560(a,1,2,1)),demod(540(5))].
563 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562).  [back_demod(561),demod(562(2))].
564 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563).  [para(504(a,1),563(a,1,2,1,2)),demod(562(3))].
565 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(564).  [para(545(a,1),550(a,1,2,1))].
566 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)) # label(565).  [para(512(a,1),565(a,1,2,2,1,1)),demod(540(7))].
568 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)) # label(567D).  [para(531(a,1),566(a,1,2,2,2)),demod(515(17),531(14),544(7)),flip(a)].
569 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568).  [para(563(a,1),566(a,1,2,2))].
571 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C).  [para(568(a,1),559(a,1,2,1)),demod(543(14),540(11)),flip(a)].
574 f(f(x,f(x,x)),y) = f(y,y) # label(573).  [para(571(a,1),512(a,1,1))].
576 f(f(x,x),f(y,f(y,y))) = x # label(594).  [para(571(a,1),540(a,1,2))].
577 f(x,f(y,f(y,y))) = f(x,x) # label(575).  [para(571(a,1),542(a,1,2))].
578 f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(y,f(y,y)) # label(576).  [para(571(a,1),564(a,1,2,2)),demod(571(14))].
579 f(x,f(x,x)) = f(y,f(y,y)) # label(577).  [para(571(a,1),569(a,1,2,2)),demod(578(7))].
581 f(f(x,y),f(f(z,f(z,z)),y)) = y # label(579).  [para(574(a,2),504(a,1,2))].
583 f(x,f(f(y,f(y,y)),f(z,x))) = f(z,x) # label(581).  [para(574(a,2),517(a,1,2))].
590 f(f(f(x,f(x,x)),y),f(y,z)) = y # label(583).  [para(574(a,2),540(a,1,1))].
593 f(f(x,x),f(f(x,y),f(x,y))) = f(x,f(x,x)) # label(590).  [para(574(a,1),569(a,1,2))].
599 f(f(x,y),f(f(y,x),y)) = y # label(597).  [para(577(a,1),553(a,1,2,1,1)),demod(576(7))].
600 f(x,f(x,f(y,x))) = f(y,x) # label(598).  [para(577(a,1),554(a,1,2,1,1)),demod(576(7))].
601 f(x,f(x,f(x,y))) = f(x,y) # label(599).  [para(577(a,1),555(a,1,2,1,1)),demod(576(7))].
610 f(f(f(x,f(x,x)),f(f(f(f(f(y,z),y),y),y),f(y,u))),f(y,y)) = y # label(607).  [para(579(a,1),520(a,1,1,1)),demod(540(6),540(7))].
624 f(f(x,y),f(f(f(x,f(x,y)),x),f(x,f(x,y)))) = f(x,f(x,y)) # label(616).  [para(601(a,1),599(a,1,1))].
628 f(f(f(x,y),x),f(x,y)) = x # label(620).  [para(590(a,1),549(a,1,2,1,1,1)),demod(590(6),593(6),590(9),583(9),590(9))].
629 f(f(x,y),x) = f(x,f(x,y)) # label(623).  [back_demod(624),demod(628(7))].
632 f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,y)) = y # label(626).  [back_demod(610),demod(629(4),629(5),601(5),629(4))].
655 f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z)) = z # label(644).  [para(600(a,1),632(a,1,1,2,1))].
657 f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z)) = z # label(646).  [para(517(a,1),655(a,1,1,2,2))].
660 f(f(f(x,y),f(z,y)),y) = f(f(u,f(u,u)),f(f(x,y),f(z,y))) # label(649).  [para(657(a,1),540(a,1,2)),demod(581(13))].
670 f(f(f(x,y),f(z,y)),y) = f(y,f(f(x,y),f(z,y))) # label(664B).  [para(660(a,1),517(a,1,2,1)),demod(590(11)),flip(a)].
672 f(f(x,y),f(y,f(f(z,y),f(x,y)))) = f(f(z,y),f(x,y)) # label(666).  [para(660(a,2),583(a,1,2)),demod(670(5))].
673 f(x,f(f(x,y),f(f(z,f(x,y)),x))) = f(f(z,f(x,y)),x) # label(669).  [para(540(a,1),672(a,1,1)),demod(540(6),540(11))].
675 f(f(x,y),f(y,f(f(y,z),f(x,y)))) = f(f(y,z),f(x,y)) # label(668).  [para(545(a,1),672(a,1,2,2,1)),demod(545(10))].
676 f(x,f(f(x,y),f(y,x))) = f(y,x) # label(670).  [para(547(a,1),673(a,1,2,2,1)),demod(547(7))].
677 f(f(x,y),f(y,x)) = f(f(y,x),f(y,x)) # label(671A).  [para(676(a,1),675(a,1,2)),flip(a)].
678 f(f(x,f(y,z)),f(f(z,y),f(y,z))) = f(y,z) # label(672).  [para(677(a,2),504(a,1,2))].
680 f(x,y) = f(y,x) # label(933C).  [para(677(a,1),677(a,1,1)),demod(540(7),678(8))].
681 $F # answer(comm).  [resolve(680,a,495,a)].

============================== end of proof ==========================

NOTE: Disabling denial clause 495.

given #120 (T,wt=-993): 680 f(x,y) = f(y,x) # label(933C).  [para(677(a,1),677(a,1,1)),demod(540(7),678(8))].

given #121 (A,wt=-485): 607 f(f(x,f(x,x)),f(y,f(z,f(z,z)))) = y # label(567D).  [para(577(a,2),575(a,1,2))].

given #122 (F,wt=-989): 679 f(f(x,f(y,x)),f(x,y)) = x # label(673).  [para(677(a,1),648(a,1,2,2)),demod(518(6))].

given #123 (F,wt=-989): 685 f(f(x,y),f(x,f(y,x))) = x # label(677).  [para(680(a,1),630(a,1,2,2))].

given #124 (T,wt=-989): 689 f(f(x,f(y,x)),f(y,x)) = x # label(629G).  [para(680(a,1),635(a,1))].

given #125 (T,wt=-985): 690 f(x,f(f(f(y,y),y),f(x,z))) = f(x,z) # label(563A).  [para(680(a,1),586(a,1,2,1))].

given #126 (A,wt=-481): 613 f(f(x,x),f(f(y,f(y,y)),f(x,z))) = f(x,f(x,x)) # label(568).  [para(579(a,1),569(a,1,2,1))].

given #127 (F,wt=-985): 691 f(f(f(x,f(x,x)),f(y,z)),y) = f(z,y) # label(678).  [para(680(a,1),587(a,1,1,2))].

given #128 (F,wt=-985): 692 f(f(f(x,f(x,x)),y),z) = f(z,f(y,y)) # label(679).  [para(680(a,1),592(a,1))].

given #129 (T,wt=-983): 678 f(f(x,f(y,z)),f(f(z,y),f(y,z))) = f(y,z) # label(672).  [para(677(a,2),504(a,1,2))].

given #130 (T,wt=-983): 682 f(x,f(f(y,x),f(y,f(z,f(y,x))))) = f(y,x) # label(676).  [back_demod(639),demod(679(5))].

given #131 (A,wt=-235): 614 f(x,f(f(y,f(y,y)),x)) = f(z,f(z,z)) # label(567D).  [para(574(a,2),579(a,1,2))].

given #132 (F,wt=-987): 706 f(x,f(f(y,z),f(z,x))) = f(z,x) # label(689).  [para(674(a,1),682(a,1,2))].

given #133 (F,wt=-987): 710 f(x,f(f(y,z),f(y,x))) = f(y,x) # label(691).  [para(545(a,1),706(a,1,2,1))].

given #134 (T,wt=-987): 714 f(x,f(f(y,z),f(x,z))) = f(z,x) # label(696).  [para(680(a,1),706(a,1,2,2))].

given #135 (T,wt=-987): 715 f(x,f(f(y,x),f(z,y))) = f(y,x) # label(697).  [para(680(a,1),706(a,1,2))].

given #136 (A,wt=-47): 615 f(x,f(x,f(y,f(y,y)))) = f(z,f(z,z)) # label(567D).  [para(577(a,2),579(a,1,2))].

given #137 (F,wt=-987): 719 f(f(f(x,y),f(x,z)),z) = f(x,z) # label(701A).  [para(710(a,1),680(a,1)),flip(a)].

given #138 (F,wt=-987): 720 f(x,f(f(y,x),f(y,z))) = f(y,x) # label(702).  [para(680(a,1),710(a,1,2))].

given #139 (T,wt=-987): 722 f(f(f(x,y),f(z,y)),z) = f(y,z) # label(704A).  [para(714(a,1),680(a,1)),flip(a)].

given #140 (T,wt=-987): 723 f(x,f(f(x,y),f(z,y))) = f(y,x) # label(705).  [para(680(a,1),714(a,1,2))].

given #141 (A,wt=-465): 619 f(f(f(x,f(x,x)),f(y,z)),f(f(f(y,z),f(f(y,z),f(y,z))),y)) = f(f(y,z),f(f(y,z),f(y,z))) # label(567B).  [para(574(a,2),570(a,1,1))].

given #142 (F,wt=-987): 741 f(f(f(x,y),f(z,y)),x) = f(y,x) # label(725).  [para(680(a,1),722(a,1,1))].

given #143 (F,wt=-985): 708 f(x,f(y,f(f(y,z),x))) = f(f(y,z),x) # label(692).  [para(540(a,1),706(a,1,2,1))].

given #144 (T,wt=-985): 709 f(x,f(y,f(f(z,y),x))) = f(f(z,y),x) # label(690).  [para(547(a,1),706(a,1,2,1))].

given #145 (T,wt=-985): 713 f(f(x,y),f(f(z,f(y,f(y,x))),y)) = y # label(695).  [para(663(a,1),706(a,1,2,2)),demod(663(10))].

given #146 (A,wt=-215): 620 f(f(f(x,y),f(x,y)),f(f(f(x,y),f(f(z,f(z,z)),f(x,y))),x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(567B).  [para(574(a,2),570(a,1,2,1,2))].

given #147 (F,wt=-985): 717 f(f(x,f(y,x)),f(f(f(y,x),z),x)) = x # label(629D).  [para(635(a,1),710(a,1,2,2)),demod(635(10))].

given #148 (F,wt=-985): 721 f(f(x,y),z) = f(z,f(y,f(z,f(x,y)))) # label(703A).  [para(547(a,1),714(a,1,2,1)),flip(a)].

given #149 (T,wt=-985): 725 f(x,f(f(f(y,z),x),z)) = f(f(y,z),x) # label(708).  [para(547(a,1),715(a,1,2,2))].

given #150 (T,wt=-985): 735 f(f(x,f(y,x)),f(x,f(f(x,y),z))) = x # label(718).  [para(685(a,1),720(a,1,2,1)),demod(685(10))].

given #151 (A,wt=-90): 621 f(f(f(x,y),f(z,f(z,z))),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(567B).  [para(577(a,2),570(a,1,1))].

given #152 (F,wt=-985): 739 f(f(x,f(y,f(x,z))),y) = f(f(x,z),y) # label(722).  [para(540(a,1),722(a,1,1,1))].

given #153 (F,wt=-985): 740 f(f(f(x,f(y,z)),z),f(z,f(z,y))) = z # label(724).  [para(631(a,1),722(a,2)),demod(663(6))].

given #154 (T,wt=-985): 743 f(x,f(f(x,f(y,z)),z)) = f(f(y,z),x) # label(726).  [para(547(a,1),723(a,1,2,2))].

given #155 (T,wt=-985): 744 f(f(f(x,f(y,z)),z),x) = f(f(y,z),x) # label(728).  [para(547(a,1),741(a,1,1,2))].

given #156 (A,wt=-27): 622 f(f(f(x,y),f(x,y)),f(f(f(x,y),f(f(x,y),f(z,f(z,z)))),x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(567B).  [para(577(a,2),570(a,1,2,1,2))].

given #157 (F,wt=-985): 747 f(f(f(x,y),y),f(f(z,f(x,y)),y)) = y # label(629A).  [para(600(a,1),713(a,1,2,1,2))].

given #158 (F,wt=-985): 749 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)) # label(731).  [para(721(a,1),680(a,1))].

given #159 (T,wt=-985): 756 f(f(f(x,f(y,z)),y),f(y,f(y,z))) = y # label(723).  [para(680(a,1),740(a,1,1,1,2))].

given #160 (T,wt=-985): 758 f(f(x,f(y,f(z,x))),y) = f(y,f(z,x)) # label(736A).  [para(749(a,1),680(a,1)),flip(a)].

given #161 (A,wt=-4): 623 f(f(f(x,y),f(x,y)),f(f(z,f(z,z)),x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(567B).  [para(579(a,1),570(a,1,2,1))].

given #162 (F,wt=-983): 699 f(f(x,f(x,x)),f(y,z)) = f(f(y,z),f(z,y)) # label(682B).  [para(691(a,1),540(a,1,2)),demod(581(9)),flip(a)].

given #163 (F,wt=-983): 703 f(f(x,f(y,z)),f(f(y,z),f(z,y))) = f(z,y) # label(686).  [para(680(a,1),678(a,1,1,2))].

given #164 (T,wt=-983): 765 f(f(f(x,y),f(y,x)),f(z,f(x,y))) = f(y,x) # label(740A).  [para(703(a,1),680(a,1)),flip(a)].

given #165 (T,wt=-983): 766 f(f(f(x,y),f(y,x)),f(z,f(y,x))) = f(x,y) # label(741).  [para(680(a,1),765(a,1,1))].

given #166 (A,wt=-973): 638 f(f(x,y),f(f(f(y,y),z),f(f(u,f(u,u)),f(f(z,f(f(y,x),z)),y)))) = y # label(632).  [back_demod(589),demod(634(8))].

given #167 (F,wt=-985): 771 f(f(x,y),f(f(z,f(f(y,x),z)),y)) = y # label(759).  [para(638(a,1),749(a,1,2,2)),demod(587(9),638(18))].

given #168 (F,wt=-985): 772 f(f(f(x,f(f(y,z),x)),y),f(z,y)) = y # label(760).  [para(638(a,1),758(a,1,1,2)),demod(587(8),638(18))].

given #169 (T,wt=-985): 773 f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z) # label(761).  [para(515(a,1),771(a,1,2,1,2,1)),demod(540(3))].

given #170 (T,wt=-985): 775 f(f(x,y),f(f(z,f(z,f(y,x))),y)) = y # label(625A).  [para(680(a,1),771(a,1,2,1,2))].

given #171 (A,wt=-29): 640 f(f(x,y),f(f(f(y,y),f(f(z,f(z,z)),x)),f(f(f(x,f(f(u,f(u,u)),x)),y),f(y,v)))) = y # label(583A).  [para(574(a,2),585(a,1,2,1,2))].

given #172 (F,wt=-985): 781 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z) # label(766).  [para(680(a,1),773(a,1,2,1,2))].

given #173 (F,wt=-981): 693 f(f(f(x,f(x,x)),y),z) = f(z,f(f(u,f(u,u)),y)) # label(527C).  [para(680(a,1),641(a,1))].

given #174 (T,wt=-981): 724 f(f(f(x,y),f(z,y)),f(f(u,z),f(y,z))) = f(y,z) # label(745A).  [para(714(a,1),706(a,1,2,2)),demod(714(11))].

given #175 (T,wt=-981): 736 f(x,f(f(y,f(f(z,x),f(z,u))),f(z,x))) = f(z,x) # label(559A).  [para(720(a,1),714(a,1,2,2)),demod(730(11))].

given #176 (A,wt=-475): 643 f(f(x,x),f(f(y,f(y,y)),f(z,f(f(u,f(u,u)),x)))) = f(z,f(x,x)) # label(570A).  [para(592(a,2),583(a,1,2,2))].

given #177 (F,wt=-981): 737 f(f(f(x,y),f(z,x)),f(f(x,y),f(y,u))) = f(x,y) # label(674B).  [para(715(a,1),720(a,1,2,1)),demod(715(11))].

given #178 (F,wt=-981): 750 f(f(f(f(x,f(x,x)),y),z),u) = f(u,f(z,f(y,y))) # label(732).  [para(692(a,2),721(a,1,1)),demod(749(11))].

given #179 (T,wt=-981): 768 f(x,f(f(f(y,z),x),f(u,f(z,y)))) = f(f(y,z),x) # label(743).  [para(765(a,1),725(a,1,2,1,1)),demod(765(12))].

given #180 (T,wt=-981): 777 f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),y)) = y # label(763).  [para(771(a,1),714(a,1,2,2)),demod(772(14))].

given #181 (A,wt=-84): 644 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(u,f(u,u)),x)),f(f(f(x,f(f(v,f(v,v)),x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(574(a,2),588(a,1,2,1,2))].

given #182 (F,wt=-981): 780 f(f(x,x),f(f(y,x),f(f(x,x),z))) = f(f(x,x),z) # label(765).  [para(667(a,1),773(a,1,2,1,2)),demod(608(8))].

given #183 (F,wt=-985): 793 f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z) # label(772).  [para(504(a,1),780(a,1,1)),demod(540(5),540(8))].

given #184 (T,wt=-985): 796 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z) # label(775).  [para(680(a,1),793(a,1,2,1))].

given #185 (T,wt=-985): 797 f(x,f(f(f(x,x),y),f(z,x))) = f(z,x) # label(776).  [para(600(a,1),796(a,1,2,2)),demod(600(8))].

given #186 (A,wt=-21): 645 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,f(u,f(u,u)))),f(f(f(x,f(f(v,f(v,v)),x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(577(a,2),588(a,1,2,1,2))].

given #187 (F,wt=-985): 800 f(f(f(f(x,x),y),f(z,x)),x) = f(z,x) # label(779A).  [para(797(a,1),680(a,1)),flip(a)].

given #188 (F,wt=-981): 788 f(f(f(x,y),f(f(z,u),y)),f(u,z)) = f(y,f(z,u)) # label(745).  [para(677(a,2),724(a,1,2,1)),demod(766(10))].

given #189 (T,wt=-981): 792 f(f(x,f(f(y,f(y,y)),z)),u) = f(u,f(x,f(z,z))) # label(749).  [para(680(a,1),750(a,1,1))].

given #190 (T,wt=-981): 795 f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y) # label(774).  [para(680(a,1),780(a,1,2))].

given #191 (A,wt=-481): 646 f(f(x,x),f(f(x,y),f(z,f(z,z)))) = f(x,f(x,x)) # label(577A).  [para(577(a,2),593(a,1,2))].

given #192 (F,wt=-979): 695 f(f(x,y),f(f(z,f(z,z)),f(f(f(y,x),y),f(u,y)))) = y # label(627C).  [para(680(a,1),633(a,1,2,2,1))].

given #193 (F,wt=-979): 697 f(f(x,y),f(f(f(y,y),x),f(f(f(x,y),y),f(y,z)))) = y # label(630C).  [para(680(a,1),636(a,1,2,2,1))].

given #194 (T,wt=-979): 764 f(f(f(x,f(x,x)),f(y,f(z,u))),f(u,z)) = f(y,f(z,u)) # label(682A).  [para(703(a,1),590(a,1,2))].

given #195 (T,wt=-979): 783 f(f(f(x,y),f(x,z)),f(f(u,f(x,u)),f(x,z))) = f(x,z) # label(761A).  [para(773(a,1),719(a,1,1,2)),demod(773(13))].

given #196 (A,wt=-217): 647 f(f(f(x,f(x,x)),y),f(f(z,f(z,z)),f(u,f(f(v,f(v,v)),y)))) = f(u,f(f(x,f(x,x)),y)) # label(570A).  [para(641(a,1),583(a,1,2,2))].

given #197 (F,wt=-979): 804 f(f(x,y),f(f(f(y,y),z),f(f(y,f(x,y)),f(y,u)))) = y # label(781).  [para(800(a,1),636(a,1,1)),demod(795(7),800(8))].

given #198 (F,wt=-979): 805 f(x,f(f(y,x),f(f(f(f(x,x),z),f(y,x)),u))) = f(y,x) # label(601B).  [para(800(a,1),720(a,1,2,1)),demod(800(13))].

given #199 (T,wt=-979): 817 f(f(f(x,y),f(x,z)),f(f(f(x,u),u),f(x,z))) = f(x,z) # label(554A).  [para(680(a,1),783(a,1,2,1))].

given #200 (T,wt=-981): 824 f(f(f(f(x,y),z),y),f(f(f(f(x,y),u),u),y)) = y # label(555A).  [para(504(a,1),817(a,1,1,2)),demod(504(9),504(11))].

given #201 (A,wt=-35): 652 f(f(f(x,f(x,x)),y),f(f(y,f(f(z,f(z,z)),y)),f(y,u))) = f(y,f(y,y)) # label(567A).  [para(574(a,2),594(a,1,2,1,2))].

given #202 (F,wt=-979): 818 f(f(x,x),f(f(f(x,x),y),f(f(z,f(z,z)),f(x,u)))) = x # label(783).  [para(579(a,1),804(a,1,2,2,1))].

given #203 (F,wt=-983): 830 f(f(x,f(f(y,f(y,y)),f(z,u))),f(z,z)) = z # label(789A).  [para(818(a,1),743(a,1)),flip(a)].

given #204 (T,wt=-983): 833 f(f(x,f(y,y)),f(f(z,y),f(z,y))) = f(z,y) # label(791).  [para(713(a,1),830(a,1,1,2)),demod(547(6),547(7),547(10))].

given #205 (T,wt=-983): 837 f(f(f(x,y),f(x,y)),f(z,f(y,y))) = f(x,y) # label(794A).  [para(833(a,1),680(a,1)),flip(a)].

given #206 (A,wt=-4): 654 f(f(f(x,f(x,x)),y),f(f(y,f(y,f(z,f(z,z)))),f(y,u))) = f(y,f(y,y)) # label(567A).  [para(577(a,2),594(a,1,2,1,2))].

given #207 (F,wt=-981): 835 f(f(x,y),f(f(z,f(y,y)),f(x,y))) = f(z,f(y,y)) # label(792).  [para(833(a,1),630(a,1,1)),demod(833(9))].

given #208 (F,wt=-985): 841 f(f(x,f(y,x)),f(x,f(z,f(y,y)))) = x # label(798).  [para(835(a,1),735(a,1,2,2))].

given #209 (T,wt=-985): 844 f(f(f(x,f(y,x)),f(y,y)),x) = f(x,x) # label(800A).  [para(841(a,1),739(a,1,1)),flip(a)].

given #210 (T,wt=-979): 826 f(f(f(x,y),f(z,x)),f(f(f(x,u),u),f(z,x))) = f(z,x) # label(553A).  [para(600(a,1),817(a,1,1,2)),demod(600(8),600(11))].

given #211 (A,wt=-481): 656 f(f(f(x,f(x,x)),f(f(y,z),f(y,u))),f(y,y)) = y # label(626).  [para(601(a,1),632(a,1,1,2,1))].

given #212 (F,wt=-979): 839 f(x,f(f(f(f(y,y),z),x),f(u,y))) = f(f(f(y,y),z),x) # label(796).  [para(837(a,1),768(a,1,2,2))].

given #213 (F,wt=-981): 852 f(x,f(f(f(y,y),z),f(f(y,u),x))) = f(f(y,u),x) # label(817).  [para(839(a,1),768(a,1,2))].

given #214 (T,wt=-981): 855 f(f(x,f(f(y,f(f(z,f(x,x)),y)),z)),z) = f(z,z) # label(822A).  [para(777(a,1),852(a,1,2)),flip(a)].

given #215 (T,wt=-981): 856 f(f(f(x,f(f(y,f(z,z)),x)),y),z) = f(z,f(y,y)) # label(823A).  [para(855(a,1),743(a,1,2)),flip(a)].

given #216 (A,wt=-481): 658 f(f(x,x),f(f(y,f(y,y)),f(f(z,x),f(x,u)))) = x # label(529).  [para(655(a,1),545(a,1,1,1)),demod(655(8),655(16))].

given #217 (F,wt=-979): 851 f(x,f(f(y,z),f(f(f(z,z),u),x))) = f(f(f(z,z),u),x) # label(510A).  [para(680(a,1),839(a,1,2))].

given #218 (F,wt=-981): 864 f(x,f(f(y,f(x,x)),f(f(x,f(z,x)),x))) = f(z,x) # label(620B).  [para(800(a,1),851(a,2)),demod(540(5))].

given #219 (T,wt=-979): 858 f(x,f(f(y,f(z,f(x,x))),f(y,f(z,f(x,x))))) = f(y,x) # label(826B).  [para(744(a,1),856(a,1,1,1,2)),demod(679(8)),flip(a)].

given #220 (T,wt=-983): 866 f(f(f(x,y),f(f(z,f(u,u)),y)),u) = f(y,u) # label(829B).  [para(722(a,1),858(a,1,2,1)),demod(722(11),858(8)),flip(a)].

given #221 (A,wt=-477): 659 f(f(f(x,f(x,x)),f(f(y,f(z,z)),f(u,f(z,z)))),z) = f(z,z) # label(527).  [para(504(a,1),657(a,1,2))].

given #222 (F,wt=-983): 867 f(f(f(f(x,f(y,y)),z),f(u,z)),y) = f(z,y) # label(830B).  [para(741(a,1),858(a,1,2,1)),demod(741(11),858(8)),flip(a)].

given #223 (F,wt=-977): 745 f(f(f(x,y),f(y,f(z,u))),f(z,f(y,f(z,u)))) = f(y,f(z,u)) # label(754A).  [para(706(a,1),708(a,1,2,2)),demod(706(14))].

given #224 (T,wt=-985): 869 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)) # label(754).  [para(510(a,1),745(a,1,1,1)),demod(540(4))].

given #225 (T,wt=-977): 791 f(x,f(f(y,f(y,y)),f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,x) # label(748).  [para(750(a,2),655(a,1)),demod(504(5))].

given #226 (A,wt=-477): 661 f(x,f(f(y,f(y,y)),f(f(x,f(z,x)),f(u,f(z,x))))) = f(z,x) # label(526).  [para(504(a,1),633(a,1,2,2,1,2)),demod(547(3),634(4))].

given #227 (F,wt=-981): 872 f(x,f(y,f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,x) # label(797).  [para(791(a,1),837(a,1,1,1)),demod(791(10),540(3),581(17),791(16))].

given #228 (F,wt=-985): 876 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x # label(808).  [para(750(a,2),872(a,1,2,2,1)),demod(504(6),540(5),540(9))].

given #229 (T,wt=-981): 880 f(f(f(x,f(x,x)),y),f(z,f(f(y,u),f(y,v)))) = y # label(529A).  [para(574(a,2),876(a,1,1))].

given #230 (T,wt=-975): 799 f(f(x,y),f(f(f(f(y,x),f(x,y)),z),f(u,f(x,y)))) = f(u,f(x,y)) # label(558A).  [para(677(a,2),797(a,1,2,1,1))].

given #231 (A,wt=-227): 662 f(x,f(f(y,f(y,y)),f(f(x,f(x,z)),f(u,f(x,z))))) = f(x,z) # label(526).  [para(515(a,1),633(a,1,2,2,1,2)),demod(540(3),629(4))].

given #232 (F,wt=-975): 854 f(f(f(f(x,f(x,x)),y),z),u) = f(u,f(f(y,v),f(u,f(z,f(y,y))))) # label(732A).  [para(750(a,1),852(a,1,2,2)),demod(581(7)),flip(a)].

given #233 (F,wt=-975): 879 f(f(f(x,y),f(x,z)),f(f(x,y),f(x,z))) = f(f(f(x,y),f(x,z)),x) # label(544D).  [para(876(a,1),543(a,1,2)),flip(a)].

given #234 (T,wt=-975): 884 f(f(f(x,y),f(z,y)),f(f(z,u),f(z,v))) = f(y,f(f(z,u),f(z,v))) # label(870B).  [para(876(a,1),866(a,1,1,2,1))].

given #235 (T,wt=-975): 885 f(f(f(x,y),f(z,y)),f(f(x,u),f(x,v))) = f(y,f(f(x,u),f(x,v))) # label(835).  [para(876(a,1),867(a,1,1,1,1))].

given #236 (A,wt=-973): 665 f(f(f(x,y),f(x,y)),f(x,f(f(x,y),z))) = f(f(x,y),f(f(x,y),f(x,y))) # label(637A).  [para(540(a,1),664(a,1,2,1))].

given #237 (F,wt=-975): 896 f(f(f(x,y),f(x,z)),f(f(x,u),f(v,u))) = f(u,f(f(x,y),f(x,z))) # label(917A).  [para(885(a,1),680(a,1)),flip(a)].

============================== PROOF =================================

% Proof 5 at 4.82 (+ 0.05) seconds: assoc.
% Length of proof is 164.
% Level of proof is 59.
% Maximum clause weight is 0.
% Given clauses 237.

6 f(c11,f(f(c10,c9),f(c10,c9))) != f(c9,f(f(c10,c11),f(c10,c11))) # answer(assoc).  [clausify].
494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].
499 f(c9,f(f(c10,c11),f(c10,c11))) != f(c11,f(f(c10,c9),f(c10,c9))) # answer(assoc).  [copy(6),flip(a)].
501 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z) # label(499).  [para(494(a,1),494(a,1,2,2,2))].
502 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y # label(500).  [para(494(a,1),501(a,1,1,2)),demod(494(12),494(12),494(14),494(17),494(30))].
503 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A).  [para(494(a,1),502(a,1,2,2))].
504 f(f(x,y),f(y,y)) = y # label(508B).  [para(494(a,1),503(a,1,2,1))].
505 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,y)),f(y,y)),y),f(y,z)))) = y # label(503).  [para(504(a,1),494(a,1,2,1))].
506 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(504).  [para(504(a,1),494(a,1,2,2,1,1,1,1))].
507 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(583A).  [para(504(a,1),494(a,1,2,2,1,1,1))].
508 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(506).  [para(504(a,1),501(a,1,2,2,1,1,1,1))].
509 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(504(a,1),501(a,1,2,2,1,1,1))].
510 f(f(x,f(y,y)),y) = f(y,y) # label(508).  [para(504(a,1),501(a,1,2,2,1)),demod(504(5),504(5))].
512 f(f(f(x,x),y),x) = f(x,x) # label(510B).  [para(503(a,1),504(a,1,1)),demod(503(7)),flip(a)].
513 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511).  [back_demod(505),demod(510(7))].
514 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512).  [para(512(a,1),494(a,1,2,2,1,1))].
515 f(f(x,y),f(x,x)) = x # label(513).  [para(504(a,1),512(a,1,1,1)),demod(504(6))].
516 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(514).  [para(515(a,1),494(a,1,2,2,1,1))].
517 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515).  [para(494(a,1),515(a,1,1))].
518 f(x,f(f(x,y),f(x,y))) = f(x,y) # label(516).  [para(515(a,1),515(a,1,1))].
519 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y # label(517).  [para(517(a,1),494(a,1,2,2,2))].
520 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = x # label(518).  [para(494(a,1),517(a,1,2,1)),demod(494(20),494(22))].
521 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y))) = f(y,z) # label(528).  [para(515(a,1),507(a,1,2,2,2))].
522 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A).  [para(513(a,1),512(a,1)),flip(a)].
523 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520).  [para(517(a,1),514(a,1,2,2,2))].
524 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B).  [para(522(a,1),504(a,1,1)),demod(522(9)),flip(a)].
525 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(533).  [para(515(a,1),508(a,1,2,2,1,1))].
526 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522).  [para(494(a,1),524(a,1,2,2))].
527 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523).  [para(504(a,1),524(a,1,2,1)),demod(515(8))].
528 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524).  [para(515(a,1),524(a,1,2,2))].
529 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525).  [para(517(a,1),527(a,1,2,2))].
530 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526).  [para(504(a,1),523(a,1,1)),demod(515(3),515(5))].
531 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x) # label(527).  [para(530(a,1),517(a,1,2,1)),demod(530(18),515(11),530(18))].
535 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E).  [para(516(a,1),509(a,1,2,2,1)),demod(515(3),517(6),504(6),515(10),517(13),504(13),515(16),517(19),504(19),504(27),527(27),510(23),515(9),515(3),517(6),504(6)),flip(a)].
536 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F).  [para(504(a,1),535(a,1,1,1)),demod(515(6))].
537 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536).  [para(517(a,1),535(a,1,2,2))].
538 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(537).  [para(494(a,1),536(a,1,2,2))].
539 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(538).  [para(515(a,1),536(a,1,2,2))].
540 f(f(x,x),f(x,y)) = x # label(525).  [para(524(a,1),521(a,1,1)),demod(536(16),515(13),510(11),515(3)),flip(a)].
542 f(x,f(f(x,x),y)) = f(x,x) # label(541E).  [para(527(a,1),521(a,1,1)),demod(540(10),540(12),535(14),504(10)),flip(a)].
543 f(x,f(y,f(x,x))) = f(x,x) # label(542E).  [para(529(a,1),521(a,1,1)),demod(540(10),540(12),537(14),504(10)),flip(a)].
544 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E).  [para(526(a,1),521(a,1,1)),demod(538(26),540(23),510(18),540(7)),flip(a)].
545 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E).  [para(528(a,1),521(a,1,1)),demod(539(26),540(23),510(18),540(7)),flip(a)].
547 f(f(x,x),f(y,x)) = x # label(548).  [para(517(a,1),540(a,1,2))].
548 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y)))) = y # label(546).  [para(540(a,1),519(a,1,2,1))].
549 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(549).  [back_demod(525),demod(547(3))].
550 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(550).  [back_demod(506),demod(547(3))].
552 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u)))) = y # label(551).  [para(544(a,1),494(a,1,1)),demod(517(7))].
553 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552).  [para(517(a,1),548(a,1,2))].
554 f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x) # label(553).  [para(504(a,1),553(a,1,2,1,1,1)),demod(547(3))].
555 f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y) # label(554).  [para(515(a,1),553(a,1,2,1,1,1)),demod(540(3))].
556 f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y # label(555).  [para(517(a,1),553(a,1,2,1,1,1)),demod(544(4))].
557 f(f(x,y),f(f(f(f(x,y),f(z,y)),f(z,y)),y)) = y # label(556).  [para(517(a,1),556(a,1,2,1,1,2)),demod(517(8))].
558 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557).  [para(494(a,1),554(a,1,2,1,1,2)),demod(494(12))].
559 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558).  [para(510(a,1),554(a,1,2,1,1,2)),demod(540(4),510(4))].
560 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559).  [para(515(a,1),554(a,1,2,1,1,2)),demod(515(4))].
561 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y) # label(560).  [para(545(a,1),558(a,1,2,2)),demod(545(9))].
562 f(f(x,x),x) = f(x,f(x,x)) # label(561).  [para(512(a,1),560(a,1,2,1)),demod(540(5))].
563 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562).  [back_demod(561),demod(562(2))].
564 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563).  [para(504(a,1),563(a,1,2,1,2)),demod(562(3))].
565 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(564).  [para(545(a,1),550(a,1,2,1))].
566 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)) # label(565).  [para(512(a,1),565(a,1,2,2,1,1)),demod(540(7))].
567 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(z,f(y,x))))) = f(y,x) # label(566).  [para(517(a,1),565(a,1,2,2,2))].
568 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)) # label(567D).  [para(531(a,1),566(a,1,2,2,2)),demod(515(17),531(14),544(7)),flip(a)].
569 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568).  [para(563(a,1),566(a,1,2,2))].
570 f(f(f(x,y),f(x,y)),f(f(f(x,y),f(f(x,y),f(x,y))),x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(567B).  [para(515(a,1),569(a,1,2,2))].
571 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C).  [para(568(a,1),559(a,1,2,1)),demod(543(14),540(11)),flip(a)].
574 f(f(x,f(x,x)),y) = f(y,y) # label(573).  [para(571(a,1),512(a,1,1))].
576 f(f(x,x),f(y,f(y,y))) = x # label(594).  [para(571(a,1),540(a,1,2))].
577 f(x,f(y,f(y,y))) = f(x,x) # label(575).  [para(571(a,1),542(a,1,2))].
578 f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(y,f(y,y)) # label(576).  [para(571(a,1),564(a,1,2,2)),demod(571(14))].
579 f(x,f(x,x)) = f(y,f(y,y)) # label(577).  [para(571(a,1),569(a,1,2,2)),demod(578(7))].
581 f(f(x,y),f(f(z,f(z,z)),y)) = y # label(579).  [para(574(a,2),504(a,1,2))].
583 f(x,f(f(y,f(y,y)),f(z,x))) = f(z,x) # label(581).  [para(574(a,2),517(a,1,2))].
586 f(x,f(f(y,f(y,y)),f(x,z))) = f(x,z) # label(582).  [para(574(a,2),518(a,1,2))].
587 f(f(f(x,f(x,x)),f(y,z)),z) = f(y,z) # label(586).  [para(574(a,1),509(a,1,2,1,2)),demod(571(13),571(14),586(13))].
589 f(f(x,y),f(f(f(y,y),z),f(f(u,f(u,u)),f(f(f(f(y,x),z),z),y)))) = y # label(585).  [para(574(a,2),519(a,1,2,2))].
590 f(f(f(x,f(x,x)),y),f(y,z)) = y # label(583).  [para(574(a,2),540(a,1,1))].
592 f(x,f(f(y,f(y,y)),z)) = f(x,f(z,z)) # label(589B).  [para(574(a,2),559(a,2,2)),demod(583(7)),flip(a)].
593 f(f(x,x),f(f(x,y),f(x,y))) = f(x,f(x,x)) # label(590).  [para(574(a,1),569(a,1,2))].
599 f(f(x,y),f(f(y,x),y)) = y # label(597).  [para(577(a,1),553(a,1,2,1,1)),demod(576(7))].
600 f(x,f(x,f(y,x))) = f(y,x) # label(598).  [para(577(a,1),554(a,1,2,1,1)),demod(576(7))].
601 f(x,f(x,f(x,y))) = f(x,y) # label(599).  [para(577(a,1),555(a,1,2,1,1)),demod(576(7))].
603 f(x,f(f(y,x),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x) # label(601).  [para(577(a,1),550(a,1,2,2,1,1,1)),demod(576(6),576(5))].
608 f(f(x,f(y,f(y,y))),f(z,f(z,z))) = x # label(613).  [para(577(a,2),576(a,1,1))].
609 f(f(x,y),f(f(z,f(z,z)),f(f(f(f(f(y,x),y),y),y),f(u,y)))) = y # label(606).  [para(579(a,1),519(a,1,2,1)),demod(540(7),540(8))].
610 f(f(f(x,f(x,x)),f(f(f(f(f(y,z),y),y),y),f(y,u))),f(y,y)) = y # label(607).  [para(579(a,1),520(a,1,1,1)),demod(540(6),540(7))].
618 f(f(f(x,y),f(x,y)),f(x,x)) = f(f(x,y),f(f(x,y),f(x,y))) # label(637).  [para(574(a,1),570(a,1,2))].
624 f(f(x,y),f(f(f(x,f(x,y)),x),f(x,f(x,y)))) = f(x,f(x,y)) # label(616).  [para(601(a,1),599(a,1,1))].
628 f(f(f(x,y),x),f(x,y)) = x # label(620).  [para(590(a,1),549(a,1,2,1,1,1)),demod(590(6),593(6),590(9),583(9),590(9))].
629 f(f(x,y),x) = f(x,f(x,y)) # label(623).  [back_demod(624),demod(628(7))].
632 f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,y)) = y # label(626).  [back_demod(610),demod(629(4),629(5),601(5),629(4))].
633 f(f(x,y),f(f(z,f(z,z)),f(f(y,f(y,x)),f(u,y)))) = y # label(627).  [back_demod(609),demod(629(5),629(6),601(6),629(5))].
634 f(f(x,y),y) = f(y,f(x,y)) # label(628B).  [para(494(a,1),629(a,1,1)),demod(494(14)),flip(a)].
635 f(f(x,y),f(y,f(x,y))) = y # label(629).  [para(629(a,1),557(a,1,2,1,1)),demod(634(2),634(5),629(8),600(8),629(5),600(5),634(4))].
636 f(f(x,y),f(f(f(y,y),x),f(f(y,f(x,y)),f(y,z)))) = y # label(630).  [para(629(a,1),552(a,1,2,2,1,1,1)),demod(629(6),601(6),634(5))].
638 f(f(x,y),f(f(f(y,y),z),f(f(u,f(u,u)),f(f(z,f(f(y,x),z)),y)))) = y # label(632).  [back_demod(589),demod(634(8))].
639 f(x,f(f(y,x),f(f(f(y,f(x,y)),f(y,x)),f(z,f(y,x))))) = f(y,x) # label(633).  [back_demod(567),demod(634(3))].
648 f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z)))) = x # label(640).  [para(635(a,1),603(a,1,2,1)),demod(635(8),629(5),600(5),635(7),635(11))].
655 f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z)) = z # label(644).  [para(600(a,1),632(a,1,1,2,1))].
657 f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z)) = z # label(646).  [para(517(a,1),655(a,1,1,2,2))].
660 f(f(f(x,y),f(z,y)),y) = f(f(u,f(u,u)),f(f(x,y),f(z,y))) # label(649).  [para(657(a,1),540(a,1,2)),demod(581(13))].
663 f(f(x,f(x,y)),f(y,x)) = x # label(652A).  [para(633(a,1),583(a,1)),flip(a)].
664 f(f(x,x),f(f(y,x),f(x,z))) = f(x,f(x,x)) # label(658).  [para(655(a,1),618(a,1,1,1)),demod(655(8),581(14),655(13),655(13),655(13))].
667 f(f(x,x),f(f(y,x),f(z,f(z,z)))) = f(x,f(x,x)) # label(660).  [para(579(a,1),664(a,1,2,2))].
670 f(f(f(x,y),f(z,y)),y) = f(y,f(f(x,y),f(z,y))) # label(664B).  [para(660(a,1),517(a,1,2,1)),demod(590(11)),flip(a)].
672 f(f(x,y),f(y,f(f(z,y),f(x,y)))) = f(f(z,y),f(x,y)) # label(666).  [para(660(a,2),583(a,1,2)),demod(670(5))].
673 f(x,f(f(x,y),f(f(z,f(x,y)),x))) = f(f(z,f(x,y)),x) # label(669).  [para(540(a,1),672(a,1,1)),demod(540(6),540(11))].
674 f(f(x,y),f(x,f(f(z,x),f(x,y)))) = f(f(z,x),f(x,y)) # label(667).  [para(545(a,1),672(a,1,1)),demod(545(6),545(11))].
675 f(f(x,y),f(y,f(f(y,z),f(x,y)))) = f(f(y,z),f(x,y)) # label(668).  [para(545(a,1),672(a,1,2,2,1)),demod(545(10))].
676 f(x,f(f(x,y),f(y,x))) = f(y,x) # label(670).  [para(547(a,1),673(a,1,2,2,1)),demod(547(7))].
677 f(f(x,y),f(y,x)) = f(f(y,x),f(y,x)) # label(671A).  [para(676(a,1),675(a,1,2)),flip(a)].
678 f(f(x,f(y,z)),f(f(z,y),f(y,z))) = f(y,z) # label(672).  [para(677(a,2),504(a,1,2))].
679 f(f(x,f(y,x)),f(x,y)) = x # label(673).  [para(677(a,1),648(a,1,2,2)),demod(518(6))].
680 f(x,y) = f(y,x) # label(933C).  [para(677(a,1),677(a,1,1)),demod(540(7),678(8))].
682 f(x,f(f(y,x),f(y,f(z,f(y,x))))) = f(y,x) # label(676).  [back_demod(639),demod(679(5))].
692 f(f(f(x,f(x,x)),y),z) = f(z,f(y,y)) # label(679).  [para(680(a,1),592(a,1))].
703 f(f(x,f(y,z)),f(f(y,z),f(z,y))) = f(z,y) # label(686).  [para(680(a,1),678(a,1,1,2))].
706 f(x,f(f(y,z),f(z,x))) = f(z,x) # label(689).  [para(674(a,1),682(a,1,2))].
713 f(f(x,y),f(f(z,f(y,f(y,x))),y)) = y # label(695).  [para(663(a,1),706(a,1,2,2)),demod(663(10))].
714 f(x,f(f(y,z),f(x,z))) = f(z,x) # label(696).  [para(680(a,1),706(a,1,2,2))].
715 f(x,f(f(y,x),f(z,y))) = f(y,x) # label(697).  [para(680(a,1),706(a,1,2))].
721 f(f(x,y),z) = f(z,f(y,f(z,f(x,y)))) # label(703A).  [para(547(a,1),714(a,1,2,1)),flip(a)].
722 f(f(f(x,y),f(z,y)),z) = f(y,z) # label(704A).  [para(714(a,1),680(a,1)),flip(a)].
723 f(x,f(f(x,y),f(z,y))) = f(y,x) # label(705).  [para(680(a,1),714(a,1,2))].
725 f(x,f(f(f(y,z),x),z)) = f(f(y,z),x) # label(708).  [para(547(a,1),715(a,1,2,2))].
741 f(f(f(x,y),f(z,y)),x) = f(y,x) # label(725).  [para(680(a,1),722(a,1,1))].
743 f(x,f(f(x,f(y,z)),z)) = f(f(y,z),x) # label(726).  [para(547(a,1),723(a,1,2,2))].
744 f(f(f(x,f(y,z)),z),x) = f(f(y,z),x) # label(728).  [para(547(a,1),741(a,1,1,2))].
749 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)) # label(731).  [para(721(a,1),680(a,1))].
750 f(f(f(f(x,f(x,x)),y),z),u) = f(u,f(z,f(y,y))) # label(732).  [para(692(a,2),721(a,1,1)),demod(749(11))].
758 f(f(x,f(y,f(z,x))),y) = f(y,f(z,x)) # label(736A).  [para(749(a,1),680(a,1)),flip(a)].
765 f(f(f(x,y),f(y,x)),f(z,f(x,y))) = f(y,x) # label(740A).  [para(703(a,1),680(a,1)),flip(a)].
768 f(x,f(f(f(y,z),x),f(u,f(z,y)))) = f(f(y,z),x) # label(743).  [para(765(a,1),725(a,1,2,1,1)),demod(765(12))].
771 f(f(x,y),f(f(z,f(f(y,x),z)),y)) = y # label(759).  [para(638(a,1),749(a,1,2,2)),demod(587(9),638(18))].
772 f(f(f(x,f(f(y,z),x)),y),f(z,y)) = y # label(760).  [para(638(a,1),758(a,1,1,2)),demod(587(8),638(18))].
773 f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z) # label(761).  [para(515(a,1),771(a,1,2,1,2,1)),demod(540(3))].
777 f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),y)) = y # label(763).  [para(771(a,1),714(a,1,2,2)),demod(772(14))].
780 f(f(x,x),f(f(y,x),f(f(x,x),z))) = f(f(x,x),z) # label(765).  [para(667(a,1),773(a,1,2,1,2)),demod(608(8))].
791 f(x,f(f(y,f(y,y)),f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,x) # label(748).  [para(750(a,2),655(a,1)),demod(504(5))].
793 f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z) # label(772).  [para(504(a,1),780(a,1,1)),demod(540(5),540(8))].
795 f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y) # label(774).  [para(680(a,1),780(a,1,2))].
796 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z) # label(775).  [para(680(a,1),793(a,1,2,1))].
797 f(x,f(f(f(x,x),y),f(z,x))) = f(z,x) # label(776).  [para(600(a,1),796(a,1,2,2)),demod(600(8))].
800 f(f(f(f(x,x),y),f(z,x)),x) = f(z,x) # label(779A).  [para(797(a,1),680(a,1)),flip(a)].
804 f(f(x,y),f(f(f(y,y),z),f(f(y,f(x,y)),f(y,u)))) = y # label(781).  [para(800(a,1),636(a,1,1)),demod(795(7),800(8))].
818 f(f(x,x),f(f(f(x,x),y),f(f(z,f(z,z)),f(x,u)))) = x # label(783).  [para(579(a,1),804(a,1,2,2,1))].
830 f(f(x,f(f(y,f(y,y)),f(z,u))),f(z,z)) = z # label(789A).  [para(818(a,1),743(a,1)),flip(a)].
833 f(f(x,f(y,y)),f(f(z,y),f(z,y))) = f(z,y) # label(791).  [para(713(a,1),830(a,1,1,2)),demod(547(6),547(7),547(10))].
837 f(f(f(x,y),f(x,y)),f(z,f(y,y))) = f(x,y) # label(794A).  [para(833(a,1),680(a,1)),flip(a)].
839 f(x,f(f(f(f(y,y),z),x),f(u,y))) = f(f(f(y,y),z),x) # label(796).  [para(837(a,1),768(a,1,2,2))].
852 f(x,f(f(f(y,y),z),f(f(y,u),x))) = f(f(y,u),x) # label(817).  [para(839(a,1),768(a,1,2))].
855 f(f(x,f(f(y,f(f(z,f(x,x)),y)),z)),z) = f(z,z) # label(822A).  [para(777(a,1),852(a,1,2)),flip(a)].
856 f(f(f(x,f(f(y,f(z,z)),x)),y),z) = f(z,f(y,y)) # label(823A).  [para(855(a,1),743(a,1,2)),flip(a)].
858 f(x,f(f(y,f(z,f(x,x))),f(y,f(z,f(x,x))))) = f(y,x) # label(826B).  [para(744(a,1),856(a,1,1,1,2)),demod(679(8)),flip(a)].
866 f(f(f(x,y),f(f(z,f(u,u)),y)),u) = f(y,u) # label(829B).  [para(722(a,1),858(a,1,2,1)),demod(722(11),858(8)),flip(a)].
867 f(f(f(f(x,f(y,y)),z),f(u,z)),y) = f(z,y) # label(830B).  [para(741(a,1),858(a,1,2,1)),demod(741(11),858(8)),flip(a)].
872 f(x,f(y,f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,x) # label(797).  [para(791(a,1),837(a,1,1,1)),demod(791(10),540(3),581(17),791(16))].
876 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x # label(808).  [para(750(a,2),872(a,1,2,2,1)),demod(504(6),540(5),540(9))].
884 f(f(f(x,y),f(z,y)),f(f(z,u),f(z,v))) = f(y,f(f(z,u),f(z,v))) # label(870B).  [para(876(a,1),866(a,1,1,2,1))].
885 f(f(f(x,y),f(z,y)),f(f(x,u),f(x,v))) = f(y,f(f(x,u),f(x,v))) # label(835).  [para(876(a,1),867(a,1,1,1,1))].
896 f(f(f(x,y),f(x,z)),f(f(x,u),f(v,u))) = f(u,f(f(x,y),f(x,z))) # label(917A).  [para(885(a,1),680(a,1)),flip(a)].
898 f(x,f(f(y,z),f(y,z))) = f(z,f(f(y,x),f(y,x))) # label(872).  [para(896(a,1),884(a,1))].
899 $F # answer(assoc).  [resolve(898,a,499,a)].

============================== end of proof ==========================

NOTE: Disabling denial clause 499.

given #238 (F,wt=-981): 898 f(x,f(f(y,z),f(y,z))) = f(z,f(f(y,x),f(y,x))) # label(872).  [para(896(a,1),884(a,1))].

given #239 (T,wt=-981): 901 f(f(f(x,y),f(x,y)),z) = f(y,f(f(x,z),f(x,z))) # label(870).  [para(898(a,1),680(a,1)),flip(a)].

given #240 (T,wt=-975): 897 f(f(f(x,y),f(x,z)),f(f(x,u),f(v,u))) = f(f(f(x,y),f(x,z)),u) # label(918).  [para(896(a,2),680(a,1))].

given #241 (A,wt=-483): 666 f(f(x,x),f(f(x,y),f(x,z))) = f(x,f(x,x)) # label(590).  [para(545(a,1),664(a,1,2,1))].

given #242 (F,wt=-975): 905 f(f(f(x,y),f(x,z)),f(f(u,v),f(x,v))) = f(f(f(x,y),f(x,z)),v) # label(851).  [para(680(a,1),897(a,1,2))].

given #243 (F,wt=-973): 819 f(f(x,f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(x,f(f(x,y),u)))) = f(x,y) # label(531A).  [para(630(a,1),804(a,1,2,2,1))].

given #244 (T,wt=-979): 907 f(f(f(x,y),y),f(f(f(y,y),z),f(f(x,y),f(y,u)))) = y # label(532A).  [para(504(a,1),819(a,1,1,2)),demod(504(5),504(5),504(8),504(12))].

given #245 (T,wt=-971): 845 f(f(x,x),f(f(y,f(y,y)),f(f(x,f(z,x)),f(z,z)))) = f(f(x,f(z,x)),f(z,z)) # label(801).  [para(844(a,1),582(a,1,1))].

given #246 (A,wt=-227): 668 f(x,f(f(y,f(y,y)),f(f(x,f(z,f(z,z))),u))) = f(z,f(z,z)) # label(565A).  [para(579(a,1),650(a,1,2,1))].

given #247 (F,wt=-969): 712 f(f(f(x,f(x,x)),y),f(f(z,u),f(u,f(f(v,f(v,v)),y)))) = f(u,f(f(x,f(x,x)),y)) # label(527A).  [para(641(a,1),706(a,1,2,2))].

given #248 (F,wt=-969): 878 f(x,f(f(y,f(f(x,z),f(x,u))),f(y,f(f(x,z),f(x,u))))) = f(y,f(f(x,z),f(x,u))) # label(521A).  [para(876(a,1),504(a,1,1))].

given #249 (T,wt=-969): 906 f(f(f(x,y),f(x,z)),f(f(u,f(f(v,w),f(v,w))),f(x,w))) = f(f(f(x,y),f(x,z)),w) # label(543C).  [para(901(a,1),905(a,1,2,1))].

given #250 (T,wt=-959): 859 f(f(f(f(f(x,x),f(f(x,x),y)),f(x,x)),f(z,f(f(x,x),y))),x) = f(x,f(f(z,f(f(x,x),y)),f(z,f(f(x,x),y)))) # label(824A).  [para(756(a,1),856(a,1,1,1,2))].

given #251 (A,wt=-102): 671 f(x,f(f(y,f(y,y)),f(f(z,f(x,x)),f(u,f(x,x))))) = f(x,x) # label(526).  [para(660(a,1),543(a,1,2))].

given #252 (F,wt=-977): 924 f(x,f(f(f(y,y),y),f(f(z,f(x,x)),f(u,f(x,x))))) = f(x,x) # label(526A).  [para(504(a,1),671(a,1,2,1,2))].

given #253 (F,wt=-967): 923 f(f(f(f(x,x),y),f(z,f(f(x,x),y))),x) = f(x,f(f(z,f(f(x,x),y)),f(z,f(f(x,x),y)))) # label(824).  [para(680(a,1),859(a,1,1,1)),demod(601(6))].

given #254 (T,wt=-981): 928 f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x) = f(z,x) # label(827).  [para(788(a,1),923(a,1,1,2)),demod(788(15),788(18),858(15))].

given #255 (T,wt=-981): 933 f(f(f(f(x,x),y),f(z,f(f(x,x),y))),x) = f(z,x) # label(828C).  [back_demod(923),demod(930(15))].

given #256 (A,wt=-489): 684 f(f(x,x),x) = f(y,f(y,y)) # label(561).  [para(680(a,1),579(a,1))].

given #257 (F,wt=-983): 934 f(f(f(x,y),f(x,f(f(z,z),u))),z) = f(x,z) # label(836B).  [para(719(a,1),933(a,1,1,2)),demod(933(7)),flip(a)].

given #258 (F,wt=-983): 939 f(x,f(f(y,z),f(y,f(f(x,x),u)))) = f(y,x) # label(838A).  [para(934(a,1),680(a,1)),flip(a)].

given #259 (T,wt=-983): 940 f(x,f(f(y,f(f(x,x),z)),f(y,u))) = f(y,x) # label(839).  [para(934(a,1),788(a,1,1,2)),demod(884(9),939(12))].

given #260 (T,wt=-983): 941 f(x,f(f(y,z),f(z,f(f(x,x),u)))) = f(z,x) # label(530).  [para(600(a,1),939(a,1,2,1))].

given #261 (A,wt=-489): 686 f(f(x,y),f(f(x,y),x)) = x # label(629E).  [para(680(a,1),630(a,1,2))].

given #262 (F,wt=-985): 950 f(f(x,f(y,f(x,z))),f(f(x,z),x)) = x # label(624A).  [para(686(a,1),741(a,2)),demod(759(4))].

given #263 (F,wt=-981): 938 f(f(f(x,y),f(x,f(z,u))),f(z,z)) = f(x,f(z,z)) # label(837).  [para(504(a,1),934(a,1,1,2,2,1))].

given #264 (T,wt=-983): 952 f(f(f(x,y),f(x,f(f(x,z),u))),z) = f(z,x) # label(921).  [para(714(a,1),938(a,2)),demod(897(9))].

given #265 (T,wt=-981): 947 f(f(x,x),f(f(y,f(z,x)),f(y,u))) = f(y,f(x,x)) # label(846).  [para(833(a,1),940(a,1,2,1,2))].

given #266 (A,wt=-489): 687 f(f(x,y),f(f(y,x),y)) = y # label(597).  [para(680(a,1),631(a,1,2))].

given #267 (F,wt=-981): 948 f(f(x,x),f(f(y,z),f(z,f(u,x)))) = f(z,f(x,x)) # label(848).  [para(833(a,1),941(a,1,2,2,2))].

given #268 (F,wt=-981): 955 f(f(x,x),f(f(y,z),f(z,f(u,x)))) = f(f(x,x),z) # label(850).  [para(948(a,2),680(a,1))].

given #269 (T,wt=-979): 956 f(f(x,x),f(f(y,f(y,y)),f(f(z,x),u))) = f(f(x,x),u) # label(852).  [para(699(a,2),955(a,1,2))].

given #270 (T,wt=-983): 960 f(f(x,f(y,x)),f(y,y)) = f(f(x,x),f(y,y)) # label(855A).  [para(845(a,1),956(a,2)),demod(956(14),958(9)),flip(a)].

given #271 (A,wt=-485): 688 f(x,f(f(f(y,y),y),f(z,x))) = f(z,x) # label(557).  [para(680(a,1),583(a,1,2,1))].

given #272 (F,wt=-981): 961 f(f(x,f(f(f(y,f(y,y)),z),x)),z) = f(f(x,x),z) # label(856).  [para(581(a,1),960(a,1,2)),demod(581(14))].

given #273 (F,wt=-979): 958 f(f(x,x),f(f(y,f(y,y)),f(f(x,z),u))) = f(f(x,x),u) # label(853).  [para(680(a,1),956(a,1,2,2,1))].

given #274 (T,wt=-979): 959 f(f(x,x),f(y,f(f(z,x),f(y,u)))) = f(f(x,x),f(y,u)) # label(854B).  [para(869(a,1),956(a,1,2,2)),demod(956(8)),flip(a)].

given #275 (T,wt=-977): 935 f(x,f(f(y,f(y,y)),f(f(f(z,z),z),f(u,f(x,x))))) = f(x,x) # label(526B).  [para(684(a,2),661(a,1,2,2,1))].

given #276 (A,wt=-489): 696 f(f(f(x,y),x),f(y,x)) = x # label(617).  [para(680(a,1),663(a,1,1))].

given #277 (F,wt=-985): 969 f(f(x,x),y) = f(y,f(f(f(z,z),z),x)) # label(560A).  [para(935(a,1),792(a,1,1)),demod(942(14))].

given #278 (F,wt=-983): 971 f(f(x,y),f(f(f(f(y,x),f(y,x)),z),y)) = y # label(597A).  [para(696(a,1),852(a,1,2,2)),demod(696(11))].

given #279 (T,wt=-975): 962 f(f(x,f(x,y)),f(y,f(f(y,x),z))) = f(f(x,x),f(y,f(f(y,x),z))) # label(922).  [para(952(a,1),961(a,1,1,2))].

given #280 (T,wt=-979): 973 f(x,f(f(y,y),f(x,f(f(x,y),z)))) = f(x,f(f(x,y),z)) # label(924).  [para(962(a,1),781(a,1,2))].

given #281 (A,wt=-100): 701 f(f(f(x,f(x,x)),y),f(f(z,f(z,z)),f(u,f(y,y)))) = f(u,f(y,y)) # label(570A).  [para(692(a,2),587(a,1))].

given #282 (F,wt=-981): 976 f(x,f(f(y,y),f(x,z))) = f(x,f(f(x,y),f(x,z))) # label(926).  [para(959(a,1),973(a,1,2))].

given #283 (F,wt=-981): 977 f(f(f(x,y),f(x,z)),x) = f(x,f(f(y,y),f(x,z))) # label(928A).  [para(976(a,2),680(a,1)),flip(a)].

given #284 (T,wt=-981): 978 f(x,f(f(x,y),f(z,z))) = f(x,f(f(x,z),f(x,y))) # label(929).  [para(680(a,1),976(a,1,2))].

given #285 (T,wt=-981): 979 f(x,f(f(x,y),f(x,f(z,z)))) = f(x,f(f(x,y),z)) # label(930B).  [para(792(a,1),978(a,2,2)),demod(581(8)),flip(a)].

given #286 (A,wt=-233): 704 f(f(x,f(y,z)),f(f(z,y),f(z,y))) = f(y,z) # label(508B).  [para(680(a,1),678(a,1,2,2))].

given #287 (F,wt=-981): 980 f(f(f(x,y),z),x) = f(x,f(f(y,y),f(x,f(z,z)))) # label(931).  [para(979(a,1),691(a,1,1,2)),demod(691(7),977(8))].

given #288 (F,wt=-981): 981 f(f(x,f(y,f(z,z))),y) = f(y,f(z,f(y,f(x,x)))) # label(932).  [para(792(a,1),980(a,1,1)),demod(581(11))].

============================== PROOF =================================

% Proof 6 at 8.07 (+ 0.07) seconds: mod.
% Length of proof is 214.
% Level of proof is 76.
% Maximum clause weight is 0.
% Given clauses 288.

494 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(y,u)))) = y # label(492).  [input].
500 f(c12,f(c14,f(c12,f(c13,c13)))) != f(c12,f(c13,f(c12,f(c14,c14)))) # answer(mod).  [clausify].
501 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z))) = f(y,z) # label(499).  [para(494(a,1),494(a,1,2,2,2))].
502 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))))) = y # label(500).  [para(494(a,1),501(a,1,1,2)),demod(494(12),494(12),494(14),494(17),494(30))].
503 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A).  [para(494(a,1),502(a,1,2,2))].
504 f(f(x,y),f(y,y)) = y # label(508B).  [para(494(a,1),503(a,1,2,1))].
505 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,y)),f(y,y)),y),f(y,z)))) = y # label(503).  [para(504(a,1),494(a,1,2,1))].
506 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(504).  [para(504(a,1),494(a,1,2,2,1,1,1,1))].
507 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z)))) = y # label(583A).  [para(504(a,1),494(a,1,2,2,1,1,1))].
508 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x))) = f(y,x) # label(506).  [para(504(a,1),501(a,1,2,2,1,1,1,1))].
509 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z))) = f(y,z) # label(586A).  [para(504(a,1),501(a,1,2,2,1,1,1))].
510 f(f(x,f(y,y)),y) = f(y,y) # label(508).  [para(504(a,1),501(a,1,2,2,1)),demod(504(5),504(5))].
512 f(f(f(x,x),y),x) = f(x,x) # label(510B).  [para(503(a,1),504(a,1,1)),demod(503(7)),flip(a)].
513 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511).  [back_demod(505),demod(510(7))].
514 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512).  [para(512(a,1),494(a,1,2,2,1,1))].
515 f(f(x,y),f(x,x)) = x # label(513).  [para(504(a,1),512(a,1,1,1)),demod(504(6))].
516 f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z)))) = y # label(514).  [para(515(a,1),494(a,1,2,2,1,1))].
517 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515).  [para(494(a,1),515(a,1,1))].
518 f(x,f(f(x,y),f(x,y))) = f(x,y) # label(516).  [para(515(a,1),515(a,1,1))].
519 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y)))) = y # label(517).  [para(517(a,1),494(a,1,2,2,2))].
520 f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x)) = x # label(518).  [para(494(a,1),517(a,1,2,1)),demod(494(20),494(22))].
521 f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y))) = f(y,z) # label(528).  [para(515(a,1),507(a,1,2,2,2))].
522 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A).  [para(513(a,1),512(a,1)),flip(a)].
523 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520).  [para(517(a,1),514(a,1,2,2,2))].
524 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B).  [para(522(a,1),504(a,1,1)),demod(522(9)),flip(a)].
525 f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(533).  [para(515(a,1),508(a,1,2,2,1,1))].
526 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522).  [para(494(a,1),524(a,1,2,2))].
527 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523).  [para(504(a,1),524(a,1,2,1)),demod(515(8))].
528 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524).  [para(515(a,1),524(a,1,2,2))].
529 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525).  [para(517(a,1),527(a,1,2,2))].
530 f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))) = f(x,x) # label(526).  [para(504(a,1),523(a,1,1)),demod(515(3),515(5))].
531 f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x) = f(x,x) # label(527).  [para(530(a,1),517(a,1,2,1)),demod(530(18),515(11),530(18))].
535 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E).  [para(516(a,1),509(a,1,2,2,1)),demod(515(3),517(6),504(6),515(10),517(13),504(13),515(16),517(19),504(19),504(27),527(27),510(23),515(9),515(3),517(6),504(6)),flip(a)].
536 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F).  [para(504(a,1),535(a,1,1,1)),demod(515(6))].
537 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536).  [para(517(a,1),535(a,1,2,2))].
538 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(537).  [para(494(a,1),536(a,1,2,2))].
539 f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(538).  [para(515(a,1),536(a,1,2,2))].
540 f(f(x,x),f(x,y)) = x # label(525).  [para(524(a,1),521(a,1,1)),demod(536(16),515(13),510(11),515(3)),flip(a)].
542 f(x,f(f(x,x),y)) = f(x,x) # label(541E).  [para(527(a,1),521(a,1,1)),demod(540(10),540(12),535(14),504(10)),flip(a)].
543 f(x,f(y,f(x,x))) = f(x,x) # label(542E).  [para(529(a,1),521(a,1,1)),demod(540(10),540(12),537(14),504(10)),flip(a)].
544 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E).  [para(526(a,1),521(a,1,1)),demod(538(26),540(23),510(18),540(7)),flip(a)].
545 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E).  [para(528(a,1),521(a,1,1)),demod(539(26),540(23),510(18),540(7)),flip(a)].
547 f(f(x,x),f(y,x)) = x # label(548).  [para(517(a,1),540(a,1,2))].
548 f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y)))) = y # label(546).  [para(540(a,1),519(a,1,2,1))].
549 f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x))) = f(y,x) # label(549).  [back_demod(525),demod(547(3))].
550 f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u)))) = f(y,x) # label(550).  [back_demod(506),demod(547(3))].
552 f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u)))) = y # label(551).  [para(544(a,1),494(a,1,1)),demod(517(7))].
553 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552).  [para(517(a,1),548(a,1,2))].
554 f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x))) = f(y,x) # label(553).  [para(504(a,1),553(a,1,2,1,1,1)),demod(547(3))].
555 f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y))) = f(x,y) # label(554).  [para(515(a,1),553(a,1,2,1,1,1)),demod(540(3))].
556 f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y # label(555).  [para(517(a,1),553(a,1,2,1,1,1)),demod(544(4))].
557 f(f(x,y),f(f(f(f(x,y),f(z,y)),f(z,y)),y)) = y # label(556).  [para(517(a,1),556(a,1,2,1,1,2)),demod(517(8))].
558 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557).  [para(494(a,1),554(a,1,2,1,1,2)),demod(494(12))].
559 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558).  [para(510(a,1),554(a,1,2,1,1,2)),demod(540(4),510(4))].
560 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559).  [para(515(a,1),554(a,1,2,1,1,2)),demod(515(4))].
561 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y) # label(560).  [para(545(a,1),558(a,1,2,2)),demod(545(9))].
562 f(f(x,x),x) = f(x,f(x,x)) # label(561).  [para(512(a,1),560(a,1,2,1)),demod(540(5))].
563 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562).  [back_demod(561),demod(562(2))].
564 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563).  [para(504(a,1),563(a,1,2,1,2)),demod(562(3))].
565 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z)))) = f(y,x) # label(564).  [para(545(a,1),550(a,1,2,1))].
566 f(f(x,x),f(f(x,f(x,x)),f(x,f(f(x,f(x,x)),y)))) = f(x,f(x,x)) # label(565).  [para(512(a,1),565(a,1,2,2,1,1)),demod(540(7))].
567 f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(z,f(y,x))))) = f(y,x) # label(566).  [para(517(a,1),565(a,1,2,2,2))].
568 f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))) = f(x,f(x,x)) # label(567D).  [para(531(a,1),566(a,1,2,2,2)),demod(515(17),531(14),544(7)),flip(a)].
569 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568).  [para(563(a,1),566(a,1,2,2)