Separation of $F_{d+1}$ from $F_d$ by depth-$d$ tautologies

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

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

This is the case of the problem in which the depth $k$ of the tautologies may depend on $d$ (with $k=d$), recorded as known on the Open Problem Garden page.

Formalization Note The statement is asked only for all sufficiently large $d$, to be robust to the offset between depth conventions (here literals have depth $0$; in this convention the statement fails for $d=1$, since depth-1 tautologies have linear-size $F_1$-proofs).