The efficient integration of theory reasoning in first-order calculi
  with free variables (such as sequent calculi or tableaux) is a
  long-standing challenge. For the case of the theory of equality, an
  approach that has been extensively studied in the 90s is rigid
  E-unification, a variant of equational unification in which the
  assumption is made that every variable denotes exactly one term
  (rigid semantics). The fact that simultaneous rigid E-unification is
  undecidable, however, has hampered practical adoption of the method,
  and today there are few theorem provers that use rigid
  E-unification.

  One solution is to consider incomplete algorithms for computing
  (simultaneous) rigid E-unifiers, which can still be sufficient to
  create sound and complete theorem provers for first-order logic with
  equality; such algorithms include rigid basic superposition proposed
  by Degtyarev and Voronkov, but also the much older subterm
  instantiation approach introduced by Kanger in 1963 (later also
  termed minus-normalisation). We introduce bounded rigid E-unification (BREU)
  as a new variant of E-unification corresponding to subterm instantiation. In
  contrast to general rigid E-unification, BREU is NP-complete for 
  individual and simultaneous unification problems, and can be solved
  efficiently with the help of SAT; BREU can be combined with
  techniques like congruence closure for ground reasoning, and be used
  to construct theorem provers that are competitive with
  state-of-the-art tableau systems. We outline ongoing research how
  BREU can be generalised to other theories than equality.