(benchmark gasburner_prop3_1.smt
  :source {
SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
Sorea, and Leonardo de Moura.  Contact demoura@csl.sri.com for more
information.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status unsat
:category { industrial }
:difficulty { 0 }
  :logic QF_LRA
  
  :extrapreds ((x_0))
  :extrafuns ((x_1 Real))
  :extrafuns ((x_2 Real))
  :extrafuns ((x_3 Real))
  :extrafuns ((x_4 Real))
  :extrapreds ((x_5))
  :extrafuns ((x_6 Real))
  :extrafuns ((x_7 Real))
  :extrafuns ((x_8 Real))
  :extrapreds ((x_9))
  :formula
(let (?cvcl_5 0) (let (?cvcl_7 0) (let (?cvcl_9 0) (flet ($cvcl_0 (not x_0)) (flet ($cvcl_8 $cvcl_0) (flet ($cvcl_2 (= x_1 0)) (let (?cvcl_6 (+ ?cvcl_5 x_2)) (flet ($cvcl_4 (= x_3 ?cvcl_9)) (flet ($cvcl_3 (= x_4 ?cvcl_7)) (flet ($cvcl_1 (not x_5)) (and (and (and (and (and (and (<= x_7 1) (>= x_7 0)) $cvcl_0) (not (< x_6 0))) (= x_7 (ite x_5 0 1))) (or (or (and (and (and (and (and (and (= x_8 0) $cvcl_1) $cvcl_8) x_9) $cvcl_2) $cvcl_3) $cvcl_4)  (and (and (and (and (and (and (and (= x_8 1) $cvcl_1) x_0) (not (< ?cvcl_5 30))) (not x_9)) $cvcl_2) $cvcl_3) $cvcl_4) )  (and (and (and (and (and (and (and (= x_8 2) x_5) (not (< x_2 0))) (or x_0  (<= ?cvcl_6 1) )) (= x_1 ?cvcl_6)) (= x_4 (+ ?cvcl_7 x_2))) (= x_3 (ite $cvcl_8 (+ ?cvcl_9 x_2) ?cvcl_9))) (iff x_9 x_0)) )) (or (and (not (< x_4 60)) (not (<= (* x_3 20) x_4)))  (and (not (< ?cvcl_7 60)) (not (<= (* ?cvcl_9 20) ?cvcl_7))) ))))))))))))
)