17.1. Error Messages🔗

When grind fails, it prints the remaining subgoal followed by all the information returned by its subsystems—the contents of the “shared whiteboard.” In particular, it presents equivalence classes of terms that it has determined to be equal. 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.