YES Problem: c(c(c(a(x1)))) -> d(d(x1)) d(b(x1)) -> c(c(x1)) c(x1) -> a(a(a(a(x1)))) d(x1) -> b(b(b(b(x1)))) b(d(x1)) -> c(c(x1)) a(c(c(c(x1)))) -> d(d(x1)) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [b](x0) = 2x0, [d](x0) = 8x0, [c](x0) = 5x0, [a](x0) = 1x0 orientation: c(c(c(a(x1)))) = 16x1 >= 16x1 = d(d(x1)) d(b(x1)) = 10x1 >= 10x1 = c(c(x1)) c(x1) = 5x1 >= 4x1 = a(a(a(a(x1)))) d(x1) = 8x1 >= 8x1 = b(b(b(b(x1)))) b(d(x1)) = 10x1 >= 10x1 = c(c(x1)) a(c(c(c(x1)))) = 16x1 >= 16x1 = d(d(x1)) problem: c(c(c(a(x1)))) -> d(d(x1)) d(b(x1)) -> c(c(x1)) d(x1) -> b(b(b(b(x1)))) b(d(x1)) -> c(c(x1)) a(c(c(c(x1)))) -> d(d(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [b](x0) = x0, [d](x0) = x0, [c](x0) = x0, [a](x0) = 9x0 orientation: c(c(c(a(x1)))) = 9x1 >= x1 = d(d(x1)) d(b(x1)) = x1 >= x1 = c(c(x1)) d(x1) = x1 >= x1 = b(b(b(b(x1)))) b(d(x1)) = x1 >= x1 = c(c(x1)) a(c(c(c(x1)))) = 9x1 >= x1 = d(d(x1)) problem: d(b(x1)) -> c(c(x1)) d(x1) -> b(b(b(b(x1)))) b(d(x1)) -> c(c(x1)) Arctic Interpretation Processor: dimension: 2 interpretation: [0 0] [b](x0) = [0 0]x0, [0 3] [d](x0) = [2 0]x0, [1 1] [c](x0) = [0 0]x0 orientation: [3 3] [2 2] d(b(x1)) = [2 2]x1 >= [1 1]x1 = c(c(x1)) [0 3] [0 0] d(x1) = [2 0]x1 >= [0 0]x1 = b(b(b(b(x1)))) [2 3] [2 2] b(d(x1)) = [2 3]x1 >= [1 1]x1 = c(c(x1)) problem: d(x1) -> b(b(b(b(x1)))) b(d(x1)) -> c(c(x1)) Arctic Interpretation Processor: dimension: 2 interpretation: [0 0] [b](x0) = [0 0]x0, [2 1] [d](x0) = [3 3]x0, [0 0] [c](x0) = [2 1]x0 orientation: [2 1] [0 0] d(x1) = [3 3]x1 >= [0 0]x1 = b(b(b(b(x1)))) [3 3] [2 1] b(d(x1)) = [3 3]x1 >= [3 2]x1 = c(c(x1)) problem: b(d(x1)) -> c(c(x1)) Arctic Interpretation Processor: dimension: 3 interpretation: [0 -& 0 ] [b](x0) = [0 0 0 ]x0 [0 1 -&] , [0 0 3 ] [d](x0) = [-& 0 1 ]x0 [1 3 0 ] , [0 0 0 ] [c](x0) = [-& 0 2 ]x0 [-& 0 0 ] orientation: [1 3 3] [0 0 2 ] b(d(x1)) = [1 3 3]x1 >= [-& 2 2 ]x1 = c(c(x1)) [0 1 3] [-& 0 2 ] problem: Qed