As stated in [1]}, given an
epistemic guess \(\Phi \)  and an ELP \(\Pi \) , verifying that \(\Pi \)  has a CWV
w.r.t. \(\Phi \)  can be done in \(D_{\mathit {2}}^{\mathit {P}}\) , and hence via two calls to a
\(\Sigma _{\mathit {2}}^{\mathit {P}}\)  oracle. We therefore obtain a straightforward guess-and-check
algorithm that runs in non-deterministic polynomial time with a \(\Sigma _{\mathit {2}}^{\mathit {P}}\)  oracle, checks non-uniform equivalence between two ELPs, and works as follows:
guess a set of atoms \(D \subseteq \mathcal {A}\) , an epistemic guess \(\Phi \subseteq \mathcal {E}\) , and a set of facts \(M \subseteq \mathcal {A}\) . Then, use a
\(\Sigma _{\mathit {2}}^{\mathit {P}}\) -oracle to check that one of the following two conditions hold:
(i) \(\Phi \)  leads to a CWV for \(\Pi _1 \cup D\) , but not for \(\Pi _2 \cup D\) , or
(ii) \(\Phi \)  leads to a CWV for both \(\Pi _1 \cup D\)  and \(\Pi _2 \cup D\) , but
that \(M\)  is an answer set that exists only in exactly one of these two CWVs.
