MAYBE

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

The following DP Processors were used

Problem 1 was processed with processor PolynomialLinearRange4iUR (0ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (0ms).
 |    | – Problem 3 remains open; application of the following processors failed [DependencyGraph (1ms), PolynomialLinearRange4iUR (404ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (21850ms), DependencyGraph (0ms), ReductionPairSAT (34532ms), DependencyGraph (1ms), SizeChangePrinciple (29ms)].

The following open problems remain:

Open Dependency Pair Problem 3

Dependency Pairs

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

→

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

Rewrite Rules

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

→

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

Original Signature

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

Problem 1: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

→

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

Original Signature

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

Strategy

Polynomial Interpretation

a(x): 0
b(x): 2
p(x,y): 2
p#(x,y): y

Improved Usable rules

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

→

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

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

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

→

p^#(x3, a(x2))

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

→

p^#(b(a(x1)), b(x0))

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

→

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

Rewrite Rules

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

→

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

Original Signature

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

Strategy

Polynomial Interpretation

a(x): 2
b(x): 0
p(x,y): 1
p#(x,y): 2x

Improved Usable rules

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

→

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

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

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

→

p^#(b(a(x1)), b(x0))