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

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

---------------- 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.
6 [hyper,3,4] (((x/x)/x)/ ((x/x)/x))/ (((y/y)/y)/ (((y/z)/ (y/z))/ (y/z)))=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.
19,18 [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.
22 [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.
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.
29,28 [para_from,18.1.1,6.1.1.2.2.2,demod,5,5,19,19,25,flip.1] (((x/x)/ (x/x))/ (x/x))/ ((((y/y)/y)/ ((y/y)/y))/ ((x/x)/x))= (x/x)/x.
31,30 [back_demod,18,demod,29] (((x/x)/x)/ ((x/x)/x))/ ((y/y)/y)=y.
36,35 [back_demod,22,demod,31,31] x/ (y/y)=x.
40 [para_into,30.1.1.1.1.1,10.1.1,demod,31,31] (x/x)/ ((y/y)/y)=y.
54 [para_into,40.1.1.2.1,35.1.1,demod,36,36] x/x=y/y.
55 [binary,54.1,1.1] $F.

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