diff --git a/CoolUtils.ml b/CoolUtils.ml
index 5fc26310f5e875a97fbb7723b86f179a5073db41..937064c7a3bff02113193643d35af54771503ea3 100644
--- a/CoolUtils.ml
+++ b/CoolUtils.ml
@@ -32,6 +32,9 @@ module TList = struct
                   let oth = List.map (fun x -> h::x) pt in
                   List.append pt oth
     let prod la lb = List.concat (List.map (fun a -> List.map (fun b -> (a,b)) lb) la)
+    let empty l = match l with
+                  | (_::_) -> false
+                  | [] -> true
 end
 
 let agents = ref ([|1;2;3;4;5|])
diff --git a/CoolUtils.mli b/CoolUtils.mli
index 24016a479673caf6a0919ac4eadc1f29f2cb62a8..9e2a54449a7832807f0916ff9414bb8922feef66 100644
--- a/CoolUtils.mli
+++ b/CoolUtils.mli
@@ -14,6 +14,7 @@ module TList : sig
     val zip : ('a list) -> ('b list) -> ('a * 'b) list
     val powerset : ('a list) -> ('a list list)
     val prod : ('a list) -> ('b list) -> (('a * 'b) list)
+    val empty : ('a list) -> bool
 end
 
 val cl_get_agents : unit -> int array
diff --git a/coalgcompare.ml b/coalgcompare.ml
index 44e7fdabf7bdd0a14b7ba00b090c4fe57ae6ce2c..de947d243e807271bc62272a4c5eb1e60a6d179f 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -142,7 +142,11 @@ let solvFact (tbox, sf) timeout =
 
 let solvTatl agents (tbox,(_,sf)) timeout = (* ignore the TBox... *)
   let tatl = "./tatl" in
-  let inp = CoAlgFormula.exportTatlFormula (C.AND (sf, C.ALLOWS (agents,C.TRUE))) in
+  let tboxlist = List.map (fun (_,f) -> CoAlgFormula.exportTatlFormula f) tbox in
+  let agstr = String.concat "," (List.map string_of_int agents) in
+  let tboxstr = "~<<"^agstr^">>F~ ("^(String.concat " /\\ " tboxlist) ^ ") /\\ " in
+  let inp = CoAlgFormula.exportTatlFormula sf in
+  let inp = if TList.empty tbox then inp else (tboxstr ^ "(" ^ inp ^ ")") in
   G.callExt (Some ("1\n"^inp^"\n4")) tatl [] (Str.regexp_string "The formula is satisfiable") timeout
 
 let solvCool functorname (tbox,sf) timeout =