Consider the following decision problem:
Given: Two (3CNF-)formulas $\varphi_1$, $\varphi_2$ on a shared set $X\cup Y$ of variables ($X$ and $Y$ disjoint).
Question: $\exists$ assignment $\tau_X$ on $X$ such that $\varphi_1$ is satisfiable and $\varphi_2$ is unsatisfiable?
(The "satisfiable" and "unsatisfiable" conditions are relative to the fixed assignment $\tau_X$ from the outer quantifier and can only "choose" the assignment to variables in $Y$.)
This problem is a generalization of the well-known 3-SAT/3-UNSAT problem, which is DP-complete:
Given: Two (3CNF-)formulas $\varphi_1$, $\varphi_2$ on a set $Y$ of variables.
Question: Is $\varphi_1$ satisfiable and $\varphi_2$ unsatisfiable?
The generalization works in the same way in which the NP-complete problem 3-SAT is generalized for higher levels of the polynomial hierarchy. In fact, if the formula $\varphi_1$ and the corresponding condition is removed, this problem coincides with the $\Sigma_2^p$-complete variant of 3-SAT:
Given: A (3CNF-)formula $\varphi_2$ on a set $X\cup Y$ of variables ($X$ and $Y$ disjoint).
Question: $\exists$ assignment $\tau_X$ on $X$ such that $\varphi_2$ is unsatisfiable?
Now I wonder how to call the complexity class that this problem is a member of (and probably complete for). It seems to be $\textit{NP}^{\textit{DP}}$, i.e., $\textit{NP}$ with access to a $\textit{DP}$ oracle, in the same way that $\Sigma_2^p=\textit{NP}^{\textit{coNP}}$ is $\textit{NP}$ with access to a $\textit{coNP}$ oracle. However, I have not found such a class in the literature. Is the problem simply too unnatural to receive any attention? Or can it be simplified such that it falls into another, more common class?
