YES
Time: 0.015797
TRS:
 {    +(+(x, y), z) -> +(x, +(y, z)),
  +(f x, +(f y, z)) -> +(f +(x, y), z),
        +(f x, f y) -> f +(x, y)}
 DP:
  DP:
   {    +#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z),
    +#(f x, +(f y, z)) -> +#(x, y),
    +#(f x, +(f y, z)) -> +#(f +(x, y), z),
          +#(f x, f y) -> +#(x, y)}
  TRS:
  {    +(+(x, y), z) -> +(x, +(y, z)),
   +(f x, +(f y, z)) -> +(f +(x, y), z),
         +(f x, f y) -> f +(x, y)}
  EDG:
   {(+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y))
    (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, f y) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(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) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(+(x, y), z) -> +#(y, z), +#(f x, f y) -> +#(x, y))
    (+#(f x, f y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(f x, f y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(f x, f y) -> +#(x, y), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(f x, f y) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(f x, f y) -> +#(x, y), +#(f x, f y) -> +#(x, y))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(x, y))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
    (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, f y) -> +#(x, y))}
   SCCS (1):
    Scc:
     {    +#(+(x, y), z) -> +#(x, +(y, z)),
          +#(+(x, y), z) -> +#(y, z),
      +#(f x, +(f y, z)) -> +#(x, y),
      +#(f x, +(f y, z)) -> +#(f +(x, y), z),
            +#(f x, f y) -> +#(x, y)}
    SCC (5):
     Strict:
      {    +#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z),
       +#(f x, +(f y, z)) -> +#(x, y),
       +#(f x, +(f y, z)) -> +#(f +(x, y), z),
             +#(f x, f y) -> +#(x, y)}
     Weak:
     {    +(+(x, y), z) -> +(x, +(y, z)),
      +(f x, +(f y, z)) -> +(f +(x, y), z),
            +(f x, f y) -> f +(x, y)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [+](x0, x1) = x0 + x1 + 1,
       
       [f](x0) = x0,
       
       [+#](x0, x1) = x0 + x1
      Strict:
       +#(f x, f y) -> +#(x, y)
       0 + 1x + 1y >= 0 + 1x + 1y
       +#(f x, +(f y, z)) -> +#(f +(x, y), z)
       1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z
       +#(f x, +(f y, z)) -> +#(x, y)
       1 + 1x + 1y + 1z >= 0 + 1x + 1y
       +#(+(x, y), z) -> +#(y, z)
       1 + 1x + 1y + 1z >= 0 + 1y + 1z
       +#(+(x, y), z) -> +#(x, +(y, z))
       1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z
      Weak:
       
     EDG:
      {(+#(f x, f y) -> +#(x, y), +#(f x, f y) -> +#(x, y))
       (+#(f x, f y) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
       (+#(f x, f y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
       (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
       (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
       (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, f y) -> +#(x, y))
       (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
       (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y))}
      SCCS (1):
       Scc:
        {    +#(+(x, y), z) -> +#(x, +(y, z)),
         +#(f x, +(f y, z)) -> +#(f +(x, y), z),
               +#(f x, f y) -> +#(x, y)}
       SCC (3):
        Strict:
         {    +#(+(x, y), z) -> +#(x, +(y, z)),
          +#(f x, +(f y, z)) -> +#(f +(x, y), z),
                +#(f x, f y) -> +#(x, y)}
        Weak:
        {    +(+(x, y), z) -> +(x, +(y, z)),
         +(f x, +(f y, z)) -> +(f +(x, y), z),
               +(f x, f y) -> f +(x, y)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [+](x0, x1) = x0,
          
          [f](x0) = x0 + 1,
          
          [+#](x0, x1) = x0
         Strict:
          +#(f x, f y) -> +#(x, y)
          1 + 0x + 1y >= 0 + 0x + 1y
          +#(f x, +(f y, z)) -> +#(f +(x, y), z)
          0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z
          +#(+(x, y), z) -> +#(x, +(y, z))
          0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z
         Weak:
          
        EDG:
         {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z))
          (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
          (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, +(f y, z)) -> +#(f +(x, y), z))}
         SCCS (2):
          Scc:
           {+#(f x, +(f y, z)) -> +#(f +(x, y), z)}
          Scc:
           {+#(+(x, y), z) -> +#(x, +(y, z))}
          SCC (1):
           Strict:
            {+#(f x, +(f y, z)) -> +#(f +(x, y), z)}
           Weak:
           {    +(+(x, y), z) -> +(x, +(y, z)),
            +(f x, +(f y, z)) -> +(f +(x, y), z),
                  +(f x, f y) -> f +(x, y)}
           SPSC:
            Simple Projection:
             pi(+#) = 1
            Strict:
             {}
            Qed
          SCC (1):
           Strict:
            {+#(+(x, y), z) -> +#(x, +(y, z))}
           Weak:
           {    +(+(x, y), z) -> +(x, +(y, z)),
            +(f x, +(f y, z)) -> +(f +(x, y), z),
                  +(f x, f y) -> f +(x, y)}
           SPSC:
            Simple Projection:
             pi(+#) = 0
            Strict:
             {}
            Qed