Stefan Mengel, Friedrich Slivovsky: Proof Complexity of Symbolic QBF Reasoning. SAT 2021: 399-416