(declare-datatypes ((|couple(integer,integer)| 0)) (((|couple(integer,integer)| (get_x_couple_integer_integer Int) (get_y_couple_integer_integer Int)))))
 (declare-fun |bv′| () (Array |couple(integer,integer)| Bool))
(declare-fun bv () (Array |couple(integer,integer)| Bool))
(declare-fun n () Int)
(assert
 (let ((?x17 (|couple(integer,integer)| 4 0)))
 (let ((?x142 (|couple(integer,integer)| 3 1)))
 (let ((?x14 (|couple(integer,integer)| 2 0)))
 (let ((?x44 (|couple(integer,integer)| 1 1)))
 (let ((?x18 ((as const (Array |couple(integer,integer)| Bool)) false)))
 (let ((?x45 (store ?x18 ?x44 true)))
 (let ((?x145 (store (store (store ?x45 ?x14 true) ?x142 true) ?x17 true)))
 (let (($x146 (= |bv′| ?x145)))
 (let (($x147 (not $x146)))
 (let (($x230 (forall ((_smt_tmp32 Int) )(let (($x228 (exists ((_smt_tmp33 Int) )(let ((?x49 (|couple(integer,integer)| _smt_tmp32 _smt_tmp33)))
 (select |bv′| ?x49)))
 ))
 (let (($x136 (= _smt_tmp32 4)))
 (let (($x139 (or (or (or (= _smt_tmp32 1) (= _smt_tmp32 2)) (= _smt_tmp32 3)) $x136)))
 (=> $x139 $x228)))))
 ))
 (let (($x212 (forall ((_smt_tmp34 Int) (_smt_tmp35 Int) (_smt_tmp36 Int) )(let (($x52 (= _smt_tmp35 _smt_tmp36)))
 (let (($x117 (and (select |bv′| (|couple(integer,integer)| _smt_tmp34 _smt_tmp35)) (select |bv′| (|couple(integer,integer)| _smt_tmp34 _smt_tmp36)))))
 (=> $x117 $x52))))
 ))
 (let (($x201 (forall ((_smt_tmp37 Int) (_smt_tmp38 Int) )(let (($x88 (= _smt_tmp38 3)))
 (let (($x58 (= _smt_tmp37 4)))
 (let (($x99 (and (or (or (or (= _smt_tmp37 1) (= _smt_tmp37 2)) (= _smt_tmp37 3)) $x58) (or (or (or (= _smt_tmp38 0) (= _smt_tmp38 1)) (= _smt_tmp38 2)) $x88))))
 (let ((?x49 (|couple(integer,integer)| _smt_tmp37 _smt_tmp38)))
 (let (($x100 (select |bv′| ?x49)))
 (=> $x100 $x99)))))))
 ))
 (let (($x233 (and (and (and $x201 $x212) $x230) $x147)))
 (let (($x234 (not $x233)))
 (let (($x180 (exists ((_smt_tmp31 Int) )(let (($x174 (select bv (|couple(integer,integer)| 4 _smt_tmp31))))
 (let ((?x18 ((as const (Array |couple(integer,integer)| Bool)) false)))
 (let ((?x176 (store ?x18 (|couple(integer,integer)| 1 _smt_tmp31) true)))
 (let ((?x170 (lambda ((_couple_cst |couple(integer,integer)|) )(exists ((x Int) (_lambda_result_ Int) )(let ((?x49 (|couple(integer,integer)| x _lambda_result_)))
 (let (($x68 (= _couple_cst ?x49)))
 (let (($x166 (exists ((_smt_tmp30 Int) )(let (($x52 (= _lambda_result_ _smt_tmp30)))
 (and (select bv (|couple(integer,integer)| (- x 1) _smt_tmp30)) $x52)))
 ))
 (let (($x58 (= x 4)))
 (let (($x62 (or (or (= x 2) (= x 3)) $x58)))
 (and (and $x62 $x166) $x68)))))))
 )
 ))
 (and (= |bv′| ((as union (Array |couple(integer,integer)| Bool)) ?x170 ?x176)) $x174))))))
 ))
 (let (($x235 (and $x180 $x234)))
 (let (($x141 (forall ((_smt_tmp23 Int) )(let (($x135 (exists ((_smt_tmp24 Int) )(let ((?x49 (|couple(integer,integer)| _smt_tmp23 _smt_tmp24)))
 (select |bv′| ?x49)))
 ))
 (let (($x136 (= _smt_tmp23 4)))
 (let (($x139 (or (or (or (= _smt_tmp23 1) (= _smt_tmp23 2)) (= _smt_tmp23 3)) $x136)))
 (=> $x139 $x135)))))
 ))
 (let (($x119 (forall ((_smt_tmp25 Int) (_smt_tmp26 Int) (_smt_tmp27 Int) )(let (($x52 (= _smt_tmp26 _smt_tmp27)))
 (let (($x117 (and (select |bv′| (|couple(integer,integer)| _smt_tmp25 _smt_tmp26)) (select |bv′| (|couple(integer,integer)| _smt_tmp25 _smt_tmp27)))))
 (=> $x117 $x52))))
 ))
 (let (($x102 (forall ((_smt_tmp28 Int) (_smt_tmp29 Int) )(let (($x88 (= _smt_tmp29 3)))
 (let (($x58 (= _smt_tmp28 4)))
 (let (($x99 (and (or (or (or (= _smt_tmp28 1) (= _smt_tmp28 2)) (= _smt_tmp28 3)) $x58) (or (or (or (= _smt_tmp29 0) (= _smt_tmp29 1)) (= _smt_tmp29 2)) $x88))))
 (let ((?x49 (|couple(integer,integer)| _smt_tmp28 _smt_tmp29)))
 (let (($x100 (select |bv′| ?x49)))
 (=> $x100 $x99)))))))
 ))
 (let (($x150 (and (and (and $x102 $x119) $x141) $x147)))
 (let (($x151 (not $x150)))
 (let ((?x66 (lambda ((_couple_cst |couple(integer,integer)|) )(exists ((x Int) (_lambda_result_ Int) )(let ((?x49 (|couple(integer,integer)| x _lambda_result_)))
 (let (($x68 (= _couple_cst ?x49)))
 (let (($x57 (exists ((_smt_tmp22 Int) )(let (($x52 (= _lambda_result_ _smt_tmp22)))
 (and (select bv (|couple(integer,integer)| (- x 1) _smt_tmp22)) $x52)))
 ))
 (let (($x58 (= x 4)))
 (let (($x62 (or (or (= x 2) (= x 3)) $x58)))
 (and (and $x62 $x57) $x68)))))))
 )
 ))
 (let ((?x46 ((as union (Array |couple(integer,integer)| Bool)) ?x66 ?x45)))
 (let (($x47 (= |bv′| ?x46)))
 (let (($x152 (and $x47 $x151)))
 (let (($x236 (or $x152 $x235)))
 (let ((?x16 (|couple(integer,integer)| 3 0)))
 (let ((?x20 (store (store ?x18 (|couple(integer,integer)| 1 0) true) ?x14 true)))
 (let ((?x22 (store (store ?x20 ?x16 true) ?x17 true)))
 (let (($x23 (= bv ?x22)))
 (let (($x9 (= n 4)))
 (and (and $x9 $x23) $x236)))))))))))))))))))))))))))))))))
(check-sat)

(declare-datatypes ((|couple(integer,integer)| 0)) (((|couple(integer,integer)| (get_x_couple_integer_integer Int) (get_y_couple_integer_integer Int)))))
 (declare-fun |bv′| () (Array |couple(integer,integer)| Bool))
(declare-fun bv () (Array |couple(integer,integer)| Bool))
(declare-fun n () Int)
(assert
 (let ((?x20 (|couple(integer,integer)| 4 0)))
 (let ((?x89 (|couple(integer,integer)| 3 1)))
 (let ((?x15 (|couple(integer,integer)| 2 0)))
 (let ((?x26 (|couple(integer,integer)| 1 1)))
 (let ((?x9 ((as const (Array |couple(integer,integer)| Bool)) false)))
 (let ((?x27 (store ?x9 ?x26 true)))
 (let ((?x91 (store (store (store ?x27 ?x15 true) ?x89 true) ?x20 true)))
 (let (($x92 (= |bv′| ?x91)))
 (let (($x93 (not $x92)))
 (let (($x123 (forall ((_smt_tmp15 Int) )(let (($x121 (exists ((_smt_tmp16 Int) )(let ((?x46 (|couple(integer,integer)| _smt_tmp15 _smt_tmp16)))
 (select |bv′| ?x46)))
 ))
 (let (($x82 (= _smt_tmp15 4)))
 (let (($x83 (or (or (or (= _smt_tmp15 1) (= _smt_tmp15 2)) (= _smt_tmp15 3)) $x82)))
 (=> $x83 $x121)))))
 ))
 (let (($x119 (forall ((_smt_tmp17 Int) (_smt_tmp18 Int) (_smt_tmp19 Int) )(let (($x41 (= _smt_tmp18 _smt_tmp19)))
 (let (($x76 (and (select |bv′| (|couple(integer,integer)| _smt_tmp17 _smt_tmp18)) (select |bv′| (|couple(integer,integer)| _smt_tmp17 _smt_tmp19)))))
 (=> $x76 $x41))))
 ))
 (let (($x118 (forall ((_smt_tmp20 Int) (_smt_tmp21 Int) )(let (($x67 (= _smt_tmp21 3)))
 (let (($x34 (= _smt_tmp20 4)))
 (let (($x69 (and (or (or (or (= _smt_tmp20 1) (= _smt_tmp20 2)) (= _smt_tmp20 3)) $x34) (or (or (or (= _smt_tmp21 0) (= _smt_tmp21 1)) (= _smt_tmp21 2)) $x67))))
 (let ((?x46 (|couple(integer,integer)| _smt_tmp20 _smt_tmp21)))
 (let (($x57 (select |bv′| ?x46)))
 (=> $x57 $x69)))))))
 ))
 (let (($x125 (and (and (and $x118 $x119) $x123) $x93)))
 (let (($x126 (not $x125)))
 (let (($x117 (exists ((_smt_tmp11 (Array |couple(integer,integer)| Bool)) (_smt_tmp14 Int) )(let (($x115 (select bv (|couple(integer,integer)| 4 _smt_tmp14))))
 (let (($x112 (forall ((x Int) (_lambda_result_ Int) )(let (($x109 (exists ((_smt_tmp13 Int) )(let (($x41 (= _lambda_result_ _smt_tmp13)))
 (and (select bv (|couple(integer,integer)| (- x 1) _smt_tmp13)) $x41)))
 ))
 (let (($x34 (= x 4)))
 (let (($x35 (or (or (= x 2) (= x 3)) $x34)))
 (let (($x110 (and $x35 $x109)))
 (let ((?x46 (|couple(integer,integer)| x _lambda_result_)))
 (let (($x105 (select _smt_tmp11 ?x46)))
 (=> $x105 $x110))))))))
 ))
 (let (($x107 (forall ((x Int) (_lambda_result_ Int) )(let ((?x46 (|couple(integer,integer)| x _lambda_result_)))
 (let (($x105 (select _smt_tmp11 ?x46)))
 (let (($x102 (exists ((_smt_tmp12 Int) )(let (($x41 (= _lambda_result_ _smt_tmp12)))
 (and (select bv (|couple(integer,integer)| (- x 1) _smt_tmp12)) $x41)))
 ))
 (let (($x34 (= x 4)))
 (let (($x35 (or (or (= x 2) (= x 3)) $x34)))
 (let (($x103 (and $x35 $x102)))
 (=> $x103 $x105))))))))
 ))
 (let ((?x9 ((as const (Array |couple(integer,integer)| Bool)) false)))
 (let ((?x99 (store ?x9 (|couple(integer,integer)| 1 _smt_tmp14) true)))
 (and (and (and (= |bv′| ((as union (Array |couple(integer,integer)| Bool)) _smt_tmp11 ?x99)) $x107) $x112) $x115)))))))
 ))
 (let (($x127 (and $x117 $x126)))
 (let (($x86 (forall ((_smt_tmp4 Int) )(let (($x84 (exists ((_smt_tmp5 Int) )(let ((?x46 (|couple(integer,integer)| _smt_tmp4 _smt_tmp5)))
 (select |bv′| ?x46)))
 ))
 (let (($x82 (= _smt_tmp4 4)))
 (let (($x83 (or (or (or (= _smt_tmp4 1) (= _smt_tmp4 2)) (= _smt_tmp4 3)) $x82)))
 (=> $x83 $x84)))))
 ))
 (let (($x78 (forall ((_smt_tmp6 Int) (_smt_tmp7 Int) (_smt_tmp8 Int) )(let (($x41 (= _smt_tmp7 _smt_tmp8)))
 (let (($x76 (and (select |bv′| (|couple(integer,integer)| _smt_tmp6 _smt_tmp7)) (select |bv′| (|couple(integer,integer)| _smt_tmp6 _smt_tmp8)))))
 (=> $x76 $x41))))
 ))
 (let (($x71 (forall ((_smt_tmp9 Int) (_smt_tmp10 Int) )(let (($x67 (= _smt_tmp10 3)))
 (let (($x34 (= _smt_tmp9 4)))
 (let (($x69 (and (or (or (or (= _smt_tmp9 1) (= _smt_tmp9 2)) (= _smt_tmp9 3)) $x34) (or (or (or (= _smt_tmp10 0) (= _smt_tmp10 1)) (= _smt_tmp10 2)) $x67))))
 (let ((?x46 (|couple(integer,integer)| _smt_tmp9 _smt_tmp10)))
 (let (($x57 (select |bv′| ?x46)))
 (=> $x57 $x69)))))))
 ))
 (let (($x94 (and (and (and $x71 $x78) $x86) $x93)))
 (let (($x95 (not $x94)))
 (let (($x56 (exists ((_smt_tmp1 (Array |couple(integer,integer)| Bool)) )(let (($x54 (forall ((x Int) (_lambda_result_ Int) )(let (($x51 (exists ((_smt_tmp3 Int) )(let (($x41 (= _lambda_result_ _smt_tmp3)))
 (and (select bv (|couple(integer,integer)| (- x 1) _smt_tmp3)) $x41)))
 ))
 (let (($x34 (= x 4)))
 (let (($x35 (or (or (= x 2) (= x 3)) $x34)))
 (let (($x52 (and $x35 $x51)))
 (let ((?x46 (|couple(integer,integer)| x _lambda_result_)))
 (let (($x47 (select _smt_tmp1 ?x46)))
 (=> $x47 $x52))))))))
 ))
 (let (($x49 (forall ((x Int) (_lambda_result_ Int) )(let ((?x46 (|couple(integer,integer)| x _lambda_result_)))
 (let (($x47 (select _smt_tmp1 ?x46)))
 (let (($x43 (exists ((_smt_tmp2 Int) )(let (($x41 (= _lambda_result_ _smt_tmp2)))
 (and (select bv (|couple(integer,integer)| (- x 1) _smt_tmp2)) $x41)))
 ))
 (let (($x34 (= x 4)))
 (let (($x35 (or (or (= x 2) (= x 3)) $x34)))
 (let (($x44 (and $x35 $x43)))
 (=> $x44 $x47))))))))
 ))
 (let ((?x26 (|couple(integer,integer)| 1 1)))
 (let ((?x9 ((as const (Array |couple(integer,integer)| Bool)) false)))
 (let ((?x27 (store ?x9 ?x26 true)))
 (and (and (= |bv′| ((as union (Array |couple(integer,integer)| Bool)) _smt_tmp1 ?x27)) $x49) $x54)))))))
 ))
 (let (($x96 (and $x56 $x95)))
 (let (($x128 (or $x96 $x127)))
 (let ((?x18 (|couple(integer,integer)| 3 0)))
 (let ((?x16 (store (store ?x9 (|couple(integer,integer)| 1 0) true) ?x15 true)))
 (let ((?x21 (store (store ?x16 ?x18 true) ?x20 true)))
 (let (($x22 (= bv ?x21)))
 (let (($x7 (= n 4)))
 (and (and $x7 $x22) $x128)))))))))))))))))))))))))))))))
(check-sat)