MAYBE
TRS:
 {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
               mark(c()) -> active(c()),
               mark(b()) -> active(b()),
     f(X1, X2, mark(X3)) -> f(X1, X2, X3),
   f(X1, X2, active(X3)) -> f(X1, X2, X3),
     f(X1, mark(X2), X3) -> f(X1, X2, X3),
   f(X1, active(X2), X3) -> f(X1, X2, X3),
     f(mark(X1), X2, X3) -> f(X1, X2, X3),
   f(active(X1), X2, X3) -> f(X1, X2, X3),
  active(f(b(), X, c())) -> mark(f(X, c(), X)),
             active(c()) -> mark(b())}
 DP:
  Strict:
   {   mark#(f(X1, X2, X3)) -> mark#(X2),
       mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3),
       mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)),
                 mark#(c()) -> active#(c()),
                 mark#(b()) -> active#(b()),
       f#(X1, X2, mark(X3)) -> f#(X1, X2, X3),
     f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
       f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
     f#(X1, active(X2), X3) -> f#(X1, X2, X3),
       f#(mark(X1), X2, X3) -> f#(X1, X2, X3),
     f#(active(X1), X2, X3) -> f#(X1, X2, X3),
    active#(f(b(), X, c())) -> mark#(f(X, c(), X)),
    active#(f(b(), X, c())) -> f#(X, c(), X),
               active#(c()) -> mark#(b())}
  Weak:
  {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                mark(c()) -> active(c()),
                mark(b()) -> active(b()),
      f(X1, X2, mark(X3)) -> f(X1, X2, X3),
    f(X1, X2, active(X3)) -> f(X1, X2, X3),
      f(X1, mark(X2), X3) -> f(X1, X2, X3),
    f(X1, active(X2), X3) -> f(X1, X2, X3),
      f(mark(X1), X2, X3) -> f(X1, X2, X3),
    f(active(X1), X2, X3) -> f(X1, X2, X3),
   active(f(b(), X, c())) -> mark(f(X, c(), X)),
              active(c()) -> mark(b())}
  EDG:
   {(active#(f(b(), X, c())) -> mark#(f(X, c(), X)), mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)))
    (active#(f(b(), X, c())) -> mark#(f(X, c(), X)), mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3))
    (active#(f(b(), X, c())) -> mark#(f(X, c(), X)), mark#(f(X1, X2, X3)) -> mark#(X2))
    (mark#(c()) -> active#(c()), active#(c()) -> mark#(b()))
    (active#(c()) -> mark#(b()), mark#(b()) -> active#(b()))
    (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(active(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
    (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
    (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
    (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
    (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(active(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
    (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
    (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
    (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
    (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(active(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
    (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
    (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
    (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
    (active#(f(b(), X, c())) -> f#(X, c(), X), f#(active(X1), X2, X3) -> f#(X1, X2, X3))
    (active#(f(b(), X, c())) -> f#(X, c(), X), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
    (active#(f(b(), X, c())) -> f#(X, c(), X), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
    (active#(f(b(), X, c())) -> f#(X, c(), X), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
    (f#(active(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
    (f#(active(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
    (f#(active(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
    (f#(active(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
    (f#(active(X1), X2, X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(active(X1), X2, X3) -> f#(X1, X2, X3), f#(active(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
    (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
    (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
    (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
    (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(active(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
    (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
    (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
    (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
    (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
    (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(active(X1), X2, X3) -> f#(X1, X2, X3))
    (mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
    (mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
    (mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
    (mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
    (mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
    (mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3), f#(active(X1), X2, X3) -> f#(X1, X2, X3))
    (mark#(f(X1, X2, X3)) -> mark#(X2), mark#(f(X1, X2, X3)) -> mark#(X2))
    (mark#(f(X1, X2, X3)) -> mark#(X2), mark#(f(X1, X2, X3)) -> f#(X1, mark(X2), X3))
    (mark#(f(X1, X2, X3)) -> mark#(X2), mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)))
    (mark#(f(X1, X2, X3)) -> mark#(X2), mark#(c()) -> active#(c()))
    (mark#(f(X1, X2, X3)) -> mark#(X2), mark#(b()) -> active#(b()))
    (mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)), active#(f(b(), X, c())) -> mark#(f(X, c(), X)))
    (mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)), active#(f(b(), X, c())) -> f#(X, c(), X))}
   SCCS:
    Scc:
     {  f#(X1, X2, mark(X3)) -> f#(X1, X2, X3),
      f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
        f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
      f#(X1, active(X2), X3) -> f#(X1, X2, X3),
        f#(mark(X1), X2, X3) -> f#(X1, X2, X3),
      f#(active(X1), X2, X3) -> f#(X1, X2, X3)}
    Scc:
     {   mark#(f(X1, X2, X3)) -> mark#(X2),
         mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)),
      active#(f(b(), X, c())) -> mark#(f(X, c(), X))}
    SCC:
     Strict:
      {  f#(X1, X2, mark(X3)) -> f#(X1, X2, X3),
       f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
         f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
       f#(X1, active(X2), X3) -> f#(X1, X2, X3),
         f#(mark(X1), X2, X3) -> f#(X1, X2, X3),
       f#(active(X1), X2, X3) -> f#(X1, X2, X3)}
     Weak:
     {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                   mark(c()) -> active(c()),
                   mark(b()) -> active(b()),
         f(X1, X2, mark(X3)) -> f(X1, X2, X3),
       f(X1, X2, active(X3)) -> f(X1, X2, X3),
         f(X1, mark(X2), X3) -> f(X1, X2, X3),
       f(X1, active(X2), X3) -> f(X1, X2, X3),
         f(mark(X1), X2, X3) -> f(X1, X2, X3),
       f(active(X1), X2, X3) -> f(X1, X2, X3),
      active(f(b(), X, c())) -> mark(f(X, c(), X)),
                 active(c()) -> mark(b())}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {  f#(X1, X2, mark(X3)) -> f#(X1, X2, X3),
        f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
          f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
        f#(X1, active(X2), X3) -> f#(X1, X2, X3),
          f#(mark(X1), X2, X3) -> f#(X1, X2, X3)}
      EDG:
       {(f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
        (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
        (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
        (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
        (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
        (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
        (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
        (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
        (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
        (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
        (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
        (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
        (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
        (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
        (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
        (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
        (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
        (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
        (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
        (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
        (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(X1, X2, mark(X3)) -> f#(X1, X2, X3))
        (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
        (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
        (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
        (f#(X1, X2, mark(X3)) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))}
       SCCS:
        Scc:
         {  f#(X1, X2, mark(X3)) -> f#(X1, X2, X3),
          f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
            f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
          f#(X1, active(X2), X3) -> f#(X1, X2, X3),
            f#(mark(X1), X2, X3) -> f#(X1, X2, X3)}
        SCC:
         Strict:
          {  f#(X1, X2, mark(X3)) -> f#(X1, X2, X3),
           f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
             f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
           f#(X1, active(X2), X3) -> f#(X1, X2, X3),
             f#(mark(X1), X2, X3) -> f#(X1, X2, X3)}
         Weak:
         {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                       mark(c()) -> active(c()),
                       mark(b()) -> active(b()),
             f(X1, X2, mark(X3)) -> f(X1, X2, X3),
           f(X1, X2, active(X3)) -> f(X1, X2, X3),
             f(X1, mark(X2), X3) -> f(X1, X2, X3),
           f(X1, active(X2), X3) -> f(X1, X2, X3),
             f(mark(X1), X2, X3) -> f(X1, X2, X3),
           f(active(X1), X2, X3) -> f(X1, X2, X3),
          active(f(b(), X, c())) -> mark(f(X, c(), X)),
                     active(c()) -> mark(b())}
         SPSC:
          Simple Projection:
           pi(f#) = 2
          Strict:
           {f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
              f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
            f#(X1, active(X2), X3) -> f#(X1, X2, X3),
              f#(mark(X1), X2, X3) -> f#(X1, X2, X3)}
          EDG:
           {(f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
            (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
            (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
            (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
            (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
            (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
            (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
            (f#(mark(X1), X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
            (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
            (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
            (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
            (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))
            (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
            (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
            (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
            (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(mark(X1), X2, X3) -> f#(X1, X2, X3))}
           SCCS:
            Scc:
             {f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
                f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
              f#(X1, active(X2), X3) -> f#(X1, X2, X3),
                f#(mark(X1), X2, X3) -> f#(X1, X2, X3)}
            SCC:
             Strict:
              {f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
                 f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
               f#(X1, active(X2), X3) -> f#(X1, X2, X3),
                 f#(mark(X1), X2, X3) -> f#(X1, X2, X3)}
             Weak:
             {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                           mark(c()) -> active(c()),
                           mark(b()) -> active(b()),
                 f(X1, X2, mark(X3)) -> f(X1, X2, X3),
               f(X1, X2, active(X3)) -> f(X1, X2, X3),
                 f(X1, mark(X2), X3) -> f(X1, X2, X3),
               f(X1, active(X2), X3) -> f(X1, X2, X3),
                 f(mark(X1), X2, X3) -> f(X1, X2, X3),
               f(active(X1), X2, X3) -> f(X1, X2, X3),
              active(f(b(), X, c())) -> mark(f(X, c(), X)),
                         active(c()) -> mark(b())}
             SPSC:
              Simple Projection:
               pi(f#) = 0
              Strict:
               {f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
                  f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
                f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
              EDG:
               {(f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
                (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
                (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
                (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
                (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
                (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
                (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, X2, active(X3)) -> f#(X1, X2, X3))
                (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
                (f#(X1, X2, active(X3)) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))}
               SCCS:
                Scc:
                 {f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
                    f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
                  f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
                SCC:
                 Strict:
                  {f#(X1, X2, active(X3)) -> f#(X1, X2, X3),
                     f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
                   f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
                 Weak:
                 {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                               mark(c()) -> active(c()),
                               mark(b()) -> active(b()),
                     f(X1, X2, mark(X3)) -> f(X1, X2, X3),
                   f(X1, X2, active(X3)) -> f(X1, X2, X3),
                     f(X1, mark(X2), X3) -> f(X1, X2, X3),
                   f(X1, active(X2), X3) -> f(X1, X2, X3),
                     f(mark(X1), X2, X3) -> f(X1, X2, X3),
                   f(active(X1), X2, X3) -> f(X1, X2, X3),
                  active(f(b(), X, c())) -> mark(f(X, c(), X)),
                             active(c()) -> mark(b())}
                 SPSC:
                  Simple Projection:
                   pi(f#) = 2
                  Strict:
                   {  f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
                    f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
                  EDG:
                   {(f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))
                    (f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
                    (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
                    (f#(X1, mark(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))}
                   SCCS:
                    Scc:
                     {  f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
                      f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
                    SCC:
                     Strict:
                      {  f#(X1, mark(X2), X3) -> f#(X1, X2, X3),
                       f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
                     Weak:
                     {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                                   mark(c()) -> active(c()),
                                   mark(b()) -> active(b()),
                         f(X1, X2, mark(X3)) -> f(X1, X2, X3),
                       f(X1, X2, active(X3)) -> f(X1, X2, X3),
                         f(X1, mark(X2), X3) -> f(X1, X2, X3),
                       f(X1, active(X2), X3) -> f(X1, X2, X3),
                         f(mark(X1), X2, X3) -> f(X1, X2, X3),
                       f(active(X1), X2, X3) -> f(X1, X2, X3),
                      active(f(b(), X, c())) -> mark(f(X, c(), X)),
                                 active(c()) -> mark(b())}
                     SPSC:
                      Simple Projection:
                       pi(f#) = 1
                      Strict:
                       {f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
                      EDG:
                       {(f#(X1, active(X2), X3) -> f#(X1, X2, X3), f#(X1, active(X2), X3) -> f#(X1, X2, X3))}
                       SCCS:
                        Scc:
                         {f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
                        SCC:
                         Strict:
                          {f#(X1, active(X2), X3) -> f#(X1, X2, X3)}
                         Weak:
                         {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                                       mark(c()) -> active(c()),
                                       mark(b()) -> active(b()),
                             f(X1, X2, mark(X3)) -> f(X1, X2, X3),
                           f(X1, X2, active(X3)) -> f(X1, X2, X3),
                             f(X1, mark(X2), X3) -> f(X1, X2, X3),
                           f(X1, active(X2), X3) -> f(X1, X2, X3),
                             f(mark(X1), X2, X3) -> f(X1, X2, X3),
                           f(active(X1), X2, X3) -> f(X1, X2, X3),
                          active(f(b(), X, c())) -> mark(f(X, c(), X)),
                                     active(c()) -> mark(b())}
                         SPSC:
                          Simple Projection:
                           pi(f#) = 1
                          Strict:
                           {}
                          Qed
    SCC:
     Strict:
      {   mark#(f(X1, X2, X3)) -> mark#(X2),
          mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)),
       active#(f(b(), X, c())) -> mark#(f(X, c(), X))}
     Weak:
     {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                   mark(c()) -> active(c()),
                   mark(b()) -> active(b()),
         f(X1, X2, mark(X3)) -> f(X1, X2, X3),
       f(X1, X2, active(X3)) -> f(X1, X2, X3),
         f(X1, mark(X2), X3) -> f(X1, X2, X3),
       f(X1, active(X2), X3) -> f(X1, X2, X3),
         f(mark(X1), X2, X3) -> f(X1, X2, X3),
       f(active(X1), X2, X3) -> f(X1, X2, X3),
      active(f(b(), X, c())) -> mark(f(X, c(), X)),
                 active(c()) -> mark(b())}
     POLY:
      Argument Filtering:
       pi(b) = [], pi(active#) = 0, pi(active) = 0, pi(c) = [], pi(f) = [0,1], pi(mark#) = 0, pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [f](x0, x1) = x0 + x1 + 1,
       [b] = 1,
       [c] = 1
      Strict:
       {   mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)),
        active#(f(b(), X, c())) -> mark#(f(X, c(), X))}
      Weak:
       {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                     mark(c()) -> active(c()),
                     mark(b()) -> active(b()),
           f(X1, X2, mark(X3)) -> f(X1, X2, X3),
         f(X1, X2, active(X3)) -> f(X1, X2, X3),
           f(X1, mark(X2), X3) -> f(X1, X2, X3),
         f(X1, active(X2), X3) -> f(X1, X2, X3),
           f(mark(X1), X2, X3) -> f(X1, X2, X3),
         f(active(X1), X2, X3) -> f(X1, X2, X3),
        active(f(b(), X, c())) -> mark(f(X, c(), X)),
                   active(c()) -> mark(b())}
      EDG:
       {(active#(f(b(), X, c())) -> mark#(f(X, c(), X)), mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)))
        (mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)), active#(f(b(), X, c())) -> mark#(f(X, c(), X)))}
       SCCS:
        Scc:
         {   mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)),
          active#(f(b(), X, c())) -> mark#(f(X, c(), X))}
        SCC:
         Strict:
          {   mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3)),
           active#(f(b(), X, c())) -> mark#(f(X, c(), X))}
         Weak:
         {   mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3)),
                       mark(c()) -> active(c()),
                       mark(b()) -> active(b()),
             f(X1, X2, mark(X3)) -> f(X1, X2, X3),
           f(X1, X2, active(X3)) -> f(X1, X2, X3),
             f(X1, mark(X2), X3) -> f(X1, X2, X3),
           f(X1, active(X2), X3) -> f(X1, X2, X3),
             f(mark(X1), X2, X3) -> f(X1, X2, X3),
           f(active(X1), X2, X3) -> f(X1, X2, X3),
          active(f(b(), X, c())) -> mark(f(X, c(), X)),
                     active(c()) -> mark(b())}
         Fail