On NP ∩ coNP proof complexity generators

Motivated by the theory of proof complexity generators we consider the following Σᵖ₂ search problem DDP determined by a propositional proof system P: given a P-proof $π$ of a disjunction ᵢ αᵢ, no two αᵢ having an atom in common, find i such that αᵢ ∈ TAUT. We formulate a hypothesis (ST) that for some strong proof system P the problem DDP 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 ≠ coNP. The assumption concerns the existence of extensions of models of a bounded arithmetic theory and it is open at present if it holds.