X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=e7ef6fa7c2b9def7764a18273fef1981eaf91baa;hb=a0cb7cf4ac234997157aac20a1a68a4a88e805e1;hp=81c2a15f1920d2cd7e496643cf912d6042432bc3;hpb=44f4e888646ac95752bbd8c3e7b9b4b48209b1a6;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 81c2a15f1..e7ef6fa7c 100644
--- 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