  Proving failure of queries for definite logic programs can be done by
constructing a finite model of the program in which the query is false. A
general purpose model generator for first order logic can be used for this. A
recent paper presented at PLILP98 shows how the peculiarities of definite
programs can be exploited to obtain a better solution. There a procedure is
described which combines abduction with tabulation and uses a meta-interpreter
for heuristic control of the search. The current paper shows how similar
results can be obtained by direct execution under the standard tabulation of
the XSB-Prolog system. The loss of control is compensated for by better
intelligent backtracking and more accurate failure analysis.
