diff --git a/clausesets.c b/clausesets.c
index 7281040..e5d57af 100644
--- a/clausesets.c
+++ b/clausesets.c
@@ -1524,7 +1524,7 @@ int solve0(satinstance sati,int conflictstogo,int restart) {
   sati->value = 0;
   return 0;
  SAT:
-  printf("SAT (%i decisions %i conflicts)\n",sati->decisions,sati->conflicts);
+  printf("SAT (%i ID %i decisions %i conflicts %i variables)\n",sati->id,sati->decisions,sati->conflicts,sati->nOfVars);
 #ifdef COSTS
   printf("FINAL COST %i.\n",sati->currentcost);
   sati->costbound = sati->currentcost;
diff --git a/main.c b/main.c
index 9f251fa..4d58d9a 100644
--- a/main.c
+++ b/main.c
@@ -736,10 +736,10 @@ int main(int argc,char **argv) {
   printf("max. learned clause length %i\n",stats_longest_learned);
 
   if(flagOutputDIMACS == 0) {
-    printf("t val conflicts decisions\n");
+    printf("t val conflicts decisions variables\n");
     i = 0;
     do {
-      printf("%i %i %i %i\n",seqs[i].sati->nOfTPoints-1,seqs[i].sati->value,seqs[i].sati->conflicts,seqs[i].sati->decisions);
+      printf("%i %i %i %i %i\n",seqs[i].sati->nOfTPoints-1,seqs[i].sati->value,seqs[i].sati->conflicts,seqs[i].sati->decisions,seqs[i].sati->nOfVars);
       i += 1;
     } while(i*outputTimeStep+firstTimePoint <= lastTimePoint && seqs[i].sati && seqs[i-1].sati->value != 1);
       //    } while(i*outputTimeStep+firstTimePoint < lastTimePoint);