diff --git a/Hammer/DuperCore.lean b/Hammer/DuperCore.lean
index 436fe4a..cefe4cb 100644
--- a/Hammer/DuperCore.lean
+++ b/Hammer/DuperCore.lean
@@ -57,7 +57,7 @@ def getDuperCoreLemmas (unsatCoreDerivLeafStrings : Array String) (userFacts : S
       coreUserFacts := coreUserFacts.push factStx
   -- Build `formulas` to pass into `runDuperPortfolioMode`
   trace[hammer.debug] "{decl_name%} :: Collecting assumptions. coreUserFacts: {coreUserFacts}"
-  let mut formulas := (← collectAssumptions coreUserFacts includeAllLctx goalDecls).toArray
+  let formulas ← collectAssumptions coreUserFacts includeAllLctx goalDecls
   -- Try to reconstruct the proof using `runDuperPortfolioMode`
   let prf ←
     try
diff --git a/Hammer/HammerCore.lean b/Hammer/HammerCore.lean
index ced2809..04b263e 100644
--- a/Hammer/HammerCore.lean
+++ b/Hammer/HammerCore.lean
@@ -123,8 +123,9 @@ def runDuper (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tact
     -- **NOTE** We collect `formulas` using `Duper.collectAssumptions` rather than `Auto.collectAllLemmas` because `Auto.collectAllLemmas`
     -- does not currently support a mode where unusable facts are ignored.
     let formulas ← withDuperOptions $ collectAssumptions premises includeLCtx goalDecls
-    withSolverOptions configOptions do
-      let lemmas ← formulasToAutoLemmas formulas (includeInSetOfSupport := true)
+    -- `runDuper` calls the solver independently as part of its own procedure, so the long timeout is used
+    withSolverOptions configOptions.solverLongTimeout do
+      let lemmas ← formulasToAutoLemmas formulas.toList (includeInSetOfSupport := true)
       -- Calling `Auto.unfoldConstAndPreprocessLemma` is an essential step for the monomorphization procedure
       let lemmas ←
         tryCatchRuntimeEx
diff --git a/Hammer/Options.lean b/Hammer/Options.lean
index cb6ec7a..e9a650f 100644
--- a/Hammer/Options.lean
+++ b/Hammer/Options.lean
@@ -19,9 +19,14 @@ declare_syntax_cat Hammer.bool_lit (behavior := symbol)
 syntax "true" : Hammer.bool_lit
 syntax "false" : Hammer.bool_lit
 
-register_option hammer.solverTimeoutDefault : Nat := {
+register_option hammer.solverShortTimeoutDefault : Nat := {
+  defValue := 1
+  descr := "The default short timeout for the solver (in seconds). This is used when Aesop calls multiple solvers as subprocedures."
+}
+
+register_option hammer.solverLongTimeoutDefault : Nat := {
   defValue := 5
-  descr := "The default timeout for the solver (in seconds)"
+  descr := "The default long timeout for the solver (in seconds). This is used when a solver is called independently as part of its own procedure."
 }
 
 register_option hammer.wallclockTimeoutDefault : Nat := {
@@ -59,9 +64,14 @@ register_option hammer.aesopPremisesDefault : Nat := {
   descr := "The default number of premises sent to aesop to be used as unsafe rules"
 }
 
-register_option hammer.duperPremisesDefault : Nat := {
+register_option hammer.duperPremisesShortDefault : Nat := {
   defValue := 16
-  descr := "The default number of premises sent to duper"
+  descr := "The default number of premises sent to duper when called as a subprocedure in Aesop"
+}
+
+register_option hammer.duperPremisesLongDefault : Nat := {
+  defValue := 100
+  descr := "The default number of premises sent to duper when called as an independent procedure"
 }
 
 register_option hammer.grindPremisesDefault : Nat := {
@@ -106,14 +116,16 @@ register_option hammer.outputAllSuggestionsDefault : Bool := {
 
 namespace HammerCore
 
-def getHammerSolverTimeoutDefault (opts : Options) : Nat := hammer.solverTimeoutDefault.get opts
+def getHammerSolverShortTimeoutDefault (opts : Options) : Nat := hammer.solverShortTimeoutDefault.get opts
+def getHammerSolverLongTimeoutDefault (opts : Options) : Nat := hammer.solverLongTimeoutDefault.get opts
 def getHammerWallclockTimeoutDefault (opts : Options) : Nat := hammer.wallclockTimeoutDefault.get opts
 def getPreprocessingDefault (opts : Options) : String := hammer.preprocessingDefault.get opts
 def getDisableAesopDefault (opts : Options) : Bool := hammer.disableAesopDefault.get opts
 def getDisableDuperDefault (opts : Options) : Bool := hammer.disableDuperDefault.get opts
 def getDisableGrindDefault (opts : Options) : Bool := hammer.disableGrindDefault.get opts
 def getDisableSmtDefault (opts : Options) : Bool := hammer.disableSmtDefault.get opts
-def getDuperPremisesDefault (opts : Options) : Nat := hammer.duperPremisesDefault.get opts
+def getDuperPremisesShortDefault (opts : Options) : Nat := hammer.duperPremisesShortDefault.get opts
+def getDuperPremisesLongDefault (opts : Options) : Nat := hammer.duperPremisesLongDefault.get opts
 def getAesopPremisesDefault (opts : Options) : Nat := hammer.aesopPremisesDefault.get opts
 def getGrindPremisesDefault (opts : Options) : Nat := hammer.grindPremisesDefault.get opts
 def getSmtPremisesDefault (opts : Options) : Nat := hammer.smtPremisesDefault.get opts
@@ -124,9 +136,13 @@ def getAesopSmtPriorityDefault (opts : Options) : Nat := hammer.aesopSmtPriority
 def getParallelismDefault (opts : Options) : Bool := hammer.parallelismDefault.get opts
 def getOutputAllSuggestionsDefault (opts : Options) : Bool := hammer.outputAllSuggestionsDefault.get opts
 
-def getHammerSolverTimeoutDefaultM : CoreM Nat := do
+def getHammerSolverShortTimeoutDefaultM : CoreM Nat := do
   let opts ← getOptions
-  return getHammerSolverTimeoutDefault opts
+  return getHammerSolverShortTimeoutDefault opts
+
+def getHammerSolverLongTimeoutDefaultM : CoreM Nat := do
+  let opts ← getOptions
+  return getHammerSolverLongTimeoutDefault opts
 
 def getHammerWallclockTimeoutDefaultM : CoreM Nat := do
   let opts ← getOptions
@@ -152,9 +168,13 @@ def getDisableSmtDefaultM : CoreM Bool := do
   let opts ← getOptions
   return getDisableSmtDefault opts
 
-def getDuperPremisesDefaultM : CoreM Nat := do
+def getDuperPremisesShortDefaultM : CoreM Nat := do
+  let opts ← getOptions
+  return getDuperPremisesShortDefault opts
+
+def getDuperPremisesLongDefaultM : CoreM Nat := do
   let opts ← getOptions
-  return getDuperPremisesDefault opts
+  return getDuperPremisesLongDefault opts
 
 def getAesopPremisesDefaultM : CoreM Nat := do
   let opts ← getOptions
@@ -231,14 +251,16 @@ def elabBoolLit [Monad m] [MonadError m] (stx : TSyntax `Hammer.bool_lit) : m Bo
     | `(bool_lit| false) => return false
     | _ => Elab.throwUnsupportedSyntax
 
-syntax (&"solverTimeout" " := " numLit) : Hammer.configOption
+syntax (&"solverShortTimeout" " := " numLit) : Hammer.configOption
+syntax (&"solverLongTimeout" " := " numLit) : Hammer.configOption
 syntax (&"wallclockTimeout" " := " numLit) : Hammer.configOption
 syntax (&"preprocessing" " := " Hammer.preprocessing) : Hammer.configOption
 syntax (&"disableDuper" " := " Hammer.bool_lit) : Hammer.configOption
 syntax (&"disableAesop" " := " Hammer.bool_lit) : Hammer.configOption
 syntax (&"disableGrind" " := " Hammer.bool_lit) : Hammer.configOption
 syntax (&"disableSmt" " := " Hammer.bool_lit) : Hammer.configOption
-syntax (&"duperPremises" " := " numLit) : Hammer.configOption -- The number of premises sent to `duper` (default: 16)
+syntax (&"duperPremisesShort" " := " numLit) : Hammer.configOption -- The number of premises sent to `duper` when called as a subprocedure in Aesop (default: 16)
+syntax (&"duperPremisesLong" " := " numLit) : Hammer.configOption -- The number of premises sent to `duper` when called as an independent procedure (default: 100)
 syntax (&"aesopPremises" " := " numLit) : Hammer.configOption -- The number of premises sent to `aesop` (default: 32)
 syntax (&"grindPremises" " := " numLit) : Hammer.configOption -- The number of premises sent to `grind` (default: 100)
 syntax (&"smtPremises" " := " numLit) : Hammer.configOption -- The number of premises sent to `lean-smt` (default: 16)
@@ -250,7 +272,8 @@ syntax (&"parallelism" " := " Hammer.bool_lit) : Hammer.configOption -- Whether
 syntax (&"outputAllSuggestions" " := " Hammer.bool_lit) : Hammer.configOption -- Whether to show the user all suggestions or just the first one (default: false)
 
 structure ConfigurationOptions where
-  solverTimeout : Nat
+  solverShortTimeout : Nat -- The solver timeout used when Aesop calls multiple solvers as subprocedures
+  solverLongTimeout : Nat -- The solver timeout used when a solver is called independently as part of its own procedure
   wallclockTimeout : Nat
   preprocessing : Preprocessing
   disableDuper : Bool
@@ -261,7 +284,8 @@ structure ConfigurationOptions where
   aesopDuperPriority : Nat
   aesopGrindPriority : Nat
   aesopSmtPriority : Nat
-  duperPremises : Nat -- The number of premises sent to `duper` (default: 16)
+  duperPremisesShort : Nat -- The number of premises sent to `duper` when called as a subprocedure in Aesop (default: 16)
+  duperPremisesLong : Nat -- The number of premises sent to `duper` when called as an independent procedure (default: 100)
   aesopPremises : Nat -- The number of premises sent to `aesop` (default: 32)
   grindPremises : Nat -- The number of premises sent to `grind` (default: 100)
   smtPremises : Nat -- The number of premises sent to `lean-smt` (default: 16)
@@ -279,8 +303,14 @@ macro_rules | `(tactic| hammerCore [$simpLemmas,*] [$facts,*]) => `(tactic| hamm
 
 /-- Checks to ensure that the set of given `configOptions` is usable. -/
 def validateConfigOptions (configOptions : ConfigurationOptions) : TacticM ConfigurationOptions := do
-  if configOptions.wallclockTimeout > 0 && configOptions.wallclockTimeout < configOptions.solverTimeout then
-    throwError "Erroneous invocation of hammer: The wallclockTimeout must be greater than or equal to the solverTimeout"
+  if configOptions.solverShortTimeout > configOptions.solverLongTimeout then
+    throwError "Erroneous invocation of hammer: The solverShortTimeout must be less than or equal to the solverLongTimeout"
+  if configOptions.wallclockTimeout == 0 then
+    throwError "Erroneous invocation of hammer: The wallclockTimeout must be greater than 0"
+  if configOptions.wallclockTimeout < configOptions.solverShortTimeout then
+    throwError "Erroneous invocation of hammer: The wallclockTimeout must be greater than or equal to the solverShortTimeout"
+  if configOptions.wallclockTimeout < configOptions.solverLongTimeout then
+    throwError "Erroneous invocation of hammer: The wallclockTimeout must be greater than or equal to the solverLongTimeout"
   if !configOptions.parallelism && configOptions.outputAllSuggestions then
     throwError "Erroneous invocation of hammer: The outputAllSuggestions option can only be enabled when parallelism is enabled"
   if configOptions.disableAesop && configOptions.disableDuper && configOptions.disableGrind && configOptions.disableSmt then
@@ -310,14 +340,16 @@ def validateConfigOptions (configOptions : ConfigurationOptions) : TacticM Confi
   return configOptions
 
 def parseConfigOptions (configOptionsStx : TSyntaxArray `Hammer.configOption) : TacticM ConfigurationOptions := do
-  let mut solverTimeoutOpt := none
+  let mut solverShortTimeoutOpt := none
+  let mut solverLongTimeoutOpt := none
   let mut wallclockTimeoutOpt := none
   let mut preprocessingOpt := none
   let mut disableDuperOpt := none
   let mut disableAesopOpt := none
   let mut disableGrindOpt := none
   let mut disableSmtOpt := none
-  let mut duperPremisesOpt := none
+  let mut duperPremisesShortOpt := none
+  let mut duperPremisesLongOpt := none
   let mut aesopPremisesOpt := none
   let mut grindPremisesOpt := none
   let mut smtPremisesOpt := none
@@ -329,9 +361,12 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Hammer.configOption) :
   let mut outputAllSuggestionsOpt := none
   for configOptionStx in configOptionsStx do
     match configOptionStx with
-    | `(Hammer.configOption| solverTimeout := $userSolverTimeout:num) =>
-      if solverTimeoutOpt.isNone then solverTimeoutOpt := some (TSyntax.getNat userSolverTimeout)
-      else throwError "Erroneous invocation of hammer: The solverTimeout option has been specified multiple times"
+    | `(Hammer.configOption| solverShortTimeout := $userSolverShortTimeout:num) =>
+      if solverShortTimeoutOpt.isNone then solverShortTimeoutOpt := some (TSyntax.getNat userSolverShortTimeout)
+      else throwError "Erroneous invocation of hammer: The solverShortTimeout option has been specified multiple times"
+    | `(Hammer.configOption| solverLongTimeout := $userSolverLongTimeout:num) =>
+      if solverLongTimeoutOpt.isNone then solverLongTimeoutOpt := some (TSyntax.getNat userSolverLongTimeout)
+      else throwError "Erroneous invocation of hammer: The solverLongTimeout option has been specified multiple times"
     | `(Hammer.configOption| wallclockTimeout := $userWallclockTimeout:num) =>
       if wallclockTimeoutOpt.isNone then wallclockTimeoutOpt := some (TSyntax.getNat userWallclockTimeout)
       else throwError "Erroneous invocation of hammer: The wallclockTimeout option has been specified multiple times"
@@ -350,9 +385,12 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Hammer.configOption) :
     | `(Hammer.configOption| disableSmt := $disableSmtBoolLit:Hammer.bool_lit) =>
       if disableSmtOpt.isNone then disableSmtOpt := some $ ← elabBoolLit disableSmtBoolLit
       else throwError "Erroneous invocation of hammer: The disableSmt option has been specified multiple times"
-    | `(Hammer.configOption| duperPremises := $userDuperPremises:num) =>
-      if duperPremisesOpt.isNone then duperPremisesOpt := some (TSyntax.getNat userDuperPremises)
-      else throwError "Erroneous invocation of hammer: The duperPremises option has been specified multiple times"
+    | `(Hammer.configOption| duperPremisesShort := $userDuperPremisesShort:num) =>
+      if duperPremisesShortOpt.isNone then duperPremisesShortOpt := some (TSyntax.getNat userDuperPremisesShort)
+      else throwError "Erroneous invocation of hammer: The duperPremisesShort option has been specified multiple times"
+    | `(Hammer.configOption| duperPremisesLong := $userDuperPremisesLong:num) =>
+      if duperPremisesLongOpt.isNone then duperPremisesLongOpt := some (TSyntax.getNat userDuperPremisesLong)
+      else throwError "Erroneous invocation of hammer: The duperPremisesLong option has been specified multiple times"
     | `(Hammer.configOption| aesopPremises := $userAesopPremises:num) =>
       if aesopPremisesOpt.isNone then aesopPremisesOpt := some (TSyntax.getNat userAesopPremises)
       else throwError "Erroneous invocation of hammer: The aesopPremises option has been specified multiple times"
@@ -382,10 +420,14 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Hammer.configOption) :
       else throwError "Erroneous invocation of hammer: The outputAllSuggestions option has been specified multiple times"
     | _ => throwUnsupportedSyntax
   -- Set default values for options that were not specified
-  let solverTimeout ←
-    match solverTimeoutOpt with
-    | none => getHammerSolverTimeoutDefaultM
-    | some solverTimeout => pure solverTimeout
+  let solverShortTimeout ←
+    match solverShortTimeoutOpt with
+    | none => getHammerSolverShortTimeoutDefaultM
+    | some solverShortTimeout => pure solverShortTimeout
+  let solverLongTimeout ←
+    match solverLongTimeoutOpt with
+    | none => getHammerSolverLongTimeoutDefaultM
+    | some solverLongTimeout => pure solverLongTimeout
   let wallclockTimeout ←
     match wallclockTimeoutOpt with
     | none => getHammerWallclockTimeoutDefaultM
@@ -412,10 +454,14 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Hammer.configOption) :
       if disableAesop && (← getPreprocessingDefaultM) == "aesop" then pure Preprocessing.no_preprocessing
       else elabPreprocessingDefault
     | some preprocessing => pure preprocessing
-  let duperPremises ←
-    match duperPremisesOpt with
-    | none => getDuperPremisesDefaultM
-    | some duperPremises => pure duperPremises
+  let duperPremisesShort ←
+    match duperPremisesShortOpt with
+    | none => getDuperPremisesShortDefaultM
+    | some duperPremisesShort => pure duperPremisesShort
+  let duperPremisesLong ←
+    match duperPremisesLongOpt with
+    | none => getDuperPremisesLongDefaultM
+    | some duperPremisesLong => pure duperPremisesLong
   let aesopPremises ←
     match aesopPremisesOpt with
     | none => getAesopPremisesDefaultM
@@ -453,9 +499,11 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Hammer.configOption) :
     | none => getOutputAllSuggestionsDefaultM
     | some outputAllSuggestions => pure outputAllSuggestions
   let configOptions := {
-    solverTimeout := solverTimeout, wallclockTimeout := wallclockTimeout, preprocessing := preprocessing,
+    solverShortTimeout := solverShortTimeout, solverLongTimeout := solverLongTimeout,
+    wallclockTimeout := wallclockTimeout, preprocessing := preprocessing,
     disableDuper := disableDuper, disableGrind := disableGrind, disableAesop := disableAesop, disableSmt := disableSmt,
-    duperPremises := duperPremises, aesopPremises := aesopPremises, grindPremises := grindPremises,
+    duperPremisesShort := duperPremisesShort, duperPremisesLong := duperPremisesLong,
+    aesopPremises := aesopPremises, grindPremises := grindPremises,
     smtPremises := smtPremises, aesopPremisePriority := aesopPremisePriority, aesopDuperPriority := aesopDuperPriority,
     aesopGrindPriority := aesopGrindPriority, aesopSmtPriority := aesopSmtPriority, parallelism := parallelism,
     outputAllSuggestions := outputAllSuggestions
@@ -463,11 +511,13 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Hammer.configOption) :
   let configOptions ← validateConfigOptions configOptions
   return configOptions
 
-def withSolverOptions [Monad m] [MonadError m] [MonadWithOptions m] (configOptions : ConfigurationOptions) (x : m α) : m α :=
+/-- `solverTimeout` should be `configOptions.solverShortTimeout` when the solver is called by Aesop as a subprocedure
+    and `configOptions.solverLongTimeout` when the solver is called independently as part of its own procedure. -/
+def withSolverOptions [Monad m] [MonadError m] [MonadWithOptions m] (solverTimeout : Nat) (x : m α) : m α :=
   withOptions
     (fun o =>
       let o := o.set `auto.tptp true
-      let o := o.set `auto.tptp.timeout configOptions.solverTimeout
+      let o := o.set `auto.tptp.timeout solverTimeout
       let o := o.set `auto.smt false
       let o := o.set `auto.tptp.premiseSelection true
       let o := o.set `auto.tptp.solver.name "zipperposition"
diff --git a/Hammer/SingleRuleTac.lean b/Hammer/SingleRuleTac.lean
index 3610306..f27aa4e 100644
--- a/Hammer/SingleRuleTac.lean
+++ b/Hammer/SingleRuleTac.lean
@@ -14,18 +14,19 @@ open Lean Meta Parser Elab Tactic Auto Duper Syntax Aesop Qq
 
 namespace HammerCore
 
-/-- Constructs a `SingleRuleTac` that uses Lean-auto/Zipperposition to attempt to solve the input goal with `formulas` (and all facts in the local context
-    if `includeLCtx` is enabled), and either throws an error (if Lean-auto/Zipperposition fail) or suggests a Duper invocation using the subset of `formulas`
-    that Zipperposition used to find a proof.
+/-- Constructs a `SingleRuleTac` that uses Lean-auto/Zipperposition to attempt to solve the input goal with `formulas` (retrieved from
+    `Hammer.duperSubprocedureInputExt`) and all facts in the local context if `includeLCtx` is enabled, then either throws an error
+    (if Lean-auto/Zipperposition fail) or suggests a Duper invocation using the subset of `formulas` that Zipperposition used to find a proof.
 
     **TODO** Currently, Zipperposition's unsat core is not used to minimize the set of formulas from the local context that are sent to Duper, but in
     the future, this behavior should be added as an option (it should theoretically improve the strength of some suggested Duper invocations at the cost
     of increasing the size of all suggested Duper invocations). -/
-def duperSingleRuleTac (formulas : List (Expr × Expr × Array Name × Bool × String))
-  (includeLCtx : Bool) (configOptions : ConfigurationOptions) : SingleRuleTac := λ input => do
+def duperSingleRuleTac : SingleRuleTac := λ input => do
   let preState ← saveState
   input.goal.withContext do
     Core.checkSystem s!"{decl_name%}"
+    let some (formulas, includeLCtx, configOptions) := Hammer.duperSubprocedureInputExt.getState (← getEnv)
+      | throwError "{decl_name%} :: The Duper subprocedure's input was not set (this rule is only meant to be invoked by `hammer`)"
     let lctxBeforeIntros ← getLCtx
     let originalMainGoal := input.goal
     let goalType ← originalMainGoal.getType
@@ -63,9 +64,17 @@ def duperSingleRuleTac (formulas : List (Expr × Expr × Array Name × Bool × S
             | none => some (fact, proof, params, isFromGoal, none)
             | some stx => some (fact, proof, params, isFromGoal, some s!"{stx}")
         )
-      let formulas := (formulas.map (fun (fact, proof, params, isFromGoal, stxOpt) => (fact, proof, params, isFromGoal, some stxOpt))) ++ lctxFormulas
-      withSolverOptions configOptions do
-        let lemmas ← formulasWithStringsToAutoLemmas formulas (includeInSetOfSupport := true)
+      /- It is important that `lctxFormulas` (which includes assumptions from `goalDecls`) comes before the `formulas` produced
+         by premise selection. This is to maintain the implicit invariant that the most important/relevant lemmas come first.
+
+         This implicit invariant is important because `Auto.Monomorphization.saturate` processes lemmas in the order that they are
+         provided, and `auto.mono.saturationThreshold` can cause later lemmas to not be processed (`trace.auto.mono` shows when
+         Monomorphization's saturation threshold has been reached). -/
+      let formulas := formulas.map (fun (fact, proof, params, isFromGoal, stxOpt) => (fact, proof, params, isFromGoal, some stxOpt))
+      let formulas := lctxFormulas.append formulas
+      -- The solver is called by Aesop as a subprocedure, so the short timeout is used
+      withSolverOptions configOptions.solverShortTimeout do
+        let lemmas ← formulasWithStringsToAutoLemmas formulas.toList (includeInSetOfSupport := true)
         -- Calling `Auto.unfoldConstAndPreprocessLemma` is an essential step for the monomorphization procedure
         let lemmas ←
           tryCatchRuntimeEx
@@ -97,9 +106,9 @@ def duperSingleRuleTac (formulas : List (Expr × Expr × Array Name × Bool × S
         -- Build a Duper call using includeLCtx and each coreUserInputFact
         let stx ←
           if !coreFormulas.isEmpty && includeLCtx then
-            `(tactic| duper [*, $(coreFormulas.toArray),*] {preprocessing := full})
+            `(tactic| duper [*, $coreFormulas,*] {preprocessing := full})
           else if !coreFormulas.isEmpty && !includeLCtx then
-            `(tactic| duper [$(coreFormulas.toArray),*] {preprocessing := full})
+            `(tactic| duper [$coreFormulas,*] {preprocessing := full})
           else if coreFormulas.isEmpty && includeLCtx then
             `(tactic| duper [*] {preprocessing := full})
           else -- coreFormulas.isEmpty && !includeLCtx
@@ -116,12 +125,14 @@ def duperSingleRuleTac (formulas : List (Expr × Expr × Array Name × Bool × S
         let postGoals ← postGoals.mapM (mvarIdToSubgoal input.goal ·)
         return (postGoals, some #[step], some ⟨1.0⟩)
 
-/-- Runs `grind?` with `grind` parameters built from `grindPremiseNames`, then records the first `grind` tactic
-    that `grind?` suggests (the same suggestion the interactive `grind?` tactic would emit) as an Aesop script step. -/
-def grindSingleRuleTac (grindPremiseNames : Array Name) : SingleRuleTac := λ input => do
+/-- Runs `grind?` with `grind` parameters built from `grindPremiseNames` (retrieved from `Hammer.grindSubprocedureInputExt`), then records the
+    first `grind` tactic that `grind?` suggests (the same suggestion the interactive `grind?` tactic would emit) as an Aesop script step. -/
+def grindSingleRuleTac : SingleRuleTac := λ input => do
   let preState ← saveState
   input.goal.withContext do
     Core.checkSystem s!"{decl_name%}"
+    let some grindPremiseNames := Hammer.grindSubprocedureInputExt.getState (← getEnv)
+      | throwError "{decl_name%} :: The Grind subprocedure's input was not set (this rule is only meant to be invoked by `hammer`)"
     let grindParamStxs : TSyntaxArray `Lean.Parser.Tactic.grindParam ←
       grindPremiseNames.mapM (fun n => `(Lean.Parser.Tactic.grindParam| $(mkIdent n):ident))
     let grindQuestionStx ← `(tactic| grind? [$grindParamStxs,*])
@@ -149,7 +160,6 @@ def grindSingleRuleTac (grindPremiseNames : Array Name) : SingleRuleTac := λ in
     let postGoals ← postGoals.mapM (mvarIdToSubgoal input.goal ·)
     return (postGoals, some #[step], some ⟨1.0⟩)
 
--- The following code was written by Tomaz Mascarenhas. It is scheduled to be added to lean-smt, and once it is, it can be removed from here.
 namespace Smt
 
 -- The type and the corresponding syntax
@@ -167,9 +177,11 @@ def createArrow (es : List Expr) (e : Expr) : Expr :=
     let hd : Q(Prop) := hd
     q($hd -> $r)
 
-def smtSingleRuleTac (ps : Premises) (includeLCtx : Bool) (configOptions : HammerCore.ConfigurationOptions) : SingleRuleTac := fun input => do
+def smtSingleRuleTac : SingleRuleTac := fun input => do
   let preState ← saveState
   input.goal.withContext do
+    let some (ps, includeLCtx, configOptions) := Hammer.smtSubprocedureInputExt.getState (← getEnv)
+      | throwError "{decl_name%} :: The Lean-SMT subprocedure's input was not set (this rule is only meant to be invoked by `hammer`)"
     let g ← input.goal.getType
     let types := ps.map (fun p => p.1)
     let arrow := createArrow types g
@@ -184,7 +196,8 @@ def smtSingleRuleTac (ps : Premises) (includeLCtx : Bool) (configOptions : Hamme
           pure ((← Smt.Preprocess.getPropHyps).filter (fun fv => !hs.contains fv))
       else
         pure #[]
-    let res ← Smt.smt {mono := true, timeout := configOptions.solverTimeout} mv' (hs.map (fun fv => .fvar fv) ++ lctxHyps.map (fun fv => .fvar fv))
+    -- Lean-SMT is called by Aesop as a subprocedure, so the short timeout is used
+    let res ← Smt.smt {mono := true, timeout := configOptions.solverShortTimeout} mv' (hs.map (fun fv => .fvar fv) ++ lctxHyps.map (fun fv => .fvar fv))
     let unsat_core ←
       match res with
       | .unsat mvs uc => pure uc
@@ -204,7 +217,7 @@ def smtSingleRuleTac (ps : Premises) (includeLCtx : Bool) (configOptions : Hamme
         pure names
     let namesT ← names.mapM cast_stx
     let idents ← namesT.mapM (fun i => `(Smt.Tactic.smtHintElem| $i:term))
-    -- `cfg` doesn't include a timeout parameter because although LeanHammer's solverTimeout should be propagated to Lean-SMT for
+    -- `cfg` doesn't include a timeout parameter because although LeanHammer's solverShortTimeout should be propagated to Lean-SMT for
     -- internal calls, that timeout doesn't need to clutter the final suggestion
     let cfg ← `(optConfig| +$(mkIdent `mono))
     let stx ←
diff --git a/Hammer/Smt.lean b/Hammer/Smt.lean
index 461350d..619f6e9 100644
--- a/Hammer/Smt.lean
+++ b/Hammer/Smt.lean
@@ -57,7 +57,8 @@ def smtPipeline (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.T
   -- We create `cfg` and `cfgWithTimeout` because LeanHammer's internal `smt` call should include a timeout argument,
   -- but the suggestion LeanHammer produces doesn't need to include said argument
   let cfg ← `(optConfig| +$(mkIdent `mono))
-  let cfgWithTimeout ← `(optConfig| +$(mkIdent `mono) (timeout := $(Syntax.mkNatLit configOptions.solverTimeout)))
+  -- `smtPipeline` calls Lean-SMT independently as part of its own procedure, so the long timeout is used
+  let cfgWithTimeout ← `(optConfig| +$(mkIdent `mono) (timeout := $(Syntax.mkNatLit configOptions.solverLongTimeout)))
   let hints ←
     if includeLCtx then `(Smt.Tactic.smtHints| [*, $premises,*])
     else `(Smt.Tactic.smtHints| [$premises,*])
diff --git a/Hammer/Tactic.lean b/Hammer/Tactic.lean
index 9e8e8e1..141d1cc 100644
--- a/Hammer/Tactic.lean
+++ b/Hammer/Tactic.lean
@@ -33,6 +33,36 @@ syntax (name := hammer) "hammer" (ppSpace "[" (term),* "]")? (ppSpace "{"Hammer.
 
 set_library_suggestions open Lean.LibrarySuggestions in Cloud.premiseSelector <|> sineQuaNonSelector.intersperse currentFile
 
+/-- The Duper subprocedure invoked by Aesop takes as input:
+    - `formulas` : `Array (Expr × Expr × Array Name × Bool × String)`
+    - `includeLCtx` : `Bool`
+    - `configOptions` : `HammerCore.ConfigurationOptions` -/
+abbrev duperSubprocedureInputType := (Array (Expr × Expr × Array Name × Bool × String)) × Bool × HammerCore.ConfigurationOptions
+
+/-- An environment extension that holds the input intended for the Duper subprocedure invoked by Aesop (`HammerCore.duperSingleRuleTac`). -/
+initialize duperSubprocedureInputExt : EnvExtension (Option duperSubprocedureInputType) ←
+  registerEnvExtension (pure none) (asyncMode := .local)
+
+/-- The Grind subprocedure invoked by Aesop takes as input:
+    - `premiseNames` : `Array Name` -/
+abbrev grindSubprocedureInputType := Array Name
+
+/-- An environment extension that holds the input intended for the Grind subprocedure invoked by Aesop
+    (`HammerCore.grindSingleRuleTac`). -/
+initialize grindSubprocedureInputExt : EnvExtension (Option grindSubprocedureInputType) ←
+  registerEnvExtension (pure none) (asyncMode := .local)
+
+/-- The Lean-SMT subprocedure invoked by Aesop takes as input:
+    - `hints` : `List (Expr × Syntax)`
+    - `includeLCtx` : `Bool`
+    - `configOptions` : `HammerCore.ConfigurationOptions` -/
+abbrev smtSubprocedureInputType := (List (Expr × Syntax)) × Bool × HammerCore.ConfigurationOptions
+
+/-- An environment extension that holds the input intended for the Lean-SMT subprocedure invoked by Aesop
+    (`HammerCore.Smt.smtSingleRuleTac`). -/
+initialize smtSubprocedureInputExt : EnvExtension (Option smtSubprocedureInputType) ←
+  registerEnvExtension (pure none) (asyncMode := .local)
+
 /-- This functions produces one Aesop call where Aesop is given:
     - unsafe rules corresponding to individual premise applications (these are determined by `addIdentStxs`).
     - one unsafe rule to call the Lean-auto/Zipperposition/Duper pipeline (if `configOptions.disableDuper` is
@@ -47,66 +77,48 @@ def runAesopWithSubprocedures (duperPremises : Array Term) (addIdentStxs : TSynt
   (grindPremiseNames : Array Name) (smtPremises : Array Term) (includeLCtx : Bool)
   (configOptions : HammerCore.ConfigurationOptions) : TacticM Unit :=
   withMainContext do withOptions (fun o => o.set `aesop.warn.applyIff false) do
-    -- Building `duperRuleTacStx`
-    let formulas ← withDuperOptions $ collectAssumptions duperPremises false #[]
-    let formulas : List (Expr × Expr × Array Name × Bool × String) :=
-      -- **TODO** This approach prohibits handling arguments that aren't disambiguated theorem names
-      formulas.filterMap (fun (fact, proof, params, isFromGoal, stxOpt) =>
-        stxOpt.map (fun stx => (fact, proof, params, isFromGoal, stx.raw.getId.toString)))
-    let ruleTacType := mkConst `Aesop.SingleRuleTac
-    let duperRuleTacVal ← mkAppM `HammerCore.duperSingleRuleTac #[q($formulas), q($includeLCtx), q($configOptions)]
-    let duperRuleTacName := mkPrivateName (← getEnv) `instantiatedDuperRuleTac
-    let duperRuleTacDecl :=
-      mkDefinitionValEx duperRuleTacName [] ruleTacType duperRuleTacVal
-        ReducibilityHints.opaque DefinitionSafety.safe [duperRuleTacName]
-    modifyEnv (markMeta · duperRuleTacName)
-    addAndCompile $ Declaration.defnDecl duperRuleTacDecl
-    let duperRuleTacStx ← `(Aesop.rule_expr| ($(mkIdent duperRuleTacName)))
-    let addAutoUnsafeRule ←
-      `(Aesop.tactic_clause| (add unsafe $(Syntax.mkNatLit configOptions.aesopDuperPriority):num% tactic $duperRuleTacStx))
-    -- Building `grindRuleTacStx`
-    let grindRuleTacVal ← mkAppM `HammerCore.grindSingleRuleTac #[q($grindPremiseNames)]
-    let grindRuleTacName := mkPrivateName (← getEnv) `instantiatedGrindRuleTac
-    let grindRuleTacDecl :=
-      mkDefinitionValEx grindRuleTacName [] ruleTacType grindRuleTacVal
-        ReducibilityHints.opaque DefinitionSafety.safe [grindRuleTacName]
-    modifyEnv (markMeta · grindRuleTacName)
-    addAndCompile $ Declaration.defnDecl grindRuleTacDecl
-    let grindRuleTacStx ← `(Aesop.rule_expr| ($(mkIdent grindRuleTacName)))
-    let addGrindUnsafeRule ←
-      `(Aesop.tactic_clause| (add unsafe $(Syntax.mkNatLit configOptions.aesopGrindPriority):num% tactic $grindRuleTacStx))
-    -- Building `smtRuleTacStx`
-    let smtHints ← smtPremises.mapM (fun n => `(Smt.Tactic.smtHintElem| $n:term))
-    let (_, elabedSmtHints) ←
-      try
-        -- `Smt.Tactic.elabHints` can yield the error: "failed to elaborate eliminator, expected type is not available". Lean-SMT's internal
-        -- filter should handle this, but if it doesn't it is better to silently pass nothing to Lean-SMT than to throw an error.
-        Smt.Tactic.elabHints (← `(Smt.Tactic.smtHints| [$(smtHints),*]))
-      catch _ =>
-        trace[hammer.debug] "{decl_name%} :: Failed to elab smt hints: {smtHints}, passing zero hints to Lean-SMT"
-        pure ({}, #[])
-    let smtHintTypes ← elabedSmtHints.mapM (fun h => Meta.inferType h)
-    let smtHintTypesAndStx : List (Expr × Syntax) := List.zip smtHintTypes.toList $ smtPremises.toList.map (fun t => t.raw)
-    let smtRuleTacVal ← mkAppM `HammerCore.Smt.smtSingleRuleTac #[q($smtHintTypesAndStx), q($includeLCtx), q($configOptions)]
-    let smtRuleTacName := mkPrivateName (← getEnv) `instantiatedSmtRuleTac
-    let smtRuleTacDecl :=
-      mkDefinitionValEx smtRuleTacName [] ruleTacType smtRuleTacVal
-        ReducibilityHints.opaque DefinitionSafety.safe [smtRuleTacName]
-    modifyEnv (markMeta · smtRuleTacName)
-    addAndCompile $ Declaration.defnDecl smtRuleTacDecl
-    let smtRuleTacStx ← `(Aesop.rule_expr| ($(mkIdent smtRuleTacName)))
-    let addSmtUnsafeRule ←
-      `(Aesop.tactic_clause| (add unsafe $(Syntax.mkNatLit configOptions.aesopSmtPriority):num% tactic $smtRuleTacStx))
-    -- Calling Aesop with the set of subprocedures determined by `configOptions`
-    match configOptions.disableDuper, configOptions.disableGrind, configOptions.disableSmt with
-    | true, true, true => Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs*))
-    | true, true, false => Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs* $addSmtUnsafeRule))
-    | true, false, true => Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs* $addGrindUnsafeRule))
-    | true, false, false => Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs* $addGrindUnsafeRule $addSmtUnsafeRule))
-    | false, true, true => Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs* $addAutoUnsafeRule))
-    | false, true, false => Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs* $addAutoUnsafeRule $addSmtUnsafeRule))
-    | false, false, true => Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs* $addAutoUnsafeRule $addGrindUnsafeRule))
-    | false, false, false => Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs* $addAutoUnsafeRule $addGrindUnsafeRule $addSmtUnsafeRule))
+    let mut subprocedures : Array (TSyntax `Aesop.tactic_clause) := #[]
+    -- Building `duperRuleTacStx` and adding it to `subprocedures`
+    if !configOptions.disableDuper then
+      -- `withAllLCtx` is set to `false` in this `collectAssumptions` call because the relevant local context to collect is the
+      -- local context where the Duper subprocedure is called by Aesop, not the top main context where `hammer` is being called
+      let formulas ← withDuperOptions $ collectAssumptions duperPremises false #[]
+      let formulas : Array (Expr × Expr × Array Name × Bool × String) :=
+        -- **TODO** This approach prohibits handling arguments that aren't disambiguated theorem names
+        formulas.filterMap (fun (fact, proof, params, isFromGoal, stxOpt) =>
+          stxOpt.map (fun stx => (fact, proof, params, isFromGoal, stx.raw.getId.toString)))
+      modifyEnv (duperSubprocedureInputExt.setState · (some (formulas, includeLCtx, configOptions)))
+      let duperRuleTacStx ← `(Aesop.rule_expr| ($(mkIdent `_root_.HammerCore.duperSingleRuleTac)))
+      let addAutoUnsafeRule ←
+        `(Aesop.tactic_clause| (add unsafe $(Syntax.mkNatLit configOptions.aesopDuperPriority):num% tactic $duperRuleTacStx))
+      subprocedures := subprocedures.push addAutoUnsafeRule
+    -- Building `grindRuleTacStx` and adding it to `subprocedures`
+    if !configOptions.disableGrind then
+      modifyEnv (grindSubprocedureInputExt.setState · (some grindPremiseNames))
+      let grindRuleTacStx ← `(Aesop.rule_expr| ($(mkIdent `_root_.HammerCore.grindSingleRuleTac)))
+      let addGrindUnsafeRule ←
+        `(Aesop.tactic_clause| (add unsafe $(Syntax.mkNatLit configOptions.aesopGrindPriority):num% tactic $grindRuleTacStx))
+      subprocedures := subprocedures.push addGrindUnsafeRule
+    -- Building `smtRuleTacStx` and adding it to `subprocedures`
+    if !configOptions.disableSmt then
+      let smtHints ← smtPremises.mapM (fun n => `(Smt.Tactic.smtHintElem| $n:term))
+      let (_, elabedSmtHints) ←
+        try
+          -- `Smt.Tactic.elabHints` can yield the error: "failed to elaborate eliminator, expected type is not available". Lean-SMT's internal
+          -- filter should handle this, but if it doesn't it is better to silently pass nothing to Lean-SMT than to throw an error.
+          Smt.Tactic.elabHints (← `(Smt.Tactic.smtHints| [$(smtHints),*]))
+        catch _ =>
+          trace[hammer.debug] "{decl_name%} :: Failed to elab smt hints: {smtHints}, passing zero hints to Lean-SMT"
+          pure ({}, #[])
+      let smtHintTypes ← elabedSmtHints.mapM (fun h => Meta.inferType h)
+      let smtHintTypesAndStx : List (Expr × Syntax) := List.zip smtHintTypes.toList $ smtPremises.toList.map (fun t => t.raw)
+      modifyEnv (smtSubprocedureInputExt.setState · (some (smtHintTypesAndStx, includeLCtx, configOptions)))
+      let smtRuleTacStx ← `(Aesop.rule_expr| ($(mkIdent `_root_.HammerCore.Smt.smtSingleRuleTac)))
+      let addSmtUnsafeRule ←
+        `(Aesop.tactic_clause| (add unsafe $(Syntax.mkNatLit configOptions.aesopSmtPriority):num% tactic $smtRuleTacStx))
+      subprocedures := subprocedures.push addSmtUnsafeRule
+    -- Calling Aesop with `subprocedures`
+    Aesop.evalAesop (← `(tactic| aesop? $addIdentStxs* $subprocedures*))
 
 /-- Runs `Meta.isProof` on `e` and every subterm of `e`. If `Meta.isProof` ever returns `true`,
     then `autoPremiseTypeEligibleAux` returns `false`.
@@ -193,7 +205,8 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
   (userInputTerms premises : Array Term) (includeLCtx : Bool) (configOptions : HammerCore.ConfigurationOptions) : TacticM Unit :=
   withMainContext do
     let premiseFilteringStart ← IO.monoMsNow
-    let mut duperPremises := userInputTerms ++ premises.take configOptions.duperPremises
+    let mut duperPremisesShort : Array Term := #[]
+    let mut duperPremisesLong : Array Term := #[]
     let aesopPremises := userInputTerms ++ premises.take configOptions.aesopPremises
     let grindPremises := userInputTerms ++ premises.take configOptions.grindPremises
     let mut smtPremises := userInputTerms ++ premises.take configOptions.smtPremises
@@ -201,7 +214,10 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
     let mut grindParamStxs : TSyntaxArray `Lean.Parser.Tactic.grindParam := #[]
     let mut grindPremiseNames : Array Name := #[]
     if !configOptions.disableDuper then
-      duperPremises ← duperPremises.filterM autoPremiseEligible -- Duper uses Lean-auto for preprocessing
+      -- Duper uses Lean-auto for preprocessing
+      let eligiblePremises ← premises.filterM autoPremiseEligible
+      duperPremisesShort := userInputTerms ++ eligiblePremises.take configOptions.duperPremisesShort
+      duperPremisesLong := userInputTerms ++ eligiblePremises.take configOptions.duperPremisesLong
     if !configOptions.disableAesop then
       for p in aesopPremises do
         -- **TODO** Add support for terms that aren't just names of premises
@@ -223,16 +239,16 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
       -- disabled) is included.
       let mut parallelTacs : List (TacticM Unit) := []
       if !configOptions.disableAesop then
-        parallelTacs := parallelTacs ++ [runAesopWithSubprocedures duperPremises addIdentStxs grindPremiseNames smtPremises includeLCtx configOptions]
+        parallelTacs := parallelTacs ++ [runAesopWithSubprocedures duperPremisesShort addIdentStxs grindPremiseNames smtPremises includeLCtx configOptions]
         if !configOptions.disableDuper || !configOptions.disableGrind || !configOptions.disableSmt then
           parallelTacs := parallelTacs ++
-            [runAesopWithSubprocedures duperPremises addIdentStxs grindPremiseNames smtPremises includeLCtx
+            [runAesopWithSubprocedures duperPremisesShort addIdentStxs grindPremiseNames smtPremises includeLCtx
               {configOptions with disableDuper := true, disableGrind := true, disableSmt := true}]
       if !configOptions.disableDuper then
         if configOptions.preprocessing == .aesop then -- `runDuper` shouldn't be run with Aesop preprocessing
-          parallelTacs := parallelTacs ++ [runDuper stxRef simpLemmas duperPremises includeLCtx {configOptions with preprocessing := .no_preprocessing}]
+          parallelTacs := parallelTacs ++ [runDuper stxRef simpLemmas duperPremisesLong includeLCtx {configOptions with preprocessing := .no_preprocessing}]
         else
-          parallelTacs := parallelTacs ++ [runDuper stxRef simpLemmas duperPremises includeLCtx configOptions]
+          parallelTacs := parallelTacs ++ [runDuper stxRef simpLemmas duperPremisesLong includeLCtx configOptions]
       if !configOptions.disableGrind then
         parallelTacs := parallelTacs ++ [evalTactic (← `(tactic| grind? [$grindParamStxs,*]))]
       if !configOptions.disableSmt then
@@ -260,10 +276,10 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
       | true, false, true, true =>
         if hammer.singleTacticParallel.get (← getOptions) then
           tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
-            runDuper stxRef simpLemmas duperPremises includeLCtx configOptions
+            runDuper stxRef simpLemmas duperPremisesLong includeLCtx configOptions
           ]
         else
-          runSingularTactic (runDuper stxRef simpLemmas duperPremises includeLCtx configOptions)
+          runSingularTactic (runDuper stxRef simpLemmas duperPremisesLong includeLCtx configOptions)
       | true, true, true, false =>
         if hammer.singleTacticParallel.get (← getOptions) then
           tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
@@ -274,10 +290,10 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
       | false, _, _, _ =>
         if hammer.singleTacticParallel.get (← getOptions) then
           tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
-            runAesopWithSubprocedures duperPremises addIdentStxs grindPremiseNames smtPremises includeLCtx configOptions
+            runAesopWithSubprocedures duperPremisesShort addIdentStxs grindPremiseNames smtPremises includeLCtx configOptions
           ]
         else
-          runSingularTactic (runAesopWithSubprocedures duperPremises addIdentStxs grindPremiseNames smtPremises includeLCtx configOptions)
+          runSingularTactic (runAesopWithSubprocedures duperPremisesShort addIdentStxs grindPremiseNames smtPremises includeLCtx configOptions)
       | true, true, true, true => throwError "Erroneous invocation of hammer: At least one of Aesop, Duper, Grind, and Lean-SMT must be enabled."
       | _, _, _, _ => throwError "Erroneous invocation of hammer: Aesop or parallelism is needed to enable more than one of Duper, Grind, and SMT."
 
@@ -289,7 +305,7 @@ def evalHammerWithArgs : Tactic
   let goal ← getMainGoal
   let userInputTerms : Array Term := userInputTerms
   let configOptions ← parseConfigOptions configOptions
-  let autoPremises := if configOptions.disableDuper then 0 else configOptions.duperPremises
+  let autoPremises := if configOptions.disableDuper then 0 else max configOptions.duperPremisesShort configOptions.duperPremisesLong
   let aesopPremises := if configOptions.disableAesop then 0 else configOptions.aesopPremises
   let grindPremises := if configOptions.disableGrind then 0 else configOptions.grindPremises
   let smtPremises := if configOptions.disableSmt then 0 else configOptions.smtPremises
diff --git a/README.md b/README.md
index 8c17b17..0429af2 100644
--- a/README.md
+++ b/README.md
@@ -101,7 +101,8 @@ Each of the `options` supplied to `hammer` have the form `option := value` and a
 - `disableSmt`: Can be set to `true` or `false` (default `false`). This option is used to remove the Lean-SMT pipeline (which involves calling Lean-auto and the Lean cvc5 FFI).
 - `preprocessing`: Can be set to `aesop`, `simp_target`, `simp_all`, or `no_preprocessing` (default `aesop`). This option determines whether the initial goal is first processed by `aesop`, `simp`, `simp_all`, or none of these. This option can only be set to a value other than `aesop` if `disableAesop` is set to `true`, and must be set to `aesop` if `disableAesop` is set to `false`.
 - `aesopPremises`: Can be set to any Nat (default 32). This option determines the number of lemmas from premise selection that are passed to Aesop as unsafe rules.
-- `duperPremises`: Can be set to any Nat (default 16). This option determines the number of lemmas from premise selection that are passed to Lean-auto, Zipperposition, and Duper.
+- `duperPremisesShort`: Can be set to any Nat (default 16). This option determines the number of lemmas from premise selection that are passed to Lean-auto, Zipperposition, and Duper when called as a subprocedure in Aesop.
+- `duperPremisesLong`: Can be set to any Nat (default 100). This option determines the number of lemmas from premise selection that are passed to Lean-auto, Zipperposition, and Duper when called as an independent procedure.
 - `grindPremises`: Can be set to any Nat (default 100). This option determines the number of lemmas from premise selection that are passed to Grind.
 - `smtPremises`: Can be set to any Nat (default 16). This option determines the number of lemmas from premise selection that are passed to Lean-SMT.
 - `aesopPremisePriority`: Can be set to any Nat between 0 and 100 (default 20). This option determines the Aesop success priority assigned to each of the lemmas from premise selection when passed to Aesop as unsafe rules. See [Aesop's README](https://github.com/leanprover-community/aesop) for additional details on the meaning of this success priority.
diff --git a/lake-manifest.json b/lake-manifest.json
index f121644..a7ebcb4 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,24 +1,24 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/ufmg-smite/lean-smt.git",
+ [{"url": "https://github.com/leanprover-community/duper.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1fbc840e0da8b26d23cb3ac9a652635f0d4bb86b",
-   "name": "Smt",
+   "rev": "34f6d228626adf1921f9fb314b0b6bd02c1a82b5",
+   "name": "Duper",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "1fbc840e0da8b26d23cb3ac9a652635f0d4bb86b",
+   "inputRev": "34f6d228626adf1921f9fb314b0b6bd02c1a82b5",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/duper.git",
+  {"url": "https://github.com/ufmg-smite/lean-smt.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "845ba5f42dd94a547ab38eae0ea3b15b9f4ac026",
-   "name": "Duper",
+   "rev": "e87b5c9c88eaf669f3cb85c73a6e75972a9c1018",
+   "name": "Smt",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "e87b5c9c88eaf669f3cb85c73a6e75972a9c1018",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
@@ -41,46 +41,46 @@
    "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
-   "name": "quote4",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.33.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/abdoo8080/lean-cvc5.git",
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7e3365990661b697ccb30e92d6912f4cc6589322",
-   "name": "cvc5",
+   "rev": "eb9c694863439fb55800228bc4c7babe42b089bf",
+   "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "7e33659",
+   "inputRev": "eb9c694863439fb55800228bc4c7babe42b089bf",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/lean-auto.git",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a66de83d4eea7f2811613d7b24ce87cf46bb3ac2",
-   "name": "auto",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "name": "quote4",
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.33.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/batteries",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/abdoo8080/lean-cvc5.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
-   "name": "batteries",
+   "rev": "7e3365990661b697ccb30e92d6912f4cc6589322",
+   "name": "cvc5",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "7e33659",
    "inherited": true,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "Hammer",
  "lakeDir": ".lake",
  "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
index f7cbd7d..f7e9b09 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -13,15 +13,15 @@ name = "«aesop»"
 git = "https://github.com/leanprover-community/aesop"
 rev = "v4.33.0"
 
-[[require]]
-name = "«Duper»"
-git = "https://github.com/leanprover-community/duper.git"
-rev = "v4.33.0"
-
 [[require]]
 name = "«Smt»"
 git = "https://github.com/ufmg-smite/lean-smt.git"
-rev = "1fbc840e0da8b26d23cb3ac9a652635f0d4bb86b" # no_mathlib branch
+rev = "e87b5c9c88eaf669f3cb85c73a6e75972a9c1018" # no_mathlib branch
+
+[[require]]
+name = "«Duper»"
+git = "https://github.com/leanprover-community/duper.git"
+rev = "34f6d228626adf1921f9fb314b0b6bd02c1a82b5"
 
 [[lean_lib]]
 name = "Hammer"