-TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP513-1.p.ma logic/equality.ma
-TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP543-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP573-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
-TPTP/Veloci/LCL112-2.p.ma logic/equality.ma
-TPTP/Veloci/COL014-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO003-2.p.ma logic/equality.ma
-TPTP/Veloci/COL024-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL135-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
-TPTP/Veloci/COL061-2.p.ma logic/equality.ma
-TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
-TPTP/Veloci/COL084-1.p.ma logic/equality.ma
-TPTP/Veloci/COL063-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP022-2.p.ma logic/equality.ma
-TPTP/Veloci/COL064-9.p.ma logic/equality.ma
-TPTP/Veloci/GRP116-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP603-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG024-6.p.ma logic/equality.ma
-TPTP/Veloci/GRP136-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP146-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP481-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP562-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP176-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
+contradiction.ma coq.ma
+TPTP/Veloci/GRP564-1.p.ma logic/equality.ma
+inversion2.ma coq.ma
+TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
+TPTP/Unsatisfiable/SYN599-1.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_pts.ma
+TPTP/Veloci/GRP597-1.p.ma logic/equality.ma