We formalize the notion of proof systems obtained by adding normal dependency schemes into the QCDCL proof system underlying algorithms for solving Quantified Boolean Formulas, by exploring the addition of the dependency schemes via two approaches: one as a preprocessing tool, and second in propagation and learnings in the QCDCL trails.

We show that QCDCL augmented with the reflexive resolution path dependency scheme D=D$^{rrs}$ produces three proof systems of interest: QCDCL(D), D+QCDCL and D+QCDCLD(D). We show that these three systems are not only pairwise incomparable, but also each system is incomparable with the standard QCDCL and QCDCL$^{cube}$, as well as with QCDCL$^{LO}_{NORED}$, QRes, QURes, and Q(D$^{rrs}$)Res.