diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean
index f71205c..f7dd7fc 100644
--- a/Duper/Tactic.lean
+++ b/Duper/Tactic.lean
@@ -7,7 +7,7 @@ open Duper
 open ProverM
 open Lean.Parser
 
-initialize 
+initialize
   registerTraceClass `TPTP_Testing
   registerTraceClass `Print_Proof
   registerTraceClass `ProofReconstruction
@@ -195,7 +195,7 @@ partial def mkClauseProof : List Clause → PRM Expr
     -- Now `parents[i] : info.proof.parents[i].toForallExpr`, for all `i`
     let instC := c.instantiateLevelParamsArray c.paramNames req
     let instC ← instC.mapMUpdateType (fun e => Core.transform e PRM.matchSkolem)
-    runMetaAsPRM <| do 
+    runMetaAsPRM <| do
       trace[ProofReconstruction] (
         m!"Reconstructing proof for #{info.number} " ++
         m!": {instC.paramNames} ↦ {req} @ {instC}, Rule Name: {info.proof.ruleName}"
@@ -256,14 +256,14 @@ def applyProof (state : ProverM.State) : TacticM Unit := do
 /-- Produces definional equations for a recursor `recVal` such as
 
   `@Nat.rec m z s (Nat.succ n) = s n (@Nat.rec m z s n)`
-  
+
   The returned list contains one equation
   for each constructor, a proof of the equation, and the contained level
   parameters. -/
 def addRecAsFact (recVal : RecursorVal): TacticM (List (Expr × Expr × Array Name)) := do
   let some (.inductInfo indVal) := (← getEnv).find? recVal.getInduct
     | throwError "Expected inductive datatype: {recVal.getInduct}"
-      
+
   let expr := mkConst recVal.name (recVal.levelParams.map Level.param)
   let res ← forallBoundedTelescope (← inferType expr) recVal.getMajorIdx fun xs _ => do
     let expr := mkAppN expr xs
@@ -274,7 +274,7 @@ def addRecAsFact (recVal : RecursorVal): TacticM (List (Expr × Expr × Array Na
         let expr := mkApp expr ctor
         let some redExpr ← reduceRecMatcher? expr
           | throwError "Could not reduce recursor application: {expr}"
-        let redExpr ← Core.betaReduce redExpr -- TODO: The prover should be able to beta-reduce!
+        let redExpr ← Core.betaReduce redExpr
         let eq ← mkEq expr redExpr
         let proof ← mkEqRefl expr
         return (← mkForallFVars ys eq, ← mkLambdaFVars ys proof)
@@ -289,32 +289,38 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
   | `($id:ident) =>
     let some expr ← Term.resolveId? id
       | throwError "Unknown identifier {id}"
-
-    match (← getEnv).find? expr.constName! with
-    | some (.recInfo val) =>
-      let facts ← addRecAsFact val
-      let facts ← facts.mapM fun (fact, proof, paramNames) => do
-        return (← instantiateMVars fact, ← instantiateMVars proof, paramNames)
-      return facts.toArray
-    | some (.defnInfo defval) =>
-      let term := defval.value
-      let type ← Meta.inferType term
-      let sort ← Meta.reduce (← Meta.inferType type) true true false
-      -- If the fact is of sort `Prop`, add itself as a fact
-      let mut ret := #[]
-      if sort.isProp then
-        ret := ret.push (← elabFactAux stx)
-      -- Generate definitional equation for the fact
-      if let some eqns ← getEqnsFor? expr.constName! (nonRec := true) then
-        ret := ret.append (← eqns.mapM fun eq => do elabFactAux (← `($(mkIdent eq))))
-      return ret
-    | some (.axiomInfo _)  => return #[← elabFactAux stx]
-    | some (.thmInfo _)    => return #[← elabFactAux stx]
-    | some (.opaqueInfo _) => throwError "Opaque constants cannot be provided as facts"
-    | some (.quotInfo _)   => throwError "Quotient constants cannot be provided as facts"
-    | some (.inductInfo _) => throwError "Inductive types cannot be provided as facts"
-    | some (.ctorInfo _)   => throwError "Constructors cannot be provided as facts"
-    | none => throwError "Unknown constant {expr.constName!}"
+    match expr with
+    | .const exprConstName _ =>
+      match (← getEnv).find? exprConstName with
+      | some (.recInfo val) =>
+        let facts ← addRecAsFact val
+        let facts ← facts.mapM fun (fact, proof, paramNames) => do
+          return (← instantiateMVars fact, ← instantiateMVars proof, paramNames)
+        return facts.toArray
+      | some (.defnInfo defval) =>
+        let term := defval.value
+        let type ← Meta.inferType term
+        let sort ← Meta.reduce (← Meta.inferType type) true true false
+        -- If the fact is of sort `Prop`, add itself as a fact
+        let mut ret := #[]
+        if sort.isProp then
+          ret := ret.push (← elabFactAux stx)
+        -- 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))))
+        return ret
+      | some (.axiomInfo _)  => return #[← elabFactAux stx]
+      | some (.thmInfo _)    => return #[← elabFactAux stx]
+      | some (.opaqueInfo _) => throwError "Opaque constants cannot be provided as facts"
+      | some (.quotInfo _)   => throwError "Quotient constants cannot be provided as facts"
+      | some (.inductInfo _) => throwError "Inductive types cannot be provided as facts"
+      | some (.ctorInfo _)   => throwError "Constructors cannot be provided as facts"
+      | none                 => throwError "Unknown constant {id}"
+    | .fvar exprFVarId =>
+      match (← getLCtx).find? exprFVarId with
+      | some _ => return #[← elabFactAux stx]
+      | none => throwError "Unknown fvar {id}"
+    | _ => throwError "Unknown identifier {id}"
   | _ => return #[← elabFactAux stx]
 where elabFactAux (stx : Term) : TacticM (Expr × Expr × Array Name) :=
   -- elaborate term as much as possible and abstract any remaining mvars:
@@ -327,22 +333,27 @@ where elabFactAux (stx : Term) : TacticM (Expr × Expr × Array Name) :=
     let paramNames := abstres.paramNames
     return (← inferType e, e, paramNames)
 
-def collectAssumptions (facts : Array Term) : TacticM (List (Expr × Expr × Array Name)) := do
+def collectAssumptions (facts : Array Term) (withAllLCtx : Bool) (goalDecls : Array LocalDecl) : TacticM (List (Expr × Expr × Array Name)) := do
   let mut formulas := []
-  -- Load all local decls:
-  for fVarId in (← getLCtx).getFVarIds do
-    let ldecl ← Lean.FVarId.getDecl fVarId
-    unless ldecl.isAuxDecl ∨ not (← instantiateMVars (← inferType ldecl.type)).isProp do
-      let ldecltype ← preprocessFact (← instantiateMVars ldecl.type)
-      formulas := (ldecltype, ← mkAppM ``eq_true #[mkFVar fVarId], #[]) :: formulas
-  -- load user-provided facts
-  for facts in ← facts.mapM elabFact do
-    for (fact, proof, params) in facts do
+  if withAllLCtx then -- Load all local decls
+    for fVarId in (← getLCtx).getFVarIds do
+      let ldecl ← Lean.FVarId.getDecl fVarId
+      unless ldecl.isAuxDecl ∨ not (← instantiateMVars (← inferType ldecl.type)).isProp do
+        let ldecltype ← preprocessFact (← instantiateMVars ldecl.type)
+        formulas := (ldecltype, ← mkAppM ``eq_true #[mkFVar fVarId], #[]) :: 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], #[]) :: 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) :: formulas
       else
-        throwError "invalid fact for duper, proposition expected {indentExpr fact}"
+        throwError "Invalid fact {factStx} for duper. Proposition expected"
   return formulas
 
 def collectedAssumptionToMessageData : Expr × Expr × Array Name → MessageData
@@ -452,55 +463,57 @@ def unfoldDefinitions (formulas : List (Expr × Expr × Array Name)) : MetaM (Li
 /-- Entry point for calling duper. Facts should consist of lemmas supplied by the user, instanceMaxHeartbeats should indicate how many
     heartbeats duper should run for before timing out (if instanceMaxHeartbeats is set to 0, then duper will run until it is timed out
     by the Core `maxHeartbeats` option). -/
-def runDuper (facts : Syntax.TSepArray `term ",") (instanceMaxHeartbeats : Nat) : TacticM ProverM.State := withNewMCtxDepth do
-  let formulas ← collectAssumptions facts.getElems
-  let formulas ← unfoldDefinitions formulas
-  trace[Meta.debug] "Formulas from collectAssumptions: {Duper.ListToMessageData formulas collectedAssumptionToMessageData}"
-  /- `collectAssumptions` should not be wrapped by `withoutModifyingCoreEnv` because new definitional equations might be
-      generated during `collectAssumptions` -/
-  withoutModifyingCoreEnv <| do
-    -- Add the constant `skolemSorry` to the environment
-    let skSorryName ← addSkolemSorry
-    let (_, state) ←
-      ProverM.runWithExprs (ctx := {}) (s := {instanceMaxHeartbeats := instanceMaxHeartbeats, skolemSorryName := skSorryName})
-        ProverM.saturateNoPreprocessingClausification
-        formulas
-    return state
+def runDuper (facts : Syntax.TSepArray `term ",") (withAllLCtx : Bool) (goalDecls : Array LocalDecl)
+  (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
+  withNewMCtxDepth do
+    let formulas ← collectAssumptions facts.getElems withAllLCtx goalDecls
+    let formulas ← unfoldDefinitions formulas
+    trace[Meta.debug] "Formulas from collectAssumptions: {Duper.ListToMessageData formulas collectedAssumptionToMessageData}"
+    /- `collectAssumptions` should not be wrapped by `withoutModifyingCoreEnv` because new definitional equations might be
+        generated during `collectAssumptions` -/
+    withoutModifyingCoreEnv <| do
+      -- Add the constant `skolemSorry` to the environment
+      let skSorryName ← addSkolemSorry
+      let (_, state) ←
+        ProverM.runWithExprs (ctx := {}) (s := {instanceMaxHeartbeats := instanceMaxHeartbeats, skolemSorryName := skSorryName})
+          ProverM.saturateNoPreprocessingClausification
+          formulas
+      return state
 
 /-- Default duper instance (does not modify any options except inhabitationReasoning if specified) -/
-def runDuperInstance0 (facts : Syntax.TSepArray `term ",") (inhabitationReasoning : Option Bool)
-  (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
+def runDuperInstance0 (facts : Syntax.TSepArray `term ",") (withAllLCtx : Bool) (goalDecls : Array LocalDecl)
+  (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
   match inhabitationReasoning with
-  | none => runDuper facts instanceMaxHeartbeats
-  | some b => withOptions (fun o => o.set `inhabitationReasoning b) $ runDuper facts instanceMaxHeartbeats
+  | none => runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
+  | some b => withOptions (fun o => o.set `inhabitationReasoning b) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
 
 /-- Runs duper with selFunction 4 (which corresponds to Zipperposition's default selection function) -/
-def runDuperInstance1 (facts : Syntax.TSepArray `term ",") (inhabitationReasoning : Option Bool)
-  (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
+def runDuperInstance1 (facts : Syntax.TSepArray `term ",") (withAllLCtx : Bool) (goalDecls : Array LocalDecl)
+  (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
   match inhabitationReasoning with
-  | none => withOptions (fun o => o.set `selFunction 4) $ runDuper facts instanceMaxHeartbeats
-  | some b => withOptions (fun o => (o.set `selFunction 4).set `inhabitationReasoning b) $ runDuper facts instanceMaxHeartbeats
+  | none => withOptions (fun o => o.set `selFunction 4) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
+  | some b => withOptions (fun o => (o.set `selFunction 4).set `inhabitationReasoning b) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
 
 /-- Runs duper with selFunction 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel) -/
-def runDuperInstance2 (facts : Syntax.TSepArray `term ",") (inhabitationReasoning : Option Bool)
-  (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
+def runDuperInstance2 (facts : Syntax.TSepArray `term ",") (withAllLCtx : Bool) (goalDecls : Array LocalDecl)
+  (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
   match inhabitationReasoning with
-  | none => withOptions (fun o => o.set `selFunction 11) $ runDuper facts instanceMaxHeartbeats
-  | some b => withOptions (fun o => (o.set `selFunction 11).set `inhabitationReasoning b) $ runDuper facts instanceMaxHeartbeats
+  | none => withOptions (fun o => o.set `selFunction 11) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
+  | some b => withOptions (fun o => (o.set `selFunction 11).set `inhabitationReasoning b) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
 
 /-- Runs duper with selFunction 12 (which corresponds to E's SelectCQIPrecWNTNp and Zipperposition's e_sel2) -/
-def runDuperInstance3 (facts : Syntax.TSepArray `term ",") (inhabitationReasoning : Option Bool)
-  (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
+def runDuperInstance3 (facts : Syntax.TSepArray `term ",") (withAllLCtx : Bool) (goalDecls : Array LocalDecl)
+  (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
   match inhabitationReasoning with
-  | none => withOptions (fun o => o.set `selFunction 12) $ runDuper facts instanceMaxHeartbeats
-  | some b => withOptions (fun o => (o.set `selFunction 12).set `inhabitationReasoning b) $ runDuper facts instanceMaxHeartbeats
+  | none => withOptions (fun o => o.set `selFunction 12) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
+  | some b => withOptions (fun o => (o.set `selFunction 12).set `inhabitationReasoning b) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
 
 /-- Runs duper with selFunction 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3) -/
-def runDuperInstance4 (facts : Syntax.TSepArray `term ",") (inhabitationReasoning : Option Bool)
-  (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
+def runDuperInstance4 (facts : Syntax.TSepArray `term ",") (withAllLCtx : Bool) (goalDecls : Array LocalDecl)
+  (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : TacticM ProverM.State :=
   match inhabitationReasoning with
-  | none => withOptions (fun o => o.set `selFunction 13) $ runDuper facts instanceMaxHeartbeats
-  | some b => withOptions (fun o => (o.set `selFunction 13).set `inhabitationReasoning b) $ runDuper facts instanceMaxHeartbeats
+  | none => withOptions (fun o => o.set `selFunction 13) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
+  | some b => withOptions (fun o => (o.set `selFunction 13).set `inhabitationReasoning b) $ runDuper facts withAllLCtx goalDecls instanceMaxHeartbeats
 
 def printSaturation (state : ProverM.State) : TacticM Unit := do
   trace[Prover.saturate] "Final Active Set: {state.activeSet.toArray}"
@@ -541,8 +554,9 @@ structure ConfigurationOptions where
   portfolioInstance : Option Nat -- None by default (unless portfolioMode is false, in which case, some 0 is default)
   inhabitationReasoning : Option Bool -- None by default
 
-syntax (name := duper) "duper" (ppSpace "[" term,* "]")? (ppSpace "{"Duper.configOption,*,?"}")? : tactic
-syntax (name := duperTrace) "duper?" (ppSpace "[" term,* "]")? (ppSpace "{"Duper.configOption,*,?"}")? : tactic
+syntax duperStar := "*"
+syntax (name := duper) "duper" (ppSpace "[" (duperStar <|> term),* "]")? (ppSpace "{"Duper.configOption,*,?"}")? : tactic
+syntax (name := duperTrace) "duper?" (ppSpace "[" (duperStar <|> term),* "]")? (ppSpace "{"Duper.configOption,*,?"}")? : tactic
 
 macro_rules
 | `(tactic| duper) => `(tactic| duper [] {}) -- Missing both facts and config options
@@ -554,6 +568,27 @@ macro_rules
 | `(tactic| duper? [$facts,*]) => `(tactic| duper? [$facts,*] {}) -- Mising just config options
 | `(tactic| duper? {$configOptions,*}) => `(tactic| duper? [] {$configOptions,*}) -- Missing just facts
 
+/-- 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 [`Lean.Elab.Tactic.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
+  let mut needToRemoveSeparator := false -- If `*` is removed, its comma also needs to be removed to preserve the elemsAndSeps ordering
+  for fact in factsArr do
+    match fact with
+    | `(duperStar| *) =>
+      removedDuperStar := true
+      needToRemoveSeparator := true
+    | _ =>
+      if needToRemoveSeparator then needToRemoveSeparator := false -- Don't push current separator onto newFactsArr
+      else newFactsArr := newFactsArr.push fact
+  if removedDuperStar && needToRemoveSeparator then -- This can occur if `*` was the last or only element of facts
+    return (removedDuperStar, {elemsAndSeps := newFactsArr.pop}) -- Remove the last extra separator in newFactsArr, if it exists
+  else
+    return (removedDuperStar, {elemsAndSeps := newFactsArr})
+
 /-- Determines what configuration options Duper should use based on a (potentially partial) set of configuration options passed in by
     the user. If configuration options are not fully specified, this function gives the following default options:
     - Enables portfolio mode by default unless a portfolio instance is specified
@@ -615,7 +650,7 @@ def portfolioInstanceToConfigOptionStx [Monad m] [MonadError m] [MonadQuotation
 
 /-- Constructs and suggests the syntax for a duper call, for use with `duper?` -/
 def mkDuperCallSuggestion (duperStxRef : Syntax) (origSpan : Syntax) (facts : Syntax.TSepArray `term ",")
-  (portfolioInstance : Nat) (inhabitationReasoning : Option Bool) : TacticM Unit := do
+  (withDuperStar : Bool) (portfolioInstance : Nat) (inhabitationReasoning : Option Bool) : TacticM Unit := do
   let mut configOptionsArr : Array Syntax := #[] -- An Array containing configuration option elements and separators (",")
   let portfolioInstanceStx ← portfolioInstanceToConfigOptionStx portfolioInstance
   configOptionsArr := configOptionsArr.push portfolioInstanceStx
@@ -628,21 +663,28 @@ def mkDuperCallSuggestion (duperStxRef : Syntax) (origSpan : Syntax) (facts : Sy
     configOptionsArr := configOptionsArr.push $ ← `(configOption| inhabitationReasoning := $inhabitationReasoningStx)
 
   let configOptionsStx : Syntax.TSepArray `Duper.configOption "," := {elemsAndSeps := configOptionsArr}
-  let suggestion ←`(tactic| duper [$facts,*] {$configOptionsStx,*})
-  Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
+  if withDuperStar && facts.elemsAndSeps.isEmpty then
+    let suggestion ←`(tactic| duper [*] {$configOptionsStx,*})
+    Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
+  else if withDuperStar then
+    let suggestion ←`(tactic| duper [*, $facts,*] {$configOptionsStx,*})
+    Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
+  else
+    let suggestion ←`(tactic| duper [$facts,*] {$configOptionsStx,*})
+    Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
 
 /-- Implements duper calls when portfolio mode is enabled. If `duperStxInfo` is not none and `runDuperPortfolioMode` succeeds in deriving
     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) -/
-def runDuperPortfolioMode (facts : Syntax.TSepArray `term ",") (configOptions : ConfigurationOptions)
-  (startTime : Nat) (duperStxInfo : Option (Syntax × Syntax)) : TacticM Unit := do
+def runDuperPortfolioMode (facts : Syntax.TSepArray `term ",") (withAllLCtx : Bool) (goalDecls : Array LocalDecl)
+  (configOptions : ConfigurationOptions) (startTime : Nat) (duperStxInfo : Option (Syntax × Syntax)) : TacticM Unit := do
   let maxHeartbeats ← getMaxHeartbeats
   let instances :=
-    #[(0, runDuperInstance0 facts),
-      (1, runDuperInstance1 facts),
-      (2, runDuperInstance2 facts),
-      (3, runDuperInstance3 facts),
-      (4, runDuperInstance4 facts)]
+    #[(0, runDuperInstance0 facts withAllLCtx goalDecls),
+      (1, runDuperInstance1 facts withAllLCtx goalDecls),
+      (2, runDuperInstance2 facts withAllLCtx goalDecls),
+      (3, runDuperInstance3 facts withAllLCtx goalDecls),
+      (4, runDuperInstance4 facts withAllLCtx goalDecls)]
   let numInstances := instances.size
   let maxInstanceHeartbeats := maxHeartbeats / numInstances -- Allocate total heartbeats among all instances
   let mut inhabitationReasoningEnabled : Bool :=
@@ -677,7 +719,7 @@ def runDuperPortfolioMode (facts : Syntax.TSepArray `term ",") (configOptions :
         match duperStxInfo with
         | none => return
         | some (duperStxRef, origSpan) =>
-          mkDuperCallSuggestion duperStxRef origSpan facts duperInstanceNum inhabitationReasoningEnabled
+          mkDuperCallSuggestion duperStxRef origSpan facts withAllLCtx duperInstanceNum inhabitationReasoningEnabled
           return
       else
         -- Attempting to solve this problem with inhabitation reasoning disabled leads to failed proof reconstruction
@@ -695,7 +737,7 @@ def runDuperPortfolioMode (facts : Syntax.TSepArray `term ",") (configOptions :
           match duperStxInfo with
           | none => return
           | some (duperStxRef, origSpan) =>
-            mkDuperCallSuggestion duperStxRef origSpan facts duperInstanceNum inhabitationReasoningEnabled
+            mkDuperCallSuggestion duperStxRef origSpan facts withAllLCtx duperInstanceNum inhabitationReasoningEnabled
             return
         | Result.saturated =>
           -- Since inhabitationReasoning has been enabled, the fact that this instance has been saturated means all instances should saturate
@@ -736,7 +778,7 @@ def runDuperPortfolioMode (facts : Syntax.TSepArray `term ",") (configOptions :
           match duperStxInfo with
           | none => return
           | some (duperStxRef, origSpan) =>
-            mkDuperCallSuggestion duperStxRef origSpan facts duperInstanceNum inhabitationReasoningEnabled
+            mkDuperCallSuggestion duperStxRef origSpan facts withAllLCtx duperInstanceNum inhabitationReasoningEnabled
             return
         | Result.saturated =>
           -- Since inhabitationReasoning has been enabled, the fact that this instance has been saturated means all instances should saturate
@@ -748,15 +790,37 @@ def runDuperPortfolioMode (facts : Syntax.TSepArray `term ",") (configOptions :
     | Result.unknown => continue -- Instance ran out of time
   throwError "Prover ran out of time before solving the goal"
 
+/-- When `duper` is called, the first thing the tactic does is call the tactic `intros; apply Classical.byContradiction _; intro`.
+    Even when `*` is not included in the duper invocation (meaning the user does not want duper to collect all the facts in the
+    local context), it is necessary to include the negated goal. This negated goal may take the form of arbitrarily many
+    declarations in the local context if the `duper` is asked to solve a goal of the form `p1 → p2 → p3 → ... pn`. So to ensure
+    that `duper` is able to see the whole original goal, `getGoalDecls` compares the local context before calling
+    `intros; apply Classical.byContradiction _; intro` and after calling `intros; apply Classical.byContradiction _; intro`. The
+    local declarations that are part of the latter lctx but not the former are considered goal decls and are to be returned so that
+    Duper can know to collect them in `collectAssumptions`.-/
+def getGoalDecls (lctxBeforeIntros : LocalContext) (lctxAfterIntros : LocalContext) : Array LocalDecl := Id.run do
+  let mut goalDecls := #[]
+  for declOpt in lctxAfterIntros.decls do
+    match declOpt with
+    | none => continue
+    | some decl =>
+      if lctxBeforeIntros.contains decl.fvarId then continue
+      else goalDecls := goalDecls.push decl
+  return goalDecls
+
 @[tactic duper]
 def evalDuper : Tactic
 | `(tactic| duper [$facts,*] {$configOptions,*}) => withMainContext do
   let startTime ← IO.monoMsNow
   let configOptions ← parseConfigOptions configOptions
+  let (factsContainsDuperStar, facts) := removeDuperStar facts
+  let lctxBeforeIntros ← getLCtx
   Elab.Tactic.evalTactic (← `(tactic| intros; apply Classical.byContradiction _; intro))
   withMainContext do
+    let lctxAfterIntros ← getLCtx
+    let goalDecls := getGoalDecls lctxBeforeIntros lctxAfterIntros
     if configOptions.portfolioMode then
-      runDuperPortfolioMode facts configOptions startTime none
+      runDuperPortfolioMode facts factsContainsDuperStar goalDecls configOptions startTime none
     else
       let portfolioInstance ←
         match configOptions.portfolioInstance with
@@ -764,11 +828,11 @@ def evalDuper : Tactic
         | none => throwError "parseConfigOptions error: portfolio mode is disabled and no portfolio instance is specified"
       let state ←
         match portfolioInstance with
-        | 0 => runDuperInstance0 facts configOptions.inhabitationReasoning 0
-        | 1 => runDuperInstance1 facts configOptions.inhabitationReasoning 0
-        | 2 => runDuperInstance2 facts configOptions.inhabitationReasoning 0
-        | 3 => runDuperInstance3 facts configOptions.inhabitationReasoning 0
-        | 4 => runDuperInstance4 facts configOptions.inhabitationReasoning 0
+        | 0 => runDuperInstance0 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
+        | 1 => runDuperInstance1 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
+        | 2 => runDuperInstance2 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
+        | 3 => runDuperInstance3 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
+        | 4 => runDuperInstance4 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
         | _ => throwError "Portfolio instance {portfolioInstance} not currently defined. Please choose instance 0-4"
       match state.result with
       | Result.contradiction => do
@@ -787,10 +851,14 @@ def evalDuperTrace : Tactic
 | `(tactic| duper?%$duperStxRef [$facts,*] {$configOptions,*}) => withMainContext do
   let startTime ← IO.monoMsNow
   let configOptions ← parseConfigOptions configOptions
+  let (factsContainsDuperStar, facts) := removeDuperStar facts
+  let lctxBeforeIntros ← getLCtx
   Elab.Tactic.evalTactic (← `(tactic| intros; apply Classical.byContradiction _; intro))
   withMainContext do
+    let lctxAfterIntros ← withMainContext getLCtx
+    let goalDecls := getGoalDecls lctxBeforeIntros lctxAfterIntros
     if configOptions.portfolioMode then
-      runDuperPortfolioMode facts configOptions startTime (some (duperStxRef, ← getRef))
+      runDuperPortfolioMode facts factsContainsDuperStar goalDecls configOptions startTime (some (duperStxRef, ← getRef))
     else
       let portfolioInstance ←
         match configOptions.portfolioInstance with
@@ -798,11 +866,11 @@ def evalDuperTrace : Tactic
         | none => throwError "parseConfigOptions error: portfolio mode is disabled and no portfolio instance is specified"
       let state ←
         match portfolioInstance with
-        | 0 => runDuperInstance0 facts configOptions.inhabitationReasoning 0
-        | 1 => runDuperInstance1 facts configOptions.inhabitationReasoning 0
-        | 2 => runDuperInstance2 facts configOptions.inhabitationReasoning 0
-        | 3 => runDuperInstance3 facts configOptions.inhabitationReasoning 0
-        | 4 => runDuperInstance4 facts configOptions.inhabitationReasoning 0
+        | 0 => runDuperInstance0 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
+        | 1 => runDuperInstance1 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
+        | 2 => runDuperInstance2 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
+        | 3 => runDuperInstance3 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
+        | 4 => runDuperInstance4 facts factsContainsDuperStar goalDecls configOptions.inhabitationReasoning 0
         | _ => throwError "Portfolio instance {portfolioInstance} not currently defined. Please choose instance 0-4"
       match state.result with
       | Result.contradiction => do
@@ -810,7 +878,7 @@ def evalDuperTrace : Tactic
         printProof state
         applyProof state
         IO.println s!"Constructed proof. Time: {(← IO.monoMsNow) - startTime}ms"
-        mkDuperCallSuggestion duperStxRef (← getRef) facts portfolioInstance configOptions.inhabitationReasoning
+        mkDuperCallSuggestion duperStxRef (← getRef) facts factsContainsDuperStar portfolioInstance configOptions.inhabitationReasoning
       | Result.saturated =>
         printSaturation state
         throwError "Prover saturated."
@@ -827,7 +895,7 @@ def evalDuperNoTiming : Tactic
 | `(tactic| duper_no_timing [$facts,*]) => withMainContext do
   Elab.Tactic.evalTactic (← `(tactic| intros; apply Classical.byContradiction _; intro))
   withMainContext do
-    let state ← runDuper facts 0
+    let state ← runDuper facts true #[] 0 -- I don't bother computing goalDecls here since I set withAllLCtx to true anyway
     match state.result with
     | Result.contradiction => do
       IO.println s!"Contradiction found"
@@ -841,4 +909,4 @@ def evalDuperNoTiming : Tactic
     | Result.unknown => throwError "Prover was terminated."
 | _ => throwUnsupportedSyntax
 
-end Lean.Elab.Tactic
\ No newline at end of file
+end Lean.Elab.Tactic
diff --git a/Duper/Tests/bugs.lean b/Duper/Tests/bugs.lean
index d96798a..ca32c6f 100644
--- a/Duper/Tests/bugs.lean
+++ b/Duper/Tests/bugs.lean
@@ -33,11 +33,11 @@ end Color2
 set_option inhabitationReasoning true in
 set_option trace.typeInhabitationReasoning.debug true in
 tptp ITP023_3 "../TPTP-v8.0.0/Problems/ITP/ITP023_3.p"
-  by duper -- Fails due to error: unknown free variable '_uniq.6173142'
+  by duper [*] -- Fails due to error: unknown free variable '_uniq.6173142'
 
 set_option inhabitationReasoning false in
 tptp ITP023_3' "../TPTP-v8.0.0/Problems/ITP/ITP023_3.p"
-  by duper -- Det timeout
+  by duper [*] -- Det timeout
 
 -- Diagnosis of the above test
 /-
@@ -61,22 +61,6 @@ example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) :=
 This might be a more viable example to investigate because of how much shorter it is
 -/
 
--- Bug 6
-set_option inhabitationReasoning true in
-example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) :=
-  by duper -- Fails because we currently do not infer that A is nonempty from the fact that B and B → A are nonempty
-
-set_option inhabitationReasoning true in
-example : ∃ (A : Type) (B : A → Type) (f : ∀ (a : A), B a) (x : A), (f x = f x) = True :=
-  by duper
-
--- Diagnosis of the above two examples
-/-
-This isn't so much a bug as it is a limitation in the current approach to inhabitation reasoning. The extent of reasoning Duper
-currently performs in attempting to determine whether a type is inhabited is limited. The two above examples provide somewhat
-more complicated cases in which Duper is not able to infer that a particular type is inhabited
--/
-
 -- Bug 7
 example (a : α) (as : List α) : [] ≠ a :: as :=
   by duper [List.rec] -- Error: AppBuilder for 'mkAppOptM', result contains metavariables @List.nil
diff --git a/Duper/Tests/fail_group.lean b/Duper/Tests/fail_group.lean
index a2f7705..d1e4b11 100644
--- a/Duper/Tests/fail_group.lean
+++ b/Duper/Tests/fail_group.lean
@@ -15,4 +15,4 @@ theorem cubeisom
   (cube_injective : ∀ x y, cube x = cube y → x = y)
   (cube_surjective : ∀ x, ∃ y, x = cube y)
   (cube_homomorphism : ∀ x y, cube (mult x y) = mult (cube x) (cube y))
-  : ∀ x y, mult x y = mult y x := by duper
+  : ∀ x y, mult x y = mult y x := by duper [*]
diff --git a/Duper/Tests/fail_lattice.lean b/Duper/Tests/fail_lattice.lean
index ed21fc7..0cd571a 100644
--- a/Duper/Tests/fail_lattice.lean
+++ b/Duper/Tests/fail_lattice.lean
@@ -22,4 +22,4 @@ theorem mod_lattice1
   (ModLatA : ∀ a x b, U (A a b) (A x b) = A (U (A a b) x) b)
   (a b c : L)
   (Hyp : A a (U b c) = U (A a b) (A a c))
-  : U a (A b c) = A (U a b) (U a c) := by duper
\ No newline at end of file
+  : U a (A b c) = A (U a b) (U a c) := by duper [*]
\ No newline at end of file
diff --git a/Duper/Tests/fail_tests.lean b/Duper/Tests/fail_tests.lean
index 6cb2e74..f34b74a 100644
--- a/Duper/Tests/fail_tests.lean
+++ b/Duper/Tests/fail_tests.lean
@@ -24,7 +24,7 @@ f (f (f a)) = d ∨ f (f b) = d ∨ f c = d)
 (h2 : f (f (f (f a1))) ≠ d)
 (h2 : f (f (f a)) ≠ d)
 (h3 : f (f b) ≠ d)
-: False := by duper
+: False := by duper [*]
 
 -- Tests where duper should time out
 -- This example is intended to test duper's ability of
diff --git a/Duper/Tests/ffffa.lean b/Duper/Tests/ffffa.lean
index 63eb685..cede179 100644
--- a/Duper/Tests/ffffa.lean
+++ b/Duper/Tests/ffffa.lean
@@ -15,4 +15,4 @@ a
 ))))))))))
 ))))))))))
 )))))))))) = a
- := by duper
\ No newline at end of file
+ := by duper [h]
\ No newline at end of file
diff --git a/Duper/Tests/fluidSupTests.lean b/Duper/Tests/fluidSupTests.lean
index 5f22de8..b3e1a81 100644
--- a/Duper/Tests/fluidSupTests.lean
+++ b/Duper/Tests/fluidSupTests.lean
@@ -1,6 +1,5 @@
 import Duper.Tactic
 import Duper.TPTP
-import Duper.DUnif.DApply
 
 set_option trace.Saturate.debug true
 set_option trace.Rule.fluidSup true
@@ -9,14 +8,14 @@ set_option trace.Rule.fluidSup true
 
 theorem supWithLambdasEx13 (a b c : t) (f g : t → t) (h : t → t → t)
   (eq1 : f a = c) (eq2 : ∀ y : t → t, h (y b) (y a) ≠ h (g (f b)) (g c)) : False :=
-  by duper
+  by duper [*] {portfolioInstance := 0}
 
 theorem supWithLambdasEx14 (a b c d : t) (f g : t → t)
   (eq1 : f a = c) (eq2 : f b = d) (eq3 : ∀ y : t → t, g c ≠ y a ∨ g d ≠ y b) : False :=
-  by duper
+  by duper [*]
 
 -- Note: Since the original example was untyped, it's possible that the types I chose for this don't work. So I don't
 -- put too much stock in it if this continues to fail. But I do think that supWithLambda13 should be solvable
 theorem supWithLambdaEx15 (a c : t) (f g : t → t) (h : t → ((t → t) → t → t) → t)
   (eq1 : f a = c) (eq2 : ∀ y : (t → t) → t → t, h (y (fun x => g (f x)) a) y ≠ h (g c) (fun w x => w x)) :
-  False := by duper
\ No newline at end of file
+  False := by duper [*]
\ No newline at end of file
diff --git a/Duper/Tests/group.lean b/Duper/Tests/group.lean
index 35ff84a..6c3555f 100644
--- a/Duper/Tests/group.lean
+++ b/Duper/Tests/group.lean
@@ -13,25 +13,25 @@ axiom exists_left_inv : ∀ (x : G), ∃ (y : G), x ⬝ y = e
 noncomputable instance : Inhabited G := ⟨e⟩
 
 theorem e_mul : e ⬝ x = x :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem exists_right_inv (x : G) : ∃ (y : G), y ⬝ x = e :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem left_neutral_unique (x : G) : (∀ y, x ⬝ y = y) → x = e :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem right_neutral_unique (x : G) : (∀ y, y ⬝ x = y) → x = e :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem right_inv_unique (x y z : G) (h : x ⬝ y = e) (h : x ⬝ z = e) : y = z :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [*, mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem left_inv_unique (x y z : G) (h : y ⬝ x = e) (h : z ⬝ x = e) : y = z :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [*, mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 noncomputable def sq (x : G) := x ⬝ x
 
 theorem sq_mul_sq_eq_e (x y : G) (h_comm : ∀ a b, a ⬝ b = b ⬝ a) (h : x ⬝ y = e) :
   sq x ⬝ sq y = e :=
-by duper [sq, mul_assoc, mul_e]
\ No newline at end of file
+by duper [h_comm, h, sq, mul_assoc, mul_e] {portfolioInstance := 0}
diff --git a/Duper/Tests/group2.lean b/Duper/Tests/group2.lean
index 7d4c86a..0882061 100644
--- a/Duper/Tests/group2.lean
+++ b/Duper/Tests/group2.lean
@@ -1,6 +1,6 @@
 import Duper.Tactic
 
-class Group (G : Type) where 
+class Group (G : Type) where
 (one : G)
 (inv : G → G)
 (mul : G → G → G)
@@ -19,25 +19,30 @@ noncomputable instance : Inhabited G := ⟨one⟩
 theorem test : x ⬝ one = x :=
 by duper [Group.mul_one]
 
+/- Note: Currently, includeHoist must be disabled in order for duper to solve these problems. In the future,
+   portfolio mode should be enhanced so that at least one portfolio instance enables hoist rules and most
+   portfolio instances disable hoist rules. -/
+set_option includeHoistRules false
+
 theorem exists_right_inv (x : G) : inv x ⬝ x = one :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 theorem left_neutral_unique (x : G) : (∀ y, x ⬝ y = y) → x = one :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 theorem right_neutral_unique (x : G) : (∀ y, y ⬝ x = y) → x = one :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 theorem right_inv_unique (x y z : G) (h : x ⬝ y = one) (h : x ⬝ z = one) : y = z :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [*, Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 theorem left_inv_unique (x y z : G) (h : y ⬝ x = one) (h : z ⬝ x = one) : y = z :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [*, Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 noncomputable def sq := x ⬝ x
 
 theorem sq_mul_sq_eq_e (h_comm : ∀ (a b : G), a ⬝ b = b ⬝ a) (h : x ⬝ y = one) :
   sq x ⬝ sq y = one :=
-by duper [sq, Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [h, h_comm, sq, Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
-end Group
\ No newline at end of file
+end Group
diff --git a/Duper/Tests/lastAsylum.lean b/Duper/Tests/lastAsylum.lean
index 5332f5e..15fc260 100644
--- a/Duper/Tests/lastAsylum.lean
+++ b/Duper/Tests/lastAsylum.lean
@@ -37,14 +37,14 @@ example
 theorem asylum_one
   (h1 : Sane Jones ↔ Doctor Smith)
   (h2 : Sane Smith ↔ ¬ Doctor Jones)
-  : ∃ x : Inhab, (¬ Sane (x) ∧ Doctor (x)) ∨ (Sane (x) ∧ ¬ Doctor (x)) := by duper
+  : ∃ x : Inhab, (¬ Sane (x) ∧ Doctor (x)) ∨ (Sane (x) ∧ ¬ Doctor (x)) := by duper [h1, h2]
 
 #print axioms asylum_one
 
 theorem asylum_seven
   (h1 : Sane A ↔ ¬ Sane B)
   (h2 : Sane B ↔ Doctor A)
-  : (¬ Sane A ∧ Doctor A) ∨ (Sane A ∧ ¬ Doctor A) := by duper
+  : (¬ Sane A ∧ Doctor A) ∨ (Sane A ∧ ¬ Doctor A) := by duper [*]
 
 #print axioms asylum_seven
 
@@ -57,7 +57,7 @@ theorem asylum_nine
   (h4 : A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D) :
   (∃ x : Inhab, Sane x ∧ ¬ Doctor x) ∨
   (∃ x : Inhab, ∃ y : Inhab, x ≠ y ∧ (¬ Sane x) ∧ Doctor x ∧ (¬ Sane y) ∧ Doctor y) :=
-  by duper
+  by duper [*]
 
 #print axioms asylum_nine
-#print asylum_nine
\ No newline at end of file
+#print asylum_nine
diff --git a/Duper/Tests/morebugs.lean b/Duper/Tests/morebugs.lean
deleted file mode 100644
index 228dd06..0000000
--- a/Duper/Tests/morebugs.lean
+++ /dev/null
@@ -1,50 +0,0 @@
-import Duper.Tactic
-
-namespace Seq
-
-instance : Neg Nat := sorry
-
-def even_fun (f : Nat → Nat) := ∀ x, f (-x) = f x
-
-instance : Add (Nat → Nat) := (⟨fun f g x => f x + g x⟩ :  Add (Nat → Nat))
-
-theorem add_apply (f g : Nat → Nat) (x : Nat) : (f + g) x = f x + g x := sorry
-
-example (f g : Nat → Nat) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by
-  unfold even_fun at *
-  duper [add_apply f g]
-
--- This should be fairly easy, too, by unfolding even_fun as above.
--- example (f g : Nat → Nat) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by
---   duper [even_fun, add_apply f g]
-
-example (f g : Nat → Nat) (hf : ∀ x, f (-x) = f x) : even_fun f := by
-  unfold even_fun at *
-  exact hf
-
--- This should be very easy
-example (f g : Nat → Nat) (hf : ∀ x, f (-x) = f x) : even_fun f := by
-  duper [even_fun]
-
-example (mq : Nat) (ef : (Nat → Nat) → Prop)
-        (f : Nat → Nat)
-        (h₁ : ∀ a, f a = f (-a))
-        (h₂ : ∀ (a : Nat → Nat), ef a = True ∨ a (-mq) ≠ a mq)
-        (h₃ : ef f = False) : False := by duper
-
-example (mq : (Nat → Nat) → Nat) (ef : (Nat → Nat) → Prop)
-        (n : Nat → Nat)
-        (f : Nat → Nat)
-        (h₁ : ∀ a, f a = f (- a))
-        (h₂ : ∀ (a : Nat → Nat), ef a = True ∨ a (- (mq a)) ≠ a (mq a))
-        (h₃ : ef f = False) : False := by duper
-
-example (mq : (Nat → Nat) → Nat) (ef : (Nat → Nat) → Prop)
-        (n : Nat → Nat)
-        (f : Nat → Nat)
-        (h₁ : ∀ a, f a = f (n a))
-        (h₂ : ∀ (a : Nat → Nat), ef a = True ∨ a (n (mq a)) ≠ a (mq a))
-        (h₃ : ef f = False) : False := by duper
-
-
-end Seq
diff --git a/Duper/Tests/test_boolSimp.lean b/Duper/Tests/test_boolSimp.lean
index 9b43559..84662f5 100644
--- a/Duper/Tests/test_boolSimp.lean
+++ b/Duper/Tests/test_boolSimp.lean
@@ -5,112 +5,112 @@ import Duper.TPTP
 set_option trace.Rule.boolSimp true
 
 theorem boolSimpRule1Test (p : Prop) (h : (p ∨ p ∨ p ∨ p) = q) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule2Test (p q : Prop) (h : (¬p ∨ p) = q) : q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule2SymTest (p q : Prop) (h : (p ∨ ¬p) = q) : q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule3Test (p q : Prop) (h : (p ∨ True) = q) : q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule3SymTest (p q : Prop) (h : (True ∨ p) = q) : q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule4Test (p q : Prop) (h : (p ∨ False) = (q ∨ False)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule4SymTest (p q : Prop) (h : (False ∨ p) = (False ∨ q)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule5Test (p q : Prop) (h : p = (q = q)) : p :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule6Test (p q : Prop) (h : (p = True) = (q = True)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule6SymTest (p q : Prop) (h : (True = p) = (True = q)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule7Test (p q : Prop) (h : p = Not False) : p :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule8Test (p : Prop) (h : (p ∧ p ∧ p ∧ p) = q) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule9Test (p q : Prop) (h : (¬p ∧ p) = q) : ¬q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule9SymTest (p q : Prop) (h : (p ∧ ¬p) = q) : ¬q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule10Test (p q : Prop) (h : (p ∧ True) = q) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule10SymTest (p q : Prop) (h : (True ∧ p) = q) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule11Test (p q : Prop) (h : (p ∧ False) = q) : ¬q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule11SymTest (p q : Prop) (h : (False ∧ p) = q) : ¬q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule12Test (p q : Prop) (h : p = (q ≠ q)) : ¬p :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule13Test (p q : Prop) (h : (p = False) = (q = False)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule13SymTest (p q : Prop) (h : (False = p) = (False = q)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule14Test (p q : Prop) (h : p = Not True) : ¬p :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule15Test (p q : Prop) (h : (¬¬p) = q) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule16Test (p q : Prop) (h : (True → p) = q) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule17Test (p q : Prop) (h : (False → p) = q) : q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule18Test (p q : Prop) (h : (p → False) = (q → False)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule19Test (p q : Prop) (h : (p → True) = q) : q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule19Test2 (α) (q : Prop) (h : (∀ _ : α, True) = q) : q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule20Test (p q : Prop) (h : (p → ¬p) = (q → ¬q)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule21Test (p q : Prop) (h : (¬p → p) = (¬q → q)) : p = q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule22Test (p q : Prop) (h : (p → p) = q) : q :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule23Test (f : Prop → Prop) (q : Prop) (hq : q) (h : (∀ p : Prop, f p) = q) : f True :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule24Test (f : Prop → Prop) (q : Prop) (hq : q) (h : (∃ p : Prop, f p) = q) : (f True) ∨ (f False) :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule25Test (p q r : Prop) (h : (p → ¬q → q → p → False) = r) : r :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule26Test (a b c shared x y z r : Prop) (h : (a → b → shared → c → (x ∨ shared ∨ y ∨ z)) = r) : r :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule27Test (a b c shared x y z r : Prop) (h : ((a ∧ b ∧ shared ∧ c) → (x ∨ shared ∨ y ∨ z)) = r) : r :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule28Test (p q r : Prop) (h : (p ↔ r) = (q ↔ r)) : p = q :=
-  by duper
+  by duper [*]
diff --git a/Duper/Tests/test_higher_order.lean b/Duper/Tests/test_higher_order.lean
index a2ef131..f8df538 100644
--- a/Duper/Tests/test_higher_order.lean
+++ b/Duper/Tests/test_higher_order.lean
@@ -3,7 +3,7 @@ import Duper.TPTP
 
 set_option maxHeartbeats 20000
 tptp NUM020_1 "../TPTP-v8.0.0/Problems/NUM/NUM020^1.p"
-  by duper
+  by duper [*]
 
 tptp AGT033 "../TPTP-v8.0.0/Problems/AGT/AGT033^1.p" by sorry
 
@@ -20,7 +20,7 @@ example
   (plus mult : ((Nat → Nat) → Nat → Nat) → ((Nat → Nat) → Nat → Nat) → ((Nat → Nat) → Nat → Nat))
   (hmult_ax: mult = fun M N X Y => M (N X) Y)
   (hthree_ax: three = fun X Y => X (X (X Y)))
-  (hthm: ¬∃ N, mult N three = three) : False := by duper
+  (hthm: ¬∃ N, mult N three = three) : False := by duper [*]
 
 -- Ex27 is example 27 from https://matryoshka-project.github.io/pubs/hosup_report.pdf
 set_option trace.Print_Proof true in
@@ -29,4 +29,4 @@ set_option trace.ProofReconstruction true in
 theorem ex27 (t : Type) (g : Prop → t) (h : t → t) (A B : t)
   (eq1 : A ≠ B)
   (eq2 : ∀ y : t → t, h (y B) ≠ h (g False) ∨ h (y A) ≠ h (g True)) : False :=
-  by duper
+  by duper [*]
diff --git a/Duper/Tests/test_inhabitationReasoning.lean b/Duper/Tests/test_inhabitationReasoning.lean
index 955d45a..d158844 100644
--- a/Duper/Tests/test_inhabitationReasoning.lean
+++ b/Duper/Tests/test_inhabitationReasoning.lean
@@ -8,28 +8,28 @@ theorem optionTest1 (t : Type) (f : Option t) : ∃ x : Option t, True := by dup
 
 theorem optionTest2 : ∀ t : Type, ∃ x : Option t, True := by duper
 
-theorem nonemptyHypTest (t : Type) (eh : Nonempty t = True ∧ True) (h : ∀ x : t, False ≠ False) : False := by duper
+theorem nonemptyHypTest (t : Type) (eh : Nonempty t = True ∧ True) (h : ∀ x : t, False ≠ False) : False := by duper [eh, h]
 
 -- Needs to synthesize Inhabited (Fin x)
 theorem finTest (x : Nat) (f : Fin x → Fin x)
-  (h : ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper
+  (h : ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper [h]
 
 -- Needs to synthesize Inhabited (Fin default)
 theorem finTest2
-  (h : ∀ x : Nat, ∃ f : Fin x → Fin x, ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper
+  (h : ∀ x : Nat, ∃ f : Fin x → Fin x, ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper [h]
 
 -- Needs to synthesize Inhabited (Fin [anonymous]) (pretty sure [anonymous] is a skolem var)
 theorem finTest3 (mult_Nats : ∃ y : Nat, y ≠ 0)
-  (h : ∀ x : Nat, x ≠ 0 → ∃ f : Fin x → Fin x, ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper
+  (h : ∀ x : Nat, x ≠ 0 → ∃ f : Fin x → Fin x, ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper [h]
 
 -- Needs to synthesize Inhabited person
 set_option trace.ProofReconstruction true in
 theorem barber_paradox1 {person : Type} {shaves : person → person → Prop}
-  (h : ∃ b : person, ∀ p : person, (shaves b p ↔ (¬ shaves p p))) : False := 
-  by duper
+  (h : ∃ b : person, ∀ p : person, (shaves b p ↔ (¬ shaves p p))) : False :=
+  by duper [h]
 
-theorem letDecBug {t : Type} (h : (∀ p : t, p = p) = False) : False := 
-  by duper
+theorem letDecBug {t : Type} (h : (∀ p : t, p = p) = False) : False :=
+  by duper [h]
 
 -- Interesting type inhabited examples (they require more advanced reasoning about type inhabitation)
 example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) :=
diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean
index ee22b49..bb69217 100644
--- a/Duper/Tests/test_regression.lean
+++ b/Duper/Tests/test_regression.lean
@@ -28,7 +28,7 @@ theorem test0000 (one : Nat) (isZero : Nat → Prop) (div mul add : Nat → Nat
 (div_self : ∀ x, ¬ isZero x → div x x = one)
 (add_mul : ∀ (x y z : Nat), mul (add x y) z = add (mul x z) (mul y z))
 (div_def : ∀ (x y : Nat), ¬ isZero y → div x y = mul x (inv y)) :
-∀ (x y : Nat), ¬ isZero y → div (add x y) y = add (div x y) one := by duper
+∀ (x y : Nat), ¬ isZero y → div (add x y) y = add (div x y) one := by duper [*]
 #print axioms test0000
 
 -- Contradiction found. Time: 647ms
@@ -48,39 +48,39 @@ f (f (f a)) = d ∨ f (f b) = d ∨ f c = d)
 (h2 : f (f (f a)) ≠ d)
 (h3 : f (f b) ≠ d)
 (h4 : f c ≠ d)
-: False := by duper
+: False := by duper [*]
 
 #print test0018
 
 theorem test00008
 (div_self : ∀ x, x ≠ zero → mul x (inv x) = one)
 (add_mul : ∀ (x y z : Nat), mul (add x y) z = add (mul x z) (mul y z)) :
-∀ (x y : Nat), y ≠ zero → mul (add x y) (inv y) = add (mul x (inv y)) one := by duper
+∀ (x y : Nat), y ≠ zero → mul (add x y) (inv y) = add (mul x (inv y)) one := by duper [*]
 
 
 theorem test00008'
 (div_self : ∀ x, x ≠ zero → div x x = one)
 (add_mul : ∀ (x y z : Nat), mul (add x y) z = add (mul x z) (mul y z))
 (div_def : ∀ (x y : Nat), y ≠ zero → div x y = mul x (inv y)) :
-∀ (x y : Nat), y ≠ zero → mul (add x y) (inv y) = add (mul x (inv y)) one := by duper
+∀ (x y : Nat), y ≠ zero → mul (add x y) (inv y) = add (mul x (inv y)) one := by duper [*]
 
 theorem test 
 (div_self : ∀ x, div x x = one)
 (add_mul : ∀ (x y z : Nat), mul (add x y) z = add (mul x z) (mul y z))
 (div_def : ∀ (x y : Nat), div x y = mul x (inv y)) :
-∀ (x y : Nat), div (add x y) y = add (div x y) one := by duper
+∀ (x y : Nat), div (add x y) y = add (div x y) one := by duper [*]
 
 -- #print test
 -- #print axioms test
 
 example --(h : ∃ x, x ≠ c ∨ a = b) 
 (h : ¬ ∃ x, x = f a ∨ ∀ x, ∃ y, y = f a ∧ x = b)-- (h :  c = b ∧ a = b) 
-: False := by duper
+: False := by duper [*]
 
 set_option trace.Meta.debug true in
 theorem test00
 (ax1 : a ≠ a ∨ ¬ (∀ x : Nat, x = x) ∨ b ≠ b)
-: False := by duper
+: False := by duper [*]
 
 
 #print test00
@@ -88,20 +88,20 @@ theorem test00
 theorem test0
 (ax1 : f a = b → f c ≠ b)
 (ax2 : ¬ ∃ x, f x ≠ b ∧ c = c)
-: False := by duper
+: False := by duper [*]
 
 #print test0
 
 theorem test1
 (div_self : ∀ x, f x = a)
 (div_self : ∀ x, f x ≠ a)
-: False := by duper
+: False := by duper [*]
 
 #print test1
 
 theorem test1'
 (div_self : ∀ x y z : Nat, f x ≠ f x ∨ g y ≠ g y ∨ h z ≠ h z)
-: False := by duper
+: False := by duper [*]
 
 theorem test2
 : ∀ (x : Nat), x = x := by duper
@@ -118,7 +118,7 @@ theorem puzzle1 {ι : Type} (johanna : ι) (bill : ι) (peanuts : ι)
   (h3 : eats bill peanuts)
   (h4 : alive bill)
   (h5 : ∀ y, alive y → ∀ x, ¬ was_killed_by y x) :
-likes johanna peanuts := by duper
+likes johanna peanuts := by duper [*]
 
 #print puzzle1
 
@@ -143,17 +143,17 @@ theorem test0011 (one : Nat) (div mul add : Nat → Nat → Nat)
 (div_self : ∀ x, div x x = one)
 (add_mul : ∀ (x y z : Nat), mul (add x y) z = add (mul x z) (mul y z))
 (div_def : ∀ (x y : Nat), div x y = mul x (inv y)) :
-∀ (x y : Nat), div (add x y) y = add (div x y) one := by duper
+∀ (x y : Nat), div (add x y) y = add (div x y) one := by duper [*]
 #print test0011
 #print axioms test0011
 
 --###############################################################################################################################
 --Clausifying prop inequality tests
 theorem propInequalityTest1 {p : Prop} {q : Prop} (h : p ≠ q) : p ∨ q :=
-  by duper
+  by duper [*]
 
 theorem propInequalityTest2 {p : Prop} {q : Prop} (h : p ≠ q) : ¬p ∨ ¬q :=
-  by duper
+  by duper [*]
 
 #print propInequalityTest1 -- clause 4 uses clausify_prop_inequality2
 #print axioms propInequalityTest1
@@ -163,10 +163,10 @@ theorem propInequalityTest2 {p : Prop} {q : Prop} (h : p ≠ q) : ¬p ∨ ¬q :=
 --###############################################################################################################################
 --Iff clausification tests
 theorem iffClausificationTest1 {p : Prop} {q : Prop} (h : p ↔ q) : (p → q) ∧ (q → p) :=
-  by duper
+  by duper [h]
 
 theorem iffClausificationTest2 {p : Prop} {q : Prop} (h : ¬(p ↔ q)) : (p → ¬q) ∧ (q → ¬p) :=
-  by duper
+  by duper [h]
 
 #print iffClausificationTest1
 #print iffClausificationTest2
@@ -184,23 +184,23 @@ List of problems pertaining to the barber paradox:
 set_option trace.Meta.debug true in
 theorem barber_paradox1 {person : Type} {person_inhabited : Inhabited person} {shaves : person → person → Prop}
   (h : ∃ b : person, ∀ p : person, (shaves b p ↔ (¬ shaves p p))) : False := 
-  by duper
+  by duper [*]
 
 theorem barber_paradox2 {person : Type} {shaves : person → person → Prop} {b : person}
   (h : ∀ p : person, (shaves b p ↔ (¬shaves p p))) : False := 
-  by duper
+  by duper [*]
 
 theorem barber_paradox3 {person : Type} {shaves : person → person → Prop} {b : person}
   (h1 : ∀ p : person, (shaves b p ↔ (¬ shaves p p))) (h2 : shaves b b ∨ ¬ shaves b b) : False :=
-  by duper
+  by duper [h1]
 
 theorem barber_paradox4 {person : Type} {person_inhabited : Inhabited person} {shaves : person → person → Prop}
   (h : ∃ b : person, ∀ p : person, (shaves b p → (¬ shaves p p)) ∧ ((¬ shaves p p) → shaves b p)) : False :=
-  by duper
+  by duper [*]
 
 theorem barber_paradox5 {person : Type} {shaves : person → person → Prop} {b : person}
   (h : shaves b b ↔ ¬shaves b b) : False :=
-  by duper
+  by duper [*]
 
 #print barber_paradox1
 #print axioms barber_paradox1
@@ -214,20 +214,19 @@ theorem barber_paradox_inline0 {person : Type} {person_inhabited : Inhabited per
   (h : ∃ b : person, ∀ p : person, (shaves b p → (¬ shaves p p)) ∧ ((¬ shaves p p) → shaves b p)) : False := by
   cases h with
   | intro b h' =>
-    duper
+    duper [h']
 
 theorem barber_paradox_inline1 {person : Type} {shaves : person → person → Prop}
   (h : ∃ b : person, ∀ p : person, (shaves b p ↔ (¬ shaves p p))) : False := by
   cases h with
   | intro b h' =>
-    duper
+    duper [*]
 
 theorem barber_paradox_inline2 {person : Type} {shaves : person → person → Prop}
   (h : ∃ b : person, ∀ p : person, (shaves b p ↔ (¬ shaves p p))) : False := by
   cases h with
   | intro b h' =>
-    have h'_b := h' b
-    duper
+    duper [h' b]
 
 theorem barber_paradox_inline3 {person : Type} {shaves : person → person → Prop}
   (h : ∃ b : person, ∀ p : person, (shaves b p ↔ (¬ shaves p p))) : False := by
@@ -235,7 +234,7 @@ theorem barber_paradox_inline3 {person : Type} {shaves : person → person → P
   | intro b h' =>
     have h'_b := h' b
     clear h'
-    duper
+    duper [h'_b]
 
 #print barber_paradox_inline0
 #print axioms barber_paradox_inline0
@@ -254,10 +253,10 @@ theorem syntacticTautologyDeletionTest {t : Type} (a : t) (b : t) (c : t)
 -/
 
 theorem elimResolvedLitTest {t : Type} (a : t) (b : t) (c : t)
-  (h : a = b ∨ a = c ∨ b ≠ b) : a = b ∨ a = c := by duper
+  (h : a = b ∨ a = c ∨ b ≠ b) : a = b ∨ a = c := by duper [h]
 
 theorem elimResolvedLitTest2 {t : Type} (a : t) (b : t) (c : t)
-  (h : b ≠ b ∨ a = b ∨ a ≠ a ∨ a = c ∨ b ≠ b ∨ c ≠ c) : a = b ∨ a = c := by duper
+  (h : b ≠ b ∨ a = b ∨ a ≠ a ∨ a = c ∨ b ≠ b ∨ c ≠ c) : a = b ∨ a = c := by duper [h]
 
 theorem elimResolvedLitTest3 {t : Type} (a : t) (b : t) (c : t)
   (h : a ≠ a ∨ b ≠ b ∨ c ≠ c) : a = a ∨ b = b ∨ c = c := by duper
@@ -272,15 +271,15 @@ theorem elimResolvedLitTest3 {t : Type} (a : t) (b : t) (c : t)
 
 theorem equalityFactoringTest1 {α : Type} (s t u v : α) 
   (h1 : s = t ∨ s = v) : t ≠ v ∨ s = v :=
-  by duper
+  by duper [*]
 
 theorem equalityFactoringTest2 {α : Type} (s t u v : α) 
   (h1 : s = t ∨ u = s) : t ≠ u ∨ u = s :=
-  by duper
+  by duper [*]
 
 theorem equalityFactoringTest3 {α : Type} (s t v : α)
   (h1 : s = t ∨ t = v) : s ≠ v ∨ t = v :=
-  by duper
+  by duper [*]
 
 /-
   Note to self: The only difference between equalityFactoringTest3 and equalityFactoringTest4 is the order of s t and v as arguments. This fact influences
@@ -289,11 +288,11 @@ theorem equalityFactoringTest3 {α : Type} (s t v : α)
 -/
 theorem equalityFactoringTest4 {α : Type} (v t s : α)
   (h1 : s = t ∨ t = v) : s ≠ v ∨ t = v :=
-  by duper
+  by duper [*]
 
 theorem equalityFactoringTest5 {α : Type} (s t u v : α)
   (h1 : s = t ∨ u = t) : s ≠ u ∨ u = t :=
-  by duper
+  by duper [*]
 
 #print equalityFactoringTest1 -- This proof uses equality_factoring_soundness1 (in the commit where this test is added, it is used in clause 5)
 #print equalityFactoringTest2 -- This proof uses equality_factoring_soundness2 (in the commit where this test is added, it is used in clause 13)
@@ -310,17 +309,17 @@ theorem equalityFactoringTest5 {α : Type} (s t u v : α)
 --###############################################################################################################################
 -- This test previously failed due to a bug in how we removed clauses
 theorem removeClausesTest {α : Type} [Inhabited α] (x y : α) (c : α → Prop)
-  (h1 : ∀ a b : α, a = b) : c x = c y := by duper
+  (h1 : ∀ a b : α, a = b) : c x = c y := by duper [*]
 
 --###############################################################################################################################
 theorem COM002_2_test (state : Type) (follows fails : state → state → Prop) (p3 p6 : state)
   (h0 : ∀ (Start_state Goal_state : state), ¬(fails Goal_state Start_state ∧ follows Goal_state Start_state))
-  (h1 : follows p6 p3) : ¬fails p6 p3 := by duper
+  (h1 : follows p6 p3) : ¬fails p6 p3 := by duper [*]
 
 theorem COM002_2_test2 (state label statement : Type) (p8 : state) (loop : label) (goto : label → statement)
   (follows fails : state → state → Prop) (labels : label → state → Prop) (has : state → statement → Prop)
   (h0 : ∀ s1 s2 : state, ∀ l1 : label, ¬(fails s1 s2 ∧ has s2 (goto l1) ∧ labels l1 s1))
-  (h1 : has p8 (goto loop)) : ∀ s1 : state, ¬(fails s1 p8 ∧ labels loop s1) := by duper
+  (h1 : has p8 (goto loop)) : ∀ s1 : state, ¬(fails s1 p8 ∧ labels loop s1) := by duper [*]
 
 /- Saturates because the goal is "False" rather than anything coherent, but the final active set is:
 [fails p3 #0 = True ∨ fails #0 p3 = True,
@@ -341,23 +340,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"
-  by duper
+  by duper [*]
 
 #print axioms KRS003_1
 
 tptp PUZ012_1 "../TPTP-v8.0.0/Problems/PUZ/PUZ012_1.p"
-  by duper
+  by duper [*]
 
 #print PUZ012_1
 --###############################################################################################################################
 -- Tests that (in the current commit at least) use positive simplify reflect
 set_option trace.Rule.simplifyReflect true in
 tptp NUN004_5 "../TPTP-v8.0.0/Problems/NUN/NUN004_5.p"
-  by duper {portfolioInstance := 0} -- Runs out of time if run in portfolio mode
+  by duper [*] {portfolioInstance := 0} -- Runs out of time if run in portfolio mode
 
 set_option trace.Rule.simplifyReflect true in
 tptp ITP209_2 "../TPTP-v8.0.0/Problems/ITP/ITP209_2.p"
-  by duper
+  by duper [*]
 
 --###############################################################################################################################
 -- Example from super
@@ -372,15 +371,15 @@ by duper
 --###############################################################################################################################
 -- Miscellaneous tests
 example (h : ∀ a, ∀ b, ∀ c, ∃ d, f a = b ∧ g c = d) :
-  ∀ a, ∀ b, ∀ c, ∃ d, f a = b ∧ g c = d := by duper
+  ∀ a, ∀ b, ∀ c, ∃ d, f a = b ∧ g c = d := by duper [*]
 
 -- Checks that duper can handle existential quantification where the variable doesn't appear in the body
-example (h : ∃ y : Nat, False) : False := by duper
-example (h : (∃ y : Nat, True) = False) : False := by duper
+example (h : ∃ y : Nat, False) : False := by duper [*]
+example (h : (∃ y : Nat, True) = False) : False := by duper [*]
 
 -- Checks that duper can handle universal quantification where the variable doesn't appear in the body
-example (h : ∀ y : Nat, False) : False := by duper
-example (h : (∀ y : Nat, True) = False) : False := by duper
+example (h : ∀ y : Nat, False) : False := by duper [*]
+example (h : (∀ y : Nat, True) = False) : False := by duper [*]
 
 -- Checks β/η reduction
 example : (let f := (fun x => (x, x)); (fun x => f x) 1) = (1, 1) := by duper
@@ -400,11 +399,11 @@ theorem assoc_test : Nat.add (Nat.add x y) z = Nat.add x (Nat.add y z) := by dup
 
 set_option trace.Print_Proof true in
 theorem eqHoistTest (a b : Nat) (f : Prop → Prop) (h : f (a = b)) : ∃ p : Prop, f p :=
-  by duper
+  by duper [h]
 
 set_option trace.Print_Proof true in
 theorem neHoistTest (a b : Nat) (f : Prop → Prop) (h : f (a ≠ b)) : ∃ p : Prop, f p :=
-  by duper
+  by duper [*]
 
 set_option trace.Print_Proof true in
 theorem existsHoistTest1 (f : Prop → Nat) : f (∃ (x : Nat), x = Nat.zero) = f True := by duper
@@ -415,15 +414,15 @@ theorem existsHoistTest2 (f : Prop → Nat) : ∀ y : Nat, f (∃ x : Nat, x = y
 
 set_option trace.Print_Proof true in
 set_option trace.Rule.existsHoist true in
-theorem existsHoistTest3 (f : Prop → Nat) (h : ∀ z : Nat, ∀ y : Nat, f (∃ x : Nat, (x = y ∧ x = z)) ≠ f True) : False := by duper
+theorem existsHoistTest3 (f : Prop → Nat) (h : ∀ z : Nat, ∀ y : Nat, f (∃ x : Nat, (x = y ∧ x = z)) ≠ f True) : False := by duper [*]
 
 set_option trace.Print_Proof true in
 theorem existsHoistTest4 (f : Prop → Nat)
-  (h : ∀ x : Nat, f (∃ y : Nat, ∀ a : Nat, ∃ b : Nat, x = y ↔ a = b) ≠ f True) : False := by duper
+  (h : ∀ x : Nat, f (∃ y : Nat, ∀ a : Nat, ∃ b : Nat, x = y ↔ a = b) ≠ f True) : False := by duper [*]
 
 set_option trace.Print_Proof true in
 theorem existsHoistTest5 (f : Prop → Nat)
-  (h : ∀ x : Nat, ∃ y : Nat, f ((∃ z : Nat, z = x) ∧ (∃ z : Nat, z = y)) ≠ f True) : False := by duper
+  (h : ∀ x : Nat, ∃ y : Nat, f ((∃ z : Nat, z = x) ∧ (∃ z : Nat, z = y)) ≠ f True) : False := by duper [*]
 
 set_option trace.Print_Proof true in
 set_option trace.Rule.existsHoist true in
@@ -438,19 +437,19 @@ theorem forallHoistTest1 (f : Prop → Nat) : f (∀ (x : Nat), x ≠ Nat.zero)
 
 set_option trace.Print_Proof true in
 theorem forallHoistTest2 (f : Prop → Nat)
-  (h : ∀ x : Nat, f (∀ y : Nat, x = y) ≠ f False) : False := by duper
+  (h : ∀ x : Nat, f (∀ y : Nat, x = y) ≠ f False) : False := by duper [*]
 
 set_option trace.Print_Proof true in
 theorem forallHoistTest3 (f : Prop → Nat)
-  (h : ∃ x : Nat, f (∀ y : Nat, x = y) ≠ f False) : False := by duper
+  (h : ∃ x : Nat, f (∀ y : Nat, x = y) ≠ f False) : False := by duper [*]
 
 set_option trace.Print_Proof true in
 theorem forallHoistTest4 (f : Prop → Nat)
-  (h : ∀ x : Nat, ∀ y : Nat, f (∀ z : Nat, x = z ↔ y = z) ≠ f False) : False := by duper
+  (h : ∀ x : Nat, ∀ y : Nat, f (∀ z : Nat, x = z ↔ y = z) ≠ f False) : False := by duper [*]
 
 set_option trace.Print_Proof true in
 theorem forallHoistTest5 (f : Prop → Nat)
-  (h : ∀ x : Nat, ∃ y : Nat, f (∀ z : Nat, x = z ∧ y = z) ≠ f False) : False := by duper
+  (h : ∀ x : Nat, ∃ y : Nat, f (∀ z : Nat, x = z ∧ y = z) ≠ f False) : False := by duper [*]
 
 --###############################################################################################################################
 -- Tests that were previously in bugs.lean
@@ -480,13 +479,13 @@ example : ∃ (A : Type) (B : A → Type) (f : ∀ (a : A), B a) (x : A), (f x =
 example (A : Type) (x : A) : (∃ x : A, x = x) := by duper
 
 example (x : Type u) (f g : Type u → Type v) (H : f = g) : f x = g x :=
-  by duper
+  by duper [*]
 
 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
+  by duper [*]
 
 tptp PUZ137_8 "../TPTP-v8.0.0/Problems/PUZ/PUZ137_8.p"
-  by duper
+  by duper [*]
 
 tptp PUZ031_1_modified "../TPTP-v8.0.0/Problems/PUZ/PUZ031_1.p" by 
   have inhabited_plant : Inhabited plant := sorry
@@ -497,15 +496,15 @@ tptp PUZ031_1_modified "../TPTP-v8.0.0/Problems/PUZ/PUZ031_1.p" by
   have inhabited_wolf : Inhabited wolf := sorry
   have inhabited_animal : Inhabited animal := sorry
   have inhabited_caterpillar : Inhabited caterpillar := sorry
-  duper
+  duper [*]
   -- If these instances are not provided, duper will fail
 
 tptp SEU123 "../TPTP-v8.0.0/Problems/SEU/SEU123+1.p"
-  by duper
+  by duper [*]
 
 set_option trace.Rule.superposition true in
 tptp SEU139 "../TPTP-v8.0.0/Problems/SEU/SEU139+1.p"
-  by duper
+  by duper [*]
 
 --###############################################################################################################################
 -- Tests that were previously in morebugs.lean
@@ -525,10 +524,10 @@ end Axioms
 /- BoolSimp tests -/
 
 theorem boolSimpRule26TestDep₁ (a b y z r : Prop) (dep : a → Prop) (h : ((x : a) → b → dep x → (dep x ∨ y ∨ z)) = r) : r :=
-  by duper
+  by duper [*]
 
 theorem boolSimpRule27TestDep₁ (a b c y z r : Prop) (f : a ∧ b ∧ c → Prop) (h : ((x : a ∧ b ∧ c) → (y ∨ f x ∨ c ∨ z)) = r) : r :=
-  by duper
+  by duper [*]
 
 /- Negative BoolSimp tests -/
 
@@ -553,7 +552,7 @@ end NegativeBoolSimpTests
 
 /- ClauseStreamHeap tests -/
 tptp MGT008 "../TPTP-v8.0.0/Problems/MGT/MGT008+1.p"
-  by duper {portfolioInstance := 0} -- Runs out of time if run in portfolio mode
+  by duper [*] {portfolioInstance := 0} -- Runs out of time if run in portfolio mode
 
 example (f : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat)
   (g : Nat → Nat → Nat → Nat → Nat → Nat)
@@ -585,7 +584,7 @@ example
 -- to show: good size implies good survival chance
 (h4: ¬∀ (X Y P1 P2 S2 T1 T2 : TPTP.iota),
     organization Y T2 → dummy X P1 T1 S2 →
-      goodChance P2) : False := by duper
+      goodChance P2) : False := by duper [*]
 
 -- Universe level tests
 
@@ -641,49 +640,52 @@ instance : Add (Int → Int) := (⟨fun f g x => f x + g x⟩ : Add (Int → Int
 instance : Add (Nat → Nat) := (⟨fun f g x => f x + g x⟩ : Add (Nat → Nat))
 
 example (f : Int → Int) (hf : ∀ x, f (-x) = f x) : even_int_fun f := by -- The goal is the same as hf
-  duper [even_int_fun]
+  duper [hf, even_int_fun]
 
 example (f : Nat → Nat) (hf : ∀ x, f (-x) = f x) : even_nat_fun f := by -- The goal is the same as hf
-  duper [even_nat_fun]
+  duper [hf, even_nat_fun]
 --###############################################################################################################################
 -- Tests duper's ability to derive that types are nonempty
 
 example (p : α → β → Prop) (h : ∀ (x : α), ∃ y, p x y) : ∃ (f : α → β), ∀ x, p x (f x) :=
-  by duper
+  by duper [*]
 
 example (p : α → β → Prop) (h : ∀ (x : α), ∀ (z : Nat), ∃ y, p x y) : ∃ (f : α → β), ∀ x, p x (f x) :=
-  by duper
+  by duper [*]
 
 example (p : α → β → Prop) (h : ∀ (x : α), ∃ (z : Nat), ∃ y, p x y) : ∃ (f : α → β), ∀ x, p x (f x) :=
-  by duper
+  by duper [*]
+
+example (h : Nonempty (α → β)) : (∀ n : Nat, ∀ a : α, ∃ b : β, True) = True :=
+  by duper [h]
 
 example (h : Nonempty (α → β) = True) : (∀ n : Nat, ∀ a : α, ∃ b : β, True) = True :=
-  by duper
+  by duper [*]
 
 example (h : Nonempty (α → β) = True) : ∀ n : Nat, ∀ a : α, ∃ b : β, True :=
-  by duper
+  by duper [h]
 
 example (h : Nonempty ((α → β) → γ)) : ∀ f : α → β, ∃ y : γ, True :=
-  by duper
+  by duper [h]
 
 example (h1 : Nonempty ((α → β) → γ)) (h2 : ∀ x : α, Nonempty β) : ∃ y : γ, true :=
-  by duper
+  by duper [*]
 
 example (h1 : ∀ f : α → β, Nonempty γ) (h2 : ∀ x : α, Nonempty β) : ∃ y : γ, true :=
-  by duper
+  by duper [h1, h2]
 
 example (p : α → β → γ → Prop) (q : α → β → γ) (h : ∀ (x : α) (y : β), p x y (q x y)) :
   ∃ (f : α → β → γ), ∀ x y, p x y (f x y) :=
-  by duper
+  by duper [h]
 
-example (p : Prop) (h : Nonempty p = True) : p := by duper
+example (p : Prop) (h : Nonempty p = True) : p := by duper [*]
 
-example (p : Prop) (h : Nonempty (PProd p α) = True) : p := by duper
+example (p : Prop) (h : Nonempty (PProd p α) = True) : p := by duper [*]
 
-example (p : Prop) (h : Nonempty (PProd α p) = True) : p := by duper
+example (p : Prop) (h : Nonempty (PProd α p) = True) : p := by duper [*]
 
-example (p : Prop) (h : ∃ hp : p, True) : p := by duper
+example (p : Prop) (h : ∃ hp : p, True) : p := by duper [*]
 
-example (h : Nonempty (α × β)) : Nonempty α := by duper
+example (h : Nonempty (α × β)) : Nonempty α := by duper [*]
 
-example (h : Nonempty (α × β)) : Nonempty β := by duper
\ No newline at end of file
+example (h : Nonempty (α × β)) : Nonempty β := by duper [*]
\ No newline at end of file
diff --git a/Duper/Tests/test_universe.lean b/Duper/Tests/test_universe.lean
index f3a5da4..ea93d54 100644
--- a/Duper/Tests/test_universe.lean
+++ b/Duper/Tests/test_universe.lean
@@ -47,4 +47,4 @@ set_option trace.ProofReconstruction true in
 def skuniverse.{u} : ∃ (x : Type u), f x := by
   duper [exftrue]
 
-end UniverseTest
\ No newline at end of file
+end UniverseTest
diff --git a/DuperOnMathlib/DuperOnMathlib/Prime.lean b/DuperOnMathlib/DuperOnMathlib/Prime.lean
index eb78a1b..4f1488c 100644
--- a/DuperOnMathlib/DuperOnMathlib/Prime.lean
+++ b/DuperOnMathlib/DuperOnMathlib/Prime.lean
@@ -10,28 +10,29 @@ namespace Nat
 
 theorem prime_def_lt_DUPER {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1 := by
   have : 2 ≤ p → 0 < p := by intro; linarith
-  duper [Nat.prime_def_lt'', Nat.le_of_dvd, Nat.lt_of_le_of_ne, Nat.lt_irrefl]
+  duper [*, Nat.prime_def_lt'', Nat.le_of_dvd, Nat.lt_of_le_of_ne, Nat.lt_irrefl]
 
 #check Nat.prime_def_lt' -- Reproving this theorem using duper:
 
 theorem prime_def_lt'_DUPER {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p := by
   constructor
   · have : ¬ 2 ≤ 1 := by duper [Nat.two_le_iff]
-    duper [prime_def_lt_DUPER]
+    duper [*, prime_def_lt_DUPER]
   · have : (∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p) →  ∀ m < p, m ∣ p → m = 1
     · duper [Nat.two_le_iff, Nat.not_eq_zero_of_lt, Nat.eq_zero_of_zero_dvd]
-    duper [prime_def_lt_DUPER]
+    duper [*, prime_def_lt_DUPER]
 
 #check prime_def_le_sqrt -- Reproving this theorem using duper:
 
 theorem prime_def_le_sqrt_DUPER' {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬m ∣ p := by
   constructor
-  · have : ∀ m, 2 ≤ m → 1 < m := by intros; linarith 
-    duper [prime_def_lt', sqrt_lt_self, Nat.lt_of_le_of_lt] 
+  · have : ∀ m, 2 ≤ m → 1 < m := by intros; linarith
+    duper [*, prime_def_lt', sqrt_lt_self, Nat.lt_of_le_of_lt]
   · intro h
     rw [prime_def_lt']
     refine ⟨h.1, ?_⟩
-    have h₂ : ∀ m, 2 ≤ m → m < p → m ∣ p → 2 ≤ (p / m) := 
-      by duper [Nat.lt_irrefl, Nat.dvd_iff_div_mul_eq, Nat.mul_zero, Nat.one_mul, two_le_iff]
-    duper [Nat.div_dvd_of_dvd, Nat.dvd_iff_div_mul_eq, le_sqrt, Nat.mul_le_mul_right, Nat.mul_le_mul_left, mul_comm, Nat.le_total]
-
+    have h₂ : ∀ m, 2 ≤ m → m < p → m ∣ p → 2 ≤ (p / m) :=
+      by duper [*, Nat.lt_irrefl, Nat.dvd_iff_div_mul_eq, Nat.mul_zero, Nat.one_mul, two_le_iff]
+    duper
+      [*, Nat.div_dvd_of_dvd, Nat.dvd_iff_div_mul_eq, le_sqrt, Nat.mul_le_mul_right, Nat.mul_le_mul_left, mul_comm, Nat.le_total]
+      {portfolioInstance := 0}
diff --git a/DuperOnMathlib/DuperOnMathlib/Set.lean b/DuperOnMathlib/DuperOnMathlib/Set.lean
index 1f5e3a7..aeb4960 100644
--- a/DuperOnMathlib/DuperOnMathlib/Set.lean
+++ b/DuperOnMathlib/DuperOnMathlib/Set.lean
@@ -25,215 +25,215 @@ set_option selFunction 0 in
 theorem test1a (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 0
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 0
 
 set_option selFunction 1 in
 theorem test1b (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 1
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 1
 
 set_option selFunction 2 in
 theorem test1c (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 2
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 2
 
 set_option selFunction 3 in
 theorem test1d (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 3
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 3
 
 set_option selFunction 4 in
 theorem test1e (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 4
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 4
 
 set_option selFunction 5 in
 theorem test1f (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 5
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 5
 
 set_option selFunction 6 in
 theorem test1g (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 6
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 6
 
 set_option selFunction 7 in
 theorem test1h (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 7
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 7
 
 set_option selFunction 8 in
 theorem test1i (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 8
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 8
 
 set_option selFunction 9 in
 theorem test1j (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
   rw [subset_def] at h -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, subset_def] -- Succeeds with selFunction 9
+  duper [h, mem_inter_iff, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 9
 
 ------------------------------------------------------------------------------------
 set_option selFunction 0 in
 theorem test2a : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Det timeout with selFunction 0
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Det timeout with selFunction 0
 
 set_option selFunction 1 in
 theorem test2b : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 1
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 1
 
 set_option selFunction 2 in
 theorem test2c : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 2
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 2
 
 set_option selFunction 3 in
 theorem test2d : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 3
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 3
 
 set_option selFunction 4 in
 theorem test2e : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 4
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 4
 
 set_option selFunction 5 in
 theorem test2f : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Det timeout with selFunction 5
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Det timeout with selFunction 5
 
 set_option selFunction 6 in
 theorem test2g : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 6
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 6
 
 set_option selFunction 7 in
 theorem test2h : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 7
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 7
 
 set_option selFunction 8 in
 theorem test2i : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 8
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 8
 
 set_option selFunction 9 in
 theorem test2j : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 9
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 9
 
 ------------------------------------------------------------------------------------
 set_option selFunction 0 in
 theorem test3a : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Det timeout with selFunction 0
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Det timeout with selFunction 0
 
 set_option selFunction 1 in
 theorem test3b : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 1
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 1
 
 set_option selFunction 2 in
 theorem test3c : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 2
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 2
 
 set_option selFunction 3 in
 theorem test3d : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 3
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 3
 
 set_option selFunction 4 in
 theorem test3e : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 4
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 4
 
 set_option selFunction 5 in
 theorem test3f : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 5
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 5
 
 set_option selFunction 6 in
 theorem test3g : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 6
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 6
 
 set_option selFunction 7 in
 theorem test3h : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 7
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 7
 
 set_option selFunction 8 in
 theorem test3i : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 8
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 8
 
 set_option selFunction 9 in
 theorem test3j : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_inter_iff, mem_union, subset_def] -- Succeeds with selFunction 9
+  duper [mem_inter_iff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 9
 ------------------------------------------------------------------------------------
 #check mem_diff
 
 set_option selFunction 0 in
 theorem test4a : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 0
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 0
 
 set_option selFunction 1 in
 theorem test4b : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 1
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 1
 
 set_option selFunction 2 in
 theorem test4c : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 2
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 2
 
 set_option selFunction 3 in
 theorem test4d : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 3
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 3
 
 set_option selFunction 4 in
 theorem test4e : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 4
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 4
 
 set_option selFunction 5 in
 theorem test4f : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 5
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 5
 
 set_option selFunction 6 in
 theorem test4g : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 6
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 6
 
 set_option selFunction 7 in
 theorem test4h : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 7
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 7
 
 set_option selFunction 8 in
 theorem test4i : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 8
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 8
 
 set_option selFunction 9 in
 theorem test4j : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rw [subset_def] -- Mimics auto's definition aware preprocessing
-  duper [mem_diff, mem_union, subset_def] -- Succeeds with selFunction 9
+  duper [mem_diff, mem_union, subset_def] {portfolioInstance := 0} -- Succeeds with selFunction 9
 ------------------------------------------------------------------------------------
 #check Set.ext
 
@@ -241,85 +241,84 @@ theorem test4j : (s \ t) \ u ⊆ s \ (t ∪ u) := by
 
 set_option selFunction 0 in
 theorem test6a : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 0
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 0
 
 set_option selFunction 1 in
 theorem test6b : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 1
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 1
 
 set_option selFunction 2 in
 theorem test6c : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 2
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 2
 
 set_option selFunction 3 in
 theorem test6d : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 3
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 3
 
 set_option selFunction 4 in
 theorem test6e : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 4
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 4
 
 set_option selFunction 5 in
 theorem test6f : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 5
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 5
 
 set_option selFunction 6 in
 theorem test6g : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 6
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 6
 
 set_option selFunction 7 in
 theorem test6h : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 7
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 7
 
 set_option selFunction 8 in
 theorem test6i : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 8
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 8
 
 set_option selFunction 9 in
 theorem test6j : s ∩ t = t ∩ s := by
-  duper [Set.ext, mem_inter_iff] -- Det timeout with selFunction 9
+  duper [Set.ext, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 9
 ----------------------------------------------------------------------
 -- Note for this problem: Zipperposition (on default settings) is able to solve this quite quickly,
 -- so it should be much more obtainable than test6
 
 set_option selFunction 0 in
 theorem test7a : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 0
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 0
 
 set_option selFunction 1 in
 theorem test7b : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 1
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 1
 
 set_option selFunction 2 in
 theorem test7c : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 2
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 2
 
 set_option selFunction 3 in
 theorem test7d : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 3
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 3
 
-set_option selFunction 4 in
 theorem test7e : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 4
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 4
 
 set_option selFunction 5 in
 theorem test7f : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 5
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 5
 
 set_option selFunction 6 in
 theorem test7g : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 6
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 6
 
 set_option selFunction 7 in
 theorem test7h : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 7
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 7
 
 set_option selFunction 8 in
 theorem test7i : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 8
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 8
 
 set_option selFunction 9 in
 theorem test7j : s ∩ (s ∪ t) = s := by
-  duper [Set.ext, mem_union, mem_inter_iff] -- Det timeout with selFunction 9
+  duper [Set.ext, mem_union, mem_inter_iff] {portfolioInstance := 0} -- Det timeout with selFunction 9
 
-end
\ No newline at end of file
+end
diff --git a/DuperOnMathlib/lake-manifest.json b/DuperOnMathlib/lake-manifest.json
index cefda32..3fcd80d 100644
--- a/DuperOnMathlib/lake-manifest.json
+++ b/DuperOnMathlib/lake-manifest.json
@@ -1,28 +1,53 @@
-{"version": 4,
+{"version": 6,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "bac7310cc18d6ed292606d26ccb5fb9ffc697c7a",
+    "rev": "57e4e03dd1782a74cf937835bbdb5f90955e4406",
+    "opts": {},
     "name": "mathlib",
-    "inputRev?": "bac7310"}},
+    "inputRev?": "57e4e03dd1782a74cf937835bbdb5f90955e4406",
+    "inherited": false}},
+  {"path": {"opts": {}, "name": "duper", "inherited": false, "dir": "./../"}},
   {"git":
-   {"url": "https://github.com/gebner/quote4",
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "ab21923ce1717d48a8d3d17e77bf6cdd3122eed8",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "opts": {},
     "name": "Qq",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/leanprover-community/aesop",
     "subDir?": null,
-    "rev": "ba61f7fec6174d8c7d2796457da5a8d0b0da44c6",
+    "rev": "9dc4a1097a690216eaa7cf2d2290efd447e60d7a",
+    "opts": {},
     "name": "aesop",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
-   {"url": "https://github.com/leanprover/std4",
+   {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "de7e2a79905a3f87cad1ad5bf57045206f9738c7",
-    "name": "std",
-    "inputRev?": "main"}},
-  {"path": {"name": "duper", "dir": "./../"}}]}
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
+    "subDir?": null,
+    "rev": "5382e38eca1e2537d75d4c4705a9e744424b0037",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.19",
+    "inherited": true}}],
+ "name": "duperOnMathlib"}
diff --git a/DuperOnMathlib/lakefile.lean b/DuperOnMathlib/lakefile.lean
index c0e7c8c..1b32048 100644
--- a/DuperOnMathlib/lakefile.lean
+++ b/DuperOnMathlib/lakefile.lean
@@ -3,7 +3,7 @@ open Lake DSL
 
 package «duperOnMathlib»
 
-require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "bac7310"
+require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "57e4e03dd1782a74cf937835bbdb5f90955e4406"
 require «duper» from "../"
 
 @[default_target]
diff --git a/DuperOnMathlib/lakefile.olean b/DuperOnMathlib/lakefile.olean
new file mode 100644
index 0000000..2641d19
Binary files /dev/null and b/DuperOnMathlib/lakefile.olean differ
diff --git a/DuperOnMathlib/lean-toolchain b/DuperOnMathlib/lean-toolchain
index 04ab6c3..183a307 100644
--- a/DuperOnMathlib/lean-toolchain
+++ b/DuperOnMathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-03
+leanprover/lean4:v4.2.0-rc4