----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:49:50 1995
----> UNIT CONFLICT at   6.13 sec ----> 1206 [binary,1205.1,5.1]  -> .

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

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

2 [] x*y=u, x*z=u -> y=z.
3 [] y*x=u, z*x=u -> y=z.
4 []  -> (x*y)*z=x* (y*z).
5 [] B*A=A*B -> .
6 [para_into,4.1.1.1.1,4.1.2]  -> (((x*y)*z)*u)*v= (x* (y*z))* (u*v).
11 [para_into,4.1.1.1,4.1.1]  -> (x* (y*z))*u= (x*y)* (z*u).
432 [gL,6]  -> (((x*y)*z)*u)*v= (x*u)* ((y*z)*v).
433 [hyper,3,11,432,flip.1]  -> ((x*y)*z)*u=x* (u* (y*z)).
1205 [hyper,2,432,433]  -> x*y=y*x.
1206 [binary,1205.1,5.1]  -> .

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