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

% DK-0.IN                 2000 May 26
% The empty set is Dedekind finite.

formula_list(sos).
% negation of Theorem DK-0
-member(0,DEDEKIND).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Fri Jun 02 14:26:04 2000

Length of proof is 5. Level of proof is 5.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
19 [] -member(x,intersection(y,z)) | member(x,y).
23 [] -member(x,V) | member(x,y) | member(x,complement(y)).
90 [] member(0,V).
218 [] -member(x,complement(singleton(x))).
1392 [] subclass(fix(composite(x,y)),intersection(R(x),D(y))).
2703 [] equal(composite(PS,Q),composite(Q,PS)).
2715 [] equal(complement(fix(composite(Q,PS))),DEDEKIND).
2717 [] -member(0,DEDEKIND).
3212 [] equal(R(PS),complement(singleton(0))).
3604 [para_into,2717.1.2,2715.1.2] 
          -member(0,complement(fix(composite(Q,PS)))).
3606 [ur,3604,23,90] member(0,fix(composite(Q,PS))).
3638 [para_into,3606.1.2.1,2703.1.2] member(0,fix(composite(PS,Q))).
3758 [ur,3638,1,1392,demod,3212] 
          member(0,intersection(complement(singleton(0)),D(Q))).
4016 [ur,3758,19] member(0,complement(singleton(0))).
4017 [binary,4016.1,218.1] $F.

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

clauses generated  210243
Kbytes malloced      2810
user CPU time          17.14  seconds