  By adapting the iterative yardstick construction of Stockmeyer, we show that
the reachability problem for vector addition systems with a stack does not have
elementary complexity. As a corollary, the same lower bound holds for the
satisfiability problem for a two-variable first-order logic on trees in which
unbounded data may label only leaf nodes. Whether the two problems are
decidable remains an open question.

Formal Languages and Automata Theory;Logic in Computer Science