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)0n__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)0n__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)