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

% FIN-SC1.IN                 2000 March 15

formula_list(sos).
% negation of Theorem FIN-SC1
-equal(U(FINITE),V).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Wed Mar 15 20:37:29 2000

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

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

76 [] subclass(x,x).
77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
87 [] -subclass(V,x) | equal(x,V).
583 [] -subclass(x,y) | subclass(U(x),U(y)).
3040 [] subclass(R(SINGLETON),FINITE).
3041 [] -equal(U(FINITE),V).
3429 [] equal(U(R(SINGLETON)),V).
4025 [binary,3041.1,87.2] -subclass(V,U(FINITE)).
4027 [binary,4025.1,77.3] -subclass(V,x) | -subclass(x,U(FINITE)).
4030 [binary,4027.2,583.2] -subclass(V,U(x)) | -subclass(x,FINITE).
4033 [binary,4030.2,3040.1,demod,3429] -subclass(V,V).
4034 [binary,4033.1,76.1] $F.

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

clauses generated    1967
Kbytes malloced      2810
user CPU time           2.48  seconds