Nonelementary problem

• the problem of regular expression equivalence with complementation
• decision problem for monadic second-order logic over trees
• decision problem for term algebras
• satisfiability of the W. V. O. Quine's fluted fragment of first-order logic