(VAR x1 x12 x2 x3 x4 x6 x8 )
(STRATEGY INNERMOST)
(RULES 
        sort#2(Nil) -> Nil
        sort#2(Cons(x4,x2)) -> insert#3(x4,sort#2(x2))
        cond_insert_ord_x_ys_1(True,x3,x2,x1) -> Cons(x3,Cons(x2,x1))
        cond_insert_ord_x_ys_1(False,x3,x2,x1) -> Cons(x2,insert#3(x3,x1))
        insert#3(x2,Nil) -> Cons(x2,Nil)
        insert#3(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(x1) -> sort#2(x1)
        
)