MAYBE

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

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (0ms).
 | – Problem 2 remains open; application of the following processors failed [DependencyGraph (1ms), PolynomialLinearRange4iUR (196ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (1592ms), DependencyGraph (1ms), ReductionPairSAT (9040ms), DependencyGraph (0ms), SizeChangePrinciple (51ms)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

p#(a(x0), p(x1, p(x2, x3))) → p#(x1, p(x0, p(a(x3), x3)))

Rewrite Rules

p(a(x0), p(x1, p(x2, x3))) → p(x1, p(x0, p(a(x3), x3)))

Original Signature

Termination of terms over the following signature is verified: p, a

Problem 1: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

p#(a(x0), p(x1, p(x2, x3))) → p#(a(x3), x3)p#(a(x0), p(x1, p(x2, x3))) → p#(x0, p(a(x3), x3))
p#(a(x0), p(x1, p(x2, x3))) → p#(x1, p(x0, p(a(x3), x3)))

Rewrite Rules

p(a(x0), p(x1, p(x2, x3))) → p(x1, p(x0, p(a(x3), x3)))

Original Signature

Termination of terms over the following signature is verified: p, a

Strategy

Polynomial Interpretation

Improved Usable rules

p(a(x0), p(x1, p(x2, x3))) → p(x1, p(x0, p(a(x3), x3)))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

p#(a(x0), p(x1, p(x2, x3))) → p#(a(x3), x3)p#(a(x0), p(x1, p(x2, x3))) → p#(x0, p(a(x3), x3))