unknown
(
  (define-fun x () Real (/ 1 4))
)