2021-04-11 10:28:22 (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=56ms, Wt=72ms. NTI: Rt=4ms, Wt=3ms at most 75 inferences for useful informations.
% NTI summary:  Complete result is optimal.
app(A,B,C)terminates_if b(A);b(C).
    % optimal. loops found: [app([A|_],x,[A|_])]. NTI took    0ms,72i,72i
app3(A,B,C,D)terminates_if b(A),b(B);b(A),b(D).
    % optimal. loops found: [app3([],[A|_],x,[A|_]),app3([_|_],y,x,y)]. NTI took    4ms,75i,75i

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

app(f, f, b).
    % ==> termination proof established
app(b, f, f).
    % ==> termination proof established
app(f, b, f).
    % ==> no proof found
app3(b, f, f, b).
    % ==> termination proof established
app3(b, b, f, f).
    % ==> termination proof established
app3(f, b, b, b).
    % ==> no proof found
app3(b, 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/apt_flptp/APPEND3:

% app3(Xs, Ys, Zs, Us) :- Us is the result of concatenating the lists Xs, Ys and Zs
app3(Xs, Ys, Zs, Us) :-	app(Xs, Ys, Vs), app(Vs, Zs, Us).

% augmented by the APPEND program
app([], Ys, Ys).
app([X | Xs], Ys, [X | Zs]) :- app(Xs, Ys, Zs).