PREFER-RIGID3 : ORDERCOMPONENTS

PREFER-RIGID3 is an argument for order-components.
If the flag ORDER-COMPONENTS is set to PREFER-RIGID3, then
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.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage