superposition_left not performed if the input goal is an identity

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 81c2a15f1920d2cd7e496643cf912d6042432bc3..e7ef6fa7c2b9def7764a18273fef1981eaf91baa 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1188,6 +1188,15 @@ let given_clause
                   let new' = infer eq_uri env current active in
                   prerr_endline "infer goal";
                   let goals = infer_goal_set_with_current env current goals in
+(*
+      match check_if_goals_set_is_solved env active goals with
+      | Some p -> 
+          prerr_endline 
+            (Printf.sprintf "Found a proof in: %f\n" 
+              (Unix.gettimeofday() -. initial_time));
+          ParamodulationSuccess p
+      | None -> 
+*)
                   let active = 
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
@@ -1555,7 +1564,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
       given_clause 
         eq_uri env goals theorems passive active max_iterations max_time 
     in