diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index 9bd812cb72a85f0d082722aa54596242cd50d2fc..80e053d43106dc8bf4d0b7a224623fa30b9f742e 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -56,7 +56,7 @@ let runSatCheckVerbose (sc:satCheck) =
     let cs = colored_string in
     let sotr = terminal_string_of_testResult in
     let (expectation,_,title) = sc in
-    PF.printf "Is %s " (cs "1" (columnCreate 50 title));
+    PF.printf "Is %s " (cs "1" (columnCreate 60 title));
     PF.printf "%s? → " (sotr expectation);
     let res = runSatCheck sc in
     (if (res = expectation)
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 7d0f14480db1749a330a7958c0d404084ba55f5d..e8517d48929edb6c93a7a4d07b8388e3b331c355 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -23,8 +23,15 @@ let k_testcases: satCheck list =
     ; c Unsat "<R> ((<R> C) & (<S> False))"
     ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
     ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
-
-    (* Some DL98-Testcases *)
+    ; c Sat   "<R> A & <R> B |- [R] C"
+    ; c Unsat "<R> A & <R> B |- [R] (~A & ~B)"
+    ; c Unsat "<R> A & <R> B |- [R] ~B"
+    ; c Sat   "<R> A & <R> ~A |- [R] B"
+    ; c Unsat "<R> A & <R> ~A & (B => [R] ~A) |- [R] B"
+    ; c Sat   "<R> A & <R> ~A & (B => [R] ~A) & (C => ~D) & (D => ~E) & <R> C & <R> D & <R> E |- True"
+    ; c Unsat "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
+    ; c Sat   "(<R> D | <R> E) & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
+    ; c Sat   "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & (D & E => <R> ~(D&E)) |- True"
     ]