How do I Get OTTER to Generate All Tautologies of a Certain Length?

Question

In OTTER an input like the following could get used to generate the bracket types of the wffs of length 13 (length is the number of symbols which are not parentheses or predicate symbols), where i(x,y) can get read as "x implies y".

set(hyper_res).
clear(for_sub).
clear(back_sub).
assign(max_weight, 14).

list(sos).
-P(x) | -P(y) | P(i(x,y)).
end_of_list.

list(usable).
P(x).
end_of_list.

It's also possible to test whether or not a formula is a tautology with an input like this:

 set(hyper_res).
 assign(stats_level, 1).
 clear(print_kept).

 list(usable).
 P(0).
 P(1).
 -P(x) | -P(y) | P(i(x,y)).
 end_of_list.

 list(sos).
 -P(x) | -P(y) | -P(z) | -P(u) | -P(v) |   D2(P(i(i(i(x,y),i(i(i(n(z),n(u)),v),z)),i(w,i(i(z,x),i(u,x))))),1).
 end_of_list.

 list(demodulators).
 i(0,0)=1.
 i(0,1)=1.
 i(1,0)=0.
 i(1,1)=1.
 end_of_list.

 list(passive).
 D2(x,x).
 end_of_list.

Update: the following works as an input to generate all formulas up to re-lettering of length 7 without subsumption on, which seems useful.

 set(hyper_res).
 set(print_lists_at_end).
 assign(stats_level,0).

 list(sos).
 %generates all relevant possibilities
 -P(i(i(i(x,y),z),u)) | -Q(x,y,z,u) | R(i(i(i(x,y),z),u)).
 -P(i(i(x,i(y,z)),u)) | -Q(x,y,z,u) | R(i(i(x,i(y,z)),u)).
 -P(i(i(x,y),i(z,u))) | -Q(x,y,z,u) | R(i(i(x,y),i(z,u))).
 -P(i(x,i(i(y,z),u))) | -Q(x,y,z,u) | R(i(x,i(i(y,z),u))).
 -P(i(x,i(y,i(z,u)))) | -Q(x,y,z,u) | R(i(x,i(y,i(z,u)))).

 end_of_list.

 list(usable).
 % bracket types
 P(i(i(i(x,y),z),u)).
 P(i(i(x,i(y,z)),u)).
 P(i(i(x,y),i(z,u))).
 P(i(x,i(i(y,z),u))).
 P(i(x,i(y,i(z,u)))).
 %relevant permutations
 Q(x,y,z,u).
 Q(x,y,z,z).
 Q(x,y,z,y).
 Q(x,y,z,x).
 Q(x,y,y,z).
 Q(x,y,y,y).
 Q(x,y,y,x).
 Q(x,y,x,z).
 Q(x,y,x,y).
 Q(x,y,x,x).
 Q(x,x,y,z).
 Q(x,x,y,y).
 Q(x,x,y,x).
 Q(x,x,x,y).
 Q(x,x,x,x).
 end_of_list.

But, I'm still not able to combine the above with some sort of input to test all of those tautologies. How can we get OTTER to generate all formulas up to a certain length, then test those formulas of a certain length as tautologies in a single run such that we only have variables in OTTER, x, y, z, u, w, v5, v6, ..., vn, in the formula, and then print those tautologies? What would be an example of an input where this works for say formulas with length 7?

Background: I'm wanting [to try and find candidates for single axioms for the implicational propositional calculus of length 13... edit, there's only one axiom and the literature has indicated this for a while], as well as find candidate for single axioms for the conditional-negation (C-N) classical propositional of length 21 (or shorter?). If there exists a way to combine such an input with a model checker like Mace4, Mace2 such that candidates can get eliminated more efficiently and output those candidates in a form usable in proof-finding with OTTER that would also come as helpful, and if you can do that, I'll try and add a bounty to this question and grant you those points if you find such a program.

(see edits for more failed attempts if you like).

Answer 1

I'm still interested in how we might combine the above with Mace2 or Mace4. Also, this doesn't indicate how we might get the generation of the bracket types, all of the possibilities of a certain length, and testing for tautologies down in a single run. Here's an input to find all tautologies of length 7:

 set(hyper_res). % hyperresolution rule of inference
 assign(max_proofs,-1).
 clear(for_sub).
 clear(back_sub). % the last two clear forward subsumption and back subsumption
 assign(max_weight,8).
 clear(print_kept). % clears kept formulas

 weight_list(pick_and_purge). 
 % these get weighted to keep weight down for the entire run
 weight(Y1(1,i(i(i(x,y),z),u)),1).
 weight(Y2(1,i(i(x,i(y,z)),u)),1).
 weight(Y3(1,i(i(x,y),i(z,u))),1).
 weight(Y4(1,i(x,i(i(y,z),u))),1).
 weight(Y5(1,i(x,i(y,i(z,u)))),1).
 end_of_list.


 list(sos). % set of support list
 %generates all relevant possibilities
 -P(i(i(i(x,y),z),u)) | -Q(x,y,z,u) | R(i(i(i(x,y),z),u)).
 -P(i(i(x,i(y,z)),u)) | -Q(x,y,z,u) | R(i(i(x,i(y,z)),u)).
 -P(i(i(x,y),i(z,u))) | -Q(x,y,z,u) | R(i(i(x,y),i(z,u))).
 -P(i(x,i(i(y,z),u))) | -Q(x,y,z,u) | R(i(x,i(i(y,z),u))).
 -P(i(x,i(y,i(z,u)))) | -Q(x,y,z,u) | R(i(x,i(y,i(z,u)))).
 % will infer to Yx(1, r), where "r" indicates a formula,
 % and "x" indicates the bracket type of the formula
 -R(i(i(i(x,y),z),u)) | -X(x) | -X(y) | -X(z) | -X(u) | Y1(1,i(i(i(x,y),z),u)).
 -R(i(i(x,i(y,z)),u)) | -X(x) | -X(y) | -X(z) | -X(u) | Y2(1,i(i(x,i(y,z)),u)).
 -R(i(i(x,y),i(z,u))) | -X(x) | -X(y) | -X(z) | -X(u) | Y3(1,i(i(x,y),i(z,u))).
 -R(i(x,i(i(y,z),u))) | -X(x) | -X(y) | -X(z) | -X(u) | Y4(1,i(x,i(i(y,z),u))).
 -R(i(x,i(y,i(z,u)))) | -X(x) | -X(y) | -X(z) | -X(u) | Y5(1,i(x,i(y,i(z,u)))).
 end_of_list.

break

 list(usable).
 % bracket types
 P(i(i(i(x,y),z),u)).
 P(i(i(x,i(y,z)),u)).
 P(i(i(x,y),i(z,u))).
 P(i(x,i(i(y,z),u))).
 P(i(x,i(y,i(z,u)))).
 %relevant permutations of the variables...
 %(Q(y,x,y,x) and Q(x,y,x,y) are the same permutation,
 % and in general, in OTTER x is always the first variable,
 % one of {x, y} is the second, one of {x, y, z} is the third, etc.)
 Q(x,y,z,u).
 Q(x,y,z,z).
 Q(x,y,z,y).
 Q(x,y,z,x).
 Q(x,y,y,z).
 Q(x,y,y,y).
 Q(x,y,y,x).
 Q(x,y,x,z).
 Q(x,y,x,y).
 Q(x,y,x,x).
 Q(x,x,y,z).
 Q(x,x,y,y).
 Q(x,x,y,x).
 Q(x,x,x,y).
 Q(x,x,x,x).
 % truth values
 X(0).
 X(1).
 end_of_list.

break

 list(demodulators). %two equations to demodulate the Yx formulas
 i(0,x)=1.
 i(1,y)=y.
 end_of_list.
 list(passive). %negations of Yx(1,0).
 -Y1(1,0).
 -Y2(1,0).
 -Y3(1,0).
 -Y4(1,0).
 -Y5(1,0).
 end_of_list. 

OTTER then proves all formulas of length 7 that are not tautologies. Therefore, any formulas that remain in the list of givens, but have not gotten proved are tautologies of length 7 (or equivalently weight 8).