YES
Time: 0.240126
TRS:
 {    mark c X -> active c X,
      mark f X -> active f mark X,
      mark g X -> active g X,
      mark d X -> active d X,
      mark h X -> active h mark X,
      c mark X -> c X,
    c active X -> c X,
      f mark X -> f X,
    f active X -> f X,
      g mark X -> g X,
    g active X -> g X,
    active c X -> mark d X,
  active f f X -> mark c f g f X,
    active h X -> mark c d X,
      d mark X -> d X,
    d active X -> d X,
      h mark X -> h X,
    h active X -> h X}
 DP:
  DP:
   {    mark# c X -> active# c X,
        mark# f X -> mark# X,
        mark# f X -> f# mark X,
        mark# f X -> active# f mark X,
        mark# g X -> active# g X,
        mark# d X -> active# d X,
        mark# h X -> mark# X,
        mark# h X -> active# h mark X,
        mark# h X -> h# mark X,
        c# mark X -> c# X,
      c# active X -> c# X,
        f# mark X -> f# X,
      f# active X -> f# X,
        g# mark X -> g# X,
      g# active X -> g# X,
      active# c X -> mark# d X,
      active# c X -> d# X,
    active# f f X -> mark# c f g f X,
    active# f f X -> c# f g f X,
    active# f f X -> f# g f X,
    active# f f X -> g# f X,
      active# h X -> mark# c d X,
      active# h X -> c# d X,
      active# h X -> d# X,
        d# mark X -> d# X,
      d# active X -> d# X,
        h# mark X -> h# X,
      h# active X -> h# X}
  TRS:
  {    mark c X -> active c X,
       mark f X -> active f mark X,
       mark g X -> active g X,
       mark d X -> active d X,
       mark h X -> active h mark X,
       c mark X -> c X,
     c active X -> c X,
       f mark X -> f X,
     f active X -> f X,
       g mark X -> g X,
     g active X -> g X,
     active c X -> mark d X,
   active f f X -> mark c f g f X,
     active h X -> mark c d X,
       d mark X -> d X,
     d active X -> d X,
       h mark X -> h X,
     h active X -> h X}
  EDG:
   {(mark# h X -> active# h mark X, active# h X -> d# X)
    (mark# h X -> active# h mark X, active# h X -> c# d X)
    (mark# h X -> active# h mark X, active# h X -> mark# c d X)
    (mark# h X -> active# h mark X, active# f f X -> g# f X)
    (mark# h X -> active# h mark X, active# f f X -> f# g f X)
    (mark# h X -> active# h mark X, active# f f X -> c# f g f X)
    (mark# h X -> active# h mark X, active# f f X -> mark# c f g f X)
    (mark# h X -> active# h mark X, active# c X -> d# X)
    (mark# h X -> active# h mark X, active# c X -> mark# d X)
    (active# h X -> mark# c d X, mark# h X -> h# mark X)
    (active# h X -> mark# c d X, mark# h X -> active# h mark X)
    (active# h X -> mark# c d X, mark# h X -> mark# X)
    (active# h X -> mark# c d X, mark# d X -> active# d X)
    (active# h X -> mark# c d X, mark# g X -> active# g X)
    (active# h X -> mark# c d X, mark# f X -> active# f mark X)
    (active# h X -> mark# c d X, mark# f X -> f# mark X)
    (active# h X -> mark# c d X, mark# f X -> mark# X)
    (active# h X -> mark# c d X, mark# c X -> active# c X)
    (mark# h X -> mark# X, mark# h X -> h# mark X)
    (mark# h X -> mark# X, mark# h X -> active# h mark X)
    (mark# h X -> mark# X, mark# h X -> mark# X)
    (mark# h X -> mark# X, mark# d X -> active# d X)
    (mark# h X -> mark# X, mark# g X -> active# g X)
    (mark# h X -> mark# X, mark# f X -> active# f mark X)
    (mark# h X -> mark# X, mark# f X -> f# mark X)
    (mark# h X -> mark# X, mark# f X -> mark# X)
    (mark# h X -> mark# X, mark# c X -> active# c X)
    (c# active X -> c# X, c# active X -> c# X)
    (c# active X -> c# X, c# mark X -> c# X)
    (f# active X -> f# X, f# active X -> f# X)
    (f# active X -> f# X, f# mark X -> f# X)
    (g# active X -> g# X, g# active X -> g# X)
    (g# active X -> g# X, g# mark X -> g# X)
    (d# active X -> d# X, d# active X -> d# X)
    (d# active X -> d# X, d# mark X -> d# X)
    (h# active X -> h# X, h# active X -> h# X)
    (h# active X -> h# X, h# mark X -> h# X)
    (mark# f X -> f# mark X, f# active X -> f# X)
    (mark# f X -> f# mark X, f# mark X -> f# X)
    (mark# d X -> active# d X, active# h X -> d# X)
    (mark# d X -> active# d X, active# h X -> c# d X)
    (mark# d X -> active# d X, active# h X -> mark# c d X)
    (mark# d X -> active# d X, active# f f X -> g# f X)
    (mark# d X -> active# d X, active# f f X -> f# g f X)
    (mark# d X -> active# d X, active# f f X -> c# f g f X)
    (mark# d X -> active# d X, active# f f X -> mark# c f g f X)
    (mark# d X -> active# d X, active# c X -> d# X)
    (mark# d X -> active# d X, active# c X -> mark# d X)
    (active# c X -> mark# d X, mark# h X -> h# mark X)
    (active# c X -> mark# d X, mark# h X -> active# h mark X)
    (active# c X -> mark# d X, mark# h X -> mark# X)
    (active# c X -> mark# d X, mark# d X -> active# d X)
    (active# c X -> mark# d X, mark# g X -> active# g X)
    (active# c X -> mark# d X, mark# f X -> active# f mark X)
    (active# c X -> mark# d X, mark# f X -> f# mark X)
    (active# c X -> mark# d X, mark# f X -> mark# X)
    (active# c X -> mark# d X, mark# c X -> active# c X)
    (active# h X -> c# d X, c# active X -> c# X)
    (active# h X -> c# d X, c# mark X -> c# X)
    (active# f f X -> c# f g f X, c# active X -> c# X)
    (active# f f X -> c# f g f X, c# mark X -> c# X)
    (active# f f X -> mark# c f g f X, mark# c X -> active# c X)
    (active# f f X -> mark# c f g f X, mark# f X -> mark# X)
    (active# f f X -> mark# c f g f X, mark# f X -> f# mark X)
    (active# f f X -> mark# c f g f X, mark# f X -> active# f mark X)
    (active# f f X -> mark# c f g f X, mark# g X -> active# g X)
    (active# f f X -> mark# c f g f X, mark# d X -> active# d X)
    (active# f f X -> mark# c f g f X, mark# h X -> mark# X)
    (active# f f X -> mark# c f g f X, mark# h X -> active# h mark X)
    (active# f f X -> mark# c f g f X, mark# h X -> h# mark X)
    (active# f f X -> g# f X, g# mark X -> g# X)
    (active# f f X -> g# f X, g# active X -> g# X)
    (mark# h X -> h# mark X, h# mark X -> h# X)
    (mark# h X -> h# mark X, h# active X -> h# X)
    (mark# g X -> active# g X, active# c X -> mark# d X)
    (mark# g X -> active# g X, active# c X -> d# X)
    (mark# g X -> active# g X, active# f f X -> mark# c f g f X)
    (mark# g X -> active# g X, active# f f X -> c# f g f X)
    (mark# g X -> active# g X, active# f f X -> f# g f X)
    (mark# g X -> active# g X, active# f f X -> g# f X)
    (mark# g X -> active# g X, active# h X -> mark# c d X)
    (mark# g X -> active# g X, active# h X -> c# d X)
    (mark# g X -> active# g X, active# h X -> d# X)
    (mark# c X -> active# c X, active# c X -> mark# d X)
    (mark# c X -> active# c X, active# c X -> d# X)
    (mark# c X -> active# c X, active# f f X -> mark# c f g f X)
    (mark# c X -> active# c X, active# f f X -> c# f g f X)
    (mark# c X -> active# c X, active# f f X -> f# g f X)
    (mark# c X -> active# c X, active# f f X -> g# f X)
    (mark# c X -> active# c X, active# h X -> mark# c d X)
    (mark# c X -> active# c X, active# h X -> c# d X)
    (mark# c X -> active# c X, active# h X -> d# X)
    (h# mark X -> h# X, h# mark X -> h# X)
    (h# mark X -> h# X, h# active X -> h# X)
    (d# mark X -> d# X, d# mark X -> d# X)
    (d# mark X -> d# X, d# active X -> d# X)
    (g# mark X -> g# X, g# mark X -> g# X)
    (g# mark X -> g# X, g# active X -> g# X)
    (f# mark X -> f# X, f# mark X -> f# X)
    (f# mark X -> f# X, f# active X -> f# X)
    (c# mark X -> c# X, c# mark X -> c# X)
    (c# mark X -> c# X, c# active X -> c# X)
    (mark# f X -> mark# X, mark# c X -> active# c X)
    (mark# f X -> mark# X, mark# f X -> mark# X)
    (mark# f X -> mark# X, mark# f X -> f# mark X)
    (mark# f X -> mark# X, mark# f X -> active# f mark X)
    (mark# f X -> mark# X, mark# g X -> active# g X)
    (mark# f X -> mark# X, mark# d X -> active# d X)
    (mark# f X -> mark# X, mark# h X -> mark# X)
    (mark# f X -> mark# X, mark# h X -> active# h mark X)
    (mark# f X -> mark# X, mark# h X -> h# mark X)
    (active# f f X -> f# g f X, f# mark X -> f# X)
    (active# f f X -> f# g f X, f# active X -> f# X)
    (mark# f X -> active# f mark X, active# c X -> mark# d X)
    (mark# f X -> active# f mark X, active# c X -> d# X)
    (mark# f X -> active# f mark X, active# f f X -> mark# c f g f X)
    (mark# f X -> active# f mark X, active# f f X -> c# f g f X)
    (mark# f X -> active# f mark X, active# f f X -> f# g f X)
    (mark# f X -> active# f mark X, active# f f X -> g# f X)
    (mark# f X -> active# f mark X, active# h X -> mark# c d X)
    (mark# f X -> active# f mark X, active# h X -> c# d X)
    (mark# f X -> active# f mark X, active# h X -> d# X)}
   STATUS:
    arrows: 0.844388
    SCCS (6):
     Scc:
      {  d# mark X -> d# X,
       d# active X -> d# X}
     Scc:
      {    mark# c X -> active# c X,
           mark# f X -> mark# X,
           mark# f X -> active# f mark X,
           mark# g X -> active# g X,
           mark# d X -> active# d X,
           mark# h X -> mark# X,
           mark# h X -> active# h mark X,
         active# c X -> mark# d X,
       active# f f X -> mark# c f g f X,
         active# h X -> mark# c d X}
     Scc:
      {  h# mark X -> h# X,
       h# active X -> h# X}
     Scc:
      {  g# mark X -> g# X,
       g# active X -> g# X}
     Scc:
      {  c# mark X -> c# X,
       c# active X -> c# X}
     Scc:
      {  f# mark X -> f# X,
       f# active X -> f# X}
     
     SCC (2):
      Strict:
       {  d# mark X -> d# X,
        d# active X -> d# X}
      Weak:
      {    mark c X -> active c X,
           mark f X -> active f mark X,
           mark g X -> active g X,
           mark d X -> active d X,
           mark h X -> active h mark X,
           c mark X -> c X,
         c active X -> c X,
           f mark X -> f X,
         f active X -> f X,
           g mark X -> g X,
         g active X -> g X,
         active c X -> mark d X,
       active f f X -> mark c f g f X,
         active h X -> mark c d X,
           d mark X -> d X,
         d active X -> d X,
           h mark X -> h X,
         h active X -> h X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [mark](x0) = x0,
        
        [c](x0) = 0,
        
        [f](x0) = 0,
        
        [g](x0) = 0,
        
        [active](x0) = x0 + 1,
        
        [d](x0) = x0 + 1,
        
        [h](x0) = 0,
        
        [d#](x0) = x0
       Strict:
        d# active X -> d# X
        1 + 1X >= 0 + 1X
        d# mark X -> d# X
        0 + 1X >= 0 + 1X
       Weak:
        h active X -> h X
        0 + 0X >= 0 + 0X
        h mark X -> h X
        0 + 0X >= 0 + 0X
        d active X -> d X
        2 + 1X >= 1 + 1X
        d mark X -> d X
        1 + 1X >= 1 + 1X
        active h X -> mark c d X
        1 + 0X >= 0 + 0X
        active f f X -> mark c f g f X
        1 + 0X >= 0 + 0X
        active c X -> mark d X
        1 + 0X >= 1 + 1X
        g active X -> g X
        0 + 0X >= 0 + 0X
        g mark X -> g X
        0 + 0X >= 0 + 0X
        f active X -> f X
        0 + 0X >= 0 + 0X
        f mark X -> f X
        0 + 0X >= 0 + 0X
        c active X -> c X
        0 + 0X >= 0 + 0X
        c mark X -> c X
        0 + 0X >= 0 + 0X
        mark h X -> active h mark X
        0 + 0X >= 1 + 0X
        mark d X -> active d X
        1 + 1X >= 2 + 1X
        mark g X -> active g X
        0 + 0X >= 1 + 0X
        mark f X -> active f mark X
        0 + 0X >= 1 + 0X
        mark c X -> active c X
        0 + 0X >= 1 + 0X
      SCCS (1):
       Scc:
        {d# mark X -> d# X}
       
       SCC (1):
        Strict:
         {d# mark X -> d# X}
        Weak:
        {    mark c X -> active c X,
             mark f X -> active f mark X,
             mark g X -> active g X,
             mark d X -> active d X,
             mark h X -> active h mark X,
             c mark X -> c X,
           c active X -> c X,
             f mark X -> f X,
           f active X -> f X,
             g mark X -> g X,
           g active X -> g X,
           active c X -> mark d X,
         active f f X -> mark c f g f X,
           active h X -> mark c d X,
             d mark X -> d X,
           d active X -> d X,
             h mark X -> h X,
           h active X -> h X}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [mark](x0) = x0 + 1,
          
          [c](x0) = x0 + 1,
          
          [f](x0) = x0 + 1,
          
          [g](x0) = x0 + 1,
          
          [active](x0) = x0,
          
          [d](x0) = 0,
          
          [h](x0) = x0 + 1,
          
          [d#](x0) = x0
         Strict:
          d# mark X -> d# X
          1 + 1X >= 0 + 1X
         Weak:
          h active X -> h X
          1 + 1X >= 1 + 1X
          h mark X -> h X
          2 + 1X >= 1 + 1X
          d active X -> d X
          0 + 0X >= 0 + 0X
          d mark X -> d X
          0 + 0X >= 0 + 0X
          active h X -> mark c d X
          1 + 1X >= 2 + 0X
          active f f X -> mark c f g f X
          2 + 1X >= 5 + 1X
          active c X -> mark d X
          1 + 1X >= 1 + 0X
          g active X -> g X
          1 + 1X >= 1 + 1X
          g mark X -> g X
          2 + 1X >= 1 + 1X
          f active X -> f X
          1 + 1X >= 1 + 1X
          f mark X -> f X
          2 + 1X >= 1 + 1X
          c active X -> c X
          1 + 1X >= 1 + 1X
          c mark X -> c X
          2 + 1X >= 1 + 1X
          mark h X -> active h mark X
          2 + 1X >= 2 + 1X
          mark d X -> active d X
          1 + 0X >= 0 + 0X
          mark g X -> active g X
          2 + 1X >= 1 + 1X
          mark f X -> active f mark X
          2 + 1X >= 2 + 1X
          mark c X -> active c X
          2 + 1X >= 1 + 1X
        Qed
    SCC (10):
     Strict:
      {    mark# c X -> active# c X,
           mark# f X -> mark# X,
           mark# f X -> active# f mark X,
           mark# g X -> active# g X,
           mark# d X -> active# d X,
           mark# h X -> mark# X,
           mark# h X -> active# h mark X,
         active# c X -> mark# d X,
       active# f f X -> mark# c f g f X,
         active# h X -> mark# c d X}
     Weak:
     {    mark c X -> active c X,
          mark f X -> active f mark X,
          mark g X -> active g X,
          mark d X -> active d X,
          mark h X -> active h mark X,
          c mark X -> c X,
        c active X -> c X,
          f mark X -> f X,
        f active X -> f X,
          g mark X -> g X,
        g active X -> g X,
        active c X -> mark d X,
      active f f X -> mark c f g f X,
        active h X -> mark c d X,
          d mark X -> d X,
        d active X -> d X,
          h mark X -> h X,
        h active X -> h X}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [mark](x0) = x0,
       
       [c](x0) = 0,
       
       [f](x0) = x0 + 1,
       
       [g](x0) = 0,
       
       [active](x0) = x0,
       
       [d](x0) = 0,
       
       [h](x0) = x0,
       
       [mark#](x0) = x0,
       
       [active#](x0) = x0
      Strict:
       active# h X -> mark# c d X
       0 + 1X >= 0 + 0X
       active# f f X -> mark# c f g f X
       2 + 1X >= 0 + 0X
       active# c X -> mark# d X
       0 + 0X >= 0 + 0X
       mark# h X -> active# h mark X
       0 + 1X >= 0 + 1X
       mark# h X -> mark# X
       0 + 1X >= 0 + 1X
       mark# d X -> active# d X
       0 + 0X >= 0 + 0X
       mark# g X -> active# g X
       0 + 0X >= 0 + 0X
       mark# f X -> active# f mark X
       1 + 1X >= 1 + 1X
       mark# f X -> mark# X
       1 + 1X >= 0 + 1X
       mark# c X -> active# c X
       0 + 0X >= 0 + 0X
      Weak:
       h active X -> h X
       0 + 1X >= 0 + 1X
       h mark X -> h X
       0 + 1X >= 0 + 1X
       d active X -> d X
       0 + 0X >= 0 + 0X
       d mark X -> d X
       0 + 0X >= 0 + 0X
       active h X -> mark c d X
       0 + 1X >= 0 + 0X
       active f f X -> mark c f g f X
       2 + 1X >= 0 + 0X
       active c X -> mark d X
       0 + 0X >= 0 + 0X
       g active X -> g X
       0 + 0X >= 0 + 0X
       g mark X -> g X
       0 + 0X >= 0 + 0X
       f active X -> f X
       1 + 1X >= 1 + 1X
       f mark X -> f X
       1 + 1X >= 1 + 1X
       c active X -> c X
       0 + 0X >= 0 + 0X
       c mark X -> c X
       0 + 0X >= 0 + 0X
       mark h X -> active h mark X
       0 + 1X >= 0 + 1X
       mark d X -> active d X
       0 + 0X >= 0 + 0X
       mark g X -> active g X
       0 + 0X >= 0 + 0X
       mark f X -> active f mark X
       1 + 1X >= 1 + 1X
       mark c X -> active c X
       0 + 0X >= 0 + 0X
     SCCS (1):
      Scc:
       {  mark# c X -> active# c X,
          mark# f X -> active# f mark X,
          mark# g X -> active# g X,
          mark# d X -> active# d X,
          mark# h X -> mark# X,
          mark# h X -> active# h mark X,
        active# c X -> mark# d X,
        active# h X -> mark# c d X}
      
      SCC (8):
       Strict:
        {  mark# c X -> active# c X,
           mark# f X -> active# f mark X,
           mark# g X -> active# g X,
           mark# d X -> active# d X,
           mark# h X -> mark# X,
           mark# h X -> active# h mark X,
         active# c X -> mark# d X,
         active# h X -> mark# c d X}
       Weak:
       {    mark c X -> active c X,
            mark f X -> active f mark X,
            mark g X -> active g X,
            mark d X -> active d X,
            mark h X -> active h mark X,
            c mark X -> c X,
          c active X -> c X,
            f mark X -> f X,
          f active X -> f X,
            g mark X -> g X,
          g active X -> g X,
          active c X -> mark d X,
        active f f X -> mark c f g f X,
          active h X -> mark c d X,
            d mark X -> d X,
          d active X -> d X,
            h mark X -> h X,
          h active X -> h X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [mark](x0) = x0,
         
         [c](x0) = x0,
         
         [f](x0) = 0,
         
         [g](x0) = 1,
         
         [active](x0) = x0,
         
         [d](x0) = 0,
         
         [h](x0) = x0,
         
         [mark#](x0) = x0,
         
         [active#](x0) = 0
        Strict:
         active# h X -> mark# c d X
         0 + 0X >= 0 + 0X
         active# c X -> mark# d X
         0 + 0X >= 0 + 0X
         mark# h X -> active# h mark X
         0 + 1X >= 0 + 0X
         mark# h X -> mark# X
         0 + 1X >= 0 + 1X
         mark# d X -> active# d X
         0 + 0X >= 0 + 0X
         mark# g X -> active# g X
         1 + 0X >= 0 + 0X
         mark# f X -> active# f mark X
         0 + 0X >= 0 + 0X
         mark# c X -> active# c X
         0 + 1X >= 0 + 0X
        Weak:
         h active X -> h X
         0 + 1X >= 0 + 1X
         h mark X -> h X
         0 + 1X >= 0 + 1X
         d active X -> d X
         0 + 0X >= 0 + 0X
         d mark X -> d X
         0 + 0X >= 0 + 0X
         active h X -> mark c d X
         0 + 1X >= 0 + 0X
         active f f X -> mark c f g f X
         0 + 0X >= 0 + 0X
         active c X -> mark d X
         0 + 1X >= 0 + 0X
         g active X -> g X
         1 + 0X >= 1 + 0X
         g mark X -> g X
         1 + 0X >= 1 + 0X
         f active X -> f X
         0 + 0X >= 0 + 0X
         f mark X -> f X
         0 + 0X >= 0 + 0X
         c active X -> c X
         0 + 1X >= 0 + 1X
         c mark X -> c X
         0 + 1X >= 0 + 1X
         mark h X -> active h mark X
         0 + 1X >= 0 + 1X
         mark d X -> active d X
         0 + 0X >= 0 + 0X
         mark g X -> active g X
         1 + 0X >= 1 + 0X
         mark f X -> active f mark X
         0 + 0X >= 0 + 0X
         mark c X -> active c X
         0 + 1X >= 0 + 1X
       SCCS (1):
        Scc:
         {  mark# c X -> active# c X,
            mark# f X -> active# f mark X,
            mark# d X -> active# d X,
            mark# h X -> mark# X,
            mark# h X -> active# h mark X,
          active# c X -> mark# d X,
          active# h X -> mark# c d X}
        
        SCC (7):
         Strict:
          {  mark# c X -> active# c X,
             mark# f X -> active# f mark X,
             mark# d X -> active# d X,
             mark# h X -> mark# X,
             mark# h X -> active# h mark X,
           active# c X -> mark# d X,
           active# h X -> mark# c d X}
         Weak:
         {    mark c X -> active c X,
              mark f X -> active f mark X,
              mark g X -> active g X,
              mark d X -> active d X,
              mark h X -> active h mark X,
              c mark X -> c X,
            c active X -> c X,
              f mark X -> f X,
            f active X -> f X,
              g mark X -> g X,
            g active X -> g X,
            active c X -> mark d X,
          active f f X -> mark c f g f X,
            active h X -> mark c d X,
              d mark X -> d X,
            d active X -> d X,
              h mark X -> h X,
            h active X -> h X}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [mark](x0) = 0,
           
           [c](x0) = 0,
           
           [f](x0) = 1,
           
           [g](x0) = 0,
           
           [active](x0) = 0,
           
           [d](x0) = 0,
           
           [h](x0) = x0,
           
           [mark#](x0) = x0,
           
           [active#](x0) = 0
          Strict:
           active# h X -> mark# c d X
           0 + 0X >= 0 + 0X
           active# c X -> mark# d X
           0 + 0X >= 0 + 0X
           mark# h X -> active# h mark X
           0 + 1X >= 0 + 0X
           mark# h X -> mark# X
           0 + 1X >= 0 + 1X
           mark# d X -> active# d X
           0 + 0X >= 0 + 0X
           mark# f X -> active# f mark X
           1 + 0X >= 0 + 0X
           mark# c X -> active# c X
           0 + 0X >= 0 + 0X
          Weak:
           h active X -> h X
           0 + 0X >= 0 + 1X
           h mark X -> h X
           0 + 0X >= 0 + 1X
           d active X -> d X
           0 + 0X >= 0 + 0X
           d mark X -> d X
           0 + 0X >= 0 + 0X
           active h X -> mark c d X
           0 + 0X >= 0 + 0X
           active f f X -> mark c f g f X
           0 + 0X >= 0 + 0X
           active c X -> mark d X
           0 + 0X >= 0 + 0X
           g active X -> g X
           0 + 0X >= 0 + 0X
           g mark X -> g X
           0 + 0X >= 0 + 0X
           f active X -> f X
           1 + 0X >= 1 + 0X
           f mark X -> f X
           1 + 0X >= 1 + 0X
           c active X -> c X
           0 + 0X >= 0 + 0X
           c mark X -> c X
           0 + 0X >= 0 + 0X
           mark h X -> active h mark X
           0 + 0X >= 0 + 0X
           mark d X -> active d X
           0 + 0X >= 0 + 0X
           mark g X -> active g X
           0 + 0X >= 0 + 0X
           mark f X -> active f mark X
           0 + 0X >= 0 + 0X
           mark c X -> active c X
           0 + 0X >= 0 + 0X
         SCCS (1):
          Scc:
           {  mark# c X -> active# c X,
              mark# d X -> active# d X,
              mark# h X -> mark# X,
              mark# h X -> active# h mark X,
            active# c X -> mark# d X,
            active# h X -> mark# c d X}
          
          SCC (6):
           Strict:
            {  mark# c X -> active# c X,
               mark# d X -> active# d X,
               mark# h X -> mark# X,
               mark# h X -> active# h mark X,
             active# c X -> mark# d X,
             active# h X -> mark# c d X}
           Weak:
           {    mark c X -> active c X,
                mark f X -> active f mark X,
                mark g X -> active g X,
                mark d X -> active d X,
                mark h X -> active h mark X,
                c mark X -> c X,
              c active X -> c X,
                f mark X -> f X,
              f active X -> f X,
                g mark X -> g X,
              g active X -> g X,
              active c X -> mark d X,
            active f f X -> mark c f g f X,
              active h X -> mark c d X,
                d mark X -> d X,
              d active X -> d X,
                h mark X -> h X,
              h active X -> h X}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [mark](x0) = 0,
             
             [c](x0) = 0,
             
             [f](x0) = 0,
             
             [g](x0) = 0,
             
             [active](x0) = 0,
             
             [d](x0) = 0,
             
             [h](x0) = x0 + 1,
             
             [mark#](x0) = x0,
             
             [active#](x0) = 0
            Strict:
             active# h X -> mark# c d X
             0 + 0X >= 0 + 0X
             active# c X -> mark# d X
             0 + 0X >= 0 + 0X
             mark# h X -> active# h mark X
             1 + 1X >= 0 + 0X
             mark# h X -> mark# X
             1 + 1X >= 0 + 1X
             mark# d X -> active# d X
             0 + 0X >= 0 + 0X
             mark# c X -> active# c X
             0 + 0X >= 0 + 0X
            Weak:
             h active X -> h X
             1 + 0X >= 1 + 1X
             h mark X -> h X
             1 + 0X >= 1 + 1X
             d active X -> d X
             0 + 0X >= 0 + 0X
             d mark X -> d X
             0 + 0X >= 0 + 0X
             active h X -> mark c d X
             0 + 0X >= 0 + 0X
             active f f X -> mark c f g f X
             0 + 0X >= 0 + 0X
             active c X -> mark d X
             0 + 0X >= 0 + 0X
             g active X -> g X
             0 + 0X >= 0 + 0X
             g mark X -> g X
             0 + 0X >= 0 + 0X
             f active X -> f X
             0 + 0X >= 0 + 0X
             f mark X -> f X
             0 + 0X >= 0 + 0X
             c active X -> c X
             0 + 0X >= 0 + 0X
             c mark X -> c X
             0 + 0X >= 0 + 0X
             mark h X -> active h mark X
             0 + 0X >= 0 + 0X
             mark d X -> active d X
             0 + 0X >= 0 + 0X
             mark g X -> active g X
             0 + 0X >= 0 + 0X
             mark f X -> active f mark X
             0 + 0X >= 0 + 0X
             mark c X -> active c X
             0 + 0X >= 0 + 0X
           SCCS (1):
            Scc:
             {  mark# c X -> active# c X,
                mark# d X -> active# d X,
              active# c X -> mark# d X,
              active# h X -> mark# c d X}
            
            SCC (4):
             Strict:
              {  mark# c X -> active# c X,
                 mark# d X -> active# d X,
               active# c X -> mark# d X,
               active# h X -> mark# c d X}
             Weak:
             {    mark c X -> active c X,
                  mark f X -> active f mark X,
                  mark g X -> active g X,
                  mark d X -> active d X,
                  mark h X -> active h mark X,
                  c mark X -> c X,
                c active X -> c X,
                  f mark X -> f X,
                f active X -> f X,
                  g mark X -> g X,
                g active X -> g X,
                active c X -> mark d X,
              active f f X -> mark c f g f X,
                active h X -> mark c d X,
                  d mark X -> d X,
                d active X -> d X,
                  h mark X -> h X,
                h active X -> h X}
             POLY:
              Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
              Interpretation:
               [mark](x0) = 0,
               
               [c](x0) = 0,
               
               [f](x0) = 0,
               
               [g](x0) = 0,
               
               [active](x0) = 0,
               
               [d](x0) = 0,
               
               [h](x0) = 1,
               
               [mark#](x0) = 0,
               
               [active#](x0) = x0
              Strict:
               active# h X -> mark# c d X
               1 + 0X >= 0 + 0X
               active# c X -> mark# d X
               0 + 0X >= 0 + 0X
               mark# d X -> active# d X
               0 + 0X >= 0 + 0X
               mark# c X -> active# c X
               0 + 0X >= 0 + 0X
              Weak:
               h active X -> h X
               1 + 0X >= 1 + 0X
               h mark X -> h X
               1 + 0X >= 1 + 0X
               d active X -> d X
               0 + 0X >= 0 + 0X
               d mark X -> d X
               0 + 0X >= 0 + 0X
               active h X -> mark c d X
               0 + 0X >= 0 + 0X
               active f f X -> mark c f g f X
               0 + 0X >= 0 + 0X
               active c X -> mark d X
               0 + 0X >= 0 + 0X
               g active X -> g X
               0 + 0X >= 0 + 0X
               g mark X -> g X
               0 + 0X >= 0 + 0X
               f active X -> f X
               0 + 0X >= 0 + 0X
               f mark X -> f X
               0 + 0X >= 0 + 0X
               c active X -> c X
               0 + 0X >= 0 + 0X
               c mark X -> c X
               0 + 0X >= 0 + 0X
               mark h X -> active h mark X
               0 + 0X >= 0 + 0X
               mark d X -> active d X
               0 + 0X >= 0 + 0X
               mark g X -> active g X
               0 + 0X >= 0 + 0X
               mark f X -> active f mark X
               0 + 0X >= 0 + 0X
               mark c X -> active c X
               0 + 0X >= 0 + 0X
             SCCS (1):
              Scc:
               {  mark# c X -> active# c X,
                  mark# d X -> active# d X,
                active# c X -> mark# d X}
              
              SCC (3):
               Strict:
                {  mark# c X -> active# c X,
                   mark# d X -> active# d X,
                 active# c X -> mark# d X}
               Weak:
               {    mark c X -> active c X,
                    mark f X -> active f mark X,
                    mark g X -> active g X,
                    mark d X -> active d X,
                    mark h X -> active h mark X,
                    c mark X -> c X,
                  c active X -> c X,
                    f mark X -> f X,
                  f active X -> f X,
                    g mark X -> g X,
                  g active X -> g X,
                  active c X -> mark d X,
                active f f X -> mark c f g f X,
                  active h X -> mark c d X,
                    d mark X -> d X,
                  d active X -> d X,
                    h mark X -> h X,
                  h active X -> h X}
               POLY:
                Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
                Interpretation:
                 [mark](x0) = x0 + 1,
                 
                 [c](x0) = 1,
                 
                 [f](x0) = x0 + 1,
                 
                 [g](x0) = x0 + 1,
                 
                 [active](x0) = x0,
                 
                 [d](x0) = 0,
                 
                 [h](x0) = 0,
                 
                 [mark#](x0) = x0 + 1,
                 
                 [active#](x0) = x0 + 1
                Strict:
                 active# c X -> mark# d X
                 2 + 0X >= 1 + 0X
                 mark# d X -> active# d X
                 1 + 0X >= 1 + 0X
                 mark# c X -> active# c X
                 2 + 0X >= 2 + 0X
                Weak:
                 h active X -> h X
                 0 + 0X >= 0 + 0X
                 h mark X -> h X
                 0 + 0X >= 0 + 0X
                 d active X -> d X
                 0 + 0X >= 0 + 0X
                 d mark X -> d X
                 0 + 0X >= 0 + 0X
                 active h X -> mark c d X
                 0 + 0X >= 2 + 0X
                 active f f X -> mark c f g f X
                 2 + 1X >= 2 + 0X
                 active c X -> mark d X
                 1 + 0X >= 1 + 0X
                 g active X -> g X
                 1 + 1X >= 1 + 1X
                 g mark X -> g X
                 2 + 1X >= 1 + 1X
                 f active X -> f X
                 1 + 1X >= 1 + 1X
                 f mark X -> f X
                 2 + 1X >= 1 + 1X
                 c active X -> c X
                 1 + 0X >= 1 + 0X
                 c mark X -> c X
                 1 + 0X >= 1 + 0X
                 mark h X -> active h mark X
                 1 + 0X >= 0 + 0X
                 mark d X -> active d X
                 1 + 0X >= 0 + 0X
                 mark g X -> active g X
                 2 + 1X >= 1 + 1X
                 mark f X -> active f mark X
                 2 + 1X >= 2 + 1X
                 mark c X -> active c X
                 2 + 0X >= 1 + 0X
               SCCS (0):
                
                
                
 
 SCC (2):
  Strict:
   {  h# mark X -> h# X,
    h# active X -> h# X}
  Weak:
  {    mark c X -> active c X,
       mark f X -> active f mark X,
       mark g X -> active g X,
       mark d X -> active d X,
       mark h X -> active h mark X,
       c mark X -> c X,
     c active X -> c X,
       f mark X -> f X,
     f active X -> f X,
       g mark X -> g X,
     g active X -> g X,
     active c X -> mark d X,
   active f f X -> mark c f g f X,
     active h X -> mark c d X,
       d mark X -> d X,
     d active X -> d X,
       h mark X -> h X,
     h active X -> h X}
  POLY:
   Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
   Interpretation:
    [mark](x0) = x0,
    
    [c](x0) = 0,
    
    [f](x0) = 0,
    
    [g](x0) = 0,
    
    [active](x0) = x0 + 1,
    
    [d](x0) = x0 + 1,
    
    [h](x0) = 0,
    
    [h#](x0) = x0
   Strict:
    h# active X -> h# X
    1 + 1X >= 0 + 1X
    h# mark X -> h# X
    0 + 1X >= 0 + 1X
   Weak:
    h active X -> h X
    0 + 0X >= 0 + 0X
    h mark X -> h X
    0 + 0X >= 0 + 0X
    d active X -> d X
    2 + 1X >= 1 + 1X
    d mark X -> d X
    1 + 1X >= 1 + 1X
    active h X -> mark c d X
    1 + 0X >= 0 + 0X
    active f f X -> mark c f g f X
    1 + 0X >= 0 + 0X
    active c X -> mark d X
    1 + 0X >= 1 + 1X
    g active X -> g X
    0 + 0X >= 0 + 0X
    g mark X -> g X
    0 + 0X >= 0 + 0X
    f active X -> f X
    0 + 0X >= 0 + 0X
    f mark X -> f X
    0 + 0X >= 0 + 0X
    c active X -> c X
    0 + 0X >= 0 + 0X
    c mark X -> c X
    0 + 0X >= 0 + 0X
    mark h X -> active h mark X
    0 + 0X >= 1 + 0X
    mark d X -> active d X
    1 + 1X >= 2 + 1X
    mark g X -> active g X
    0 + 0X >= 1 + 0X
    mark f X -> active f mark X
    0 + 0X >= 1 + 0X
    mark c X -> active c X
    0 + 0X >= 1 + 0X
  SCCS (1):
   Scc:
    {h# mark X -> h# X}
   
   SCC (1):
    Strict:
     {h# mark X -> h# X}
    Weak:
    {    mark c X -> active c X,
         mark f X -> active f mark X,
         mark g X -> active g X,
         mark d X -> active d X,
         mark h X -> active h mark X,
         c mark X -> c X,
       c active X -> c X,
         f mark X -> f X,
       f active X -> f X,
         g mark X -> g X,
       g active X -> g X,
       active c X -> mark d X,
     active f f X -> mark c f g f X,
       active h X -> mark c d X,
         d mark X -> d X,
       d active X -> d X,
         h mark X -> h X,
       h active X -> h X}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [mark](x0) = x0 + 1,
      
      [c](x0) = x0 + 1,
      
      [f](x0) = x0 + 1,
      
      [g](x0) = x0 + 1,
      
      [active](x0) = x0,
      
      [d](x0) = 0,
      
      [h](x0) = x0 + 1,
      
      [h#](x0) = x0
     Strict:
      h# mark X -> h# X
      1 + 1X >= 0 + 1X
     Weak:
      h active X -> h X
      1 + 1X >= 1 + 1X
      h mark X -> h X
      2 + 1X >= 1 + 1X
      d active X -> d X
      0 + 0X >= 0 + 0X
      d mark X -> d X
      0 + 0X >= 0 + 0X
      active h X -> mark c d X
      1 + 1X >= 2 + 0X
      active f f X -> mark c f g f X
      2 + 1X >= 5 + 1X
      active c X -> mark d X
      1 + 1X >= 1 + 0X
      g active X -> g X
      1 + 1X >= 1 + 1X
      g mark X -> g X
      2 + 1X >= 1 + 1X
      f active X -> f X
      1 + 1X >= 1 + 1X
      f mark X -> f X
      2 + 1X >= 1 + 1X
      c active X -> c X
      1 + 1X >= 1 + 1X
      c mark X -> c X
      2 + 1X >= 1 + 1X
      mark h X -> active h mark X
      2 + 1X >= 2 + 1X
      mark d X -> active d X
      1 + 0X >= 0 + 0X
      mark g X -> active g X
      2 + 1X >= 1 + 1X
      mark f X -> active f mark X
      2 + 1X >= 2 + 1X
      mark c X -> active c X
      2 + 1X >= 1 + 1X
    Qed



SCC (2):
 Strict:
  {  g# mark X -> g# X,
   g# active X -> g# X}
 Weak:
 {    mark c X -> active c X,
      mark f X -> active f mark X,
      mark g X -> active g X,
      mark d X -> active d X,
      mark h X -> active h mark X,
      c mark X -> c X,
    c active X -> c X,
      f mark X -> f X,
    f active X -> f X,
      g mark X -> g X,
    g active X -> g X,
    active c X -> mark d X,
  active f f X -> mark c f g f X,
    active h X -> mark c d X,
      d mark X -> d X,
    d active X -> d X,
      h mark X -> h X,
    h active X -> h X}
 POLY:
  Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
  Interpretation:
   [mark](x0) = x0,
   
   [c](x0) = 0,
   
   [f](x0) = 0,
   
   [g](x0) = 0,
   
   [active](x0) = x0 + 1,
   
   [d](x0) = x0 + 1,
   
   [h](x0) = 0,
   
   [g#](x0) = x0
  Strict:
   g# active X -> g# X
   1 + 1X >= 0 + 1X
   g# mark X -> g# X
   0 + 1X >= 0 + 1X
  Weak:
   h active X -> h X
   0 + 0X >= 0 + 0X
   h mark X -> h X
   0 + 0X >= 0 + 0X
   d active X -> d X
   2 + 1X >= 1 + 1X
   d mark X -> d X
   1 + 1X >= 1 + 1X
   active h X -> mark c d X
   1 + 0X >= 0 + 0X
   active f f X -> mark c f g f X
   1 + 0X >= 0 + 0X
   active c X -> mark d X
   1 + 0X >= 1 + 1X
   g active X -> g X
   0 + 0X >= 0 + 0X
   g mark X -> g X
   0 + 0X >= 0 + 0X
   f active X -> f X
   0 + 0X >= 0 + 0X
   f mark X -> f X
   0 + 0X >= 0 + 0X
   c active X -> c X
   0 + 0X >= 0 + 0X
   c mark X -> c X
   0 + 0X >= 0 + 0X
   mark h X -> active h mark X
   0 + 0X >= 1 + 0X
   mark d X -> active d X
   1 + 1X >= 2 + 1X
   mark g X -> active g X
   0 + 0X >= 1 + 0X
   mark f X -> active f mark X
   0 + 0X >= 1 + 0X
   mark c X -> active c X
   0 + 0X >= 1 + 0X
 SCCS (1):
  Scc:
   {g# mark X -> g# X}
  
  SCC (1):
   Strict:
    {g# mark X -> g# X}
   Weak:
   {    mark c X -> active c X,
        mark f X -> active f mark X,
        mark g X -> active g X,
        mark d X -> active d X,
        mark h X -> active h mark X,
        c mark X -> c X,
      c active X -> c X,
        f mark X -> f X,
      f active X -> f X,
        g mark X -> g X,
      g active X -> g X,
      active c X -> mark d X,
    active f f X -> mark c f g f X,
      active h X -> mark c d X,
        d mark X -> d X,
      d active X -> d X,
        h mark X -> h X,
      h active X -> h X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [mark](x0) = x0 + 1,
     
     [c](x0) = x0 + 1,
     
     [f](x0) = x0 + 1,
     
     [g](x0) = x0 + 1,
     
     [active](x0) = x0,
     
     [d](x0) = 0,
     
     [h](x0) = x0 + 1,
     
     [g#](x0) = x0
    Strict:
     g# mark X -> g# X
     1 + 1X >= 0 + 1X
    Weak:
     h active X -> h X
     1 + 1X >= 1 + 1X
     h mark X -> h X
     2 + 1X >= 1 + 1X
     d active X -> d X
     0 + 0X >= 0 + 0X
     d mark X -> d X
     0 + 0X >= 0 + 0X
     active h X -> mark c d X
     1 + 1X >= 2 + 0X
     active f f X -> mark c f g f X
     2 + 1X >= 5 + 1X
     active c X -> mark d X
     1 + 1X >= 1 + 0X
     g active X -> g X
     1 + 1X >= 1 + 1X
     g mark X -> g X
     2 + 1X >= 1 + 1X
     f active X -> f X
     1 + 1X >= 1 + 1X
     f mark X -> f X
     2 + 1X >= 1 + 1X
     c active X -> c X
     1 + 1X >= 1 + 1X
     c mark X -> c X
     2 + 1X >= 1 + 1X
     mark h X -> active h mark X
     2 + 1X >= 2 + 1X
     mark d X -> active d X
     1 + 0X >= 0 + 0X
     mark g X -> active g X
     2 + 1X >= 1 + 1X
     mark f X -> active f mark X
     2 + 1X >= 2 + 1X
     mark c X -> active c X
     2 + 1X >= 1 + 1X
   Qed


SCC (2):
 Strict:
  {  c# mark X -> c# X,
   c# active X -> c# X}
 Weak:
 {    mark c X -> active c X,
      mark f X -> active f mark X,
      mark g X -> active g X,
      mark d X -> active d X,
      mark h X -> active h mark X,
      c mark X -> c X,
    c active X -> c X,
      f mark X -> f X,
    f active X -> f X,
      g mark X -> g X,
    g active X -> g X,
    active c X -> mark d X,
  active f f X -> mark c f g f X,
    active h X -> mark c d X,
      d mark X -> d X,
    d active X -> d X,
      h mark X -> h X,
    h active X -> h X}
 POLY:
  Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
  Interpretation:
   [mark](x0) = x0,
   
   [c](x0) = 0,
   
   [f](x0) = 0,
   
   [g](x0) = 0,
   
   [active](x0) = x0 + 1,
   
   [d](x0) = x0 + 1,
   
   [h](x0) = 0,
   
   [c#](x0) = x0
  Strict:
   c# active X -> c# X
   1 + 1X >= 0 + 1X
   c# mark X -> c# X
   0 + 1X >= 0 + 1X
  Weak:
   h active X -> h X
   0 + 0X >= 0 + 0X
   h mark X -> h X
   0 + 0X >= 0 + 0X
   d active X -> d X
   2 + 1X >= 1 + 1X
   d mark X -> d X
   1 + 1X >= 1 + 1X
   active h X -> mark c d X
   1 + 0X >= 0 + 0X
   active f f X -> mark c f g f X
   1 + 0X >= 0 + 0X
   active c X -> mark d X
   1 + 0X >= 1 + 1X
   g active X -> g X
   0 + 0X >= 0 + 0X
   g mark X -> g X
   0 + 0X >= 0 + 0X
   f active X -> f X
   0 + 0X >= 0 + 0X
   f mark X -> f X
   0 + 0X >= 0 + 0X
   c active X -> c X
   0 + 0X >= 0 + 0X
   c mark X -> c X
   0 + 0X >= 0 + 0X
   mark h X -> active h mark X
   0 + 0X >= 1 + 0X
   mark d X -> active d X
   1 + 1X >= 2 + 1X
   mark g X -> active g X
   0 + 0X >= 1 + 0X
   mark f X -> active f mark X
   0 + 0X >= 1 + 0X
   mark c X -> active c X
   0 + 0X >= 1 + 0X
 SCCS (1):
  Scc:
   {c# mark X -> c# X}
  
  SCC (1):
   Strict:
    {c# mark X -> c# X}
   Weak:
   {    mark c X -> active c X,
        mark f X -> active f mark X,
        mark g X -> active g X,
        mark d X -> active d X,
        mark h X -> active h mark X,
        c mark X -> c X,
      c active X -> c X,
        f mark X -> f X,
      f active X -> f X,
        g mark X -> g X,
      g active X -> g X,
      active c X -> mark d X,
    active f f X -> mark c f g f X,
      active h X -> mark c d X,
        d mark X -> d X,
      d active X -> d X,
        h mark X -> h X,
      h active X -> h X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [mark](x0) = x0 + 1,
     
     [c](x0) = x0 + 1,
     
     [f](x0) = x0 + 1,
     
     [g](x0) = x0 + 1,
     
     [active](x0) = x0,
     
     [d](x0) = 0,
     
     [h](x0) = x0 + 1,
     
     [c#](x0) = x0
    Strict:
     c# mark X -> c# X
     1 + 1X >= 0 + 1X
    Weak:
     h active X -> h X
     1 + 1X >= 1 + 1X
     h mark X -> h X
     2 + 1X >= 1 + 1X
     d active X -> d X
     0 + 0X >= 0 + 0X
     d mark X -> d X
     0 + 0X >= 0 + 0X
     active h X -> mark c d X
     1 + 1X >= 2 + 0X
     active f f X -> mark c f g f X
     2 + 1X >= 5 + 1X
     active c X -> mark d X
     1 + 1X >= 1 + 0X
     g active X -> g X
     1 + 1X >= 1 + 1X
     g mark X -> g X
     2 + 1X >= 1 + 1X
     f active X -> f X
     1 + 1X >= 1 + 1X
     f mark X -> f X
     2 + 1X >= 1 + 1X
     c active X -> c X
     1 + 1X >= 1 + 1X
     c mark X -> c X
     2 + 1X >= 1 + 1X
     mark h X -> active h mark X
     2 + 1X >= 2 + 1X
     mark d X -> active d X
     1 + 0X >= 0 + 0X
     mark g X -> active g X
     2 + 1X >= 1 + 1X
     mark f X -> active f mark X
     2 + 1X >= 2 + 1X
     mark c X -> active c X
     2 + 1X >= 1 + 1X
   Qed

SCC (2):
 Strict:
  {  f# mark X -> f# X,
   f# active X -> f# X}
 Weak:
 {    mark c X -> active c X,
      mark f X -> active f mark X,
      mark g X -> active g X,
      mark d X -> active d X,
      mark h X -> active h mark X,
      c mark X -> c X,
    c active X -> c X,
      f mark X -> f X,
    f active X -> f X,
      g mark X -> g X,
    g active X -> g X,
    active c X -> mark d X,
  active f f X -> mark c f g f X,
    active h X -> mark c d X,
      d mark X -> d X,
    d active X -> d X,
      h mark X -> h X,
    h active X -> h X}
 POLY:
  Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
  Interpretation:
   [mark](x0) = x0,
   
   [c](x0) = 0,
   
   [f](x0) = 0,
   
   [g](x0) = 0,
   
   [active](x0) = x0 + 1,
   
   [d](x0) = x0 + 1,
   
   [h](x0) = 0,
   
   [f#](x0) = x0
  Strict:
   f# active X -> f# X
   1 + 1X >= 0 + 1X
   f# mark X -> f# X
   0 + 1X >= 0 + 1X
  Weak:
   h active X -> h X
   0 + 0X >= 0 + 0X
   h mark X -> h X
   0 + 0X >= 0 + 0X
   d active X -> d X
   2 + 1X >= 1 + 1X
   d mark X -> d X
   1 + 1X >= 1 + 1X
   active h X -> mark c d X
   1 + 0X >= 0 + 0X
   active f f X -> mark c f g f X
   1 + 0X >= 0 + 0X
   active c X -> mark d X
   1 + 0X >= 1 + 1X
   g active X -> g X
   0 + 0X >= 0 + 0X
   g mark X -> g X
   0 + 0X >= 0 + 0X
   f active X -> f X
   0 + 0X >= 0 + 0X
   f mark X -> f X
   0 + 0X >= 0 + 0X
   c active X -> c X
   0 + 0X >= 0 + 0X
   c mark X -> c X
   0 + 0X >= 0 + 0X
   mark h X -> active h mark X
   0 + 0X >= 1 + 0X
   mark d X -> active d X
   1 + 1X >= 2 + 1X
   mark g X -> active g X
   0 + 0X >= 1 + 0X
   mark f X -> active f mark X
   0 + 0X >= 1 + 0X
   mark c X -> active c X
   0 + 0X >= 1 + 0X
 SCCS (1):
  Scc:
   {f# mark X -> f# X}
  
  SCC (1):
   Strict:
    {f# mark X -> f# X}
   Weak:
   {    mark c X -> active c X,
        mark f X -> active f mark X,
        mark g X -> active g X,
        mark d X -> active d X,
        mark h X -> active h mark X,
        c mark X -> c X,
      c active X -> c X,
        f mark X -> f X,
      f active X -> f X,
        g mark X -> g X,
      g active X -> g X,
      active c X -> mark d X,
    active f f X -> mark c f g f X,
      active h X -> mark c d X,
        d mark X -> d X,
      d active X -> d X,
        h mark X -> h X,
      h active X -> h X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [mark](x0) = x0 + 1,
     
     [c](x0) = x0 + 1,
     
     [f](x0) = x0 + 1,
     
     [g](x0) = x0 + 1,
     
     [active](x0) = x0,
     
     [d](x0) = 0,
     
     [h](x0) = x0 + 1,
     
     [f#](x0) = x0
    Strict:
     f# mark X -> f# X
     1 + 1X >= 0 + 1X
    Weak:
     h active X -> h X
     1 + 1X >= 1 + 1X
     h mark X -> h X
     2 + 1X >= 1 + 1X
     d active X -> d X
     0 + 0X >= 0 + 0X
     d mark X -> d X
     0 + 0X >= 0 + 0X
     active h X -> mark c d X
     1 + 1X >= 2 + 0X
     active f f X -> mark c f g f X
     2 + 1X >= 5 + 1X
     active c X -> mark d X
     1 + 1X >= 1 + 0X
     g active X -> g X
     1 + 1X >= 1 + 1X
     g mark X -> g X
     2 + 1X >= 1 + 1X
     f active X -> f X
     1 + 1X >= 1 + 1X
     f mark X -> f X
     2 + 1X >= 1 + 1X
     c active X -> c X
     1 + 1X >= 1 + 1X
     c mark X -> c X
     2 + 1X >= 1 + 1X
     mark h X -> active h mark X
     2 + 1X >= 2 + 1X
     mark d X -> active d X
     1 + 0X >= 0 + 0X
     mark g X -> active g X
     2 + 1X >= 1 + 1X
     mark f X -> active f mark X
     2 + 1X >= 2 + 1X
     mark c X -> active c X
     2 + 1X >= 1 + 1X
   Qed