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

% FIN-PC3.IN                 2000 April 2

formula_list(sos).
% negation of Corollary FIN-PC3
-(all x (member(x,FINITE) -> member(P(x),FINITE))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Apr 02 23:05:09 2000

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

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
1926 [] -member(x,image(inverse(POWER),y)) | member(P(x),y).
3109 [] subclass(FINITE,image(inverse(POWER),FINITE)).
3110 [] member($c1,FINITE).
3111 [] -member(P($c1),FINITE).
4105 [ur,3110,1,3109] member($c1,image(inverse(POWER),FINITE)).
4106 [ur,3111,1926] -member($c1,image(inverse(POWER),FINITE)).
4107 [binary,4106.1,4105.1] $F.

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

clauses generated    2400
Kbytes malloced      2842
user CPU time           2.25  seconds