(declare-fun it118 () Int)
(declare-fun it132 () Int)
(declare-fun iat119 () (Array Int Int))
(declare-fun iat131 () (Array Int Int))
(declare-fun it111 () Int)
(declare-fun it130 () Int)
(declare-fun iat113 () (Array Int Int))
(declare-fun iat129 () (Array Int Int))
(declare-fun it127 () Int)
(declare-fun it117 () Int)
(declare-fun it126 () Int)
(declare-fun it125 () Int)
(declare-fun it110 () Int)
(declare-fun it124 () Int)
(declare-fun it121 () Int)
(declare-fun i1 () Int)
(declare-fun it158 () Int)
(declare-fun iat157 () (Array Int Int))
(declare-fun it156 () Int)
(declare-fun iat155 () (Array Int Int))
(declare-fun it153 () Int)
(declare-fun it135 () Int)
(declare-fun it152 () Int)
(declare-fun it136 () Int)
(declare-fun it151 () Int)
(declare-fun it150 () Int)
(declare-fun it122 () Int)
(declare-fun it133 () Int)
(declare-fun it134 () Int)
(declare-fun it184 () Int)
(declare-fun iat183 () (Array Int Int))
(declare-fun it182 () Int)
(declare-fun iat181 () (Array Int Int))
(declare-fun it179 () Int)
(declare-fun it161 () Int)
(declare-fun it178 () Int)
(declare-fun it162 () Int)
(declare-fun it177 () Int)
(declare-fun it176 () Int)
(declare-fun it148 () Int)
(declare-fun it159 () Int)
(declare-fun it160 () Int)
(declare-fun it210 () Int)
(declare-fun it236 () Int)
(declare-fun iat209 () (Array Int Int))
(declare-fun iat235 () (Array Int Int))
(declare-fun it208 () Int)
(declare-fun it234 () Int)
(declare-fun iat207 () (Array Int Int))
(declare-fun it203 () Int)
(declare-fun it202 () Int)
(declare-fun iat233 () (Array Int Int))
(declare-fun it205 () Int)
(declare-fun it231 () Int)
(declare-fun it204 () Int)
(declare-fun it230 () Int)
(declare-fun it229 () Int)
(declare-fun it228 () Int)
(declare-fun it174 () Int)
(declare-fun it187 () Int)
(declare-fun it188 () Int)
(declare-fun it185 () Int)
(declare-fun it186 () Int)
(declare-fun it175 () Int)
(declare-fun it213 () Int)
(declare-fun it214 () Int)
(declare-fun it200 () Int)
(declare-fun it211 () Int)
(declare-fun it212 () Int)
(declare-fun it247 () Int)
(declare-fun it262 () Int)
(declare-fun iat261 () (Array Int Int))
(declare-fun it248 () Int)
(declare-fun it260 () Int)
(declare-fun iat259 () (Array Int Int))
(declare-fun it257 () Int)
(declare-fun it249 () Int)
(declare-fun it256 () Int)
(declare-fun it251 () Int)
(declare-fun it255 () Int)
(declare-fun it250 () Int)
(declare-fun it254 () Int)
(declare-fun it226 () Int)
(assert (and (= i1 0)
     (not (<= it110 0))
     (not (<= it111 0))
     (not (<= it117 0))
     (or (not (<= it117 0)) (not (>= it117 1)))
     (= it121 50)
     (= (+ it124 (* (- 1) it110)) 0)
     (= it125 0)
     (= (+ it126 (* (- 1) it117)) 0)
     (= it127 3)
     (= iat129 iat113)
     (= (+ it130 (* (- 1) it111)) 0)
     (= iat131 iat119)
     (= (+ it132 (* (- 1) it118)) 0)))
(assert (let ((a!1 (or (not (>= it124 1)) (not (<= (+ it124 it125) 0))))
      (a!2 (not (<= (+ (* (- 1) it125) it126) 0)))
      (a!3 (not (<= (+ it125 (* (- 1) it126)) (- 1))))
      (a!6 (or (not (>= it130 1)) (not (<= (+ it130 it125) 0))))
      (a!7 (store iat131
                  (+ it130 it125)
                  (+ (select iat129 (+ it124 it125)) it132)))
      (a!10 (or (not (>= it125 1)) (not (<= (+ it125 it132) 0))))
      (a!11 (= (+ (select iat129 (+ it125 it132)) (* (- 1) it124)) 42))
      (a!12 (not (<= (+ (* (- 1) it132) it130) 0)))
      (a!13 (not (<= (+ it132 (* (- 1) it130)) (- 1)))))
(let ((a!4 (and a!1
                a!2
                (not (<= it124 0))
                (or a!2 a!3)
                (= it127 3)
                (= it122 25)
                (= (+ it150 (* (- 1) it124)) 0)
                (= (+ it151 (* (- 1) it125)) 1)
                (= (+ it152 (* (- 1) it126)) 0)
                (= it153 3)
                (= iat155 (store iat129 (+ it124 it125) 42))
                (= (+ it156 (* (- 1) it130)) 0)
                (= iat157 iat131)
                (= (+ it158 (* (- 1) it132)) 0)))
      (a!5 (and a!3
                (or a!2 a!3)
                (= it127 3)
                (= it122 30)
                (= (+ it150 (* (- 1) it124)) 0)
                (= it151 0)
                (= (+ it152 (* (- 1) it126)) 0)
                (= it153 4)
                (= iat155 iat129)
                (= (+ it156 (* (- 1) it130)) 0)
                (= iat157 iat131)
                (= (+ it158 (* (- 1) it132)) 0)))
      (a!8 (and a!1
                a!6
                a!2
                (not (<= it124 0))
                (not (<= it130 0))
                (or a!2 a!3)
                (= it127 4)
                (= it122 36)
                (= (+ it150 (* (- 1) it124)) 0)
                (= (+ it151 (* (- 1) it125)) 1)
                (= (+ it152 (* (- 1) it126)) 0)
                (= it153 4)
                (= iat155 iat129)
                (= (+ it156 (* (- 1) it130)) 0)
                (= iat157 a!7)
                (= (+ it158 (* (- 1) it132)) 0)))
      (a!9 (and a!3
                (or a!2 a!3)
                (= it127 4)
                (= it122 39)
                (= (+ it150 (* (- 1) it132)) 0)
                (= (+ it151 (* (- 1) it134)) 0)
                (= (+ it152 (* (- 1) it133)) 0)
                (= it153 5)
                (= iat155 iat131)
                (= (+ it156 (* (- 1) it126)) 0)
                (= iat157 iat131)
                (= it158 0)))
      (a!14 (and a!10
                 a!11
                 (not (<= it125 0))
                 a!12
                 (or a!12 a!13)
                 (= it127 5)
                 (= it122 46)
                 (= (+ it150 (* (- 1) it124)) 0)
                 (= (+ it151 (* (- 1) it136)) 0)
                 (= (+ it152 (* (- 1) it135)) 0)
                 (= it153 5)
                 (= iat155 iat129)
                 (= (+ it156 (* (- 1) it130)) 0)
                 (= iat157 iat131)
                 (= (+ it158 (* (- 1) it132)) 1))))
  (or a!4 a!5 a!8 a!9 a!14))))
(assert (let ((a!1 (or (not (>= it150 1)) (not (<= (+ it150 it151) 0))))
      (a!2 (not (<= (+ (* (- 1) it151) it152) 0)))
      (a!3 (not (<= (+ it151 (* (- 1) it152)) (- 1))))
      (a!6 (or (not (>= it156 1)) (not (<= (+ it156 it151) 0))))
      (a!7 (store iat157
                  (+ it156 it151)
                  (+ (select iat155 (+ it150 it151)) it158)))
      (a!10 (or (not (>= it151 1)) (not (<= (+ it151 it158) 0))))
      (a!11 (= (+ (select iat155 (+ it151 it158)) (* (- 1) it150)) 42))
      (a!12 (not (<= (+ (* (- 1) it158) it156) 0)))
      (a!13 (not (<= (+ it158 (* (- 1) it156)) (- 1)))))
(let ((a!4 (and a!1
                a!2
                (not (<= it150 0))
                (or a!2 a!3)
                (= it153 3)
                (= it148 25)
                (= (+ it176 (* (- 1) it150)) 0)
                (= (+ it177 (* (- 1) it151)) 1)
                (= (+ it178 (* (- 1) it152)) 0)
                (= it179 3)
                (= iat181 (store iat155 (+ it150 it151) 42))
                (= (+ it182 (* (- 1) it156)) 0)
                (= iat183 iat157)
                (= (+ it184 (* (- 1) it158)) 0)))
      (a!5 (and a!3
                (or a!2 a!3)
                (= it153 3)
                (= it148 30)
                (= (+ it176 (* (- 1) it150)) 0)
                (= it177 0)
                (= (+ it178 (* (- 1) it152)) 0)
                (= it179 4)
                (= iat181 iat155)
                (= (+ it182 (* (- 1) it156)) 0)
                (= iat183 iat157)
                (= (+ it184 (* (- 1) it158)) 0)))
      (a!8 (and a!1
                a!6
                a!2
                (not (<= it150 0))
                (not (<= it156 0))
                (or a!2 a!3)
                (= it153 4)
                (= it148 36)
                (= (+ it176 (* (- 1) it150)) 0)
                (= (+ it177 (* (- 1) it151)) 1)
                (= (+ it178 (* (- 1) it152)) 0)
                (= it179 4)
                (= iat181 iat155)
                (= (+ it182 (* (- 1) it156)) 0)
                (= iat183 a!7)
                (= (+ it184 (* (- 1) it158)) 0)))
      (a!9 (and a!3
                (or a!2 a!3)
                (= it153 4)
                (= it148 39)
                (= (+ it176 (* (- 1) it158)) 0)
                (= (+ it177 (* (- 1) it160)) 0)
                (= (+ it178 (* (- 1) it159)) 0)
                (= it179 5)
                (= iat181 iat157)
                (= (+ it182 (* (- 1) it152)) 0)
                (= iat183 iat157)
                (= it184 0)))
      (a!14 (and a!10
                 a!11
                 (not (<= it151 0))
                 a!12
                 (or a!12 a!13)
                 (= it153 5)
                 (= it148 46)
                 (= (+ it176 (* (- 1) it150)) 0)
                 (= (+ it177 (* (- 1) it162)) 0)
                 (= (+ it178 (* (- 1) it161)) 0)
                 (= it179 5)
                 (= iat181 iat155)
                 (= (+ it182 (* (- 1) it156)) 0)
                 (= iat183 iat157)
                 (= (+ it184 (* (- 1) it158)) 1))))
  (or a!4 a!5 a!8 a!9 a!14))))
(assert (let ((a!1 (not (<= (+ (* (- 1) it176) (* (- 1) it177)) (- 1))))
      (a!2 (not (<= (+ it177 (* (- 1) it178)) (- 1))))
      (a!3 (not (= (+ it202 (* (- 1) it176)) 0)))
      (a!4 (not (= (+ it203 (* (- 1) it177)) 1)))
      (a!5 (not (= (+ it204 (* (- 1) it178)) 0)))
      (a!6 (not (= (+ it205 (* (- 1) it179)) 0)))
      (a!7 (not (= (+ it208 (* (- 1) it182)) 0)))
      (a!8 (= iat207
              (lambda ((it31 Int))
                (let ((a!1 (not (<= (+ it31 (* (- 1) it176) (* (- 1) it177))
                                    (- 1))))
                      (a!2 (not (<= (+ (* (- 1) it31) it176 it177) (- 1)))))
                  (ite (and a!1 a!2) 42 (select iat181 it31))))))
      (a!9 (not (= (+ it210 (* (- 1) it184)) 0)))
      (a!10 (not (<= (+ (* (- 1) it202) (* (- 1) it203)) (- 1))))
      (a!11 (not (<= (+ it203 (* (- 1) it204)) (- 1))))
      (a!12 (not (= (+ it228 (* (- 1) it202)) 0)))
      (a!13 (not (= (+ it229 (* (- 1) it203)) 1)))
      (a!14 (not (= (+ it230 (* (- 1) it204)) 0)))
      (a!15 (not (= (+ it231 (* (- 1) it205)) 0)))
      (a!16 (= iat233
               (lambda ((it31 Int))
                 (let ((a!1 (not (<= (+ it31 (* (- 1) it202) (* (- 1) it203))
                                     (- 1))))
                       (a!2 (not (<= (+ (* (- 1) it31) it202 it203) (- 1)))))
                   (ite (and a!1 a!2) 42 (select iat207 it31))))))
      (a!17 (not (= (+ it234 (* (- 1) it208)) 0)))
      (a!18 (not (= (+ it236 (* (- 1) it210)) 0))))
  (and (or (not (= it179 3))
           (= it174 62)
           a!1
           a!2
           (not (>= it176 1))
           a!3
           a!4
           a!5
           a!6
           a!7
           (not a!8)
           (not (= iat209 iat183))
           a!9)
       (or (not (= it174 62))
           a!10
           a!11
           (not (>= it202 1))
           (not (= it205 3))
           a!12
           a!13
           a!14
           a!15
           (not a!16)
           a!17
           (not (= iat235 iat209))
           a!18))))
(assert (let ((a!1 (not (<= (+ it178 (* (- 1) it177) (* (- 1) it175)) (- 1))))
      (a!2 (= iat207
              (lambda ((it31 Int))
                (let ((a!1 (not (<= (+ it31 (* (- 1) it176) (* (- 1) it177))
                                    (- 1))))
                      (a!2 (not (<= (+ it175 (* (- 1) it31) it176 it177) 0))))
                  (ite (and a!1 a!2) 42 (select iat181 it31))))))
      (a!4 (or (not (>= it176 1)) (not (<= (+ it176 it177) 0))))
      (a!5 (not (<= (+ (* (- 1) it177) it178) 0)))
      (a!6 (not (<= (+ it177 (* (- 1) it178)) (- 1))))
      (a!9 (or (not (>= it182 1)) (not (<= (+ it182 it177) 0))))
      (a!10 (store iat183
                   (+ it182 it177)
                   (+ (select iat181 (+ it176 it177)) it184)))
      (a!13 (or (not (>= it177 1)) (not (<= (+ it177 it184) 0))))
      (a!14 (= (+ (select iat181 (+ it177 it184)) (* (- 1) it176)) 42))
      (a!15 (not (<= (+ (* (- 1) it184) it182) 0)))
      (a!16 (not (<= (+ it184 (* (- 1) it182)) (- 1)))))
(let ((a!3 (and (not (<= it175 0))
                (not (<= (+ it176 it177) 0))
                a!1
                (not (<= it176 0))
                (= it179 3)
                (= it174 62)
                (= (+ it202 (* (- 1) it176)) 0)
                (= (+ it203 (* (- 1) it175) (* (- 1) it177)) 0)
                (= (+ it204 (* (- 1) it178)) 0)
                (= (+ it205 (* (- 1) it179)) 0)
                a!2
                (= (+ it208 (* (- 1) it182)) 0)
                (= iat209 iat183)
                (= (+ it210 (* (- 1) it184)) 0)))
      (a!7 (and a!4
                a!5
                (not (<= it176 0))
                (or a!6 a!5)
                (= it179 3)
                (= it174 25)
                (= (+ it202 (* (- 1) it176)) 0)
                (= (+ it203 (* (- 1) it177)) 1)
                (= (+ it204 (* (- 1) it178)) 0)
                (= it205 3)
                (= iat207 (store iat181 (+ it176 it177) 42))
                (= (+ it208 (* (- 1) it182)) 0)
                (= iat209 iat183)
                (= (+ it210 (* (- 1) it184)) 0)))
      (a!8 (and a!6
                (or a!6 a!5)
                (= it179 3)
                (= it174 30)
                (= (+ it202 (* (- 1) it176)) 0)
                (= it203 0)
                (= (+ it204 (* (- 1) it178)) 0)
                (= it205 4)
                (= iat207 iat181)
                (= (+ it208 (* (- 1) it182)) 0)
                (= iat209 iat183)
                (= (+ it210 (* (- 1) it184)) 0)))
      (a!11 (and a!4
                 a!9
                 a!5
                 (not (<= it176 0))
                 (not (<= it182 0))
                 (or a!6 a!5)
                 (= it179 4)
                 (= it174 36)
                 (= (+ it202 (* (- 1) it176)) 0)
                 (= (+ it203 (* (- 1) it177)) 1)
                 (= (+ it204 (* (- 1) it178)) 0)
                 (= it205 4)
                 (= iat207 iat181)
                 (= (+ it208 (* (- 1) it182)) 0)
                 (= iat209 a!10)
                 (= (+ it210 (* (- 1) it184)) 0)))
      (a!12 (and a!6
                 (or a!6 a!5)
                 (= it179 4)
                 (= it174 39)
                 (= (+ it202 (* (- 1) it184)) 0)
                 (= (+ it203 (* (- 1) it186)) 0)
                 (= (+ it204 (* (- 1) it185)) 0)
                 (= it205 5)
                 (= iat207 iat183)
                 (= (+ it208 (* (- 1) it178)) 0)
                 (= iat209 iat183)
                 (= it210 0)))
      (a!17 (and a!13
                 a!14
                 (not (<= it177 0))
                 a!15
                 (or a!15 a!16)
                 (= it179 5)
                 (= it174 46)
                 (= (+ it202 (* (- 1) it176)) 0)
                 (= (+ it203 (* (- 1) it188)) 0)
                 (= (+ it204 (* (- 1) it187)) 0)
                 (= it205 5)
                 (= iat207 iat181)
                 (= (+ it208 (* (- 1) it182)) 0)
                 (= iat209 iat183)
                 (= (+ it210 (* (- 1) it184)) 1))))
  (or a!3 a!7 a!8 a!11 a!12 a!17))))
(assert (let ((a!1 (or (not (>= it202 1)) (not (<= (+ it202 it203) 0))))
      (a!2 (not (<= (+ (* (- 1) it203) it204) 0)))
      (a!3 (not (<= (+ it203 (* (- 1) it204)) (- 1))))
      (a!6 (or (not (>= it208 1)) (not (<= (+ it208 it203) 0))))
      (a!7 (store iat209
                  (+ it208 it203)
                  (+ (select iat207 (+ it202 it203)) it210)))
      (a!10 (or (not (>= it203 1)) (not (<= (+ it203 it210) 0))))
      (a!11 (= (+ (select iat207 (+ it203 it210)) (* (- 1) it202)) 42))
      (a!12 (not (<= (+ (* (- 1) it210) it208) 0)))
      (a!13 (not (<= (+ it210 (* (- 1) it208)) (- 1)))))
(let ((a!4 (and a!1
                a!2
                (not (<= it202 0))
                (or a!3 a!2)
                (= it205 3)
                (= it200 25)
                (= (+ it228 (* (- 1) it202)) 0)
                (= (+ it229 (* (- 1) it203)) 1)
                (= (+ it230 (* (- 1) it204)) 0)
                (= it231 3)
                (= iat233 (store iat207 (+ it202 it203) 42))
                (= (+ it234 (* (- 1) it208)) 0)
                (= iat235 iat209)
                (= (+ it236 (* (- 1) it210)) 0)))
      (a!5 (and a!3
                (or a!3 a!2)
                (= it205 3)
                (= it200 30)
                (= (+ it228 (* (- 1) it202)) 0)
                (= it229 0)
                (= (+ it230 (* (- 1) it204)) 0)
                (= it231 4)
                (= iat233 iat207)
                (= (+ it234 (* (- 1) it208)) 0)
                (= iat235 iat209)
                (= (+ it236 (* (- 1) it210)) 0)))
      (a!8 (and a!1
                a!6
                a!2
                (not (<= it202 0))
                (not (<= it208 0))
                (or a!3 a!2)
                (= it205 4)
                (= it200 36)
                (= (+ it228 (* (- 1) it202)) 0)
                (= (+ it229 (* (- 1) it203)) 1)
                (= (+ it230 (* (- 1) it204)) 0)
                (= it231 4)
                (= iat233 iat207)
                (= (+ it234 (* (- 1) it208)) 0)
                (= iat235 a!7)
                (= (+ it236 (* (- 1) it210)) 0)))
      (a!9 (and a!3
                (or a!3 a!2)
                (= it205 4)
                (= it200 39)
                (= (+ it228 (* (- 1) it210)) 0)
                (= (+ it229 (* (- 1) it212)) 0)
                (= (+ it230 (* (- 1) it211)) 0)
                (= it231 5)
                (= iat233 iat209)
                (= (+ it234 (* (- 1) it204)) 0)
                (= iat235 iat209)
                (= it236 0)))
      (a!14 (and a!10
                 a!11
                 (not (<= it203 0))
                 a!12
                 (or a!12 a!13)
                 (= it205 5)
                 (= it200 46)
                 (= (+ it228 (* (- 1) it202)) 0)
                 (= (+ it229 (* (- 1) it214)) 0)
                 (= (+ it230 (* (- 1) it213)) 0)
                 (= it231 5)
                 (= iat233 iat207)
                 (= (+ it234 (* (- 1) it208)) 0)
                 (= iat235 iat209)
                 (= (+ it236 (* (- 1) it210)) 1))))
  (or a!4 a!5 a!8 a!9 a!14))))
(assert (let ((a!1 (or (not (>= it229 1)) (not (<= (+ it229 it236) 0))))
      (a!2 (= (+ (select iat233 (+ it229 it236)) (* (- 1) it228)) 42))
      (a!3 (not (<= (+ (* (- 1) it236) it234) 0)))
      (a!4 (not (<= (+ it236 (* (- 1) it234)) (- 1)))))
  (and a!1
       (not a!2)
       (not (<= it229 0))
       a!3
       (or a!3 a!4)
       (= it231 5)
       (= it226 56)
       (= (+ it254 (* (- 1) it250)) 0)
       (= (+ it255 (* (- 1) it251)) 0)
       (= (+ it256 (* (- 1) it249)) 0)
       (= it257 1)
       (= iat259 iat233)
       (= (+ it260 (* (- 1) it248)) 0)
       (= iat261 iat235)
       (= (+ it262 (* (- 1) it247)) 0))))
(check-sat)
(get-info :reason-unknown)