(benchmark autogen
  :logic UNKNOWN
  :extrafuns ((MININT Int)
              (MAXINT Int)
              (mod Int Int Int)
              (second Int)
              (second' Int))
  :extrapreds ((INTEGER Int)
               (NATURAL Int)
               (FINSET Int)
               (NATURAL_1 Int))
  :formula
(flet ($RV_1 (and (<= second 59) (<= 0 second)))
(flet ($RV_2 (and (<= second' 59) (<= 0 second')))
(and
  (= MININT (~ 2147483647))
  (= 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))))
  (forall (?var_1 Int) (iff (NATURAL_1 ?var_1) (and (not (<= ?var_1 0)) (<= ?var_1 MAXINT))))
  (forall (?var_2 Int) (?var_1 Int) (implies
                                       (and (<= 0 ?var_1) (not (<= ?var_2 0)))
                                       (and (<= (mod ?var_1 ?var_2) 0) (not (<= ?var_2 (mod ?var_1 ?var_2))))))
  (not (iff (and (and (and (and $RV_1 true) true) (and (and (and $RV_2 true) true) true)) true) (and $RV_1 $RV_2))))
))
  :status unknown
)