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