O. Beyersdorff, B. Böhm, and M. Mahajan, “Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs”, AAAI, vol. 38, no. 8, pp. 7943-7951, Mar. 2024.