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