From d811085efd81ce196a2d6cfee54ce1eb7a076a22 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 10 Apr 2006 09:02:37 +0000
Subject: [PATCH 1/1] Removed negative equations.

---
 .../tactics/paramodulation/saturation.ml      | 1443 +++--------------
 .../tactics/paramodulation/utils.ml           |    2 +-
 helm/software/components/tactics/tactics.mli  |    2 +-
 3 files changed, 215 insertions(+), 1232 deletions(-)

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index e88a061a3..5b5121e86 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -28,11 +28,6 @@
 open Inference;;
 open Utils;;
 
-let check_table t l =
-  List.fold_left
-    (fun b (_,eq) -> b && (Indexing.in_index t eq)) true l
-
-
 (* set to false to disable paramodulation inside auto_tac *)
 let connect_to_auto = true;;
 
@@ -54,7 +49,7 @@ let maximal_retained_equality = ref None;;
 
 (* equality-selection related globals *)
 let use_fullred = ref true;;
-let weight_age_ratio = ref 4 (* 5 *);; (* settable by the user *)
+let weight_age_ratio = ref 6 (* 5 *);; (* settable by the user *)
 let weight_age_counter = ref !weight_age_ratio ;;
 let symbols_ratio = ref 0 (* 3 *);;
 let symbols_counter = ref 0;;
@@ -75,16 +70,6 @@ let maxmeta = ref 0;;
 let maxdepth = ref 3;;
 let maxwidth = ref 3;;
 
-let test eq = false
-(*
-  let (_,(_,_,(ty,left,right,_),m1)) = eq in
-  let actual = 
-    (Inference.metas_of_term left)@(Inference.metas_of_term right) 
-  in
-  let m = List.filter (fun (i, _, _) -> List.mem i actual) m1 in
-    m <> m1
-;; *)
-
 type result =
   | ParamodulationFailure
   | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option
@@ -126,119 +111,50 @@ module OrderedEquality = struct
         | res -> res 
 end 
 
-(*
-module OrderedEquality = struct
-  type t = Inference.equality
-
-  let minor eq =
-    let w, _, (ty, left, right, o), _ = eq in
-      match o with
-         | Lt -> Some left
-         | Le -> assert false
-         | Gt -> Some right
-         | Ge -> assert false
-         | Eq 
-         | Incomparable -> None
-             
-  let compare eq1 eq2 =
-    let w1, _, (ty, left, right, o1), m1 = eq1
-    and w2, _, (ty', left', right', o2), m2 = eq2 in
-      match Pervasives.compare w1 w2 with
-        | 0 ->
-            (match minor eq1, minor eq2 with
-              | Some t1, Some t2 ->
-                  fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2)
-              | Some _, None -> -1
-              | None, Some _ -> 1
-              | _,_ -> 
-                  (List.length m2) - (List.length m1) )
-        | res ->  res
-  
-  let compare eq1 eq2 =
-    match compare eq1 eq2 with
-        0 -> Pervasives.compare eq1 eq2
-      | res -> res 
-end 
-*)
-
 module EqualitySet = Set.Make(OrderedEquality);;
 
 exception Empty_list;;
 
 let passive_is_empty = function
-  | ([], _), ([], _), _ -> true
+  | ([], _), _ -> true
   | _ -> false
 ;;
 
 
-let size_of_passive ((_, ns), (_, ps), _) =
-  (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
+let size_of_passive ((passive_list, ps), _) = List.length passive_list
+(* EqualitySet.cardinal ps *)
 ;;
 
 
-let size_of_active (active_list, _) =
-  List.length active_list
+let size_of_active (active_list, _) = List.length active_list
 ;;
 
 let age_factor = 0.01;;
 
-let min_elt weight l =
-  fst
-  (match l with
-      [] -> raise Empty_list
-    | a::tl -> 
-        let wa = float_of_int (weight a) in
-        let x = ref 0. in
-        List.fold_left
-          (fun (current,w) arg ->
-            x:=!x +. 1.;
-            let w1 = weight arg in
-            let wa = (float_of_int w1) +. !x *. age_factor in
-            if wa < w then (arg,wa) else (current,w))
-          (a,wa) tl)
-;;
-
-(* 
-let compare eq1 eq2 =
-  let w1, _, (ty, left, right, _), m1, _ = eq1 in
-  let w2, _, (ty', left', right', _), m2, _ = eq2 in
-  match Pervasives.compare w1 w2 with
-    | 0 -> (List.length m1) - (List.length m2)
-    | res -> res
-;;
-*)
-
 (**
    selects one equality from passive. The selection strategy is a combination
    of weight, age and goal-similarity
 *)
-let rec select env goals passive (active, _) =
+
+let rec select env goals passive =
   processed_clauses := !processed_clauses + 1;
   let goal =
     match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
   in
-  let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
-  let remove eq l =
-    List.filter (fun e -> e <> eq) l
-  in
+  let (pos_list, pos_set), passive_table = passive in
+  let remove eq l = List.filter (fun e -> e <> eq) l in
   if !weight_age_ratio > 0 then
     weight_age_counter := !weight_age_counter - 1;
   match !weight_age_counter with
   | 0 -> (
       weight_age_counter := !weight_age_ratio;
-      match neg_list, pos_list with
-      | hd::tl, pos ->
-          (* Negatives aren't indexed, no need to remove them... *)
-          (Negative, hd),
-          ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
-      | [], (hd:EqualitySet.elt)::tl ->
+      match pos_list with
+      | (hd:EqualitySet.elt)::tl ->
           let passive_table =
             Indexing.remove_index passive_table hd
-          in  (Positive, hd),
-          (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
-      | _, _ -> assert false
-    )
-  | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> 
+          in  hd, ((tl, EqualitySet.remove hd pos_set), passive_table)
+      | _ -> assert false)
+  | _ when (!symbols_counter > 0) -> 
      (symbols_counter := !symbols_counter - 1;
       let cardinality map =
         TermMap.fold (fun k v res -> res + v) map 0
@@ -276,43 +192,29 @@ let rec select env goals passive (active, _) =
       let passive_table =
         Indexing.remove_index passive_table current
       in
-      (Positive, current),
-      (([], neg_set),
-       (remove current pos_list, EqualitySet.remove current pos_set),
-       passive_table)
-    )
+	current,
+      ((remove current pos_list, EqualitySet.remove current pos_set),
+       passive_table))
   | _ ->
       symbols_counter := !symbols_ratio;
-      let set_selection set = EqualitySet.min_elt set in 
-      (* let set_selection l = min_elt (fun (w,_,_,_) -> w) l in *)
-      if EqualitySet.is_empty neg_set then
-        let current = set_selection pos_set in
-        let passive =
-          (neg_list, neg_set),
-          (remove current pos_list, EqualitySet.remove current pos_set),
-          Indexing.remove_index passive_table current
-        in
-        (Positive, current), passive
-      else
-        let current = set_selection neg_set in
-        let passive =
-          (remove current neg_list, EqualitySet.remove current neg_set),
-          (pos_list, pos_set),
-          passive_table
-        in
-        (Negative, current), passive
+      let current = EqualitySet.min_elt pos_set in
+      let passive_table =
+        Indexing.remove_index passive_table current
+      in
+        current, 
+      ((remove current pos_list, EqualitySet.remove current pos_set),
+      passive_table)
 ;;
 
 
 (* initializes the passive set of equalities *)
-let make_passive neg pos =
+let make_passive pos =
   let set_of equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
   in
   let table =
       List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos
   in
-  (neg, set_of neg),
   (pos, set_of pos),
   table
 ;;
@@ -323,29 +225,26 @@ let make_active () =
 ;;
 
 
-(* adds to passive a list of equalities: new_neg is a list of negative
-   equalities, new_pos a list of positive equalities *)
-let add_to_passive passive (new_neg, new_pos) =
-  let (neg_list, neg_set), (pos_list, pos_set), table = passive in
+(* adds to passive a list of equalities new_pos *)
+let add_to_passive passive new_pos =
+  let (pos_list, pos_set), table = passive in
   let ok set equality = not (EqualitySet.mem equality set) in
-  let neg = List.filter (ok neg_set) new_neg
-  and pos = List.filter (ok pos_set) new_pos in
+  let pos = List.filter (ok pos_set) new_pos in
   let table = 
      List.fold_left (fun tbl e -> Indexing.index tbl e) table pos 
   in
   let add set equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
   in
-  (neg @ neg_list, add neg_set neg),
   (pos_list @ pos, add pos_set pos),
   table
 ;;
 
-
+(* TODO *)
 (* removes from passive equalities that are estimated impossible to activate
    within the current time limit *)
 let prune_passive howmany (active, _) passive =
-  let (nl, ns), (pl, ps), tbl = passive in
+  let (pl, ps), tbl = passive in
   let howmany = float_of_int howmany
   and ratio = float_of_int !weight_age_ratio in
   let round v =
@@ -356,67 +255,26 @@ let prune_passive howmany (active, _) passive =
   and in_age = round (howmany /. (ratio +. 1.)) in 
   debug_print
     (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
-  let symbols, card =
-    match active with
-    | (Negative, e)::_ ->
-        let symbols = symbols_of_equality e in
-        let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
-        Some symbols, card
-    | _ -> None, 0
+  let symbols, card = None, 0
   in
   let counter = ref !symbols_ratio in
-  let rec pickw w ns ps =
+  let rec pickw w ps =
     if w > 0 then
-      if not (EqualitySet.is_empty ns) then
-        let e = EqualitySet.min_elt ns in
-        let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
-        EqualitySet.add e ns', ps
-      else if !counter > 0 then
+      if !counter > 0 then
         let _ =
           counter := !counter - 1;
-          if !counter = 0 then counter := !symbols_ratio
-        in
-        match symbols with
-        | None ->
-            let e = EqualitySet.min_elt ps in
-            let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
-            ns, EqualitySet.add e ps'
-        | Some symbols ->
-            let foldfun k v (r1, r2) =
-              if TermMap.mem k symbols then
-                let c = TermMap.find k symbols in
-                let c1 = abs (c - v) in
-                let c2 = v - c1 in
-                r1 + c2, r2 + c1
-              else
-                r1, r2 + v
-            in
-            let f equality (i, e) =
-              let common, others =
-                TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
-              in
-              let c = others + (abs (common - card)) in
-              if c < i then (c, equality)
-              else (i, e)
-            in
-            let e1 = EqualitySet.min_elt ps in
-            let initial =
-              let common, others = 
-                TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
-              in
-              (others + (abs (common - card))), e1
-            in
-            let _, e = EqualitySet.fold f ps initial in
-            let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
-            ns, EqualitySet.add e ps'
+          if !counter = 0 then counter := !symbols_ratio in
+	let e = EqualitySet.min_elt ps in
+        let ps' = pickw (w-1) (EqualitySet.remove e ps) in
+          EqualitySet.add e ps'
       else
         let e = EqualitySet.min_elt ps in
-        let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
-        ns, EqualitySet.add e ps'        
+        let ps' = pickw (w-1) (EqualitySet.remove e ps) in
+        EqualitySet.add e ps'        
     else
-      EqualitySet.empty, EqualitySet.empty
+      EqualitySet.empty
   in
-  let ns, ps = pickw in_weight ns ps in
+  let ps = pickw in_weight ps in
   let rec picka w s l =
     if w > 0 then
       match l with
@@ -430,7 +288,6 @@ let prune_passive howmany (active, _) passive =
     else
       0, s, l
   in
-  let in_age, ns, nl = picka in_age ns nl in
   let _, ps, pl = picka in_age ps pl in
   if not (EqualitySet.is_empty ps) then
     maximal_retained_equality := Some (EqualitySet.max_elt ps); 
@@ -438,167 +295,77 @@ let prune_passive howmany (active, _) passive =
     EqualitySet.fold
       (fun e tbl -> Indexing.index tbl e) ps Indexing.empty
   in
-  (nl, ns), (pl, ps), tbl  
+  (pl, ps), tbl  
 ;;
 
 
 (** inference of new equalities between current and some in active *)
-let infer env sign current (active_list, active_table) =
+let infer env current ((active_list:Inference.equality list), active_table) =
   let (_,c,_) = env in 
   if Utils.debug_metas then
     (ignore(Indexing.check_target c current "infer1");
-     ignore(List.map (function (_,current) -> Indexing.check_target c current "infer2") active_list)); 
-  let new_neg, new_pos = 
-    match sign with
-    | Negative ->
-        let maxm, res = 
-          Indexing.superposition_left !maxmeta env active_table current in
-          if Utils.debug_metas then
-            ignore(List.map 
-                     (function current -> 
-                        Indexing.check_target c current "sup-1") res);
-        maxmeta := maxm;
-        res, [] 
-    | Positive ->
-        let maxm, res =
-          Indexing.superposition_right !maxmeta env active_table current in
-          if Utils.debug_metas then
-            ignore(List.map 
-                     (function current -> 
-                        Indexing.check_target c current "sup0") res);
-          maxmeta := maxm;
-        let rec infer_positive table = function
-          | [] -> [], []
-          | (Negative, equality)::tl ->
-              let maxm, res =
-                Indexing.superposition_left !maxmeta env table equality in
-              maxmeta := maxm;
-              if Utils.debug_metas then 
-                ignore(List.map 
-                         (function current -> 
-                            Indexing.check_target c current "supl") res);
-              let neg, pos = infer_positive table tl in
-              res @ neg, pos
-          | (Positive, equality)::tl ->
-              let maxm, res =
-                Indexing.superposition_right !maxmeta env table equality in
+     ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list)); 
+  let new_pos = 
+    let maxm, res =
+      Indexing.superposition_right !maxmeta env active_table current in
+      if Utils.debug_metas then
+        ignore(List.map 
+                 (function current -> 
+                    Indexing.check_target c current "sup0") res);
+      maxmeta := maxm;
+      let rec infer_positive table = function
+        | [] -> []
+        | equality::tl ->
+            let maxm, res =
+              Indexing.superposition_right !maxmeta env table equality in
               maxmeta := maxm;
-                if Utils.debug_metas then
-                  ignore
-                    (List.map 
-                       (function current -> 
-                          Indexing.check_target c current "sup2") res);
-              let neg, pos = infer_positive table tl in
-              neg, res @ pos
-        in
-        let maxm, copy_of_current = Inference.fix_metas !maxmeta current in
-        maxmeta := maxm;
-        let curr_table = Indexing.index Indexing.empty current in
-        let neg, pos = 
-          infer_positive curr_table ((sign,copy_of_current)::active_list) 
-        in
-          if Utils.debug_metas then 
-            ignore(List.map 
+              if Utils.debug_metas then
+                ignore
+                  (List.map 
                      (function current -> 
-                        Indexing.check_target c current "sup3") pos);
-        neg, res @ pos
-  in
-  derived_clauses := !derived_clauses + (List.length new_neg) +
-    (List.length new_pos);
-  match !maximal_retained_equality with
-  | None -> 
+                        Indexing.check_target c current "sup2") res);
+              let pos = infer_positive table tl in
+	      res @ pos
+      in
+      let maxm, copy_of_current = Inference.fix_metas !maxmeta current in
+        maxmeta := maxm;
+      let curr_table = Indexing.index Indexing.empty current in
+      let pos = infer_positive curr_table (copy_of_current::active_list) 
+      in 
       if Utils.debug_metas then 
-        (ignore(List.map 
-                 (function current -> 
-                    Indexing.check_target c current "sup4") new_pos);
         ignore(List.map 
                  (function current -> 
-                    Indexing.check_target c current "sup5") new_neg));
-      new_neg, new_pos
-  | Some eq ->
+                    Indexing.check_target c current "sup3") pos);
+	res @ pos
+  in
+  derived_clauses := !derived_clauses + (List.length new_pos);
+  match !maximal_retained_equality with
+    | None -> new_pos
+    | Some eq ->
       ignore(assert false);
       (* if we have a maximal_retained_equality, we can discard all equalities
          "greater" than it, as they will never be reached...  An equality is
          greater than maximal_retained_equality if it is bigger
          wrt. OrderedEquality.compare and it is less similar than
          maximal_retained_equality to the current goal *)
-      let symbols, card =
-        match active_list with
-        | (Negative, e)::_ ->
-            let symbols = symbols_of_equality e in
-            let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
-            Some symbols, card
-        | _ -> None, 0
-      in
-      let new_pos = 
-        match symbols with
-        | None ->
-            List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
-        | Some symbols ->
-            let filterfun e =
-              if OrderedEquality.compare e eq <= 0 then
-                true
-              else
-                let foldfun k v (r1, r2) =
-                  if TermMap.mem k symbols then
-                    let c = TermMap.find k symbols in
-                    let c1 = abs (c - v) in
-                    let c2 = v - c1 in
-                    r1 + c2, r2 + c1
-                  else
-                    r1, r2 + v
-                in
-                let initial =
-                  let common, others =
-                    TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in
-                  others + (abs (common - card))
-                in
-                let common, others =
-                  TermMap.fold foldfun (symbols_of_equality e) (0, 0) in
-                let c = others + (abs (common - card)) in
-                if c < initial then true else false 
-            in
-            List.filter filterfun new_pos
-      in
-        new_neg, new_pos
-;;
-
-
-let contains_empty env (negative, positive) =
-  let metasenv, context, ugraph = env in
-  try
-    let found =
-      List.find
-        (fun (w, proof, (ty, left, right, ordering), m) ->
-           fst (CicReduction.are_convertible context left right ugraph))
-        negative
-    in
-    true, Some found
-  with Not_found ->
-    false, None
+        List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
 ;;
 
+(* buttare via sign *)
 
 (** simplifies current using active and passive *)
-let forward_simplify env (sign, current) ?passive (active_list, active_table) =
+let forward_simplify env (sign,current) ?passive (active_list, active_table) =
   let _, context, _ = env in
-  let pl, passive_table =
+  let passive_table =
     match passive with
-    | None -> [], None
-    | Some ((pn, _), (pp, _), pt) ->
-        let pn = List.map (fun e -> (Negative, e)) pn
-        and pp = List.map (fun e -> (Positive, e)) pp in
-        pn @ pp, Some pt
+    | None -> None
+    | Some ((_, _), pt) -> Some pt
   in
-  let all =  if pl = [] then active_list else active_list @ pl in 
-  
   let demodulate table current = 
     let newmeta, newcurrent =
       Indexing.demodulation_equality !maxmeta env table sign current in
     maxmeta := newmeta;
     if is_identity env newcurrent then
-      if sign = Negative then Some (sign, newcurrent)
-      else (
 (*         debug_print  *)
 (*           (lazy *)
 (*              (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
@@ -610,41 +377,33 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 (*                 (String.concat "\n"  *)
 (*                    (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
         None
-      )
     else
-      Some (sign, newcurrent)
+      Some newcurrent
   in
   let rec demod current =
     if Utils.debug_metas then
       ignore (Indexing.check_target context current "demod0");
     let res = demodulate active_table current in
       if Utils.debug_metas then
-        ignore ((function None -> () | Some (_,x) -> 
+        ignore ((function None -> () | Some x -> 
                    ignore (Indexing.check_target context x "demod1");()) res);
     match res with
     | None -> None
-    | Some (sign, newcurrent) ->
+    | Some newcurrent ->
         match passive_table with
         | None -> res
         | Some passive_table -> 
             match demodulate passive_table newcurrent with
               | None -> None
-              | Some (sign,newnewcurrent) -> 
+              | Some newnewcurrent -> 
                   if newcurrent <> newnewcurrent then 
                     demod newnewcurrent
-                  else Some (sign,newnewcurrent)
+                  else Some newnewcurrent
   in 
   let res = demod current in
   match res with
   | None -> None
-  | Some (Negative, c) ->
-      let ok = not (
-        List.exists
-          (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
-          all)
-      in
-      if ok then res else None
-  | Some (Positive, c) ->
+  | Some c ->
       if Indexing.in_index active_table c then
         None
       else
@@ -676,13 +435,10 @@ let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
 
 
 (** simplifies new using active and passive *)
-let forward_simplify_new env (new_neg, new_pos) ?passive active =
+let forward_simplify_new env new_pos ?passive active =
   if Utils.debug_metas then
     begin
       let m,c,u = env in
-        ignore(List.map 
-                 (fun current -> 
-                    Indexing.check_target c current "forward new neg") new_neg);
         ignore(List.map 
         (fun current -> Indexing.check_target c current "forward new pos") 
       new_pos;)
@@ -690,15 +446,11 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let t1 = Unix.gettimeofday () in
 
   let active_list, active_table = active in
-  let pl, passive_table =
+  let passive_table =
     match passive with
-    | None -> [], None
-    | Some ((pn, _), (pp, _), pt) ->
-        let pn = List.map (fun e -> (Negative, e)) pn
-        and pp = List.map (fun e -> (Positive, e)) pp in
-        pn @ pp, Some pt
+    | None -> None
+    | Some ((_, _), pt) -> Some pt
   in
-  
   let t2 = Unix.gettimeofday () in
   fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
   
@@ -709,19 +461,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
     newtarget
   in
   let t1 = Unix.gettimeofday () in
-
-  let new_neg, new_pos =
-    let new_neg = List.map (demodulate Negative active_table) new_neg
-    and new_pos = List.map (demodulate Positive active_table) new_pos in
-      new_neg,new_pos  
-(* PROVA 
-    match passive_table with
-    | None -> new_neg, new_pos
-    | Some passive_table ->
-        List.map (demodulate Negative passive_table) new_neg,
-        List.map (demodulate Positive passive_table) new_pos *)
+  (* we could also demodulate using passive. Currently we don't *)
+  let new_pos =
+    List.map (demodulate Positive active_table) new_pos 
   in
-
   let t2 = Unix.gettimeofday () in
   fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
 
@@ -756,19 +499,16 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
            not ((Indexing.in_index active_table e) ||
                   (Indexing.in_index passive_table e)))
   in
-  new_neg, List.filter subs (List.filter is_duplicate new_pos)
+  List.filter subs (List.filter is_duplicate new_pos)
 ;;
 
 
 (** simplifies a goal with equalities in active and passive *)  
 let rec simplify_goal env goal ?passive (active_list, active_table) =
-  let pl, passive_table =
+  let passive_table =
     match passive with
-    | None -> [], None
-    | Some ((pn, _), (pp, _), pt) ->
-        let pn = List.map (fun e -> (Negative, e)) pn
-        and pp = List.map (fun e -> (Positive, e)) pp in
-        pn @ pp, Some pt
+    | None -> None
+    | Some ((_, _), pt) -> Some pt
   in
 
   let demodulate table goal = 
@@ -824,52 +564,49 @@ let backward_simplify_active env new_pos new_table min_weight active =
   let active_list, active_table = active in
   let active_list, newa = 
     List.fold_right
-      (fun (s, equality) (res, newn) ->
+      (fun equality (res, newn) ->
          let ew, _, _, _ = equality in
          if ew < min_weight then
-           (s, equality)::res, newn
+           equality::res, newn
          else
-           match forward_simplify env (s, equality) (new_pos, new_table) with
+           match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with
            | None -> res, newn
-           | Some (s, e) ->
+           | Some e ->
                if equality = e then
-                 (s, e)::res, newn
+                 e::res, newn
                else 
-                 res, (s, e)::newn)
+                 res, e::newn)
       active_list ([], [])
   in
   let find eq1 where =
-    List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
+    List.exists (meta_convertibility_eq eq1) where
   in
   let active, newa =
     List.fold_right
-      (fun (s, eq) (res, tbl) ->
-         if List.mem (s, eq) res then
+      (fun eq (res, tbl) ->
+         if List.mem eq res then
            res, tbl
          else if (is_identity env eq) || (find eq res) then (
            res, tbl
          ) 
          else
-           (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
+           eq::res, Indexing.index tbl eq)
       active_list ([], Indexing.empty),
     List.fold_right
-      (fun (s, eq) (n, p) ->
-         if (s <> Negative) && (is_identity env eq) then (
-           (n, p)
-         ) else
-           if s = Negative then eq::n, p
-           else n, eq::p)
-      newa ([], [])
+      (fun eq p ->
+         if (is_identity env eq) then p
+	 else eq::p)
+      newa []
   in
   match newa with
-  | [], [] -> active, None
+  | [] -> active, None
   | _ -> active, Some newa
 ;;
 
 
 (** simplifies passive using new *)
 let backward_simplify_passive env new_pos new_table min_weight passive =
-  let (nl, ns), (pl, ps), passive_table = passive in
+  let (pl, ps), passive_table = passive in
   let f sign equality (resl, ress, newn) =
     let ew, _, _, _ = equality in
     if ew < min_weight then
@@ -877,22 +614,21 @@ let backward_simplify_passive env new_pos new_table min_weight passive =
     else
       match forward_simplify env (sign, equality) (new_pos, new_table) with
       | None -> resl, EqualitySet.remove equality ress, newn
-      | Some (s, e) ->
+      | Some e ->
           if equality = e then
             equality::resl, ress, newn
           else
             let ress = EqualitySet.remove equality ress in
-            resl, ress, e::newn
+              resl, ress, e::newn
   in
-  let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
-  and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
+  let pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
   let passive_table =
     List.fold_left
       (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
   in
-  match newn, newp with
-  | [], [] -> ((nl, ns), (pl, ps), passive_table), None
-  | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
+  match newp with
+  | [] -> ((pl, ps), passive_table), None
+  |  _ -> ((pl, ps), passive_table), Some (newp)
 ;;
 
 
@@ -901,14 +637,14 @@ let backward_simplify env new' ?passive active =
     List.fold_left
       (fun (l, t, w) e ->
          let ew, _, _, _ = e in
-         (Positive, e)::l, Indexing.index t e, min ew w)
-      ([], Indexing.empty, 1000000) (snd new')
+         e::l, Indexing.index t e, min ew w)
+      ([], Indexing.empty, 1000000) new'
   in
   let active, newa =
     backward_simplify_active env new_pos new_table min_weight active in
   match passive with
   | None ->
-      active, (make_passive [] []), newa, None
+      active, (make_passive []), newa, None
   | Some passive ->
      active, passive, newa, None
 (* prova
@@ -923,18 +659,18 @@ let close env new' given =
     List.fold_left
       (fun (l, t, w) e ->
          let ew, _, _, _ = e in
-         (Positive, e)::l, Indexing.index t e, min ew w)
+         e::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) (snd new')
   in
   List.fold_left
-    (fun (n,p) (s,c) ->
-       let neg,pos = infer env s c (new_pos,new_table) in
-         neg@n,pos@p)
-    ([],[]) given 
+    (fun p c ->
+       let pos = infer env c (new_pos,new_table) in
+         pos@p)
+    [] given 
 ;;
 
 let is_commutative_law eq =
-  let w, proof, (eq_ty, left, right, order), metas = snd eq in
+  let w, proof, (eq_ty, left, right, order), metas = eq in
     match left,right with
         Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], 
         Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
@@ -949,10 +685,9 @@ let prova env new' active =
       (lazy
          (Printf.sprintf "symmetric:\n%s\n"
             (String.concat "\n"
-               ((List.map
-                   (fun (s, e) -> (string_of_sign s) ^ " " ^
-                      (string_of_equality ~env e))
-                   (given)))))) in
+               (List.map
+                  (fun e -> string_of_equality ~env e)
+                   given)))) in
     close env new' given
 ;;
 
@@ -1037,10 +772,10 @@ let rec simpl env e others others_simpl =
   let active = others @ others_simpl in
   let tbl =
     List.fold_left
-      (fun t (_, e) -> Indexing.index t e)
+      (fun t e -> Indexing.index t e)
       Indexing.empty active
   in
-  let res = forward_simplify env e (active, tbl) in
+  let res = forward_simplify env (Positive,e) (active, tbl) in
     match others with
       | hd::tl -> (
           match res with
@@ -1064,9 +799,8 @@ let simplify_equalities env equalities =
   match equalities with
     | [] -> []
     | hd::tl ->
-        let others = List.map (fun e -> (Positive, e)) tl in
         let res =
-          List.rev (List.map snd (simpl env (Positive, hd) others []))
+          List.rev (simpl env hd tl [])
         in
           debug_print
             (lazy
@@ -1076,433 +810,6 @@ let simplify_equalities env equalities =
           res
 ;;
 
-(*
-(* applies equality to goal to see if the goal can be closed *)
-let apply_equality_to_goal env equality goal =
-  let module C = Cic in
-  let module HL = HelmLibraryObjects in
-  let module I = Inference in
-  let metasenv, context, ugraph = env in
-  let _, proof, (ty, left, right, _), metas = equality in
-  let eqterm =
-    C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
-  let gproof, gmetas, gterm = goal in
-(*   debug_print *)
-(*     (lazy *)
-(*        (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" *)
-(*           (string_of_equality equality) (CicPp.ppterm gterm))); *)
-  try
-    let subst, metasenv', _ =
-      Inference.unification metas gmetas context eqterm gterm ugraph
-    in
-    let newproof =
-      match proof with
-      | I.BasicProof (subst',t) -> I.BasicProof (subst@subst',t)
-      | I.ProofBlock (s, uri, nt, t, pe, p) ->
-          I.ProofBlock (subst @ s, uri, nt, t, pe, p)
-      | _ -> assert false
-    in
-    let newgproof =
-      let rec repl = function
-        | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp)
-        | I.NoProof -> newproof
-        | I.BasicProof _ -> newproof
-        | I.SubProof (t, i, p) -> 
-            prerr_endline "SUBPROOF!";
-            I.SubProof (t, i, repl p)
-        | _ -> assert false
-      in
-      repl gproof
-    in
-    true, (subst:Inference.substitution), newgproof
-  with CicUnification.UnificationFailure _ ->
-    false, [], I.NoProof
-;;
-
-
-
-let new_meta metasenv =
-  let m = CicMkImplicit.new_meta metasenv [] in
-  incr maxmeta;
-  while !maxmeta <= m do incr maxmeta done;
-  !maxmeta
-;;
-
-
-(* applies a theorem or an equality to goal, returning a list of subgoals or
-   an indication of failure *)
-let apply_to_goal env theorems ?passive active goal =
-  let metasenv, context, ugraph = env in
-  let proof, metas, term = goal in
-  (*   debug_print *)
-  (*     (lazy *)
-  (*        (Printf.sprintf "apply_to_goal with goal: %s" *)
-  (*           (\* (string_of_proof proof)  *\)(CicPp.ppterm term))); *)
-  let status =
-    let irl =
-      CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let proof', newmeta =
-      let rec get_meta = function
-        | SubProof (t, i, p) ->
-            let t', i' = get_meta p in
-            if i' = -1 then t, i else t', i'
-        | ProofGoalBlock (_, p) -> get_meta p
-        | _ -> Cic.Implicit None, -1
-      in
-      let p, m = get_meta proof in
-      if m = -1 then
-        let n = new_meta (metasenv @ metas) in
-        Cic.Meta (n, irl), n
-      else
-        p, m
-    in
-    let metasenv = (newmeta, context, term)::metasenv @ metas in
-    let bit = new_meta metasenv, context, term in 
-    let metasenv' = bit::metasenv in
-    ((None, metasenv', Cic.Meta (newmeta, irl), term), newmeta)
-  in
-  let rec aux = function
-    | [] -> `No
-    | (theorem, thmty, _)::tl ->
-        try
-          let subst, (newproof, newgoals) =
-            PrimitiveTactics.apply_tac_verbose_with_subst ~term:theorem status
-          in
-          if newgoals = [] then
-            let _, _, p, _ = newproof in
-            let newp =
-              let rec repl = function
-                | Inference.ProofGoalBlock (_, gp) ->
-                    Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
-                | Inference.NoProof -> Inference.BasicProof ([],p)
-                | Inference.BasicProof _ -> Inference.BasicProof ([],p)
-                | Inference.SubProof (t, i, p2) ->
-                    Inference.SubProof (t, i, repl p2)
-                | _ -> assert false
-              in
-              repl proof
-            in
-            let _, m = status in
-            let subst = List.filter (fun (i, _) -> i = m) subst in
-            `Ok (subst, [newp, metas, term])
-          else
-            let _, menv, p, _ = newproof in
-            let irl =
-              CicMkImplicit.identity_relocation_list_for_metavariable context
-            in
-            let goals =
-              List.map
-                (fun i ->
-                   let _, _, ty = CicUtil.lookup_meta i menv in
-                   let p' =
-                     let rec gp = function
-                       | SubProof (t, i, p) ->
-                           SubProof (t, i, gp p)
-                       | ProofGoalBlock (sp1, sp2) ->
-                           ProofGoalBlock (sp1, gp sp2)
-                       | BasicProof _
-                       | NoProof ->
-                           SubProof (p, i, BasicProof ([],Cic.Meta (i, irl)))
-                       | ProofSymBlock (s, sp) ->
-                           ProofSymBlock (s, gp sp)
-                       | ProofBlock (s, u, nt, t, pe, sp) ->
-                           prerr_endline "apply_to_goal!";
-                           ProofBlock (s, u, nt, t, pe, gp sp)
-                     in gp proof
-                   in
-                   (p', menv, ty))
-                newgoals
-            in
-            let goals =
-              let weight t =
-                let w, m = weight_of_term t in
-                w + 2 * (List.length m)
-              in
-              List.sort
-                (fun (_, _, t1) (_, _, t2) ->
-                   Pervasives.compare (weight t1) (weight t2))
-                goals
-            in
-            let best = aux tl in
-            match best with
-            | `Ok (_, _) -> best
-            | `No -> `GoOn ([subst, goals])
-            | `GoOn sl -> `GoOn ((subst, goals)::sl)
-        with ProofEngineTypes.Fail msg ->
-          aux tl
-  in
-  let r, s, l =
-    if Inference.term_is_equality term then
-      let rec appleq_a = function
-        | [] -> false, [], []
-        | (Positive, equality)::tl ->
-            let ok, s, newproof = apply_equality_to_goal env equality goal in
-            if ok then true, s, [newproof, metas, term] else appleq_a tl
-        | _::tl -> appleq_a tl
-      in
-      let rec appleq_p = function
-        | [] -> false, [], []
-        | equality::tl ->
-            let ok, s, newproof = apply_equality_to_goal env equality goal in
-            if ok then true, s, [newproof, metas, term] else appleq_p tl
-      in
-      let al, _ = active in
-      match passive with
-      | None -> appleq_a al
-      | Some (_, (pl, _), _) ->
-          let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl
-    else
-      false, [], []
-  in
-  if r = true then `Ok ((s:Cic.substitution),l) else aux theorems
-;;
-
-
-(* sorts a conjunction of goals in order to detect earlier if it is
-   unsatisfiable. Non-predicate goals are placed at the end of the list *)
-let sort_goal_conj (metasenv, context, ugraph) (depth, gl) =
-  let gl = 
-    List.stable_sort
-      (fun (_, e1, g1) (_, e2, g2) ->
-         let ty1, _ =
-           CicTypeChecker.type_of_aux' (e1 @ metasenv) context g1 ugraph 
-         and ty2, _ =
-           CicTypeChecker.type_of_aux' (e2 @ metasenv) context g2 ugraph
-         in
-         let prop1 =
-           let b, _ =
-             CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty1 ugraph
-           in
-           if b then 0 else 1
-         and prop2 =
-           let b, _ =
-             CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty2 ugraph
-           in
-           if b then 0 else 1
-         in
-         if prop1 = 0 && prop2 = 0 then
-           let e1 = if Inference.term_is_equality g1 then 0 else 1
-           and e2 = if Inference.term_is_equality g2 then 0 else 1 in
-           e1 - e2
-         else
-           prop1 - prop2)
-      gl
-  in
-  (depth, gl)
-;;
-
-
-let is_meta_closed goals =
-  List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals
-;;
-
-
-(* applies a series of theorems/equalities to a conjunction of goals *)
-let rec apply_to_goal_conj env theorems ?passive active (depth, goals) =
-  let aux (goal, r) tl =
-    let propagate_subst subst (proof, metas, term) =
-      let rec repl = function
-        | NoProof -> NoProof 
-        | BasicProof (subst',t) ->
-            BasicProof (subst@subst',t)
-        | ProofGoalBlock (p, pb) ->
-            let pb' = repl pb in
-            ProofGoalBlock (p, pb')
-        | SubProof (t, i, p) ->
-            let t' = Inference.apply_subst subst t in
-            let p = repl p in
-            SubProof (t', i, p)
-        | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
-        | ProofBlock (s, u, nty, t, pe, p) ->
-            ProofBlock (subst @ s, u, nty, t, pe, p)
-      in (repl proof, metas, term)
-    in
-    (* let r = apply_to_goal env theorems ?passive active goal in *) (
-      match r with
-      | `No -> `No (depth, goals)
-      | `GoOn sl ->
-          let l =
-            List.map
-              (fun (s, gl) ->
-                 let tl = List.map (propagate_subst s) tl in
-                 sort_goal_conj env (depth+1, gl @ tl)) sl
-          in
-          `GoOn l
-      | `Ok (subst, gl) ->
-          if tl = [] then
-            `Ok (depth, gl)
-          else
-            let p, _, _ = List.hd gl in
-            let subproof =
-              let rec repl = function
-                | SubProof (_, _, p) -> repl p
-                | ProofGoalBlock (p1, p2) ->
-                    ProofGoalBlock (repl p1, repl p2)
-                | p -> p
-              in
-              build_proof_term (repl p)
-            in
-            let i = 
-              let rec get_meta = function
-                | SubProof (_, i, p) ->
-                    let i' = get_meta p in
-                    if i' = -1 then i else i'
-(*                         max i (get_meta p) *)
-                | ProofGoalBlock (_, p) -> get_meta p
-                | _ -> -1
-              in
-              get_meta p
-            in
-            let subst =
-              let _, (context, _, _) = List.hd subst in
-              [i, (context, subproof, Cic.Implicit None)]
-            in
-            let tl = List.map (propagate_subst subst) tl in
-            let conj = sort_goal_conj env (depth(* +1 *), tl) in
-            `GoOn ([conj])
-    )
-  in
-  if depth > !maxdepth || (List.length goals) > !maxwidth then 
-    `No (depth, goals)
-  else
-    let rec search_best res = function
-      | [] -> res
-      | goal::tl ->
-          let r = apply_to_goal env theorems ?passive active goal in
-          match r with
-          | `Ok _ -> (goal, r)
-          | `No -> search_best res tl
-          | `GoOn l ->
-              let newres = 
-                match res with
-                | _, `Ok _ -> assert false
-                | _, `No -> goal, r
-                | _, `GoOn l2 ->
-                    if (List.length l) < (List.length l2) then goal, r else res
-              in
-              search_best newres tl
-    in
-    let hd = List.hd goals in
-    let res = hd, (apply_to_goal env theorems ?passive active hd) in
-    let best =
-      match res with
-      | _, `Ok _ -> res
-      | _, _ -> search_best res (List.tl goals)
-    in
-    let res = aux best (List.filter (fun g -> g != (fst best)) goals) in
-    match res with
-    | `GoOn ([conj]) when is_meta_closed (snd conj) &&
-        (List.length (snd conj)) < (List.length goals)->
-        apply_to_goal_conj env theorems ?passive active conj
-    | _ -> res
-;;
-
-
-(*
-module OrderedGoals = struct
-  type t = int * (Inference.proof * Cic.metasenv * Cic.term) list
-
-  let compare g1 g2 =
-    let d1, l1 = g1
-    and d2, l2 = g2 in
-    let r = d2 - d1 in
-    if r <> 0 then r
-    else let r = (List.length l1) - (List.length l2) in
-    if r <> 0 then r
-    else
-      let res = ref 0 in
-      let _ = 
-        List.exists2
-          (fun (_, _, t1) (_, _, t2) ->
-             let r = Pervasives.compare t1 t2 in
-             if r <> 0 then (
-               res := r;
-               true
-             ) else
-               false) l1 l2
-      in !res
-end
-
-module GoalsSet = Set.Make(OrderedGoals);;
-
-
-exception SearchSpaceOver;;
-*)
-
-
-(*
-let apply_to_goals env is_passive_empty theorems active goals =
-  debug_print (lazy "\n\n\tapply_to_goals\n\n");
-  let add_to set goals =
-    List.fold_left (fun s g -> GoalsSet.add g s) set goals 
-  in
-  let rec aux set = function
-    | [] ->
-        debug_print (lazy "HERE!!!");
-        if is_passive_empty then raise SearchSpaceOver else false, set
-    | goals::tl ->
-        let res = apply_to_goal_conj env theorems active goals in
-        match res with
-        | `Ok newgoals ->
-            let _ =
-              let d, p, t =
-                match newgoals with
-                | (d, (p, _, t)::_) -> d, p, t
-                | _ -> assert false
-              in
-              debug_print
-                (lazy
-                   (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n"
-                      d (string_of_proof p) (CicPp.ppterm t)))
-            in
-            true, GoalsSet.singleton newgoals
-        | `GoOn newgoals ->
-            let set' = add_to set (goals::tl) in
-            let set' = add_to set' newgoals in
-            false, set'
-        | `No newgoals ->
-            aux set tl
-  in
-  let n = List.length goals in
-  let res, goals = aux (add_to GoalsSet.empty goals) goals in
-  let goals = GoalsSet.elements goals in
-  debug_print (lazy "\n\tapply_to_goals end\n");
-  let m = List.length goals in
-  if m = n && is_passive_empty then
-    raise SearchSpaceOver
-  else
-    res, goals
-;;
-*)
-
-
-(* sorts the list of passive goals to minimize the search for a proof (doesn't
-   work that well yet...) *)
-let sort_passive_goals goals =
-  List.stable_sort
-    (fun (d1, l1) (d2, l2) ->
-       let r1 = d2 - d1 
-       and r2 = (List.length l1) - (List.length l2) in
-       let foldfun ht (_, _, t) = 
-         let _ = List.map (fun i -> Hashtbl.replace ht i 1) (metas_of_term t)
-         in ht
-       in
-       let m1 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l1)
-       and m2 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l2)
-       in let r3 = m1 - m2 in
-       if r3 <> 0 then r3
-       else if r2 <> 0 then r2 
-       else r1)
-    (*          let _, _, g1 = List.hd l1 *)
-(*          and _, _, g2 = List.hd l2 in *)
-(*          let e1 = if Inference.term_is_equality g1 then 0 else 1 *)
-(*          and e2 = if Inference.term_is_equality g2 then 0 else 1 *)
-(*          in let r4 = e1 - e2 in *)
-(*          if r4 <> 0 then r3 else r1) *)
-    goals
-;;
-
-
 let print_goals goals = 
   (String.concat "\n"
      (List.map
@@ -1515,241 +822,6 @@ let print_goals goals =
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
 
-
-(* tries to prove the first conjunction in goals with applications of
-   theorems/equalities, returning new sub-goals or an indication of success *)
-let apply_goal_to_theorems dbd env theorems ?passive active goals =
-  let theorems, _ = theorems in
-  let a_goals, p_goals = goals in
-  let goal = List.hd a_goals in
-  let not_in_active gl =
-    not
-      (List.exists
-         (fun (_, gl') ->
-            if (List.length gl) = (List.length gl') then
-              List.for_all2 (fun (_, _, g1) (_, _, g2) -> g1 = g2) gl gl'
-            else
-              false)
-         a_goals)
-  in
-  let aux theorems =
-    let res = apply_to_goal_conj env theorems ?passive active goal in
-    match res with
-    | `Ok newgoals ->
-        true, ([newgoals], [])
-    | `No _ ->
-        false, (a_goals, p_goals)
-    | `GoOn newgoals ->
-        let newgoals =
-          List.filter
-            (fun (d, gl) ->
-               (d <= !maxdepth) && (List.length gl) <= !maxwidth &&
-                 not_in_active gl)
-            newgoals in
-        let p_goals = newgoals @ p_goals in
-        let p_goals = sort_passive_goals p_goals in
-        false, (a_goals, p_goals)
-  in
-  aux theorems
-;;
-
-
-let apply_theorem_to_goals env theorems active goals =
-  let a_goals, p_goals = goals in
-  let theorem = List.hd (fst theorems) in
-  let theorems = [theorem] in
-  let rec aux p = function
-    | [] -> false, ([], p)
-    | goal::tl ->
-        let res = apply_to_goal_conj env theorems active goal in
-        match res with
-        | `Ok newgoals -> true, ([newgoals], [])
-        | `No _ -> aux p tl
-        | `GoOn newgoals -> aux (newgoals @ p) tl
-  in
-  let ok, (a, p) = aux p_goals a_goals in
-  if ok then
-    ok, (a, p)
-  else
-    let p_goals =
-      List.stable_sort
-        (fun (d1, l1) (d2, l2) ->
-           let r = d2 - d1 in
-           if r <> 0 then r
-           else let r = (List.length l1) - (List.length l2) in
-           if r <> 0 then r
-           else
-             let res = ref 0 in
-             let _ = 
-               List.exists2
-                 (fun (_, _, t1) (_, _, t2) ->
-                    let r = Pervasives.compare t1 t2 in
-                    if r <> 0 then (res := r; true) else false) l1 l2
-             in !res)
-        p
-    in
-    ok, (a_goals, p_goals)
-;;
-
-(* given-clause algorithm with lazy reduction strategy *)
-let rec given_clause dbd env goals theorems passive active =
-  let goals = simplify_goals env goals active in
-  let ok, goals = activate_goal goals in
-  (*   let theorems = simplify_theorems env theorems active in *)
-  if ok then
-    let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
-    if ok then
-      let proof =
-        match (fst goals) with
-        | (_, [proof, _, _])::_ -> Some proof
-        | _ -> assert false
-      in
-      ParamodulationSuccess (proof, env)
-    else
-      given_clause_aux dbd env goals theorems passive active
-  else
-(*     let ok', theorems = activate_theorem theorems in *)
-    let ok', theorems = false, theorems in
-    if ok' then
-      let ok, goals = apply_theorem_to_goals env theorems active goals in
-      if ok then
-        let proof =
-          match (fst goals) with
-          | (_, [proof, _, _])::_ -> Some proof
-          | _ -> assert false
-        in
-        ParamodulationSuccess (proof, env)
-      else
-        given_clause_aux dbd env goals theorems passive active
-    else
-      if (passive_is_empty passive) then ParamodulationFailure
-      else given_clause_aux dbd env goals theorems passive active
-
-and given_clause_aux dbd env goals theorems passive active = 
-  let _,context,_ = env in
-  let time1 = Unix.gettimeofday () in
- 
-  let selection_estimate = get_selection_estimate () in
-  let kept = size_of_passive passive in
-  let passive =
-    if !time_limit = 0. || !processed_clauses = 0 then
-      passive
-    else if !elapsed_time > !time_limit then (
-      debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
-                           !time_limit !elapsed_time));
-      make_passive [] []
-    ) else if kept > selection_estimate then (
-      debug_print
-        (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
-                                 "(kept: %d, selection_estimate: %d)\n")
-                 kept selection_estimate));
-      prune_passive selection_estimate active passive
-    ) else
-      passive
-  in
-
-  let time2 = Unix.gettimeofday () in
-  passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
-
-  kept_clauses := (size_of_passive passive) + (size_of_active active);
-  match passive_is_empty passive with
-  | true -> (* ParamodulationFailure *)
-      given_clause dbd env goals theorems passive active
-  | false ->
-      let (sign, current), passive = select env (fst goals) passive active in
-      let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in 
-      prerr_endline ("Selected = " ^ 
-                       (CicPp.pp (Inference.term_of_equality current) names));
-      let time1 = Unix.gettimeofday () in
-      let res = forward_simplify env (sign, current) ~passive active in
-      let time2 = Unix.gettimeofday () in
-      forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
-      match res with
-      | None ->
-          given_clause dbd env goals theorems passive active
-      | Some (sign, current) ->
-          if (sign = Negative) && (is_identity env current) then (
-            debug_print
-              (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
-                       (string_of_equality ~env current)));
-            let _, proof, _, _ = current in
-            ParamodulationSuccess (Some proof, env)
-          ) else (           
-            debug_print
-              (lazy "\n================================================");
-            debug_print (lazy (Printf.sprintf "selected: %s %s"
-                                 (string_of_sign sign)
-                                 (string_of_equality ~env current)));
-
-            let t1 = Unix.gettimeofday () in
-            let new' = infer env sign current active in
-            let t2 = Unix.gettimeofday () in
-            infer_time := !infer_time +. (t2 -. t1);
-            
-            let res, goal' = contains_empty env new' in
-            if res then
-              let proof =
-                match goal' with
-                | Some goal -> let _, proof, _, _ = goal in Some proof
-                | None -> None
-              in
-              ParamodulationSuccess (proof, env)
-            else 
-              let t1 = Unix.gettimeofday () in
-              let new' = forward_simplify_new env new' active in
-              let t2 = Unix.gettimeofday () in
-              let _ =
-                forward_simpl_new_time :=
-                  !forward_simpl_new_time +. (t2 -. t1)
-              in
-              let active =
-                match sign with
-                | Negative -> active
-                | Positive ->
-                    let t1 = Unix.gettimeofday () in
-                    let active, _, newa, _ =
-                      backward_simplify env ([], [current]) active
-                    in
-                    let t2 = Unix.gettimeofday () in
-                    backward_simpl_time :=
-                      !backward_simpl_time +. (t2 -. t1);
-                    match newa with
-                    | None -> active
-                    | Some (n, p) ->
-                        let al, tbl = active in
-                        let nn = List.map (fun e -> Negative, e) n in
-                        let pp, tbl =
-                          List.fold_right
-                            (fun e (l, t) ->
-                               (Positive, e)::l,
-                               Indexing.index tbl e)
-                            p ([], tbl)
-                        in
-                        nn @ al @ pp, tbl
-              in
-              match contains_empty env new' with
-              | false, _ -> 
-                  let active =
-                    let al, tbl = active in
-                    match sign with
-                    | Negative -> (sign, current)::al, tbl
-                    | Positive ->
-                        al @ [(sign, current)], Indexing.index tbl current
-                  in
-                  let passive = add_to_passive passive new' in
-                  given_clause dbd env goals theorems passive active
-              | true, goal ->
-                  let proof =
-                    match goal with
-                    | Some goal ->
-                        let _, proof, _, _ = goal in Some proof
-                    | None -> None
-                  in
-                  ParamodulationSuccess (proof, env)
-          )
-;;
-*)
-
 let check_if_goal_is_subsumed env (proof,menv,ty) table =
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
@@ -1778,11 +850,7 @@ let check_if_goal_is_subsumed env (proof,menv,ty) table =
 let counter = ref 0
 
 (** given-clause algorithm with full reduction strategy *)
-let rec given_clause_fullred dbd env goals theorems passive active =
-(*
-  let table,list = active in
-    assert (check_table list table);
-*)
+let rec given_clause_fullred dbd env goals theorems ~passive active =
   let goals = simplify_goals env goals ~passive active in 
   let _,context,_ = env in
   let ok, goals = activate_goal goals in
@@ -1835,26 +903,6 @@ let rec given_clause_fullred dbd env goals theorems passive active =
     in 
     if ok then
       ( prerr_endline "esco qui";
-        let active = 
-          List.filter test (fst active) in
-        let s = Printf.sprintf "actives:\n%s\n"
-          (String.concat "\n"
-             ((List.map
-                 (fun (s, e) -> (string_of_sign s) ^ " " ^
-                    (string_of_equality ~env e))
-                 active)))
-        in prerr_endline s;
-        let passive = 
-          List.filter 
-            (fun x -> test (1,x))
-            (let x,y,_ = passive in (fst x)@(fst y)) in
-        let p = Printf.sprintf "passives:\n%s\n"
-          (String.concat "\n"
-             ((List.map
-                 (fun e -> 
-                    (string_of_equality ~env e))
-                 passive)))
-        in prerr_endline p;
         (*
         let s = Printf.sprintf "actives:\n%s\n"
           (String.concat "\n"
@@ -1896,7 +944,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
                  " #ACTIVES: " ^ string_of_int (size_of_active active) ^
                  " #PASSIVES: " ^ string_of_int (size_of_passive passive));
   incr counter;
-(*  if !counter mod 10 = 0 then
+(*
+    if !counter mod 10 = 0 then
     begin
       let size = HExtlib.estimate_size (passive,active) in
       let sizep = HExtlib.estimate_size (passive) in
@@ -1938,7 +987,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
     else if !elapsed_time > !time_limit then (
       debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
                            !time_limit !elapsed_time));
-      make_passive [] []
+      make_passive [] 
     ) else if kept > selection_estimate then (
       debug_print
         (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
@@ -1954,13 +1003,12 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
   
   kept_clauses := (size_of_passive passive) + (size_of_active active);
   match passive_is_empty passive with
-  | true -> (* ParamodulationFailure *)
-      given_clause_fullred dbd env goals theorems passive active        
+  | true -> ParamodulationFailure 
+      (* given_clause_fullred dbd env goals theorems passive active  *)     
   | false ->
-      let (sign, current), passive = select env (fst goals) passive active in
+      let current, passive = select env (fst goals) passive in
       prerr_endline 
-        ("Selected = " ^ (string_of_sign sign) ^ " " ^ 
-           string_of_equality ~env current);
+        ("Selected = " ^ string_of_equality ~env current);
 (* ^ 
            (let w,p,(t,l,r,o),m = current in
            " size w: " ^ string_of_int (HExtlib.estimate_size w)^
@@ -1973,66 +1021,34 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
            " size m-c: " ^ string_of_int 
              (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *)
       let time1 = Unix.gettimeofday () in
-      let res = forward_simplify env (sign, current) ~passive active in
+      let res = forward_simplify env (Positive, current) ~passive active in
       let time2 = Unix.gettimeofday () in
       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
       match res with
       | None ->
           (* weight_age_counter := !weight_age_counter + 1; *)
           given_clause_fullred dbd env goals theorems passive active
-      | Some (sign, current) ->
-          if test (sign, current) then
-            (prerr_endline 
-              ("Simplified = " ^ (string_of_sign sign) ^ " " ^ 
-             string_of_equality ~env current);
-             let active = fst active in
-             let s = Printf.sprintf "actives:\n%s\n"
-               (String.concat "\n"
-             ((List.map
-                 (fun (s, e) -> (string_of_sign s) ^ " " ^
-                    (string_of_equality ~env e))
-                 active)))
-             in prerr_endline s;
-               assert false);
-          if (sign = Negative) && (is_identity env current) then (
-            debug_print
-              (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
-                       (string_of_equality ~env current)));
-            let _, proof, _, m = current in 
-            ParamodulationSuccess (Some (proof, m))
-          ) else (
+      | Some current ->
+          debug_print (lazy (Printf.sprintf "selected: %s"
+                               (string_of_equality ~env current)));
+          let t1 = Unix.gettimeofday () in
+          let new' = infer env current active in
+          let _ =
             debug_print
-              (lazy "\n================================================");
-            debug_print (lazy (Printf.sprintf "selected: %s %s"
-                                 (string_of_sign sign)
-                                 (string_of_equality ~env current)));
-
-            let t1 = Unix.gettimeofday () in
-            let new' = infer env sign current active in
-            let _ =
-              match new' with
-              | neg, pos ->
-                  debug_print
-                    (lazy
-                       (Printf.sprintf "new' (senza semplificare):\n%s\n"
-                          (String.concat "\n"
-                             ((List.map
-                                 (fun e -> "Negative " ^
-                                    (string_of_equality ~env e)) neg) @
-                                (List.map
-                                   (fun e -> "Positive " ^
-                                      (string_of_equality ~env e)) pos)))))
-            in
-            let t2 = Unix.gettimeofday () in
+              (lazy
+                 (Printf.sprintf "new' (senza semplificare):\n%s\n"
+                    (String.concat "\n"
+                       (List.map
+                          (fun e -> "Positive " ^
+                             (string_of_equality ~env e)) new'))))
+          in
+          let t2 = Unix.gettimeofday () in
             infer_time := !infer_time +. (t2 -. t1);
             let active =
               if is_identity env current then active
               else
                 let al, tbl = active in
-                match sign with
-                | Negative -> (sign, current)::al, tbl
-                | Positive ->
-                    al @ [(sign, current)], Indexing.index tbl current
+                  al @ [current], Indexing.index tbl current
             in
             let rec simplify new' active passive =
               let t1 = Unix.gettimeofday () in
@@ -2043,27 +1059,22 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
               let t1 = Unix.gettimeofday () in
               let active, passive, newa, retained =
                 backward_simplify env new' ~passive  active in
-              
               let t2 = Unix.gettimeofday () in
                 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
               match newa, retained with
               | None, None -> active, passive, new'
-              | Some (n, p), None
-              | None, Some (n, p) ->
-                  let nn, np = new' in
+              | Some p, None
+              | None, Some p ->
+                  let np = new' in
                     if Utils.debug_metas then
                       begin
                         List.iter 
                           (fun x->Indexing.check_target context x "simplify1")
-                          n;
-                        List.iter 
-                          (fun x->Indexing.check_target context x "simplify2")
-                          p
+                          p;
                       end;
-                    simplify (nn @ n, np @ p) active passive
-              | Some (n, p), Some (rn, rp) ->
-                  let nn, np = new' in
-                  simplify (nn @ n @ rn, np @ p @ rp) active passive
+                    simplify (new' @ p) active passive
+              | Some p, Some rp ->
+                  simplify (new' @ p @ rp) active passive
             in
             let active, _, new' = simplify new' active passive in
 (* pessima prova 
@@ -2094,69 +1105,50 @@ end prova *)
                    (Printf.sprintf "active:\n%s\n"
                       (String.concat "\n"
                          ((List.map
-                             (fun (s, e) -> (string_of_sign s) ^ " " ^
-                                (string_of_equality ~env e))
+                             (fun e -> (string_of_equality ~env e))
                              (fst active))))))
             in
             let _ =
-              match new' with
-              | neg, pos ->
-                  debug_print
-                    (lazy
-                       (Printf.sprintf "new':\n%s\n"
-                          (String.concat "\n"
-                             ((List.map
-                                 (fun e -> "Negative " ^
-                                    (string_of_equality ~env e)) neg) @
-                                (List.map
-                                   (fun e -> "Positive " ^
-                                      (string_of_equality ~env e)) pos)))))
+              debug_print
+                (lazy
+                   (Printf.sprintf "new':\n%s\n"
+                      (String.concat "\n"
+                         ((List.map
+                             (fun e -> "Negative " ^
+                                (string_of_equality ~env e)) new')))))
             in
-            match contains_empty env new' with
-            | false, _ -> 
-                let passive = add_to_passive passive new' in
-                given_clause_fullred dbd env goals theorems passive active
-            | true, goal ->
-                let proof =
-                  match goal with
-                  | Some goal -> let _, proof, _, env = goal in Some (proof,env)
-                  | None -> None
-                in
-                ParamodulationSuccess proof
-          )
-  
+            let passive = add_to_passive passive new' in
+              given_clause_fullred dbd env goals theorems passive active
 ;;
 
+(*
 let profiler0 = HExtlib.profile "P/Saturation.given_clause_fullred"
 
 let given_clause_fullred dbd env goals theorems passive active =
   profiler0.HExtlib.profile 
     (given_clause_fullred dbd env goals theorems passive) active
-  
+*)
+
 
 let rec saturate_equations env goal accept_fun passive active =
   elapsed_time := Unix.gettimeofday () -. !start_time;
   if !elapsed_time > !time_limit then
     (active, passive)
   else
-    let (sign, current), passive = select env [1, [goal]] passive active in
-    let res = forward_simplify env (sign, current) ~passive active in
+    let current, passive = select env [1, [goal]] passive in
+    let res = forward_simplify env (Positive, current) ~passive active in
     match res with
     | None ->
         saturate_equations env goal accept_fun passive active
-    | Some (sign, current) ->
-        assert (sign = Positive);
-        debug_print
-          (lazy "\n================================================");
-        debug_print (lazy (Printf.sprintf "selected: %s %s"
-                             (string_of_sign sign)
+    | Some current ->
+        debug_print (lazy (Printf.sprintf "selected: %s"
                              (string_of_equality ~env current)));
-        let new' = infer env sign current active in
+        let new' = infer env current active in
         let active =
           if is_identity env current then active
           else
             let al, tbl = active in
-            al @ [(sign, current)], Indexing.index tbl current
+            al @ [current], Indexing.index tbl current
         in
         let rec simplify new' active passive =
           let new' = forward_simplify_new env new' ~passive active in
@@ -2164,13 +1156,9 @@ let rec saturate_equations env goal accept_fun passive active =
             backward_simplify env new' ~passive active in
           match newa, retained with
           | None, None -> active, passive, new'
-          | Some (n, p), None
-          | None, Some (n, p) ->
-              let nn, np = new' in
-              simplify (nn @ n, np @ p) active passive
-          | Some (n, p), Some (rn, rp) ->
-              let nn, np = new' in
-              simplify (nn @ n @ rn, np @ p @ rp) active passive
+          | Some p, None
+          | None, Some p -> simplify (new' @ p) active passive
+          | Some p, Some rp -> simplify (new' @ p @ rp) active passive
         in
         let active, passive, new' = simplify new' active passive in
         let _ =
@@ -2178,33 +1166,25 @@ let rec saturate_equations env goal accept_fun passive active =
             (lazy
                (Printf.sprintf "active:\n%s\n"
                   (String.concat "\n"
-                     ((List.map
-                         (fun (s, e) -> (string_of_sign s) ^ " " ^
-                            (string_of_equality ~env e))
-                         (fst active))))))
+                     (List.map
+                         (fun e -> string_of_equality ~env e)
+                         (fst active)))))
         in
-        let _ =
-          match new' with
-          | neg, pos ->
-              debug_print
-                (lazy
-                   (Printf.sprintf "new':\n%s\n"
-                      (String.concat "\n"
-                         ((List.map
-                             (fun e -> "Negative " ^
-                                (string_of_equality ~env e)) neg) @
-                            (List.map
-                               (fun e -> "Positive " ^
-                                  (string_of_equality ~env e)) pos)))))
+	let _ =
+          debug_print
+            (lazy
+               (Printf.sprintf "new':\n%s\n"
+                  (String.concat "\n"
+                     (List.map
+                         (fun e -> "Negative " ^
+                            (string_of_equality ~env e)) new'))))
         in
-        let new' = match new' with _, pos -> [], List.filter accept_fun pos in
+        let new' = List.filter accept_fun new' in
         let passive = add_to_passive passive new' in
         saturate_equations env goal accept_fun passive active
 ;;
   
 
-
-
 let main dbd full term metasenv ugraph =
   let module C = Cic in
   let module T = CicTypeChecker in
@@ -2270,7 +1250,7 @@ let main dbd full term metasenv ugraph =
     let equalities = simplify_equalities env 
       (equalities@library_equalities) in 
     let active = make_active () in
-    let passive = make_passive [] equalities in
+    let passive = make_passive equalities in
     Printf.printf "\ncurrent goal: %s\n"
       (let _, _, g = goal in CicPp.ppterm g);
     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
@@ -2455,7 +1435,7 @@ let saturate
            (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
     in
     let active = make_active () in
-    let passive = make_passive [] equalities in
+    let passive = make_passive equalities in
     let start = Unix.gettimeofday () in
     let res =
       let goals = make_goals goal in
@@ -2466,6 +1446,7 @@ let saturate
   in
   match res with
   | ParamodulationSuccess (Some (proof, proof_menv)) ->
+      prerr_endline "OK, found a proof!";
       debug_print (lazy "OK, found a proof!");
       let proof = Inference.build_proof_term proof in
       let equality_for_replace i t1 =
@@ -2473,6 +1454,7 @@ let saturate
         | C.Meta (n, _) -> n = i
         | _ -> false
       in
+      prerr_endline "replacing metas";
       let proof_menv, what, with_what = 
         let irl = 
           CicMkImplicit.identity_relocation_list_for_metavariable context
@@ -2502,9 +1484,10 @@ let saturate
       let newstatus =
         try
           let ty, ug =
+            prerr_endline "type checking ... ";
             CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
           in
-          debug_print (lazy (CicPp.pp proof [](* names *)));
+          prerr_endline (CicPp.pp proof [](* names *));
           debug_print
             (lazy
                (Printf.sprintf
@@ -2622,12 +1605,12 @@ let retrieve_and_print dbd term metasenv ugraph =
         | hd::tl -> (
             match res with
               | None -> simpl hd tl others_simpl
-              | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
+              | Some e -> simpl hd tl ((u, e)::others_simpl)
           )
         | [] -> (
             match res with
               | None -> others_simpl
-              | Some e -> (u, (snd e))::others_simpl
+              | Some e -> (u, e)::others_simpl
           ) 
   in
   let _equalities =
@@ -2689,7 +1672,7 @@ let main_demod_equalities dbd term metasenv ugraph =
     let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
     let equalities = simplify_equalities env (equalities@library_equalities) in
     let active = make_active () in
-    let passive = make_passive [] equalities in
+    let passive = make_passive equalities in
     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
     Printf.printf "\nequalities:\n%s\n"
@@ -2714,11 +1697,11 @@ let main_demod_equalities dbd term metasenv ugraph =
 
     let passive =
       match rp with
-      | (n, _), (p, _), _ ->
+      | (p, _), _ ->
           EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
     in
     let active =
-      let l = List.map snd (fst ra) in
+      let l = fst ra in
       EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
     in
     Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index 16556588f..db19e87d1 100644
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/components/tactics/paramodulation/utils.ml
@@ -291,7 +291,7 @@ end
 module IntSet = Set.Make(OrderedInt)
 
 let compute_equality_weight (ty,left,right,o) =
-  let factor = 2 in
+  let factor = 1 in
   match o with
     | Lt -> 
 	let w, m = (weight_of_term 
diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 60a485bce..7d55e7589 100644
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 27 15:17:54 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr  5 15:04:24 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
-- 
2.39.2