We establish a collection of new size lower bounds against fairly strong algebraic-Boolean propositional proof systems, from depth-3 semantic polynomial calculus for CNFs, up to semantic $AC^0[2]$-Frege in the regime of deep formulas, as follows:

(1) $\Sigma\Pi\Sigma$-PC: Exponential lower bound against semantic $\Sigma\Pi\Sigma$-PC over $F_2$, namely, polynomial calculus operating with ... more >>>