  We prove the first 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 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.
