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