YES Problem: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) Proof: DP Processor: DPs: b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(x1) -> c#(x1) b#(x1) -> c#(c(x1)) c#(d(x1)) -> a#(x1) c#(d(x1)) -> c#(a(x1)) c#(d(x1)) -> b#(c(a(x1))) c#(d(x1)) -> a#(b(c(a(x1)))) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> c#(b(a(x1))) a#(a(x1)) -> a#(c(b(a(x1)))) TRS: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) TDG Processor: DPs: b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(x1) -> c#(x1) b#(x1) -> c#(c(x1)) c#(d(x1)) -> a#(x1) c#(d(x1)) -> c#(a(x1)) c#(d(x1)) -> b#(c(a(x1))) c#(d(x1)) -> a#(b(c(a(x1)))) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> c#(b(a(x1))) a#(a(x1)) -> a#(c(b(a(x1)))) TRS: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) graph: a#(a(x1)) -> a#(c(b(a(x1)))) -> a#(a(x1)) -> a#(c(b(a(x1)))) a#(a(x1)) -> a#(c(b(a(x1)))) -> a#(a(x1)) -> c#(b(a(x1))) a#(a(x1)) -> a#(c(b(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> c#(b(a(x1))) -> c#(d(x1)) -> a#(b(c(a(x1)))) a#(a(x1)) -> c#(b(a(x1))) -> c#(d(x1)) -> b#(c(a(x1))) a#(a(x1)) -> c#(b(a(x1))) -> c#(d(x1)) -> c#(a(x1)) a#(a(x1)) -> c#(b(a(x1))) -> c#(d(x1)) -> a#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(x1) -> c#(c(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(x1) -> c#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> a#(b(c(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> b#(c(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> c#(x1) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> a#(c(b(a(x1)))) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> c#(b(a(x1))) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> a#(c(b(a(x1)))) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> c#(b(a(x1))) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> b#(a(x1)) c#(d(x1)) -> c#(a(x1)) -> c#(d(x1)) -> a#(b(c(a(x1)))) c#(d(x1)) -> c#(a(x1)) -> c#(d(x1)) -> b#(c(a(x1))) c#(d(x1)) -> c#(a(x1)) -> c#(d(x1)) -> c#(a(x1)) c#(d(x1)) -> c#(a(x1)) -> c#(d(x1)) -> a#(x1) c#(d(x1)) -> b#(c(a(x1))) -> b#(x1) -> c#(c(x1)) c#(d(x1)) -> b#(c(a(x1))) -> b#(x1) -> c#(x1) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> a#(b(c(x1))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> b#(c(x1)) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> a#(c(b(a(x1)))) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> c#(b(a(x1))) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) -> a#(a(x1)) -> a#(c(b(a(x1)))) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) -> a#(a(x1)) -> c#(b(a(x1))) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) -> a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> c#(x1) -> c#(d(x1)) -> a#(b(c(a(x1)))) b#(c(a(x1))) -> c#(x1) -> c#(d(x1)) -> b#(c(a(x1))) b#(c(a(x1))) -> c#(x1) -> c#(d(x1)) -> c#(a(x1)) b#(c(a(x1))) -> c#(x1) -> c#(d(x1)) -> a#(x1) b#(c(a(x1))) -> b#(c(x1)) -> b#(x1) -> c#(c(x1)) b#(c(a(x1))) -> b#(c(x1)) -> b#(x1) -> c#(x1) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(x1) -> c#(c(x1)) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(x1) -> c#(x1) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> c#(x1) b#(x1) -> c#(c(x1)) -> c#(d(x1)) -> a#(b(c(a(x1)))) b#(x1) -> c#(c(x1)) -> c#(d(x1)) -> b#(c(a(x1))) b#(x1) -> c#(c(x1)) -> c#(d(x1)) -> c#(a(x1)) b#(x1) -> c#(c(x1)) -> c#(d(x1)) -> a#(x1) b#(x1) -> c#(x1) -> c#(d(x1)) -> a#(b(c(a(x1)))) b#(x1) -> c#(x1) -> c#(d(x1)) -> b#(c(a(x1))) b#(x1) -> c#(x1) -> c#(d(x1)) -> c#(a(x1)) b#(x1) -> c#(x1) -> c#(d(x1)) -> a#(x1) EDG Processor: DPs: b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(x1) -> c#(x1) b#(x1) -> c#(c(x1)) c#(d(x1)) -> a#(x1) c#(d(x1)) -> c#(a(x1)) c#(d(x1)) -> b#(c(a(x1))) c#(d(x1)) -> a#(b(c(a(x1)))) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> c#(b(a(x1))) a#(a(x1)) -> a#(c(b(a(x1)))) TRS: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) graph: a#(a(x1)) -> a#(c(b(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(c(b(a(x1)))) -> a#(a(x1)) -> c#(b(a(x1))) a#(a(x1)) -> a#(c(b(a(x1)))) -> a#(a(x1)) -> a#(c(b(a(x1)))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> c#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> b#(c(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> a#(b(c(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) a#(a(x1)) -> b#(a(x1)) -> b#(x1) -> c#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(x1) -> c#(c(x1)) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> c#(b(a(x1))) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> a#(c(b(a(x1)))) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> b#(a(x1)) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> c#(b(a(x1))) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> a#(c(b(a(x1)))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> c#(x1) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> b#(c(x1)) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> a#(b(c(x1))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) c#(d(x1)) -> b#(c(a(x1))) -> b#(x1) -> c#(x1) c#(d(x1)) -> b#(c(a(x1))) -> b#(x1) -> c#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> c#(b(a(x1))) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> a#(c(b(a(x1)))) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) -> a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) -> a#(a(x1)) -> c#(b(a(x1))) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) -> a#(a(x1)) -> a#(c(b(a(x1)))) b#(c(a(x1))) -> c#(x1) -> c#(d(x1)) -> a#(x1) b#(c(a(x1))) -> c#(x1) -> c#(d(x1)) -> c#(a(x1)) b#(c(a(x1))) -> c#(x1) -> c#(d(x1)) -> b#(c(a(x1))) b#(c(a(x1))) -> c#(x1) -> c#(d(x1)) -> a#(b(c(a(x1)))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(c(a(x1))) -> b#(c(x1)) -> b#(x1) -> c#(x1) b#(c(a(x1))) -> b#(c(x1)) -> b#(x1) -> c#(c(x1)) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(x1) -> c#(x1) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(x1) -> c#(c(x1)) b#(x1) -> c#(x1) -> c#(d(x1)) -> a#(x1) b#(x1) -> c#(x1) -> c#(d(x1)) -> c#(a(x1)) b#(x1) -> c#(x1) -> c#(d(x1)) -> b#(c(a(x1))) b#(x1) -> c#(x1) -> c#(d(x1)) -> a#(b(c(a(x1)))) CDG Processor: DPs: b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(x1) -> c#(x1) b#(x1) -> c#(c(x1)) c#(d(x1)) -> a#(x1) c#(d(x1)) -> c#(a(x1)) c#(d(x1)) -> b#(c(a(x1))) c#(d(x1)) -> a#(b(c(a(x1)))) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> c#(b(a(x1))) a#(a(x1)) -> a#(c(b(a(x1)))) TRS: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) graph: a#(a(x1)) -> b#(a(x1)) -> b#(x1) -> c#(c(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(x1) -> c#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> a#(b(c(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> b#(c(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> c#(x1) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> a#(c(b(a(x1)))) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> c#(b(a(x1))) c#(d(x1)) -> a#(b(c(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> a#(c(b(a(x1)))) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> c#(b(a(x1))) c#(d(x1)) -> a#(x1) -> a#(a(x1)) -> b#(a(x1)) c#(d(x1)) -> b#(c(a(x1))) -> b#(x1) -> c#(c(x1)) c#(d(x1)) -> b#(c(a(x1))) -> b#(x1) -> c#(x1) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> a#(b(c(x1))) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> b#(c(x1)) c#(d(x1)) -> b#(c(a(x1))) -> b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> a#(c(b(a(x1)))) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> c#(b(a(x1))) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> b#(c(x1)) -> b#(x1) -> c#(c(x1)) b#(c(a(x1))) -> b#(c(x1)) -> b#(x1) -> c#(x1) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> c#(x1) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(x1) -> c#(c(x1)) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(x1) -> c#(x1) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> a#(b(a(b(c(x1))))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> b#(a(b(c(x1)))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> b#(a(b(c(x1)))) -> b#(c(a(x1))) -> c#(x1) SCC Processor: #sccs: 1 #rules: 4 #arcs: 37/196 DPs: a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> b#(a(b(c(x1)))) TRS: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) Arctic Interpretation Processor: dimension: 1 interpretation: [a#](x0) = 2x0 + 0, [b#](x0) = 2x0 + 0, [d](x0) = -16x0 + 12, [b](x0) = x0 + 14, [c](x0) = 14, [a](x0) = 0 orientation: a#(a(x1)) = 2 >= 2 = b#(a(x1)) b#(c(a(x1))) = 16 >= 16 = b#(c(x1)) b#(c(a(x1))) = 16 >= 16 = a#(b(c(x1))) b#(c(a(x1))) = 16 >= 2 = b#(a(b(c(x1)))) b(c(a(x1))) = 14 >= 0 = a(b(a(b(c(x1))))) b(x1) = x1 + 14 >= 14 = c(c(x1)) c(d(x1)) = 14 >= 0 = a(b(c(a(x1)))) a(a(x1)) = 0 >= 0 = a(c(b(a(x1)))) problem: DPs: a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) TRS: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) EDG Processor: DPs: a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) TRS: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) graph: a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> b#(c(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(c(a(x1))) -> a#(b(c(x1))) b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> b#(c(x1)) -> b#(c(a(x1))) -> a#(b(c(x1))) CDG Processor: DPs: a#(a(x1)) -> b#(a(x1)) b#(c(a(x1))) -> b#(c(x1)) b#(c(a(x1))) -> a#(b(c(x1))) TRS: b(c(a(x1))) -> a(b(a(b(c(x1))))) b(x1) -> c(c(x1)) c(d(x1)) -> a(b(c(a(x1)))) a(a(x1)) -> a(c(b(a(x1)))) graph: b#(c(a(x1))) -> a#(b(c(x1))) -> a#(a(x1)) -> b#(a(x1)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9