Term Rewriting System R:

   [x, y, z, u, v]
   f(x, y, f(z, u, v)) -> f(f(x, y, z), u, f(x, y, v))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   F(x, y, f(z, u, v)) -> F(f(x, y, z), u, f(x, y, v))
   F(x, y, f(z, u, v)) -> F(x, y, z)
   F(x, y, f(z, u, v)) -> F(x, y, v)

Furthermore, R contains one SCC.


SCC1:

F(x, y, f(z, u, v)) -> F(x, y, v)
F(x, y, f(z, u, v)) -> F(x, y, z)
F(x, y, f(z, u, v)) -> F(f(x, y, z), u, f(x, y, v))

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


Non-Termination of R could be shown.

Duration: 0.520 seconds.