Is the validity of some instance of an equational problem decidable?

Is the following FOL-problem (equality is a logical symbol)
effectively decidable?

Given. A finite equation system $E$ and an equation $s = t$.

Question. Is there a substitution $\sigma$, such that $\sigma(E)
\models \sigma(s = t)$?

Some useful information.

-
Obviously one can restrict $\sigma$ to be a ground substitution.

-
This problem is decidable: Given a finite system $E$ of

ground equations and a ground equation $s = t$, does $E \models s = t$

hold? (c.f. [1: Corollary 4.3.6])

References

[1] Franz Baader, Tobias Nipkow: Term Rewriting and All That,
© 1998 Cambridge University Press.

This problem is known as rigid E-unification. This problem is NP-complete. The first proof was given by Gallier, Narendran, Plaisted and Snyder [1].

However a related problem, the Simultaneous rigid E-unification that is to find a substitution that simultaneously satisfies several instances of rigid E-unification is undecidable. This result was proved by Degtyarev and Voronkov [2].

References

-
Jean H. Gallier, Paliath Narendran, David A. Plaisted, Wayne Snyder: Rigid E-Unification: NP-Completeness and Applications to Equational Matings Inf. Comput. 87(1/2): 129-195 (1990)

-
Anatoli Degtyarev, Andrei Voronkov: The Undecidability of Simultaneous Rigid E-Unification. Theor. Comput. Sci. 166(1&2): 291-300 (1996)

StackExchange Computer Science Q#3312, answer score: 8