#!/bin/ksh

DIR="$1"
PROBLEM="$2"
TIME="$3"

for FILE in `ls ${DIR}/p-${PROBLEM}*` ;
do

cat /dev/null > result

SPASS -Auto=1 -Sorts=0 -CNFOptSkolem=0 -CNFStrSkolem=0 \
      -DocProof=0 -PProblem=0 -PGiven=0 -PKept=0 \
      -EMLTranslation=2 -EMLFuncFluted=1 \
      -TimeLimit=$TIME $FILE > result | true


INSTANCE=`echo ${FILE} | sed "s#${DIR}/##"` 

if test -s result
then
UNSAT=`grep -c "^SPASS beiseite: Proof found" result | sed "s#[^0-9]##g`
SAT=`grep -c "^SPASS beiseite: Completion found" result | sed "s#[^0-9]##g`

WHEN=`grep "^SPASS spent" result | sed  "s#SPASS spent##" | sed "s#on the problem\.##"`

if test $UNSAT -eq 0 -a $SAT -eq 0 ;
then
TIME=360000
else
HOUR=`echo $WHEN | sed "s#\([0-9]*\):\([0-9]*\):\([0-9]*\)\.\([0-9]*\)#\1#" | sed "s#[^0-9]##g"`
MIN=`echo $WHEN | sed "s#\([0-9]*\):\([0-9]*\):\([0-9]*\)\.\([0-9]*\)#\2#" | sed "s#[^0-9]##g"`
SEC=`echo $WHEN | sed "s#\([0-9]*\):\([0-9]*\):\([0-9]*\)\.\([0-9]*\)#\3#"  | sed "s#[^0-9]##g"`
MSEC=`echo $WHEN | sed "s#\([0-9]*\):\([0-9]*\):\([0-9]*\)\.\([0-9]*\)#\4#"  | sed "s#[^0-9]##g"`


let TIME=$(($MSEC+$((100*$(($SEC+$((60*$(($MIN+$((60*$HOUR))))))))))))
fi

if test $UNSAT -eq 1 ;
then
	echo "r ${INSTANCE} ${TIME} U"
elif test $SAT -eq 1 ;
then
	echo "r ${INSTANCE} ${TIME} S"
else
	echo "r ${INSTANCE} ${TIME} T"
fi
else
	echo "r ${INSTANCE} 360000 T"
fi
done