TIMEOUT

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

The following DP Processors were used


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

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Problem 1: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

Polynomial Interpretation

Improved Usable rules

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

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

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