MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { nats() -> adx(zeros())
  , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
  , zeros() -> cons(0(), zeros())
  , incr(cons(X, Y)) -> cons(s(X), incr(Y))
  , hd(cons(X, Y)) -> X
  , tl(cons(X, Y)) -> Y }
Obligation:
  runtime complexity
Answer:
  MAYBE

The input is overlay and right-linear. Switching to innermost
rewriting.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { nats() -> adx(zeros())
  , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
  , zeros() -> cons(0(), zeros())
  , incr(cons(X, Y)) -> cons(s(X), incr(Y))
  , hd(cons(X, Y)) -> X
  , tl(cons(X, Y)) -> Y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
         failed due to the following reason:
         
         The weightgap principle applies (using the following nonconstant
         growth matrix-interpretation)
         
         The following argument positions are usable:
           Uargs(adx) = {1}, Uargs(cons) = {2}, Uargs(incr) = {1}
         
         TcT has computed the following matrix interpretation satisfying
         not(EDA) and not(IDA(1)).
         
                   [nats] = [7]                  
                                                 
                [adx](x1) = [1] x1 + [6]         
                                                 
                  [zeros] = [5]                  
                                                 
           [cons](x1, x2) = [1] x1 + [1] x2 + [1]
                                                 
                      [0] = [7]                  
                                                 
               [incr](x1) = [1] x1 + [7]         
                                                 
                  [s](x1) = [1] x1 + [7]         
                                                 
                 [hd](x1) = [1] x1 + [3]         
                                                 
                 [tl](x1) = [1] x1 + [5]         
         
         The following symbols are considered usable
         
           {nats, adx, zeros, incr, hd, tl}
         
         The order satisfies the following ordering constraints:
         
                     [nats()] = [7]                    
                              ? [11]                   
                              = [adx(zeros())]         
                                                       
            [adx(cons(X, Y))] = [1] X + [1] Y + [7]    
                              ? [1] X + [1] Y + [14]   
                              = [incr(cons(X, adx(Y)))]
                                                       
                    [zeros()] = [5]                    
                              ? [13]                   
                              = [cons(0(), zeros())]   
                                                       
           [incr(cons(X, Y))] = [1] X + [1] Y + [8]    
                              ? [1] X + [1] Y + [15]   
                              = [cons(s(X), incr(Y))]  
                                                       
             [hd(cons(X, Y))] = [1] X + [1] Y + [4]    
                              > [1] X + [0]            
                              = [X]                    
                                                       
             [tl(cons(X, Y))] = [1] X + [1] Y + [6]    
                              > [1] Y + [0]            
                              = [Y]                    
                                                       
         
         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y)) }
         Weak Trs:
           { hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         The weightgap principle applies (using the following nonconstant
         growth matrix-interpretation)
         
         The following argument positions are usable:
           Uargs(adx) = {1}, Uargs(cons) = {2}, Uargs(incr) = {1}
         
         TcT has computed the following matrix interpretation satisfying
         not(EDA) and not(IDA(1)).
         
                   [nats] = [7]                  
                                                 
                [adx](x1) = [1] x1 + [0]         
                                                 
                  [zeros] = [4]                  
                                                 
           [cons](x1, x2) = [1] x1 + [1] x2 + [0]
                                                 
                      [0] = [4]                  
                                                 
               [incr](x1) = [1] x1 + [0]         
                                                 
                  [s](x1) = [1] x1 + [0]         
                                                 
                 [hd](x1) = [1] x1 + [7]         
                                                 
                 [tl](x1) = [1] x1 + [7]         
         
         The following symbols are considered usable
         
           {nats, adx, zeros, incr, hd, tl}
         
         The order satisfies the following ordering constraints:
         
                     [nats()] =  [7]                    
                              >  [4]                    
                              =  [adx(zeros())]         
                                                        
            [adx(cons(X, Y))] =  [1] X + [1] Y + [0]    
                              >= [1] X + [1] Y + [0]    
                              =  [incr(cons(X, adx(Y)))]
                                                        
                    [zeros()] =  [4]                    
                              ?  [8]                    
                              =  [cons(0(), zeros())]   
                                                        
           [incr(cons(X, Y))] =  [1] X + [1] Y + [0]    
                              >= [1] X + [1] Y + [0]    
                              =  [cons(s(X), incr(Y))]  
                                                        
             [hd(cons(X, Y))] =  [1] X + [1] Y + [7]    
                              >  [1] X + [0]            
                              =  [X]                    
                                                        
             [tl(cons(X, Y))] =  [1] X + [1] Y + [7]    
                              >  [1] Y + [0]            
                              =  [Y]                    
                                                        
         
         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict Trs:
           { adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y)) }
         Weak Trs:
           { nats() -> adx(zeros())
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'empty' failed due to the following reason:
            
            Empty strict component of the problem is NOT empty.
         
         2) 'WithProblem' failed due to the following reason:
            
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
            1) 'empty' failed due to the following reason:
               
               Empty strict component of the problem is NOT empty.
            
            2) 'Fastest' failed due to the following reason:
               
               None of the processors succeeded.
               
               Details of failed attempt(s):
               -----------------------------
               1) 'WithProblem' failed due to the following reason:
                  
                  None of the processors succeeded.
                  
                  Details of failed attempt(s):
                  -----------------------------
                  1) 'empty' failed due to the following reason:
                     
                     Empty strict component of the problem is NOT empty.
                  
                  2) 'WithProblem' failed due to the following reason:
                     
                     The weightgap principle applies (using the following nonconstant
                     growth matrix-interpretation)
                     
                     The following argument positions are usable:
                       Uargs(adx) = {1}, Uargs(cons) = {2}, Uargs(incr) = {1}
                     
                     TcT has computed the following matrix interpretation satisfying
                     not(EDA) and not(IDA(1)).
                     
                               [nats] = [7]                      
                                        [7]                      
                                                                 
                            [adx](x1) = [1 1] x1 + [0]           
                                        [0 0]      [0]           
                                                                 
                              [zeros] = [0]                      
                                        [0]                      
                                                                 
                       [cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                        [0 1]      [0 1]      [4]
                                                                 
                                  [0] = [0]                      
                                        [0]                      
                                                                 
                           [incr](x1) = [1 0] x1 + [0]           
                                        [0 0]      [0]           
                                                                 
                              [s](x1) = [0]                      
                                        [0]                      
                                                                 
                             [hd](x1) = [1 0] x1 + [7]           
                                        [0 1]      [7]           
                                                                 
                             [tl](x1) = [1 0] x1 + [7]           
                                        [0 1]      [7]           
                     
                     The following symbols are considered usable
                     
                       {nats, adx, zeros, incr, hd, tl}
                     
                     The order satisfies the following ordering constraints:
                     
                                 [nats()] = [7]                     
                                            [7]                     
                                          > [0]                     
                                            [0]                     
                                          = [adx(zeros())]          
                                                                    
                        [adx(cons(X, Y))] = [1 1] X + [1 1] Y + [4] 
                                            [0 0]     [0 0]     [0] 
                                          > [1 0] X + [1 1] Y + [0] 
                                            [0 0]     [0 0]     [0] 
                                          = [incr(cons(X, adx(Y)))] 
                                                                    
                                [zeros()] = [0]                     
                                            [0]                     
                                          ? [0]                     
                                            [4]                     
                                          = [cons(0(), zeros())]    
                                                                    
                       [incr(cons(X, Y))] = [1 0] X + [1 0] Y + [0] 
                                            [0 0]     [0 0]     [0] 
                                          ? [1 0] Y + [0]           
                                            [0 0]     [4]           
                                          = [cons(s(X), incr(Y))]   
                                                                    
                         [hd(cons(X, Y))] = [1 0] X + [1 0] Y + [7] 
                                            [0 1]     [0 1]     [11]
                                          > [1 0] X + [0]           
                                            [0 1]     [0]           
                                          = [X]                     
                                                                    
                         [tl(cons(X, Y))] = [1 0] X + [1 0] Y + [7] 
                                            [0 1]     [0 1]     [11]
                                          > [1 0] Y + [0]           
                                            [0 1]     [0]           
                                          = [Y]                     
                                                                    
                     
                     Further, it can be verified that all rules not oriented are covered by the weightgap condition.
                     
                     We are left with following problem, upon which TcT provides the
                     certificate MAYBE.
                     
                     Strict Trs:
                       { zeros() -> cons(0(), zeros())
                       , incr(cons(X, Y)) -> cons(s(X), incr(Y)) }
                     Weak Trs:
                       { nats() -> adx(zeros())
                       , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
                       , hd(cons(X, Y)) -> X
                       , tl(cons(X, Y)) -> Y }
                     Obligation:
                       innermost runtime complexity
                     Answer:
                       MAYBE
                     
                     None of the processors succeeded.
                     
                     Details of failed attempt(s):
                     -----------------------------
                     1) 'empty' failed due to the following reason:
                        
                        Empty strict component of the problem is NOT empty.
                     
                     2) 'WithProblem' failed due to the following reason:
                        
                        None of the processors succeeded.
                        
                        Details of failed attempt(s):
                        -----------------------------
                        1) 'empty' failed due to the following reason:
                           
                           Empty strict component of the problem is NOT empty.
                        
                        2) 'WithProblem' failed due to the following reason:
                           
                           Empty strict component of the problem is NOT empty.
                        
                     
                  
               
               2) 'WithProblem' failed due to the following reason:
                  
                  None of the processors succeeded.
                  
                  Details of failed attempt(s):
                  -----------------------------
                  1) 'empty' failed due to the following reason:
                     
                     Empty strict component of the problem is NOT empty.
                  
                  2) 'WithProblem' failed due to the following reason:
                     
                     Empty strict component of the problem is NOT empty.
                  
               
            
         
      
      2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
         due to the following reason:
         
         Computation stopped due to timeout after 5.0 seconds.
      
      3) 'Best' failed due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
            to the following reason:
            
            The input cannot be shown compatible
         
         2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
            following reason:
            
            The input cannot be shown compatible
         
      
   
   2) 'WithProblem (timeout of 60 seconds)' failed due to the
      following reason:
      
      We add the following dependency tuples:
      
      Strict DPs:
        { nats^#() -> c_1(adx^#(zeros()), zeros^#())
        , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
        , zeros^#() -> c_3(zeros^#())
        , incr^#(cons(X, Y)) -> c_4(incr^#(Y))
        , hd^#(cons(X, Y)) -> c_5()
        , tl^#(cons(X, Y)) -> c_6() }
      
      and mark the set of starting terms.
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs:
        { nats^#() -> c_1(adx^#(zeros()), zeros^#())
        , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
        , zeros^#() -> c_3(zeros^#())
        , incr^#(cons(X, Y)) -> c_4(incr^#(Y))
        , hd^#(cons(X, Y)) -> c_5()
        , tl^#(cons(X, Y)) -> c_6() }
      Weak Trs:
        { nats() -> adx(zeros())
        , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
        , zeros() -> cons(0(), zeros())
        , incr(cons(X, Y)) -> cons(s(X), incr(Y))
        , hd(cons(X, Y)) -> X
        , tl(cons(X, Y)) -> Y }
      Obligation:
        innermost runtime complexity
      Answer:
        MAYBE
      
      We estimate the number of application of {5,6} by applications of
      Pre({5,6}) = {}. Here rules are labeled as follows:
      
        DPs:
          { 1: nats^#() -> c_1(adx^#(zeros()), zeros^#())
          , 2: adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
          , 3: zeros^#() -> c_3(zeros^#())
          , 4: incr^#(cons(X, Y)) -> c_4(incr^#(Y))
          , 5: hd^#(cons(X, Y)) -> c_5()
          , 6: tl^#(cons(X, Y)) -> c_6() }
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs:
        { nats^#() -> c_1(adx^#(zeros()), zeros^#())
        , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
        , zeros^#() -> c_3(zeros^#())
        , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
      Weak DPs:
        { hd^#(cons(X, Y)) -> c_5()
        , tl^#(cons(X, Y)) -> c_6() }
      Weak Trs:
        { nats() -> adx(zeros())
        , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
        , zeros() -> cons(0(), zeros())
        , incr(cons(X, Y)) -> cons(s(X), incr(Y))
        , hd(cons(X, Y)) -> X
        , tl(cons(X, Y)) -> Y }
      Obligation:
        innermost runtime complexity
      Answer:
        MAYBE
      
      The following weak DPs constitute a sub-graph of the DG that is
      closed under successors. The DPs are removed.
      
      { hd^#(cons(X, Y)) -> c_5()
      , tl^#(cons(X, Y)) -> c_6() }
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs:
        { nats^#() -> c_1(adx^#(zeros()), zeros^#())
        , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
        , zeros^#() -> c_3(zeros^#())
        , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
      Weak Trs:
        { nats() -> adx(zeros())
        , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
        , zeros() -> cons(0(), zeros())
        , incr(cons(X, Y)) -> cons(s(X), incr(Y))
        , hd(cons(X, Y)) -> X
        , tl(cons(X, Y)) -> Y }
      Obligation:
        innermost runtime complexity
      Answer:
        MAYBE
      
      We analyse the complexity of following sub-problems (R) and (S).
      Problem (S) is obtained from the input problem by shifting strict
      rules from (R) into the weak component:
      
      Problem (R):
      ------------
        Strict DPs:
          { nats^#() -> c_1(adx^#(zeros()), zeros^#())
          , zeros^#() -> c_3(zeros^#()) }
        Weak DPs:
          { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
          , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
        Weak Trs:
          { nats() -> adx(zeros())
          , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
          , zeros() -> cons(0(), zeros())
          , incr(cons(X, Y)) -> cons(s(X), incr(Y))
          , hd(cons(X, Y)) -> X
          , tl(cons(X, Y)) -> Y }
        StartTerms:
          basic terms
          Defined Symbols: nats^# adx^# zeros^# incr^# hd^# tl^#
          Constructors: cons 0 s
        Strategy: innermost
      
      Problem (S):
      ------------
        Strict DPs:
          { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
          , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
        Weak DPs:
          { nats^#() -> c_1(adx^#(zeros()), zeros^#())
          , zeros^#() -> c_3(zeros^#()) }
        Weak Trs:
          { nats() -> adx(zeros())
          , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
          , zeros() -> cons(0(), zeros())
          , incr(cons(X, Y)) -> cons(s(X), incr(Y))
          , hd(cons(X, Y)) -> X
          , tl(cons(X, Y)) -> Y }
        StartTerms:
          basic terms
          Defined Symbols: nats^# adx^# zeros^# incr^# hd^# tl^#
          Constructors: cons 0 s
        Strategy: innermost
      
      Overall, the transformation results in the following sub-problem(s):
      
      Generated new problems:
      -----------------------
      R) Strict DPs:
           { nats^#() -> c_1(adx^#(zeros()), zeros^#())
           , zeros^#() -> c_3(zeros^#()) }
         Weak DPs:
           { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
           , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
         Weak Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y))
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         StartTerms:
           basic terms
           Defined Symbols: nats^# adx^# zeros^# incr^# hd^# tl^#
           Constructors: cons 0 s
         Strategy: innermost
         
         This problem remains open.
      
      S) Strict DPs:
           { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
           , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
         Weak DPs:
           { nats^#() -> c_1(adx^#(zeros()), zeros^#())
           , zeros^#() -> c_3(zeros^#()) }
         Weak Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y))
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         StartTerms:
           basic terms
           Defined Symbols: nats^# adx^# zeros^# incr^# hd^# tl^#
           Constructors: cons 0 s
         Strategy: innermost
         
         This problem remains open.
      
      
      Proofs for generated problems:
      ------------------------------
      R) We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict DPs:
           { nats^#() -> c_1(adx^#(zeros()), zeros^#())
           , zeros^#() -> c_3(zeros^#()) }
         Weak DPs:
           { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
           , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
         Weak Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y))
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         The following weak DPs constitute a sub-graph of the DG that is
         closed under successors. The DPs are removed.
         
         { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
         , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict DPs:
           { nats^#() -> c_1(adx^#(zeros()), zeros^#())
           , zeros^#() -> c_3(zeros^#()) }
         Weak Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y))
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         Due to missing edges in the dependency-graph, the right-hand sides
         of following rules could be simplified:
         
           { nats^#() -> c_1(adx^#(zeros()), zeros^#()) }
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict DPs:
           { nats^#() -> c_1(zeros^#())
           , zeros^#() -> c_2(zeros^#()) }
         Weak Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y))
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         No rule is usable, rules are removed from the input problem.
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict DPs:
           { nats^#() -> c_1(zeros^#())
           , zeros^#() -> c_2(zeros^#()) }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'empty' failed due to the following reason:
            
            Empty strict component of the problem is NOT empty.
         
         2) 'WithProblem' failed due to the following reason:
            
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
            1) 'empty' failed due to the following reason:
               
               Empty strict component of the problem is NOT empty.
            
            2) 'Fastest' failed due to the following reason:
               
               None of the processors succeeded.
               
               Details of failed attempt(s):
               -----------------------------
               1) 'WithProblem' failed due to the following reason:
                  
                  We use the processor 'polynomial interpretation' to orient
                  following rules strictly.
                  
                  DPs: { nats^#() -> c_1(zeros^#()) }
                  
                  The induced complexity on above rules (modulo remaining rules) is
                  YES(?,O(n^3)) . These rules are moved into the corresponding weak
                  component(s).
                  
                  Sub-proof:
                  ----------
                    The following argument positions are considered usable:
                    
                      Uargs(c_1) = {1}, Uargs(c_2) = {1}
                    
                    TcT has computed the following constructor-restricted polynomial
                    interpretation.
                    
                          [nats]() = 0                                                                                
                                                                                                                      
                         [adx](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                         [zeros]() = 0                                                                                
                                                                                                                      
                    [cons](x1, x2) = x1 + x2                                                                          
                                                                                                                      
                             [0]() = 0                                                                                
                                                                                                                      
                        [incr](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                           [s](x1) = x1                                                                               
                                                                                                                      
                          [hd](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                          [tl](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                        [nats^#]() = 3                                                                                
                                                                                                                      
                     [c_1](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1*x2^2 + 3*x1^2 + 3*x1^2*x2 + 3*x1^3 + 3*x2 + 3*x2^2 + 3*x2^3
                                                                                                                      
                       [adx^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                       [zeros^#]() = 0                                                                                
                                                                                                                      
                     [c_2](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1*x2^2 + 3*x1^2 + 3*x1^2*x2 + 3*x1^3 + 3*x2 + 3*x2^2 + 3*x2^3
                                                                                                                      
                      [incr^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                         [c_3](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                         [c_4](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                        [hd^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                           [c_5]() = 0                                                                                
                                                                                                                      
                        [tl^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                           [c_6]() = 0                                                                                
                                                                                                                      
                             [c]() = 0                                                                                
                                                                                                                      
                         [c_1](x1) = 1 + 3*x1 + 3*x1^2 + 3*x1^3                                                       
                                                                                                                      
                         [c_2](x1) = 3*x1 + 3*x1^2 + 3*x1^3                                                           
                                                                                                                      
                    
                    The following symbols are considered usable
                    
                      {nats^#, adx^#, zeros^#, incr^#, hd^#, tl^#}
                    
                    This order satisfies the following ordering constraints.
                    
                       [nats^#()] =  3               
                                  >  1               
                                  =  [c_1(zeros^#())]
                                                     
                      [zeros^#()] =                  
                                  >=                 
                                  =  [c_2(zeros^#())]
                                                     
                  
                  We return to the main proof.
                  
                  We are left with following problem, upon which TcT provides the
                  certificate MAYBE.
                  
                  Strict DPs: { zeros^#() -> c_2(zeros^#()) }
                  Weak DPs: { nats^#() -> c_1(zeros^#()) }
                  Obligation:
                    innermost runtime complexity
                  Answer:
                    MAYBE
                  
                  None of the processors succeeded.
                  
                  Details of failed attempt(s):
                  -----------------------------
                  1) 'empty' failed due to the following reason:
                     
                     Empty strict component of the problem is NOT empty.
                  
                  2) 'Polynomial Path Order (PS)' failed due to the following reason:
                     
                     The input cannot be shown compatible
                  
               
               2) 'Fastest (timeout of 5 seconds)' failed due to the following
                  reason:
                  
                  Computation stopped due to timeout after 5.0 seconds.
               
               3) 'Polynomial Path Order (PS)' failed due to the following reason:
                  
                  The input cannot be shown compatible
               
            
         
      
      S) We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict DPs:
           { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
           , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
         Weak DPs:
           { nats^#() -> c_1(adx^#(zeros()), zeros^#())
           , zeros^#() -> c_3(zeros^#()) }
         Weak Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y))
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         The following weak DPs constitute a sub-graph of the DG that is
         closed under successors. The DPs are removed.
         
         { zeros^#() -> c_3(zeros^#()) }
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict DPs:
           { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
           , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
         Weak DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) }
         Weak Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y))
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         Due to missing edges in the dependency-graph, the right-hand sides
         of following rules could be simplified:
         
           { nats^#() -> c_1(adx^#(zeros()), zeros^#()) }
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict DPs:
           { adx^#(cons(X, Y)) -> c_1(incr^#(cons(X, adx(Y))), adx^#(Y))
           , incr^#(cons(X, Y)) -> c_2(incr^#(Y)) }
         Weak DPs: { nats^#() -> c_3(adx^#(zeros())) }
         Weak Trs:
           { nats() -> adx(zeros())
           , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y))
           , hd(cons(X, Y)) -> X
           , tl(cons(X, Y)) -> Y }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         We replace rewrite rules by usable rules:
         
           Weak Usable Rules:
             { adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
             , zeros() -> cons(0(), zeros())
             , incr(cons(X, Y)) -> cons(s(X), incr(Y)) }
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict DPs:
           { adx^#(cons(X, Y)) -> c_1(incr^#(cons(X, adx(Y))), adx^#(Y))
           , incr^#(cons(X, Y)) -> c_2(incr^#(Y)) }
         Weak DPs: { nats^#() -> c_3(adx^#(zeros())) }
         Weak Trs:
           { adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
           , zeros() -> cons(0(), zeros())
           , incr(cons(X, Y)) -> cons(s(X), incr(Y)) }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         All rules are usable.
         
         No progress on transformation, no sub-problems were generated.
      
   


Arrrr..