YES

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

Proof:
 DP Processor:
  DPs:
   f#(y,f(y,x)) -> f#(a(),y)
   f#(y,f(y,x)) -> f#(f(a(),y),f(a(),y))
  TRS:
   f(y,f(y,x)) -> f(f(a(),y),f(a(),y))
  Bounds Processor:
   bound: 3
   enrichment: match
   automaton:
    final states: {3}
    transitions:
     f{#,0}(27,26) -> 3*
     f{#,0}(20,19) -> 3*
     f{#,0}(21,2) -> 3*
     f{#,0}(1,2) -> 3*
     f{#,0}(21,26) -> 3*
     f{#,0}(1,26) -> 3*
     f{#,0}(27,19) -> 3*
     f{#,0}(20,2) -> 3*
     f{#,0}(20,26) -> 3*
     f{#,0}(21,19) -> 3*
     f{#,0}(27,2) -> 3*
     f{#,0}(1,19) -> 3*
     f0(27,26) -> 1*
     f0(20,19) -> 1*
     f0(21,2) -> 1*
     f0(1,2) -> 1*
     f0(21,26) -> 1*
     f0(1,26) -> 1*
     f0(27,19) -> 1*
     f0(20,2) -> 1*
     f0(20,26) -> 1*
     f0(21,19) -> 1*
     f0(27,2) -> 1*
     f0(1,19) -> 1*
     f1(27,20) -> 1*
     f1(2,20) -> 1*
     f1(2,26) -> 1*
     f1(19,2) -> 1*
     f1(19,20) -> 1*
     f1(20,1) -> 1*
     f1(19,26) -> 1*
     f1(26,2) -> 1*
     f1(20,21) -> 1*
     f1(20,27) -> 1*
     f1(26,20) -> 1*
     f1(27,1) -> 1*
     f1(21,20) -> 1*
     f1(1,20) -> 1*
     f1(2,1) -> 1*
     f1(26,26) -> 1*
     f1(27,21) -> 1*
     f1(2,19) -> 1*
     f1(2,21) -> 1*
     f1(27,27) -> 1*
     f1(2,27) -> 1*
     f1(19,1) -> 1*
     f1(19,19) -> 1*
     f1(19,21) -> 1*
     f1(19,27) -> 1*
     f1(26,1) -> 1*
     f1(20,20) -> 1*
     f1(21,1) -> 1*
     f1(1,1) -> 1*
     f1(26,19) -> 1*
     f1(26,21) -> 1*
     f1(21,21) -> 1*
     f1(1,21) -> 1*
     f1(2,2) -> 1*
     f1(26,27) -> 1*
     f1(21,27) -> 1*
     f1(1,27) -> 1*
     f{#,1}(27,20) -> 3*
     f{#,1}(2,20) -> 3*
     f{#,1}(2,26) -> 3*
     f{#,1}(19,2) -> 3*
     f{#,1}(19,20) -> 3*
     f{#,1}(20,1) -> 3*
     f{#,1}(19,26) -> 3*
     f{#,1}(26,2) -> 3*
     f{#,1}(20,21) -> 3*
     f{#,1}(20,27) -> 3*
     f{#,1}(26,20) -> 3*
     f{#,1}(27,1) -> 3*
     f{#,1}(21,20) -> 3*
     f{#,1}(1,20) -> 3*
     f{#,1}(2,1) -> 3*
     f{#,1}(26,26) -> 3*
     f{#,1}(27,21) -> 3*
     f{#,1}(2,19) -> 3*
     f{#,1}(2,21) -> 3*
     f{#,1}(27,27) -> 3*
     f{#,1}(2,27) -> 3*
     f{#,1}(19,1) -> 3*
     f{#,1}(19,19) -> 3*
     f{#,1}(19,21) -> 3*
     f{#,1}(19,27) -> 3*
     f{#,1}(26,1) -> 3*
     f{#,1}(20,20) -> 3*
     f{#,1}(21,1) -> 3*
     f{#,1}(1,1) -> 3*
     f{#,1}(26,19) -> 3*
     f{#,1}(26,21) -> 3*
     f{#,1}(21,21) -> 3*
     f{#,1}(1,21) -> 3*
     f{#,1}(2,2) -> 3*
     f{#,1}(26,27) -> 3*
     f{#,1}(21,27) -> 3*
     f{#,1}(1,27) -> 3*
     f2(27,20) -> 1*
     f2(17,20) -> 1*
     f2(18,13) -> 1*
     f2(13,13) -> 1*
     f2(18,21) -> 1*
     f2(19,2) -> 17,20*,1
     f2(13,21) -> 1*
     f2(9,2) -> 17*,16,15
     f2(19,20) -> 1,21*
     f2(9,20) -> 18*
     f2(19,26) -> 1,20*
     f2(9,26) -> 17*
     f2(20,15) -> 1*
     f2(15,15) -> 1*
     f2(20,17) -> 1*
     f2(15,17) -> 1*
     f2(26,2) -> 1,20*
     f2(20,27) -> 1*
     f2(15,27) -> 1*
     f2(21,18) -> 1*
     f2(26,20) -> 1,21*
     f2(26,26) -> 20*
     f2(27,15) -> 1*
     f2(27,17) -> 1*
     f2(17,15) -> 1*
     f2(17,17) -> 1*
     f2(27,27) -> 1*
     f2(17,27) -> 1*
     f2(18,18) -> 1*
     f2(13,18) -> 1*
     f2(19,1) -> 18,21*,1
     f2(9,1) -> 18*,14,13
     f2(19,19) -> 17,20*,1
     f2(19,21) -> 1,21*
     f2(9,19) -> 17*
     f2(9,21) -> 18*
     f2(19,27) -> 1,21*
     f2(9,27) -> 18*
     f2(26,1) -> 1,21*
     f2(20,20) -> 1*
     f2(15,20) -> 1*
     f2(21,13) -> 1*
     f2(26,19) -> 20*
     f2(26,21) -> 1,21*
     f2(21,21) -> 1*
     f2(26,27) -> 1,21*
     f{#,2}(27,20) -> 3*
     f{#,2}(17,20) -> 3*
     f{#,2}(18,13) -> 3*
     f{#,2}(18,21) -> 3*
     f{#,2}(19,2) -> 3*
     f{#,2}(9,2) -> 3*
     f{#,2}(14,18) -> 3*
     f{#,2}(19,20) -> 3*
     f{#,2}(9,20) -> 3*
     f{#,2}(19,26) -> 3*
     f{#,2}(9,26) -> 3*
     f{#,2}(20,15) -> 3*
     f{#,2}(20,17) -> 3*
     f{#,2}(26,2) -> 3*
     f{#,2}(20,27) -> 3*
     f{#,2}(21,18) -> 3*
     f{#,2}(26,20) -> 3*
     f{#,2}(16,20) -> 3*
     f{#,2}(26,26) -> 3*
     f{#,2}(27,15) -> 3*
     f{#,2}(27,17) -> 3*
     f{#,2}(17,15) -> 3*
     f{#,2}(17,17) -> 3*
     f{#,2}(27,27) -> 3*
     f{#,2}(17,27) -> 3*
     f{#,2}(18,18) -> 3*
     f{#,2}(19,1) -> 3*
     f{#,2}(9,1) -> 3*
     f{#,2}(14,13) -> 3*
     f{#,2}(19,19) -> 3*
     f{#,2}(19,21) -> 3*
     f{#,2}(9,19) -> 3*
     f{#,2}(14,21) -> 3*
     f{#,2}(9,21) -> 3*
     f{#,2}(19,27) -> 3*
     f{#,2}(9,27) -> 3*
     f{#,2}(26,1) -> 3*
     f{#,2}(20,20) -> 3*
     f{#,2}(21,13) -> 3*
     f{#,2}(16,15) -> 3*
     f{#,2}(26,19) -> 3*
     f{#,2}(16,17) -> 3*
     f{#,2}(26,21) -> 3*
     f{#,2}(21,21) -> 3*
     f{#,2}(26,27) -> 3*
     f{#,2}(16,27) -> 3*
     f3(22,26) -> 25*
     f3(23,23) -> 21*
     f3(23,25) -> 21*
     f3(23,27) -> 21*
     f3(25,23) -> 21*
     f3(25,25) -> 21*
     f3(25,27) -> 21*
     f3(26,26) -> 25,20,27*,1
     f3(22,19) -> 25*,24,23
     f3(27,23) -> 21*
     f3(27,25) -> 21*
     f3(27,27) -> 1,21*
     f3(26,19) -> 25,20,27*,1
     a3() -> 19,26*,9,2,22
     f{#,3}(22,26) -> 3*
     f{#,3}(25,23) -> 3*
     f{#,3}(25,25) -> 3*
     f{#,3}(25,27) -> 3*
     f{#,3}(26,26) -> 3*
     f{#,3}(22,19) -> 3*
     f{#,3}(27,23) -> 3*
     f{#,3}(27,25) -> 3*
     f{#,3}(27,27) -> 3*
     f{#,3}(24,23) -> 3*
     f{#,3}(24,25) -> 3*
     f{#,3}(24,27) -> 3*
     f{#,3}(26,19) -> 3*
   problem:
    DPs:
     
    TRS:
     f(y,f(y,x)) -> f(f(a(),y),f(a(),y))
   Qed