(STRATEGY
    INNERMOST)

(VAR
    x2 x1 x3 x0 x5 x6 x4 x8 x12)
(RULES
    fold#3(Nil()) -> Nil()
    fold#3(Cons(x2,x1)) -> insert_ord#2(x2,fold#3(x1))
    cond_insert_ord_x_ys_1(True(),x3,x2,x1) -> Cons(x3,Cons(x2,x1))
    cond_insert_ord_x_ys_1(False(),x0,x5,x2) -> Cons(x5,insert_ord#2(x0,x2))
    insert_ord#2(x2,Nil()) -> Cons(x2,Nil())
    insert_ord#2(x6,Cons(x4,x2)) -> cond_insert_ord_x_ys_1(leq#2(x6,x4)
                                                          ,x6
                                                          ,x4
                                                          ,x2)
    leq#2(0(),x8) -> True()
    leq#2(S(x12),0()) -> False()
    leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
    main(x3) -> fold#3(x3))