MAYBE
Time: 0.021695
TRS:
 {        c ok X -> ok c X,
        f mark X -> mark f X,
          f ok X -> ok f X,
        g mark X -> mark g X,
          g ok X -> ok g X,
      active f X -> f active X,
  active f f a() -> mark c f g f a(),
      active g X -> g active X,
      proper c X -> c proper X,
      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:
   {        c# ok X -> c# X,
          f# mark X -> f# X,
            f# ok X -> f# X,
          g# mark X -> g# X,
            g# ok X -> g# X,
        active# f X -> f# active X,
        active# f X -> active# X,
    active# f f a() -> c# f g f a(),
    active# f f a() -> f# g f a(),
    active# f f a() -> g# f a(),
        active# g X -> g# active X,
        active# g X -> active# X,
        proper# c X -> c# proper X,
        proper# c X -> proper# X,
        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:
  {        c ok X -> ok c X,
         f mark X -> mark f X,
           f ok X -> ok f X,
         g mark X -> mark g X,
           g ok X -> ok g X,
       active f X -> f active X,
   active f f a() -> mark c f g f a(),
       active g X -> g active X,
       proper c X -> c proper X,
       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}
  EDG:
   {(f# mark X -> f# X, f# ok X -> f# X)
    (f# mark X -> f# X, f# mark X -> f# X)
    (g# mark X -> g# X, g# ok X -> g# X)
    (g# mark X -> g# X, g# mark X -> g# X)
    (active# f X -> active# X, active# g X -> active# X)
    (active# f X -> active# X, active# g X -> g# active X)
    (active# f X -> active# X, active# f f a() -> g# f a())
    (active# f X -> active# X, active# f f a() -> f# g f a())
    (active# f X -> active# X, active# f f a() -> c# f g f a())
    (active# f X -> active# X, active# f X -> active# X)
    (active# f X -> active# X, active# f X -> f# active X)
    (proper# c X -> proper# X, proper# g X -> proper# X)
    (proper# c X -> proper# X, proper# g X -> g# proper X)
    (proper# c X -> proper# X, proper# f X -> proper# X)
    (proper# c X -> proper# X, proper# f X -> f# proper X)
    (proper# c X -> proper# X, proper# c X -> proper# X)
    (proper# c X -> proper# X, proper# c X -> c# proper X)
    (proper# g X -> proper# X, proper# g X -> proper# X)
    (proper# g X -> proper# X, proper# g X -> g# proper X)
    (proper# g X -> proper# X, proper# f X -> proper# X)
    (proper# g X -> proper# X, proper# f X -> f# proper X)
    (proper# g X -> proper# X, proper# c X -> proper# X)
    (proper# g X -> proper# X, proper# c X -> c# proper X)
    (top# ok X -> active# X, active# g X -> active# X)
    (top# ok X -> active# X, active# g X -> g# active X)
    (top# ok X -> active# X, active# f f a() -> g# f a())
    (top# ok X -> active# X, active# f f a() -> f# g f a())
    (top# ok X -> active# X, active# f f a() -> c# f g f a())
    (top# ok X -> active# X, active# f X -> active# X)
    (top# ok X -> active# X, active# f X -> f# active X)
    (active# f X -> f# active X, f# ok X -> f# X)
    (active# f X -> f# active X, f# mark X -> f# X)
    (proper# c X -> c# proper X, c# ok X -> c# X)
    (proper# g X -> g# proper X, g# ok X -> g# X)
    (proper# g X -> g# proper X, g# mark X -> g# X)
    (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 X -> f# proper X, f# mark X -> f# X)
    (proper# f X -> f# proper X, f# ok X -> f# X)
    (active# g X -> g# active X, g# mark X -> g# X)
    (active# g X -> g# active X, g# ok X -> g# X)
    (top# mark X -> proper# X, proper# c X -> c# proper X)
    (top# mark X -> proper# X, proper# c X -> proper# X)
    (top# mark X -> proper# X, proper# f X -> f# proper X)
    (top# mark X -> proper# X, proper# f X -> proper# X)
    (top# mark X -> proper# X, proper# g X -> g# proper X)
    (top# mark X -> proper# X, proper# g X -> proper# X)
    (proper# f X -> proper# X, proper# c X -> c# proper X)
    (proper# f X -> proper# X, proper# c 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# f X -> proper# X, proper# g X -> g# proper X)
    (proper# f X -> proper# X, proper# g X -> proper# X)
    (active# g X -> active# X, active# f X -> f# active X)
    (active# g X -> active# X, active# f X -> active# X)
    (active# g X -> active# X, active# f f a() -> c# f g f a())
    (active# g X -> active# X, active# f f a() -> f# g f a())
    (active# g X -> active# X, active# f f a() -> g# f a())
    (active# g X -> active# X, active# g X -> g# active X)
    (active# g X -> active# X, active# g X -> active# X)
    (g# ok X -> g# X, g# mark X -> g# X)
    (g# ok X -> g# X, g# ok X -> g# X)
    (f# ok X -> f# X, f# mark X -> f# X)
    (f# ok X -> f# X, f# ok X -> f# X)
    (c# ok X -> c# X, c# ok X -> c# X)}
   STATUS:
    arrows: 0.853306
    SCCS (6):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      {proper# c X -> proper# X,
       proper# f X -> proper# X,
       proper# g X -> proper# X}
     Scc:
      {active# f X -> active# X,
       active# g X -> active# X}
     Scc:
      {g# mark X -> g# X,
         g# ok X -> g# X}
     Scc:
      {f# mark X -> f# X,
         f# ok X -> f# X}
     Scc:
      {c# ok X -> c# X}
     
     SCC (2):
      Strict:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Weak:
      {        c ok X -> ok c X,
             f mark X -> mark f X,
               f ok X -> ok f X,
             g mark X -> mark g X,
               g ok X -> ok g X,
           active f X -> f active X,
       active f f a() -> mark c f g f a(),
           active g X -> g active X,
           proper c X -> c proper X,
           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
     
     
     SCC (3):
      Strict:
       {proper# c X -> proper# X,
        proper# f X -> proper# X,
        proper# g X -> proper# X}
      Weak:
      {        c ok X -> ok c X,
             f mark X -> mark f X,
               f ok X -> ok f X,
             g mark X -> mark g X,
               g ok X -> ok g X,
           active f X -> f active X,
       active f f a() -> mark c f g f a(),
           active g X -> g active X,
           proper c X -> c proper X,
           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
     
     
     
     SCC (2):
      Strict:
       {active# f X -> active# X,
        active# g X -> active# X}
      Weak:
      {        c ok X -> ok c X,
             f mark X -> mark f X,
               f ok X -> ok f X,
             g mark X -> mark g X,
               g ok X -> ok g X,
           active f X -> f active X,
       active f f a() -> mark c f g f a(),
           active g X -> g active X,
           proper c X -> c proper X,
           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
     
     
     
     
     
     SCC (2):
      Strict:
       {g# mark X -> g# X,
          g# ok X -> g# X}
      Weak:
      {        c ok X -> ok c X,
             f mark X -> mark f X,
               f ok X -> ok f X,
             g mark X -> mark g X,
               g ok X -> ok g X,
           active f X -> f active X,
       active f f a() -> mark c f g f a(),
           active g X -> g active X,
           proper c X -> c proper X,
           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
     SCC (2):
      Strict:
       {f# mark X -> f# X,
          f# ok X -> f# X}
      Weak:
      {        c ok X -> ok c X,
             f mark X -> mark f X,
               f ok X -> ok f X,
             g mark X -> mark g X,
               g ok X -> ok g X,
           active f X -> f active X,
       active f f a() -> mark c f g f a(),
           active g X -> g active X,
           proper c X -> c proper X,
           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
     SCC (1):
      Strict:
       {c# ok X -> c# X}
      Weak:
      {        c ok X -> ok c X,
             f mark X -> mark f X,
               f ok X -> ok f X,
             g mark X -> mark g X,
               g ok X -> ok g X,
           active f X -> f active X,
       active f f a() -> mark c f g f a(),
           active g X -> g active X,
           proper c X -> c proper X,
           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