TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60001 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (60ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (781ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (11544ms), DependencyGraph (1ms), ReductionPairSAT (1363ms), DependencyGraph (2ms), SizeChangePrinciple (6351ms), ForwardNarrowing (2ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].
 | – Problem 5 was processed with processor SubtermCriterion (0ms).
 | – Problem 6 was processed with processor SubtermCriterion (0ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).

The following open problems remain:

Open Dependency Pair Problem 4

Dependency Pairs

f#(s(x), s(y)) → f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))

Rewrite Rules

min(0, y) → 0min(x, 0) → 0
min(s(x), s(y)) → s(min(x, y))max(0, y) → y
max(x, 0) → xmax(s(x), s(y)) → s(max(x, y))
+(0, y) → y+(s(x), y) → s(+(x, y))
-(x, 0) → x-(s(x), s(y)) → -(x, y)
*(x, 0) → 0*(x, s(y)) → +(x, *(x, y))
p(s(x)) → xf(s(x), s(y)) → f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))

Original Signature

Termination of terms over the following signature is verified: f, min, max, 0, s, p, *, +, -

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

*#(x, s(y)) → +#(x, *(x, y))min#(s(x), s(y)) → min#(x, y)
*#(x, s(y)) → *#(x, y)f#(s(x), s(y)) → max#(s(x), s(y))
f#(s(x), s(y)) → *#(s(x), s(y))f#(s(x), s(y)) → min#(s(x), s(y))
f#(s(x), s(y)) → f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))max#(s(x), s(y)) → max#(x, y)
+#(s(x), y) → +#(x, y)-#(s(x), s(y)) → -#(x, y)
f#(s(x), s(y)) → -#(min(s(x), s(y)), max(s(x), s(y)))

Rewrite Rules

min(0, y) → 0min(x, 0) → 0
min(s(x), s(y)) → s(min(x, y))max(0, y) → y
max(x, 0) → xmax(s(x), s(y)) → s(max(x, y))
+(0, y) → y+(s(x), y) → s(+(x, y))
-(x, 0) → x-(s(x), s(y)) → -(x, y)
*(x, 0) → 0*(x, s(y)) → +(x, *(x, y))
p(s(x)) → xf(s(x), s(y)) → f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))

Original Signature

Termination of terms over the following signature is verified: min, f, 0, max, s, p, *, +, -

Strategy

The following SCCs where found

min#(s(x), s(y)) → min#(x, y)
*#(x, s(y)) → *#(x, y)
f#(s(x), s(y)) → f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))
max#(s(x), s(y)) → max#(x, y)
+#(s(x), y) → +#(x, y)
-#(s(x), s(y)) → -#(x, y)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

min#(s(x), s(y)) → min#(x, y)

Rewrite Rules

min(0, y) → 0min(x, 0) → 0
min(s(x), s(y)) → s(min(x, y))max(0, y) → y
max(x, 0) → xmax(s(x), s(y)) → s(max(x, y))
+(0, y) → y+(s(x), y) → s(+(x, y))
-(x, 0) → x-(s(x), s(y)) → -(x, y)
*(x, 0) → 0*(x, s(y)) → +(x, *(x, y))
p(s(x)) → xf(s(x), s(y)) → f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))

Original Signature

Termination of terms over the following signature is verified: min, f, 0, max, s, p, *, +, -

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

min#(s(x), s(y)) → min#(x, y)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

-#(s(x), s(y)) → -#(x, y)

Rewrite Rules

min(0, y) → 0min(x, 0) → 0
min(s(x), s(y)) → s(min(x, y))max(0, y) → y
max(x, 0) → xmax(s(x), s(y)) → s(max(x, y))
+(0, y) → y+(s(x), y) → s(+(x, y))
-(x, 0) → x-(s(x), s(y)) → -(x, y)
*(x, 0) → 0*(x, s(y)) → +(x, *(x, y))
p(s(x)) → xf(s(x), s(y)) → f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))

Original Signature

Termination of terms over the following signature is verified: min, f, 0, max, s, p, *, +, -

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

-#(s(x), s(y)) → -#(x, y)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

*#(x, s(y)) → *#(x, y)

Rewrite Rules

min(0, y) → 0min(x, 0) → 0
min(s(x), s(y)) → s(min(x, y))max(0, y) → y
max(x, 0) → xmax(s(x), s(y)) → s(max(x, y))
+(0, y) → y+(s(x), y) → s(+(x, y))
-(x, 0) → x-(s(x), s(y)) → -(x, y)
*(x, 0) → 0*(x, s(y)) → +(x, *(x, y))
p(s(x)) → xf(s(x), s(y)) → f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))

Original Signature

Termination of terms over the following signature is verified: min, f, 0, max, s, p, *, +, -

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

*#(x, s(y)) → *#(x, y)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

min(0, y) → 0min(x, 0) → 0
min(s(x), s(y)) → s(min(x, y))max(0, y) → y
max(x, 0) → xmax(s(x), s(y)) → s(max(x, y))
+(0, y) → y+(s(x), y) → s(+(x, y))
-(x, 0) → x-(s(x), s(y)) → -(x, y)
*(x, 0) → 0*(x, s(y)) → +(x, *(x, y))
p(s(x)) → xf(s(x), s(y)) → f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))

Original Signature

Termination of terms over the following signature is verified: min, f, 0, max, s, p, *, +, -

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

max#(s(x), s(y)) → max#(x, y)

Rewrite Rules

min(0, y) → 0min(x, 0) → 0
min(s(x), s(y)) → s(min(x, y))max(0, y) → y
max(x, 0) → xmax(s(x), s(y)) → s(max(x, y))
+(0, y) → y+(s(x), y) → s(+(x, y))
-(x, 0) → x-(s(x), s(y)) → -(x, y)
*(x, 0) → 0*(x, s(y)) → +(x, *(x, y))
p(s(x)) → xf(s(x), s(y)) → f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))

Original Signature

Termination of terms over the following signature is verified: min, f, 0, max, s, p, *, +, -

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

max#(s(x), s(y)) → max#(x, y)