Нижние оценки увеличения сложности выводов после устранения сечений

Обозначим посредством $C_k^*$ формулу
\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}
В работе при всех $k$ построен такой вывод фрмулы $C_k^*$ с сечением, число секвенций в котором линейно зависит от $k$. С другой стороны, нельзя оценить сверху элементарной по Кальмару функцией от $k$ как число секвенций в любом выводе формулы $C_k^*$ без сечений, так и число дизъюнктов в опровержении по методу резолюций системы дизъюнктов, соответствующей отрицанию формулы $C_k^*$. В частности, можно построить такой вывод с сечением формулы $C_6^*$, в котором содержится не более 253 секвенций, но при поиске вывода формулы $C_k^*$ по методу резолюций необходимо построить более $10^{19200}$ дизъюнктов.
С помощью сколемизации и вынесения кванторов по формуле $C_k^*$ построена формула $\exists v_0 B_k^+(v_0)$, которая удовлетворяет следующим условиям:
1) можно построить такой вывод с сечениями формулы $\exists v_0 B_k^+(v_0)$ в конструктивном исчислении предикатов, число секвенций в котором линейно зависит от $k$;
2) нельзя оценить сверху элементарной по Кальмару функцией от $k$ длину такого терма $t$, что формула $B_k^+(t)$ выводима. Библ. – 11 назв.