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.
Jan Krajicek (Wed,) studied this question.