Term Rewriting System R:

   [x, y, z]
   f(g(x, y), x, z) -> f(z, z, z)
   g(x, y) -> x
   g(x, y) -> y

Termination of R to be shown.


R contains the following Dependency Pairs: 


   F(g(x, y), x, z) -> F(z, z, z)

Furthermore, R contains one SCC.


SCC1:

F(g(x, y), x, z) -> F(z, z, z)

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


Non-Termination of R could be shown.

Duration: 0.457 seconds.