Solution (source code)

= Solution

Expand the <commutator>:
$$
c=at a t^{-1}a^{-1}t a^{-1}t^{-1}.
$$
Its possible pinches have intervening coefficients $a$, $a^{-1}$, and $a^{-1}$. For a $t(\cdot)t^{-1}$ pinch the coefficient must lie in $\langle a^2\rangle$; neither $a$ nor $a^{-1}$ does. For the $t^{-1}(\cdot)t$ pinch it must lie in $\langle a^3\rangle$, and again $a^{-1}$ does not. Here $\langle a\rangle\cong\mathbb Z$ embeds by the <normal form theorem for an HNN extension>, so these divisibility tests are valid inside $S$.

The word is a <reduced sequence in an HNN extension> with four stable letters. <Britton's lemma> gives
$$
\boxed{c\ne1,\qquad c\in\ker\theta.}
$$
Thus $S$ is a finitely presented <non-Hopfian group>: it has a surjective <endomorphism> which is not injective. This group is the <Baumslag-Solitar group> $BS(2,3)$.