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 TDG 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 graph: ... Arctic Interpretation Processor: dimension: 1 interpretation: [B#](x0) = 9x0, [c#](x0) = 7x0, [A#](x0) = 9x0, [b#](x0) = 8x0, [C#](x0) = 8x0, [a#](x0) = 6x0, [B](x0) = 3x0, [A](x0) = 3x0, [c](x0) = 2x0, [C](x0) = 3x0, [a](x0) = 2x0, [b](x0) = 2x0 orientation: a#(a(b(b(x1)))) = 12x1 >= 8x1 = C#(x1) a#(a(b(b(x1)))) = 12x1 >= 11x1 = C#(C(x1)) b#(b(c(c(x1)))) = 14x1 >= 9x1 = A#(x1) b#(b(c(c(x1)))) = 14x1 >= 12x1 = A#(A(x1)) c#(c(a(a(x1)))) = 13x1 >= 9x1 = B#(x1) c#(c(a(a(x1)))) = 13x1 >= 12x1 = B#(B(x1)) A#(A(C(C(x1)))) = 18x1 >= 8x1 = b#(x1) A#(A(C(C(x1)))) = 18x1 >= 10x1 = b#(b(x1)) C#(C(B(B(x1)))) = 17x1 >= 6x1 = a#(x1) C#(C(B(B(x1)))) = 17x1 >= 8x1 = a#(a(x1)) B#(B(A(A(x1)))) = 18x1 >= 7x1 = c#(x1) B#(B(A(A(x1)))) = 18x1 >= 9x1 = c#(c(x1)) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = 24x1 >= 9x1 = A#(x1) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = 24x1 >= 12x1 = A#(A(x1)) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = 24x1 >= 15x1 = A#(A(A(x1))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = 24x1 >= 18x1 = A#(A(A(A(x1)))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = 24x1 >= 21x1 = A#(A(A(A(A(x1))))) a#(a(a(a(a(a(a(a(a(a(x1)))))))))) = 24x1 >= 24x1 = A#(A(A(A(A(A(x1)))))) A#(A(A(A(A(A(A(A(x1)))))))) = 30x1 >= 6x1 = a#(x1) A#(A(A(A(A(A(A(A(x1)))))))) = 30x1 >= 8x1 = a#(a(x1)) A#(A(A(A(A(A(A(A(x1)))))))) = 30x1 >= 10x1 = a#(a(a(x1))) A#(A(A(A(A(A(A(A(x1)))))))) = 30x1 >= 12x1 = a#(a(a(a(x1)))) A#(A(A(A(A(A(A(A(x1)))))))) = 30x1 >= 14x1 = a#(a(a(a(a(x1))))) A#(A(A(A(A(A(A(A(x1)))))))) = 30x1 >= 16x1 = a#(a(a(a(a(a(x1)))))) A#(A(A(A(A(A(A(A(x1)))))))) = 30x1 >= 18x1 = a#(a(a(a(a(a(a(x1))))))) A#(A(A(A(A(A(A(A(x1)))))))) = 30x1 >= 20x1 = a#(a(a(a(a(a(a(a(x1)))))))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = 26x1 >= 9x1 = B#(x1) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = 26x1 >= 12x1 = B#(B(x1)) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = 26x1 >= 15x1 = B#(B(B(x1))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = 26x1 >= 18x1 = B#(B(B(B(x1)))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = 26x1 >= 21x1 = B#(B(B(B(B(x1))))) b#(b(b(b(b(b(b(b(b(b(x1)))))))))) = 26x1 >= 24x1 = B#(B(B(B(B(B(x1)))))) B#(B(B(B(B(B(B(B(x1)))))))) = 30x1 >= 8x1 = b#(x1) B#(B(B(B(B(B(B(B(x1)))))))) = 30x1 >= 10x1 = b#(b(x1)) B#(B(B(B(B(B(B(B(x1)))))))) = 30x1 >= 12x1 = b#(b(b(x1))) B#(B(B(B(B(B(B(B(x1)))))))) = 30x1 >= 14x1 = b#(b(b(b(x1)))) B#(B(B(B(B(B(B(B(x1)))))))) = 30x1 >= 16x1 = b#(b(b(b(b(x1))))) B#(B(B(B(B(B(B(B(x1)))))))) = 30x1 >= 18x1 = b#(b(b(b(b(b(x1)))))) B#(B(B(B(B(B(B(B(x1)))))))) = 30x1 >= 20x1 = b#(b(b(b(b(b(b(x1))))))) B#(B(B(B(B(B(B(B(x1)))))))) = 30x1 >= 22x1 = b#(b(b(b(b(b(b(b(x1)))))))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = 25x1 >= 8x1 = C#(x1) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = 25x1 >= 11x1 = C#(C(x1)) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = 25x1 >= 14x1 = C#(C(C(x1))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = 25x1 >= 17x1 = C#(C(C(C(x1)))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = 25x1 >= 20x1 = C#(C(C(C(C(x1))))) c#(c(c(c(c(c(c(c(c(c(x1)))))))))) = 25x1 >= 23x1 = C#(C(C(C(C(C(x1)))))) C#(C(C(C(C(C(C(C(x1)))))))) = 29x1 >= 7x1 = c#(x1) C#(C(C(C(C(C(C(C(x1)))))))) = 29x1 >= 9x1 = c#(c(x1)) C#(C(C(C(C(C(C(C(x1)))))))) = 29x1 >= 11x1 = c#(c(c(x1))) C#(C(C(C(C(C(C(C(x1)))))))) = 29x1 >= 13x1 = c#(c(c(c(x1)))) C#(C(C(C(C(C(C(C(x1)))))))) = 29x1 >= 15x1 = c#(c(c(c(c(x1))))) C#(C(C(C(C(C(C(C(x1)))))))) = 29x1 >= 17x1 = c#(c(c(c(c(c(x1)))))) C#(C(C(C(C(C(C(C(x1)))))))) = 29x1 >= 19x1 = c#(c(c(c(c(c(c(x1))))))) C#(C(C(C(C(C(C(C(x1)))))))) = 29x1 >= 21x1 = c#(c(c(c(c(c(c(c(x1)))))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = 28x1 >= 9x1 = A#(x1) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = 28x1 >= 12x1 = A#(A(x1)) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = 28x1 >= 15x1 = A#(A(A(x1))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = 28x1 >= 18x1 = A#(A(A(A(x1)))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = 28x1 >= 21x1 = A#(A(A(A(A(x1))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = 28x1 >= 24x1 = A#(A(A(A(A(A(x1)))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = 28x1 >= 25x1 = c#(A(A(A(A(A(A(x1))))))) B#(B(a(a(a(a(a(a(a(a(x1)))))))))) = 28x1 >= 27x1 = c#(c(A(A(A(A(A(A(x1)))))))) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 8x1 = C#(x1) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 11x1 = C#(C(x1)) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 12x1 = a#(C(C(x1))) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 14x1 = a#(a(C(C(x1)))) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 16x1 = a#(a(a(C(C(x1))))) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 18x1 = a#(a(a(a(C(C(x1)))))) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 20x1 = a#(a(a(a(a(C(C(x1))))))) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 22x1 = a#(a(a(a(a(a(C(C(x1)))))))) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 24x1 = a#(a(a(a(a(a(a(C(C(x1))))))))) A#(A(A(A(A(A(b(b(x1)))))))) = 28x1 >= 26x1 = a#(a(a(a(a(a(a(a(C(C(x1)))))))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = 27x1 >= 9x1 = B#(x1) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = 27x1 >= 12x1 = B#(B(x1)) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = 27x1 >= 15x1 = B#(B(B(x1))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = 27x1 >= 18x1 = B#(B(B(B(x1)))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = 27x1 >= 21x1 = B#(B(B(B(B(x1))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = 27x1 >= 24x1 = B#(B(B(B(B(B(x1)))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = 27x1 >= 24x1 = a#(B(B(B(B(B(B(x1))))))) C#(C(b(b(b(b(b(b(b(b(x1)))))))))) = 27x1 >= 26x1 = a#(a(B(B(B(B(B(B(x1)))))))) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 9x1 = A#(x1) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 12x1 = A#(A(x1)) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 14x1 = b#(A(A(x1))) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 16x1 = b#(b(A(A(x1)))) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 18x1 = b#(b(b(A(A(x1))))) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 20x1 = b#(b(b(b(A(A(x1)))))) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 22x1 = b#(b(b(b(b(A(A(x1))))))) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 24x1 = b#(b(b(b(b(b(A(A(x1)))))))) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 26x1 = b#(b(b(b(b(b(b(A(A(x1))))))))) B#(B(B(B(B(B(c(c(x1)))))))) = 28x1 >= 28x1 = b#(b(b(b(b(b(b(b(A(A(x1)))))))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = 28x1 >= 8x1 = C#(x1) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = 28x1 >= 11x1 = C#(C(x1)) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = 28x1 >= 14x1 = C#(C(C(x1))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = 28x1 >= 17x1 = C#(C(C(C(x1)))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = 28x1 >= 20x1 = C#(C(C(C(C(x1))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = 28x1 >= 23x1 = C#(C(C(C(C(C(x1)))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = 28x1 >= 26x1 = b#(C(C(C(C(C(C(x1))))))) A#(A(c(c(c(c(c(c(c(c(x1)))))))))) = 28x1 >= 28x1 = b#(b(C(C(C(C(C(C(x1)))))))) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 9x1 = B#(x1) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 12x1 = B#(B(x1)) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 13x1 = c#(B(B(x1))) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 15x1 = c#(c(B(B(x1)))) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 17x1 = c#(c(c(B(B(x1))))) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 19x1 = c#(c(c(c(B(B(x1)))))) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 21x1 = c#(c(c(c(c(B(B(x1))))))) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 23x1 = c#(c(c(c(c(c(B(B(x1)))))))) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 25x1 = c#(c(c(c(c(c(c(B(B(x1))))))))) C#(C(C(C(C(C(a(a(x1)))))))) = 27x1 >= 27x1 = c#(c(c(c(c(c(c(c(B(B(x1)))))))))) a(a(b(b(x1)))) = 8x1 >= 6x1 = C(C(x1)) b(b(c(c(x1)))) = 8x1 >= 6x1 = A(A(x1)) c(c(a(a(x1)))) = 8x1 >= 6x1 = B(B(x1)) A(A(C(C(x1)))) = 12x1 >= 4x1 = b(b(x1)) C(C(B(B(x1)))) = 12x1 >= 4x1 = a(a(x1)) B(B(A(A(x1)))) = 12x1 >= 4x1 = c(c(x1)) a(a(a(a(a(a(a(a(a(a(x1)))))))))) = 20x1 >= 18x1 = A(A(A(A(A(A(x1)))))) A(A(A(A(A(A(A(A(x1)))))))) = 24x1 >= 16x1 = a(a(a(a(a(a(a(a(x1)))))))) b(b(b(b(b(b(b(b(b(b(x1)))))))))) = 20x1 >= 18x1 = B(B(B(B(B(B(x1)))))) B(B(B(B(B(B(B(B(x1)))))))) = 24x1 >= 16x1 = b(b(b(b(b(b(b(b(x1)))))))) c(c(c(c(c(c(c(c(c(c(x1)))))))))) = 20x1 >= 18x1 = C(C(C(C(C(C(x1)))))) C(C(C(C(C(C(C(C(x1)))))))) = 24x1 >= 16x1 = c(c(c(c(c(c(c(c(x1)))))))) B(B(a(a(a(a(a(a(a(a(x1)))))))))) = 22x1 >= 22x1 = c(c(A(A(A(A(A(A(x1)))))))) A(A(A(A(A(A(b(b(x1)))))))) = 22x1 >= 22x1 = a(a(a(a(a(a(a(a(C(C(x1)))))))))) C(C(b(b(b(b(b(b(b(b(x1)))))))))) = 22x1 >= 22x1 = a(a(B(B(B(B(B(B(x1)))))))) B(B(B(B(B(B(c(c(x1)))))))) = 22x1 >= 22x1 = b(b(b(b(b(b(b(b(A(A(x1)))))))))) A(A(c(c(c(c(c(c(c(c(x1)))))))))) = 22x1 >= 22x1 = b(b(C(C(C(C(C(C(x1)))))))) C(C(C(C(C(C(a(a(x1)))))))) = 22x1 >= 22x1 = c(c(c(c(c(c(c(c(B(B(x1)))))))))) a(a(A(A(x1)))) = 10x1 >= x1 = x1 A(A(a(a(x1)))) = 10x1 >= x1 = x1 b(b(B(B(x1)))) = 10x1 >= x1 = x1 B(B(b(b(x1)))) = 10x1 >= x1 = x1 c(c(C(C(x1)))) = 10x1 >= x1 = x1 C(C(c(c(x1)))) = 10x1 >= x1 = x1 problem: DPs: a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(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)))))))))) -> 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)))))))))) 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 EDG Processor: DPs: a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(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)))))))))) -> 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)))))))))) 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 graph: a#(a(a(a(a(a(a(a(a(a(x1)))))))))) -> A#(A(A(A(A(A(x1)))))) -> A#(A(c(c(c(c(c(c(c(c(x1)))))))))) -> b#(b(C(C(C(C(C(C(x1)))))))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/16