Simple and Efficient Clause Subsumption with Feature Vector Indexing 
                        Stephan Schulz
                      schulz@eprover.org

This paper describes feature vector indexing, a new, non-perfect
indexing method for clause subsumption. It is suitable for both
forward (i.e., finding a subsuming clause in a set) and backward
(finding all subsumed clauses in a set) subsumption. Moreover, it is
easy to implement, but still yields excellent performance in
practice. As an added benefit, by restricting the selection of
features used in the index, our technique immediately adapts to
indexing modulo arbitrary AC theories with only minor loss of
efficiency. Alternatively, the feature selection can be restricted to
result in set subsumption.  Feature vector indexing has been
implemented in our equational theorem prover E, and has enabled us to
integrate new simplification techniques making heavy use of
subsumption. We experimentally compare the performance of the prover
for a number of strategies using feature vector indexing and
conventional sequential subsumption.