----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 0.67 sec ----> 977 [binary,976.1,2.1] $F. Length of proof is 37. Level of proof is 11. ---------------- PROOF ---------------- 1 [] f(a,b)!=f(b,a). 2 [copy,1,flip.1] f(b,a)!=f(a,b). 5,4 [] f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y. 6 [para_into,4.1.1.1.2.1,4.1.1] f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z)))))=f(z,f(f(x,z),z)). 9,8 [para_into,4.1.1.2.2,4.1.1] f(f(f(x,f(y,z)),f(f(u,f(x,f(y,z))),f(x,f(y,z)))),f(u,x))=u. 10 [para_into,4.1.1.2,4.1.1] f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z)=f(y,f(f(z,y),y)). 12 [para_into,8.1.1.1.1.2,8.1.1,demod,9,9] f(f(f(x,y),f(f(z,f(x,y)),f(x,y))),f(z,x))=z. 17,16 [para_into,8.1.1.1.1,4.1.1,demod,5,5] f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z))))=y. 50 [para_into,16.1.1.2,4.1.1] f(f(x,f(f(f(y,f(f(y,y),y)),x),x)),y)=f(y,f(f(y,y),y)). 54 [para_from,16.1.1,4.1.1.2] f(f(f(x,f(f(y,x),x)),f(f(f(y,f(f(z,y),y)),f(x,f(f(y,x),x))),f(x,f(f(y,x),x)))),z)=f(y,f(f(z,y),y)). 68 [para_into,6.1.1.1,16.1.1] f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x)))))=f(x,f(f(x,x),x)). 81,80 [para_into,6.1.1.2,16.1.1,demod,17,flip.1] f(x,f(f(x,x),x))=f(x,x). 82 [back_demod,68,demod,81,81,81] f(x,f(f(x,x),f(y,f(x,x))))=f(x,x). 85,84 [back_demod,50,demod,81,81] f(f(x,f(f(f(y,y),x),x)),y)=f(y,y). 100 [para_from,80.1.1,12.1.1.1] f(f(f(x,y),f(x,y)),f(f(x,y),x))=f(x,y). 115,114 [para_from,80.1.1,4.1.1.2,demod,81] f(f(x,x),f(x,x))=x. 120 [para_from,80.1.1,4.1.1.1] f(f(x,x),f(x,f(y,x)))=x. 146 [para_from,82.1.1,16.1.1.2] f(f(x,f(f(y,x),x)),f(y,y))=y. 247,246 [para_from,84.1.1,10.1.1.1.2.1,demod,81,115,flip.1] f(x,f(f(f(f(y,x),f(y,x)),x),x))=f(y,x). 248 [para_from,84.1.1,10.1.1.1.2.1.1.2.1,demod,81,85,81] f(f(f(x,y),f(f(f(y,y),f(x,y)),f(x,y))),f(z,f(f(f(y,y),z),z)))=f(y,y). 366 [para_into,246.1.1.2.1.1.1,246.1.1,demod,247,247] f(f(f(f(f(x,y),f(x,y)),y),y),f(f(f(f(x,y),f(x,y)),f(f(f(f(x,y),f(x,y)),y),y)),f(f(f(f(x,y),f(x,y)),y),y)))=f(x,y). 445,444 [para_from,246.1.1,120.1.1.2] f(f(x,x),f(y,x))=x. 452 [para_from,246.1.1,12.1.1.1.2.1] f(f(f(f(f(f(x,y),f(x,y)),y),y),f(f(x,y),f(f(f(f(x,y),f(x,y)),y),y))),f(y,f(f(f(x,y),f(x,y)),y)))=y. 457,456 [para_from,246.1.1,100.1.1.2.1,demod,247,247,247] f(f(f(x,y),f(x,y)),f(f(x,y),y))=f(x,y). 472 [para_from,246.1.1,16.1.1.2.2.2.1] f(f(x,f(f(y,x),x)),f(y,f(f(f(f(f(z,x),f(z,x)),x),x),f(f(z,x),f(f(f(f(z,x),f(z,x)),x),x)))))=y. 494 [para_from,246.1.1,146.1.1.1.2.1] f(f(f(f(f(f(x,y),f(x,y)),y),y),f(f(x,y),f(f(f(f(x,y),f(x,y)),y),y))),f(y,y))=y. 500 [back_demod,248,demod,445] f(f(f(x,y),f(y,f(x,y))),f(z,f(f(f(y,y),z),z)))=f(y,y). 505,504 [para_into,444.1.1.2,444.1.1] f(f(f(x,y),f(x,y)),y)=f(x,y). 526 [back_demod,494,demod,505,505] f(f(f(f(x,y),y),f(f(x,y),f(f(x,y),y))),f(y,y))=y. 532 [back_demod,472,demod,505,505] f(f(x,f(f(y,x),x)),f(y,f(f(f(z,x),x),f(f(z,x),f(f(z,x),x)))))=y. 540 [back_demod,452,demod,505,505,505] f(f(f(f(x,y),y),f(f(x,y),f(f(x,y),y))),f(y,f(x,y)))=y. 545,544 [back_demod,366,demod,505,505,457,505] f(f(f(x,y),y),f(f(x,y),f(f(x,y),y)))=f(x,y). 547,546 [back_demod,246,demod,505] f(x,f(f(y,x),x))=f(y,x). 551,550 [back_demod,540,demod,545] f(f(x,y),f(y,f(x,y)))=y. 557,556 [back_demod,532,demod,547,545] f(f(x,y),f(x,f(z,y)))=x. 561,560 [back_demod,526,demod,557] f(f(x,y),f(y,y))=y. 570 [back_demod,500,demod,551,547] f(x,f(f(x,x),y))=f(x,x). 674 [back_demod,54,demod,547,547,547,547,547,547] f(f(f(x,y),f(y,z)),x)=f(x,y). 976 [para_into,674.1.1.1.2,570.1.1,demod,561] f(x,y)=f(y,x). 977 [binary,976.1,2.1] $F. ------------ end of proof -------------