YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (519ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (1739ms).
 |    | – Problem 4 was processed with processor DependencyGraph (4ms).
 | – Problem 3 was processed with processor SubtermCriterion (7ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

+#(p2, +(p2, p2)) → +#(p1, p5)+#(p2, p1) → +#(p1, p2)
+#(p10, +(p1, x)) → +#(p10, x)+#(+(x, y), z) → +#(y, z)
+#(p1, +(p2, +(p2, x))) → +#(p5, x)+#(+(x, y), z) → +#(x, +(y, z))
+#(p1, +(p1, x)) → +#(p2, x)+#(p10, +(p2, x)) → +#(p10, x)
+#(p5, +(p5, x)) → +#(p10, x)+#(p5, p2) → +#(p2, p5)
+#(p5, +(p2, x)) → +#(p2, +(p5, x))+#(p5, p1) → +#(p1, p5)
+#(p5, +(p1, x)) → +#(p5, x)+#(p10, +(p5, x)) → +#(p5, +(p10, x))
+#(p10, +(p1, x)) → +#(p1, +(p10, x))+#(p10, +(p5, x)) → +#(p10, x)
+#(p10, p1) → +#(p1, p10)+#(p5, +(p2, x)) → +#(p5, x)
+#(p10, +(p2, x)) → +#(p2, +(p10, x))+#(p2, +(p1, x)) → +#(p1, +(p2, x))
+#(p5, +(p1, x)) → +#(p1, +(p5, x))+#(p2, +(p2, +(p2, x))) → +#(p5, x)
+#(p2, +(p1, x)) → +#(p2, x)+#(p10, p2) → +#(p2, p10)
+#(p10, p5) → +#(p5, p10)+#(p2, +(p2, +(p2, x))) → +#(p1, +(p5, x))

Rewrite Rules

+(p1, p1) → p2+(p1, +(p2, p2)) → p5
+(p5, p5) → p10+(+(x, y), z) → +(x, +(y, z))
+(p1, +(p1, x)) → +(p2, x)+(p1, +(p2, +(p2, x))) → +(p5, x)
+(p2, p1) → +(p1, p2)+(p2, +(p1, x)) → +(p1, +(p2, x))
+(p2, +(p2, p2)) → +(p1, p5)+(p2, +(p2, +(p2, x))) → +(p1, +(p5, x))
+(p5, p1) → +(p1, p5)+(p5, +(p1, x)) → +(p1, +(p5, x))
+(p5, p2) → +(p2, p5)+(p5, +(p2, x)) → +(p2, +(p5, x))
+(p5, +(p5, x)) → +(p10, x)+(p10, p1) → +(p1, p10)
+(p10, +(p1, x)) → +(p1, +(p10, x))+(p10, p2) → +(p2, p10)
+(p10, +(p2, x)) → +(p2, +(p10, x))+(p10, p5) → +(p5, p10)
+(p10, +(p5, x)) → +(p5, +(p10, x))

Original Signature

Termination of terms over the following signature is verified: p5, p2, p1, +, p10

Strategy

The following SCCs where found

+#(p10, +(p5, x)) → +#(p5, +(p10, x))+#(p10, +(p1, x)) → +#(p1, +(p10, x))
+#(p10, +(p5, x)) → +#(p10, x)+#(p10, +(p1, x)) → +#(p10, x)
+#(p1, +(p2, +(p2, x))) → +#(p5, x)+#(p5, +(p2, x)) → +#(p5, x)
+#(p1, +(p1, x)) → +#(p2, x)+#(p10, +(p2, x)) → +#(p10, x)
+#(p10, +(p2, x)) → +#(p2, +(p10, x))+#(p5, +(p5, x)) → +#(p10, x)
+#(p2, +(p1, x)) → +#(p1, +(p2, x))+#(p5, +(p1, x)) → +#(p1, +(p5, x))
+#(p5, +(p2, x)) → +#(p2, +(p5, x))+#(p2, +(p1, x)) → +#(p2, x)
+#(p2, +(p2, +(p2, x))) → +#(p5, x)+#(p2, +(p2, +(p2, x))) → +#(p1, +(p5, x))
+#(p5, +(p1, x)) → +#(p5, x)
+#(+(x, y), z) → +#(y, z)+#(+(x, y), z) → +#(x, +(y, z))

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

+#(p10, +(p5, x)) → +#(p5, +(p10, x))+#(p10, +(p1, x)) → +#(p1, +(p10, x))
+#(p10, +(p5, x)) → +#(p10, x)+#(p10, +(p1, x)) → +#(p10, x)
+#(p1, +(p2, +(p2, x))) → +#(p5, x)+#(p5, +(p2, x)) → +#(p5, x)
+#(p1, +(p1, x)) → +#(p2, x)+#(p10, +(p2, x)) → +#(p10, x)
+#(p10, +(p2, x)) → +#(p2, +(p10, x))+#(p5, +(p5, x)) → +#(p10, x)
+#(p2, +(p1, x)) → +#(p1, +(p2, x))+#(p5, +(p2, x)) → +#(p2, +(p5, x))
+#(p5, +(p1, x)) → +#(p1, +(p5, x))+#(p2, +(p1, x)) → +#(p2, x)
+#(p2, +(p2, +(p2, x))) → +#(p5, x)+#(p2, +(p2, +(p2, x))) → +#(p1, +(p5, x))
+#(p5, +(p1, x)) → +#(p5, x)

Rewrite Rules

+(p1, p1) → p2+(p1, +(p2, p2)) → p5
+(p5, p5) → p10+(+(x, y), z) → +(x, +(y, z))
+(p1, +(p1, x)) → +(p2, x)+(p1, +(p2, +(p2, x))) → +(p5, x)
+(p2, p1) → +(p1, p2)+(p2, +(p1, x)) → +(p1, +(p2, x))
+(p2, +(p2, p2)) → +(p1, p5)+(p2, +(p2, +(p2, x))) → +(p1, +(p5, x))
+(p5, p1) → +(p1, p5)+(p5, +(p1, x)) → +(p1, +(p5, x))
+(p5, p2) → +(p2, p5)+(p5, +(p2, x)) → +(p2, +(p5, x))
+(p5, +(p5, x)) → +(p10, x)+(p10, p1) → +(p1, p10)
+(p10, +(p1, x)) → +(p1, +(p10, x))+(p10, p2) → +(p2, p10)
+(p10, +(p2, x)) → +(p2, +(p10, x))+(p10, p5) → +(p5, p10)
+(p10, +(p5, x)) → +(p5, +(p10, x))

Original Signature

Termination of terms over the following signature is verified: p5, p2, p1, +, p10

Strategy

Polynomial Interpretation

Improved Usable rules

+(+(x, y), z) → +(x, +(y, z))+(p10, p5) → +(p5, p10)
+(p10, +(p2, x)) → +(p2, +(p10, x))+(p2, +(p2, +(p2, x))) → +(p1, +(p5, x))
+(p2, +(p2, p2)) → +(p1, p5)+(p1, +(p2, p2)) → p5
+(p10, p2) → +(p2, p10)+(p5, +(p2, x)) → +(p2, +(p5, x))
+(p2, p1) → +(p1, p2)+(p1, +(p2, +(p2, x))) → +(p5, x)
+(p5, +(p5, x)) → +(p10, x)+(p10, +(p5, x)) → +(p5, +(p10, x))
+(p2, +(p1, x)) → +(p1, +(p2, x))+(p1, +(p1, x)) → +(p2, x)
+(p10, +(p1, x)) → +(p1, +(p10, x))+(p5, +(p1, x)) → +(p1, +(p5, x))
+(p5, p2) → +(p2, p5)+(p5, p5) → p10
+(p5, p1) → +(p1, p5)+(p10, p1) → +(p1, p10)
+(p1, p1) → p2

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

+#(p10, +(p5, x)) → +#(p10, x)+#(p10, +(p1, x)) → +#(p10, x)
+#(p1, +(p2, +(p2, x))) → +#(p5, x)+#(p5, +(p2, x)) → +#(p5, x)
+#(p1, +(p1, x)) → +#(p2, x)+#(p10, +(p2, x)) → +#(p10, x)
+#(p5, +(p5, x)) → +#(p10, x)+#(p2, +(p2, +(p2, x))) → +#(p5, x)
+#(p2, +(p1, x)) → +#(p2, x)+#(p2, +(p2, +(p2, x))) → +#(p1, +(p5, x))
+#(p5, +(p1, x)) → +#(p5, x)

Problem 4: DependencyGraph

Dependency Pair Problem

Dependency Pairs

+#(p10, +(p2, x)) → +#(p2, +(p10, x))+#(p2, +(p1, x)) → +#(p1, +(p2, x))
+#(p10, +(p5, x)) → +#(p5, +(p10, x))+#(p10, +(p1, x)) → +#(p1, +(p10, x))
+#(p5, +(p1, x)) → +#(p1, +(p5, x))+#(p5, +(p2, x)) → +#(p2, +(p5, x))

Rewrite Rules

+(p1, p1) → p2+(p1, +(p2, p2)) → p5
+(p5, p5) → p10+(+(x, y), z) → +(x, +(y, z))
+(p1, +(p1, x)) → +(p2, x)+(p1, +(p2, +(p2, x))) → +(p5, x)
+(p2, p1) → +(p1, p2)+(p2, +(p1, x)) → +(p1, +(p2, x))
+(p2, +(p2, p2)) → +(p1, p5)+(p2, +(p2, +(p2, x))) → +(p1, +(p5, x))
+(p5, p1) → +(p1, p5)+(p5, +(p1, x)) → +(p1, +(p5, x))
+(p5, p2) → +(p2, p5)+(p5, +(p2, x)) → +(p2, +(p5, x))
+(p5, +(p5, x)) → +(p10, x)+(p10, p1) → +(p1, p10)
+(p10, +(p1, x)) → +(p1, +(p10, x))+(p10, p2) → +(p2, p10)
+(p10, +(p2, x)) → +(p2, +(p10, x))+(p10, p5) → +(p5, p10)
+(p10, +(p5, x)) → +(p5, +(p10, x))

Original Signature

Termination of terms over the following signature is verified: p5, p2, p1, p10, +

Strategy

There are no SCCs!

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

+#(+(x, y), z) → +#(y, z)+#(+(x, y), z) → +#(x, +(y, z))

Rewrite Rules

+(p1, p1) → p2+(p1, +(p2, p2)) → p5
+(p5, p5) → p10+(+(x, y), z) → +(x, +(y, z))
+(p1, +(p1, x)) → +(p2, x)+(p1, +(p2, +(p2, x))) → +(p5, x)
+(p2, p1) → +(p1, p2)+(p2, +(p1, x)) → +(p1, +(p2, x))
+(p2, +(p2, p2)) → +(p1, p5)+(p2, +(p2, +(p2, x))) → +(p1, +(p5, x))
+(p5, p1) → +(p1, p5)+(p5, +(p1, x)) → +(p1, +(p5, x))
+(p5, p2) → +(p2, p5)+(p5, +(p2, x)) → +(p2, +(p5, x))
+(p5, +(p5, x)) → +(p10, x)+(p10, p1) → +(p1, p10)
+(p10, +(p1, x)) → +(p1, +(p10, x))+(p10, p2) → +(p2, p10)
+(p10, +(p2, x)) → +(p2, +(p10, x))+(p10, p5) → +(p5, p10)
+(p10, +(p5, x)) → +(p5, +(p10, x))

Original Signature

Termination of terms over the following signature is verified: p5, p2, p1, +, p10

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

+#(+(x, y), z) → +#(y, z)+#(+(x, y), z) → +#(x, +(y, z))