Here's an example of a third-order matching problem with a solution which is not ground

Consider the problem F(lambda x . a) =? a

A solution is F |-> lambda x . x Y, which is not ground.

This example is on p. 66 of Prehofer 98.