2021-04-11 10:33:59 (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=64ms, Wt=85ms. NTI: Rt=16ms, Wt=31ms at most 73 inferences for useful informations.
% NTI summary: 3 cases unresolved, 0 predicates have been ignored: []

flat(A,B)terminates_if false.
    % 3 unresolved: [flat(b,b),flat(b,f),flat(f,b)].
    % loops found: [flat(tree(A,niltree,_),cons(A,_))]. NTI took   16ms,73i,100i
right(A,B)terminates_if true.

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

flat(b, b).
    % ==> no proof found
right(f, f).
    % ==> termination proof established

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/talp/flat:

% Source: http://bibiserv.techfak.uni-bielefeld.de/cgi-bin/talp_submit/examples
% from: Thomas Arts, Hans Zantema,
%       Termination of logic programs using semantic unification,
%       In Proceedings of the Fifth International Workshop on
%       Logic Program Synthesis and Transformation, LNCS 1048,
%       pp. 219-233, Springer-Verlag, Berlin, 1996

right(tree(X, XS1, XS2), XS2).

flat(niltree, nil).
flat(tree(X, niltree, XS), cons(X, YS)) :-
        right(tree(X, niltree, XS), ZS),
        flat(ZS, YS).
flat(tree(X, tree(Y, YS1, YS2), XS), ZS) :-
        flat(tree(Y, YS1, tree(X, YS2, XS)), ZS).