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$决定的以下$Σ^p_2$搜索问题$\mbox{DD}_P$：给定一个$P$证明$π$，其结论是析取式$\bigvee_i α_i$，且任意两个$α_i$不共享原子变元，寻找一个使得$α_i \in \mbox{TAUT}$的$i$。我们提出一个假设(ST)：对于某个强证明系统$P$，问题$\mbox{DD}_P$在师生模型（学生为p-时间，轮数为常数）中不可解。该假设源于存在难解单向置换。利用一个模型论假设，我们证明(ST)蕴含$NP \neq coNP$。该假设涉及有界算术理论模型扩展的存在性，目前其是否成立尚属开放问题。