Gordeev, L.; Haeusler, E. H. Proof Compression and NP Versus PSPACE II. B Sect Log 2020, 49, 213-230.