  This paper proves Buss's hierarchy of bounded arithmetics $S^1_2 \subseteq
S^2_2 \subseteq \cdots \subseteq S^i_2 \subseteq \cdots$ does not entirely
collapse. More precisely, we prove that, for a certain $D$, $S^1_2 \subsetneq
S^{2D+5}_2$ holds. Further, we can allow any finite set of true quantifier free
formulas for the BASIC axioms of $S^1_2, S^2_2, \ldots$. By Takeuti's argument,
this implies $\mathrm{P} \neq \mathrm{NP}$. Let $\mathbf{Ax}$ be a certain
formulation of BASIC axioms. We prove that $S^1_2 \not\vdash
\mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$ for sufficiently large $D$,
while $S^{2D+7}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$ for a
system $\mathrm{PV}^-_1(D)$, a fragment of the system $\mathrm{PV}^-_1$,
induction free first order extension of Cook's $\mathrm{PV}$, of which proofs
contain only formulas with less than $D$ connectives. $S^1_2 \not\vdash
\mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$ is proved by straightforward
adaption of the proof of $\mathrm{PV} \not\vdash \mathrm{Con}(\mathrm{PV}^-)$
by Buss and Ignjatovi\'c. $S^{2D+5}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_1(D) +
\mathbf{Ax})$ is proved by $S^{2D+7}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_q(D+2)
+ \mathbf{Ax})$, where $\mathrm{PV}^-_q$ is a quantifier-only extension of
$\mathrm{PV}^-$. The later statement is proved by an extension of a technique
used for Yamagata's proof of $S^2_2 \vdash \mathrm{Con}(\mathrm{PV}^-)$, in
which a kind of satisfaction relation $\mathrm{Sat}$ is defined. By extending
$\mathrm{Sat}$ to formulas with less than $D$-quantifiers, $S^{2D+3}_2 \vdash
\mathrm{Con}(\mathrm{PV}^-_q(D) + \mathbf{Ax})$ is obtained in a
straightforward way.
