MAYBE
Time: 0.205627
TRS:
 {             mark and(X1, X2) -> active and(mark X1, X2),
                    mark true() -> active true(),
                   mark false() -> active false(),
            mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
               mark add(X1, X2) -> active add(mark X1, X2),
                       mark 0() -> active 0(),
                       mark s X -> active s X,
                     mark nil() -> active nil(),
             mark first(X1, X2) -> active first(mark X1, mark X2),
              mark cons(X1, X2) -> active cons(X1, X2),
                    mark from X -> active from X,
          active and(true(), X) -> mark X,
         active and(false(), Y) -> mark false(),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
             active add(0(), X) -> mark X,
             active add(s X, Y) -> mark s add(X, Y),
           active first(0(), X) -> mark nil(),
  active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                  active from X -> mark cons(X, from s X),
               and(X1, mark X2) -> and(X1, X2),
             and(X1, active X2) -> and(X1, X2),
               and(mark X1, X2) -> and(X1, X2),
             and(active X1, X2) -> and(X1, X2),
            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),
               add(X1, mark X2) -> add(X1, X2),
             add(X1, active X2) -> add(X1, X2),
               add(mark X1, X2) -> add(X1, X2),
             add(active X1, X2) -> add(X1, X2),
                       s mark X -> s X,
                     s active X -> s X,
             first(X1, mark X2) -> first(X1, X2),
           first(X1, active X2) -> first(X1, X2),
             first(mark X1, X2) -> first(X1, X2),
           first(active X1, X2) -> first(X1, X2),
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                    from mark X -> from X,
                  from active X -> from X}
 DP:
  DP:
   {             mark# and(X1, X2) -> mark# X1,
                 mark# and(X1, X2) -> active# and(mark X1, X2),
                 mark# and(X1, X2) -> and#(mark X1, X2),
                      mark# true() -> active# true(),
                     mark# false() -> active# false(),
              mark# if(X1, X2, X3) -> mark# X1,
              mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3),
              mark# if(X1, X2, X3) -> if#(mark X1, X2, X3),
                 mark# add(X1, X2) -> mark# X1,
                 mark# add(X1, X2) -> active# add(mark X1, X2),
                 mark# add(X1, X2) -> add#(mark X1, X2),
                         mark# 0() -> active# 0(),
                         mark# s X -> active# s X,
                       mark# nil() -> active# nil(),
               mark# first(X1, X2) -> mark# X1,
               mark# first(X1, X2) -> mark# X2,
               mark# first(X1, X2) -> active# first(mark X1, mark X2),
               mark# first(X1, X2) -> first#(mark X1, mark X2),
                mark# cons(X1, X2) -> active# cons(X1, X2),
                      mark# from X -> active# from X,
            active# and(true(), X) -> mark# X,
           active# and(false(), Y) -> mark# false(),
          active# if(true(), X, Y) -> mark# X,
         active# if(false(), X, Y) -> mark# Y,
               active# add(0(), X) -> mark# X,
               active# add(s X, Y) -> mark# s add(X, Y),
               active# add(s X, Y) -> add#(X, Y),
               active# add(s X, Y) -> s# add(X, Y),
             active# first(0(), X) -> mark# nil(),
    active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)),
    active# first(s X, cons(Y, Z)) -> first#(X, Z),
    active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)),
                    active# from X -> mark# cons(X, from s X),
                    active# from X -> s# X,
                    active# from X -> cons#(X, from s X),
                    active# from X -> from# s X,
                 and#(X1, mark X2) -> and#(X1, X2),
               and#(X1, active X2) -> and#(X1, X2),
                 and#(mark X1, X2) -> and#(X1, X2),
               and#(active X1, X2) -> and#(X1, X2),
              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),
                 add#(X1, mark X2) -> add#(X1, X2),
               add#(X1, active X2) -> add#(X1, X2),
                 add#(mark X1, X2) -> add#(X1, X2),
               add#(active X1, X2) -> add#(X1, X2),
                         s# mark X -> s# X,
                       s# active X -> s# X,
               first#(X1, mark X2) -> first#(X1, X2),
             first#(X1, active X2) -> first#(X1, X2),
               first#(mark X1, X2) -> first#(X1, X2),
             first#(active X1, X2) -> first#(X1, X2),
                cons#(X1, mark X2) -> cons#(X1, X2),
              cons#(X1, active X2) -> cons#(X1, X2),
                cons#(mark X1, X2) -> cons#(X1, X2),
              cons#(active X1, X2) -> cons#(X1, X2),
                      from# mark X -> from# X,
                    from# active X -> from# X}
  TRS:
  {             mark and(X1, X2) -> active and(mark X1, X2),
                     mark true() -> active true(),
                    mark false() -> active false(),
             mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                mark add(X1, X2) -> active add(mark X1, X2),
                        mark 0() -> active 0(),
                        mark s X -> active s X,
                      mark nil() -> active nil(),
              mark first(X1, X2) -> active first(mark X1, mark X2),
               mark cons(X1, X2) -> active cons(X1, X2),
                     mark from X -> active from X,
           active and(true(), X) -> mark X,
          active and(false(), Y) -> mark false(),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
              active add(0(), X) -> mark X,
              active add(s X, Y) -> mark s add(X, Y),
            active first(0(), X) -> mark nil(),
   active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                   active from X -> mark cons(X, from s X),
                and(X1, mark X2) -> and(X1, X2),
              and(X1, active X2) -> and(X1, X2),
                and(mark X1, X2) -> and(X1, X2),
              and(active X1, X2) -> and(X1, X2),
             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),
                add(X1, mark X2) -> add(X1, X2),
              add(X1, active X2) -> add(X1, X2),
                add(mark X1, X2) -> add(X1, X2),
              add(active X1, X2) -> add(X1, X2),
                        s mark X -> s X,
                      s active X -> s X,
              first(X1, mark X2) -> first(X1, X2),
            first(X1, active X2) -> first(X1, X2),
              first(mark X1, X2) -> first(X1, X2),
            first(active X1, X2) -> first(X1, X2),
               cons(X1, mark X2) -> cons(X1, X2),
             cons(X1, active X2) -> cons(X1, X2),
               cons(mark X1, X2) -> cons(X1, X2),
             cons(active X1, X2) -> cons(X1, X2),
                     from mark X -> from X,
                   from active X -> from X}
  EDG:
   {
    (active# add(s X, Y) -> mark# s add(X, Y), mark# from X -> active# from X)
    (active# add(s X, Y) -> mark# s add(X, Y), mark# cons(X1, X2) -> active# cons(X1, X2))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> mark# X2)
    (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> mark# X1)
    (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s X)
    (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> add#(mark X1, X2))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> active# add(mark X1, X2))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X1)
    (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> mark# X1)
    (active# add(s X, Y) -> mark# s add(X, Y), mark# and(X1, X2) -> and#(mark X1, X2))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# add(s X, Y) -> mark# s add(X, Y), mark# and(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# from X -> active# from X)
    (mark# if(X1, X2, X3) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# nil() -> active# nil())
    (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> active# s X)
    (mark# if(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0())
    (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark 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# false() -> active# false())
    (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true())
    (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X1, mark# from X -> active# from X)
    (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2))
    (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s X)
    (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, X2))
    (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2))
    (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false())
    (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true())
    (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (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))
    (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, active X2) -> cons#(X1, X2))
    (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, mark X2) -> cons#(X1, X2))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> from# s X)
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> cons#(X, from s X))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> s# X)
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> mark# cons(X, from s X))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(0(), X) -> mark# nil())
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(0(), X) -> mark# X)
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y)
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# if(true(), X, Y) -> mark# X)
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# and(false(), Y) -> mark# false())
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# and(true(), X) -> mark# X)
    (active# if(true(), X, Y) -> mark# X, mark# from X -> active# from X)
    (active# if(true(), X, Y) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
    (active# if(true(), X, Y) -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# if(true(), X, Y) -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# if(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X2)
    (active# if(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X1)
    (active# if(true(), X, Y) -> mark# X, mark# nil() -> active# nil())
    (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s X)
    (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0())
    (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, X2))
    (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, X2))
    (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
    (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (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# and(X1, X2) -> and#(mark X1, X2))
    (active# if(true(), X, Y) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# if(true(), X, Y) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (s# active X -> s# X, s# active X -> s# X)
    (s# active X -> s# X, s# mark X -> s# X)
    (from# active X -> from# X, from# active X -> from# X)
    (from# active X -> from# X, from# mark X -> from# X)
    (mark# add(X1, X2) -> add#(mark X1, X2), add#(active X1, X2) -> add#(X1, X2))
    (mark# add(X1, X2) -> add#(mark X1, X2), add#(mark X1, X2) -> add#(X1, X2))
    (active# from X -> cons#(X, from s X), cons#(X1, active X2) -> cons#(X1, X2))
    (active# from X -> cons#(X, from s X), cons#(X1, mark X2) -> cons#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
    (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
    (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
    (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
    (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
    (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
    (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
    (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
    (first#(X1, active X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2))
    (first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
    (first#(X1, active X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2))
    (first#(X1, active X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
    (first#(active X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2))
    (first#(active X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
    (first#(active X1, X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2))
    (first#(active X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# from X -> from# s X)
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# from X -> cons#(X, from s X))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# from X -> s# X)
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# from X -> mark# cons(X, from s X))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# first(0(), X) -> mark# nil())
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> s# add(X, Y))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> add#(X, Y))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> mark# s add(X, Y))
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(0(), X) -> mark# X)
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(false(), X, Y) -> mark# Y)
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(true(), X, Y) -> mark# X)
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# and(false(), Y) -> mark# false())
    (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# and(true(), X) -> mark# X)
    (active# first(0(), X) -> mark# nil(), mark# nil() -> active# nil())
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# from X -> from# s X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# from X -> cons#(X, from s X))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# from X -> s# X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# from X -> mark# cons(X, from s X))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# first(0(), X) -> mark# nil())
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# add(s X, Y) -> s# add(X, Y))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# add(s X, Y) -> add#(X, Y))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# add(s X, Y) -> mark# s add(X, Y))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# add(0(), X) -> mark# X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# if(false(), X, Y) -> mark# Y)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# if(true(), X, Y) -> mark# X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(false(), Y) -> mark# false())
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(true(), X) -> mark# X)
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> from# s X)
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> cons#(X, from s X))
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> s# X)
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> mark# cons(X, from s X))
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# first(0(), X) -> mark# nil())
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# add(s X, Y) -> s# add(X, Y))
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# add(s X, Y) -> add#(X, Y))
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# add(s X, Y) -> mark# s add(X, Y))
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# add(0(), X) -> mark# X)
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# if(false(), X, Y) -> mark# Y)
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# if(true(), X, Y) -> mark# X)
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# and(false(), Y) -> mark# false())
    (mark# cons(X1, X2) -> active# cons(X1, X2), active# and(true(), X) -> mark# X)
    (mark# s X -> active# s X, active# from X -> from# s X)
    (mark# s X -> active# s X, active# from X -> cons#(X, from s X))
    (mark# s X -> active# s X, active# from X -> s# X)
    (mark# s X -> active# s X, active# from X -> mark# cons(X, from s X))
    (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# s X -> active# s X, active# first(0(), X) -> mark# nil())
    (mark# s X -> active# s X, active# add(s X, Y) -> s# add(X, Y))
    (mark# s X -> active# s X, active# add(s X, Y) -> add#(X, Y))
    (mark# s X -> active# s X, active# add(s X, Y) -> mark# s add(X, Y))
    (mark# s X -> active# s X, active# add(0(), X) -> mark# X)
    (mark# s X -> active# s X, active# if(false(), X, Y) -> mark# Y)
    (mark# s X -> active# s X, active# if(true(), X, Y) -> mark# X)
    (mark# s X -> active# s X, active# and(false(), Y) -> mark# false())
    (mark# s X -> active# s X, active# and(true(), X) -> mark# X)
    (active# from X -> from# s X, from# active X -> from# X)
    (active# from X -> from# s X, from# mark X -> from# X)
    (mark# from X -> active# from X, active# and(true(), X) -> mark# X)
    (mark# from X -> active# from X, active# and(false(), Y) -> mark# false())
    (mark# from X -> active# from X, active# if(true(), X, Y) -> mark# X)
    (mark# from X -> active# from X, active# if(false(), X, Y) -> mark# Y)
    (mark# from X -> active# from X, active# add(0(), X) -> mark# X)
    (mark# from X -> active# from X, active# add(s X, Y) -> mark# s add(X, Y))
    (mark# from X -> active# from X, active# add(s X, Y) -> add#(X, Y))
    (mark# from X -> active# from X, active# add(s X, Y) -> s# add(X, Y))
    (mark# from X -> active# from X, active# first(0(), X) -> mark# nil())
    (mark# from X -> active# from X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# from X -> active# from X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# from X -> active# from X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# from X -> active# from X, active# from X -> mark# cons(X, from s X))
    (mark# from X -> active# from X, active# from X -> s# X)
    (mark# from X -> active# from X, active# from X -> cons#(X, from s X))
    (mark# from X -> active# from X, active# from X -> from# s X)
    (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X)
    (active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X)
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# and(true(), X) -> mark# X)
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# and(false(), Y) -> mark# false())
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# if(true(), X, Y) -> mark# X)
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# if(false(), X, Y) -> mark# Y)
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# add(0(), X) -> mark# X)
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# add(s X, Y) -> mark# s add(X, Y))
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# add(s X, Y) -> add#(X, Y))
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# add(s X, Y) -> s# add(X, Y))
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# first(0(), X) -> mark# nil())
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# from X -> mark# cons(X, from s X))
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# from X -> s# X)
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# from X -> cons#(X, from s X))
    (mark# add(X1, X2) -> active# add(mark X1, X2), active# from X -> from# s X)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# and(X1, X2) -> mark# X1)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# and(X1, X2) -> and#(mark X1, X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# if(X1, X2, X3) -> mark# X1)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> mark# X1)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> active# add(mark X1, X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> add#(mark X1, X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> active# s X)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> mark# X1)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> mark# X2)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> active# cons(X1, X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> active# from X)
    (active# and(false(), Y) -> mark# false(), mark# false() -> active# false())
    (active# if(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> mark# X1)
    (active# if(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# if(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> and#(mark X1, X2))
    (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true())
    (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false())
    (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) -> active# if(mark X1, X2, X3))
    (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
    (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, X2))
    (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, X2))
    (active# if(false(), X, Y) -> mark# Y, mark# 0() -> active# 0())
    (active# if(false(), X, Y) -> mark# Y, mark# s X -> active# s X)
    (active# if(false(), X, Y) -> mark# Y, mark# nil() -> active# nil())
    (active# if(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X1)
    (active# if(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X2)
    (active# if(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# if(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# if(false(), X, Y) -> mark# Y, mark# cons(X1, X2) -> active# cons(X1, X2))
    (active# if(false(), X, Y) -> mark# Y, mark# from X -> active# from X)
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
    (first#(mark X1, X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2))
    (first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
    (first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2))
    (first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
    (first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2))
    (first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
    (first#(X1, mark X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2))
    (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
    (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
    (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
    (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
    (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
    (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
    (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
    (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# true() -> active# true())
    (mark# first(X1, X2) -> mark# X2, mark# false() -> active# false())
    (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# 0() -> active# 0())
    (mark# first(X1, X2) -> mark# X2, mark# s X -> active# s X)
    (mark# first(X1, X2) -> mark# X2, mark# nil() -> active# nil())
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2)
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# from X -> active# from X)
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (from# mark X -> from# X, from# mark X -> from# X)
    (from# mark X -> from# X, from# active X -> from# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (s# mark X -> s# X, s# active X -> s# X)
    (active# add(0(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (active# add(0(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# add(0(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (active# add(0(), X) -> mark# X, mark# true() -> active# true())
    (active# add(0(), X) -> mark# X, mark# false() -> active# false())
    (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
    (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, X2))
    (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, X2))
    (active# add(0(), X) -> mark# X, mark# 0() -> active# 0())
    (active# add(0(), X) -> mark# X, mark# s X -> active# s X)
    (active# add(0(), X) -> mark# X, mark# nil() -> active# nil())
    (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1)
    (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2)
    (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# add(0(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
    (active# add(0(), X) -> mark# X, mark# from X -> active# from X)
    (active# and(true(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (active# and(true(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# and(true(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (active# and(true(), X) -> mark# X, mark# true() -> active# true())
    (active# and(true(), X) -> mark# X, mark# false() -> active# false())
    (active# and(true(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (active# and(true(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (active# and(true(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (active# and(true(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
    (active# and(true(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, X2))
    (active# and(true(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, X2))
    (active# and(true(), X) -> mark# X, mark# 0() -> active# 0())
    (active# and(true(), X) -> mark# X, mark# s X -> active# s X)
    (active# and(true(), X) -> mark# X, mark# nil() -> active# nil())
    (active# and(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X1)
    (active# and(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X2)
    (active# and(true(), X) -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# and(true(), X) -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# and(true(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
    (active# and(true(), X) -> mark# X, mark# from X -> active# from X)
    (active# from X -> mark# cons(X, from s X), mark# and(X1, X2) -> mark# X1)
    (active# from X -> mark# cons(X, from s X), mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# and(X1, X2) -> and#(mark X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# if(X1, X2, X3) -> mark# X1)
    (active# from X -> mark# cons(X, from s X), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (active# from X -> mark# cons(X, from s X), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> mark# X1)
    (active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> active# add(mark X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> add#(mark X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# s X -> active# s X)
    (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> mark# X1)
    (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> mark# X2)
    (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# from X -> active# from X)
    (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# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# true() -> active# true())
    (mark# first(X1, X2) -> mark# X1, mark# false() -> active# false())
    (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# first(X1, X2) -> mark# X1, mark# s X -> active# s X)
    (mark# first(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# from X -> active# from X)
    (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
    (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# true() -> active# true())
    (mark# and(X1, X2) -> mark# X1, mark# false() -> active# false())
    (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
    (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
    (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# and(X1, X2) -> mark# X1, mark# s X -> active# s X)
    (mark# and(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# from X -> active# from X)
    (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, mark X2) -> first#(X1, X2))
    (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, active X2) -> first#(X1, X2))
    (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(mark X1, X2) -> first#(X1, X2))
    (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(active X1, X2) -> first#(X1, X2))
   }
   STATUS:
    arrows: 0.878252
    SCCS (8):
     Scc:
      {             mark# and(X1, X2) -> mark# X1,
                    mark# and(X1, X2) -> active# and(mark X1, X2),
                 mark# if(X1, X2, X3) -> mark# X1,
                 mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3),
                    mark# add(X1, X2) -> mark# X1,
                    mark# add(X1, X2) -> active# add(mark X1, X2),
                            mark# s X -> active# s X,
                  mark# first(X1, X2) -> mark# X1,
                  mark# first(X1, X2) -> mark# X2,
                  mark# first(X1, X2) -> active# first(mark X1, mark X2),
                   mark# cons(X1, X2) -> active# cons(X1, X2),
                         mark# from X -> active# from X,
               active# and(true(), X) -> mark# X,
             active# if(true(), X, Y) -> mark# X,
            active# if(false(), X, Y) -> mark# Y,
                  active# add(0(), X) -> mark# X,
                  active# add(s X, Y) -> mark# s add(X, Y),
       active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)),
                       active# from X -> mark# cons(X, from s X)}
     Scc:
      {  from# mark X -> from# X,
       from# active X -> from# X}
     Scc:
      {  cons#(X1, mark X2) -> cons#(X1, X2),
       cons#(X1, active X2) -> cons#(X1, X2),
         cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(active X1, X2) -> cons#(X1, X2)}
     Scc:
      {  s# mark X -> s# X,
       s# active X -> s# X}
     Scc:
      {  add#(X1, mark X2) -> add#(X1, X2),
       add#(X1, active X2) -> add#(X1, X2),
         add#(mark X1, X2) -> add#(X1, X2),
       add#(active X1, X2) -> add#(X1, X2)}
     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:
      {  and#(X1, mark X2) -> and#(X1, X2),
       and#(X1, active X2) -> and#(X1, X2),
         and#(mark X1, X2) -> and#(X1, X2),
       and#(active X1, X2) -> and#(X1, X2)}
     Scc:
      {  first#(X1, mark X2) -> first#(X1, X2),
       first#(X1, active X2) -> first#(X1, X2),
         first#(mark X1, X2) -> first#(X1, X2),
       first#(active X1, X2) -> first#(X1, X2)}
     
     SCC (19):
      Strict:
       {             mark# and(X1, X2) -> mark# X1,
                     mark# and(X1, X2) -> active# and(mark X1, X2),
                  mark# if(X1, X2, X3) -> mark# X1,
                  mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3),
                     mark# add(X1, X2) -> mark# X1,
                     mark# add(X1, X2) -> active# add(mark X1, X2),
                             mark# s X -> active# s X,
                   mark# first(X1, X2) -> mark# X1,
                   mark# first(X1, X2) -> mark# X2,
                   mark# first(X1, X2) -> active# first(mark X1, mark X2),
                    mark# cons(X1, X2) -> active# cons(X1, X2),
                          mark# from X -> active# from X,
                active# and(true(), X) -> mark# X,
              active# if(true(), X, Y) -> mark# X,
             active# if(false(), X, Y) -> mark# Y,
                   active# add(0(), X) -> mark# X,
                   active# add(s X, Y) -> mark# s add(X, Y),
        active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)),
                        active# from X -> mark# cons(X, from s X)}
      Weak:
      {             mark and(X1, X2) -> active and(mark X1, X2),
                         mark true() -> active true(),
                        mark false() -> active false(),
                 mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                    mark add(X1, X2) -> active add(mark X1, X2),
                            mark 0() -> active 0(),
                            mark s X -> active s X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                   mark cons(X1, X2) -> active cons(X1, X2),
                         mark from X -> active from X,
               active and(true(), X) -> mark X,
              active and(false(), Y) -> mark false(),
             active if(true(), X, Y) -> mark X,
            active if(false(), X, Y) -> mark Y,
                  active add(0(), X) -> mark X,
                  active add(s X, Y) -> mark s add(X, Y),
                active first(0(), X) -> mark nil(),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                       active from X -> mark cons(X, from s X),
                    and(X1, mark X2) -> and(X1, X2),
                  and(X1, active X2) -> and(X1, X2),
                    and(mark X1, X2) -> and(X1, X2),
                  and(active X1, X2) -> and(X1, X2),
                 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),
                    add(X1, mark X2) -> add(X1, X2),
                  add(X1, active X2) -> add(X1, X2),
                    add(mark X1, X2) -> add(X1, X2),
                  add(active X1, X2) -> add(X1, X2),
                            s mark X -> s X,
                          s active X -> s X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, X2),
                   cons(X1, mark X2) -> cons(X1, X2),
                 cons(X1, active X2) -> cons(X1, X2),
                   cons(mark X1, X2) -> cons(X1, X2),
                 cons(active X1, X2) -> cons(X1, X2),
                         from mark X -> from X,
                       from active X -> from X}
      Open
     
     SCC (2):
      Strict:
       {  from# mark X -> from# X,
        from# active X -> from# X}
      Weak:
      {             mark and(X1, X2) -> active and(mark X1, X2),
                         mark true() -> active true(),
                        mark false() -> active false(),
                 mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                    mark add(X1, X2) -> active add(mark X1, X2),
                            mark 0() -> active 0(),
                            mark s X -> active s X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                   mark cons(X1, X2) -> active cons(X1, X2),
                         mark from X -> active from X,
               active and(true(), X) -> mark X,
              active and(false(), Y) -> mark false(),
             active if(true(), X, Y) -> mark X,
            active if(false(), X, Y) -> mark Y,
                  active add(0(), X) -> mark X,
                  active add(s X, Y) -> mark s add(X, Y),
                active first(0(), X) -> mark nil(),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                       active from X -> mark cons(X, from s X),
                    and(X1, mark X2) -> and(X1, X2),
                  and(X1, active X2) -> and(X1, X2),
                    and(mark X1, X2) -> and(X1, X2),
                  and(active X1, X2) -> and(X1, X2),
                 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),
                    add(X1, mark X2) -> add(X1, X2),
                  add(X1, active X2) -> add(X1, X2),
                    add(mark X1, X2) -> add(X1, X2),
                  add(active X1, X2) -> add(X1, X2),
                            s mark X -> s X,
                          s active X -> s X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, X2),
                   cons(X1, mark X2) -> cons(X1, X2),
                 cons(X1, active X2) -> cons(X1, X2),
                   cons(mark X1, X2) -> cons(X1, X2),
                 cons(active X1, X2) -> cons(X1, X2),
                         from mark X -> from X,
                       from active X -> from X}
      Open
     
     
     
     SCC (4):
      Strict:
       {  cons#(X1, mark X2) -> cons#(X1, X2),
        cons#(X1, active X2) -> cons#(X1, X2),
          cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(active X1, X2) -> cons#(X1, X2)}
      Weak:
      {             mark and(X1, X2) -> active and(mark X1, X2),
                         mark true() -> active true(),
                        mark false() -> active false(),
                 mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                    mark add(X1, X2) -> active add(mark X1, X2),
                            mark 0() -> active 0(),
                            mark s X -> active s X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                   mark cons(X1, X2) -> active cons(X1, X2),
                         mark from X -> active from X,
               active and(true(), X) -> mark X,
              active and(false(), Y) -> mark false(),
             active if(true(), X, Y) -> mark X,
            active if(false(), X, Y) -> mark Y,
                  active add(0(), X) -> mark X,
                  active add(s X, Y) -> mark s add(X, Y),
                active first(0(), X) -> mark nil(),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                       active from X -> mark cons(X, from s X),
                    and(X1, mark X2) -> and(X1, X2),
                  and(X1, active X2) -> and(X1, X2),
                    and(mark X1, X2) -> and(X1, X2),
                  and(active X1, X2) -> and(X1, X2),
                 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),
                    add(X1, mark X2) -> add(X1, X2),
                  add(X1, active X2) -> add(X1, X2),
                    add(mark X1, X2) -> add(X1, X2),
                  add(active X1, X2) -> add(X1, X2),
                            s mark X -> s X,
                          s active X -> s X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, X2),
                   cons(X1, mark X2) -> cons(X1, X2),
                 cons(X1, active X2) -> cons(X1, X2),
                   cons(mark X1, X2) -> cons(X1, X2),
                 cons(active X1, X2) -> cons(X1, X2),
                         from mark X -> from X,
                       from active X -> from X}
      Open
     
     
     
     SCC (2):
      Strict:
       {  s# mark X -> s# X,
        s# active X -> s# X}
      Weak:
      {             mark and(X1, X2) -> active and(mark X1, X2),
                         mark true() -> active true(),
                        mark false() -> active false(),
                 mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                    mark add(X1, X2) -> active add(mark X1, X2),
                            mark 0() -> active 0(),
                            mark s X -> active s X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                   mark cons(X1, X2) -> active cons(X1, X2),
                         mark from X -> active from X,
               active and(true(), X) -> mark X,
              active and(false(), Y) -> mark false(),
             active if(true(), X, Y) -> mark X,
            active if(false(), X, Y) -> mark Y,
                  active add(0(), X) -> mark X,
                  active add(s X, Y) -> mark s add(X, Y),
                active first(0(), X) -> mark nil(),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                       active from X -> mark cons(X, from s X),
                    and(X1, mark X2) -> and(X1, X2),
                  and(X1, active X2) -> and(X1, X2),
                    and(mark X1, X2) -> and(X1, X2),
                  and(active X1, X2) -> and(X1, X2),
                 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),
                    add(X1, mark X2) -> add(X1, X2),
                  add(X1, active X2) -> add(X1, X2),
                    add(mark X1, X2) -> add(X1, X2),
                  add(active X1, X2) -> add(X1, X2),
                            s mark X -> s X,
                          s active X -> s X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, X2),
                   cons(X1, mark X2) -> cons(X1, X2),
                 cons(X1, active X2) -> cons(X1, X2),
                   cons(mark X1, X2) -> cons(X1, X2),
                 cons(active X1, X2) -> cons(X1, X2),
                         from mark X -> from X,
                       from active X -> from X}
      Open
     
     
     
     
     SCC (4):
      Strict:
       {  add#(X1, mark X2) -> add#(X1, X2),
        add#(X1, active X2) -> add#(X1, X2),
          add#(mark X1, X2) -> add#(X1, X2),
        add#(active X1, X2) -> add#(X1, X2)}
      Weak:
      {             mark and(X1, X2) -> active and(mark X1, X2),
                         mark true() -> active true(),
                        mark false() -> active false(),
                 mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                    mark add(X1, X2) -> active add(mark X1, X2),
                            mark 0() -> active 0(),
                            mark s X -> active s X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                   mark cons(X1, X2) -> active cons(X1, X2),
                         mark from X -> active from X,
               active and(true(), X) -> mark X,
              active and(false(), Y) -> mark false(),
             active if(true(), X, Y) -> mark X,
            active if(false(), X, Y) -> mark Y,
                  active add(0(), X) -> mark X,
                  active add(s X, Y) -> mark s add(X, Y),
                active first(0(), X) -> mark nil(),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                       active from X -> mark cons(X, from s X),
                    and(X1, mark X2) -> and(X1, X2),
                  and(X1, active X2) -> and(X1, X2),
                    and(mark X1, X2) -> and(X1, X2),
                  and(active X1, X2) -> and(X1, X2),
                 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),
                    add(X1, mark X2) -> add(X1, X2),
                  add(X1, active X2) -> add(X1, X2),
                    add(mark X1, X2) -> add(X1, X2),
                  add(active X1, X2) -> add(X1, X2),
                            s mark X -> s X,
                          s active X -> s X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, X2),
                   cons(X1, mark X2) -> cons(X1, X2),
                 cons(X1, active X2) -> cons(X1, X2),
                   cons(mark X1, X2) -> cons(X1, X2),
                 cons(active X1, X2) -> cons(X1, X2),
                         from mark X -> from X,
                       from active X -> from X}
      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 and(X1, X2) -> active and(mark X1, X2),
                         mark true() -> active true(),
                        mark false() -> active false(),
                 mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                    mark add(X1, X2) -> active add(mark X1, X2),
                            mark 0() -> active 0(),
                            mark s X -> active s X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                   mark cons(X1, X2) -> active cons(X1, X2),
                         mark from X -> active from X,
               active and(true(), X) -> mark X,
              active and(false(), Y) -> mark false(),
             active if(true(), X, Y) -> mark X,
            active if(false(), X, Y) -> mark Y,
                  active add(0(), X) -> mark X,
                  active add(s X, Y) -> mark s add(X, Y),
                active first(0(), X) -> mark nil(),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                       active from X -> mark cons(X, from s X),
                    and(X1, mark X2) -> and(X1, X2),
                  and(X1, active X2) -> and(X1, X2),
                    and(mark X1, X2) -> and(X1, X2),
                  and(active X1, X2) -> and(X1, X2),
                 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),
                    add(X1, mark X2) -> add(X1, X2),
                  add(X1, active X2) -> add(X1, X2),
                    add(mark X1, X2) -> add(X1, X2),
                  add(active X1, X2) -> add(X1, X2),
                            s mark X -> s X,
                          s active X -> s X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, X2),
                   cons(X1, mark X2) -> cons(X1, X2),
                 cons(X1, active X2) -> cons(X1, X2),
                   cons(mark X1, X2) -> cons(X1, X2),
                 cons(active X1, X2) -> cons(X1, X2),
                         from mark X -> from X,
                       from active X -> from X}
      Open
     
     
     
     
     SCC (4):
      Strict:
       {  and#(X1, mark X2) -> and#(X1, X2),
        and#(X1, active X2) -> and#(X1, X2),
          and#(mark X1, X2) -> and#(X1, X2),
        and#(active X1, X2) -> and#(X1, X2)}
      Weak:
      {             mark and(X1, X2) -> active and(mark X1, X2),
                         mark true() -> active true(),
                        mark false() -> active false(),
                 mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                    mark add(X1, X2) -> active add(mark X1, X2),
                            mark 0() -> active 0(),
                            mark s X -> active s X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                   mark cons(X1, X2) -> active cons(X1, X2),
                         mark from X -> active from X,
               active and(true(), X) -> mark X,
              active and(false(), Y) -> mark false(),
             active if(true(), X, Y) -> mark X,
            active if(false(), X, Y) -> mark Y,
                  active add(0(), X) -> mark X,
                  active add(s X, Y) -> mark s add(X, Y),
                active first(0(), X) -> mark nil(),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                       active from X -> mark cons(X, from s X),
                    and(X1, mark X2) -> and(X1, X2),
                  and(X1, active X2) -> and(X1, X2),
                    and(mark X1, X2) -> and(X1, X2),
                  and(active X1, X2) -> and(X1, X2),
                 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),
                    add(X1, mark X2) -> add(X1, X2),
                  add(X1, active X2) -> add(X1, X2),
                    add(mark X1, X2) -> add(X1, X2),
                  add(active X1, X2) -> add(X1, X2),
                            s mark X -> s X,
                          s active X -> s X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, X2),
                   cons(X1, mark X2) -> cons(X1, X2),
                 cons(X1, active X2) -> cons(X1, X2),
                   cons(mark X1, X2) -> cons(X1, X2),
                 cons(active X1, X2) -> cons(X1, X2),
                         from mark X -> from X,
                       from active X -> from X}
      Open
     
     SCC (4):
      Strict:
       {  first#(X1, mark X2) -> first#(X1, X2),
        first#(X1, active X2) -> first#(X1, X2),
          first#(mark X1, X2) -> first#(X1, X2),
        first#(active X1, X2) -> first#(X1, X2)}
      Weak:
      {             mark and(X1, X2) -> active and(mark X1, X2),
                         mark true() -> active true(),
                        mark false() -> active false(),
                 mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                    mark add(X1, X2) -> active add(mark X1, X2),
                            mark 0() -> active 0(),
                            mark s X -> active s X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                   mark cons(X1, X2) -> active cons(X1, X2),
                         mark from X -> active from X,
               active and(true(), X) -> mark X,
              active and(false(), Y) -> mark false(),
             active if(true(), X, Y) -> mark X,
            active if(false(), X, Y) -> mark Y,
                  active add(0(), X) -> mark X,
                  active add(s X, Y) -> mark s add(X, Y),
                active first(0(), X) -> mark nil(),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                       active from X -> mark cons(X, from s X),
                    and(X1, mark X2) -> and(X1, X2),
                  and(X1, active X2) -> and(X1, X2),
                    and(mark X1, X2) -> and(X1, X2),
                  and(active X1, X2) -> and(X1, X2),
                 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),
                    add(X1, mark X2) -> add(X1, X2),
                  add(X1, active X2) -> add(X1, X2),
                    add(mark X1, X2) -> add(X1, X2),
                  add(active X1, X2) -> add(X1, X2),
                            s mark X -> s X,
                          s active X -> s X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, X2),
                   cons(X1, mark X2) -> cons(X1, X2),
                 cons(X1, active X2) -> cons(X1, X2),
                   cons(mark X1, X2) -> cons(X1, X2),
                 cons(active X1, X2) -> cons(X1, X2),
                         from mark X -> from X,
                       from active X -> from X}
      Open