diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index a69c40f1d..68b3f1e4d 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -880,6 +880,17 @@ namespace datalog {
         return r;
     }
 
+    bool context::is_monotone() {
+        try {
+            m_rule_properties.check_for_negated_predicates();
+            return true;
+        }
+        catch (...) {
+            return false;
+        }
+    }
+
+
     lbool context::query_from_lvl (expr* query, unsigned lvl) {
         m_mc = mk_skip_model_converter();
         m_last_status = OK;
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index adb98592d..5a19bfd43 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -528,6 +528,8 @@ namespace datalog {
          */
         model_ref get_model();
 
+        bool is_monotone();
+
         /**
            \brief retrieve proof from derivation of the query.
 
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index a95fae07a..a50fa692d 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -266,7 +266,10 @@ class horn_tactic : public tactic {
             switch (is_reachable) {
             case l_true: {
                 // goal is unsat
-                if (produce_proofs) {
+                if (!m_ctx.is_monotone()) {
+                    is_reachable = l_undef;
+                }
+                else if (produce_proofs) {
                     proof_ref proof = m_ctx.get_proof();
                     pc = proof2proof_converter(m, proof);
                     g->assert_expr(m.get_fact(proof), proof, nullptr);