4 TODO=Unsatisfiable/[A-Z]*.ma
14 LOGNAME=logs/log.`basename $X`.gz
15 ../../matitac.opt -nodb $X | gzip -9 > $LOGNAME 2>&1
16 RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
17 if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then
18 TIME=`grep "TIME NEEDED" $LOGNAME`
19 echo OK $TIME $RATING $i