----- Otter 3.0.4a, November 1995 -----
The job was started by mccune on gyro, Fri May  3 09:14:51 1996
----> UNIT CONFLICT at   0.54 sec ----> 105 [binary,103.1,6.1] $F.

Length of proof is 12.  Level of proof is 8.

---------------- 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.
28 [para_into,20.1.1.2,18.1.1] (e/ ((e/x)/y))/x=y.
30 [para_into,24.1.1.1,18.1.1] x/ ((e/y)/ ((e/x)/ (y/z)))=z.
103 [para_into,30.1.1.2.2.2,28.1.1,demod,19] x/ (((e/y)/z)/ ((e/x)/z))=y.
105 [binary,103.1,6.1] $F.

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