-TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP595-1.p.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/Veloci/LCL112-2.p.ma logic/equality.ma
formal_topology.ma logic/connectives.ma
TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
-test2.ma coq.ma
replace.ma coq.ma
+test2.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/Veloci/BOO001-1.p.ma logic/equality.ma
TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
TPTP/Veloci/GRP600-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
TPTP/Veloci/COL063-5.p.ma logic/equality.ma
+TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
continuationals.ma coq.ma
TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
TPTP/Veloci/BOO034-1.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/GRP168-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
TPTP/Veloci/GRP143-1.p.ma logic/equality.ma
TPTP/Veloci/GRP586-1.p.ma logic/equality.ma
TPTP/Veloci/GRP561-1.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
-TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP189-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/COL064-4.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/COL018-1.p.ma logic/equality.ma
TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
+TPTP/Veloci/COL018-1.p.ma logic/equality.ma
tinycals.ma logic/connectives.ma
coercions_contravariant.ma logic/equality.ma nat/nat.ma
interactive/automatic_insertion.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/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/GRP542-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
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/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
+TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
+TPTP/Veloci/COL083-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
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
first.ma
+ng_coercions.ma
TPTP/Veloci/COL045-1.p.ma logic/equality.ma
TPTP/Veloci/BOO005-4.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
+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
metasenv_ordering.ma coq.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/Veloci/LCL161-1.p.ma logic/equality.ma
TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
decompose.ma logic/connectives.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/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
rewrite.ma coq.ma
bad_tests/auto.ma coq.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/GRP137-1.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
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/COL063-4.p.ma logic/equality.ma
TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
paramodulation.ma coq.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/BOO010-4.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/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
compose.ma logic/equality.ma
TPTP/Veloci/COL025-1.p.ma logic/equality.ma
TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
-letrecand.ma nat/nat.ma
unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
hard_refine.ma coq.ma
+letrecand.ma nat/nat.ma
paramodulation/group.ma coq.ma
TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
TPTP/Veloci/LCL133-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
+TPTP/Veloci/GRP486-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
second.ma first.ma
TPTP/Veloci/COL062-2.p.ma logic/equality.ma
match_inference.ma
-simpl.ma coq.ma
unifhint_simple.ma logic/equality.ma
+ng_includeB.ma ng_include.ma
+simpl.ma coq.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