diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean
index b48070cb18..5eb9a2c636 100644
--- a/src/Init/Grind/Config.lean
+++ b/src/Init/Grind/Config.lean
@@ -111,11 +111,10 @@ structure Config where
   ring := true
   /--
   Maximum number of steps performed by the `ring` solver.
-  A step is counted whenever one polynomial is used to simplify another.
-  For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
-  used to simplify the second to `-1 * y^3 + x * y`.
+  A step is counted whenever one polynomial is used to simplify another,
+  weighted by the number of terms in the resulting polynomial.
   -/
-  ringSteps := 10000
+  ringSteps := 100000
   /--
   When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
   `CommRing`.
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
index ffa2d1fe3c..34d7728594 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
@@ -109,7 +109,7 @@ def _root_.Lean.Grind.CommRing.Poly.findSimp? (p : Poly) : RingM (Option EqCnstr
 /-- Simplifies `d.p` using `c`, and returns an extended polynomial derivation. -/
 def PolyDerivation.simplifyWith (d : PolyDerivation) (c : EqCnstr) : RingM PolyDerivation := do
   let some r := d.p.simp? c.p (← nonzeroChar?) | return d
-  incSteps
+  incSteps r.p.numTerms
   trace_goal[grind.ring.simp] "{← r.p.denoteExpr}"
   return .step r.p r.k₁ d r.k₂ r.m₂ c
 
@@ -137,7 +137,7 @@ def EqCnstr.simplifyWithCore (c₁ c₂ : EqCnstr) : RingM (Option EqCnstr) := d
     p := r.p
     h := .simp r.k₁ c₁ r.k₂ r.m₂ c₂
   }
-  incSteps
+  incSteps r.p.numTerms
   trace_goal[grind.ring.simp] "{← c.p.denoteExpr}"
   return some c
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
index 9651a94161..0805cb0420 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
@@ -184,6 +184,15 @@ def Poly.degree : Poly → Nat
   | .num _ => 0
   | .add _ m _ => m.degree
 
+/-- Returns the number of monomials in the polynomial. -/
+def Poly.numTerms (p : Poly) : Nat :=
+  go p 0
+where
+  go (p : Poly) (acc : Nat) : Nat :=
+    match p with
+    | .num .. => acc
+    | .add _ _ p => go p (acc + 1)
+
 /-- Returns `true` if the leading monomial of `p` divides `m`. -/
 def Poly.divides (p : Poly) (m : Mon) : Bool :=
   match p with
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean
index 06cc4fb099..1ed90897da 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean
@@ -13,8 +13,8 @@ namespace Lean.Meta.Grind.Arith.CommRing
 def checkMaxSteps : GoalM Bool := do
   return (← get').steps >= (← getConfig).ringSteps
 
-def incSteps : GoalM Unit := do
-  modify' fun s => { s with steps := s.steps + 1 }
+def incSteps (n : Nat := 1) : GoalM Unit := do
+  modify' fun s => { s with steps := s.steps + n }
 
 structure RingM.Context where
   ringId : Nat