We prove in this paper that there is 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 by any ${\rm co}\mathcal{NP}$ machines. Then we further show that $L_s$ is in $\mathcal{NP}$, thus proving that $$\mathcal{NP}\neq{\rm co}\mathcal{NP}.$$ The main techniques used in this paper are simulation and the novel new techniques developed in the author's recent work. Our main result has profound implications, such as $\mathcal{P}\neq\mathcal{NP}$, etc. Further, if there exists some oracle $A$ such that $\mathcal{P}^A\ne\mathcal{NP}^A={\rm co}\mathcal{NP}^A$, we then explore what mystery lies behind it and show that if $\mathcal{P}^A\ne\mathcal{NP}^A={\rm co}\mathcal{NP}^A$ and under some rational assumptions, then the set of all ${\rm co}\mathcal{NP}^A$ machines is not enumerable, thus showing that the simulation techniques are not applicable for the first half of the whole step to separate $\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).

翻译：本文证明存在一种语言$L_s$，它可由某个非确定性图灵机在$O(n^k)$时间内接受（其中$k$为任意正整数$k\\in\\mathbb{N}_1$），但无法被任何${\\rm co}\\mathcal{NP}$机器接受。进一步我们证明$L_s$属于$\\mathcal{NP}$，从而证明$$\\mathcal{NP}\\neq{\\rm co}\\mathcal{NP}$$。本文采用的主要技术包括模拟方法以及作者近期工作中提出的创新技术。我们的主要结果具有深远影响，例如可推导出$\\mathcal{P}\\neq\\mathcal{NP}$等结论。此外，若存在预言机$A$使得$\\mathcal{P}^A\\ne\\mathcal{NP}^A={\\rm co}\\mathcal{NP}^A$，我们探究其背后的奥秘并证明：在$\\mathcal{P}^A\\ne\\mathcal{NP}^A={\\rm co}\\mathcal{NP}^A$及某些合理假设下，所有${\\rm co}\\mathcal{NP}^A$机器的集合不可枚举，这表明模拟技术无法应用于分离$\\mathcal{NP}^A$与${\\rm co}\\mathcal{NP}^A$全过程的前半阶段。最后，本文给出了Frege证明系统的下界结果（即不存在多项式有界的Frege证明系统）。