----- Otter 3.0.4c, May 1996 ----- The job was started by mccune on cosmo.mcs.anl.gov, Sat Oct 12 20:54:03 1996 ----> UNIT CONFLICT at 18.30 sec ----> 1212 [binary,1211.1,211.1] $F. Length of proof is 34. Level of proof is 17. ---------------- PROOF ---------------- 2 [] x+y=y+x. 3 [] (x+y)+z=x+y+z. 4 [] (x+y)+z=x+y+z. 5 [] n(n(n(x)+y)+n(x+y))=y. 6 [] n(x+y)!=n(x). 64 [para_into,4.1.1.1,2.1.1,demod,3] x+y+z=y+x+z. 71 [para_into,5.1.1.1.2.1,2.1.1] n(n(n(x)+y)+n(y+x))=y. 73 [para_into,5.1.1.1,2.1.1] n(n(x+y)+n(n(x)+y))=y. 75 [para_into,6.1.1.1,2.1.1] n(x+y)!=n(y). 93 [para_into,71.1.1.1,2.1.1] n(n(x+y)+n(n(y)+x))=x. 116 [para_into,75.1.1.1,4.1.1] n(x+y+z)!=n(z). 130 [para_into,93.1.1.1.2,73.1.1] n(n(n(n(x)+y)+x+y)+y)=n(n(x)+y). 132 [para_into,93.1.1.1.2,5.1.1] n(n(n(x+y)+n(x)+y)+y)=n(x+y). 139 [para_into,116.1.1.1.2,64.1.1] n(x+y+z+u)!=n(y+u). 170 [para_from,130.1.1,73.1.1.1.2,demod,3,3] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y. 174 [para_from,130.1.1,5.1.1.1.1,demod,3,3] n(n(n(x)+y)+n(n(n(x)+y)+x+y+y))=y. 190 [para_into,132.1.1.1.1.1.2,64.1.1] n(n(n(x+y+z)+y+n(x)+z)+y+z)=n(x+y+z). 211 [para_into,139.1.1.1,64.1.1] n(x+y+z+u)!=n(x+u). 253 [para_from,170.1.1,93.1.1.1.2] n(n(n(n(x)+y)+n(n(x)+y)+x+y+y)+y)=n(n(x)+y). 260 [para_from,170.1.1,73.1.1.1.2.1.1,demod,3] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z))=z. 346 [para_into,190.1.1.1.2,2.1.1] n(n(n(x+y+z)+y+n(x)+z)+z+y)=n(x+y+z). 423 [para_from,253.1.1,5.1.1.1.1,demod,3,3,3,3] n(n(n(x)+y)+n(n(n(x)+y)+n(n(x)+y)+x+y+y+y))=y. 475 [para_from,260.1.1,73.1.1.1.2,demod,3,3] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z+n(y+z))+z)=n(y+z). 486 [para_into,346.1.1.1.1.1.1.1,2.1.1,demod,3] n(n(n(x+y+z)+x+n(z)+y)+y+x)=n(z+x+y). 684 [para_into,475.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). 801 [para_from,684.1.1,73.1.1.1.2.1.1,demod,3] 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. 848 [para_into,801.1.1.1.1,486.1.1,demod,3] n(n(x+x+n(n(x)+x)+x)+n(n(x+x)+n(n(x)+x)))=n(n(x)+x). 878 [para_into,848.1.1.1.2,93.1.1] n(n(x+x+n(n(x)+x)+x)+x)=n(n(x)+x). 897 [para_into,878.1.1.1.1.1.2,64.1.1] n(n(x+n(n(x)+x)+x+x)+x)=n(n(x)+x). 948 [para_into,897.1.1.1.1.1,64.1.1] n(n(n(n(x)+x)+x+x+x)+x)=n(n(x)+x). 1015 [para_from,948.1.1,73.1.1.1.2.1.1,demod,3] n(n(n(n(n(x)+x)+x+x+x)+x+y)+n(n(n(x)+x)+y))=y. 1036 [para_from,948.1.1,73.1.1.1.2,demod,3,3,3] n(n(n(n(x)+x)+x+x+x+x)+n(n(x)+x))=x. 1053 [para_into,1015.1.1.1.2,423.1.1] n(n(n(n(n(x)+x)+x+x+x)+x+n(n(n(x)+x)+n(n(x)+x)+x+x+x+x))+x)=n(n(n(x)+x)+n(n(x)+x)+x+x+x+x). 1079 [para_from,1036.1.1,93.1.1.1.2] n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x)=n(n(x)+x). 1112 [para_into,1053.1.1.1.1.1,2.1.1,demod,3] n(n(x+n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+n(n(n(x)+x)+x+x+x))+x)=n(n(n(x)+x)+n(n(x)+x)+x+x+x+x). 1130 [para_from,1079.1.1,73.1.1.1.2.1.1,demod,3] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x+y)+n(n(n(x)+x)+y))=y. 1149 [para_into,1112.1.1.1.1.1,64.1.1] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x+n(n(n(x)+x)+x+x+x))+x)=n(n(n(x)+x)+n(n(x)+x)+x+x+x+x). 1169 [para_into,1130.1.1.1.2,174.1.1] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x+n(n(n(x)+x)+x+x+x))+x)=n(n(n(x)+x)+x+x+x). 1211 [para_into,1169.1.1,1149.1.1] n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)=n(n(n(x)+x)+x+x+x). 1212 [binary,1211.1,211.1] $F. ------------ end of proof -------------