Begin mating search MS91-7 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 MS90-3 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-7 is:

<Mate>MS91-7

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

© 1988-99, Carnegie Mellon University.