We have recently heard rumors that researchers are again studying paramodulation [Wos87] in the context of strategy for its control.
In part to facilitate such research, and in part to provide test problems for evaluating other approaches to equality-oriented reasoning, we offer in this article a set of benchmark problems in which equality plays the dominant role.
The test problems are taken from group theory, ring theory, Robbins algebra, combinatory logic, and other areas.
For each problem, we include appropriate clauses and comment as to its status with regard to provability by an unaided automated reasoning program.
To complement the test problems, we offer various open questions.