Term Rewriting System R:

   [x, y, z]
   f(s(a), s(b), x) -> f(x, x, x)
   g(f(s(x), s(y), z)) -> g(f(x, y, z))
   cons(x, y) -> x
   cons(x, y) -> y

Termination of R to be shown.


R contains the following Dependency Pairs: 


   F(s(a), s(b), x) -> F(x, x, x)
   G(f(s(x), s(y), z)) -> G(f(x, y, z))
   G(f(s(x), s(y), z)) -> F(x, y, z)

Furthermore, R contains two SCCs.


SCC1:

F(s(a), s(b), x) -> F(x, x, x)

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


Non-Termination of R could be shown.

Duration: 0.589 seconds.