----- SUMMARY FOR THEOREM FS-SC IN DIRECTORY Q:\FS -----

% FS-SC.IN                  1997 July 7
% A demodulator for FUNS

formula_list(sos).
% negation of Theorem FS-SC
-equal(U(FUNS),cart(V,V)).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon Jul 07 12:05:59 1997

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

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

1 [] -subclass(x,y) | -member(u,x) | member(u,y).
2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
7 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
115 [] -member(x,V) | member(x,singleton(x)).
374 [] -member(z,y) | -member(y,x) | member(z,U(x)).
397 [] subclass(cart(x,y),P(P(union(x,P(y))))).
774 [] -member(x,cart(V,V)) | member(singleton(x),FUNS).
776 [] subclass(U(FUNS),cart(V,V)).
781 [] -equal(U(FUNS),cart(V,V)).
808 [] equal(union(x,x),x).
851 [] equal(P(V),V).
934 [ur,781,7,776] -subclass(cart(V,V),U(FUNS)).
943 [ur,934,3] -member(notsub(cart(V,V),U(FUNS)),U(FUNS)).
944 [ur,934,2] member(notsub(cart(V,V),U(FUNS)),cart(V,V)).
967 [ur,944,774] member(singleton(notsub(cart(V,V),U(FUNS))),FUNS).
973 [ur,944,1,397,demod,851,808,851,851] 
          member(notsub(cart(V,V),U(FUNS)),V).
1021 [ur,967,374,943] 
          -member(notsub(cart(V,V),U(FUNS)),
          singleton(notsub(cart(V,V),U(FUNS)))).
1037 [ur,973,115] member(notsub(cart(V,V),U(FUNS)),
          singleton(notsub(cart(V,V),U(FUNS)))).
1038 [binary,1037.1,1021.1] $F.

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

clauses generated    4721
Kbytes malloced       830
user CPU time           2.63  seconds