MAYBE
Time: 0.075447
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:
  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(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}
  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}
  EDG:
   {(proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3))
    (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) -> active# X2, active# f(a(), X, X) -> f#(X, b(), b()))
    (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# 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, 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))
    (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)}
   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# 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)
     (active# f(X1, X2, X3) -> f#(X1, active X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3))}
    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# 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)
      (active# f(X1, X2, X3) -> f#(X1, active X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3))}
     STATUS:
      arrows: 0.964497
      SCCS (1):
       Scc:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       
       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(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}
        Open