MAYBE
TRS:
 {  f(mark(X1), X2) -> mark(f(X1, X2)),
  f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
    active(f(X, X)) -> mark(f(a(), b())),
  active(f(X1, X2)) -> f(active(X1), X2),
        active(b()) -> mark(a()),
  proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
        proper(a()) -> ok(a()),
        proper(b()) -> ok(b()),
       top(mark(X)) -> top(proper(X)),
         top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {  f#(mark(X1), X2) -> f#(X1, X2),
    f#(ok(X1), ok(X2)) -> f#(X1, X2),
      active#(f(X, X)) -> f#(a(), b()),
    active#(f(X1, X2)) -> f#(active(X1), X2),
    active#(f(X1, X2)) -> active#(X1),
    proper#(f(X1, X2)) -> f#(proper(X1), proper(X2)),
    proper#(f(X1, X2)) -> proper#(X1),
    proper#(f(X1, X2)) -> proper#(X2),
         top#(mark(X)) -> proper#(X),
         top#(mark(X)) -> top#(proper(X)),
           top#(ok(X)) -> active#(X),
           top#(ok(X)) -> top#(active(X))}
  Weak:
  {  f(mark(X1), X2) -> mark(f(X1, X2)),
   f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
     active(f(X, X)) -> mark(f(a(), b())),
   active(f(X1, X2)) -> f(active(X1), X2),
         active(b()) -> mark(a()),
   proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
         proper(a()) -> ok(a()),
         proper(b()) -> ok(b()),
        top(mark(X)) -> top(proper(X)),
          top(ok(X)) -> top(active(X))}
  EDG:
   {(top#(ok(X)) -> active#(X), active#(f(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(f(X1, X2)) -> f#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(f(X, X)) -> f#(a(), b()))
    (f#(mark(X1), X2) -> f#(X1, X2), f#(ok(X1), ok(X2)) -> f#(X1, X2))
    (f#(mark(X1), X2) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
    (proper#(f(X1, X2)) -> proper#(X2), proper#(f(X1, X2)) -> proper#(X2))
    (proper#(f(X1, X2)) -> proper#(X2), proper#(f(X1, X2)) -> proper#(X1))
    (proper#(f(X1, X2)) -> proper#(X2), proper#(f(X1, X2)) -> f#(proper(X1), proper(X2)))
    (active#(f(X1, X2)) -> f#(active(X1), X2), f#(ok(X1), ok(X2)) -> f#(X1, X2))
    (active#(f(X1, X2)) -> f#(active(X1), X2), f#(mark(X1), X2) -> f#(X1, X2))
    (proper#(f(X1, X2)) -> proper#(X1), proper#(f(X1, X2)) -> proper#(X2))
    (proper#(f(X1, X2)) -> proper#(X1), proper#(f(X1, X2)) -> proper#(X1))
    (proper#(f(X1, X2)) -> proper#(X1), proper#(f(X1, X2)) -> f#(proper(X1), proper(X2)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
    (active#(f(X1, X2)) -> active#(X1), active#(f(X, X)) -> f#(a(), b()))
    (active#(f(X1, X2)) -> active#(X1), active#(f(X1, X2)) -> f#(active(X1), X2))
    (active#(f(X1, X2)) -> active#(X1), active#(f(X1, X2)) -> active#(X1))
    (f#(ok(X1), ok(X2)) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
    (f#(ok(X1), ok(X2)) -> f#(X1, X2), f#(ok(X1), ok(X2)) -> f#(X1, X2))
    (proper#(f(X1, X2)) -> f#(proper(X1), proper(X2)), f#(mark(X1), X2) -> f#(X1, X2))
    (proper#(f(X1, X2)) -> f#(proper(X1), proper(X2)), f#(ok(X1), ok(X2)) -> f#(X1, X2))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2)) -> f#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2)) -> proper#(X2))}
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {proper#(f(X1, X2)) -> proper#(X1),
      proper#(f(X1, X2)) -> proper#(X2)}
    Scc:
     {active#(f(X1, X2)) -> active#(X1)}
    Scc:
     {  f#(mark(X1), X2) -> f#(X1, X2),
      f#(ok(X1), ok(X2)) -> f#(X1, X2)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {  f(mark(X1), X2) -> mark(f(X1, X2)),
      f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
        active(f(X, X)) -> mark(f(a(), b())),
      active(f(X1, X2)) -> f(active(X1), X2),
            active(b()) -> mark(a()),
      proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
            proper(a()) -> ok(a()),
            proper(b()) -> ok(b()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     Fail
    SCC:
     Strict:
      {proper#(f(X1, X2)) -> proper#(X1),
       proper#(f(X1, X2)) -> proper#(X2)}
     Weak:
     {  f(mark(X1), X2) -> mark(f(X1, X2)),
      f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
        active(f(X, X)) -> mark(f(a(), b())),
      active(f(X1, X2)) -> f(active(X1), X2),
            active(b()) -> mark(a()),
      proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
            proper(a()) -> ok(a()),
            proper(b()) -> ok(b()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {proper#(f(X1, X2)) -> proper#(X2)}
      EDG:
       {(proper#(f(X1, X2)) -> proper#(X2), proper#(f(X1, X2)) -> proper#(X2))}
       SCCS:
        Scc:
         {proper#(f(X1, X2)) -> proper#(X2)}
        SCC:
         Strict:
          {proper#(f(X1, X2)) -> proper#(X2)}
         Weak:
         {  f(mark(X1), X2) -> mark(f(X1, X2)),
          f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
            active(f(X, X)) -> mark(f(a(), b())),
          active(f(X1, X2)) -> f(active(X1), X2),
                active(b()) -> mark(a()),
          proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
                proper(a()) -> ok(a()),
                proper(b()) -> ok(b()),
               top(mark(X)) -> top(proper(X)),
                 top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {active#(f(X1, X2)) -> active#(X1)}
     Weak:
     {  f(mark(X1), X2) -> mark(f(X1, X2)),
      f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
        active(f(X, X)) -> mark(f(a(), b())),
      active(f(X1, X2)) -> f(active(X1), X2),
            active(b()) -> mark(a()),
      proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
            proper(a()) -> ok(a()),
            proper(b()) -> ok(b()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {  f#(mark(X1), X2) -> f#(X1, X2),
       f#(ok(X1), ok(X2)) -> f#(X1, X2)}
     Weak:
     {  f(mark(X1), X2) -> mark(f(X1, X2)),
      f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
        active(f(X, X)) -> mark(f(a(), b())),
      active(f(X1, X2)) -> f(active(X1), X2),
            active(b()) -> mark(a()),
      proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
            proper(a()) -> ok(a()),
            proper(b()) -> ok(b()),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(mark(X1), X2) -> f#(X1, X2)}
      EDG:
       {(f#(mark(X1), X2) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))}
       SCCS:
        Scc:
         {f#(mark(X1), X2) -> f#(X1, X2)}
        SCC:
         Strict:
          {f#(mark(X1), X2) -> f#(X1, X2)}
         Weak:
         {  f(mark(X1), X2) -> mark(f(X1, X2)),
          f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
            active(f(X, X)) -> mark(f(a(), b())),
          active(f(X1, X2)) -> f(active(X1), X2),
                active(b()) -> mark(a()),
          proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
                proper(a()) -> ok(a()),
                proper(b()) -> ok(b()),
               top(mark(X)) -> top(proper(X)),
                 top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed