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

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

if'(true', t, e) → t
if'(false', t, e) → e
member'(x, nil') → false'
member'(x, cons'(y, ys)) → if'(eq'(x, y), true', member'(x, ys))
eq'(nil', nil') → true'
eq'(O'(x), 0'(y)) → eq'(x, y)
eq'(0'(x), 1'(y)) → false'
eq'(1'(x), 0'(y)) → false'
eq'(1'(x), 1'(y)) → eq'(x, y)
negate'(0'(x)) → 1'(x)
negate'(1'(x)) → 0'(x)
choice'(cons'(x, xs)) → x
choice'(cons'(x, xs)) → choice'(xs)
guess'(nil') → nil'
guess'(cons'(clause, cnf)) → cons'(choice'(clause), guess'(cnf))
verify'(nil') → true'
verify'(cons'(l, ls)) → if'(member'(negate'(l), ls), false', verify'(ls))
sat'(cnf) → satck'(cnf, guess'(cnf))
satck'(cnf, assign) → if'(verify'(assign), assign, unsat')

Rewrite Strategy: INNERMOST

Sliced the following arguments:
satck'/0

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

if'(true', t, e) → t
if'(false', t, e) → e
member'(x, nil') → false'
member'(x, cons'(y, ys)) → if'(eq'(x, y), true', member'(x, ys))
eq'(nil', nil') → true'
eq'(O'(x), 0'(y)) → eq'(x, y)
eq'(0'(x), 1'(y)) → false'
eq'(1'(x), 0'(y)) → false'
eq'(1'(x), 1'(y)) → eq'(x, y)
negate'(0'(x)) → 1'(x)
negate'(1'(x)) → 0'(x)
choice'(cons'(x, xs)) → x
choice'(cons'(x, xs)) → choice'(xs)
guess'(nil') → nil'
guess'(cons'(clause, cnf)) → cons'(choice'(clause), guess'(cnf))
verify'(nil') → true'
verify'(cons'(l, ls)) → if'(member'(negate'(l), ls), false', verify'(ls))
sat'(cnf) → satck'(guess'(cnf))
satck'(assign) → if'(verify'(assign), assign, unsat')

Rewrite Strategy: INNERMOST

Infered types.

Rules:
if'(true', t, e) → t
if'(false', t, e) → e
member'(x, nil') → false'
member'(x, cons'(y, ys)) → if'(eq'(x, y), true', member'(x, ys))
eq'(nil', nil') → true'
eq'(O'(x), 0'(y)) → eq'(x, y)
eq'(0'(x), 1'(y)) → false'
eq'(1'(x), 0'(y)) → false'
eq'(1'(x), 1'(y)) → eq'(x, y)
negate'(0'(x)) → 1'(x)
negate'(1'(x)) → 0'(x)
choice'(cons'(x, xs)) → x
choice'(cons'(x, xs)) → choice'(xs)
guess'(nil') → nil'
guess'(cons'(clause, cnf)) → cons'(choice'(clause), guess'(cnf))
verify'(nil') → true'
verify'(cons'(l, ls)) → if'(member'(negate'(l), ls), false', verify'(ls))
sat'(cnf) → satck'(guess'(cnf))
satck'(assign) → if'(verify'(assign), assign, unsat')

Types:
if' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
true' :: true':false':nil':cons':O':0':1':unsat'
false' :: true':false':nil':cons':O':0':1':unsat'
member' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
nil' :: true':false':nil':cons':O':0':1':unsat'
cons' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
eq' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
O' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
0' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
1' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
negate' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
choice' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
guess' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
verify' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
sat' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
satck' :: true':false':nil':cons':O':0':1':unsat' → true':false':nil':cons':O':0':1':unsat'
unsat' :: true':false':nil':cons':O':0':1':unsat'
_hole_true':false':nil':cons':O':0':1':unsat'1 :: true':false':nil':cons':O':0':1':unsat'
_gen_true':false':nil':cons':O':0':1':unsat'2 :: Nat → true':false':nil':cons':O':0':1':unsat'

Heuristically decided to analyse the following defined symbols:
member', eq', choice', guess', verify'

They will be analysed ascendingly in the following order:
eq' < member'
member' < verify'
choice' < guess'

Generator Equations:
_gen_true':false':nil':cons':O':0':1':unsat'2(0) ⇔ true'
_gen_true':false':nil':cons':O':0':1':unsat'2(+(x, 1)) ⇔ cons'(true', _gen_true':false':nil':cons':O':0':1':unsat'2(x))

The following defined symbols remain to be analysed:
eq', member', choice', guess', verify'

They will be analysed ascendingly in the following order:
eq' < member'
member' < verify'
choice' < guess'

Could not prove a rewrite lemma for the defined symbol eq'.

The following defined symbols remain to be analysed:
member', choice', guess', verify'

They will be analysed ascendingly in the following order:
member' < verify'
choice' < guess'

Proved the following rewrite lemma:
member'(_gen_true':false':nil':cons':O':0':1':unsat'2(a), _gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _n248))) → _*3, rt ∈ Ω(_n248)

Induction Base:
member'(_gen_true':false':nil':cons':O':0':1':unsat'2(a), _gen_true':false':nil':cons':O':0':1':unsat'2(+(1, 0)))

Induction Step:
member'(_gen_true':false':nil':cons':O':0':1':unsat'2(_a137611), _gen_true':false':nil':cons':O':0':1':unsat'2(+(1, +(_$n249, 1)))) →_R^Ω(1)
if'(eq'(_gen_true':false':nil':cons':O':0':1':unsat'2(_a137611), true'), true', member'(_gen_true':false':nil':cons':O':0':1':unsat'2(_a137611), _gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _$n249)))) →_IH
if'(eq'(_gen_true':false':nil':cons':O':0':1':unsat'2(_a137611), true'), true', _*3)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
member'(_gen_true':false':nil':cons':O':0':1':unsat'2(a), _gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _n248))) → _*3, rt ∈ Ω(_n248)

The following defined symbols remain to be analysed:
choice', guess', verify'

They will be analysed ascendingly in the following order:
choice' < guess'

Proved the following rewrite lemma:
choice'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _n139196))) → _*3, rt ∈ Ω(_n139196)

Induction Base:
choice'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, 0)))

Induction Step:
choice'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, +(_$n139197, 1)))) →_R^Ω(1)
choice'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _$n139197))) →_IH
_*3

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
member'(_gen_true':false':nil':cons':O':0':1':unsat'2(a), _gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _n248))) → _*3, rt ∈ Ω(_n248)
choice'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _n139196))) → _*3, rt ∈ Ω(_n139196)

The following defined symbols remain to be analysed:
guess', verify'

Proved the following rewrite lemma:
guess'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _n140286))) → _*3, rt ∈ Ω(_n140286)

Induction Base:
guess'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, 0)))

Induction Step:
guess'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, +(_$n140287, 1)))) →_R^Ω(1)
cons'(choice'(true'), guess'(_gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _$n140287)))) →_IH
cons'(choice'(true'), _*3)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
verify'

Could not prove a rewrite lemma for the defined symbol verify'.

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
member'(_gen_true':false':nil':cons':O':0':1':unsat'2(a), _gen_true':false':nil':cons':O':0':1':unsat'2(+(1, _n248))) → _*3, rt ∈ Ω(_n248)