diff --git a/main.c b/main.c
index 0950af1..ff775e0 100644
--- a/main.c
+++ b/main.c
@@ -199,6 +199,66 @@ void processheuristic(char *decls) {
 
 }
 
+void printStatistics()
+{
+  printf("\n\n# statistics in YAML format\n---\n");
+
+  printf("runtime:\n  total: %.2f # [s]\n  preprocessing: %.2f # [s]\n",
+	 time2real(time10ms() - TIMEstart),
+	 time2real(TIMEpreprocess - TIMEstart));
+
+  givememorystatistics();
+
+  printf("maxLearnedClauseLength: %i\n",stats_longest_learned);
+
+  int solutionIndex = -1;
+
+  for (int i = 0; seqs[i].sati; i++)
+  {
+    if (seqs[i].sati->value != 1)
+      continue;
+
+    solutionIndex = i;
+    break;
+  }
+
+  const auto planLength = seqs[solutionIndex].sati->nOfTPoints - 1;
+
+  int numberOfActions = 0;
+
+  const satinstance sati = seqs[solutionIndex].sati;
+
+  for (int t = 0; t < sati->nOfTPoints - 1; t++)
+    for (int i = 0; i < sati->nOfActions; i++)
+      if (vartruep(sati,TACT(i,t)))
+        numberOfActions++;
+
+  printf("plan:\n  length: %i\n  actions: %i\n", planLength, numberOfActions);
+
+  if(flagOutputDIMACS == 0) {
+    printf("iterations:\n");
+    int i = 0;
+    do {
+      printf("  - horizon: %i\n",seqs[i].sati->nOfTPoints-1);
+      printf("    result: ");
+      if (seqs[i].sati->value == 0)
+        printf("unsatisfiable");
+      else if (seqs[i].sati->value == 1)
+        printf("satisfiable");
+      else
+        printf("unknown");
+      printf("\n");
+      printf("    conflicts: %i\n",seqs[i].sati->conflicts);
+      printf("    decisions: %i\n",seqs[i].sati->decisions);
+      printf("    variables: %i\n",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);
+  }
+
+  printf("...\n");
+}
+
 int main(int argc,char **argv) {
   int i,j;
 
@@ -715,62 +775,7 @@ int main(int argc,char **argv) {
 
   encoding();
 
-  printf("\n\n# statistics in YAML format\n---\n");
-
-  printf("runtime:\n  total: %.2f # [s]\n  preprocessing: %.2f # [s]\n",
-	 time2real(time10ms() - TIMEstart),
-	 time2real(TIMEpreprocess - TIMEstart));
-
-  givememorystatistics();
-
-  printf("maxLearnedClauseLength: %i\n",stats_longest_learned);
-
-  int solutionIndex = -1;
-
-  for (int i = 0; seqs[i].sati; i++)
-  {
-    if (seqs[i].sati->value != 1)
-      continue;
-
-    solutionIndex = i;
-    break;
-  }
-
-  const auto planLength = seqs[solutionIndex].sati->nOfTPoints - 1;
-
-  int numberOfActions = 0;
-
-  const satinstance sati = seqs[solutionIndex].sati;
-
-  for (int t = 0; t < sati->nOfTPoints - 1; t++)
-    for (int i = 0; i < sati->nOfActions; i++)
-      if (vartruep(sati,TACT(i,t)))
-        numberOfActions++;
-
-  printf("plan:\n  length: %i\n  actions: %i\n", planLength, numberOfActions);
-
-  if(flagOutputDIMACS == 0) {
-    printf("iterations:\n");
-    i = 0;
-    do {
-      printf("  - horizon: %i\n",seqs[i].sati->nOfTPoints-1);
-      printf("    result: ");
-      if (seqs[i].sati->value == 0)
-        printf("unsatisfiable");
-      else if (seqs[i].sati->value == 1)
-        printf("satisfiable");
-      else
-        printf("unknown");
-      printf("\n");
-      printf("    conflicts: %i\n",seqs[i].sati->conflicts);
-      printf("    decisions: %i\n",seqs[i].sati->decisions);
-      printf("    variables: %i\n",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);
-  }
-
-  printf("...\n");
+  printStatistics();
 
  }