MAYBE

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (3ms), PolynomialLinearRange4 (147ms), DependencyGraph (1ms), ReductionPairSAT (104ms), DependencyGraph (1ms), SizeChangePrinciple (15ms)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

U21#(x, x)g#(a)g#(x)U21#(f(x), x)

Rewrite Rules

abf(a)b
g(x)U21(f(x), x)U21(x, x)g(a)

Original Signature

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


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

U21#(x, x)g#(a)g#(x)f#(x)
g#(x)U21#(f(x), x)U21#(x, x)a#

Rewrite Rules

abf(a)b
g(x)U21(f(x), x)U21(x, x)g(a)

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(b) = μ(a) = μ(a#) = ∅
μ(f) = μ(g) = μ(f#) = μ(U21#) = μ(g#) = μ(U21) = {1}


The following SCCs where found

U21#(x, x) → g#(a)g#(x) → U21#(f(x), x)