Non-automatizability of bounded-depth Frege proofs
scientific article; zbMATH DE number 2138076