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)))
    Usable Rule Processor:
     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)))
     Bounds Processor:
      bound: 1
      enrichment: match-dp
      automaton:
       final states: {14}
       transitions:
        f{#,1}(25,26) -> 12,13
        a1() -> 25*
        f1(25,9) -> 26*
        f1(25,11) -> 26*
        f1(25,10) -> 26*
        f1(25,12) -> 26*
        f1(25,26) -> 9*
        f{#,0}(9,10) -> 12*
        f{#,0}(9,12) -> 12*
        f{#,0}(10,9) -> 12*
        f{#,0}(10,11) -> 12*
        f{#,0}(11,10) -> 12*
        f{#,0}(11,12) -> 12*
        f{#,0}(12,9) -> 12*
        f{#,0}(12,11) -> 12*
        f{#,0}(9,9) -> 12*
        f{#,0}(9,11) -> 12*
        f{#,0}(10,10) -> 12*
        f{#,0}(10,12) -> 12*
        f{#,0}(11,9) -> 12*
        f{#,0}(11,11) -> 12*
        f{#,0}(11,15) -> 14*
        f{#,0}(12,10) -> 12*
        f{#,0}(12,12) -> 12*
        a0() -> 11*
        f0(9,10) -> 10*
        f0(9,12) -> 10*
        f0(10,9) -> 10*
        f0(10,11) -> 10*
        f0(11,10) -> 10*
        f0(11,12) -> 10*
        f0(12,9) -> 10*
        f0(12,11) -> 10*
        f0(9,9) -> 10*
        f0(9,11) -> 10*
        f0(10,10) -> 10*
        f0(10,12) -> 10*
        f0(11,9) -> 10*
        f0(11,11) -> 10*
        f0(11,13) -> 15*
        f0(12,10) -> 10*
        f0(12,12) -> 10*
        b0() -> 9*
        9 -> 13*
        10 -> 13*
        11 -> 13*
        12 -> 13*
      problem:
       DPs:
        f#(a(),f(b(),x)) -> f#(a(),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)))
      Restore Modifier:
       DPs:
        f#(a(),f(b(),x)) -> f#(a(),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)))
       Usable Rule Processor:
        DPs:
         f#(a(),f(b(),x)) -> f#(a(),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)))
        Bounds Processor:
         bound: 1
         enrichment: match-dp
         automaton:
          final states: {6}
          transitions:
           f{#,1}(15,17) -> 4,5
           a1() -> 15*
           f1(15,1) -> 16*
           f1(15,3) -> 16*
           f1(15,17) -> 16*
           f1(15,2) -> 16*
           f1(15,4) -> 16*
           f1(15,16) -> 17*
           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(),x)
          TRS:
           f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
         Restore Modifier:
          DPs:
           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)))
          Subterm Criterion Processor:
           simple projection:
            pi(f#) = 1
           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)))
    Usable Rule Processor:
     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(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
     Bounds Processor:
      bound: 1
      enrichment: match-dp
      automaton:
       final states: {14}
       transitions:
        f{#,1}(25,26) -> 12,13
        f1(25,9) -> 26*
        f1(25,11) -> 26*
        f1(25,10) -> 26*
        f1(25,12) -> 26*
        f1(25,26) -> 9*
        b1() -> 25*
        f{#,0}(9,10) -> 12*
        f{#,0}(9,12) -> 12*
        f{#,0}(10,9) -> 12*
        f{#,0}(10,11) -> 12*
        f{#,0}(11,10) -> 12*
        f{#,0}(11,12) -> 12*
        f{#,0}(12,9) -> 12*
        f{#,0}(12,11) -> 12*
        f{#,0}(9,9) -> 12*
        f{#,0}(9,11) -> 12*
        f{#,0}(10,10) -> 12*
        f{#,0}(10,12) -> 12*
        f{#,0}(11,9) -> 12*
        f{#,0}(11,11) -> 12*
        f{#,0}(11,15) -> 14*
        f{#,0}(12,10) -> 12*
        f{#,0}(12,12) -> 12*
        a0() -> 9*
        f0(9,10) -> 10*
        f0(9,12) -> 10*
        f0(10,9) -> 10*
        f0(10,11) -> 10*
        f0(11,10) -> 10*
        f0(11,12) -> 10*
        f0(12,9) -> 10*
        f0(12,11) -> 10*
        f0(9,9) -> 10*
        f0(9,11) -> 10*
        f0(10,10) -> 10*
        f0(10,12) -> 10*
        f0(11,9) -> 10*
        f0(11,11) -> 10*
        f0(11,13) -> 15*
        f0(12,10) -> 10*
        f0(12,12) -> 10*
        b0() -> 11*
        9 -> 13*
        10 -> 13*
        11 -> 13*
        12 -> 13*
      problem:
       DPs:
        f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x)))
        f#(b(),f(a(),x)) -> f#(b(),x)
       TRS:
        f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
      Restore Modifier:
       DPs:
        f#(b(),f(a(),x)) -> f#(b(),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)))
       Usable Rule Processor:
        DPs:
         f#(b(),f(a(),x)) -> f#(b(),f(b(),f(b(),x)))
         f#(b(),f(a(),x)) -> f#(b(),x)
        TRS:
         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}(15,17) -> 4,5
           f1(15,1) -> 16*
           f1(15,3) -> 16*
           f1(15,17) -> 16*
           f1(15,2) -> 16*
           f1(15,4) -> 16*
           f1(15,16) -> 17*
           b1() -> 15*
           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(),x)
          TRS:
           f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
         Restore Modifier:
          DPs:
           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)))
          Subterm Criterion Processor:
           simple projection:
            pi(f#) = 1
           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