(set-info :smt-lib-version 2.6)
(set-logic QF_LIA)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(assert (>= (* 1 x0) 0))
(assert (>= (* (- 1) x0) (- 1)))
(assert (>= (* 1 x1) 0))
(assert (>= (* (- 1) x1) (- 1)))
(assert (>= (* 1 x1) 1))
(check-sat)
(exit)