diff --git a/kore/src/Kore/Builtin/KEqual.hs b/kore/src/Kore/Builtin/KEqual.hs
index 140d8779a5..36f32440b4 100644
--- a/kore/src/Kore/Builtin/KEqual.hs
+++ b/kore/src/Kore/Builtin/KEqual.hs
@@ -147,7 +147,8 @@ evalKEq true (valid :< app) =
 
         defined1 <- Ceil.makeEvaluate sideCondition pattern1
         defined2 <- Ceil.makeEvaluate sideCondition pattern2
-        defined <- And.simplifyEvaluated sideCondition defined1 defined2
+        defined <-
+            And.simplifyEvaluated Not.notSimplifier sideCondition defined1 defined2
 
         equalTerms <-
             Equals.makeEvaluateTermsToPredicate
@@ -162,7 +163,8 @@ evalKEq true (valid :< app) =
             falsePatterns = Pattern.withCondition falseTerm <$> notEqualTerms
 
         let undefinedResults = Or.simplifyEvaluated truePatterns falsePatterns
-        results <- And.simplifyEvaluated sideCondition defined undefinedResults
+        results <-
+            And.simplifyEvaluated Not.notSimplifier sideCondition defined undefinedResults
         pure $ Applied AttemptedAxiomResults
             { results
             , remainders = OrPattern.bottom
diff --git a/kore/src/Kore/Repl/Data.hs b/kore/src/Kore/Repl/Data.hs
index 825243e418..807af4c0cd 100644
--- a/kore/src/Kore/Repl/Data.hs
+++ b/kore/src/Kore/Repl/Data.hs
@@ -88,8 +88,9 @@ import Kore.Profiler.Data
     ( MonadProfiler
     )
 import Kore.Step.Simplification.Data
-    ( MonadSimplify
+    ( MonadSimplify (..)
     )
+import qualified Kore.Step.Simplification.Not as Not
 import qualified Kore.Step.Strategy as Strategy
 import Kore.Strategies.Goal
 import Kore.Strategies.Verification
@@ -494,6 +495,10 @@ deriving instance MonadSMT m => MonadSMT (UnifierWithExplanation m)
 
 deriving instance MonadProfiler m => MonadProfiler (UnifierWithExplanation m)
 
+instance MonadTrans UnifierWithExplanation where
+    lift = UnifierWithExplanation . lift . lift
+    {-# INLINE lift #-}
+
 instance MonadLog m => MonadLog (UnifierWithExplanation m) where
     logEntry entry = UnifierWithExplanation $ logEntry entry
     {-# INLINE logEntry #-}
@@ -501,7 +506,13 @@ instance MonadLog m => MonadLog (UnifierWithExplanation m) where
         UnifierWithExplanation $ logWhile entry (getUnifierWithExplanation ma)
     {-# INLINE logWhile #-}
 
-deriving instance MonadSimplify m => MonadSimplify (UnifierWithExplanation m)
+instance MonadSimplify m => MonadSimplify (UnifierWithExplanation m) where
+    localSimplifierTermLike locally (UnifierWithExplanation unifierT) =
+        UnifierWithExplanation
+        $ localSimplifierTermLike locally unifierT
+    localSimplifierAxioms locally (UnifierWithExplanation unifierT) =
+        UnifierWithExplanation
+        $ localSimplifierAxioms locally unifierT
 
 instance MonadSimplify m => MonadUnify (UnifierWithExplanation m) where
     throwUnificationError =
@@ -570,7 +581,7 @@ runUnifierWithExplanation (UnifierWithExplanation unifier) =
     unificationResults =
         fmap (\(r, ex) -> flip (,) ex <$> r)
         . flip runAccumT mempty
-        . Monad.Unify.runUnifierT
+        . Monad.Unify.runUnifierT Not.notSimplifier
         $ unifier
     explainError = Left . makeAuxReplOutput . show . Pretty.pretty
     failWithExplanation
diff --git a/kore/src/Kore/Step/Search.hs b/kore/src/Kore/Step/Search.hs
index f9c644c548..6a2e763a78 100644
--- a/kore/src/Kore/Step/Search.hs
+++ b/kore/src/Kore/Step/Search.hs
@@ -55,6 +55,7 @@ import qualified Kore.Internal.Pattern as Conditional
 import Kore.Internal.SideCondition
     ( SideCondition
     )
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Step.Simplification.Simplify
 import qualified Kore.Step.SMT.Evaluator as SMT.Evaluator
     ( evaluate
@@ -138,7 +139,7 @@ matchWith
     -> MaybeT m (OrCondition variable)
 matchWith sideCondition e1 e2 = do
     eitherUnifiers <-
-        lift $ Unifier.runUnifierT
+        lift $ Unifier.runUnifierT Not.notSimplifier
         $ unificationProcedureWorker sideCondition t1 t2
     let
         maybeUnifiers :: Maybe [Condition variable]
diff --git a/kore/src/Kore/Step/Simplification/And.hs b/kore/src/Kore/Step/Simplification/And.hs
index 4e6f587bc5..c7a1cc6513 100644
--- a/kore/src/Kore/Step/Simplification/And.hs
+++ b/kore/src/Kore/Step/Simplification/And.hs
@@ -19,8 +19,7 @@ module Kore.Step.Simplification.And
 import Prelude.Kore
 
 import Control.Error
-    ( fromMaybe
-    , runMaybeT
+    ( runMaybeT
     )
 import Control.Monad
     ( foldM
@@ -111,13 +110,12 @@ import qualified Kore.Internal.TermLike as TermLike
 import Kore.Step.Simplification.AndTerms
     ( maybeTermAnd
     )
+import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.Simplify
 import qualified Kore.Step.Substitution as Substitution
 import Kore.Unification.UnifierT
-    ( runUnifierT
-    )
-import Kore.Unification.Unify
-    ( MonadUnify
+    ( UnifierT (..)
+    , runUnifierT
     )
 import Kore.Unparser
     ( unparse
@@ -164,12 +162,14 @@ Also, we have
     the same for two string literals and two chars
 -}
 simplify
-    :: (InternalVariable variable, MonadSimplify simplifier)
-    => SideCondition variable
+    :: InternalVariable variable
+    => MonadSimplify simplifier
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> And Sort (OrPattern variable)
     -> simplifier (OrPattern variable)
-simplify sideCondition And { andFirst = first, andSecond = second } =
-    simplifyEvaluated sideCondition first second
+simplify notSimplifier sideCondition And { andFirst = first, andSecond = second } =
+    simplifyEvaluated notSimplifier sideCondition first second
 
 {-| simplifies an And given its two 'OrPattern' children.
 
@@ -189,12 +189,14 @@ to carry around.
 
 -}
 simplifyEvaluated
-    :: (InternalVariable variable, MonadSimplify simplifier)
-    => SideCondition variable
+    :: InternalVariable variable
+    => MonadSimplify simplifier
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> OrPattern variable
     -> OrPattern variable
     -> simplifier (OrPattern variable)
-simplifyEvaluated sideCondition first second
+simplifyEvaluated notSimplifier sideCondition first second
   | OrPattern.isFalse first  = return OrPattern.bottom
   | OrPattern.isFalse second = return OrPattern.bottom
   | OrPattern.isTrue first   = return second
@@ -204,17 +206,19 @@ simplifyEvaluated sideCondition first second
         gather $ do
             first1 <- scatter first
             second1 <- scatter second
-            makeEvaluate sideCondition first1 second1
+            makeEvaluate notSimplifier sideCondition first1 second1
     return (OrPattern.fromPatterns result)
 
 simplifyEvaluatedMultiple
-    :: (InternalVariable variable, MonadSimplify simplifier)
-    => SideCondition variable
+    :: InternalVariable variable
+    => MonadSimplify simplifier
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> [OrPattern variable]
     -> simplifier (OrPattern variable)
-simplifyEvaluatedMultiple _ [] = return OrPattern.top
-simplifyEvaluatedMultiple sideCondition (pat : patterns) =
-    foldM (simplifyEvaluated sideCondition) pat patterns
+simplifyEvaluatedMultiple _ _ [] = return OrPattern.top
+simplifyEvaluatedMultiple notSimplifier sideCondition (pat : patterns) =
+    foldM (simplifyEvaluated notSimplifier sideCondition) pat patterns
 
 {-|'makeEvaluate' simplifies an 'And' of 'Pattern's.
 
@@ -225,31 +229,34 @@ makeEvaluate
         , HasCallStack
         , MonadSimplify simplifier
         )
-    => SideCondition variable
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> Pattern variable
     -> Pattern variable
     -> BranchT simplifier (Pattern variable)
-makeEvaluate sideCondition first second
+makeEvaluate notSimplifier sideCondition first second
   | Pattern.isBottom first || Pattern.isBottom second = empty
   | Pattern.isTop first = return second
   | Pattern.isTop second = return first
-  | otherwise = makeEvaluateNonBool sideCondition first second
+  | otherwise = makeEvaluateNonBool notSimplifier sideCondition first second
 
 makeEvaluateNonBool
     ::  ( InternalVariable variable
         , HasCallStack
         , MonadSimplify simplifier
         )
-    => SideCondition variable
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> Pattern variable
     -> Pattern variable
     -> BranchT simplifier (Pattern variable)
 makeEvaluateNonBool
+    notSimplifier
     sideCondition
     first@Conditional { term = firstTerm }
     second@Conditional { term = secondTerm }
   = do
-    terms <- termAnd firstTerm secondTerm
+    terms <- termAnd notSimplifier firstTerm secondTerm
     let firstCondition = Conditional.withoutTerm first
         secondCondition = Conditional.withoutTerm second
         initialConditions = firstCondition <> secondCondition
@@ -433,23 +440,24 @@ The comment for 'simplify' describes all the special cases handled by this.
 -}
 termAnd
     :: forall variable simplifier
-    .  (InternalVariable variable, MonadSimplify simplifier)
+    .  InternalVariable variable
+    => MonadSimplify simplifier
     => HasCallStack
-    => TermLike variable
+    => NotSimplifier (UnifierT simplifier)
+    -> TermLike variable
     -> TermLike variable
     -> BranchT simplifier (Pattern variable)
-termAnd p1 p2 =
+termAnd notSimplifier p1 p2 =
     either (const andTerm) BranchT.scatter
-    =<< (lift . runUnifierT) (termAndWorker p1 p2)
+    =<< (lift . runUnifierT notSimplifier) (termAndWorker p1 p2)
   where
     andTerm = return $ Pattern.fromTermLike (mkAnd p1 p2)
     termAndWorker
-        :: MonadUnify unifier
-        => TermLike variable
+        :: TermLike variable
         -> TermLike variable
-        -> unifier (Pattern variable)
+        -> UnifierT simplifier (Pattern variable)
     termAndWorker first second = do
-        let maybeTermAnd' = maybeTermAnd termAndWorker first second
+        let maybeTermAnd' = maybeTermAnd notSimplifier termAndWorker first second
         patt <- runMaybeT maybeTermAnd'
         return $ fromMaybe andPattern patt
       where
diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs
index b8d78217b3..75326ee8bf 100644
--- a/kore/src/Kore/Step/Simplification/AndTerms.hs
+++ b/kore/src/Kore/Step/Simplification/AndTerms.hs
@@ -68,6 +68,7 @@ import Kore.Step.Simplification.ExpandAlias
     )
 import Kore.Step.Simplification.InjSimplifier
 import Kore.Step.Simplification.NoConfusion
+import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.Overloading
 import Kore.Step.Simplification.SimplificationType
     ( SimplificationType
@@ -114,10 +115,11 @@ termUnification
     .  InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => TermLike variable
+    => NotSimplifier unifier
+    -> TermLike variable
     -> TermLike variable
     -> unifier (Pattern variable)
-termUnification =
+termUnification notSimplifier =
     termUnificationWorker
   where
     termUnificationWorker
@@ -127,7 +129,8 @@ termUnification =
     termUnificationWorker pat1 pat2 = do
         let
             maybeTermUnification :: MaybeT unifier (Pattern variable)
-            maybeTermUnification = maybeTermAnd termUnificationWorker pat1 pat2
+            maybeTermUnification =
+                maybeTermAnd notSimplifier termUnificationWorker pat1 pat2
             unsupportedPatternsError =
                 throwUnificationError
                     (unsupportedPatterns
@@ -141,32 +144,38 @@ maybeTermEquals
     :: InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => TermSimplifier variable unifier
+    => NotSimplifier unifier
+    -> TermSimplifier variable unifier
     -- ^ Used to simplify subterm "and".
     -> TermLike variable
     -> TermLike variable
     -> MaybeT unifier (Pattern variable)
-maybeTermEquals = maybeTransformTerm equalsFunctions
+maybeTermEquals notSimplifier =
+    maybeTransformTerm (equalsFunctions notSimplifier)
 
 maybeTermAnd
     :: InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => TermSimplifier variable unifier
+    => NotSimplifier unifier
+    -> TermSimplifier variable unifier
     -- ^ Used to simplify subterm "and".
     -> TermLike variable
     -> TermLike variable
     -> MaybeT unifier (Pattern variable)
-maybeTermAnd = maybeTransformTerm andFunctions
+maybeTermAnd notSimplifier =
+    maybeTransformTerm (andFunctions notSimplifier)
 
 andFunctions
     :: forall variable unifier
     .  InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => [TermTransformationOld variable unifier]
-andFunctions =
-    map (forAnd . snd) (filter appliesToAnd andEqualsFunctions)
+    => NotSimplifier unifier
+    -> [TermTransformationOld variable unifier]
+andFunctions notSimplifier =
+    forAnd . snd
+    <$> filter appliesToAnd (andEqualsFunctions notSimplifier)
   where
     appliesToAnd :: (SimplificationTarget, a) -> Bool
     appliesToAnd (AndT, _) = True
@@ -183,9 +192,11 @@ equalsFunctions
     .  InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => [TermTransformationOld variable unifier]
-equalsFunctions =
-    map (forEquals . snd) (filter appliesToEquals andEqualsFunctions)
+    => NotSimplifier unifier
+    -> [TermTransformationOld variable unifier]
+equalsFunctions notSimplifier =
+    forEquals . snd
+    <$> filter appliesToEquals (andEqualsFunctions notSimplifier)
   where
     appliesToEquals :: (SimplificationTarget, a) -> Bool
     appliesToEquals (AndT, _) = False
@@ -202,9 +213,10 @@ andEqualsFunctions
     .  InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => [(SimplificationTarget, TermTransformation variable unifier)]
-andEqualsFunctions = fmap mapEqualsFunctions
-    [ (AndT,    \_ _ s -> expandAlias (maybeTermAnd s), "expandAlias")
+    => NotSimplifier unifier
+    -> [(SimplificationTarget, TermTransformation variable unifier)]
+andEqualsFunctions notSimplifier = fmap mapEqualsFunctions
+    [ (AndT,    \_ _ s -> expandAlias (maybeTermAnd notSimplifier s), "expandAlias")
     , (AndT,    \_ _ _ -> boolAnd, "boolAnd")
     , (BothT,   \_ _ _ -> equalAndEquals, "equalAndEquals")
     , (BothT,   \_ _ _ -> bytesDifferent, "bytesDifferent")
diff --git a/kore/src/Kore/Step/Simplification/Equals.hs b/kore/src/Kore/Step/Simplification/Equals.hs
index ef85462280..bc04fc9cb1 100644
--- a/kore/src/Kore/Step/Simplification/Equals.hs
+++ b/kore/src/Kore/Step/Simplification/Equals.hs
@@ -73,7 +73,8 @@ import qualified Kore.Step.Simplification.Implies as Implies
     ( simplifyEvaluated
     )
 import qualified Kore.Step.Simplification.Not as Not
-    ( simplifyEvaluated
+    ( notSimplifier
+    , simplifyEvaluated
     , simplifyEvaluatedPredicate
     )
 import qualified Kore.Step.Simplification.Or as Or
@@ -231,7 +232,7 @@ makeEvaluateFunctionalOr sideCondition first seconds = do
     let oneNotBottom = foldl' Or.simplifyEvaluated OrPattern.bottom secondCeils
     allAreBottom <-
         foldM
-            (And.simplifyEvaluated sideCondition)
+            (And.simplifyEvaluated Not.notSimplifier sideCondition)
             (OrPattern.fromPatterns [Pattern.top])
             (firstNotCeil : secondNotCeils)
     firstEqualsSeconds <-
@@ -240,7 +241,7 @@ makeEvaluateFunctionalOr sideCondition first seconds = do
             (zip seconds secondCeils)
     oneIsNotBottomEquals <-
         foldM
-            (And.simplifyEvaluated sideCondition)
+            (And.simplifyEvaluated Not.notSimplifier sideCondition)
             firstCeil
             (oneNotBottom : firstEqualsSeconds)
     return (MultiOr.merge allAreBottom oneIsNotBottomEquals)
@@ -300,13 +301,14 @@ makeEvaluate
     firstCeilNegation <- Not.simplifyEvaluated sideCondition firstCeil
     secondCeilNegation <- Not.simplifyEvaluated sideCondition secondCeil
     termEquality <- makeEvaluateTermsAssumesNoBottom firstTerm secondTerm
-    negationAnd <-
-        And.simplifyEvaluated sideCondition firstCeilNegation secondCeilNegation
-    ceilAnd <- And.simplifyEvaluated sideCondition firstCeil secondCeil
-    equalityAnd <- And.simplifyEvaluated sideCondition termEquality ceilAnd
+    negationAnd <- simplifyEvaluatedAnd firstCeilNegation secondCeilNegation
+    ceilAnd <- simplifyEvaluatedAnd firstCeil secondCeil
+    equalityAnd <- simplifyEvaluatedAnd termEquality ceilAnd
     return $ Or.simplifyEvaluated equalityAnd negationAnd
   where
     termsAreEqual = firstTerm == secondTerm
+    simplifyEvaluatedAnd =
+        And.simplifyEvaluated Not.notSimplifier sideCondition
 
 -- Do not export this. This not valid as a standalone function, it
 -- assumes that some extra conditions will be added on the outside
@@ -412,7 +414,9 @@ termEqualsAnd
 termEqualsAnd p1 p2 =
     MaybeT $ run $ maybeTermEqualsWorker p1 p2
   where
-    run it = (runUnifierT . runMaybeT) it >>= either missingCase BranchT.scatter
+    run it =
+        (runUnifierT Not.notSimplifier . runMaybeT) it
+        >>= either missingCase BranchT.scatter
     missingCase = const (return Nothing)
 
     maybeTermEqualsWorker
@@ -421,7 +425,8 @@ termEqualsAnd p1 p2 =
         => TermLike variable
         -> TermLike variable
         -> MaybeT unifier (Pattern variable)
-    maybeTermEqualsWorker = maybeTermEquals termEqualsAndWorker
+    maybeTermEqualsWorker =
+        maybeTermEquals Not.notSimplifier termEqualsAndWorker
 
     termEqualsAndWorker
         :: forall unifier
@@ -431,8 +436,9 @@ termEqualsAnd p1 p2 =
         -> unifier (Pattern variable)
     termEqualsAndWorker first second =
         either ignoreErrors scatterResults
-        =<< (runUnifierT . runMaybeT) (maybeTermEqualsWorker first second)
+        =<< runUnification (maybeTermEqualsWorker first second)
       where
+        runUnification = runUnifierT Not.notSimplifier . runMaybeT
         ignoreErrors _ = return equalsPredicate
         scatterResults =
             maybe
diff --git a/kore/src/Kore/Step/Simplification/Implies.hs b/kore/src/Kore/Step/Simplification/Implies.hs
index c362b0267f..b28353950e 100644
--- a/kore/src/Kore/Step/Simplification/Implies.hs
+++ b/kore/src/Kore/Step/Simplification/Implies.hs
@@ -31,6 +31,7 @@ import qualified Kore.Step.Simplification.And as And
     )
 import qualified Kore.Step.Simplification.Not as Not
     ( makeEvaluate
+    , notSimplifier
     , simplifyEvaluated
     )
 import Kore.Step.Simplification.Simplify
@@ -120,6 +121,7 @@ distributeEvaluateImplies
     -> simplifier (OrPattern variable)
 distributeEvaluateImplies sideCondition firsts second =
     And.simplifyEvaluatedMultiple
+        Not.notSimplifier
         sideCondition
         (map (\first -> makeEvaluateImplies first second) firsts)
 
diff --git a/kore/src/Kore/Step/Simplification/Not.hs b/kore/src/Kore/Step/Simplification/Not.hs
index eec17004a0..50bf75e87d 100644
--- a/kore/src/Kore/Step/Simplification/Not.hs
+++ b/kore/src/Kore/Step/Simplification/Not.hs
@@ -13,6 +13,7 @@ module Kore.Step.Simplification.Not
     , simplify
     , simplifyEvaluated
     , simplifyEvaluatedPredicate
+    , notSimplifier
     ) where
 
 import Prelude.Kore
@@ -61,6 +62,7 @@ import qualified Kore.Internal.TermLike as TermLike
     ( markSimplified
     )
 import qualified Kore.Step.Simplification.And as And
+import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.Simplify
 import Kore.TopBottom
     ( TopBottom (..)
@@ -233,7 +235,10 @@ mkMultiAndPattern
     -> MultiAnd (Pattern variable)
     -> BranchT simplifier (Pattern variable)
 mkMultiAndPattern sideCondition patterns =
-    Foldable.foldrM (And.makeEvaluate sideCondition) Pattern.top patterns
+    Foldable.foldrM
+        (And.makeEvaluate notSimplifier sideCondition)
+        Pattern.top
+        patterns
 
 {- | Conjoin and simplify a 'MultiAnd' of 'Condition'.
  -}
@@ -245,3 +250,9 @@ mkMultiAndPredicate predicates =
     -- Using Foldable.fold because the Monoid instance of Condition
     -- implements And semantics.
     return $ Foldable.fold predicates
+
+notSimplifier
+    :: MonadSimplify simplifier
+    => NotSimplifier simplifier
+notSimplifier =
+    NotSimplifier simplifyEvaluated
diff --git a/kore/src/Kore/Step/Simplification/NotSimplifier.hs b/kore/src/Kore/Step/Simplification/NotSimplifier.hs
new file mode 100644
index 0000000000..fd61538f96
--- /dev/null
+++ b/kore/src/Kore/Step/Simplification/NotSimplifier.hs
@@ -0,0 +1,29 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Step.Simplification.NotSimplifier
+    ( NotSimplifier (..)
+    ) where
+
+import Kore.Internal.OrPattern
+    ( OrPattern
+    )
+import Kore.Internal.SideCondition
+    ( SideCondition
+    )
+import Kore.Internal.TermLike
+    ( InternalVariable
+    )
+
+newtype NotSimplifier simplifier =
+    NotSimplifier
+        { runNotSimplifier
+            :: forall variable
+            .  InternalVariable variable
+            => SideCondition variable
+            -> OrPattern variable
+            -> simplifier (OrPattern variable)
+        }
diff --git a/kore/src/Kore/Step/Simplification/TermLike.hs b/kore/src/Kore/Step/Simplification/TermLike.hs
index 23b38e7ae7..f56b2c780f 100644
--- a/kore/src/Kore/Step/Simplification/TermLike.hs
+++ b/kore/src/Kore/Step/Simplification/TermLike.hs
@@ -115,7 +115,8 @@ import qualified Kore.Step.Simplification.Next as Next
     ( simplify
     )
 import qualified Kore.Step.Simplification.Not as Not
-    ( simplify
+    ( notSimplifier
+    , simplify
     )
 import qualified Kore.Step.Simplification.Nu as Nu
     ( simplify
@@ -384,7 +385,8 @@ simplifyInternal term sideCondition = do
             SignednessF _ -> doNotSimplify
             --
             AndF andF ->
-                And.simplify sideCondition =<< simplifyChildren andF
+                And.simplify Not.notSimplifier sideCondition
+                    =<< simplifyChildren andF
             ApplySymbolF applySymbolF ->
                 Application.simplify sideCondition
                     =<< simplifyChildren applySymbolF
diff --git a/kore/src/Kore/Unification/Procedure.hs b/kore/src/Kore/Unification/Procedure.hs
index f227de3027..e5b242881e 100644
--- a/kore/src/Kore/Unification/Procedure.hs
+++ b/kore/src/Kore/Unification/Procedure.hs
@@ -39,6 +39,7 @@ import Kore.Step.Simplification.AndTerms
 import qualified Kore.Step.Simplification.Ceil as Ceil
     ( makeEvaluateTerm
     )
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Step.Simplification.Simplify
     ( MonadSimplify
     , simplifyCondition
@@ -47,7 +48,7 @@ import qualified Kore.TopBottom as TopBottom
 import Kore.Unification.Error
 import Kore.Unification.UnificationProcedure
 import Kore.Unification.UnifierT
-    ( getUnifierT
+    ( evalEnvUnifierT
     )
 import Kore.Unification.Unify
     ( InternalVariable
@@ -71,7 +72,7 @@ unificationProcedureWorker sideCondition p1 p2
   | p1Sort /= p2Sort =
     Monad.Unify.explainAndReturnBottom "Cannot unify different sorts."  p1 p2
   | otherwise = infoAttemptUnification p1 p2 $ do
-    pat <- termUnification p1 p2
+    pat <- termUnification Not.notSimplifier p1 p2
     TopBottom.guardAgainstBottom pat
     let (term, conditions) = Conditional.splitTerm pat
         mergedSideCondition =
@@ -90,4 +91,4 @@ unificationProcedure
 unificationProcedure =
     UnificationProcedure $ \sideCondition term1 term2 ->
         unificationProcedureWorker sideCondition term1 term2
-        & getUnifierT
+        & evalEnvUnifierT Not.notSimplifier
diff --git a/kore/src/Kore/Unification/SubstitutionSimplifier.hs b/kore/src/Kore/Unification/SubstitutionSimplifier.hs
index 9727b28ed3..883f6d8450 100644
--- a/kore/src/Kore/Unification/SubstitutionSimplifier.hs
+++ b/kore/src/Kore/Unification/SubstitutionSimplifier.hs
@@ -14,7 +14,8 @@ module Kore.Unification.SubstitutionSimplifier
 import Prelude.Kore
 
 import Control.Error
-    ( maybeT
+    ( MaybeT
+    , maybeT
     )
 
 import qualified Branch as BranchT
@@ -23,15 +24,26 @@ import Kore.Internal.OrCondition
     ( OrCondition
     )
 import qualified Kore.Internal.OrCondition as OrCondition
+import Kore.Internal.Pattern
+    ( Pattern
+    )
+import Kore.Internal.Predicate
+    ( Predicate
+    )
 import Kore.Internal.SideCondition
     ( SideCondition
     )
 import Kore.Internal.Substitution
-    ( Substitution
+    ( Normalization
+    , Substitution
+    )
+import Kore.Internal.TermLike
+    ( TermLike
     )
 import Kore.Step.Simplification.AndTerms
     ( termUnification
     )
+import Kore.Step.Simplification.NotSimplifier
 import qualified Kore.Step.Simplification.Simplify as Simplifier
 import Kore.Step.Simplification.SubstitutionSimplifier
     ( MakeAnd (..)
@@ -51,8 +63,9 @@ uses 'Unifier.throwUnificationError'.
 substitutionSimplifier
     :: forall unifier
     .  MonadUnify unifier
-    => SubstitutionSimplifier unifier
-substitutionSimplifier =
+    => NotSimplifier unifier
+    -> SubstitutionSimplifier unifier
+substitutionSimplifier notSimplifier =
     SubstitutionSimplifier wrapper
   where
     wrapper
@@ -62,20 +75,41 @@ substitutionSimplifier =
         -> Substitution variable
         -> unifier (OrCondition variable)
     wrapper sideCondition substitution = do
-        (predicate, result) <- worker substitution & maybeT empty return
+        (predicate, result) <-
+            worker substitution
+            & maybeT empty return
         let condition = Condition.fromNormalizationSimplified result
         let condition' = Condition.fromPredicate predicate <> condition
             conditions = OrCondition.fromCondition condition'
         TopBottom.guardAgainstBottom conditions
         return conditions
       where
-        worker = simplifySubstitutionWorker sideCondition unificationMakeAnd
+        worker
+            :: Substitution variable
+            -> MaybeT
+                unifier
+                (Predicate variable, Normalization variable)
+        worker =
+            simplifySubstitutionWorker
+                sideCondition
+                (unificationMakeAnd notSimplifier)
 
-unificationMakeAnd :: MonadUnify unifier => MakeAnd unifier
-unificationMakeAnd =
+unificationMakeAnd
+    :: forall unifier
+    .  MonadUnify unifier
+    => NotSimplifier unifier
+    -> MakeAnd unifier
+unificationMakeAnd notSimplifier =
     MakeAnd { makeAnd }
   where
+    makeAnd
+        :: forall variable
+        .  InternalVariable variable
+        => TermLike variable
+        -> TermLike variable
+        -> SideCondition variable
+        -> unifier (Pattern variable)
     makeAnd termLike1 termLike2 sideCondition = do
-        unified <- termUnification termLike1 termLike2
+        unified <- termUnification notSimplifier termLike1 termLike2
         Simplifier.simplifyCondition sideCondition unified
             & BranchT.alternate
diff --git a/kore/src/Kore/Unification/UnifierT.hs b/kore/src/Kore/Unification/UnifierT.hs
index f6c686d793..75f69bb88a 100644
--- a/kore/src/Kore/Unification/UnifierT.hs
+++ b/kore/src/Kore/Unification/UnifierT.hs
@@ -8,6 +8,7 @@ module Kore.Unification.UnifierT
     , lowerExceptT
     , runUnifierT
     , maybeUnifierT
+    , evalEnvUnifierT
     , substitutionSimplifier
     -- * Re-exports
     , module Kore.Unification.Unify
@@ -21,9 +22,16 @@ import Control.Monad
     )
 import qualified Control.Monad.Except as Error
 import qualified Control.Monad.Morph as Morph
+import Control.Monad.Reader
+    ( MonadReader (..)
+    )
 import Control.Monad.Trans.Class
     ( MonadTrans (..)
     )
+import Control.Monad.Trans.Reader
+    ( ReaderT (..)
+    , mapReaderT
+    )
 
 import Branch
     ( BranchT
@@ -33,6 +41,7 @@ import Kore.Profiler.Data
     ( MonadProfiler
     )
 import qualified Kore.Step.Simplification.Condition as ConditionSimplifier
+import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.Simplify
     ( ConditionSimplifier (..)
     , InternalVariable
@@ -51,13 +60,21 @@ import SMT
     )
 
 newtype UnifierT (m :: * -> *) a =
-    UnifierT { getUnifierT :: BranchT (ExceptT UnificationError m) a }
+    UnifierT
+        { getUnifierT
+            :: ReaderT
+                (ConditionSimplifier (UnifierT m))
+                (BranchT (ExceptT UnificationError m))
+                a
+        }
     deriving (Functor, Applicative, Monad, Alternative, MonadPlus)
 
 instance MonadTrans UnifierT where
-    lift = UnifierT . lift . lift
+    lift = UnifierT . lift . lift . lift
     {-# INLINE lift #-}
 
+deriving instance MonadReader (ConditionSimplifier (UnifierT m)) (UnifierT m)
+
 deriving instance MonadLog m => MonadLog (UnifierT m)
 
 deriving instance MonadSMT m => MonadSMT (UnifierT m)
@@ -65,39 +82,39 @@ deriving instance MonadSMT m => MonadSMT (UnifierT m)
 deriving instance MonadProfiler m => MonadProfiler (UnifierT m)
 
 instance MonadSimplify m => MonadSimplify (UnifierT m) where
-    localSimplifierTermLike locally =
-        \(UnifierT branchT) ->
-            UnifierT
+    localSimplifierTermLike locally (UnifierT readerT) =
+        UnifierT $
+            mapReaderT
                 (BranchT.mapBranchT
                     (Morph.hoist (localSimplifierTermLike locally))
-                    branchT
                 )
+                readerT
     {-# INLINE localSimplifierTermLike #-}
 
-    localSimplifierAxioms locally =
-        \(UnifierT branchT) ->
-            UnifierT
+    localSimplifierAxioms locally (UnifierT readerT) =
+        UnifierT $
+            mapReaderT
                 (BranchT.mapBranchT
                     (Morph.hoist (localSimplifierAxioms locally))
-                    branchT
                 )
+                readerT
     {-# INLINE localSimplifierAxioms #-}
 
-    simplifyCondition sideCondition condition =
-        simplifyCondition' sideCondition condition
-      where
-        ConditionSimplifier simplifyCondition' =
-            ConditionSimplifier.create substitutionSimplifier
+    simplifyCondition sideCondition condition = do
+        ConditionSimplifier conditionSimplifier <- ask
+        conditionSimplifier sideCondition condition
     {-# INLINE simplifyCondition #-}
 
 instance MonadSimplify m => MonadUnify (UnifierT m) where
-    throwUnificationError = UnifierT . lift . Error.throwError
+    throwUnificationError = UnifierT . lift . lift . Error.throwError
     {-# INLINE throwUnificationError #-}
 
-    gather = UnifierT . lift . BranchT.gather . getUnifierT
+    gather (UnifierT readerT) =
+        UnifierT $ mapReaderT (lift . BranchT.gather) readerT
     {-# INLINE gather #-}
 
-    scatter = UnifierT . BranchT.scatter
+    scatter ta =
+        UnifierT . ReaderT $ const (BranchT.scatter ta)
     {-# INLINE scatter #-}
 
 -- | Lower an 'ExceptT UnificationError' into a 'MonadUnify'.
@@ -109,11 +126,34 @@ lowerExceptT e = runExceptT e >>= either throwUnificationError pure
 
 runUnifierT
     :: MonadSimplify m
-    => UnifierT m a
+    => NotSimplifier (UnifierT m)
+    -> UnifierT m a
     -> m (Either UnificationError [a])
-runUnifierT = runExceptT . BranchT.gather . getUnifierT
+runUnifierT notSimplifier =
+    runExceptT
+    . BranchT.gather
+    . evalEnvUnifierT notSimplifier
 
 {- | Run a 'Unifier', returning 'Nothing' upon error.
  -}
-maybeUnifierT :: MonadSimplify m => UnifierT m a -> MaybeT m [a]
-maybeUnifierT = hushT . BranchT.gather . getUnifierT
+maybeUnifierT
+    :: MonadSimplify m
+    => NotSimplifier (UnifierT m)
+    -> UnifierT m a
+    -> MaybeT m [a]
+maybeUnifierT notSimplifier =
+    hushT
+    . BranchT.gather
+    . evalEnvUnifierT notSimplifier
+
+evalEnvUnifierT
+    :: MonadSimplify m
+    => NotSimplifier (UnifierT m)
+    -> UnifierT m a
+    -> BranchT (ExceptT UnificationError m) a
+evalEnvUnifierT notSimplifier =
+    flip runReaderT conditionSimplifier
+    . getUnifierT
+  where
+    conditionSimplifier =
+        ConditionSimplifier.create (substitutionSimplifier notSimplifier)
diff --git a/kore/test/Test/Kore/Builtin/Bool.hs b/kore/test/Test/Kore/Builtin/Bool.hs
index 20a6474e10..eee8305787 100644
--- a/kore/test/Test/Kore/Builtin/Bool.hs
+++ b/kore/test/Test/Kore/Builtin/Bool.hs
@@ -35,6 +35,7 @@ import Kore.Internal.TermLike
 import Kore.Step.Simplification.Data
     ( runSimplifier
     )
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Unification.UnifierT
     ( runUnifierT
     )
@@ -171,7 +172,7 @@ test_termAndEquals =
     run =
         runNoSMT
         . runSimplifier testEnv
-        . runUnifierT
+        . runUnifierT Not.notSimplifier
         . runMaybeT
 
     expectRight (Right r) = return r
diff --git a/kore/test/Test/Kore/Builtin/Endianness.hs b/kore/test/Test/Kore/Builtin/Endianness.hs
index 7d05a48864..ced1225fc7 100644
--- a/kore/test/Test/Kore/Builtin/Endianness.hs
+++ b/kore/test/Test/Kore/Builtin/Endianness.hs
@@ -23,6 +23,7 @@ import Kore.Step.Simplification.AndTerms
 import Kore.Step.Simplification.Data
     ( runSimplifier
     )
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Unification.Error
     ( UnificationError
     )
@@ -116,5 +117,5 @@ unify
 unify term1 term2 =
     runNoSMT
     $ runSimplifier testEnv
-    $ runUnifierT
-    $ termUnification term1 term2
+    $ runUnifierT Not.notSimplifier
+    $ termUnification Not.notSimplifier term1 term2
diff --git a/kore/test/Test/Kore/Builtin/Set.hs b/kore/test/Test/Kore/Builtin/Set.hs
index 7fb78efbf2..c661e299df 100644
--- a/kore/test/Test/Kore/Builtin/Set.hs
+++ b/kore/test/Test/Kore/Builtin/Set.hs
@@ -114,6 +114,7 @@ import Kore.Step.RulePattern as RulePattern
 import Kore.Step.Simplification.AndTerms
     ( termUnification
     )
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Syntax.Id
     ( Id
     )
@@ -1783,8 +1784,8 @@ unifiedBy (termLike1, termLike2) substitution testName =
     testCase testName $ do
         Right actual <-
             runSimplifier testEnv
-            $ runUnifierT
-            $ termUnification termLike1 termLike2
+            $ runUnifierT Not.notSimplifier
+            $ termUnification Not.notSimplifier termLike1 termLike2
         liftIO $ assertEqual "" [expect] (Pattern.withoutTerm <$> actual)
   where
     expect = Condition.fromSubstitution $ Substitution.unsafeWrap substitution
diff --git a/kore/test/Test/Kore/Builtin/Signedness.hs b/kore/test/Test/Kore/Builtin/Signedness.hs
index e68a9b6448..c57bff6744 100644
--- a/kore/test/Test/Kore/Builtin/Signedness.hs
+++ b/kore/test/Test/Kore/Builtin/Signedness.hs
@@ -23,6 +23,7 @@ import Kore.Step.Simplification.AndTerms
 import Kore.Step.Simplification.Data
     ( runSimplifier
     )
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Unification.Error
     ( UnificationError
     )
@@ -116,5 +117,5 @@ unify
 unify term1 term2 =
     runNoSMT
     $ runSimplifier testEnv
-    $ runUnifierT
-    $ termUnification term1 term2
+    $ runUnifierT Not.notSimplifier
+    $ termUnification Not.notSimplifier term1 term2
diff --git a/kore/test/Test/Kore/Step/Simplification/And.hs b/kore/test/Test/Kore/Step/Simplification/And.hs
index 9e190c5d34..4d4ecd9cd8 100644
--- a/kore/test/Test/Kore/Step/Simplification/And.hs
+++ b/kore/test/Test/Kore/Step/Simplification/And.hs
@@ -33,6 +33,7 @@ import qualified Kore.Internal.SideCondition as SideCondition
 import qualified Kore.Internal.Substitution as Substitution
 import Kore.Internal.TermLike
 import Kore.Step.Simplification.And
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Variables.UnifiedVariable
     ( UnifiedVariable (..)
     )
@@ -621,7 +622,8 @@ findSort [] = testSort
 findSort ( Conditional {term} : _ ) = termLikeSort term
 
 evaluate :: And Sort (OrPattern Variable) -> IO (OrPattern Variable)
-evaluate = runSimplifier Mock.env . simplify SideCondition.top
+evaluate =
+    runSimplifier Mock.env . simplify Not.notSimplifier SideCondition.top
 
 evaluatePatterns
     :: Pattern Variable
@@ -630,4 +632,4 @@ evaluatePatterns
 evaluatePatterns first second =
     fmap OrPattern.fromPatterns
     $ runSimplifierBranch Mock.env
-    $ makeEvaluate SideCondition.top first second
+    $ makeEvaluate Not.notSimplifier SideCondition.top first second
diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs
index f606796745..8659e8bcfa 100644
--- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs
+++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs
@@ -57,6 +57,7 @@ import Kore.Step.Simplification.AndTerms
 import Kore.Step.Simplification.Equals
     ( termEquals
     )
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Step.Simplification.Simplify
 import Kore.Syntax.Sentence
     ( SentenceAlias
@@ -1271,8 +1272,13 @@ unify first second =
         -- The unification error is discarded because, for testing purposes, we
         -- are not interested in the /reason/ unification failed. For the tests,
         -- the failure is almost always due to unsupported patterns anyway.
-        MaybeT . fmap Error.hush . Monad.Unify.runUnifierT
-        $ termUnification (simplifiedTerm first) (simplifiedTerm second)
+        MaybeT
+        . fmap Error.hush
+        . Monad.Unify.runUnifierT Not.notSimplifier
+        $ termUnification
+            Not.notSimplifier
+            (simplifiedTerm first)
+            (simplifiedTerm second)
 
 simplify
     :: TermLike Variable
@@ -1280,7 +1286,7 @@ simplify
     -> IO [Pattern Variable]
 simplify first second =
     runSimplifierBranch mockEnv
-    $ termAnd (simplifiedTerm first) (simplifiedTerm second)
+    $ termAnd Not.notSimplifier (simplifiedTerm first) (simplifiedTerm second)
   where
     mockEnv = Mock.env
 
diff --git a/kore/test/Test/Kore/Step/Simplification/SubstitutionSimplifier.hs b/kore/test/Test/Kore/Step/Simplification/SubstitutionSimplifier.hs
index baadf856ed..4e99a5a54e 100644
--- a/kore/test/Test/Kore/Step/Simplification/SubstitutionSimplifier.hs
+++ b/kore/test/Test/Kore/Step/Simplification/SubstitutionSimplifier.hs
@@ -18,6 +18,7 @@ import Kore.Internal.Substitution
     )
 import qualified Kore.Internal.Substitution as Substitution
 import Kore.Internal.TermLike
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Step.Simplification.SubstitutionSimplifier
     ( SubstitutionSimplifier (..)
     )
@@ -207,9 +208,9 @@ test_SubstitutionSimplifier =
                     (all Substitution.isNormalized actualSubstitutions)
             , testCase "unification" $ do
                 let SubstitutionSimplifier { simplifySubstitution } =
-                        Unification.substitutionSimplifier
+                        Unification.substitutionSimplifier Not.notSimplifier
                 actual <-
-                    runSimplifier Mock.env . runUnifierT
+                    runSimplifier Mock.env . runUnifierT Not.notSimplifier
                     $ simplifySubstitution SideCondition.top input
                 let expect1 = Right . Condition.fromNormalizationSimplified
                     expect
diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs
index 2e6ae34d6c..478d625165 100644
--- a/kore/test/Test/Kore/Unification/Unifier.hs
+++ b/kore/test/Test/Kore/Unification/Unifier.hs
@@ -45,6 +45,7 @@ import Kore.Step.Simplification.Data
     ( Env (..)
     , runSimplifier
     )
+import qualified Kore.Step.Simplification.Not as Not
 import qualified Kore.Step.Simplification.Pattern as Pattern
 import Kore.Step.Simplification.Simplify
     ( BuiltinAndAxiomSimplifierMap
@@ -192,7 +193,8 @@ simplifyAnds
     => NonEmpty (TermLike Variable)
     -> unifier (Pattern Variable)
 simplifyAnds =
-    SubstitutionSimplifier.simplifyAnds Unification.unificationMakeAnd
+    SubstitutionSimplifier.simplifyAnds
+        (Unification.unificationMakeAnd Not.notSimplifier)
 
 andSimplifySuccess
     :: HasCallStack
@@ -205,7 +207,7 @@ andSimplifySuccess term1 term2 results = do
     Right subst' <-
         runNoSMT
         $ runSimplifier testEnv
-        $ Monad.Unify.runUnifierT
+        $ Monad.Unify.runUnifierT Not.notSimplifier
         $ simplifyAnds (unificationProblem term1 term2 :| [])
     assertEqual (message expect subst') expect subst'
   where
@@ -233,7 +235,7 @@ andSimplifyFailure term1 term2 err = do
     actual <-
         runNoSMT
         $ runSimplifier testEnv
-        $ Monad.Unify.runUnifierT
+        $ Monad.Unify.runUnifierT Not.notSimplifier
         $ simplifyAnds (unificationProblem term1 term2 :| [])
     assertEqual "" (show expect) (show actual)
 
@@ -250,7 +252,7 @@ andSimplifyException message term1 term2 exceptionMessage =
         test = do
             assignment <-
                 runNoSMT $ runSimplifier testEnv
-                $ Monad.Unify.runUnifierT
+                $ Monad.Unify.runUnifierT Not.notSimplifier
                 $ simplifyAnds (unificationProblem term1 term2 :| [])
             _ <- evaluate assignment
             assertFailure "This evaluation should fail"
@@ -278,7 +280,7 @@ unificationProcedureSuccessWithSimplifiers
                 SideCondition.topTODO
                 term1
                 term2
-            & Monad.Unify.runUnifierT
+            & Monad.Unify.runUnifierT Not.notSimplifier
             & runSimplifier mockEnv
             & runNoSMT
         let
diff --git a/kore/test/Test/Kore/Unification/UnifierT.hs b/kore/test/Test/Kore/Unification/UnifierT.hs
index f71f23a482..2691f00753 100644
--- a/kore/test/Test/Kore/Unification/UnifierT.hs
+++ b/kore/test/Test/Kore/Unification/UnifierT.hs
@@ -39,6 +39,7 @@ import qualified Kore.Step.Simplification.Condition as Condition
 import Kore.Step.Simplification.Data
     ( Env (..)
     )
+import qualified Kore.Step.Simplification.Not as Not
 import qualified Kore.Step.Simplification.Simplify as Simplifier
 import Kore.Unification.Error
 import qualified Kore.Unification.UnifierT as Monad.Unify
@@ -365,7 +366,7 @@ merge
     (Substitution.mkUnwrappedSubstitution -> s2)
   =
     Test.runSimplifier mockEnv
-    $ Monad.Unify.runUnifierT
+    $ Monad.Unify.runUnifierT Not.notSimplifier
     $ mergeSubstitutionsExcept
     $ Substitution.wrap
     . fmap simplifiedAssignment
@@ -401,7 +402,7 @@ normalizeExcept
 normalizeExcept predicated =
     (fmap . fmap) MultiOr.make
     $ Test.runSimplifier mockEnv
-    $ Monad.Unify.runUnifierT
+    $ Monad.Unify.runUnifierT Not.notSimplifier
     $ Branch.alternate
     $ Simplifier.simplifyCondition SideCondition.top predicated
   where