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

% FIN-Q-OM.IN                 2000 April 29

formula_list(sos).
% negation of Theorem FIN-Q-OM
-equal(image(Q,omega),FINITE).
end_of_list.


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

Length of proof is 12. Level of proof is 7.

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

2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
301 [] -member(x,cart(y,z)) | member(first(x),y).
302 [] -member(x,cart(y,z)) | member(second(x),z).
494 [] -member(x,image(y,z)) | member(dom(y,z,x),z).
506 [] -member(x,image(y,z)) | member(pair(dom(y,z,x),x),y).
1274 [] -member(x,R(SINGLETON)) | equal(singleton(U(x)),x).
2266 [] -member(pair(x,y),CUP) | equal(union(first(x),second(x)),y).
2618 [] member(0,image(Q,omega)).
2858 [] -member(x,image(Q,omega)) | member(union(x,singleton(y)),
          image(Q,omega)).
3129 [] -member(0,x) | -subclass(image(CUP,cart(x,R(SINGLETON))),x)
           | subclass(FINITE,x).
3188 [] subclass(image(Q,omega),FINITE).
3189 [] -equal(image(Q,omega),FINITE).
4209 [] equal(notsub(image(CUP,cart(image(Q,omega),R(SINGLETON))),
          image(Q,omega)),n$).
4210 [] equal(dom(CUP,cart(image(Q,omega),R(SINGLETON)),n$),d$).
4211 [] equal(first(d$),f$).
4212 [] equal(second(d$),s$).
4214 [ur,3189,5,3188] -subclass(FINITE,image(Q,omega)).
4215 [ur,4214,3129,2618] 
          -subclass(image(CUP,cart(image(Q,omega),R(SINGLETON))),
          image(Q,omega)).
4227 [ur,4215,3,demod,4209] -member(n$,image(Q,omega)).
4228 [ur,4215,2,demod,4209] 
          member(n$,image(CUP,cart(image(Q,omega),R(SINGLETON)))).
4253 [ur,4228,506,demod,4210] member(pair(d$,n$),CUP).
4258 [ur,4228,494,demod,4210] 
          member(d$,cart(image(Q,omega),R(SINGLETON))).
4295,4294 [ur,4253,2266,demod,4211,4212] equal(union(f$,s$),n$).
4309 [ur,4258,302,demod,4212] member(s$,R(SINGLETON)).
4310 [ur,4258,301,demod,4211] member(f$,image(Q,omega)).
4381 [ur,4309,1274] equal(singleton(U(s$)),s$).
4391 [ur,4310,2858] member(union(f$,singleton(x)),image(Q,omega)).
4507 [para_into,4391.1.1.2,4381.1.1,demod,4295] 
          member(n$,image(Q,omega)).
4508 [binary,4507.1,4227.1] $F.

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

clauses generated   78938
Kbytes malloced      3065
user CPU time          11.04  seconds