We prove in this paper that there exists a language $L_s$ accepted by some nondeterministic Turing machine that runs within time $O(n^k)$ for any positive integer $k\in\mathbb{N}_1$ but not accepted by any ${\rm co}\mathcal{NP}$ machines. We further show that $L_s$ is in $\mathcal{NP}$, thereby proving the groundbreaking result that $$\mathcal{NP}\neq{\rm co}\mathcal{NP}. $$ The main techniques used in this paper are simulation together with the novel techniques developed in the author's recent work. Our main result has profound implications, such as $\mathcal{P}\neq\mathcal{NP}$. Furthermore, if there exists some oracle $A$ such that $\mathcal{P}^A\ne\mathcal{NP}^A={\rm co}\mathcal{NP}^A$, we explore the underlying reasons and show that, under this condition and some reasonable assumptions, the set of all ${\rm co}\mathcal{NP}^A$ machines is not enumerable. This implies that simulation techniques cannot be applied to the first part of the separation of $\mathcal{NP}^A$ from ${\rm co}\mathcal{NP}^A$. Finally, a lower bounds result for Frege proof systems is presented (i.e., no Frege proof systems can be polynomially bounded).

翻译：暂无翻译