### Input File for Finding a Short Proof of MV5 from MV1-4

For additional input files and a copy of OTTER, see A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, L. Wos with G. W. Pieper, World Scientific, 1999

% Trying for a short proof of MV5 from MV1-4 avoiding 2.22 3.5 3.51.
% This file yields a 30-step proof.
% The goal is to find a proof strictly shorter than length 30.
set(hyper_res).
assign(max_weight,48).
assign(change_limit_after,2000).
assign(new_max_weight,24).
assign(max_proofs,-1).
clear(print_kept).

% set(process_input).
set(ancestor_subsume).
set(back_sub).
clear(print_back_sub).
assign(max_distinct_vars,4).
assign(pick_given_ratio,4).
% assign(max_seconds,30).
assign(max_mem,480000).
assign(report,3600).
set(order_history).
set(input_sos_first).
assign(heat,0).
% assign(dynamic_heat_weight,0).

weight_list(pick_and_purge).
% Following is a 32-step proof of MV5 avoiding 3 lemmas.
weight(P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))),2).
weight(P(i(i(i(x,y),z),i(y,z))),2).
weight(P(i(i(i(x,y),z),i(i(n(y),n(x)),z))),2).
weight(P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))),2).
weight(P(i(n(x),i(x,y))),2).
weight(P(i(x,i(i(x,y),y))),2).
weight(P(i(i(n(x),n(i(y,z))),i(z,x))),2).
weight(P(i(i(i(x,y),z),i(n(x),z))),2).
weight(P(i(i(x,i(y,z)),i(y,i(x,z)))),2).
weight(P(i(i(i(n(x),y),z),i(i(i(x,u),y),z))),2).
weight(P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))),2).
weight(P(i(i(x,y),i(i(z,x),i(z,y)))),2).
weight(P(i(i(i(x,y),n(z)),i(z,x))),2).
weight(P(i(i(x,i(y,z)),i(i(u,x),i(y,i(u,z))))),2).
weight(P(i(i(x,i(y,z)),i(i(z,u),i(x,i(y,u))))),2).
weight(P(i(i(x,i(i(y,z),z)),i(i(z,y),i(x,y)))),2).
weight(P(i(i(i(x,y),z),i(i(x,i(i(y,u),u)),i(i(u,y),z)))),2).
weight(P(i(i(i(x,y),i(i(n(z),u),u)),i(i(u,n(z)),i(z,x)))),2).
weight(P(i(i(n(x),i(i(n(y),z),z)),i(i(z,n(y)),i(y,x)))),2).
weight(P(i(i(x,n(y)),i(y,n(x)))),2).
weight(P(i(i(x,i(y,n(z))),i(z,i(x,n(y))))),2).
weight(P(i(i(i(x,y),i(z,n(u))),i(u,i(n(x),n(z))))),2).
weight(P(i(i(x,y),i(z,i(n(y),n(x))))),2).
weight(P(i(i(i(n(x),n(y)),z),i(i(y,x),z))),2).
weight(P(i(i(x,i(y,z)),i(u,i(x,i(n(z),n(y)))))),2).
weight(P(i(x,i(y,i(n(z),n(i(y,z)))))),2).
weight(P(i(x,i(n(y),n(i(x,y))))),2).
weight(P(i(i(x,y),i(n(z),i(x,n(i(y,z)))))),2).
weight(P(i(n(x),i(i(n(y),n(i(z,u))),n(i(i(u,y),x))))),2).
weight(P(i(i(n(i(i(x,y),x)),n(y)),i(y,x))),2).
weight(P(i(i(x,i(i(y,x),y)),i(x,y))),2).
weight(P(i(i(i(x,y),i(y,x)),i(y,x))),2).
% Just the implicational axioms: A1 - A3
weight(P(i(x,i(y,x))),3).
weight(P(i(i(x,y),i(i(y,z),i(x,z)))),3).
weight(P(i(i(i(x,y),y),i(i(y,x),x))),3).
% Following is MV4.
weight(P(i(i(n(x),n(y)),i(y,x))),3).
% Following are 2 steps from a 33-step 5-var proof of MV5, not in the preceding 33-step proof.
weight(P(i(i(x,i(y,z)),i(u,i(y,i(n(z),n(x)))))),4).
weight(P(i(x,i(i(n(y),n(i(z,u))),i(n(v),n(i(i(u,y),v)))))),4).
end_of_list.

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

list(sos).
% Just the implicational axioms: A1 - A3
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))).
% Following is MV4.
P(i(i(n(x),n(y)),i(y,x))).
end_of_list.

list(passive).
% To prove MV5 dependent on MV1-MV4, whose denial is the following.
% MV5 is P(i(i(i(x,y),i(y,x)),i(y,x))).
-P(i(i(i(a,b),i(b,a)),i(b,a))) | \$ANS(MV_5).
end_of_list.

list(demodulators).
(P(i(i(x,y),i(i(z,x),i(z,y)))) = junk).
(P(i(n(x),i(x,y))) = junk).
% (P(i(i(i(x,y),z),i(n(x),z))) = junk).
% Following 3 to block, 2.22 3.5 3.51.
(P(i(i(i(x,y),i(z,y)),i(i(y,x),i(z,x)))) = junk).
(P(i(i(x,y),i(n(y),n(x)))) = junk).
(P(i(i(i(x,y),i(x,z)),i(i(y,x),i(y,z)))) = junk).
% (n(n(n(x))) = junk).
(n(n(x)) = junk).
% (i(i(x,x),y) = junk).
% (i(y,i(x,x)) = junk).
% (i(n(i(x,x)),y) = junk).
% (i(y,n(i(x,x))) = junk).
(i(x,junk) = junk).
(i(junk,x) = junk).
(n(junk) = junk).
(P(junk) = \$T).
end_of_list.

list(hot).
-P(i(x,y)) | -P(x) | P(y).
% Following is MV1 -- MV4.
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.