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

set(auto).

formula_list(usable).

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

% All S are M:
all x (S(x) -> M(x)).

% And now the denial, for contradiction, of
% No S are P -- to show that this E proposition
% does indeed follow.
exists x (S(x) & P(x)).

end_of_list.