MAYBE

Problem:
 f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
 f(a(x),y) -> f(x,a(y))
 f(b(x),y) -> f(x,b(y))
 f(c(x),y) -> f(x,c(y))

Proof:
 Complexity Transformation Processor:
  strict:
   f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
   f(a(x),y) -> f(x,a(y))
   f(b(x),y) -> f(x,b(y))
   f(c(x),y) -> f(x,c(y))
  weak:
   
  Bounds Processor:
   bound: 3
   enrichment: match
   automaton:
    final states: {5}
    transitions:
     f3(29,103) -> 5*
     f3(52,115) -> 5*
     f3(53,103) -> 5*
     f3(50,91) -> 5*
     f3(51,84) -> 5*
     f3(30,103) -> 5*
     f3(5,103) -> 5*
     f1(30,5) -> 5*
     f1(30,19) -> 5*
     f1(5,19) -> 5*
     f1(29,19) -> 5*
     f1(29,27) -> 5*
     b3(91) -> 103*
     b3(103) -> 115*
     b1(30) -> 27*
     b1(5) -> 27*
     b1(72) -> 19*
     b1(29) -> 30*
     b1(19) -> 19*
     b1(103) -> 19*
     b1(53) -> 27*
     c3(50) -> 84*
     c3(97) -> 84*
     c3(74) -> 84*
     c3(115) -> 84*
     c1(5) -> 19*
     c1(72) -> 19*
     c1(19) -> 19*
     c1(103) -> 19*
     c1(28) -> 29*
     a3(84) -> 91*
     a1(72) -> 19*
     a1(27) -> 28*
     a1(19) -> 19*
     a1(103) -> 19*
     f2(53,5) -> 5*
     f2(30,72) -> 5*
     f2(53,19) -> 5*
     f2(5,72) -> 5*
     f2(29,97) -> 5*
     f2(52,50) -> 5*
     f2(27,64) -> 5*
     f2(28,49) -> 5*
     f2(52,74) -> 5*
     f2(53,72) -> 5*
     f2(52,97) -> 5*
     f0(5,5) -> 5*
     b2(30) -> 50*
     b2(5) -> 50*
     b2(72) -> 97*
     b2(52) -> 53*
     b2(64) -> 72*
     b2(29) -> 50*
     b2(19) -> 74*
     b2(103) -> 97*
     b2(53) -> 50*
     a0(5) -> 5*
     c2(97) -> 49*
     c2(27) -> 49*
     c2(19) -> 49*
     c2(51) -> 52*
     c2(103) -> 49*
     b0(5) -> 5*
     a2(50) -> 51*
     a2(49) -> 64*
     c0(5) -> 5*
   problem:
    strict:
     f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
     f(a(x),y) -> f(x,a(y))
     f(b(x),y) -> f(x,b(y))
    weak:
     f(c(x),y) -> f(x,c(y))
   Bounds Processor:
    bound: 2
    enrichment: match
    automaton:
     final states: {4,3,2,1}
     transitions:
      f1(9,2) -> 1*
      f1(9,4) -> 1*
      f1(7,48) -> 1*
      f1(2,48) -> 1*
      f1(9,48) -> 1*
      f1(4,48) -> 1*
      f1(6,42) -> 1*
      f1(8,6) -> 1*
      f1(6,48) -> 1*
      f1(1,48) -> 1*
      f1(9,1) -> 1*
      f1(7,41) -> 1*
      f1(9,3) -> 1*
      f1(8,48) -> 1*
      f1(3,48) -> 1*
      b1(42) -> 48*
      b1(2) -> 6*
      b1(79) -> 48*
      b1(9) -> 6*
      b1(4) -> 6*
      b1(71) -> 48*
      b1(1) -> 6*
      b1(48) -> 48*
      b1(8) -> 9*
      b1(3) -> 6*
      c1(7) -> 8*
      c1(79) -> 48*
      c1(71) -> 48*
      c1(6) -> 41*
      c1(48) -> 48*
      a1(79) -> 48*
      a1(71) -> 48*
      a1(41) -> 42*
      a1(6) -> 7*
      a1(48) -> 48*
      f2(4,71) -> 1*
      f2(9,79) -> 1*
      f2(4,79) -> 1*
      f2(1,71) -> 1*
      f2(6,79) -> 1*
      f2(1,79) -> 1*
      f2(57,74) -> 1*
      f2(7,74) -> 1*
      f2(59,48) -> 1*
      f2(58,71) -> 1*
      f2(8,71) -> 1*
      f2(3,71) -> 1*
      f2(8,79) -> 1*
      f2(3,79) -> 1*
      f2(56,78) -> 1*
      f2(6,78) -> 1*
      f2(2,71) -> 1*
      f2(7,79) -> 1*
      f2(2,79) -> 1*
      f2(59,71) -> 1*
      f2(59,79) -> 1*
      f2(9,71) -> 1*
      f0(3,1) -> 1*
      f0(3,3) -> 1*
      f0(4,2) -> 1*
      f0(4,4) -> 1*
      f0(1,2) -> 1*
      f0(1,4) -> 1*
      f0(2,1) -> 1*
      f0(2,3) -> 1*
      f0(3,2) -> 1*
      f0(3,4) -> 1*
      f0(4,1) -> 1*
      f0(4,3) -> 1*
      f0(1,1) -> 1*
      f0(1,3) -> 1*
      f0(2,2) -> 1*
      f0(2,4) -> 1*
      b2(7) -> 56*
      b2(2) -> 56*
      b2(79) -> 71*
      b2(59) -> 56*
      b2(9) -> 56*
      b2(4) -> 56*
      b2(71) -> 71*
      b2(6) -> 56*
      b2(1) -> 56*
      b2(78) -> 79*
      b2(58) -> 59*
      b2(48) -> 71*
      b2(8) -> 56*
      b2(3) -> 56*
      a0(2) -> 2*
      a0(4) -> 2*
      a0(1) -> 2*
      a0(3) -> 2*
      c2(57) -> 58*
      c2(79) -> 79*
      c2(71) -> 74*
      b0(2) -> 3*
      b0(4) -> 3*
      b0(1) -> 3*
      b0(3) -> 3*
      a2(79) -> 79*
      a2(74) -> 78*
      a2(56) -> 57*
      c0(2) -> 4*
      c0(4) -> 4*
      c0(1) -> 4*
      c0(3) -> 4*
    problem:
     strict:
      f(a(x),y) -> f(x,a(y))
      f(b(x),y) -> f(x,b(y))
     weak:
      f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
      f(c(x),y) -> f(x,c(y))
    Bounds Processor:
     bound: 3
     enrichment: match
     automaton:
      final states: {5}
      transitions:
       f3(32,48) -> 5*
       f3(12,48) -> 5*
       f3(14,48) -> 5*
       f3(30,61) -> 5*
       f3(31,58) -> 5*
       f3(13,48) -> 5*
       f3(29,47) -> 5*
       f3(15,48) -> 5*
       f3(5,48) -> 5*
       f1(13,7) -> 5*
       f1(13,19) -> 5*
       f1(14,12) -> 5*
       f1(15,5) -> 5*
       f1(15,7) -> 5*
       f1(5,7) -> 5*
       f1(14,7) -> 5*
       b3(47) -> 48*
       b3(48) -> 58*
       b1(15) -> 12*
       b1(5) -> 12*
       b1(32) -> 12*
       b1(7) -> 7*
       b1(14) -> 15*
       b1(26) -> 7*
       b1(48) -> 7*
       b1(13) -> 12*
       c3(58) -> 61*
       c1(12) -> 19*
       c1(7) -> 7*
       c1(26) -> 7*
       c1(48) -> 7*
       c1(13) -> 14*
       a3(45) -> 47*
       a3(61) -> 47*
       a3(26) -> 47*
       a1(15) -> 13*
       a1(5) -> 7*
       a1(12) -> 13*
       a1(7) -> 7*
       a1(26) -> 7*
       a1(48) -> 7*
       f2(31,37) -> 5*
       f2(32,26) -> 5*
       f2(12,24) -> 5*
       f2(14,26) -> 5*
       f2(30,45) -> 5*
       f2(32,7) -> 5*
       f2(32,35) -> 5*
       f2(13,26) -> 5*
       f2(14,35) -> 5*
       f2(30,26) -> 5*
       f2(15,24) -> 5*
       f2(15,26) -> 5*
       f2(5,26) -> 5*
       f2(31,35) -> 5*
       f0(5,5) -> 5*
       b2(35) -> 35*
       b2(15) -> 29*
       b2(5) -> 29*
       b2(32) -> 29*
       b2(12) -> 29*
       b2(7) -> 37*
       b2(24) -> 26*
       b2(14) -> 29*
       b2(31) -> 32*
       b2(26) -> 35*
       b2(48) -> 26*
       b2(13) -> 29*
       a0(5) -> 5*
       c2(35) -> 26*
       c2(30) -> 31*
       c2(37) -> 45*
       c2(26) -> 26*
       c2(48) -> 26*
       b0(5) -> 5*
       a2(7) -> 24*
       a2(29) -> 30*
       a2(19) -> 24*
       a2(26) -> 24*
       a2(48) -> 24*
       c0(5) -> 5*
     problem:
      strict:
       f(b(x),y) -> f(x,b(y))
      weak:
       f(a(x),y) -> f(x,a(y))
       f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
       f(c(x),y) -> f(x,c(y))
     Open