WORST_CASE(?,O(n^2))
* Step 1: Sum WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            -(x,0()) -> x
            -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
            -(0(),y) -> 0()
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {-/2,p/1} / {0/0,greater/2,if/3,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,p} and constructors {0,greater,if,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            -(x,0()) -> x
            -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
            -(0(),y) -> 0()
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {-/2,p/1} / {0/0,greater/2,if/3,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,p} and constructors {0,greater,if,s}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(-) = {2},
          uargs(if) = {2},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {-,p}
        TcT has computed the following interpretation:
                p(-) = 2 + x1 + x2
                p(0) = 15         
          p(greater) = 4          
               p(if) = x2         
                p(p) = x1         
                p(s) = x1         
        
        Following rules are strictly oriented:
        -(x,0()) = 17 + x
                 > x     
                 = x     
        
        -(0(),y) = 17 + y
                 > 15    
                 = 0()   
        
        
        Following rules are (at-least) weakly oriented:
        -(x,s(y)) =  2 + x + y                              
                  >= 2 + x + y                              
                  =  if(greater(x,s(y)),s(-(x,p(s(y)))),0())
        
           p(0()) =  15                                     
                  >= 15                                     
                  =  0()                                    
        
          p(s(x)) =  x                                      
                  >= x                                      
                  =  x                                      
        
* Step 3: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
            p(0()) -> 0()
            p(s(x)) -> x
        - Weak TRS:
            -(x,0()) -> x
            -(0(),y) -> 0()
        - Signature:
            {-/2,p/1} / {0/0,greater/2,if/3,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,p} and constructors {0,greater,if,s}
    + Applied Processor:
        Ara {araHeuristics = Heuristics, minDegree = 2, maxDegree = 2, araTimeout = 3, araRuleShifting = Nothing}
    + Details:
        Signatures used:
        ----------------
          - :: ["A"(0, 0) x "A"(6, 3)] -(0)-> "A"(0, 0)
          0 :: [] -(0)-> "A"(3, 3)
          0 :: [] -(0)-> "A"(6, 3)
          0 :: [] -(0)-> "A"(0, 0)
          greater :: ["A"(0, 0) x "A"(1, 0)] -(0)-> "A"(0, 1)
          if :: ["A"(0, 0) x "A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0)
          p :: ["A"(3, 3)] -(1)-> "A"(6, 3)
          s :: ["A"(9, 3)] -(6)-> "A"(6, 3)
          s :: ["A"(6, 3)] -(3)-> "A"(3, 3)
          s :: ["A"(1, 0)] -(1)-> "A"(1, 0)
          s :: ["A"(0, 0)] -(0)-> "A"(0, 0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
        
        

WORST_CASE(?,O(n^2))