NegationAsFailure
ISO negation-as-failure '\+'/1, encoded as the two clauses of the classic Prolog idiom \+ X :- must_be_executable(X), call(X), !, fail. \+ X :- true.: Fail tries X, and if it succeeds at all, cuts (via it.unibo.tuprolog.solve.stdlib.magic.MagicCut, since an ordinary ! here would only be transparent up to this clause, not back to the caller that invoked \+) and fails; Success is only ever reached, via backtracking into the second clause, when Fail's X had no solution at all. Both implementations are registered together (see it.unibo.tuprolog.solve.classic.stdlib.DefaultBuiltins) so that ordinary clause selection on \+/1 finds exactly these two clauses, in order.
Inheritors
Types
The first clause: prove X, and on success cut back to the caller of \+ and fail.
The fallback clause: reached only if Fail's X failed outright, so \+ X succeeds.