diff --git a/Duper/Interface.lean b/Duper/Interface.lean
index a255f28..c08dbe8 100644
--- a/Duper/Interface.lean
+++ b/Duper/Interface.lean
@@ -7,10 +7,13 @@ open Duper
 open ProverM
 open Lean.Parser
 
+namespace Duper
+
 initialize
   registerTraceClass `duper.saturate.debug
   registerTraceClass `duper.portfolio.debug
   registerTraceClass `duper.monomorphization.debug
+  registerTraceClass `duper.elabFact.debug
 
 register_option duper.printPortfolioInstance : Bool := {
   defValue := false
@@ -416,11 +419,11 @@ def runDuper (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMax
        of this error message to determine whether Duper threw an error due to an actual problem or due to timeout. -/
     throwError "Duper was terminated"
 
-/- Note for converting between Duper's formulas format and Auto's lemmas format. If `hp : p`, then Duper stores the formula
-   `(p, eq_true hp, #[], isFromGoal)` whereas Auto stores the lemma `⟨hp, p, #[]⟩`. Importantly, Duper stores the proof of `p = True` and
-   Auto stores the proof of `p`, so this must be accounted for in the conversion (maybe later, it will be good to refactor Duper
-   to be in alignment with how Auto stores lemmas to avoid the unnecessary cost of this conversion, but for now, it suffices to
-   add or remove `eq_true` as needed) -/
+/- Note for converting between Duper's formulas format and Auto's lemmas format: If `hp : p`, then Duper stores the formula
+   `(p, eq_true hp, #[], isFromGoal, stxArray)` whereas Auto stores the lemma `⟨hp, p, #[], deriv⟩`. Importantly, Duper stores
+   the proof of `p = True` and Auto stores the proof of `p`, so this must be accounted for in the conversion (maybe later, it
+   will be good to refactor Duper to be in alignment with how Auto stores lemmas to avoid the unnecessary cost of this conversion,
+   but for now, it suffices to add or remove `eq_true` as needed) -/
 
 partial def getLeavesFromDTr (t : Auto.DTr) : Array String :=
   match t with
@@ -428,25 +431,24 @@ partial def getLeavesFromDTr (t : Auto.DTr) : Array String :=
   | Auto.DTr.leaf s => #[s]
 
 /-- Converts formulas/lemmas from the format used by Duper to the format used by Auto. Duper uses Auto's deriv DTr to keep
-    track of `isFromGoal` information through the monomorphization procedure. -/
-def formulasToAutoLemmas (formulas : List (Expr × Expr × Array Name × Bool)) : MetaM (Array Auto.Lemma) :=
+    track of `isFromGoal` and optional syntax information through the monomorphization procedure. -/
+def formulasToAutoLemmas (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) : MetaM (Array Auto.Lemma) :=
   formulas.toArray.mapM
-    (fun (fact, proof, params, isFromGoal) =>
-      return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"{isFromGoal}")})
+    (fun (fact, proof, params, isFromGoal, stxOption) =>
+      match stxOption with
+      | none => return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"{isFromGoal}")}
+      | some stx => return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"{isFromGoal}, {stx}")})
 
 /-- Converts formulas/lemmas from the format used by Auto to the format used by Duper. -/
 def autoLemmasToFormulas (lemmas : Array Auto.Lemma) : MetaM (List (Expr × Expr × Array Name × Bool)) :=
-  /- Currently, we don't have any means of determining which lemmas are originally from the goal, so for now, we are
-     indicating that all lemmas don't come from the goal. This behavior should be updated once we get a means of tracking
-     that information through the monomorphization procedure. -/
   lemmas.toList.mapM
     (fun lem => do
       let derivLeaves := getLeavesFromDTr lem.deriv
-      let isFromGoal := derivLeaves.contains "true"
+      let isFromGoal := derivLeaves.any (fun l => "true".isPrefixOf l)
       return (lem.type, ← Meta.mkAppM ``eq_true #[lem.proof], lem.params, isFromGoal))
 
 /-- Given `formulas`, `instanceMaxHeartbeats`, and an instance of Duper `inst`, runs `inst` with monomorphization preprocessing. -/
-def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMaxHeartbeats : Nat)
+def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (instanceMaxHeartbeats : Nat)
   (inst : List (Expr × Expr × Array Name × Bool) → Nat → MetaM Expr) : MetaM Expr := do
   let lemmas ← formulasToAutoLemmas formulas
   -- Calling Auto.unfoldConstAndPreprocessLemma is an essential step for the monomorphization procedure
@@ -456,13 +458,14 @@ def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array
     fun lemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
+      trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"
       trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => (f.1, f.2.2.2))}"
       inst monomorphizedFormulas instanceMaxHeartbeats
   Auto.monoInterface lemmas inhFacts prover
 
 /-- Given `formulas`, `instanceMaxHeartbeats`, `declName?` and an instance of Duper `inst`, runs `inst` with all of Auto's preprocessing
     (monomorphization, skolemization, definition unfolding, exhaustive function extensionality rewrites, and BitVec simplicfication). -/
-def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name)
+def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name)
   (instanceMaxHeartbeats : Nat) (inst : List (Expr × Expr × Array Name × Bool) → Nat → MetaM Expr) : MetaM Expr := do
   let lemmas ← formulasToAutoLemmas formulas
   -- Calling Auto.unfoldConstAndPreprocessLemma is an essential step for the monomorphization procedure
@@ -472,6 +475,7 @@ def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Arra
     fun lemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
+      trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"
       trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => (f.1, f.2.2.2))}"
       inst monomorphizedFormulas instanceMaxHeartbeats
   Auto.runNativeProverWithAuto declName? prover lemmas inhFacts
@@ -479,7 +483,7 @@ def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Arra
 /-- `mkDuperInstance` is called by each `runDuperInstanceN` function to construct the desired Duper instance. Additionally,
     if a user invokes portfolio instance 0 (which is the special instance reserved for allowing the user to manually construct
     an instance with their own configuration options), then this function will be called directly. -/
-def mkDuperInstance (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat)
+def mkDuperInstance (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat)
   (inhabitationReasoning : Option Bool) (preprocessing : Option PreprocessingOption) (includeExpensiveRules : Option Bool)
   (selFunction : Option Nat) : MetaM Expr :=
   let addInhabitationReasoningOption : MetaM Expr → MetaM Expr :=
@@ -502,6 +506,8 @@ def mkDuperInstance (formulas : List (Expr × Expr × Array Name × Bool)) (decl
     addInhabitationReasoningOption ∘ addIncludeExpensiveRulesOption ∘ addSelFunctionOption $
       runDuperInstanceWithMonomorphization formulas instanceMaxHeartbeats runDuper
   | some NoPreprocessing =>
+    -- Remove syntax option from `formulas` since we are not converting to Auto.Lemmas
+    let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2.1))
     addInhabitationReasoningOption ∘ addIncludeExpensiveRulesOption ∘ addSelFunctionOption $
       runDuper formulas instanceMaxHeartbeats
   | none => -- Use full preprocessing by default
@@ -513,7 +519,7 @@ def mkDuperInstance (formulas : List (Expr × Expr × Array Name × Bool)) (decl
     - inhabitationReasoning = false
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = false -/
-def runDuperInstance1 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance1 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 4)
 
@@ -522,7 +528,7 @@ def runDuperInstance1 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = true
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = false -/
-def runDuperInstance2 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance2 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 4)
 
@@ -531,7 +537,7 @@ def runDuperInstance2 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = false
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = true -/
-def runDuperInstance3 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance3 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 11)
 
@@ -540,7 +546,7 @@ def runDuperInstance3 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = true
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = true -/
-def runDuperInstance4 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance4 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 11)
 
@@ -549,7 +555,7 @@ def runDuperInstance4 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = false
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = false -/
-def runDuperInstance5 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance5 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 13)
 
@@ -558,7 +564,7 @@ def runDuperInstance5 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = true
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = false -/
-def runDuperInstance6 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance6 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 13)
 
@@ -567,7 +573,7 @@ def runDuperInstance6 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = true
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = true -/
-def runDuperInstance7 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance7 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 2)
 
@@ -576,7 +582,7 @@ def runDuperInstance7 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = false
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = true -/
-def runDuperInstance8 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance8 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 2)
 
@@ -585,7 +591,7 @@ def runDuperInstance8 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = false
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = false -/
-def runDuperInstance9 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance9 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 4)
 
@@ -594,7 +600,7 @@ def runDuperInstance9 (formulas : List (Expr × Expr × Array Name × Bool)) (de
     - inhabitationReasoning = true
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = false -/
-def runDuperInstance10 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance10 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 4)
 
@@ -603,7 +609,7 @@ def runDuperInstance10 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = true -/
-def runDuperInstance11 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance11 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 11)
 
@@ -612,7 +618,7 @@ def runDuperInstance11 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = true -/
-def runDuperInstance12 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance12 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 11)
 
@@ -621,7 +627,7 @@ def runDuperInstance12 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = false -/
-def runDuperInstance13 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance13 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 13)
 
@@ -630,7 +636,7 @@ def runDuperInstance13 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = false -/
-def runDuperInstance14 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance14 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 13)
 
@@ -639,7 +645,7 @@ def runDuperInstance14 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = true -/
-def runDuperInstance15 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance15 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 2)
 
@@ -648,7 +654,7 @@ def runDuperInstance15 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = true -/
-def runDuperInstance16 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance16 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 2)
 
@@ -657,7 +663,7 @@ def runDuperInstance16 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = false -/
-def runDuperInstance17 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance17 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := Monomorphization)
     (includeExpensiveRules := false) (selFunction := some 4)
 
@@ -666,7 +672,7 @@ def runDuperInstance17 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = false -/
-def runDuperInstance18 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance18 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := Monomorphization)
     (includeExpensiveRules := false) (selFunction := some 4)
 
@@ -675,7 +681,7 @@ def runDuperInstance18 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = true -/
-def runDuperInstance19 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance19 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := Monomorphization)
     (includeExpensiveRules := true) (selFunction := some 11)
 
@@ -684,7 +690,7 @@ def runDuperInstance19 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = true -/
-def runDuperInstance20 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance20 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := Monomorphization)
     (includeExpensiveRules := true) (selFunction := some 11)
 
@@ -693,7 +699,7 @@ def runDuperInstance20 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = false -/
-def runDuperInstance21 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance21 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := Monomorphization)
     (includeExpensiveRules := false) (selFunction := some 13)
 
@@ -702,7 +708,7 @@ def runDuperInstance21 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = false -/
-def runDuperInstance22 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance22 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := Monomorphization)
     (includeExpensiveRules := false) (selFunction := some 13)
 
@@ -711,7 +717,7 @@ def runDuperInstance22 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = true -/
-def runDuperInstance23 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance23 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := Monomorphization)
     (includeExpensiveRules := true) (selFunction := some 2)
 
@@ -720,7 +726,7 @@ def runDuperInstance23 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = true -/
-def runDuperInstance24 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance24 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := Monomorphization)
     (includeExpensiveRules := true) (selFunction := some 2)
 
@@ -729,7 +735,7 @@ def runDuperInstance24 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = true -/
-def runDuperInstance25 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance25 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 4)
 
@@ -738,7 +744,7 @@ def runDuperInstance25 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = true -/
-def runDuperInstance26 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance26 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 4)
 
@@ -747,7 +753,7 @@ def runDuperInstance26 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = false -/
-def runDuperInstance27 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance27 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 11)
 
@@ -756,7 +762,7 @@ def runDuperInstance27 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = false -/
-def runDuperInstance28 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance28 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 11)
 
@@ -765,7 +771,7 @@ def runDuperInstance28 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = true -/
-def runDuperInstance29 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance29 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 13)
 
@@ -774,7 +780,7 @@ def runDuperInstance29 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = true -/
-def runDuperInstance30 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance30 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 13)
 
@@ -783,7 +789,7 @@ def runDuperInstance30 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = false -/
-def runDuperInstance31 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance31 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 2)
 
@@ -792,7 +798,7 @@ def runDuperInstance31 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = false -/
-def runDuperInstance32 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance32 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 2)
 
@@ -801,7 +807,7 @@ def runDuperInstance32 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = true -/
-def runDuperInstance33 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance33 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 4)
 
@@ -810,7 +816,7 @@ def runDuperInstance33 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = true -/
-def runDuperInstance34 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance34 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 4)
 
@@ -819,7 +825,7 @@ def runDuperInstance34 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = false -/
-def runDuperInstance35 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance35 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 11)
 
@@ -828,7 +834,7 @@ def runDuperInstance35 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = false -/
-def runDuperInstance36 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance36 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 11)
 
@@ -837,7 +843,7 @@ def runDuperInstance36 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = true -/
-def runDuperInstance37 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance37 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 13)
 
@@ -846,7 +852,7 @@ def runDuperInstance37 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = true -/
-def runDuperInstance38 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance38 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := NoPreprocessing)
     (includeExpensiveRules := true) (selFunction := some 13)
 
@@ -855,7 +861,7 @@ def runDuperInstance38 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = false -/
-def runDuperInstance39 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance39 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 2)
 
@@ -864,7 +870,7 @@ def runDuperInstance39 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = false -/
-def runDuperInstance40 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance40 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := FullPreprocessing)
     (includeExpensiveRules := false) (selFunction := some 2)
 
@@ -873,7 +879,7 @@ def runDuperInstance40 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = true -/
-def runDuperInstance41 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance41 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := Monomorphization)
     (includeExpensiveRules := true) (selFunction := some 4)
 
@@ -882,7 +888,7 @@ def runDuperInstance41 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 4 (which corresponds to Zipperposition's default selection function)
     - includeExpensiveRules = true -/
-def runDuperInstance42 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance42 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := Monomorphization)
     (includeExpensiveRules := true) (selFunction := some 4)
 
@@ -891,7 +897,7 @@ def runDuperInstance42 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = false -/
-def runDuperInstance43 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance43 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := Monomorphization)
     (includeExpensiveRules := false) (selFunction := some 11)
 
@@ -900,7 +906,7 @@ def runDuperInstance43 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
     - includeExpensiveRules = false -/
-def runDuperInstance44 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance44 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := Monomorphization)
     (includeExpensiveRules := false) (selFunction := some 11)
 
@@ -909,7 +915,7 @@ def runDuperInstance44 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = true -/
-def runDuperInstance45 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance45 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := Monomorphization)
     (includeExpensiveRules := true) (selFunction := some 13)
 
@@ -918,7 +924,7 @@ def runDuperInstance45 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
     - includeExpensiveRules = true -/
-def runDuperInstance46 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance46 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := Monomorphization)
     (includeExpensiveRules := true) (selFunction := some 13)
 
@@ -927,7 +933,7 @@ def runDuperInstance46 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = true
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = false -/
-def runDuperInstance47 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance47 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := true) (preprocessing := Monomorphization)
     (includeExpensiveRules := false) (selFunction := some 2)
 
@@ -936,7 +942,7 @@ def runDuperInstance47 (formulas : List (Expr × Expr × Array Name × Bool)) (d
     - inhabitationReasoning = false
     - selFunction = 2 (NoSelection)
     - includeExpensiveRules = false -/
-def runDuperInstance48 (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
+def runDuperInstance48 (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   mkDuperInstance formulas declName? instanceMaxHeartbeats (inhabitationReasoning := false) (preprocessing := Monomorphization)
     (includeExpensiveRules := false) (selFunction := some 2)
 
@@ -998,7 +1004,7 @@ def instanceHasInhabitationReasoning [Monad m] [MonadError m] (n : Nat) : m Bool
 /-- If the given duper instance `n` has inhabitation reasoning disabled and there is another instance `m` that is identical
     except that it has inhabitation reasoning enabled, then `getInstanceWithInhabitationReasoning` returns `some m`. Otherwise,
     `getInstanceWithInhabitationReasoning` returns `none`. -/
-def getInstanceWithInhabitationReasoning (n : Nat) : Option (Nat × (List (Expr × Expr × Array Name × Bool) → Option Name → Nat → MetaM Expr)) := do
+def getInstanceWithInhabitationReasoning (n : Nat) : Option (Nat × (List (Expr × Expr × Array Name × Bool × Option Term) → Option Name → Nat → MetaM Expr)) := do
   match n with
   | 1 => some (2, runDuperInstance2)
   | 3 => some (4, runDuperInstance4)
@@ -1029,7 +1035,7 @@ def getInstanceWithInhabitationReasoning (n : Nat) : Option (Nat × (List (Expr
 /-- If the given duper instance `n` has inhabitation reasoning enabled and there is another instance `m` that is identical
     except that it has inhabitation reasoning disabled, then `getInstanceWithoutInhabitationReasoning` returns `some m`. Otherwise,
     `getInstanceWithoutInhabitationReasoning` returns `none`. -/
-def getInstanceWithoutInhabitationReasoning (n : Nat) : Option (Nat × (List (Expr × Expr × Array Name × Bool) → Option Name → Nat → MetaM Expr)) := do
+def getInstanceWithoutInhabitationReasoning (n : Nat) : Option (Nat × (List (Expr × Expr × Array Name × Bool × Option Term) → Option Name → Nat → MetaM Expr)) := do
   match n with
   | 2 => some (1, runDuperInstance1)
   | 4 => some (3, runDuperInstance3)
@@ -1060,7 +1066,7 @@ def getInstanceWithoutInhabitationReasoning (n : Nat) : Option (Nat × (List (Ex
 /-- If the given duper instance `n` has includeExpensiveRules set to false and there is another instance `m` that is identical
     except that it has includeExpensiveRules set to true, then `getInstanceWithExpensiveRules` returns `some m`. Otherwise,
     `getInstanceWithExpensiveRules` returns `none`. -/
-def getInstanceWithExpensiveRules (n : Nat) : Option (Nat × (List (Expr × Expr × Array Name × Bool) → Option Name → Nat → MetaM Expr)) := do
+def getInstanceWithExpensiveRules (n : Nat) : Option (Nat × (List (Expr × Expr × Array Name × Bool × Option Term) → Option Name → Nat → MetaM Expr)) := do
   match n with
   | 1 => some (25, runDuperInstance25)
   | 2 => some (26, runDuperInstance26)
@@ -1091,7 +1097,7 @@ def getInstanceWithExpensiveRules (n : Nat) : Option (Nat × (List (Expr × Expr
 /-- If the given duper instance `n` has includeExpensiveRules set to true and there is another instance `m` that is identical
     except that it has includeExpensiveRules set to false, then `getInstanceWithoutExpensiveRules` returns `some m`. Otherwise,
     `getInstanceWithoutExpensiveRules` returns `none`. -/
-def getInstanceWithoutExpensiveRules (n : Nat) : Option (Nat × (List (Expr × Expr × Array Name × Bool) → Option Name → Nat → MetaM Expr)) := do
+def getInstanceWithoutExpensiveRules (n : Nat) : Option (Nat × (List (Expr × Expr × Array Name × Bool × Option Term) → Option Name → Nat → MetaM Expr)) := do
   match n with
   | 25 => some (1, runDuperInstance1)
   | 26 => some (2, runDuperInstance2)
@@ -1123,8 +1129,8 @@ def getInstanceWithoutExpensiveRules (n : Nat) : Option (Nat × (List (Expr × E
     a contradiction, then `Std.Tactic.TryThis.addSuggestion` will be used to give the user a more specific invocation of duper that can
     reproduce the proof (without having to run duper in portfolio mode). As with the other `runDuper` functions, `runDuperPortfolioMode`
     ultimately returns a proof if successful and throws an error if unsuccessful. -/
-def runDuperPortfolioMode (formulas : List (Expr × Expr × Array Name × Bool)) (declName? : Option Name) (configOptions : ConfigurationOptions)
-  (duperStxInfo : Option (Syntax × Syntax × Syntax.TSepArray `term ","  × Bool)) : MetaM Expr := do
+def runDuperPortfolioMode (formulas : List (Expr × Expr × Array Name × Bool × Option Term)) (declName? : Option Name)
+  (configOptions : ConfigurationOptions) (duperStxInfo : Option (Syntax × Syntax × Syntax.TSepArray `term ","  × Bool)) : MetaM Expr := do
   let initHeartbeats ← IO.getNumHeartbeats
   let maxHeartbeats ← getMaxHeartbeats
   -- Use the preprocessing option to determine the set of portfolio instances
@@ -1280,3 +1286,5 @@ def runDuperPortfolioMode (formulas : List (Expr × Expr × Array Name × Bool))
     throwError
       m!"Duper failed to solve the goal and determined that it will be unable to do so with the current " ++
       m!"configuration of options and selection of premises"
+
+end Duper
diff --git a/Duper/Rules/BoolSimp.lean b/Duper/Rules/BoolSimp.lean
index feb2da8..2f734ca 100644
--- a/Duper/Rules/BoolSimp.lean
+++ b/Duper/Rules/BoolSimp.lean
@@ -14,34 +14,58 @@ open Comparison
 
 initialize Lean.registerTraceClass `duper.rule.boolSimp
 
-/-
+/--
   Rules 1 through 15 are from Leo-III. Rules 16 through 22 and 25 through 27 are from "Superposition with
   First-Class Booleans and Inprocessing Clausification." Rules 23, 24, and 28 were made just for duper.
+  Rules with the `b` suffix operate on `Bool`, rules without the `b` suffix operate on `Prop`.
 -/
 inductive BoolSimpRule
   | rule1 -- s ∨ s ↦ s
+  | rule1b -- s || s ↦ s
   | rule2 -- ¬s ∨ s ↦ True
+  | rule2b -- !s || s ↦ true
   | rule2Sym -- s ∨ ¬s ↦ True
+  | rule2bSym -- s || !s ↦ true
   | rule3 -- s ∨ True ↦ True
+  | rule3b -- s || true ↦ true
   | rule3Sym -- True ∨ s ↦ True
+  | rule3bSym -- true || s ↦ true
   | rule4 -- s ∨ False ↦ s
+  | rule4b -- s || false ↦ s
   | rule4Sym -- False ∨ s ↦ s
+  | rule4bSym -- false || s ↦ s
   | rule5 -- s = s ↦ True
+  | rule5b -- s == s ↦ true
   | rule6 -- s = True ↦ s
+  | rule6b -- s == true ↦ s
   | rule6Sym -- True = s ↦ s
+  | rule6bSym -- true == s ↦ s
   | rule7 -- Not False ↦ True
+  | rule7b -- !false ↦ true
   | rule8 -- s ∧ s ↦ s
+  | rule8b -- s && s ↦ s
   | rule9 -- ¬s ∧ s ↦ False
+  | rule9b -- !s && s ↦ false
   | rule9Sym -- s ∧ ¬s ↦ False
+  | rule9bSym -- s && !s ↦ false
   | rule10 -- s ∧ True ↦ s
+  | rule10b -- s && true ↦ s
   | rule10Sym -- True ∧ s ↦ s
+  | rule10bSym -- true && s ↦ s
   | rule11 -- s ∧ False ↦ False
+  | rule11b -- s && false ↦ false
   | rule11Sym -- False ∧ s ↦ False
+  | rule11bSym -- false && s ↦ false
   | rule12 -- s ≠ s ↦ False
+  | rule12b -- s != s ↦ false
   | rule13 -- s = False ↦ ¬s
+  | rule13b -- s == false ↦ !s
   | rule13Sym -- False = s ↦ ¬s
+  | rule13bSym -- false == s ↦ !s
   | rule14 -- Not True ↦ False
+  | rule14b -- !true ↦ false
   | rule15 -- ¬¬s ↦ s
+  | rule15b -- !!s ↦ s
   | rule16 -- True → s ↦ s
   | rule17 -- False → s ↦ True
   | rule18 -- s → False ↦ ¬s
@@ -50,7 +74,9 @@ inductive BoolSimpRule
   | rule21 -- ¬s → s ↦ s
   | rule22 -- s → s ↦ True
   | rule23 -- ∀ p : Prop, f(p) ↦ f True ∧ f False
+  | rule23b -- ∀ b : Bool, f(b) ↦ f true ∧ f false (assuming `f : Bool → Prop`)
   | rule24 -- ∃ p : Prop, f(p) ↦ f True ∨ f False
+  | rule24b -- ∃ b : Bool, f(b) ↦ f true ∨ f false (assuming `f : Bool → Prop`)
   | rule25 -- (s1 → s2 → ... → sn → v) ↦ True if there exists i and j such that si = ¬sj
   | rule26 -- (s1 → s2 → ... → sn → v1 ∨ ... ∨ vm) ↦ True if there exists i and j such that si = vj
   | rule27 -- (s1 ∧ s2 ∧ ... ∧ sn → v1 ∨ ... ∨ vm) ↦ True if there exists i and j such that si = vj
@@ -62,28 +88,51 @@ open BoolSimpRule
 def BoolSimpRule.format (boolSimpRule : BoolSimpRule) : MessageData :=
   match boolSimpRule with
   | rule1 => m!"rule1"
+  | rule1b => m!"rule1b"
   | rule2 => m!"rule2"
+  | rule2b => m!"rule2b"
   | rule2Sym => m!"rule2Sym"
+  | rule2bSym => m!"rule2bSym"
   | rule3 => m!"rule3"
+  | rule3b => m!"rule3b"
   | rule3Sym => m!"rule3Sym"
+  | rule3bSym => m!"rule3bSym"
   | rule4 => m!"rule4"
+  | rule4b => m!"rule4b"
   | rule4Sym => m!"rule4Sym"
+  | rule4bSym => m!"rule4bSym"
   | rule5 => m!"rule5"
+  | rule5b => m!"rule5b"
   | rule6 => m!"rule6"
+  | rule6b => m!"rule6b"
   | rule6Sym => m!"rule6Sym"
+  | rule6bSym => m!"rule6bSym"
   | rule7 => m!"rule7"
+  | rule7b => m!"rule7b"
   | rule8 => m!"rule8"
+  | rule8b => m!"rule8b"
   | rule9 => m!"rule9"
+  | rule9b => m!"rule9b"
   | rule9Sym => m!"rule9Sym"
+  | rule9bSym => m!"rule9bSym"
   | rule10 => m!"rule10"
+  | rule10b => m!"rule10b"
   | rule10Sym => m!"rule10Sym"
+  | rule10bSym => m!"rule10bSym"
   | rule11 => m!"rule11"
+  | rule11b => m!"rule11b"
   | rule11Sym => m!"rule11Sym"
+  | rule11bSym => m!"rule11bSym"
   | rule12 => m!"rule12"
+  | rule12b => m!"rule12b"
   | rule13 => m!"rule13"
+  | rule13b => m!"rule13b"
   | rule13Sym => m!"rule13Sym"
+  | rule13bSym => m!"rule13bSym"
   | rule14 => m!"rule14"
+  | rule14b => m!"rule14b"
   | rule15 => m!"rule15"
+  | rule15b => m!"rule15b"
   | rule16 => m!"rule16"
   | rule17 => m!"rule17"
   | rule18 => m!"rule18"
@@ -92,7 +141,9 @@ def BoolSimpRule.format (boolSimpRule : BoolSimpRule) : MessageData :=
   | rule21 => m!"rule21"
   | rule22 => m!"rule22"
   | rule23 => m!"rule23"
+  | rule23b => m!"rule23b"
   | rule24 => m!"rule24"
+  | rule24b => m!"rule24b"
   | rule25 => m!"rule25"
   | rule26 => m!"rule26"
   | rule27 => m!"rule27"
@@ -101,6 +152,7 @@ def BoolSimpRule.format (boolSimpRule : BoolSimpRule) : MessageData :=
 instance : ToMessageData BoolSimpRule := ⟨BoolSimpRule.format⟩
 
 theorem rule1Theorem (p : Prop) : (p ∨ p) = p := by simp
+theorem rule1bTheorem (b : Bool) : (b || b) = b := by simp
 theorem rule2Theorem (p : Prop) : (¬p ∨ p) = True := by
   apply @Classical.byCases p
   . intro hp
@@ -109,32 +161,54 @@ theorem rule2Theorem (p : Prop) : (¬p ∨ p) = True := by
   . intro hnp
     apply eq_true
     exact Or.intro_left _ hnp
+theorem rule2bTheorem (b : Bool) : (!b || b) = true := by simp
 theorem rule2SymTheorem (p : Prop) : (p ∨ ¬p) = True := by
   by_cases h : p
   . apply eq_true
     exact Or.intro_left _ h
   . apply eq_true
     exact Or.intro_right _ h
+theorem rule2bSymTheorem (b : Bool) : (b || !b) = true := by simp
 theorem rule3Theorem (p : Prop) : (p ∨ True) = True := by simp
+theorem rule3bTheorem (b : Bool) : (b || true) = true := by simp
 theorem rule3SymTheorem (p : Prop) : (True ∨ p) = True := by simp
+theorem rule3bSymTheorem (b : Bool) : (true || b) = true := by simp
 theorem rule4Theorem (p : Prop) : (p ∨ False) = p := by simp
+theorem rule4bTheorem (b : Bool) : (b || false) = b := by simp
 theorem rule4SymTheorem (p : Prop) : (False ∨ p) = p := by simp
+theorem rule4bSymTheorem (b : Bool) : (false || b) = b := by simp
 theorem rule5Theorem (p : α) : (p = p) = True := by simp
+theorem rule5bTheorem (b : Bool) : (b == b) = true := by simp
 theorem rule6Theorem (p : Prop) : (p = True) = p := by simp
+theorem rule6bTheorem (b : Bool) : (b == true) = b := by simp
 theorem rule6SymTheorem (p : Prop) : (True = p) = p := by simp
+theorem rule6bSymTheorem (b : Bool) : (true == b) = b := by simp
 theorem rule7Theorem : Not False = True := by simp
+theorem rule7bTheorem : (!false) = true := by simp
 theorem rule8Theorem (p : Prop) : (p ∧ p) = p := by simp
+theorem rule8bTheorem (b : Bool) : (b && b) = b := by simp
 theorem rule9Theorem (p : Prop) : (¬p ∧ p) = False := by simp
+theorem rule9bTheorem (b : Bool) : (!b && b) = false := by simp
 theorem rule9SymTheorem (p : Prop) : (p ∧ ¬p) = False := by simp
+theorem rule9bSymTheorem (b : Bool) : (b && !b) = false := by simp
 theorem rule10Theorem (p : Prop) : (p ∧ True) = p := by simp
+theorem rule10bTheorem (b : Bool) : (b && true) = b := by simp
 theorem rule10SymTheorem (p : Prop) : (True ∧ p) = p := by simp
+theorem rule10bSymTheorem (b : Bool) : (true && b) = b := by simp
 theorem rule11Theorem (p : Prop) : (p ∧ False) = False := by simp
+theorem rule11bTheorem (b : Bool) : (b && false) = false := by simp
 theorem rule11SymTheorem (p : Prop) : (False ∧ p) = False := by simp
+theorem rule11bSymTheorem (b : Bool) : (false && b) = false := by simp
 theorem rule12Theorem (p : α) : (p ≠ p) = False := by simp
+theorem rule12bTheorem (b : Bool) : (b != b) = false := by simp
 theorem rule13Theorem (p : Prop) : (p = False) = ¬p := by simp
+theorem rule13bTheorem (b : Bool) : (b == false) = !b := by simp
 theorem rule13SymTheorem (p : Prop) : (False = p) = ¬p := by simp
+theorem rule13bSymTheorem (b : Bool) : (false == b) = !b := by simp
 theorem rule14Theorem : Not True = False := by simp
+theorem rule14bTheorem : (!true) = false := by simp
 theorem rule15Theorem (p : Prop) : (¬¬p) = p := by rw [Classical.not_not]
+theorem rule15bTheorem (b : Bool) : (!!b) = b := by simp
 theorem rule16Theorem (p : Prop) : (True → p) = p := by simp
 theorem rule17Theorem (p : Prop) : (False → p) = True := by simp
 theorem rule18Theorem (p : Prop) : (p → False) = ¬p := by rfl
@@ -167,6 +241,27 @@ theorem rule23Theorem (f : Prop → Prop) : (∀ p : Prop, f p) = (f True ∧ f
       . rw [eq_false hp]
         exact h2.2
     exact h h3
+theorem rule23bTheorem (f : Bool → Prop) : (∀ b : Bool, f b) = (f true ∧ f false) := by
+  by_cases h : ∀ b : Bool, f b
+  . rw [eq_true h]
+    apply Eq.symm
+    apply eq_true
+    constructor
+    . exact h True
+    . exact h False
+  . rw [eq_false h]
+    apply Eq.symm
+    apply eq_false
+    intro h2
+    have h3 : (∀ b : Bool, f b) := by
+      intro b
+      by_cases hb : b
+      . rw [hb]
+        exact h2.1
+      . rw [Bool.not_eq_true] at hb
+        rw [hb]
+        exact h2.2
+    exact h h3
 theorem rule24Theorem (f : Prop → Prop) : (∃ p : Prop, f p) = (f True ∨ f False) := by
   by_cases h : ∃ p : Prop, f p
   . rw [eq_true h]
@@ -192,6 +287,27 @@ theorem rule24Theorem (f : Prop → Prop) : (∃ p : Prop, f p) = (f True ∨ f
     | inr f_false =>
       have h2 : ∃ p : Prop, f p := Exists.intro False f_false
       exact h h2
+theorem rule24bTheorem (f : Bool → Prop) : (∃ b : Bool, f b) = (f true ∨ f false) := by
+  by_cases h : ∃ b : Bool, f b
+  . rw [eq_true h]
+    apply Eq.symm
+    apply eq_true
+    cases h with
+    | intro b h =>
+      by_cases hb : b
+      . rw [hb] at h
+        exact Or.inl h
+      . simp only [Bool.not_eq_true] at hb
+        rw [hb] at h
+        exact Or.inr h
+  . rw [eq_false h]
+    apply Eq.symm
+    apply eq_false
+    intro h2
+    simp only [not_exists] at h
+    cases h2 with
+    | inl f_true => exact h true f_true
+    | inr f_false => exact h false f_false
 theorem rule28Theorem (p1 : Prop) (p2 : Prop) : (p1 ↔ p2) = (p1 = p2) := by simp
 
 partial def mkRule25Theorem (e : Expr) (counter : Nat) (i : Nat) (j : Nat) : MetaM Expr := do
@@ -241,6 +357,14 @@ def applyRule1 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s || s ↦ s -/
+def applyRule1b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``or _) e1) e2 =>
+    if e1 == e2 then some e1
+    else none
+  | _ => none
+
 /-- ¬s ∨ s ↦ True -/
 def applyRule2 (e : Expr) : Option Expr :=
   match e with
@@ -249,6 +373,14 @@ def applyRule2 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- !s || s ↦ true -/
+def applyRule2b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``or _) e1) e2 =>
+    if e1 == Expr.app (Expr.const ``not []) e2 then some (mkConst ``true)
+    else none
+  | _ => none
+
 /-- s ∨ ¬s ↦ True -/
 def applyRule2Sym (e : Expr) : Option Expr :=
   match e with
@@ -257,6 +389,14 @@ def applyRule2Sym (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s || !s ↦ true -/
+def applyRule2bSym (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``or _) e1) e2 =>
+    if e2 == Expr.app (Expr.const ``not []) e1 then some (mkConst ``true)
+    else none
+  | _ => none
+
 /-- s ∨ True ↦ True -/
 def applyRule3 (e : Expr) : Option Expr :=
   match e with
@@ -265,6 +405,14 @@ def applyRule3 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s || true ↦ true -/
+def applyRule3b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``or _) _) e2 =>
+    if e2 == mkConst ``true then some (mkConst ``true)
+    else none
+  | _ => none
+
 /-- True ∨ s ↦ True -/
 def applyRule3Sym (e : Expr) : Option Expr :=
   match e with
@@ -273,6 +421,14 @@ def applyRule3Sym (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- true || s ↦ true -/
+def applyRule3bSym (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``or _) e1) _ =>
+    if e1 == mkConst ``true then some (mkConst ``true)
+    else none
+  | _ => none
+
 /-- s ∨ False ↦ s -/
 def applyRule4 (e : Expr) : Option Expr :=
   match e with
@@ -281,6 +437,15 @@ def applyRule4 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s || false ↦ s -/
+def applyRule4b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``or _) e1) e2 =>
+    if e2 == mkConst ``false then
+      some e1
+    else none
+  | _ => none
+
 /-- False ∨ s ↦ s -/
 def applyRule4Sym (e : Expr) : Option Expr :=
   match e with
@@ -289,6 +454,14 @@ def applyRule4Sym (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- false || s ↦ s -/
+def applyRule4bSym (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``or _) e1) e2 =>
+    if e1 == mkConst ``false then some e2
+    else none
+  | _ => none
+
 /-- s = s ↦ True -/
 def applyRule5 (e : Expr) : Option Expr :=
   match e with
@@ -297,6 +470,14 @@ def applyRule5 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s == s ↦ true -/
+def applyRule5b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) e1) e2 =>
+    if e1 == e2 then some (mkConst ``true)
+    else none
+  | _ => none
+
 /-- s = True ↦ s -/
 def applyRule6 (e : Expr) : Option Expr :=
   match e with
@@ -305,6 +486,14 @@ def applyRule6 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s == true ↦ s -/
+def applyRule6b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) e1) e2 =>
+    if e2 == mkConst ``true then some e1
+    else none
+  | _ => none
+
 /-- True = s ↦ s -/
 def applyRule6Sym (e : Expr) : Option Expr :=
   match e with
@@ -313,12 +502,26 @@ def applyRule6Sym (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- true == s ↦ s -/
+def applyRule6bSym (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) e1) e2 =>
+    if e1 == mkConst ``true then some e2
+    else none
+  | _ => none
+
 /-- Not False ↦ True -/
 def applyRule7 (e : Expr) : Option Expr :=
   match e with
   | Expr.app (Expr.const ``Not _) (Expr.const ``False _) => some (mkConst ``True)
   | _ => none
 
+/-- !false ↦ True -/
+def applyRule7b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.const ``not _) (Expr.const ``false _) => some (mkConst ``true)
+  | _ => none
+
 /-- s ∧ s ↦ s -/
 def applyRule8 (e : Expr) : Option Expr :=
   match e with
@@ -327,6 +530,14 @@ def applyRule8 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s && s ↦ s -/
+def applyRule8b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``and _) e1) e2 =>
+    if e1 == e2 then some e1
+    else none
+  | _ => none
+
 /-- ¬s ∧ s ↦ False -/
 def applyRule9 (e : Expr) : Option Expr :=
   match e with
@@ -335,6 +546,14 @@ def applyRule9 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- !s && s ↦ false -/
+def applyRule9b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``and _) e1) e2 =>
+    if e1 == Expr.app (Expr.const ``not []) e2 then some (mkConst ``false)
+    else none
+  | _ => none
+
 /-- s ∧ ¬s ↦ False -/
 def applyRule9Sym (e : Expr) : Option Expr :=
   match e with
@@ -343,6 +562,14 @@ def applyRule9Sym (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s && !s ↦ false -/
+def applyRule9bSym (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``and _) e1) e2 =>
+    if e2 == Expr.app (Expr.const ``not []) e1 then some (mkConst ``false)
+    else none
+  | _ => none
+
 /-- s ∧ True ↦ s -/
 def applyRule10 (e : Expr) : Option Expr :=
   match e with
@@ -351,6 +578,14 @@ def applyRule10 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s && true ↦ s -/
+def applyRule10b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``and _) e1) e2 =>
+    if e2 == mkConst ``true then some e1
+    else none
+  | _ => none
+
 /-- True ∧ s ↦ s -/
 def applyRule10Sym (e : Expr) : Option Expr :=
   match e with
@@ -359,6 +594,14 @@ def applyRule10Sym (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- true && s ↦ s -/
+def applyRule10bSym (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``and _) e1) e2 =>
+    if e1 == mkConst ``true then some e2
+    else none
+  | _ => none
+
 /-- s ∧ False ↦ False -/
 def applyRule11 (e : Expr) : Option Expr :=
   match e with
@@ -367,6 +610,14 @@ def applyRule11 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s && false ↦ false -/
+def applyRule11b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``and _) _) e2 =>
+    if e2 == mkConst ``false then some (mkConst ``false)
+    else none
+  | _ => none
+
 /-- False ∧ s ↦ False -/
 def applyRule11Sym (e : Expr) : Option Expr :=
   match e with
@@ -375,6 +626,14 @@ def applyRule11Sym (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- false && s ↦ false -/
+def applyRule11bSym (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.const ``and _) e1) _ =>
+    if e1 == mkConst ``false then some (mkConst ``false)
+    else none
+  | _ => none
+
 /-- s ≠ s ↦ False -/
 def applyRule12 (e : Expr) : Option Expr :=
   match e with
@@ -383,6 +642,14 @@ def applyRule12 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s != s ↦ False -/
+def applyRule12b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``bne _) _) _) e1) e2 =>
+    if e1 == e2 then some (mkConst ``false)
+    else none
+  | _ => none
+
 /-- s = False ↦ ¬s -/
 def applyRule13 (e : Expr) : Option Expr :=
   match e with
@@ -391,6 +658,14 @@ def applyRule13 (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- s == false ↦ !s -/
+def applyRule13b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) e1) e2 =>
+    if e2 == mkConst ``false then some (mkApp (mkConst ``not) e1)
+    else none
+  | _ => none
+
 /-- False = s ↦ ¬s -/
 def applyRule13Sym (e : Expr) : Option Expr :=
   match e with
@@ -399,18 +674,38 @@ def applyRule13Sym (e : Expr) : Option Expr :=
     else none
   | _ => none
 
+/-- false == s ↦ !s -/
+def applyRule13bSym (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) e1) e2 =>
+    if e1 == mkConst ``false then some (mkApp (mkConst ``not) e2)
+    else none
+  | _ => none
+
 /-- Not True ↦ False -/
 def applyRule14 (e : Expr) : Option Expr :=
   match e with
   | Expr.app (Expr.const ``Not _) (Expr.const ``True _) => some (mkConst ``False)
   | _ => none
 
+/-- !true ↦ false -/
+def applyRule14b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.const ``not _) (Expr.const ``true _) => some (mkConst ``false)
+  | _ => none
+
 /-- ¬¬s ↦ s -/
 def applyRule15 (e : Expr) : Option Expr :=
   match e with
   | Expr.app (Expr.const ``Not _) (Expr.app (Expr.const ``Not _) e') => some e'
   | _ => none
 
+/-- !!s ↦ s -/
+def applyRule15b (e : Expr) : Option Expr :=
+  match e with
+  | Expr.app (Expr.const ``not _) (Expr.app (Expr.const ``not _) e') => some e'
+  | _ => none
+
 /-- True → s ↦ s -/
 def applyRule16 (e : Expr) : Option Expr :=
   match e with
@@ -478,6 +773,17 @@ def applyRule23 (e : Expr) : RuleM (Option Expr) := do
     else return none
   | _ => return none
 
+/-- ∀ b : Bool, f(b) ↦ f true ∧ f false (assuming `f : Bool → Prop`) -/
+def applyRule23b (e : Expr) : RuleM (Option Expr) := do
+  match e with
+  | Expr.forallE _ t b _ =>
+    if t == (mkConst ``Bool) && (← inferType e).isProp then
+      let btrue := b.instantiate1 (mkConst ``true)
+      let bfalse := b.instantiate1 (mkConst ``false)
+      mkAppM ``And #[btrue, bfalse]
+    else return none
+  | _ => return none
+
 /-- ∃ p : Prop, f(p) ↦ f True ∨ f False -/
 def applyRule24 (e : Expr) : RuleM (Option Expr) := do
   match e with
@@ -489,6 +795,17 @@ def applyRule24 (e : Expr) : RuleM (Option Expr) := do
     else return none
   | _ => return none
 
+/-- ∃ b : Bool, f(b) ↦ f true ∨ f false (assuming `f : Bool → Prop`) -/
+def applyRule24b (e : Expr) : RuleM (Option Expr) := do
+  match e with
+  | Expr.app (Expr.app (Expr.const ``Exists _) t) b =>
+    if t == (mkConst ``Bool) then
+      let btrue ← whnf $ mkApp b (mkConst ``true)
+      let bfalse ← whnf $ mkApp b (mkConst ``false)
+      mkAppM ``Or #[btrue, bfalse]
+    else return none
+  | _ => return none
+
 partial def applyRule25Helper (e : Expr) (hyps : Array Expr) : RuleM (Option (Nat × Nat)) := do
   match e.consumeMData with
   | Expr.forallE _ t b _ =>
@@ -565,94 +882,186 @@ def getBoolSimpRuleTheorem (boolSimpRule : BoolSimpRule) (originalExp : Expr) (i
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``Or _) e1) _ => return mkApp (mkConst ``rule1Theorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule1"
+  | rule1b => -- s || s ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``or _) e1) _ => return mkApp (mkConst ``rule1bTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule1b"
   | rule2 => -- ¬s ∨ s ↦ True
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``Or _) _) e2 => return mkApp (mkConst ``rule2Theorem) e2
     | _ => throwError "Invalid originalExp {originalExp} for rule2"
+  | rule2b => -- !s || s ↦ true
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``or _) _) e2 => return mkApp (mkConst ``rule2bTheorem) e2
+    | _ => throwError "Invalid originalExp {originalExp} for rule2b"
   | rule2Sym => -- s ∨ ¬s ↦ True
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``Or _) e1) _ => return mkApp (mkConst ``rule2SymTheorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule2Sym"
+  | rule2bSym => -- s || !s ↦ true
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``or _) e1) _ => return mkApp (mkConst ``rule2bSymTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule2bSym"
   | rule3 => -- s ∨ True ↦ True
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``Or _) e1) _ => return mkApp (mkConst ``rule3Theorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule3"
+  | rule3b => -- s || true ↦ true
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``or _) e1) _ => return mkApp (mkConst ``rule3bTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule3b"
   | rule3Sym => -- True ∨ s ↦ True
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``Or _) _) e2 => return mkApp (mkConst ``rule3SymTheorem) e2
     | _ => throwError "Invalid originalExp {originalExp} for rule3Sym"
+  | rule3bSym => -- true || s ↦ true
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``or _) _) e2 => return mkApp (mkConst ``rule3bSymTheorem) e2
+    | _ => throwError "Invalid originalExp {originalExp} for rule3bSym"
   | rule4 => -- s ∨ False ↦ s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``Or _) e1) _ => return mkApp (mkConst ``rule4Theorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule4"
+  | rule4b => -- s || false ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``or _) e1) _ => return mkApp (mkConst ``rule4bTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule4b"
   | rule4Sym => -- False ∨ s ↦ s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``Or _) _) e2 => return mkApp (mkConst ``rule4SymTheorem) e2
     | _ => throwError "Invalid originalExp {originalExp} for rule4Sym"
+  | rule4bSym => -- false || s ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``or _) _) e2 => return mkApp (mkConst ``rule4bSymTheorem) e2
+    | _ => throwError "Invalid originalExp {originalExp} for rule4bSym"
   | rule5 => -- s = s ↦ True
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.app (Expr.const ``Eq _) _) e1) _ => Meta.mkAppM ``rule5Theorem #[e1]
     | _ => throwError "Invalid originalExp {originalExp} for rule5"
+  | rule5b => -- s == s ↦ true
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) e1) _ => Meta.mkAppM ``rule5bTheorem #[e1]
+    | _ => throwError "Invalid originalExp {originalExp} for rule5b"
   | rule6 => -- s = True ↦ s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.app (Expr.const ``Eq _) _) e1) _ => return mkApp (mkConst ``rule6Theorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule6"
+  | rule6b => -- s == true ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) e1) _ => return mkApp (mkConst ``rule6bTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule6b"
   | rule6Sym => -- True = s ↦ s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.app (Expr.const ``Eq _) _) _) e2 => return mkApp (mkConst ``rule6SymTheorem) e2
     | _ => throwError "Invalid originalExp {originalExp} for rule6Sym"
+  | rule6bSym => -- true == s ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) _) e2 => return mkApp (mkConst ``rule6bSymTheorem) e2
+    | _ => throwError "Invalid originalExp {originalExp} for rule6bSym"
   | rule7 => -- Not False ↦ True
     match originalExp.consumeMData with
     | Expr.app (Expr.const ``Not _) (Expr.const ``False _) => return mkConst ``rule7Theorem
     | _ => throwError "Invalid originalExp {originalExp} for rule7"
+  | rule7b => -- !false ↦ true
+    match originalExp.consumeMData with
+    | Expr.app (Expr.const ``not _) (Expr.const ``false _) => return mkConst ``rule7bTheorem
+    | _ => throwError "Invalid originalExp {originalExp} for rule7b"
   | rule8 => -- s ∧ s ↦ s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``And _) e1) _ => return mkApp (mkConst ``rule8Theorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule8"
+  | rule8b => -- s && s ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``and _) e1) _ => return mkApp (mkConst ``rule8bTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule8b"
   | rule9 => -- ¬s ∧ s ↦ False
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``And _) _) e2 => return mkApp (mkConst ``rule9Theorem) e2
     | _ => throwError "Invalid originalExp {originalExp} for rule9"
+  | rule9b => -- !s && s ↦ false
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``and _) _) e2 => return mkApp (mkConst ``rule9bTheorem) e2
+    | _ => throwError "Invalid originalExp {originalExp} for rule9b"
   | rule9Sym => -- s ∧ ¬s ↦ False
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``And _) e1) _ => return mkApp (mkConst ``rule9SymTheorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule9Sym"
+  | rule9bSym => -- s && !s ↦ false
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``and _) e1) _ => return mkApp (mkConst ``rule9bSymTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule9bSym"
   | rule10 => -- s ∧ True ↦ s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``And _) e1) _ => return mkApp (mkConst ``rule10Theorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule10"
+  | rule10b => -- s && true ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``and _) e1) _ => return mkApp (mkConst ``rule10bTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule10b"
   | rule10Sym => -- True ∧ s ↦ s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``And _) _) e2 => return mkApp (mkConst ``rule10SymTheorem) e2
     | _ => throwError "Invalid originalExp {originalExp} for rule10Sym"
+  | rule10bSym => -- true && s ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``and _) _) e2 => return mkApp (mkConst ``rule10bSymTheorem) e2
+    | _ => throwError "Invalid originalExp {originalExp} for rule10bSym"
   | rule11 => -- s ∧ False ↦ False
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``And _) e1) _ => return mkApp (mkConst ``rule11Theorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule11"
+  | rule11b => -- s && false ↦ false
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``and _) e1) _ => return mkApp (mkConst ``rule11bTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule11b"
   | rule11Sym => -- False ∧ s ↦ False
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``And _) _) e2 => return mkApp (mkConst ``rule11SymTheorem) e2
     | _ => throwError "Invalid originalExp {originalExp} for rule11Sym"
+  | rule11bSym => -- false && s ↦ false
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``and _) _) e2 => return mkApp (mkConst ``rule11bSymTheorem) e2
+    | _ => throwError "Invalid originalExp {originalExp} for rule11bSym"
   | rule12 => -- s ≠ s ↦ False
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.app (Expr.const ``Ne _) _) e1) _ => Meta.mkAppM ``rule12Theorem #[e1]
     | _ => throwError "Invalid originalExp {originalExp} for rule12"
+  | rule12b => -- s != s ↦ false
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``bne _) _) _) e1) _ => Meta.mkAppM ``rule12bTheorem #[e1]
+    | _ => throwError "Invalid originalExp {originalExp} for rule12b"
   | rule13 => -- s = False ↦ ¬s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.app (Expr.const ``Eq _) _) e1) _ => return mkApp (mkConst ``rule13Theorem) e1
     | _ => throwError "Invalid originalExp {originalExp} for rule13"
+  | rule13b => -- s == false ↦ !s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) e1) _ => return mkApp (mkConst ``rule13bTheorem) e1
+    | _ => throwError "Invalid originalExp {originalExp} for rule13b"
   | rule13Sym => -- False = s ↦ ¬s
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.app (Expr.const ``Eq _) _) _) e2 => return mkApp (mkConst ``rule13SymTheorem) e2
     | _ => throwError "Invalid originalExp {originalExp} for rule13Sym"
+  | rule13bSym => -- false == s ↦ !s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.app (Expr.app (Expr.const ``BEq.beq _) _) _) _) e2 => return mkApp (mkConst ``rule13bSymTheorem) e2
+    | _ => throwError "Invalid originalExp {originalExp} for rule13bSym"
   | rule14 => -- Not True ↦ False
     match originalExp.consumeMData with
     | Expr.app (Expr.const ``Not _) (Expr.const ``True _) => return mkConst ``rule14Theorem
     | _ => throwError "Invalid originalExp {originalExp} for rule14"
+  | rule14b => -- !true ↦ false
+    match originalExp.consumeMData with
+    | Expr.app (Expr.const ``not _) (Expr.const ``true _) => return mkConst ``rule14bTheorem
+    | _ => throwError "Invalid originalExp {originalExp} for rule14b"
   | rule15 => -- ¬¬s ↦ s
     match originalExp.consumeMData with
     | Expr.app (Expr.const ``Not _) (Expr.app (Expr.const ``Not _) e') => return mkApp (mkConst ``rule15Theorem) e'
     | _ => throwError "Invalid originalExp {originalExp} for rule15"
+  | rule15b => -- !!s ↦ s
+    match originalExp.consumeMData with
+    | Expr.app (Expr.const ``not _) (Expr.app (Expr.const ``not _) e') => return mkApp (mkConst ``rule15bTheorem) e'
+    | _ => throwError "Invalid originalExp {originalExp} for rule15b"
   | rule16 => -- True → s ↦ s
     match originalExp.consumeMData with
     | Expr.forallE _ _ b _ => return mkApp (mkConst ``rule16Theorem) b
@@ -687,10 +1096,20 @@ def getBoolSimpRuleTheorem (boolSimpRule : BoolSimpRule) (originalExp : Expr) (i
       let bFunction := Expr.lam n (mkSort levelZero) b BinderInfo.default
       return mkApp (mkConst ``rule23Theorem) bFunction
     | _ => throwError "Invalid originalExp {originalExp} for rule23"
+  | rule23b => -- ∀ b : Bool, f(b) ↦ f true ∧ f false (assuming `f : Bool → Prop`)
+    match originalExp.consumeMData with
+    | Expr.forallE n _ b _ => do
+      let bFunction := Expr.lam n (mkConst ``Bool) b BinderInfo.default
+      return mkApp (mkConst ``rule23bTheorem) bFunction
+    | _ => throwError "Invalid originalExp {originalExp} for rule23b"
   | rule24 => -- ∃ p : Prop, f(p) ↦ f True ∨ f False
     match originalExp.consumeMData with
     | Expr.app (Expr.app (Expr.const ``Exists _) t) b => return mkApp (mkConst ``rule24Theorem) b
     | _ => throwError "Invalid originalExp {originalExp} for rule24"
+  | rule24b => -- ∃ b : Bool, f(b) ↦ f true ∨ f false (assuming `f : Bool → Prop`)
+    match originalExp.consumeMData with
+    | Expr.app (Expr.app (Expr.const ``Exists _) t) b => return mkApp (mkConst ``rule24bTheorem) b
+    | _ => throwError "Invalid originalExp {originalExp} for rule24b"
   | rule25 => -- (s1 → s2 → ... → sn → v) ↦ True if there exists i and j such that si = ¬sj
     match ijOpt with
     | some (i, j) => do Meta.mkAppM ``eq_true #[← mkRule25Theorem originalExp 0 i j]
@@ -708,6 +1127,14 @@ def getBoolSimpRuleTheorem (boolSimpRule : BoolSimpRule) (originalExp : Expr) (i
     | Expr.app (Expr.app (Expr.const ``Iff _) e1) e2 => return mkApp2 (mkConst ``rule28Theorem) e1 e2
     | _ => throwError "Invalid originalExpr {originalExp} for rule28"
 
+/-- Some boolSimpRules (those with `b` suffixes) operates on `Bool` rather than `Prop`. `mkBoolSimpProp` needs to know whether
+    `boolSimpRule` is one such rule in order to pass the correct type into `congrArg` -/
+def boolSimpRuleOperatesOnBool (boolSimpRule : BoolSimpRule) : Bool :=
+  match boolSimpRule with
+  | rule1b | rule2b | rule2bSym | rule3b | rule3bSym | rule4b | rule4bSym | rule5b | rule6b | rule6bSym | rule7b | rule8b
+  | rule9b | rule9bSym | rule10b | rule10bSym | rule11b | rule11bSym | rule12b | rule13b | rule13bSym | rule14b | rule15b => true
+  | _ => false -- `rule23b` and `rule24b` yield false because technically they take `Prop`s as input
+
 def mkBoolSimpProof (substPos : ClausePos) (boolSimpRule : BoolSimpRule) (ijOpt : Option (Nat × Nat)) (premises : List Expr)
   (parents : List ProofParent) (transferExprs : Array Expr) (c : Clause) : MetaM Expr :=
   Meta.forallTelescope c.toForallExpr fun xs body => do
@@ -726,7 +1153,9 @@ def mkBoolSimpProof (substPos : ClausePos) (boolSimpRule : BoolSimpRule) (ijOpt
 
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam :=
+            if boolSimpRuleOperatesOnBool boolSimpRule then mkLambda `x BinderInfo.default (mkConst ``Bool) abstrExp
+            else mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
           let rwproof ← Meta.mkAppM ``Eq.mp #[← Meta.mkAppM ``congrArg #[abstrLam, boolSimpRuleThm], h]
           Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i $ rwproof
         else
@@ -738,28 +1167,51 @@ def mkBoolSimpProof (substPos : ClausePos) (boolSimpRule : BoolSimpRule) (ijOpt
 /-- The list of rules that do not require the RuleM monad -/
 def applyRulesList1 : List ((Expr → (Option Expr)) × BoolSimpRule) := [
   (applyRule1, rule1),
+  (applyRule1b, rule1b),
   (applyRule2, rule2),
+  (applyRule2b, rule2b),
   (applyRule2Sym, rule2Sym),
+  (applyRule2bSym, rule2bSym),
   (applyRule3, rule3),
+  (applyRule3b, rule3b),
   (applyRule3Sym, rule3Sym),
+  (applyRule3bSym, rule3bSym),
   (applyRule4, rule4),
+  (applyRule4b, rule4b),
   (applyRule4Sym, rule4Sym),
+  (applyRule4bSym, rule4bSym),
   (applyRule5, rule5),
+  (applyRule5b, rule5b),
   (applyRule6, rule6),
+  (applyRule6b, rule6b),
   (applyRule6Sym, rule6Sym),
+  (applyRule6bSym, rule6bSym),
   (applyRule7, rule7),
+  (applyRule7b, rule7b),
   (applyRule8, rule8),
+  (applyRule8b, rule8b),
   (applyRule9, rule9),
+  (applyRule9b, rule9b),
   (applyRule9Sym, rule9Sym),
+  (applyRule9bSym, rule9bSym),
   (applyRule10, rule10),
+  (applyRule10b, rule10b),
   (applyRule10Sym, rule10Sym),
+  (applyRule10bSym, rule10bSym),
   (applyRule11, rule11),
+  (applyRule11b, rule11b),
   (applyRule11Sym, rule11Sym),
+  (applyRule11bSym, rule11bSym),
   (applyRule12, rule12),
+  (applyRule12b, rule12b),
   (applyRule13, rule13),
+  (applyRule13b, rule13b),
   (applyRule13Sym, rule13Sym),
+  (applyRule13bSym, rule13bSym),
   (applyRule14, rule14),
+  (applyRule14b, rule14b),
   (applyRule15, rule15),
+  (applyRule15b, rule15b),
   (applyRule16, rule16),
   (applyRule17, rule17),
   (applyRule19, rule19),
@@ -773,7 +1225,9 @@ def applyRulesList2 : List ((Expr → RuleM (Option Expr)) × BoolSimpRule) := [
   (applyRule18, rule18),
   (applyRule22, rule22),
   (applyRule23, rule23),
-  (applyRule24, rule24)
+  (applyRule23b, rule23b),
+  (applyRule24, rule24),
+  (applyRule24b, rule24b)
 ]
 
 /-- The list of rules for which indices must be returned -/
diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean
index b05d51a..50da552 100644
--- a/Duper/Tactic.lean
+++ b/Duper/Tactic.lean
@@ -1,13 +1,9 @@
 import Lean
 import Duper.Interface
 
-open Lean
-open Lean.Meta
-open Duper
-open ProverM
-open Lean.Parser
+open Lean Meta Duper ProverM Parser Elab Tactic
 
-namespace Lean.Elab.Tactic
+namespace Duper
 
 register_option duper.printTimeInformation : Bool := {
   defValue := false
@@ -67,6 +63,7 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
         let facts ← addRecAsFact val
         let facts ← facts.mapM fun (fact, proof, paramNames) => do
           return (← instantiateMVars fact, ← instantiateMVars proof, paramNames)
+        trace[duper.elabFact.debug] "Adding recursor {expr} as the following facts: {facts.map (fun x => x.1)}"
         return facts.toArray
       | some (.defnInfo defval) =>
         let term := defval.value
@@ -79,6 +76,7 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
         -- Generate definitional equation for the fact
         if let some eqns ← getEqnsFor? exprConstName (nonRec := true) then
           ret := ret.append (← eqns.mapM fun eq => do elabFactAux (← `($(mkIdent eq))))
+        trace[duper.elabFact.debug] "Adding definition {expr} as the following facts: {ret.map (fun x => x.1)}"
         return ret
       | some (.axiomInfo _)  => return #[← elabFactAux stx]
       | some (.thmInfo _)    => return #[← elabFactAux stx]
@@ -104,7 +102,14 @@ where elabFactAux (stx : Term) : TacticM (Expr × Expr × Array Name) :=
     let paramNames := abstres.paramNames
     return (← inferType e, e, paramNames)
 
-def collectAssumptions (facts : Array Term) (withAllLCtx : Bool) (goalDecls : Array LocalDecl) : TacticM (List (Expr × Expr × Array Name × Bool)) := do
+/-- Formulas in Duper are represented as a tuple containing the following:
+    - The fact that Duper can use
+    - A proof that said fact is true (if the fact is `p` then second argument of the tuple is a proof of `p = True`)
+    - An array of universe level parameter names
+    - A boolean indicating whether the fact came from the original target
+    - If the fact is a user-provided non-lctx fact, then the Term that was used to indicate said fact -/
+def collectAssumptions (facts : Array Term) (withAllLCtx : Bool) (goalDecls : Array LocalDecl)
+  : TacticM (List (Expr × Expr × Array Name × Bool × Option Term)) := do
   let mut formulas := []
   if withAllLCtx then -- Load all local decls
     for fVarId in (← getLCtx).getFVarIds do
@@ -112,18 +117,18 @@ def collectAssumptions (facts : Array Term) (withAllLCtx : Bool) (goalDecls : Ar
       unless ldecl.isAuxDecl ∨ not (← instantiateMVars (← inferType ldecl.type)).isProp do
         let ldecltype ← preprocessFact (← instantiateMVars ldecl.type)
         let isFromGoal := goalDecls.any (fun goalDecl => goalDecl.index = ldecl.index)
-        formulas := (ldecltype, ← mkAppM ``eq_true #[mkFVar fVarId], #[], isFromGoal) :: formulas
+        formulas := (ldecltype, ← mkAppM ``eq_true #[mkFVar fVarId], #[], isFromGoal, none) :: formulas
   else -- Even if withAllLCtx is false, we still need to load the goal decls
     for ldecl in goalDecls do
       unless ldecl.isAuxDecl ∨ not (← instantiateMVars (← inferType ldecl.type)).isProp do
         let ldecltype ← preprocessFact (← instantiateMVars ldecl.type)
-        formulas := (ldecltype, ← mkAppM ``eq_true #[mkFVar ldecl.fvarId], #[], true) :: formulas
+        formulas := (ldecltype, ← mkAppM ``eq_true #[mkFVar ldecl.fvarId], #[], true, none) :: formulas
   -- Load user-provided facts
   for factStx in facts do
     for (fact, proof, params) in ← elabFact factStx do
       if ← isProp fact then
         let fact ← preprocessFact (← instantiateMVars fact)
-        formulas := (fact, ← mkAppM ``eq_true #[proof], params, false) :: formulas
+        formulas := (fact, ← mkAppM ``eq_true #[proof], params, false, some factStx) :: formulas
       else
         throwError "Invalid fact {factStx} for duper. Proposition expected"
   return formulas
@@ -141,7 +146,7 @@ macro_rules
 /-- Given a Syntax.TSepArray of facts provided by the user (which may include `*` to indicate that duper should read in the
     full local context) `removeDuperStar` returns the Syntax.TSepArray with `*` removed and a boolean that indicates whether `*`
     was included in the original input. -/
-def removeDuperStar (facts : Syntax.TSepArray [`duperStar, `term] ",") : Bool × Syntax.TSepArray `term "," := Id.run do
+def removeDuperStar (facts : Syntax.TSepArray [`Duper.duperStar, `term] ",") : Bool × Syntax.TSepArray `term "," := Id.run do
   let factsArr := facts.elemsAndSeps -- factsArr contains both the elements of facts and separators, ordered like `#[e1, s1, e2, s2, e3]`
   let mut newFactsArr : Array Syntax := #[]
   let mut removedDuperStar := false
@@ -433,9 +438,11 @@ def evalDuperNoTiming : Tactic
   withMainContext do
     let (_, facts) := removeDuperStar facts
     let formulas ← collectAssumptions facts true  #[] -- I don't bother computing goalDecls here since I set withAllLCtx to true anyway
+    -- Remove syntax option from `formulas` since we are not converting to Auto.Lemmas
+    let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2.1))
     let proof ← runDuper formulas 0
     Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal
     IO.println s!"Constructed proof"
 | _ => throwUnsupportedSyntax
 
-end Lean.Elab.Tactic
+end Duper
diff --git a/Duper/Tests/temp.lean b/Duper/Tests/temp.lean
new file mode 100644
index 0000000..bd2be0a
--- /dev/null
+++ b/Duper/Tests/temp.lean
@@ -0,0 +1,44 @@
+import Duper
+import Duper.TPTP
+
+set_option auto.tptp true
+set_option auto.tptp.premiseSelection true
+set_option auto.tptp.solver.name "zipperposition"
+set_option trace.auto.tptp.result true
+set_option trace.auto.tptp.printQuery true
+set_option auto.native true
+
+open Lean Auto
+
+@[rebind Auto.Native.solverFunc]
+def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
+  let formulas ← Duper.autoLemmasToFormulas lemmas
+  Duper.runDuperPortfolioMode formulas .none
+    { portfolioMode := true,
+      portfolioInstance := none,
+      inhabitationReasoning := none,
+      preprocessing := Duper.PreprocessingOption.NoPreprocessing, -- It would be redundant to enable Auto's preprocessing for Auto calls
+      includeExpensiveRules := none,
+      selFunction := none
+    }
+    .none
+
+-- Misc Duper issue:
+example (hFin : ∀ x : Nat, ∀ y : Nat, x < y ↔ ∃ a : Fin x, a.1 = x)
+  (lt_succ : ∀ n : Nat, n < n.succ) (lt_trans : ∀ x y z : Nat, x < y → y < z → x < z) :
+  ∃ a : Fin (Nat.succ (Nat.succ 0)), a.1 = 0 := by
+  sorry -- duper [*] {portfolioInstance := 7} -- This causes a stack overflow
+
+inductive myProd (t1 t2 : Type _)
+| mk : t1 → t2 → myProd t1 t2
+
+open myProd
+
+-- `unfoldProj` bug in lean-auto
+example (sum : myProd Int Int → Int)
+  (hSum : ∀ x : Int, ∀ y : Int, sum (mk x y) = x + y)
+  (x : myProd Int Int) : ∃ y : myProd Int Int, sum x < sum y := by
+  have test :
+    let _mk_sel0 : myProd Int Int → Int := myProd.rec (motive := fun _ => Int) fun arg0 arg1 => arg0
+    _mk_sel0 x = 0 := sorry -- This triggers `unfoldProj :: myProd is not a structure`
+  duper [*] {portfolioInstance := 1}
diff --git a/Duper/Tests/temp2.lean b/Duper/Tests/temp2.lean
new file mode 100644
index 0000000..88c52f7
--- /dev/null
+++ b/Duper/Tests/temp2.lean
@@ -0,0 +1,117 @@
+import Duper
+import Duper.TPTP
+
+set_option auto.tptp true
+set_option auto.tptp.premiseSelection true
+set_option auto.tptp.solver.name "zipperposition"
+set_option trace.auto.tptp.result true
+set_option trace.auto.tptp.printQuery true
+set_option auto.native true
+
+open Lean Auto
+
+@[rebind Auto.Native.solverFunc]
+def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
+  let formulas ← Duper.autoLemmasToFormulas lemmas
+  let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
+  Duper.runDuperPortfolioMode formulas .none
+    { portfolioMode := true,
+      portfolioInstance := none,
+      inhabitationReasoning := none,
+      preprocessing := Duper.PreprocessingOption.NoPreprocessing, -- It would be redundant to enable Auto's preprocessing for Auto calls
+      includeExpensiveRules := none,
+      selFunction := none
+    }
+    .none
+
+inductive myType
+| const1 : myType
+| const2 : myType
+
+inductive myType2 (t : Type _)
+| const3 : t → myType2 t
+| const4 : t → myType2 t
+
+inductive myType3
+| const5 : myType3
+| const6 : myType3 → myType3
+
+inductive myType4 (t1 t2 : Type _)
+| const7 : t1 → t2 → myType4 t1 t2
+
+inductive myEmpty (t1 : Type _) (t2 : Type _)
+
+open myType myType2 myType3 myType4
+
+set_option duper.collectDatatypes true
+set_option trace.duper.rule.datatypeExhaustiveness true
+set_option trace.duper.printProof true
+set_option trace.duper.collectDatatypes.debug true
+
+example : ∀ xs : List Unit, ∀ x : Unit, x :: xs ≠ xs := by
+  -- duper [List.all_nil] {portfolioInstance := 7}
+  sorry -- Works when datatypeAcyclicity is enabled
+
+--------------------------------------------------------------------
+/- This example times out when `duper.collectDatatypes` is enabled, look into whether this is a bug or to be expected
+
+example (f : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat)
+  (g : Nat → Nat → Nat → Nat → Nat → Nat)
+  (inertia : TPTP.iota → TPTP.iota → TPTP.iota → Prop)
+  (goodInertia goodChance : TPTP.iota → Prop)
+  (organization: TPTP.iota → TPTP.iota → Prop)
+  -- good inertia implies good survival chance
+  (dummy: ∀ (Y T2 I2 P2 : TPTP.iota), organization Y T2 ∧ inertia Y I2 T2 ∧ goodInertia I2 → goodChance P2)
+  : ∃ x : Nat,
+       f (g x x x x x) (g x 1 x x x) (g x x x x x) (g x 1 x x x) (g x x x x x) (g x 1 x x x) (g x x x x x)
+     = f (g 1 x x x x) (g x x x x x) (g x 1 x x x) (g x x x x x) (g x 1 x x x) (g x x x x x) (g x 1 x x x) :=
+  by duper {portfolioInstance := 7}
+-/
+
+--------------------------------------------------------------------
+-- Issues relating to Bool support
+
+set_option trace.duper.saturate.debug true in
+theorem Bool.not_eq_true2 (b : Bool) : (¬(b = true)) = (b = false) := by
+  duper {portfolioInstance := 1}
+  -- Final Active Set: [∀ (a a_1 : Bool), a = a_1]
+
+set_option trace.duper.saturate.debug true in
+theorem Bool.not_eq_false2 (b : Bool) : (¬(b = false)) = (b = true) := by
+  duper {portfolioInstance := 1}
+  -- Final Active Set: [∀ (a a_1 : Bool), a = a_1]
+
+--------------------------------------------------------------------
+-- Issues relating to type inhabitation reasoning
+
+set_option trace.duper.timeout.debug true in
+theorem forall_comm2 {p : α → β → Prop} : (∀ a b, p a b) ↔ (∀ b a, p a b) :=
+  by sorry -- duper {inhabitationReasoning := true}
+
+set_option trace.duper.timeout.debug true in
+theorem exists_comm2 {p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p a b) :=
+  by sorry -- duper {inhabitationReasoning := true}
+
+set_option trace.duper.timeout.debug true in
+theorem forall_apply_eq_imp_iff2 {f : α → β} {p : β → Prop} :
+  (∀ b a, f a = b → p b) ↔ ∀ a, p (f a) := by sorry -- duper {inhabitationReasoning := true}
+
+theorem exists_exists_and_eq_and {f : α → β} {p : α → Prop} {q : β → Prop} :
+  ∃ a, p a ∧ q (f a) → (∃ b, (∃ a, p a ∧ f a = b) ∧ q b) := by duper
+
+theorem exists_exists_eq_and {f : α → β} {p : β → Prop} :
+  ∃ a, p (f a) → (∃ b, (∃ a, f a = b) ∧ p b) := by duper
+
+--------------------------------------------------------------------
+theorem forall₂_true_iff1 {β : α → Sort} : (∀ a, β a → True) ↔ True := by duper [*]
+
+-- Look into why Duper can solve `forall₂_true_iff1` but not `forall₂_true_iff2`
+theorem forall₂_true_iff2 {β : α → Sort _} : (∀ a, β a → True) ↔ True := by duper [*]
+
+--------------------------------------------------------------------
+set_option trace.duper.saturate.debug true in
+set_option duper.throwPortfolioErrors true in
+theorem exists₂_comm
+    {ι₁ ι₂ : Sort} {κ₁ : ι₁ → Sort} {κ₂ : ι₂ → Sort} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
+    (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂ := by
+  duper [*] {preprocessing := no_preprocessing}
diff --git a/Duper/Tests/test_continuity.lean b/Duper/Tests/test_continuity.lean
index 4a65d23..3ea2fe3 100644
--- a/Duper/Tests/test_continuity.lean
+++ b/Duper/Tests/test_continuity.lean
@@ -1,9 +1,9 @@
 import Duper.Tactic
 
 axiom Real : Type
-axiom dist : Real → Real → Real 
-axiom add : Real → Real → Real 
-axiom lt : Real → Real → Prop 
+axiom dist : Real → Real → Real
+axiom add : Real → Real → Real
+axiom lt : Real → Real → Prop
 axiom zero : Real
 axiom one : Real
 
@@ -22,15 +22,26 @@ theorem zero_lt_one (a : Real) : lt zero one := sorry
 example (a : Real) : continuous (λ _ => a) :=
   by simp only [continuous_at, continuous]; duper [dist_self]
 
+example (a : Real) : continuous (λ _ => a) :=
+  by duper [continuous_at, continuous, dist_self]
+
 example (a : Real) : uniformly_continuous (λ _ => a) :=
   by simp only [uniformly_continuous]; duper [dist_self, zero_lt_one]
 
+example (a : Real) : uniformly_continuous (λ _ => a) :=
+  by duper [uniformly_continuous, dist_self, zero_lt_one]
+
 example (a : Real) : continuous (λ x => x) :=
   by simp only [continuous_at, continuous]; duper [dist_self]
 
+example (a : Real) : continuous (λ x => x) :=
+  by duper [continuous_at, continuous, dist_self]
+
 example (a : Real) : uniformly_continuous (λ x => x) :=
-  by simp only [uniformly_continuous]; duper [dist_self, zero_lt_one]
+  by duper [uniformly_continuous, dist_self, zero_lt_one]
 
 example (f : Real → Real) : uniformly_continuous f → continuous f :=
   by simp only [continuous, continuous_at, uniformly_continuous]; duper
 
+example (f : Real → Real) : uniformly_continuous f → continuous f :=
+  by duper [continuous, continuous_at, uniformly_continuous]
diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean
index 82ba924..435ab96 100644
--- a/Duper/Tests/test_regression.lean
+++ b/Duper/Tests/test_regression.lean
@@ -1,4 +1,4 @@
-import Duper.Tactic
+import Duper
 import Duper.TPTP
 
 -- set_option pp.all true
@@ -337,23 +337,23 @@ theorem COM002_2_test3 (state label statement : Type) (p3 : state) (goto : label
 -/
 
 --###############################################################################################################################
-tptp KRS003_1 "../TPTP-v8.0.0/Problems/KRS/KRS003_1.p"
+tptp KRS003_1 "../TPTP-v9.0.0/Problems/KRS/KRS003_1.p"
   by duper [*]
 
 #print axioms KRS003_1
 
-tptp PUZ012_1 "../TPTP-v8.0.0/Problems/PUZ/PUZ012_1.p"
+tptp PUZ012_1 "../TPTP-v9.0.0/Problems/PUZ/PUZ012_1.p"
   by duper [*]
 
 #print PUZ012_1
 --###############################################################################################################################
 -- Tests that (in the current commit at least) use positive simplify reflect
 set_option trace.duper.rule.simplifyReflect true in
-tptp NUN004_5 "../TPTP-v8.0.0/Problems/NUN/NUN004_5.p"
+tptp NUN004_5 "../TPTP-v9.0.0/Problems/NUN/NUN004_5.p"
   by duper [*]
 
 set_option trace.duper.rule.simplifyReflect true in
-tptp ITP209_2 "../TPTP-v8.0.0/Problems/ITP/ITP209_2.p"
+tptp ITP209_2 "../TPTP-v9.0.0/Problems/ITP/ITP209_2.p"
   by duper [*]
 
 --###############################################################################################################################
@@ -471,10 +471,10 @@ example (x : Type u) (f g : Type u → Type v) (H : f = g) : f x = g x :=
 example (x y z : Type u) (f g : Type u → Type u → Type u → Type v) (H : f = g) : f x y z = g x y z :=
   by duper [*]
 
-tptp PUZ137_8 "../TPTP-v8.0.0/Problems/PUZ/PUZ137_8.p"
+tptp PUZ137_8 "../TPTP-v9.0.0/Problems/PUZ/PUZ137_8.p"
   by duper [*]
 
-tptp PUZ031_1_modified "../TPTP-v8.0.0/Problems/PUZ/PUZ031_1.p" by
+tptp PUZ031_1_modified "../TPTP-v9.0.0/Problems/PUZ/PUZ031_1.p" by
   have inhabited_plant : Inhabited plant := sorry
   have inhabited_snail : Inhabited snail := sorry
   have inhabited_grain : Inhabited grain := sorry
@@ -486,11 +486,11 @@ tptp PUZ031_1_modified "../TPTP-v8.0.0/Problems/PUZ/PUZ031_1.p" by
   duper [*]
   -- If these instances are not provided, duper will fail
 
-tptp SEU123 "../TPTP-v8.0.0/Problems/SEU/SEU123+1.p"
+tptp SEU123 "../TPTP-v9.0.0/Problems/SEU/SEU123+1.p"
   by duper [*]
 
 set_option trace.duper.rule.superposition true in
-tptp SEU139 "../TPTP-v8.0.0/Problems/SEU/SEU139+1.p"
+tptp SEU139 "../TPTP-v9.0.0/Problems/SEU/SEU139+1.p"
   by duper [*]
 
 --###############################################################################################################################
@@ -538,7 +538,7 @@ def neg3 : g (True → True) (fun _ => True.intro) = g (True → True) (fun _ =>
 end NegativeBoolSimpTests
 
 /- ClauseStreamHeap tests -/
-tptp MGT008 "../TPTP-v8.0.0/Problems/MGT/MGT008+1.p"
+tptp MGT008 "../TPTP-v9.0.0/Problems/MGT/MGT008+1.p"
   by duper [*]
 
 example (f : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat)