When T or PATHNUM, the components of a jform node will be

rearranged in order of the number of paths which lie below them (go

through them).

When T-REVERSED or PATHNUM-REVERSED, the components of a jform node will be

rearranged in reverse order of the number of paths which lie below them (go

through them).

When NIL or COMMON, then the jform of the current eproof will not be modified

by the mating search;

When REVERSE, the order of the components in the jform of current eproof will

be reversed;

When PREFER-RIGID2, the order of the components in the jform of the current

eproof will be sorted in terms of the number of rigid literals in a jform

before beginning the mating search.

When PREFER-RIGID3, the components in the jform of the current eproof will

be sorted as for PREFER-RIGID2, but with preference given to literals that

arise from DUAL rewriting.

(PREFER-RIGID1 is still available; it is an obsolete version of PREFER-RIGID2.)

ORDER-COMPONENTS takes values of type ORDERCOM.

It belongs to subjects MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 IMPORTANT JFORMS MATING-SEARCH .

Its default value is T

Its current value is T.

The file order-components is used to rearrange the current

jform with the help of some heuristics.

/home/theorem/tps/bin/order-components.fasl is part of module MS88.

© 1988-99, Carnegie Mellon University.