YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

+(-(x, y), z)-(+(x, z), y)-(+(x, y), y)x

Original Signature

Termination of terms over the following signature is verified: +, -

Strategy


The following SCCs where found

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

+(-(x, y), z)-(+(x, z), y)-(+(x, y), y)x

Original Signature

Termination of terms over the following signature is verified: +, -

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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