% Demo for very simple types.
% David A. Wheeler
% Released to the public domain.
% Usage:
%   prover9 -f *.in > *.out

% Use prolog naming format (initial uppercase is variable):
set(prolog_style_variables).


formulas(assumptions).
 % human(X) is true if X is human.
 human(abraham_lincoln).

 % penguin(X) is true if X is a penguin.
 % This isn't used in the proof, but it demonstrates the idea.
 penguin(tux).

 % Any X cannot be BOTH a human AND a penguin.
 -(human(X) & penguin(X)).
end_of_list.

% Simple demonstration, to show that it works:

formulas(goals).
 % Prove that abraham lincoln is not a penguin:
 -penguin(abraham_lincoln).
end_of_list.