MAYBE
Time: 0.003751
TRS:
 {          i 0() -> 0(),
            i i x -> x,
        i +(x, y) -> +(i x, i y),
        +(x, 0()) -> x,
        +(x, i x) -> 0(),
    +(x, +(y, z)) -> +(+(x, y), z),
        +(0(), y) -> y,
        +(i x, x) -> 0(),
  +(+(x, y), i y) -> x,
  +(+(x, i y), y) -> x}
 DP:
  DP:
   {    i# +(x, y) -> i# y,
        i# +(x, y) -> i# x,
        i# +(x, y) -> +#(i x, i y),
    +#(x, +(y, z)) -> +#(x, y),
    +#(x, +(y, z)) -> +#(+(x, y), z)}
  TRS:
  {          i 0() -> 0(),
             i i x -> x,
         i +(x, y) -> +(i x, i y),
         +(x, 0()) -> x,
         +(x, i x) -> 0(),
     +(x, +(y, z)) -> +(+(x, y), z),
         +(0(), y) -> y,
         +(i x, x) -> 0(),
   +(+(x, y), i y) -> x,
   +(+(x, i y), y) -> x}
  EDG:
   {(+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y))
    (i# +(x, y) -> +#(i x, i y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (i# +(x, y) -> +#(i x, i y), +#(x, +(y, z)) -> +#(x, y))
    (i# +(x, y) -> i# y, i# +(x, y) -> i# y)
    (i# +(x, y) -> i# y, i# +(x, y) -> i# x)
    (i# +(x, y) -> i# y, i# +(x, y) -> +#(i x, i y))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (i# +(x, y) -> i# x, i# +(x, y) -> i# y)
    (i# +(x, y) -> i# x, i# +(x, y) -> i# x)
    (i# +(x, y) -> i# x, i# +(x, y) -> +#(i x, i y))}
   STATUS:
    arrows: 0.520000
    SCCS (2):
     Scc:
      {i# +(x, y) -> i# y,
       i# +(x, y) -> i# x}
     Scc:
      {+#(x, +(y, z)) -> +#(x, y),
       +#(x, +(y, z)) -> +#(+(x, y), z)}
     
     SCC (2):
      Strict:
       {i# +(x, y) -> i# y,
        i# +(x, y) -> i# x}
      Weak:
      {          i 0() -> 0(),
                 i i x -> x,
             i +(x, y) -> +(i x, i y),
             +(x, 0()) -> x,
             +(x, i x) -> 0(),
         +(x, +(y, z)) -> +(+(x, y), z),
             +(0(), y) -> y,
             +(i x, x) -> 0(),
       +(+(x, y), i y) -> x,
       +(+(x, i y), y) -> x}
      Open
     
     SCC (2):
      Strict:
       {+#(x, +(y, z)) -> +#(x, y),
        +#(x, +(y, z)) -> +#(+(x, y), z)}
      Weak:
      {          i 0() -> 0(),
                 i i x -> x,
             i +(x, y) -> +(i x, i y),
             +(x, 0()) -> x,
             +(x, i x) -> 0(),
         +(x, +(y, z)) -> +(+(x, y), z),
             +(0(), y) -> y,
             +(i x, x) -> 0(),
       +(+(x, y), i y) -> x,
       +(+(x, i y), y) -> x}
      Open