MAYBE
Time: 0.015942
TRS:
 {      f(x, 0(), 0()) -> s x,
      f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
      f(s x, s y, 0()) -> f(x, y, s 0()),
      f(s x, 0(), s z) -> f(x, s 0(), z),
        f(s 0(), y, z) -> f(0(), s y, s z),
        f(0(), y, 0()) -> s y,
  f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
  f(0(), s s y, s 0()) -> f(0(), y, s 0()),
  f(0(), s 0(), s s z) -> f(0(), s 0(), z),
  f(0(), s 0(), s 0()) -> s s 0(),
        f(0(), 0(), z) -> s z}
 DP:
  DP:
   {    f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)),
        f#(s x, s y, s z) -> f#(s x, s y, z),
        f#(s x, s y, 0()) -> f#(x, y, s 0()),
        f#(s x, 0(), s z) -> f#(x, s 0(), z),
          f#(s 0(), y, z) -> f#(0(), s y, s z),
    f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)),
    f#(0(), s s y, s s z) -> f#(0(), s s y, s z),
    f#(0(), s s y, s 0()) -> f#(0(), y, s 0()),
    f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)}
  TRS:
  {      f(x, 0(), 0()) -> s x,
       f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
       f(s x, s y, 0()) -> f(x, y, s 0()),
       f(s x, 0(), s z) -> f(x, s 0(), z),
         f(s 0(), y, z) -> f(0(), s y, s z),
         f(0(), y, 0()) -> s y,
   f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
   f(0(), s s y, s 0()) -> f(0(), y, s 0()),
   f(0(), s 0(), s s z) -> f(0(), s 0(), z),
   f(0(), s 0(), s 0()) -> s s 0(),
         f(0(), 0(), z) -> s z}
  UR:
   {      f(x, 0(), 0()) -> s x,
        f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
        f(s x, s y, 0()) -> f(x, y, s 0()),
        f(s x, 0(), s z) -> f(x, s 0(), z),
          f(s 0(), y, z) -> f(0(), s y, s z),
          f(0(), y, 0()) -> s y,
    f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
    f(0(), s s y, s 0()) -> f(0(), y, s 0()),
    f(0(), s 0(), s s z) -> f(0(), s 0(), z),
    f(0(), s 0(), s 0()) -> s s 0(),
          f(0(), 0(), z) -> s z,
                 a(w, v) -> w,
                 a(w, v) -> v}
   EDG:
    {(f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
     (f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s 0(), y, z) -> f#(0(), s y, s z))
     (f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, 0()) -> f#(x, y, s 0()))
     (f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, s z) -> f#(s x, s y, z))
     (f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)))
     (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
     (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s 0(), y, z) -> f#(0(), s y, s z))
     (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, 0(), s z) -> f#(x, s 0(), z))
     (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, s y, s z) -> f#(s x, s y, z))
     (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)))
     (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
     (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
     (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z))
     (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)))
     (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s 0(), y, z) -> f#(0(), s y, s z))
     (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, 0(), s z) -> f#(x, s 0(), z))
     (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(s x, s y, z))
     (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)))
     (f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
     (f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
     (f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z))
     (f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)))
     (f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)))
     (f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s s z) -> f#(0(), s s y, s z))
     (f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
     (f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)))
     (f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s s z) -> f#(0(), s s y, s z))
     (f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
     (f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
     (f#(0(), s s y, s 0()) -> f#(0(), y, s 0()), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
     (f#(0(), s 0(), s s z) -> f#(0(), s 0(), z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
     (f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)))
     (f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, s z) -> f#(s x, s y, z))
     (f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, 0()) -> f#(x, y, s 0()))
     (f#(s x, s y, s z) -> f#(s x, s y, z), f#(s 0(), y, z) -> f#(0(), s y, s z))}
    STATUS:
     arrows: 0.567901
     SCCS (4):
      Scc:
       {f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)),
        f#(s x, s y, s z) -> f#(s x, s y, z),
        f#(s x, s y, 0()) -> f#(x, y, s 0()),
        f#(s x, 0(), s z) -> f#(x, s 0(), z)}
      Scc:
       {f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)),
        f#(0(), s s y, s s z) -> f#(0(), s s y, s z)}
      Scc:
       {f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)}
      Scc:
       {f#(0(), s s y, s 0()) -> f#(0(), y, s 0())}
      
      SCC (4):
       Strict:
        {f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)),
         f#(s x, s y, s z) -> f#(s x, s y, z),
         f#(s x, s y, 0()) -> f#(x, y, s 0()),
         f#(s x, 0(), s z) -> f#(x, s 0(), z)}
       Weak:
       {      f(x, 0(), 0()) -> s x,
            f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
            f(s x, s y, 0()) -> f(x, y, s 0()),
            f(s x, 0(), s z) -> f(x, s 0(), z),
              f(s 0(), y, z) -> f(0(), s y, s z),
              f(0(), y, 0()) -> s y,
        f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
        f(0(), s s y, s 0()) -> f(0(), y, s 0()),
        f(0(), s 0(), s s z) -> f(0(), s 0(), z),
        f(0(), s 0(), s 0()) -> s s 0(),
              f(0(), 0(), z) -> s z}
       Open
      
      SCC (2):
       Strict:
        {f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)),
         f#(0(), s s y, s s z) -> f#(0(), s s y, s z)}
       Weak:
       {      f(x, 0(), 0()) -> s x,
            f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
            f(s x, s y, 0()) -> f(x, y, s 0()),
            f(s x, 0(), s z) -> f(x, s 0(), z),
              f(s 0(), y, z) -> f(0(), s y, s z),
              f(0(), y, 0()) -> s y,
        f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
        f(0(), s s y, s 0()) -> f(0(), y, s 0()),
        f(0(), s 0(), s s z) -> f(0(), s 0(), z),
        f(0(), s 0(), s 0()) -> s s 0(),
              f(0(), 0(), z) -> s z}
       Open
      SCC (1):
       Strict:
        {f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)}
       Weak:
       {      f(x, 0(), 0()) -> s x,
            f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
            f(s x, s y, 0()) -> f(x, y, s 0()),
            f(s x, 0(), s z) -> f(x, s 0(), z),
              f(s 0(), y, z) -> f(0(), s y, s z),
              f(0(), y, 0()) -> s y,
        f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
        f(0(), s s y, s 0()) -> f(0(), y, s 0()),
        f(0(), s 0(), s s z) -> f(0(), s 0(), z),
        f(0(), s 0(), s 0()) -> s s 0(),
              f(0(), 0(), z) -> s z}
       Open
      SCC (1):
       Strict:
        {f#(0(), s s y, s 0()) -> f#(0(), y, s 0())}
       Weak:
       {      f(x, 0(), 0()) -> s x,
            f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
            f(s x, s y, 0()) -> f(x, y, s 0()),
            f(s x, 0(), s z) -> f(x, s 0(), z),
              f(s 0(), y, z) -> f(0(), s y, s z),
              f(0(), y, 0()) -> s y,
        f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
        f(0(), s s y, s 0()) -> f(0(), y, s 0()),
        f(0(), s 0(), s s z) -> f(0(), s 0(), z),
        f(0(), s 0(), s 0()) -> s s 0(),
              f(0(), 0(), z) -> s z}
       Open