diff --git a/horname.cabal b/horname.cabal
--- a/horname.cabal
+++ b/horname.cabal
@@ -1,5 +1,5 @@
 name:                horname
-version:             0.1.1.0
+version:             0.1.2.0
 synopsis:            Rename function definitions returned by SMT solvers
 description:         Please see README.md
 homepage:            https://github.com/cocreature/horname#readme
diff --git a/src/Horname/Internal/SMT.hs b/src/Horname/Internal/SMT.hs
--- a/src/Horname/Internal/SMT.hs
+++ b/src/Horname/Internal/SMT.hs
@@ -5,6 +5,7 @@
 
 import           Data.Data
 import           Data.List (foldl', find)
+import qualified Data.List as List
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Maybe
@@ -106,6 +107,7 @@
 sumExprs [e] = e
 sumExprs args = List (StringLit "+" : args)
 
+-- first pass of simplifications
 simplify :: SExpr -> SExpr
 -- (* (- 1) x) → x
 simplify (List [StringLit "*", List [StringLit "-", IntLit i], expr]) =
@@ -147,6 +149,32 @@
 simplify (List [StringLit "not", List (StringLit "or":args)]) =
   List (StringLit "and" : map negateExpr args)
 simplify e = e
+
+antiSymmetricOp :: Text -> Bool
+antiSymmetricOp n = n `elem` ["<=",">="]
+-- second pass of simplifications
+simplify' :: SExpr -> SExpr
+-- transform two inequalities to an equality
+simplify' (List (StringLit "and":args)) =
+  List (StringLit "and" : other ++ mergeInequalities inequality)
+  where
+    (inequality, other) =
+      List.partition
+        (\case
+           List [StringLit op, _, _] -> antiSymmetricOp op
+           _ -> False)
+        args
+    mergeInequalities :: [SExpr] -> [SExpr]
+    mergeInequalities [] = []
+    mergeInequalities (e@(List [StringLit op, expr1, expr2]):rest) =
+      let reversedE = List [StringLit op, expr2, expr1]
+      in if reversedE `elem` rest
+           then List [StringLit "=", expr1, expr2] :
+                mergeInequalities (filter (not . (`elem` [e, reversedE])) rest)
+           else e : mergeInequalities rest
+    mergeInequalities (e:es) = e : mergeInequalities es
+simplify' e = e
+
 
 negateExpr :: SExpr -> SExpr
 negateExpr (List [StringLit "not", expr]) = expr
diff --git a/src/Horname/Internal/SMT/Parser.hs b/src/Horname/Internal/SMT/Parser.hs
--- a/src/Horname/Internal/SMT/Parser.hs
+++ b/src/Horname/Internal/SMT/Parser.hs
@@ -78,7 +78,12 @@
   expr <- parseSExpr
   space
   _ <- char ')'
-  pure (DefineFun name args retSort (transform simplify $ inlineLets expr))
+  pure
+    (DefineFun
+       name
+       args
+       retSort
+       (transform simplify' . transform simplify $ inlineLets expr))
 
 parseDefineFuns :: Parser [DefineFun]
 parseDefineFuns = many (try parseDefineFun)