...

diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends
index a718b23965d78a9fe7b7fa90ffbc6065976ae5a0..a54510177cd2e5728a54c26150d52626588c35b8 100644 (file)
--- a/helm/software/matita/tests/depends
+++ b/helm/software/matita/tests/depends
@@ -1,24 +1,20 @@
 TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA011-2.ma logic/equality.ma
 dependent_guarded_bove_capretta.ma nat/nat.ma
 interactive/test5.ma 
 TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SWV014-1.ma logic/equality.ma
 TPTP/Veloci/COL008-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL063-1.ma logic/equality.ma
-TPTP/Unsatisfiable/NUM017-1.ma logic/equality.ma
 TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
 record.ma 
-TPTP/Veloci/GRP516-1.p.ma logic/equality.ma
 TPTP/Veloci/COL060-3.p.ma logic/equality.ma
+TPTP/Veloci/GRP516-1.p.ma logic/equality.ma
 TPTP/Veloci/COL016-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
+reduction_old_preamble.ma 
 TPTP/Veloci/COL024-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL167-1.ma logic/equality.ma
-TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO006-2.p.ma logic/equality.ma
+TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL157-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL132-1.p.ma logic/equality.ma
 constructor.ma coq.ma
@@ -27,131 +23,103 @@ elim.ma coq.ma
 TPTP/Veloci/GRP155-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO004-4.p.ma logic/equality.ma
 TPTP/Veloci/LCL140-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP573-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP598-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL393-1.ma logic/equality.ma
+TPTP/Veloci/GRP573-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP188-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP485-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP460-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP163-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP485-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP188-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL253-1.ma logic/equality.ma
 TPTP/Veloci/BOO012-4.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL375-1.ma logic/equality.ma
 TPTP/Veloci/GRP581-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP493-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-3.p.ma logic/equality.ma
 TPTP/Veloci/LCL112-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP493-1.p.ma logic/equality.ma
 formal_topology.ma logic/connectives.ma
+esempio_oliboni.ma logic/equality.ma nat/nat.ma
 TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
-replace.ma coq.ma
 test2.ma coq.ma
-TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
+replace.ma coq.ma
 TPTP/Veloci/COL064-7.p.ma logic/equality.ma
+TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP510-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL037-1.ma logic/equality.ma
 TPTP/Veloci/COL010-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN615-1.ma logic/equality.ma
 TPTP/Veloci/COL061-2.p.ma logic/equality.ma
-TPTP/Veloci/LCL135-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO017-2.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN600-1.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL019-1.ma logic/equality.ma
+TPTP/Veloci/LCL135-1.p.ma logic/equality.ma
 elim_pattern.ma nat/plus.ma
 assumption.ma coq.ma
-TPTP/Veloci/GRP551-1.p.ma logic/equality.ma
 interactive/grafite.ma 
+TPTP/Veloci/GRP551-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP141-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP463-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL001-1.ma logic/equality.ma
 fix_betareduction.ma coq.ma
-TPTP/Unsatisfiable/SYN704-1.ma logic/equality.ma
 TPTP/Veloci/GRP606-1.p.ma logic/equality.ma
 coercions_dependent.ma decidable_kit/list_aux.ma list/list.ma nat/nat.ma
 TPTP/Veloci/GRP518-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP584-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA016-1.ma logic/equality.ma
-TPTP/Veloci/COL084-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP174-1.p.ma logic/equality.ma
 paramodulation/boolean_algebra.ma coq.ma
 TPTP/Veloci/GRP496-1.p.ma logic/equality.ma
+TPTP/Veloci/COL084-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP174-1.p.ma logic/equality.ma
 TPTP/Veloci/RNG011-5.p.ma logic/equality.ma
 TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA001-1.ma logic/equality.ma
 inversion.ma coq.ma
 TPTP/Veloci/GRP592-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL105-1.ma logic/equality.ma
 bad_tests/baseuri.ma 
 TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP116-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL230-1.ma logic/equality.ma
 coercions.ma nat/compare.ma nat/times.ma
-TPTP/Unsatisfiable/LCL227-1.ma logic/equality.ma
 TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
 TPTP/Veloci/COL013-1.p.ma logic/equality.ma
-TPTP/Veloci/COL064-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
+TPTP/Veloci/COL064-2.p.ma logic/equality.ma
 comments.ma coq.ma
-TPTP/Unsatisfiable/LCL032-1.ma logic/equality.ma
-TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
 TPTP/Veloci/COL021-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
 TPTP/Veloci/BOO003-2.p.ma logic/equality.ma
 TPTP/Veloci/RNG024-6.p.ma logic/equality.ma
 bool.ma coq.ma
 ng_tactics.ma logic/connectives.ma nat/plus.ma ng_pts.ma
 TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
 TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
+ng_auto.ma 
 TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL423-1.ma logic/equality.ma
 letrec.ma 
-TPTP/Unsatisfiable/LCL395-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA011-1.ma logic/equality.ma
-TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO001-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA008-1.ma logic/equality.ma
+TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP600-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL377-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA005-2.ma logic/equality.ma
 TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-5.p.ma logic/equality.ma
 continuationals.ma coq.ma
 TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN653-1.ma logic/equality.ma
 TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/ANA003-2.ma logic/equality.ma
 ng_pts.ma 
 fold.ma coq.ma
-TPTP/Unsatisfiable/LCL084-3.ma logic/equality.ma
-TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP457-1.p.ma logic/equality.ma
-TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-9.p.ma logic/equality.ma
 TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
+TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP578-1.p.ma logic/equality.ma
 change.ma coq.ma
-TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP143-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP168-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN617-1.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL024-1.ma logic/equality.ma
-TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP586-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
+reduction_old.ma reduction_old_preamble.ma
 TPTP/Veloci/GRP498-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP176-1.p.ma logic/equality.ma
 overred.ma logic/equality.ma
 TPTP/Veloci/COL007-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA021-1.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN556-1.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL125-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA018-1.ma logic/equality.ma
-TPTP/Veloci/GRP603-1.p.ma logic/equality.ma
+reduction_new.ma reduction_new_preamble.ma
 TPTP/Veloci/COL058-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP603-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP515-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG007-4.p.ma logic/equality.ma
 TPTP/Veloci/COL015-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL085-1.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL369-1.ma logic/equality.ma
+TPTP/Veloci/RNG007-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
 TPTP/Veloci/COL048-1.p.ma logic/equality.ma
@@ -159,16 +127,15 @@ TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
 TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP556-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP146-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL156-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-4.p.ma logic/equality.ma
+TPTP/Veloci/LCL156-1.p.ma logic/equality.ma
 contradiction.ma coq.ma
 TPTP/Veloci/GRP564-1.p.ma logic/equality.ma
 inversion2.ma coq.ma
 TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN599-1.ma logic/equality.ma
-TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
-TPTP/Veloci/ROB009-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO003-4.p.ma logic/equality.ma
+TPTP/Veloci/ROB009-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
 ng_elim.ma ng_pts.ma
 TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
@@ -177,32 +144,27 @@ TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
 fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
 subsumption.ma logic/equality.ma
 TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL425-1.ma logic/equality.ma
 TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
 TPTP/Veloci/COL062-3.p.ma logic/equality.ma
 TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
 cut.ma coq.ma
 TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
 TPTP/Veloci/COL018-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA013-1.ma logic/equality.ma
 coercions_contravariant.ma logic/equality.ma nat/nat.ma
 tinycals.ma logic/connectives.ma
 interactive/automatic_insertion.ma 
 clearbody.ma coq.ma
-TPTP/Unsatisfiable/SYN655-1.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL062-1.ma logic/equality.ma
-TPTP/Veloci/BOO016-2.p.ma logic/equality.ma
-TPTP/Veloci/LCL134-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN640-1.ma logic/equality.ma
+ng_copy2.ma ng_copy.ma
 TPTP/Veloci/COL060-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL134-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO016-2.p.ma logic/equality.ma
 TPTP/Veloci/LAT039-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL166-1.ma logic/equality.ma
+TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
 ng_commands.ma nat/nat.ma ng_pts.ma
 TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
 paratest.ma nat/plus.ma
@@ -211,73 +173,58 @@ paramodulation/BOO075-1.ma
 fguidi.ma logic/connectives.ma nat/nat.ma
 TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
 TPTP/Veloci/COL083-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN711-1.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL005-1.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN708-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA023-1.ma logic/equality.ma
+TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
 coercions_propagation.ma logic/connectives.ma nat/orders.ma
 TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL249-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA005-1.ma logic/equality.ma
 interactive/test_instance.ma 
 TPTP/Veloci/COL012-1.p.ma logic/equality.ma
 ng_lexiconn.ma ng_pts.ma
 TPTP/Veloci/COL063-2.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL084-2.ma logic/equality.ma
 first.ma 
-ng_coercions.ma 
-TPTP/Veloci/COL045-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN647-1.ma logic/equality.ma
+ng_coercions.ma ng_pts.ma
 TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
+TPTP/Veloci/COL045-1.p.ma logic/equality.ma
 interactive/test7.ma 
 bad_induction.ma logic/equality.ma nat/nat.ma
 TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
-color.ma logic/equality.ma nat/nat.ma
 ng_include.ma nat/plus.ma ng_pts.ma
+color.ma logic/equality.ma nat/nat.ma
 TPTP/Veloci/COL064-6.p.ma logic/equality.ma
 apply2.ma nat/nat.ma
 metasenv_ordering.ma coq.ma
+TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
-TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN614-1.ma logic/equality.ma
 pullback.ma logic/equality.ma
 TPTP/Veloci/COL086-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL021-1.ma logic/equality.ma
+reduction_new_preamble.ma 
 TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
-ng_lexicon.ma 
+TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
 decompose.ma logic/connectives.ma
 TPTP/Veloci/GRP481-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP118-1.p.ma logic/equality.ma
 generalize.ma coq.ma
 TPTP/Veloci/GRP511-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP192-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL122-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA015-1.ma logic/equality.ma
 TPTP/Veloci/GRP569-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP544-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL119-1.ma logic/equality.ma
 dependent_type_inference.ma nat/nat.ma
 TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
 TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA009-2.ma logic/equality.ma
-TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN639-1.ma logic/equality.ma
 rewrite.ma coq.ma
-bad_tests/auto.ma coq.ma
 TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
+bad_tests/auto.ma coq.ma
 diabolic_fix.ma nat/nat.ma
 TPTP/Veloci/GRP001-2.p.ma logic/equality.ma
 test4.ma coq.ma
@@ -286,64 +233,51 @@ TPTP/Veloci/GRP602-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
-TPTP/Veloci/COL004-3.p.ma logic/equality.ma
-TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO069-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL394-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA010-1.ma logic/equality.ma
+TPTP/Veloci/COL004-3.p.ma logic/equality.ma
 TPTP/Veloci/GRP188-2.p.ma logic/equality.ma
 apply.ma coq.ma
-TPTP/Unsatisfiable/PLA007-1.ma logic/equality.ma
 TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-4.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA004-2.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL074-1.ma logic/equality.ma
 TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN649-1.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL218-1.ma logic/equality.ma
 paramodulation.ma coq.ma
 TPTP/Veloci/GRP596-1.p.ma logic/equality.ma
 coercions_nonuniform.ma 
 TPTP/Veloci/GRP161-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-8.p.ma logic/equality.ma
 TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
-TPTP/Veloci/COL050-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL038-1.ma logic/equality.ma
+TPTP/Veloci/COL050-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
 TPTP/Veloci/COL061-3.p.ma logic/equality.ma
 TPTP/Veloci/COL017-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
 compose.ma logic/equality.ma
-TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
 TPTP/Veloci/COL025-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL002-1.ma logic/equality.ma
+TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
 unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
 letrecand.ma nat/nat.ma
 hard_refine.ma coq.ma
 paramodulation/group.ma coq.ma
-TPTP/Unsatisfiable/LCL124-1.ma logic/equality.ma
 TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP541-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP566-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA014-2.ma logic/equality.ma
+TPTP/Veloci/GRP541-1.p.ma logic/equality.ma
 decl.ma nat/orders.ma nat/times.ma
 TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
 mysql_escaping.ma 
 TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL231-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PUZ040-1.ma logic/equality.ma
 TPTP/Veloci/GRP182-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP599-1.p.ma logic/equality.ma
 interactive/drop.ma 
 interactive/test6.ma 
+TPTP/Veloci/GRP599-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
 TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
 unfold.ma coq.ma
 TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
@@ -351,91 +285,77 @@ TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO013-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP494-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-3.p.ma logic/equality.ma
 TPTP/Veloci/LCL113-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP494-1.p.ma logic/equality.ma
 TPTP/Veloci/RNG008-4.p.ma logic/equality.ma
 demodulation_matita.ma nat/minus.ma
 TPTP/Veloci/ROB002-1.p.ma logic/equality.ma
 tacticals.ma 
-TPTP/Veloci/GRP590-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP549-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP001-4.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN598-1.ma logic/equality.ma
+TPTP/Veloci/GRP590-1.p.ma logic/equality.ma
 applys.ma nat/div_and_mod.ma nat/factorial.ma nat/primes.ma
 TPTP/Veloci/RNG024-7.p.ma logic/equality.ma
-TPTP/Unsatisfiable/RNG004-3.ma logic/equality.ma
 injection.ma coq.ma
 second.ma first.ma
 TPTP/Veloci/COL062-2.p.ma logic/equality.ma
 match_inference.ma 
-TPTP/Unsatisfiable/PLA012-1.ma logic/equality.ma
+ng_includeB.ma ng_include.ma
 unifhint_simple.ma logic/equality.ma
 simpl.ma coq.ma
-TPTP/Unsatisfiable/PLA009-1.ma logic/equality.ma
-TPTP/Unsatisfiable/PUZ050-1.ma logic/equality.ma
-TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-6.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN654-1.ma logic/equality.ma
+TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
 third.ma first.ma second.ma
-TPTP/Unsatisfiable/LCL061-1.ma logic/equality.ma
 TPTP/Veloci/GRP560-1.p.ma logic/equality.ma
-TPTP/Veloci/COL085-1.p.ma logic/equality.ma
+ng_coercion_and_hints.ma ng_pts.ma
 TPTP/Veloci/GRP150-1.p.ma logic/equality.ma
+TPTP/Veloci/COL085-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP615-1.p.ma logic/equality.ma
 TPTP/Veloci/LAT039-1.p.ma logic/equality.ma
 luo.ma Z/times.ma logic/equality.ma
 TPTP/Veloci/GRP022-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP186-3.p.ma logic/equality.ma
 coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma list/sort.ma nat/compare.ma nat/orders.ma
+ng_copy.ma 
 TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
 multiple_inheritance.ma logic/equality.ma
 test3.ma coq.ma
-TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
 TPTP/Veloci/ROB013-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
 naiveparamod.ma logic/equality.ma
 TPTP/Veloci/GRP176-2.p.ma logic/equality.ma
 TPTP/Veloci/COL014-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP543-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP568-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP158-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP543-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP455-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP158-1.p.ma logic/equality.ma
 TPTP/Veloci/COL022-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP576-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO004-2.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN707-1.ma logic/equality.ma
+TPTP/Veloci/GRP576-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP488-1.p.ma logic/equality.ma
 TPTP/Veloci/COL058-3.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA019-1.ma logic/equality.ma
 dependent_injection.ma coq.ma
 TPTP/Veloci/BOO012-2.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA004-1.ma logic/equality.ma
 TPTP/Veloci/LCL115-2.p.ma logic/equality.ma
 absurd.ma coq.ma
-TPTP/Unsatisfiable/PUZ042-1.ma logic/equality.ma
 TPTP/Veloci/GRP182-4.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PUZ039-1.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN646-1.ma logic/equality.ma
 destruct.ma datatypes/constructors.ma logic/equality.ma nat/nat.ma
-TPTP/Unsatisfiable/SYN631-1.ma logic/equality.ma
-TPTP/Veloci/GRP513-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-5.p.ma logic/equality.ma
-TPTP/Unsatisfiable/SYN628-1.ma logic/equality.ma
+TPTP/Veloci/GRP513-1.p.ma logic/equality.ma
 TPTP/Veloci/LAT033-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP546-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/LCL020-1.ma logic/equality.ma
-TPTP/Veloci/GRP458-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP136-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP458-1.p.ma logic/equality.ma
 coercions_open.ma logic/equality.ma nat/nat.ma
 paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
 ng_uris_and_notation.ma nat/nat.ma ng_pts.ma
 TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
 TPTP/Veloci/LAT008-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
 demodulation_coq.ma coq.ma
 TPTP/Veloci/GRP562-1.p.ma logic/equality.ma
-TPTP/Unsatisfiable/PLA014-1.ma logic/equality.ma
 TPTP/Veloci/GRP152-1.p.ma logic/equality.ma
 Z/times.ma 
 coq.ma 

diff --git a/helm/software/matita/tests/ng_auto.ma b/helm/software/matita/tests/ng_auto.ma
new file mode 100644 (file)
index 0000000..b2a4206
--- /dev/null
+++ b/helm/software/matita/tests/ng_auto.ma
@@ -0,0 +1,45 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+
+naxiom T : Type[0].
+naxiom P : T → T → CProp[0].
+naxiom Q : T → CProp[0].
+naxiom f : T → T → T.
+
+naxiom f_com : ∀x,y. P (f x y) (f y x).
+naxiom f_Q : ∀x,y. P x y → Q (f x y).
+
+nlemma foo : ∀x,y. Q x → Q (f (f x y) (f y x)).
+#x; #y; #H; 
+ncut (Q x);
+##[##2: #_; nauto;
+##| nassumption;
+##]
+nqed.
+
+naxiom And : CProp[0] → CProp[0] → CProp[0].
+naxiom And_intro : ∀A,B.A → B → And A B.
+
+naxiom zero : T.
+naxiom succ : T → T.
+naxiom is_nat : T → CProp[0].
+naxiom is_nat_0 : is_nat zero.
+naxiom is_nat_S : ∀x.is_nat x → is_nat (succ x).
+
+nlemma bar : ∀P:T → CProp[0].P (succ zero) → (λx.And (is_nat x) (P x)) ?.
+##[ #P; #H; nwhd; ##] nauto.  
+nqed.  
\ No newline at end of file