YES Problem: f(f(x1)) -> b(b(b(x1))) a(f(x1)) -> f(a(a(x1))) b(b(x1)) -> c(c(a(c(x1)))) d(b(x1)) -> d(a(b(x1))) c(c(x1)) -> d(d(d(x1))) b(d(x1)) -> d(b(x1)) c(d(d(x1))) -> f(x1) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [d](x0) = 4x0, [c](x0) = 6x0, [a](x0) = x0, [b](x0) = 9x0, [f](x0) = 14x0 orientation: f(f(x1)) = 28x1 >= 27x1 = b(b(b(x1))) a(f(x1)) = 14x1 >= 14x1 = f(a(a(x1))) b(b(x1)) = 18x1 >= 18x1 = c(c(a(c(x1)))) d(b(x1)) = 13x1 >= 13x1 = d(a(b(x1))) c(c(x1)) = 12x1 >= 12x1 = d(d(d(x1))) b(d(x1)) = 13x1 >= 13x1 = d(b(x1)) c(d(d(x1))) = 14x1 >= 14x1 = f(x1) problem: a(f(x1)) -> f(a(a(x1))) b(b(x1)) -> c(c(a(c(x1)))) d(b(x1)) -> d(a(b(x1))) c(c(x1)) -> d(d(d(x1))) b(d(x1)) -> d(b(x1)) c(d(d(x1))) -> f(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [d](x0) = x0, [c](x0) = 8x0, [a](x0) = x0, [b](x0) = 13x0, [f](x0) = x0 orientation: a(f(x1)) = x1 >= x1 = f(a(a(x1))) b(b(x1)) = 26x1 >= 24x1 = c(c(a(c(x1)))) d(b(x1)) = 13x1 >= 13x1 = d(a(b(x1))) c(c(x1)) = 16x1 >= x1 = d(d(d(x1))) b(d(x1)) = 13x1 >= 13x1 = d(b(x1)) c(d(d(x1))) = 8x1 >= x1 = f(x1) problem: a(f(x1)) -> f(a(a(x1))) d(b(x1)) -> d(a(b(x1))) b(d(x1)) -> d(b(x1)) Arctic Interpretation Processor: dimension: 2 interpretation: [0 1] [d](x0) = [1 2]x0, [0 0 ] [a](x0) = [-& -&]x0, [0 1] [b](x0) = [0 1]x0, [0 0 ] [f](x0) = [-& 0 ]x0 orientation: [0 0 ] [0 0 ] a(f(x1)) = [-& -&]x1 >= [-& -&]x1 = f(a(a(x1))) [1 2] [0 1] d(b(x1)) = [2 3]x1 >= [1 2]x1 = d(a(b(x1))) [2 3] [1 2] b(d(x1)) = [2 3]x1 >= [2 3]x1 = d(b(x1)) problem: a(f(x1)) -> f(a(a(x1))) b(d(x1)) -> d(b(x1)) KBO Processor: weight function: w0 = 1 w(d) = w(b) = w(f) = 1 w(a) = 0 precedence: a > b > d ~ f problem: Qed