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