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_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/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
-a.ma nat/nat.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/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
-ng_elim.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/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/GRP550-1.p.ma logic/equality.ma
TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
TPTP/Unsatisfiable/LCL166-1.ma logic/equality.ma
-ng_commands.ma ng_pts.ma
+ng_commands.ma nat/nat.ma ng_pts.ma
TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
+paratest.ma nat/plus.ma
TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
paramodulation/BOO075-1.ma
fguidi.ma logic/connectives.ma nat/nat.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
TPTP/Veloci/BOO005-4.p.ma logic/equality.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
TPTP/Veloci/COL064-6.p.ma logic/equality.ma
apply2.ma nat/nat.ma
metasenv_ordering.ma coq.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
decompose.ma logic/connectives.ma
TPTP/Veloci/GRP481-1.p.ma logic/equality.ma
TPTP/Veloci/GRP118-1.p.ma logic/equality.ma
TPTP/Veloci/GRP136-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