2021-04-11 10:33:57 (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=24ms, Wt=49ms. NTI: Rt=4ms, Wt=4ms at most 92 inferences for useful informations.
% NTI summary: 1 case unresolved, 0 predicates have been ignored: []

g1 terminates_if false.
    % optimal. loops found: [g1]. NTI took    0ms,79i,79i
g2 terminates_if false.
    % optimal. loops found: [g2]. NTI took    0ms,79i,79i
g3 terminates_if false.
    % optimal. loops found: [g3]. NTI took    4ms,79i,79i
g4 terminates_if false.
    % all cases unresolved.
    %  NTI took    0ms, 0i,88i
r(A,B)terminates_if true.
tc(A,B)terminates_if false.
    % optimal. loops found: [tc(a,x)]. NTI took    0ms,92i,92i

% Comparison with termination analyzers
% A termination analyser of identical power would verify
% with the following 6 proofs the 6 inferred conditions:

g1.
    % ==> no proof found
g2.
    % ==> no proof found
g3.
    % ==> no proof found
g4.
    % ==> no proof found
r(f, f).
    % ==> termination proof established
tc(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/bol_thesis/ch0_p3:

% P
tc(X,Y) :- r(X,Y).
tc(X,Y) :- r(X,Z), tc(Z,Y).

r(a,a).
r(a,b).
r(b,c).
r(d,a).

g1 :- tc(a,b).
g2 :- tc(a,c).
g3 :- tc(a,d).
g4 :- tc(b,d).