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

(0) Obligation:

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

overlap(Cons(x, xs), ys) → overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys)
overlap(Nil, ys) → False
member(x', Cons(x, xs)) → member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
member(x, Nil) → False
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
goal(xs, ys) → overlap(xs, ys)

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
overlap[Ite][True][Ite](False, Cons(x, xs), ys) → overlap(xs, ys)
member[Ite][True][Ite](False, x', Cons(x, xs)) → member(x', xs)
overlap[Ite][True][Ite](True, xs, ys) → True
member[Ite][True][Ite](True, x, xs) → True

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
overlap(Cons(x, xs), Nil) →⁺ overlap(xs, Nil)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(x, xs)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)