The order command directs LP to attempt to orient formulas into rewrite rules. When the automatic-ordering setting is on , LP attempts to orient formulas into rewrite rules automatically. When it is off , LP orients formulas only in response to an explicit order or complete command. If the current ordering method is a registered or polynomial ordering, the order command also attempts to orient the formulas into a provably terminating set of rewrite rules. If the current ordering method is a brute-force ordering, the order command may orient the formulas into a nonterminating set of rewrite rules.
Users can interrupt and resume the operation of the order command.