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