YES
Time: 0.006249
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}
  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))}
   SCCS (4):
    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:
     {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#(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 (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}
     SPSC:
      Simple Projection:
       pi(f#) = 2
      Strict:
       {}
      Qed
    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}
     SPSC:
      Simple Projection:
       pi(f#) = 1
      Strict:
       {}
      Qed
    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}
     SPSC:
      Simple Projection:
       pi(f#) = 1
      Strict:
       {f#(0(), s s y, s s z) -> f#(0(), s s y, s z)}
      EDG:
       {(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))}
       SCCS (1):
        Scc:
         {f#(0(), s s y, s s z) -> f#(0(), s s y, s z)}
        SCC (1):
         Strict:
          {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}
         SPSC:
          Simple Projection:
           pi(f#) = 2
          Strict:
           {}
          Qed
    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}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {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)}
      EDG:
       {(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, 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, 0(), s z) -> f#(x, s 0(), 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()))}
       SCCS (1):
        Scc:
         {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 (3):
         Strict:
          {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}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {f#(s x, s y, s z) -> f#(s x, s y, z),
            f#(s x, 0(), s z) -> f#(x, s 0(), z)}
          EDG:
           {(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, s y, s z) -> f#(s x, s y, z), f#(s x, s y, s z) -> f#(s x, s y, z))}
           SCCS (1):
            Scc:
             {f#(s x, s y, s z) -> f#(s x, s y, z)}
            SCC (1):
             Strict:
              {f#(s x, s y, s z) -> f#(s x, s y, 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}
             SPSC:
              Simple Projection:
               pi(f#) = 2
              Strict:
               {}
              Qed