Atserias, Kolaitis, and Vardi [AKV04] showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD($\land$, weakening), simulates CP* (Cutting Planes with unary coefficients). We show that OBDD($\land$, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring tautologies have polynomial size proofs in the OBDD($\land$, weakening) system.

The reordering rule allows changing the variable order for OBDDs. We show that OBDD($\land$, weakening, reordering) is strictly stronger than OBDD($\land$, weakening). This is proved using the Clique-Coloring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD($\land$) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolved open question proposed by Groote and Zantema [GZ03].

Applying dag-like and tree-like lifting techniques to the mentioned results we completely investigate the mutual strength for every pair of systems among $CP^*$, OBDD($\land$), OBDD($\land$, weakening) and OBDD($\land$, weakening, reordering). For dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.