----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:01:55 1995
----> UNIT CONFLICT at   0.46 sec ----> 85 [binary,84.1,1.1]  -> .

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

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

1 [] A@ *A=B@ *B -> .
4,3 []  -> x* ((((x*y@ )*y)@ *z)* (u@ *u))=z.
5 [para_into,3.1.1.2.1,3.1.1]  -> x* (y* (z@ *z))= (((((x*u@ )*u)@ *v@ )*v)@ *y)* (w@ *w).
6 [copy,5,flip.1]  -> (((((x*y@ )*y)@ *z@ )*z)@ *u)* (v@ *v)=x* (u* (w@ *w)).
28 [para_into,6.1.1,6.1.1]  -> x* (y* (z@ *z))=x* (y* (u@ *u)).
64 [para_from,28.1.1,3.1.1.2.1,demod,4]  -> x* (y@ *y)=x* (z@ *z).
84 [para_from,64.1.1,3.1.1.2.1,demod,4]  -> x@ *x=y@ *y.
85 [binary,84.1,1.1]  -> .

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