YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (96ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4iUR (1484ms).
 |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (1062ms).
 |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (469ms).
 |    |    |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (476ms).
 |    |    |    |    | – Problem 9 was processed with processor DependencyGraph (0ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy


The following SCCs where found

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

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

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

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

Termination of terms over the following signature is verified: f, g, 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 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

Termination of terms over the following signature is verified: f, g, 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)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy


Polynomial Interpretation

Improved Usable rules

g(active(X))g(X)h(mark(X))h(X)
f(active(X))f(X)g(mark(X))g(X)
f(mark(X))f(X)h(active(X))h(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 6: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy


Polynomial Interpretation

Improved Usable rules

g(active(X))g(X)g(mark(X))g(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 7: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy


Polynomial Interpretation

Improved Usable rules

g(active(X))g(X)g(mark(X))g(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)

Problem 8: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy


Polynomial Interpretation

Improved Usable rules

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

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

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

Problem 9: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy


There are no SCCs!

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

Termination of terms over the following signature is verified: f, g, 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)