----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Thu Nov  2 00:23:11 1995
----> UNIT CONFLICT at  55.76 sec ----> 72 [binary,70.1,13.1]  -> .

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

---------------- 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=x.
6,5 []  -> e* (e*x)=x.
7 []  -> C4*A=C3*B.
9 []  -> C2*A=C1*B.
11 []  -> C4*F=C3*E.
13 [] C2*F=C1*E -> .
20 [hyper,2,1.1,3.1,5.1,1.1]  -> ((e*x)*e)* (e* (y*e))=y*x.
22 [hyper,2,5.1,1.1,1.1,3.1]  -> x*y= ((e*y)*e)* (e* (x*e)).
39 [hyper,2,11.1,20.1,7.1,20.1]  -> ((e*E)*e)*A= ((e*B)*e)*F.
60 [hyper,2,20.1,9.1,1.1,39.1,flip.1]  -> ((e*E)*e)* (e* (C1*e))=C2*F.
70 [para_into,60.1.1,22.1.1,demod,6,4,4,6,flip.1]  -> C2*F=C1*E.
72 [binary,70.1,13.1]  -> .

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