YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (233ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (3739ms).
 |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (3125ms).
 |    |    | – Problem 9 was processed with processor PolynomialLinearRange4iUR (2691ms).
 |    |    |    | – Problem 10 was processed with processor PolynomialLinearRange4iUR (1191ms).
 |    |    |    |    | – Problem 11 was processed with processor PolynomialLinearRange4iUR (106ms).
 |    |    |    |    |    | – Problem 12 was processed with processor PolynomialLinearRange4iUR (86ms).
 |    |    |    |    |    |    | – Problem 13 was processed with processor PolynomialLinearRange4iUR (63ms).
 |    |    |    |    |    |    |    | – Problem 14 was processed with processor DependencyGraph (0ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (0ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 was processed with processor SubtermCriterion (0ms).
 | – Problem 7 was processed with processor SubtermCriterion (27ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

h#(mark(X))h#(X)mark#(g(X))g#(X)
g#(mark(X))g#(X)active#(f(f(X)))c#(f(g(f(X))))
mark#(c(X))active#(c(X))f#(active(X))f#(X)
active#(h(X))mark#(c(d(X)))mark#(g(X))active#(g(X))
d#(active(X))d#(X)mark#(h(X))active#(h(mark(X)))
active#(f(f(X)))g#(f(X))active#(h(X))c#(d(X))
active#(h(X))d#(X)h#(active(X))h#(X)
mark#(f(X))f#(mark(X))f#(mark(X))f#(X)
c#(active(X))c#(X)active#(c(X))mark#(d(X))
d#(mark(X))d#(X)active#(c(X))d#(X)
mark#(d(X))d#(X)mark#(f(X))mark#(X)
mark#(f(X))active#(f(mark(X)))active#(f(f(X)))f#(X)
g#(active(X))g#(X)mark#(d(X))active#(d(X))
active#(f(f(X)))mark#(c(f(g(f(X)))))active#(f(f(X)))f#(g(f(X)))
c#(mark(X))c#(X)mark#(c(X))c#(X)
mark#(h(X))mark#(X)mark#(h(X))h#(mark(X))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


The following SCCs where found

d#(mark(X)) → d#(X)d#(active(X)) → d#(X)

f#(active(X)) → f#(X)f#(mark(X)) → f#(X)

active#(f(f(X))) → mark#(c(f(g(f(X)))))mark#(d(X)) → active#(d(X))
mark#(h(X)) → active#(h(mark(X)))mark#(c(X)) → active#(c(X))
active#(c(X)) → mark#(d(X))mark#(f(X)) → mark#(X)
active#(h(X)) → mark#(c(d(X)))mark#(h(X)) → mark#(X)
mark#(f(X)) → active#(f(mark(X)))mark#(g(X)) → active#(g(X))

c#(active(X)) → c#(X)c#(mark(X)) → c#(X)

g#(active(X)) → g#(X)g#(mark(X)) → g#(X)

h#(mark(X)) → h#(X)h#(active(X)) → h#(X)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

active#(f(f(X)))mark#(c(f(g(f(X)))))mark#(d(X))active#(d(X))
mark#(h(X))active#(h(mark(X)))mark#(c(X))active#(c(X))
active#(c(X))mark#(d(X))mark#(f(X))mark#(X)
active#(h(X))mark#(c(d(X)))mark#(h(X))mark#(X)
mark#(f(X))active#(f(mark(X)))mark#(g(X))active#(g(X))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Polynomial Interpretation

Improved Usable rules

d(active(X))d(X)c(mark(X))c(X)
g(active(X))g(X)h(mark(X))h(X)
c(active(X))c(X)f(active(X))f(X)
g(mark(X))g(X)f(mark(X))f(X)
h(active(X))h(X)d(mark(X))d(X)

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

mark#(d(X))active#(d(X))

Problem 8: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

active#(f(f(X)))mark#(c(f(g(f(X)))))mark#(h(X))active#(h(mark(X)))
mark#(c(X))active#(c(X))active#(c(X))mark#(d(X))
active#(h(X))mark#(c(d(X)))mark#(f(X))mark#(X)
mark#(h(X))mark#(X)mark#(f(X))active#(f(mark(X)))
mark#(g(X))active#(g(X))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Polynomial Interpretation

Improved Usable rules

d(active(X))d(X)c(mark(X))c(X)
c(active(X))c(X)d(mark(X))d(X)

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

mark#(g(X))active#(g(X))

Problem 9: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

active#(f(f(X)))mark#(c(f(g(f(X)))))mark#(h(X))active#(h(mark(X)))
mark#(c(X))active#(c(X))active#(c(X))mark#(d(X))
mark#(f(X))mark#(X)active#(h(X))mark#(c(d(X)))
mark#(h(X))mark#(X)mark#(f(X))active#(f(mark(X)))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Polynomial Interpretation

Improved Usable rules

d(active(X))d(X)c(mark(X))c(X)
c(active(X))c(X)d(mark(X))d(X)

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

mark#(h(X))active#(h(mark(X)))mark#(h(X))mark#(X)

Problem 10: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

active#(f(f(X)))mark#(c(f(g(f(X)))))mark#(c(X))active#(c(X))
active#(c(X))mark#(d(X))active#(h(X))mark#(c(d(X)))
mark#(f(X))mark#(X)mark#(f(X))active#(f(mark(X)))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Polynomial Interpretation

Improved Usable rules

d(active(X))d(X)c(mark(X))c(X)
c(active(X))c(X)d(mark(X))d(X)

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

mark#(f(X))mark#(X)mark#(f(X))active#(f(mark(X)))

Problem 11: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

active#(f(f(X)))mark#(c(f(g(f(X)))))mark#(c(X))active#(c(X))
active#(c(X))mark#(d(X))active#(h(X))mark#(c(d(X)))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Polynomial Interpretation

Improved Usable rules

c(mark(X))c(X)c(active(X))c(X)

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

active#(f(f(X)))mark#(c(f(g(f(X)))))

Problem 12: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(c(X))active#(c(X))active#(c(X))mark#(d(X))
active#(h(X))mark#(c(d(X)))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Polynomial Interpretation

Improved Usable rules

d(active(X))d(X)c(mark(X))c(X)
c(active(X))c(X)d(mark(X))d(X)

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

active#(h(X))mark#(c(d(X)))

Problem 13: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(c(X))active#(c(X))active#(c(X))mark#(d(X))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Polynomial Interpretation

Improved Usable rules

d(active(X))d(X)d(mark(X))d(X)

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

active#(c(X))mark#(d(X))

Problem 14: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(c(X))active#(c(X))

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


There are no SCCs!

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

c#(active(X))c#(X)c#(mark(X))c#(X)

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

c#(active(X))c#(X)c#(mark(X))c#(X)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

d#(mark(X))d#(X)d#(active(X))d#(X)

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

d#(mark(X))d#(X)d#(active(X))d#(X)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

f#(active(X))f#(X)f#(mark(X))f#(X)

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

f#(active(X))f#(X)f#(mark(X))f#(X)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

g#(active(X))g#(X)g#(mark(X))g#(X)

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

g#(active(X))g#(X)g#(mark(X))g#(X)

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

h#(mark(X))h#(X)h#(active(X))h#(X)

Rewrite Rules

active(f(f(X)))mark(c(f(g(f(X)))))active(c(X))mark(d(X))
active(h(X))mark(c(d(X)))mark(f(X))active(f(mark(X)))
mark(c(X))active(c(X))mark(g(X))active(g(X))
mark(d(X))active(d(X))mark(h(X))active(h(mark(X)))
f(mark(X))f(X)f(active(X))f(X)
c(mark(X))c(X)c(active(X))c(X)
g(mark(X))g(X)g(active(X))g(X)
d(mark(X))d(X)d(active(X))d(X)
h(mark(X))h(X)h(active(X))h(X)

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, active, mark, h

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

h#(mark(X))h#(X)h#(active(X))h#(X)