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))
   Bounds Processor:
    bound: 1
    enrichment: match-dp
    automaton:
     final states: {13}
     transitions:
      a1(31) -> 32*
      f50() -> 14*
      b1(32) -> 33*
      b1(33) -> 38*
      f{#,0}(14,32) -> 13*
      f{#,0}(25,15) -> 13*
      f{#,0}(14,38) -> 13*
      f{#,0}(25,23) -> 13*
      f{#,0}(26,14) -> 13*
      f{#,0}(26,38) -> 13*
      f{#,0}(14,15) -> 13*
      f{#,0}(14,31) -> 13*
      f{#,0}(26,15) -> 13*
      f{#,0}(26,23) -> 13*
      f{#,0}(26,31) -> 13*
      c1(15) -> 31*
      c1(38) -> 31*
      c1(33) -> 31*
      c1(23) -> 31*
      b0(25) -> 26*
      b0(15) -> 15*
      b0(14) -> 23*
      b0(31) -> 15*
      b0(26) -> 23*
      b0(38) -> 15*
      b0(23) -> 15*
      c0(15) -> 15*
      c0(32) -> 15*
      c0(24) -> 25*
      c0(14) -> 15*
      c0(31) -> 15*
      a0(15) -> 15*
      a0(32) -> 15*
      a0(26) -> 24*
      a0(38) -> 15*
      a0(33) -> 15*
      a0(23) -> 24*
      f{#,1}(25,33) -> 13*
      f{#,1}(26,32) -> 13*
      f{#,1}(23,32) -> 13*
      f{#,1}(24,31) -> 13*
      f{#,1}(14,33) -> 13*
      f{#,1}(25,38) -> 13*
      f{#,1}(26,33) -> 13*
    problem:
     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))
     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,
      
      [b](x0) = x0,
      
      [c](x0) = x0 + 1
     orientation:
      f#(x,a(b(c(y)))) = y + 1 >= y = f#(b(c(a(b(x)))),y)
      
      f#(a(x),y) = y >= y = f#(x,a(y))
      
      f#(b(x),y) = y >= y = f#(x,b(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#(a(x),y) -> f#(x,a(y))
       f#(b(x),y) -> f#(x,b(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