MAYBE
Time: 0.014536
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:
    {(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)}
    STATUS:
     arrows: 0.930556
     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 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}
       Fail