On $NP\cap coNP$ proof complexity generators

Motivated by the theory of proof complexity generators we consider the following ${\mathrm{\Sigma }}_2^p$ search problem $D{D}_P$ determined by a propositional proof system $P$: given a $P$-proof $\pi$ of a disjunction ${\bigvee }_i{\alpha }_i$, no two ${\alpha }_i$ having an atom in common, find $i$ such that ${\alpha }_i\in TAUT$. We formulate a hypothesis (ST) that for some strong proof system $P$ the problem $D{D}_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\mathrm{\ne }coNP$. The assumption concerns the existence of extensions of models of a bounded arithmetic theory and it is open at present if it holds.