Runs the prover across the TPTP TH0/TH1 problem library and records one CSV row per problem. Designed for long unattended benchmark sweeps on a laptop:

• Parameterised. Accepts a ShotTx.Data.Parameters struct so an ablation sweep can invoke the same runner once per configuration.
• Resumable. Each call reads the destination CSV and skips any (run_label, problem) row that is already recorded. Interrupting the runner (Ctrl-C, kill, laptop lid) and re-invoking with the same arguments picks up where it left off; at worst the in-flight problem is re-run.
• Pausable. Between problems, the runner checks for a STOP sentinel file in the output directory and exits cleanly if it exists. Delete the file to resume.
• SZS-scored. The TPTP problem header (% Status : ...) is parsed from each file so the CSV records whether the prover's answer matched the expected TPTP status.
• Snapshotted. A <label>.meta sidecar file is written on the first run of each config, capturing the start timestamp, git rev-parse HEAD, and the full %Parameters{} value. On resume, if the current call's parameters disagree with the recorded ones, the runner logs a warning and continues — so a mid-sweep code change never silently mixes configurations into one CSV without a trail.

CSV columns

run_label, problem, language, expected_szs, result, correct, time_ms,
steps, worker_yields, rules_total, active_branches_max,
branches_closed, branches_saturated, csp_calls, csp_succeeded, details

• run_label — the label of the parameter configuration.
• problem — path relative to TPTP/Problems, e.g. SYO/SYO001^1.p.

• language — TH0 | TH1 | unknown (from the file Syntax header).

• expected_szs — TPTP-declared status: Theorem, CounterSatisfiable, Unknown, Open, … (or unknown if the header is missing).

• result — thm | csa | unk | timeout | parser_error | prover_error | unexpected | no_conjecture.

• correct — yes | no | n/a. Only decidable when both the expected status is one of Theorem / CounterSatisfiable and the prover terminated with a definite answer.

• time_ms — wall-clock milliseconds for parse + prove.
• steps, worker_yields — proof-search counters (see ShotTx.Prover.Stats).
• rules_total — total rule firings across all workers.
• active_branches_max — peak open-branch count.
• branches_closed, branches_saturated — branches closed locally vs. saturated (SAT witnesses).
• csp_calls, csp_succeeded — CSP solver calls and successes.
• details — free-form detail string, commas/semicolons replaced with spaces for CSV safety. Empty for cases that produced no stats (parser_error, no_conjecture, catastrophic prover_error).

Options

• label (default "default") — configuration label written into every row. Also determines the CSV filename (<output_dir>/<label>.csv).
• output_dir (default "bench_results") — directory that holds all CSV files and the STOP sentinel for this run. Persist a stable name across resumes.
• language (default :both) — :th0, :th1, or :both. Filters problems by the Syntax header line.
• problem_limit (default nil) — max number of problems to process in this invocation (after already-completed rows are skipped). Handy for smoke tests.
• problem_filter (default nil) — a function (relative_path -> boolean).