YES
Time: 0.227808
TRS:
 {      mark f X -> active f X,
        mark g X -> active g mark X,
        mark a() -> active a(),
        f mark X -> f X,
      f active X -> f X,
        g mark X -> g X,
      g active X -> g X,
  active f f a() -> mark f g f a()}
 DP:
  DP:
   {      mark# f X -> active# f X,
          mark# g X -> mark# X,
          mark# g X -> g# mark X,
          mark# g X -> active# g mark X,
          mark# a() -> active# a(),
          f# mark X -> f# X,
        f# active X -> f# X,
          g# mark X -> g# X,
        g# active X -> g# X,
    active# f f a() -> mark# f g f a(),
    active# f f a() -> f# g f a(),
    active# f f a() -> g# f a()}
  TRS:
  {      mark f X -> active f X,
         mark g X -> active g mark X,
         mark a() -> active a(),
         f mark X -> f X,
       f active X -> f X,
         g mark X -> g X,
       g active X -> g X,
   active f f a() -> mark f g f a()}
  UR:
   {      mark f X -> active f X,
          mark g X -> active g mark X,
          mark a() -> active a(),
          f mark X -> f X,
        f active X -> f X,
          g mark X -> g X,
        g active X -> g X,
    active f f a() -> mark f g f a()}
   EDG:
    {(f# mark X -> f# X, f# active X -> f# X)
     (f# mark X -> f# X, f# mark X -> f# X)
     (g# mark X -> g# X, g# active X -> g# X)
     (g# mark X -> g# X, g# mark X -> g# X)
     (mark# f X -> active# f X, active# f f a() -> g# f a())
     (mark# f X -> active# f X, active# f f a() -> f# g f a())
     (mark# f X -> active# f X, active# f f a() -> mark# f g f a())
     (active# f f a() -> mark# f g f a(), mark# f X -> active# f X)
     (mark# g X -> g# mark X, g# mark X -> g# X)
     (mark# g X -> g# mark X, g# active X -> g# X)
     (g# active X -> g# X, g# mark X -> g# X)
     (g# active X -> g# X, g# active X -> g# X)
     (f# active X -> f# X, f# mark X -> f# X)
     (f# active X -> f# X, f# active X -> f# X)
     (mark# g X -> mark# X, mark# f X -> active# f X)
     (mark# g X -> mark# X, mark# g X -> mark# X)
     (mark# g X -> mark# X, mark# g X -> g# mark X)
     (mark# g X -> mark# X, mark# g X -> active# g mark X)
     (mark# g X -> mark# X, mark# a() -> active# a())}
    STATUS:
     arrows: 0.868056
     SCCS (4):
      Scc:
       {  f# mark X -> f# X,
        f# active X -> f# X}
      Scc:
       {mark# g X -> mark# X}
      Scc:
       {  g# mark X -> g# X,
        g# active X -> g# X}
      Scc:
       {      mark# f X -> active# f X,
        active# f f a() -> mark# f g f a()}
      
      SCC (2):
       Strict:
        {  f# mark X -> f# X,
         f# active X -> f# X}
       Weak:
       {      mark f X -> active f X,
              mark g X -> active g mark X,
              mark a() -> active a(),
              f mark X -> f X,
            f active X -> f X,
              g mark X -> g X,
            g active X -> g X,
        active f f a() -> mark f g f a()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [mark](x0) = x0 + 1,
         
         [f](x0) = 0,
         
         [g](x0) = x0 + 1,
         
         [active](x0) = x0 + 1,
         
         [a] = 1,
         
         [f#](x0) = x0 + 1
        Strict:
         f# active X -> f# X
         2 + 1X >= 1 + 1X
         f# mark X -> f# X
         2 + 1X >= 1 + 1X
        Weak:
         active f f a() -> mark f g f a()
         1 >= 1
         g active X -> g X
         2 + 1X >= 1 + 1X
         g mark X -> g X
         2 + 1X >= 1 + 1X
         f active X -> f X
         0 + 0X >= 0 + 0X
         f mark X -> f X
         0 + 0X >= 0 + 0X
         mark a() -> active a()
         2 >= 2
         mark g X -> active g mark X
         2 + 1X >= 3 + 1X
         mark f X -> active f X
         1 + 0X >= 1 + 0X
       Qed
     SCC (1):
      Strict:
       {mark# g X -> mark# X}
      Weak:
      {      mark f X -> active f X,
             mark g X -> active g mark X,
             mark a() -> active a(),
             f mark X -> f X,
           f active X -> f X,
             g mark X -> g X,
           g active X -> g X,
       active f f a() -> mark f g f a()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [mark](x0) = x0 + 1,
        
        [f](x0) = x0 + 1,
        
        [g](x0) = x0 + 1,
        
        [active](x0) = x0 + 1,
        
        [a] = 1,
        
        [mark#](x0) = x0 + 1
       Strict:
        mark# g X -> mark# X
        2 + 1X >= 1 + 1X
       Weak:
        active f f a() -> mark f g f a()
        4 >= 5
        g active X -> g X
        2 + 1X >= 1 + 1X
        g mark X -> g X
        2 + 1X >= 1 + 1X
        f active X -> f X
        2 + 1X >= 1 + 1X
        f mark X -> f X
        2 + 1X >= 1 + 1X
        mark a() -> active a()
        2 >= 2
        mark g X -> active g mark X
        2 + 1X >= 3 + 1X
        mark f X -> active f X
        2 + 1X >= 2 + 1X
      Qed
     
     
     SCC (2):
      Strict:
       {  g# mark X -> g# X,
        g# active X -> g# X}
      Weak:
      {      mark f X -> active f X,
             mark g X -> active g mark X,
             mark a() -> active a(),
             f mark X -> f X,
           f active X -> f X,
             g mark X -> g X,
           g active X -> g X,
       active f f a() -> mark f g f a()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [mark](x0) = x0 + 1,
        
        [f](x0) = 0,
        
        [g](x0) = x0 + 1,
        
        [active](x0) = x0 + 1,
        
        [a] = 1,
        
        [g#](x0) = x0 + 1
       Strict:
        g# active X -> g# X
        2 + 1X >= 1 + 1X
        g# mark X -> g# X
        2 + 1X >= 1 + 1X
       Weak:
        active f f a() -> mark f g f a()
        1 >= 1
        g active X -> g X
        2 + 1X >= 1 + 1X
        g mark X -> g X
        2 + 1X >= 1 + 1X
        f active X -> f X
        0 + 0X >= 0 + 0X
        f mark X -> f X
        0 + 0X >= 0 + 0X
        mark a() -> active a()
        2 >= 2
        mark g X -> active g mark X
        2 + 1X >= 3 + 1X
        mark f X -> active f X
        1 + 0X >= 1 + 0X
      Qed
    SCC (2):
     Strict:
      {      mark# f X -> active# f X,
       active# f f a() -> mark# f g f a()}
     Weak:
     {      mark f X -> active f X,
            mark g X -> active g mark X,
            mark a() -> active a(),
            f mark X -> f X,
          f active X -> f X,
            g mark X -> g X,
          g active X -> g X,
      active f f a() -> mark f g f a()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [mark](x0) = x0,
       
       [f](x0) = x0,
       
       [g](x0) = 0,
       
       [active](x0) = x0,
       
       [a] = 1,
       
       [mark#](x0) = x0,
       
       [active#](x0) = x0
      Strict:
       active# f f a() -> mark# f g f a()
       1 >= 0
       mark# f X -> active# f X
       0 + 1X >= 0 + 1X
      Weak:
       active f f a() -> mark f g f a()
       1 >= 0
       g active X -> g X
       0 + 0X >= 0 + 0X
       g mark X -> g X
       0 + 0X >= 0 + 0X
       f active X -> f X
       0 + 1X >= 0 + 1X
       f mark X -> f X
       0 + 1X >= 0 + 1X
       mark a() -> active a()
       1 >= 1
       mark g X -> active g mark X
       0 + 0X >= 0 + 0X
       mark f X -> active f X
       0 + 1X >= 0 + 1X
     SCCS (0):