YES

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

Proof:
 DP Processor:
  DPs:
   f#(g(x),y,y) -> f#(x,x,y)
  TRS:
   f(g(x),y,y) -> g(f(x,x,y))
  Usable Rule Processor:
   DPs:
    f#(g(x),y,y) -> f#(x,x,y)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [f#](x0, x1, x2) = 1x0 + 5x1 + x2,
     
     [g](x0) = 5x0 + -2
    orientation:
     f#(g(x),y,y) = 6x + 5y + -1 >= 5x + y = f#(x,x,y)
    problem:
     DPs:
      
     TRS:
      
    Qed