Motivated by the theory of proof complexity generators we consider the following $Σ^p_2$ search problem $\mbox{DD}_P$ determined by a propositional proof system $P$: given a $P$-proof $π$ of a disjunction $\bigvee_i α_i$, no two $α_i$ having an atom in common, find $i$ such that $α_i \in \mbox{TAUT}$. We formulate a hypothesis (ST) that for some strong proof system $P$ the problem $\mbox{DD}_P$ is not solvable in the student-teacher model with a p-time student and a constant number of rounds. The hypothesis follows from the existence of hard one-way permutations. We prove, using a model-theoretic assumption, that (ST) implies $NP \neq coNP$. The assumption concerns the existence of extensions of models of a bounded arithmetic theory and it is open at present if it holds.

翻译：受证明复杂度生成器理论的启发，我们考虑由命题证明系统 $P$ 确定的如下 $\Sigma^p_2$ 搜索问题 $\mbox{DD}_P$：给定一个 $P$-证明 $\pi$，其结论为析取式 $\bigvee_i α_i$，且任意两个 $α_i$ 无公共原子，求 $i$ 使得 $α_i \in \mbox{TAUT}$。我们提出一个假设 (ST)：存在某个强证明系统 $P$，使得问题 $\mbox{DD}_P$ 在师生模型（其中学生为 p-时间算法，且轮次为常数）下不可解。该假设源于困难单向置换的存在性。我们利用一个模型论假设证明，(ST) 蕴含 $NP \neq coNP$。该假设涉及有界算术理论模型的扩张存在性，目前尚不清楚其是否成立。