YES
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:
  Strict:
   {     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)}
  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)}
  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))
    (active#(h(X)) -> d#(X), d#(active(X)) -> d#(X))
    (active#(h(X)) -> d#(X), d#(mark(X)) -> d#(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))
    (active#(c(X)) -> d#(X), d#(mark(X)) -> d#(X))
    (active#(c(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))}
   SCCS:
    Scc:
     {  h#(mark(X)) -> h#(X),
      h#(active(X)) -> h#(X)}
    Scc:
     {  d#(mark(X)) -> d#(X),
      d#(active(X)) -> d#(X)}
    Scc:
     {  g#(mark(X)) -> g#(X),
      g#(active(X)) -> g#(X)}
    Scc:
     {  f#(mark(X)) -> f#(X),
      f#(active(X)) -> f#(X)}
    Scc:
     {  c#(mark(X)) -> c#(X),
      c#(active(X)) -> c#(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:
     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)}
     SPSC:
      Simple Projection:
       pi(h#) = 0
      Strict:
       {h#(active(X)) -> h#(X)}
      EDG:
       {(h#(active(X)) -> h#(X), h#(active(X)) -> h#(X))}
       SCCS:
        Scc:
         {h#(active(X)) -> h#(X)}
        SCC:
         Strict:
          {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)}
         SPSC:
          Simple Projection:
           pi(h#) = 0
          Strict:
           {}
          Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(d#) = 0
      Strict:
       {d#(active(X)) -> d#(X)}
      EDG:
       {(d#(active(X)) -> d#(X), d#(active(X)) -> d#(X))}
       SCCS:
        Scc:
         {d#(active(X)) -> d#(X)}
        SCC:
         Strict:
          {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)}
         SPSC:
          Simple Projection:
           pi(d#) = 0
          Strict:
           {}
          Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {g#(active(X)) -> g#(X)}
      EDG:
       {(g#(active(X)) -> g#(X), g#(active(X)) -> g#(X))}
       SCCS:
        Scc:
         {g#(active(X)) -> g#(X)}
        SCC:
         Strict:
          {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)}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {}
          Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(active(X)) -> f#(X)}
      EDG:
       {(f#(active(X)) -> f#(X), f#(active(X)) -> f#(X))}
       SCCS:
        Scc:
         {f#(active(X)) -> f#(X)}
        SCC:
         Strict:
          {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)}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(c#) = 0
      Strict:
       {c#(active(X)) -> c#(X)}
      EDG:
       {(c#(active(X)) -> c#(X), c#(active(X)) -> c#(X))}
       SCCS:
        Scc:
         {c#(active(X)) -> c#(X)}
        SCC:
         Strict:
          {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)}
         SPSC:
          Simple Projection:
           pi(c#) = 0
          Strict:
           {}
          Qed
    SCC:
     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:
      Argument Filtering:
       pi(h) = 0, pi(d) = [], pi(active#) = [], pi(active) = [], pi(g) = [], pi(f) = [0], pi(c) = [], pi(mark#) = 0, pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [active#] = 0,
       [d] = 0,
       [g] = 0,
       [f](x0) = x0 + 1,
       [c] = 0
      Strict:
       {     mark#(c(X)) -> active#(c(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)}
      EDG:
       {(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#(c(X)) -> active#(c(X)))
        (mark#(g(X)) -> active#(g(X)), active#(h(X)) -> mark#(c(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#(c(X)) -> mark#(d(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#(c(X)) -> active#(c(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)) -> mark#(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#(g(X)) -> active#(g(X)))
        (active#(f(f(X))) -> mark#(c(f(g(f(X))))), mark#(c(X)) -> active#(c(X)))
        (mark#(h(X)) -> mark#(X), mark#(c(X)) -> active#(c(X)))
        (mark#(h(X)) -> mark#(X), mark#(g(X)) -> active#(g(X)))
        (mark#(h(X)) -> mark#(X), mark#(d(X)) -> active#(d(X)))
        (mark#(h(X)) -> mark#(X), mark#(h(X)) -> mark#(X))
        (mark#(h(X)) -> mark#(X), mark#(h(X)) -> active#(h(mark(X))))
        (mark#(d(X)) -> active#(d(X)), active#(c(X)) -> mark#(d(X)))
        (mark#(d(X)) -> active#(d(X)), active#(f(f(X))) -> mark#(c(f(g(f(X))))))
        (mark#(d(X)) -> active#(d(X)), active#(h(X)) -> mark#(c(d(X))))
        (mark#(c(X)) -> active#(c(X)), active#(c(X)) -> mark#(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#(h(X)) -> mark#(c(d(X))))
        (mark#(h(X)) -> active#(h(mark(X))), active#(c(X)) -> mark#(d(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#(h(X)) -> mark#(c(d(X))))}
       SCCS:
        Scc:
         {     mark#(c(X)) -> active#(c(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:
         Strict:
          {     mark#(c(X)) -> active#(c(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:
          Argument Filtering:
           pi(h) = [], pi(d) = [], pi(active#) = 0, pi(active) = [], pi(g) = [], pi(f) = [], pi(c) = [], pi(mark#) = [], pi(mark) = []
          Usable Rules:
           {}
          Interpretation:
           [mark#] = 0,
           [h] = 0,
           [d] = 0,
           [g] = 0,
           [f] = 1,
           [c] = 0
          Strict:
           {  mark#(c(X)) -> active#(c(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)}
          EDG:
           {(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#(c(X)) -> active#(c(X)))
            (mark#(c(X)) -> active#(c(X)), active#(h(X)) -> mark#(c(d(X))))
            (mark#(c(X)) -> active#(c(X)), active#(c(X)) -> mark#(d(X)))
            (mark#(d(X)) -> active#(d(X)), active#(h(X)) -> mark#(c(d(X))))
            (mark#(d(X)) -> active#(d(X)), active#(c(X)) -> mark#(d(X)))
            (active#(c(X)) -> mark#(d(X)), mark#(c(X)) -> active#(c(X)))
            (active#(c(X)) -> mark#(d(X)), mark#(g(X)) -> active#(g(X)))
            (active#(c(X)) -> mark#(d(X)), mark#(d(X)) -> active#(d(X)))
            (active#(c(X)) -> mark#(d(X)), mark#(h(X)) -> mark#(X))
            (active#(c(X)) -> mark#(d(X)), mark#(h(X)) -> active#(h(mark(X))))
            (mark#(g(X)) -> active#(g(X)), active#(c(X)) -> mark#(d(X)))
            (mark#(g(X)) -> active#(g(X)), active#(h(X)) -> mark#(c(d(X))))
            (mark#(h(X)) -> mark#(X), mark#(c(X)) -> active#(c(X)))
            (mark#(h(X)) -> mark#(X), mark#(g(X)) -> active#(g(X)))
            (mark#(h(X)) -> mark#(X), mark#(d(X)) -> active#(d(X)))
            (mark#(h(X)) -> mark#(X), mark#(h(X)) -> mark#(X))
            (mark#(h(X)) -> mark#(X), mark#(h(X)) -> active#(h(mark(X))))
            (mark#(h(X)) -> active#(h(mark(X))), active#(c(X)) -> mark#(d(X)))
            (mark#(h(X)) -> active#(h(mark(X))), active#(h(X)) -> mark#(c(d(X))))}
           SCCS:
            Scc:
             {  mark#(c(X)) -> active#(c(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:
             Strict:
              {  mark#(c(X)) -> active#(c(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:
              Argument Filtering:
               pi(h) = [0], pi(d) = [], pi(active#) = [], pi(active) = [], pi(g) = [0], pi(f) = [], pi(c) = [], pi(mark#) = [0], pi(mark) = []
              Usable Rules:
               {}
              Interpretation:
               [active#] = 1,
               [mark#](x0) = x0 + 1,
               [h](x0) = x0 + 1,
               [d] = 0,
               [g](x0) = x0 + 1,
               [c] = 0
              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)}
              EDG:
               {(mark#(c(X)) -> active#(c(X)), active#(h(X)) -> mark#(c(d(X))))
                (mark#(c(X)) -> active#(c(X)), active#(c(X)) -> mark#(d(X)))
                (active#(c(X)) -> mark#(d(X)), mark#(d(X)) -> active#(d(X)))
                (active#(c(X)) -> mark#(d(X)), mark#(c(X)) -> active#(c(X)))
                (mark#(d(X)) -> active#(d(X)), active#(c(X)) -> mark#(d(X)))
                (mark#(d(X)) -> active#(d(X)), active#(h(X)) -> mark#(c(d(X))))
                (active#(h(X)) -> mark#(c(d(X))), mark#(c(X)) -> active#(c(X)))
                (active#(h(X)) -> mark#(c(d(X))), mark#(d(X)) -> active#(d(X)))}
               SCCS:
                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:
                 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:
                  Argument Filtering:
                   pi(h) = [], pi(d) = [], pi(active#) = 0, pi(active) = [], pi(g) = [], pi(f) = [], pi(c) = [], pi(mark#) = [], pi(mark) = []
                  Usable Rules:
                   {}
                  Interpretation:
                   [mark#] = 1,
                   [h] = 1,
                   [d] = 0,
                   [c] = 1
                  Strict:
                   {  mark#(c(X)) -> active#(c(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)}
                  EDG:
                   {(mark#(c(X)) -> active#(c(X)), active#(h(X)) -> mark#(c(d(X))))
                    (mark#(c(X)) -> active#(c(X)), active#(c(X)) -> mark#(d(X)))
                    (active#(c(X)) -> mark#(d(X)), mark#(c(X)) -> active#(c(X)))
                    (active#(h(X)) -> mark#(c(d(X))), mark#(c(X)) -> active#(c(X)))}
                   SCCS:
                    Scc:
                     {  mark#(c(X)) -> active#(c(X)),
                      active#(c(X)) -> mark#(d(X)),
                      active#(h(X)) -> mark#(c(d(X)))}
                    SCC:
                     Strict:
                      {  mark#(c(X)) -> active#(c(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:
                      Argument Filtering:
                       pi(h) = [], pi(d) = [], pi(active#) = 0, pi(active) = [], pi(g) = [], pi(f) = [], pi(c) = [], pi(mark#) = [], pi(mark) = []
                      Usable Rules:
                       {}
                      Interpretation:
                       [mark#] = 0,
                       [h] = 1,
                       [c] = 0
                      Strict:
                       {  mark#(c(X)) -> active#(c(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)}
                      EDG:
                       {(active#(c(X)) -> mark#(d(X)), mark#(c(X)) -> active#(c(X)))
                        (mark#(c(X)) -> active#(c(X)), active#(c(X)) -> mark#(d(X)))}
                       SCCS:
                        Scc:
                         {  mark#(c(X)) -> active#(c(X)),
                          active#(c(X)) -> mark#(d(X))}
                        SCC:
                         Strict:
                          {  mark#(c(X)) -> active#(c(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:
                          Argument Filtering:
                           pi(h) = [], pi(d) = [], pi(active#) = [], pi(active) = [], pi(g) = [], pi(f) = [], pi(c) = [], pi(mark#) = 0, pi(mark) = []
                          Usable Rules:
                           {}
                          Interpretation:
                           [active#] = 0,
                           [d] = 0,
                           [c] = 1
                          Strict:
                           {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)}
                          EDG:
                           {}
                           SCCS:
                            
                            Qed