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{0, x1, x2, x3}
  if#_A(x1,x2,x3) = max{0, x1, x2, x3}
  true_A = 0
  true#_A = 0
  false_A = 0
  false#_A = 0
  member_A(x1,x2) = max{0, x1, x2}
  member#_A(x1,x2) = max{0, x1, x2}
  nil_A = 0
  nil#_A = 0
  cons_A(x1,x2) = max{0, x1, x2}
  cons#_A(x1,x2) = max{0, x1, x2}
  eq_A(x1,x2) = max{0, x1, x2}
  eq#_A(x1,x2) = max{0, x1, x2}
  O_A(x1) = max{0, x1}
  O#_A(x1) = max{0, x1}
  0_A(x1) = max{0, x1}
  0#_A(x1) = max{0, x1}
  1_A(x1) = max{0, x1}
  1#_A(x1) = max{0, x1}
  negate_A(x1) = max{0, x1}
  negate#_A(x1) = max{0, x1}
  choice_A(x1) = max{0, x1}
  choice#_A(x1) = max{0, x1}
  guess_A(x1) = max{0, x1}
  guess#_A(x1) = max{0, x1}
  verify_A(x1) = max{0, x1}
  verify#_A(x1) = max{0, x1}
  sat_A(x1) = max{0, x1}
  sat#_A(x1) = max{0, x1}
  satck_A(x1,x2) = max{0, x1, x2}
  satck#_A(x1,x2) = max{0, x1, x2}
  unsat_A = 0
  unsat#_A = 0

precedence:

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