YES
Time: 0.029414
TRS:
 {                 f X -> cons(X, n__f n__g X),
                   f X -> n__f X,
                   g X -> n__g X,
                 g s X -> s s g X,
                 g 0() -> s 0(),
  sel(s X, cons(Y, Z)) -> sel(X, activate Z),
  sel(0(), cons(X, Y)) -> X,
            activate X -> X,
       activate n__f X -> f activate X,
       activate n__g X -> g activate X}
 DP:
  DP:
   {               g# s X -> g# X,
    sel#(s X, cons(Y, Z)) -> sel#(X, activate Z),
    sel#(s X, cons(Y, Z)) -> activate# Z,
         activate# n__f X -> f# activate X,
         activate# n__f X -> activate# X,
         activate# n__g X -> g# activate X,
         activate# n__g X -> activate# X}
  TRS:
  {                 f X -> cons(X, n__f n__g X),
                    f X -> n__f X,
                    g X -> n__g X,
                  g s X -> s s g X,
                  g 0() -> s 0(),
   sel(s X, cons(Y, Z)) -> sel(X, activate Z),
   sel(0(), cons(X, Y)) -> X,
             activate X -> X,
        activate n__f X -> f activate X,
        activate n__g X -> g activate X}
  UR:
   {            f X -> cons(X, n__f n__g X),
                f X -> n__f X,
                g X -> n__g X,
              g s X -> s s g X,
              g 0() -> s 0(),
         activate X -> X,
    activate n__f X -> f activate X,
    activate n__g X -> g activate X,
            a(x, y) -> x,
            a(x, y) -> y}
   EDG:
    {(sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__g X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__g X -> g# activate X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__f X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__f X -> f# activate X)
     (activate# n__f X -> activate# X, activate# n__g X -> activate# X)
     (activate# n__f X -> activate# X, activate# n__g X -> g# activate X)
     (activate# n__f X -> activate# X, activate# n__f X -> activate# X)
     (activate# n__f X -> activate# X, activate# n__f X -> f# activate X)
     (activate# n__g X -> g# activate X, g# s X -> g# X)
     (activate# n__g X -> activate# X, activate# n__f X -> f# activate X)
     (activate# n__g X -> activate# X, activate# n__f X -> activate# X)
     (activate# n__g X -> activate# X, activate# n__g X -> g# activate X)
     (activate# n__g X -> activate# X, activate# n__g X -> activate# X)
     (g# s X -> g# X, g# s X -> g# 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)}
    STATUS:
     arrows: 0.673469
     SCCS (3):
      Scc:
       {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
      Scc:
       {activate# n__f X -> activate# X,
        activate# n__g X -> activate# X}
      Scc:
       {g# s X -> g# X}
      
      SCC (1):
       Strict:
        {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
       Weak:
       {                 f X -> cons(X, n__f n__g X),
                         f X -> n__f X,
                         g X -> n__g X,
                       g s X -> s s g X,
                       g 0() -> s 0(),
        sel(s X, cons(Y, Z)) -> sel(X, activate Z),
        sel(0(), cons(X, Y)) -> X,
                  activate X -> X,
             activate n__f X -> f activate X,
             activate n__g X -> g activate X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = x0,
         
         [sel](x0, x1) = x0 + x1 + 1,
         
         [n__f](x0) = x0,
         
         [n__g](x0) = 1,
         
         [f](x0) = x0,
         
         [s](x0) = x0 + 1,
         
         [g](x0) = x0,
         
         [activate](x0) = 1,
         
         [0] = 0,
         
         [sel#](x0, x1) = x0
        Strict:
         sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)
         1 + 1X + 0Y + 0Z >= 0 + 1X + 0Z
        Weak:
         activate n__g X -> g activate X
         1 + 0X >= 1 + 0X
         activate n__f X -> f activate X
         1 + 0X >= 1 + 0X
         activate X -> X
         1 + 0X >= 1X
         sel(0(), cons(X, Y)) -> X
         1 + 0X + 1Y >= 1X
         sel(s X, cons(Y, Z)) -> sel(X, activate Z)
         2 + 1X + 0Y + 1Z >= 2 + 1X + 0Z
         g 0() -> s 0()
         0 >= 1
         g s X -> s s g X
         1 + 1X >= 2 + 1X
         g X -> n__g X
         0 + 1X >= 1 + 0X
         f X -> n__f X
         0 + 1X >= 0 + 1X
         f X -> cons(X, n__f n__g X)
         0 + 1X >= 1 + 0X
       Qed
     
     SCC (2):
      Strict:
       {activate# n__f X -> activate# X,
        activate# n__g X -> activate# X}
      Weak:
      {                 f X -> cons(X, n__f n__g X),
                        f X -> n__f X,
                        g X -> n__g X,
                      g s X -> s s g X,
                      g 0() -> s 0(),
       sel(s X, cons(Y, Z)) -> sel(X, activate Z),
       sel(0(), cons(X, Y)) -> X,
                 activate X -> X,
            activate n__f X -> f activate X,
            activate n__g X -> g activate X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [cons](x0, x1) = 0,
        
        [sel](x0, x1) = 0,
        
        [n__f](x0) = x0,
        
        [n__g](x0) = x0 + 1,
        
        [f](x0) = 0,
        
        [s](x0) = 0,
        
        [g](x0) = 0,
        
        [activate](x0) = 0,
        
        [0] = 0,
        
        [activate#](x0) = x0
       Strict:
        activate# n__g X -> activate# X
        1 + 1X >= 0 + 1X
        activate# n__f X -> activate# X
        0 + 1X >= 0 + 1X
       Weak:
        activate n__g X -> g activate X
        0 + 0X >= 0 + 0X
        activate n__f X -> f activate X
        0 + 0X >= 0 + 0X
        activate X -> X
        0 + 0X >= 1X
        sel(0(), cons(X, Y)) -> X
        0 + 0X + 0Y >= 1X
        sel(s X, cons(Y, Z)) -> sel(X, activate Z)
        0 + 0X + 0Y + 0Z >= 0 + 0X + 0Z
        g 0() -> s 0()
        0 >= 0
        g s X -> s s g X
        0 + 0X >= 0 + 0X
        g X -> n__g X
        0 + 0X >= 1 + 1X
        f X -> n__f X
        0 + 0X >= 0 + 1X
        f X -> cons(X, n__f n__g X)
        0 + 0X >= 0 + 0X
      SCCS (1):
       Scc:
        {activate# n__f X -> activate# X}
       
       SCC (1):
        Strict:
         {activate# n__f X -> activate# X}
        Weak:
        {                 f X -> cons(X, n__f n__g X),
                          f X -> n__f X,
                          g X -> n__g X,
                        g s X -> s s g X,
                        g 0() -> s 0(),
         sel(s X, cons(Y, Z)) -> sel(X, activate Z),
         sel(0(), cons(X, Y)) -> X,
                   activate X -> X,
              activate n__f X -> f activate X,
              activate n__g X -> g activate X}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [cons](x0, x1) = 0,
          
          [sel](x0, x1) = x0 + x1 + 1,
          
          [n__f](x0) = x0 + 1,
          
          [n__g](x0) = 1,
          
          [f](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [g](x0) = x0 + 1,
          
          [activate](x0) = x0 + 1,
          
          [0] = 1,
          
          [activate#](x0) = x0
         Strict:
          activate# n__f X -> activate# X
          1 + 1X >= 0 + 1X
         Weak:
          activate n__g X -> g activate X
          2 + 0X >= 2 + 1X
          activate n__f X -> f activate X
          2 + 1X >= 2 + 1X
          activate X -> X
          1 + 1X >= 1X
          sel(0(), cons(X, Y)) -> X
          2 + 0X + 0Y >= 1X
          sel(s X, cons(Y, Z)) -> sel(X, activate Z)
          2 + 1X + 0Y + 0Z >= 2 + 1X + 1Z
          g 0() -> s 0()
          2 >= 2
          g s X -> s s g X
          2 + 1X >= 3 + 1X
          g X -> n__g X
          1 + 1X >= 1 + 0X
          f X -> n__f X
          1 + 1X >= 1 + 1X
          f X -> cons(X, n__f n__g X)
          1 + 1X >= 0 + 0X
        Qed
    
    SCC (1):
     Strict:
      {g# s X -> g# X}
     Weak:
     {                 f X -> cons(X, n__f n__g X),
                       f X -> n__f X,
                       g X -> n__g X,
                     g s X -> s s g X,
                     g 0() -> s 0(),
      sel(s X, cons(Y, Z)) -> sel(X, activate Z),
      sel(0(), cons(X, Y)) -> X,
                activate X -> X,
           activate n__f X -> f activate X,
           activate n__g X -> g activate X}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [cons](x0, x1) = 1,
       
       [sel](x0, x1) = x0 + 1,
       
       [n__f](x0) = x0 + 1,
       
       [n__g](x0) = 1,
       
       [f](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [g](x0) = x0 + 1,
       
       [activate](x0) = 1,
       
       [0] = 1,
       
       [g#](x0) = x0
      Strict:
       g# s X -> g# X
       1 + 1X >= 0 + 1X
      Weak:
       activate n__g X -> g activate X
       1 + 0X >= 2 + 0X
       activate n__f X -> f activate X
       1 + 0X >= 2 + 0X
       activate X -> X
       1 + 0X >= 1X
       sel(0(), cons(X, Y)) -> X
       2 + 0X + 0Y >= 1X
       sel(s X, cons(Y, Z)) -> sel(X, activate Z)
       2 + 0X + 0Y + 0Z >= 2 + 0X + 0Z
       g 0() -> s 0()
       2 >= 2
       g s X -> s s g X
       2 + 1X >= 3 + 1X
       g X -> n__g X
       1 + 1X >= 1 + 0X
       f X -> n__f X
       1 + 1X >= 1 + 1X
       f X -> cons(X, n__f n__g X)
       1 + 1X >= 1 + 0X
     Qed