----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 13.60 sec ----> 2610 [binary,2609.1,2.1] $F. Length of proof is 93. Level of proof is 25. ---------------- PROOF ---------------- 1 [] f(f(X,f(f(Y,X),X)),f(Y,f(Z,X)))!=Y. 2 [] x=x. 4,3 [] f(f(f(x,f(y,x)),x),f(y,f(z,x)))=y. 6,5 [para_into,3.1.1.1.1.2,3.1.1] f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),f(u,f(x,f(y,z)))))=f(f(z,f(x,z)),z). 8,7 [para_into,3.1.1.1.1,3.1.1] f(f(x,f(f(y,f(x,y)),y)),f(x,f(z,f(f(y,f(x,y)),y))))=x. 10,9 [para_into,3.1.1.2.2,3.1.1] f(f(f(f(x,f(y,z)),f(u,f(x,f(y,z)))),f(x,f(y,z))),f(u,x))=u. 11 [para_into,3.1.1.2,3.1.1] f(f(f(f(x,y),f(f(f(y,f(z,y)),y),f(x,y))),f(x,y)),z)=f(f(y,f(z,y)),y). 13 [para_into,7.1.1.1.2.1,7.1.1,demod,8] f(f(x,f(x,f(x,f(f(y,f(x,y)),y)))),f(x,f(z,f(x,f(x,f(f(y,f(x,y)),y))))))=x. 19 [para_into,7.1.1.2,3.1.1] f(f(f(f(x,f(y,x)),x),f(f(x,f(f(f(x,f(y,x)),x),x)),x)),y)=f(f(x,f(y,x)),x). 22,21 [para_into,9.1.1.1.1.1.2,9.1.1,demod,10,10] f(f(f(f(x,y),f(z,f(x,y))),f(x,y)),f(z,x))=z. 25 [para_into,9.1.1.1.1.1,7.1.1,demod,8,8] f(f(f(x,f(y,x)),x),f(y,f(x,f(f(z,f(x,z)),z))))=y. 27 [para_into,9.1.1.1.1.1,3.1.1,demod,4,4] f(f(f(x,f(y,x)),x),f(y,f(f(z,f(x,z)),z)))=y. 31 [para_into,9.1.1.1.1.2,3.1.1] f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),x))=f(f(z,f(x,z)),z). 33 [para_into,9.1.1.1.1,7.1.1] f(f(x,f(x,f(f(y,f(x,y)),y))),f(x,x))=x. 39 [para_into,33.1.1.1.2.2.1,3.1.1] f(f(x,f(x,f(x,f(f(y,f(x,y)),y)))),f(x,x))=x. 41 [para_from,33.1.1,3.1.1.2] f(f(f(x,f(f(x,f(x,f(f(y,f(x,y)),y))),x)),x),x)=f(x,f(x,f(f(y,f(x,y)),y))). 48,47 [para_into,5.1.1.1,3.1.1] f(x,f(f(f(x,f(x,x)),x),f(y,f(x,f(x,x)))))=f(f(x,f(x,x)),x). 51 [para_into,21.1.1.1.1.1,5.1.1,demod,6,6] f(f(f(f(f(x,f(y,x)),x),f(z,f(f(x,f(y,x)),x))),f(f(x,f(y,x)),x)),f(z,f(f(f(y,f(u,x)),y),f(y,f(u,x)))))=z. 53 [para_into,21.1.1.1.1.2,33.1.1] f(f(f(f(x,x),x),f(x,x)),f(f(x,f(x,f(f(y,f(x,y)),y))),x))=f(x,f(x,f(f(y,f(x,y)),y))). 59 [para_into,21.1.1.1.1,3.1.1] f(f(x,f(f(y,f(x,y)),y)),f(x,f(y,f(x,y))))=x. 67 [para_from,21.1.1,5.1.1.2.2.2.2,demod,22,22] f(f(f(f(x,y),x),f(x,y)),f(f(f(f(y,z),f(x,f(y,z))),f(y,z)),f(u,f(x,y))))=f(f(f(y,z),f(x,f(y,z))),f(y,z)). 69 [para_from,21.1.1,3.1.1.2] f(f(f(x,f(f(f(f(x,y),f(z,f(x,y))),f(x,y)),x)),x),z)=f(f(f(x,y),f(z,f(x,y))),f(x,y)). 81 [para_into,27.1.1.1.1,3.1.1] f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(z,f(f(f(y,f(x,y)),y),z)),z)))=x. 94,93 [para_into,39.1.1.1.2.2.2.1,7.1.1] f(f(x,f(x,f(x,f(x,f(x,f(f(y,f(x,y)),y)))))),f(x,x))=x. 109 [para_from,59.1.1,3.1.1.2] f(f(f(f(x,f(y,x)),f(f(y,f(f(x,f(y,x)),x)),f(x,f(y,x)))),f(x,f(y,x))),y)=f(y,f(f(x,f(y,x)),x)). 127 [para_into,25.1.1.2,7.1.1] f(f(f(x,f(f(x,f(f(y,f(x,y)),y)),x)),x),x)=f(x,f(f(y,f(x,y)),y)). 129 [para_into,25.1.1.2,3.1.1] f(f(f(x,f(f(f(y,f(x,y)),y),x)),x),x)=f(f(y,f(x,y)),y). 157 [para_from,93.1.1,21.1.1.1.2,demod,94,94] f(f(f(x,f(y,x)),x),f(y,f(x,f(x,f(x,f(x,f(x,f(f(z,f(x,z)),z))))))))=y. 192,191 [para_into,47.1.1.2.2,21.1.1] f(x,f(f(f(x,f(x,x)),x),x))=f(f(x,f(x,x)),x). 194,193 [para_from,47.1.1,25.1.1.2,demod,4] f(f(x,f(f(x,f(x,x)),x)),f(f(x,f(x,x)),x))=x. 197 [para_from,47.1.1,21.1.1.1.2,demod,48,48] f(f(f(f(f(x,f(x,x)),x),f(y,f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(y,x))=y. 204,203 [para_from,191.1.1,129.1.1.1.1] f(f(f(f(x,f(x,x)),x),x),x)=f(f(x,f(x,x)),x). 236,235 [para_from,191.1.1,3.1.1.2] f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))=x. 243 [para_from,191.1.1,27.1.1.1.1.2] f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),x)),f(x,f(f(y,f(f(f(f(x,f(x,x)),x),x),y)),y)))=x. 245 [para_from,191.1.1,3.1.1.1.1.2] f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),x)),f(x,f(y,f(f(f(x,f(x,x)),x),x))))=x. 258,257 [para_from,235.1.1,21.1.1.1.1.2,demod,4] f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),x)=f(f(x,f(x,x)),x). 259 [para_from,235.1.1,7.1.1.2.2] f(f(x,f(f(x,f(x,x)),x)),f(x,x))=x. 263 [para_from,235.1.1,5.1.1.2.2.2,demod,236,236,192,192] f(f(f(x,f(f(x,f(x,x)),x)),x),f(f(f(f(x,f(x,x)),x),x),f(y,x)))=f(f(f(x,f(x,x)),x),x). 275 [para_from,259.1.1,21.1.1.1.1.2] f(f(f(f(x,x),x),f(x,x)),f(f(x,f(f(x,f(x,x)),x)),x))=f(x,f(f(x,f(x,x)),x)). 299 [para_from,203.1.1,11.1.1.1.1.2.1.1.2,demod,204] f(f(f(f(x,y),f(f(f(y,f(f(y,f(y,y)),y)),y),f(x,y))),f(x,y)),f(f(f(y,f(y,y)),y),y))=f(f(y,f(f(y,f(y,y)),y)),y). 319 [para_into,19.1.1.1.1.1,27.1.1,demod,4,194,4] f(f(f(x,f(f(x,f(x,x)),x)),f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x))),x)=f(x,f(f(x,f(x,x)),x)). 345 [para_into,81.1.1.2.2.1.2,21.1.1] f(f(x,f(f(f(y,z),f(x,f(y,z))),f(y,z))),f(x,f(f(f(x,y),x),f(x,y))))=x. 378,377 [para_into,31.1.1.1.1.1,191.1.1,demod,192] f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),x))=f(f(x,f(x,x)),x). 381 [back_demod,245,demod,378] f(f(f(x,f(x,x)),x),f(x,f(y,f(f(f(x,f(x,x)),x),x))))=x. 383 [back_demod,243,demod,378] f(f(f(x,f(x,x)),x),f(x,f(f(y,f(f(f(f(x,f(x,x)),x),x),y)),y)))=x. 387 [para_into,381.1.1.2.2,127.1.1] f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(y,f(f(f(f(x,f(x,x)),x),x),y)),y))))=x. 395 [para_into,157.1.1.2.2.2.2.2.2.2.1,13.1.1] f(f(f(x,f(y,x)),x),f(y,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(z,f(x,z)),z))))))))))))=y. 425 [para_into,345.1.1.2.2,3.1.1] f(f(x,f(f(f(f(x,x),y),f(x,f(f(x,x),y))),f(f(x,x),y))),f(x,x))=x. 433 [para_into,425.1.1.1.2.1.1.1,235.1.1,demod,236,236,236] f(f(f(f(x,f(x,x)),x),f(f(f(x,y),f(f(f(x,f(x,x)),x),f(x,y))),f(x,y))),x)=f(f(x,f(x,x)),x). 466,465 [para_into,197.1.1.1.1.2,193.1.1] f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(x,f(x,x)),x)),x))=f(x,f(f(x,f(x,x)),x)). 469 [para_from,275.1.1,3.1.1.2] f(f(f(x,f(f(f(f(x,x),x),f(x,x)),x)),x),f(x,f(f(x,f(x,x)),x)))=f(f(f(x,x),x),f(x,x)). 498,497 [para_into,69.1.1.1.1.2,11.1.1] f(f(f(x,f(f(y,f(x,y)),y)),x),f(f(y,f(x,y)),y))=f(f(f(x,y),f(f(f(y,f(x,y)),y),f(x,y))),f(x,y)). 524,523 [para_from,263.1.1,383.1.1.2.2.1] f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x))))=x. 531 [para_into,67.1.1.2,51.1.1,demod,4,4,498,236] f(f(f(x,x),f(f(f(x,f(x,x)),x),f(x,x))),f(x,x))=f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)). 541 [para_from,469.1.1,5.1.1.2.2] f(f(f(f(x,f(f(x,f(x,x)),x)),x),f(x,f(f(x,f(x,x)),x))),f(f(f(x,f(x,x)),x),f(f(f(x,x),x),f(x,x))))=f(f(x,f(x,x)),x). 543 [para_into,387.1.1.2.2.2.1,263.1.1] f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))=x. 550,549 [para_into,433.1.1.1.2.1.1,523.1.1,demod,236,236,524,258,524,466,194,236,flip.1] f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x))=x. 567 [back_demod,531,demod,550] f(f(f(x,x),f(f(f(x,f(x,x)),x),f(x,x))),f(x,x))=x. 575 [back_demod,319,demod,550] f(f(f(x,f(f(x,f(x,x)),x)),x),x)=f(x,f(f(x,f(x,x)),x)). 584,583 [back_demod,257,demod,550,flip.1] f(f(x,f(x,x)),x)=f(x,x). 596,595 [back_demod,575,demod,584,584,584] f(f(x,x),x)=f(x,f(x,x)). 600,599 [back_demod,567,demod,584,584] f(f(x,x),f(x,x))=x. 612,611 [back_demod,549,demod,584,596,584] f(f(x,f(x,x)),f(x,x))=x. 614,613 [back_demod,543,demod,584,584,596,584,596,584,584,612,584] f(f(x,x),f(x,f(x,x)))=x. 616,615 [back_demod,541,demod,584,584,584,614,584,596,612,596,584] f(x,f(x,f(x,x)))=f(x,x). 666,665 [back_demod,299,demod,584,584,584,596,584,584] f(f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y)),f(y,f(y,y)))=f(y,y). 744,743 [back_demod,53,demod,596,612] f(x,f(f(x,f(x,f(f(y,f(x,y)),y))),x))=f(x,f(x,f(f(y,f(x,y)),y))). 751 [back_demod,41,demod,744] f(f(f(x,f(x,f(f(y,f(x,y)),y))),x),x)=f(x,f(x,f(f(y,f(x,y)),y))). 839 [para_from,583.1.1,11.1.1.1.1.2.1,demod,584] f(f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y)),y)=f(y,y). 865 [para_from,583.1.1,395.1.1.2.2.2.2.2.2.2.2.2.2.2,demod,616,616,616,616] f(f(f(x,f(y,x)),x),f(y,f(x,f(x,x))))=y. 892,891 [para_from,583.1.1,27.1.1.1] f(f(x,x),f(x,f(f(y,f(x,y)),y)))=x. 893 [para_from,583.1.1,3.1.1.1] f(f(x,x),f(x,f(y,x)))=x. 1054,1053 [para_into,893.1.1.2,7.1.1] f(f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y))),x)=f(x,f(f(y,f(x,y)),y)). 1674,1673 [para_from,839.1.1,865.1.1.1.1.2,demod,584,666,600,flip.1] f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y))=y. 1680,1679 [para_into,1673.1.1.1.1,891.1.1,demod,892,1054,892] f(f(x,f(x,f(f(y,f(x,y)),y))),x)=f(x,f(f(y,f(x,y)),y)). 1728,1727 [back_demod,751,demod,1680] f(f(x,f(f(y,f(x,y)),y)),x)=f(x,f(x,f(f(y,f(x,y)),y))). 1848,1847 [para_from,1673.1.1,69.1.1.1.1.2.1,demod,1674] f(f(f(x,f(y,x)),x),f(y,y))=y. 1849 [para_from,1673.1.1,21.1.1.1] f(x,f(f(x,x),y))=f(x,x). 1936,1935 [para_into,1849.1.1.2.1,599.1.1,demod,600] f(f(x,x),f(x,y))=x. 2037 [para_from,1935.1.1,69.1.1.1.1.2.1.1.2,demod,1936] f(f(f(x,f(f(f(f(x,y),x),f(x,y)),x)),x),f(x,x))=f(f(f(x,y),x),f(x,y)). 2098,2097 [para_into,1847.1.1.1.1.2,1935.1.1,demod,1936] f(f(f(f(x,y),x),f(x,y)),x)=f(x,x). 2122,2121 [back_demod,2037,demod,2098,584,1936,flip.1] f(f(f(x,y),x),f(x,y))=x. 2208,2207 [para_into,2121.1.1.1.1,1847.1.1,demod,1848,1728] f(x,f(x,f(f(y,f(x,y)),y)))=f(f(y,f(x,y)),y). 2218,2217 [para_into,2121.1.1.1,2121.1.1] f(x,f(f(x,y),x))=f(x,y). 2220,2219 [para_into,2121.1.1.1,1673.1.1] f(x,f(f(y,x),f(f(x,x),f(y,x))))=f(y,x). 2222,2221 [para_into,2121.1.1.2,1673.1.1,demod,1674,2220,flip.1] f(f(x,y),f(f(y,y),f(x,y)))=f(f(x,y),y). 2243 [back_demod,1727,demod,2208] f(f(x,f(f(y,f(x,y)),y)),x)=f(f(y,f(x,y)),y). 2282,2281 [back_demod,2219,demod,2222] f(x,f(f(y,x),x))=f(y,x). 2308,2307 [back_demod,1673,demod,2222] f(f(f(x,y),y),f(x,y))=y. 2309 [back_demod,19,demod,2282] f(f(f(f(x,f(y,x)),x),f(f(f(x,f(y,x)),x),x)),y)=f(f(x,f(y,x)),x). 2311 [back_demod,1,demod,2282] f(f(Y,X),f(Y,f(Z,X)))!=Y. 2359,2358 [para_from,2121.1.1,109.1.1.1.2.2,demod,2122,2122,2122,2122,2308,2308,2218,2122,2122,flip.1] f(f(f(x,y),x),x)=f(x,y). 2385,2384 [back_demod,2309,demod,2359,2122,flip.1] f(f(x,f(y,x)),x)=f(x,y). 2426 [back_demod,2243,demod,2385,2385,2385] f(x,y)=f(y,x). 2557,2556 [back_demod,27,demod,2385,2385] f(f(x,y),f(y,f(z,x)))=y. 2609 [para_into,2311.1.1.1,2426.1.1,demod,2557] Y!=Y. 2610 [binary,2609.1,2.1] $F. ------------ end of proof -------------