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 Exists(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 not(Exists(X) G). But what we want is Exists(X) not(G). That is, find an X that makes G false. But not(Exists(X) G) is not logically equivalent to Exists(X) not(G).