MAYBE

The TRS could not be proven terminating. The proof attempt took 1465 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 (1ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (135ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (621ms), DependencyGraph (1ms), ReductionPairSAT (441ms), DependencyGraph (1ms), SizeChangePrinciple (4ms)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

f#(n__a, X, X)f#(activate(X), b, n__b)

Rewrite Rules

f(n__a, X, X)f(activate(X), b, n__b)ba
an__abn__b
activate(n__a)aactivate(n__b)b
activate(X)X

Original Signature

Termination of terms over the following signature is verified: f, activate, n__b, b, n__a, a


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__a)a#f#(n__a, X, X)b#
activate#(n__b)b#f#(n__a, X, X)f#(activate(X), b, n__b)
f#(n__a, X, X)activate#(X)b#a#

Rewrite Rules

f(n__a, X, X)f(activate(X), b, n__b)ba
an__abn__b
activate(n__a)aactivate(n__b)b
activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, f, n__b, b, n__a, a

Strategy


The following SCCs where found

f#(n__a, X, X) → f#(activate(X), b, n__b)