A crucial way for reducing the search space in automated deduction are the so-called
selection strategies: in each clause, the subset of
selected literals are the only ones involved in inferences.
For first-order Horn clauses without equality, resolution is complete with an arbitrary selection of one single literal in
each clause [dN96].
For Horn clauses with built-in equality, i.e., paramodulation-based inference systems, the situation is far more complex.
Here we show that if a paramodulation-based inference system is complete with eager selection of negative equations and, moreover,
it is compatible with equality constraint inheritance, then it is complete with arbitrary selection strategies. A first important
application of this result is the one for paramodulation wrt. non-monotonic orderings, which was left open in [BGNR99].
Keywords automated deduction