Given two theories $T_1$ and $T_2$ with disjoint-signatures $Σ_1$ and $Σ_2$ respectively, and a conjunction of literals $φ$ over $Σ_1 \cup Σ_2$, we want to decide if $φ$ is satisfiable under $T1∪T2$. Nelson and Oppen [G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures] provided a method for combining the satisfiability procedures for $T_1$ and $T_2$ to produce a satisfiability procedure for $T_1 \cup T_2$.
However, Nelson-Oppen is: solely applicable to (disjoint-signature) quantifier-free theories. Thus, are we referring to those theories that admit quantifier elimination (i.e., they does this mean decidable)?
I ask because 'quantifier-free' sounds to me like quantifiers will not be accepted in the signature.