----- SUMMARY FOR THEOREM DK-FIN IN DIRECTORY Q:\dedekind -----

% DK-FIN.IN                 2000 June 2
% Finite sets are Dedekind finite.

formula_list(sos).
% negation of Corollary DK-FIN
-subclass(FINITE,DEDEKIND).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Fri Jun 02 21:31:20 2000

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

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

3214 [] -member(0,x) | -subclass(image(K,x),x) | subclass(FINITE,x).
3284 [] subclass(image(K,DEDEKIND),DEDEKIND).
3287 [] member(0,DEDEKIND).
3288 [] -subclass(FINITE,DEDEKIND).
4345 [ur,3288,3214,3284] -member(0,DEDEKIND).
4346 [binary,4345.1,3287.1] $F.

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

clauses generated       1
Kbytes malloced      2969
user CPU time           2.42  seconds