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) |
| choice#(cons(x,xs)) | → | choice#(xs) | (20) |
| verify#(cons(l,ls)) | → | negate#(l) | (21) |
| member#(x,cons(y,ys)) | → | eq#(x,y) | (22) |
| satck#(cnf,assign) | → | verify#(assign) | (23) |
| guess#(cons(clause,cnf)) | → | guess#(cnf) | (24) |
| member#(x,cons(y,ys)) | → | if#(eq(x,y),true,member(x,ys)) | (25) |
| member#(x,cons(y,ys)) | → | member#(x,ys) | (26) |
| verify#(cons(l,ls)) | → | verify#(ls) | (27) |
| guess#(cons(clause,cnf)) | → | choice#(clause) | (28) |
| verify#(cons(l,ls)) | → | member#(negate(l),ls) | (29) |
| sat#(cnf) | → | guess#(cnf) | (30) |
| eq#(1(x),1(y)) | → | eq#(x,y) | (31) |
| eq#(O(x),0(y)) | → | eq#(x,y) | (32) |
| satck#(cnf,assign) | → | if#(verify(assign),assign,unsat) | (33) |
| sat#(cnf) | → | satck#(cnf,guess(cnf)) | (34) |
| verify#(cons(l,ls)) | → | if#(member(negate(l),ls),false,verify(ls)) | (35) |
The dependency pairs are split into 5 components.
| guess#(cons(clause,cnf)) | → | guess#(cnf) | (24) |
| [choice#(x1)] | = | 0 |
| [verify(x1)] | = | 0 |
| [negate#(x1)] | = | 0 |
| [1(x1)] | = | 0 |
| [sat#(x1)] | = | 0 |
| [unsat] | = | 0 |
| [guess#(x1)] | = | x1 + 0 |
| [negate(x1)] | = | 0 |
| [choice(x1)] | = | 0 |
| [member(x1, x2)] | = | 0 |
| [eq(x1, x2)] | = | 0 |
| [false] | = | 0 |
| [satck(x1, x2)] | = | 0 |
| [O(x1)] | = | 0 |
| [true] | = | 0 |
| [sat(x1)] | = | 0 |
| [eq#(x1, x2)] | = | 0 |
| [satck#(x1, x2)] | = | 0 |
| [if(x1, x2, x3)] | = | 0 |
| [0(x1)] | = | 0 |
| [nil] | = | 0 |
| [guess(x1)] | = | 0 |
| [cons(x1, x2)] | = | x2 + 1 |
| [member#(x1, x2)] | = | 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [verify#(x1)] | = | 0 |
| guess#(cons(clause,cnf)) | → | guess#(cnf) | (24) |
The dependency pairs are split into 0 components.
| verify#(cons(l,ls)) | → | verify#(ls) | (27) |
| [choice#(x1)] | = | 0 |
| [verify(x1)] | = | 0 |
| [negate#(x1)] | = | 0 |
| [1(x1)] | = | 0 |
| [sat#(x1)] | = | 0 |
| [unsat] | = | 0 |
| [guess#(x1)] | = | 0 |
| [negate(x1)] | = | 0 |
| [choice(x1)] | = | 0 |
| [member(x1, x2)] | = | 0 |
| [eq(x1, x2)] | = | 0 |
| [false] | = | 0 |
| [satck(x1, x2)] | = | 0 |
| [O(x1)] | = | 0 |
| [true] | = | 0 |
| [sat(x1)] | = | 0 |
| [eq#(x1, x2)] | = | 0 |
| [satck#(x1, x2)] | = | 0 |
| [if(x1, x2, x3)] | = | 0 |
| [0(x1)] | = | 0 |
| [nil] | = | 0 |
| [guess(x1)] | = | 0 |
| [cons(x1, x2)] | = | x2 + 1 |
| [member#(x1, x2)] | = | 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [verify#(x1)] | = | x1 + 0 |
| verify#(cons(l,ls)) | → | verify#(ls) | (27) |
The dependency pairs are split into 0 components.
| member#(x,cons(y,ys)) | → | member#(x,ys) | (26) |
| [choice#(x1)] | = | 0 |
| [verify(x1)] | = | 0 |
| [negate#(x1)] | = | 0 |
| [1(x1)] | = | 0 |
| [sat#(x1)] | = | 0 |
| [unsat] | = | 0 |
| [guess#(x1)] | = | 0 |
| [negate(x1)] | = | 0 |
| [choice(x1)] | = | 0 |
| [member(x1, x2)] | = | 0 |
| [eq(x1, x2)] | = | 0 |
| [false] | = | 0 |
| [satck(x1, x2)] | = | 0 |
| [O(x1)] | = | 0 |
| [true] | = | 0 |
| [sat(x1)] | = | 0 |
| [eq#(x1, x2)] | = | 0 |
| [satck#(x1, x2)] | = | 0 |
| [if(x1, x2, x3)] | = | 0 |
| [0(x1)] | = | 0 |
| [nil] | = | 0 |
| [guess(x1)] | = | 0 |
| [cons(x1, x2)] | = | x2 + 1 |
| [member#(x1, x2)] | = | x2 + 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [verify#(x1)] | = | 0 |
| member#(x,cons(y,ys)) | → | member#(x,ys) | (26) |
The dependency pairs are split into 0 components.
| eq#(O(x),0(y)) | → | eq#(x,y) | (32) |
| eq#(1(x),1(y)) | → | eq#(x,y) | (31) |
| [choice#(x1)] | = | 0 |
| [verify(x1)] | = | 0 |
| [negate#(x1)] | = | 0 |
| [1(x1)] | = | x1 + 1 |
| [sat#(x1)] | = | 0 |
| [unsat] | = | 0 |
| [guess#(x1)] | = | 0 |
| [negate(x1)] | = | 0 |
| [choice(x1)] | = | 0 |
| [member(x1, x2)] | = | 0 |
| [eq(x1, x2)] | = | 0 |
| [false] | = | 0 |
| [satck(x1, x2)] | = | 0 |
| [O(x1)] | = | 1 |
| [true] | = | 0 |
| [sat(x1)] | = | 0 |
| [eq#(x1, x2)] | = | x2 + 0 |
| [satck#(x1, x2)] | = | 0 |
| [if(x1, x2, x3)] | = | 0 |
| [0(x1)] | = | x1 + 1 |
| [nil] | = | 0 |
| [guess(x1)] | = | 0 |
| [cons(x1, x2)] | = | 1 |
| [member#(x1, x2)] | = | 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [verify#(x1)] | = | 0 |
| eq#(O(x),0(y)) | → | eq#(x,y) | (32) |
| eq#(1(x),1(y)) | → | eq#(x,y) | (31) |
The dependency pairs are split into 0 components.
| choice#(cons(x,xs)) | → | choice#(xs) | (20) |
| [choice#(x1)] | = | x1 + 0 |
| [verify(x1)] | = | 0 |
| [negate#(x1)] | = | 0 |
| [1(x1)] | = | 1 |
| [sat#(x1)] | = | 0 |
| [unsat] | = | 0 |
| [guess#(x1)] | = | 0 |
| [negate(x1)] | = | 0 |
| [choice(x1)] | = | 0 |
| [member(x1, x2)] | = | 0 |
| [eq(x1, x2)] | = | 0 |
| [false] | = | 0 |
| [satck(x1, x2)] | = | 0 |
| [O(x1)] | = | 1 |
| [true] | = | 0 |
| [sat(x1)] | = | 0 |
| [eq#(x1, x2)] | = | 0 |
| [satck#(x1, x2)] | = | 0 |
| [if(x1, x2, x3)] | = | 0 |
| [0(x1)] | = | 1 |
| [nil] | = | 0 |
| [guess(x1)] | = | 0 |
| [cons(x1, x2)] | = | x2 + 1 |
| [member#(x1, x2)] | = | 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [verify#(x1)] | = | 0 |
| choice#(cons(x,xs)) | → | choice#(xs) | (20) |
The dependency pairs are split into 0 components.