Stephan Schulz: Empirical Properties of Term Orderings for Superposition 

Term orderings play a critical role in most modern automated theorem
proving systems, in particular for systems dealing with equality. In
this paper we report on a set of experiments with the superposition
theorem prover E, comparing the performance of the system under
Knuth-Bendix Ordering and Lexicographic Path Ordering with a number of
different precedence and weight generation schemes. Results indicate
that relative performance under a short time limit seems to be a good
predictor for longer run times and that KBO generally outperforms
LPO. Also, if other strategy elements (especially clause selection)
are independent of the ordering, performance of a given ordering
instance with one strategy is a decent predictor of performance with a
different strategy.