unsat
((set-logic QF_LRA)
(proof
(let (($x96 (<= (+ skoZ skoX skoY) (- (/ 14.0 9.0)))))
(let ((?x30 (- 1.0)))
(let ((?x34 (* skoY ?x30)))
(let ((?x31 (* skoX ?x30)))
(let ((?x25 (- 14.0)))
(let ((?x27 (/ ?x25 9.0)))
(let ((?x32 (+ ?x27 ?x31)))
(let ((?x35 (+ ?x32 ?x34)))
(let (($x36 (<= skoZ ?x35)))
(let ((@x98 (rewrite (= (<= skoZ (+ (- (/ 14.0 9.0)) (* (- 1.0) skoX) (* (- 1.0) skoY))) $x96))))
(let ((?x79 (* (- 1.0) skoY)))
(let ((?x68 (* (- 1.0) skoX)))
(let ((?x87 (+ (- (/ 14.0 9.0)) ?x68 ?x79)))
(let ((?x73 (+ (- (/ 14.0 9.0)) ?x68)))
(let ((?x84 (+ ?x73 ?x79)))
(let ((@x83 (trans (monotonicity (rewrite (= ?x30 (- 1.0))) (= ?x34 (* skoY (- 1.0)))) (rewrite (= (* skoY (- 1.0)) ?x79)) (= ?x34 ?x79))))
(let ((@x72 (trans (monotonicity (rewrite (= ?x30 (- 1.0))) (= ?x31 (* skoX (- 1.0)))) (rewrite (= (* skoX (- 1.0)) ?x68)) (= ?x31 ?x68))))
(let ((@x61 (trans (monotonicity (rewrite (= ?x25 (- 14.0))) (= ?x27 (/ (- 14.0) 9.0))) (rewrite (= (/ (- 14.0) 9.0) (- (/ 14.0 9.0)))) (= ?x27 (- (/ 14.0 9.0))))))
(let ((@x86 (monotonicity (monotonicity @x61 @x72 (= ?x32 ?x73)) @x83 (= ?x35 ?x84))))
(let ((@x94 (monotonicity (trans @x86 (rewrite (= ?x84 ?x87)) (= ?x35 ?x87)) (= $x36 (<= skoZ ?x87)))))
(let ((@x100 (trans @x94 @x98 (= $x36 $x96))))
(let (($x43 (<= 0.0 skoX)))
(let (($x42 (<= 0.0 skoY)))
(let (($x44 (and $x42 $x43)))
(let (($x41 (<= 0.0 skoZ)))
(let (($x45 (and $x41 $x44)))
(let (($x39 (<= skoX 1.0)))
(let (($x46 (and $x39 $x45)))
(let (($x38 (<= skoY 1.0)))
(let (($x47 (and $x38 $x46)))
(let (($x37 (<= skoZ 1.0)))
(let (($x48 (and $x37 $x47)))
(let (($x49 (and $x36 $x48)))
(let ((@x50 (asserted $x49)))
(let (($x104 (>= skoY 0.0)))
(let ((@x106 (rewrite (= $x42 $x104))))
(let ((@x168 (and-elim (and-elim (and-elim (and-elim @x50 $x48) $x47) $x46) $x45)))
(let ((@x170 (and-elim @x168 $x44)))
(let (($x107 (>= skoX 0.0)))
(let ((@x109 (rewrite (= $x43 $x107))))
(let (($x102 (>= skoZ 0.0)))
(let ((@x103 (rewrite (= $x41 $x102))))
((_ th-lemma arith farkas 1 1 1 1) (mp (and-elim @x168 $x41) @x103 $x102) (mp (and-elim @x170 $x43) @x109 $x107) (mp (and-elim @x170 $x42) @x106 $x104) (mp (and-elim @x50 $x36) @x100 $x96) false)))))))))))))))))))))))))))))))))))))))))))))

