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