diff --git a/kore/src/Kore/Step/Simplification/Iff.hs b/kore/src/Kore/Step/Simplification/Iff.hs
index abd04e6f88..f9356fb4ef 100644
--- a/kore/src/Kore/Step/Simplification/Iff.hs
+++ b/kore/src/Kore/Step/Simplification/Iff.hs
@@ -13,6 +13,7 @@ module Kore.Step.Simplification.Iff (
     simplifyEvaluated,
 ) where
 
+import qualified Kore.Internal.MultiAnd as MultiAnd
 import Kore.Internal.OrPattern (
     OrPattern,
  )
@@ -30,8 +31,15 @@ import qualified Kore.Internal.TermLike as TermLike (
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
+import qualified Kore.Step.Simplification.And as And (
+    simplify,
+ )
+import qualified Kore.Step.Simplification.Implies as Implies (
+    simplifyEvaluated,
+ )
 import qualified Kore.Step.Simplification.Not as Not (
     makeEvaluate,
+    notSimplifier,
     simplifyEvaluated,
  )
 import Kore.Step.Simplification.Simplify
@@ -83,13 +91,15 @@ simplifyEvaluated
         | OrPattern.isFalse first = Not.simplifyEvaluated sideCondition second
         | OrPattern.isTrue second = return first
         | OrPattern.isFalse second = Not.simplifyEvaluated sideCondition first
-        | otherwise =
-            return $ case (firstPatterns, secondPatterns) of
-                ([firstP], [secondP]) -> makeEvaluate firstP secondP
-                _ ->
-                    makeEvaluate
-                        (OrPattern.toPattern first)
-                        (OrPattern.toPattern second)
+        | otherwise = case (firstPatterns, secondPatterns) of
+            ([firstP], [secondP]) -> return $ makeEvaluate firstP secondP
+            _ -> do
+                fwd <- Implies.simplifyEvaluated sideCondition first second
+                bwd <- Implies.simplifyEvaluated sideCondition second first
+                And.simplify
+                    Not.notSimplifier
+                    sideCondition
+                    (MultiAnd.make [fwd, bwd])
       where
         firstPatterns = toList first
         secondPatterns = toList second
diff --git a/kore/test/Test/Kore/Step/Simplification/Integration.hs b/kore/test/Test/Kore/Step/Simplification/Integration.hs
index 717a18aa03..c3fe2fda6c 100644
--- a/kore/test/Test/Kore/Step/Simplification/Integration.hs
+++ b/kore/test/Test/Kore/Step/Simplification/Integration.hs
@@ -541,7 +541,7 @@ test_simplificationIntegration =
                 )
                     [ [fromNot cfCeil, fromNot chCeil]
                     , [chCeil, cgCeil, cfCeil]
-                    , [chCeil, cfCeil]
+                    , [chCeil, cfCeil, fromNot cgCeil]
                     ]
             cfCeil = makeCeilPredicate Mock.cf
             cgCeil = makeCeilPredicate Mock.cg