MAYBE
Time: 0.022973
TRS:
 {     mark if(X1, X2, X3) -> active if(mark X1, mark X2, X3),
                  mark c() -> active c(),
                  mark f X -> active f mark X,
               mark true() -> active true(),
              mark false() -> active false(),
       if(X1, X2, mark X3) -> if(X1, X2, X3),
     if(X1, X2, active X3) -> if(X1, X2, X3),
       if(X1, mark X2, X3) -> if(X1, X2, X3),
     if(X1, active X2, X3) -> if(X1, X2, X3),
       if(mark X1, X2, X3) -> if(X1, X2, X3),
     if(active X1, X2, X3) -> if(X1, X2, X3),
                  f mark X -> f X,
                f active X -> f X,
   active if(true(), X, Y) -> mark X,
  active if(false(), X, Y) -> mark Y,
                active f X -> mark if(X, c(), f true())}
 DP:
  DP:
   {     mark# if(X1, X2, X3) -> mark# X1,
         mark# if(X1, X2, X3) -> mark# X2,
         mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3),
         mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3),
                    mark# c() -> active# c(),
                    mark# f X -> mark# X,
                    mark# f X -> f# mark X,
                    mark# f X -> active# f mark X,
                 mark# true() -> active# true(),
                mark# false() -> active# false(),
         if#(X1, X2, mark X3) -> if#(X1, X2, X3),
       if#(X1, X2, active X3) -> if#(X1, X2, X3),
         if#(X1, mark X2, X3) -> if#(X1, X2, X3),
       if#(X1, active X2, X3) -> if#(X1, X2, X3),
         if#(mark X1, X2, X3) -> if#(X1, X2, X3),
       if#(active X1, X2, X3) -> if#(X1, X2, X3),
                    f# mark X -> f# X,
                  f# active X -> f# X,
     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 -> if#(X, c(), f true()),
                  active# f X -> f# true()}
  TRS:
  {     mark if(X1, X2, X3) -> active if(mark X1, mark X2, X3),
                   mark c() -> active c(),
                   mark f X -> active f mark X,
                mark true() -> active true(),
               mark false() -> active false(),
        if(X1, X2, mark X3) -> if(X1, X2, X3),
      if(X1, X2, active X3) -> if(X1, X2, X3),
        if(X1, mark X2, X3) -> if(X1, X2, X3),
      if(X1, active X2, X3) -> if(X1, X2, X3),
        if(mark X1, X2, X3) -> if(X1, X2, X3),
      if(active X1, X2, X3) -> if(X1, X2, X3),
                   f mark X -> f X,
                 f active X -> f X,
    active if(true(), X, Y) -> mark X,
   active if(false(), X, Y) -> mark Y,
                 active f X -> mark if(X, c(), f true())}
  UR:
   {     mark if(X1, X2, X3) -> active if(mark X1, mark X2, X3),
                    mark c() -> active c(),
                    mark f X -> active f mark X,
                 mark true() -> active true(),
                mark false() -> active false(),
         if(X1, X2, mark X3) -> if(X1, X2, X3),
       if(X1, X2, active X3) -> if(X1, X2, X3),
         if(X1, mark X2, X3) -> if(X1, X2, X3),
       if(X1, active X2, X3) -> if(X1, X2, X3),
         if(mark X1, X2, X3) -> if(X1, X2, X3),
       if(active X1, X2, X3) -> if(X1, X2, X3),
                    f mark X -> f X,
                  f active X -> f X,
     active if(true(), X, Y) -> mark X,
    active if(false(), X, Y) -> mark Y,
                  active f X -> mark if(X, c(), f true())}
   EDG:
    {(mark# f X -> f# mark X, f# active X -> f# X)
     (mark# f X -> f# mark X, f# mark X -> f# X)
     (mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(active 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#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active 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#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active 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#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active 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#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (mark# f X -> active# f mark X, active# f X -> f# true())
     (mark# f X -> active# f mark X, active# f X -> if#(X, c(), f true()))
     (mark# f X -> active# f mark X, active# f X -> mark# if(X, c(), f true()))
     (mark# f X -> active# f mark X, active# if(false(), X, Y) -> mark# Y)
     (mark# f X -> active# f mark X, active# if(true(), X, Y) -> mark# X)
     (f# mark X -> f# X, f# active X -> f# X)
     (f# mark X -> f# X, f# mark X -> f# X)
     (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false())
     (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true())
     (active# if(true(), X, Y) -> mark# X, mark# f X -> active# f mark X)
     (active# if(true(), X, Y) -> mark# X, mark# f X -> f# mark X)
     (active# if(true(), X, Y) -> mark# X, mark# f X -> mark# X)
     (active# if(true(), X, Y) -> mark# X, mark# c() -> active# c())
     (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3))
     (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3))
     (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X2)
     (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# if(X1, X2, X3) -> mark# X2, mark# false() -> active# false())
     (mark# if(X1, X2, X3) -> mark# X2, mark# true() -> active# true())
     (mark# if(X1, X2, X3) -> mark# X2, mark# f X -> active# f mark X)
     (mark# if(X1, X2, X3) -> mark# X2, mark# f X -> f# mark X)
     (mark# if(X1, X2, X3) -> mark# X2, mark# f X -> mark# X)
     (mark# if(X1, X2, X3) -> mark# X2, mark# c() -> active# c())
     (mark# if(X1, X2, X3) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3))
     (mark# if(X1, X2, X3) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3))
     (mark# if(X1, X2, X3) -> mark# X2, mark# if(X1, X2, X3) -> mark# X2)
     (mark# if(X1, X2, X3) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
     (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
     (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X2)
     (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3))
     (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3))
     (active# if(false(), X, Y) -> mark# Y, mark# c() -> active# c())
     (active# if(false(), X, Y) -> mark# Y, mark# f X -> mark# X)
     (active# if(false(), X, Y) -> mark# Y, mark# f X -> f# mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# f X -> active# f mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true())
     (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false())
     (active# f X -> mark# if(X, c(), f true()), mark# if(X1, X2, X3) -> mark# X1)
     (active# f X -> mark# if(X, c(), f true()), mark# if(X1, X2, X3) -> mark# X2)
     (active# f X -> mark# if(X, c(), f true()), mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3))
     (active# f X -> mark# if(X, c(), f true()), mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3))
     (active# f X -> mark# if(X, c(), f true()), mark# f X -> mark# X)
     (active# f X -> mark# if(X, c(), f true()), mark# f X -> f# mark X)
     (active# f X -> mark# if(X, c(), f true()), mark# f X -> active# f mark X)
     (f# active X -> f# X, f# mark X -> f# X)
     (f# active X -> f# X, f# active X -> f# X)
     (mark# f X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# f X -> mark# X, mark# if(X1, X2, X3) -> mark# X2)
     (mark# f X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3))
     (mark# f X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3))
     (mark# f X -> mark# X, mark# c() -> active# c())
     (mark# f X -> mark# X, mark# f X -> mark# X)
     (mark# f X -> mark# X, mark# f X -> f# mark X)
     (mark# f X -> mark# X, mark# f X -> active# f mark X)
     (mark# f X -> mark# X, mark# true() -> active# true())
     (mark# f X -> mark# X, mark# false() -> active# false())
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
     (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X2)
     (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, mark X2, X3))
     (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3))
     (mark# if(X1, X2, X3) -> mark# X1, mark# c() -> active# c())
     (mark# if(X1, X2, X3) -> mark# X1, mark# f X -> mark# X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# f X -> f# mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# f X -> active# f mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true())
     (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false())
     (mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3), active# if(true(), X, Y) -> mark# X)
     (mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3), active# if(false(), X, Y) -> mark# Y)
     (mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3), active# f X -> mark# if(X, c(), f true()))
     (mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3), active# f X -> if#(X, c(), f true()))
     (mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3), active# f X -> f# true())}
    STATUS:
     arrows: 0.786389
     SCCS (3):
      Scc:
       {     mark# if(X1, X2, X3) -> mark# X1,
             mark# if(X1, X2, X3) -> mark# X2,
             mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3),
                        mark# f X -> mark# X,
                        mark# f X -> active# f mark X,
         active# if(true(), X, Y) -> mark# X,
        active# if(false(), X, Y) -> mark# Y,
                      active# f X -> mark# if(X, c(), f true())}
      Scc:
       {  if#(X1, X2, mark X3) -> if#(X1, X2, X3),
        if#(X1, X2, active X3) -> if#(X1, X2, X3),
          if#(X1, mark X2, X3) -> if#(X1, X2, X3),
        if#(X1, active X2, X3) -> if#(X1, X2, X3),
          if#(mark X1, X2, X3) -> if#(X1, X2, X3),
        if#(active X1, X2, X3) -> if#(X1, X2, X3)}
      Scc:
       {  f# mark X -> f# X,
        f# active X -> f# X}
      
      SCC (8):
       Strict:
        {     mark# if(X1, X2, X3) -> mark# X1,
              mark# if(X1, X2, X3) -> mark# X2,
              mark# if(X1, X2, X3) -> active# if(mark X1, mark X2, X3),
                         mark# f X -> mark# X,
                         mark# f X -> active# f mark X,
          active# if(true(), X, Y) -> mark# X,
         active# if(false(), X, Y) -> mark# Y,
                       active# f X -> mark# if(X, c(), f true())}
       Weak:
       {     mark if(X1, X2, X3) -> active if(mark X1, mark X2, X3),
                        mark c() -> active c(),
                        mark f X -> active f mark X,
                     mark true() -> active true(),
                    mark false() -> active false(),
             if(X1, X2, mark X3) -> if(X1, X2, X3),
           if(X1, X2, active X3) -> if(X1, X2, X3),
             if(X1, mark X2, X3) -> if(X1, X2, X3),
           if(X1, active X2, X3) -> if(X1, X2, X3),
             if(mark X1, X2, X3) -> if(X1, X2, X3),
           if(active X1, X2, X3) -> if(X1, X2, X3),
                        f mark X -> f X,
                      f active X -> f X,
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true())}
       Open
      
      SCC (6):
       Strict:
        {  if#(X1, X2, mark X3) -> if#(X1, X2, X3),
         if#(X1, X2, active X3) -> if#(X1, X2, X3),
           if#(X1, mark X2, X3) -> if#(X1, X2, X3),
         if#(X1, active X2, X3) -> if#(X1, X2, X3),
           if#(mark X1, X2, X3) -> if#(X1, X2, X3),
         if#(active X1, X2, X3) -> if#(X1, X2, X3)}
       Weak:
       {     mark if(X1, X2, X3) -> active if(mark X1, mark X2, X3),
                        mark c() -> active c(),
                        mark f X -> active f mark X,
                     mark true() -> active true(),
                    mark false() -> active false(),
             if(X1, X2, mark X3) -> if(X1, X2, X3),
           if(X1, X2, active X3) -> if(X1, X2, X3),
             if(X1, mark X2, X3) -> if(X1, X2, X3),
           if(X1, active X2, X3) -> if(X1, X2, X3),
             if(mark X1, X2, X3) -> if(X1, X2, X3),
           if(active X1, X2, X3) -> if(X1, X2, X3),
                        f mark X -> f X,
                      f active X -> f X,
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true())}
       Open
      
      SCC (2):
       Strict:
        {  f# mark X -> f# X,
         f# active X -> f# X}
       Weak:
       {     mark if(X1, X2, X3) -> active if(mark X1, mark X2, X3),
                        mark c() -> active c(),
                        mark f X -> active f mark X,
                     mark true() -> active true(),
                    mark false() -> active false(),
             if(X1, X2, mark X3) -> if(X1, X2, X3),
           if(X1, X2, active X3) -> if(X1, X2, X3),
             if(X1, mark X2, X3) -> if(X1, X2, X3),
           if(X1, active X2, X3) -> if(X1, X2, X3),
             if(mark X1, X2, X3) -> if(X1, X2, X3),
           if(active X1, X2, X3) -> if(X1, X2, X3),
                        f mark X -> f X,
                      f active X -> f X,
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true())}
       Open