TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60004 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (165ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (982ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (724ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (6290ms), DependencyGraph (3ms), ReductionPairSAT (timeout)].
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (3101ms).
| | – Problem 4 was processed with processor DependencyGraph (21ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| length#(cons(N, L)) | → | U11#(tt, activate(L)) | | U12#(tt, L) | → | length#(activate(L)) |
| U11#(tt, L) | → | U12#(tt, activate(L)) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, L) | → | U12(tt, activate(L)) |
| U12(tt, L) | → | s(length(activate(L))) | | U21(tt, IL, M, N) | → | U22(tt, activate(IL), activate(M), activate(N)) |
| U22(tt, IL, M, N) | → | U23(tt, activate(IL), activate(M), activate(N)) | | U23(tt, IL, M, N) | → | cons(activate(N), n__take(activate(M), activate(IL))) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, activate(L)) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, activate(IL), M, N) |
| zeros | → | n__zeros | | take(X1, X2) | → | n__take(X1, X2) |
| activate(n__zeros) | → | zeros | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__take, activate, 0, s, zeros, tt, take, length, U11, U12, U23, n__zeros, U21, nil, cons, U22
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| take#(s(M), cons(N, IL)) | → | U21#(tt, activate(IL), M, N) | | U21#(tt, IL, M, N) | → | U22#(tt, activate(IL), activate(M), activate(N)) |
| activate#(n__zeros) | → | zeros# | | length#(cons(N, L)) | → | U11#(tt, activate(L)) |
| U12#(tt, L) | → | activate#(L) | | U21#(tt, IL, M, N) | → | activate#(N) |
| U22#(tt, IL, M, N) | → | U23#(tt, activate(IL), activate(M), activate(N)) | | U23#(tt, IL, M, N) | → | activate#(N) |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | | U11#(tt, L) | → | activate#(L) |
| U23#(tt, IL, M, N) | → | activate#(M) | | U21#(tt, IL, M, N) | → | activate#(IL) |
| U21#(tt, IL, M, N) | → | activate#(M) | | U22#(tt, IL, M, N) | → | activate#(N) |
| U22#(tt, IL, M, N) | → | activate#(IL) | | activate#(n__take(X1, X2)) | → | activate#(X1) |
| U22#(tt, IL, M, N) | → | activate#(M) | | U12#(tt, L) | → | length#(activate(L)) |
| take#(s(M), cons(N, IL)) | → | activate#(IL) | | activate#(n__take(X1, X2)) | → | activate#(X2) |
| U11#(tt, L) | → | U12#(tt, activate(L)) | | U23#(tt, IL, M, N) | → | activate#(IL) |
| length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, L) | → | U12(tt, activate(L)) |
| U12(tt, L) | → | s(length(activate(L))) | | U21(tt, IL, M, N) | → | U22(tt, activate(IL), activate(M), activate(N)) |
| U22(tt, IL, M, N) | → | U23(tt, activate(IL), activate(M), activate(N)) | | U23(tt, IL, M, N) | → | cons(activate(N), n__take(activate(M), activate(IL))) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, activate(L)) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, activate(IL), M, N) |
| zeros | → | n__zeros | | take(X1, X2) | → | n__take(X1, X2) |
| activate(n__zeros) | → | zeros | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__take, activate, 0, s, zeros, tt, take, length, U11, U12, U23, n__zeros, U21, U22, cons, nil
Strategy
The following SCCs where found
| length#(cons(N, L)) → U11#(tt, activate(L)) | U12#(tt, L) → length#(activate(L)) |
| U11#(tt, L) → U12#(tt, activate(L)) |
| U21#(tt, IL, M, N) → U22#(tt, activate(IL), activate(M), activate(N)) | take#(s(M), cons(N, IL)) → U21#(tt, activate(IL), M, N) |
| U21#(tt, IL, M, N) → activate#(N) | U23#(tt, IL, M, N) → activate#(N) |
| U22#(tt, IL, M, N) → U23#(tt, activate(IL), activate(M), activate(N)) | activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) |
| U23#(tt, IL, M, N) → activate#(M) | U21#(tt, IL, M, N) → activate#(IL) |
| U21#(tt, IL, M, N) → activate#(M) | U22#(tt, IL, M, N) → activate#(N) |
| U22#(tt, IL, M, N) → activate#(IL) | activate#(n__take(X1, X2)) → activate#(X1) |
| U22#(tt, IL, M, N) → activate#(M) | activate#(n__take(X1, X2)) → activate#(X2) |
| take#(s(M), cons(N, IL)) → activate#(IL) | U23#(tt, IL, M, N) → activate#(IL) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| take#(s(M), cons(N, IL)) | → | U21#(tt, activate(IL), M, N) | | U21#(tt, IL, M, N) | → | U22#(tt, activate(IL), activate(M), activate(N)) |
| U21#(tt, IL, M, N) | → | activate#(N) | | U22#(tt, IL, M, N) | → | U23#(tt, activate(IL), activate(M), activate(N)) |
| U23#(tt, IL, M, N) | → | activate#(N) | | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) |
| U23#(tt, IL, M, N) | → | activate#(M) | | U21#(tt, IL, M, N) | → | activate#(IL) |
| U21#(tt, IL, M, N) | → | activate#(M) | | U22#(tt, IL, M, N) | → | activate#(N) |
| U22#(tt, IL, M, N) | → | activate#(IL) | | activate#(n__take(X1, X2)) | → | activate#(X1) |
| U22#(tt, IL, M, N) | → | activate#(M) | | activate#(n__take(X1, X2)) | → | activate#(X2) |
| take#(s(M), cons(N, IL)) | → | activate#(IL) | | U23#(tt, IL, M, N) | → | activate#(IL) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, L) | → | U12(tt, activate(L)) |
| U12(tt, L) | → | s(length(activate(L))) | | U21(tt, IL, M, N) | → | U22(tt, activate(IL), activate(M), activate(N)) |
| U22(tt, IL, M, N) | → | U23(tt, activate(IL), activate(M), activate(N)) | | U23(tt, IL, M, N) | → | cons(activate(N), n__take(activate(M), activate(IL))) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, activate(L)) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, activate(IL), M, N) |
| zeros | → | n__zeros | | take(X1, X2) | → | n__take(X1, X2) |
| activate(n__zeros) | → | zeros | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__take, activate, 0, s, zeros, tt, take, length, U11, U12, U23, n__zeros, U21, U22, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x,y): 0
- U12(x,y): 0
- U21(x1,x2,x3,x4): x4 + 2x3 + x2 + x1 + 1
- U21#(x1,x2,x3,x4): 2x4 + 2x3 + 2x2
- U22(x1,x2,x3,x4): x4 + 2x3 + x2 + x1
- U22#(x1,x2,x3,x4): 2x4 + 2x3 + 2x2
- U23(x1,x2,x3,x4): x4 + 2x3 + x2 + 1
- U23#(x1,x2,x3,x4): 2x4 + 2x3 + 2x2
- activate(x): x
- activate#(x): 2x
- cons(x,y): y + x
- length(x): 0
- n__take(x,y): y + 2x + 1
- n__zeros: 0
- nil: 1
- s(x): x + 1
- take(x,y): y + 2x + 1
- take#(x,y): 2y + 2x
- tt: 2
- zeros: 0
Improved Usable rules
| activate(n__zeros) | → | zeros | | take(X1, X2) | → | n__take(X1, X2) |
| U23(tt, IL, M, N) | → | cons(activate(N), n__take(activate(M), activate(IL))) | | take(0, IL) | → | nil |
| zeros | → | cons(0, n__zeros) | | activate(X) | → | X |
| U22(tt, IL, M, N) | → | U23(tt, activate(IL), activate(M), activate(N)) | | U21(tt, IL, M, N) | → | U22(tt, activate(IL), activate(M), activate(N)) |
| take(s(M), cons(N, IL)) | → | U21(tt, activate(IL), M, N) | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| zeros | → | n__zeros |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| take#(s(M), cons(N, IL)) | → | U21#(tt, activate(IL), M, N) | | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) |
| activate#(n__take(X1, X2)) | → | activate#(X1) | | take#(s(M), cons(N, IL)) | → | activate#(IL) |
| activate#(n__take(X1, X2)) | → | activate#(X2) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U21#(tt, IL, M, N) | → | activate#(IL) | | U21#(tt, IL, M, N) | → | U22#(tt, activate(IL), activate(M), activate(N)) |
| U21#(tt, IL, M, N) | → | activate#(M) | | U22#(tt, IL, M, N) | → | activate#(N) |
| U21#(tt, IL, M, N) | → | activate#(N) | | U22#(tt, IL, M, N) | → | activate#(IL) |
| U23#(tt, IL, M, N) | → | activate#(N) | | U22#(tt, IL, M, N) | → | U23#(tt, activate(IL), activate(M), activate(N)) |
| U22#(tt, IL, M, N) | → | activate#(M) | | U23#(tt, IL, M, N) | → | activate#(IL) |
| U23#(tt, IL, M, N) | → | activate#(M) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, L) | → | U12(tt, activate(L)) |
| U12(tt, L) | → | s(length(activate(L))) | | U21(tt, IL, M, N) | → | U22(tt, activate(IL), activate(M), activate(N)) |
| U22(tt, IL, M, N) | → | U23(tt, activate(IL), activate(M), activate(N)) | | U23(tt, IL, M, N) | → | cons(activate(N), n__take(activate(M), activate(IL))) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, activate(L)) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, activate(IL), M, N) |
| zeros | → | n__zeros | | take(X1, X2) | → | n__take(X1, X2) |
| activate(n__zeros) | → | zeros | | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__take, activate, 0, s, zeros, tt, take, length, U11, U12, U23, n__zeros, U21, nil, cons, U22
Strategy
There are no SCCs!