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.
• Wall-clock bounded. Parsing and proving each run in a throwaway process the runner kills when its budget expires, so no single problem can stall a sweep. A killed phase is still recorded as a CSV row (parse_timeout / hard_timeout), so the data set stays complete.
• 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 SPC header).

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

• result — thm | csa | unk | timeout | parse_timeout | hard_timeout | parser_error | prover_error | no_conjecture. timeout is the prover reporting its own budget exhausted; hard_timeout is the runner killing a prover that overran it anyway; parse_timeout is the parser killed before the prover ever started.

• 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 SPC 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).
• log_level (default :none) — level applied to the prover's Logger for the duration of the run. The runner's own progress and result lines go straight to standard output and are unaffected. Raising it costs search time as well as screen space: Logger skips argument evaluation for suppressed calls, and several hot sites build their message eagerly.
• parse_timeout (default 60_000 ms) — wall-clock budget for parsing one problem. A handful of TPTP problems pull in enough includes to keep the parser busy for many minutes; those are killed at the budget and recorded as parse_timeout.
• prove_grace (default 10_000 ms) — slack added to params.timeout to obtain the wall-clock budget for the proof attempt. The prover's own timeout is cooperative (workers have to come back around to notice it); this is the hard backstop, recorded as hard_timeout.

Parse cache

The parser never sees %Parameters{}, so a problem that times out or fails to parse under one configuration does the same under all of them. The first configuration to hit one appends the outcome to <output_dir>/parse_cache; later configurations replay it from there instead of paying the parse again — which is the difference between one 60-second stall and one per configuration. Successful parses are not cached: the parsed problem is what the prover needs. Delete the file to force a re-attempt (e.g. after a parser fix).

Progress output

One line per problem on standard output, prefixed with the local wall-clock time and carrying an ETA extrapolated from the problems completed so far in this invocation:

[07-28 14:03:22] [baseline] 142/5138 2.8% | SYO/SYO001^1.p → thm 152ms correct=yes | elapsed 00:04:11 eta 02:27:03