MAYBE
Time: 0.009351
TRS:
 {  g(mark X1, X2) -> mark g(X1, X2),
   g(ok X1, ok X2) -> ok g(X1, X2),
  active g(X1, X2) -> g(active X1, X2),
  active g(a(), X) -> mark f(b(), X),
        active h X -> mark g(X, X),
        active h X -> h active X,
    active f(X, X) -> mark h a(),
  active f(X1, X2) -> f(active X1, X2),
        active a() -> mark b(),
          h mark X -> mark h X,
            h ok X -> ok h X,
    f(mark X1, X2) -> mark f(X1, X2),
   f(ok X1, ok X2) -> ok f(X1, X2),
  proper g(X1, X2) -> g(proper X1, proper X2),
        proper h X -> h proper X,
  proper f(X1, X2) -> f(proper X1, proper X2),
        proper b() -> ok b(),
        proper a() -> ok a(),
        top mark X -> top proper X,
          top ok X -> top active X}
 DP:
  DP:
   {  g#(mark X1, X2) -> g#(X1, X2),
     g#(ok X1, ok X2) -> g#(X1, X2),
    active# g(X1, X2) -> g#(active X1, X2),
    active# g(X1, X2) -> active# X1,
    active# g(a(), X) -> f#(b(), X),
          active# h X -> g#(X, X),
          active# h X -> active# X,
          active# h X -> h# active X,
      active# f(X, X) -> h# a(),
    active# f(X1, X2) -> active# X1,
    active# f(X1, X2) -> f#(active X1, X2),
            h# mark X -> h# X,
              h# ok X -> h# X,
      f#(mark X1, X2) -> f#(X1, X2),
     f#(ok X1, ok X2) -> f#(X1, X2),
    proper# g(X1, X2) -> g#(proper X1, proper X2),
    proper# g(X1, X2) -> proper# X1,
    proper# g(X1, X2) -> proper# X2,
          proper# h X -> h# proper X,
          proper# h X -> proper# X,
    proper# f(X1, X2) -> f#(proper X1, proper X2),
    proper# f(X1, X2) -> proper# X1,
    proper# f(X1, X2) -> proper# X2,
          top# mark X -> proper# X,
          top# mark X -> top# proper X,
            top# ok X -> active# X,
            top# ok X -> top# active X}
  TRS:
  {  g(mark X1, X2) -> mark g(X1, X2),
    g(ok X1, ok X2) -> ok g(X1, X2),
   active g(X1, X2) -> g(active X1, X2),
   active g(a(), X) -> mark f(b(), X),
         active h X -> mark g(X, X),
         active h X -> h active X,
     active f(X, X) -> mark h a(),
   active f(X1, X2) -> f(active X1, X2),
         active a() -> mark b(),
           h mark X -> mark h X,
             h ok X -> ok h X,
     f(mark X1, X2) -> mark f(X1, X2),
    f(ok X1, ok X2) -> ok f(X1, X2),
   proper g(X1, X2) -> g(proper X1, proper X2),
         proper h X -> h proper X,
   proper f(X1, X2) -> f(proper X1, proper X2),
         proper b() -> ok b(),
         proper a() -> ok a(),
         top mark X -> top proper X,
           top ok X -> top active X}
  UR:
   {  g(mark X1, X2) -> mark g(X1, X2),
     g(ok X1, ok X2) -> ok g(X1, X2),
    active g(X1, X2) -> g(active X1, X2),
    active g(a(), X) -> mark f(b(), X),
          active h X -> mark g(X, X),
          active h X -> h active X,
      active f(X, X) -> mark h a(),
    active f(X1, X2) -> f(active X1, X2),
          active a() -> mark b(),
            h mark X -> mark h X,
              h ok X -> ok h X,
      f(mark X1, X2) -> mark f(X1, X2),
     f(ok X1, ok X2) -> ok f(X1, X2),
    proper g(X1, X2) -> g(proper X1, proper X2),
          proper h X -> h proper X,
    proper f(X1, X2) -> f(proper X1, proper X2),
          proper b() -> ok b(),
          proper a() -> ok a(),
             c(x, y) -> x,
             c(x, y) -> y}
   EDG:
    {(active# f(X, X) -> h# a(), h# ok X -> h# X)
     (active# f(X, X) -> h# a(), h# mark X -> h# X)
     (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(mark X1, X2) -> f#(X1, X2))
     (h# mark X -> h# X, h# ok X -> h# X)
     (h# mark X -> h# X, h# mark X -> h# X)
     (proper# h X -> proper# X, proper# f(X1, X2) -> proper# X2)
     (proper# h X -> proper# X, proper# f(X1, X2) -> proper# X1)
     (proper# h X -> proper# X, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (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(X1, X2) -> proper# X2)
     (proper# h X -> proper# X, proper# g(X1, X2) -> proper# X1)
     (proper# h X -> proper# X, proper# g(X1, X2) -> g#(proper X1, proper X2))
     (top# ok X -> active# X, active# f(X1, X2) -> f#(active X1, X2))
     (top# ok X -> active# X, active# f(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# f(X, X) -> h# a())
     (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# h X -> g#(X, X))
     (top# ok X -> active# X, active# g(a(), X) -> f#(b(), X))
     (top# ok X -> active# X, active# g(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# g(X1, X2) -> g#(active X1, X2))
     (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X2)
     (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X1)
     (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (proper# f(X1, X2) -> proper# X2, proper# h X -> proper# X)
     (proper# f(X1, X2) -> proper# X2, proper# h X -> h# proper X)
     (proper# f(X1, X2) -> proper# X2, proper# g(X1, X2) -> proper# X2)
     (proper# f(X1, X2) -> proper# X2, proper# g(X1, X2) -> proper# X1)
     (proper# f(X1, X2) -> proper# X2, proper# g(X1, X2) -> g#(proper X1, proper X2))
     (active# f(X1, X2) -> f#(active X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (active# f(X1, X2) -> f#(active X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (proper# h X -> h# proper X, h# ok X -> h# X)
     (proper# h X -> h# proper X, h# mark X -> h# 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)
     (g#(ok X1, ok X2) -> g#(X1, X2), g#(ok X1, ok X2) -> g#(X1, X2))
     (g#(ok X1, ok X2) -> g#(X1, X2), g#(mark X1, X2) -> g#(X1, X2))
     (f#(ok X1, ok X2) -> f#(X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (f#(ok X1, ok X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (active# f(X1, X2) -> active# X1, active# f(X1, X2) -> f#(active X1, X2))
     (active# f(X1, X2) -> active# X1, active# f(X1, X2) -> active# X1)
     (active# f(X1, X2) -> active# X1, active# f(X, X) -> h# a())
     (active# f(X1, X2) -> active# X1, active# h X -> h# active X)
     (active# f(X1, X2) -> active# X1, active# h X -> active# X)
     (active# f(X1, X2) -> active# X1, active# h X -> g#(X, X))
     (active# f(X1, X2) -> active# X1, active# g(a(), X) -> f#(b(), X))
     (active# f(X1, X2) -> active# X1, active# g(X1, X2) -> active# X1)
     (active# f(X1, X2) -> active# X1, active# g(X1, X2) -> g#(active X1, X2))
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X2)
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X1)
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (proper# f(X1, X2) -> proper# X1, proper# h X -> proper# X)
     (proper# f(X1, X2) -> proper# X1, proper# h X -> h# proper X)
     (proper# f(X1, X2) -> proper# X1, proper# g(X1, X2) -> proper# X2)
     (proper# f(X1, X2) -> proper# X1, proper# g(X1, X2) -> proper# X1)
     (proper# f(X1, X2) -> proper# X1, proper# g(X1, X2) -> g#(proper X1, proper X2))
     (active# g(a(), X) -> f#(b(), X), f#(mark X1, X2) -> f#(X1, X2))
     (active# g(a(), X) -> f#(b(), X), f#(ok X1, ok X2) -> f#(X1, X2))
     (proper# g(X1, X2) -> proper# X1, proper# g(X1, X2) -> g#(proper X1, proper X2))
     (proper# g(X1, X2) -> proper# X1, proper# g(X1, X2) -> proper# X1)
     (proper# g(X1, X2) -> proper# X1, proper# g(X1, X2) -> proper# X2)
     (proper# g(X1, X2) -> proper# X1, proper# h X -> h# proper X)
     (proper# g(X1, X2) -> proper# X1, proper# h X -> proper# X)
     (proper# g(X1, X2) -> proper# X1, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (proper# g(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X1)
     (proper# g(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X2)
     (active# g(X1, X2) -> active# X1, active# g(X1, X2) -> g#(active X1, X2))
     (active# g(X1, X2) -> active# X1, active# g(X1, X2) -> active# X1)
     (active# g(X1, X2) -> active# X1, active# g(a(), X) -> f#(b(), X))
     (active# g(X1, X2) -> active# X1, active# h X -> g#(X, X))
     (active# g(X1, X2) -> active# X1, active# h X -> active# X)
     (active# g(X1, X2) -> active# X1, active# h X -> h# active X)
     (active# g(X1, X2) -> active# X1, active# f(X, X) -> h# a())
     (active# g(X1, X2) -> active# X1, active# f(X1, X2) -> active# X1)
     (active# g(X1, X2) -> active# X1, active# f(X1, X2) -> f#(active X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (g#(mark X1, X2) -> g#(X1, X2), g#(mark X1, X2) -> g#(X1, X2))
     (g#(mark X1, X2) -> g#(X1, X2), g#(ok X1, ok X2) -> g#(X1, X2))
     (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)
     (active# h X -> h# active X, h# mark X -> h# X)
     (active# h X -> h# active X, h# ok X -> h# X)
     (active# g(X1, X2) -> g#(active X1, X2), g#(mark X1, X2) -> g#(X1, X2))
     (active# g(X1, X2) -> g#(active X1, X2), g#(ok X1, ok X2) -> g#(X1, X2))
     (proper# g(X1, X2) -> proper# X2, proper# g(X1, X2) -> g#(proper X1, proper X2))
     (proper# g(X1, X2) -> proper# X2, proper# g(X1, X2) -> proper# X1)
     (proper# g(X1, X2) -> proper# X2, proper# g(X1, X2) -> proper# X2)
     (proper# g(X1, X2) -> proper# X2, proper# h X -> h# proper X)
     (proper# g(X1, X2) -> proper# X2, proper# h X -> proper# X)
     (proper# g(X1, X2) -> proper# X2, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (proper# g(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X1)
     (proper# g(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# g(X1, X2) -> g#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# g(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# g(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# h X -> h# proper X)
     (top# mark X -> proper# X, proper# h X -> proper# X)
     (top# mark X -> proper# X, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# f(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# f(X1, X2) -> proper# X2)
     (h# ok X -> h# X, h# mark X -> h# X)
     (h# ok X -> h# X, h# ok X -> h# X)
     (active# h X -> active# X, active# g(X1, X2) -> g#(active X1, X2))
     (active# h X -> active# X, active# g(X1, X2) -> active# X1)
     (active# h X -> active# X, active# g(a(), X) -> f#(b(), X))
     (active# h X -> active# X, active# h X -> g#(X, X))
     (active# h X -> active# X, active# h X -> active# X)
     (active# h X -> active# X, active# h X -> h# active X)
     (active# h X -> active# X, active# f(X, X) -> h# a())
     (active# h X -> active# X, active# f(X1, X2) -> active# X1)
     (active# h X -> active# X, active# f(X1, X2) -> f#(active X1, X2))
     (proper# g(X1, X2) -> g#(proper X1, proper X2), g#(mark X1, X2) -> g#(X1, X2))
     (proper# g(X1, X2) -> g#(proper X1, proper X2), g#(ok X1, ok X2) -> g#(X1, X2))
     (active# h X -> g#(X, X), g#(mark X1, X2) -> g#(X1, X2))
     (active# h X -> g#(X, X), g#(ok X1, ok X2) -> g#(X1, X2))}
    STATUS:
     arrows: 0.832647
     SCCS (6):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {proper# g(X1, X2) -> proper# X1,
        proper# g(X1, X2) -> proper# X2,
              proper# h X -> proper# X,
        proper# f(X1, X2) -> proper# X1,
        proper# f(X1, X2) -> proper# X2}
      Scc:
       {active# g(X1, X2) -> active# X1,
              active# h X -> active# X,
        active# f(X1, X2) -> active# X1}
      Scc:
       { f#(mark X1, X2) -> f#(X1, X2),
        f#(ok X1, ok X2) -> f#(X1, X2)}
      Scc:
       {h# mark X -> h# X,
          h# ok X -> h# X}
      Scc:
       { g#(mark X1, X2) -> g#(X1, X2),
        g#(ok X1, ok X2) -> g#(X1, X2)}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {  g(mark X1, X2) -> mark g(X1, X2),
         g(ok X1, ok X2) -> ok g(X1, X2),
        active g(X1, X2) -> g(active X1, X2),
        active g(a(), X) -> mark f(b(), X),
              active h X -> mark g(X, X),
              active h X -> h active X,
          active f(X, X) -> mark h a(),
        active f(X1, X2) -> f(active X1, X2),
              active a() -> mark b(),
                h mark X -> mark h X,
                  h ok X -> ok h X,
          f(mark X1, X2) -> mark f(X1, X2),
         f(ok X1, ok X2) -> ok f(X1, X2),
        proper g(X1, X2) -> g(proper X1, proper X2),
              proper h X -> h proper X,
        proper f(X1, X2) -> f(proper X1, proper X2),
              proper b() -> ok b(),
              proper a() -> ok a(),
              top mark X -> top proper X,
                top ok X -> top active X}
       Open
      
      
      SCC (5):
       Strict:
        {proper# g(X1, X2) -> proper# X1,
         proper# g(X1, X2) -> proper# X2,
               proper# h X -> proper# X,
         proper# f(X1, X2) -> proper# X1,
         proper# f(X1, X2) -> proper# X2}
       Weak:
       {  g(mark X1, X2) -> mark g(X1, X2),
         g(ok X1, ok X2) -> ok g(X1, X2),
        active g(X1, X2) -> g(active X1, X2),
        active g(a(), X) -> mark f(b(), X),
              active h X -> mark g(X, X),
              active h X -> h active X,
          active f(X, X) -> mark h a(),
        active f(X1, X2) -> f(active X1, X2),
              active a() -> mark b(),
                h mark X -> mark h X,
                  h ok X -> ok h X,
          f(mark X1, X2) -> mark f(X1, X2),
         f(ok X1, ok X2) -> ok f(X1, X2),
        proper g(X1, X2) -> g(proper X1, proper X2),
              proper h X -> h proper X,
        proper f(X1, X2) -> f(proper X1, proper X2),
              proper b() -> ok b(),
              proper a() -> ok a(),
              top mark X -> top proper X,
                top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        {active# g(X1, X2) -> active# X1,
               active# h X -> active# X,
         active# f(X1, X2) -> active# X1}
       Weak:
       {  g(mark X1, X2) -> mark g(X1, X2),
         g(ok X1, ok X2) -> ok g(X1, X2),
        active g(X1, X2) -> g(active X1, X2),
        active g(a(), X) -> mark f(b(), X),
              active h X -> mark g(X, X),
              active h X -> h active X,
          active f(X, X) -> mark h a(),
        active f(X1, X2) -> f(active X1, X2),
              active a() -> mark b(),
                h mark X -> mark h X,
                  h ok X -> ok h X,
          f(mark X1, X2) -> mark f(X1, X2),
         f(ok X1, ok X2) -> ok f(X1, X2),
        proper g(X1, X2) -> g(proper X1, proper X2),
              proper h X -> h proper X,
        proper f(X1, X2) -> f(proper X1, proper X2),
              proper b() -> ok b(),
              proper a() -> ok a(),
              top mark X -> top proper X,
                top ok X -> top active X}
       Open
      
      
      
      
      
      SCC (2):
       Strict:
        { f#(mark X1, X2) -> f#(X1, X2),
         f#(ok X1, ok X2) -> f#(X1, X2)}
       Weak:
       {  g(mark X1, X2) -> mark g(X1, X2),
         g(ok X1, ok X2) -> ok g(X1, X2),
        active g(X1, X2) -> g(active X1, X2),
        active g(a(), X) -> mark f(b(), X),
              active h X -> mark g(X, X),
              active h X -> h active X,
          active f(X, X) -> mark h a(),
        active f(X1, X2) -> f(active X1, X2),
              active a() -> mark b(),
                h mark X -> mark h X,
                  h ok X -> ok h X,
          f(mark X1, X2) -> mark f(X1, X2),
         f(ok X1, ok X2) -> ok f(X1, X2),
        proper g(X1, X2) -> g(proper X1, proper X2),
              proper h X -> h proper X,
        proper f(X1, X2) -> f(proper X1, proper X2),
              proper b() -> ok b(),
              proper a() -> ok a(),
              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(mark X1, X2) -> mark g(X1, X2),
         g(ok X1, ok X2) -> ok g(X1, X2),
        active g(X1, X2) -> g(active X1, X2),
        active g(a(), X) -> mark f(b(), X),
              active h X -> mark g(X, X),
              active h X -> h active X,
          active f(X, X) -> mark h a(),
        active f(X1, X2) -> f(active X1, X2),
              active a() -> mark b(),
                h mark X -> mark h X,
                  h ok X -> ok h X,
          f(mark X1, X2) -> mark f(X1, X2),
         f(ok X1, ok X2) -> ok f(X1, X2),
        proper g(X1, X2) -> g(proper X1, proper X2),
              proper h X -> h proper X,
        proper f(X1, X2) -> f(proper X1, proper X2),
              proper b() -> ok b(),
              proper a() -> ok a(),
              top mark X -> top proper X,
                top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        { g#(mark X1, X2) -> g#(X1, X2),
         g#(ok X1, ok X2) -> g#(X1, X2)}
       Weak:
       {  g(mark X1, X2) -> mark g(X1, X2),
         g(ok X1, ok X2) -> ok g(X1, X2),
        active g(X1, X2) -> g(active X1, X2),
        active g(a(), X) -> mark f(b(), X),
              active h X -> mark g(X, X),
              active h X -> h active X,
          active f(X, X) -> mark h a(),
        active f(X1, X2) -> f(active X1, X2),
              active a() -> mark b(),
                h mark X -> mark h X,
                  h ok X -> ok h X,
          f(mark X1, X2) -> mark f(X1, X2),
         f(ok X1, ok X2) -> ok f(X1, X2),
        proper g(X1, X2) -> g(proper X1, proper X2),
              proper h X -> h proper X,
        proper f(X1, X2) -> f(proper X1, proper X2),
              proper b() -> ok b(),
              proper a() -> ok a(),
              top mark X -> top proper X,
                top ok X -> top active X}
       Open