(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: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)
Tuples:

IF(true, z0, z1) → c
IF(false, z0, z1) → c1
MEMBER(z0, nil) → c2
MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(nil, nil) → c4
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(0(z0), 1(z1)) → c6
EQ(1(z0), 0(z1)) → c7
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
NEGATE(0(z0)) → c9
NEGATE(1(z0)) → c10
CHOICE(cons(z0, z1)) → c11
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(nil) → c13
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(nil) → c15
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
S tuples:

IF(true, z0, z1) → c
IF(false, z0, z1) → c1
MEMBER(z0, nil) → c2
MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(nil, nil) → c4
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(0(z0), 1(z1)) → c6
EQ(1(z0), 0(z1)) → c7
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
NEGATE(0(z0)) → c9
NEGATE(1(z0)) → c10
CHOICE(cons(z0, z1)) → c11
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(nil) → c13
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(nil) → c15
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

IF, MEMBER, EQ, NEGATE, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 11 trailing nodes:

CHOICE(cons(z0, z1)) → c11
NEGATE(1(z0)) → c10
IF(true, z0, z1) → c
VERIFY(nil) → c15
IF(false, z0, z1) → c1
MEMBER(z0, nil) → c2
EQ(nil, nil) → c4
NEGATE(0(z0)) → c9
EQ(0(z0), 1(z1)) → c6
GUESS(nil) → c13
EQ(1(z0), 0(z1)) → c7

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)
Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
S tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

EQ, CHOICE, GUESS, SAT, MEMBER, VERIFY, SATCK

Compound Symbols:

c5, c8, c12, c14, c17, c3, c16, c18

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
SAT(z0) → c(GUESS(z0))
S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
SAT(z0) → c(GUESS(z0))
K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

SAT(z0) → c(GUESS(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(13) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(15) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
We considered the (Usable) Rules:none
And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x1)) = [2]   
POL(1(x1)) = [4]   
POL(CHOICE(x1)) = [5] + x1   
POL(EQ(x1, x2)) = 0   
POL(GUESS(x1)) = x1   
POL(MEMBER(x1, x2)) = 0   
POL(O(x1)) = 0   
POL(SAT(x1)) = [4] + [4]x1   
POL(SATCK(x1, x2)) = [3] + [3]x1   
POL(VERIFY(x1)) = 0   
POL(c(x1)) = x1   
POL(c12(x1)) = x1   
POL(c14(x1, x2)) = x1 + x2   
POL(c16(x1, x2)) = x1 + x2   
POL(c18(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c8(x1)) = x1   
POL(choice(x1)) = [3] + x1   
POL(cons(x1, x2)) = [5] + x1 + x2   
POL(guess(x1)) = [3] + [3]x1   
POL(negate(x1)) = [4]x1   
POL(nil) = [2]   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(17) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
We considered the (Usable) Rules:none
And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x1)) = [3]   
POL(1(x1)) = [4]   
POL(CHOICE(x1)) = [2] + [3]x1   
POL(EQ(x1, x2)) = 0   
POL(GUESS(x1)) = [4]x1   
POL(MEMBER(x1, x2)) = 0   
POL(O(x1)) = 0   
POL(SAT(x1)) = [4] + [4]x1   
POL(SATCK(x1, x2)) = [3] + [3]x1   
POL(VERIFY(x1)) = 0   
POL(c(x1)) = x1   
POL(c12(x1)) = x1   
POL(c14(x1, x2)) = x1 + x2   
POL(c16(x1, x2)) = x1 + x2   
POL(c18(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c8(x1)) = x1   
POL(choice(x1)) = [5] + [3]x1   
POL(cons(x1, x2)) = [5] + x1 + x2   
POL(guess(x1)) = [1] + [3]x1   
POL(negate(x1)) = [2]x1   
POL(nil) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(19) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
We considered the (Usable) Rules:

negate(1(z0)) → 0(z0)
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
guess(nil) → nil
negate(0(z0)) → 1(z0)
And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x1)) = [1]   
POL(1(x1)) = 0   
POL(CHOICE(x1)) = [2]   
POL(EQ(x1, x2)) = 0   
POL(GUESS(x1)) = [3]x1   
POL(MEMBER(x1, x2)) = x1   
POL(O(x1)) = 0   
POL(SAT(x1)) = [4] + [4]x1   
POL(SATCK(x1, x2)) = [4] + [4]x2   
POL(VERIFY(x1)) = [4] + [4]x1   
POL(c(x1)) = x1   
POL(c12(x1)) = x1   
POL(c14(x1, x2)) = x1 + x2   
POL(c16(x1, x2)) = x1 + x2   
POL(c18(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c8(x1)) = x1   
POL(choice(x1)) = [5]   
POL(cons(x1, x2)) = [1] + x2   
POL(guess(x1)) = x1   
POL(negate(x1)) = [1]   
POL(nil) = [3]   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(21) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
We considered the (Usable) Rules:

guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
guess(nil) → nil
choice(cons(z0, z1)) → choice(z1)
And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x1)) = [1] + x1   
POL(1(x1)) = x1   
POL(CHOICE(x1)) = x1 + x12   
POL(EQ(x1, x2)) = x2   
POL(GUESS(x1)) = x12   
POL(MEMBER(x1, x2)) = [2]x2   
POL(O(x1)) = 0   
POL(SAT(x1)) = [3] + [3]x1 + [2]x12   
POL(SATCK(x1, x2)) = [2]x2 + x22   
POL(VERIFY(x1)) = [2]x1 + x12   
POL(c(x1)) = x1   
POL(c12(x1)) = x1   
POL(c14(x1, x2)) = x1 + x2   
POL(c16(x1, x2)) = x1 + x2   
POL(c18(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c8(x1)) = x1   
POL(choice(x1)) = x1   
POL(cons(x1, x2)) = [1] + x1 + x2   
POL(guess(x1)) = x1   
POL(negate(x1)) = 0   
POL(nil) = 0   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
S tuples:

EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(23) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
We considered the (Usable) Rules:

guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
guess(nil) → nil
choice(cons(z0, z1)) → choice(z1)
And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x1)) = x1   
POL(1(x1)) = [3] + x1   
POL(CHOICE(x1)) = [1] + x1   
POL(EQ(x1, x2)) = [3] + [3]x2   
POL(GUESS(x1)) = x1   
POL(MEMBER(x1, x2)) = [3]x2   
POL(O(x1)) = 0   
POL(SAT(x1)) = [3] + [2]x1 + [2]x12   
POL(SATCK(x1, x2)) = [3] + x1 + x22   
POL(VERIFY(x1)) = [2] + x12   
POL(c(x1)) = x1   
POL(c12(x1)) = x1   
POL(c14(x1, x2)) = x1 + x2   
POL(c16(x1, x2)) = x1 + x2   
POL(c18(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c8(x1)) = x1   
POL(choice(x1)) = x1   
POL(cons(x1, x2)) = [2] + x1 + x2   
POL(guess(x1)) = x1   
POL(negate(x1)) = 0   
POL(nil) = 0   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
S tuples:none
K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(25) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(26) BOUNDS(O(1), O(1))