YES

The TRS could be proven terminating. The proof took 1985 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (409ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4iUR (821ms).
 |    | – Problem 10 was processed with processor PolynomialLinearRange4iUR (476ms).
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (2ms).
 | – Problem 6 was processed with processor SubtermCriterion (29ms).
 | – Problem 7 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 9 was processed with processor SubtermCriterion (3ms).
 | – Problem 8 was processed with processor SubtermCriterion (21ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

active#(U11(X))active#(X)top#(ok(X))top#(active(X))
active#(__(__(X, Y), Z))__#(X, __(Y, Z))active#(U12(X))active#(X)
proper#(U11(X))proper#(X)top#(ok(X))active#(X)
U12#(mark(X))U12#(X)proper#(__(X1, X2))__#(proper(X1), proper(X2))
active#(isNePal(__(I, __(P, I))))U11#(tt)active#(U12(X))U12#(active(X))
active#(__(X1, X2))active#(X2)proper#(U11(X))U11#(proper(X))
active#(__(X1, X2))__#(X1, active(X2))active#(isNePal(X))isNePal#(active(X))
top#(mark(X))proper#(X)U11#(mark(X))U11#(X)
active#(__(X1, X2))__#(active(X1), X2)proper#(__(X1, X2))proper#(X1)
__#(mark(X1), X2)__#(X1, X2)active#(isNePal(X))active#(X)
top#(mark(X))top#(proper(X))active#(__(X1, X2))active#(X1)
proper#(U12(X))proper#(X)active#(U11(X))U11#(active(X))
__#(ok(X1), ok(X2))__#(X1, X2)active#(U11(tt))U12#(tt)
proper#(isNePal(X))proper#(X)proper#(U12(X))U12#(proper(X))
__#(X1, mark(X2))__#(X1, X2)active#(__(__(X, Y), Z))__#(Y, Z)
isNePal#(mark(X))isNePal#(X)proper#(__(X1, X2))proper#(X2)
isNePal#(ok(X))isNePal#(X)proper#(isNePal(X))isNePal#(proper(X))
U12#(ok(X))U12#(X)U11#(ok(X))U11#(X)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, active, __, U11, mark, U12, ok, proper, nil, top

Strategy


The following SCCs where found

U12#(ok(X)) → U12#(X)U12#(mark(X)) → U12#(X)

U11#(ok(X)) → U11#(X)U11#(mark(X)) → U11#(X)

active#(isNePal(X)) → active#(X)active#(U11(X)) → active#(X)
active#(__(X1, X2)) → active#(X1)active#(__(X1, X2)) → active#(X2)
active#(U12(X)) → active#(X)

proper#(__(X1, X2)) → proper#(X1)proper#(U12(X)) → proper#(X)
proper#(isNePal(X)) → proper#(X)proper#(U11(X)) → proper#(X)
proper#(__(X1, X2)) → proper#(X2)

__#(mark(X1), X2) → __#(X1, X2)__#(ok(X1), ok(X2)) → __#(X1, X2)
__#(X1, mark(X2)) → __#(X1, X2)

isNePal#(mark(X)) → isNePal#(X)isNePal#(ok(X)) → isNePal#(X)

top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNePal#(mark(X))isNePal#(X)isNePal#(ok(X))isNePal#(X)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, active, __, U11, mark, U12, ok, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNePal#(mark(X))isNePal#(X)isNePal#(ok(X))isNePal#(X)

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

top#(mark(X))top#(proper(X))top#(ok(X))top#(active(X))

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, active, __, U11, mark, U12, ok, proper, nil, top

Strategy


Polynomial Interpretation

Improved Usable rules

active(__(X1, X2))__(active(X1), X2)active(__(X, nil))mark(X)
U12(mark(X))mark(U12(X))U11(mark(X))mark(U11(X))
__(mark(X1), X2)mark(__(X1, X2))active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))
active(isNePal(__(I, __(P, I))))mark(U11(tt))isNePal(ok(X))ok(isNePal(X))
active(U12(X))U12(active(X))__(ok(X1), ok(X2))ok(__(X1, X2))
active(__(nil, X))mark(X)U11(ok(X))ok(U11(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(tt)ok(tt)
active(U12(tt))mark(tt)active(U11(tt))mark(U12(tt))
active(isNePal(X))isNePal(active(X))active(U11(X))U11(active(X))
proper(isNePal(X))isNePal(proper(X))U12(ok(X))ok(U12(X))
proper(U11(X))U11(proper(X))proper(U12(X))U12(proper(X))
proper(nil)ok(nil)active(__(X1, X2))__(X1, active(X2))
isNePal(mark(X))mark(isNePal(X))__(X1, mark(X2))mark(__(X1, X2))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

top#(mark(X))top#(proper(X))

Problem 10: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

top#(ok(X))top#(active(X))

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, U11, __, active, ok, U12, mark, proper, top, nil

Strategy


Polynomial Interpretation

Improved Usable rules

active(__(X1, X2))__(active(X1), X2)__(ok(X1), ok(X2))ok(__(X1, X2))
active(__(nil, X))mark(X)U11(ok(X))ok(U11(X))
active(__(X, nil))mark(X)U12(mark(X))mark(U12(X))
active(U12(tt))mark(tt)active(isNePal(X))isNePal(active(X))
active(U11(tt))mark(U12(tt))U11(mark(X))mark(U11(X))
active(U11(X))U11(active(X))__(mark(X1), X2)mark(__(X1, X2))
U12(ok(X))ok(U12(X))active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))
active(isNePal(__(I, __(P, I))))mark(U11(tt))active(__(X1, X2))__(X1, active(X2))
isNePal(ok(X))ok(isNePal(X))isNePal(mark(X))mark(isNePal(X))
__(X1, mark(X2))mark(__(X1, X2))active(U12(X))U12(active(X))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

top#(ok(X))top#(active(X))

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

proper#(__(X1, X2))proper#(X1)proper#(U12(X))proper#(X)
proper#(isNePal(X))proper#(X)proper#(U11(X))proper#(X)
proper#(__(X1, X2))proper#(X2)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, active, __, U11, mark, U12, ok, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(__(X1, X2))proper#(X1)proper#(U12(X))proper#(X)
proper#(isNePal(X))proper#(X)proper#(U11(X))proper#(X)
proper#(__(X1, X2))proper#(X2)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U11#(ok(X))U11#(X)U11#(mark(X))U11#(X)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, active, __, U11, mark, U12, ok, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U11#(ok(X))U11#(X)U11#(mark(X))U11#(X)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

active#(isNePal(X))active#(X)active#(U11(X))active#(X)
active#(__(X1, X2))active#(X1)active#(__(X1, X2))active#(X2)
active#(U12(X))active#(X)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, active, __, U11, mark, U12, ok, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(U11(X))active#(X)active#(isNePal(X))active#(X)
active#(__(X1, X2))active#(X1)active#(__(X1, X2))active#(X2)
active#(U12(X))active#(X)

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

__#(mark(X1), X2)__#(X1, X2)__#(ok(X1), ok(X2))__#(X1, X2)
__#(X1, mark(X2))__#(X1, X2)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, active, __, U11, mark, U12, ok, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

__#(mark(X1), X2)__#(X1, X2)__#(ok(X1), ok(X2))__#(X1, X2)

Problem 9: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

__#(X1, mark(X2))__#(X1, X2)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, U11, __, active, ok, U12, mark, proper, top, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

__#(X1, mark(X2))__#(X1, X2)

Problem 8: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U12#(ok(X))U12#(X)U12#(mark(X))U12#(X)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(U11(tt))mark(U12(tt))
active(U12(tt))mark(tt)active(isNePal(__(I, __(P, I))))mark(U11(tt))
active(__(X1, X2))__(active(X1), X2)active(__(X1, X2))__(X1, active(X2))
active(U11(X))U11(active(X))active(U12(X))U12(active(X))
active(isNePal(X))isNePal(active(X))__(mark(X1), X2)mark(__(X1, X2))
__(X1, mark(X2))mark(__(X1, X2))U11(mark(X))mark(U11(X))
U12(mark(X))mark(U12(X))isNePal(mark(X))mark(isNePal(X))
proper(__(X1, X2))__(proper(X1), proper(X2))proper(nil)ok(nil)
proper(U11(X))U11(proper(X))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNePal(X))isNePal(proper(X))
__(ok(X1), ok(X2))ok(__(X1, X2))U11(ok(X))ok(U11(X))
U12(ok(X))ok(U12(X))isNePal(ok(X))ok(isNePal(X))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: tt, isNePal, active, __, U11, mark, U12, ok, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U12#(ok(X))U12#(X)U12#(mark(X))U12#(X)