Tradeoffs in propositional proof complexity typically involve two parameters (e.g., size, width, depth) and exhibit a CNF for which both of these parameters can be made small separately, but keeping one parameter small necessarily makes the other parameter big. Typically, the lower bound on the other parameter is close to the trivial upper bound on that parameter.
In a supercritical tradeoff, keeping one parameter small implies a lower bound on the other parameter which is significantly larger than the trivial upper bound. The first such supercritical tradeoff for resolution was exhibited by Razborov, for the parameters width and tree-size. Since then there has been active research on finding more supercritical tradeoffs.
We shall describe the first supercritical tradeoff found by Razborov: there exists a CNF which has a refutation of width k, but any tree-like refutation of width $n^{1-epsilon}/k$ must have size $exp(n^k)$. (The trivial upper bound for tree-like size is $exp(n)$)
