MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            gen(x,y,z) -> if(ge(z,x),x,y,z)
            generate(x,y) -> gen(x,y,0())
            if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
            if(true(),x,y,z) -> nil()
            sum(cons(0(),xs)) -> sum(xs)
            sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
            sum(nil()) -> 0()
            times(x,y) -> sum(generate(x,y))
        - Signature:
            {ge/2,gen/3,generate/2,if/4,sum/1,times/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ge,gen,generate,if,sum,times} and constructors {0,cons
            ,false,nil,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          ge#(x,0()) -> c_1()
          ge#(0(),s(y)) -> c_2()
          ge#(s(x),s(y)) -> c_3(ge#(x,y))
          gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
          generate#(x,y) -> c_5(gen#(x,y,0()))
          if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
          if#(true(),x,y,z) -> c_7()
          sum#(cons(0(),xs)) -> c_8(sum#(xs))
          sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
          sum#(nil()) -> c_10()
          times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(x,0()) -> c_1()
            ge#(0(),s(y)) -> c_2()
            ge#(s(x),s(y)) -> c_3(ge#(x,y))
            gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
            generate#(x,y) -> c_5(gen#(x,y,0()))
            if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
            if#(true(),x,y,z) -> c_7()
            sum#(cons(0(),xs)) -> c_8(sum#(xs))
            sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
            sum#(nil()) -> c_10()
            times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            gen(x,y,z) -> if(ge(z,x),x,y,z)
            generate(x,y) -> gen(x,y,0())
            if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
            if(true(),x,y,z) -> nil()
            sum(cons(0(),xs)) -> sum(xs)
            sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
            sum(nil()) -> 0()
            times(x,y) -> sum(generate(x,y))
        - Signature:
            {ge/2,gen/3,generate/2,if/4,sum/1,times/2,ge#/2,gen#/3,generate#/2,if#/4,sum#/1,times#/2} / {0/0,cons/2
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ge#,gen#,generate#,if#,sum#,times#} and constructors {0
            ,cons,false,nil,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          ge(x,0()) -> true()
          ge(0(),s(y)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          gen(x,y,z) -> if(ge(z,x),x,y,z)
          generate(x,y) -> gen(x,y,0())
          if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
          if(true(),x,y,z) -> nil()
          ge#(x,0()) -> c_1()
          ge#(0(),s(y)) -> c_2()
          ge#(s(x),s(y)) -> c_3(ge#(x,y))
          gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
          generate#(x,y) -> c_5(gen#(x,y,0()))
          if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
          if#(true(),x,y,z) -> c_7()
          sum#(cons(0(),xs)) -> c_8(sum#(xs))
          sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
          sum#(nil()) -> c_10()
          times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(x,0()) -> c_1()
            ge#(0(),s(y)) -> c_2()
            ge#(s(x),s(y)) -> c_3(ge#(x,y))
            gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
            generate#(x,y) -> c_5(gen#(x,y,0()))
            if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
            if#(true(),x,y,z) -> c_7()
            sum#(cons(0(),xs)) -> c_8(sum#(xs))
            sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
            sum#(nil()) -> c_10()
            times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            gen(x,y,z) -> if(ge(z,x),x,y,z)
            generate(x,y) -> gen(x,y,0())
            if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
            if(true(),x,y,z) -> nil()
        - Signature:
            {ge/2,gen/3,generate/2,if/4,sum/1,times/2,ge#/2,gen#/3,generate#/2,if#/4,sum#/1,times#/2} / {0/0,cons/2
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ge#,gen#,generate#,if#,sum#,times#} and constructors {0
            ,cons,false,nil,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,7,10}
        by application of
          Pre({1,2,7,10}) = {3,4,8,11}.
        Here rules are labelled as follows:
          1: ge#(x,0()) -> c_1()
          2: ge#(0(),s(y)) -> c_2()
          3: ge#(s(x),s(y)) -> c_3(ge#(x,y))
          4: gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
          5: generate#(x,y) -> c_5(gen#(x,y,0()))
          6: if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
          7: if#(true(),x,y,z) -> c_7()
          8: sum#(cons(0(),xs)) -> c_8(sum#(xs))
          9: sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
          10: sum#(nil()) -> c_10()
          11: times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_3(ge#(x,y))
            gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
            generate#(x,y) -> c_5(gen#(x,y,0()))
            if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
            sum#(cons(0(),xs)) -> c_8(sum#(xs))
            sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
            times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
        - Weak DPs:
            ge#(x,0()) -> c_1()
            ge#(0(),s(y)) -> c_2()
            if#(true(),x,y,z) -> c_7()
            sum#(nil()) -> c_10()
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            gen(x,y,z) -> if(ge(z,x),x,y,z)
            generate(x,y) -> gen(x,y,0())
            if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
            if(true(),x,y,z) -> nil()
        - Signature:
            {ge/2,gen/3,generate/2,if/4,sum/1,times/2,ge#/2,gen#/3,generate#/2,if#/4,sum#/1,times#/2} / {0/0,cons/2
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ge#,gen#,generate#,if#,sum#,times#} and constructors {0
            ,cons,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:ge#(s(x),s(y)) -> c_3(ge#(x,y))
             -->_1 ge#(0(),s(y)) -> c_2():9
             -->_1 ge#(x,0()) -> c_1():8
             -->_1 ge#(s(x),s(y)) -> c_3(ge#(x,y)):1
          
          2:S:gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
             -->_1 if#(false(),x,y,z) -> c_6(gen#(x,y,s(z))):4
             -->_1 if#(true(),x,y,z) -> c_7():10
             -->_2 ge#(0(),s(y)) -> c_2():9
             -->_2 ge#(x,0()) -> c_1():8
             -->_2 ge#(s(x),s(y)) -> c_3(ge#(x,y)):1
          
          3:S:generate#(x,y) -> c_5(gen#(x,y,0()))
             -->_1 gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x)):2
          
          4:S:if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
             -->_1 gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x)):2
          
          5:S:sum#(cons(0(),xs)) -> c_8(sum#(xs))
             -->_1 sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs))):6
             -->_1 sum#(nil()) -> c_10():11
             -->_1 sum#(cons(0(),xs)) -> c_8(sum#(xs)):5
          
          6:S:sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
             -->_1 sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs))):6
             -->_1 sum#(cons(0(),xs)) -> c_8(sum#(xs)):5
          
          7:S:times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
             -->_1 sum#(nil()) -> c_10():11
             -->_1 sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs))):6
             -->_1 sum#(cons(0(),xs)) -> c_8(sum#(xs)):5
             -->_2 generate#(x,y) -> c_5(gen#(x,y,0())):3
          
          8:W:ge#(x,0()) -> c_1()
             
          
          9:W:ge#(0(),s(y)) -> c_2()
             
          
          10:W:if#(true(),x,y,z) -> c_7()
             
          
          11:W:sum#(nil()) -> c_10()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          11: sum#(nil()) -> c_10()
          10: if#(true(),x,y,z) -> c_7()
          8: ge#(x,0()) -> c_1()
          9: ge#(0(),s(y)) -> c_2()
* Step 5: NaturalMI MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_3(ge#(x,y))
            gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
            generate#(x,y) -> c_5(gen#(x,y,0()))
            if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
            sum#(cons(0(),xs)) -> c_8(sum#(xs))
            sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
            times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            gen(x,y,z) -> if(ge(z,x),x,y,z)
            generate(x,y) -> gen(x,y,0())
            if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
            if(true(),x,y,z) -> nil()
        - Signature:
            {ge/2,gen/3,generate/2,if/4,sum/1,times/2,ge#/2,gen#/3,generate#/2,if#/4,sum#/1,times#/2} / {0/0,cons/2
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ge#,gen#,generate#,if#,sum#,times#} and constructors {0
            ,cons,false,nil,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_3) = {1},
          uargs(c_4) = {1,2},
          uargs(c_5) = {1},
          uargs(c_6) = {1},
          uargs(c_8) = {1},
          uargs(c_9) = {1},
          uargs(c_11) = {1,2}
        
        Following symbols are considered usable:
          {ge#,gen#,generate#,if#,sum#,times#}
        TcT has computed the following interpretation:
                  p(0) = [3]                  
               p(cons) = [4]                  
              p(false) = [0]                  
                 p(ge) = [2] x2 + [10]        
                p(gen) = [2] x2 + [4] x3 + [2]
           p(generate) = [1] x2 + [1]         
                 p(if) = [2] x3 + [8] x4 + [0]
                p(nil) = [8]                  
                  p(s) = [4]                  
                p(sum) = [1] x1 + [1]         
              p(times) = [1] x1 + [1] x2 + [2]
               p(true) = [1]                  
                p(ge#) = [0]                  
               p(gen#) = [0]                  
          p(generate#) = [8] x1 + [8] x2 + [8]
                p(if#) = [0]                  
               p(sum#) = [0]                  
             p(times#) = [8] x1 + [8] x2 + [9]
                p(c_1) = [8]                  
                p(c_2) = [0]                  
                p(c_3) = [4] x1 + [0]         
                p(c_4) = [1] x1 + [8] x2 + [0]
                p(c_5) = [1] x1 + [4]         
                p(c_6) = [2] x1 + [0]         
                p(c_7) = [2]                  
                p(c_8) = [4] x1 + [0]         
                p(c_9) = [1] x1 + [0]         
               p(c_10) = [1]                  
               p(c_11) = [2] x1 + [1] x2 + [1]
        
        Following rules are strictly oriented:
        generate#(x,y) = [8] x + [8] y + [8]
                       > [4]                
                       = c_5(gen#(x,y,0())) 
        
        
        Following rules are (at-least) weakly oriented:
             ge#(s(x),s(y)) =  [0]                                     
                            >= [0]                                     
                            =  c_3(ge#(x,y))                           
        
                gen#(x,y,z) =  [0]                                     
                            >= [0]                                     
                            =  c_4(if#(ge(z,x),x,y,z),ge#(z,x))        
        
         if#(false(),x,y,z) =  [0]                                     
                            >= [0]                                     
                            =  c_6(gen#(x,y,s(z)))                     
        
         sum#(cons(0(),xs)) =  [0]                                     
                            >= [0]                                     
                            =  c_8(sum#(xs))                           
        
        sum#(cons(s(x),xs)) =  [0]                                     
                            >= [0]                                     
                            =  c_9(sum#(cons(x,xs)))                   
        
                times#(x,y) =  [8] x + [8] y + [9]                     
                            >= [8] x + [8] y + [9]                     
                            =  c_11(sum#(generate(x,y)),generate#(x,y))
        
* Step 6: NaturalMI MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_3(ge#(x,y))
            gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
            if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
            sum#(cons(0(),xs)) -> c_8(sum#(xs))
            sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
            times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
        - Weak DPs:
            generate#(x,y) -> c_5(gen#(x,y,0()))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            gen(x,y,z) -> if(ge(z,x),x,y,z)
            generate(x,y) -> gen(x,y,0())
            if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
            if(true(),x,y,z) -> nil()
        - Signature:
            {ge/2,gen/3,generate/2,if/4,sum/1,times/2,ge#/2,gen#/3,generate#/2,if#/4,sum#/1,times#/2} / {0/0,cons/2
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ge#,gen#,generate#,if#,sum#,times#} and constructors {0
            ,cons,false,nil,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_3) = {1},
          uargs(c_4) = {1,2},
          uargs(c_5) = {1},
          uargs(c_6) = {1},
          uargs(c_8) = {1},
          uargs(c_9) = {1},
          uargs(c_11) = {1,2}
        
        Following symbols are considered usable:
          {ge#,gen#,generate#,if#,sum#,times#}
        TcT has computed the following interpretation:
                  p(0) = [8]                    
               p(cons) = [13]                   
              p(false) = [0]                    
                 p(ge) = [0]                    
                p(gen) = [2] x3 + [2]           
           p(generate) = [1] x1 + [4] x2 + [1]  
                 p(if) = [2] x1 + [8] x2 + [0]  
                p(nil) = [1]                    
                  p(s) = [0]                    
                p(sum) = [1] x1 + [1]           
              p(times) = [1] x1 + [1] x2 + [1]  
               p(true) = [0]                    
                p(ge#) = [0]                    
               p(gen#) = [0]                    
          p(generate#) = [3] x1 + [2] x2 + [0]  
                p(if#) = [0]                    
               p(sum#) = [0]                    
             p(times#) = [12] x1 + [9] x2 + [13]
                p(c_1) = [0]                    
                p(c_2) = [1]                    
                p(c_3) = [2] x1 + [0]           
                p(c_4) = [8] x1 + [1] x2 + [0]  
                p(c_5) = [1] x1 + [0]           
                p(c_6) = [8] x1 + [0]           
                p(c_7) = [4]                    
                p(c_8) = [8] x1 + [0]           
                p(c_9) = [1] x1 + [0]           
               p(c_10) = [0]                    
               p(c_11) = [4] x1 + [4] x2 + [11] 
        
        Following rules are strictly oriented:
        times#(x,y) = [12] x + [9] y + [13]                   
                    > [12] x + [8] y + [11]                   
                    = c_11(sum#(generate(x,y)),generate#(x,y))
        
        
        Following rules are (at-least) weakly oriented:
             ge#(s(x),s(y)) =  [0]                             
                            >= [0]                             
                            =  c_3(ge#(x,y))                   
        
                gen#(x,y,z) =  [0]                             
                            >= [0]                             
                            =  c_4(if#(ge(z,x),x,y,z),ge#(z,x))
        
             generate#(x,y) =  [3] x + [2] y + [0]             
                            >= [0]                             
                            =  c_5(gen#(x,y,0()))              
        
         if#(false(),x,y,z) =  [0]                             
                            >= [0]                             
                            =  c_6(gen#(x,y,s(z)))             
        
         sum#(cons(0(),xs)) =  [0]                             
                            >= [0]                             
                            =  c_8(sum#(xs))                   
        
        sum#(cons(s(x),xs)) =  [0]                             
                            >= [0]                             
                            =  c_9(sum#(cons(x,xs)))           
        
* Step 7: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          ge#(s(x),s(y)) -> c_3(ge#(x,y))
          gen#(x,y,z) -> c_4(if#(ge(z,x),x,y,z),ge#(z,x))
          if#(false(),x,y,z) -> c_6(gen#(x,y,s(z)))
          sum#(cons(0(),xs)) -> c_8(sum#(xs))
          sum#(cons(s(x),xs)) -> c_9(sum#(cons(x,xs)))
      - Weak DPs:
          generate#(x,y) -> c_5(gen#(x,y,0()))
          times#(x,y) -> c_11(sum#(generate(x,y)),generate#(x,y))
      - Weak TRS:
          ge(x,0()) -> true()
          ge(0(),s(y)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          gen(x,y,z) -> if(ge(z,x),x,y,z)
          generate(x,y) -> gen(x,y,0())
          if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
          if(true(),x,y,z) -> nil()
      - Signature:
          {ge/2,gen/3,generate/2,if/4,sum/1,times/2,ge#/2,gen#/3,generate#/2,if#/4,sum#/1,times#/2} / {0/0,cons/2
          ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {ge#,gen#,generate#,if#,sum#,times#} and constructors {0
          ,cons,false,nil,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE