TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor ReductionPairSAT (16981ms).
 | – Problem 2 remains open; application of the following processors failed [DependencyGraph (265ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

a__U22#(tt, M, N) → a__plus#(a__x(mark(N), mark(M)), mark(N))mark#(x(X1, X2)) → a__x#(mark(X1), mark(X2))
a__U21#(tt, M, N) → a__U22#(tt, M, N)mark#(U22(X1, X2, X3)) → a__U22#(mark(X1), X2, X3)
a__U12#(tt, M, N) → mark#(M)mark#(plus(X1, X2)) → mark#(X2)
mark#(U12(X1, X2, X3)) → a__U12#(mark(X1), X2, X3)a__U12#(tt, M, N) → mark#(N)
a__x#(N, s(M)) → a__U21#(tt, M, N)mark#(s(X)) → mark#(X)
mark#(U12(X1, X2, X3)) → mark#(X1)a__U22#(tt, M, N) → mark#(N)
a__U22#(tt, M, N) → mark#(M)mark#(plus(X1, X2)) → a__plus#(mark(X1), mark(X2))
mark#(U21(X1, X2, X3)) → a__U21#(mark(X1), X2, X3)a__plus#(N, s(M)) → a__U11#(tt, M, N)
mark#(U22(X1, X2, X3)) → mark#(X1)mark#(plus(X1, X2)) → mark#(X1)
a__U11#(tt, M, N) → a__U12#(tt, M, N)mark#(x(X1, X2)) → mark#(X2)
mark#(U21(X1, X2, X3)) → mark#(X1)a__plus#(N, 0) → mark#(N)
mark#(U11(X1, X2, X3)) → a__U11#(mark(X1), X2, X3)mark#(x(X1, X2)) → mark#(X1)
mark#(U11(X1, X2, X3)) → mark#(X1)a__U12#(tt, M, N) → a__plus#(mark(N), mark(M))

Rewrite Rules

a__U11(tt, M, N) → a__U12(tt, M, N)a__U12(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__U21(tt, M, N) → a__U22(tt, M, N)a__U22(tt, M, N) → a__plus(a__x(mark(N), mark(M)), mark(N))
a__plus(N, 0) → mark(N)a__plus(N, s(M)) → a__U11(tt, M, N)
a__x(N, 0) → 0a__x(N, s(M)) → a__U21(tt, M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(U21(X1, X2, X3)) → a__U21(mark(X1), X2, X3)
mark(U22(X1, X2, X3)) → a__U22(mark(X1), X2, X3)mark(x(X1, X2)) → a__x(mark(X1), mark(X2))
mark(tt) → ttmark(s(X)) → s(mark(X))
mark(0) → 0a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__U12(X1, X2, X3) → U12(X1, X2, X3)a__plus(X1, X2) → plus(X1, X2)
a__U21(X1, X2, X3) → U21(X1, X2, X3)a__U22(X1, X2, X3) → U22(X1, X2, X3)
a__x(X1, X2) → x(X1, X2)

Original Signature

Termination of terms over the following signature is verified: plus, a__plus, mark, 0, s, tt, a__U22, U11, a__U12, U12, a__U11, a__x, a__U21, U21, U22, x

Problem 1: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

a__U22#(tt, M, N) → a__plus#(a__x(mark(N), mark(M)), mark(N))mark#(x(X1, X2)) → a__x#(mark(X1), mark(X2))
a__U22#(tt, M, N) → a__x#(mark(N), mark(M))a__U21#(tt, M, N) → a__U22#(tt, M, N)
mark#(U22(X1, X2, X3)) → a__U22#(mark(X1), X2, X3)a__U12#(tt, M, N) → mark#(M)
mark#(plus(X1, X2)) → mark#(X2)mark#(U12(X1, X2, X3)) → a__U12#(mark(X1), X2, X3)
a__U12#(tt, M, N) → mark#(N)a__x#(N, s(M)) → a__U21#(tt, M, N)
mark#(s(X)) → mark#(X)mark#(U12(X1, X2, X3)) → mark#(X1)
a__U22#(tt, M, N) → mark#(N)a__U22#(tt, M, N) → mark#(M)
mark#(plus(X1, X2)) → a__plus#(mark(X1), mark(X2))mark#(U21(X1, X2, X3)) → a__U21#(mark(X1), X2, X3)
a__plus#(N, s(M)) → a__U11#(tt, M, N)mark#(U22(X1, X2, X3)) → mark#(X1)
mark#(plus(X1, X2)) → mark#(X1)a__U11#(tt, M, N) → a__U12#(tt, M, N)
mark#(x(X1, X2)) → mark#(X2)mark#(U21(X1, X2, X3)) → mark#(X1)
a__plus#(N, 0) → mark#(N)mark#(U11(X1, X2, X3)) → a__U11#(mark(X1), X2, X3)
mark#(x(X1, X2)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)
a__U12#(tt, M, N) → a__plus#(mark(N), mark(M))

Rewrite Rules

a__U11(tt, M, N) → a__U12(tt, M, N)a__U12(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__U21(tt, M, N) → a__U22(tt, M, N)a__U22(tt, M, N) → a__plus(a__x(mark(N), mark(M)), mark(N))
a__plus(N, 0) → mark(N)a__plus(N, s(M)) → a__U11(tt, M, N)
a__x(N, 0) → 0a__x(N, s(M)) → a__U21(tt, M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(U21(X1, X2, X3)) → a__U21(mark(X1), X2, X3)
mark(U22(X1, X2, X3)) → a__U22(mark(X1), X2, X3)mark(x(X1, X2)) → a__x(mark(X1), mark(X2))
mark(tt) → ttmark(s(X)) → s(mark(X))
mark(0) → 0a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__U12(X1, X2, X3) → U12(X1, X2, X3)a__plus(X1, X2) → plus(X1, X2)
a__U21(X1, X2, X3) → U21(X1, X2, X3)a__U22(X1, X2, X3) → U22(X1, X2, X3)
a__x(X1, X2) → x(X1, X2)

Original Signature

Termination of terms over the following signature is verified: plus, a__plus, mark, 0, s, tt, a__U22, U11, a__U12, U12, a__U11, a__x, a__U21, U21, U22, x

Strategy

Function Precedence

mark < a__U22# = a__x# = a__U21# = a__U22 = a__x = a__U21 = U21 = x = U22 < plus = a__plus = a__U11# = a__U12# = a__plus# = U11 = a__U12 = U12 = a__U11 < mark# = 0 = s = tt

Argument Filtering

plus: 1 2
a__U22#: 1 2 3
a__x#: 1 2
a__plus: 1 2
mark: collapses to 1
mark#: collapses to 1
a__U11#: 1 2 3
0: all arguments are removed from 0
a__U12#: 1 2 3
s: 1
tt: all arguments are removed from tt
a__plus#: 1 2
a__U21#: 1 2 3
U11: 1 2 3
a__U22: 1 2 3
a__U12: 1 2 3
U12: 1 2 3
a__U11: 1 2 3
a__x: 1 2
a__U21: 1 2 3
U21: 1 2 3
x: 1 2
U22: 1 2 3

Status

plus: multiset
a__U22#: multiset
a__x#: multiset
a__plus: multiset
a__U11#: multiset
0: multiset
a__U12#: multiset
s: multiset
tt: multiset
a__plus#: multiset
a__U21#: multiset
U11: multiset
a__U22: multiset
a__U12: multiset
U12: multiset
a__U11: multiset
a__x: multiset
a__U21: multiset
U21: multiset
x: multiset
U22: multiset

Usable Rules

a__U11(X1, X2, X3) → U11(X1, X2, X3)a__x(N, s(M)) → a__U21(tt, M, N)
mark(tt) → tta__plus(N, 0) → mark(N)
mark(0) → 0a__plus(X1, X2) → plus(X1, X2)
mark(U22(X1, X2, X3)) → a__U22(mark(X1), X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)a__U21(tt, M, N) → a__U22(tt, M, N)
a__plus(N, s(M)) → a__U11(tt, M, N)a__x(X1, X2) → x(X1, X2)
a__U11(tt, M, N) → a__U12(tt, M, N)a__U21(X1, X2, X3) → U21(X1, X2, X3)
a__U12(tt, M, N) → s(a__plus(mark(N), mark(M)))mark(s(X)) → s(mark(X))
a__U22(X1, X2, X3) → U22(X1, X2, X3)mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
a__x(N, 0) → 0mark(U21(X1, X2, X3)) → a__U21(mark(X1), X2, X3)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)a__U22(tt, M, N) → a__plus(a__x(mark(N), mark(M)), mark(N))
mark(x(X1, X2)) → a__x(mark(X1), mark(X2))

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

a__U22#(tt, M, N) → a__x#(mark(N), mark(M))