Termination w.r.t. Q proof of Transformed_CSR_04_Ex9_Luc04

Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS

↳1 DependencyPairsProof (⇔, 0 ms)

↳2 QDP

↳3 DependencyGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 QDP

        ↳6 UsableRulesProof (⇔, 0 ms)

        ↳7 QDP

        ↳8 QDPSizeChangeProof (⇔, 0 ms)

        ↳9 YES

    ↳10 QDP

        ↳11 QDPOrderProof (⇔, 9 ms)

        ↳12 QDP

        ↳13 QDPOrderProof (⇔, 10 ms)

        ↳14 QDP

        ↳15 TransformationProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 QDPOrderProof (⇔, 1266 ms)

        ↳18 QDP

        ↳19 QDPOrderProof (⇔, 670 ms)

        ↳20 QDP

        ↳21 QDPOrderProof (⇔, 1602 ms)

        ↳22 QDP

        ↳23 NonTerminationLoopProof (⇒, 8262 ms)

        ↳24 NO

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
ACTIVE(f(a, b, X)) → F(X, X, X)
ACTIVE(c) → MARK(a)
ACTIVE(c) → MARK(b)
MARK(f(X1, X2, X3)) → ACTIVE(f(mark(X1), X2, mark(X3)))
MARK(f(X1, X2, X3)) → F(mark(X1), X2, mark(X3))
MARK(f(X1, X2, X3)) → MARK(X1)
MARK(f(X1, X2, X3)) → MARK(X3)
MARK(a) → ACTIVE(a)
MARK(b) → ACTIVE(b)
MARK(c) → ACTIVE(c)
F(mark(X1), X2, X3) → F(X1, X2, X3)
F(X1, mark(X2), X3) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
F(active(X1), X2, X3) → F(X1, X2, X3)
F(X1, active(X2), X3) → F(X1, X2, X3)
F(X1, X2, active(X3)) → F(X1, X2, X3)

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 7 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(X1, mark(X2), X3) → F(X1, X2, X3)
F(mark(X1), X2, X3) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
F(active(X1), X2, X3) → F(X1, X2, X3)
F(X1, active(X2), X3) → F(X1, X2, X3)
F(X1, X2, active(X3)) → F(X1, X2, X3)

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(X1, mark(X2), X3) → F(X1, X2, X3)
F(mark(X1), X2, X3) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
F(active(X1), X2, X3) → F(X1, X2, X3)
F(X1, active(X2), X3) → F(X1, X2, X3)
F(X1, X2, active(X3)) → F(X1, X2, X3)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

F(X1, mark(X2), X3) → F(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
F(mark(X1), X2, X3) → F(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
F(X1, X2, mark(X3)) → F(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
F(active(X1), X2, X3) → F(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
F(X1, active(X2), X3) → F(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
F(X1, X2, active(X3)) → F(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

(9) YES

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(f(X1, X2, X3)) → ACTIVE(f(mark(X1), X2, mark(X3)))
ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
MARK(f(X1, X2, X3)) → MARK(X1)
MARK(f(X1, X2, X3)) → MARK(X3)

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MARK(f(X1, X2, X3)) → MARK(X3)

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x₁)) = 2A + 0A · x₁

POL(f(x₁, x₂, x₃)) = 3A + 0A · x₁ + 0A · x₂ + 3A · x₃

POL(ACTIVE(x₁)) = 3A + 0A · x₁

POL(mark(x₁)) = -I + 0A · x₁

POL(a) = 3A

POL(b) = 1A

POL(active(x₁)) = -I + 0A · x₁

POL(c) = 3A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
active(f(a, b, X)) → mark(f(X, X, X))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
active(c) → mark(a)
active(c) → mark(b)

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(f(X1, X2, X3)) → ACTIVE(f(mark(X1), X2, mark(X3)))
ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
MARK(f(X1, X2, X3)) → MARK(X1)

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MARK(f(X1, X2, X3)) → MARK(X1)

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x₁)) = 4A + 5A · x₁

POL(f(x₁, x₂, x₃)) = 0A + 1A · x₁ + -I · x₂ + 2A · x₃

POL(ACTIVE(x₁)) = 4A + 5A · x₁

POL(mark(x₁)) = -I + 0A · x₁

POL(a) = 0A

POL(b) = 3A

POL(active(x₁)) = -I + 0A · x₁

POL(c) = 3A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
active(f(a, b, X)) → mark(f(X, X, X))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
active(c) → mark(a)
active(c) → mark(b)

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(f(X1, X2, X3)) → ACTIVE(f(mark(X1), X2, mark(X3)))
ACTIVE(f(a, b, X)) → MARK(f(X, X, X))

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(15) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MARK(f(X1, X2, X3)) → ACTIVE(f(mark(X1), X2, mark(X3))) at position [0] we obtained the following new rules [LPAR04]:

MARK(f(x0, x1, y2)) → ACTIVE(f(x0, x1, mark(y2))) → MARK(f(x0, x1, y2)) → ACTIVE(f(x0, x1, mark(y2)))
MARK(f(y0, mark(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2))) → MARK(f(y0, mark(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(y0, x1, x2)) → ACTIVE(f(mark(y0), x1, x2)) → MARK(f(y0, x1, x2)) → ACTIVE(f(mark(y0), x1, x2))
MARK(f(y0, active(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2))) → MARK(f(y0, active(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(f(x0, x1, x2), y1, y2)) → ACTIVE(f(active(f(mark(x0), x1, mark(x2))), y1, mark(y2))) → MARK(f(f(x0, x1, x2), y1, y2)) → ACTIVE(f(active(f(mark(x0), x1, mark(x2))), y1, mark(y2)))
MARK(f(a, y1, y2)) → ACTIVE(f(active(a), y1, mark(y2))) → MARK(f(a, y1, y2)) → ACTIVE(f(active(a), y1, mark(y2)))
MARK(f(b, y1, y2)) → ACTIVE(f(active(b), y1, mark(y2))) → MARK(f(b, y1, y2)) → ACTIVE(f(active(b), y1, mark(y2)))
MARK(f(c, y1, y2)) → ACTIVE(f(active(c), y1, mark(y2))) → MARK(f(c, y1, y2)) → ACTIVE(f(active(c), y1, mark(y2)))
MARK(f(y0, y1, f(x0, x1, x2))) → ACTIVE(f(mark(y0), y1, active(f(mark(x0), x1, mark(x2))))) → MARK(f(y0, y1, f(x0, x1, x2))) → ACTIVE(f(mark(y0), y1, active(f(mark(x0), x1, mark(x2)))))
MARK(f(y0, y1, a)) → ACTIVE(f(mark(y0), y1, active(a))) → MARK(f(y0, y1, a)) → ACTIVE(f(mark(y0), y1, active(a)))
MARK(f(y0, y1, b)) → ACTIVE(f(mark(y0), y1, active(b))) → MARK(f(y0, y1, b)) → ACTIVE(f(mark(y0), y1, active(b)))
MARK(f(y0, y1, c)) → ACTIVE(f(mark(y0), y1, active(c))) → MARK(f(y0, y1, c)) → ACTIVE(f(mark(y0), y1, active(c)))

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
MARK(f(x0, x1, y2)) → ACTIVE(f(x0, x1, mark(y2)))
MARK(f(y0, mark(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(y0, x1, x2)) → ACTIVE(f(mark(y0), x1, x2))
MARK(f(y0, active(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(f(x0, x1, x2), y1, y2)) → ACTIVE(f(active(f(mark(x0), x1, mark(x2))), y1, mark(y2)))
MARK(f(a, y1, y2)) → ACTIVE(f(active(a), y1, mark(y2)))
MARK(f(b, y1, y2)) → ACTIVE(f(active(b), y1, mark(y2)))
MARK(f(c, y1, y2)) → ACTIVE(f(active(c), y1, mark(y2)))
MARK(f(y0, y1, f(x0, x1, x2))) → ACTIVE(f(mark(y0), y1, active(f(mark(x0), x1, mark(x2)))))
MARK(f(y0, y1, a)) → ACTIVE(f(mark(y0), y1, active(a)))
MARK(f(y0, y1, b)) → ACTIVE(f(mark(y0), y1, active(b)))
MARK(f(y0, y1, c)) → ACTIVE(f(mark(y0), y1, active(c)))

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MARK(f(y0, y1, b)) → ACTIVE(f(mark(y0), y1, active(b)))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVE(x₁)) = 1A +
[ -I, 1A, 2A ]

· x₁

POL(f(x₁, x₂, x₃)) =
/ 2A \

| 1A |

\ 0A /

+
/ -I 0A 3A \

| -I -I -I |

\ -I -I 0A /

· x₁ +
/ -I -I -I \

| -I -I -I |

\ -I -I -I /

· x₂ +
/ -I -I -I \

| -I 2A 3A |

\ -I -I 3A /

· x₃

POL(a) =
/ 1A \

| -I |

\ 2A /

POL(b) =
/ 1A \

| -I |

\ -I /

POL(MARK(x₁)) = 3A +
[ 0A, 1A, 2A ]

· x₁

POL(mark(x₁)) =
/ 1A \

| -I |

\ -I /

+
/ 3A 3A 3A \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(active(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 3A 3A 1A \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(c) =
/ 0A \

| 3A |

\ 2A /

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

f(X1, mark(X2), X3) → f(X1, X2, X3)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
active(f(a, b, X)) → mark(f(X, X, X))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
active(c) → mark(a)
active(c) → mark(b)

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
MARK(f(x0, x1, y2)) → ACTIVE(f(x0, x1, mark(y2)))
MARK(f(y0, mark(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(y0, x1, x2)) → ACTIVE(f(mark(y0), x1, x2))
MARK(f(y0, active(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(f(x0, x1, x2), y1, y2)) → ACTIVE(f(active(f(mark(x0), x1, mark(x2))), y1, mark(y2)))
MARK(f(a, y1, y2)) → ACTIVE(f(active(a), y1, mark(y2)))
MARK(f(b, y1, y2)) → ACTIVE(f(active(b), y1, mark(y2)))
MARK(f(c, y1, y2)) → ACTIVE(f(active(c), y1, mark(y2)))
MARK(f(y0, y1, f(x0, x1, x2))) → ACTIVE(f(mark(y0), y1, active(f(mark(x0), x1, mark(x2)))))
MARK(f(y0, y1, a)) → ACTIVE(f(mark(y0), y1, active(a)))
MARK(f(y0, y1, c)) → ACTIVE(f(mark(y0), y1, active(c)))

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MARK(f(y0, y1, a)) → ACTIVE(f(mark(y0), y1, active(a)))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVE(x₁)) = 3A +
[ -I, -I, 1A ]

· x₁

POL(f(x₁, x₂, x₃)) =
/ 3A \

| 3A |

\ -I /

+
/ -I -I -I \

| -I -I -I |

\ -I -I -I /

· x₁ +
/ -I 0A 1A \

| -I 0A -I |

\ -I 1A 2A /

· x₂ +
/ -I 0A 1A \

| -I 0A 1A |

\ -I 2A 3A /

· x₃

POL(a) =
/ 2A \

| -I |

\ -I /

POL(b) =
/ 0A \

| 3A |

\ 3A /

POL(MARK(x₁)) = 0A +
[ 3A, -I, -I ]

· x₁

POL(mark(x₁)) =
/ 3A \

| 0A |

\ -I /

+
/ -I -I 0A \

| -I 0A 1A |

\ -I -I -I /

· x₁

POL(active(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A -I 0A \

| -I 0A 1A |

\ -I -I -I /

· x₁

POL(c) =
/ 3A \

| 3A |

\ 3A /

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

f(X1, mark(X2), X3) → f(X1, X2, X3)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
active(f(a, b, X)) → mark(f(X, X, X))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
active(c) → mark(a)
active(c) → mark(b)

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
MARK(f(x0, x1, y2)) → ACTIVE(f(x0, x1, mark(y2)))
MARK(f(y0, mark(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(y0, x1, x2)) → ACTIVE(f(mark(y0), x1, x2))
MARK(f(y0, active(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(f(x0, x1, x2), y1, y2)) → ACTIVE(f(active(f(mark(x0), x1, mark(x2))), y1, mark(y2)))
MARK(f(a, y1, y2)) → ACTIVE(f(active(a), y1, mark(y2)))
MARK(f(b, y1, y2)) → ACTIVE(f(active(b), y1, mark(y2)))
MARK(f(c, y1, y2)) → ACTIVE(f(active(c), y1, mark(y2)))
MARK(f(y0, y1, f(x0, x1, x2))) → ACTIVE(f(mark(y0), y1, active(f(mark(x0), x1, mark(x2)))))
MARK(f(y0, y1, c)) → ACTIVE(f(mark(y0), y1, active(c)))

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MARK(f(y0, y1, f(x0, x1, x2))) → ACTIVE(f(mark(y0), y1, active(f(mark(x0), x1, mark(x2)))))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVE(x₁)) = 0A +
[ -I, 3A, 2A ]

· x₁

POL(f(x₁, x₂, x₃)) =
/ 0A \

| -I |

\ 3A /

+
/ -I -I -I \

| 1A -I -I |

\ 2A -I -I /

· x₁ +
/ -I -I -I \

| -I -I -I |

\ -I -I -I /

· x₂ +
/ -I -I -I \

| 2A -I -I |

\ 2A -I -I /

· x₃

POL(a) =
/ 2A \

| -I |

\ -I /

POL(b) =
/ 0A \

| -I |

\ 0A /

POL(MARK(x₁)) = 0A +
[ -I, 3A, 3A ]

· x₁

POL(mark(x₁)) =
/ -I \

| -I |

\ 2A /

+
/ 0A -I -I \

| -I 1A -I |

\ -I 0A 0A /

· x₁

POL(active(x₁)) =
/ -I \

| -I |

\ 2A /

+
/ 0A -I -I \

| -I 1A -I |

\ -I -I 0A /

· x₁

POL(c) =
/ 2A \

| -I |

\ -I /

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

f(X1, mark(X2), X3) → f(X1, X2, X3)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
active(f(a, b, X)) → mark(f(X, X, X))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
active(c) → mark(a)
active(c) → mark(b)

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
MARK(f(x0, x1, y2)) → ACTIVE(f(x0, x1, mark(y2)))
MARK(f(y0, mark(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(y0, x1, x2)) → ACTIVE(f(mark(y0), x1, x2))
MARK(f(y0, active(x1), y2)) → ACTIVE(f(mark(y0), x1, mark(y2)))
MARK(f(f(x0, x1, x2), y1, y2)) → ACTIVE(f(active(f(mark(x0), x1, mark(x2))), y1, mark(y2)))
MARK(f(a, y1, y2)) → ACTIVE(f(active(a), y1, mark(y2)))
MARK(f(b, y1, y2)) → ACTIVE(f(active(b), y1, mark(y2)))
MARK(f(c, y1, y2)) → ACTIVE(f(active(c), y1, mark(y2)))
MARK(f(y0, y1, c)) → ACTIVE(f(mark(y0), y1, active(c)))

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) NonTerminationLoopProof (COMPLETE transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = MARK(f(active(c), active(c), X3')) evaluates to t =MARK(f(X3', X3', X3'))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [X3' / active(c)]

Rewriting sequence

MARK(f(active(c), active(c), active(c))) → MARK(f(active(c), mark(b), active(c)))
with rule active(c) → mark(b) at position [0,1] and matcher [ ]

MARK(f(active(c), mark(b), active(c))) → MARK(f(mark(a), mark(b), active(c)))
with rule active(c) → mark(a) at position [0,0] and matcher [ ]

MARK(f(mark(a), mark(b), active(c))) → MARK(f(mark(a), b, active(c)))
with rule f(X1, mark(X2), X3') → f(X1, X2, X3') at position [0] and matcher [X1 / mark(a), X2 / b, X3' / active(c)]

MARK(f(mark(a), b, active(c))) → MARK(f(a, b, active(c)))
with rule f(mark(X1), X2, X3) → f(X1, X2, X3) at position [0] and matcher [X1 / a, X2 / b, X3 / active(c)]

MARK(f(a, b, active(c))) → ACTIVE(f(mark(a), b, active(c)))
with rule MARK(f(y0, x1, x2)) → ACTIVE(f(mark(y0), x1, x2)) at position [] and matcher [y0 / a, x1 / b, x2 / active(c)]

ACTIVE(f(mark(a), b, active(c))) → ACTIVE(f(a, b, active(c)))
with rule f(mark(X1), X2, X3) → f(X1, X2, X3) at position [0] and matcher [X1 / a, X2 / b, X3 / active(c)]

ACTIVE(f(a, b, active(c))) → MARK(f(active(c), active(c), active(c)))
with rule ACTIVE(f(a, b, X)) → MARK(f(X, X, X))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) UsableRulesProof (EQUIVALENT transformation)

(7) Obligation:

(8) QDPSizeChangeProof (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) QDPOrderProof (EQUIVALENT transformation)

(14) Obligation:

(15) TransformationProof (EQUIVALENT transformation)

(16) Obligation:

(17) QDPOrderProof (EQUIVALENT transformation)

(18) Obligation:

(19) QDPOrderProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPOrderProof (EQUIVALENT transformation)

(22) Obligation:

(23) NonTerminationLoopProof (COMPLETE transformation)

(24) NO