equal
deleted
inserted
replaced
27 for FILE in "$@" |
27 for FILE in "$@" |
28 do |
28 do |
29 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
29 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
30 ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ |
30 ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ |
31 > /tmp/$SCRATCH.thy |
31 > /tmp/$SCRATCH.thy |
32 "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" |
32 "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" |
33 done |
33 done |