Rigid E-unification is the problem of unifying two expressions modulo a set
  of equations, with the assumption that every variable denotes
  exactly one term (rigid semantics). This form of unification
  was originally developed as an approach to integrate equational
  reasoning in tableau-like proof procedures, and studied extensively
  in the late 80s and 90s. However, the fact that simultaneous
  rigid E-unification is undecidable has limited the practical relevance of
  the method, and to the best of our knowledge there is no
  tableau-based theorem prover that uses rigid E-unification. We recently
  introduced a new decidable variant of (simultaneous) rigid E-unification, bounded
  rigid E-unification (BREU), in which variables only represent terms from
  finite domains, and used it to define a first-order logic
  calculus. In this paper, we study the problem of computing solutions
  of (individual or simultaneous) BREU problems. Two new unification
  procedures for BREU are introduced, and compared theoretically and
  experimentally.