### (0) Obligation:

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: FULL

### (1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
member(x, cons(y, ys)) →+ if(eq(x, y), true, member(x, ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [ys / cons(y, ys)].
The result substitution is [ ].

### (3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

### (4) Obligation:

Runtime Complexity Relative 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)

S is empty.
Rewrite Strategy: FULL

### (5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
satck/0

### (6) Obligation:

Runtime Complexity Relative 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)

S is empty.
Rewrite Strategy: FULL

Infered types.

### (8) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

### (9) OrderProof (LOWER BOUND(ID) transformation)

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

### (10) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_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

### (11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

### (12) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

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

### (13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)

Induction Base:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n127_2, 1)))) →RΩ(1)
if(eq(gen_true:false:nil:cons:O:0:1:unsat2_2(a), true), true, member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2)))) →IH
if(eq(gen_true:false:nil:cons:O:0:1:unsat2_2(a), true), true, *3_2)

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

### (15) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

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

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

### (16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) → *3_2, rt ∈ Ω(n1316882)

Induction Base:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n131688_2, 1)))) →RΩ(1)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) →IH
*3_2

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

### (18) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) → *3_2, rt ∈ Ω(n1316882)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

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

### (19) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132159_2))) → *3_2, rt ∈ Ω(n1321592)

Induction Base:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n132159_2, 1)))) →RΩ(1)
cons(choice(true), guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132159_2)))) →IH
cons(choice(true), *3_2)

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

### (21) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) → *3_2, rt ∈ Ω(n1316882)
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132159_2))) → *3_2, rt ∈ Ω(n1321592)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
verify

### (22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

### (23) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) → *3_2, rt ∈ Ω(n1316882)
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132159_2))) → *3_2, rt ∈ Ω(n1321592)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

### (24) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)

### (26) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) → *3_2, rt ∈ Ω(n1316882)
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132159_2))) → *3_2, rt ∈ Ω(n1321592)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

### (27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)

### (29) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) → *3_2, rt ∈ Ω(n1316882)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

### (30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)

### (32) Obligation:

TRS:
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:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

### (33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n1272)