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