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$：给定一个析取式$\bigvee_i α_i$的$P$证明$π$（其中任意两个$α_i$不共享原子命题），寻找满足$α_i \in \mbox{TAUT}$的索引$i$。我们提出一个假设（ST）：对于某个强证明系统$P$，问题$\mbox{DD}_P$在具有多项式时间学生和常数轮次的学生-教师模型中不可解。该假设可由硬单向置换的存在性推导得出。通过使用一个模型论假设，我们证明（ST）蕴含$NP \neq coNP$。该模型论假设涉及有界算术理论模型的扩张存在性，其是否成立目前尚未解决。