*** 1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
Weak DP Rules:
Weak TRS Rules:
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [0]
p(choice) = [2] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [0]
p(eq) = [3]
p(false) = [1]
p(guess) = [3] x1 + [5]
p(if) = [1] x1 + [1] x2 + [1] x3 + [6]
p(member) = [1] x1 + [2]
p(negate) = [4]
p(nil) = [1]
p(sat) = [7] x1 + [0]
p(satck) = [4] x1 + [1] x2 + [0]
p(true) = [0]
p(unsat) = [0]
p(verify) = [0]
Following rules are strictly oriented:
eq(0(x),1(y)) = [3]
> [1]
= false()
eq(1(x),0(y)) = [3]
> [1]
= false()
eq(nil(),nil()) = [3]
> [0]
= true()
guess(nil()) = [8]
> [1]
= nil()
if(false(),t,e) = [1] e + [1] t + [7]
> [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [6]
> [1] t + [0]
= t
member(x,nil()) = [1] x + [2]
> [1]
= false()
negate(0(x)) = [4]
> [0]
= 1(x)
negate(1(x)) = [4]
> [0]
= 0(x)
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [2] x + [2] xs + [0]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [2] x + [2] xs + [0]
>= [2] xs + [0]
= choice(xs)
eq(1(x),1(y)) = [3]
>= [3]
= eq(x,y)
eq(O(x),0(y)) = [3]
>= [3]
= eq(x,y)
guess(cons(clause,cnf)) = [3] clause + [3] cnf + [5]
>= [2] clause + [3] cnf + [5]
= cons(choice(clause),guess(cnf))
member(x,cons(y,ys)) = [1] x + [2]
>= [1] x + [11]
= if(eq(x,y),true(),member(x,ys))
sat(cnf) = [7] cnf + [0]
>= [7] cnf + [5]
= satck(cnf,guess(cnf))
satck(cnf,assign) = [1] assign + [4] cnf + [0]
>= [1] assign + [6]
= if(verify(assign)
,assign
,unsat())
verify(cons(l,ls)) = [0]
>= [13]
= if(member(negate(l),ls)
,false()
,verify(ls))
verify(nil()) = [0]
>= [0]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
Weak DP Rules:
Weak TRS Rules:
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [1] x1 + [0]
p(choice) = [4] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [0]
p(eq) = [0]
p(false) = [0]
p(guess) = [4] x1 + [0]
p(if) = [1] x1 + [1] x2 + [1] x3 + [0]
p(member) = [1] x1 + [0]
p(negate) = [0]
p(nil) = [0]
p(sat) = [4] x1 + [0]
p(satck) = [1] x2 + [4]
p(true) = [0]
p(unsat) = [0]
p(verify) = [3]
Following rules are strictly oriented:
satck(cnf,assign) = [1] assign + [4]
> [1] assign + [3]
= if(verify(assign)
,assign
,unsat())
verify(nil()) = [3]
> [0]
= true()
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [4] x + [4] xs + [0]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [4] x + [4] xs + [0]
>= [4] xs + [0]
= choice(xs)
eq(0(x),1(y)) = [0]
>= [0]
= false()
eq(1(x),0(y)) = [0]
>= [0]
= false()
eq(1(x),1(y)) = [0]
>= [0]
= eq(x,y)
eq(O(x),0(y)) = [0]
>= [0]
= eq(x,y)
eq(nil(),nil()) = [0]
>= [0]
= true()
guess(cons(clause,cnf)) = [4] clause + [4] cnf + [0]
>= [4] clause + [4] cnf + [0]
= cons(choice(clause),guess(cnf))
guess(nil()) = [0]
>= [0]
= nil()
if(false(),t,e) = [1] e + [1] t + [0]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [0]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [0]
>= [1] x + [0]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [0]
>= [0]
= false()
negate(0(x)) = [0]
>= [0]
= 1(x)
negate(1(x)) = [0]
>= [0]
= 0(x)
sat(cnf) = [4] cnf + [0]
>= [4] cnf + [4]
= satck(cnf,guess(cnf))
verify(cons(l,ls)) = [3]
>= [3]
= if(member(negate(l),ls)
,false()
,verify(ls))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
sat(cnf) -> satck(cnf,guess(cnf))
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
Weak DP Rules:
Weak TRS Rules:
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(nil()) -> true()
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [0]
p(choice) = [1] x1 + [6]
p(cons) = [1] x1 + [1] x2 + [2]
p(eq) = [5]
p(false) = [0]
p(guess) = [1] x1 + [0]
p(if) = [1] x1 + [1] x2 + [1] x3 + [0]
p(member) = [1] x1 + [3]
p(negate) = [0]
p(nil) = [1]
p(sat) = [2] x1 + [1]
p(satck) = [1] x1 + [1] x2 + [6]
p(true) = [5]
p(unsat) = [1]
p(verify) = [5]
Following rules are strictly oriented:
choice(cons(x,xs)) = [1] x + [1] xs + [8]
> [1] x + [0]
= x
choice(cons(x,xs)) = [1] x + [1] xs + [8]
> [1] xs + [6]
= choice(xs)
Following rules are (at-least) weakly oriented:
eq(0(x),1(y)) = [5]
>= [0]
= false()
eq(1(x),0(y)) = [5]
>= [0]
= false()
eq(1(x),1(y)) = [5]
>= [5]
= eq(x,y)
eq(O(x),0(y)) = [5]
>= [5]
= eq(x,y)
eq(nil(),nil()) = [5]
>= [5]
= true()
guess(cons(clause,cnf)) = [1] clause + [1] cnf + [2]
>= [1] clause + [1] cnf + [8]
= cons(choice(clause),guess(cnf))
guess(nil()) = [1]
>= [1]
= nil()
if(false(),t,e) = [1] e + [1] t + [0]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [5]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [3]
>= [1] x + [13]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [3]
>= [0]
= false()
negate(0(x)) = [0]
>= [0]
= 1(x)
negate(1(x)) = [0]
>= [0]
= 0(x)
sat(cnf) = [2] cnf + [1]
>= [2] cnf + [6]
= satck(cnf,guess(cnf))
satck(cnf,assign) = [1] assign + [1] cnf + [6]
>= [1] assign + [6]
= if(verify(assign)
,assign
,unsat())
verify(cons(l,ls)) = [5]
>= [8]
= if(member(negate(l),ls)
,false()
,verify(ls))
verify(nil()) = [5]
>= [5]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
sat(cnf) -> satck(cnf,guess(cnf))
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
Weak DP Rules:
Weak TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(nil()) -> true()
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [0]
p(choice) = [4] x1 + [1]
p(cons) = [1] x1 + [1] x2 + [2]
p(eq) = [0]
p(false) = [0]
p(guess) = [4] x1 + [3]
p(if) = [1] x1 + [1] x2 + [1] x3 + [1]
p(member) = [1] x1 + [0]
p(negate) = [0]
p(nil) = [2]
p(sat) = [4] x1 + [1]
p(satck) = [1] x2 + [1]
p(true) = [0]
p(unsat) = [0]
p(verify) = [0]
Following rules are strictly oriented:
guess(cons(clause,cnf)) = [4] clause + [4] cnf + [11]
> [4] clause + [4] cnf + [6]
= cons(choice(clause),guess(cnf))
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [4] x + [4] xs + [9]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [4] x + [4] xs + [9]
>= [4] xs + [1]
= choice(xs)
eq(0(x),1(y)) = [0]
>= [0]
= false()
eq(1(x),0(y)) = [0]
>= [0]
= false()
eq(1(x),1(y)) = [0]
>= [0]
= eq(x,y)
eq(O(x),0(y)) = [0]
>= [0]
= eq(x,y)
eq(nil(),nil()) = [0]
>= [0]
= true()
guess(nil()) = [11]
>= [2]
= nil()
if(false(),t,e) = [1] e + [1] t + [1]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [1]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [0]
>= [1] x + [1]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [0]
>= [0]
= false()
negate(0(x)) = [0]
>= [0]
= 1(x)
negate(1(x)) = [0]
>= [0]
= 0(x)
sat(cnf) = [4] cnf + [1]
>= [4] cnf + [4]
= satck(cnf,guess(cnf))
satck(cnf,assign) = [1] assign + [1]
>= [1] assign + [1]
= if(verify(assign)
,assign
,unsat())
verify(cons(l,ls)) = [0]
>= [1]
= if(member(negate(l),ls)
,false()
,verify(ls))
verify(nil()) = [0]
>= [0]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
sat(cnf) -> satck(cnf,guess(cnf))
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
Weak DP Rules:
Weak TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(nil()) -> true()
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [1] x1 + [0]
p(choice) = [1] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [2]
p(eq) = [0]
p(false) = [0]
p(guess) = [1] x1 + [0]
p(if) = [1] x1 + [1] x2 + [1] x3 + [2]
p(member) = [1] x1 + [0]
p(negate) = [7]
p(nil) = [0]
p(sat) = [2] x1 + [5]
p(satck) = [1] x1 + [1] x2 + [4]
p(true) = [0]
p(unsat) = [0]
p(verify) = [0]
Following rules are strictly oriented:
sat(cnf) = [2] cnf + [5]
> [2] cnf + [4]
= satck(cnf,guess(cnf))
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [1] x + [1] xs + [2]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [1] x + [1] xs + [2]
>= [1] xs + [0]
= choice(xs)
eq(0(x),1(y)) = [0]
>= [0]
= false()
eq(1(x),0(y)) = [0]
>= [0]
= false()
eq(1(x),1(y)) = [0]
>= [0]
= eq(x,y)
eq(O(x),0(y)) = [0]
>= [0]
= eq(x,y)
eq(nil(),nil()) = [0]
>= [0]
= true()
guess(cons(clause,cnf)) = [1] clause + [1] cnf + [2]
>= [1] clause + [1] cnf + [2]
= cons(choice(clause),guess(cnf))
guess(nil()) = [0]
>= [0]
= nil()
if(false(),t,e) = [1] e + [1] t + [2]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [2]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [0]
>= [1] x + [2]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [0]
>= [0]
= false()
negate(0(x)) = [7]
>= [0]
= 1(x)
negate(1(x)) = [7]
>= [0]
= 0(x)
satck(cnf,assign) = [1] assign + [1] cnf + [4]
>= [1] assign + [2]
= if(verify(assign)
,assign
,unsat())
verify(cons(l,ls)) = [0]
>= [9]
= if(member(negate(l),ls)
,false()
,verify(ls))
verify(nil()) = [0]
>= [0]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
Weak DP Rules:
Weak TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(nil()) -> true()
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{choice,eq,guess,if,member,negate,sat,satck,verify}
TcT has computed the following interpretation:
p(0) = [1]
p(1) = [0]
p(O) = [0]
p(choice) = [1] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [8]
p(eq) = [0]
p(false) = [0]
p(guess) = [1] x1 + [0]
p(if) = [4] x1 + [1] x2 + [1] x3 + [0]
p(member) = [1] x1 + [0]
p(negate) = [1]
p(nil) = [4]
p(sat) = [8] x1 + [4]
p(satck) = [3] x1 + [5] x2 + [4]
p(true) = [0]
p(unsat) = [4]
p(verify) = [1] x1 + [0]
Following rules are strictly oriented:
verify(cons(l,ls)) = [1] l + [1] ls + [8]
> [1] ls + [4]
= if(member(negate(l),ls)
,false()
,verify(ls))
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [1] x + [1] xs + [8]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [1] x + [1] xs + [8]
>= [1] xs + [0]
= choice(xs)
eq(0(x),1(y)) = [0]
>= [0]
= false()
eq(1(x),0(y)) = [0]
>= [0]
= false()
eq(1(x),1(y)) = [0]
>= [0]
= eq(x,y)
eq(O(x),0(y)) = [0]
>= [0]
= eq(x,y)
eq(nil(),nil()) = [0]
>= [0]
= true()
guess(cons(clause,cnf)) = [1] clause + [1] cnf + [8]
>= [1] clause + [1] cnf + [8]
= cons(choice(clause),guess(cnf))
guess(nil()) = [4]
>= [4]
= nil()
if(false(),t,e) = [1] e + [1] t + [0]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [0]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [0]
>= [1] x + [0]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [0]
>= [0]
= false()
negate(0(x)) = [1]
>= [0]
= 1(x)
negate(1(x)) = [1]
>= [1]
= 0(x)
sat(cnf) = [8] cnf + [4]
>= [8] cnf + [4]
= satck(cnf,guess(cnf))
satck(cnf,assign) = [5] assign + [3] cnf + [4]
>= [5] assign + [4]
= if(verify(assign)
,assign
,unsat())
verify(nil()) = [4]
>= [0]
= true()
*** 1.1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
Weak DP Rules:
Weak TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{choice,eq,guess,if,member,negate,sat,satck,verify}
TcT has computed the following interpretation:
p(0) = x1
p(1) = x1
p(O) = 1 + x1
p(choice) = x1
p(cons) = 1 + x1 + x2
p(eq) = x1
p(false) = 0
p(guess) = x1
p(if) = x1 + x2 + x2*x3 + x3
p(member) = x1 + 2*x1*x2
p(negate) = x1
p(nil) = 1
p(sat) = 3 + 2*x1 + 2*x1^2
p(satck) = 2 + x1^2 + 2*x2 + x2^2
p(true) = 0
p(unsat) = 0
p(verify) = 2 + x1 + x1^2
Following rules are strictly oriented:
eq(O(x),0(y)) = 1 + x
> x
= eq(x,y)
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = 1 + x + xs
>= x
= x
choice(cons(x,xs)) = 1 + x + xs
>= xs
= choice(xs)
eq(0(x),1(y)) = x
>= 0
= false()
eq(1(x),0(y)) = x
>= 0
= false()
eq(1(x),1(y)) = x
>= x
= eq(x,y)
eq(nil(),nil()) = 1
>= 0
= true()
guess(cons(clause,cnf)) = 1 + clause + cnf
>= 1 + clause + cnf
= cons(choice(clause),guess(cnf))
guess(nil()) = 1
>= 1
= nil()
if(false(),t,e) = e + e*t + t
>= e
= e
if(true(),t,e) = e + e*t + t
>= t
= t
member(x,cons(y,ys)) = 3*x + 2*x*y + 2*x*ys
>= 2*x + 2*x*ys
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = 3*x
>= 0
= false()
negate(0(x)) = x
>= x
= 1(x)
negate(1(x)) = x
>= x
= 0(x)
sat(cnf) = 3 + 2*cnf + 2*cnf^2
>= 2 + 2*cnf + 2*cnf^2
= satck(cnf,guess(cnf))
satck(cnf,assign) = 2 + 2*assign + assign^2 + cnf^2
>= 2 + 2*assign + assign^2
= if(verify(assign)
,assign
,unsat())
verify(cons(l,ls)) = 4 + 3*l + 2*l*ls + l^2 + 3*ls + ls^2
>= 2 + l + 2*l*ls + ls + ls^2
= if(member(negate(l),ls)
,false()
,verify(ls))
verify(nil()) = 4
>= 0
= true()
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
eq(1(x),1(y)) -> eq(x,y)
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
Weak DP Rules:
Weak TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(O(x),0(y)) -> eq(x,y)
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{choice,eq,guess,if,member,negate,sat,satck,verify}
TcT has computed the following interpretation:
p(0) = 0
p(1) = 0
p(O) = 1 + x1
p(choice) = x1
p(cons) = 1 + x1 + x2
p(eq) = 0
p(false) = 0
p(guess) = x1
p(if) = 2*x1 + 2*x2 + x3
p(member) = 2*x1 + x2
p(negate) = 0
p(nil) = 0
p(sat) = 2 + 2*x1 + 2*x1^2
p(satck) = 1 + 2*x2 + 2*x2^2
p(true) = 0
p(unsat) = 0
p(verify) = x1^2
Following rules are strictly oriented:
member(x,cons(y,ys)) = 1 + 2*x + y + ys
> 2*x + ys
= if(eq(x,y),true(),member(x,ys))
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = 1 + x + xs
>= x
= x
choice(cons(x,xs)) = 1 + x + xs
>= xs
= choice(xs)
eq(0(x),1(y)) = 0
>= 0
= false()
eq(1(x),0(y)) = 0
>= 0
= false()
eq(1(x),1(y)) = 0
>= 0
= eq(x,y)
eq(O(x),0(y)) = 0
>= 0
= eq(x,y)
eq(nil(),nil()) = 0
>= 0
= true()
guess(cons(clause,cnf)) = 1 + clause + cnf
>= 1 + clause + cnf
= cons(choice(clause),guess(cnf))
guess(nil()) = 0
>= 0
= nil()
if(false(),t,e) = e + 2*t
>= e
= e
if(true(),t,e) = e + 2*t
>= t
= t
member(x,nil()) = 2*x
>= 0
= false()
negate(0(x)) = 0
>= 0
= 1(x)
negate(1(x)) = 0
>= 0
= 0(x)
sat(cnf) = 2 + 2*cnf + 2*cnf^2
>= 1 + 2*cnf + 2*cnf^2
= satck(cnf,guess(cnf))
satck(cnf,assign) = 1 + 2*assign + 2*assign^2
>= 2*assign + 2*assign^2
= if(verify(assign)
,assign
,unsat())
verify(cons(l,ls)) = 1 + 2*l + 2*l*ls + l^2 + 2*ls + ls^2
>= 2*ls + ls^2
= if(member(negate(l),ls)
,false()
,verify(ls))
verify(nil()) = 0
>= 0
= true()
*** 1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
eq(1(x),1(y)) -> eq(x,y)
Weak DP Rules:
Weak TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(O(x),0(y)) -> eq(x,y)
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{choice,eq,guess,if,member,negate,sat,satck,verify}
TcT has computed the following interpretation:
p(0) = x1
p(1) = 1 + x1
p(O) = 0
p(choice) = x1
p(cons) = 1 + x1 + x2
p(eq) = x2
p(false) = 0
p(guess) = x1
p(if) = x1 + x2 + x3
p(member) = x1 + x2
p(negate) = 1 + 2*x1
p(nil) = 0
p(sat) = 1 + 3*x1 + 3*x1^2
p(satck) = 1 + 2*x1*x2 + 3*x2 + x2^2
p(true) = 0
p(unsat) = 0
p(verify) = 2*x1 + x1^2
Following rules are strictly oriented:
eq(1(x),1(y)) = 1 + y
> y
= eq(x,y)
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = 1 + x + xs
>= x
= x
choice(cons(x,xs)) = 1 + x + xs
>= xs
= choice(xs)
eq(0(x),1(y)) = 1 + y
>= 0
= false()
eq(1(x),0(y)) = y
>= 0
= false()
eq(O(x),0(y)) = y
>= y
= eq(x,y)
eq(nil(),nil()) = 0
>= 0
= true()
guess(cons(clause,cnf)) = 1 + clause + cnf
>= 1 + clause + cnf
= cons(choice(clause),guess(cnf))
guess(nil()) = 0
>= 0
= nil()
if(false(),t,e) = e + t
>= e
= e
if(true(),t,e) = e + t
>= t
= t
member(x,cons(y,ys)) = 1 + x + y + ys
>= x + y + ys
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = x
>= 0
= false()
negate(0(x)) = 1 + 2*x
>= 1 + x
= 1(x)
negate(1(x)) = 3 + 2*x
>= x
= 0(x)
sat(cnf) = 1 + 3*cnf + 3*cnf^2
>= 1 + 3*cnf + 3*cnf^2
= satck(cnf,guess(cnf))
satck(cnf,assign) = 1 + 3*assign + 2*assign*cnf + assign^2
>= 3*assign + assign^2
= if(verify(assign)
,assign
,unsat())
verify(cons(l,ls)) = 3 + 4*l + 2*l*ls + l^2 + 4*ls + ls^2
>= 1 + 2*l + 3*ls + ls^2
= if(member(negate(l),ls)
,false()
,verify(ls))
verify(nil()) = 0
>= 0
= true()
*** 1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0,true/0,unsat/0}
Obligation:
Innermost
basic terms: {choice,eq,guess,if,member,negate,sat,satck,verify}/{0,1,O,cons,false,nil,true,unsat}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).