path: root/test/regress/regress0/uflia/error1.smtv1.smt2

(set-option :incremental false)
(set-info :status sat)
(set-logic QF_UFLIA)
(declare-fun f0 (Int Int Int) Int)
(declare-fun f1 (Int) Int)
(declare-fun p0 (Int Int) Bool)
(declare-fun v0 () Int)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(check-sat-assuming ( (let ((_let_0 (ite (p0 (+ v2 v2) v1) 1 0))) (let ((_let_1 (ite (p0 (f1 v1) v1) 1 0))) (let ((_let_2 (ite (p0 v2 _let_1) 1 0))) (let ((_let_3 (* (- 2) (+ v2 v2)))) (let ((_let_4 (+ v1 (f1 v1)))) (let ((_let_5 (* 2 _let_3))) (let ((_let_6 (f0 v2 (f1 v1) v0))) (let ((_let_7 (+ (ite (p0 v1 (+ v2 v2)) 1 0) _let_3))) (let ((_let_8 (- _let_4 _let_3))) (let ((_let_9 (* _let_8 (- 2)))) (let ((_let_10 (- (+ v2 v2)))) (let ((_let_11 (f1 (+ v2 v2)))) (let ((_let_12 (> _let_0 _let_3))) (let ((_let_13 (= v2 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (let ((_let_14 (< _let_3 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0)))) (let ((_let_15 (distinct _let_1 _let_9))) (let ((_let_16 (>= v0 (+ _let_4 _let_7)))) (let ((_let_17 (distinct _let_11 (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))))) (let ((_let_18 (distinct (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) (+ _let_4 _let_7)))) (let ((_let_19 (ite (> _let_7 (f1 v1)) (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_3))) (let ((_let_20 (ite _let_14 (+ (+ v2 v2) _let_1) _let_8))) (let ((_let_21 (ite (< _let_1 _let_2) (+ (+ v2 v2) _let_1) _let_10))) (let ((_let_22 (ite (p0 v1 _let_9) v2 _let_10))) (let ((_let_23 (ite (<= v2 v2) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) _let_6))) (let ((_let_24 (ite (= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (* _let_10 (- 1))) (+ _let_4 _let_7) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))))) (let ((_let_25 (ite _let_18 v0 _let_2))) (let ((_let_26 (ite (distinct (f1 v1) _let_10) (+ v2 v2) v0))) (let ((_let_27 (ite (> _let_3 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_20 _let_4))) (let ((_let_28 (ite (> _let_4 _let_6) _let_8 _let_9))) (let ((_let_29 (ite _let_16 (ite _let_12 _let_26 v2) v2))) (let ((_let_30 (ite _let_14 _let_0 _let_6))) (let ((_let_31 (ite (> _let_6 _let_8) (* _let_10 (- 1)) (* _let_10 (- 1))))) (let ((_let_32 (ite (>= _let_6 _let_0) (ite (p0 v1 (+ v2 v2)) 1 0) _let_3))) (let ((_let_33 (ite (<= _let_4 _let_3) _let_11 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (let ((_let_34 (ite (< _let_0 (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) v1))) (let ((_let_35 (ite (distinct _let_0 (+ (+ v2 v2) _let_1)) (ite _let_18 _let_7 v0) _let_6))) (let ((_let_36 (ite _let_16 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1)) (* _let_10 (- 1))))) (let ((_let_37 (ite _let_18 _let_10 _let_21))) (let ((_let_38 (ite (distinct _let_2 _let_9) (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2)) _let_5))) (let ((_let_39 (ite (= _let_3 _let_1) _let_32 _let_0))) (let ((_let_40 (ite _let_12 (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))))) (let ((_let_41 (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (p0 v1 (+ v2 v2)) 1 0)) _let_0 _let_27))) (let ((_let_42 (ite (< _let_4 (+ v2 v2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (let ((_let_43 (ite (<= v2 v2) (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) _let_27))) (let ((_let_44 (ite (distinct (+ _let_4 _let_7) (+ _let_4 _let_7)) _let_2 (ite (p0 v1 (+ v2 v2)) 1 0)))) (let ((_let_45 (ite _let_15 _let_42 _let_24))) (let ((_let_46 (ite (>= _let_1 _let_2) _let_40 (ite _let_18 _let_7 v0)))) (let ((_let_47 (ite (> _let_4 _let_6) (+ _let_4 _let_7) (ite (> (+ _let_4 _let_7) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) _let_21)))) (let ((_let_48 (ite (< _let_0 (+ v2 v2)) (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33) _let_9))) (let ((_let_49 (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_48 (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))))) (let ((_let_50 (ite _let_17 _let_0 _let_10))) (let ((_let_51 (ite (< _let_2 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_0 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))))) (let ((_let_52 (ite _let_13 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1)) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (let ((_let_53 (ite (= _let_7 (f1 v1)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) _let_11))) (let ((_let_54 (ite (>= v1 (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) _let_24 _let_10))) (let ((_let_55 (and (= (= (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_31) (>= (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) _let_7)) (= (p0 v2 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9)) (< (ite (< _let_1 _let_2) _let_26 _let_8) _let_31))))) (let ((_let_56 (ite (= (> (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f1 v1)) (= (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2))) (= (= (xor (= (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5) (ite (= _let_3 _let_1) _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (or (or (>= v1 (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (or (> _let_5 (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21)) (distinct (ite (< _let_1 _let_2) _let_26 _let_8) _let_6))) (p0 _let_40 _let_8))) (<= _let_31 (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)))) (distinct _let_3 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (ite (<= _let_31 _let_40) (xor (= (= (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1)) (+ (+ v2 v2) _let_1)) (= (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33) _let_5)) (and (>= _let_4 _let_47) (<= _let_40 _let_31))) (not (= (p0 (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2)) _let_47) (and _let_12 (= (ite _let_18 _let_7 v0) _let_9)))))))) (let ((_let_57 (or (ite (ite (= (<= (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) _let_2) _let_18) (or (or (and (and (not (distinct (ite _let_18 _let_7 v0) _let_52)) (distinct (ite (< _let_1 _let_2) _let_26 _let_8) _let_0)) (<= (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5))) (not (<= _let_4 (+ (+ v2 v2) _let_1)))) (or (< (ite _let_12 _let_26 v2) _let_9) (p0 v0 _let_19))) (not (or (p0 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) _let_3) (<= _let_4 _let_41)))) (ite (= (<= (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) _let_2) _let_18) (or (or (and (and (not (distinct (ite _let_18 _let_7 v0) _let_52)) (distinct (ite (< _let_1 _let_2) _let_26 _let_8) _let_0)) (<= (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5))) (not (<= _let_4 (+ (+ v2 v2) _let_1)))) (or (< (ite _let_12 _let_26 v2) _let_9) (p0 v0 _let_19))) (not (or (p0 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) _let_3) (<= _let_4 _let_41)))) (= (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (or (p0 v0 (ite (= _let_3 _let_1) _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (> (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)))) (not (< _let_39 (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))))) (=> (= (> _let_34 _let_36) (and (= _let_54 _let_39) (>= _let_3 (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25))))) (>= (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) (f1 v1))))) (=> (or (or (or (= (distinct _let_2 _let_9) (ite (distinct _let_20 _let_35) (<= _let_9 _let_30) (p0 _let_50 _let_39))) (not (and (=> (= (f1 v1) _let_25) (p0 _let_50 _let_4)) (not (and (< _let_19 _let_26) (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))))))) (=> (ite (=> (ite (distinct _let_45 (f1 v1)) (<= _let_4 _let_36) (= (+ v2 v2) (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)))) (= _let_4 _let_23)) (=> (> (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_50) (distinct (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) v0)) (and (or (= (not (<= _let_27 _let_42)) (< _let_50 _let_52)) (=> (p0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_33) (< _let_4 (+ v2 v2)))) (xor (= _let_44 (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))) (distinct _let_10 _let_6)))) (and (< _let_5 _let_52) (or (xor (= (and (<= _let_45 _let_11) (or (> (* _let_10 (- 1)) _let_10) (<= _let_4 _let_8))) (= _let_3 v0)) (xor (= _let_10 (* _let_10 (- 1))) (> (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_1))) (and (distinct (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (distinct (+ _let_4 _let_7) (+ _let_4 _let_7))))))) (and (= (and (ite (and (<= (ite _let_12 _let_26 v2) _let_44) (ite (>= _let_46 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (= _let_50 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (p0 _let_38 _let_22))) (=> (>= (+ _let_4 _let_7) _let_4) (= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (* _let_10 (- 1)))) (<= _let_31 _let_30)) (=> (not (= _let_51 (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (=> (or (< _let_38 _let_35) (p0 (ite _let_12 _let_26 v2) (ite (< _let_1 _let_2) _let_26 _let_8))) (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (p0 v1 (+ v2 v2)) 1 0))))) (xor (distinct _let_0 (+ (+ v2 v2) _let_1)) (and (not (<= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25))) (= (=> (< (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_1) (> _let_4 _let_6)) (not (xor (and (not (<= _let_38 (+ _let_4 _let_7))) (= (+ _let_4 _let_7) (+ v2 v2))) (=> (and (<= v2 _let_45) (>= _let_6 _let_0)) (not (>= (ite (p0 v1 (+ v2 v2)) 1 0) _let_1))))))))) (= (ite (>= _let_22 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (> _let_9 (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7))) (=> (and _let_14 (>= (+ v2 v2) (* _let_10 (- 1)))) (xor (< (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) _let_32) (p0 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33))))) (not (= _let_34 _let_3))))) (or (or (or (= (distinct _let_2 _let_9) (ite (distinct _let_20 _let_35) (<= _let_9 _let_30) (p0 _let_50 _let_39))) (not (and (=> (= (f1 v1) _let_25) (p0 _let_50 _let_4)) (not (and (< _let_19 _let_26) (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))))))) (=> (ite (=> (ite (distinct _let_45 (f1 v1)) (<= _let_4 _let_36) (= (+ v2 v2) (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)))) (= _let_4 _let_23)) (=> (> (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_50) (distinct (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) v0)) (and (or (= (not (<= _let_27 _let_42)) (< _let_50 _let_52)) (=> (p0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_33) (< _let_4 (+ v2 v2)))) (xor (= _let_44 (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))) (distinct _let_10 _let_6)))) (and (< _let_5 _let_52) (or (xor (= (and (<= _let_45 _let_11) (or (> (* _let_10 (- 1)) _let_10) (<= _let_4 _let_8))) (= _let_3 v0)) (xor (= _let_10 (* _let_10 (- 1))) (> (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_1))) (and (distinct (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (distinct (+ _let_4 _let_7) (+ _let_4 _let_7))))))) (and (= (and (ite (and (<= (ite _let_12 _let_26 v2) _let_44) (ite (>= _let_46 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (= _let_50 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (p0 _let_38 _let_22))) (=> (>= (+ _let_4 _let_7) _let_4) (= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (* _let_10 (- 1)))) (<= _let_31 _let_30)) (=> (not (= _let_51 (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (=> (or (< _let_38 _let_35) (p0 (ite _let_12 _let_26 v2) (ite (< _let_1 _let_2) _let_26 _let_8))) (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (p0 v1 (+ v2 v2)) 1 0))))) (xor (distinct _let_0 (+ (+ v2 v2) _let_1)) (and (not (<= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25))) (= (=> (< (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_1) (> _let_4 _let_6)) (not (xor (and (not (<= _let_38 (+ _let_4 _let_7))) (= (+ _let_4 _let_7) (+ v2 v2))) (=> (and (<= v2 _let_45) (>= _let_6 _let_0)) (not (>= (ite (p0 v1 (+ v2 v2)) 1 0) _let_1))))))))) (= (ite (>= _let_22 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (> _let_9 (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7))) (=> (and _let_14 (>= (+ v2 v2) (* _let_10 (- 1)))) (xor (< (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) _let_32) (p0 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33))))) (not (= _let_34 _let_3))))))))) (=> (= (or (or (= (< (+ _let_4 _let_7) (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25))) (<= _let_33 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9))) (= _let_8 _let_37)) (or (or (=> (p0 (ite (< _let_1 _let_2) _let_26 _let_8) _let_47) (or (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (< _let_22 _let_46))) (not (ite (xor (p0 _let_22 _let_26) (= (p0 _let_4 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (= _let_45 (+ (+ v2 v2) _let_1)))) (xor (and (= _let_49 v1) (< _let_10 _let_45)) (xor (=> (>= _let_41 _let_3) (> (ite (p0 v1 (+ v2 v2)) 1 0) _let_7)) (= _let_44 _let_22))) (xor (= (ite (< _let_1 _let_2) _let_26 _let_8) (+ v2 v2)) (<= (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2) (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21)))))) (not (ite (not (< (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) (+ v2 v2))) (=> (xor (distinct _let_4 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))) (=> (< v0 _let_31) _let_15)) (distinct _let_4 (+ (+ v2 v2) _let_1))) (and (ite (= _let_3 _let_1) (> (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) _let_50) (=> (> (* _let_10 (- 1)) (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (xor (distinct _let_50 v1) (<= v2 _let_54)))) (distinct v1 _let_29)))))) (or (or (or (xor (< _let_9 _let_33) (= (and (p0 (* _let_10 (- 1)) _let_33) (< _let_0 (+ v2 v2))) (and (= _let_11 _let_53) (= _let_36 _let_26)))) (not (> _let_46 _let_22))) (= (and (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) (>= _let_0 _let_9)) (= _let_33 _let_19))) (distinct (f1 v1) (+ (+ v2 v2) _let_1)))) (and (not (=> (xor (not (p0 _let_45 _let_48)) (>= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9))) (and (or (= (> _let_10 _let_7) (distinct (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) _let_50)) (< _let_51 _let_48)) (>= _let_54 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2))))) (ite (= (and (=> (= (xor (and (= (p0 _let_46 v2) (p0 v1 _let_8)) (< (ite _let_12 _let_26 v2) (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21))) (=> (>= (ite (> _let_10 _let_7) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_21) _let_37) (= _let_33 _let_34))) (xor (=> (< _let_8 _let_1) (p0 _let_44 _let_54)) (p0 v1 _let_9))) (or (= (not (<= _let_22 _let_21)) (xor (= (p0 _let_5 _let_32) (<= _let_22 _let_53)) (>= _let_22 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)))) (=> (ite (<= _let_4 _let_50) (>= _let_29 _let_4) (p0 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1)) _let_42)) (ite (distinct (+ _let_4 _let_7) _let_44) (<= _let_25 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (< _let_9 _let_9))))) (< _let_49 _let_20)) (ite (not (xor (ite (not (<= (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_19)) (p0 _let_9 v2) (ite (not (< (ite _let_18 _let_7 v0) _let_36)) (ite (ite (xor (= v2 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (= _let_40 _let_11)) (= (or (p0 _let_3 _let_11) (p0 v2 _let_20)) (<= _let_4 _let_3)) (ite (distinct _let_36 _let_21) (distinct _let_6 (ite (> (+ _let_4 _let_7) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) _let_21)) (p0 _let_26 _let_11))) (>= (* _let_10 (- 1)) _let_27) (xor _let_55 _let_55)) (not (>= _let_22 _let_2)))) (=> (=> (>= _let_6 _let_30) (or (or (> _let_27 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (<= _let_31 (+ _let_4 _let_7))) (= (* _let_10 (- 1)) _let_39))) (xor (not (xor (p0 (+ v2 v2) _let_5) (> _let_7 (f1 v1)))) (=> (distinct (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* _let_10 (- 1))) (=> (and (xor (= _let_34 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0)) (>= _let_27 _let_5)) (ite (not (ite (distinct _let_53 (* _let_10 (- 1))) (= _let_46 _let_21) (> (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))))) (p0 _let_52 (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (<= _let_25 _let_3))) (xor (= (= _let_53 _let_23) (> v1 v2)) (>= _let_48 _let_28)))))))) (xor _let_57 _let_57) (not (and (=> (= (not (not (xor (ite (and (=> (not (< _let_32 (+ (+ v2 v2) _let_1))) (= (< (ite _let_18 _let_7 v0) (ite _let_18 _let_7 v0)) (>= v1 (+ (+ v2 v2) _let_1)))) (= v1 (ite (p0 v1 (+ v2 v2)) 1 0))) (< _let_22 _let_20) (> (+ _let_4 _let_7) (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (not (< _let_2 (ite (p0 v1 (+ v2 v2)) 1 0)))))) (= (<= v2 v2) (= _let_17 (p0 (* _let_10 (- 1)) _let_31)))) (and (xor (not (not (and (>= _let_38 _let_46) (> _let_20 _let_33)))) (not (xor (not (>= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_41)) (ite (and (= (> _let_3 (ite (p0 v1 (+ v2 v2)) 1 0)) (p0 _let_5 _let_52)) (and (<= _let_28 _let_35) (> _let_49 _let_6))) (=> (< _let_25 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2)) (= _let_48 _let_27)) (or (xor (xor (= _let_40 _let_7) (and (<= _let_38 _let_35) (> _let_2 _let_42))) (or (>= _let_43 _let_26) (=> (>= _let_38 _let_31) (= _let_8 (ite (p0 v1 (+ v2 v2)) 1 0))))) (or (= _let_7 (f1 v1)) (distinct (+ (+ v2 v2) _let_1) (ite (p0 v1 (+ v2 v2)) 1 0)))))))) (not (not (not (or (and (= (xor (distinct _let_8 _let_39) (<= (+ _let_4 _let_7) _let_0)) (=> (distinct (ite (> (+ _let_4 _let_7) (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) _let_21) (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0)) (< (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33) _let_10))) (>= _let_5 _let_6)) (ite (= (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) (<= _let_11 _let_3)) (=> (not (>= _let_1 _let_2)) (p0 _let_23 _let_10)) (<= _let_45 _let_44)))))))) (xor (not (xor (and (=> (= _let_4 _let_22) (= (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_47)) (= (= _let_46 _let_36) (p0 _let_4 (ite (>= (+ v2 v2) (* _let_10 (- 1))) _let_1 _let_33)))) (= (<= (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1))) (= (not (= _let_48 _let_4)) (= (p0 _let_4 (ite _let_18 _let_7 v0)) (= (<= (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))) (xor (<= (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25) _let_42) (< _let_1 _let_2)))))))) (= (xor (or (=> (not (<= _let_42 (ite (> _let_10 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9) v2))) (=> (= (< _let_0 (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) (< _let_46 (ite (< _let_1 _let_2) _let_26 _let_8))) (< _let_34 (ite _let_12 _let_26 v2)))) (< _let_53 (ite (p0 v1 (+ v2 v2)) 1 0))) (= (= (not (<= _let_42 _let_38)) (or (xor (ite (distinct _let_35 _let_11) (< _let_32 _let_51) (p0 (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5) (f1 v1))) (p0 (ite (< _let_1 _let_2) _let_26 _let_8) (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)))) (or (ite (or (p0 _let_53 (ite (>= (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_0) _let_25 (ite _let_12 _let_26 v2))) (distinct (f1 v1) _let_10)) (ite (< _let_43 _let_40) (= (distinct _let_6 _let_6) (>= _let_52 (ite _let_12 _let_26 v2))) (<= _let_26 _let_43)) (and (< _let_33 _let_49) (> _let_6 _let_8))) (=> (p0 _let_47 (ite _let_12 _let_26 v2)) (= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) _let_38))))) (xor (xor (not (distinct _let_54 (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0))) _let_13) (and (=> (=> (not (ite (>= v0 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (distinct (ite _let_18 _let_7 v0) _let_23) (<= (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) _let_0) (<= _let_49 _let_46)) (>= _let_54 _let_51))) (>= (ite (p0 (f1 v1) (+ v2 v2)) 1 0) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)))) (and (ite (ite (<= _let_27 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (= _let_53 _let_52) (p0 _let_41 (ite (p0 (f1 v1) (+ v2 v2)) 1 0))) (< _let_26 _let_22) (ite (>= (ite (>= (ite (p0 (+ (+ v2 v2) _let_1) _let_8) 1 0) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) _let_1 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) _let_19) (< (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_21) (p0 _let_23 (ite (< _let_1 _let_2) _let_26 _let_8)))) (ite (distinct _let_45 _let_42) (>= (ite (= _let_3 _let_1) _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_27) _let_16))) (and (= (or (=> (= (> (ite (< _let_1 _let_2) _let_26 _let_8) (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9)) (not (not (<= _let_48 _let_48)))) (not (=> (= (< _let_20 _let_0) (xor (= _let_23 _let_2) (xor (distinct _let_40 (ite _let_18 _let_7 v0)) (= _let_7 (ite (= (+ _let_4 _let_7) (+ v2 v2)) (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2) _let_9))))) (and _let_15 (not (distinct _let_25 _let_21)))))) (and (= (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)) _let_31) (=> (>= _let_39 (* (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) 2)) (ite (p0 (ite (distinct (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1)) (f0 (f1 v1) (+ _let_0 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) (f1 v1))) _let_11 (f1 v1)) _let_51) (= (p0 _let_39 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_8 _let_25)) (p0 _let_38 _let_29)) (p0 _let_32 _let_41))))) (xor (>= (+ (+ v2 v2) _let_1) _let_19) (p0 _let_36 (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))))) (> _let_35 (ite _let_12 _let_26 v2))))))) (= (or (or (distinct _let_44 _let_24) (= _let_30 (ite (<= _let_11 _let_3) _let_33 (+ _let_4 _let_7)))) (ite (p0 _let_31 _let_42) (= (<= _let_20 _let_10) (xor (< _let_48 _let_34) (> _let_3 _let_35))) (>= (ite (< _let_1 _let_2) _let_26 _let_8) _let_38))) (or (<= (+ _let_4 _let_7) (ite (= v1 (ite (p0 v1 (+ v2 v2)) 1 0)) _let_6 (+ (+ v2 v2) _let_1))) (>= _let_37 (ite (= _let_5 (ite (p0 (f1 v1) (+ v2 v2)) 1 0)) _let_5 _let_5)))))))))) _let_56 _let_56))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))