YES

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

Proof:
 DP Processor:
  DPs:
   +#(a(),b()) -> +#(b(),a())
   +#(a(),+(b(),z)) -> +#(a(),z)
   +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   f#(+(x,y),z) -> f#(y,z)
   f#(+(x,y),z) -> f#(x,z)
   f#(+(x,y),z) -> +#(f(x,z),f(y,z))
  TRS:
   +(a(),b()) -> +(b(),a())
   +(a(),+(b(),z)) -> +(b(),+(a(),z))
   +(+(x,y),z) -> +(x,+(y,z))
   f(a(),y) -> a()
   f(b(),y) -> b()
   f(+(x,y),z) -> +(f(x,z),f(y,z))
  TDG Processor:
   DPs:
    +#(a(),b()) -> +#(b(),a())
    +#(a(),+(b(),z)) -> +#(a(),z)
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z))
    f#(+(x,y),z) -> f#(y,z)
    f#(+(x,y),z) -> f#(x,z)
    f#(+(x,y),z) -> +#(f(x,z),f(y,z))
   TRS:
    +(a(),b()) -> +(b(),a())
    +(a(),+(b(),z)) -> +(b(),+(a(),z))
    +(+(x,y),z) -> +(x,+(y,z))
    f(a(),y) -> a()
    f(b(),y) -> b()
    f(+(x,y),z) -> +(f(x,z),f(y,z))
   graph:
    f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z))
    f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(x,z)
    f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(y,z)
    f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z))
    f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(x,z)
    f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(y,z)
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) ->
    +#(+(x,y),z) -> +#(x,+(y,z))
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(y,z)
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) ->
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) ->
    +#(a(),+(b(),z)) -> +#(a(),z)
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),b()) -> +#(b(),a())
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(a(),z)
    +#(+(x,y),z) -> +#(y,z) -> +#(a(),b()) -> +#(b(),a())
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z)) ->
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),b()) -> +#(b(),a())
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) ->
    +#(+(x,y),z) -> +#(x,+(y,z))
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) ->
    +#(+(x,y),z) -> +#(y,z)
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) ->
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) ->
    +#(a(),+(b(),z)) -> +#(a(),z)
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) -> +#(a(),b()) -> +#(b(),a())
    +#(a(),+(b(),z)) -> +#(a(),z) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(a(),+(b(),z)) -> +#(a(),z) -> +#(+(x,y),z) -> +#(y,z)
    +#(a(),+(b(),z)) -> +#(a(),z) ->
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(a(),z)
    +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),b()) -> +#(b(),a())
    +#(a(),b()) -> +#(b(),a()) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(a(),b()) -> +#(b(),a()) -> +#(+(x,y),z) -> +#(y,z)
    +#(a(),b()) -> +#(b(),a()) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(a(),b()) -> +#(b(),a()) -> +#(a(),+(b(),z)) -> +#(a(),z)
    +#(a(),b()) -> +#(b(),a()) -> +#(a(),b()) -> +#(b(),a())
   Restore Modifier:
    DPs:
     +#(a(),b()) -> +#(b(),a())
     +#(a(),+(b(),z)) -> +#(a(),z)
     +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
     +#(+(x,y),z) -> +#(y,z)
     +#(+(x,y),z) -> +#(x,+(y,z))
     f#(+(x,y),z) -> f#(y,z)
     f#(+(x,y),z) -> f#(x,z)
     f#(+(x,y),z) -> +#(f(x,z),f(y,z))
    TRS:
     +(a(),b()) -> +(b(),a())
     +(a(),+(b(),z)) -> +(b(),+(a(),z))
     +(+(x,y),z) -> +(x,+(y,z))
     f(a(),y) -> a()
     f(b(),y) -> b()
     f(+(x,y),z) -> +(f(x,z),f(y,z))
    SCC Processor:
     #sccs: 2
     #rules: 7
     #arcs: 36/64
     DPs:
      f#(+(x,y),z) -> f#(y,z)
      f#(+(x,y),z) -> f#(x,z)
     TRS:
      +(a(),b()) -> +(b(),a())
      +(a(),+(b(),z)) -> +(b(),+(a(),z))
      +(+(x,y),z) -> +(x,+(y,z))
      f(a(),y) -> a()
      f(b(),y) -> b()
      f(+(x,y),z) -> +(f(x,z),f(y,z))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [f#](x0, x1) = x0 + 1,
       
       [f](x0, x1) = x0,
       
       [+](x0, x1) = x0 + x1 + 1,
       
       [b] = 0,
       
       [a] = 0
      orientation:
       f#(+(x,y),z) = x + y + 2 >= y + 1 = f#(y,z)
       
       f#(+(x,y),z) = x + y + 2 >= x + 1 = f#(x,z)
       
       +(a(),b()) = 1 >= 1 = +(b(),a())
       
       +(a(),+(b(),z)) = z + 2 >= z + 2 = +(b(),+(a(),z))
       
       +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z))
       
       f(a(),y) = 0 >= 0 = a()
       
       f(b(),y) = 0 >= 0 = b()
       
       f(+(x,y),z) = x + y + 1 >= x + y + 1 = +(f(x,z),f(y,z))
      problem:
       DPs:
        
       TRS:
        +(a(),b()) -> +(b(),a())
        +(a(),+(b(),z)) -> +(b(),+(a(),z))
        +(+(x,y),z) -> +(x,+(y,z))
        f(a(),y) -> a()
        f(b(),y) -> b()
        f(+(x,y),z) -> +(f(x,z),f(y,z))
      Qed
     
     DPs:
      +#(a(),b()) -> +#(b(),a())
      +#(a(),+(b(),z)) -> +#(a(),z)
      +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
      +#(+(x,y),z) -> +#(y,z)
      +#(+(x,y),z) -> +#(x,+(y,z))
     TRS:
      +(a(),b()) -> +(b(),a())
      +(a(),+(b(),z)) -> +(b(),+(a(),z))
      +(+(x,y),z) -> +(x,+(y,z))
      f(a(),y) -> a()
      f(b(),y) -> b()
      f(+(x,y),z) -> +(f(x,z),f(y,z))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [+#](x0, x1) = x0,
       
       [f](x0, x1) = x0,
       
       [+](x0, x1) = x0 + x1 + 1,
       
       [b] = 0,
       
       [a] = 0
      orientation:
       +#(a(),b()) = 0 >= 0 = +#(b(),a())
       
       +#(a(),+(b(),z)) = 0 >= 0 = +#(a(),z)
       
       +#(a(),+(b(),z)) = 0 >= 0 = +#(b(),+(a(),z))
       
       +#(+(x,y),z) = x + y + 1 >= y = +#(y,z)
       
       +#(+(x,y),z) = x + y + 1 >= x = +#(x,+(y,z))
       
       +(a(),b()) = 1 >= 1 = +(b(),a())
       
       +(a(),+(b(),z)) = z + 2 >= z + 2 = +(b(),+(a(),z))
       
       +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z))
       
       f(a(),y) = 0 >= 0 = a()
       
       f(b(),y) = 0 >= 0 = b()
       
       f(+(x,y),z) = x + y + 1 >= x + y + 1 = +(f(x,z),f(y,z))
      problem:
       DPs:
        +#(a(),b()) -> +#(b(),a())
        +#(a(),+(b(),z)) -> +#(a(),z)
        +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
       TRS:
        +(a(),b()) -> +(b(),a())
        +(a(),+(b(),z)) -> +(b(),+(a(),z))
        +(+(x,y),z) -> +(x,+(y,z))
        f(a(),y) -> a()
        f(b(),y) -> b()
        f(+(x,y),z) -> +(f(x,z),f(y,z))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [+#](x0, x1) = x0 + x1,
        
        [f](x0, x1) = x0,
        
        [+](x0, x1) = x0 + x1,
        
        [b] = 1,
        
        [a] = 0
       orientation:
        +#(a(),b()) = 1 >= 1 = +#(b(),a())
        
        +#(a(),+(b(),z)) = z + 1 >= z = +#(a(),z)
        
        +#(a(),+(b(),z)) = z + 1 >= z + 1 = +#(b(),+(a(),z))
        
        +(a(),b()) = 1 >= 1 = +(b(),a())
        
        +(a(),+(b(),z)) = z + 1 >= z + 1 = +(b(),+(a(),z))
        
        +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
        
        f(a(),y) = 0 >= 0 = a()
        
        f(b(),y) = 1 >= 1 = b()
        
        f(+(x,y),z) = x + y >= x + y = +(f(x,z),f(y,z))
       problem:
        DPs:
         +#(a(),b()) -> +#(b(),a())
         +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
        TRS:
         +(a(),b()) -> +(b(),a())
         +(a(),+(b(),z)) -> +(b(),+(a(),z))
         +(+(x,y),z) -> +(x,+(y,z))
         f(a(),y) -> a()
         f(b(),y) -> b()
         f(+(x,y),z) -> +(f(x,z),f(y,z))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [+#](x0, x1) = x0 + x1 + 1,
         
         [f](x0, x1) = x0,
         
         [+](x0, x1) = 1,
         
         [b] = 0,
         
         [a] = 1
        orientation:
         +#(a(),b()) = 2 >= 2 = +#(b(),a())
         
         +#(a(),+(b(),z)) = 3 >= 2 = +#(b(),+(a(),z))
         
         +(a(),b()) = 1 >= 1 = +(b(),a())
         
         +(a(),+(b(),z)) = 1 >= 1 = +(b(),+(a(),z))
         
         +(+(x,y),z) = 1 >= 1 = +(x,+(y,z))
         
         f(a(),y) = 1 >= 1 = a()
         
         f(b(),y) = 0 >= 0 = b()
         
         f(+(x,y),z) = 1 >= 1 = +(f(x,z),f(y,z))
        problem:
         DPs:
          +#(a(),b()) -> +#(b(),a())
         TRS:
          +(a(),b()) -> +(b(),a())
          +(a(),+(b(),z)) -> +(b(),+(a(),z))
          +(+(x,y),z) -> +(x,+(y,z))
          f(a(),y) -> a()
          f(b(),y) -> b()
          f(+(x,y),z) -> +(f(x,z),f(y,z))
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [+#](x0, x1) = x1,
          
          [f](x0, x1) = x0,
          
          [+](x0, x1) = 0,
          
          [b] = 1,
          
          [a] = 0
         orientation:
          +#(a(),b()) = 1 >= 0 = +#(b(),a())
          
          +(a(),b()) = 0 >= 0 = +(b(),a())
          
          +(a(),+(b(),z)) = 0 >= 0 = +(b(),+(a(),z))
          
          +(+(x,y),z) = 0 >= 0 = +(x,+(y,z))
          
          f(a(),y) = 0 >= 0 = a()
          
          f(b(),y) = 1 >= 1 = b()
          
          f(+(x,y),z) = 0 >= 0 = +(f(x,z),f(y,z))
         problem:
          DPs:
           
          TRS:
           +(a(),b()) -> +(b(),a())
           +(a(),+(b(),z)) -> +(b(),+(a(),z))
           +(+(x,y),z) -> +(x,+(y,z))
           f(a(),y) -> a()
           f(b(),y) -> b()
           f(+(x,y),z) -> +(f(x,z),f(y,z))
         Qed