Stephan Schulz and Maria Paola Bonacina:
"On Handling  Distinct Objects in the Superposition Calculus"

Abstract:

  Many domains of reasoning include a set of distinct objects. For
  general-purpose automated theorem provers, this property has to be
  specified explicitly, by including distinctness axioms. Since their
  number grows quadratically with the number of distinct objects, this
  results in large and clumsy specifications, that may affect
  performance adversely.  We show that object distinctness can be
  handled directly by a modified superposition-based inference system,
  including additional inference rules. The new calculus is shown to
  be sound and complete. A preliminary implementation shows promising
  results in the theory of arrays.