Added script useful for running benchmarks

diff --git a/helm/software/matita/contribs/ng_TPTP/Veloci b/helm/software/matita/contribs/ng_TPTP/Veloci
new file mode 100644 (file)
index 0000000..798c787
--- /dev/null
+++ b/helm/software/matita/contribs/ng_TPTP/Veloci
@@ -0,0 +1,256 @@
+BOO001-1.ma
+BOO003-2.ma
+BOO003-4.ma
+BOO004-2.ma
+BOO004-4.ma
+BOO005-2.ma
+BOO005-4.ma
+BOO006-2.ma
+BOO006-4.ma
+BOO009-2.ma
+BOO009-4.ma
+BOO010-2.ma
+BOO010-4.ma
+BOO010-4.ma
+BOO011-2.ma
+BOO011-4.ma
+BOO012-2.ma
+BOO012-4.ma
+BOO013-2.ma
+BOO013-4.ma
+BOO016-2.ma
+BOO017-2.ma
+BOO018-4.ma
+BOO034-1.ma
+BOO069-1.ma
+BOO071-1.ma
+BOO075-1.ma
+COL004-3.ma
+COL007-1.ma
+COL008-1.ma
+COL010-1.ma
+COL012-1.ma
+COL013-1.ma
+COL014-1.ma
+COL015-1.ma
+COL016-1.ma
+COL017-1.ma
+COL018-1.ma
+COL021-1.ma
+COL022-1.ma
+COL024-1.ma
+COL025-1.ma
+COL045-1.ma
+COL048-1.ma
+COL050-1.ma
+COL058-2.ma
+COL058-3.ma
+COL060-2.ma
+COL060-3.ma
+COL061-2.ma
+COL061-3.ma
+COL062-2.ma
+COL062-3.ma
+COL063-2.ma
+COL063-3.ma
+COL063-4.ma
+COL063-5.ma
+COL063-6.ma
+COL064-2.ma
+COL064-3.ma
+COL064-4.ma
+COL064-5.ma
+COL064-6.ma
+COL064-7.ma
+COL064-8.ma
+COL064-9.ma
+COL083-1.ma
+COL084-1.ma
+COL085-1.ma
+COL086-1.ma
+GRP001-2.ma
+GRP001-4.ma
+GRP010-4.ma
+GRP011-4.ma
+GRP012-4.ma
+GRP022-2.ma
+GRP023-2.ma
+GRP115-1.ma
+GRP116-1.ma
+GRP117-1.ma
+GRP118-1.ma
+GRP136-1.ma
+GRP137-1.ma
+GRP139-1.ma
+GRP141-1.ma
+GRP142-1.ma
+GRP143-1.ma
+GRP144-1.ma
+GRP145-1.ma
+GRP146-1.ma
+GRP149-1.ma
+GRP150-1.ma
+GRP151-1.ma
+GRP152-1.ma
+GRP153-1.ma
+GRP154-1.ma
+GRP155-1.ma
+GRP156-1.ma
+GRP157-1.ma
+GRP158-1.ma
+GRP159-1.ma
+GRP160-1.ma
+GRP161-1.ma
+GRP162-1.ma
+GRP163-1.ma
+GRP168-1.ma
+GRP168-2.ma
+GRP173-1.ma
+GRP174-1.ma
+GRP176-1.ma
+GRP176-2.ma
+GRP182-1.ma
+GRP182-2.ma
+GRP182-3.ma
+GRP182-4.ma
+GRP186-3.ma
+GRP186-4.ma
+GRP188-1.ma
+GRP188-2.ma
+GRP189-1.ma
+GRP189-2.ma
+GRP192-1.ma
+GRP206-1.ma
+GRP454-1.ma
+GRP455-1.ma
+GRP456-1.ma
+GRP457-1.ma
+GRP458-1.ma
+GRP459-1.ma
+GRP460-1.ma
+GRP463-1.ma
+GRP467-1.ma
+GRP481-1.ma
+GRP484-1.ma
+GRP485-1.ma
+GRP486-1.ma
+GRP487-1.ma
+GRP488-1.ma
+GRP490-1.ma
+GRP491-1.ma
+GRP492-1.ma
+GRP493-1.ma
+GRP494-1.ma
+GRP495-1.ma
+GRP496-1.ma
+GRP497-1.ma
+GRP498-1.ma
+GRP509-1.ma
+GRP510-1.ma
+GRP511-1.ma
+GRP512-1.ma
+GRP513-1.ma
+GRP514-1.ma
+GRP515-1.ma
+GRP516-1.ma
+GRP517-1.ma
+GRP518-1.ma
+GRP520-1.ma
+GRP541-1.ma
+GRP542-1.ma
+GRP543-1.ma
+GRP544-1.ma
+GRP545-1.ma
+GRP546-1.ma
+GRP547-1.ma
+GRP548-1.ma
+GRP549-1.ma
+GRP550-1.ma
+GRP551-1.ma
+GRP552-1.ma
+GRP556-1.ma
+GRP558-1.ma
+GRP560-1.ma
+GRP561-1.ma
+GRP562-1.ma
+GRP564-1.ma
+GRP565-1.ma
+GRP566-1.ma
+GRP567-1.ma
+GRP568-1.ma
+GRP569-1.ma
+GRP570-1.ma
+GRP572-1.ma
+GRP573-1.ma
+GRP574-1.ma
+GRP576-1.ma
+GRP577-1.ma
+GRP578-1.ma
+GRP580-1.ma
+GRP581-1.ma
+GRP582-1.ma
+GRP583-1.ma
+GRP584-1.ma
+GRP586-1.ma
+GRP588-1.ma
+GRP590-1.ma
+GRP592-1.ma
+GRP595-1.ma
+GRP596-1.ma
+GRP597-1.ma
+GRP598-1.ma
+GRP599-1.ma
+GRP600-1.ma
+GRP602-1.ma
+GRP603-1.ma
+GRP604-1.ma
+GRP605-1.ma
+GRP606-1.ma
+GRP608-1.ma
+GRP612-1.ma
+GRP613-1.ma
+GRP614-1.ma
+GRP615-1.ma
+GRP616-1.ma
+LAT008-1.ma
+LAT033-1.ma
+LAT034-1.ma
+LAT039-1.ma
+LAT039-2.ma
+LAT040-1.ma
+LAT045-1.ma
+LCL110-2.ma
+LCL112-2.ma
+LCL113-2.ma
+LCL114-2.ma
+LCL115-2.ma
+LCL132-1.ma
+LCL133-1.ma
+LCL134-1.ma
+LCL135-1.ma
+LCL139-1.ma
+LCL140-1.ma
+LCL141-1.ma
+LCL153-1.ma
+LCL154-1.ma
+LCL155-1.ma
+LCL156-1.ma
+LCL157-1.ma
+LCL158-1.ma
+LCL161-1.ma
+LCL164-1.ma
+LDA001-1.ma
+LDA007-3.ma
+RNG007-4.ma
+RNG008-4.ma
+RNG011-5.ma
+RNG023-6.ma
+RNG023-7.ma
+RNG024-6.ma
+RNG024-7.ma
+ROB002-1.ma
+ROB009-1.ma
+ROB010-1.ma
+ROB013-1.ma
+ROB030-1.ma
+SYN083-1.ma

diff --git a/helm/software/matita/contribs/ng_TPTP/run_veloci.sh b/helm/software/matita/contribs/ng_TPTP/run_veloci.sh
new file mode 100755 (executable)
index 0000000..68976da
--- /dev/null
+++ b/helm/software/matita/contribs/ng_TPTP/run_veloci.sh
@@ -0,0 +1,7 @@
+for X in `cat Veloci`;
+do
+echo $X;
+touch $X;
+/home/maxime/matita/software/matita/matitac.opt $X 2> /dev/null
+done
+