(benchmark autogen
  :logic QF_UF
  :extrafuns ((MININT Int)
              (MAXINT Int)
              (mod Int Int Int)
              (second' Int))
  :extrapreds ((INTEGER Int)
               (NATURAL Int))
  :formula
(flet ($RV_1 (= 0 second'))
(and
  (= (~ 2147483647) MININT)
  (= MAXINT 2147483647)
  (forall (?var_1 Int) (iff (INTEGER ?var_1) (and (<= MININT ?var_1) (<= ?var_1 MAXINT))))
  (forall (?var_1 Int) (iff (NATURAL ?var_1) (and (<= 0 ?var_1) (<= ?var_1 MAXINT))))
  (not (iff (and (and (and (and (and (<= second' 59) (<= 0 second')) true) true) true) $RV_1) $RV_1)))
)
  :status unknown
)