WORST_CASE(?,O(n^2))
* Step 1: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            div_active(x,y) -> div(x,y)
            div_active(0(),s(y)) -> 0()
            div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
            ge_active(x,y) -> ge(x,y)
            ge_active(x,0()) -> true()
            ge_active(0(),s(y)) -> false()
            ge_active(s(x),s(y)) -> ge_active(x,y)
            if_active(x,y,z) -> if(x,y,z)
            if_active(false(),x,y) -> mark(y)
            if_active(true(),x,y) -> mark(x)
            mark(0()) -> 0()
            mark(div(x,y)) -> div_active(mark(x),y)
            mark(ge(x,y)) -> ge_active(x,y)
            mark(if(x,y,z)) -> if_active(mark(x),y,z)
            mark(minus(x,y)) -> minus_active(x,y)
            mark(s(x)) -> s(mark(x))
            minus_active(x,y) -> minus(x,y)
            minus_active(0(),y) -> 0()
            minus_active(s(x),s(y)) -> minus_active(x,y)
        - Signature:
            {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1
            ,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark
            ,minus_active} and constructors {0,div,false,ge,if,minus,s,true}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> A(14, 0)
          0 :: [] -(0)-> A(0, 0)
          0 :: [] -(0)-> A(4, 0)
          0 :: [] -(0)-> A(8, 7)
          0 :: [] -(0)-> A(5, 0)
          0 :: [] -(0)-> A(13, 7)
          0 :: [] -(0)-> A(15, 13)
          0 :: [] -(0)-> A(13, 11)
          div :: [A(15, 7) x A(0, 0)] -(7)-> A(8, 7)
          div :: [A(14, 0) x A(0, 0)] -(0)-> A(14, 0)
          div_active :: [A(14, 0) x A(0, 0)] -(6)-> A(7, 0)
          false :: [] -(0)-> A(7, 0)
          false :: [] -(0)-> A(15, 6)
          ge :: [A(7, 0) x A(0, 0)] -(0)-> A(8, 7)
          ge :: [A(0, 0) x A(0, 0)] -(0)-> A(10, 0)
          ge_active :: [A(4, 0) x A(0, 0)] -(1)-> A(8, 0)
          if :: [A(8, 7) x A(8, 7) x A(8, 7)] -(7)-> A(8, 7)
          if :: [A(7, 0) x A(7, 0) x A(7, 0)] -(0)-> A(7, 0)
          if_active :: [A(7, 0) x A(8, 7) x A(8, 7)] -(3)-> A(7, 0)
          mark :: [A(8, 7)] -(2)-> A(7, 0)
          minus :: [A(7, 0) x A(0, 0)] -(0)-> A(8, 7)
          minus :: [A(7, 0) x A(0, 0)] -(0)-> A(15, 7)
          minus :: [A(5, 0) x A(0, 0)] -(0)-> A(13, 5)
          minus_active :: [A(5, 0) x A(0, 0)] -(1)-> A(10, 5)
          s :: [A(0, 0)] -(0)-> A(0, 0)
          s :: [A(14, 0)] -(14)-> A(14, 0)
          s :: [A(4, 0)] -(4)-> A(4, 0)
          s :: [A(8, 7)] -(8)-> A(8, 7)
          s :: [A(5, 0)] -(5)-> A(5, 0)
          s :: [A(7, 0)] -(7)-> A(7, 0)
          true :: [] -(0)-> A(7, 0)
          true :: [] -(0)-> A(15, 6)
        
        
        Cost-free Signatures used:
        --------------------------
          0 :: [] -(0)-> A_cf(0, 0)
          0 :: [] -(0)-> A_cf(7, 0)
          0 :: [] -(0)-> A_cf(11, 3)
          0 :: [] -(0)-> A_cf(5, 0)
          0 :: [] -(0)-> A_cf(15, 11)
          0 :: [] -(0)-> A_cf(10, 2)
          div :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          div :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
          div_active :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          div_active :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
          false :: [] -(0)-> A_cf(0, 0)
          false :: [] -(0)-> A_cf(3, 2)
          false :: [] -(0)-> A_cf(7, 0)
          false :: [] -(0)-> A_cf(11, 2)
          ge :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          ge :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(2, 0)
          ge :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
          ge :: [A_cf(5, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 5)
          ge :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(13, 0)
          ge_active :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          ge_active :: [A_cf(0, 0) x A_cf(0, 0)] -(2)-> A_cf(0, 0)
          ge_active :: [A_cf(5, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 0)
          ge_active :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
          if :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          if :: [A_cf(7, 0) x A_cf(7, 0) x A_cf(7, 0)] -(0)-> A_cf(7, 0)
          if_active :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          if_active :: [A_cf(7, 0) x A_cf(7, 0) x A_cf(15, 8)] -(0)-> A_cf(7, 0)
          if_active :: [A_cf(7, 0) x A_cf(7, 0) x A_cf(7, 0)] -(0)-> A_cf(7, 0)
          mark :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
          mark :: [A_cf(7, 0)] -(0)-> A_cf(7, 0)
          minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
          minus :: [A_cf(1, 0) x A_cf(0, 0)] -(0)-> A_cf(9, 1)
          minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 0)
          minus_active :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          minus_active :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 0)
          s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
          s :: [A_cf(7, 0)] -(7)-> A_cf(7, 0)
          s :: [A_cf(5, 0)] -(5)-> A_cf(5, 0)
          true :: [] -(0)-> A_cf(0, 0)
          true :: [] -(0)-> A_cf(3, 2)
          true :: [] -(0)-> A_cf(7, 0)
          true :: [] -(0)-> A_cf(11, 2)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          0_A :: [] -(0)-> A(1, 0)
          0_A :: [] -(0)-> A(0, 1)
          div_A :: [A(1, 0) x A(0, 0)] -(0)-> A(1, 0)
          div_A :: [A(1, 1) x A(0, 0)] -(1)-> A(0, 1)
          false_A :: [] -(0)-> A(1, 0)
          false_A :: [] -(0)-> A(0, 1)
          ge_A :: [A(0, 0) x A(0, 0)] -(0)-> A(1, 0)
          ge_A :: [A(1, 0) x A(0, 0)] -(0)-> A(0, 1)
          if_A :: [A(1, 0) x A(1, 0) x A(1, 0)] -(0)-> A(1, 0)
          if_A :: [A(0, 1) x A(0, 1) x A(0, 1)] -(1)-> A(0, 1)
          minus_A :: [A(0, 0) x A(0, 0)] -(0)-> A(1, 0)
          minus_A :: [A(1, 0) x A(0, 0)] -(0)-> A(0, 1)
          s_A :: [A(1, 0)] -(1)-> A(1, 0)
          s_A :: [A(0, 1)] -(0)-> A(0, 1)
          true_A :: [] -(0)-> A(1, 0)
          true_A :: [] -(0)-> A(0, 1)
        
* Step 2: Open MAYBE
    - Strict TRS:
        div_active(x,y) -> div(x,y)
        div_active(0(),s(y)) -> 0()
        div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
        ge_active(x,y) -> ge(x,y)
        ge_active(x,0()) -> true()
        ge_active(0(),s(y)) -> false()
        ge_active(s(x),s(y)) -> ge_active(x,y)
        if_active(x,y,z) -> if(x,y,z)
        if_active(false(),x,y) -> mark(y)
        if_active(true(),x,y) -> mark(x)
        mark(0()) -> 0()
        mark(div(x,y)) -> div_active(mark(x),y)
        mark(ge(x,y)) -> ge_active(x,y)
        mark(if(x,y,z)) -> if_active(mark(x),y,z)
        mark(minus(x,y)) -> minus_active(x,y)
        mark(s(x)) -> s(mark(x))
        minus_active(x,y) -> minus(x,y)
        minus_active(0(),y) -> 0()
        minus_active(s(x),s(y)) -> minus_active(x,y)
    - Signature:
        {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1
        ,true/0}
    - Obligation:
        innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark
        ,minus_active} and constructors {0,div,false,ge,if,minus,s,true}
Following problems could not be solved:
  - Strict TRS:
      div_active(x,y) -> div(x,y)
      div_active(0(),s(y)) -> 0()
      div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      ge_active(x,y) -> ge(x,y)
      ge_active(x,0()) -> true()
      ge_active(0(),s(y)) -> false()
      ge_active(s(x),s(y)) -> ge_active(x,y)
      if_active(x,y,z) -> if(x,y,z)
      if_active(false(),x,y) -> mark(y)
      if_active(true(),x,y) -> mark(x)
      mark(0()) -> 0()
      mark(div(x,y)) -> div_active(mark(x),y)
      mark(ge(x,y)) -> ge_active(x,y)
      mark(if(x,y,z)) -> if_active(mark(x),y,z)
      mark(minus(x,y)) -> minus_active(x,y)
      mark(s(x)) -> s(mark(x))
      minus_active(x,y) -> minus(x,y)
      minus_active(0(),y) -> 0()
      minus_active(s(x),s(y)) -> minus_active(x,y)
  - Signature:
      {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1
      ,true/0}
  - Obligation:
      innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark
      ,minus_active} and constructors {0,div,false,ge,if,minus,s,true}
WORST_CASE(?,O(n^2))