% This is a proof-checking job.  The search simply follows the
% hints.  Because max_weight=0, if a derived clause is not
% more general than some hint, it will be discarded.

assign(new_constants, 1).

clear(lex_dep_demod).

assign(max_weight, 0).  % Hope that everything matches a hint!

formulas(sos).
  f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x.  % MOL sax
end_of_list.

formulas(goals).
  f(y,x) = f(x,y)                               # answer(comm).
  f(y,f(y,y)) = f(x,f(x,x))                     # 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(z,f(f(y,x),f(y,x))) = f(x,f(f(y,z),f(y,z))) # answer(assoc).
  f(x,f(z,f(x,f(y,y)))) = f(x,f(y,f(x,f(z,z)))) # answer(mod).
end_of_list.

formulas(hints).
% Arguments: -x t8.out
% 487 hints were constructed from the clauses in 6 proofs.
% Length of xproof is 59.  (0.71 + 0.01 seconds) absorb.
% Length of xproof is 147.  (1.11 + 0.02 seconds) one.
% Length of xproof is 139.  (1.18 + 0.03 seconds) oml.
% Length of xproof is 213.  (1.94 + 0.04 seconds) comm.
% Length of xproof is 434.  (6.69 + 0.29 seconds) assoc.
% Length of xproof is 470.  (14.94 + 0.62 seconds) mod.
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),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(500C).
f(f(x,y),f(f(f(y,y),w),f(f(f(f(f(y,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(500D).
f(f(x,y),f(f(f(y,y),w),f(f(f(f(f(y,x),w),w),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)))) # 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(z,x),f(u,x))) = f(f(f(z,x),f(u,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(y,f(x,x)) = f(y,f(f(z,f(z,z)),x)) # 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(y,f(x,y)),f(f(f(f(x,y),f(f(x,y),y)),f(x,y)),y)) = y # label(629B).
f(f(y,f(x,y)),f(f(f(f(x,y),f(y,f(x,y))),f(x,y)),y)) = y # label(629C).
f(f(y,f(x,y)),f(f(f(x,y),f(f(x,y),f(y,f(x,y)))),y)) = y # label(629D).
f(f(y,f(x,y)),f(f(y,f(x,y)),y)) = y # label(629E).
f(f(y,f(x,y)),f(y,f(y,f(x,y)))) = y # label(629F).
f(f(y,f(x,y)),f(x,y)) = y # 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(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(658C).
f(f(x,x),f(f(z,x),f(x,u))) = f(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(658D).
f(f(x,x),f(f(z,x),f(x,u))) = f(x,f(x,f(f(f(y,f(y,y)),f(f(z,x),f(x,u))),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(z,u),f(u,z)) = f(f(y,f(y,y)),f(z,u)) # 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(u,f(f(y,x),u)),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(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(y,f(f(z,u),y)),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(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(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(797B).
f(x,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(797C).
f(x,f(v,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(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,u),f(f(f(x,x),f(x,x)),v)))) = f(f(x,x),f(x,x)) # label(808B).
f(f(x,x),f(y,f(f(x,u),f(x,v)))) = 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,z) = f(z,f(f(x,f(y,f(z,z))),f(x,f(y,f(z,z))))) # 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(z,x) = f(f(f(u,z),f(f(y,f(x,x)),z)),x) # 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(z,x) = f(f(f(z,u),f(z,f(f(x,x),y))),x) # 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(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(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(z,z)) = f(f(x,f(z,x)),f(z,z)) # 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(z,x) = f(f(f(f(y,f(x,x)),z),f(u,z)),x) # 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(u,v)) = f(f(x,x),f(u,f(f(z,x),f(u,v)))) # 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),u)) = f(x,f(f(x,y),f(x,f(u,u)))) # 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(y,z),u),y) = f(f(f(y,z),f(y,f(u,u))),y) # 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(z,f(y,f(u,u))),y) = f(f(u,f(y,f(z,z))),y) # label(933B).
f(y,f(u,f(y,f(z,z)))) = f(f(u,f(y,f(z,z))),y) # 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.