MAYBE
Time: 3.217390
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:
  DP:
   {    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}
  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}
  EDG:
   {(proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (top# ok X -> active# X, active# f(b(), X, c()) -> f#(X, c(), X))
    (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) -> 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))
    (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# X2)
    (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) -> 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))
    (top# mark X -> top# proper X, top# ok X -> top# active X)
    (top# mark X -> top# proper X, top# ok X -> active# X)
    (top# ok X -> top# active X, top# mark X -> proper# X)
    (top# ok X -> top# active X, top# mark X -> top# proper X)
    (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))
    (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)
    (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)}
   STATUS:
    arrows: 0.810651
    SCCS (4):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      {active# f(X1, X2, X3) -> active# X2}
     Scc:
      {proper# f(X1, X2, X3) -> proper# X1,
       proper# f(X1, X2, X3) -> proper# X2,
       proper# f(X1, X2, X3) -> proper# X3}
     Scc:
      {    f#(X1, mark X2, X3) -> f#(X1, X2, X3),
       f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)}
     
     SCC (2):
      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}
      Open
     
     SCC (1):
      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}
      Open
     
     
     SCC (3):
      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}
      Open
     
     SCC (2):
      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}
      Open