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])
 Franz Baader, Tobias Nipkow: Term Rewriting and All That, © 1998 Cambridge University Press.