  We consider the task of proving integer infeasibility of a bounded convex $K$
in $\mathbb{R}^n$ using a general branching proof system. In a general
branching proof, one constructs a branching tree by adding an integer
disjunction $\mathbf{a} \mathbf{x} \leq b$ or $\mathbf{a} \mathbf{x} \geq b+1$,
$\mathbf{a} \in \mathbb{Z}^n$, $b \in \mathbb{Z}$, at each node, such that the
leaves of the tree correspond to empty sets (i.e., $K$ together with the
inequalities picked up from the root to leaf is empty). Recently, Beame et al
(ITCS 2018), asked whether the bit size of the coefficients in a branching
proof, which they named stabbing planes (SP) refutations, for the case of
polytopes derived from SAT formulas, can be assumed to be polynomial in $n$. We
resolve this question by showing that any branching proof can be recompiled so
that the integer disjunctions have coefficients of size at most $(n
R)^{O(n^2)}$, where $R \in \mathbb{N}$ such that $K \in R \mathbb{B}_1^n$,
while increasing the number of nodes in the branching tree by at most a factor
$O(n)$. As our second contribution, we show that Tseitin formulas, an important
class of infeasible SAT instances, have quasi-polynomial sized cutting plane
(CP) refutations, disproving the conjecture that Tseitin formulas are
(exponentially) hard for CP. As our final contribution, we give a simple family
of polytopes in $[0,1]^n$ requiring branching proofs of length $2^n/n$.
