----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:02:16 1995
----> UNIT CONFLICT at   1.28 sec ----> 175 [binary,174.1,1.1]  -> .

Length of proof is 7.  Level of proof is 7.

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

1 [] A@ *A=B@ *B -> .
4,3 []  -> beta=alpha.
5 []  -> x* ((((x*y@ )*y)@ *z)* ((alpha*u)@ * (beta*u)))=z.
7,6 [copy,5,demod,4]  -> x* ((((x*y@ )*y)@ *z)* ((alpha*u)@ * (alpha*u)))=z.
10,9 [para_into,6.1.1.2.2.1.1,6.1.1,demod,7]  -> x* ((((x*y@ )*y)@ *z)* (u@ *u))=z.
12 [para_into,9.1.1.2.1,9.1.1]  -> x* (y* (z@ *z))= (((((x*u@ )*u)@ *v@ )*v)@ *y)* (w@ *w).
13 [copy,12,flip.1]  -> (((((x*y@ )*y)@ *z@ )*z)@ *u)* (v@ *v)=x* (u* (w@ *w)).
35 [para_into,13.1.1,13.1.1]  -> x* (y* (z@ *z))=x* (y* (u@ *u)).
141 [para_from,35.1.1,9.1.1.2.1,demod,10]  -> x* (y@ *y)=x* (z@ *z).
174 [para_from,141.1.1,9.1.1.2.1,demod,10]  -> x@ *x=y@ *y.
175 [binary,174.1,1.1]  -> .

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