We prove that there is a constant $K$ such that \emph{Tseitin} formulas for an undirected graph $G$ requires proofs of
size $2^{\mathrm{tw}(G)^{\Omega(1/d)}}$ in depth-$d$ Frege systems for $d<\frac{K \log n}{\log \log n}$, where $\mathrm{tw}(G)$ is the treewidth of $G$. This extends Håstad's recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent.
Namely, we show that if a Tseitin formula for a graph $G$ has size $s$, then for all large enough $d$, it has a depth-$d$ Frege proof of size $2^{\mathrm{tw}(G)^{\mathcal{O}(1/d)}} \mathrm{poly}(s)$.
Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.

We prove that there is a constant $K$ such that \emph{Tseitin} formulas for an undirected graph $G$ requires proofs of
size $2^{\mathrm{tw}(G)^{\Omega(1/d)}}$ in depth-$d$ Frege systems for $d<\frac{K \log n}{\log \log n}$, where $\tw(G)$ is the treewidth of $G$. This extends H{\aa}stad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent.
Namely, we show that if a Tseitin formula for a graph $G$ has size $s$, then for all large enough $d$, it has a depth-$d$ Frege proof of size $2^{\mathrm{tw}(G)^{\O(1/d)}} \mathrm{poly}(s)$.
Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.