----- Otter 3.0.4, August 1995 ----- The job was started by mccune on cosmo.mcs.anl.gov, Thu Oct 24 19:45:20 1996 ----> UNIT CONFLICT at 18.30 sec ----> 2178 [binary,2177.1,1.1] $F. Length of proof is 39. Level of proof is 14. ---------------- PROOF ---------------- 1 [] x=x. 2 [] x+y=y+x. 4,3 [] (x+y)+z=x+y+z. 6,5 [] n(n(x+y)+n(x+n(y)))=x. 7 [] C+C=C. 9 [] n(n(A)+B)+n(n(A)+n(B))!=A. 10 [para_into,3.1.1.1,7.1.1,flip.1] C+C+x=C+x. 13 [para_into,3.1.1,2.1.1] x+y+z=y+z+x. 14 [copy,13,flip.1] x+y+z=z+x+y. 16,15 [para_into,10.1.1.2,2.1.1] C+x+C=C+x. 25 [para_into,5.1.1.1.1.1,7.1.1] n(n(C)+n(C+n(C)))=C. 27 [para_into,5.1.1.1.1.1,3.1.1,demod,4] n(n(x+y+z)+n(x+y+n(z)))=x+y. 29 [para_into,5.1.1.1.1.1,2.1.1] n(n(x+y)+n(y+n(x)))=y. 33 [para_into,5.1.1.1.2.1.2,5.1.1] n(n(x+n(y+z)+n(y+n(z)))+n(x+y))=x. 35 [para_into,5.1.1.1.2.1,2.1.1] n(n(x+y)+n(n(y)+x))=x. 39 [para_into,5.1.1.1,2.1.1] n(n(x+n(y))+n(x+y))=x. 49 [para_into,13.1.1.2,2.1.1] x+y+z=z+y+x. 63 [para_into,25.1.1.1,2.1.1] n(n(C+n(C))+n(C))=C. 65 [para_from,25.1.1,5.1.1.1.2] n(n(n(C)+C+n(C))+C)=n(C). 71 [para_into,9.1.1.1.1,2.1.1] n(B+n(A))+n(n(A)+n(B))!=A. 98 [para_from,63.1.1,5.1.1.1.2.1.2] n(n(x+n(C+n(C))+n(C))+n(x+C))=x. 117 [para_into,29.1.1.1.1.1,49.1.1,demod,4] n(n(x+y+z)+n(y+x+n(z)))=y+x. 147 [para_into,29.1.1.1.2.1,2.1.1] n(n(x+y)+n(n(x)+y))=y. 159 [para_into,29.1.1.1,2.1.1] n(n(x+n(y))+n(y+x))=x. 227 [para_into,35.1.1.1,2.1.1] n(n(n(x)+y)+n(y+x))=y. 289 [para_into,39.1.1.1.1,25.1.1] n(C+n(n(C)+C+n(C)))=n(C). 303 [para_into,39.1.1.1.2.1,14.1.1] n(n(x+n(y+z))+n(z+x+y))=x. 381 [para_into,147.1.1.1,2.1.1] n(n(n(x)+y)+n(x+y))=y. 459 [para_into,159.1.1.1.2.1,10.1.1,demod,4] n(n(C+x+n(C))+n(C+x))=C+x. 646,645 [para_from,65.1.1,381.1.1.1.1,demod,4,4,16] n(n(C)+n(n(C)+C+n(C)))=C. 652,651 [para_from,65.1.1,227.1.1.1.2,demod,646,flip.1] n(n(C)+C+n(C))=n(C+n(C)). 681 [back_demod,289,demod,652] n(C+n(C+n(C)))=n(C). 711 [para_into,71.1.1.2.1,2.1.1] n(B+n(A))+n(n(B)+n(A))!=A. 873 [para_into,711.1.1,2.1.1] n(n(B)+n(A))+n(B+n(A))!=A. 1451,1450 [para_into,98.1.1.1.2.1,7.1.1] n(n(C+n(C+n(C))+n(C))+n(C))=C. 1583,1582 [para_into,303.1.1.1.1.1.2,25.1.1] n(n(x+C)+n(n(C+n(C))+x+n(C)))=x. 1644 [para_into,459.1.1.1.2,681.1.1,demod,1451,flip.1] C+n(C+n(C))=C. 1646 [para_into,1644.1.1,2.1.1] n(C+n(C))+C=C. 1719,1718 [para_from,1646.1.1,117.1.1.1.1.1.2,demod,1583,flip.1] n(C+n(C))+x=x. 1725,1724 [para_from,1646.1.1,27.1.1.1.1.1.2,demod,1719,6,flip.1] x+n(C+n(C))=x. 1770 [para_from,1718.1.1,33.1.1.1.1.1,demod,6,1719] n(x+n(x))=n(C+n(C)). 1957,1956 [para_from,1770.1.1,227.1.1.1.1,demod,1719] n(n(n(n(x))+x))=n(n(x)). 1959,1958 [para_from,1770.1.1,227.1.1.1.2,demod,1725,1957] n(n(x))=x. 2091,2090 [para_into,1958.1.1.1,381.1.1,flip.1] n(n(x)+y)+n(x+y)=n(y). 2177 [back_demod,873,demod,2091,1959] A!=A. 2178 [binary,2177.1,1.1] $F. ------------ end of proof -------------