diff --git a/CoolUtils.ml b/CoolUtils.ml
index 13d5ed52cb1b1b5984ded3290b3f556f7645a026..ffb4bfbc9c2bb7ead1680fc05ddf1d739d6aec2c 100644
--- a/CoolUtils.ml
+++ b/CoolUtils.ml
@@ -20,6 +20,14 @@ module TArray = struct
         Array.of_list (Array.fold_right combine arr [])
 end
 
+module TList = struct
+    let rec zip l1 l2 = match l1 with
+                        | h1::t1 -> (match l2 with
+                                     | h2::t2 -> (h1,h2)::(zip t1 t2)
+                                     | [] -> [])
+                        | [] -> []
+end
+
 let agents = ref ([|1;2;3;4;5;6;7;8;9;10|])
 
 let cl_get_agents () = !agents
diff --git a/CoolUtils.mli b/CoolUtils.mli
index f0f060575cbc98f01f25f2c03271e40a2b800f49..daa96bbe6dbab8dde3ee1940c4a054ad2023377a 100644
--- a/CoolUtils.mli
+++ b/CoolUtils.mli
@@ -10,6 +10,10 @@ module TArray : sig
     val uniq : 'a array -> 'a array (* delete consecutive duplicates *)
 end
 
+module TList : sig
+    val zip : ('a list) -> ('b list) -> ('a * 'b) list
+end
+
 val cl_get_agents : unit -> int array
 val cl_set_agents : int array -> unit
 
diff --git a/coalgcompare.ml b/coalgcompare.ml
index d9329e470af0872e213a7b19690ccbfe78ba5e99..87985af44b60d2701c7a392a64a4db28776f81df 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -9,20 +9,34 @@ module G = GenAndComp
 module C = CoAlgFormula
 module A = ALCFormula
 
-type solvanswer = ASAT | AUNSAT | ATIMEOUT
+open CoolUtils
+
+type solvanswer = ASAT | AUNSAT | ATIMEOUT | AFAILED
+
+let string_of_solvanswer a =
+    match a with
+    | ASAT -> "sat"
+    | AUNSAT -> "unsat"
+    | ATIMEOUT -> "timeout"
+    | AFAILED -> "failed"
 
 type testresults =
    ((string list) (* solver names *)
     * ((string * ((solvanswer * int) list)) (*some test case with times for each reasoner*)
         list))
 
+let debugMsg str =
+    print_endline (":: " ^ str)
+
 (* 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 }
+*)
 
 
 let seed =
@@ -33,7 +47,7 @@ let seed =
 
 let _ = 
   Random.init seed;
-  print_endline (string_of_int (seed))
+  debugMsg ("seed is " ^ (string_of_int (seed)))
 
 
 let sortK = Array.make 1 (CoAlgMisc.MultiModalK, [0])
@@ -112,10 +126,15 @@ let solvALC (tbox, sf) =
   let args = exportALCQuery tbox sf in
   G.evaluateFkt (fun (fl, tboxND, tboxD) -> ALCGraph.isSat fl tboxND tboxD) args
 
-let solvFact (tbox, sf) =
+let solvFact (tbox, sf) timeout =
   let (fl, tboxND, tboxD) = exportALCQuery tbox sf in
   A.createFactTBox "fact.tbox" fl tboxND tboxD;
-  G.callExt None "FaCT++" ["fact.conf"] (Str.regexp_string "is sat")
+  let fact = "/usr/bin/FaCT++" in
+  let reg = "is satisfiable" in
+  let call () = G.callExt None fact ["fact.conf"] (Str.regexp_string reg) timeout in
+  let ignore_exception = false in
+  if ignore_exception then try call () with _ -> (G.FAILED, -1.0, 0)
+                      else call ()
 
 let solvers =
   let _ = [(solvCoalg sortK, "CoAlg"); (solvALC, "alc"); (solvFact, "fact")] in
@@ -127,7 +146,7 @@ let printUsage () =
   exit 1
 
 let doTestK () : testresults =
-  let solvs = [(solvFact, "fact"); (solvCoalg sortK, "CoAlg")] in
+  let solvs = [(solvFact, "fact"); (solvCoalg sortK, "cool")] in
   (*
     lF A list of pairs (f, n), e.g. (p, 1).
     The list must not be empty.
@@ -153,21 +172,39 @@ let doTestK () : testresults =
   let lPPP = [] in
   let (genF,_) = G.mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP in
   let reasonerNames = List.map (fun (_,s) -> s) solvs in
-  let formulas : (string*C.sortedFormula) list = List.map (fun n -> ("size "^(string_of_int n),(0,genF n))) (2--40) in
-  let fillCell formula (solver,_) =
+  let form_maxsize = 900000 in
+  let form_count = 20 in
+  let form_sizes = ((form_maxsize-form_count)--form_maxsize) in
+  let formulas : (string*C.sortedFormula) list = List.map (fun n -> ("randsize"^(string_of_int n),(0,genF n))) form_sizes in
+  let fillCell (fn,formula) (solver,sn) =
+    debugMsg ("K: running " ^ sn ^ " on " ^ fn);
     let (res, time, _) = solver ([],formula) timeout in
-    (ASAT, -10)
+    let answer = match res with
+                 | G.FINISHED (v) -> if (v) then ASAT else AUNSAT
+                 | G.TIMED_OUT -> ATIMEOUT
+                 | G.FAILED -> AFAILED
+    in
+    (answer, int_of_float time)
   in
   let results = List.map (fun (str,f) ->
                     (str,List.map (fun s ->
-                        fillCell f s) solvs)) formulas
+                        fillCell (str,f) s) solvs)) formulas
   in
   (reasonerNames,results)
 
+let printRawData ((rn,results):testresults) : unit =
+    let doubler l = List.fold_right (fun a b -> (a ^ "_state")::(a^"_time")::b) l [] in
+    print_endline (String.concat ";" ("formula"::doubler rn)) ;
+    let format_cell (stat,time) = (string_of_solvanswer stat) ^ ";" ^ (string_of_int time) in
+    let format_line (fn,res) = fn ^ ";" ^ (String.concat ";" (List.map format_cell res)) in
+    let lines = List.map format_line results in
+    print_endline (String.concat "\n" lines)
+
+
 let _ =
-    if Array.length Sys.argv < 1 then printUsage ()
+    if Array.length Sys.argv < 2 then printUsage ()
     else match Sys.argv.(1) with
-    | "K" -> doTestK ()
+    | "K" -> printRawData (doTestK ())
     | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Logic name »" ^ (Sys.argv.(1)) ^ "«"))