(STRATEGY
    INNERMOST)

(VAR
    x1 x2 x19 x11 x4 x3 x6 x8 x20 x24 x10 x12 x16)
(RULES
    compare_list_l1#1(Nil(),x1) -> True()
    compare_list_l1#1(Cons(x2,x1),Nil()) -> False()
    compare_list_l1#1(Cons(x19,x2),Cons(x11,x4)) ->
      ite3_b#2(eqNat#2(x19,x11),compare_list_l1#1(x2,x4),leqNat#2(x19,x11))
    cond_quicksort_gt_xyz_1(Pair(x3,x2),x1) -> append#2(quicksort#2(x3)
                                                       ,Cons(x1
                                                            ,quicksort#2(x2)))
    quicksort#2(Nil()) -> Nil()
    quicksort#2(Cons(x4,x6)) ->
      cond_quicksort_gt_xyz_1(partition#2(compare_list_l1(x4),x6),x4)
    cond_partition_f_l_1(Pair(x4,x3),compare_list_l1(x2),x1) ->
      ite_b#2(compare_list_l1#1(x2,x1)
             ,Pair(x4,Cons(x1,x3))
             ,Pair(Cons(x1,x4),x3))
    partition#2(compare_list_l1(x1),Nil()) -> Pair(Nil(),Nil())
    partition#2(compare_list_l1(x3),Cons(x2,x1)) ->
      cond_partition_f_l_1(partition#2(compare_list_l1(x3),x1)
                          ,compare_list_l1(x3)
                          ,x2)
    append#2(Nil(),Cons(x2,x4)) -> Cons(x2,x4)
    append#2(Cons(x8,x6),Cons(x2,x4)) -> Cons(x8,append#2(x6,Cons(x2,x4)))
    ite3_b#2(True(),x20,x24) -> x20
    ite3_b#2(False(),x20,x24) -> x24
    ite_b#2(True(),Pair(x8,Cons(x10,x12)),Pair(Cons(x2,x4),x6)) ->
      Pair(x8,Cons(x10,x12))
    ite_b#2(False(),Pair(x8,Cons(x10,x12)),Pair(Cons(x2,x4),x6)) ->
      Pair(Cons(x2,x4),x6)
    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) -> quicksort#2(x1))