We continue the program of proving circuit lower bounds via circuit satisfiability algorithms. So far, this program has yielded several concrete results, proving that functions in_{1},…,_{n}) is

^{k}-size^{n}/^{k}time (for all

Applying^{0}∘