(benchmark autogen
  :logic QF_UF
  :extrafuns ((MININT Int)
              (MAXINT Int)
              (mod Int Int Int)
              (second' Int)
              (minute' Int))
  :extrapreds ((INTEGER Int)
               (NATURAL Int))
  :formula
(flet ($RV_1 (= 0 minute'))
(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')) (and (and (<= minute' 59) (<= 0 minute')) true)) true)
          true)
        (and (= minute' second') $RV_1))
      (and (= 0 second') $RV_1))))
)
  :status unknown
)