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(b(), X, c())) -> mark(f(X, c(), X)),
                active(c()) -> mark(b()),
      proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                proper(c()) -> ok(c()),
                proper(b()) -> ok(b()),
               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(b(), X, c())) -> f#(X, c(), X),
        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(b(), X, c())) -> mark(f(X, c(), X)),
                 active(c()) -> mark(b()),
       proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                 proper(c()) -> ok(c()),
                 proper(b()) -> ok(b()),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))}
  EDG:
   {(top#(mark(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X3))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), 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#(X3))
    (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#(X1))
    (proper#(f(X1, X2, X3)) -> proper#(X1), proper#(f(X1, X2, X3)) -> f#(proper(X1), proper(X2), proper(X3)))
    (f#(X1, mark(X2), 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), f#(X1, mark(X2), X3) -> f#(X1, X2, X3))
    (active#(f(X1, X2, X3)) -> active#(X2), active#(f(b(), X, c())) -> f#(X, c(), X))
    (active#(f(X1, X2, X3)) -> active#(X2), active#(f(X1, X2, X3)) -> active#(X2))
    (active#(f(X1, X2, X3)) -> active#(X2), active#(f(X1, X2, X3)) -> f#(X1, active(X2), 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))
    (proper#(f(X1, X2, X3)) -> proper#(X2), proper#(f(X1, X2, X3)) -> f#(proper(X1), proper(X2), proper(X3)))
    (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)) -> proper#(X2))
    (proper#(f(X1, X2, X3)) -> proper#(X2), proper#(f(X1, X2, X3)) -> proper#(X3))
    (f#(ok(X1), ok(X2), ok(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), 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))
    (active#(f(X1, X2, X3)) -> f#(X1, active(X2), X3), f#(ok(X1), ok(X2), ok(X3)) -> f#(X1, X2, X3))
    (top#(ok(X)) -> active#(X), active#(f(X1, X2, X3)) -> f#(X1, active(X2), X3))
    (top#(ok(X)) -> active#(X), active#(f(X1, X2, X3)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(f(b(), X, c())) -> f#(X, c(), X))
    (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(b(), X, c())) -> mark(f(X, c(), X)),
                    active(c()) -> mark(b()),
          proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                    proper(c()) -> ok(c()),
                    proper(b()) -> ok(b()),
                   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(b(), X, c())) -> mark(f(X, c(), X)),
                    active(c()) -> mark(b()),
          proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                    proper(c()) -> ok(c()),
                    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, 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(b(), X, c())) -> mark(f(X, c(), X)),
                        active(c()) -> mark(b()),
              proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                        proper(c()) -> ok(c()),
                        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, 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(b(), X, c())) -> mark(f(X, c(), X)),
                            active(c()) -> mark(b()),
                  proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                            proper(c()) -> ok(c()),
                            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, 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(b(), X, c())) -> mark(f(X, c(), X)),
                    active(c()) -> mark(b()),
          proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                    proper(c()) -> ok(c()),
                    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#(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(b(), X, c())) -> mark(f(X, c(), X)),
                    active(c()) -> mark(b()),
          proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                    proper(c()) -> ok(c()),
                    proper(b()) -> ok(b()),
                   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(b(), X, c())) -> mark(f(X, c(), X)),
                        active(c()) -> mark(b()),
              proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)),
                        proper(c()) -> ok(c()),
                        proper(b()) -> ok(b()),
                       top(mark(X)) -> top(proper(X)),
                         top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed