-TPTP/Veloci/COL010-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP146-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
-TPTP/Veloci/LAT039-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/GRP143-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO004-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP488-1.p.ma logic/equality.ma
-TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP543-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP118-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO003-4.p.ma logic/equality.ma
-TPTP/Veloci/LCL157-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
-TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP606-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP549-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG008-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
-TPTP/Veloci/COL013-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
-TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP565-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL115-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP572-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
+TPTP/Veloci/COL060-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/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
+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