Exponential separation between Res(k) and Res(k+1) for k⩽ɛlogn

Res(k) is a propositional proof system that extends resolution by working with k-DNFs instead of clauses. We show that there exist constants β,γ>0 so that if k is a function from positive integers to positive integers so that for all n, k(n)⩽βlogn, then for each n, there exists a set of clauses Cn of size nO(1) that has Res(k(n)+1) refutations of size nO(1), yet every Res(k(n)) refutation of Cn has size at least 2nγ.