MAYBE
TRS:
 {                 a__sqr(X) -> sqr(X),
                a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))),
                 a__sqr(0()) -> 0(),
          mark(cons(X1, X2)) -> cons(mark(X1), X2),
              mark(recip(X)) -> recip(mark(X)),
              mark(terms(X)) -> a__terms(mark(X)),
                  mark(s(X)) -> s(mark(X)),
                   mark(0()) -> 0(),
                 mark(nil()) -> nil(),
         mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                mark(sqr(X)) -> a__sqr(mark(X)),
           mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                mark(dbl(X)) -> a__dbl(mark(X)),
                 a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                 a__terms(X) -> terms(X),
              a__add(X1, X2) -> add(X1, X2),
             a__add(s(X), Y) -> s(a__add(mark(X), mark(Y))),
              a__add(0(), X) -> mark(X),
                   a__dbl(X) -> dbl(X),
                a__dbl(s(X)) -> s(s(a__dbl(mark(X)))),
                 a__dbl(0()) -> 0(),
            a__first(X1, X2) -> first(X1, X2),
  a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
            a__first(0(), X) -> nil()}
 DP:
  Strict:
   {              a__sqr#(s(X)) -> a__sqr#(mark(X)),
                  a__sqr#(s(X)) -> mark#(X),
                  a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))),
                  a__sqr#(s(X)) -> a__dbl#(mark(X)),
            mark#(cons(X1, X2)) -> mark#(X1),
                mark#(recip(X)) -> mark#(X),
                mark#(terms(X)) -> mark#(X),
                mark#(terms(X)) -> a__terms#(mark(X)),
                    mark#(s(X)) -> mark#(X),
           mark#(first(X1, X2)) -> mark#(X1),
           mark#(first(X1, X2)) -> mark#(X2),
           mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                  mark#(sqr(X)) -> a__sqr#(mark(X)),
                  mark#(sqr(X)) -> mark#(X),
             mark#(add(X1, X2)) -> mark#(X1),
             mark#(add(X1, X2)) -> mark#(X2),
             mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                  mark#(dbl(X)) -> mark#(X),
                  mark#(dbl(X)) -> a__dbl#(mark(X)),
                   a__terms#(N) -> a__sqr#(mark(N)),
                   a__terms#(N) -> mark#(N),
               a__add#(s(X), Y) -> mark#(X),
               a__add#(s(X), Y) -> mark#(Y),
               a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)),
                a__add#(0(), X) -> mark#(X),
                  a__dbl#(s(X)) -> mark#(X),
                  a__dbl#(s(X)) -> a__dbl#(mark(X)),
    a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
  Weak:
  {                 a__sqr(X) -> sqr(X),
                 a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))),
                  a__sqr(0()) -> 0(),
           mark(cons(X1, X2)) -> cons(mark(X1), X2),
               mark(recip(X)) -> recip(mark(X)),
               mark(terms(X)) -> a__terms(mark(X)),
                   mark(s(X)) -> s(mark(X)),
                    mark(0()) -> 0(),
                  mark(nil()) -> nil(),
          mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                 mark(sqr(X)) -> a__sqr(mark(X)),
            mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                 mark(dbl(X)) -> a__dbl(mark(X)),
                  a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                  a__terms(X) -> terms(X),
               a__add(X1, X2) -> add(X1, X2),
              a__add(s(X), Y) -> s(a__add(mark(X), mark(Y))),
               a__add(0(), X) -> mark(X),
                    a__dbl(X) -> dbl(X),
                 a__dbl(s(X)) -> s(s(a__dbl(mark(X)))),
                  a__dbl(0()) -> 0(),
             a__first(X1, X2) -> first(X1, X2),
   a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
             a__first(0(), X) -> nil()}
  EDG:
   {
    (a__add#(s(X), Y) -> mark#(Y), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(dbl(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2))
    (a__add#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(Y), mark#(sqr(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(Y), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
    (a__add#(s(X), Y) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(Y), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(terms(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(Y), mark#(recip(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (a__sqr#(s(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__sqr#(s(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (a__sqr#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__sqr#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__sqr#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__sqr#(s(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (a__sqr#(s(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__sqr#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__sqr#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__sqr#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__sqr#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__sqr#(s(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__sqr#(s(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (a__sqr#(s(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (a__sqr#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(terms(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(terms(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(terms(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(terms(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(sqr(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__add#(s(X), Y) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__add#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__add#(s(X), Y) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__add#(s(X), Y) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__add#(s(X), Y) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__dbl#(s(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__dbl#(s(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (a__dbl#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__dbl#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__dbl#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__dbl#(s(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (a__dbl#(s(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__dbl#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__dbl#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__dbl#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__dbl#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__dbl#(s(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__dbl#(s(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (a__dbl#(s(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (a__dbl#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (a__terms#(N) -> mark#(N), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__terms#(N) -> mark#(N), mark#(dbl(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> mark#(X2))
    (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> mark#(X1))
    (a__terms#(N) -> mark#(N), mark#(sqr(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X2))
    (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X1))
    (a__terms#(N) -> mark#(N), mark#(s(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__terms#(N) -> mark#(N), mark#(terms(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(recip(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1))
    (a__sqr#(s(X)) -> a__dbl#(mark(X)), a__dbl#(s(X)) -> a__dbl#(mark(X)))
    (a__sqr#(s(X)) -> a__dbl#(mark(X)), a__dbl#(s(X)) -> mark#(X))
    (mark#(sqr(X)) -> a__sqr#(mark(X)), a__sqr#(s(X)) -> a__dbl#(mark(X)))
    (mark#(sqr(X)) -> a__sqr#(mark(X)), a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))))
    (mark#(sqr(X)) -> a__sqr#(mark(X)), a__sqr#(s(X)) -> mark#(X))
    (mark#(sqr(X)) -> a__sqr#(mark(X)), a__sqr#(s(X)) -> a__sqr#(mark(X)))
    (a__dbl#(s(X)) -> a__dbl#(mark(X)), a__dbl#(s(X)) -> a__dbl#(mark(X)))
    (a__dbl#(s(X)) -> a__dbl#(mark(X)), a__dbl#(s(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y))
    (a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)), a__add#(0(), X) -> mark#(X))
    (a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)), a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)))
    (a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)), a__add#(s(X), Y) -> mark#(Y))
    (a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)), a__add#(s(X), Y) -> mark#(X))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(s(X), Y) -> mark#(X))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(s(X), Y) -> mark#(Y))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X))
    (a__terms#(N) -> a__sqr#(mark(N)), a__sqr#(s(X)) -> a__sqr#(mark(X)))
    (a__terms#(N) -> a__sqr#(mark(N)), a__sqr#(s(X)) -> mark#(X))
    (a__terms#(N) -> a__sqr#(mark(N)), a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))))
    (a__terms#(N) -> a__sqr#(mark(N)), a__sqr#(s(X)) -> a__dbl#(mark(X)))
    (mark#(dbl(X)) -> a__dbl#(mark(X)), a__dbl#(s(X)) -> mark#(X))
    (mark#(dbl(X)) -> a__dbl#(mark(X)), a__dbl#(s(X)) -> a__dbl#(mark(X)))
    (mark#(terms(X)) -> a__terms#(mark(X)), a__terms#(N) -> a__sqr#(mark(N)))
    (mark#(terms(X)) -> a__terms#(mark(X)), a__terms#(N) -> mark#(N))
    (a__sqr#(s(X)) -> a__sqr#(mark(X)), a__sqr#(s(X)) -> a__sqr#(mark(X)))
    (a__sqr#(s(X)) -> a__sqr#(mark(X)), a__sqr#(s(X)) -> mark#(X))
    (a__sqr#(s(X)) -> a__sqr#(mark(X)), a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))))
    (a__sqr#(s(X)) -> a__sqr#(mark(X)), a__sqr#(s(X)) -> a__dbl#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(dbl(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(dbl(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(dbl(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(recip(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(terms(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))), a__add#(s(X), Y) -> mark#(X))
    (a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))), a__add#(s(X), Y) -> mark#(Y))
    (a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))), a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)))
    (a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))), a__add#(0(), X) -> mark#(X))
   }
   SCCS:
    Scc:
     {              a__sqr#(s(X)) -> a__sqr#(mark(X)),
                    a__sqr#(s(X)) -> mark#(X),
                    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))),
                    a__sqr#(s(X)) -> a__dbl#(mark(X)),
              mark#(cons(X1, X2)) -> mark#(X1),
                  mark#(recip(X)) -> mark#(X),
                  mark#(terms(X)) -> mark#(X),
                  mark#(terms(X)) -> a__terms#(mark(X)),
                      mark#(s(X)) -> mark#(X),
             mark#(first(X1, X2)) -> mark#(X1),
             mark#(first(X1, X2)) -> mark#(X2),
             mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                    mark#(sqr(X)) -> a__sqr#(mark(X)),
                    mark#(sqr(X)) -> mark#(X),
               mark#(add(X1, X2)) -> mark#(X1),
               mark#(add(X1, X2)) -> mark#(X2),
               mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                    mark#(dbl(X)) -> mark#(X),
                    mark#(dbl(X)) -> a__dbl#(mark(X)),
                     a__terms#(N) -> a__sqr#(mark(N)),
                     a__terms#(N) -> mark#(N),
                 a__add#(s(X), Y) -> mark#(X),
                 a__add#(s(X), Y) -> mark#(Y),
                 a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)),
                  a__add#(0(), X) -> mark#(X),
                    a__dbl#(s(X)) -> mark#(X),
                    a__dbl#(s(X)) -> a__dbl#(mark(X)),
      a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
    SCC:
     Strict:
      {              a__sqr#(s(X)) -> a__sqr#(mark(X)),
                     a__sqr#(s(X)) -> mark#(X),
                     a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)), a__dbl(mark(X))),
                     a__sqr#(s(X)) -> a__dbl#(mark(X)),
               mark#(cons(X1, X2)) -> mark#(X1),
                   mark#(recip(X)) -> mark#(X),
                   mark#(terms(X)) -> mark#(X),
                   mark#(terms(X)) -> a__terms#(mark(X)),
                       mark#(s(X)) -> mark#(X),
              mark#(first(X1, X2)) -> mark#(X1),
              mark#(first(X1, X2)) -> mark#(X2),
              mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                     mark#(sqr(X)) -> a__sqr#(mark(X)),
                     mark#(sqr(X)) -> mark#(X),
                mark#(add(X1, X2)) -> mark#(X1),
                mark#(add(X1, X2)) -> mark#(X2),
                mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                     mark#(dbl(X)) -> mark#(X),
                     mark#(dbl(X)) -> a__dbl#(mark(X)),
                      a__terms#(N) -> a__sqr#(mark(N)),
                      a__terms#(N) -> mark#(N),
                  a__add#(s(X), Y) -> mark#(X),
                  a__add#(s(X), Y) -> mark#(Y),
                  a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)),
                   a__add#(0(), X) -> mark#(X),
                     a__dbl#(s(X)) -> mark#(X),
                     a__dbl#(s(X)) -> a__dbl#(mark(X)),
       a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
     Weak:
     {                 a__sqr(X) -> sqr(X),
                    a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))),
                     a__sqr(0()) -> 0(),
              mark(cons(X1, X2)) -> cons(mark(X1), X2),
                  mark(recip(X)) -> recip(mark(X)),
                  mark(terms(X)) -> a__terms(mark(X)),
                      mark(s(X)) -> s(mark(X)),
                       mark(0()) -> 0(),
                     mark(nil()) -> nil(),
             mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                    mark(sqr(X)) -> a__sqr(mark(X)),
               mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                    mark(dbl(X)) -> a__dbl(mark(X)),
                     a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                     a__terms(X) -> terms(X),
                  a__add(X1, X2) -> add(X1, X2),
                 a__add(s(X), Y) -> s(a__add(mark(X), mark(Y))),
                  a__add(0(), X) -> mark(X),
                       a__dbl(X) -> dbl(X),
                    a__dbl(s(X)) -> s(s(a__dbl(mark(X)))),
                     a__dbl(0()) -> 0(),
                a__first(X1, X2) -> first(X1, X2),
      a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                a__first(0(), X) -> nil()}
     Fail