LP, the Larch Prover -- Interacting with the ordering procedures

When the automatic-ordering setting is off, LP will prompt users to confirm any extensions to the registry when as registered ordering is in use, or to select an action for an equation LP is unable to orient. When presented with a prompt like

The following sets of suggestions will allow the equation to be oriented into
a rewrite rule:

    Direction   Suggestions
    ---------   -----------
1.     ->       a > b
2.     <-       b > a

What do you want to do with the formula?

users can type ? to see a menu such as

Enter one of the following, or type < ret > to exit.
  accept[1..2]   interrupt      left-to-right  postpone       suggestions
  divide         kill           ordering       right-to-left

of possible responses, which have the following effects.

accept (or a number in the indicated range): Confirms the first (or the selected) extension to the registry. If this action is missing from the menu, no extension to the registry will orient the equation.
divide: Causes LP to assert two new equations that imply the original equation. This action is useful when an incompatible equation such as x/x = y/y cannot be oriented into a rewrite rule because each side contains a variable not present in the other side. If the user elects to divide this equation, LP will ask the user to supply a name for a new operator, for example, e; it will then declare the operator and assert two equations, x/x = e and y/y = e, both of which can be oriented (by making / higher than e) and which normalize the original equation to an identity. The resulting system is a conservative extension of the old system.
interrupt: Interrupts the ordering process and returns LP to the command level.
kill: Deletes the problematic equation from the system. This action should be used with caution, since it may change the theory associated with the current logical system.
left-to-right: Orients the equation from left to right without extending the registry. Doing this removes any guarantee of termination.
ordering: Displays the current registry (as does the display ordering command) and prompts the user for another response.
postpone: Defers the attempt to orient this equation. Whenever another equation is successfully oriented, all postponed equations are re-examined, since they may have been normalized into something more tractable.
right-to-left: Orients the equation from right to left without extending the registry. Doing this removes any guarantee of termination.
suggestions: Redisplays the LP-generated suggestions for extending the registry and prompts the user for another response.