We prove superpolynomial length lower bounds for the semantic tree-like Frege refutation system with bounded line size. Concretely, for any function $n^{2-\varepsilon} \leq s(n) \leq 2^{n^{1-\varepsilon}}$ we exhibit an explicit family $\mathcal{A}$ of $n$-variate CNF formulas $A$, each of size $|A| \le s(n)^{1+\varepsilon}$, such that if $A$ is chosen uniformly from $\mathcal{A}$, then asymptotically almost surely any tree-like Frege refutation of $A$ in line-size $s(n)$ is of length super-polynomial in $|A|$. Our lower bounds apply also to tree-like degree-$d$ threshold systems, for $d \approx \log\bigl(s(n)\bigr)$, that is, for $d$ up to $n^{1-\varepsilon}$. More generally, our lower bounds apply to the semantic version of these systems and to any semantic tree-like proof system where the number of distinct lines is bounded by $\exp\bigl(s(n)\bigr)$.

翻译：我们证明了带限行大小的树状语义弗雷格反驳系统的超多项式长度下界。具体而言，对于任意函数 $n^{2-\varepsilon} \leq s(n) \leq 2^{n^{1-\varepsilon}}$，我们构造一个显式的 $n$ 元 CNF 公式族 $\mathcal{A}$（每个公式 $A$ 的大小 $|A| \le s(n)^{1+\varepsilon}$），使得当 $A$ 从 $\mathcal{A}$ 中均匀随机选取时，渐近几乎必然地，任何行大小不超过 $s(n)$ 的树状弗雷格反驳 $A$ 的长度关于 $|A|$ 是超多项式的。我们的下界同样适用于 $d \approx \log\bigl(s(n)\bigr)$（即 $d$ 可达 $n^{1-\varepsilon}$）的树状 $d$ 次阈值系统。更一般地，我们的下界适用于这些系统的语义版本以及任何不同行数目不超过 $\exp\bigl(s(n)\bigr)$ 的树状语义证明系统。