MAYBE

The TRS could not be proven terminating. The proof attempt took 550 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 (5ms), PolynomialLinearRange4iUR (90ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (264ms), DependencyGraph (2ms), ReductionPairSAT (37ms), DependencyGraph (2ms), SizeChangePrinciple (3ms)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

c#f#(n__g(n__c))f#(n__g(X))activate#(X)
activate#(n__c)c#

Rewrite Rules

cf(n__g(n__c))f(n__g(X))g(activate(X))
g(X)n__g(X)cn__c
activate(n__g(X))g(X)activate(n__c)c
activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, f, g, n__c, c, n__g


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

c#f#(n__g(n__c))f#(n__g(X))g#(activate(X))
f#(n__g(X))activate#(X)activate#(n__g(X))g#(X)
activate#(n__c)c#

Rewrite Rules

cf(n__g(n__c))f(n__g(X))g(activate(X))
g(X)n__g(X)cn__c
activate(n__g(X))g(X)activate(n__c)c
activate(X)X

Original Signature

Termination of terms over the following signature is verified: f, activate, g, n__c, c, n__g

Strategy


The following SCCs where found

c# → f#(n__g(n__c))f#(n__g(X)) → activate#(X)
activate#(n__c) → c#