MAYBE

Problem:
 eq(0(),0()) -> true()
 eq(0(),s(y)) -> false()
 eq(s(x),0()) -> false()
 eq(s(x),s(y)) -> eq(x,y)
 lt(0(),s(y)) -> true()
 lt(x,0()) -> false()
 lt(s(x),s(y)) -> lt(x,y)
 bin2s(nil()) -> 0()
 bin2s(cons(x,xs)) -> bin2ss(x,xs)
 bin2ss(x,nil()) -> x
 bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
 bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 log(0()) -> 0()
 log(s(0())) -> 0()
 log(s(s(x))) -> s(log(half(s(s(x)))))
 more(nil()) -> nil()
 more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
 s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
 s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
 if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
 if1(false(),x,y,lists) -> s2bin2(x,lists)
 s2bin2(x,nil()) -> bug_list_not()
 s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
 if2(true(),x,xs,ys) -> xs
 if2(false(),x,xs,ys) -> s2bin2(x,ys)

Proof:
 DP Processor:
  DPs:
   eq#(s(x),s(y)) -> eq#(x,y)
   lt#(s(x),s(y)) -> lt#(x,y)
   bin2s#(cons(x,xs)) -> bin2ss#(x,xs)
   bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs)
   bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs)
   half#(s(s(x))) -> half#(x)
   log#(s(s(x))) -> half#(s(s(x)))
   log#(s(s(x))) -> log#(half(s(s(x))))
   s2bin#(x) -> s2bin1#(x,0(),cons(nil(),nil()))
   s2bin1#(x,y,lists) -> log#(x)
   s2bin1#(x,y,lists) -> lt#(y,log(x))
   s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists)
   if1#(true(),x,y,lists) -> more#(lists)
   if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists))
   if1#(false(),x,y,lists) -> s2bin2#(x,lists)
   s2bin2#(x,cons(xs,ys)) -> bin2s#(xs)
   s2bin2#(x,cons(xs,ys)) -> eq#(x,bin2s(xs))
   s2bin2#(x,cons(xs,ys)) -> if2#(eq(x,bin2s(xs)),x,xs,ys)
   if2#(false(),x,xs,ys) -> s2bin2#(x,ys)
  TRS:
   eq(0(),0()) -> true()
   eq(0(),s(y)) -> false()
   eq(s(x),0()) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   lt(0(),s(y)) -> true()
   lt(x,0()) -> false()
   lt(s(x),s(y)) -> lt(x,y)
   bin2s(nil()) -> 0()
   bin2s(cons(x,xs)) -> bin2ss(x,xs)
   bin2ss(x,nil()) -> x
   bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
   bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
   log(0()) -> 0()
   log(s(0())) -> 0()
   log(s(s(x))) -> s(log(half(s(s(x)))))
   more(nil()) -> nil()
   more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
   s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
   s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
   if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
   if1(false(),x,y,lists) -> s2bin2(x,lists)
   s2bin2(x,nil()) -> bug_list_not()
   s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
   if2(true(),x,xs,ys) -> xs
   if2(false(),x,xs,ys) -> s2bin2(x,ys)
  Usable Rule Processor:
   DPs:
    eq#(s(x),s(y)) -> eq#(x,y)
    lt#(s(x),s(y)) -> lt#(x,y)
    bin2s#(cons(x,xs)) -> bin2ss#(x,xs)
    bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs)
    bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs)
    half#(s(s(x))) -> half#(x)
    log#(s(s(x))) -> half#(s(s(x)))
    log#(s(s(x))) -> log#(half(s(s(x))))
    s2bin#(x) -> s2bin1#(x,0(),cons(nil(),nil()))
    s2bin1#(x,y,lists) -> log#(x)
    s2bin1#(x,y,lists) -> lt#(y,log(x))
    s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists)
    if1#(true(),x,y,lists) -> more#(lists)
    if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists))
    if1#(false(),x,y,lists) -> s2bin2#(x,lists)
    s2bin2#(x,cons(xs,ys)) -> bin2s#(xs)
    s2bin2#(x,cons(xs,ys)) -> eq#(x,bin2s(xs))
    s2bin2#(x,cons(xs,ys)) -> if2#(eq(x,bin2s(xs)),x,xs,ys)
    if2#(false(),x,xs,ys) -> s2bin2#(x,ys)
   TRS:
    f33(x,y) -> x
    f33(x,y) -> y
    half(s(s(x))) -> s(half(x))
    half(0()) -> 0()
    half(s(0())) -> 0()
    log(0()) -> 0()
    log(s(0())) -> 0()
    log(s(s(x))) -> s(log(half(s(s(x)))))
    lt(0(),s(y)) -> true()
    lt(x,0()) -> false()
    lt(s(x),s(y)) -> lt(x,y)
    more(nil()) -> nil()
    more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
    bin2s(nil()) -> 0()
    bin2s(cons(x,xs)) -> bin2ss(x,xs)
    bin2ss(x,nil()) -> x
    bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
    bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
    eq(0(),0()) -> true()
    eq(0(),s(y)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
   CDG Processor:
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
     lt#(s(x),s(y)) -> lt#(x,y)
     bin2s#(cons(x,xs)) -> bin2ss#(x,xs)
     bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs)
     bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs)
     half#(s(s(x))) -> half#(x)
     log#(s(s(x))) -> half#(s(s(x)))
     log#(s(s(x))) -> log#(half(s(s(x))))
     s2bin#(x) -> s2bin1#(x,0(),cons(nil(),nil()))
     s2bin1#(x,y,lists) -> log#(x)
     s2bin1#(x,y,lists) -> lt#(y,log(x))
     s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists)
     if1#(true(),x,y,lists) -> more#(lists)
     if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists))
     if1#(false(),x,y,lists) -> s2bin2#(x,lists)
     s2bin2#(x,cons(xs,ys)) -> bin2s#(xs)
     s2bin2#(x,cons(xs,ys)) -> eq#(x,bin2s(xs))
     s2bin2#(x,cons(xs,ys)) -> if2#(eq(x,bin2s(xs)),x,xs,ys)
     if2#(false(),x,xs,ys) -> s2bin2#(x,ys)
    TRS:
     f33(x,y) -> x
     f33(x,y) -> y
     half(s(s(x))) -> s(half(x))
     half(0()) -> 0()
     half(s(0())) -> 0()
     log(0()) -> 0()
     log(s(0())) -> 0()
     log(s(s(x))) -> s(log(half(s(s(x)))))
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     more(nil()) -> nil()
     more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
     bin2s(nil()) -> 0()
     bin2s(cons(x,xs)) -> bin2ss(x,xs)
     bin2ss(x,nil()) -> x
     bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
     bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
    graph:
     if2#(false(),x,xs,ys) -> s2bin2#(x,ys) ->
     s2bin2#(x,cons(xs,ys)) -> bin2s#(xs)
     if2#(false(),x,xs,ys) -> s2bin2#(x,ys) ->
     s2bin2#(x,cons(xs,ys)) -> eq#(x,bin2s(xs))
     if2#(false(),x,xs,ys) -> s2bin2#(x,ys) ->
     s2bin2#(x,cons(xs,ys)) -> if2#(eq(x,bin2s(xs)),x,xs,ys)
     s2bin2#(x,cons(xs,ys)) -> if2#(eq(x,bin2s(xs)),x,xs,ys) ->
     if2#(false(),x,xs,ys) -> s2bin2#(x,ys)
     s2bin2#(x,cons(xs,ys)) -> bin2s#(xs) ->
     bin2s#(cons(x,xs)) -> bin2ss#(x,xs)
     s2bin2#(x,cons(xs,ys)) -> eq#(x,bin2s(xs)) ->
     eq#(s(x),s(y)) -> eq#(x,y)
     if1#(false(),x,y,lists) -> s2bin2#(x,lists) ->
     s2bin2#(x,cons(xs,ys)) -> bin2s#(xs)
     if1#(false(),x,y,lists) -> s2bin2#(x,lists) ->
     s2bin2#(x,cons(xs,ys)) -> eq#(x,bin2s(xs))
     if1#(false(),x,y,lists) -> s2bin2#(x,lists) ->
     s2bin2#(x,cons(xs,ys)) -> if2#(eq(x,bin2s(xs)),x,xs,ys)
     if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists)) ->
     s2bin1#(x,y,lists) -> log#(x)
     if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists)) ->
     s2bin1#(x,y,lists) -> lt#(y,log(x))
     if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists)) ->
     s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists)
     s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists) ->
     if1#(true(),x,y,lists) -> more#(lists)
     s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists) ->
     if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists))
     s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists) ->
     if1#(false(),x,y,lists) -> s2bin2#(x,lists)
     s2bin1#(x,y,lists) -> log#(x) -> log#(s(s(x))) -> half#(s(s(x)))
     s2bin1#(x,y,lists) -> log#(x) ->
     log#(s(s(x))) -> log#(half(s(s(x))))
     s2bin1#(x,y,lists) -> lt#(y,log(x)) ->
     lt#(s(x),s(y)) -> lt#(x,y)
     s2bin#(x) -> s2bin1#(x,0(),cons(nil(),nil())) ->
     s2bin1#(x,y,lists) -> log#(x)
     s2bin#(x) -> s2bin1#(x,0(),cons(nil(),nil())) ->
     s2bin1#(x,y,lists) -> lt#(y,log(x))
     s2bin#(x) -> s2bin1#(x,0(),cons(nil(),nil())) ->
     s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists)
     log#(s(s(x))) -> log#(half(s(s(x)))) ->
     log#(s(s(x))) -> half#(s(s(x)))
     log#(s(s(x))) -> log#(half(s(s(x)))) ->
     log#(s(s(x))) -> log#(half(s(s(x))))
     log#(s(s(x))) -> half#(s(s(x))) -> half#(s(s(x))) -> half#(x)
     half#(s(s(x))) -> half#(x) ->
     half#(s(s(x))) -> half#(x)
     bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs) ->
     bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs)
     bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs) ->
     bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs)
     bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs) ->
     bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs)
     bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs) ->
     bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs)
     bin2s#(cons(x,xs)) -> bin2ss#(x,xs) ->
     bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs)
     bin2s#(cons(x,xs)) -> bin2ss#(x,xs) ->
     bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs)
     lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
     eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
    Restore Modifier:
     DPs:
      eq#(s(x),s(y)) -> eq#(x,y)
      lt#(s(x),s(y)) -> lt#(x,y)
      bin2s#(cons(x,xs)) -> bin2ss#(x,xs)
      bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs)
      bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs)
      half#(s(s(x))) -> half#(x)
      log#(s(s(x))) -> half#(s(s(x)))
      log#(s(s(x))) -> log#(half(s(s(x))))
      s2bin#(x) -> s2bin1#(x,0(),cons(nil(),nil()))
      s2bin1#(x,y,lists) -> log#(x)
      s2bin1#(x,y,lists) -> lt#(y,log(x))
      s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists)
      if1#(true(),x,y,lists) -> more#(lists)
      if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists))
      if1#(false(),x,y,lists) -> s2bin2#(x,lists)
      s2bin2#(x,cons(xs,ys)) -> bin2s#(xs)
      s2bin2#(x,cons(xs,ys)) -> eq#(x,bin2s(xs))
      s2bin2#(x,cons(xs,ys)) -> if2#(eq(x,bin2s(xs)),x,xs,ys)
      if2#(false(),x,xs,ys) -> s2bin2#(x,ys)
     TRS:
      eq(0(),0()) -> true()
      eq(0(),s(y)) -> false()
      eq(s(x),0()) -> false()
      eq(s(x),s(y)) -> eq(x,y)
      lt(0(),s(y)) -> true()
      lt(x,0()) -> false()
      lt(s(x),s(y)) -> lt(x,y)
      bin2s(nil()) -> 0()
      bin2s(cons(x,xs)) -> bin2ss(x,xs)
      bin2ss(x,nil()) -> x
      bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
      bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
      half(0()) -> 0()
      half(s(0())) -> 0()
      half(s(s(x))) -> s(half(x))
      log(0()) -> 0()
      log(s(0())) -> 0()
      log(s(s(x))) -> s(log(half(s(s(x)))))
      more(nil()) -> nil()
      more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
      s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
      s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
      if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
      if1(false(),x,y,lists) -> s2bin2(x,lists)
      s2bin2(x,nil()) -> bug_list_not()
      s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
      if2(true(),x,xs,ys) -> xs
      if2(false(),x,xs,ys) -> s2bin2(x,ys)
     SCC Processor:
      #sccs: 7
      #rules: 10
      #arcs: 33/361
      DPs:
       if1#(true(),x,y,lists) -> s2bin1#(x,s(y),more(lists))
       s2bin1#(x,y,lists) -> if1#(lt(y,log(x)),x,y,lists)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       bin2s(nil()) -> 0()
       bin2s(cons(x,xs)) -> bin2ss(x,xs)
       bin2ss(x,nil()) -> x
       bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
       bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       log(0()) -> 0()
       log(s(0())) -> 0()
       log(s(s(x))) -> s(log(half(s(s(x)))))
       more(nil()) -> nil()
       more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
       s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
       s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
       if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
       if1(false(),x,y,lists) -> s2bin2(x,lists)
       s2bin2(x,nil()) -> bug_list_not()
       s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
       if2(true(),x,xs,ys) -> xs
       if2(false(),x,xs,ys) -> s2bin2(x,ys)
      Open
      
      DPs:
       log#(s(s(x))) -> log#(half(s(s(x))))
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       bin2s(nil()) -> 0()
       bin2s(cons(x,xs)) -> bin2ss(x,xs)
       bin2ss(x,nil()) -> x
       bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
       bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       log(0()) -> 0()
       log(s(0())) -> 0()
       log(s(s(x))) -> s(log(half(s(s(x)))))
       more(nil()) -> nil()
       more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
       s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
       s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
       if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
       if1(false(),x,y,lists) -> s2bin2(x,lists)
       s2bin2(x,nil()) -> bug_list_not()
       s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
       if2(true(),x,xs,ys) -> xs
       if2(false(),x,xs,ys) -> s2bin2(x,ys)
      Open
      
      DPs:
       half#(s(s(x))) -> half#(x)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       bin2s(nil()) -> 0()
       bin2s(cons(x,xs)) -> bin2ss(x,xs)
       bin2ss(x,nil()) -> x
       bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
       bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       log(0()) -> 0()
       log(s(0())) -> 0()
       log(s(s(x))) -> s(log(half(s(s(x)))))
       more(nil()) -> nil()
       more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
       s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
       s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
       if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
       if1(false(),x,y,lists) -> s2bin2(x,lists)
       s2bin2(x,nil()) -> bug_list_not()
       s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
       if2(true(),x,xs,ys) -> xs
       if2(false(),x,xs,ys) -> s2bin2(x,ys)
      Open
      
      DPs:
       lt#(s(x),s(y)) -> lt#(x,y)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       bin2s(nil()) -> 0()
       bin2s(cons(x,xs)) -> bin2ss(x,xs)
       bin2ss(x,nil()) -> x
       bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
       bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       log(0()) -> 0()
       log(s(0())) -> 0()
       log(s(s(x))) -> s(log(half(s(s(x)))))
       more(nil()) -> nil()
       more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
       s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
       s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
       if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
       if1(false(),x,y,lists) -> s2bin2(x,lists)
       s2bin2(x,nil()) -> bug_list_not()
       s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
       if2(true(),x,xs,ys) -> xs
       if2(false(),x,xs,ys) -> s2bin2(x,ys)
      Open
      
      DPs:
       if2#(false(),x,xs,ys) -> s2bin2#(x,ys)
       s2bin2#(x,cons(xs,ys)) -> if2#(eq(x,bin2s(xs)),x,xs,ys)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       bin2s(nil()) -> 0()
       bin2s(cons(x,xs)) -> bin2ss(x,xs)
       bin2ss(x,nil()) -> x
       bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
       bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       log(0()) -> 0()
       log(s(0())) -> 0()
       log(s(s(x))) -> s(log(half(s(s(x)))))
       more(nil()) -> nil()
       more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
       s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
       s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
       if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
       if1(false(),x,y,lists) -> s2bin2(x,lists)
       s2bin2(x,nil()) -> bug_list_not()
       s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
       if2(true(),x,xs,ys) -> xs
       if2(false(),x,xs,ys) -> s2bin2(x,ys)
      Open
      
      DPs:
       bin2ss#(x,cons(1(),xs)) -> bin2ss#(s(double(x)),xs)
       bin2ss#(x,cons(0(),xs)) -> bin2ss#(double(x),xs)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       bin2s(nil()) -> 0()
       bin2s(cons(x,xs)) -> bin2ss(x,xs)
       bin2ss(x,nil()) -> x
       bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
       bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       log(0()) -> 0()
       log(s(0())) -> 0()
       log(s(s(x))) -> s(log(half(s(s(x)))))
       more(nil()) -> nil()
       more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
       s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
       s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
       if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
       if1(false(),x,y,lists) -> s2bin2(x,lists)
       s2bin2(x,nil()) -> bug_list_not()
       s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
       if2(true(),x,xs,ys) -> xs
       if2(false(),x,xs,ys) -> s2bin2(x,ys)
      Open
      
      DPs:
       eq#(s(x),s(y)) -> eq#(x,y)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       bin2s(nil()) -> 0()
       bin2s(cons(x,xs)) -> bin2ss(x,xs)
       bin2ss(x,nil()) -> x
       bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
       bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       log(0()) -> 0()
       log(s(0())) -> 0()
       log(s(s(x))) -> s(log(half(s(s(x)))))
       more(nil()) -> nil()
       more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
       s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
       s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
       if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
       if1(false(),x,y,lists) -> s2bin2(x,lists)
       s2bin2(x,nil()) -> bug_list_not()
       s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
       if2(true(),x,xs,ys) -> xs
       if2(false(),x,xs,ys) -> s2bin2(x,ys)
      Open