YES Problem: b(b(b(x1))) -> a(a(b(x1))) b(a(a(x1))) -> a(a(b(x1))) a(a(x1)) -> b(a(b(x1))) Proof: Arctic Interpretation Processor: dimension: 3 interpretation: [0 0 0 ] [a](x0) = [-& -& 0 ]x0 [1 2 -&] , [0 1 -&] [b](x0) = [0 1 -&]x0 [-& 0 -&] orientation: [2 3 -&] [2 3 -&] b(b(b(x1))) = [2 3 -&]x1 >= [2 3 -&]x1 = a(a(b(x1))) [1 2 -&] [1 2 -&] [2 3 0 ] [2 3 -&] b(a(a(x1))) = [2 3 0 ]x1 >= [2 3 -&]x1 = a(a(b(x1))) [1 2 -&] [1 2 -&] [1 2 0 ] [0 1 -&] a(a(x1)) = [1 2 -&]x1 >= [0 1 -&]x1 = b(a(b(x1))) [1 1 2 ] [-& 0 -&] problem: b(b(b(x1))) -> a(a(b(x1))) b(a(a(x1))) -> a(a(b(x1))) Arctic Interpretation Processor: dimension: 2 interpretation: [0 0] [a](x0) = [0 0]x0, [1 0] [b](x0) = [0 1]x0 orientation: [3 2] [1 1] b(b(b(x1))) = [2 3]x1 >= [1 1]x1 = a(a(b(x1))) [1 1] [1 1] b(a(a(x1))) = [1 1]x1 >= [1 1]x1 = a(a(b(x1))) problem: b(a(a(x1))) -> a(a(b(x1))) KBO Processor: weight function: w0 = 1 w(a) = w(b) = 1 precedence: b > a problem: Qed