----- SUMMARY FOR THEOREM DJ-10C IN DIRECTORY Q:\DJ -----

% DJ-10C.IN       1994 April 18
% Theorem 10C about Disjoint Classes
% Theorem DJ-10C subsumes theorem DJ-10A

formula_list(sos).
% negation of theorem DJ-10C
-(all xr all z (-disjoint(xr,cart(singleton(z),V)) -> member(z,D(xr)))).
end_of_list.


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

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

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

118 [] member(x,V) | equal(singleton(x),0).
228 [] disjoint(x,0).
241 [] -member(z,V) | disjoint(xr,cart(singleton(z),V))
           | member(z,D(xr)).
243 [] -disjoint($c2,cart(singleton($c1),V)).
244 [] -member($c1,D($c2)).
277 [] equal(cart(0,y),0).
299 [ur,243,241,244] -member($c1,V).
309 [ur,299,118] equal(singleton($c1),0).
315 [para_from,309.1.1,243.1.2.1,demod,277] -disjoint($c2,0).
316 [binary,315.1,228.1] $F.

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

clauses generated     231
Kbytes malloced       319
user CPU time           0.55  seconds