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