YES
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:
  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),
             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)}
  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)}
  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:
    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:
     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:
     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:
     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:
        Scc:
         {f#(0(), s(s(y)), s(s(z))) -> f#(0(), s(s(y)), s(z))}
        SCC:
         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:
     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#(x, y, f(s(x), s(y), 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)}
      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), 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#(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#(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), 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#(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))}
       SCCS:
        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), 0(), s(z)) -> f#(x, s(0()), z)}
        SCC:
         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), 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#(x, y, f(s(x), s(y), z)),
            f#(s(x), s(y), s(z)) -> f#(s(x), s(y), z)}
          EDG:
           {(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#(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))}
           SCCS:
            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)}
            SCC:
             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)}
             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#(s(x), s(y), s(z)) -> f#(s(x), s(y), z)}
              EDG:
               {(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:
                Scc:
                 {f#(s(x), s(y), s(z)) -> f#(s(x), s(y), z)}
                SCC:
                 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