TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60001 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1199ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (89ms), PolynomialLinearRange4iUR (1971ms), DependencyGraph (84ms), PolynomialLinearRange8NegiUR (10001ms), DependencyGraph (59ms), ReductionPairSAT (2593ms), DependencyGraph (62ms), SizeChangePrinciple (timeout)].
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (40ms), PolynomialLinearRange4iUR (385ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (2ms), DependencyGraph (1ms), ReductionPairSAT (941ms), DependencyGraph (1ms)].
 | – Problem 7 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (10ms), PolynomialLinearRange4iUR (1291ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (29ms), DependencyGraph (7ms), ReductionPairSAT (1581ms), DependencyGraph (8ms)].

The following open problems remain:



Open Dependency Pair Problem 4

Dependency Pairs

activate#(n__sel(X1, X2))sel#(activate(X1), activate(X2))activate#(n__sel(X1, X2))activate#(X2)
activate#(n__s(X))activate#(X)activate#(n__sel(X1, X2))activate#(X1)
activate#(n__from(X))activate#(X)sel#(s(X), cons(Y, Z))sel#(X, activate(Z))
activate#(n__first(X1, X2))activate#(X2)activate#(n__first(X1, X2))first#(activate(X1), activate(X2))
activate#(n__first(X1, X2))activate#(X1)activate#(n__cons(X1, X2))activate#(X1)
sel#(s(X), cons(Y, Z))activate#(Z)first#(s(X), cons(Y, Z))activate#(Z)

Rewrite Rules

sel(s(X), cons(Y, Z))sel(X, activate(Z))sel(0, cons(X, Z))X
first(0, Z)nilfirst(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))
from(X)cons(X, n__from(n__s(X)))sel1(s(X), cons(Y, Z))sel1(X, activate(Z))
sel1(0, cons(X, Z))quote(X)first1(0, Z)nil1
first1(s(X), cons(Y, Z))cons1(quote(Y), first1(X, activate(Z)))quote(n__0)01
quote1(n__cons(X, Z))cons1(quote(activate(X)), quote1(activate(Z)))quote1(n__nil)nil1
quote(n__s(X))s1(quote(activate(X)))quote(n__sel(X, Z))sel1(activate(X), activate(Z))
quote1(n__first(X, Z))first1(activate(X), activate(Z))unquote(01)0
unquote(s1(X))s(unquote(X))unquote1(nil1)nil
unquote1(cons1(X, Z))fcons(unquote(X), unquote1(Z))fcons(X, Z)cons(X, Z)
first(X1, X2)n__first(X1, X2)from(X)n__from(X)
s(X)n__s(X)0n__0
cons(X1, X2)n__cons(X1, X2)niln__nil
sel(X1, X2)n__sel(X1, X2)activate(n__first(X1, X2))first(activate(X1), activate(X2))
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__0)0activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(n__sel(X1, X2))sel(activate(X1), activate(X2))
activate(X)X

Original Signature

Termination of terms over the following signature is verified: cons1, n__from, from, n__sel, n__s, activate, n__0, unquote, sel1, n__first, unquote1, quote, n__nil, cons, s1, fcons, 01, first1, n__cons, quote1, 0, s, nil1, first, sel, nil




Open Dependency Pair Problem 6

Dependency Pairs

quote1#(n__cons(X, Z))quote1#(activate(Z))

Rewrite Rules

sel(s(X), cons(Y, Z))sel(X, activate(Z))sel(0, cons(X, Z))X
first(0, Z)nilfirst(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))
from(X)cons(X, n__from(n__s(X)))sel1(s(X), cons(Y, Z))sel1(X, activate(Z))
sel1(0, cons(X, Z))quote(X)first1(0, Z)nil1
first1(s(X), cons(Y, Z))cons1(quote(Y), first1(X, activate(Z)))quote(n__0)01
quote1(n__cons(X, Z))cons1(quote(activate(X)), quote1(activate(Z)))quote1(n__nil)nil1
quote(n__s(X))s1(quote(activate(X)))quote(n__sel(X, Z))sel1(activate(X), activate(Z))
quote1(n__first(X, Z))first1(activate(X), activate(Z))unquote(01)0
unquote(s1(X))s(unquote(X))unquote1(nil1)nil
unquote1(cons1(X, Z))fcons(unquote(X), unquote1(Z))fcons(X, Z)cons(X, Z)
first(X1, X2)n__first(X1, X2)from(X)n__from(X)
s(X)n__s(X)0n__0
cons(X1, X2)n__cons(X1, X2)niln__nil
sel(X1, X2)n__sel(X1, X2)activate(n__first(X1, X2))first(activate(X1), activate(X2))
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__0)0activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(n__sel(X1, X2))sel(activate(X1), activate(X2))
activate(X)X

Original Signature

Termination of terms over the following signature is verified: cons1, n__from, from, n__sel, n__s, activate, n__0, unquote, sel1, n__first, unquote1, quote, n__nil, cons, s1, fcons, 01, first1, n__cons, quote1, 0, s, nil1, first, sel, nil




Open Dependency Pair Problem 7

Dependency Pairs

sel1#(s(X), cons(Y, Z))sel1#(X, activate(Z))quote#(n__s(X))quote#(activate(X))
quote#(n__sel(X, Z))sel1#(activate(X), activate(Z))sel1#(0, cons(X, Z))quote#(X)

Rewrite Rules

sel(s(X), cons(Y, Z))sel(X, activate(Z))sel(0, cons(X, Z))X
first(0, Z)nilfirst(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))
from(X)cons(X, n__from(n__s(X)))sel1(s(X), cons(Y, Z))sel1(X, activate(Z))
sel1(0, cons(X, Z))quote(X)first1(0, Z)nil1
first1(s(X), cons(Y, Z))cons1(quote(Y), first1(X, activate(Z)))quote(n__0)01
quote1(n__cons(X, Z))cons1(quote(activate(X)), quote1(activate(Z)))quote1(n__nil)nil1
quote(n__s(X))s1(quote(activate(X)))quote(n__sel(X, Z))sel1(activate(X), activate(Z))
quote1(n__first(X, Z))first1(activate(X), activate(Z))unquote(01)0
unquote(s1(X))s(unquote(X))unquote1(nil1)nil
unquote1(cons1(X, Z))fcons(unquote(X), unquote1(Z))fcons(X, Z)cons(X, Z)
first(X1, X2)n__first(X1, X2)from(X)n__from(X)
s(X)n__s(X)0n__0
cons(X1, X2)n__cons(X1, X2)niln__nil
sel(X1, X2)n__sel(X1, X2)activate(n__first(X1, X2))first(activate(X1), activate(X2))
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__0)0activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(n__sel(X1, X2))sel(activate(X1), activate(X2))
activate(X)X

Original Signature

Termination of terms over the following signature is verified: cons1, n__from, from, n__sel, n__s, activate, n__0, unquote, sel1, n__first, unquote1, quote, n__nil, cons, s1, fcons, 01, first1, n__cons, quote1, 0, s, nil1, first, sel, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

quote#(n__sel(X, Z))activate#(X)activate#(n__sel(X1, X2))activate#(X2)
quote1#(n__first(X, Z))activate#(Z)activate#(n__s(X))activate#(X)
quote1#(n__cons(X, Z))quote#(activate(X))activate#(n__sel(X1, X2))activate#(X1)
sel#(s(X), cons(Y, Z))sel#(X, activate(Z))activate#(n__first(X1, X2))activate#(X2)
quote1#(n__first(X, Z))activate#(X)unquote1#(cons1(X, Z))fcons#(unquote(X), unquote1(Z))
activate#(n__first(X1, X2))first#(activate(X1), activate(X2))activate#(n__first(X1, X2))activate#(X1)
activate#(n__cons(X1, X2))cons#(activate(X1), X2)activate#(n__cons(X1, X2))activate#(X1)
unquote1#(cons1(X, Z))unquote1#(Z)first#(s(X), cons(Y, Z))activate#(Z)
sel#(s(X), cons(Y, Z))activate#(Z)quote#(n__sel(X, Z))sel1#(activate(X), activate(Z))
first#(0, Z)nil#quote1#(n__cons(X, Z))activate#(X)
first1#(s(X), cons(Y, Z))first1#(X, activate(Z))first1#(s(X), cons(Y, Z))activate#(Z)
sel1#(0, cons(X, Z))quote#(X)fcons#(X, Z)cons#(X, Z)
quote1#(n__cons(X, Z))activate#(Z)activate#(n__sel(X1, X2))sel#(activate(X1), activate(X2))
sel1#(s(X), cons(Y, Z))activate#(Z)unquote#(s1(X))unquote#(X)
first1#(s(X), cons(Y, Z))quote#(Y)quote#(n__s(X))activate#(X)
activate#(n__from(X))activate#(X)unquote1#(nil1)nil#
quote1#(n__first(X, Z))first1#(activate(X), activate(Z))unquote1#(cons1(X, Z))unquote#(X)
unquote#(01)0#unquote#(s1(X))s#(unquote(X))
quote#(n__sel(X, Z))activate#(Z)sel1#(s(X), cons(Y, Z))sel1#(X, activate(Z))
activate#(n__nil)nil#quote#(n__s(X))quote#(activate(X))
from#(X)cons#(X, n__from(n__s(X)))first#(s(X), cons(Y, Z))cons#(Y, n__first(X, activate(Z)))
activate#(n__from(X))from#(activate(X))activate#(n__0)0#
activate#(n__s(X))s#(activate(X))quote1#(n__cons(X, Z))quote1#(activate(Z))

Rewrite Rules

sel(s(X), cons(Y, Z))sel(X, activate(Z))sel(0, cons(X, Z))X
first(0, Z)nilfirst(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))
from(X)cons(X, n__from(n__s(X)))sel1(s(X), cons(Y, Z))sel1(X, activate(Z))
sel1(0, cons(X, Z))quote(X)first1(0, Z)nil1
first1(s(X), cons(Y, Z))cons1(quote(Y), first1(X, activate(Z)))quote(n__0)01
quote1(n__cons(X, Z))cons1(quote(activate(X)), quote1(activate(Z)))quote1(n__nil)nil1
quote(n__s(X))s1(quote(activate(X)))quote(n__sel(X, Z))sel1(activate(X), activate(Z))
quote1(n__first(X, Z))first1(activate(X), activate(Z))unquote(01)0
unquote(s1(X))s(unquote(X))unquote1(nil1)nil
unquote1(cons1(X, Z))fcons(unquote(X), unquote1(Z))fcons(X, Z)cons(X, Z)
first(X1, X2)n__first(X1, X2)from(X)n__from(X)
s(X)n__s(X)0n__0
cons(X1, X2)n__cons(X1, X2)niln__nil
sel(X1, X2)n__sel(X1, X2)activate(n__first(X1, X2))first(activate(X1), activate(X2))
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__0)0activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(n__sel(X1, X2))sel(activate(X1), activate(X2))
activate(X)X

Original Signature

Termination of terms over the following signature is verified: cons1, n__from, from, n__sel, activate, n__s, unquote, n__0, sel1, unquote1, n__first, quote, n__nil, cons, s1, fcons, 01, first1, n__cons, quote1, 0, s, nil1, first, sel, nil

Strategy


The following SCCs where found

unquote1#(cons1(X, Z)) → unquote1#(Z)

unquote#(s1(X)) → unquote#(X)

activate#(n__first(X1, X2)) → first#(activate(X1), activate(X2))activate#(n__first(X1, X2)) → activate#(X1)
activate#(n__cons(X1, X2)) → activate#(X1)activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2))
first#(s(X), cons(Y, Z)) → activate#(Z)sel#(s(X), cons(Y, Z)) → activate#(Z)
activate#(n__sel(X1, X2)) → activate#(X2)activate#(n__s(X)) → activate#(X)
activate#(n__sel(X1, X2)) → activate#(X1)activate#(n__from(X)) → activate#(X)
sel#(s(X), cons(Y, Z)) → sel#(X, activate(Z))activate#(n__first(X1, X2)) → activate#(X2)

sel1#(s(X), cons(Y, Z)) → sel1#(X, activate(Z))quote#(n__s(X)) → quote#(activate(X))
quote#(n__sel(X, Z)) → sel1#(activate(X), activate(Z))sel1#(0, cons(X, Z)) → quote#(X)

first1#(s(X), cons(Y, Z)) → first1#(X, activate(Z))

quote1#(n__cons(X, Z)) → quote1#(activate(Z))

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

unquote#(s1(X))unquote#(X)

Rewrite Rules

sel(s(X), cons(Y, Z))sel(X, activate(Z))sel(0, cons(X, Z))X
first(0, Z)nilfirst(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))
from(X)cons(X, n__from(n__s(X)))sel1(s(X), cons(Y, Z))sel1(X, activate(Z))
sel1(0, cons(X, Z))quote(X)first1(0, Z)nil1
first1(s(X), cons(Y, Z))cons1(quote(Y), first1(X, activate(Z)))quote(n__0)01
quote1(n__cons(X, Z))cons1(quote(activate(X)), quote1(activate(Z)))quote1(n__nil)nil1
quote(n__s(X))s1(quote(activate(X)))quote(n__sel(X, Z))sel1(activate(X), activate(Z))
quote1(n__first(X, Z))first1(activate(X), activate(Z))unquote(01)0
unquote(s1(X))s(unquote(X))unquote1(nil1)nil
unquote1(cons1(X, Z))fcons(unquote(X), unquote1(Z))fcons(X, Z)cons(X, Z)
first(X1, X2)n__first(X1, X2)from(X)n__from(X)
s(X)n__s(X)0n__0
cons(X1, X2)n__cons(X1, X2)niln__nil
sel(X1, X2)n__sel(X1, X2)activate(n__first(X1, X2))first(activate(X1), activate(X2))
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__0)0activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(n__sel(X1, X2))sel(activate(X1), activate(X2))
activate(X)X

Original Signature

Termination of terms over the following signature is verified: cons1, n__from, from, n__sel, activate, n__s, unquote, n__0, sel1, unquote1, n__first, quote, n__nil, cons, s1, fcons, 01, first1, n__cons, quote1, 0, s, nil1, first, sel, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

unquote#(s1(X))unquote#(X)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

unquote1#(cons1(X, Z))unquote1#(Z)

Rewrite Rules

sel(s(X), cons(Y, Z))sel(X, activate(Z))sel(0, cons(X, Z))X
first(0, Z)nilfirst(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))
from(X)cons(X, n__from(n__s(X)))sel1(s(X), cons(Y, Z))sel1(X, activate(Z))
sel1(0, cons(X, Z))quote(X)first1(0, Z)nil1
first1(s(X), cons(Y, Z))cons1(quote(Y), first1(X, activate(Z)))quote(n__0)01
quote1(n__cons(X, Z))cons1(quote(activate(X)), quote1(activate(Z)))quote1(n__nil)nil1
quote(n__s(X))s1(quote(activate(X)))quote(n__sel(X, Z))sel1(activate(X), activate(Z))
quote1(n__first(X, Z))first1(activate(X), activate(Z))unquote(01)0
unquote(s1(X))s(unquote(X))unquote1(nil1)nil
unquote1(cons1(X, Z))fcons(unquote(X), unquote1(Z))fcons(X, Z)cons(X, Z)
first(X1, X2)n__first(X1, X2)from(X)n__from(X)
s(X)n__s(X)0n__0
cons(X1, X2)n__cons(X1, X2)niln__nil
sel(X1, X2)n__sel(X1, X2)activate(n__first(X1, X2))first(activate(X1), activate(X2))
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__0)0activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(n__sel(X1, X2))sel(activate(X1), activate(X2))
activate(X)X

Original Signature

Termination of terms over the following signature is verified: cons1, n__from, from, n__sel, activate, n__s, unquote, n__0, sel1, unquote1, n__first, quote, n__nil, cons, s1, fcons, 01, first1, n__cons, quote1, 0, s, nil1, first, sel, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

unquote1#(cons1(X, Z))unquote1#(Z)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

first1#(s(X), cons(Y, Z))first1#(X, activate(Z))

Rewrite Rules

sel(s(X), cons(Y, Z))sel(X, activate(Z))sel(0, cons(X, Z))X
first(0, Z)nilfirst(s(X), cons(Y, Z))cons(Y, n__first(X, activate(Z)))
from(X)cons(X, n__from(n__s(X)))sel1(s(X), cons(Y, Z))sel1(X, activate(Z))
sel1(0, cons(X, Z))quote(X)first1(0, Z)nil1
first1(s(X), cons(Y, Z))cons1(quote(Y), first1(X, activate(Z)))quote(n__0)01
quote1(n__cons(X, Z))cons1(quote(activate(X)), quote1(activate(Z)))quote1(n__nil)nil1
quote(n__s(X))s1(quote(activate(X)))quote(n__sel(X, Z))sel1(activate(X), activate(Z))
quote1(n__first(X, Z))first1(activate(X), activate(Z))unquote(01)0
unquote(s1(X))s(unquote(X))unquote1(nil1)nil
unquote1(cons1(X, Z))fcons(unquote(X), unquote1(Z))fcons(X, Z)cons(X, Z)
first(X1, X2)n__first(X1, X2)from(X)n__from(X)
s(X)n__s(X)0n__0
cons(X1, X2)n__cons(X1, X2)niln__nil
sel(X1, X2)n__sel(X1, X2)activate(n__first(X1, X2))first(activate(X1), activate(X2))
activate(n__from(X))from(activate(X))activate(n__s(X))s(activate(X))
activate(n__0)0activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(n__sel(X1, X2))sel(activate(X1), activate(X2))
activate(X)X

Original Signature

Termination of terms over the following signature is verified: cons1, n__from, from, n__sel, activate, n__s, unquote, n__0, sel1, unquote1, n__first, quote, n__nil, cons, s1, fcons, 01, first1, n__cons, quote1, 0, s, nil1, first, sel, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

first1#(s(X), cons(Y, Z))first1#(X, activate(Z))