----- Otter 3.0.4a, November 1995 -----
The job was started by mccune on gyro, Fri May  3 09:17:11 1996
----> UNIT CONFLICT at   0.22 sec ----> 45 [binary,43.1,1.1] $F.

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

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

1 [] A- (B- (C- (A-B)))!=C.
2 [] x=x.
3 [] x-y!=z-u|u- (z-x)=y.
5,4 [hyper,3,2] x- (y-y)=x.
6 [hyper,3,4] x- (y- (y-x))=z-z.
10 [para_into,6.1.1.2.2,4.1.1,demod,5] x-x=y-y.
12 [hyper,3,10] x- (x-y)=y.
14 [hyper,3,12] x- (y-z)=z- (y-x).
21 [para_from,14.1.1,12.1.1.2] x- (y- (z-x))=z-y.
22 [copy,21,flip.1] x-y=z- (y- (x-z)).
43 [para_from,22.1.1,12.1.1.2] x- (y- (z- (x-y)))=z.
45 [binary,43.1,1.1] $F.

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