#22 exists_not implementation bug

[Michael Kifer]

A problem with the implementation of exists_not.
We need to implement this:
/
exists_not(Varlist1,Goal)
Let Varlist2 be those vars in Goal that are not in Varlist_1
exists Varlist1 forall Varlist2 naf Goal
==
exists Varlist1 naf exists Varlist2 Goal/

One of the clauses in the implementation is:
% Case 3.2a
exists_not(_Vars,Goal):- neg(Goal).

But this is wrong. Suppose we have
neg(p(a,b)).
p(a,c).
and consider

exists(X) naf exists(Y) p(X,Y)
that is: exists_not(X,p(X,Y)).

By case 3.2a above, we get X=a. But this is wrong because naf exists(Y) p(a,Y) is false, since p(a,c) is true.
So, this case 3.2 is sound ONLY if Varlist2 is empty.