YES
(VAR X Y Z X1 X2 X3)
(RULES 
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)
)

Proving termination of rewriting for Ex15_Luc98_iGM:

-> Dependency pairs:
nF_active(and(true,X)) -> nF_mark(X)
nF_active(and(false,Y)) -> nF_mark(false)
nF_active(if(true,X,Y)) -> nF_mark(X)
nF_active(if(false,X,Y)) -> nF_mark(Y)
nF_active(add(0,X)) -> nF_mark(X)
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_active(add(s(X),Y)) -> nF_s(add(X,Y))
nF_active(add(s(X),Y)) -> nF_add(X,Y)
nF_active(first(0,X)) -> nF_mark(nil)
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_active(first(s(X),cons(Y,Z))) -> nF_cons(Y,first(X,Z))
nF_active(first(s(X),cons(Y,Z))) -> nF_first(X,Z)
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_active(from(X)) -> nF_cons(X,from(s(X)))
nF_active(from(X)) -> nF_from(s(X))
nF_active(from(X)) -> nF_s(X)
nF_mark(and(X1,X2)) -> nF_active(and(mark(X1),X2))
nF_mark(and(X1,X2)) -> nF_and(mark(X1),X2)
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(true) -> nF_active(true)
nF_mark(false) -> nF_active(false)
nF_mark(if(X1,X2,X3)) -> nF_active(if(mark(X1),X2,X3))
nF_mark(if(X1,X2,X3)) -> nF_if(mark(X1),X2,X3)
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_mark(add(X1,X2)) -> nF_add(mark(X1),X2)
nF_mark(add(X1,X2)) -> nF_mark(X1)
nF_mark(0) -> nF_active(0)
nF_mark(s(X)) -> nF_active(s(X))
nF_mark(s(X)) -> nF_s(X)
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_mark(first(X1,X2)) -> nF_first(mark(X1),mark(X2))
nF_mark(first(X1,X2)) -> nF_mark(X1)
nF_mark(first(X1,X2)) -> nF_mark(X2)
nF_mark(nil) -> nF_active(nil)
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_mark(cons(X1,X2)) -> nF_cons(X1,X2)
nF_mark(from(X)) -> nF_active(from(X))
nF_mark(from(X)) -> nF_from(X)
nF_and(mark(X1),X2) -> nF_and(X1,X2)
nF_and(X1,mark(X2)) -> nF_and(X1,X2)
nF_and(active(X1),X2) -> nF_and(X1,X2)
nF_and(X1,active(X2)) -> nF_and(X1,X2)
nF_if(mark(X1),X2,X3) -> nF_if(X1,X2,X3)
nF_if(X1,mark(X2),X3) -> nF_if(X1,X2,X3)
nF_if(X1,X2,mark(X3)) -> nF_if(X1,X2,X3)
nF_if(active(X1),X2,X3) -> nF_if(X1,X2,X3)
nF_if(X1,active(X2),X3) -> nF_if(X1,X2,X3)
nF_if(X1,X2,active(X3)) -> nF_if(X1,X2,X3)
nF_add(mark(X1),X2) -> nF_add(X1,X2)
nF_add(X1,mark(X2)) -> nF_add(X1,X2)
nF_add(active(X1),X2) -> nF_add(X1,X2)
nF_add(X1,active(X2)) -> nF_add(X1,X2)
nF_s(mark(X)) -> nF_s(X)
nF_s(active(X)) -> nF_s(X)
nF_first(mark(X1),X2) -> nF_first(X1,X2)
nF_first(X1,mark(X2)) -> nF_first(X1,X2)
nF_first(active(X1),X2) -> nF_first(X1,X2)
nF_first(X1,active(X2)) -> nF_first(X1,X2)
nF_cons(mark(X1),X2) -> nF_cons(X1,X2)
nF_cons(X1,mark(X2)) -> nF_cons(X1,X2)
nF_cons(active(X1),X2) -> nF_cons(X1,X2)
nF_cons(X1,active(X2)) -> nF_cons(X1,X2)
nF_from(mark(X)) -> nF_from(X)
nF_from(active(X)) -> nF_from(X)

-> Proof of termination for Ex15_Luc98_iGM_1_1:
-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(from(X)) -> nF_active(from(X))
nF_mark(first(X1,X2)) -> nF_mark(X2)
nF_mark(first(X1,X2)) -> nF_mark(X1)
nF_mark(add(X1,X2)) -> nF_mark(X1)
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_active(if(false,X,Y)) -> nF_mark(Y)
nF_mark(if(X1,X2,X3)) -> nF_active(if(mark(X1),X2,X3))
nF_active(if(true,X,Y)) -> nF_mark(X)
nF_mark(and(X1,X2)) -> nF_active(and(mark(X1),X2))

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2
[true] = 1
[mark](X) = X
[false] = 0
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[add](X1,X2) = X1 + X2 + 1
[0] = 1
[s](X) = 0
[first](X1,X2) = X1 + X2 + 1
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X + 1

TIME: 8.9648e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(if(X1,X2,X3)) -> nF_active(if(mark(X1),X2,X3))
nF_active(if(true,X,Y)) -> nF_mark(X)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_active(if(false,X,Y)) -> nF_mark(Y)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(from(X)) -> nF_active(from(X))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)
nF_mark(add(X1,X2)) -> nF_mark(X1)
nF_mark(first(X1,X2)) -> nF_mark(X1)
nF_mark(first(X1,X2)) -> nF_mark(X2)

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[add](X1,X2) = X1 + X2 + 1
[0] = 1
[s](X) = 0
[first](X1,X2) = X1 + X2 + 1
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 9.9342e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(from(X)) -> nF_active(from(X))
nF_mark(first(X1,X2)) -> nF_mark(X1)
nF_mark(add(X1,X2)) -> nF_mark(X1)
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_active(if(false,X,Y)) -> nF_mark(Y)
nF_mark(if(X1,X2,X3)) -> nF_active(if(mark(X1),X2,X3))
nF_active(if(true,X,Y)) -> nF_mark(X)

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 0
[mark](X) = X
[false] = 0
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[add](X1,X2) = X1 + X2 + 1
[0] = 0
[s](X) = 0
[first](X1,X2) = X1 + 1
[nil] = 1
[cons](X1,X2) = 1
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 9.9069e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(if(X1,X2,X3)) -> nF_active(if(mark(X1),X2,X3))
nF_active(if(false,X,Y)) -> nF_mark(Y)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(from(X)) -> nF_active(from(X))
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)
nF_mark(add(X1,X2)) -> nF_mark(X1)
nF_mark(first(X1,X2)) -> nF_mark(X1)

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[add](X1,X2) = X1 + X2 + 1
[0] = 1
[s](X) = 0
[first](X1,X2) = X1 + 1
[nil] = 0
[cons](X1,X2) = 1
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 0.10139699999999996

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(from(X)) -> nF_active(from(X))
nF_mark(add(X1,X2)) -> nF_mark(X1)
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_active(if(false,X,Y)) -> nF_mark(Y)
nF_mark(if(X1,X2,X3)) -> nF_active(if(mark(X1),X2,X3))

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X1 + X2 + X3
[add](X1,X2) = X1 + X2 + 1
[0] = 1
[s](X) = 1
[first](X1,X2) = X1
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X + 1

TIME: 0.100301

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_active(if(false,X,Y)) -> nF_mark(Y)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(from(X)) -> nF_active(from(X))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)
nF_mark(add(X1,X2)) -> nF_mark(X1)

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[add](X1,X2) = X1 + X2 + 1
[0] = 1
[s](X) = 0
[first](X1,X2) = X1 + 1
[nil] = 0
[cons](X1,X2) = 1
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 9.8963e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(from(X)) -> nF_active(from(X))
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_active(if(false,X,Y)) -> nF_mark(Y)

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[add](X1,X2) = X2
[0] = 0
[s](X) = 0
[first](X1,X2) = 1
[nil] = 1
[cons](X1,X2) = 1
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 9.9013e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(from(X)) -> nF_active(from(X))
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_mark(if(X1,X2,X3)) -> nF_mark(X1)

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X1 + X2 + X3 + 1
[add](X1,X2) = X2 + 1
[0] = 1
[s](X) = 0
[first](X1,X2) = X1 + 1
[nil] = 0
[cons](X1,X2) = 1
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 9.9598e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(from(X)) -> nF_active(from(X))
nF_mark(and(X1,X2)) -> nF_mark(X1)
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(add(X1,X2)) -> nF_active(add(mark(X1),X2))

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X2 + X3 + 1
[add](X1,X2) = X2 + 1
[0] = 1
[s](X) = 0
[first](X1,X2) = 1
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X + 1

TIME: 9.7757e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(from(X)) -> nF_active(from(X))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(and(X1,X2)) -> nF_mark(X1)

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X2 + X3 + 1
[add](X1,X2) = X2 + 1
[0] = 1
[s](X) = 0
[first](X1,X2) = X1 + 1
[nil] = 0
[cons](X1,X2) = 1
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 9.5948e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(from(X)) -> nF_active(from(X))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(0,X)) -> nF_mark(X)

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 1
[if](X1,X2,X3) = X2 + X3 + 1
[add](X1,X2) = X1 + X2
[0] = 1
[s](X) = 0
[first](X1,X2) = 0
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 0
[nF_active](X) = X
[nF_mark](X) = 0

TIME: 9.7326e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(from(X)) -> nF_active(from(X))

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X2 + 1
[true] = 0
[mark](X) = X
[false] = 0
[if](X1,X2,X3) = X2 + X3 + 1
[add](X1,X2) = X2 + 1
[0] = 0
[s](X) = 0
[first](X1,X2) = 1
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X + 1

TIME: 8.6444e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(s(X)) -> nF_active(s(X))
nF_active(add(s(X),Y)) -> nF_mark(s(add(X,Y)))

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 0
[if](X1,X2,X3) = X2 + X3 + 1
[add](X1,X2) = X2 + 1
[0] = 0
[s](X) = 0
[first](X1,X2) = 1
[nil] = 1
[cons](X1,X2) = 1
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 9.2917e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(cons(X1,X2)) -> nF_active(cons(X1,X2))

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = 1
[true] = 1
[mark](X) = 1
[false] = 1
[if](X1,X2,X3) = 1
[add](X1,X2) = 1
[0] = 1
[s](X) = 0
[first](X1,X2) = 1
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = 1

TIME: 9.230400000000005e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(s(X)) -> nF_active(s(X))
nF_active(first(s(X),cons(Y,Z))) -> nF_mark(cons(Y,first(X,Z)))

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = X
[and](X1,X2) = X1 + X2 + 1
[true] = 1
[mark](X) = X
[false] = 0
[if](X1,X2,X3) = X2 + X3 + 1
[add](X1,X2) = X1 + X2
[0] = 1
[s](X) = X + 1
[first](X1,X2) = X1
[nil] = 0
[cons](X1,X2) = X2
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 9.2771e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))
nF_mark(first(X1,X2)) -> nF_active(first(mark(X1),mark(X2)))

UsableRules:
active(and(true,X)) -> mark(X)
active(and(false,Y)) -> mark(false)
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(first(0,X)) -> mark(nil)
active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
active(from(X)) -> mark(cons(X,from(s(X))))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(true) -> active(true)
mark(false) -> active(false)
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(add(X1,X2)) -> active(add(mark(X1),X2))
mark(0) -> active(0)
mark(s(X)) -> active(s(X))
mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
mark(nil) -> active(nil)
mark(cons(X1,X2)) -> active(cons(X1,X2))
mark(from(X)) -> active(from(X))
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
first(mark(X1),X2) -> first(X1,X2)
first(X1,mark(X2)) -> first(X1,X2)
first(active(X1),X2) -> first(X1,X2)
first(X1,active(X2)) -> first(X1,X2)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = 0
[and](X1,X2) = 1
[true] = 0
[mark](X) = 0
[false] = 0
[if](X1,X2,X3) = 0
[add](X1,X2) = 0
[0] = 0
[s](X) = 0
[first](X1,X2) = 0
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = 1

TIME: 7.8775e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(s(X)) -> nF_active(s(X))
nF_active(from(X)) -> nF_mark(cons(X,from(s(X))))

UsableRules:
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
from(mark(X)) -> from(X)
from(active(X)) -> from(X)

Polynomial Interpretation:

[active](X) = 0
[and](X1,X2) = 0
[true] = 0
[mark](X) = 0
[false] = 0
[if](X1,X2,X3) = 0
[add](X1,X2) = 0
[0] = 0
[s](X) = 0
[first](X1,X2) = 0
[nil] = 0
[cons](X1,X2) = 0
[from](X) = 1
[nF_active](X) = X
[nF_mark](X) = 0

TIME: 4.7659e-2

-> -> Dependency pairs in cycle:
nF_active(and(true,X)) -> nF_mark(X)
nF_mark(s(X)) -> nF_active(s(X))

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex15_Luc98_iGM_1_2:
-> -> Dependency pairs in cycle:
nF_and(X1,active(X2)) -> nF_and(X1,X2)
nF_and(active(X1),X2) -> nF_and(X1,X2)
nF_and(X1,mark(X2)) -> nF_and(X1,X2)
nF_and(mark(X1),X2) -> nF_and(X1,X2)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_and(X1,active(X2)) -> nF_and(X1,X2)
nF_and(X1,mark(X2)) -> nF_and(X1,X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex15_Luc98_iGM_1_3:
-> -> Dependency pairs in cycle:
nF_if(X1,X2,active(X3)) -> nF_if(X1,X2,X3)
nF_if(X1,active(X2),X3) -> nF_if(X1,X2,X3)
nF_if(active(X1),X2,X3) -> nF_if(X1,X2,X3)
nF_if(X1,X2,mark(X3)) -> nF_if(X1,X2,X3)
nF_if(X1,mark(X2),X3) -> nF_if(X1,X2,X3)
nF_if(mark(X1),X2,X3) -> nF_if(X1,X2,X3)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_if(X1,X2,active(X3)) -> nF_if(X1,X2,X3)
nF_if(X1,mark(X2),X3) -> nF_if(X1,X2,X3)
nF_if(X1,X2,mark(X3)) -> nF_if(X1,X2,X3)
nF_if(X1,active(X2),X3) -> nF_if(X1,X2,X3)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_if(X1,X2,active(X3)) -> nF_if(X1,X2,X3)
nF_if(X1,X2,mark(X3)) -> nF_if(X1,X2,X3)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex15_Luc98_iGM_1_4:
-> -> Dependency pairs in cycle:
nF_add(X1,active(X2)) -> nF_add(X1,X2)
nF_add(active(X1),X2) -> nF_add(X1,X2)
nF_add(X1,mark(X2)) -> nF_add(X1,X2)
nF_add(mark(X1),X2) -> nF_add(X1,X2)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_add(X1,active(X2)) -> nF_add(X1,X2)
nF_add(X1,mark(X2)) -> nF_add(X1,X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex15_Luc98_iGM_1_5:
-> -> Dependency pairs in cycle:
nF_first(X1,active(X2)) -> nF_first(X1,X2)
nF_first(active(X1),X2) -> nF_first(X1,X2)
nF_first(X1,mark(X2)) -> nF_first(X1,X2)
nF_first(mark(X1),X2) -> nF_first(X1,X2)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_first(X1,active(X2)) -> nF_first(X1,X2)
nF_first(X1,mark(X2)) -> nF_first(X1,X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex15_Luc98_iGM_1_6:
-> -> Dependency pairs in cycle:
nF_cons(X1,active(X2)) -> nF_cons(X1,X2)
nF_cons(active(X1),X2) -> nF_cons(X1,X2)
nF_cons(X1,mark(X2)) -> nF_cons(X1,X2)
nF_cons(mark(X1),X2) -> nF_cons(X1,X2)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_cons(X1,active(X2)) -> nF_cons(X1,X2)
nF_cons(X1,mark(X2)) -> nF_cons(X1,X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex15_Luc98_iGM_1_7:
-> -> Dependency pairs in cycle:
nF_s(active(X)) -> nF_s(X)
nF_s(mark(X)) -> nF_s(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex15_Luc98_iGM_1_8:
-> -> Dependency pairs in cycle:
nF_from(active(X)) -> nF_from(X)
nF_from(mark(X)) -> nF_from(X)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.