TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60021 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (170ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (83ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (68ms), DependencyGraph (4ms), ReductionPairSAT (385ms)].
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (209ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (809ms), DependencyGraph (2ms), ReductionPairSAT (331ms)].
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (548ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (2162ms), DependencyGraph (2ms), ReductionPairSAT (timeout)].
| – Problem 7 was processed with processor SubtermCriterion (0ms).
| – Problem 8 was processed with processor SubtermCriterion (5ms).
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| f2#(x, 1, z) | → | f0#(x, z, z) | | f0#(0, y, x) | → | f1#(x, y, x) |
| f1#(x, y, z) | → | f2#(x, y, z) |
Rewrite Rules
| plus(x, y) | → | ifPlus(isZero(x), x, inc(y)) | | ifPlus(true, x, y) | → | p(y) |
| ifPlus(false, x, y) | → | plus(p(x), y) | | times(x, y) | → | timesIter(0, x, y, 0) |
| timesIter(i, x, y, z) | → | ifTimes(ge(i, x), i, x, y, z) | | ifTimes(true, i, x, y, z) | → | z |
| ifTimes(false, i, x, y, z) | → | timesIter(inc(i), x, y, plus(z, y)) | | isZero(0) | → | true |
| isZero(s(0)) | → | false | | isZero(s(s(x))) | → | isZero(s(x)) |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| inc(x) | → | s(x) | | p(0) | → | 0 |
| p(s(x)) | → | x | | p(s(s(x))) | → | s(p(s(x))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | f0(0, y, x) | → | f1(x, y, x) |
| f1(x, y, z) | → | f2(x, y, z) | | f2(x, 1, z) | → | f0(x, z, z) |
| f0(x, y, z) | → | d | | f1(x, y, z) | → | c |
Original Signature
Termination of terms over the following signature is verified: plus, ifTimes, d, c, true, ge, ifPlus, 1, timesIter, 0, inc, s, times, p, false, f1, f0, f2, isZero
Open Dependency Pair Problem 4
Dependency Pairs
| ifPlus#(false, x, y) | → | plus#(p(x), y) | | plus#(x, y) | → | ifPlus#(isZero(x), x, inc(y)) |
Rewrite Rules
| plus(x, y) | → | ifPlus(isZero(x), x, inc(y)) | | ifPlus(true, x, y) | → | p(y) |
| ifPlus(false, x, y) | → | plus(p(x), y) | | times(x, y) | → | timesIter(0, x, y, 0) |
| timesIter(i, x, y, z) | → | ifTimes(ge(i, x), i, x, y, z) | | ifTimes(true, i, x, y, z) | → | z |
| ifTimes(false, i, x, y, z) | → | timesIter(inc(i), x, y, plus(z, y)) | | isZero(0) | → | true |
| isZero(s(0)) | → | false | | isZero(s(s(x))) | → | isZero(s(x)) |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| inc(x) | → | s(x) | | p(0) | → | 0 |
| p(s(x)) | → | x | | p(s(s(x))) | → | s(p(s(x))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | f0(0, y, x) | → | f1(x, y, x) |
| f1(x, y, z) | → | f2(x, y, z) | | f2(x, 1, z) | → | f0(x, z, z) |
| f0(x, y, z) | → | d | | f1(x, y, z) | → | c |
Original Signature
Termination of terms over the following signature is verified: plus, ifTimes, d, c, true, ge, ifPlus, 1, timesIter, 0, inc, s, times, p, false, f1, f0, f2, isZero
Open Dependency Pair Problem 6
Dependency Pairs
| ifTimes#(false, i, x, y, z) | → | timesIter#(inc(i), x, y, plus(z, y)) | | timesIter#(i, x, y, z) | → | ifTimes#(ge(i, x), i, x, y, z) |
Rewrite Rules
| plus(x, y) | → | ifPlus(isZero(x), x, inc(y)) | | ifPlus(true, x, y) | → | p(y) |
| ifPlus(false, x, y) | → | plus(p(x), y) | | times(x, y) | → | timesIter(0, x, y, 0) |
| timesIter(i, x, y, z) | → | ifTimes(ge(i, x), i, x, y, z) | | ifTimes(true, i, x, y, z) | → | z |
| ifTimes(false, i, x, y, z) | → | timesIter(inc(i), x, y, plus(z, y)) | | isZero(0) | → | true |
| isZero(s(0)) | → | false | | isZero(s(s(x))) | → | isZero(s(x)) |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| inc(x) | → | s(x) | | p(0) | → | 0 |
| p(s(x)) | → | x | | p(s(s(x))) | → | s(p(s(x))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | f0(0, y, x) | → | f1(x, y, x) |
| f1(x, y, z) | → | f2(x, y, z) | | f2(x, 1, z) | → | f0(x, z, z) |
| f0(x, y, z) | → | d | | f1(x, y, z) | → | c |
Original Signature
Termination of terms over the following signature is verified: plus, ifTimes, d, c, true, ge, ifPlus, 1, timesIter, 0, inc, s, times, p, false, f1, f0, f2, isZero
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| ifPlus#(false, x, y) | → | p#(x) | | timesIter#(i, x, y, z) | → | ge#(i, x) |
| f2#(x, 1, z) | → | f0#(x, z, z) | | ifTimes#(false, i, x, y, z) | → | timesIter#(inc(i), x, y, plus(z, y)) |
| ifTimes#(false, i, x, y, z) | → | plus#(z, y) | | plus#(x, y) | → | inc#(y) |
| ifPlus#(true, x, y) | → | p#(y) | | f0#(0, y, x) | → | f1#(x, y, x) |
| plus#(x, y) | → | ifPlus#(isZero(x), x, inc(y)) | | f1#(x, y, z) | → | f2#(x, y, z) |
| ifPlus#(false, x, y) | → | plus#(p(x), y) | | isZero#(s(s(x))) | → | isZero#(s(x)) |
| ifTimes#(false, i, x, y, z) | → | inc#(i) | | ge#(s(x), s(y)) | → | ge#(x, y) |
| timesIter#(i, x, y, z) | → | ifTimes#(ge(i, x), i, x, y, z) | | times#(x, y) | → | timesIter#(0, x, y, 0) |
| inc#(s(x)) | → | inc#(x) | | plus#(x, y) | → | isZero#(x) |
| p#(s(s(x))) | → | p#(s(x)) |
Rewrite Rules
| plus(x, y) | → | ifPlus(isZero(x), x, inc(y)) | | ifPlus(true, x, y) | → | p(y) |
| ifPlus(false, x, y) | → | plus(p(x), y) | | times(x, y) | → | timesIter(0, x, y, 0) |
| timesIter(i, x, y, z) | → | ifTimes(ge(i, x), i, x, y, z) | | ifTimes(true, i, x, y, z) | → | z |
| ifTimes(false, i, x, y, z) | → | timesIter(inc(i), x, y, plus(z, y)) | | isZero(0) | → | true |
| isZero(s(0)) | → | false | | isZero(s(s(x))) | → | isZero(s(x)) |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| inc(x) | → | s(x) | | p(0) | → | 0 |
| p(s(x)) | → | x | | p(s(s(x))) | → | s(p(s(x))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | f0(0, y, x) | → | f1(x, y, x) |
| f1(x, y, z) | → | f2(x, y, z) | | f2(x, 1, z) | → | f0(x, z, z) |
| f0(x, y, z) | → | d | | f1(x, y, z) | → | c |
Original Signature
Termination of terms over the following signature is verified: plus, ifTimes, d, c, true, ge, ifPlus, 1, timesIter, 0, inc, s, times, p, false, f1, f0, f2, isZero
Strategy
The following SCCs where found
| ifTimes#(false, i, x, y, z) → timesIter#(inc(i), x, y, plus(z, y)) | timesIter#(i, x, y, z) → ifTimes#(ge(i, x), i, x, y, z) |
| isZero#(s(s(x))) → isZero#(s(x)) |
| ifPlus#(false, x, y) → plus#(p(x), y) | plus#(x, y) → ifPlus#(isZero(x), x, inc(y)) |
| ge#(s(x), s(y)) → ge#(x, y) |
| f2#(x, 1, z) → f0#(x, z, z) | f0#(0, y, x) → f1#(x, y, x) |
| f1#(x, y, z) → f2#(x, y, z) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isZero#(s(s(x))) | → | isZero#(s(x)) |
Rewrite Rules
| plus(x, y) | → | ifPlus(isZero(x), x, inc(y)) | | ifPlus(true, x, y) | → | p(y) |
| ifPlus(false, x, y) | → | plus(p(x), y) | | times(x, y) | → | timesIter(0, x, y, 0) |
| timesIter(i, x, y, z) | → | ifTimes(ge(i, x), i, x, y, z) | | ifTimes(true, i, x, y, z) | → | z |
| ifTimes(false, i, x, y, z) | → | timesIter(inc(i), x, y, plus(z, y)) | | isZero(0) | → | true |
| isZero(s(0)) | → | false | | isZero(s(s(x))) | → | isZero(s(x)) |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| inc(x) | → | s(x) | | p(0) | → | 0 |
| p(s(x)) | → | x | | p(s(s(x))) | → | s(p(s(x))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | f0(0, y, x) | → | f1(x, y, x) |
| f1(x, y, z) | → | f2(x, y, z) | | f2(x, 1, z) | → | f0(x, z, z) |
| f0(x, y, z) | → | d | | f1(x, y, z) | → | c |
Original Signature
Termination of terms over the following signature is verified: plus, ifTimes, d, c, true, ge, ifPlus, 1, timesIter, 0, inc, s, times, p, false, f1, f0, f2, isZero
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isZero#(s(s(x))) | → | isZero#(s(x)) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| plus(x, y) | → | ifPlus(isZero(x), x, inc(y)) | | ifPlus(true, x, y) | → | p(y) |
| ifPlus(false, x, y) | → | plus(p(x), y) | | times(x, y) | → | timesIter(0, x, y, 0) |
| timesIter(i, x, y, z) | → | ifTimes(ge(i, x), i, x, y, z) | | ifTimes(true, i, x, y, z) | → | z |
| ifTimes(false, i, x, y, z) | → | timesIter(inc(i), x, y, plus(z, y)) | | isZero(0) | → | true |
| isZero(s(0)) | → | false | | isZero(s(s(x))) | → | isZero(s(x)) |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| inc(x) | → | s(x) | | p(0) | → | 0 |
| p(s(x)) | → | x | | p(s(s(x))) | → | s(p(s(x))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | f0(0, y, x) | → | f1(x, y, x) |
| f1(x, y, z) | → | f2(x, y, z) | | f2(x, 1, z) | → | f0(x, z, z) |
| f0(x, y, z) | → | d | | f1(x, y, z) | → | c |
Original Signature
Termination of terms over the following signature is verified: plus, ifTimes, d, c, true, ge, ifPlus, 1, timesIter, 0, inc, s, times, p, false, f1, f0, f2, isZero
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ge#(s(x), s(y)) | → | ge#(x, y) |
Rewrite Rules
| plus(x, y) | → | ifPlus(isZero(x), x, inc(y)) | | ifPlus(true, x, y) | → | p(y) |
| ifPlus(false, x, y) | → | plus(p(x), y) | | times(x, y) | → | timesIter(0, x, y, 0) |
| timesIter(i, x, y, z) | → | ifTimes(ge(i, x), i, x, y, z) | | ifTimes(true, i, x, y, z) | → | z |
| ifTimes(false, i, x, y, z) | → | timesIter(inc(i), x, y, plus(z, y)) | | isZero(0) | → | true |
| isZero(s(0)) | → | false | | isZero(s(s(x))) | → | isZero(s(x)) |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| inc(x) | → | s(x) | | p(0) | → | 0 |
| p(s(x)) | → | x | | p(s(s(x))) | → | s(p(s(x))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | f0(0, y, x) | → | f1(x, y, x) |
| f1(x, y, z) | → | f2(x, y, z) | | f2(x, 1, z) | → | f0(x, z, z) |
| f0(x, y, z) | → | d | | f1(x, y, z) | → | c |
Original Signature
Termination of terms over the following signature is verified: plus, ifTimes, d, c, true, ge, ifPlus, 1, timesIter, 0, inc, s, times, p, false, f1, f0, f2, isZero
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ge#(s(x), s(y)) | → | ge#(x, y) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| plus(x, y) | → | ifPlus(isZero(x), x, inc(y)) | | ifPlus(true, x, y) | → | p(y) |
| ifPlus(false, x, y) | → | plus(p(x), y) | | times(x, y) | → | timesIter(0, x, y, 0) |
| timesIter(i, x, y, z) | → | ifTimes(ge(i, x), i, x, y, z) | | ifTimes(true, i, x, y, z) | → | z |
| ifTimes(false, i, x, y, z) | → | timesIter(inc(i), x, y, plus(z, y)) | | isZero(0) | → | true |
| isZero(s(0)) | → | false | | isZero(s(s(x))) | → | isZero(s(x)) |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| inc(x) | → | s(x) | | p(0) | → | 0 |
| p(s(x)) | → | x | | p(s(s(x))) | → | s(p(s(x))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) | | f0(0, y, x) | → | f1(x, y, x) |
| f1(x, y, z) | → | f2(x, y, z) | | f2(x, 1, z) | → | f0(x, z, z) |
| f0(x, y, z) | → | d | | f1(x, y, z) | → | c |
Original Signature
Termination of terms over the following signature is verified: plus, ifTimes, d, c, true, ge, ifPlus, 1, timesIter, 0, inc, s, times, p, false, f1, f0, f2, isZero
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed: