Beyersdorff, O.; Böhm, B.; Mahajan, M. Runtime Vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs. AAAI 2024, 38, 7943-7951.