diff --git a/gen2.ml b/gen2.ml
deleted file mode 100644
index 958eda6b4e7f2f0de408063910cbf43b0adac426..0000000000000000000000000000000000000000
--- a/gen2.ml
+++ /dev/null
@@ -1,160 +0,0 @@
-open CoAlgFormula
-
-(* Generates the negation of the formulas in
- http://files.oliverfriedmann.de/papers/a_solver_for_modal_fixpoint_logics.pdf, page 7 *)
-
-exception CTLException of string
-
-let iota n =
-  let rec intern i n =
-    if i = n then [i]
-    else i::intern (i+1) n
-  in
-  intern 1 n
-
-let name n i = n ^ string_of_int i
-
-let psi n =
-  let inside i =
-    let not_qis =
-      List.map (fun j -> (NOT (AP (name "q" j))))
-               (List.filter (fun x -> x <> i) (iota n))
-    in
-    List.fold_right const_and not_qis (AP (name "q" i))
-  in
-
-  (NU("X",const_and (const_ax "" (VAR "X"))
-            (List.fold_right const_or (List.map inside (iota n)) FALSE))) 
-
-let neg_phi n =
-  const_and (psi n)
-            (const_or (const_and (before_biimpl n) (after_biimpl_neg n))
-                      (const_and (before_biimpl_neg n) (after_biimpl n)))
-
-
-(** Converts a formula into a string representation for MLSolver.
-        @param f A formula.
-        @return A string representing f for MLSolver.
-        @raise CTLException If the name of an atomic program
-        or a propositional variable in f is "tt" or "ff".
- *)
-let exportMLSolver f =
-  let sb = Buffer.create 3000 in
-  let rec expML = function
-    | TRUE -> Buffer.add_string sb "(tt)"
-    | FALSE -> Buffer.add_string sb "(ff)"
-    | AP s ->
-       if s <> "tt" && s <> "ff" then begin
-           Buffer.add_string sb s;
-         end
-       else raise (CTLException "Formula contains ff or tt.")
-    | VAR s ->
-       Buffer.add_string sb " ";
-       Buffer.add_string sb s;
-       Buffer.add_string sb " "
-    | NOT f1 ->
-       Buffer.add_string sb "(!";
-       expML f1;
-       Buffer.add_string sb ")"
-    (* | EX (_, f1) -> *)
-    (*    Buffer.add_string sb "(E X"; *)
-    (*    expML f1; *)
-    (*    Buffer.add_string sb ")" *)
-    (* | AX (_, f1) -> *)
-    (*    Buffer.add_string sb "(A X"; *)
-    (*    expML f1; *)
-    (*    Buffer.add_string sb ")" *)
-    | EF f1 ->
-       Buffer.add_string sb "(E F";
-       expML f1;
-       Buffer.add_string sb ")"
-    | AF f1 ->
-       Buffer.add_string sb "(A F";
-       expML f1;
-       Buffer.add_string sb ")"
-    | EG f1 ->
-       Buffer.add_string sb "(E G";
-       expML f1;
-       Buffer.add_string sb ")"
-    | AG f1 ->
-       Buffer.add_string sb "(A G";
-       expML f1;
-       Buffer.add_string sb ")"
-    | EQU (f1, f2) ->
-       Buffer.add_string sb  "(";
-       expML f1;
-       Buffer.add_string sb " <==> ";
-       expML f2;
-       Buffer.add_string sb ")"
-    | IMP (f1, f2) ->
-       Buffer.add_string sb "(";
-       expML f1;
-       Buffer.add_string sb " ==> ";
-       expML f2;
-       Buffer.add_string sb ")"
-    | OR (f1, f2) ->
-       Buffer.add_string sb "(";
-       expML f1;
-       Buffer.add_string sb " | ";
-       expML f2;
-       Buffer.add_string sb ")"
-    | AND (f1, f2) ->
-       Buffer.add_string sb "(";
-       expML f1;
-       Buffer.add_string sb " & ";
-       expML f2;
-       Buffer.add_string sb ")"
-    | EU (f1, f2) ->
-       Buffer.add_string sb "(E (";
-       expML f1;
-       Buffer.add_string sb " U ";
-       expML f2;
-       Buffer.add_string sb "))"
-    | AU (f1, f2) ->
-       Buffer.add_string sb "(A (";
-       expML f1;
-       Buffer.add_string sb " U ";
-       expML f2;
-       Buffer.add_string sb "))"
-    | EB (f1, f2) ->
-       Buffer.add_string sb "(E (";
-       expML f1;
-       Buffer.add_string sb " R ";
-       expML (NOT f2);
-       Buffer.add_string sb "))"
-    | AB (f1, f2) ->
-       Buffer.add_string sb "(A (";
-       expML f1;
-       Buffer.add_string sb " R ";
-       expML (NOT f2);
-       Buffer.add_string sb "))"
-    | NU (var, f1) ->
-       Buffer.add_string sb ("(nu " ^ var ^ ". ");
-       expML f1;
-       Buffer.add_string sb ")"
-    | MU (var, f1) ->
-       Buffer.add_string sb ("(mu " ^ var ^ ". ");
-       expML f1;
-       Buffer.add_string sb ")"
-    | AX (_, f1) ->
-       Buffer.add_string sb "([](";
-       expML f1;
-       Buffer.add_string sb "))"
-       
-  in
-  expML f;
-  Buffer.contents sb
-
-let print_usage () =
-  print_endline ("Usage: " ^ Sys.argv.(0) ^ " (cool|mlsolver) n");
-  print_endline ("   where n is the number of the formula to generate")
-
-let () =
-  if Array.length Sys.argv < 3 then
-    print_usage ()
-  else
-    let n = int_of_string Sys.argv.(2) in
-    match Sys.argv.(1) with
-    | "cool" -> print_endline (exportFormula (neg_phi n))
-    | "mlsolver" -> print_endline (exportMLSolver (neg_phi n))
-    | _ -> print_usage ()