TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (126ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (1864ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (9223ms), DependencyGraph (1ms), ReductionPairSAT (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (2ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| if#(true, c, xs, ys, z) | → | if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Rewrite Rules
| min(0, y) | → | 0 | | min(s(x), 0) | → | 0 |
| min(s(x), s(y)) | → | min(x, y) | | len(nil) | → | 0 |
| len(cons(x, xs)) | → | s(len(xs)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) | | le(0, x) | → | true |
| le(s(x), 0) | → | false | | le(s(x), s(y)) | → | le(x, y) |
| take(0, cons(y, ys)) | → | y | | take(s(x), cons(y, ys)) | → | take(x, ys) |
| addList(x, y) | → | if(le(0, min(len(x), len(y))), 0, x, y, nil) | | if(false, c, x, y, z) | → | z |
| if(true, c, xs, ys, z) | → | if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Original Signature
Termination of terms over the following signature is verified: min, sum, true, len, 0, s, le, take, if, false, nil, cons, addList
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(true, c, xs, ys, z) | → | min#(len(xs), len(ys)) | | sum#(x, s(y)) | → | sum#(x, y) |
| addList#(x, y) | → | len#(y) | | if#(true, c, xs, ys, z) | → | le#(s(c), min(len(xs), len(ys))) |
| if#(true, c, xs, ys, z) | → | take#(c, ys) | | addList#(x, y) | → | len#(x) |
| if#(true, c, xs, ys, z) | → | len#(xs) | | if#(true, c, xs, ys, z) | → | len#(ys) |
| min#(s(x), s(y)) | → | min#(x, y) | | len#(cons(x, xs)) | → | len#(xs) |
| le#(s(x), s(y)) | → | le#(x, y) | | addList#(x, y) | → | le#(0, min(len(x), len(y))) |
| addList#(x, y) | → | min#(len(x), len(y)) | | if#(true, c, xs, ys, z) | → | take#(c, xs) |
| take#(s(x), cons(y, ys)) | → | take#(x, ys) | | if#(true, c, xs, ys, z) | → | sum#(take(c, xs), take(c, ys)) |
| if#(true, c, xs, ys, z) | → | if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) | | addList#(x, y) | → | if#(le(0, min(len(x), len(y))), 0, x, y, nil) |
Rewrite Rules
| min(0, y) | → | 0 | | min(s(x), 0) | → | 0 |
| min(s(x), s(y)) | → | min(x, y) | | len(nil) | → | 0 |
| len(cons(x, xs)) | → | s(len(xs)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) | | le(0, x) | → | true |
| le(s(x), 0) | → | false | | le(s(x), s(y)) | → | le(x, y) |
| take(0, cons(y, ys)) | → | y | | take(s(x), cons(y, ys)) | → | take(x, ys) |
| addList(x, y) | → | if(le(0, min(len(x), len(y))), 0, x, y, nil) | | if(false, c, x, y, z) | → | z |
| if(true, c, xs, ys, z) | → | if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Original Signature
Termination of terms over the following signature is verified: min, sum, true, len, 0, s, le, take, if, false, nil, cons, addList
Strategy
The following SCCs where found
| le#(s(x), s(y)) → le#(x, y) |
| len#(cons(x, xs)) → len#(xs) |
| sum#(x, s(y)) → sum#(x, y) |
| min#(s(x), s(y)) → min#(x, y) |
| take#(s(x), cons(y, ys)) → take#(x, ys) |
| if#(true, c, xs, ys, z) → if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(x), s(y)) | → | le#(x, y) |
Rewrite Rules
| min(0, y) | → | 0 | | min(s(x), 0) | → | 0 |
| min(s(x), s(y)) | → | min(x, y) | | len(nil) | → | 0 |
| len(cons(x, xs)) | → | s(len(xs)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) | | le(0, x) | → | true |
| le(s(x), 0) | → | false | | le(s(x), s(y)) | → | le(x, y) |
| take(0, cons(y, ys)) | → | y | | take(s(x), cons(y, ys)) | → | take(x, ys) |
| addList(x, y) | → | if(le(0, min(len(x), len(y))), 0, x, y, nil) | | if(false, c, x, y, z) | → | z |
| if(true, c, xs, ys, z) | → | if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Original Signature
Termination of terms over the following signature is verified: min, sum, true, len, 0, s, le, take, if, false, nil, cons, addList
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(x), s(y)) | → | le#(x, y) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| min#(s(x), s(y)) | → | min#(x, y) |
Rewrite Rules
| min(0, y) | → | 0 | | min(s(x), 0) | → | 0 |
| min(s(x), s(y)) | → | min(x, y) | | len(nil) | → | 0 |
| len(cons(x, xs)) | → | s(len(xs)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) | | le(0, x) | → | true |
| le(s(x), 0) | → | false | | le(s(x), s(y)) | → | le(x, y) |
| take(0, cons(y, ys)) | → | y | | take(s(x), cons(y, ys)) | → | take(x, ys) |
| addList(x, y) | → | if(le(0, min(len(x), len(y))), 0, x, y, nil) | | if(false, c, x, y, z) | → | z |
| if(true, c, xs, ys, z) | → | if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Original Signature
Termination of terms over the following signature is verified: min, sum, true, len, 0, s, le, take, if, false, nil, cons, addList
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| min#(s(x), s(y)) | → | min#(x, y) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sum#(x, s(y)) | → | sum#(x, y) |
Rewrite Rules
| min(0, y) | → | 0 | | min(s(x), 0) | → | 0 |
| min(s(x), s(y)) | → | min(x, y) | | len(nil) | → | 0 |
| len(cons(x, xs)) | → | s(len(xs)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) | | le(0, x) | → | true |
| le(s(x), 0) | → | false | | le(s(x), s(y)) | → | le(x, y) |
| take(0, cons(y, ys)) | → | y | | take(s(x), cons(y, ys)) | → | take(x, ys) |
| addList(x, y) | → | if(le(0, min(len(x), len(y))), 0, x, y, nil) | | if(false, c, x, y, z) | → | z |
| if(true, c, xs, ys, z) | → | if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Original Signature
Termination of terms over the following signature is verified: min, sum, true, len, 0, s, le, take, if, false, nil, cons, addList
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sum#(x, s(y)) | → | sum#(x, y) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| take#(s(x), cons(y, ys)) | → | take#(x, ys) |
Rewrite Rules
| min(0, y) | → | 0 | | min(s(x), 0) | → | 0 |
| min(s(x), s(y)) | → | min(x, y) | | len(nil) | → | 0 |
| len(cons(x, xs)) | → | s(len(xs)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) | | le(0, x) | → | true |
| le(s(x), 0) | → | false | | le(s(x), s(y)) | → | le(x, y) |
| take(0, cons(y, ys)) | → | y | | take(s(x), cons(y, ys)) | → | take(x, ys) |
| addList(x, y) | → | if(le(0, min(len(x), len(y))), 0, x, y, nil) | | if(false, c, x, y, z) | → | z |
| if(true, c, xs, ys, z) | → | if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Original Signature
Termination of terms over the following signature is verified: min, sum, true, len, 0, s, le, take, if, false, nil, cons, addList
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| take#(s(x), cons(y, ys)) | → | take#(x, ys) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| len#(cons(x, xs)) | → | len#(xs) |
Rewrite Rules
| min(0, y) | → | 0 | | min(s(x), 0) | → | 0 |
| min(s(x), s(y)) | → | min(x, y) | | len(nil) | → | 0 |
| len(cons(x, xs)) | → | s(len(xs)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) | | le(0, x) | → | true |
| le(s(x), 0) | → | false | | le(s(x), s(y)) | → | le(x, y) |
| take(0, cons(y, ys)) | → | y | | take(s(x), cons(y, ys)) | → | take(x, ys) |
| addList(x, y) | → | if(le(0, min(len(x), len(y))), 0, x, y, nil) | | if(false, c, x, y, z) | → | z |
| if(true, c, xs, ys, z) | → | if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) |
Original Signature
Termination of terms over the following signature is verified: min, sum, true, len, 0, s, le, take, if, false, nil, cons, addList
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| len#(cons(x, xs)) | → | len#(xs) |