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
TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
fold.ma coq.ma
+ng_pts.ma
TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
-a.ma
TPTP/Veloci/GRP457-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/ROB009-1.p.ma logic/equality.ma
TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
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/GRP484-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/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
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
-universe_inconsistency.ma
mysql_escaping.ma
TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
TPTP/Veloci/GRP182-2.p.ma logic/equality.ma
TPTP/Veloci/COL062-2.p.ma logic/equality.ma
match_inference.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
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