NO

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

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

c# →* c#

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (5ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (51ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (30ms), DependencyGraph (0ms), ReductionPairSAT (9ms), DependencyGraph (1ms), SizeChangePrinciple (1ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

c# → c#c# → f#(g(c))

Rewrite Rules

c → f(g(c))f(g(X)) → g(X)

Original Signature

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

Strategy

The following SCCs where found

c# → c#