MAYBE
Time: 0.005754
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), +#(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))}
    STATUS:
     arrows: 0.861111
     SCCS (1):
      Scc:
       {+#(x, +(y, z)) -> +#(x, y)}
      
      
      SCC (1):
       Strict:
        {+#(x, +(y, z)) -> +#(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()}
       Open