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: Arctic Interpretation Processor: dimension: 1 interpretation: [B](x0) = 3x0, [A](x0) = 3x0, [c](x0) = 2x0, [C](x0) = 3x0, [a](x0) = 2x0, [b](x0) = 2x0 orientation: 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: 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)))))))))) String Reversal Processor: a(a(a(a(a(a(a(a(B(B(x1)))))))))) -> A(A(A(A(A(A(c(c(x1)))))))) b(b(A(A(A(A(A(A(x1)))))))) -> C(C(a(a(a(a(a(a(a(a(x1)))))))))) b(b(b(b(b(b(b(b(C(C(x1)))))))))) -> B(B(B(B(B(B(a(a(x1)))))))) c(c(B(B(B(B(B(B(x1)))))))) -> A(A(b(b(b(b(b(b(b(b(x1)))))))))) c(c(c(c(c(c(c(c(A(A(x1)))))))))) -> C(C(C(C(C(C(b(b(x1)))))))) a(a(C(C(C(C(C(C(x1)))))))) -> B(B(c(c(c(c(c(c(c(c(x1)))))))))) DP Processor: DPs: a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) TRS: a(a(a(a(a(a(a(a(B(B(x1)))))))))) -> A(A(A(A(A(A(c(c(x1)))))))) b(b(A(A(A(A(A(A(x1)))))))) -> C(C(a(a(a(a(a(a(a(a(x1)))))))))) b(b(b(b(b(b(b(b(C(C(x1)))))))))) -> B(B(B(B(B(B(a(a(x1)))))))) c(c(B(B(B(B(B(B(x1)))))))) -> A(A(b(b(b(b(b(b(b(b(x1)))))))))) c(c(c(c(c(c(c(c(A(A(x1)))))))))) -> C(C(C(C(C(C(b(b(x1)))))))) a(a(C(C(C(C(C(C(x1)))))))) -> B(B(c(c(c(c(c(c(c(c(x1)))))))))) TDG Processor: DPs: a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) TRS: a(a(a(a(a(a(a(a(B(B(x1)))))))))) -> A(A(A(A(A(A(c(c(x1)))))))) b(b(A(A(A(A(A(A(x1)))))))) -> C(C(a(a(a(a(a(a(a(a(x1)))))))))) b(b(b(b(b(b(b(b(C(C(x1)))))))))) -> B(B(B(B(B(B(a(a(x1)))))))) c(c(B(B(B(B(B(B(x1)))))))) -> A(A(b(b(b(b(b(b(b(b(x1)))))))))) c(c(c(c(c(c(c(c(A(A(x1)))))))))) -> C(C(C(C(C(C(b(b(x1)))))))) a(a(C(C(C(C(C(C(x1)))))))) -> B(B(c(c(c(c(c(c(c(c(x1)))))))))) graph: b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) -> a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(a(x1)) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(b(b(b(b(b(b(C(C(x1)))))))))) -> a#(x1) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(a(x1)))))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(a(x1))))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(a(x1)))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(a(x1))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(a(x1)))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(a(x1))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(a(x1)) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) -> b#(b(A(A(A(A(A(A(x1)))))))) -> a#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(c(x1)))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(c(x1))))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(c(x1)))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(c(x1))))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(c(x1)))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(c(x1))) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(c(x1)) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(b(x1)) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(c(c(c(c(c(c(A(A(x1)))))))))) -> b#(x1) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(b(x1)))))))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(b(x1))))))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(b(x1)))))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(b(x1))))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(b(x1)))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(b(x1))) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(b(x1)) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) -> c#(x1) -> c#(c(B(B(B(B(B(B(x1)))))))) -> b#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = 2x0 + 0, [c#](x0) = 5x0, [a#](x0) = x0, [B](x0) = 3x0 + 4, [A](x0) = 3x0 + 1, [c](x0) = 2x0, [C](x0) = 3x0 + 3, [a](x0) = 2x0 + 0, [b](x0) = 2x0 orientation: a#(a(a(a(a(a(a(a(B(B(x1)))))))))) = 20x1 + 21 >= 5x1 = c#(x1) a#(a(a(a(a(a(a(a(B(B(x1)))))))))) = 20x1 + 21 >= 7x1 = c#(c(x1)) b#(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= x1 = a#(x1) b#(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= 2x1 + 0 = a#(a(x1)) b#(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= 4x1 + 2 = a#(a(a(x1))) b#(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= 6x1 + 4 = a#(a(a(a(x1)))) b#(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= 8x1 + 6 = a#(a(a(a(a(x1))))) b#(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= 10x1 + 8 = a#(a(a(a(a(a(x1)))))) b#(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= 12x1 + 10 = a#(a(a(a(a(a(a(x1))))))) b#(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= 14x1 + 12 = a#(a(a(a(a(a(a(a(x1)))))))) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) = 22x1 + 22 >= x1 = a#(x1) b#(b(b(b(b(b(b(b(C(C(x1)))))))))) = 22x1 + 22 >= 2x1 + 0 = a#(a(x1)) c#(c(B(B(B(B(B(B(x1)))))))) = 25x1 + 26 >= 2x1 + 0 = b#(x1) c#(c(B(B(B(B(B(B(x1)))))))) = 25x1 + 26 >= 4x1 + 0 = b#(b(x1)) c#(c(B(B(B(B(B(B(x1)))))))) = 25x1 + 26 >= 6x1 + 0 = b#(b(b(x1))) c#(c(B(B(B(B(B(B(x1)))))))) = 25x1 + 26 >= 8x1 + 0 = b#(b(b(b(x1)))) c#(c(B(B(B(B(B(B(x1)))))))) = 25x1 + 26 >= 10x1 + 0 = b#(b(b(b(b(x1))))) c#(c(B(B(B(B(B(B(x1)))))))) = 25x1 + 26 >= 12x1 + 0 = b#(b(b(b(b(b(x1)))))) c#(c(B(B(B(B(B(B(x1)))))))) = 25x1 + 26 >= 14x1 + 0 = b#(b(b(b(b(b(b(x1))))))) c#(c(B(B(B(B(B(B(x1)))))))) = 25x1 + 26 >= 16x1 + 0 = b#(b(b(b(b(b(b(b(x1)))))))) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) = 25x1 + 23 >= 2x1 + 0 = b#(x1) c#(c(c(c(c(c(c(c(A(A(x1)))))))))) = 25x1 + 23 >= 4x1 + 0 = b#(b(x1)) a#(a(C(C(C(C(C(C(x1)))))))) = 20x1 + 20 >= 5x1 = c#(x1) a#(a(C(C(C(C(C(C(x1)))))))) = 20x1 + 20 >= 7x1 = c#(c(x1)) a#(a(C(C(C(C(C(C(x1)))))))) = 20x1 + 20 >= 9x1 = c#(c(c(x1))) a#(a(C(C(C(C(C(C(x1)))))))) = 20x1 + 20 >= 11x1 = c#(c(c(c(x1)))) a#(a(C(C(C(C(C(C(x1)))))))) = 20x1 + 20 >= 13x1 = c#(c(c(c(c(x1))))) a#(a(C(C(C(C(C(C(x1)))))))) = 20x1 + 20 >= 15x1 = c#(c(c(c(c(c(x1)))))) a#(a(C(C(C(C(C(C(x1)))))))) = 20x1 + 20 >= 17x1 = c#(c(c(c(c(c(c(x1))))))) a#(a(C(C(C(C(C(C(x1)))))))) = 20x1 + 20 >= 19x1 = c#(c(c(c(c(c(c(c(x1)))))))) a(a(a(a(a(a(a(a(B(B(x1)))))))))) = 22x1 + 23 >= 22x1 + 16 = A(A(A(A(A(A(c(c(x1)))))))) b(b(A(A(A(A(A(A(x1)))))))) = 22x1 + 20 >= 22x1 + 20 = C(C(a(a(a(a(a(a(a(a(x1)))))))))) b(b(b(b(b(b(b(b(C(C(x1)))))))))) = 22x1 + 22 >= 22x1 + 20 = B(B(B(B(B(B(a(a(x1)))))))) c(c(B(B(B(B(B(B(x1)))))))) = 22x1 + 23 >= 22x1 + 4 = A(A(b(b(b(b(b(b(b(b(x1)))))))))) c(c(c(c(c(c(c(c(A(A(x1)))))))))) = 22x1 + 20 >= 22x1 + 18 = C(C(C(C(C(C(b(b(x1)))))))) a(a(C(C(C(C(C(C(x1)))))))) = 22x1 + 22 >= 22x1 + 7 = B(B(c(c(c(c(c(c(c(c(x1)))))))))) problem: DPs: TRS: a(a(a(a(a(a(a(a(B(B(x1)))))))))) -> A(A(A(A(A(A(c(c(x1)))))))) b(b(A(A(A(A(A(A(x1)))))))) -> C(C(a(a(a(a(a(a(a(a(x1)))))))))) b(b(b(b(b(b(b(b(C(C(x1)))))))))) -> B(B(B(B(B(B(a(a(x1)))))))) c(c(B(B(B(B(B(B(x1)))))))) -> A(A(b(b(b(b(b(b(b(b(x1)))))))))) c(c(c(c(c(c(c(c(A(A(x1)))))))))) -> C(C(C(C(C(C(b(b(x1)))))))) a(a(C(C(C(C(C(C(x1)))))))) -> B(B(c(c(c(c(c(c(c(c(x1)))))))))) Qed