YES
Time: 0.029116
TRS:
 {      f(x, 0()) -> x,
    f(f(x, y), z) -> f(x, f(y, z)),
        f(0(), y) -> y,
        f(i x, y) -> i x,
    f(g(x, y), z) -> g(f(x, z), f(y, z)),
  f(1(), g(x, y)) -> x,
  f(2(), g(x, y)) -> y}
 DP:
  DP:
   {f#(f(x, y), z) -> f#(y, z),
    f#(f(x, y), z) -> f#(x, f(y, z)),
    f#(g(x, y), z) -> f#(y, z),
    f#(g(x, y), z) -> f#(x, z)}
  TRS:
  {      f(x, 0()) -> x,
     f(f(x, y), z) -> f(x, f(y, z)),
         f(0(), y) -> y,
         f(i x, y) -> i x,
     f(g(x, y), z) -> g(f(x, z), f(y, z)),
   f(1(), g(x, y)) -> x,
   f(2(), g(x, y)) -> y}
  UR:
   {      f(x, 0()) -> x,
      f(f(x, y), z) -> f(x, f(y, z)),
          f(0(), y) -> y,
          f(i x, y) -> i x,
      f(g(x, y), z) -> g(f(x, z), f(y, z)),
    f(1(), g(x, y)) -> x,
    f(2(), g(x, y)) -> y,
            a(w, v) -> w,
            a(w, v) -> v}
   EDG:
    {(f#(f(x, y), z) -> f#(x, f(y, z)), f#(g(x, y), z) -> f#(x, z))
     (f#(f(x, y), z) -> f#(x, f(y, z)), f#(g(x, y), z) -> f#(y, z))
     (f#(f(x, y), z) -> f#(x, f(y, z)), f#(f(x, y), z) -> f#(x, f(y, z)))
     (f#(f(x, y), z) -> f#(x, f(y, z)), f#(f(x, y), z) -> f#(y, z))
     (f#(g(x, y), z) -> f#(x, z), f#(g(x, y), z) -> f#(x, z))
     (f#(g(x, y), z) -> f#(x, z), f#(g(x, y), z) -> f#(y, z))
     (f#(g(x, y), z) -> f#(x, z), f#(f(x, y), z) -> f#(x, f(y, z)))
     (f#(g(x, y), z) -> f#(x, z), f#(f(x, y), z) -> f#(y, z))
     (f#(g(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(y, z))
     (f#(g(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(x, f(y, z)))
     (f#(g(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(y, z))
     (f#(g(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(x, z))
     (f#(f(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(y, z))
     (f#(f(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(x, f(y, z)))
     (f#(f(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(y, z))
     (f#(f(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(x, z))}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {f#(f(x, y), z) -> f#(y, z),
        f#(f(x, y), z) -> f#(x, f(y, z)),
        f#(g(x, y), z) -> f#(y, z),
        f#(g(x, y), z) -> f#(x, z)}
      
      SCC (4):
       Strict:
        {f#(f(x, y), z) -> f#(y, z),
         f#(f(x, y), z) -> f#(x, f(y, z)),
         f#(g(x, y), z) -> f#(y, z),
         f#(g(x, y), z) -> f#(x, z)}
       Weak:
       {      f(x, 0()) -> x,
          f(f(x, y), z) -> f(x, f(y, z)),
              f(0(), y) -> y,
              f(i x, y) -> i x,
          f(g(x, y), z) -> g(f(x, z), f(y, z)),
        f(1(), g(x, y)) -> x,
        f(2(), g(x, y)) -> y}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1) = x0 + x1,
         
         [g](x0, x1) = x0 + x1 + 1,
         
         [i](x0) = 0,
         
         [0] = 0,
         
         [1] = 0,
         
         [2] = 1,
         
         [f#](x0, x1) = x0
        Strict:
         f#(g(x, y), z) -> f#(x, z)
         1 + 1y + 1x + 0z >= 0 + 1x + 0z
         f#(g(x, y), z) -> f#(y, z)
         1 + 1y + 1x + 0z >= 0 + 1y + 0z
         f#(f(x, y), z) -> f#(x, f(y, z))
         0 + 1y + 1x + 0z >= 0 + 0y + 1x + 0z
         f#(f(x, y), z) -> f#(y, z)
         0 + 1y + 1x + 0z >= 0 + 1y + 0z
        Weak:
         f(2(), g(x, y)) -> y
         2 + 1y + 1x >= 1y
         f(1(), g(x, y)) -> x
         1 + 1y + 1x >= 1x
         f(g(x, y), z) -> g(f(x, z), f(y, z))
         1 + 1y + 1x + 1z >= 1 + 1y + 1x + 2z
         f(i x, y) -> i x
         0 + 1y + 0x >= 0 + 0x
         f(0(), y) -> y
         0 + 1y >= 1y
         f(f(x, y), z) -> f(x, f(y, z))
         0 + 1y + 1x + 1z >= 0 + 1y + 1x + 1z
         f(x, 0()) -> x
         0 + 1x >= 1x
       SCCS (1):
        Scc:
         {f#(f(x, y), z) -> f#(y, z),
          f#(f(x, y), z) -> f#(x, f(y, z))}
        
        SCC (2):
         Strict:
          {f#(f(x, y), z) -> f#(y, z),
           f#(f(x, y), z) -> f#(x, f(y, z))}
         Weak:
         {      f(x, 0()) -> x,
            f(f(x, y), z) -> f(x, f(y, z)),
                f(0(), y) -> y,
                f(i x, y) -> i x,
            f(g(x, y), z) -> g(f(x, z), f(y, z)),
          f(1(), g(x, y)) -> x,
          f(2(), g(x, y)) -> y}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [f](x0, x1) = x0 + x1 + 1,
           
           [g](x0, x1) = 1,
           
           [i](x0) = 1,
           
           [0] = 0,
           
           [1] = 1,
           
           [2] = 1,
           
           [f#](x0, x1) = x0 + 1
          Strict:
           f#(f(x, y), z) -> f#(x, f(y, z))
           2 + 1y + 1x + 0z >= 1 + 0y + 1x + 0z
           f#(f(x, y), z) -> f#(y, z)
           2 + 1y + 1x + 0z >= 1 + 1y + 0z
          Weak:
           f(2(), g(x, y)) -> y
           3 + 0y + 0x >= 1y
           f(1(), g(x, y)) -> x
           3 + 0y + 0x >= 1x
           f(g(x, y), z) -> g(f(x, z), f(y, z))
           2 + 0y + 0x + 1z >= 1 + 0y + 0x + 0z
           f(i x, y) -> i x
           2 + 1y + 0x >= 1 + 0x
           f(0(), y) -> y
           1 + 1y >= 1y
           f(f(x, y), z) -> f(x, f(y, z))
           2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z
           f(x, 0()) -> x
           1 + 1x >= 1x
         Qed