----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:18:46 1995
----> UNIT CONFLICT at  17.08 sec ----> 305 [binary,304.1,135.1] $F.

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

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

2 [] m(x,y,y)=x.
3 [] m(x,x,y)=y.
4 [] m(A,B,m(C,D,E))!=m(E,D,m(A,B,C)).
25 [para_into,3.1.1.3,2.1.1] m(x,x,y)=m(y,z,z).
70 [gL,25] m(x,y,z)=m(z,y,x).
98 [para_into,70.1.1,3.1.2] m(x,x,m(y,z,u))=m(u,z,y).
99 [para_into,70.1.1,2.1.2] m(m(x,y,z),u,u)=m(z,y,x).
135 [para_from,70.1.1,4.1.1] m(m(C,D,E),B,A)!=m(E,D,m(A,B,C)).
183 [gL,98] m(x,y,m(z,u,y))=m(x,u,z).
291 [gL,99] m(m(x,y,z),x,u)=m(z,y,u).
304 [para_into,291.1.1,183.1.1] m(m(x,y,z),u,v)=m(z,y,m(v,u,x)).
305 [binary,304.1,135.1] $F.

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