Termination Proof using AProVE

Term Rewriting System R:
[X, X1, X2, X3]
a_{_a} -> a_{_c}
a_{_a} -> a_{_d}
a_{_a} -> a
a_{_b} -> a_{_c}
a_{_b} -> a_{_d}
a_{_b} -> b
a_{_c} -> e
a_{_c} -> l
a_{_c} -> c
a_{_k} -> l
a_{_k} -> m
a_{_k} -> k
a_{_d} -> m
a_{_d} -> d
a_{_A} -> a_{_h}(a_{_f}(a_{_a}), a_{_f}(a_{_b}))
a_{_A} -> A
a_{_h}(X, X) -> a_{_g}(mark(X), mark(X), a_{_f}(a_{_k}))
a_{_h}(X1, X2) -> h(X1, X2)
a_{_g}(d, X, X) -> a_{_A}
a_{_g}(X1, X2, X3) -> g(X1, X2, X3)
a_{_f}(X) -> a_{_z}(mark(X), X)
a_{_f}(X) -> f(X)
a_{_z}(e, X) -> mark(X)
a_{_z}(X1, X2) -> z(X1, X2)
mark(A) -> a_{_A}
mark(a) -> a_{_a}
mark(b) -> a_{_b}
mark(c) -> a_{_c}
mark(d) -> a_{_d}
mark(k) -> a_{_k}
mark(z(X1, X2)) -> a_{_z}(mark(X1), X2)
mark(f(X)) -> a_{_f}(mark(X))
mark(h(X1, X2)) -> a_{_h}(mark(X1), mark(X2))
mark(g(X1, X2, X3)) -> a_{_g}(mark(X1), mark(X2), mark(X3))
mark(e) -> e
mark(l) -> l
mark(m) -> m

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A_{_A} -> A_{_C}
A_{_A} -> A_{_D}
A_{_B} -> A_{_C}
A_{_B} -> A_{_D}
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_F}(a_{_a})
A_{_A'} -> A_{_A}
A_{_A'} -> A_{_F}(a_{_b})
A_{_A'} -> A_{_B}
A_{_H}(X, X) -> A_{_G}(mark(X), mark(X), a_{_f}(a_{_k}))
A_{_H}(X, X) -> MARK(X)
A_{_H}(X, X) -> A_{_F}(a_{_k})
A_{_H}(X, X) -> A_{_K}
A_{_G}(d, X, X) -> A_{_A'}
A_{_F}(X) -> A_{_Z}(mark(X), X)
A_{_F}(X) -> MARK(X)
A_{_Z}(e, X) -> MARK(X)
MARK(A) -> A_{_A'}
MARK(a) -> A_{_A}
MARK(b) -> A_{_B}
MARK(c) -> A_{_C}
MARK(d) -> A_{_D}
MARK(k) -> A_{_K}
MARK(z(X1, X2)) -> A_{_Z}(mark(X1), X2)
MARK(z(X1, X2)) -> MARK(X1)
MARK(f(X)) -> A_{_F}(mark(X))
MARK(f(X)) -> MARK(X)
MARK(h(X1, X2)) -> A_{_H}(mark(X1), mark(X2))
MARK(h(X1, X2)) -> MARK(X1)
MARK(h(X1, X2)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> A_{_G}(mark(X1), mark(X2), mark(X3))
MARK(g(X1, X2, X3)) -> MARK(X1)
MARK(g(X1, X2, X3)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> MARK(X3)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

A_{_H}(X, X) -> A_{_F}(a_{_k})
MARK(g(X1, X2, X3)) -> MARK(X3)
MARK(g(X1, X2, X3)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> MARK(X1)
MARK(g(X1, X2, X3)) -> A_{_G}(mark(X1), mark(X2), mark(X3))
MARK(h(X1, X2)) -> MARK(X2)
MARK(h(X1, X2)) -> MARK(X1)
A_{_H}(X, X) -> MARK(X)
MARK(h(X1, X2)) -> A_{_H}(mark(X1), mark(X2))
MARK(f(X)) -> MARK(X)
MARK(f(X)) -> A_{_F}(mark(X))
MARK(z(X1, X2)) -> MARK(X1)
MARK(z(X1, X2)) -> A_{_Z}(mark(X1), X2)
A_{_F}(X) -> MARK(X)
A_{_A'} -> A_{_F}(a_{_b})
MARK(A) -> A_{_A'}
A_{_Z}(e, X) -> MARK(X)
A_{_F}(X) -> A_{_Z}(mark(X), X)
A_{_A'} -> A_{_F}(a_{_a})
A_{_G}(d, X, X) -> A_{_A'}
A_{_H}(X, X) -> A_{_G}(mark(X), mark(X), a_{_f}(a_{_k}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_b}))

Rules:

a_{_a} -> a_{_c}
a_{_a} -> a_{_d}
a_{_a} -> a
a_{_b} -> a_{_c}
a_{_b} -> a_{_d}
a_{_b} -> b
a_{_c} -> e
a_{_c} -> l
a_{_c} -> c
a_{_k} -> l
a_{_k} -> m
a_{_k} -> k
a_{_d} -> m
a_{_d} -> d
a_{_A} -> a_{_h}(a_{_f}(a_{_a}), a_{_f}(a_{_b}))
a_{_A} -> A
a_{_h}(X, X) -> a_{_g}(mark(X), mark(X), a_{_f}(a_{_k}))
a_{_h}(X1, X2) -> h(X1, X2)
a_{_g}(d, X, X) -> a_{_A}
a_{_g}(X1, X2, X3) -> g(X1, X2, X3)
a_{_f}(X) -> a_{_z}(mark(X), X)
a_{_f}(X) -> f(X)
a_{_z}(e, X) -> mark(X)
a_{_z}(X1, X2) -> z(X1, X2)
mark(A) -> a_{_A}
mark(a) -> a_{_a}
mark(b) -> a_{_b}
mark(c) -> a_{_c}
mark(d) -> a_{_d}
mark(k) -> a_{_k}
mark(z(X1, X2)) -> a_{_z}(mark(X1), X2)
mark(f(X)) -> a_{_f}(mark(X))
mark(h(X1, X2)) -> a_{_h}(mark(X1), mark(X2))
mark(g(X1, X2, X3)) -> a_{_g}(mark(X1), mark(X2), mark(X3))
mark(e) -> e
mark(l) -> l
mark(m) -> m

Strategy:

innermost

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