% This propositional logic problem that was the
% "most difficult" (!) theorem proved by the original
% Logic Theorist of 1957.
% 
% Selmer Bringsjord (born 1958)
% Intro to Logic Programming and AI, Spring 1998

set(auto).
set(propositional).

formula_list(usable).

-((p -> q) <-> (-q -> -p)).

end_of_list.