src/HOL/Boogie/Examples/cert/VCC_maximum

tuned signature;

(benchmark Isabelle
:extrasorts ( T2 T5 T8 T3 T15 T16 T4 T1 T6 T17 T11 T18 T7 T9 T13 T14 T12 T10 T19)
:extrafuns (
  (uf_9 T2)
  (uf_48 T5 T3 T2)
  (uf_26 T5)
  (uf_126 T5 T15 T5)
  (uf_66 T5 Int T3 T5)
  (uf_43 T3 Int T5)
  (uf_116 T5 Int)
  (uf_13 T5 T3)
  (uf_81 Int Int Int)
  (uf_80 Int Int Int)
  (uf_46 T4 T4 T5 T3 T2)
  (uf_121 T5)
  (uf_53 T4 T5 T6)
  (uf_163 T5 T6)
  (uf_72 T3 Int Int Int)
  (uf_124 T3 Int T3)
  (uf_25 T4 T5 T5)
  (uf_24 T4 T5 T2)
  (uf_255 T3)
  (uf_254 T3)
  (uf_94 T3)
  (uf_90 T3)
  (uf_87 T3)
  (uf_83 T3)
  (uf_7 T3)
  (uf_91 T3)
  (uf_4 T3)
  (uf_84 T3)
  (uf_70 T3 Int Int Int)
  (uf_69 Int Int Int)
  (uf_73 T3 Int Int)
  (uf_101 T3 Int Int Int)
  (uf_100 Int Int Int)
  (uf_71 T3 Int Int Int)
  (uf_27 T4 T5 T2)
  (uf_16 T4 T5 T6)
  (uf_128 T4 T5 T6)
  (uf_20 T4 T9)
  (uf_139 T3 Int)
  (uf_5 T3)
  (uf_291 T1)
  (uf_79 Int Int)
  (uf_207 T4 T4 T5 T5 T2)
  (uf_259 T3 T3 T3)
  (uf_61 T4 T5 T2)
  (uf_169 T4 T4 T5 T5 T4)
  (uf_59 T4 T13)
  (uf_258 T3)
  (uf_240 T3)
  (uf_284 T16)
  (uf_96 Int)
  (uf_93 Int)
  (uf_89 Int)
  (uf_86 Int)
  (uf_78 Int)
  (uf_77 Int)
  (uf_76 Int)
  (uf_75 Int)
  (uf_253 Int)
  (uf_95 Int)
  (uf_92 Int)
  (uf_88 Int)
  (uf_85 Int)
  (uf_6 T3 T3)
  (uf_224 T17 T17 T2)
  (uf_171 T4 T5 T5 T11)
  (uf_153 T6 T6 T2)
  (uf_15 T5 T6 T2)
  (uf_135 T14 T5)
  (uf_37 T3)
  (uf_279 T1)
  (uf_281 T1)
  (uf_287 T1)
  (uf_122 T2 T2)
  (uf_12 T3 T8)
  (uf_114 T4 T5 Int)
  (uf_113 T4 T5 Int)
  (uf_112 T4 T5 Int)
  (uf_111 T4 T5 Int)
  (uf_110 T4 T5 Int)
  (uf_109 T4 T5 Int)
  (uf_108 T4 T5 Int)
  (uf_107 T4 T5 Int)
  (uf_38 T4 T5 Int)
  (uf_145 T5 T6 T2)
  (uf_147 T5 T6 T2)
  (uf_41 T4 T12)
  (uf_172 T4 T5 Int)
  (uf_82 T3 Int Int)
  (uf_232 T4 T5 T18)
  (uf_188 T4 T5 T5 T5 T5)
  (uf_65 T4 T5 T3 Int T2)
  (uf_42 T5)
  (uf_230 T17)
  (uf_179 T4 T4 T5 T3 T2)
  (uf_215 T11 T5)
  (uf_170 T12 T5 T11 T12)
  (uf_251 T13 T5 T14 T13)
  (uf_266 T3 T3)
  (uf_234 T18 T4)
  (uf_257 T3)
  (uf_99 Int Int Int Int Int Int)
  (uf_55 T4 T2)
  (uf_60 Int T3 T5)
  (uf_245 Int T5)
  (uf_220 T5 T15 Int)
  (uf_196 T4 T5 T5 T2)
  (uf_264 T3 T3)
  (uf_142 T3 Int)
  (uf_222 T17 T15 Int)
  (uf_40 T12 T5 T11)
  (uf_58 T13 T5 T14)
  (uf_152 T6)
  (uf_157 T6 T6 T6)
  (uf_177 T9 T5 Int T9)
  (uf_174 T4 T5 T5 T4)
  (uf_106 T3 Int Int Int)
  (uf_103 T3 Int Int Int)
  (uf_102 T3 Int Int Int)
  (uf_104 T3 Int Int Int)
  (uf_105 T3 Int Int Int)
  (uf_241 T15 Int T15)
  (uf_50 T5 T5 T2)
  (uf_246 Int T15)
  (uf_51 T4 T2)
  (uf_195 T4 T5 T5 T2)
  (uf_262 T8)
  (uf_161 T5 Int T5)
  (uf_265 T3 T3)
  (uf_47 T4 T5 T2)
  (uf_229 T17 T15 Int T17)
  (uf_19 T9 T5 Int)
  (uf_154 T6 T6 T2)
  (uf_175 T4 T5 T5 T11)
  (uf_176 T4 T5 Int T4)
  (uf_192 T7 T6)
  (uf_219 T3)
  (uf_268 T3)
  (uf_289 T1)
  (uf_132 T5 T3 Int T6)
  (uf_138 T5 T5 T2)
  (uf_276 T19 Int)
  (uf_130 T5 T6)
  (uf_44 T4 T2)
  (uf_261 T8)
  (uf_250 T3 T3 Int)
  (uf_249 T3 T3 Int)
  (uf_181 T4 T4 T2)
  (uf_117 T5 Int)
  (uf_119 T5 Int)
  (uf_118 T5 Int)
  (uf_120 T5 Int)
  (uf_160 T5 Int T5)
  (uf_235 T18)
  (uf_49 T4 T5 T2)
  (uf_267 T3)
  (uf_143 T3 Int)
  (uf_54 T5 T5 T2)
  (uf_144 T3 T3)
  (uf_237 T15 Int)
  (uf_74 T3 Int T2)
  (uf_125 T5 T5 Int)
  (uf_28 Int T5)
  (uf_141 T3 T2)
  (uf_260 T3 T2)
  (uf_22 T3 T2)
  (uf_159 T5 T5 T5)
  (uf_29 T5 Int)
  (uf_201 T4 T5 T3 T5)
  (uf_11 T4 T5 T7)
  (uf_131 T6 T6 T2)
  (uf_149 T6)
  (uf_39 T11 Int)
  (uf_217 T11 Int)
  (uf_68 T4 T5 T2)
  (uf_275 T1)
  (uf_134 T5 T3 Int T6)
  (uf_189 T5 T7)
  (uf_140 T5 T3 T5)
  (uf_208 T3 T2)
  (uf_221 Int Int T2)
  (uf_151 T5 T6)
  (uf_162 T4 T5 T6)
  (uf_233 T18 Int)
  (uf_256 T3)
  (uf_286 T1)
  (uf_288 T1)
  (uf_295 T1)
  (uf_290 T1)
  (uf_301 T1)
  (uf_243 T15 T15)
  (uf_244 T15 Int)
  (uf_45 T4 T5 T2)
  (uf_203 T4 T2)
  (uf_148 T5 T2)
  (uf_283 Int T5 T2)
  (uf_57 T3 T2)
  (uf_263 T8)
  (uf_14 T8)
  (uf_156 T6 T6 T6)
  (uf_306 T1)
  (uf_302 T1)
  (uf_178 T4 T4 T2)
  (uf_183 T10 T5 Int)
  (uf_62 Int Int)
  (uf_63 Int Int)
  (uf_200 T4 T5 T5 T16 T2)
  (uf_34 Int T6)
  (uf_225 Int T17)
  (uf_56 T3 T2)
  (uf_35 T6 Int)
  (uf_231 T17 T15 Int Int Int Int T17)
  (uf_226 T17 Int)
  (uf_150 T6 Int)
  (uf_18 T5 T2)
  (uf_202 T1 T4 T2)
  (uf_198 T4 T5 T5 T16 T2)
  (uf_32 Int T7)
  (uf_185 T3 T15 T15 T2)
  (uf_211 T4 T5 T2)
  (uf_228 T3 T2)
  (uf_214 T3 T15)
  (uf_155 T6 T6 T6)
  (uf_206 T4 T4 T5 T3 T2)
  (uf_136 T14 T2)
  (uf_33 T7 Int)
  (uf_236 T5 T15 T5)
  (uf_173 T4 Int)
  (uf_133 T5 T6 T6 Int)
  (uf_186 T5 T5 T2)
  (uf_247 T3 T3 Int Int T2)
  (uf_227 T3 T15 T3 T2)
  (uf_127 T4 T5 T6)
  (uf_23 T3 T2)
  (uf_184 T4 T5 T10)
  (uf_97 Int Int Int Int Int)
  (uf_8 T4 T4 T5 T6 T2)
  (uf_10 T7 T5 Int)
  (uf_238 T15 T3)
  (uf_210 T4 T5 T2)
  (uf_180 T3 T15 T2)
  (uf_252 T3)
  (uf_64 Int Int T5)
  (uf_98 Int Int Int Int Int)
  (uf_277 Int)
  (uf_164 T4 T2)
  (uf_21 T4 T4 T6 T2)
  (uf_115 T5 T5 Int)
  (uf_167 T5)
  (uf_30 Int T10)
  (uf_168 Int)
  (uf_17 T4 T4 T6 T2)
  (uf_31 T10 Int)
  (uf_239 T5 T15 Int)
  (uf_166 T3)
  (uf_191 T4 T2)
  (uf_129 T5 T3 Int T6)
  (uf_123 T4 T4 T5 T3 T2)
  (uf_223 T15 T15)
  (uf_158 T5 T6)
  (uf_137 T4 T5 T3 Int T2 T2)
  (uf_204 T4 T4 T5 T3 T2)
  (uf_187 T15 Int T2)
  (uf_2 T1)
  (uf_190 T15 T2)
  (uf_194 T15 Int T3 T2)
  (uf_273 T4)
  (uf_270 Int)
  (uf_294 Int)
  (uf_305 Int)
  (uf_297 Int)
  (uf_269 Int)
  (uf_274 Int)
  (uf_272 Int)
  (uf_285 Int)
  (uf_292 Int)
  (uf_300 Int)
  (uf_303 Int)
  (uf_296 Int)
  (uf_299 Int)
  (uf_271 Int)
  (uf_282 Int)
  (uf_293 Int)
  (uf_304 Int)
  (uf_298 Int)
 )
:extrapreds (
  (up_199 T4 T5 T16)
  (up_146 T5 T6)
  (up_213 T14)
  (up_209 T4 T5 T3)
  (up_248 T3 T3)
  (up_218 T11)
  (up_36 T3)
  (up_1 Int T1)
  (up_212 T11)
  (up_3 Int T3)
  (up_182 Int)
  (up_242 T15)
  (up_216)
  (up_193 T2)
  (up_278 T4 T1 T1 Int T3)
  (up_52 T6)
  (up_67 T14)
  (up_280 T4 T1 T1 T5 T3)
  (up_197 T3)
  (up_165 T4)
  (up_205 T4 T4 T5 T3)
 )
:assumption (up_1 1 uf_2)
:assumption (up_3 1 uf_4)
:assumption (= uf_5 (uf_6 uf_7))
:assumption (forall (?x1 T4) (?x2 T4) (?x3 T5) (?x4 T6) (iff (= (uf_8 ?x1 ?x2 ?x3 ?x4) uf_9) (and (forall (?x5 T5) (implies (and (= (uf_12 (uf_13 ?x5)) uf_14) (not (= (uf_15 ?x5 ?x4) uf_9))) (= (uf_10 (uf_11 ?x1 ?x3) ?x5) (uf_10 (uf_11 ?x2 ?x3) ?x5))) :pat { (uf_10 (uf_11 ?x2 ?x3) ?x5) }) (= (uf_16 ?x1 ?x3) (uf_16 ?x2 ?x3)))) :pat { (uf_8 ?x1 ?x2 ?x3 ?x4) })
:assumption (forall (?x6 T4) (?x7 T4) (?x8 T6) (implies (forall (?x9 T5) (implies (and (= (uf_15 ?x9 ?x8) uf_9) (not (= (uf_12 (uf_13 ?x9)) uf_14))) (or (= (uf_19 (uf_20 ?x6) ?x9) (uf_19 (uf_20 ?x7) ?x9)) (= (uf_8 ?x6 ?x7 ?x9 ?x8) uf_9))) :pat { (uf_18 ?x9) }) (= (uf_17 ?x6 ?x7 ?x8) uf_9)) :pat { (uf_17 ?x6 ?x7 ?x8) })
:assumption (forall (?x10 T4) (?x11 T4) (?x12 T6) (implies (forall (?x13 T5) (implies (or (= (uf_22 (uf_13 ?x13)) uf_9) (= (uf_23 (uf_13 ?x13)) uf_9)) (implies (and (= (uf_24 ?x10 ?x13) uf_9) (not (or (not (= (uf_25 ?x10 ?x13) uf_26)) (and (= (uf_12 (uf_13 ?x13)) uf_14) (= (uf_27 ?x10 ?x13) uf_9))))) (or (= (uf_19 (uf_20 ?x10) ?x13) (uf_19 (uf_20 ?x11) ?x13)) (= (uf_15 ?x13 ?x12) uf_9)))) :pat { (uf_18 ?x13) }) (= (uf_21 ?x10 ?x11 ?x12) uf_9)) :pat { (uf_21 ?x10 ?x11 ?x12) })
:assumption (forall (?x14 T5) (= (uf_28 (uf_29 ?x14)) ?x14))
:assumption (forall (?x15 T10) (= (uf_30 (uf_31 ?x15)) ?x15))
:assumption (forall (?x16 T7) (= (uf_32 (uf_33 ?x16)) ?x16))
:assumption (forall (?x17 T6) (= (uf_34 (uf_35 ?x17)) ?x17))
:assumption (up_36 uf_37)
:assumption (forall (?x18 T4) (?x19 T5) (= (uf_38 ?x18 ?x19) (uf_39 (uf_40 (uf_41 ?x18) ?x19))) :pat { (uf_38 ?x18 ?x19) })
:assumption (= uf_42 (uf_43 uf_37 0))
:assumption (forall (?x20 T4) (?x21 T5) (implies (and (= (uf_44 ?x20) uf_9) (= (uf_45 ?x20 ?x21) uf_9)) (= (uf_46 ?x20 ?x20 ?x21 (uf_13 ?x21)) uf_9)) :pat { (uf_44 ?x20) (uf_45 ?x20 ?x21) })
:assumption (forall (?x22 T4) (?x23 T5) (iff (= (uf_45 ?x22 ?x23) uf_9) (= (uf_27 ?x22 ?x23) uf_9)) :pat { (uf_45 ?x22 ?x23) })
:assumption (forall (?x24 T4) (?x25 T5) (iff (= (uf_47 ?x24 ?x25) uf_9) (and (= (uf_27 ?x24 ?x25) uf_9) (and (= (uf_25 ?x24 ?x25) uf_26) (and (= (uf_48 ?x25 (uf_13 ?x25)) uf_9) (and (= (uf_24 ?x24 ?x25) uf_9) (and (not (= (uf_12 (uf_13 ?x25)) uf_14)) (and (= (uf_23 (uf_13 ?x25)) uf_9) (or (not (up_36 (uf_13 ?x25))) (= (uf_38 ?x24 ?x25) 0))))))))) :pat { (uf_47 ?x24 ?x25) })
:assumption (forall (?x26 T4) (?x27 T5) (?x28 Int) (implies (and (= (uf_49 ?x26 ?x27) uf_9) (= (uf_50 ?x27 (uf_43 uf_37 ?x28)) uf_9)) (= (uf_49 ?x26 (uf_43 uf_37 ?x28)) uf_9)) :pat { (uf_49 ?x26 ?x27) (uf_50 ?x27 (uf_43 uf_37 ?x28)) })
:assumption (forall (?x29 T4) (?x30 T5) (?x31 T5) (implies (and (= (uf_49 ?x29 ?x30) uf_9) (= (uf_50 ?x30 ?x31) uf_9)) (= (uf_46 ?x29 ?x29 ?x31 (uf_13 ?x31)) uf_9)) :pat { (uf_49 ?x29 ?x30) (uf_50 ?x30 ?x31) })
:assumption (forall (?x32 T4) (?x33 T5) (?x34 T5) (implies (= (uf_51 ?x32) uf_9) (implies (and (= (uf_50 ?x33 ?x34) uf_9) (= (uf_27 ?x32 ?x33) uf_9)) (and (up_52 (uf_53 ?x32 ?x34)) (and (= (uf_27 ?x32 ?x34) uf_9) (< 0 (uf_38 ?x32 ?x34)))))) :pat { (uf_27 ?x32 ?x33) (uf_50 ?x33 ?x34) })
:assumption (forall (?x35 T4) (?x36 T5) (?x37 T5) (implies (and (= (uf_49 ?x35 ?x36) uf_9) (= (uf_54 ?x36 ?x37) uf_9)) (= (uf_49 ?x35 ?x37) uf_9)) :pat { (uf_49 ?x35 ?x36) (uf_54 ?x36 ?x37) })
:assumption (forall (?x38 T5) (?x39 T5) (implies (and (= (uf_48 ?x38 uf_37) uf_9) (and (= (uf_48 ?x39 uf_37) uf_9) (forall (?x40 T4) (implies (= (uf_49 ?x40 ?x38) uf_9) (= (uf_27 ?x40 ?x39) uf_9))))) (= (uf_54 ?x38 ?x39) uf_9)) :pat { (uf_54 ?x38 ?x39) })
:assumption (forall (?x41 T4) (?x42 T5) (implies (= (uf_49 ?x41 ?x42) uf_9) (and (= (uf_27 ?x41 ?x42) uf_9) (= (uf_44 ?x41) uf_9))) :pat { (uf_49 ?x41 ?x42) })
:assumption (forall (?x43 T4) (?x44 T5) (implies (and (= (uf_55 ?x43) uf_9) (= (uf_27 ?x43 ?x44) uf_9)) (= (uf_49 ?x43 ?x44) uf_9)) :pat { (uf_55 ?x43) (uf_49 ?x43 ?x44) })
:assumption (forall (?x45 T3) (implies (= (uf_56 ?x45) uf_9) (= (uf_22 ?x45) uf_9)) :pat { (uf_56 ?x45) })
:assumption (forall (?x46 T3) (implies (= (uf_57 ?x46) uf_9) (= (uf_22 ?x46) uf_9)) :pat { (uf_57 ?x46) })
:assumption (forall (?x47 T4) (?x48 Int) (?x49 T3) (implies (and (= (uf_56 ?x49) uf_9) (= (uf_51 ?x47) uf_9)) (= (uf_61 ?x47 (uf_60 ?x48 ?x49)) uf_9)) :pat { (uf_58 (uf_59 ?x47) (uf_60 ?x48 ?x49)) } :pat { (uf_40 (uf_41 ?x47) (uf_60 ?x48 ?x49)) })
:assumption (forall (?x50 Int) (= (uf_62 (uf_63 ?x50)) ?x50))
:assumption (forall (?x51 Int) (?x52 T3) (= (uf_60 ?x51 ?x52) (uf_43 ?x52 (uf_63 ?x51))) :pat { (uf_60 ?x51 ?x52) })
:assumption (forall (?x53 Int) (?x54 Int) (?x55 T4) (implies (= (uf_51 ?x55) uf_9) (and (= (uf_24 ?x55 (uf_64 ?x53 ?x54)) uf_9) (forall (?x56 Int) (implies (and (<= 0 ?x56) (< ?x56 ?x54)) (and (up_67 (uf_58 (uf_59 ?x55) (uf_66 (uf_64 ?x53 ?x54) ?x56 uf_7))) (and (= (uf_48 (uf_66 (uf_64 ?x53 ?x54) ?x56 uf_7) uf_7) uf_9) (= (uf_68 ?x55 (uf_66 (uf_64 ?x53 ?x54) ?x56 uf_7)) uf_9)))) :pat { (uf_40 (uf_41 ?x55) (uf_66 (uf_64 ?x53 ?x54) ?x56 uf_7)) } :pat { (uf_58 (uf_59 ?x55) (uf_66 (uf_64 ?x53 ?x54) ?x56 uf_7)) }))) :pat { (uf_24 ?x55 (uf_64 ?x53 ?x54)) } :pat { (uf_65 ?x55 (uf_64 ?x53 ?x54) uf_7 ?x54) })
:assumption (forall (?x57 Int) (?x58 Int) (= (uf_48 (uf_64 ?x57 ?x58) uf_7) uf_9) :pat { (uf_64 ?x57 ?x58) })
:assumption (forall (?x59 Int) (?x60 Int) (= (uf_69 ?x59 ?x60) (* ?x59 ?x60)) :pat { (uf_69 ?x59 ?x60) })
:assumption (forall (?x61 T3) (?x62 Int) (?x63 Int) (= (uf_70 ?x61 ?x62 ?x63) (uf_70 ?x61 ?x63 ?x62)) :pat { (uf_70 ?x61 ?x62 ?x63) })
:assumption (forall (?x64 T3) (?x65 Int) (?x66 Int) (= (uf_71 ?x64 ?x65 ?x66) (uf_71 ?x64 ?x66 ?x65)) :pat { (uf_71 ?x64 ?x65 ?x66) })
:assumption (forall (?x67 T3) (?x68 Int) (?x69 Int) (= (uf_72 ?x67 ?x68 ?x69) (uf_72 ?x67 ?x69 ?x68)) :pat { (uf_72 ?x67 ?x68 ?x69) })
:assumption (forall (?x70 T3) (?x71 Int) (implies (= (uf_74 ?x70 ?x71) uf_9) (= (uf_73 ?x70 (uf_73 ?x70 ?x71)) ?x71)) :pat { (uf_73 ?x70 (uf_73 ?x70 ?x71)) })
:assumption (forall (?x72 T3) (?x73 Int) (= (uf_71 ?x72 ?x73 (uf_73 ?x72 0)) (uf_73 ?x72 ?x73)) :pat { (uf_71 ?x72 ?x73 (uf_73 ?x72 0)) })
:assumption (forall (?x74 T3) (?x75 Int) (= (uf_71 ?x74 ?x75 ?x75) 0) :pat { (uf_71 ?x74 ?x75 ?x75) })
:assumption (forall (?x76 T3) (?x77 Int) (implies (= (uf_74 ?x76 ?x77) uf_9) (= (uf_71 ?x76 ?x77 0) ?x77)) :pat { (uf_71 ?x76 ?x77 0) })
:assumption (forall (?x78 T3) (?x79 Int) (?x80 Int) (= (uf_70 ?x78 (uf_72 ?x78 ?x79 ?x80) ?x79) ?x79) :pat { (uf_70 ?x78 (uf_72 ?x78 ?x79 ?x80) ?x79) })
:assumption (forall (?x81 T3) (?x82 Int) (?x83 Int) (= (uf_70 ?x81 (uf_72 ?x81 ?x82 ?x83) ?x83) ?x83) :pat { (uf_70 ?x81 (uf_72 ?x81 ?x82 ?x83) ?x83) })
:assumption (forall (?x84 T3) (?x85 Int) (implies (= (uf_74 ?x84 ?x85) uf_9) (= (uf_70 ?x84 ?x85 ?x85) ?x85)) :pat { (uf_70 ?x84 ?x85 ?x85) })
:assumption (forall (?x86 T3) (?x87 Int) (implies (= (uf_74 ?x86 ?x87) uf_9) (= (uf_70 ?x86 ?x87 (uf_73 ?x86 0)) ?x87)) :pat { (uf_70 ?x86 ?x87 (uf_73 ?x86 0)) })
:assumption (forall (?x88 T3) (?x89 Int) (= (uf_70 ?x88 ?x89 0) 0) :pat { (uf_70 ?x88 ?x89 0) })
:assumption (forall (?x90 T3) (?x91 Int) (implies (= (uf_74 ?x90 ?x91) uf_9) (= (uf_72 ?x90 ?x91 ?x91) ?x91)) :pat { (uf_72 ?x90 ?x91 ?x91) })
:assumption (forall (?x92 T3) (?x93 Int) (= (uf_72 ?x92 ?x93 (uf_73 ?x92 0)) (uf_73 ?x92 0)) :pat { (uf_72 ?x92 ?x93 (uf_73 ?x92 0)) })
:assumption (forall (?x94 T3) (?x95 Int) (implies (= (uf_74 ?x94 ?x95) uf_9) (= (uf_72 ?x94 ?x95 0) ?x95)) :pat { (uf_72 ?x94 ?x95 0) })
:assumption (forall (?x96 T3) (?x97 Int) (= (uf_70 ?x96 ?x97 (uf_73 ?x96 ?x97)) 0) :pat { (uf_70 ?x96 ?x97 (uf_73 ?x96 ?x97)) })
:assumption (forall (?x98 T3) (?x99 Int) (= (uf_72 ?x98 ?x99 (uf_73 ?x98 ?x99)) (uf_73 ?x98 0)) :pat { (uf_72 ?x98 ?x99 (uf_73 ?x98 ?x99)) })
:assumption (forall (?x100 T3) (?x101 Int) (= (uf_74 ?x100 (uf_73 ?x100 ?x101)) uf_9) :pat { (uf_73 ?x100 ?x101) })
:assumption (forall (?x102 T3) (?x103 Int) (?x104 Int) (implies (and (<= 0 ?x103) (and (<= ?x103 uf_75) (and (<= 0 ?x104) (<= ?x104 uf_75)))) (and (<= 0 (uf_71 ?x102 ?x103 ?x104)) (<= (uf_71 ?x102 ?x103 ?x104) uf_75))) :pat { (uf_71 ?x102 ?x103 ?x104) })
:assumption (forall (?x105 T3) (?x106 Int) (?x107 Int) (implies (and (<= 0 ?x106) (and (<= ?x106 uf_76) (and (<= 0 ?x107) (<= ?x107 uf_76)))) (and (<= 0 (uf_71 ?x105 ?x106 ?x107)) (<= (uf_71 ?x105 ?x106 ?x107) uf_76))) :pat { (uf_71 ?x105 ?x106 ?x107) })
:assumption (forall (?x108 T3) (?x109 Int) (?x110 Int) (implies (and (<= 0 ?x109) (and (<= ?x109 uf_77) (and (<= 0 ?x110) (<= ?x110 uf_77)))) (and (<= 0 (uf_71 ?x108 ?x109 ?x110)) (<= (uf_71 ?x108 ?x109 ?x110) uf_77))) :pat { (uf_71 ?x108 ?x109 ?x110) })
:assumption (forall (?x111 T3) (?x112 Int) (?x113 Int) (implies (and (<= 0 ?x112) (and (<= ?x112 uf_78) (and (<= 0 ?x113) (<= ?x113 uf_78)))) (and (<= 0 (uf_71 ?x111 ?x112 ?x113)) (<= (uf_71 ?x111 ?x112 ?x113) uf_78))) :pat { (uf_71 ?x111 ?x112 ?x113) })
:assumption (forall (?x114 T3) (?x115 Int) (?x116 Int) (implies (and (<= 0 ?x115) (and (<= ?x115 uf_75) (and (<= 0 ?x116) (<= ?x116 uf_75)))) (and (<= 0 (uf_70 ?x114 ?x115 ?x116)) (<= (uf_70 ?x114 ?x115 ?x116) uf_75))) :pat { (uf_70 ?x114 ?x115 ?x116) })
:assumption (forall (?x117 T3) (?x118 Int) (?x119 Int) (implies (and (<= 0 ?x118) (and (<= ?x118 uf_76) (and (<= 0 ?x119) (<= ?x119 uf_76)))) (and (<= 0 (uf_70 ?x117 ?x118 ?x119)) (<= (uf_70 ?x117 ?x118 ?x119) uf_76))) :pat { (uf_70 ?x117 ?x118 ?x119) })
:assumption (forall (?x120 T3) (?x121 Int) (?x122 Int) (implies (and (<= 0 ?x121) (and (<= ?x121 uf_77) (and (<= 0 ?x122) (<= ?x122 uf_77)))) (and (<= 0 (uf_70 ?x120 ?x121 ?x122)) (<= (uf_70 ?x120 ?x121 ?x122) uf_77))) :pat { (uf_70 ?x120 ?x121 ?x122) })
:assumption (forall (?x123 T3) (?x124 Int) (?x125 Int) (implies (and (<= 0 ?x124) (and (<= ?x124 uf_78) (and (<= 0 ?x125) (<= ?x125 uf_78)))) (and (<= 0 (uf_70 ?x123 ?x124 ?x125)) (<= (uf_70 ?x123 ?x124 ?x125) uf_78))) :pat { (uf_70 ?x123 ?x124 ?x125) })
:assumption (forall (?x126 T3) (?x127 Int) (?x128 Int) (implies (and (<= 0 ?x127) (and (<= ?x127 uf_75) (and (<= 0 ?x128) (<= ?x128 uf_75)))) (and (<= 0 (uf_72 ?x126 ?x127 ?x128)) (<= (uf_72 ?x126 ?x127 ?x128) uf_75))) :pat { (uf_72 ?x126 ?x127 ?x128) })
:assumption (forall (?x129 T3) (?x130 Int) (?x131 Int) (implies (and (<= 0 ?x130) (and (<= ?x130 uf_76) (and (<= 0 ?x131) (<= ?x131 uf_76)))) (and (<= 0 (uf_72 ?x129 ?x130 ?x131)) (<= (uf_72 ?x129 ?x130 ?x131) uf_76))) :pat { (uf_72 ?x129 ?x130 ?x131) })
:assumption (forall (?x132 T3) (?x133 Int) (?x134 Int) (implies (and (<= 0 ?x133) (and (<= ?x133 uf_77) (and (<= 0 ?x134) (<= ?x134 uf_77)))) (and (<= 0 (uf_72 ?x132 ?x133 ?x134)) (<= (uf_72 ?x132 ?x133 ?x134) uf_77))) :pat { (uf_72 ?x132 ?x133 ?x134) })
:assumption (forall (?x135 T3) (?x136 Int) (?x137 Int) (implies (and (<= 0 ?x136) (and (<= ?x136 uf_78) (and (<= 0 ?x137) (<= ?x137 uf_78)))) (and (<= 0 (uf_72 ?x135 ?x136 ?x137)) (<= (uf_72 ?x135 ?x136 ?x137) uf_78))) :pat { (uf_72 ?x135 ?x136 ?x137) })
:assumption (forall (?x138 T3) (?x139 Int) (?x140 Int) (?x141 Int) (implies (and (<= 0 ?x139) (and (<= 0 ?x140) (and (<= 0 ?x141) (and (< ?x141 64) (and (< ?x139 (uf_79 ?x141)) (and (< ?x140 (uf_79 ?x141)) (and (= (uf_74 ?x138 ?x139) uf_9) (= (uf_74 ?x138 ?x140) uf_9)))))))) (< (uf_72 ?x138 ?x139 ?x140) (uf_79 ?x141))) :pat { (uf_72 ?x138 ?x139 ?x140) (uf_79 ?x141) })
:assumption (forall (?x142 T3) (?x143 Int) (?x144 Int) (implies (and (<= 0 ?x143) (and (<= 0 ?x144) (and (= (uf_74 ?x142 ?x143) uf_9) (= (uf_74 ?x142 ?x144) uf_9)))) (and (<= ?x143 (uf_72 ?x142 ?x143 ?x144)) (<= ?x144 (uf_72 ?x142 ?x143 ?x144)))) :pat { (uf_72 ?x142 ?x143 ?x144) })
:assumption (forall (?x145 T3) (?x146 Int) (?x147 Int) (implies (and (<= 0 ?x146) (and (<= 0 ?x147) (and (= (uf_74 ?x145 ?x146) uf_9) (= (uf_74 ?x145 ?x147) uf_9)))) (and (<= 0 (uf_72 ?x145 ?x146 ?x147)) (<= (uf_72 ?x145 ?x146 ?x147) (+ ?x146 ?x147)))) :pat { (uf_72 ?x145 ?x146 ?x147) })
:assumption (forall (?x148 T3) (?x149 Int) (?x150 Int) (implies (and (<= 0 ?x149) (and (<= 0 ?x150) (and (= (uf_74 ?x148 ?x149) uf_9) (= (uf_74 ?x148 ?x150) uf_9)))) (and (<= (uf_70 ?x148 ?x149 ?x150) ?x149) (<= (uf_70 ?x148 ?x149 ?x150) ?x150))) :pat { (uf_70 ?x148 ?x149 ?x150) })
:assumption (forall (?x151 T3) (?x152 Int) (?x153 Int) (implies (and (<= 0 ?x152) (= (uf_74 ?x151 ?x152) uf_9)) (and (<= 0 (uf_70 ?x151 ?x152 ?x153)) (<= (uf_70 ?x151 ?x152 ?x153) ?x152))) :pat { (uf_70 ?x151 ?x152 ?x153) })
:assumption (forall (?x154 Int) (?x155 Int) (implies (and (<= ?x154 0) (< ?x155 0)) (and (< ?x155 (uf_80 ?x154 ?x155)) (<= (uf_80 ?x154 ?x155) 0))) :pat { (uf_80 ?x154 ?x155) })
:assumption (forall (?x156 Int) (?x157 Int) (implies (and (<= ?x156 0) (< 0 ?x157)) (and (< (- 0 ?x157) (uf_80 ?x156 ?x157)) (<= (uf_80 ?x156 ?x157) 0))) :pat { (uf_80 ?x156 ?x157) })
:assumption (forall (?x158 Int) (?x159 Int) (implies (and (<= 0 ?x158) (< ?x159 0)) (and (<= 0 (uf_80 ?x158 ?x159)) (< (uf_80 ?x158 ?x159) (- 0 ?x159)))) :pat { (uf_80 ?x158 ?x159) })
:assumption (forall (?x160 Int) (?x161 Int) (implies (and (<= 0 ?x160) (< 0 ?x161)) (and (<= 0 (uf_80 ?x160 ?x161)) (< (uf_80 ?x160 ?x161) ?x161))) :pat { (uf_80 ?x160 ?x161) })
:assumption (forall (?x162 Int) (?x163 Int) (= (uf_80 ?x162 ?x163) (- ?x162 (* (uf_81 ?x162 ?x163) ?x163))) :pat { (uf_80 ?x162 ?x163) } :pat { (uf_81 ?x162 ?x163) })
:assumption (forall (?x164 Int) (implies (not (= ?x164 0)) (= (uf_81 ?x164 ?x164) 1)) :pat { (uf_81 ?x164 ?x164) })
:assumption (forall (?x165 Int) (?x166 Int) (implies (and (< 0 ?x165) (< 0 ?x166)) (and (< (- ?x165 ?x166) (* (uf_81 ?x165 ?x166) ?x166)) (<= (* (uf_81 ?x165 ?x166) ?x166) ?x165))) :pat { (uf_81 ?x165 ?x166) })
:assumption (forall (?x167 Int) (?x168 Int) (implies (and (<= 0 ?x167) (< 0 ?x168)) (<= (uf_81 ?x167 ?x168) ?x167)) :pat { (uf_81 ?x167 ?x168) })
:assumption (forall (?x169 T3) (?x170 Int) (?x171 Int) (?x172 Int) (implies (and (= (uf_74 ?x169 ?x170) uf_9) (and (= (uf_74 ?x169 (- (uf_79 ?x171) 1)) uf_9) (<= 0 ?x170))) (= (uf_80 ?x170 (uf_79 ?x171)) (uf_70 ?x169 ?x170 (- (uf_79 ?x171) 1)))) :pat { (uf_80 ?x170 (uf_79 ?x171)) (uf_70 ?x169 ?x170 ?x172) })
:assumption (forall (?x173 Int) (implies (and (<= uf_85 ?x173) (<= ?x173 uf_86)) (= (uf_82 uf_83 (uf_82 uf_84 ?x173)) ?x173)) :pat { (uf_82 uf_83 (uf_82 uf_84 ?x173)) })
:assumption (forall (?x174 Int) (implies (and (<= uf_88 ?x174) (<= ?x174 uf_89)) (= (uf_82 uf_87 (uf_82 uf_4 ?x174)) ?x174)) :pat { (uf_82 uf_87 (uf_82 uf_4 ?x174)) })
:assumption (forall (?x175 Int) (implies (and (<= uf_92 ?x175) (<= ?x175 uf_93)) (= (uf_82 uf_90 (uf_82 uf_91 ?x175)) ?x175)) :pat { (uf_82 uf_90 (uf_82 uf_91 ?x175)) })
:assumption (forall (?x176 Int) (implies (and (<= uf_95 ?x176) (<= ?x176 uf_96)) (= (uf_82 uf_94 (uf_82 uf_7 ?x176)) ?x176)) :pat { (uf_82 uf_94 (uf_82 uf_7 ?x176)) })
:assumption (forall (?x177 Int) (implies (and (<= 0 ?x177) (<= ?x177 uf_75)) (= (uf_82 uf_84 (uf_82 uf_83 ?x177)) ?x177)) :pat { (uf_82 uf_84 (uf_82 uf_83 ?x177)) })
:assumption (forall (?x178 Int) (implies (and (<= 0 ?x178) (<= ?x178 uf_76)) (= (uf_82 uf_4 (uf_82 uf_87 ?x178)) ?x178)) :pat { (uf_82 uf_4 (uf_82 uf_87 ?x178)) })
:assumption (forall (?x179 Int) (implies (and (<= 0 ?x179) (<= ?x179 uf_77)) (= (uf_82 uf_91 (uf_82 uf_90 ?x179)) ?x179)) :pat { (uf_82 uf_91 (uf_82 uf_90 ?x179)) })
:assumption (forall (?x180 Int) (implies (and (<= 0 ?x180) (<= ?x180 uf_78)) (= (uf_82 uf_7 (uf_82 uf_94 ?x180)) ?x180)) :pat { (uf_82 uf_7 (uf_82 uf_94 ?x180)) })
:assumption (forall (?x181 T3) (?x182 Int) (= (uf_74 ?x181 (uf_82 ?x181 ?x182)) uf_9) :pat { (uf_82 ?x181 ?x182) })
:assumption (forall (?x183 T3) (?x184 Int) (implies (= (uf_74 ?x183 ?x184) uf_9) (= (uf_82 ?x183 ?x184) ?x184)) :pat { (uf_82 ?x183 ?x184) })
:assumption (forall (?x185 Int) (iff (= (uf_74 uf_84 ?x185) uf_9) (and (<= 0 ?x185) (<= ?x185 uf_75))) :pat { (uf_74 uf_84 ?x185) })
:assumption (forall (?x186 Int) (iff (= (uf_74 uf_4 ?x186) uf_9) (and (<= 0 ?x186) (<= ?x186 uf_76))) :pat { (uf_74 uf_4 ?x186) })
:assumption (forall (?x187 Int) (iff (= (uf_74 uf_91 ?x187) uf_9) (and (<= 0 ?x187) (<= ?x187 uf_77))) :pat { (uf_74 uf_91 ?x187) })
:assumption (forall (?x188 Int) (iff (= (uf_74 uf_7 ?x188) uf_9) (and (<= 0 ?x188) (<= ?x188 uf_78))) :pat { (uf_74 uf_7 ?x188) })
:assumption (forall (?x189 Int) (iff (= (uf_74 uf_83 ?x189) uf_9) (and (<= uf_85 ?x189) (<= ?x189 uf_86))) :pat { (uf_74 uf_83 ?x189) })
:assumption (forall (?x190 Int) (iff (= (uf_74 uf_87 ?x190) uf_9) (and (<= uf_88 ?x190) (<= ?x190 uf_89))) :pat { (uf_74 uf_87 ?x190) })
:assumption (forall (?x191 Int) (iff (= (uf_74 uf_90 ?x191) uf_9) (and (<= uf_92 ?x191) (<= ?x191 uf_93))) :pat { (uf_74 uf_90 ?x191) })
:assumption (forall (?x192 Int) (iff (= (uf_74 uf_94 ?x192) uf_9) (and (<= uf_95 ?x192) (<= ?x192 uf_96))) :pat { (uf_74 uf_94 ?x192) })
:assumption (forall (?x193 Int) (?x194 Int) (?x195 Int) (?x196 Int) (implies (and (<= 0 ?x193) (and (< ?x193 ?x194) (and (<= ?x194 ?x196) (and (<= 0 ?x195) (<= (uf_79 (- (- ?x194 ?x193) 1)) (uf_80 (uf_81 ?x195 (uf_79 ?x193)) (uf_79 (- ?x194 ?x193)))))))) (= (uf_97 ?x195 ?x196 ?x193 ?x194) (- (uf_79 (- (- ?x194 ?x193) 1)) (uf_80 (uf_81 ?x195 (uf_79 ?x193)) (uf_79 (- ?x194 ?x193)))))) :pat { (uf_97 ?x195 ?x196 ?x193 ?x194) })
:assumption (forall (?x197 Int) (?x198 Int) (?x199 Int) (?x200 Int) (implies (and (<= 0 ?x197) (and (< ?x197 ?x198) (and (<= ?x198 ?x200) (and (<= 0 ?x199) (< (uf_80 (uf_81 ?x199 (uf_79 ?x197)) (uf_79 (- ?x198 ?x197))) (uf_79 (- (- ?x198 ?x197) 1))))))) (= (uf_97 ?x199 ?x200 ?x197 ?x198) (uf_80 (uf_81 ?x199 (uf_79 ?x197)) (uf_79 (- ?x198 ?x197))))) :pat { (uf_97 ?x199 ?x200 ?x197 ?x198) })
:assumption (forall (?x201 Int) (?x202 Int) (?x203 Int) (?x204 Int) (implies (and (<= 0 ?x201) (and (< ?x201 ?x202) (and (<= ?x202 ?x204) (<= 0 ?x203)))) (= (uf_98 ?x203 ?x204 ?x201 ?x202) (uf_80 (uf_81 ?x203 (uf_79 ?x201)) (uf_79 (- ?x202 ?x201))))) :pat { (uf_98 ?x203 ?x204 ?x201 ?x202) })
:assumption (forall (?x205 Int) (?x206 Int) (?x207 Int) (implies (and (<= 0 ?x205) (and (< ?x205 ?x206) (<= ?x206 ?x207))) (= (uf_98 0 ?x207 ?x205 ?x206) 0)) :pat { (uf_98 0 ?x207 ?x205 ?x206) })
:assumption (forall (?x208 Int) (?x209 Int) (?x210 Int) (implies (and (<= 0 ?x208) (and (< ?x208 ?x209) (<= ?x209 ?x210))) (= (uf_97 0 ?x210 ?x208 ?x209) 0)) :pat { (uf_97 0 ?x210 ?x208 ?x209) })
:assumption (forall (?x211 Int) (?x212 Int) (?x213 Int) (?x214 Int) (?x215 Int) (?x216 Int) (?x217 Int) (implies (and (<= 0 ?x211) (and (< ?x211 ?x212) (<= ?x212 ?x215))) (implies (and (<= 0 ?x216) (and (< ?x216 ?x217) (<= ?x217 ?x215))) (implies (or (<= ?x217 ?x211) (<= ?x212 ?x216)) (= (uf_98 (uf_99 ?x214 ?x215 ?x211 ?x212 ?x213) ?x215 ?x216 ?x217) (uf_98 ?x214 ?x215 ?x216 ?x217))))) :pat { (uf_98 (uf_99 ?x214 ?x215 ?x211 ?x212 ?x213) ?x215 ?x216 ?x217) })
:assumption (forall (?x218 Int) (?x219 Int) (?x220 Int) (?x221 Int) (?x222 Int) (?x223 Int) (?x224 Int) (implies (and (<= 0 ?x218) (and (< ?x218 ?x219) (<= ?x219 ?x222))) (implies (and (<= 0 ?x223) (and (< ?x223 ?x224) (<= ?x224 ?x222))) (implies (or (<= ?x224 ?x218) (<= ?x219 ?x223)) (= (uf_97 (uf_99 ?x221 ?x222 ?x218 ?x219 ?x220) ?x222 ?x223 ?x224) (uf_97 ?x221 ?x222 ?x223 ?x224))))) :pat { (uf_97 (uf_99 ?x221 ?x222 ?x218 ?x219 ?x220) ?x222 ?x223 ?x224) })
:assumption (forall (?x225 Int) (?x226 Int) (?x227 Int) (?x228 Int) (implies (and (<= 0 ?x225) (and (< ?x225 ?x226) (<= ?x226 ?x228))) (and (<= 0 (uf_98 ?x227 ?x228 ?x225 ?x226)) (<= (uf_98 ?x227 ?x228 ?x225 ?x226) (- (uf_79 (- ?x226 ?x225)) 1)))) :pat { (uf_98 ?x227 ?x228 ?x225 ?x226) })
:assumption (forall (?x229 Int) (?x230 Int) (?x231 Int) (?x232 Int) (implies (and (<= 0 ?x229) (and (< ?x229 ?x230) (<= ?x230 ?x232))) (and (<= (- 0 (uf_79 (- (- ?x230 ?x229) 1))) (uf_97 ?x231 ?x232 ?x229 ?x230)) (<= (uf_97 ?x231 ?x232 ?x229 ?x230) (- (uf_79 (- (- ?x230 ?x229) 1)) 1)))) :pat { (uf_97 ?x231 ?x232 ?x229 ?x230) })
:assumption (forall (?x233 Int) (?x234 Int) (?x235 Int) (?x236 Int) (?x237 Int) (implies (and (<= 0 ?x233) (and (< ?x233 ?x234) (<= ?x234 ?x237))) (implies (and (<= 0 ?x235) (< ?x235 (uf_79 (- ?x234 ?x233)))) (= (uf_98 (uf_99 ?x236 ?x237 ?x233 ?x234 ?x235) ?x237 ?x233 ?x234) ?x235))) :pat { (uf_98 (uf_99 ?x236 ?x237 ?x233 ?x234 ?x235) ?x237 ?x233 ?x234) })
:assumption (forall (?x238 Int) (?x239 Int) (?x240 Int) (?x241 Int) (?x242 Int) (implies (and (<= 0 ?x238) (and (< ?x238 ?x239) (<= ?x239 ?x242))) (implies (and (<= (- 0 (uf_79 (- (- ?x239 ?x238) 1))) ?x240) (< ?x240 (uf_79 (- (- ?x239 ?x238) 1)))) (= (uf_97 (uf_99 ?x241 ?x242 ?x238 ?x239 ?x240) ?x242 ?x238 ?x239) ?x240))) :pat { (uf_97 (uf_99 ?x241 ?x242 ?x238 ?x239 ?x240) ?x242 ?x238 ?x239) })
:assumption (forall (?x243 Int) (?x244 Int) (?x245 Int) (implies (and (<= 0 ?x243) (and (< ?x243 ?x244) (<= ?x244 ?x245))) (= (uf_99 0 ?x245 ?x243 ?x244 0) 0)) :pat { (uf_99 0 ?x245 ?x243 ?x244 0) })
:assumption (forall (?x246 Int) (?x247 Int) (?x248 Int) (?x249 Int) (?x250 Int) (implies (and (<= 0 ?x247) (and (< ?x247 ?x248) (<= ?x248 ?x249))) (implies (and (<= 0 ?x250) (< ?x250 (uf_79 (- ?x248 ?x247)))) (and (<= 0 (uf_99 ?x246 ?x249 ?x247 ?x248 ?x250)) (< (uf_99 ?x246 ?x249 ?x247 ?x248 ?x250) (uf_79 ?x249))))) :pat { (uf_99 ?x246 ?x249 ?x247 ?x248 ?x250) })
:assumption (forall (?x251 Int) (?x252 Int) (= (uf_100 ?x251 ?x252) (uf_81 ?x251 (uf_79 ?x252))) :pat { (uf_100 ?x251 ?x252) })
:assumption (forall (?x253 T3) (?x254 Int) (?x255 Int) (= (uf_101 ?x253 ?x254 ?x255) (uf_82 ?x253 (* ?x254 (uf_79 ?x255)))) :pat { (uf_101 ?x253 ?x254 ?x255) })
:assumption (forall (?x256 T3) (?x257 Int) (?x258 Int) (= (uf_102 ?x256 ?x257 ?x258) (uf_82 ?x256 (uf_80 ?x257 ?x258))) :pat { (uf_102 ?x256 ?x257 ?x258) })
:assumption (forall (?x259 T3) (?x260 Int) (?x261 Int) (= (uf_103 ?x259 ?x260 ?x261) (uf_82 ?x259 (uf_81 ?x260 ?x261))) :pat { (uf_103 ?x259 ?x260 ?x261) })
:assumption (forall (?x262 T3) (?x263 Int) (?x264 Int) (= (uf_104 ?x262 ?x263 ?x264) (uf_82 ?x262 (* ?x263 ?x264))) :pat { (uf_104 ?x262 ?x263 ?x264) })
:assumption (forall (?x265 T3) (?x266 Int) (?x267 Int) (= (uf_105 ?x265 ?x266 ?x267) (uf_82 ?x265 (- ?x266 ?x267))) :pat { (uf_105 ?x265 ?x266 ?x267) })
:assumption (forall (?x268 T3) (?x269 Int) (?x270 Int) (= (uf_106 ?x268 ?x269 ?x270) (uf_82 ?x268 (+ ?x269 ?x270))) :pat { (uf_106 ?x268 ?x269 ?x270) })
:assumption (and (= (uf_79 0) 1) (and (= (uf_79 1) 2) (and (= (uf_79 2) 4) (and (= (uf_79 3) 8) (and (= (uf_79 4) 16) (and (= (uf_79 5) 32) (and (= (uf_79 6) 64) (and (= (uf_79 7) 128) (and (= (uf_79 8) 256) (and (= (uf_79 9) 512) (and (= (uf_79 10) 1024) (and (= (uf_79 11) 2048) (and (= (uf_79 12) 4096) (and (= (uf_79 13) 8192) (and (= (uf_79 14) 16384) (and (= (uf_79 15) 32768) (and (= (uf_79 16) 65536) (and (= (uf_79 17) 131072) (and (= (uf_79 18) 262144) (and (= (uf_79 19) 524288) (and (= (uf_79 20) 1048576) (and (= (uf_79 21) 2097152) (and (= (uf_79 22) 4194304) (and (= (uf_79 23) 8388608) (and (= (uf_79 24) 16777216) (and (= (uf_79 25) 33554432) (and (= (uf_79 26) 67108864) (and (= (uf_79 27) 134217728) (and (= (uf_79 28) 268435456) (and (= (uf_79 29) 536870912) (and (= (uf_79 30) 1073741824) (and (= (uf_79 31) 2147483648) (and (= (uf_79 32) 4294967296) (and (= (uf_79 33) 8589934592) (and (= (uf_79 34) 17179869184) (and (= (uf_79 35) 34359738368) (and (= (uf_79 36) 68719476736) (and (= (uf_79 37) 137438953472) (and (= (uf_79 38) 274877906944) (and (= (uf_79 39) 549755813888) (and (= (uf_79 40) 1099511627776) (and (= (uf_79 41) 2199023255552) (and (= (uf_79 42) 4398046511104) (and (= (uf_79 43) 8796093022208) (and (= (uf_79 44) 17592186044416) (and (= (uf_79 45) 35184372088832) (and (= (uf_79 46) 70368744177664) (and (= (uf_79 47) 140737488355328) (and (= (uf_79 48) 281474976710656) (and (= (uf_79 49) 562949953421312) (and (= (uf_79 50) 1125899906842624) (and (= (uf_79 51) 2251799813685248) (and (= (uf_79 52) 4503599627370496) (and (= (uf_79 53) 9007199254740992) (and (= (uf_79 54) 18014398509481984) (and (= (uf_79 55) 36028797018963968) (and (= (uf_79 56) 72057594037927936) (and (= (uf_79 57) 144115188075855872) (and (= (uf_79 58) 288230376151711744) (and (= (uf_79 59) 576460752303423488) (and (= (uf_79 60) 1152921504606846976) (and (= (uf_79 61) 2305843009213693952) (and (= (uf_79 62) 4611686018427387904) (= (uf_79 63) 9223372036854775808))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
:assumption (forall (?x271 T4) (?x272 T5) (implies (= (uf_51 ?x271) uf_9) (and (<= 0 (uf_107 ?x271 ?x272)) (<= (uf_107 ?x271 ?x272) uf_75))) :pat { (uf_107 ?x271 ?x272) })
:assumption (forall (?x273 T4) (?x274 T5) (implies (= (uf_51 ?x273) uf_9) (and (<= 0 (uf_108 ?x273 ?x274)) (<= (uf_108 ?x273 ?x274) uf_76))) :pat { (uf_108 ?x273 ?x274) })
:assumption (forall (?x275 T4) (?x276 T5) (implies (= (uf_51 ?x275) uf_9) (and (<= 0 (uf_109 ?x275 ?x276)) (<= (uf_109 ?x275 ?x276) uf_77))) :pat { (uf_109 ?x275 ?x276) })
:assumption (forall (?x277 T4) (?x278 T5) (implies (= (uf_51 ?x277) uf_9) (and (<= 0 (uf_110 ?x277 ?x278)) (<= (uf_110 ?x277 ?x278) uf_78))) :pat { (uf_110 ?x277 ?x278) })
:assumption (forall (?x279 T4) (?x280 T5) (implies (= (uf_51 ?x279) uf_9) (and (<= uf_85 (uf_111 ?x279 ?x280)) (<= (uf_111 ?x279 ?x280) uf_86))) :pat { (uf_111 ?x279 ?x280) })
:assumption (forall (?x281 T4) (?x282 T5) (implies (= (uf_51 ?x281) uf_9) (and (<= uf_88 (uf_112 ?x281 ?x282)) (<= (uf_112 ?x281 ?x282) uf_89))) :pat { (uf_112 ?x281 ?x282) })
:assumption (forall (?x283 T4) (?x284 T5) (implies (= (uf_51 ?x283) uf_9) (and (<= uf_92 (uf_113 ?x283 ?x284)) (<= (uf_113 ?x283 ?x284) uf_93))) :pat { (uf_113 ?x283 ?x284) })
:assumption (forall (?x285 T4) (?x286 T5) (implies (= (uf_51 ?x285) uf_9) (and (<= uf_95 (uf_114 ?x285 ?x286)) (<= (uf_114 ?x285 ?x286) uf_96))) :pat { (uf_114 ?x285 ?x286) })
:assumption (forall (?x287 T5) (?x288 T5) (= (uf_115 ?x287 ?x288) (- (uf_116 ?x287) (uf_116 ?x288))) :pat { (uf_115 ?x287 ?x288) })
:assumption (forall (?x289 T5) (implies (and (<= uf_88 (uf_116 ?x289)) (<= (uf_116 ?x289) uf_89)) (= (uf_117 ?x289) (uf_116 ?x289))) :pat { (uf_117 ?x289) })
:assumption (forall (?x290 T5) (implies (and (<= 0 (uf_116 ?x290)) (<= (uf_116 ?x290) uf_76)) (= (uf_118 ?x290) (uf_116 ?x290))) :pat { (uf_118 ?x290) })
:assumption (forall (?x291 T5) (implies (and (<= uf_85 (uf_116 ?x291)) (<= (uf_116 ?x291) uf_86)) (= (uf_119 ?x291) (uf_116 ?x291))) :pat { (uf_119 ?x291) })
:assumption (forall (?x292 T5) (implies (and (<= 0 (uf_116 ?x292)) (<= (uf_116 ?x292) uf_75)) (= (uf_120 ?x292) (uf_116 ?x292))) :pat { (uf_120 ?x292) })
:assumption (= (uf_117 uf_121) 0)
:assumption (= (uf_118 uf_121) 0)
:assumption (= (uf_119 uf_121) 0)
:assumption (= (uf_120 uf_121) 0)
:assumption (forall (?x293 T4) (?x294 T5) (= (uf_107 ?x293 ?x294) (uf_19 (uf_20 ?x293) ?x294)) :pat { (uf_107 ?x293 ?x294) })
:assumption (forall (?x295 T4) (?x296 T5) (= (uf_108 ?x295 ?x296) (uf_19 (uf_20 ?x295) ?x296)) :pat { (uf_108 ?x295 ?x296) })
:assumption (forall (?x297 T4) (?x298 T5) (= (uf_109 ?x297 ?x298) (uf_19 (uf_20 ?x297) ?x298)) :pat { (uf_109 ?x297 ?x298) })
:assumption (forall (?x299 T4) (?x300 T5) (= (uf_110 ?x299 ?x300) (uf_19 (uf_20 ?x299) ?x300)) :pat { (uf_110 ?x299 ?x300) })
:assumption (forall (?x301 T4) (?x302 T5) (= (uf_111 ?x301 ?x302) (uf_19 (uf_20 ?x301) ?x302)) :pat { (uf_111 ?x301 ?x302) })
:assumption (forall (?x303 T4) (?x304 T5) (= (uf_112 ?x303 ?x304) (uf_19 (uf_20 ?x303) ?x304)) :pat { (uf_112 ?x303 ?x304) })
:assumption (forall (?x305 T4) (?x306 T5) (= (uf_113 ?x305 ?x306) (uf_19 (uf_20 ?x305) ?x306)) :pat { (uf_113 ?x305 ?x306) })
:assumption (forall (?x307 T4) (?x308 T5) (= (uf_114 ?x307 ?x308) (uf_19 (uf_20 ?x307) ?x308)) :pat { (uf_114 ?x307 ?x308) })
:assumption (= uf_75 (- (* (* (* 65536 65536) 65536) 65536) 1))
:assumption (= uf_76 (- (* 65536 65536) 1))
:assumption (= uf_77 65535)
:assumption (= uf_78 255)
:assumption (= uf_86 (- (* (* (* 65536 65536) 65536) 32768) 1))
:assumption (= uf_85 (- 0 (* (* (* 65536 65536) 65536) 32768)))
:assumption (= uf_89 (- (* 65536 32768) 1))
:assumption (= uf_88 (- 0 (* 65536 32768)))
:assumption (= uf_93 32767)
:assumption (= uf_92 (- 0 32768))
:assumption (= uf_96 127)
:assumption (= uf_95 (- 0 128))
:assumption (forall (?x309 T2) (iff (= (uf_122 ?x309) uf_9) (= ?x309 uf_9)) :pat { (uf_122 ?x309) })
:assumption (forall (?x310 T4) (?x311 T4) (?x312 T5) (?x313 T3) (?x314 Int) (implies (= (uf_22 ?x313) uf_9) (implies (= (uf_123 ?x310 ?x311 ?x312 (uf_124 ?x313 ?x314)) uf_9) (forall (?x315 Int) (implies (and (<= 0 ?x315) (< ?x315 ?x314)) (= (uf_19 (uf_20 ?x310) (uf_66 (uf_43 ?x313 (uf_116 ?x312)) ?x315 ?x313)) (uf_19 (uf_20 ?x311) (uf_66 (uf_43 ?x313 (uf_116 ?x312)) ?x315 ?x313)))) :pat { (uf_19 (uf_20 ?x311) (uf_66 (uf_43 ?x313 (uf_116 ?x312)) ?x315 ?x313)) }))) :pat { (uf_123 ?x310 ?x311 ?x312 (uf_124 ?x313 ?x314)) (uf_22 ?x313) })
:assumption (forall (?x316 T5) (?x317 Int) (?x318 T15) (= (uf_125 (uf_126 (uf_66 ?x316 ?x317 (uf_13 ?x316)) ?x318) ?x316) ?x317) :pat { (uf_125 (uf_126 (uf_66 ?x316 ?x317 (uf_13 ?x316)) ?x318) ?x316) })
:assumption (forall (?x319 T5) (?x320 Int) (= (uf_125 (uf_66 ?x319 ?x320 (uf_13 ?x319)) ?x319) ?x320) :pat { (uf_66 ?x319 ?x320 (uf_13 ?x319)) })
:assumption (forall (?x321 T5) (?x322 T4) (?x323 T5) (iff (= (uf_15 ?x321 (uf_127 ?x322 ?x323)) uf_9) (and (not (= (uf_116 ?x323) (uf_116 uf_121))) (= (uf_15 ?x321 (uf_128 ?x322 ?x323)) uf_9))) :pat { (uf_15 ?x321 (uf_127 ?x322 ?x323)) })
:assumption (forall (?x324 T5) (?x325 Int) (?x326 T3) (?x327 Int) (iff (= (uf_15 ?x324 (uf_129 (uf_43 ?x326 ?x325) ?x326 ?x327)) uf_9) (and (not (= ?x325 0)) (and (<= 0 (uf_125 ?x324 (uf_43 ?x326 ?x325))) (and (<= (uf_125 ?x324 (uf_43 ?x326 ?x325)) (- ?x327 1)) (= (uf_15 ?x324 (uf_130 (uf_66 (uf_43 ?x326 ?x325) (uf_125 ?x324 (uf_43 ?x326 ?x325)) ?x326))) uf_9))))) :pat { (uf_15 ?x324 (uf_129 (uf_43 ?x326 ?x325) ?x326 ?x327)) })
:assumption (forall (?x328 T5) (?x329 T3) (?x330 Int) (?x331 Int) (?x332 T6) (implies (and (<= 0 ?x331) (< ?x331 ?x330)) (= (uf_133 (uf_66 ?x328 ?x331 ?x329) ?x332 (uf_132 ?x328 ?x329 ?x330)) 2)) :pat { (uf_66 ?x328 ?x331 ?x329) (uf_131 ?x332 (uf_132 ?x328 ?x329 ?x330)) })
:assumption (forall (?x333 T5) (?x334 T3) (?x335 Int) (?x336 Int) (?x337 T6) (implies (and (<= 0 ?x336) (< ?x336 ?x335)) (= (uf_133 (uf_66 ?x333 ?x336 ?x334) (uf_132 ?x333 ?x334 ?x335) ?x337) 1)) :pat { (uf_66 ?x333 ?x336 ?x334) (uf_131 (uf_132 ?x333 ?x334 ?x335) ?x337) })
:assumption (forall (?x338 T5) (?x339 Int) (?x340 T3) (?x341 Int) (iff (= (uf_15 ?x338 (uf_132 (uf_43 ?x340 ?x339) ?x340 ?x341)) uf_9) (and (<= 0 (uf_125 ?x338 (uf_43 ?x340 ?x339))) (and (<= (uf_125 ?x338 (uf_43 ?x340 ?x339)) (- ?x341 1)) (= (uf_15 ?x338 (uf_130 (uf_66 (uf_43 ?x340 ?x339) (uf_125 ?x338 (uf_43 ?x340 ?x339)) ?x340))) uf_9)))) :pat { (uf_15 ?x338 (uf_132 (uf_43 ?x340 ?x339) ?x340 ?x341)) })
:assumption (forall (?x342 T5) (?x343 T3) (?x344 Int) (?x345 T5) (iff (= (uf_15 ?x345 (uf_134 ?x342 ?x343 ?x344)) uf_9) (and (<= 0 (uf_125 ?x345 ?x342)) (and (<= (uf_125 ?x345 ?x342) (- ?x344 1)) (= ?x345 (uf_66 ?x342 (uf_125 ?x345 ?x342) ?x343))))) :pat { (uf_15 ?x345 (uf_134 ?x342 ?x343 ?x344)) })
:assumption (forall (?x346 T4) (?x347 Int) (?x348 T3) (?x349 Int) (?x350 Int) (implies (= (uf_24 ?x346 (uf_43 (uf_124 ?x348 ?x349) ?x347)) uf_9) (implies (and (<= 0 ?x350) (< ?x350 ?x349)) (and (= (uf_135 (uf_58 (uf_59 ?x346) (uf_66 (uf_43 (uf_124 ?x348 ?x349) ?x347) ?x350 ?x348))) (uf_43 (uf_124 ?x348 ?x349) ?x347)) (and (not (= (uf_136 (uf_58 (uf_59 ?x346) (uf_66 (uf_43 (uf_124 ?x348 ?x349) ?x347) ?x350 ?x348))) uf_9)) (and (up_67 (uf_58 (uf_59 ?x346) (uf_66 (uf_43 (uf_124 ?x348 ?x349) ?x347) ?x350 ?x348))) (= (uf_24 ?x346 (uf_66 (uf_43 (uf_124 ?x348 ?x349) ?x347) ?x350 ?x348)) uf_9)))))) :pat { (uf_40 (uf_41 ?x346) (uf_66 (uf_43 ?x348 ?x347) ?x350 ?x348)) (uf_43 (uf_124 ?x348 ?x349) ?x347) } :pat { (uf_58 (uf_59 ?x346) (uf_66 (uf_43 ?x348 ?x347) ?x350 ?x348)) (uf_43 (uf_124 ?x348 ?x349) ?x347) })
:assumption (forall (?x351 T4) (?x352 T5) (?x353 Int) (?x354 T3) (?x355 Int) (iff (= (uf_15 ?x352 (uf_128 ?x351 (uf_43 (uf_124 ?x354 ?x355) ?x353))) uf_9) (or (= ?x352 (uf_43 (uf_124 ?x354 ?x355) ?x353)) (and (<= 0 (uf_125 ?x352 (uf_43 ?x354 ?x353))) (and (<= (uf_125 ?x352 (uf_43 ?x354 ?x353)) (- ?x355 1)) (= (uf_15 ?x352 (uf_128 ?x351 (uf_66 (uf_43 ?x354 ?x353) (uf_125 ?x352 (uf_43 ?x354 ?x353)) ?x354))) uf_9))))) :pat { (uf_15 ?x352 (uf_128 ?x351 (uf_43 (uf_124 ?x354 ?x355) ?x353))) })
:assumption (forall (?x356 T5) (?x357 Int) (?x358 T3) (?x359 Int) (iff (= (uf_15 ?x356 (uf_130 (uf_43 (uf_124 ?x358 ?x359) ?x357))) uf_9) (or (= ?x356 (uf_43 (uf_124 ?x358 ?x359) ?x357)) (and (<= 0 (uf_125 ?x356 (uf_43 ?x358 ?x357))) (and (<= (uf_125 ?x356 (uf_43 ?x358 ?x357)) (- ?x359 1)) (= (uf_15 ?x356 (uf_130 (uf_66 (uf_43 ?x358 ?x357) (uf_125 ?x356 (uf_43 ?x358 ?x357)) ?x358))) uf_9))))) :pat { (uf_15 ?x356 (uf_130 (uf_43 (uf_124 ?x358 ?x359) ?x357))) })
:assumption (forall (?x360 T4) (?x361 T5) (?x362 T3) (?x363 Int) (iff (= (uf_65 ?x360 ?x361 ?x362 ?x363) uf_9) (and (= (uf_48 ?x361 ?x362) uf_9) (forall (?x364 Int) (implies (and (<= 0 ?x364) (< ?x364 ?x363)) (and (up_67 (uf_58 (uf_59 ?x360) (uf_66 ?x361 ?x364 ?x362))) (= (uf_24 ?x360 (uf_66 ?x361 ?x364 ?x362)) uf_9))) :pat { (uf_40 (uf_41 ?x360) (uf_66 ?x361 ?x364 ?x362)) } :pat { (uf_58 (uf_59 ?x360) (uf_66 ?x361 ?x364 ?x362)) } :pat { (uf_19 (uf_20 ?x360) (uf_66 ?x361 ?x364 ?x362)) }))) :pat { (uf_65 ?x360 ?x361 ?x362 ?x363) })
:assumption (forall (?x365 T4) (?x366 T5) (?x367 T3) (?x368 Int) (?x369 T2) (iff (= (uf_137 ?x365 ?x366 ?x367 ?x368 ?x369) uf_9) (and (= (uf_48 ?x366 ?x367) uf_9) (forall (?x370 Int) (implies (and (<= 0 ?x370) (< ?x370 ?x368)) (and (iff (= (uf_136 (uf_58 (uf_59 ?x365) (uf_66 ?x366 ?x370 ?x367))) uf_9) (= ?x369 uf_9)) (and (up_67 (uf_58 (uf_59 ?x365) (uf_66 ?x366 ?x370 ?x367))) (= (uf_24 ?x365 (uf_66 ?x366 ?x370 ?x367)) uf_9)))) :pat { (uf_40 (uf_41 ?x365) (uf_66 ?x366 ?x370 ?x367)) } :pat { (uf_58 (uf_59 ?x365) (uf_66 ?x366 ?x370 ?x367)) } :pat { (uf_19 (uf_20 ?x365) (uf_66 ?x366 ?x370 ?x367)) }))) :pat { (uf_137 ?x365 ?x366 ?x367 ?x368 ?x369) })
:assumption (forall (?x371 T5) (?x372 Int) (?x373 Int) (?x374 T3) (implies (and (not (= ?x372 0)) (not (= ?x373 0))) (= (uf_66 (uf_66 ?x371 ?x372 ?x374) ?x373 ?x374) (uf_66 ?x371 (+ ?x372 ?x373) ?x374))) :pat { (uf_66 (uf_66 ?x371 ?x372 ?x374) ?x373 ?x374) })
:assumption (forall (?x375 T5) (?x376 Int) (?x377 T3) (and (= (uf_138 (uf_66 ?x375 ?x376 ?x377) ?x375) uf_9) (= (uf_66 ?x375 ?x376 ?x377) (uf_43 ?x377 (+ (uf_116 ?x375) (* ?x376 (uf_139 ?x377)))))) :pat { (uf_66 ?x375 ?x376 ?x377) })
:assumption (forall (?x378 T5) (?x379 T3) (= (uf_140 ?x378 ?x379) ?x378) :pat { (uf_140 ?x378 ?x379) })
:assumption (forall (?x380 T3) (?x381 Int) (not (up_36 (uf_124 ?x380 ?x381))) :pat { (uf_124 ?x380 ?x381) })
:assumption (forall (?x382 T3) (?x383 Int) (= (uf_141 (uf_124 ?x382 ?x383)) uf_9) :pat { (uf_124 ?x382 ?x383) })
:assumption (forall (?x384 T3) (?x385 Int) (= (uf_142 (uf_124 ?x384 ?x385)) 0) :pat { (uf_124 ?x384 ?x385) })
:assumption (forall (?x386 T3) (?x387 Int) (= (uf_143 (uf_124 ?x386 ?x387)) ?x387) :pat { (uf_124 ?x386 ?x387) })
:assumption (forall (?x388 T3) (?x389 Int) (= (uf_144 (uf_124 ?x388 ?x389)) ?x388) :pat { (uf_124 ?x388 ?x389) })
:assumption (forall (?x390 T5) (?x391 T6) (iff (= (uf_15 ?x390 ?x391) uf_9) (= (uf_145 ?x390 ?x391) uf_9)) :pat { (uf_145 ?x390 ?x391) })
:assumption (forall (?x392 T5) (?x393 T6) (iff (= (uf_15 ?x392 ?x393) uf_9) (up_146 ?x392 ?x393)) :pat { (uf_15 ?x392 ?x393) })
:assumption (forall (?x394 T5) (?x395 T6) (iff (= (uf_15 ?x394 ?x395) uf_9) (= (uf_147 ?x394 ?x395) uf_9)) :pat { (uf_15 ?x394 ?x395) })
:assumption (forall (?x396 T5) (?x397 T4) (?x398 T5) (iff (= (uf_15 ?x396 (uf_53 ?x397 ?x398)) uf_9) (= (uf_147 ?x396 (uf_53 ?x397 ?x398)) uf_9)) :pat { (uf_147 ?x396 (uf_53 ?x397 ?x398)) (uf_148 ?x396) })
:assumption (forall (?x399 T5) (?x400 T4) (?x401 T5) (implies (= (uf_15 ?x399 (uf_53 ?x400 ?x401)) uf_9) (= (uf_148 ?x399) uf_9)) :pat { (uf_15 ?x399 (uf_53 ?x400 ?x401)) })
:assumption (forall (?x402 T6) (?x403 T6) (implies (forall (?x404 T5) (and (implies (= (uf_15 ?x404 ?x402) uf_9) (not (= (uf_15 ?x404 ?x403) uf_9))) (implies (= (uf_15 ?x404 ?x403) uf_9) (not (= (uf_15 ?x404 ?x402) uf_9)))) :pat { (uf_18 ?x404) }) (= (uf_131 ?x402 ?x403) uf_9)) :pat { (uf_131 ?x402 ?x403) })
:assumption (forall (?x405 T5) (?x406 T6) (?x407 T6) (implies (and (= (uf_131 ?x406 ?x407) uf_9) (= (uf_15 ?x405 ?x407) uf_9)) (= (uf_133 ?x405 ?x406 ?x407) 2)) :pat { (uf_131 ?x406 ?x407) (uf_15 ?x405 ?x407) })
:assumption (forall (?x408 T5) (?x409 T6) (?x410 T6) (implies (and (= (uf_131 ?x409 ?x410) uf_9) (= (uf_15 ?x408 ?x409) uf_9)) (= (uf_133 ?x408 ?x409 ?x410) 1)) :pat { (uf_131 ?x409 ?x410) (uf_15 ?x408 ?x409) })
:assumption (forall (?x411 T5) (= (uf_15 ?x411 uf_149) uf_9) :pat { (uf_15 ?x411 uf_149) })
:assumption (forall (?x412 T5) (= (uf_150 (uf_151 ?x412)) 1))
:assumption (= (uf_150 uf_152) 0)
:assumption (forall (?x413 T6) (?x414 T6) (implies (= (uf_153 ?x413 ?x414) uf_9) (= ?x413 ?x414)) :pat { (uf_153 ?x413 ?x414) })
:assumption (forall (?x415 T6) (?x416 T6) (implies (forall (?x417 T5) (iff (= (uf_15 ?x417 ?x415) uf_9) (= (uf_15 ?x417 ?x416) uf_9)) :pat { (uf_18 ?x417) }) (= (uf_153 ?x415 ?x416) uf_9)) :pat { (uf_153 ?x415 ?x416) })
:assumption (forall (?x418 T6) (?x419 T6) (iff (= (uf_154 ?x418 ?x419) uf_9) (forall (?x420 T5) (implies (= (uf_15 ?x420 ?x418) uf_9) (= (uf_15 ?x420 ?x419) uf_9)) :pat { (uf_15 ?x420 ?x418) } :pat { (uf_15 ?x420 ?x419) })) :pat { (uf_154 ?x418 ?x419) })
:assumption (forall (?x421 T6) (?x422 T6) (?x423 T5) (iff (= (uf_15 ?x423 (uf_155 ?x421 ?x422)) uf_9) (and (= (uf_15 ?x423 ?x421) uf_9) (= (uf_15 ?x423 ?x422) uf_9))) :pat { (uf_15 ?x423 (uf_155 ?x421 ?x422)) })
:assumption (forall (?x424 T6) (?x425 T6) (?x426 T5) (iff (= (uf_15 ?x426 (uf_156 ?x424 ?x425)) uf_9) (and (= (uf_15 ?x426 ?x424) uf_9) (not (= (uf_15 ?x426 ?x425) uf_9)))) :pat { (uf_15 ?x426 (uf_156 ?x424 ?x425)) })
:assumption (forall (?x427 T6) (?x428 T6) (?x429 T5) (iff (= (uf_15 ?x429 (uf_157 ?x427 ?x428)) uf_9) (or (= (uf_15 ?x429 ?x427) uf_9) (= (uf_15 ?x429 ?x428) uf_9))) :pat { (uf_15 ?x429 (uf_157 ?x427 ?x428)) })
:assumption (forall (?x430 T5) (?x431 T5) (iff (= (uf_15 ?x431 (uf_158 ?x430)) uf_9) (and (= ?x430 ?x431) (not (= (uf_116 ?x430) (uf_116 uf_121))))) :pat { (uf_15 ?x431 (uf_158 ?x430)) })
:assumption (forall (?x432 T5) (?x433 T5) (iff (= (uf_15 ?x433 (uf_151 ?x432)) uf_9) (= ?x432 ?x433)) :pat { (uf_15 ?x433 (uf_151 ?x432)) })
:assumption (forall (?x434 T5) (not (= (uf_15 ?x434 uf_152) uf_9)) :pat { (uf_15 ?x434 uf_152) })
:assumption (forall (?x435 T5) (?x436 T5) (= (uf_159 ?x435 ?x436) (uf_43 (uf_124 (uf_144 (uf_13 ?x435)) (+ (uf_143 (uf_13 ?x435)) (uf_143 (uf_13 ?x436)))) (uf_116 ?x435))) :pat { (uf_159 ?x435 ?x436) })
:assumption (forall (?x437 T5) (?x438 Int) (= (uf_160 ?x437 ?x438) (uf_43 (uf_124 (uf_144 (uf_13 ?x437)) (- (uf_143 (uf_13 ?x437)) ?x438)) (uf_116 (uf_66 (uf_43 (uf_144 (uf_13 ?x437)) (uf_116 ?x437)) ?x438 (uf_144 (uf_13 ?x437)))))) :pat { (uf_160 ?x437 ?x438) })
:assumption (forall (?x439 T5) (?x440 Int) (= (uf_161 ?x439 ?x440) (uf_43 (uf_124 (uf_144 (uf_13 ?x439)) ?x440) (uf_116 ?x439))) :pat { (uf_161 ?x439 ?x440) })
:assumption (forall (?x441 T4) (?x442 T5) (?x443 T5) (iff (= (uf_15 ?x442 (uf_162 ?x441 ?x443)) uf_9) (or (= ?x442 ?x443) (and (= (uf_136 (uf_58 (uf_59 ?x441) ?x442)) uf_9) (= (uf_15 ?x442 (uf_163 ?x443)) uf_9)))) :pat { (uf_15 ?x442 (uf_162 ?x441 ?x443)) })
:assumption (forall (?x444 T4) (implies (= (uf_164 ?x444) uf_9) (up_165 ?x444)) :pat { (uf_164 ?x444) })
:assumption (= (uf_142 uf_166) 0)
:assumption (= uf_167 (uf_43 uf_166 uf_168))
:assumption (forall (?x445 T4) (?x446 T4) (?x447 T5) (?x448 T5) (and (= (uf_41 (uf_169 ?x445 ?x446 ?x447 ?x448)) (uf_170 (uf_41 ?x446) ?x448 (uf_171 ?x446 ?x447 ?x448))) (and (= (uf_27 (uf_169 ?x445 ?x446 ?x447 ?x448) ?x448) uf_9) (and (= (uf_25 (uf_169 ?x445 ?x446 ?x447 ?x448) ?x448) uf_26) (and (= (uf_38 (uf_169 ?x445 ?x446 ?x447 ?x448) ?x448) (uf_38 ?x446 ?x448)) (and (= (uf_172 (uf_169 ?x445 ?x446 ?x447 ?x448) ?x448) (uf_173 ?x445)) true))))) :pat { (uf_169 ?x445 ?x446 ?x447 ?x448) })
:assumption (forall (?x449 T4) (?x450 T5) (?x451 T5) (implies (not (= (uf_12 (uf_13 ?x450)) uf_14)) (and (= (uf_41 (uf_174 ?x449 ?x450 ?x451)) (uf_170 (uf_41 ?x449) ?x451 (uf_175 ?x449 ?x450 ?x451))) (and (= (uf_27 (uf_174 ?x449 ?x450 ?x451) ?x451) uf_9) (and (= (uf_25 (uf_174 ?x449 ?x450 ?x451) ?x451) ?x450) (and (= (uf_38 (uf_174 ?x449 ?x450 ?x451) ?x451) (uf_38 ?x449 ?x451)) true))))) :pat { (uf_174 ?x449 ?x450 ?x451) })
:assumption (forall (?x452 T4) (?x453 T5) (?x454 Int) (and (= (uf_59 (uf_176 ?x452 ?x453 ?x454)) (uf_59 ?x452)) (and (= (uf_41 (uf_176 ?x452 ?x453 ?x454)) (uf_41 ?x452)) (and (= (uf_20 (uf_176 ?x452 ?x453 ?x454)) (uf_177 (uf_20 ?x452) ?x453 ?x454)) (and (< (uf_173 ?x452) (uf_173 (uf_176 ?x452 ?x453 ?x454))) (and (forall (?x455 T5) (<= (uf_172 ?x452 ?x455) (uf_172 (uf_176 ?x452 ?x455 ?x454) ?x455)) :pat { (uf_172 (uf_176 ?x452 ?x455 ?x454) ?x455) }) (= (uf_178 ?x452 (uf_176 ?x452 ?x453 ?x454)) uf_9)))))) :pat { (uf_176 ?x452 ?x453 ?x454) })
:assumption (forall (?x456 T4) (implies (= (uf_51 ?x456) uf_9) (forall (?x457 T5) (?x458 T5) (implies (and (= (uf_51 ?x456) uf_9) (and (= (uf_15 ?x457 (uf_53 ?x456 ?x458)) uf_9) (= (uf_27 ?x456 ?x458) uf_9))) (and (= (uf_27 ?x456 ?x457) uf_9) (not (= (uf_116 ?x457) 0)))) :pat { (uf_15 ?x457 (uf_53 ?x456 ?x458)) })) :pat { (uf_51 ?x456) })
:assumption (forall (?x459 T4) (?x460 T5) (?x461 T3) (implies (and (= (uf_44 ?x459) uf_9) (= (uf_27 ?x459 ?x460) uf_9)) (= (uf_46 ?x459 ?x459 ?x460 ?x461) uf_9)) :pat { (uf_46 ?x459 ?x459 ?x460 ?x461) })
:assumption (forall (?x462 T4) (?x463 Int) (?x464 T3) (implies (= (uf_51 ?x462) uf_9) (implies (= (uf_141 ?x464) uf_9) (= (uf_53 ?x462 (uf_43 ?x464 ?x463)) uf_152))) :pat { (uf_53 ?x462 (uf_43 ?x464 ?x463)) (uf_141 ?x464) })
:assumption (forall (?x465 T4) (?x466 T4) (?x467 T5) (?x468 T3) (implies (and (= (uf_141 ?x468) uf_9) (= (uf_13 ?x467) ?x468)) (and (iff (= (uf_46 ?x465 ?x466 ?x467 ?x468) uf_9) (= (uf_24 ?x466 ?x467) uf_9)) (= (uf_179 ?x465 ?x466 ?x467 ?x468) uf_9))) :pat { (uf_141 ?x468) (uf_46 ?x465 ?x466 ?x467 ?x468) })
:assumption (forall (?x469 T4) (?x470 T5) (?x471 T5) (implies (and (= (uf_51 ?x469) uf_9) (and (= (uf_27 ?x469 ?x471) uf_9) (= (uf_23 (uf_13 ?x470)) uf_9))) (iff (= (uf_15 ?x470 (uf_53 ?x469 ?x471)) uf_9) (= (uf_25 ?x469 ?x470) ?x471))) :pat { (uf_15 ?x470 (uf_53 ?x469 ?x471)) (uf_23 (uf_13 ?x470)) })
:assumption (forall (?x472 T4) (?x473 T4) (?x474 Int) (?x475 T3) (?x476 T15) (up_182 (uf_19 (uf_20 ?x473) (uf_126 (uf_43 ?x475 ?x474) ?x476))) :pat { (uf_180 ?x475 ?x476) (uf_181 ?x472 ?x473) (uf_19 (uf_20 ?x472) (uf_126 (uf_43 ?x475 ?x474) ?x476)) })
:assumption (forall (?x477 T4) (?x478 Int) (?x479 T3) (?x480 T15) (implies (and (= (uf_55 ?x477) uf_9) (and (= (uf_27 ?x477 (uf_43 ?x479 ?x478)) uf_9) (and (= (uf_180 ?x479 ?x480) uf_9) (= (uf_25 ?x477 (uf_43 ?x479 ?x478)) uf_26)))) (= (uf_19 (uf_20 ?x477) (uf_126 (uf_43 ?x479 ?x478) ?x480)) (uf_183 (uf_184 ?x477 (uf_43 ?x479 ?x478)) (uf_126 (uf_43 ?x479 ?x478) ?x480)))) :pat { (uf_180 ?x479 ?x480) (uf_19 (uf_20 ?x477) (uf_126 (uf_43 ?x479 ?x478) ?x480)) })
:assumption (forall (?x481 T4) (?x482 Int) (?x483 T3) (?x484 T15) (?x485 T15) (implies (and (= (uf_55 ?x481) uf_9) (and (= (uf_185 ?x483 ?x484 ?x485) uf_9) (and (= (uf_27 ?x481 (uf_43 ?x483 ?x482)) uf_9) (or (= (uf_28 (uf_19 (uf_20 ?x481) (uf_126 (uf_43 ?x483 ?x482) ?x484))) uf_26) (= (uf_28 (uf_183 (uf_184 ?x481 (uf_43 ?x483 ?x482)) (uf_126 (uf_43 ?x483 ?x482) ?x484))) uf_26))))) (= (uf_19 (uf_20 ?x481) (uf_126 (uf_43 ?x483 ?x482) ?x485)) (uf_183 (uf_184 ?x481 (uf_43 ?x483 ?x482)) (uf_126 (uf_43 ?x483 ?x482) ?x485)))) :pat { (uf_185 ?x483 ?x484 ?x485) (uf_19 (uf_20 ?x481) (uf_126 (uf_43 ?x483 ?x482) ?x485)) })
:assumption (forall (?x486 T4) (?x487 T5) (= (uf_184 ?x486 ?x487) (uf_30 (uf_19 (uf_20 ?x486) ?x487))) :pat { (uf_184 ?x486 ?x487) })
:assumption (forall (?x488 T4) (?x489 T5) (?x490 T5) (?x491 T15) (?x492 Int) (?x493 Int) (?x494 T3) (implies (and (= (uf_51 ?x488) uf_9) (and (= (uf_27 ?x488 ?x490) uf_9) (and (= (uf_186 ?x489 ?x490) uf_9) (and (= (uf_187 ?x491 ?x493) uf_9) (and (<= 0 ?x492) (< ?x492 ?x493)))))) (= (uf_19 (uf_20 ?x488) (uf_66 (uf_126 ?x489 ?x491) ?x492 ?x494)) (uf_10 (uf_189 ?x490) (uf_66 (uf_126 ?x489 ?x491) ?x492 ?x494)))) :pat { (uf_49 ?x488 ?x490) (uf_186 ?x489 ?x490) (uf_19 (uf_20 ?x488) (uf_66 (uf_126 ?x489 ?x491) ?x492 ?x494)) (uf_187 ?x491 ?x493) } :pat { (uf_188 ?x488 ?x490 ?x489 (uf_66 (uf_126 ?x489 ?x491) ?x492 ?x494)) (uf_187 ?x491 ?x493) })
:assumption (forall (?x495 T4) (?x496 T5) (?x497 T5) (?x498 T15) (implies (and (= (uf_51 ?x495) uf_9) (and (= (uf_27 ?x495 ?x497) uf_9) (and (= (uf_186 ?x496 ?x497) uf_9) (= (uf_190 ?x498) uf_9)))) (and (= (uf_186 ?x496 ?x497) uf_9) (= (uf_19 (uf_20 ?x495) (uf_126 ?x496 ?x498)) (uf_10 (uf_189 ?x497) (uf_126 ?x496 ?x498))))) :pat { (uf_186 ?x496 ?x497) (uf_19 (uf_20 ?x495) (uf_126 ?x496 ?x498)) } :pat { (uf_188 ?x495 ?x497 ?x496 (uf_126 ?x496 ?x498)) })
:assumption (forall (?x499 T4) (?x500 T5) (?x501 T5) (?x502 T5) (= (uf_188 ?x499 ?x500 ?x501 ?x502) ?x502) :pat { (uf_188 ?x499 ?x500 ?x501 ?x502) })
:assumption (forall (?x503 T5) (?x504 T5) (implies (forall (?x505 T4) (implies (= (uf_49 ?x505 ?x504) uf_9) (= (uf_27 ?x505 ?x503) uf_9)) :pat { (uf_191 ?x505) }) (= (uf_186 ?x503 ?x504) uf_9)) :pat { (uf_186 ?x503 ?x504) })
:assumption (forall (?x506 T5) (?x507 T4) (?x508 T4) (?x509 T5) (up_193 (uf_15 ?x509 (uf_192 (uf_11 ?x508 ?x506)))) :pat { (uf_15 ?x509 (uf_192 (uf_11 ?x507 ?x506))) (uf_178 ?x507 ?x508) })
:assumption (forall (?x510 T5) (?x511 T4) (?x512 T4) (?x513 T5) (up_193 (uf_15 ?x513 (uf_16 ?x512 ?x510))) :pat { (uf_15 ?x513 (uf_16 ?x511 ?x510)) (uf_178 ?x511 ?x512) })
:assumption (forall (?x514 T4) (?x515 T5) (?x516 T15) (?x517 Int) (?x518 Int) (?x519 T3) (implies (and (= (uf_51 ?x514) uf_9) (and (= (uf_194 ?x516 ?x517 ?x519) uf_9) (and (<= 0 ?x518) (< ?x518 ?x517)))) (= (uf_136 (uf_58 (uf_59 ?x514) (uf_66 (uf_126 ?x515 ?x516) ?x518 ?x519))) uf_9)) :pat { (uf_194 ?x516 ?x517 ?x519) (uf_136 (uf_58 (uf_59 ?x514) (uf_66 (uf_126 ?x515 ?x516) ?x518 ?x519))) })
:assumption (forall (?x520 T4) (?x521 Int) (?x522 T5) (?x523 Int) (?x524 Int) (?x525 T3) (implies (and (= (uf_55 ?x520) uf_9) (and (= (uf_22 ?x525) uf_9) (and (= (uf_15 (uf_43 (uf_124 ?x525 ?x523) ?x521) (uf_16 ?x520 ?x522)) uf_9) (and (<= 0 ?x524) (< ?x524 ?x523))))) (= (uf_19 (uf_20 ?x520) (uf_66 (uf_43 ?x525 ?x521) ?x524 ?x525)) (uf_10 (uf_11 ?x520 ?x522) (uf_66 (uf_43 ?x525 ?x521) ?x524 ?x525)))) :pat { (uf_15 (uf_43 (uf_124 ?x525 ?x523) ?x521) (uf_16 ?x520 ?x522)) (uf_19 (uf_20 ?x520) (uf_66 (uf_43 ?x525 ?x521) ?x524 ?x525)) (uf_22 ?x525) })
:assumption (forall (?x526 T4) (?x527 Int) (?x528 T5) (?x529 Int) (?x530 Int) (?x531 T3) (implies (and (= (uf_55 ?x526) uf_9) (and (= (uf_22 ?x531) uf_9) (and (= (uf_15 (uf_43 (uf_124 ?x531 ?x529) ?x527) (uf_16 ?x526 ?x528)) uf_9) (and (<= 0 ?x530) (< ?x530 ?x529))))) (and (= (uf_24 ?x526 (uf_66 (uf_43 ?x531 ?x527) ?x530 ?x531)) uf_9) (not (= (uf_136 (uf_58 (uf_59 ?x526) (uf_66 (uf_43 ?x531 ?x527) ?x530 ?x531))) uf_9)))) :pat { (uf_15 (uf_43 (uf_124 ?x531 ?x529) ?x527) (uf_16 ?x526 ?x528)) (uf_58 (uf_59 ?x526) (uf_66 (uf_43 ?x531 ?x527) ?x530 ?x531)) (uf_22 ?x531) } :pat { (uf_15 (uf_43 (uf_124 ?x531 ?x529) ?x527) (uf_16 ?x526 ?x528)) (uf_25 ?x526 (uf_66 (uf_43 ?x531 ?x527) ?x530 ?x531)) (uf_22 ?x531) })
:assumption (forall (?x532 T4) (?x533 T5) (?x534 T5) (?x535 T15) (?x536 Int) (?x537 Int) (?x538 T3) (implies (and (= (uf_55 ?x532) uf_9) (and (= (uf_15 ?x533 (uf_16 ?x532 ?x534)) uf_9) (and (= (uf_187 ?x535 ?x536) uf_9) (and (<= 0 ?x537) (< ?x537 ?x536))))) (and (= (uf_24 ?x532 (uf_66 (uf_126 ?x533 ?x535) ?x537 ?x538)) uf_9) (not (= (uf_136 (uf_58 (uf_59 ?x532) (uf_66 (uf_126 ?x533 ?x535) ?x537 ?x538))) uf_9)))) :pat { (uf_15 ?x533 (uf_16 ?x532 ?x534)) (uf_187 ?x535 ?x536) (uf_58 (uf_59 ?x532) (uf_66 (uf_126 ?x533 ?x535) ?x537 ?x538)) } :pat { (uf_15 ?x533 (uf_16 ?x532 ?x534)) (uf_187 ?x535 ?x536) (uf_25 ?x532 (uf_66 (uf_126 ?x533 ?x535) ?x537 ?x538)) })
:assumption (forall (?x539 T4) (?x540 T5) (?x541 T5) (?x542 T15) (?x543 Int) (?x544 Int) (?x545 T3) (implies (and (= (uf_55 ?x539) uf_9) (and (= (uf_15 ?x540 (uf_16 ?x539 ?x541)) uf_9) (and (= (uf_187 ?x542 ?x543) uf_9) (and (<= 0 ?x544) (< ?x544 ?x543))))) (= (uf_19 (uf_20 ?x539) (uf_66 (uf_126 ?x540 ?x542) ?x544 ?x545)) (uf_10 (uf_11 ?x539 ?x541) (uf_66 (uf_126 ?x540 ?x542) ?x544 ?x545)))) :pat { (uf_15 ?x540 (uf_16 ?x539 ?x541)) (uf_187 ?x542 ?x543) (uf_19 (uf_20 ?x539) (uf_66 (uf_126 ?x540 ?x542) ?x544 ?x545)) })
:assumption (forall (?x546 T4) (?x547 T5) (?x548 T5) (?x549 T15) (implies (and (= (uf_55 ?x546) uf_9) (and (= (uf_15 ?x547 (uf_16 ?x546 ?x548)) uf_9) (= (uf_190 ?x549) uf_9))) (and (= (uf_24 ?x546 (uf_126 ?x547 ?x549)) uf_9) (not (= (uf_136 (uf_58 (uf_59 ?x546) (uf_126 ?x547 ?x549))) uf_9)))) :pat { (uf_15 ?x547 (uf_16 ?x546 ?x548)) (uf_190 ?x549) (uf_25 ?x546 (uf_126 ?x547 ?x549)) } :pat { (uf_15 ?x547 (uf_16 ?x546 ?x548)) (uf_190 ?x549) (uf_58 (uf_59 ?x546) (uf_126 ?x547 ?x549)) })
:assumption (forall (?x550 T4) (?x551 T5) (?x552 T5) (implies (and (= (uf_55 ?x550) uf_9) (= (uf_15 ?x551 (uf_16 ?x550 ?x552)) uf_9)) (and (= (uf_24 ?x550 ?x551) uf_9) (not (= (uf_136 (uf_58 (uf_59 ?x550) ?x551)) uf_9)))) :pat { (uf_55 ?x550) (uf_15 ?x551 (uf_16 ?x550 ?x552)) (uf_40 (uf_41 ?x550) ?x551) } :pat { (uf_55 ?x550) (uf_15 ?x551 (uf_16 ?x550 ?x552)) (uf_58 (uf_59 ?x550) ?x551) })
:assumption (forall (?x553 T4) (?x554 T5) (?x555 T5) (?x556 T15) (implies (and (= (uf_15 ?x554 (uf_16 ?x553 ?x555)) uf_9) (= (uf_190 ?x556) uf_9)) (= (uf_19 (uf_20 ?x553) (uf_126 ?x554 ?x556)) (uf_10 (uf_11 ?x553 ?x555) (uf_126 ?x554 ?x556)))) :pat { (uf_15 ?x554 (uf_16 ?x553 ?x555)) (uf_190 ?x556) (uf_19 (uf_20 ?x553) (uf_126 ?x554 ?x556)) })
:assumption (forall (?x557 T4) (?x558 T5) (?x559 T5) (implies (= (uf_195 ?x557 ?x558 ?x559) uf_9) (= (uf_196 ?x557 ?x558 ?x559) uf_9)) :pat { (uf_195 ?x557 ?x558 ?x559) })
:assumption (forall (?x560 T4) (?x561 T5) (?x562 T5) (?x563 T5) (implies (and (up_197 (uf_13 ?x562)) (and (= (uf_15 ?x562 (uf_16 ?x560 ?x561)) uf_9) (forall (?x564 T4) (implies (and (= (uf_46 ?x564 ?x564 ?x562 (uf_13 ?x562)) uf_9) (and (= (uf_11 ?x564 ?x561) (uf_11 ?x560 ?x561)) (= (uf_16 ?x564 ?x561) (uf_16 ?x560 ?x561)))) (= (uf_145 ?x563 (uf_53 ?x564 ?x562)) uf_9))))) (and (= (uf_195 ?x560 ?x563 ?x561) uf_9) (= (uf_145 ?x563 (uf_53 ?x560 ?x562)) uf_9))) :pat { (uf_15 ?x562 (uf_16 ?x560 ?x561)) (uf_195 ?x560 ?x563 ?x561) })
:assumption (forall (?x565 T4) (?x566 T5) (?x567 T5) (?x568 T5) (implies (and (not (up_197 (uf_13 ?x567))) (and (= (uf_15 ?x567 (uf_16 ?x565 ?x566)) uf_9) (= (uf_145 ?x568 (uf_53 ?x565 ?x567)) uf_9))) (and (= (uf_196 ?x565 ?x568 ?x566) uf_9) (= (uf_145 ?x568 (uf_53 ?x565 ?x567)) uf_9))) :pat { (uf_15 ?x567 (uf_16 ?x565 ?x566)) (uf_196 ?x565 ?x568 ?x566) })
:assumption (forall (?x569 T4) (?x570 T5) (?x571 T5) (implies (and (= (uf_55 ?x569) uf_9) (= (uf_15 ?x571 (uf_16 ?x569 ?x570)) uf_9)) (= (uf_196 ?x569 ?x571 ?x570) uf_9)) :pat { (uf_196 ?x569 ?x571 ?x570) })
:assumption (forall (?x572 T4) (?x573 T5) (implies (and (= (uf_55 ?x572) uf_9) (and (= (uf_27 ?x572 ?x573) uf_9) (and (= (uf_25 ?x572 ?x573) uf_26) (and (= (uf_48 ?x573 (uf_13 ?x573)) uf_9) (and (= (uf_24 ?x572 ?x573) uf_9) (and (not (= (uf_12 (uf_13 ?x573)) uf_14)) (= (uf_23 (uf_13 ?x573)) uf_9))))))) (= (uf_196 ?x572 ?x573 ?x573) uf_9)) :pat { (uf_196 ?x572 ?x573 ?x573) })
:assumption (forall (?x574 T4) (?x575 T5) (?x576 T5) (implies (= (uf_196 ?x574 ?x575 ?x576) uf_9) (and (= (uf_15 ?x575 (uf_16 ?x574 ?x576)) uf_9) (and (= (uf_27 ?x574 ?x575) uf_9) (forall (?x577 T5) (implies (and (not (up_197 (uf_13 ?x575))) (= (uf_15 ?x577 (uf_53 ?x574 ?x575)) uf_9)) (= (uf_147 ?x577 (uf_192 (uf_11 ?x574 ?x576))) uf_9)) :pat { (uf_15 ?x577 (uf_53 ?x574 ?x575)) })))) :pat { (uf_196 ?x574 ?x575 ?x576) })
:assumption (forall (?x578 T4) (?x579 T5) (?x580 T5) (?x581 T16) (iff (= (uf_198 ?x578 ?x579 ?x580 ?x581) uf_9) (= (uf_195 ?x578 ?x579 ?x580) uf_9)) :pat { (uf_198 ?x578 ?x579 ?x580 ?x581) })
:assumption (forall (?x582 T4) (?x583 T5) (?x584 T5) (?x585 T16) (implies (= (uf_198 ?x582 ?x583 ?x584 ?x585) uf_9) (up_199 ?x582 ?x583 ?x585)) :pat { (uf_198 ?x582 ?x583 ?x584 ?x585) })
:assumption (forall (?x586 T4) (?x587 T5) (?x588 T5) (?x589 T16) (iff (= (uf_200 ?x586 ?x587 ?x588 ?x589) uf_9) (= (uf_196 ?x586 ?x587 ?x588) uf_9)) :pat { (uf_200 ?x586 ?x587 ?x588 ?x589) })
:assumption (forall (?x590 T4) (?x591 T5) (?x592 T5) (?x593 T16) (implies (= (uf_200 ?x590 ?x591 ?x592 ?x593) uf_9) (up_199 ?x590 ?x591 ?x593)) :pat { (uf_200 ?x590 ?x591 ?x592 ?x593) })
:assumption (forall (?x594 T4) (?x595 T5) (= (uf_16 ?x594 ?x595) (uf_192 (uf_11 ?x594 ?x595))) :pat { (uf_16 ?x594 ?x595) })
:assumption (forall (?x596 T4) (?x597 T5) (= (uf_11 ?x596 ?x597) (uf_32 (uf_19 (uf_20 ?x596) ?x597))) :pat { (uf_11 ?x596 ?x597) })
:assumption (forall (?x598 T4) (?x599 Int) (?x600 T3) (= (uf_43 ?x600 (uf_19 (uf_20 ?x598) (uf_43 (uf_6 ?x600) ?x599))) (uf_201 ?x598 (uf_43 (uf_6 ?x600) ?x599) ?x600)) :pat { (uf_43 ?x600 (uf_19 (uf_20 ?x598) (uf_43 (uf_6 ?x600) ?x599))) })
:assumption (forall (?x601 T1) (?x602 T4) (implies (= (uf_202 ?x601 ?x602) uf_9) (= (uf_51 ?x602) uf_9)) :pat { (uf_202 ?x601 ?x602) })
:assumption (forall (?x603 T4) (implies (= (uf_44 ?x603) uf_9) (= (uf_51 ?x603) uf_9)) :pat { (uf_44 ?x603) })
:assumption (forall (?x604 T4) (implies (= (uf_55 ?x604) uf_9) (and (= (uf_51 ?x604) uf_9) (= (uf_44 ?x604) uf_9))) :pat { (uf_55 ?x604) })
:assumption (forall (?x605 T4) (implies (= (uf_203 ?x605) uf_9) (and (= (uf_55 ?x605) uf_9) (<= 0 (uf_173 ?x605)))) :pat { (uf_203 ?x605) })
:assumption (forall (?x606 T3) (implies (= (uf_22 ?x606) uf_9) (forall (?x607 T4) (?x608 Int) (?x609 T5) (iff (= (uf_15 ?x609 (uf_128 ?x607 (uf_43 ?x606 ?x608))) uf_9) (= ?x609 (uf_43 ?x606 ?x608))) :pat { (uf_15 ?x609 (uf_128 ?x607 (uf_43 ?x606 ?x608))) })) :pat { (uf_22 ?x606) })
:assumption (forall (?x610 T3) (implies (= (uf_22 ?x610) uf_9) (forall (?x611 Int) (?x612 T5) (iff (= (uf_15 ?x612 (uf_130 (uf_43 ?x610 ?x611))) uf_9) (= ?x612 (uf_43 ?x610 ?x611))) :pat { (uf_15 ?x612 (uf_130 (uf_43 ?x610 ?x611))) })) :pat { (uf_22 ?x610) })
:assumption (forall (?x613 T4) (?x614 T4) (?x615 T5) (?x616 T3) (iff (= (uf_204 ?x613 ?x614 ?x615 ?x616) uf_9) (and (= (uf_11 ?x613 ?x615) (uf_11 ?x614 ?x615)) (and (= (uf_58 (uf_59 ?x613) ?x615) (uf_58 (uf_59 ?x614) ?x615)) (up_205 ?x613 ?x614 ?x615 ?x616)))) :pat { (uf_204 ?x613 ?x614 ?x615 ?x616) })
:assumption (forall (?x617 T4) (?x618 T4) (?x619 T5) (?x620 T3) (iff (= (uf_206 ?x617 ?x618 ?x619 ?x620) uf_9) (and (= (uf_11 ?x617 ?x619) (uf_11 ?x618 ?x619)) (and (= (uf_53 ?x617 ?x619) (uf_53 ?x618 ?x619)) (and (= (uf_58 (uf_59 ?x617) ?x619) (uf_58 (uf_59 ?x618) ?x619)) (= (uf_123 ?x617 ?x618 ?x619 ?x620) uf_9))))) :pat { (uf_206 ?x617 ?x618 ?x619 ?x620) })
:assumption (forall (?x621 T4) (?x622 T4) (?x623 T5) (?x624 T5) (iff (= (uf_207 ?x621 ?x622 ?x623 ?x624) uf_9) (or (= (uf_206 ?x621 ?x622 ?x624 (uf_13 ?x624)) uf_9) (or (and (not (= (uf_27 ?x621 ?x623) uf_9)) (not (= (uf_27 ?x622 ?x623) uf_9))) (or (and (= (uf_46 ?x621 ?x622 ?x623 (uf_13 ?x623)) uf_9) (= (uf_204 ?x621 ?x622 ?x623 (uf_13 ?x623)) uf_9)) (= (uf_208 (uf_13 ?x623)) uf_9))))) :pat { (uf_207 ?x621 ?x622 ?x623 ?x624) })
:assumption (forall (?x625 T4) (?x626 T4) (?x627 T5) (?x628 T3) (iff (= (uf_179 ?x625 ?x626 ?x627 ?x628) uf_9) (implies (and (= (uf_27 ?x625 ?x627) uf_9) (= (uf_27 ?x626 ?x627) uf_9)) (= (uf_206 ?x625 ?x626 ?x627 ?x628) uf_9))) :pat { (uf_179 ?x625 ?x626 ?x627 ?x628) })
:assumption (forall (?x629 T4) (?x630 T5) (?x631 T3) (implies (up_209 ?x629 ?x630 ?x631) (= (uf_46 ?x629 ?x629 ?x630 ?x631) uf_9)) :pat { (uf_46 ?x629 ?x629 ?x630 ?x631) })
:assumption (forall (?x632 T4) (?x633 T5) (iff (= (uf_68 ?x632 ?x633) uf_9) (and (= (uf_24 ?x632 ?x633) uf_9) (or (and (= (uf_12 (uf_13 ?x633)) uf_14) (and (or (not (= (uf_136 (uf_58 (uf_59 ?x632) ?x633)) uf_9)) (not (= (uf_27 ?x632 (uf_135 (uf_58 (uf_59 ?x632) ?x633))) uf_9))) (and (not (= (uf_12 (uf_13 (uf_135 (uf_58 (uf_59 ?x632) ?x633)))) uf_14)) (or (= (uf_25 ?x632 (uf_135 (uf_58 (uf_59 ?x632) ?x633))) uf_26) (= (uf_210 ?x632 (uf_135 (uf_58 (uf_59 ?x632) ?x633))) uf_9))))) (and (not (= (uf_12 (uf_13 ?x633)) uf_14)) (or (= (uf_25 ?x632 ?x633) uf_26) (= (uf_210 ?x632 ?x633) uf_9)))))) :pat { (uf_68 ?x632 ?x633) })
:assumption (forall (?x634 T4) (?x635 T5) (iff (= (uf_210 ?x634 ?x635) uf_9) (exists (?x636 T5) (and (= (uf_15 ?x635 (uf_192 (uf_11 ?x634 ?x636))) uf_9) (and (= (uf_27 ?x634 ?x636) uf_9) (and (= (uf_25 ?x634 ?x636) uf_26) (and (= (uf_48 ?x636 (uf_13 ?x636)) uf_9) (and (= (uf_24 ?x634 ?x636) uf_9) (and (not (= (uf_12 (uf_13 ?x636)) uf_14)) (and (= (uf_23 (uf_13 ?x636)) uf_9) (= (uf_211 ?x634 ?x636) uf_9)))))))) :pat { (uf_147 ?x635 (uf_192 (uf_11 ?x634 ?x636))) })) :pat { (uf_210 ?x634 ?x635) })
:assumption (forall (?x637 T4) (?x638 T5) (iff (= (uf_211 ?x637 ?x638) uf_9) true) :pat { (uf_211 ?x637 ?x638) })
:assumption (forall (?x639 T4) (?x640 T4) (?x641 T5) (implies (= (uf_178 ?x639 ?x640) uf_9) (up_212 (uf_40 (uf_41 ?x639) ?x641))) :pat { (uf_40 (uf_41 ?x640) ?x641) (uf_178 ?x639 ?x640) })
:assumption (forall (?x642 T4) (?x643 T5) (implies (and (= (uf_51 ?x642) uf_9) (= (uf_24 ?x642 ?x643) uf_9)) (< 0 (uf_116 ?x643))) :pat { (uf_24 ?x642 ?x643) })
:assumption (forall (?x644 T4) (?x645 T5) (implies (= (uf_51 ?x644) uf_9) (iff (= (uf_24 ?x644 ?x645) uf_9) (up_213 (uf_58 (uf_59 ?x644) ?x645)))) :pat { (uf_24 ?x644 ?x645) })
:assumption (forall (?x646 T4) (?x647 T5) (iff (= (uf_61 ?x646 ?x647) uf_9) (and (= (uf_24 ?x646 ?x647) uf_9) (and (= (uf_25 ?x646 ?x647) uf_26) (not (= (uf_27 ?x646 ?x647) uf_9))))) :pat { (uf_61 ?x646 ?x647) })
:assumption (forall (?x648 T4) (?x649 T5) (= (uf_53 ?x648 ?x649) (uf_34 (uf_19 (uf_20 ?x648) (uf_126 ?x649 (uf_214 (uf_13 ?x649)))))) :pat { (uf_53 ?x648 ?x649) })
:assumption (forall (?x650 T11) (and (not (= (uf_12 (uf_13 (uf_215 ?x650))) uf_14)) (= (uf_23 (uf_13 (uf_215 ?x650))) uf_9)) :pat { (uf_215 ?x650) })
:assumption up_216
:assumption (forall (?x651 T4) (?x652 T5) (implies (= (uf_23 (uf_13 ?x652)) uf_9) (= (uf_172 ?x651 ?x652) (uf_217 (uf_40 (uf_41 ?x651) ?x652)))) :pat { (uf_23 (uf_13 ?x652)) (uf_172 ?x651 ?x652) })
:assumption (forall (?x653 T4) (?x654 T5) (implies (= (uf_22 (uf_13 ?x654)) uf_9) (= (uf_172 ?x653 ?x654) (uf_217 (uf_40 (uf_41 ?x653) (uf_135 (uf_58 (uf_59 ?x653) ?x654)))))) :pat { (uf_22 (uf_13 ?x654)) (uf_172 ?x653 ?x654) })
:assumption (forall (?x655 T4) (?x656 T5) (implies (= (uf_23 (uf_13 ?x656)) uf_9) (iff (= (uf_27 ?x655 ?x656) uf_9) (up_218 (uf_40 (uf_41 ?x655) ?x656)))) :pat { (uf_23 (uf_13 ?x656)) (uf_27 ?x655 ?x656) })
:assumption (forall (?x657 T4) (?x658 T5) (implies (= (uf_22 (uf_13 ?x658)) uf_9) (iff (= (uf_27 ?x657 ?x658) uf_9) (up_218 (uf_40 (uf_41 ?x657) (uf_135 (uf_58 (uf_59 ?x657) ?x658)))))) :pat { (uf_22 (uf_13 ?x658)) (uf_27 ?x657 ?x658) })
:assumption (forall (?x659 T4) (?x660 T5) (implies (= (uf_23 (uf_13 ?x660)) uf_9) (= (uf_25 ?x659 ?x660) (uf_215 (uf_40 (uf_41 ?x659) ?x660)))) :pat { (uf_23 (uf_13 ?x660)) (uf_25 ?x659 ?x660) })
:assumption (forall (?x661 T4) (?x662 T5) (implies (= (uf_22 (uf_13 ?x662)) uf_9) (= (uf_25 ?x661 ?x662) (uf_25 ?x661 (uf_135 (uf_58 (uf_59 ?x661) ?x662))))) :pat { (uf_22 (uf_13 ?x662)) (uf_25 ?x661 ?x662) })
:assumption (forall (?x663 T5) (?x664 T3) (= (uf_126 ?x663 (uf_214 ?x664)) (uf_43 uf_219 (uf_220 ?x663 (uf_214 ?x664)))) :pat { (uf_126 ?x663 (uf_214 ?x664)) })
:assumption (up_197 uf_37)
:assumption (forall (?x665 T17) (?x666 T17) (?x667 T15) (implies (= (uf_224 (uf_225 (uf_222 ?x665 ?x667)) (uf_225 (uf_222 ?x666 ?x667))) uf_9) (= (uf_221 (uf_222 ?x665 ?x667) (uf_222 ?x666 ?x667)) uf_9)) :pat { (uf_221 (uf_222 ?x665 ?x667) (uf_222 ?x666 (uf_223 ?x667))) })
:assumption (forall (?x668 T17) (?x669 T17) (implies (forall (?x670 T15) (= (uf_221 (uf_222 ?x668 ?x670) (uf_222 ?x669 ?x670)) uf_9)) (= (uf_224 ?x668 ?x669) uf_9)) :pat { (uf_224 ?x668 ?x669) })
:assumption (forall (?x671 T17) (= (uf_225 (uf_226 ?x671)) ?x671))
:assumption (forall (?x672 Int) (?x673 Int) (iff (= (uf_221 ?x672 ?x673) uf_9) (= ?x672 ?x673)) :pat { (uf_221 ?x672 ?x673) })
:assumption (forall (?x674 T17) (?x675 T17) (iff (= (uf_224 ?x674 ?x675) uf_9) (= ?x674 ?x675)) :pat { (uf_224 ?x674 ?x675) })
:assumption (forall (?x676 T3) (?x677 T15) (?x678 T3) (implies (and (= (uf_227 ?x676 ?x677 ?x678) uf_9) (= (uf_228 ?x678) uf_9)) (= (uf_223 ?x677) ?x677)) :pat { (uf_227 ?x676 ?x677 ?x678) (uf_228 ?x678) })
:assumption (forall (?x679 T3) (implies (= (uf_228 ?x679) uf_9) (= (uf_22 ?x679) uf_9)) :pat { (uf_228 ?x679) })
:assumption (forall (?x680 T17) (?x681 T15) (?x682 T15) (?x683 Int) (or (= (uf_222 (uf_229 ?x680 ?x681 ?x683) ?x682) (uf_222 ?x680 ?x682)) (= ?x681 ?x682)) :pat { (uf_222 (uf_229 ?x680 ?x681 ?x683) ?x682) })
:assumption (forall (?x684 T17) (?x685 T15) (?x686 Int) (= (uf_222 (uf_229 ?x684 ?x685 ?x686) ?x685) ?x686) :pat { (uf_222 (uf_229 ?x684 ?x685 ?x686) ?x685) })
:assumption (forall (?x687 T15) (= (uf_222 uf_230 ?x687) 0))
:assumption (forall (?x688 T17) (?x689 T15) (?x690 Int) (?x691 Int) (?x692 Int) (?x693 Int) (= (uf_231 ?x688 ?x689 ?x690 ?x691 ?x692 ?x693) (uf_229 ?x688 ?x689 (uf_99 (uf_222 ?x688 ?x689) ?x690 ?x691 ?x692 ?x693))) :pat { (uf_231 ?x688 ?x689 ?x690 ?x691 ?x692 ?x693) })
:assumption (forall (?x694 T4) (?x695 T5) (implies (= (uf_51 ?x694) uf_9) (and (= (uf_233 (uf_232 ?x694 ?x695)) (uf_116 ?x695)) (= (uf_234 (uf_232 ?x694 ?x695)) ?x694))) :pat { (uf_232 ?x694 ?x695) })
:assumption (forall (?x696 T18) (= (uf_51 (uf_234 ?x696)) uf_9))
:assumption (= (uf_51 (uf_234 uf_235)) uf_9)
:assumption (forall (?x697 T4) (?x698 T5) (or (<= (uf_172 ?x697 ?x698) (uf_173 ?x697)) (not (up_213 (uf_58 (uf_59 ?x697) ?x698)))) :pat { (uf_40 (uf_41 ?x697) ?x698) })
:assumption (forall (?x699 T4) (?x700 T5) (implies (and (= (uf_51 ?x699) uf_9) (= (uf_136 (uf_58 (uf_59 ?x699) ?x700)) uf_9)) (= (uf_12 (uf_13 ?x700)) uf_14)) :pat { (uf_136 (uf_58 (uf_59 ?x699) ?x700)) })
:assumption (forall (?x701 T4) (?x702 T5) (implies (= (uf_24 ?x701 ?x702) uf_9) (= (uf_24 ?x701 (uf_135 (uf_58 (uf_59 ?x701) ?x702))) uf_9)) :pat { (uf_24 ?x701 ?x702) (uf_58 (uf_59 ?x701) (uf_135 (uf_58 (uf_59 ?x701) ?x702))) })
:assumption (forall (?x703 T14) (and (not (= (uf_12 (uf_13 (uf_135 ?x703))) uf_14)) (= (uf_23 (uf_13 (uf_135 ?x703))) uf_9)) :pat { (uf_135 ?x703) })
:assumption (forall (?x704 T5) (?x705 T15) (implies (<= 0 (uf_237 ?x705)) (= (uf_116 (uf_126 (uf_236 ?x704 ?x705) ?x705)) (uf_116 ?x704))) :pat { (uf_126 (uf_236 ?x704 ?x705) ?x705) })
:assumption (forall (?x706 T5) (?x707 T15) (= (uf_236 ?x706 ?x707) (uf_43 (uf_238 ?x707) (uf_239 ?x706 ?x707))) :pat { (uf_236 ?x706 ?x707) })
:assumption (forall (?x708 Int) (?x709 T15) (= (uf_236 (uf_126 (uf_43 (uf_238 ?x709) ?x708) ?x709) ?x709) (uf_43 (uf_238 ?x709) ?x708)) :pat { (uf_236 (uf_126 (uf_43 (uf_238 ?x709) ?x708) ?x709) ?x709) })
:assumption (forall (?x710 T5) (?x711 T3) (implies (= (uf_48 ?x710 ?x711) uf_9) (= ?x710 (uf_43 ?x711 (uf_116 ?x710)))) :pat { (uf_48 ?x710 ?x711) })
:assumption (forall (?x712 T5) (?x713 T3) (iff (= (uf_48 ?x712 ?x713) uf_9) (= (uf_13 ?x712) ?x713)))
:assumption (= uf_121 (uf_43 uf_240 0))
:assumption (forall (?x714 T15) (?x715 Int) (and (not (up_242 (uf_241 ?x714 ?x715))) (and (= (uf_243 (uf_241 ?x714 ?x715)) ?x714) (= (uf_244 (uf_241 ?x714 ?x715)) ?x715))) :pat { (uf_241 ?x714 ?x715) })
:assumption (forall (?x716 T5) (?x717 T15) (and (= (uf_245 (uf_220 ?x716 ?x717)) ?x716) (= (uf_246 (uf_220 ?x716 ?x717)) ?x717)) :pat { (uf_220 ?x716 ?x717) })
:assumption (forall (?x718 T3) (?x719 Int) (= (uf_116 (uf_43 ?x718 ?x719)) ?x719))
:assumption (forall (?x720 T3) (?x721 Int) (= (uf_13 (uf_43 ?x720 ?x721)) ?x720))
:assumption (forall (?x722 T3) (?x723 T3) (?x724 Int) (?x725 Int) (iff (= (uf_247 ?x722 ?x723 ?x724 ?x725) uf_9) (and (up_248 ?x722 ?x723) (and (= (uf_249 ?x722 ?x723) ?x724) (= (uf_250 ?x722 ?x723) ?x725)))) :pat { (uf_247 ?x722 ?x723 ?x724 ?x725) })
:assumption (forall (?x726 T5) (= (uf_138 ?x726 ?x726) uf_9) :pat { (uf_13 ?x726) })
:assumption (forall (?x727 T5) (?x728 T5) (?x729 T5) (implies (and (= (uf_138 ?x727 ?x728) uf_9) (= (uf_138 ?x728 ?x729) uf_9)) (= (uf_138 ?x727 ?x729) uf_9)) :pat { (uf_138 ?x727 ?x728) (uf_138 ?x728 ?x729) })
:assumption (forall (?x730 T12) (?x731 T5) (?x732 T5) (?x733 T11) (or (= ?x731 ?x732) (= (uf_40 (uf_170 ?x730 ?x731 ?x733) ?x732) (uf_40 ?x730 ?x732))))
:assumption (forall (?x734 T12) (?x735 T5) (?x736 T11) (= (uf_40 (uf_170 ?x734 ?x735 ?x736) ?x735) ?x736))
:assumption (forall (?x737 T13) (?x738 T5) (?x739 T5) (?x740 T14) (or (= ?x738 ?x739) (= (uf_58 (uf_251 ?x737 ?x738 ?x740) ?x739) (uf_58 ?x737 ?x739))))
:assumption (forall (?x741 T13) (?x742 T5) (?x743 T14) (= (uf_58 (uf_251 ?x741 ?x742 ?x743) ?x742) ?x743))
:assumption (forall (?x744 T9) (?x745 T5) (?x746 T5) (?x747 Int) (or (= ?x745 ?x746) (= (uf_19 (uf_177 ?x744 ?x745 ?x747) ?x746) (uf_19 ?x744 ?x746))))
:assumption (forall (?x748 T9) (?x749 T5) (?x750 Int) (= (uf_19 (uf_177 ?x748 ?x749 ?x750) ?x749) ?x750))
:assumption (= uf_26 (uf_43 uf_252 uf_253))
:assumption (= (uf_22 uf_254) uf_9)
:assumption (= (uf_22 uf_255) uf_9)
:assumption (= (uf_22 uf_84) uf_9)
:assumption (= (uf_22 uf_4) uf_9)
:assumption (= (uf_22 uf_91) uf_9)
:assumption (= (uf_22 uf_7) uf_9)
:assumption (= (uf_22 uf_83) uf_9)
:assumption (= (uf_22 uf_87) uf_9)
:assumption (= (uf_22 uf_90) uf_9)
:assumption (= (uf_22 uf_94) uf_9)
:assumption (= (uf_208 uf_252) uf_9)
:assumption (= (uf_22 uf_256) uf_9)
:assumption (= (uf_22 uf_219) uf_9)
:assumption (= (uf_22 uf_257) uf_9)
:assumption (= (uf_22 uf_258) uf_9)
:assumption (= (uf_22 uf_240) uf_9)
:assumption (forall (?x751 T3) (implies (= (uf_22 ?x751) uf_9) (not (up_36 ?x751))) :pat { (uf_22 ?x751) })
:assumption (forall (?x752 T3) (= (uf_22 (uf_6 ?x752)) uf_9) :pat { (uf_6 ?x752) })
:assumption (forall (?x753 T3) (?x754 T3) (= (uf_22 (uf_259 ?x753 ?x754)) uf_9) :pat { (uf_259 ?x753 ?x754) })
:assumption (forall (?x755 T3) (implies (= (uf_208 ?x755) uf_9) (= (uf_23 ?x755) uf_9)) :pat { (uf_208 ?x755) })
:assumption (forall (?x756 T3) (implies (= (uf_141 ?x756) uf_9) (= (uf_23 ?x756) uf_9)) :pat { (uf_141 ?x756) })
:assumption (forall (?x757 T3) (implies (= (uf_260 ?x757) uf_9) (= (uf_23 ?x757) uf_9)) :pat { (uf_260 ?x757) })
:assumption (forall (?x758 T3) (iff (= (uf_208 ?x758) uf_9) (= (uf_12 ?x758) uf_261)) :pat { (uf_208 ?x758) })
:assumption (forall (?x759 T3) (iff (= (uf_141 ?x759) uf_9) (= (uf_12 ?x759) uf_262)) :pat { (uf_141 ?x759) })
:assumption (forall (?x760 T3) (iff (= (uf_260 ?x760) uf_9) (= (uf_12 ?x760) uf_263)) :pat { (uf_260 ?x760) })
:assumption (forall (?x761 T3) (iff (= (uf_22 ?x761) uf_9) (= (uf_12 ?x761) uf_14)) :pat { (uf_22 ?x761) })
:assumption (forall (?x762 T3) (?x763 T3) (= (uf_142 (uf_259 ?x762 ?x763)) (+ (uf_142 ?x762) 23)) :pat { (uf_259 ?x762 ?x763) })
:assumption (forall (?x764 T3) (= (uf_142 (uf_6 ?x764)) (+ (uf_142 ?x764) 17)) :pat { (uf_6 ?x764) })
:assumption (forall (?x765 T3) (?x766 T3) (= (uf_264 (uf_259 ?x765 ?x766)) ?x765) :pat { (uf_259 ?x765 ?x766) })
:assumption (forall (?x767 T3) (?x768 T3) (= (uf_265 (uf_259 ?x767 ?x768)) ?x768) :pat { (uf_259 ?x767 ?x768) })
:assumption (forall (?x769 T3) (= (uf_139 (uf_6 ?x769)) 8) :pat { (uf_6 ?x769) })
:assumption (forall (?x770 T3) (= (uf_266 (uf_6 ?x770)) ?x770) :pat { (uf_6 ?x770) })
:assumption (= (uf_260 uf_267) uf_9)
:assumption (= (uf_260 uf_37) uf_9)
:assumption (= (uf_142 uf_268) 0)
:assumption (= (uf_142 uf_256) 0)
:assumption (= (uf_142 uf_252) 0)
:assumption (= (uf_142 uf_219) 0)
:assumption (= (uf_142 uf_267) 0)
:assumption (= (uf_142 uf_37) 0)
:assumption (= (uf_142 uf_240) 0)
:assumption (= (uf_142 uf_258) 0)
:assumption (= (uf_142 uf_257) 0)
:assumption (= (uf_142 uf_254) 0)
:assumption (= (uf_142 uf_255) 0)
:assumption (= (uf_142 uf_84) 0)
:assumption (= (uf_142 uf_4) 0)
:assumption (= (uf_142 uf_91) 0)
:assumption (= (uf_142 uf_7) 0)
:assumption (= (uf_142 uf_83) 0)
:assumption (= (uf_142 uf_87) 0)
:assumption (= (uf_142 uf_90) 0)
:assumption (= (uf_142 uf_94) 0)
:assumption (= (uf_139 uf_219) 1)
:assumption (= (uf_139 uf_252) 1)
:assumption (= (uf_139 uf_254) 8)
:assumption (= (uf_139 uf_255) 4)
:assumption (= (uf_139 uf_84) 8)
:assumption (= (uf_139 uf_4) 4)
:assumption (= (uf_139 uf_91) 2)
:assumption (= (uf_139 uf_7) 1)
:assumption (= (uf_139 uf_83) 8)
:assumption (= (uf_139 uf_87) 4)
:assumption (= (uf_139 uf_90) 2)
:assumption (= (uf_139 uf_94) 1)
:assumption (not (implies true (implies (and (<= 0 uf_269) (<= uf_269 uf_78)) (implies (and (<= 0 uf_270) (<= uf_270 uf_76)) (implies (and (<= 0 uf_271) (<= uf_271 uf_76)) (implies (< uf_272 1099511627776) (implies (< 0 uf_272) (implies (and (= (uf_27 uf_273 (uf_43 (uf_124 uf_7 uf_272) (uf_116 (uf_43 uf_7 uf_274)))) uf_9) (and (= (uf_25 uf_273 (uf_43 (uf_124 uf_7 uf_272) (uf_116 (uf_43 uf_7 uf_274)))) uf_26) (and (= (uf_48 (uf_43 (uf_124 uf_7 uf_272) (uf_116 (uf_43 uf_7 uf_274))) (uf_124 uf_7 uf_272)) uf_9) (and (= (uf_24 uf_273 (uf_43 (uf_124 uf_7 uf_272) (uf_116 (uf_43 uf_7 uf_274)))) uf_9) (and (not (= (uf_12 (uf_124 uf_7 uf_272)) uf_14)) (= (uf_23 (uf_124 uf_7 uf_272)) uf_9)))))) (implies true (implies (= (uf_203 uf_273) uf_9) (implies (and (= (uf_202 uf_275 uf_273) uf_9) (= (uf_55 uf_273) uf_9)) (implies (forall (?x771 T19) (< (uf_276 ?x771) uf_277) :pat { (uf_276 ?x771) }) (implies (and (up_278 uf_273 uf_275 uf_279 (uf_29 (uf_43 uf_7 uf_274)) (uf_6 uf_7)) (up_280 uf_273 uf_275 uf_279 (uf_43 uf_7 uf_274) (uf_6 uf_7))) (implies (up_278 uf_273 uf_275 uf_281 uf_272 uf_4) (implies (= uf_282 (uf_173 uf_273)) (implies (forall (?x772 T5) (iff (= (uf_283 uf_282 ?x772) uf_9) false) :pat { (uf_283 uf_282 ?x772) }) (implies (and (<= 0 uf_272) (<= uf_272 uf_76)) (and (= (uf_200 uf_273 (uf_43 (uf_124 uf_7 uf_272) (uf_116 (uf_43 uf_7 uf_274))) (uf_43 (uf_124 uf_7 uf_272) (uf_116 (uf_43 uf_7 uf_274))) uf_284) uf_9) (implies (= (uf_200 uf_273 (uf_43 (uf_124 uf_7 uf_272) (uf_116 (uf_43 uf_7 uf_274))) (uf_43 (uf_124 uf_7 uf_272) (uf_116 (uf_43 uf_7 uf_274))) uf_284) uf_9) (and (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7) uf_7) uf_9) (= (uf_24 uf_273 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7)) uf_9)) (implies (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7) uf_7) uf_9) (= (uf_24 uf_273 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7)) uf_9)) (and (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7) uf_7) uf_9) (= (uf_68 uf_273 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7)) uf_9)) (implies (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7) uf_7) uf_9) (= (uf_68 uf_273 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7)) uf_9)) (implies (= uf_285 (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7))) (implies (up_278 uf_273 uf_286 uf_287 uf_285 uf_7) (implies (up_278 uf_273 uf_288 uf_289 0 uf_4) (implies (up_278 uf_273 uf_290 uf_291 1 uf_4) (implies (and (<= 1 1) (and (<= 1 1) (and (<= 0 0) (<= 0 0)))) (and (<= 1 uf_272) (implies (<= 1 uf_272) (and (forall (?x773 Int) (implies (and (<= 0 ?x773) (<= ?x773 uf_76)) (implies (< ?x773 1) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x773 uf_7)) uf_285)))) (implies (forall (?x774 Int) (implies (and (<= 0 ?x774) (<= ?x774 uf_76)) (implies (< ?x774 1) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x774 uf_7)) uf_285)))) (and (and (< 0 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7)) uf_285)) (implies (and (< 0 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) 0 uf_7)) uf_285)) (implies true (implies (and (<= 0 uf_292) (<= uf_292 uf_78)) (implies (and (<= 0 uf_293) (<= uf_293 uf_76)) (implies (and (<= 0 uf_294) (<= uf_294 uf_76)) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (<= uf_294 uf_272) (implies (forall (?x775 Int) (implies (and (<= 0 ?x775) (<= ?x775 uf_76)) (implies (< ?x775 uf_294) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x775 uf_7)) uf_292)))) (implies (and (< uf_293 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_293 uf_7)) uf_292)) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (and (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (not true) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (and (= (uf_202 uf_295 uf_273) uf_9) (= (uf_55 uf_273) uf_9)) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (and up_216 (implies up_216 (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (= uf_296 uf_292) (implies (= uf_297 uf_294) (implies (= uf_298 uf_293) (implies (= uf_299 uf_292) (implies true (and (forall (?x776 Int) (implies (and (<= 0 ?x776) (<= ?x776 uf_76)) (implies (< ?x776 uf_272) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x776 uf_7)) uf_299)))) (implies (forall (?x777 Int) (implies (and (<= 0 ?x777) (<= ?x777 uf_76)) (implies (< ?x777 uf_272) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x777 uf_7)) uf_299)))) (and (exists (?x778 Int) (and (<= 0 ?x778) (and (<= ?x778 uf_76) (and (< ?x778 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x778 uf_7)) uf_299))))) (implies (exists (?x779 Int) (and (<= 0 ?x779) (and (<= ?x779 uf_76) (and (< ?x779 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x779 uf_7)) uf_299))))) true)))))))))))))))))))))))))) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (and (forall (?x780 T5) (implies (not (= (uf_12 (uf_13 (uf_25 uf_273 ?x780))) uf_261)) (not (= (uf_12 (uf_13 (uf_25 uf_273 ?x780))) uf_261))) :pat { (uf_40 (uf_41 uf_273) ?x780) }) (and (forall (?x781 T5) (implies (= (uf_68 uf_273 ?x781) uf_9) (and (= (uf_19 (uf_20 uf_273) ?x781) (uf_19 (uf_20 uf_273) ?x781)) (= (uf_68 uf_273 ?x781) uf_9))) :pat { (uf_19 (uf_20 uf_273) ?x781) }) (and (forall (?x782 T5) (implies (= (uf_68 uf_273 ?x782) uf_9) (and (= (uf_40 (uf_41 uf_273) ?x782) (uf_40 (uf_41 uf_273) ?x782)) (= (uf_68 uf_273 ?x782) uf_9))) :pat { (uf_40 (uf_41 uf_273) ?x782) }) (and (forall (?x783 T5) (implies (= (uf_68 uf_273 ?x783) uf_9) (and (= (uf_58 (uf_59 uf_273) ?x783) (uf_58 (uf_59 uf_273) ?x783)) (= (uf_68 uf_273 ?x783) uf_9))) :pat { (uf_58 (uf_59 uf_273) ?x783) }) (and (<= (uf_173 uf_273) (uf_173 uf_273)) (and (forall (?x784 T5) (<= (uf_172 uf_273 ?x784) (uf_172 uf_273 ?x784)) :pat { (uf_172 uf_273 ?x784) }) (= (uf_178 uf_273 uf_273) uf_9))))))) (implies (and (<= (uf_173 uf_273) (uf_173 uf_273)) (and (forall (?x785 T5) (<= (uf_172 uf_273 ?x785) (uf_172 uf_273 ?x785)) :pat { (uf_172 uf_273 ?x785) }) (= (uf_178 uf_273 uf_273) uf_9))) (implies (and (= (uf_202 uf_295 uf_273) uf_9) (= (uf_55 uf_273) uf_9)) (implies (up_278 uf_273 uf_295 uf_291 uf_294 uf_4) (implies (up_278 uf_273 uf_295 uf_289 uf_293 uf_4) (implies (up_278 uf_273 uf_295 uf_287 uf_292 uf_7) (implies (up_278 uf_273 uf_295 uf_281 uf_272 uf_4) (implies (and (up_278 uf_273 uf_295 uf_279 (uf_29 (uf_43 uf_7 uf_274)) (uf_6 uf_7)) (up_280 uf_273 uf_295 uf_279 (uf_43 uf_7 uf_274) (uf_6 uf_7))) (implies (and (= (uf_59 uf_273) (uf_59 uf_273)) (= (uf_41 uf_273) (uf_41 uf_273))) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (and (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (< uf_294 uf_272) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (and (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7) uf_7) uf_9) (= (uf_24 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_9)) (implies (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7) uf_7) uf_9) (= (uf_24 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_9)) (and (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7) uf_7) uf_9) (= (uf_68 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_9)) (implies (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7) uf_7) uf_9) (= (uf_68 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_9)) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (and (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (< uf_292 (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7))) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (and (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7) uf_7) uf_9) (= (uf_24 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_9)) (implies (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7) uf_7) uf_9) (= (uf_24 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_9)) (and (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7) uf_7) uf_9) (= (uf_68 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_9)) (implies (and (= (uf_48 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7) uf_7) uf_9) (= (uf_68 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_9)) (implies (= uf_300 (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7))) (implies (up_278 uf_273 uf_301 uf_287 uf_300 uf_7) (implies (up_278 uf_273 uf_302 uf_289 uf_294 uf_4) (implies (and (<= 1 uf_294) (<= 1 uf_294)) (implies true (implies (= uf_303 uf_300) (implies (= uf_304 uf_294) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_304)) (and (and (<= 0 (+ uf_294 1)) (<= (+ uf_294 1) uf_76)) (implies (and (<= 0 (+ uf_294 1)) (<= (+ uf_294 1) uf_76)) (implies (= uf_305 (+ uf_294 1)) (implies (up_278 uf_273 uf_306 uf_291 uf_305 uf_4) (implies (and (<= 2 uf_305) (<= 0 uf_304)) (implies true (and (<= uf_305 uf_272) (implies (<= uf_305 uf_272) (and (forall (?x786 Int) (implies (and (<= 0 ?x786) (<= ?x786 uf_76)) (implies (< ?x786 uf_305) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x786 uf_7)) uf_303)))) (implies (forall (?x787 Int) (implies (and (<= 0 ?x787) (<= ?x787 uf_76)) (implies (< ?x787 uf_305) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x787 uf_7)) uf_303)))) (and (and (< uf_304 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_304 uf_7)) uf_303)) (implies (and (< uf_304 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_304 uf_7)) uf_303)) (implies false true)))))))))))))))))))))))))))))))) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_294 uf_7)) uf_292) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (= uf_303 uf_292) (implies (= uf_304 uf_293) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_304)) (and (and (<= 0 (+ uf_294 1)) (<= (+ uf_294 1) uf_76)) (implies (and (<= 0 (+ uf_294 1)) (<= (+ uf_294 1) uf_76)) (implies (= uf_305 (+ uf_294 1)) (implies (up_278 uf_273 uf_306 uf_291 uf_305 uf_4) (implies (and (<= 2 uf_305) (<= 0 uf_304)) (implies true (and (<= uf_305 uf_272) (implies (<= uf_305 uf_272) (and (forall (?x788 Int) (implies (and (<= 0 ?x788) (<= ?x788 uf_76)) (implies (< ?x788 uf_305) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x788 uf_7)) uf_303)))) (implies (forall (?x789 Int) (implies (and (<= 0 ?x789) (<= ?x789 uf_76)) (implies (< ?x789 uf_305) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x789 uf_7)) uf_303)))) (and (and (< uf_304 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_304 uf_7)) uf_303)) (implies (and (< uf_304 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) uf_304 uf_7)) uf_303)) (implies false true))))))))))))))))))))))))))))))))))))) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (<= uf_272 uf_294) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (and up_216 (implies up_216 (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies (and (<= 1 uf_294) (<= 0 uf_293)) (implies true (implies (= uf_296 uf_292) (implies (= uf_297 uf_294) (implies (= uf_298 uf_293) (implies (= uf_299 uf_292) (implies true (and (forall (?x790 Int) (implies (and (<= 0 ?x790) (<= ?x790 uf_76)) (implies (< ?x790 uf_272) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x790 uf_7)) uf_299)))) (implies (forall (?x791 Int) (implies (and (<= 0 ?x791) (<= ?x791 uf_76)) (implies (< ?x791 uf_272) (<= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x791 uf_7)) uf_299)))) (and (exists (?x792 Int) (and (<= 0 ?x792) (and (<= ?x792 uf_76) (and (< ?x792 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x792 uf_7)) uf_299))))) (implies (exists (?x793 Int) (and (<= 0 ?x793) (and (<= ?x793 uf_76) (and (< ?x793 uf_272) (= (uf_110 uf_273 (uf_66 (uf_43 uf_7 uf_274) ?x793 uf_7)) uf_299))))) true))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
:formula true
)