YES Problem: a(a(b(b(x1)))) -> C(C(x1)) b(b(c(c(x1)))) -> A(A(x1)) c(c(a(a(x1)))) -> B(B(x1)) A(A(C(C(x1)))) -> b(b(x1)) C(C(B(B(x1)))) -> a(a(x1)) B(B(A(A(x1)))) -> c(c(x1)) a(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A(A(A(A(A(A(x1)))))) A(A(A(A(A(A(A(A(x1)))))))) -> a(a(a(a(a(a(a(a(x1)))))))) b(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B(B(B(B(B(B(x1)))))) B(B(B(B(B(B(B(B(x1)))))))) -> b(b(b(b(b(b(b(b(x1)))))))) c(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C(C(C(C(C(C(x1)))))) C(C(C(C(C(C(C(C(x1)))))))) -> c(c(c(c(c(c(c(c(x1)))))))) B(B(a(a(a(a(a(a(a(a(x1)))))))))) -> c(c(A(A(A(A(A(A(x1)))))))) A(A(A(A(A(A(b(b(x1)))))))) -> a(a(a(a(a(a(a(a(C(C(x1)))))))))) C(C(b(b(b(b(b(b(b(b(x1)))))))))) -> a(a(B(B(B(B(B(B(x1)))))))) B(B(B(B(B(B(c(c(x1)))))))) -> b(b(b(b(b(b(b(b(A(A(x1)))))))))) A(A(c(c(c(c(c(c(c(c(x1)))))))))) -> b(b(C(C(C(C(C(C(x1)))))))) C(C(C(C(C(C(a(a(x1)))))))) -> c(c(c(c(c(c(c(c(B(B(x1)))))))))) a(a(A(A(x1)))) -> x1 A(A(a(a(x1)))) -> x1 b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 c(c(C(C(x1)))) -> x1 C(C(c(c(x1)))) -> x1 Proof: DP Processor: DPs: a#(a(b(b(x1)))) -> C#(x1) a#(a(b(b(x1)))) -> C#(C(x1)) b#(b(c(c(x1)))) -> A#(x1) b#(b(c(c(x1)))) -> A#(A(x1)) c#(c(a(a(x1)))) -> B#(x1) c#(c(a(a(x1)))) -> B#(B(x1)) A#(A(C(C(x1)))) -> b#(x1) A#(A(C(C(x1)))) -> b#(b(x1)) C#(C(B(B(x1)))) -> a#(x1) C#(C(B(B(x1)))) -> a#(a(x1)) B#(B(A(A(x1)))) -> c#(x1) B#(B(A(A(x1)))) -> c#(c(x1)) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(x1) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(x1)) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(x1))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(x1)))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(A(x1))))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(A(A(x1)))))) A#(A(A(A(A(A(A(A(x1)))))))) -> a#(x1) A#(A(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) A#(A(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) A#(A(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) A#(A(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) A#(A(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) A#(A(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) A#(A(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(x1) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(x1)) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(B(x1))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(B(B(x1)))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(B(B(B(x1))))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(B(B(B(B(x1)))))) B#(B(B(B(B(B(B(B(x1)))))))) -> b#(x1) B#(B(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) B#(B(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) B#(B(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) B#(B(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) B#(B(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) B#(B(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) B#(B(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(x1) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(x1)) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(C(x1))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(C(C(x1)))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(C(C(C(x1))))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(C(C(C(C(x1)))))) C#(C(C(C(C(C(C(C(x1)))))))) -> c#(x1) C#(C(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) C#(C(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) C#(C(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) C#(C(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) C#(C(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) C#(C(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) C#(C(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(x1) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(x1)) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(x1))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(x1)))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(A(x1))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(A(A(x1)))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) -> c#(A(A(A(A(A(A(x1))))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) -> c#(c(A(A(A(A(A(A(x1)))))))) A#(A(A(A(A(A(b(b(x1)))))))) -> C#(x1) A#(A(A(A(A(A(b(b(x1)))))))) -> C#(C(x1)) A#(A(A(A(A(A(b(b(x1)))))))) -> a#(C(C(x1))) A#(A(A(A(A(A(b(b(x1)))))))) -> a#(a(C(C(x1)))) A#(A(A(A(A(A(b(b(x1)))))))) -> a#(a(a(C(C(x1))))) A#(A(A(A(A(A(b(b(x1)))))))) -> a#(a(a(a(C(C(x1)))))) A#(A(A(A(A(A(b(b(x1)))))))) -> a#(a(a(a(a(C(C(x1))))))) A#(A(A(A(A(A(b(b(x1)))))))) -> a#(a(a(a(a(a(C(C(x1)))))))) A#(A(A(A(A(A(b(b(x1)))))))) -> a#(a(a(a(a(a(a(C(C(x1))))))))) A#(A(A(A(A(A(b(b(x1)))))))) -> a#(a(a(a(a(a(a(a(C(C(x1)))))))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(x1) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(x1)) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(B(x1))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(B(B(x1)))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(B(B(B(x1))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) -> B#(B(B(B(B(B(x1)))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) -> a#(B(B(B(B(B(B(x1))))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) -> a#(a(B(B(B(B(B(B(x1)))))))) B#(B(B(B(B(B(c(c(x1)))))))) -> A#(x1) B#(B(B(B(B(B(c(c(x1)))))))) -> A#(A(x1)) B#(B(B(B(B(B(c(c(x1)))))))) -> b#(A(A(x1))) B#(B(B(B(B(B(c(c(x1)))))))) -> b#(b(A(A(x1)))) B#(B(B(B(B(B(c(c(x1)))))))) -> b#(b(b(A(A(x1))))) B#(B(B(B(B(B(c(c(x1)))))))) -> b#(b(b(b(A(A(x1)))))) B#(B(B(B(B(B(c(c(x1)))))))) -> b#(b(b(b(b(A(A(x1))))))) B#(B(B(B(B(B(c(c(x1)))))))) -> b#(b(b(b(b(b(A(A(x1)))))))) B#(B(B(B(B(B(c(c(x1)))))))) -> b#(b(b(b(b(b(b(A(A(x1))))))))) B#(B(B(B(B(B(c(c(x1)))))))) -> b#(b(b(b(b(b(b(b(A(A(x1)))))))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(x1) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(x1)) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(C(x1))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(C(C(x1)))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(C(C(C(x1))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> C#(C(C(C(C(C(x1)))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> b#(C(C(C(C(C(C(x1))))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> b#(b(C(C(C(C(C(C(x1)))))))) C#(C(C(C(C(C(a(a(x1)))))))) -> B#(x1) C#(C(C(C(C(C(a(a(x1)))))))) -> B#(B(x1)) C#(C(C(C(C(C(a(a(x1)))))))) -> c#(B(B(x1))) C#(C(C(C(C(C(a(a(x1)))))))) -> c#(c(B(B(x1)))) C#(C(C(C(C(C(a(a(x1)))))))) -> c#(c(c(B(B(x1))))) C#(C(C(C(C(C(a(a(x1)))))))) -> c#(c(c(c(B(B(x1)))))) C#(C(C(C(C(C(a(a(x1)))))))) -> c#(c(c(c(c(B(B(x1))))))) C#(C(C(C(C(C(a(a(x1)))))))) -> c#(c(c(c(c(c(B(B(x1)))))))) C#(C(C(C(C(C(a(a(x1)))))))) -> c#(c(c(c(c(c(c(B(B(x1))))))))) C#(C(C(C(C(C(a(a(x1)))))))) -> c#(c(c(c(c(c(c(c(B(B(x1)))))))))) TRS: a(a(b(b(x1)))) -> C(C(x1)) b(b(c(c(x1)))) -> A(A(x1)) c(c(a(a(x1)))) -> B(B(x1)) A(A(C(C(x1)))) -> b(b(x1)) C(C(B(B(x1)))) -> a(a(x1)) B(B(A(A(x1)))) -> c(c(x1)) a(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A(A(A(A(A(A(x1)))))) A(A(A(A(A(A(A(A(x1)))))))) -> a(a(a(a(a(a(a(a(x1)))))))) b(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B(B(B(B(B(B(x1)))))) B(B(B(B(B(B(B(B(x1)))))))) -> b(b(b(b(b(b(b(b(x1)))))))) c(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C(C(C(C(C(C(x1)))))) C(C(C(C(C(C(C(C(x1)))))))) -> c(c(c(c(c(c(c(c(x1)))))))) B(B(a(a(a(a(a(a(a(a(x1)))))))))) -> c(c(A(A(A(A(A(A(x1)))))))) A(A(A(A(A(A(b(b(x1)))))))) -> a(a(a(a(a(a(a(a(C(C(x1)))))))))) C(C(b(b(b(b(b(b(b(b(x1)))))))))) -> a(a(B(B(B(B(B(B(x1)))))))) B(B(B(B(B(B(c(c(x1)))))))) -> b(b(b(b(b(b(b(b(A(A(x1)))))))))) A(A(c(c(c(c(c(c(c(c(x1)))))))))) -> b(b(C(C(C(C(C(C(x1)))))))) C(C(C(C(C(C(a(a(x1)))))))) -> c(c(c(c(c(c(c(c(B(B(x1)))))))))) a(a(A(A(x1)))) -> x1 A(A(a(a(x1)))) -> x1 b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 c(c(C(C(x1)))) -> x1 C(C(c(c(x1)))) -> x1 Matrix Interpretation Processor: dim=1 interpretation: [B#](x0) = x0 + 2, [c#](x0) = x0, [A#](x0) = x0 + 2, [b#](x0) = x0, [C#](x0) = x0 + 2, [a#](x0) = x0, [B](x0) = x0 + 3, [A](x0) = x0 + 3, [c](x0) = x0 + 2, [C](x0) = x0 + 3, [a](x0) = x0 + 2, [b](x0) = x0 + 2 orientation: a#(a(b(b(x1)))) = x1 + 6 >= x1 + 2 = C#(x1) a#(a(b(b(x1)))) = x1 + 6 >= x1 + 5 = C#(C(x1)) b#(b(c(c(x1)))) = x1 + 6 >= x1 + 2 = A#(x1) b#(b(c(c(x1)))) = x1 + 6 >= x1 + 5 = A#(A(x1)) c#(c(a(a(x1)))) = x1 + 6 >= x1 + 2 = B#(x1) c#(c(a(a(x1)))) = x1 + 6 >= x1 + 5 = B#(B(x1)) A#(A(C(C(x1)))) = x1 + 11 >= x1 = b#(x1) A#(A(C(C(x1)))) = x1 + 11 >= x1 + 2 = b#(b(x1)) C#(C(B(B(x1)))) = x1 + 11 >= x1 = a#(x1) C#(C(B(B(x1)))) = x1 + 11 >= x1 + 2 = a#(a(x1)) B#(B(A(A(x1)))) = x1 + 11 >= x1 = c#(x1) B#(B(A(A(x1)))) = x1 + 11 >= x1 + 2 = c#(c(x1)) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 18 >= x1 + 2 = A#(x1) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 18 >= x1 + 5 = A#(A(x1)) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 18 >= x1 + 8 = A#(A(A(x1))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 18 >= x1 + 11 = A#(A(A(A(x1)))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 18 >= x1 + 14 = A#(A(A(A(A(x1))))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 18 >= x1 + 17 = A#(A(A(A(A(A(x1)))))) A#(A(A(A(A(A(A(A(x1)))))))) = x1 + 23 >= x1 = a#(x1) A#(A(A(A(A(A(A(A(x1)))))))) = x1 + 23 >= x1 + 2 = a#(a(x1)) A#(A(A(A(A(A(A(A(x1)))))))) = x1 + 23 >= x1 + 4 = a#(a(a(x1))) A#(A(A(A(A(A(A(A(x1)))))))) = x1 + 23 >= x1 + 6 = a#(a(a(a(x1)))) A#(A(A(A(A(A(A(A(x1)))))))) = x1 + 23 >= x1 + 8 = a#(a(a(a(a(x1))))) A#(A(A(A(A(A(A(A(x1)))))))) = x1 + 23 >= x1 + 10 = a#(a(a(a(a(a(x1)))))) A#(A(A(A(A(A(A(A(x1)))))))) = x1 + 23 >= x1 + 12 = a#(a(a(a(a(a(a(x1))))))) A#(A(A(A(A(A(A(A(x1)))))))) = x1 + 23 >= x1 + 14 = a#(a(a(a(a(a(a(a(x1)))))))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 18 >= x1 + 2 = B#(x1) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 18 >= x1 + 5 = B#(B(x1)) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 18 >= x1 + 8 = B#(B(B(x1))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 18 >= x1 + 11 = B#(B(B(B(x1)))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 18 >= x1 + 14 = B#(B(B(B(B(x1))))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 18 >= x1 + 17 = B#(B(B(B(B(B(x1)))))) B#(B(B(B(B(B(B(B(x1)))))))) = x1 + 23 >= x1 = b#(x1) B#(B(B(B(B(B(B(B(x1)))))))) = x1 + 23 >= x1 + 2 = b#(b(x1)) B#(B(B(B(B(B(B(B(x1)))))))) = x1 + 23 >= x1 + 4 = b#(b(b(x1))) B#(B(B(B(B(B(B(B(x1)))))))) = x1 + 23 >= x1 + 6 = b#(b(b(b(x1)))) B#(B(B(B(B(B(B(B(x1)))))))) = x1 + 23 >= x1 + 8 = b#(b(b(b(b(x1))))) B#(B(B(B(B(B(B(B(x1)))))))) = x1 + 23 >= x1 + 10 = b#(b(b(b(b(b(x1)))))) B#(B(B(B(B(B(B(B(x1)))))))) = x1 + 23 >= x1 + 12 = b#(b(b(b(b(b(b(x1))))))) B#(B(B(B(B(B(B(B(x1)))))))) = x1 + 23 >= x1 + 14 = b#(b(b(b(b(b(b(b(x1)))))))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 18 >= x1 + 2 = C#(x1) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 18 >= x1 + 5 = C#(C(x1)) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 18 >= x1 + 8 = C#(C(C(x1))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 18 >= x1 + 11 = C#(C(C(C(x1)))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 18 >= x1 + 14 = C#(C(C(C(C(x1))))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 18 >= x1 + 17 = C#(C(C(C(C(C(x1)))))) C#(C(C(C(C(C(C(C(x1)))))))) = x1 + 23 >= x1 = c#(x1) C#(C(C(C(C(C(C(C(x1)))))))) = x1 + 23 >= x1 + 2 = c#(c(x1)) C#(C(C(C(C(C(C(C(x1)))))))) = x1 + 23 >= x1 + 4 = c#(c(c(x1))) C#(C(C(C(C(C(C(C(x1)))))))) = x1 + 23 >= x1 + 6 = c#(c(c(c(x1)))) C#(C(C(C(C(C(C(C(x1)))))))) = x1 + 23 >= x1 + 8 = c#(c(c(c(c(x1))))) C#(C(C(C(C(C(C(C(x1)))))))) = x1 + 23 >= x1 + 10 = c#(c(c(c(c(c(x1)))))) C#(C(C(C(C(C(C(C(x1)))))))) = x1 + 23 >= x1 + 12 = c#(c(c(c(c(c(c(x1))))))) C#(C(C(C(C(C(C(C(x1)))))))) = x1 + 23 >= x1 + 14 = c#(c(c(c(c(c(c(c(x1)))))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 21 >= x1 + 2 = A#(x1) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 21 >= x1 + 5 = A#(A(x1)) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 21 >= x1 + 8 = A#(A(A(x1))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 21 >= x1 + 11 = A#(A(A(A(x1)))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 21 >= x1 + 14 = A#(A(A(A(A(x1))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 21 >= x1 + 17 = A#(A(A(A(A(A(x1)))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 21 >= x1 + 18 = c#(A(A(A(A(A(A(x1))))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 21 >= x1 + 20 = c#(c(A(A(A(A(A(A(x1)))))))) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 2 = C#(x1) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 5 = C#(C(x1)) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 6 = a#(C(C(x1))) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 8 = a#(a(C(C(x1)))) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 10 = a#(a(a(C(C(x1))))) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 12 = a#(a(a(a(C(C(x1)))))) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 14 = a#(a(a(a(a(C(C(x1))))))) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 16 = a#(a(a(a(a(a(C(C(x1)))))))) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 18 = a#(a(a(a(a(a(a(C(C(x1))))))))) A#(A(A(A(A(A(b(b(x1)))))))) = x1 + 21 >= x1 + 20 = a#(a(a(a(a(a(a(a(C(C(x1)))))))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 21 >= x1 + 2 = B#(x1) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 21 >= x1 + 5 = B#(B(x1)) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 21 >= x1 + 8 = B#(B(B(x1))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 21 >= x1 + 11 = B#(B(B(B(x1)))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 21 >= x1 + 14 = B#(B(B(B(B(x1))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 21 >= x1 + 17 = B#(B(B(B(B(B(x1)))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 21 >= x1 + 18 = a#(B(B(B(B(B(B(x1))))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 21 >= x1 + 20 = a#(a(B(B(B(B(B(B(x1)))))))) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 2 = A#(x1) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 5 = A#(A(x1)) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 6 = b#(A(A(x1))) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 8 = b#(b(A(A(x1)))) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 10 = b#(b(b(A(A(x1))))) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 12 = b#(b(b(b(A(A(x1)))))) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 14 = b#(b(b(b(b(A(A(x1))))))) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 16 = b#(b(b(b(b(b(A(A(x1)))))))) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 18 = b#(b(b(b(b(b(b(A(A(x1))))))))) B#(B(B(B(B(B(c(c(x1)))))))) = x1 + 21 >= x1 + 20 = b#(b(b(b(b(b(b(b(A(A(x1)))))))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 21 >= x1 + 2 = C#(x1) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 21 >= x1 + 5 = C#(C(x1)) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 21 >= x1 + 8 = C#(C(C(x1))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 21 >= x1 + 11 = C#(C(C(C(x1)))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 21 >= x1 + 14 = C#(C(C(C(C(x1))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 21 >= x1 + 17 = C#(C(C(C(C(C(x1)))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 21 >= x1 + 18 = b#(C(C(C(C(C(C(x1))))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 21 >= x1 + 20 = b#(b(C(C(C(C(C(C(x1)))))))) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 2 = B#(x1) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 5 = B#(B(x1)) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 6 = c#(B(B(x1))) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 8 = c#(c(B(B(x1)))) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 10 = c#(c(c(B(B(x1))))) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 12 = c#(c(c(c(B(B(x1)))))) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 14 = c#(c(c(c(c(B(B(x1))))))) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 16 = c#(c(c(c(c(c(B(B(x1)))))))) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 18 = c#(c(c(c(c(c(c(B(B(x1))))))))) C#(C(C(C(C(C(a(a(x1)))))))) = x1 + 21 >= x1 + 20 = c#(c(c(c(c(c(c(c(B(B(x1)))))))))) a(a(b(b(x1)))) = x1 + 8 >= x1 + 6 = C(C(x1)) b(b(c(c(x1)))) = x1 + 8 >= x1 + 6 = A(A(x1)) c(c(a(a(x1)))) = x1 + 8 >= x1 + 6 = B(B(x1)) A(A(C(C(x1)))) = x1 + 12 >= x1 + 4 = b(b(x1)) C(C(B(B(x1)))) = x1 + 12 >= x1 + 4 = a(a(x1)) B(B(A(A(x1)))) = x1 + 12 >= x1 + 4 = c(c(x1)) a(a(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 20 >= x1 + 18 = A(A(A(A(A(A(x1)))))) A(A(A(A(A(A(A(A(x1)))))))) = x1 + 24 >= x1 + 16 = a(a(a(a(a(a(a(a(x1)))))))) b(b(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 20 >= x1 + 18 = B(B(B(B(B(B(x1)))))) B(B(B(B(B(B(B(B(x1)))))))) = x1 + 24 >= x1 + 16 = b(b(b(b(b(b(b(b(x1)))))))) c(c(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 20 >= x1 + 18 = C(C(C(C(C(C(x1)))))) C(C(C(C(C(C(C(C(x1)))))))) = x1 + 24 >= x1 + 16 = c(c(c(c(c(c(c(c(x1)))))))) B(B(a(a(a(a(a(a(a(a(x1)))))))))) = x1 + 22 >= x1 + 22 = c(c(A(A(A(A(A(A(x1)))))))) A(A(A(A(A(A(b(b(x1)))))))) = x1 + 22 >= x1 + 22 = a(a(a(a(a(a(a(a(C(C(x1)))))))))) C(C(b(b(b(b(b(b(b(b(x1)))))))))) = x1 + 22 >= x1 + 22 = a(a(B(B(B(B(B(B(x1)))))))) B(B(B(B(B(B(c(c(x1)))))))) = x1 + 22 >= x1 + 22 = b(b(b(b(b(b(b(b(A(A(x1)))))))))) A(A(c(c(c(c(c(c(c(c(x1)))))))))) = x1 + 22 >= x1 + 22 = b(b(C(C(C(C(C(C(x1)))))))) C(C(C(C(C(C(a(a(x1)))))))) = x1 + 22 >= x1 + 22 = c(c(c(c(c(c(c(c(B(B(x1)))))))))) a(a(A(A(x1)))) = x1 + 10 >= x1 = x1 A(A(a(a(x1)))) = x1 + 10 >= x1 = x1 b(b(B(B(x1)))) = x1 + 10 >= x1 = x1 B(B(b(b(x1)))) = x1 + 10 >= x1 = x1 c(c(C(C(x1)))) = x1 + 10 >= x1 = x1 C(C(c(c(x1)))) = x1 + 10 >= x1 = x1 problem: DPs: TRS: a(a(b(b(x1)))) -> C(C(x1)) b(b(c(c(x1)))) -> A(A(x1)) c(c(a(a(x1)))) -> B(B(x1)) A(A(C(C(x1)))) -> b(b(x1)) C(C(B(B(x1)))) -> a(a(x1)) B(B(A(A(x1)))) -> c(c(x1)) a(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A(A(A(A(A(A(x1)))))) A(A(A(A(A(A(A(A(x1)))))))) -> a(a(a(a(a(a(a(a(x1)))))))) b(b(b(b(b(b(b(b(b(b(x1)))))))))) -> B(B(B(B(B(B(x1)))))) B(B(B(B(B(B(B(B(x1)))))))) -> b(b(b(b(b(b(b(b(x1)))))))) c(c(c(c(c(c(c(c(c(c(x1)))))))))) -> C(C(C(C(C(C(x1)))))) C(C(C(C(C(C(C(C(x1)))))))) -> c(c(c(c(c(c(c(c(x1)))))))) B(B(a(a(a(a(a(a(a(a(x1)))))))))) -> c(c(A(A(A(A(A(A(x1)))))))) A(A(A(A(A(A(b(b(x1)))))))) -> a(a(a(a(a(a(a(a(C(C(x1)))))))))) C(C(b(b(b(b(b(b(b(b(x1)))))))))) -> a(a(B(B(B(B(B(B(x1)))))))) B(B(B(B(B(B(c(c(x1)))))))) -> b(b(b(b(b(b(b(b(A(A(x1)))))))))) A(A(c(c(c(c(c(c(c(c(x1)))))))))) -> b(b(C(C(C(C(C(C(x1)))))))) C(C(C(C(C(C(a(a(x1)))))))) -> c(c(c(c(c(c(c(c(B(B(x1)))))))))) a(a(A(A(x1)))) -> x1 A(A(a(a(x1)))) -> x1 b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 c(c(C(C(x1)))) -> x1 C(C(c(c(x1)))) -> x1 Qed