First tests for paramodulation (pretty printer, unification)

[helm.git] / helm / software / matita / tests / depends

diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends
index 0a676a77c77ebda4a986d6d1129427c9dfd60494..ccbafd0cdb51de3a32f94b18e408b0a402543405 100644 (file)
--- a/helm/software/matita/tests/depends
+++ b/helm/software/matita/tests/depends
@@ -1,8 +1,8 @@
 TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
 dependent_guarded_bove_capretta.ma nat/nat.ma
-TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
 interactive/test5.ma 
+TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
 TPTP/Veloci/COL008-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
 record.ma 
@@ -12,8 +12,8 @@ TPTP/Veloci/COL016-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
 TPTP/Veloci/COL024-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP139-1.p.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
@@ -35,8 +35,8 @@ TPTP/Veloci/COL063-3.p.ma logic/equality.ma
 TPTP/Veloci/LCL112-2.p.ma logic/equality.ma
 formal_topology.ma logic/connectives.ma
 TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
-replace.ma coq.ma
 test2.ma coq.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
@@ -59,19 +59,19 @@ 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/Veloci/RNG011-5.p.ma logic/equality.ma
 inversion.ma coq.ma
 TPTP/Veloci/GRP592-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP182-1.p.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
 coercions.ma nat/compare.ma nat/times.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/GRP567-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
 comments.ma coq.ma
 TPTP/Veloci/COL021-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
@@ -96,8 +96,8 @@ ng_pts.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/BOO009-4.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
@@ -134,8 +134,8 @@ TPTP/Veloci/BOO003-4.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
-TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
 fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
 TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
@@ -151,27 +151,28 @@ clearbody.ma coq.ma
 TPTP/Veloci/LCL134-1.p.ma logic/equality.ma
 TPTP/Veloci/COL060-2.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/LAT039-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP509-1.p.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
 paramodulation/BOO075-1.ma 
 TPTP/Veloci/GRP605-1.p.ma logic/equality.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/GRP495-1.p.ma logic/equality.ma
 TPTP/Veloci/COL083-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP495-1.p.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/GRP010-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
 interactive/test_instance.ma 
 TPTP/Veloci/COL012-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-2.p.ma logic/equality.ma
@@ -183,8 +184,8 @@ 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
 TPTP/Veloci/COL064-6.p.ma logic/equality.ma
-apply2.ma nat/nat.ma
 metasenv_ordering.ma coq.ma
+apply2.ma nat/nat.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
@@ -211,8 +212,8 @@ TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
 rewrite.ma coq.ma
-TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
 bad_tests/auto.ma coq.ma
+TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
 diabolic_fix.ma nat/nat.ma
 TPTP/Veloci/GRP001-2.p.ma logic/equality.ma
 test4.ma coq.ma
@@ -221,10 +222,10 @@ 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/GRP137-1.p.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/Veloci/GRP467-1.p.ma logic/equality.ma
@@ -232,7 +233,6 @@ TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-4.p.ma logic/equality.ma
 TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
-lara.ma nat/nat.ma
 TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
 paramodulation.ma coq.ma
 TPTP/Veloci/GRP596-1.p.ma logic/equality.ma
@@ -240,8 +240,8 @@ 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/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
@@ -250,9 +250,9 @@ TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
 compose.ma logic/equality.ma
 TPTP/Veloci/COL025-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
-hard_refine.ma coq.ma
 letrecand.ma nat/nat.ma
 unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
+hard_refine.ma coq.ma
 paramodulation/group.ma coq.ma
 TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
@@ -263,11 +263,11 @@ TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
 mysql_escaping.ma 
 TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP182-2.p.ma logic/equality.ma
-TPTP/Veloci/LDA007-3.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
 TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
@@ -292,8 +292,8 @@ TPTP/Veloci/COL062-2.p.ma logic/equality.ma
 match_inference.ma 
 simpl.ma coq.ma
 unifhint_simple.ma logic/equality.ma
-TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-6.p.ma logic/equality.ma
+TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
 third.ma first.ma second.ma
 TPTP/Veloci/GRP560-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP150-1.p.ma logic/equality.ma
@@ -307,8 +307,8 @@ coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma li
 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
@@ -336,7 +336,7 @@ 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_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