The Clergyman's conjecture for anti-recurrence sequences

An anti-recurrence sequence is the increasing sequence generated by a positive integral linear form, by selecting the integers represented by that form without repetition. A linear sequence is an arithmetic progression, and an automatic sequence is a sequence generated by a finite automaton reading the indices in a fixed base. The Clergyman's conjecture. Every anti-recurrence sequence is a sum of a linear sequence and an automatic sequence. This meta-conjecture combines several conjectures of Kimberling and Moses about complementary sequences; the paper settles two previously open instances using the automatic theorem prover Walnut, while the general assertion remains open.