TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3149ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (1933ms), PolynomialLinearRange4iUR (timeout), PolynomialLinearRange4iUR (0ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (1775ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

and#(tt, X) → activate#(X)U31#(tt, V1, V2) → U32#(isNat(activate(V1)), activate(V2))
U41#(tt, N) → activate#(N)isNat#(n__x(V1, V2)) → activate#(V2)
U51#(tt, M, N) → plus#(activate(N), activate(M))plus#(N, s(M)) → and#(isNat(M), n__isNatKind(M))
x#(N, s(M)) → and#(isNat(M), n__isNatKind(M))isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))
U71#(tt, M, N) → x#(activate(N), activate(M))x#(N, 0) → and#(isNat(N), n__isNatKind(N))
U11#(tt, V1, V2) → isNat#(activate(V1))U32#(tt, V2) → activate#(V2)
isNat#(n__s(V1)) → activate#(V1)isNat#(n__plus(V1, V2)) → U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
U12#(tt, V2) → isNat#(activate(V2))x#(N, s(M)) → isNat#(M)
isNat#(n__x(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))plus#(N, s(M)) → and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))
U31#(tt, V1, V2) → isNat#(activate(V1))activate#(n__x(X1, X2)) → x#(X1, X2)
isNatKind#(n__x(V1, V2)) → isNatKind#(activate(V1))U31#(tt, V1, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U71#(tt, M, N) → activate#(N)
activate#(n__isNatKind(X)) → isNatKind#(X)plus#(N, 0) → U41#(and(isNat(N), n__isNatKind(N)), N)
plus#(N, s(M)) → U51#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)U11#(tt, V1, V2) → U12#(isNat(activate(V1)), activate(V2))
isNat#(n__plus(V1, V2)) → activate#(V1)U51#(tt, M, N) → activate#(M)
isNatKind#(n__s(V1)) → isNatKind#(activate(V1))isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
isNat#(n__s(V1)) → isNatKind#(activate(V1))activate#(n__plus(X1, X2)) → plus#(X1, X2)
isNatKind#(n__x(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))U51#(tt, M, N) → activate#(N)
isNatKind#(n__x(V1, V2)) → activate#(V1)isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
plus#(N, s(M)) → isNat#(N)isNat#(n__x(V1, V2)) → isNatKind#(activate(V1))
plus#(N, 0) → and#(isNat(N), n__isNatKind(N))isNatKind#(n__s(V1)) → activate#(V1)
x#(N, s(M)) → U71#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)U12#(tt, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → activate#(V2)plus#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → activate#(V2)x#(N, 0) → isNat#(N)
isNatKind#(n__plus(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))U32#(tt, V2) → isNat#(activate(V2))
isNatKind#(n__plus(V1, V2)) → activate#(V2)isNatKind#(n__x(V1, V2)) → activate#(V2)
x#(N, s(M)) → isNat#(N)isNat#(n__x(V1, V2)) → activate#(V1)
U31#(tt, V1, V2) → activate#(V1)isNatKind#(n__plus(V1, V2)) → activate#(V1)
U21#(tt, V1) → activate#(V1)plus#(N, s(M)) → isNat#(M)
x#(N, s(M)) → and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))isNat#(n__plus(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
isNat#(n__x(V1, V2)) → U31#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))U71#(tt, M, N) → plus#(x(activate(N), activate(M)), activate(N))
U21#(tt, V1) → isNat#(activate(V1))U71#(tt, M, N) → activate#(M)
activate#(n__and(X1, X2)) → and#(X1, X2)

Rewrite Rules

U11(tt, V1, V2) → U12(isNat(activate(V1)), activate(V2))U12(tt, V2) → U13(isNat(activate(V2)))
U13(tt) → ttU21(tt, V1) → U22(isNat(activate(V1)))
U22(tt) → ttU31(tt, V1, V2) → U32(isNat(activate(V1)), activate(V2))
U32(tt, V2) → U33(isNat(activate(V2)))U33(tt) → tt
U41(tt, N) → activate(N)U51(tt, M, N) → s(plus(activate(N), activate(M)))
U61(tt) → 0U71(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
and(tt, X) → activate(X)isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))
isNat(n__x(V1, V2)) → U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))isNatKind(n__0) → tt
isNatKind(n__plus(V1, V2)) → and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))isNatKind(n__s(V1)) → isNatKind(activate(V1))
isNatKind(n__x(V1, V2)) → and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))plus(N, 0) → U41(and(isNat(N), n__isNatKind(N)), N)
plus(N, s(M)) → U51(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)x(N, 0) → U61(and(isNat(N), n__isNatKind(N)))
x(N, s(M)) → U71(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)0 → n__0
plus(X1, X2) → n__plus(X1, X2)isNatKind(X) → n__isNatKind(X)
s(X) → n__s(X)x(X1, X2) → n__x(X1, X2)
and(X1, X2) → n__and(X1, X2)activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(X1, X2)activate(n__isNatKind(X)) → isNatKind(X)
activate(n__s(X)) → s(X)activate(n__x(X1, X2)) → x(X1, X2)
activate(n__and(X1, X2)) → and(X1, X2)activate(X) → X

Original Signature

Termination of terms over the following signature is verified: n__plus, isNat, activate, n__s, U61, n__0, U41, U21, n__x, U22, plus, isNatKind, U71, and, n__and, 0, s, U51, tt, U11, U12, U31, U13, U32, U33, x, n__isNatKind

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U61#(tt) → 0#and#(tt, X) → activate#(X)
U31#(tt, V1, V2) → U32#(isNat(activate(V1)), activate(V2))U41#(tt, N) → activate#(N)
isNat#(n__x(V1, V2)) → activate#(V2)U51#(tt, M, N) → plus#(activate(N), activate(M))
x#(N, s(M)) → and#(isNat(M), n__isNatKind(M))plus#(N, s(M)) → and#(isNat(M), n__isNatKind(M))
U21#(tt, V1) → U22#(isNat(activate(V1)))U32#(tt, V2) → U33#(isNat(activate(V2)))
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))x#(N, 0) → and#(isNat(N), n__isNatKind(N))
U71#(tt, M, N) → x#(activate(N), activate(M))U11#(tt, V1, V2) → isNat#(activate(V1))
U32#(tt, V2) → activate#(V2)isNat#(n__s(V1)) → activate#(V1)
isNat#(n__plus(V1, V2)) → U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))U12#(tt, V2) → isNat#(activate(V2))
x#(N, s(M)) → isNat#(M)isNat#(n__x(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
plus#(N, s(M)) → and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))U31#(tt, V1, V2) → isNat#(activate(V1))
activate#(n__x(X1, X2)) → x#(X1, X2)isNatKind#(n__x(V1, V2)) → isNatKind#(activate(V1))
U31#(tt, V1, V2) → activate#(V2)U11#(tt, V1, V2) → activate#(V1)
U71#(tt, M, N) → activate#(N)activate#(n__isNatKind(X)) → isNatKind#(X)
plus#(N, 0) → U41#(and(isNat(N), n__isNatKind(N)), N)plus#(N, s(M)) → U51#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)
U11#(tt, V1, V2) → U12#(isNat(activate(V1)), activate(V2))activate#(n__0) → 0#
isNat#(n__plus(V1, V2)) → activate#(V1)U51#(tt, M, N) → activate#(M)
isNatKind#(n__s(V1)) → isNatKind#(activate(V1))isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
activate#(n__plus(X1, X2)) → plus#(X1, X2)U12#(tt, V2) → U13#(isNat(activate(V2)))
isNat#(n__s(V1)) → isNatKind#(activate(V1))U51#(tt, M, N) → activate#(N)
isNatKind#(n__x(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))isNatKind#(n__x(V1, V2)) → activate#(V1)
plus#(N, s(M)) → isNat#(N)isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
isNat#(n__x(V1, V2)) → isNatKind#(activate(V1))plus#(N, 0) → and#(isNat(N), n__isNatKind(N))
isNatKind#(n__s(V1)) → activate#(V1)x#(N, s(M)) → U71#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)
U12#(tt, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → activate#(V2)
plus#(N, 0) → isNat#(N)U11#(tt, V1, V2) → activate#(V2)
x#(N, 0) → isNat#(N)isNatKind#(n__plus(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
U32#(tt, V2) → isNat#(activate(V2))isNatKind#(n__plus(V1, V2)) → activate#(V2)
isNatKind#(n__x(V1, V2)) → activate#(V2)x#(N, s(M)) → isNat#(N)
isNat#(n__x(V1, V2)) → activate#(V1)U31#(tt, V1, V2) → activate#(V1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U21#(tt, V1) → activate#(V1)
x#(N, 0) → U61#(and(isNat(N), n__isNatKind(N)))U51#(tt, M, N) → s#(plus(activate(N), activate(M)))
activate#(n__s(X)) → s#(X)plus#(N, s(M)) → isNat#(M)
x#(N, s(M)) → and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))isNat#(n__plus(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
isNat#(n__x(V1, V2)) → U31#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))U71#(tt, M, N) → plus#(x(activate(N), activate(M)), activate(N))
U21#(tt, V1) → isNat#(activate(V1))U71#(tt, M, N) → activate#(M)
activate#(n__and(X1, X2)) → and#(X1, X2)

Rewrite Rules

U11(tt, V1, V2) → U12(isNat(activate(V1)), activate(V2))U12(tt, V2) → U13(isNat(activate(V2)))
U13(tt) → ttU21(tt, V1) → U22(isNat(activate(V1)))
U22(tt) → ttU31(tt, V1, V2) → U32(isNat(activate(V1)), activate(V2))
U32(tt, V2) → U33(isNat(activate(V2)))U33(tt) → tt
U41(tt, N) → activate(N)U51(tt, M, N) → s(plus(activate(N), activate(M)))
U61(tt) → 0U71(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
and(tt, X) → activate(X)isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))
isNat(n__x(V1, V2)) → U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))isNatKind(n__0) → tt
isNatKind(n__plus(V1, V2)) → and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))isNatKind(n__s(V1)) → isNatKind(activate(V1))
isNatKind(n__x(V1, V2)) → and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))plus(N, 0) → U41(and(isNat(N), n__isNatKind(N)), N)
plus(N, s(M)) → U51(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)x(N, 0) → U61(and(isNat(N), n__isNatKind(N)))
x(N, s(M)) → U71(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)0 → n__0
plus(X1, X2) → n__plus(X1, X2)isNatKind(X) → n__isNatKind(X)
s(X) → n__s(X)x(X1, X2) → n__x(X1, X2)
and(X1, X2) → n__and(X1, X2)activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(X1, X2)activate(n__isNatKind(X)) → isNatKind(X)
activate(n__s(X)) → s(X)activate(n__x(X1, X2)) → x(X1, X2)
activate(n__and(X1, X2)) → and(X1, X2)activate(X) → X

Original Signature

Termination of terms over the following signature is verified: n__plus, n__s, activate, isNat, n__0, U61, U41, U21, U22, n__x, plus, isNatKind, U71, and, n__and, 0, s, U51, tt, U11, U12, U31, U13, U32, U33, n__isNatKind, x

Strategy

The following SCCs where found

and#(tt, X) → activate#(X)U31#(tt, V1, V2) → U32#(isNat(activate(V1)), activate(V2))
U41#(tt, N) → activate#(N)isNat#(n__x(V1, V2)) → activate#(V2)
U51#(tt, M, N) → plus#(activate(N), activate(M))x#(N, s(M)) → and#(isNat(M), n__isNatKind(M))
plus#(N, s(M)) → and#(isNat(M), n__isNatKind(M))isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))
x#(N, 0) → and#(isNat(N), n__isNatKind(N))U71#(tt, M, N) → x#(activate(N), activate(M))
U11#(tt, V1, V2) → isNat#(activate(V1))U32#(tt, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))isNat#(n__s(V1)) → activate#(V1)
U12#(tt, V2) → isNat#(activate(V2))x#(N, s(M)) → isNat#(M)
isNat#(n__x(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))plus#(N, s(M)) → and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))
activate#(n__x(X1, X2)) → x#(X1, X2)U31#(tt, V1, V2) → isNat#(activate(V1))
isNatKind#(n__x(V1, V2)) → isNatKind#(activate(V1))U31#(tt, V1, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U71#(tt, M, N) → activate#(N)
activate#(n__isNatKind(X)) → isNatKind#(X)plus#(N, 0) → U41#(and(isNat(N), n__isNatKind(N)), N)
plus#(N, s(M)) → U51#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)U11#(tt, V1, V2) → U12#(isNat(activate(V1)), activate(V2))
isNat#(n__plus(V1, V2)) → activate#(V1)U51#(tt, M, N) → activate#(M)
isNatKind#(n__s(V1)) → isNatKind#(activate(V1))isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
activate#(n__plus(X1, X2)) → plus#(X1, X2)isNat#(n__s(V1)) → isNatKind#(activate(V1))
U51#(tt, M, N) → activate#(N)isNatKind#(n__x(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
isNatKind#(n__x(V1, V2)) → activate#(V1)plus#(N, s(M)) → isNat#(N)
isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))isNat#(n__x(V1, V2)) → isNatKind#(activate(V1))
plus#(N, 0) → and#(isNat(N), n__isNatKind(N))isNatKind#(n__s(V1)) → activate#(V1)
x#(N, s(M)) → U71#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)U12#(tt, V2) → activate#(V2)
plus#(N, 0) → isNat#(N)isNat#(n__plus(V1, V2)) → activate#(V2)
x#(N, 0) → isNat#(N)U11#(tt, V1, V2) → activate#(V2)
isNatKind#(n__plus(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))U32#(tt, V2) → isNat#(activate(V2))
isNatKind#(n__plus(V1, V2)) → activate#(V2)isNatKind#(n__x(V1, V2)) → activate#(V2)
x#(N, s(M)) → isNat#(N)isNat#(n__x(V1, V2)) → activate#(V1)
U31#(tt, V1, V2) → activate#(V1)isNatKind#(n__plus(V1, V2)) → activate#(V1)
U21#(tt, V1) → activate#(V1)plus#(N, s(M)) → isNat#(M)
x#(N, s(M)) → and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))isNat#(n__plus(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
U71#(tt, M, N) → plus#(x(activate(N), activate(M)), activate(N))isNat#(n__x(V1, V2)) → U31#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
U21#(tt, V1) → isNat#(activate(V1))activate#(n__and(X1, X2)) → and#(X1, X2)
U71#(tt, M, N) → activate#(M)