----- Otter 3.1-b0, May 2000 ----- The process was started by wos on jaguar.mcs.anl.gov, Tue Jun 27 15:37:55 2000 The command was "otter". The process ID is 3471. ----> UNIT CONFLICT at 0.73 sec ----> 591 [binary,590.1,3.1] $ANS(SING_3). Length of proof is 22. Level of proof is 19. ---------------- PROOF ---------------- 2 [] f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y. 3 [] f(f(f(a,b),c),f(a,f(f(a,c),a)))!=c|$ANS(SING_3). 30 [para_into,2.1.1.2,2.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)). 31 [para_from,30.1.1,2.1.1.2.2] f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z))))=y. 32 [para_into,31.1.1.2,2.1.1] f(f(x,f(f(f(y,f(f(y,y),y)),x),x)),y)=f(y,f(f(y,y),y)). 33 [para_into,32.1.1.1.2.1,2.1.1] f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x)=f(x,f(f(x,x),x)). 34 [para_into,33.1.1.1,31.1.1,flip.1] f(x,f(f(x,x),x))=f(x,x). 40 [para_from,34.1.1,2.1.1.2] f(f(x,f(f(x,x),x)),f(x,x))=x. 41 [para_from,34.1.1,2.1.1.1] f(f(x,x),f(x,f(y,x)))=x. 49 [para_from,41.1.1,31.1.1.2] f(f(x,f(f(f(y,y),x),x)),y)=f(y,y). 57 [para_from,49.1.2,40.1.1.1.2.1] f(f(x,f(f(f(y,f(f(f(x,x),y),y)),x),x)),f(x,x))=x. 61 [para_into,57.1.1,30.1.1] f(x,f(f(f(f(y,x),f(y,x)),x),x))=f(y,x). 64 [para_from,61.1.1,41.1.1.2] f(f(x,x),f(y,x))=x. 71 [para_into,64.1.1.2,64.1.1] f(f(f(x,y),f(x,y)),y)=f(x,y). 95 [para_from,71.1.1,61.1.1.2.1] f(x,f(f(y,x),x))=f(y,x). 117 [para_from,95.1.1,2.1.1.1] f(f(x,y),f(x,f(z,y)))=x. 135 [para_into,117.1.1.2.2,64.1.1] f(f(x,f(y,z)),f(x,z))=x. 141 [para_into,135.1.1.1,117.1.1] f(x,f(f(x,y),f(z,y)))=f(x,y). 170 [para_into,141.1.1.2,2.1.1,flip.1] f(x,f(f(y,x),x))=f(x,y). 208 [para_into,170.1.1,95.1.1] f(x,y)=f(y,x). 231 [para_from,170.1.1,2.1.1.1] f(f(x,y),f(y,f(z,x)))=y. 301 [para_from,208.1.1,95.1.1.2.1] f(x,f(f(x,y),x))=f(y,x). 399 [para_into,231.1.1.2.2,135.1.1] f(f(f(x,y),z),f(z,x))=z. 590 [para_into,399.1.1.2,301.1.2] f(f(f(x,y),z),f(x,f(f(x,z),x)))=z. 591 [binary,590.1,3.1] $ANS(SING_3). ------------ end of proof -------------