<unorder-command> ::= unorder [ <names> ]
unorder unorder nat
Even if the automatic-ordering setting is on, the unordered formulas are not immediately reordered into rewrite rules. This gives users an opportunity to change the ordering-method or the registry. The formulas will be oriented into rewrite rules in response to an explicit order command or in response to some other command that would invoke LP's automatic ordering (for example, the assert command).