----- Otter 3.0.4a, November 1995 -----
The job was started by mccune on gyro, Fri May  3 09:14:08 1996
----> UNIT CONFLICT at   1.27 sec ----> 173 [binary,172.1,1.1] $F.

Length of proof is 20.  Level of proof is 11.

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

1 [] x=x.
2 [] x/y!=z/u|y/ (((z/z)/z)/ ((x/x)/x))=u.
4,3 [] x/x=e.
5 [] A/ ((((A/A)/B)/C)/ (((A/A)/A)/C))!=B.
6 [copy,5,demod,4,4] A/ (((e/B)/C)/ ((e/A)/C))!=B.
7 [back_demod,2,demod,4,4] x/y!=z/u|y/ ((e/z)/ (e/x))=u.
9,8 [hyper,7,1,demod,4] x/e=x.
10 [hyper,7,8] e/ ((e/x)/ (e/ (x/y)))=y.
12 [hyper,7,10,demod,4,9] ((e/x)/ (e/ (x/ (y/z))))/ (e/y)=z.
17,16 [para_into,10.1.1.2.2.2,10.1.1,demod,4,flip.1] (e/x)/ (e/ (x/y))=e/ (e/ (e/y)).
19,18 [para_into,10.1.1.2.2.2,3.1.1,demod,4,9] e/ (e/x)=x.
20 [back_demod,12,demod,17,19] (e/ (x/y))/ (e/x)=y.
24 [hyper,7,20,demod,19] (e/x)/ ((e/y)/ (x/ (y/z)))=z.
26 [para_into,20.1.1.1.2,20.1.1,demod,19] (e/x)/ (y/x)=e/y.
30 [hyper,7,26,demod,4,19] (x/y)/ (e/y)=x.
32 [para_into,26.1.1.1,18.1.1] x/ (y/ (e/x))=e/y.
33 [copy,32,flip.1] e/x=y/ (x/ (e/y)).
36 [para_into,30.1.1.1,20.1.1,demod,19] x/y=e/ (y/x).
39 [copy,36,flip.1] e/ (x/y)=y/x.
43 [para_from,36.1.1,6.1.1.2.1] A/ ((e/ (C/ (e/B)))/ ((e/A)/C))!=B.
100,99 [para_into,33.1.1,39.1.1,flip.1] x/ ((y/z)/ (e/x))=z/y.
104 [para_from,33.1.1,30.1.1.2] (x/y)/ (z/ (y/ (e/z)))=x.
171,170 [para_from,104.1.1,24.1.1.2.2] (e/ (x/y))/ ((e/z)/x)=y/ (e/z).
172 [back_demod,43,demod,171,100,9] B!=B.
173 [binary,172.1,1.1] $F.

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