MAYBE
Time: 0.003622
TRS:
 {                   from X -> cons(X, n__from n__s X),
                     from X -> n__from X,
              first(X1, X2) -> n__first(X1, X2),
              first(0(), Z) -> nil(),
     first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                 activate X -> X,
         activate n__from X -> from activate X,
            activate n__s X -> s activate X,
  activate n__first(X1, X2) -> first(activate X1, activate X2),
                        s X -> n__s X,
       sel(0(), cons(X, Z)) -> X,
       sel(s X, cons(Y, Z)) -> sel(X, activate Z)}
 DP:
  DP:
   {   first#(s X, cons(Y, Z)) -> activate# Z,
           activate# n__from X -> from# activate X,
           activate# n__from X -> activate# X,
              activate# n__s X -> activate# X,
              activate# n__s X -> s# activate X,
    activate# n__first(X1, X2) -> first#(activate X1, activate X2),
    activate# n__first(X1, X2) -> activate# X1,
    activate# n__first(X1, X2) -> activate# X2,
         sel#(s X, cons(Y, Z)) -> activate# Z,
         sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
  TRS:
  {                   from X -> cons(X, n__from n__s X),
                      from X -> n__from X,
               first(X1, X2) -> n__first(X1, X2),
               first(0(), Z) -> nil(),
      first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                  activate X -> X,
          activate n__from X -> from activate X,
             activate n__s X -> s activate X,
   activate n__first(X1, X2) -> first(activate X1, activate X2),
                         s X -> n__s X,
        sel(0(), cons(X, Z)) -> X,
        sel(s X, cons(Y, Z)) -> sel(X, activate Z)}
  UR:
   {                   from X -> cons(X, n__from n__s X),
                       from X -> n__from X,
                first(X1, X2) -> n__first(X1, X2),
                first(0(), Z) -> nil(),
       first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                   activate X -> X,
           activate n__from X -> from activate X,
              activate n__s X -> s activate X,
    activate n__first(X1, X2) -> first(activate X1, activate X2),
                          s X -> n__s X,
                      a(x, y) -> x,
                      a(x, y) -> y}
   EDG:
    {(sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X1)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# activate X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# activate X)
     (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__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__from X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X2, activate# n__from X -> from# activate X)
     (sel#(s X, cons(Y, Z)) -> sel#(X, activate Z), sel#(s X, cons(Y, Z)) -> sel#(X, activate Z))
     (sel#(s X, cons(Y, Z)) -> sel#(X, activate Z), sel#(s X, cons(Y, Z)) -> activate# Z)
     (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> from# activate X)
     (activate# n__from X -> activate# X, activate# n__from X -> from# activate X)
     (activate# n__from X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__from X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2))
     (activate# n__from X -> activate# X, activate# n__first(X1, X2) -> activate# X1)
     (activate# n__from X -> activate# X, activate# n__first(X1, X2) -> activate# X2)
     (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__from X -> from# activate X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__from X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> s# 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# X1)
     (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# activate X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> activate# X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> activate# X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# 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# X1)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2)}
    STATUS:
     arrows: 0.550000
     SCCS (2):
      Scc:
       {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
      Scc:
       {   first#(s X, cons(Y, Z)) -> activate# Z,
               activate# n__from X -> activate# X,
                  activate# n__s X -> activate# X,
        activate# n__first(X1, X2) -> first#(activate X1, activate X2),
        activate# n__first(X1, X2) -> activate# X1,
        activate# n__first(X1, X2) -> activate# X2}
      
      SCC (1):
       Strict:
        {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
       Weak:
       {                   from X -> cons(X, n__from n__s X),
                           from X -> n__from X,
                    first(X1, X2) -> n__first(X1, X2),
                    first(0(), Z) -> nil(),
           first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                       activate X -> X,
               activate n__from X -> from activate X,
                  activate n__s X -> s activate X,
        activate n__first(X1, X2) -> first(activate X1, activate X2),
                              s X -> n__s X,
             sel(0(), cons(X, Z)) -> X,
             sel(s X, cons(Y, Z)) -> sel(X, activate Z)}
       Open
      
      SCC (6):
       Strict:
        {   first#(s X, cons(Y, Z)) -> activate# Z,
                activate# n__from X -> activate# X,
                   activate# n__s X -> activate# X,
         activate# n__first(X1, X2) -> first#(activate X1, activate X2),
         activate# n__first(X1, X2) -> activate# X1,
         activate# n__first(X1, X2) -> activate# X2}
       Weak:
       {                   from X -> cons(X, n__from n__s X),
                           from X -> n__from X,
                    first(X1, X2) -> n__first(X1, X2),
                    first(0(), Z) -> nil(),
           first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                       activate X -> X,
               activate n__from X -> from activate X,
                  activate n__s X -> s activate X,
        activate n__first(X1, X2) -> first(activate X1, activate X2),
                              s X -> n__s X,
             sel(0(), cons(X, Z)) -> X,
             sel(s X, cons(Y, Z)) -> sel(X, activate Z)}
       Open