----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:16:48 1995
----> UNIT CONFLICT at 187.41 sec ----> 4009 [binary,4008.1,1.1] $F.

Length of proof is 8.  Level of proof is 5.

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

1 [] A*B*A*B*A*B*A*B!=A*A*A*A*B*B*B*B.
4,3 [] (x*y)*z=x*y*z.
5 [] x*y*y=y*y*x.
8 [para_into,5.1.1.2,3.1.1,demod,4,4] x*y*z*y*z=y*z*y*z*x.
13 [para_from,5.1.1,3.1.1.1,demod,4,4,4] x*x*y*z=y*x*x*z.
14 [copy,13,flip.1] x*y*y*z=y*y*x*z.
48 [para_from,8.1.1,3.1.1.1,demod,4,4,4,4,4,4,4] x*y*x*y*z*u=z*x*y*x*y*u.
50 [copy,48,flip.1] x*y*z*y*z*u=y*z*y*z*x*u.
78 [para_into,14.1.1.2.2,14.1.1] x*y*z*z*y*u=y*y*x*z*z*u.
3988 [para_from,78.1.1,50.1.1.2.2] x*y*y*y*z*z*z*u=y*z*y*z*x*z*y*u.
4008 [copy,3988,flip.1] x*y*x*y*z*y*x*u=z*x*x*x*y*y*y*u.
4009 [binary,4008.1,1.1] $F.

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