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

% FIN-Q-2.IN                 2000 April 29

formula_list(sos).
% negation of Corollary FIN-Q-2
-subclass(image(Q,omega),FINITE).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Apr 30 01:21:45 2000

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

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

76 [] subclass(x,x).
77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
518 [] -subclass(x,y) | subclass(image(z,x),image(z,y)).
3187 [] subclass(omega,FINITE).
3188 [] -subclass(image(Q,omega),FINITE).
4207 [] equal(image(Q,FINITE),FINITE).
4209 [binary,3188.1,77.3] 
          -subclass(image(Q,omega),x) | -subclass(x,FINITE).
4216 [binary,4209.1,518.2] 
          -subclass(image(Q,x),FINITE) | -subclass(omega,x).
4226 [binary,4216.2,3187.1,demod,4207] -subclass(FINITE,FINITE).
4227 [binary,4226.1,76.1] $F.

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

clauses generated    1824
Kbytes malloced      2937
user CPU time           2.64  seconds