We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , 2ndspos(0(), Z) -> rnil()
     , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
     , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
       rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
     , 2ndsneg(0(), Z) -> rnil()
     , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
     , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
       rcons(negrecip(Y), 2ndspos(N, activate(Z)))
     , pi(X) -> 2ndspos(X, from(0()))
     , plus(0(), Y) -> Y
     , plus(s(X), Y) -> s(plus(X, Y))
     , times(0(), Y) -> 0()
     , times(s(X), Y) -> plus(Y, times(X, Y))
     , square(X) -> times(X, X)
     , from(X) -> n__from(X)
     , activate(n__from(X)) -> from(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {  from(X) -> cons(X, n__from(s(X)))
       , 2ndspos(0(), Z) -> rnil()
       , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
       , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
         rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
       , 2ndsneg(0(), Z) -> rnil()
       , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
       , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
         rcons(negrecip(Y), 2ndspos(N, activate(Z)))
       , pi(X) -> 2ndspos(X, from(0()))
       , plus(0(), Y) -> Y
       , plus(s(X), Y) -> s(plus(X, Y))
       , times(0(), Y) -> 0()
       , times(s(X), Y) -> plus(Y, times(X, Y))
       , square(X) -> times(X, X)
       , from(X) -> n__from(X)
       , activate(n__from(X)) -> from(X)
       , activate(X) -> X}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^2))
  
  Proof:
    The weightgap principle applies, where following rules are oriented strictly:
    
    TRS Component:
      {  2ndspos(0(), Z) -> rnil()
       , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
       , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
       , times(0(), Y) -> 0()}
    
    Interpretation of nonconstant growth:
    -------------------------------------
      The following argument positions are usable:
        Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
        Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
        Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
        Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
        Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
      Interpretation Functions:
       from(x1) = [1 1] x1 + [0]
                  [0 0]      [0]
       cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                      [0 0]      [1 1]      [1]
       n__from(x1) = [0 0] x1 + [0]
                     [1 1]      [0]
       s(x1) = [1 0] x1 + [0]
               [0 0]      [0]
       2ndspos(x1, x2) = [0 0] x1 + [1 1] x2 + [1]
                         [0 0]      [0 0]      [1]
       0() = [0]
             [0]
       rnil() = [0]
                [0]
       cons2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                       [0 1]      [0 0]      [0]
       activate(x1) = [1 1] x1 + [0]
                      [0 0]      [0]
       rcons(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                       [0 0]      [0 1]      [1]
       posrecip(x1) = [0 0] x1 + [0]
                      [0 0]      [0]
       2ndsneg(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                         [0 0]      [0 0]      [0]
       negrecip(x1) = [0 0] x1 + [0]
                      [0 0]      [0]
       pi(x1) = [0 0] x1 + [0]
                [0 0]      [0]
       plus(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                      [0 1]      [0 0]      [1]
       times(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                       [0 0]      [1 1]      [1]
       square(x1) = [0 0] x1 + [0]
                    [0 0]      [0]
    
    The strictly oriented rules are moved into the weak component.
    
    We consider the following Problem:
    
      Strict Trs:
        {  from(X) -> cons(X, n__from(s(X)))
         , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
           rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
         , 2ndsneg(0(), Z) -> rnil()
         , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
           rcons(negrecip(Y), 2ndspos(N, activate(Z)))
         , pi(X) -> 2ndspos(X, from(0()))
         , plus(0(), Y) -> Y
         , plus(s(X), Y) -> s(plus(X, Y))
         , times(s(X), Y) -> plus(Y, times(X, Y))
         , square(X) -> times(X, X)
         , from(X) -> n__from(X)
         , activate(n__from(X)) -> from(X)
         , activate(X) -> X}
      Weak Trs:
        {  2ndspos(0(), Z) -> rnil()
         , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
         , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
         , times(0(), Y) -> 0()}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^2))
    
    Proof:
      The weightgap principle applies, where following rules are oriented strictly:
      
      TRS Component: {pi(X) -> 2ndspos(X, from(0()))}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
          Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
          Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
          Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
          Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         from(x1) = [1 1] x1 + [0]
                    [0 0]      [0]
         cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                        [0 0]      [1 1]      [1]
         n__from(x1) = [0 0] x1 + [0]
                       [1 1]      [0]
         s(x1) = [1 0] x1 + [0]
                 [0 0]      [0]
         2ndspos(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                           [0 0]      [0 0]      [1]
         0() = [0]
               [0]
         rnil() = [0]
                  [0]
         cons2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                         [0 1]      [0 0]      [0]
         activate(x1) = [1 1] x1 + [0]
                        [0 0]      [0]
         rcons(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                         [0 0]      [0 0]      [1]
         posrecip(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
         2ndsneg(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                           [0 0]      [0 0]      [1]
         negrecip(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
         pi(x1) = [0 0] x1 + [2]
                  [0 0]      [2]
         plus(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                        [0 1]      [0 0]      [1]
         times(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                         [0 0]      [1 1]      [1]
         square(x1) = [0 0] x1 + [0]
                      [0 0]      [0]
      
      The strictly oriented rules are moved into the weak component.
      
      We consider the following Problem:
      
        Strict Trs:
          {  from(X) -> cons(X, n__from(s(X)))
           , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
             rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
           , 2ndsneg(0(), Z) -> rnil()
           , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
             rcons(negrecip(Y), 2ndspos(N, activate(Z)))
           , plus(0(), Y) -> Y
           , plus(s(X), Y) -> s(plus(X, Y))
           , times(s(X), Y) -> plus(Y, times(X, Y))
           , square(X) -> times(X, X)
           , from(X) -> n__from(X)
           , activate(n__from(X)) -> from(X)
           , activate(X) -> X}
        Weak Trs:
          {  pi(X) -> 2ndspos(X, from(0()))
           , 2ndspos(0(), Z) -> rnil()
           , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
           , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
           , times(0(), Y) -> 0()}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^2))
      
      Proof:
        The weightgap principle applies, where following rules are oriented strictly:
        
        TRS Component: {square(X) -> times(X, X)}
        
        Interpretation of nonconstant growth:
        -------------------------------------
          The following argument positions are usable:
            Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
            Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
            Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
            Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
            Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
          Interpretation Functions:
           from(x1) = [1 1] x1 + [0]
                      [0 0]      [0]
           cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                          [0 0]      [1 1]      [1]
           n__from(x1) = [0 0] x1 + [0]
                         [1 1]      [0]
           s(x1) = [1 0] x1 + [0]
                   [0 0]      [0]
           2ndspos(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                             [0 0]      [0 0]      [1]
           0() = [0]
                 [0]
           rnil() = [0]
                    [0]
           cons2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                           [0 1]      [0 0]      [0]
           activate(x1) = [1 1] x1 + [0]
                          [0 0]      [0]
           rcons(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                           [0 0]      [0 0]      [1]
           posrecip(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
           2ndsneg(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                             [0 0]      [0 0]      [1]
           negrecip(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
           pi(x1) = [0 0] x1 + [0]
                    [0 0]      [2]
           plus(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                          [0 1]      [0 0]      [1]
           times(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                           [0 0]      [1 1]      [1]
           square(x1) = [0 0] x1 + [2]
                        [1 1]      [2]
        
        The strictly oriented rules are moved into the weak component.
        
        We consider the following Problem:
        
          Strict Trs:
            {  from(X) -> cons(X, n__from(s(X)))
             , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
               rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
             , 2ndsneg(0(), Z) -> rnil()
             , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
               rcons(negrecip(Y), 2ndspos(N, activate(Z)))
             , plus(0(), Y) -> Y
             , plus(s(X), Y) -> s(plus(X, Y))
             , times(s(X), Y) -> plus(Y, times(X, Y))
             , from(X) -> n__from(X)
             , activate(n__from(X)) -> from(X)
             , activate(X) -> X}
          Weak Trs:
            {  square(X) -> times(X, X)
             , pi(X) -> 2ndspos(X, from(0()))
             , 2ndspos(0(), Z) -> rnil()
             , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
             , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
             , times(0(), Y) -> 0()}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(?,O(n^2))
        
        Proof:
          The weightgap principle applies, where following rules are oriented strictly:
          
          TRS Component: {plus(0(), Y) -> Y}
          
          Interpretation of nonconstant growth:
          -------------------------------------
            The following argument positions are usable:
              Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
              Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
              Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
              Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
              Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
            Interpretation Functions:
             from(x1) = [1 1] x1 + [0]
                        [0 0]      [0]
             cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                            [0 0]      [1 1]      [1]
             n__from(x1) = [0 0] x1 + [0]
                           [1 1]      [0]
             s(x1) = [1 0] x1 + [0]
                     [0 0]      [0]
             2ndspos(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                               [0 0]      [0 0]      [1]
             0() = [0]
                   [0]
             rnil() = [0]
                      [0]
             cons2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                             [0 1]      [0 0]      [0]
             activate(x1) = [1 1] x1 + [0]
                            [0 0]      [0]
             rcons(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                             [0 0]      [0 0]      [1]
             posrecip(x1) = [0 0] x1 + [0]
                            [0 0]      [0]
             2ndsneg(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                               [0 0]      [0 0]      [1]
             negrecip(x1) = [0 0] x1 + [0]
                            [0 0]      [0]
             pi(x1) = [0 0] x1 + [0]
                      [0 0]      [2]
             plus(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                            [0 1]      [0 1]      [0]
             times(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [1]
             square(x1) = [0 0] x1 + [0]
                          [0 0]      [2]
          
          The strictly oriented rules are moved into the weak component.
          
          We consider the following Problem:
          
            Strict Trs:
              {  from(X) -> cons(X, n__from(s(X)))
               , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                 rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
               , 2ndsneg(0(), Z) -> rnil()
               , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                 rcons(negrecip(Y), 2ndspos(N, activate(Z)))
               , plus(s(X), Y) -> s(plus(X, Y))
               , times(s(X), Y) -> plus(Y, times(X, Y))
               , from(X) -> n__from(X)
               , activate(n__from(X)) -> from(X)
               , activate(X) -> X}
            Weak Trs:
              {  plus(0(), Y) -> Y
               , square(X) -> times(X, X)
               , pi(X) -> 2ndspos(X, from(0()))
               , 2ndspos(0(), Z) -> rnil()
               , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
               , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
               , times(0(), Y) -> 0()}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(?,O(n^2))
          
          Proof:
            The weightgap principle applies, where following rules are oriented strictly:
            
            TRS Component: {2ndsneg(0(), Z) -> rnil()}
            
            Interpretation of nonconstant growth:
            -------------------------------------
              The following argument positions are usable:
                Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
              We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
              Interpretation Functions:
               from(x1) = [1 1] x1 + [0]
                          [0 0]      [0]
               cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                              [0 0]      [1 1]      [0]
               n__from(x1) = [0 0] x1 + [0]
                             [1 1]      [0]
               s(x1) = [1 0] x1 + [0]
                       [0 0]      [1]
               2ndspos(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                 [0 0]      [0 0]      [0]
               0() = [0]
                     [0]
               rnil() = [0]
                        [0]
               cons2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                               [0 1]      [0 0]      [0]
               activate(x1) = [1 1] x1 + [0]
                              [0 0]      [3]
               rcons(x1, x2) = [0 0] x1 + [1 1] x2 + [1]
                               [0 0]      [0 0]      [1]
               posrecip(x1) = [0 0] x1 + [0]
                              [0 0]      [0]
               2ndsneg(x1, x2) = [0 0] x1 + [1 1] x2 + [2]
                                 [0 0]      [0 0]      [1]
               negrecip(x1) = [0 0] x1 + [0]
                              [0 0]      [0]
               pi(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
               plus(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
               times(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                               [0 0]      [0 1]      [1]
               square(x1) = [0 0] x1 + [0]
                            [0 1]      [1]
            
            The strictly oriented rules are moved into the weak component.
            
            We consider the following Problem:
            
              Strict Trs:
                {  from(X) -> cons(X, n__from(s(X)))
                 , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                   rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                 , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                   rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                 , plus(s(X), Y) -> s(plus(X, Y))
                 , times(s(X), Y) -> plus(Y, times(X, Y))
                 , from(X) -> n__from(X)
                 , activate(n__from(X)) -> from(X)
                 , activate(X) -> X}
              Weak Trs:
                {  2ndsneg(0(), Z) -> rnil()
                 , plus(0(), Y) -> Y
                 , square(X) -> times(X, X)
                 , pi(X) -> 2ndspos(X, from(0()))
                 , 2ndspos(0(), Z) -> rnil()
                 , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                 , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                 , times(0(), Y) -> 0()}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: YES(?,O(n^2))
            
            Proof:
              The weightgap principle applies, where following rules are oriented strictly:
              
              TRS Component: {activate(n__from(X)) -> from(X)}
              
              Interpretation of nonconstant growth:
              -------------------------------------
                The following argument positions are usable:
                  Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                  Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                  Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                  Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                  Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
                We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                Interpretation Functions:
                 from(x1) = [1 1] x1 + [0]
                            [0 0]      [0]
                 cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                                [0 0]      [1 1]      [1]
                 n__from(x1) = [0 0] x1 + [0]
                               [1 1]      [0]
                 s(x1) = [1 0] x1 + [0]
                         [0 0]      [0]
                 2ndspos(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                   [0 0]      [0 0]      [1]
                 0() = [0]
                       [0]
                 rnil() = [0]
                          [0]
                 cons2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                 [0 1]      [0 0]      [0]
                 activate(x1) = [1 1] x1 + [2]
                                [0 0]      [3]
                 rcons(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                 [0 0]      [0 0]      [1]
                 posrecip(x1) = [0 0] x1 + [0]
                                [0 0]      [0]
                 2ndsneg(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                   [0 0]      [0 0]      [2]
                 negrecip(x1) = [0 0] x1 + [0]
                                [0 0]      [0]
                 pi(x1) = [0 0] x1 + [0]
                          [0 0]      [2]
                 plus(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                [0 1]      [0 1]      [1]
                 times(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                 [0 0]      [0 1]      [1]
                 square(x1) = [0 0] x1 + [0]
                              [0 1]      [2]
              
              The strictly oriented rules are moved into the weak component.
              
              We consider the following Problem:
              
                Strict Trs:
                  {  from(X) -> cons(X, n__from(s(X)))
                   , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                     rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                   , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                     rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                   , plus(s(X), Y) -> s(plus(X, Y))
                   , times(s(X), Y) -> plus(Y, times(X, Y))
                   , from(X) -> n__from(X)
                   , activate(X) -> X}
                Weak Trs:
                  {  activate(n__from(X)) -> from(X)
                   , 2ndsneg(0(), Z) -> rnil()
                   , plus(0(), Y) -> Y
                   , square(X) -> times(X, X)
                   , pi(X) -> 2ndspos(X, from(0()))
                   , 2ndspos(0(), Z) -> rnil()
                   , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                   , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                   , times(0(), Y) -> 0()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(?,O(n^2))
              
              Proof:
                The weightgap principle applies, where following rules are oriented strictly:
                
                TRS Component: {times(s(X), Y) -> plus(Y, times(X, Y))}
                
                Interpretation of nonconstant growth:
                -------------------------------------
                  The following argument positions are usable:
                    Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                    Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                    Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                    Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                    Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
                  We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                  Interpretation Functions:
                   from(x1) = [1 1] x1 + [0]
                              [0 0]      [0]
                   cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                                  [0 0]      [1 1]      [0]
                   n__from(x1) = [0 1] x1 + [0]
                                 [1 0]      [0]
                   s(x1) = [1 0] x1 + [0]
                           [0 1]      [1]
                   2ndspos(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                     [0 0]      [0 0]      [1]
                   0() = [0]
                         [0]
                   rnil() = [0]
                            [0]
                   cons2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                   [0 1]      [0 0]      [0]
                   activate(x1) = [1 1] x1 + [0]
                                  [0 0]      [0]
                   rcons(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                                   [0 0]      [0 0]      [1]
                   posrecip(x1) = [0 0] x1 + [0]
                                  [0 0]      [0]
                   2ndsneg(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                     [0 0]      [0 0]      [1]
                   negrecip(x1) = [0 0] x1 + [0]
                                  [0 0]      [0]
                   pi(x1) = [0 0] x1 + [0]
                            [0 0]      [2]
                   plus(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                  [0 0]      [0 1]      [0]
                   times(x1, x2) = [0 1] x1 + [1 0] x2 + [0]
                                   [0 0]      [0 0]      [0]
                   square(x1) = [1 1] x1 + [0]
                                [0 0]      [0]
                
                The strictly oriented rules are moved into the weak component.
                
                We consider the following Problem:
                
                  Strict Trs:
                    {  from(X) -> cons(X, n__from(s(X)))
                     , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                       rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                     , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                       rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                     , plus(s(X), Y) -> s(plus(X, Y))
                     , from(X) -> n__from(X)
                     , activate(X) -> X}
                  Weak Trs:
                    {  times(s(X), Y) -> plus(Y, times(X, Y))
                     , activate(n__from(X)) -> from(X)
                     , 2ndsneg(0(), Z) -> rnil()
                     , plus(0(), Y) -> Y
                     , square(X) -> times(X, X)
                     , pi(X) -> 2ndspos(X, from(0()))
                     , 2ndspos(0(), Z) -> rnil()
                     , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                     , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                     , times(0(), Y) -> 0()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(?,O(n^2))
                
                Proof:
                  The weightgap principle applies, where following rules are oriented strictly:
                  
                  TRS Component:
                    {2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                     rcons(posrecip(Y), 2ndsneg(N, activate(Z)))}
                  
                  Interpretation of nonconstant growth:
                  -------------------------------------
                    The following argument positions are usable:
                      Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                      Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                      Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                      Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                      Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
                    We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                    Interpretation Functions:
                     from(x1) = [1 1] x1 + [0]
                                [0 0]      [0]
                     cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                                    [0 0]      [1 1]      [3]
                     n__from(x1) = [0 1] x1 + [0]
                                   [1 0]      [0]
                     s(x1) = [1 0] x1 + [0]
                             [0 1]      [2]
                     2ndspos(x1, x2) = [1 1] x1 + [1 1] x2 + [0]
                                       [0 0]      [0 0]      [1]
                     0() = [0]
                           [0]
                     rnil() = [0]
                              [0]
                     cons2(x1, x2) = [1 0] x1 + [1 1] x2 + [3]
                                     [0 1]      [0 0]      [0]
                     activate(x1) = [1 1] x1 + [0]
                                    [0 0]      [0]
                     rcons(x1, x2) = [1 1] x1 + [1 1] x2 + [0]
                                     [0 0]      [0 0]      [1]
                     posrecip(x1) = [0 1] x1 + [1]
                                    [1 0]      [0]
                     2ndsneg(x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                                       [0 1]      [0 0]      [0]
                     negrecip(x1) = [1 0] x1 + [0]
                                    [0 0]      [0]
                     pi(x1) = [1 1] x1 + [0]
                              [0 0]      [2]
                     plus(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                                    [0 0]      [0 1]      [0]
                     times(x1, x2) = [0 1] x1 + [0 0] x2 + [0]
                                     [0 0]      [0 0]      [0]
                     square(x1) = [0 1] x1 + [0]
                                  [0 0]      [0]
                  
                  The strictly oriented rules are moved into the weak component.
                  
                  We consider the following Problem:
                  
                    Strict Trs:
                      {  from(X) -> cons(X, n__from(s(X)))
                       , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                         rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                       , plus(s(X), Y) -> s(plus(X, Y))
                       , from(X) -> n__from(X)
                       , activate(X) -> X}
                    Weak Trs:
                      {  2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                         rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                       , times(s(X), Y) -> plus(Y, times(X, Y))
                       , activate(n__from(X)) -> from(X)
                       , 2ndsneg(0(), Z) -> rnil()
                       , plus(0(), Y) -> Y
                       , square(X) -> times(X, X)
                       , pi(X) -> 2ndspos(X, from(0()))
                       , 2ndspos(0(), Z) -> rnil()
                       , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                       , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                       , times(0(), Y) -> 0()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(?,O(n^2))
                  
                  Proof:
                    The weightgap principle applies, where following rules are oriented strictly:
                    
                    TRS Component:
                      {2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                       rcons(negrecip(Y), 2ndspos(N, activate(Z)))}
                    
                    Interpretation of nonconstant growth:
                    -------------------------------------
                      The following argument positions are usable:
                        Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                        Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                        Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                        Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                        Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
                      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                      Interpretation Functions:
                       from(x1) = [1 1] x1 + [0]
                                  [0 0]      [0]
                       cons(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
                                      [0 0]      [1 1]      [0]
                       n__from(x1) = [0 0] x1 + [0]
                                     [1 1]      [0]
                       s(x1) = [1 0] x1 + [3]
                               [0 1]      [2]
                       2ndspos(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                         [0 0]      [0 0]      [1]
                       0() = [0]
                             [0]
                       rnil() = [0]
                                [0]
                       cons2(x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                                       [0 1]      [0 0]      [0]
                       activate(x1) = [1 1] x1 + [0]
                                      [0 0]      [0]
                       rcons(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                       [0 0]      [0 0]      [1]
                       posrecip(x1) = [0 0] x1 + [0]
                                      [0 0]      [0]
                       2ndsneg(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                         [0 0]      [0 0]      [1]
                       negrecip(x1) = [0 0] x1 + [0]
                                      [0 0]      [0]
                       pi(x1) = [0 0] x1 + [0]
                                [0 0]      [2]
                       plus(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                      [0 0]      [0 1]      [0]
                       times(x1, x2) = [1 1] x1 + [0 0] x2 + [0]
                                       [0 0]      [0 0]      [0]
                       square(x1) = [1 1] x1 + [0]
                                    [0 0]      [0]
                    
                    The strictly oriented rules are moved into the weak component.
                    
                    We consider the following Problem:
                    
                      Strict Trs:
                        {  from(X) -> cons(X, n__from(s(X)))
                         , plus(s(X), Y) -> s(plus(X, Y))
                         , from(X) -> n__from(X)
                         , activate(X) -> X}
                      Weak Trs:
                        {  2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                           rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                         , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                           rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                         , times(s(X), Y) -> plus(Y, times(X, Y))
                         , activate(n__from(X)) -> from(X)
                         , 2ndsneg(0(), Z) -> rnil()
                         , plus(0(), Y) -> Y
                         , square(X) -> times(X, X)
                         , pi(X) -> 2ndspos(X, from(0()))
                         , 2ndspos(0(), Z) -> rnil()
                         , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                         , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                         , times(0(), Y) -> 0()}
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(?,O(n^2))
                    
                    Proof:
                      The weightgap principle applies, where following rules are oriented strictly:
                      
                      TRS Component: {activate(X) -> X}
                      
                      Interpretation of nonconstant growth:
                      -------------------------------------
                        The following argument positions are usable:
                          Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                          Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                          Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                          Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                          Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
                        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                        Interpretation Functions:
                         from(x1) = [0 0] x1 + [0]
                                    [0 0]      [0]
                         cons(x1, x2) = [0 0] x1 + [1 0] x2 + [3]
                                        [1 0]      [0 0]      [3]
                         n__from(x1) = [0 0] x1 + [2]
                                       [0 0]      [0]
                         s(x1) = [1 0] x1 + [0]
                                 [0 0]      [1]
                         2ndspos(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                           [0 0]      [0 0]      [1]
                         0() = [0]
                               [0]
                         rnil() = [0]
                                  [0]
                         cons2(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                         [0 0]      [0 0]      [3]
                         activate(x1) = [1 0] x1 + [1]
                                        [0 1]      [1]
                         rcons(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                         [1 1]      [0 0]      [1]
                         posrecip(x1) = [0 0] x1 + [0]
                                        [0 0]      [0]
                         2ndsneg(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                           [0 1]      [1 1]      [1]
                         negrecip(x1) = [0 0] x1 + [0]
                                        [0 0]      [0]
                         pi(x1) = [0 0] x1 + [0]
                                  [0 0]      [2]
                         plus(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                        [0 0]      [0 1]      [0]
                         times(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                                         [0 0]      [0 0]      [0]
                         square(x1) = [0 0] x1 + [2]
                                      [0 0]      [0]
                      
                      The strictly oriented rules are moved into the weak component.
                      
                      We consider the following Problem:
                      
                        Strict Trs:
                          {  from(X) -> cons(X, n__from(s(X)))
                           , plus(s(X), Y) -> s(plus(X, Y))
                           , from(X) -> n__from(X)}
                        Weak Trs:
                          {  activate(X) -> X
                           , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                             rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                           , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                             rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                           , times(s(X), Y) -> plus(Y, times(X, Y))
                           , activate(n__from(X)) -> from(X)
                           , 2ndsneg(0(), Z) -> rnil()
                           , plus(0(), Y) -> Y
                           , square(X) -> times(X, X)
                           , pi(X) -> 2ndspos(X, from(0()))
                           , 2ndspos(0(), Z) -> rnil()
                           , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                           , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                           , times(0(), Y) -> 0()}
                        StartTerms: basic terms
                        Strategy: innermost
                      
                      Certificate: YES(?,O(n^2))
                      
                      Proof:
                        The weightgap principle applies, where following rules are oriented strictly:
                        
                        TRS Component: {from(X) -> n__from(X)}
                        
                        Interpretation of nonconstant growth:
                        -------------------------------------
                          The following argument positions are usable:
                            Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                            Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                            Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                            Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                            Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
                          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                          Interpretation Functions:
                           from(x1) = [0 0] x1 + [2]
                                      [0 0]      [0]
                           cons(x1, x2) = [0 0] x1 + [1 0] x2 + [3]
                                          [1 0]      [0 0]      [3]
                           n__from(x1) = [0 0] x1 + [1]
                                         [0 0]      [0]
                           s(x1) = [1 0] x1 + [3]
                                   [0 1]      [1]
                           2ndspos(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                                             [1 0]      [1 1]      [0]
                           0() = [0]
                                 [0]
                           rnil() = [0]
                                    [0]
                           cons2(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
                                           [0 0]      [0 0]      [2]
                           activate(x1) = [1 0] x1 + [2]
                                          [0 1]      [1]
                           rcons(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                                           [0 0]      [0 0]      [1]
                           posrecip(x1) = [0 0] x1 + [2]
                                          [0 0]      [0]
                           2ndsneg(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                             [1 0]      [0 0]      [0]
                           negrecip(x1) = [0 0] x1 + [0]
                                          [0 0]      [0]
                           pi(x1) = [0 0] x1 + [3]
                                    [1 0]      [2]
                           plus(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                          [0 0]      [0 1]      [0]
                           times(x1, x2) = [1 0] x1 + [0 0] x2 + [2]
                                           [1 1]      [0 0]      [1]
                           square(x1) = [1 0] x1 + [2]
                                        [1 1]      [2]
                        
                        The strictly oriented rules are moved into the weak component.
                        
                        We consider the following Problem:
                        
                          Strict Trs:
                            {  from(X) -> cons(X, n__from(s(X)))
                             , plus(s(X), Y) -> s(plus(X, Y))}
                          Weak Trs:
                            {  from(X) -> n__from(X)
                             , activate(X) -> X
                             , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                               rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                             , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                               rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                             , times(s(X), Y) -> plus(Y, times(X, Y))
                             , activate(n__from(X)) -> from(X)
                             , 2ndsneg(0(), Z) -> rnil()
                             , plus(0(), Y) -> Y
                             , square(X) -> times(X, X)
                             , pi(X) -> 2ndspos(X, from(0()))
                             , 2ndspos(0(), Z) -> rnil()
                             , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                             , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                             , times(0(), Y) -> 0()}
                          StartTerms: basic terms
                          Strategy: innermost
                        
                        Certificate: YES(?,O(n^2))
                        
                        Proof:
                          The weightgap principle applies, where following rules are oriented strictly:
                          
                          TRS Component: {from(X) -> cons(X, n__from(s(X)))}
                          
                          Interpretation of nonconstant growth:
                          -------------------------------------
                            The following argument positions are usable:
                              Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                              Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                              Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                              Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                              Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
                            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                            Interpretation Functions:
                             from(x1) = [0 0] x1 + [1]
                                        [0 0]      [1]
                             cons(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                            [0 0]      [0 0]      [1]
                             n__from(x1) = [0 0] x1 + [0]
                                           [0 0]      [0]
                             s(x1) = [1 0] x1 + [0]
                                     [0 1]      [2]
                             2ndspos(x1, x2) = [0 2] x1 + [1 1] x2 + [0]
                                               [0 0]      [0 0]      [1]
                             0() = [0]
                                   [0]
                             rnil() = [0]
                                      [0]
                             cons2(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                             [0 0]      [0 0]      [0]
                             activate(x1) = [1 0] x1 + [1]
                                            [0 1]      [2]
                             rcons(x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                                             [0 0]      [0 0]      [0]
                             posrecip(x1) = [0 0] x1 + [1]
                                            [0 0]      [0]
                             2ndsneg(x1, x2) = [0 2] x1 + [1 1] x2 + [0]
                                               [0 0]      [0 0]      [0]
                             negrecip(x1) = [0 0] x1 + [0]
                                            [0 0]      [0]
                             pi(x1) = [0 2] x1 + [2]
                                      [0 0]      [1]
                             plus(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                            [0 0]      [0 1]      [0]
                             times(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                             [0 0]      [0 0]      [1]
                             square(x1) = [1 1] x1 + [0]
                                          [0 0]      [2]
                          
                          The strictly oriented rules are moved into the weak component.
                          
                          We consider the following Problem:
                          
                            Strict Trs: {plus(s(X), Y) -> s(plus(X, Y))}
                            Weak Trs:
                              {  from(X) -> cons(X, n__from(s(X)))
                               , from(X) -> n__from(X)
                               , activate(X) -> X
                               , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                                 rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                               , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                                 rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                               , times(s(X), Y) -> plus(Y, times(X, Y))
                               , activate(n__from(X)) -> from(X)
                               , 2ndsneg(0(), Z) -> rnil()
                               , plus(0(), Y) -> Y
                               , square(X) -> times(X, X)
                               , pi(X) -> 2ndspos(X, from(0()))
                               , 2ndspos(0(), Z) -> rnil()
                               , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                               , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                               , times(0(), Y) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(?,O(n^2))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {plus(s(X), Y) -> s(plus(X, Y))}
                              Weak Trs:
                                {  from(X) -> cons(X, n__from(s(X)))
                                 , from(X) -> n__from(X)
                                 , activate(X) -> X
                                 , 2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
                                   rcons(negrecip(Y), 2ndspos(N, activate(Z)))
                                 , 2ndspos(s(N), cons2(X, cons(Y, Z))) ->
                                   rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
                                 , times(s(X), Y) -> plus(Y, times(X, Y))
                                 , activate(n__from(X)) -> from(X)
                                 , 2ndsneg(0(), Z) -> rnil()
                                 , plus(0(), Y) -> Y
                                 , square(X) -> times(X, X)
                                 , pi(X) -> 2ndspos(X, from(0()))
                                 , 2ndspos(0(), Z) -> rnil()
                                 , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
                                 , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
                                 , times(0(), Y) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(?,O(n^2))
                            
                            Proof:
                              The following argument positions are usable:
                                Uargs(from) = {}, Uargs(cons) = {}, Uargs(n__from) = {},
                                Uargs(s) = {1}, Uargs(2ndspos) = {2}, Uargs(cons2) = {2},
                                Uargs(activate) = {}, Uargs(rcons) = {2}, Uargs(posrecip) = {},
                                Uargs(2ndsneg) = {2}, Uargs(negrecip) = {}, Uargs(pi) = {},
                                Uargs(plus) = {2}, Uargs(times) = {}, Uargs(square) = {}
                              We have the following restricted  polynomial interpretation:
                              Interpretation Functions:
                               [from](x1) = 0
                               [cons](x1, x2) = x2
                               [n__from](x1) = 0
                               [s](x1) = 2 + x1
                               [2ndspos](x1, x2) = 2*x2
                               [0]() = 0
                               [rnil]() = 0
                               [cons2](x1, x2) = x2
                               [activate](x1) = x1
                               [rcons](x1, x2) = x2
                               [posrecip](x1) = 0
                               [2ndsneg](x1, x2) = 2*x2
                               [negrecip](x1) = 0
                               [pi](x1) = 0
                               [plus](x1, x2) = 2*x1 + x2
                               [times](x1, x2) = 2*x1 + x1*x2
                               [square](x1) = 2*x1 + 2*x1^2

Hurray, we answered YES(?,O(n^2))