  In a recent paper of Rampersad et al., the authors conjectured that the
smallest possible critical exponent of an infinite balanced word over a
5-letter alphabet is $3/2$. We prove this result, using a formulation of
first-order logic, the Pell number system, and a machine computation based on
finite-state automata.
