sat
(
  (define-fun a () Bool false)
  (define-fun b () Bool false)
)