$F_d$ versus $F_{d+1}$: a fixed depth $k$ separating all consecutive levels

There is a constant $k$ such that for every $d\ge k$ there is a family $(\tau_m)_{m\in\mathbb N}$ of tautologies of depth at most $k$ with $|\tau_m|\ge m$ such that

1. (quasi-polynomial upper bound) for some $C$, each $\tau_m$ has an $F_{d+1}$-proof of size at most $2^{C(\log_2|\tau_m|)^{C}}$;
2. (exponential lower bound) for some $\varepsilon>0$ and all sufficiently large $m$, every $F_d$-proof of $\tau_m$ has size at least $2^{|\tau_m|^{\varepsilon}}$.

In symbols:

This is Krajíček's open problem: one extra level of proof depth gives an exponential speed-up already on tautologies of one fixed depth.

Formalization Note The problem says "for any $d$"; since a depth-$k$ formula has no $F_{d+1}$-proof when $d+1<k$, the statement is taken for $d\ge k$. The problem allows a polynomial or quasi-polynomial upper bound; the goal uses the weaker (quasi-polynomial) one, so a polynomial solution also proves it.