----- Otter 3.0.4a, November 1995 -----
The job was started by mccune on gyro, Fri May  3 09:44:30 1996
----> UNIT CONFLICT at   0.74 sec ----> 167 [binary,165.1,121.1] $F.

Length of proof is 29.  Level of proof is 18.

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

1 [] x=x.
2 [] A* (B* (((C*C@ )* (D*B)@ )*A))@ !=D.
3 [] (x*y)*z!= (x*u)*v|u* (v*z@ )=y.
5,4 [hyper,3,1] x* (y*y@ )=x.
6 [para_from,4.1.1,3.2.1] (x*y)*z!= (x*u)*z|u=y.
8 [para_into,6.1.1,4.1.1,demod,5] x*y!=x*z|z=y.
9 [para_into,8.1.1,4.1.1,flip.1] x*y!=x|y=z*z@ .
10 [hyper,9,4] x*x@ =y*y@ .
11 [hyper,9,10] (x*x@ )@ =y*y@ .
12 [hyper,3,10] x* ((y*x)@ * (y*z)@ @ )=z.
14 [copy,11,flip.1] x*x@ = (y*y@ )@ .
17 [para_from,11.1.1,3.2.1.2.2,demod,5,5] x*y!= (x*z)*u|z*u=y.
21 [para_from,14.1.1,4.1.1.2] x* (y*y@ )@ =x.
26,25 [para_into,21.1.1.2.1,14.1.1] x* (y*y@ )@ @ =x.
30 [para_into,12.1.1.2.1.1,4.1.1] (x*x@ )* (y@ * (y*z)@ @ )=z.
32 [para_into,12.1.1.2.1,11.1.1] x@ * ((y*y@ )* (x*z)@ @ )=z.
34 [para_into,12.1.1.2.2.1.1,10.1.1,demod,26] x* (y*x)@ =y@ .
38 [para_into,34.1.1.2.1,34.1.1] (x*y)@ *x@ @ =y@ .
43,42 [para_into,34.1.1.2.1,4.1.1] (x*x@ )*y@ =y@ .
45,44 [back_demod,32,demod,43] x@ * (x*y)@ @ =y.
46 [back_demod,2,demod,43] A* (B* ((D*B)@ *A))@ !=D.
48,47 [back_demod,30,demod,45] (x*x@ )*y=y.
61 [para_from,47.1.1,6.1.1.1,demod,48] x*y!=z*y|z=x.
81,80 [para_into,44.1.1.1,11.1.1,demod,48,48] x@ @ =x.
83,82 [para_into,44.1.1.2.1.1,34.1.1,demod,81,flip.1] (x*y)@ =y@ *x@ .
89 [back_demod,44,demod,83,83,81,81] x@ * (x*y)=y.
91 [back_demod,38,demod,83,81] (x@ *y@ )*y=x@ .
95 [back_demod,46,demod,83,83,83,83,81,81] A* ((A@ * (D*B))*B@ )!=D.
118,117 [hyper,17,89,flip.1] x* ((x@ *y)*z)=y*z.
121 [back_demod,95,demod,118] (D*B)*B@ !=D.
161 [para_into,91.1.1.1.1,80.1.1,demod,81] (x*y@ )*y=x.
165 [hyper,61,161,flip.1] (x*y)*y@ =x.
167 [binary,165.1,121.1] $F.

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