----- Otter 3.0.4a, November 1995 -----
The job was started by mccune on gyro, Fri May  3 09:28:17 1996
----> UNIT CONFLICT at   0.32 sec ----> 67 [binary,66.1,1.1] $F.

Length of proof is 18.  Level of proof is 14.

---------------- PROOF ----------------

1 [] x=x.
2 [] ((A+B)+C)+ (A+C)@ !=B.
3 [] x+y!=z+u| (y@ +z)+u=x.
4 [hyper,3,1] (x@ +y)+x=y.
7,6 [hyper,3,4] (x@ +y)+z=x@ + (y+z).
9,8 [back_demod,4,demod,7] x@ + (y+x)=y.
10 [para_into,8.1.1.2,8.1.1] (x+y)@ +x=y@ .
15,14 [para_into,10.1.1.1.1,8.1.1,flip.1] (x+y)@ =x@ +y@ .
16 [back_demod,2,demod,15] ((A+B)+C)+ (A@ +C@ )!=B.
17 [para_from,14.1.1,8.1.1.1,demod,7] x@ + (y@ + (z+ (x+y)))=z.
19 [para_into,6.1.1.1,8.1.1,flip.1] x@ + ((y+x)+z)=y+z.
22,21 [para_into,17.1.1.2,19.1.1] x@ + (y+ (x+z))=y+z.
25 [para_into,21.1.1.2,17.1.1,demod,22] x@ @ +y=y+x.
28,27 [para_into,21.1.1,19.1.1,flip.1] (x+y)+z=x+ (y+z).
30 [copy,25,flip.1] x+y=y@ @ +x.
31 [back_demod,16,demod,28,28,28] A+ (B+ (C+ (A@ +C@ )))!=B.
41,40 [para_into,30.1.1,25.1.1,flip.1] x@ @ +y@ @ =x+y.
45,44 [para_into,30.1.1,8.1.1,demod,15,15,41,28,flip.1] x+ (y+y@ )=x.
49 [para_from,30.1.1,17.1.1.2,demod,15,15,15,15,41,28,28,45,9] x@ @ =x.
64,63 [para_from,49.1.1,8.1.1.1] x+ (y+x@ )=y.
66 [back_demod,31,demod,64,64] B!=B.
67 [binary,66.1,1.1] $F.

------------ end of proof -------------