YES
Time: 0.000682
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)}
  EDG:
   {(+#(-(x, y), z) -> +#(x, z), +#(-(x, y), z) -> +#(x, z))
    (+#(-(x, y), z) -> +#(x, z), +#(-(x, y), z) -> -#(+(x, z), y))}
   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)}
     SPSC:
      Simple Projection:
       pi(+#) = 0
      Strict:
       {}
      Qed