MAYBE
Time: 0.658287
TRS:
 {    +(+(x, y), z) -> +(x, +(y, z)),
  +(a(), +(b(), z)) -> +(b(), +(a(), z)),
        +(a(), b()) -> +(b(), a()),
      f(+(x, y), z) -> +(f(x, z), f(y, z)),
          f(b(), y) -> b(),
          f(a(), y) -> a()}
 DP:
  DP:
   {    +#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z),
    +#(a(), +(b(), z)) -> +#(b(), +(a(), z)),
    +#(a(), +(b(), z)) -> +#(a(), z),
          +#(a(), b()) -> +#(b(), a()),
        f#(+(x, y), z) -> +#(f(x, z), f(y, z)),
        f#(+(x, y), z) -> f#(x, z),
        f#(+(x, y), z) -> f#(y, z)}
  TRS:
  {    +(+(x, y), z) -> +(x, +(y, z)),
   +(a(), +(b(), z)) -> +(b(), +(a(), z)),
         +(a(), b()) -> +(b(), a()),
       f(+(x, y), z) -> +(f(x, z), f(y, z)),
           f(b(), y) -> b(),
           f(a(), y) -> a()}
  UR:
   {    +(+(x, y), z) -> +(x, +(y, z)),
    +(a(), +(b(), z)) -> +(b(), +(a(), z)),
          +(a(), b()) -> +(b(), a()),
        f(+(x, y), z) -> +(f(x, z), f(y, z)),
            f(b(), y) -> b(),
            f(a(), y) -> a(),
              c(w, v) -> w,
              c(w, v) -> v}
   EDG:
    {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(a(), +(b(), z)) -> +#(a(), z))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(a(), +(b(), z)) -> +#(b(), +(a(), z)))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
     (f#(+(x, y), z) -> +#(f(x, z), f(y, z)), +#(a(), b()) -> +#(b(), a()))
     (f#(+(x, y), z) -> +#(f(x, z), f(y, z)), +#(a(), +(b(), z)) -> +#(a(), z))
     (f#(+(x, y), z) -> +#(f(x, z), f(y, z)), +#(a(), +(b(), z)) -> +#(b(), +(a(), z)))
     (f#(+(x, y), z) -> +#(f(x, z), f(y, z)), +#(+(x, y), z) -> +#(y, z))
     (f#(+(x, y), z) -> +#(f(x, z), f(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(y, z), +#(a(), b()) -> +#(b(), a()))
     (+#(+(x, y), z) -> +#(y, z), +#(a(), +(b(), z)) -> +#(a(), z))
     (+#(+(x, y), z) -> +#(y, z), +#(a(), +(b(), z)) -> +#(b(), +(a(), z)))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
     (f#(+(x, y), z) -> f#(y, z), f#(+(x, y), z) -> f#(y, z))
     (f#(+(x, y), z) -> f#(y, z), f#(+(x, y), z) -> f#(x, z))
     (f#(+(x, y), z) -> f#(y, z), f#(+(x, y), z) -> +#(f(x, z), f(y, z)))
     (f#(+(x, y), z) -> f#(x, z), f#(+(x, y), z) -> +#(f(x, z), f(y, z)))
     (f#(+(x, y), z) -> f#(x, z), f#(+(x, y), z) -> f#(x, z))
     (f#(+(x, y), z) -> f#(x, z), f#(+(x, y), z) -> f#(y, z))
     (+#(a(), +(b(), z)) -> +#(a(), z), +#(a(), +(b(), z)) -> +#(b(), +(a(), z)))
     (+#(a(), +(b(), z)) -> +#(a(), z), +#(a(), +(b(), z)) -> +#(a(), z))
     (+#(a(), +(b(), z)) -> +#(a(), z), +#(a(), b()) -> +#(b(), a()))}
    STATUS:
     arrows: 0.640625
     SCCS (3):
      Scc:
       {f#(+(x, y), z) -> f#(x, z),
        f#(+(x, y), z) -> f#(y, z)}
      Scc:
       {+#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z)}
      Scc:
       {+#(a(), +(b(), z)) -> +#(a(), z)}
      
      SCC (2):
       Strict:
        {f#(+(x, y), z) -> f#(x, z),
         f#(+(x, y), z) -> f#(y, z)}
       Weak:
       {    +(+(x, y), z) -> +(x, +(y, z)),
        +(a(), +(b(), z)) -> +(b(), +(a(), z)),
              +(a(), b()) -> +(b(), a()),
            f(+(x, y), z) -> +(f(x, z), f(y, z)),
                f(b(), y) -> b(),
                f(a(), y) -> a()}
       Open
      
      SCC (2):
       Strict:
        {+#(+(x, y), z) -> +#(x, +(y, z)),
         +#(+(x, y), z) -> +#(y, z)}
       Weak:
       {    +(+(x, y), z) -> +(x, +(y, z)),
        +(a(), +(b(), z)) -> +(b(), +(a(), z)),
              +(a(), b()) -> +(b(), a()),
            f(+(x, y), z) -> +(f(x, z), f(y, z)),
                f(b(), y) -> b(),
                f(a(), y) -> a()}
       Open
      SCC (1):
       Strict:
        {+#(a(), +(b(), z)) -> +#(a(), z)}
       Weak:
       {    +(+(x, y), z) -> +(x, +(y, z)),
        +(a(), +(b(), z)) -> +(b(), +(a(), z)),
              +(a(), b()) -> +(b(), a()),
            f(+(x, y), z) -> +(f(x, z), f(y, z)),
                f(b(), y) -> b(),
                f(a(), y) -> a()}
       Open