----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:57:43 1995
----> UNIT CONFLICT at   0.22 sec ----> 64 [binary,63.1,59.1]  -> .

Length of proof is 12.  Level of proof is 8.

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

1 []  -> x=x.
2 [] B*B@ =A*A@ , A* (B*B@ )=A, (A*B)*C=A* (B*C) -> .
4,3 []  -> x* (x@ *y)=y.
6,5 []  -> (x*y@ )*y=x.
7 []  -> ((x*alpha)*y)* (beta*z)= (x*alpha)* (y* (beta*z)).
9 [para_into,3.1.1.2,3.1.1,flip.1]  -> x@ @ *y=x*y.
13 [para_from,9.1.1,5.1.1.1,demod,6,flip.1]  -> x@ @ =x.
15 [para_from,9.1.1,3.1.1.2]  -> x@ * (x*y)=y.
17 [para_from,13.1.1,5.1.1.1.2]  -> (x*y)*y@ =x.
21 [para_into,7.1.1.1.1,5.1.1,demod,6]  -> (x*y)* (beta*z)=x* (y* (beta*z)).
27 [para_into,17.1.1.1,15.1.1]  -> x* (y*x)@ =y@ .
31 [para_into,27.1.1.2.1,17.1.1,flip.1]  -> (x*y)@ =y@ *x@ .
35 [para_from,31.1.1,17.1.1.2]  -> (x* (y*z))* (z@ *y@ )=x.
54,53 [para_into,21.1.1.2,3.1.1,demod,4]  -> (x*y)*z=x* (y*z).
58,57 [back_demod,35,demod,54,54,4]  -> x* (y*y@ )=x.
59 [back_demod,2,demod,58,54,unit_del,1,1] B*B@ =A*A@  -> .
63 [para_from,57.1.1,3.1.1.2]  -> x*x@ =y*y@ .
64 [binary,63.1,59.1]  -> .

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