We show that for any integer $d>0$, depth $d$ Frege systems are NP-hard to automate. Namely, given a set $S$ of depth $d$ formulas, it is NP-hard to find a depth $d$ Frege refutation of $S$ in time polynomial in the size of the shortest such a refutation. This extends the result of Atserias and Muller [JACM, 2020] for the non-automatability of resolution—a depth 1 Frege system—to any depth $d>0$ Frege system.

Some typos fixed, keywords added

We show that for any integer $d>0$, depth $d$ Frege systems are NP-hard to automate. Namely, given a set $S$ of depth $d$ formulas, it is NP-hard to find a depth $d$ Frege refutation of $S$ in time polynomial in the size of the shortest such a refutation. This extends the result of Atserias and Muller [JACM, 2020] for the non-automatability of resolution—a depth 1 Frege system—to any depth $d>0$ Frege system.