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