You will get one question chosen at random
from the following two:
(1)
The feasible interpolation theorem for resolution and an exponential
lower bound for R-refutations of the Clique-Color clauses.
The non-automatizability of proof systems not admitting
FI.
[There are three different proofs in
my 2019 book of the FI for R:
Secs. 5.6, 17.6 (using 17.5) and 17.7; in lectures we covered the
second.
The lower bound argument is in Sec.13.5, the non-automatizability
in Sec.17.3.]
(2) Ajtai's theorem:
an exponential lower bound for constant depth Frege proofs
of PHP.
[This is in Sections 15.1-3 in the
book.]