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