diff --git a/smt/mcsat.ml b/smt/mcsat.ml
index 6514ea08..ed2e53fc 100644
--- a/smt/mcsat.ml
+++ b/smt/mcsat.ml
@@ -139,7 +139,10 @@ module Make(Dummy:sig end) = struct
     (* SmtSolver.Proof.learn (SmtSolver.history ()); *)
     match SmtSolver.unsat_conflict () with
     | None -> assert false
-    | Some c -> SmtSolver.Proof.prove_unsat c
+    | Some c ->
+      let p = SmtSolver.Proof.prove_unsat c in
+      SmtSolver.Proof.check p;
+      p
 
   let eval = SmtSolver.eval
 
diff --git a/smt/smt.ml b/smt/smt.ml
index fc630713..ce92f16c 100644
--- a/smt/smt.ml
+++ b/smt/smt.ml
@@ -89,7 +89,10 @@ module Make(Dummy:sig end) = struct
   let get_proof () =
     match SmtSolver.unsat_conflict () with
     | None -> assert false
-    | Some c -> SmtSolver.Proof.prove_unsat c
+    | Some c ->
+      let p = SmtSolver.Proof.prove_unsat c in
+      SmtSolver.Proof.check p;
+      p
 
   let eval = SmtSolver.eval
 
diff --git a/solver/internal.ml b/solver/internal.ml
index b68b44a7..98d2ecf7 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -27,7 +27,6 @@ module Make
     ul_th_env : Th.level; (* Theory state at level 0 *)
     ul_clauses : int; (* number of clauses *)
     ul_learnt : int; (* number of learnt clauses *)
-    ul_proof_lvl : int; (* push/pop index for Res module *)
   }
 
   (* Singleton type containing the current state *)
@@ -128,7 +127,6 @@ module Make
         ul_learnt = 0;
         ul_clauses = 0;
         ul_th_env = Th.dummy;
-        ul_proof_lvl = -1;
       };
 
     order = Iheap.init 0;
@@ -383,6 +381,8 @@ module Make
     ()
 
   let report_unsat ({atoms=atoms} as confl) =
+    L.debug 5 "Unsat conflict:";
+    L.debug 5 " %a" St.pp_clause confl;
     env.unsat_conflict <- Some confl;
     raise Unsat
 
@@ -393,7 +393,7 @@ module Make
         | [ a ] ->
           if history = [] then r
           else
-            let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (List.rev (cl :: history))) c_lvl in
+            let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) c_lvl in
             Bcp (Some tmp_cl)
         | _ -> assert false
       end
@@ -490,7 +490,7 @@ module Make
     with Exit ->
       let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in
       let blevel = backtrack_lvl !is_uip learnt in
-      blevel, learnt, !history, !is_uip, !c_level
+      blevel, learnt, List.rev !history, !is_uip, !c_level
 
   let get_atom i =
     destruct (Vec.get env.elt_queue i)
@@ -552,7 +552,7 @@ module Make
       | n, _ -> assert false
     done;
     List.iter (fun q -> q.var.seen <- false) !seen;
-    !blevel, !learnt, !history, true, !c_level
+    !blevel, !learnt, List.rev !history, true, !c_level
 
   let analyze c_clause =
     if St.mcsat then
@@ -605,9 +605,9 @@ module Make
       | History _ -> assert false
     in
     try
-      if not force && Proof.has_been_proved init0 then raise Trivial;
-      if not (Proof.is_proven init0) then assert false; (* Important side-effect, DO NOT REMOVE *)
-      let atoms, init, level = partition (Vec.to_list init0.atoms) init0.c_level in
+      (* if not force && Proof.has_been_proved init0 then raise Trivial; *)
+      (* if not (Proof.is_proven init0) then assert false; (* Important side-effect, DO NOT REMOVE *) *)
+      let atoms, history, level = partition (Vec.to_list init0.atoms) init0.c_level in
       let size = List.length atoms in
       match atoms with
       | [] ->
@@ -1003,8 +1003,7 @@ module Make
       in
       let ul_clauses = Vec.size env.clauses_hyps in
       let ul_learnt = Vec.size env.clauses_learnt in
-      let ul_proof_lvl = Proof.push () in
-      Vec.push env.user_levels {ul_elt_lvl; ul_th_lvl; ul_th_env; ul_clauses; ul_learnt; ul_proof_lvl;};
+      Vec.push env.user_levels {ul_elt_lvl; ul_th_lvl; ul_th_env; ul_clauses; ul_learnt;};
       res
     end
 
@@ -1081,9 +1080,6 @@ module Make
       done;
       Vec.shrink env.clauses_hyps (Vec.size env.clauses_hyps - ul.ul_clauses);
 
-      (* Backtrack the Proof module *)
-      Proof.pop ul.ul_proof_lvl;
-
       (* Refresh the known tautologies simplified because of clauses that have been removed *)
       let s = Stack.create () in
       let new_sz = ref ul.ul_learnt in
diff --git a/solver/res.ml b/solver/res.ml
index 85f56aad..89c9af0b 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -16,43 +16,9 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
   type atom = St.atom
   type int_cl = clause * St.atom list
 
-  type node =
-    | Assumption
-    | Lemma of lemma
-    | Resolution of atom * int_cl * int_cl
-    (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
-
   exception Insuficient_hyps
   exception Resolution_error of string
 
-  (* Proof graph *)
-  let hash_cl cl =
-    Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl)
-
-  let equal_cl cl_c cl_d =
-    try
-      List.for_all2 (==) cl_c cl_d
-    with Invalid_argument _ ->
-      false
-
-  module H = Hashtbl.Make(struct
-      type t = St.atom list
-      let hash = hash_cl
-      let equal = equal_cl
-    end)
-  let proof : node H.t ref = ref (H.create 1007);;
-
-  let push_stack = Vec.make 0 (H.create 0)
-
-  let push () =
-    let res = Vec.size push_stack in
-    Vec.push push_stack (H.copy !proof);
-    res
-
-  let pop i =
-    proof := Vec.get push_stack i;
-    Vec.shrink push_stack (Vec.size push_stack - i)
-
   (* Misc functions *)
   let equal_atoms a b = St.(a.aid) = St.(b.aid)
   let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
@@ -60,7 +26,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
   let merge = List.merge compare_atoms
 
   let _c = ref 0
-  let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c)
+  let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c)
 
   (* Printing functions *)
   let rec print_cl fmt = function
@@ -104,164 +70,11 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
       L.debug 3 "Input clause is a tautology";
     res
 
+  (* Printing *)
   let print_clause fmt c = print_cl fmt (to_list c)
 
-  (* Adding hyptoheses *)
-  let has_been_proved c = H.mem !proof (to_list c)
-
-  let is_proved (c, cl) =
-    if H.mem !proof cl then
-      true
-    else if not St.(c.learnt) then begin
-      H.add !proof cl Assumption;
-      true
-    end else match St.(c.cpremise) with
-      | St.Lemma p -> H.add !proof cl (Lemma p); true
-      | St.History _ -> false
-
-  let is_proven c = is_proved (c, to_list c)
-
-  let add_res (c, cl_c) (d, cl_d) =
-    L.debug 7 "  Resolving clauses :";
-    L.debug 7 "    %a" St.pp_clause c;
-    L.debug 7 "    %a" St.pp_clause d;
-    assert (is_proved (c, cl_c));
-    assert (is_proved (d, cl_d));
-    let l = merge cl_c cl_d in
-    let resolved, new_clause = resolve l in
-    match resolved with
-    | [] -> raise (Resolution_error "No literal to resolve over")
-    | [a] ->
-      H.add !proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
-      let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause)
-          true St.(History [c; d]) (max c.St.c_level d.St.c_level) in
-      L.debug 5 "New clause : %a" St.pp_clause new_c;
-      new_c, new_clause
-    | _ -> raise (Resolution_error "Resolved to a tautology")
-
-  let rec diff_learnt acc l l' =
-    match l, l' with
-    | [], _ -> l' @ acc
-    | a :: r, b :: r' ->
-      if equal_atoms a b then
-        diff_learnt acc r r'
-      else
-        diff_learnt (b :: acc) l r'
-    | _ -> raise (Resolution_error "Impossible to derive correct clause")
-
-  let clause_unit a = match St.(a.var.level, a.var.reason) with
-    | 0, St.Bcp Some c -> c, to_list c
-    | _ ->
-      raise (Resolution_error "Could not find a reason needed to resolve")
-
-  let need_clause (c, cl) =
-    if is_proved (c, cl) then
-      []
-    else
-      match St.(c.cpremise) with
-      | St.History l -> l
-      | St.Lemma _ -> assert false
-
-  let rec add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
-    match l with
-    | a :: r ->
-      L.debug 5 "Resolving (with history) %a" St.pp_clause c;
-      let temp_c, temp_cl = List.fold_left add_res a r in
-      let tmp = diff_learnt [] cl temp_cl in
-      List.iter (fun a ->
-          L.debug 0 " -> %a" St.pp_atom a) tmp;
-      assert (equal_cl cl temp_cl)
-      (*
-      while not (equal_cl cl !new_cl) do
-        let unit_to_use = diff_learnt [] cl !new_cl in
-        let unit_r = List.map (fun a -> clause_unit a) unit_to_use in
-        do_clause (List.map fst unit_r);
-        let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in
-        new_c := temp_c;
-        new_cl := temp_cl;
-      done
-         *)
-    | _ -> assert false
-
-  and do_clause = function
-    | [] -> ()
-    | c :: r ->
-      let cl = to_list c in
-      match need_clause (c, cl) with
-      | [] -> do_clause r
-      | history ->
-        let history_cl = List.rev_map (fun c -> c, to_list c) history in
-        let to_prove = List.filter (fun (c, cl) -> not (is_proved (c, cl))) history_cl in
-        let to_prove = (List.rev_map fst to_prove) in
-        begin match to_prove with
-          | [] ->
-            add_clause c cl history_cl;
-            do_clause r
-          | _ -> do_clause (to_prove @ (c :: r))
-        end
-
-  let prove c =
-    L.debug 3 "Proving : %a" St.pp_clause c;
-    do_clause [c];
-    L.debug 3 "Proved : %a" St.pp_clause c
-
-  let rec prove_unsat_cl (c, cl) = match cl with
-    | [] -> true
-    | a :: r ->
-      L.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
-      let d = match St.(a.var.level, a.var.reason) with
-        | 0, St.Bcp Some d -> d
-        | _ -> raise Exit
-      in
-      prove d;
-      let cl_d = to_list d in
-      prove_unsat_cl (add_res (c, cl) (d, cl_d))
-
-  let prove_unsat_cl c =
-    try
-      prove_unsat_cl c
-    with Exit ->
-      false
-
-  let learn v =
-    Vec.iter (fun c -> L.debug 15 "history : %a" St.pp_clause c) v;
-    Vec.iter prove v
-
-  let assert_can_prove_unsat c =
-    L.debug 1 "=================== Proof =====================";
-    prove c;
-    if not (prove_unsat_cl (c, to_list c)) then
-      raise Insuficient_hyps
-
-  (* Interface exposed *)
-  type proof = {
-    table : node H.t;
-    clause : clause * atom list;
-  }
-  and proof_node = {
-    conclusion : clause;
-    step : step;
-  }
-  and step =
-    | Hypothesis
-    | Lemma of lemma
-    | Resolution of proof * proof * atom
-
-  let expand { clause = (c, cl); table; } =
-    let st = match H.find table cl with
-      | Assumption -> Hypothesis
-      | Lemma l -> Lemma l
-      | Resolution (a, cl_c, cl_d) ->
-        Resolution ({ clause = cl_c; table}, {clause = cl_d; table}, a)
-    in
-    { conclusion = c; step = st }
-
-  let prove_unsat c =
-    assert_can_prove_unsat c;
-    {clause = St.empty_clause, []; table = !proof; }
-
-  (* Compute unsat-core *)
-  let compare_cl c d =
+  (* Comparison of clauses *)
+  let cmp_cl c d =
     let rec aux = function
       | [], [] -> 0
       | a :: r, a' :: r' -> begin match compare_atoms a a' with
@@ -271,8 +84,77 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
       | _ :: _ , [] -> -1
       | [], _ :: _ -> 1
     in
-    aux (to_list c, to_list d)
+    aux (c, d)
 
+  let cmp c d =
+    cmp_cl (to_list c) (to_list d)
+
+  let prove conclusion =
+    assert St.(conclusion.learnt || conclusion.cpremise <> History []);
+    conclusion
+
+  let prove_unsat c =
+    let l = Vec.to_list c.St.atoms in
+    let l = List.map (fun a ->
+        match St.(a.var.reason) with
+        | St.Bcp Some d -> d
+        | _ -> assert false) l
+    in
+    St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l))
+      (List.fold_left (fun i c -> max i c.St.c_level) 0 l)
+
+  (* Interface exposed *)
+  type proof = clause
+  and proof_node = {
+    conclusion : clause;
+    step : step;
+  }
+  and step =
+    | Hypothesis
+    | Lemma of lemma
+    | Resolution of proof * proof * atom
+
+  let rec chain_res (c, cl) = function
+    | d :: r ->
+      L.debug 10 " Resolving :";
+      L.debug 10 "   - %a" St.pp_clause c;
+      L.debug 10 "   - %a" St.pp_clause d;
+      let dl = to_list d in
+      begin match resolve (merge cl dl) with
+      | [ a ], l ->
+        begin match r with
+          | [] -> (l, c, d, a)
+          | _ ->
+            let new_clause = St.make_clause (fresh_pcl_name ()) l (List.length l) true
+                (St.History [c; d]) (max c.St.c_level d.St.c_level) in
+            chain_res (new_clause, l) r
+        end
+      | _ -> assert false
+      end
+    | _ -> assert false
+
+  let rec expand conclusion =
+    L.debug 5 "Expanding : %a" St.pp_clause conclusion;
+    match conclusion.St.cpremise with
+    | St.Lemma l ->
+      {conclusion; step = Lemma l; }
+    | St.History [] ->
+      assert (not conclusion.St.learnt);
+      { conclusion; step = Hypothesis; }
+    | St.History [ c ] ->
+      assert (cmp c conclusion = 0);
+      expand c
+    | St.History ( c :: ([d] as r)) ->
+      let (l, c', d', a) = chain_res (c, to_list c) r in
+      assert (cmp_cl l (to_list conclusion) = 0);
+      { conclusion; step = Resolution (c', d', a); }
+    | St.History ( c :: r ) ->
+      let (l, c', d', a) = chain_res (c, to_list c) r in
+      conclusion.St.cpremise <- St.History [c'; d'];
+      assert (cmp_cl l (to_list conclusion) = 0);
+      { conclusion; step = Resolution (c', d', a); }
+
+  (* Compute unsat-core *)
   let unsat_core proof =
     let rec aux acc proof =
       let p = expand proof in
@@ -281,9 +163,16 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
       | Resolution (proof1, proof2, _) ->
         aux (aux acc proof1) proof2
     in
-    sort_uniq compare_cl (aux [] proof)
+    sort_uniq cmp (aux [] proof)
 
   (* Iter on proofs *)
+  module H = Hashtbl.Make(struct
+      type t = clause
+      let hash cl =
+        Vec.fold (fun i a -> Hashtbl.hash St.(a.aid, i)) 0 cl.St.atoms
+      let equal = (==)
+    end)
+
   type task =
     | Enter of proof
     | Leaving of proof
@@ -293,13 +182,13 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
   let rec fold_aux s h f acc =
     match spop s with
     | None -> acc
-    | Some (Leaving ({clause = (_, cl)} as p)) ->
-      H.add h cl true;
-      fold_aux s h f (f acc (expand p))
-    | Some (Enter ({clause = (_, cl)} as p)) ->
-      if not (H.mem h cl) then begin
-        Stack.push (Leaving p) s;
-        let node = expand p in
+    | Some (Leaving c) ->
+      H.add h c true;
+      fold_aux s h f (f acc (expand c))
+    | Some (Enter c) ->
+      if not (H.mem h c) then begin
+        Stack.push (Leaving c) s;
+        let node = expand c in
         begin match node.step with
           | Resolution (p1, p2, _) ->
             Stack.push (Enter p2) s;
@@ -315,5 +204,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
     Stack.push (Enter p) s;
     fold_aux s h f acc
 
+  let check p = fold (fun () _ -> ()) () p
+
 end
 
diff --git a/solver/res.mli b/solver/res.mli
index 6fe8f9e9..382e5291 100644
--- a/solver/res.mli
+++ b/solver/res.mli
@@ -8,9 +8,6 @@ module type S = Res_intf.S
 
 module Make :
   functor (L : Log_intf.S) ->
-  functor (St : Solver_types.S) -> sig
-    include S with module St = St
-    val push : unit -> int
-    val pop : int -> unit
-  end
+  functor (St : Solver_types.S) ->
+    S with module St = St
 (** Functor to create a module building proofs from a sat-solver unsat trace. *)
diff --git a/solver/res_intf.ml b/solver/res_intf.ml
index 8dfce476..2cb995ee 100644
--- a/solver/res_intf.ml
+++ b/solver/res_intf.ml
@@ -45,29 +45,11 @@ module type S = sig
 
   (** {3 Proof building functions} *)
 
-  val has_been_proved : clause -> bool
-  (** Returns [true] if the clause is part of the current proof graph. This function does not alter
-      the proof graph (contrary to [is_proven]). *)
-
-  val is_proven : clause -> bool
-  (** Checks if the given clause has a derivation in the current state. Whatever the result,
-      new proven clauses (including the given clause) may be added to the proof graph. In particular,
-      hyptohesis and theory lemmas always have trivial derivations, and as such [is_proven c] (where [c]
-      is a hypothesis or lemma) will always return [true] and add it to the proof graph. *)
-
-  val prove : clause -> unit
+  val prove : clause -> proof
   (** Same as 'learn', but works on single clauses instead of vectors. *)
 
-  val learn : clause Vec.t -> unit
-  (** Learn and build proofs for the clause in the vector. Clauses in the vector should be in the order they were learned. *)
-
-  val assert_can_prove_unsat : clause -> unit
-  (** [assert_can_prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved.
-      @raise Insuficient_hyps if it is impossible. *)
-
   val prove_unsat : clause -> proof
-  (** Given a conflict clause [c], returns a proof of the empty clause. Same as [assert_can_prove_unsat] but returns
-      the proof if it succeeds.
+  (** Given a conflict clause [c], returns a proof of the empty clause.
       @raise Insuficient_hyps if it does not succeed. *)
 
   (** {3 Proof Manipulation} *)
@@ -81,10 +63,14 @@ module type S = sig
       [f] on a proof node happens after the execution on the children of the nodes. *)
 
   val unsat_core : proof -> clause list
-  (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. *)
+  (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof.
+      More efficient than using the [fold] function since it has access to the internal representation of proofs *)
 
   (** {3 Misc} *)
 
+  val check : proof -> unit
+  (** Check the contents of a proof. Mainly for internal use *)
+
   val print_clause : Format.formatter -> clause -> unit
   (** A nice looking printer for clauses, which sort the atoms before printing. *)
 
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 3d0e5fd6..384ffc8a 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -59,8 +59,8 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
     tag : int option;
     atoms : atom Vec.t;
     learnt : bool;
-    cpremise : premise;
     c_level : int;
+    mutable cpremise : premise;
     mutable activity : float;
     mutable removed : bool;
   }
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index d3b09ee0..fa056407 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -54,8 +54,8 @@ module type S = sig
     tag : int option;
     atoms : atom Vec.t;
     learnt : bool;
-    cpremise : premise;
     c_level : int;
+    mutable cpremise : premise;
     mutable activity : float;
     mutable removed : bool;
   }