WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: 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 runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck ,verify} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs choice#(cons(x,xs)) -> c_1() choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(0(x),1(y)) -> c_3() eq#(1(x),0(y)) -> c_4() eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) eq#(nil(),nil()) -> c_7() guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) guess#(nil()) -> c_9() if#(false(),t,e) -> c_10() if#(true(),t,e) -> c_11() member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) member#(x,nil()) -> c_13() negate#(0(x)) -> c_14() negate#(1(x)) -> c_15() sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) verify#(nil()) -> c_19() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_1() choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(0(x),1(y)) -> c_3() eq#(1(x),0(y)) -> c_4() eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) eq#(nil(),nil()) -> c_7() guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) guess#(nil()) -> c_9() if#(false(),t,e) -> c_10() if#(true(),t,e) -> c_11() member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) member#(x,nil()) -> c_13() negate#(0(x)) -> c_14() negate#(1(x)) -> c_15() sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) verify#(nil()) -> c_19() - Weak TRS: 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0,c_14/0,c_15/0,c_16/2,c_17/2 ,c_18/4,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,4,7,9,10,11,13,14,15,19} by application of Pre({1,3,4,7,9,10,11,13,14,15,19}) = {2,5,6,8,12,16,17,18}. Here rules are labelled as follows: 1: choice#(cons(x,xs)) -> c_1() 2: choice#(cons(x,xs)) -> c_2(choice#(xs)) 3: eq#(0(x),1(y)) -> c_3() 4: eq#(1(x),0(y)) -> c_4() 5: eq#(1(x),1(y)) -> c_5(eq#(x,y)) 6: eq#(O(x),0(y)) -> c_6(eq#(x,y)) 7: eq#(nil(),nil()) -> c_7() 8: guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) 9: guess#(nil()) -> c_9() 10: if#(false(),t,e) -> c_10() 11: if#(true(),t,e) -> c_11() 12: member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) 13: member#(x,nil()) -> c_13() 14: negate#(0(x)) -> c_14() 15: negate#(1(x)) -> c_15() 16: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) 17: satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) 18: verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) 19: verify#(nil()) -> c_19() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) - Weak DPs: choice#(cons(x,xs)) -> c_1() eq#(0(x),1(y)) -> c_3() eq#(1(x),0(y)) -> c_4() eq#(nil(),nil()) -> c_7() guess#(nil()) -> c_9() if#(false(),t,e) -> c_10() if#(true(),t,e) -> c_11() member#(x,nil()) -> c_13() negate#(0(x)) -> c_14() negate#(1(x)) -> c_15() verify#(nil()) -> c_19() - Weak TRS: 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0,c_14/0,c_15/0,c_16/2,c_17/2 ,c_18/4,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:choice#(cons(x,xs)) -> c_2(choice#(xs)) -->_1 choice#(cons(x,xs)) -> c_1():9 -->_1 choice#(cons(x,xs)) -> c_2(choice#(xs)):1 2:S:eq#(1(x),1(y)) -> c_5(eq#(x,y)) -->_1 eq#(O(x),0(y)) -> c_6(eq#(x,y)):3 -->_1 eq#(nil(),nil()) -> c_7():12 -->_1 eq#(1(x),0(y)) -> c_4():11 -->_1 eq#(0(x),1(y)) -> c_3():10 -->_1 eq#(1(x),1(y)) -> c_5(eq#(x,y)):2 3:S:eq#(O(x),0(y)) -> c_6(eq#(x,y)) -->_1 eq#(nil(),nil()) -> c_7():12 -->_1 eq#(1(x),0(y)) -> c_4():11 -->_1 eq#(0(x),1(y)) -> c_3():10 -->_1 eq#(O(x),0(y)) -> c_6(eq#(x,y)):3 -->_1 eq#(1(x),1(y)) -> c_5(eq#(x,y)):2 4:S:guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) -->_2 guess#(nil()) -> c_9():13 -->_1 choice#(cons(x,xs)) -> c_1():9 -->_2 guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4 -->_1 choice#(cons(x,xs)) -> c_2(choice#(xs)):1 5:S:member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) -->_3 member#(x,nil()) -> c_13():16 -->_1 if#(true(),t,e) -> c_11():15 -->_1 if#(false(),t,e) -> c_10():14 -->_2 eq#(nil(),nil()) -> c_7():12 -->_2 eq#(1(x),0(y)) -> c_4():11 -->_2 eq#(0(x),1(y)) -> c_3():10 -->_3 member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5 -->_2 eq#(O(x),0(y)) -> c_6(eq#(x,y)):3 -->_2 eq#(1(x),1(y)) -> c_5(eq#(x,y)):2 6:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) -->_1 satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)):7 -->_2 guess#(nil()) -> c_9():13 -->_2 guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4 7:S:satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) -->_2 verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)):8 -->_2 verify#(nil()) -> c_19():19 -->_1 if#(true(),t,e) -> c_11():15 -->_1 if#(false(),t,e) -> c_10():14 8:S:verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) -->_4 verify#(nil()) -> c_19():19 -->_3 negate#(1(x)) -> c_15():18 -->_3 negate#(0(x)) -> c_14():17 -->_2 member#(x,nil()) -> c_13():16 -->_1 if#(true(),t,e) -> c_11():15 -->_1 if#(false(),t,e) -> c_10():14 -->_4 verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)):8 -->_2 member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5 9:W:choice#(cons(x,xs)) -> c_1() 10:W:eq#(0(x),1(y)) -> c_3() 11:W:eq#(1(x),0(y)) -> c_4() 12:W:eq#(nil(),nil()) -> c_7() 13:W:guess#(nil()) -> c_9() 14:W:if#(false(),t,e) -> c_10() 15:W:if#(true(),t,e) -> c_11() 16:W:member#(x,nil()) -> c_13() 17:W:negate#(0(x)) -> c_14() 18:W:negate#(1(x)) -> c_15() 19:W:verify#(nil()) -> c_19() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 17: negate#(0(x)) -> c_14() 18: negate#(1(x)) -> c_15() 19: verify#(nil()) -> c_19() 14: if#(false(),t,e) -> c_10() 15: if#(true(),t,e) -> c_11() 16: member#(x,nil()) -> c_13() 13: guess#(nil()) -> c_9() 10: eq#(0(x),1(y)) -> c_3() 11: eq#(1(x),0(y)) -> c_4() 12: eq#(nil(),nil()) -> c_7() 9: choice#(cons(x,xs)) -> c_1() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) - Weak TRS: 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0,c_14/0,c_15/0,c_16/2,c_17/2 ,c_18/4,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:choice#(cons(x,xs)) -> c_2(choice#(xs)) -->_1 choice#(cons(x,xs)) -> c_2(choice#(xs)):1 2:S:eq#(1(x),1(y)) -> c_5(eq#(x,y)) -->_1 eq#(O(x),0(y)) -> c_6(eq#(x,y)):3 -->_1 eq#(1(x),1(y)) -> c_5(eq#(x,y)):2 3:S:eq#(O(x),0(y)) -> c_6(eq#(x,y)) -->_1 eq#(O(x),0(y)) -> c_6(eq#(x,y)):3 -->_1 eq#(1(x),1(y)) -> c_5(eq#(x,y)):2 4:S:guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) -->_2 guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4 -->_1 choice#(cons(x,xs)) -> c_2(choice#(xs)):1 5:S:member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) -->_3 member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5 -->_2 eq#(O(x),0(y)) -> c_6(eq#(x,y)):3 -->_2 eq#(1(x),1(y)) -> c_5(eq#(x,y)):2 6:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) -->_1 satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)):7 -->_2 guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4 7:S:satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) -->_2 verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)):8 8:S:verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) -->_4 verify#(cons(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)):8 -->_2 member#(x,cons(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) - Weak TRS: 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(0(x)) -> 1(x) negate(1(x)) -> 0(x) choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) and a lower component choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) Further, following extension rules are added to the lower component. guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) -->_2 guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):1 2:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):3 -->_2 guess#(cons(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):1 3:S:satck#(cnf,assign) -> c_17(verify#(assign)) -->_1 verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4 4:S:verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) -->_2 verify#(cons(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: guess#(cons(clause,cnf)) -> c_8(guess#(cnf)) verify#(cons(l,ls)) -> c_18(verify#(ls)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: guess#(cons(clause,cnf)) -> c_8(guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(verify#(ls)) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/1,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() guess#(cons(clause,cnf)) -> c_8(guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(verify#(ls)) ** Step 6.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: guess#(cons(clause,cnf)) -> c_8(guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(verify#(ls)) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/1,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant 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(satck#) = {2}, uargs(c_8) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] x1 + [0] p(1) = [1] x1 + [0] p(O) = [1] x1 + [0] p(choice) = [4] x1 + [1] p(cons) = [1] x1 + [1] x2 + [1] p(eq) = [0] p(false) = [0] p(guess) = [4] x1 + [0] p(if) = [0] p(member) = [0] p(negate) = [0] p(nil) = [0] p(sat) = [0] p(satck) = [0] p(true) = [0] p(unsat) = [0] p(verify) = [0] p(choice#) = [0] p(eq#) = [0] p(guess#) = [0] p(if#) = [0] p(member#) = [0] p(negate#) = [8] x1 + [1] p(sat#) = [5] x1 + [10] p(satck#) = [1] x2 + [7] p(verify#) = [9] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [1] p(c_19) = [0] Following rules are strictly oriented: sat#(cnf) = [5] cnf + [10] > [4] cnf + [7] = c_16(satck#(cnf,guess(cnf)),guess#(cnf)) Following rules are (at-least) weakly oriented: guess#(cons(clause,cnf)) = [0] >= [0] = c_8(guess#(cnf)) satck#(cnf,assign) = [1] assign + [7] >= [9] = c_17(verify#(assign)) verify#(cons(l,ls)) = [9] >= [10] = c_18(verify#(ls)) choice(cons(x,xs)) = [4] x + [4] xs + [5] >= [1] x + [0] = x choice(cons(x,xs)) = [4] x + [4] xs + [5] >= [4] xs + [1] = choice(xs) guess(cons(clause,cnf)) = [4] clause + [4] cnf + [4] >= [4] clause + [4] cnf + [2] = cons(choice(clause),guess(cnf)) guess(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: guess#(cons(clause,cnf)) -> c_8(guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(verify#(ls)) - Weak DPs: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/1,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant 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(satck#) = {2}, uargs(c_8) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] x1 + [0] p(1) = [1] x1 + [0] p(O) = [1] x1 + [0] p(choice) = [2] x1 + [8] p(cons) = [1] x1 + [1] x2 + [4] p(eq) = [0] p(false) = [0] p(guess) = [4] x1 + [0] p(if) = [0] p(member) = [0] p(negate) = [0] p(nil) = [0] p(sat) = [0] p(satck) = [0] p(true) = [0] p(unsat) = [0] p(verify) = [0] p(choice#) = [0] p(eq#) = [0] p(guess#) = [4] x1 + [0] p(if#) = [0] p(member#) = [0] p(negate#) = [1] p(sat#) = [12] x1 + [12] p(satck#) = [4] x1 + [1] x2 + [12] p(verify#) = [9] p(c_1) = [1] p(c_2) = [2] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [2] x1 + [2] p(c_6) = [4] x1 + [1] p(c_7) = [2] p(c_8) = [1] x1 + [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] Following rules are strictly oriented: guess#(cons(clause,cnf)) = [4] clause + [4] cnf + [16] > [4] cnf + [0] = c_8(guess#(cnf)) satck#(cnf,assign) = [1] assign + [4] cnf + [12] > [9] = c_17(verify#(assign)) Following rules are (at-least) weakly oriented: sat#(cnf) = [12] cnf + [12] >= [12] cnf + [12] = c_16(satck#(cnf,guess(cnf)),guess#(cnf)) verify#(cons(l,ls)) = [9] >= [9] = c_18(verify#(ls)) choice(cons(x,xs)) = [2] x + [2] xs + [16] >= [1] x + [0] = x choice(cons(x,xs)) = [2] x + [2] xs + [16] >= [2] xs + [8] = choice(xs) guess(cons(clause,cnf)) = [4] clause + [4] cnf + [16] >= [2] clause + [4] cnf + [12] = cons(choice(clause),guess(cnf)) guess(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: verify#(cons(l,ls)) -> c_18(verify#(ls)) - Weak DPs: guess#(cons(clause,cnf)) -> c_8(guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/1,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant 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(satck#) = {2}, uargs(c_8) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] x1 + [0] p(1) = [1] x1 + [0] p(O) = [1] x1 + [0] p(choice) = [5] x1 + [1] p(cons) = [1] x1 + [1] x2 + [3] p(eq) = [0] p(false) = [0] p(guess) = [6] x1 + [0] p(if) = [0] p(member) = [0] p(negate) = [0] p(nil) = [0] p(sat) = [0] p(satck) = [0] p(true) = [0] p(unsat) = [0] p(verify) = [0] p(choice#) = [0] p(eq#) = [0] p(guess#) = [0] p(if#) = [0] p(member#) = [8] x1 + [8] x2 + [0] p(negate#) = [4] x1 + [8] p(sat#) = [7] x1 + [1] p(satck#) = [1] x2 + [0] p(verify#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] Following rules are strictly oriented: verify#(cons(l,ls)) = [1] l + [1] ls + [3] > [1] ls + [0] = c_18(verify#(ls)) Following rules are (at-least) weakly oriented: guess#(cons(clause,cnf)) = [0] >= [0] = c_8(guess#(cnf)) sat#(cnf) = [7] cnf + [1] >= [6] cnf + [0] = c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) = [1] assign + [0] >= [1] assign + [0] = c_17(verify#(assign)) choice(cons(x,xs)) = [5] x + [5] xs + [16] >= [1] x + [0] = x choice(cons(x,xs)) = [5] x + [5] xs + [16] >= [5] xs + [1] = choice(xs) guess(cons(clause,cnf)) = [6] clause + [6] cnf + [18] >= [5] clause + [6] cnf + [4] = cons(choice(clause),guess(cnf)) guess(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: guess#(cons(clause,cnf)) -> c_8(guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(cons(l,ls)) -> c_18(verify#(ls)) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/1,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) - Weak DPs: guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component choice#(cons(x,xs)) -> c_2(choice#(xs)) guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) and a lower component eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) Further, following extension rules are added to the lower component. choice#(cons(x,xs)) -> choice#(xs) guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) member#(x,cons(y,ys)) -> eq#(x,y) member#(x,cons(y,ys)) -> member#(x,ys) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) *** Step 6.b:1.a:1: RemoveHeads WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) - Weak DPs: guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:choice#(cons(x,xs)) -> c_2(choice#(xs)) -->_1 choice#(cons(x,xs)) -> c_2(choice#(xs)):1 2:S:member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) -->_2 member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2 3:W:guess#(cons(clause,cnf)) -> choice#(clause) -->_1 choice#(cons(x,xs)) -> c_2(choice#(xs)):1 4:W:guess#(cons(clause,cnf)) -> guess#(cnf) -->_1 guess#(cons(clause,cnf)) -> guess#(cnf):4 -->_1 guess#(cons(clause,cnf)) -> choice#(clause):3 5:W:sat#(cnf) -> guess#(cnf) -->_1 guess#(cons(clause,cnf)) -> guess#(cnf):4 -->_1 guess#(cons(clause,cnf)) -> choice#(clause):3 6:W:sat#(cnf) -> satck#(cnf,guess(cnf)) -->_1 satck#(cnf,assign) -> verify#(assign):7 7:W:satck#(cnf,assign) -> verify#(assign) -->_1 verify#(cons(l,ls)) -> verify#(ls):9 -->_1 verify#(cons(l,ls)) -> member#(negate(l),ls):8 8:W:verify#(cons(l,ls)) -> member#(negate(l),ls) -->_1 member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2 9:W:verify#(cons(l,ls)) -> verify#(ls) -->_1 verify#(cons(l,ls)) -> verify#(ls):9 -->_1 verify#(cons(l,ls)) -> member#(negate(l),ls):8 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(5,sat#(cnf) -> guess#(cnf))] *** Step 6.b:1.a:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) - Weak DPs: guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:choice#(cons(x,xs)) -> c_2(choice#(xs)) -->_1 choice#(cons(x,xs)) -> c_2(choice#(xs)):1 2:S:member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) -->_2 member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2 3:W:guess#(cons(clause,cnf)) -> choice#(clause) -->_1 choice#(cons(x,xs)) -> c_2(choice#(xs)):1 4:W:guess#(cons(clause,cnf)) -> guess#(cnf) -->_1 guess#(cons(clause,cnf)) -> guess#(cnf):4 -->_1 guess#(cons(clause,cnf)) -> choice#(clause):3 6:W:sat#(cnf) -> satck#(cnf,guess(cnf)) -->_1 satck#(cnf,assign) -> verify#(assign):7 7:W:satck#(cnf,assign) -> verify#(assign) -->_1 verify#(cons(l,ls)) -> verify#(ls):9 -->_1 verify#(cons(l,ls)) -> member#(negate(l),ls):8 8:W:verify#(cons(l,ls)) -> member#(negate(l),ls) -->_1 member#(x,cons(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2 9:W:verify#(cons(l,ls)) -> verify#(ls) -->_1 verify#(cons(l,ls)) -> verify#(ls):9 -->_1 verify#(cons(l,ls)) -> member#(negate(l),ls):8 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: member#(x,cons(y,ys)) -> c_12(member#(x,ys)) *** Step 6.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) member#(x,cons(y,ys)) -> c_12(member#(x,ys)) - Weak DPs: guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant 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(member#) = {1}, uargs(satck#) = {2}, uargs(c_2) = {1}, uargs(c_12) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] x1 + [3] p(1) = [1] x1 + [3] p(O) = [1] x1 + [0] p(choice) = [2] x1 + [5] p(cons) = [1] x1 + [1] x2 + [5] p(eq) = [0] p(false) = [0] p(guess) = [2] x1 + [0] p(if) = [0] p(member) = [0] p(negate) = [1] x1 + [0] p(nil) = [0] p(sat) = [0] p(satck) = [0] p(true) = [0] p(unsat) = [0] p(verify) = [0] p(choice#) = [3] p(eq#) = [0] p(guess#) = [3] p(if#) = [0] p(member#) = [1] x1 + [1] x2 + [0] p(negate#) = [0] p(sat#) = [2] x1 + [0] p(satck#) = [1] x2 + [0] p(verify#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [2] p(c_12) = [1] x1 + [4] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] x2 + [1] p(c_19) = [2] Following rules are strictly oriented: member#(x,cons(y,ys)) = [1] x + [1] y + [1] ys + [5] > [1] x + [1] ys + [4] = c_12(member#(x,ys)) Following rules are (at-least) weakly oriented: choice#(cons(x,xs)) = [3] >= [3] = c_2(choice#(xs)) guess#(cons(clause,cnf)) = [3] >= [3] = choice#(clause) guess#(cons(clause,cnf)) = [3] >= [3] = guess#(cnf) sat#(cnf) = [2] cnf + [0] >= [2] cnf + [0] = satck#(cnf,guess(cnf)) satck#(cnf,assign) = [1] assign + [0] >= [1] assign + [0] = verify#(assign) verify#(cons(l,ls)) = [1] l + [1] ls + [5] >= [1] l + [1] ls + [0] = member#(negate(l),ls) verify#(cons(l,ls)) = [1] l + [1] ls + [5] >= [1] ls + [0] = verify#(ls) choice(cons(x,xs)) = [2] x + [2] xs + [15] >= [1] x + [0] = x choice(cons(x,xs)) = [2] x + [2] xs + [15] >= [2] xs + [5] = choice(xs) guess(cons(clause,cnf)) = [2] clause + [2] cnf + [10] >= [2] clause + [2] cnf + [10] = cons(choice(clause),guess(cnf)) guess(nil()) = [0] >= [0] = nil() negate(0(x)) = [1] x + [3] >= [1] x + [3] = 1(x) negate(1(x)) = [1] x + [3] >= [1] x + [3] = 0(x) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) - Weak DPs: guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) member#(x,cons(y,ys)) -> c_12(member#(x,ys)) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant 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(member#) = {1}, uargs(satck#) = {2}, uargs(c_2) = {1}, uargs(c_12) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [6] p(1) = [5] p(O) = [1] x1 + [0] p(choice) = [2] x1 + [1] p(cons) = [1] x1 + [1] x2 + [1] p(eq) = [0] p(false) = [0] p(guess) = [2] x1 + [0] p(if) = [0] p(member) = [0] p(negate) = [1] x1 + [1] p(nil) = [7] p(sat) = [0] p(satck) = [0] p(true) = [0] p(unsat) = [0] p(verify) = [0] p(choice#) = [1] x1 + [0] p(eq#) = [0] p(guess#) = [2] x1 + [4] p(if#) = [0] p(member#) = [1] x1 + [0] p(negate#) = [4] x1 + [1] p(sat#) = [6] x1 + [3] p(satck#) = [4] x1 + [1] x2 + [1] p(verify#) = [1] x1 + [0] p(c_1) = [4] p(c_2) = [1] x1 + [0] p(c_3) = [2] p(c_4) = [0] p(c_5) = [4] x1 + [2] p(c_6) = [4] x1 + [2] p(c_7) = [0] p(c_8) = [4] x2 + [1] p(c_9) = [1] p(c_10) = [0] p(c_11) = [2] p(c_12) = [1] x1 + [0] p(c_13) = [0] p(c_14) = [1] p(c_15) = [2] p(c_16) = [1] x2 + [1] p(c_17) = [1] p(c_18) = [1] x1 + [1] x2 + [1] p(c_19) = [2] Following rules are strictly oriented: choice#(cons(x,xs)) = [1] x + [1] xs + [1] > [1] xs + [0] = c_2(choice#(xs)) Following rules are (at-least) weakly oriented: guess#(cons(clause,cnf)) = [2] clause + [2] cnf + [6] >= [1] clause + [0] = choice#(clause) guess#(cons(clause,cnf)) = [2] clause + [2] cnf + [6] >= [2] cnf + [4] = guess#(cnf) member#(x,cons(y,ys)) = [1] x + [0] >= [1] x + [0] = c_12(member#(x,ys)) sat#(cnf) = [6] cnf + [3] >= [6] cnf + [1] = satck#(cnf,guess(cnf)) satck#(cnf,assign) = [1] assign + [4] cnf + [1] >= [1] assign + [0] = verify#(assign) verify#(cons(l,ls)) = [1] l + [1] ls + [1] >= [1] l + [1] = member#(negate(l),ls) verify#(cons(l,ls)) = [1] l + [1] ls + [1] >= [1] ls + [0] = verify#(ls) choice(cons(x,xs)) = [2] x + [2] xs + [3] >= [1] x + [0] = x choice(cons(x,xs)) = [2] x + [2] xs + [3] >= [2] xs + [1] = choice(xs) guess(cons(clause,cnf)) = [2] clause + [2] cnf + [2] >= [2] clause + [2] cnf + [2] = cons(choice(clause),guess(cnf)) guess(nil()) = [14] >= [7] = nil() negate(0(x)) = [7] >= [5] = 1(x) negate(1(x)) = [6] >= [6] = 0(x) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: choice#(cons(x,xs)) -> c_2(choice#(xs)) guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) member#(x,cons(y,ys)) -> c_12(member#(x,ys)) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 6.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) - Weak DPs: choice#(cons(x,xs)) -> choice#(xs) guess#(cons(clause,cnf)) -> choice#(clause) guess#(cons(clause,cnf)) -> guess#(cnf) member#(x,cons(y,ys)) -> eq#(x,y) member#(x,cons(y,ys)) -> member#(x,ys) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eq#(1(x),1(y)) -> c_5(eq#(x,y)) -->_1 eq#(O(x),0(y)) -> c_6(eq#(x,y)):2 -->_1 eq#(1(x),1(y)) -> c_5(eq#(x,y)):1 2:S:eq#(O(x),0(y)) -> c_6(eq#(x,y)) -->_1 eq#(O(x),0(y)) -> c_6(eq#(x,y)):2 -->_1 eq#(1(x),1(y)) -> c_5(eq#(x,y)):1 3:W:choice#(cons(x,xs)) -> choice#(xs) -->_1 choice#(cons(x,xs)) -> choice#(xs):3 4:W:guess#(cons(clause,cnf)) -> choice#(clause) -->_1 choice#(cons(x,xs)) -> choice#(xs):3 5:W:guess#(cons(clause,cnf)) -> guess#(cnf) -->_1 guess#(cons(clause,cnf)) -> guess#(cnf):5 -->_1 guess#(cons(clause,cnf)) -> choice#(clause):4 6:W:member#(x,cons(y,ys)) -> eq#(x,y) -->_1 eq#(O(x),0(y)) -> c_6(eq#(x,y)):2 -->_1 eq#(1(x),1(y)) -> c_5(eq#(x,y)):1 7:W:member#(x,cons(y,ys)) -> member#(x,ys) -->_1 member#(x,cons(y,ys)) -> member#(x,ys):7 -->_1 member#(x,cons(y,ys)) -> eq#(x,y):6 8:W:sat#(cnf) -> guess#(cnf) -->_1 guess#(cons(clause,cnf)) -> guess#(cnf):5 -->_1 guess#(cons(clause,cnf)) -> choice#(clause):4 9:W:sat#(cnf) -> satck#(cnf,guess(cnf)) -->_1 satck#(cnf,assign) -> verify#(assign):10 10:W:satck#(cnf,assign) -> verify#(assign) -->_1 verify#(cons(l,ls)) -> verify#(ls):12 -->_1 verify#(cons(l,ls)) -> member#(negate(l),ls):11 11:W:verify#(cons(l,ls)) -> member#(negate(l),ls) -->_1 member#(x,cons(y,ys)) -> member#(x,ys):7 -->_1 member#(x,cons(y,ys)) -> eq#(x,y):6 12:W:verify#(cons(l,ls)) -> verify#(ls) -->_1 verify#(cons(l,ls)) -> verify#(ls):12 -->_1 verify#(cons(l,ls)) -> member#(negate(l),ls):11 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: sat#(cnf) -> guess#(cnf) 5: guess#(cons(clause,cnf)) -> guess#(cnf) 4: guess#(cons(clause,cnf)) -> choice#(clause) 3: choice#(cons(x,xs)) -> choice#(xs) *** Step 6.b:1.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) - Weak DPs: member#(x,cons(y,ys)) -> eq#(x,y) member#(x,cons(y,ys)) -> member#(x,ys) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant 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(member#) = {1}, uargs(satck#) = {2}, uargs(c_5) = {1}, uargs(c_6) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] x1 + [0] p(1) = [1] x1 + [0] p(O) = [1] x1 + [4] p(choice) = [1] x1 + [0] p(cons) = [1] x1 + [1] x2 + [5] p(eq) = [0] p(false) = [2] p(guess) = [1] x1 + [0] p(if) = [2] x3 + [0] p(member) = [0] p(negate) = [1] x1 + [5] p(nil) = [0] p(sat) = [0] p(satck) = [0] p(true) = [0] p(unsat) = [0] p(verify) = [0] p(choice#) = [0] p(eq#) = [1] x1 + [0] p(guess#) = [0] p(if#) = [2] x1 + [4] x2 + [0] p(member#) = [1] x1 + [0] p(negate#) = [1] x1 + [0] p(sat#) = [2] x1 + [1] p(satck#) = [1] x2 + [1] p(verify#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [1] p(c_7) = [2] p(c_8) = [4] x2 + [2] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [2] x1 + [1] x2 + [0] p(c_13) = [0] p(c_14) = [2] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [1] p(c_17) = [2] p(c_18) = [1] p(c_19) = [1] Following rules are strictly oriented: eq#(O(x),0(y)) = [1] x + [4] > [1] x + [1] = c_6(eq#(x,y)) Following rules are (at-least) weakly oriented: eq#(1(x),1(y)) = [1] x + [0] >= [1] x + [0] = c_5(eq#(x,y)) member#(x,cons(y,ys)) = [1] x + [0] >= [1] x + [0] = eq#(x,y) member#(x,cons(y,ys)) = [1] x + [0] >= [1] x + [0] = member#(x,ys) sat#(cnf) = [2] cnf + [1] >= [1] cnf + [1] = satck#(cnf,guess(cnf)) satck#(cnf,assign) = [1] assign + [1] >= [1] assign + [0] = verify#(assign) verify#(cons(l,ls)) = [1] l + [1] ls + [5] >= [1] l + [5] = member#(negate(l),ls) verify#(cons(l,ls)) = [1] l + [1] ls + [5] >= [1] ls + [0] = verify#(ls) choice(cons(x,xs)) = [1] x + [1] xs + [5] >= [1] x + [0] = x choice(cons(x,xs)) = [1] x + [1] xs + [5] >= [1] xs + [0] = choice(xs) guess(cons(clause,cnf)) = [1] clause + [1] cnf + [5] >= [1] clause + [1] cnf + [5] = cons(choice(clause),guess(cnf)) guess(nil()) = [0] >= [0] = nil() negate(0(x)) = [1] x + [5] >= [1] x + [0] = 1(x) negate(1(x)) = [1] x + [5] >= [1] x + [0] = 0(x) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(1(x),1(y)) -> c_5(eq#(x,y)) - Weak DPs: eq#(O(x),0(y)) -> c_6(eq#(x,y)) member#(x,cons(y,ys)) -> eq#(x,y) member#(x,cons(y,ys)) -> member#(x,ys) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant 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(member#) = {1}, uargs(satck#) = {2}, uargs(c_5) = {1}, uargs(c_6) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] x1 + [2] p(1) = [1] x1 + [2] p(O) = [1] x1 + [0] p(choice) = [1] x1 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(false) = [0] p(guess) = [3] x1 + [0] p(if) = [0] p(member) = [0] p(negate) = [1] x1 + [0] p(nil) = [0] p(sat) = [0] p(satck) = [2] x1 + [1] x2 + [0] p(true) = [0] p(unsat) = [0] p(verify) = [2] x1 + [2] p(choice#) = [2] x1 + [4] p(eq#) = [1] x1 + [0] p(guess#) = [1] p(if#) = [1] x1 + [1] x3 + [4] p(member#) = [1] x1 + [0] p(negate#) = [2] x1 + [1] p(sat#) = [4] x1 + [4] p(satck#) = [1] x1 + [1] x2 + [0] p(verify#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [1] p(c_3) = [4] p(c_4) = [1] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [1] x1 + [2] x2 + [2] p(c_9) = [1] p(c_10) = [0] p(c_11) = [1] p(c_12) = [2] p(c_13) = [1] p(c_14) = [0] p(c_15) = [1] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [4] p(c_18) = [0] p(c_19) = [2] Following rules are strictly oriented: eq#(1(x),1(y)) = [1] x + [2] > [1] x + [0] = c_5(eq#(x,y)) Following rules are (at-least) weakly oriented: eq#(O(x),0(y)) = [1] x + [0] >= [1] x + [0] = c_6(eq#(x,y)) member#(x,cons(y,ys)) = [1] x + [0] >= [1] x + [0] = eq#(x,y) member#(x,cons(y,ys)) = [1] x + [0] >= [1] x + [0] = member#(x,ys) sat#(cnf) = [4] cnf + [4] >= [4] cnf + [0] = satck#(cnf,guess(cnf)) satck#(cnf,assign) = [1] assign + [1] cnf + [0] >= [1] assign + [0] = verify#(assign) verify#(cons(l,ls)) = [1] l + [1] ls + [0] >= [1] l + [0] = member#(negate(l),ls) verify#(cons(l,ls)) = [1] l + [1] ls + [0] >= [1] ls + [0] = verify#(ls) choice(cons(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [0] = x choice(cons(x,xs)) = [1] x + [1] xs + [0] >= [1] xs + [0] = choice(xs) guess(cons(clause,cnf)) = [3] clause + [3] cnf + [0] >= [1] clause + [3] cnf + [0] = cons(choice(clause),guess(cnf)) guess(nil()) = [0] >= [0] = nil() negate(0(x)) = [1] x + [2] >= [1] x + [2] = 1(x) negate(1(x)) = [1] x + [2] >= [1] x + [2] = 0(x) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eq#(1(x),1(y)) -> c_5(eq#(x,y)) eq#(O(x),0(y)) -> c_6(eq#(x,y)) member#(x,cons(y,ys)) -> eq#(x,y) member#(x,cons(y,ys)) -> member#(x,ys) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(cons(l,ls)) -> member#(negate(l),ls) verify#(cons(l,ls)) -> verify#(ls) - Weak TRS: choice(cons(x,xs)) -> x choice(cons(x,xs)) -> choice(xs) guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf)) guess(nil()) -> nil() 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,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,c_1/0 ,c_2/1,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {0,1,O,cons,false,nil,true,unsat} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))