R
↳Dependency Pair Analysis
+'(+(x, y), z) -> +'(x, +(y, z))
+'(+(x, y), z) -> +'(y, z)
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, p1) -> +'(p1, p2)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p2, +(p2, p2)) -> +'(p1, p5)
+'(p2, +(p2, +(p2, x))) -> +'(p1, +(p5, x))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p5, p1) -> +'(p1, p5)
+'(p5, +(p1, x)) -> +'(p1, +(p5, x))
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p5, p2) -> +'(p2, p5)
+'(p5, +(p2, x)) -> +'(p2, +(p5, x))
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p10, p1) -> +'(p1, p10)
+'(p10, +(p1, x)) -> +'(p1, +(p10, x))
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p10, p2) -> +'(p2, p10)
+'(p10, +(p2, x)) -> +'(p2, +(p10, x))
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, p5) -> +'(p5, p10)
+'(p10, +(p5, x)) -> +'(p5, +(p10, x))
+'(p10, +(p5, x)) -> +'(p10, x)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p5, x)) -> +'(p5, +(p10, x))
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p2, +(p10, x))
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p1, +(p10, x))
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p2, +(p2, x))) -> +'(p1, +(p5, x))
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, x)) -> +'(p2, +(p5, x))
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p1, +(p5, x))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
six new Dependency Pairs are created:
+'(p2, +(p2, +(p2, x))) -> +'(p1, +(p5, x))
+'(p2, +(p2, +(p2, p5))) -> +'(p1, p10)
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p2))) -> +'(p1, +(p2, p5))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, x)) -> +'(p5, +(p10, x))
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, p2))) -> +'(p1, +(p2, p5))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p10, +(p2, x)) -> +'(p2, +(p10, x))
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, x)) -> +'(p2, +(p5, x))
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p1, +(p5, x))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, x)) -> +'(p1, +(p10, x))
+'(p10, +(p5, x)) -> +'(p10, x)
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
six new Dependency Pairs are created:
+'(p5, +(p1, x)) -> +'(p1, +(p5, x))
+'(p5, +(p1, p5)) -> +'(p1, p10)
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p2)) -> +'(p1, +(p2, p5))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 4
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, p2))) -> +'(p1, +(p2, p5))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p10, +(p2, x)) -> +'(p2, +(p10, x))
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, p2)) -> +'(p1, +(p2, p5))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p10, +(p1, x)) -> +'(p1, +(p10, x))
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p5, +(p2, x)) -> +'(p2, +(p5, x))
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, x)) -> +'(p5, +(p10, x))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
six new Dependency Pairs are created:
+'(p5, +(p2, x)) -> +'(p2, +(p5, x))
+'(p5, +(p2, p5)) -> +'(p2, p10)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p5, +(p2, p2)) -> +'(p2, +(p2, p5))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, x)) -> +'(p5, +(p10, x))
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p5, +(p2, p2)) -> +'(p2, +(p2, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, p2))) -> +'(p1, +(p2, p5))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, p2)) -> +'(p1, +(p2, p5))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p10, +(p2, x)) -> +'(p2, +(p10, x))
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, x)) -> +'(p1, +(p10, x))
+'(p10, +(p5, x)) -> +'(p10, x)
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
six new Dependency Pairs are created:
+'(p10, +(p1, x)) -> +'(p1, +(p10, x))
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p10, +(p1, p2)) -> +'(p1, +(p2, p10))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, p2)) -> +'(p1, +(p2, p10))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p5, +(p2, p2)) -> +'(p2, +(p2, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, p2))) -> +'(p1, +(p2, p5))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, p2)) -> +'(p1, +(p2, p5))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p10, +(p2, x)) -> +'(p2, +(p10, x))
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, x)) -> +'(p5, +(p10, x))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
six new Dependency Pairs are created:
+'(p10, +(p2, x)) -> +'(p2, +(p10, x))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, p2)) -> +'(p1, +(p2, p10))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p5, +(p2, p2)) -> +'(p2, +(p2, p5))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, p2))) -> +'(p1, +(p2, p5))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, p2)) -> +'(p1, +(p2, p5))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p10, +(p5, x)) -> +'(p5, +(p10, x))
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
six new Dependency Pairs are created:
+'(p10, +(p5, x)) -> +'(p5, +(p10, x))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, p2)) -> +'(p1, +(p2, p10))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p5, +(p2, p2)) -> +'(p2, +(p2, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, p2))) -> +'(p1, +(p2, p5))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, p2)) -> +'(p1, +(p2, p5))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
no new Dependency Pairs are created.
+'(p2, +(p2, +(p2, p2))) -> +'(p1, +(p2, p5))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 9
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, p2)) -> +'(p1, +(p2, p10))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p5, +(p2, p2)) -> +'(p2, +(p2, p5))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, p2)) -> +'(p1, +(p2, p5))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
no new Dependency Pairs are created.
+'(p5, +(p1, p2)) -> +'(p1, +(p2, p5))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 10
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, p2)) -> +'(p1, +(p2, p10))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p5, +(p2, p2)) -> +'(p2, +(p2, p5))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
no new Dependency Pairs are created.
+'(p5, +(p2, p2)) -> +'(p2, +(p2, p5))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 11
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, p2)) -> +'(p1, +(p2, p10))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
no new Dependency Pairs are created.
+'(p10, +(p1, p2)) -> +'(p1, +(p2, p10))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 12
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
no new Dependency Pairs are created.
+'(p10, +(p1, p5)) -> +'(p1, +(p5, p10))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 13
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
no new Dependency Pairs are created.
+'(p10, +(p2, p2)) -> +'(p2, +(p2, p10))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 3
↳Nar
...
→DP Problem 14
↳Narrowing Transformation
→DP Problem 2
↳Remaining
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
no new Dependency Pairs are created.
+'(p10, +(p2, p5)) -> +'(p2, +(p5, p10))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Remaining Obligation(s)
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
+'(+(x, y), z) -> +'(x, +(y, z))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Remaining Obligation(s)
+'(p10, +(p5, p5)) -> +'(p5, +(p5, p10))
+'(p10, +(p5, +(p2, x''))) -> +'(p5, +(p2, +(p10, x'')))
+'(p10, +(p5, p2)) -> +'(p5, +(p2, p10))
+'(p10, +(p5, +(p1, x''))) -> +'(p5, +(p1, +(p10, x'')))
+'(p10, +(p5, p1)) -> +'(p5, +(p1, p10))
+'(p10, +(p2, +(p5, x''))) -> +'(p2, +(p5, +(p10, x'')))
+'(p10, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p10, x'')))
+'(p10, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p10, x'')))
+'(p10, +(p2, p1)) -> +'(p2, +(p1, p10))
+'(p10, +(p1, +(p5, x''))) -> +'(p1, +(p5, +(p10, x'')))
+'(p10, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p10, x'')))
+'(p10, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p10, x'')))
+'(p5, +(p2, +(p5, x''))) -> +'(p2, +(p10, x''))
+'(p5, +(p2, +(p2, x''))) -> +'(p2, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p5, x'')))) -> +'(p1, +(p10, x''))
+'(p2, +(p2, +(p2, +(p2, x'')))) -> +'(p1, +(p2, +(p5, x'')))
+'(p2, +(p2, +(p2, +(p1, x'')))) -> +'(p1, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, p1))) -> +'(p1, +(p1, p5))
+'(p5, +(p2, +(p1, x''))) -> +'(p2, +(p1, +(p5, x'')))
+'(p2, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p2, x)
+'(p5, +(p2, p1)) -> +'(p2, +(p1, p5))
+'(p5, +(p1, +(p5, x''))) -> +'(p1, +(p10, x''))
+'(p5, +(p1, +(p2, x''))) -> +'(p1, +(p2, +(p5, x'')))
+'(p5, +(p1, +(p1, x''))) -> +'(p1, +(p1, +(p5, x'')))
+'(p5, +(p1, p1)) -> +'(p1, +(p1, p5))
+'(p1, +(p2, +(p2, x))) -> +'(p5, x)
+'(p2, +(p1, x)) -> +'(p1, +(p2, x))
+'(p1, +(p1, x)) -> +'(p2, x)
+'(p10, +(p1, p1)) -> +'(p1, +(p1, p10))
+'(p10, +(p5, x)) -> +'(p10, x)
+'(p10, +(p2, x)) -> +'(p10, x)
+'(p10, +(p1, x)) -> +'(p10, x)
+'(p5, +(p5, x)) -> +'(p10, x)
+'(p5, +(p2, x)) -> +'(p5, x)
+'(p5, +(p1, x)) -> +'(p5, x)
+'(p10, +(p5, +(p5, x''))) -> +'(p5, +(p5, +(p10, x'')))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))
+'(+(x, y), z) -> +'(x, +(y, z))
+(p1, p1) -> p2
+(p1, +(p2, p2)) -> p5
+(p5, p5) -> p10
+(+(x, y), z) -> +(x, +(y, z))
+(p1, +(p1, x)) -> +(p2, x)
+(p1, +(p2, +(p2, x))) -> +(p5, x)
+(p2, p1) -> +(p1, p2)
+(p2, +(p1, x)) -> +(p1, +(p2, x))
+(p2, +(p2, p2)) -> +(p1, p5)
+(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
+(p5, p1) -> +(p1, p5)
+(p5, +(p1, x)) -> +(p1, +(p5, x))
+(p5, p2) -> +(p2, p5)
+(p5, +(p2, x)) -> +(p2, +(p5, x))
+(p5, +(p5, x)) -> +(p10, x)
+(p10, p1) -> +(p1, p10)
+(p10, +(p1, x)) -> +(p1, +(p10, x))
+(p10, p2) -> +(p2, p10)
+(p10, +(p2, x)) -> +(p2, +(p10, x))
+(p10, p5) -> +(p5, p10)
+(p10, +(p5, x)) -> +(p5, +(p10, x))