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