MAYBE
Time: 0.040803
TRS:
 {  f(mark X1, X2) -> mark f(X1, X2),
   f(ok X1, ok X2) -> ok f(X1, X2),
    active f(X, X) -> mark f(a(), b()),
  active f(X1, X2) -> f(active X1, X2),
        active b() -> mark a(),
  proper f(X1, X2) -> f(proper X1, proper X2),
        proper a() -> ok a(),
        proper b() -> ok b(),
        top mark X -> top proper X,
          top ok X -> top active X}
 DP:
  DP:
   {  f#(mark X1, X2) -> f#(X1, X2),
     f#(ok X1, ok X2) -> f#(X1, X2),
      active# f(X, X) -> f#(a(), b()),
    active# f(X1, X2) -> f#(active X1, X2),
    active# f(X1, X2) -> active# X1,
    proper# f(X1, X2) -> f#(proper X1, proper X2),
    proper# f(X1, X2) -> proper# X1,
    proper# f(X1, X2) -> proper# X2,
          top# mark X -> proper# X,
          top# mark X -> top# proper X,
            top# ok X -> active# X,
            top# ok X -> top# active X}
  TRS:
  {  f(mark X1, X2) -> mark f(X1, X2),
    f(ok X1, ok X2) -> ok f(X1, X2),
     active f(X, X) -> mark f(a(), b()),
   active f(X1, X2) -> f(active X1, X2),
         active b() -> mark a(),
   proper f(X1, X2) -> f(proper X1, proper X2),
         proper a() -> ok a(),
         proper b() -> ok b(),
         top mark X -> top proper X,
           top ok X -> top active X}
  EDG:
   {(proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X2)
    (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X1)
    (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> f#(proper X1, proper X2))
    (active# f(X1, X2) -> active# X1, active# f(X1, X2) -> active# X1)
    (active# f(X1, X2) -> active# X1, active# f(X1, X2) -> f#(active X1, X2))
    (active# f(X1, X2) -> active# X1, active# f(X, X) -> f#(a(), b()))
    (f#(mark X1, X2) -> f#(X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
    (f#(mark X1, X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
    (active# f(X1, X2) -> f#(active X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
    (active# f(X1, X2) -> f#(active X1, X2), f#(mark X1, X2) -> f#(X1, X2))
    (top# ok X -> active# X, active# f(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# f(X1, X2) -> f#(active X1, X2))
    (top# ok X -> active# X, active# f(X, X) -> f#(a(), b()))
    (top# ok X -> top# active X, top# ok X -> top# active X)
    (top# ok X -> top# active X, top# ok X -> active# X)
    (top# ok X -> top# active X, top# mark X -> top# proper X)
    (top# ok X -> top# active X, top# mark X -> proper# X)
    (top# mark X -> top# proper X, top# mark X -> proper# X)
    (top# mark X -> top# proper X, top# mark X -> top# proper X)
    (top# mark X -> top# proper X, top# ok X -> active# X)
    (top# mark X -> top# proper X, top# ok X -> top# active X)
    (top# mark X -> proper# X, proper# f(X1, X2) -> f#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# f(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# f(X1, X2) -> proper# X2)
    (f#(ok X1, ok X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
    (f#(ok X1, ok X2) -> f#(X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
    (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> f#(proper X1, proper X2))
    (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X1)
    (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X2)
    (active# f(X, X) -> f#(a(), b()), f#(mark X1, X2) -> f#(X1, X2))
    (active# f(X, X) -> f#(a(), b()), f#(ok X1, ok X2) -> f#(X1, X2))
    (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(mark X1, X2) -> f#(X1, X2))
    (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(ok X1, ok X2) -> f#(X1, X2))}
   EDG:
    {(proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X2)
     (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X1)
     (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (active# f(X1, X2) -> active# X1, active# f(X1, X2) -> active# X1)
     (active# f(X1, X2) -> active# X1, active# f(X1, X2) -> f#(active X1, X2))
     (active# f(X1, X2) -> active# X1, active# f(X, X) -> f#(a(), b()))
     (f#(mark X1, X2) -> f#(X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (active# f(X1, X2) -> f#(active X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (active# f(X1, X2) -> f#(active X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (top# ok X -> active# X, active# f(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# f(X1, X2) -> f#(active X1, X2))
     (top# ok X -> active# X, active# f(X, X) -> f#(a(), b()))
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (top# mark X -> proper# X, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# f(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# f(X1, X2) -> proper# X2)
     (f#(ok X1, ok X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (f#(ok X1, ok X2) -> f#(X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X1)
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X2)
     (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(mark X1, X2) -> f#(X1, X2))
     (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(ok X1, ok X2) -> f#(X1, X2))}
    EDG:
     {(active# f(X1, X2) -> f#(active X1, X2), f#(mark X1, X2) -> f#(X1, X2))
      (top# ok X -> top# active X, top# ok X -> top# active X)
      (top# ok X -> top# active X, top# ok X -> active# X)
      (top# ok X -> top# active X, top# mark X -> top# proper X)
      (top# ok X -> top# active X, top# mark X -> proper# X)
      (top# mark X -> top# proper X, top# mark X -> proper# X)
      (top# mark X -> top# proper X, top# mark X -> top# proper X)
      (top# mark X -> top# proper X, top# ok X -> active# X)
      (top# mark X -> top# proper X, top# ok X -> top# active X)
      (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(ok X1, ok X2) -> f#(X1, X2))}
     EDG:
      {(active# f(X1, X2) -> f#(active X1, X2), f#(mark X1, X2) -> f#(X1, X2))
       (top# ok X -> top# active X, top# mark X -> top# proper X)
       (top# ok X -> top# active X, top# mark X -> proper# X)
       (top# mark X -> top# proper X, top# ok X -> active# X)
       (top# mark X -> top# proper X, top# ok X -> top# active X)
       (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(ok X1, ok X2) -> f#(X1, X2))}
      STATUS:
       arrows: 0.958333
       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(mark X1, X2) -> mark f(X1, X2),
           f(ok X1, ok X2) -> ok f(X1, X2),
            active f(X, X) -> mark f(a(), b()),
          active f(X1, X2) -> f(active X1, X2),
                active b() -> mark a(),
          proper f(X1, X2) -> f(proper X1, proper X2),
                proper a() -> ok a(),
                proper b() -> ok b(),
                top mark X -> top proper X,
                  top ok X -> top active X}
         Fail