Lower bounds for lengthening of proofs after cut-elimination

Let $C_k^*$ be the formula
\begin{align} \forall b_0((\forall w_0\exists v_0 P(w_0,b_0,v_0) &\&\forall uvw(\exists y(P(y,b_0,u)\&\exists z(P(v,y,z)\notag\\ &\& P(z,y,w)))\supset P(v,u,w)))\supset\exists v_k(P(b_0,b_0,v_k)\notag\\ &\&\exists v_{k+1}(P(b_0,v_k,V_{k-1})\&\dots\exists v_0 P(b_0,v_1,v_0)\dots))).\notag \end{align}
and let $LK$ be the Gentzen system for classical predicate calculus. Given a sequent calculus $\mathfrak P$ let $\mathfrak P\vdash_nS$ mean that $S$ has a proof in $\mathfrak P$ of at most $n$, sequent occurrences.
The main aim of the paper is to show that
(a) there is a linear function $l$ such that $LK\vdash_{l(k)}C_k^*$,
(b) there is no Kalmar elementary function $f$ with $(LK-\operatorname{cut})\vdash_{f(k)}C_k^*$.
In particular $LK\vdash_{253}C_6^*$ but $\rceil C_6^*$ does not have a refutation in resolution method with less than $10^{19200}$ clauses.