YES

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:
 DP Processor:
  DPs:
   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))
  TRS:
   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))
  EDG Processor:
   DPs:
    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))
   TRS:
    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))
   graph:
    f#(a(x),y) -> f#(x,a(y)) -> f#(x,a(b(c(y)))) -> f#(b(c(a(b(x)))),y)
    f#(a(x),y) -> f#(x,a(y)) -> f#(a(x),y) -> f#(x,a(y))
    f#(a(x),y) -> f#(x,a(y)) -> f#(b(x),y) -> f#(x,b(y))
    f#(a(x),y) -> f#(x,a(y)) -> f#(c(x),y) -> f#(x,c(y))
    f#(b(x),y) -> f#(x,b(y)) -> f#(a(x),y) -> f#(x,a(y))
    f#(b(x),y) -> f#(x,b(y)) -> f#(b(x),y) -> f#(x,b(y))
    f#(b(x),y) -> f#(x,b(y)) -> f#(c(x),y) -> f#(x,c(y))
    f#(c(x),y) -> f#(x,c(y)) -> f#(a(x),y) -> f#(x,a(y))
    f#(c(x),y) -> f#(x,c(y)) -> f#(b(x),y) -> f#(x,b(y))
    f#(c(x),y) -> f#(x,c(y)) -> f#(c(x),y) -> f#(x,c(y))
    f#(x,a(b(c(y)))) -> f#(b(c(a(b(x)))),y) ->
    f#(x,a(b(c(y)))) -> f#(b(c(a(b(x)))),y)
    f#(x,a(b(c(y)))) -> f#(b(c(a(b(x)))),y) -> f#(b(x),y) -> f#(x,b(y))
   Usable Rule Processor:
    DPs:
     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))
    TRS:
     
    Bounds Processor:
     bound: 4
     enrichment: match-dp
     automaton:
      final states: {16}
      transitions:
       c2(102) -> 103*
       c2(106) -> 95*
       c2(113) -> 122*
       c2(115) -> 124*
       c2(95) -> 95*
       a2(106) -> 77*
       a2(101) -> 102*
       a2(76) -> 77*
       a2(41) -> 100*
       a2(36) -> 77*
       a2(95) -> 77*
       c3(142) -> 152*
       c3(137) -> 138*
       c3(144) -> 154*
       c3(140) -> 150*
       a3(152) -> 123*
       a3(122) -> 123*
       a3(124) -> 125*
       a3(136) -> 137*
       a3(106) -> 123*
       a3(150) -> 123*
       a3(95) -> 123*
       f{#,4}(101,158) -> 12,15,16
       f{#,4}(136,155) -> 12,15,16
       b4(155) -> 158*
       f{#,0}(12,14) -> 12*
       f{#,0}(13,11) -> 12*
       f{#,0}(13,13) -> 12*
       f{#,0}(14,12) -> 12*
       f{#,0}(14,14) -> 12*
       f{#,0}(60,11) -> 16*
       f{#,0}(60,13) -> 16*
       f{#,0}(15,17) -> 16*
       f{#,0}(11,12) -> 12*
       f{#,0}(11,14) -> 12*
       f{#,0}(12,11) -> 12*
       f{#,0}(12,13) -> 12*
       f{#,0}(58,14) -> 16*
       f{#,0}(13,12) -> 12*
       f{#,0}(13,14) -> 12*
       f{#,0}(59,13) -> 16*
       f{#,0}(14,11) -> 12*
       f{#,0}(14,13) -> 12*
       f{#,0}(60,12) -> 16*
       f{#,0}(60,14) -> 16*
       f{#,0}(11,11) -> 12*
       f{#,0}(11,13) -> 12*
       f{#,0}(12,12) -> 12*
       a0(15) -> 17*
       a0(57) -> 58*
       a0(12) -> 11*
       a0(14) -> 11*
       a0(11) -> 11*
       a0(13) -> 11*
       b0(60) -> 57*
       b0(15) -> 57*
       b0(17) -> 17*
       b0(12) -> 13*
       b0(59) -> 60*
       b0(14) -> 13*
       b0(11) -> 13*
       b0(13) -> 13*
       a4(154) -> 155*
       c0(17) -> 17*
       c0(12) -> 14*
       c0(14) -> 14*
       c0(11) -> 14*
       c0(58) -> 59*
       c0(13) -> 14*
       f{#,1}(11,41) -> 16*
       f{#,1}(59,95) -> 16*
       f{#,1}(57,36) -> 12,15,16
       f{#,1}(49,95) -> 16*
       f{#,1}(47,36) -> 16,12,15
       f{#,1}(12,36) -> 12*
       f{#,1}(103,41) -> 16*
       f{#,1}(49,12) -> 16,12
       f{#,1}(49,14) -> 16,12
       f{#,1}(48,41) -> 16*
       f{#,1}(13,41) -> 16*
       f{#,1}(59,36) -> 12,15,16
       f{#,1}(49,36) -> 16,12,15
       f{#,1}(47,76) -> 16,12,15
       f{#,1}(14,36) -> 12*
       f{#,1}(11,36) -> 12*
       f{#,1}(102,41) -> 16*
       f{#,1}(47,41) -> 16*
       f{#,1}(49,106) -> 12,15
       f{#,1}(104,17) -> 16*
       f{#,1}(12,41) -> 16*
       f{#,1}(49,11) -> 16,12
       f{#,1}(60,95) -> 16*
       f{#,1}(49,13) -> 16,12
       f{#,1}(58,36) -> 12,15,16
       f{#,1}(48,36) -> 16,12,15
       f{#,1}(49,17) -> 16*
       f{#,1}(15,95) -> 16*
       f{#,1}(13,36) -> 12*
       f{#,1}(48,46) -> 16,12,15
       f{#,1}(49,41) -> 16*
       f{#,1}(14,41) -> 16*
       f{#,1}(60,36) -> 12,15,16
       f{#,1}(15,36) -> 12,15,16
       b1(60) -> 46*
       b1(15) -> 46*
       b1(102) -> 46*
       b1(57) -> 46*
       b1(47) -> 46*
       b1(17) -> 41*
       b1(12) -> 46*
       b1(104) -> 46*
       b1(59) -> 46*
       b1(49) -> 46*
       b1(14) -> 46*
       b1(41) -> 41*
       b1(36) -> 36*
       b1(11) -> 46*
       b1(58) -> 46*
       b1(48) -> 49*
       b1(13) -> 46*
       b1(95) -> 36*
       c1(47) -> 48*
       c1(106) -> 36*
       c1(46) -> 76*
       c1(41) -> 41*
       c1(36) -> 36*
       c1(95) -> 36*
       a1(17) -> 41*
       a1(12) -> 36*
       a1(104) -> 47*
       a1(49) -> 47*
       a1(14) -> 36*
       a1(106) -> 36*
       a1(46) -> 47*
       a1(41) -> 41*
       a1(36) -> 36*
       a1(11) -> 36*
       a1(13) -> 36*
       a1(95) -> 36*
       f{#,2}(104,95) -> 12,15,16
       f{#,2}(58,106) -> 16*
       f{#,2}(48,106) -> 16*
       f{#,2}(59,95) -> 12,15,16
       f{#,2}(13,106) -> 16*
       f{#,2}(49,95) -> 16,12,15
       f{#,2}(14,95) -> 16,12,15
       f{#,2}(46,77) -> 16,12,15
       f{#,2}(60,106) -> 16*
       f{#,2}(101,95) -> 16*
       f{#,2}(104,36) -> 16,12,15
       f{#,2}(15,106) -> 16*
       f{#,2}(46,95) -> 16*
       f{#,2}(11,95) -> 16,12,15
       f{#,2}(102,106) -> 16*
       f{#,2}(103,95) -> 12,15,16
       f{#,2}(57,106) -> 16*
       f{#,2}(47,106) -> 16*
       f{#,2}(58,95) -> 12,15,16
       f{#,2}(12,106) -> 16*
       f{#,2}(48,95) -> 16,12,15
       f{#,2}(13,95) -> 16,12,15
       f{#,2}(104,100) -> 16*
       f{#,2}(104,106) -> 12,15,16
       f{#,2}(49,100) -> 16*
       f{#,2}(59,106) -> 16*
       f{#,2}(49,106) -> 16*
       f{#,2}(102,122) -> 16*
       f{#,2}(102,124) -> 16,12,15
       f{#,2}(60,95) -> 12,15,16
       f{#,2}(14,106) -> 16*
       f{#,2}(103,113) -> 16*
       f{#,2}(103,115) -> 16,12,15
       f{#,2}(15,95) -> 12,15,16
       f{#,2}(101,100) -> 16*
       f{#,2}(104,41) -> 16*
       f{#,2}(101,106) -> 16*
       f{#,2}(46,100) -> 16*
       f{#,2}(102,95) -> 12,15,16
       f{#,2}(46,106) -> 16*
       f{#,2}(57,95) -> 16,12,15
       f{#,2}(11,106) -> 16*
       f{#,2}(47,95) -> 12,15,16
       f{#,2}(12,95) -> 16,12,15
       f{#,2}(104,77) -> 12,15,16
       f{#,2}(103,106) -> 16*
       f{#,2}(49,77) -> 16,12,15
       b2(142) -> 95*
       b2(127) -> 95*
       b2(77) -> 95*
       b2(104) -> 101*
       b2(49) -> 101*
       b2(126) -> 95*
       b2(106) -> 95*
       b2(101) -> 101*
       b2(46) -> 101*
       b2(41) -> 113*
       b2(36) -> 115*
       b2(103) -> 104*
       b2(140) -> 95*
       b2(100) -> 106*
       b2(95) -> 95*
       f{#,3}(101,126) -> 12,15,16
       f{#,3}(46,126) -> 12,15,16
       f{#,3}(101,140) -> 12,15,16
       f{#,3}(101,142) -> 12,15,16
       f{#,3}(46,140) -> 12,15,16
       f{#,3}(46,142) -> 12,15,16
       f{#,3}(138,144) -> 12,15,16
       f{#,3}(103,140) -> 12,15,16
       f{#,3}(103,142) -> 16,12,15
       f{#,3}(104,127) -> 16,12,15
       f{#,3}(49,127) -> 16,12,15
       f{#,3}(101,123) -> 12,15,16
       f{#,3}(139,106) -> 12,15,16
       f{#,3}(101,125) -> 16,12,15
       f{#,3}(101,127) -> 12,15,16
       f{#,3}(46,127) -> 16,12,15
       f{#,3}(137,154) -> 12,15,16
       f{#,3}(102,150) -> 12,15,16
       f{#,3}(102,152) -> 16,12,15
       f{#,3}(104,126) -> 12,15,16
       f{#,3}(49,126) -> 12,15,16
       f{#,3}(104,140) -> 12,15,16
       f{#,3}(104,142) -> 12,15,16
       f{#,3}(49,140) -> 12,15,16
       f{#,3}(139,95) -> 12,15,16
       f{#,3}(49,142) -> 12,15,16
       b3(142) -> 140*
       b3(127) -> 142*
       b3(126) -> 140*
       b3(106) -> 144*
       b3(101) -> 136*
       b3(158) -> 126*
       b3(138) -> 139*
       b3(123) -> 126*
       b3(140) -> 140*
       b3(125) -> 127*
       b3(95) -> 144*
       11 -> 15*
       12 -> 15*
       13 -> 15*
       14 -> 15*
     problem:
      DPs:
       f#(x,a(b(c(y)))) -> f#(b(c(a(b(x)))),y)
       f#(b(x),y) -> f#(x,b(y))
       f#(c(x),y) -> f#(x,c(y))
      TRS:
       
     Restore Modifier:
      DPs:
       f#(x,a(b(c(y)))) -> f#(b(c(a(b(x)))),y)
       f#(b(x),y) -> f#(x,b(y))
       f#(c(x),y) -> f#(x,c(y))
      TRS:
       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))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1) = x1,
        
        [f](x0, x1) = 0,
        
        [a](x0) = x0 + 1,
        
        [b](x0) = x0,
        
        [c](x0) = x0
       orientation:
        f#(x,a(b(c(y)))) = y + 1 >= y = f#(b(c(a(b(x)))),y)
        
        f#(b(x),y) = y >= y = f#(x,b(y))
        
        f#(c(x),y) = y >= y = f#(x,c(y))
        
        f(x,a(b(c(y)))) = 0 >= 0 = f(b(c(a(b(x)))),y)
        
        f(a(x),y) = 0 >= 0 = f(x,a(y))
        
        f(b(x),y) = 0 >= 0 = f(x,b(y))
        
        f(c(x),y) = 0 >= 0 = f(x,c(y))
       problem:
        DPs:
         f#(b(x),y) -> f#(x,b(y))
         f#(c(x),y) -> f#(x,c(y))
        TRS:
         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))
       Subterm Criterion Processor:
        simple projection:
         pi(f#) = 0
        problem:
         DPs:
          
         TRS:
          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))
        Qed