We describ e a system LK(c[\lambda]) for refuting CNF formulae, as a restriction of the sequent calculus in which every formula in a sequent is defined over at most \lambda variables. This further generalizes the system Res(k), a generalization of Resolution to k-DNF introduced in [9]. We adapt the Pudlák-Impagliazzo game ([11]) to prove lower bounds for treelike LK(c[\lambda]). We show that dynamic satisfiability, which was introduced in [6] to study resolution space complexity, is a sufficient "but not necessary" condition to obtain exponential lower bounds.