diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp
index 1aee09f3f..c8a048a6a 100644
--- a/src/muz_qe/duality_dl_interface.cpp
+++ b/src/muz_qe/duality_dl_interface.cpp
@@ -240,6 +240,10 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
     out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]);
   out << ")\n";
 
+  // print the rule number
+
+  out << " rule!" << node.Outgoing->map->number;
+
   // print the substitution
 
   out << "  (subst\n";