YES
Time: 0.016543
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)}
  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