----- SUMMARY FOR THEOREM DJ-3A IN DIRECTORY Q:\DJ -----

% DJ-3A.IN      corrected 1994 April 16
% Theorem 3A about Disjoint Classes

formula_list(sos).
% negation of theorem DJ-3A
-(all x (disjoint(x,x) -> equal(x,0))).
end_of_list.


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

Length of proof is 1. Level of proof is 1.

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

225 [] -disjoint(x,y) | equal(intersection(x,y),0).
228 [] disjoint($c1,$c1).
229 [] -equal($c1,0).
237 [] equal(intersection(x,x),x).
274 [ur,228,225,demod,237] equal($c1,0).
275 [binary,274.1,229.1] $F.

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

clauses generated       1
Kbytes malloced       287
user CPU time           0.44  seconds