TIMEOUT

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (timeout)].

The following open problems remain:



Open Dependency Pair Problem 1

Dependency Pairs

U12#(active(X1), X2)U12#(X1, X2)mark#(U61(X))U61#(mark(X))
mark#(U11(X1, X2, X3))U11#(mark(X1), X2, X3)active#(U71(tt, M, N))x#(N, M)
U31#(X1, active(X2), X3)U31#(X1, X2, X3)x#(active(X1), X2)x#(X1, X2)
x#(X1, active(X2))x#(X1, X2)active#(plus(N, 0))and#(isNat(N), isNatKind(N))
active#(isNatKind(x(V1, V2)))isNatKind#(V2)active#(U61(tt))mark#(0)
isNat#(active(X))isNat#(X)U21#(X1, active(X2))U21#(X1, X2)
mark#(s(X))mark#(X)U71#(X1, mark(X2), X3)U71#(X1, X2, X3)
mark#(U12(X1, X2))mark#(X1)active#(isNat(x(V1, V2)))mark#(U31(and(isNatKind(V1), isNatKind(V2)), V1, V2))
mark#(U31(X1, X2, X3))active#(U31(mark(X1), X2, X3))mark#(plus(X1, X2))active#(plus(mark(X1), mark(X2)))
active#(plus(N, s(M)))and#(isNat(N), isNatKind(N))active#(U11(tt, V1, V2))mark#(U12(isNat(V1), V2))
and#(mark(X1), X2)and#(X1, X2)active#(U21(tt, V1))isNat#(V1)
active#(plus(N, s(M)))isNatKind#(M)active#(U51(tt, M, N))s#(plus(N, M))
mark#(U22(X))U22#(mark(X))mark#(U22(X))active#(U22(mark(X)))
mark#(U11(X1, X2, X3))mark#(X1)mark#(U13(X))U13#(mark(X))
U12#(X1, active(X2))U12#(X1, X2)active#(x(N, s(M)))and#(isNat(M), isNatKind(M))
U31#(active(X1), X2, X3)U31#(X1, X2, X3)active#(U71(tt, M, N))plus#(x(N, M), N)
active#(isNat(x(V1, V2)))isNatKind#(V1)mark#(U21(X1, X2))active#(U21(mark(X1), X2))
U32#(X1, active(X2))U32#(X1, X2)U11#(active(X1), X2, X3)U11#(X1, X2, X3)
mark#(U33(X))active#(U33(mark(X)))U71#(active(X1), X2, X3)U71#(X1, X2, X3)
active#(U32(tt, V2))isNat#(V2)mark#(U41(X1, X2))mark#(X1)
U41#(X1, active(X2))U41#(X1, X2)mark#(U61(X))mark#(X)
isNatKind#(mark(X))isNatKind#(X)mark#(isNatKind(X))isNatKind#(X)
active#(U11(tt, V1, V2))U12#(isNat(V1), V2)mark#(x(X1, X2))active#(x(mark(X1), mark(X2)))
U21#(active(X1), X2)U21#(X1, X2)U33#(mark(X))U33#(X)
active#(U31(tt, V1, V2))isNat#(V1)active#(plus(N, s(M)))and#(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
mark#(U71(X1, X2, X3))U71#(mark(X1), X2, X3)U31#(X1, X2, active(X3))U31#(X1, X2, X3)
active#(x(N, s(M)))isNat#(M)active#(isNat(s(V1)))U21#(isNatKind(V1), V1)
active#(x(N, s(M)))isNat#(N)U33#(active(X))U33#(X)
mark#(x(X1, X2))mark#(X1)active#(plus(N, s(M)))and#(isNat(M), isNatKind(M))
active#(isNatKind(x(V1, V2)))and#(isNatKind(V1), isNatKind(V2))active#(isNat(x(V1, V2)))isNatKind#(V2)
active#(plus(N, s(M)))mark#(U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N))mark#(s(X))s#(mark(X))
mark#(U11(X1, X2, X3))active#(U11(mark(X1), X2, X3))U12#(mark(X1), X2)U12#(X1, X2)
U22#(mark(X))U22#(X)active#(isNatKind(plus(V1, V2)))and#(isNatKind(V1), isNatKind(V2))
active#(x(N, s(M)))and#(isNat(N), isNatKind(N))active#(U32(tt, V2))mark#(U33(isNat(V2)))
U51#(X1, mark(X2), X3)U51#(X1, X2, X3)U41#(X1, mark(X2))U41#(X1, X2)
active#(isNat(0))mark#(tt)mark#(and(X1, X2))and#(mark(X1), X2)
active#(isNatKind(x(V1, V2)))mark#(and(isNatKind(V1), isNatKind(V2)))U11#(mark(X1), X2, X3)U11#(X1, X2, X3)
active#(U12(tt, V2))U13#(isNat(V2))mark#(U31(X1, X2, X3))mark#(X1)
active#(U21(tt, V1))U22#(isNat(V1))mark#(plus(X1, X2))mark#(X1)
mark#(x(X1, X2))mark#(X2)isNatKind#(active(X))isNatKind#(X)
U22#(active(X))U22#(X)active#(x(N, 0))U61#(and(isNat(N), isNatKind(N)))
U51#(active(X1), X2, X3)U51#(X1, X2, X3)active#(plus(N, s(M)))isNat#(N)
and#(X1, active(X2))and#(X1, X2)active#(plus(N, s(M)))isNatKind#(N)
U71#(X1, X2, active(X3))U71#(X1, X2, X3)mark#(U21(X1, X2))mark#(X1)
mark#(U21(X1, X2))U21#(mark(X1), X2)mark#(isNat(X))isNat#(X)
isNat#(mark(X))isNat#(X)active#(isNat(plus(V1, V2)))isNatKind#(V1)
active#(isNat(plus(V1, V2)))isNatKind#(V2)U11#(X1, X2, mark(X3))U11#(X1, X2, X3)
mark#(U61(X))active#(U61(mark(X)))U31#(X1, X2, mark(X3))U31#(X1, X2, X3)
U41#(mark(X1), X2)U41#(X1, X2)active#(U13(tt))mark#(tt)
active#(isNat(plus(V1, V2)))and#(isNatKind(V1), isNatKind(V2))and#(X1, mark(X2))and#(X1, X2)
U12#(X1, mark(X2))U12#(X1, X2)mark#(U32(X1, X2))active#(U32(mark(X1), X2))
active#(isNatKind(plus(V1, V2)))isNatKind#(V2)active#(isNat(s(V1)))mark#(U21(isNatKind(V1), V1))
mark#(plus(X1, X2))plus#(mark(X1), mark(X2))mark#(U12(X1, X2))U12#(mark(X1), X2)
s#(mark(X))s#(X)U32#(active(X1), X2)U32#(X1, X2)
mark#(U51(X1, X2, X3))U51#(mark(X1), X2, X3)active#(isNat(plus(V1, V2)))mark#(U11(and(isNatKind(V1), isNatKind(V2)), V1, V2))
U31#(X1, mark(X2), X3)U31#(X1, X2, X3)mark#(U13(X))mark#(X)
active#(isNatKind(0))mark#(tt)active#(isNat(x(V1, V2)))and#(isNatKind(V1), isNatKind(V2))
active#(U32(tt, V2))U33#(isNat(V2))active#(isNat(plus(V1, V2)))U11#(and(isNatKind(V1), isNatKind(V2)), V1, V2)
active#(isNatKind(plus(V1, V2)))isNatKind#(V1)active#(x(N, s(M)))isNatKind#(N)
active#(U22(tt))mark#(tt)active#(U12(tt, V2))isNat#(V2)
x#(X1, mark(X2))x#(X1, X2)mark#(U31(X1, X2, X3))U31#(mark(X1), X2, X3)
active#(plus(N, 0))isNat#(N)U51#(X1, X2, active(X3))U51#(X1, X2, X3)
U11#(X1, active(X2), X3)U11#(X1, X2, X3)U71#(mark(X1), X2, X3)U71#(X1, X2, X3)
U41#(active(X1), X2)U41#(X1, X2)mark#(U33(X))U33#(mark(X))
active#(isNat(s(V1)))isNatKind#(V1)mark#(and(X1, X2))mark#(X1)
mark#(U32(X1, X2))mark#(X1)U61#(active(X))U61#(X)
active#(U12(tt, V2))mark#(U13(isNat(V2)))plus#(mark(X1), X2)plus#(X1, X2)
active#(x(N, 0))mark#(U61(and(isNat(N), isNatKind(N))))plus#(active(X1), X2)plus#(X1, X2)
active#(plus(N, 0))mark#(U41(and(isNat(N), isNatKind(N)), N))active#(x(N, 0))isNat#(N)
mark#(tt)active#(tt)active#(plus(N, 0))U41#(and(isNat(N), isNatKind(N)), N)
mark#(U33(X))mark#(X)active#(x(N, s(M)))isNatKind#(M)
active#(U11(tt, V1, V2))isNat#(V1)mark#(U51(X1, X2, X3))mark#(X1)
U21#(X1, mark(X2))U21#(X1, X2)x#(mark(X1), X2)x#(X1, X2)
active#(plus(N, s(M)))U51#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)U13#(mark(X))U13#(X)
mark#(U13(X))active#(U13(mark(X)))active#(isNatKind(s(V1)))mark#(isNatKind(V1))
active#(U41(tt, N))mark#(N)active#(x(N, 0))isNatKind#(N)
mark#(0)active#(0)U51#(mark(X1), X2, X3)U51#(X1, X2, X3)
mark#(s(X))active#(s(mark(X)))active#(U51(tt, M, N))mark#(s(plus(N, M)))
U61#(mark(X))U61#(X)active#(isNat(x(V1, V2)))U31#(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U71#(X1, X2, mark(X3))U71#(X1, X2, X3)mark#(U22(X))mark#(X)
active#(U51(tt, M, N))plus#(N, M)active#(plus(N, s(M)))isNat#(M)
mark#(U51(X1, X2, X3))active#(U51(mark(X1), X2, X3))mark#(U12(X1, X2))active#(U12(mark(X1), X2))
active#(x(N, 0))and#(isNat(N), isNatKind(N))U13#(active(X))U13#(X)
mark#(x(X1, X2))x#(mark(X1), mark(X2))active#(U31(tt, V1, V2))U32#(isNat(V1), V2)
U11#(X1, X2, active(X3))U11#(X1, X2, X3)active#(x(N, s(M)))U71#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
active#(U21(tt, V1))mark#(U22(isNat(V1)))mark#(U71(X1, X2, X3))active#(U71(mark(X1), X2, X3))
mark#(isNatKind(X))active#(isNatKind(X))active#(x(N, s(M)))mark#(U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N))
mark#(U41(X1, X2))active#(U41(mark(X1), X2))U51#(X1, active(X2), X3)U51#(X1, X2, X3)
active#(U33(tt))mark#(tt)plus#(X1, mark(X2))plus#(X1, X2)
U71#(X1, active(X2), X3)U71#(X1, X2, X3)mark#(U71(X1, X2, X3))mark#(X1)
mark#(U32(X1, X2))U32#(mark(X1), X2)active#(isNatKind(plus(V1, V2)))mark#(and(isNatKind(V1), isNatKind(V2)))
active#(U31(tt, V1, V2))mark#(U32(isNat(V1), V2))mark#(U41(X1, X2))U41#(mark(X1), X2)
plus#(X1, active(X2))plus#(X1, X2)and#(active(X1), X2)and#(X1, X2)
mark#(isNat(X))active#(isNat(X))active#(plus(N, 0))isNatKind#(N)
U32#(X1, mark(X2))U32#(X1, X2)mark#(plus(X1, X2))mark#(X2)
mark#(and(X1, X2))active#(and(mark(X1), X2))active#(isNatKind(x(V1, V2)))isNatKind#(V1)
active#(x(N, s(M)))and#(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))active#(isNatKind(s(V1)))isNatKind#(V1)
active#(U71(tt, M, N))mark#(plus(x(N, M), N))U51#(X1, X2, mark(X3))U51#(X1, X2, X3)
active#(and(tt, X))mark#(X)U21#(mark(X1), X2)U21#(X1, X2)
U32#(mark(X1), X2)U32#(X1, X2)U11#(X1, mark(X2), X3)U11#(X1, X2, X3)
s#(active(X))s#(X)U31#(mark(X1), X2, X3)U31#(X1, X2, X3)

Rewrite Rules

active(U11(tt, V1, V2))mark(U12(isNat(V1), V2))active(U12(tt, V2))mark(U13(isNat(V2)))
active(U13(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V1, V2))mark(U32(isNat(V1), V2))
active(U32(tt, V2))mark(U33(isNat(V2)))active(U33(tt))mark(tt)
active(U41(tt, N))mark(N)active(U51(tt, M, N))mark(s(plus(N, M)))
active(U61(tt))mark(0)active(U71(tt, M, N))mark(plus(x(N, M), N))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(plus(V1, V2)))mark(U11(and(isNatKind(V1), isNatKind(V2)), V1, V2))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNat(x(V1, V2)))mark(U31(and(isNatKind(V1), isNatKind(V2)), V1, V2))active(isNatKind(0))mark(tt)
active(isNatKind(plus(V1, V2)))mark(and(isNatKind(V1), isNatKind(V2)))active(isNatKind(s(V1)))mark(isNatKind(V1))
active(isNatKind(x(V1, V2)))mark(and(isNatKind(V1), isNatKind(V2)))active(plus(N, 0))mark(U41(and(isNat(N), isNatKind(N)), N))
active(plus(N, s(M)))mark(U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N))active(x(N, 0))mark(U61(and(isNat(N), isNatKind(N))))
active(x(N, s(M)))mark(U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N))mark(U11(X1, X2, X3))active(U11(mark(X1), X2, X3))
mark(tt)active(tt)mark(U12(X1, X2))active(U12(mark(X1), X2))
mark(isNat(X))active(isNat(X))mark(U13(X))active(U13(mark(X)))
mark(U21(X1, X2))active(U21(mark(X1), X2))mark(U22(X))active(U22(mark(X)))
mark(U31(X1, X2, X3))active(U31(mark(X1), X2, X3))mark(U32(X1, X2))active(U32(mark(X1), X2))
mark(U33(X))active(U33(mark(X)))mark(U41(X1, X2))active(U41(mark(X1), X2))
mark(U51(X1, X2, X3))active(U51(mark(X1), X2, X3))mark(s(X))active(s(mark(X)))
mark(plus(X1, X2))active(plus(mark(X1), mark(X2)))mark(U61(X))active(U61(mark(X)))
mark(0)active(0)mark(U71(X1, X2, X3))active(U71(mark(X1), X2, X3))
mark(x(X1, X2))active(x(mark(X1), mark(X2)))mark(and(X1, X2))active(and(mark(X1), X2))
mark(isNatKind(X))active(isNatKind(X))U11(mark(X1), X2, X3)U11(X1, X2, X3)
U11(X1, mark(X2), X3)U11(X1, X2, X3)U11(X1, X2, mark(X3))U11(X1, X2, X3)
U11(active(X1), X2, X3)U11(X1, X2, X3)U11(X1, active(X2), X3)U11(X1, X2, X3)
U11(X1, X2, active(X3))U11(X1, X2, X3)U12(mark(X1), X2)U12(X1, X2)
U12(X1, mark(X2))U12(X1, X2)U12(active(X1), X2)U12(X1, X2)
U12(X1, active(X2))U12(X1, X2)isNat(mark(X))isNat(X)
isNat(active(X))isNat(X)U13(mark(X))U13(X)
U13(active(X))U13(X)U21(mark(X1), X2)U21(X1, X2)
U21(X1, mark(X2))U21(X1, X2)U21(active(X1), X2)U21(X1, X2)
U21(X1, active(X2))U21(X1, X2)U22(mark(X))U22(X)
U22(active(X))U22(X)U31(mark(X1), X2, X3)U31(X1, X2, X3)
U31(X1, mark(X2), X3)U31(X1, X2, X3)U31(X1, X2, mark(X3))U31(X1, X2, X3)
U31(active(X1), X2, X3)U31(X1, X2, X3)U31(X1, active(X2), X3)U31(X1, X2, X3)
U31(X1, X2, active(X3))U31(X1, X2, X3)U32(mark(X1), X2)U32(X1, X2)
U32(X1, mark(X2))U32(X1, X2)U32(active(X1), X2)U32(X1, X2)
U32(X1, active(X2))U32(X1, X2)U33(mark(X))U33(X)
U33(active(X))U33(X)U41(mark(X1), X2)U41(X1, X2)
U41(X1, mark(X2))U41(X1, X2)U41(active(X1), X2)U41(X1, X2)
U41(X1, active(X2))U41(X1, X2)U51(mark(X1), X2, X3)U51(X1, X2, X3)
U51(X1, mark(X2), X3)U51(X1, X2, X3)U51(X1, X2, mark(X3))U51(X1, X2, X3)
U51(active(X1), X2, X3)U51(X1, X2, X3)U51(X1, active(X2), X3)U51(X1, X2, X3)
U51(X1, X2, active(X3))U51(X1, X2, X3)s(mark(X))s(X)
s(active(X))s(X)plus(mark(X1), X2)plus(X1, X2)
plus(X1, mark(X2))plus(X1, X2)plus(active(X1), X2)plus(X1, X2)
plus(X1, active(X2))plus(X1, X2)U61(mark(X))U61(X)
U61(active(X))U61(X)U71(mark(X1), X2, X3)U71(X1, X2, X3)
U71(X1, mark(X2), X3)U71(X1, X2, X3)U71(X1, X2, mark(X3))U71(X1, X2, X3)
U71(active(X1), X2, X3)U71(X1, X2, X3)U71(X1, active(X2), X3)U71(X1, X2, X3)
U71(X1, X2, active(X3))U71(X1, X2, X3)x(mark(X1), X2)x(X1, X2)
x(X1, mark(X2))x(X1, X2)x(active(X1), X2)x(X1, X2)
x(X1, active(X2))x(X1, X2)and(mark(X1), X2)and(X1, X2)
and(X1, mark(X2))and(X1, X2)and(active(X1), X2)and(X1, X2)
and(X1, active(X2))and(X1, X2)isNatKind(mark(X))isNatKind(X)
isNatKind(active(X))isNatKind(X)

Original Signature

Termination of terms over the following signature is verified: plus, isNatKind, mark, and, U71, isNat, U61, 0, U51, s, tt, U41, active, U11, U12, U13, U31, U32, U33, U21, x, U22