----- SUMMARY FOR THEOREM FIN-RASG IN DIRECTORY Q:\finite -----

% FIN-RASG.IN                 2000 March 10
% Restatement of FIN-SS without variables.

formula_list(sos).
% negation of Corollary FIN-RASG
-subclass(R(SINGLETON),FINITE).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Mar 11 00:56:54 2000

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

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

2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
1264 [] -member(x,R(SINGLETON)) | equal(singleton(U(x)),x).
3022 [] member(singleton(x),FINITE).
3023 [] -subclass(R(SINGLETON),FINITE).
4004 [] equal(notsub(R(SINGLETON),FINITE),n$).
4007 [ur,3023,3,demod,4004] -member(n$,FINITE).
4008 [ur,3023,2,demod,4004] member(n$,R(SINGLETON)).
4011 [ur,4008,1264] equal(singleton(U(n$)),n$).
4017 [para_from,4011.1.1,3022.1.1] member(n$,FINITE).
4018 [binary,4017.1,4007.1] $F.

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

clauses generated    7144
Kbytes malloced      2778
user CPU time           2.47  seconds