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

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

f#(a) →* f#(a)

The following DP Processors were used


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

Problem 1: BackwardInstantiation

Dependency Pair Problem

Dependency Pairs

f#(X) → f#(a)

Rewrite Rules

f(X) → f(a)b → a

Original Signature

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

Strategy

Instantiation

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