; EXPECT: unsat
(set-logic ALL)
(set-option :incremental false)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Bool)
(declare-fun u () Bool)
(declare-fun v () Bool)
(declare-fun P1 () Bool)
(declare-fun P2 () Bool)
(declare-fun P3 () Bool)
(declare-fun P4 () Bool)
(declare-fun P6 () Bool)
(declare-fun P5 () Bool)
(define-fun a41 () Bool (ite p false true))
(define-fun a42 () Bool (ite (ite p false true) false true))
(define-fun a45 () Bool (ite p p (ite p false true)))
(define-fun a46 () Bool (ite q false true))
(define-fun a49 () Bool (ite s t false))
(define-fun a58 () Bool (ite q q (ite q false true)))
(define-fun a59 () Bool (ite r false true))
(define-fun a61 () Bool (ite s false true))
(define-fun a62 () Bool (ite s s (ite s false true)))
(define-fun a65 () Bool (ite t false true))
(define-fun a67 () Bool (ite u false true))
(define-fun a73 () Bool (ite p q false))
(define-fun a74 () Bool (ite q p false))
(define-fun a77 () Bool (ite r true s))
(define-fun a78 () Bool (ite s true r))
(define-fun a81 () Bool (ite t u (ite u false true)))
(define-fun a82 () Bool (ite u t (ite t false true)))
(define-fun a88 () Bool (ite q r false))
(define-fun a89 () Bool (ite p (ite q r false) false))
(define-fun a92 () Bool (ite s true t))
(define-fun a94 () Bool (ite t true u))
(define-fun a95 () Bool (ite s true (ite t true u)))
(define-fun a105 () Bool (ite t u false))
(define-fun a111 () Bool (ite p q true))
(define-fun a112 () Bool (ite q r true))
(define-fun a114 () Bool (ite p r true))
(define-fun a116 () Bool (ite s t (ite t false true)))
(define-fun a121 () Bool (ite (ite q false true) (ite p false true) true))
(define-fun a126 () Bool (let ((_let_1 (ite s false true))) (ite (ite r false true) _let_1 (ite _let_1 false true))))
(define-fun a130 () Bool (ite q true r))
(define-fun a132 () Bool (ite p r false))
(define-fun a133 () Bool (ite (ite p q false) true (ite p r false)))
(define-fun a138 () Bool (ite (ite s true t) (ite s true u) false))
(define-fun a143 () Bool (ite (ite p r true) (ite q r true) false))
(define-fun a145 () Bool (let ((_let_1 (ite (ite p r true) (ite q r true) false))) (ite (ite (ite p true q) r true) _let_1 (ite _let_1 false true))))
(define-fun a147 () Bool (ite s t true))
(define-fun a148 () Bool (ite s u true))
(define-fun a149 () Bool (ite (ite s t true) true (ite s u true)))
(define-fun a153 () Bool (ite (ite p q false) r true))
(define-fun a154 () Bool (ite (ite p r true) true (ite q r true)))
(define-fun a158 () Bool (ite (ite s t true) (ite s u true) false))
(define-fun a162 () Bool (ite p (ite q r true) true))
(define-fun a167 () Bool (ite (ite q false true) true (ite r false true)))
(define-fun a171 () Bool (ite (ite s false true) (ite t false true) false))
(define-fun a176 () Bool (ite p q r))
(define-fun a178 () Bool (ite p (ite q false true) (ite r false true)))
(define-fun a183 () Bool (let ((_let_1 (ite t false true))) (ite s _let_1 (ite _let_1 false true))))
(define-fun a187 () Bool (ite (ite p false true) true q))
(define-fun a192 () Bool (ite (ite r s false) true (ite (ite r false true) t false)))
(define-fun a197 () Bool (ite (ite p q true) (ite (ite p false true) r true) false))
(define-fun a200 () Bool (ite (ite s t false) true (ite (ite s false true) (ite t false true) false)))
(define-fun a204 () Bool (ite p q (ite q false true)))
(define-fun a205 () Bool (ite q p true))
(define-fun a206 () Bool (ite (ite p q true) (ite q p true) false))
(define-fun a210 () Bool (ite p (ite q false true) true))
(define-fun a214 () Bool (ite (ite p q false) false true))
(define-fun a221 () Bool (ite (ite p (ite q false true) false) r true))
(define-fun a225 () Bool (ite (ite (ite p false true) true q) (ite p r false) true))
(define-fun a228 () Bool (ite q r (ite r false true)))
(define-fun a231 () Bool (ite (ite p q (ite q false true)) r (ite r false true)))
(define-fun a237 () Bool (ite q (ite p r false) (ite (ite p false true) s false)))
(define-fun a288 () Bool (let ((_let_1 (ite p false true))) (let ((_let_2 (ite p r false))) (let ((_let_3 (ite q _let_2 (ite _let_1 s false)))) (let ((_let_4 (ite q false true))) (let ((_let_5 (ite q r false))) (let ((_let_6 (ite r false true))) (let ((_let_7 (ite p q _let_4))) (let ((_let_8 (ite _let_7 r _let_6))) (let ((_let_9 (ite q r _let_6))) (let ((_let_10 (ite _let_1 true q))) (let ((_let_11 (ite _let_10 _let_2 true))) (let ((_let_12 (ite q r true))) (let ((_let_13 (ite (ite p _let_4 false) r true))) (let ((_let_14 (ite q true r))) (let ((_let_15 (ite p q false))) (let ((_let_16 (ite _let_15 r true))) (let ((_let_17 (ite p _let_12 true))) (let ((_let_18 (ite p r true))) (let ((_let_19 (ite _let_18 _let_12 false))) (let ((_let_20 (ite (ite (ite p true q) r true) _let_19 (ite _let_19 false true)))) (let ((_let_21 (ite _let_15 false true))) (let ((_let_22 (ite p _let_4 true))) (let ((_let_23 (ite q p true))) (let ((_let_24 (ite p q true))) (let ((_let_25 (ite _let_24 _let_23 false))) (let ((_let_26 (ite t false true))) (let ((_let_27 (ite s false true))) (let ((_let_28 (ite _let_27 _let_26 false))) (let ((_let_29 (ite s t false))) (let ((_let_30 (ite _let_29 true _let_28))) (let ((_let_31 (ite s t _let_26))) (let ((_let_32 (ite _let_24 (ite _let_1 r true) false))) (let ((_let_33 (ite p q r))) (let ((_let_34 (ite (ite r s false) true (ite _let_6 t false)))) (let ((_let_35 (ite s _let_26 (ite _let_26 false true)))) (let ((_let_36 (ite p _let_4 _let_6))) (let ((_let_37 (ite s true t))) (let ((_let_38 (ite _let_4 true _let_6))) (let ((_let_39 (ite _let_1 false true))) (let ((_let_40 (ite s u true))) (let ((_let_41 (ite s t true))) (let ((_let_42 (ite _let_41 _let_40 false))) (let ((_let_43 (ite t u false))) (let ((_let_44 (ite _let_18 true _let_12))) (let ((_let_45 (ite _let_41 true _let_40))) (let ((_let_46 (ite t true u))) (let ((_let_47 (ite _let_37 (ite s true u) false))) (let ((_let_48 (ite _let_15 true _let_2))) (let ((_let_49 (ite _let_6 _let_27 (ite _let_27 false true)))) (let ((_let_50 (ite _let_4 _let_1 true))) (let ((_let_51 (ite u false true))) (let ((_let_52 (ite t u _let_51))) (let ((_let_53 (ite q q _let_4))) (let ((_let_54 (ite r true s))) (let ((_let_55 (ite s true _let_46))) (let ((_let_56 (ite p _let_5 false))) (let ((_let_57 (ite u t _let_26))) (let ((_let_58 (ite s true r))) (let ((_let_59 (ite q p false))) (let ((_let_60 (ite s s _let_27))) (let ((_let_61 (ite p p _let_1))) (ite (ite (ite p _let_1 _let_39) false true) (ite (ite _let_61 (ite (ite q true _let_4) (ite (ite r r true) (ite (ite _let_29 s true) (ite u (ite u true v) true) false) false) false) false) (ite (ite _let_53 (ite (ite r r _let_6) _let_60 false) false) (ite (ite _let_61 (ite _let_60 (ite (ite t t _let_26) (ite _let_51 _let_51 (ite _let_51 false true)) false) false) false) (ite (ite (ite _let_15 _let_59 (ite _let_59 false true)) (ite (ite _let_54 _let_58 (ite _let_58 false true)) (ite _let_52 _let_57 (ite _let_57 false true)) false) false) (ite (ite (ite (ite _let_15 r false) _let_56 (ite _let_56 false true)) (ite (ite _let_37 true u) _let_55 (ite _let_55 false true)) false) (ite (ite (ite (ite p p false) p _let_1) (ite (ite (ite q true q) q _let_4) (ite (ite (ite r _let_54 false) r _let_6) (ite (ite t true _let_43) t _let_26) false) false) false) (ite _let_53 (ite (ite (ite (ite _let_24 _let_12 false) _let_18 true) (ite (ite _let_31 _let_52 false) (ite s u _let_51) true) false) (ite (ite (ite _let_24 _let_50 (ite _let_50 false true)) (ite (ite r s _let_27) _let_49 (ite _let_49 false true)) false) (ite (ite (ite (ite p _let_14 false) _let_48 (ite _let_48 false true)) (ite (ite s true _let_43) _let_47 (ite _let_47 false true)) false) (ite (ite _let_20 (ite (ite s _let_46 true) _let_45 (ite _let_45 false true)) false) (ite (ite (ite _let_16 _let_44 (ite _let_44 false true)) (ite (ite s _let_43 true) _let_42 (ite _let_42 false true)) false) (ite (ite _let_16 _let_17 (ite _let_17 false true)) (ite (ite (ite _let_39 p _let_1) (ite (ite (ite _let_5 false true) _let_38 (ite _let_38 false true)) (ite (ite _let_37 false true) _let_28 (ite _let_28 false true)) false) false) (ite (ite (ite (ite _let_33 false true) _let_36 (ite _let_36 false true)) (ite (ite _let_31 false true) _let_35 (ite _let_35 false true)) false) (ite (ite (ite _let_24 _let_10 (ite _let_10 false true)) (ite (ite r s t) _let_34 (ite _let_34 false true)) false) (ite (ite (ite _let_33 _let_32 (ite _let_32 false true)) (ite _let_31 _let_30 (ite _let_30 false true)) false) (ite (ite _let_7 _let_25 (ite _let_25 false true)) (ite (ite _let_24 true _let_23) (ite (ite _let_4 true (ite (ite _let_22 p false) false true)) (ite (ite _let_22 _let_21 (ite _let_21 false true)) (ite _let_20 (ite (ite _let_17 _let_16 (ite _let_16 false true)) (ite (ite (ite p _let_14 true) _let_13 (ite _let_13 false true)) (ite (ite (ite p _let_12 false) _let_11 (ite _let_11 false true)) (ite (ite (ite p _let_9 (ite _let_9 false true)) _let_8 (ite _let_8 false true)) (ite (ite (ite p _let_5 (ite _let_4 s false)) _let_3 (ite _let_3 false true)) (ite (ite (ite P1 (ite P2 true P3) (ite P3 true P4)) (ite (ite P3 (ite P6 false true) (ite P4 P1 true)) (ite (ite (ite P2 P5 false) false true) (ite P2 P5 true) false) false) false) (ite (ite P3 P6 true) false true) true) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat-assuming ( (not (let ((_let_1 (ite p false true))) (let ((_let_2 (ite p r false))) (let ((_let_3 (ite q _let_2 (ite _let_1 s false)))) (let ((_let_4 (ite q false true))) (let ((_let_5 (ite q r false))) (let ((_let_6 (ite r false true))) (let ((_let_7 (ite p q _let_4))) (let ((_let_8 (ite _let_7 r _let_6))) (let ((_let_9 (ite q r _let_6))) (let ((_let_10 (ite _let_1 true q))) (let ((_let_11 (ite _let_10 _let_2 true))) (let ((_let_12 (ite q r true))) (let ((_let_13 (ite (ite p _let_4 false) r true))) (let ((_let_14 (ite q true r))) (let ((_let_15 (ite p q false))) (let ((_let_16 (ite _let_15 r true))) (let ((_let_17 (ite p _let_12 true))) (let ((_let_18 (ite p r true))) (let ((_let_19 (ite _let_18 _let_12 false))) (let ((_let_20 (ite (ite (ite p true q) r true) _let_19 (ite _let_19 false true)))) (let ((_let_21 (ite _let_15 false true))) (let ((_let_22 (ite p _let_4 true))) (let ((_let_23 (ite q p true))) (let ((_let_24 (ite p q true))) (let ((_let_25 (ite _let_24 _let_23 false))) (let ((_let_26 (ite t false true))) (let ((_let_27 (ite s false true))) (let ((_let_28 (ite _let_27 _let_26 false))) (let ((_let_29 (ite s t false))) (let ((_let_30 (ite _let_29 true _let_28))) (let ((_let_31 (ite s t _let_26))) (let ((_let_32 (ite _let_24 (ite _let_1 r true) false))) (let ((_let_33 (ite p q r))) (let ((_let_34 (ite (ite r s false) true (ite _let_6 t false)))) (let ((_let_35 (ite s _let_26 (ite _let_26 false true)))) (let ((_let_36 (ite p _let_4 _let_6))) (let ((_let_37 (ite s true t))) (let ((_let_38 (ite _let_4 true _let_6))) (let ((_let_39 (ite _let_1 false true))) (let ((_let_40 (ite s u true))) (let ((_let_41 (ite s t true))) (let ((_let_42 (ite _let_41 _let_40 false))) (let ((_let_43 (ite t u false))) (let ((_let_44 (ite _let_18 true _let_12))) (let ((_let_45 (ite _let_41 true _let_40))) (let ((_let_46 (ite t true u))) (let ((_let_47 (ite _let_37 (ite s true u) false))) (let ((_let_48 (ite _let_15 true _let_2))) (let ((_let_49 (ite _let_6 _let_27 (ite _let_27 false true)))) (let ((_let_50 (ite _let_4 _let_1 true))) (let ((_let_51 (ite u false true))) (let ((_let_52 (ite t u _let_51))) (let ((_let_53 (ite q q _let_4))) (let ((_let_54 (ite r true s))) (let ((_let_55 (ite s true _let_46))) (let ((_let_56 (ite p _let_5 false))) (let ((_let_57 (ite u t _let_26))) (let ((_let_58 (ite s true r))) (let ((_let_59 (ite q p false))) (let ((_let_60 (ite s s _let_27))) (let ((_let_61 (ite p p _let_1))) (ite (ite (ite p _let_1 _let_39) false true) (ite (ite _let_61 (ite (ite q true _let_4) (ite (ite r r true) (ite (ite _let_29 s true) (ite u (ite u true v) true) false) false) false) false) (ite (ite _let_53 (ite (ite r r _let_6) _let_60 false) false) (ite (ite _let_61 (ite _let_60 (ite (ite t t _let_26) (ite _let_51 _let_51 (ite _let_51 false true)) false) false) false) (ite (ite (ite _let_15 _let_59 (ite _let_59 false true)) (ite (ite _let_54 _let_58 (ite _let_58 false true)) (ite _let_52 _let_57 (ite _let_57 false true)) false) false) (ite (ite (ite (ite _let_15 r false) _let_56 (ite _let_56 false true)) (ite (ite _let_37 true u) _let_55 (ite _let_55 false true)) false) (ite (ite (ite (ite p p false) p _let_1) (ite (ite (ite q true q) q _let_4) (ite (ite (ite r _let_54 false) r _let_6) (ite (ite t true _let_43) t _let_26) false) false) false) (ite _let_53 (ite (ite (ite (ite _let_24 _let_12 false) _let_18 true) (ite (ite _let_31 _let_52 false) (ite s u _let_51) true) false) (ite (ite (ite _let_24 _let_50 (ite _let_50 false true)) (ite (ite r s _let_27) _let_49 (ite _let_49 false true)) false) (ite (ite (ite (ite p _let_14 false) _let_48 (ite _let_48 false true)) (ite (ite s true _let_43) _let_47 (ite _let_47 false true)) false) (ite (ite _let_20 (ite (ite s _let_46 true) _let_45 (ite _let_45 false true)) false) (ite (ite (ite _let_16 _let_44 (ite _let_44 false true)) (ite (ite s _let_43 true) _let_42 (ite _let_42 false true)) false) (ite (ite _let_16 _let_17 (ite _let_17 false true)) (ite (ite (ite _let_39 p _let_1) (ite (ite (ite _let_5 false true) _let_38 (ite _let_38 false true)) (ite (ite _let_37 false true) _let_28 (ite _let_28 false true)) false) false) (ite (ite (ite (ite _let_33 false true) _let_36 (ite _let_36 false true)) (ite (ite _let_31 false true) _let_35 (ite _let_35 false true)) false) (ite (ite (ite _let_24 _let_10 (ite _let_10 false true)) (ite (ite r s t) _let_34 (ite _let_34 false true)) false) (ite (ite (ite _let_33 _let_32 (ite _let_32 false true)) (ite _let_31 _let_30 (ite _let_30 false true)) false) (ite (ite _let_7 _let_25 (ite _let_25 false true)) (ite (ite _let_24 true _let_23) (ite (ite _let_4 true (ite (ite _let_22 p false) false true)) (ite (ite _let_22 _let_21 (ite _let_21 false true)) (ite _let_20 (ite (ite _let_17 _let_16 (ite _let_16 false true)) (ite (ite (ite p _let_14 true) _let_13 (ite _let_13 false true)) (ite (ite (ite p _let_12 false) _let_11 (ite _let_11 false true)) (ite (ite (ite p _let_9 (ite _let_9 false true)) _let_8 (ite _let_8 false true)) (ite (ite (ite p _let_5 (ite _let_4 s false)) _let_3 (ite _let_3 false true)) (ite (ite (ite P1 (ite P2 true P3) (ite P3 true P4)) (ite (ite P3 (ite P6 false true) (ite P4 P1 true)) (ite (ite (ite P2 P5 false) false true) (ite P2 P5 true) false) false) false) (ite (ite P3 P6 true) false true) true) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))