YES

Problem:
 a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
 a(a(x)) -> f(b(),a(f(a(x),b())))
 f(a(x),b()) -> f(b(),a(x))

Proof:
 DP Processor:
  DPs:
   a#(a(f(b(),a(x)))) -> a#(a(x))
   a#(a(f(b(),a(x)))) -> a#(a(a(x)))
   a#(a(f(b(),a(x)))) -> f#(a(a(a(x))),b())
   a#(a(x)) -> f#(a(x),b())
   a#(a(x)) -> a#(f(a(x),b()))
   a#(a(x)) -> f#(b(),a(f(a(x),b())))
   f#(a(x),b()) -> f#(b(),a(x))
  TRS:
   a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
   a(a(x)) -> f(b(),a(f(a(x),b())))
   f(a(x),b()) -> f(b(),a(x))
  TDG Processor:
   DPs:
    a#(a(f(b(),a(x)))) -> a#(a(x))
    a#(a(f(b(),a(x)))) -> a#(a(a(x)))
    a#(a(f(b(),a(x)))) -> f#(a(a(a(x))),b())
    a#(a(x)) -> f#(a(x),b())
    a#(a(x)) -> a#(f(a(x),b()))
    a#(a(x)) -> f#(b(),a(f(a(x),b())))
    f#(a(x),b()) -> f#(b(),a(x))
   TRS:
    a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
    a(a(x)) -> f(b(),a(f(a(x),b())))
    f(a(x),b()) -> f(b(),a(x))
   graph:
    f#(a(x),b()) -> f#(b(),a(x)) ->
    f#(a(x),b()) -> f#(b(),a(x))
    a#(a(f(b(),a(x)))) -> f#(a(a(a(x))),b()) ->
    f#(a(x),b()) -> f#(b(),a(x))
    a#(a(f(b(),a(x)))) -> a#(a(a(x))) ->
    a#(a(x)) -> f#(b(),a(f(a(x),b())))
    a#(a(f(b(),a(x)))) -> a#(a(a(x))) ->
    a#(a(x)) -> a#(f(a(x),b()))
    a#(a(f(b(),a(x)))) -> a#(a(a(x))) -> a#(a(x)) -> f#(a(x),b())
    a#(a(f(b(),a(x)))) -> a#(a(a(x))) ->
    a#(a(f(b(),a(x)))) -> f#(a(a(a(x))),b())
    a#(a(f(b(),a(x)))) -> a#(a(a(x))) ->
    a#(a(f(b(),a(x)))) -> a#(a(a(x)))
    a#(a(f(b(),a(x)))) -> a#(a(a(x))) ->
    a#(a(f(b(),a(x)))) -> a#(a(x))
    a#(a(f(b(),a(x)))) -> a#(a(x)) ->
    a#(a(x)) -> f#(b(),a(f(a(x),b())))
    a#(a(f(b(),a(x)))) -> a#(a(x)) -> a#(a(x)) -> a#(f(a(x),b()))
    a#(a(f(b(),a(x)))) -> a#(a(x)) -> a#(a(x)) -> f#(a(x),b())
    a#(a(f(b(),a(x)))) -> a#(a(x)) ->
    a#(a(f(b(),a(x)))) -> f#(a(a(a(x))),b())
    a#(a(f(b(),a(x)))) -> a#(a(x)) ->
    a#(a(f(b(),a(x)))) -> a#(a(a(x)))
    a#(a(f(b(),a(x)))) -> a#(a(x)) -> a#(a(f(b(),a(x)))) -> a#(a(x))
    a#(a(x)) -> f#(a(x),b()) -> f#(a(x),b()) -> f#(b(),a(x))
    a#(a(x)) -> f#(b(),a(f(a(x),b()))) -> f#(a(x),b()) -> f#(b(),a(x))
    a#(a(x)) -> a#(f(a(x),b())) -> a#(a(x)) -> f#(b(),a(f(a(x),b())))
    a#(a(x)) -> a#(f(a(x),b())) -> a#(a(x)) -> a#(f(a(x),b()))
    a#(a(x)) -> a#(f(a(x),b())) -> a#(a(x)) -> f#(a(x),b())
    a#(a(x)) -> a#(f(a(x),b())) ->
    a#(a(f(b(),a(x)))) -> f#(a(a(a(x))),b())
    a#(a(x)) -> a#(f(a(x),b())) -> a#(a(f(b(),a(x)))) -> a#(a(a(x)))
    a#(a(x)) -> a#(f(a(x),b())) -> a#(a(f(b(),a(x)))) -> a#(a(x))
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 22/49
    DPs:
     a#(a(f(b(),a(x)))) -> a#(a(a(x)))
     a#(a(f(b(),a(x)))) -> a#(a(x))
     a#(a(x)) -> a#(f(a(x),b()))
    TRS:
     a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
     a(a(x)) -> f(b(),a(f(a(x),b())))
     f(a(x),b()) -> f(b(),a(x))
    EDG Processor:
     DPs:
      a#(a(f(b(),a(x)))) -> a#(a(a(x)))
      a#(a(f(b(),a(x)))) -> a#(a(x))
      a#(a(x)) -> a#(f(a(x),b()))
     TRS:
      a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
      a(a(x)) -> f(b(),a(f(a(x),b())))
      f(a(x),b()) -> f(b(),a(x))
     graph:
      a#(a(f(b(),a(x)))) -> a#(a(a(x))) ->
      a#(a(f(b(),a(x)))) -> a#(a(x))
      a#(a(f(b(),a(x)))) -> a#(a(a(x))) ->
      a#(a(f(b(),a(x)))) -> a#(a(a(x)))
      a#(a(f(b(),a(x)))) -> a#(a(a(x))) ->
      a#(a(x)) -> a#(f(a(x),b()))
      a#(a(f(b(),a(x)))) -> a#(a(x)) ->
      a#(a(f(b(),a(x)))) -> a#(a(x))
      a#(a(f(b(),a(x)))) -> a#(a(x)) ->
      a#(a(f(b(),a(x)))) -> a#(a(a(x)))
      a#(a(f(b(),a(x)))) -> a#(a(x)) -> a#(a(x)) -> a#(f(a(x),b()))
     SCC Processor:
      #sccs: 1
      #rules: 2
      #arcs: 6/9
      DPs:
       a#(a(f(b(),a(x)))) -> a#(a(a(x)))
       a#(a(f(b(),a(x)))) -> a#(a(x))
      TRS:
       a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
       a(a(x)) -> f(b(),a(f(a(x),b())))
       f(a(x),b()) -> f(b(),a(x))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [a#](x0) = x0 + 2,
        
        [f](x0, x1) = x0 + x1 + -16,
        
        [a](x0) = 2x0 + 1,
        
        [b] = 0
       orientation:
        a#(a(f(b(),a(x)))) = 4x + 3 >= 4x + 3 = a#(a(a(x)))
        
        a#(a(f(b(),a(x)))) = 4x + 3 >= 2x + 2 = a#(a(x))
        
        a(a(f(b(),a(x)))) = 6x + 5 >= 6x + 5 = f(a(a(a(x))),b())
        
        a(a(x)) = 4x + 3 >= 4x + 3 = f(b(),a(f(a(x),b())))
        
        f(a(x),b()) = 2x + 1 >= 2x + 1 = f(b(),a(x))
       problem:
        DPs:
         a#(a(f(b(),a(x)))) -> a#(a(a(x)))
        TRS:
         a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
         a(a(x)) -> f(b(),a(f(a(x),b())))
         f(a(x),b()) -> f(b(),a(x))
       Arctic Interpretation Processor:
        dimension: 2
        interpretation:
         [a#](x0) = [0  -&]x0 + [0],
         
                       [-& -&]     [-& -&]     [0 ]
         [f](x0, x1) = [-& 1 ]x0 + [-& 1 ]x1 + [-&],
         
                   [-& 0 ]     [1]
         [a](x0) = [1  -&]x0 + [1],
         
               [0 ]
         [b] = [-&]
        orientation:
         a#(a(f(b(),a(x)))) = [2  -&]x + [2] >= [1  -&]x + [1] = a#(a(a(x)))
         
                             [-& -&]    [1]    [-& -&]    [0]                    
         a(a(f(b(),a(x)))) = [3  -&]x + [3] >= [3  -&]x + [3] = f(a(a(a(x))),b())
         
                   [1  -&]    [1]    [0]                        
         a(a(x)) = [-& 1 ]x + [2] >= [2] = f(b(),a(f(a(x),b())))
         
                       [-& -&]    [0]    [-& -&]    [0]              
         f(a(x),b()) = [2  -&]x + [2] >= [2  -&]x + [2] = f(b(),a(x))
        problem:
         DPs:
          
         TRS:
          a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
          a(a(x)) -> f(b(),a(f(a(x),b())))
          f(a(x),b()) -> f(b(),a(x))
        Qed
    
    DPs:
     f#(a(x),b()) -> f#(b(),a(x))
    TRS:
     a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
     a(a(x)) -> f(b(),a(f(a(x),b())))
     f(a(x),b()) -> f(b(),a(x))
    EDG Processor:
     DPs:
      f#(a(x),b()) -> f#(b(),a(x))
     TRS:
      a(a(f(b(),a(x)))) -> f(a(a(a(x))),b())
      a(a(x)) -> f(b(),a(f(a(x),b())))
      f(a(x),b()) -> f(b(),a(x))
     graph:
      
     Qed