2021-04-11 10:32: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=28ms, Wt=29ms. NTI: Rt=4ms, Wt=4ms at most 72 inferences for useful informations.
% NTI summary: 1 case unresolved, 0 predicates have been ignored: []

inf terminates_if false.
    % optimal. loops found: [inf]. NTI took    0ms,72i,72i
inf_fail terminates_if true.
inf_false terminates_if true.
inf_myfalse terminates_if true.
inf_unif terminates_if true.
myfalse terminates_if true.
myfalse(A)terminates_if true.
repeat_fail terminates_if true.
repeat_false terminates_if true.
repeat_myfalse terminates_if true.
repeat_unif terminates_if true.
urepeat terminates_if false.
    % optimal. loops found: [urepeat]. NTI took    0ms,72i,72i
xf_fail terminates_if true.
xf_false terminates_if true.
xf_myfalse terminates_if false.
    % all cases unresolved.
    %  NTI took    0ms, 0i,76i
xf_unif terminates_if true.

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

inf.
    % ==> no proof found
inf_fail.
    % ==> termination proof established
inf_false.
    % ==> termination proof established
inf_myfalse.
    % ==> termination proof established
inf_unif.
    % ==> termination proof established
myfalse.
    % ==> termination proof established
myfalse(f).
    % ==> termination proof established
repeat_fail.
    % ==> termination proof established
repeat_false.
    % ==> termination proof established
repeat_myfalse.
    % ==> termination proof established
repeat_unif.
    % ==> termination proof established
urepeat.
    % ==> no proof found
xf_fail.
    % ==> termination proof established
xf_false.
    % ==> termination proof established
xf_myfalse.
    % ==> no proof found
xf_unif.
    % ==> termination proof established

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/q/inf.pl:

% Quality testing for termination analysers
% All predicates terminate exception inf/0 and urepeat/0

myfalse :-
	myfalse(0).

myfalse(s(0)).

inf :-
	 inf.

urepeat.
urepeat :-
	urepeat.

inf_false :-
	false,
	inf_false.

inf_fail :-
	fail,
	inf_fail.

inf_myfalse :-
	myfalse,
	inf_myfalse.

inf_unif :-
	0=s(0),
	inf_unif.


repeat_false.
repeat_false :-
	false,
	repeat_false.

repeat_fail.
repeat_fail :-
	fail,
	repeat_fail.

repeat_myfalse.
repeat_myfalse :-
	myfalse,
	repeat_myfalse.

repeat_unif.
repeat_unif :-
	0=s(0),
	repeat_unif.

xf_false :-
	false,
	inf.

xf_fail :-
	fail,
	inf.

xf_myfalse :-
	myfalse,
	inf.

xf_unif :-
	0 = s(0),
	inf.