R
↳Dependency Pair Analysis
A(b(x)) -> B(a(a(x)))
A(b(x)) -> A(a(x))
A(b(x)) -> A(x)
B(c(x)) -> C(b(b(x)))
B(c(x)) -> B(b(x))
B(c(x)) -> B(x)
C(a(x)) -> A(c(c(x)))
C(a(x)) -> C(c(x))
C(a(x)) -> C(x)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
B(c(x)) -> B(x)
B(c(x)) -> B(b(x))
C(a(x)) -> C(x)
C(a(x)) -> C(c(x))
A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
C(a(x)) -> A(c(c(x)))
B(c(x)) -> C(b(b(x)))
A(b(x)) -> B(a(a(x)))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
two new Dependency Pairs are created:
A(b(x)) -> B(a(a(x)))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
A(b(u(x''))) -> B(a(x''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
C(a(x)) -> C(x)
C(a(x)) -> C(c(x))
A(b(u(x''))) -> B(a(x''))
B(c(x)) -> B(b(x))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
C(a(x)) -> A(c(c(x)))
B(c(x)) -> C(b(b(x)))
B(c(x)) -> B(x)
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
two new Dependency Pairs are created:
A(b(x)) -> A(a(x))
A(b(b(x''))) -> A(b(a(a(x''))))
A(b(u(x''))) -> A(x'')
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Narrowing Transformation
A(b(u(x''))) -> A(x'')
A(b(b(x''))) -> A(b(a(a(x''))))
A(b(u(x''))) -> B(a(x''))
B(c(x)) -> B(x)
B(c(x)) -> B(b(x))
C(a(x)) -> C(c(x))
B(c(x)) -> C(b(b(x)))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
A(b(x)) -> A(x)
C(a(x)) -> A(c(c(x)))
C(a(x)) -> C(x)
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
two new Dependency Pairs are created:
B(c(x)) -> C(b(b(x)))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(v(x''))) -> C(b(x''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Narrowing Transformation
A(b(b(x''))) -> A(b(a(a(x''))))
C(a(x)) -> C(x)
C(a(x)) -> C(c(x))
B(c(v(x''))) -> C(b(x''))
A(b(u(x''))) -> B(a(x''))
C(a(x)) -> A(c(c(x)))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(x)) -> B(x)
B(c(x)) -> B(b(x))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
A(b(x)) -> A(x)
A(b(u(x''))) -> A(x'')
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
two new Dependency Pairs are created:
B(c(x)) -> B(b(x))
B(c(c(x''))) -> B(c(b(b(x''))))
B(c(v(x''))) -> B(x'')
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
A(b(u(x''))) -> A(x'')
B(c(v(x''))) -> B(x'')
B(c(c(x''))) -> B(c(b(b(x''))))
C(a(x)) -> C(x)
C(a(x)) -> C(c(x))
B(c(v(x''))) -> C(b(x''))
A(b(u(x''))) -> B(a(x''))
C(a(x)) -> A(c(c(x)))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(x)) -> B(x)
A(b(b(x''))) -> B(a(b(a(a(x'')))))
A(b(x)) -> A(x)
A(b(b(x''))) -> A(b(a(a(x''))))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
two new Dependency Pairs are created:
C(a(x)) -> A(c(c(x)))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
C(a(w(x''))) -> A(c(x''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
B(c(v(x''))) -> B(x'')
B(c(c(x''))) -> B(c(b(b(x''))))
A(b(b(x''))) -> A(b(a(a(x''))))
C(a(w(x''))) -> A(c(x''))
B(c(v(x''))) -> C(b(x''))
A(b(u(x''))) -> B(a(x''))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
C(a(x)) -> C(x)
C(a(x)) -> C(c(x))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(x)) -> B(x)
A(b(b(x''))) -> B(a(b(a(a(x'')))))
A(b(x)) -> A(x)
A(b(u(x''))) -> A(x'')
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
two new Dependency Pairs are created:
C(a(x)) -> C(c(x))
C(a(a(x''))) -> C(a(c(c(x''))))
C(a(w(x''))) -> C(x'')
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Forward Instantiation Transformation
C(a(w(x''))) -> C(x'')
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(u(x''))) -> A(x'')
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(c(x''))) -> B(c(b(b(x''))))
A(b(u(x''))) -> B(a(x''))
C(a(w(x''))) -> A(c(x''))
B(c(v(x''))) -> C(b(x''))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
A(b(x)) -> A(x)
C(a(a(x''))) -> A(c(a(c(c(x'')))))
C(a(x)) -> C(x)
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(x)) -> B(x)
B(c(v(x''))) -> B(x'')
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
three new Dependency Pairs are created:
A(b(x)) -> A(x)
A(b(b(x''))) -> A(b(x''))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(u(x'''')))) -> A(b(u(x'''')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 8
↳Forward Instantiation Transformation
A(b(b(u(x'''')))) -> A(b(u(x'''')))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(u(x''))) -> A(x'')
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(v(x''))) -> B(x'')
B(c(c(x''))) -> B(c(b(b(x''))))
C(a(a(x''))) -> C(a(c(c(x''))))
B(c(v(x''))) -> C(b(x''))
A(b(u(x''))) -> B(a(x''))
C(a(w(x''))) -> A(c(x''))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(x)) -> B(x)
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
C(a(x)) -> C(x)
C(a(w(x''))) -> C(x'')
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
three new Dependency Pairs are created:
B(c(x)) -> B(x)
B(c(c(x''))) -> B(c(x''))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(v(x'''')))) -> B(c(v(x'''')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 9
↳Forward Instantiation Transformation
B(c(c(v(x'''')))) -> B(c(v(x'''')))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(v(x''))) -> B(x'')
B(c(c(x''))) -> B(c(b(b(x''))))
C(a(w(x''))) -> C(x'')
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(u(x''))) -> A(x'')
A(b(b(x''))) -> A(b(a(a(x''))))
C(a(w(x''))) -> A(c(x''))
B(c(v(x''))) -> C(b(x''))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
C(a(x)) -> C(x)
B(c(c(x''))) -> C(b(c(b(b(x'')))))
A(b(u(x''))) -> B(a(x''))
A(b(b(u(x'''')))) -> A(b(u(x'''')))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
three new Dependency Pairs are created:
C(a(x)) -> C(x)
C(a(a(x''))) -> C(a(x''))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(w(x'''')))) -> C(a(w(x'''')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 10
↳Forward Instantiation Transformation
C(a(a(w(x'''')))) -> C(a(w(x'''')))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(w(x''))) -> C(x'')
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(b(u(x'''')))) -> A(b(u(x'''')))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(u(x''))) -> A(x'')
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(v(x''))) -> B(x'')
B(c(c(x''))) -> B(c(b(b(x''))))
A(b(u(x''))) -> B(a(x''))
C(a(w(x''))) -> A(c(x''))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
B(c(v(x''))) -> C(b(x''))
B(c(c(v(x'''')))) -> B(c(v(x'''')))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
four new Dependency Pairs are created:
A(b(u(x''))) -> A(x'')
A(b(u(b(b(x''''))))) -> A(b(b(x'''')))
A(b(u(b(u(x''''))))) -> A(b(u(x'''')))
A(b(u(b(b(b(x'''''')))))) -> A(b(b(b(x''''''))))
A(b(u(b(b(u(x'''''')))))) -> A(b(b(u(x''''''))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 11
↳Forward Instantiation Transformation
A(b(u(b(b(u(x'''''')))))) -> A(b(b(u(x''''''))))
A(b(u(b(b(b(x'''''')))))) -> A(b(b(b(x''''''))))
A(b(u(b(u(x''''))))) -> A(b(u(x'''')))
A(b(u(b(b(x''''))))) -> A(b(b(x'''')))
A(b(b(u(x'''')))) -> A(b(u(x'''')))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(c(v(x'''')))) -> B(c(v(x'''')))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(v(x''))) -> B(x'')
B(c(c(x''))) -> B(c(b(b(x''))))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(w(x''))) -> C(x'')
C(a(a(x''))) -> C(a(c(c(x''))))
B(c(v(x''))) -> C(b(x''))
A(b(u(x''))) -> B(a(x''))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(w(x''))) -> A(c(x''))
C(a(a(w(x'''')))) -> C(a(w(x'''')))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
four new Dependency Pairs are created:
B(c(v(x''))) -> B(x'')
B(c(v(c(c(x''''))))) -> B(c(c(x'''')))
B(c(v(c(v(x''''))))) -> B(c(v(x'''')))
B(c(v(c(c(c(x'''''')))))) -> B(c(c(c(x''''''))))
B(c(v(c(c(v(x'''''')))))) -> B(c(c(v(x''''''))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 12
↳Forward Instantiation Transformation
B(c(v(c(c(v(x'''''')))))) -> B(c(c(v(x''''''))))
B(c(v(c(c(c(x'''''')))))) -> B(c(c(c(x''''''))))
B(c(v(c(v(x''''))))) -> B(c(v(x'''')))
B(c(v(c(c(x''''))))) -> B(c(c(x'''')))
B(c(c(v(x'''')))) -> B(c(v(x'''')))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(c(x''))) -> B(c(b(b(x''))))
C(a(a(w(x'''')))) -> C(a(w(x'''')))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(w(x''))) -> C(x'')
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(u(b(b(b(x'''''')))))) -> A(b(b(b(x''''''))))
A(b(u(b(u(x''''))))) -> A(b(u(x'''')))
A(b(u(b(b(x''''))))) -> A(b(b(x'''')))
A(b(b(u(x'''')))) -> A(b(u(x'''')))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
C(a(w(x''))) -> A(c(x''))
B(c(v(x''))) -> C(b(x''))
A(b(u(x''))) -> B(a(x''))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
A(b(u(b(b(u(x'''''')))))) -> A(b(b(u(x''''''))))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
four new Dependency Pairs are created:
C(a(w(x''))) -> C(x'')
C(a(w(a(a(x''''))))) -> C(a(a(x'''')))
C(a(w(a(w(x''''))))) -> C(a(w(x'''')))
C(a(w(a(a(a(x'''''')))))) -> C(a(a(a(x''''''))))
C(a(w(a(a(w(x'''''')))))) -> C(a(a(w(x''''''))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 13
↳Polynomial Ordering
C(a(w(a(a(w(x'''''')))))) -> C(a(a(w(x''''''))))
C(a(w(a(a(a(x'''''')))))) -> C(a(a(a(x''''''))))
C(a(w(a(w(x''''))))) -> C(a(w(x'''')))
C(a(w(a(a(x''''))))) -> C(a(a(x'''')))
C(a(a(w(x'''')))) -> C(a(w(x'''')))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(u(b(b(u(x'''''')))))) -> A(b(b(u(x''''''))))
A(b(u(b(b(b(x'''''')))))) -> A(b(b(b(x''''''))))
A(b(u(b(u(x''''))))) -> A(b(u(x'''')))
A(b(u(b(b(x''''))))) -> A(b(b(x'''')))
A(b(b(u(x'''')))) -> A(b(u(x'''')))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(v(c(c(c(x'''''')))))) -> B(c(c(c(x''''''))))
B(c(v(c(v(x''''))))) -> B(c(v(x'''')))
B(c(v(c(c(x''''))))) -> B(c(c(x'''')))
B(c(c(v(x'''')))) -> B(c(v(x'''')))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(c(x''))) -> B(c(b(b(x''))))
A(b(u(x''))) -> B(a(x''))
C(a(w(x''))) -> A(c(x''))
B(c(v(x''))) -> C(b(x''))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(v(c(c(v(x'''''')))))) -> B(c(c(v(x''''''))))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
A(b(u(b(b(u(x'''''')))))) -> A(b(b(u(x''''''))))
A(b(u(b(b(b(x'''''')))))) -> A(b(b(b(x''''''))))
A(b(u(b(u(x''''))))) -> A(b(u(x'''')))
A(b(u(b(b(x''''))))) -> A(b(b(x'''')))
A(b(u(x''))) -> B(a(x''))
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
w(c(x)) -> x
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
POL(c(x1)) = x1 POL(C(x1)) = x1 POL(v(x1)) = x1 POL(B(x1)) = x1 POL(b(x1)) = x1 POL(a(x1)) = x1 POL(w(x1)) = x1 POL(u(x1)) = 1 + x1 POL(A(x1)) = x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 14
↳Dependency Graph
C(a(w(a(a(w(x'''''')))))) -> C(a(a(w(x''''''))))
C(a(w(a(a(a(x'''''')))))) -> C(a(a(a(x''''''))))
C(a(w(a(w(x''''))))) -> C(a(w(x'''')))
C(a(w(a(a(x''''))))) -> C(a(a(x'''')))
C(a(a(w(x'''')))) -> C(a(w(x'''')))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(b(u(x'''')))) -> A(b(u(x'''')))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(v(c(c(c(x'''''')))))) -> B(c(c(c(x''''''))))
B(c(v(c(v(x''''))))) -> B(c(v(x'''')))
B(c(v(c(c(x''''))))) -> B(c(c(x'''')))
B(c(c(v(x'''')))) -> B(c(v(x'''')))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(c(x''))) -> B(c(b(b(x''))))
C(a(w(x''))) -> A(c(x''))
B(c(v(x''))) -> C(b(x''))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(v(c(c(v(x'''''')))))) -> B(c(c(v(x''''''))))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 15
↳Polynomial Ordering
B(c(v(c(c(v(x'''''')))))) -> B(c(c(v(x''''''))))
B(c(v(c(c(c(x'''''')))))) -> B(c(c(c(x''''''))))
B(c(v(c(v(x''''))))) -> B(c(v(x'''')))
B(c(v(c(c(x''''))))) -> B(c(c(x'''')))
B(c(c(v(x'''')))) -> B(c(v(x'''')))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(c(x''))) -> B(c(b(b(x''))))
B(c(v(x''))) -> C(b(x''))
C(a(w(a(a(a(x'''''')))))) -> C(a(a(a(x''''''))))
C(a(w(a(w(x''''))))) -> C(a(w(x'''')))
C(a(w(a(a(x''''))))) -> C(a(a(x'''')))
C(a(a(w(x'''')))) -> C(a(w(x'''')))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
C(a(w(x''))) -> A(c(x''))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
C(a(w(a(a(w(x'''''')))))) -> C(a(a(w(x''''''))))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
B(c(v(c(c(v(x'''''')))))) -> B(c(c(v(x''''''))))
B(c(v(c(c(c(x'''''')))))) -> B(c(c(c(x''''''))))
B(c(v(c(v(x''''))))) -> B(c(v(x'''')))
B(c(v(c(c(x''''))))) -> B(c(c(x'''')))
B(c(v(x''))) -> C(b(x''))
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
v(b(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
w(c(x)) -> x
POL(c(x1)) = x1 POL(C(x1)) = x1 POL(v(x1)) = 1 + x1 POL(B(x1)) = x1 POL(b(x1)) = x1 POL(a(x1)) = x1 POL(w(x1)) = x1 POL(u(x1)) = 1 + x1 POL(A(x1)) = x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 16
↳Dependency Graph
B(c(c(v(x'''')))) -> B(c(v(x'''')))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(c(x''))) -> B(c(b(b(x''))))
C(a(w(a(a(a(x'''''')))))) -> C(a(a(a(x''''''))))
C(a(w(a(w(x''''))))) -> C(a(w(x'''')))
C(a(w(a(a(x''''))))) -> C(a(a(x'''')))
C(a(a(w(x'''')))) -> C(a(w(x'''')))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
C(a(w(x''))) -> A(c(x''))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
C(a(w(a(a(w(x'''''')))))) -> C(a(a(w(x''''''))))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 17
↳Polynomial Ordering
C(a(w(a(a(w(x'''''')))))) -> C(a(a(w(x''''''))))
C(a(w(a(a(a(x'''''')))))) -> C(a(a(a(x''''''))))
C(a(w(a(w(x''''))))) -> C(a(w(x'''')))
C(a(w(a(a(x''''))))) -> C(a(a(x'''')))
C(a(a(w(x'''')))) -> C(a(w(x'''')))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(a(x''))) -> C(a(c(c(x''))))
C(a(w(x''))) -> A(c(x''))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(c(x''))) -> B(c(x''))
B(c(c(x''))) -> B(c(b(b(x''))))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
C(a(w(a(a(w(x'''''')))))) -> C(a(a(w(x''''''))))
C(a(w(a(a(a(x'''''')))))) -> C(a(a(a(x''''''))))
C(a(w(a(w(x''''))))) -> C(a(w(x'''')))
C(a(w(a(a(x''''))))) -> C(a(a(x'''')))
C(a(w(x''))) -> A(c(x''))
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
w(c(x)) -> x
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
POL(c(x1)) = x1 POL(C(x1)) = x1 POL(v(x1)) = 1 + x1 POL(B(x1)) = x1 POL(b(x1)) = x1 POL(a(x1)) = x1 POL(w(x1)) = 1 + x1 POL(u(x1)) = 1 + x1 POL(A(x1)) = x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 18
↳Dependency Graph
C(a(a(w(x'''')))) -> C(a(w(x'''')))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
C(a(a(x''))) -> C(a(x''))
C(a(a(x''))) -> C(a(c(c(x''))))
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(c(x''))) -> B(c(x''))
B(c(c(x''))) -> B(c(b(b(x''))))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 19
↳Remaining Obligation(s)
A(b(b(b(x'''')))) -> A(b(b(x'''')))
A(b(b(x''))) -> A(b(x''))
A(b(b(x''))) -> A(b(a(a(x''))))
B(c(c(c(x'''')))) -> B(c(c(x'''')))
B(c(c(x''))) -> B(c(x''))
B(c(c(x''))) -> B(c(b(b(x''))))
C(a(a(x''))) -> C(a(x''))
C(a(a(x''))) -> C(a(c(c(x''))))
B(c(c(x''))) -> C(b(c(b(b(x'')))))
A(b(b(x''))) -> B(a(b(a(a(x'')))))
C(a(a(x''))) -> A(c(a(c(c(x'')))))
C(a(a(a(x'''')))) -> C(a(a(x'''')))
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
innermost