----- SUMMARY FOR THEOREM FINC-SC IN DIRECTORY Q:\finite -----

% FINC-SC.IN                 2000 March 15
% a demodulator

formula_list(sos).
% negation of Theorem FINC-SC
-equal(U(complement(FINITE)),V).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Wed Mar 15 22:07:04 2000

Length of proof is 11. Level of proof is 8.

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

2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
23 [] -member(x,V) | member(x,y) | member(x,complement(y)).
53 [] member(omega,V).
76 [] subclass(x,x).
87 [] -subclass(V,x) | equal(x,V).
142 [] subclass(x,union(x,y)).
143 [] subclass(x,union(y,x)).
244 [] -member(x,V) | -subclass(singleton(x),y) | member(x,y).
582 [] -member(x,y) | -member(y,z) | member(x,U(z)).
603 [] -member(x,V) | member(union(x,singleton(y)),V).
1636 [] -member(x,V) | equal(U(complement(x)),V).
3043 [] -member(omega,FINITE).
3044 [] -member(x,FINITE) | -subclass(y,x) | member(y,FINITE).
3045 [] -equal(U(complement(FINITE)),V).
4030 [] equal(notsub(V,U(complement(FINITE))),n$).
4032 [binary,3045.1,87.2] -subclass(V,U(complement(FINITE))).
4034 [binary,4032.1,3.2,demod,4030] 
          -member(n$,U(complement(FINITE))).
4035 [binary,4032.1,2.2,demod,4030] member(n$,V).
4041,4040 [binary,4035.1,1636.1] equal(U(complement(n$)),V).
4054 [ur,4035,244,143] member(n$,union(x,singleton(n$))).
4183 [para_into,4040.1.2,87.2.2,demod,4041] 
          equal(V,x) | -subclass(V,x).
4306 [ur,4054,582,4034] 
          -member(union(x,singleton(n$)),complement(FINITE)).
4402 [para_from,4183.1.1,53.1.2] member(omega,x) | -subclass(V,x).
4473 [binary,4402.1,603.1,unit_del,76] 
          member(union(omega,singleton(x)),V).
5057 [ur,4306,23,4473] member(union(omega,singleton(n$)),FINITE).
5060 [ur,5057,3044,3043] -subclass(omega,union(omega,singleton(n$))).
5061 [binary,5060.1,142.1] $F.

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

clauses generated  398187
Kbytes malloced      3161
user CPU time          48.06  seconds