(benchmark autogen
  :logic QF_UF
  :extrafuns ((v1 Int)
              (v2 Int)
              (v3 Int)
              (maior Int)
              (menor Int)
              (meio Int)
              (x1 Int)
              (x2 Int)
              (x3 Int)
              (x4 Int)
              (x5 Int)
              (x6 Int))
  :formula
(and
  (<= v2 x1)
  (<= v3 x1)
  (<= v1 maior)
  (<= x1 maior)
  (<= x2 v2)
  (<= x2 v3)
  (<= menor v1)
  (<= menor x2)
  (<= x3 v1)
  (<= x3 v2)
  (<= x4 v1)
  (<= x4 v3)
  (<= x3 x5)
  (<= x4 x5)
  (<= x6 v2)
  (<= x6 v3)
  (<= x5 meio)
  (<= x6 meio)
  (<= v2 maior)
  (<= v3 maior)
  (<= menor v2)
  (<= menor v3)
  (not (<= meio maior)))
  :status unknown
)