Summary: A transformation technique is introduced which, given the Horn-clause definitions of a set of predicates \(p_ i\), synthesizes the definitions of new predicates \(\widetilde p_ i\) which can be used, under a suitable refutation procedure, to compute the finite failure set of \(p_ i\). This technique exhibits some computational advantages, such as the possibility of computing nonground negative goals still preserving the capability of producing answers. The refutation procedure, named SLDN refutation, is proved sound and complete with respect to the completed program.