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,70) -> 4*
     f3(31,61) -> 4*
     f3(21,61) -> 4*
     f3(1,61) -> 4*
     f3(28,55) -> 4*
     f3(3,61) -> 4*
     f3(22,61) -> 4*
     f3(2,61) -> 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) -> 61*
     b3(61) -> 70*
     b1(22) -> 19*
     b1(2) -> 19*
     b1(61) -> 11*
     b1(31) -> 19*
     b1(21) -> 22*
     b1(11) -> 11*
     b1(1) -> 19*
     b1(53) -> 11*
     b1(3) -> 19*
     c3(70) -> 51*
     c3(50) -> 51*
     c3(58) -> 51*
     c3(28) -> 51*
     c1(20) -> 21*
     c1(2) -> 11*
     c1(61) -> 11*
     c1(11) -> 11*
     c1(1) -> 11*
     c1(53) -> 11*
     c1(3) -> 11*
     a3(51) -> 55*
     a1(19) -> 20*
     a1(61) -> 11*
     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(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*
     f2(30,50) -> 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(61) -> 58*
     b2(46) -> 53*
     b2(31) -> 28*
     b2(21) -> 28*
     b2(11) -> 50*
     b2(1) -> 28*
     b2(53) -> 58*
     b2(3) -> 28*
     a0(2) -> 1*
     a0(1) -> 1*
     a0(3) -> 1*
     c2(29) -> 30*
     c2(19) -> 27*
     c2(61) -> 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: 2
    enrichment: match
    automaton:
     final states: {4}
     transitions:
      f1(8,1) -> 4*
      f1(8,3) -> 4*
      f1(8,21) -> 4*
      f1(3,21) -> 4*
      f1(5,21) -> 4*
      f1(7,5) -> 4*
      f1(7,21) -> 4*
      f1(8,2) -> 4*
      f1(2,21) -> 4*
      f1(5,20) -> 4*
      f1(6,19) -> 4*
      f1(6,21) -> 4*
      f1(1,21) -> 4*
      b1(20) -> 21*
      b1(7) -> 8*
      b1(2) -> 5*
      b1(41) -> 21*
      b1(36) -> 21*
      b1(21) -> 21*
      b1(1) -> 5*
      b1(8) -> 5*
      b1(3) -> 5*
      c1(5) -> 19*
      c1(41) -> 21*
      c1(36) -> 21*
      c1(21) -> 21*
      c1(6) -> 7*
      a1(5) -> 6*
      a1(19) -> 20*
      a1(41) -> 21*
      a1(36) -> 21*
      a1(21) -> 21*
      f2(6,39) -> 4*
      f2(6,41) -> 4*
      f2(1,41) -> 4*
      f2(7,36) -> 4*
      f2(2,36) -> 4*
      f2(8,41) -> 4*
      f2(3,41) -> 4*
      f2(29,36) -> 4*
      f2(5,41) -> 4*
      f2(26,40) -> 4*
      f2(1,36) -> 4*
      f2(27,39) -> 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,41) -> 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(7) -> 26*
      b2(2) -> 26*
      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*
      b0(2) -> 2*
      b0(1) -> 2*
      b0(3) -> 2*
      a2(39) -> 40*
      a2(41) -> 41*
      a2(26) -> 27*
      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) -> 34*
       b3(17) -> 29*
       b3(12) -> 29*
       b3(9) -> 29*
       b3(41) -> 27*
       b3(31) -> 32*
       b3(26) -> 27*
       b3(16) -> 35*
       c3(35) -> 37*
       c3(30) -> 31*
       c3(34) -> 39*
       a3(25) -> 26*
       a3(39) -> 26*
       a3(29) -> 30*
       a3(16) -> 26*
       f4(29,38) -> 4*
       f4(17,41) -> 4*
       f4(12,41) -> 4*
       f4(9,41) -> 4*
       b4(38) -> 41*
       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*
       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*
       a4(37) -> 38*
       a4(39) -> 38*
       b1(20) -> 9*
       b1(10) -> 9*
       b1(5) -> 5*
       b1(27) -> 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(27) -> 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(41) -> 16*
       b2(16) -> 16*
       b2(11) -> 17*
       b2(1) -> 17*
       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,39) -> 4*
       f3(19,34) -> 4*
       f3(20,27) -> 4*
       f3(10,27) -> 4*
       f3(30,37) -> 4*
       f3(30,39) -> 4*
       f3(31,34) -> 4*
       f3(32,27) -> 4*
       f3(12,27) -> 4*
       f3(2,27) -> 4*
       f3(9,27) -> 4*
       f3(11,27) -> 4*
       f3(1,27) -> 4*
       f3(31,35) -> 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