MAYBE
Time: 0.047047
TRS:
 {                    sqr X -> n__sqr X,
                    sqr 0() -> 0(),
                    sqr s X -> s n__add(n__sqr activate X, n__dbl activate X),
                    terms N -> cons(recip sqr N, n__terms n__s N),
                    terms X -> n__terms X,
                        s X -> n__s X,
                 activate X -> X,
        activate n__terms X -> terms activate X,
            activate n__s X -> s X,
    activate n__add(X1, X2) -> add(activate X1, activate X2),
          activate n__sqr X -> sqr activate X,
          activate n__dbl X -> dbl activate X,
  activate n__first(X1, X2) -> first(activate X1, activate X2),
                      dbl X -> n__dbl X,
                    dbl 0() -> 0(),
                    dbl s X -> s n__s n__dbl activate X,
                add(X1, X2) -> n__add(X1, X2),
                add(0(), X) -> X,
                add(s X, Y) -> s n__add(activate X, Y),
              first(X1, X2) -> n__first(X1, X2),
              first(0(), X) -> nil(),
     first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z))}
 DP:
  DP:
   {                  sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X),
                      sqr# s X -> activate# X,
                      terms# N -> sqr# N,
          activate# n__terms X -> terms# activate X,
          activate# n__terms X -> activate# X,
              activate# n__s X -> s# X,
      activate# n__add(X1, X2) -> activate# X1,
      activate# n__add(X1, X2) -> activate# X2,
      activate# n__add(X1, X2) -> add#(activate X1, activate X2),
            activate# n__sqr X -> sqr# activate X,
            activate# n__sqr X -> activate# X,
            activate# n__dbl X -> activate# X,
            activate# n__dbl X -> dbl# activate X,
    activate# n__first(X1, X2) -> activate# X1,
    activate# n__first(X1, X2) -> activate# X2,
    activate# n__first(X1, X2) -> first#(activate X1, activate X2),
                      dbl# s X -> s# n__s n__dbl activate X,
                      dbl# s X -> activate# X,
                  add#(s X, Y) -> s# n__add(activate X, Y),
                  add#(s X, Y) -> activate# X,
       first#(s X, cons(Y, Z)) -> activate# X,
       first#(s X, cons(Y, Z)) -> activate# Z}
  TRS:
  {                    sqr X -> n__sqr X,
                     sqr 0() -> 0(),
                     sqr s X -> s n__add(n__sqr activate X, n__dbl activate X),
                     terms N -> cons(recip sqr N, n__terms n__s N),
                     terms X -> n__terms X,
                         s X -> n__s X,
                  activate X -> X,
         activate n__terms X -> terms activate X,
             activate n__s X -> s X,
     activate n__add(X1, X2) -> add(activate X1, activate X2),
           activate n__sqr X -> sqr activate X,
           activate n__dbl X -> dbl activate X,
   activate n__first(X1, X2) -> first(activate X1, activate X2),
                       dbl X -> n__dbl X,
                     dbl 0() -> 0(),
                     dbl s X -> s n__s n__dbl activate X,
                 add(X1, X2) -> n__add(X1, X2),
                 add(0(), X) -> X,
                 add(s X, Y) -> s n__add(activate X, Y),
               first(X1, X2) -> n__first(X1, X2),
               first(0(), X) -> nil(),
      first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z))}
  UR:
   {                    sqr X -> n__sqr X,
                      sqr 0() -> 0(),
                      sqr s X -> s n__add(n__sqr activate X, n__dbl activate X),
                      terms N -> cons(recip sqr N, n__terms n__s N),
                      terms X -> n__terms X,
                          s X -> n__s X,
                   activate X -> X,
          activate n__terms X -> terms activate X,
              activate n__s X -> s X,
      activate n__add(X1, X2) -> add(activate X1, activate X2),
            activate n__sqr X -> sqr activate X,
            activate n__dbl X -> dbl activate X,
    activate n__first(X1, X2) -> first(activate X1, activate X2),
                        dbl X -> n__dbl X,
                      dbl 0() -> 0(),
                      dbl s X -> s n__s n__dbl activate X,
                  add(X1, X2) -> n__add(X1, X2),
                  add(0(), X) -> X,
                  add(s X, Y) -> s n__add(activate X, Y),
                first(X1, X2) -> n__first(X1, X2),
                first(0(), X) -> nil(),
       first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)),
                      a(x, y) -> x,
                      a(x, y) -> y}
   EDG:
    {
     (sqr# s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (sqr# s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (sqr# s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (sqr# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (sqr# s X -> activate# X, activate# n__dbl X -> activate# X)
     (sqr# s X -> activate# X, activate# n__sqr X -> activate# X)
     (sqr# s X -> activate# X, activate# n__sqr X -> sqr# activate X)
     (sqr# s X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (sqr# s X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (sqr# s X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (sqr# s X -> activate# X, activate# n__s X -> s# X)
     (sqr# s X -> activate# X, activate# n__terms X -> activate# X)
     (sqr# s X -> activate# X, activate# n__terms X -> terms# activate X)
     (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__dbl X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (activate# n__dbl X -> activate# X, activate# n__dbl X -> activate# X)
     (activate# n__dbl X -> activate# X, activate# n__sqr X -> activate# X)
     (activate# n__dbl X -> activate# X, activate# n__sqr X -> sqr# activate X)
     (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__dbl X -> activate# X, activate# n__s X -> s# X)
     (activate# n__dbl X -> activate# X, activate# n__terms X -> activate# X)
     (activate# n__dbl X -> activate# X, activate# n__terms X -> terms# activate X)
     (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (add#(s X, Y) -> activate# X, activate# n__dbl X -> dbl# activate X)
     (add#(s X, Y) -> activate# X, activate# n__dbl X -> activate# X)
     (add#(s X, Y) -> activate# X, activate# n__sqr X -> activate# X)
     (add#(s X, Y) -> activate# X, activate# n__sqr X -> sqr# activate X)
     (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (add#(s X, Y) -> activate# X, activate# n__s X -> s# X)
     (add#(s X, Y) -> activate# X, activate# n__terms X -> activate# X)
     (add#(s X, Y) -> activate# X, activate# n__terms X -> terms# activate X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X1)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> dbl# activate X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> activate# X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__sqr X -> activate# X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__sqr X -> sqr# activate X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X2)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X1)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> activate# X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# activate X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__sqr X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__sqr X -> sqr# activate X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> s# X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__sqr X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__sqr X -> sqr# activate X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> s# X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X)
     (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# Z)
     (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# X)
     (activate# n__terms X -> terms# activate X, terms# N -> sqr# N)
     (activate# n__dbl X -> dbl# activate X, dbl# s X -> activate# X)
     (activate# n__dbl X -> dbl# activate X, dbl# s X -> s# n__s n__dbl activate X)
     (activate# n__sqr X -> sqr# activate X, sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X))
     (activate# n__sqr X -> sqr# activate X, sqr# s X -> activate# X)
     (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> s# n__add(activate X, Y))
     (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> activate# X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__terms X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__s X -> s# X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__add(X1, X2) -> activate# X2, activate# n__sqr X -> sqr# activate X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__sqr X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__add(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__terms X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__s X -> s# X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__add(X1, X2) -> activate# X1, activate# n__sqr X -> sqr# activate X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__sqr X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> terms# activate X)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> activate# X)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__sqr X -> sqr# activate X)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__sqr X -> activate# X)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> activate# X)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> dbl# activate X)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (dbl# s X -> activate# X, activate# n__terms X -> terms# activate X)
     (dbl# s X -> activate# X, activate# n__terms X -> activate# X)
     (dbl# s X -> activate# X, activate# n__s X -> s# X)
     (dbl# s X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (dbl# s X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (dbl# s X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (dbl# s X -> activate# X, activate# n__sqr X -> sqr# activate X)
     (dbl# s X -> activate# X, activate# n__sqr X -> activate# X)
     (dbl# s X -> activate# X, activate# n__dbl X -> activate# X)
     (dbl# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (dbl# s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (dbl# s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (dbl# s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__sqr X -> activate# X, activate# n__terms X -> terms# activate X)
     (activate# n__sqr X -> activate# X, activate# n__terms X -> activate# X)
     (activate# n__sqr X -> activate# X, activate# n__s X -> s# X)
     (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__sqr X -> activate# X, activate# n__sqr X -> sqr# activate X)
     (activate# n__sqr X -> activate# X, activate# n__sqr X -> activate# X)
     (activate# n__sqr X -> activate# X, activate# n__dbl X -> activate# X)
     (activate# n__sqr X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__terms X -> activate# X, activate# n__terms X -> terms# activate X)
     (activate# n__terms X -> activate# X, activate# n__terms X -> activate# X)
     (activate# n__terms X -> activate# X, activate# n__s X -> s# X)
     (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__terms X -> activate# X, activate# n__sqr X -> sqr# activate X)
     (activate# n__terms X -> activate# X, activate# n__sqr X -> activate# X)
     (activate# n__terms X -> activate# X, activate# n__dbl X -> activate# X)
     (activate# n__terms X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (terms# N -> sqr# N, sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X))
     (terms# N -> sqr# N, sqr# s X -> activate# X)
    }
    EDG:
     {
      (sqr# s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (sqr# s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
      (sqr# s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
      (sqr# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
      (sqr# s X -> activate# X, activate# n__dbl X -> activate# X)
      (sqr# s X -> activate# X, activate# n__sqr X -> activate# X)
      (sqr# s X -> activate# X, activate# n__sqr X -> sqr# activate X)
      (sqr# s X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (sqr# s X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
      (sqr# s X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
      (sqr# s X -> activate# X, activate# n__s X -> s# X)
      (sqr# s X -> activate# X, activate# n__terms X -> activate# X)
      (sqr# s X -> activate# X, activate# n__terms X -> terms# activate X)
      (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
      (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
      (activate# n__dbl X -> activate# X, activate# n__dbl X -> dbl# activate X)
      (activate# n__dbl X -> activate# X, activate# n__dbl X -> activate# X)
      (activate# n__dbl X -> activate# X, activate# n__sqr X -> activate# X)
      (activate# n__dbl X -> activate# X, activate# n__sqr X -> sqr# activate X)
      (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
      (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
      (activate# n__dbl X -> activate# X, activate# n__s X -> s# X)
      (activate# n__dbl X -> activate# X, activate# n__terms X -> activate# X)
      (activate# n__dbl X -> activate# X, activate# n__terms X -> terms# activate X)
      (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> activate# X2)
      (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> activate# X1)
      (add#(s X, Y) -> activate# X, activate# n__dbl X -> dbl# activate X)
      (add#(s X, Y) -> activate# X, activate# n__dbl X -> activate# X)
      (add#(s X, Y) -> activate# X, activate# n__sqr X -> activate# X)
      (add#(s X, Y) -> activate# X, activate# n__sqr X -> sqr# activate X)
      (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
      (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
      (add#(s X, Y) -> activate# X, activate# n__s X -> s# X)
      (add#(s X, Y) -> activate# X, activate# n__terms X -> activate# X)
      (add#(s X, Y) -> activate# X, activate# n__terms X -> terms# activate X)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X1)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> dbl# activate X)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> activate# X)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__sqr X -> activate# X)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__sqr X -> sqr# activate X)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X2)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X1)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> activate# X)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# activate X)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__sqr X -> activate# X)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__sqr X -> sqr# activate X)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> s# X)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> activate# X)
      (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__sqr X -> activate# X)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__sqr X -> sqr# activate X)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> s# X)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> activate# X)
      (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X)
      (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# Z)
      (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# X)
      (activate# n__terms X -> terms# activate X, terms# N -> sqr# N)
      (activate# n__dbl X -> dbl# activate X, dbl# s X -> activate# X)
      (activate# n__dbl X -> dbl# activate X, dbl# s X -> s# n__s n__dbl activate X)
      (activate# n__sqr X -> sqr# activate X, sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X))
      (activate# n__sqr X -> sqr# activate X, sqr# s X -> activate# X)
      (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> s# n__add(activate X, Y))
      (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> activate# X)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__terms X -> activate# X)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__s X -> s# X)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (activate# n__add(X1, X2) -> activate# X2, activate# n__sqr X -> sqr# activate X)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__sqr X -> activate# X)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2)
      (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (activate# n__add(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__terms X -> activate# X)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__s X -> s# X)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (activate# n__add(X1, X2) -> activate# X1, activate# n__sqr X -> sqr# activate X)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__sqr X -> activate# X)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
      (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> terms# activate X)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> activate# X)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__sqr X -> sqr# activate X)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__sqr X -> activate# X)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> activate# X)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> dbl# activate X)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> activate# X1)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> activate# X2)
      (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (dbl# s X -> activate# X, activate# n__terms X -> terms# activate X)
      (dbl# s X -> activate# X, activate# n__terms X -> activate# X)
      (dbl# s X -> activate# X, activate# n__s X -> s# X)
      (dbl# s X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
      (dbl# s X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
      (dbl# s X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (dbl# s X -> activate# X, activate# n__sqr X -> sqr# activate X)
      (dbl# s X -> activate# X, activate# n__sqr X -> activate# X)
      (dbl# s X -> activate# X, activate# n__dbl X -> activate# X)
      (dbl# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
      (dbl# s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
      (dbl# s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
      (dbl# s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (activate# n__sqr X -> activate# X, activate# n__terms X -> terms# activate X)
      (activate# n__sqr X -> activate# X, activate# n__terms X -> activate# X)
      (activate# n__sqr X -> activate# X, activate# n__s X -> s# X)
      (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
      (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
      (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (activate# n__sqr X -> activate# X, activate# n__sqr X -> sqr# activate X)
      (activate# n__sqr X -> activate# X, activate# n__sqr X -> activate# X)
      (activate# n__sqr X -> activate# X, activate# n__dbl X -> activate# X)
      (activate# n__sqr X -> activate# X, activate# n__dbl X -> dbl# activate X)
      (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
      (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
      (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (activate# n__terms X -> activate# X, activate# n__terms X -> terms# activate X)
      (activate# n__terms X -> activate# X, activate# n__terms X -> activate# X)
      (activate# n__terms X -> activate# X, activate# n__s X -> s# X)
      (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
      (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
      (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
      (activate# n__terms X -> activate# X, activate# n__sqr X -> sqr# activate X)
      (activate# n__terms X -> activate# X, activate# n__sqr X -> activate# X)
      (activate# n__terms X -> activate# X, activate# n__dbl X -> activate# X)
      (activate# n__terms X -> activate# X, activate# n__dbl X -> dbl# activate X)
      (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
      (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
      (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
      (terms# N -> sqr# N, sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X))
      (terms# N -> sqr# N, sqr# s X -> activate# X)
     }
     EDG:
      {
       (sqr# s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (sqr# s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
       (sqr# s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
       (sqr# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
       (sqr# s X -> activate# X, activate# n__dbl X -> activate# X)
       (sqr# s X -> activate# X, activate# n__sqr X -> activate# X)
       (sqr# s X -> activate# X, activate# n__sqr X -> sqr# activate X)
       (sqr# s X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (sqr# s X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
       (sqr# s X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
       (sqr# s X -> activate# X, activate# n__s X -> s# X)
       (sqr# s X -> activate# X, activate# n__terms X -> activate# X)
       (sqr# s X -> activate# X, activate# n__terms X -> terms# activate X)
       (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
       (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
       (activate# n__dbl X -> activate# X, activate# n__dbl X -> dbl# activate X)
       (activate# n__dbl X -> activate# X, activate# n__dbl X -> activate# X)
       (activate# n__dbl X -> activate# X, activate# n__sqr X -> activate# X)
       (activate# n__dbl X -> activate# X, activate# n__sqr X -> sqr# activate X)
       (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
       (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
       (activate# n__dbl X -> activate# X, activate# n__s X -> s# X)
       (activate# n__dbl X -> activate# X, activate# n__terms X -> activate# X)
       (activate# n__dbl X -> activate# X, activate# n__terms X -> terms# activate X)
       (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> activate# X2)
       (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> activate# X1)
       (add#(s X, Y) -> activate# X, activate# n__dbl X -> dbl# activate X)
       (add#(s X, Y) -> activate# X, activate# n__dbl X -> activate# X)
       (add#(s X, Y) -> activate# X, activate# n__sqr X -> activate# X)
       (add#(s X, Y) -> activate# X, activate# n__sqr X -> sqr# activate X)
       (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
       (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
       (add#(s X, Y) -> activate# X, activate# n__s X -> s# X)
       (add#(s X, Y) -> activate# X, activate# n__terms X -> activate# X)
       (add#(s X, Y) -> activate# X, activate# n__terms X -> terms# activate X)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X1)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> dbl# activate X)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> activate# X)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__sqr X -> activate# X)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__sqr X -> sqr# activate X)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X2)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X1)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> activate# X)
       (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# activate X)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__sqr X -> activate# X)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__sqr X -> sqr# activate X)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> s# X)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> activate# X)
       (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__sqr X -> activate# X)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__sqr X -> sqr# activate X)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> s# X)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> activate# X)
       (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X)
       (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# Z)
       (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# X)
       (activate# n__terms X -> terms# activate X, terms# N -> sqr# N)
       (activate# n__dbl X -> dbl# activate X, dbl# s X -> activate# X)
       (activate# n__dbl X -> dbl# activate X, dbl# s X -> s# n__s n__dbl activate X)
       (activate# n__sqr X -> sqr# activate X, sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X))
       (activate# n__sqr X -> sqr# activate X, sqr# s X -> activate# X)
       (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> s# n__add(activate X, Y))
       (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> activate# X)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__terms X -> activate# X)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__s X -> s# X)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (activate# n__add(X1, X2) -> activate# X2, activate# n__sqr X -> sqr# activate X)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__sqr X -> activate# X)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2)
       (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (activate# n__add(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__terms X -> activate# X)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__s X -> s# X)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (activate# n__add(X1, X2) -> activate# X1, activate# n__sqr X -> sqr# activate X)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__sqr X -> activate# X)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
       (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> terms# activate X)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> activate# X)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__sqr X -> sqr# activate X)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__sqr X -> activate# X)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> activate# X)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> dbl# activate X)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> activate# X1)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> activate# X2)
       (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (dbl# s X -> activate# X, activate# n__terms X -> terms# activate X)
       (dbl# s X -> activate# X, activate# n__terms X -> activate# X)
       (dbl# s X -> activate# X, activate# n__s X -> s# X)
       (dbl# s X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
       (dbl# s X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
       (dbl# s X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (dbl# s X -> activate# X, activate# n__sqr X -> sqr# activate X)
       (dbl# s X -> activate# X, activate# n__sqr X -> activate# X)
       (dbl# s X -> activate# X, activate# n__dbl X -> activate# X)
       (dbl# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
       (dbl# s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
       (dbl# s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
       (dbl# s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (activate# n__sqr X -> activate# X, activate# n__terms X -> terms# activate X)
       (activate# n__sqr X -> activate# X, activate# n__terms X -> activate# X)
       (activate# n__sqr X -> activate# X, activate# n__s X -> s# X)
       (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
       (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
       (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (activate# n__sqr X -> activate# X, activate# n__sqr X -> sqr# activate X)
       (activate# n__sqr X -> activate# X, activate# n__sqr X -> activate# X)
       (activate# n__sqr X -> activate# X, activate# n__dbl X -> activate# X)
       (activate# n__sqr X -> activate# X, activate# n__dbl X -> dbl# activate X)
       (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
       (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
       (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (activate# n__terms X -> activate# X, activate# n__terms X -> terms# activate X)
       (activate# n__terms X -> activate# X, activate# n__terms X -> activate# X)
       (activate# n__terms X -> activate# X, activate# n__s X -> s# X)
       (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
       (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
       (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
       (activate# n__terms X -> activate# X, activate# n__sqr X -> sqr# activate X)
       (activate# n__terms X -> activate# X, activate# n__sqr X -> activate# X)
       (activate# n__terms X -> activate# X, activate# n__dbl X -> activate# X)
       (activate# n__terms X -> activate# X, activate# n__dbl X -> dbl# activate X)
       (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
       (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
       (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
       (terms# N -> sqr# N, sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X))
       (terms# N -> sqr# N, sqr# s X -> activate# X)
      }
      EDG:
       {
        (sqr# s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (sqr# s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
        (sqr# s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
        (sqr# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
        (sqr# s X -> activate# X, activate# n__dbl X -> activate# X)
        (sqr# s X -> activate# X, activate# n__sqr X -> activate# X)
        (sqr# s X -> activate# X, activate# n__sqr X -> sqr# activate X)
        (sqr# s X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (sqr# s X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
        (sqr# s X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
        (sqr# s X -> activate# X, activate# n__s X -> s# X)
        (sqr# s X -> activate# X, activate# n__terms X -> activate# X)
        (sqr# s X -> activate# X, activate# n__terms X -> terms# activate X)
        (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
        (activate# n__dbl X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
        (activate# n__dbl X -> activate# X, activate# n__dbl X -> dbl# activate X)
        (activate# n__dbl X -> activate# X, activate# n__dbl X -> activate# X)
        (activate# n__dbl X -> activate# X, activate# n__sqr X -> activate# X)
        (activate# n__dbl X -> activate# X, activate# n__sqr X -> sqr# activate X)
        (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
        (activate# n__dbl X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
        (activate# n__dbl X -> activate# X, activate# n__s X -> s# X)
        (activate# n__dbl X -> activate# X, activate# n__terms X -> activate# X)
        (activate# n__dbl X -> activate# X, activate# n__terms X -> terms# activate X)
        (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> activate# X2)
        (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> activate# X1)
        (add#(s X, Y) -> activate# X, activate# n__dbl X -> dbl# activate X)
        (add#(s X, Y) -> activate# X, activate# n__dbl X -> activate# X)
        (add#(s X, Y) -> activate# X, activate# n__sqr X -> activate# X)
        (add#(s X, Y) -> activate# X, activate# n__sqr X -> sqr# activate X)
        (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
        (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
        (add#(s X, Y) -> activate# X, activate# n__s X -> s# X)
        (add#(s X, Y) -> activate# X, activate# n__terms X -> activate# X)
        (add#(s X, Y) -> activate# X, activate# n__terms X -> terms# activate X)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X1)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> dbl# activate X)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> activate# X)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__sqr X -> activate# X)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__sqr X -> sqr# activate X)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X2)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X1)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> activate# X)
        (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# activate X)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__sqr X -> activate# X)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__sqr X -> sqr# activate X)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> s# X)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> activate# X)
        (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__sqr X -> activate# X)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__sqr X -> sqr# activate X)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> s# X)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> activate# X)
        (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X)
        (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# Z)
        (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# X)
        (activate# n__terms X -> terms# activate X, terms# N -> sqr# N)
        (activate# n__dbl X -> dbl# activate X, dbl# s X -> activate# X)
        (activate# n__dbl X -> dbl# activate X, dbl# s X -> s# n__s n__dbl activate X)
        (activate# n__sqr X -> sqr# activate X, sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X))
        (activate# n__sqr X -> sqr# activate X, sqr# s X -> activate# X)
        (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> s# n__add(activate X, Y))
        (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> activate# X)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__terms X -> activate# X)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__s X -> s# X)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (activate# n__add(X1, X2) -> activate# X2, activate# n__sqr X -> sqr# activate X)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__sqr X -> activate# X)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2)
        (activate# n__add(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (activate# n__add(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__terms X -> activate# X)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__s X -> s# X)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (activate# n__add(X1, X2) -> activate# X1, activate# n__sqr X -> sqr# activate X)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__sqr X -> activate# X)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
        (activate# n__add(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> terms# activate X)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> activate# X)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__sqr X -> sqr# activate X)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__sqr X -> activate# X)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> activate# X)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> dbl# activate X)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> activate# X1)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> activate# X2)
        (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (dbl# s X -> activate# X, activate# n__terms X -> terms# activate X)
        (dbl# s X -> activate# X, activate# n__terms X -> activate# X)
        (dbl# s X -> activate# X, activate# n__s X -> s# X)
        (dbl# s X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
        (dbl# s X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
        (dbl# s X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (dbl# s X -> activate# X, activate# n__sqr X -> sqr# activate X)
        (dbl# s X -> activate# X, activate# n__sqr X -> activate# X)
        (dbl# s X -> activate# X, activate# n__dbl X -> activate# X)
        (dbl# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
        (dbl# s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
        (dbl# s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
        (dbl# s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (activate# n__sqr X -> activate# X, activate# n__terms X -> terms# activate X)
        (activate# n__sqr X -> activate# X, activate# n__terms X -> activate# X)
        (activate# n__sqr X -> activate# X, activate# n__s X -> s# X)
        (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
        (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
        (activate# n__sqr X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (activate# n__sqr X -> activate# X, activate# n__sqr X -> sqr# activate X)
        (activate# n__sqr X -> activate# X, activate# n__sqr X -> activate# X)
        (activate# n__sqr X -> activate# X, activate# n__dbl X -> activate# X)
        (activate# n__sqr X -> activate# X, activate# n__dbl X -> dbl# activate X)
        (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
        (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
        (activate# n__sqr X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (activate# n__terms X -> activate# X, activate# n__terms X -> terms# activate X)
        (activate# n__terms X -> activate# X, activate# n__terms X -> activate# X)
        (activate# n__terms X -> activate# X, activate# n__s X -> s# X)
        (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
        (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
        (activate# n__terms X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
        (activate# n__terms X -> activate# X, activate# n__sqr X -> sqr# activate X)
        (activate# n__terms X -> activate# X, activate# n__sqr X -> activate# X)
        (activate# n__terms X -> activate# X, activate# n__dbl X -> activate# X)
        (activate# n__terms X -> activate# X, activate# n__dbl X -> dbl# activate X)
        (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
        (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
        (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
        (terms# N -> sqr# N, sqr# s X -> s# n__add(n__sqr activate X, n__dbl activate X))
        (terms# N -> sqr# N, sqr# s X -> activate# X)
       }
       STATUS:
        arrows: 0.654959
        SCCS (1):
         Scc:
          {                  sqr# s X -> activate# X,
                             terms# N -> sqr# N,
                 activate# n__terms X -> terms# activate X,
                 activate# n__terms X -> activate# X,
             activate# n__add(X1, X2) -> activate# X1,
             activate# n__add(X1, X2) -> activate# X2,
             activate# n__add(X1, X2) -> add#(activate X1, activate X2),
                   activate# n__sqr X -> sqr# activate X,
                   activate# n__sqr X -> activate# X,
                   activate# n__dbl X -> activate# X,
                   activate# n__dbl X -> dbl# activate X,
           activate# n__first(X1, X2) -> activate# X1,
           activate# n__first(X1, X2) -> activate# X2,
           activate# n__first(X1, X2) -> first#(activate X1, activate X2),
                             dbl# s X -> activate# X,
                         add#(s X, Y) -> activate# X,
              first#(s X, cons(Y, Z)) -> activate# X,
              first#(s X, cons(Y, Z)) -> activate# Z}
         
         SCC (18):
          Strict:
           {                  sqr# s X -> activate# X,
                              terms# N -> sqr# N,
                  activate# n__terms X -> terms# activate X,
                  activate# n__terms X -> activate# X,
              activate# n__add(X1, X2) -> activate# X1,
              activate# n__add(X1, X2) -> activate# X2,
              activate# n__add(X1, X2) -> add#(activate X1, activate X2),
                    activate# n__sqr X -> sqr# activate X,
                    activate# n__sqr X -> activate# X,
                    activate# n__dbl X -> activate# X,
                    activate# n__dbl X -> dbl# activate X,
            activate# n__first(X1, X2) -> activate# X1,
            activate# n__first(X1, X2) -> activate# X2,
            activate# n__first(X1, X2) -> first#(activate X1, activate X2),
                              dbl# s X -> activate# X,
                          add#(s X, Y) -> activate# X,
               first#(s X, cons(Y, Z)) -> activate# X,
               first#(s X, cons(Y, Z)) -> activate# Z}
          Weak:
          {                    sqr X -> n__sqr X,
                             sqr 0() -> 0(),
                             sqr s X -> s n__add(n__sqr activate X, n__dbl activate X),
                             terms N -> cons(recip sqr N, n__terms n__s N),
                             terms X -> n__terms X,
                                 s X -> n__s X,
                          activate X -> X,
                 activate n__terms X -> terms activate X,
                     activate n__s X -> s X,
             activate n__add(X1, X2) -> add(activate X1, activate X2),
                   activate n__sqr X -> sqr activate X,
                   activate n__dbl X -> dbl activate X,
           activate n__first(X1, X2) -> first(activate X1, activate X2),
                               dbl X -> n__dbl X,
                             dbl 0() -> 0(),
                             dbl s X -> s n__s n__dbl activate X,
                         add(X1, X2) -> n__add(X1, X2),
                         add(0(), X) -> X,
                         add(s X, Y) -> s n__add(activate X, Y),
                       first(X1, X2) -> n__first(X1, X2),
                       first(0(), X) -> nil(),
              first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z))}
          Fail