----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:24:10 1995
----> UNIT CONFLICT at   4.67 sec ----> 212 [binary,211.1,1.1]  -> .

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

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

1 [] B*A*B*A*B*A*B*A=A*B*A*B*A*B*A*B -> .
2 []  -> x=x.
3 [] x*y=z, x*u=z -> y=u.
6,5 []  -> (x*y)*z=x*y*z.
7 []  -> x*y*y*y*y=y*y*y*y*x.
10 [para_into,7.1.1.2.2.2,5.1.1,demod,6,6,6,6,6,6]  -> x*y*z*y*z*y*z*y*z=y*z*y*z*y*z*y*z*x.
211 [hyper,3,2.1,10.1]  -> x*y*x*y*x*y*x*y=y*x*y*x*y*x*y*x.
212 [binary,211.1,1.1]  -> .

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