YES

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())

max/plus interpretations on N:

  if_A(x1,x2,x3) = max{13, 12, x2, x3}
  if#_A(x1,x2,x3) = max{3, -2 + x1, 3, 9}
  true_A = 13
  true#_A = 6
  false_A = 13
  false#_A = 17
  member_A(x1,x2) = max{13, 9, 1 + x2}
  member#_A(x1,x2) = max{9, 9, -1 + x2}
  nil_A = 3
  nil#_A = 20
  cons_A(x1,x2) = max{8, 10 + x1, 10 + x2}
  cons#_A(x1,x2) = max{10, 18, 8}
  eq_A(x1,x2) = max{10, 9, 11 + x2}
  eq#_A(x1,x2) = max{0, 1, 2 + x2}
  O_A(x1) = max{1, 1 + x1}
  O#_A(x1) = max{0, 0}
  0_A(x1) = max{1, 7 + x1}
  0#_A(x1) = max{18, 19}
  1_A(x1) = max{14, x1}
  1#_A(x1) = max{19, 16}
  negate_A(x1) = max{0, 7 + x1}
  negate#_A(x1) = max{15, 4}
  choice_A(x1) = max{3, 1 + x1}
  choice#_A(x1) = max{17, 9}
  guess_A(x1) = max{1, 3 + x1}
  guess#_A(x1) = max{19, 21}
  verify_A(x1) = max{0, 13}
  verify#_A(x1) = max{5, 4 + x1}
  sat_A(x1) = max{13, 12 + x1}
  sat#_A(x1) = max{22, 22 + x1}
  satck_A(x1,x2) = max{13, 12, 9 + x2}
  satck#_A(x1,x2) = max{4, 11, 4 + x2}
  unsat_A = 13
  unsat#_A = 5

precedence:

  cons = sat > guess > nil = 0 = 1 = choice > false = O = satck > verify = unsat > member = negate > if = true > eq