----- Otter 3.0.4c, May 1996 ----- The job was started by mccune on cosmo.mcs.anl.gov, Mon Oct 21 15:56:36 1996 ----> UNIT CONFLICT at 1340.15 sec ----> 8089 [binary,8087.1,1.1] \$F. Length of proof is 40. Level of proof is 12. ---------------- PROOF ---------------- 1 [] x+x!=x. 4,3 [] x+y=y+x. 6,5 [] (x+y)+z=x+ (y+z). 8,7 [] x+ (y+z)=y+ (x+z). 10,9 [] C+D=C. 11 [] n(n(x+y)+n(x+n(y)))=x. 16,15 [para_from,9.1.1,5.1.1.1,flip.1] C+ (D+x)=C+x. 17 [para_into,11.1.1.1.1.1,15.1.1] n(n(C+x)+n(C+n(D+x)))=C. 23 [para_into,11.1.1.1.1.1,7.1.1] n(n(x+ (y+z))+n(y+n(x+z)))=y. 27 [para_into,11.1.1.1.1.1,3.1.1] n(n(x+y)+n(y+n(x)))=y. 29 [para_into,11.1.1.1.2.1.2,11.1.1,demod,4] n(n(x+y)+n(x+ (n(y+z)+n(y+n(z)))))=x. 31 [para_into,11.1.1.1.2.1,3.1.1] n(n(x+y)+n(n(y)+x))=x. 43 [para_into,17.1.1.1.1.1,3.1.1] n(n(x+C)+n(C+n(D+x)))=C. 61 [para_into,27.1.1.1.1.1,9.1.1] n(n(C)+n(D+n(C)))=D. 77 [para_into,27.1.1.1.2.1,3.1.1] n(n(x+y)+n(n(x)+y))=y. 81 [para_into,27.1.1.1,3.1.1] n(n(x+n(y))+n(y+x))=x. 109 [para_into,31.1.1.1.2.1.1,27.1.1] n(n(x+ (n(y+z)+n(z+n(y))))+n(z+x))=x. 121 [para_into,31.1.1.1.2,61.1.1,demod,4,4] n(D+n(C+n(D+n(C))))=n(D+n(C)). 123 [para_into,31.1.1.1.2,31.1.1,demod,8,4,4] n(x+n(x+ (y+n(n(y)+x))))=n(n(y)+x). 149 [para_into,77.1.1.1.1.1,5.1.1] n(n(x+ (y+z))+n(n(x+y)+z))=z. 171 [para_into,77.1.1.1.2,77.1.1,demod,6,4] n(x+n(y+ (x+n(n(y)+x))))=n(n(y)+x). 186,185 [para_into,23.1.1.1.1.1,15.1.1] n(n(C+x)+n(D+n(C+x)))=D. 233 [para_into,81.1.1.1.2.1,7.1.1,demod,6] n(n(x+ (y+n(z)))+n(x+ (z+y)))=x+y. 235 [para_into,81.1.1.1.2.1,5.1.1] n(n(x+n(y+z))+n(y+ (z+x)))=x. 287 [para_into,43.1.1.1,3.1.1] n(n(C+n(D+x))+n(x+C))=C. 391 [para_into,29.1.1.1.2.1.2.2,81.1.1,demod,8,4,4] n(n(x+n(y+n(z)))+n(x+ (y+n(z+ (y+n(y+n(z)))))))=x. 415 [para_into,185.1.1.1.1.1,3.1.1] n(n(x+C)+n(D+n(C+x)))=D. 493 [para_into,415.1.1.1,3.1.1] n(n(D+n(C+x))+n(x+C))=D. 537 [para_from,493.1.1,27.1.1.1.2.1.2,demod,6] n(n(n(D+n(C+x))+ (n(x+C)+y))+n(y+D))=y. 719 [para_into,149.1.1.1.1.1,7.1.1] n(n(x+ (y+z))+n(n(y+x)+z))=z. 897 [para_into,235.1.1.1.1.1.2.1,3.1.1] n(n(x+n(y+z))+n(z+ (y+x)))=x. 1159 [para_into,897.1.1.1.2.1.2,15.1.1,demod,6] n(n(D+ (x+n(C+y)))+n(y+ (C+x)))=D+x. 2224,2223 [para_into,109.1.1.1.2.1,9.1.1,demod,4] n(n(C)+n(D+ (n(x+C)+n(C+n(x)))))=D. 2573 [para_from,121.1.1,287.1.1.1.1.1.2,demod,4] n(n(C+n(D+n(C)))+n(C+n(C+n(D+n(C)))))=C. 2655 [para_into,123.1.1.1.2.1.2.2,185.1.1,demod,4,8,16,4,6,186] n(n(D+n(C+x))+n(C+ (x+n(D+n(C+x)))))=D. 4267 [para_into,233.1.1.1.1.1,3.1.1,demod,6] n(n(x+ (n(y)+z))+n(z+ (y+x)))=z+x. 5538,5537 [para_into,391.1.1.1.1,185.1.1,demod,8,6,8,16,8] n(D+n(D+ (n(C+x)+n(C+ (x+n(D+n(C+x)))))))=n(C+x). 6527 [para_from,2655.1.1,719.1.1.1.2,demod,8,4,5538,flip.1] n(C+ (x+n(D+n(C+x))))=n(C+x). 6538,6537 [para_into,6527.1.1.1.2.2.1.2.1,9.1.1,demod,16,10] n(C+n(D+n(C)))=n(C). 6584,6583 [back_demod,2573,demod,6538,6538] n(n(C)+n(C+n(C)))=C. 6650,6649 [para_from,6583.1.1,391.1.1.1.1,demod,8] n(C+n(C+ (n(C)+n(C+ (C+n(C+n(C)))))))=n(C). 6727 [para_from,6583.1.1,171.1.1.1.2.1.2.2,demod,4,6584] n(n(C+n(C))+n(C+ (C+n(C+n(C)))))=C. 7795 [para_from,6727.1.1,719.1.1.1.2,demod,8,4,6650,flip.1] n(C+ (C+n(C+n(C))))=n(C). 7797 [para_from,7795.1.1,1159.1.1.1.2,demod,4,4,2224,flip.1] D+n(C+n(C))=D. 8084,8083 [para_from,7797.1.1,537.1.1.1.1.1.1.1,demod,4] n(n(n(D)+ (n(C+n(C))+x))+n(x+D))=x. 8087 [para_from,7797.1.1,4267.1.1.1.2.1.2,demod,8,8084,flip.1] x+n(C+n(C))=x. 8089 [binary,8087.1,1.1] \$F. ------------ end of proof -------------