YES
Time: 0.012686
TRS:
 {-(-(neg x, neg x), -(neg y, neg y)) -> -(-(x, y), -(x, y))}
 DP:
  DP:
   {-#(-(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))}
  UR:
   {-(-(neg x, neg x), -(neg y, neg y)) -> -(-(x, y), -(x, y))}
   EDG:
    {(-#(-(neg x, neg x), -(neg y, neg y)) -> -#(x, y), -#(-(neg x, neg x), -(neg y, neg y)) -> -#(-(x, y), -(x, y)))
     (-#(-(neg x, neg x), -(neg y, neg y)) -> -#(x, y), -#(-(neg x, neg x), -(neg y, neg y)) -> -#(x, y))
     (-#(-(neg x, neg x), -(neg y, neg y)) -> -#(-(x, y), -(x, y)), -#(-(neg x, neg x), -(neg y, neg y)) -> -#(x, y))
     (-#(-(neg x, neg x), -(neg y, neg y)) -> -#(-(x, y), -(x, y)), -#(-(neg x, neg x), -(neg y, neg y)) -> -#(-(x, y), -(x, y)))}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {-#(-(neg x, neg x), -(neg y, neg y)) -> -#(x, y),
        -#(-(neg x, neg x), -(neg y, neg y)) -> -#(-(x, y), -(x, y))}
      
      SCC (2):
       Strict:
        {-#(-(neg x, neg x), -(neg y, neg y)) -> -#(x, y),
         -#(-(neg x, neg x), -(neg y, neg y)) -> -#(-(x, y), -(x, y))}
       Weak:
       {-(-(neg x, neg x), -(neg y, neg y)) -> -(-(x, y), -(x, y))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [-](x0, x1) = x0 + 1,
         
         [neg](x0) = x0 + 1,
         
         [-#](x0, x1) = x0
        Strict:
         -#(-(neg x, neg x), -(neg y, neg y)) -> -#(-(x, y), -(x, y))
         2 + 1x + 0y >= 1 + 1x + 0y
         -#(-(neg x, neg x), -(neg y, neg y)) -> -#(x, y)
         2 + 1x + 0y >= 0 + 1x + 0y
        Weak:
         -(-(neg x, neg x), -(neg y, neg y)) -> -(-(x, y), -(x, y))
         3 + 1x + 0y >= 2 + 1x + 0y
       Qed