MAYBE
Time: 0.003246
TRS:
 {               activate X -> X,
    activate n__add(X1, X2) -> add(X1, X2),
  activate n__first(X1, X2) -> first(X1, 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:
  DP:
   {  activate# n__add(X1, X2) -> add#(X1, X2),
    activate# n__first(X1, X2) -> first#(X1, 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}
  TRS:
  {               activate X -> X,
     activate n__add(X1, X2) -> add(X1, X2),
   activate n__first(X1, X2) -> first(X1, 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:
   {(add#(s X, Y) -> activate# Y, activate# n__s X -> s# X)
    (add#(s X, Y) -> activate# Y, activate# n__from X -> from# X)
    (add#(s X, Y) -> activate# Y, activate# n__first(X1, X2) -> first#(X1, X2))
    (add#(s X, Y) -> activate# Y, activate# n__add(X1, X2) -> add#(X1, X2))
    (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#(X1, X2))
    (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> add#(X1, X2))
    (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Z)
    (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Y)
    (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# X)
    (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#(X1, X2))
    (if#(true(), X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2))
    (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#(X1, X2))
    (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2))
    (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#(X1, X2))
    (from# X -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2))
    (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2))
    (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> first#(X1, 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) -> add#(X1, X2))
    (add#(0(), X) -> activate# X, activate# n__first(X1, X2) -> first#(X1, 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) -> add#(X1, X2))
    (and#(true(), X) -> activate# X, activate# n__first(X1, X2) -> first#(X1, 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)
    (activate# n__add(X1, X2) -> add#(X1, X2), add#(0(), X) -> activate# X)
    (activate# n__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> activate# X)
    (activate# n__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> activate# Y)
    (activate# n__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> s# n__add(activate X, activate Y))
    (first#(s X, cons(Y, Z)) -> activate# Y, activate# n__add(X1, X2) -> add#(X1, X2))
    (first#(s X, cons(Y, Z)) -> activate# Y, activate# n__first(X1, X2) -> first#(X1, X2))
    (first#(s X, cons(Y, Z)) -> activate# Y, activate# n__from X -> from# X)
    (first#(s X, cons(Y, Z)) -> activate# Y, activate# n__s X -> s# X)
    (if#(false(), X, Y) -> activate# Y, activate# n__add(X1, X2) -> add#(X1, X2))
    (if#(false(), X, Y) -> activate# Y, activate# n__first(X1, X2) -> first#(X1, X2))
    (if#(false(), X, Y) -> activate# Y, activate# n__from X -> from# X)
    (if#(false(), X, Y) -> activate# Y, activate# n__s X -> s# X)}
   STATUS:
    arrows: 0.786667
    SCCS (1):
     Scc:
      {  activate# n__add(X1, X2) -> add#(X1, X2),
       activate# n__first(X1, X2) -> first#(X1, 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 (10):
      Strict:
       {  activate# n__add(X1, X2) -> add#(X1, X2),
        activate# n__first(X1, X2) -> first#(X1, 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(X1, X2),
       activate n__first(X1, X2) -> first(X1, 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}
      Open