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