----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:50:32 1995
----> UNIT CONFLICT at  16.28 sec ----> 209 [binary,208.1,1.1]  -> .

Length of proof is 10.  Level of proof is 7.

---------------- 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*v)))= (((x*y)*z)*u)*v.
6 [copy,5,flip.1]  -> (((x*y)*z)*u)*v=x* (y* (z* (u*v))).
7 [para_into,6.1.1.1.1,6.1.1]  -> ((x* (y* (z* (u*v))))*w)*v6= ((x*y)*z)* (u* (v* (w*v6))).
8 [para_into,6.1.1.1,6.1.1]  -> (x* (y* (z* (u*v))))*w= (x*y)* (z* (u* (v*w))).
25 [gL,7]  -> ((x* (y* (z* (u*v))))*w)*v6= ((x*y)*w)* (u* (v* (z*v6))).
32 [hyper,4,8,25,flip.1]  -> (x* (y* (z* (u*v))))*w= (x*y)* (w* (u* (v*z))).
33 [hyper,4,7,25,gL-id]  -> (x* (y* (z*u)))*v= (x* (y* (v*u)))*z.
37 [para_into,25.1.1,7.1.1,gL-id]  -> (x*y)* (z* (u* (v*w)))= (x*v)* (z* (u* (y*w))).
56 [para_into,32.1.1,8.1.1,gL-id]  -> x* (y* (z* (u*v)))=x* (v* (z* (u*y))).
61 [hyper,3,33,56]  -> x* (y* (z*u))=u* (y* (z*x)).
208 [hyper,4,61,37]  -> x*y=y*x.
209 [binary,208.1,1.1]  -> .

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