Experimental Evaluation

This page contains a detailed experimental evaluation corresponding to the paper:

Termination Analysis of Logic Programs through Combination of Type-Based Norms

Maurice Bruynooghe, Michael Codish, John Gallagher, Samir Genaim and Wim Vanhoof

to appear in TOPLAS

We have performed an experimental evaluation focusing on cost and precision of our techniques based on a collection of 45 typed logic programs. The Table below summarises these experiments. Also by clicking on the program name you will be forwarded to the relevant part in the detailed information section which provides a detailed information about the corresponding analyses.

The experiments were performed using SICStus 3.10.0 running on an Intel Pentium III 933MHz, 640MB RAM, Linux 2.4.22. For all analyses, the analyser is set to allow 2 iterations before applying widening (except for mergesort where 4 iterations are allowed). Note that the only operation performed manually is the addition of the type declarations.

The first column of the Table indicates the benchmark program name. The columns headed ll and ts indicate the analysis times (in milliseconds) using the list-length and term-size norms respectively. The column headed tsxll specifies the analysis time for the combined list-length and term-sizeanalysis. Similarly, the columns headed T1,...,T4 indicate the analysis times using type-based norms for the (up to four) data-types defined in the programs. The column headed T1-4 indicates the analysis time using the corresponding combined type-based norms. Finally the column headed Reference indicate the publication from which the corresponding program was taken.

The columns tsxll and T1-4 include a precision comparison also. The precision is measured in terms of the size of the class of initial queries for which termination can be guaranteed. The colour    in the column tsxll indicates for a combined analysis that it is more precise than each of the corresponding individual analyses. The colour    in the column T1-4 indicates for a combined type-based analysis that it is more precise than each of the corresponding individual type-based analyses. The colour    in the T1-4 column indicates that the combined type-based analysis, is more precise than the combined list-length and term-size analysis. Finally the color    in the first column indicates that the number of abstract binary clauses has increased (by one) in the combined analyses with respect to the maximal number in the corresponding individual analyses.

Below you will find a detailed information about the analyses of each program which includes: (1) the terminating modes inferred by the analyses based on several settings; (2) a link to the program's source; and (3) a link though which you can activate the analyser for each setting.

The terminating modes are given in the form p(L₁,...,L_n) where each L_i is a list of norms, this mode describes a class of terminating initial queries where the i-th argument must be a rigid with respect to all norms in L_i. Here tt stands for term-size and ll for list-length.

ANALYSES OF append.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

app([ll],[],[])
app([],[],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

app([tt],[],[])
app([],[],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

app([list],[],[])
app([],[],[list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

app([poly],[],[])
app([],[],[poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

app([list],[],[])
app([poly],[],[])
app([],[],[list])
app([],[],[poly])

ANALYSES OF delete.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

delmin([tt],[],[])
delmin([],[],[tt])
less([tt],[])
less([],[tt])
delete([],[tt],[])
delete([],[],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

delmin([tt],[],[])
delmin([],[],[tt])
less([tt],[])
less([],[tt])
delete([],[tt],[])
delete([],[],[tt])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

delmin([nat],[],[])
delmin([],[],[nat])
less([nat],[])
less([],[nat])
delete([],[nat],[])
delete([],[],[nat])

Analysis wrt: treen   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

delmin([treen],[],[])
delmin([],[],[treen])

Analysis wrt: nat,treen   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

delmin([nat],[],[])
delmin([treen],[],[])
delmin([],[],[nat])
delmin([],[],[treen])
less([nat],[])
less([],[nat])
delete([nat],[nat],[])
delete([nat],[treen],[])
delete([nat],[],[nat])
delete([nat],[],[treen])
delete([],[nat],[])
delete([],[],[nat])

ANALYSES OF frontier.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([ll],[],[])
app([],[],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([tt],[],[])
app([],[],[tt])
front([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
front([tt],[])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([list],[],[])
app([],[],[list])

Analysis wrt: tree   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([poly],[],[])
app([],[],[poly])
front([poly],[])

Analysis wrt: list,tree,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([list],[],[])
app([poly],[],[])
app([],[],[list])
app([],[],[poly])
front([tree],[])
front([poly],[])

ANALYSES OF in.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([tt],[])
less([],[tt])
in([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([tt],[])
less([],[tt])
in([],[tt])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([nat],[])
less([],[nat])
in([],[nat])

Analysis wrt: treen   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: nat,treen   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([nat],[])
less([],[nat])
in([nat],[nat])
in([nat],[treen])
in([],[nat])

ANALYSES OF inorder.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([ll],[],[])
app([],[],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([tt],[],[])
app([],[],[tt])
in_order([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
in_order([tt],[])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([list],[],[])
app([],[],[list])

Analysis wrt: tree   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([poly],[],[])
app([],[],[poly])
in_order([poly],[])

Analysis wrt: list,tree,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([list],[],[])
app([poly],[],[])
app([],[],[list])
app([],[],[poly])
in_order([tree],[])
in_order([poly],[])

ANALYSES OF insert.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([tt],[])
less([],[tt])
insert([],[tt],[])
insert([],[],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([tt],[])
less([],[tt])
insert([],[tt],[])
insert([],[],[tt])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([nat],[])
less([],[nat])
insert([],[nat],[])
insert([],[],[nat])

Analysis wrt: treen   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: nat,treen   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([nat],[])
less([],[nat])
insert([nat],[nat],[])
insert([nat],[treen],[])
insert([nat],[],[nat])
insert([nat],[],[treen])
insert([],[nat],[])
insert([],[],[nat])

ANALYSES OF length.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

len([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

len([tt],[])
len([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

len([tt],[])
len([ll],[])
len([],[tt])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

len([list],[])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

len([],[nat])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

len([poly],[])

Analysis wrt: list,nat,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

len([list],[])
len([poly],[])
len([],[nat])

ANALYSES OF length1.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

eq([],[])
len1([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

eq([],[])
len1([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

eq([],[])
len1([tt],[])
len1([ll],[])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

eq([],[])
len1([list],[])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

eq([],[])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

eq([],[])
len1([poly],[])

Analysis wrt: list,nat,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

eq([],[])
len1([list],[])
len1([poly],[])

ANALYSES OF less.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

less([tt],[])
less([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

less([tt],[])
less([],[tt])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

less([nat],[])
less([],[nat])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

less([nat],[])
less([],[nat])

ANALYSES OF list.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

list([ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

list([tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

list([tt])
list([ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

list([list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

list([poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

list([list])
list([poly])

ANALYSES OF map_color.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

select([],[ll],[])
select([],[],[ll])
member([],[ll])
subset([ll],[ll])
map([])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

select([],[tt],[])
select([],[],[tt])
member([],[tt])
subset([tt],[tt])
color_region([tt],[tt])
color_map([tt],[tt])
map([])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

select([],[tt],[])
select([],[ll],[])
select([],[],[tt])
select([],[],[ll])
member([],[tt])
member([],[ll])
subset([tt],[tt])
subset([tt],[ll])
subset([ll],[tt])
subset([ll],[ll])
color_region([tt],[tt])
color_region([tt],[ll])
color_map([tt],[tt])
color_map([tt],[ll])
map([])

Analysis wrt: listc   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

select([],[listc],[])
select([],[],[listc])
member([],[listc])
subset([listc],[listc])
color_region([listc],[listc])
color_map([listc],[listc])
map([])

Analysis wrt: color   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

select([],[color],[])
select([],[],[color])
member([],[color])
subset([color],[color])
color_region([color],[color])
color_map([color],[color])
map([])

Analysis wrt: listr   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

map([])

Analysis wrt: region   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

map([])

Analysis wrt: listc,color,listr,region   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

select([],[listc],[])
select([],[color],[])
select([],[],[listc])
select([],[],[color])
member([],[listc])
member([],[color])
subset([listc],[listc])
subset([listc],[color])
subset([color],[listc])
subset([color],[color])
color_region([listc],[listc])
color_region([listc],[color])
color_region([color],[listc])
color_region([color],[color])
color_map([listc],[listc])
color_map([listc],[color])
color_map([color],[listc])
color_map([color],[color])
query
map([])

ANALYSES OF maximum.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

less([tt],[])
less([],[tt])
max([tt],[],[])
max([],[tt],[])
max([],[],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

less([tt],[])
less([],[tt])
max([tt],[],[])
max([],[tt],[])
max([],[],[tt])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

less([nat],[])
less([],[nat])
max([nat],[],[])
max([],[nat],[])
max([],[],[nat])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

less([nat],[])
less([],[nat])
max([nat],[],[])
max([],[nat],[])
max([],[],[nat])

ANALYSES OF member.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

member([],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

member([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

member([],[tt])
member([],[ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

member([],[list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

member([],[poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

member([],[list])
member([],[poly])

ANALYSES OF mergesort.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 11

Terminating modes:

split([ll],[],[])
split([],[ll],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 12

Terminating modes:

less([tt],[])
less([],[tt])
merge([tt],[tt],[])
merge([tt],[],[tt])
merge([],[],[tt])
split([tt],[],[])
split([],[tt],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 12

Terminating modes:

less([tt],[])
less([],[tt])
merge([tt],[tt],[])
merge([tt],[ll],[])
merge([tt],[],[tt])
merge([tt],[],[ll])
merge([ll],[tt],[])
merge([ll],[],[tt])
merge([],[tt],[tt])
merge([],[tt],[ll])
merge([],[],[tt])
split([tt],[],[])
split([ll],[],[])
split([],[ll,tt],[ll,tt])
ms([tt],[])

Analysis wrt: listn   (Run the Analyser)

Detailed runtime:

Number of binary clause: 11

Terminating modes:

split([listn],[],[])
split([],[listn],[listn])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 11

Terminating modes:

less([nat],[])
less([],[nat])
merge([nat],[nat],[])
merge([nat],[],[nat])
merge([],[],[nat])
split([nat],[],[])
split([],[nat],[nat])

Analysis wrt: listn,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 11

Terminating modes:

less([nat],[])
less([],[nat])
merge([nat,listn],[listn],[])
merge([nat,listn],[nat],[])
merge([nat,listn],[],[listn])
merge([nat,listn],[],[nat])
merge([listn],[nat],[])
merge([listn],[],[nat])
merge([nat],[listn],[])
merge([nat],[nat],[])
merge([nat],[],[listn])
merge([nat],[],[nat])
merge([],[nat],[listn])
merge([],[nat],[nat])
merge([],[],[nat])
split([listn],[],[])
split([nat],[],[])
split([],[nat,listn],[nat,listn])
ms([nat],[])

ANALYSES OF minimum.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

minimum([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

minimum([tt],[])

Analysis wrt: tree   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

minimum([tree],[])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

minimum([poly],[])

Analysis wrt: tree,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

minimum([tree],[])
minimum([poly],[])

ANALYSES OF mult.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

sum([],[tt],[])
sum([],[],[tt])
mult([tt],[tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

sum([],[tt],[])
sum([],[],[tt])
mult([tt],[tt],[])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

sum([],[nat],[])
sum([],[],[nat])
mult([nat],[nat],[])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

sum([],[nat],[])
sum([],[],[nat])
mult([nat],[nat],[])

ANALYSES OF naive_reverse.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([ll],[],[])
app([],[],[ll])
rev([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([tt],[],[])
app([],[],[tt])
rev([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
rev([tt],[])
rev([ll],[])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([list],[],[])
app([],[],[list])
rev([list],[])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([poly],[],[])
app([],[],[poly])
rev([poly],[])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([list],[],[])
app([poly],[],[])
app([],[],[list])
app([],[],[poly])
rev([list],[])
rev([poly],[])

ANALYSES OF numeral.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

num([tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

num([tt])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

num([nat])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

num([nat])

ANALYSES OF ordered.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

less([tt],[])
less([],[tt])
ordered([tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

less([tt],[])
less([],[tt])
ordered([tt])

Analysis wrt: listn   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

less([nat],[])
less([],[nat])
ordered([nat])

Analysis wrt: listn,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

less([nat],[])
less([],[nat])
ordered([nat])

ANALYSES OF palindrome.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

reverse([ll],[],[])
reverse([ll],[])
palindrome([ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

reverse([tt],[],[])
reverse([tt],[])
palindrome([tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

reverse([tt],[],[])
reverse([ll],[],[])
reverse([tt],[])
reverse([ll],[])
palindrome([tt])
palindrome([ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

reverse([list],[],[])
reverse([list],[])
palindrome([list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

reverse([poly],[],[])
reverse([poly],[])
palindrome([poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

reverse([list],[],[])
reverse([poly],[],[])
reverse([list],[])
reverse([poly],[])
palindrome([list])
palindrome([poly])

ANALYSES OF permutation.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

app([ll],[],[])
app([],[],[ll])
perm([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

app([tt],[],[])
app([],[],[tt])
perm([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
perm([tt],[])
perm([ll],[])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

app([list],[],[])
app([],[],[list])
perm([list],[])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

app([poly],[],[])
app([],[],[poly])
perm([poly],[])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

app([list],[],[])
app([poly],[],[])
app([],[],[list])
app([],[],[poly])
perm([list],[])
perm([poly],[])

ANALYSES OF permutation1.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

select([],[ll],[])
select([],[],[ll])
perm1([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

select([],[tt],[])
select([],[],[tt])
perm1([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

select([],[tt],[])
select([],[ll],[])
select([],[],[tt])
select([],[],[ll])
perm1([tt],[])
perm1([ll],[])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

select([],[list],[])
select([],[],[list])
perm1([list],[])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

select([],[poly],[])
select([],[],[poly])
perm1([poly],[])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

select([],[list],[])
select([],[poly],[])
select([],[],[list])
select([],[],[poly])
perm1([list],[])
perm1([poly],[])

ANALYSES OF prefix.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([ll],[],[])
app([],[],[ll])
prefix([ll],[])
prefix([],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([tt],[],[])
app([],[],[tt])
prefix([tt],[])
prefix([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
prefix([tt],[])
prefix([ll],[])
prefix([],[tt])
prefix([],[ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([list],[],[])
app([],[],[list])
prefix([list],[])
prefix([],[list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([poly],[],[])
app([],[],[poly])
prefix([poly],[])
prefix([],[poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([list],[],[])
app([poly],[],[])
app([],[],[list])
app([],[],[poly])
prefix([list],[])
prefix([poly],[])
prefix([],[list])
prefix([],[poly])

ANALYSES OF quicksort.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

app([ll],[],[])
app([],[],[ll])
part([],[ll],[],[])
part([],[],[ll],[ll])
qs([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

app([tt],[],[])
app([],[],[tt])
part([],[tt],[],[])
part([],[],[tt],[tt])
less([tt],[])
less([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
part([],[tt],[],[])
part([],[ll],[],[])
part([],[],[tt],[tt])
part([],[],[tt],[ll])
part([],[],[ll],[tt])
part([],[],[ll],[ll])
qs([tt],[])
qs([ll],[])
less([tt],[])
less([],[tt])

Analysis wrt: listn   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

app([listn],[],[])
app([],[],[listn])
part([],[listn],[],[])
part([],[],[listn],[listn])
qs([listn],[])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

app([nat],[],[])
app([],[],[nat])
part([],[nat],[],[])
part([],[],[nat],[nat])
less([nat],[])
less([],[nat])

Analysis wrt: listn,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 8

Terminating modes:

app([listn],[],[])
app([nat],[],[])
app([],[],[listn])
app([],[],[nat])
part([],[listn],[],[])
part([],[nat],[],[])
part([],[],[listn],[listn])
part([],[],[listn],[nat])
part([],[],[nat],[listn])
part([],[],[nat],[nat])
qs([listn],[])
qs([nat],[])
less([nat],[])
less([],[nat])

ANALYSES OF reverse.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

reverse([ll],[],[])
reverse([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

reverse([tt],[],[])
reverse([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

reverse([tt],[],[])
reverse([ll],[],[])
reverse([tt],[])
reverse([ll],[])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

reverse([list],[],[])
reverse([list],[])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

reverse([poly],[],[])
reverse([poly],[])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

reverse([list],[],[])
reverse([poly],[],[])
reverse([list],[])
reverse([poly],[])

ANALYSES OF search_tree.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

less([tt],[])
less([],[tt])
search_tree([tt],[],[])
search_tree([tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

less([tt],[])
less([],[tt])
search_tree([tt],[],[])
search_tree([tt])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([nat],[])
less([],[nat])
search_tree([nat],[],[])
search_tree([nat])

Analysis wrt: treen   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

Analysis wrt: nat,treen   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

less([nat],[])
less([],[nat])
search_tree([nat],[],[])
search_tree([nat])

ANALYSES OF select.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

select([],[ll],[])
select([],[],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

select([],[tt],[])
select([],[],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

select([],[tt],[])
select([],[ll],[])
select([],[],[tt])
select([],[],[ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

select([],[list],[])
select([],[],[list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

select([],[poly],[])
select([],[],[poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

select([],[list],[])
select([],[poly],[])
select([],[],[list])
select([],[],[poly])

ANALYSES OF slowsort.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 9

Terminating modes:

app([ll],[],[])
app([],[],[ll])
perm([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 9

Terminating modes:

less([tt],[])
less([],[tt])
ordered([tt])
app([tt],[],[])
app([],[],[tt])
perm([tt],[])
ss([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 9

Terminating modes:

less([tt],[])
less([],[tt])
ordered([tt])
app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
perm([tt],[])
perm([ll],[])
ss([tt],[])
ss([ll],[tt])

Analysis wrt: listn   (Run the Analyser)

Detailed runtime:

Number of binary clause: 9

Terminating modes:

app([listn],[],[])
app([],[],[listn])
perm([listn],[])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 9

Terminating modes:

less([nat],[])
less([],[nat])
ordered([nat])
app([nat],[],[])
app([],[],[nat])
perm([nat],[])
ss([nat],[])

Analysis wrt: listn,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 9

Terminating modes:

less([nat],[])
less([],[nat])
ordered([nat])
app([listn],[],[])
app([nat],[],[])
app([],[],[listn])
app([],[],[nat])
perm([listn],[])
perm([nat],[])
ss([nat,listn],[])
ss([listn],[nat])
ss([nat],[])

ANALYSES OF sublist.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([ll],[],[])
app([],[],[ll])
sublist([],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([tt],[],[])
app([],[],[tt])
sublist([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
sublist([],[tt])
sublist([],[ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([list],[],[])
app([],[],[list])
sublist([],[list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([poly],[],[])
app([],[],[poly])
sublist([],[poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

app([list],[],[])
app([poly],[],[])
app([],[],[list])
app([],[],[poly])
sublist([],[list])
sublist([],[poly])

ANALYSES OF subset.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

member([],[ll])
subset([ll],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

member([],[tt])
subset([tt],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

member([],[tt])
member([],[ll])
subset([tt],[tt])
subset([tt],[ll])
subset([ll],[tt])
subset([ll],[ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

member([],[list])
subset([list],[list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

member([],[poly])
subset([poly],[poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

member([],[list])
member([],[poly])
subset([list],[list])
subset([list],[poly])
subset([poly],[list])
subset([poly],[poly])

ANALYSES OF suffix.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([ll],[],[])
app([],[],[ll])
suffix([],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([tt],[],[])
app([],[],[tt])
suffix([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([tt],[],[])
app([ll],[],[])
app([],[],[tt])
app([],[],[ll])
suffix([],[tt])
suffix([],[ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([list],[],[])
app([],[],[list])
suffix([],[list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([poly],[],[])
app([],[],[poly])
suffix([],[poly])

Analysis wrt: list,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

app([list],[],[])
app([poly],[],[])
app([],[],[list])
app([],[],[poly])
suffix([],[list])
suffix([],[poly])

ANALYSES OF sum.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

sum([],[tt],[])
sum([],[],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

sum([],[tt],[])
sum([],[],[tt])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

sum([],[nat],[])
sum([],[],[nat])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

sum([],[nat],[])
sum([],[],[nat])

ANALYSES OF tree.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

bin_tree([tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

bin_tree([tt])

Analysis wrt: tree   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

bin_tree([tree])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

bin_tree([poly])

Analysis wrt: tree,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

bin_tree([tree])
bin_tree([poly])

ANALYSES OF tree_member.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

tree_member([],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

tree_member([],[tt])

Analysis wrt: tree   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

tree_member([],[tree])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

tree_member([],[poly])

Analysis wrt: tree,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

tree_member([],[tree])
tree_member([],[poly])

ANALYSES OF factor.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

plus([tt],[],[])
plus([],[],[tt])
times([tt],[tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

plus([tt],[],[])
plus([],[],[tt])
times([tt],[tt],[])
factor([ll,tt],[])

Analysis wrt: listn   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

plus([nat],[],[])
plus([],[],[nat])
times([nat],[nat],[])

Analysis wrt: listn,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

plus([nat],[],[])
plus([],[],[nat])
times([nat],[nat],[])
factor([nat,listn],[])

ANALYSES OF flat.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

flat([ll],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

flat([tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

flat([tt],[])
flat([ll],[tt])
flat([ll],[ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

flat([list],[list])

Analysis wrt: list_2   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

flat([list_2],[])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

Analysis wrt: list,list_2,poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

flat([list_2,list],[])
flat([poly,list],[])
flat([list],[list])
flat([list],[list_2])
flat([list_2],[])

ANALYSES OF flatlength.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

append([ll],[],[])
append([],[],[ll])
fl([ll],[ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

append([tt],[],[])
append([],[],[tt])
fl([tt],[],[])
fl([],[tt],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

append([tt],[],[])
append([ll],[],[])
append([],[],[tt])
append([],[],[ll])
fl([tt],[],[])
fl([ll],[tt],[])
fl([ll],[ll],[])
fl([],[tt],[tt])
fl([],[ll],[tt])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

append([list],[],[])
append([],[],[list])
fl([list],[list],[])

Analysis wrt: list_2   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

append([list_2],[],[])
append([],[],[list_2])
fl([list_2],[],[])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

Analysis wrt: list,list_2,poly,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

append([list],[],[])
append([list_2],[],[])
append([],[],[list])
append([],[],[list_2])
fl([list_2,list],[],[])
fl([list],[list],[])
fl([list],[list_2],[])
fl([list_2],[],[])
fl([],[list],[nat])
fl([],[list_2],[nat])

ANALYSES OF g.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

app_1([ll],[],[])
app_1([],[],[ll])
app_2([ll],[],[])
app_2([],[],[ll])
eq([],[])
g([ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

app_1([tt],[],[])
app_1([],[],[tt])
app_2([tt],[],[])
app_2([],[],[tt])
eq([],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

app_1([tt],[],[])
app_1([ll],[],[])
app_1([],[],[tt])
app_1([],[],[ll])
app_2([tt],[],[])
app_2([ll],[],[])
app_2([],[],[tt])
app_2([],[],[ll])
eq([],[])
g([tt])
g([ll])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

app_1([list],[],[])
app_1([],[],[list])
eq([],[])

Analysis wrt: list_erk   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

app_1([list_erk],[],[])
app_1([],[],[list_erk])
app_2([list_erk],[],[])
app_2([],[],[list_erk])
eq([],[])
g([])

Analysis wrt: erk   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

app_2([erk],[],[])
app_2([],[],[erk])
eq([],[])

Analysis wrt: list,list_erk,erk   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

app_1([list],[],[])
app_1([list_erk],[],[])
app_1([],[],[list])
app_1([],[],[list_erk])
app_2([list_erk],[],[])
app_2([erk],[],[])
app_2([],[],[list_erk])
app_2([],[],[erk])
eq([],[])
g([])

ANALYSES OF p.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

p([ll,tt])

Analysis wrt: listn   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: listn,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

p([nat,listn])

ANALYSES OF t.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

ll([],[ll])
select([],[ll],[])
select([],[],[ll])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

ll([tt],[])
ll([],[tt])
select([],[tt],[])
select([],[],[tt])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

ll([tt],[])
ll([],[tt])
ll([],[ll])
select([],[tt],[])
select([],[ll],[])
select([],[],[tt])
select([],[],[ll])
t([tt])

Analysis wrt: list   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

ll([],[list])
select([],[list],[])
select([],[],[list])

Analysis wrt: poly   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

ll([],[poly])
select([],[poly],[])
select([],[],[poly])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

ll([nat],[])

Analysis wrt: list,poly,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

ll([nat],[])
ll([],[list])
ll([],[poly])
select([],[list],[])
select([],[poly],[])
select([],[],[list])
select([],[],[poly])
t([nat])

ANALYSES OF ackerman.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

ackermann([tt],[tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

ackermann([tt],[tt],[])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

ackermann([nat],[nat],[])

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

ackermann([nat],[nat],[])

ANALYSES OF der.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: dt   (Run the Analyser)

Detailed runtime:

Number of binary clause: 2

Terminating modes:

Analysis wrt: exp   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: num   (Run the Analyser)

Detailed runtime:

Number of binary clause: 1

Terminating modes:

Analysis wrt: dt,exp,num   (Run the Analyser)

Detailed runtime:

Number of binary clause: 3

Terminating modes:

p([exp,dt],[])

ANALYSES OF p_nonlin.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

sum([],[tt],[])
sum([],[],[tt])
mult([tt],[tt],[])

Analysis wrt: termsize_nodes,listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 7

Terminating modes:

sum([],[tt],[])
sum([],[],[tt])
mult([tt],[tt],[])
p([ll,tt])

Analysis wrt: listn   (Run the Analyser)

Detailed runtime:

Number of binary clause: 6

Terminating modes:

Analysis wrt: nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 5

Terminating modes:

sum([],[nat],[])
sum([],[],[nat])
mult([nat],[nat],[])

Analysis wrt: listn,nat   (Run the Analyser)

Detailed runtime:

Number of binary clause: 7

Terminating modes:

sum([],[nat],[])
sum([],[],[nat])
mult([nat],[nat],[])
p([nat,listn])

ANALYSES OF parse.pl   (View Source)

Analysis wrt: listlength   (Run the Analyser)

Detailed runtime:

Number of binary clause: 4

Terminating modes:

app([ll],[],[])
app([],[],[ll])
parse([ll],[])

Analysis wrt: termsize_nodes   (Run the Analyser)

Detailed runtime: