----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:50:56 1995
----> UNIT CONFLICT at   0.48 sec ----> 92 [binary,91.1,1.1]  -> .

Length of proof is 5.  Level of proof is 4.

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

1 [] B*A=A*B -> .
3 [] x*y=z, x*u=z -> y=u.
4 [] x*y=z, u*y=z -> x=u.
5 []  -> x* (y* (z*u))= (x*y)* (z*u).
6 [copy,5,flip.1]  -> (x*y)* (z*u)=x* (y* (z*u)).
13 [para_into,6.1.2.2,6.1.2,gL-id]  -> (x*y)* (z*u)=x* ((y*z)*u).
15 [gL,6]  -> (x*y)* (z*u)=x* (z* (y*u)).
42 [hyper,3,13,15,flip.1]  -> (x*y)*z=y* (x*z).
91 [hyper,4,15,42]  -> x*y=y*x.
92 [binary,91.1,1.1]  -> .

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