Summary: We show that any nondeterministic read-once branching program that decides a satisfiable Tseitin formula based on an \(n\times n\) grid graph has size at least \(2^{ \Omega (n)}\). Then using the Excluded Grid Theorem by Robertson and Seymour we show that for an arbitrary graph \(G(V,E)\) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on \(G\) has size at least \(2^{\Omega (\operatorname{tw}(G)^{\delta})}\) for all \(\delta<1/36\), where \(\operatorname{tw}(G)\) is the treewidth of \(G\) (for planar graphs and some other classes of graphs the statement holds for \(\delta = 1)\). We apply the mentioned results to the analysis of the complexity of derivations in the proof system \(\mathrm{OBDD}(\land, \mathrm{reordering})\) and show that any \(\mathrm{OBDD}(\land, \mathrm{reordering})\)-refutation of an unsatisfiable Tseitin formula based on a graph \(G\) has size at least \(2^{\Omega(\operatorname{tw}(G)^{\delta})}\). We also show an upper bound \(O(|E|2^{\operatorname{pw}(G)} )\) on the size of OBDD representations of a satisfiable Tseitin formula based on \(G\) and an upper bound \(O(|E||V| 2^{\operatorname{pw}(G)}+|\mathrm{TS}_{G,c}|^2)\) on the size of \(\mathrm{OBDD}(\land)\)-refutation of an unsatisifable Tseitin formula \(\mathrm{TS}_{G,c}\), where \(\operatorname{pw}(G)\) is the pathwidth of \(G\).