17.5. Debugging tip

When grind fails it prints the remaining subgoal followed by all equivalence classes. The two largest classes are shown as True propositions and False propositions, listing every literal currently known to be provable or refutable. Inspect these lists to spot missing facts or contradictory assumptions.