{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreig63ubowxeofqsmatv5o7cg26y3bbyy5hddqbzhf5gfrh7y3pqs2q",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mlzlfvgplb52"
  },
  "path": "/report/2026/078",
  "publishedAt": "2026-05-17T03:11:22.000Z",
  "site": "https://eccc.weizmann.ac.il",
  "textContent": "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 \\exp\\bigl(n^{1-\\varepsilon}\\bigr)$ 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)$.",
  "title": "TR26-078 |  Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size | \n\n\tSusanna F. de Rezende, \n\n\tDavid Engström, \n\n\tYassine Ghannane, \n\n\tKilian Risse"
}