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