diff --git a/src/tseitin/CDCL_tseitin.ml b/src/tseitin/CDCL_tseitin.ml
deleted file mode 100644
index 3dff62e8..00000000
--- a/src/tseitin/CDCL_tseitin.ml
+++ /dev/null
@@ -1,243 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                          Alt-Ergo Zero                                 *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                      Universite Paris-Sud 11                           *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-module type Arg = Tseitin_intf.Arg
-
-module type S = Tseitin_intf.S
-
-module Make (A : Tseitin_intf.Arg) = struct
-  module F = A.Form
-
-  exception Empty_Or
-  type combinator = And | Or | Imp | Not
-
-  type atom = A.Form.t
-  type t =
-    | True
-    | Lit of atom
-    | Comb of combinator * t list
-
-  let rec print fmt phi =
-    match phi with
-    | True -> Format.fprintf fmt "true"
-    | Lit a -> F.print fmt a
-    | Comb (Not, [f]) ->
-      Format.fprintf fmt "not (%a)" print f
-    | Comb (And, l) -> Format.fprintf fmt "(%a)" (print_list "and") l
-    | Comb (Or, l) ->  Format.fprintf fmt "(%a)" (print_list "or") l
-    | Comb (Imp, [f1; f2]) ->
-      Format.fprintf fmt "(%a => %a)" print f1 print f2
-    | _ -> assert false
-  and print_list sep fmt = function
-    | [] -> ()
-    | [f] -> print fmt f
-    | f::l -> Format.fprintf fmt "%a %s %a" print f sep (print_list sep) l
-
-  let make comb l = Comb (comb, l)
-
-  let make_atom p = Lit p
-
-  let f_true = True
-  let f_false = Comb(Not, [True])
-
-  let rec flatten comb acc = function
-    | [] -> acc
-    | (Comb (c, l)) :: r when c = comb ->
-      flatten comb (List.rev_append l acc) r
-    | a :: r ->
-      flatten comb (a :: acc) r
-
-  let rec opt_rev_map f acc = function
-    | [] -> acc
-    | a :: r -> begin match f a with
-        | None -> opt_rev_map f acc r
-        | Some b -> opt_rev_map f (b :: acc) r
-      end
-
-  let remove_true l =
-    let aux = function
-      | True -> None
-      | f -> Some f
-    in
-    opt_rev_map aux [] l
-
-  let remove_false l =
-    let aux = function
-      | Comb(Not, [True]) -> None
-      | f -> Some f
-    in
-    opt_rev_map aux [] l
-
-
-  let make_not f = make Not [f]
-
-  let make_and l =
-    let l' = remove_true (flatten And [] l) in
-    if List.exists ((=) f_false) l' then
-      f_false
-    else
-      make And l'
-
-  let make_or l =
-    let l' = remove_false (flatten Or [] l) in
-    if List.exists ((=) f_true) l' then
-      f_true
-    else match l' with
-      | [] -> raise Empty_Or
-      | [a] -> a
-      | _ -> Comb (Or, l')
-
-  let make_imply f1 f2 = make Imp [f1; f2]
-  let make_equiv f1 f2 = make_and [ make_imply f1 f2; make_imply f2 f1]
-  let make_xor f1 f2 = make_or [ make_and [ make_not f1; f2 ];
-                                 make_and [ f1; make_not f2 ] ]
-
-  (* simplify formula *)
-  let (%%) f g x = f (g x)
-
-  let rec sform f k = match f with
-    | True | Comb (Not, [True]) -> k f
-    | Comb (Not, [Lit a]) -> k (Lit (F.neg a))
-    | Comb (Not, [Comb (Not, [f])]) -> sform f k
-    | Comb (Not, [Comb (Or, l)]) -> sform_list_not [] l (k %% make_and)
-    | Comb (Not, [Comb (And, l)]) -> sform_list_not [] l (k %% make_or)
-    | Comb (And, l) -> sform_list [] l (k %% make_and)
-    | Comb (Or, l) -> sform_list [] l (k %% make_or)
-    | Comb (Imp, [f1; f2]) ->
-      sform (make_not f1) (fun f1' -> sform f2 (fun f2' -> k (make_or [f1'; f2'])))
-    | Comb (Not, [Comb (Imp, [f1; f2])]) ->
-      sform f1 (fun f1' -> sform (make_not f2) (fun f2' -> k (make_and [f1';f2'])))
-    | Comb ((Imp | Not), _) -> assert false
-    | Lit _ -> k f
-  and sform_list acc l k = match l with
-    | [] -> k acc
-    | f :: tail ->
-      sform f (fun f' -> sform_list (f'::acc) tail k)
-  and sform_list_not acc l k = match l with
-    | [] -> k acc
-    | f :: tail ->
-      sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k)
-
-  let ( @@ ) l1 l2 = List.rev_append l1 l2
-  (* let ( @ ) = `Use_rev_append_instead   (* prevent use of non-tailrec append *) *)
-
-  type fresh_state = A.t
-
-  type state = {
-    fresh: fresh_state;
-    mutable acc_or : (atom * atom list) list;
-    mutable acc_and : (atom * atom list) list;
-
-  }
-
-  let create fresh : state = {
-    fresh;
-    acc_or=[];
-    acc_and=[];
-  }
-
-  let mk_proxy st : F.t = A.fresh st.fresh
-
-  (* build a clause by flattening (if sub-formulas have the
-     same combinator) and proxy-ing sub-formulas that have the
-     opposite operator. *)
-  let rec cnf st f = match f with
-    | Lit a -> None, [a]
-    | Comb (Not, [Lit a]) -> None, [F.neg a]
-
-    | Comb (And, l) ->
-      List.fold_left
-        (fun (_, acc) f ->
-           match cnf st f with
-           | _, [] -> assert false
-           | _cmb, [a] -> Some And, a :: acc
-           | Some And, l ->
-             Some And, l @@ acc
-           (* let proxy = mk_proxy () in *)
-           (* acc_and := (proxy, l) :: !acc_and; *)
-           (* proxy :: acc *)
-           | Some Or, l ->
-             let proxy = mk_proxy st in
-             st.acc_or <- (proxy, l) :: st.acc_or;
-             Some And, proxy :: acc
-           | None, l -> Some And, l @@ acc
-           | _ -> assert false
-        ) (None, []) l
-
-    | Comb (Or, l) ->
-      List.fold_left
-        (fun (_, acc) f ->
-           match cnf st f with
-           | _, [] -> assert false
-           | _cmb, [a] -> Some Or, a :: acc
-           | Some Or, l ->
-             Some Or, l @@ acc
-           (* let proxy = mk_proxy () in *)
-           (* acc_or := (proxy, l) :: !acc_or; *)
-           (* proxy :: acc *)
-           | Some And, l ->
-             let proxy = mk_proxy st  in
-             st.acc_and <- (proxy, l) :: st.acc_and;
-             Some Or, proxy :: acc
-           | None, l -> Some Or, l @@ acc
-           | _ -> assert false)
-        (None, []) l
-    | _ -> assert false
-
-  let cnf st f =
-    let acc = match f with
-      | True -> []
-      | Comb(Not, [True]) -> [[]]
-      | Comb (And, l) -> List.rev_map (fun f -> snd(cnf st f)) l
-      | _ -> [snd (cnf st f)]
-    in
-    let proxies = ref [] in
-    (* encore clauses that make proxies in !acc_and equivalent to
-       their clause *)
-    let acc =
-      List.fold_left
-        (fun acc (p,l) ->
-           proxies := p :: !proxies;
-           let np = F.neg p in
-           (* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]]
-              also add clauses [p => l1], [p => l2], etc. *)
-           let cl, acc =
-             List.fold_left
-               (fun (cl,acc) a -> (F.neg a :: cl), [np; a] :: acc)
-               ([p],acc) l in
-           cl :: acc)
-        acc st.acc_and
-    in
-    (* encore clauses that make proxies in !acc_or equivalent to
-       their clause *)
-    let acc =
-      List.fold_left
-        (fun acc (p,l) ->
-           proxies := p :: !proxies;
-           (* add clause [p => l1 | l2 | ... | ln], and add clauses
-              [l1 => p], [l2 => p], etc. *)
-           let acc = List.fold_left (fun acc a -> [p; F.neg a]::acc)
-               acc l in
-           (F.neg p :: l) :: acc)
-        acc st.acc_or
-    in
-    acc
-
-  let make_cnf st f : _ list list =
-    st.acc_or <- [];
-    st.acc_and <- [];
-    cnf st (sform f (fun f' -> f'))
-
-  (* Naive CNF XXX remove???
-     let make_cnf f = mk_cnf (sform f)
-  *)
-end
diff --git a/src/tseitin/CDCL_tseitin.mli b/src/tseitin/CDCL_tseitin.mli
deleted file mode 100644
index 85220b17..00000000
--- a/src/tseitin/CDCL_tseitin.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** Tseitin CNF conversion
-
-    This modules implements Tseitin's Conjunctive Normal Form conversion, i.e.
-    the ability to transform an arbitrary boolean formula into an equi-satisfiable
-    CNF, that can then be fed to a SAT/SMT/McSat solver.
-*)
-
-module type Arg = Tseitin_intf.Arg
-(** The implementation of formulas required to implement Tseitin's CNF conversion. *)
-
-module type S = Tseitin_intf.S
-(** The exposed interface of Tseitin's CNF conversion. *)
-
-module Make(A : Arg) : S with type atom = A.Form.t and type fresh_state = A.t
-(** This functor provides an implementation of Tseitin's CNF conversion. *)
-
diff --git a/src/tseitin/Tseitin_intf.ml b/src/tseitin/Tseitin_intf.ml
deleted file mode 100644
index de596d91..00000000
--- a/src/tseitin/Tseitin_intf.ml
+++ /dev/null
@@ -1,99 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                          Alt-Ergo Zero                                 *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                      Universite Paris-Sud 11                           *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** Interfaces for Tseitin's CNF conversion *)
-
-module type Arg = sig
-  (** Formulas
-
-      This defines what is needed of formulas in order to implement
-      Tseitin's CNF conversion.
-  *)
-
-  module Form : sig
-    type t
-    (** Type of atomic formulas. *)
-
-    val neg : t -> t
-    (** Negation of atomic formulas. *)
-
-    val print : Format.formatter -> t -> unit
-    (** Print the given formula. *)
-  end
-
-  type t
-  (** State *)
-
-  val fresh : t -> Form.t
-  (** Generate fresh formulas (that are different from any other). *)
-
-end
-
-module type S = sig
-  (** CNF conversion
-
-      This modules allows to convert arbitrary boolean formulas
-      into CNF.
-  *)
-
-  type atom
-  (** The type of atomic formulas. *)
-
-  type t
-  (** The type of arbitrary boolean formulas. Arbitrary boolean formulas
-      can be built using functions in this module, and then converted
-      to a CNF, which is a list of clauses that only use atomic formulas. *)
-
-  val f_true : t
-  (** The [true] formula, i.e a formula that is always satisfied. *)
-
-  val f_false : t
-  (** The [false] formula, i.e a formula that cannot be satisfied. *)
-
-  val make_atom : atom -> t
-  (** [make_atom p] builds the boolean formula equivalent to the atomic formula [p]. *)
-
-  val make_not : t -> t
-  (** Creates the negation of a boolean formula. *)
-
-  val make_and : t list -> t
-  (** Creates the conjunction of a list of formulas. An empty conjunction is always satisfied. *)
-
-  val make_or : t list -> t
-  (** Creates the disjunction of a list of formulas. An empty disjunction is never satisfied. *)
-
-  val make_xor : t -> t -> t
-  (** [make_xor p q] creates the boolean formula "[p] xor [q]". *)
-
-  val make_imply : t -> t -> t
-  (** [make_imply p q] creates the boolean formula "[p] implies [q]". *)
-
-  val make_equiv : t -> t -> t
-  (** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *)
-
-  type fresh_state
-  (** State used to produce fresh atoms *)
-
-  type state
-  (** State used for the Tseitin transformation *)
-
-  val create : fresh_state -> state
-
-  val make_cnf : state -> t -> atom list list
-  (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a
-      list (which is a conjunction) of lists (which are disjunctions) of
-      atomic formulas. *)
-
-  val print : Format.formatter -> t -> unit
-  (** [print fmt f] prints the formula on the formatter [fmt].*)
-
-end
diff --git a/src/tseitin/jbuild b/src/tseitin/jbuild
deleted file mode 100644
index 29c01d08..00000000
--- a/src/tseitin/jbuild
+++ /dev/null
@@ -1,12 +0,0 @@
-; vim:ft=lisp:
-
-(library
-  ((name CDCL_tseitin)
-   (public_name sidekick.tseitin)
-   (synopsis "Tseitin transformation for CDCL")
-   (libraries ())
-   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))
-   (ocamlopt_flags (:standard -O3 -bin-annot
-                    -unbox-closures -unbox-closures-factor 20))
-  ))
-