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

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

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

3,2 [] x*x=x.
4 [] (x*y)*x=y.
6 [] ((A*A)*B)* (C* (A*B))!=C.
7 [copy,6,demod,3] (A*B)* (C* (A*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 -------------