(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
  )