MAYBE
Time: 0.008456
TRS:
 {                 a__sqr X -> sqr X,
                 a__sqr s X -> s add(sqr X, dbl 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 X,
                   mark 0() -> 0(),
           mark add(X1, X2) -> a__add(mark X1, mark X2),
                 mark sqr X -> a__sqr mark X,
                 mark dbl X -> a__dbl mark X,
                 mark nil() -> nil(),
         mark first(X1, X2) -> a__first(mark X1, mark X2),
                 a__terms N -> cons(recip a__sqr mark N, terms s N),
                 a__terms X -> terms X,
                   a__dbl X -> dbl X,
                 a__dbl s X -> s s dbl X,
                 a__dbl 0() -> 0(),
             a__add(X1, X2) -> add(X1, X2),
             a__add(s X, Y) -> s add(X, Y),
             a__add(0(), X) -> mark X,
           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:
  DP:
   {        mark# cons(X1, X2) -> mark# X1,
                 mark# recip X -> mark# X,
                 mark# terms X -> mark# X,
                 mark# terms X -> a__terms# 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# sqr X -> a__sqr# mark X,
                   mark# sqr X -> mark# X,
                   mark# dbl X -> mark# X,
                   mark# dbl X -> a__dbl# mark X,
           mark# first(X1, X2) -> mark# X1,
           mark# first(X1, X2) -> mark# X2,
           mark# first(X1, X2) -> a__first#(mark X1, mark X2),
                   a__terms# N -> a__sqr# mark N,
                   a__terms# N -> mark# N,
               a__add#(0(), X) -> mark# X,
    a__first#(s X, cons(Y, Z)) -> mark# Y}
  TRS:
  {                 a__sqr X -> sqr X,
                  a__sqr s X -> s add(sqr X, dbl 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 X,
                    mark 0() -> 0(),
            mark add(X1, X2) -> a__add(mark X1, mark X2),
                  mark sqr X -> a__sqr mark X,
                  mark dbl X -> a__dbl mark X,
                  mark nil() -> nil(),
          mark first(X1, X2) -> a__first(mark X1, mark X2),
                  a__terms N -> cons(recip a__sqr mark N, terms s N),
                  a__terms X -> terms X,
                    a__dbl X -> dbl X,
                  a__dbl s X -> s s dbl X,
                  a__dbl 0() -> 0(),
              a__add(X1, X2) -> add(X1, X2),
              a__add(s X, Y) -> s add(X, Y),
              a__add(0(), X) -> mark X,
            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:
   {
    (mark# terms X -> a__terms# mark X, a__terms# N -> mark# N)
    (mark# terms X -> a__terms# mark X, a__terms# N -> a__sqr# mark N)
    (mark# recip X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (mark# recip X -> mark# X, mark# first(X1, X2) -> mark# X2)
    (mark# recip X -> mark# X, mark# first(X1, X2) -> mark# X1)
    (mark# recip X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (mark# recip X -> mark# X, mark# dbl X -> mark# X)
    (mark# recip X -> mark# X, mark# sqr X -> mark# X)
    (mark# recip X -> mark# X, mark# sqr X -> a__sqr# mark X)
    (mark# recip X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
    (mark# recip X -> mark# X, mark# add(X1, X2) -> mark# X2)
    (mark# recip X -> mark# X, mark# add(X1, X2) -> mark# X1)
    (mark# recip X -> mark# X, mark# terms X -> a__terms# mark X)
    (mark# recip X -> mark# X, mark# terms X -> mark# X)
    (mark# recip X -> mark# X, mark# recip X -> mark# X)
    (mark# recip X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (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# dbl X -> a__dbl# mark X)
    (mark# sqr X -> mark# X, mark# dbl X -> mark# X)
    (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# 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# 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#(0(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2)
    (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1)
    (a__add#(0(), X) -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__add#(0(), X) -> mark# X, mark# dbl X -> mark# X)
    (a__add#(0(), X) -> mark# X, mark# sqr X -> mark# X)
    (a__add#(0(), X) -> mark# X, mark# sqr X -> a__sqr# mark X)
    (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
    (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
    (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
    (a__add#(0(), X) -> mark# X, mark# terms X -> a__terms# mark X)
    (a__add#(0(), X) -> mark# X, mark# terms X -> mark# X)
    (a__add#(0(), X) -> mark# X, mark# recip X -> mark# X)
    (a__add#(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__first#(s X, cons(Y, Z)) -> mark# Y)
    (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2)
    (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X)
    (mark# add(X1, X2) -> mark# X2, mark# dbl X -> mark# X)
    (mark# add(X1, X2) -> mark# X2, mark# sqr X -> mark# X)
    (mark# add(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X)
    (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
    (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2)
    (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X2, mark# terms X -> a__terms# mark X)
    (mark# add(X1, X2) -> mark# X2, mark# terms X -> mark# X)
    (mark# add(X1, X2) -> mark# X2, mark# recip X -> mark# X)
    (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
    (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
    (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# terms X -> a__terms# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# terms X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
    (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# dbl X -> a__dbl# mark X)
    (mark# first(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
    (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# 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# 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)
    (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# 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# sqr X -> a__sqr# mark X)
    (mark# add(X1, X2) -> mark# X1, mark# sqr X -> mark# X)
    (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# 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# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# recip X -> mark# X)
    (mark# first(X1, X2) -> mark# X2, mark# terms X -> mark# X)
    (mark# first(X1, X2) -> mark# X2, mark# terms X -> a__terms# mark X)
    (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2)
    (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X)
    (mark# first(X1, X2) -> mark# X2, mark# sqr X -> mark# X)
    (mark# first(X1, X2) -> mark# X2, mark# dbl X -> mark# X)
    (mark# first(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X)
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2)
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (a__terms# N -> mark# N, mark# cons(X1, X2) -> mark# X1)
    (a__terms# N -> mark# N, mark# recip X -> mark# X)
    (a__terms# N -> mark# N, mark# terms X -> mark# X)
    (a__terms# N -> mark# N, mark# terms X -> a__terms# mark X)
    (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X1)
    (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X2)
    (a__terms# N -> mark# N, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
    (a__terms# N -> mark# N, mark# sqr X -> a__sqr# mark X)
    (a__terms# N -> mark# N, mark# sqr X -> mark# X)
    (a__terms# N -> mark# N, mark# dbl X -> mark# X)
    (a__terms# N -> mark# N, mark# dbl X -> a__dbl# mark X)
    (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X1)
    (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X2)
    (a__terms# N -> mark# N, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (mark# add(X1, X2) -> a__add#(mark X1, mark X2), a__add#(0(), X) -> 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# 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# sqr X -> a__sqr# mark X)
    (mark# dbl X -> mark# X, mark# sqr X -> mark# X)
    (mark# dbl X -> mark# X, mark# dbl X -> mark# X)
    (mark# dbl X -> mark# X, mark# dbl X -> a__dbl# 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# terms X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# terms X -> mark# X, mark# recip X -> mark# X)
    (mark# terms X -> mark# X, mark# terms X -> mark# X)
    (mark# terms X -> mark# X, mark# terms X -> a__terms# mark X)
    (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X1)
    (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X2)
    (mark# terms X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
    (mark# terms X -> mark# X, mark# sqr X -> a__sqr# mark X)
    (mark# terms X -> mark# X, mark# sqr X -> mark# X)
    (mark# terms X -> mark# X, mark# dbl X -> mark# X)
    (mark# terms X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X1)
    (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X2)
    (mark# terms X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (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# 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# 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# dbl X -> mark# X)
    (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> a__dbl# 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))
   }
   STATUS:
    arrows: 0.469136
    SCCS (1):
     Scc:
      {        mark# cons(X1, X2) -> mark# X1,
                    mark# recip X -> mark# X,
                    mark# terms X -> mark# X,
                    mark# terms X -> a__terms# 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# sqr X -> mark# X,
                      mark# dbl 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),
                      a__terms# N -> mark# N,
                  a__add#(0(), X) -> mark# X,
       a__first#(s X, cons(Y, Z)) -> mark# Y}
     
     SCC (15):
      Strict:
       {        mark# cons(X1, X2) -> mark# X1,
                     mark# recip X -> mark# X,
                     mark# terms X -> mark# X,
                     mark# terms X -> a__terms# 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# sqr X -> mark# X,
                       mark# dbl 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),
                       a__terms# N -> mark# N,
                   a__add#(0(), X) -> mark# X,
        a__first#(s X, cons(Y, Z)) -> mark# Y}
      Weak:
      {                 a__sqr X -> sqr X,
                      a__sqr s X -> s add(sqr X, dbl 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 X,
                        mark 0() -> 0(),
                mark add(X1, X2) -> a__add(mark X1, mark X2),
                      mark sqr X -> a__sqr mark X,
                      mark dbl X -> a__dbl mark X,
                      mark nil() -> nil(),
              mark first(X1, X2) -> a__first(mark X1, mark X2),
                      a__terms N -> cons(recip a__sqr mark N, terms s N),
                      a__terms X -> terms X,
                        a__dbl X -> dbl X,
                      a__dbl s X -> s s dbl X,
                      a__dbl 0() -> 0(),
                  a__add(X1, X2) -> add(X1, X2),
                  a__add(s X, Y) -> s add(X, Y),
                  a__add(0(), X) -> mark X,
                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()}
      Open