Robinson's binary resolution, often presented in terms of binary trees,
may be restricted to be regular: no atom is resolved upon twice in any
branch. In this work we consider reordering two consecutive resolution
steps, inducing an AVL rotation on the tree, which may expose a new
irregularity. Without sacrificing completeness, we strengthen the
restriction by enforcing regularity after (all sequences of) rotations.
Such a tree is said to be minimal, and the smallest proof tree must be
minimal. Although the number of re-orderings may be intractable, an
efficient algorithm is given to determine minimality. Experiments show
that the theorem prover OTTER spends much effort building non-minimal
trees, and that restricting it to minimal trees sometimes improves
performance.