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.