2021-04-11 05:24:27 (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=84ms, Wt=83ms. NTI: Rt=4ms, Wt=2ms at most 82 inferences for useful informations.
% using the norm [op(A,B)=xop(A,A,B)].

% NTI summary: 0 cases unresolved, 1 predicate has been ignored: [!/0]

normal_form(A,B)terminates_if b(A).
    % optimal. loops found: [normal_form(op(op(_,_),_),x)]. NTI took    0ms,82i,82i WARNING: ignored predicates: [!/0]
rewrite(A,B)terminates_if b(A);b(B).
    % optimal. loops found: [rewrite(op(A,op(B,op(_,_))),op(A,op(B,_)))]. NTI took    0ms,73i,73i WARNING: ignored predicates: [!/0]

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

normal_form(b, f).
    % ==> termination proof established
normal_form(f, b).
    % ==> no proof found
rewrite(f, b).
    % ==> termination proof established
rewrite(b, f).
    % ==> termination proof established
rewrite(f, f).
    % ==> no proof found

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

Analyzed program:

:- cti:norm_tmap([ op(A,B) = xop(A,A,B) ]).
rewrite(op(op(A,B),C),op(A,op(B,C))) :- !.
rewrite(op(A,op(B,C)),op(A,L)) :-
	rewrite(op(B,C),L).

normal_form(F,N) :- rewrite(F,F1), !, normal_form(F1,N).
normal_form(F,F).