% This is the input file for proving that the
% (strongly) valid syllogism Ferison is valid.

set(auto).

formula_list(usable).

% An E proposition No M are P:
-(exists x (M(x) & P(x))).

% An I proposition Some M are S:
exists x (M(x) & S(x)).

% The conclusion is an O proposition, viz.,
% Not all S are P, or, alternative, Some S are non-P, which is
% negated here for contradiction, yielding:
-(exists x (S(x) & -P(x))).

end_of_list.