YES

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

Proof:
 DP Processor:
  DPs:
   f#(f(x,a()),y) -> f#(x,y)
   f#(f(x,a()),y) -> f#(y,f(x,y))
  TRS:
   f(f(x,a()),y) -> f(y,f(x,y))
  Bounds Processor:
   bound: 2
   enrichment: top-dp
   automaton:
    final states: {20}
    transitions:
     a0() -> 18*
     f{#,1}(18,21) -> 20*
     f{#,1}(18,23) -> 16*
     f{#,1}(20,21) -> 20*
     f{#,1}(16,24) -> 16*
     f{#,1}(19,21) -> 20*
     f{#,1}(20,22) -> 16*
     f{#,1}(16,21) -> 20*
     f1(18,19) -> 21*
     f1(18,23) -> 23*
     f1(19,16) -> 24*
     f1(19,18) -> 23*
     f1(19,20) -> 22*
     f1(20,19) -> 21*
     f1(16,16) -> 24*
     f1(16,18) -> 23*
     f1(16,20) -> 22*
     f1(16,24) -> 24*
     f1(18,16) -> 24*
     f1(18,18) -> 23*
     f1(18,20) -> 22*
     f1(19,19) -> 21*
     f1(19,21) -> 21*
     f1(20,16) -> 24*
     f1(20,18) -> 23*
     f1(20,20) -> 22*
     f1(20,22) -> 22*
     f1(16,19) -> 21*
     f1(21,21) -> 21*
     f1(21,25) -> 21*
     f{#,2}(21,25) -> 20*
     f2(18,21) -> 25*
     f2(20,21) -> 25*
     f2(19,21) -> 25*
     f2(16,21) -> 25*
     f2(21,25) -> 25*
     f{#,0}(18,19) -> 20*
     f{#,0}(19,16) -> 16*
     f{#,0}(19,18) -> 16*
     f{#,0}(19,20) -> 16*
     f{#,0}(20,19) -> 20*
     f{#,0}(16,16) -> 16*
     f{#,0}(16,18) -> 16*
     f{#,0}(16,20) -> 16*
     f{#,0}(18,16) -> 16*
     f{#,0}(18,18) -> 16*
     f{#,0}(18,20) -> 16*
     f{#,0}(19,19) -> 20*
     f{#,0}(20,16) -> 16*
     f{#,0}(20,18) -> 16*
     f{#,0}(20,20) -> 16*
     f{#,0}(16,19) -> 20*
     f0(18,19) -> 19*
     f0(19,16) -> 19*
     f0(19,18) -> 19*
     f0(19,20) -> 19*
     f0(20,19) -> 19*
     f0(16,16) -> 19*
     f0(16,18) -> 19*
     f0(16,20) -> 19*
     f0(18,16) -> 19*
     f0(18,18) -> 19*
     f0(18,20) -> 19*
     f0(19,19) -> 19*
     f0(20,16) -> 19*
     f0(20,18) -> 19*
     f0(20,20) -> 19*
     f0(16,19) -> 19*
   problem:
    DPs:
     f#(f(x,a()),y) -> f#(x,y)
    TRS:
     f(f(x,a()),y) -> f(y,f(x,y))
   Subterm Criterion Processor:
    simple projection:
     pi(f#) = 0
    problem:
     DPs:
      
     TRS:
      f(f(x,a()),y) -> f(y,f(x,y))
    Qed