YES
Time: 0.002147
TRS:
 {-(+(x, y), y) -> x,
  +(-(x, y), z) -> -(+(x, z), y)}
 DP:
  DP:
   {+#(-(x, y), z) -> -#(+(x, z), y),
    +#(-(x, y), z) -> +#(x, z)}
  TRS:
  {-(+(x, y), y) -> x,
   +(-(x, y), z) -> -(+(x, z), y)}
  UR:
   {-(+(x, y), y) -> x,
    +(-(x, y), z) -> -(+(x, z), y)}
   EDG:
    {(+#(-(x, y), z) -> +#(x, z), +#(-(x, y), z) -> +#(x, z))
     (+#(-(x, y), z) -> +#(x, z), +#(-(x, y), z) -> -#(+(x, z), y))}
    STATUS:
     arrows: 0.500000
     SCCS (1):
      Scc:
       {+#(-(x, y), z) -> +#(x, z)}
      
      SCC (1):
       Strict:
        {+#(-(x, y), z) -> +#(x, z)}
       Weak:
       {-(+(x, y), y) -> x,
        +(-(x, y), z) -> -(+(x, z), y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [-](x0, x1) = x0 + 1,
         
         [+](x0, x1) = x0 + 1,
         
         [+#](x0, x1) = x0
        Strict:
         +#(-(x, y), z) -> +#(x, z)
         1 + 1x + 0z + 0y >= 0 + 1x + 0z
        Weak:
         +(-(x, y), z) -> -(+(x, z), y)
         2 + 1x + 0z + 0y >= 2 + 1x + 0z + 0y
         -(+(x, y), y) -> x
         2 + 1x + 0y >= 1x
       Qed