MAYBE
Time: 30.504876
TRS:
 {    f(X1, X2, mark 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, X2, active X3),
   active f(a(), b(), X) -> mark f(X, X, X),
              active c() -> mark a(),
              active c() -> mark b(),
    proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
              proper a() -> ok a(),
              proper b() -> ok b(),
              proper c() -> ok c(),
              top mark X -> top proper X,
                top ok X -> top active X}
 DP:
  DP:
   {    f#(X1, X2, mark X3) -> f#(X1, X2, X3),
    f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3),
      active# f(X1, X2, X3) -> f#(X1, X2, active X3),
      active# f(X1, X2, X3) -> active# X3,
     active# f(a(), b(), X) -> f#(X, X, 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, X2, mark 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, X2, active X3),
    active f(a(), b(), X) -> mark f(X, X, X),
               active c() -> mark a(),
               active c() -> mark b(),
     proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
               proper a() -> ok a(),
               proper b() -> ok b(),
               proper c() -> ok c(),
               top mark X -> top proper X,
                 top ok X -> top active X}
  UR:
   {    f(X1, X2, mark 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, X2, active X3),
     active f(a(), b(), X) -> mark f(X, X, X),
                active c() -> mark a(),
                active c() -> mark b(),
      proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                proper a() -> ok a(),
                proper b() -> ok b(),
                proper c() -> ok c(),
                   d(x, y) -> x,
                   d(x, y) -> y}
   EDG:
    {(active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (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))
     (active# f(X1, X2, X3) -> active# X3, active# f(a(), b(), X) -> f#(X, X, X))
     (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> active# X3)
     (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
     (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, mark 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# 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)
     (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(X1, X2, mark 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))
     (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)
     (top# ok X -> active# X, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
     (top# ok X -> active# X, active# f(X1, X2, X3) -> active# X3)
     (top# ok X -> active# X, active# f(a(), b(), X) -> f#(X, X, X))
     (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(X1, X2, mark 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))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))}
    STATUS:
     arrows: 0.763314
     SCCS (4):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {active# f(X1, X2, X3) -> active# X3}
      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, X2, mark 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, X2, mark 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, X2, active X3),
         active f(a(), b(), X) -> mark f(X, X, X),
                    active c() -> mark a(),
                    active c() -> mark b(),
          proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                    proper a() -> ok a(),
                    proper b() -> ok b(),
                    proper c() -> ok c(),
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {active# f(X1, X2, X3) -> active# X3}
       Weak:
       {    f(X1, X2, mark 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, X2, active X3),
         active f(a(), b(), X) -> mark f(X, X, X),
                    active c() -> mark a(),
                    active c() -> mark b(),
          proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                    proper a() -> ok a(),
                    proper b() -> ok b(),
                    proper c() -> ok c(),
                    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, X2, mark 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, X2, active X3),
         active f(a(), b(), X) -> mark f(X, X, X),
                    active c() -> mark a(),
                    active c() -> mark b(),
          proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                    proper a() -> ok a(),
                    proper b() -> ok b(),
                    proper c() -> ok c(),
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open
      
      
      
      SCC (2):
       Strict:
        {    f#(X1, X2, mark X3) -> f#(X1, X2, X3),
         f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)}
       Weak:
       {    f(X1, X2, mark 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, X2, active X3),
         active f(a(), b(), X) -> mark f(X, X, X),
                    active c() -> mark a(),
                    active c() -> mark b(),
          proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                    proper a() -> ok a(),
                    proper b() -> ok b(),
                    proper c() -> ok c(),
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open