diff -r 866b075aa99b -r 04c87dec70b8 src/HOL/Tools/ATP/scripts/spass
--- a/src/HOL/Tools/ATP/scripts/spass	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/spass	Sat Oct 29 13:15:58 2011 +0200
@@ -8,7 +8,9 @@
 options=${@:1:$(($#-1))}
 name=${@:$(($#)):1}
 
-"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg
+# Try converting the file from TPTP to DFG, but fail gracefully if it is already
+# in DFG format.
+"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg || cp $name $name.fof.dfg
 "$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
     | sed 's/description({$/description({*/' \
     | sed 's/set_ClauseFormulaRelation()\.//' \