YES

Problem:
 -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y))

Proof:
 DP Processor:
  DPs:
   -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(x,y)
   -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(-(x,y),-(x,y))
  TRS:
   -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y))
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [-#](x0, x1) = 1x1,
    
    [-](x0, x1) = 3x1 + 3,
    
    [neg](x0) = x0 + 1
   orientation:
    -#(-(neg(x),neg(x)),-(neg(y),neg(y))) = 4y + 5 >= 1y = -#(x,y)
    
    -#(-(neg(x),neg(x)),-(neg(y),neg(y))) = 4y + 5 >= 4y + 4 = -#(-(x,y),-(x,y))
    
    -(-(neg(x),neg(x)),-(neg(y),neg(y))) = 6y + 7 >= 6y + 6 = -(-(x,y),-(x,y))
   problem:
    DPs:
     -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(-(x,y),-(x,y))
    TRS:
     -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y))
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [-#](x0, x1) = x0 + 0,
     
     [-](x0, x1) = x0 + 0,
     
     [neg](x0) = 1x0 + 2
    orientation:
     -#(-(neg(x),neg(x)),-(neg(y),neg(y))) = 1x + 2 >= x + 0 = -#(-(x,y),-(x,y))
     
     -(-(neg(x),neg(x)),-(neg(y),neg(y))) = 1x + 2 >= x + 0 = -(-(x,y),-(x,y))
    problem:
     DPs:
      
     TRS:
      -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y))
    Qed