----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:51:13 1995
----> UNIT CONFLICT at   1.52 sec ----> 39 [binary,38.1,1.1]  -> .

Length of proof is 6.  Level of proof is 4.

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

1 [] B*A=A*B -> .
2 []  -> x=x.
3 [] x*y=z, x*u=z -> y=u.
4 [] x*y=z, u*y=z -> x=u.
5 []  -> (x*x)*y=x* (x*y).
6 []  -> (x*y)*x=x* (y*x).
12 [para_from,6.1.2,5.1.2.2,gL-id]  -> (x*x)* (y*z)=x* ((x*y)*z).
13 [para_into,12.1.1,5.1.1,gL-id,flip.1]  -> x* ((y*z)*u)=x* (y* (z*u)).
14 [para_into,12.1.2.2,5.1.1,gL-id]  -> (x*x)* (y*z)=x* (y* (x*z)).
19 [hyper,3,2,13,flip.1]  -> (x*y)*z=x* (y*z).
22 [hyper,3,12,14,flip.1]  -> (x*y)*z=y* (x*z).
38 [hyper,4,19,22]  -> x*y=y*x.
39 [binary,38.1,1.1]  -> .

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