Arthur Milchior: Undecidability of satisfiability of expansions of FO[<] over words with a FO[+]-definable set. Comput. 6(4): 333-363 (2017)