- INSTANCE: A Frege proof of a tautology .
- SOLUTION:
A Frege proof
of
shorter than ,
i.e., containing at
most as many symbols as .
- MEASURE:
Number of symbols in .

*Good News:*Approximable within*O(n)*.*Bad News:*APX-hard [8].*Comment:*The result applies to all Frege systems, to all extended Frege systems, to resolution, to Horn clause resolution, to the sequent calculus, and to the cut-free sequent calculus. Not approximable within for any unless [8].