Chapter 8: Evaluation

Mix.install([
  {:kino, "~> 0.19.0"},
  {:kino_vega_lite, "~> 0.1.13"}
])

Overview

The architecture of Chapter 6 and the rules of Chapters 3 to 5 were each introduced with an argument for why they belong in the prover. This chapter measures what each of them contributes, by switching one off at a time against a fixed baseline and running the whole TPTP higher-order corpus at a uniform budget, and then characterises the prover's coverage on a smaller structured set against five reference systems. Nothing measured here was tuned: every configuration is the default of Chapter 6 with one value changed, each ran once, and no portfolio or per-problem strategy selection took place, so the counts rank the components against one another and are a lower bound on what the calculus reaches.

Three results carry the chapter. The contradiction agent $\mathcal{CA}$ accounts for roughly half of all refutations, since disabling it costs $364$ of $682$ and nothing else in the matrix is within a factor of four of that. Iterative deepening, demodulation, atom decomposition, finite $o$-quantification and the initial $\gamma$-limit each contribute measurably, and eager definition unfolding improves on the default by $48$ problems, while primitive substitution, the suggestion agent $\mathcal{SA}$, instance-based $\gamma$-expansion, the primitive substitution batch size and the size of the worker pool all lie inside the run-to-run band of about ten problems established in § Baseline. The pool is the answer to the question Chapter 1 left open: eight workers perform about three times the inference of one within the same budget and solve two problems fewer, because the additional inference widens the frontier of open branches without raising the rate at which global closure is attempted, and global closure is what produces the refutations.

Every figure here is scored on refutations. Countermodel answers are reported separately and are not counted as solves, for the reason given in § Method and Scoring: the prover infers the countermodel verdict from a syntactic test and never checks it, so a CounterSatisfiable answer is not attested whether or not it agrees with the TPTP status.

Method and Scoring

The corpus is every TH0 and TH1 problem of the TPTP library [Sut17], $5109$ problems in the version used here. Sixteen configurations were run over the full corpus: the baseline, one configuration per component switched off relative to it, and two numeric sweeps at three values each. Each configuration ran once, and each problem received a uniform budget of timeout ($2000$ ms), so a difference in solved count between two rows is attributable to the component under ablation rather than to differing time. The derived tables this chapter reads are in files/; the $81,744$ per-problem records they summarise are held in the implementation repository.

The sweep ran on commit 2a05f05 between 2026-08-15 and 2026-08-16, on an AMD Ryzen 7 4700U with $15$ GiB of memory under Arch Linux, where worker_pool_size (:auto) resolves to eight. The follow-up probe of § Closure Search under the Two Pool Sizes ran on an AMD Ryzen 7 3700X in a container under a Linux subsystem on Windows 11 (Ubuntu), where the runtime reports sixteen online schedulers. The two pool sizes are therefore eight against one in the matrix and sixteen against one in the probe, which bears on any comparison of the two inference ratios.

An answer counts as a solve when it agrees with the SZS status [Sut08] declared in the problem file, and three conventions narrow that. Refutations only: the countermodel verdict is decided by a pairwise syntactic test over a saturated branch and is never checked, so a countermodel agreeing with the TPTP status rests on the same unvalidated predicate as one contradicting it. Countermodels are therefore reported as a separate column and excluded from the solved counts, and restricting to refutations leaves the ordering of the sixteen configurations unchanged.

Agreement with the problem file: three problems whose header carries no usable status were answered by the prover and are not counted. Scoring is also narrower than the SZS ontology, since only Theorem and CounterSatisfiable are scored and every other status is recorded as undecidable; re-scoring the sweep under the full ontology produced no further disagreements.

defmodule Ch8.Data do
  @moduledoc """
  Loader for the derived tables in `files/`. Each file is a comma-separated
  table with a header row and no quoted fields; numeric cells are cast so the
  tables can be sorted and charted without further conversion.
  """

  @dir Path.join(__DIR__, "files")

  def load(name) do
    [header | rows] =
      @dir
      |> Path.join(name)
      |> File.read!()
      |> String.split("\n", trim: true)
      |> Enum.map(&(&1 |> String.trim() |> String.split(",")))

    keys = Enum.map(header, &String.to_atom/1)

    Enum.map(rows, fn cells ->
      keys
      |> Enum.zip(cells)
      |> Map.new(fn {key, value} -> {key, cast(value)} end)
    end)
  end

  defp cast(value) do
    with :error <- parse_integer(value), :error <- parse_float(value) do
      value
    end
  end

  defp parse_integer(value) do
    case Integer.parse(value) do
      {number, ""} -> number
      _other -> :error
    end
  end

  defp parse_float(value) do
    case Float.parse(value) do
      {number, ""} -> number
      _other -> :error
    end
  end
end

summary = Ch8.Data.load("ablation_summary.csv")
Kino.nothing()

Baseline

The baseline is the default %ShotTx.Data.Parameters{} of Chapter 6 with timeout set to $2000$ ms: both peer agents present in their default state, every calculus rule enabled, iterative deepening on, and worker_pool_size (:auto). One departure from the defaults bounds what the chapter can claim: model_agent_backend (:none) in every one of the sixteen configurations, so $\mathcal{MA}$ ran as an idle process throughout and its contribution is not measured here.

Ch8.Data.load("baseline_outcomes.csv")
|> Enum.map(fn row ->
  %{
    "Outcome" => row.outcome,
    "Problems" => row.count,
    "Share (%)" => row.share_pct
  }
end)
|> Kino.DataTable.new(name: "Baseline outcomes over 5109 problems")

[%{"Outcome" => "timeout", "Problems" => 3423, "Share (%)" => 67.0}, %{"Outcome" => "thm", "Problems" => 685, "Share (%)" => 13.4}, %{"Outcome" => "parse_timeout", "Problems" => 628, "Share (%)" => 12.3}, %{"Outcome" => "parser_error", "Problems" => 221, "Share (%)" => 4.3}, %{"Outcome" => "no_conjecture", "Problems" => 77, "Share (%)" => 1.5}, %{"Outcome" => "csa", "Problems" => 62, "Share (%)" => 1.2}, %{"Outcome" => "unk", "Problems" => 8, "Share (%)" => 0.2}, %{"Outcome" => "prover_error", "Problems" => 5, "Share (%)" => 0.1}]

parse_timeout and parser_error are properties of ShotDs.Tptp rather than of the prover: the parser never sees %Parameters{}, so a problem it cannot read is unreadable under every configuration. no_conjecture marks problems that are not attemptable as posed.

Removing the $628$ parse timeouts, the $221$ parse failures and the $77$ problems without a conjecture leaves $4183$ genuine attempts, of which the baseline solved $747$ (thm & csa). One problem in six never reached the prover, so the corpus-level rate is bounded by the parser rather than by the calculus, and repairing the parser is the largest single coverage gain available.

The distribution of solve times over the baseline's refutations is flat well before the budget expires. What the prover solves, it solves quickly, and the problems it does not solve are not close to being solved, which is also why the ablation deltas are stable against the choice of $2000$ ms. A few solves lie past the budget, which is the cooperative timeout of § Threats to Validity.

The three sections that follow read against one table of deltas from this baseline.

summary
|> Enum.map(fn row ->
  %{
    "Configuration" => row.configuration,
    "Parameter" => row.parameter,
    "Refutations" => row.theorems,
    "Delta" => row.delta_theorems,
    "Gained" => row.gained,
    "Lost" => row.lost,
    "Only solver" => row.uniquely_solved,
    "Countermodels" => row.countermodels_agreeing,
    "Contradicting" => row.countermodels_contradicting
  }
end)
|> Kino.DataTable.new(name: "Sixteen configurations, refutations and deltas against the baseline")

[%{"Configuration" => "eager_unfold_defs", "Contradicting" => 2, "Countermodels" => 61, "Delta" => 48, "Gained" => 72, "Lost" => 24, "Only solver" => 44, "Parameter" => "unfold_defs: :eager", "Refutations" => 730}, %{"Configuration" => "no_beta_variant", "Contradicting" => 1, "Countermodels" => 62, "Delta" => 21, "Gained" => 41, "Lost" => 20, "Only solver" => 16, "Parameter" => "beta_variant: false", "Refutations" => 703}, %{"Configuration" => "prim_batch_16", "Contradicting" => 1, "Countermodels" => 61, "Delta" => 3, "Gained" => 21, "Lost" => 18, "Only solver" => 2, "Parameter" => "prim_subst_batch_size: 16", "Refutations" => 685}, %{"Configuration" => "prim_batch_4", "Contradicting" => 2, "Countermodels" => 61, "Delta" => 1, "Gained" => 24, "Lost" => 23, "Only solver" => 0, "Parameter" => "prim_subst_batch_size: 4", "Refutations" => 683}, %{"Configuration" => "baseline", "Contradicting" => 1, "Countermodels" => 61, "Delta" => 0, "Gained" => 0, "Lost" => 0, "Only solver" => 3, "Parameter" => "(none)", "Refutations" => 682}, %{"Configuration" => "no_prim_subst", "Contradicting" => 1, "Countermodels" => 61, "Delta" => -1, "Gained" => 23, "Lost" => 24, "Only solver" => 2, "Parameter" => "primitive_substitution: false", "Refutations" => 681}, %{"Configuration" => "no_suggestions", "Contradicting" => 2, "Countermodels" => 61, "Delta" => -1, "Gained" => 34, "Lost" => 35, "Only solver" => 11, "Parameter" => "suggestions_enabled: false", "Refutations" => 681}, %{"Configuration" => "serial", "Contradicting" => 2, "Countermodels" => 61, "Delta" => -2, "Gained" => 36, "Lost" => 38, "Only solver" => 10, "Parameter" => "worker_pool_size: 1", "Refutations" => 680}, %{"Configuration" => "no_instance_based_gamma", "Contradicting" => 2, "Countermodels" => 61, "Delta" => -3, "Gained" => 16, "Lost" => 19, "Only solver" => 1, "Parameter" => "instance_based_gamma: false", "Refutations" => 679}, %{"Configuration" => "no_atom_decomposition", "Contradicting" => 3, "Countermodels" => 61, "Delta" => -12, "Gained" => 26, "Lost" => 38, "Only solver" => 3, "Parameter" => "atom_decomposition: false", "Refutations" => 670}, ...]

alias VegaLite, as: Vl

deltas =
  summary
  |> Enum.reject(&(&1.configuration == "no_contradiction_agent"))
  |> Enum.map(fn row ->
    sign =
      cond do
        row.delta_theorems > 0 -> "more"
        row.delta_theorems < 0 -> "fewer"
        true -> "baseline"
      end

    %{"configuration" => row.configuration, "delta" => row.delta_theorems, "sign" => sign}
  end)

order = deltas |> Enum.sort_by(& &1["delta"], :desc) |> Enum.map(& &1["configuration"])

shared_axes = fn spec ->
  spec
  |> Vl.encode_field(:y, "configuration",
    type: :nominal,
    sort: order,
    title: nil,
    axis: [label_font_size: 11, domain: false, ticks: false]
  )
  |> Vl.encode_field(:x, "delta",
    type: :quantitative,
    scale: [domain: [-100, 60], nice: false],
    axis: [grid: true, grid_color: "#e5e7eb", title: "refutations gained or lost"]
  )
end

Vl.new(
  width: 460,
  height: 360,
  title: [
    text: "Refutations gained and lost against the baseline",
    subtitle: "no_contradiction_agent is off this scale at -364",
    anchor: :start,
    font_size: 13,
    subtitle_font_size: 11,
    subtitle_color: "#6b7280"
  ]
)
|> Vl.data_from_values(deltas)
|> Vl.layers([
  Vl.new()
  |> Vl.mark(:bar, corner_radius_end: 2, height: [band: 0.65])
  |> shared_axes.()
  |> Vl.encode_field(:color, "sign",
    type: :nominal,
    scale: [domain: ["more", "baseline", "fewer"], range: ["#2c5fa8", "#8a939c", "#b02418"]],
    legend: nil
  ),
  Vl.new()
  |> Vl.mark(:text,
    font_size: 10,
    color: "#4b5563",
    align: [expr: "datum.delta >= 0 ? 'left' : 'right'"],
    dx: [expr: "datum.delta >= 0 ? 4 : -4"]
  )
  |> shared_axes.()
  |> Vl.encode_field(:text, "delta", type: :quantitative)
])
|> Vl.config(view: [stroke: nil])

{"$schema":"https://vega.github.io/schema/vega-lite/v5.json","config":{"view":{"stroke":null}},"data":{"values":[{"configuration":"eager_unfold_defs","delta":48,"sign":"more"},{"configuration":"no_beta_variant","delta":21,"sign":"more"},{"configuration":"prim_batch_16","delta":3,"sign":"more"},{"configuration":"prim_batch_4","delta":1,"sign":"more"},{"configuration":"baseline","delta":0,"sign":"baseline"},{"configuration":"no_prim_subst","delta":-1,"sign":"fewer"},{"configuration":"no_suggestions","delta":-1,"sign":"fewer"},{"configuration":"serial","delta":-2,"sign":"fewer"},{"configuration":"no_instance_based_gamma","delta":-3,"sign":"fewer"},{"configuration":"no_atom_decomposition","delta":-12,"sign":"fewer"},{"configuration":"no_finite_o_quantification","delta":-20,"sign":"fewer"},{"configuration":"gamma_limit_3","delta":-21,"sign":"fewer"},{"configuration":"gamma_limit_5","delta":-25,"sign":"fewer"},{"configuration":"no_demodulation","delta":-41,"sign":"fewer"},{"configuration":"no_iterative_deepening","delta":-87,"sign":"fewer"}]},"height":360,"layer":[{"encoding":{"color":{"field":"sign","legend":null,"scale":{"domain":["more","baseline","fewer"],"range":["#2c5fa8","#8a939c","#b02418"]},"type":"nominal"},"x":{"axis":{"grid":true,"gridColor":"#e5e7eb","title":"refutations gained or lost"},"field":"delta","scale":{"domain":[-100,60],"nice":false},"type":"quantitative"},"y":{"axis":{"domain":false,"labelFontSize":11,"ticks":false},"field":"configuration","sort":["eager_unfold_defs","no_beta_variant","prim_batch_16","prim_batch_4","baseline","no_prim_subst","no_suggestions","serial","no_instance_based_gamma","no_atom_decomposition","no_finite_o_quantification","gamma_limit_3","gamma_limit_5","no_demodulation","no_iterative_deepening"],"title":null,"type":"nominal"}},"mark":{"cornerRadiusEnd":2,"height":{"band":0.65},"type":"bar"}},{"encoding":{"text":{"field":"delta","type":"quantitative"},"x":{"axis":{"grid":true,"gridColor":"#e5e7eb","title":"refutations gained or lost"},"field":"delta","scale":{"domain":[-100,60],"nice":false},"type":"quantitative"},"y":{"axis":{"domain":false,"labelFontSize":11,"ticks":false},"field":"configuration","sort":["eager_unfold_defs","no_beta_variant","prim_batch_16","prim_batch_4","baseline","no_prim_subst","no_suggestions","serial","no_instance_based_gamma","no_atom_decomposition","no_finite_o_quantification","gamma_limit_3","gamma_limit_5","no_demodulation","no_iterative_deepening"],"title":null,"type":"nominal"}},"mark":{"align":{"expr":"datum.delta >= 0 ? 'left' : 'right'"},"color":"#4b5563","dx":{"expr":"datum.delta >= 0 ? 4 : -4"},"fontSize":10,"type":"text"}}],"title":{"anchor":"start","fontSize":13,"subtitle":"no_contradiction_agent is off this scale at -364","subtitleColor":"#6b7280","subtitleFontSize":11,"text":"Refutations gained and lost against the baseline"},"width":460}

Bars to the right of zero are configurations that solve more than the baseline. Sign is carried by the direction of the bar as well as by the colour, so the figure needs no legend. Gained and Lost in the table are set differences rather than a decomposition of the delta: a configuration can be flat overall while exchanging tens of problems in both directions, which several of them do.

The size of that exchange was measured rather than inferred. The two worker-pool configurations were run three times each over the $1677$ problems on which the agent dispatches at least one closure search, at the same budget. Of the $3354$ pairs of a configuration and a problem, $84$ answered differently across three identical repeats, which is $2.5,%$. Estimating each problem's per-run solve probability from its three draws puts the standard deviation of one configuration's solved count at $4.0$ problems under the pool and $3.4$ serial, and the standard deviation of the difference between two independent single runs at $5.3$. A net delta inside roughly ten problems is therefore not evidence of a contribution, and the sections below support an ordering into tiers rather than a point estimate of any single delta. The exchanged problems are also not hard ones traded against easy ones: of the $38$ problems the baseline solves and the serial configuration does not, the median takes $84$ ms and none takes longer than $1497$ ms, so the exchange reflects the order in which the search reaches branches rather than the time available to it.

Ablating the Agents, the Calculus and the Search Control

Two of the three layers of Chapter 7 were switched here. Disabling contradiction_agent costs $364$ of $682$ refutations, and local ground closure alone, which is what remains when $\mathcal{CA}$ never dispatches a global search, solves $318$ problems. The result is the chapter's largest and the one the architecture predicts, since rigidity makes closure a global constraint and a prover deciding closure only locally answers a weaker question. It also fixes the reading of the other rows, because a configuration solving $318$ problems is not far enough into any search to be informative about the rules.

Disabling suggestions_enabled costs one problem, which is inside the floor. $\mathcal{SA}$ is a heuristic over a complete calculus, so this is a statement about the value of the hints rather than about the verdicts: the configuration exchanges $34$ problems against $35$ and is the third largest source of uniquely solved problems in the matrix, at $11$. The hints change which proofs are found without changing how many. Where they go is not in the data, since TptpRunner records steps and rules_total and not the per-rule breakdown that would separate a hint shortening a proof from one displacing a rule making progress.

$\mathcal{MA}$ was not ablated. model_agent_backend (:none) held in all sixteen configurations, so the layer was inert throughout and this chapter reports nothing about it.

The rules of Chapter 3 divide into three groups by contribution. Two are substantial: removing demodulation costs $41$ refutations, the largest calculus effect in the matrix, losing $61$ problems while gaining $20$, and removing atom_decomposition costs $12$, losing $38$ against $26$ gained. The second is also the configuration with the most countermodel answers contradicting TPTP, at three, which fits the mechanism: without decomposition a branch reaches saturation earlier and the unchecked countermodel test is consulted sooner. Two more concern $o$-typed subterms: removing finite_o_quantification costs $20$, and removing instance_based_gamma costs three, which is inside the floor.

One change improves on the default. Setting unfold_defs to :eager gains $48$ refutations, gaining $72$ and losing $24$, and supplies $44$ uniquely solved problems, by a wide margin the largest such count in the matrix. Ten of the $72$ gains were reported past the $2000$ ms budget, some as late as $6$ s, because the prover's timeout is cooperative, so the gain is real and smaller than $48$; and an eager unfolding enlarges the formulae a branch carries, so the improvement is specific to a corpus in which definitions are shallow. That a single non-default value outweighs every component's contribution is the clearest indication that the baseline is untuned.

One rule is a net cost at this budget. Switching off beta_variant gains $21$ refutations while losing $20$ and gaining $41$, so the rule contributes $20$ refutations and displaces $41$.

Two numeric parameters were swept rather than switched, and both say the default is the value to keep. The initial $\gamma$-limit was run at $1$, $3$ and $5$: the default of $1$ is best by a wide margin, since $3$ costs $21$ refutations and $5$ costs $25$, and a higher initial limit fills the first deepening round with instantiations that do not contribute to a closure. The primitive substitution batch size was run at $4$, $8$ and $16$, and the three values span three problems in total, which is inside the floor. Neither parameter is worth exposing as a tuning surface, and neither was tuned here.

The search control was ablated at one switch. Removing iterative_deepening costs $87$ refutations and loses $102$ problems against $15$ gained, which is the second largest effect in the matrix and the largest that is not an agent. The deepening schedule of Chapter 3 is doing what it was introduced to do: the alternative, a single search at the full bound, exhausts the budget in a region of the space that contains no closure. It is also the one configuration in which the countermodel column moves, from $61$ agreeing answers to $54$, since a branch that saturates at a lower bound never reaches the state that would have closed it.

The remaining search control parameter is the size of the worker pool, which the next section treats on its own.

Scaling with the Worker Pool

The pool is compared at worker_pool_size (:auto), which resolves to one worker per online scheduler and so to eight on the machine the matrix ran on, against worker_pool_size: 1. The two configurations differ in that parameter alone. To keep the comparison free of the parse cache and of the difference in total sweep time, the counters below are restricted to the $3383$ problems on which both configurations exhausted the budget, so the wall clock available to each is equal by construction.

Ch8.Data.load("worker_pool.csv")
|> Enum.map(fn row ->
  [
    "Quantity": row.quantity,
    "Statistic": row.statistic,
    "Pool": row.pool_auto,
    "Serial": row.pool_serial,
    "Ratio": row.ratio
  ]
end)
|> Kino.DataTable.new(name: "worker_pool_size :auto against 1")

[[Quantity: "problems compared (budget exhausted under both)", Statistic: "count", Pool: 3383, Serial: 3383, Ratio: ""], [Quantity: "steps", Statistic: "total", Pool: 5414451, Serial: 1654858, Ratio: 3.27], [Quantity: "branches closed locally", Statistic: "total", Pool: 121798, Serial: 38853, Ratio: 3.13], [Quantity: "peak open branches", Statistic: "median", Pool: 66, Serial: 21, Ratio: 3.14], [Quantity: "global closure searches", Statistic: "total", Pool: 2469, Serial: 2115, Ratio: 1.17], [Quantity: "global closure searches per 1000 steps", Statistic: "rate", Pool: 0.46, Serial: 1.28, Ratio: 0.36], [Quantity: "problems solved by both", Statistic: "count", Pool: 705, Serial: 705, Ratio: ""], [Quantity: "wall clock on those (ms)", Statistic: "total", Pool: 61003, Serial: 77785, Ratio: 1.28]]

steps and branches closed locally are worker-side counters; global closure searches is the number of times $\mathcal{CA}$ dispatched a search through find_global_closure/3. The last row is over the $705$ problems both configurations solved, where the ratio is a latency ratio rather than a throughput one.

The pool multiplies inference by $3.27$ and local branch closure by $3.13$ within the same wall clock, and increases the number of global closure searches by $1.17$, which as a rate is $0.46$ global closures per thousand steps against the serial configuration's $1.28$. On the problems both configurations solve the pool is faster by a factor of $1.28$ in aggregate, and it solves two problems fewer. The parallel speedup therefore lands on branch expansion, and the component producing roughly half of all refutations does not receive it. Three properties of $\mathcal{CA}$ account for that, each visible in the agent rather than inferred from the numbers.

At most one global closure search runs at a time: check_global_closure/1 returns immediately when pending_search holds a task, so a clash or split arriving during a search increments evidence_version and is otherwise discarded. A search is dispatched only when insufficient_options?/1 is false, which requires every open branch to carry at least one clash candidate, so a single branch without one suppresses the check for all of them. Once dispatched, find_global_closure/3 enumerates the cartesian product of the per-branch option lists, so a dispatched search costs exponentially more as the frontier widens, and abandons at the proof deadline.

The frontier connects those properties to the measurement: additional workers raise the rate at which branch evidence arrives and hold three times as many branches open, and both make a dispatch less likely and a dispatched search more expensive. The taxonomy of [Bon00] classifies the outcome as a parallel search that is not a faster version of the sequential one, and it is the cost of the partition Chapter 6 made between local expansion and one serialised global decision. What the sweep does not settle is whether the agent is saturated by the cost of each search or starved of opportunities to begin one.

Closure Search under the Two Pool Sizes

The sweep cannot separate the two accounts of that, because TptpRunner exports neither the time spent inside a search nor the number of checks suppressed, although Stats records both. A follow-up run recorded them. The two worker-pool configurations were run three times each over the $1677$ problems on which either dispatched at least one search during the sweep, at the same $2000$ ms budget, with one counter added to the clause of check_global_closure/1 that returns when a search is already in flight, since that path previously recorded nothing. This run is on the second machine of § Method and Scoring, where the pool is sixteen workers rather than eight, so its ratios are read against a wider pool than the matrix's.

Ch8.Data.load("ca_probe_summary.csv")
|> Enum.map(fn row ->
  [
    "Measure": row.measure,
    "Statistic": row.statistic,
    "Pool": row.pool_auto,
    "Serial": row.pool_serial,
    "Ratio": row.ratio
  ]
end)
|> Kino.DataTable.new(name: "ContradictionAgent counters, 5031 runs per configuration")

[[Measure: "tableau steps", Statistic: "total", Pool: 14353411, Serial: 2460501, Ratio: 5.83], [Measure: "peak open branches", Statistic: "median run", Pool: 196, Serial: 30, Ratio: 6.53], [Measure: "runs dispatching at least one search", Statistic: "count", Pool: 4826, Serial: 4442, Ratio: 1.09], [Measure: "searches dispatched", Statistic: "total", Pool: 9347, Serial: 8317, Ratio: 1.12], [Measure: "searches per 1000 steps", Statistic: "rate", Pool: 0.65, Serial: 3.38, Ratio: 0.19], [Measure: "checks skipped (no clash options)", Statistic: "total", Pool: 208292, Serial: 175057, Ratio: 1.19], [Measure: "checks suppressed (search in flight)", Statistic: "total", Pool: 5559732, Serial: 677507, Ratio: 8.21], [Measure: "suppressed per search dispatched", Statistic: "rate", Pool: 595, Serial: 81, Ratio: 7.3], [Measure: "recorded time inside search (ms)", Statistic: "total", Pool: 3997654, Serial: 4113722, Ratio: 0.97], [Measure: "share of wall clock in search (%)", Statistic: "rate", Pool: 46.5, Serial: 51.6, Ratio: 0.9], [Measure: "longest single search (ms)", Statistic: "max", Pool: 1982, Serial: 1977, Ratio: 1.0], [Measure: "branches per search", Statistic: "mean", Pool: 21.41, Serial: 10.37, Ratio: 2.06], [Measure: "candidates per search", Statistic: "mean", Pool: 996.84, Serial: 161.05, Ratio: 6.19], [Measure: "searches finding a closure (%)", Statistic: "rate", Pool: 12.4, Serial: 13.6, Ratio: 0.91], [Measure: "searches killed unfinished (%)", Statistic: "rate", Pool: 17.8, Serial: 10.8, Ratio: 1.65], [Measure: "problems solved (majority of 3 repeats)", Statistic: "count", Pool: 389, Serial: 381, Ratio: 1.02]]

The pool leaves the three quantities that determine the verdict close to unchanged: the number of searches, the time spent searching, and the number of problems closed. The quantities it does multiply describe the space each individual search has to cover.

The two accounts describe the same mechanism. A closure search occupies the only slot for a large part of the budget, $46.5,%$ of wall clock under the pool and $51.6,%$ serial, and every check arriving while it runs is discarded, so searches are at once expensive and infrequent and additional workers cannot make them more frequent. Under the pool $595$ checks are discarded for every search that runs, against $81$ serial, which at $8.21$ is the quantity the pool moves furthest. Saturation is therefore present with a single worker and is not produced by the wider frontier. What the pool changes is what a search has to cover, $6.19$ times as many candidates over $2.06$ times as many open branches, and $17.8,%$ of its dispatches are killed by the deadline before finishing against $10.8,%$ serial.

The $46.5,%$ understates the cost, since csp_duration_us is recorded on the completion path of the search task, so a search killed at the deadline contributes nothing and killing is more common under the pool. The share is the fraction of the proof during which a closure search was running rather than the fraction of the proof's effort diverted into one, because the search runs in its own supervised task.

Three changes to $\mathcal{CA}$ follow from these counters, and Chapter 9 takes them up as future work. A per-search deadline set as a fraction of the remaining budget, rather than the session deadline currently passed as deadline_us, would replace one search that cannot finish with several that can, since only $12.4,%$ of dispatches find a closure. Retaining the most recent suppressed trigger and running it when the slot frees would recover one of the several hundred opportunities now discarded per search. Allowing a small number of searches in flight over disjoint subsets of the open branches would put the pool's remaining schedulers on the step that decides the verdict. On this evidence the wider pool is not otherwise worth its inference.

The Structured Problem Set

The matrix measures the prover's components against one another. It says nothing about how the prover stands against systems built on other substrates, and it does not characterise the problem classes the search decides, since the TPTP corpus is too heterogeneous for either question and $67,%$ of it reaches only a timeout. A second and smaller study addresses both. ShotTx.Benchmark.HolSuite normalises the structured higher-order problems of Appendix A into $130$ self-contained THF problems, run at the prover's defaults with timeout ($5000$ ms), three times over the whole set, each problem in a fresh runtime since state carried between proof sessions would otherwise make a verdict depend on what ran before it. Reference verdicts for the same problem text came from Vampire 5.0.1, E 3.5.1, Zipperposition 2.1 [BBT+21], Leo-III 1.8.0 [SB21] and Satallax 3.5 [Bro12] through a public submission service at a $10$ s limit on that service's hardware.

alias VegaLite, as: Vl

coverage = Ch8.Data.load("structured_coverage.csv")

coverage_order =
  coverage |> Enum.sort_by(& &1.definite, :desc) |> Enum.map(& &1.prover)

coverage_axes = fn spec ->
  spec
  |> Vl.encode_field(:y, "prover",
    type: :nominal,
    sort: coverage_order,
    title: nil,
    axis: [label_font_size: 11, domain: false, ticks: false]
  )
  |> Vl.encode_field(:x, "definite",
    type: :quantitative,
    scale: [domain: [0, 130], nice: false],
    axis: [
      grid: true,
      grid_color: "#e5e7eb",
      title: "problems given a definite answer, of 130"
    ]
  )
end

coverage_values =
  Enum.map(coverage, fn row ->
    %{
      "prover" => row.prover,
      "definite" => row.definite,
      "emphasis" => if(row.prover == "Shot", do: "Shot", else: "reference")
    }
  end)

Vl.new(
  width: 440,
  height: 200,
  title: [
    text: "Coverage on the structured problem set",
    subtitle: "reference provers at a 10 s limit; Shot at 5 s",
    anchor: :start,
    font_size: 13,
    subtitle_font_size: 11,
    subtitle_color: "#6b7280"
  ]
)
|> Vl.data_from_values(coverage_values)
|> Vl.layers([
  Vl.new()
  |> Vl.mark(:bar, corner_radius_end: 2, height: [band: 0.62])
  |> coverage_axes.()
  |> Vl.encode_field(:color, "emphasis",
    type: :nominal,
    scale: [domain: ["Shot", "reference"], range: ["#2c5fa8", "#a9b2bb"]],
    legend: nil
  ),
  Vl.new()
  |> Vl.mark(:text, font_size: 10, color: "#4b5563", align: :left, dx: 4)
  |> coverage_axes.()
  |> Vl.encode_field(:text, "definite", type: :quantitative)
])
|> Vl.config(view: [stroke: nil])

{"$schema":"https://vega.github.io/schema/vega-lite/v5.json","config":{"view":{"stroke":null}},"data":{"values":[{"definite":121,"emphasis":"reference","prover":"Vampire"},{"definite":120,"emphasis":"reference","prover":"Leo-III"},{"definite":118,"emphasis":"reference","prover":"Satallax"},{"definite":116,"emphasis":"reference","prover":"E"},{"definite":112,"emphasis":"reference","prover":"Zipperposition"},{"definite":79,"emphasis":"Shot","prover":"Shot"}]},"height":200,"layer":[{"encoding":{"color":{"field":"emphasis","legend":null,"scale":{"domain":["Shot","reference"],"range":["#2c5fa8","#a9b2bb"]},"type":"nominal"},"x":{"axis":{"grid":true,"gridColor":"#e5e7eb","title":"problems given a definite answer, of 130"},"field":"definite","scale":{"domain":[0,130],"nice":false},"type":"quantitative"},"y":{"axis":{"domain":false,"labelFontSize":11,"ticks":false},"field":"prover","sort":["Vampire","Leo-III","Satallax","E","Zipperposition","Shot"],"title":null,"type":"nominal"}},"mark":{"cornerRadiusEnd":2,"height":{"band":0.62},"type":"bar"}},{"encoding":{"text":{"field":"definite","type":"quantitative"},"x":{"axis":{"grid":true,"gridColor":"#e5e7eb","title":"problems given a definite answer, of 130"},"field":"definite","scale":{"domain":[0,130],"nice":false},"type":"quantitative"},"y":{"axis":{"domain":false,"labelFontSize":11,"ticks":false},"field":"prover","sort":["Vampire","Leo-III","Satallax","E","Zipperposition","Shot"],"title":null,"type":"nominal"}},"mark":{"align":"left","color":"#4b5563","dx":4,"fontSize":10,"type":"text"}}],"title":{"anchor":"start","fontSize":13,"subtitle":"reference provers at a 10 s limit; Shot at 5 s","subtitleColor":"#6b7280","subtitleFontSize":11,"text":"Coverage on the structured problem set"},"width":440}

The prover proved $76$ of the $130$ on all three runs and $79$ on the best of them, returned three unknown answers, produced no countermodel, and produced no answer contradicting the reference panel. Of the $130$, $122$ carry a Theorem consensus across the five reference systems, so the prover decides roughly two thirds of what the panel decides; the remaining eight are the designated non-theorems, which no reference system refutes either.

Over the $79$ problems it proves, its median self-reported solve time is $0.035$ s, against $0.012$ s for E, $0.013$ s for Zipperposition, $0.024$ s for Vampire and $1.374$ s for Leo-III. Compared with the best reference time on each problem it is $2.7$ times slower at the median, $43$ times at the ninth decile and $388$ times at worst, and faster on $14$ of the $79$, which share a shape: small propositional or reflexivity-style goals that close in a handful of rule applications, where the tableau reaches a contradiction directly and a saturation-based system pays for a clausification it does not need. This is the measurement Chapter 1 conceded would be needed, taken on an untuned prototype, and read together with § Scaling with the Worker Pool the parallelism does not compensate for the constant factor, since the pool multiplies inference rather than closure.

The comparison is loose in two ways that bound how it should be read. The systems ran on different hardware, and the prover's figure excludes runtime startup while the service's wall clock includes process launch. Differences below roughly a factor of two carry no signal; what the numbers support is an order of magnitude and the question of which problems each side decides at all.

Six problems were proved on some runs and not others, and the distribution is bimodal rather than borderline: one closes in $33$ ms on two runs and exhausts $5000$ ms on the third. The shared queue imposes no preference over which open branch a free worker takes, so which worker reaches the productive primitive substitution instance decides the verdict, which is the instability quantified at $2.5,%$ in § Baseline.

Coverage by Model Class

Every example in the set carries the largest model class in which it is valid, over the semantics of [BBK04], and validity in a larger class implies validity in every smaller one. Appendix A sets out the two dimensions and works the examples individually. Grouping the three runs by that annotation separates the prover's coverage along one line.

Ch8.Data.load("structured_classes.csv")
|> Enum.map(fn row ->
  %{
    "Model class" => row.class,
    "Problems" => row.problems,
    "Proved on all runs" => row.stable,
    "Proved on some" => row.flip,
    "Never proved" => row.never
  }
end)
|> Kino.DataTable.new(name: "The 130 problems by the class in which they are valid")

[%{"Model class" => "M_beta", "Never proved" => 9, "Problems" => 47, "Proved on all runs" => 37, "Proved on some" => 1}, %{"Model class" => "M_beta-eta", "Never proved" => 0, "Problems" => 1, "Proved on all runs" => 1, "Proved on some" => 0}, %{"Model class" => "M_beta-b", "Never proved" => 1, "Problems" => 21, "Proved on all runs" => 19, "Proved on some" => 1}, %{"Model class" => "M_beta-eta-b", "Never proved" => 1, "Problems" => 1, "Proved on all runs" => 0, "Proved on some" => 0}, %{"Model class" => "M_beta-xi", "Never proved" => 6, "Problems" => 6, "Proved on all runs" => 0, "Proved on some" => 0}, %{"Model class" => "M_beta-xi-b", "Never proved" => 11, "Problems" => 14, "Proved on all runs" => 2, "Proved on some" => 1}, %{"Model class" => "M_beta-f", "Never proved" => 6, "Problems" => 6, "Proved on all runs" => 0, "Proved on some" => 0}, %{"Model class" => "M_beta-f-b", "Never proved" => 3, "Problems" => 9, "Proved on all runs" => 3, "Proved on some" => 3}, %{"Model class" => "property q", "Never proved" => 2, "Problems" => 3, "Proved on all runs" => 1, "Proved on some" => 0}, %{"Model class" => "signature", "Never proved" => 1, "Problems" => 13, "Proved on all runs" => 12, "Proved on some" => 0}, %{"Model class" => "non-theorem", "Never proved" => 8, "Problems" => 8, "Proved on all runs" => 0, "Proved on some" => 0}, %{"Model class" => "warm-up", "Never proved" => 0, "Problems" => 1, "Proved on all runs" => 1, "Proved on some" => 0}]

The properties the prover decides are $\beta$- and $\eta$-conversion together with Boolean extensionality; the ones it does not are the two functional principles, the congruence rule for abstractions and full functional extensionality. Of the $70$ problems that are valid without either functional principle, $57$ are proved on all three runs. Of the $35$ that require one of them, five are. The class names in the table are those of Appendix A, which sets out the eight classes and the property each one adds.

The two pure cases are the sharpest. Example 13, extension with identity, requires the congruence rule for abstractions and nothing else; Example 14, extension of identity, requires full functional extensionality. Neither is proved in any of its six variants on any of the three runs. At the other end $\eta$ costs nothing, since terms are held in $\eta$-long $\beta$-normal form throughout, and Boolean extensionality costs little, with $19$ of the $21$ problems that need it proved.

The calculus accounts for the line, and Appendix A states the commitment the table measures: the renaming and instantiation rules give Boolean extensionality, the $\eta$-long $\beta$-normal representation of Chapter 2 gives $\eta$ without a rule firing, and the equality-expansion rules give the functional principles. That last commitment is the narrow one. An equality at a functional type expands into extensional equality, so both functional principles are available to a formula that already is an equality, and nothing in Chapter 3 turns a rigid-headed atom pair into a disequality goal, which is the rule identified as absent in § Soundness and Completeness. A branch needing one of them to separate two atoms saturates rather than closing, which is what the three unknown answers do, while the variants of the same theorems that state the equality in the conjecture are proved in under $60$ ms.

The exceptions locate the line rather than blurring it. Of the nine problems that need functional and Boolean extensionality together, the three proved include Example 21, which states that there are exactly four functions of type $o {\to} o$ and which finite_o_quantification (true) decides by finite expansion over a pure $o$-type without any extensionality rule firing. A rule covering one class of extensionality obligation decides the examples inside its scope and leaves the rest untouched, which is the shape a rule for the congruence principle would have to take. The individual problems are not worked here: Appendix A names each example, the class it belongs to and the commitment it tests, and runs it.

Threats to Validity

Nothing was tuned, and one run was taken per configuration. Each delta therefore carries the band of about ten problems established in § Baseline, and the matrix is a one-at-a-time ablation, so interactions between components are unmeasured. The union of solves across all sixteen configurations is $905$ problems against the baseline's $747$, which bounds what a portfolio over them could reach and indicates how far from tuned the baseline is. No figure here is this prover's ceiling.

The countermodel verdict is inferred, not checked. Branch.model_certain?/2 tests pairwise syntactic non-complementarity over a saturated branch, without enforcing congruence, using the two-element cardinality of $o$ or consulting the unifier. Across the whole sweep $22$ answers contradict the TPTP status, spanning five problems whose conjectures hold only because $o$ has exactly two elements, and every one is a countermodel claimed on a theorem; no refutation in $81,744$ rows contradicts the status. Countermodels are excluded from the scoring above for that reason, which also leaves the $61$ agreeing countermodel answers unattested. One of the two defects behind them has since been corrected; the general one remains, since the verdict is still a syntactic test rather than a satisfiability check.

The prover does not always answer identically on repeated runs. Workers race, evidence reaches the agent in a nondeterministic order, and the budget cuts wherever it falls. The instability also persists at worker_pool_size: 1, which is presumably because the total term order of § The Total Prover-Side Wrapper uses :erlang.phash2/1 on the nondeterministic Erlang references given as unique names to parameters.

The probe ran on a later tree and on other hardware. The counters of § Closure Search under the Two Pool Sizes and the estimate of run-to-run variation come from commit 4a9c4f3 with one instrumentation line added, while the matrix comes from 2a05f05. The two corrections that landed between them, to Branch.distinguishable?/2 and to Proof.interior_event/2, touch neither the calculus nor the agent's scheduling, so the mechanism described in that section is unaffected, but the two sets of absolute counters should not be combined, and the probe ran at sixteen schedulers against the matrix's eight.

The budget is cooperative, and one problem in six never reached the prover. A worker notices the deadline between steps, so a step entering a long pre-unification enumeration overruns it: forty-five solves across the sweep were recorded past $2000$ ms, as late as $6$ s, with eager_unfold_defs accounting for eleven. Those solves are counted here and would not be counted under a hard budget. The parse failures of § Baseline bound every corpus-level statement, since the solved counts are counts over what was attempted. Per-configuration wall clock is not comparable either, because the baseline ran first and populated the shared parse cache, so per-problem times are quoted and per-configuration totals are not. A further $57$ results, about four per configuration, were recorded as prover errors because ShotTx.Proof.interior_event/2 had no clause for {:instantiate, ...} trace entries, and are counted as unsolved.

The two studies were run under different conditions. The matrix ran at a $2000$ ms budget on the full corpus with one run per configuration; the structured set ran at $5000$ ms over three runs with a fresh runtime per problem. Solved counts from the two are not comparable, and the reference verdicts of § The Structured Problem Set were obtained on other hardware through a public service.

Chapter References

• [BBK04] Christoph Benzmüller, Chad E. Brown, and Michael Kohlhase. Higher-order semantics and extensionality. The Journal of Symbolic Logic, 69(4):1027–1088, 2004.
• [BBT+21] Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Superposition with lambdas. Journal of Automated Reasoning, 65(7):893–940, 2021.
• [Bon00] Maria Paola Bonacina. A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence, 29(1):223–257, 2000.
• [Bro12] Chad E. Brown. Satallax: An automatic higher-order prover. In Automated Reasoning (IJCAR 2012), LNCS 7364, pages 111–117. Springer, 2012.
• [SB21] Alexander Steen and Christoph Benzmüller. Extensional higher-order paramodulation in Leo-III. Journal of Automated Reasoning, 65(6):775–807, 2021.
• [Sut08] Geoff Sutcliffe. The SZS ontologies for automated reasoning software. In LPAR Workshops (KEAPPA/IWIL), CEUR Workshop Proceedings 418, pages 38–49, 2008.
• [Sut17] Geoff Sutcliffe. The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017.

Previous: Chapter 7: Peer Agents and Proof Reconstruction  $\cdot$  Contents  $\cdot$  Next: Chapter 9: Conclusion