MAYBE
Time: 0.153633
TRS:
 {         active first(X1, X2) -> first(X1, active X2),
           active first(X1, X2) -> first(active X1, X2),
           active first(0(), X) -> mark nil(),
  active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
            active cons(X1, X2) -> cons(active X1, X2),
                     active s X -> s active X,
                  active from X -> mark cons(X, from s X),
                  active from X -> from active X,
             first(X1, mark X2) -> mark first(X1, X2),
             first(mark X1, X2) -> mark first(X1, X2),
            first(ok X1, ok X2) -> ok first(X1, X2),
              cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                    from mark X -> mark from X,
                      from ok X -> ok from X,
                   proper nil() -> ok nil(),
           proper first(X1, X2) -> first(proper X1, proper X2),
                     proper 0() -> ok 0(),
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper s X -> s proper X,
                  proper from X -> from proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
 DP:
  DP:
   {         active# first(X1, X2) -> active# X1,
             active# first(X1, X2) -> active# X2,
             active# first(X1, X2) -> first#(X1, active X2),
             active# first(X1, X2) -> first#(active X1, X2),
    active# first(s X, cons(Y, Z)) -> first#(X, Z),
    active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)),
              active# cons(X1, X2) -> active# X1,
              active# cons(X1, X2) -> cons#(active X1, X2),
                       active# s X -> active# X,
                       active# s X -> s# active X,
                    active# from X -> active# X,
                    active# from X -> cons#(X, from s X),
                    active# from X -> s# X,
                    active# from X -> from# active X,
                    active# from X -> from# s X,
               first#(X1, mark X2) -> first#(X1, X2),
               first#(mark X1, X2) -> first#(X1, X2),
              first#(ok X1, ok X2) -> first#(X1, X2),
                cons#(mark X1, X2) -> cons#(X1, X2),
               cons#(ok X1, ok X2) -> cons#(X1, X2),
                         s# mark X -> s# X,
                           s# ok X -> s# X,
                      from# mark X -> from# X,
                        from# ok X -> from# X,
             proper# first(X1, X2) -> first#(proper X1, proper X2),
             proper# first(X1, X2) -> proper# X1,
             proper# first(X1, X2) -> proper# X2,
              proper# cons(X1, X2) -> cons#(proper X1, proper X2),
              proper# cons(X1, X2) -> proper# X1,
              proper# cons(X1, X2) -> proper# X2,
                       proper# s X -> s# proper X,
                       proper# s X -> proper# X,
                    proper# from X -> from# proper X,
                    proper# from X -> proper# X,
                       top# mark X -> proper# X,
                       top# mark X -> top# proper X,
                         top# ok X -> active# X,
                         top# ok X -> top# active X}
  TRS:
  {         active first(X1, X2) -> first(X1, active X2),
            active first(X1, X2) -> first(active X1, X2),
            active first(0(), X) -> mark nil(),
   active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
             active cons(X1, X2) -> cons(active X1, X2),
                      active s X -> s active X,
                   active from X -> mark cons(X, from s X),
                   active from X -> from active X,
              first(X1, mark X2) -> mark first(X1, X2),
              first(mark X1, X2) -> mark first(X1, X2),
             first(ok X1, ok X2) -> ok first(X1, X2),
               cons(mark X1, X2) -> mark cons(X1, X2),
              cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
                     from mark X -> mark from X,
                       from ok X -> ok from X,
                    proper nil() -> ok nil(),
            proper first(X1, X2) -> first(proper X1, proper X2),
                      proper 0() -> ok 0(),
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper from X -> from proper X,
                      top mark X -> top proper X,
                        top ok X -> top active X}
  UR:
   {         active first(X1, X2) -> first(X1, active X2),
             active first(X1, X2) -> first(active X1, X2),
             active first(0(), X) -> mark nil(),
    active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
              active cons(X1, X2) -> cons(active X1, X2),
                       active s X -> s active X,
                    active from X -> mark cons(X, from s X),
                    active from X -> from active X,
               first(X1, mark X2) -> mark first(X1, X2),
               first(mark X1, X2) -> mark first(X1, X2),
              first(ok X1, ok X2) -> ok first(X1, X2),
                cons(mark X1, X2) -> mark cons(X1, X2),
               cons(ok X1, ok X2) -> ok cons(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                      from mark X -> mark from X,
                        from ok X -> ok from X,
                     proper nil() -> ok nil(),
             proper first(X1, X2) -> first(proper X1, proper X2),
                       proper 0() -> ok 0(),
              proper cons(X1, X2) -> cons(proper X1, proper X2),
                       proper s X -> s proper X,
                    proper from X -> from proper X,
                          a(x, y) -> x,
                          a(x, y) -> y}
   EDG:
    {
     (active# s X -> s# active X, s# ok X -> s# X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (active# from X -> from# s X, from# ok X -> from# X)
     (active# from X -> from# s X, from# mark X -> from# X)
     (proper# from X -> from# proper X, from# ok X -> from# X)
     (proper# from X -> from# proper X, from# mark X -> from# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok 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#(X1, mark X2) -> first#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# s X -> active# X, active# from X -> from# s X)
     (active# s X -> active# X, active# from X -> from# active X)
     (active# s X -> active# X, active# from X -> s# X)
     (active# s X -> active# X, active# from X -> cons#(X, from s X))
     (active# s X -> active# X, active# from X -> active# X)
     (active# s X -> active# X, active# s X -> s# active X)
     (active# s X -> active# X, active# s X -> active# X)
     (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# s X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# s X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# s X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
     (active# s X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
     (active# s X -> active# X, active# first(X1, X2) -> active# X2)
     (active# s X -> active# X, active# first(X1, X2) -> active# X1)
     (active# from X -> s# X, s# ok X -> s# X)
     (active# from X -> s# X, s# mark X -> s# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (s# ok X -> s# X, s# mark X -> s# X)
     (from# ok X -> from# X, from# ok X -> from# X)
     (from# ok X -> from# X, from# mark X -> from# X)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# from X -> proper# X)
     (proper# from X -> proper# X, proper# from X -> from# proper X)
     (proper# from X -> proper# X, proper# s X -> proper# X)
     (proper# from X -> proper# X, proper# s X -> s# proper X)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (top# ok X -> active# X, active# from X -> from# s X)
     (top# ok X -> active# X, active# from X -> from# active X)
     (top# ok X -> active# X, active# from X -> s# X)
     (top# ok X -> active# X, active# from X -> cons#(X, from s X))
     (top# ok X -> active# X, active# from X -> active# X)
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
     (top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
     (top# ok X -> active# X, active# first(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# first(X1, X2) -> active# X1)
     (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> active# X1, active# from X -> from# s X)
     (active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
     (active# cons(X1, X2) -> active# X1, active# from X -> s# X)
     (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
     (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
     (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
     (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
     (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# first(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# first(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
     (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
     (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
     (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# first(X1, X2) -> active# X1, active# s X -> active# X)
     (active# first(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# first(X1, X2) -> active# X1, active# from X -> active# X)
     (active# first(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# first(X1, X2) -> active# X1, active# from X -> s# X)
     (active# first(X1, X2) -> active# X1, active# from X -> from# active X)
     (active# first(X1, X2) -> active# X1, active# from X -> from# s 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#(ok X1, ok X2) -> cons#(X1, X2))
     (top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# from X -> from# proper X)
     (top# mark X -> proper# X, proper# from X -> proper# X)
     (proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# from X -> from# proper X)
     (proper# s X -> proper# X, proper# from X -> proper# X)
     (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# first(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# first(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (from# mark X -> from# X, from# mark X -> from# X)
     (from# mark X -> from# X, from# ok X -> from# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# ok X -> s# X)
     (active# from X -> active# X, active# first(X1, X2) -> active# X1)
     (active# from X -> active# X, active# first(X1, X2) -> active# X2)
     (active# from X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
     (active# from X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
     (active# from X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# from X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# from X -> active# X, active# s X -> active# X)
     (active# from X -> active# X, active# s X -> s# active X)
     (active# from X -> active# X, active# from X -> active# X)
     (active# from X -> active# X, active# from X -> cons#(X, from s X))
     (active# from X -> active# X, active# from X -> s# X)
     (active# from X -> active# X, active# from X -> from# active X)
     (active# from X -> active# X, active# from X -> from# s X)
     (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
     (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
     (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
     (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# first(X1, X2) -> active# X2, active# s X -> active# X)
     (active# first(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# first(X1, X2) -> active# X2, active# from X -> active# X)
     (active# first(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
     (active# first(X1, X2) -> active# X2, active# from X -> s# X)
     (active# first(X1, X2) -> active# X2, active# from X -> from# active X)
     (active# first(X1, X2) -> active# X2, active# from X -> from# s X)
     (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
     (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
     (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
     (first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
     (first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok 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#(mark X1, X2) -> first#(X1, X2))
     (first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (active# from X -> from# active X, from# mark X -> from# X)
     (active# from X -> from# active X, from# ok X -> from# X)
     (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark 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#(ok X1, ok X2) -> first#(X1, X2))
    }
    EDG:
     {
      (active# s X -> s# active X, s# ok X -> s# X)
      (active# s X -> s# active X, s# mark X -> s# X)
      (active# from X -> from# s X, from# ok X -> from# X)
      (active# from X -> from# s X, from# mark X -> from# X)
      (proper# from X -> from# proper X, from# ok X -> from# X)
      (proper# from X -> from# proper X, from# mark X -> from# X)
      (top# ok X -> top# active X, top# ok X -> top# active X)
      (top# ok X -> top# active X, top# ok X -> active# X)
      (top# ok X -> top# active X, top# mark X -> top# proper X)
      (top# ok X -> top# active X, top# mark X -> proper# X)
      (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok 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#(X1, mark X2) -> first#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
      (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# s X -> active# X, active# from X -> from# s X)
      (active# s X -> active# X, active# from X -> from# active X)
      (active# s X -> active# X, active# from X -> s# X)
      (active# s X -> active# X, active# from X -> cons#(X, from s X))
      (active# s X -> active# X, active# from X -> active# X)
      (active# s X -> active# X, active# s X -> s# active X)
      (active# s X -> active# X, active# s X -> active# X)
      (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
      (active# s X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# s X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# s X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
      (active# s X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
      (active# s X -> active# X, active# first(X1, X2) -> active# X2)
      (active# s X -> active# X, active# first(X1, X2) -> active# X1)
      (active# from X -> s# X, s# ok X -> s# X)
      (active# from X -> s# X, s# mark X -> s# X)
      (s# ok X -> s# X, s# ok X -> s# X)
      (s# ok X -> s# X, s# mark X -> s# X)
      (from# ok X -> from# X, from# ok X -> from# X)
      (from# ok X -> from# X, from# mark X -> from# X)
      (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
      (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
      (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# from X -> proper# X, proper# from X -> proper# X)
      (proper# from X -> proper# X, proper# from X -> from# proper X)
      (proper# from X -> proper# X, proper# s X -> proper# X)
      (proper# from X -> proper# X, proper# s X -> s# proper X)
      (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
      (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
      (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# from X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (proper# from X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (proper# from X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (top# ok X -> active# X, active# from X -> from# s X)
      (top# ok X -> active# X, active# from X -> from# active X)
      (top# ok X -> active# X, active# from X -> s# X)
      (top# ok X -> active# X, active# from X -> cons#(X, from s X))
      (top# ok X -> active# X, active# from X -> active# X)
      (top# ok X -> active# X, active# s X -> s# active X)
      (top# ok X -> active# X, active# s X -> active# X)
      (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
      (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
      (top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
      (top# ok X -> active# X, active# first(X1, X2) -> active# X2)
      (top# ok X -> active# X, active# first(X1, X2) -> active# X1)
      (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# cons(X1, X2) -> active# X1, active# from X -> from# s X)
      (active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
      (active# cons(X1, X2) -> active# X1, active# from X -> s# X)
      (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
      (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
      (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
      (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
      (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
      (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
      (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
      (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
      (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
      (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
      (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# first(X1, X2) -> proper# X1, proper# from X -> from# proper X)
      (proper# first(X1, X2) -> proper# X1, proper# from X -> proper# X)
      (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
      (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
      (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
      (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# first(X1, X2) -> active# X1, active# s X -> active# X)
      (active# first(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# first(X1, X2) -> active# X1, active# from X -> active# X)
      (active# first(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
      (active# first(X1, X2) -> active# X1, active# from X -> s# X)
      (active# first(X1, X2) -> active# X1, active# from X -> from# active X)
      (active# first(X1, X2) -> active# X1, active# from X -> from# s 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#(ok X1, ok X2) -> cons#(X1, X2))
      (top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# s X -> s# proper X)
      (top# mark X -> proper# X, proper# s X -> proper# X)
      (top# mark X -> proper# X, proper# from X -> from# proper X)
      (top# mark X -> proper# X, proper# from X -> proper# X)
      (proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# s X -> s# proper X)
      (proper# s X -> proper# X, proper# s X -> proper# X)
      (proper# s X -> proper# X, proper# from X -> from# proper X)
      (proper# s X -> proper# X, proper# from X -> proper# X)
      (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (proper# first(X1, X2) -> proper# X2, proper# from X -> from# proper X)
      (proper# first(X1, X2) -> proper# X2, proper# from X -> proper# X)
      (from# mark X -> from# X, from# mark X -> from# X)
      (from# mark X -> from# X, from# ok X -> from# X)
      (s# mark X -> s# X, s# mark X -> s# X)
      (s# mark X -> s# X, s# ok X -> s# X)
      (active# from X -> active# X, active# first(X1, X2) -> active# X1)
      (active# from X -> active# X, active# first(X1, X2) -> active# X2)
      (active# from X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
      (active# from X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
      (active# from X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# from X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
      (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# from X -> active# X, active# s X -> active# X)
      (active# from X -> active# X, active# s X -> s# active X)
      (active# from X -> active# X, active# from X -> active# X)
      (active# from X -> active# X, active# from X -> cons#(X, from s X))
      (active# from X -> active# X, active# from X -> s# X)
      (active# from X -> active# X, active# from X -> from# active X)
      (active# from X -> active# X, active# from X -> from# s X)
      (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
      (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
      (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
      (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# first(X1, X2) -> active# X2, active# s X -> active# X)
      (active# first(X1, X2) -> active# X2, active# s X -> s# active X)
      (active# first(X1, X2) -> active# X2, active# from X -> active# X)
      (active# first(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
      (active# first(X1, X2) -> active# X2, active# from X -> s# X)
      (active# first(X1, X2) -> active# X2, active# from X -> from# active X)
      (active# first(X1, X2) -> active# X2, active# from X -> from# s X)
      (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
      (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
      (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
      (first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
      (first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok 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#(mark X1, X2) -> first#(X1, X2))
      (first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (top# mark X -> top# proper X, top# mark X -> proper# X)
      (top# mark X -> top# proper X, top# mark X -> top# proper X)
      (top# mark X -> top# proper X, top# ok X -> active# X)
      (top# mark X -> top# proper X, top# ok X -> top# active X)
      (proper# s X -> s# proper X, s# mark X -> s# X)
      (proper# s X -> s# proper X, s# ok X -> s# X)
      (active# from X -> from# active X, from# mark X -> from# X)
      (active# from X -> from# active X, from# ok X -> from# X)
      (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark 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#(ok X1, ok X2) -> first#(X1, X2))
     }
     EDG:
      {
       (active# s X -> s# active X, s# ok X -> s# X)
       (active# s X -> s# active X, s# mark X -> s# X)
       (active# from X -> from# s X, from# ok X -> from# X)
       (active# from X -> from# s X, from# mark X -> from# X)
       (proper# from X -> from# proper X, from# ok X -> from# X)
       (proper# from X -> from# proper X, from# mark X -> from# X)
       (top# ok X -> top# active X, top# ok X -> top# active X)
       (top# ok X -> top# active X, top# ok X -> active# X)
       (top# ok X -> top# active X, top# mark X -> top# proper X)
       (top# ok X -> top# active X, top# mark X -> proper# X)
       (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
       (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok 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#(X1, mark X2) -> first#(X1, X2))
       (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
       (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
       (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
       (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (active# s X -> active# X, active# from X -> from# s X)
       (active# s X -> active# X, active# from X -> from# active X)
       (active# s X -> active# X, active# from X -> s# X)
       (active# s X -> active# X, active# from X -> cons#(X, from s X))
       (active# s X -> active# X, active# from X -> active# X)
       (active# s X -> active# X, active# s X -> s# active X)
       (active# s X -> active# X, active# s X -> active# X)
       (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
       (active# s X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# s X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# s X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
       (active# s X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
       (active# s X -> active# X, active# first(X1, X2) -> active# X2)
       (active# s X -> active# X, active# first(X1, X2) -> active# X1)
       (active# from X -> s# X, s# ok X -> s# X)
       (active# from X -> s# X, s# mark X -> s# X)
       (s# ok X -> s# X, s# ok X -> s# X)
       (s# ok X -> s# X, s# mark X -> s# X)
       (from# ok X -> from# X, from# ok X -> from# X)
       (from# ok X -> from# X, from# mark X -> from# X)
       (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
       (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
       (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
       (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
       (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# from X -> proper# X, proper# from X -> proper# X)
       (proper# from X -> proper# X, proper# from X -> from# proper X)
       (proper# from X -> proper# X, proper# s X -> proper# X)
       (proper# from X -> proper# X, proper# s X -> s# proper X)
       (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
       (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
       (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# from X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (proper# from X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (proper# from X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (top# ok X -> active# X, active# from X -> from# s X)
       (top# ok X -> active# X, active# from X -> from# active X)
       (top# ok X -> active# X, active# from X -> s# X)
       (top# ok X -> active# X, active# from X -> cons#(X, from s X))
       (top# ok X -> active# X, active# from X -> active# X)
       (top# ok X -> active# X, active# s X -> s# active X)
       (top# ok X -> active# X, active# s X -> active# X)
       (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
       (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
       (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
       (top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
       (top# ok X -> active# X, active# first(X1, X2) -> active# X2)
       (top# ok X -> active# X, active# first(X1, X2) -> active# X1)
       (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
       (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
       (active# cons(X1, X2) -> active# X1, active# from X -> from# s X)
       (active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
       (active# cons(X1, X2) -> active# X1, active# from X -> s# X)
       (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
       (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
       (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
       (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
       (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
       (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
       (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
       (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
       (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
       (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
       (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
       (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
       (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
       (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
       (proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
       (proper# first(X1, X2) -> proper# X1, proper# from X -> from# proper X)
       (proper# first(X1, X2) -> proper# X1, proper# from X -> proper# X)
       (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
       (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
       (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
       (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# first(X1, X2) -> active# X1, active# s X -> active# X)
       (active# first(X1, X2) -> active# X1, active# s X -> s# active X)
       (active# first(X1, X2) -> active# X1, active# from X -> active# X)
       (active# first(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
       (active# first(X1, X2) -> active# X1, active# from X -> s# X)
       (active# first(X1, X2) -> active# X1, active# from X -> from# active X)
       (active# first(X1, X2) -> active# X1, active# from X -> from# s 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#(ok X1, ok X2) -> cons#(X1, X2))
       (top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
       (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
       (top# mark X -> proper# X, proper# s X -> s# proper X)
       (top# mark X -> proper# X, proper# s X -> proper# X)
       (top# mark X -> proper# X, proper# from X -> from# proper X)
       (top# mark X -> proper# X, proper# from X -> proper# X)
       (proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
       (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
       (proper# s X -> proper# X, proper# s X -> s# proper X)
       (proper# s X -> proper# X, proper# s X -> proper# X)
       (proper# s X -> proper# X, proper# from X -> from# proper X)
       (proper# s X -> proper# X, proper# from X -> proper# X)
       (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
       (proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
       (proper# first(X1, X2) -> proper# X2, proper# from X -> from# proper X)
       (proper# first(X1, X2) -> proper# X2, proper# from X -> proper# X)
       (from# mark X -> from# X, from# mark X -> from# X)
       (from# mark X -> from# X, from# ok X -> from# X)
       (s# mark X -> s# X, s# mark X -> s# X)
       (s# mark X -> s# X, s# ok X -> s# X)
       (active# from X -> active# X, active# first(X1, X2) -> active# X1)
       (active# from X -> active# X, active# first(X1, X2) -> active# X2)
       (active# from X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
       (active# from X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
       (active# from X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# from X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
       (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# from X -> active# X, active# s X -> active# X)
       (active# from X -> active# X, active# s X -> s# active X)
       (active# from X -> active# X, active# from X -> active# X)
       (active# from X -> active# X, active# from X -> cons#(X, from s X))
       (active# from X -> active# X, active# from X -> s# X)
       (active# from X -> active# X, active# from X -> from# active X)
       (active# from X -> active# X, active# from X -> from# s X)
       (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
       (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
       (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
       (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# first(X1, X2) -> active# X2, active# s X -> active# X)
       (active# first(X1, X2) -> active# X2, active# s X -> s# active X)
       (active# first(X1, X2) -> active# X2, active# from X -> active# X)
       (active# first(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
       (active# first(X1, X2) -> active# X2, active# from X -> s# X)
       (active# first(X1, X2) -> active# X2, active# from X -> from# active X)
       (active# first(X1, X2) -> active# X2, active# from X -> from# s X)
       (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
       (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
       (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
       (first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
       (first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
       (first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok 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#(mark X1, X2) -> first#(X1, X2))
       (first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (top# mark X -> top# proper X, top# mark X -> proper# X)
       (top# mark X -> top# proper X, top# mark X -> top# proper X)
       (top# mark X -> top# proper X, top# ok X -> active# X)
       (top# mark X -> top# proper X, top# ok X -> top# active X)
       (proper# s X -> s# proper X, s# mark X -> s# X)
       (proper# s X -> s# proper X, s# ok X -> s# X)
       (active# from X -> from# active X, from# mark X -> from# X)
       (active# from X -> from# active X, from# ok X -> from# X)
       (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark 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#(ok X1, ok X2) -> first#(X1, X2))
      }
      EDG:
       {
        (active# s X -> s# active X, s# ok X -> s# X)
        (active# s X -> s# active X, s# mark X -> s# X)
        (active# from X -> from# s X, from# ok X -> from# X)
        (active# from X -> from# s X, from# mark X -> from# X)
        (proper# from X -> from# proper X, from# ok X -> from# X)
        (proper# from X -> from# proper X, from# mark X -> from# X)
        (top# ok X -> top# active X, top# ok X -> top# active X)
        (top# ok X -> top# active X, top# ok X -> active# X)
        (top# ok X -> top# active X, top# mark X -> top# proper X)
        (top# ok X -> top# active X, top# mark X -> proper# X)
        (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
        (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok 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#(X1, mark X2) -> first#(X1, X2))
        (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
        (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
        (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
        (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (active# s X -> active# X, active# from X -> from# s X)
        (active# s X -> active# X, active# from X -> from# active X)
        (active# s X -> active# X, active# from X -> s# X)
        (active# s X -> active# X, active# from X -> cons#(X, from s X))
        (active# s X -> active# X, active# from X -> active# X)
        (active# s X -> active# X, active# s X -> s# active X)
        (active# s X -> active# X, active# s X -> active# X)
        (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
        (active# s X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# s X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# s X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
        (active# s X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
        (active# s X -> active# X, active# first(X1, X2) -> active# X2)
        (active# s X -> active# X, active# first(X1, X2) -> active# X1)
        (active# from X -> s# X, s# ok X -> s# X)
        (active# from X -> s# X, s# mark X -> s# X)
        (s# ok X -> s# X, s# ok X -> s# X)
        (s# ok X -> s# X, s# mark X -> s# X)
        (from# ok X -> from# X, from# ok X -> from# X)
        (from# ok X -> from# X, from# mark X -> from# X)
        (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
        (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
        (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
        (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
        (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# from X -> proper# X, proper# from X -> proper# X)
        (proper# from X -> proper# X, proper# from X -> from# proper X)
        (proper# from X -> proper# X, proper# s X -> proper# X)
        (proper# from X -> proper# X, proper# s X -> s# proper X)
        (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
        (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
        (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# from X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (proper# from X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (proper# from X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (top# ok X -> active# X, active# from X -> from# s X)
        (top# ok X -> active# X, active# from X -> from# active X)
        (top# ok X -> active# X, active# from X -> s# X)
        (top# ok X -> active# X, active# from X -> cons#(X, from s X))
        (top# ok X -> active# X, active# from X -> active# X)
        (top# ok X -> active# X, active# s X -> s# active X)
        (top# ok X -> active# X, active# s X -> active# X)
        (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
        (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
        (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
        (top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
        (top# ok X -> active# X, active# first(X1, X2) -> active# X2)
        (top# ok X -> active# X, active# first(X1, X2) -> active# X1)
        (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
        (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
        (active# cons(X1, X2) -> active# X1, active# from X -> from# s X)
        (active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
        (active# cons(X1, X2) -> active# X1, active# from X -> s# X)
        (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
        (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
        (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
        (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
        (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
        (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
        (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
        (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
        (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
        (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
        (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
        (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
        (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
        (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
        (proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
        (proper# first(X1, X2) -> proper# X1, proper# from X -> from# proper X)
        (proper# first(X1, X2) -> proper# X1, proper# from X -> proper# X)
        (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
        (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
        (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
        (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# first(X1, X2) -> active# X1, active# s X -> active# X)
        (active# first(X1, X2) -> active# X1, active# s X -> s# active X)
        (active# first(X1, X2) -> active# X1, active# from X -> active# X)
        (active# first(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
        (active# first(X1, X2) -> active# X1, active# from X -> s# X)
        (active# first(X1, X2) -> active# X1, active# from X -> from# active X)
        (active# first(X1, X2) -> active# X1, active# from X -> from# s 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#(ok X1, ok X2) -> cons#(X1, X2))
        (top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
        (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
        (top# mark X -> proper# X, proper# s X -> s# proper X)
        (top# mark X -> proper# X, proper# s X -> proper# X)
        (top# mark X -> proper# X, proper# from X -> from# proper X)
        (top# mark X -> proper# X, proper# from X -> proper# X)
        (proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
        (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
        (proper# s X -> proper# X, proper# s X -> s# proper X)
        (proper# s X -> proper# X, proper# s X -> proper# X)
        (proper# s X -> proper# X, proper# from X -> from# proper X)
        (proper# s X -> proper# X, proper# from X -> proper# X)
        (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
        (proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
        (proper# first(X1, X2) -> proper# X2, proper# from X -> from# proper X)
        (proper# first(X1, X2) -> proper# X2, proper# from X -> proper# X)
        (from# mark X -> from# X, from# mark X -> from# X)
        (from# mark X -> from# X, from# ok X -> from# X)
        (s# mark X -> s# X, s# mark X -> s# X)
        (s# mark X -> s# X, s# ok X -> s# X)
        (active# from X -> active# X, active# first(X1, X2) -> active# X1)
        (active# from X -> active# X, active# first(X1, X2) -> active# X2)
        (active# from X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
        (active# from X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
        (active# from X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# from X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
        (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# from X -> active# X, active# s X -> active# X)
        (active# from X -> active# X, active# s X -> s# active X)
        (active# from X -> active# X, active# from X -> active# X)
        (active# from X -> active# X, active# from X -> cons#(X, from s X))
        (active# from X -> active# X, active# from X -> s# X)
        (active# from X -> active# X, active# from X -> from# active X)
        (active# from X -> active# X, active# from X -> from# s X)
        (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
        (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
        (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
        (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# first(X1, X2) -> active# X2, active# s X -> active# X)
        (active# first(X1, X2) -> active# X2, active# s X -> s# active X)
        (active# first(X1, X2) -> active# X2, active# from X -> active# X)
        (active# first(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
        (active# first(X1, X2) -> active# X2, active# from X -> s# X)
        (active# first(X1, X2) -> active# X2, active# from X -> from# active X)
        (active# first(X1, X2) -> active# X2, active# from X -> from# s X)
        (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
        (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
        (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
        (first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
        (first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
        (first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok 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#(mark X1, X2) -> first#(X1, X2))
        (first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (top# mark X -> top# proper X, top# mark X -> proper# X)
        (top# mark X -> top# proper X, top# mark X -> top# proper X)
        (top# mark X -> top# proper X, top# ok X -> active# X)
        (top# mark X -> top# proper X, top# ok X -> top# active X)
        (proper# s X -> s# proper X, s# mark X -> s# X)
        (proper# s X -> s# proper X, s# ok X -> s# X)
        (active# from X -> from# active X, from# mark X -> from# X)
        (active# from X -> from# active X, from# ok X -> from# X)
        (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark 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#(ok X1, ok X2) -> first#(X1, X2))
       }
       STATUS:
        arrows: 0.846953
        SCCS (7):
         Scc:
          {top# mark X -> top# proper X,
             top# ok X -> top# active X}
         Scc:
          {active# first(X1, X2) -> active# X1,
           active# first(X1, X2) -> active# X2,
            active# cons(X1, X2) -> active# X1,
                     active# s X -> active# X,
                  active# from X -> active# X}
         Scc:
          {proper# first(X1, X2) -> proper# X1,
           proper# first(X1, X2) -> proper# X2,
            proper# cons(X1, X2) -> proper# X1,
            proper# cons(X1, X2) -> proper# X2,
                     proper# s X -> proper# X,
                  proper# from X -> proper# X}
         Scc:
          { cons#(mark X1, X2) -> cons#(X1, X2),
           cons#(ok X1, ok X2) -> cons#(X1, X2)}
         Scc:
          {from# mark X -> from# X,
             from# ok X -> from# X}
         Scc:
          {s# mark X -> s# X,
             s# ok X -> s# X}
         Scc:
          { first#(X1, mark X2) -> first#(X1, X2),
            first#(mark X1, X2) -> first#(X1, X2),
           first#(ok X1, ok X2) -> first#(X1, X2)}
         
         SCC (2):
          Strict:
           {top# mark X -> top# proper X,
              top# ok X -> top# active X}
          Weak:
          {         active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
                    active first(0(), X) -> mark nil(),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                     active cons(X1, X2) -> cons(active X1, X2),
                              active s X -> s active X,
                           active from X -> mark cons(X, from s X),
                           active from X -> from active X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                       cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                                s mark X -> mark s X,
                                  s ok X -> ok s X,
                             from mark X -> mark from X,
                               from ok X -> ok from X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              proper 0() -> ok 0(),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                              proper s X -> s proper X,
                           proper from X -> from proper X,
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (5):
          Strict:
           {active# first(X1, X2) -> active# X1,
            active# first(X1, X2) -> active# X2,
             active# cons(X1, X2) -> active# X1,
                      active# s X -> active# X,
                   active# from X -> active# X}
          Weak:
          {         active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
                    active first(0(), X) -> mark nil(),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                     active cons(X1, X2) -> cons(active X1, X2),
                              active s X -> s active X,
                           active from X -> mark cons(X, from s X),
                           active from X -> from active X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                       cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                                s mark X -> mark s X,
                                  s ok X -> ok s X,
                             from mark X -> mark from X,
                               from ok X -> ok from X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              proper 0() -> ok 0(),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                              proper s X -> s proper X,
                           proper from X -> from proper X,
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         
         
         
         
         
         
         SCC (6):
          Strict:
           {proper# first(X1, X2) -> proper# X1,
            proper# first(X1, X2) -> proper# X2,
             proper# cons(X1, X2) -> proper# X1,
             proper# cons(X1, X2) -> proper# X2,
                      proper# s X -> proper# X,
                   proper# from X -> proper# X}
          Weak:
          {         active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
                    active first(0(), X) -> mark nil(),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                     active cons(X1, X2) -> cons(active X1, X2),
                              active s X -> s active X,
                           active from X -> mark cons(X, from s X),
                           active from X -> from active X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                       cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                                s mark X -> mark s X,
                                  s ok X -> ok s X,
                             from mark X -> mark from X,
                               from ok X -> ok from X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              proper 0() -> ok 0(),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                              proper s X -> s proper X,
                           proper from X -> from proper X,
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (2):
          Strict:
           { cons#(mark X1, X2) -> cons#(X1, X2),
            cons#(ok X1, ok X2) -> cons#(X1, X2)}
          Weak:
          {         active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
                    active first(0(), X) -> mark nil(),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                     active cons(X1, X2) -> cons(active X1, X2),
                              active s X -> s active X,
                           active from X -> mark cons(X, from s X),
                           active from X -> from active X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                       cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                                s mark X -> mark s X,
                                  s ok X -> ok s X,
                             from mark X -> mark from X,
                               from ok X -> ok from X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              proper 0() -> ok 0(),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                              proper s X -> s proper X,
                           proper from X -> from proper X,
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         
         
         
         
         SCC (2):
          Strict:
           {from# mark X -> from# X,
              from# ok X -> from# X}
          Weak:
          {         active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
                    active first(0(), X) -> mark nil(),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                     active cons(X1, X2) -> cons(active X1, X2),
                              active s X -> s active X,
                           active from X -> mark cons(X, from s X),
                           active from X -> from active X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                       cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                                s mark X -> mark s X,
                                  s ok X -> ok s X,
                             from mark X -> mark from X,
                               from ok X -> ok from X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              proper 0() -> ok 0(),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                              proper s X -> s proper X,
                           proper from X -> from proper X,
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (2):
          Strict:
           {s# mark X -> s# X,
              s# ok X -> s# X}
          Weak:
          {         active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
                    active first(0(), X) -> mark nil(),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                     active cons(X1, X2) -> cons(active X1, X2),
                              active s X -> s active X,
                           active from X -> mark cons(X, from s X),
                           active from X -> from active X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                       cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                                s mark X -> mark s X,
                                  s ok X -> ok s X,
                             from mark X -> mark from X,
                               from ok X -> ok from X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              proper 0() -> ok 0(),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                              proper s X -> s proper X,
                           proper from X -> from proper X,
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (3):
          Strict:
           { first#(X1, mark X2) -> first#(X1, X2),
             first#(mark X1, X2) -> first#(X1, X2),
            first#(ok X1, ok X2) -> first#(X1, X2)}
          Weak:
          {         active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
                    active first(0(), X) -> mark nil(),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                     active cons(X1, X2) -> cons(active X1, X2),
                              active s X -> s active X,
                           active from X -> mark cons(X, from s X),
                           active from X -> from active X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                       cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                                s mark X -> mark s X,
                                  s ok X -> ok s X,
                             from mark X -> mark from X,
                               from ok X -> ok from X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              proper 0() -> ok 0(),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                              proper s X -> s proper X,
                           proper from X -> from proper X,
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open