(set-option :incremental false)
(set-info :status sat)
(set-logic QF_UFLIA)
(declare-fun f0 (Int 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 (f0 v2 v2))) (let ((_let_1 (* 6 v0))) (let ((_let_2 (* (+ v1 v0) (- 6)))) (let ((_let_3 (* v1 (- 6)))) (let ((_let_4 (ite (p0 _let_2 v2) 1 0))) (let ((_let_5 (= v1 _let_2))) (let ((_let_6 (ite (>= _let_1 (* v0 6)) _let_1 v1))) (let ((_let_7 (ite (= _let_4 _let_1) v2 _let_4))) (let ((_let_8 (ite (>= _let_3 _let_3) _let_4 _let_7))) (let ((_let_9 (ite (p0 _let_1 v0) (+ v1 v0) (ite (> _let_3 v0) _let_4 _let_6)))) (let ((_let_10 (= (xor (= (ite (not (distinct (ite _let_5 _let_0 _let_6) (ite _let_5 _let_0 _let_6))) (not (not (< v1 _let_2))) (not (distinct (ite _let_5 _let_0 _let_6) (ite _let_5 _let_0 _let_6)))) (ite (=> (<= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_6) (p0 (+ v1 v0) _let_2)) (=> (<= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_6) (p0 (+ v1 v0) _let_2)) (> _let_3 (+ v1 v0)))) (xor (= (p0 _let_2 v1) (= _let_3 _let_0)) (or (ite (xor (= (distinct v2 _let_7) (p0 (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) (ite (> _let_3 v0) _let_4 _let_6))) (p0 v0 _let_0)) (> (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6)) _let_2) (= (< _let_7 _let_8) (= (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) (* v0 6)))) (p0 _let_2 _let_9)))) (ite (=> (xor (and (not (= (= (<= _let_2 (ite _let_5 _let_0 _let_6)) (= (>= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_7) (>= _let_3 _let_3))) (p0 v0 (ite _let_5 _let_0 _let_6)))) (not (= (= (<= _let_2 (ite _let_5 _let_0 _let_6)) (= (>= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_7) (>= _let_3 _let_3))) (p0 v0 (ite _let_5 _let_0 _let_6))))) (=> (< (ite (distinct v2 (* v0 6)) _let_7 v0) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (> _let_3 _let_8))) (xor (and (not (= (= (<= _let_2 (ite _let_5 _let_0 _let_6)) (= (>= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_7) (>= _let_3 _let_3))) (p0 v0 (ite _let_5 _let_0 _let_6)))) (not (= (= (<= _let_2 (ite _let_5 _let_0 _let_6)) (= (>= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) _let_7) (>= _let_3 _let_3))) (p0 v0 (ite _let_5 _let_0 _let_6))))) (=> (< (ite (distinct v2 (* v0 6)) _let_7 v0) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (> _let_3 _let_8)))) (= (< _let_0 (+ v1 v0)) (ite (= v0 (ite (p0 v0 _let_0) _let_2 _let_3)) (= v0 (ite (p0 v0 _let_0) _let_2 _let_3)) (and (xor (ite (distinct (* v0 6) v1) (= _let_2 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (not (p0 (* v0 6) v0))) (xor (not (>= (* v0 6) v2)) (and (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_7) (< _let_9 (ite (< v1 _let_2) _let_4 v2))))) (distinct _let_8 _let_8)))) (not (or (= (ite (ite (= v1 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (xor (= _let_8 _let_6) (xor (distinct v2 (* v0 6)) (=> (>= (ite (< v1 _let_2) _let_4 v2) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (= _let_4 _let_1)))) (not (<= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))))) (= (or (p0 _let_1 v0) (p0 v1 _let_1)) (=> (> _let_3 v0) (p0 (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) _let_4))) (= (or (p0 _let_1 v0) (p0 v1 _let_1)) (=> (> _let_3 v0) (p0 (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) _let_4)))) (=> (distinct _let_0 (ite (> _let_3 v0) _let_4 _let_6)) (not (= (ite (p0 v0 _let_0) _let_2 _let_3) (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6)))))) (= (ite (ite (= v1 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (xor (= _let_8 _let_6) (xor (distinct v2 (* v0 6)) (=> (>= (ite (< v1 _let_2) _let_4 v2) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (= _let_4 _let_1)))) (not (<= (ite (p0 v1 _let_1) _let_6 (ite _let_5 _let_0 _let_6)) (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))))) (= (or (p0 _let_1 v0) (p0 v1 _let_1)) (=> (> _let_3 v0) (p0 (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) _let_4))) (= (or (p0 _let_1 v0) (p0 v1 _let_1)) (=> (> _let_3 v0) (p0 (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6)) _let_4)))) (=> (distinct _let_0 (ite (> _let_3 v0) _let_4 _let_6)) (not (= (ite (p0 v0 _let_0) _let_2 _let_3) (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6)))))))))))) (let ((_let_11 (or (or (xor (xor (distinct (* v0 6) v1) (= _let_4 _let_8)) (=> (xor (>= _let_1 (* v0 6)) (=> (p0 _let_3 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (p0 _let_0 _let_7))) (and (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))) (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6))))))) (xor (xor (distinct (* v0 6) v1) (= _let_4 _let_8)) (=> (xor (>= _let_1 (* v0 6)) (=> (p0 _let_3 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (p0 _let_0 _let_7))) (and (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))) (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))))))) (or (xor (xor (distinct (* v0 6) v1) (= _let_4 _let_8)) (=> (xor (>= _let_1 (* v0 6)) (=> (p0 _let_3 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (p0 _let_0 _let_7))) (and (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))) (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6))))))) (xor (xor (distinct (* v0 6) v1) (= _let_4 _let_8)) (=> (xor (>= _let_1 (* v0 6)) (=> (p0 _let_3 (ite (= _let_4 _let_1) _let_8 (ite _let_5 _let_0 _let_6))) (p0 _let_0 _let_7))) (and (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6)))) (ite (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (< (ite (p0 v0 _let_0) _let_2 _let_3) (ite (>= (* v0 6) v2) (* v0 6) (ite _let_5 _let_0 _let_6))) (ite (distinct (ite (> _let_3 (+ v1 v0)) _let_3 (ite (< v1 _let_2) _let_4 v2)) _let_1) _let_5 (= v0 (ite (> _let_3 v0) _let_4 _let_6))))))))))) (=> (=> _let_10 _let_10) (not (or _let_11 _let_11))))))))))))))) ))