(STRATEGY
    INNERMOST)

(VAR
    x4 x2 x3 x1 x6 x8 x12)
(RULES
    sort#2(Nil()) -> Nil()
    sort#2(Cons(x4,x2)) -> insert#3(x4,sort#2(x2))
    cond_insert_ord_x_y1_1(True(),x3,x2,x1) -> Cons(x3,Cons(x2,x1))
    cond_insert_ord_x_y1_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_y1_1(gt#2(x6,x4),x6,x4,x2)
    gt#2(0(),x8) -> False()
    gt#2(S(x12),0()) -> True()
    gt#2(S(x4),S(x2)) -> gt#2(x4,x2)
    main(x1) -> sort#2(x1))