\begin{thebibliography}{10}
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\urlprefix}{URL }

\bibitem{AB70}
Anderson, R., Bledsoe, W.W.: A linear format for resolution with merging and a
  new technique for establishing completeness. Journal of the ACM  17(3),
  525--534 (1970)

\bibitem{AL97-jar}
Astrachan, O.L., Loveland, D.W.: The use of lemmas in the model elimination
  procedure. Journal of Automated Reasoning  19,  117--141 (1997)

\bibitem{bcj19-TCT}
Beyersdorff, O., Chew, L. Janota, M.: New resolution-based {QBF} calculi and their proof complexity. ACM Transactions on Computation Theory 11, 1--42 (2019)

\bibitem{Burris98}
Burris, S.: Logic for Mathematics and Computer Science. Prentice Hall (1998)

\bibitem{GVGB-strategies-IJCAI11}
Goultiaeva, A., Van~Gelder, A., Bacchus, F.: A uniform approach for generating
  proofs and strategies for both true and false {QBF} formulas. In: Proc.\
  IJCAI (2011)

\bibitem{HSB-Skolem-FMCAD14}
Heule, M., Seidl, M., Biere, A.: Efficient Extraction of Skolem Functions
from {QRAT} Proofs. In: Proc.\ FMCAD (2014)

\bibitem{KBMF95}
Kleine~B{\"u}ning, H., Karpinski, M., Fl{\"o}gel, A.: Resolution for quantified
  boolean formulas. Information and Computation  117,  12--18 (1995)

\bibitem{KBL1999-book}
Kleine~B{\"u}ning, H., Lettmann, T.: Propositional Logic: Deduction and
  Algorithms. Cambridge University Press (1999)

\bibitem{Klieber-ghostq-SAT10}
Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal {QBF}
  solver with game-state learning. In: SAT, LNCS (2010)

\bibitem{Letz02}
Letz, R.: Lemma and model caching in decision procedures for quantified boolean
  formulas. In: Proc.\ TABLEAUX (LNAI 2381). pp. 160--175 (2002)

\bibitem{LetzMayrGoller94}
Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into
  connection tableau calculi. JAR  13,  297--337 (1994)

\bibitem{Loveland68}
Loveland, D.W.: Mechanical theorem-proving by model elimination. Journal of the
  ACM  15(2),  236--251 (1968)

\bibitem{Lov69}
Loveland, D.W.: A simplified format for the model elimination theorem-proving
  procedure. JACM  16(3),  349--363 (1969)

\bibitem{Lov78}
Loveland, D.W.: Automated Theorem Proving: A Logical Basis. North-Holland,
  Amsterdam (1978)

\bibitem{MZ82}
Minker, J., Zanon, G.: {An Extension to Linear Resolution with Selection
  Function}. Information Processing Letters  14(4),  191--194 (1982)

\bibitem{SDB-CP06}
Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing {QBF}. In: Proc.\ CP
  2006 (LNCS 4204). pp. 514--529 (2006)

\bibitem{Sli22}
Slivovsky, F.: Quantified {CDCL} with Universal Resolution.
  In: Proc.\ Sat 2022. (2022)

\bibitem{VanGelder-aut-modoc-JAR}
Van~Gelder, A.: Autarky pruning in propositional model elimination reduces
  failure redundancy. Journal of Automated Reasoning  23(2),  137--193 (1999)

\bibitem{VanGelder-sat2005}
Van~Gelder, A.: Input distance and lower bounds for propositional resolution
  proof length. In: Theory and Applications of Satisfiability Testing (SAT)
  (2005)

\bibitem{VG-qpup-CP12}
Van~Gelder, A.: Contributions to the theory of practical quantified boolean
  formula solving. In: Proc.\ CP. pp. 647--673 (2012)

\bibitem{VGWL-EFL-SAT12}
Van~Gelder, A., Wood, S.B., Lonsing, F.: Extended failed literal detection for
  {QBF}. In: Proc.\ SAT. pp. 86--99 (2012)

\end{thebibliography}