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

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F1(a, x) -> G1(x, x)
F1(x, a) -> G2(x, x)
F2(a, x) -> G1(x, x)
F2(x, a) -> G2(x, x)
G1(a, x) -> H1(x)
G1(x, a) -> H2(x)
G2(a, x) -> H1(x)
G2(x, a) -> H2(x)
E1(h1(w), h2(w), x, y, z, w) -> E2(x, x, y, z, z, w)
E1(x1, x1, x, y, z, a) -> E5(x1, x, y, z)
E2(f1(w, w), x, y, z, f2(w, w), w) -> E3(x, y, x, y, y, z, y, z, x, y, z, w)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
E4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> E1(x1, x1, x, y, z, w)
E4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) -> E5(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(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> E1(x1, x1, x, y, z, w)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
E2(f1(w, w), x, y, z, f2(w, w), w) -> E3(x, y, x, y, y, z, y, z, x, y, z, w)
E1(h1(w), h2(w), x, y, z, w) -> E2(x, x, y, z, z, w)


Rules:


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




Termination of R could not be shown.
Duration:
0:31 minutes