What algorithm solves high-order unification for untyped terms in most cases?
Maybe you should try nominal unification. In the paper nominal unification, it gives 4 examples which are untyped $\lambda$-terms.