\contentsline {section}{\numberline {1}Introduction}{2}
\contentsline {section}{\numberline {2}Getting Started}{3}
\contentsline {section}{\numberline {3}Calculus and Proof Procedure}{3}
\contentsline {subsection}{\numberline {3.1}Calculus}{4}
\contentsline {subsection}{\numberline {3.2}Preprocessing}{8}
\contentsline {subsubsection}{\numberline {3.2.1}Axiom Filtering}{8}
\contentsline {subsubsection}{\numberline {3.2.2}Clausification}{10}
\contentsline {subsubsection}{\numberline {3.2.3}Equational Definition unfolding}{10}
\contentsline {subsubsection}{\numberline {3.2.4}Presaturation Interreduction}{10}
\contentsline {subsection}{\numberline {3.3}Proof Procedure}{11}
\contentsline {section}{\numberline {4}Controlling the Proof Search}{11}
\contentsline {subsection}{\numberline {4.1}Search Control Heuristics}{11}
\contentsline {subsubsection}{\numberline {4.1.1}Priority functions}{13}
\contentsline {subsubsection}{\numberline {4.1.2}Generic Weight Functions}{15}
\contentsline {subsubsection}{\numberline {4.1.3}Clause Evaluation Functions}{16}
\contentsline {subsubsection}{\numberline {4.1.4}Heuristics}{17}
\contentsline {subsection}{\numberline {4.2}Term Orderings}{18}
\contentsline {subsubsection}{\numberline {4.2.1}Precedence Generation Schemes}{20}
\contentsline {subsubsection}{\numberline {4.2.2}Weight Generation Schemes}{21}
\contentsline {subsection}{\numberline {4.3}Literal Selection Strategies}{22}
\contentsline {subsection}{\numberline {4.4}The Watchlist Feature}{23}
\contentsline {subsection}{\numberline {4.5}Learning Clause Evaluation Functions}{24}
\contentsline {subsubsection}{\numberline {4.5.1}Creating Knowledge Bases}{24}
\contentsline {subsubsection}{\numberline {4.5.2}Populating Knowledge Bases}{25}
\contentsline {subsubsection}{\numberline {4.5.3}Using Learned Knowledge}{25}
\contentsline {subsection}{\numberline {4.6}Other Options}{25}
\contentsline {section}{\numberline {5}Input Language}{25}
\contentsline {subsection}{\numberline {5.1}LOP}{25}
\contentsline {subsection}{\numberline {5.2}TPTP Format}{26}
\contentsline {section}{\numberline {6}Output\ldots or how to interpret what you see}{27}
\contentsline {subsection}{\numberline {6.1}The Bare Essentials}{27}
\contentsline {subsection}{\numberline {6.2}Impressing your Friends}{28}
\contentsline {subsection}{\numberline {6.3}Detailed Reporting}{28}
\contentsline {subsection}{\numberline {6.4}Requesting Specific Output}{29}
\contentsline {section}{\numberline {A}License}{31}
