----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Thu Nov  2 00:24:29 1995
----> UNIT CONFLICT at  74.62 sec ----> 517 [binary,515.1,13.1]  -> .

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

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

1 []  -> x=x.
2 [] x*y=z, u*v=z, x*w=v6, v7*v=v6 -> u*w=v7*y.
4,3 []  -> ((x*e)*e)*e=x.
6,5 []  -> e* (e* (e*x))=x.
7 []  -> C4*A=C3*B.
9 []  -> C2*A=C1*B.
11 []  -> C4*F=C3*E.
13 [] C2*F=C1*E -> .
14 [hyper,2,1.1,3.1,1.1,3.1]  -> (((x*y)*e)*e)*z= (((x*z)*e)*e)*y.
18,17 [hyper,2,1.1,3.1,9.1,3.1]  -> (((C2*x)*e)*e)*A= (((C1*B)*e)*e)*x.
33 [hyper,2,5.1,1.1,5.1,3.1]  -> x* (e* (e*y))= ((y*e)*e)* (e* (e* (x*e))).
36 [hyper,2,1.1,3.1,5.1,1.1]  -> (((e*x)*e)*e)* (e* (e* (y*e)))=y*x.
293 [hyper,2,11.1,36.1,7.1,36.1]  -> (((e*E)*e)*e)*A= (((e*B)*e)*e)*F.
418,417 [hyper,2,36.1,17.1,36.1,293.1,demod,4,6,4,flip.1]  -> (((e*E)*e)*e)* (e* (e* (C1*B)))= (((C2*F)*e)*e)*B.
423 [hyper,2,33.1,17.1,293.1,293.1,demod,4,6,18,418,flip.1]  -> (((C2*F)*e)*e)*B= (((C1*B)*e)*e)*E.
515 [hyper,2,3.1,14.1,3.1,423.1,demod,4,4,flip.1]  -> C2*F=C1*E.
517 [binary,515.1,13.1]  -> .

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