2021-04-11 03:38:56 (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=152ms, Wt=154ms. NTI: Rt=8ms, Wt=5ms at most 80 inferences for useful informations.
% NTI summary:  Complete result is optimal.
delete(A,B,C)terminates_if b(B);b(C).
    % optimal. loops found: [delete(x,[A|_],[A|_])]. NTI took    0ms,72i,72i
member(A,B)terminates_if b(B).
    % optimal. loops found: [member(x,[_|_])]. NTI took    0ms,72i,72i
reach(A,B,C,D)terminates_if b(C),b(D).
    % optimal. loops found: [reach(_,x,[_|_],_),reach(y,x,[_|_],y),reach(y,x,[[y,y]|y],[y|_])]. NTI took    4ms,80i,80i

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

delete(f, f, b).
    % ==> termination proof established
delete(f, b, f).
    % ==> termination proof established
delete(b, f, f).
    % ==> no proof found
member(f, b).
    % ==> termination proof established
member(b, f).
    % ==> no proof found
reach(f, f, b, b).
    % ==> termination proof established
reach(b, b, b, f).
    % ==> no proof found
reach(b, b, 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/plumer/pl7.6.2c:

reach(X,Y,Edges,Not_Visited) :- member([X,Y],Edges).
reach(X,Z,Edges,Not_Visited) :- member([X,Y],Edges),
                                member(Y,Not_Visited),
                                delete(Y,Not_Visited,V1),
                                reach(Y,Z,Edges,V1).

member(H,[H|L]).
member(X,[H|L]) :- member(X,L).

delete(X,[X|Y],Y).
delete(X,[H|T1],[H|T2]) :- delete(X,T1,T2).