(STRATEGY
    INNERMOST)

(VAR
    x2 x1 x7 x5 x3 x4 x11 x8 x6 x14 x10 x18 x26)
(RULES
    rec[fold_0][3](Nil()) -> Nil()
    rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1))
    insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
    insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8))
    insert_ord[2](x6,Nil()) -> Cons(x6,Nil())
    insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10)
                                                    ,x14
                                                    ,x10
                                                    ,x6)
    rec[leq_0][2](0(),x18) -> True()
    rec[leq_0][2](S(x26),0()) -> False()
    rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
    main(x7) -> rec[fold_0][3](x7))