----- Otter 3.0.4a, November 1995 -----
The job was started by mccune on gyro, Fri May  3 09:13:32 1996
----> UNIT CONFLICT at   1.24 sec ----> 65 [binary,64.1,1.1] $F.

Length of proof is 16.  Level of proof is 11.

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

1 [] A/A!=B/B.
2 [] x=x.
3 [] x/y!=z/u|y/ (((z/z)/z)/ ((x/x)/x))=u.
5,4 [hyper,3,2] x/ (((y/y)/y)/ ((y/y)/y))=x.
7,6 [hyper,3,4] (((x/x)/x)/ ((x/x)/x))/ (((y/y)/y)/ (((y/z)/ (y/z))/ (y/z)))=z.
8 [hyper,3,6,demod,5,5,5] (((x/x)/x)/ (((x/ (y/z))/ (x/ (y/z)))/ (x/ (y/z))))/ ((y/y)/y)=z.
10 [para_into,6.1.1.2.2.1.1,4.1.1,demod,5,5,5] ((x/x)/x)/ ((x/x)/x)= ((y/y)/y)/ ((y/y)/y).
11 [para_into,6.1.1.2.2.1,4.1.1,demod,5,5] (((x/x)/x)/ ((x/x)/x))/ ((((y/y)/y)/ ((y/y)/y))/ ((y/y)/y))= (y/y)/y.
14,13 [para_from,10.1.1,6.1.1.2.2.1] (((x/x)/x)/ ((x/x)/x))/ ((((y/y)/ (y/y))/ (y/y))/ ((((z/z)/z)/ ((z/z)/z))/ ((y/y)/y)))=y.
17 [para_from,10.1.1,4.1.1.2.1.1] x/ (((((y/y)/y)/ ((y/y)/y))/ ((z/z)/z))/ ((((z/z)/z)/ ((z/z)/z))/ ((z/z)/z)))=x.
19 [para_into,8.1.1.1.2.1.1.2,6.1.1,demod,7,7,5,5,5] ((x/x)/x)/ (((x/y)/ (x/y))/ (x/y))= ((z/z)/z)/ (((z/y)/ (z/y))/ (z/y)).
25,24 [para_into,11.1.1.2.1,10.1.1] (((x/x)/x)/ ((x/x)/x))/ ((((y/y)/y)/ ((y/y)/y))/ ((z/z)/z))= (z/z)/z.
33,32 [para_from,13.1.1,6.1.1.2.2.2,demod,5,5,14,14,25,flip.1] (((x/x)/ (x/x))/ (x/x))/ ((((y/y)/y)/ ((y/y)/y))/ ((x/x)/x))= (x/x)/x.
35,34 [back_demod,13,demod,33] (((x/x)/x)/ ((x/x)/x))/ ((y/y)/y)=y.
42,41 [back_demod,17,demod,35,35] x/ (y/y)=x.
49,48 [para_from,41.1.1,19.1.1.2,demod,42,42,flip.1] ((x/x)/x)/ (((x/y)/ (x/y))/ (x/y))= (y/y)/y.
54,53 [para_from,41.1.1,8.1.1.2,demod,49,42,42] (((x/x)/y)/ ((x/x)/y))/ ((x/x)/y)=y.
56 [para_from,41.1.1,19.1.1.1,demod,42,54,49] (x/x)/y= (y/y)/y.
64 [para_into,56.1.1,41.1.1,demod,42,42] x/x=y/y.
65 [binary,64.1,1.1] $F.

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