  This paper concerns Boolean satisfiability (SAT) solvers based on Ordered
Binary Decision Diagrams (BDDs), especially those that can generate proofs of
unsatisfiability. Mengel (arXiv:2306.00886) has presented a theoretical
analysis that a BDD-based SAT solver can generate a proof of unsatisfiability
for the pigeonhole problem (PHP$_n$) in polynomial time, even when the problem
is encoded in the standard ``direct'' form. His approach is based on bucket
elimination, using different orderings for the variables in the BDDs than in
the buckets. We show experimentally that these proofs scale as $O(n^5)$. We
also confirm the exponential scaling that occurs when the same variable
ordering is used for the BDDs as for the buckets.
