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