2021-04-11 10:29:29 (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=396ms, Wt=398ms. NTI: Rt=4ms, Wt=6ms at most 79 inferences for useful informations.
% NTI summary: 0 cases unresolved, 2 predicates have been ignored: [=< /2,> /2]

merge(A,B,C)terminates_if b(A),b(B);b(C).
    % optimal. loops found: [merge([A,B|_],[_|_],[A,B|_]),merge([C,D|_],[y|y],[C,D|_]),merge([y|y],[_,_|_],[y,y|_])]. NTI took    0ms,77i,77i WARNING: ignored predicates: [=< /2,> /2]
mergesort(A,B)terminates_if b(A).
    % optimal. loops found: [mergesort([_,_|_],_),mergesort([_,_|_],y)]. NTI took    0ms,79i,79i
split(A,B,C)terminates_if b(A);b(B);b(C).
    % optimal. loops found: [split([A,B|_],[A|_],[B|_])]. NTI took    0ms,75i,75i
split0(A,B,C)terminates_if true.
split1(A,B,C)terminates_if true.
split2(A,B,C)terminates_if b(A);b(B);b(C).
    % optimal. loops found: [split2([A,B|_],[A|_],[B|_])]. NTI took    0ms,75i,75i

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

merge(f, f, b).
    % ==> termination proof established
merge(b, b, f).
    % ==> termination proof established
merge(b, f, f).
    % ==> no proof found
merge(f, b, f).
    % ==> no proof found
mergesort(b, f).
    % ==> termination proof established
mergesort(f, b).
    % ==> no proof found
split(f, f, b).
    % ==> termination proof established
split(f, b, f).
    % ==> termination proof established
split(b, f, f).
    % ==> termination proof established
split(f, f, f).
    % ==> no proof found
split0(f, f, f).
    % ==> termination proof established
split1(f, f, f).
    % ==> termination proof established
split2(f, f, b).
    % ==> termination proof established
split2(f, b, f).
    % ==> termination proof established
split2(b, f, f).
    % ==> termination proof established
split2(f, f, f).
    % ==> 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/plumer/mergesort_t:

mergesort([],[]).
mergesort([X],[X]).
mergesort([X,Y|Xs],Ys) :- split2([X,Y|Xs],X1s,X2s),
                          mergesort(X1s,Y1s),
                          mergesort(X2s,Y2s),
                          merge(Y1s,Y2s,Ys).

split(Xs,Ys,Zs) :- split0(Xs,Ys,Zs).
split(Xs,Ys,Zs) :- split1(Xs,Ys,Zs).
split(Xs,Ys,Zs) :- split2(Xs,Ys,Zs).

split0([],[],[]).
split1([X],[X],[]).
split2([X,Y|Xs],[X|Ys],[Y|Zs]) :- split(Xs,Ys,Zs).

merge([],Xs,Xs).
merge(Xs,[],Xs).
merge([X|Xs],[Y|Ys],[X|Zs]) :- X=<Y, merge(Xs,[Y|Ys],Zs).
merge([X|Xs],[Y|Ys],[X|Zs]) :- X>Y, merge([X|Xs],Ys,Zs).