The problem is that, when you prove a goal, you are implicitly doing an existence proof. Imagine that goal G contains variable X. Proving goal G tries to prove ∃X G (in a constructive way). Negation as failure says to try to prove G, and conclude that G is false if the proof fails. That is, try to show ¬(∃X G). But what we want is ∃X ¬(G). That is, find an X that makes G false. But ¬(∃X G) is not logically equivalent to ∃X ¬(G).