----- SUMMARY FOR THEOREM DJ-EQ IN DIRECTORY Q:\DJ -----

% DJ-EQ.IN                 1997 May 22

formula_list(sos).
% negation of theorem DJ-EQ
-(all x y ((disjoint(x,y) & subclass(complement(x),y)) 
            -> equal(complement(x),y))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Jul 13 22:41:40 1997

Length of proof is 3. Level of proof is 2.

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

7 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
232 [] -disjoint(x,y) | disjoint(y,x).
234 [] -disjoint(x,complement(y)) | subclass(x,y).
246 [] disjoint($c2,$c1).
247 [] subclass(complement($c2),$c1).
248 [] -equal(complement($c2),$c1).
262 [] equal(complement(complement(x)),x).
294 [ur,246,232] disjoint($c1,$c2).
299 [ur,248,7,247] -subclass($c1,complement($c2)).
300 [ur,299,234,demod,262] -disjoint($c1,$c2).
301 [binary,300.1,294.1] $F.

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

clauses generated     187
Kbytes malloced       287
user CPU time           0.50  seconds