(benchmark ctpexam3q2v0
:status sat
:logic QF_IDL
:extrafuns ((v1 Int))
:extrafuns ((v2 Int))
:extrafuns ((v3 Int))
:extrafuns ((maior Int))
:extrafuns ((menor Int))
:extrafuns ((meio Int))
:extrafuns ((x1 Int))
:extrafuns ((x2 Int))
:extrafuns ((x3 Int))
:extrafuns ((x4 Int))
:extrafuns ((x5 Int))
:extrafuns ((x6 Int))
:formula
(not
 (implies
  (and
   (>= x1 v2)
   (>= x1 v3)
   (>= maior v1)
   (>= maior x1)
   (<= x2 v2)
   (<= x2 v3)
   (<= menor v1)
   (<= menor x2)
   (<= x3 v1)
   (<= x3 v2)
   (<= x4 v1)
   (<= x4 v3)
   (>= x5 x3)
   (>= x5 x4)
   (<= x6 v2)
   (<= x6 v3)
   (>= meio x5)
   (>= meio x6)
   )
  (and
   (>= maior v1)
   (>= maior v2)
   (>= maior v3)
   (<= menor v1)
   (<= menor v2)
   (<= menor v3)
   (<= meio maior)
   (>= meio menor))))
)