fixed proof generation again

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index aab75e9410dc1cf1823381e49fc1ed00428b8505..52918d9af1359017f94b3ffd4b6e6af5f534d528 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -678,7 +678,8 @@ let build_goal_proof l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se
+  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), 
+   se
 ;;
 
 let refl_proof ty term = 

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index da76559e843f6f16ec80be9c78cb671b085aa647..e4dec639749adff715b48e7ce993d7d4ca45296c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -399,7 +399,7 @@ let subsumption_aux use_unification env table target =
           in
           (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok what leftorright tl
-          | Some s -> Some (s, equation, leftorright))
+          | Some s -> Some (s, equation, leftorright <> pos ))
         with 
         | Inference.MatchingFailure 
         | CicUnification.UnificationFailure _ -> ok what leftorright tl

diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index 8fd6187024cbc9bc51ee579215de33480509aaff..a446747e5c53ff3a10c3940103c5173e84dc46a0 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -45,12 +45,12 @@ val unification :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Subst.substitution * Equality.equality * Utils.pos) option
+  (Subst.substitution * Equality.equality * bool) option
 val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Subst.substitution * Equality.equality * Utils.pos) option
+  (Subst.substitution * Equality.equality * bool) option
 val superposition_left :
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
   Index.t ->

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 02b080147aa2c0ccbafaf1529137840c700c566c..b3a53d92953f61e2f86dad7baf146deab69dec79 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -896,14 +896,14 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
       in
 (*      match Indexing.subsumption env table goal_equation with*)
        match Indexing.unification env table goal_equation with 
-        | Some (subst, equality, pos ) ->
+        | Some (subst, equality, swapped ) ->
             prerr_endline 
               ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
             prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
-              if pos = Utils.Left then
+              if swapped then
                 Equality.symmetric eq_ty l id uri m
               else
                 p

diff --git a/helm/software/matita/tests/TPTP/elenco_problemi_veloci_per_test.txt b/helm/software/matita/tests/TPTP/elenco_problemi_veloci_per_test.txt
new file mode 100644 (file)
index 0000000..d8503a4
--- /dev/null
+++ b/helm/software/matita/tests/TPTP/elenco_problemi_veloci_per_test.txt
@@ -0,0 +1,255 @@
+Unsatisfiable/COL007-1.ma 
+Unsatisfiable/COL012-1.ma 
+Unsatisfiable/COL013-1.ma 
+Unsatisfiable/COL058-2.ma 
+Unsatisfiable/COL060-2.ma 
+Unsatisfiable/COL060-3.ma 
+Unsatisfiable/COL061-2.ma 
+Unsatisfiable/COL061-3.ma 
+Unsatisfiable/COL062-2.ma 
+Unsatisfiable/COL062-3.ma 
+Unsatisfiable/COL063-2.ma 
+Unsatisfiable/COL063-3.ma 
+Unsatisfiable/COL063-4.ma 
+Unsatisfiable/COL063-5.ma 
+Unsatisfiable/COL063-6.ma 
+Unsatisfiable/COL064-2.ma 
+Unsatisfiable/COL064-3.ma 
+Unsatisfiable/COL064-4.ma 
+Unsatisfiable/COL064-5.ma 
+Unsatisfiable/COL064-6.ma 
+Unsatisfiable/COL064-7.ma 
+Unsatisfiable/COL064-8.ma 
+Unsatisfiable/COL064-9.ma 
+Unsatisfiable/COL085-1.ma 
+Unsatisfiable/COL086-1.ma 
+Unsatisfiable/GRP023-2.ma 
+Unsatisfiable/GRP136-1.ma 
+Unsatisfiable/GRP137-1.ma 
+Unsatisfiable/GRP160-1.ma 
+Unsatisfiable/GRP161-1.ma 
+Unsatisfiable/GRP454-1.ma 
+Unsatisfiable/GRP457-1.ma 
+Unsatisfiable/GRP460-1.ma 
+Unsatisfiable/GRP463-1.ma 
+Unsatisfiable/GRP541-1.ma 
+Unsatisfiable/GRP545-1.ma 
+Unsatisfiable/GRP549-1.ma 
+Unsatisfiable/LAT033-1.ma 
+Unsatisfiable/LAT034-1.ma 
+Unsatisfiable/ROB030-1.ma 
+Unsatisfiable/SYN083-1.ma 
+Unsatisfiable/BOO006-4.ma 
+Unsatisfiable/BOO011-2.ma 
+Unsatisfiable/BOO011-4.ma 
+Unsatisfiable/COL004-3.ma 
+Unsatisfiable/COL008-1.ma 
+Unsatisfiable/COL016-1.ma 
+Unsatisfiable/COL022-1.ma 
+Unsatisfiable/COL045-1.ma 
+Unsatisfiable/COL048-1.ma 
+Unsatisfiable/COL050-1.ma 
+Unsatisfiable/COL058-3.ma 
+Unsatisfiable/COL083-1.ma 
+Unsatisfiable/COL084-1.ma 
+Unsatisfiable/GRP010-4.ma 
+Unsatisfiable/GRP022-2.ma 
+Unsatisfiable/GRP151-1.ma 
+Unsatisfiable/GRP496-1.ma 
+Unsatisfiable/GRP542-1.ma 
+Unsatisfiable/GRP546-1.ma 
+Unsatisfiable/RNG007-4.ma 
+Unsatisfiable/ROB010-1.ma 
+Unsatisfiable/ROB013-1.ma 
+Unsatisfiable/BOO018-4.ma 
+Unsatisfiable/COL015-1.ma 
+Unsatisfiable/COL017-1.ma 
+Unsatisfiable/COL025-1.ma 
+Unsatisfiable/GRP011-4.ma 
+Unsatisfiable/GRP012-4.ma 
+Unsatisfiable/GRP182-1.ma 
+Unsatisfiable/GRP481-1.ma 
+Unsatisfiable/GRP487-1.ma 
+Unsatisfiable/GRP493-1.ma 
+Unsatisfiable/GRP550-1.ma 
+Unsatisfiable/GRP552-1.ma 
+Unsatisfiable/BOO003-2.ma 
+Unsatisfiable/BOO006-2.ma 
+Unsatisfiable/COL018-1.ma 
+Unsatisfiable/COL024-1.ma 
+Unsatisfiable/GRP001-4.ma 
+Unsatisfiable/GRP115-1.ma 
+Unsatisfiable/GRP117-1.ma 
+Unsatisfiable/GRP182-3.ma 
+Unsatisfiable/GRP455-1.ma 
+Unsatisfiable/GRP458-1.ma 
+Unsatisfiable/GRP490-1.ma 
+Unsatisfiable/GRP494-1.ma 
+Unsatisfiable/GRP544-1.ma 
+Unsatisfiable/GRP573-1.ma 
+Unsatisfiable/GRP581-1.ma 
+Unsatisfiable/LCL132-1.ma 
+Unsatisfiable/ROB002-1.ma 
+Unsatisfiable/GRP001-2.ma 
+Unsatisfiable/GRP142-1.ma 
+Unsatisfiable/GRP144-1.ma 
+Unsatisfiable/GRP189-1.ma 
+Unsatisfiable/GRP206-1.ma 
+Unsatisfiable/GRP562-1.ma 
+Unsatisfiable/GRP566-1.ma 
+Unsatisfiable/GRP569-1.ma 
+Unsatisfiable/GRP570-1.ma 
+Unsatisfiable/LDA001-1.ma 
+Unsatisfiable/GRP173-1.ma 
+Unsatisfiable/GRP182-2.ma 
+Unsatisfiable/GRP188-2.ma 
+Unsatisfiable/GRP484-1.ma 
+Unsatisfiable/GRP491-1.ma 
+Unsatisfiable/GRP548-1.ma 
+Unsatisfiable/GRP558-1.ma 
+Unsatisfiable/GRP565-1.ma 
+Unsatisfiable/LCL133-1.ma 
+Unsatisfiable/LCL134-1.ma 
+Unsatisfiable/LCL135-1.ma 
+Unsatisfiable/BOO004-2.ma 
+Unsatisfiable/BOO009-2.ma 
+Unsatisfiable/GRP150-1.ma 
+Unsatisfiable/GRP153-1.ma 
+Unsatisfiable/GRP174-1.ma 
+Unsatisfiable/GRP182-4.ma 
+Unsatisfiable/GRP189-2.ma 
+Unsatisfiable/BOO010-2.ma 
+Unsatisfiable/BOO010-4.ma 
+Unsatisfiable/GRP118-1.ma 
+Unsatisfiable/GRP143-1.ma 
+Unsatisfiable/GRP145-1.ma 
+Unsatisfiable/GRP152-1.ma 
+Unsatisfiable/GRP188-1.ma 
+Unsatisfiable/GRP485-1.ma 
+Unsatisfiable/GRP510-1.ma 
+Unsatisfiable/GRP577-1.ma 
+Unsatisfiable/LCL161-1.ma 
+Unsatisfiable/GRP518-1.ma 
+Unsatisfiable/GRP520-1.ma 
+Unsatisfiable/BOO003-4.ma 
+Unsatisfiable/BOO004-4.ma 
+Unsatisfiable/GRP514-1.ma 
+Unsatisfiable/GRP516-1.ma 
+Unsatisfiable/GRP574-1.ma 
+Unsatisfiable/GRP586-1.ma 
+Unsatisfiable/LDA007-3.ma 
+Unsatisfiable/BOO005-4.ma 
+Unsatisfiable/COL014-1.ma 
+Unsatisfiable/GRP139-1.ma 
+Unsatisfiable/GRP141-1.ma 
+Unsatisfiable/BOO005-2.ma 
+Unsatisfiable/GRP497-1.ma 
+Unsatisfiable/GRP512-1.ma 
+Unsatisfiable/GRP561-1.ma 
+Unsatisfiable/GRP564-1.ma 
+Unsatisfiable/GRP582-1.ma 
+Unsatisfiable/LCL164-1.ma 
+Unsatisfiable/GRP590-1.ma 
+Unsatisfiable/GRP595-1.ma 
+Unsatisfiable/GRP146-1.ma 
+Unsatisfiable/GRP149-1.ma 
+Unsatisfiable/GRP162-1.ma 
+Unsatisfiable/GRP576-1.ma 
+Unsatisfiable/RNG024-6.ma 
+Unsatisfiable/GRP157-1.ma 
+Unsatisfiable/GRP163-1.ma 
+Unsatisfiable/GRP456-1.ma 
+Unsatisfiable/RNG008-4.ma 
+Unsatisfiable/RNG023-6.ma 
+Unsatisfiable/GRP459-1.ma 
+Unsatisfiable/GRP578-1.ma 
+Unsatisfiable/BOO017-2.ma 
+Unsatisfiable/GRP159-1.ma 
+Unsatisfiable/GRP186-3.ma 
+Unsatisfiable/GRP192-1.ma 
+Unsatisfiable/GRP560-1.ma 
+Unsatisfiable/GRP598-1.ma 
+Unsatisfiable/GRP543-1.ma 
+Unsatisfiable/BOO016-2.ma 
+Unsatisfiable/GRP158-1.ma 
+Unsatisfiable/GRP186-4.ma 
+Unsatisfiable/GRP572-1.ma 
+Unsatisfiable/GRP592-1.ma 
+Unsatisfiable/RNG011-5.ma 
+Unsatisfiable/GRP495-1.ma 
+Unsatisfiable/GRP596-1.ma 
+Unsatisfiable/GRP614-1.ma 
+Unsatisfiable/LCL156-1.ma 
+Unsatisfiable/LCL110-2.ma 
+Unsatisfiable/LCL154-1.ma 
+Unsatisfiable/LCL157-1.ma 
+Unsatisfiable/GRP154-1.ma 
+Unsatisfiable/GRP616-1.ma 
+Unsatisfiable/LCL112-2.ma 
+Unsatisfiable/LCL140-1.ma 
+Unsatisfiable/GRP168-1.ma 
+Unsatisfiable/GRP612-1.ma 
+Unsatisfiable/LCL113-2.ma 
+Unsatisfiable/BOO009-4.ma 
+Unsatisfiable/GRP116-1.ma 
+Unsatisfiable/LCL155-1.ma 
+Unsatisfiable/RNG023-7.ma 
+Unsatisfiable/RNG024-7.ma 
+Unsatisfiable/GRP600-1.ma 
+Unsatisfiable/LCL153-1.ma 
+Unsatisfiable/LCL158-1.ma 
+Unsatisfiable/GRP498-1.ma 
+Unsatisfiable/COL021-1.ma 
+Unsatisfiable/GRP155-1.ma 
+Unsatisfiable/GRP176-2.ma 
+Unsatisfiable/LCL139-1.ma 
+Unsatisfiable/GRP486-1.ma 
+Unsatisfiable/GRP606-1.ma 
+Unsatisfiable/LCL114-2.ma 
+Unsatisfiable/BOO013-2.ma 
+Unsatisfiable/GRP156-1.ma 
+Unsatisfiable/GRP176-1.ma 
+Unsatisfiable/LAT045-1.ma 
+Unsatisfiable/GRP168-2.ma 
+Unsatisfiable/GRP608-1.ma 
+Unsatisfiable/GRP551-1.ma 
+Unsatisfiable/GRP588-1.ma 
+Unsatisfiable/LAT039-1.ma 
+Unsatisfiable/LAT039-2.ma 
+Unsatisfiable/GRP584-1.ma 
+Unsatisfiable/BOO012-2.ma 
+Unsatisfiable/GRP568-1.ma 
+Unsatisfiable/GRP492-1.ma 
+Unsatisfiable/GRP602-1.ma 
+Unsatisfiable/GRP603-1.ma 
+Unsatisfiable/GRP467-1.ma 
+Unsatisfiable/GRP613-1.ma 
+Unsatisfiable/GRP547-1.ma 
+Unsatisfiable/BOO012-4.ma 
+Unsatisfiable/GRP580-1.ma 
+Unsatisfiable/GRP597-1.ma 
+Unsatisfiable/GRP517-1.ma 
+Unsatisfiable/BOO075-1.ma 
+Unsatisfiable/LCL115-2.ma 
+Unsatisfiable/LCL141-1.ma 
+Unsatisfiable/GRP605-1.ma 
+Unsatisfiable/GRP515-1.ma 
+Unsatisfiable/GRP509-1.ma 
+Unsatisfiable/GRP604-1.ma 
+Unsatisfiable/GRP513-1.ma 
+Unsatisfiable/GRP556-1.ma 
+Unsatisfiable/BOO013-4.ma 
+Unsatisfiable/GRP615-1.ma 
+Unsatisfiable/BOO001-1.ma 
+Unsatisfiable/GRP488-1.ma 
+Unsatisfiable/GRP583-1.ma 
+Unsatisfiable/GRP511-1.ma 
+Unsatisfiable/LAT008-1.ma 
+Unsatisfiable/BOO069-1.ma 
+Unsatisfiable/ROB009-1.ma 
+Unsatisfiable/BOO071-1.ma 
+Unsatisfiable/GRP567-1.ma 
+Unsatisfiable/BOO034-1.ma 
+Unsatisfiable/LAT040-1.ma 
+Unsatisfiable/GRP599-1.ma 
+Unsatisfiable/COL010-1.ma