The periodic characterization of the greedy 3-subsumfree sequence S_{1,2,3}

Let $S_{1,2,3}$ be the greedy 3-subsumfree sequence beginning with $1,2,3$: after the initial values, each term is the smallest larger integer that is not the sum of three distinct previous terms. The periodic characterization conjecture. For every positive integer $z$,

$$z\in S_{1,2,3}\quad\iff\quad z\in\{1,5,13\}\ \text{or}\ z\bmod 23\in\{2,3,4,14,15\}.$$

The paper reports that Walnut verifies this statement, so it is subsequently promoted to a theorem.