TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60000 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

mark#(U32(X))U32#(mark(X))U62#(X1, mark(X2), X3)U62#(X1, X2, X3)
mark#(U51(X1, X2))U51#(mark(X1), X2)U15#(X1, active(X2))U15#(X1, X2)
mark#(U11(X1, X2, X3))U11#(mark(X1), X2, X3)active#(U15(tt, V2))U16#(isNat(V2))
U61#(X1, active(X2), X3)U61#(X1, X2, X3)mark#(U41(X))U41#(mark(X))
U61#(X1, X2, mark(X3))U61#(X1, X2, X3)U52#(X1, active(X2))U52#(X1, X2)
U51#(mark(X1), X2)U51#(X1, X2)mark#(U12(X1, X2, X3))active#(U12(mark(X1), X2, X3))
isNat#(active(X))isNat#(X)U21#(X1, active(X2))U21#(X1, X2)
mark#(s(X))mark#(X)active#(U51(tt, N))mark#(U52(isNatKind(N), N))
mark#(U13(X1, X2, X3))mark#(X1)mark#(plus(X1, X2))active#(plus(mark(X1), mark(X2)))
active#(U31(tt, V2))U32#(isNatKind(V2))U62#(X1, X2, active(X3))U62#(X1, X2, X3)
U14#(X1, mark(X2), X3)U14#(X1, X2, X3)active#(U21(tt, V1))isNatKind#(V1)
U63#(X1, X2, active(X3))U63#(X1, X2, X3)active#(U61(tt, M, N))mark#(U62(isNatKind(M), M, N))
U12#(X1, active(X2), X3)U12#(X1, X2, X3)U12#(X1, X2, mark(X3))U12#(X1, X2, X3)
mark#(U41(X))mark#(X)mark#(U11(X1, X2, X3))mark#(X1)
active#(U15(tt, V2))mark#(U16(isNat(V2)))active#(U15(tt, V2))isNat#(V2)
U61#(active(X1), X2, X3)U61#(X1, X2, X3)active#(isNatKind(s(V1)))U41#(isNatKind(V1))
mark#(U32(X))mark#(X)U14#(X1, active(X2), X3)U14#(X1, X2, X3)
U32#(mark(X))U32#(X)U15#(X1, mark(X2))U15#(X1, X2)
U14#(mark(X1), X2, X3)U14#(X1, X2, X3)mark#(U16(X))mark#(X)
U63#(X1, X2, mark(X3))U63#(X1, X2, X3)active#(U12(tt, V1, V2))U13#(isNatKind(V2), V1, V2)
U64#(X1, mark(X2), X3)U64#(X1, X2, X3)mark#(U22(X1, X2))mark#(X1)
mark#(U21(X1, X2))active#(U21(mark(X1), X2))U11#(active(X1), X2, X3)U11#(X1, X2, X3)
mark#(U14(X1, X2, X3))active#(U14(mark(X1), X2, X3))U61#(mark(X1), X2, X3)U61#(X1, X2, X3)
mark#(isNatKind(X))isNatKind#(X)active#(U31(tt, V2))mark#(U32(isNatKind(V2)))
isNatKind#(mark(X))isNatKind#(X)U52#(X1, mark(X2))U52#(X1, X2)
U12#(X1, X2, active(X3))U12#(X1, X2, X3)U15#(mark(X1), X2)U15#(X1, X2)
mark#(U61(X1, X2, X3))U61#(mark(X1), X2, X3)U21#(active(X1), X2)U21#(X1, X2)
U64#(X1, X2, active(X3))U64#(X1, X2, X3)mark#(U63(X1, X2, X3))U63#(mark(X1), X2, X3)
U16#(active(X))U16#(X)U51#(X1, mark(X2))U51#(X1, X2)
active#(isNat(s(V1)))U21#(isNatKind(V1), V1)active#(plus(N, 0))mark#(U51(isNat(N), N))
U52#(mark(X1), X2)U52#(X1, X2)mark#(U64(X1, X2, X3))U64#(mark(X1), X2, X3)
U63#(X1, active(X2), X3)U63#(X1, X2, X3)mark#(U52(X1, X2))U52#(mark(X1), X2)
active#(isNat(plus(V1, V2)))U11#(isNatKind(V1), V1, V2)mark#(s(X))s#(mark(X))
active#(U21(tt, V1))U22#(isNatKind(V1), V1)mark#(U11(X1, X2, X3))active#(U11(mark(X1), X2, X3))
active#(U12(tt, V1, V2))mark#(U13(isNatKind(V2), V1, V2))U41#(active(X))U41#(X)
U16#(mark(X))U16#(X)U64#(active(X1), X2, X3)U64#(X1, X2, X3)
U13#(X1, active(X2), X3)U13#(X1, X2, X3)active#(isNat(0))mark#(tt)
U11#(mark(X1), X2, X3)U11#(X1, X2, X3)active#(U61(tt, M, N))U62#(isNatKind(M), M, N)
mark#(U15(X1, X2))U15#(mark(X1), X2)active#(U22(tt, V1))U23#(isNat(V1))
mark#(plus(X1, X2))mark#(X1)isNatKind#(active(X))isNatKind#(X)
active#(U64(tt, M, N))mark#(s(plus(N, M)))U13#(X1, X2, mark(X3))U13#(X1, X2, X3)
U12#(X1, mark(X2), X3)U12#(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#(U12(tt, V1, V2))isNatKind#(V2)
active#(isNat(plus(V1, V2)))isNatKind#(V1)U11#(X1, X2, mark(X3))U11#(X1, X2, X3)
U14#(active(X1), X2, X3)U14#(X1, X2, X3)U23#(active(X))U23#(X)
U64#(X1, active(X2), X3)U64#(X1, X2, X3)mark#(U12(X1, X2, X3))mark#(X1)
mark#(U22(X1, X2))active#(U22(mark(X1), X2))active#(U63(tt, M, N))isNatKind#(N)
mark#(U62(X1, X2, X3))active#(U62(mark(X1), X2, X3))mark#(U64(X1, X2, X3))active#(U64(mark(X1), X2, X3))
active#(isNat(s(V1)))mark#(U21(isNatKind(V1), V1))mark#(plus(X1, X2))plus#(mark(X1), mark(X2))
U64#(mark(X1), X2, X3)U64#(X1, X2, X3)mark#(U13(X1, X2, X3))U13#(mark(X1), X2, X3)
s#(mark(X))s#(X)mark#(U31(X1, X2))U31#(mark(X1), X2)
mark#(U32(X))active#(U32(mark(X)))active#(isNatKind(0))mark#(tt)
U63#(mark(X1), X2, X3)U63#(X1, X2, X3)active#(isNatKind(plus(V1, V2)))isNatKind#(V1)
active#(U13(tt, V1, V2))U14#(isNatKind(V2), V1, V2)active#(U62(tt, M, N))isNat#(N)
mark#(U22(X1, X2))U22#(mark(X1), X2)active#(U11(tt, V1, V2))mark#(U12(isNatKind(V1), V1, V2))
active#(plus(N, 0))isNat#(N)active#(U22(tt, V1))isNat#(V1)
active#(isNatKind(plus(V1, V2)))mark#(U31(isNatKind(V1), V2))U22#(active(X1), X2)U22#(X1, X2)
U11#(X1, active(X2), X3)U11#(X1, X2, X3)U12#(mark(X1), X2, X3)U12#(X1, X2, X3)
active#(U41(tt))mark#(tt)mark#(U13(X1, X2, X3))active#(U13(mark(X1), X2, X3))
mark#(U51(X1, X2))active#(U51(mark(X1), X2))active#(U51(tt, N))U52#(isNatKind(N), N)
active#(U61(tt, M, N))isNatKind#(M)active#(U22(tt, V1))mark#(U23(isNat(V1)))
active#(isNatKind(s(V1)))mark#(U41(isNatKind(V1)))mark#(U15(X1, X2))mark#(X1)
active#(isNat(s(V1)))isNatKind#(V1)active#(U11(tt, V1, V2))isNatKind#(V1)
active#(U63(tt, M, N))U64#(isNatKind(N), M, N)active#(U14(tt, V1, V2))U15#(isNat(V1), V2)
U13#(X1, X2, active(X3))U13#(X1, X2, X3)U63#(X1, mark(X2), X3)U63#(X1, X2, X3)
U64#(X1, X2, mark(X3))U64#(X1, X2, X3)plus#(mark(X1), X2)plus#(X1, X2)
U13#(mark(X1), X2, X3)U13#(X1, X2, X3)plus#(active(X1), X2)plus#(X1, X2)
U51#(X1, active(X2))U51#(X1, X2)U22#(mark(X1), X2)U22#(X1, X2)
mark#(tt)active#(tt)active#(U52(tt, N))mark#(N)
U31#(X1, active(X2))U31#(X1, X2)mark#(U23(X))active#(U23(mark(X)))
U63#(active(X1), X2, X3)U63#(X1, X2, X3)mark#(U14(X1, X2, X3))mark#(X1)
U22#(X1, active(X2))U22#(X1, X2)U62#(X1, X2, mark(X3))U62#(X1, X2, X3)
U21#(X1, mark(X2))U21#(X1, X2)mark#(U23(X))mark#(X)
active#(plus(N, 0))U51#(isNat(N), N)U12#(active(X1), X2, X3)U12#(X1, X2, X3)
active#(U64(tt, M, N))s#(plus(N, M))U62#(mark(X1), X2, X3)U62#(X1, X2, X3)
mark#(U31(X1, X2))active#(U31(mark(X1), X2))active#(U21(tt, V1))mark#(U22(isNatKind(V1), V1))
U13#(X1, mark(X2), X3)U13#(X1, X2, X3)mark#(0)active#(0)
mark#(s(X))active#(s(mark(X)))U52#(active(X1), X2)U52#(X1, X2)
mark#(U14(X1, X2, X3))U14#(mark(X1), X2, X3)active#(U62(tt, M, N))U63#(isNat(N), M, N)
mark#(U12(X1, X2, X3))U12#(mark(X1), X2, X3)active#(plus(N, s(M)))isNat#(M)
active#(U16(tt))mark#(tt)U11#(X1, X2, active(X3))U11#(X1, X2, X3)
mark#(U15(X1, X2))active#(U15(mark(X1), X2))mark#(isNatKind(X))active#(isNatKind(X))
active#(isNatKind(plus(V1, V2)))U31#(isNatKind(V1), V2)active#(U63(tt, M, N))mark#(U64(isNatKind(N), M, N))
active#(isNat(plus(V1, V2)))mark#(U11(isNatKind(V1), V1, V2))mark#(U63(X1, X2, X3))active#(U63(mark(X1), X2, X3))
U23#(mark(X))U23#(X)U41#(mark(X))U41#(X)
active#(U31(tt, V2))isNatKind#(V2)active#(plus(N, s(M)))U61#(isNat(M), M, N)
active#(U13(tt, V1, V2))isNatKind#(V2)plus#(X1, mark(X2))plus#(X1, X2)
U31#(active(X1), X2)U31#(X1, X2)U62#(active(X1), X2, X3)U62#(X1, X2, X3)
mark#(U31(X1, X2))mark#(X1)U62#(X1, active(X2), X3)U62#(X1, X2, X3)
mark#(U23(X))U23#(mark(X))active#(U32(tt))mark#(tt)
U14#(X1, X2, active(X3))U14#(X1, X2, X3)U61#(X1, mark(X2), X3)U61#(X1, X2, X3)
U15#(active(X1), X2)U15#(X1, X2)active#(U51(tt, N))isNatKind#(N)
active#(U64(tt, M, N))plus#(N, M)U13#(active(X1), X2, X3)U13#(X1, X2, X3)
plus#(X1, active(X2))plus#(X1, X2)mark#(U63(X1, X2, X3))mark#(X1)
mark#(U52(X1, X2))active#(U52(mark(X1), X2))mark#(isNat(X))active#(isNat(X))
mark#(U16(X))U16#(mark(X))active#(U14(tt, V1, V2))mark#(U15(isNat(V1), V2))
mark#(U61(X1, X2, X3))active#(U61(mark(X1), X2, X3))mark#(U61(X1, X2, X3))mark#(X1)
U22#(X1, mark(X2))U22#(X1, X2)U51#(active(X1), X2)U51#(X1, X2)
mark#(U16(X))active#(U16(mark(X)))mark#(U51(X1, X2))mark#(X1)
U31#(X1, mark(X2))U31#(X1, X2)mark#(U62(X1, X2, X3))mark#(X1)
active#(U13(tt, V1, V2))mark#(U14(isNatKind(V2), V1, V2))mark#(plus(X1, X2))mark#(X2)
active#(plus(N, s(M)))mark#(U61(isNat(M), M, N))U14#(X1, X2, mark(X3))U14#(X1, X2, X3)
active#(U14(tt, V1, V2))isNat#(V1)active#(isNatKind(s(V1)))isNatKind#(V1)
U32#(active(X))U32#(X)mark#(U52(X1, X2))mark#(X1)
active#(U11(tt, V1, V2))U12#(isNatKind(V1), V1, V2)active#(U62(tt, M, N))mark#(U63(isNat(N), M, N))
U31#(mark(X1), X2)U31#(X1, X2)active#(U23(tt))mark#(tt)
U61#(X1, X2, active(X3))U61#(X1, X2, X3)U21#(mark(X1), X2)U21#(X1, X2)
U11#(X1, mark(X2), X3)U11#(X1, X2, X3)s#(active(X))s#(X)
mark#(U41(X))active#(U41(mark(X)))mark#(U64(X1, X2, X3))mark#(X1)
mark#(U62(X1, X2, X3))U62#(mark(X1), X2, X3)

Rewrite Rules

active(U11(tt, V1, V2))mark(U12(isNatKind(V1), V1, V2))active(U12(tt, V1, V2))mark(U13(isNatKind(V2), V1, V2))
active(U13(tt, V1, V2))mark(U14(isNatKind(V2), V1, V2))active(U14(tt, V1, V2))mark(U15(isNat(V1), V2))
active(U15(tt, V2))mark(U16(isNat(V2)))active(U16(tt))mark(tt)
active(U21(tt, V1))mark(U22(isNatKind(V1), V1))active(U22(tt, V1))mark(U23(isNat(V1)))
active(U23(tt))mark(tt)active(U31(tt, V2))mark(U32(isNatKind(V2)))
active(U32(tt))mark(tt)active(U41(tt))mark(tt)
active(U51(tt, N))mark(U52(isNatKind(N), N))active(U52(tt, N))mark(N)
active(U61(tt, M, N))mark(U62(isNatKind(M), M, N))active(U62(tt, M, N))mark(U63(isNat(N), M, N))
active(U63(tt, M, N))mark(U64(isNatKind(N), M, N))active(U64(tt, M, N))mark(s(plus(N, M)))
active(isNat(0))mark(tt)active(isNat(plus(V1, V2)))mark(U11(isNatKind(V1), V1, V2))
active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))active(isNatKind(0))mark(tt)
active(isNatKind(plus(V1, V2)))mark(U31(isNatKind(V1), V2))active(isNatKind(s(V1)))mark(U41(isNatKind(V1)))
active(plus(N, 0))mark(U51(isNat(N), N))active(plus(N, s(M)))mark(U61(isNat(M), M, N))
mark(U11(X1, X2, X3))active(U11(mark(X1), X2, X3))mark(tt)active(tt)
mark(U12(X1, X2, X3))active(U12(mark(X1), X2, X3))mark(isNatKind(X))active(isNatKind(X))
mark(U13(X1, X2, X3))active(U13(mark(X1), X2, X3))mark(U14(X1, X2, X3))active(U14(mark(X1), X2, X3))
mark(U15(X1, X2))active(U15(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(U16(X))active(U16(mark(X)))mark(U21(X1, X2))active(U21(mark(X1), X2))
mark(U22(X1, X2))active(U22(mark(X1), X2))mark(U23(X))active(U23(mark(X)))
mark(U31(X1, X2))active(U31(mark(X1), X2))mark(U32(X))active(U32(mark(X)))
mark(U41(X))active(U41(mark(X)))mark(U51(X1, X2))active(U51(mark(X1), X2))
mark(U52(X1, X2))active(U52(mark(X1), X2))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2, X3))active(U62(mark(X1), X2, X3))mark(U63(X1, X2, X3))active(U63(mark(X1), X2, X3))
mark(U64(X1, X2, X3))active(U64(mark(X1), X2, X3))mark(s(X))active(s(mark(X)))
mark(plus(X1, X2))active(plus(mark(X1), mark(X2)))mark(0)active(0)
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, X3)U12(X1, X2, X3)U12(X1, mark(X2), X3)U12(X1, X2, X3)
U12(X1, X2, mark(X3))U12(X1, X2, X3)U12(active(X1), X2, X3)U12(X1, X2, X3)
U12(X1, active(X2), X3)U12(X1, X2, X3)U12(X1, X2, active(X3))U12(X1, X2, X3)
isNatKind(mark(X))isNatKind(X)isNatKind(active(X))isNatKind(X)
U13(mark(X1), X2, X3)U13(X1, X2, X3)U13(X1, mark(X2), X3)U13(X1, X2, X3)
U13(X1, X2, mark(X3))U13(X1, X2, X3)U13(active(X1), X2, X3)U13(X1, X2, X3)
U13(X1, active(X2), X3)U13(X1, X2, X3)U13(X1, X2, active(X3))U13(X1, X2, X3)
U14(mark(X1), X2, X3)U14(X1, X2, X3)U14(X1, mark(X2), X3)U14(X1, X2, X3)
U14(X1, X2, mark(X3))U14(X1, X2, X3)U14(active(X1), X2, X3)U14(X1, X2, X3)
U14(X1, active(X2), X3)U14(X1, X2, X3)U14(X1, X2, active(X3))U14(X1, X2, X3)
U15(mark(X1), X2)U15(X1, X2)U15(X1, mark(X2))U15(X1, X2)
U15(active(X1), X2)U15(X1, X2)U15(X1, active(X2))U15(X1, X2)
isNat(mark(X))isNat(X)isNat(active(X))isNat(X)
U16(mark(X))U16(X)U16(active(X))U16(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(X1), X2)U22(X1, X2)U22(X1, mark(X2))U22(X1, X2)
U22(active(X1), X2)U22(X1, X2)U22(X1, active(X2))U22(X1, X2)
U23(mark(X))U23(X)U23(active(X))U23(X)
U31(mark(X1), X2)U31(X1, X2)U31(X1, mark(X2))U31(X1, X2)
U31(active(X1), X2)U31(X1, X2)U31(X1, active(X2))U31(X1, X2)
U32(mark(X))U32(X)U32(active(X))U32(X)
U41(mark(X))U41(X)U41(active(X))U41(X)
U51(mark(X1), X2)U51(X1, X2)U51(X1, mark(X2))U51(X1, X2)
U51(active(X1), X2)U51(X1, X2)U51(X1, active(X2))U51(X1, X2)
U52(mark(X1), X2)U52(X1, X2)U52(X1, mark(X2))U52(X1, X2)
U52(active(X1), X2)U52(X1, X2)U52(X1, active(X2))U52(X1, X2)
U61(mark(X1), X2, X3)U61(X1, X2, X3)U61(X1, mark(X2), X3)U61(X1, X2, X3)
U61(X1, X2, mark(X3))U61(X1, X2, X3)U61(active(X1), X2, X3)U61(X1, X2, X3)
U61(X1, active(X2), X3)U61(X1, X2, X3)U61(X1, X2, active(X3))U61(X1, X2, X3)
U62(mark(X1), X2, X3)U62(X1, X2, X3)U62(X1, mark(X2), X3)U62(X1, X2, X3)
U62(X1, X2, mark(X3))U62(X1, X2, X3)U62(active(X1), X2, X3)U62(X1, X2, X3)
U62(X1, active(X2), X3)U62(X1, X2, X3)U62(X1, X2, active(X3))U62(X1, X2, X3)
U63(mark(X1), X2, X3)U63(X1, X2, X3)U63(X1, mark(X2), X3)U63(X1, X2, X3)
U63(X1, X2, mark(X3))U63(X1, X2, X3)U63(active(X1), X2, X3)U63(X1, X2, X3)
U63(X1, active(X2), X3)U63(X1, X2, X3)U63(X1, X2, active(X3))U63(X1, X2, X3)
U64(mark(X1), X2, X3)U64(X1, X2, X3)U64(X1, mark(X2), X3)U64(X1, X2, X3)
U64(X1, X2, mark(X3))U64(X1, X2, X3)U64(active(X1), X2, X3)U64(X1, X2, X3)
U64(X1, active(X2), X3)U64(X1, X2, X3)U64(X1, X2, active(X3))U64(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)

Original Signature

Termination of terms over the following signature is verified: isNat, U64, U63, U62, U61, U41, U23, U21, U22, plus, isNatKind, mark, 0, U14, U51, s, U15, tt, U16, U52, U11, active, U12, U13, U31, U32