(STRATEGY
    INNERMOST)

(VAR
    x4 x2 x14 x10 x6 x8 x40 x48 x16 x12 x1)
(RULES
    isort#2(Nil()) -> Nil()
    isort#2(Cons(x4,x2)) -> insert#3(x4,isort#2(x2))
    insert#3(x2,Nil()) -> Cons(x2,Nil())
    insert#3(x14,Cons(x10,x6)) -> ite_cond#2(compare_list#2(x10,x14)
                                            ,Cons(x10,insert#3(x14,x6))
                                            ,Cons(x14,Cons(x10,x6)))
    compare_list#2(Nil(),x2) -> True()
    compare_list#2(Cons(x4,x2),Nil()) -> False()
    compare_list#2(Cons(x8,x6),Cons(x4,x2)) -> ite2#3(eqNat#2(x8,x4)
                                                     ,compare_list#2(x6,x2)
                                                     ,ltNat#2(x8,x4))
    ite2#3(True(),x40,x48) -> x40
    ite2#3(False(),x40,x48) -> x48
    ite_cond#2(True(),Cons(x8,x10),Cons(x2,Cons(x4,x6))) -> Cons(x8,x10)
    ite_cond#2(False(),Cons(x8,x10),Cons(x2,Cons(x4,x6))) -> Cons(x2
                                                                 ,Cons(x4,x6))
    ltNat#2(x8,0()) -> False()
    ltNat#2(0(),S(x16)) -> True()
    ltNat#2(S(x4),S(x2)) -> ltNat#2(x4,x2)
    eqNat#2(0(),0()) -> True()
    eqNat#2(S(x12),0()) -> False()
    eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2)
    eqNat#2(0(),S(x12)) -> False()
    main(x1) -> isort#2(x1))