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