X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Ftests%2FTPTP%2FREADME;fp=matita%2Ftests%2FTPTP%2FREADME;h=e5d4b04b1676d125184921b4299e699543e8b4d2;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/tests/TPTP/README b/matita/tests/TPTP/README
new file mode 100644
index 000000000..e5d4b04b1
--- /dev/null
+++ b/matita/tests/TPTP/README
@@ -0,0 +1,42 @@
+to generate the problems:
+
+  cd ../../../components/binaries/tptp2grafite/
+  make generate
+  cd ../../../matita/tests/TPTP
+  ./classify.sh
+
+to start a run:
+
+  be sure to have matitac.opt in ../../
+  ./try | tee logname
+
+if you have a file containing the list of files to execute, like 
+
+  ...
+  Unsatisfiable/BOO001-1.ma
+  Unsatisfiable/BOO002-1.ma
+  Unsatisfiable/BOO004-2.ma
+  Unsatisfiable/LCL113-2.ma
+  ...
+
+  you can run 
+  
+  ./try filewithproblemlist | tee logname
+
+logname format
+
+  log.SECONDS.DAY-MONTH.MESSAGE
+
+other scripts
+
+  simulate_casc.sh logfile 
+
+    Gives the results of the problems listed in elenco_CASC.txt
+
+  merge_sorted_logs.awk
+
+    Given a file composed by the sorted concatenation of 2 logs
+    returns the one obtaining using the best of duplicate lines
+    (use to merge a log with a successive run on the FAIL problems)
+
+# eof