YES

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

Proof:
 DP Processor:
  DPs:
   f#(a(),f(b(),x)) -> f#(a(),x)
   f#(a(),f(b(),x)) -> f#(a(),f(a(),x))
   f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x)))
   f#(b(),f(a(),x)) -> f#(b(),x)
   f#(b(),f(a(),x)) -> f#(b(),f(b(),x))
   f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x)))
  TRS:
   f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
   f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
  EDG Processor:
   DPs:
    f#(a(),f(b(),x)) -> f#(a(),x)
    f#(a(),f(b(),x)) -> f#(a(),f(a(),x))
    f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x)))
    f#(b(),f(a(),x)) -> f#(b(),x)
    f#(b(),f(a(),x)) -> f#(b(),f(b(),x))
    f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x)))
   TRS:
    f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
    f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
   graph:
    f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) ->
    f#(b(),f(a(),x)) -> f#(b(),x)
    f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) ->
    f#(b(),f(a(),x)) -> f#(b(),f(b(),x))
    f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x))) ->
    f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x)))
    f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) ->
    f#(b(),f(a(),x)) -> f#(b(),x)
    f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) ->
    f#(b(),f(a(),x)) -> f#(b(),f(b(),x))
    f#(b(),f(a(),x)) -> f#(b(),f(b(),x)) ->
    f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x)))
    f#(b(),f(a(),x)) -> f#(b(),x) -> f#(b(),f(a(),x)) -> f#(b(),x)
    f#(b(),f(a(),x)) -> f#(b(),x) ->
    f#(b(),f(a(),x)) -> f#(b(),f(b(),x))
    f#(b(),f(a(),x)) -> f#(b(),x) ->
    f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x)))
    f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) ->
    f#(a(),f(b(),x)) -> f#(a(),x)
    f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) ->
    f#(a(),f(b(),x)) -> f#(a(),f(a(),x))
    f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x))) ->
    f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x)))
    f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) ->
    f#(a(),f(b(),x)) -> f#(a(),x)
    f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) ->
    f#(a(),f(b(),x)) -> f#(a(),f(a(),x))
    f#(a(),f(b(),x)) -> f#(a(),f(a(),x)) ->
    f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x)))
    f#(a(),f(b(),x)) -> f#(a(),x) -> f#(a(),f(b(),x)) -> f#(a(),x)
    f#(a(),f(b(),x)) -> f#(a(),x) ->
    f#(a(),f(b(),x)) -> f#(a(),f(a(),x))
    f#(a(),f(b(),x)) -> f#(a(),x) -> f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x)))
   SCC Processor:
    #sccs: 2
    #rules: 6
    #arcs: 18/36
    DPs:
     f#(a(),f(b(),x)) -> f#(a(),f(a(),f(a(),x)))
     f#(a(),f(b(),x)) -> f#(a(),f(a(),x))
     f#(a(),f(b(),x)) -> f#(a(),x)
    TRS:
     f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
     f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
    Bounds Processor:
     bound: 1
     enrichment: match-dp
     automaton:
      final states: {6}
      transitions:
       f{#,1}(22,24) -> 4,5
       a1() -> 22*
       f1(22,24) -> 23*
       f1(22,1) -> 23*
       f1(22,3) -> 23*
       f1(22,23) -> 24*
       f1(22,2) -> 23*
       f1(22,4) -> 23*
       f{#,0}(3,1) -> 4*
       f{#,0}(3,3) -> 4*
       f{#,0}(4,2) -> 4*
       f{#,0}(4,4) -> 4*
       f{#,0}(1,2) -> 4*
       f{#,0}(1,4) -> 4*
       f{#,0}(2,1) -> 4*
       f{#,0}(2,3) -> 4*
       f{#,0}(3,2) -> 4*
       f{#,0}(3,4) -> 4*
       f{#,0}(3,8) -> 6*
       f{#,0}(4,1) -> 4*
       f{#,0}(4,3) -> 4*
       f{#,0}(1,1) -> 4*
       f{#,0}(1,3) -> 4*
       f{#,0}(2,2) -> 4*
       f{#,0}(2,4) -> 4*
       a0() -> 3*
       f0(3,1) -> 2*
       f0(3,3) -> 2*
       f0(3,5) -> 7*
       f0(3,7) -> 8*
       f0(4,2) -> 2*
       f0(4,4) -> 2*
       f0(1,2) -> 2*
       f0(1,4) -> 2*
       f0(2,1) -> 2*
       f0(2,3) -> 2*
       f0(3,2) -> 2*
       f0(3,4) -> 2*
       f0(4,1) -> 2*
       f0(4,3) -> 2*
       f0(1,1) -> 2*
       f0(1,3) -> 2*
       f0(2,2) -> 2*
       f0(2,4) -> 2*
       b0() -> 1*
       1 -> 5*
       2 -> 5*
       3 -> 5*
       4 -> 5*
     problem:
      DPs:
       f#(a(),f(b(),x)) -> f#(a(),f(a(),x))
       f#(a(),f(b(),x)) -> f#(a(),x)
      TRS:
       f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
       f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
     Bounds Processor:
      bound: 1
      enrichment: match-dp
      automaton:
       final states: {13}
       transitions:
        f{#,1}(16,8) -> 11,13,12
        f{#,1}(16,10) -> 11,13,12
        f{#,1}(16,9) -> 11,13,12
        f{#,1}(16,11) -> 11,13,12
        a1() -> 16*
        f1(16,8) -> 8*
        f1(16,10) -> 8*
        f1(16,9) -> 8*
        f1(16,11) -> 8*
        f{#,0}(8,9) -> 11*
        f{#,0}(8,11) -> 11*
        f{#,0}(9,8) -> 11*
        f{#,0}(9,10) -> 11*
        f{#,0}(10,9) -> 11*
        f{#,0}(10,11) -> 11*
        f{#,0}(11,8) -> 11*
        f{#,0}(11,10) -> 11*
        f{#,0}(8,8) -> 11*
        f{#,0}(8,10) -> 11*
        f{#,0}(9,9) -> 11*
        f{#,0}(9,11) -> 11*
        f{#,0}(10,8) -> 11*
        f{#,0}(10,10) -> 11*
        f{#,0}(10,12) -> 13*
        f{#,0}(11,9) -> 11*
        f{#,0}(11,11) -> 11*
        a0() -> 10*
        f0(8,9) -> 9*
        f0(8,11) -> 9*
        f0(9,8) -> 9*
        f0(9,10) -> 9*
        f0(10,9) -> 9*
        f0(10,11) -> 9*
        f0(11,8) -> 9*
        f0(11,10) -> 9*
        f0(8,8) -> 9*
        f0(8,10) -> 9*
        f0(9,9) -> 9*
        f0(9,11) -> 9*
        f0(10,8) -> 9*
        f0(10,10) -> 9*
        f0(11,9) -> 9*
        f0(11,11) -> 9*
        b0() -> 8*
        8 -> 12*
        9 -> 12*
        10 -> 12*
        11 -> 12*
      problem:
       DPs:
        f#(a(),f(b(),x)) -> f#(a(),f(a(),x))
       TRS:
        f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
        f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1) = x1,
        
        [f](x0, x1) = x0,
        
        [b] = 1,
        
        [a] = 0
       orientation:
        f#(a(),f(b(),x)) = 1 >= 0 = f#(a(),f(a(),x))
        
        f(a(),f(b(),x)) = 0 >= 0 = f(a(),f(a(),f(a(),x)))
        
        f(b(),f(a(),x)) = 1 >= 1 = f(b(),f(b(),f(b(),x)))
       problem:
        DPs:
         
        TRS:
         f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
         f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
       Qed
    
    DPs:
     f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x)))
     f#(b(),f(a(),x)) -> f#(b(),f(b(),x))
     f#(b(),f(a(),x)) -> f#(b(),x)
    TRS:
     f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
     f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
    Bounds Processor:
     bound: 1
     enrichment: match-dp
     automaton:
      final states: {6}
      transitions:
       f{#,1}(22,24) -> 4,5
       f1(22,24) -> 23*
       f1(22,1) -> 23*
       f1(22,3) -> 23*
       f1(22,23) -> 24*
       f1(22,2) -> 23*
       f1(22,4) -> 23*
       b1() -> 22*
       f{#,0}(3,1) -> 4*
       f{#,0}(3,3) -> 4*
       f{#,0}(4,2) -> 4*
       f{#,0}(4,4) -> 4*
       f{#,0}(1,2) -> 4*
       f{#,0}(1,4) -> 4*
       f{#,0}(2,1) -> 4*
       f{#,0}(2,3) -> 4*
       f{#,0}(3,2) -> 4*
       f{#,0}(3,4) -> 4*
       f{#,0}(3,8) -> 6*
       f{#,0}(4,1) -> 4*
       f{#,0}(4,3) -> 4*
       f{#,0}(1,1) -> 4*
       f{#,0}(1,3) -> 4*
       f{#,0}(2,2) -> 4*
       f{#,0}(2,4) -> 4*
       a0() -> 1*
       f0(3,1) -> 2*
       f0(3,3) -> 2*
       f0(3,5) -> 7*
       f0(3,7) -> 8*
       f0(4,2) -> 2*
       f0(4,4) -> 2*
       f0(1,2) -> 2*
       f0(1,4) -> 2*
       f0(2,1) -> 2*
       f0(2,3) -> 2*
       f0(3,2) -> 2*
       f0(3,4) -> 2*
       f0(4,1) -> 2*
       f0(4,3) -> 2*
       f0(1,1) -> 2*
       f0(1,3) -> 2*
       f0(2,2) -> 2*
       f0(2,4) -> 2*
       b0() -> 3*
       1 -> 5*
       2 -> 5*
       3 -> 5*
       4 -> 5*
     problem:
      DPs:
       f#(b(),f(a(),x)) -> f#(b(),f(b(),x))
       f#(b(),f(a(),x)) -> f#(b(),x)
      TRS:
       f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
       f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
     Bounds Processor:
      bound: 1
      enrichment: match-dp
      automaton:
       final states: {13}
       transitions:
        f{#,1}(16,8) -> 11,13,12
        f{#,1}(16,10) -> 11,13,12
        f{#,1}(16,9) -> 11,13,12
        f{#,1}(16,11) -> 11,13,12
        f1(16,8) -> 8*
        f1(16,10) -> 8*
        f1(16,9) -> 8*
        f1(16,11) -> 8*
        b1() -> 16*
        f{#,0}(8,9) -> 11*
        f{#,0}(8,11) -> 11*
        f{#,0}(9,8) -> 11*
        f{#,0}(9,10) -> 11*
        f{#,0}(10,9) -> 11*
        f{#,0}(10,11) -> 11*
        f{#,0}(11,8) -> 11*
        f{#,0}(11,10) -> 11*
        f{#,0}(8,8) -> 11*
        f{#,0}(8,10) -> 11*
        f{#,0}(9,9) -> 11*
        f{#,0}(9,11) -> 11*
        f{#,0}(10,8) -> 11*
        f{#,0}(10,10) -> 11*
        f{#,0}(10,12) -> 13*
        f{#,0}(11,9) -> 11*
        f{#,0}(11,11) -> 11*
        a0() -> 8*
        f0(8,9) -> 9*
        f0(8,11) -> 9*
        f0(9,8) -> 9*
        f0(9,10) -> 9*
        f0(10,9) -> 9*
        f0(10,11) -> 9*
        f0(11,8) -> 9*
        f0(11,10) -> 9*
        f0(8,8) -> 9*
        f0(8,10) -> 9*
        f0(9,9) -> 9*
        f0(9,11) -> 9*
        f0(10,8) -> 9*
        f0(10,10) -> 9*
        f0(11,9) -> 9*
        f0(11,11) -> 9*
        b0() -> 10*
        8 -> 12*
        9 -> 12*
        10 -> 12*
        11 -> 12*
      problem:
       DPs:
        f#(b(),f(a(),x)) -> f#(b(),f(b(),x))
       TRS:
        f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
        f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1) = x1,
        
        [f](x0, x1) = x0,
        
        [b] = 0,
        
        [a] = 1
       orientation:
        f#(b(),f(a(),x)) = 1 >= 0 = f#(b(),f(b(),x))
        
        f(a(),f(b(),x)) = 1 >= 1 = f(a(),f(a(),f(a(),x)))
        
        f(b(),f(a(),x)) = 0 >= 0 = f(b(),f(b(),f(b(),x)))
       problem:
        DPs:
         
        TRS:
         f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
         f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
       Qed