MAYBE
Time: 0.011622
TRS:
 {    g ok X -> ok g X,
    h mark X -> mark h X,
      h ok X -> ok h X,
    f mark X -> mark f X,
      f ok X -> ok f X,
  active h X -> h active X,
  active f X -> mark g h f X,
  active f X -> f active X,
  proper g X -> g proper X,
  proper h X -> h proper X,
  proper f X -> f proper X,
  top mark X -> top proper X,
    top ok X -> top active X}
 DP:
  DP:
   {    g# ok X -> g# X,
      h# mark X -> h# X,
        h# ok X -> h# X,
      f# mark X -> f# X,
        f# ok X -> f# X,
    active# h X -> h# active X,
    active# h X -> active# X,
    active# f X -> g# h f X,
    active# f X -> h# f X,
    active# f X -> f# active X,
    active# f X -> active# X,
    proper# g X -> g# proper X,
    proper# g X -> proper# X,
    proper# h X -> h# proper X,
    proper# h X -> proper# X,
    proper# f X -> f# proper X,
    proper# f 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:
  {    g ok X -> ok g X,
     h mark X -> mark h X,
       h ok X -> ok h X,
     f mark X -> mark f X,
       f ok X -> ok f X,
   active h X -> h active X,
   active f X -> mark g h f X,
   active f X -> f active X,
   proper g X -> g proper X,
   proper h X -> h proper X,
   proper f X -> f proper X,
   top mark X -> top proper X,
     top ok X -> top active X}
  UR:
   {    g ok X -> ok g X,
      h mark X -> mark h X,
        h ok X -> ok h X,
      f mark X -> mark f X,
        f ok X -> ok f X,
    active h X -> h active X,
    active f X -> mark g h f X,
    active f X -> f active X,
    proper g X -> g proper X,
    proper h X -> h proper X,
    proper f X -> f proper X}
   EDG:
    {(active# h X -> h# active X, h# ok X -> h# X)
     (active# h X -> h# active X, h# mark X -> h# X)
     (active# f X -> f# active X, f# ok X -> f# X)
     (active# f X -> f# active X, f# mark X -> f# X)
     (proper# h X -> h# proper X, h# ok X -> h# X)
     (proper# h X -> h# proper X, h# mark X -> h# 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)
     (g# ok X -> g# X, g# ok X -> g# X)
     (h# ok X -> h# X, h# ok X -> h# X)
     (h# ok X -> h# X, h# mark X -> h# X)
     (f# ok X -> f# X, f# ok X -> f# X)
     (f# ok X -> f# X, f# mark X -> f# X)
     (active# f X -> active# X, active# f X -> active# X)
     (active# f X -> active# X, active# f X -> f# active X)
     (active# f X -> active# X, active# f X -> h# f X)
     (active# f X -> active# X, active# f X -> g# h f X)
     (active# f X -> active# X, active# h X -> active# X)
     (active# f X -> active# X, active# h X -> h# active X)
     (proper# h X -> proper# X, proper# f X -> proper# X)
     (proper# h X -> proper# X, proper# f X -> f# proper X)
     (proper# h X -> proper# X, proper# h X -> proper# X)
     (proper# h X -> proper# X, proper# h X -> h# proper X)
     (proper# h X -> proper# X, proper# g X -> proper# X)
     (proper# h 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# mark X -> proper# X, proper# h X -> proper# X)
     (top# mark X -> proper# X, proper# h X -> h# proper X)
     (top# mark X -> proper# X, proper# g X -> proper# X)
     (top# mark X -> proper# X, proper# g X -> g# proper X)
     (top# ok X -> active# X, active# h X -> h# active X)
     (top# ok X -> active# X, active# h X -> active# X)
     (top# ok X -> active# X, active# f X -> g# h f X)
     (top# ok X -> active# X, active# f X -> h# f X)
     (top# ok X -> active# X, active# f X -> f# active X)
     (top# ok X -> active# X, active# f X -> active# X)
     (proper# f X -> proper# X, proper# g X -> g# proper X)
     (proper# f X -> proper# X, proper# g X -> proper# X)
     (proper# f X -> proper# X, proper# h X -> h# proper X)
     (proper# f X -> proper# X, proper# h X -> proper# X)
     (proper# f X -> proper# X, proper# f X -> f# proper X)
     (proper# f 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)
     (proper# g X -> proper# X, proper# h X -> h# proper X)
     (proper# g X -> proper# X, proper# h X -> proper# X)
     (proper# g X -> proper# X, proper# f X -> f# proper X)
     (proper# g X -> proper# X, proper# f X -> proper# X)
     (active# h X -> active# X, active# h X -> h# active X)
     (active# h X -> active# X, active# h X -> active# X)
     (active# h X -> active# X, active# f X -> g# h f X)
     (active# h X -> active# X, active# f X -> h# f X)
     (active# h X -> active# X, active# f X -> f# active X)
     (active# h X -> active# X, active# f X -> active# X)
     (f# mark X -> f# X, f# mark X -> f# X)
     (f# mark X -> f# X, f# ok X -> f# X)
     (h# mark X -> h# X, h# mark X -> h# X)
     (h# mark X -> h# X, h# ok X -> h# 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# f X -> f# proper X, f# mark X -> f# X)
     (proper# f X -> f# proper X, f# ok X -> f# X)
     (proper# g X -> g# proper X, g# ok X -> g# X)
     (active# f X -> h# f X, h# mark X -> h# X)
     (active# f X -> h# f X, h# ok X -> h# X)
     (active# f X -> g# h f X, g# ok X -> g# X)}
    STATUS:
     arrows: 0.839002
     SCCS (6):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {active# h X -> active# X,
        active# f X -> active# X}
      Scc:
       {proper# g X -> proper# X,
        proper# h X -> proper# X,
        proper# f X -> proper# X}
      Scc:
       {f# mark X -> f# X,
          f# ok X -> f# X}
      Scc:
       {h# mark X -> h# X,
          h# ok X -> h# X}
      Scc:
       {g# ok X -> g# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {    g ok X -> ok g X,
          h mark X -> mark h X,
            h ok X -> ok h X,
          f mark X -> mark f X,
            f ok X -> ok f X,
        active h X -> h active X,
        active f X -> mark g h f X,
        active f X -> f active X,
        proper g X -> g proper X,
        proper h X -> h proper X,
        proper f X -> f proper X,
        top mark X -> top proper X,
          top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {active# h X -> active# X,
         active# f X -> active# X}
       Weak:
       {    g ok X -> ok g X,
          h mark X -> mark h X,
            h ok X -> ok h X,
          f mark X -> mark f X,
            f ok X -> ok f X,
        active h X -> h active X,
        active f X -> mark g h f X,
        active f X -> f active X,
        proper g X -> g proper X,
        proper h X -> h proper X,
        proper f X -> f proper X,
        top mark X -> top proper X,
          top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        {proper# g X -> proper# X,
         proper# h X -> proper# X,
         proper# f X -> proper# X}
       Weak:
       {    g ok X -> ok g X,
          h mark X -> mark h X,
            h ok X -> ok h X,
          f mark X -> mark f X,
            f ok X -> ok f X,
        active h X -> h active X,
        active f X -> mark g h f X,
        active f X -> f active X,
        proper g X -> g proper X,
        proper h X -> h proper X,
        proper f X -> f proper X,
        top mark X -> top proper X,
          top ok X -> top active X}
       Open
      
      
      
      
      SCC (2):
       Strict:
        {f# mark X -> f# X,
           f# ok X -> f# X}
       Weak:
       {    g ok X -> ok g X,
          h mark X -> mark h X,
            h ok X -> ok h X,
          f mark X -> mark f X,
            f ok X -> ok f X,
        active h X -> h active X,
        active f X -> mark g h f X,
        active f X -> f active X,
        proper g X -> g proper X,
        proper h X -> h proper X,
        proper f X -> f proper X,
        top mark X -> top proper X,
          top ok X -> top active X}
       Open
      
      
      SCC (2):
       Strict:
        {h# mark X -> h# X,
           h# ok X -> h# X}
       Weak:
       {    g ok X -> ok g X,
          h mark X -> mark h X,
            h ok X -> ok h X,
          f mark X -> mark f X,
            f ok X -> ok f X,
        active h X -> h active X,
        active f X -> mark g h f X,
        active f X -> f active X,
        proper g X -> g proper X,
        proper h X -> h proper X,
        proper f X -> f proper X,
        top mark X -> top proper X,
          top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {g# ok X -> g# X}
       Weak:
       {    g ok X -> ok g X,
          h mark X -> mark h X,
            h ok X -> ok h X,
          f mark X -> mark f X,
            f ok X -> ok f X,
        active h X -> h active X,
        active f X -> mark g h f X,
        active f X -> f active X,
        proper g X -> g proper X,
        proper h X -> h proper X,
        proper f X -> f proper X,
        top mark X -> top proper X,
          top ok X -> top active X}
       Open