MAYBE
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:
  Strict:
   {     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())}
  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())))}
  EDG:
   {(mark#(f(X)) -> mark#(X), mark#(false()) -> active#(false()))
    (mark#(f(X)) -> mark#(X), mark#(true()) -> active#(true()))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> f#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(c()) -> active#(c()))
    (mark#(f(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), mark(X2), X3)))
    (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)) -> mark#(X2))
    (mark#(f(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (f#(active(X)) -> f#(X), f#(active(X)) -> f#(X))
    (f#(active(X)) -> f#(X), f#(mark(X)) -> f#(X))
    (active#(f(X)) -> if#(X, c(), f(true())), if#(active(X1), X2, X3) -> if#(X1, X2, X3))
    (active#(f(X)) -> if#(X, c(), f(true())), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), mark(X2), X3)), active#(f(X)) -> 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)) -> mark#(if(X, c(), f(true()))))
    (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#(if(true(), X, Y)) -> mark#(X))
    (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))
    (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))
    (mark#(if(X1, X2, X3)) -> if#(mark(X1), mark(X2), X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3))
    (mark#(if(X1, X2, X3)) -> if#(mark(X1), mark(X2), X3), if#(X1, X2, mark(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, 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#(X1, active(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, 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, X2, mark(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, 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#(X1, active(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, 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, X2, mark(X3)) -> if#(X1, X2, X3))
    (if#(active(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#(mark(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#(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, X2, active(X3)) -> if#(X1, X2, X3))
    (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3))
    (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))))
    (if#(mark(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, active(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, active(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#(active(X1), X2, 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, 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, mark(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#(mark(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, X2, mark(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, X2, active(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, active(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#(active(X1), X2, X3) -> if#(X1, X2, X3))
    (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()))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
    (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)) -> if#(mark(X1), mark(X2), X3))
    (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#(c()) -> active#(c()))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(f(X)) -> 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)) -> active#(f(mark(X))))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(true()) -> active#(true()))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(false()) -> active#(false()))
    (mark#(f(X)) -> f#(mark(X)), f#(mark(X)) -> f#(X))
    (mark#(f(X)) -> f#(mark(X)), f#(active(X)) -> f#(X))
    (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (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)) -> 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(true(), X, Y)) -> mark#(X), mark#(c()) -> active#(c()))
    (active#(if(true(), X, Y)) -> mark#(X), mark#(f(X)) -> 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)) -> active#(f(mark(X))))
    (active#(if(true(), X, Y)) -> mark#(X), mark#(true()) -> active#(true()))
    (active#(if(true(), X, Y)) -> mark#(X), mark#(false()) -> active#(false()))
    (f#(mark(X)) -> f#(X), f#(mark(X)) -> f#(X))
    (f#(mark(X)) -> f#(X), f#(active(X)) -> f#(X))
    (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()))}
   SCCS:
    Scc:
     {  f#(mark(X)) -> f#(X),
      f#(active(X)) -> f#(X)}
    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:
     {     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:
     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())))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(active(X)) -> f#(X)}
      EDG:
       {(f#(active(X)) -> f#(X), f#(active(X)) -> f#(X))}
       SCCS:
        Scc:
         {f#(active(X)) -> f#(X)}
        SCC:
         Strict:
          {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())))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed
    SCC:
     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())))}
     SPSC:
      Simple Projection:
       pi(if#) = 0
      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)}
      EDG:
       {(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#(X1, active(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, 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, X2, mark(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#(X1, active(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, 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, 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#(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, mark(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#(mark(X1), X2, 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, 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, mark(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#(mark(X1), X2, 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, 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, mark(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#(mark(X1), X2, X3) -> if#(X1, X2, X3))}
       SCCS:
        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)}
        SCC:
         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)}
         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())))}
         SPSC:
          Simple Projection:
           pi(if#) = 2
          Strict:
           {  if#(X1, X2, mark(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)}
          EDG:
           {(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, mark(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, 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, 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, X2, mark(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#(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#(mark(X1), X2, X3) -> if#(X1, X2, X3))}
           SCCS:
            Scc:
             {  if#(X1, X2, mark(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)}
            SCC:
             Strict:
              {  if#(X1, X2, mark(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)}
             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())))}
             SPSC:
              Simple Projection:
               pi(if#) = 0
              Strict:
               {  if#(X1, X2, mark(X3)) -> if#(X1, X2, X3),
                  if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
                if#(X1, active(X2), X3) -> if#(X1, X2, X3)}
              EDG:
               {(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, 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, 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, X2, mark(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#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3))}
               SCCS:
                Scc:
                 {  if#(X1, X2, mark(X3)) -> if#(X1, X2, X3),
                    if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
                  if#(X1, active(X2), X3) -> if#(X1, X2, X3)}
                SCC:
                 Strict:
                  {  if#(X1, X2, mark(X3)) -> if#(X1, X2, X3),
                     if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
                   if#(X1, active(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())))}
                 SPSC:
                  Simple Projection:
                   pi(if#) = 1
                  Strict:
                   {if#(X1, X2, mark(X3)) -> if#(X1, X2, X3),
                    if#(X1, mark(X2), X3) -> if#(X1, X2, X3)}
                  EDG:
                   {(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, mark(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, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))}
                   SCCS:
                    Scc:
                     {if#(X1, X2, mark(X3)) -> if#(X1, X2, X3),
                      if#(X1, mark(X2), X3) -> if#(X1, X2, X3)}
                    SCC:
                     Strict:
                      {if#(X1, X2, mark(X3)) -> if#(X1, X2, X3),
                       if#(X1, mark(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())))}
                     SPSC:
                      Simple Projection:
                       pi(if#) = 1
                      Strict:
                       {if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)}
                      EDG:
                       {(if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3))}
                       SCCS:
                        Scc:
                         {if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)}
                        SCC:
                         Strict:
                          {if#(X1, X2, mark(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())))}
                         SPSC:
                          Simple Projection:
                           pi(if#) = 2
                          Strict:
                           {}
                          Qed
    SCC:
     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())))}
     POLY:
      Argument Filtering:
       pi(false) = [], pi(active#) = 0, pi(active) = 0, pi(true) = [], pi(f) = 0, pi(c) = [], pi(if) = [0,1,2], pi(mark#) = 0, pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [if](x0, x1, x2) = x0 + x1 + x2,
       [false] = 1,
       [true] = 0,
       [c] = 0
      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#(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())))}
      EDG:
       {(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#(if(true(), X, Y)) -> mark#(X))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(f(X)) -> mark#(X))
        (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#(if(X1, X2, X3)) -> mark#(X2))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
        (active#(if(true(), X, Y)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
        (active#(if(true(), X, Y)) -> mark#(X), mark#(f(X)) -> mark#(X))
        (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)) -> mark#(X2))
        (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
        (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)) -> 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)) -> active#(f(mark(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)) -> active#(if(mark(X1), mark(X2), X3)))
        (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
        (mark#(f(X)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
        (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)) -> active#(if(mark(X1), mark(X2), X3)))
        (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(f(X)) -> mark#(X))
        (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(f(X)) -> active#(f(mark(X))), active#(if(true(), X, Y)) -> mark#(X))
        (mark#(f(X)) -> active#(f(mark(X))), active#(f(X)) -> mark#(if(X, c(), f(true()))))}
       SCCS:
        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#(f(X)) -> mark#(if(X, c(), f(true())))}
        SCC:
         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#(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())))}
         POLY:
          Argument Filtering:
           pi(false) = [], pi(active#) = [0], pi(active) = 0, pi(true) = [], pi(f) = [0], pi(c) = [], pi(if) = [0,1,2], pi(mark#) = [0], pi(mark) = 0
          Usable Rules:
           {}
          Interpretation:
           [active#](x0) = x0 + 1,
           [mark#](x0) = x0 + 1,
           [if](x0, x1, x2) = x0 + x1 + x2,
           [f](x0) = x0 + 1,
           [true] = 0,
           [c] = 0
          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)) -> active#(f(mark(X))),
            active#(if(true(), X, Y)) -> mark#(X),
                        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())))}
          EDG:
           {(active#(f(X)) -> mark#(if(X, c(), f(true()))), mark#(f(X)) -> active#(f(mark(X))))
            (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#(if(X1, X2, X3)) -> mark#(X2))
            (active#(f(X)) -> mark#(if(X, c(), f(true()))), mark#(if(X1, X2, X3)) -> mark#(X1))
            (active#(if(true(), X, Y)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
            (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)) -> mark#(X2))
            (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
            (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#(if(true(), X, Y)) -> mark#(X))
            (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
            (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)) -> active#(if(mark(X1), mark(X2), X3)))
            (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(f(X)) -> active#(f(mark(X))))
            (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)) -> active#(if(mark(X1), mark(X2), X3)))
            (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(f(X)) -> active#(f(mark(X))))
            (mark#(f(X)) -> active#(f(mark(X))), active#(if(true(), X, Y)) -> mark#(X))
            (mark#(f(X)) -> active#(f(mark(X))), active#(f(X)) -> mark#(if(X, c(), f(true()))))}
           SCCS:
            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)) -> active#(f(mark(X))),
              active#(if(true(), X, Y)) -> mark#(X),
                          active#(f(X)) -> mark#(if(X, c(), f(true())))}
            SCC:
             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)) -> active#(f(mark(X))),
               active#(if(true(), X, Y)) -> mark#(X),
                           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())))}
             Fail