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

set(auto).

formula_list(usable).
% An A proposition All M are P:
all x (M(x) -> P(x)).

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

% The conclusion is another A proposition, viz.,
% All S are P, which is negated here for contradiction.
-(all x (S(x) -> P(x))).
end_of_list.