TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (20ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (529ms).
 |    | – Problem 3 remains open; application of the following processors failed [DependencyGraph (1ms), PolynomialLinearRange4iUR (347ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (4175ms), DependencyGraph (2ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 3

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

The following SCCs where found

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

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

Polynomial Interpretation

Improved Usable rules

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

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

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