2021-04-11 10:33:28 (CEST) cTI start

% cTI_lt 0.25 using 23.619 MLIPS SICStus 3.8.5 (x86-linux-glibc2.1): Mon Oct 30 16:34:14 CET 2000.
% cTI: Rt=224ms, Wt=223ms. NTI: Rt=4ms, Wt=3ms at most 80 inferences for useful informations.
% NTI summary: 1 case unresolved, 0 predicates have been ignored: []

ack(A,B,C)terminates_if false.
    % 1 unresolved: [ack(b,b,f)].
    % loops found: [ack(s(_),s(s(_)),x),ack(s(y),s(s(_)),x),ack(s(s(_)),0,x)]. NTI took    4ms,80i,95i

% Comparison with termination analyzers
% A termination analyser of identical power would verify
% with the following 1 proof the 1 inferred condition:

ack(b, b, b).
    % ==> no proof found

Tooltip: You can skip this comparison with termination analyzers by selecting "Comp. skipped" above

Analyzed program located at URL http://www.complang.tuwien.ac.at/cti/bench/various/ack:

%int(0).
%int(s(X)) :- int(X).
ack(0,N,s(N)). % :- int(N).
ack(s(M),0,A) :- ack(M,s(0),A).
ack(s(M),s(N),A) :- ack(s(M),N,A1),ack(M,A1,A).