----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Thu Nov  2 00:20:18 1995
----> UNIT CONFLICT at   0.03 sec ----> 10 [binary,8.1,7.1] $F.

Length of proof is 2.  Level of proof is 1.

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

3,2 [] x*x=x.
5,4 [] (x*y)*x=y.
6 [] (((A*A)*B)*A)* (C*B)!=C.
7 [copy,6,demod,3,5] B* (C*B)!=C.
8 [para_into,4.1.1.1,4.1.1] x* (y*x)=y.
10 [binary,8.1,7.1] $F.

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