The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

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

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

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

Removed 4 trailing tuple parts

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

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

(5) CdtKnowledgeProof (EQUIVALENT transformation)

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

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))

(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))
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) → c17(SATCK(z0, guess(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, SAT, MEMBER, VERIFY, SATCK

Compound Symbols:

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

(7) CdtPolyRedPairProof (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))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))

We considered the (Usable) 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)

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))
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))

The order we found is given by the following interpretation:
Polynomial interpretation :

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

(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))
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))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(VERIFY(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))

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

(9) CdtPolyRedPairProof (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:

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)

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))
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))

The order we found is given by the following interpretation:
Polynomial interpretation :

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

(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))
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))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(VERIFY(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))

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

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))

We considered the (Usable) 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)

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))
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))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(1(x₁)) = 0   
POL(CHOICE(x₁)) = 0   
POL(EQ(x₁, x₂)) = 0   
POL(GUESS(x₁)) = 0   
POL(MEMBER(x₁, x₂)) = [3] + x₂   
POL(O(x₁)) = 0   
POL(SAT(x₁)) = x₁ + [2]x₁²   
POL(SATCK(x₁, x₂)) = x₂²   
POL(VERIFY(x₁)) = x₁²   
POL(c12(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(choice(x₁)) = 0   
POL(cons(x₁, x₂)) = [2] + x₂   
POL(guess(x₁)) = x₁   
POL(negate(x₁)) = 0   
POL(nil) = 0   

(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))
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))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(VERIFY(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))

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

(13) CdtPolyRedPairProof (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:

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)

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))
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))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [1] + x₁   
POL(1(x₁)) = [1] + x₁   
POL(CHOICE(x₁)) = 0   
POL(EQ(x₁, x₂)) = [2]x₁·x₂   
POL(GUESS(x₁)) = 0   
POL(MEMBER(x₁, x₂)) = [2]x₁·x₂ + x₁²   
POL(O(x₁)) = x₁   
POL(SAT(x₁)) = [2] + [2]x₁ + [2]x₁²   
POL(SATCK(x₁, x₂)) = [1] + [2]x₁ + x₂² + x₁·x₂   
POL(VERIFY(x₁)) = [1] + x₁²   
POL(c12(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(choice(x₁)) = x₁   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(guess(x₁)) = x₁   
POL(negate(x₁)) = x₁   
POL(nil) = 0   

(14) 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))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(VERIFY(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(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:

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

(15) CdtPolyRedPairProof (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))

We considered the (Usable) 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)

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))
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))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [1] + x₁   
POL(1(x₁)) = x₁   
POL(CHOICE(x₁)) = 0   
POL(EQ(x₁, x₂)) = [2] + [2]x₂   
POL(GUESS(x₁)) = 0   
POL(MEMBER(x₁, x₂)) = [2]x₂   
POL(O(x₁)) = 0   
POL(SAT(x₁)) = [2] + [3]x₁ + [2]x₁²   
POL(SATCK(x₁, x₂)) = [2] + [2]x₂ + x₂²   
POL(VERIFY(x₁)) = [1] + [2]x₁ + x₁²   
POL(c12(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(choice(x₁)) = x₁   
POL(cons(x₁, x₂)) = [1] + x₁ + x₂   
POL(guess(x₁)) = x₁   
POL(negate(x₁)) = 0   
POL(nil) = 0   

(16) 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:none
K tuples:

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

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

(17) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(18) BOUNDS(O(1), O(1))