MAYBE
Time: 0.013781
TRS:
 {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
       if(mark X1, X2, X3) -> mark if(X1, X2, X3),
   if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                  f mark X -> mark f X,
                    f ok X -> ok f X,
     active if(X1, X2, X3) -> if(X1, active X2, X3),
     active if(X1, X2, X3) -> if(active X1, X2, X3),
   active if(true(), X, Y) -> mark X,
  active if(false(), X, Y) -> mark Y,
                active f X -> mark if(X, c(), f true()),
                active f X -> f active X,
     proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                proper c() -> ok c(),
                proper f X -> f proper X,
             proper true() -> ok true(),
            proper false() -> ok false(),
                top mark X -> top proper X,
                  top ok X -> top active X}
 DP:
  DP:
   {    if#(X1, mark X2, X3) -> if#(X1, X2, X3),
        if#(mark X1, X2, X3) -> if#(X1, X2, X3),
    if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3),
                   f# mark X -> f# X,
                     f# ok X -> f# X,
      active# if(X1, X2, X3) -> if#(X1, active X2, X3),
      active# if(X1, X2, X3) -> if#(active X1, X2, X3),
      active# if(X1, X2, X3) -> active# X1,
      active# if(X1, X2, X3) -> active# X2,
                 active# f X -> if#(X, c(), f true()),
                 active# f X -> f# true(),
                 active# f X -> f# active X,
                 active# f X -> active# X,
      proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3),
      proper# if(X1, X2, X3) -> proper# X1,
      proper# if(X1, X2, X3) -> proper# X2,
      proper# if(X1, X2, X3) -> proper# X3,
                 proper# f X -> f# proper X,
                 proper# f 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:
  {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
        if(mark X1, X2, X3) -> mark if(X1, X2, X3),
    if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                   f mark X -> mark f X,
                     f ok X -> ok f X,
      active if(X1, X2, X3) -> if(X1, active X2, X3),
      active if(X1, X2, X3) -> if(active X1, X2, X3),
    active if(true(), X, Y) -> mark X,
   active if(false(), X, Y) -> mark Y,
                 active f X -> mark if(X, c(), f true()),
                 active f X -> f active X,
      proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                 proper c() -> ok c(),
                 proper f X -> f proper X,
              proper true() -> ok true(),
             proper false() -> ok false(),
                 top mark X -> top proper X,
                   top ok X -> top active X}
  UR:
   {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
         if(mark X1, X2, X3) -> mark if(X1, X2, X3),
     if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                    f mark X -> mark f X,
                      f ok X -> ok f X,
       active if(X1, X2, X3) -> if(X1, active X2, X3),
       active if(X1, X2, X3) -> if(active X1, X2, X3),
     active if(true(), X, Y) -> mark X,
    active if(false(), X, Y) -> mark Y,
                  active f X -> mark if(X, c(), f true()),
                  active f X -> f active X,
       proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                  proper c() -> ok c(),
                  proper f X -> f proper X,
               proper true() -> ok true(),
              proper false() -> ok false()}
   EDG:
    {(active# f X -> if#(X, c(), f true()), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (active# f X -> if#(X, c(), f true()), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# f X -> if#(X, c(), f true()), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (proper# f X -> f# proper X, f# ok X -> f# X)
     (proper# f X -> f# proper X, f# mark X -> f# 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)
     (proper# if(X1, X2, X3) -> proper# X3, proper# f X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# f X -> f# proper X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X3)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> active# X1, active# f X -> active# X)
     (active# if(X1, X2, X3) -> active# X1, active# f X -> f# active X)
     (active# if(X1, X2, X3) -> active# X1, active# f X -> f# true())
     (active# if(X1, X2, X3) -> active# X1, active# f X -> if#(X, c(), f true()))
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X2)
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X1)
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(X1, active X2, X3))
     (f# mark X -> f# X, f# ok X -> f# X)
     (f# mark X -> f# X, f# mark X -> f# X)
     (active# f X -> active# X, active# f X -> active# X)
     (active# f X -> active# X, active# f X -> f# active X)
     (active# f X -> active# X, active# f X -> f# true())
     (active# f X -> active# X, active# f X -> if#(X, c(), f true()))
     (active# f X -> active# X, active# if(X1, X2, X3) -> active# X2)
     (active# f X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (active# f X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# f X -> active# X, active# if(X1, X2, X3) -> if#(X1, active X2, X3))
     (top# mark X -> proper# X, proper# f X -> proper# X)
     (top# mark X -> proper# X, proper# f X -> f# proper X)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (active# if(X1, X2, X3) -> active# X2, active# f X -> active# X)
     (active# if(X1, X2, X3) -> active# X2, active# f X -> f# active X)
     (active# if(X1, X2, X3) -> active# X2, active# f X -> f# true())
     (active# if(X1, X2, X3) -> active# X2, active# f X -> if#(X, c(), f true()))
     (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> active# X2)
     (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> active# X1)
     (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> if#(X1, active X2, X3))
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
     (proper# if(X1, X2, X3) -> proper# X2, proper# f X -> f# proper X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# f X -> proper# X)
     (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(X1, active X2, X3))
     (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X2)
     (top# ok X -> active# X, active# f X -> if#(X, c(), f true()))
     (top# ok X -> active# X, active# f X -> f# true())
     (top# ok X -> active# X, active# f X -> f# active X)
     (top# ok X -> active# X, active# f X -> active# X)
     (proper# f X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (proper# f X -> proper# X, proper# f X -> f# proper X)
     (proper# f X -> proper# X, proper# f X -> proper# X)
     (f# ok X -> f# X, f# mark X -> f# X)
     (f# ok X -> f# X, f# ok X -> f# X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
     (proper# if(X1, X2, X3) -> proper# X1, proper# f X -> f# proper X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# f X -> proper# X)
     (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (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# f X -> f# active X, f# mark X -> f# X)
     (active# f X -> f# active X, f# ok X -> f# X)
     (active# f X -> f# true(), f# mark X -> f# X)
     (active# f X -> f# true(), f# ok X -> f# X)}
    STATUS:
     arrows: 0.809074
     SCCS (5):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {active# if(X1, X2, X3) -> active# X1,
        active# if(X1, X2, X3) -> active# X2,
                   active# f X -> active# X}
      Scc:
       {proper# if(X1, X2, X3) -> proper# X1,
        proper# if(X1, X2, X3) -> proper# X2,
        proper# if(X1, X2, X3) -> proper# X3,
                   proper# f X -> proper# X}
      Scc:
       {    if#(X1, mark X2, X3) -> if#(X1, X2, X3),
            if#(mark X1, X2, X3) -> if#(X1, X2, X3),
        if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)}
      Scc:
       {f# mark X -> f# X,
          f# ok X -> f# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                        f mark X -> mark f X,
                          f ok X -> ok f X,
           active if(X1, X2, X3) -> if(X1, active X2, X3),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true()),
                      active f X -> f active X,
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      proper c() -> ok c(),
                      proper f X -> f proper X,
                   proper true() -> ok true(),
                  proper false() -> ok false(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        {active# if(X1, X2, X3) -> active# X1,
         active# if(X1, X2, X3) -> active# X2,
                    active# f X -> active# X}
       Weak:
       {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                        f mark X -> mark f X,
                          f ok X -> ok f X,
           active if(X1, X2, X3) -> if(X1, active X2, X3),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true()),
                      active f X -> f active X,
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      proper c() -> ok c(),
                      proper f X -> f proper X,
                   proper true() -> ok true(),
                  proper false() -> ok false(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      
      SCC (4):
       Strict:
        {proper# if(X1, X2, X3) -> proper# X1,
         proper# if(X1, X2, X3) -> proper# X2,
         proper# if(X1, X2, X3) -> proper# X3,
                    proper# f X -> proper# X}
       Weak:
       {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                        f mark X -> mark f X,
                          f ok X -> ok f X,
           active if(X1, X2, X3) -> if(X1, active X2, X3),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true()),
                      active f X -> f active X,
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      proper c() -> ok c(),
                      proper f X -> f proper X,
                   proper true() -> ok true(),
                  proper false() -> ok false(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      
      
      SCC (3):
       Strict:
        {    if#(X1, mark X2, X3) -> if#(X1, X2, X3),
             if#(mark X1, X2, X3) -> if#(X1, X2, X3),
         if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)}
       Weak:
       {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                        f mark X -> mark f X,
                          f ok X -> ok f X,
           active if(X1, X2, X3) -> if(X1, active X2, X3),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true()),
                      active f X -> f active X,
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      proper c() -> ok c(),
                      proper f X -> f proper X,
                   proper true() -> ok true(),
                  proper false() -> ok false(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {f# mark X -> f# X,
           f# ok X -> f# X}
       Weak:
       {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                        f mark X -> mark f X,
                          f ok X -> ok f X,
           active if(X1, X2, X3) -> if(X1, active X2, X3),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true()),
                      active f X -> f active X,
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      proper c() -> ok c(),
                      proper f X -> f proper X,
                   proper true() -> ok true(),
                  proper false() -> ok false(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open