An

LP automatically recognizes the formula `x ~= t`, where `t` is a term not
involving the variable `x`, as inconsistent. Thus, LP rules out empty
sorts. It also recognizes the formulas `false` and `b = t`, where `t`
is a term not involving the boolean variable `b`, as inconsistent. Thus,
the boolean sort contains two distinct values.

If an inconsistency arises during a proof by contradiction, that proof succeeds. If it arises during a proof by cases, the current case is deemed impossible.