example02.smt

(declare-const P1 Bool)
(declare-const P2 Bool)
(declare-const P3 Bool)
(declare-const P4 Bool)
(declare-const P5 Bool)
(declare-const P6 Bool)
(declare-const P7 Bool)
(declare-const P8 Bool)
(declare-const P9 Bool)
(declare-const P10 Bool)
(declare-const P11 Bool)
(declare-const P12 Bool)
(declare-const P13 Bool)
(declare-const P14 Bool)
(declare-const P15 Bool)
(declare-const P16 Bool)
(declare-const P17 Bool)
(declare-const P18 Bool)
(declare-const P19 Bool)
(declare-const P20 Bool)

(assert (=> P1 P2))
(assert (=> P2 P3))
(assert (=> P3 P4))
(assert (=> P4 P5))
(assert (=> P5 P6))
(assert (=> P6 P7))
(assert (=> P7 P8))
(assert (=> P8 P9))
(assert (=> P9 P10))
(assert (=> P10 P11))
(assert (=> P11 P12))
(assert (=> P12 P13))
(assert (=> P13 P14))
(assert (=> P14 P15))
(assert (=> P15 P16))
(assert (=> P16 P17))
(assert (=> P17 P18))
(assert (=> P18 P19))
(assert (=> P19 P20))
(assert (not P20))

(check-sat)
(get-model)