diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index 7817ab033999890a71d35e35d581e2fd4689ae3b..065b5fe71a0b443d664cfaa3708db3afc759a491 100644
--- a/src_colibri2/core/datastructure.ml
+++ b/src_colibri2/core/datastructure.ml
@@ -218,32 +218,32 @@ end
 module HNode = Hashtbl(Nodes.Node)
 module HTermConst = Hashtbl(Expr.Term.Const)
 
-module Queue = struct
+module Push = struct
 
-  type 'a t = 'a Context.Queue.t Env.Unsaved.t
+  type 'a t = 'a Context.Push.t Env.Unsaved.t
 
   let create : type a. a Colibri2_popop_lib.Pp.pp -> _ -> a t = fun pp name ->
     let module M = struct
-      type t = a Context.Queue.t
+      type t = a Context.Push.t
       let name = name end
     in
     let key = Env.Unsaved.create_key (module M) in
-    let init = Context.Queue.create in
-    let pp = Colibri2_popop_lib.Pp.(iter1 Context.Queue.iter semi pp) in
+    let init = Context.Push.create in
+    let pp = Colibri2_popop_lib.Pp.(iter1 Context.Push.iter semi pp) in
     Env.Unsaved.register ~init ~pp key;
     key
 
   let push t d v =
-    Context.Queue.push (Egraph.get_unsaved_env d t) v
+    Context.Push.push (Egraph.get_unsaved_env d t) v
 
   let iter ~f t d =
-    Context.Queue.iter f (Egraph.get_unsaved_env d t)
+    Context.Push.iter f (Egraph.get_unsaved_env d t)
 
   let fold ~f ~init t d =
-    Context.Queue.fold f init (Egraph.get_unsaved_env d t)
+    Context.Push.fold f init (Egraph.get_unsaved_env d t)
 
-  let length t d = Context.Queue.length (Egraph.get_unsaved_env d t)
-  let get t d i = Context.Queue.get (Egraph.get_unsaved_env d t) i
+  let length t d = Context.Push.length (Egraph.get_unsaved_env d t)
+  let get t d i = Context.Push.get (Egraph.get_unsaved_env d t) i
 
 end
 
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
index 63cc3222a1b45c791447560005ee9a388aae4774..bcbbd8eeeeb250b3d77491447ba3c2d8060b5a6d 100644
--- a/src_colibri2/core/datastructure.mli
+++ b/src_colibri2/core/datastructure.mli
@@ -75,7 +75,7 @@ module Memo (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key :=
 module HNode : Sig with type key := Nodes.Node.t
 module HTermConst : Sig with type key := Expr.Term.Const.t
 
-module Queue: sig
+module Push: sig
   type 'a t
 
   val create: 'a Format.printer -> string -> 'a t
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index cc708f14d5a08cc6768033bfd869ad38cc07ae78..b91e3ce738c2879d7ba66c5fa5c9a8c52b335a29 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -277,10 +277,10 @@ module Defs = struct
       end
 end
 
-let registered_converter = Datastructure.Queue.create Fmt.nop "Ground.converters"
+let registered_converter = Datastructure.Push.create Fmt.nop "Ground.converters"
 
 let register_converter d f =
-  Datastructure.Queue.push registered_converter d f
+  Datastructure.Push.push registered_converter d f
 
 let dom_tys =
   DomKind.create_key
@@ -325,7 +325,7 @@ let init d =
        let s = ThTerm.sem g in
        add_ty d n s.ty;
        Defs.converter d g;
-       Datastructure.Queue.iter registered_converter d ~f:(fun f -> f d g))
+       Datastructure.Push.iter registered_converter d ~f:(fun f -> f d g))
     d;
   Demon.Fast.register_init_daemon ~name:"Ground.convert"
     (module ThClosedQuantifier)
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index ca255f6b892dca94b6c7f7a624b2fdd95b39df66..1a549d2e1d53d905e41843689a5041e5258e2db1 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -36,15 +36,15 @@ type during = {
 type env = Before  (** fixing model *) | During of during [@@deriving show]
 
 module Data = struct
-  let check = Datastructure.Queue.create Fmt.nop "Interp.check"
+  let check = Datastructure.Push.create Fmt.nop "Interp.check"
 
-  let node = Datastructure.Queue.create Fmt.nop "Interp.node"
+  let node = Datastructure.Push.create Fmt.nop "Interp.node"
 
-  let ty = Datastructure.Queue.create Fmt.nop "Interp.ty"
+  let ty = Datastructure.Push.create Fmt.nop "Interp.ty"
 
-  let reg_ground = Datastructure.Queue.create Fmt.nop "Interp.reg_ground"
+  let reg_ground = Datastructure.Push.create Fmt.nop "Interp.reg_ground"
 
-  (* let reg_node = Datastructure.Queue.create Fmt.nop "Interp.reg_node" *)
+  (* let reg_node = Datastructure.Push.create Fmt.nop "Interp.reg_node" *)
 
   let env =
     Env.Saved.create_key
@@ -113,11 +113,11 @@ module Register : sig
 end = struct
   open Data
 
-  let check d f = Datastructure.Queue.push check d f
+  let check d f = Datastructure.Push.push check d f
 
-  let node d f = Datastructure.Queue.push node d f
+  let node d f = Datastructure.Push.push node d f
 
-  let ty d f = Datastructure.Queue.push ty d f
+  let ty d f = Datastructure.Push.push ty d f
 end
 
 let spy_sequence msg s i =
@@ -132,7 +132,7 @@ let spy_sequence msg s i =
 let get_registered (type a) exn db call d x =
   let exception Found of a in
   match
-    Datastructure.Queue.iter
+    Datastructure.Push.iter
       ~f:(fun f -> Option.iter (call f d x) ~f:(fun s -> raise (Found s)))
       db d
   with
@@ -198,7 +198,7 @@ exception GroundTermWithoutValueAfterModelFixing of Ground.t
 exception ArgOfGroundTermWithoutValueAfterModelFixing of Ground.t * Node.t
 
 let check_ground_terms d =
-  Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
+  Datastructure.Push.iter Data.reg_ground d ~f:(fun g ->
       if Option.is_none (Egraph.get_value d (Ground.node g)) then
         raise (GroundTermWithoutValueAfterModelFixing g);
       IArray.iter (Ground.sem g).args ~f:(fun n ->
@@ -234,7 +234,7 @@ let sequence_of_ground d =
       if Option.is_none (Egraph.get_value d n) then Queue.enqueue inits n;
       Hashtbl.set n2g ~key:n ~data:[])
   in
-  Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
+  Datastructure.Push.iter Data.reg_ground d ~f:(fun g ->
       let n = Egraph.find d (Ground.node g) in
       push n;
       IArray.iter ~f:push (Ground.sem g).args;
@@ -414,7 +414,7 @@ end
 let init d =
   Egraph.set_env d Data.env Before;
   (* Demon.Fast.register_any_new_node_daemon ~name:"Interp.new_node"
-   *   (fun d g -> Datastructure.Queue.push Data.reg_node d g)
+   *   (fun d g -> Datastructure.Push.push Data.reg_node d g)
    *   d; *)
   Ground.register_converter d (fun d g ->
-      Datastructure.Queue.push Data.reg_ground d g)
+      Datastructure.Push.push Data.reg_ground d g)
diff --git a/src_colibri2/stdlib/context.ml b/src_colibri2/stdlib/context.ml
index a189dcb3e0880fe90adde5f1da2a80baae0d7570..ac13de13312cd1da9200eba12483f80a4d55c080 100644
--- a/src_colibri2/stdlib/context.ml
+++ b/src_colibri2/stdlib/context.ml
@@ -298,7 +298,7 @@ module Basic(S:sig
 
 end
 
-module Queue = struct
+module Push = struct
 
   type 'a t = {
     v : 'a Vector.vector;
diff --git a/src_colibri2/stdlib/context.mli b/src_colibri2/stdlib/context.mli
index bd74832fbbdad707c3e3180b29e13606600cad48..45e05c0741c97f7ad469ee6e25529a2a6e598df5 100644
--- a/src_colibri2/stdlib/context.mli
+++ b/src_colibri2/stdlib/context.mli
@@ -168,7 +168,7 @@ module Expert: sig
   val create: creator -> 'a history
 end
 
-module Queue: sig
+module Push: sig
 
   type 'a t
 
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 103be8d66cb1da63bd67993901a635a0fb219b44..22624bd5e5683bcce55a1c9a65f22684b62f80d6 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -21,7 +21,7 @@
 open Colibri2_popop_lib
 open Colibri2_core
 
-let comparisons = Datastructure.Queue.create Ground.pp "LRA.fourier.comparisons"
+let comparisons = Datastructure.Push.create Ground.pp "LRA.fourier.comparisons"
 let scheduled = Datastructure.Ref.create Bool.pp "LRA.fourier.scheduled" false
 
 let debug = Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "fourier"
@@ -178,7 +178,7 @@ let fm (d:Egraph.t) =
   Debug.dprintf0 debug "[Fourier]";
   Debug.incr stats_run;
   Datastructure.Ref.set scheduled d false;
-  let eqs, vars = Datastructure.Queue.fold comparisons d
+  let eqs, vars = Datastructure.Push.fold comparisons d
       ~f:(make_equations d) ~init:([],Node.S.empty)
   in
   let rec split n positive negative absent = function
@@ -258,7 +258,7 @@ let converter d (f:Ground.t) =
     in
     IArray.iter ~f:attach args;
     Egraph.attach_value d (Ground.node f) Boolean.dom Daemon.key ();
-    Datastructure.Queue.push comparisons d f;
+    Datastructure.Push.push comparisons d f;
     Egraph.register_delayed_event d Daemon.key ()
   | _ -> ()
 
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index 3949f617514b4d1091bc934c2f4a486f9f46e772..6d5c02821debd380d6ea727c0407db71eed327a9 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -112,7 +112,7 @@ let pp_ips = HPP.create Fmt.nop "Quantifier.pp" (fun c _ -> create c)
 
 (** parent-type, wait for a type to match a variable *)
 let pt_ips =
-  HPT.create Fmt.nop "Quantifier.pt" (fun c _ -> Context.Queue.create c)
+  HPT.create Fmt.nop "Quantifier.pt" (fun c _ -> Context.Push.create c)
 
 (** parent-node, wait for a subterm with the right class *)
 let pn_ips = HPN.create Fmt.nop "Quantifier.pn" (fun c _ -> create c)
@@ -159,7 +159,7 @@ let insert_pattern d (trigger : Trigger.t) =
         in
         let ips = List.map (fun pp -> HPP.find pp_ips d pp) pairs in
         let ip = create (Egraph.context d) in
-        Context.Queue.push (HPT.find pt_ips d fp) (v.ty, ip);
+        Context.Push.push (HPT.find pt_ips d fp) (v.ty, ip);
         let ips = ip :: ips in
         let ips = List.map (add_match p) ips in
         ips
diff --git a/src_colibri2/theories/quantifier/InvertedPath.mli b/src_colibri2/theories/quantifier/InvertedPath.mli
index c2a1ed3b00e6a45e23b63414a4faf088e0d904b6..47c93d5e44ed7cf3a6107fd4b20b65c2deae3b6b 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.mli
+++ b/src_colibri2/theories/quantifier/InvertedPath.mli
@@ -51,7 +51,7 @@ val pc_ips : t HPC.t
 
 module HPT : Datastructure.Memo with type key := F_Pos.t
 
-val pt_ips : (Expr.Ty.t * t) Context.Queue.t HPT.t
+val pt_ips : (Expr.Ty.t * t) Context.Push.t HPT.t
 (** The database of inverted path for each parent-type, needed for polymorphic
     variables *)
 
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index 6996c6cc69581812b25fea768cd9587027d51ccf..dc3873dc00ab4fefd51e519b3a056ad147f3714c 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -266,14 +266,14 @@ let get_pps pattern =
     m
 
 let env_ground_by_apps =
-  F.EnvApps.create (Context.Queue.pp ~sep:Fmt.semi Ground.pp)
-    "Quantifier.Trigger.ground_by_apps" (fun c _ -> Context.Queue.create c)
+  F.EnvApps.create (Context.Push.pp ~sep:Fmt.semi Ground.pp)
+    "Quantifier.Trigger.ground_by_apps" (fun c _ -> Context.Push.create c)
 
 module EnvTy = Datastructure.Memo (Ground.Ty)
 
 let env_node_by_ty =
-  EnvTy.create (Context.Queue.pp ~sep:Fmt.semi Node.pp)
-    "Quantifier.Trigger.node_by_ty" (fun c _ -> Context.Queue.create c)
+  EnvTy.create (Context.Push.pp ~sep:Fmt.semi Node.pp)
+    "Quantifier.Trigger.node_by_ty" (fun c _ -> Context.Push.create c)
 
 let match_any_term d subst (p : t) : Ground.Subst.S.t =
   Debug.dprintf2 debug "[Quant] matching any for %a" pp p;
@@ -286,7 +286,7 @@ let match_any_term d subst (p : t) : Ground.Subst.S.t =
           else
             Ground.Subst.S.fold_left
               (fun acc subst ->
-                Context.Queue.fold
+                Context.Push.fold
                   (fun acc n ->
                     Ground.Subst.S.add
                       {
@@ -298,7 +298,7 @@ let match_any_term d subst (p : t) : Ground.Subst.S.t =
               acc substs)
         env_node_by_ty d Ground.Subst.S.empty
   | App (pf, ptyl, pargs) ->
-      Context.Queue.fold
+      Context.Push.fold
         (fun acc n ->
           let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
           assert (Term.Const.equal f pf);
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index 81e4e87d9e26ddd8dfb16c28c59fe7ec70974230..c32d8c7bee7114c4493fd93f759010dd464a8c16 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -64,10 +64,10 @@ val match_any_term : Egraph.t -> Ground.Subst.S.t -> t -> Ground.Subst.S.t
 val get_pps : t -> PP.t list Term.Var.M.t
 (** [get_pps pat] return the parent-parent pairs in [pat] for each variables *)
 
-val env_ground_by_apps : Ground.t Context.Queue.t F.EnvApps.t
+val env_ground_by_apps : Ground.t Context.Push.t F.EnvApps.t
 (** The set of ground terms sorted by their top function *)
 
 module EnvTy : Datastructure.Memo with type key := Ground.Ty.t
 
-val env_node_by_ty : Node.t Context.Queue.t EnvTy.t
+val env_node_by_ty : Node.t Context.Push.t EnvTy.t
 (** The set of nodes sorted by their type. A node can have multiple types *)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index dabab5f4ac4ed2ca66522dfea157f41d49c25264..50d0c035071d8a4b1acdb2e3a2b76ab34d2b779b 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -92,7 +92,7 @@ let find_new_event d n (info : Info.t) n' (info' : Info.t) =
     let aux acc n info1 n' _ =
       match F_Pos.M.find_opt f_pos info1.Info.parents with
       | Some _ ->
-          Context.Queue.fold
+          Context.Push.fold
             (fun acc (vty, ip) ->
               let substs_by n0 =
                 let match_ty (acc : Ground.Subst.S.t) ty : Ground.Subst.S.t =
@@ -289,11 +289,11 @@ let add_info_on_ground_terms d thg =
   IArray.iteri ~f:add_pc g.args;
   merge_info res
     { Info.empty with apps = F.M.singleton g.app (Ground.S.singleton thg) };
-  Context.Queue.push (F.EnvApps.find Pattern.env_ground_by_apps d g.app) thg;
-  Context.Queue.push (Pattern.EnvTy.find Pattern.env_node_by_ty d g.ty) res;
+  Context.Push.push (F.EnvApps.find Pattern.env_ground_by_apps d g.app) thg;
+  Context.Push.push (Pattern.EnvTy.find Pattern.env_node_by_ty d g.ty) res;
   (* Try pattern from the start *)
   let trgs = F.EnvApps.find Trigger.env_tri_by_apps d g.app in
-  Context.Queue.iter (fun trg -> Trigger.match_ d trg res) trgs
+  Context.Push.iter (fun trg -> Trigger.match_ d trg res) trgs
 
 let th_register d =
   let delay = Events.Delayed_by 10 in
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index c4c447bfef6cfa98f2ea6249eadb446df9f710f8..b05f39aa1e7f69c8e0bfb3a86ed46cc17e4c9a25 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -153,16 +153,16 @@ let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
   in
   pats
 
-let env_vars = Datastructure.Queue.create pp "Quantifier.Trigger.vars"
+let env_vars = Datastructure.Push.create pp "Quantifier.Trigger.vars"
 
 let env_tri_by_apps =
-  F.EnvApps.create (Context.Queue.pp ~sep:Fmt.semi pp)
-    "Quantifier.Trigger.tri_by_apps" (fun c _ -> Context.Queue.create c)
+  F.EnvApps.create (Context.Push.pp ~sep:Fmt.semi pp)
+    "Quantifier.Trigger.tri_by_apps" (fun c _ -> Context.Push.create c)
 
 let add_trigger d t =
   match t.pat with
-  | Var _ -> Datastructure.Queue.push env_vars d t
-  | App (f, _, _) -> Context.Queue.push (F.EnvApps.find env_tri_by_apps d f) t
+  | Var _ -> Datastructure.Push.push env_vars d t
+  | App (f, _, _) -> Context.Push.push (F.EnvApps.find env_tri_by_apps d f) t
   | Node _ -> ()
 
 let instantiate_aux d tri subst =
diff --git a/src_colibri2/theories/quantifier/trigger.mli b/src_colibri2/theories/quantifier/trigger.mli
index 8dca75064344fd38259726a93fb7f547e878a07d..5d0dc129652220b2ca5d761d85add8dbcaeb6eb1 100644
--- a/src_colibri2/theories/quantifier/trigger.mli
+++ b/src_colibri2/theories/quantifier/trigger.mli
@@ -39,10 +39,10 @@ val compute_top_triggers : Ground.ThClosedQuantifier.t -> t list
 val compute_all_triggers : Ground.ThClosedQuantifier.t -> t list
 (** Compute all the triggers whose patterns contain all the variables of the formula *)
 
-val env_vars : t Datastructure.Queue.t
+val env_vars : t Datastructure.Push.t
 (** Triggers that are only variables *)
 
-val env_tri_by_apps : t Context.Queue.t F.EnvApps.t
+val env_tri_by_apps : t Context.Push.t F.EnvApps.t
 (** Triggers sorted by their top symbol *)
 
 val add_trigger : Egraph.t -> t -> unit
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index a4e4615acb714becba5019404e8ee69603944eb1..017874c96884573a680df6aa78ca5904ec3cd8e0 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -230,18 +230,18 @@ module USModel = struct
   (** The value created for uninterpreted sorts *)
 
   let create_value q ty =
-    US.nodevalue @@ US.index { id = Context.Queue.length q; ty }
+    US.nodevalue @@ US.index { id = Context.Push.length q; ty }
 
   (** The values are generated so we could just store the current id,
       and pay the small cost of indexing *)
   let env =
-    H.create (Context.Queue.pp Value.pp) "Uninterp.Model.env" (fun creator _ ->
-        Context.Queue.create creator)
+    H.create (Context.Push.pp Value.pp) "Uninterp.Model.env" (fun creator _ ->
+        Context.Push.create creator)
 
   let new_value d ty =
     let q = H.find env d ty in
     let v = create_value q ty in
-    Context.Queue.push q v;
+    Context.Push.push q v;
     (v, q)
 end
 
@@ -252,7 +252,7 @@ let init_ty d =
           match Ground.Ty.definition sym with
           | Abstract ->
               let _, q = USModel.new_value d ty in
-              Some (Interp.SeqLim.of_seq d (Context.Queue.of_seq q))
+              Some (Interp.SeqLim.of_seq d (Context.Push.of_seq q))
           | _ -> None)
       | _ -> None)
 
diff --git a/src_common/interval.mlw b/src_common/interval.mlw
index f348f33a3f04785f7fe9c6a11de1ec248afcc978..a97b41139949b1accb3fc098ed9d91e9321d41dc 100644
--- a/src_common/interval.mlw
+++ b/src_common/interval.mlw
@@ -26,6 +26,7 @@ module Convexe
        else Q.(minv < maxv)
      end
    }
+   by { a = Inf }
 
    predicate cmp (x:real) (b:Bound.t) (y:real) =
      match b with
diff --git a/src_common/interval/why3session.xml b/src_common/interval/why3session.xml
index 26653aeabf18d431ac48c71a83c38768a162123f..670d406f4ddf79fdf2c326845fc578e77437a943 100644
--- a/src_common/interval/why3session.xml
+++ b/src_common/interval/why3session.xml
@@ -5,90 +5,172 @@
 <prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.3.3" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
-<file format="whyml" proved="true">
+<prover id="3" name="Colibri2" version="0.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<file format="whyml">
 <path name=".."/><path name="interval.mlw"/>
-<theory name="Convexe" proved="true">
+<theory name="Convexe">
  <goal name="t&#39;&#39;vc" expl="VC for t&#39;" proved="true">
- <proof prover="2"><result status="valid" time="0.04" steps="15710"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="15710"/></proof>
+ <proof prover="3"><path name="interval-Convexe-tqtqtvc_1.psmt2"/><result status="valid" time="0.00"/></proof>
  </goal>
- <goal name="exists_mem&#39;vc" expl="VC for exists_mem" proved="true">
- <proof prover="1"><result status="valid" time="0.54" steps="3253"/></proof>
+ <goal name="exists_mem&#39;vc" expl="VC for exists_mem">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.54" steps="3253"/></proof>
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+  <goal name="exists_mem&#39;vc.0" expl="postcondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="exists_mem&#39;vc.1" expl="postcondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="exists_mem&#39;vc.2" expl="postcondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="exists_mem&#39;vc.3" expl="postcondition">
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
+  <transf name="unfold" arg1="mem">
+   <goal name="exists_mem&#39;vc.3.0" expl="VC for exists_mem">
+   <transf name="split_vc" >
+    <goal name="exists_mem&#39;vc.3.0.0" expl="VC for exists_mem" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="exists_mem&#39;vc.3.0.1" expl="VC for exists_mem" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="exists_mem&#39;vc.3.0.2" expl="VC for exists_mem">
+    <proof prover="3"><result status="timeout" time="5.00"/></proof>
+    <transf name="unfold" arg1="cmp">
+     <goal name="exists_mem&#39;vc.3.0.2.0" expl="VC for exists_mem">
+     <transf name="split_vc" >
+      <goal name="exists_mem&#39;vc.3.0.2.0.0" expl="VC for exists_mem">
+      <proof prover="3"><result status="timeout" time="5.00"/></proof>
+      </goal>
+      <goal name="exists_mem&#39;vc.3.0.2.0.1" expl="VC for exists_mem">
+      <proof prover="3"><result status="timeout" time="5.00"/></proof>
+      <transf name="instantiate" arg1="t&#39;&#39;invariant" arg2="e">
+       <goal name="exists_mem&#39;vc.3.0.2.0.1.0" expl="VC for exists_mem">
+       <proof prover="3"><result status="highfailure" time="3.05"/></proof>
+       <transf name="cut" arg1="x6 &lt; x4">
+        <goal name="exists_mem&#39;vc.3.0.2.0.1.0.0" expl="VC for exists_mem">
+        <proof prover="3"><result status="highfailure" time="3.07"/></proof>
+        </goal>
+        <goal name="exists_mem&#39;vc.3.0.2.0.1.0.1" expl="asserted formula" proved="true">
+        <proof prover="3"><result status="valid" time="0.01"/></proof>
+        </goal>
+       </transf>
+       </goal>
+      </transf>
+      </goal>
+     </transf>
+     </goal>
+    </transf>
+    </goal>
+    <goal name="exists_mem&#39;vc.3.0.3" expl="VC for exists_mem">
+    <proof prover="3"><result status="timeout" time="5.00"/></proof>
+    </goal>
+   </transf>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
  </goal>
- <goal name="is_singleton&#39;vc" expl="VC for is_singleton" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="is_singleton&#39;vc" expl="VC for is_singleton">
+ <transf name="split_vc" >
   <goal name="is_singleton&#39;vc.0" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="27812"/></proof>
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="27812"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.1" expl="assertion" proved="true">
-  <proof prover="2"><result status="valid" time="0.06" steps="7112"/></proof>
+  <proof prover="2" obsolete="true"><result status="valid" time="0.06" steps="7112"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.2" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.15" steps="831"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.15" steps="831"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.3" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.13" steps="867"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.13" steps="867"/></proof>
+  <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.4" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.13" steps="834"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.13" steps="834"/></proof>
+  <proof prover="3"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.5" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.14" steps="851"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.14" steps="851"/></proof>
+  <proof prover="3"><result status="valid" time="0.10"/></proof>
   </goal>
-  <goal name="is_singleton&#39;vc.6" expl="assertion" proved="true">
-  <proof prover="2"><result status="valid" time="0.02" steps="7657"/></proof>
+  <goal name="is_singleton&#39;vc.6" expl="assertion">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="7657"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.7" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.03" steps="197"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="197"/></proof>
+  <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="is_singleton&#39;vc.8" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.13" steps="150"/></proof>
+  <goal name="is_singleton&#39;vc.8" expl="assertion">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.13" steps="150"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="is_singleton&#39;vc.9" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.02" steps="63"/></proof>
+  <goal name="is_singleton&#39;vc.9" expl="assertion">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="63"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="is_singleton&#39;vc.10" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="63"/></proof>
+  <goal name="is_singleton&#39;vc.10" expl="assertion">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="63"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="is_singleton&#39;vc.11" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="66"/></proof>
+  <goal name="is_singleton&#39;vc.11" expl="assertion">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="66"/></proof>
+  <proof prover="3"><result status="highfailure" time="1.46"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.12" expl="assertion" proved="true">
-  <proof prover="2"><result status="valid" time="0.03" steps="7320"/></proof>
+  <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7320"/></proof>
+  <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.13" expl="assertion" proved="true">
-  <proof prover="2"><result status="valid" time="0.03" steps="7337"/></proof>
+  <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7337"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="is_singleton&#39;vc.14" expl="postcondition" proved="true">
-  <transf name="split_vc" proved="true" >
+  <goal name="is_singleton&#39;vc.14" expl="postcondition">
+  <transf name="split_vc" >
    <goal name="is_singleton&#39;vc.14.0" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="is_singleton&#39;vc.14.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="20"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.14.0.1" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="32003"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="32003"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.14.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="20"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.14.0.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="119"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="119"/></proof>
+    <proof prover="3"><result status="valid" time="0.46"/></proof>
     </goal>
    </transf>
    </goal>
-   <goal name="is_singleton&#39;vc.14.1" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
+   <goal name="is_singleton&#39;vc.14.1" expl="postcondition">
+   <transf name="split_vc" >
     <goal name="is_singleton&#39;vc.14.1.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.05"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.14.1.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.03"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.14.1.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="is_singleton&#39;vc.14.1.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="109"/></proof>
+    <goal name="is_singleton&#39;vc.14.1.3" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="109"/></proof>
+    <proof prover="3"><result status="timeout" time="5.00"/></proof>
     </goal>
    </transf>
    </goal>
@@ -97,107 +179,136 @@
   <goal name="is_singleton&#39;vc.15" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="is_singleton&#39;vc.15.0" expl="postcondition" proved="true">
-   <proof prover="2" timelimit="5"><result status="valid" time="0.02" steps="7017"/></proof>
+   <proof prover="2" timelimit="5" obsolete="true"><result status="valid" time="0.02" steps="7017"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="is_singleton&#39;vc.15.1" expl="postcondition" proved="true">
-   <proof prover="2" timelimit="5"><result status="valid" time="0.02" steps="7055"/></proof>
+   <proof prover="2" timelimit="5" obsolete="true"><result status="valid" time="0.02" steps="7055"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="is_singleton&#39;vc.15.2" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.02" steps="7047"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="7047"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="is_singleton&#39;vc.15.3" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.02" steps="41007"/></proof>
-   <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
-   <proof prover="2"><result status="valid" time="0.03" steps="8566"/></proof>
+   <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="41007"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="28"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="8566"/></proof>
+   <proof prover="3"><result status="valid" time="0.10"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
  <goal name="singleton&#39;vc" expl="VC for singleton" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="30166"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.00" steps="30166"/></proof>
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
  </goal>
- <goal name="except&#39;vc" expl="VC for except" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="except&#39;vc" expl="VC for except">
+ <transf name="split_vc" >
   <goal name="except&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="except&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="except&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+  <goal name="except&#39;vc.2" expl="precondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="11"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="except&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+  <goal name="except&#39;vc.3" expl="precondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="11"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="except&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="55"/></proof>
+  <goal name="except&#39;vc.4" expl="precondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="55"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="except&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="53"/></proof>
+  <goal name="except&#39;vc.5" expl="precondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="53"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
   <goal name="except&#39;vc.6" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="except&#39;vc.6.0" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="except&#39;vc.6.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="18"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="except&#39;vc.6.0.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="except&#39;vc.6.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="1.05" steps="3161"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="1.05" steps="3161"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="except&#39;vc.6.0.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="except&#39;vc.6.0.4" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.44" steps="1651"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.44" steps="1651"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="except&#39;vc.6.0.5" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="except&#39;vc.6.0.6" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.42" steps="1778"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.42" steps="1778"/></proof>
+    <proof prover="3"><result status="valid" time="0.04"/></proof>
     </goal>
     <goal name="except&#39;vc.6.0.7" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.47" steps="1928"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.47" steps="1928"/></proof>
+    <proof prover="3"><result status="valid" time="0.03"/></proof>
     </goal>
     <goal name="except&#39;vc.6.0.8" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.62" steps="2794"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.62" steps="2794"/></proof>
+    <proof prover="3"><result status="valid" time="0.07"/></proof>
     </goal>
    </transf>
    </goal>
    <goal name="except&#39;vc.6.1" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="except&#39;vc.6.1.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="except&#39;vc.6.1.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="except&#39;vc.6.1.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="101"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="101"/></proof>
+    <proof prover="3"><result status="valid" time="0.03"/></proof>
     </goal>
     <goal name="except&#39;vc.6.1.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="except&#39;vc.6.1.4" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.02" steps="101"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="101"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="except&#39;vc.6.1.5" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="except&#39;vc.6.1.6" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="119"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="119"/></proof>
+    <proof prover="3"><result status="valid" time="0.03"/></proof>
     </goal>
     <goal name="except&#39;vc.6.1.7" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="119"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="119"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="except&#39;vc.6.1.8" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.09" steps="639"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.09" steps="639"/></proof>
+    <proof prover="3"><result status="valid" time="0.05"/></proof>
     </goal>
    </transf>
    </goal>
@@ -205,357 +316,449 @@
   </goal>
  </transf>
  </goal>
- <goal name="is_comparable&#39;vc" expl="VC for is_comparable" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="is_comparable&#39;vc" expl="VC for is_comparable">
+ <transf name="split_vc" >
   <goal name="is_comparable&#39;vc.0" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.2" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="is_comparable&#39;vc.2.0" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="is_comparable&#39;vc.2.1" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+   <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="is_comparable&#39;vc.2.2" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.11" steps="12"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.11" steps="12"/></proof>
+   <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="is_comparable&#39;vc.2.3" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+   <proof prover="3"><result status="valid" time="0.00"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="is_comparable&#39;vc.3" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.4" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="2.26" steps="4390"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="2.26" steps="4390"/></proof>
+  <proof prover="3"><result status="valid" time="0.14"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.5" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="2.62" steps="6393"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="2.62" steps="6393"/></proof>
+  <proof prover="3"><result status="valid" time="1.64"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.6" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.7" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.8" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="2.47" steps="5293"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="2.47" steps="5293"/></proof>
+  <proof prover="3"><result status="valid" time="1.63"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.9" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="1.59" steps="4469"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="1.59" steps="4469"/></proof>
+  <proof prover="3"><result status="valid" time="0.11"/></proof>
   </goal>
   <goal name="is_comparable&#39;vc.10" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
   </goal>
-  <goal name="is_comparable&#39;vc.11" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="2.07" steps="5669"/></proof>
+  <goal name="is_comparable&#39;vc.11" expl="postcondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="2.07" steps="5669"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="is_comparable&#39;vc.12" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="1.64" steps="5189"/></proof>
+  <goal name="is_comparable&#39;vc.12" expl="postcondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="1.64" steps="5189"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="is_comparable&#39;vc.13" expl="postcondition" proved="true">
-  <transf name="split_vc" proved="true" >
-   <goal name="is_comparable&#39;vc.13.0" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
+  <goal name="is_comparable&#39;vc.13" expl="postcondition">
+  <transf name="split_vc" >
+   <goal name="is_comparable&#39;vc.13.0" expl="postcondition">
+   <transf name="split_vc" >
     <goal name="is_comparable&#39;vc.13.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.03" steps="211"/></proof>
-    <proof prover="2"><result status="valid" time="0.47" steps="110468"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="211"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.47" steps="110468"/></proof>
+    <proof prover="3"><result status="valid" time="0.07"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.03" steps="212"/></proof>
-    <proof prover="2"><result status="valid" time="0.75" steps="117022"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="212"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.75" steps="117022"/></proof>
+    <proof prover="3"><result status="valid" time="4.24"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.4" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.5" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.6" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.7" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.8" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.9" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.06" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.06" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.10" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="37279"/></proof>
-    <proof prover="1"><result status="valid" time="0.03" steps="209"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="37279"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="209"/></proof>
+    <proof prover="3"><result status="valid" time="0.05"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.11" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="37396"/></proof>
-    <proof prover="1"><result status="valid" time="0.03" steps="210"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="37396"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="210"/></proof>
+    <proof prover="3"><result status="valid" time="4.46"/></proof>
     </goal>
-    <goal name="is_comparable&#39;vc.13.0.12" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.01" steps="36418"/></proof>
-    <proof prover="1"><result status="valid" time="0.04" steps="272"/></proof>
+    <goal name="is_comparable&#39;vc.13.0.12" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="36418"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="272"/></proof>
+    <proof prover="3"><result status="timeout" time="5.00"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.13" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7829"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7829"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.14" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.15" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="37279"/></proof>
-    <proof prover="1"><result status="valid" time="0.06" steps="229"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="37279"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.06" steps="229"/></proof>
+    <proof prover="3"><result status="valid" time="0.09"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.16" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.30" steps="701"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.30" steps="701"/></proof>
+    <proof prover="3"><result status="valid" time="4.58"/></proof>
     </goal>
-    <goal name="is_comparable&#39;vc.13.0.17" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.42" steps="724"/></proof>
+    <goal name="is_comparable&#39;vc.13.0.17" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.42" steps="724"/></proof>
+    <proof prover="3"><result status="timeout" time="5.00"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.0.18" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7829"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7829"/></proof>
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
     </goal>
    </transf>
    </goal>
-   <goal name="is_comparable&#39;vc.13.1" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
+   <goal name="is_comparable&#39;vc.13.1" expl="postcondition">
+   <transf name="split_vc" >
     <goal name="is_comparable&#39;vc.13.1.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.4" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.01" steps="36944"/></proof>
-    <proof prover="1"><result status="valid" time="0.03" steps="208"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="36944"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="208"/></proof>
+    <proof prover="3"><result status="valid" time="0.05"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.5" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="37171"/></proof>
-    <proof prover="1"><result status="valid" time="0.03" steps="210"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="37171"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="210"/></proof>
+    <proof prover="3"><result status="valid" time="2.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.6" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.7" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.01" steps="36944"/></proof>
-    <proof prover="1"><result status="valid" time="0.07" steps="228"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="36944"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.07" steps="228"/></proof>
+    <proof prover="3"><result status="valid" time="0.05"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.8" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.32" steps="731"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.32" steps="731"/></proof>
+    <proof prover="3"><result status="valid" time="2.04"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.9" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.10" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.11" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.12" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7829"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7829"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
-    <goal name="is_comparable&#39;vc.13.1.13" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.45" steps="754"/></proof>
+    <goal name="is_comparable&#39;vc.13.1.13" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.45" steps="754"/></proof>
+    <proof prover="3"><result status="timeout" time="5.00"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.14" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.15" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7827"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.16" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7828"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.17" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7829"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7829"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.1.18" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7829"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7829"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
    </transf>
    </goal>
    <goal name="is_comparable&#39;vc.13.2" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="is_comparable&#39;vc.13.2.0" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.01" steps="38056"/></proof>
-    <proof prover="1"><result status="valid" time="0.09" steps="268"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="38056"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.09" steps="268"/></proof>
+    <proof prover="3"><result status="valid" time="0.09"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.4" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.5" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.6" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.7" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.8" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.9" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.01" steps="37310"/></proof>
-    <proof prover="1"><result status="valid" time="0.04" steps="274"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="37310"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="274"/></proof>
+    <proof prover="3"><result status="valid" time="0.06"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.10" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.11" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.04" steps="7831"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.12" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.13" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.14" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="37310"/></proof>
-    <proof prover="1"><result status="valid" time="0.06" steps="224"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="37310"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.06" steps="224"/></proof>
+    <proof prover="3"><result status="valid" time="0.06"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.15" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.16" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.17" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.2.18" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
-    <proof prover="2"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
    </transf>
    </goal>
    <goal name="is_comparable&#39;vc.13.3" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.26" steps="1034"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.26" steps="1034"/></proof>
    <transf name="split_vc" proved="true" >
     <goal name="is_comparable&#39;vc.13.3.0" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.1" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.2" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.3" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.01" steps="36975"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="36975"/></proof>
+    <proof prover="3"><result status="valid" time="0.06"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.4" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.5" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="7831"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.6" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="36975"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="36975"/></proof>
+    <proof prover="3"><result status="valid" time="0.06"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.7" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.8" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.05" steps="7831"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.9" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.10" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.11" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="7831"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.12" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.13" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.05" steps="7832"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="7832"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.14" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.05" steps="7830"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.15" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7830"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.16" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7831"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.17" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.06" steps="7832"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.06" steps="7832"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_comparable&#39;vc.13.3.18" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7832"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
    </transf>
    </goal>
@@ -563,579 +766,751 @@
   </goal>
  </transf>
  </goal>
- <goal name="is_distinct&#39;vc" expl="VC for is_distinct" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="83"/></proof>
+ <goal name="is_distinct&#39;vc" expl="VC for is_distinct">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="83"/></proof>
+ <proof prover="3"><result status="highfailure" time="3.18"/></proof>
  </goal>
- <goal name="is_included&#39;vc" expl="VC for is_included" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="is_included&#39;vc" expl="VC for is_included">
+ <transf name="split_vc" >
   <goal name="is_included&#39;vc.0" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="390"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="390"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_included&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.04" steps="644"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="644"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_included&#39;vc.2" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="is_included&#39;vc.2.0" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="is_included&#39;vc.3" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="is_included&#39;vc.4" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.29" steps="1371"/></proof>
+  <goal name="is_included&#39;vc.4" expl="postcondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.29" steps="1371"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="is_included&#39;vc.5" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.15" steps="1095"/></proof>
+  <goal name="is_included&#39;vc.5" expl="postcondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.15" steps="1095"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
   <goal name="is_included&#39;vc.6" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
   </goal>
   <goal name="is_included&#39;vc.7" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_included&#39;vc.8" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.07" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.07" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="is_included&#39;vc.9" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="4.76" steps="14893"/></proof>
+  <goal name="is_included&#39;vc.9" expl="postcondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="4.76" steps="14893"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
   <goal name="is_included&#39;vc.10" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_included&#39;vc.11" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_included&#39;vc.12" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.29" steps="1563"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.29" steps="1563"/></proof>
+  <proof prover="3"><result status="valid" time="0.73"/></proof>
   </goal>
   <goal name="is_included&#39;vc.13" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.24" steps="1281"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.24" steps="1281"/></proof>
+  <proof prover="3"><result status="valid" time="0.40"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="mem&#39;vc" expl="VC for mem" proved="true">
- <proof prover="1"><result status="valid" time="0.90" steps="5065"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.90" steps="5065"/></proof>
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
  </goal>
- <goal name="mult_pos&#39;vc" expl="VC for mult_pos" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="absent&#39;vc" expl="VC for absent" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="mult_pos&#39;vc" expl="VC for mult_pos">
+ <transf name="split_vc" >
   <goal name="mult_pos&#39;vc.0" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="mult_pos&#39;vc.0.0" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.67" steps="1606789"/></proof>
+   <proof prover="0" obsolete="true"><result status="valid" time="0.67" steps="1606789"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="mult_pos&#39;vc.0.1" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.63" steps="1635162"/></proof>
+   <proof prover="0" obsolete="true"><result status="valid" time="0.63" steps="1635162"/></proof>
+   <proof prover="3"><result status="valid" time="0.00"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="mult_pos&#39;vc.1" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="52"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="52"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="mult_pos&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
   </goal>
   <goal name="mult_pos&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="mult_pos&#39;vc.4" expl="precondition" proved="true">
   <transf name="split_vc" proved="true" >
   </transf>
   </goal>
-  <goal name="mult_pos&#39;vc.5" expl="precondition" proved="true">
-  <transf name="split_vc" proved="true" >
-   <goal name="mult_pos&#39;vc.5.0" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.05" steps="86"/></proof>
+  <goal name="mult_pos&#39;vc.5" expl="precondition">
+  <transf name="split_vc" >
+   <goal name="mult_pos&#39;vc.5.0" expl="precondition">
+   <proof prover="1" obsolete="true"><result status="valid" time="0.05" steps="86"/></proof>
+   <proof prover="3"><result status="timeout" time="5.00"/></proof>
    </goal>
-   <goal name="mult_pos&#39;vc.5.1" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.05" steps="86"/></proof>
+   <goal name="mult_pos&#39;vc.5.1" expl="precondition">
+   <proof prover="1" obsolete="true"><result status="valid" time="0.05" steps="86"/></proof>
+   <proof prover="3"><result status="timeout" time="5.00"/></proof>
    </goal>
-   <goal name="mult_pos&#39;vc.5.2" expl="precondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.02" steps="41497"/></proof>
-   <proof prover="1"><result status="valid" time="0.05" steps="84"/></proof>
+   <goal name="mult_pos&#39;vc.5.2" expl="precondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="41497"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.05" steps="84"/></proof>
+   <proof prover="3"><result status="timeout" time="5.00"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="mult_pos&#39;vc.6" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="mult_pos&#39;vc.6.0" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.32" steps="1157"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.32" steps="1157"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="mult_pos&#39;vc.6.1" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="2.02" steps="4259"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="2.02" steps="4259"/></proof>
+   <proof prover="3"><result status="valid" time="0.07"/></proof>
    </goal>
    <goal name="mult_pos&#39;vc.6.2" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="2.52" steps="7059"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="2.52" steps="7059"/></proof>
+   <proof prover="3"><result status="valid" time="0.15"/></proof>
    </goal>
    <goal name="mult_pos&#39;vc.6.3" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="30"><result status="valid" time="9.55" steps="22347"/></proof>
+   <proof prover="1" timelimit="30" obsolete="true"><result status="valid" time="9.55" steps="22347"/></proof>
+   <proof prover="3"><result status="valid" time="3.26"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
- <goal name="mult_neg&#39;vc" expl="VC for mult_neg" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="mult_neg&#39;vc" expl="VC for mult_neg">
+ <transf name="split_vc" >
   <goal name="mult_neg&#39;vc.0" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="mult_neg&#39;vc.0.0" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.59" steps="1718062"/></proof>
+   <proof prover="0" obsolete="true"><result status="valid" time="0.59" steps="1718062"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="mult_neg&#39;vc.0.1" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.18" steps="543713"/></proof>
+   <proof prover="0" obsolete="true"><result status="valid" time="0.18" steps="543713"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="mult_neg&#39;vc.1" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="52"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="52"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="mult_neg&#39;vc.2" expl="precondition" proved="true">
   <transf name="split_vc" proved="true" >
   </transf>
   </goal>
   <goal name="mult_neg&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="mult_neg&#39;vc.4" expl="precondition" proved="true">
   <transf name="split_vc" proved="true" >
   </transf>
   </goal>
-  <goal name="mult_neg&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.16" steps="442"/></proof>
+  <goal name="mult_neg&#39;vc.5" expl="precondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.16" steps="442"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
   <goal name="mult_neg&#39;vc.6" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="mult_neg&#39;vc.6.0" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.03" steps="8296"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="8296"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="mult_neg&#39;vc.6.1" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="30"><result status="valid" time="4.45" steps="17596"/></proof>
+   <proof prover="1" timelimit="30" obsolete="true"><result status="valid" time="4.45" steps="17596"/></proof>
+   <proof prover="3"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="mult_neg&#39;vc.6.2" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="2.21" steps="6599"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="2.21" steps="6599"/></proof>
+   <proof prover="3"><result status="valid" time="0.24"/></proof>
    </goal>
    <goal name="mult_neg&#39;vc.6.3" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="30"><result status="valid" time="12.15" steps="24395"/></proof>
+   <proof prover="1" timelimit="30" obsolete="true"><result status="valid" time="12.15" steps="24395"/></proof>
+   <proof prover="3"><result status="valid" time="3.09"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
- <goal name="mult_cst&#39;vc" expl="VC for mult_cst" proved="true">
- <proof prover="1"><result status="valid" time="0.25" steps="999"/></proof>
+ <goal name="mult_cst&#39;vc" expl="VC for mult_cst">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.25" steps="999"/></proof>
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
  </goal>
- <goal name="add_cst&#39;vc" expl="VC for add_cst" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="add_cst&#39;vc" expl="VC for add_cst">
+ <transf name="split_vc" >
   <goal name="add_cst&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.06" steps="8"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.06" steps="8"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add_cst&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02" steps="6939"/></proof>
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="6939"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add_cst&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02" steps="6939"/></proof>
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="6939"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="add_cst&#39;vc.3" expl="precondition" proved="true">
-  <transf name="split_vc" proved="true" >
-   <goal name="add_cst&#39;vc.3.0" expl="precondition" proved="true">
-   <proof prover="1" timelimit="30"><result status="valid" time="0.04" steps="64"/></proof>
+  <goal name="add_cst&#39;vc.3" expl="precondition">
+  <transf name="split_vc" >
+   <goal name="add_cst&#39;vc.3.0" expl="precondition">
+   <proof prover="1" timelimit="30" obsolete="true"><result status="valid" time="0.04" steps="64"/></proof>
+   <proof prover="3"><result status="timeout" time="5.00"/></proof>
    </goal>
-   <goal name="add_cst&#39;vc.3.1" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.04" steps="64"/></proof>
+   <goal name="add_cst&#39;vc.3.1" expl="precondition">
+   <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="64"/></proof>
+   <proof prover="3"><result status="timeout" time="5.00"/></proof>
    </goal>
-   <goal name="add_cst&#39;vc.3.2" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.04" steps="62"/></proof>
+   <goal name="add_cst&#39;vc.3.2" expl="precondition">
+   <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="62"/></proof>
+   <proof prover="3"><result status="timeout" time="5.00"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="add_cst&#39;vc.4" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="add_cst&#39;vc.4.0" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.04" steps="7972"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="7972"/></proof>
+   <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="add_cst&#39;vc.4.1" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="1.62" steps="4282"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="1.62" steps="4282"/></proof>
+   <proof prover="3"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="add_cst&#39;vc.4.2" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="1.82" steps="5253"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="1.82" steps="5253"/></proof>
+   <proof prover="3"><result status="valid" time="0.11"/></proof>
    </goal>
    <goal name="add_cst&#39;vc.4.3" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="30"><result status="valid" time="5.19" steps="18377"/></proof>
+   <proof prover="1" timelimit="30" obsolete="true"><result status="valid" time="5.19" steps="18377"/></proof>
+   <proof prover="3"><result status="valid" time="4.39"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
  <goal name="add_bound&#39;vc" expl="VC for add_bound" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="31953"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="31953"/></proof>
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
  </goal>
- <goal name="add&#39;vc" expl="VC for add" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="add&#39;vc" expl="VC for add">
+ <transf name="split_vc" >
   <goal name="add&#39;vc.0" expl="precondition" proved="true">
   <transf name="split_vc" proved="true" >
   </transf>
   </goal>
   <goal name="add&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="add&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add&#39;vc.6" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="add&#39;vc.7" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add&#39;vc.8" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add&#39;vc.9" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add&#39;vc.10" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="add&#39;vc.11" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
   </goal>
   <goal name="add&#39;vc.12" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02" steps="7108"/></proof>
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="7108"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="add&#39;vc.13" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="40553"/></proof>
+  <goal name="add&#39;vc.13" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="40553"/></proof>
+  <proof prover="3"><result status="timeout" time="5.00"/></proof>
   </goal>
-  <goal name="add&#39;vc.14" expl="postcondition" proved="true">
-  <transf name="split_vc" proved="true" >
+  <goal name="add&#39;vc.14" expl="postcondition">
+  <transf name="split_vc" >
    <goal name="add&#39;vc.14.0" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.03" steps="7985"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="7985"/></proof>
+   <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="add&#39;vc.14.1" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.03" steps="8156"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="8156"/></proof>
+   <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="add&#39;vc.14.2" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.03" steps="8009"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="8009"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
    <goal name="add&#39;vc.14.3" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.03" steps="8017"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="8017"/></proof>
+   <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="add&#39;vc.14.4" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.02" steps="35698"/></proof>
+   <goal name="add&#39;vc.14.4" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="36675"/></proof>
+   <proof prover="3"><undone/></proof>
    </goal>
-   <goal name="add&#39;vc.14.5" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.01" steps="36661"/></proof>
+   <goal name="add&#39;vc.14.5" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="36661"/></proof>
+   <proof prover="3"><undone/></proof>
    </goal>
    <goal name="add&#39;vc.14.6" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.05" steps="8009"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="8009"/></proof>
+   <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="add&#39;vc.14.7" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.04" steps="8017"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="8017"/></proof>
+   <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="add&#39;vc.14.8" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.02" steps="35698"/></proof>
+   <goal name="add&#39;vc.14.8" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="43886"/></proof>
+   <proof prover="3"><undone/></proof>
    </goal>
-   <goal name="add&#39;vc.14.9" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.03" steps="36805"/></proof>
+   <goal name="add&#39;vc.14.9" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="36819"/></proof>
+   <proof prover="3"><undone/></proof>
    </goal>
    <goal name="add&#39;vc.14.10" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.04" steps="8029"/></proof>
+   <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="8029"/></proof>
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
    </goal>
-   <goal name="add&#39;vc.14.11" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.03" steps="36819"/></proof>
+   <goal name="add&#39;vc.14.11" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="36805"/></proof>
+   <proof prover="3"><undone/></proof>
    </goal>
-   <goal name="add&#39;vc.14.12" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.01" steps="36675"/></proof>
+   <goal name="add&#39;vc.14.12" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="35698"/></proof>
+   <proof prover="3"><undone/></proof>
    </goal>
-   <goal name="add&#39;vc.14.13" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.02" steps="43886"/></proof>
+   <goal name="add&#39;vc.14.13" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="35698"/></proof>
+   <proof prover="3"><undone/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
- <goal name="minus&#39;vc" expl="VC for minus" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="33927"/></proof>
+ <goal name="minus&#39;vc" expl="VC for minus">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="33927"/></proof>
+ <proof prover="3"><undone/></proof>
  </goal>
  <goal name="gt&#39;vc" expl="VC for gt" proved="true">
- <proof prover="1"><result status="valid" time="0.19" steps="1087"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.19" steps="1087"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="ge&#39;vc" expl="VC for ge" proved="true">
- <proof prover="1"><result status="valid" time="0.21" steps="1224"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.21" steps="1224"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="lt&#39;vc" expl="VC for lt" proved="true">
- <proof prover="1"><result status="valid" time="0.20" steps="1080"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.20" steps="1080"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="le&#39;vc" expl="VC for le" proved="true">
- <proof prover="1"><result status="valid" time="0.19" steps="1080"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.19" steps="1080"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="gt&#39;&#39;vc" expl="VC for gt&#39;">
+ <proof prover="3"><undone/></proof>
+ </goal>
+ <goal name="ge&#39;&#39;vc" expl="VC for ge&#39;">
+ <proof prover="3"><undone/></proof>
+ </goal>
+ <goal name="lt&#39;&#39;vc" expl="VC for lt&#39;">
+ <proof prover="3"><undone/></proof>
+ </goal>
+ <goal name="le&#39;&#39;vc" expl="VC for le&#39;">
+ <proof prover="3"><undone/></proof>
  </goal>
  <goal name="min_bound_sup&#39;vc" expl="VC for min_bound_sup" proved="true">
- <proof prover="1"><result status="valid" time="0.10" steps="1263"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.10" steps="1263"/></proof>
+ <proof prover="3"><result status="valid" time="0.42"/></proof>
  </goal>
  <goal name="min_bound_inf&#39;vc" expl="VC for min_bound_inf" proved="true">
- <proof prover="1"><result status="valid" time="0.20" steps="1546"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.20" steps="1546"/></proof>
+ <proof prover="3"><result status="valid" time="0.40"/></proof>
  </goal>
  <goal name="max_bound_sup&#39;vc" expl="VC for max_bound_sup" proved="true">
- <proof prover="1"><result status="valid" time="0.09" steps="1310"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.09" steps="1310"/></proof>
+ <proof prover="3"><result status="valid" time="0.41"/></proof>
  </goal>
  <goal name="max_bound_inf&#39;vc" expl="VC for max_bound_inf" proved="true">
- <proof prover="1"><result status="valid" time="0.15" steps="1447"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.15" steps="1447"/></proof>
+ <proof prover="3"><result status="valid" time="0.46"/></proof>
  </goal>
- <goal name="union&#39;vc" expl="VC for union" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="98815"/></proof>
+ <goal name="union&#39;vc" expl="VC for union">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="98815"/></proof>
+ <proof prover="3"><undone/></proof>
  </goal>
  <goal name="mem_bottom_som" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="8585"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="8585"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
  </goal>
- <goal name="mk_finite&#39;vc" expl="VC for mk_finite" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="mk_finite&#39;vc" expl="VC for mk_finite">
+ <transf name="split_vc" >
   <goal name="mk_finite&#39;vc.0" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="mk_finite&#39;vc.1" expl="precondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="mk_finite&#39;vc.1.0" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+   <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="12"/></proof>
+   <proof prover="3"><result status="valid" time="0.00"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="mk_finite&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="34231"/></proof>
-  <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="34231"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="11"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="mk_finite&#39;vc.3" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="mk_finite&#39;vc.3.0" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="mk_finite&#39;vc.3.0.0" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.01" steps="38371"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="38371"/></proof>
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.0.1" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="34998"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="34998"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="52"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.0.3" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="34844"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="34844"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.0.4" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="51"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="51"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
    </transf>
    </goal>
    <goal name="mk_finite&#39;vc.3.1" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="mk_finite&#39;vc.3.1.0" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="37126"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="37126"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.1.1" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.06" steps="8539"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.06" steps="8539"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.1.2" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.06" steps="8426"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.06" steps="8426"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.1.3" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="34738"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="34738"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.1.4" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.03" steps="8358"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="8358"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
    </transf>
    </goal>
    <goal name="mk_finite&#39;vc.3.2" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="mk_finite&#39;vc.3.2.0" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="38149"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="38149"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.2.1" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.05" steps="8539"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="8539"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.2.2" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.06" steps="8426"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.06" steps="8426"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.2.3" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.01" steps="34738"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="34738"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="mk_finite&#39;vc.3.2.4" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="8358"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="8358"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
    </transf>
    </goal>
   </transf>
   </goal>
+  <goal name="mk_finite&#39;vc.4" expl="postcondition">
+  <proof prover="3"><undone/></proof>
+  </goal>
  </transf>
  </goal>
- <goal name="inter&#39;vc" expl="VC for inter" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="inter&#39;vc" expl="VC for inter">
+ <transf name="split_vc" >
   <goal name="inter&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="14"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="inter&#39;vc.1" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.02" steps="78"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="78"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="inter&#39;vc.2" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.03" steps="21"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="21"/></proof>
+  <proof prover="3"><result status="valid" time="0.22"/></proof>
   </goal>
   <goal name="inter&#39;vc.3" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.59" steps="2213"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.59" steps="2213"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="inter&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="14"/></proof>
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
   </goal>
-  <goal name="inter&#39;vc.5" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="103"/></proof>
+  <goal name="inter&#39;vc.5" expl="assertion">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="103"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="inter&#39;vc.6" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.02" steps="105"/></proof>
+  <goal name="inter&#39;vc.6" expl="assertion">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="105"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="inter&#39;vc.7" expl="postcondition" proved="true">
-  <transf name="split_vc" proved="true" >
-   <goal name="inter&#39;vc.7.0" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
+  <goal name="inter&#39;vc.7" expl="postcondition">
+  <transf name="split_vc" >
+   <goal name="inter&#39;vc.7.0" expl="postcondition">
+   <transf name="split_vc" >
     <goal name="inter&#39;vc.7.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.0.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="19"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.0.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.11" steps="171"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.11" steps="171"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.0.4" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="1.21" steps="3447"/></proof>
+    <goal name="inter&#39;vc.7.0.4" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="1.21" steps="3447"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.0.5" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.07" steps="203"/></proof>
+    <goal name="inter&#39;vc.7.0.5" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.07" steps="203"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
     <goal name="inter&#39;vc.7.0.6" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="18"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.0.7" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="171"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="171"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.0.8" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="1.08" steps="2979"/></proof>
+    <goal name="inter&#39;vc.7.0.8" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="1.08" steps="2979"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.0.9" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.07" steps="202"/></proof>
+    <goal name="inter&#39;vc.7.0.9" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.07" steps="202"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
     <goal name="inter&#39;vc.7.0.10" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+    <proof prover="3"><result status="valid" time="0.03"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.0.11" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="202"/></proof>
+    <goal name="inter&#39;vc.7.0.11" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="202"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.0.12" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.13" steps="203"/></proof>
+    <goal name="inter&#39;vc.7.0.12" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.13" steps="203"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.0.13" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.13" steps="103"/></proof>
+    <goal name="inter&#39;vc.7.0.13" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.13" steps="103"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
    </transf>
    </goal>
-   <goal name="inter&#39;vc.7.1" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
+   <goal name="inter&#39;vc.7.1" expl="postcondition">
+   <transf name="split_vc" >
     <goal name="inter&#39;vc.7.1.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.07" steps="426"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.07" steps="426"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.1.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.08" steps="17"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.08" steps="17"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.1.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.06" steps="437"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.06" steps="437"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.1.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.07" steps="523"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.07" steps="523"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.1.4" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="83"/></proof>
+    <goal name="inter&#39;vc.7.1.4" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="83"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.1.5" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.69" steps="1645"/></proof>
+    <goal name="inter&#39;vc.7.1.5" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.69" steps="1645"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
     <goal name="inter&#39;vc.7.1.6" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.06" steps="436"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.06" steps="436"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.1.7" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.14" steps="524"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.14" steps="524"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.1.8" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.98" steps="2816"/></proof>
+    <goal name="inter&#39;vc.7.1.8" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.98" steps="2816"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.1.9" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.50" steps="1796"/></proof>
+    <goal name="inter&#39;vc.7.1.9" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.50" steps="1796"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
     <goal name="inter&#39;vc.7.1.10" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="481"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="481"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.1.11" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.04" steps="717"/></proof>
+    <goal name="inter&#39;vc.7.1.11" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="717"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.1.12" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.14" steps="715"/></proof>
+    <goal name="inter&#39;vc.7.1.12" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.14" steps="715"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.1.13" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.94" steps="3410"/></proof>
+    <goal name="inter&#39;vc.7.1.13" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.94" steps="3410"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
    </transf>
    </goal>
-   <goal name="inter&#39;vc.7.2" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
+   <goal name="inter&#39;vc.7.2" expl="postcondition">
+   <transf name="split_vc" >
     <goal name="inter&#39;vc.7.2.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.2.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.02" steps="469"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="469"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.2.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.2.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.04" steps="524"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="524"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.2.4" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.02" steps="618"/></proof>
+    <goal name="inter&#39;vc.7.2.4" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="618"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.2.5" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.15" steps="715"/></proof>
+    <goal name="inter&#39;vc.7.2.5" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.15" steps="715"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
     <goal name="inter&#39;vc.7.2.6" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="inter&#39;vc.7.2.7" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.13" steps="523"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.13" steps="523"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.2.8" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="1.05" steps="3021"/></proof>
+    <goal name="inter&#39;vc.7.2.8" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="1.05" steps="3021"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.2.9" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.15" steps="717"/></proof>
+    <goal name="inter&#39;vc.7.2.9" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.15" steps="717"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
     <goal name="inter&#39;vc.7.2.10" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.02" steps="16"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.2.11" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.85" steps="1731"/></proof>
+    <goal name="inter&#39;vc.7.2.11" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.85" steps="1731"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.2.12" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.49" steps="1564"/></proof>
+    <goal name="inter&#39;vc.7.2.12" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.49" steps="1564"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
-    <goal name="inter&#39;vc.7.2.13" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.51" steps="1207"/></proof>
+    <goal name="inter&#39;vc.7.2.13" expl="postcondition">
+    <proof prover="1" obsolete="true"><result status="valid" time="0.51" steps="1207"/></proof>
+    <proof prover="3"><undone/></proof>
     </goal>
    </transf>
    </goal>
@@ -1144,101 +1519,132 @@
  </transf>
  </goal>
  <goal name="zero&#39;vc" expl="VC for zero" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="3"><result status="valid" time="0.10"/></proof>
  </goal>
  <goal name="reals&#39;vc" expl="VC for reals" proved="true">
- <proof prover="1"><result status="valid" time="0.04" steps="359"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="359"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="is_reals&#39;vc" expl="VC for is_reals">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.52" steps="2960"/></proof>
+ <proof prover="3"><undone/></proof>
  </goal>
- <goal name="is_reals&#39;vc" expl="VC for is_reals" proved="true">
- <proof prover="1"><result status="valid" time="0.52" steps="2960"/></proof>
+ <goal name="is_integer&#39;vc" expl="VC for is_integer">
+ <proof prover="3"><undone/></proof>
  </goal>
- <goal name="choose&#39;vc" expl="VC for choose" proved="true">
- <proof prover="1"><result status="valid" time="3.36" steps="8124"/></proof>
+ <goal name="choose&#39;vc" expl="VC for choose">
+ <proof prover="1" obsolete="true"><result status="valid" time="3.36" steps="8124"/></proof>
+ <proof prover="3"><undone/></proof>
  </goal>
- <goal name="split_heuristic&#39;vc" expl="VC for split_heuristic" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic&#39;vc" expl="VC for split_heuristic">
+ <transf name="split_vc" >
   <goal name="split_heuristic&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="14"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="1418"/></proof>
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="1418"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="37528"/></proof>
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="37528"/></proof>
+  <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.6" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="18"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.7" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.8" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.9" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="20"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="20"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.10" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.11" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="20"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="20"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.12" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="86"/></proof>
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="44582"/></proof>
+  <proof prover="3"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.13" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="119"/></proof>
+  <goal name="split_heuristic&#39;vc.13" expl="precondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="119"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.14" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="83"/></proof>
+  <goal name="split_heuristic&#39;vc.14" expl="precondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="83"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.15" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="44582"/></proof>
+  <goal name="split_heuristic&#39;vc.15" expl="precondition">
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="86"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.16" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="14"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.17" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="59312"/></proof>
-  <proof prover="1"><result status="valid" time="19.90" steps="5196"/></proof>
+  <goal name="split_heuristic&#39;vc.17" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="59312"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="19.90" steps="5196"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.18" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="60644"/></proof>
+  <goal name="split_heuristic&#39;vc.18" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="60644"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.19" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="1468"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.20" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="58842"/></proof>
+  <goal name="split_heuristic&#39;vc.20" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="58842"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.21" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="60260"/></proof>
+  <goal name="split_heuristic&#39;vc.21" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="59832"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.22" expl="precondition" proved="true">
-  <transf name="split_vc" proved="true" >
+  <goal name="split_heuristic&#39;vc.22" expl="precondition">
+  <transf name="split_vc" >
    <goal name="split_heuristic&#39;vc.22.0" expl="precondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="split_heuristic&#39;vc.22.0.0" expl="precondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.04" steps="10872"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="10872"/></proof>
+    <proof prover="3"><result status="valid" time="0.04"/></proof>
     </goal>
    </transf>
    </goal>
-   <goal name="split_heuristic&#39;vc.22.1" expl="precondition" proved="true">
-   <transf name="split_vc" proved="true" >
-    <goal name="split_heuristic&#39;vc.22.1.0" expl="precondition" proved="true">
-    <transf name="split_vc" proved="true" >
-     <goal name="split_heuristic&#39;vc.22.1.0.0" expl="precondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="35"/></proof>
+   <goal name="split_heuristic&#39;vc.22.1" expl="precondition">
+   <transf name="split_vc" >
+    <goal name="split_heuristic&#39;vc.22.1.0" expl="precondition">
+    <transf name="split_vc" >
+     <goal name="split_heuristic&#39;vc.22.1.0.0" expl="precondition">
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="35"/></proof>
+     <proof prover="3"><undone/></proof>
      </goal>
     </transf>
     </goal>
@@ -1247,109 +1653,136 @@
   </transf>
   </goal>
   <goal name="split_heuristic&#39;vc.23" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="1470"/></proof>
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="1470"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.24" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="58686"/></proof>
+  <goal name="split_heuristic&#39;vc.24" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="58613"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.25" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="61675"/></proof>
+  <goal name="split_heuristic&#39;vc.25" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="61675"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.26" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="1468"/></proof>
+  <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="14"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.27" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="58613"/></proof>
+  <goal name="split_heuristic&#39;vc.27" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="58686"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
-  <goal name="split_heuristic&#39;vc.28" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="59832"/></proof>
+  <goal name="split_heuristic&#39;vc.28" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="60260"/></proof>
+  <proof prover="3"><undone/></proof>
   </goal>
   <goal name="split_heuristic&#39;vc.29" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="split_heuristic&#39;vc.29.0" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="split_heuristic&#39;vc.29.0.0" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.08" steps="11264"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.08" steps="11264"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="split_heuristic&#39;vc.29.0.1" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.05" steps="12449"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="12449"/></proof>
+    <proof prover="3"><result status="valid" time="0.43"/></proof>
     </goal>
     <goal name="split_heuristic&#39;vc.29.0.2" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.07" steps="12438"/></proof>
+    <proof prover="2" obsolete="true"><result status="valid" time="0.07" steps="12438"/></proof>
+    <proof prover="3"><result status="valid" time="0.45"/></proof>
     </goal>
     <goal name="split_heuristic&#39;vc.29.0.3" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="split_heuristic&#39;vc.29.0.3.0" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="45135"/></proof>
-     <proof prover="1"><result status="valid" time="0.10" steps="292"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="45135"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.10" steps="292"/></proof>
+     <proof prover="3"><result status="valid" time="0.15"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.1" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.02" steps="109"/></proof>
-     <proof prover="2"><result status="valid" time="0.52" steps="132892"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="109"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.52" steps="132892"/></proof>
+     <proof prover="3"><result status="valid" time="0.06"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.2" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="11096"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="29"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11096"/></proof>
+     <proof prover="3"><result status="valid" time="0.32"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.3" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="109"/></proof>
-     <proof prover="2"><result status="valid" time="0.50" steps="132896"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="109"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.50" steps="132896"/></proof>
+     <proof prover="3"><result status="valid" time="0.04"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.4" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.03" steps="48671"/></proof>
-     <proof prover="1"><result status="valid" time="0.25" steps="390"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="48671"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.25" steps="390"/></proof>
+     <proof prover="3"><result status="valid" time="0.13"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.5" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="11381"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="30"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11429"/></proof>
+     <proof prover="3"><result status="valid" time="0.13"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.6" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="11096"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="29"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11096"/></proof>
+     <proof prover="3"><result status="valid" time="0.23"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.7" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="11290"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.31" steps="59"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.07" steps="10922"/></proof>
+     <proof prover="3"><result status="valid" time="0.15"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.8" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="11429"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.36" steps="59"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.07" steps="10876"/></proof>
+     <proof prover="3"><result status="valid" time="0.47"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.9" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="31"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="10821"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="34"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11026"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.10" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="36"/></proof>
-     <proof prover="2"><result status="valid" time="0.06" steps="11026"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.33" steps="55"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="10914"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.11" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="10921"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="30"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11381"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.12" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.01" steps="34"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="11026"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="31"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="10821"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.13" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.33" steps="55"/></proof>
-     <proof prover="2"><result status="valid" time="0.05" steps="10914"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="36"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.06" steps="11026"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.14" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.36" steps="59"/></proof>
-     <proof prover="2"><result status="valid" time="0.07" steps="10876"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="30"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11290"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.15" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.02" steps="36"/></proof>
-     <proof prover="2"><result status="valid" time="0.08" steps="10921"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="36"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.08" steps="10921"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.16" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.33" steps="59"/></proof>
-     <proof prover="2"><result status="valid" time="0.08" steps="10882"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.33" steps="59"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.08" steps="10882"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.0.3.17" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.31" steps="59"/></proof>
-     <proof prover="2"><result status="valid" time="0.07" steps="10922"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="40"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="10921"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
     </transf>
     </goal>
@@ -1358,117 +1791,148 @@
    <goal name="split_heuristic&#39;vc.29.1" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="split_heuristic&#39;vc.29.1.0" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.02" steps="43714"/></proof>
+    <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="43714"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="split_heuristic&#39;vc.29.1.1" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="split_heuristic&#39;vc.29.1.1.0" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="45088"/></proof>
-     <proof prover="1"><result status="valid" time="0.22" steps="1289"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="45088"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.22" steps="1289"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.1.1" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.03" steps="9272"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="9272"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.1.2" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="45539"/></proof>
-     <proof prover="1"><result status="valid" time="0.33" steps="1920"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="45539"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.33" steps="1920"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.1.3" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.1.4" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.1.5" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="45546"/></proof>
-     <proof prover="1"><result status="valid" time="0.33" steps="1926"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="45546"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.33" steps="1926"/></proof>
+     <proof prover="3"><result status="valid" time="0.03"/></proof>
      </goal>
     </transf>
     </goal>
     <goal name="split_heuristic&#39;vc.29.1.2" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="split_heuristic&#39;vc.29.1.2.0" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="45415"/></proof>
-     <proof prover="1"><result status="valid" time="0.23" steps="1328"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="45415"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.23" steps="1328"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.2.1" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.2.2" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="45524"/></proof>
-     <proof prover="1"><result status="valid" time="0.48" steps="2232"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="45524"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.48" steps="2232"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.2.3" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.2.4" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="9272"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.2.5" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="45522"/></proof>
-     <proof prover="1"><result status="valid" time="0.64" steps="2477"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="45522"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.64" steps="2477"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
     </transf>
     </goal>
     <goal name="split_heuristic&#39;vc.29.1.3" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="split_heuristic&#39;vc.29.1.3.0" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.05" steps="10777"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="10777"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.1" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.04" steps="10870"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="10870"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.2" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.05" steps="11027"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11027"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.3" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.05" steps="10870"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="10870"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.4" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.05" steps="11075"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11075"/></proof>
+     <proof prover="3"><result status="valid" time="0.01"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.5" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.04" steps="10976"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11024"/></proof>
+     <proof prover="3"><result status="valid" time="0.00"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.6" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.05" steps="11027"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11027"/></proof>
+     <proof prover="3"><result status="valid" time="0.03"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.7" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.05" steps="11167"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="60738"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.8" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.05" steps="11024"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="60808"/></proof>
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.9" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.05" steps="12177"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="49104"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.35" steps="1732"/></proof>
+     <proof prover="3"><result status="valid" time="0.04"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.10" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="49104"/></proof>
-     <proof prover="1"><result status="valid" time="0.47" steps="1517"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="59890"/></proof>
+     <proof prover="3"><result status="valid" time="0.27"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.11" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="49102"/></proof>
-     <proof prover="1"><result status="valid" time="0.67" steps="2077"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="10976"/></proof>
+     <proof prover="3"><result status="valid" time="0.30"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.12" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="49104"/></proof>
-     <proof prover="1"><result status="valid" time="0.35" steps="1732"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="12177"/></proof>
+     <proof prover="3"><result status="valid" time="0.22"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.13" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="59890"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="49104"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.47" steps="1517"/></proof>
+     <proof prover="3"><result status="valid" time="0.68"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.14" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.03" steps="60808"/></proof>
+     <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="11167"/></proof>
+     <proof prover="3"><result status="valid" time="0.77"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.15" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="49100"/></proof>
-     <proof prover="1"><result status="valid" time="0.64" steps="2011"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="49100"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.64" steps="2011"/></proof>
+     <proof prover="3"><result status="valid" time="0.22"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.16" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.04" steps="60803"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.04" steps="60803"/></proof>
+     <proof prover="3"><result status="valid" time="0.69"/></proof>
      </goal>
      <goal name="split_heuristic&#39;vc.29.1.3.17" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="0.02" steps="60738"/></proof>
+     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="49102"/></proof>
+     <proof prover="1" obsolete="true"><result status="valid" time="0.67" steps="2077"/></proof>
+     <proof prover="3"><result status="valid" time="1.10"/></proof>
      </goal>
     </transf>
     </goal>