YES Problem: a(a(x1)) -> b(b(b(x1))) a(x1) -> c(d(x1)) b(b(x1)) -> c(c(c(x1))) c(c(x1)) -> d(d(d(x1))) e(d(x1)) -> a(b(c(d(e(x1))))) b(x1) -> d(d(x1)) e(c(x1)) -> b(a(a(e(x1)))) c(d(d(x1))) -> a(x1) Proof: DP Processor: DPs: a#(a(x1)) -> b#(x1) a#(a(x1)) -> b#(b(x1)) a#(a(x1)) -> b#(b(b(x1))) a#(x1) -> c#(d(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) e#(d(x1)) -> e#(x1) e#(d(x1)) -> c#(d(e(x1))) e#(d(x1)) -> b#(c(d(e(x1)))) e#(d(x1)) -> a#(b(c(d(e(x1))))) e#(c(x1)) -> e#(x1) e#(c(x1)) -> a#(e(x1)) e#(c(x1)) -> a#(a(e(x1))) e#(c(x1)) -> b#(a(a(e(x1)))) c#(d(d(x1))) -> a#(x1) TRS: a(a(x1)) -> b(b(b(x1))) a(x1) -> c(d(x1)) b(b(x1)) -> c(c(c(x1))) c(c(x1)) -> d(d(d(x1))) e(d(x1)) -> a(b(c(d(e(x1))))) b(x1) -> d(d(x1)) e(c(x1)) -> b(a(a(e(x1)))) c(d(d(x1))) -> a(x1) TDG Processor: DPs: a#(a(x1)) -> b#(x1) a#(a(x1)) -> b#(b(x1)) a#(a(x1)) -> b#(b(b(x1))) a#(x1) -> c#(d(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) e#(d(x1)) -> e#(x1) e#(d(x1)) -> c#(d(e(x1))) e#(d(x1)) -> b#(c(d(e(x1)))) e#(d(x1)) -> a#(b(c(d(e(x1))))) e#(c(x1)) -> e#(x1) e#(c(x1)) -> a#(e(x1)) e#(c(x1)) -> a#(a(e(x1))) e#(c(x1)) -> b#(a(a(e(x1)))) c#(d(d(x1))) -> a#(x1) TRS: a(a(x1)) -> b(b(b(x1))) a(x1) -> c(d(x1)) b(b(x1)) -> c(c(c(x1))) c(c(x1)) -> d(d(d(x1))) e(d(x1)) -> a(b(c(d(e(x1))))) b(x1) -> d(d(x1)) e(c(x1)) -> b(a(a(e(x1)))) c(d(d(x1))) -> a(x1) graph: e#(c(x1)) -> e#(x1) -> e#(c(x1)) -> b#(a(a(e(x1)))) e#(c(x1)) -> e#(x1) -> e#(c(x1)) -> a#(a(e(x1))) e#(c(x1)) -> e#(x1) -> e#(c(x1)) -> a#(e(x1)) e#(c(x1)) -> e#(x1) -> e#(c(x1)) -> e#(x1) e#(c(x1)) -> e#(x1) -> e#(d(x1)) -> a#(b(c(d(e(x1))))) e#(c(x1)) -> e#(x1) -> e#(d(x1)) -> b#(c(d(e(x1)))) e#(c(x1)) -> e#(x1) -> e#(d(x1)) -> c#(d(e(x1))) e#(c(x1)) -> e#(x1) -> e#(d(x1)) -> e#(x1) e#(c(x1)) -> b#(a(a(e(x1)))) -> b#(b(x1)) -> c#(c(c(x1))) e#(c(x1)) -> b#(a(a(e(x1)))) -> b#(b(x1)) -> c#(c(x1)) e#(c(x1)) -> b#(a(a(e(x1)))) -> b#(b(x1)) -> c#(x1) e#(c(x1)) -> a#(e(x1)) -> a#(x1) -> c#(d(x1)) e#(c(x1)) -> a#(e(x1)) -> a#(a(x1)) -> b#(b(b(x1))) e#(c(x1)) -> a#(e(x1)) -> a#(a(x1)) -> b#(b(x1)) e#(c(x1)) -> a#(e(x1)) -> a#(a(x1)) -> b#(x1) e#(c(x1)) -> a#(a(e(x1))) -> a#(x1) -> c#(d(x1)) e#(c(x1)) -> a#(a(e(x1))) -> a#(a(x1)) -> b#(b(b(x1))) e#(c(x1)) -> a#(a(e(x1))) -> a#(a(x1)) -> b#(b(x1)) e#(c(x1)) -> a#(a(e(x1))) -> a#(a(x1)) -> b#(x1) e#(d(x1)) -> e#(x1) -> e#(c(x1)) -> b#(a(a(e(x1)))) e#(d(x1)) -> e#(x1) -> e#(c(x1)) -> a#(a(e(x1))) e#(d(x1)) -> e#(x1) -> e#(c(x1)) -> a#(e(x1)) e#(d(x1)) -> e#(x1) -> e#(c(x1)) -> e#(x1) e#(d(x1)) -> e#(x1) -> e#(d(x1)) -> a#(b(c(d(e(x1))))) e#(d(x1)) -> e#(x1) -> e#(d(x1)) -> b#(c(d(e(x1)))) e#(d(x1)) -> e#(x1) -> e#(d(x1)) -> c#(d(e(x1))) e#(d(x1)) -> e#(x1) -> e#(d(x1)) -> e#(x1) e#(d(x1)) -> c#(d(e(x1))) -> c#(d(d(x1))) -> a#(x1) e#(d(x1)) -> b#(c(d(e(x1)))) -> b#(b(x1)) -> c#(c(c(x1))) e#(d(x1)) -> b#(c(d(e(x1)))) -> b#(b(x1)) -> c#(c(x1)) e#(d(x1)) -> b#(c(d(e(x1)))) -> b#(b(x1)) -> c#(x1) e#(d(x1)) -> a#(b(c(d(e(x1))))) -> a#(x1) -> c#(d(x1)) e#(d(x1)) -> a#(b(c(d(e(x1))))) -> a#(a(x1)) -> b#(b(b(x1))) e#(d(x1)) -> a#(b(c(d(e(x1))))) -> a#(a(x1)) -> b#(b(x1)) e#(d(x1)) -> a#(b(c(d(e(x1))))) -> a#(a(x1)) -> b#(x1) c#(d(d(x1))) -> a#(x1) -> a#(x1) -> c#(d(x1)) c#(d(d(x1))) -> a#(x1) -> a#(a(x1)) -> b#(b(b(x1))) c#(d(d(x1))) -> a#(x1) -> a#(a(x1)) -> b#(b(x1)) c#(d(d(x1))) -> a#(x1) -> a#(a(x1)) -> b#(x1) b#(b(x1)) -> c#(c(c(x1))) -> c#(d(d(x1))) -> a#(x1) b#(b(x1)) -> c#(c(x1)) -> c#(d(d(x1))) -> a#(x1) b#(b(x1)) -> c#(x1) -> c#(d(d(x1))) -> a#(x1) a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(c(x1)) a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(x1) a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(c(x1)) a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(x1) a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(c(x1)) a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(x1) a#(x1) -> c#(d(x1)) -> c#(d(d(x1))) -> a#(x1) SCC Processor: #sccs: 2 #rules: 10 #arcs: 52/256 DPs: e#(c(x1)) -> e#(x1) e#(d(x1)) -> e#(x1) TRS: a(a(x1)) -> b(b(b(x1))) a(x1) -> c(d(x1)) b(b(x1)) -> c(c(c(x1))) c(c(x1)) -> d(d(d(x1))) e(d(x1)) -> a(b(c(d(e(x1))))) b(x1) -> d(d(x1)) e(c(x1)) -> b(a(a(e(x1)))) c(d(d(x1))) -> a(x1) Matrix Interpretation Processor: dim=1 interpretation: [e#](x0) = 3x0 + 2, [e](x0) = 9x0, [c](x0) = x0 + 6, [d](x0) = x0 + 4, [b](x0) = x0 + 9, [a](x0) = x0 + 14 orientation: e#(c(x1)) = 3x1 + 20 >= 3x1 + 2 = e#(x1) e#(d(x1)) = 3x1 + 14 >= 3x1 + 2 = e#(x1) a(a(x1)) = x1 + 28 >= x1 + 27 = b(b(b(x1))) a(x1) = x1 + 14 >= x1 + 10 = c(d(x1)) b(b(x1)) = x1 + 18 >= x1 + 18 = c(c(c(x1))) c(c(x1)) = x1 + 12 >= x1 + 12 = d(d(d(x1))) e(d(x1)) = 9x1 + 36 >= 9x1 + 33 = a(b(c(d(e(x1))))) b(x1) = x1 + 9 >= x1 + 8 = d(d(x1)) e(c(x1)) = 9x1 + 54 >= 9x1 + 37 = b(a(a(e(x1)))) c(d(d(x1))) = x1 + 14 >= x1 + 14 = a(x1) problem: DPs: TRS: a(a(x1)) -> b(b(b(x1))) a(x1) -> c(d(x1)) b(b(x1)) -> c(c(c(x1))) c(c(x1)) -> d(d(d(x1))) e(d(x1)) -> a(b(c(d(e(x1))))) b(x1) -> d(d(x1)) e(c(x1)) -> b(a(a(e(x1)))) c(d(d(x1))) -> a(x1) Qed DPs: c#(d(d(x1))) -> a#(x1) a#(a(x1)) -> b#(x1) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> b#(b(x1)) a#(a(x1)) -> b#(b(b(x1))) a#(x1) -> c#(d(x1)) TRS: a(a(x1)) -> b(b(b(x1))) a(x1) -> c(d(x1)) b(b(x1)) -> c(c(c(x1))) c(c(x1)) -> d(d(d(x1))) e(d(x1)) -> a(b(c(d(e(x1))))) b(x1) -> d(d(x1)) e(c(x1)) -> b(a(a(e(x1)))) c(d(d(x1))) -> a(x1) Matrix Interpretation Processor: dim=1 interpretation: [c#](x0) = x0 + 8, [b#](x0) = x0 + 11, [a#](x0) = x0 + 15, [e](x0) = 9x0 + 1, [c](x0) = x0 + 6, [d](x0) = x0 + 4, [b](x0) = x0 + 9, [a](x0) = x0 + 14 orientation: c#(d(d(x1))) = x1 + 16 >= x1 + 15 = a#(x1) a#(a(x1)) = x1 + 29 >= x1 + 11 = b#(x1) b#(b(x1)) = x1 + 20 >= x1 + 8 = c#(x1) b#(b(x1)) = x1 + 20 >= x1 + 14 = c#(c(x1)) b#(b(x1)) = x1 + 20 >= x1 + 20 = c#(c(c(x1))) a#(a(x1)) = x1 + 29 >= x1 + 20 = b#(b(x1)) a#(a(x1)) = x1 + 29 >= x1 + 29 = b#(b(b(x1))) a#(x1) = x1 + 15 >= x1 + 12 = c#(d(x1)) a(a(x1)) = x1 + 28 >= x1 + 27 = b(b(b(x1))) a(x1) = x1 + 14 >= x1 + 10 = c(d(x1)) b(b(x1)) = x1 + 18 >= x1 + 18 = c(c(c(x1))) c(c(x1)) = x1 + 12 >= x1 + 12 = d(d(d(x1))) e(d(x1)) = 9x1 + 37 >= 9x1 + 34 = a(b(c(d(e(x1))))) b(x1) = x1 + 9 >= x1 + 8 = d(d(x1)) e(c(x1)) = 9x1 + 55 >= 9x1 + 38 = b(a(a(e(x1)))) c(d(d(x1))) = x1 + 14 >= x1 + 14 = a(x1) problem: DPs: b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> b#(b(b(x1))) TRS: a(a(x1)) -> b(b(b(x1))) a(x1) -> c(d(x1)) b(b(x1)) -> c(c(c(x1))) c(c(x1)) -> d(d(d(x1))) e(d(x1)) -> a(b(c(d(e(x1))))) b(x1) -> d(d(x1)) e(c(x1)) -> b(a(a(e(x1)))) c(d(d(x1))) -> a(x1) EDG Processor: DPs: b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> b#(b(b(x1))) TRS: a(a(x1)) -> b(b(b(x1))) a(x1) -> c(d(x1)) b(b(x1)) -> c(c(c(x1))) c(c(x1)) -> d(d(d(x1))) e(d(x1)) -> a(b(c(d(e(x1))))) b(x1) -> d(d(x1)) e(c(x1)) -> b(a(a(e(x1)))) c(d(d(x1))) -> a(x1) graph: a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(c(c(x1))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/4