2021-04-11 10:34:04 (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=228ms, Wt=230ms. NTI: Rt=4ms, Wt=5ms at most 80 inferences for useful informations.
% NTI summary: 2 cases unresolved, 0 predicates have been ignored: []

div(A,B,C)terminates_if b(A);b(B),b(C).
    % optimal. loops found: [div(s(s(_)),s(s(_)),s(_)),div(s(s(_)),s(s(_)),s(y)),div(s(s(_)),s(0),s(s(_)))]. NTI took    0ms,80i,80i
minus(A,B,C)terminates_if b(A);b(B).
    % optimal. loops found: [minus(s(_),s(_),x)]. NTI took    0ms,72i,72i
multi(A,B,C)terminates_if b(A),b(B).
    % 2 unresolved: [multi(f,b,b),multi(f,b,f)].
    % loops found: [multi(_,s(_),_),multi(y,s(_),y)]. NTI took    4ms,72i,72i
plus(A,B,C)terminates_if b(B);b(C).
    % optimal. loops found: [plus(x,s(_),s(_))]. NTI took    0ms,72i,72i

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

div(b, f, f).
    % ==> termination proof established
div(f, b, b).
    % ==> termination proof established
div(f, b, f).
    % ==> no proof found
div(f, f, b).
    % ==> no proof found
minus(f, b, f).
    % ==> termination proof established
minus(b, f, f).
    % ==> termination proof established
minus(f, f, b).
    % ==> no proof found
multi(b, b, f).
    % ==> termination proof established
multi(b, f, b).
    % ==> no proof found
multi(f, b, b).
    % ==> no proof found
plus(f, f, b).
    % ==> termination proof established
plus(f, b, f).
    % ==> termination proof established
plus(b, f, 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/nguyen/AC_04.pl:

plus(X,0,X).
plus(X,s(Y),s(Z)):- plus(X,Y,Z).
multi(X,0,0).
multi(X,s(Y),Z):- multi(X,Y,T), plus(X,T,Z).
minus(X,0,X).
minus(s(X),s(Y),Z):- minus(X,Y,Z).
div(0,s(Y),0).
div(s(X),s(Y),s(Z)):- minus(X,Y,T),div(T,s(Y),Z).