Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/TCT_12/sat)

The rewrite relation of the following TRS is considered.

if(true,t,e) → t (1)
if(false,t,e) → e (2)
member(x,nil) → false (3)
member(x,cons(y,ys)) → if(eq(x,y),true,member(x,ys)) (4)
eq(nil,nil) → true (5)
eq(O(x),0(y)) → eq(x,y) (6)
eq(0(x),1(y)) → false (7)
eq(1(x),0(y)) → false (8)
eq(1(x),1(y)) → eq(x,y) (9)
negate(0(x)) → 1(x) (10)
negate(1(x)) → 0(x) (11)
choice(cons(x,xs)) → x (12)
choice(cons(x,xs)) → choice(xs) (13)
guess(nil) → nil (14)
guess(cons(clause,cnf)) → cons(choice(clause),guess(cnf)) (15)
verify(nil) → true (16)
verify(cons(l,ls)) → if(member(negate(l),ls),false,verify(ls)) (17)
sat(cnf) → satck(cnf,guess(cnf)) (18)
satck(cnf,assign) → if(verify(assign),assign,unsat) (19)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n2).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
if#(true,z0,z1) → c (21)
originates from
if(true,z0,z1) → z0 (20)
if#(false,z0,z1) → c1 (23)
originates from
if(false,z0,z1) → z1 (22)
member#(z0,nil) → c2 (25)
originates from
member(z0,nil) → false (24)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
originates from
member(z0,cons(z1,z2)) → if(eq(z0,z1),true,member(z0,z2)) (26)
eq#(nil,nil) → c4 (28)
originates from
eq(nil,nil) → true (5)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
originates from
eq(O(z0),0(z1)) → eq(z0,z1) (29)
eq#(0(z0),1(z1)) → c6 (32)
originates from
eq(0(z0),1(z1)) → false (31)
eq#(1(z0),0(z1)) → c7 (34)
originates from
eq(1(z0),0(z1)) → false (33)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
originates from
eq(1(z0),1(z1)) → eq(z0,z1) (35)
negate#(0(z0)) → c9 (38)
originates from
negate(0(z0)) → 1(z0) (37)
negate#(1(z0)) → c10 (40)
originates from
negate(1(z0)) → 0(z0) (39)
choice#(cons(z0,z1)) → c11 (42)
originates from
choice(cons(z0,z1)) → z0 (41)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
originates from
choice(cons(z0,z1)) → choice(z1) (43)
guess#(nil) → c13 (45)
originates from
guess(nil) → nil (14)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
originates from
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
verify#(nil) → c15 (48)
originates from
verify(nil) → true (16)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
originates from
verify(cons(z0,z1)) → if(member(negate(z0),z1),false,verify(z1)) (49)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
originates from
sat(z0) → satck(z0,guess(z0)) (51)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
originates from
satck(z0,z1) → if(verify(z1),z1,unsat) (53)
Moreover, we add the following terms to the innermost strategy.
if#(true,z0,z1)
if#(false,z0,z1)
member#(z0,nil)
member#(z0,cons(z1,z2))
eq#(nil,nil)
eq#(O(z0),0(z1))
eq#(0(z0),1(z1))
eq#(1(z0),0(z1))
eq#(1(z0),1(z1))
negate#(0(z0))
negate#(1(z0))
choice#(cons(z0,z1))
choice#(cons(z0,z1))
guess#(nil)
guess#(cons(z0,z1))
verify#(nil)
verify#(cons(z0,z1))
sat#(z0)
satck#(z0,z1)

1.1 Usable Rules

We remove the following rules since they are not usable.
sat(z0) → satck(z0,guess(z0)) (51)
satck(z0,z1) → if(verify(z1),z1,unsat) (53)

1.1.1 Rule Shifting

The rules
guess#(nil) → c13 (45)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[negate(x1)] = 0
[verify(x1)] = 1 · x1 + 0
[guess(x1)] = 1 · x1 + 0
[choice(x1)] = 1 + 1 · x1
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 0
[choice#(x1)] = 0
[guess#(x1)] = 1
[verify#(x1)] = 0
[sat#(x1)] = 1 + 1 · x1
[satck#(x1, x2)] = 1 · x1 + 0
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 · x2 + 0
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 1 · x1 + 0
[unsat] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)

1.1.1.1 Rule Shifting

The rules
verify#(nil) → c15 (48)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[negate(x1)] = 0
[verify(x1)] = 0
[guess(x1)] = 0
[choice(x1)] = 1 + 1 · x1
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 0
[choice#(x1)] = 0
[guess#(x1)] = 1 · x1 + 0
[verify#(x1)] = 1
[sat#(x1)] = 1 + 1 · x1
[satck#(x1, x2)] = 1 + 1 · x2
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 · x2 + 0
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 1 · x1 + 0
[unsat] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)

1.1.1.1.1 Rule Shifting

The rules
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[negate(x1)] = 0
[verify(x1)] = 1 · x1 + 0
[guess(x1)] = 0
[choice(x1)] = 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 0
[choice#(x1)] = 1 · x1 + 0
[guess#(x1)] = 1 · x1 + 0
[verify#(x1)] = 0
[sat#(x1)] = 1 + 1 · x1
[satck#(x1, x2)] = 0
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 · x1 + 0 + 1 · x2
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 1 · x1 + 0
[unsat] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)

1.1.1.1.1.1 Rule Shifting

The rules
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[negate(x1)] = 0
[verify(x1)] = 0
[guess(x1)] = 0
[choice(x1)] = 1 + 1 · x1
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 0
[choice#(x1)] = 0
[guess#(x1)] = 1 · x1 + 0
[verify#(x1)] = 0
[sat#(x1)] = 1 + 1 · x1
[satck#(x1, x2)] = 1 + 1 · x2
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 · x2 + 0
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 1 · x1 + 0
[unsat] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)

1.1.1.1.1.1.1 Rule Shifting

The rules
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[negate(x1)] = 0
[verify(x1)] = 1 · x1 + 0
[guess(x1)] = 1 + 1 · x1
[choice(x1)] = 1 + 1 · x1
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 0
[choice#(x1)] = 1 · x1 + 0
[guess#(x1)] = 1 · x1 + 0
[verify#(x1)] = 1
[sat#(x1)] = 1 + 1 · x1
[satck#(x1, x2)] = 1
[nil] = 1
[true] = 0
[cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 1 · x1 + 0
[unsat] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
negate#(0(z0)) → c9 (38)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 3 · x1 + 0
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 3 + 3 · x3
[negate(x1)] = 0
[verify(x1)] = 0
[guess(x1)] = 1 · x1 + 0
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 1 · x1 + 0
[choice#(x1)] = 1 · x1 + 0
[guess#(x1)] = 1 · x1 + 0
[verify#(x1)] = 1 · x1 + 0
[sat#(x1)] = 1 + 3 · x1
[satck#(x1, x2)] = 1 + 2 · x2
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 · x1 + 0 + 1 · x2
[false] = 0
[0(x1)] = 2
[1(x1)] = 0
[O(x1)] = 1 · x1 + 0
[unsat] = 3
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
negate#(1(z0)) → c10 (40)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[negate(x1)] = 0
[verify(x1)] = 1 · x1 + 0
[guess(x1)] = 1 + 1 · x1
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 1 · x1 + 0
[choice#(x1)] = 0
[guess#(x1)] = 0
[verify#(x1)] = 1 · x1 + 0
[sat#(x1)] = 1 + 1 · x1
[satck#(x1, x2)] = 1 · x2 + 0
[nil] = 1
[true] = 0
[cons(x1, x2)] = 1 · x1 + 0 + 1 · x2
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 + 1 · x1
[O(x1)] = 1 · x1 + 0
[unsat] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
member#(z0,nil) → c2 (25)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[negate(x1)] = 0
[verify(x1)] = 1 · x1 + 0
[guess(x1)] = 1 + 1 · x1
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 1
[eq#(x1, x2)] = 0
[negate#(x1)] = 1 · x1 + 0
[choice#(x1)] = 0
[guess#(x1)] = 0
[verify#(x1)] = 1 · x1 + 0
[sat#(x1)] = 1 + 1 · x1
[satck#(x1, x2)] = 1 · x2 + 0
[nil] = 1
[true] = 0
[cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 1 · x1 + 0
[unsat] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[negate(x1)] = 0
[verify(x1)] = 1 · x1 + 0
[guess(x1)] = 1 + 1 · x1
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 1 · x1 + 0
[choice#(x1)] = 0
[guess#(x1)] = 0
[verify#(x1)] = 1 · x1 + 0
[sat#(x1)] = 1 + 1 · x1
[satck#(x1, x2)] = 1 · x2 + 0
[nil] = 1
[true] = 0
[cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 1 · x1 + 0
[unsat] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
eq#(nil,nil) → c4 (28)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 2 + 2 · x2 · x2
[negate(x1)] = 1 · x1 + 0
[verify(x1)] = 0
[guess(x1)] = 1 · x1 + 0
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 2 · x1 · x2 + 0
[eq#(x1, x2)] = 2 · x1 · x2 + 0
[negate#(x1)] = 0
[choice#(x1)] = 0
[guess#(x1)] = 1
[verify#(x1)] = 1 · x1 · x1 + 0
[sat#(x1)] = 2 + 1 · x1 + 2 · x1 · x1
[satck#(x1, x2)] = 2 · x2 · x2 + 0
[nil] = 2
[true] = 0
[cons(x1, x2)] = 1 · x1 + 0 + 1 · x2
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 1 · x1 + 0
[unsat] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
negate(1(z0)) → 0(z0) (39)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)
negate(0(z0)) → 1(z0) (37)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 2 + 2 · x2 · x2
[negate(x1)] = 2 + 1 · x1
[verify(x1)] = 0
[guess(x1)] = 1 · x1 + 0
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 1 · x1 · x2 + 0
[eq#(x1, x2)] = 1 · x1 + 0
[negate#(x1)] = 0
[choice#(x1)] = 1 + 2 · x1 + 1 · x1 · x1
[guess#(x1)] = 1 · x1 · x1 + 0
[verify#(x1)] = 1 · x1 · x1 + 0
[sat#(x1)] = 1 · x1 + 0 + 2 · x1 · x1
[satck#(x1, x2)] = 1 · x2 · x2 + 0
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 2 + 1 · x1
[O(x1)] = 1 · x1 + 0
[unsat] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
negate(1(z0)) → 0(z0) (39)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)
negate(0(z0)) → 1(z0) (37)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 2 + 2 · x2 · x2
[negate(x1)] = 0
[verify(x1)] = 0
[guess(x1)] = 1 · x1 + 0
[choice(x1)] = 2 + 1 · x1 + 2 · x1 · x1
[if#(x1, x2, x3)] = 1
[member#(x1, x2)] = 1 · x2 + 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 0
[choice#(x1)] = 0
[guess#(x1)] = 1 · x1 · x1 + 0
[verify#(x1)] = 1 · x1 · x1 + 0
[sat#(x1)] = 2 + 2 · x1 · x1
[satck#(x1, x2)] = 1 + 1 · x2 · x2
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 + 1 · x2
[false] = 0
[0(x1)] = 0
[1(x1)] = 0
[O(x1)] = 0
[unsat] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
eq#(0(z0),1(z1)) → c6 (32)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 2 + 1 · x2 · x2
[negate(x1)] = 2 · x1 + 0
[verify(x1)] = 0
[guess(x1)] = 1 · x1 + 0
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 2 · x1 · x2 + 0
[eq#(x1, x2)] = 2 · x1 · x2 + 0
[negate#(x1)] = 0
[choice#(x1)] = 0
[guess#(x1)] = 1
[verify#(x1)] = 2 · x1 · x1 + 0
[sat#(x1)] = 1 + 2 · x1 + 2 · x1 · x1
[satck#(x1, x2)] = 2 · x2 · x2 + 0
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 · x1 + 0 + 1 · x2
[false] = 0
[0(x1)] = 2 + 1 · x1
[1(x1)] = 1 + 1 · x1
[O(x1)] = 1 · x1 + 0
[unsat] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
negate(1(z0)) → 0(z0) (39)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)
negate(0(z0)) → 1(z0) (37)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 1 + 2 · x2 · x2
[negate(x1)] = 0
[verify(x1)] = 0
[guess(x1)] = 1 · x1 + 0
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 1 · x2 + 0
[eq#(x1, x2)] = 0
[negate#(x1)] = 0
[choice#(x1)] = 2 · x1 + 0 + 1 · x1 · x1
[guess#(x1)] = 1 + 1 · x1 · x1
[verify#(x1)] = 1 · x1 · x1 + 0
[sat#(x1)] = 1 + 2 · x1 + 2 · x1 · x1
[satck#(x1, x2)] = 1 · x2 · x2 + 0
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[false] = 0
[0(x1)] = 0
[1(x1)] = 0
[O(x1)] = 0
[unsat] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12(x1)] = 1 · x1 + 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1,...,x4)] = 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4
[c17(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c18(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[member(x1, x2)] = 0
[if(x1, x2, x3)] = 2 + 2 · x2 · x2
[negate(x1)] = 1 · x1 + 0
[verify(x1)] = 0
[guess(x1)] = 1 · x1 + 0
[choice(x1)] = 1 · x1 + 0
[if#(x1, x2, x3)] = 0
[member#(x1, x2)] = 1 · x1 · x2 + 0
[eq#(x1, x2)] = 1 · x1 + 0
[negate#(x1)] = 0
[choice#(x1)] = 0
[guess#(x1)] = 0
[verify#(x1)] = 2 · x1 · x1 + 0
[sat#(x1)] = 2 + 2 · x1 · x1
[satck#(x1, x2)] = 2 · x2 · x2 + 0
[nil] = 0
[true] = 0
[cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[false] = 0
[0(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[O(x1)] = 2 + 1 · x1
[unsat] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
if#(true,z0,z1) → c (21)
if#(false,z0,z1) → c1 (23)
member#(z0,nil) → c2 (25)
member#(z0,cons(z1,z2)) → c3(if#(eq(z0,z1),true,member(z0,z2)),eq#(z0,z1),member#(z0,z2)) (27)
eq#(nil,nil) → c4 (28)
eq#(O(z0),0(z1)) → c5(eq#(z0,z1)) (30)
eq#(0(z0),1(z1)) → c6 (32)
eq#(1(z0),0(z1)) → c7 (34)
eq#(1(z0),1(z1)) → c8(eq#(z0,z1)) (36)
negate#(0(z0)) → c9 (38)
negate#(1(z0)) → c10 (40)
choice#(cons(z0,z1)) → c11 (42)
choice#(cons(z0,z1)) → c12(choice#(z1)) (44)
guess#(nil) → c13 (45)
guess#(cons(z0,z1)) → c14(choice#(z0),guess#(z1)) (47)
verify#(nil) → c15 (48)
verify#(cons(z0,z1)) → c16(if#(member(negate(z0),z1),false,verify(z1)),member#(negate(z0),z1),negate#(z0),verify#(z1)) (50)
sat#(z0) → c17(satck#(z0,guess(z0)),guess#(z0)) (52)
satck#(z0,z1) → c18(if#(verify(z1),z1,unsat),verify#(z1)) (54)
negate(1(z0)) → 0(z0) (39)
guess(nil) → nil (14)
guess(cons(z0,z1)) → cons(choice(z0),guess(z1)) (46)
choice(cons(z0,z1)) → choice(z1) (43)
choice(cons(z0,z1)) → z0 (41)
negate(0(z0)) → 1(z0) (37)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).