----- SUMMARY FOR THEOREM FS-RP-1 IN DIRECTORY Q:\FS -----

% Q:\FS\FS-RP-1.IN              1997 August 23
% FUNS is not a set.

formula_list(sos).
% negation of Theorem FS-RP-1
-(all x -member(FUNS,x)).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Aug 24 11:13:32 1997

Length of proof is 2. Level of proof is 2.

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

1 [] -subclass(x,y) | -member(u,x) | member(u,y).
4 [] subclass(x,V).
56 [] -member(x,V) | member(U(x),V).
659 [] -member(cart(V,V),x).
785 [] member(FUNS,$c1).
938 [] equal(U(FUNS),cart(V,V)).
940 [ur,785,1,4] member(FUNS,V).
949 [ur,940,56,demod,938] member(cart(V,V),V).
950 [binary,949.1,659.1] $F.

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

clauses generated     221
Kbytes malloced       734
user CPU time           1.59  seconds