MAYBE
Time: 0.005134
TRS:
 {    +(+(x, y), z) -> +(x, +(y, z)),
  +(f x, +(f y, z)) -> +(f +(x, y), z),
        +(f x, f y) -> f +(x, y)}
 DP:
  DP:
   {    +#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z),
    +#(f x, +(f y, z)) -> +#(x, y),
    +#(f x, +(f y, z)) -> +#(f +(x, y), z),
          +#(f x, f y) -> +#(x, y)}
  TRS:
  {    +(+(x, y), z) -> +(x, +(y, z)),
   +(f x, +(f y, z)) -> +(f +(x, y), z),
         +(f x, f y) -> f +(x, y)}
  EDG:
   {(+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y))
    (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(+(x, y), z) -> +#(y, z))
    (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, f y) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(+(x, y), z) -> +#(y, z), +#(f x, f y) -> +#(x, y))
    (+#(f x, f y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(f x, f y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(f x, f y) -> +#(x, y), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(f x, f y) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(f x, f y) -> +#(x, y), +#(f x, f y) -> +#(x, y))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, f y) -> +#(x, y))}
   STATUS:
    arrows: 0.000000
    SCCS (1):
     Scc:
      {    +#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z),
       +#(f x, +(f y, z)) -> +#(x, y),
       +#(f x, +(f y, z)) -> +#(f +(x, y), z),
             +#(f x, f y) -> +#(x, y)}
     
     SCC (5):
      Strict:
       {    +#(+(x, y), z) -> +#(x, +(y, z)),
            +#(+(x, y), z) -> +#(y, z),
        +#(f x, +(f y, z)) -> +#(x, y),
        +#(f x, +(f y, z)) -> +#(f +(x, y), z),
              +#(f x, f y) -> +#(x, y)}
      Weak:
      {    +(+(x, y), z) -> +(x, +(y, z)),
       +(f x, +(f y, z)) -> +(f +(x, y), z),
             +(f x, f y) -> f +(x, y)}
      Open