MAYBE
Time: 0.033234
TRS:
 {      f mark X -> mark f X,
          f ok X -> ok f X,
          g ok X -> ok g X,
      active f X -> f active X,
  active f f a() -> mark f g f a(),
      proper f X -> f proper X,
      proper g X -> g proper X,
      proper a() -> ok a(),
      top mark X -> top proper X,
        top ok X -> top active X}
 DP:
  DP:
   {      f# mark X -> f# X,
            f# ok X -> f# X,
            g# ok X -> g# X,
        active# f X -> f# active X,
        active# f X -> active# X,
    active# f f a() -> f# g f a(),
    active# f f a() -> g# f a(),
        proper# f X -> f# proper X,
        proper# f X -> proper# X,
        proper# g X -> g# proper X,
        proper# g X -> proper# X,
        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 X -> mark f X,
           f ok X -> ok f X,
           g ok X -> ok g X,
       active f X -> f active X,
   active f f a() -> mark f g f a(),
       proper f X -> f proper X,
       proper g X -> g proper X,
       proper a() -> ok a(),
       top mark X -> top proper X,
         top ok X -> top active X}
  UR:
   {      f mark X -> mark f X,
            f ok X -> ok f X,
            g ok X -> ok g X,
        active f X -> f active X,
    active f f a() -> mark f g f a(),
        proper f X -> f proper X,
        proper g X -> g proper X,
        proper a() -> ok a()}
   EDG:
    {(active# f f a() -> g# f a(), g# ok X -> g# X)
     (proper# f X -> f# proper X, f# ok X -> f# X)
     (proper# f X -> f# proper X, f# mark X -> f# X)
     (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)
     (f# mark X -> f# X, f# ok X -> f# X)
     (f# mark X -> f# X, f# mark X -> f# X)
     (g# ok X -> g# X, g# ok X -> g# X)
     (proper# f X -> proper# X, proper# g X -> proper# X)
     (proper# f X -> proper# X, proper# g X -> g# proper X)
     (proper# f X -> proper# X, proper# f X -> proper# X)
     (proper# f X -> proper# X, proper# f X -> f# proper X)
     (top# mark X -> proper# X, proper# g X -> proper# X)
     (top# mark X -> proper# X, proper# g X -> g# proper X)
     (top# mark X -> proper# X, proper# f X -> proper# X)
     (top# mark X -> proper# X, proper# f X -> f# proper X)
     (top# ok X -> active# X, active# f X -> f# active X)
     (top# ok X -> active# X, active# f X -> active# X)
     (top# ok X -> active# X, active# f f a() -> f# g f a())
     (top# ok X -> active# X, active# f f a() -> g# f a())
     (proper# g X -> proper# X, proper# f X -> f# proper X)
     (proper# g X -> proper# X, proper# f X -> proper# X)
     (proper# g X -> proper# X, proper# g X -> g# proper X)
     (proper# g X -> proper# X, proper# g X -> proper# X)
     (active# f X -> active# X, active# f X -> f# active X)
     (active# f X -> active# X, active# f X -> active# X)
     (active# f X -> active# X, active# f f a() -> f# g f a())
     (active# f X -> active# X, active# f f a() -> g# f a())
     (f# ok X -> f# X, f# mark X -> f# X)
     (f# ok X -> f# X, f# ok X -> f# 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# g X -> g# proper X, g# ok X -> g# X)
     (active# f X -> f# active X, f# mark X -> f# X)
     (active# f X -> f# active X, f# ok X -> f# X)
     (active# f f a() -> f# g f a(), f# mark X -> f# X)
     (active# f f a() -> f# g f a(), f# ok X -> f# X)}
    EDG:
     {(proper# f X -> f# proper X, f# ok X -> f# X)
      (proper# f X -> f# proper X, f# mark X -> f# X)
      (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)
      (f# mark X -> f# X, f# ok X -> f# X)
      (f# mark X -> f# X, f# mark X -> f# X)
      (g# ok X -> g# X, g# ok X -> g# X)
      (proper# f X -> proper# X, proper# g X -> proper# X)
      (proper# f X -> proper# X, proper# g X -> g# proper X)
      (proper# f X -> proper# X, proper# f X -> proper# X)
      (proper# f X -> proper# X, proper# f X -> f# proper X)
      (top# mark X -> proper# X, proper# g X -> proper# X)
      (top# mark X -> proper# X, proper# g X -> g# proper X)
      (top# mark X -> proper# X, proper# f X -> proper# X)
      (top# mark X -> proper# X, proper# f X -> f# proper X)
      (top# ok X -> active# X, active# f X -> f# active X)
      (top# ok X -> active# X, active# f X -> active# X)
      (top# ok X -> active# X, active# f f a() -> f# g f a())
      (top# ok X -> active# X, active# f f a() -> g# f a())
      (proper# g X -> proper# X, proper# f X -> f# proper X)
      (proper# g X -> proper# X, proper# f X -> proper# X)
      (proper# g X -> proper# X, proper# g X -> g# proper X)
      (proper# g X -> proper# X, proper# g X -> proper# X)
      (active# f X -> active# X, active# f X -> f# active X)
      (active# f X -> active# X, active# f X -> active# X)
      (active# f X -> active# X, active# f f a() -> f# g f a())
      (active# f X -> active# X, active# f f a() -> g# f a())
      (f# ok X -> f# X, f# mark X -> f# X)
      (f# ok X -> f# X, f# ok X -> f# 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# g X -> g# proper X, g# ok X -> g# X)
      (active# f X -> f# active X, f# mark X -> f# X)
      (active# f X -> f# active X, f# ok X -> f# X)}
     EDG:
      {(proper# f X -> f# proper X, f# ok X -> f# X)
       (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# g X -> g# proper X, g# ok X -> g# X)
       (active# f X -> f# active X, f# mark X -> f# X)}
      EDG:
       {(proper# f X -> f# proper X, f# ok X -> f# X)
        (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# g X -> g# proper X, g# ok X -> g# X)
        (active# f X -> f# active X, f# mark X -> f# X)}
       STATUS:
        arrows: 0.951111
        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 X -> mark f X,
                   f ok X -> ok f X,
                   g ok X -> ok g X,
               active f X -> f active X,
           active f f a() -> mark f g f a(),
               proper f X -> f proper X,
               proper g X -> g proper X,
               proper a() -> ok a(),
               top mark X -> top proper X,
                 top ok X -> top active X}
          Open