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 (204ms), SubtermCriterion (0ms), DependencyGraph (167ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (129ms), PolynomialLinearRange8NegiUR (30000ms), ReductionPairSAT (5601ms), DependencyGraph (152ms), SizeChangePrinciple (timeout)].

The following open problems remain:



Open Dependency Pair Problem 1

Dependency Pairs

mark#(diff(X1, X2))mark#(X1)mark#(leq(X1, X2))mark#(X1)
mark#(if(X1, X2, X3))a__if#(mark(X1), X2, X3)mark#(p(X))a__p#(mark(X))
mark#(leq(X1, X2))mark#(X2)a__if#(true, X, Y)mark#(X)
mark#(diff(X1, X2))mark#(X2)a__diff#(X, Y)mark#(Y)
mark#(diff(X1, X2))a__diff#(mark(X1), mark(X2))a__leq#(s(X), s(Y))mark#(X)
mark#(p(X))mark#(X)a__if#(false, X, Y)mark#(Y)
mark#(leq(X1, X2))a__leq#(mark(X1), mark(X2))mark#(if(X1, X2, X3))mark#(X1)
a__diff#(X, Y)mark#(X)mark#(s(X))mark#(X)
a__leq#(s(X), s(Y))mark#(Y)a__diff#(X, Y)a__leq#(mark(X), mark(Y))
a__p#(s(X))mark#(X)a__leq#(s(X), s(Y))a__leq#(mark(X), mark(Y))
a__diff#(X, Y)a__if#(a__leq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))

Rewrite Rules

a__p(0)0a__p(s(X))mark(X)
a__leq(0, Y)truea__leq(s(X), 0)false
a__leq(s(X), s(Y))a__leq(mark(X), mark(Y))a__if(true, X, Y)mark(X)
a__if(false, X, Y)mark(Y)a__diff(X, Y)a__if(a__leq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
mark(p(X))a__p(mark(X))mark(leq(X1, X2))a__leq(mark(X1), mark(X2))
mark(if(X1, X2, X3))a__if(mark(X1), X2, X3)mark(diff(X1, X2))a__diff(mark(X1), mark(X2))
mark(0)0mark(s(X))s(mark(X))
mark(true)truemark(false)false
a__p(X)p(X)a__leq(X1, X2)leq(X1, X2)
a__if(X1, X2, X3)if(X1, X2, X3)a__diff(X1, X2)diff(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__p, diff, leq, true, mark, a__diff, 0, s, a__leq, a__if, if, p, false