Complexity class for NP with access to a DP oracle 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 &quot;satisfiable&quot; and &quot;unsatisfiable&quot; conditions are relative to the fixed assignment $\tau_X$ from the outer quantifier and can only &quot;choose&quot; 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?
You have not found explicit mention of it because it is the same class as $\Sigma_2 = \textbf{NP}^\textbf{NP}$. $\Sigma_2 \subseteq \textbf{NP}^\text{DP}$ holds because any $\textbf{NP}$ query can be poly-time (many-one) reduced to a SAT query, which, in turn, can be cast as a DP query (by setting $\varphi_2$ to a trivially unsatisfiable formula). Conversely, $\Sigma_2 \supseteq \textbf{NP}^\text{DP}$ because any DP query can be answered by two (adaptive) SAT queries.