一句话：提出由证明系统定义的 Σ₂ᵖ 搜索问题 DD_P 与假设 (ST)，并在模型论假设下证明它蕴含 NP≠coNP。
论文受证明复杂度生成器理论启发，研究由命题证明系统 P 决定的 Σ₂ᵖ 搜索问题 DD_P：给定无公共原子的析取式 ∨_i α_i 的 P-证明，要求找出 i 使 α_i ∈ TAUT。作者提出假设 (ST)：存在某个强证明系统 P，使 DD_P 无法在学生-教师模型中以 p 时间学生和常数轮求解；该假设可由难解单向置换的存在性推出。作者进一步借助一个关于有界算术理论模型扩张的模型论假设，证明 (ST) 蕴含 NP ≠ coNP。该模型论假设目前尚未解决，因此工作把证明复杂度的不可解性假设与 NP 对 coNP 分离问题联系起来。
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.