path: root/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt

(benchmark clock_synchro
  :source { Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) }
  :status unsat
  :category { industrial }
  :difficulty { 0 }
  :logic QF_LRA
  
  :extrafuns ((x_0 Real))
  :extrafuns ((x_1 Real))
  :extrafuns ((x_2 Real))
  :extrafuns ((x_3 Real))
  :extrafuns ((x_4 Real))
  :extrafuns ((x_5 Real))
  :extrafuns ((x_6 Real))
  :extrafuns ((x_7 Real))
  :extrafuns ((x_8 Real))
  :extrafuns ((x_9 Real))
  :extrafuns ((x_10 Real))
  :extrafuns ((x_11 Real))
  :extrafuns ((x_12 Real))
  :extrafuns ((x_13 Real))
  :extrafuns ((x_14 Real))
  :extrafuns ((x_15 Real))
  :extrafuns ((x_16 Real))
  :extrafuns ((x_17 Real))
  :extrafuns ((x_18 Real))
  :extrafuns ((x_19 Real))
  :extrafuns ((x_20 Real))
  :extrafuns ((x_21 Real))
  :extrafuns ((x_22 Real))
  :extrafuns ((x_23 Real))
  :extrafuns ((x_24 Real))
  :extrafuns ((x_25 Real))
  :extrafuns ((x_26 Real))
  :extrafuns ((x_27 Real))
  :extrafuns ((x_28 Real))
  :extrafuns ((x_29 Real))
  :extrafuns ((x_30 Real))
  :extrafuns ((x_31 Real))
  :extrafuns ((x_32 Real))
  :extrafuns ((x_33 Real))
  :extrafuns ((x_34 Real))
  :extrafuns ((x_35 Real))
  :extrafuns ((x_36 Real))
  :extrafuns ((x_37 Real))
  :extrafuns ((x_38 Real))
  :extrafuns ((x_39 Real))
  :extrafuns ((x_40 Real))
  :extrafuns ((x_41 Real))
  :extrafuns ((x_42 Real))
  :extrafuns ((x_43 Real))
  :extrafuns ((x_44 Real))
  :extrafuns ((x_45 Real))
  :extrafuns ((x_46 Real))
  :extrafuns ((x_47 Real))
  :extrafuns ((x_48 Real))
  :extrafuns ((x_49 Real))
  :extrafuns ((x_50 Real))
  :extrafuns ((x_51 Real))
  :extrafuns ((x_52 Real))
  :extrafuns ((x_53 Real))
  :extrafuns ((x_54 Real))
  :extrafuns ((x_55 Real))
  :extrafuns ((x_56 Real))
  :extrafuns ((x_57 Real))
  :extrafuns ((x_58 Real))
  :extrafuns ((x_59 Real))
  :extrafuns ((x_60 Real))
  :extrafuns ((x_61 Real))
  :extrafuns ((x_62 Real))
  :extrafuns ((x_63 Real))
  :extrafuns ((x_64 Real))
  :extrafuns ((x_65 Real))
  :extrafuns ((x_66 Real))
  :extrafuns ((x_67 Real))
  :extrafuns ((x_68 Real))
  :extrafuns ((x_69 Real))
  :extrafuns ((x_70 Real))
  :extrafuns ((x_71 Real))
  :extrafuns ((x_72 Real))
  :extrafuns ((x_73 Real))
  :extrafuns ((x_74 Real))
  :extrafuns ((x_75 Real))
  :extrafuns ((x_76 Real))
  :extrafuns ((x_77 Real))
  :extrafuns ((x_78 Real))
  :extrafuns ((x_79 Real))
  :extrafuns ((x_80 Real))
  :extrafuns ((x_81 Real))
  :extrafuns ((x_82 Real))
  :extrafuns ((x_83 Real))
  :extrafuns ((x_84 Real))

:assumption (=x_76 1)
:assumption (=x_76 1)
:assumption (=x_0 0)
:assumption (=x_0 0)
:assumption (not (<= x_6 0))
:assumption (not (<= x_7 0))
:assumption (=x_70 1)
:assumption (=x_70 1)
:assumption (=x_75 1)
:assumption (=x_75 1)
:assumption (=x_69 1)
:assumption (=x_69 1)
:assumption (=x_74 1)
:assumption (=x_74 1)
:assumption (=x_68 1)
:assumption (=x_68 1)
:assumption (=x_38 1)
:assumption (=x_38 1)
:assumption (not (<= x_44 0))
:assumption (=x_73 1)
:assumption (=x_73 1)
:assumption (=x_67 1)
:assumption (=x_67 1)
:assumption (=x_72 1)
:assumption (=x_72 1)
:assumption (=x_66 1)
:assumption (=x_66 1)
:assumption (=x_65 1)
:assumption (=x_65 1)
:assumption (=x_60 1)
:assumption (=x_60 1)
:assumption (=x_64 1)
:assumption (=x_64 1)
:assumption (=x_55 1)
:assumption (=x_55 1)
:assumption (=x_63 1)
:assumption (=x_63 1)
:assumption (=x_36 1)
:assumption (=x_36 1)
:assumption (=x_50 1)
:assumption (=x_50 1)
:assumption (=x_62 1)
:assumption (=x_62 1)
:assumption (=x_35 1)
:assumption (=x_35 1)
:assumption (=x_61 1)
:assumption (=x_61 1)
:assumption (=x_34 1)
:assumption (=x_34 1)
:assumption (=x_59 1)
:assumption (=x_59 1)
:assumption (=x_40 1)
:assumption (=x_40 1)
:assumption (=x_54 1)
:assumption (=x_54 1)
:assumption (not (<= x_84 0))
:assumption (=x_58 1)
:assumption (=x_58 1)
:assumption (=x_49 1)
:assumption (=x_49 1)
:assumption (=x_57 1)
:assumption (=x_57 1)
:assumption (=x_56 1)
:assumption (=x_56 1)
:assumption (>= x_82 0)
:assumption (=x_53 1)
:assumption (=x_53 1)
:assumption (=x_48 1)
:assumption (=x_48 1)
:assumption (=x_52 1)
:assumption (=x_52 1)
:assumption (=x_51 1)
:assumption (=x_51 1)
:assumption (=x_47 1)
:assumption (=x_47 1)
:assumption (=x_46 1)
:assumption (=x_46 1)
:assumption (=x_14 0)
:assumption (=x_14 0)
:assumption (=x_28 0)
:assumption (=x_28 0)
:assumption (=x_25 0)
:assumption (=x_25 0)
:assumption (=x_22 0)
:assumption (=x_22 0)
:assumption (=x_19 0)
:assumption (=x_19 0)
:assumption (=x_15 0)
:assumption (=x_15 0)
:assumption (=x_27 0)
:assumption (=x_27 0)
:assumption (=x_24 0)
:assumption (=x_24 0)
:assumption (=x_21 0)
:assumption (=x_21 0)
:assumption (=x_18 0)
:assumption (=x_18 0)
:assumption (=x_16 0)
:assumption (=x_16 0)
:assumption (=x_26 0)
:assumption (=x_26 0)
:assumption (=x_23 0)
:assumption (=x_23 0)
:assumption (=x_20 0)
:assumption (=x_20 0)
:assumption (=x_17 0)
:assumption (=x_17 0)
:assumption (=x_33 0)
:assumption (=x_33 0)
:assumption (=x_32 0)
:assumption (=x_32 0)
:assumption (=x_31 0)
:assumption (=x_31 0)
:assumption (=x_30 0)
:assumption (=x_30 0)
:assumption (=x_29 0)
:assumption (=x_29 0)
:assumption (<= (+ x_13 (* (~ 1) x_73) (* (~ 1) x_83)) 0)
:assumption (<= (+ x_13 (* (~ 1) x_72) (* (~ 1) x_83)) 0)
:assumption (<= (+ x_13 (* (~ 1) x_74) (* (~ 1) x_83)) 0)
:assumption (<= (+ x_13 (* (~ 1) x_75) (* (~ 1) x_83)) 0)
:assumption (<= (+ x_13 (* (~ 1) x_76) (* (~ 1) x_83)) 0)
:assumption (>= (+ x_13 (* (~ 1) x_72) (* (~ 1) x_84)) 0)
:assumption (>= (+ x_13 (* (~ 1) x_73) (* (~ 1) x_84)) 0)
:assumption (>= (+ x_13 (* (~ 1) x_74) (* (~ 1) x_84)) 0)
:assumption (>= (+ x_13 (* (~ 1) x_75) (* (~ 1) x_84)) 0)
:assumption (>= (+ x_13 (* (~ 1) x_76) (* (~ 1) x_84)) 0)
:assumption (>= (+ x_72 (* (~ 1) x_73) x_82) 0)
:assumption (>= (+ x_72 (* (~ 1) x_74) x_82) 0)
:assumption (>= (+ x_72 (* (~ 1) x_75) x_82) 0)
:assumption (>= (+ x_72 (* (~ 1) x_76) x_82) 0)
:assumption (<= (+ x_72 (* (~ 1) x_73) (* (~ 1) x_82)) 0)
:assumption (>= (+ x_73 (* (~ 1) x_74) x_82) 0)
:assumption (>= (+ x_73 (* (~ 1) x_75) x_82) 0)
:assumption (>= (+ x_73 (* (~ 1) x_76) x_82) 0)
:assumption (<= (+ x_72 (* (~ 1) x_74) (* (~ 1) x_82)) 0)
:assumption (<= (+ x_73 (* (~ 1) x_74) (* (~ 1) x_82)) 0)
:assumption (>= (+ x_74 (* (~ 1) x_75) x_82) 0)
:assumption (>= (+ x_74 (* (~ 1) x_76) x_82) 0)
:assumption (<= (+ x_72 (* (~ 1) x_75) (* (~ 1) x_82)) 0)
:assumption (<= (+ x_73 (* (~ 1) x_75) (* (~ 1) x_82)) 0)
:assumption (<= (+ x_74 (* (~ 1) x_75) (* (~ 1) x_82)) 0)
:assumption (>= (+ x_75 (* (~ 1) x_76) x_82) 0)
:assumption (<= (+ x_72 (* (~ 1) x_76) (* (~ 1) x_82)) 0)
:assumption (<= (+ x_73 (* (~ 1) x_76) (* (~ 1) x_82)) 0)
:assumption (<= (+ x_74 (* (~ 1) x_76) (* (~ 1) x_82)) 0)
:assumption (>= (+ x_7 x_13 (* (~ 1) x_40)) 0)
:assumption (<= (+ x_75 (* (~ 1) x_76) (* (~ 1) x_82)) 0)
:assumption (>= (+ x_7 x_13 (* (~ 1) x_34)) 0)
:assumption (>= (+ x_9 (* (~ 1) x_13)) 0)
:assumption (<= (+ x_9 (* (~ 1) x_13)) 0)
:assumption (>= (+ x_7 x_13 (* (~ 1) x_35)) 0)
:assumption (>= (+ x_7 x_13 (* (~ 1) x_36)) 0)
:assumption (>= (+ x_11 (* (~ 1) x_13)) 0)
:assumption (<= (+ x_11 (* (~ 1) x_13)) 0)
:assumption (>= (+ x_7 x_13 (* (~ 1) x_38)) 0)
:assumption (<= (+ x_39 (* (~ (/ 1001 1000)) x_40) (* (/ 1001 1000) x_72) (* (~ 1) x_77)) 0)
:assumption (>= (+ x_39 (* (~ (/ 999 1000)) x_40) (* (/ 999 1000) x_72) (* (~ 1) x_77)) 0)
:assumption (>= (+ x_34 (* (~ (/ 1000 1001)) x_41) (* (~ 1) x_73) (* (/ 1000 1001) x_78)) 0)
:assumption (<= (+ x_34 (* (~ (/ 1000 999)) x_41) (* (~ 1) x_73) (* (/ 1000 999) x_78)) 0)
:assumption (>= (+ x_35 (* (~ (/ 1000 1001)) x_42) (* (~ 1) x_74) (* (/ 1000 1001) x_79)) 0)
:assumption (<= (+ x_35 (* (~ (/ 1000 999)) x_42) (* (~ 1) x_74) (* (/ 1000 999) x_79)) 0)
:assumption (>= (+ x_36 (* (~ (/ 1000 1001)) x_43) (* (~ 1) x_75) (* (/ 1000 1001) x_80)) 0)
:assumption (<= (+ x_36 (* (~ (/ 1000 999)) x_43) (* (~ 1) x_75) (* (/ 1000 999) x_80)) 0)
:assumption (>= (+ x_13 (* (~ (/ 1000 999)) x_19) (* (/ 1000 999) x_39) (* (~ 1) x_40)) 0)
:assumption (<= (+ x_19 (* (~ 1) x_45)) 0)
:assumption (<= (+ x_37 (* (~ (/ 1001 1000)) x_38) (* (/ 1001 1000) x_76) (* (~ 1) x_81)) 0)
:assumption (>= (+ x_37 (* (~ (/ 999 1000)) x_38) (* (/ 999 1000) x_76) (* (~ 1) x_81)) 0)
:assumption (>= (+ x_13 (* (~ (/ 1000 999)) x_22) (* (~ 1) x_34) (* (/ 1000 999) x_41)) 0)
:assumption (<= (+ x_22 (* (~ 1) x_45)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 1001)) x_19) (* (/ 1000 1001) x_39) (* (~ 1) x_40)) 0))
:assumption (>= (+ x_13 (* (~ 1) x_40)) 0)
:assumption (>= (+ x_13 (* (~ (/ 1000 999)) x_25) (* (~ 1) x_35) (* (/ 1000 999) x_42)) 0)
:assumption (<= (+ x_25 (* (~ 1) x_45)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 1001)) x_22) (* (~ 1) x_34) (* (/ 1000 1001) x_41)) 0))
:assumption (>= (+ x_13 (* (~ 1) x_34)) 0)
:assumption (>= (+ x_13 (* (~ (/ 1000 999)) x_28) (* (~ 1) x_36) (* (/ 1000 999) x_43)) 0)
:assumption (<= (+ x_28 (* (~ 1) x_45)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 1001)) x_25) (* (~ 1) x_35) (* (/ 1000 1001) x_42)) 0))
:assumption (>= (+ x_13 (* (~ 1) x_35)) 0)
:assumption (>= (+ x_13 (* (~ (/ 1000 999)) x_14) (* (/ 1000 999) x_37) (* (~ 1) x_38)) 0)
:assumption (<= (+ x_14 (* (~ 1) x_45)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 1001)) x_28) (* (~ 1) x_36) (* (/ 1000 1001) x_43)) 0))
:assumption (>= (+ x_13 (* (~ 1) x_36)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 1001)) x_14) (* (/ 1000 1001) x_37) (* (~ 1) x_38)) 0))
:assumption (>= (+ x_13 (* (~ 1) x_38)) 0)
:assumption (<= (+ x_19 (* (~ (/ 1001 1000)) x_29) (* (~ (/ 1001 1000)) x_44) (* (/ 1001 2000) x_72) (* (/ 1001 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (/ 1001 2000))
:assumption (>= (+ x_19 (* (~ (/ 999 1000)) x_29) (* (/ 999 1000) x_44) (* (/ 999 2000) x_72) (* (/ 999 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (~ (/ 3001 2000)))
:assumption (<= (+ x_22 (* (~ (/ 1001 1000)) x_30) (* (~ (/ 1001 1000)) x_44) (* (/ 1001 2000) x_72) (* (/ 1001 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (/ 1001 2000))
:assumption (>= (+ x_22 (* (~ (/ 999 1000)) x_30) (* (/ 999 1000) x_44) (* (/ 999 2000) x_72) (* (/ 999 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (~ (/ 3001 2000)))
:assumption (<= (+ x_25 (* (~ (/ 1001 1000)) x_31) (* (~ (/ 1001 1000)) x_44) (* (/ 1001 2000) x_72) (* (/ 1001 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (/ 1001 2000))
:assumption (>= (+ x_25 (* (~ (/ 999 1000)) x_31) (* (/ 999 1000) x_44) (* (/ 999 2000) x_72) (* (/ 999 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (~ (/ 3001 2000)))
:assumption (>= (+ x_0 (* (~ 1) x_21)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_21)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_22)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_22)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_18)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_18)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_19)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_19)) 0)
:assumption (<= (+ x_28 (* (~ (/ 1001 1000)) x_32) (* (~ (/ 1001 1000)) x_44) (* (/ 1001 2000) x_72) (* (/ 1001 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (/ 1001 2000))
:assumption (>= (+ x_28 (* (~ (/ 999 1000)) x_32) (* (/ 999 1000) x_44) (* (/ 999 2000) x_72) (* (/ 999 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (~ (/ 3001 2000)))
:assumption (>= (+ x_0 (* (~ 1) x_24)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_24)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_25)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_25)) 0)
:assumption (>= (+ x_20 (* (~ 1) x_34)) (~ 1))
:assumption (<= (+ x_20 (* (~ 1) x_34)) (~ 1))
:assumption (=(+ x_6 (* (~ 1) x_9)) 0)
:assumption (=(+ x_6 (* (~ 1) x_9)) 0)
:assumption (>= (+ x_17 (* (~ 1) x_40)) (~ 1))
:assumption (<= (+ x_17 (* (~ 1) x_40)) (~ 1))
:assumption (=(+ x_6 (* (~ 1) x_8)) 0)
:assumption (=(+ x_6 (* (~ 1) x_8)) 0)
:assumption (<= (+ x_14 (* (~ (/ 1001 1000)) x_33) (* (~ (/ 1001 1000)) x_44) (* (/ 1001 2000) x_72) (* (/ 1001 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (/ 1001 2000))
:assumption (>= (+ x_14 (* (~ (/ 999 1000)) x_33) (* (/ 999 1000) x_44) (* (/ 999 2000) x_72) (* (/ 999 2000) x_76) (* (~ (/ 1 2)) x_77) (* (~ (/ 1 2)) x_81)) (~ (/ 3001 2000)))
:assumption (>= (+ x_0 (* (~ 1) x_27)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_27)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_28)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_28)) 0)
:assumption (>= (+ x_23 (* (~ 1) x_35)) (~ 1))
:assumption (<= (+ x_23 (* (~ 1) x_35)) (~ 1))
:assumption (=(+ x_6 (* (~ 1) x_10)) 0)
:assumption (=(+ x_6 (* (~ 1) x_10)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_41)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_41)) (~ (/ 999 1000)))
:assumption (>= (+ x_0 (* (~ 1) x_2)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_2)) (~ (/ 999 1000)))
:assumption (>= (+ x_0 (* (~ 1) x_39)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_39)) (~ (/ 999 1000)))
:assumption (>= (+ x_0 (* (~ 1) x_1)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_1)) (~ (/ 999 1000)))
:assumption (>= (+ x_13 (* (~ (/ 1000 1001)) x_19) (* (~ 1) x_72) (* (/ 1000 1001) x_77)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 999)) x_19) (* (~ 1) x_72) (* (/ 1000 999) x_77)) 0))
:assumption (>= (+ x_0 (* (~ 1) x_15)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_15)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_14)) 0)
:assumption (<= (+ x_0 (* (~ 1) x_14)) 0)
:assumption (>= (+ x_26 (* (~ 1) x_36)) (~ 1))
:assumption (<= (+ x_26 (* (~ 1) x_36)) (~ 1))
:assumption (=(+ x_6 (* (~ 1) x_11)) 0)
:assumption (=(+ x_6 (* (~ 1) x_11)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_42)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_42)) (~ (/ 999 1000)))
:assumption (>= (+ x_0 (* (~ 1) x_3)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_3)) (~ (/ 999 1000)))
:assumption (>= (+ x_13 (* (~ (/ 1000 1001)) x_22) (* (~ 1) x_73) (* (/ 1000 1001) x_78)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 999)) x_22) (* (~ 1) x_73) (* (/ 1000 999) x_78)) 0))
:assumption (>= (+ x_16 (* (~ 1) x_38)) (~ 1))
:assumption (<= (+ x_16 (* (~ 1) x_38)) (~ 1))
:assumption (=(+ x_6 (* (~ 1) x_12)) 0)
:assumption (=(+ x_6 (* (~ 1) x_12)) 0)
:assumption (>= (+ x_0 (* (~ 1) x_43)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_43)) (~ (/ 999 1000)))
:assumption (>= (+ x_0 (* (~ 1) x_4)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_4)) (~ (/ 999 1000)))
:assumption (>= (+ x_13 (* (~ (/ 1000 1001)) x_25) (* (~ 1) x_74) (* (/ 1000 1001) x_79)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 999)) x_25) (* (~ 1) x_74) (* (/ 1000 999) x_79)) 0))
:assumption (>= (+ x_0 (* (~ 1) x_37)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_37)) (~ (/ 999 1000)))
:assumption (>= (+ x_0 (* (~ 1) x_5)) (~ (/ 1001 1000)))
:assumption (<= (+ x_0 (* (~ 1) x_5)) (~ (/ 999 1000)))
:assumption (>= (+ x_13 (* (~ (/ 1000 1001)) x_28) (* (~ 1) x_75) (* (/ 1000 1001) x_80)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 999)) x_28) (* (~ 1) x_75) (* (/ 1000 999) x_80)) 0))
:assumption (=(+ x_1 (* (~ 1) x_39)) 0)
:assumption (=(+ x_1 (* (~ 1) x_39)) 0)
:assumption (=(+ x_2 (* (~ 1) x_41)) 0)
:assumption (=(+ x_2 (* (~ 1) x_41)) 0)
:assumption (>= (+ x_13 (* (~ (/ 1000 1001)) x_14) (* (~ 1) x_76) (* (/ 1000 1001) x_81)) 0)
:assumption (not (<= (+ x_13 (* (~ (/ 1000 999)) x_14) (* (~ 1) x_76) (* (/ 1000 999) x_81)) 0))
:assumption (>= (+ x_7 (* (~ (/ 1000 1001)) x_18) (* (/ 1000 1001) x_19)) 0)
:assumption (not (<= (+ x_7 (* (~ (/ 1000 999)) x_18) (* (/ 1000 999) x_19)) 0))
:assumption (=(+ x_3 (* (~ 1) x_42)) 0)
:assumption (=(+ x_3 (* (~ 1) x_42)) 0)
:assumption (>= (+ x_7 (* (~ (/ 1000 1001)) x_21) (* (/ 1000 1001) x_22)) 0)
:assumption (not (<= (+ x_7 (* (~ (/ 1000 999)) x_21) (* (/ 1000 999) x_22)) 0))
:assumption (>= (+ x_7 (* (~ (/ 1000 1001)) x_24) (* (/ 1000 1001) x_25)) 0)
:assumption (not (<= (+ x_7 (* (~ (/ 1000 999)) x_24) (* (/ 1000 999) x_25)) 0))
:assumption (>= (+ x_7 (* (~ (/ 1000 1001)) x_27) (* (/ 1000 1001) x_28)) 0)
:assumption (not (<= (+ x_7 (* (~ (/ 1000 999)) x_27) (* (/ 1000 999) x_28)) 0))
:assumption (>= (+ x_7 (* (/ 1000 1001) x_14) (* (~ (/ 1000 1001)) x_15)) 0)
:assumption (not (<= (+ x_7 (* (/ 1000 999) x_14) (* (~ (/ 1000 999)) x_15)) 0))
:assumption (<= (+ x_0 x_6 (* (~ 1) x_83)) 1)
:assumption (=(+ x_4 (* (~ 1) x_43)) 0)
:assumption (=(+ x_4 (* (~ 1) x_43)) 0)
:assumption (not (>= (+ x_0 (* (~ 1) x_45)) 0))
:assumption (not (<= (+ x_1 (* (~ 1) x_45)) 0))
:assumption (not (<= (+ x_2 (* (~ 1) x_45)) 0))
:assumption (>= (+ x_0 x_6 (* (~ 1) x_84)) 1)
:assumption (not (<= (+ x_3 (* (~ 1) x_45)) 0))
:assumption (=(+ x_4 (* (~ 1) x_45)) 0)
:assumption (=(+ x_4 (* (~ 1) x_45)) 0)
:assumption (=(+ x_5 (* (~ 1) x_37)) 0)
:assumption (=(+ x_5 (* (~ 1) x_37)) 0)
:assumption (>= (+ x_5 (* (~ 1) x_45)) 0)
:assumption (<= (+ x_40 (* (~ 1) x_44) (* (~ 1) x_46)) 0)
:assumption (<= (+ x_40 (* (~ 1) x_44) (* (~ 1) x_51)) 0)
:assumption (<= (+ x_40 (* (~ 1) x_44) (* (~ 1) x_56)) 0)
:assumption (<= (+ x_40 (* (~ 1) x_44) (* (~ 1) x_61)) 0)
:assumption (<= (+ x_40 (* (~ 1) x_44) (* (~ 1) x_66)) 0)
:assumption (<= (+ x_34 (* (~ 1) x_44) (* (~ 1) x_47)) 0)
:assumption (<= (+ x_34 (* (~ 1) x_44) (* (~ 1) x_52)) 0)
:assumption (<= (+ x_34 (* (~ 1) x_44) (* (~ 1) x_57)) 0)
:assumption (<= (+ x_34 (* (~ 1) x_44) (* (~ 1) x_62)) 0)
:assumption (<= (+ x_34 (* (~ 1) x_44) (* (~ 1) x_67)) 0)
:assumption (<= (+ x_35 (* (~ 1) x_44) (* (~ 1) x_48)) 0)
:assumption (<= (+ x_35 (* (~ 1) x_44) (* (~ 1) x_53)) 0)
:assumption (<= (+ x_35 (* (~ 1) x_44) (* (~ 1) x_58)) 0)
:assumption (<= (+ x_35 (* (~ 1) x_44) (* (~ 1) x_63)) 0)
:assumption (<= (+ x_35 (* (~ 1) x_44) (* (~ 1) x_68)) 0)
:assumption (>= (+ x_0 x_6 x_7) 1)
:assumption (<= (+ x_36 (* (~ 1) x_44) (* (~ 1) x_49)) 0)
:assumption (<= (+ x_36 (* (~ 1) x_44) (* (~ 1) x_54)) 0)
:assumption (<= (+ x_36 (* (~ 1) x_44) (* (~ 1) x_59)) 0)
:assumption (<= (+ x_36 (* (~ 1) x_44) (* (~ 1) x_64)) 0)
:assumption (<= (+ x_36 (* (~ 1) x_44) (* (~ 1) x_69)) 0)
:assumption (<= (+ x_38 (* (~ 1) x_44) (* (~ 1) x_50)) 0)
:assumption (<= (+ x_38 (* (~ 1) x_44) (* (~ 1) x_55)) 0)
:assumption (<= (+ x_38 (* (~ 1) x_44) (* (~ 1) x_60)) 0)
:assumption (<= (+ x_38 (* (~ 1) x_44) (* (~ 1) x_65)) 0)
:assumption (<= (+ x_38 (* (~ 1) x_44) (* (~ 1) x_70)) 0)
:assumption (not (<= (+ x_0 (* (/ 1000 999) x_1) x_6) 1))
:assumption (>= (+ x_40 x_44 (* (~ 1) x_46)) 0)
:assumption (not (<= (+ x_0 (* (/ 1000 999) x_2) x_6) 1))
:assumption (not (<= (+ x_0 (* (/ 1000 1001) x_1) x_6) 1))
:assumption (>= (+ x_0 x_6) 1)
:assumption (>= (+ x_40 x_44 (* (~ 1) x_51)) 0)
:assumption (not (<= (+ x_0 (* (/ 1000 999) x_3) x_6) 1))
:assumption (not (<= (+ x_0 (* (/ 1000 1001) x_2) x_6) 1))
:assumption (>= (+ x_40 x_44 (* (~ 1) x_56)) 0)
:assumption (not (<= (+ x_0 (* (/ 1000 999) x_4) x_6) 1))
:assumption (not (<= (+ x_0 (* (/ 1000 1001) x_3) x_6) 1))
:assumption (>= (+ x_40 x_44 (* (~ 1) x_61)) 0)
:assumption (not (<= (+ x_0 (* (/ 1000 999) x_5) x_6) 1))
:assumption (not (<= (+ x_0 (* (/ 1000 1001) x_4) x_6) 1))
:assumption (>= (+ x_40 x_44 (* (~ 1) x_66)) 0)
:assumption (not (<= (+ x_0 (* (/ 1000 1001) x_5) x_6) 1))
:assumption (>= (+ x_34 x_44 (* (~ 1) x_47)) 0)
:assumption (>= (+ x_1 x_5 (* (/ 1001 500) x_44)) (/ 1001 1000))
:assumption (<= (+ x_1 x_5 (* (~ (/ 999 500)) x_44)) (/ 4999 1000))
:assumption (>= (+ x_34 x_44 (* (~ 1) x_52)) 0)
:assumption (>= (+ x_34 x_44 (* (~ 1) x_57)) 0)
:assumption (>= (+ x_34 x_44 (* (~ 1) x_62)) 0)
:assumption (>= (+ x_34 x_44 (* (~ 1) x_67)) 0)
:assumption (<= (+ x_7 (* (/ 1998 1001) x_44) (* (~ (/ 1998 1001)) x_82)) (~ 2))
:assumption (>= (+ x_0 x_6 (* (~ 1) x_9)) 0)
:assumption (>= (+ x_0 x_6 (* (~ 1) x_8)) 0)
:assumption (>= (+ x_35 x_44 (* (~ 1) x_48)) 0)
:assumption (>= (+ x_0 x_6 (* (~ 1) x_10)) 0)
:assumption (>= (+ x_35 x_44 (* (~ 1) x_53)) 0)
:assumption (<= (+ x_6 x_44 x_82 (* (~ (/ 999 1001)) x_83)) (~ (/ 1501 1000)))
:assumption (not (<= (+ x_7 (* (~ 1) x_82) (* (~ (/ 2 999)) x_83)) (/ 1001 999)))
:assumption (>= (+ x_0 x_6 (* (~ 1) x_11)) 0)
:assumption (>= (+ x_35 x_44 (* (~ 1) x_58)) 0)
:assumption (>= (+ x_0 x_6 (* (~ 1) x_12)) 0)
:assumption (>= (+ x_35 x_44 (* (~ 1) x_63)) 0)
:assumption (>= (+ x_35 x_44 (* (~ 1) x_68)) 0)
:assumption (=(+ x_0 x_6 (* (~ 1) x_13)) 0)
:assumption (=(+ x_0 x_6 (* (~ 1) x_13)) 0)
:assumption (>= (+ x_36 x_44 (* (~ 1) x_49)) 0)
:assumption (>= (+ x_6 (* (~ (/ 1001 999)) x_7) (* (~ 1) x_44) (* (~ 1) x_84)) (/ 5003 1998))
:assumption (=(+ x_0 (* (~ 1) x_71)) 0)
:assumption (=(+ x_0 (* (~ 1) x_71)) 0)
:assumption (=(+ x_40 (* (~ 1) x_72)) 0)
:assumption (=(+ x_40 (* (~ 1) x_72)) 0)
:assumption (>= (+ x_36 x_44 (* (~ 1) x_54)) 0)
:assumption (=(+ x_1 (* (~ 1) x_77)) 0)
:assumption (=(+ x_1 (* (~ 1) x_77)) 0)
:assumption (=(+ x_34 (* (~ 1) x_73)) 0)
:assumption (=(+ x_34 (* (~ 1) x_73)) 0)
:assumption (>= (+ x_36 x_44 (* (~ 1) x_59)) 0)
:assumption (=(+ x_2 (* (~ 1) x_78)) 0)
:assumption (=(+ x_2 (* (~ 1) x_78)) 0)
:assumption (=(+ x_35 (* (~ 1) x_74)) 0)
:assumption (=(+ x_35 (* (~ 1) x_74)) 0)
:assumption (>= (+ x_36 x_44 (* (~ 1) x_64)) 0)
:assumption (=(+ x_3 (* (~ 1) x_79)) 0)
:assumption (=(+ x_3 (* (~ 1) x_79)) 0)
:assumption (=(+ x_36 (* (~ 1) x_75)) 0)
:assumption (=(+ x_36 (* (~ 1) x_75)) 0)
:assumption (>= (+ x_36 x_44 (* (~ 1) x_69)) 0)
:assumption (=(+ x_4 (* (~ 1) x_80)) 0)
:assumption (=(+ x_4 (* (~ 1) x_80)) 0)
:assumption (=(+ x_38 (* (~ 1) x_76)) 0)
:assumption (=(+ x_38 (* (~ 1) x_76)) 0)
:assumption (>= (+ x_38 x_44 (* (~ 1) x_50)) 0)
:assumption (=(+ x_5 (* (~ 1) x_81)) 0)
:assumption (=(+ x_5 (* (~ 1) x_81)) 0)
:assumption (=(+ x_39 (* (~ 1) x_77)) 0)
:assumption (=(+ x_39 (* (~ 1) x_77)) 0)
:assumption (>= (+ x_38 x_44 (* (~ 1) x_55)) 0)
:assumption (=(+ x_41 (* (~ 1) x_78)) 0)
:assumption (=(+ x_41 (* (~ 1) x_78)) 0)
:assumption (>= (+ x_38 x_44 (* (~ 1) x_60)) 0)
:assumption (=(+ x_42 (* (~ 1) x_79)) 0)
:assumption (=(+ x_42 (* (~ 1) x_79)) 0)
:assumption (>= (+ x_38 x_44 (* (~ 1) x_65)) 0)
:assumption (=(+ x_43 (* (~ 1) x_80)) 0)
:assumption (=(+ x_43 (* (~ 1) x_80)) 0)
:assumption (>= (+ x_38 x_44 (* (~ 1) x_70)) 0)
:assumption (=(+ x_37 (* (~ 1) x_81)) 0)
:assumption (=(+ x_37 (* (~ 1) x_81)) 0)

:assumption (not (=(+ x_7 (* (~ 1) x_26) x_32) 0))
:assumption (not (=(+ x_0 (* 2 x_6) x_7 (* (~ 1) x_13)) 0))
:assumption (not (=(+ x_45 (* (~ 1) x_71)) 0))
:assumption (not (=x_6 1))
:assumption (not (=(+ x_6 x_7) 1))
:assumption (not (=(+ x_0 x_6 x_7) 0))
:assumption (not (=(+ x_6 x_7 (* (~ 1) x_11) x_13) 0))
:assumption (not (=x_7 0))
:assumption (not (=(+ x_6 x_7 (* (~ 1) x_10) x_13) 0))
:assumption (not (=(+ x_6 (* (/ 1 2) x_7) (* (~ (/ 1 2)) x_9)) 0))
:assumption (not (=(+ x_10 (* (~ 1) x_13)) 0))
:assumption (not (=(+ x_6 x_7 (* (~ 1) x_12) x_13) 0))
:assumption (not (=(+ x_6 x_7 (* (~ 1) x_9) x_13) 0))
:assumption (not (=(+ x_0 (* (~ 1) x_45)) 0))
:assumption (not (=(+ x_8 (* (~ 1) x_13)) 0))
:assumption (not (=(+ x_6 x_7 (* (~ 1) x_8) x_13) 0))
:assumption (not (=(+ x_7 (* (~ 1) x_36)) (~ 1)))
:assumption (not (=(+ x_6 (* (/ 1 2) x_7) (* (~ (/ 1 2)) x_8)) 0))
:assumption (not (=(+ x_5 (* (~ 1) x_45)) 0))
:assumption (not (=(+ x_7 (* (~ 1) x_23) x_31) 0))
:assumption (not (=(+ x_7 (* (~ 1) x_38)) (~ 1)))
:assumption (not (=(+ x_7 (* (~ 1) x_17) x_29) 0))
:assumption (not (=(+ x_7 (* (~ 1) x_20) x_30) 0))
:assumption (not (=(+ x_7 (* (~ 1) x_16) x_33) 0))
:assumption (not (=(+ x_2 (* (~ 1) x_45)) 0))
:assumption (not (=(+ x_6 (* (/ 1 2) x_7) (* (~ (/ 1 2)) x_10)) 0))
:assumption (not (=(+ x_7 (* (~ 1) x_40)) (~ 1)))
:assumption (not (=(+ x_7 (* (~ 1) x_35)) (~ 1)))
:assumption (not (=(+ x_3 (* (~ 1) x_45)) 0))
:assumption (not (=(+ x_7 (* (~ 1) x_34)) (~ 1)))
:assumption (not (=(+ x_6 (* (/ 1 2) x_7) (* (~ (/ 1 2)) x_11)) 0))
:assumption (not (=(+ x_1 (* (~ 1) x_45)) 0))
:assumption (not (=(+ x_12 (* (~ 1) x_13)) 0))
:assumption (not (=(+ x_6 (* (/ 1 2) x_7) (* (~ (/ 1 2)) x_12)) 0))
  
  :formula true
)