% The sentential calculus (CN).
%
% {CN1, CN2, CN3} (Lukasiewicz), along with condensed detachment,
% axiomatizes the sentential calculus (the classical propositional calculus).
%
% Show that CN16, CN18, and CN19 can be derived.

set(hyper_res).
clear(back_sub).
assign(pick_given_ratio, 3).
assign(max_proofs, 3).
assign(max_weight, 16).
clear(print_kept).
set(order_history).

assign(max_mem, 1500).       % 1.5 Megabytes

% The symbols -> and - have built-in declarations, and they are used for
% clauses and formulas.  When redeclaring them for use with terms, we
% must be careful that they will still work for clauses and formulas.

op(800, yfx, ->).  % left association

list(usable).
-P(x -> y) | -P(x) | P(y).    % condensed detachment
end_of_list.

list(sos).
P(x -> y -> (y -> z -> (x -> z))).  % CN1
P(-x -> x -> x).                      % CN2
P(x -> (-x -> y)).                      % CN3
end_of_list.

list(passive).
-P(a -> a) | $Ans(CN_16).
-P(b -> (a -> b)) | $Ans(CN_18).
-P(a -> b -> c -> (b -> c)) | $Ans(CN_19).
end_of_list.