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

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

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


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

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

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

224 [] -equal(intersection(x,y),0) | disjoint(x,y).
229 [] equal($c1,0).
230 [] -disjoint($c1,$c1).
238 [] equal(intersection(x,x),x).
277 [ur,230,224,demod,238] -equal($c1,0).
278 [binary,277.1,229.1] $F.

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

clauses generated      58
Kbytes malloced       287
user CPU time           0.44  seconds