----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:58:17 1995
----> UNIT CONFLICT at   0.52 sec ----> 126 [binary,125.1,121.1]  -> .

Length of proof is 17.  Level of proof is 10.

---------------- 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*y)* ((z*z@ )*u)= (x* (v@ *v))* (y*u).
8 [copy,7,flip.1]  -> (x* (y@ *y))* (z*u)= (x*z)* ((v*v@ )*u).
9 [para_into,3.1.1.2,3.1.1,flip.1]  -> x@ @ *y=x*y.
14,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.
27 [para_into,7.1.1.2,5.1.1]  -> (x*y)*z= (x* (u@ *u))* (y*z).
38 [copy,27,flip.1]  -> (x* (y@ *y))* (z*u)= (x*z)*u.
42 [para_into,17.1.1.1,15.1.1]  -> x* (y*x)@ =y@ .
50 [para_into,42.1.1.2.1,17.1.1,flip.1]  -> (x*y)@ =y@ *x@ .
65 [para_from,50.1.1,17.1.1.2]  -> (x* (y*z))* (z@ *y@ )=x.
80 [para_into,65.1.1.2.2,50.1.1]  -> (x* ((y*z)*u))* (u@ * (z@ *y@ ))=x.
91,90 [para_into,8.1.1.1,15.1.1,demod,14,flip.1]  -> (x*y)* ((z*z@ )*u)=x* (y*u).
99,98 [para_into,8.1.1,65.1.1,demod,14,91,flip.1]  -> x* (y@ *y)=x.
118,117 [back_demod,38,demod,99,flip.1]  -> (x*y)*z=x* (y*z).
120,119 [back_demod,80,demod,118,118,118,118,4,4]  -> x* (y*y@ )=x.
121 [back_demod,2,demod,120,118,unit_del,1,1] B*B@ =A*A@  -> .
125 [para_from,119.1.1,3.1.1.2]  -> x*x@ =y*y@ .
126 [binary,125.1,121.1]  -> .

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