diff --git a/Hammer/Options.lean b/Hammer/Options.lean
index b770ef5..88a710d 100644
--- a/Hammer/Options.lean
+++ b/Hammer/Options.lean
@@ -53,7 +53,7 @@ register_option hammer.aesopPremisesDefault : Nat := {
 }
 
 register_option hammer.grindPremisesDefault : Nat := {
-  defValue := 32
+  defValue := 100
   descr := "The default number of premises sent to grind"
 }
 
diff --git a/Hammer/ParallelismUtil.lean b/Hammer/ParallelismUtil.lean
index 13fe4c4..06826d3 100644
--- a/Hammer/ParallelismUtil.lean
+++ b/Hammer/ParallelismUtil.lean
@@ -103,12 +103,20 @@ def wrapTactic {α : Type} (tactic : α → TacticM Unit) (cancelTk? : Option IO
       Term.withoutModifyingElabMetaStateWithInfo do
         let preCount := (← Core.getMessageLog).reportedPlusUnreported.size
         let ngoals ← Term.withSynthesize (postpone := .no) do
-          Tactic.run mvar.mvarId! (tactic x)
+          Tactic.run mvar.mvarId! $ do
+            taskEventsRef.modify (·.push s!"Task {taskIdx} Tactic.run call started at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
+            tactic x
+            taskEventsRef.modify (·.push s!"Task {taskIdx} Tactic.run call ending at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
         let tryThisDelta := coreMessageLogDelta preCount (← Core.getMessageLog)
         if ngoals.isEmpty then
           taskEventsRef.modify (·.push s!"Task {taskIdx} confirmed that all goals were resolved at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
           let result ← instantiateMVars mvar
-          let result ← try inlineFreshProofs env0 result catch _ => return (none, tryThisDelta)
+          let result ←
+            try
+              inlineFreshProofs env0 result
+            catch _ =>
+              taskEventsRef.modify (·.push s!"Task {taskIdx} yielded a proof that couldn't be inlined at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
+              return (none, tryThisDelta)
           if (← proofExprIncomplete result) then
             taskEventsRef.modify (·.push s!"Task {taskIdx} confirmed to yield an incomplete proof at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
             return (none, tryThisDelta)
@@ -165,7 +173,7 @@ def tryAllTacsOnGoal (stxRef : Syntax) (outputAllSuggestions : Bool) (wallclockT
   let mut taskIdx := 0
   for tac in tacs do
     let wrappedTac := (← wrapTactic (fun () => tac) cancelTk stxRef taskIdx buildParallelTacticsStart taskEventsRef) ()
-    let t ← BaseIO.asTask do
+    let t ← BaseIO.asTask (prio := Task.Priority.max) do
       let startMs ← IO.monoMsNow
       taskEventsRef.modify (·.push s!"Task {taskIdx} started at +{startMs - buildParallelTacticsStart}ms")
       let r ← wrappedTac
diff --git a/Hammer/Tactic.lean b/Hammer/Tactic.lean
index 455240e..eb54c60 100644
--- a/Hammer/Tactic.lean
+++ b/Hammer/Tactic.lean
@@ -8,6 +8,11 @@ initialize
   Lean.registerTraceClass `hammer.premises
   Lean.registerTraceClass `hammer.profiling
 
+register_option hammer.singleTacticParallel : Bool := {
+  defValue := false
+  descr := "A temporary option to test the impact of using tryAllTacsOnGoal"
+}
+
 namespace Hammer
 
 open Lean Meta Elab Tactic HammerCore Syntax LibrarySuggestions Duper Aesop Qq Util
@@ -159,9 +164,27 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
     trace[hammer.profiling] "Premise filtering took {(← IO.monoMsNow) - premiseFilteringStart}ms"
     if configOptions.parallelism then
       match configOptions.disableAesop, configOptions.disableAuto, configOptions.disableGrind with
-      | true, true, false => runSingularTactic (evalTactic (← `(tactic| grind? [$grindParamStxs,*])))
-      | true, false, true => runSingularTactic (runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions)
-      | false, true, true => runSingularTactic (runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions)
+      | true, true, false =>
+        if hammer.singleTacticParallel.get (← getOptions) then
+          tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
+            evalTactic (← `(tactic| grind? [$grindParamStxs,*]))
+          ]
+        else
+          runSingularTactic (evalTactic (← `(tactic| grind? [$grindParamStxs,*])))
+      | true, false, true =>
+        if hammer.singleTacticParallel.get (← getOptions) then
+          tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
+            runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions
+          ]
+        else
+          runSingularTactic (runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions)
+      | false, true, true =>
+        if hammer.singleTacticParallel.get (← getOptions) then
+          tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
+            runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions
+          ]
+        else
+          runSingularTactic (runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions)
       | false, false, true =>
         tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
           runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions,
@@ -189,9 +212,27 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
       | true, true, true => throwError "Erroneous invocation of hammer: At least one of Aesop, Auto, and Grind must be enabled."
     else
       match configOptions.disableAesop, configOptions.disableAuto, configOptions.disableGrind with
-      | true, true, false => runSingularTactic (evalTactic (← `(tactic| grind? [$grindParamStxs,*])))
-      | true, false, true => runSingularTactic (runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions)
-      | false, _, _ => runSingularTactic (runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions)
+      | true, true, false =>
+        if hammer.singleTacticParallel.get (← getOptions) then
+          tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
+            evalTactic (← `(tactic| grind? [$grindParamStxs,*]))
+          ]
+        else
+          runSingularTactic (evalTactic (← `(tactic| grind? [$grindParamStxs,*])))
+      | true, false, true =>
+        if hammer.singleTacticParallel.get (← getOptions) then
+          tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
+            runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions
+          ]
+        else
+          runSingularTactic (runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions)
+      | false, _, _ =>
+        if hammer.singleTacticParallel.get (← getOptions) then
+          tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
+            runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions
+          ]
+        else
+          runSingularTactic (runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions)
       | true, false, false => throwError "Erroneous invocation of hammer: Aesop or parallelism is needed to enable both Auto and Grind."
       | true, true, true => throwError "Erroneous invocation of hammer: At least one of Aesop, Auto, and Grind must be enabled."