L. Gordeev and E. H. Haeusler, “Proof Compression and NP Versus PSPACE II”, B Sect Log, vol. 49, no. 3, pp. 213–230, Nov. 2020.