MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          choice(cons(x,xs)) -> x
          choice(cons(x,xs)) -> choice(xs)
          eq(0(x),1(y)) -> false()
          eq(1(x),0(y)) -> false()
          eq(1(x),1(y)) -> eq(x,y)
          eq(O(x),0(y)) -> eq(x,y)
          eq(nil(),nil()) -> true()
          guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
          guess(nil()) -> nil()
          if(false(),t,e) -> e
          if(true(),t,e) -> t
          member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
          member(x,nil()) -> false()
          negate(0(x)) -> 1(x)
          negate(1(x)) -> 0(x)
          sat(cnf) -> satck(cnf,guess(cnf))
          satck(cnf,assign) -> if(verify(assign),assign,unsat())
          verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
          verify(nil()) -> true()
      - Signature:
          {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
          ,true/0,unsat/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
          ,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
  + Applied Processor:
      NaturalPI {shape = Mixed 3, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing}
  + Details:
      Incompatible
MAYBE