diff --git a/CMakeLists.txt b/CMakeLists.txt
index e498566..1451838 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -8,6 +8,7 @@ set(CMAKE_CXX_STANDARD 17)
 
 option(STATIC_BINARIES "Link binaries statically." ON)
 option(USE_SORELEASE   "Use SORELEASE in shared library filename." ON)
+option(PRINT_PROOFS    "Enable the -c option in the minisat binary to print resolution proofs." ON)
 
 #--------------------------------------------------------------------------------------------------
 # Library version:
@@ -36,6 +37,13 @@ include_directories(${minisat_SOURCE_DIR})
 
 add_definitions(-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS)
 
+#--------------------------------------------------------------------------------------------------
+# Macro switches:
+
+if(PRINT_PROOFS)
+    add_compile_definitions(ENABLE_PROOF)
+endif()
+
 #--------------------------------------------------------------------------------------------------
 # Build Targets:
 
diff --git a/src/Main.C b/src/Main.C
index f188264..7069089 100644
--- a/src/Main.C
+++ b/src/Main.C
@@ -231,18 +231,24 @@ struct Checker : public ProofTraverser {
     vec<vec<Lit> >  clauses;
 
     void root   (const vec<Lit>& c) {
-        //**/printf("%d: ROOT", clauses.size()); for (int i = 0; i < c.size(); i++) printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");
+#ifdef ENABLE_PROOF
+        printf("%d: ROOT", clauses.size()); for (int i = 0; i < c.size(); i++) printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");
+#endif
         clauses.push();
         c.copyTo(clauses.last()); }
 
     void chain  (const vec<ClauseId>& cs, const vec<Var>& xs) {
-        //**/printf("%d: CHAIN %d", clauses.size(), cs[0]); for (int i = 0; i < xs.size(); i++) printf(" [%d] %d", xs[i]+1, cs[i+1]);
+#ifdef ENABLE_PROOF
+        printf("%d: CHAIN %d", clauses.size(), cs[0]); for (int i = 0; i < xs.size(); i++) printf(" [%d] %d", xs[i]+1, cs[i+1]);
+#endif
         clauses.push();
         vec<Lit>& c = clauses.last();
         clauses[cs[0]].copyTo(c);
         for (int i = 0; i < xs.size(); i++)
             resolve(c, clauses[cs[i+1]], xs[i]);
-        //**/printf(" =>"); for (int i = 0; i < c.size(); i++) printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");
+#ifdef ENABLE_PROOF
+        printf(" =>"); for (int i = 0; i < c.size(); i++) printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");
+#endif
         }
 
     void deleted(ClauseId c) {