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