2021-04-11 10:34:00 (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=36ms, Wt=36ms. NTI: Rt=0ms, Wt=1ms at most 72 inferences for useful informations.
% NTI summary:  Complete result is optimal.
append(A,B,C)terminates_if b(A);b(C).
    % optimal. loops found: [append([A|_],x,[A|_])]. NTI took    0ms,72i,72i

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

append(f, f, b).
    % ==> termination proof established
append(b, f, f).
    % ==> termination proof established
append(f, b, 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/terminweb/append:

% Source: http://www.cs.bgu.ac.il/cgi-bin/genaim/TerminWeb/term_check?example=append

append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).
append([],Ys,Ys).