I have the next rules

% Signature: natural_number(N)/1
% Purpose: N is a natural number.
natural_number(0).
natural_number(s(X)) :- natural_number(X)

ackermann(0, N, s(N)). //rule 1
ackermann(s(M),0,Result):- ackermann(M,s(0),Result). //rule 2
ackermann(s(M),s(N),Result):-ackermann(M,Result1,Result),ackermann(s(M),N,Result1). //rule 3

The query is: ackermann (M,N,s(s(0))).

Now, as I understood, In the third calculation, we got an infinite search (failture branch). I check it, and I got a finite search (failture branch).

I'll explain: In the first, we got a substitue of M=0, N=s(0) (rule 1 - succsess!). In the second, we got a substitue of M=s(0),N=0 (rule 2 - sucsses!). But what now? I try to match M=s(s(0)) N=0, But it got a finite search - failture branch. Why the comipler doesn't write me "fail".

Thank you.