Reproducibility: Mace4, Prover9 and Vampire input files?

Stream: Equational

[Louis Cabarion]

I'm trying to locate the Mace4, Prover9, and Vampire input files that produced useful results in the project.

I found the Mace4 file equational_theories/Generated/All4x4Tables/src/cancellative5x5.in in the repository, which seems to work as intended:

$ mace4 < ./equational_theories/Generated/All4x4Tables/src/cancellative5x5.in
…
Exiting with 10944 models.
…

However, I couldn’t find any Vampire files (*.p) or Prover9 files (*.p9) in the repository.

Were the useful Mace4 results obtained exclusively from cancellative5x5.in?

Are the Vampire and Prover9 input files that produced useful results available in the repository, or perhaps located elsewhere?

[Vlad Tsyrklevich]

The vampire files were not archived. The most interesting ones, the ones that were used to search for counterexamples using human assistance are probably in specific threads. Just to generate a .p files for a specific pair you can generate vampire files using scripts, see e.g. equational_theories/Generated/FiniteImplicationSearch/README.md though there are others in the repo as well, e.g. equational_theories/Generated/VampireProven/src

[Zoltan A. Kocsis (Z.A.K.)]

A few of us, including I, obtained counterexamples from Mace4 using long runs from both standard and manually tuned input files (some posts on how this was done are linked from the log). The Mace4 inputs were not retained in the repo: only the outputs (converted into the planner's format) were saved into the txt files in the data/ directory. Since the claims are checked independently by Lean, there was no reproducibility concern: as long as you know the multiplication tables, you can verify the claims .

You might find more information about how the specific structures were by following the commits and PRs involving the data directory. The PRs will sometimes have an explanation of how the tables were obtained, or links to surrounding discussions which might have the Mace4 inputs.

[Louis Cabarion]

@Vlad Tsyrklevich @Zoltan A. Kocsis (Z.A.K.) Thanks for the clarifications! Just to be clear, I wasn’t suggesting there are any reproducibility issues with the results themselves: those are formalized, so their correctness is fully trusted.

What I'm hoping to reproduce isn't the final result, but the process that led to it: specifically, how the tools like Mace4, Prover9, or Vampire were used along the way. I'm interested in retracing those steps more precisely to better understand the workflow and how the tools contributed to the development.

[Louis Cabarion]

More concretely, for pedagogical purposes, I’d like to collect one example for each of Mace4, Prover9, and Vampire that shows how the tool produced a result meaningful (and ideally significant/important) to the project, along with the specific input that led to it.

[Zoltan A. Kocsis (Z.A.K.)]

I'll see if I have anything retained from my Mace4 explorations of finite models, but probably not: the laptop I was using to work on the project last October has already been repurposed. I am tagging @Jose Brox as well, I suspect he'll have some interesting searches.

Also, Mace4 supplied one of the last pieces of the puzzle when we worked on the full spectrum problem: the Python script which generated the relevant parts of the Mace4 input was retained there, so we can reconstruct the input file used.