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

% FIN-SS.IN                 2000 March 10

formula_list(sos).
% negation of Theorem FIN-SS
-(all x member(singleton(x),FINITE)).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Fri Mar 10 18:58:48 2000

Length of proof is 14. Level of proof is 10.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
23 [] -member(x,V) | member(x,y) | member(x,complement(y)).
77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
215 [] member(singleton(x),V).
235 [] -subclass(x,singleton(y)) | equal(x,0)
           | equal(singleton(y),x).
243 [] -equal(x,0) | -member(x,complement(singleton(0))).
479 [] subclass(image(x,y),R(x)).
492 [] -member(x,image(y,z)) | member(dom(y,z,x),z).
504 [] -member(x,image(y,z)) | member(pair(dom(y,z,x),x),y).
580 [] -member(x,U(y)) | member(x,ran(E,x,y)).
581 [] -member(x,U(y)) | member(ran(E,x,y),y).
1500 [] -member(pair(x,x),PS).
1501 [] -member(pair(x,y),PS) | subclass(x,y).
2979 [] -member(x,subvar(y)) | subclass(x,image(y,x)).
3019 [] equal(complement(U(subvar(PS))),FINITE).
3021 [] -member(singleton($c1),FINITE).
3447 [] equal(R(PS),complement(singleton(0))).
4002 [] equal(ran(E,singleton(x),subvar(PS)),r$(x)).
4003 [] equal(dom(PS,r$(x),singleton(x)),d$(x)).
4004 [para_into,3021.1.2,3019.1.2] 
          -member(singleton($c1),complement(U(subvar(PS)))).
4005 [ur,4004,23,215] member(singleton($c1),U(subvar(PS))).
4006 [ur,4005,581,demod,4002] member(r$($c1),subvar(PS)).
4007 [ur,4005,580,demod,4002] member(singleton($c1),r$($c1)).
4010 [ur,4006,2979] subclass(r$($c1),image(PS,r$($c1))).
4024 [ur,4010,77,479,demod,3447] 
          subclass(r$($c1),complement(singleton(0))).
4025 [ur,4010,1,4007] member(singleton($c1),image(PS,r$($c1))).
4051 [ur,4025,504,demod,4003] 
          member(pair(d$($c1),singleton($c1)),PS).
4052 [ur,4025,492,demod,4003] member(d$($c1),r$($c1)).
4084 [ur,4051,1501] subclass(d$($c1),singleton($c1)).
4088 [ur,4052,1,4024] member(d$($c1),complement(singleton(0))).
4121 [ur,4088,243] -equal(d$($c1),0).
4144,4143 [ur,4121,235,4084] equal(singleton($c1),d$($c1)).
4148 [back_demod,4051,demod,4144] member(pair(d$($c1),d$($c1)),PS).
4149 [binary,4148.1,1500.1] $F.

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

clauses generated   96527
Kbytes malloced      2842
user CPU time           9.94  seconds