(STRATEGY
    INNERMOST)

(VAR
    x2 x4 x8 x6 x5 x3 x1 x12 x112 x144 x160 x18 x14 x10 x11 x7 x9 x20 x48 x56
    x16)
(RULES
    compare_list#2(Nil(),x2) -> True()
    compare_list#2(Cons(x4,x2),Nil()) -> False()
    compare_list#2(Cons(x8,x6),Cons(x4,x2)) -> ite2#3(eqNat#2(x8,x4)
                                                     ,compare_list#2(x6,x2)
                                                     ,leqNat#2(x8,x4))
    cond_mergesort_compare_log_l_l_2(Pair(Cons(x4,x5),Cons(x2,x3)),x1) ->
      merge#3(mergesort#3(x1,Cons(x4,x5)),mergesort#3(x1,Cons(x2,x3)))
    mergesort#3(0(),Cons(x1,x2)) -> Nil()
    mergesort#3(S(S(S(S(S(S(0())))))),Nil()) -> bot[0]()
    mergesort#3(S(x4),Cons(x8,Nil())) -> Cons(x8,Nil())
    mergesort#3(S(x12),Cons(x112,Cons(x144,x160))) ->
      cond_mergesort_compare_log_l_l_2(cond_split_l_2(split#1(x160),x112,x144)
                                      ,x12)
    merge#3(Nil(),x2) -> x2
    merge#3(Cons(x4,x2),Nil()) -> Cons(x4,x2)
    merge#3(Cons(x18,x14),Cons(x10,x6)) -> ite_b#2(compare_list#2(x18,x10)
                                                  ,Cons(x18
                                                       ,merge#3(x14
                                                               ,Cons(x10,x6)))
                                                  ,Cons(x10
                                                       ,merge#3(Cons(x18,x14)
                                                               ,x6)))
    cond_split_l_2(Pair(x11,x12),x7,x9) -> Pair(Cons(x7,x11),Cons(x9,x12))
    split#1(Nil()) -> Pair(Nil(),Nil())
    split#1(Cons(x14,Nil())) -> Pair(Cons(x14,Nil()),Nil())
    split#1(Cons(x14,Cons(x18,x20))) -> cond_split_l_2(split#1(x20),x14,x18)
    ite2#3(True(),x48,x56) -> x48
    ite2#3(False(),x48,x56) -> x56
    ite_b#2(True(),Cons(x6,x8),Cons(x2,x4)) -> Cons(x6,x8)
    ite_b#2(False(),Cons(x6,x8),Cons(x2,x4)) -> Cons(x2,x4)
    eqNat#2(0(),0()) -> True()
    eqNat#2(S(x16),0()) -> False()
    eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2)
    eqNat#2(0(),S(x16)) -> False()
    leqNat#2(x4,0()) -> True()
    leqNat#2(S(x4),S(x2)) -> leqNat#2(x4,x2)
    leqNat#2(0(),S(x12)) -> False()
    main(x1) -> mergesort#3(S(S(S(S(S(S(0())))))),x1))