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