MAYBE
TRS:
 {               activate(X) -> X,
    activate(n__add(X1, X2)) -> add(activate(X1), X2),
  activate(n__first(X1, X2)) -> first(activate(X1), activate(X2)),
        activate(n__from(X)) -> from(X),
           activate(n__s(X)) -> s(X),
              and(true(), X) -> activate(X),
             and(false(), Y) -> false(),
            if(true(), X, Y) -> activate(X),
           if(false(), X, Y) -> activate(Y),
                 add(X1, X2) -> n__add(X1, X2),
                 add(0(), X) -> activate(X),
                add(s(X), Y) -> s(n__add(activate(X), activate(Y))),
                        s(X) -> n__s(X),
               first(X1, X2) -> n__first(X1, X2),
               first(0(), X) -> nil(),
     first(s(X), cons(Y, Z)) -> cons(activate(Y), n__first(activate(X), activate(Z))),
                     from(X) -> cons(activate(X), n__from(n__s(activate(X)))),
                     from(X) -> n__from(X)}
 DP:
  Strict:
   {  activate#(n__add(X1, X2)) -> activate#(X1),
      activate#(n__add(X1, X2)) -> add#(activate(X1), X2),
    activate#(n__first(X1, X2)) -> activate#(X1),
    activate#(n__first(X1, X2)) -> activate#(X2),
    activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)),
          activate#(n__from(X)) -> from#(X),
             activate#(n__s(X)) -> s#(X),
                and#(true(), X) -> activate#(X),
              if#(true(), X, Y) -> activate#(X),
             if#(false(), X, Y) -> activate#(Y),
                   add#(0(), X) -> activate#(X),
                  add#(s(X), Y) -> activate#(X),
                  add#(s(X), Y) -> activate#(Y),
                  add#(s(X), Y) -> s#(n__add(activate(X), activate(Y))),
       first#(s(X), cons(Y, Z)) -> activate#(X),
       first#(s(X), cons(Y, Z)) -> activate#(Y),
       first#(s(X), cons(Y, Z)) -> activate#(Z),
                       from#(X) -> activate#(X)}
  Weak:
  {               activate(X) -> X,
     activate(n__add(X1, X2)) -> add(activate(X1), X2),
   activate(n__first(X1, X2)) -> first(activate(X1), activate(X2)),
         activate(n__from(X)) -> from(X),
            activate(n__s(X)) -> s(X),
               and(true(), X) -> activate(X),
              and(false(), Y) -> false(),
             if(true(), X, Y) -> activate(X),
            if(false(), X, Y) -> activate(Y),
                  add(X1, X2) -> n__add(X1, X2),
                  add(0(), X) -> activate(X),
                 add(s(X), Y) -> s(n__add(activate(X), activate(Y))),
                         s(X) -> n__s(X),
                first(X1, X2) -> n__first(X1, X2),
                first(0(), X) -> nil(),
      first(s(X), cons(Y, Z)) -> cons(activate(Y), n__first(activate(X), activate(Z))),
                      from(X) -> cons(activate(X), n__from(n__s(activate(X)))),
                      from(X) -> n__from(X)}
  EDG:
   {(activate#(n__add(X1, X2)) -> add#(activate(X1), X2), add#(s(X), Y) -> s#(n__add(activate(X), activate(Y))))
    (activate#(n__add(X1, X2)) -> add#(activate(X1), X2), add#(s(X), Y) -> activate#(Y))
    (activate#(n__add(X1, X2)) -> add#(activate(X1), X2), add#(s(X), Y) -> activate#(X))
    (activate#(n__add(X1, X2)) -> add#(activate(X1), X2), add#(0(), 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__from(X)) -> from#(X))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (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)) -> activate#(X1))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (activate#(n__add(X1, X2)) -> activate#(X1), 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__from(X)) -> from#(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__add(X1, X2)) -> add#(activate(X1), X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> activate#(X1))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__from(X)) -> from#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__first(X1, X2)) -> activate#(X2))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__first(X1, X2)) -> activate#(X1))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__add(X1, X2)) -> activate#(X1))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__from(X)) -> from#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__first(X1, X2)) -> activate#(X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__first(X1, X2)) -> activate#(X1))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__add(X1, X2)) -> activate#(X1))
    (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (if#(true(), X, Y) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (if#(true(), X, Y) -> activate#(X), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (if#(true(), X, Y) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X2))
    (if#(true(), X, Y) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X1))
    (if#(true(), X, Y) -> activate#(X), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (if#(true(), 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__from(X)) -> from#(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__add(X1, X2)) -> add#(activate(X1), X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X1))
    (from#(X) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (from#(X) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (from#(X) -> activate#(X), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (from#(X) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X2))
    (from#(X) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X1))
    (from#(X) -> activate#(X), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (from#(X) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X1))
    (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)) -> add#(activate(X1), X2))
    (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)))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (add#(0(), X) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X1))
    (add#(0(), X) -> activate#(X), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (add#(0(), X) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X1))
    (add#(0(), X) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X2))
    (add#(0(), X) -> activate#(X), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (add#(0(), X) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (add#(0(), X) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (and#(true(), X) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X1))
    (and#(true(), X) -> activate#(X), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (and#(true(), X) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X1))
    (and#(true(), X) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X2))
    (and#(true(), X) -> activate#(X), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (and#(true(), X) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (and#(true(), X) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (activate#(n__from(X)) -> from#(X), from#(X) -> activate#(X))
    (add#(s(X), Y) -> activate#(Y), activate#(n__add(X1, X2)) -> activate#(X1))
    (add#(s(X), Y) -> activate#(Y), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (add#(s(X), Y) -> activate#(Y), activate#(n__first(X1, X2)) -> activate#(X1))
    (add#(s(X), Y) -> activate#(Y), activate#(n__first(X1, X2)) -> activate#(X2))
    (add#(s(X), Y) -> activate#(Y), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (add#(s(X), Y) -> activate#(Y), activate#(n__from(X)) -> from#(X))
    (add#(s(X), Y) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)), first#(s(X), cons(Y, Z)) -> activate#(X))
    (activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)), first#(s(X), cons(Y, Z)) -> activate#(Y))
    (activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)), first#(s(X), cons(Y, Z)) -> activate#(Z))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__first(X1, X2)) -> activate#(X1))
    (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)) -> first#(activate(X1), activate(X2)))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> from#(X))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(X))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> add#(activate(X1), X2))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__first(X1, X2)) -> activate#(X1))
    (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)) -> first#(activate(X1), activate(X2)))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> from#(X))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(X))}
   SCCS:
    Scc:
     {  activate#(n__add(X1, X2)) -> activate#(X1),
        activate#(n__add(X1, X2)) -> add#(activate(X1), X2),
      activate#(n__first(X1, X2)) -> activate#(X1),
      activate#(n__first(X1, X2)) -> activate#(X2),
      activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)),
            activate#(n__from(X)) -> from#(X),
                     add#(0(), X) -> activate#(X),
                    add#(s(X), Y) -> activate#(X),
                    add#(s(X), Y) -> activate#(Y),
         first#(s(X), cons(Y, Z)) -> activate#(X),
         first#(s(X), cons(Y, Z)) -> activate#(Y),
         first#(s(X), cons(Y, Z)) -> activate#(Z),
                         from#(X) -> activate#(X)}
    SCC:
     Strict:
      {  activate#(n__add(X1, X2)) -> activate#(X1),
         activate#(n__add(X1, X2)) -> add#(activate(X1), X2),
       activate#(n__first(X1, X2)) -> activate#(X1),
       activate#(n__first(X1, X2)) -> activate#(X2),
       activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)),
             activate#(n__from(X)) -> from#(X),
                      add#(0(), X) -> activate#(X),
                     add#(s(X), Y) -> activate#(X),
                     add#(s(X), Y) -> activate#(Y),
          first#(s(X), cons(Y, Z)) -> activate#(X),
          first#(s(X), cons(Y, Z)) -> activate#(Y),
          first#(s(X), cons(Y, Z)) -> activate#(Z),
                          from#(X) -> activate#(X)}
     Weak:
     {               activate(X) -> X,
        activate(n__add(X1, X2)) -> add(activate(X1), X2),
      activate(n__first(X1, X2)) -> first(activate(X1), activate(X2)),
            activate(n__from(X)) -> from(X),
               activate(n__s(X)) -> s(X),
                  and(true(), X) -> activate(X),
                 and(false(), Y) -> false(),
                if(true(), X, Y) -> activate(X),
               if(false(), X, Y) -> activate(Y),
                     add(X1, X2) -> n__add(X1, X2),
                     add(0(), X) -> activate(X),
                    add(s(X), Y) -> s(n__add(activate(X), activate(Y))),
                            s(X) -> n__s(X),
                   first(X1, X2) -> n__first(X1, X2),
                   first(0(), X) -> nil(),
         first(s(X), cons(Y, Z)) -> cons(activate(Y), n__first(activate(X), activate(Z))),
                         from(X) -> cons(activate(X), n__from(n__s(activate(X)))),
                         from(X) -> n__from(X)}
     Fail