MAYBE
Time: 0.047490
TRS:
 {:(z, +(x, f y)) -> :(g(z, y), +(x, a())),
    :(:(x, y), z) -> :(x, :(y, z)),
    :(+(x, y), z) -> +(:(x, z), :(y, z))}
 DP:
  DP:
   {:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())),
      :#(:(x, y), z) -> :#(x, :(y, z)),
      :#(:(x, y), z) -> :#(y, z),
      :#(+(x, y), z) -> :#(x, z),
      :#(+(x, y), z) -> :#(y, z)}
  TRS:
  {:(z, +(x, f y)) -> :(g(z, y), +(x, a())),
     :(:(x, y), z) -> :(x, :(y, z)),
     :(+(x, y), z) -> +(:(x, z), :(y, z))}
  UR:
   {:(z, +(x, f y)) -> :(g(z, y), +(x, a())),
      :(:(x, y), z) -> :(x, :(y, z)),
      :(+(x, y), z) -> +(:(x, z), :(y, z)),
            b(w, v) -> w,
            b(w, v) -> v}
   EDG:
    {(:#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(y, z))
     (:#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(x, z))
     (:#(+(x, y), z) -> :#(x, z), :#(:(x, y), z) -> :#(y, z))
     (:#(+(x, y), z) -> :#(x, z), :#(:(x, y), z) -> :#(x, :(y, z)))
     (:#(+(x, y), z) -> :#(x, z), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a())))
     (:#(+(x, y), z) -> :#(y, z), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a())))
     (:#(+(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), :#(+(x, y), z) -> :#(x, z))
     (:#(+(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(y, z))
     (:#(:(x, y), z) -> :#(y, z), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a())))
     (:#(:(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), :#(+(x, y), z) -> :#(x, z))
     (:#(:(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(y, z))
     (:#(:(x, y), z) -> :#(x, :(y, z)), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a())))
     (:#(:(x, y), z) -> :#(x, :(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) -> :#(x, z))
     (:#(:(x, y), z) -> :#(x, :(y, z)), :#(+(x, y), z) -> :#(y, z))}
    STATUS:
     arrows: 0.200000
     SCCS (1):
      Scc:
       {:#(:(x, y), z) -> :#(x, :(y, z)),
        :#(:(x, y), z) -> :#(y, z),
        :#(+(x, y), z) -> :#(x, z),
        :#(+(x, y), z) -> :#(y, z)}
      
      SCC (4):
       Strict:
        {:#(:(x, y), z) -> :#(x, :(y, z)),
         :#(:(x, y), z) -> :#(y, z),
         :#(+(x, y), z) -> :#(x, z),
         :#(+(x, y), z) -> :#(y, z)}
       Weak:
       {:(z, +(x, f y)) -> :(g(z, y), +(x, a())),
          :(:(x, y), z) -> :(x, :(y, z)),
          :(+(x, y), z) -> +(:(x, z), :(y, z))}
       Open