diff --git a/src/main.c b/src/main.c
index 6538db5..d25236c 100644
--- a/src/main.c
+++ b/src/main.c
@@ -60,6 +60,7 @@ enum exittypes
 #include "binding.h"
 #include "switches.h"
 #include "specialterm.h"
+#include "color.h"
 
 // The global system state
 System sys;
@@ -103,6 +104,9 @@ main (int argc, char **argv)
   /* process any command-line switches */
   switchesInit (argc, argv);
 
+  /* process colors */
+  colorInit ();
+
   /* start system */
   sys = systemInit ();
 
@@ -267,6 +271,7 @@ main (int argc, char **argv)
     }
   knowledgeDestroy (sys->know);
   systemDone (sys);
+  colorDone ();
   compilerDone ();
 
   /* done symbols */
@@ -285,6 +290,37 @@ exit:
   return exitcode;
 }
 
+//! Print something bad
+void
+printBad (char *s)
+{
+  eprintf ("%s%s%s", COLOR_Red, s, COLOR_Reset);
+}
+
+//! Print something good
+void
+printGood (char *s)
+{
+  eprintf ("%s%s%s", COLOR_Green, s, COLOR_Reset);
+}
+
+//! Print state (existState, isAttack)
+/**
+ * Fail == ( existState xor isAttack )
+ */
+void
+printOkFail (int existState, int isAttack)
+{
+  if (existState != isAttack)
+    {
+      printGood ("Ok");
+    }
+  else
+    {
+      printBad ("Fail");
+    }
+}
+
 //! Display time and state space size information using ASCII.
 /**
  * Displays also whether an attack was found or not.
@@ -379,7 +415,17 @@ timersPrint (const System sys)
 	  Term pname;
 	  Term rname;
 	  Termlist labellist;
+	  int isAttack;		// stores whether this claim failure constitutes an attack or not
 
+	  if (isTermEqual (cl_scan->type, CLAIM_Reachable))
+	    {
+	      // An attack on reachable is not really an attack, we're just generating the state space
+	      isAttack = false;
+	    }
+	  else
+	    {
+	      isAttack = true;
+	    }
 	  anyclaims = true;
 
 	  eprintf ("claim\t");
@@ -452,20 +498,10 @@ timersPrint (const System sys)
 
 	  /* now report the status */
 	  eprintf ("\t");
-	  eprintf ("attacks: ");
 	  if (cl_scan->count > 0 && cl_scan->failed > 0)
 	    {
-	      /* there is an attack */
-	      if (!isTermEqual (cl_scan->type, CLAIM_Reachable))
-		{
-		  /* a normal claim */
-		  eprintf ("yes");
-		}
-	      else
-		{
-		  /* Reachable is not an attack */
-		  eprintf ("no");
-		}
+	      /* there is a state */
+	      printOkFail (true, isAttack);
 
 	      eprintf ("\t");
 	      /* are these all attacks? */
@@ -478,7 +514,15 @@ timersPrint (const System sys)
 		{
 		  eprintf ("at least");
 		}
-	      eprintf (" %i variant", cl_scan->failed);
+	      eprintf (" %i ", cl_scan->failed);
+	      if (isAttack)
+		{
+		  eprintf ("attack");
+		}
+	      else
+		{
+		  eprintf ("variant");
+		}
 	      if (cl_scan->failed != 1)
 		{
 		  eprintf ("s");
@@ -487,8 +531,9 @@ timersPrint (const System sys)
 	    }
 	  else
 	    {
-	      /* no attack */
-	      eprintf ("no\t");
+	      /* no state */
+	      printOkFail (false, isAttack);
+	      eprintf ("\t");
 
 	      /* subcases */
 	      if (cl_scan->count == 0)
@@ -502,7 +547,8 @@ timersPrint (const System sys)
 		  if (cl_scan->complete)
 		    {
 		      /* complete proof */
-		      eprintf ("[proof of correctness]");
+		      eprintf ("[%sproof of correctness%s]", COLOR_Bold,
+			       COLOR_Reset);
 		    }
 		  else
 		    {
diff --git a/src/switches.c b/src/switches.c
index a73bc5e..0d9f87d 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -89,6 +89,7 @@ switchesInit (int argc, char **argv)
   switches.reportStates = 0;
   switches.extendNonReads = 0;	// default off
   switches.extendTrivial = 0;	// default off
+  switches.monochrome = false;	// default colors
 
   // Obsolete
   switches.latex = 0;		// latex output?
@@ -898,6 +899,19 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect (' ', "monochrome", 0))
+    {
+      if (!process)
+	{
+	  helptext ("--monochrome", "disable color terminal output");
+	}
+      else
+	{
+	  switches.monochrome = true;
+	  return index;
+	}
+    }
+
 #ifdef DEBUG
   if (detect ('D', "debug", 1))
     {
diff --git a/src/switches.h b/src/switches.h
index 606660b..3c9bbc0 100644
--- a/src/switches.h
+++ b/src/switches.h
@@ -68,6 +68,7 @@ struct switchdata
   int reportStates;		//!< Progress display switch. (traversed states)
   int extendNonReads;		//!< Show further events in arachne xml output.
   int extendTrivial;		//!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)
+  int monochrome;		//!< Disable color output
 
   //! Latex output switch.
   /**