 SYNOPSIS

Determines skew in MESON proof tree search limits.
 DESCRIPTION

This is one of several parameters determining the behavior of MESON,
MESON_TAC and related rules and tactics. During search, MESON successively
searches for proofs of larger and larger `size'. The ``skew'' value determines
what proportion of the entire proof size is permitted in the lefthand half of
the list of subgoals. The symmetrical value is 2 (meaning one half), the
default setting of 3 (one third) seems generally better because it can cut
down on redundancy in proofs.
 FAILURE CONDITIONS

Not applicable.
 USES

For users requiring fine control over the algorithms used in MESON's
firstorder proof search.
 COMMENTS

For more details of MESON's search strategy, see Harrison's paper
``Optimizing Proof Search in Model Elimination'', CADE13, 1996.
 SEE ALSO

meson_brand, meson_chatty, meson_dcutin, meson_depth, meson_prefine,
meson_split_limit,