diff --git a/CoAlgFormula.ml b/CoAlgFormula.ml
index d735dee0ec2435875bc3619f1c2b6b83f39aaf12..77c4965b5c7aadce2de4b52d0b522a1237507449 100644
--- a/CoAlgFormula.ml
+++ b/CoAlgFormula.ml
@@ -227,6 +227,82 @@ let exportFormula f =
   exportFormula_buffer sb f;
   Buffer.contents sb
 
+(** export (CL)-formula suitable for tatl-inputs *)
+let rec exportTatlFormula_buffer sb f =
+  let negate = function
+    | NOT f -> f
+    | f -> NOT f
+  in
+  let prio n lf =
+    let prionr = function
+      | EQU _ -> 0
+      | IMP _  -> 1 
+      | OR _ -> 2
+      | AND _ -> 3
+      | _ -> 4
+    in
+    if prionr lf < n then begin
+      Buffer.add_char sb '(';
+      exportFormula_buffer sb lf;
+      Buffer.add_char sb ')'
+    end
+    else exportFormula_buffer sb lf
+  in
+  match f with
+  | TRUE -> Buffer.add_string sb "(p \\/ ~p)"
+  | FALSE -> Buffer.add_string sb "(p /\\ ~p)"
+  | AP s -> Buffer.add_string sb s
+  | NOT f1 ->
+      Buffer.add_string sb "~";
+      prio 4 f1
+  | OR (f1, f2) ->
+      prio 2 f1;
+      Buffer.add_string sb " \\/ ";
+      prio 2 f2
+  | AND (f1, f2) ->
+      prio 3 f1;
+      Buffer.add_string sb " /\\ ";
+      prio 3 f2
+  | EQU (f1, f2) ->
+      prio 0 (AND (IMP (f1,f2), IMP (f2,f1)))
+  | IMP (f1, f2) ->
+      prio 2 f1;
+      Buffer.add_string sb " -> ";
+      prio 2 f2
+  | ALLOWS (s, f1) ->
+      Buffer.add_string sb "<<";
+      Buffer.add_string sb (
+          match s with
+          | [] -> " "
+          | _ ->(Str.concat "," (L.map string_of_int s))
+      );
+      Buffer.add_string sb ">>X ";
+      prio 4 f1
+  | ENFORCES (s, f1) ->
+      Buffer.add_string sb "~<<";
+      Buffer.add_string sb (
+          match s with
+          | [] -> " "
+          | _ ->(Str.concat "," (L.map string_of_int s))
+      );
+      Buffer.add_string sb ">>X ~ ";
+      prio 4 f1
+  | EX _
+  | AX _
+  | MIN _
+  | MAX _
+  | MORETHAN _
+  | MAXEXCEPT _
+  | AT _
+  | CHC _
+  | CHCN _
+  | FUS _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
+
+let exportTatlFormula f =
+  let sb = Buffer.create 128 in
+  exportTatlFormula_buffer sb f;
+  Buffer.contents sb
+
 (** Appends a string representation of a sorted formula to a string buffer.
     Parentheses are ommited where possible
     where the preference rules are defined as usual.
diff --git a/CoAlgFormula.mli b/CoAlgFormula.mli
index 27b369c79d04bfc0dd37a1667f06ac26b8f22c68..0369b4ddf948b7c7046546bcf9e8f900d4de3960 100644
--- a/CoAlgFormula.mli
+++ b/CoAlgFormula.mli
@@ -38,6 +38,7 @@ val sizeFormula : formula -> int
 val sizeSortedFormula : sortedFormula -> int
 
 val exportFormula : formula -> string
+val exportTatlFormula : formula -> string
 val exportSortedFormula : sortedFormula -> string
 val exportQuery : sortedFormula list -> sortedFormula -> string
 val exportQueryParsable : sortedFormula list -> sortedFormula -> string
diff --git a/coalgcompare.ml b/coalgcompare.ml
index b182e9205f5194c6b48f88aac0f4963489ce0675..82f1c815e517d81a56a08815a9e451ece7e61d9f 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -140,10 +140,10 @@ let solvFact (tbox, sf) timeout =
   if ignore_exception then try call () with _ -> (G.FAILED, -1.0, 0)
                       else call ()
 
-let solvTatl (tbox,(_,sf)) timeout = (* ignore the TBox... *)
-  let tatl = "./tatl-compatibility-wrapper.sh" in
-  let inp = CoAlgFormula.exportFormula sf in
-  G.callExt (Some inp) tatl [] (Str.regexp_string "The formula is satisfiable") 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
+  G.callExt (Some ("1\n"^inp^"\n4\n")) tatl [] (Str.regexp_string "The formula is satisfiable") timeout
 
 let solvCool functorname (tbox,sf) timeout =
   let inp = CoAlgFormula.exportQueryParsable tbox sf in
@@ -274,7 +274,8 @@ let doTestGenericK () : testresults =
 
 
 let doTestGenericCL () : testresults =
-  let solvs = [(solvCoolCL, "cool"); (solvTatl, "tatl")] in
+  let agents = [1;2;3;4;5] in
+  let solvs = [(solvCoolCL, "cool"); (solvTatl agents, "tatl")] in
   let timeout = !ptimeout in (* 5 minutes *)
   let formulas = ref [] in
   let counter = ref 0 in
@@ -303,8 +304,8 @@ let printRawData ((rn,results):testresults) : unit =
     let lines = List.map format_line results in
     print_endline (String.concat "\n" lines)
 
-let doTestCL formulas : testresults =
-  let solvs = [(solvCoolCL, "cool"); (solvTatl, "tatl")] in
+let doTestCL agents formulas : testresults =
+  let solvs = [(solvCoolCL, "cool"); (solvTatl agents, "tatl")] in
   runTests solvs formulas !ptimeout
 
 let doGenCL aglist sizelist : CoAlgFormula.formula list =
@@ -374,8 +375,9 @@ let _ =
     | "genericCL" ->
             printRawData (doTestGenericCL ())
     | "CL1" -> let sz = (5000 -- 5080) in
+               let agents = [1;2;3;4;5] in
                let ats (str,f) = (str, ([], (0, f))) in (* add tbox and sort *)
-               printRawData (doTestCL (List.map ats (TList.zip (List.map string_of_int sz) (doGenCL [1;2;3;4;5] sz))))
+               printRawData (doTestCL agents (List.map ats (TList.zip (List.map string_of_int sz) (doGenCL agents sz))))
     | "genCL" -> let p1 = getarg () in
                  let p2 = getarg () in
                  let forms = doGenCL (intlist_of_string p1) (intlist_of_string p2) in