(STRATEGY
    INNERMOST)

(VAR
    x451 x63 x79 x112 x128 x44 x7 x8 x5 x6 x4 x3 x2 x1 x229 x10 x56 x64 x22 x14
    x16 x20 x113)
(RULES
    divide_ys#1(Cons(x451,Cons(x63,x79)),S(0())) -> Cons(Cons(x451,Nil())
                                                        ,Cons(Cons(x63,x79)
                                                             ,Nil()))
    divide_ys#1(Cons(x451,Cons(x112,x128)),S(S(x44))) ->
      Cons(Cons(x451,Cons(x112,take#2(x44,x128))),Cons(drop#2(x44,x128),Nil()))
    cond_merge_ys_zs_2(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) ->
      Cons(x4,merge#2(x3,Cons(x5,x6)))
    cond_merge_ys_zs_2(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) ->
      Cons(x2,merge#2(Cons(x7,x8),x1))
    merge#2(Nil(),x2) -> x2
    merge#2(Cons(x4,x2),Nil()) -> Cons(x4,x2)
    merge#2(Cons(x8,x6),Cons(x4,x2)) -> cond_merge_ys_zs_2(leq#2(x8,x4)
                                                          ,Cons(x8,x6)
                                                          ,Cons(x4,x2)
                                                          ,x8
                                                          ,x6
                                                          ,x4
                                                          ,x2)
    dc#1(Nil()) -> Nil()
    dc#1(Cons(x229,Nil())) -> Cons(x229,Nil())
    dc#1(Cons(x3,Cons(x2,x1))) ->
      const_f#2(Cons(x3,Cons(x2,x1))
               ,map#2(divide_ys#1(Cons(x3,Cons(x2,x1))
                                 ,S(halve#1(length#1(x1))))))
    drop#2(0(),x2) -> x2
    drop#2(S(0()),Nil()) -> bot[1]()
    drop#2(S(x10),Cons(x56,x64)) -> drop#2(x10,x64)
    take#2(0(),x2) -> Nil()
    take#2(S(0()),Nil()) -> Cons(bot[0](),Nil())
    take#2(S(x22),Cons(x56,x64)) -> Cons(x56,take#2(x22,x64))
    halve#1(0()) -> 0()
    halve#1(S(0())) -> S(0())
    halve#1(S(S(x14))) -> S(halve#1(x14))
    const_f#2(Cons(x4,Cons(x5,x6)),Cons(x3,Cons(x2,x1))) -> merge#2(x3,x2)
    leq#2(0(),x16) -> True()
    leq#2(S(x20),0()) -> False()
    leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
    length#1(Nil()) -> 0()
    length#1(Cons(x6,x8)) -> S(length#1(x8))
    map#2(Nil()) -> Nil()
    map#2(Cons(x2,x1)) -> Cons(dc#1(x2),map#2(x1))
    main(x113) -> dc#1(x113))