diff --git a/lltodk.ml b/lltodk.ml
index 8aeaee5..dd51dde 100644
--- a/lltodk.ml
+++ b/lltodk.ml
@@ -1073,4 +1073,5 @@ let output_term oc phrases _ llp =
   fprintf oc "zenon.nnpp (%a)\n(%a)"
     print_dk_term dkgoal print_dk_term dkproof;
   if !Globals.signature_name <> "" then fprintf oc ".";
+  fprintf oc "\n";
   []
diff --git a/main.ml b/main.ml
index 831c68b..6ee841d 100644
--- a/main.ml
+++ b/main.ml
@@ -19,6 +19,7 @@ type szs_error =
     NoSuccess
   | Unknown
   | ResourceOut
+  | GaveUp
 
 type szs_status =
     Suc of szs_success
@@ -33,6 +34,7 @@ let szs_status out (status, file) =
       | Err NoSuccess -> fprintf out "NoSuccess"
       | Err Unknown -> fprintf out "Unknown"
       | Err ResourceOut -> fprintf out "ResourceOut"
+      | Err GaveUp -> fprintf out "GaveUp"
     )
     status file
 
@@ -553,7 +555,7 @@ let main () =
   | Prove.NoProof ->
      retcode := 12;
      if not !quiet_flag then
-       print_status (Err Unknown) file
+       print_status (Err GaveUp) file
   | Prove.LimitsExceeded ->
      retcode := 13;
      if not !quiet_flag then