----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:50:04 1995
----> UNIT CONFLICT at  18.78 sec ----> 541 [binary,540.1,1.1]  -> .

Length of proof is 13.  Level of proof is 9.

---------------- 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* (y* (z*u))= ((x*y)*z)*u.
6 [copy,5,flip.1]  -> ((x*y)*z)*u=x* (y* (z*u)).
7 [para_into,6.1.1.1.1,6.1.2]  -> ((((x*y)*z)*u)*v)*w=x* ((y* (z*u))* (v*w)).
8 [para_into,6.1.1.1.1,6.1.1]  -> ((x* (y* (z*u)))*v)*w= ((x*y)*z)* (u* (v*w)).
14 [para_into,6.1.2.2,6.1.2]  -> ((x*y)*z)* (u*v)=x* (((y*z)*u)*v).
38 [para_into,7.1.1,6.1.1,gL-id]  -> ((x*y)*z)* (u*v)=x* ((y* (z*u))*v).
42 [para_into,38.1.1,14.1.1]  -> x* (((y*z)*u)*v)=x* ((y* (z*u))*v).
53 [hyper,3,2,42,flip.1]  -> ((x*y)*z)*u= (x* (y*z))*u.
63 [hyper,4,2,53,flip.1]  -> (x*y)*z=x* (y*z).
111 [gL,8]  -> ((x* (y* (z*u)))*v)*w= ((x*y)*v)* (u* (z*w)).
125 [para_into,63.1.1.1,63.1.1]  -> (x* (y*z))*u= (x*y)* (z*u).
273 [para_into,111.1.1,8.1.1,gL-id]  -> (x*y)* (z* (u*v))= (x*u)* (z* (y*v)).
453 [hyper,3,273,125,flip.1]  -> (x*y)*z=y* (x*z).
540 [hyper,4,63,453]  -> x*y=y*x.
541 [binary,540.1,1.1]  -> .

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