============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10728 was started by mccune on cleo.thornwood, Sat Aug 12 20:58:20 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). 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. 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). 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. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(y,x) = f(x,y) # answer(comm). [goal]. 2 f(y,f(y,y)) = f(x,f(x,x)) # answer(one). [goal]. 3 f(f(x,x),f(x,y)) = x # answer(absorb). [goal]. 4 f(x,f(x,f(x,y))) = f(x,y) # answer(oml). [goal]. 5 f(z,f(f(y,x),f(y,x))) = f(x,f(f(y,z),f(y,z))) # answer(assoc). [goal]. 6 f(x,f(z,f(x,f(y,y)))) = f(x,f(y,f(x,f(z,z)))) # answer(mod). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(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. [assumption]. f(c2,c1) != f(c1,c2) # answer(comm). [deny(1)]. f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one). [deny(2)]. f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb). [deny(3)]. f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml). [deny(4)]. f(c9,f(f(c10,c11),f(c10,c11))) != f(c11,f(f(c10,c9),f(c10,c9))) # answer(assoc). [deny(5)]. f(c12,f(c13,f(c12,f(c14,c14)))) != f(c12,f(c14,f(c12,f(c13,c13)))) # answer(mod). [deny(6)]. end_of_list. formulas(demodulators). end_of_list. % 486 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 6). % (Horn set with more than one neg. clause) 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: (no changes). 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: formulas(usable). end_of_list. formulas(sos). 7 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). [assumption]. 8 f(c2,c1) != f(c1,c2) # answer(comm). [deny(1)]. 9 f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one). [deny(2)]. 10 f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb). [deny(3)]. 11 f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml). [deny(4)]. 12 f(c9,f(f(c10,c11),f(c10,c11))) != f(c11,f(f(c10,c9),f(c10,c9))) # answer(assoc). [deny(5)]. 14 f(c12,f(c14,f(c12,f(c13,c13)))) != f(c12,f(c13,f(c12,f(c14,c14)))) # answer(mod). [copy(13),flip(a)]. end_of_list. formulas(demodulators). 7 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). [assumption]. end_of_list. % 486 hints processed (44 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.03 seconds. given #1 (I,wt=-975): 7 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). [assumption]. given #2 (I,wt=7): 8 f(c2,c1) != f(c1,c2) # answer(comm). [deny(1)]. given #3 (I,wt=11): 9 f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one). [deny(2)]. given #4 (I,wt=9): 10 f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb). [deny(3)]. given #5 (I,wt=11): 11 f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml). [deny(4)]. given #6 (I,wt=19): 12 f(c9,f(f(c10,c11),f(c10,c11))) != f(c11,f(f(c10,c9),f(c10,c9))) # answer(assoc). [deny(5)]. given #7 (I,wt=19): 14 f(c12,f(c14,f(c12,f(c13,c13)))) != f(c12,f(c13,f(c12,f(c14,c14)))) # answer(mod). [copy(13),flip(a)]. given #8 (F,wt=-965): 15 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(7(a,1),7(a,1,2,2,2))]. given #9 (T,wt=-959): 16 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(7(a,1),15(a,1,1,2)),rewrite(7(12),7(12),7(14),7(17),7(30))]. given #10 (T,wt=-987): 17 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A). [para(7(a,1),16(a,1,2,2))]. given #11 (A,wt=-991): 18 f(f(x,y),f(y,y)) = y # label(508B). [para(7(a,1),17(a,1,2,1))]. given #12 (F,wt=-989): 24 f(f(x,f(y,y)),y) = f(y,y) # label(508). [para(18(a,1),15(a,1,2,2,1)),rewrite(18(5),18(5))]. given #13 (F,wt=-989): 26 f(f(f(x,x),y),x) = f(x,x) # label(510B). [para(17(a,1),18(a,1,1)),rewrite(17(7)),flip(a)]. given #14 (T,wt=-991): 29 f(f(x,y),f(x,x)) = x # label(513). [para(18(a,1),26(a,1,1,1)),rewrite(18(6))]. given #15 (T,wt=-987): 31 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515). [para(7(a,1),29(a,1,1))]. given #16 (A,wt=-963): 20 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(18(a,1),7(a,1,2,2,1,1,1,1))]. given #17 (F,wt=-987): 32 f(x,f(f(x,y),f(x,y))) = f(x,y) # label(516). [para(29(a,1),29(a,1,1))]. given #18 (F,wt=-985): 27 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511). [back_rewrite(19),rewrite(24(7))]. given #19 (T,wt=-979): 28 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512). [para(26(a,1),7(a,1,2,2,1,1))]. given #20 (T,wt=-979): 35 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A). [para(27(a,1),26(a,1)),flip(a)]. given #21 (A,wt=-975): 21 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(18(a,1),7(a,1,2,2,1,1,1))]. given #22 (F,wt=-987): 37 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B). [para(35(a,1),18(a,1,1)),rewrite(35(9)),flip(a)]. given #23 (F,wt=-987): 40 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523). [para(18(a,1),37(a,1,2,1)),rewrite(29(8))]. given #24 (T,wt=-987): 42 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525). [para(31(a,1),40(a,1,2,2))]. given #25 (T,wt=-979): 36 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520). [para(31(a,1),28(a,1,2,2,2))]. given #26 (A,wt=-967): 22 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(18(a,1),15(a,1,2,2,1,1,1,1))]. given #27 (F,wt=-979): 39 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522). [para(7(a,1),37(a,1,2,2))]. given #28 (F,wt=-979): 41 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524). [para(29(a,1),37(a,1,2,2))]. given #29 (T,wt=-977): 43 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(18(a,1),36(a,1,1)),rewrite(29(3),29(5))]. given #30 (T,wt=-977): 45 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(43(a,1),31(a,1,2,1)),rewrite(43(18),29(11),43(18))]. given #31 (A,wt=-967): 23 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(18(a,1),15(a,1,2,2,1,1,1))]. given #32 (F,wt=-981): 46 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(529). [para(45(a,1),21(a,1,2,2,1)),rewrite(24(3),31(8))]. given #33 (F,wt=-981): 47 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x) # label(530). [para(18(a,1),46(a,1,1)),rewrite(29(4),29(5))]. given #34 (T,wt=-975): 33 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(31(a,1),7(a,1,2,2,2))]. given #35 (T,wt=-975): 34 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(7(a,1),31(a,1,2,1)),rewrite(7(20),7(22))]. given #36 (A,wt=-973): 30 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(29(a,1),7(a,1,2,2,1,1))]. given #37 (F,wt=-985): 52 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E). [para(30(a,1),23(a,1,2,2,1)),rewrite(29(3),31(6),18(6),47(7),29(4),31(7),18(7),29(10),31(13),18(13),18(21),40(21),24(17),29(3),29(3),31(6),18(6)),flip(a)]. given #38 (F,wt=-985): 54 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536). [para(31(a,1),52(a,1,2,2))]. given #39 (T,wt=-983): 53 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F). [back_rewrite(48),rewrite(51(23),37(18),18(16)),flip(a)]. given #40 (T,wt=-971): 55 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(7(a,1),53(a,1,2,2))]. given #41 (A,wt=-967): 38 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(29(a,1),21(a,1,2,2,2))]. ============================== PROOF ================================= % Proof 1 at 0.17 (+ 0.01) seconds: absorb. % Length of proof is 29. % Level of proof is 15. % Maximum clause weight is 9. % Given clauses 41. 3 f(f(x,x),f(x,y)) = x # answer(absorb). [goal]. 7 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). [assumption]. 10 f(f(c5,c5),f(c5,c6)) != c5 # answer(absorb). [deny(3)]. 15 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(7(a,1),7(a,1,2,2,2))]. 16 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(7(a,1),15(a,1,1,2)),rewrite(7(12),7(12),7(14),7(17),7(30))]. 17 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A). [para(7(a,1),16(a,1,2,2))]. 18 f(f(x,y),f(y,y)) = y # label(508B). [para(7(a,1),17(a,1,2,1))]. 19 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(18(a,1),7(a,1,2,1))]. 21 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(18(a,1),7(a,1,2,2,1,1,1))]. 23 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(18(a,1),15(a,1,2,2,1,1,1))]. 24 f(f(x,f(y,y)),y) = f(y,y) # label(508). [para(18(a,1),15(a,1,2,2,1)),rewrite(18(5),18(5))]. 26 f(f(f(x,x),y),x) = f(x,x) # label(510B). [para(17(a,1),18(a,1,1)),rewrite(17(7)),flip(a)]. 27 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511). [back_rewrite(19),rewrite(24(7))]. 28 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512). [para(26(a,1),7(a,1,2,2,1,1))]. 29 f(f(x,y),f(x,x)) = x # label(513). [para(18(a,1),26(a,1,1,1)),rewrite(18(6))]. 30 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(29(a,1),7(a,1,2,2,1,1))]. 31 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515). [para(7(a,1),29(a,1,1))]. 35 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A). [para(27(a,1),26(a,1)),flip(a)]. 36 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520). [para(31(a,1),28(a,1,2,2,2))]. 37 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B). [para(35(a,1),18(a,1,1)),rewrite(35(9)),flip(a)]. 38 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(29(a,1),21(a,1,2,2,2))]. 43 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(18(a,1),36(a,1,1)),rewrite(29(3),29(5))]. 45 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(43(a,1),31(a,1,2,1)),rewrite(43(18),29(11),43(18))]. 46 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(529). [para(45(a,1),21(a,1,2,2,1)),rewrite(24(3),31(8))]. 48 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). [para(46(a,1),23(a,1,1)),rewrite(29(16),29(18))]. 51 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(532). [para(24(a,1),30(a,1,2,2,1)),rewrite(31(9))]. 53 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F). [back_rewrite(48),rewrite(51(23),37(18),18(16)),flip(a)]. 57 f(f(x,x),f(x,y)) = x # label(525). [para(37(a,1),38(a,1,1)),rewrite(53(16),29(13),24(11),29(3)),flip(a)]. 58 $F # answer(absorb). [resolve(57,a,10,a)]. ============================== end of proof ========================== % Redundant proof: 63 $F # answer(absorb). [back_rewrite(10),rewrite(57(7)),xx(a)]. % Disable descendants: 10x given #42 (F,wt=-989): 59 f(x,f(f(x,x),y)) = f(x,x) # label(541E). [para(40(a,1),38(a,1,1)),rewrite(57(10),57(12),52(14),18(10)),flip(a)]. given #43 (F,wt=-989): 60 f(x,f(y,f(x,x))) = f(x,x) # label(542E). [para(42(a,1),38(a,1,1)),rewrite(57(10),57(12),54(14),18(10)),flip(a)]. given #44 (T,wt=-991): 67 f(f(x,x),f(y,x)) = x # label(548). [para(18(a,1),60(a,1,2,2)),rewrite(57(6))]. given #45 (T,wt=-987): 61 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E). [para(39(a,1),38(a,1,1)),rewrite(55(26),57(23),24(18),57(7)),flip(a)]. given #46 (A,wt=-491): 57 f(f(x,x),f(x,y)) = x # label(525). [para(37(a,1),38(a,1,1)),rewrite(53(16),29(13),24(11),29(3)),flip(a)]. given #47 (F,wt=-987): 62 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E). [para(41(a,1),38(a,1,1)),rewrite(56(26),57(23),24(18),57(7)),flip(a)]. given #48 (F,wt=-975): 65 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(59(a,1),33(a,1,2,1)),rewrite(57(4),57(5),57(7))]. given #49 (T,wt=-981): 71 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552). [para(31(a,1),65(a,1,2))]. given #50 (T,wt=-981): 74 f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y # label(555). [para(31(a,1),71(a,1,2,1,1,1)),rewrite(61(4))]. given #51 (A,wt=-475): 64 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(59(a,1),7(a,1,2,1)),rewrite(57(4),57(5),57(7))]. given #52 (F,wt=-981): 75 f(f(x,y),f(f(f(f(x,y),f(z,y)),f(z,y)),y)) = y # label(556). [para(31(a,1),74(a,1,2,1,1,2)),rewrite(31(8))]. given #53 (F,wt=-977): 72 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(18(a,1),71(a,1,2,1,1,1)),rewrite(67(3))]. given #54 (T,wt=-985): 76 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557). [para(7(a,1),72(a,1,2,1,1,2)),rewrite(7(12))]. given #55 (T,wt=-985): 78 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559). [para(29(a,1),72(a,1,2,1,1,2)),rewrite(29(4))]. given #56 (A,wt=-225): 66 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(60(a,1),7(a,1,2,1)),rewrite(57(4),57(5),57(7))]. given #57 (F,wt=-989): 80 f(f(x,x),x) = f(x,f(x,x)) # label(561). [para(26(a,1),78(a,1,2,1)),rewrite(57(5))]. given #58 (F,wt=-985): 81 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562). [back_rewrite(79),rewrite(80(2))]. given #59 (T,wt=-979): 77 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558). [para(24(a,1),72(a,1,2,1,1,2)),rewrite(57(4),24(4))]. given #60 (T,wt=-979): 82 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563). [para(18(a,1),81(a,1,2,1,2)),rewrite(80(3))]. given #61 (A,wt=-975): 68 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_rewrite(44),rewrite(67(3))]. given #62 (F,wt=-977): 73 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(29(a,1),71(a,1,2,1,1,1)),rewrite(57(3))]. given #63 (F,wt=-975): 70 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(61(a,1),7(a,1,1)),rewrite(31(7))]. given #64 (T,wt=-969): 69 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_rewrite(20),rewrite(67(3))]. given #65 (T,wt=-975): 83 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(62(a,1),69(a,1,2,1))]. given #66 (A,wt=-975): 84 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(26(a,1),83(a,1,2,2,1,1)),rewrite(57(7))]. given #67 (F,wt=-981): 87 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568). [para(81(a,1),84(a,1,2,2))]. given #68 (F,wt=-977): 86 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(45(a,1),84(a,1,2,2,2)),rewrite(29(17),45(14),61(7)),flip(a)]. given #69 (T,wt=-981): 89 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C). [para(86(a,1),77(a,1,2,1)),rewrite(60(14),57(11)),flip(a)]. ============================== PROOF ================================= % Proof 2 at 0.39 (+ 0.01) seconds: one. % Length of proof is 63. % Level of proof is 25. % Maximum clause weight is 11. % Given clauses 69. 2 f(y,f(y,y)) = f(x,f(x,x)) # answer(one). [goal]. 7 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). [assumption]. 9 f(c4,f(c4,c4)) != f(c3,f(c3,c3)) # answer(one). [deny(2)]. 15 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(7(a,1),7(a,1,2,2,2))]. 16 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(7(a,1),15(a,1,1,2)),rewrite(7(12),7(12),7(14),7(17),7(30))]. 17 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A). [para(7(a,1),16(a,1,2,2))]. 18 f(f(x,y),f(y,y)) = y # label(508B). [para(7(a,1),17(a,1,2,1))]. 19 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(18(a,1),7(a,1,2,1))]. 20 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(18(a,1),7(a,1,2,2,1,1,1,1))]. 21 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(18(a,1),7(a,1,2,2,1,1,1))]. 23 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(18(a,1),15(a,1,2,2,1,1,1))]. 24 f(f(x,f(y,y)),y) = f(y,y) # label(508). [para(18(a,1),15(a,1,2,2,1)),rewrite(18(5),18(5))]. 26 f(f(f(x,x),y),x) = f(x,x) # label(510B). [para(17(a,1),18(a,1,1)),rewrite(17(7)),flip(a)]. 27 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511). [back_rewrite(19),rewrite(24(7))]. 28 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512). [para(26(a,1),7(a,1,2,2,1,1))]. 29 f(f(x,y),f(x,x)) = x # label(513). [para(18(a,1),26(a,1,1,1)),rewrite(18(6))]. 30 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(29(a,1),7(a,1,2,2,1,1))]. 31 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515). [para(7(a,1),29(a,1,1))]. 33 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(31(a,1),7(a,1,2,2,2))]. 35 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A). [para(27(a,1),26(a,1)),flip(a)]. 36 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520). [para(31(a,1),28(a,1,2,2,2))]. 37 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B). [para(35(a,1),18(a,1,1)),rewrite(35(9)),flip(a)]. 38 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(29(a,1),21(a,1,2,2,2))]. 39 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522). [para(7(a,1),37(a,1,2,2))]. 40 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523). [para(18(a,1),37(a,1,2,1)),rewrite(29(8))]. 41 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524). [para(29(a,1),37(a,1,2,2))]. 42 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525). [para(31(a,1),40(a,1,2,2))]. 43 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(18(a,1),36(a,1,1)),rewrite(29(3),29(5))]. 45 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(43(a,1),31(a,1,2,1)),rewrite(43(18),29(11),43(18))]. 46 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(529). [para(45(a,1),21(a,1,2,2,1)),rewrite(24(3),31(8))]. 47 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x) # label(530). [para(18(a,1),46(a,1,1)),rewrite(29(4),29(5))]. 48 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). [para(46(a,1),23(a,1,1)),rewrite(29(16),29(18))]. 51 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(532). [para(24(a,1),30(a,1,2,2,1)),rewrite(31(9))]. 52 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E). [para(30(a,1),23(a,1,2,2,1)),rewrite(29(3),31(6),18(6),47(7),29(4),31(7),18(7),29(10),31(13),18(13),18(21),40(21),24(17),29(3),29(3),31(6),18(6)),flip(a)]. 53 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F). [back_rewrite(48),rewrite(51(23),37(18),18(16)),flip(a)]. 54 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536). [para(31(a,1),52(a,1,2,2))]. 55 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(7(a,1),53(a,1,2,2))]. 56 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(29(a,1),53(a,1,2,2))]. 57 f(f(x,x),f(x,y)) = x # label(525). [para(37(a,1),38(a,1,1)),rewrite(53(16),29(13),24(11),29(3)),flip(a)]. 59 f(x,f(f(x,x),y)) = f(x,x) # label(541E). [para(40(a,1),38(a,1,1)),rewrite(57(10),57(12),52(14),18(10)),flip(a)]. 60 f(x,f(y,f(x,x))) = f(x,x) # label(542E). [para(42(a,1),38(a,1,1)),rewrite(57(10),57(12),54(14),18(10)),flip(a)]. 61 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E). [para(39(a,1),38(a,1,1)),rewrite(55(26),57(23),24(18),57(7)),flip(a)]. 62 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E). [para(41(a,1),38(a,1,1)),rewrite(56(26),57(23),24(18),57(7)),flip(a)]. 65 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(59(a,1),33(a,1,2,1)),rewrite(57(4),57(5),57(7))]. 67 f(f(x,x),f(y,x)) = x # label(548). [para(18(a,1),60(a,1,2,2)),rewrite(57(6))]. 69 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_rewrite(20),rewrite(67(3))]. 71 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552). [para(31(a,1),65(a,1,2))]. 72 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(18(a,1),71(a,1,2,1,1,1)),rewrite(67(3))]. 76 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557). [para(7(a,1),72(a,1,2,1,1,2)),rewrite(7(12))]. 77 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558). [para(24(a,1),72(a,1,2,1,1,2)),rewrite(57(4),24(4))]. 78 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559). [para(29(a,1),72(a,1,2,1,1,2)),rewrite(29(4))]. 79 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y) # label(560). [para(62(a,1),76(a,1,2,2)),rewrite(62(9))]. 80 f(f(x,x),x) = f(x,f(x,x)) # label(561). [para(26(a,1),78(a,1,2,1)),rewrite(57(5))]. 81 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562). [back_rewrite(79),rewrite(80(2))]. 82 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563). [para(18(a,1),81(a,1,2,1,2)),rewrite(80(3))]. 83 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(62(a,1),69(a,1,2,1))]. 84 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(26(a,1),83(a,1,2,2,1,1)),rewrite(57(7))]. 86 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(45(a,1),84(a,1,2,2,2)),rewrite(29(17),45(14),61(7)),flip(a)]. 87 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568). [para(81(a,1),84(a,1,2,2))]. 89 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C). [para(86(a,1),77(a,1,2,1)),rewrite(60(14),57(11)),flip(a)]. 96 f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(y,f(y,y)) # label(576). [para(89(a,1),82(a,1,2,2)),rewrite(89(14))]. 97 f(x,f(x,x)) = f(y,f(y,y)) # label(577). [para(89(a,1),87(a,1,2,2)),rewrite(96(7))]. 98 $F # answer(one). [resolve(97,a,9,a)]. ============================== end of proof ========================== NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(97)]. 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 ]). % Disable descendants: 9 given #70 (T,wt=-989): 92 f(f(x,f(x,x)),y) = f(y,y) # label(573). [para(89(a,1),26(a,1,1))]. given #71 (A,wt=-975): 85 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(31(a,1),83(a,1,2,2,2))]. given #72 (F,wt=-989): 93 f(f(x,f(x,x)),f(y,y)) = y # label(574). [para(89(a,1),29(a,1,1))]. given #73 (F,wt=-989): 94 f(x,f(y,f(y,y))) = f(x,x) # label(575). [para(89(a,1),59(a,1,2))]. ============================== PROOF ================================= % Proof 3 at 0.44 (+ 0.01) seconds: oml. % Length of proof is 58. % Level of proof is 24. % Maximum clause weight is 11. % Given clauses 73. 4 f(x,f(x,f(x,y))) = f(x,y) # answer(oml). [goal]. 7 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). [assumption]. 11 f(c7,f(c7,f(c7,c8))) != f(c7,c8) # answer(oml). [deny(4)]. 15 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(7(a,1),7(a,1,2,2,2))]. 16 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(7(a,1),15(a,1,1,2)),rewrite(7(12),7(12),7(14),7(17),7(30))]. 17 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A). [para(7(a,1),16(a,1,2,2))]. 18 f(f(x,y),f(y,y)) = y # label(508B). [para(7(a,1),17(a,1,2,1))]. 19 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(18(a,1),7(a,1,2,1))]. 20 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(18(a,1),7(a,1,2,2,1,1,1,1))]. 21 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(18(a,1),7(a,1,2,2,1,1,1))]. 23 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(18(a,1),15(a,1,2,2,1,1,1))]. 24 f(f(x,f(y,y)),y) = f(y,y) # label(508). [para(18(a,1),15(a,1,2,2,1)),rewrite(18(5),18(5))]. 26 f(f(f(x,x),y),x) = f(x,x) # label(510B). [para(17(a,1),18(a,1,1)),rewrite(17(7)),flip(a)]. 27 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511). [back_rewrite(19),rewrite(24(7))]. 28 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512). [para(26(a,1),7(a,1,2,2,1,1))]. 29 f(f(x,y),f(x,x)) = x # label(513). [para(18(a,1),26(a,1,1,1)),rewrite(18(6))]. 30 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(29(a,1),7(a,1,2,2,1,1))]. 31 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515). [para(7(a,1),29(a,1,1))]. 33 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(31(a,1),7(a,1,2,2,2))]. 35 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A). [para(27(a,1),26(a,1)),flip(a)]. 36 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520). [para(31(a,1),28(a,1,2,2,2))]. 37 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B). [para(35(a,1),18(a,1,1)),rewrite(35(9)),flip(a)]. 38 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(29(a,1),21(a,1,2,2,2))]. 39 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522). [para(7(a,1),37(a,1,2,2))]. 40 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523). [para(18(a,1),37(a,1,2,1)),rewrite(29(8))]. 41 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524). [para(29(a,1),37(a,1,2,2))]. 42 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525). [para(31(a,1),40(a,1,2,2))]. 43 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(18(a,1),36(a,1,1)),rewrite(29(3),29(5))]. 45 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(43(a,1),31(a,1,2,1)),rewrite(43(18),29(11),43(18))]. 46 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(529). [para(45(a,1),21(a,1,2,2,1)),rewrite(24(3),31(8))]. 47 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x) # label(530). [para(18(a,1),46(a,1,1)),rewrite(29(4),29(5))]. 48 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). [para(46(a,1),23(a,1,1)),rewrite(29(16),29(18))]. 51 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(532). [para(24(a,1),30(a,1,2,2,1)),rewrite(31(9))]. 52 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E). [para(30(a,1),23(a,1,2,2,1)),rewrite(29(3),31(6),18(6),47(7),29(4),31(7),18(7),29(10),31(13),18(13),18(21),40(21),24(17),29(3),29(3),31(6),18(6)),flip(a)]. 53 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F). [back_rewrite(48),rewrite(51(23),37(18),18(16)),flip(a)]. 54 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536). [para(31(a,1),52(a,1,2,2))]. 55 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(7(a,1),53(a,1,2,2))]. 56 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(29(a,1),53(a,1,2,2))]. 57 f(f(x,x),f(x,y)) = x # label(525). [para(37(a,1),38(a,1,1)),rewrite(53(16),29(13),24(11),29(3)),flip(a)]. 59 f(x,f(f(x,x),y)) = f(x,x) # label(541E). [para(40(a,1),38(a,1,1)),rewrite(57(10),57(12),52(14),18(10)),flip(a)]. 60 f(x,f(y,f(x,x))) = f(x,x) # label(542E). [para(42(a,1),38(a,1,1)),rewrite(57(10),57(12),54(14),18(10)),flip(a)]. 61 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E). [para(39(a,1),38(a,1,1)),rewrite(55(26),57(23),24(18),57(7)),flip(a)]. 62 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E). [para(41(a,1),38(a,1,1)),rewrite(56(26),57(23),24(18),57(7)),flip(a)]. 65 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(59(a,1),33(a,1,2,1)),rewrite(57(4),57(5),57(7))]. 67 f(f(x,x),f(y,x)) = x # label(548). [para(18(a,1),60(a,1,2,2)),rewrite(57(6))]. 69 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_rewrite(20),rewrite(67(3))]. 71 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552). [para(31(a,1),65(a,1,2))]. 72 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(18(a,1),71(a,1,2,1,1,1)),rewrite(67(3))]. 73 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(29(a,1),71(a,1,2,1,1,1)),rewrite(57(3))]. 77 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558). [para(24(a,1),72(a,1,2,1,1,2)),rewrite(57(4),24(4))]. 83 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(62(a,1),69(a,1,2,1))]. 84 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(26(a,1),83(a,1,2,2,1,1)),rewrite(57(7))]. 86 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(45(a,1),84(a,1,2,2,2)),rewrite(29(17),45(14),61(7)),flip(a)]. 89 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C). [para(86(a,1),77(a,1,2,1)),rewrite(60(14),57(11)),flip(a)]. 94 f(x,f(y,f(y,y))) = f(x,x) # label(575). [para(89(a,1),59(a,1,2))]. 95 f(f(x,x),f(y,f(y,y))) = x # label(594). [para(89(a,1),57(a,1,2))]. 118 f(x,f(x,f(x,y))) = f(x,y) # label(599). [para(94(a,1),73(a,1,2,1,1)),rewrite(95(7))]. 119 $F # answer(oml). [resolve(118,a,11,a)]. ============================== end of proof ========================== % Redundant proof: 125 $F # answer(oml). [back_rewrite(11),rewrite(118(7)),xx(a)]. % Disable descendants: 11x given #74 (T,wt=-989): 95 f(f(x,x),f(y,f(y,y))) = x # label(594). [para(89(a,1),57(a,1,2))]. given #75 (T,wt=-989): 97 f(x,f(x,x)) = f(y,f(y,y)) # label(577). [para(89(a,1),87(a,1,2,2)),rewrite(96(7))]. given #76 (A,wt=-967): 88 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(29(a,1),87(a,1,2,2))]. given #77 (F,wt=-989): 116 f(f(x,y),f(f(y,x),y)) = y # label(597). [para(94(a,1),71(a,1,2,1,1)),rewrite(95(7))]. given #78 (F,wt=-989): 117 f(x,f(x,f(y,x))) = f(y,x) # label(598). [para(94(a,1),72(a,1,2,1,1)),rewrite(95(7))]. given #79 (T,wt=-989): 118 f(x,f(x,f(x,y))) = f(x,y) # label(599). [para(94(a,1),73(a,1,2,1,1)),rewrite(95(7))]. given #80 (T,wt=-989): 140 f(f(x,y),f(f(x,y),x)) = x # label(629E). [para(32(a,1),116(a,1,2,1)),rewrite(62(4))]. given #81 (A,wt=-987): 99 f(f(x,y),f(f(z,f(z,z)),y)) = y # label(579). [para(92(a,2),18(a,1,2))]. given #82 (F,wt=-987): 100 f(f(x,y),f(f(z,f(z,z)),x)) = x # label(580). [para(92(a,2),29(a,1,2))]. given #83 (F,wt=-987): 103 f(f(f(x,f(x,x)),y),f(y,z)) = y # label(583). [para(92(a,1),21(a,1,2,1,2)),rewrite(89(10),89(13),102(12))]. given #84 (T,wt=-989): 147 f(f(x,y),x) = f(x,f(x,y)) # label(623). [back_rewrite(142),rewrite(146(7))]. given #85 (T,wt=-989): 148 f(f(x,y),f(x,f(x,y))) = x # label(629F). [back_rewrite(143),rewrite(147(3),118(3),147(3))]. given #86 (A,wt=-985): 101 f(x,f(f(y,f(y,y)),f(z,x))) = f(z,x) # label(581). [para(92(a,2),31(a,1,2))]. given #87 (F,wt=-989): 149 f(f(x,y),f(y,f(y,x))) = y # label(625). [back_rewrite(141),rewrite(147(3),118(4),147(3))]. given #88 (F,wt=-989): 152 f(f(x,y),y) = f(y,f(x,y)) # label(628B). [para(7(a,1),147(a,1,1)),rewrite(7(14)),flip(a)]. given #89 (T,wt=-989): 153 f(f(x,y),f(y,f(x,y))) = y # label(629). [para(147(a,1),75(a,1,2,1,1)),rewrite(152(2),152(5),147(8),117(8),147(5),117(5),152(4))]. given #90 (T,wt=-985): 102 f(x,f(f(y,f(y,y)),f(x,z))) = f(x,z) # label(582). [para(92(a,2),32(a,1,2))]. given #91 (A,wt=-471): 104 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(92(a,2),21(a,1,2,2,1,1,2))]. given #92 (F,wt=-985): 105 f(f(f(x,f(x,x)),f(y,z)),z) = f(y,z) # label(586). [para(92(a,1),23(a,1,2,1,2)),rewrite(89(13),89(14),102(13))]. given #93 (F,wt=-985): 109 f(x,f(f(y,f(y,y)),z)) = f(x,f(z,z)) # label(589B). [para(92(a,2),77(a,2,2)),rewrite(101(7)),flip(a)]. given #94 (T,wt=-985): 114 f(f(x,f(x,x)),f(f(y,f(y,y)),z)) = z # label(595). [para(92(a,2),93(a,1,2))]. given #95 (T,wt=-985): 115 f(x,f(f(y,x),f(z,f(z,z)))) = f(y,x) # label(577A). [para(94(a,2),31(a,1,2))]. given #96 (A,wt=-463): 106 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(92(a,2),23(a,1,2,2,1,1,2))]. given #97 (F,wt=-985): 126 f(f(x,f(y,f(y,y))),f(z,f(z,z))) = x # label(613). [para(94(a,2),95(a,1,1))]. given #98 (F,wt=-983): 110 f(f(x,x),f(f(x,y),f(x,y))) = f(x,f(x,x)) # label(590). [para(92(a,1),87(a,1,2))]. given #99 (T,wt=-981): 161 f(x,f(f(y,f(y,y)),z)) = f(x,f(f(u,f(u,u)),z)) # label(576A). [para(92(a,2),109(a,2,2))]. given #100 (T,wt=-979): 120 f(x,f(f(y,x),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x) # label(601). [para(94(a,1),69(a,1,2,2,1,1,1)),rewrite(95(6),95(5))]. given #101 (A,wt=-977): 111 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(92(a,2),87(a,1,1))]. given #102 (F,wt=-983): 168 f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z)))) = x # label(640). [para(153(a,1),120(a,1,2,1)),rewrite(153(8),147(5),117(5),153(7),153(11))]. given #103 (F,wt=-981): 171 f(f(f(x,f(x,x)),f(x,f(x,x))),y) = f(z,f(z,z)) # label(567C). [para(94(a,1),111(a,1,1)),rewrite(113(13),114(11),113(14))]. given #104 (T,wt=-979): 150 f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,y)) = y # label(626). [back_rewrite(128),rewrite(147(4),147(5),118(5),147(4))]. given #105 (T,wt=-981): 175 f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z)) = z # label(644). [para(117(a,1),150(a,1,1,2,1))]. given #106 (A,wt=-477): 112 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(92(a,2),87(a,1,2,1,2))]. given #107 (F,wt=-981): 177 f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z)) = z # label(646). [para(31(a,1),175(a,1,1,2,2))]. given #108 (F,wt=-979): 151 f(f(x,y),f(f(z,f(z,z)),f(f(y,f(y,x)),f(u,y)))) = y # label(627). [back_rewrite(127),rewrite(147(5),147(6),118(6),147(5))]. given #109 (T,wt=-989): 183 f(f(x,f(x,y)),f(y,x)) = x # label(652A). [para(151(a,1),101(a,1)),flip(a)]. given #110 (T,wt=-979): 154 f(f(x,y),f(f(f(y,y),x),f(f(y,f(x,y)),f(y,z)))) = y # label(630). [para(147(a,1),70(a,1,2,2,1,1,1)),rewrite(147(6),118(6),152(5))]. given #111 (A,wt=-481): 113 f(x,f(f(y,f(y,y)),f(z,f(z,z)))) = f(z,f(z,z)) # label(576). [para(92(a,2),89(a,1,2))]. given #112 (F,wt=-977): 134 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(92(a,1),88(a,1,2))]. given #113 (F,wt=-983): 184 f(f(x,x),f(f(y,x),f(x,z))) = f(x,f(x,x)) # label(658). [para(175(a,1),134(a,1,1,1)),rewrite(175(8),99(14),175(13),175(13),175(13))]. given #114 (T,wt=-981): 187 f(f(x,x),f(f(y,x),f(z,f(z,z)))) = f(x,f(x,x)) # label(660). [para(97(a,1),184(a,1,2,2))]. given #115 (T,wt=-977): 173 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(93(a,1),168(a,1,2,2,2)),rewrite(124(6))]. given #116 (A,wt=-227): 121 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(94(a,2),87(a,1,1))]. given #117 (F,wt=-977): 180 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(177(a,1),57(a,1,2)),rewrite(99(13))]. given #118 (F,wt=-981): 190 f(f(f(x,y),f(z,y)),y) = f(y,f(f(x,y),f(z,y))) # label(664B). [para(180(a,1),31(a,1,2,1)),rewrite(103(11)),flip(a)]. given #119 (T,wt=-979): 192 f(f(x,y),f(y,f(f(z,y),f(x,y)))) = f(f(z,y),f(x,y)) # label(666). [para(180(a,2),101(a,1,2)),rewrite(190(5))]. given #120 (T,wt=-979): 193 f(x,f(f(x,y),f(f(z,f(x,y)),x))) = f(f(z,f(x,y)),x) # label(669). [para(57(a,1),192(a,1,1)),rewrite(57(6),57(11))]. given #121 (A,wt=-16): 123 f(f(x,f(x,x)),y) = f(y,f(z,f(z,z))) # label(594B). [para(94(a,2),92(a,2))]. given #122 (F,wt=-987): 196 f(x,f(f(x,y),f(y,x))) = f(y,x) # label(670). [para(67(a,1),193(a,1,2,2,1)),rewrite(67(7))]. given #123 (F,wt=-979): 194 f(f(x,y),f(x,f(f(z,x),f(x,y)))) = f(f(z,x),f(x,y)) # label(667). [para(62(a,1),192(a,1,1)),rewrite(62(6),62(11))]. given #124 (T,wt=-979): 195 f(f(x,y),f(y,f(f(y,z),f(x,y)))) = f(f(y,z),f(x,y)) # label(668). [para(62(a,1),192(a,1,2,2,1)),rewrite(62(10))]. given #125 (T,wt=-985): 197 f(f(x,y),f(y,x)) = f(f(y,x),f(y,x)) # label(671A). [para(196(a,1),195(a,1,2)),flip(a)]. % Operation f is commutative; C redundancy checks enabled. ============================== PROOF ================================= % Proof 4 at 0.92 (+ 0.01) seconds: comm. % Length of proof is 96. % Level of proof is 38. % Maximum clause weight is 7. % Given clauses 125. 1 f(y,x) = f(x,y) # answer(comm). [goal]. 7 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). [assumption]. 8 f(c2,c1) != f(c1,c2) # answer(comm). [deny(1)]. 15 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(7(a,1),7(a,1,2,2,2))]. 16 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(7(a,1),15(a,1,1,2)),rewrite(7(12),7(12),7(14),7(17),7(30))]. 17 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A). [para(7(a,1),16(a,1,2,2))]. 18 f(f(x,y),f(y,y)) = y # label(508B). [para(7(a,1),17(a,1,2,1))]. 19 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(18(a,1),7(a,1,2,1))]. 20 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(18(a,1),7(a,1,2,2,1,1,1,1))]. 21 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(18(a,1),7(a,1,2,2,1,1,1))]. 22 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(18(a,1),15(a,1,2,2,1,1,1,1))]. 23 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(18(a,1),15(a,1,2,2,1,1,1))]. 24 f(f(x,f(y,y)),y) = f(y,y) # label(508). [para(18(a,1),15(a,1,2,2,1)),rewrite(18(5),18(5))]. 26 f(f(f(x,x),y),x) = f(x,x) # label(510B). [para(17(a,1),18(a,1,1)),rewrite(17(7)),flip(a)]. 27 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511). [back_rewrite(19),rewrite(24(7))]. 28 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512). [para(26(a,1),7(a,1,2,2,1,1))]. 29 f(f(x,y),f(x,x)) = x # label(513). [para(18(a,1),26(a,1,1,1)),rewrite(18(6))]. 30 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(29(a,1),7(a,1,2,2,1,1))]. 31 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515). [para(7(a,1),29(a,1,1))]. 32 f(x,f(f(x,y),f(x,y))) = f(x,y) # label(516). [para(29(a,1),29(a,1,1))]. 33 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(31(a,1),7(a,1,2,2,2))]. 34 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(7(a,1),31(a,1,2,1)),rewrite(7(20),7(22))]. 35 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A). [para(27(a,1),26(a,1)),flip(a)]. 36 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520). [para(31(a,1),28(a,1,2,2,2))]. 37 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B). [para(35(a,1),18(a,1,1)),rewrite(35(9)),flip(a)]. 38 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(29(a,1),21(a,1,2,2,2))]. 39 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522). [para(7(a,1),37(a,1,2,2))]. 40 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523). [para(18(a,1),37(a,1,2,1)),rewrite(29(8))]. 41 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524). [para(29(a,1),37(a,1,2,2))]. 42 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525). [para(31(a,1),40(a,1,2,2))]. 43 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(18(a,1),36(a,1,1)),rewrite(29(3),29(5))]. 44 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(29(a,1),22(a,1,2,2,1,1))]. 45 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(43(a,1),31(a,1,2,1)),rewrite(43(18),29(11),43(18))]. 46 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(529). [para(45(a,1),21(a,1,2,2,1)),rewrite(24(3),31(8))]. 47 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x) # label(530). [para(18(a,1),46(a,1,1)),rewrite(29(4),29(5))]. 48 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). [para(46(a,1),23(a,1,1)),rewrite(29(16),29(18))]. 51 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(532). [para(24(a,1),30(a,1,2,2,1)),rewrite(31(9))]. 52 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E). [para(30(a,1),23(a,1,2,2,1)),rewrite(29(3),31(6),18(6),47(7),29(4),31(7),18(7),29(10),31(13),18(13),18(21),40(21),24(17),29(3),29(3),31(6),18(6)),flip(a)]. 53 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F). [back_rewrite(48),rewrite(51(23),37(18),18(16)),flip(a)]. 54 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536). [para(31(a,1),52(a,1,2,2))]. 55 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(7(a,1),53(a,1,2,2))]. 56 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(29(a,1),53(a,1,2,2))]. 57 f(f(x,x),f(x,y)) = x # label(525). [para(37(a,1),38(a,1,1)),rewrite(53(16),29(13),24(11),29(3)),flip(a)]. 59 f(x,f(f(x,x),y)) = f(x,x) # label(541E). [para(40(a,1),38(a,1,1)),rewrite(57(10),57(12),52(14),18(10)),flip(a)]. 60 f(x,f(y,f(x,x))) = f(x,x) # label(542E). [para(42(a,1),38(a,1,1)),rewrite(57(10),57(12),54(14),18(10)),flip(a)]. 61 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E). [para(39(a,1),38(a,1,1)),rewrite(55(26),57(23),24(18),57(7)),flip(a)]. 62 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E). [para(41(a,1),38(a,1,1)),rewrite(56(26),57(23),24(18),57(7)),flip(a)]. 65 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(59(a,1),33(a,1,2,1)),rewrite(57(4),57(5),57(7))]. 67 f(f(x,x),f(y,x)) = x # label(548). [para(18(a,1),60(a,1,2,2)),rewrite(57(6))]. 68 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_rewrite(44),rewrite(67(3))]. 69 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_rewrite(20),rewrite(67(3))]. 71 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552). [para(31(a,1),65(a,1,2))]. 72 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(18(a,1),71(a,1,2,1,1,1)),rewrite(67(3))]. 73 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(29(a,1),71(a,1,2,1,1,1)),rewrite(57(3))]. 76 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557). [para(7(a,1),72(a,1,2,1,1,2)),rewrite(7(12))]. 77 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558). [para(24(a,1),72(a,1,2,1,1,2)),rewrite(57(4),24(4))]. 78 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559). [para(29(a,1),72(a,1,2,1,1,2)),rewrite(29(4))]. 79 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y) # label(560). [para(62(a,1),76(a,1,2,2)),rewrite(62(9))]. 80 f(f(x,x),x) = f(x,f(x,x)) # label(561). [para(26(a,1),78(a,1,2,1)),rewrite(57(5))]. 81 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562). [back_rewrite(79),rewrite(80(2))]. 82 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563). [para(18(a,1),81(a,1,2,1,2)),rewrite(80(3))]. 83 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(62(a,1),69(a,1,2,1))]. 84 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(26(a,1),83(a,1,2,2,1,1)),rewrite(57(7))]. 86 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(45(a,1),84(a,1,2,2,2)),rewrite(29(17),45(14),61(7)),flip(a)]. 87 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568). [para(81(a,1),84(a,1,2,2))]. 89 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C). [para(86(a,1),77(a,1,2,1)),rewrite(60(14),57(11)),flip(a)]. 92 f(f(x,f(x,x)),y) = f(y,y) # label(573). [para(89(a,1),26(a,1,1))]. 94 f(x,f(y,f(y,y))) = f(x,x) # label(575). [para(89(a,1),59(a,1,2))]. 95 f(f(x,x),f(y,f(y,y))) = x # label(594). [para(89(a,1),57(a,1,2))]. 96 f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(y,f(y,y)) # label(576). [para(89(a,1),82(a,1,2,2)),rewrite(89(14))]. 97 f(x,f(x,x)) = f(y,f(y,y)) # label(577). [para(89(a,1),87(a,1,2,2)),rewrite(96(7))]. 99 f(f(x,y),f(f(z,f(z,z)),y)) = y # label(579). [para(92(a,2),18(a,1,2))]. 101 f(x,f(f(y,f(y,y)),f(z,x))) = f(z,x) # label(581). [para(92(a,2),31(a,1,2))]. 102 f(x,f(f(y,f(y,y)),f(x,z))) = f(x,z) # label(582). [para(92(a,2),32(a,1,2))]. 103 f(f(f(x,f(x,x)),y),f(y,z)) = y # label(583). [para(92(a,1),21(a,1,2,1,2)),rewrite(89(10),89(13),102(12))]. 110 f(f(x,x),f(f(x,y),f(x,y))) = f(x,f(x,x)) # label(590). [para(92(a,1),87(a,1,2))]. 116 f(f(x,y),f(f(y,x),y)) = y # label(597). [para(94(a,1),71(a,1,2,1,1)),rewrite(95(7))]. 117 f(x,f(x,f(y,x))) = f(y,x) # label(598). [para(94(a,1),72(a,1,2,1,1)),rewrite(95(7))]. 118 f(x,f(x,f(x,y))) = f(x,y) # label(599). [para(94(a,1),73(a,1,2,1,1)),rewrite(95(7))]. 128 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(97(a,1),34(a,1,1,1)),rewrite(57(6),57(7))]. 142 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(118(a,1),116(a,1,1))]. 146 f(f(f(x,y),x),f(x,y)) = x # label(620). [para(103(a,1),68(a,1,2,1,1,1)),rewrite(103(6),110(6),103(9),101(9),103(9))]. 147 f(f(x,y),x) = f(x,f(x,y)) # label(623). [back_rewrite(142),rewrite(146(7))]. 150 f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,y)) = y # label(626). [back_rewrite(128),rewrite(147(4),147(5),118(5),147(4))]. 175 f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z)) = z # label(644). [para(117(a,1),150(a,1,1,2,1))]. 177 f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z)) = z # label(646). [para(31(a,1),175(a,1,1,2,2))]. 180 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(177(a,1),57(a,1,2)),rewrite(99(13))]. 190 f(f(f(x,y),f(z,y)),y) = f(y,f(f(x,y),f(z,y))) # label(664B). [para(180(a,1),31(a,1,2,1)),rewrite(103(11)),flip(a)]. 192 f(f(x,y),f(y,f(f(z,y),f(x,y)))) = f(f(z,y),f(x,y)) # label(666). [para(180(a,2),101(a,1,2)),rewrite(190(5))]. 193 f(x,f(f(x,y),f(f(z,f(x,y)),x))) = f(f(z,f(x,y)),x) # label(669). [para(57(a,1),192(a,1,1)),rewrite(57(6),57(11))]. 195 f(f(x,y),f(y,f(f(y,z),f(x,y)))) = f(f(y,z),f(x,y)) # label(668). [para(62(a,1),192(a,1,2,2,1)),rewrite(62(10))]. 196 f(x,f(f(x,y),f(y,x))) = f(y,x) # label(670). [para(67(a,1),193(a,1,2,2,1)),rewrite(67(7))]. 197 f(f(x,y),f(y,x)) = f(f(y,x),f(y,x)) # label(671A). [para(196(a,1),195(a,1,2)),flip(a)]. 198 f(f(x,f(y,z)),f(f(z,y),f(y,z))) = f(y,z) # label(672). [para(197(a,2),18(a,1,2))]. 200 f(x,y) = f(y,x) # label(933C). [para(197(a,1),197(a,1,1)),rewrite(57(7),198(8))]. 201 $F # answer(comm). [resolve(200,a,8,a)]. ============================== end of proof ========================== % back CAC tautology: 197 f(f(x,y),f(y,x)) = f(f(y,x),f(y,x)) # label(671A). [para(196(a,1),195(a,1,2)),flip(a)]. % Disable descendants: 8 given #126 (A,wt=-485): 124 f(f(x,f(x,x)),f(y,f(z,f(z,z)))) = y # label(567D). [para(94(a,2),93(a,1,2))]. given #127 (F,wt=-993): 200 f(x,y) = f(y,x) # label(933C). [para(197(a,1),197(a,1,1)),rewrite(57(7),198(8))]. given #128 (F,wt=-989): 199 f(f(x,f(y,x)),f(x,y)) = x # label(673). [para(197(a,1),168(a,1,2,2)),rewrite(32(6))]. given #129 (T,wt=-989): 205 f(f(x,y),f(x,f(y,x))) = x # label(677). [para(200(a,1),148(a,1,2,2))]. given #130 (T,wt=-989): 209 f(f(x,f(y,x)),f(y,x)) = x # label(629G). [para(200(a,1),153(a,1))]. given #131 (A,wt=-481): 131 f(f(x,x),f(f(y,f(y,y)),f(x,z))) = f(x,f(x,x)) # label(568). [para(97(a,1),87(a,1,2,1))]. given #132 (F,wt=-985): 210 f(x,f(f(f(y,y),y),f(x,z))) = f(x,z) # label(563A). [para(200(a,1),102(a,1,2,1))]. given #133 (F,wt=-985): 211 f(f(f(x,f(x,x)),f(y,z)),y) = f(z,y) # label(678). [para(200(a,1),105(a,1,1,2))]. given #134 (T,wt=-985): 212 f(f(f(x,f(x,x)),y),z) = f(z,f(y,y)) # label(679). [para(200(a,1),109(a,1))]. given #135 (T,wt=-983): 198 f(f(x,f(y,z)),f(f(z,y),f(y,z))) = f(y,z) # label(672). [para(197(a,2),18(a,1,2))]. given #136 (A,wt=-235): 132 f(x,f(f(y,f(y,y)),x)) = f(z,f(z,z)) # label(567D). [para(92(a,2),97(a,1,2))]. given #137 (F,wt=-983): 202 f(x,f(f(y,x),f(y,f(z,f(y,x))))) = f(y,x) # label(676). [back_rewrite(157),rewrite(199(5))]. given #138 (F,wt=-987): 227 f(x,f(f(y,z),f(z,x))) = f(z,x) # label(689). [para(194(a,1),202(a,1,2))]. given #139 (T,wt=-987): 230 f(x,f(f(y,z),f(y,x))) = f(y,x) # label(691). [para(62(a,1),227(a,1,2,1))]. given #140 (T,wt=-987): 234 f(x,f(f(y,z),f(x,z))) = f(z,x) # label(696). [para(200(a,1),227(a,1,2,2))]. given #141 (A,wt=-47): 133 f(x,f(x,f(y,f(y,y)))) = f(z,f(z,z)) # label(567D). [para(94(a,2),97(a,1,2))]. given #142 (F,wt=-987): 235 f(x,f(f(y,x),f(z,y))) = f(y,x) # label(697). [para(200(a,1),227(a,1,2))]. given #143 (F,wt=-987): 239 f(f(f(x,y),f(x,z)),z) = f(x,z) # label(701A). [para(230(a,1),200(a,1)),flip(a)]. given #144 (T,wt=-987): 240 f(x,f(f(y,x),f(y,z))) = f(y,x) # label(702). [para(200(a,1),230(a,1,2))]. given #145 (T,wt=-987): 242 f(f(f(x,y),f(z,y)),z) = f(y,z) # label(704A). [para(234(a,1),200(a,1)),flip(a)]. given #146 (A,wt=-465): 135 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(92(a,2),88(a,1,1))]. given #147 (F,wt=-987): 243 f(x,f(f(x,y),f(z,y))) = f(y,x) # label(705). [para(200(a,1),234(a,1,2))]. given #148 (F,wt=-987): 261 f(f(f(x,y),f(z,y)),x) = f(y,x) # label(725). [para(200(a,1),242(a,1,1))]. given #149 (T,wt=-985): 228 f(x,f(y,f(f(z,y),x))) = f(f(z,y),x) # label(690). [para(67(a,1),227(a,1,2,1))]. given #150 (T,wt=-985): 229 f(x,f(y,f(f(y,z),x))) = f(f(y,z),x) # label(692). [para(57(a,1),227(a,1,2,1))]. given #151 (A,wt=-215): 136 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(92(a,2),88(a,1,2,1,2))]. given #152 (F,wt=-985): 233 f(f(x,y),f(f(z,f(y,f(y,x))),y)) = y # label(695). [para(183(a,1),227(a,1,2,2)),rewrite(183(10))]. given #153 (F,wt=-985): 237 f(f(x,f(y,x)),f(f(f(y,x),z),x)) = x # label(629D). [para(153(a,1),230(a,1,2,2)),rewrite(153(10))]. given #154 (T,wt=-985): 241 f(f(x,y),z) = f(z,f(y,f(z,f(x,y)))) # label(703A). [para(67(a,1),234(a,1,2,1)),flip(a)]. given #155 (T,wt=-985): 246 f(x,f(f(f(y,z),x),z)) = f(f(y,z),x) # label(708). [para(67(a,1),235(a,1,2,2))]. given #156 (A,wt=-90): 137 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(94(a,2),88(a,1,1))]. given #157 (F,wt=-985): 255 f(f(x,f(y,x)),f(x,f(f(x,y),z))) = x # label(718). [para(205(a,1),240(a,1,2,1)),rewrite(205(10))]. given #158 (F,wt=-985): 259 f(f(x,f(y,f(x,z))),y) = f(f(x,z),y) # label(722). [para(57(a,1),242(a,1,1,1))]. given #159 (T,wt=-985): 260 f(f(f(x,f(y,z)),z),f(z,f(z,y))) = z # label(724). [para(149(a,1),242(a,2)),rewrite(183(6))]. given #160 (T,wt=-985): 262 f(x,f(f(x,f(y,z)),z)) = f(f(y,z),x) # label(726). [para(67(a,1),243(a,1,2,2))]. given #161 (A,wt=-27): 138 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(94(a,2),88(a,1,2,1,2))]. given #162 (F,wt=-985): 264 f(f(f(x,f(y,z)),z),x) = f(f(y,z),x) # label(728). [para(67(a,1),261(a,1,1,2))]. given #163 (F,wt=-985): 267 f(f(f(x,y),y),f(f(z,f(x,y)),y)) = y # label(629A). [para(117(a,1),233(a,1,2,1,2))]. given #164 (T,wt=-985): 269 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)) # label(731). [para(241(a,1),200(a,1))]. given #165 (T,wt=-985): 276 f(f(f(x,f(y,z)),y),f(y,f(y,z))) = y # label(723). [para(200(a,1),260(a,1,1,1,2))]. given #166 (A,wt=-4): 139 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(97(a,1),88(a,1,2,1))]. given #167 (F,wt=-985): 278 f(f(x,f(y,f(z,x))),y) = f(y,f(z,x)) # label(736A). [para(269(a,1),200(a,1)),flip(a)]. given #168 (F,wt=-983): 219 f(f(x,f(x,x)),f(y,z)) = f(f(y,z),f(z,y)) # label(682B). [para(211(a,1),57(a,1,2)),rewrite(99(9)),flip(a)]. given #169 (T,wt=-983): 223 f(f(x,f(y,z)),f(f(y,z),f(z,y))) = f(z,y) # label(686). [para(200(a,1),198(a,1,1,2))]. given #170 (T,wt=-983): 285 f(f(f(x,y),f(y,x)),f(z,f(x,y))) = f(y,x) # label(740A). [para(223(a,1),200(a,1)),flip(a)]. given #171 (A,wt=-973): 156 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_rewrite(107),rewrite(152(8))]. given #172 (F,wt=-985): 290 f(f(x,y),f(f(z,f(f(y,x),z)),y)) = y # label(759). [para(156(a,1),269(a,1,2,2)),rewrite(105(9),156(18))]. given #173 (F,wt=-985): 291 f(f(f(x,f(f(y,z),x)),y),f(z,y)) = y # label(760). [para(156(a,1),278(a,1,1,2)),rewrite(105(8),156(18))]. given #174 (T,wt=-985): 292 f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z) # label(761). [para(29(a,1),290(a,1,2,1,2,1)),rewrite(57(3))]. given #175 (T,wt=-985): 294 f(f(x,y),f(f(z,f(z,f(y,x))),y)) = y # label(625A). [para(200(a,1),290(a,1,2,1,2))]. given #176 (A,wt=-92): 158 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(92(a,2),104(a,1,2,1,2))]. given #177 (F,wt=-985): 300 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z) # label(766). [para(200(a,1),292(a,1,2,1,2))]. given #178 (F,wt=-983): 286 f(f(f(x,y),f(y,x)),f(z,f(y,x))) = f(x,y) # label(741). [para(200(a,1),285(a,1,1))]. given #179 (T,wt=-981): 213 f(f(f(x,f(x,x)),y),z) = f(z,f(f(u,f(u,u)),y)) # label(527C). [para(200(a,1),161(a,1))]. given #180 (T,wt=-981): 244 f(f(f(x,y),f(z,y)),f(f(u,z),f(y,z))) = f(y,z) # label(745A). [para(234(a,1),227(a,1,2,2)),rewrite(234(11))]. given #181 (A,wt=-29): 159 f(f(x,y),f(f(f(y,y),f(x,f(z,f(z,z)))),f(f(f(x,f(f(u,f(u,u)),x)),y),f(y,v)))) = y # label(583A). [para(94(a,2),104(a,1,2,1,2))]. given #182 (F,wt=-981): 256 f(x,f(f(y,f(f(z,x),f(z,u))),f(z,x))) = f(z,x) # label(559A). [para(240(a,1),234(a,1,2,2)),rewrite(250(11))]. given #183 (F,wt=-981): 257 f(f(f(x,y),f(z,x)),f(f(x,y),f(y,u))) = f(x,y) # label(674B). [para(235(a,1),240(a,1,2,1)),rewrite(235(11))]. given #184 (T,wt=-981): 270 f(f(f(f(x,f(x,x)),y),z),u) = f(u,f(z,f(y,y))) # label(732). [para(212(a,2),241(a,1,1)),rewrite(269(11))]. given #185 (T,wt=-981): 288 f(x,f(f(f(y,z),x),f(u,f(z,y)))) = f(f(y,z),x) # label(743). [para(285(a,1),246(a,1,2,1,1)),rewrite(285(12))]. given #186 (A,wt=-2): 160 f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,f(z,f(z,z)))),y),f(y,u)))) = y # label(583A). [para(117(a,1),104(a,1,2,2,1,1,2)),rewrite(124(6),124(8),124(8),124(10))]. given #187 (F,wt=-981): 296 f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),y)) = y # label(763). [para(290(a,1),234(a,1,2,2)),rewrite(291(14))]. given #188 (F,wt=-981): 299 f(f(x,x),f(f(y,x),f(f(x,x),z))) = f(f(x,x),z) # label(765). [para(187(a,1),292(a,1,2,1,2)),rewrite(126(8))]. given #189 (T,wt=-985): 313 f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z) # label(772). [para(18(a,1),299(a,1,1)),rewrite(57(5),57(8))]. given #190 (T,wt=-985): 316 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z) # label(775). [para(200(a,1),313(a,1,2,1))]. given #191 (A,wt=-475): 163 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(109(a,2),101(a,1,2,2))]. given #192 (F,wt=-985): 317 f(x,f(f(f(x,x),y),f(z,x))) = f(z,x) # label(776). [para(117(a,1),316(a,1,2,2)),rewrite(117(8))]. given #193 (F,wt=-985): 319 f(f(f(f(x,x),y),f(z,x)),x) = f(z,x) # label(779A). [para(317(a,1),200(a,1)),flip(a)]. given #194 (T,wt=-981): 308 f(f(f(x,y),f(f(z,u),y)),f(u,z)) = f(y,f(z,u)) # label(745). [para(219(a,1),244(a,1,2,1)),rewrite(285(10))]. given #195 (T,wt=-981): 312 f(f(x,f(f(y,f(y,y)),z)),u) = f(u,f(x,f(z,z))) # label(749). [para(200(a,1),270(a,1,1))]. given #196 (A,wt=-84): 164 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(92(a,2),106(a,1,2,1,2))]. given #197 (F,wt=-981): 315 f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y) # label(774). [para(200(a,1),299(a,1,2))]. given #198 (F,wt=-979): 215 f(f(x,y),f(f(z,f(z,z)),f(f(f(y,x),y),f(u,y)))) = y # label(627C). [para(200(a,1),151(a,1,2,2,1))]. given #199 (T,wt=-979): 217 f(f(x,y),f(f(f(y,y),x),f(f(f(x,y),y),f(y,z)))) = y # label(630C). [para(200(a,1),154(a,1,2,2,1))]. given #200 (T,wt=-979): 284 f(f(f(x,f(x,x)),f(y,f(z,u))),f(u,z)) = f(y,f(z,u)) # label(682A). [para(223(a,1),103(a,1,2))]. given #201 (A,wt=-21): 165 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(94(a,2),106(a,1,2,1,2))]. given #202 (F,wt=-979): 302 f(f(f(x,y),f(x,z)),f(f(u,f(x,u)),f(x,z))) = f(x,z) # label(761A). [para(292(a,1),239(a,1,1,2)),rewrite(292(13))]. given #203 (F,wt=-979): 321 f(f(x,y),f(f(f(y,y),z),f(f(y,f(x,y)),f(y,u)))) = y # label(781). [para(319(a,1),154(a,1,1)),rewrite(315(7),319(8))]. given #204 (T,wt=-979): 322 f(x,f(f(y,x),f(f(f(f(x,x),z),f(y,x)),u))) = f(y,x) # label(601B). [para(319(a,1),240(a,1,2,1)),rewrite(319(13))]. given #205 (T,wt=-979): 336 f(f(f(x,y),f(x,z)),f(f(f(x,u),u),f(x,z))) = f(x,z) # label(554A). [para(200(a,1),302(a,1,2,1))]. given #206 (A,wt=-481): 166 f(f(x,x),f(f(x,y),f(z,f(z,z)))) = f(x,f(x,x)) # label(577A). [para(94(a,2),110(a,1,2))]. given #207 (F,wt=-981): 343 f(f(f(f(x,y),z),y),f(f(f(f(x,y),u),u),y)) = y # label(555A). [para(18(a,1),336(a,1,1,2)),rewrite(18(9),18(11))]. given #208 (F,wt=-979): 337 f(f(x,x),f(f(f(x,x),y),f(f(z,f(z,z)),f(x,u)))) = x # label(783). [para(97(a,1),321(a,1,2,2,1))]. given #209 (T,wt=-983): 349 f(f(x,f(f(y,f(y,y)),f(z,u))),f(z,z)) = z # label(789A). [para(337(a,1),262(a,1)),flip(a)]. given #210 (T,wt=-983): 352 f(f(x,f(y,y)),f(f(z,y),f(z,y))) = f(z,y) # label(791). [para(233(a,1),349(a,1,1,2)),rewrite(67(6),67(7),67(10))]. given #211 (A,wt=-217): 167 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(161(a,1),101(a,1,2,2))]. given #212 (F,wt=-983): 355 f(f(f(x,y),f(x,y)),f(z,f(y,y))) = f(x,y) # label(794A). [para(352(a,1),200(a,1)),flip(a)]. given #213 (F,wt=-981): 354 f(f(x,y),f(f(z,f(y,y)),f(x,y))) = f(z,f(y,y)) # label(792). [para(352(a,1),148(a,1,1)),rewrite(352(9))]. given #214 (T,wt=-985): 360 f(f(x,f(y,x)),f(x,f(z,f(y,y)))) = x # label(798). [para(354(a,1),255(a,1,2,2))]. given #215 (T,wt=-985): 363 f(f(f(x,f(y,x)),f(y,y)),x) = f(x,x) # label(800A). [para(360(a,1),259(a,1,1)),flip(a)]. given #216 (A,wt=-35): 170 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(92(a,2),111(a,1,2,1,2))]. given #217 (F,wt=-979): 345 f(f(f(x,y),f(z,x)),f(f(f(x,u),u),f(z,x))) = f(z,x) # label(553A). [para(117(a,1),336(a,1,1,2)),rewrite(117(8),117(11))]. given #218 (F,wt=-979): 358 f(x,f(f(f(f(y,y),z),x),f(u,y))) = f(f(f(y,y),z),x) # label(796). [para(355(a,1),288(a,1,2,2))]. given #219 (T,wt=-981): 368 f(x,f(f(f(y,y),z),f(f(y,u),x))) = f(f(y,u),x) # label(817). [para(358(a,1),288(a,1,2))]. given #220 (T,wt=-981): 371 f(f(x,f(f(y,f(f(z,f(x,x)),y)),z)),z) = f(z,z) # label(822A). [para(296(a,1),368(a,1,2)),flip(a)]. given #221 (A,wt=-4): 172 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(94(a,2),111(a,1,2,1,2))]. given #222 (F,wt=-981): 372 f(f(f(x,f(f(y,f(z,z)),x)),y),z) = f(z,f(y,y)) # label(823A). [para(371(a,1),262(a,1,2)),flip(a)]. given #223 (F,wt=-979): 367 f(x,f(f(y,z),f(f(f(z,z),u),x))) = f(f(f(z,z),u),x) # label(510A). [para(200(a,1),358(a,1,2))]. given #224 (T,wt=-981): 376 f(x,f(f(y,f(x,x)),f(f(x,f(z,x)),x))) = f(z,x) # label(620B). [para(319(a,1),367(a,2)),rewrite(57(5))]. given #225 (T,wt=-979): 374 f(x,f(f(y,f(z,f(x,x))),f(y,f(z,f(x,x))))) = f(y,x) # label(826B). [para(264(a,1),372(a,1,1,1,2)),rewrite(199(8)),flip(a)]. given #226 (A,wt=-481): 176 f(f(f(x,f(x,x)),f(f(y,z),f(y,u))),f(y,y)) = y # label(626). [para(118(a,1),150(a,1,1,2,1))]. given #227 (F,wt=-983): 378 f(f(f(x,y),f(f(z,f(u,u)),y)),u) = f(y,u) # label(829B). [para(242(a,1),374(a,1,2,1)),rewrite(242(11),374(8)),flip(a)]. given #228 (F,wt=-983): 379 f(f(f(f(x,f(y,y)),z),f(u,z)),y) = f(z,y) # label(830B). [para(261(a,1),374(a,1,2,1)),rewrite(261(11),374(8)),flip(a)]. given #229 (T,wt=-977): 265 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(227(a,1),229(a,1,2,2)),rewrite(227(14))]. given #230 (T,wt=-985): 383 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)) # label(754). [para(24(a,1),265(a,1,1,1)),rewrite(57(4))]. given #231 (A,wt=-481): 178 f(f(x,x),f(f(y,f(y,y)),f(f(z,x),f(x,u)))) = x # label(529). [para(175(a,1),62(a,1,1,1)),rewrite(175(8),175(16))]. given #232 (F,wt=-977): 311 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(270(a,2),175(a,1)),rewrite(18(5))]. given #233 (F,wt=-981): 389 f(x,f(y,f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,x) # label(797). [para(311(a,1),355(a,1,1,1)),rewrite(311(10),57(3),99(17),311(16))]. given #234 (T,wt=-985): 392 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x # label(808). [para(270(a,2),389(a,1,2,2,1)),rewrite(18(6),57(5),57(9))]. given #235 (T,wt=-981): 396 f(f(f(x,f(x,x)),y),f(z,f(f(y,u),f(y,v)))) = y # label(529A). [para(92(a,2),392(a,1,1))]. given #236 (A,wt=-477): 179 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(18(a,1),177(a,1,2))]. given #237 (F,wt=-975): 325 f(f(x,y),f(f(f(f(x,y),f(x,y)),z),f(u,f(y,x)))) = f(u,f(y,x)) # label(558A). [para(308(a,1),317(a,1,2,2)),rewrite(308(15))]. given #238 (F,wt=-975): 370 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(270(a,1),368(a,1,2,2)),rewrite(99(7)),flip(a)]. given #239 (T,wt=-975): 395 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(392(a,1),60(a,1,2)),flip(a)]. given #240 (T,wt=-975): 400 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(392(a,1),378(a,1,1,2,1))]. given #241 (A,wt=-477): 181 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(18(a,1),151(a,1,2,2,1,2)),rewrite(67(3),152(4))]. given #242 (F,wt=-975): 401 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(392(a,1),379(a,1,1,1,1))]. given #243 (F,wt=-975): 413 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(401(a,1),200(a,1)),flip(a)]. ============================== PROOF ================================= % Proof 5 at 4.75 (+ 0.04) seconds: assoc. % Length of proof is 168. % Level of proof is 63. % Maximum clause weight is 19. % Given clauses 243. 5 f(z,f(f(y,x),f(y,x))) = f(x,f(f(y,z),f(y,z))) # answer(assoc). [goal]. 7 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). [assumption]. 12 f(c9,f(f(c10,c11),f(c10,c11))) != f(c11,f(f(c10,c9),f(c10,c9))) # answer(assoc). [deny(5)]. 15 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(7(a,1),7(a,1,2,2,2))]. 16 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(7(a,1),15(a,1,1,2)),rewrite(7(12),7(12),7(14),7(17),7(30))]. 17 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A). [para(7(a,1),16(a,1,2,2))]. 18 f(f(x,y),f(y,y)) = y # label(508B). [para(7(a,1),17(a,1,2,1))]. 19 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(18(a,1),7(a,1,2,1))]. 20 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(18(a,1),7(a,1,2,2,1,1,1,1))]. 21 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(18(a,1),7(a,1,2,2,1,1,1))]. 22 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(18(a,1),15(a,1,2,2,1,1,1,1))]. 23 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(18(a,1),15(a,1,2,2,1,1,1))]. 24 f(f(x,f(y,y)),y) = f(y,y) # label(508). [para(18(a,1),15(a,1,2,2,1)),rewrite(18(5),18(5))]. 26 f(f(f(x,x),y),x) = f(x,x) # label(510B). [para(17(a,1),18(a,1,1)),rewrite(17(7)),flip(a)]. 27 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511). [back_rewrite(19),rewrite(24(7))]. 28 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512). [para(26(a,1),7(a,1,2,2,1,1))]. 29 f(f(x,y),f(x,x)) = x # label(513). [para(18(a,1),26(a,1,1,1)),rewrite(18(6))]. 30 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(29(a,1),7(a,1,2,2,1,1))]. 31 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515). [para(7(a,1),29(a,1,1))]. 32 f(x,f(f(x,y),f(x,y))) = f(x,y) # label(516). [para(29(a,1),29(a,1,1))]. 33 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(31(a,1),7(a,1,2,2,2))]. 34 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(7(a,1),31(a,1,2,1)),rewrite(7(20),7(22))]. 35 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A). [para(27(a,1),26(a,1)),flip(a)]. 36 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520). [para(31(a,1),28(a,1,2,2,2))]. 37 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B). [para(35(a,1),18(a,1,1)),rewrite(35(9)),flip(a)]. 38 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(29(a,1),21(a,1,2,2,2))]. 39 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522). [para(7(a,1),37(a,1,2,2))]. 40 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523). [para(18(a,1),37(a,1,2,1)),rewrite(29(8))]. 41 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524). [para(29(a,1),37(a,1,2,2))]. 42 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525). [para(31(a,1),40(a,1,2,2))]. 43 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(18(a,1),36(a,1,1)),rewrite(29(3),29(5))]. 44 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(29(a,1),22(a,1,2,2,1,1))]. 45 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(43(a,1),31(a,1,2,1)),rewrite(43(18),29(11),43(18))]. 46 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(529). [para(45(a,1),21(a,1,2,2,1)),rewrite(24(3),31(8))]. 47 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x) # label(530). [para(18(a,1),46(a,1,1)),rewrite(29(4),29(5))]. 48 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). [para(46(a,1),23(a,1,1)),rewrite(29(16),29(18))]. 51 f(f(f(x,x),x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(532). [para(24(a,1),30(a,1,2,2,1)),rewrite(31(9))]. 52 f(f(f(x,x),x),f(x,f(f(x,x),y))) = x # label(535E). [para(30(a,1),23(a,1,2,2,1)),rewrite(29(3),31(6),18(6),47(7),29(4),31(7),18(7),29(10),31(13),18(13),18(21),40(21),24(17),29(3),29(3),31(6),18(6)),flip(a)]. 53 f(f(x,f(x,x)),f(f(x,x),f(x,y))) = f(x,x) # label(534F). [back_rewrite(48),rewrite(51(23),37(18),18(16)),flip(a)]. 54 f(f(f(x,x),x),f(x,f(y,f(x,x)))) = x # label(536). [para(31(a,1),52(a,1,2,2))]. 55 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(7(a,1),53(a,1,2,2))]. 56 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(29(a,1),53(a,1,2,2))]. 57 f(f(x,x),f(x,y)) = x # label(525). [para(37(a,1),38(a,1,1)),rewrite(53(16),29(13),24(11),29(3)),flip(a)]. 59 f(x,f(f(x,x),y)) = f(x,x) # label(541E). [para(40(a,1),38(a,1,1)),rewrite(57(10),57(12),52(14),18(10)),flip(a)]. 60 f(x,f(y,f(x,x))) = f(x,x) # label(542E). [para(42(a,1),38(a,1,1)),rewrite(57(10),57(12),54(14),18(10)),flip(a)]. 61 f(f(f(x,y),f(x,y)),y) = f(x,y) # label(543E). [para(39(a,1),38(a,1,1)),rewrite(55(26),57(23),24(18),57(7)),flip(a)]. 62 f(f(f(x,y),f(x,y)),x) = f(x,y) # label(544E). [para(41(a,1),38(a,1,1)),rewrite(56(26),57(23),24(18),57(7)),flip(a)]. 65 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(59(a,1),33(a,1,2,1)),rewrite(57(4),57(5),57(7))]. 67 f(f(x,x),f(y,x)) = x # label(548). [para(18(a,1),60(a,1,2,2)),rewrite(57(6))]. 68 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_rewrite(44),rewrite(67(3))]. 69 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_rewrite(20),rewrite(67(3))]. 70 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(61(a,1),7(a,1,1)),rewrite(31(7))]. 71 f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y)) = y # label(552). [para(31(a,1),65(a,1,2))]. 72 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(18(a,1),71(a,1,2,1,1,1)),rewrite(67(3))]. 73 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(29(a,1),71(a,1,2,1,1,1)),rewrite(57(3))]. 74 f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y)) = y # label(555). [para(31(a,1),71(a,1,2,1,1,1)),rewrite(61(4))]. 75 f(f(x,y),f(f(f(f(x,y),f(z,y)),f(z,y)),y)) = y # label(556). [para(31(a,1),74(a,1,2,1,1,2)),rewrite(31(8))]. 76 f(x,f(f(f(x,x),x),f(y,x))) = f(y,x) # label(557). [para(7(a,1),72(a,1,2,1,1,2)),rewrite(7(12))]. 77 f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x)))) = f(y,f(x,x)) # label(558). [para(24(a,1),72(a,1,2,1,1,2)),rewrite(57(4),24(4))]. 78 f(x,f(f(f(x,y),y),f(y,x))) = f(y,x) # label(559). [para(29(a,1),72(a,1,2,1,1,2)),rewrite(29(4))]. 79 f(x,f(f(f(x,x),x),f(x,y))) = f(x,y) # label(560). [para(62(a,1),76(a,1,2,2)),rewrite(62(9))]. 80 f(f(x,x),x) = f(x,f(x,x)) # label(561). [para(26(a,1),78(a,1,2,1)),rewrite(57(5))]. 81 f(x,f(f(x,f(x,x)),f(x,y))) = f(x,y) # label(562). [back_rewrite(79),rewrite(80(2))]. 82 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),y))) = f(f(x,x),y) # label(563). [para(18(a,1),81(a,1,2,1,2)),rewrite(80(3))]. 83 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(62(a,1),69(a,1,2,1))]. 84 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(26(a,1),83(a,1,2,2,1,1)),rewrite(57(7))]. 85 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(31(a,1),83(a,1,2,2,2))]. 86 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(45(a,1),84(a,1,2,2,2)),rewrite(29(17),45(14),61(7)),flip(a)]. 87 f(f(x,x),f(f(x,f(x,x)),f(x,y))) = f(x,f(x,x)) # label(568). [para(81(a,1),84(a,1,2,2))]. 88 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(29(a,1),87(a,1,2,2))]. 89 f(x,f(f(y,f(y,y)),f(y,f(y,y)))) = f(y,f(y,y)) # label(570C). [para(86(a,1),77(a,1,2,1)),rewrite(60(14),57(11)),flip(a)]. 92 f(f(x,f(x,x)),y) = f(y,y) # label(573). [para(89(a,1),26(a,1,1))]. 94 f(x,f(y,f(y,y))) = f(x,x) # label(575). [para(89(a,1),59(a,1,2))]. 95 f(f(x,x),f(y,f(y,y))) = x # label(594). [para(89(a,1),57(a,1,2))]. 96 f(f(x,x),f(f(x,f(x,x)),f(y,f(y,y)))) = f(y,f(y,y)) # label(576). [para(89(a,1),82(a,1,2,2)),rewrite(89(14))]. 97 f(x,f(x,x)) = f(y,f(y,y)) # label(577). [para(89(a,1),87(a,1,2,2)),rewrite(96(7))]. 99 f(f(x,y),f(f(z,f(z,z)),y)) = y # label(579). [para(92(a,2),18(a,1,2))]. 101 f(x,f(f(y,f(y,y)),f(z,x))) = f(z,x) # label(581). [para(92(a,2),31(a,1,2))]. 102 f(x,f(f(y,f(y,y)),f(x,z))) = f(x,z) # label(582). [para(92(a,2),32(a,1,2))]. 103 f(f(f(x,f(x,x)),y),f(y,z)) = y # label(583). [para(92(a,1),21(a,1,2,1,2)),rewrite(89(10),89(13),102(12))]. 105 f(f(f(x,f(x,x)),f(y,z)),z) = f(y,z) # label(586). [para(92(a,1),23(a,1,2,1,2)),rewrite(89(13),89(14),102(13))]. 107 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(92(a,2),33(a,1,2,2))]. 109 f(x,f(f(y,f(y,y)),z)) = f(x,f(z,z)) # label(589B). [para(92(a,2),77(a,2,2)),rewrite(101(7)),flip(a)]. 110 f(f(x,x),f(f(x,y),f(x,y))) = f(x,f(x,x)) # label(590). [para(92(a,1),87(a,1,2))]. 116 f(f(x,y),f(f(y,x),y)) = y # label(597). [para(94(a,1),71(a,1,2,1,1)),rewrite(95(7))]. 117 f(x,f(x,f(y,x))) = f(y,x) # label(598). [para(94(a,1),72(a,1,2,1,1)),rewrite(95(7))]. 118 f(x,f(x,f(x,y))) = f(x,y) # label(599). [para(94(a,1),73(a,1,2,1,1)),rewrite(95(7))]. 120 f(x,f(f(y,x),f(f(x,f(y,x)),f(f(y,x),z)))) = f(y,x) # label(601). [para(94(a,1),69(a,1,2,2,1,1,1)),rewrite(95(6),95(5))]. 126 f(f(x,f(y,f(y,y))),f(z,f(z,z))) = x # label(613). [para(94(a,2),95(a,1,1))]. 127 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(97(a,1),33(a,1,2,1)),rewrite(57(7),57(8))]. 128 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(97(a,1),34(a,1,1,1)),rewrite(57(6),57(7))]. 134 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(92(a,1),88(a,1,2))]. 142 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(118(a,1),116(a,1,1))]. 146 f(f(f(x,y),x),f(x,y)) = x # label(620). [para(103(a,1),68(a,1,2,1,1,1)),rewrite(103(6),110(6),103(9),101(9),103(9))]. 147 f(f(x,y),x) = f(x,f(x,y)) # label(623). [back_rewrite(142),rewrite(146(7))]. 150 f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,y)) = y # label(626). [back_rewrite(128),rewrite(147(4),147(5),118(5),147(4))]. 151 f(f(x,y),f(f(z,f(z,z)),f(f(y,f(y,x)),f(u,y)))) = y # label(627). [back_rewrite(127),rewrite(147(5),147(6),118(6),147(5))]. 152 f(f(x,y),y) = f(y,f(x,y)) # label(628B). [para(7(a,1),147(a,1,1)),rewrite(7(14)),flip(a)]. 153 f(f(x,y),f(y,f(x,y))) = y # label(629). [para(147(a,1),75(a,1,2,1,1)),rewrite(152(2),152(5),147(8),117(8),147(5),117(5),152(4))]. 154 f(f(x,y),f(f(f(y,y),x),f(f(y,f(x,y)),f(y,z)))) = y # label(630). [para(147(a,1),70(a,1,2,2,1,1,1)),rewrite(147(6),118(6),152(5))]. 156 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_rewrite(107),rewrite(152(8))]. 157 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_rewrite(85),rewrite(152(3))]. 168 f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z)))) = x # label(640). [para(153(a,1),120(a,1,2,1)),rewrite(153(8),147(5),117(5),153(7),153(11))]. 175 f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z)) = z # label(644). [para(117(a,1),150(a,1,1,2,1))]. 177 f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z)) = z # label(646). [para(31(a,1),175(a,1,1,2,2))]. 180 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(177(a,1),57(a,1,2)),rewrite(99(13))]. 183 f(f(x,f(x,y)),f(y,x)) = x # label(652A). [para(151(a,1),101(a,1)),flip(a)]. 184 f(f(x,x),f(f(y,x),f(x,z))) = f(x,f(x,x)) # label(658). [para(175(a,1),134(a,1,1,1)),rewrite(175(8),99(14),175(13),175(13),175(13))]. 187 f(f(x,x),f(f(y,x),f(z,f(z,z)))) = f(x,f(x,x)) # label(660). [para(97(a,1),184(a,1,2,2))]. 190 f(f(f(x,y),f(z,y)),y) = f(y,f(f(x,y),f(z,y))) # label(664B). [para(180(a,1),31(a,1,2,1)),rewrite(103(11)),flip(a)]. 192 f(f(x,y),f(y,f(f(z,y),f(x,y)))) = f(f(z,y),f(x,y)) # label(666). [para(180(a,2),101(a,1,2)),rewrite(190(5))]. 193 f(x,f(f(x,y),f(f(z,f(x,y)),x))) = f(f(z,f(x,y)),x) # label(669). [para(57(a,1),192(a,1,1)),rewrite(57(6),57(11))]. 194 f(f(x,y),f(x,f(f(z,x),f(x,y)))) = f(f(z,x),f(x,y)) # label(667). [para(62(a,1),192(a,1,1)),rewrite(62(6),62(11))]. 195 f(f(x,y),f(y,f(f(y,z),f(x,y)))) = f(f(y,z),f(x,y)) # label(668). [para(62(a,1),192(a,1,2,2,1)),rewrite(62(10))]. 196 f(x,f(f(x,y),f(y,x))) = f(y,x) # label(670). [para(67(a,1),193(a,1,2,2,1)),rewrite(67(7))]. 197 f(f(x,y),f(y,x)) = f(f(y,x),f(y,x)) # label(671A). [para(196(a,1),195(a,1,2)),flip(a)]. 198 f(f(x,f(y,z)),f(f(z,y),f(y,z))) = f(y,z) # label(672). [para(197(a,2),18(a,1,2))]. 199 f(f(x,f(y,x)),f(x,y)) = x # label(673). [para(197(a,1),168(a,1,2,2)),rewrite(32(6))]. 200 f(x,y) = f(y,x) # label(933C). [para(197(a,1),197(a,1,1)),rewrite(57(7),198(8))]. 202 f(x,f(f(y,x),f(y,f(z,f(y,x))))) = f(y,x) # label(676). [back_rewrite(157),rewrite(199(5))]. 212 f(f(f(x,f(x,x)),y),z) = f(z,f(y,y)) # label(679). [para(200(a,1),109(a,1))]. 223 f(f(x,f(y,z)),f(f(y,z),f(z,y))) = f(z,y) # label(686). [para(200(a,1),198(a,1,1,2))]. 227 f(x,f(f(y,z),f(z,x))) = f(z,x) # label(689). [para(194(a,1),202(a,1,2))]. 233 f(f(x,y),f(f(z,f(y,f(y,x))),y)) = y # label(695). [para(183(a,1),227(a,1,2,2)),rewrite(183(10))]. 234 f(x,f(f(y,z),f(x,z))) = f(z,x) # label(696). [para(200(a,1),227(a,1,2,2))]. 235 f(x,f(f(y,x),f(z,y))) = f(y,x) # label(697). [para(200(a,1),227(a,1,2))]. 241 f(f(x,y),z) = f(z,f(y,f(z,f(x,y)))) # label(703A). [para(67(a,1),234(a,1,2,1)),flip(a)]. 242 f(f(f(x,y),f(z,y)),z) = f(y,z) # label(704A). [para(234(a,1),200(a,1)),flip(a)]. 243 f(x,f(f(x,y),f(z,y))) = f(y,x) # label(705). [para(200(a,1),234(a,1,2))]. 246 f(x,f(f(f(y,z),x),z)) = f(f(y,z),x) # label(708). [para(67(a,1),235(a,1,2,2))]. 261 f(f(f(x,y),f(z,y)),x) = f(y,x) # label(725). [para(200(a,1),242(a,1,1))]. 262 f(x,f(f(x,f(y,z)),z)) = f(f(y,z),x) # label(726). [para(67(a,1),243(a,1,2,2))]. 264 f(f(f(x,f(y,z)),z),x) = f(f(y,z),x) # label(728). [para(67(a,1),261(a,1,1,2))]. 269 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)) # label(731). [para(241(a,1),200(a,1))]. 270 f(f(f(f(x,f(x,x)),y),z),u) = f(u,f(z,f(y,y))) # label(732). [para(212(a,2),241(a,1,1)),rewrite(269(11))]. 278 f(f(x,f(y,f(z,x))),y) = f(y,f(z,x)) # label(736A). [para(269(a,1),200(a,1)),flip(a)]. 285 f(f(f(x,y),f(y,x)),f(z,f(x,y))) = f(y,x) # label(740A). [para(223(a,1),200(a,1)),flip(a)]. 288 f(x,f(f(f(y,z),x),f(u,f(z,y)))) = f(f(y,z),x) # label(743). [para(285(a,1),246(a,1,2,1,1)),rewrite(285(12))]. 290 f(f(x,y),f(f(z,f(f(y,x),z)),y)) = y # label(759). [para(156(a,1),269(a,1,2,2)),rewrite(105(9),156(18))]. 291 f(f(f(x,f(f(y,z),x)),y),f(z,y)) = y # label(760). [para(156(a,1),278(a,1,1,2)),rewrite(105(8),156(18))]. 292 f(x,f(f(y,f(x,y)),f(x,z))) = f(x,z) # label(761). [para(29(a,1),290(a,1,2,1,2,1)),rewrite(57(3))]. 296 f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),y)) = y # label(763). [para(290(a,1),234(a,1,2,2)),rewrite(291(14))]. 299 f(f(x,x),f(f(y,x),f(f(x,x),z))) = f(f(x,x),z) # label(765). [para(187(a,1),292(a,1,2,1,2)),rewrite(126(8))]. 311 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(270(a,2),175(a,1)),rewrite(18(5))]. 313 f(x,f(f(y,f(x,x)),f(x,z))) = f(x,z) # label(772). [para(18(a,1),299(a,1,1)),rewrite(57(5),57(8))]. 315 f(f(x,x),f(f(f(x,x),y),f(z,x))) = f(f(x,x),y) # label(774). [para(200(a,1),299(a,1,2))]. 316 f(x,f(f(f(x,x),y),f(x,z))) = f(x,z) # label(775). [para(200(a,1),313(a,1,2,1))]. 317 f(x,f(f(f(x,x),y),f(z,x))) = f(z,x) # label(776). [para(117(a,1),316(a,1,2,2)),rewrite(117(8))]. 319 f(f(f(f(x,x),y),f(z,x)),x) = f(z,x) # label(779A). [para(317(a,1),200(a,1)),flip(a)]. 321 f(f(x,y),f(f(f(y,y),z),f(f(y,f(x,y)),f(y,u)))) = y # label(781). [para(319(a,1),154(a,1,1)),rewrite(315(7),319(8))]. 337 f(f(x,x),f(f(f(x,x),y),f(f(z,f(z,z)),f(x,u)))) = x # label(783). [para(97(a,1),321(a,1,2,2,1))]. 349 f(f(x,f(f(y,f(y,y)),f(z,u))),f(z,z)) = z # label(789A). [para(337(a,1),262(a,1)),flip(a)]. 352 f(f(x,f(y,y)),f(f(z,y),f(z,y))) = f(z,y) # label(791). [para(233(a,1),349(a,1,1,2)),rewrite(67(6),67(7),67(10))]. 355 f(f(f(x,y),f(x,y)),f(z,f(y,y))) = f(x,y) # label(794A). [para(352(a,1),200(a,1)),flip(a)]. 358 f(x,f(f(f(f(y,y),z),x),f(u,y))) = f(f(f(y,y),z),x) # label(796). [para(355(a,1),288(a,1,2,2))]. 368 f(x,f(f(f(y,y),z),f(f(y,u),x))) = f(f(y,u),x) # label(817). [para(358(a,1),288(a,1,2))]. 371 f(f(x,f(f(y,f(f(z,f(x,x)),y)),z)),z) = f(z,z) # label(822A). [para(296(a,1),368(a,1,2)),flip(a)]. 372 f(f(f(x,f(f(y,f(z,z)),x)),y),z) = f(z,f(y,y)) # label(823A). [para(371(a,1),262(a,1,2)),flip(a)]. 374 f(x,f(f(y,f(z,f(x,x))),f(y,f(z,f(x,x))))) = f(y,x) # label(826B). [para(264(a,1),372(a,1,1,1,2)),rewrite(199(8)),flip(a)]. 378 f(f(f(x,y),f(f(z,f(u,u)),y)),u) = f(y,u) # label(829B). [para(242(a,1),374(a,1,2,1)),rewrite(242(11),374(8)),flip(a)]. 379 f(f(f(f(x,f(y,y)),z),f(u,z)),y) = f(z,y) # label(830B). [para(261(a,1),374(a,1,2,1)),rewrite(261(11),374(8)),flip(a)]. 389 f(x,f(y,f(f(z,f(x,x)),f(f(x,x),u)))) = f(x,x) # label(797). [para(311(a,1),355(a,1,1,1)),rewrite(311(10),57(3),99(17),311(16))]. 392 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x # label(808). [para(270(a,2),389(a,1,2,2,1)),rewrite(18(6),57(5),57(9))]. 400 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(392(a,1),378(a,1,1,2,1))]. 401 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(392(a,1),379(a,1,1,1,1))]. 413 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(401(a,1),200(a,1)),flip(a)]. 415 f(x,f(f(y,z),f(y,z))) = f(z,f(f(y,x),f(y,x))) # label(872). [para(413(a,1),400(a,1))]. 416 $F # answer(assoc). [resolve(415,a,12,a)]. ============================== end of proof ========================== % Disable descendants: 12 given #244 (T,wt=-981): 415 f(x,f(f(y,z),f(y,z))) = f(z,f(f(y,x),f(y,x))) # label(872). [para(413(a,1),400(a,1))]. given #245 (T,wt=-981): 418 f(f(f(x,y),f(x,y)),z) = f(y,f(f(x,z),f(x,z))) # label(870). [para(415(a,1),200(a,1)),flip(a)]. given #246 (A,wt=-227): 182 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(29(a,1),151(a,1,2,2,1,2)),rewrite(57(3),147(4))]. given #247 (F,wt=-975): 414 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(413(a,2),200(a,1))]. given #248 (F,wt=-975): 423 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(200(a,1),414(a,1,2))]. given #249 (T,wt=-973): 185 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(57(a,1),184(a,1,2,1))]. given #250 (T,wt=-973): 338 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(148(a,1),321(a,1,2,2,1))]. given #251 (A,wt=-483): 186 f(f(x,x),f(f(x,y),f(x,z))) = f(x,f(x,x)) # label(590). [para(62(a,1),184(a,1,2,1))]. given #252 (F,wt=-979): 425 f(f(f(x,y),y),f(f(f(y,y),z),f(f(x,y),f(y,u)))) = y # label(532A). [para(18(a,1),338(a,1,1,2)),rewrite(18(5),18(5),18(8),18(12))]. given #253 (F,wt=-971): 364 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(363(a,1),100(a,1,1))]. given #254 (T,wt=-969): 232 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(161(a,1),227(a,1,2,2))]. given #255 (T,wt=-969): 394 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(392(a,1),18(a,1,1))]. given #256 (A,wt=-227): 188 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(97(a,1),173(a,1,2,1))]. given #257 (F,wt=-969): 424 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(418(a,1),423(a,1,2,1))]. given #258 (F,wt=-959): 375 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(276(a,1),372(a,1,1,1,2))]. given #259 (T,wt=-967): 441 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(200(a,1),375(a,1,1,1)),rewrite(118(6))]. given #260 (T,wt=-981): 442 f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x) = f(z,x) # label(827). [para(308(a,1),441(a,1,1,2)),rewrite(308(15),308(18),374(15))]. given #261 (A,wt=-102): 191 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(180(a,1),60(a,1,2))]. given #262 (F,wt=-981): 447 f(f(f(f(x,x),y),f(z,f(f(x,x),y))),x) = f(z,x) # label(828C). [back_rewrite(441),rewrite(444(15))]. given #263 (F,wt=-983): 452 f(f(f(x,y),f(x,f(f(z,z),u))),z) = f(x,z) # label(836B). [para(239(a,1),447(a,1,1,2)),rewrite(447(7)),flip(a)]. given #264 (T,wt=-983): 454 f(x,f(f(y,z),f(y,f(f(x,x),u)))) = f(y,x) # label(838A). [para(452(a,1),200(a,1)),flip(a)]. given #265 (T,wt=-983): 455 f(x,f(f(y,f(f(x,x),z)),f(y,u))) = f(y,x) # label(839). [para(452(a,1),308(a,1,1,2)),rewrite(400(9),454(12))]. given #266 (A,wt=-489): 204 f(f(x,x),x) = f(y,f(y,y)) # label(561). [para(200(a,1),97(a,1))]. given #267 (F,wt=-981): 453 f(f(f(x,y),f(x,f(z,u))),f(z,z)) = f(x,f(z,z)) # label(837). [para(18(a,1),452(a,1,1,2,2,1))]. given #268 (F,wt=-983): 465 f(f(f(x,y),f(x,f(f(x,z),u))),z) = f(z,x) # label(921). [para(234(a,1),453(a,2)),rewrite(414(9))]. given #269 (T,wt=-981): 461 f(f(x,x),f(f(y,f(z,x)),f(y,u))) = f(y,f(x,x)) # label(846). [para(352(a,1),455(a,1,2,1,2))]. given #270 (T,wt=-981): 467 f(f(x,x),f(f(y,z),f(z,f(u,x)))) = f(z,f(x,x)) # label(848). [para(228(a,1),461(a,1,2))]. given #271 (A,wt=-489): 206 f(f(x,y),f(f(x,y),x)) = x # label(629E). [para(200(a,1),148(a,1,2))]. given #272 (F,wt=-985): 470 f(f(x,f(y,f(x,z))),f(f(x,z),x)) = x # label(624A). [para(206(a,1),261(a,2)),rewrite(279(4))]. given #273 (F,wt=-981): 468 f(f(x,x),f(f(y,z),f(z,f(u,x)))) = f(f(x,x),z) # label(850). [para(467(a,2),200(a,1))]. given #274 (T,wt=-979): 472 f(f(x,x),f(f(y,f(y,y)),f(f(z,x),u))) = f(f(x,x),u) # label(852). [para(219(a,2),468(a,1,2))]. given #275 (T,wt=-983): 476 f(f(x,f(y,x)),f(y,y)) = f(f(x,x),f(y,y)) # label(855A). [para(364(a,1),472(a,2)),rewrite(472(14),474(9)),flip(a)]. given #276 (A,wt=-485): 207 f(x,f(f(f(y,y),y),f(z,x))) = f(z,x) # label(557). [para(200(a,1),101(a,1,2,1))]. given #277 (F,wt=-981): 477 f(f(x,f(f(f(y,f(y,y)),z),x)),z) = f(f(x,x),z) # label(856). [para(99(a,1),476(a,1,2)),rewrite(99(14))]. given #278 (F,wt=-979): 474 f(f(x,x),f(f(y,f(y,y)),f(f(x,z),u))) = f(f(x,x),u) # label(853). [para(200(a,1),472(a,1,2,2,1))]. given #279 (T,wt=-979): 475 f(f(x,x),f(y,f(f(z,x),f(y,u)))) = f(f(x,x),f(y,u)) # label(854B). [para(383(a,1),472(a,1,2,2)),rewrite(472(8)),flip(a)]. given #280 (T,wt=-977): 448 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(18(a,1),191(a,1,2,1,2))]. given #281 (A,wt=-489): 208 f(f(x,y),f(f(y,x),y)) = y # label(597). [para(200(a,1),149(a,1,2))]. given #282 (F,wt=-977): 462 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(204(a,2),181(a,1,2,2,1))]. given #283 (F,wt=-985): 486 f(f(x,x),y) = f(y,f(f(f(z,z),z),x)) # label(560A). [para(462(a,1),312(a,1,1)),rewrite(457(14))]. given #284 (T,wt=-975): 478 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(465(a,1),477(a,1,1,2))]. given #285 (T,wt=-979): 489 f(x,f(f(y,y),f(x,f(f(x,y),z)))) = f(x,f(f(x,y),z)) # label(924). [para(478(a,1),300(a,1,2))]. given #286 (A,wt=-489): 216 f(f(f(x,y),x),f(y,x)) = x # label(617). [para(200(a,1),183(a,1,1))]. given #287 (F,wt=-983): 492 f(f(x,y),f(f(f(f(y,x),f(y,x)),z),y)) = y # label(597A). [para(216(a,1),368(a,1,2,2)),rewrite(216(11))]. given #288 (F,wt=-981): 491 f(x,f(f(y,y),f(x,z))) = f(x,f(f(x,y),f(x,z))) # label(926). [para(475(a,1),489(a,1,2))]. given #289 (T,wt=-981): 494 f(f(f(x,y),f(x,z)),x) = f(x,f(f(y,y),f(x,z))) # label(928A). [para(491(a,2),200(a,1)),flip(a)]. given #290 (T,wt=-981): 495 f(x,f(f(x,y),f(z,z))) = f(x,f(f(x,z),f(x,y))) # label(929). [para(200(a,1),491(a,1,2))]. given #291 (A,wt=-100): 221 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(212(a,2),105(a,1))]. given #292 (F,wt=-981): 496 f(x,f(f(x,y),f(x,f(z,z)))) = f(x,f(f(x,y),z)) # label(930B). [para(312(a,1),495(a,2,2)),rewrite(99(8)),flip(a)]. given #293 (F,wt=-981): 497 f(f(f(x,y),z),x) = f(x,f(f(y,y),f(x,f(z,z)))) # label(931). [para(496(a,1),211(a,1,1,2)),rewrite(211(7),494(8))]. given #294 (T,wt=-981): 498 f(f(x,f(y,f(z,z))),y) = f(y,f(z,f(y,f(x,x)))) # label(932). [para(312(a,1),497(a,1,1)),rewrite(99(11))]. ============================== PROOF ================================= % Proof 6 at 8.03 (+ 0.06) seconds: mod. % Length of proof is 223. % Level of proof is 81. % Maximum clause weight is 19. % Given clauses 294. 6 f(x,f(z,f(x,f(y,y)))) = f(x,f(y,f(x,f(z,z)))) # answer(mod). [goal]. 7 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). [assumption]. 13 f(c12,f(c13,f(c12,f(c14,c14)))) != f(c12,f(c14,f(c12,f(c13,c13)))) # answer(mod). [deny(6)]. 14 f(c12,f(c14,f(c12,f(c13,c13)))) != f(c12,f(c13,f(c12,f(c14,c14)))) # answer(mod). [copy(13),flip(a)]. 15 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(7(a,1),7(a,1,2,2,2))]. 16 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(7(a,1),15(a,1,1,2)),rewrite(7(12),7(12),7(14),7(17),7(30))]. 17 f(f(x,y),f(f(f(y,y),z),y)) = y # label(508A). [para(7(a,1),16(a,1,2,2))]. 18 f(f(x,y),f(y,y)) = y # label(508B). [para(7(a,1),17(a,1,2,1))]. 19 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(18(a,1),7(a,1,2,1))]. 20 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(18(a,1),7(a,1,2,2,1,1,1,1))]. 21 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(18(a,1),7(a,1,2,2,1,1,1))]. 22 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(18(a,1),15(a,1,2,2,1,1,1,1))]. 23 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(18(a,1),15(a,1,2,2,1,1,1))]. 24 f(f(x,f(y,y)),y) = f(y,y) # label(508). [para(18(a,1),15(a,1,2,2,1)),rewrite(18(5),18(5))]. 26 f(f(f(x,x),y),x) = f(x,x) # label(510B). [para(17(a,1),18(a,1,1)),rewrite(17(7)),flip(a)]. 27 f(f(x,y),f(y,f(f(y,y),f(y,z)))) = y # label(511). [back_rewrite(19),rewrite(24(7))]. 28 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))) = x # label(512). [para(26(a,1),7(a,1,2,2,1,1))]. 29 f(f(x,y),f(x,x)) = x # label(513). [para(18(a,1),26(a,1,1,1)),rewrite(18(6))]. 30 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(29(a,1),7(a,1,2,2,1,1))]. 31 f(x,f(f(y,x),f(y,x))) = f(y,x) # label(515). [para(7(a,1),29(a,1,1))]. 32 f(x,f(f(x,y),f(x,y))) = f(x,y) # label(516). [para(29(a,1),29(a,1,1))]. 33 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(31(a,1),7(a,1,2,2,2))]. 34 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(7(a,1),31(a,1,2,1)),rewrite(7(20),7(22))]. 35 f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y)))) = x # label(519A). [para(27(a,1),26(a,1)),flip(a)]. 36 f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x)))) = x # label(520). [para(31(a,1),28(a,1,2,2,2))]. 37 f(x,f(f(x,x),f(x,y))) = f(x,x) # label(521B). [para(35(a,1),18(a,1,1)),rewrite(35(9)),flip(a)]. 38 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(29(a,1),21(a,1,2,2,2))]. 39 f(f(x,y),f(f(f(x,y),f(x,y)),y)) = f(f(x,y),f(x,y)) # label(522). [para(7(a,1),37(a,1,2,2))]. 40 f(f(x,x),f(x,f(f(x,x),y))) = x # label(523). [para(18(a,1),37(a,1,2,1)),rewrite(29(8))]. 41 f(f(x,y),f(f(f(x,y),f(x,y)),x)) = f(f(x,y),f(x,y)) # label(524). [para(29(a,1),37(a,1,2,2))]. 42 f(f(x,x),f(x,f(y,f(x,x)))) = x # label(525). [para(31(a,1),40(a,1,2,2))]. 43 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(18(a,1),36(a,1,1)),rewrite(29(3),29(5))]. 44 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(29(a,1),22(a,1,2,2,1,1))]. 45 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(43(a,1),31(a,1,2,1)),rewrite(43(18),29(11),43(18))]. 46 f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y)))) = x # label(529). [para(45(a,1),21(a,1,2,2,1)),rewrite(24(3),31(8))]. 47 f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))) = f(x,x) # label(530). [para(18(a,1),46(a,1,1)),rewrite(29(4),29(5))]. 48 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). [para(46(a,1),23(a,1,1)),rewrite(29(16),29(18))]. 51 f(f(f(x,x),