Wrong function.
New utility: HAS-INCLUDE-INSTRUCTION-P.
Die if there's an include instruction.
Select from the non-definitions.
SETF.
Use conditional FORMATting.
Two values: whether the DB is satisfiable, and the SZS status.
Use an auxiliary method to deal with the conjecture case.
Use SATISFIABLE-P.
Use HAS-CONJECTURE-P.
Return the conjecture item, not a cons.
Using the extra return value of SATISFIABLBLE-P, we can determine whether to say "unknown".
Use an around auxiliary method.
Cruft.
It's not to safe to assume that the list is made up of TPTP-FORMULA objects.
We don't need the BLOCK.
Dump the error output and make the UNWIND-PROTECT go around the (LET immediately around) RUN-PROGRAM.
Stop using WITH-TIMEOUT.

It may leave streams open.  We now just trust the ATPs to timeout
properly.  We really ought to have our own timeouts, but I need to
think how to make sure that streams are closed.  Perhaps with a
condition?
Use LET*.
Use the long name.