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