MAYBE
Time: 0.040315
TRS:
 {                   mark nil() -> active nil(),
             mark first(X1, X2) -> active first(mark X1, mark X2),
                       mark 0() -> active 0(),
              mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark s X -> active s mark X,
                    mark from X -> active from mark X,
           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),
             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),
                       s mark X -> s X,
                     s active X -> s X,
                    from mark X -> from X,
                  from active X -> from X}
 DP:
  DP:
   {                   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# 0() -> active# 0(),
                mark# cons(X1, X2) -> mark# X1,
                mark# cons(X1, X2) -> active# cons(mark X1, X2),
                mark# cons(X1, X2) -> cons#(mark X1, X2),
                         mark# s X -> mark# X,
                         mark# s X -> active# s mark X,
                         mark# s X -> s# mark X,
                      mark# from X -> mark# X,
                      mark# from X -> active# from mark X,
                      mark# from X -> from# mark X,
             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 -> cons#(X, from s X),
                    active# from X -> s# X,
                    active# from X -> from# 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),
                         s# mark X -> s# X,
                       s# active X -> s# X,
                      from# mark X -> from# X,
                    from# active X -> from# X}
  TRS:
  {                   mark nil() -> active nil(),
              mark first(X1, X2) -> active first(mark X1, mark X2),
                        mark 0() -> active 0(),
               mark cons(X1, X2) -> active cons(mark X1, X2),
                        mark s X -> active s mark X,
                     mark from X -> active from mark X,
            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),
              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),
                        s mark X -> s X,
                      s active X -> s X,
                     from mark X -> from X,
                   from active X -> from X}
  UR:
   {                   mark nil() -> active nil(),
               mark first(X1, X2) -> active first(mark X1, mark X2),
                         mark 0() -> active 0(),
                mark cons(X1, X2) -> active cons(mark X1, X2),
                         mark s X -> active s mark X,
                      mark from X -> active from mark X,
             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),
               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),
                         s mark X -> s X,
                       s active X -> s X,
                      from mark X -> from X,
                    from active X -> from X,
                          a(x, y) -> x,
                          a(x, y) -> y}
   EDG:
    {
     (mark# first(X1, X2) -> mark# X1, mark# from X -> from# mark X)
     (mark# first(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
     (mark# first(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# first(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# first(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# first(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# first(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, 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) -> mark# X2)
     (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
     (mark# first(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(active X1, X2) -> first#(X1, X2))
     (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
     (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, active X2) -> first#(X1, X2))
     (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
     (mark# 0() -> active# 0(), active# from X -> from# s X)
     (mark# 0() -> active# 0(), active# from X -> s# X)
     (mark# 0() -> active# 0(), active# from X -> cons#(X, from s X))
     (mark# 0() -> active# 0(), active# from X -> mark# cons(X, from s X))
     (mark# 0() -> active# 0(), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (mark# 0() -> active# 0(), active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (mark# 0() -> active# 0(), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
     (mark# 0() -> active# 0(), active# first(0(), X) -> mark# nil())
     (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(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))
     (mark# s X -> mark# X, mark# from X -> from# mark X)
     (mark# s X -> mark# X, mark# from X -> active# from mark X)
     (mark# s X -> mark# X, mark# from X -> mark# X)
     (mark# s X -> mark# X, mark# s X -> s# mark X)
     (mark# s X -> mark# X, mark# s X -> active# s mark X)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# 0() -> active# 0())
     (mark# s X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
     (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# nil() -> active# nil())
     (active# from X -> s# X, s# active X -> s# X)
     (active# from X -> s# X, s# mark X -> s# X)
     (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# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(active X1, 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#(X1, active X2) -> first#(X1, X2))
     (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, mark X2) -> first#(X1, X2))
     (active# from X -> mark# cons(X, from s X), mark# from X -> from# mark X)
     (active# from X -> mark# cons(X, from s X), mark# from X -> active# from mark X)
     (active# from X -> mark# cons(X, from s X), mark# from X -> mark# X)
     (active# from X -> mark# cons(X, from s X), mark# s X -> s# mark X)
     (active# from X -> mark# cons(X, from s X), mark# s X -> active# s mark X)
     (active# from X -> mark# cons(X, from s X), mark# s X -> mark# X)
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
     (active# from X -> mark# cons(X, from s X), mark# 0() -> active# 0())
     (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# first(X1, X2) -> active# first(mark X1, mark X2))
     (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) -> mark# X1)
     (active# from X -> mark# cons(X, from s X), mark# nil() -> active# nil())
     (mark# from X -> active# from mark X, active# from X -> from# s X)
     (mark# from X -> active# from mark X, active# from X -> s# X)
     (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
     (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
     (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
     (mark# from X -> active# from mark X, active# first(0(), X) -> mark# nil())
     (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# from X -> from# mark X, from# active X -> from# X)
     (mark# from X -> from# mark X, from# mark X -> from# X)
     (active# from X -> from# s X, from# mark X -> from# X)
     (active# from X -> from# s X, from# active X -> from# X)
     (mark# s X -> s# mark X, s# mark X -> s# X)
     (mark# s X -> s# mark X, s# active X -> s# 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))
     (mark# s X -> active# s mark X, active# first(0(), X) -> mark# nil())
     (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
     (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (mark# s X -> active# s mark X, active# from X -> mark# cons(X, from s X))
     (mark# s X -> active# s mark X, active# from X -> cons#(X, from s X))
     (mark# s X -> active# s mark X, active# from X -> s# X)
     (mark# s X -> active# s mark X, active# from X -> from# s X)
     (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# 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)) -> first#(X, Z))
     (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# from X -> mark# cons(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 -> from# 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# 0() -> active# 0())
     (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# first(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# first(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# first(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
     (mark# first(X1, X2) -> mark# X2, mark# from X -> from# mark X)
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# nil() -> active# nil())
     (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# 0() -> active# 0())
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> mark# X1)
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> mark# X)
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> active# s mark X)
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> s# mark X)
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> mark# X)
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> active# from mark X)
     (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> from# mark X)
     (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)
     (mark# from X -> mark# X, mark# nil() -> active# nil())
     (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X2)
     (mark# from X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
     (mark# from X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
     (mark# from X -> mark# X, mark# 0() -> active# 0())
     (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# from X -> mark# X, mark# s X -> mark# X)
     (mark# from X -> mark# X, mark# s X -> active# s mark X)
     (mark# from X -> mark# X, mark# s X -> s# mark X)
     (mark# from X -> mark# X, mark# from X -> mark# X)
     (mark# from X -> mark# X, mark# from X -> active# from mark X)
     (mark# from X -> mark# X, mark# from X -> from# mark X)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(0(), X) -> mark# nil())
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> mark# cons(X, from s X))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> cons#(X, from s X))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> s# X)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> from# s X)
     (active# first(0(), X) -> mark# nil(), mark# nil() -> active# nil())
     (active# first(0(), X) -> mark# nil(), mark# first(X1, X2) -> mark# X1)
     (active# first(0(), X) -> mark# nil(), mark# first(X1, X2) -> mark# X2)
     (active# first(0(), X) -> mark# nil(), mark# first(X1, X2) -> active# first(mark X1, mark X2))
     (active# first(0(), X) -> mark# nil(), mark# first(X1, X2) -> first#(mark X1, mark X2))
     (active# first(0(), X) -> mark# nil(), mark# 0() -> active# 0())
     (active# first(0(), X) -> mark# nil(), mark# cons(X1, X2) -> mark# X1)
     (active# first(0(), X) -> mark# nil(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# first(0(), X) -> mark# nil(), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# first(0(), X) -> mark# nil(), mark# s X -> mark# X)
     (active# first(0(), X) -> mark# nil(), mark# s X -> active# s mark X)
     (active# first(0(), X) -> mark# nil(), mark# s X -> s# mark X)
     (active# first(0(), X) -> mark# nil(), mark# from X -> mark# X)
     (active# first(0(), X) -> mark# nil(), mark# from X -> active# from mark X)
     (active# first(0(), X) -> mark# nil(), mark# from X -> from# mark X)
     (mark# nil() -> active# nil(), active# first(0(), X) -> mark# nil())
     (mark# nil() -> active# nil(), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
     (mark# nil() -> active# nil(), active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (mark# nil() -> active# nil(), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (mark# nil() -> active# nil(), active# from X -> mark# cons(X, from s X))
     (mark# nil() -> active# nil(), active# from X -> cons#(X, from s X))
     (mark# nil() -> active# nil(), active# from X -> s# X)
     (mark# nil() -> active# nil(), active# from X -> from# s X)
     (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
     (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, mark X2) -> cons#(X1, X2))
     (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#(mark X1, X2) -> cons#(X1, X2))
     (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(active X1, X2) -> cons#(X1, X2))
    }
    EDG:
     {
      (mark# first(X1, X2) -> mark# X1, mark# from X -> from# mark X)
      (mark# first(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
      (mark# first(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# first(X1, X2) -> mark# X1, mark# s X -> s# mark X)
      (mark# first(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
      (mark# first(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# first(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, 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) -> mark# X2)
      (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
      (mark# first(X1, X2) -> mark# X1, mark# nil() -> active# nil())
      (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(active X1, X2) -> first#(X1, X2))
      (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
      (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, active X2) -> first#(X1, X2))
      (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
      (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
      (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(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))
      (mark# s X -> mark# X, mark# from X -> from# mark X)
      (mark# s X -> mark# X, mark# from X -> active# from mark X)
      (mark# s X -> mark# X, mark# from X -> mark# X)
      (mark# s X -> mark# X, mark# s X -> s# mark X)
      (mark# s X -> mark# X, mark# s X -> active# s mark X)
      (mark# s X -> mark# X, mark# s X -> mark# X)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# 0() -> active# 0())
      (mark# s X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
      (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X2)
      (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# nil() -> active# nil())
      (active# from X -> s# X, s# active X -> s# X)
      (active# from X -> s# X, s# mark X -> s# X)
      (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# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(active X1, 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#(X1, active X2) -> first#(X1, X2))
      (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, mark X2) -> first#(X1, X2))
      (active# from X -> mark# cons(X, from s X), mark# from X -> from# mark X)
      (active# from X -> mark# cons(X, from s X), mark# from X -> active# from mark X)
      (active# from X -> mark# cons(X, from s X), mark# from X -> mark# X)
      (active# from X -> mark# cons(X, from s X), mark# s X -> s# mark X)
      (active# from X -> mark# cons(X, from s X), mark# s X -> active# s mark X)
      (active# from X -> mark# cons(X, from s X), mark# s X -> mark# X)
      (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
      (active# from X -> mark# cons(X, from s X), mark# 0() -> active# 0())
      (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# first(X1, X2) -> active# first(mark X1, mark X2))
      (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) -> mark# X1)
      (active# from X -> mark# cons(X, from s X), mark# nil() -> active# nil())
      (mark# from X -> active# from mark X, active# from X -> from# s X)
      (mark# from X -> active# from mark X, active# from X -> s# X)
      (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
      (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
      (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
      (mark# from X -> active# from mark X, active# first(0(), X) -> mark# nil())
      (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# from X -> from# mark X, from# active X -> from# X)
      (mark# from X -> from# mark X, from# mark X -> from# X)
      (active# from X -> from# s X, from# mark X -> from# X)
      (active# from X -> from# s X, from# active X -> from# X)
      (mark# s X -> s# mark X, s# mark X -> s# X)
      (mark# s X -> s# mark X, s# active X -> s# 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))
      (mark# s X -> active# s mark X, active# first(0(), X) -> mark# nil())
      (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
      (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (mark# s X -> active# s mark X, active# from X -> mark# cons(X, from s X))
      (mark# s X -> active# s mark X, active# from X -> cons#(X, from s X))
      (mark# s X -> active# s mark X, active# from X -> s# X)
      (mark# s X -> active# s mark X, active# from X -> from# s X)
      (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# 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)) -> first#(X, Z))
      (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# from X -> mark# cons(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 -> from# 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# 0() -> active# 0())
      (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# first(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
      (mark# first(X1, X2) -> mark# X2, mark# s X -> s# mark X)
      (mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X)
      (mark# first(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
      (mark# first(X1, X2) -> mark# X2, mark# from X -> from# mark X)
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# nil() -> active# nil())
      (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# 0() -> active# 0())
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> mark# X1)
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> mark# X)
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> active# s mark X)
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> s# mark X)
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> mark# X)
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> active# from mark X)
      (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> from# mark X)
      (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)
      (mark# from X -> mark# X, mark# nil() -> active# nil())
      (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X1)
      (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X2)
      (mark# from X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
      (mark# from X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
      (mark# from X -> mark# X, mark# 0() -> active# 0())
      (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# from X -> mark# X, mark# s X -> mark# X)
      (mark# from X -> mark# X, mark# s X -> active# s mark X)
      (mark# from X -> mark# X, mark# s X -> s# mark X)
      (mark# from X -> mark# X, mark# from X -> mark# X)
      (mark# from X -> mark# X, mark# from X -> active# from mark X)
      (mark# from X -> mark# X, mark# from X -> from# mark X)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(0(), X) -> mark# nil())
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> mark# cons(X, from s X))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> cons#(X, from s X))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> s# X)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> from# s X)
      (active# first(0(), X) -> mark# nil(), mark# nil() -> active# nil())
      (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
      (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
      (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
      (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, mark X2) -> cons#(X1, X2))
      (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#(mark X1, X2) -> cons#(X1, X2))
      (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(active X1, X2) -> cons#(X1, X2))
     }
     EDG:
      {
       (mark# first(X1, X2) -> mark# X1, mark# from X -> from# mark X)
       (mark# first(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
       (mark# first(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# first(X1, X2) -> mark# X1, mark# s X -> s# mark X)
       (mark# first(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
       (mark# first(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# first(X1, X2) -> mark# X1, mark# 0() -> active# 0())
       (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, 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) -> mark# X2)
       (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
       (mark# first(X1, X2) -> mark# X1, mark# nil() -> active# nil())
       (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(active X1, X2) -> first#(X1, X2))
       (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
       (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, active X2) -> first#(X1, X2))
       (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
       (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
       (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
       (mark# s X -> mark# X, mark# from X -> from# mark X)
       (mark# s X -> mark# X, mark# from X -> active# from mark X)
       (mark# s X -> mark# X, mark# from X -> mark# X)
       (mark# s X -> mark# X, mark# s X -> s# mark X)
       (mark# s X -> mark# X, mark# s X -> active# s mark X)
       (mark# s X -> mark# X, mark# s X -> mark# X)
       (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# 0() -> active# 0())
       (mark# s X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
       (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X2)
       (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# nil() -> active# nil())
       (active# from X -> s# X, s# active X -> s# X)
       (active# from X -> s# X, s# mark X -> s# X)
       (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# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
       (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
       (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
       (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(active X1, 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#(X1, active X2) -> first#(X1, X2))
       (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, mark X2) -> first#(X1, X2))
       (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
       (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
       (mark# from X -> active# from mark X, active# from X -> from# s X)
       (mark# from X -> active# from mark X, active# from X -> s# X)
       (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
       (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
       (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# from X -> from# mark X, from# active X -> from# X)
       (mark# from X -> from# mark X, from# mark X -> from# X)
       (mark# s X -> s# mark X, s# mark X -> s# X)
       (mark# s X -> s# mark X, s# active X -> s# 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))
       (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# 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)) -> first#(X, Z))
       (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) -> 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# 0() -> active# 0())
       (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
       (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X)
       (mark# first(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
       (mark# first(X1, X2) -> mark# X2, mark# s X -> s# mark X)
       (mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X)
       (mark# first(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
       (mark# first(X1, X2) -> mark# X2, mark# from X -> from# mark X)
       (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> mark# X1)
       (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> cons#(mark 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)
       (mark# from X -> mark# X, mark# nil() -> active# nil())
       (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X1)
       (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X2)
       (mark# from X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
       (mark# from X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
       (mark# from X -> mark# X, mark# 0() -> active# 0())
       (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# from X -> mark# X, mark# s X -> mark# X)
       (mark# from X -> mark# X, mark# s X -> active# s mark X)
       (mark# from X -> mark# X, mark# s X -> s# mark X)
       (mark# from X -> mark# X, mark# from X -> mark# X)
       (mark# from X -> mark# X, mark# from X -> active# from mark X)
       (mark# from X -> mark# X, mark# from X -> from# mark X)
       (active# first(0(), X) -> mark# nil(), mark# nil() -> active# nil())
       (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
       (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
       (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
       (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
       (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
       (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
       (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(active X1, X2) -> cons#(X1, X2))
      }
      EDG:
       {
        (mark# first(X1, X2) -> mark# X1, mark# from X -> from# mark X)
        (mark# first(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
        (mark# first(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# first(X1, X2) -> mark# X1, mark# s X -> s# mark X)
        (mark# first(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
        (mark# first(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# first(X1, X2) -> mark# X1, mark# 0() -> active# 0())
        (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, 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) -> mark# X2)
        (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
        (mark# first(X1, X2) -> mark# X1, mark# nil() -> active# nil())
        (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(active X1, X2) -> first#(X1, X2))
        (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
        (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, active X2) -> first#(X1, X2))
        (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
        (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
        (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
        (mark# s X -> mark# X, mark# from X -> from# mark X)
        (mark# s X -> mark# X, mark# from X -> active# from mark X)
        (mark# s X -> mark# X, mark# from X -> mark# X)
        (mark# s X -> mark# X, mark# s X -> s# mark X)
        (mark# s X -> mark# X, mark# s X -> active# s mark X)
        (mark# s X -> mark# X, mark# s X -> mark# X)
        (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# 0() -> active# 0())
        (mark# s X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
        (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X2)
        (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# nil() -> active# nil())
        (active# from X -> s# X, s# active X -> s# X)
        (active# from X -> s# X, s# mark X -> s# X)
        (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# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
        (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
        (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
        (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(active X1, 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#(X1, active X2) -> first#(X1, X2))
        (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, mark X2) -> first#(X1, X2))
        (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
        (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
        (mark# from X -> active# from mark X, active# from X -> from# s X)
        (mark# from X -> active# from mark X, active# from X -> s# X)
        (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
        (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
        (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# from X -> from# mark X, from# active X -> from# X)
        (mark# from X -> from# mark X, from# mark X -> from# X)
        (mark# s X -> s# mark X, s# mark X -> s# X)
        (mark# s X -> s# mark X, s# active X -> s# 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))
        (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# 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)) -> first#(X, Z))
        (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) -> 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# 0() -> active# 0())
        (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
        (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X)
        (mark# first(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
        (mark# first(X1, X2) -> mark# X2, mark# s X -> s# mark X)
        (mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X)
        (mark# first(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
        (mark# first(X1, X2) -> mark# X2, mark# from X -> from# mark X)
        (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> mark# X1)
        (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> cons#(mark 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)
        (mark# from X -> mark# X, mark# nil() -> active# nil())
        (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X1)
        (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X2)
        (mark# from X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
        (mark# from X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
        (mark# from X -> mark# X, mark# 0() -> active# 0())
        (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# from X -> mark# X, mark# s X -> mark# X)
        (mark# from X -> mark# X, mark# s X -> active# s mark X)
        (mark# from X -> mark# X, mark# s X -> s# mark X)
        (mark# from X -> mark# X, mark# from X -> mark# X)
        (mark# from X -> mark# X, mark# from X -> active# from mark X)
        (mark# from X -> mark# X, mark# from X -> from# mark X)
        (active# first(0(), X) -> mark# nil(), mark# nil() -> active# nil())
        (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
        (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
        (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
        (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
        (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
        (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
        (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(active X1, X2) -> cons#(X1, X2))
       }
       STATUS:
        arrows: 0.875918
        SCCS (5):
         Scc:
          {           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) -> mark# X1,
                                mark# s X -> mark# X,
                             mark# from X -> mark# X,
                             mark# from X -> active# from mark X,
           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:
          {  s# mark X -> s# X,
           s# active X -> s# X}
         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:
          {  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 (9):
          Strict:
           {           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) -> mark# X1,
                                 mark# s X -> mark# X,
                              mark# from X -> mark# X,
                              mark# from X -> active# from mark X,
            active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)),
                            active# from X -> mark# cons(X, from s X)}
          Weak:
          {                   mark nil() -> active nil(),
                      mark first(X1, X2) -> active first(mark X1, mark X2),
                                mark 0() -> active 0(),
                       mark cons(X1, X2) -> active cons(mark X1, X2),
                                mark s X -> active s mark X,
                             mark from X -> active from mark X,
                    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),
                      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),
                                s mark X -> s X,
                              s active X -> s X,
                             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 nil() -> active nil(),
                      mark first(X1, X2) -> active first(mark X1, mark X2),
                                mark 0() -> active 0(),
                       mark cons(X1, X2) -> active cons(mark X1, X2),
                                mark s X -> active s mark X,
                             mark from X -> active from mark X,
                    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),
                      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),
                                s mark X -> s X,
                              s active X -> s X,
                             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 nil() -> active nil(),
                      mark first(X1, X2) -> active first(mark X1, mark X2),
                                mark 0() -> active 0(),
                       mark cons(X1, X2) -> active cons(mark X1, X2),
                                mark s X -> active s mark X,
                             mark from X -> active from mark X,
                    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),
                      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),
                                s mark X -> s X,
                              s active X -> s X,
                             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 nil() -> active nil(),
                      mark first(X1, X2) -> active first(mark X1, mark X2),
                                mark 0() -> active 0(),
                       mark cons(X1, X2) -> active cons(mark X1, X2),
                                mark s X -> active s mark X,
                             mark from X -> active from mark X,
                    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),
                      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),
                                s mark X -> s X,
                              s active X -> s X,
                             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 nil() -> active nil(),
                      mark first(X1, X2) -> active first(mark X1, mark X2),
                                mark 0() -> active 0(),
                       mark cons(X1, X2) -> active cons(mark X1, X2),
                                mark s X -> active s mark X,
                             mark from X -> active from mark X,
                    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),
                      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),
                                s mark X -> s X,
                              s active X -> s X,
                             from mark X -> from X,
                           from active X -> from X}
          Open