WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            eq(#1(x),#1(y)) -> eq(x,y)
            eq(#1(x),O(y)) -> false()
            eq(O(x),#1(y)) -> false()
            eq(O(x),O(y)) -> eq(x,y)
            eq(nil(),nil()) -> true()
            guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
            guess(nil()) -> nil()
            if(false(),t,e) -> e
            if(true(),t,e) -> t
            member(x,dd(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(dd(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,dd/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,dd,false,nil,true,unsat}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          choice#(dd(x,xs)) -> c_1()
          choice#(dd(x,xs)) -> c_2(choice#(xs))
          eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
          eq#(#1(x),O(y)) -> c_4()
          eq#(O(x),#1(y)) -> c_5()
          eq#(O(x),O(y)) -> c_6(eq#(x,y))
          eq#(nil(),nil()) -> c_7()
          guess#(dd(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,dd(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#(dd(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: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_1()
            choice#(dd(x,xs)) -> c_2(choice#(xs))
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(#1(x),O(y)) -> c_4()
            eq#(O(x),#1(y)) -> c_5()
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            eq#(nil(),nil()) -> c_7()
            guess#(dd(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,dd(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#(dd(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(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            eq(#1(x),#1(y)) -> eq(x,y)
            eq(#1(x),O(y)) -> false()
            eq(O(x),#1(y)) -> false()
            eq(O(x),O(y)) -> eq(x,y)
            eq(nil(),nil()) -> true()
            guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
            guess(nil()) -> nil()
            if(false(),t,e) -> e
            if(true(),t,e) -> t
            member(x,dd(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(dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          choice(dd(x,xs)) -> x
          choice(dd(x,xs)) -> choice(xs)
          eq(#1(x),#1(y)) -> eq(x,y)
          eq(#1(x),O(y)) -> false()
          eq(O(x),#1(y)) -> false()
          eq(O(x),O(y)) -> eq(x,y)
          eq(nil(),nil()) -> true()
          guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
          guess(nil()) -> nil()
          if(false(),t,e) -> e
          if(true(),t,e) -> t
          member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys))
          member(x,nil()) -> false()
          negate(#0(x)) -> #1(x)
          negate(#1(x)) -> #0(x)
          verify(dd(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
          verify(nil()) -> true()
          choice#(dd(x,xs)) -> c_1()
          choice#(dd(x,xs)) -> c_2(choice#(xs))
          eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
          eq#(#1(x),O(y)) -> c_4()
          eq#(O(x),#1(y)) -> c_5()
          eq#(O(x),O(y)) -> c_6(eq#(x,y))
          eq#(nil(),nil()) -> c_7()
          guess#(dd(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,dd(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#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls))
                                   ,member#(negate(l),ls)
                                   ,negate#(l)
                                   ,verify#(ls))
          verify#(nil()) -> c_19()
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_1()
            choice#(dd(x,xs)) -> c_2(choice#(xs))
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(#1(x),O(y)) -> c_4()
            eq#(O(x),#1(y)) -> c_5()
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            eq#(nil(),nil()) -> c_7()
            guess#(dd(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,dd(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#(dd(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(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            eq(#1(x),#1(y)) -> eq(x,y)
            eq(#1(x),O(y)) -> false()
            eq(O(x),#1(y)) -> false()
            eq(O(x),O(y)) -> eq(x,y)
            eq(nil(),nil()) -> true()
            guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
            guess(nil()) -> nil()
            if(false(),t,e) -> e
            if(true(),t,e) -> t
            member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys))
            member(x,nil()) -> false()
            negate(#0(x)) -> #1(x)
            negate(#1(x)) -> #0(x)
            verify(dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,4,5,7,9,10,11,13,14,15,19}
        by application of
          Pre({1,4,5,7,9,10,11,13,14,15,19}) = {2,3,6,8,12,16,17,18}.
        Here rules are labelled as follows:
          1: choice#(dd(x,xs)) -> c_1()
          2: choice#(dd(x,xs)) -> c_2(choice#(xs))
          3: eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
          4: eq#(#1(x),O(y)) -> c_4()
          5: eq#(O(x),#1(y)) -> c_5()
          6: eq#(O(x),O(y)) -> c_6(eq#(x,y))
          7: eq#(nil(),nil()) -> c_7()
          8: guess#(dd(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,dd(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#(dd(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 4: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls))
                                     ,member#(negate(l),ls)
                                     ,negate#(l)
                                     ,verify#(ls))
        - Weak DPs:
            choice#(dd(x,xs)) -> c_1()
            eq#(#1(x),O(y)) -> c_4()
            eq#(O(x),#1(y)) -> c_5()
            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(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            eq(#1(x),#1(y)) -> eq(x,y)
            eq(#1(x),O(y)) -> false()
            eq(O(x),#1(y)) -> false()
            eq(O(x),O(y)) -> eq(x,y)
            eq(nil(),nil()) -> true()
            guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
            guess(nil()) -> nil()
            if(false(),t,e) -> e
            if(true(),t,e) -> t
            member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys))
            member(x,nil()) -> false()
            negate(#0(x)) -> #1(x)
            negate(#1(x)) -> #0(x)
            verify(dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:choice#(dd(x,xs)) -> c_2(choice#(xs))
             -->_1 choice#(dd(x,xs)) -> c_1():9
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
          
          2:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
             -->_1 eq#(nil(),nil()) -> c_7():12
             -->_1 eq#(O(x),#1(y)) -> c_5():11
             -->_1 eq#(#1(x),O(y)) -> c_4():10
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2
          
          3:S:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(nil(),nil()) -> c_7():12
             -->_1 eq#(O(x),#1(y)) -> c_5():11
             -->_1 eq#(#1(x),O(y)) -> c_4():10
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2
          
          4:S:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
             -->_2 guess#(nil()) -> c_9():13
             -->_1 choice#(dd(x,xs)) -> c_1():9
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
          
          5:S:member#(x,dd(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#(O(x),#1(y)) -> c_5():11
             -->_2 eq#(#1(x),O(y)) -> c_4():10
             -->_3 member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5
             -->_2 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
             -->_2 eq#(#1(x),#1(y)) -> c_3(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#(dd(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#(dd(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#(dd(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#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls))
                                            ,member#(negate(l),ls)
                                            ,negate#(l)
                                            ,verify#(ls)):8
             -->_2 member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5
          
          9:W:choice#(dd(x,xs)) -> c_1()
             
          
          10:W:eq#(#1(x),O(y)) -> c_4()
             
          
          11:W:eq#(O(x),#1(y)) -> c_5()
             
          
          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#(#1(x),O(y)) -> c_4()
          11: eq#(O(x),#1(y)) -> c_5()
          12: eq#(nil(),nil()) -> c_7()
          9: choice#(dd(x,xs)) -> c_1()
* Step 5: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls))
                                     ,member#(negate(l),ls)
                                     ,negate#(l)
                                     ,verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            eq(#1(x),#1(y)) -> eq(x,y)
            eq(#1(x),O(y)) -> false()
            eq(O(x),#1(y)) -> false()
            eq(O(x),O(y)) -> eq(x,y)
            eq(nil(),nil()) -> true()
            guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
            guess(nil()) -> nil()
            if(false(),t,e) -> e
            if(true(),t,e) -> t
            member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys))
            member(x,nil()) -> false()
            negate(#0(x)) -> #1(x)
            negate(#1(x)) -> #0(x)
            verify(dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:choice#(dd(x,xs)) -> c_2(choice#(xs))
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
          
          2:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2
          
          3:S:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2
          
          4:S:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
          
          5:S:member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys))
             -->_3 member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5
             -->_2 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
             -->_2 eq#(#1(x),#1(y)) -> c_3(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#(dd(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#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls))
                                            ,member#(negate(l),ls)
                                            ,negate#(l)
                                            ,verify#(ls)):8
          
          8:S:verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls))
                                       ,member#(negate(l),ls)
                                       ,negate#(l)
                                       ,verify#(ls))
             -->_4 verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls))
                                            ,member#(negate(l),ls)
                                            ,negate#(l)
                                            ,verify#(ls)):8
             -->_2 member#(x,dd(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,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
          satck#(cnf,assign) -> c_17(verify#(assign))
          verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
* Step 6: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            eq(#1(x),#1(y)) -> eq(x,y)
            eq(#1(x),O(y)) -> false()
            eq(O(x),#1(y)) -> false()
            eq(O(x),O(y)) -> eq(x,y)
            eq(nil(),nil()) -> true()
            guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
            guess(nil()) -> nil()
            if(false(),t,e) -> e
            if(true(),t,e) -> t
            member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys))
            member(x,nil()) -> false()
            negate(#0(x)) -> #1(x)
            negate(#1(x)) -> #0(x)
            verify(dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          choice(dd(x,xs)) -> x
          choice(dd(x,xs)) -> choice(xs)
          guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
          guess(nil()) -> nil()
          negate(#0(x)) -> #1(x)
          negate(#1(x)) -> #0(x)
          choice#(dd(x,xs)) -> c_2(choice#(xs))
          eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
          eq#(O(x),O(y)) -> c_6(eq#(x,y))
          guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
          member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
* Step 7: Decompose WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    + Details:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          - Strict DPs:
              choice#(dd(x,xs)) -> c_2(choice#(xs))
          - Weak DPs:
              eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
              eq#(O(x),O(y)) -> c_6(eq#(x,y))
              guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
              member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          - Weak TRS:
              choice(dd(x,xs)) -> x
              choice(dd(x,xs)) -> choice(xs)
              guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
              ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
        
        Problem (S)
          - Strict DPs:
              eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
              eq#(O(x),O(y)) -> c_6(eq#(x,y))
              guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
              member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          - Weak DPs:
              choice#(dd(x,xs)) -> c_2(choice#(xs))
          - Weak TRS:
              choice(dd(x,xs)) -> x
              choice(dd(x,xs)) -> choice(xs)
              guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
              ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
** Step 7.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
        - Weak DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:choice#(dd(x,xs)) -> c_2(choice#(xs))
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
          
          2:W:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2
          
          3:W:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
          
          4:W:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4
          
          5:W:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3
             -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):5
          
          6:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):7
          
          7:W:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):8
          
          8:W:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):5
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):8
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: satck#(cnf,assign) -> c_17(verify#(assign))
          8: verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          5: member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
          2: eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
          3: eq#(O(x),O(y)) -> c_6(eq#(x,y))
** Step 7.a:2: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
        - Weak DPs:
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:choice#(dd(x,xs)) -> c_2(choice#(xs))
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
          
          4:W:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4
          
          6:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          sat#(cnf) -> c_16(guess#(cnf))
** Step 7.a:3: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
        - Weak DPs:
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            sat#(cnf) -> c_16(guess#(cnf))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          choice#(dd(x,xs)) -> c_2(choice#(xs))
          guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
          sat#(cnf) -> c_16(guess#(cnf))
** Step 7.a:4: PredecessorEstimationCP WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
        - Weak DPs:
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            sat#(cnf) -> c_16(guess#(cnf))
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          1: choice#(dd(x,xs)) -> c_2(choice#(xs))
          
        Consider the set of all dependency pairs
          1: choice#(dd(x,xs)) -> c_2(choice#(xs))
          2: guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
          3: sat#(cnf) -> c_16(guess#(cnf))
        Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
        SPACE(?,?)on application of the dependency pairs
          {1}
        These cover all (indirect) predecessors of dependency pairs
          {1,3}
        their number of applications is equally bounded.
        The dependency pairs are shifted into the weak component.
*** Step 7.a:4.a:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
        - Weak DPs:
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            sat#(cnf) -> c_16(guess#(cnf))
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_2) = {1},
          uargs(c_8) = {1,2},
          uargs(c_16) = {1}
        
        Following symbols are considered usable:
          {choice#,eq#,guess#,if#,member#,negate#,sat#,satck#,verify#}
        TcT has computed the following interpretation:
               p(#0) = [1] x1 + [0]         
               p(#1) = [1] x1 + [0]         
                p(O) = [1] x1 + [0]         
           p(choice) = [0]                  
               p(dd) = [1] x1 + [1] x2 + [8]
               p(eq) = [0]                  
            p(false) = [0]                  
            p(guess) = [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#) = [2] x1 + [0]         
              p(eq#) = [0]                  
           p(guess#) = [3] x1 + [0]         
              p(if#) = [0]                  
          p(member#) = [0]                  
          p(negate#) = [1] x1 + [1]         
             p(sat#) = [12] x1 + [9]        
           p(satck#) = [1]                  
          p(verify#) = [1] x1 + [1]         
              p(c_1) = [2]                  
              p(c_2) = [1] x1 + [6]         
              p(c_3) = [8]                  
              p(c_4) = [0]                  
              p(c_5) = [1]                  
              p(c_6) = [1] x1 + [1]         
              p(c_7) = [0]                  
              p(c_8) = [1] x1 + [1] x2 + [6]
              p(c_9) = [0]                  
             p(c_10) = [2]                  
             p(c_11) = [1]                  
             p(c_12) = [1] x2 + [2]         
             p(c_13) = [2]                  
             p(c_14) = [2]                  
             p(c_15) = [4]                  
             p(c_16) = [4] x1 + [1]         
             p(c_17) = [1]                  
             p(c_18) = [4] x1 + [1]         
             p(c_19) = [1]                  
        
        Following rules are strictly oriented:
        choice#(dd(x,xs)) = [2] x + [2] xs + [16]
                          > [2] xs + [6]         
                          = c_2(choice#(xs))     
        
        
        Following rules are (at-least) weakly oriented:
        guess#(dd(clause,cnf)) =  [3] clause + [3] cnf + [24]     
                               >= [2] clause + [3] cnf + [6]      
                               =  c_8(choice#(clause),guess#(cnf))
        
                     sat#(cnf) =  [12] cnf + [9]                  
                               >= [12] cnf + [1]                  
                               =  c_16(guess#(cnf))               
        
*** Step 7.a:4.a:2: Assumption WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            sat#(cnf) -> c_16(guess#(cnf))
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
    + Details:
        ()

*** Step 7.a:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            sat#(cnf) -> c_16(guess#(cnf))
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:choice#(dd(x,xs)) -> c_2(choice#(xs))
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
          
          2:W:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):2
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1
          
          3:W:sat#(cnf) -> c_16(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):2
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          3: sat#(cnf) -> c_16(guess#(cnf))
          2: guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
          1: choice#(dd(x,xs)) -> c_2(choice#(xs))
*** Step 7.a:4.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

** Step 7.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak DPs:
            choice#(dd(x,xs)) -> c_2(choice#(xs))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          2:S:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          3:S:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):8
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):3
          
          4:S:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
             -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):4
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          5:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):6
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):3
          
          6:S:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):7
          
          7:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):7
             -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):4
          
          8:W:choice#(dd(x,xs)) -> c_2(choice#(xs))
             -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):8
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          8: choice#(dd(x,xs)) -> c_2(choice#(xs))
** Step 7.b:2: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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,dd,false,nil,true,unsat}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          2:S:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          3:S:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):3
          
          4:S:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
             -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):4
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          5:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):6
             -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):3
          
          6:S:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):7
          
          7:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):7
             -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
** Step 7.b:3: Decompose WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/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,dd,false,nil,true,unsat}
    + Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    + Details:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          - Strict DPs:
              eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
              eq#(O(x),O(y)) -> c_6(eq#(x,y))
          - Weak DPs:
              guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
              member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          - Weak TRS:
              choice(dd(x,xs)) -> x
              choice(dd(x,xs)) -> choice(xs)
              guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
              ,c_2/1,c_3/1,c_4/0,c_5/0,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/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,dd,false,nil,true,unsat}
        
        Problem (S)
          - Strict DPs:
              guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
              member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          - Weak DPs:
              eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
              eq#(O(x),O(y)) -> c_6(eq#(x,y))
          - Weak TRS:
              choice(dd(x,xs)) -> x
              choice(dd(x,xs)) -> choice(xs)
              guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
              ,c_2/1,c_3/1,c_4/0,c_5/0,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/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,dd,false,nil,true,unsat}
*** Step 7.b:3.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
        - Weak DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          2:S:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
          
          3:W:guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):3
          
          4:W:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):4
          
          5:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):3
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):6
          
          6:W:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):7
          
          7:W:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):4
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):7
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          3: guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
*** Step 7.b:3.a:2: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
        - Weak DPs:
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/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,dd,false,nil,true,unsat}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          2:S:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
          
          4:W:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):4
          
          5:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):6
          
          6:W:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):7
          
          7:W:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):4
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):7
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
*** Step 7.b:3.a:3: PredecessorEstimationCP WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
        - Weak DPs:
            member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          1: eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
          2: eq#(O(x),O(y)) -> c_6(eq#(x,y))
          
        Consider the set of all dependency pairs
          1: eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
          2: eq#(O(x),O(y)) -> c_6(eq#(x,y))
          3: member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
          4: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
          5: satck#(cnf,assign) -> c_17(verify#(assign))
          6: verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2))
        SPACE(?,?)on application of the dependency pairs
          {1,2}
        These cover all (indirect) predecessors of dependency pairs
          {1,2,4,5}
        their number of applications is equally bounded.
        The dependency pairs are shifted into the weak component.
**** Step 7.b:3.a:3.a:1: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
        - Weak DPs:
            member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(c_3) = {1},
          uargs(c_6) = {1},
          uargs(c_12) = {1,2},
          uargs(c_16) = {1},
          uargs(c_17) = {1},
          uargs(c_18) = {1,2}
        
        Following symbols are considered usable:
          {choice,guess,negate,choice#,eq#,guess#,if#,member#,negate#,sat#,satck#,verify#}
        TcT has computed the following interpretation:
               p(#0) = 2 + x1                                            
               p(#1) = 2 + x1                                            
                p(O) = 2 + x1                                            
           p(choice) = x1                                                
               p(dd) = 1 + x1 + x2                                       
               p(eq) = 4 + 2*x1 + 2*x1*x2 + x1^2 + x2 + 2*x2^2           
            p(false) = 2                                                 
            p(guess) = x1                                                
               p(if) = 2 + x1*x2 + 4*x1*x3 + x1^2 + x2 + x2^2 + x3 + x3^2
           p(member) = x1^2 + 4*x2                                       
           p(negate) = x1                                                
              p(nil) = 0                                                 
              p(sat) = 4*x1 + 2*x1^2                                     
            p(satck) = x1 + x1^2 + x2                                    
             p(true) = 1                                                 
            p(unsat) = 1                                                 
           p(verify) = 0                                                 
          p(choice#) = 4 + 4*x1                                          
              p(eq#) = 4*x1                                              
           p(guess#) = 0                                                 
              p(if#) = 2 + x1*x2 + x1^2 + x2^2                           
          p(member#) = 2*x1 + 6*x1*x2 + 5*x1^2                           
          p(negate#) = 1 + x1 + 4*x1^2                                   
             p(sat#) = 6 + 6*x1 + 6*x1^2                                 
           p(satck#) = 2*x1 + 4*x2 + 6*x2^2                              
          p(verify#) = x1 + 6*x1^2                                       
              p(c_1) = 1                                                 
              p(c_2) = 1                                                 
              p(c_3) = 4 + x1                                            
              p(c_4) = 1                                                 
              p(c_5) = 0                                                 
              p(c_6) = x1                                                
              p(c_7) = 1                                                 
              p(c_8) = 1                                                 
              p(c_9) = 0                                                 
             p(c_10) = 0                                                 
             p(c_11) = 0                                                 
             p(c_12) = x1 + x2                                           
             p(c_13) = 1                                                 
             p(c_14) = 2                                                 
             p(c_15) = 2                                                 
             p(c_16) = 6 + x1                                            
             p(c_17) = x1                                                
             p(c_18) = 1 + x1 + x2                                       
             p(c_19) = 1                                                 
        
        Following rules are strictly oriented:
        eq#(#1(x),#1(y)) = 8 + 4*x      
                         > 4 + 4*x      
                         = c_3(eq#(x,y))
        
          eq#(O(x),O(y)) = 8 + 4*x      
                         > 4*x          
                         = c_6(eq#(x,y))
        
        
        Following rules are (at-least) weakly oriented:
          member#(x,dd(y,ys)) =  8*x + 6*x*y + 6*x*ys + 5*x^2               
                              >= 6*x + 6*x*ys + 5*x^2                       
                              =  c_12(eq#(x,y),member#(x,ys))               
        
                    sat#(cnf) =  6 + 6*cnf + 6*cnf^2                        
                              >= 6 + 6*cnf + 6*cnf^2                        
                              =  c_16(satck#(cnf,guess(cnf)))               
        
           satck#(cnf,assign) =  4*assign + 6*assign^2 + 2*cnf              
                              >= assign + 6*assign^2                        
                              =  c_17(verify#(assign))                      
        
            verify#(dd(l,ls)) =  7 + 13*l + 12*l*ls + 6*l^2 + 13*ls + 6*ls^2
                              >= 1 + 2*l + 6*l*ls + 5*l^2 + ls + 6*ls^2     
                              =  c_18(member#(negate(l),ls),verify#(ls))    
        
             choice(dd(x,xs)) =  1 + x + xs                                 
                              >= x                                          
                              =  x                                          
        
             choice(dd(x,xs)) =  1 + x + xs                                 
                              >= xs                                         
                              =  choice(xs)                                 
        
        guess(dd(clause,cnf)) =  1 + clause + cnf                           
                              >= 1 + clause + cnf                           
                              =  dd(choice(clause),guess(cnf))              
        
                 guess(nil()) =  0                                          
                              >= 0                                          
                              =  nil()                                      
        
                negate(#0(x)) =  2 + x                                      
                              >= 2 + x                                      
                              =  #1(x)                                      
        
                negate(#1(x)) =  2 + x                                      
                              >= 2 + x                                      
                              =  #0(x)                                      
        
**** Step 7.b:3.a:3.a:2: Assumption WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
    + Details:
        ()

**** Step 7.b:3.a:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
            member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          2:W:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          3:W:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
             -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):3
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1
          
          4:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):5
          
          5:W:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):6
          
          6:W:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):6
             -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):3
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          4: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
          5: satck#(cnf,assign) -> c_17(verify#(assign))
          6: verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          3: member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
          1: eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
          2: eq#(O(x),O(y)) -> c_6(eq#(x,y))
**** Step 7.b:3.a:3.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

*** Step 7.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak DPs:
            eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
            eq#(O(x),O(y)) -> c_6(eq#(x,y))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
          2:S:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):7
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):6
             -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2
          
          3:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):4
             -->_2 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
          4:S:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):5
          
          5:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):5
             -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2
          
          6:W:eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):7
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):6
          
          7:W:eq#(O(x),O(y)) -> c_6(eq#(x,y))
             -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):7
             -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):6
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: eq#(O(x),O(y)) -> c_6(eq#(x,y))
          6: eq#(#1(x),#1(y)) -> c_3(eq#(x,y))
*** Step 7.b:3.b:2: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
            member#(x,dd(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#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,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/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,dd,false,nil,true,unsat}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
          2:S:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys))
             -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2
          
          3:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):4
             -->_2 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
          4:S:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):5
          
          5:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):5
             -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          member#(x,dd(y,ys)) -> c_12(member#(x,ys))
*** Step 7.b:3.b:3: Decompose WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    + Details:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          - Strict DPs:
              guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
          - Weak DPs:
              member#(x,dd(y,ys)) -> c_12(member#(x,ys))
              sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
              satck#(cnf,assign) -> c_17(verify#(assign))
              verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          - Weak TRS:
              choice(dd(x,xs)) -> x
              choice(dd(x,xs)) -> choice(xs)
              guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
              ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,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,dd,false,nil,true,unsat}
        
        Problem (S)
          - Strict DPs:
              member#(x,dd(y,ys)) -> c_12(member#(x,ys))
              sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
              satck#(cnf,assign) -> c_17(verify#(assign))
              verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          - Weak DPs:
              guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
          - Weak TRS:
              choice(dd(x,xs)) -> x
              choice(dd(x,xs)) -> choice(xs)
              guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
              ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,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,dd,false,nil,true,unsat}
**** Step 7.b:3.b:3.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
        - Weak DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
          2:W:member#(x,dd(y,ys)) -> c_12(member#(x,ys))
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):2
          
          3:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):4
          
          4:W:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):5
          
          5:W:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):2
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):5
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          4: satck#(cnf,assign) -> c_17(verify#(assign))
          5: verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          2: member#(x,dd(y,ys)) -> c_12(member#(x,ys))
**** Step 7.b:3.b:3.a:2: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
        - Weak DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
          3:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          sat#(cnf) -> c_16(guess#(cnf))
**** Step 7.b:3.b:3.a:3: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
        - Weak DPs:
            sat#(cnf) -> c_16(guess#(cnf))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
          sat#(cnf) -> c_16(guess#(cnf))
**** Step 7.b:3.b:3.a:4: PredecessorEstimationCP WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
        - Weak DPs:
            sat#(cnf) -> c_16(guess#(cnf))
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          1: guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
          
        Consider the set of all dependency pairs
          1: guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
          2: sat#(cnf) -> c_16(guess#(cnf))
        Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
        SPACE(?,?)on application of the dependency pairs
          {1}
        These cover all (indirect) predecessors of dependency pairs
          {1,2}
        their number of applications is equally bounded.
        The dependency pairs are shifted into the weak component.
***** Step 7.b:3.b:3.a:4.a:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
        - Weak DPs:
            sat#(cnf) -> c_16(guess#(cnf))
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_8) = {1},
          uargs(c_16) = {1}
        
        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) = [1]                  
                p(O) = [1]                  
           p(choice) = [8] x1 + [1]         
               p(dd) = [1] x2 + [8]         
               p(eq) = [1] x1 + [1]         
            p(false) = [0]                  
            p(guess) = [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#) = [2] x1 + [0]         
              p(if#) = [0]                  
          p(member#) = [0]                  
          p(negate#) = [0]                  
             p(sat#) = [8] x1 + [0]         
           p(satck#) = [1]                  
          p(verify#) = [1]                  
              p(c_1) = [2]                  
              p(c_2) = [1] x1 + [0]         
              p(c_3) = [8]                  
              p(c_4) = [1]                  
              p(c_5) = [2]                  
              p(c_6) = [0]                  
              p(c_7) = [1]                  
              p(c_8) = [1] x1 + [12]        
              p(c_9) = [8]                  
             p(c_10) = [1]                  
             p(c_11) = [1]                  
             p(c_12) = [1] x1 + [2]         
             p(c_13) = [1]                  
             p(c_14) = [0]                  
             p(c_15) = [4]                  
             p(c_16) = [1] x1 + [0]         
             p(c_17) = [1] x1 + [0]         
             p(c_18) = [1] x1 + [1] x2 + [0]
             p(c_19) = [2]                  
        
        Following rules are strictly oriented:
        guess#(dd(clause,cnf)) = [2] cnf + [16]  
                               > [2] cnf + [12]  
                               = c_8(guess#(cnf))
        
        
        Following rules are (at-least) weakly oriented:
        sat#(cnf) =  [8] cnf + [0]    
                  >= [2] cnf + [0]    
                  =  c_16(guess#(cnf))
        
***** Step 7.b:3.b:3.a:4.a:2: Assumption WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
            sat#(cnf) -> c_16(guess#(cnf))
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
    + Details:
        ()

***** Step 7.b:3.b:3.a:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
            sat#(cnf) -> c_16(guess#(cnf))
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
          2:W:sat#(cnf) -> c_16(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):1
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          2: sat#(cnf) -> c_16(guess#(cnf))
          1: guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
***** Step 7.b:3.b:3.a:4.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        
        - 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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

**** Step 7.b:3.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak DPs:
            guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:member#(x,dd(y,ys)) -> c_12(member#(x,ys))
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):1
          
          2:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_2 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):5
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):3
          
          3:S:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4
          
          4:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):1
          
          5:W:guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
             -->_1 guess#(dd(clause,cnf)) -> c_8(guess#(cnf)):5
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          5: guess#(dd(clause,cnf)) -> c_8(guess#(cnf))
**** Step 7.b:3.b:3.b:2: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:member#(x,dd(y,ys)) -> c_12(member#(x,ys))
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):1
          
          2:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):3
          
          3:S:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4
          
          4:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
**** Step 7.b:3.b:3.b:3: Decompose WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    + Details:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          - Strict DPs:
              member#(x,dd(y,ys)) -> c_12(member#(x,ys))
          - Weak DPs:
              sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
              satck#(cnf,assign) -> c_17(verify#(assign))
              verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          - Weak TRS:
              choice(dd(x,xs)) -> x
              choice(dd(x,xs)) -> choice(xs)
              guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
              ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
        
        Problem (S)
          - Strict DPs:
              sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
              satck#(cnf,assign) -> c_17(verify#(assign))
              verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          - Weak DPs:
              member#(x,dd(y,ys)) -> c_12(member#(x,ys))
          - Weak TRS:
              choice(dd(x,xs)) -> x
              choice(dd(x,xs)) -> choice(xs)
              guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
              ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
***** Step 7.b:3.b:3.b:3.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
        - Weak DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          1: member#(x,dd(y,ys)) -> c_12(member#(x,ys))
          
        Consider the set of all dependency pairs
          1: member#(x,dd(y,ys)) -> c_12(member#(x,ys))
          2: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
          3: satck#(cnf,assign) -> c_17(verify#(assign))
          4: verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2))
        SPACE(?,?)on application of the dependency pairs
          {1}
        These cover all (indirect) predecessors of dependency pairs
          {1,2,3}
        their number of applications is equally bounded.
        The dependency pairs are shifted into the weak component.
****** Step 7.b:3.b:3.b:3.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
        - Weak DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(c_12) = {1},
          uargs(c_16) = {1},
          uargs(c_17) = {1},
          uargs(c_18) = {1,2}
        
        Following symbols are considered usable:
          {guess,choice#,eq#,guess#,if#,member#,negate#,sat#,satck#,verify#}
        TcT has computed the following interpretation:
               p(#0) = 1 + x1                                           
               p(#1) = x1                                               
                p(O) = 0                                                
           p(choice) = x1^2                                             
               p(dd) = 1 + x2                                           
               p(eq) = 1                                                
            p(false) = 0                                                
            p(guess) = x1                                               
               p(if) = 1 + 4*x1 + 2*x2 + x2*x3 + x2^2 + x3 + 2*x3^2     
           p(member) = 1 + x1*x2 + x1^2 + x2 + x2^2                     
           p(negate) = 2*x1^2                                           
              p(nil) = 0                                                
              p(sat) = 4                                                
            p(satck) = 1 + x1 + 2*x2 + x2^2                             
             p(true) = 0                                                
            p(unsat) = 2                                                
           p(verify) = x1^2                                             
          p(choice#) = 0                                                
              p(eq#) = x1 + 4*x1*x2 + x2 + x2^2                         
           p(guess#) = 0                                                
              p(if#) = 1 + 4*x1*x2 + 4*x1*x3 + 4*x1^2 + x2 + x2^2 + 2*x3
          p(member#) = x2                                               
          p(negate#) = 1 + 2*x1^2                                       
             p(sat#) = 6 + 6*x1 + 7*x1^2                                
           p(satck#) = 3 + 4*x1 + 2*x2 + 4*x2^2                         
          p(verify#) = 2*x1 + 4*x1^2                                    
              p(c_1) = 2                                                
              p(c_2) = 0                                                
              p(c_3) = x1                                               
              p(c_4) = 0                                                
              p(c_5) = 0                                                
              p(c_6) = 1 + x1                                           
              p(c_7) = 0                                                
              p(c_8) = 1 + x1                                           
              p(c_9) = 0                                                
             p(c_10) = 0                                                
             p(c_11) = 0                                                
             p(c_12) = x1                                               
             p(c_13) = 1                                                
             p(c_14) = 2                                                
             p(c_15) = 4                                                
             p(c_16) = 3 + x1                                           
             p(c_17) = x1                                               
             p(c_18) = x1 + x2                                          
             p(c_19) = 0                                                
        
        Following rules are strictly oriented:
        member#(x,dd(y,ys)) = 1 + ys             
                            > ys                 
                            = c_12(member#(x,ys))
        
        
        Following rules are (at-least) weakly oriented:
                    sat#(cnf) =  6 + 6*cnf + 7*cnf^2                    
                              >= 6 + 6*cnf + 4*cnf^2                    
                              =  c_16(satck#(cnf,guess(cnf)))           
        
           satck#(cnf,assign) =  3 + 2*assign + 4*assign^2 + 4*cnf      
                              >= 2*assign + 4*assign^2                  
                              =  c_17(verify#(assign))                  
        
            verify#(dd(l,ls)) =  6 + 10*ls + 4*ls^2                     
                              >= 3*ls + 4*ls^2                          
                              =  c_18(member#(negate(l),ls),verify#(ls))
        
        guess(dd(clause,cnf)) =  1 + cnf                                
                              >= 1 + cnf                                
                              =  dd(choice(clause),guess(cnf))          
        
                 guess(nil()) =  0                                      
                              >= 0                                      
                              =  nil()                                  
        
****** Step 7.b:3.b:3.b:3.a:1.a:2: Assumption WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
    + Details:
        ()

****** Step 7.b:3.b:3.b:3.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:member#(x,dd(y,ys)) -> c_12(member#(x,ys))
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):1
          
          2:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):3
          
          3:W:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4
          
          4:W:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):1
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          2: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
          3: satck#(cnf,assign) -> c_17(verify#(assign))
          4: verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
          1: member#(x,dd(y,ys)) -> c_12(member#(x,ys))
****** Step 7.b:3.b:3.b:3.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

***** Step 7.b:3.b:3.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak DPs:
            member#(x,dd(y,ys)) -> c_12(member#(x,ys))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):2
          
          2:S:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):3
          
          3:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):4
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):3
          
          4:W:member#(x,dd(y,ys)) -> c_12(member#(x,ys))
             -->_1 member#(x,dd(y,ys)) -> c_12(member#(x,ys)):4
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          4: member#(x,dd(y,ys)) -> c_12(member#(x,ys))
***** Step 7.b:3.b:3.b:3.b:2: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):2
          
          2:S:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):3
          
          3:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls))
             -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):3
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          verify#(dd(l,ls)) -> c_18(verify#(ls))
***** Step 7.b:3.b:3.b:3.b:3: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          choice(dd(x,xs)) -> x
          choice(dd(x,xs)) -> choice(xs)
          guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf))
          guess(nil()) -> nil()
          sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
          satck#(cnf,assign) -> c_17(verify#(assign))
          verify#(dd(l,ls)) -> c_18(verify#(ls))
***** Step 7.b:3.b:3.b:3.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          1: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
          3: verify#(dd(l,ls)) -> c_18(verify#(ls))
          
        Consider the set of all dependency pairs
          1: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
          2: satck#(cnf,assign) -> c_17(verify#(assign))
          3: verify#(dd(l,ls)) -> c_18(verify#(ls))
        Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
        SPACE(?,?)on application of the dependency pairs
          {1,3}
        These cover all (indirect) predecessors of dependency pairs
          {1,2,3}
        their number of applications is equally bounded.
        The dependency pairs are shifted into the weak component.
****** Step 7.b:3.b:3.b:3.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_16) = {1},
          uargs(c_17) = {1},
          uargs(c_18) = {1}
        
        Following symbols are considered usable:
          {guess,choice#,eq#,guess#,if#,member#,negate#,sat#,satck#,verify#}
        TcT has computed the following interpretation:
               p(#0) = [1] x1 + [0]         
               p(#1) = [1] x1 + [0]         
                p(O) = [1] x1 + [0]         
           p(choice) = [0]                  
               p(dd) = [1] x2 + [4]         
               p(eq) = [0]                  
            p(false) = [0]                  
            p(guess) = [1] 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#) = [8] x1 + [0]         
              p(if#) = [1] x2 + [0]         
          p(member#) = [1] x2 + [1]         
          p(negate#) = [1] x1 + [0]         
             p(sat#) = [12] x1 + [14]       
           p(satck#) = [2] x1 + [4] x2 + [1]
          p(verify#) = [4] x1 + [1]         
              p(c_1) = [1]                  
              p(c_2) = [1] x1 + [0]         
              p(c_3) = [1] x1 + [2]         
              p(c_4) = [1]                  
              p(c_5) = [1]                  
              p(c_6) = [1] x1 + [8]         
              p(c_7) = [4]                  
              p(c_8) = [1] x1 + [0]         
              p(c_9) = [0]                  
             p(c_10) = [1]                  
             p(c_11) = [0]                  
             p(c_12) = [1] x1 + [0]         
             p(c_13) = [1]                  
             p(c_14) = [4]                  
             p(c_15) = [0]                  
             p(c_16) = [2] x1 + [2]         
             p(c_17) = [1] x1 + [0]         
             p(c_18) = [1] x1 + [8]         
             p(c_19) = [1]                  
        
        Following rules are strictly oriented:
                sat#(cnf) = [12] cnf + [14]             
                          > [12] cnf + [4]              
                          = c_16(satck#(cnf,guess(cnf)))
        
        verify#(dd(l,ls)) = [4] ls + [17]               
                          > [4] ls + [9]                
                          = c_18(verify#(ls))           
        
        
        Following rules are (at-least) weakly oriented:
           satck#(cnf,assign) =  [4] assign + [2] cnf + [1]   
                              >= [4] assign + [1]             
                              =  c_17(verify#(assign))        
        
        guess(dd(clause,cnf)) =  [1] cnf + [4]                
                              >= [1] cnf + [4]                
                              =  dd(choice(clause),guess(cnf))
        
                 guess(nil()) =  [0]                          
                              >= [0]                          
                              =  nil()                        
        
****** Step 7.b:3.b:3.b:3.b:4.a:2: Assumption WORST_CASE(?,O(1))
    + Considered Problem:
        - Strict DPs:
            satck#(cnf,assign) -> c_17(verify#(assign))
        - Weak DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            verify#(dd(l,ls)) -> c_18(verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
    + Details:
        ()

****** Step 7.b:3.b:3.b:3.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
            satck#(cnf,assign) -> c_17(verify#(assign))
            verify#(dd(l,ls)) -> c_18(verify#(ls))
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
             -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):2
          
          2:W:satck#(cnf,assign) -> c_17(verify#(assign))
             -->_1 verify#(dd(l,ls)) -> c_18(verify#(ls)):3
          
          3:W:verify#(dd(l,ls)) -> c_18(verify#(ls))
             -->_1 verify#(dd(l,ls)) -> c_18(verify#(ls)):3
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          1: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)))
          2: satck#(cnf,assign) -> c_17(verify#(assign))
          3: verify#(dd(l,ls)) -> c_18(verify#(ls))
****** Step 7.b:3.b:3.b:3.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            choice(dd(x,xs)) -> x
            choice(dd(x,xs)) -> choice(xs)
            guess(dd(clause,cnf)) -> dd(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,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0
            ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/1,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,dd,false,nil,true,unsat}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))