----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:51:02 1995
----> UNIT CONFLICT at   2.32 sec ----> 184 [binary,183.1,1.1]  -> .

Length of proof is 6.  Level of proof is 5.

---------------- 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).
8 [para_into,5.1.1.1,5.1.2]  -> ((x* (y*z))*u)*v= ((x*y)*z)* (u*v).
24 [gL,8]  -> ((x* (y*z))*u)*v= ((x*y)*u)* (z*v).
29 [para_into,24.1.1.1,5.1.1,gL-id]  -> (x* (y*z))*u= (x*z)* (y*u).
32 [para_into,24.1.1,8.1.1,gL-id]  -> (x*y)* (z*u)= (x*z)* (y*u).
67 [hyper,4,5,29]  -> x* (y*z)=x* (z*y).
183 [hyper,3,32,67]  -> x*y=y*x.
184 [binary,183.1,1.1]  -> .

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