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 (81ms), SubtermCriterion (2ms), DependencyGraph (42ms), PolynomialLinearRange4iUR (2636ms), DependencyGraph (41ms), PolynomialLinearRange8NegiUR (28020ms), DependencyGraph (32ms), ReductionPairSAT (1142ms), DependencyGraph (36ms), SizeChangePrinciple (timeout)].

The following open problems remain:



Open Dependency Pair Problem 1

Dependency Pairs

a__from#(X)mark#(X)a__2nd#(cons(X, X1))mark#(X1)
mark#(from(X))a__from#(mark(X))a__2nd#(cons(X, X1))mark#(X)
mark#(from(X))mark#(X)mark#(cons(X1, X2))mark#(X1)
a__2nd#(cons(X, X1))a__2nd#(cons1(mark(X), mark(X1)))mark#(cons1(X1, X2))mark#(X2)
mark#(cons1(X1, X2))mark#(X1)mark#(2nd(X))a__2nd#(mark(X))
a__2nd#(cons1(X, cons(Y, Z)))mark#(Y)mark#(s(X))mark#(X)
mark#(2nd(X))mark#(X)

Rewrite Rules

a__2nd(cons1(X, cons(Y, Z)))mark(Y)a__2nd(cons(X, X1))a__2nd(cons1(mark(X), mark(X1)))
a__from(X)cons(mark(X), from(s(X)))mark(2nd(X))a__2nd(mark(X))
mark(from(X))a__from(mark(X))mark(cons(X1, X2))cons(mark(X1), X2)
mark(s(X))s(mark(X))mark(cons1(X1, X2))cons1(mark(X1), mark(X2))
a__2nd(X)2nd(X)a__from(X)from(X)

Original Signature

Termination of terms over the following signature is verified: 2nd, cons1, s, mark, from, a__2nd, a__from, cons