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

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

h#(c) →* h#(c)

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

h#(d)c#g#(X)h#(X)
h#(d)g#(c)

Rewrite Rules

g(X)h(X)cd
h(d)g(c)

Original Signature

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

Strategy


Parameters


The following SCCs where found

g#(X) → h#(X)h#(d) → g#(c)

Problem 2: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

g#(X)h#(X)h#(d)g#(c)

Rewrite Rules

g(X)h(X)cd
h(d)g(c)

Original Signature

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

Strategy


Instantiation

For all potential predecessors l → r of the rule g#(X) → h#(X) on dependency pair chains it holds that: Thus, g#(X) → h#(X) is replaced by instances determined through the above matching. These instances are:
g#(c) → h#(c)
Caught Exception: class java.lang.ThreadDeath
null

Problem 3: Propagation



Dependency Pair Problem

Dependency Pairs

g#(c)h#(c)h#(d)g#(c)

Rewrite Rules

g(X)h(X)cd
h(d)g(c)

Original Signature

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

Strategy


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

This is possible as

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

This is possible as


Summary

Removed Dependency PairsAdded Dependency Pairs
g#(c) → h#(c)h#(d) → h#(c)
h#(d) → g#(c) 

Problem 4: BackwardsNarrowing



Dependency Pair Problem

Dependency Pairs

h#(d)h#(c)

Rewrite Rules

g(X)h(X)cd
h(d)g(c)

Original Signature

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

Strategy


Parameters


The left-hand side of the rule h#(d) → h#(c) is backward 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#(c) 
Thus, the rule h#(d) → h#(c) is replaced by the following rules:
h#(c) → h#(c)