We say that a graph with n vertices is c-Ramsey if it does not contain either a clique or an independent set of size c \log n. We define a CNF formula which expresses this property for a graph G. We show a superpolynomial lower bound on the length of ... more >>>