YES
TRS:
 {     mark(f(X)) -> active(f(X)),
       mark(g(X)) -> active(g(X)),
        mark(c()) -> active(c()),
       f(mark(X)) -> f(X),
     f(active(X)) -> f(X),
       g(mark(X)) -> g(X),
     g(active(X)) -> g(X),
  active(f(g(X))) -> mark(g(X)),
      active(c()) -> mark(f(g(c())))}
 DP:
  Strict:
   {     mark#(f(X)) -> active#(f(X)),
         mark#(g(X)) -> active#(g(X)),
          mark#(c()) -> active#(c()),
         f#(mark(X)) -> f#(X),
       f#(active(X)) -> f#(X),
         g#(mark(X)) -> g#(X),
       g#(active(X)) -> g#(X),
    active#(f(g(X))) -> mark#(g(X)),
        active#(c()) -> mark#(f(g(c()))),
        active#(c()) -> f#(g(c())),
        active#(c()) -> g#(c())}
  Weak:
  {     mark(f(X)) -> active(f(X)),
        mark(g(X)) -> active(g(X)),
         mark(c()) -> active(c()),
        f(mark(X)) -> f(X),
      f(active(X)) -> f(X),
        g(mark(X)) -> g(X),
      g(active(X)) -> g(X),
   active(f(g(X))) -> mark(g(X)),
       active(c()) -> mark(f(g(c())))}
  EDG:
   {(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))
    (mark#(c()) -> active#(c()), active#(c()) -> g#(c()))
    (mark#(c()) -> active#(c()), active#(c()) -> f#(g(c())))
    (mark#(c()) -> active#(c()), active#(c()) -> mark#(f(g(c()))))
    (mark#(g(X)) -> active#(g(X)), active#(f(g(X))) -> mark#(g(X)))
    (active#(f(g(X))) -> mark#(g(X)), mark#(f(X)) -> active#(f(X)))
    (active#(f(g(X))) -> mark#(g(X)), mark#(g(X)) -> active#(g(X)))
    (mark#(f(X)) -> active#(f(X)), active#(f(g(X))) -> mark#(g(X)))
    (active#(c()) -> mark#(f(g(c()))), mark#(f(X)) -> active#(f(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))}
   SCCS:
    Scc:
     {  g#(mark(X)) -> g#(X),
      g#(active(X)) -> g#(X)}
    Scc:
     {  f#(mark(X)) -> f#(X),
      f#(active(X)) -> f#(X)}
    Scc:
     {     mark#(f(X)) -> active#(f(X)),
           mark#(g(X)) -> active#(g(X)),
      active#(f(g(X))) -> mark#(g(X))}
    SCC:
     Strict:
      {  g#(mark(X)) -> g#(X),
       g#(active(X)) -> g#(X)}
     Weak:
     {     mark(f(X)) -> active(f(X)),
           mark(g(X)) -> active(g(X)),
            mark(c()) -> active(c()),
           f(mark(X)) -> f(X),
         f(active(X)) -> f(X),
           g(mark(X)) -> g(X),
         g(active(X)) -> g(X),
      active(f(g(X))) -> mark(g(X)),
          active(c()) -> mark(f(g(c())))}
     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(f(X)) -> active(f(X)),
               mark(g(X)) -> active(g(X)),
                mark(c()) -> active(c()),
               f(mark(X)) -> f(X),
             f(active(X)) -> f(X),
               g(mark(X)) -> g(X),
             g(active(X)) -> g(X),
          active(f(g(X))) -> mark(g(X)),
              active(c()) -> mark(f(g(c())))}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  f#(mark(X)) -> f#(X),
       f#(active(X)) -> f#(X)}
     Weak:
     {     mark(f(X)) -> active(f(X)),
           mark(g(X)) -> active(g(X)),
            mark(c()) -> active(c()),
           f(mark(X)) -> f(X),
         f(active(X)) -> f(X),
           g(mark(X)) -> g(X),
         g(active(X)) -> g(X),
      active(f(g(X))) -> mark(g(X)),
          active(c()) -> mark(f(g(c())))}
     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(f(X)) -> active(f(X)),
               mark(g(X)) -> active(g(X)),
                mark(c()) -> active(c()),
               f(mark(X)) -> f(X),
             f(active(X)) -> f(X),
               g(mark(X)) -> g(X),
             g(active(X)) -> g(X),
          active(f(g(X))) -> mark(g(X)),
              active(c()) -> mark(f(g(c())))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {     mark#(f(X)) -> active#(f(X)),
            mark#(g(X)) -> active#(g(X)),
       active#(f(g(X))) -> mark#(g(X))}
     Weak:
     {     mark(f(X)) -> active(f(X)),
           mark(g(X)) -> active(g(X)),
            mark(c()) -> active(c()),
           f(mark(X)) -> f(X),
         f(active(X)) -> f(X),
           g(mark(X)) -> g(X),
         g(active(X)) -> g(X),
      active(f(g(X))) -> mark(g(X)),
          active(c()) -> mark(f(g(c())))}
     SPSC:
      Simple Projection:
       pi(active#) = 0, pi(mark#) = 0
      Strict:
       {mark#(f(X)) -> active#(f(X)),
        mark#(g(X)) -> active#(g(X))}
      EDG:
       {}
       SCCS:
        
        Qed