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 (185ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (379ms).
| | – Problem 8 was processed with processor DependencyGraph (3ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| | – Problem 7 was processed with processor DependencyGraph (3ms).
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (3307ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (2743ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (3ms), ReductionPairSAT (4148ms), DependencyGraph (2ms), SizeChangePrinciple (timeout)].
| – Problem 5 was processed with processor SubtermCriterion (0ms).
| – Problem 6 was processed with processor SubtermCriterion (0ms).
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| if#(false, x, y, z) | → | sortIter#(replace(min(x), head(x), tail(x)), z) | | sortIter#(x, y) | → | if#(empty(x), x, y, append(y, cons(min(x), nil))) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(x, nil)) | → | x |
| min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) | | if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) |
| if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) | | replace(n, m, nil) | → | nil |
| replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) | | if_replace(true, n, m, cons(k, x)) | → | cons(m, x) |
| if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) | | empty(nil) | → | true |
| empty(cons(n, x)) | → | false | | head(cons(n, x)) | → | n |
| tail(nil) | → | nil | | tail(cons(n, x)) | → | x |
| sort(x) | → | sortIter(x, nil) | | sortIter(x, y) | → | if(empty(x), x, y, append(y, cons(min(x), nil))) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | sortIter(replace(min(x), head(x), tail(x)), z) |
Original Signature
Termination of terms over the following signature is verified: min, append, sort, true, tail, if_replace, replace, if_min, 0, s, le, if, sortIter, empty, false, head, eq, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(false, x, y, z) | → | tail#(x) | | sortIter#(x, y) | → | min#(x) |
| if#(false, x, y, z) | → | min#(x) | | if#(false, x, y, z) | → | replace#(min(x), head(x), tail(x)) |
| if_min#(false, cons(n, cons(m, x))) | → | min#(cons(m, x)) | | replace#(n, m, cons(k, x)) | → | if_replace#(eq(n, k), n, m, cons(k, x)) |
| le#(s(n), s(m)) | → | le#(n, m) | | min#(cons(n, cons(m, x))) | → | if_min#(le(n, m), cons(n, cons(m, x))) |
| if#(false, x, y, z) | → | head#(x) | | eq#(s(n), s(m)) | → | eq#(n, m) |
| if#(false, x, y, z) | → | sortIter#(replace(min(x), head(x), tail(x)), z) | | min#(cons(n, cons(m, x))) | → | le#(n, m) |
| if_min#(true, cons(n, cons(m, x))) | → | min#(cons(n, x)) | | sort#(x) | → | sortIter#(x, nil) |
| replace#(n, m, cons(k, x)) | → | eq#(n, k) | | sortIter#(x, y) | → | empty#(x) |
| if_replace#(false, n, m, cons(k, x)) | → | replace#(n, m, x) | | sortIter#(x, y) | → | if#(empty(x), x, y, append(y, cons(min(x), nil))) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(x, nil)) | → | x |
| min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) | | if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) |
| if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) | | replace(n, m, nil) | → | nil |
| replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) | | if_replace(true, n, m, cons(k, x)) | → | cons(m, x) |
| if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) | | empty(nil) | → | true |
| empty(cons(n, x)) | → | false | | head(cons(n, x)) | → | n |
| tail(nil) | → | nil | | tail(cons(n, x)) | → | x |
| sort(x) | → | sortIter(x, nil) | | sortIter(x, y) | → | if(empty(x), x, y, append(y, cons(min(x), nil))) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | sortIter(replace(min(x), head(x), tail(x)), z) |
Original Signature
Termination of terms over the following signature is verified: min, append, sort, true, tail, if_replace, replace, if_min, 0, s, le, if, empty, sortIter, false, head, cons, nil, eq
Strategy
The following SCCs where found
| if#(false, x, y, z) → sortIter#(replace(min(x), head(x), tail(x)), z) | sortIter#(x, y) → if#(empty(x), x, y, append(y, cons(min(x), nil))) |
| replace#(n, m, cons(k, x)) → if_replace#(eq(n, k), n, m, cons(k, x)) | if_replace#(false, n, m, cons(k, x)) → replace#(n, m, x) |
| le#(s(n), s(m)) → le#(n, m) |
| if_min#(false, cons(n, cons(m, x))) → min#(cons(m, x)) | if_min#(true, cons(n, cons(m, x))) → min#(cons(n, x)) |
| min#(cons(n, cons(m, x))) → if_min#(le(n, m), cons(n, cons(m, x))) |
| eq#(s(n), s(m)) → eq#(n, m) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| if_min#(false, cons(n, cons(m, x))) | → | min#(cons(m, x)) | | if_min#(true, cons(n, cons(m, x))) | → | min#(cons(n, x)) |
| min#(cons(n, cons(m, x))) | → | if_min#(le(n, m), cons(n, cons(m, x))) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(x, nil)) | → | x |
| min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) | | if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) |
| if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) | | replace(n, m, nil) | → | nil |
| replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) | | if_replace(true, n, m, cons(k, x)) | → | cons(m, x) |
| if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) | | empty(nil) | → | true |
| empty(cons(n, x)) | → | false | | head(cons(n, x)) | → | n |
| tail(nil) | → | nil | | tail(cons(n, x)) | → | x |
| sort(x) | → | sortIter(x, nil) | | sortIter(x, y) | → | if(empty(x), x, y, append(y, cons(min(x), nil))) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | sortIter(replace(min(x), head(x), tail(x)), z) |
Original Signature
Termination of terms over the following signature is verified: min, append, sort, true, tail, if_replace, replace, if_min, 0, s, le, if, empty, sortIter, false, head, cons, nil, eq
Strategy
Polynomial Interpretation
- 0: 3
- append(x,y): 0
- cons(x,y): y + 1
- empty(x): 0
- eq(x,y): 0
- false: 0
- head(x): 0
- if(x1,x2,x3,x4): 0
- if_min(x,y): 0
- if_min#(x,y): y
- if_replace(x1,x2,x3,x4): 0
- le(x,y): 1
- min(x): 0
- min#(x): x + 1
- nil: 0
- replace(x,y,z): 0
- s(x): 3x
- sort(x): 0
- sortIter(x,y): 0
- tail(x): 0
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| min#(cons(n, cons(m, x))) | → | if_min#(le(n, m), cons(n, cons(m, x))) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if_min#(true, cons(n, cons(m, x))) | → | min#(cons(n, x)) | | if_min#(false, cons(n, cons(m, x))) | → | min#(cons(m, x)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(x, nil)) | → | x |
| min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) | | if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) |
| if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) | | replace(n, m, nil) | → | nil |
| replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) | | if_replace(true, n, m, cons(k, x)) | → | cons(m, x) |
| if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) | | empty(nil) | → | true |
| empty(cons(n, x)) | → | false | | head(cons(n, x)) | → | n |
| tail(nil) | → | nil | | tail(cons(n, x)) | → | x |
| sort(x) | → | sortIter(x, nil) | | sortIter(x, y) | → | if(empty(x), x, y, append(y, cons(min(x), nil))) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | sortIter(replace(min(x), head(x), tail(x)), z) |
Original Signature
Termination of terms over the following signature is verified: min, append, sort, true, tail, if_replace, replace, if_min, 0, s, le, if, sortIter, empty, false, head, eq, nil, cons
Strategy
There are no SCCs!
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| replace#(n, m, cons(k, x)) | → | if_replace#(eq(n, k), n, m, cons(k, x)) | | if_replace#(false, n, m, cons(k, x)) | → | replace#(n, m, x) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(x, nil)) | → | x |
| min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) | | if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) |
| if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) | | replace(n, m, nil) | → | nil |
| replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) | | if_replace(true, n, m, cons(k, x)) | → | cons(m, x) |
| if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) | | empty(nil) | → | true |
| empty(cons(n, x)) | → | false | | head(cons(n, x)) | → | n |
| tail(nil) | → | nil | | tail(cons(n, x)) | → | x |
| sort(x) | → | sortIter(x, nil) | | sortIter(x, y) | → | if(empty(x), x, y, append(y, cons(min(x), nil))) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | sortIter(replace(min(x), head(x), tail(x)), z) |
Original Signature
Termination of terms over the following signature is verified: min, append, sort, true, tail, if_replace, replace, if_min, 0, s, le, if, empty, sortIter, false, head, cons, nil, eq
Strategy
Projection
The following projection was used:
- π (replace#): 3
- π (if_replace#): 4
Thus, the following dependency pairs are removed:
| if_replace#(false, n, m, cons(k, x)) | → | replace#(n, m, x) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| replace#(n, m, cons(k, x)) | → | if_replace#(eq(n, k), n, m, cons(k, x)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(x, nil)) | → | x |
| min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) | | if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) |
| if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) | | replace(n, m, nil) | → | nil |
| replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) | | if_replace(true, n, m, cons(k, x)) | → | cons(m, x) |
| if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) | | empty(nil) | → | true |
| empty(cons(n, x)) | → | false | | head(cons(n, x)) | → | n |
| tail(nil) | → | nil | | tail(cons(n, x)) | → | x |
| sort(x) | → | sortIter(x, nil) | | sortIter(x, y) | → | if(empty(x), x, y, append(y, cons(min(x), nil))) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | sortIter(replace(min(x), head(x), tail(x)), z) |
Original Signature
Termination of terms over the following signature is verified: min, append, sort, true, tail, if_replace, replace, if_min, 0, s, le, if, sortIter, empty, false, head, eq, nil, cons
Strategy
There are no SCCs!
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(n), s(m)) | → | le#(n, m) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(x, nil)) | → | x |
| min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) | | if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) |
| if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) | | replace(n, m, nil) | → | nil |
| replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) | | if_replace(true, n, m, cons(k, x)) | → | cons(m, x) |
| if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) | | empty(nil) | → | true |
| empty(cons(n, x)) | → | false | | head(cons(n, x)) | → | n |
| tail(nil) | → | nil | | tail(cons(n, x)) | → | x |
| sort(x) | → | sortIter(x, nil) | | sortIter(x, y) | → | if(empty(x), x, y, append(y, cons(min(x), nil))) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | sortIter(replace(min(x), head(x), tail(x)), z) |
Original Signature
Termination of terms over the following signature is verified: min, append, sort, true, tail, if_replace, replace, if_min, 0, s, le, if, empty, sortIter, false, head, cons, nil, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(n), s(m)) | → | le#(n, m) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(s(n), s(m)) | → | eq#(n, m) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(x, nil)) | → | x |
| min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) | | if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) |
| if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) | | replace(n, m, nil) | → | nil |
| replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) | | if_replace(true, n, m, cons(k, x)) | → | cons(m, x) |
| if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) | | empty(nil) | → | true |
| empty(cons(n, x)) | → | false | | head(cons(n, x)) | → | n |
| tail(nil) | → | nil | | tail(cons(n, x)) | → | x |
| sort(x) | → | sortIter(x, nil) | | sortIter(x, y) | → | if(empty(x), x, y, append(y, cons(min(x), nil))) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | sortIter(replace(min(x), head(x), tail(x)), z) |
Original Signature
Termination of terms over the following signature is verified: min, append, sort, true, tail, if_replace, replace, if_min, 0, s, le, if, empty, sortIter, false, head, cons, nil, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(s(n), s(m)) | → | eq#(n, m) |