diff --git a/CLAUDE.md b/CLAUDE.md
index f98680e..74c5d7a 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -141,7 +141,7 @@ back to `sorryAx` — that produces a *successful build*.
 | `Testimony/Bib/` | `Core` types, `Attr` registry attribute, `Works` entries, `Render`, `Registry` guards |
 | `Testimony/Provenance.lean` | `Reference`, `Source`, `Tradition`, `Confidence` |
 | `Testimony/Intertext.lean` | Typed relations between passages |
-| `Testimony/Logic/` | `Basic` formula, `Notation` (`p`/`notP`), `Entail` + countermodels + `Independent`, `Package` arguments + manifests, `Line` lines of reason, `Tactic` (`establish`, Horn-only, and `establish_by_search`/`refute_with`/`satisfied_by`/`leaves_open`/`granted`), `ModelCheck` a reading written as a table, checked against every premise by the kernel, `Framework` Dung semantics (grounded, preferred), `Dispute` packages as its nodes, defeat derived from entailment and cited confidence, `Horn` the decision procedure that computes a dispute's defeat table, `Certificate` the search that finds what the kernel checks of it (`horn_certify`), `Solver` the verified solver that computes its verdicts, `Witness` the checked reasons they are stated with, `Verdict` a verdict and its witness as one declaration, rendered from the witness, `Support` one position lending another a premise, `Map` a dispute drawn with its defeats, supports and the attacks support implies, `Because` why one package stands against another, at a checked crux, `Burden` the minimal sets of readings an opponent must reject, complete, `Dilemma` every reading of a rival's ambiguous claim, each answered, `Aif` every dispute as an AIF graph, checked against AIF's Definition 1.1 |
+| `Testimony/Logic/` | `Basic` formula, `Notation` (`p`/`notP`), `Entail` + countermodels + `Independent`, `Package` arguments + manifests, `Line` lines of reason, `Tactic` (`establish`, Horn-only, and `establish_by_search`/`refute_with`/`satisfied_by`/`leaves_open`/`granted`), `ModelCheck` a reading written as a table, checked against every premise by the kernel, `Framework` Dung semantics (grounded, preferred), `Dispute` packages as its nodes, defeat derived from entailment and cited confidence, `Horn` the decision procedure that computes a dispute's defeat table, `Certificate` the search that finds what the kernel checks of it (`horn_certify`), and each party's position converted once per table (`prepare_clauses`), `Solver` the verified solver that computes its verdicts, `Witness` the checked reasons they are stated with, `Verdict` a verdict and its witness as one declaration, rendered from the witness, `Support` one position lending another a premise, `Map` a dispute drawn with its defeats, supports and the attacks support implies, `Because` why one package stands against another, at a checked crux, `Burden` the minimal sets of readings an opponent must reject, complete, `Dilemma` every reading of a rival's ambiguous claim, each answered, `Aif` every dispute as an AIF graph, checked against AIF's Definition 1.1 |
 | `Testimony/Argument.lean` | Criteria, definitions, `Satisfies`, `People` |
 | `Testimony/Semantics/` | `Upper` (DOLCE's categories, each with its BFO counterpart), `Vocabulary`, `Grammar` (a claim's meaning as a term, over concepts, words and particulars), `Ontology` (a meaning taken apart and read under definitions), `Meaning` (`HasMeanings`, `HasJoins`), `Discourse` |
 | `Testimony/Ontology/` | Articles that derive what the vocabulary's words mean — definitions with sources, each shown at work — naming no argument (`Relations`; `Time`, an occurrence lasts one length of time; `Kinds`, each concept's category, or why it has none); `Search`, the generic queries; `Shared`, the definitions every join is read under |
diff --git a/Testimony/Checks/Citations.lean b/Testimony/Checks/Citations.lean
index 195091b..70ef471 100644
--- a/Testimony/Checks/Citations.lean
+++ b/Testimony/Checks/Citations.lean
@@ -84,7 +84,7 @@ syntax (name := checkCitationsCmd) "#check_citations" " under " ident : command
 elab_rules : command
   | `(#check_citations under $root) => checkCitations [root.getId]
 
-/-- info: every entry is a tagged definition, and every key names one: 48 definitions, 15 entries -/
+/-- info: every entry is a tagged definition, and every key names one: 49 definitions, 15 entries -/
 #guard_msgs in
 #check_citations under Testimony.Checks.Fixture
 
diff --git a/Testimony/Checks/Fixture.lean b/Testimony/Checks/Fixture.lean
index 5e4057c..ecaf67e 100644
--- a/Testimony/Checks/Fixture.lean
+++ b/Testimony/Checks/Fixture.lean
@@ -216,10 +216,13 @@ theorem node_strength : ∀ i, (node i).strength = strength i
   | .minutes => by decide
   | .clock => by decide
 
+prepare_clauses disputeClauses for dispute
+
 /-- Who defeats whom, computed and checked by the kernel. -/
 theorem dispute_defeats : ∀ i j, dispute.defeats i j ↔ defeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (node_strength i) (node_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (node_strength i) (node_strength j)
+    (disputeClauses.spec i) (disputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute, in the form the solver and the AIF check read. -/
diff --git a/Testimony/Logic/Certificate.lean b/Testimony/Logic/Certificate.lean
index 1f699cf..43e992a 100644
--- a/Testimony/Logic/Certificate.lean
+++ b/Testimony/Logic/Certificate.lean
@@ -116,6 +116,23 @@ question `Horn.satisfiable_of_certified` asks. -/
 def hintsAppend (index : α → ℕ) (Γ Δ : List (Formula α)) : List Hint :=
   [hintOnAll index (base Γ) Δ]
 
+/-- The base of a list of clauses, already converted: what propagation settled
+from them, and the clauses that fired. -/
+def baseOfClauses (cs : List (Clause α)) : Base α :=
+  let (s, trace) := chainTrace cs (cs.length + 1) ⟨[], []⟩ []
+  ⟨cs, s, trace⟩
+
+/-- **The hints for a cell whose positions are given as clauses**
+(`Horn.defeatsWith?`), in the order `Horn.defeatChecks` asks its questions, as
+`hintsFor` finds them from the packages. -/
+@[nospecialize]
+def hintsWith (index : α → ℕ) (ca cb : Option (List (Clause α))) (b : ArgumentPackage α) :
+    List Hint :=
+  let ba := ca.map baseOfClauses
+  let bb := cb.map baseOfClauses
+  (hintOn index ba b.conclusion :: b.premises.map (hintOn index ba)) ++
+    (stepsOf b.premises).flatMap fun q => [hintOn index bb (∼q.2), hintOn index ba q.2]
+
 /-- **The hints for a support cell**, in the order `supportsBy?` asks its
 questions: for each claim among `b`'s premises, whether `a`'s conclusion can
 hold with its negation. -/
@@ -198,6 +215,8 @@ def searchFor (index lhs : Expr) : MetaM Expr := do
   let args := lhs.getAppArgs
   if lhs.isAppOfArity ``Horn.defeatsBy? 9 then
     mkAppOptM ``Horn.hintsFor #[args[0]!, args[1]!, args[2]!, index, args[5]!, args[6]!]
+  else if lhs.isAppOfArity ``Horn.defeatsWith? 9 then
+    mkAppOptM ``Horn.hintsWith #[args[0]!, args[1]!, index, args[4]!, args[5]!, args[6]!]
   else if lhs.isAppOfArity ``Dissent.findingsBy? 6 then
     mkAppOptM ``Horn.findingsHints #[args[0]!, args[1]!, args[2]!, index, args[5]!]
   else if lhs.isAppOfArity ``supportsBy? 6 then
@@ -210,8 +229,9 @@ def searchFor (index lhs : Expr) : MetaM Expr := do
       throwError "horn_certify: expected the clauses of a list, got{indentExpr base}"
     mkAppOptM ``Horn.hintsAppend #[args[0]!, args[1]!, index, base.appArg!, args[5]!]
   else
-    throwError "horn_certify: expected `Horn.defeatsBy? …`, `Dissent.findingsBy? …`, \
-      `supportsBy? …`, `partOfBy? …` or `Horn.satisfiableAppend? …`, got{indentExpr lhs}"
+    throwError "horn_certify: expected `Horn.defeatsBy? …`, `Horn.defeatsWith? …`, \
+      `Dissent.findingsBy? …`, `supportsBy? …`, `partOfBy? …` or \
+      `Horn.satisfiableAppend? …`, got{indentExpr lhs}"
 
 /-- Prove `∃ index, Function.Injective index ∧ ∃ hints, decision index hints … = v`,
 for a defeat, support or part-of cell or a dissent's findings, or `∃ index hints, … = v` for a
@@ -248,4 +268,95 @@ elab (name := hornCertify) "horn_certify" : tactic => do
   goal.assign <| mkApp4 (.const ``Exists.intro us) indexTy p index body
   replaceMainGoal []
 
+/-! ### Each party's clauses, once
+
+A defeat table asks every cell about two parties' positions as clauses, and
+converting a position is most of what a cell costs the kernel. `prepare_clauses`
+converts each party's position once, at elaboration time, writes the result as a
+literal, and proves for each party that the literal is what the conversion
+gives: the kernel evaluates the conversion once per party, and every cell reads
+the literal. -/
+
+/-- A list of clauses as a term, each atom the constructor at its index. -/
+def clausesExpr (α : Expr) (ctors : Array Name) (cs : List (List ℕ × List ℕ)) :
+    MetaM Expr := do
+  let atom (k : ℕ) : MetaM Expr := do
+    let some c := ctors[k]? | throwError "prepare_clauses: no constructor {k}"
+    return mkConst c
+  let clauseTy := mkApp (mkConst ``Horn.Clause) α
+  let mut out : Array Expr := #[]
+  for (body, heads) in cs do
+    let b ← body.mapM atom
+    let h ← heads.mapM atom
+    out := out.push (mkApp3 (mkConst ``Horn.Clause.mk) α (← mkListLit α b) (← mkListLit α h))
+  mkListLit clauseTy out.toList
+
+/-- `prepare_clauses name for d`: define `name : ι → Option (List (Clause α))`,
+each party's position as clauses, written out, and prove `name_spec : ∀ i,
+clausesOf (d.node i).held = name i`, which the kernel checks once per party. -/
+elab "prepare_clauses " name:ident " for " d:term : command => Command.liftTermElabM do
+  let d ← Term.elabTerm d none
+  Term.synthesizeSyntheticMVarsNoPostponing
+  let d ← instantiateMVars d
+  let dTy ← whnfR (← inferType d)
+  let #[α, inst, ι] := dTy.getAppArgs | throwError "prepare_clauses: not a dispute"
+  let enumCtors (ty : Expr) : MetaM (Name × Array Name) := do
+    let .const n [] := ty | throwError "prepare_clauses: {ty} is not an enumeration"
+    let some (.inductInfo i) := (← getEnv).find? n | throwError "prepare_clauses: {n}?"
+    return (n, i.ctors.toArray)
+  let (ιName, parties) ← enumCtors ι
+  let (_, atoms) ← enumCtors α
+  let αName := α.constName!
+  let optTy := mkApp (mkConst ``Option [Level.zero]) (mkApp (mkConst ``List [Level.zero])
+    (mkApp (mkConst ``Horn.Clause) α))
+  let mut lits : Array Expr := #[]
+  for c in parties do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) (mkConst c))
+    let cl := mkApp2 (mkConst ``Horn.clausesOf) α held
+    -- Evaluated as constructor indices, a type the evaluator knows.
+    let idx := mkConst (αName ++ `ctorIdx)
+    let toIdx ← withLocalDeclD `c (mkApp (mkConst ``Horn.Clause) α) fun c => do
+      let body ← mkAppM ``List.map #[idx, ← mkAppM ``Horn.Clause.body #[c]]
+      let heads ← mkAppM ``List.map #[idx, ← mkAppM ``Horn.Clause.heads #[c]]
+      mkLambdaFVars #[c] (← mkAppM ``Prod.mk #[body, heads])
+    let mapClauses ← mkAppM ``List.map #[toIdx]
+    let asIdx ← mkAppM ``Option.map #[mapClauses, cl]
+    let v ← unsafe evalExpr (Option (List (List ℕ × List ℕ)))
+      (← inferType asIdx) asIdx
+    let lit ← match v with
+      | some cs => pure (mkApp2 (mkConst ``Option.some [Level.zero])
+          (mkApp (mkConst ``List [Level.zero]) (mkApp (mkConst ``Horn.Clause) α))
+          (← clausesExpr α atoms cs))
+      | none => pure (mkApp (mkConst ``Option.none [Level.zero])
+          (mkApp (mkConst ``List [Level.zero]) (mkApp (mkConst ``Horn.Clause) α)))
+    lits := lits.push lit
+  let defName := (← getCurrNamespace) ++ name.getId
+  let casesOn (motive : Expr) (minors : Array Expr) (i : Expr) (lvl : Level) : Expr :=
+    mkAppN (mkConst (ιName ++ `casesOn) [lvl]) (#[motive, i] ++ minors)
+  let body := Expr.lam `i ι (casesOn (.lam `_ ι optTy .default) lits (.bvar 0) Level.one) .default
+  addAndCompile <| .defnDecl {
+    name := defName, levelParams := [], type := .forallE `i ι optTy .default, value := body,
+    hints := .abbrev, safety := .safe }
+  addDocStringCore defName s!"Each party's position in `{d}`, as clauses, written out once \
+    so that every cell of its defeat table reads them rather than converting the position \
+    again. Generated by `prepare_clauses`; `{defName ++ `spec}` proves it."
+  -- For each party, the conversion reduces to its literal: `Eq.refl`, checked by the kernel.
+  let specTy ← withLocalDeclD `i ι fun i => do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) i)
+    mkForallFVars #[i] (← mkEq (mkApp2 (mkConst ``Horn.clausesOf) α held)
+      (mkApp (mkConst defName) i))
+  let motive ← withLocalDeclD `i ι fun i => do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) i)
+    mkLambdaFVars #[i] (← mkEq (mkApp2 (mkConst ``Horn.clausesOf) α held)
+      (mkApp (mkConst defName) i))
+  let proofs ← lits.mapM fun lit => mkEqRefl lit
+  let specVal := Expr.lam `i ι (casesOn motive proofs (.bvar 0) Level.zero) .default
+  addDecl <| .thmDecl {
+    name := defName ++ `spec, levelParams := [], type := specTy, value := specVal }
+  addDocStringCore (defName ++ `spec) s!"Each party's clauses in `{defName}` are what \
+    converting its position gives, checked by the kernel once for each party."
+
 end Testimony.Logic.Certificate
diff --git a/Testimony/Logic/Horn.lean b/Testimony/Logic/Horn.lean
index ade29c4..778e85e 100644
--- a/Testimony/Logic/Horn.lean
+++ b/Testimony/Logic/Horn.lean
@@ -887,11 +887,10 @@ def stepRebuts? (index : α → ℕ) (hb ha : Hint) (ca cb : Option (List (Claus
     else none
 
 /-- Every way `a` could defeat `b`: the rebuttal, each premise of `b`, and each
-claim `b`'s steps deliver, each with its hint. -/
-def defeatChecks (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
-    List (Option Bool) :=
-  let ca := clausesOf a.held
-  let cb := clausesOf b.held
+claim `b`'s steps deliver, each with its hint, given the clauses of what each
+holds, `ca` and `cb`. -/
+def defeatChecks (index : α → ℕ) (hints : List Hint) (ca cb : Option (List (Clause α)))
+    (b : ArgumentPackage α) (s t : ℕ) : List (Option Bool) :=
   let n := b.premises.length
   (rebuts? index (hintAt hints 0) b ca s t ::
     b.premises.zipIdx.map fun (φ, i) => undermines? index (hintAt hints (i + 1)) b ca s φ) ++
@@ -899,17 +898,25 @@ def defeatChecks (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage
       stepRebuts? index (hintAt hints (n + 1 + 2 * i)) (hintAt hints (n + 2 + 2 * i)) ca cb s t
         q.2
 
-/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints:
-`some true` if any way succeeds, `some false` if every way is shown to fail,
-`none` if some check was on a formula without clauses, or its hint did not
-check, and none succeeded. The checks are made once. -/
-def defeatsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
-    Option Bool :=
-  let checks := defeatChecks index hints a b s t
+/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints, given
+the clauses of what each holds: `some true` if any way succeeds, `some false` if
+every way is shown to fail, `none` if some check was on a formula without
+clauses, or its hint did not check, and none succeeded. The checks are made
+once. A table converts each party's position once, not once for every cell it
+appears in (`defeats_iff_of_prepared`). -/
+def defeatsWith? (index : α → ℕ) (hints : List Hint) (ca cb : Option (List (Clause α)))
+    (b : ArgumentPackage α) (s t : ℕ) : Option Bool :=
+  let checks := defeatChecks index hints ca cb b s t
   if checks.any (· == some true) then some true
   else if checks.all (· == some false) then some false
   else none
 
+/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints, each
+position converted to clauses here. -/
+def defeatsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
+    Option Bool :=
+  defeatsWith? index hints (clausesOf a.held) (clausesOf b.held) b s t
+
 /-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, every question
 searched: `defeatsBy?` with no hints. -/
 def defeats? (a b : ArgumentPackage α) (s t : ℕ) : Option Bool :=
@@ -1028,8 +1035,9 @@ theorem defeats_of_defeatsBy? {index : α → ℕ} {hints : List Hint} {a b : Ar
     {s t : ℕ} (hidx : Function.Injective index ∨ hints = []) (hs : a.strength = s)
     (ht : b.strength = t) (h : defeatsBy? index hints a b s t = some true) : Defeats a b := by
   subst hs ht
-  dsimp only [defeatsBy?] at h
-  generalize hc : defeatChecks index hints a b a.strength b.strength = checks at h
+  dsimp only [defeatsBy?, defeatsWith?] at h
+  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) b a.strength
+    b.strength = checks at h
   split at h
   · rename_i hany
     obtain ⟨x, hx, hxt⟩ := List.any_eq_true.mp hany
@@ -1055,8 +1063,9 @@ theorem not_defeats_of_defeatsBy? {index : α → ℕ} {hints : List Hint}
     {a b : ArgumentPackage α} {s t : ℕ} (hs : a.strength = s) (ht : b.strength = t)
     (h : defeatsBy? index hints a b s t = some false) : ¬ Defeats a b := by
   subst hs ht
-  dsimp only [defeatsBy?] at h
-  generalize hc : defeatChecks index hints a b a.strength b.strength = checks at h
+  dsimp only [defeatsBy?, defeatsWith?] at h
+  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) b a.strength
+    b.strength = checks at h
   split at h
   · simp at h
   · split at h
@@ -1138,6 +1147,19 @@ theorem defeats_iff_of_certified {a b : ArgumentPackage α} {s t : ℕ} {P : Pro
   · simp only [hP, decide_false] at h
     exact iff_of_false (not_defeats_of_defeatsBy? hs ht h) hP
 
+/-- **A cell of a defeat table, from hints the kernel checks and each position's
+clauses given.** The clauses are proved once for each party
+(`prepare_clauses`), so a table converts each position once rather than in every
+cell. -/
+theorem defeats_iff_of_prepared {a b : ArgumentPackage α} {s t : ℕ} {P : Prop} [Decidable P]
+    {ca cb : Option (List (Clause α))} (hs : a.strength = s) (ht : b.strength = t)
+    (hca : clausesOf a.held = ca) (hcb : clausesOf b.held = cb)
+    (h : ∃ (index : α → ℕ), Function.Injective index ∧
+      ∃ hints : List Hint, defeatsWith? index hints ca cb b s t = some (decide P)) :
+    Defeats a b ↔ P := by
+  subst hca hcb
+  exact defeats_iff_of_certified hs ht h
+
 end Attacks
 
 end Testimony.Logic.Horn
diff --git a/Testimony/Tools/Pages.lean b/Testimony/Tools/Pages.lean
index 2701950..1cffe61 100644
--- a/Testimony/Tools/Pages.lean
+++ b/Testimony/Tools/Pages.lean
@@ -253,7 +253,11 @@ def deriveArgumentBodies (tableName : Ident) (root : Name) : CommandElabM Unit :
       | _ =>
         let some modIdx := env.getModuleIdxFor? n | continue
         let some k := modOrder[env.header.moduleNames[modIdx.toNat]!]? | continue
-        let line := (← findDeclarationRanges? n).map (·.range.pos.line) |>.getD 0
+        -- A declaration with no place in the source was generated by a command
+        -- (`prepare_clauses`'s clauses), machinery for the kernel, not
+        -- something written for a reader.
+        let some ranges ← findDeclarationRanges? n | continue
+        let line := ranges.range.pos.line
         let dname := n.getString!
         let headOf (e : Expr) : Option Name :=
           match e.getAppFn with
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
index b740f02..748ae20 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
@@ -513,6 +513,8 @@ theorem partyNode_strength : ∀ i, (partyNode i).strength = partyStrength i
   | .motyer => motyerReply_strength
   | .micah => micahParity_strength
 
+prepare_clauses isaiahDisputeClauses for isaiahDispute
+
 /-- **Who defeats whom**, all thirty-six pairs: the critic and the scriptural
 reading defeat each other; each reply defeats the critic; the critic defeats
 Berry and Motyer back, but neither of Postell's counterexamples; nothing
@@ -523,7 +525,8 @@ checked by the kernel; the table is what the computation is checked
 against. -/
 theorem isaiahDispute_defeats : ∀ i j, isaiahDispute.defeats i j ↔ partyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (isaiahDisputeClauses.spec i) (isaiahDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
index 7aae5fa..5cb7c3e 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
@@ -212,14 +212,16 @@ theorem genesisPartyNode_strength : ∀ i, (genesisPartyNode i).strength = 0
   | .posterity => posterityCase_strength
   | .idiom => idiomCase_strength
 
+prepare_clauses genesisDisputeClauses for genesisDispute
+
 /-- **Who defeats whom**, all nine pairs: Luther and Leupold defeat each other,
 Luther and Lewis defeat each other, and nothing else. Every cell is computed
 from what the parties hold by `Horn.defeats?` and checked by the kernel. -/
 theorem genesisDispute_defeats :
     ∀ i j, genesisDispute.defeats i j ↔ genesisPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (genesisPartyNode_strength i)
-    (genesisPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (genesisPartyNode_strength i) (genesisPartyNode_strength j)
+    (genesisDisputeClauses.spec i) (genesisDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Matthew.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Matthew.lean
index b8d6828..a6ce54e 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Matthew.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Matthew.lean
@@ -159,14 +159,16 @@ theorem matthewPartyNode_strength : ∀ i, (matthewPartyNode i).strength = 0
   | .matthew => matthewCase_strength
   | .drift => driftObjection_strength
 
+prepare_clauses matthewDisputeClauses for matthewDispute
+
 /-- **Who defeats whom**, all four pairs: Matthew's reading and Wegner defeat
 each other, and nothing else. Every cell is computed from what the parties hold
 by `Horn.defeats?` and checked by the kernel. -/
 theorem matthewDispute_defeats :
     ∀ i j, matthewDispute.defeats i j ↔ matthewPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (matthewPartyNode_strength i)
-    (matthewPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (matthewPartyNode_strength i) (matthewPartyNode_strength j)
+    (matthewDisputeClauses.spec i) (matthewDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Protoevangelium.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Protoevangelium.lean
index c2c8227..55c451a 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Protoevangelium.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Protoevangelium.lean
@@ -371,14 +371,16 @@ theorem promisePartyNode_strength : ∀ i, (promisePartyNode i).strength = 0
   | .syntax => syntaxCase_strength
   | .scene => sceneCase_strength
 
+prepare_clauses promiseDisputeClauses for promiseDispute
+
 /-- **Who defeats whom**, all sixteen pairs: Westermann defeats the fulfilment,
 the syntax and the scene, and each defeats him back; and nothing else. Every cell is computed
 from what the parties hold by `Horn.defeats?` and checked by the kernel. -/
 theorem promiseDispute_defeats :
     ∀ i j, promiseDispute.defeats i j ↔ promisePartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (promisePartyNode_strength i)
-    (promisePartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (promisePartyNode_strength i) (promisePartyNode_strength j)
+    (promiseDisputeClauses.spec i) (promiseDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
index 7fb96f8..3bcf205 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
@@ -542,6 +542,8 @@ theorem septuagintPartyNode_strength :
   | .dinah => dinahCase_strength
   | .miller => millerCase_strength
 
+prepare_clauses septuagintDisputeClauses for septuagintDispute
+
 /-- **Who defeats whom**, all thirty-six pairs: Wegner defeats the witness,
 Rico and Gentry and the laws, and each defeats him back; so does Miller, and
 each defeats him back; the status reading defeats Wegner and Miller, and
@@ -550,8 +552,9 @@ parties hold by `Horn.defeats?` and checked by the kernel. -/
 theorem septuagintDispute_defeats :
     ∀ i j, septuagintDispute.defeats i j ↔ septuagintPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (septuagintPartyNode_strength i)
-    (septuagintPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (septuagintPartyNode_strength i)
+    (septuagintPartyNode_strength j)
+    (septuagintDisputeClauses.spec i) (septuagintDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
index 22bacc7..b08ef2e 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
@@ -198,6 +198,8 @@ theorem wegnerPartyNode_strength : ∀ i, (wegnerPartyNode i).strength = 0
   | .sign => signArgument_strength
   | .reply => ordinarySignReply_strength
 
+prepare_clauses wegnerDisputeClauses for wegnerDispute
+
 /-- **Who defeats whom**, all nine pairs: the fathers and Wegner defeat each
 other, the fathers and the reply defeat each other, and nothing else. Every
 cell is computed from the parties' premises by `Horn.defeats?` and checked by
@@ -205,8 +207,8 @@ the kernel. -/
 theorem wegnerDispute_defeats :
     ∀ i j, wegnerDispute.defeats i j ↔ wegnerPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (wegnerPartyNode_strength i)
-    (wegnerPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (wegnerPartyNode_strength i) (wegnerPartyNode_strength j)
+    (wegnerDisputeClauses.spec i) (wegnerDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean
index cff3c2c..f570cba 100644
--- a/arguments/TestimonyArguments/Checks.lean
+++ b/arguments/TestimonyArguments/Checks.lean
@@ -101,13 +101,13 @@ The canonical witness
 #check_refutations under TestimonyArguments using unfoldSets
 
 /--
-info: every entry is a tagged definition, and every key names one: 2332 definitions, 176 entries
+info: every entry is a tagged definition, and every key names one: 2338 definitions, 176 entries
 -/
 #guard_msgs in
 #check_citations under Testimony
 
 /--
-info: every entry is a tagged definition, and every key names one: 1622 definitions, 176 entries
+info: every entry is a tagged definition, and every key names one: 1633 definitions, 176 entries
 -/
 #guard_msgs in
 #check_citations under TestimonyArguments
diff --git a/arguments/TestimonyArguments/SolaFide/Dispute.lean b/arguments/TestimonyArguments/SolaFide/Dispute.lean
index d20d2f2..e821ef5 100644
--- a/arguments/TestimonyArguments/SolaFide/Dispute.lean
+++ b/arguments/TestimonyArguments/SolaFide/Dispute.lean
@@ -927,13 +927,16 @@ theorem partyNode_strength : ∀ i, (partyNode i).strength = partyStrength i
   | .trentOnPaulsWord => tridentineOnPaulsWord_strength
   | .romansOnTheWord => romansFourOnTheWord_strength
 
+prepare_clauses solaFideDisputeClauses for solaFideDispute
+
 /-- The first six rows of the table, computed from the parties' premises and
 checked by the kernel. The table is split in two only so that each declaration
 stays within the heartbeat budget. -/
 private theorem solaFideDispute_defeats_first (i : Party)
     (hi : i ∈ [.pauline, .dominical, .apostolic, .trent, .apocalyptic, .sanders])
     (j : Party) : solaFideDispute.defeats i j ↔ partyDefeats i j := by
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (solaFideDisputeClauses.spec i) (solaFideDisputeClauses.spec j) ?_
   simp only [List.mem_cons, List.not_mem_nil, or_false] at hi
   rcases hi with rfl | rfl | rfl | rfl | rfl | rfl <;> cases j <;> horn_certify
 
@@ -941,7 +944,8 @@ private theorem solaFideDispute_defeats_first (i : Party)
 private theorem solaFideDispute_defeats_second (i : Party)
     (hi : i ∈ [.critics, .jervell, .gospel, .lexical, .trentOnPaulsWord, .romansOnTheWord])
     (j : Party) : solaFideDispute.defeats i j ↔ partyDefeats i j := by
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (solaFideDisputeClauses.spec i) (solaFideDisputeClauses.spec j) ?_
   simp only [List.mem_cons, List.not_mem_nil, or_false] at hi
   rcases hi with rfl | rfl | rfl | rfl | rfl | rfl <;> cases j <;> horn_certify
 
diff --git a/arguments/TestimonyArguments/SolaFide/James.lean b/arguments/TestimonyArguments/SolaFide/James.lean
index 72ab1f4..0a67d60 100644
--- a/arguments/TestimonyArguments/SolaFide/James.lean
+++ b/arguments/TestimonyArguments/SolaFide/James.lean
@@ -799,6 +799,8 @@ theorem jamesPartyNode_strength : ∀ i, (jamesPartyNode i).strength = jamesPart
   | .renewalOnTheWord => renewalOnTheWord_strength
   | .westminsterOnReward => westminsterOnReward_strength
 
+prepare_clauses jamesDisputeClauses for jamesDispute
+
 /-- **Who defeats whom**, all 144 pairs. James's word defeats Trent's reading of
 it, and the reading's reply fails; it defeats the renewal reading too, whose
 reply fails for the same reason — it rests on Paul's word as renewal, rated
@@ -822,7 +824,8 @@ by the kernel. -/
 theorem jamesDispute_defeats :
     ∀ i j, jamesDispute.defeats i j ↔ jamesPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (jamesPartyNode_strength i) (jamesPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (jamesPartyNode_strength i) (jamesPartyNode_strength j)
+    (jamesDisputeClauses.spec i) (jamesDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/SolaFide/JesusWords.lean b/arguments/TestimonyArguments/SolaFide/JesusWords.lean
index 2e9d0e6..ddb83ae 100644
--- a/arguments/TestimonyArguments/SolaFide/JesusWords.lean
+++ b/arguments/TestimonyArguments/SolaFide/JesusWords.lean
@@ -550,6 +550,8 @@ theorem wordsPartyNode_strength : ∀ i, (wordsPartyNode i).strength = wordsPart
   | .matthew19Way => matthew19WayCase_strength
   | .matthew19Legal => matthew19LegalCase_strength
 
+prepare_clauses jesusWordsDisputeClauses for jesusWordsDispute
+
 /-- **Who defeats whom**, all 49 pairs: four standoffs, and nothing else. Luke
 7:50 and Trent defeat each other, and so do Luke 18 and Trent, over Trent's
 definition of justification; each Matthean reading defeats its rival, and is
@@ -558,7 +560,8 @@ defeated back. Every cell is computed from the parties' premises by
 theorem jesusWordsDispute_defeats :
     ∀ i j, jesusWordsDispute.defeats i j ↔ wordsPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (wordsPartyNode_strength i) (wordsPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (wordsPartyNode_strength i) (wordsPartyNode_strength j)
+    (jesusWordsDisputeClauses.spec i) (jesusWordsDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/SolaScriptura/Dispute.lean b/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
index fb10de7..267c51d 100644
--- a/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
+++ b/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
@@ -179,6 +179,8 @@ theorem mark7PartyNode_strength : ∀ i, (mark7PartyNode i).strength = mark7Part
   | .trentAsMensCommandments => tridentineAsMensCommandments_strength
   | .trentAsApostolicWord => tridentineAsApostolicWord_strength
 
+prepare_clauses mark7DisputeClauses for mark7Dispute
+
 /-- **Who defeats whom**, all 25 pairs. Mark 7's principle defeats Trent read as
 commandments of men, and that reading's reply fails against it. Mark 7's case
 and Trent defeat each other, as Trent states it and read either way. Nothing
@@ -189,7 +191,8 @@ by the kernel — the defeats, and the absences of defeat, alike. -/
 theorem mark7Dispute_defeats :
     ∀ i j, mark7Dispute.defeats i j ↔ mark7PartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (mark7PartyNode_strength i) (mark7PartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (mark7PartyNode_strength i) (mark7PartyNode_strength j)
+    (mark7DisputeClauses.spec i) (mark7DisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean b/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
index e4d8209..f138501 100644
--- a/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
+++ b/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
@@ -154,6 +154,8 @@ theorem viewNode_strength : ∀ i, (viewNode i).strength = viewStrength i
   | .holiness => holinessCase_strength
   | .sacramental => sacramentalCase_strength
 
+prepare_clauses spiritBaptismDisputeClauses for spiritBaptismDispute
+
 /-- **Who defeats whom**, all 16 pairs: four standoffs, and nothing else. The
 conversion view and each subsequence view defeat each other — "no second to
 seek" against "a second to seek" — and the Pentecostal view also denies the
@@ -163,7 +165,8 @@ subsequence view defeat each other on the same point. Every cell is computed by
 theorem spiritBaptismDispute_defeats :
     ∀ i j, spiritBaptismDispute.defeats i j ↔ viewDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (viewNode_strength i) (viewNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (viewNode_strength i) (viewNode_strength j)
+    (spiritBaptismDisputeClauses.spec i) (spiritBaptismDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/bench/Engine.lean b/arguments/bench/Engine.lean
index 44eb650..0800777 100644
--- a/arguments/bench/Engine.lean
+++ b/arguments/bench/Engine.lean
@@ -168,6 +168,14 @@ example : ∀ i j, septuagintDispute.defeats i j ↔ septuagintPartyDefeats i j
     (septuagintPartyNode_strength j) ?_
   cases i <;> cases j <;> horn_certify
 
+#bench "table, prepared: Septuagint, 36 cells" in
+example : ∀ i j, septuagintDispute.defeats i j ↔ septuagintPartyDefeats i j := by
+  intro i j
+  refine Horn.defeats_iff_of_prepared (septuagintPartyNode_strength i)
+    (septuagintPartyNode_strength j) (septuagintDisputeClauses.spec i)
+    (septuagintDisputeClauses.spec j) ?_
+  cases i <;> cases j <;> horn_certify
+
 #bench "verdict: Septuagint, grounded in stages" in
 example : Verdict septuagintDispute where
   finite := septuagintFinite
@@ -275,6 +283,15 @@ example : Satisfiable paulineCase.premises := by
 example : Grants tridentineCase (notP .pistisChristouObjective) := by
   satisfied_by trentWithoutDeliveranceReading [Grants, solaFideDefs]
 
+#bench (runs := 1) "table, prepared: sola fide, first half, 72 cells" in
+example (i : Party)
+    (hi : i ∈ [.pauline, .dominical, .apostolic, .trent, .apocalyptic, .sanders])
+    (j : Party) : solaFideDispute.defeats i j ↔ partyDefeats i j := by
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (solaFideDisputeClauses.spec i) (solaFideDisputeClauses.spec j) ?_
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hi
+  rcases hi with rfl | rfl | rfl | rfl | rfl | rfl <;> cases j <;> horn_certify
+
 #bench "strengths: James hearing under evidence, 12 parties" in
 example :
     ∀ i, ((jamesRegister.rerated .evidence).node i).strength = ratedStrength .evidence i := by
diff --git a/docs/src/logic.md b/docs/src/logic.md
index d9c4b19..8c640da 100644
--- a/docs/src/logic.md
+++ b/docs/src/logic.md
@@ -572,9 +572,12 @@ dispute's relation equal to the table. Every cell is computed from the
 premises and checked by the kernel — the defeats and the absences alike:
 
 ```lean
+prepare_clauses isaiahDisputeClauses for isaiahDispute
+
 theorem isaiahDispute_defeats : ∀ i j, isaiahDispute.defeats i j ↔ partyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (isaiahDisputeClauses.spec i) (isaiahDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 ```
 
@@ -613,6 +616,13 @@ can only make the proof fail, and `Horn.defeats_iff_of_certified` states exactly
 what `Horn.defeats_iff_of_defeats?` does. `decide +kernel` on `Horn.defeats?`
 still proves any cell, searching.
 
+Every cell asks its questions of two parties' positions as clauses, and a party
+appears in a row and a column of cells. `prepare_clauses` converts each party's
+position once, writes the clauses out, and proves for each party that they are
+what the conversion gives (`isaiahDisputeClauses.spec`); every cell then reads
+them, and `Horn.defeats_iff_of_prepared` takes the proofs, so the kernel converts
+each position once per table rather than once per cell.
+
 A single defeat worth naming is one line, from the same computation:
 
 ```lean
diff --git a/docs/src/performance.md b/docs/src/performance.md
index 24f22b1..dd71fe5 100644
--- a/docs/src/performance.md
+++ b/docs/src/performance.md
@@ -79,6 +79,45 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s),
 | 7 | Find exclusions through shared keys, not every pair | the sola fide joins | 45.4 s, 3.43 GiB | 10.6 s, 1.06 GiB | 0.008 | kept |
 | 8 | Certify the support and part-of tables | sola fide's part-of table | 8.01 s, 131 MiB | 5.00 s, 102 MiB | 0.008 | kept |
 | 9 | Check a named reading in the kernel, as a table, not by `simp` | `satisfied_by` and `leaves_open` | 1.11 s, 8 MiB | 45 ms, 4 MiB | 0.008 | kept |
+| 10 | Convert each party's position to clauses once per table, not once per cell | the certified defeat tables | 1.61 s, 13 MiB | 0.99 s, 11 MiB | 0.008 | kept |
+
+Round 10, measured on one side of a `scripts/bench-ab.sh` run against `main`,
+five interleaved rounds, as rounds 3 and 8 were: each defeat table is
+benchmarked certified, as before, and prepared. A certified cell converted both
+parties' positions to clauses, so a party appearing in a row and a column of
+cells was converted once for every cell. `prepare_clauses` converts each
+party's position once, at elaboration time, writes the clauses out, and has the
+kernel check, once for each party, that they are what the conversion gives;
+every cell then reads them (`Horn.defeatsWith?`,
+`Horn.defeats_iff_of_prepared`). The Septuagint's table fell from 1.61 s to
+0.99 s (−39%, p = 0.008), and half of sola fide's from 7.14 s to 5.44 s (−24%,
+p = 0.008); preparing sola fide's twelve parties costs 0.35 s, once. Every
+benchmark shared with `main` matched it. An earlier run, before the hints were
+searched from the clauses rather than the packages, measured −39% and −12%
+(p = 0.016).
+
+Before this, the round's real target was measured and set aside. Pruning each
+question to the components of a position it touches, found by union-find over
+the claims each clause mentions, asked the kernel about a third of the clauses
+(6,671 of 19,800 in half of sola fide's table) but saved only 15% of the time.
+Most of a question's cost is not in the clauses it reads but in how the kernel
+reads them: a model check of Paul's 33 clauses took 7.6 ms, of which the
+library's list functions, compiled through `brecOn`, and each claim's
+constructor index, computed by a case split over the claim type's hundred-odd
+constructors, are most. Written on `List.rec` and over indices, the same check
+took about 3 ms, cold.
+
+That did not carry over to the tables, and is recorded so that nobody tries it
+again. The checker's model check, clause checks and replay were rewritten on
+`List.rec`, each function proved equal to its core counterpart. A lookup written
+that way, `List.rec` over `Nat.rec`, made each refutation's replay exponential
+in the kernel, from 0.13 s to over 150 s as a synthetic position grew from 24 to
+32 formulas; without it, against this round's head, five interleaved rounds,
+neither table moved (the prepared ones −5%, p = 0.15, and +2%, p = 0.84) and
+one certified cell was 21% slower (p = 0.032). Within a cell the kernel shares
+the work the cold measurement repeated, so the list functions are not where a
+table's time goes. The rewrite was dropped, and clauses over indices with it,
+which the same measurement had suggested.
 
 Round 9, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A
 profile of the slowest modules after round 6 put most of their elaboration in
diff --git a/examples/TestimonyExamples/Checks.lean b/examples/TestimonyExamples/Checks.lean
index 1a82bc0..6e077c1 100644
--- a/examples/TestimonyExamples/Checks.lean
+++ b/examples/TestimonyExamples/Checks.lean
@@ -52,7 +52,7 @@ The grits
 #guard_msgs in
 #check_refutations under TestimonyExamples using unfoldSets
 
-/-- info: every entry is a tagged definition, and every key names one: 76 definitions, 17 entries -/
+/-- info: every entry is a tagged definition, and every key names one: 78 definitions, 17 entries -/
 #guard_msgs in
 #check_citations under TestimonyExamples
 
diff --git a/examples/TestimonyExamples/Grits/Dispute.lean b/examples/TestimonyExamples/Grits/Dispute.lean
index b39fe44..d79e199 100644
--- a/examples/TestimonyExamples/Grits/Dispute.lean
+++ b/examples/TestimonyExamples/Grits/Dispute.lean
@@ -163,6 +163,8 @@ theorem sideNode_strength : ∀ i, (sideNode i).strength = sideStrength i
   | .direct => direct_strength
   | .cross => cross_strength
 
+prepare_clauses gritsDisputeClauses for gritsDispute
+
 /-- **Who defeats whom**, all four pairs. The cross-examination defeats the
 testimony: it denies the five-minute breakfast and the five minutes, and it is
 the stronger. The testimony's denials of the twenty minutes are attacks, and
@@ -170,7 +172,8 @@ fail: its weakest link is weaker than the cross-examination's. Every cell is
 computed by `Horn.defeats?` and checked by the kernel. -/
 theorem gritsDispute_defeats : ∀ i j, gritsDispute.defeats i j ↔ sideDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (sideNode_strength i) (sideNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (sideNode_strength i) (sideNode_strength j)
+    (gritsDisputeClauses.spec i) (gritsDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
@@ -277,14 +280,16 @@ theorem atTheFastCookNode_strength : ∀ i, (atTheFastCookNode i).strength = fas
   | .direct => direct_strength
   | .cross => crossAtTheFastCook_strength
 
+prepare_clauses atTheFastCookDisputeClauses for atTheFastCookDispute
+
 /-- **Who defeated whom at the fast cook**, all four pairs: a standoff. With both
 weakest links `disputed`, each side's attacks on the other are defeats. Every
 cell is computed by `Horn.defeats?` and checked by the kernel. -/
 theorem atTheFastCookDispute_defeats :
     ∀ i j, atTheFastCookDispute.defeats i j ↔ fastCookDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (atTheFastCookNode_strength i)
-    (atTheFastCookNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (atTheFastCookNode_strength i) (atTheFastCookNode_strength j)
+    (atTheFastCookDisputeClauses.spec i) (atTheFastCookDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute at the fast cook, in the form the verdict solver computes with. -/