----- Otter 3.1-b0, May 2000 ----- The process was started by wos on jaguar.mcs.anl.gov, Tue Jun 27 09:31:06 2000 The command was "otter". The process ID is 2261. ----> UNIT CONFLICT at 1.07 sec ----> 859 [binary,858.1,3.1] $F. Length of proof is 23. Level of proof is 21. ---------------- PROOF ---------------- 2 [] f(f(f(x,y),z),f(f(x,f(x,z)),x))=z # label("SING_1"). 3 [] f(f(a,f(f(b,a),a)),f(b,f(c,a)))!=b # label("neg SING_2"). 33 [para_into,2.1.1.1,2.1.1] f(x,f(f(f(y,z),f(f(y,z),f(f(y,f(y,x)),y))),f(y,z)))=f(f(y,f(y,x)),y). 34 [para_from,33.1.1,2.1.1.1.1] f(f(f(f(x,f(x,y)),x),z),f(f(y,f(y,z)),y))=z. 35 [para_into,34.1.1.1,2.1.1] f(x,f(f(y,f(y,f(f(x,f(x,x)),x))),y))=f(f(x,f(x,x)),x). 36 [para_into,35.1.1.2.1.2,2.1.1] f(x,f(f(f(f(x,y),x),x),f(f(x,y),x)))=f(f(x,f(x,x)),x). 37 [para_into,36.1.1.2,34.1.1,flip.1] f(f(x,f(x,x)),x)=f(x,x). 43 [para_from,37.1.1,2.1.1.2] f(f(f(x,y),x),f(x,x))=x. 44 [para_from,37.1.1,2.1.1.1] f(f(x,x),f(f(x,f(x,x)),x))=x. 50 [para_from,43.1.1,34.1.1.1] f(x,f(f(y,f(y,f(x,x))),y))=f(x,x). 59 [para_from,50.1.2,44.1.1.2.1.2] f(f(x,x),f(f(x,f(x,f(f(y,f(y,f(x,x))),y))),x))=x. 62 [para_into,59.1.1,33.1.1] f(f(x,f(x,f(f(x,y),f(x,y)))),x)=f(x,y). 66 [para_from,62.1.1,43.1.1.1] f(f(x,y),f(x,x))=x. 68 [para_into,66.1.1.1,66.1.1] f(x,f(f(x,y),f(x,y)))=f(x,y). 97 [para_from,68.1.1,62.1.1.1.2] f(f(x,f(x,y)),x)=f(x,y). 119 [para_from,97.1.1,2.1.1.2] f(f(f(x,y),z),f(x,z))=z. 133 [para_into,119.1.1.1.1,66.1.1] f(f(x,y),f(f(x,z),y))=y. 150 [para_into,133.1.1.2,97.1.1] f(f(x,x),f(x,y))=x. 174 [para_from,150.1.1,119.1.1.2] f(f(f(f(x,x),y),f(x,z)),x)=f(x,z). 370 [para_into,174.1.1.1,119.1.1] f(x,y)=f(y,x). 407 [para_from,370.1.1,119.1.1.2] f(f(f(x,y),z),f(z,x))=z. 500 [para_into,407.1.1.1.1,133.1.1] f(f(x,y),f(y,f(z,x)))=y. 508 [para_into,407.1.1.1,150.1.1] f(x,f(f(x,y),x))=f(x,y). 702 [para_into,508.1.1.2.1,370.1.2] f(x,f(f(y,x),x))=f(x,y). 858 [para_from,702.1.2,500.1.1.1] f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y. 859 [binary,858.1,3.1] $F. ------------ end of proof -------------