TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60042 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (64ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (252ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (852ms), DependencyGraph (3ms), ReductionPairSAT (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (0ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| help#(false, c, x, y, z) | → | towerIter#(s(c), x, y, exp(y, z)) | | towerIter#(c, x, y, z) | → | help#(ge(c, x), c, x, y, z) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| ge(x, 0) | → | true | | ge(0, s(x)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | tower(x, y) | → | towerIter(0, x, y, s(0)) |
| towerIter(c, x, y, z) | → | help(ge(c, x), c, x, y, z) | | help(true, c, x, y, z) | → | z |
| help(false, c, x, y, z) | → | towerIter(s(c), x, y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: exp, plus, help, tower, 0, s, times, towerIter, false, true, ge
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | plus#(y, times(x, y)) | | towerIter#(c, x, y, z) | → | ge#(c, x) |
| exp#(x, s(y)) | → | exp#(x, y) | | help#(false, c, x, y, z) | → | towerIter#(s(c), x, y, exp(y, z)) |
| times#(s(x), y) | → | times#(x, y) | | tower#(x, y) | → | towerIter#(0, x, y, s(0)) |
| plus#(s(x), y) | → | plus#(x, y) | | ge#(s(x), s(y)) | → | ge#(x, y) |
| exp#(x, s(y)) | → | times#(x, exp(x, y)) | | towerIter#(c, x, y, z) | → | help#(ge(c, x), c, x, y, z) |
| help#(false, c, x, y, z) | → | exp#(y, z) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| ge(x, 0) | → | true | | ge(0, s(x)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | tower(x, y) | → | towerIter(0, x, y, s(0)) |
| towerIter(c, x, y, z) | → | help(ge(c, x), c, x, y, z) | | help(true, c, x, y, z) | → | z |
| help(false, c, x, y, z) | → | towerIter(s(c), x, y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, help, 0, s, times, true, false, towerIter, ge
Strategy
The following SCCs where found
| exp#(x, s(y)) → exp#(x, y) |
| help#(false, c, x, y, z) → towerIter#(s(c), x, y, exp(y, z)) | towerIter#(c, x, y, z) → help#(ge(c, x), c, x, y, z) |
| times#(s(x), y) → times#(x, y) |
| plus#(s(x), y) → plus#(x, y) |
| ge#(s(x), s(y)) → ge#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| exp#(x, s(y)) | → | exp#(x, y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| ge(x, 0) | → | true | | ge(0, s(x)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | tower(x, y) | → | towerIter(0, x, y, s(0)) |
| towerIter(c, x, y, z) | → | help(ge(c, x), c, x, y, z) | | help(true, c, x, y, z) | → | z |
| help(false, c, x, y, z) | → | towerIter(s(c), x, y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, help, 0, s, times, true, false, towerIter, ge
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| exp#(x, s(y)) | → | exp#(x, y) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| ge(x, 0) | → | true | | ge(0, s(x)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | tower(x, y) | → | towerIter(0, x, y, s(0)) |
| towerIter(c, x, y, z) | → | help(ge(c, x), c, x, y, z) | | help(true, c, x, y, z) | → | z |
| help(false, c, x, y, z) | → | towerIter(s(c), x, y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, help, 0, s, times, true, false, towerIter, ge
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| plus#(s(x), y) | → | plus#(x, y) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ge#(s(x), s(y)) | → | ge#(x, y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| ge(x, 0) | → | true | | ge(0, s(x)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | tower(x, y) | → | towerIter(0, x, y, s(0)) |
| towerIter(c, x, y, z) | → | help(ge(c, x), c, x, y, z) | | help(true, c, x, y, z) | → | z |
| help(false, c, x, y, z) | → | towerIter(s(c), x, y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, help, 0, s, times, true, false, towerIter, ge
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ge#(s(x), s(y)) | → | ge#(x, y) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | times#(x, y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| exp(x, 0) | → | s(0) | | exp(x, s(y)) | → | times(x, exp(x, y)) |
| ge(x, 0) | → | true | | ge(0, s(x)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | tower(x, y) | → | towerIter(0, x, y, s(0)) |
| towerIter(c, x, y, z) | → | help(ge(c, x), c, x, y, z) | | help(true, c, x, y, z) | → | z |
| help(false, c, x, y, z) | → | towerIter(s(c), x, y, exp(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, exp, tower, help, 0, s, times, true, false, towerIter, ge
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| times#(s(x), y) | → | times#(x, y) |