16.1. 错误消息🔗

grind 失败时，会先打印剩余子目标，再打印其各子系统返回的全部信息，也就是“共享白板”上的内容。 具体而言，它会展示由已判定相等的项构成的等价类。 最大的两个类显示为 True propositions 和 False propositions，分别列出当前已知可证明或可证伪的每个文字。 检查这些列表，可以找出缺失的事实或相互矛盾的假设。