This paper is motivated by seeking lower bounds on OBDD($\land$, weakening, reordering) refutations, namely OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1-NBP($\land$) refutations based on read-once nondeterministic branching programs. These generalize OBDD($\land$, reordering) refutations. There are polynomial size 1-NBP($\land$) refutations of the pigeonhole principle, hence 1-NBP($\land$) is strictly stronger than OBDD($\land$, reordering). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP($\land$) refutations. As a corollary, OBDD($\land$, reordering) does not simulate tree-like resolution, answering a previously open question.

The system 1-NBP($\land$, $\exists$) uses projection inferences instead of weakening. 1-NBP($\land$, $\exists_k$) is the system restricted to projection on at most $k$ distinct variables. We construct explicit constant degree graphs $G_n$ on $n$ vertices and an $\epsilon > 0$, such that 1-NBP($\land$, $\exists_{\epsilon n}$) refutations of the Tseitin formula for $G_n$ require exponential size.

Second, we study the proof system OBDD($\land$, weakening, reordering$_\ell$) which allows $\ell$ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD($\land$, weakening, reordering$_\ell$) refutations for $\ell = \epsilon \log n$, where $n$ is the number of variables and $\epsilon > 0$ is a constant. The lower bound is based on multiparty communication complexity.