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

% FIN-SC6.IN                 2000 April 3

formula_list(sos).
% negation of Corollary FIN-SC6
-(all x y (member(U(x),FINITE) -> member(x,FINITE))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon Apr 03 23:13:25 2000

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

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

587 [] subclass(x,P(U(x))).
3087 [] -member(x,FINITE) | -subclass(y,x) | member(y,FINITE).
3110 [] -member(x,FINITE) | member(P(x),FINITE).
3111 [] member(U($c2),FINITE).
3112 [] -member($c2,FINITE).
4104 [ur,3111,3110] member(P(U($c2)),FINITE).
4122 [ur,3112,3087,587] -member(P(U($c2)),FINITE).
4123 [binary,4122.1,4104.1] $F.

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

clauses generated    2409
Kbytes malloced      2842
user CPU time           2.31  seconds