MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          bin2s(cons(x,xs)) -> bin2ss(x,xs)
          bin2s(nil()) -> 0()
          bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
          bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
          bin2ss(x,nil()) -> x
          eq(0(),0()) -> true()
          eq(0(),s(y)) -> false()
          eq(s(x),0()) -> false()
          eq(s(x),s(y)) -> eq(x,y)
          half(0()) -> 0()
          half(s(0())) -> 0()
          half(s(s(x))) -> s(half(x))
          if1(false(),x,y,lists) -> s2bin2(x,lists)
          if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
          if2(false(),x,xs,ys) -> s2bin2(x,ys)
          if2(true(),x,xs,ys) -> xs
          log(0()) -> 0()
          log(s(0())) -> 0()
          log(s(s(x))) -> s(log(half(s(s(x)))))
          lt(x,0()) -> false()
          lt(0(),s(y)) -> true()
          lt(s(x),s(y)) -> lt(x,y)
          more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
          more(nil()) -> nil()
          s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
          s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
          s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
          s2bin2(x,nil()) -> bug_list_not()
      - Signature:
          {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2} / {0/0,1/0
          ,bug_list_not/0,cons/2,double/1,false/0,nil/0,s/1,true/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {bin2s,bin2ss,eq,half,if1,if2,log,lt,more,s2bin,s2bin1
          ,s2bin2} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true}
  + Applied Processor:
      Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT}
  + Details:
      The input can not be schown compatible.
MAYBE