TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60032 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (481ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (238ms), PolynomialLinearRange4iUR (10005ms), DependencyGraph (timeout), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (175ms), ReductionPairSAT (5756ms), DependencyGraph (177ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| and#(tt, X) | → | activate#(X) | | isNatIList#(n__cons(V1, V2)) | → | activate#(V2) |
| activate#(n__isNatIList(X)) | → | isNatIList#(X) | | isNatList#(n__cons(V1, V2)) | → | and#(isNat(activate(V1)), n__isNatList(activate(V2))) |
| isNatIList#(n__cons(V1, V2)) | → | and#(isNat(activate(V1)), n__isNatIList(activate(V2))) | | length#(cons(N, L)) | → | and#(isNatList(activate(L)), n__isNat(N)) |
| isNatList#(n__cons(V1, V2)) | → | isNat#(activate(V1)) | | activate#(n__isNat(X)) | → | isNat#(X) |
| isNatIList#(V) | → | activate#(V) | | isNat#(n__s(V1)) | → | activate#(V1) |
| isNat#(n__length(V1)) | → | activate#(V1) | | isNatIList#(V) | → | isNatList#(activate(V)) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V2) | | U11#(tt, L) | → | activate#(L) |
| activate#(n__isNatList(X)) | → | isNatList#(X) | | activate#(n__length(X)) | → | length#(X) |
| length#(cons(N, L)) | → | isNatList#(activate(L)) | | isNat#(n__length(V1)) | → | isNatList#(activate(V1)) |
| isNat#(n__s(V1)) | → | isNat#(activate(V1)) | | isNatList#(n__cons(V1, V2)) | → | activate#(V1) |
| isNatIList#(n__cons(V1, V2)) | → | isNat#(activate(V1)) | | U11#(tt, L) | → | length#(activate(L)) |
| isNatIList#(n__cons(V1, V2)) | → | activate#(V1) | | length#(cons(N, L)) | → | U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)) |
| length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, L) | → | s(length(activate(L))) |
| and(tt, X) | → | activate(X) | | isNat(n__0) | → | tt |
| isNat(n__length(V1)) | → | isNatList(activate(V1)) | | isNat(n__s(V1)) | → | isNat(activate(V1)) |
| isNatIList(V) | → | isNatList(activate(V)) | | isNatIList(n__zeros) | → | tt |
| isNatIList(n__cons(V1, V2)) | → | and(isNat(activate(V1)), n__isNatIList(activate(V2))) | | isNatList(n__nil) | → | tt |
| isNatList(n__cons(V1, V2)) | → | and(isNat(activate(V1)), n__isNatList(activate(V2))) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)) | | zeros | → | n__zeros |
| 0 | → | n__0 | | length(X) | → | n__length(X) |
| s(X) | → | n__s(X) | | cons(X1, X2) | → | n__cons(X1, X2) |
| isNatIList(X) | → | n__isNatIList(X) | | nil | → | n__nil |
| isNatList(X) | → | n__isNatList(X) | | isNat(X) | → | n__isNat(X) |
| activate(n__zeros) | → | zeros | | activate(n__0) | → | 0 |
| activate(n__length(X)) | → | length(X) | | activate(n__s(X)) | → | s(X) |
| activate(n__cons(X1, X2)) | → | cons(X1, X2) | | activate(n__isNatIList(X)) | → | isNatIList(X) |
| activate(n__nil) | → | nil | | activate(n__isNatList(X)) | → | isNatList(X) |
| activate(n__isNat(X)) | → | isNat(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: isNatIList, n__isNatIList, n__length, n__isNat, n__isNatList, and, n__s, activate, isNat, n__cons, 0, n__0, s, isNatList, zeros, tt, length, U11, n__nil, n__zeros, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNatIList#(n__cons(V1, V2)) | → | activate#(V2) | | and#(tt, X) | → | activate#(X) |
| activate#(n__zeros) | → | zeros# | | activate#(n__isNatIList(X)) | → | isNatIList#(X) |
| isNatList#(n__cons(V1, V2)) | → | and#(isNat(activate(V1)), n__isNatList(activate(V2))) | | zeros# | → | 0# |
| isNatIList#(n__cons(V1, V2)) | → | and#(isNat(activate(V1)), n__isNatIList(activate(V2))) | | length#(cons(N, L)) | → | and#(isNatList(activate(L)), n__isNat(N)) |
| isNatList#(n__cons(V1, V2)) | → | isNat#(activate(V1)) | | activate#(n__isNat(X)) | → | isNat#(X) |
| U11#(tt, L) | → | s#(length(activate(L))) | | isNatIList#(V) | → | activate#(V) |
| activate#(n__cons(X1, X2)) | → | cons#(X1, X2) | | isNat#(n__s(V1)) | → | activate#(V1) |
| isNat#(n__length(V1)) | → | activate#(V1) | | isNatIList#(V) | → | isNatList#(activate(V)) |
| length#(nil) | → | 0# | | zeros# | → | cons#(0, n__zeros) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V2) | | U11#(tt, L) | → | activate#(L) |
| activate#(n__isNatList(X)) | → | isNatList#(X) | | activate#(n__s(X)) | → | s#(X) |
| activate#(n__nil) | → | nil# | | activate#(n__length(X)) | → | length#(X) |
| length#(cons(N, L)) | → | isNatList#(activate(L)) | | isNat#(n__length(V1)) | → | isNatList#(activate(V1)) |
| isNat#(n__s(V1)) | → | isNat#(activate(V1)) | | isNatList#(n__cons(V1, V2)) | → | activate#(V1) |
| activate#(n__0) | → | 0# | | isNatIList#(n__cons(V1, V2)) | → | isNat#(activate(V1)) |
| isNatIList#(n__cons(V1, V2)) | → | activate#(V1) | | U11#(tt, L) | → | length#(activate(L)) |
| length#(cons(N, L)) | → | U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)) | | length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, L) | → | s(length(activate(L))) |
| and(tt, X) | → | activate(X) | | isNat(n__0) | → | tt |
| isNat(n__length(V1)) | → | isNatList(activate(V1)) | | isNat(n__s(V1)) | → | isNat(activate(V1)) |
| isNatIList(V) | → | isNatList(activate(V)) | | isNatIList(n__zeros) | → | tt |
| isNatIList(n__cons(V1, V2)) | → | and(isNat(activate(V1)), n__isNatIList(activate(V2))) | | isNatList(n__nil) | → | tt |
| isNatList(n__cons(V1, V2)) | → | and(isNat(activate(V1)), n__isNatList(activate(V2))) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)) | | zeros | → | n__zeros |
| 0 | → | n__0 | | length(X) | → | n__length(X) |
| s(X) | → | n__s(X) | | cons(X1, X2) | → | n__cons(X1, X2) |
| isNatIList(X) | → | n__isNatIList(X) | | nil | → | n__nil |
| isNatList(X) | → | n__isNatList(X) | | isNat(X) | → | n__isNat(X) |
| activate(n__zeros) | → | zeros | | activate(n__0) | → | 0 |
| activate(n__length(X)) | → | length(X) | | activate(n__s(X)) | → | s(X) |
| activate(n__cons(X1, X2)) | → | cons(X1, X2) | | activate(n__isNatIList(X)) | → | isNatIList(X) |
| activate(n__nil) | → | nil | | activate(n__isNatList(X)) | → | isNatList(X) |
| activate(n__isNat(X)) | → | isNat(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: isNatIList, n__isNatIList, n__length, n__isNat, n__isNatList, and, n__s, activate, isNat, n__cons, 0, n__0, isNatList, s, tt, zeros, length, U11, n__nil, n__zeros, cons, nil
Strategy
The following SCCs where found
| isNatIList#(n__cons(V1, V2)) → activate#(V2) | and#(tt, X) → activate#(X) |
| activate#(n__isNatIList(X)) → isNatIList#(X) | isNatList#(n__cons(V1, V2)) → and#(isNat(activate(V1)), n__isNatList(activate(V2))) |
| isNatIList#(n__cons(V1, V2)) → and#(isNat(activate(V1)), n__isNatIList(activate(V2))) | length#(cons(N, L)) → and#(isNatList(activate(L)), n__isNat(N)) |
| isNatList#(n__cons(V1, V2)) → isNat#(activate(V1)) | activate#(n__isNat(X)) → isNat#(X) |
| isNatIList#(V) → activate#(V) | isNat#(n__length(V1)) → activate#(V1) |
| isNat#(n__s(V1)) → activate#(V1) | isNatIList#(V) → isNatList#(activate(V)) |
| isNatList#(n__cons(V1, V2)) → activate#(V2) | U11#(tt, L) → activate#(L) |
| activate#(n__isNatList(X)) → isNatList#(X) | length#(cons(N, L)) → isNatList#(activate(L)) |
| activate#(n__length(X)) → length#(X) | isNat#(n__length(V1)) → isNatList#(activate(V1)) |
| isNat#(n__s(V1)) → isNat#(activate(V1)) | isNatList#(n__cons(V1, V2)) → activate#(V1) |
| isNatIList#(n__cons(V1, V2)) → isNat#(activate(V1)) | isNatIList#(n__cons(V1, V2)) → activate#(V1) |
| U11#(tt, L) → length#(activate(L)) | length#(cons(N, L)) → U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)) |
| length#(cons(N, L)) → activate#(L) |