Begin mating search MS91-6 on the current expansion proof.

Primitive substitutions and duplications are performed systematically,

with multiple jforms being worked on simultaneously. On each

particular jform, the search procedure MS88 is used. The flags

MAX-SEARCH-LIMIT and SEARCH-TIME-LIMIT are used to control the amount

of time spent on each jform.

The order in which the possible jforms are considered depends on a

number of flags. Firstly, the primitive substitutions which are generated

are determined by the values of MAX-PRIM-DEPTH, MIN-PRIM-DEPTH,

PRIM-QUANTIFIER and NEG-PRIM-SUB. If DUP-ALLOWED is T, then additional

options are generated corresponding to duplicated quantifiers. These

options are then combined into sets; because there can be many such sets,

the flag NEW-OPTION-SET-LIMIT controls how many are generated at once.

Each set is given a weighting (see flags WEIGHT-x-COEFFICIENT and

WEIGHT-x-FN, for x = A,B,C), and the lowest-weighted set is chosen

for searching. If the weight of the lowest-weighted set is too large,

TPS may generate more sets; the interpretation of "too large" is given

by MS91-WEIGHT-LIMIT-RANGE. If the search fails, it will be discarded;

if it runs out of time then it will be re-weighted to be continued

later (see RECONSIDER-FN).

The command format for MS91-6 is:

<Mate>MS91-6

Flags relevant to the MS91-6 mating-search procedure.

© 1988-99, Carnegie Mellon University.