----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:02:37 1995
----> UNIT CONFLICT at   0.41 sec ----> 145 [binary,143.1,1.1]  -> .

Length of proof is 16.  Level of proof is 9.

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

1 [] beta=alpha -> .
3 []  -> x* ((((x*y@ )*y)@ *z)* ((alpha*u)@ * (beta*u)))=z.
5 []  -> x@ *x=y@ *y.
6 []  -> x@ * (x*y)=y.
8 []  -> (x*y)*y@ =x.
11 [para_into,3.1.1.2.2.1.1,3.1.1]  -> x* ((((x*y@ )*y)@ *z)* (u@ * (beta* ((((alpha*v@ )*v)@ *u)* ((alpha*w)@ * (beta*w))))))=z.
19,18 [para_into,6.1.1.2,3.1.1,flip.1]  -> (((x*y@ )*y)@ *z)* ((alpha*u)@ * (beta*u))=x@ *z.
23 [back_demod,11,demod,19]  -> x* ((((x*y@ )*y)@ *z)* (u@ * (beta* (alpha@ *u))))=z.
26 [back_demod,3,demod,19]  -> x* (x@ *y)=y.
31,30 [para_into,8.1.1.1,6.1.1]  -> x* (y*x)@ =y@ .
35,34 [para_from,26.1.1,8.1.1.1,demod,31]  -> x@ @ =x.
37,36 [para_from,34.1.1,8.1.1.2]  -> (x*y@ )*y=x.
40 [back_demod,23,demod,37]  -> x* ((x@ *y)* (z@ * (beta* (alpha@ *z))))=y.
48 [para_from,5.1.1,26.1.1.2]  -> x* (y@ *y)=x.
52 [para_into,36.1.1.1,5.1.1,demod,35]  -> (x@ *x)*y=y.
55,54 [para_into,48.1.1.2.1,34.1.1]  -> x* (y*y@ )=x.
61,60 [para_into,52.1.1.1.1,34.1.1]  -> (x*x@ )*y=y.
70 [para_from,54.1.1,26.1.1.2]  -> x*x@ =y*y@ .
84 [para_into,40.1.1.2.1,70.1.1,demod,61,35]  -> x* (y@ * (beta* (alpha@ *y)))=x.
126 [para_into,84.1.1.2.2.2,70.1.1,demod,35,55]  -> x* (alpha@ *beta)=x.
143 [para_into,126.1.1,26.1.1]  -> beta=alpha.
145 [binary,143.1,1.1]  -> .

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