diff --git a/Testimony/Logic/Certificate.lean b/Testimony/Logic/Certificate.lean
index 339fbc4..1f699cf 100644
--- a/Testimony/Logic/Certificate.lean
+++ b/Testimony/Logic/Certificate.lean
@@ -1,5 +1,6 @@
 import Testimony.Logic.Horn
 import Testimony.Logic.Credibility
+import Testimony.Logic.Support
 
 /-!
 # Testimony.Logic.Certificate — finding what the kernel checks
@@ -115,6 +116,21 @@ question `Horn.satisfiable_of_certified` asks. -/
 def hintsAppend (index : α → ℕ) (Γ Δ : List (Formula α)) : List Hint :=
   [hintOnAll index (base Γ) Δ]
 
+/-- **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. -/
+@[nospecialize]
+def supportHints (index : α → ℕ) (a b : ArgumentPackage α) : List Hint :=
+  let ba := base [a.conclusion]
+  (b.premises.filter (Page.Explanation.isLiteral ·)).map fun φ => hintOnAll index ba [∼φ]
+
+/-- **The hints for a part-of cell**, in the order `partOfBy?` asks its
+questions: for each premise of `b`, whether `a`'s premises entail it. -/
+@[nospecialize]
+def partHints (index : α → ℕ) (b a : ArgumentPackage α) : List Hint :=
+  let ba := base a.premises
+  b.premises.map fun φ => hintOnAll index ba (entailsQuestion φ)
+
 variable [HasPostulates α]
 
 /-- **The hints for a dissent's findings**, in the order `Dissent.findingsBy?`
@@ -176,25 +192,29 @@ def injectiveFor (index : Expr) : MetaM Expr := do
 
 /-- The search that finds a decision's hints, from the decision the goal
 states: a defeat cell (`Horn.defeatsBy?`), a dissent's findings
-(`Dissent.findingsBy?`), or one question of satisfiability
-(`Horn.satisfiableAppend?`). -/
+(`Dissent.findingsBy?`), a support or part-of cell (`supportsBy?`,
+`partOfBy?`), or one question of satisfiability (`Horn.satisfiableAppend?`). -/
 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 ``Dissent.findingsBy? 6 then
     mkAppOptM ``Horn.findingsHints #[args[0]!, args[1]!, args[2]!, index, args[5]!]
+  else if lhs.isAppOfArity ``supportsBy? 6 then
+    mkAppOptM ``Horn.supportHints #[args[0]!, args[1]!, index, args[4]!, args[5]!]
+  else if lhs.isAppOfArity ``partOfBy? 6 then
+    mkAppOptM ``Horn.partHints #[args[0]!, args[1]!, index, args[4]!, args[5]!]
   else if lhs.isAppOfArity ``Horn.satisfiableAppend? 6 then
     let base := args[4]!
     unless base.isAppOfArity ``Horn.clausesOf 2 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? …` or \
-      `Horn.satisfiableAppend? …`, got{indentExpr lhs}"
+    throwError "horn_certify: expected `Horn.defeatsBy? …`, `Dissent.findingsBy? …`, \
+      `supportsBy? …`, `partOfBy? …` or `Horn.satisfiableAppend? …`, got{indentExpr lhs}"
 
 /-- Prove `∃ index, Function.Injective index ∧ ∃ hints, decision index hints … = v`,
-for a defeat cell or a dissent's findings, or `∃ index hints, … = v` for a
+for a defeat, support or part-of cell or a dissent's findings, or `∃ index hints, … = v` for a
 question of satisfiability, by finding the hints and having the kernel check
 them. -/
 elab (name := hornCertify) "horn_certify" : tactic => do
diff --git a/Testimony/Logic/Support.lean b/Testimony/Logic/Support.lean
index cd4b82f..270704b 100644
--- a/Testimony/Logic/Support.lean
+++ b/Testimony/Logic/Support.lean
@@ -14,8 +14,10 @@ another; that one is part of another.
 
 `Supports a b` is that relation: `a`'s conclusion entails a **claim** `b` rests
 on — an atom or a denied atom among `b`'s premises. It is decided by the Horn
-engine and checked by the kernel, as defeats are (`supports?`,
-`supports_iff_of_supports?`).
+engine and checked by the kernel, as defeats are: from hints, a model or a
+refutation for each question, which `horn_certify` finds and the kernel checks
+(`supportsBy?`, `supports_iff_of_certified`), or by a search the kernel runs
+itself (`supports?`).
 
 ## Why claims and not steps
 
@@ -56,47 +58,107 @@ section Decide
 
 variable [DecidableEq α]
 
-/-- For each claim among `b`'s premises, whether `a`'s conclusion can hold with
-its negation: `some false` is an entailment. -/
-def supportChecks (a b : ArgumentPackage α) : List (Formula α × Option Bool) :=
-  (b.premises.filter (Page.Explanation.isLiteral ·)).map fun φ =>
-    (φ, satisfiable? [a.conclusion, ∼φ])
-
-/-- **Whether `a` supports `b`**, decided by the engine: `none` when some
-claim's check is undecided and none succeeded. -/
-def supports? (a b : ArgumentPackage α) : Option Bool :=
-  if (supportChecks a b).any (·.2 == some false) then some true
-  else if (supportChecks a b).all (·.2 == some true) then some false
+/-! #### Checks, each with a hint
+
+Both relations ask one question of satisfiability per premise of `b`, and each
+question can be given a hint, a model or a refutation, which the kernel checks
+in place of a search (`Horn.clausesSatisfiableBy?`). `checksBy` hands the
+questions their hints in order, and any question without one is searched. -/
+
+/-- One check per formula, each asked with the hint at its position, or with
+`search` past the end of the hints. -/
+def checksBy (f : Hint → Formula α → Option Bool) :
+    List Hint → List (Formula α) → List (Option Bool)
+  | _, [] => []
+  | hs, φ :: φs => f (hs.headD .search) φ :: checksBy f hs.tail φs
+
+omit [DecidableEq α] in
+/-- Every check was asked of one of the formulas, with a hint that is `search`
+unless the index tells atoms apart. -/
+theorem mem_checksBy {P : Prop} {f : Hint → Formula α → Option Bool} {hs : List Hint}
+    {φs : List (Formula α)} {x : Option Bool} (hidx : P ∨ hs = []) (hx : x ∈ checksBy f hs φs) :
+    ∃ φ ∈ φs, ∃ h, (P ∨ h = .search) ∧ f h φ = x := by
+  induction φs generalizing hs with
+  | nil => simp [checksBy] at hx
+  | cons φ φs ih =>
+    rcases List.mem_cons.mp hx with rfl | hx
+    · refine ⟨φ, List.mem_cons_self, _, hidx.imp id fun h => ?_, rfl⟩
+      subst h; rfl
+    · obtain ⟨ψ, hψ, h, hh, e⟩ := ih (hs := hs.tail) (hidx.imp id fun h => by subst h; rfl) hx
+      exact ⟨ψ, List.mem_cons_of_mem _ hψ, h, hh, e⟩
+
+omit [DecidableEq α] in
+/-- Every formula was asked about, with a hint that is `search` unless the index
+tells atoms apart. -/
+theorem checksBy_mem {P : Prop} {f : Hint → Formula α → Option Bool} {hs : List Hint}
+    {φs : List (Formula α)} {φ : Formula α} (hidx : P ∨ hs = []) (hφ : φ ∈ φs) :
+    ∃ h, (P ∨ h = .search) ∧ f h φ ∈ checksBy f hs φs := by
+  induction φs generalizing hs with
+  | nil => simp at hφ
+  | cons ψ φs ih =>
+    rcases List.mem_cons.mp hφ with rfl | hφ
+    · refine ⟨_, hidx.imp id fun h => ?_, List.mem_cons_self⟩
+      subst h; rfl
+    · obtain ⟨h, hh, hm⟩ := ih (hs := hs.tail) (hidx.imp id fun h => by subst h; rfl) hφ
+      exact ⟨h, hh, List.mem_cons_of_mem _ hm⟩
+
+/-- For each claim among `b`'s premises, in order, whether `a`'s conclusion can
+hold with its negation, from a hint: `some false` is an entailment. `a`'s
+conclusion is converted to clauses once. -/
+def supportChecksBy (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) :
+    List (Option Bool) :=
+  let ca := clausesOf [a.conclusion]
+  checksBy (fun h φ => satisfiableAppend? index h ca [∼φ]) hints
+    (b.premises.filter (Page.Explanation.isLiteral ·))
+
+/-- **Whether `a` supports `b`**, decided from hints: `none` when some claim's
+check is undecided, or its hint did not check, and none succeeded. -/
+def supportsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) : Option Bool :=
+  let checks := supportChecksBy index hints a b
+  if checks.any (· == some false) then some true
+  else if checks.all (· == some true) then some false
   else none
 
-theorem supports_of_supports? {a b : ArgumentPackage α} (h : supports? a b = some true) :
+/-- **Whether `a` supports `b`**, every question searched: `supportsBy?` with
+no hints. -/
+def supports? (a b : ArgumentPackage α) : Option Bool := supportsBy? (fun _ => 0) [] a b
+
+theorem supports_of_supportsBy? {index : α → ℕ} {hints : List Hint} {a b : ArgumentPackage α}
+    (hidx : Function.Injective index ∨ hints = []) (e : supportsBy? index hints a b = some true) :
     Supports a b := by
-  unfold supports? at h
-  split at h
+  dsimp only [supportsBy?] at e
+  split at e
   · rename_i hany
-    obtain ⟨⟨φ, r⟩, hmem, hr⟩ := List.any_eq_true.mp hany
-    simp only [supportChecks, List.mem_map, List.mem_filter, Prod.mk.injEq] at hmem
-    obtain ⟨ψ, ⟨hψ, hlit⟩, rfl, rfl⟩ := hmem
-    have hsat : ¬ Satisfiable ([a.conclusion] ++ [∼ψ]) :=
-      not_satisfiable_of_satisfiable? (by simpa using hr)
-    exact ⟨ψ, hψ, hlit, entails_iff_not_satisfiable.mpr hsat⟩
-  · split at h <;> simp at h
-
-theorem not_supports_of_supports? {a b : ArgumentPackage α} (h : supports? a b = some false) :
+    obtain ⟨r, hmem, hr⟩ := List.any_eq_true.mp hany
+    obtain ⟨φ, hφ, h, hh, rfl⟩ := mem_checksBy hidx hmem
+    obtain ⟨hφ, hlit⟩ := List.mem_filter.mp hφ
+    exact ⟨φ, hφ, hlit, entails_iff_not_satisfiable.mpr
+      (not_satisfiable_of_satisfiableAppend? hh (by simpa using hr))⟩
+  · split at e <;> simp at e
+
+theorem not_supports_of_supportsBy? {index : α → ℕ} {hints : List Hint}
+    {a b : ArgumentPackage α} (e : supportsBy? index hints a b = some false) :
     ¬ Supports a b := by
-  unfold supports? at h
-  split at h
-  · simp at h
-  · split at h
+  dsimp only [supportsBy?] at e
+  split at e
+  · simp at e
+  · split at e
     · rename_i hall
       rintro ⟨φ, hφ, hlit, hent⟩
-      have hmem : (φ, satisfiable? [a.conclusion, ∼φ]) ∈ supportChecks a b := by
-        simp only [supportChecks, List.mem_map, List.mem_filter]
-        exact ⟨φ, ⟨hφ, hlit⟩, rfl⟩
-      have hsat : satisfiable? ([a.conclusion] ++ [∼φ]) = some true := by
-        simpa using List.all_eq_true.mp hall _ hmem
-      exact entails_iff_not_satisfiable.mp hent (satisfiable_of_satisfiable? hsat)
-    · simp at h
+      obtain ⟨h, -, hmem⟩ := checksBy_mem (f := fun h φ =>
+        satisfiableAppend? index h (clausesOf [a.conclusion]) [∼φ]) (P := True) (.inl trivial)
+        (List.mem_filter.mpr ⟨hφ, hlit⟩)
+      exact entails_iff_not_satisfiable.mp hent
+        (satisfiable_of_satisfiableAppend? (by simpa using List.all_eq_true.mp hall _ hmem))
+    · simp at e
+
+theorem supports_of_supports? {a b : ArgumentPackage α} (h : supports? a b = some true) :
+    Supports a b :=
+  supports_of_supportsBy? (.inr rfl) h
+
+theorem not_supports_of_supports? {a b : ArgumentPackage α} (h : supports? a b = some false) :
+    ¬ Supports a b :=
+  not_supports_of_supportsBy? h
 
 /-- **A support table cell, from the engine**: whenever it decides, the relation
 is exactly what it says. -/
@@ -108,6 +170,20 @@ theorem supports_iff_of_supports? {a b : ArgumentPackage α} {P : Prop} [Decidab
   · simp only [hP, decide_false] at h
     exact ⟨fun hs => absurd hs (not_supports_of_supports? h), fun h' => absurd h' hP⟩
 
+/-- **A support table cell, from hints the kernel checks.** Whichever index
+that tells atoms apart, and whichever hints, decide the cell, the answer is
+sound. `horn_certify` (`Testimony.Logic.Certificate`) finds them. -/
+theorem supports_iff_of_certified {a b : ArgumentPackage α} {P : Prop} [Decidable P]
+    (h : ∃ (index : α → ℕ), Function.Injective index ∧
+      ∃ hints : List Hint, supportsBy? index hints a b = some (decide P)) :
+    Supports a b ↔ P := by
+  obtain ⟨_, hinj, _, h⟩ := h
+  by_cases hP : P
+  · simp only [hP, decide_true] at h
+    exact iff_of_true (supports_of_supportsBy? (.inl hinj) h) hP
+  · simp only [hP, decide_false] at h
+    exact iff_of_false (not_supports_of_supportsBy? h) hP
+
 end Decide
 
 /-! ### One position as part of another
@@ -160,37 +236,84 @@ theorem not_entails_of_entailsCheck {Γ : List (Formula α)} {φ : Formula α}
   | imp p q => exact fun he => entails_imp_iff.mp he (satisfiable_of_satisfiable? h)
   | _ => exact fun he => entails_iff_not_satisfiable.mp he (satisfiable_of_satisfiable? h)
 
-/-- For each premise of `b`, whether `a`'s premises entail it. -/
-def partChecks (b a : ArgumentPackage α) : List (Option Bool) :=
-  b.premises.map (entailsCheck a.premises)
+/-- What is asked of a list of formulas to learn whether it entails `φ`: for a
+step `p → q`, `p` and `q`'s negation, and otherwise `φ`'s negation. The list
+entails `φ` when it cannot hold with them. -/
+def entailsQuestion : Formula α → List (Formula α)
+  | .imp p q => [p, ∼q]
+  | φ => [∼φ]
+
+/-- Whether the formulas whose clauses are `base` entail `φ`, from a hint:
+`some false` is an entailment. -/
+def entailsCheckBy (index : α → ℕ) (h : Hint) (base : Option (List (Clause α)))
+    (φ : Formula α) : Option Bool :=
+  satisfiableAppend? index h base (entailsQuestion φ)
+
+theorem entails_of_entailsCheckBy {index : α → ℕ} {h : Hint} {Γ : List (Formula α)}
+    {φ : Formula α} (hidx : Function.Injective index ∨ h = .search)
+    (e : entailsCheckBy index h (clausesOf Γ) φ = some false) : Entails Γ φ := by
+  have hn := not_satisfiable_of_satisfiableAppend? hidx e
+  cases φ with
+  | imp p q => exact entails_imp_iff.mpr hn
+  | _ => exact entails_iff_not_satisfiable.mpr hn
 
-/-- **Whether `b` is part of `a`**, decided by the engine. -/
-def partOf? (b a : ArgumentPackage α) : Option Bool :=
-  if (partChecks b a).all (· == some false) then some true
-  else if (partChecks b a).any (· == some true) then some false
+theorem not_entails_of_entailsCheckBy {index : α → ℕ} {h : Hint} {Γ : List (Formula α)}
+    {φ : Formula α} (e : entailsCheckBy index h (clausesOf Γ) φ = some true) :
+    ¬ Entails Γ φ := by
+  have hs := satisfiable_of_satisfiableAppend? e
+  cases φ with
+  | imp p q => exact fun he => entails_imp_iff.mp he hs
+  | _ => exact fun he => entails_iff_not_satisfiable.mp he hs
+
+/-- For each premise of `b`, in order, whether `a`'s premises entail it, from a
+hint. `a`'s premises are converted to clauses once. -/
+def partChecksBy (index : α → ℕ) (hints : List Hint) (b a : ArgumentPackage α) :
+    List (Option Bool) :=
+  let ca := clausesOf a.premises
+  checksBy (fun h φ => entailsCheckBy index h ca φ) hints b.premises
+
+/-- **Whether `b` is part of `a`**, decided from hints. -/
+def partOfBy? (index : α → ℕ) (hints : List Hint) (b a : ArgumentPackage α) : Option Bool :=
+  let checks := partChecksBy index hints b a
+  if checks.all (· == some false) then some true
+  else if checks.any (· == some true) then some false
   else none
 
-theorem partOf_of_partOf? {b a : ArgumentPackage α} (h : partOf? b a = some true) :
+/-- **Whether `b` is part of `a`**, every question searched: `partOfBy?` with
+no hints. -/
+def partOf? (b a : ArgumentPackage α) : Option Bool := partOfBy? (fun _ => 0) [] b a
+
+theorem partOf_of_partOfBy? {index : α → ℕ} {hints : List Hint} {b a : ArgumentPackage α}
+    (hidx : Function.Injective index ∨ hints = []) (e : partOfBy? index hints b a = some true) :
     PartOf b a := by
-  unfold partOf? at h
-  split at h
+  dsimp only [partOfBy?] at e
+  split at e
   · rename_i hall
     intro φ hφ
-    have hmem := List.mem_map_of_mem (f := entailsCheck a.premises) hφ
-    exact entails_of_entailsCheck (by simpa using List.all_eq_true.mp hall _ hmem)
-  · split at h <;> simp at h
-
-theorem not_partOf_of_partOf? {b a : ArgumentPackage α} (h : partOf? b a = some false) :
-    ¬ PartOf b a := by
-  unfold partOf? at h
-  split at h
-  · simp at h
-  · split at h
+    obtain ⟨h, hh, hmem⟩ := checksBy_mem (f := fun h φ =>
+      entailsCheckBy index h (clausesOf a.premises) φ) hidx hφ
+    exact entails_of_entailsCheckBy hh (by simpa using List.all_eq_true.mp hall _ hmem)
+  · split at e <;> simp at e
+
+theorem not_partOf_of_partOfBy? {index : α → ℕ} {hints : List Hint} {b a : ArgumentPackage α}
+    (e : partOfBy? index hints b a = some false) : ¬ PartOf b a := by
+  dsimp only [partOfBy?] at e
+  split at e
+  · simp at e
+  · split at e
     · rename_i _ hany
       obtain ⟨r, hr, hr'⟩ := List.any_eq_true.mp hany
-      obtain ⟨φ, hφ, rfl⟩ := List.mem_map.mp (by simpa [partChecks] using hr)
-      exact fun hp => not_entails_of_entailsCheck (by simpa using hr') (hp φ hφ)
-    · simp at h
+      obtain ⟨φ, hφ, h, -, rfl⟩ := mem_checksBy (P := True) (.inl trivial) hr
+      exact fun hp => not_entails_of_entailsCheckBy (by simpa using hr') (hp φ hφ)
+    · simp at e
+
+theorem partOf_of_partOf? {b a : ArgumentPackage α} (h : partOf? b a = some true) :
+    PartOf b a :=
+  partOf_of_partOfBy? (.inr rfl) h
+
+theorem not_partOf_of_partOf? {b a : ArgumentPackage α} (h : partOf? b a = some false) :
+    ¬ PartOf b a :=
+  not_partOf_of_partOfBy? h
 
 /-- **A part-of table cell, from the engine.** -/
 theorem partOf_iff_of_partOf? {b a : ArgumentPackage α} {P : Prop} [Decidable P]
@@ -201,6 +324,18 @@ theorem partOf_iff_of_partOf? {b a : ArgumentPackage α} {P : Prop} [Decidable P
   · simp only [hP, decide_false] at h
     exact ⟨fun hs => absurd hs (not_partOf_of_partOf? h), fun h' => absurd h' hP⟩
 
+/-- **A part-of table cell, from hints the kernel checks.** -/
+theorem partOf_iff_of_certified {b a : ArgumentPackage α} {P : Prop} [Decidable P]
+    (h : ∃ (index : α → ℕ), Function.Injective index ∧
+      ∃ hints : List Hint, partOfBy? index hints b a = some (decide P)) :
+    PartOf b a ↔ P := by
+  obtain ⟨_, hinj, _, h⟩ := h
+  by_cases hP : P
+  · simp only [hP, decide_true] at h
+    exact iff_of_true (partOf_of_partOfBy? (.inl hinj) h) hP
+  · simp only [hP, decide_false] at h
+    exact iff_of_false (not_partOf_of_partOfBy? h) hP
+
 end DecidePart
 
 namespace Dispute
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
index 0ae0287..b740f02 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
@@ -542,15 +542,15 @@ entailment lends a premise (see `Testimony.Logic.Support`). Every cell is
 computed by `supports?` and checked by the kernel. -/
 theorem isaiahDispute_supports : ∀ i j, ¬ isaiahDispute.supports i j := by
   intro i j
-  refine (supports_iff_of_supports? (P := False) ?_).not.mpr id
-  cases i <;> cases j <;> decide +kernel
+  refine (supports_iff_of_certified (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> horn_certify
 
 /-- **No case is part of another's** here, in all thirty-six pairs, except each
 party's own. Every cell is computed by `partOf?` and checked by the kernel. -/
 theorem isaiahDispute_partOf : ∀ i j, isaiahDispute.partOf i j ↔ i = j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute drawn: who defeats whom. -/
 def isaiahMap : ArgumentMap isaiahDispute where
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
index 181535c..7aae5fa 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
@@ -241,15 +241,15 @@ premise. Every cell is computed by `supports?` and checked by the kernel. -/
 theorem genesisDispute_supports :
     ∀ i j, genesisDispute.supports i j ↔ genesisPartySupports i j := by
   intro i j
-  refine supports_iff_of_supports? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine supports_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- **No case is part of another's** here, in all nine pairs, except each
 party's own. Every cell is computed by `partOf?` and checked by the kernel. -/
 theorem genesisDispute_partOf : ∀ i j, genesisDispute.partOf i j ↔ i = j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute drawn: who defeats whom, with no support between the parties. -/
 def genesisMap : ArgumentMap genesisDispute where
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
index 57780f4..7fb96f8 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
@@ -580,15 +580,15 @@ by `supports?` and checked by the kernel. -/
 theorem septuagintDispute_supports :
     ∀ i j, septuagintDispute.supports i j ↔ septuagintPartySupports i j := by
   intro i j
-  refine supports_iff_of_supports? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine supports_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- **No case is part of another's** here, in all thirty-six pairs, except each
 party's own. Every cell is computed by `partOf?` and checked by the kernel. -/
 theorem septuagintDispute_partOf : ∀ i j, septuagintDispute.partOf i j ↔ i = j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute drawn: who defeats whom, and the one support. -/
 def septuagintMap : ArgumentMap septuagintDispute where
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
index f71e7b2..22bacc7 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
@@ -221,15 +221,15 @@ all nine pairs. Every cell is computed by `supports?` and checked by the
 kernel. -/
 theorem wegnerDispute_supports : ∀ i j, ¬ wegnerDispute.supports i j := by
   intro i j
-  refine (supports_iff_of_supports? (P := False) ?_).not.mpr id
-  cases i <;> cases j <;> decide +kernel
+  refine (supports_iff_of_certified (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> horn_certify
 
 /-- **No case is part of another's** here, in all nine pairs, except each
 party's own. Every cell is computed by `partOf?` and checked by the kernel. -/
 theorem wegnerDispute_partOf : ∀ i j, wegnerDispute.partOf i j ↔ i = j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute drawn: who defeats whom. -/
 def wegnerMap : ArgumentMap wegnerDispute where
diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean
index fd4161c..4a39037 100644
--- a/arguments/TestimonyArguments/Checks.lean
+++ b/arguments/TestimonyArguments/Checks.lean
@@ -101,7 +101,7 @@ The canonical witness
 #check_refutations under TestimonyArguments using unfoldSets
 
 /--
-info: every entry is a tagged definition, and every key names one: 2319 definitions, 176 entries
+info: every entry is a tagged definition, and every key names one: 2326 definitions, 176 entries
 -/
 #guard_msgs in
 #check_citations under Testimony
diff --git a/arguments/TestimonyArguments/SolaFide/Dispute.lean b/arguments/TestimonyArguments/SolaFide/Dispute.lean
index b896256..d20d2f2 100644
--- a/arguments/TestimonyArguments/SolaFide/Dispute.lean
+++ b/arguments/TestimonyArguments/SolaFide/Dispute.lean
@@ -987,8 +987,8 @@ support (see `Testimony.Logic.Support`). Every cell is computed by `supports?`
 and checked by the kernel. -/
 theorem solaFideDispute_supports : ∀ i j, ¬ solaFideDispute.supports i j := by
   intro i j
-  refine (supports_iff_of_supports? (P := False) ?_).not.mpr id
-  cases i <;> cases j <;> decide +kernel
+  refine (supports_iff_of_certified (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> horn_certify
 
 /-- Whose case is part of whose, as a table: besides each party's own, two
 pairs. -/
@@ -1008,8 +1008,8 @@ only adds to it; and every case is part of itself. Nothing else. Every cell is
 computed by `partOf?` and checked by the kernel. -/
 theorem solaFideDispute_partOf : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute drawn: who defeats whom, and whose case is part of whose. -/
 def solaFideMap : ArgumentMap solaFideDispute where
diff --git a/arguments/TestimonyArguments/SolaFide/JesusWords.lean b/arguments/TestimonyArguments/SolaFide/JesusWords.lean
index 2746786..2e9d0e6 100644
--- a/arguments/TestimonyArguments/SolaFide/JesusWords.lean
+++ b/arguments/TestimonyArguments/SolaFide/JesusWords.lean
@@ -575,15 +575,15 @@ all 49 pairs. Every cell is computed by `supports?` and checked by the
 kernel. -/
 theorem jesusWordsDispute_supports : ∀ i j, ¬ jesusWordsDispute.supports i j := by
   intro i j
-  refine (supports_iff_of_supports? (P := False) ?_).not.mpr id
-  cases i <;> cases j <;> decide +kernel
+  refine (supports_iff_of_certified (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> horn_certify
 
 /-- Each party's case is part of its own and of no other's. Every cell is
 computed by `partOf?` and checked by the kernel. -/
 theorem jesusWordsDispute_partOf : ∀ i j, jesusWordsDispute.partOf i j ↔ i = j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute over Jesus' words drawn: who defeats whom. -/
 def jesusWordsMap : ArgumentMap jesusWordsDispute where
diff --git a/arguments/TestimonyArguments/SolaScriptura/Dispute.lean b/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
index 77cedaf..fb10de7 100644
--- a/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
+++ b/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
@@ -208,8 +208,8 @@ is not support. Every cell is computed by `supports?` and checked by the
 kernel. -/
 theorem mark7Dispute_supports : ∀ i j, ¬ mark7Dispute.supports i j := by
   intro i j
-  refine (supports_iff_of_supports? (P := False) ?_).not.mpr id
-  cases i <;> cases j <;> decide +kernel
+  refine (supports_iff_of_certified (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> horn_certify
 
 /-- Whose case is part of whose, as a table: besides each party's own, Trent's
 is part of each reading of it. -/
@@ -227,8 +227,8 @@ reading of it, which only adds to it; and every case is part of itself. Every
 cell is computed by `partOf?` and checked by the kernel. -/
 theorem mark7Dispute_partOf : ∀ i j, mark7Dispute.partOf i j ↔ mark7PartyPartOf i j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute over Mark 7 drawn: who defeats whom, and whose case is part of
 whose. -/
diff --git a/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean b/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
index 0ad8ee3..e4d8209 100644
--- a/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
+++ b/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
@@ -177,15 +177,15 @@ def spiritBaptismFinite : Solver.Finite spiritBaptismDispute.defeats where
 `supports?` and checked by the kernel. -/
 theorem spiritBaptismDispute_supports : ∀ i j, ¬ spiritBaptismDispute.supports i j := by
   intro i j
-  refine (supports_iff_of_supports? (P := False) ?_).not.mpr id
-  cases i <;> cases j <;> decide +kernel
+  refine (supports_iff_of_certified (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> horn_certify
 
 /-- Each view's case is part of its own and of no other's. Every cell is computed
 by `partOf?` and checked by the kernel. -/
 theorem spiritBaptismDispute_partOf : ∀ i j, spiritBaptismDispute.partOf i j ↔ i = j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute over Spirit baptism drawn: who defeats whom. -/
 def spiritBaptismMap : ArgumentMap spiritBaptismDispute where
diff --git a/arguments/bench/Engine.lean b/arguments/bench/Engine.lean
index f530e6b..1fddca4 100644
--- a/arguments/bench/Engine.lean
+++ b/arguments/bench/Engine.lean
@@ -243,6 +243,30 @@ example (i : Party)
   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 (runs := 1) "supports: sola fide, 144 cells" in
+example : ∀ i j, ¬ solaFideDispute.supports i j := by
+  intro i j
+  refine (supports_iff_of_supports? (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> decide +kernel
+
+#bench (runs := 1) "supports, certified: sola fide, 144 cells" in
+example : ∀ i j, ¬ solaFideDispute.supports i j := by
+  intro i j
+  refine (supports_iff_of_certified (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> horn_certify
+
+#bench (runs := 1) "part of: sola fide, 144 cells" in
+example : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by
+  intro i j
+  refine partOf_iff_of_partOf? ?_
+  cases i <;> cases j <;> decide +kernel
+
+#bench (runs := 1) "part of, certified: sola fide, 144 cells" in
+example : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by
+  intro i j
+  refine partOf_iff_of_certified ?_
+  cases i <;> 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 4043a9e..d9c4b19 100644
--- a/docs/src/logic.md
+++ b/docs/src/logic.md
@@ -759,14 +759,15 @@ tables of how parties stand together (`Testimony.Logic.Support`).
   of assuming it. So the critics' case is part of Paul's, and Sanders meets Paul
   on the history of Second Temple Judaism, where the literature has the dispute.
 
-Both tables are proved like the defeat table, cell by cell, by `supports?` or
-`partOf?` and `decide +kernel`:
+Both tables are proved like the defeat table, cell by cell, from hints the
+kernel checks: `horn_certify` finds a model or a refutation for each question
+`supportsBy?` or `partOfBy?` asks, and `decide +kernel` checks them.
 
 ```lean
 theorem solaFideDispute_partOf : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 ```
 
 The page draws the graph, lists the parties by number, and tabulates every
diff --git a/docs/src/performance.md b/docs/src/performance.md
index 80100d4..42afca6 100644
--- a/docs/src/performance.md
+++ b/docs/src/performance.md
@@ -77,6 +77,21 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s),
 | 5 | Compare a citation by its key and locus, a key checked to name one entry | a hearing's rerated strengths | 2.54 s, 83 MiB | 0.86 s, 25 MiB | 0.008 | kept |
 | 6 | Replay a refutation on bitmasks (#180) | the certified defeat tables | 7.21 s, 94 MiB | 5.99 s, 70 MiB | 0.008 | kept |
 | 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 |
+
+Round 8, measured on one side of a `scripts/bench-ab.sh` run against `main`,
+five interleaved rounds, as round 3 was: each of sola fide's two tables of how
+parties stand together is benchmarked searched, as before, and certified. Both
+were still decided by a search the kernel ran, `supports?` and `partOf?`, and
+the part-of table converted a party's premises to clauses afresh for every
+premise it asked about. Now each question takes a hint, as a defeat cell's
+does (`supportsBy?`, `partOfBy?`), `horn_certify` finds them, and each party's
+premises are converted once a cell. The part-of table fell from 8.01 s to
+5.00 s (−38%, p = 0.008) and from 131 to 102 MiB; the support table from
+3.37 s to 1.99 s (−41%, p = 0.008), 17 to 13 MiB. The searched forms, now the
+same decisions with no hints, matched `main` (p ≥ 0.55). Measured by hand,
+two runs each: `SolaFide.Dispute` elaborates in 41.5 s against 47.6 s with its
+two tables searched.
 
 Round 7, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A
 profile of `Meanings.SolaFide` put 51 of its 64 seconds in one proof: that the
diff --git a/examples/TestimonyExamples/Grits/Dispute.lean b/examples/TestimonyExamples/Grits/Dispute.lean
index d4342bc..b39fe44 100644
--- a/examples/TestimonyExamples/Grits/Dispute.lean
+++ b/examples/TestimonyExamples/Grits/Dispute.lean
@@ -184,15 +184,15 @@ def gritsFinite : Solver.Finite gritsDispute.defeats where
 `supports?` and checked by the kernel. -/
 theorem gritsDispute_supports : ∀ i j, ¬ gritsDispute.supports i j := by
   intro i j
-  refine (supports_iff_of_supports? (P := False) ?_).not.mpr id
-  cases i <;> cases j <;> decide +kernel
+  refine (supports_iff_of_certified (P := False) ?_).not.mpr id
+  cases i <;> cases j <;> horn_certify
 
 /-- Each side's case is part of its own and of no other's. Every cell is computed
 by `partOf?` and checked by the kernel. -/
 theorem gritsDispute_partOf : ∀ i j, gritsDispute.partOf i j ↔ i = j := by
   intro i j
-  refine partOf_iff_of_partOf? ?_
-  cases i <;> cases j <;> decide +kernel
+  refine partOf_iff_of_certified ?_
+  cases i <;> cases j <;> horn_certify
 
 /-- The dispute over the five minutes drawn: who defeats whom. -/
 def gritsMap : ArgumentMap gritsDispute where