  We prove the first genuine QBF proof size lower bounds for the proof system
Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof
system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike
most QBF resolution systems in the literature, proofs in MRes consist of
resolution steps together with information on countermodels, which are
syntactically stored in the proofs as merge maps. As demonstrated in [Olaf
Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy
extraction by design and allows short proofs for formulas which are hard for
classical QBF resolution systems.
  Here we show the first genuine QBF exponential lower bounds for MRes, thereby
uncovering limitations of MRes. Technically, the results are either transferred
from bounds from circuit complexity (for restricted versions of MRes) or
directly obtained by combinatorial arguments (for full MRes). Our results imply
that the MRes approach is largely orthogonal to other QBF resolution models
such as the QCDCL resolution systems QRes and QURes and the expansion systems
$\forall$Exp+Res and IR.
