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