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:

#equal(@x, @y) → #eq(@x, @y)
and(@x, @y) → #and(@x, @y)
eq(@l1, @l2) → eq#1(@l1, @l2)
eq#1(::(@x, @xs), @l2) → eq#3(@l2, @x, @xs)
eq#1(nil, @l2) → eq#2(@l2)
eq#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
nub(@l) → nub#1(@l)
nub#1(::(@x, @xs)) → ::(@x, nub(remove(@x, @xs)))
nub#1(nil) → nil
remove(@x, @l) → remove#1(@l, @x)
remove#1(::(@y, @ys), @x) → remove#2(eq(@x, @y), @x, @y, @ys)
remove#1(nil, @x) → nil
remove#2(#false, @x, @y, @ys) → ::(@y, remove(@x, @ys))
remove#2(#true, @x, @y, @ys) → remove(@x, @ys)

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

#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
eq(::(@x7987_4, @xs7988_4), ::(@y8050_4, @ys8051_4)) →⁺ and(#equal(@x7987_4, @y8050_4), eq(@xs7988_4, @ys8051_4))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs7988_4 / ::(@x7987_4, @xs7988_4), @ys8051_4 / ::(@y8050_4, @ys8051_4)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)