----- Otter 3.0.4c, May 1996 ----- The job was started by mccune on cosmo.mcs.anl.gov, Thu Oct 24 19:45:53 1996 ----> UNIT CONFLICT at 17.11 sec ----> 112 [binary,111.1,7.1] $F. Length of proof is 50. Level of proof is 20. ---------------- PROOF ---------------- 2 [] x+y=y+x. 3 [] (x+y)+z=x+y+z. 4 [] n(n(x+y)+n(x+n(y)))=x. 5 [] n(C+D)=n(C). 6 [] (x+y)+z=x+y+z. 7 [] x+y!=x. 62 [para_into,3.1.1.1,2.1.1,demod,6] x+y+z=y+x+z. 63 [para_into,3.1.1,2.1.1] x+y+z=y+z+x. 64 [para_from,3.1.1,2.1.1] x+y+z=z+x+y. 65 [para_into,4.1.1.1.1.1,2.1.1] n(n(x+y)+n(y+n(x)))=y. 66 [para_into,4.1.1.1.2.1,2.1.1] n(n(x+y)+n(n(y)+x))=x. 67 [para_into,4.1.1.1,2.1.1] n(n(x+n(y))+n(x+y))=x. 68 [para_into,5.1.1.1,2.1.1] n(D+C)=n(C). 69 [para_from,64.1.1,4.1.1.1.1.1] n(n(x+y+z)+n(y+n(z+x)))=y. 70 [para_into,65.1.1.1.1,5.1.1] n(n(C)+n(D+n(C)))=D. 71 [para_into,65.1.1.1.2.1,2.1.1] n(n(x+y)+n(n(x)+y))=y. 72 [para_into,66.1.1.1.1.1,63.1.1] n(n(x+y+z)+n(n(x+y)+z))=z. 73 [para_into,66.1.1.1,2.1.1] n(n(n(x)+y)+n(y+x))=y. 74 [para_into,71.1.1.1,2.1.1] n(n(n(x)+y)+n(x+y))=y. 75 [para_from,71.1.1,66.1.1.1.2] n(n(n(n(x)+y)+x+y)+y)=n(n(x)+y). 76 [para_into,73.1.1.1.1.1.1,68.1.1] n(n(n(C)+x)+n(x+D+C))=x. 77 [para_into,73.1.1.1.2,68.1.1] n(n(n(C)+D)+n(C))=D. 78 [para_from,73.1.1,69.1.1.1.2] n(n(x+n(n(x)+y)+y)+y)=n(n(x)+y). 79 [para_from,75.1.1,72.1.1.1.2,demod,6] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y. 80 [para_from,76.1.1,69.1.1.1.2,demod,6] n(n(D+C+n(n(C)+x)+x)+x)=n(n(C)+x). 81 [para_from,77.1.1,67.1.1.1.1.1.2] n(n(x+D)+n(x+n(n(C)+D)+n(C)))=x. 82 [para_into,78.1.1.1.1.1.2.1.1.1,74.1.1,demod,6] n(n(n(n(x)+y)+n(x+y)+n(y+z)+z)+z)=n(n(n(n(x)+y)+n(x+y))+z). 83 [para_from,79.1.1,71.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. 84 [para_into,80.1.1.1.1.1,63.1.1,demod,6] n(n(C+n(n(C)+x)+x+D)+x)=n(n(C)+x). 85 [para_into,82.1.2.1.1,74.1.1] n(n(n(n(x)+y)+n(x+y)+n(y+z)+z)+z)=n(y+z). 86 [para_into,83.1.1.1.1.1.1.1,62.1.1] n(n(n(x+n(n(x)+y)+y+y)+n(n(x)+y)+z)+n(y+z))=z. 87 [para_from,84.1.1,81.1.1.1.1] n(n(n(C)+D)+n(n(C+n(n(C)+D)+D+D)+n(n(C)+D)+n(C)))=n(C+n(n(C)+D)+D+D). 88 [para_into,85.1.1.1.1.1.2.2.1,70.1.1] n(n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C)))+n(D+n(C)))=n(n(C)+n(D+n(C))). 89 [para_from,85.1.1,71.1.1.1.2.1.1,demod,6] n(n(n(n(n(x)+y)+n(x+y)+n(y+z)+z)+z+u)+n(n(y+z)+u))=u. 90 [para_into,86.1.1.1.2.1,2.1.1] n(n(n(x+n(n(x)+y)+y+y)+n(n(x)+y)+z)+n(z+y))=z. 91 [para_into,88.1.2,70.1.1] n(n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C)))+n(D+n(C)))=D. 92 [para_into,89.1.1.1.2,77.1.1] n(n(n(n(n(x)+n(C))+n(x+n(C))+n(n(C)+D)+D)+D+n(C))+D)=n(C). 93 [para_into,90.1.1.1,2.1.1] n(n(x+y)+n(n(z+n(n(z)+y)+y+y)+n(n(z)+y)+x))=x. 94 [para_from,91.1.1,4.1.1.1.2] n(n(n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C)))+D+n(C))+D)=n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C))). 95 [para_into,93.1.1,87.1.1] n(C+n(n(C)+D)+D+D)=n(C). 96 [para_into,94.1.1.1.1.1.1.1.2.2,2.1.1] n(n(n(n(n(x)+n(C))+n(x+n(C))+n(D+n(C))+D)+D+n(C))+D)=n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C))). 97 [para_into,95.1.1.1.2.1.1,2.1.1] n(C+n(D+n(C))+D+D)=n(C). 98 [para_into,96.1.1.1.1.1.1.1.2.2.1.1,2.1.1] n(n(n(n(n(x)+n(C))+n(x+n(C))+n(n(C)+D)+D)+D+n(C))+D)=n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C))). 99 [para_into,97.1.1.1,64.1.1,demod,6] n(D+D+C+n(D+n(C)))=n(C). 100 [para_into,98.1.1,92.1.1,flip.1] n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C)))=n(C). 101 [para_from,99.1.1,78.1.1.1.1.1.2.1.1.1,demod,6,6,6] n(n(D+D+C+n(D+n(C))+n(n(C)+x)+x)+x)=n(n(D+D+C+n(D+n(C)))+x). 102 [para_into,100.1.1.1.1.1.1,68.1.1,demod,6] n(n(n(C)+n(C))+n(D+C+n(C))+D+n(D+n(C)))=n(C). 103 [para_into,101.1.2.1.1,99.1.1] n(n(D+D+C+n(D+n(C))+n(n(C)+x)+x)+x)=n(n(C)+x). 104 [para_into,102.1.1.1,62.1.1] n(n(D+C+n(C))+n(n(C)+n(C))+D+n(D+n(C)))=n(C). 105 [para_from,104.1.1,72.1.1.1.2,demod,6] n(n(D+C+n(C)+n(n(C)+n(C))+D+n(D+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)). 106 [para_into,105.1.1.1.1.1.2.2.2,62.1.1] n(n(D+C+n(C)+D+n(n(C)+n(C))+n(D+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)). 107 [para_into,106.1.1.1.1.1.2.2,62.1.1] n(n(D+C+D+n(C)+n(n(C)+n(C))+n(D+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)). 108 [para_into,107.1.1.1.1.1.2,62.1.1] n(n(D+D+C+n(C)+n(n(C)+n(C))+n(D+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)). 109 [para_into,108.1.1.1.1.1.2.2.2.2,2.1.1] n(n(D+D+C+n(C)+n(D+n(C))+n(n(C)+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)). 110 [para_into,109.1.1.1.1.1.2.2.2,63.1.1] n(n(D+D+C+n(D+n(C))+n(n(C)+n(C))+n(C))+n(C))=n(n(C)+n(C))+D+n(D+n(C)). 111 [para_into,110.1.1,103.1.1,flip.1] n(n(C)+n(C))+D+n(D+n(C))=n(n(C)+n(C)). 112 [binary,111.1,7.1] $F. ------------ end of proof -------------