% The sentential calculus (CN).
%
% {CN1, CN2, CN3} (Lukasiewicz), along with condensed detachment,
% axiomatizes the sentential calculus (the classical propositional calculus).
%

set(auto).

list(usable).
-P(i(x,y)) | -P(x) | P(y).      % condensed detachment

P(i(i(x,y),i(i(y,z),i(x,z)))).  % CN1
P(i(i(n(x),x),x)).              % CN2
P(i(x,i(n(x),y))).              % CN3

-P(i(i(i(a,b),c),i(b,c))) | $Ans(CN_19).
end_of_list.