diff options
Diffstat (limited to 'test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt')
| -rw-r--r-- | test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt | 533 |
1 files changed, 533 insertions, 0 deletions
diff --git a/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt b/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt new file mode 100644 index 000000000..edbff7148 --- /dev/null +++ b/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt @@ -0,0 +1,533 @@ +(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 +) |