YES
Time: 0.049049
TRS:
 {  f f x -> f c f x,
    f f x -> f d f x,
    g c x -> x,
  g c 1() -> g d 0(),
  g c 0() -> g d 1(),
    g d x -> x}
 DP:
  DP:
   {  f# f x -> f# c f x,
      f# f x -> f# d f x,
    g# c 1() -> g# d 0(),
    g# c 0() -> g# d 1()}
  TRS:
  {  f f x -> f c f x,
     f f x -> f d f x,
     g c x -> x,
   g c 1() -> g d 0(),
   g c 0() -> g d 1(),
     g d x -> x}
  UR:
   {f f x -> f c f x,
    f f x -> f d f x}
   EDG:
    {(f# f x -> f# d f x, f# f x -> f# d f x)
     (f# f x -> f# d f x, f# f x -> f# c f x)
     (g# c 0() -> g# d 1(), g# c 0() -> g# d 1())
     (g# c 0() -> g# d 1(), g# c 1() -> g# d 0())
     (g# c 1() -> g# d 0(), g# c 1() -> g# d 0())
     (g# c 1() -> g# d 0(), g# c 0() -> g# d 1())
     (f# f x -> f# c f x, f# f x -> f# c f x)
     (f# f x -> f# c f x, f# f x -> f# d f x)}
    STATUS:
     arrows: 0.500000
     SCCS (2):
      Scc:
       {g# c 1() -> g# d 0(),
        g# c 0() -> g# d 1()}
      Scc:
       {f# f x -> f# c f x,
        f# f x -> f# d f x}
      
      SCC (2):
       Strict:
        {g# c 1() -> g# d 0(),
         g# c 0() -> g# d 1()}
       Weak:
       {  f f x -> f c f x,
          f f x -> f d f x,
          g c x -> x,
        g c 1() -> g d 0(),
        g c 0() -> g d 1(),
          g d x -> x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0) = 0,
         
         [c](x0) = x0 + 1,
         
         [d](x0) = 1,
         
         [g](x0) = 0,
         
         [1] = 1,
         
         [0] = 1,
         
         [g#](x0) = x0
        Strict:
         g# c 0() -> g# d 1()
         2 >= 1
         g# c 1() -> g# d 0()
         2 >= 1
        Weak:
         g d x -> x
         0 + 0x >= 1x
         g c 0() -> g d 1()
         0 >= 0
         g c 1() -> g d 0()
         0 >= 0
         g c x -> x
         0 + 0x >= 1x
         f f x -> f d f x
         0 + 0x >= 0 + 0x
         f f x -> f c f x
         0 + 0x >= 0 + 0x
       Qed
     SCC (2):
      Strict:
       {f# f x -> f# c f x,
        f# f x -> f# d f 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 0(),
       g c 0() -> g d 1(),
         g d x -> x}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0) = 1,
        
        [c](x0) = 0,
        
        [d](x0) = 0,
        
        [g](x0) = 0,
        
        [1] = 0,
        
        [0] = 0,
        
        [f#](x0) = x0
       Strict:
        f# f x -> f# d f x
        1 + 0x >= 0 + 0x
        f# f x -> f# c f x
        1 + 0x >= 0 + 0x
       Weak:
        g d x -> x
        0 + 0x >= 1x
        g c 0() -> g d 1()
        0 >= 0
        g c 1() -> g d 0()
        0 >= 0
        g c x -> x
        0 + 0x >= 1x
        f f x -> f d f x
        1 + 0x >= 1 + 0x
        f f x -> f c f x
        1 + 0x >= 1 + 0x
      Qed