Farmer’s Theorem revisited
Information Processing Letters | , Vol 74: pp. 47-53
The main result is that there is an integer n, such that second-order unification is undecidable in all non-monadic second-order term languages with at least n first-order variables, and even if the arguments of all second-order variables are ground terms of size bounded by n and the total number of variable occurrences is at most n.