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

% FS-3.IN     1997 June 8

formula_list(sos).
% negation of Theorem FS-3
-(all x (member(x,FUNS) ->  subclass(x,cart(V,V)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Jul 03 22:02:12 1997

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

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

1 [] -subclass(x,y) | -member(u,x) | member(u,y).
385 [] -member(x,P(y)) | subclass(x,y).
732 [] subclass(FUNS,P(cart(V,V))).
734 [] member($c1,FUNS).
735 [] -subclass($c1,cart(V,V)).
853 [ur,734,1,732] member($c1,P(cart(V,V))).
855 [ur,735,385] -member($c1,P(cart(V,V))).
856 [binary,855.1,853.1] $F.

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

clauses generated      72
Kbytes malloced       606
user CPU time           1.54  seconds