LTS Termination Proof

by AProVE

Input

• Initial Location: f913_0__init__GE, f9340_0_possibleValues_GE, f8234_0_resolve_aux_GE, f9691_0_possibleValues_GE, __init, f9214_0_possibleValues_GE, f8739_0_possibleValues_GE, f10650_0_resolve_aux_GE, f1158_0__init__GE, f7719_0_resolve_aux_LE, f10649_0_resolve_aux_GE, f9214_0_possibleValues_GE', f1907_0_resolve_GE, f2103_0_resolve_GE, f8467_0_resolve_aux_GE, f1_0_main_Load, f8384_0_possibleValues_GE
• Transitions: (pre-variables and post-variables)

  f1_0_main_Load	1	f913_0__init__GE:		x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ _arg2 = _arg3P ∧ 0 = _arg2P ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg1 − 1 ∧ 1 ≤ _arg2 − 1 ∧ _arg1P ≤ _arg1
  f913_0__init__GE	2	f1158_0__init__GE:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x1 = _x6 ∧ x2 = _x7 ∧ x3 = _x8 ∧ x4 = _x9 ∧ x5 = _x10 ∧ x6 = _x11 ∧ _x2 = _x9 ∧ 0 = _x8 ∧ _x1 = _x7 ∧ 0 ≤ _x6 − 1 ∧ 0 ≤ _x − 1 ∧ _x1 ≤ 8 ∧ _x6 ≤ _x
  f1158_0__init__GE	3	f913_0__init__GE:		x1 = _x12 ∧ x2 = _x13 ∧ x3 = _x14 ∧ x4 = _x15 ∧ x5 = _x16 ∧ x6 = _x19 ∧ x1 = _x20 ∧ x2 = _x21 ∧ x3 = _x22 ∧ x4 = _x23 ∧ x5 = _x24 ∧ x6 = _x25 ∧ _x15 = _x22 ∧ _x13 + 1 = _x21 ∧ 0 ≤ _x20 − 1 ∧ 0 ≤ _x12 − 1 ∧ 8 ≤ _x14 − 1 ∧ _x20 ≤ _x12
  f1158_0__init__GE	4	f1158_0__init__GE:		x1 = _x26 ∧ x2 = _x27 ∧ x3 = _x28 ∧ x4 = _x29 ∧ x5 = _x30 ∧ x6 = _x31 ∧ x1 = _x32 ∧ x2 = _x33 ∧ x3 = _x34 ∧ x4 = _x35 ∧ x5 = _x36 ∧ x6 = _x37 ∧ _x27 ≤ 8 ∧ _x28 ≤ 8 ∧ −1 ≤ _x38 − 1 ∧ _x28 ≤ _x38 − 1 ∧ _x28 ≤ _x39 − 1 ∧ −1 ≤ _x39 − 1 ∧ _x32 ≤ _x26 ∧ 0 ≤ _x26 − 1 ∧ 0 ≤ _x32 − 1 ∧ _x27 = _x33 ∧ _x28 + 1 = _x34 ∧ _x29 = _x35
  f913_0__init__GE	5	f1907_0_resolve_GE:		x1 = _x40 ∧ x2 = _x41 ∧ x3 = _x42 ∧ x4 = _x43 ∧ x5 = _x46 ∧ x6 = _x47 ∧ x1 = _x48 ∧ x2 = _x49 ∧ x3 = _x50 ∧ x4 = _x51 ∧ x5 = _x53 ∧ x6 = _x54 ∧ _x42 = _x53 ∧ 0 = _x51 ∧ 0 = _x50 ∧ 0 = _x49 ∧ 0 ≤ _x48 − 1 ∧ 0 ≤ _x40 − 1 ∧ 8 ≤ _x41 − 1 ∧ _x48 ≤ _x40
  f1907_0_resolve_GE	6	f7719_0_resolve_aux_LE:		x1 = _x55 ∧ x2 = _x56 ∧ x3 = _x57 ∧ x4 = _x58 ∧ x5 = _x59 ∧ x6 = _x60 ∧ x1 = _x61 ∧ x2 = _x62 ∧ x3 = _x66 ∧ x4 = _x67 ∧ x5 = _x68 ∧ x6 = _x69 ∧ _x56 = _x61 ∧ _x57 = _x58 ∧ 0 ≤ _x55 − 1 ∧ 1 ≤ _x59 − 1 ∧ 8 ≤ _x57 − 1
  f1907_0_resolve_GE	7	f2103_0_resolve_GE:		x1 = _x70 ∧ x2 = _x71 ∧ x3 = _x74 ∧ x4 = _x75 ∧ x5 = _x76 ∧ x6 = _x77 ∧ x1 = _x78 ∧ x2 = _x79 ∧ x3 = _x80 ∧ x4 = _x81 ∧ x5 = _x82 ∧ x6 = _x83 ∧ _x76 = _x82 ∧ 0 = _x81 ∧ _x74 = _x80 ∧ _x71 = _x79 ∧ _x74 = _x75 ∧ 0 ≤ _x78 − 1 ∧ 0 ≤ _x70 − 1 ∧ _x74 ≤ 8 ∧ _x78 ≤ _x70
  f2103_0_resolve_GE	8	f1907_0_resolve_GE:		x1 = _x84 ∧ x2 = _x85 ∧ x3 = _x89 ∧ x4 = _x90 ∧ x5 = _x91 ∧ x6 = _x92 ∧ x1 = _x96 ∧ x2 = _x97 ∧ x3 = _x98 ∧ x4 = _x99 ∧ x5 = _x105 ∧ x6 = _x106 ∧ _x91 = _x105 ∧ _x89 + 1 = _x99 ∧ _x89 + 1 = _x98 ∧ _x85 = _x97 ∧ 0 ≤ _x96 − 1 ∧ 0 ≤ _x84 − 1 ∧ 8 ≤ _x90 − 1 ∧ _x96 ≤ _x84
  f2103_0_resolve_GE	9	f2103_0_resolve_GE:		x1 = _x107 ∧ x2 = _x108 ∧ x3 = _x114 ∧ x4 = _x115 ∧ x5 = _x116 ∧ x6 = _x117 ∧ x1 = _x118 ∧ x2 = _x119 ∧ x3 = _x122 ∧ x4 = _x123 ∧ x5 = _x124 ∧ x6 = _x125 ∧ _x114 ≤ 8 ∧ _x115 ≤ 8 ∧ −1 ≤ _x126 − 1 ∧ _x127 ≤ −1 ∧ _x115 ≤ _x126 − 1 ∧ _x118 ≤ _x107 ∧ 0 ≤ _x107 − 1 ∧ 0 ≤ _x118 − 1 ∧ _x108 = _x119 ∧ _x114 = _x122 ∧ _x115 + 1 = _x123 ∧ _x116 = _x124
  f2103_0_resolve_GE	10	f2103_0_resolve_GE:		x1 = _x128 ∧ x2 = _x129 ∧ x3 = _x130 ∧ x4 = _x133 ∧ x5 = _x134 ∧ x6 = _x135 ∧ x1 = _x142 ∧ x2 = _x143 ∧ x3 = _x144 ∧ x4 = _x145 ∧ x5 = _x146 ∧ x6 = _x147 ∧ _x130 ≤ 8 ∧ _x133 ≤ 8 ∧ −1 ≤ _x148 − 1 ∧ 0 ≤ _x149 − 1 ∧ _x133 ≤ _x148 − 1 ∧ _x142 ≤ _x128 ∧ 0 ≤ _x128 − 1 ∧ 0 ≤ _x142 − 1 ∧ _x129 = _x143 ∧ _x130 = _x144 ∧ _x133 + 1 = _x145 ∧ _x134 = _x146
  f2103_0_resolve_GE	11	f2103_0_resolve_GE:		x1 = _x150 ∧ x2 = _x153 ∧ x3 = _x154 ∧ x4 = _x155 ∧ x5 = _x162 ∧ x6 = _x163 ∧ x1 = _x164 ∧ x2 = _x165 ∧ x3 = _x166 ∧ x4 = _x167 ∧ x5 = _x168 ∧ x6 = _x169 ∧ _x154 ≤ 8 ∧ _x155 ≤ 8 ∧ _x155 ≤ _x170 − 1 ∧ −1 ≤ _x170 − 1 ∧ _x164 ≤ _x150 ∧ 0 ≤ _x150 − 1 ∧ 0 ≤ _x164 − 1 ∧ _x153 + 1 = _x165 ∧ _x154 = _x166 ∧ _x155 + 1 = _x167 ∧ _x162 = _x168
  f7719_0_resolve_aux_LE	12	f8234_0_resolve_aux_GE:		x1 = _x171 ∧ x2 = _x172 ∧ x3 = _x173 ∧ x4 = _x174 ∧ x5 = _x175 ∧ x6 = _x178 ∧ x1 = _x179 ∧ x2 = _x180 ∧ x3 = _x181 ∧ x4 = _x182 ∧ x5 = _x189 ∧ x6 = _x190 ∧ 0 = _x181 ∧ 0 = _x180 ∧ _x171 = _x179 ∧ 0 ≤ _x171 − 1
  f8234_0_resolve_aux_GE	13	f8467_0_resolve_aux_GE:		x1 = _x191 ∧ x2 = _x192 ∧ x3 = _x193 ∧ x4 = _x194 ∧ x5 = _x197 ∧ x6 = _x198 ∧ x1 = _x199 ∧ x2 = _x203 ∧ x3 = _x204 ∧ x4 = _x205 ∧ x5 = _x206 ∧ x6 = _x210 ∧ 0 = _x204 ∧ _x193 = _x203 ∧ _x191 = _x199 ∧ _x193 ≤ 8
  f8467_0_resolve_aux_GE	14	f8234_0_resolve_aux_GE:		x1 = _x211 ∧ x2 = _x212 ∧ x3 = _x213 ∧ x4 = _x217 ∧ x5 = _x218 ∧ x6 = _x219 ∧ x1 = _x220 ∧ x2 = _x226 ∧ x3 = _x227 ∧ x4 = _x228 ∧ x5 = _x229 ∧ x6 = _x235 ∧ _x212 + 1 = _x227 ∧ _x213 = _x226 ∧ _x211 = _x220 ∧ 8 ≤ _x213 − 1
  f8467_0_resolve_aux_GE	15	f8467_0_resolve_aux_GE:		x1 = _x236 ∧ x2 = _x237 ∧ x3 = _x244 ∧ x4 = _x245 ∧ x5 = _x246 ∧ x6 = _x249 ∧ x1 = _x250 ∧ x2 = _x251 ∧ x3 = _x252 ∧ x4 = _x259 ∧ x5 = _x260 ∧ x6 = _x261 ∧ −1 ≤ _x268 − 1 ∧ _x244 ≤ 8 ∧ _x237 ≤ _x268 − 1 ∧ −1 ≤ _x269 − 1 ∧ _x244 ≤ _x269 − 1 ∧ _x270 ≤ −1 ∧ _x236 = _x250 ∧ _x237 = _x251 ∧ _x244 + 1 = _x252
  f8467_0_resolve_aux_GE	16	f8467_0_resolve_aux_GE:		x1 = _x271 ∧ x2 = _x272 ∧ x3 = _x273 ∧ x4 = _x280 ∧ x5 = _x281 ∧ x6 = _x282 ∧ x1 = _x283 ∧ x2 = _x284 ∧ x3 = _x285 ∧ x4 = _x286 ∧ x5 = _x287 ∧ x6 = _x288 ∧ −1 ≤ _x289 − 1 ∧ _x273 ≤ 8 ∧ _x272 ≤ _x289 − 1 ∧ −1 ≤ _x290 − 1 ∧ _x273 ≤ _x290 − 1 ∧ 0 ≤ _x291 − 1 ∧ _x271 = _x283 ∧ _x272 = _x284 ∧ _x273 + 1 = _x285
  f8234_0_resolve_aux_GE	17	f10649_0_resolve_aux_GE:		x1 = _x292 ∧ x2 = _x293 ∧ x3 = _x294 ∧ x4 = _x295 ∧ x5 = _x296 ∧ x6 = _x297 ∧ x1 = _x298 ∧ x2 = _x299 ∧ x3 = _x300 ∧ x4 = _x301 ∧ x5 = _x302 ∧ x6 = _x303 ∧ 0 = _x301 ∧ _x293 = _x300 ∧ _x294 = _x299 ∧ _x292 = _x298 ∧ 8 ≤ _x294 − 1 ∧ 0 ≤ _x292 − 1
  f8467_0_resolve_aux_GE	18	f10650_0_resolve_aux_GE:		x1 = _x304 ∧ x2 = _x305 ∧ x3 = _x306 ∧ x4 = _x307 ∧ x5 = _x308 ∧ x6 = _x309 ∧ x1 = _x310 ∧ x2 = _x311 ∧ x3 = _x312 ∧ x4 = _x313 ∧ x5 = _x314 ∧ x6 = _x315 ∧ −1 ≤ _x316 − 1 ∧ _x306 ≤ 8 ∧ _x305 ≤ _x316 − 1 ∧ −1 ≤ _x317 − 1 ∧ _x306 ≤ _x317 − 1 ∧ 0 ≤ _x304 − 1 ∧ _x304 = _x310 ∧ _x305 = _x311 ∧ _x306 = _x312 ∧ 0 = _x313
  f10649_0_resolve_aux_GE	19	f10649_0_resolve_aux_GE:		x1 = _x318 ∧ x2 = _x319 ∧ x3 = _x320 ∧ x4 = _x321 ∧ x5 = _x322 ∧ x6 = _x323 ∧ x1 = _x324 ∧ x2 = _x325 ∧ x3 = _x326 ∧ x4 = _x327 ∧ x5 = _x328 ∧ x6 = _x329 ∧ _x321 + 1 = _x327 ∧ _x320 = _x326 ∧ _x319 = _x325 ∧ _x318 = _x324 ∧ _x321 ≤ 8
  f10650_0_resolve_aux_GE	20	f10650_0_resolve_aux_GE:		x1 = _x330 ∧ x2 = _x331 ∧ x3 = _x332 ∧ x4 = _x333 ∧ x5 = _x334 ∧ x6 = _x335 ∧ x1 = _x336 ∧ x2 = _x337 ∧ x3 = _x338 ∧ x4 = _x339 ∧ x5 = _x340 ∧ x6 = _x341 ∧ _x333 + 1 = _x339 ∧ _x332 = _x338 ∧ _x331 = _x337 ∧ _x330 = _x336 ∧ _x333 ≤ 8
  f10649_0_resolve_aux_GE	21	f7719_0_resolve_aux_LE:		x1 = _x342 ∧ x2 = _x343 ∧ x3 = _x344 ∧ x4 = _x345 ∧ x5 = _x346 ∧ x6 = _x347 ∧ x1 = _x348 ∧ x2 = _x349 ∧ x3 = _x350 ∧ x4 = _x351 ∧ x5 = _x352 ∧ x6 = _x353 ∧ _x354 ≤ −1 ∧ _x345 ≤ 8 ∧ −1 ≤ _x355 − 1 ∧ _x343 ≤ _x355 − 1 ∧ −1 ≤ _x345 − 1 ∧ −1 ≤ _x356 − 1 ∧ _x344 ≤ _x356 − 1 ∧ 1 ≤ _x343 − 1 ∧ _x342 − 1 ≤ _x342 − 1 ∧ 0 ≤ _x342 − 1 ∧ _x342 − 1 = _x348
  f10649_0_resolve_aux_GE	22	f7719_0_resolve_aux_LE:		x1 = _x357 ∧ x2 = _x358 ∧ x3 = _x359 ∧ x4 = _x360 ∧ x5 = _x361 ∧ x6 = _x362 ∧ x1 = _x363 ∧ x2 = _x364 ∧ x3 = _x365 ∧ x4 = _x366 ∧ x5 = _x367 ∧ x6 = _x368 ∧ 0 ≤ _x369 − 1 ∧ _x360 ≤ 8 ∧ −1 ≤ _x370 − 1 ∧ _x358 ≤ _x370 − 1 ∧ −1 ≤ _x360 − 1 ∧ −1 ≤ _x371 − 1 ∧ _x359 ≤ _x371 − 1 ∧ 1 ≤ _x358 − 1 ∧ _x357 − 1 ≤ _x357 − 1 ∧ 0 ≤ _x357 − 1 ∧ _x357 − 1 = _x363
  f10650_0_resolve_aux_GE	23	f7719_0_resolve_aux_LE:		x1 = _x372 ∧ x2 = _x373 ∧ x3 = _x374 ∧ x4 = _x375 ∧ x5 = _x376 ∧ x6 = _x377 ∧ x1 = _x378 ∧ x2 = _x379 ∧ x3 = _x380 ∧ x4 = _x381 ∧ x5 = _x382 ∧ x6 = _x383 ∧ _x384 ≤ −1 ∧ _x375 ≤ 8 ∧ −1 ≤ _x385 − 1 ∧ _x373 ≤ _x385 − 1 ∧ −1 ≤ _x375 − 1 ∧ −1 ≤ _x386 − 1 ∧ _x374 ≤ _x386 − 1 ∧ _x372 − 1 ≤ _x372 − 1 ∧ 0 ≤ _x372 − 1 ∧ _x372 − 1 = _x378
  f10650_0_resolve_aux_GE	24	f7719_0_resolve_aux_LE:		x1 = _x387 ∧ x2 = _x388 ∧ x3 = _x389 ∧ x4 = _x390 ∧ x5 = _x391 ∧ x6 = _x392 ∧ x1 = _x393 ∧ x2 = _x394 ∧ x3 = _x395 ∧ x4 = _x396 ∧ x5 = _x397 ∧ x6 = _x398 ∧ 0 ≤ _x399 − 1 ∧ _x390 ≤ 8 ∧ −1 ≤ _x400 − 1 ∧ _x388 ≤ _x400 − 1 ∧ −1 ≤ _x390 − 1 ∧ −1 ≤ _x401 − 1 ∧ _x389 ≤ _x401 − 1 ∧ _x387 − 1 ≤ _x387 − 1 ∧ 0 ≤ _x387 − 1 ∧ _x387 − 1 = _x393
  f10649_0_resolve_aux_GE	25	f10649_0_resolve_aux_GE:		x1 = _x402 ∧ x2 = _x403 ∧ x3 = _x404 ∧ x4 = _x405 ∧ x5 = _x406 ∧ x6 = _x407 ∧ x1 = _x408 ∧ x2 = _x409 ∧ x3 = _x410 ∧ x4 = _x411 ∧ x5 = _x412 ∧ x6 = _x413 ∧ _x414 ≤ −1 ∧ _x405 ≤ 8 ∧ −1 ≤ _x415 − 1 ∧ _x403 ≤ _x415 − 1 ∧ −1 ≤ _x405 − 1 ∧ −1 ≤ _x416 − 1 ∧ _x404 ≤ _x416 − 1 ∧ 1 ≤ _x403 − 1 ∧ 0 ≤ _x402 − 1 ∧ _x402 − 1 ≤ _x402 − 1 ∧ −1 ≤ _x417 − 1 ∧ _x403 ≤ _x417 − 1 ∧ −1 ≤ _x418 − 1 ∧ _x404 ≤ _x418 − 1 ∧ _x402 = _x408 ∧ _x403 = _x409 ∧ _x404 = _x410 ∧ _x405 + 1 = _x411
  f10649_0_resolve_aux_GE	26	f10649_0_resolve_aux_GE:		x1 = _x419 ∧ x2 = _x420 ∧ x3 = _x421 ∧ x4 = _x422 ∧ x5 = _x423 ∧ x6 = _x424 ∧ x1 = _x425 ∧ x2 = _x426 ∧ x3 = _x427 ∧ x4 = _x428 ∧ x5 = _x429 ∧ x6 = _x430 ∧ 0 ≤ _x431 − 1 ∧ _x422 ≤ 8 ∧ −1 ≤ _x432 − 1 ∧ _x420 ≤ _x432 − 1 ∧ −1 ≤ _x422 − 1 ∧ −1 ≤ _x433 − 1 ∧ _x421 ≤ _x433 − 1 ∧ 1 ≤ _x420 − 1 ∧ 0 ≤ _x419 − 1 ∧ _x419 − 1 ≤ _x419 − 1 ∧ −1 ≤ _x434 − 1 ∧ _x420 ≤ _x434 − 1 ∧ −1 ≤ _x435 − 1 ∧ _x421 ≤ _x435 − 1 ∧ _x419 = _x425 ∧ _x420 = _x426 ∧ _x421 = _x427 ∧ _x422 + 1 = _x428
  f10650_0_resolve_aux_GE	27	f10650_0_resolve_aux_GE:		x1 = _x436 ∧ x2 = _x437 ∧ x3 = _x438 ∧ x4 = _x439 ∧ x5 = _x440 ∧ x6 = _x441 ∧ x1 = _x442 ∧ x2 = _x443 ∧ x3 = _x444 ∧ x4 = _x445 ∧ x5 = _x446 ∧ x6 = _x447 ∧ _x448 ≤ −1 ∧ _x439 ≤ 8 ∧ −1 ≤ _x449 − 1 ∧ _x437 ≤ _x449 − 1 ∧ −1 ≤ _x439 − 1 ∧ −1 ≤ _x450 − 1 ∧ _x438 ≤ _x450 − 1 ∧ 0 ≤ _x436 − 1 ∧ _x436 − 1 ≤ _x436 − 1 ∧ −1 ≤ _x451 − 1 ∧ _x437 ≤ _x451 − 1 ∧ −1 ≤ _x452 − 1 ∧ _x438 ≤ _x452 − 1 ∧ _x436 = _x442 ∧ _x437 = _x443 ∧ _x438 = _x444 ∧ _x439 + 1 = _x445
  f10650_0_resolve_aux_GE	28	f10650_0_resolve_aux_GE:		x1 = _x453 ∧ x2 = _x454 ∧ x3 = _x455 ∧ x4 = _x456 ∧ x5 = _x457 ∧ x6 = _x458 ∧ x1 = _x459 ∧ x2 = _x460 ∧ x3 = _x461 ∧ x4 = _x462 ∧ x5 = _x463 ∧ x6 = _x464 ∧ 0 ≤ _x465 − 1 ∧ _x456 ≤ 8 ∧ −1 ≤ _x466 − 1 ∧ _x454 ≤ _x466 − 1 ∧ −1 ≤ _x456 − 1 ∧ −1 ≤ _x467 − 1 ∧ _x455 ≤ _x467 − 1 ∧ 0 ≤ _x453 − 1 ∧ _x453 − 1 ≤ _x453 − 1 ∧ −1 ≤ _x468 − 1 ∧ _x454 ≤ _x468 − 1 ∧ −1 ≤ _x469 − 1 ∧ _x455 ≤ _x469 − 1 ∧ _x453 = _x459 ∧ _x454 = _x460 ∧ _x455 = _x461 ∧ _x456 + 1 = _x462
  f8234_0_resolve_aux_GE	29	f8384_0_possibleValues_GE:		x1 = _x470 ∧ x2 = _x471 ∧ x3 = _x472 ∧ x4 = _x473 ∧ x5 = _x474 ∧ x6 = _x475 ∧ x1 = _x476 ∧ x2 = _x477 ∧ x3 = _x478 ∧ x4 = _x479 ∧ x5 = _x480 ∧ x6 = _x481 ∧ 0 = _x478 ∧ _x471 = _x477 ∧ _x472 = _x476 ∧ 8 ≤ _x472 − 1 ∧ 0 ≤ _x470 − 1
  f8467_0_resolve_aux_GE	30	f8384_0_possibleValues_GE:		x1 = _x482 ∧ x2 = _x483 ∧ x3 = _x484 ∧ x4 = _x485 ∧ x5 = _x486 ∧ x6 = _x487 ∧ x1 = _x488 ∧ x2 = _x489 ∧ x3 = _x490 ∧ x4 = _x491 ∧ x5 = _x492 ∧ x6 = _x493 ∧ −1 ≤ _x494 − 1 ∧ _x484 ≤ 8 ∧ _x483 ≤ _x494 − 1 ∧ −1 ≤ _x495 − 1 ∧ _x484 ≤ _x495 − 1 ∧ 0 ≤ _x482 − 1 ∧ _x483 = _x488 ∧ _x484 = _x489 ∧ 0 = _x490
  f8384_0_possibleValues_GE	31	f8384_0_possibleValues_GE:		x1 = _x496 ∧ x2 = _x497 ∧ x3 = _x498 ∧ x4 = _x499 ∧ x5 = _x500 ∧ x6 = _x501 ∧ x1 = _x502 ∧ x2 = _x503 ∧ x3 = _x504 ∧ x4 = _x505 ∧ x5 = _x506 ∧ x6 = _x507 ∧ _x498 + 1 = _x504 ∧ _x497 = _x503 ∧ _x496 = _x502 ∧ _x498 ≤ 8
  f8384_0_possibleValues_GE	32	f8739_0_possibleValues_GE:		x1 = _x508 ∧ x2 = _x509 ∧ x3 = _x510 ∧ x4 = _x511 ∧ x5 = _x512 ∧ x6 = _x513 ∧ x1 = _x514 ∧ x2 = _x515 ∧ x3 = _x516 ∧ x4 = _x517 ∧ x5 = _x518 ∧ x6 = _x519 ∧ 0 = _x516 ∧ _x509 = _x515 ∧ _x508 = _x514 ∧ 8 ≤ _x510 − 1
  f8739_0_possibleValues_GE	33	f8739_0_possibleValues_GE:		x1 = _x520 ∧ x2 = _x521 ∧ x3 = _x522 ∧ x4 = _x523 ∧ x5 = _x524 ∧ x6 = _x525 ∧ x1 = _x526 ∧ x2 = _x527 ∧ x3 = _x528 ∧ x4 = _x529 ∧ x5 = _x530 ∧ x6 = _x531 ∧ −1 ≤ _x532 − 1 ∧ _x522 ≤ 8 ∧ _x520 ≤ _x532 − 1 ∧ −1 ≤ _x533 − 1 ∧ _x522 ≤ _x533 − 1 ∧ _x520 = _x526 ∧ _x521 = _x527 ∧ _x522 + 1 = _x528
  f8739_0_possibleValues_GE	34	f8739_0_possibleValues_GE:		x1 = _x534 ∧ x2 = _x535 ∧ x3 = _x536 ∧ x4 = _x537 ∧ x5 = _x538 ∧ x6 = _x539 ∧ x1 = _x540 ∧ x2 = _x541 ∧ x3 = _x542 ∧ x4 = _x543 ∧ x5 = _x544 ∧ x6 = _x545 ∧ −1 ≤ _x546 − 1 ∧ _x536 ≤ 8 ∧ _x534 ≤ _x546 − 1 ∧ −1 ≤ _x547 − 1 ∧ _x536 ≤ _x547 − 1 ∧ _x548 ≤ −1 ∧ −1 ≤ _x549 − 1 ∧ _x534 ≤ _x549 − 1 ∧ −1 ≤ _x550 − 1 ∧ _x536 ≤ _x550 − 1 ∧ _x551 ≤ 9 ∧ _x534 = _x540 ∧ _x535 = _x541 ∧ _x536 + 1 = _x542
  f8739_0_possibleValues_GE	35	f8739_0_possibleValues_GE:		x1 = _x552 ∧ x2 = _x553 ∧ x3 = _x554 ∧ x4 = _x555 ∧ x5 = _x556 ∧ x6 = _x557 ∧ x1 = _x558 ∧ x2 = _x559 ∧ x3 = _x560 ∧ x4 = _x561 ∧ x5 = _x562 ∧ x6 = _x563 ∧ −1 ≤ _x564 − 1 ∧ _x554 ≤ 8 ∧ _x552 ≤ _x564 − 1 ∧ −1 ≤ _x565 − 1 ∧ _x554 ≤ _x565 − 1 ∧ 0 ≤ _x566 − 1 ∧ −1 ≤ _x567 − 1 ∧ _x552 ≤ _x567 − 1 ∧ −1 ≤ _x568 − 1 ∧ _x554 ≤ _x568 − 1 ∧ _x569 ≤ 9 ∧ _x552 = _x558 ∧ _x553 = _x559 ∧ _x554 + 1 = _x560
  f8739_0_possibleValues_GE	36	f9214_0_possibleValues_GE:		x1 = _x570 ∧ x2 = _x571 ∧ x3 = _x572 ∧ x4 = _x573 ∧ x5 = _x574 ∧ x6 = _x575 ∧ x1 = _x576 ∧ x2 = _x577 ∧ x3 = _x578 ∧ x4 = _x579 ∧ x5 = _x580 ∧ x6 = _x581 ∧ 0 = _x578 ∧ _x571 = _x577 ∧ _x570 = _x576 ∧ 8 ≤ _x572 − 1
  f9214_0_possibleValues_GE	37	f9214_0_possibleValues_GE':		x1 = _x582 ∧ x2 = _x583 ∧ x3 = _x584 ∧ x4 = _x585 ∧ x5 = _x586 ∧ x6 = _x587 ∧ x1 = _x588 ∧ x2 = _x589 ∧ x3 = _x590 ∧ x4 = _x591 ∧ x5 = _x592 ∧ x6 = _x593 ∧ 0 ≤ _x582 − 3⋅_x594 ∧ 8 ≤ _x584 − 1 ∧ −1 ≤ _x582 − 1 ∧ 0 ≤ _x583 − 3⋅_x595 ∧ −1 ≤ _x583 − 1 ∧ _x582 = _x588 ∧ _x583 = _x589 ∧ _x584 = _x590
  f9214_0_possibleValues_GE'	38	f9340_0_possibleValues_GE:		x1 = _x596 ∧ x2 = _x597 ∧ x3 = _x598 ∧ x4 = _x599 ∧ x5 = _x600 ∧ x6 = _x601 ∧ x1 = _x602 ∧ x2 = _x603 ∧ x3 = _x604 ∧ x4 = _x605 ∧ x5 = _x606 ∧ x6 = _x607 ∧ 0 ≤ _x596 − 3⋅_x608 ∧ 8 ≤ _x598 − 1 ∧ −1 ≤ _x596 − 1 ∧ −1 ≤ _x597 − 1 ∧ 0 ≤ _x597 − 3⋅_x609 ∧ _x596 − 3⋅_x608 ≤ 2 ∧ _x597 − 3⋅_x609 ≤ 2 ∧ 0 ≤ _x597 − 3⋅_x610 ∧ _x597 − 3⋅_x610 ≤ 2 ∧ 0 ≤ _x597 − 3⋅_x611 ∧ _x597 − 3⋅_x611 ≤ 2 ∧ 0 ≤ _x596 − 3⋅_x612 ∧ _x596 − 3⋅_x612 ≤ 2 ∧ _x596 − 3⋅_x613 ≤ 2 ∧ 0 ≤ _x596 − 3⋅_x613 ∧ _x597 − _x597 − 3⋅_x610 = _x602 ∧ _x597 − _x597 − 3⋅_x611 + 3 = _x603 ∧ _x596 − _x596 − 3⋅_x612 = _x604 ∧ _x596 − _x596 − 3⋅_x613 + 3 = _x605
  f9214_0_possibleValues_GE	39	f9214_0_possibleValues_GE:		x1 = _x614 ∧ x2 = _x615 ∧ x3 = _x616 ∧ x4 = _x617 ∧ x5 = _x618 ∧ x6 = _x619 ∧ x1 = _x620 ∧ x2 = _x621 ∧ x3 = _x622 ∧ x4 = _x623 ∧ x5 = _x624 ∧ x6 = _x625 ∧ −1 ≤ _x626 − 1 ∧ _x616 ≤ 8 ∧ _x616 ≤ _x626 − 1 ∧ −1 ≤ _x627 − 1 ∧ _x615 ≤ _x627 − 1 ∧ _x614 = _x620 ∧ _x615 = _x621 ∧ _x616 + 1 = _x622
  f9214_0_possibleValues_GE	40	f9214_0_possibleValues_GE:		x1 = _x628 ∧ x2 = _x629 ∧ x3 = _x630 ∧ x4 = _x631 ∧ x5 = _x632 ∧ x6 = _x633 ∧ x1 = _x634 ∧ x2 = _x635 ∧ x3 = _x636 ∧ x4 = _x637 ∧ x5 = _x638 ∧ x6 = _x639 ∧ −1 ≤ _x640 − 1 ∧ _x630 ≤ 8 ∧ _x630 ≤ _x640 − 1 ∧ −1 ≤ _x641 − 1 ∧ _x629 ≤ _x641 − 1 ∧ _x642 ≤ −1 ∧ −1 ≤ _x643 − 1 ∧ _x630 ≤ _x643 − 1 ∧ −1 ≤ _x644 − 1 ∧ _x629 ≤ _x644 − 1 ∧ _x645 ≤ 9 ∧ _x628 = _x634 ∧ _x629 = _x635 ∧ _x630 + 1 = _x636
  f9214_0_possibleValues_GE	41	f9214_0_possibleValues_GE:		x1 = _x646 ∧ x2 = _x647 ∧ x3 = _x648 ∧ x4 = _x649 ∧ x5 = _x650 ∧ x6 = _x651 ∧ x1 = _x652 ∧ x2 = _x653 ∧ x3 = _x654 ∧ x4 = _x655 ∧ x5 = _x656 ∧ x6 = _x657 ∧ −1 ≤ _x658 − 1 ∧ _x648 ≤ 8 ∧ _x648 ≤ _x658 − 1 ∧ −1 ≤ _x659 − 1 ∧ _x647 ≤ _x659 − 1 ∧ 0 ≤ _x660 − 1 ∧ −1 ≤ _x661 − 1 ∧ _x648 ≤ _x661 − 1 ∧ −1 ≤ _x662 − 1 ∧ _x647 ≤ _x662 − 1 ∧ _x663 ≤ 9 ∧ _x646 = _x652 ∧ _x647 = _x653 ∧ _x648 + 1 = _x654
  f9340_0_possibleValues_GE	42	f9691_0_possibleValues_GE:		x1 = _x664 ∧ x2 = _x665 ∧ x3 = _x666 ∧ x4 = _x667 ∧ x5 = _x668 ∧ x6 = _x669 ∧ x1 = _x670 ∧ x2 = _x671 ∧ x3 = _x672 ∧ x4 = _x673 ∧ x5 = _x674 ∧ x6 = _x675 ∧ _x665 = _x675 ∧ _x664 = _x674 ∧ _x664 = _x673 ∧ _x666 = _x672 ∧ _x667 = _x671 ∧ _x664 = _x670 ∧ _x666 ≤ _x667 − 1
  f9691_0_possibleValues_GE	43	f9340_0_possibleValues_GE:		x1 = _x676 ∧ x2 = _x677 ∧ x3 = _x678 ∧ x4 = _x679 ∧ x5 = _x680 ∧ x6 = _x681 ∧ x1 = _x682 ∧ x2 = _x683 ∧ x3 = _x684 ∧ x4 = _x685 ∧ x5 = _x686 ∧ x6 = _x687 ∧ _x677 = _x685 ∧ _x678 + 1 = _x684 ∧ _x681 = _x683 ∧ _x676 = _x682 ∧ _x679 = _x680 ∧ _x681 ≤ _x679
  f9691_0_possibleValues_GE	44	f9691_0_possibleValues_GE:		x1 = _x688 ∧ x2 = _x689 ∧ x3 = _x690 ∧ x4 = _x691 ∧ x5 = _x692 ∧ x6 = _x693 ∧ x1 = _x694 ∧ x2 = _x695 ∧ x3 = _x696 ∧ x4 = _x697 ∧ x5 = _x698 ∧ x6 = _x699 ∧ −1 ≤ _x700 − 1 ∧ _x691 ≤ _x693 − 1 ∧ _x690 ≤ _x700 − 1 ∧ −1 ≤ _x701 − 1 ∧ _x691 ≤ _x701 − 1 ∧ _x691 = _x692 ∧ _x688 = _x694 ∧ _x689 = _x695 ∧ _x690 = _x696 ∧ _x691 + 1 = _x697 ∧ _x691 + 1 = _x698 ∧ _x693 = _x699
  f9691_0_possibleValues_GE	45	f9691_0_possibleValues_GE:		x1 = _x702 ∧ x2 = _x703 ∧ x3 = _x704 ∧ x4 = _x705 ∧ x5 = _x706 ∧ x6 = _x707 ∧ x1 = _x708 ∧ x2 = _x709 ∧ x3 = _x710 ∧ x4 = _x711 ∧ x5 = _x712 ∧ x6 = _x713 ∧ −1 ≤ _x714 − 1 ∧ _x705 ≤ _x707 − 1 ∧ _x704 ≤ _x714 − 1 ∧ −1 ≤ _x715 − 1 ∧ _x705 ≤ _x715 − 1 ∧ _x716 ≤ −1 ∧ −1 ≤ _x717 − 1 ∧ _x704 ≤ _x717 − 1 ∧ −1 ≤ _x718 − 1 ∧ _x705 ≤ _x718 − 1 ∧ _x719 ≤ 9 ∧ _x705 = _x706 ∧ _x702 = _x708 ∧ _x703 = _x709 ∧ _x704 = _x710 ∧ _x705 + 1 = _x711 ∧ _x705 + 1 = _x712 ∧ _x707 = _x713
  f9691_0_possibleValues_GE	46	f9691_0_possibleValues_GE:		x1 = _x720 ∧ x2 = _x721 ∧ x3 = _x722 ∧ x4 = _x723 ∧ x5 = _x724 ∧ x6 = _x725 ∧ x1 = _x726 ∧ x2 = _x727 ∧ x3 = _x728 ∧ x4 = _x729 ∧ x5 = _x730 ∧ x6 = _x731 ∧ −1 ≤ _x732 − 1 ∧ _x723 ≤ _x725 − 1 ∧ _x722 ≤ _x732 − 1 ∧ −1 ≤ _x733 − 1 ∧ _x723 ≤ _x733 − 1 ∧ 0 ≤ _x734 − 1 ∧ −1 ≤ _x735 − 1 ∧ _x722 ≤ _x735 − 1 ∧ −1 ≤ _x736 − 1 ∧ _x723 ≤ _x736 − 1 ∧ _x737 ≤ 9 ∧ _x723 = _x724 ∧ _x720 = _x726 ∧ _x721 = _x727 ∧ _x722 = _x728 ∧ _x723 + 1 = _x729 ∧ _x723 + 1 = _x730 ∧ _x725 = _x731
  __init	47	f1_0_main_Load:		x1 = _x738 ∧ x2 = _x739 ∧ x3 = _x740 ∧ x4 = _x741 ∧ x5 = _x742 ∧ x6 = _x743 ∧ x1 = _x744 ∧ x2 = _x745 ∧ x3 = _x746 ∧ x4 = _x747 ∧ x5 = _x748 ∧ x6 = _x749 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

We consider subproblems for each of the 7 SCC(s) of the program graph.

2.1 SCC Subproblem 1/7

Here we consider the SCC { f913_0__init__GE, f1158_0__init__GE }.

2.1.1 Transition Removal

We remove transition 2 using the following ranking functions, which are bounded by −16.

2.1.2 Transition Removal

We remove transition 3 using the following ranking functions, which are bounded by 0.

2.1.3 Transition Removal

We remove transition 4 using the following ranking functions, which are bounded by −8.

2.1.4 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.2 SCC Subproblem 2/7

Here we consider the SCC { f1907_0_resolve_GE, f2103_0_resolve_GE }.

2.2.1 Transition Removal

We remove transition 7 using the following ranking functions, which are bounded by −14.

2.2.2 Transition Removal

We remove transition 8 using the following ranking functions, which are bounded by 0.

2.2.3 Transition Removal

We remove transitions 9, 10, 11 using the following ranking functions, which are bounded by 0.

2.2.4 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.3 SCC Subproblem 3/7

Here we consider the SCC { f10650_0_resolve_aux_GE, f7719_0_resolve_aux_LE, f10649_0_resolve_aux_GE, f8467_0_resolve_aux_GE, f8234_0_resolve_aux_GE }.

2.3.1 Transition Removal

We remove transition 12 using the following ranking functions, which are bounded by 0.

2.3.2 Transition Removal

We remove transitions 18, 17 using the following ranking functions, which are bounded by 0.

2.3.3 Transition Removal

We remove transition 13 using the following ranking functions, which are bounded by 0.

2.3.4 Transition Removal

We remove transitions 15, 16 using the following ranking functions, which are bounded by 0.

2.3.5 Transition Removal

We remove transition 14 using the following ranking functions, which are bounded by 0.

2.3.6 Transition Removal

We remove transitions 24, 23 using the following ranking functions, which are bounded by 0.

2.3.7 Transition Removal

We remove transitions 20, 27, 28 using the following ranking functions, which are bounded by 0.

2.3.8 Transition Removal

We remove transitions 22, 21 using the following ranking functions, which are bounded by 0.

2.3.9 Transition Removal

We remove transitions 19, 25, 26 using the following ranking functions, which are bounded by 0.

2.3.10 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.4 SCC Subproblem 4/7

Here we consider the SCC { f8384_0_possibleValues_GE }.

2.4.1 Transition Removal

We remove transition 31 using the following ranking functions, which are bounded by 0.

2.4.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.5 SCC Subproblem 5/7

Here we consider the SCC { f8739_0_possibleValues_GE }.

2.5.1 Transition Removal

We remove transitions 33, 34, 35 using the following ranking functions, which are bounded by −8.

2.5.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.6 SCC Subproblem 6/7

Here we consider the SCC { f9214_0_possibleValues_GE }.

2.6.1 Transition Removal

We remove transitions 39, 40, 41 using the following ranking functions, which are bounded by 0.

2.6.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.7 SCC Subproblem 7/7

Here we consider the SCC { f9340_0_possibleValues_GE, f9691_0_possibleValues_GE }.

2.7.1 Transition Removal

We remove transition 42 using the following ranking functions, which are bounded by 0.

2.7.2 Transition Removal

We remove transition 43 using the following ranking functions, which are bounded by 0.

2.7.3 Transition Removal

We remove transitions 44, 45, 46 using the following ranking functions, which are bounded by 0.

2.7.4 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

Tool configuration

AProVE

• version: AProVE Commit ID: unknown
• strategy: Statistics for single proof: 100.00 % (37 real / 0 unknown / 0 assumptions / 37 total proof steps)