The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
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(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, 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(insert_ord(leq), x3)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
fold#3(insert_ord(x6), Cons(x4, x2)) →⁺ insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [x2 / Cons(x4, x2)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)