Resolution trees with lemmas ($\mathrm{RTL}$) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments $\mathrm{RTL}(k)$ are related to clause learning algorithms where the width of learned clauses is bounded by $k$.

For every $k$ up to $O(\log n)$, an exponential separation ... more >>>