Pudlák's conjecture on non-simulation of consistency extensions

Let $\mathcal S$ be the base arithmetic theory under consideration, and let $Con_{\mathcal S}(n)$ denote its bounded consistency statement at length $n$. Write $\mathcal S\centernot{\sststile{}{n^c}}\varphi(n)$ to mean that $\mathcal S$ does not have proofs of $\varphi(n)$ of size bounded by $n^c$. Pudlák's conjecture. For every constant $c$,

$$\mathcal S\centernot{\sststile{}{n^c}}Con_{\mathcal S+Con_{\mathcal S}}(n).$$

This conjecture asserts that adjoining the consistency statement of $\mathcal S$ produces an extension that $\mathcal S$ cannot simulate with any fixed polynomial proof-size bound. The surrounding discussion presents it as a benchmark non-simulation case and notes that it would also imply non-simulation for suitable soundness extensions, but no resolution is given.