16.1. 错误信息🔗

当 grind 失败时，它会打印剩余的子目标，然后打印其子系统返回的所有信息 - “共享白板”的内容。 特别是，它提供了已确定为相等的术语的等价类。 最大的两个类显示为 True propositions 和 False propositions，列出了当前已知的可证明或可反驳的每个文字。 检查这些列表以发现缺失的事实或矛盾的假设。