Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms.