----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:01:45 1995
----> UNIT CONFLICT at   0.35 sec ----> 116 [binary,114.1,1.1] $F.

Length of proof is 10.  Level of proof is 6.

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

1 [] d*d0!=c*c0.
4,3 [] (x*y)*z=x* (y*z).
15 [] x@ * (x*y)=y.
18,17 [] x* (x@ *y)=y.
23 [] a*a0=b*b0.
24 [copy,23,flip.1] b*b0=a*a0.
26 [] c*a0=d*b0.
27 [copy,26,flip.1] d*b0=c*a0.
29 [] a*c0=b*d0.
30 [copy,29,flip.1] b*d0=a*c0.
32 [para_from,24.1.1,3.1.1.1,demod,4,flip.1] b* (b0*x)=a* (a0*x).
34 [para_from,27.1.1,3.1.1.1,demod,4,flip.1] d* (b0*x)=c* (a0*x).
44 [para_into,15.1.1.2,30.1.1] b@ * (a*c0)=d0.
62 [para_from,32.1.1,15.1.1.2] b@ * (a* (a0*x))=b0*x.
97,96 [para_into,62.1.1.2.2,17.1.1] b@ * (a*x)=b0* (a0@ *x).
106 [back_demod,44,demod,97] b0* (a0@ *c0)=d0.
114 [para_from,106.1.1,34.1.1.2,demod,18] d*d0=c*c0.
116 [binary,114.1,1.1] $F.

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