TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (794ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (207ms), PolynomialLinearRange4iUR (5001ms), DependencyGraph (147ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (150ms), ReductionPairSAT (3971ms), DependencyGraph (163ms), SizeChangePrinciple (timeout)].
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (22ms), PolynomialLinearRange4iUR (65ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (24ms), DependencyGraph (2ms), ReductionPairSAT (1088ms), DependencyGraph (1ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| U61#(tt, L, N) | → | activate#(N) | | U51#(tt, V2) | → | isNatList#(activate(V2)) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V2) | | activate#(n__length(X)) | → | activate#(X) |
| activate#(n__s(X)) | → | activate#(X) | | isNatList#(n__cons(V1, V2)) | → | isNat#(activate(V1)) |
| U61#(tt, L, N) | → | activate#(L) | | U62#(tt, L) | → | length#(activate(L)) |
| activate#(n__length(X)) | → | length#(activate(X)) | | length#(cons(N, L)) | → | isNatList#(activate(L)) |
| isNat#(n__length(V1)) | → | isNatList#(activate(V1)) | | activate#(n__cons(X1, X2)) | → | activate#(X1) |
| U61#(tt, L, N) | → | isNat#(activate(N)) | | isNat#(n__s(V1)) | → | isNat#(activate(V1)) |
| isNatList#(n__cons(V1, V2)) | → | U51#(isNat(activate(V1)), activate(V2)) | | U61#(tt, L, N) | → | U62#(isNat(activate(N)), activate(L)) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V1) | | length#(cons(N, L)) | → | U61#(isNatList(activate(L)), activate(L), N) |
| U51#(tt, V2) | → | activate#(V2) | | isNat#(n__length(V1)) | → | activate#(V1) |
| isNat#(n__s(V1)) | → | activate#(V1) | | U62#(tt, L) | → | activate#(L) |
| length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt) | → | tt |
| U41(tt, V2) | → | U42(isNatIList(activate(V2))) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isNatList(activate(V2))) | | U52(tt) | → | tt |
| U61(tt, L, N) | → | U62(isNat(activate(N)), activate(L)) | | U62(tt, L) | → | s(length(activate(L))) |
| isNat(n__0) | → | tt | | isNat(n__length(V1)) | → | U11(isNatList(activate(V1))) |
| isNat(n__s(V1)) | → | U21(isNat(activate(V1))) | | isNatIList(V) | → | U31(isNatList(activate(V))) |
| isNatIList(n__zeros) | → | tt | | isNatIList(n__cons(V1, V2)) | → | U41(isNat(activate(V1)), activate(V2)) |
| isNatList(n__nil) | → | tt | | isNatList(n__cons(V1, V2)) | → | U51(isNat(activate(V1)), activate(V2)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U61(isNatList(activate(L)), activate(L), N) |
| zeros | → | n__zeros | | 0 | → | n__0 |
| length(X) | → | n__length(X) | | s(X) | → | n__s(X) |
| cons(X1, X2) | → | n__cons(X1, X2) | | nil | → | n__nil |
| activate(n__zeros) | → | zeros | | activate(n__0) | → | 0 |
| activate(n__length(X)) | → | length(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | | activate(n__nil) | → | nil |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, isNat, n__s, U62, U61, n__0, U42, U41, length, n__nil, n__zeros, U21, cons, isNatIList, n__length, n__cons, 0, isNatList, U51, s, tt, zeros, U52, U11, U31, nil
Open Dependency Pair Problem 3
Dependency Pairs
| U41#(tt, V2) | → | isNatIList#(activate(V2)) | | isNatIList#(n__cons(V1, V2)) | → | U41#(isNat(activate(V1)), activate(V2)) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt) | → | tt |
| U41(tt, V2) | → | U42(isNatIList(activate(V2))) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isNatList(activate(V2))) | | U52(tt) | → | tt |
| U61(tt, L, N) | → | U62(isNat(activate(N)), activate(L)) | | U62(tt, L) | → | s(length(activate(L))) |
| isNat(n__0) | → | tt | | isNat(n__length(V1)) | → | U11(isNatList(activate(V1))) |
| isNat(n__s(V1)) | → | U21(isNat(activate(V1))) | | isNatIList(V) | → | U31(isNatList(activate(V))) |
| isNatIList(n__zeros) | → | tt | | isNatIList(n__cons(V1, V2)) | → | U41(isNat(activate(V1)), activate(V2)) |
| isNatList(n__nil) | → | tt | | isNatList(n__cons(V1, V2)) | → | U51(isNat(activate(V1)), activate(V2)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U61(isNatList(activate(L)), activate(L), N) |
| zeros | → | n__zeros | | 0 | → | n__0 |
| length(X) | → | n__length(X) | | s(X) | → | n__s(X) |
| cons(X1, X2) | → | n__cons(X1, X2) | | nil | → | n__nil |
| activate(n__zeros) | → | zeros | | activate(n__0) | → | 0 |
| activate(n__length(X)) | → | length(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | | activate(n__nil) | → | nil |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, isNat, n__s, U62, U61, n__0, U42, U41, length, n__nil, n__zeros, U21, cons, isNatIList, n__length, n__cons, 0, isNatList, U51, s, tt, zeros, U52, U11, U31, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U61#(tt, L, N) | → | activate#(N) | | isNatIList#(n__cons(V1, V2)) | → | activate#(V2) |
| activate#(n__zeros) | → | zeros# | | U51#(tt, V2) | → | isNatList#(activate(V2)) |
| activate#(n__length(X)) | → | activate#(X) | | zeros# | → | 0# |
| activate#(n__s(X)) | → | activate#(X) | | isNatList#(n__cons(V1, V2)) | → | isNat#(activate(V1)) |
| U62#(tt, L) | → | length#(activate(L)) | | isNat#(n__length(V1)) | → | U11#(isNatList(activate(V1))) |
| U41#(tt, V2) | → | U42#(isNatIList(activate(V2))) | | activate#(n__cons(X1, X2)) | → | cons#(activate(X1), X2) |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | | U41#(tt, V2) | → | activate#(V2) |
| isNatIList#(n__cons(V1, V2)) | → | U41#(isNat(activate(V1)), activate(V2)) | | U51#(tt, V2) | → | U52#(isNatList(activate(V2))) |
| length#(cons(N, L)) | → | U61#(isNatList(activate(L)), activate(L), N) | | isNatIList#(V) | → | activate#(V) |
| U51#(tt, V2) | → | activate#(V2) | | isNat#(n__length(V1)) | → | activate#(V1) |
| isNat#(n__s(V1)) | → | activate#(V1) | | length#(nil) | → | 0# |
| isNatIList#(V) | → | isNatList#(activate(V)) | | zeros# | → | cons#(0, n__zeros) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V2) | | isNatIList#(V) | → | U31#(isNatList(activate(V))) |
| U62#(tt, L) | → | s#(length(activate(L))) | | U61#(tt, L, N) | → | activate#(L) |
| activate#(n__length(X)) | → | length#(activate(X)) | | length#(cons(N, L)) | → | isNatList#(activate(L)) |
| activate#(n__nil) | → | nil# | | isNat#(n__length(V1)) | → | isNatList#(activate(V1)) |
| U41#(tt, V2) | → | isNatIList#(activate(V2)) | | isNat#(n__s(V1)) | → | U21#(isNat(activate(V1))) |
| U61#(tt, L, N) | → | isNat#(activate(N)) | | isNat#(n__s(V1)) | → | isNat#(activate(V1)) |
| isNatList#(n__cons(V1, V2)) | → | U51#(isNat(activate(V1)), activate(V2)) | | U61#(tt, L, N) | → | U62#(isNat(activate(N)), activate(L)) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V1) | | activate#(n__0) | → | 0# |
| isNatIList#(n__cons(V1, V2)) | → | isNat#(activate(V1)) | | activate#(n__s(X)) | → | s#(activate(X)) |
| isNatIList#(n__cons(V1, V2)) | → | activate#(V1) | | U62#(tt, L) | → | activate#(L) |
| length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt) | → | tt |
| U41(tt, V2) | → | U42(isNatIList(activate(V2))) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isNatList(activate(V2))) | | U52(tt) | → | tt |
| U61(tt, L, N) | → | U62(isNat(activate(N)), activate(L)) | | U62(tt, L) | → | s(length(activate(L))) |
| isNat(n__0) | → | tt | | isNat(n__length(V1)) | → | U11(isNatList(activate(V1))) |
| isNat(n__s(V1)) | → | U21(isNat(activate(V1))) | | isNatIList(V) | → | U31(isNatList(activate(V))) |
| isNatIList(n__zeros) | → | tt | | isNatIList(n__cons(V1, V2)) | → | U41(isNat(activate(V1)), activate(V2)) |
| isNatList(n__nil) | → | tt | | isNatList(n__cons(V1, V2)) | → | U51(isNat(activate(V1)), activate(V2)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U61(isNatList(activate(L)), activate(L), N) |
| zeros | → | n__zeros | | 0 | → | n__0 |
| length(X) | → | n__length(X) | | s(X) | → | n__s(X) |
| cons(X1, X2) | → | n__cons(X1, X2) | | nil | → | n__nil |
| activate(n__zeros) | → | zeros | | activate(n__0) | → | 0 |
| activate(n__length(X)) | → | length(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | | activate(n__nil) | → | nil |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__s, isNat, activate, U62, n__0, U61, U42, U41, length, n__nil, n__zeros, U21, cons, isNatIList, n__length, n__cons, 0, isNatList, U51, s, tt, zeros, U52, U11, U31, nil
Strategy
The following SCCs where found
| U61#(tt, L, N) → activate#(N) | isNatList#(n__cons(V1, V2)) → activate#(V2) |
| U51#(tt, V2) → isNatList#(activate(V2)) | activate#(n__length(X)) → activate#(X) |
| activate#(n__s(X)) → activate#(X) | isNatList#(n__cons(V1, V2)) → isNat#(activate(V1)) |
| U61#(tt, L, N) → activate#(L) | activate#(n__length(X)) → length#(activate(X)) |
| U62#(tt, L) → length#(activate(L)) | length#(cons(N, L)) → isNatList#(activate(L)) |
| isNat#(n__length(V1)) → isNatList#(activate(V1)) | activate#(n__cons(X1, X2)) → activate#(X1) |
| U61#(tt, L, N) → isNat#(activate(N)) | isNat#(n__s(V1)) → isNat#(activate(V1)) |
| isNatList#(n__cons(V1, V2)) → U51#(isNat(activate(V1)), activate(V2)) | U61#(tt, L, N) → U62#(isNat(activate(N)), activate(L)) |
| isNatList#(n__cons(V1, V2)) → activate#(V1) | length#(cons(N, L)) → U61#(isNatList(activate(L)), activate(L), N) |
| U51#(tt, V2) → activate#(V2) | isNat#(n__s(V1)) → activate#(V1) |
| isNat#(n__length(V1)) → activate#(V1) | U62#(tt, L) → activate#(L) |
| length#(cons(N, L)) → activate#(L) |
| U41#(tt, V2) → isNatIList#(activate(V2)) | isNatIList#(n__cons(V1, V2)) → U41#(isNat(activate(V1)), activate(V2)) |