The TRS could be proven non-terminating. The proof took 616 ms.

The following reduction sequence is a witness for non-termination:

g#(n__c) →* g#(n__c)

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor ForwardNarrowing (4ms).
 |    | – Problem 3 was processed with processor ForwardNarrowing (3ms).
 |    |    | – Problem 4 was processed with processor ForwardNarrowing (2ms).
 |    |    |    | – Problem 5 was processed with processor ForwardNarrowing (1ms).
 |    |    |    |    | – Problem 6 was processed with processor ForwardNarrowing (1ms).
 |    |    |    |    |    | – Problem 7 was processed with processor BackwardInstantiation (3ms).
 |    |    |    |    |    |    | – Problem 8 was processed with processor Propagation (3ms).
 |    |    |    |    |    |    |    | – Problem 9 was processed with processor ForwardNarrowing (1ms).
 |    |    |    |    |    |    |    |    | – Problem 10 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (4ms), ForwardInstantiation (2ms), Propagation (9ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (3ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

g#(X)activate#(X)g#(X)h#(activate(X))
c#d#activate#(n__c)c#
activate#(n__d)d#h#(n__d)g#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h

Strategy


Parameters


The following SCCs where found

g#(X) → h#(activate(X))h#(n__d) → g#(n__c)

Problem 2: ForwardNarrowing



Dependency Pair Problem

Dependency Pairs

g#(X)h#(activate(X))h#(n__d)g#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h

Strategy


Parameters


The right-hand side of the rule g#(X) → h#(activate(X)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
h#(d) 
h#(c) 
h#(_x21) 
Thus, the rule g#(X) → h#(activate(X)) is replaced by the following rules:
g#(_x21) → h#(_x21)g#(n__d) → h#(d)
g#(n__c) → h#(c)

Problem 3: ForwardNarrowing



Dependency Pair Problem

Dependency Pairs

g#(_x21)h#(_x21)g#(n__d)h#(d)
g#(n__c)h#(c)h#(n__d)g#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: n__d, activate, g, d, n__c, c, h

Strategy


Parameters


The right-hand side of the rule g#(n__c) → h#(c) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
h#(d) 
h#(n__c) 
Thus, the rule g#(n__c) → h#(c) is replaced by the following rules:
g#(n__c) → h#(n__c)g#(n__c) → h#(d)

Problem 4: ForwardNarrowing



Dependency Pair Problem

Dependency Pairs

g#(_x21)h#(_x21)g#(n__d)h#(d)
g#(n__c)h#(n__c)g#(n__c)h#(d)
h#(n__d)g#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h

Strategy


Parameters


The right-hand side of the rule g#(n__d) → h#(d) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
h#(n__d) 
Thus, the rule g#(n__d) → h#(d) is replaced by the following rules:
g#(n__d) → h#(n__d)

Problem 5: ForwardNarrowing



Dependency Pair Problem

Dependency Pairs

g#(_x21)h#(_x21)g#(n__d)h#(n__d)
g#(n__c)h#(n__c)g#(n__c)h#(d)
h#(n__d)g#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: n__d, activate, g, d, n__c, c, h

Strategy


Parameters


The right-hand side of the rule g#(n__c) → h#(n__c) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
Thus, the rule g#(n__c) → h#(n__c) is deleted.

Problem 6: ForwardNarrowing



Dependency Pair Problem

Dependency Pairs

g#(_x21)h#(_x21)g#(n__d)h#(n__d)
g#(n__c)h#(d)h#(n__d)g#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h

Strategy


Parameters


The right-hand side of the rule g#(n__c) → h#(d) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
h#(n__d) 
Thus, the rule g#(n__c) → h#(d) is replaced by the following rules:
g#(n__c) → h#(n__d)

Problem 7: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

g#(n__c)h#(n__d)g#(_x21)h#(_x21)
g#(n__d)h#(n__d)h#(n__d)g#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: n__d, activate, g, d, n__c, c, h

Strategy


Instantiation

For all potential predecessors l → r of the rule g#(_x21) → h#(_x21) on dependency pair chains it holds that: Thus, g#(_x21) → h#(_x21) is replaced by instances determined through the above matching. These instances are:
g#(n__c) → h#(n__c)

Problem 8: Propagation



Dependency Pair Problem

Dependency Pairs

g#(n__c)h#(n__d)g#(n__d)h#(n__d)
g#(n__c)h#(n__c)h#(n__d)g#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h

Strategy


The dependency pairs g#(n__c) → h#(n__d) and h#(n__d) → g#(n__c) are consolidated into the rule g#(n__c) → g#(n__c) .

This is possible as

The dependency pairs h#(n__d) → g#(n__c) and g#(n__c) → h#(n__d) are consolidated into the rule h#(n__d) → h#(n__d) .

This is possible as

The dependency pairs h#(n__d) → g#(n__c) and g#(n__c) → h#(n__d) are consolidated into the rule h#(n__d) → h#(n__d) .

This is possible as


Summary

Removed Dependency PairsAdded Dependency Pairs
g#(n__c) → h#(n__d)g#(n__c) → g#(n__c)
h#(n__d) → g#(n__c)h#(n__d) → h#(n__d)

Problem 9: ForwardNarrowing



Dependency Pair Problem

Dependency Pairs

g#(n__c)g#(n__c)g#(n__d)h#(n__d)
h#(n__d)h#(n__d)g#(n__c)h#(n__c)

Rewrite Rules

g(X)h(activate(X))cd
h(n__d)g(n__c)dn__d
cn__cactivate(n__d)d
activate(n__c)cactivate(X)X

Original Signature

Termination of terms over the following signature is verified: n__d, activate, g, d, n__c, c, h

Strategy


Parameters


The right-hand side of the rule g#(n__c) → h#(n__c) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
Thus, the rule g#(n__c) → h#(n__c) is deleted.