2021-04-11 03:39:34 (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=380ms, Wt=382ms. NTI: Rt=0ms, Wt=6ms at most 91 inferences for useful informations.
% NTI summary: 0 cases unresolved, 1 predicate has been ignored: [integer/1]

phrase(exp,Xs0,Xs)terminates_if b(Xs0).
    % optimal. loops found: [phrase(exp,['('|_],x)]. NTI took    0ms,87i,87i WARNING: ignored predicates: [integer/1]
phrase(pdt,Xs0,Xs)terminates_if b(Xs0).
    % optimal. loops found: [phrase(pdt,[_,_,_|_],x)]. NTI took    0ms,80i,80i WARNING: ignored predicates: [integer/1]
phrase(pri,Xs0,Xs)terminates_if b(Xs0).
    % optimal. loops found: [phrase(pri,['('|_],x)]. NTI took    0ms,82i,82i WARNING: ignored predicates: [integer/1]
phrase(rdp,Xs0,Xs)terminates_if b(Xs0).
    % optimal. loops found: [phrase(rdp,[_,_|_],x)]. NTI took    0ms,73i,73i WARNING: ignored predicates: [integer/1]
phrase(rds,Xs0,Xs)terminates_if b(Xs0).
    % optimal. loops found: [phrase(rds,[_,_|_],x)]. NTI took    0ms,78i,78i WARNING: ignored predicates: [integer/1]
phrase(som,Xs0,Xs)terminates_if b(Xs0).
    % optimal. loops found: [phrase(som,[_,_,_|_],x)]. NTI took    0ms,91i,91i WARNING: ignored predicates: [integer/1]

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

phrase(exp, b, f).
    % ==> termination proof established
phrase(exp, f, b).
    % ==> no proof found
phrase(pdt, b, f).
    % ==> termination proof established
phrase(pdt, f, b).
    % ==> no proof found
phrase(pri, b, f).
    % ==> termination proof established
phrase(pri, f, b).
    % ==> no proof found
phrase(rdp, b, f).
    % ==> termination proof established
phrase(rdp, f, b).
    % ==> no proof found
phrase(rds, b, f).
    % ==> termination proof established
phrase(rds, f, b).
    % ==> no proof found
phrase(som, b, f).
    % ==> termination proof established
phrase(som, f, b).
    % ==> no proof found

Tooltip: You can skip this comparison with termination analyzers by selecting "Comp. skipped" above

Analyzed program:

som-->pdt,rds.
pdt-->pri,rdp.
pri-->[N],{integer(N)}.
pri-->['('],exp,[')'].
rds-->[].
rds-->[Op],pdt,rds.
rdp-->[].
rdp-->[Op],pri,rdp.
exp-->som.