  Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is a
refutational proof system for quantified Boolean formulas (QBF). Each line of
MRes consists of clauses with only existential literals, together with
information of countermodels stored as merge maps. As a result, MRes has
strategy extraction by design. The QRAT [Heule et al. J. Autom. Reason.'2017]
proof system was designed to capture QBF preprocessing. QRAT can simulate both
the expansion-based proof system $\forall$Exp+Res and CDCL-based QBF proof
system LD-Q-Res.
  A family of false QBFs called SquaredEquality formulas were introduced in
[Beyersdorff et al. J. Autom. Reason.'2021] and shown to be easy for MRes but
need exponential size proofs in Q-Res, QU-Res, CP+$\forall$red,
$\forall$Exp+Res, IR-calc and reductionless LD-Q-Res. As a result none of these
systems can simulate MRes. In this paper, we show a short QRAT refutation of
the SquaredEquality formulas. We further show that QRAT strictly p-simulates
MRes. Besides highlighting the power of QRAT system, this work also presents
the first simulation result for MRes.
