Unsolvable problems for SLDNF resolution

AbstractShepherdson showed that there are maximal safe computation rules Rm for SLDNF resolution, such that if a query succeeds under any safe rule it succeeds under Rm, and if it fails under any safe rule it fails under Rm. Later he showed that such maximal rules also get all possible answers, i.e., if a query succeeds with answer θ under any safe rule, then it succeeds with answer equivalent to θ under Rm. The question was raised there, whether there were always recursive maximal rules. We answer this negatively. We also show the unsolvability of the problems of deciding whether a query leads to a dead end, whether the Clark completion comp(P) of a program P is consistent, and whether a query which is known to be a logical consequence of the program succeeds in PROLOG