We consider the following Problem:

  Strict Trs:
    {  if(true(), t, e) -> t
     , if(false(), t, e) -> e
     , member(x, nil()) -> false()
     , member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys))
     , eq(nil(), nil()) -> true()
     , eq(O(x), 0(y)) -> eq(x, y)
     , eq(0(x), 1(y)) -> false()
     , eq(1(x), 0(y)) -> false()
     , eq(1(x), 1(y)) -> eq(x, y)
     , negate(0(x)) -> 1(x)
     , negate(1(x)) -> 0(x)
     , choice(cons(x, xs)) -> x
     , choice(cons(x, xs)) -> choice(xs)
     , guess(nil()) -> nil()
     , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf))
     , verify(nil()) -> true()
     , verify(cons(l, ls)) ->
       if(member(negate(l), ls), false(), verify(ls))
     , sat(cnf) -> satck(cnf, guess(cnf))
     , satck(cnf, assign) -> if(verify(assign), assign, unsat())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {  if(true(), t, e) -> t
       , if(false(), t, e) -> e
       , member(x, nil()) -> false()
       , member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys))
       , eq(nil(), nil()) -> true()
       , eq(O(x), 0(y)) -> eq(x, y)
       , eq(0(x), 1(y)) -> false()
       , eq(1(x), 0(y)) -> false()
       , eq(1(x), 1(y)) -> eq(x, y)
       , negate(0(x)) -> 1(x)
       , negate(1(x)) -> 0(x)
       , choice(cons(x, xs)) -> x
       , choice(cons(x, xs)) -> choice(xs)
       , guess(nil()) -> nil()
       , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf))
       , verify(nil()) -> true()
       , verify(cons(l, ls)) ->
         if(member(negate(l), ls), false(), verify(ls))
       , sat(cnf) -> satck(cnf, guess(cnf))
       , satck(cnf, assign) -> if(verify(assign), assign, unsat())}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^2))
  
  Proof:
    We consider the following Problem:
    
      Strict Trs:
        {  if(true(), t, e) -> t
         , if(false(), t, e) -> e
         , member(x, nil()) -> false()
         , member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys))
         , eq(nil(), nil()) -> true()
         , eq(O(x), 0(y)) -> eq(x, y)
         , eq(0(x), 1(y)) -> false()
         , eq(1(x), 0(y)) -> false()
         , eq(1(x), 1(y)) -> eq(x, y)
         , negate(0(x)) -> 1(x)
         , negate(1(x)) -> 0(x)
         , choice(cons(x, xs)) -> x
         , choice(cons(x, xs)) -> choice(xs)
         , guess(nil()) -> nil()
         , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf))
         , verify(nil()) -> true()
         , verify(cons(l, ls)) ->
           if(member(negate(l), ls), false(), verify(ls))
         , sat(cnf) -> satck(cnf, guess(cnf))
         , satck(cnf, assign) -> if(verify(assign), assign, unsat())}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^2))
    
    Proof:
      The following argument positions are usable:
        Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(cons) = {1, 2},
        Uargs(eq) = {}, Uargs(O) = {}, Uargs(0) = {}, Uargs(1) = {},
        Uargs(negate) = {}, Uargs(choice) = {}, Uargs(guess) = {},
        Uargs(verify) = {}, Uargs(sat) = {}, Uargs(satck) = {2}
      We have the following constructor-based EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
      Interpretation Functions:
       if(x1, x2, x3) = [1 0 0] x1 + [1 0 0] x2 + [1 0 0] x3 + [0]
                        [0 0 0]      [0 1 0]      [0 1 0]      [0]
                        [0 0 0]      [0 0 1]      [0 0 1]      [0]
       true() = [1]
                [0]
                [0]
       false() = [1]
                 [0]
                 [0]
       member(x1, x2) = [2 0 0] x1 + [0 1 0] x2 + [0]
                        [1 2 1]      [0 0 0]      [0]
                        [2 0 0]      [0 0 0]      [0]
       nil() = [2]
               [2]
               [0]
       cons(x1, x2) = [1 2 0] x1 + [1 2 0] x2 + [2]
                      [0 1 0]      [0 1 0]      [2]
                      [0 0 1]      [0 0 1]      [0]
       eq(x1, x2) = [0 0 0] x1 + [0 1 0] x2 + [0]
                    [0 0 0]      [0 0 2]      [0]
                    [0 0 0]      [0 0 0]      [0]
       O(x1) = [0 0 0] x1 + [0]
               [0 0 0]      [0]
               [0 0 0]      [0]
       0(x1) = [0 0 0] x1 + [0]
               [0 1 0]      [2]
               [0 0 1]      [2]
       1(x1) = [0 0 0] x1 + [0]
               [0 1 0]      [2]
               [0 0 1]      [0]
       negate(x1) = [0 1 0] x1 + [0]
                    [0 1 0]      [2]
                    [0 0 1]      [2]
       choice(x1) = [1 0 0] x1 + [0]
                    [0 1 0]      [0]
                    [0 0 1]      [0]
       guess(x1) = [1 1 0] x1 + [0]
                   [0 1 0]      [0]
                   [0 0 1]      [0]
       verify(x1) = [1 0 0] x1 + [0]
                    [0 0 0]      [0]
                    [0 0 0]      [0]
       sat(x1) = [2 2 0] x1 + [2]
                 [2 1 1]      [2]
                 [0 1 2]      [2]
       satck(x1, x2) = [0 0 0] x1 + [2 0 0] x2 + [1]
                       [1 0 1]      [0 1 0]      [1]
                       [0 1 0]      [0 0 1]      [1]
       unsat() = [0]
                 [0]
                 [0]

Hurray, we answered YES(?,O(n^2))