\begin{theindex}

  \item clause evaluation, 16
  \item clause splitting, 8
  \item clausification, 10
  \item contextual simplify-reflect, 7

  \indexspace

  \item DISCOUNT, 8

  \indexspace

  \item E (theorem prover), 6
  \item eligible for paramodulation, \see{literals, eligible}{5}
  \item eligible for resolution, \see{literals, eligible}{5}
  \item eligible literals, \see{literals, eligible}{5}
  \item equality      resolution, 7
  \item equality factoring, 6
  \item equality resolution, 5
  \item equational definition, 10
  \item equations, 4

  \indexspace

  \item given clause, 11
  \item GNU General Public     License, 31
  \item GNU Lesser General Public License, 31
  \item GPL, 31

  \indexspace

  \item interreduction, 10

  \indexspace

  \item LGPL, 31
  \item literal, 4
    \subitem selection, 11, 22
  \item literals
    \subitem eligible, 5
  \item LOP, 24, 25

  \indexspace

  \item ordering, 4
  \item Otter, 2, 28

  \indexspace

  \item PCL, 27, 28
  \item proof procedure, 12

  \indexspace

  \item reduction ordering, 4
  \item relevancy pruning, 8
  \item rewriting, 6

  \indexspace

  \item selection functions, 4
  \item SETHEO, 2, 25, 26
  \item simplify-reflect, 7
  \item SInE, 9
  \item \textbf{SP} (calculus), 5
  \item SPASS, 2, 6, 8
  \item subsumption, 6
  \item subterm, 4
  \item superposition
    \subitem inference rule, 5, 6

  \indexspace

  \item tautology deletion, 7
  \item term   ordering, 11
  \item term ordering, 11, 18
  \item terms, 4
  \item TPTP, 9, 26
    \subitem language, 3, 10, 24, 26, 28

  \indexspace

  \item Vampire, 2
  \item variables, 4

  \indexspace

  \item xyzzy, 3

\end{theindex}
