----- SUMMARY FOR THEOREM FS-FU-DO IN DIRECTORY Q:\fs -----

% FS-FU-DO.IN                 2000 March 2
% Corollary of Theorem FS-FU

formula_list(sos).
% negation of Corollary FS-FU-DO
-(all x ((FUNCTION(x) & member(D(x),V)) -> member(x,FUNS))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Mar 02 10:51:59 2000

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

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

1331 [] -FUNCTION(x) | -member(D(x),V) | member(x,V).
2258 [] -FUNCTION(x) | -member(x,V) | member(x,FUNS).
2259 [] FUNCTION($c1).
2260 [] member(D($c1),V).
2261 [] -member($c1,FUNS).
3037 [ur,2260,1331,2259] member($c1,V).
3039 [ur,2261,2258,2259] -member($c1,V).
3040 [binary,3039.1,3037.1] $F.

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

clauses generated    2248
Kbytes malloced      2171
user CPU time           1.81  seconds