%  Input File for Studying Two-Valued Sentential Calculus with OTTER 3.0
set(hyper_res).
assign(max_weight,20).
assign(max_proofs, -1).
clear(print_kept).
% clear(for_sub).
clear(back_sub).
% assign(max_seconds, 1200).
assign(max_mem, 24000).
% assign(report, 900).
% assign(max_distinct_vars, 4).
% assign(pick_given_ratio, 3).
assign(max_given, 618).
set(order_history).
set(input_sos_first).
% set(sos_queue).
  
weight_list(pick_and_purge).
%  Following are templates corresponding to the 68 theses to be proved.
weight(P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))),2).
weight(P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))),2).
weight(P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))),2).
weight(P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))),2).
weight(P(i(i(x,y),i(i(z,x),i(i(y,u),i(z,u))))),2).
weight(P(i(i(i(n(x),y),z),i(x,z))),2).
weight(P(i(x,i(i(i(n(x),x),x),i(i(y,x),x)))),2).
weight(P(i(i(x,i(i(n(y),y),y)),i(i(n(y),y),y))),2).
weight(P(i(x,i(i(n(y),y),y))),2).
weight(P(i(i(n(x),y),i(z,i(i(y,x),x)))),2).
weight(P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))),2).
weight(P(i(i(n(x),y),i(i(y,x),x))),2).
weight(P(i(x,x)),2).
weight(P(i(x,i(i(y,x),x))),2).
weight(P(i(x,i(y,x))),2).
weight(P(i(i(i(x,y),z),i(y,z))),2).
weight(P(i(x,i(i(x,y),y))),2).
weight(P(i(i(x,i(y,z)),i(y,i(x,z)))),2).
weight(P(i(i(x,y),i(i(z,x),i(z,y)))),2).
weight(P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))),2).
weight(P(i(i(i(x,y),x),x)),2).
weight(P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))),2).
weight(P(i(i(i(x,y),z),i(i(z,x),x))),2).
weight(P(i(i(i(x,y),y),i(i(y,x),x))),2).
weight(P(i(i(i(i(x,y),y),z),i(i(i(y,u),x),z))),2).
weight(P(i(i(i(x,y),z),i(i(x,z),z))),2).
weight(P(i(i(x,i(x,y)),i(x,y))),2).
weight(P(i(i(x,y),i(i(i(x,z),u),i(i(y,u),u)))),2).
weight(P(i(i(i(x,y),z),i(i(x,u),i(i(u,z),z)))),2).
weight(P(i(i(x,y),i(i(y,i(z,i(x,u))),i(z,i(x,u))))),2).
weight(P(i(i(x,i(y,i(z,u))),i(i(z,x),i(y,i(z,u))))),2).
weight(P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))),2).
weight(P(i(n(x),i(x,y))),2).
weight(P(i(i(i(x,y),z),i(n(x),z))),2).
weight(P(i(i(x,n(x)),n(x))),2).
weight(P(i(n(n(x)),x)),2).
weight(P(i(x,n(n(x)))),2).
weight(P(i(i(x,y),i(n(n(x)),y))),2).
weight(P(i(i(i(n(n(x)),y),z),i(i(x,y),z))),2).
weight(P(i(i(x,y),i(i(y,n(x)),n(x)))),2).
weight(P(i(i(x,i(y,n(z))),i(i(z,y),i(x,n(z))))),2).
weight(P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))),2).
weight(P(i(i(x,y),i(n(y),n(x)))),2).
weight(P(i(i(x,n(y)),i(y,n(x)))),2).
weight(P(i(i(n(x),y),i(n(y),x))),2).
weight(P(i(i(n(x),n(y)),i(y,x))),2).
weight(P(i(i(i(n(x),y),z),i(i(n(y),x),z))),2).
weight(P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))),2).
weight(P(i(i(x,i(y,n(z))),i(x,i(z,n(y))))),2).
weight(P(i(i(n(x),y),i(i(x,y),y))),2).
weight(P(i(i(x,y),i(i(n(x),y),y))),2).
weight(P(i(i(x,y),i(i(x,n(y)),n(x)))),2).
weight(P(i(i(i(i(x,y),y),z),i(i(n(x),y),z))),2).
weight(P(i(i(n(x),y),i(i(x,z),i(i(z,y),y)))),2).
weight(P(i(i(i(i(x,y),i(i(y,z),z)),u),i(i(n(x),z),u))),2).
weight(P(i(i(n(x),y),i(i(z,y),i(i(x,z),y)))),2).
weight(P(i(i(x,i(n(y),z)),i(x,i(i(u,z),i(i(y,u),z))))),2).
weight(P(i(i(x,y),i(i(z,y),i(i(n(x),z),y)))),2).
weight(P(i(i(n(n(x)),y),i(x,y))),2).
weight(P(i(x,i(y,y))),2).
weight(P(i(n(i(x,x)),y)),2).
weight(P(i(i(n(x),n(i(y,y))),x)),2).
weight(P(i(n(i(x,y)),x)),2).
weight(P(i(n(i(x,y)),n(y))),2).
weight(P(i(n(i(x,n(y))),y)),2).
weight(P(i(x,i(n(y),n(i(x,y))))),2).
weight(P(i(x,i(y,n(i(x,n(y)))))),2).
weight(P(n(i(i(x,x),n(i(y,y))))),2).
end_of_list.
  
list(usable).
%  The following clause is used with hyperresolution for condensed detachment.
-P(i(x,y)) | -P(x) | P(y).
%  The following disjunctions, except those mentioning Scott,
%  are the negation of known axiom systems.
  
-P(i(p,i(q,p))) | -P(i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | -P(i(n(n(p)),p)) | 
-P(i(p,n(n(p)))) | -P(i(i(p,q),i(n(q),n(p)))) | -P(i(i(p,i(q,r)),i(q,i(p,r)))) | 
$ANSWER(step_allFrege_18_35_39_40_46_21).  % 21 is dependent.
  
-P(i(p,i(q,p))) | -P(i(i(p,i(q,r)),i(q,i(p,r)))) | 
-P(i(i(q,r),i(i(p,q),i(p,r)))) | -P(i(p,i(n(p),q))) | 
-P(i(i(p,q),i(i(n(p),q),q))) | -P(i(i(p,i(p,q)),i(p,q))) | 
$ANSWER(step_allHilbert_18_21_22_3_54_30).  % 30 is dependent.
  
-P(i(p,i(q,p))) | -P(i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | 
-P(i(i(n(p),n(q)),i(q,p))) | $ANSWER(step_allBEH_Church_FL_18_35_49).
  
-P(i(i(i(p,q),r),i(q,r))) | -P(i(i(i(p,q),r),i(n(p),r))) | 
-P(i(i(n(p),r),i(i(q,r),i(i(p,q),r)))) | $ANSWER(step_allLuka_x_19_37_59).
  
-P(i(i(i(p,q),r),i(q,r))) | -P(i(i(i(p,q),r),i(n(p),r))) | 
-P(i(i(s,i(n(p),r)),i(s,i(i(q,r),i(i(p,q),r))))) | $ANSWER(step_allWos_x_19_37_60).
  
-P(i(i(p,q),i(i(q,r),i(p,r)))) | -P(i(i(n(p),p),p)) | 
-P(i(p,i(n(p),q))) | $ANSWER(step_allLuka_1_2_3).
  
-P(i(p,p)) | -P(i(p,i(q,p))) | -P(i(i(p,i(q,r)),i(q,i(p,r)))) | 
-P(i(i(i(p,q),p),p)) | -P(i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | 
-P(i(n(n(p)),p)) | -P(i(p,n(n(p)))) | -P(i(i(p,q),i(n(q),n(p)))) | 
$ANSWER(step_allScott_orig_16_18_21_24_35_39_40_46).
  
-P(i(p,p)) | -P(i(p,i(q,p))) | -P(i(i(p,i(q,r)),i(q,i(p,r)))) | 
-P(i(i(i(p,q),p),p)) | -P(i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | 
-P(i(n(n(p)),p)) | -P(i(p,n(n(p)))) | -P(i(i(n(p),n(q)),i(q,p))) | 
$ANSWER(step_allScott_orig0_16_18_21_24_35_39_40_49).
  
end_of_list.
  
list(sos).
%  The following three are Luka, 1 2 3.
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(i(n(x),x),x)).
P(i(x,i(n(x),y))).
  
%  The following are from Frege, 18 35 21 46 39 40, with 21 dependent.
% P(i(x,i(y,x))).  %  axiom F1.
% P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  %  axiom F2.
% P(i(i(x,i(y,z)),i(y,i(x,z)))).  %  axiom F3.
% P(i(i(x,y),i(n(y),n(x)))).  %  axiom F4.
% P(i(n(n(x)),x)).  %  axiom F5.
% P(i(x,n(n(x)))).  %  axiom f6.
end_of_list.
  
list(passive).
-P(i(i(i(i(q,r),i(p,r)),s),i(i(p,q),s))) | $ANS(neg_th_04).
-P(i(i(p,i(q,r)),i(i(s,q),i(p,i(s,r))))) | $ANS(neg_th_05).
-P(i(i(p,q),i(i(i(p,r),s),i(i(q,r),s)))) | $ANS(neg_th_06).
-P(i(i(t,i(i(p,r),s)),i(i(p,q),i(t,i(i(q,r),s))))) | $ANS(neg_th_07).
-P(i(i(q,r),i(i(p,q),i(i(r,s),i(p,s))))) | $ANS(neg_th_08).
-P(i(i(i(n(p),q),r),i(p,r))) | $ANS(neg_th_09).
-P(i(p,i(i(i(n(p),p),p),i(i(q,p),p)))) | $ANS(neg_th_10).
-P(i(i(q,i(i(n(p),p),p)),i(i(n(p),p),p))) | $ANS(neg_th_11).
-P(i(t,i(i(n(p),p),p))) | $ANS(neg_th_12).
-P(i(i(n(p),q),i(t,i(i(q,p),p)))) | $ANS(neg_th_13).
-P(i(i(i(t,i(i(q,p),p)),r),i(i(n(p),q),r))) | $ANS(neg_th_14).
-P(i(i(n(p),q),i(i(q,p),p))) | $ANS(neg_th_15).
-P(i(p,p)) | $ANS(neg_th_16).
-P(i(p,i(i(q,p),p))) | $ANS(neg_th_17).
-P(i(q,i(p,q))) | $ANS(neg_th_18).
-P(i(i(i(p,q),r),i(q,r))) | $ANS(neg_th_19).
-P(i(p,i(i(p,q),q))) | $ANS(neg_th_20).
-P(i(i(p,i(q,r)),i(q,i(p,r)))) | $ANS(neg_th_21).
-P(i(i(q,r),i(i(p,q),i(p,r)))) | $ANS(neg_th_22).
-P(i(i(i(q,i(p,r)),s),i(i(p,i(q,r)),s))) | $ANS(neg_th_23).
-P(i(i(i(p,q),p),p)) | $ANS(neg_th_24).
-P(i(i(i(p,r),s),i(i(p,q),i(i(q,r),s)))) | $ANS(neg_th_25).
-P(i(i(i(p,q),r),i(i(r,p),p))) | $ANS(neg_th_26).
-P(i(i(i(p,q),q),i(i(q,p),p))) | $ANS(neg_th_27).
-P(i(i(i(i(r,p),p),s),i(i(i(p,q),r),s))) | $ANS(neg_th_28).
-P(i(i(i(p,q),r),i(i(p,r),r))) | $ANS(neg_th_29).
-P(i(i(p,i(p,q)),i(p,q))) | $ANS(neg_th_30).
-P(i(i(p,s),i(i(i(p,q),r),i(i(s,r),r)))) | $ANS(neg_th_31).
-P(i(i(i(p,q),r),i(i(p,s),i(i(s,r),r)))) | $ANS(neg_th_32).
-P(i(i(p,s),i(i(s,i(q,i(p,r))),i(q,i(p,r))))) | $ANS(neg_th_33).
-P(i(i(s,i(q,i(p,r))),i(i(p,s),i(q,i(p,r))))) | $ANS(neg_th_34).
-P(i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | $ANS(neg_th_35).
-P(i(n(p),i(p,q))) | $ANS(neg_th_36).
-P(i(i(i(p,q),r),i(n(p),r))) | $ANS(neg_th_37).
-P(i(i(p,n(p)),n(p))) | $ANS(neg_th_38).
-P(i(n(n(p)),p)) | $ANS(neg_th_39).
-P(i(p,n(n(p)))) | $ANS(neg_th_40).
-P(i(i(p,q),i(n(n(p)),q))) | $ANS(neg_th_41).
-P(i(i(i(n(n(p)),q),r),i(i(p,q),r))) | $ANS(neg_th_42).
-P(i(i(p,q),i(i(q,n(p)),n(p)))) | $ANS(neg_th_43).
-P(i(i(s,i(q,n(p))),i(i(p,q),i(s,n(p))))) | $ANS(neg_th_44).
-P(i(i(s,i(q,p)),i(i(n(p),q),i(s,p)))) | $ANS(neg_th_45).
-P(i(i(p,q),i(n(q),n(p)))) | $ANS(neg_th_46).
-P(i(i(p,n(q)),i(q,n(p)))) | $ANS(neg_th_47).
-P(i(i(n(p),q),i(n(q),p))) | $ANS(neg_th_48).
-P(i(i(n(p),n(q)),i(q,p))) | $ANS(neg_th_49).
-P(i(i(i(n(q),p),r),i(i(n(p),q),r))) | $ANS(neg_th_50).
-P(i(i(p,i(q,r)),i(p,i(n(r),n(q))))) | $ANS(neg_th_51).
-P(i(i(p,i(q,n(r))),i(p,i(r,n(q))))) | $ANS(neg_th_52).
-P(i(i(n(p),q),i(i(p,q),q))) | $ANS(neg_th_53).
-P(i(i(p,q),i(i(n(p),q),q))) | $ANS(neg_th_54).
-P(i(i(p,q),i(i(p,n(q)),n(p)))) | $ANS(neg_th_55).
-P(i(i(i(i(p,q),q),r),i(i(n(p),q),r))) | $ANS(neg_th_56).
-P(i(i(n(p),r),i(i(p,q),i(i(q,r),r)))) | $ANS(neg_th_57).
-P(i(i(i(i(p,q),i(i(q,r),r)),s),i(i(n(p),r),s))) | $ANS(neg_th_58).
-P(i(i(n(p),r),i(i(q,r),i(i(p,q),r)))) | $ANS(neg_th_59).
-P(i(i(s,i(n(p),r)),i(s,i(i(q,r),i(i(p,q),r))))) | $ANS(neg_th_60).
-P(i(i(p,r),i(i(q,r),i(i(n(p),q),r)))) | $ANS(neg_th_61).
-P(i(i(n(n(p)),q),i(p,q))) | $ANS(neg_th_62).
-P(i(q,i(p,p))) | $ANS(neg_th_63).
-P(i(n(i(p,p)),q)) | $ANS(neg_th_64).
-P(i(i(n(q),n(i(p,p))),q)) | $ANS(neg_th_65).
-P(i(n(i(p,q)),p)) | $ANS(neg_th_66).
-P(i(n(i(p,q)),n(q))) | $ANS(neg_th_67).
-P(i(n(i(p,n(q))),q)) | $ANS(neg_th_68).
-P(i(p,i(n(q),n(i(p,q))))) | $ANS(neg_th_69).
-P(i(p,i(q,n(i(p,n(q)))))) | $ANS(neg_th_70).
-P(n(i(i(p,p),n(i(q,q))))) | $ANS(neg_th_71).
end_of_list.
  
% list(demodulators).
%  (n(n(x)) = junk).
%  (n(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(junk,x) = junk).
% (i(x,junk) = junk).
% (n(junk) = junk).
% (P(junk) = $T).
% end_of_list.