Prover9 “找到了一些，但不是全部，要求的证明”答案

【问题标题】：Prover9 "Some, but not all, of the requested proofs were found"Prover9 “找到了一些，但不是全部，要求的证明”
【发布时间】：2019-06-27 13:27:05
【问题描述】：

我正在通过 Prover9/Mace4 运行一些格子证明。 Prover9 的说法是Exit: Time limit. 加上标题中的信息。

我将时间限制从 60 秒增加到 120 秒。相同的消息（两次）。奇怪的是：

我为那条消息找到了一些 GHits，但它们似乎都是中文的（？）

我给出的公理可能是（相互）递归的——我试图引入一个函数和一个指定的“吸收元素”[**]；解决问题需要无限统一。 Prover9 会这样做吗？

我很高兴在此消息中添加公理和目标。（我使用非标准方式来定义会面和加入。）但首先，我应该通过什么健全性检查？

[**] 吸收元素既不是格子顶部也不是格子底部；更像格子左角。（元素将是格子底部，以防格子退化为两个元素。）该函数是与顶部/底部“成直角”的部分排序。我期望的格子既不是互补的也不是分配的（同样，除非是 2 个元素）。

【问题讨论】：

Prover9 用反证法证明，所以$F 表示发现了矛盾，从而证明存在证明。你能准确地发布你给 Prover9 的内容，包括目标和假设吗？
查看我发布的答案，感谢@Doug 并为误报道歉。我认为这与具体的假设/目标无关。
顺便说一句，有使用 Prover9 的理由吗？自从 Bill McCune 于 2009 年去世后，它就不再被进一步开发。例如E Prover 和Vampire。
有理由不使用Prover9吗？它有效（出于我的目的）。逻辑是永恒的。为什么我想要“进一步发展”的东西？
反对使用 EProver 或 Vampire 的原因：查看他们的下载页面；不适用于 Windows；事实上，他们似乎并没有意识到 Windows 是一个平台。我不想在 UNIX 环境中编译软件。我想运行证明。当他们准备好黄金时段时，我会再看一遍。

【解决方案1】：

经过多次尝试，我重现了这一点，但只是通过设置一些我确信我不会触及的奇怪选项。（我通常更改的唯一选项是Time limit，而我经常更改Reset to defaults，所以这会掩盖任何证据。）

这是我对发生的事情的猜测。

but not all 是怎么回事？

[注意**] 我从来没有打算设定多个目标；但是当我使用公理进行黑客攻击/实验时，我将所有目标保留在Goals: 框中，以便我可以轻松地切换取消/评论。我想我在取消注释另一个时没有注释掉一个。

如手册中所述，通常的行为是 Prover9 在它证明的第一个目标上报告成功；不会继续其他目标。如果有多个可证明的目标，它似乎会选择最简单/最快的（？），而不考虑文件中的位置。

但是有了max_proofs set to more than default 1，Prover9 会继续尝试。（还有一个 auto_denials 标志与它有关，我不明白。）

我不知道我是如何设置max_proofs 的——当我最终找到Options/Limits 子屏幕时，我没有认出它。很奇怪。

【讨论】：