YES Problem: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) Proof: DP Processor: DPs: a#(x1) -> g#(d(x1)) b#(b(b(x1))) -> c#(x1) b#(b(b(x1))) -> c#(d(c(x1))) b#(b(x1)) -> g#(x1) b#(b(x1)) -> g#(g(x1)) b#(b(x1)) -> a#(g(g(x1))) c#(d(x1)) -> g#(x1) c#(d(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) g#(g(g(x1))) -> b#(b(x1)) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) TDG Processor: DPs: a#(x1) -> g#(d(x1)) b#(b(b(x1))) -> c#(x1) b#(b(b(x1))) -> c#(d(c(x1))) b#(b(x1)) -> g#(x1) b#(b(x1)) -> g#(g(x1)) b#(b(x1)) -> a#(g(g(x1))) c#(d(x1)) -> g#(x1) c#(d(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) g#(g(g(x1))) -> b#(b(x1)) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) graph: c#(d(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(b(x1)) c#(d(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(x1) c#(d(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(b(x1)) c#(d(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(x1) b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(g(x1)) b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(x1) b#(b(b(x1))) -> c#(x1) -> c#(d(x1)) -> g#(g(x1)) b#(b(b(x1))) -> c#(x1) -> c#(d(x1)) -> g#(x1) b#(b(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> a#(g(g(x1))) -> a#(x1) -> g#(d(x1)) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> a#(g(g(x1))) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> g#(x1) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(b(x1))) -> c#(d(c(x1))) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(b(x1))) -> c#(x1) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> a#(g(g(x1))) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> g#(x1) g#(g(g(x1))) -> b#(x1) -> b#(b(b(x1))) -> c#(d(c(x1))) g#(g(g(x1))) -> b#(x1) -> b#(b(b(x1))) -> c#(x1) a#(x1) -> g#(d(x1)) -> g#(g(g(x1))) -> b#(b(x1)) a#(x1) -> g#(d(x1)) -> g#(g(g(x1))) -> b#(x1) EDG Processor: DPs: a#(x1) -> g#(d(x1)) b#(b(b(x1))) -> c#(x1) b#(b(b(x1))) -> c#(d(c(x1))) b#(b(x1)) -> g#(x1) b#(b(x1)) -> g#(g(x1)) b#(b(x1)) -> a#(g(g(x1))) c#(d(x1)) -> g#(x1) c#(d(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) g#(g(g(x1))) -> b#(b(x1)) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) graph: c#(d(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(x1) c#(d(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(b(x1)) c#(d(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(x1) c#(d(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(x1) b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(g(x1)) b#(b(b(x1))) -> c#(x1) -> c#(d(x1)) -> g#(x1) b#(b(b(x1))) -> c#(x1) -> c#(d(x1)) -> g#(g(x1)) b#(b(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> a#(g(g(x1))) -> a#(x1) -> g#(d(x1)) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(b(x1))) -> c#(x1) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(b(x1))) -> c#(d(c(x1))) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> g#(x1) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> a#(g(g(x1))) g#(g(g(x1))) -> b#(x1) -> b#(b(b(x1))) -> c#(x1) g#(g(g(x1))) -> b#(x1) -> b#(b(b(x1))) -> c#(d(c(x1))) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> g#(x1) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> a#(g(g(x1))) SCC Processor: #sccs: 1 #rules: 8 #arcs: 23/100 DPs: c#(d(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> g#(x1) b#(b(b(x1))) -> c#(d(c(x1))) c#(d(x1)) -> g#(x1) b#(b(b(x1))) -> c#(x1) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [c#](x0) = 4x0, [b#](x0) = 1x0, [g#](x0) = x0, [c](x0) = 9x0, [b](x0) = 6x0, [g](x0) = 4x0, [d](x0) = x0, [a](x0) = 4x0 orientation: c#(d(x1)) = 4x1 >= 4x1 = g#(g(x1)) g#(g(g(x1))) = 8x1 >= 7x1 = b#(b(x1)) b#(b(x1)) = 7x1 >= 4x1 = g#(g(x1)) g#(g(g(x1))) = 8x1 >= 1x1 = b#(x1) b#(b(x1)) = 7x1 >= x1 = g#(x1) b#(b(b(x1))) = 13x1 >= 13x1 = c#(d(c(x1))) c#(d(x1)) = 4x1 >= x1 = g#(x1) b#(b(b(x1))) = 13x1 >= 4x1 = c#(x1) a(x1) = 4x1 >= 4x1 = g(d(x1)) b(b(b(x1))) = 18x1 >= 18x1 = c(d(c(x1))) b(b(x1)) = 12x1 >= 12x1 = a(g(g(x1))) c(d(x1)) = 9x1 >= 8x1 = g(g(x1)) g(g(g(x1))) = 12x1 >= 12x1 = b(b(x1)) problem: DPs: c#(d(x1)) -> g#(g(x1)) b#(b(b(x1))) -> c#(d(c(x1))) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) EDG Processor: DPs: c#(d(x1)) -> g#(g(x1)) b#(b(b(x1))) -> c#(d(c(x1))) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) graph: b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(g(x1)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/4