Local ATP Benchmark

Mix.install([
  {:atp_benchmark_runner, path: "item_14_ATP_Benchmark_Runner/atp_benchmark_runner", force: true}
])

1. Configure paths from .env

env_file = Path.expand("../.env", __DIR__)

# Load .env values into the OS environment (Config.get() and hpc_connect pick them up).
env_map = AtpBenchmarkRunner.load_env!(env_file)

IO.puts("Configured paths:")
IO.puts("  TPTP_ROOT:      #{AtpBenchmarkRunner.tptp_dir()}")
IO.puts("  Store dir:      #{AtpBenchmarkRunner.store_dir()}")
IO.puts("  SMT temp dir:   #{AtpBenchmarkRunner.Config.smt_tmp_dir()}")
IO.puts("  THF temp dir:   #{AtpBenchmarkRunner.Config.thf_tmp_dir()}")
IO.puts("  .env file:      #{env_file}")

This notebook is the local counterpart to benchmark_hpc.livemd. It runs the same prover images (via Docker instead of Apptainer) and applies the same input preparation as on the cluster:

• :cvc5 — problems are converted to SMT-LIB (TPTPToSMT) before cvc5 sees them (cvc5 has no TPTP input dialect); its bare sat/unsat/unknown answer is mapped to an SZS status.
• :lash — FOF/CNF/TFF problems are converted to THF (TPTP.ToTHF) because lash is a THF-$o-only prover.
• All other provers read the TPTP file directly.

No HPC session, SLURM, or execution plans are needed here — everything runs on this machine, sequentially.

2. Detect available execution methods

AtpBenchmarkRunner.LocalRunner.print_image_status_summary()

Available provers:

• :tableaux — uses the local escript (always available after mix escript.build in item #12)
• :eprover, :vampire, :cvc5, :zipperposition, :leo3, :leo2, :lash — run via Docker images built from their Containerfiles

Native binaries of the reference provers are not distributed for Windows. The Docker images are built from the same sources as the HPC Apptainer .defs, so results are directly comparable with the cluster.

3. Build / pull Docker images for all provers

This builds images for all registered provers from their Containerfiles (Docker) or apptainer.defs (Apptainer). The first build downloads dependencies and may take a few minutes; subsequent runs are instant. force: true rebuilds everything. Returns {:ok, name} / {:error, name, reason} per prover.

# Build (or pull) local images for all registered provers in one call.
# backend: :auto (default) | :docker | :apptainer   ·   force: true rebuilds all.
results = AtpBenchmarkRunner.build_local_images!(:all, backend: :docker)

4. Download problems

Single problems are downloaded from the TPTP distribution into TPTP_ROOT (C:\tmp\tptp from .env). download_tptp_problems!/2 returns the resolved Problem structs plus any download warnings.

selected_problems = [
  "ALG001+0.p",
  "GRP001-0.p",
  "GRP002+0.p",
  "GRP003+0.p",
  "GRP004+0.p",
  "GRP720+1.p",
  "GRP752-1.p",
  "LAT001+0.p",
  "PUZ001+0.p",
  "REL001+0.p",
  "SET001^0.p",
  "SMT001+0.p",
  "SYN000+0.p",
  "THF001+0.p"
]

{downloaded, download_warnings} =
  AtpBenchmarkRunner.download_tptp_problems!(selected_problems, force: false)

IO.puts("Downloaded #{length(downloaded)} problem(s):")
Enum.each(downloaded, fn problem ->
  IO.puts("  ✅ #{problem.name}  status=#{problem.expected_status}  rating=#{problem.rating}")
  IO.puts("     -> #{problem.path}")
end)

if download_warnings == [] do
  IO.puts("No warnings.")
else
  IO.puts("Warnings (#{length(download_warnings)}):")
  Enum.each(download_warnings, fn w ->
    IO.puts("  ⚠️  #{w.name}: #{inspect(w.reason)}")
  end)
end

Tip: download_tptp_problems!/2 is the "single problem download" entry point. Pass any TPTP problem name (e.g. "GRP001-0.p"); problems already present under TPTP_ROOT are reused (set force: true to re-download).

5. Select provers and problems

All eight provers, including our own :tableaux solver. Problems are selected by name — they resolve from TPTP_ROOT, the bundled examples, or a livebook cache automatically.

selected_provers = [
  :tableaux,
  :eprover,
  :vampire,
  :cvc5,
  :zipperposition,
  :leo3,
  :leo2,
  :lash
]

problems =
  AtpBenchmarkRunner.select_problems(
    names: selected_problems,
    limit: 10
  )

IO.puts("Provers (#{length(selected_provers)}): #{inspect(selected_provers)}")
IO.puts("")
IO.inspect(Enum.map(problems, &%{name: &1.name, path: &1.path}), label: "Problems")

6. Run the local benchmark

Each prover runs against each problem sequentially, exactly like the single-node sequential HPC mode. auto_ensure_images: true builds any missing Docker image on demand, and the same SMT/THF input preparation as on HPC is applied per prover.

IO.puts("Starting local benchmark...")
IO.puts("  Provers: #{inspect(selected_provers)}")
IO.puts("  Problems: #{length(problems)}")
IO.puts("")

{t_ms, results} =
  :timer.tc(fn ->
    AtpBenchmarkRunner.local_benchmark(selected_provers, problems,
      timeout_seconds: 30,
      auto_ensure_images: true,
      include_raw_output: true
    )
  end)

elapsed_s = t_ms / 1_000_000
IO.puts("Benchmark completed in #{Float.round(elapsed_s, 2)}s")
IO.puts("Total results: #{length(results)}")

7. Results table

# Guard: fall back to an empty list if this cell is evaluated before section 6.
results = binding()[:results] || []

AtpBenchmarkRunner.results_table(results)

8. Aggregated report

report = AtpBenchmarkRunner.report(results)

IO.puts("Run ID: #{report.run_id}")
IO.puts("Generated: #{report.generated_at}")
IO.puts("")
AtpBenchmarkRunner.print_report_markdown(report)

Per-prover breakdown

IO.puts("| Prover | Total | Solved | Failed | Solve Rate |")
IO.puts("|--------|------:|-------:|-------:|-----------:|")

Enum.each(report.by_prover, fn p ->
  IO.puts("| #{p.prover} | #{p.total} | #{p.solved} | #{p.failed} | #{Float.round(p.solve_rate * 100, 1)}% |")
end)

Per-problem comparison

AtpBenchmarkRunner.print_per_problem(report)

Full explained results

IO.puts("Full explained results with proofs:\n")
AtpBenchmarkRunner.print_explain_full(results)

Filtered results by prover

target_prover = :vampire

AtpBenchmarkRunner.print_verbose_report(results, prover: target_prover, solved_only: true)

View a specific proof

target_prover = :vampire
target_problem = "GRP001-0"

AtpBenchmarkRunner.show_proof(results, target_prover, target_problem)

Raw prover debug output

AtpBenchmarkRunner.print_raw_output(results, :vampire, "GRP001-0")

Interesting findings

interesting = report.interesting

IO.puts("### Easy problems our prover failed (rating <= 0.3)")
if interesting.easy_failed_by_ours == [] do
  IO.puts("  (none) 🎉")
else
  Enum.each(interesting.easy_failed_by_ours, &IO.puts("  - #{&1}"))
end

IO.puts("")
IO.puts("### Hard problems our prover solved (rating >= 0.7)")
if interesting.hard_solved_by_ours == [] do
  IO.puts("  (none)")
else
  Enum.each(interesting.hard_solved_by_ours, &IO.puts("  - #{&1}"))
end

IO.puts("")
IO.puts("### Solved only by our prover")
if interesting.only_ours == [] do
  IO.puts("  (none)")
else
  Enum.each(interesting.only_ours, &IO.puts("  - #{&1}"))
end

IO.puts("")
IO.puts("### Solved only by reference provers")
if interesting.only_others == [] do
  IO.puts("  (none)")
else
  Enum.each(interesting.only_others, &IO.puts("  - #{&1}"))
end

9. Visualizations

Mermaid-based visual companions to explain/1 / explain_full/1. Each cell returns a Kino.Mermaid diagram (or a fenced markdown block outside Livebook). If the real run has not produced results yet — or the kernel was restarted — the cells fall back to synthetic sample results so you can see the look of every diagram without needing the Docker images.

Synthetic sample results (fallback when section 6 has not run)

defmodule VisualizeSample do
  def results do
    refutation = """
    % SZS output start CNFRefutation
    fof(unit_not_a, axiom, ~(a), file('GRP001-0.p', unit_not_a)).
    fof(unit_a, axiom, a, file('GRP001-0.p', unit_a)).
    fof(c_0_2, plain, ~a, inference(fof_simplification,[status(thm)],[unit_not_a])).
    cnf(c_0_4, plain, (~a), inference(split_conjunct,[status(thm)],[c_0_2])).
    cnf(c_0_5, plain, (a), inference(split_conjunct,[status(thm)],[unit_a])).
    cnf(c_0_6, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_4, c_0_5])]), ['proof']).
    % SZS output end CNFRefutation
    """

    [
      AtpBenchmarkRunner.Result.new(
        problem_id: "GRP001-0",
        prover: :eprover,
        szs_status: "Theorem",
        wall_time_ms: 812,
        memory_kb: 12_345,
        raw_output: refutation
      ),
      AtpBenchmarkRunner.Result.new(
        problem_id: "GRP002+0",
        prover: :eprover,
        szs_status: "GaveUp",
        wall_time_ms: 30_000,
        memory_kb: 8_100
      ),
      AtpBenchmarkRunner.Result.new(
        problem_id: "GRP001-0",
        prover: :vampire,
        szs_status: "Theorem",
        wall_time_ms: 402,
        memory_kb: 9_900
      ),
      AtpBenchmarkRunner.Result.new(
        problem_id: "SMT001+0",
        prover: :cvc5,
        szs_status: "Satisfiable",
        wall_time_ms: 604,
        memory_kb: 4_200
      )
    ]
  end
end

9a. Single result — AtpBenchmarkRunner.visualize(result)

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

target =
  Enum.find(results, fn r ->
    r.prover == :eprover and AtpBenchmarkRunner.Result.solved?(r)
  end)

if target, do: AtpBenchmarkRunner.visualize(target), else: "No solved eprover result found."

9b. Proof dependency graph — AtpBenchmarkRunner.visualize_proof(result)

For provers that emit machine-readable TPTP clause refutations (E, Vampire) this renders the proof as a dependency DAG. Other provers fall back to a pipeline diagram.

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

target =
  Enum.find(results, fn r ->
    match?({:ok, _}, AtpBenchmarkRunner.Visualize.Proof.parse(r))
  end)

if target, do: AtpBenchmarkRunner.visualize_proof(target), else: "No parseable proof found."

9c. Run summary — status pie + wall-time chart

AtpBenchmarkRunner.visualize(results) is the one-call shortcut for Visualize.status_pie/2 + Visualize.timeline/2; it pushes both diagrams as Livebook outputs.

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

case AtpBenchmarkRunner.visualize(results) do
  :ok -> :ok
  markdowns -> Enum.each(markdowns, &IO.puts/1)
end

9d. Report scoreboard — AtpBenchmarkRunner.visualize(report)

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

report = AtpBenchmarkRunner.report(results)
AtpBenchmarkRunner.visualize(report)

9e. Raw Mermaid source (copy into a markdown cell)

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

target =
  Enum.find(results, fn r ->
    match?({:ok, _}, AtpBenchmarkRunner.Visualize.Proof.parse(r))
  end)

if target do
  IO.puts(AtpBenchmarkRunner.Visualize.markdown(AtpBenchmarkRunner.Visualize.proof(target)))
else
  IO.puts("No parseable proof — nothing to show.")
end

10. Persist results to local store

run = AtpBenchmarkRunner.new_run(
  title: "Local smoke test",
  problems: problems,
  provers: selected_provers,
  walltime: "00:30:00",
  problem_timeout_seconds: 30
)

paths = AtpBenchmarkRunner.persist_run!(run, results, report)
IO.puts("Run saved: #{paths.run_path}")
IO.puts("Results saved: #{paths.results_path}")
IO.puts("Report saved: #{paths.report_path}")

Runs are persisted to the store directory from .env (ATP_BENCHMARK_RUNNER_STORE_DIR, e.g. C:\tmp\atp_benchmark_runner_store).

11. Compare with a previous run (longitudinal diff)

prev_results_path = nil

if prev_results_path && File.exists?(prev_results_path) do
  prev_results = AtpBenchmarkRunner.Store.load_results!(prev_results_path)
  diff = AtpBenchmarkRunner.compare_runs(prev_results, results)
  AtpBenchmarkRunner.print_diff(diff)
else
  IO.puts("No previous results to compare against. Set `prev_results_path` to enable.")
end

12. Inspect raw output (optional)

target_index = 0

if results != [] do
  r = Enum.at(results, target_index)

  if r && r.raw_output do
    IO.puts("Raw output for #{r.problem_id} / #{r.prover}:")
    IO.puts("")
    IO.puts(r.raw_output)
  else
    IO.puts("No raw output stored (rerun with include_raw_output: true)")
  end
else
  IO.puts("No results available.")
end