unsat
((set-logic QF_LRA)
(proof
(let ((?x77 (* (- 1.0) skoY)))
(let ((?x70 (* 10.0 skoX)))
(let ((?x78 (+ ?x70 ?x77)))
(let (($x79 (<= ?x78 0.0)))
(let ((@x72 (rewrite (= (* skoX 10.0) ?x70))))
(let ((@x75 (monotonicity @x72 (= (<= (* skoX 10.0) skoY) (<= ?x70 skoY)))))
(let ((@x83 (trans @x75 (rewrite (= (<= ?x70 skoY) $x79)) (= (<= (* skoX 10.0) skoY) $x79))))
(let ((?x25 (* skoX 10.0)))
(let (($x27 (<= ?x25 skoY)))
(let ((?x54 (/ 15707963.0 5000000.0)))
(let (($x55 (<= pi ?x54)))
(let (($x56 (not $x55)))
(let ((?x49 (/ 31415927.0 10000000.0)))
(let (($x50 (<= ?x49 pi)))
(let (($x51 (not $x50)))
(let (($x57 (and $x51 $x56)))
(let ((?x44 (/ 1.0 2.0)))
(let ((?x45 (* pi ?x44)))
(let (($x46 (<= skoY ?x45)))
(let (($x58 (and $x46 $x57)))
(let ((?x40 (/ 1.0 20.0)))
(let (($x41 (<= ?x40 skoX)))
(let (($x59 (and $x41 $x58)))
(let (($x36 (<= skoY skoX)))
(let (($x37 (not $x36)))
(let (($x60 (and $x37 $x59)))
(let (($x29 (<= skoY 0.0)))
(let (($x30 (<= skoY ?x25)))
(let (($x33 (not $x30)))
(let (($x34 (or $x33 $x29)))
(let (($x32 (not $x27)))
(let (($x35 (or $x32 $x34)))
(let (($x61 (and $x35 $x60)))
(let (($x62 (and $x30 $x61)))
(let (($x63 (and $x29 $x62)))
(let (($x64 (and $x27 $x63)))
(let (($x31 (<= 0.0 skoY)))
(let (($x65 (and $x31 $x64)))
(let ((@x66 (asserted $x65)))
(let ((@x251 (and-elim @x66 $x64)))
(let (($x124 (>= skoX (/ 1.0 20.0))))
(let ((@x126 (trans (monotonicity (rewrite (= ?x40 (/ 1.0 20.0))) (= $x41 (<= (/ 1.0 20.0) skoX))) (rewrite (= (<= (/ 1.0 20.0) skoX) $x124)) (= $x41 $x124))))
(let ((@x261 (and-elim (and-elim (and-elim (and-elim (and-elim @x251 $x63) $x62) $x61) $x60) $x59)))
((_ th-lemma arith farkas 10 1 1) (mp (and-elim @x261 $x41) @x126 $x124) (and-elim (and-elim @x251 $x63) $x29) (mp (and-elim @x251 $x27) @x83 $x79) false))))))))))))))))))))))))))))))))))))))))))))))

