5 MATITAC=../../matitac.opt
7 MATITAPROVER=../../matitaprover.opt
8 TPTPPATH=/home/tassi/TPTP-v3.1.1/
11 if [ $prover = 'y' ]; then
12 TODO=`cat elenco_unsatisfiable.txt`
14 TODO=Unsatisfiable/[A-Z]*.ma
25 LOGNAME=logs/log.`basename $X`
26 if [ $prover = 'y' ]; then
27 $MATITAPROVER -tptppath $TPTPPATH $X > $LOGNAME 2>&1
29 $MATITAC -nodb $X > $LOGNAME 2>&1
31 if [ $prover = 'y' ]; then
32 BASE=`echo $X | cut -c 1-3`
33 RATING=`grep "Rating" $TPTPPATH/Problems/$BASE/$X | sed 's/v.*//' | sed 's/%//'`
35 RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
37 if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then
38 TIME=`grep "TIME" $LOGNAME`
39 MAXWEIGHT=`grep "max weight:" $LOGNAME`
40 echo OK $TIME $RATING $MAXWEIGHT $i