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: {4}
    transitions:
     f3(30,66) -> 4*
     f3(31,59) -> 4*
     f3(21,59) -> 4*
     f3(1,59) -> 4*
     f3(28,55) -> 4*
     f3(3,59) -> 4*
     f3(22,59) -> 4*
     f3(2,59) -> 4*
     f3(29,51) -> 4*
     f1(3,11) -> 4*
     f1(22,1) -> 4*
     f1(22,3) -> 4*
     f1(22,11) -> 4*
     f1(2,11) -> 4*
     f1(21,11) -> 4*
     f1(1,11) -> 4*
     f1(21,19) -> 4*
     f1(22,2) -> 4*
     b3(55) -> 59*
     b3(59) -> 66*
     b1(22) -> 19*
     b1(2) -> 19*
     b1(59) -> 11*
     b1(21) -> 22*
     b1(11) -> 11*
     b1(1) -> 19*
     b1(53) -> 11*
     b1(3) -> 19*
     c3(49) -> 51*
     c3(66) -> 51*
     c3(58) -> 51*
     c3(28) -> 51*
     c1(20) -> 21*
     c1(2) -> 11*
     c1(59) -> 11*
     c1(11) -> 11*
     c1(1) -> 11*
     c1(53) -> 11*
     c1(3) -> 11*
     a3(51) -> 55*
     a1(59) -> 11*
     a1(19) -> 20*
     a1(11) -> 11*
     a1(53) -> 11*
     f2(30,58) -> 4*
     f2(31,53) -> 4*
     f2(1,53) -> 4*
     f2(3,53) -> 4*
     f2(31,2) -> 4*
     f2(19,46) -> 4*
     f2(20,27) -> 4*
     f2(30,49) -> 4*
     f2(21,58) -> 4*
     f2(22,53) -> 4*
     f2(2,53) -> 4*
     f2(31,1) -> 4*
     f2(31,3) -> 4*
     f2(30,28) -> 4*
     f2(31,11) -> 4*
     f0(3,1) -> 4*
     f0(3,3) -> 4*
     f0(1,2) -> 4*
     f0(2,1) -> 4*
     f0(2,3) -> 4*
     f0(3,2) -> 4*
     f0(1,1) -> 4*
     f0(1,3) -> 4*
     f0(2,2) -> 4*
     b2(30) -> 31*
     b2(22) -> 28*
     b2(2) -> 28*
     b2(59) -> 58*
     b2(46) -> 53*
     b2(31) -> 28*
     b2(21) -> 28*
     b2(11) -> 49*
     b2(1) -> 28*
     b2(53) -> 58*
     b2(3) -> 28*
     a0(2) -> 1*
     a0(1) -> 1*
     a0(3) -> 1*
     c2(59) -> 27*
     c2(29) -> 30*
     c2(19) -> 27*
     c2(11) -> 27*
     c2(58) -> 27*
     b0(2) -> 2*
     b0(1) -> 2*
     b0(3) -> 2*
     a2(27) -> 46*
     a2(28) -> 29*
     c0(2) -> 3*
     c0(1) -> 3*
     c0(3) -> 3*
   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: 3
    enrichment: match
    automaton:
     final states: {4}
     transitions:
      f3(55,68) -> 4*
      f3(57,36) -> 4*
      f3(56,63) -> 4*
      f3(6,63) -> 4*
      f3(1,63) -> 4*
      f3(26,69) -> 4*
      f3(27,68) -> 4*
      f3(28,63) -> 4*
      f3(8,63) -> 4*
      f3(3,63) -> 4*
      f3(54,62) -> 4*
      f3(55,61) -> 4*
      f3(5,63) -> 4*
      f3(56,60) -> 4*
      f3(57,41) -> 4*
      f3(57,63) -> 4*
      f3(7,63) -> 4*
      f3(2,63) -> 4*
      f3(29,63) -> 4*
      f3(54,69) -> 4*
      f3(29,69) -> 4*
      f1(1,39) -> 4*
      f1(8,1) -> 4*
      f1(8,3) -> 4*
      f1(2,36) -> 4*
      f1(8,21) -> 4*
      f1(2,40) -> 4*
      f1(3,21) -> 4*
      f1(3,39) -> 4*
      f1(5,21) -> 4*
      f1(7,5) -> 4*
      f1(1,36) -> 4*
      f1(7,21) -> 4*
      f1(1,40) -> 4*
      f1(8,2) -> 4*
      f1(2,21) -> 4*
      f1(2,39) -> 4*
      f1(3,36) -> 4*
      f1(3,40) -> 4*
      f1(5,20) -> 4*
      f1(6,19) -> 4*
      f1(6,21) -> 4*
      f1(1,21) -> 4*
      b3(5) -> 54*
      b3(62) -> 63*
      b3(57) -> 54*
      b3(7) -> 54*
      b3(2) -> 54*
      b3(69) -> 63*
      b3(29) -> 54*
      b3(56) -> 57*
      b3(41) -> 60*
      b3(36) -> 60*
      b3(6) -> 54*
      b3(1) -> 54*
      b3(63) -> 63*
      b3(28) -> 54*
      b3(8) -> 54*
      b3(3) -> 54*
      b1(20) -> 21*
      b1(7) -> 8*
      b1(2) -> 5*
      b1(39) -> 21*
      b1(36) -> 21*
      b1(21) -> 21*
      b1(1) -> 5*
      b1(8) -> 5*
      b1(3) -> 5*
      c3(60) -> 61*
      c3(55) -> 56*
      c3(63) -> 68*
      c1(40) -> 21*
      c1(5) -> 19*
      c1(39) -> 21*
      c1(21) -> 21*
      c1(6) -> 7*
      a3(54) -> 55*
      a3(61) -> 62*
      a3(68) -> 69*
      a1(40) -> 21*
      a1(5) -> 6*
      a1(19) -> 20*
      a1(41) -> 21*
      a1(36) -> 21*
      a1(21) -> 21*
      a1(63) -> 21*
      f2(26,41) -> 4*
      f2(6,39) -> 4*
      f2(6,41) -> 4*
      f2(1,41) -> 4*
      f2(7,36) -> 4*
      f2(2,36) -> 4*
      f2(28,41) -> 4*
      f2(8,41) -> 4*
      f2(3,41) -> 4*
      f2(29,36) -> 4*
      f2(29,40) -> 4*
      f2(5,41) -> 4*
      f2(6,36) -> 4*
      f2(26,40) -> 4*
      f2(1,36) -> 4*
      f2(27,39) -> 4*
      f2(27,41) -> 4*
      f2(7,41) -> 4*
      f2(2,41) -> 4*
      f2(28,36) -> 4*
      f2(8,36) -> 4*
      f2(29,21) -> 4*
      f2(3,36) -> 4*
      f2(29,39) -> 4*
      f2(29,41) -> 4*
      f2(5,36) -> 4*
      f2(5,40) -> 4*
      f0(3,1) -> 4*
      f0(3,3) -> 4*
      f0(1,2) -> 4*
      f0(2,1) -> 4*
      f0(2,3) -> 4*
      f0(3,2) -> 4*
      f0(1,1) -> 4*
      f0(1,3) -> 4*
      f0(2,2) -> 4*
      b2(40) -> 41*
      b2(5) -> 26*
      b2(57) -> 26*
      b2(7) -> 26*
      b2(2) -> 26*
      b2(39) -> 36*
      b2(29) -> 26*
      b2(41) -> 36*
      b2(36) -> 36*
      b2(21) -> 36*
      b2(6) -> 26*
      b2(1) -> 26*
      b2(28) -> 29*
      b2(8) -> 26*
      b2(3) -> 26*
      a0(2) -> 1*
      a0(1) -> 1*
      a0(3) -> 1*
      c2(27) -> 28*
      c2(41) -> 41*
      c2(36) -> 39*
      c2(63) -> 36*
      b0(2) -> 2*
      b0(1) -> 2*
      b0(3) -> 2*
      a2(39) -> 40*
      a2(29) -> 27*
      a2(41) -> 41*
      a2(36) -> 36*
      a2(26) -> 27*
      a2(63) -> 36*
      c0(2) -> 3*
      c0(1) -> 3*
      c0(3) -> 3*
    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: 4
     enrichment: match
     automaton:
      final states: {4}
      transitions:
       b3(27) -> 33*
       b3(17) -> 29*
       b3(12) -> 29*
       b3(9) -> 29*
       b3(31) -> 32*
       b3(26) -> 27*
       b3(16) -> 34*
       b3(43) -> 27*
       c3(30) -> 31*
       c3(34) -> 41*
       c3(33) -> 35*
       a3(35) -> 26*
       a3(25) -> 26*
       a3(29) -> 30*
       a3(16) -> 26*
       f4(29,42) -> 4*
       f4(17,43) -> 4*
       f4(12,43) -> 4*
       f4(9,43) -> 4*
       a4(35) -> 42*
       a4(41) -> 42*
       f0(3,1) -> 4*
       f0(3,3) -> 4*
       f0(1,2) -> 4*
       f0(2,1) -> 4*
       f0(2,3) -> 4*
       f0(3,2) -> 4*
       f0(1,1) -> 4*
       f0(1,3) -> 4*
       f0(2,2) -> 4*
       a0(2) -> 1*
       a0(1) -> 1*
       a0(3) -> 1*
       b0(2) -> 2*
       b0(1) -> 2*
       b0(3) -> 2*
       b4(42) -> 43*
       c0(2) -> 3*
       c0(1) -> 3*
       c0(3) -> 3*
       f1(3,5) -> 4*
       f1(10,5) -> 4*
       f1(12,1) -> 4*
       f1(12,3) -> 4*
       f1(12,5) -> 4*
       f1(2,5) -> 4*
       f1(10,14) -> 4*
       f1(11,5) -> 4*
       f1(1,5) -> 4*
       f1(11,9) -> 4*
       f1(12,2) -> 4*
       b1(20) -> 9*
       b1(10) -> 9*
       b1(5) -> 5*
       b1(12) -> 9*
       b1(2) -> 9*
       b1(16) -> 5*
       b1(11) -> 12*
       b1(1) -> 9*
       b1(3) -> 9*
       c1(10) -> 11*
       c1(5) -> 5*
       c1(9) -> 14*
       c1(16) -> 5*
       a1(5) -> 5*
       a1(27) -> 5*
       a1(12) -> 10*
       a1(2) -> 5*
       a1(9) -> 10*
       a1(16) -> 5*
       a1(1) -> 5*
       a1(3) -> 5*
       f2(12,16) -> 4*
       f2(2,16) -> 4*
       f2(18,25) -> 4*
       f2(19,16) -> 4*
       f2(20,5) -> 4*
       f2(11,16) -> 4*
       f2(1,16) -> 4*
       f2(12,15) -> 4*
       f2(18,16) -> 4*
       f2(3,16) -> 4*
       f2(9,15) -> 4*
       f2(19,23) -> 4*
       f2(20,16) -> 4*
       f2(10,16) -> 4*
       b2(20) -> 17*
       b2(15) -> 16*
       b2(10) -> 17*
       b2(5) -> 23*
       b2(27) -> 16*
       b2(12) -> 17*
       b2(2) -> 17*
       b2(19) -> 20*
       b2(9) -> 17*
       b2(16) -> 16*
       b2(11) -> 17*
       b2(1) -> 17*
       b2(43) -> 16*
       b2(3) -> 17*
       c2(27) -> 16*
       c2(16) -> 16*
       c2(23) -> 25*
       c2(18) -> 19*
       a2(5) -> 15*
       a2(27) -> 15*
       a2(17) -> 18*
       a2(14) -> 15*
       a2(16) -> 15*
       f3(32,16) -> 4*
       f3(17,26) -> 4*
       f3(3,27) -> 4*
       f3(18,35) -> 4*
       f3(20,27) -> 4*
       f3(10,27) -> 4*
       f3(30,35) -> 4*
       f3(30,41) -> 4*
       f3(31,34) -> 4*
       f3(32,27) -> 4*
       f3(12,27) -> 4*
       f3(2,27) -> 4*
       f3(9,27) -> 4*
       f3(19,33) -> 4*
       f3(11,27) -> 4*
       f3(31,33) -> 4*
       f3(1,27) -> 4*
     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