Can you help me understand the class of problems solvable by a nondetermimistic Turing machine with an oracle for SAT running in polynomial time?