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

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

         ↳Narrowing Transformation

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

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_b}))

10 new Dependency Pairs are created:

A_{_A'} -> A_{_H}(a_{_z}(mark(a_{_a}), a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(f(a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_c}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_d}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_z}(mark(a_{_b}), a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), f(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_c}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_d}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(b))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(b))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_d}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_c}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), f(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_z}(mark(a_{_b}), a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_d}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_c}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(f(a_{_a}), a_{_f}(a_{_b}))
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)
A_{_A'} -> A_{_H}(a_{_z}(mark(a_{_a}), a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_F}(a_{_b})
A_{_G}(d, X, X) -> A_{_A'}
A_{_H}(X, X) -> A_{_G}(mark(X), mark(X), a_{_f}(a_{_k}))
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_{_a})
MARK(A) -> A_{_A'}
A_{_Z}(e, X) -> MARK(X)
A_{_F}(X) -> A_{_Z}(mark(X), X)
A_{_H}(X, X) -> A_{_F}(a_{_k})

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

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(z(X1, X2)) -> A_{_Z}(mark(X1), X2)

13 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_d}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_c}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), f(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_z}(mark(a_{_b}), a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_d}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_c}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(f(a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_z}(mark(a_{_a}), a_{_a}), a_{_f}(a_{_b}))
A_{_H}(X, X) -> A_{_F}(a_{_k})
MARK(z(e, X2)) -> A_{_Z}(e, X2)
MARK(z(g(X1'', X2'', X3'), X2)) -> A_{_Z}(a_{_g}(mark(X1''), mark(X2''), mark(X3')), X2)
MARK(z(h(X1'', X2''), X2)) -> A_{_Z}(a_{_h}(mark(X1''), mark(X2'')), X2)
MARK(z(f(X'), X2)) -> A_{_Z}(a_{_f}(mark(X')), X2)
MARK(z(z(X1'', X2''), X2)) -> A_{_Z}(a_{_z}(mark(X1''), X2''), X2)
MARK(z(k, X2)) -> A_{_Z}(a_{_k}, X2)
MARK(z(d, X2)) -> A_{_Z}(a_{_d}, X2)
MARK(z(c, X2)) -> A_{_Z}(a_{_c}, X2)
MARK(z(b, X2)) -> A_{_Z}(a_{_b}, X2)
MARK(z(a, X2)) -> A_{_Z}(a_{_a}, X2)
MARK(z(A, X2)) -> A_{_Z}(a_{_A}, X2)
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)
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}(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

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(g(X1, X2, X3)) -> A_{_G}(mark(X1), mark(X2), mark(X3))

39 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Polynomial Ordering

Dependency Pairs:

A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(b))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_c}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), f(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_z}(mark(a_{_b}), a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_d}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_c}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(f(a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_z}(mark(a_{_a}), a_{_a}), a_{_f}(a_{_b}))
A_{_H}(X, X) -> A_{_F}(a_{_k})
MARK(g(X1, X2, m)) -> A_{_G}(mark(X1), mark(X2), m)
MARK(g(X1, X2, l)) -> A_{_G}(mark(X1), mark(X2), l)
MARK(g(X1, X2, e)) -> A_{_G}(mark(X1), mark(X2), e)
MARK(g(X1, X2, g(X1'', X2'', X3''))) -> A_{_G}(mark(X1), mark(X2), a_{_g}(mark(X1''), mark(X2''), mark(X3'')))
MARK(g(X1, X2, h(X1'', X2''))) -> A_{_G}(mark(X1), mark(X2), a_{_h}(mark(X1''), mark(X2'')))
MARK(g(X1, X2, f(X'))) -> A_{_G}(mark(X1), mark(X2), a_{_f}(mark(X')))
MARK(g(X1, X2, z(X1'', X2''))) -> A_{_G}(mark(X1), mark(X2), a_{_z}(mark(X1''), X2''))
MARK(g(X1, X2, k)) -> A_{_G}(mark(X1), mark(X2), a_{_k})
MARK(g(X1, X2, d)) -> A_{_G}(mark(X1), mark(X2), a_{_d})
MARK(g(X1, X2, c)) -> A_{_G}(mark(X1), mark(X2), a_{_c})
MARK(g(X1, X2, b)) -> A_{_G}(mark(X1), mark(X2), a_{_b})
MARK(g(X1, X2, a)) -> A_{_G}(mark(X1), mark(X2), a_{_a})
MARK(g(X1, X2, A)) -> A_{_G}(mark(X1), mark(X2), a_{_A})
MARK(g(X1, m, X3)) -> A_{_G}(mark(X1), m, mark(X3))
MARK(g(X1, l, X3)) -> A_{_G}(mark(X1), l, mark(X3))
MARK(g(X1, e, X3)) -> A_{_G}(mark(X1), e, mark(X3))
MARK(g(X1, g(X1'', X2'', X3''), X3)) -> A_{_G}(mark(X1), a_{_g}(mark(X1''), mark(X2''), mark(X3'')), mark(X3))
MARK(g(X1, h(X1'', X2''), X3)) -> A_{_G}(mark(X1), a_{_h}(mark(X1''), mark(X2'')), mark(X3))
MARK(g(X1, f(X'), X3)) -> A_{_G}(mark(X1), a_{_f}(mark(X')), mark(X3))
MARK(g(X1, z(X1'', X2''), X3)) -> A_{_G}(mark(X1), a_{_z}(mark(X1''), X2''), mark(X3))
MARK(g(X1, k, X3)) -> A_{_G}(mark(X1), a_{_k}, mark(X3))
MARK(g(X1, d, X3)) -> A_{_G}(mark(X1), a_{_d}, mark(X3))
MARK(g(X1, c, X3)) -> A_{_G}(mark(X1), a_{_c}, mark(X3))
MARK(g(X1, b, X3)) -> A_{_G}(mark(X1), a_{_b}, mark(X3))
MARK(g(X1, a, X3)) -> A_{_G}(mark(X1), a_{_a}, mark(X3))
MARK(g(X1, A, X3)) -> A_{_G}(mark(X1), a_{_A}, mark(X3))
MARK(g(g(X1'', X2'', X3''), X2, X3)) -> A_{_G}(a_{_g}(mark(X1''), mark(X2''), mark(X3'')), mark(X2), mark(X3))
MARK(g(h(X1'', X2''), X2, X3)) -> A_{_G}(a_{_h}(mark(X1''), mark(X2'')), mark(X2), mark(X3))
MARK(g(f(X'), X2, X3)) -> A_{_G}(a_{_f}(mark(X')), mark(X2), mark(X3))
MARK(g(z(X1'', X2''), X2, X3)) -> A_{_G}(a_{_z}(mark(X1''), X2''), mark(X2), mark(X3))
MARK(g(k, X2, X3)) -> A_{_G}(a_{_k}, mark(X2), mark(X3))
MARK(g(d, X2, X3)) -> A_{_G}(a_{_d}, mark(X2), mark(X3))
MARK(g(c, X2, X3)) -> A_{_G}(a_{_c}, mark(X2), mark(X3))
MARK(g(b, X2, X3)) -> A_{_G}(a_{_b}, mark(X2), mark(X3))
MARK(g(a, X2, X3)) -> A_{_G}(a_{_a}, mark(X2), mark(X3))
MARK(g(A, X2, X3)) -> A_{_G}(a_{_A}, mark(X2), mark(X3))
MARK(z(e, X2)) -> A_{_Z}(e, X2)
MARK(z(g(X1'', X2'', X3'), X2)) -> A_{_Z}(a_{_g}(mark(X1''), mark(X2''), mark(X3')), X2)
MARK(z(h(X1'', X2''), X2)) -> A_{_Z}(a_{_h}(mark(X1''), mark(X2'')), X2)
MARK(z(f(X'), X2)) -> A_{_Z}(a_{_f}(mark(X')), X2)
MARK(z(z(X1'', X2''), X2)) -> A_{_Z}(a_{_z}(mark(X1''), X2''), X2)
MARK(z(k, X2)) -> A_{_Z}(a_{_k}, X2)
MARK(z(d, X2)) -> A_{_Z}(a_{_d}, X2)
MARK(z(c, X2)) -> A_{_Z}(a_{_c}, X2)
MARK(z(b, X2)) -> A_{_Z}(a_{_b}, X2)
MARK(z(a, X2)) -> A_{_Z}(a_{_a}, X2)
MARK(z(A, X2)) -> A_{_Z}(a_{_A}, X2)
MARK(g(X1, X2, X3)) -> MARK(X3)
MARK(g(X1, X2, X3)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> MARK(X1)
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)
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_{_d}))

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

The following dependency pairs can be strictly oriented:

MARK(g(g(X1'', X2'', X3''), X2, X3)) -> A_{_G}(a_{_g}(mark(X1''), mark(X2''), mark(X3'')), mark(X2), mark(X3))
MARK(g(h(X1'', X2''), X2, X3)) -> A_{_G}(a_{_h}(mark(X1''), mark(X2'')), mark(X2), mark(X3))
MARK(g(k, X2, X3)) -> A_{_G}(a_{_k}, mark(X2), mark(X3))
MARK(g(A, X2, X3)) -> A_{_G}(a_{_A}, mark(X2), mark(X3))
MARK(z(g(X1'', X2'', X3'), X2)) -> A_{_Z}(a_{_g}(mark(X1''), mark(X2''), mark(X3')), X2)
MARK(z(h(X1'', X2''), X2)) -> A_{_Z}(a_{_h}(mark(X1''), mark(X2'')), X2)
MARK(z(k, X2)) -> A_{_Z}(a_{_k}, X2)
MARK(z(A, X2)) -> A_{_Z}(a_{_A}, X2)

Additionally, the following rules can be oriented:

a_{_a} -> a_{_c}
a_{_a} -> a_{_d}
a_{_a} -> a
a_{_c} -> e
a_{_c} -> l
a_{_c} -> c
a_{_d} -> m
a_{_d} -> d
a_{_b} -> a_{_c}
a_{_b} -> a_{_d}
a_{_b} -> b
a_{_k} -> l
a_{_k} -> m
a_{_k} -> k
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_{_f}(X) -> a_{_z}(mark(X), X)
a_{_f}(X) -> f(X)
a_{_g}(d, X, X) -> a_{_A}
a_{_g}(X1, X2, X3) -> g(X1, X2, X3)
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
a_{_z}(e, X) -> mark(X)
a_{_z}(X1, X2) -> z(X1, X2)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(a__z(x₁, x₂)) = 1

POL(mark(x₁)) = 1

POL(f(x₁)) = 0

POL(a__h(x₁, x₂)) = 0

POL(c) = 0

POL(l) = 0

POL(a__k) = 0

POL(d) = 1

POL(a__b) = 1

POL(A__F(x₁)) = 1

POL(A__A') = 1

POL(k) = 0

POL(a__f(x₁)) = 1

POL(MARK(x₁)) = 1

POL(a__c) = 1

POL(e) = 1

POL(z(x₁, x₂)) = 0

POL(A__H(x₁, x₂)) = 1

POL(A__G(x₁, x₂, x₃)) = x₁

POL(a__A) = 0

POL(m) = 0

POL(a__g(x₁, x₂, x₃)) = 0

POL(a__a) = 1

POL(a__d) = 1

POL(g(x₁, x₂, x₃)) = 0

POL(b) = 0

POL(A__Z(x₁, x₂)) = x₁

POL(h(x₁, x₂)) = 0

POL(a) = 0

POL(A) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Polynomial Ordering

Dependency Pairs:

A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(b))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_c}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), f(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_z}(mark(a_{_b}), a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_d}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_c}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(f(a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_z}(mark(a_{_a}), a_{_a}), a_{_f}(a_{_b}))
A_{_H}(X, X) -> A_{_F}(a_{_k})
MARK(g(X1, X2, m)) -> A_{_G}(mark(X1), mark(X2), m)
MARK(g(X1, X2, l)) -> A_{_G}(mark(X1), mark(X2), l)
MARK(g(X1, X2, e)) -> A_{_G}(mark(X1), mark(X2), e)
MARK(g(X1, X2, g(X1'', X2'', X3''))) -> A_{_G}(mark(X1), mark(X2), a_{_g}(mark(X1''), mark(X2''), mark(X3'')))
MARK(g(X1, X2, h(X1'', X2''))) -> A_{_G}(mark(X1), mark(X2), a_{_h}(mark(X1''), mark(X2'')))
MARK(g(X1, X2, f(X'))) -> A_{_G}(mark(X1), mark(X2), a_{_f}(mark(X')))
MARK(g(X1, X2, z(X1'', X2''))) -> A_{_G}(mark(X1), mark(X2), a_{_z}(mark(X1''), X2''))
MARK(g(X1, X2, k)) -> A_{_G}(mark(X1), mark(X2), a_{_k})
MARK(g(X1, X2, d)) -> A_{_G}(mark(X1), mark(X2), a_{_d})
MARK(g(X1, X2, c)) -> A_{_G}(mark(X1), mark(X2), a_{_c})
MARK(g(X1, X2, b)) -> A_{_G}(mark(X1), mark(X2), a_{_b})
MARK(g(X1, X2, a)) -> A_{_G}(mark(X1), mark(X2), a_{_a})
MARK(g(X1, X2, A)) -> A_{_G}(mark(X1), mark(X2), a_{_A})
MARK(g(X1, m, X3)) -> A_{_G}(mark(X1), m, mark(X3))
MARK(g(X1, l, X3)) -> A_{_G}(mark(X1), l, mark(X3))
MARK(g(X1, e, X3)) -> A_{_G}(mark(X1), e, mark(X3))
MARK(g(X1, g(X1'', X2'', X3''), X3)) -> A_{_G}(mark(X1), a_{_g}(mark(X1''), mark(X2''), mark(X3'')), mark(X3))
MARK(g(X1, h(X1'', X2''), X3)) -> A_{_G}(mark(X1), a_{_h}(mark(X1''), mark(X2'')), mark(X3))
MARK(g(X1, f(X'), X3)) -> A_{_G}(mark(X1), a_{_f}(mark(X')), mark(X3))
MARK(g(X1, z(X1'', X2''), X3)) -> A_{_G}(mark(X1), a_{_z}(mark(X1''), X2''), mark(X3))
MARK(g(X1, k, X3)) -> A_{_G}(mark(X1), a_{_k}, mark(X3))
MARK(g(X1, d, X3)) -> A_{_G}(mark(X1), a_{_d}, mark(X3))
MARK(g(X1, c, X3)) -> A_{_G}(mark(X1), a_{_c}, mark(X3))
MARK(g(X1, b, X3)) -> A_{_G}(mark(X1), a_{_b}, mark(X3))
MARK(g(X1, a, X3)) -> A_{_G}(mark(X1), a_{_a}, mark(X3))
MARK(g(X1, A, X3)) -> A_{_G}(mark(X1), a_{_A}, mark(X3))
MARK(g(f(X'), X2, X3)) -> A_{_G}(a_{_f}(mark(X')), mark(X2), mark(X3))
MARK(g(z(X1'', X2''), X2, X3)) -> A_{_G}(a_{_z}(mark(X1''), X2''), mark(X2), mark(X3))
MARK(g(d, X2, X3)) -> A_{_G}(a_{_d}, mark(X2), mark(X3))
MARK(g(c, X2, X3)) -> A_{_G}(a_{_c}, mark(X2), mark(X3))
MARK(g(b, X2, X3)) -> A_{_G}(a_{_b}, mark(X2), mark(X3))
MARK(g(a, X2, X3)) -> A_{_G}(a_{_a}, mark(X2), mark(X3))
MARK(z(e, X2)) -> A_{_Z}(e, X2)
MARK(z(f(X'), X2)) -> A_{_Z}(a_{_f}(mark(X')), X2)
MARK(z(z(X1'', X2''), X2)) -> A_{_Z}(a_{_z}(mark(X1''), X2''), X2)
MARK(z(d, X2)) -> A_{_Z}(a_{_d}, X2)
MARK(z(c, X2)) -> A_{_Z}(a_{_c}, X2)
MARK(z(b, X2)) -> A_{_Z}(a_{_b}, X2)
MARK(z(a, X2)) -> A_{_Z}(a_{_a}, X2)
MARK(g(X1, X2, X3)) -> MARK(X3)
MARK(g(X1, X2, X3)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> MARK(X1)
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)
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_{_d}))

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

The following dependency pair can be strictly oriented:

MARK(g(c, X2, X3)) -> A_{_G}(a_{_c}, mark(X2), mark(X3))

Additionally, the following rules can be oriented:

a_{_a} -> a_{_c}
a_{_a} -> a_{_d}
a_{_a} -> a
a_{_c} -> e
a_{_c} -> l
a_{_c} -> c
a_{_d} -> m
a_{_d} -> d
a_{_b} -> a_{_c}
a_{_b} -> a_{_d}
a_{_b} -> b
a_{_k} -> l
a_{_k} -> m
a_{_k} -> k
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_{_f}(X) -> a_{_z}(mark(X), X)
a_{_f}(X) -> f(X)
a_{_g}(d, X, X) -> a_{_A}
a_{_g}(X1, X2, X3) -> g(X1, X2, X3)
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
a_{_z}(e, X) -> mark(X)
a_{_z}(X1, X2) -> z(X1, X2)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(a__z(x₁, x₂)) = 1

POL(mark(x₁)) = 1

POL(f(x₁)) = 0

POL(a__h(x₁, x₂)) = 0

POL(c) = 0

POL(l) = 0

POL(a__k) = 0

POL(d) = 1

POL(a__b) = 1

POL(A__F(x₁)) = 1

POL(A__A') = 1

POL(k) = 0

POL(a__f(x₁)) = 1

POL(MARK(x₁)) = 1

POL(a__c) = 0

POL(e) = 0

POL(z(x₁, x₂)) = 0

POL(A__H(x₁, x₂)) = 1

POL(A__G(x₁, x₂, x₃)) = x₁

POL(a__A) = 0

POL(m) = 0

POL(a__g(x₁, x₂, x₃)) = 0

POL(a__a) = 1

POL(a__d) = 1

POL(g(x₁, x₂, x₃)) = 0

POL(b) = 0

POL(A__Z(x₁, x₂)) = 1

POL(h(x₁, x₂)) = 0

POL(a) = 0

POL(A) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 6

                 ↳Polynomial Ordering

Dependency Pairs:

A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(b))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_c}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), f(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_z}(mark(a_{_b}), a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_d}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_c}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(f(a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_z}(mark(a_{_a}), a_{_a}), a_{_f}(a_{_b}))
A_{_H}(X, X) -> A_{_F}(a_{_k})
MARK(g(X1, X2, m)) -> A_{_G}(mark(X1), mark(X2), m)
MARK(g(X1, X2, l)) -> A_{_G}(mark(X1), mark(X2), l)
MARK(g(X1, X2, e)) -> A_{_G}(mark(X1), mark(X2), e)
MARK(g(X1, X2, g(X1'', X2'', X3''))) -> A_{_G}(mark(X1), mark(X2), a_{_g}(mark(X1''), mark(X2''), mark(X3'')))
MARK(g(X1, X2, h(X1'', X2''))) -> A_{_G}(mark(X1), mark(X2), a_{_h}(mark(X1''), mark(X2'')))
MARK(g(X1, X2, f(X'))) -> A_{_G}(mark(X1), mark(X2), a_{_f}(mark(X')))
MARK(g(X1, X2, z(X1'', X2''))) -> A_{_G}(mark(X1), mark(X2), a_{_z}(mark(X1''), X2''))
MARK(g(X1, X2, k)) -> A_{_G}(mark(X1), mark(X2), a_{_k})
MARK(g(X1, X2, d)) -> A_{_G}(mark(X1), mark(X2), a_{_d})
MARK(g(X1, X2, c)) -> A_{_G}(mark(X1), mark(X2), a_{_c})
MARK(g(X1, X2, b)) -> A_{_G}(mark(X1), mark(X2), a_{_b})
MARK(g(X1, X2, a)) -> A_{_G}(mark(X1), mark(X2), a_{_a})
MARK(g(X1, X2, A)) -> A_{_G}(mark(X1), mark(X2), a_{_A})
MARK(g(X1, m, X3)) -> A_{_G}(mark(X1), m, mark(X3))
MARK(g(X1, l, X3)) -> A_{_G}(mark(X1), l, mark(X3))
MARK(g(X1, e, X3)) -> A_{_G}(mark(X1), e, mark(X3))
MARK(g(X1, g(X1'', X2'', X3''), X3)) -> A_{_G}(mark(X1), a_{_g}(mark(X1''), mark(X2''), mark(X3'')), mark(X3))
MARK(g(X1, h(X1'', X2''), X3)) -> A_{_G}(mark(X1), a_{_h}(mark(X1''), mark(X2'')), mark(X3))
MARK(g(X1, f(X'), X3)) -> A_{_G}(mark(X1), a_{_f}(mark(X')), mark(X3))
MARK(g(X1, z(X1'', X2''), X3)) -> A_{_G}(mark(X1), a_{_z}(mark(X1''), X2''), mark(X3))
MARK(g(X1, k, X3)) -> A_{_G}(mark(X1), a_{_k}, mark(X3))
MARK(g(X1, d, X3)) -> A_{_G}(mark(X1), a_{_d}, mark(X3))
MARK(g(X1, c, X3)) -> A_{_G}(mark(X1), a_{_c}, mark(X3))
MARK(g(X1, b, X3)) -> A_{_G}(mark(X1), a_{_b}, mark(X3))
MARK(g(X1, a, X3)) -> A_{_G}(mark(X1), a_{_a}, mark(X3))
MARK(g(X1, A, X3)) -> A_{_G}(mark(X1), a_{_A}, mark(X3))
MARK(g(f(X'), X2, X3)) -> A_{_G}(a_{_f}(mark(X')), mark(X2), mark(X3))
MARK(g(z(X1'', X2''), X2, X3)) -> A_{_G}(a_{_z}(mark(X1''), X2''), mark(X2), mark(X3))
MARK(g(d, X2, X3)) -> A_{_G}(a_{_d}, mark(X2), mark(X3))
MARK(g(b, X2, X3)) -> A_{_G}(a_{_b}, mark(X2), mark(X3))
MARK(g(a, X2, X3)) -> A_{_G}(a_{_a}, mark(X2), mark(X3))
MARK(z(e, X2)) -> A_{_Z}(e, X2)
MARK(z(f(X'), X2)) -> A_{_Z}(a_{_f}(mark(X')), X2)
MARK(z(z(X1'', X2''), X2)) -> A_{_Z}(a_{_z}(mark(X1''), X2''), X2)
MARK(z(d, X2)) -> A_{_Z}(a_{_d}, X2)
MARK(z(c, X2)) -> A_{_Z}(a_{_c}, X2)
MARK(z(b, X2)) -> A_{_Z}(a_{_b}, X2)
MARK(z(a, X2)) -> A_{_Z}(a_{_a}, X2)
MARK(g(X1, X2, X3)) -> MARK(X3)
MARK(g(X1, X2, X3)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> MARK(X1)
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)
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_{_d}))

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

The following dependency pair can be strictly oriented:

MARK(z(d, X2)) -> A_{_Z}(a_{_d}, X2)

Additionally, the following rules can be oriented:

a_{_a} -> a_{_c}
a_{_a} -> a_{_d}
a_{_a} -> a
a_{_c} -> e
a_{_c} -> l
a_{_c} -> c
a_{_d} -> m
a_{_d} -> d
a_{_b} -> a_{_c}
a_{_b} -> a_{_d}
a_{_b} -> b
a_{_k} -> l
a_{_k} -> m
a_{_k} -> k
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_{_f}(X) -> a_{_z}(mark(X), X)
a_{_f}(X) -> f(X)
a_{_g}(d, X, X) -> a_{_A}
a_{_g}(X1, X2, X3) -> g(X1, X2, X3)
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
a_{_z}(e, X) -> mark(X)
a_{_z}(X1, X2) -> z(X1, X2)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(a__z(x₁, x₂)) = 1

POL(mark(x₁)) = 1

POL(f(x₁)) = 0

POL(a__h(x₁, x₂)) = 0

POL(c) = 0

POL(l) = 0

POL(a__k) = 0

POL(d) = 0

POL(a__b) = 1

POL(A__F(x₁)) = 1

POL(A__A') = 1

POL(k) = 0

POL(a__f(x₁)) = 1

POL(MARK(x₁)) = 1

POL(a__c) = 1

POL(e) = 1

POL(z(x₁, x₂)) = 0

POL(A__H(x₁, x₂)) = 1

POL(A__G(x₁, x₂, x₃)) = 1

POL(a__A) = 0

POL(m) = 0

POL(a__g(x₁, x₂, x₃)) = 0

POL(a__a) = 1

POL(a__d) = 0

POL(g(x₁, x₂, x₃)) = 0

POL(b) = 0

POL(A__Z(x₁, x₂)) = x₁

POL(h(x₁, x₂)) = 0

POL(a) = 0

POL(A) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(b))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_f}(a_{_c}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), f(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_a}), a_{_z}(mark(a_{_b}), a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_d}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_f}(a_{_c}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(f(a_{_a}), a_{_f}(a_{_b}))
A_{_A'} -> A_{_H}(a_{_z}(mark(a_{_a}), a_{_a}), a_{_f}(a_{_b}))
A_{_H}(X, X) -> A_{_F}(a_{_k})
MARK(g(X1, X2, m)) -> A_{_G}(mark(X1), mark(X2), m)
MARK(g(X1, X2, l)) -> A_{_G}(mark(X1), mark(X2), l)
MARK(g(X1, X2, e)) -> A_{_G}(mark(X1), mark(X2), e)
MARK(g(X1, X2, g(X1'', X2'', X3''))) -> A_{_G}(mark(X1), mark(X2), a_{_g}(mark(X1''), mark(X2''), mark(X3'')))
MARK(g(X1, X2, h(X1'', X2''))) -> A_{_G}(mark(X1), mark(X2), a_{_h}(mark(X1''), mark(X2'')))
MARK(g(X1, X2, f(X'))) -> A_{_G}(mark(X1), mark(X2), a_{_f}(mark(X')))
MARK(g(X1, X2, z(X1'', X2''))) -> A_{_G}(mark(X1), mark(X2), a_{_z}(mark(X1''), X2''))
MARK(g(X1, X2, k)) -> A_{_G}(mark(X1), mark(X2), a_{_k})
MARK(g(X1, X2, d)) -> A_{_G}(mark(X1), mark(X2), a_{_d})
MARK(g(X1, X2, c)) -> A_{_G}(mark(X1), mark(X2), a_{_c})
MARK(g(X1, X2, b)) -> A_{_G}(mark(X1), mark(X2), a_{_b})
MARK(g(X1, X2, a)) -> A_{_G}(mark(X1), mark(X2), a_{_a})
MARK(g(X1, X2, A)) -> A_{_G}(mark(X1), mark(X2), a_{_A})
MARK(g(X1, m, X3)) -> A_{_G}(mark(X1), m, mark(X3))
MARK(g(X1, l, X3)) -> A_{_G}(mark(X1), l, mark(X3))
MARK(g(X1, e, X3)) -> A_{_G}(mark(X1), e, mark(X3))
MARK(g(X1, g(X1'', X2'', X3''), X3)) -> A_{_G}(mark(X1), a_{_g}(mark(X1''), mark(X2''), mark(X3'')), mark(X3))
MARK(g(X1, h(X1'', X2''), X3)) -> A_{_G}(mark(X1), a_{_h}(mark(X1''), mark(X2'')), mark(X3))
MARK(g(X1, f(X'), X3)) -> A_{_G}(mark(X1), a_{_f}(mark(X')), mark(X3))
MARK(g(X1, z(X1'', X2''), X3)) -> A_{_G}(mark(X1), a_{_z}(mark(X1''), X2''), mark(X3))
MARK(g(X1, k, X3)) -> A_{_G}(mark(X1), a_{_k}, mark(X3))
MARK(g(X1, d, X3)) -> A_{_G}(mark(X1), a_{_d}, mark(X3))
MARK(g(X1, c, X3)) -> A_{_G}(mark(X1), a_{_c}, mark(X3))
MARK(g(X1, b, X3)) -> A_{_G}(mark(X1), a_{_b}, mark(X3))
MARK(g(X1, a, X3)) -> A_{_G}(mark(X1), a_{_a}, mark(X3))
MARK(g(X1, A, X3)) -> A_{_G}(mark(X1), a_{_A}, mark(X3))
MARK(g(f(X'), X2, X3)) -> A_{_G}(a_{_f}(mark(X')), mark(X2), mark(X3))
MARK(g(z(X1'', X2''), X2, X3)) -> A_{_G}(a_{_z}(mark(X1''), X2''), mark(X2), mark(X3))
MARK(g(d, X2, X3)) -> A_{_G}(a_{_d}, mark(X2), mark(X3))
MARK(g(b, X2, X3)) -> A_{_G}(a_{_b}, mark(X2), mark(X3))
MARK(g(a, X2, X3)) -> A_{_G}(a_{_a}, mark(X2), mark(X3))
MARK(z(e, X2)) -> A_{_Z}(e, X2)
MARK(z(f(X'), X2)) -> A_{_Z}(a_{_f}(mark(X')), X2)
MARK(z(z(X1'', X2''), X2)) -> A_{_Z}(a_{_z}(mark(X1''), X2''), X2)
MARK(z(c, X2)) -> A_{_Z}(a_{_c}, X2)
MARK(z(b, X2)) -> A_{_Z}(a_{_b}, X2)
MARK(z(a, X2)) -> A_{_Z}(a_{_a}, X2)
MARK(g(X1, X2, X3)) -> MARK(X3)
MARK(g(X1, X2, X3)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> MARK(X1)
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)
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_{_d}))

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

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

POL(a__z(x₁, x₂))	= 1
POL(mark(x₁))	= 1
POL(f(x₁))	= 0
POL(a__h(x₁, x₂))	= 0
POL(c)	= 0
POL(l)	= 0
POL(a__k)	= 0
POL(d)	= 1
POL(a__b)	= 1
POL(A__F(x₁))	= 1
POL(A__A')	= 1
POL(k)	= 0
POL(a__f(x₁))	= 1
POL(MARK(x₁))	= 1
POL(a__c)	= 1
POL(e)	= 1
POL(z(x₁, x₂))	= 0
POL(A__H(x₁, x₂))	= 1
POL(A__G(x₁, x₂, x₃))	= x₁
POL(a__A)	= 0
POL(m)	= 0
POL(a__g(x₁, x₂, x₃))	= 0
POL(a__a)	= 1
POL(a__d)	= 1
POL(g(x₁, x₂, x₃))	= 0
POL(b)	= 0
POL(A__Z(x₁, x₂))	= x₁
POL(h(x₁, x₂))	= 0
POL(a)	= 0
POL(A)	= 0