2021-04-11 10:34:01 (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=48ms, Wt=92ms. NTI: Rt=0ms, Wt=5ms at most 80 inferences for useful informations.
% NTI summary:  Complete result is optimal.
liste_gleichlang(A,B)terminates_if b(A);b(B).
    % optimal. loops found: [liste_gleichlang([_|_],[_|_])]. NTI took    0ms,72i,72i
listen_gleichlangmit(A,B)terminates_if b(A).
    % optimal. loops found: [listen_gleichlangmit([[_|_]|_],[_|_]),listen_gleichlangmit([[],[]|_],[])]. NTI took    0ms,80i,80i

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

liste_gleichlang(f, b).
    % ==> termination proof established
liste_gleichlang(b, f).
    % ==> termination proof established
liste_gleichlang(f, f).
    % ==> no proof found
listen_gleichlangmit(b, f).
    % ==> termination proof established
listen_gleichlangmit(f, 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/ttr/listen_gleichlang.pl:

liste_gleichlang([], []).
liste_gleichlang([_X|Xs],[_Y|Ys]) :-
	liste_gleichlang(Xs, Ys).

listen_gleichlangmit([], _Z).
listen_gleichlangmit([Z|Zs], X) :-
	liste_gleichlang(Z, X),
	listen_gleichlangmit(Zs, X).