  We consider the positions of occurrences of a factor $x$ and its binary
complement $\overline{x}$ in the Thue-Morse word ${\bf t} = {\tt 01101001}
\cdots$, and show that these occurrences are "intertwined" in essentially two
different ways. Our proof method consists of stating the needed properties as a
first-order logic formula $\varphi$, and then using a theorem-prover to prove
$\varphi$.
