diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 1e117e9ff..e8e8471c0 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -57,7 +57,7 @@ namespace polysat {
             if (!m_out)
                 m_out = alloc(std::ofstream, "conflicts.txt");
             else
-                out() << "\n\n\n\n\n" << hline() << "\n" << hline() << "\n" << hline() << "\n\n\n\n\n";
+                out() << "\n\n\n\n\n\n\n\n\n\n\n\n";
             out() << "CONFLICT #" << ++m_conflicts << "\n";
         }
 
@@ -74,13 +74,15 @@ namespace polysat {
                 m_used_constraints.insert(c.blit().index());
             }
             for (auto v : core.vars()) {
-                out_indent() << "v" << v << "\n";
+                out_indent() << "v" << v << " := " << core.s.get_value(v) << "\n";
                 m_used_vars.insert(v);
             }
             for (auto v : core.bail_vars()) {
-                out_indent() << "v" << v << " (bail)\n";
+                out_indent() << "v" << v << " := " << core.s.get_value(v) << " (bail)\n";
                 m_used_vars.insert(v);
             }
+            if (core.is_bailout())
+                out_indent() << "(bailout)\n";
             out().flush();
         }
 
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 58a3e5dea..109ef701c 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -106,6 +106,7 @@ namespace polysat {
         uint_set m_vars;                    // variable assignments used as premises
         uint_set m_bail_vars;
 
+        friend class inference_logger;
         scoped_ptr<inference_logger> m_logger;
 
         // If this is not null_var, the conflict was due to empty viable set for this variable.
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 00559aaab..a902a7c63 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -143,6 +143,17 @@ namespace polysat {
         }
     }
 
+    struct inference_sup : public inference {
+        const char* name;
+        pvar var;
+        signed_constraint reduced;
+        signed_constraint reducer;
+        inference_sup(const char* name, pvar var, signed_constraint reduced, signed_constraint reducer) : name(name), var(var), reduced(reduced), reducer(reducer) {}
+        std::ostream& display(std::ostream& out) const override {
+            return out << "Superposition " << name << ", reduced v" << var << " in   " << reduced << "   by   " << reducer;
+        }
+    };
+
     bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict& core) {
         pdd p = eq.eq();
         LOG("using v" << v << " " << eq);
@@ -189,7 +200,7 @@ namespace polysat {
                 return true;
             }
             core.set(c2);
-            core.log_inference("superposition 5");
+            core.log_inference(inference_sup("5", v, c, eq));
             return true;
         }
         return false;