TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60010 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3076ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (10ms), PolynomialLinearRange4iUR (5001ms), DependencyGraph (5ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (5ms), ReductionPairSAT (6915ms)].
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (975ms), PolynomialLinearRange4iUR (5ms), DependencyGraph (795ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (796ms), ReductionPairSAT (timeout)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

isNatIList#(n__cons(V1, V2))U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))U41#(tt, V1, V2)U42#(isNat(activate(V1)), activate(V2))
U42#(tt, V2)isNatIList#(activate(V2))

Rewrite Rules

zeroscons(0, n__zeros)U11(tt, V1)U12(isNatList(activate(V1)))
U12(tt)ttU21(tt, V1)U22(isNat(activate(V1)))
U22(tt)ttU31(tt, V)U32(isNatList(activate(V)))
U32(tt)ttU41(tt, V1, V2)U42(isNat(activate(V1)), activate(V2))
U42(tt, V2)U43(isNatIList(activate(V2)))U43(tt)tt
U51(tt, V1, V2)U52(isNat(activate(V1)), activate(V2))U52(tt, V2)U53(isNatList(activate(V2)))
U53(tt)ttU61(tt, L)s(length(activate(L)))
and(tt, X)activate(X)isNat(n__0)tt
isNat(n__length(V1))U11(isNatIListKind(activate(V1)), activate(V1))isNat(n__s(V1))U21(isNatKind(activate(V1)), activate(V1))
isNatIList(V)U31(isNatIListKind(activate(V)), activate(V))isNatIList(n__zeros)tt
isNatIList(n__cons(V1, V2))U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNatIListKind(n__nil)tt
isNatIListKind(n__zeros)ttisNatIListKind(n__cons(V1, V2))and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatKind(n__0)ttisNatKind(n__length(V1))isNatIListKind(activate(V1))
isNatKind(n__s(V1))isNatKind(activate(V1))isNatList(n__nil)tt
isNatList(n__cons(V1, V2))U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))length(nil)0
length(cons(N, L))U61(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))zerosn__zeros
0n__0length(X)n__length(X)
s(X)n__s(X)cons(X1, X2)n__cons(X1, X2)
isNatIListKind(X)n__isNatIListKind(X)niln__nil
and(X1, X2)n__and(X1, X2)isNatKind(X)n__isNatKind(X)
activate(n__zeros)zerosactivate(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__isNatIListKind(X))isNatIListKind(X)
activate(n__nil)nilactivate(n__and(X1, X2))and(X1, X2)
activate(n__isNatKind(X))isNatKind(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__isNatIListKind, isNatIListKind, n__s, isNat, activate, n__0, U43, U61, U42, U41, length, n__nil, n__zeros, U21, U22, cons, isNatIList, n__length, isNatKind, and, n__and, n__cons, 0, isNatList, U51, s, tt, zeros, U53, U52, U11, U12, U31, U32, n__isNatKind, nil




Open Dependency Pair Problem 3

Dependency Pairs

and#(tt, X)activate#(X)length#(cons(N, L))isNat#(N)
U11#(tt, V1)isNatList#(activate(V1))U51#(tt, V1, V2)isNat#(activate(V1))
U51#(tt, V1, V2)activate#(V2)U51#(tt, V1, V2)activate#(V1)
length#(cons(N, L))U61#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))U52#(tt, V2)isNatList#(activate(V2))
U51#(tt, V1, V2)U52#(isNat(activate(V1)), activate(V2))isNatKind#(n__length(V1))activate#(V1)
isNatKind#(n__s(V1))activate#(V1)length#(cons(N, L))and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N)))
isNatList#(n__cons(V1, V2))isNatKind#(activate(V1))isNat#(n__s(V1))activate#(V1)
isNat#(n__length(V1))activate#(V1)isNatIListKind#(n__cons(V1, V2))activate#(V2)
activate#(n__isNatIListKind(X))isNatIListKind#(X)isNatList#(n__cons(V1, V2))U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
length#(cons(N, L))and#(isNatList(activate(L)), n__isNatIListKind(activate(L)))U52#(tt, V2)activate#(V2)
U21#(tt, V1)activate#(V1)isNatList#(n__cons(V1, V2))activate#(V2)
isNatKind#(n__length(V1))isNatIListKind#(activate(V1))isNatIListKind#(n__cons(V1, V2))isNatKind#(activate(V1))
isNat#(n__length(V1))U11#(isNatIListKind(activate(V1)), activate(V1))U11#(tt, V1)activate#(V1)
isNatList#(n__cons(V1, V2))and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))U61#(tt, L)length#(activate(L))
length#(cons(N, L))isNatList#(activate(L))activate#(n__length(X))length#(X)
activate#(n__isNatKind(X))isNatKind#(X)U61#(tt, L)activate#(L)
isNatIListKind#(n__cons(V1, V2))and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))isNatList#(n__cons(V1, V2))activate#(V1)
isNat#(n__length(V1))isNatIListKind#(activate(V1))U21#(tt, V1)isNat#(activate(V1))
isNatKind#(n__s(V1))isNatKind#(activate(V1))isNatIListKind#(n__cons(V1, V2))activate#(V1)
isNat#(n__s(V1))U21#(isNatKind(activate(V1)), activate(V1))activate#(n__and(X1, X2))and#(X1, X2)
isNat#(n__s(V1))isNatKind#(activate(V1))length#(cons(N, L))activate#(L)

Rewrite Rules

zeroscons(0, n__zeros)U11(tt, V1)U12(isNatList(activate(V1)))
U12(tt)ttU21(tt, V1)U22(isNat(activate(V1)))
U22(tt)ttU31(tt, V)U32(isNatList(activate(V)))
U32(tt)ttU41(tt, V1, V2)U42(isNat(activate(V1)), activate(V2))
U42(tt, V2)U43(isNatIList(activate(V2)))U43(tt)tt
U51(tt, V1, V2)U52(isNat(activate(V1)), activate(V2))U52(tt, V2)U53(isNatList(activate(V2)))
U53(tt)ttU61(tt, L)s(length(activate(L)))
and(tt, X)activate(X)isNat(n__0)tt
isNat(n__length(V1))U11(isNatIListKind(activate(V1)), activate(V1))isNat(n__s(V1))U21(isNatKind(activate(V1)), activate(V1))
isNatIList(V)U31(isNatIListKind(activate(V)), activate(V))isNatIList(n__zeros)tt
isNatIList(n__cons(V1, V2))U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNatIListKind(n__nil)tt
isNatIListKind(n__zeros)ttisNatIListKind(n__cons(V1, V2))and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatKind(n__0)ttisNatKind(n__length(V1))isNatIListKind(activate(V1))
isNatKind(n__s(V1))isNatKind(activate(V1))isNatList(n__nil)tt
isNatList(n__cons(V1, V2))U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))length(nil)0
length(cons(N, L))U61(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))zerosn__zeros
0n__0length(X)n__length(X)
s(X)n__s(X)cons(X1, X2)n__cons(X1, X2)
isNatIListKind(X)n__isNatIListKind(X)niln__nil
and(X1, X2)n__and(X1, X2)isNatKind(X)n__isNatKind(X)
activate(n__zeros)zerosactivate(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__isNatIListKind(X))isNatIListKind(X)
activate(n__nil)nilactivate(n__and(X1, X2))and(X1, X2)
activate(n__isNatKind(X))isNatKind(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__isNatIListKind, isNatIListKind, n__s, isNat, activate, n__0, U43, U61, U42, U41, length, n__nil, n__zeros, U21, U22, cons, isNatIList, n__length, isNatKind, and, n__and, n__cons, 0, isNatList, U51, s, tt, zeros, U53, U52, U11, U12, U31, U32, n__isNatKind, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

and#(tt, X)activate#(X)U11#(tt, V1)isNatList#(activate(V1))
isNatIList#(V)U31#(isNatIListKind(activate(V)), activate(V))U51#(tt, V1, V2)activate#(V1)
zeros#0#length#(cons(N, L))and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N)))
U21#(tt, V1)U22#(isNat(activate(V1)))U42#(tt, V2)U43#(isNatIList(activate(V2)))
isNatIList#(n__cons(V1, V2))U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNat#(n__length(V1))activate#(V1)
isNat#(n__s(V1))activate#(V1)activate#(n__isNatIListKind(X))isNatIListKind#(X)
isNatIListKind#(n__cons(V1, V2))activate#(V2)length#(nil)0#
U52#(tt, V2)activate#(V2)length#(cons(N, L))and#(isNatList(activate(L)), n__isNatIListKind(activate(L)))
isNatKind#(n__length(V1))isNatIListKind#(activate(V1))isNatIList#(V)isNatIListKind#(activate(V))
isNatList#(n__cons(V1, V2))activate#(V2)isNatIListKind#(n__cons(V1, V2))isNatKind#(activate(V1))
isNatList#(n__cons(V1, V2))and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))isNatIList#(n__cons(V1, V2))isNatKind#(activate(V1))
U61#(tt, L)s#(length(activate(L)))U11#(tt, V1)U12#(isNatList(activate(V1)))
U41#(tt, V1, V2)activate#(V1)length#(cons(N, L))isNatList#(activate(L))
activate#(n__isNatKind(X))isNatKind#(X)U61#(tt, L)activate#(L)
isNatIList#(n__cons(V1, V2))and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))activate#(n__0)0#
U41#(tt, V1, V2)U42#(isNat(activate(V1)), activate(V2))isNatKind#(n__s(V1))isNatKind#(activate(V1))
isNatIListKind#(n__cons(V1, V2))activate#(V1)isNat#(n__s(V1))U21#(isNatKind(activate(V1)), activate(V1))
isNat#(n__s(V1))isNatKind#(activate(V1))activate#(n__zeros)zeros#
isNatIList#(n__cons(V1, V2))activate#(V2)length#(cons(N, L))isNat#(N)
U51#(tt, V1, V2)isNat#(activate(V1))U51#(tt, V1, V2)activate#(V2)
length#(cons(N, L))U61#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))U52#(tt, V2)isNatList#(activate(V2))
U51#(tt, V1, V2)U52#(isNat(activate(V1)), activate(V2))isNatKind#(n__length(V1))activate#(V1)
isNatKind#(n__s(V1))activate#(V1)isNatList#(n__cons(V1, V2))isNatKind#(activate(V1))
U31#(tt, V)activate#(V)U42#(tt, V2)activate#(V2)
isNatIList#(V)activate#(V)activate#(n__cons(X1, X2))cons#(X1, X2)
U42#(tt, V2)isNatIList#(activate(V2))isNatList#(n__cons(V1, V2))U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
U41#(tt, V1, V2)isNat#(activate(V1))zeros#cons#(0, n__zeros)
U21#(tt, V1)activate#(V1)U31#(tt, V)isNatList#(activate(V))
isNat#(n__length(V1))U11#(isNatIListKind(activate(V1)), activate(V1))U11#(tt, V1)activate#(V1)
U41#(tt, V1, V2)activate#(V2)U52#(tt, V2)U53#(isNatList(activate(V2)))
U31#(tt, V)U32#(isNatList(activate(V)))U61#(tt, L)length#(activate(L))
activate#(n__s(X))s#(X)activate#(n__length(X))length#(X)
activate#(n__nil)nil#isNatIListKind#(n__cons(V1, V2))and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatList#(n__cons(V1, V2))activate#(V1)isNat#(n__length(V1))isNatIListKind#(activate(V1))
U21#(tt, V1)isNat#(activate(V1))isNatIList#(n__cons(V1, V2))activate#(V1)
activate#(n__and(X1, X2))and#(X1, X2)length#(cons(N, L))activate#(L)

Rewrite Rules

zeroscons(0, n__zeros)U11(tt, V1)U12(isNatList(activate(V1)))
U12(tt)ttU21(tt, V1)U22(isNat(activate(V1)))
U22(tt)ttU31(tt, V)U32(isNatList(activate(V)))
U32(tt)ttU41(tt, V1, V2)U42(isNat(activate(V1)), activate(V2))
U42(tt, V2)U43(isNatIList(activate(V2)))U43(tt)tt
U51(tt, V1, V2)U52(isNat(activate(V1)), activate(V2))U52(tt, V2)U53(isNatList(activate(V2)))
U53(tt)ttU61(tt, L)s(length(activate(L)))
and(tt, X)activate(X)isNat(n__0)tt
isNat(n__length(V1))U11(isNatIListKind(activate(V1)), activate(V1))isNat(n__s(V1))U21(isNatKind(activate(V1)), activate(V1))
isNatIList(V)U31(isNatIListKind(activate(V)), activate(V))isNatIList(n__zeros)tt
isNatIList(n__cons(V1, V2))U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNatIListKind(n__nil)tt
isNatIListKind(n__zeros)ttisNatIListKind(n__cons(V1, V2))and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatKind(n__0)ttisNatKind(n__length(V1))isNatIListKind(activate(V1))
isNatKind(n__s(V1))isNatKind(activate(V1))isNatList(n__nil)tt
isNatList(n__cons(V1, V2))U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))length(nil)0
length(cons(N, L))U61(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))zerosn__zeros
0n__0length(X)n__length(X)
s(X)n__s(X)cons(X1, X2)n__cons(X1, X2)
isNatIListKind(X)n__isNatIListKind(X)niln__nil
and(X1, X2)n__and(X1, X2)isNatKind(X)n__isNatKind(X)
activate(n__zeros)zerosactivate(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__isNatIListKind(X))isNatIListKind(X)
activate(n__nil)nilactivate(n__and(X1, X2))and(X1, X2)
activate(n__isNatKind(X))isNatKind(X)activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__isNatIListKind, isNatIListKind, activate, isNat, n__s, U61, U43, n__0, U42, U41, length, n__nil, n__zeros, U21, U22, cons, isNatIList, n__length, isNatKind, and, n__and, n__cons, 0, s, isNatList, U51, zeros, tt, U53, U52, U11, U12, U31, U32, nil, n__isNatKind

Strategy


The following SCCs where found

isNatIList#(n__cons(V1, V2)) → U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))U41#(tt, V1, V2) → U42#(isNat(activate(V1)), activate(V2))
U42#(tt, V2) → isNatIList#(activate(V2))

and#(tt, X) → activate#(X)U11#(tt, V1) → isNatList#(activate(V1))
length#(cons(N, L)) → isNat#(N)U51#(tt, V1, V2) → isNat#(activate(V1))
U51#(tt, V1, V2) → activate#(V1)U51#(tt, V1, V2) → activate#(V2)
length#(cons(N, L)) → U61#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))isNatKind#(n__length(V1)) → activate#(V1)
U51#(tt, V1, V2) → U52#(isNat(activate(V1)), activate(V2))U52#(tt, V2) → isNatList#(activate(V2))
isNatKind#(n__s(V1)) → activate#(V1)length#(cons(N, L)) → and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N)))
isNatList#(n__cons(V1, V2)) → isNatKind#(activate(V1))isNat#(n__length(V1)) → activate#(V1)
isNat#(n__s(V1)) → activate#(V1)activate#(n__isNatIListKind(X)) → isNatIListKind#(X)
isNatIListKind#(n__cons(V1, V2)) → activate#(V2)isNatList#(n__cons(V1, V2)) → U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
U52#(tt, V2) → activate#(V2)length#(cons(N, L)) → and#(isNatList(activate(L)), n__isNatIListKind(activate(L)))
U21#(tt, V1) → activate#(V1)isNatKind#(n__length(V1)) → isNatIListKind#(activate(V1))
isNatList#(n__cons(V1, V2)) → activate#(V2)isNatIListKind#(n__cons(V1, V2)) → isNatKind#(activate(V1))
U11#(tt, V1) → activate#(V1)isNat#(n__length(V1)) → U11#(isNatIListKind(activate(V1)), activate(V1))
isNatList#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))U61#(tt, L) → length#(activate(L))
activate#(n__length(X)) → length#(X)length#(cons(N, L)) → isNatList#(activate(L))
activate#(n__isNatKind(X)) → isNatKind#(X)U61#(tt, L) → activate#(L)
isNatIListKind#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))isNatList#(n__cons(V1, V2)) → activate#(V1)
isNat#(n__length(V1)) → isNatIListKind#(activate(V1))isNatIListKind#(n__cons(V1, V2)) → activate#(V1)
isNatKind#(n__s(V1)) → isNatKind#(activate(V1))U21#(tt, V1) → isNat#(activate(V1))
activate#(n__and(X1, X2)) → and#(X1, X2)isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
length#(cons(N, L)) → activate#(L)isNat#(n__s(V1)) → isNatKind#(activate(V1))