Term Rewriting System R:

   [X]
   f(a, b, X) -> f(X, X, X)
   c -> a
   c -> b

Termination of R to be shown.


R contains the following Dependency Pairs: 


   F(a, b, X) -> F(X, X, X)

Furthermore, R contains one SCC.


SCC1:

F(a, b, X) -> F(X, X, X)

Found an infinite P-chain over R:
P = F(a, b, X) -> F(X, X, X)
R = [c -> a, c -> b, f(a, b, X) -> f(X, X, X)]
s = F(a, b, c) evaluates to t = F(a, b, c)
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 0.449 seconds.