Term Rewriting System R:
[x, y, z, x1, x2, x3, x4]
f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
e1(h1, h2, x, y, z) -> e2(x, x, y, z, z)
e2(f1, x, y, z, f2) -> e3(x, y, x, y, y, z, y, z, x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1(x1, x1, x, y, z)

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F1 -> G1
F1 -> G2
F2 -> G1
F2 -> G2
E1(h1, h2, x, y, z) -> E2(x, x, y, z, z)
E2(f1, x, y, z, f2) -> E3(x, y, x, y, y, z, y, z, x, y, z)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E1(x1, x1, x, y, z)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

E4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E1(x1, x1, x, y, z)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E2(f1, x, y, z, f2) -> E3(x, y, x, y, y, z, y, z, x, y, z)
E1(h1, h2, x, y, z) -> E2(x, x, y, z, z)


Rules:


f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
e1(h1, h2, x, y, z) -> e2(x, x, y, z, z)
e2(f1, x, y, z, f2) -> e3(x, y, x, y, y, z, y, z, x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1(x1, x1, x, y, z)




The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
1:03 minutes