\indexentry{SETHEO}{2}
\indexentry{Otter}{2}
\indexentry{SPASS}{2}
\indexentry{Vampire}{2}
\indexentry{xyzzy}{3}
\indexentry{TPTP!language}{3}
\indexentry{terms}{4}
\indexentry{variables}{4}
\indexentry{subterm}{4}
\indexentry{equations}{4}
\indexentry{literal}{4}
\indexentry{ordering}{4}
\indexentry{reduction ordering}{4}
\indexentry{selection functions}{4}
\indexentry{literals!eligible}{5}
\indexentry{eligible for paramodulation|see{literals, eligible}}{5}
\indexentry{eligible for resolution|see{literals, eligible}}{5}
\indexentry{eligible literals|see{literals, eligible}}{5}
\indexentry{literals!eligible}{5}
\indexentry{SP@\textbf{SP} (calculus)}{5}
\indexentry{equality resolution}{5}
\indexentry{superposition!inference rule}{5}
\indexentry{superposition!inference rule}{6}
\indexentry{equality factoring}{6}
\indexentry{rewriting}{6}
\indexentry{rewriting}{6}
\indexentry{subsumption}{6}
\indexentry{subsumption}{6}
\indexentry{E (theorem prover)}{6}
\indexentry{SPASS}{6}
\indexentry{simplify-reflect}{7}
\indexentry{simplify-reflect}{7}
\indexentry{contextual simplify-reflect}{7}
\indexentry{tautology deletion}{7}
\indexentry{equality      resolution}{7}
\indexentry{clause splitting}{8}
\indexentry{clause splitting}{8}
\indexentry{DISCOUNT}{8}
\indexentry{SPASS}{8}
\indexentry{relevancy pruning}{8}
\indexentry{SInE}{9}
\indexentry{TPTP}{9}
\indexentry{clausification}{10}
\indexentry{TPTP!language}{10}
\indexentry{equational definition}{10}
\indexentry{interreduction}{10}
\indexentry{given clause}{11}
\indexentry{term   ordering}{11}
\indexentry{literal!selection}{11}
\indexentry{term ordering}{11}
\indexentry{given clause}{11}
\indexentry{literal!selection}{11}
\indexentry{proof procedure}{12}
\indexentry{clause evaluation}{16}
\indexentry{term ordering}{18}
\indexentry{literal!selection}{22}
\indexentry{LOP}{24}
\indexentry{TPTP!language}{24}
\indexentry{LOP}{25}
\indexentry{SETHEO}{25}
\indexentry{SETHEO}{26}
\indexentry{TPTP}{26}
\indexentry{TPTP!language}{26}
\indexentry{PCL}{27}
\indexentry{Otter}{28}
\indexentry{PCL}{28}
\indexentry{TPTP!language}{28}
\indexentry{GPL}{31}
\indexentry{GNU General Public     License}{31}
\indexentry{LGPL}{31}
\indexentry{GNU Lesser General Public License}{31}
