YES(?,O(n^1))
TRS:
 {
      f mark X -> f X,
    f active X -> f X,
      g mark X -> g X,
    g active X -> g X,
      mark f X -> active f X,
      mark g X -> active g X,
      mark c() -> active c(),
  active f g X -> mark g X,
    active c() -> mark f g c()
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
        f mark X -> f X,
      f active X -> f X,
        g mark X -> g X,
      g active X -> g X,
        mark f X -> active f X,
        mark g X -> active g X,
        mark c() -> active c(),
    active f g X -> mark g X,
      active c() -> mark f g c()
   }
  RLAB:
   Strict:
    {
       f(mark) mark(f) X -> f(f) X,
       f(mark) mark(f) f(f) X -> f(active) active(f) f(f) X,
       f(mark) mark(f) f(mark) X -> f(active) active(f) f(mark) X,
       f(mark) mark(f) f(g) X -> f(active) active(f) f(g) X,
       f(mark) mark(f) f(c) X -> f(active) active(f) f(c) X,
       f(mark) mark(f) f(active) X -> f(active) active(f) f(active) X,
       f(mark) mark(mark) X -> f(mark) X,
       f(mark) mark(g) X -> f(g) X,
       f(mark) mark(g) g(f) X -> f(active) active(g) g(f) X,
       f(mark) mark(g) g(mark) X -> f(active) active(g) g(mark) X,
       f(mark) mark(g) g(g) X -> f(active) active(g) g(g) X,
       f(mark) mark(g) g(c) X -> f(active) active(g) g(c) X,
       f(mark) mark(g) g(active) X -> f(active) active(g) g(active) X,
       f(mark) mark(c) X -> f(c) X,
     f(mark) mark(c) c() -> f(active) active(c) c(),
       f(mark) mark(active) X -> f(active) X,
       f(active) active(f) X -> f(f) X,
       f(active) active(f) f(g) g(f) X -> f(mark) mark(g) g(f) X,
       f(active) active(f) f(g) g(mark) X -> f(mark) mark(g) g(mark) X,
       f(active) active(f) f(g) g(g) X -> f(mark) mark(g) g(g) X,
       f(active) active(f) f(g) g(c) X -> f(mark) mark(g) g(c) X,
       f(active) active(f) f(g) g(active) X -> f(mark) mark(g) g(active) X,
       f(active) active(mark) X -> f(mark) X,
       f(active) active(g) X -> f(g) X,
       f(active) active(c) X -> f(c) X,
     f(active) active(c) c() -> f(mark) mark(f) f(g) g(c) c(),
       f(active) active(active) X -> f(active) X,
       g(mark) mark(f) X -> g(f) X,
       g(mark) mark(f) f(f) X -> g(active) active(f) f(f) X,
       g(mark) mark(f) f(mark) X -> g(active) active(f) f(mark) X,
       g(mark) mark(f) f(g) X -> g(active) active(f) f(g) X,
       g(mark) mark(f) f(c) X -> g(active) active(f) f(c) X,
       g(mark) mark(f) f(active) X -> g(active) active(f) f(active) X,
       g(mark) mark(mark) X -> g(mark) X,
       g(mark) mark(g) X -> g(g) X,
       g(mark) mark(g) g(f) X -> g(active) active(g) g(f) X,
       g(mark) mark(g) g(mark) X -> g(active) active(g) g(mark) X,
       g(mark) mark(g) g(g) X -> g(active) active(g) g(g) X,
       g(mark) mark(g) g(c) X -> g(active) active(g) g(c) X,
       g(mark) mark(g) g(active) X -> g(active) active(g) g(active) X,
       g(mark) mark(c) X -> g(c) X,
     g(mark) mark(c) c() -> g(active) active(c) c(),
       g(mark) mark(active) X -> g(active) X,
       g(active) active(f) X -> g(f) X,
       g(active) active(f) f(g) g(f) X -> g(mark) mark(g) g(f) X,
       g(active) active(f) f(g) g(mark) X -> g(mark) mark(g) g(mark) X,
       g(active) active(f) f(g) g(g) X -> g(mark) mark(g) g(g) X,
       g(active) active(f) f(g) g(c) X -> g(mark) mark(g) g(c) X,
       g(active) active(f) f(g) g(active) X -> g(mark) mark(g) g(active) X,
       g(active) active(mark) X -> g(mark) X,
       g(active) active(g) X -> g(g) X,
       g(active) active(c) X -> g(c) X,
     g(active) active(c) c() -> g(mark) mark(f) f(g) g(c) c(),
       g(active) active(active) X -> g(active) X,
       mark(mark) mark(f) f(f) X -> mark(active) active(f) f(f) X,
       mark(mark) mark(f) f(mark) X -> mark(active) active(f) f(mark) X,
       mark(mark) mark(f) f(g) X -> mark(active) active(f) f(g) X,
       mark(mark) mark(f) f(c) X -> mark(active) active(f) f(c) X,
       mark(mark) mark(f) f(active) X -> mark(active) active(f) f(active) X,
       mark(mark) mark(g) g(f) X -> mark(active) active(g) g(f) X,
       mark(mark) mark(g) g(mark) X -> mark(active) active(g) g(mark) X,
       mark(mark) mark(g) g(g) X -> mark(active) active(g) g(g) X,
       mark(mark) mark(g) g(c) X -> mark(active) active(g) g(c) X,
       mark(mark) mark(g) g(active) X -> mark(active) active(g) g(active) X,
     mark(mark) mark(c) c() -> mark(active) active(c) c(),
       mark(active) active(f) f(g) g(f) X -> mark(mark) mark(g) g(f) X,
       mark(active) active(f) f(g) g(mark) X -> mark(mark) mark(g) g(mark) X,
       mark(active) active(f) f(g) g(g) X -> mark(mark) mark(g) g(g) X,
       mark(active) active(f) f(g) g(c) X -> mark(mark) mark(g) g(c) X,
       mark(active) active(f) f(g) g(active) X ->
     mark(mark) mark(g) g(active) X,
     mark(active) active(c) c() -> mark(mark) mark(f) f(g) g(c) c(),
       active(mark) mark(f) f(f) X -> active(active) active(f) f(f) X,
       active(mark) mark(f) f(mark) X -> active(active) active(f) f(mark) X,
       active(mark) mark(f) f(g) X -> active(active) active(f) f(g) X,
       active(mark) mark(f) f(c) X -> active(active) active(f) f(c) X,
       active(mark) mark(f) f(active) X ->
     active(active) active(f) f(active) X,
       active(mark) mark(g) g(f) X -> active(active) active(g) g(f) X,
       active(mark) mark(g) g(mark) X -> active(active) active(g) g(mark) X,
       active(mark) mark(g) g(g) X -> active(active) active(g) g(g) X,
       active(mark) mark(g) g(c) X -> active(active) active(g) g(c) X,
       active(mark) mark(g) g(active) X ->
     active(active) active(g) g(active) X,
     active(mark) mark(c) c() -> active(active) active(c) c(),
       active(active) active(f) f(g) g(f) X -> active(mark) mark(g) g(f) X,
       active(active) active(f) f(g) g(mark) X ->
     active(mark) mark(g) g(mark) X,
       active(active) active(f) f(g) g(g) X -> active(mark) mark(g) g(g) X,
       active(active) active(f) f(g) g(c) X -> active(mark) mark(g) g(c) X,
       active(active) active(f) f(g) g(active) X ->
     active(mark) mark(g) g(active) X,
     active(active) active(c) c() -> active(mark) mark(f) f(g) g(c) c()
    }
   Weak:
    {}
   Natural interpretation:
    Strict:
     {
        f(mark) mark(f) X -> f(f) X,
        f(mark) mark(f) f(f) X -> f(active) active(f) f(f) X,
        f(mark) mark(f) f(mark) X -> f(active) active(f) f(mark) X,
        f(mark) mark(f) f(g) X -> f(active) active(f) f(g) X,
        f(mark) mark(f) f(c) X -> f(active) active(f) f(c) X,
        f(mark) mark(f) f(active) X -> f(active) active(f) f(active) X,
        f(mark) mark(mark) X -> f(mark) X,
        f(mark) mark(g) X -> f(g) X,
        f(mark) mark(g) g(f) X -> f(active) active(g) g(f) X,
        f(mark) mark(g) g(mark) X -> f(active) active(g) g(mark) X,
        f(mark) mark(g) g(g) X -> f(active) active(g) g(g) X,
        f(mark) mark(g) g(c) X -> f(active) active(g) g(c) X,
        f(mark) mark(g) g(active) X -> f(active) active(g) g(active) X,
        f(mark) mark(c) X -> f(c) X,
      f(mark) mark(c) c() -> f(active) active(c) c(),
        f(mark) mark(active) X -> f(active) X,
        f(active) active(f) X -> f(f) X,
        f(active) active(f) f(g) g(f) X -> f(mark) mark(g) g(f) X,
        f(active) active(f) f(g) g(mark) X -> f(mark) mark(g) g(mark) X,
        f(active) active(f) f(g) g(g) X -> f(mark) mark(g) g(g) X,
        f(active) active(f) f(g) g(c) X -> f(mark) mark(g) g(c) X,
        f(active) active(f) f(g) g(active) X -> f(mark) mark(g) g(active) X,
        f(active) active(mark) X -> f(mark) X,
        f(active) active(g) X -> f(g) X,
        f(active) active(c) X -> f(c) X,
      f(active) active(c) c() -> f(mark) mark(f) f(g) g(c) c(),
        f(active) active(active) X -> f(active) X,
        g(mark) mark(f) X -> g(f) X,
        g(mark) mark(f) f(f) X -> g(active) active(f) f(f) X,
        g(mark) mark(f) f(mark) X -> g(active) active(f) f(mark) X,
        g(mark) mark(f) f(g) X -> g(active) active(f) f(g) X,
        g(mark) mark(f) f(c) X -> g(active) active(f) f(c) X,
        g(mark) mark(f) f(active) X -> g(active) active(f) f(active) X,
        g(mark) mark(mark) X -> g(mark) X,
        g(mark) mark(g) X -> g(g) X,
        g(mark) mark(g) g(f) X -> g(active) active(g) g(f) X,
        g(mark) mark(g) g(mark) X -> g(active) active(g) g(mark) X,
        g(mark) mark(g) g(g) X -> g(active) active(g) g(g) X,
        g(mark) mark(g) g(c) X -> g(active) active(g) g(c) X,
        g(mark) mark(g) g(active) X -> g(active) active(g) g(active) X,
        g(mark) mark(c) X -> g(c) X,
      g(mark) mark(c) c() -> g(active) active(c) c(),
        g(mark) mark(active) X -> g(active) X,
        g(active) active(f) X -> g(f) X,
        g(active) active(f) f(g) g(f) X -> g(mark) mark(g) g(f) X,
        g(active) active(f) f(g) g(mark) X -> g(mark) mark(g) g(mark) X,
        g(active) active(f) f(g) g(g) X -> g(mark) mark(g) g(g) X,
        g(active) active(f) f(g) g(c) X -> g(mark) mark(g) g(c) X,
        g(active) active(f) f(g) g(active) X -> g(mark) mark(g) g(active) X,
        g(active) active(mark) X -> g(mark) X,
        g(active) active(g) X -> g(g) X,
        g(active) active(c) X -> g(c) X,
      g(active) active(c) c() -> g(mark) mark(f) f(g) g(c) c(),
        g(active) active(active) X -> g(active) X,
        mark(mark) mark(f) f(f) X -> mark(active) active(f) f(f) X,
        mark(mark) mark(f) f(mark) X -> mark(active) active(f) f(mark) X,
        mark(mark) mark(f) f(g) X -> mark(active) active(f) f(g) X,
        mark(mark) mark(f) f(c) X -> mark(active) active(f) f(c) X,
        mark(mark) mark(f) f(active) X -> mark(active) active(f) f(active) X,
        mark(mark) mark(g) g(f) X -> mark(active) active(g) g(f) X,
        mark(mark) mark(g) g(mark) X -> mark(active) active(g) g(mark) X,
        mark(mark) mark(g) g(g) X -> mark(active) active(g) g(g) X,
        mark(mark) mark(g) g(c) X -> mark(active) active(g) g(c) X,
        mark(mark) mark(g) g(active) X -> mark(active) active(g) g(active) X,
      mark(mark) mark(c) c() -> mark(active) active(c) c(),
        mark(active) active(f) f(g) g(f) X -> mark(mark) mark(g) g(f) X,
        mark(active) active(f) f(g) g(mark) X -> mark(mark) mark(g) g(mark) X,
        mark(active) active(f) f(g) g(g) X -> mark(mark) mark(g) g(g) X,
        mark(active) active(f) f(g) g(c) X -> mark(mark) mark(g) g(c) X,
        mark(active) active(f) f(g) g(active) X ->
      mark(mark) mark(g) g(active) X,
      mark(active) active(c) c() -> mark(mark) mark(f) f(g) g(c) c(),
        active(mark) mark(f) f(f) X -> active(active) active(f) f(f) X,
        active(mark) mark(f) f(mark) X -> active(active) active(f) f(mark) X,
        active(mark) mark(f) f(g) X -> active(active) active(f) f(g) X,
        active(mark) mark(f) f(c) X -> active(active) active(f) f(c) X,
        active(mark) mark(f) f(active) X ->
      active(active) active(f) f(active) X,
        active(mark) mark(g) g(f) X -> active(active) active(g) g(f) X,
        active(mark) mark(g) g(mark) X -> active(active) active(g) g(mark) X,
        active(mark) mark(g) g(g) X -> active(active) active(g) g(g) X,
        active(mark) mark(g) g(c) X -> active(active) active(g) g(c) X,
        active(mark) mark(g) g(active) X ->
      active(active) active(g) g(active) X,
      active(mark) mark(c) c() -> active(active) active(c) c(),
        active(active) active(f) f(g) g(f) X -> active(mark) mark(g) g(f) X,
        active(active) active(f) f(g) g(mark) X ->
      active(mark) mark(g) g(mark) X,
        active(active) active(f) f(g) g(g) X -> active(mark) mark(g) g(g) X,
        active(active) active(f) f(g) g(c) X -> active(mark) mark(g) g(c) X,
        active(active) active(f) f(g) g(active) X ->
      active(mark) mark(g) g(active) X,
      active(active) active(c) c() -> active(mark) mark(f) f(g) g(c) c()
     }
    Weak:
     {}
    Interpretation class: stronglylinear
    [active(4)](X0) = + 1*X0 + 1
    [active(3)](X0) = + 1*X0 + 7
    [active(2)](X0) = + 1*X0 + 2
    [active(1)](X0) = + 1*X0 + 2
    [active(0)](X0) = + 1*X0 + 0
    [c] = + 4
    [mark(4)](X0) = + 1*X0 + 6
    [mark(3)](X0) = + 1*X0 + 7
    [mark(2)](X0) = + 1*X0 + 2
    [mark(1)](X0) = + 1*X0 + 7
    [mark(0)](X0) = + 1*X0 + 0
    [g(4)](X0) = + 1*X0 + 6
    [g(3)](X0) = + 1*X0 + 1
    [g(2)](X0) = + 1*X0 + 0
    [g(1)](X0) = + 1*X0 + 7
    [g(0)](X0) = + 1*X0 + 2
    [f(4)](X0) = + 1*X0 + 3
    [f(3)](X0) = + 1*X0 + 0
    [f(2)](X0) = + 1*X0 + 4
    [f(1)](X0) = + 1*X0 + 4
    [f(0)](X0) = + 1*X0 + 0
    
    Qed