MAYBE
Time: 0.015045
TRS:
 {    f(X1, X2, mark X3) -> mark f(X1, X2, X3),
      f(mark X1, X2, X3) -> mark f(X1, X2, X3),
  f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
    active f(X1, X2, X3) -> f(X1, X2, active X3),
    active f(X1, X2, X3) -> f(active X1, X2, X3),
   active f(a(), b(), X) -> mark f(X, X, X),
              active c() -> mark a(),
              active c() -> mark b(),
    proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
              proper a() -> ok a(),
              proper b() -> ok b(),
              proper c() -> ok c(),
              top mark X -> top proper X,
                top ok X -> top active X}
 DP:
  DP:
   {    f#(X1, X2, mark X3) -> f#(X1, X2, X3),
        f#(mark X1, X2, X3) -> f#(X1, X2, X3),
    f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3),
      active# f(X1, X2, X3) -> f#(X1, X2, active X3),
      active# f(X1, X2, X3) -> f#(active X1, X2, X3),
      active# f(X1, X2, X3) -> active# X1,
      active# f(X1, X2, X3) -> active# X3,
     active# f(a(), b(), X) -> f#(X, X, X),
      proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3),
      proper# f(X1, X2, X3) -> proper# X1,
      proper# f(X1, X2, X3) -> proper# X2,
      proper# f(X1, X2, X3) -> proper# X3,
                top# mark X -> proper# X,
                top# mark X -> top# proper X,
                  top# ok X -> active# X,
                  top# ok X -> top# active X}
  TRS:
  {    f(X1, X2, mark X3) -> mark f(X1, X2, X3),
       f(mark X1, X2, X3) -> mark f(X1, X2, X3),
   f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
     active f(X1, X2, X3) -> f(X1, X2, active X3),
     active f(X1, X2, X3) -> f(active X1, X2, X3),
    active f(a(), b(), X) -> mark f(X, X, X),
               active c() -> mark a(),
               active c() -> mark b(),
     proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
               proper a() -> ok a(),
               proper b() -> ok b(),
               proper c() -> ok c(),
               top mark X -> top proper X,
                 top ok X -> top active X}
  EDG:
   {(top# ok X -> active# X, active# f(a(), b(), X) -> f#(X, X, X))
    (top# ok X -> active# X, active# f(X1, X2, X3) -> active# X3)
    (top# ok X -> active# X, active# f(X1, X2, X3) -> active# X1)
    (top# ok X -> active# X, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
    (top# ok X -> active# X, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
    (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)
    (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (active# f(X1, X2, X3) -> active# X1, active# f(a(), b(), X) -> f#(X, X, X))
    (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> active# X3)
    (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> active# X1)
    (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
    (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
    (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3)
    (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X2)
    (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X1)
    (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X3)
    (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X2)
    (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X1)
    (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
    (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
    (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> active# X1)
    (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> active# X3)
    (active# f(X1, X2, X3) -> active# X3, active# f(a(), b(), X) -> f#(X, X, X))
    (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X1)
    (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2)
    (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X3)
    (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (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)
    (active# f(a(), b(), X) -> f#(X, X, X), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (active# f(a(), b(), X) -> f#(X, X, X), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (active# f(a(), b(), X) -> f#(X, X, X), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (top# mark X -> proper# X, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X1)
    (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X2)
    (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X3)}
   EDG:
    {(top# ok X -> active# X, active# f(a(), b(), X) -> f#(X, X, X))
     (top# ok X -> active# X, active# f(X1, X2, X3) -> active# X3)
     (top# ok X -> active# X, active# f(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
     (top# ok X -> active# X, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
     (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)
     (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (active# f(X1, X2, X3) -> active# X1, active# f(a(), b(), X) -> f#(X, X, X))
     (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> active# X3)
     (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> active# X1)
     (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
     (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
     (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3)
     (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X2)
     (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X1)
     (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
     (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X3)
     (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X2)
     (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X1)
     (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
     (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
     (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
     (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> active# X1)
     (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> active# X3)
     (active# f(X1, X2, X3) -> active# X3, active# f(a(), b(), X) -> f#(X, X, X))
     (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
     (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X1)
     (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2)
     (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X3)
     (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (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)
     (active# f(a(), b(), X) -> f#(X, X, X), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
     (top# mark X -> proper# X, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X3)}
    EDG:
     {(top# ok X -> active# X, active# f(a(), b(), X) -> f#(X, X, X))
      (top# ok X -> active# X, active# f(X1, X2, X3) -> active# X3)
      (top# ok X -> active# X, active# f(X1, X2, X3) -> active# X1)
      (top# ok X -> active# X, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
      (top# ok X -> active# X, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
      (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)
      (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
      (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
      (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
      (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
      (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
      (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
      (active# f(X1, X2, X3) -> active# X1, active# f(a(), b(), X) -> f#(X, X, X))
      (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> active# X3)
      (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> active# X1)
      (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
      (active# f(X1, X2, X3) -> active# X1, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
      (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
      (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
      (active# f(X1, X2, X3) -> f#(X1, X2, active X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
      (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3)
      (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X2)
      (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X1)
      (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
      (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X3)
      (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X2)
      (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X1)
      (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
      (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> f#(X1, X2, active X3))
      (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> f#(active X1, X2, X3))
      (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> active# X1)
      (active# f(X1, X2, X3) -> active# X3, active# f(X1, X2, X3) -> active# X3)
      (active# f(X1, X2, X3) -> active# X3, active# f(a(), b(), X) -> f#(X, X, X))
      (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
      (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
      (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
      (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
      (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X1)
      (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2)
      (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X3)
      (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
      (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
      (active# f(X1, X2, X3) -> f#(active X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
      (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
      (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
      (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
      (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)
      (active# f(a(), b(), X) -> f#(X, X, X), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
      (active# f(a(), b(), X) -> f#(X, X, X), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
      (active# f(a(), b(), X) -> f#(X, X, X), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
      (top# mark X -> proper# X, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
      (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X1)
      (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X2)
      (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X3)}
     STATUS:
      arrows: 0.765625
      SCCS (4):
       Scc:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Scc:
        {active# f(X1, X2, X3) -> active# X1,
         active# f(X1, X2, X3) -> active# X3}
       Scc:
        {proper# f(X1, X2, X3) -> proper# X1,
         proper# f(X1, X2, X3) -> proper# X2,
         proper# f(X1, X2, X3) -> proper# X3}
       Scc:
        {    f#(X1, X2, mark X3) -> f#(X1, X2, X3),
             f#(mark X1, X2, X3) -> f#(X1, X2, X3),
         f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)}
       
       SCC (2):
        Strict:
         {top# mark X -> top# proper X,
            top# ok X -> top# active X}
        Weak:
        {    f(X1, X2, mark X3) -> mark f(X1, X2, X3),
             f(mark X1, X2, X3) -> mark f(X1, X2, X3),
         f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
           active f(X1, X2, X3) -> f(X1, X2, active X3),
           active f(X1, X2, X3) -> f(active X1, X2, X3),
          active f(a(), b(), X) -> mark f(X, X, X),
                     active c() -> mark a(),
                     active c() -> mark b(),
           proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                     proper a() -> ok a(),
                     proper b() -> ok b(),
                     proper c() -> ok c(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
        Open
       
       SCC (2):
        Strict:
         {active# f(X1, X2, X3) -> active# X1,
          active# f(X1, X2, X3) -> active# X3}
        Weak:
        {    f(X1, X2, mark X3) -> mark f(X1, X2, X3),
             f(mark X1, X2, X3) -> mark f(X1, X2, X3),
         f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
           active f(X1, X2, X3) -> f(X1, X2, active X3),
           active f(X1, X2, X3) -> f(active X1, X2, X3),
          active f(a(), b(), X) -> mark f(X, X, X),
                     active c() -> mark a(),
                     active c() -> mark b(),
           proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                     proper a() -> ok a(),
                     proper b() -> ok b(),
                     proper c() -> ok c(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
        Open
       
       
       
       
       SCC (3):
        Strict:
         {proper# f(X1, X2, X3) -> proper# X1,
          proper# f(X1, X2, X3) -> proper# X2,
          proper# f(X1, X2, X3) -> proper# X3}
        Weak:
        {    f(X1, X2, mark X3) -> mark f(X1, X2, X3),
             f(mark X1, X2, X3) -> mark f(X1, X2, X3),
         f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
           active f(X1, X2, X3) -> f(X1, X2, active X3),
           active f(X1, X2, X3) -> f(active X1, X2, X3),
          active f(a(), b(), X) -> mark f(X, X, X),
                     active c() -> mark a(),
                     active c() -> mark b(),
           proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                     proper a() -> ok a(),
                     proper b() -> ok b(),
                     proper c() -> ok c(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
        Open
       
       SCC (3):
        Strict:
         {    f#(X1, X2, mark X3) -> f#(X1, X2, X3),
              f#(mark X1, X2, X3) -> f#(X1, X2, X3),
          f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)}
        Weak:
        {    f(X1, X2, mark X3) -> mark f(X1, X2, X3),
             f(mark X1, X2, X3) -> mark f(X1, X2, X3),
         f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
           active f(X1, X2, X3) -> f(X1, X2, active X3),
           active f(X1, X2, X3) -> f(active X1, X2, X3),
          active f(a(), b(), X) -> mark f(X, X, X),
                     active c() -> mark a(),
                     active c() -> mark b(),
           proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                     proper a() -> ok a(),
                     proper b() -> ok b(),
                     proper c() -> ok c(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
        Open