\documentstyle[11pt]{article}
\setlength{\hoffset}{-.5in}
\setlength{\voffset}{-1in}
\setlength{\parskip}{.1in}
\textwidth=16cm \textheight=23.5cm
\newcommand{\otter}{{\sc Otter}}
\begin{document}
\title{{\Large\bf O{\large\bf TTER} 3.0}\thanks{This work was
supported by the Office of Scientific Computing,
U.S. Department of Energy, under Contract W-31-109-Eng-38.}}
\author{{\it William McCune} \\ \\
Mathematics and Computer Science Division \\
Argonne National Laboratory \\
Argonne, Illinois 60439-4844, U.S.A. \\
e-mail: mccune@mcs.anl.gov \\
phone: 708-252-3065}
\date{December 15, 1993}
\maketitle
\thispagestyle{empty}

\otter\ is a clause-based theorem prover for first-order logic
with equality.  It offers the inference rules binary resolution,
hyperresolution, unit-resulting resolution, and paramodulation;
it also offers forward and backward subsumption, forward and
backward demodulation (rewriting), term ordering, Knuth-Bendix
completion, answer literals,
and conversion of first-order formulas to clauses.
\otter\ 3.0 can be used in two modes.  In the ordinary mode, the
user specifies inferences rules and a search strategy, and in the
autonomous mode (new in \otter\ 3.0, see below) the user simply
supplies a set of clauses.
The goal in building \otter\ was to have a fast, production-quality
theorem prover for experimenting with new methods 
and for assisting mathematicians and logicians with
their research.

At the core of \otter\ is a straightforward mechanism, the {\em
given-clause algorithm}, for drawing inferences and searching for a
refutation with the set of support strategy.  The given-clause
algorithm operates mainly on two lists of clauses, {\em sos} and
{\em usable}.  At the start of the search, {\em sos} is the supported
clauses, and {\em usable} is the nonsupported clauses.
The main loop of the given-clause algorithm is the following.
{\small
\begin{verbatim}
    While (sos is not empty and no refutation has been found)
        1. Let given_clause be the `best' clause in sos;
        2. Move given_clause from sos to usable;
        3. Infer and process new clauses using the inference rules in
               effect; each new clause must have the given_clause as
               one of its parents and members of usable as its other
               parents;  new clauses that pass the retention tests
               are appended to sos;
    End of while loop.
\end{verbatim}
}
Surrounding the core of \otter\ are many additional features, including
weighting functions  to guide and restrict the search,
a simple interactive routine for modifying the search,
a flexible syntax, and
evaluable functions and enhanced term rewriting for
``programming'' searches.

\paragraph{New Features.} Features new in \otter\ 3.0 include
Prolog-style operator declaration,
the hot-list strategy for emphasizing key clauses,
interactive selection of given clauses,
ordered hyperresolution,
optimization for propositional problems, and
an autonomous mode.

For the autonomous mode, the user
supplies a set of clauses and/or nonclausal formulas, then
\otter\ does a simple syntactic analysis, automatically
setting parameters and assigning clauses to lists.  The properties that
are considered are whether the clauses are Horn, are propositional,
involve equality, contain equality axioms, and are all units.

\paragraph{Experiments on TPTP.}
Table 1 lists the results of \otter\ in its autonomous mode for the
problems of TPTP v1.0.0 \cite{tptp1}.  TPTP problems involving
equality contain equality axioms, and for those problems, we deleted
the equality axioms and used paramodulation and demodulation instead.

The TPTP experiments were run on an i486 DX2-66 processor running the
Linux operating system.  (For \otter\ jobs, the Linux i486 is about
1.3 times faster than a SPARCstation 2.)  For problems that are
listed, the number of seconds taken to find a proof is shown.  If a
problem is not listed, then a proof was not found within ten minutes.

\paragraph{Availability.}
The \otter\ 3.0 distribution, including source code, many test
problems, and the manual \cite{otter3}, is freely available by anonymous FTP
from \verb:info@mcs.anl.gov:; see the file \verb:pub/Otter/README:.
\otter\ 3.0 might be available for DOS and/or
Macintosh operating systems in the near future.  One can request
information by e-mail from \verb:otter@mcs.anl.gov:.

% \vspace{.5in}
% Tables:  lines (including caption, if any)
\begin{center}
{\small
% \begin{table}[h] \centering
% \caption{TPTP Problem---Seconds to Proof} \label{tab}
\begin{tabular}{lr|lr|lr|lr|lr}
\multicolumn{10}{c}{Table 1: TPTP Problem---Seconds to Proof} \\ \hline
ALG001-3 & 418 & ALG002-1 & 2 &  &  &  &  &  &  \\
BOO001-1 & $<$1 & BOO002-1 & 34 & BOO003-1 & 14 & BOO003-2 & $<$1 & BOO004-1 & 2 \\
BOO004-2 & 1 & BOO005-1 & 8 & BOO006-1 & 20 & BOO006-2 & $<$1 & BOO007-2 & 100 \\
BOO008-1 & 221 & BOO008-2 & 173 & BOO009-1 & 19 & BOO009-2 & 1 & BOO010-1 & 9 \\
BOO010-2 & 1 & BOO011-1 & $<$1 & BOO012-1 & 60 & BOO012-2 & $<$1 & BOO012-3 & 407 \\
BOO013-1 & 22 & BOO013-2 & $<$1 & BOO013-3 & 23 & BOO014-2 & 40 & BOO016-1 & 11 \\
BOO016-2 & 2 & BOO017-1 & 31 & BOO017-2 & 3 &  &  &  &  \\
CAT001-1 & 14 & CAT001-3 & 3 & CAT002-1 & 31 & CAT002-3 & 572 & CAT002-4 & 53 \\
CAT003-1 & 12 & CAT003-4 & 577 & CAT004-1 & 30 & CAT005-1 & 2 & CAT005-3 & $<$1 \\
CAT005-4 & $<$1 & CAT006-1 & 2 & CAT006-3 & $<$1 & CAT006-4 & $<$1 & CAT007-1 & $<$1 \\
CAT007-3 & 13 & CAT008-1 & 3 & CAT009-1 & 4 & CAT010-1 & 4 & CAT011-1 & $<$1 \\
CAT011-2 & $<$1 & CAT011-3 & 548 & CAT011-4 & 21 & CAT012-1 & 2 & CAT012-3 & 228 \\
CAT012-4 & 14 & CAT013-1 & $<$1 & CAT013-3 & 546 & CAT013-4 & 18 & CAT014-1 & 2 \\
CAT014-2 & $<$1 & CAT014-3 & 551 & CAT014-4 & 18 & CAT016-3 & $<$1 & CAT016-4 & $<$1 \\
CAT017-3 & $<$1 & CAT017-4 & $<$1 & CAT018-1 & 3 & CAT019-1 & $<$1 & CAT019-2 & $<$1 \\
CAT019-3 & 23 &  &  &  &  &  &  &  &  \\
COL001-1 & 2 & COL001-2 & $<$1 & COL002-1 & 1 & COL002-2 & 14 & COL004-3 & $<$1 \\
COL007-1 & $<$1 & COL008-1 & $<$1 & COL009-1 & 3 & COL010-1 & $<$1 & COL011-1 & 13 \\
COL012-1 & $<$1 & COL013-1 & $<$1 & COL014-1 & $<$1 & COL015-1 & $<$1 & COL016-1 & $<$1 \\
COL017-1 & $<$1 & COL018-1 & $<$1 & COL019-1 & $<$1 & COL020-1 & $<$1 & COL021-1 & $<$1 \\
COL022-1 & $<$1 & COL023-1 & $<$1 & COL024-1 & $<$1 & COL025-1 & $<$1 & COL026-1 & 1 \\
COL027-1 & 2 & COL028-1 & $<$1 & COL029-1 & $<$1 & COL030-1 & $<$1 & COL031-1 & $<$1 \\
COL032-1 & $<$1 & COL033-1 & $<$1 & COL034-1 & 2 & COL035-1 & 19 & COL039-1 & 13 \\
COL040-1 & 17 & COL041-1 & 1 & COL044-1 & 17 & COL045-1 & $<$1 & COL048-1 & $<$1 \\
COL049-1 & 5 & COL050-1 & $<$1 & COL051-1 & $<$1 & COL052-1 & $<$1 & COL052-2 & $<$1 \\
COL053-1 & $<$1 & COL054-1 & $<$1 & COL055-1 & $<$1 & COL056-1 & $<$1 & COL057-1 & 8 \\
COL058-1 & $<$1 & COL058-2 & 1 & COL058-3 & $<$1 & COL059-1 & $<$1 & COL060-2 & $<$1 \\
\end{tabular}
% \end{table}
}
\end{center}

\begin{center}
{\small
% \begin{table}[h] \centering
\begin{tabular}{lr|lr|lr|lr|lr}
\multicolumn{10}{c}{Table 1: TPTP Problem---Seconds to Proof (continued)} \\ \hline
COL060-3 & $<$1 & COL061-2 & $<$1 & COL061-3 & $<$1 & COL062-2 & $<$1 & COL062-3 & $<$1 \\
COL063-2 & $<$1 & COL063-3 & $<$1 & COL063-4 & $<$1 & COL063-5 & $<$1 & COL063-6 & $<$1 \\
COL064-10 & $<$1 & COL064-11 & $<$1 & COL064-2 & $<$1 & COL064-3 & $<$1 & COL064-4 & $<$1 \\
COL064-5 & $<$1 & COL064-6 & $<$1 & COL064-7 & $<$1 & COL064-8 & $<$1 & COL064-9 & $<$1 \\
COL066-2 & $<$1 & COL066-3 & $<$1 &  &  &  &  &  &  \\
COM001-1 & $<$1 & COM002-1 & $<$1 & COM002-2 & $<$1 &  &  &  &  \\
GEO002-3 & $<$1 & GEO003-1 & 2 & GEO003-2 & 3 & GEO003-3 & 1 & GEO006-3 & 15 \\
GEO007-3 & 255 & GEO011-2 & $<$1 & GEO011-3 & 3 & GEO011-4 & $<$1 & GEO011-5 & $<$1 \\
GEO013-3 & 101 & GEO014-2 & $<$1 & GEO015-2 & 2 & GEO015-3 & $<$1 & GEO016-2 & $<$1 \\
GEO016-3 & $<$1 & GEO017-2 & 5 & GEO017-3 & 4 & GEO018-2 & 4 & GEO018-3 & 6 \\
GEO019-2 & $<$1 & GEO019-3 & $<$1 & GEO020-2 & 5 & GEO020-3 & 4 & GEO021-2 & 3 \\
GEO021-3 & 6 & GEO022-2 & 17 & GEO022-3 & 16 & GEO024-2 & 4 & GEO024-3 & 3 \\
GEO026-2 & 14 & GEO026-3 & 27 & GEO027-3 & 4 & GEO030-2 & 110 & GEO030-3 & 93 \\
GEO034-3 & 95 & GEO035-2 & 1 & GEO035-3 & 1 & GEO036-2 & 469 & GEO036-3 & 85 \\
GEO038-2 & 3 & GEO038-3 & 2 & GEO039-2 & 27 & GEO039-3 & $<$1 & GEO041-3 & 3 \\
GEO045-3 & 10 & GEO046-3 & 9 & GEO047-3 & 6 & GEO051-3 & 93 & GEO052-3 & 92 \\
GEO053-3 & 15 & GEO054-2 & $<$1 & GEO054-3 & $<$1 & GEO055-2 & $<$1 & GEO055-3 & $<$1 \\
GEO056-2 & 6 & GEO056-3 & $<$1 & GEO057-2 & 2 & GEO057-3 & $<$1 & GEO058-2 & 38 \\
GEO058-3 & 8 & GEO064-3 & 5 & GEO065-3 & 5 & GEO066-3 & 5 & GEO067-2 & 4 \\
GEO067-3 & 3 & GEO069-3 & 107 &  &  &  &  &  &  \\
GRA001-1 & $<$1 &  &  &  &  &  &  &  &  \\
GRP001-1 & $<$1 & GRP001-2 & $<$1 & GRP001-4 & $<$1 & GRP001-5 & $<$1 & GRP002-3 & 2 \\
GRP002-4 & 4 & GRP003-1 & $<$1 & GRP003-2 & $<$1 & GRP004-1 & $<$1 & GRP004-2 & $<$1 \\
GRP005-1 & $<$1 & GRP006-1 & $<$1 & GRP007-1 & $<$1 & GRP008-1 & 11 & GRP009-1 & $<$1 \\
GRP010-1 & $<$1 & GRP010-4 & $<$1 & GRP011-4 & $<$1 & GRP012-1 & $<$1 & GRP012-2 & $<$1 \\
GRP012-3 & 4 & GRP012-4 & $<$1 & GRP013-1 & $<$1 & GRP017-1 & $<$1 & GRP018-1 & $<$1 \\
GRP019-1 & $<$1 & GRP020-1 & $<$1 & GRP021-1 & $<$1 & GRP022-1 & $<$1 & GRP022-2 & $<$1 \\
GRP023-1 & $<$1 & GRP023-2 & $<$1 & GRP025-1 & 4 & GRP025-2 & 2 & GRP025-3 & 4 \\
GRP025-4 & 4 & GRP026-1 & 11 & GRP026-2 & 4 & GRP026-3 & 11 & GRP026-4 & 7 \\
GRP027-1 & $<$1 & GRP027-2 & $<$1 & GRP028-1 & $<$1 & GRP029-1 & $<$1 & GRP029-2 & $<$1 \\
GRP030-1 & $<$1 & GRP031-1 & $<$1 & GRP031-2 & $<$1 & GRP032-3 & $<$1 & GRP033-3 & $<$1 \\
GRP033-4 & $<$1 & GRP034-3 & $<$1 & GRP034-4 & $<$1 & GRP035-3 & $<$1 & GRP036-3 & $<$1 \\
GRP037-3 & 2 & GRP038-3 & $<$1 & GRP041-2 & $<$1 & GRP042-2 & $<$1 & GRP043-2 & $<$1 \\
GRP044-2 & $<$1 & GRP045-2 & $<$1 & GRP046-2 & $<$1 & GRP047-2 & $<$1 & GRP048-2 & $<$1 \\
GRP050-1 & 37 & GRP058-1 & 10 & GRP059-1 & 11 & GRP070-1 & 225 & GRP075-1 & 140 \\
GRP076-1 & 313 & GRP078-1 & 254 & GRP079-1 & 100 & GRP085-1 & 2 & GRP086-1 & 2 \\
GRP087-1 & 24 & GRP096-1 & 211 & GRP098-1 & 258 & GRP100-1 & 224 & GRP103-1 & 326 \\
HEN001-1 & $<$1 & HEN001-3 & $<$1 & HEN001-5 & $<$1 & HEN002-1 & $<$1 & HEN002-2 & $<$1 \\
HEN002-3 & $<$1 & HEN002-4 & $<$1 & HEN002-5 & $<$1 & HEN003-1 & $<$1 & HEN003-2 & $<$1 \\
HEN003-3 & $<$1 & HEN003-4 & $<$1 & HEN003-5 & 2 & HEN004-1 & 3 & HEN004-2 & 2 \\
HEN004-3 & 1 & HEN004-4 & 4 & HEN004-5 & 5 & HEN004-6 & 2 & HEN005-1 & $<$1 \\
HEN005-2 & 2 & HEN005-3 & $<$1 & HEN005-4 & 4 & HEN005-5 & 5 & HEN005-6 & $<$1 \\
HEN006-1 & 4 & HEN006-2 & 7 & HEN006-3 & 52 & HEN006-4 & 4 & HEN006-5 & 8 \\
HEN006-6 & 65 & HEN006-7 & 4 & HEN007-1 & 24 & HEN007-2 & 2 & HEN007-3 & 199 \\
HEN007-4 & $<$1 & HEN007-5 & 61 & HEN007-6 & 2 & HEN008-1 & $<$1 & HEN008-2 & 3 \\
HEN008-3 & $<$1 & HEN008-4 & 2 & HEN008-5 & $<$1 & HEN008-6 & $<$1 & HEN009-1 & 18 \\
HEN009-2 & 2 & HEN009-3 & 518 & HEN009-4 & 1 & HEN009-5 & 3 & HEN009-6 & 17 \\
HEN010-1 & 14 & HEN010-2 & 3 & HEN010-4 & 7 & HEN010-5 & 6 & HEN010-6 & 8 \\
HEN010-7 & 2 & HEN011-1 & 209 & HEN011-2 & 162 & HEN011-4 & 255 & HEN011-5 & 483 \\
HEN012-1 & 1 & HEN012-3 & $<$1 &  &  &  &  &  &  \\
LAT005-1 & 16 & LAT005-2 & 5 &  &  &  &  &  &  \\
LCL004-1 & 24 & LCL006-1 & 419 & LCL007-1 & $<$1 & LCL008-1 & $<$1 & LCL009-1 & $<$1 \\
LCL010-1 & 3 & LCL011-1 & 75 & LCL012-1 & 555 & LCL013-1 & $<$1 & LCL014-1 & 164 \\
LCL015-1 & 481 & LCL016-1 & 272 & LCL017-1 & 549 & LCL018-1 & 379 & LCL022-1 & $<$1 \\
\end{tabular}
% \end{table}
}
\end{center}

\begin{center}
{\small
% \begin{table}[h] \centering
\begin{tabular}{l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r}
\multicolumn{10}{c}{Table 1: TPTP Problem---Seconds to Proof (continued)} \\ \hline
LCL023-1 & 3 & LCL024-1 & 516 & LCL025-1 & 37 & LCL026-1 & 53 & LCL027-1 & $<$1 \\
LCL029-1 & 3 & LCL030-1 & 420 & LCL033-1 & $<$1 & LCL034-1 & 8 & LCL035-1 & $<$1 \\
LCL036-1 & 2 & LCL039-1 & 127 & LCL040-1 & 113 & LCL041-1 & 3 & LCL043-1 & 4 \\
LCL044-1 & 5 & LCL046-1 & $<$1 & LCL047-1 & 4 & LCL048-1 & 4 & LCL049-1 & 42 \\
LCL050-1 & 44 & LCL051-1 & 223 & LCL052-1 & 43 & LCL053-1 & 46 & LCL055-1 & 23 \\
LCL056-1 & 20 & LCL057-1 & 22 & LCL059-1 & 20 & LCL064-1 & 486 & LCL064-2 & 8 \\
LCL065-1 & 2 & LCL066-1 & $<$1 & LCL067-1 & 249 & LCL070-1 & 248 & LCL071-1 & 253 \\
LCL072-1 & 115 & LCL075-1 & 9 & LCL076-1 & $<$1 & LCL076-2 & $<$1 & LCL076-3 & $<$1 \\
LCL077-1 & $<$1 & LCL077-2 & $<$1 & LCL079-1 & $<$1 & LCL080-1 & 66 & LCL080-2 & 52 \\
LCL081-1 & $<$1 & LCL082-1 & $<$1 & LCL083-1 & 16 & LCL083-2 & $<$1 & LCL084-2 & $<$1 \\
LCL084-3 & $<$1 & LCL086-1 & $<$1 & LCL087-1 & $<$1 & LCL088-1 & 2 & LCL089-1 & 3 \\
LCL090-1 & 2 & LCL091-1 & 3 & LCL092-1 & 4 & LCL093-1 & 112 & LCL094-1 & 5 \\
LCL095-1 & 13 & LCL096-1 & 105 & LCL097-1 & 4 & LCL098-1 & 6 & LCL101-1 & $<$1 \\
LCL102-1 & 33 & LCL103-1 & 221 & LCL104-1 & $<$1 & LCL106-1 & $<$1 & LCL107-1 & $<$1 \\
LCL108-1 & 1 & LCL109-5 & $<$1 & LCL109-6 & 102 & LCL110-1 & 1 & LCL110-2 & $<$1 \\
LCL111-1 & 2 & LCL111-2 & 9 & LCL112-1 & $<$1 & LCL112-2 & $<$1 & LCL113-2 & $<$1 \\
LCL114-2 & 1 & LCL115-1 & 8 & LCL115-2 & 2 & LCL116-2 & 2 & LCL117-1 & $<$1 \\
LCL118-1 & 8 & LCL120-1 & 50 & LCL121-1 & 120 & LCL126-1 & $<$1 & LCL128-1 & 125 \\
LCL130-1 & $<$1 & LCL131-1 & 122 & LCL132-1 & $<$1 & LCL133-1 & $<$1 & LCL134-1 & $<$1 \\
LCL135-1 & $<$1 & LCL138-1 & 105 & LCL139-1 & $<$1 & LCL140-1 & $<$1 & LCL141-1 & $<$1 \\
LCL143-1 & $<$1 & LCL146-1 & 107 & LCL153-1 & $<$1 & LCL154-1 & $<$1 & LCL155-1 & $<$1 \\
LCL156-1 & $<$1 & LCL157-1 & $<$1 & LCL158-1 & $<$1 & LCL159-1 & 1 & LCL161-1 & $<$1 \\
LCL162-1 & 40 & LCL163-1 & 162 & LCL164-1 & 1 &  &  &  &  \\
LDA001-1 & $<$1 & LDA002-1 & 2 & LDA003-1 & $<$1 & LDA007-1 & 40 & LDA007-2 & 25 \\
LDA007-3 & $<$1 & LDA010-2 & 195 & LDA011-2 & 189 & LDA012-2 & 11 & LDA013-1 & $<$1 \\
MSC001-1 & 7 & MSC002-1 & $<$1 & MSC002-2 & $<$1 & MSC003-1 & $<$1 & MSC004-1 & $<$1 \\
MSC005-1 & 29 & MSC006-1 & 5 & MSC007-1.002 & $<$1 & MSC007-1.003 & $<$1 & MSC007-1.004 & $<$1 \\
MSC007-1.005 & $<$1 & MSC007-1.006 & 9 & MSC007-1.007 & 193 & MSC007-2.002 & $<$1 & MSC007-2.003 & 3 \\
MSC008-1.002 & 67 &  &  &  &  &  &  &  &  \\
NUM001-1 & $<$1 & NUM002-1 & $<$1 & NUM003-1 & $<$1 & NUM004-1 & $<$1 & NUM009-1 & 40 \\
NUM014-1 & $<$1 & NUM015-1 & $<$1 & NUM016-1 & $<$1 & NUM016-2 & $<$1 & NUM017-1 & 168 \\
NUM017-2 & 168 & NUM019-1 & $<$1 & NUM020-1 & $<$1 & NUM021-1 & $<$1 & NUM022-1 & $<$1 \\
NUM023-1 & $<$1 & NUM025-1 & $<$1 & NUM025-2 & $<$1 & NUM180-1 & 7 & NUM183-1 & 45 \\
NUM190-1 & 11 & NUM228-1 & 10 & NUM283-1.002 & $<$1 & NUM283-1.003 & $<$1 & NUM283-1.004 & $<$1 \\
NUM283-1.005 & 9 & NUM284-1.002 & $<$1 & NUM284-1.003 & $<$1 & NUM284-1.004 & $<$1 & NUM284-1.005 & $<$1 \\
NUM284-1.006 & $<$1 & NUM284-1.007 & $<$1 & NUM284-1.008 & $<$1 & NUM284-1.009 & $<$1 & NUM284-1.010 & $<$1 \\
PLA002-1 & $<$1 & PLA003-1 & $<$1 &  &  &  &  &  &  \\
PRV001-1 & $<$1 & PRV002-1 & 2 & PRV003-1 & $<$1 & PRV005-1 & 2 & PRV006-1 & $<$1 \\
PRV008-1 & 2 & PRV009-1 & $<$1 &  &  &  &  &  &  \\
PUZ001-1 & $<$1 & PUZ001-2 & $<$1 & PUZ002-1 & $<$1 & PUZ003-1 & $<$1 & PUZ004-1 & $<$1 \\
PUZ005-1 & 1 & PUZ006-1 & $<$1 & PUZ007-1 & $<$1 & PUZ008-1 & $<$1 & PUZ008-2 & $<$1 \\
PUZ009-1 & $<$1 & PUZ011-1 & $<$1 & PUZ012-1 & $<$1 & PUZ013-1 & $<$1 & PUZ014-1 & $<$1 \\
PUZ016-1 & 4 & PUZ018-1 & $<$1 &  &  &  &  &  &  \\
RNG001-1 & 31 & RNG001-2 & 7 & RNG001-3 & 77 & RNG001-4 & 19 & RNG001-5 & 32 \\
RNG002-1 & $<$1 & RNG003-1 & $<$1 & RNG004-1 & 20 & RNG004-2 & 31 & RNG004-3 & 5 \\
RNG005-1 & 4 & RNG005-2 & $<$1 & RNG006-1 & 50 & RNG006-2 & 8 & RNG006-3 & 12 \\
RNG007-1 & 11 & RNG007-4 & $<$1 & RNG008-1 & 130 & RNG008-2 & 183 & RNG008-3 & 1 \\
RNG008-4 & 1 & RNG008-5 & 98 & RNG008-6 & 164 & RNG008-7 & 2 & RNG010-1 & $<$1 \\
RNG010-2 & $<$1 & RNG011-5 & $<$1 & RNG012-6 & $<$1 & RNG013-6 & $<$1 & RNG014-6 & $<$1 \\
RNG015-6 & $<$1 & RNG016-6 & 1 & RNG017-6 & $<$1 & RNG018-6 & $<$1 & RNG019-6 & 2 \\
RNG019-7 & 1 & RNG020-6 & 1 & RNG020-7 & 1 & RNG021-6 & 1 & RNG021-7 & 1 \\
RNG023-6 & 1 & RNG023-7 & 1 & RNG024-6 & 1 & RNG024-7 & 1 & RNG025-4 & 77 \\
RNG025-5 & 115 & RNG025-6 & 76 & RNG025-7 & 116 & RNG027-2 & $<$1 & RNG028-2 & $<$1 \\
RNG029-2 & $<$1 & RNG037-1 & 4 & RNG037-2 & $<$1 & RNG038-1 & $<$1 & RNG038-2 & $<$1 \\
\end{tabular}
% \end{table}
}
\end{center}

\begin{center}
{\small
% \begin{table}[h] \centering
\begin{tabular}{l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r}
\multicolumn{10}{c}{Table 1: TPTP Problem---Seconds to Proof (continued)} \\ \hline
RNG039-1 & 10 & RNG039-2 & 11 & RNG040-1 & $<$1 & RNG040-2 & 1 & RNG041-1 & 3 \\
ROB002-1 & $<$1 & ROB003-1 & $<$1 & ROB004-1 & 1 & ROB005-1 & 46 & ROB008-1 & $<$1 \\
ROB009-1 & $<$1 & ROB010-1 & $<$1 & ROB011-1 & $<$1 & ROB013-1 & $<$1 & ROB014-2 & 216 \\
ROB016-1 & $<$1 & ROB021-1 & 2 & ROB022-1 & 2 & ROB023-1 & 2 & ROB025-1 & 313 \\
SYN001-1.001 & $<$1 & SYN001-1.002 & $<$1 & SYN001-1.003 & $<$1 & SYN001-1.004 & $<$1 & SYN001-1.005 & $<$1 \\
SYN001-1.006 & $<$1 & SYN001-1.007 & 3 & SYN001-1.008 & 11 & SYN001-1.009 & 63 & SYN001-1.010 & 449 \\
SYN002-1.000 & $<$1 & SYN002-1.002 & $<$1 & SYN002-1.004 & $<$1 & SYN002-1.006 & $<$1 & SYN002-1.008 & $<$1 \\
SYN002-1.010 & $<$1 & SYN002-1.012 & $<$1 & SYN002-1.016 & $<$1 & SYN002-1.020 & 1 & SYN002-1.030 & 3 \\
SYN002-1.040 & 9 & SYN002-1.050 & 25 & SYN003-1.002 & $<$1 & SYN003-1.003 & $<$1 & SYN003-1.004 & $<$1 \\
SYN003-1.005 & $<$1 & SYN003-1.006 & $<$1 & SYN003-1.007 & $<$1 & SYN003-1.008 & $<$1 & SYN003-1.009 & $<$1 \\
SYN003-1.010 & $<$1 & SYN004-1.002 & $<$1 & SYN004-1.003 & $<$1 & SYN004-1.004 & $<$1 & SYN004-1.005 & $<$1 \\
SYN004-1.006 & $<$1 & SYN004-1.007 & $<$1 & SYN004-1.008 & $<$1 & SYN004-1.009 & $<$1 & SYN004-1.010 & $<$1 \\
SYN005-1.002 & $<$1 & SYN005-1.003 & $<$1 & SYN005-1.004 & $<$1 & SYN005-1.005 & $<$1 & SYN005-1.006 & $<$1 \\
SYN005-1.007 & $<$1 & SYN005-1.008 & $<$1 & SYN005-1.009 & $<$1 & SYN005-1.010 & $<$1 & SYN006-1 & $<$1 \\
SYN007-1.001 & $<$1 & SYN007-1.002 & $<$1 & SYN007-1.003 & $<$1 & SYN007-1.004 & $<$1 & SYN007-1.005 & 3 \\
SYN007-1.006 & 13 & SYN007-1.007 & 62 & SYN008-1 & $<$1 & SYN009-1 & $<$1 & SYN010-1.002 & $<$1 \\
SYN010-1.005 & $<$1 & SYN010-1.010 & $<$1 & SYN010-2.002 & $<$1 & SYN010-2.005 & $<$1 & SYN010-2.010 & $<$1 \\
SYN010-3.002 & $<$1 & SYN010-3.005 & $<$1 & SYN010-3.010 & 2 & SYN014-2 & $<$1 & SYN015-2 & 219 \\
SYN028-1 & $<$1 & SYN029-1 & $<$1 & SYN030-1 & $<$1 & SYN031-1 & $<$1 & SYN032-1 & $<$1 \\
SYN033-1 & $<$1 & SYN034-1 & $<$1 & SYN035-1 & $<$1 & SYN036-3 & 2 & SYN036-4 & 26 \\
SYN037-1 & 74 & SYN037-2 & $<$1 & SYN038-1 & 2 & SYN039-1 & 2 & SYN040-1 & $<$1 \\
SYN041-1 & $<$1 & SYN042-1 & $<$1 & SYN043-1 & $<$1 & SYN044-1 & $<$1 & SYN045-1 & $<$1 \\
SYN046-1 & $<$1 & SYN047-1 & $<$1 & SYN048-1 & $<$1 & SYN049-1 & $<$1 & SYN050-1 & $<$1 \\
SYN051-1 & $<$1 & SYN052-1 & $<$1 & SYN053-1 & $<$1 & SYN054-1 & $<$1 & SYN055-1 & $<$1 \\
SYN057-1 & $<$1 & SYN058-1 & $<$1 & SYN060-1 & $<$1 & SYN061-1 & $<$1 & SYN062-1 & $<$1 \\
SYN063-1 & $<$1 & SYN064-1 & $<$1 & SYN065-1 & $<$1 & SYN066-1 & $<$1 & SYN068-1 & $<$1 \\
SYN069-1 & $<$1 & SYN070-1 & $<$1 & SYN071-1 & $<$1 & SYN072-1 & $<$1 & SYN073-1 & $<$1 \\
SYN074-1 & 12 & SYN075-1 & 2 & SYN079-1 & $<$1 & SYN080-1 & $<$1 & SYN081-1 & $<$1 \\
SYN082-1 & $<$1 & SYN083-1 & $<$1 & SYN085-1.005 & $<$1 & SYN085-1.010 & $<$1 & SYN085-1.020 & $<$1 \\
SYN088-1.005 & $<$1 & SYN088-1.010 & $<$1 & SYN089-1.005 & $<$1 & SYN089-1.010 & 2 & SYN089-1.020 & 22 \\
SYN090-1.005 & $<$1 & SYN090-1.010 & $<$1 & SYN090-1.020 & 2 & SYN093-1.005 & 1 & SYN093-1.010 & 9 \\
SYN093-1.020 & 130 & SYN094-1.005 & $<$1 & SYN094-1.010 & 2 & SYN094-1.020 & 6 & SYN095-1.005 & $<$1 \\
SYN095-1.010 & 2 & SYN095-1.020 & 17 & SYN096-1.005 & $<$1 & SYN096-1.010 & $<$1 & SYN096-1.020 & 2 \\
SYN097-1.005 & 3 & SYN097-1.010 & 33 & SYN097-1.020 & 538 & SYN098-1.005 & 2 & SYN098-1.010 & 6 \\
SYN098-1.020 & 20 & SYN099-1.005 & $<$1 & SYN099-1.010 & 6 & SYN099-1.020 & 52 & SYN100-1.005 & $<$1 \\
SYN100-1.010 & 2 & SYN100-1.020 & 4 & SYN101-1.005 & 5 & SYN101-1.010 & 23 & SYN101-1.020 & 140 \\
SYN102-1.005 & 4 & SYN102-1.010 & 7 & SYN102-1.020 & 16 &  &  &  &  \\
TOP002-2 & $<$1 & TOP004-1 & $<$1 & TOP004-2 & $<$1 & TOP005-2 & $<$1 &  &  \\
SET001-1 & $<$1 & SET002-1 & 31 & SET003-1 & $<$1 & SET004-1 & $<$1 & SET006-1 & $<$1 \\
SET008-1 & 5 & SET009-1 & 3 & SET012-4 & 263 & SET017-6 & 96 & SET017-7 & 221 \\
SET019-3 & 30 & SET019-4 & 24 & SET024-3 & 5 & SET024-4 & 3 & SET024-6 & $<$1 \\
SET024-7 & 2 & SET025-3 & 4 & SET025-4 & 2 & SET025-6 & 2 & SET025-7 & 3 \\
SET027-3 & 583 & SET027-4 & 559 & SET027-6 & 4 & SET027-7 & 4 & SET043-5 & $<$1 \\
SET044-5 & $<$1 & SET045-5 & $<$1 & SET046-5 & $<$1 & SET050-6 & 7 & SET051-6 & 6 \\
SET052-6 & 8 & SET053-6 & 8 & SET054-6 & $<$1 & SET054-7 & $<$1 & SET055-6 & 81 \\
SET055-7 & $<$1 & SET056-6 & 123 & SET056-7 & 127 & SET057-6 & 1 & SET057-7 & 1 \\
SET058-6 & 1 & SET058-7 & 1 & SET059-6 & 1 & SET059-7 & 1 & SET060-6 & 3 \\
SET060-7 & 5 & SET061-6 & 86 & SET061-7 & 10 & SET062-6 & 33 & SET062-7 & 1 \\
SET063-6 & 32 & SET063-7 & 1 & SET064-6 & 133 & SET064-7 & 13 & SET065-6 & $<$1 \\
SET065-7 & 1 & SET072-6 & 197 & SET072-7 & 403 & SET073-6 & 83 & SET073-7 & 2 \\
SET074-6 & 83 & SET074-7 & 2 & SET075-6 & 67 & SET075-7 & 2 & SET077-6 & $<$1 \\
SET077-7 & $<$1 & SET078-6 & 1 & SET078-7 & 1 & SET079-6 & 100 & SET079-7 & 2 \\
SET080-6 & $<$1 & SET080-7 & 1 & SET081-6 & 1 & SET081-7 & 2 & SET082-6 & 138 \\
SET082-7 & 99 & SET083-6 & 133 & SET083-7 & 279 & SET084-6 & 8 & SET084-7 & 46 \\
\end{tabular}
% \end{table}
}
\end{center}

\begin{center}
{\small
% \begin{table}[h] \centering
\begin{tabular}{l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r@{\hspace{.1cm}}|l@{\hspace{.1cm}}r}
\multicolumn{10}{c}{Table 1: TPTP Problem---Seconds to Proof (continued)} \\ \hline
SET085-6 & 158 & SET093-6 & 7 & SET093-7 & 87 & SET094-6 & 107 & SET094-7 & 64 \\
SET095-7 & 2 & SET096-6 & 495 & SET096-7 & 33 & SET101-6 & 2 & SET101-7 & 3 \\
SET102-6 & 2 & SET102-7 & 3 & SET108-6 & 6 & SET108-7 & 41 & SET117-6 & 8 \\
SET117-7 & 62 & SET118-6 & 1 & SET118-7 & 3 & SET146-6 & 159 & SET152-6 & 7 \\
SET158-6 & 1 & SET166-6 & 102 & SET184-6 & 5 & SET196-6 & 135 & SET197-6 & 135 \\
SET203-6 & 1 & SET204-6 & 8 & SET235-6 & 33 & SET236-6 & 34 & SET242-6 & 2 \\
SET296-6 & $<$1 & SET411-6 & 52 & SET479-6 & 185 & SET506-6 & 43 & SET507-6 & 87 \\
SET510-6 & 156 & SET516-6 & 443 & SET517-6 & 491 & SET553-6 & 476 & SET558-6 & 1 \\
SET559-6 & 293 & SET561-6 & 310 & SET562-6 & 427 & SET563-6 & 120 & SET564-6 & 102 \\
SET565-6 & 291 & SET566-6 & 118 &  &  &  &  &  &  \\
\end{tabular}
% \end{table}
}
\end{center}

\bibliographystyle{plain}
\begin{thebibliography}{1}

\bibitem{otter3}
W.~McCune.
\newblock {\sc Otter} 3.0 {R}eference {M}anual and {G}uide.
\newblock Tech. report, Argonne National Laboratory, Argonne, Ill., 1993.

\bibitem{tptp1}
C.B. Suttner, G.~Sutcliffe, and T.~Yemenis.
\newblock {The TPTP Problem Library (TPTP v1.0.0 - TR 13.11.93)}.
\newblock Technical Report FKI-184-93, Institut f{\"u}r Informatik, Technische
  Universit{\"a}t M{\"u}nchen, Munich, Germany; Technical Report 93/11,
  Department of Computer Science, James Cook University, Townsville, Australia,
  1993.

\end{thebibliography}

\end{document}



