Are there any non-casework proofs of the $18$-point problem? There is a cute little problem stated as follows:

Choose a sequence $x_1,x_2,x_3,\ldots$ with $x_i\in[0,1)$ such that $x_1$ and $x_2$ are in different halves of the unit interval, $x_1,x_2,$ and $x_3$ are in different thirds, and so on. How long can such a sequence be?

It turns out the answer is exactly $17$; it is not possible to find a length-$18$ sequence obeying these constraints. See Wolfram Mathworld for more.
Berkelamp and Graham's original 1970 paper proves this with a rather involved casework argument on the relative positions of various terms in the sequence, though later in the paper they present a non-casework argument that implies the sequence can be at most $63$ terms long.
I am curious whether a more direct or "natural" argument has been developed in the 50 years hence; I wouldn't be surprised if getting an exact bound ultimately required a fairly casework-y approach, but it seems plausible that at least better upper bounds could be reached with some other method. Is anything more known about this problem?
 A: "A supplementary note on the irregularities of distributions" by M. Warmus (1976) gives a simpler proof. In fact, Warmus may have been the first to solve the problem, though not the first to publish. The paper states

Berlekamp and Graham [2] published a paper in which they considered the same problem, although in a generalized form, and they gave a proof that $17$ is the greatest possible $N$. They also mention my name as the author of this result. It is not true, however, that I solved the problem with the aid of a computer.
Since my proof is very simple and seems to be shorter than the one given by Berlekamp and Graham, I give it here. It has not been published before.

I think the paper should be accessible by everyone by the link above, since I can access it and I'm at home. The argument is still casework, but short casework: it considers only six cases of $x_9^5$, defined to be the unique element of $\{x_1, x_2, \dots, x_9\}$ which lies in the interval $[\frac49, \frac59)$. Without loss of generality, $x_9^5 \le \frac12$, so we split the possible values as $$x_9^5 \in [\tfrac49, \tfrac5{11}) \cup [\tfrac5{11}, \tfrac6{13}) \cup [\tfrac6{13},\tfrac7{15}) \cup [\tfrac7{15},\tfrac8{17}) \cup [\tfrac8{17}, \tfrac12) \cup \{\tfrac12\}.$$
Each of these cases tells us something about the other similarly-defined $x_n^k$ that ultimately leads to a contradiction, and in fact it seems like all intervals other than $[\frac5{11}, \frac6{13})$ lead to a contradiction even for $N=17$.
A: I first came across the 18-point problem in the Aug 1983 edition of Scientific American.  I was just starting studies in engineering at Cambridge and wrote a program on my Sinclair Spectrum in basic that would search the whole space.  It was going to take well over a day to process, so I converted it to Fortran for the engineering dept. computers and got my results in ~1h.  I then converted to Z80 assembler on my Spectrum and got it down to 45mins :-)  I used this program over later years, converted to C, C++, Java and most recently PHP as a measure of Moore's Law and the performance of new computers.  PHP on my [somewhat ancient] Mac Book Pro 2013 model now runs in ~0.4s.  I've yet to try it on an M2 processor!
The output shows how many branches of the search tree hit the limit where no more points can be added:
time = 0.399411s
Solutions with  1 point  =      0
Solutions with  2 points =      0
Solutions with  3 points =      0
Solutions with  4 points =      0
Solutions with  5 points =      0
Solutions with  6 points =      0
Solutions with  7 points =     48
Solutions with  8 points =      0
Solutions with  9 points =    256
Solutions with 10 points =    448
Solutions with 11 points =   2880
Solutions with 12 points =      0
Solutions with 13 points =   6272
Solutions with 14 points =   4736
Solutions with 15 points =   2304
Solutions with 16 points =   1920
Solutions with 17 points =    768
Solutions with 18 points =      0

I'm sure you'll regard this as the ultimate 'casework' answer to the problem, but it gives a proof and some interesting insight into the search space.
