YES Problem: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) Proof: DP Processor: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) b#(b(x1)) -> a#(c(c(c(x1)))) c#(c(x1)) -> b#(x1) c#(c(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) TDG Processor: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) b#(b(x1)) -> a#(c(c(c(x1)))) c#(c(x1)) -> b#(x1) c#(c(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) graph: b#(b(x1)) -> c#(c(c(x1))) -> c#(c(x1)) -> a#(b(x1)) b#(b(x1)) -> c#(c(c(x1))) -> c#(c(x1)) -> b#(x1) b#(b(x1)) -> c#(c(x1)) -> c#(c(x1)) -> a#(b(x1)) b#(b(x1)) -> c#(c(x1)) -> c#(c(x1)) -> b#(x1) b#(b(x1)) -> c#(x1) -> c#(c(x1)) -> a#(b(x1)) b#(b(x1)) -> c#(x1) -> c#(c(x1)) -> b#(x1) b#(b(x1)) -> a#(c(c(c(x1)))) -> a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> a#(c(c(c(x1)))) -> a#(a(x1)) -> c#(x1) c#(c(x1)) -> b#(x1) -> b#(b(x1)) -> a#(c(c(c(x1)))) c#(c(x1)) -> b#(x1) -> b#(b(x1)) -> c#(c(c(x1))) c#(c(x1)) -> b#(x1) -> b#(b(x1)) -> c#(c(x1)) c#(c(x1)) -> b#(x1) -> b#(b(x1)) -> c#(x1) c#(c(x1)) -> a#(b(x1)) -> a#(a(x1)) -> b#(c(x1)) c#(c(x1)) -> a#(b(x1)) -> a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> a#(c(c(c(x1)))) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(c(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(x1) a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> a#(b(x1)) a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> b#(x1) Arctic Interpretation Processor: dimension: 2 usable rules: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) interpretation: [b#](x0) = [-& 0 ]x0 + [2], [c#](x0) = [1 -1]x0, [a#](x0) = [-& 0 ]x0 + [2], [-& -2] [0] [b](x0) = [1 1 ]x0 + [3], [0 0 ] [2] [c](x0) = [0 -&]x0 + [0], [-4 -1] [1] [a](x0) = [2 -1]x0 + [1] orientation: a#(a(x1)) = [2 -1]x1 + [2] >= [1 -1]x1 = c#(x1) a#(a(x1)) = [2 -1]x1 + [2] >= [0 -&]x1 + [2] = b#(c(x1)) b#(b(x1)) = [1 1]x1 + [3] >= [1 -1]x1 = c#(x1) b#(b(x1)) = [1 1]x1 + [3] >= [1 1]x1 + [3] = c#(c(x1)) b#(b(x1)) = [1 1]x1 + [3] >= [1 1]x1 + [3] = c#(c(c(x1))) b#(b(x1)) = [1 1]x1 + [3] >= [0 0]x1 + [2] = a#(c(c(c(x1)))) c#(c(x1)) = [1 1]x1 + [3] >= [-& 0 ]x1 + [2] = b#(x1) c#(c(x1)) = [1 1]x1 + [3] >= [1 1]x1 + [3] = a#(b(x1)) [1 -2] [1] [-2 -&] [0] a(a(x1)) = [1 1 ]x1 + [3] >= [1 1 ]x1 + [3] = b(c(x1)) [-1 -1] [1] [-1 -1] [1] b(b(x1)) = [2 2 ]x1 + [4] >= [2 2 ]x1 + [4] = a(c(c(c(x1)))) [0 0] [2] [0 0] [2] c(c(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = a(b(x1)) problem: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) c#(c(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) Restore Modifier: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) c#(c(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) EDG Processor: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) c#(c(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) graph: b#(b(x1)) -> c#(c(c(x1))) -> c#(c(x1)) -> a#(b(x1)) b#(b(x1)) -> c#(c(x1)) -> c#(c(x1)) -> a#(b(x1)) b#(b(x1)) -> c#(x1) -> c#(c(x1)) -> a#(b(x1)) c#(c(x1)) -> a#(b(x1)) -> a#(a(x1)) -> c#(x1) c#(c(x1)) -> a#(b(x1)) -> a#(a(x1)) -> b#(c(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(c(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> a#(b(x1)) Arctic Interpretation Processor: dimension: 2 usable rules: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) interpretation: [b#](x0) = [-1 0 ]x0 + [0], [c#](x0) = [0 -&]x0 + [2], [a#](x0) = [-& 1 ]x0 + [0], [1 -&] [3] [b](x0) = [-2 -&]x0 + [0], [0 -&] [2] [c](x0) = [0 -&]x0 + [1], [-1 2 ] [1] [a](x0) = [-1 -&]x0 + [1] orientation: a#(a(x1)) = [0 -&]x1 + [2] >= [0 -&]x1 + [2] = c#(x1) a#(a(x1)) = [0 -&]x1 + [2] >= [0 -&]x1 + [1] = b#(c(x1)) b#(b(x1)) = [0 -&]x1 + [2] >= [0 -&]x1 + [2] = c#(x1) b#(b(x1)) = [0 -&]x1 + [2] >= [0 -&]x1 + [2] = c#(c(x1)) b#(b(x1)) = [0 -&]x1 + [2] >= [0 -&]x1 + [2] = c#(c(c(x1))) c#(c(x1)) = [0 -&]x1 + [2] >= [-1 -&]x1 + [1] = a#(b(x1)) [1 1 ] [3] [1 -&] [3] a(a(x1)) = [-2 1 ]x1 + [1] >= [-2 -&]x1 + [0] = b(c(x1)) [2 -&] [4] [2 -&] [4] b(b(x1)) = [-1 -&]x1 + [1] >= [-1 -&]x1 + [1] = a(c(c(c(x1)))) [0 -&] [2] [0 -&] [2] c(c(x1)) = [0 -&]x1 + [2] >= [0 -&]x1 + [2] = a(b(x1)) problem: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) Restore Modifier: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) EDG Processor: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> c#(x1) b#(b(x1)) -> c#(c(x1)) b#(b(x1)) -> c#(c(c(x1))) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> a(c(c(c(x1)))) c(c(x1)) -> a(b(x1)) graph: a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(c(c(x1))) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(c(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(x1) SCC Processor: #sccs: 0 #rules: 0 #arcs: 3/25