MAYBE
Time: 0.006692
TRS:
 {      f(x, y, mark z) -> mark f(x, y, z),
    f(ok x, ok y, ok z) -> ok f(x, y, z),
      active f(x, y, z) -> f(x, y, active z),
  active f(b(), c(), x) -> mark f(x, x, x),
             active d() -> mark c(),
             active d() -> m b(),
      proper f(x, y, z) -> f(proper x, proper y, proper z),
             proper b() -> ok b(),
             proper c() -> ok c(),
             proper d() -> ok d(),
             top mark x -> top proper x,
               top ok x -> top active x}
 DP:
  DP:
   {      f#(x, y, mark z) -> f#(x, y, z),
      f#(ok x, ok y, ok z) -> f#(x, y, z),
        active# f(x, y, z) -> f#(x, y, active z),
        active# f(x, y, z) -> active# z,
    active# f(b(), c(), x) -> f#(x, x, x),
        proper# f(x, y, z) -> f#(proper x, proper y, proper z),
        proper# f(x, y, z) -> proper# x,
        proper# f(x, y, z) -> proper# y,
        proper# f(x, y, z) -> proper# z,
               top# mark x -> proper# x,
               top# mark x -> top# proper x,
                 top# ok x -> active# x,
                 top# ok x -> top# active x}
  TRS:
  {      f(x, y, mark z) -> mark f(x, y, z),
     f(ok x, ok y, ok z) -> ok f(x, y, z),
       active f(x, y, z) -> f(x, y, active z),
   active f(b(), c(), x) -> mark f(x, x, x),
              active d() -> mark c(),
              active d() -> m b(),
       proper f(x, y, z) -> f(proper x, proper y, proper z),
              proper b() -> ok b(),
              proper c() -> ok c(),
              proper d() -> ok d(),
              top mark x -> top proper x,
                top ok x -> top active x}
  UR:
   {      f(x, y, mark z) -> mark f(x, y, z),
      f(ok x, ok y, ok z) -> ok f(x, y, z),
        active f(x, y, z) -> f(x, y, active z),
    active f(b(), c(), x) -> mark f(x, x, x),
               active d() -> mark c(),
               active d() -> m b(),
        proper f(x, y, z) -> f(proper x, proper y, proper z),
               proper b() -> ok b(),
               proper c() -> ok c(),
               proper d() -> ok d(),
                  a(w, v) -> w,
                  a(w, v) -> v}
   EDG:
    {(active# f(x, y, z) -> f#(x, y, active z), f#(ok x, ok y, ok z) -> f#(x, y, z))
     (active# f(x, y, z) -> f#(x, y, active z), f#(x, y, mark z) -> f#(x, y, z))
     (proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# z)
     (proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# y)
     (proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# x)
     (proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> f#(proper x, proper y, proper z))
     (top# ok x -> active# x, active# f(b(), c(), x) -> f#(x, x, x))
     (top# ok x -> active# x, active# f(x, y, z) -> active# z)
     (top# ok x -> active# x, active# f(x, y, z) -> f#(x, y, active z))
     (f#(x, y, mark z) -> f#(x, y, z), f#(ok x, ok y, ok z) -> f#(x, y, z))
     (f#(x, y, mark z) -> f#(x, y, z), f#(x, y, mark z) -> f#(x, y, z))
     (active# f(x, y, z) -> active# z, active# f(b(), c(), x) -> f#(x, x, x))
     (active# f(x, y, z) -> active# z, active# f(x, y, z) -> active# z)
     (active# f(x, y, z) -> active# z, active# f(x, y, z) -> f#(x, y, active z))
     (top# mark x -> top# proper x, top# ok x -> top# active x)
     (top# mark x -> top# proper x, top# ok x -> active# x)
     (top# mark x -> top# proper x, top# mark x -> top# proper x)
     (top# mark x -> top# proper x, top# mark x -> proper# x)
     (top# ok x -> top# active x, top# mark x -> proper# x)
     (top# ok x -> top# active x, top# mark x -> top# proper x)
     (top# ok x -> top# active x, top# ok x -> active# x)
     (top# ok x -> top# active x, top# ok x -> top# active x)
     (proper# f(x, y, z) -> proper# z, proper# f(x, y, z) -> f#(proper x, proper y, proper z))
     (proper# f(x, y, z) -> proper# z, proper# f(x, y, z) -> proper# x)
     (proper# f(x, y, z) -> proper# z, proper# f(x, y, z) -> proper# y)
     (proper# f(x, y, z) -> proper# z, proper# f(x, y, z) -> proper# z)
     (f#(ok x, ok y, ok z) -> f#(x, y, z), f#(x, y, mark z) -> f#(x, y, z))
     (f#(ok x, ok y, ok z) -> f#(x, y, z), f#(ok x, ok y, ok z) -> f#(x, y, z))
     (proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> f#(proper x, proper y, proper z))
     (proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# x)
     (proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# y)
     (proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# z)
     (top# mark x -> proper# x, proper# f(x, y, z) -> f#(proper x, proper y, proper z))
     (top# mark x -> proper# x, proper# f(x, y, z) -> proper# x)
     (top# mark x -> proper# x, proper# f(x, y, z) -> proper# y)
     (top# mark x -> proper# x, proper# f(x, y, z) -> proper# z)
     (proper# f(x, y, z) -> f#(proper x, proper y, proper z), f#(x, y, mark z) -> f#(x, y, z))
     (proper# f(x, y, z) -> f#(proper x, proper y, proper z), f#(ok x, ok y, ok z) -> f#(x, y, z))
     (active# f(b(), c(), x) -> f#(x, x, x), f#(x, y, mark z) -> f#(x, y, z))
     (active# f(b(), c(), x) -> f#(x, x, x), f#(ok x, ok y, ok z) -> f#(x, y, z))}
    STATUS:
     arrows: 0.763314
     SCCS (4):
      Scc:
       {top# mark x -> top# proper x,
          top# ok x -> top# active x}
      Scc:
       {active# f(x, y, z) -> active# z}
      Scc:
       {proper# f(x, y, z) -> proper# x,
        proper# f(x, y, z) -> proper# y,
        proper# f(x, y, z) -> proper# z}
      Scc:
       {    f#(x, y, mark z) -> f#(x, y, z),
        f#(ok x, ok y, ok z) -> f#(x, y, z)}
      
      SCC (2):
       Strict:
        {top# mark x -> top# proper x,
           top# ok x -> top# active x}
       Weak:
       {      f(x, y, mark z) -> mark f(x, y, z),
          f(ok x, ok y, ok z) -> ok f(x, y, z),
            active f(x, y, z) -> f(x, y, active z),
        active f(b(), c(), x) -> mark f(x, x, x),
                   active d() -> mark c(),
                   active d() -> m b(),
            proper f(x, y, z) -> f(proper x, proper y, proper z),
                   proper b() -> ok b(),
                   proper c() -> ok c(),
                   proper d() -> ok d(),
                   top mark x -> top proper x,
                     top ok x -> top active x}
       Open
      
      SCC (1):
       Strict:
        {active# f(x, y, z) -> active# z}
       Weak:
       {      f(x, y, mark z) -> mark f(x, y, z),
          f(ok x, ok y, ok z) -> ok f(x, y, z),
            active f(x, y, z) -> f(x, y, active z),
        active f(b(), c(), x) -> mark f(x, x, x),
                   active d() -> mark c(),
                   active d() -> m b(),
            proper f(x, y, z) -> f(proper x, proper y, proper z),
                   proper b() -> ok b(),
                   proper c() -> ok c(),
                   proper d() -> ok d(),
                   top mark x -> top proper x,
                     top ok x -> top active x}
       Open
      
      SCC (3):
       Strict:
        {proper# f(x, y, z) -> proper# x,
         proper# f(x, y, z) -> proper# y,
         proper# f(x, y, z) -> proper# z}
       Weak:
       {      f(x, y, mark z) -> mark f(x, y, z),
          f(ok x, ok y, ok z) -> ok f(x, y, z),
            active f(x, y, z) -> f(x, y, active z),
        active f(b(), c(), x) -> mark f(x, x, x),
                   active d() -> mark c(),
                   active d() -> m b(),
            proper f(x, y, z) -> f(proper x, proper y, proper z),
                   proper b() -> ok b(),
                   proper c() -> ok c(),
                   proper d() -> ok d(),
                   top mark x -> top proper x,
                     top ok x -> top active x}
       Open
      
      
      
      SCC (2):
       Strict:
        {    f#(x, y, mark z) -> f#(x, y, z),
         f#(ok x, ok y, ok z) -> f#(x, y, z)}
       Weak:
       {      f(x, y, mark z) -> mark f(x, y, z),
          f(ok x, ok y, ok z) -> ok f(x, y, z),
            active f(x, y, z) -> f(x, y, active z),
        active f(b(), c(), x) -> mark f(x, x, x),
                   active d() -> mark c(),
                   active d() -> m b(),
            proper f(x, y, z) -> f(proper x, proper y, proper z),
                   proper b() -> ok b(),
                   proper c() -> ok c(),
                   proper d() -> ok d(),
                   top mark x -> top proper x,
                     top ok x -> top active x}
       Open