----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Thu Nov  9 15:39:27 1995
----> UNIT CONFLICT at   2.15 sec ----> 350 [binary,349.1,115.1]  -> .

Length of proof is 9.  Level of proof is 6.

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

1 []  -> x=x.
2 [] x*y=z, u*v=z, x*w=v6, v7*v=v6 -> u*w=v7*y.
3 [] f(B,A)=f(A,B), f(f(A,B),C)=f(A,f(B,C)), f(e,A)=A, f(x,A)=e -> .
5,4 []  -> x* (y*x)=y.
6 []  -> x*e=e*x.
8,7 []  -> f(x,y)=e* (y*x).
10 [back_demod,3,demod,8,8,8,8,8,8,8,5,8,unit_del,1,flip.1,flip.2] e* (B*A)=e* (A*B), e* ((e* (C*B))*A)=e* (C* (e* (B*A))), e* (A*x)=e -> .
17,16 [para_into,4.1.1.2,4.1.1]  -> (x*y)*x=y.
19 [hyper,2,4.1,6.1,1.1,6.1,demod,17]  -> x*y=y*x.
115 [para_into,19.1.1,16.1.1,flip.1]  -> x* (x*y)=y.
117 [para_into,19.1.1,4.1.1,flip.1]  -> (x*y)*y=x.
119 [hyper,2,115.1,115.1,4.1,115.1]  -> x* (y*z)=x* (z*y).
243,242 [hyper,2,117.1,115.1,4.1,117.1,flip.1]  -> (x* (y*z))*u=y* (x* (z*u)).
348 [back_demod,10,demod,243,unit_del,119,1] e* (A*x)=e -> .
349 [para_into,348.1.1.2,115.1.1] e*x=e -> .
350 [binary,349.1,115.1]  -> .

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