MAYBE
TRS:
 {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                     mark(f(X)) -> active(f(mark(X))),
                     mark(g(X)) -> active(g(mark(X))),
                     mark(s(X)) -> active(s(mark(X))),
                      mark(0()) -> active(0()),
              mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                     f(mark(X)) -> f(X),
                   f(active(X)) -> f(X),
                     g(mark(X)) -> g(X),
                   g(active(X)) -> g(X),
                   active(f(X)) -> mark(cons(X, f(g(X)))),
                active(g(s(X))) -> mark(s(s(g(X)))),
                 active(g(0())) -> mark(s(0())),
  active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
   active(sel(0(), cons(X, Y))) -> mark(X),
                     s(mark(X)) -> s(X),
                   s(active(X)) -> s(X),
              sel(X1, mark(X2)) -> sel(X1, X2),
            sel(X1, active(X2)) -> sel(X1, X2),
              sel(mark(X1), X2) -> sel(X1, X2),
            sel(active(X1), X2) -> sel(X1, X2)}
 DP:
  Strict:
   {           mark#(cons(X1, X2)) -> mark#(X1),
               mark#(cons(X1, X2)) -> cons#(mark(X1), X2),
               mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                       mark#(f(X)) -> mark#(X),
                       mark#(f(X)) -> f#(mark(X)),
                       mark#(f(X)) -> active#(f(mark(X))),
                       mark#(g(X)) -> mark#(X),
                       mark#(g(X)) -> g#(mark(X)),
                       mark#(g(X)) -> active#(g(mark(X))),
                       mark#(s(X)) -> mark#(X),
                       mark#(s(X)) -> active#(s(mark(X))),
                       mark#(s(X)) -> s#(mark(X)),
                        mark#(0()) -> active#(0()),
                mark#(sel(X1, X2)) -> mark#(X1),
                mark#(sel(X1, X2)) -> mark#(X2),
                mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                mark#(sel(X1, X2)) -> sel#(mark(X1), mark(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),
                       f#(mark(X)) -> f#(X),
                     f#(active(X)) -> f#(X),
                       g#(mark(X)) -> g#(X),
                     g#(active(X)) -> g#(X),
                     active#(f(X)) -> mark#(cons(X, f(g(X)))),
                     active#(f(X)) -> cons#(X, f(g(X))),
                     active#(f(X)) -> f#(g(X)),
                     active#(f(X)) -> g#(X),
                  active#(g(s(X))) -> mark#(s(s(g(X)))),
                  active#(g(s(X))) -> g#(X),
                  active#(g(s(X))) -> s#(g(X)),
                  active#(g(s(X))) -> s#(s(g(X))),
                   active#(g(0())) -> mark#(s(0())),
                   active#(g(0())) -> s#(0()),
    active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)),
    active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z),
     active#(sel(0(), cons(X, Y))) -> mark#(X),
                       s#(mark(X)) -> s#(X),
                     s#(active(X)) -> s#(X),
                sel#(X1, mark(X2)) -> sel#(X1, X2),
              sel#(X1, active(X2)) -> sel#(X1, X2),
                sel#(mark(X1), X2) -> sel#(X1, X2),
              sel#(active(X1), X2) -> sel#(X1, X2)}
  Weak:
  {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                      mark(f(X)) -> active(f(mark(X))),
                      mark(g(X)) -> active(g(mark(X))),
                      mark(s(X)) -> active(s(mark(X))),
                       mark(0()) -> active(0()),
               mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                      f(mark(X)) -> f(X),
                    f(active(X)) -> f(X),
                      g(mark(X)) -> g(X),
                    g(active(X)) -> g(X),
                    active(f(X)) -> mark(cons(X, f(g(X)))),
                 active(g(s(X))) -> mark(s(s(g(X)))),
                  active(g(0())) -> mark(s(0())),
   active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
    active(sel(0(), cons(X, Y))) -> mark(X),
                      s(mark(X)) -> s(X),
                    s(active(X)) -> s(X),
               sel(X1, mark(X2)) -> sel(X1, X2),
             sel(X1, active(X2)) -> sel(X1, X2),
               sel(mark(X1), X2) -> sel(X1, X2),
             sel(active(X1), X2) -> sel(X1, X2)}
  EDG:
   {
    (mark#(g(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(g(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(g(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(g(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(g(X)) -> mark#(X), mark#(0()) -> active#(0()))
    (mark#(g(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (mark#(g(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(g(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(g(X)) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
    (mark#(g(X)) -> mark#(X), mark#(g(X)) -> g#(mark(X)))
    (mark#(g(X)) -> mark#(X), mark#(g(X)) -> mark#(X))
    (mark#(g(X)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
    (mark#(g(X)) -> mark#(X), mark#(f(X)) -> f#(mark(X)))
    (mark#(g(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(g(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(g(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(g(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (f#(mark(X)) -> f#(X), f#(active(X)) -> f#(X))
    (f#(mark(X)) -> f#(X), f#(mark(X)) -> f#(X))
    (g#(mark(X)) -> g#(X), g#(active(X)) -> g#(X))
    (g#(mark(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (active#(f(X)) -> g#(X), g#(active(X)) -> g#(X))
    (active#(f(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(0()) -> active#(0()))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(s(X)) -> mark#(X))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(g(X)) -> g#(mark(X)))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(g(X)) -> mark#(X))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(f(X)) -> f#(mark(X)))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(f(X)) -> mark#(X))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))
    (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(g(X)) -> active#(g(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(g(X)) -> g#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(g(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(f(X)) -> active#(f(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(f(X)) -> f#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(f(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(f(X)) -> cons#(X, f(g(X))), cons#(active(X1), X2) -> cons#(X1, X2))
    (active#(f(X)) -> cons#(X, f(g(X))), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(f(X)) -> cons#(X, f(g(X))), cons#(X1, active(X2)) -> cons#(X1, X2))
    (active#(f(X)) -> cons#(X, f(g(X))), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(0(), cons(X, Y))) -> mark#(X))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(g(0())) -> s#(0()))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(g(0())) -> mark#(s(0())))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(g(s(X))) -> s#(s(g(X))))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(g(s(X))) -> s#(g(X)))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(g(s(X))) -> g#(X))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(g(s(X))) -> mark#(s(s(g(X)))))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(f(X)) -> g#(X))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(f(X)) -> f#(g(X)))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(f(X)) -> cons#(X, f(g(X))))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(f(X)) -> mark#(cons(X, f(g(X)))))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), 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#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), 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#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(active(X1), X2) -> sel#(X1, X2))
    (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(mark(X1), X2) -> sel#(X1, X2))
    (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(X1, active(X2)) -> sel#(X1, X2))
    (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(0(), cons(X, Y))) -> mark#(X))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(g(0())) -> s#(0()))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(g(0())) -> mark#(s(0())))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(g(s(X))) -> s#(s(g(X))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(g(s(X))) -> s#(g(X)))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(g(s(X))) -> g#(X))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(g(s(X))) -> mark#(s(s(g(X)))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(f(X)) -> g#(X))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(f(X)) -> f#(g(X)))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(f(X)) -> cons#(X, f(g(X))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(f(X)) -> mark#(cons(X, f(g(X)))))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(sel(X1, X2)) -> mark#(X1))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(s(X)) -> s#(mark(X)))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(s(X)) -> active#(s(mark(X))))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(s(X)) -> mark#(X))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(g(X)) -> active#(g(mark(X))))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(g(X)) -> g#(mark(X)))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(g(X)) -> mark#(X))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(f(X)) -> active#(f(mark(X))))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(f(X)) -> f#(mark(X)))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(f(X)) -> mark#(X))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(g(X)) -> active#(g(mark(X))), active#(sel(0(), cons(X, Y))) -> mark#(X))
    (mark#(g(X)) -> active#(g(mark(X))), active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z))
    (mark#(g(X)) -> active#(g(mark(X))), active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)))
    (mark#(g(X)) -> active#(g(mark(X))), active#(g(0())) -> s#(0()))
    (mark#(g(X)) -> active#(g(mark(X))), active#(g(0())) -> mark#(s(0())))
    (mark#(g(X)) -> active#(g(mark(X))), active#(g(s(X))) -> s#(s(g(X))))
    (mark#(g(X)) -> active#(g(mark(X))), active#(g(s(X))) -> s#(g(X)))
    (mark#(g(X)) -> active#(g(mark(X))), active#(g(s(X))) -> g#(X))
    (mark#(g(X)) -> active#(g(mark(X))), active#(g(s(X))) -> mark#(s(s(g(X)))))
    (mark#(g(X)) -> active#(g(mark(X))), active#(f(X)) -> g#(X))
    (mark#(g(X)) -> active#(g(mark(X))), active#(f(X)) -> f#(g(X)))
    (mark#(g(X)) -> active#(g(mark(X))), active#(f(X)) -> cons#(X, f(g(X))))
    (mark#(g(X)) -> active#(g(mark(X))), active#(f(X)) -> mark#(cons(X, f(g(X)))))
    (active#(g(s(X))) -> s#(s(g(X))), s#(active(X)) -> s#(X))
    (active#(g(s(X))) -> s#(s(g(X))), s#(mark(X)) -> s#(X))
    (mark#(f(X)) -> f#(mark(X)), f#(active(X)) -> f#(X))
    (mark#(f(X)) -> f#(mark(X)), f#(mark(X)) -> f#(X))
    (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X))
    (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X))
    (active#(g(s(X))) -> s#(g(X)), s#(active(X)) -> s#(X))
    (active#(g(s(X))) -> s#(g(X)), s#(mark(X)) -> s#(X))
    (active#(f(X)) -> f#(g(X)), f#(mark(X)) -> f#(X))
    (active#(f(X)) -> f#(g(X)), f#(active(X)) -> f#(X))
    (mark#(g(X)) -> g#(mark(X)), g#(mark(X)) -> g#(X))
    (mark#(g(X)) -> g#(mark(X)), g#(active(X)) -> g#(X))
    (active#(g(0())) -> mark#(s(0())), mark#(s(X)) -> mark#(X))
    (active#(g(0())) -> mark#(s(0())), mark#(s(X)) -> active#(s(mark(X))))
    (active#(g(0())) -> mark#(s(0())), mark#(s(X)) -> s#(mark(X)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(f(X)) -> mark#(cons(X, f(g(X)))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(f(X)) -> cons#(X, f(g(X))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(f(X)) -> f#(g(X)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(f(X)) -> g#(X))
    (mark#(s(X)) -> active#(s(mark(X))), active#(g(s(X))) -> mark#(s(s(g(X)))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(g(s(X))) -> g#(X))
    (mark#(s(X)) -> active#(s(mark(X))), active#(g(s(X))) -> s#(g(X)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(g(s(X))) -> s#(s(g(X))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(g(0())) -> mark#(s(0())))
    (mark#(s(X)) -> active#(s(mark(X))), active#(g(0())) -> s#(0()))
    (mark#(s(X)) -> active#(s(mark(X))), active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z))
    (mark#(s(X)) -> active#(s(mark(X))), active#(sel(0(), cons(X, Y))) -> mark#(X))
    (mark#(f(X)) -> active#(f(mark(X))), active#(f(X)) -> mark#(cons(X, f(g(X)))))
    (mark#(f(X)) -> active#(f(mark(X))), active#(f(X)) -> cons#(X, f(g(X))))
    (mark#(f(X)) -> active#(f(mark(X))), active#(f(X)) -> f#(g(X)))
    (mark#(f(X)) -> active#(f(mark(X))), active#(f(X)) -> g#(X))
    (mark#(f(X)) -> active#(f(mark(X))), active#(g(s(X))) -> mark#(s(s(g(X)))))
    (mark#(f(X)) -> active#(f(mark(X))), active#(g(s(X))) -> g#(X))
    (mark#(f(X)) -> active#(f(mark(X))), active#(g(s(X))) -> s#(g(X)))
    (mark#(f(X)) -> active#(f(mark(X))), active#(g(s(X))) -> s#(s(g(X))))
    (mark#(f(X)) -> active#(f(mark(X))), active#(g(0())) -> mark#(s(0())))
    (mark#(f(X)) -> active#(f(mark(X))), active#(g(0())) -> s#(0()))
    (mark#(f(X)) -> active#(f(mark(X))), active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)))
    (mark#(f(X)) -> active#(f(mark(X))), active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z))
    (mark#(f(X)) -> active#(f(mark(X))), active#(sel(0(), cons(X, Y))) -> mark#(X))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(f(X)) -> mark#(X))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(f(X)) -> f#(mark(X)))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(f(X)) -> active#(f(mark(X))))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(g(X)) -> mark#(X))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(g(X)) -> g#(mark(X)))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(g(X)) -> active#(g(mark(X))))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(s(X)) -> mark#(X))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(s(X)) -> active#(s(mark(X))))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(s(X)) -> s#(mark(X)))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(sel(X1, X2)) -> mark#(X1))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z), sel#(X1, active(X2)) -> sel#(X1, X2))
    (active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z), sel#(mark(X1), X2) -> sel#(X1, X2))
    (active#(sel(s(X), cons(Y, Z))) -> sel#(X, Z), sel#(active(X1), X2) -> sel#(X1, X2))
    (sel#(active(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(active(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
    (sel#(active(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(active(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2))
    (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
    (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(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#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(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#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(f(X)) -> mark#(X))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(f(X)) -> f#(mark(X)))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(f(X)) -> active#(f(mark(X))))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(g(X)) -> mark#(X))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(g(X)) -> g#(mark(X)))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(g(X)) -> active#(g(mark(X))))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(s(X)) -> mark#(X))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(s(X)) -> active#(s(mark(X))))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(s(X)) -> s#(mark(X)))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(sel(X1, X2)) -> mark#(X1))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, mark(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#(mark(X1), X2) -> cons#(X1, X2))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(f(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(f(X)) -> f#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(f(X)) -> active#(f(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(g(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(g(X)) -> g#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(g(X)) -> active#(g(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0()))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> f#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> active#(f(mark(X))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(g(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(g(X)) -> g#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(g(X)) -> active#(g(mark(X))))
    (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#(0()) -> active#(0()))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X))
    (active#(g(s(X))) -> g#(X), g#(mark(X)) -> g#(X))
    (active#(g(s(X))) -> g#(X), g#(active(X)) -> g#(X))
    (g#(active(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (g#(active(X)) -> g#(X), g#(active(X)) -> g#(X))
    (f#(active(X)) -> f#(X), f#(mark(X)) -> f#(X))
    (f#(active(X)) -> f#(X), f#(active(X)) -> f#(X))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (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#(f(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(f(X)) -> f#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
    (mark#(s(X)) -> mark#(X), mark#(g(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(g(X)) -> g#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0()))
    (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(f(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(f(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(f(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> f#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
    (mark#(f(X)) -> mark#(X), mark#(g(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(g(X)) -> g#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
    (mark#(f(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(f(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(0()) -> active#(0()))
    (mark#(f(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(f(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(f(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(f(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
   }
   SCCS:
    Scc:
     {  sel#(X1, mark(X2)) -> sel#(X1, X2),
      sel#(X1, active(X2)) -> sel#(X1, X2),
        sel#(mark(X1), X2) -> sel#(X1, X2),
      sel#(active(X1), X2) -> sel#(X1, X2)}
    Scc:
     {  s#(mark(X)) -> s#(X),
      s#(active(X)) -> s#(X)}
    Scc:
     {  g#(mark(X)) -> g#(X),
      g#(active(X)) -> g#(X)}
    Scc:
     {  f#(mark(X)) -> f#(X),
      f#(active(X)) -> f#(X)}
    Scc:
     {  cons#(X1, mark(X2)) -> cons#(X1, X2),
      cons#(X1, active(X2)) -> cons#(X1, X2),
        cons#(mark(X1), X2) -> cons#(X1, X2),
      cons#(active(X1), X2) -> cons#(X1, X2)}
    Scc:
     {           mark#(cons(X1, X2)) -> mark#(X1),
                 mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                         mark#(f(X)) -> mark#(X),
                         mark#(f(X)) -> active#(f(mark(X))),
                         mark#(g(X)) -> mark#(X),
                         mark#(g(X)) -> active#(g(mark(X))),
                         mark#(s(X)) -> mark#(X),
                         mark#(s(X)) -> active#(s(mark(X))),
                  mark#(sel(X1, X2)) -> mark#(X1),
                  mark#(sel(X1, X2)) -> mark#(X2),
                  mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                       active#(f(X)) -> mark#(cons(X, f(g(X)))),
                    active#(g(s(X))) -> mark#(s(s(g(X)))),
                     active#(g(0())) -> mark#(s(0())),
      active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)),
       active#(sel(0(), cons(X, Y))) -> mark#(X)}
    SCC:
     Strict:
      {  sel#(X1, mark(X2)) -> sel#(X1, X2),
       sel#(X1, active(X2)) -> sel#(X1, X2),
         sel#(mark(X1), X2) -> sel#(X1, X2),
       sel#(active(X1), X2) -> sel#(X1, X2)}
     Weak:
     {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                         mark(f(X)) -> active(f(mark(X))),
                         mark(g(X)) -> active(g(mark(X))),
                         mark(s(X)) -> active(s(mark(X))),
                          mark(0()) -> active(0()),
                  mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                         f(mark(X)) -> f(X),
                       f(active(X)) -> f(X),
                         g(mark(X)) -> g(X),
                       g(active(X)) -> g(X),
                       active(f(X)) -> mark(cons(X, f(g(X)))),
                    active(g(s(X))) -> mark(s(s(g(X)))),
                     active(g(0())) -> mark(s(0())),
      active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
       active(sel(0(), cons(X, Y))) -> mark(X),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                  sel(X1, mark(X2)) -> sel(X1, X2),
                sel(X1, active(X2)) -> sel(X1, X2),
                  sel(mark(X1), X2) -> sel(X1, X2),
                sel(active(X1), X2) -> sel(X1, X2)}
     SPSC:
      Simple Projection:
       pi(sel#) = 0
      Strict:
       {  sel#(X1, mark(X2)) -> sel#(X1, X2),
        sel#(X1, active(X2)) -> sel#(X1, X2),
          sel#(mark(X1), X2) -> sel#(X1, X2)}
      EDG:
       {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
        (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
        (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
        (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
        (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
        (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))}
       SCCS:
        Scc:
         {  sel#(X1, mark(X2)) -> sel#(X1, X2),
          sel#(X1, active(X2)) -> sel#(X1, X2),
            sel#(mark(X1), X2) -> sel#(X1, X2)}
        SCC:
         Strict:
          {  sel#(X1, mark(X2)) -> sel#(X1, X2),
           sel#(X1, active(X2)) -> sel#(X1, X2),
             sel#(mark(X1), X2) -> sel#(X1, X2)}
         Weak:
         {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(f(X)) -> active(f(mark(X))),
                             mark(g(X)) -> active(g(mark(X))),
                             mark(s(X)) -> active(s(mark(X))),
                              mark(0()) -> active(0()),
                      mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                             f(mark(X)) -> f(X),
                           f(active(X)) -> f(X),
                             g(mark(X)) -> g(X),
                           g(active(X)) -> g(X),
                           active(f(X)) -> mark(cons(X, f(g(X)))),
                        active(g(s(X))) -> mark(s(s(g(X)))),
                         active(g(0())) -> mark(s(0())),
          active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
           active(sel(0(), cons(X, Y))) -> mark(X),
                             s(mark(X)) -> s(X),
                           s(active(X)) -> s(X),
                      sel(X1, mark(X2)) -> sel(X1, X2),
                    sel(X1, active(X2)) -> sel(X1, X2),
                      sel(mark(X1), X2) -> sel(X1, X2),
                    sel(active(X1), X2) -> sel(X1, X2)}
         SPSC:
          Simple Projection:
           pi(sel#) = 0
          Strict:
           {  sel#(X1, mark(X2)) -> sel#(X1, X2),
            sel#(X1, active(X2)) -> sel#(X1, X2)}
          EDG:
           {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
            (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
            (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
            (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))}
           SCCS:
            Scc:
             {  sel#(X1, mark(X2)) -> sel#(X1, X2),
              sel#(X1, active(X2)) -> sel#(X1, X2)}
            SCC:
             Strict:
              {  sel#(X1, mark(X2)) -> sel#(X1, X2),
               sel#(X1, active(X2)) -> sel#(X1, X2)}
             Weak:
             {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                 mark(f(X)) -> active(f(mark(X))),
                                 mark(g(X)) -> active(g(mark(X))),
                                 mark(s(X)) -> active(s(mark(X))),
                                  mark(0()) -> active(0()),
                          mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                                 f(mark(X)) -> f(X),
                               f(active(X)) -> f(X),
                                 g(mark(X)) -> g(X),
                               g(active(X)) -> g(X),
                               active(f(X)) -> mark(cons(X, f(g(X)))),
                            active(g(s(X))) -> mark(s(s(g(X)))),
                             active(g(0())) -> mark(s(0())),
              active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
               active(sel(0(), cons(X, Y))) -> mark(X),
                                 s(mark(X)) -> s(X),
                               s(active(X)) -> s(X),
                          sel(X1, mark(X2)) -> sel(X1, X2),
                        sel(X1, active(X2)) -> sel(X1, X2),
                          sel(mark(X1), X2) -> sel(X1, X2),
                        sel(active(X1), X2) -> sel(X1, X2)}
             SPSC:
              Simple Projection:
               pi(sel#) = 1
              Strict:
               {sel#(X1, active(X2)) -> sel#(X1, X2)}
              EDG:
               {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))}
               SCCS:
                Scc:
                 {sel#(X1, active(X2)) -> sel#(X1, X2)}
                SCC:
                 Strict:
                  {sel#(X1, active(X2)) -> sel#(X1, X2)}
                 Weak:
                 {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                     mark(f(X)) -> active(f(mark(X))),
                                     mark(g(X)) -> active(g(mark(X))),
                                     mark(s(X)) -> active(s(mark(X))),
                                      mark(0()) -> active(0()),
                              mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                                     f(mark(X)) -> f(X),
                                   f(active(X)) -> f(X),
                                     g(mark(X)) -> g(X),
                                   g(active(X)) -> g(X),
                                   active(f(X)) -> mark(cons(X, f(g(X)))),
                                active(g(s(X))) -> mark(s(s(g(X)))),
                                 active(g(0())) -> mark(s(0())),
                  active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
                   active(sel(0(), cons(X, Y))) -> mark(X),
                                     s(mark(X)) -> s(X),
                                   s(active(X)) -> s(X),
                              sel(X1, mark(X2)) -> sel(X1, X2),
                            sel(X1, active(X2)) -> sel(X1, X2),
                              sel(mark(X1), X2) -> sel(X1, X2),
                            sel(active(X1), X2) -> sel(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(sel#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {  s#(mark(X)) -> s#(X),
       s#(active(X)) -> s#(X)}
     Weak:
     {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                         mark(f(X)) -> active(f(mark(X))),
                         mark(g(X)) -> active(g(mark(X))),
                         mark(s(X)) -> active(s(mark(X))),
                          mark(0()) -> active(0()),
                  mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                         f(mark(X)) -> f(X),
                       f(active(X)) -> f(X),
                         g(mark(X)) -> g(X),
                       g(active(X)) -> g(X),
                       active(f(X)) -> mark(cons(X, f(g(X)))),
                    active(g(s(X))) -> mark(s(s(g(X)))),
                     active(g(0())) -> mark(s(0())),
      active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
       active(sel(0(), cons(X, Y))) -> mark(X),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                  sel(X1, mark(X2)) -> sel(X1, X2),
                sel(X1, active(X2)) -> sel(X1, X2),
                  sel(mark(X1), X2) -> sel(X1, X2),
                sel(active(X1), X2) -> sel(X1, X2)}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {s#(active(X)) -> s#(X)}
      EDG:
       {(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))}
       SCCS:
        Scc:
         {s#(active(X)) -> s#(X)}
        SCC:
         Strict:
          {s#(active(X)) -> s#(X)}
         Weak:
         {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(f(X)) -> active(f(mark(X))),
                             mark(g(X)) -> active(g(mark(X))),
                             mark(s(X)) -> active(s(mark(X))),
                              mark(0()) -> active(0()),
                      mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                             f(mark(X)) -> f(X),
                           f(active(X)) -> f(X),
                             g(mark(X)) -> g(X),
                           g(active(X)) -> g(X),
                           active(f(X)) -> mark(cons(X, f(g(X)))),
                        active(g(s(X))) -> mark(s(s(g(X)))),
                         active(g(0())) -> mark(s(0())),
          active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
           active(sel(0(), cons(X, Y))) -> mark(X),
                             s(mark(X)) -> s(X),
                           s(active(X)) -> s(X),
                      sel(X1, mark(X2)) -> sel(X1, X2),
                    sel(X1, active(X2)) -> sel(X1, X2),
                      sel(mark(X1), X2) -> sel(X1, X2),
                    sel(active(X1), X2) -> sel(X1, X2)}
         SPSC:
          Simple Projection:
           pi(s#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  g#(mark(X)) -> g#(X),
       g#(active(X)) -> g#(X)}
     Weak:
     {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                         mark(f(X)) -> active(f(mark(X))),
                         mark(g(X)) -> active(g(mark(X))),
                         mark(s(X)) -> active(s(mark(X))),
                          mark(0()) -> active(0()),
                  mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                         f(mark(X)) -> f(X),
                       f(active(X)) -> f(X),
                         g(mark(X)) -> g(X),
                       g(active(X)) -> g(X),
                       active(f(X)) -> mark(cons(X, f(g(X)))),
                    active(g(s(X))) -> mark(s(s(g(X)))),
                     active(g(0())) -> mark(s(0())),
      active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
       active(sel(0(), cons(X, Y))) -> mark(X),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                  sel(X1, mark(X2)) -> sel(X1, X2),
                sel(X1, active(X2)) -> sel(X1, X2),
                  sel(mark(X1), X2) -> sel(X1, X2),
                sel(active(X1), X2) -> sel(X1, X2)}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {g#(active(X)) -> g#(X)}
      EDG:
       {(g#(active(X)) -> g#(X), g#(active(X)) -> g#(X))}
       SCCS:
        Scc:
         {g#(active(X)) -> g#(X)}
        SCC:
         Strict:
          {g#(active(X)) -> g#(X)}
         Weak:
         {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(f(X)) -> active(f(mark(X))),
                             mark(g(X)) -> active(g(mark(X))),
                             mark(s(X)) -> active(s(mark(X))),
                              mark(0()) -> active(0()),
                      mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                             f(mark(X)) -> f(X),
                           f(active(X)) -> f(X),
                             g(mark(X)) -> g(X),
                           g(active(X)) -> g(X),
                           active(f(X)) -> mark(cons(X, f(g(X)))),
                        active(g(s(X))) -> mark(s(s(g(X)))),
                         active(g(0())) -> mark(s(0())),
          active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
           active(sel(0(), cons(X, Y))) -> mark(X),
                             s(mark(X)) -> s(X),
                           s(active(X)) -> s(X),
                      sel(X1, mark(X2)) -> sel(X1, X2),
                    sel(X1, active(X2)) -> sel(X1, X2),
                      sel(mark(X1), X2) -> sel(X1, X2),
                    sel(active(X1), X2) -> sel(X1, X2)}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  f#(mark(X)) -> f#(X),
       f#(active(X)) -> f#(X)}
     Weak:
     {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                         mark(f(X)) -> active(f(mark(X))),
                         mark(g(X)) -> active(g(mark(X))),
                         mark(s(X)) -> active(s(mark(X))),
                          mark(0()) -> active(0()),
                  mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                         f(mark(X)) -> f(X),
                       f(active(X)) -> f(X),
                         g(mark(X)) -> g(X),
                       g(active(X)) -> g(X),
                       active(f(X)) -> mark(cons(X, f(g(X)))),
                    active(g(s(X))) -> mark(s(s(g(X)))),
                     active(g(0())) -> mark(s(0())),
      active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
       active(sel(0(), cons(X, Y))) -> mark(X),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                  sel(X1, mark(X2)) -> sel(X1, X2),
                sel(X1, active(X2)) -> sel(X1, X2),
                  sel(mark(X1), X2) -> sel(X1, X2),
                sel(active(X1), X2) -> sel(X1, X2)}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(active(X)) -> f#(X)}
      EDG:
       {(f#(active(X)) -> f#(X), f#(active(X)) -> f#(X))}
       SCCS:
        Scc:
         {f#(active(X)) -> f#(X)}
        SCC:
         Strict:
          {f#(active(X)) -> f#(X)}
         Weak:
         {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(f(X)) -> active(f(mark(X))),
                             mark(g(X)) -> active(g(mark(X))),
                             mark(s(X)) -> active(s(mark(X))),
                              mark(0()) -> active(0()),
                      mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                             f(mark(X)) -> f(X),
                           f(active(X)) -> f(X),
                             g(mark(X)) -> g(X),
                           g(active(X)) -> g(X),
                           active(f(X)) -> mark(cons(X, f(g(X)))),
                        active(g(s(X))) -> mark(s(s(g(X)))),
                         active(g(0())) -> mark(s(0())),
          active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
           active(sel(0(), cons(X, Y))) -> mark(X),
                             s(mark(X)) -> s(X),
                           s(active(X)) -> s(X),
                      sel(X1, mark(X2)) -> sel(X1, X2),
                    sel(X1, active(X2)) -> sel(X1, X2),
                      sel(mark(X1), X2) -> sel(X1, X2),
                    sel(active(X1), X2) -> sel(X1, X2)}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed
    SCC:
     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(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                         mark(f(X)) -> active(f(mark(X))),
                         mark(g(X)) -> active(g(mark(X))),
                         mark(s(X)) -> active(s(mark(X))),
                          mark(0()) -> active(0()),
                  mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                         f(mark(X)) -> f(X),
                       f(active(X)) -> f(X),
                         g(mark(X)) -> g(X),
                       g(active(X)) -> g(X),
                       active(f(X)) -> mark(cons(X, f(g(X)))),
                    active(g(s(X))) -> mark(s(s(g(X)))),
                     active(g(0())) -> mark(s(0())),
      active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
       active(sel(0(), cons(X, Y))) -> mark(X),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                  sel(X1, mark(X2)) -> sel(X1, X2),
                sel(X1, active(X2)) -> sel(X1, X2),
                  sel(mark(X1), X2) -> sel(X1, X2),
                sel(active(X1), X2) -> sel(X1, X2)}
     SPSC:
      Simple Projection:
       pi(cons#) = 0
      Strict:
       {  cons#(X1, mark(X2)) -> cons#(X1, X2),
        cons#(X1, active(X2)) -> cons#(X1, X2),
          cons#(mark(X1), X2) -> cons#(X1, X2)}
      EDG:
       {(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#(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#(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))}
       SCCS:
        Scc:
         {  cons#(X1, mark(X2)) -> cons#(X1, X2),
          cons#(X1, active(X2)) -> cons#(X1, X2),
            cons#(mark(X1), X2) -> cons#(X1, X2)}
        SCC:
         Strict:
          {  cons#(X1, mark(X2)) -> cons#(X1, X2),
           cons#(X1, active(X2)) -> cons#(X1, X2),
             cons#(mark(X1), X2) -> cons#(X1, X2)}
         Weak:
         {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(f(X)) -> active(f(mark(X))),
                             mark(g(X)) -> active(g(mark(X))),
                             mark(s(X)) -> active(s(mark(X))),
                              mark(0()) -> active(0()),
                      mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                             f(mark(X)) -> f(X),
                           f(active(X)) -> f(X),
                             g(mark(X)) -> g(X),
                           g(active(X)) -> g(X),
                           active(f(X)) -> mark(cons(X, f(g(X)))),
                        active(g(s(X))) -> mark(s(s(g(X)))),
                         active(g(0())) -> mark(s(0())),
          active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
           active(sel(0(), cons(X, Y))) -> mark(X),
                             s(mark(X)) -> s(X),
                           s(active(X)) -> s(X),
                      sel(X1, mark(X2)) -> sel(X1, X2),
                    sel(X1, active(X2)) -> sel(X1, X2),
                      sel(mark(X1), X2) -> sel(X1, X2),
                    sel(active(X1), X2) -> sel(X1, X2)}
         SPSC:
          Simple Projection:
           pi(cons#) = 0
          Strict:
           {  cons#(X1, mark(X2)) -> cons#(X1, X2),
            cons#(X1, active(X2)) -> cons#(X1, X2)}
          EDG:
           {(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#(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))}
           SCCS:
            Scc:
             {  cons#(X1, mark(X2)) -> cons#(X1, X2),
              cons#(X1, active(X2)) -> cons#(X1, X2)}
            SCC:
             Strict:
              {  cons#(X1, mark(X2)) -> cons#(X1, X2),
               cons#(X1, active(X2)) -> cons#(X1, X2)}
             Weak:
             {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                 mark(f(X)) -> active(f(mark(X))),
                                 mark(g(X)) -> active(g(mark(X))),
                                 mark(s(X)) -> active(s(mark(X))),
                                  mark(0()) -> active(0()),
                          mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                                 f(mark(X)) -> f(X),
                               f(active(X)) -> f(X),
                                 g(mark(X)) -> g(X),
                               g(active(X)) -> g(X),
                               active(f(X)) -> mark(cons(X, f(g(X)))),
                            active(g(s(X))) -> mark(s(s(g(X)))),
                             active(g(0())) -> mark(s(0())),
              active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
               active(sel(0(), cons(X, Y))) -> mark(X),
                                 s(mark(X)) -> s(X),
                               s(active(X)) -> s(X),
                          sel(X1, mark(X2)) -> sel(X1, X2),
                        sel(X1, active(X2)) -> sel(X1, X2),
                          sel(mark(X1), X2) -> sel(X1, X2),
                        sel(active(X1), X2) -> sel(X1, X2)}
             SPSC:
              Simple Projection:
               pi(cons#) = 1
              Strict:
               {cons#(X1, active(X2)) -> cons#(X1, X2)}
              EDG:
               {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))}
               SCCS:
                Scc:
                 {cons#(X1, active(X2)) -> cons#(X1, X2)}
                SCC:
                 Strict:
                  {cons#(X1, active(X2)) -> cons#(X1, X2)}
                 Weak:
                 {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                     mark(f(X)) -> active(f(mark(X))),
                                     mark(g(X)) -> active(g(mark(X))),
                                     mark(s(X)) -> active(s(mark(X))),
                                      mark(0()) -> active(0()),
                              mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                                     f(mark(X)) -> f(X),
                                   f(active(X)) -> f(X),
                                     g(mark(X)) -> g(X),
                                   g(active(X)) -> g(X),
                                   active(f(X)) -> mark(cons(X, f(g(X)))),
                                active(g(s(X))) -> mark(s(s(g(X)))),
                                 active(g(0())) -> mark(s(0())),
                  active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
                   active(sel(0(), cons(X, Y))) -> mark(X),
                                     s(mark(X)) -> s(X),
                                   s(active(X)) -> s(X),
                              sel(X1, mark(X2)) -> sel(X1, X2),
                            sel(X1, active(X2)) -> sel(X1, X2),
                              sel(mark(X1), X2) -> sel(X1, X2),
                            sel(active(X1), X2) -> sel(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(cons#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {           mark#(cons(X1, X2)) -> mark#(X1),
                  mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                          mark#(f(X)) -> mark#(X),
                          mark#(f(X)) -> active#(f(mark(X))),
                          mark#(g(X)) -> mark#(X),
                          mark#(g(X)) -> active#(g(mark(X))),
                          mark#(s(X)) -> mark#(X),
                          mark#(s(X)) -> active#(s(mark(X))),
                   mark#(sel(X1, X2)) -> mark#(X1),
                   mark#(sel(X1, X2)) -> mark#(X2),
                   mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                        active#(f(X)) -> mark#(cons(X, f(g(X)))),
                     active#(g(s(X))) -> mark#(s(s(g(X)))),
                      active#(g(0())) -> mark#(s(0())),
       active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)),
        active#(sel(0(), cons(X, Y))) -> mark#(X)}
     Weak:
     {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                         mark(f(X)) -> active(f(mark(X))),
                         mark(g(X)) -> active(g(mark(X))),
                         mark(s(X)) -> active(s(mark(X))),
                          mark(0()) -> active(0()),
                  mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                         f(mark(X)) -> f(X),
                       f(active(X)) -> f(X),
                         g(mark(X)) -> g(X),
                       g(active(X)) -> g(X),
                       active(f(X)) -> mark(cons(X, f(g(X)))),
                    active(g(s(X))) -> mark(s(s(g(X)))),
                     active(g(0())) -> mark(s(0())),
      active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
       active(sel(0(), cons(X, Y))) -> mark(X),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                  sel(X1, mark(X2)) -> sel(X1, X2),
                sel(X1, active(X2)) -> sel(X1, X2),
                  sel(mark(X1), X2) -> sel(X1, X2),
                sel(active(X1), X2) -> sel(X1, X2)}
     POLY:
      Argument Filtering:
       pi(sel) = [], pi(0) = [], pi(s) = [], pi(active#) = 0, pi(active) = [], pi(g) = [], pi(f) = [], pi(cons) = [], pi(mark#) = [], pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [mark#] = 1,
       [sel] = 1,
       [cons] = 0,
       [s] = 0,
       [g] = 1,
       [f] = 1
      Strict:
       {           mark#(cons(X1, X2)) -> mark#(X1),
                           mark#(f(X)) -> mark#(X),
                           mark#(f(X)) -> active#(f(mark(X))),
                           mark#(g(X)) -> mark#(X),
                           mark#(g(X)) -> active#(g(mark(X))),
                           mark#(s(X)) -> mark#(X),
                    mark#(sel(X1, X2)) -> mark#(X1),
                    mark#(sel(X1, X2)) -> mark#(X2),
                    mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                         active#(f(X)) -> mark#(cons(X, f(g(X)))),
                      active#(g(s(X))) -> mark#(s(s(g(X)))),
                       active#(g(0())) -> mark#(s(0())),
        active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)),
         active#(sel(0(), cons(X, Y))) -> mark#(X)}
      Weak:
       {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(f(X)) -> active(f(mark(X))),
                           mark(g(X)) -> active(g(mark(X))),
                           mark(s(X)) -> active(s(mark(X))),
                            mark(0()) -> active(0()),
                    mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                           f(mark(X)) -> f(X),
                         f(active(X)) -> f(X),
                           g(mark(X)) -> g(X),
                         g(active(X)) -> g(X),
                         active(f(X)) -> mark(cons(X, f(g(X)))),
                      active(g(s(X))) -> mark(s(s(g(X)))),
                       active(g(0())) -> mark(s(0())),
        active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
         active(sel(0(), cons(X, Y))) -> mark(X),
                           s(mark(X)) -> s(X),
                         s(active(X)) -> s(X),
                    sel(X1, mark(X2)) -> sel(X1, X2),
                  sel(X1, active(X2)) -> sel(X1, X2),
                    sel(mark(X1), X2) -> sel(X1, X2),
                  sel(active(X1), X2) -> sel(X1, X2)}
      EDG:
       {(mark#(g(X)) -> active#(g(mark(X))), active#(sel(0(), cons(X, Y))) -> mark#(X))
        (mark#(g(X)) -> active#(g(mark(X))), active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)))
        (mark#(g(X)) -> active#(g(mark(X))), active#(g(0())) -> mark#(s(0())))
        (mark#(g(X)) -> active#(g(mark(X))), active#(g(s(X))) -> mark#(s(s(g(X)))))
        (mark#(g(X)) -> active#(g(mark(X))), active#(f(X)) -> mark#(cons(X, f(g(X)))))
        (active#(g(0())) -> mark#(s(0())), mark#(s(X)) -> mark#(X))
        (mark#(g(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(g(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(g(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(g(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(g(X)) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
        (mark#(g(X)) -> mark#(X), mark#(g(X)) -> mark#(X))
        (mark#(g(X)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(g(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
        (mark#(g(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(s(X)) -> mark#(X))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(g(X)) -> mark#(X))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(f(X)) -> mark#(X))
        (active#(sel(0(), cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(g(X)) -> active#(g(mark(X))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(g(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(0(), cons(X, Y))) -> mark#(X))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(g(0())) -> mark#(s(0())))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(g(s(X))) -> mark#(s(s(g(X)))))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(f(X)) -> mark#(cons(X, f(g(X)))))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(s(X)) -> mark#(X))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(g(X)) -> active#(g(mark(X))))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(g(X)) -> mark#(X))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(f(X)) -> active#(f(mark(X))))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(f(X)) -> mark#(X))
        (active#(g(s(X))) -> mark#(s(s(g(X)))), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(f(X)) -> mark#(X))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(f(X)) -> active#(f(mark(X))))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(g(X)) -> mark#(X))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(g(X)) -> active#(g(mark(X))))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(s(X)) -> mark#(X))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(f(X)) -> mark#(cons(X, f(g(X)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(f(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(g(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(g(X)) -> active#(g(mark(X))))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(f(X)) -> mark#(X))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(f(X)) -> active#(f(mark(X))))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(g(X)) -> mark#(X))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(g(X)) -> active#(g(mark(X))))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(s(X)) -> mark#(X))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(s(X)) -> mark#(X), mark#(g(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(f(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
        (mark#(f(X)) -> mark#(X), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(f(X)) -> mark#(X), mark#(g(X)) -> mark#(X))
        (mark#(f(X)) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
        (mark#(f(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(f(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(f(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(f(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(f(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(f(X)) -> active#(f(mark(X))))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(g(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(g(X)) -> active#(g(mark(X))))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(f(X)) -> active#(f(mark(X))), active#(f(X)) -> mark#(cons(X, f(g(X)))))
        (mark#(f(X)) -> active#(f(mark(X))), active#(g(s(X))) -> mark#(s(s(g(X)))))
        (mark#(f(X)) -> active#(f(mark(X))), active#(g(0())) -> mark#(s(0())))
        (mark#(f(X)) -> active#(f(mark(X))), active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)))
        (mark#(f(X)) -> active#(f(mark(X))), active#(sel(0(), cons(X, Y))) -> mark#(X))}
       SCCS:
        Scc:
         {           mark#(cons(X1, X2)) -> mark#(X1),
                             mark#(f(X)) -> mark#(X),
                             mark#(f(X)) -> active#(f(mark(X))),
                             mark#(g(X)) -> mark#(X),
                             mark#(g(X)) -> active#(g(mark(X))),
                             mark#(s(X)) -> mark#(X),
                      mark#(sel(X1, X2)) -> mark#(X1),
                      mark#(sel(X1, X2)) -> mark#(X2),
                      mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                           active#(f(X)) -> mark#(cons(X, f(g(X)))),
                        active#(g(s(X))) -> mark#(s(s(g(X)))),
                         active#(g(0())) -> mark#(s(0())),
          active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)),
           active#(sel(0(), cons(X, Y))) -> mark#(X)}
        SCC:
         Strict:
          {           mark#(cons(X1, X2)) -> mark#(X1),
                              mark#(f(X)) -> mark#(X),
                              mark#(f(X)) -> active#(f(mark(X))),
                              mark#(g(X)) -> mark#(X),
                              mark#(g(X)) -> active#(g(mark(X))),
                              mark#(s(X)) -> mark#(X),
                       mark#(sel(X1, X2)) -> mark#(X1),
                       mark#(sel(X1, X2)) -> mark#(X2),
                       mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                            active#(f(X)) -> mark#(cons(X, f(g(X)))),
                         active#(g(s(X))) -> mark#(s(s(g(X)))),
                          active#(g(0())) -> mark#(s(0())),
           active#(sel(s(X), cons(Y, Z))) -> mark#(sel(X, Z)),
            active#(sel(0(), cons(X, Y))) -> mark#(X)}
         Weak:
         {           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(f(X)) -> active(f(mark(X))),
                             mark(g(X)) -> active(g(mark(X))),
                             mark(s(X)) -> active(s(mark(X))),
                              mark(0()) -> active(0()),
                      mark(sel(X1, X2)) -> active(sel(mark(X1), mark(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),
                             f(mark(X)) -> f(X),
                           f(active(X)) -> f(X),
                             g(mark(X)) -> g(X),
                           g(active(X)) -> g(X),
                           active(f(X)) -> mark(cons(X, f(g(X)))),
                        active(g(s(X))) -> mark(s(s(g(X)))),
                         active(g(0())) -> mark(s(0())),
          active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
           active(sel(0(), cons(X, Y))) -> mark(X),
                             s(mark(X)) -> s(X),
                           s(active(X)) -> s(X),
                      sel(X1, mark(X2)) -> sel(X1, X2),
                    sel(X1, active(X2)) -> sel(X1, X2),
                      sel(mark(X1), X2) -> sel(X1, X2),
                    sel(active(X1), X2) -> sel(X1, X2)}
         Fail