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