Input File for Studying Many-Valued Sentential Calculus

set(hyper_res).
assign(max_weight, 22).  %  limits the purge_gen weight of retained clauses
%  With OTTER 3.0.4, the following command must be modified; see Section 8.3.4.
assign(reduce_weight_limit, 100016).
%  With OTTER 3.0.4, the following command must be modified; see Section 8.3.6.
assign(max_proofs, 0).
clear(print_kept).
clear(back_sub).
assign(max_mem, 128000).
assign(report, 900).
assign(max_distinct_vars, 4).
assign(pick_given_ratio, 3).
set(order_history).
set(input_sos_first).
%  With OTTER 3.0.4, remove the following unneeded command; see Section 8.3.2.
set(print_level).
%  OTTER 3.0.4 does not accept the preceding option; level is always computed.

weight_list(pick_given).
%  Following are four lemmas to be proved.
weight(P(i(n(n(x)),x)), 2).
weight(P(i(x,n(n(x)))), 2).
weight(P(i(i(x,y),i(i(z,x),i(z,y)))), 2).
weight(P(i(i(x,y),i(n(y),n(x)))), 2).
%  Following are the axioms for many-valued.
weight(P(i(x,i(y,x))), 2).
weight(P(i(i(x,y),i(i(y,z),i(x,z)))), 2).
weight(P(i(i(i(x,y),y),i(i(y,x),x))), 2).
weight(P(i(i(n(x),n(y)),i(y,x))), 2).
%  Following is for recursive tail strategy.
weight(i($(1),$(2)),1).
end_of_list.

%  Used to complete applications of inference rules.
list(usable).
-P(i(x,y)) | -P(x) | P(y).
end_of_list.

%  Used to initiate applications of inference rules.
list(sos).
P(i(x,i(y,x))).
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(i(i(x,y),y),i(i(y,x),x))).
P(i(i(n(x),n(y)),i(y,x))).
end_of_list.

%  Used mainly to detect proof completion and to monitor progress.
list(passive).
-P(i(n(n(a)),a)) | $ANS(lemma_24).
-P(i(a,n(n(a)))) | $ANS(lemma_29).
-P(i(i(a,b),i(i(c,a),i(c,b)))) | $ANS(lemma_25).
-P(i(i(a,b),i(n(b),n(a)))) | $ANS(lemma_36).
end_of_list.

%  Following purges unwanted formulas.
list(demodulators).
(n(n(n(x))) = junk).
(i(i(x,x),y) = junk).
(i(y,i(x,x)) = junk).
(i(junk,x) = junk).
(i(x,junk) = junk).
(n(junk) = junk).
(P(junk) = $T).
end_of_list.