Termination Proof using AProVE

Term Rewriting System R:
[X]
a_{_f}(X) -> g(h(f(X)))
a_{_f}(X) -> f(X)
mark(f(X)) -> a_{_f}(mark(X))
mark(g(X)) -> g(X)
mark(h(X)) -> h(mark(X))

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

MARK(f(X)) -> A_{_F}(mark(X))
MARK(f(X)) -> MARK(X)
MARK(h(X)) -> MARK(X)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

MARK(h(X)) -> MARK(X)
MARK(f(X)) -> MARK(X)

Rules:

a_{_f}(X) -> g(h(f(X)))
a_{_f}(X) -> f(X)
mark(f(X)) -> a_{_f}(mark(X))
mark(g(X)) -> g(X)
mark(h(X)) -> h(mark(X))

Termination of R could not be shown.
Duration:
0:00 minutes