----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:58:26 1995
----> UNIT CONFLICT at   0.17 sec ----> 52 [binary,51.1,45.1]  -> .

Length of proof is 10.  Level of proof is 6.

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

1 []  -> x=x.
2 [] B*B@ =A*A@ , A* (B*B@ )=A, (A*B)*C=A* (B*C) -> .
3 []  -> x* (x@ *y)=y.
5 []  -> (x*y@ )*y=x.
7 []  -> ((x* (y*z))*y)*u=x* (y* ((z*y)*u)).
9 []  -> x*x@ =y@ *y.
17,16 [para_from,9.1.1,5.1.1.1]  -> (x@ *x)*y=y.
18 [para_from,9.1.1,3.1.1.2]  -> x* (y@ *y)=x@ @ .
19 [copy,18,flip.1]  -> x@ @ =x* (y@ *y).
22,21 [para_into,16.1.1,5.1.1]  -> x@ @ =x.
27,26 [back_demod,19,demod,22,flip.1]  -> x* (y@ *y)=x.
28 [para_from,21.1.1,5.1.1.1.2]  -> (x*y)*y@ =x.
35,34 [para_into,7.1.1.1.1.2,16.1.1,demod,27,27,17]  -> (x*y)*z=x* (y*z).
44,43 [back_demod,28,demod,35]  -> x* (y*y@ )=x.
45 [back_demod,2,demod,44,35,unit_del,1,1] B*B@ =A*A@  -> .
51 [para_from,43.1.1,3.1.1.2]  -> x*x@ =y*y@ .
52 [binary,51.1,45.1]  -> .

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