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.