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 (114ms), SubtermCriterion (1ms), DependencyGraph (72ms), PolynomialLinearRange4iUR (3296ms), DependencyGraph (73ms), PolynomialLinearRange8NegiUR (timeout), PolynomialLinearRange8NegiUR (-2ms), ReductionPairSAT (2207ms), DependencyGraph (60ms), SizeChangePrinciple (timeout)].

The following open problems remain:



Open Dependency Pair Problem 1

Dependency Pairs

a__sel#(0, cons(X, Y))mark#(X)mark#(g(X))mark#(X)
a__sel#(s(X), cons(Y, Z))mark#(Z)a__sel#(s(X), cons(Y, Z))a__sel#(mark(X), mark(Z))
mark#(cons(X1, X2))mark#(X1)mark#(f(X))a__f#(mark(X))
a__g#(s(X))mark#(X)mark#(f(X))mark#(X)
mark#(g(X))a__g#(mark(X))a__g#(s(X))a__g#(mark(X))
mark#(sel(X1, X2))a__sel#(mark(X1), mark(X2))mark#(sel(X1, X2))mark#(X2)
a__f#(X)mark#(X)mark#(s(X))mark#(X)
mark#(sel(X1, X2))mark#(X1)a__sel#(s(X), cons(Y, Z))mark#(X)

Rewrite Rules

a__f(X)cons(mark(X), f(g(X)))a__g(0)s(0)
a__g(s(X))s(s(a__g(mark(X))))a__sel(0, cons(X, Y))mark(X)
a__sel(s(X), cons(Y, Z))a__sel(mark(X), mark(Z))mark(f(X))a__f(mark(X))
mark(g(X))a__g(mark(X))mark(sel(X1, X2))a__sel(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__f(X)f(X)
a__g(X)g(X)a__sel(X1, X2)sel(X1, X2)

Original Signature

Termination of terms over the following signature is verified: f, g, 0, s, a__sel, mark, sel, a__g, a__f, cons