YES
Time: 0.001619
TRS:
 {  f +(x, 0()) -> f x,
  +(x, +(y, z)) -> +(+(x, y), z)}
 RUF:
  Strict:
   {+(x, +(y, z)) -> +(+(x, y), z)}
  Weak:
   {}
  DP:
   DP:
    {+#(x, +(y, z)) -> +#(x, y),
     +#(x, +(y, z)) -> +#(+(x, y), z)}
   TRS:
   {+(x, +(y, z)) -> +(+(x, y), z)}
   EDG:
    {(+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))}
    SCCS (1):
     Scc:
      {+#(x, +(y, z)) -> +#(x, y),
       +#(x, +(y, z)) -> +#(+(x, y), z)}
     SCC (2):
      Strict:
       {+#(x, +(y, z)) -> +#(x, y),
        +#(x, +(y, z)) -> +#(+(x, y), z)}
      Weak:
      {+(x, +(y, z)) -> +(+(x, y), z)}
      SPSC:
       Simple Projection:
        pi(+#) = 1
       Strict:
        {+#(x, +(y, z)) -> +#(+(x, y), z)}
       EDG:
        {(+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))}
        SCCS (1):
         Scc:
          {+#(x, +(y, z)) -> +#(+(x, y), z)}
         SCC (1):
          Strict:
           {+#(x, +(y, z)) -> +#(+(x, y), z)}
          Weak:
          {+(x, +(y, z)) -> +(+(x, y), z)}
          SPSC:
           Simple Projection:
            pi(+#) = 1
           Strict:
            {}
           Qed