MAYBE
Time: 0.012063
TRS:
 {      h ok X -> ok h X,
  active h d() -> mark g c(),
    active g X -> mark h X,
    active c() -> mark d(),
        g ok X -> ok g X,
    proper h X -> h proper X,
    proper g X -> g proper X,
    proper d() -> ok d(),
    proper c() -> ok c(),
    top mark X -> top proper X,
      top ok X -> top active X}
 DP:
  DP:
   {      h# ok X -> h# X,
    active# h d() -> g# c(),
      active# g X -> h# X,
          g# ok X -> g# X,
      proper# h X -> h# proper X,
      proper# h 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:
  {      h ok X -> ok h X,
   active h d() -> mark g c(),
     active g X -> mark h X,
     active c() -> mark d(),
         g ok X -> ok g X,
     proper h X -> h proper X,
     proper g X -> g proper X,
     proper d() -> ok d(),
     proper c() -> ok c(),
     top mark X -> top proper X,
       top ok X -> top active X}
  UR:
   {      h ok X -> ok h X,
    active h d() -> mark g c(),
      active g X -> mark h X,
      active c() -> mark d(),
          g ok X -> ok g X,
      proper h X -> h proper X,
      proper g X -> g proper X,
      proper d() -> ok d(),
      proper c() -> ok c()}
   EDG:
    {(active# g X -> h# X, h# ok X -> h# X)
     (proper# h X -> proper# X, proper# g X -> proper# X)
     (proper# h X -> proper# X, proper# g X -> g# proper X)
     (proper# h X -> proper# X, proper# h X -> proper# X)
     (proper# h 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# mark X -> proper# X, proper# h X -> proper# X)
     (top# mark X -> proper# X, proper# h X -> h# proper X)
     (proper# g X -> g# proper X, g# ok X -> g# 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# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (proper# h X -> h# proper X, h# ok X -> h# X)
     (top# ok X -> active# X, active# h d() -> g# c())
     (top# ok X -> active# X, active# g X -> h# 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# g X -> g# proper X)
     (proper# g X -> proper# X, proper# g X -> proper# X)
     (g# ok X -> g# X, g# ok X -> g# X)
     (h# ok X -> h# X, h# ok X -> h# X)}
    STATUS:
     arrows: 0.840278
     SCCS (4):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {proper# h X -> proper# X,
        proper# g X -> proper# X}
      Scc:
       {g# ok X -> g# X}
      Scc:
       {h# ok X -> h# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {      h ok X -> ok h X,
        active h d() -> mark g c(),
          active g X -> mark h X,
          active c() -> mark d(),
              g ok X -> ok g X,
          proper h X -> h proper X,
          proper g X -> g proper X,
          proper d() -> ok d(),
          proper c() -> ok c(),
          top mark X -> top proper X,
            top ok X -> top active X}
       Open
      
      
      
      SCC (2):
       Strict:
        {proper# h X -> proper# X,
         proper# g X -> proper# X}
       Weak:
       {      h ok X -> ok h X,
        active h d() -> mark g c(),
          active g X -> mark h X,
          active c() -> mark d(),
              g ok X -> ok g X,
          proper h X -> h proper X,
          proper g X -> g proper X,
          proper d() -> ok d(),
          proper c() -> ok c(),
          top mark X -> top proper X,
            top ok X -> top active X}
       Open
      
      
      SCC (1):
       Strict:
        {g# ok X -> g# X}
       Weak:
       {      h ok X -> ok h X,
        active h d() -> mark g c(),
          active g X -> mark h X,
          active c() -> mark d(),
              g ok X -> ok g X,
          proper h X -> h proper X,
          proper g X -> g proper X,
          proper d() -> ok d(),
          proper c() -> ok c(),
          top mark X -> top proper X,
            top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {h# ok X -> h# X}
       Weak:
       {      h ok X -> ok h X,
        active h d() -> mark g c(),
          active g X -> mark h X,
          active c() -> mark d(),
              g ok X -> ok g X,
          proper h X -> h proper X,
          proper g X -> g proper X,
          proper d() -> ok d(),
          proper c() -> ok c(),
          top mark X -> top proper X,
            top ok X -> top active X}
       Open