% Dclauses DL entails Q using sat (defined elsewhere).
estsat(DL,Q) :- negs(Q,NQ), \+ sat([NQ|DL],_).

% negs(Q,NQ): NQ is the negation of the literals in Q.
negs([],[]).
negs([not(A)|T],[A|NT]) :- negs(T,NT).
negs([A|T],[not(A)|NT]) :- \+ A=not(_), negs(T,NT).
