Fingerprint Indexing for Paramodulation and Rewriting
                        Stephan Schulz

Indexing is critical for the performance of first-order theorem
provers. We introduce \emph{fingerprint indexing}, a non-perfect
indexing technique that is based on short, constant length vectors
of samples of term positions (``fingerprints'') organized in a
trie. Fingerprint indexing supports matching and unification as
retrieval relations. The algorithms are simple, the indices are
small, and performance is very good in practice.

We demonstrate the performance of the index both in relative and
absolute terms using large-scale profiling.