R
↳Dependency Pair Analysis
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)
E1(x1, x1, x, y, z) -> E5(x1, x, y, 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)
E4(i, x1, i, x1, i, x1, i, x1, x, y, z) -> E5(x1, x, y, z)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
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)
f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1(h1, h2, x, y, z) -> e2(x, x, y, z, z)
e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
e2(f1, x, y, z, f2) -> e3(x, y, x, y, y, z, y, z, x, y, z)
e2(x, x, y, z, z) -> e6(x, y, z)
e2(i, x, y, z, i) -> e6(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)
e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1(x1, x1, x, y, z)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
e5(i, x, y, z) -> e6(x, y, z)
one new Dependency Pair is created:
E1(h1, h2, x, y, z) -> E2(x, x, y, z, z)
E1(h1, h2, f1, y'', f2) -> E2(f1, f1, y'', f2, f2)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Forward Instantiation Transformation
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, f1, y'', f2) -> E2(f1, f1, y'', f2, f2)
E4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E1(x1, x1, x, y, z)
f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1(h1, h2, x, y, z) -> e2(x, x, y, z, z)
e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
e2(f1, x, y, z, f2) -> e3(x, y, x, y, y, z, y, z, x, y, z)
e2(x, x, y, z, z) -> e6(x, y, z)
e2(i, x, y, z, i) -> e6(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)
e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1(x1, x1, x, y, z)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
e5(i, x, y, z) -> e6(x, y, z)
one new Dependency Pair is created:
E4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E1(x1, x1, x, y, z)
E4(g1, x1', g2, x1', g1, x1', g2, x1', f1, y', f2) -> E1(x1', x1', f1, y', f2)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 3
↳Forward Instantiation Transformation
E2(f1, x, y, z, f2) -> E3(x, y, x, y, y, z, y, z, x, y, z)
E1(h1, h2, f1, y'', f2) -> E2(f1, f1, y'', f2, f2)
E4(g1, x1', g2, x1', g1, x1', g2, x1', f1, y', f2) -> E1(x1', x1', f1, y', f2)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1(h1, h2, x, y, z) -> e2(x, x, y, z, z)
e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
e2(f1, x, y, z, f2) -> e3(x, y, x, y, y, z, y, z, x, y, z)
e2(x, x, y, z, z) -> e6(x, y, z)
e2(i, x, y, z, i) -> e6(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)
e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1(x1, x1, x, y, z)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
e5(i, x, y, z) -> e6(x, y, z)
one new Dependency Pair is created:
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E3(x1', x1', x2', x2', x3', x3', x4', x4', f1, y', f2) -> E4(x1', x1', x2', x2', x3', x3', x4', x4', f1, y', f2)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 4
↳Forward Instantiation Transformation
E1(h1, h2, f1, y'', f2) -> E2(f1, f1, y'', f2, f2)
E4(g1, x1', g2, x1', g1, x1', g2, x1', f1, y', f2) -> E1(x1', x1', f1, y', f2)
E3(x1', x1', x2', x2', x3', x3', x4', x4', f1, y', f2) -> E4(x1', x1', x2', x2', x3', x3', x4', x4', f1, y', f2)
E2(f1, x, y, z, f2) -> E3(x, y, x, y, y, z, y, z, x, y, z)
f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1(h1, h2, x, y, z) -> e2(x, x, y, z, z)
e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
e2(f1, x, y, z, f2) -> e3(x, y, x, y, y, z, y, z, x, y, z)
e2(x, x, y, z, z) -> e6(x, y, z)
e2(i, x, y, z, i) -> e6(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)
e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1(x1, x1, x, y, z)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
e5(i, x, y, z) -> e6(x, y, z)
one new Dependency Pair is created:
E2(f1, x, y, z, f2) -> E3(x, y, x, y, y, z, y, z, x, y, z)
E2(f1, f1, y', f2, f2) -> E3(f1, y', f1, y', y', f2, y', f2, f1, y', f2)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 5
↳Remaining Obligation(s)
E4(g1, x1', g2, x1', g1, x1', g2, x1', f1, y', f2) -> E1(x1', x1', f1, y', f2)
E3(x1', x1', x2', x2', x3', x3', x4', x4', f1, y', f2) -> E4(x1', x1', x2', x2', x3', x3', x4', x4', f1, y', f2)
E2(f1, f1, y', f2, f2) -> E3(f1, y', f1, y', y', f2, y', f2, f1, y', f2)
E1(h1, h2, f1, y'', f2) -> E2(f1, f1, y'', f2, f2)
f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1(h1, h2, x, y, z) -> e2(x, x, y, z, z)
e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
e2(f1, x, y, z, f2) -> e3(x, y, x, y, y, z, y, z, x, y, z)
e2(x, x, y, z, z) -> e6(x, y, z)
e2(i, x, y, z, i) -> e6(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)
e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1(x1, x1, x, y, z)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
e5(i, x, y, z) -> e6(x, y, z)