helm/software/matita/tests/TPTP/README

   1 to generate the problems:
   2
   3   cd ../../../components/binaries/tptp2grafite/
   4   make generate
   5   cd ../../../matita/tests/TPTP
   6   ./classify.sh
   7
   8 to start a run:
   9
  10   be sure to have matitac.opt in ../../
  11   ./try | tee logname
  12
  13 if you have a file containing the list of files to execute, like
  14
  15   ...
  16   Unsatisfiable/BOO001-1.ma
  17   Unsatisfiable/BOO002-1.ma
  18   Unsatisfiable/BOO004-2.ma
  19   Unsatisfiable/LCL113-2.ma
  20   ...
  21
  22   you can run
  23
  24   ./try filewithproblemlist | tee logname
  25
  26 logname format
  27
  28   log.SECONDS.DAY-MONTH.MESSAGE
  29
  30 other scripts
  31
  32   simulate_casc.sh logfile
  33
  34     Gives the results of the problems listed in elenco_CASC.txt
  35
  36   merge_sorted_logs.awk
  37
  38     Given a file composed by the sorted concatenation of 2 logs
  39     returns the one obtaining using the best of duplicate lines
  40     (use to merge a log with a successive run on the FAIL problems)
  41
  42 # eof