diff --git a/kore/src/Kore/Reachability/Claim.hs b/kore/src/Kore/Reachability/Claim.hs
index 6d8882b254..2ebea20715 100644
--- a/kore/src/Kore/Reachability/Claim.hs
+++ b/kore/src/Kore/Reachability/Claim.hs
@@ -773,7 +773,7 @@ checkSimpleImplication inLeft inRight existentials =
         rhsBottom <-
             fmap isBottom . liftSimplifier $
                 SMT.Evaluator.filterMultiOr $srcLoc
-                    =<< Pattern.simplify right
+                    =<< Exists.makeEvaluate SideCondition.top existentials right
 
         case (trivial, rhsBottom) of
             (True, _) -> pure (claimToCheck, Implied Nothing)
diff --git a/kore/src/Kore/Simplify/Condition.hs b/kore/src/Kore/Simplify/Condition.hs
index c8aff5a50c..a0d2a61e10 100644
--- a/kore/src/Kore/Simplify/Condition.hs
+++ b/kore/src/Kore/Simplify/Condition.hs
@@ -16,16 +16,9 @@ import Control.Monad.State.Strict (
     StateT,
  )
 import Control.Monad.State.Strict qualified as State
-import Data.Functor.Foldable qualified as Recursive
 import Data.Generics.Product (
     field,
  )
-import Data.Set (
-    Set,
- )
-import Kore.Attribute.Pattern.FreeVariables (
-    freeVariableNames,
- )
 import Kore.Internal.Condition qualified as Condition
 import Kore.Internal.Conditional qualified as Conditional
 import Kore.Internal.MultiAnd (
@@ -60,8 +53,6 @@ import Kore.Simplify.SubstitutionSimplifier (
     SubstitutionSimplifier (..),
  )
 import Kore.Substitute
-import Kore.Syntax.Exists qualified as Exists
-import Kore.Syntax.Variable (SomeVariableName)
 import Kore.TopBottom qualified as TopBottom
 import Logic
 import Prelude.Kore
@@ -188,40 +179,15 @@ simplifyPredicates sideCondition original = do
     let predicates =
             SideCondition.simplifyConjunctionByAssumption original
                 & fst . extract
-    simplifiedPredicates <- do
-        let eliminatedExists =
-                map
-                    ( simplifyPredicateExistElim $
-                        -- TODO (sam): this is quite conservative and we may not need to
-                        -- avoid names here, but there doesn't seem to be a negative
-                        -- impact on performance, so best leave this in for now.
-                        freeVariableNames original
-                            <> freeVariableNames sideCondition
-                    )
-                    $ toList predicates
+    simplifiedPredicates <-
         simplifyPredicatesWithAssumptions
             sideCondition
-            eliminatedExists
+            (toList predicates)
     let simplified = foldMap mkCondition simplifiedPredicates
     if original == simplifiedPredicates
         then return (Condition.markSimplified simplified)
         else simplifyPredicates sideCondition simplifiedPredicates
 
-{- | Simplify an existential predicate by removing the existential binder and refreshing
-all occurrences of the name within the child term
--}
-simplifyPredicateExistElim ::
-    Set (SomeVariableName RewritingVariableName) ->
-    Predicate RewritingVariableName ->
-    Predicate RewritingVariableName
-simplifyPredicateExistElim avoid predicate = case predicateF of
-    Predicate.ExistsF existsF ->
-        let existsF'@Exists.Exists{existsChild} = Exists.refreshExists avoid existsF
-         in simplifyPredicateExistElim (avoid <> freeVariableNames existsF') existsChild
-    _ -> predicate
-  where
-    _ :< predicateF = Recursive.project predicate
-
 {- | Simplify a conjunction of predicates by simplifying each one
 under the assumption that the others are true.
 -}
diff --git a/kore/test/Test/Kore/Simplify/Pattern.hs b/kore/test/Test/Kore/Simplify/Pattern.hs
index a0ee6d9108..db022b5008 100644
--- a/kore/test/Test/Kore/Simplify/Pattern.hs
+++ b/kore/test/Test/Kore/Simplify/Pattern.hs
@@ -48,13 +48,16 @@ test_Pattern_simplify =
         "\\or(a, a)"
     , bottomLike `becomes` OrPattern.bottom $
         "\\and(a, \\bottom)"
-    , testCase "Removes top level exist quantifier whilst simplifying" $ do
+    , testCase "Replaces and terms under independent quantifiers" $ do
         let expect =
                 Pattern.fromTermAndPredicate
                     (Mock.constr10 fOfX)
                     ( makeAndPredicate
                         (makeCeilPredicate fOfX)
-                        (makeCeilPredicate fOfY)
+                        ( makeExistsPredicate
+                            Mock.yConfig
+                            (makeCeilPredicate fOfY)
+                        )
                     )
         actual <-
             simplify
@@ -114,7 +117,10 @@ test_Pattern_simplify =
                     (Mock.constr10 fOfX)
                     ( makeAndPredicate
                         (makeCeilPredicate fOfX)
-                        (fromCeil_ $ Mock.f (mkElemVar x'))
+                        ( makeExistsPredicate
+                            x'
+                            (fromCeil_ $ Mock.f (mkElemVar x'))
+                        )
                     )
                     & OrPattern.fromPattern
         actual <-
diff --git a/kore/test/Test/Kore/Unification/UnifierT.hs b/kore/test/Test/Kore/Unification/UnifierT.hs
index acf70f754f..9b0b025f23 100644
--- a/kore/test/Test/Kore/Unification/UnifierT.hs
+++ b/kore/test/Test/Kore/Unification/UnifierT.hs
@@ -60,12 +60,9 @@ test_simplifyCondition =
         actual <- normalize Condition.bottomCondition
         assertEqual "Expected empty result" expect actual
         assertNormalizedPredicatesMulti actual
-    , testCase
-        ( "∃ y z. x = σ(y, z) normalized to a substitution x = σ(y, z) "
-            <> "(top-level exists get removed, and y,z must be fresh in the context)"
-        )
-        $ do
-            assertNormalized existsSubst
+    , testCase "∃ y z. x = σ(y, z)" $ do
+        let expect = Condition.fromPredicate existsPredicate
+        assertNormalized expect
     , testCase "¬∃ y z. x = σ(y, z)" $ do
         let expect =
                 Condition.fromPredicate $
@@ -96,10 +93,6 @@ test_simplifyCondition =
         assertEqual "Expected \\top" expect actual
     ]
   where
-    existsSubst =
-        Condition.fromSubstitution $
-            Substitution.unsafeWrap
-                [(inject Mock.xConfig, (Mock.sigma (mkElemVar Mock.yConfig) (mkElemVar Mock.zConfig)))]
     existsPredicate =
         Predicate.makeMultipleExists [Mock.yConfig, Mock.zConfig] $
             Predicate.makeEqualsPredicate
diff --git a/test/rpc-server/implies/not-implied-stuck/README.md b/test/rpc-server/implies/not-implied-stuck/README.md
deleted file mode 100644
index 5b2f54fa0e..0000000000
--- a/test/rpc-server/implies/not-implied-stuck/README.md
+++ /dev/null
@@ -1 +0,0 @@
-`X => ∃ Z. (Z ∧ ¬ (X = Z))`, response `False`, with substitution `[Z/X]`
diff --git a/test/rpc-server/implies/not-implied-stuck/antecedent.json b/test/rpc-server/implies/not-implied-stuck/antecedent.json
deleted file mode 100644
index 1f7d7583e2..0000000000
--- a/test/rpc-server/implies/not-implied-stuck/antecedent.json
+++ /dev/null
@@ -1,13 +0,0 @@
-{
-    "format": "KORE",
-    "version": 1,
-    "term": {
-        "tag": "EVar",
-        "name": "X",
-        "sort": {
-            "tag": "SortApp",
-            "name": "SortK",
-            "args": []
-        }
-    }
-}
diff --git a/test/rpc-server/implies/not-implied-stuck/consequent.json b/test/rpc-server/implies/not-implied-stuck/consequent.json
deleted file mode 100644
index 845cf85d6c..0000000000
--- a/test/rpc-server/implies/not-implied-stuck/consequent.json
+++ /dev/null
@@ -1,74 +0,0 @@
-{
-    "format": "KORE",
-    "version": 1,
-    "term": {
-        "tag": "Exists",
-        "sort": {
-            "tag": "SortApp",
-            "name": "SortK",
-            "args": []
-        },
-        "var": "Z",
-        "varSort": {
-            "tag": "SortApp",
-            "name": "SortK",
-            "args": []
-        },
-        "arg": {
-            "tag": "And",
-            "sort": {
-                "tag": "SortApp",
-                "name": "SortK",
-                "args": []
-            },
-            "first": {
-                "tag": "EVar",
-                "name": "Z",
-                "sort": {
-                    "tag": "SortApp",
-                    "name": "SortK",
-                    "args": []
-                }
-            },
-            "second": {
-                "tag": "Not",
-                "sort": {
-                    "tag": "SortApp",
-                    "name": "SortK",
-                    "args": []
-                },
-                "arg": {
-                    "tag":"Equals",
-                    "sort":{
-                        "tag": "SortApp",
-                        "name": "SortK",
-                        "args": []
-                    },
-                    "argSort":{
-                        "tag": "SortApp",
-                        "name": "SortK",
-                        "args": []
-                    },
-                    "first":{
-                        "tag":"EVar",
-                        "name":"X",
-                        "sort":{
-                            "tag": "SortApp",
-                            "name": "SortK",
-                            "args": []
-                        }
-                    },
-                    "second":{
-                        "tag":"EVar",
-                        "name":"Z",
-                        "sort":{
-                            "tag": "SortApp",
-                            "name": "SortK",
-                            "args": []
-                        }
-                    }
-                }
-            }
-        }
-    }
-}
diff --git a/test/rpc-server/implies/not-implied-stuck/definition.kore b/test/rpc-server/implies/not-implied-stuck/definition.kore
deleted file mode 120000
index 89dde956b8..0000000000
--- a/test/rpc-server/implies/not-implied-stuck/definition.kore
+++ /dev/null
@@ -1 +0,0 @@
-../../resources/empty/definition.kore
\ No newline at end of file
diff --git a/test/rpc-server/implies/not-implied-stuck/response.golden b/test/rpc-server/implies/not-implied-stuck/response.golden
deleted file mode 100644
index 40423b8537..0000000000
--- a/test/rpc-server/implies/not-implied-stuck/response.golden
+++ /dev/null
@@ -1 +0,0 @@
-{"jsonrpc":"2.0","id":1,"result":{"satisfiable":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"And","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Not","sort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}