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

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

f#(c) →* f#(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 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (2ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(X)f#(c)f#(X)c#

Rewrite Rules

f(X)f(c)cb

Original Signature

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

Strategy


Parameters


The following SCCs where found

f#(X) → f#(c)

Problem 2: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(X)f#(c)

Rewrite Rules

f(X)f(c)cb

Original Signature

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

Strategy


Instantiation

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