Unifiability algorithms for higher-order logic are algorithms which decide the unification problem for sub-classes of higher-order logic by providing a witness. They contrast with unification procedures by deciding unification problems of infinitary nature, which might have in- finitely many most general unifiers. Unification procedures for these sub- classes return a complete set of these unifiers and do not terminate. The common practice in automated deduction for higher-order logic is to utilize unification procedures and to force their termination by re- stricting the size of the generated unifiers. The unifiability algorithms, which are complete for certain sub-classes, allow us to have a more se- mantical approach. In this paper we claim that the standard resolution calculi for higher-order automated deduction do not take full advantage of the strengths of these algorithms and suggest a new calculus. We prove that this calculus can have an exponential speed-up over the traditional calculi.