diff --git a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp
index 049f6f13529..85a44d3ecf4 100644
--- a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp
+++ b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp
@@ -149,6 +149,56 @@ Node ArithNlCompareProofGenerator::getCompareLit(const Node& olit)
   return olit.getAttribute(ancla);
 }
 
+Kind ArithNlCompareProofGenerator::decomposeCompareLit(const Node& lit, bool isAbsolute, std::vector<Node>& a, std::vector<Node>& b)
+{
+  Kind k = lit.getKind();
+  if (k!=Kind::EQUAL && k!=Kind::GT && k!=Kind::GEQ && k!=Kind::LT && k!=Kind::LEQ)
+  {
+    return Kind::UNDEFINED_KIND;
+  }
+  if (isAbsolute)
+  {
+    if (lit[0].getKind()!=Kind::ABS || lit[1].getKind()!=Kind::ABS)
+    {
+      return Kind::UNDEFINED_KIND;
+    }
+    a.emplace_back(lit[0][0]);
+    b.emplace_back(lit[1][0]);
+  }
+  else
+  {
+    a.emplace_back(lit[0]);
+    b.emplace_back(lit[1]);
+  }
+  return k;
+}
+
+Kind ArithNlCompareProofGenerator::combineRelation(Kind k1, Kind k2)
+{
+  if (k2==Kind::EQUAL)
+  {
+    return k1;
+  }
+  if (k1==Kind::EQUAL)
+  {
+    return k2;
+  }
+  if (k1==k2)
+  {
+    return k1;
+  }
+  if ((k1==Kind::GT && k2==Kind::GEQ) || (k2==Kind::GT && k1==Kind::GEQ))
+  {
+    return Kind::GT ;
+  }
+  else 
+  if ((k1==Kind::LT && k2==Kind::LEQ) || (k2==Kind::LT && k1==Kind::LEQ))
+  {
+    return Kind::LT;
+  }
+  return Kind::UNDEFINED_KIND;  
+}
+
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
diff --git a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h
index 9b6f75a72e5..35ca60cff1f 100644
--- a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h
+++ b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h
@@ -46,6 +46,10 @@ class ArithNlCompareProofGenerator : protected EnvObj, public ProofGenerator
                             bool isAbsolute);
   /** */
   static Node getCompareLit(const Node& olit);
+  /** */
+  static Kind decomposeCompareLit(const Node& lit, bool isAbsolute, std::vector<Node>& a, std::vector<Node>& b);
+  /** */
+  static Kind combineRelation(Kind k1, Kind k2);
 };
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp
index b4ca8bc889e..6b0833800cb 100644
--- a/src/theory/arith/nl/ext/proof_checker.cpp
+++ b/src/theory/arith/nl/ext/proof_checker.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/sequence.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/ext/arith_nl_compare_proof_gen.h"
 #include "theory/rewriter.h"
 
 using namespace cvc5::internal::kind;
@@ -156,6 +157,40 @@ Node ExtProofRuleChecker::checkInternal(ProofRule id,
   else if (id == ProofRule::MACRO_ARITH_NL_COMPARISON
            || id == ProofRule::MACRO_ARITH_NL_ABS_COMPARISON)
   {
+    bool isAbs = (id == ProofRule::MACRO_ARITH_NL_ABS_COMPARISON);
+    std::vector<Node> eproda;
+    std::vector<Node> eprodb;
+    Kind k = Kind::EQUAL;
+    std::vector<Node> deq;
+    for (const Node& c : children)
+    {
+      Kind ck = c.getKind();
+      if (ck==Kind::NOT && c[0].getKind()==Kind::EQUAL)
+      {
+        deq.emplace_back(c);
+        continue;
+      }
+      ck = ArithNlCompareProofGenerator::decomposeCompareLit(c, isAbs, eproda, eprodb);
+      if (ck==Kind::UNDEFINED_KIND)
+      {
+        return Node::null();
+      }
+      // combine the implied relation
+      k = ArithNlCompareProofGenerator::combineRelation(k, ck);
+      if (k==Kind::UNDEFINED_KIND)
+      {
+        return Node::null();
+      }
+    }
+    std::vector<Node> cproda;
+    std::vector<Node> cprodb;
+    Kind ck = ArithNlCompareProofGenerator::decomposeCompareLit(args[0], isAbs, cproda, cprodb);
+    if (ck!=k)
+    {
+      return Node::null();
+    }
+    
+    
     return args[0];
   }
   return Node::null();