----- Otter 3.0.4c, May 1996 ----- The job was started by mccune on cosmo.mcs.anl.gov, Thu Jan 23 15:36:28 1997 ----> UNIT CONFLICT at 24.80 sec ----> 3039 [binary,3038.1,51.1] $F. Length of proof is 40. Level of proof is 18. ---------------- PROOF ---------------- 2 [] x+y=y+x. 3 [] (x+y)+z=x+y+z. 4 [] x+y!=x. 5 [] n(n(n(x)+y)+n(x+y))=y. 6 [] (x+y)+z=x+y+z. 47 [para_into,3.1.1.1,2.1.1,demod,6] x+y+z=y+x+z. 49 [para_from,3.1.1,2.1.1] x+y+z=z+x+y. 51 [para_into,4.1.1,2.1.1] x+y!=y. 53 [para_into,5.1.1.1.1.1,2.1.1] n(n(x+n(y))+n(y+x))=x. 55 [para_into,5.1.1.1.2.1,3.1.1] n(n(n(x+y)+z)+n(x+y+z))=z. 56 [para_into,5.1.1.1.2.1,2.1.1] n(n(n(x)+y)+n(y+x))=y. 58 [para_into,5.1.1.1,2.1.1] n(n(x+y)+n(n(x)+y))=y. 62 [para_from,47.1.1,5.1.1.1.1.1] n(n(x+n(y)+z)+n(y+x+z))=x+z. 67 [para_into,49.1.1.2,3.1.1] x+y+z+u=u+x+y+z. 93 [para_into,55.1.1.1.1.1.1.1,3.1.1,demod,6] n(n(n(x+y+z)+u)+n(x+y+z+u))=u. 111 [para_into,56.1.1.1.1.1.1,5.1.1] n(n(x+y)+n(y+n(n(z)+x)+n(z+x)))=y. 123 [para_into,56.1.1.1,2.1.1] n(n(x+y)+n(n(y)+x))=x. 212 [para_into,93.1.1.1.1.1.1.1.2,3.1.1,demod,6] n(n(n(x+y+z+u)+v)+n(x+y+z+u+v))=v. 327 [para_into,123.1.1.1.2,123.1.1] n(n(n(n(x)+y)+y+x)+y)=n(n(x)+y). 330 [para_into,123.1.1.1.2,62.1.1] n(n(n(x+y+z)+y+n(x)+z)+y+z)=n(x+y+z). 331 [para_into,123.1.1.1.2,58.1.1] n(n(n(n(x)+y)+x+y)+y)=n(n(x)+y). 352 [para_into,212.1.1.1.1.1.1.1.2.2,3.1.1,demod,6] n(n(n(x+y+z+u+v)+w)+n(x+y+z+u+v+w))=w. 445 [para_from,327.1.1,111.1.1.1.2.1.2.1,demod,6,6] n(n(x+y)+n(y+n(n(z)+x)+n(n(n(z)+x)+x+z+x)))=y. 476 [para_into,330.1.1.1.1.1.1.1,47.1.1] n(n(n(x+y+z)+x+n(y)+z)+x+z)=n(y+x+z). 570 [para_into,331.1.1.1.1.1.2,3.1.1] n(n(n(n(x+y)+z)+x+y+z)+z)=n(n(x+y)+z). 592 [para_from,331.1.1,58.1.1.1.2,demod,6,6] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y. 690 [para_into,445.1.1.1.1.1,2.1.1] n(n(x+y)+n(x+n(n(z)+y)+n(n(n(z)+y)+y+z+y)))=x. 858 [para_into,476.1.1.1.2,2.1.1] n(n(n(x+y+z)+x+n(y)+z)+z+x)=n(y+x+z). 906 [para_into,570.1.1.1.1.1.1.1.1.1,3.1.1,demod,6,6] n(n(n(n(x+y+z)+u)+x+y+z+u)+u)=n(n(x+y+z)+u). 1068 [para_from,592.1.1,58.1.1.1.2.1.1,demod,6] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z))=z. 1188 [para_into,690.1.1.1.2.1.2.2.1.2.2,2.1.1] n(n(x+y)+n(x+n(n(z)+y)+n(n(n(z)+y)+y+y+z)))=x. 1593 [para_from,1068.1.1,58.1.1.1.2,demod,6,6] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z+n(y+z))+z)=n(y+z). 1904 [para_into,1593.1.1.1.1.1.2.2,2.1.1] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z)=n(y+z). 2150 [para_from,1904.1.1,58.1.1.1.2.1.1,demod,6] n(n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u))=u. 2322 [para_into,2150.1.1.1.1,858.1.1,demod,6,6] n(n(x+x+x+n(n(x+x+x)+x)+x+x)+n(n(x+x+x)+n(n(x+x+x)+x)))=n(n(x+x+x)+x). 2438 [para_from,2322.1.1,53.1.1.1.1,demod,6] n(n(n(x+x+x)+x)+n(n(x+x+x)+n(n(x+x+x)+x)+n(x+x+x+n(n(x+x+x)+x)+x+x)))=n(x+x+x+n(n(x+x+x)+x)+x+x). 2447 [para_into,2438.1.1.1.2.1.2.2.1,67.1.1,demod,6,6] n(n(n(x+x+x)+x)+n(n(x+x+x)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+x+x+x+x+x)))=n(x+x+x+n(n(x+x+x)+x)+x+x). 2471 [para_into,2447.1.1,1188.1.1,flip.1] n(x+x+x+n(n(x+x+x)+x)+x+x)=n(x+x+x). 2499 [para_into,2471.1.1.1,67.1.1,demod,6,6] n(n(n(x+x+x)+x)+x+x+x+x+x)=n(x+x+x). 2520 [para_from,2471.1.1,93.1.1.1.2] n(n(n(x+x+x)+n(n(x+x+x)+x)+x+x)+n(x+x+x))=n(n(x+x+x)+x)+x+x. 2581 [para_from,2499.1.1,352.1.1.1.2] n(n(n(n(n(x+x+x)+x)+x+x+x+x)+x)+n(x+x+x))=x. 2744 [para_into,2581.1.1.1.1,906.1.1] n(n(n(x+x+x)+x)+n(x+x+x))=x. 2863 [para_from,2744.1.1,58.1.1.1.2.1.1,demod,6] n(n(n(n(x+x+x)+x)+n(x+x+x)+y)+n(x+y))=y. 2914 [para_into,2863.1.1.1.1.1,47.1.1] n(n(n(x+x+x)+n(n(x+x+x)+x)+y)+n(x+y))=y. 3038 [para_into,2914.1.1,2520.1.1] n(n(x+x+x)+x)+x+x=x+x. 3039 [binary,3038.1,51.1] $F. ------------ end of proof -------------