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
  practical adoption, and to the best of our knowledge there is no
  tableau-based theorem prover that uses rigid E-unification. We introduce
  simultaneous bounded rigid E-unification (BREU), a new version of rigid
  E-unification that is bounded in the sense that variables only represent
  terms from finite domains. We show that (simultaneous) BREU is
  NP-complete, outline how 
  BREU problems can be encoded as propositional SAT-problems, and use
  BREU to introduce a sound and complete sequent calculus for
  first-order logic with equality.