MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          active(div(X1,X2)) -> div(active(X1),X2)
          active(div(0(),s(Y))) -> mark(0())
          active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
          active(geq(X,0())) -> mark(true())
          active(geq(0(),s(Y))) -> mark(false())
          active(geq(s(X),s(Y))) -> mark(geq(X,Y))
          active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
          active(if(false(),X,Y)) -> mark(Y)
          active(if(true(),X,Y)) -> mark(X)
          active(minus(0(),Y)) -> mark(0())
          active(minus(s(X),s(Y))) -> mark(minus(X,Y))
          active(s(X)) -> s(active(X))
          div(mark(X1),X2) -> mark(div(X1,X2))
          div(ok(X1),ok(X2)) -> ok(div(X1,X2))
          geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
          if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
          if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
          minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
          proper(0()) -> ok(0())
          proper(div(X1,X2)) -> div(proper(X1),proper(X2))
          proper(false()) -> ok(false())
          proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
          proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
          proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
          proper(s(X)) -> s(proper(X))
          proper(true()) -> ok(true())
          s(mark(X)) -> mark(s(X))
          s(ok(X)) -> ok(s(X))
          top(mark(X)) -> top(proper(X))
          top(ok(X)) -> top(active(X))
      - Signature:
          {active/1,div/2,geq/2,if/3,minus/2,proper/1,s/1,top/1} / {0/0,false/0,mark/1,ok/1,true/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {active,div,geq,if,minus,proper,s,top} and constructors {0
          ,false,mark,ok,true}
  + Applied Processor:
      NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
  + Details:
      Incompatible
MAYBE