Finite-variable hierarchy conjecture

It seems that Ben Rossman has resolved another long-standing open problem in finite model theory: finite-variable hierarchy conjecture. Loosely speaking, the conjecture is that over ordered graphs first-order logic with k+1 variable is more powerful than first-order logic with k variable. The problem is nicely summarized in Anuj Dawar's survey. Ben has shown that this hierarchy is strict. What was previously known is that (over ordered graphs) first-order logic with 3 variables is strictly more expressive than first-order logic with 2 variables, but it was not known whether first-order logic with 3 variables is less expressive than first-order logic with k variables, for every k > 3. Worse yet, it wasn't even known whether this hierarchy is strict. See Anuj Dawar's survey for further details.

I believe this is the third big open problems that Ben has resolved in this decade. Go Ben!