diff --git a/coalgcompare.ml b/coalgcompare.ml
index 8356f34c10720f9778d1bbfed7840041b10dcda9..e7f5363d663e20213db07d27e326c06f06444bdb 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -9,6 +9,18 @@ module G = GenAndComp
 module C = CoAlgFormula
 module A = ALCFormula
 
+type solvanswer = ASAT | AUNSAT | ATIMEOUT
+
+type testresults =
+   ((string list) (* solver names *)
+    * ((string * ((solvanswer * int) list)) (*some test case with times for each reasoner*)
+        list))
+
+(* generates the int range from i to j (including) *)
+let (--) i j = 
+    let rec aux n acc =
+      if n < i then acc else aux (n-1) (n :: acc)
+    in aux j []
 
 let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
 
@@ -24,7 +36,7 @@ let _ =
   print_endline (string_of_int (seed))
 
 
-let sorts = Array.make 1 (CoAlgMisc.MultiModalK, [0])
+let sortK = Array.make 1 (CoAlgMisc.MultiModalK, [0])
 
 let nomTable name =
   assert (CoAlgFormula.isNominal name);
@@ -93,8 +105,8 @@ let exportALCQuery tbox (_, f) =
   ([exportALCFormula f], tboxND, [])
 
 
-let solvCoalg args =
-  G.evaluateFkt (fun (tbox, sf) -> CoAlgReasoner.isSat sorts nomTable tbox sf) args
+let solvCoalg sortTable args =
+  G.evaluateFkt (fun (tbox, sf) -> CoAlgReasoner.isSat sortTable nomTable tbox sf) args
 
 let solvALC (tbox, sf) =
   let args = exportALCQuery tbox sf in
@@ -106,14 +118,67 @@ let solvFact (tbox, sf) =
   G.callExt None "FaCT++" ["fact.conf"] (Str.regexp_string "is sat")
 
 let solvers =
-  let _ = [(solvCoalg, "CoAlg"); (solvALC, "alc"); (solvFact, "fact")] in
-  [(solvALC, "alc"); (solvCoalg, "CoAlg")]
-
+  let _ = [(solvCoalg sortK, "CoAlg"); (solvALC, "alc"); (solvFact, "fact")] in
+  [(solvFact, "fact"); (solvCoalg sortK, "CoAlg")]
+
+let printUsage () =
+  print_endline "Usage: \"coalgcompare <logic>\" does tests where";
+  print_endline "       <logic> in { K }";
+  exit 1
+
+let doTestK () : testresults =
+  let sorts = sortK in
+  let solvs = [(solvFact, "fact"); (solvCoalg sortK, "CoAlg")] in
+  (*
+    lF A list of pairs (f, n), e.g. (p, 1).
+    The list must not be empty.
+    lFF A list of pairs (f->f, n), e.g. (~., 1).
+    The list must not be empty.
+    lFFF A list of pairs (f->f->f, n), e.g. (.&., 1).
+    lPFF A list of pairs (p->f->f, n), e.g. (<.>., 1).
+    lP A list of pairs (p, n), e.g. (a, 1).
+    The list must not be empty unless lPFF is also empty.
+    lPP A list of pairs (p->p, n), e.g. ( *., 1).
+    lFP A list of pairs (f->p, n), e.g. (?., 1).
+    lPPP A list of pairs (p->p->p, n), e.g. (.+., 1).
+  *)
+  let timeout = 300 in (* 5 minutes *)
+  let lF = List.map (fun p -> (string_of_int p, 1)) (0--10) in
+  let lFF = [((fun x -> C.NOT x),1)] in
+  let lFFF = [(C.AND,1),(C.OR,1)] in
+  let lPFF = [(C.EX,1),(C.AX,1)] in
+  (* role names *)
+  let lP = List.map (fun p -> (string_of_int p, 1)) (0--10) in
+  let lPP = [] in
+  let lFP = [] in
+  let lPPP = [] in
+  let (genF,_) = mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP in
+  let resonerNames = List.map (fun (_,s) -> s) solvs in
+  let formulas = List.map (fun n -> ("size "^(string_of_int n),genF n)) (2--40) in
+  let fillCell formula solver =
+    let (res, time, _) = solver ([],formula) timeout in
+    (ASAT, -10)
+    (*match res with
+    |
+    |
+    *)
+  in
+  let results = List.map (fun f ->
+                    List.map (fun s ->
+                        fillCell f s) solvs) formulas
+  in
+  (reasonerNames,results)
 
-let expQ (tbox, sf) = C.exportQuery tbox sf
+let _ =
+    if Array.length Sys.argv < 1 then printUsage ()
+    else match Sys.argv.(1) with
+    | "K" -> doTestK ()
+    | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Logic name »" ^ str ^ "«"))
 
 
 (*
+let expQ (tbox, sf) = C.exportQuery tbox sf
+
 let rateF = int_of_string Sys.argv.(1)
 let rateP = int_of_string Sys.argv.(2)
 let nr = int_of_string Sys.argv.(3)