A method based on superposition on maximal literals in clauses and conditional rewriting is discussed for automatically proving theorems in first-order predicate calculus with equality. First-order formulae (clauses) are represented as conditional rewrite rules which turn out to be an efficient representation. The use of conditional rewriting for reducing search space is discussed. The method has been implemented in RRL, a Rewrite Rule Laboratory, a theorem proving environment based on rewriting techniques. It has been tried on a number of examples with considerable success. Its performance on bench-mark examples, including Schubert's Steamroller problem, SAM's lemma, and examples from set theory, compared favorably with the performance of other methods reported in the literature.