YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l13, true>
<l1, l2, (undef1 = (0 + x0^0)) /\ (undef6 = (0 + x1^0)) /\ (undef7 = (0 + x2^0)) /\ (undef8 = (0 + x3^0)) /\ (undef9 = (0 + x4^0)) /\ (undef11 = (0 + x6^0)) /\ (undef12 = undef12), par{oldX0^0 -> undef1, oldX1^0 -> undef6, oldX2^0 -> undef7, oldX3^0 -> undef8, oldX4^0 -> undef9, oldX5^0 -> (0 + x5^0), oldX6^0 -> undef11, oldX7^0 -> undef12, x0^0 -> (0 + undef1), x1^0 -> (0 + undef6), x2^0 -> (0 + undef7), x3^0 -> (0 + undef8), x4^0 -> (0 + undef9), x5^0 -> (0 + undef11), x6^0 -> (0 + undef12)}>
<l3, l4, (undef22 = (0 + x0^0)) /\ (undef27 = (0 + x1^0)) /\ (undef28 = (0 + x2^0)) /\ (undef29 = (0 + x3^0)) /\ (undef30 = (0 + x4^0)) /\ (undef31 = (0 + x5^0)) /\ (undef33 = undef33) /\ (1 <= (0 + undef30)), par{oldX0^0 -> undef22, oldX1^0 -> undef27, oldX2^0 -> undef28, oldX3^0 -> undef29, oldX4^0 -> undef30, oldX5^0 -> undef31, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef33, x0^0 -> (0 + undef22), x1^0 -> (0 + undef27), x2^0 -> (0 + undef28), x3^0 -> (0 + undef29), x4^0 -> (0 + undef30), x5^0 -> (0 + undef31), x6^0 -> (0 + undef33)}>
<l3, l4, (undef43 = (0 + x0^0)) /\ (undef48 = (0 + x1^0)) /\ (undef49 = (0 + x2^0)) /\ (undef50 = (0 + x3^0)) /\ (undef51 = (0 + x4^0)) /\ (undef52 = (0 + x5^0)) /\ (undef54 = undef54) /\ ((1 + undef51) <= 0), par{oldX0^0 -> undef43, oldX1^0 -> undef48, oldX2^0 -> undef49, oldX3^0 -> undef50, oldX4^0 -> undef51, oldX5^0 -> undef52, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef54, x0^0 -> (0 + undef43), x1^0 -> (0 + undef48), x2^0 -> (0 + undef49), x3^0 -> (0 + undef50), x4^0 -> (0 + undef51), x5^0 -> (0 + undef52), x6^0 -> (0 + undef54)}>
<l3, l5, (undef64 = (0 + x0^0)) /\ (undef69 = (0 + x1^0)) /\ (undef70 = (0 + x2^0)) /\ (undef71 = (0 + x3^0)) /\ (undef72 = (0 + x4^0)) /\ (undef73 = (0 + x5^0)) /\ (undef75 = undef75) /\ ((0 + undef72) <= 0) /\ (0 <= (0 + undef72)), par{oldX0^0 -> undef64, oldX1^0 -> undef69, oldX2^0 -> undef70, oldX3^0 -> undef71, oldX4^0 -> undef72, oldX5^0 -> undef73, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef75, x0^0 -> (0 + undef64), x1^0 -> (0 + undef69), x2^0 -> (0 + undef70), x3^0 -> (0 + undef71), x4^0 -> (0 + undef72), x5^0 -> (0 + undef73), x6^0 -> (0 + undef75)}>
<l6, l1, (undef85 = (0 + x0^0)) /\ (undef90 = (0 + x1^0)) /\ (undef91 = (0 + x2^0)) /\ (undef92 = (0 + x3^0)) /\ (undef93 = (0 + x4^0)) /\ (undef94 = (0 + x5^0)) /\ (undef96 = undef96) /\ ((1 + undef96) <= (0 + undef92)) /\ ((1 + undef96) <= (0 + undef92)), par{oldX0^0 -> undef85, oldX1^0 -> undef90, oldX2^0 -> undef91, oldX3^0 -> undef92, oldX4^0 -> undef93, oldX5^0 -> undef94, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef96, x0^0 -> (0 + undef85), x1^0 -> (0 + undef90), x2^0 -> (0 + undef91), x3^0 -> (0 + undef92), x4^0 -> (0 + undef93), x5^0 -> (0 + undef94), x6^0 -> (1 + undef94)}>
<l6, l1, (undef106 = (0 + x0^0)) /\ (undef111 = (0 + x1^0)) /\ (undef112 = (0 + x2^0)) /\ (undef113 = (0 + x3^0)) /\ (undef114 = (0 + x4^0)) /\ (undef115 = (0 + x5^0)) /\ (undef117 = undef117) /\ ((1 + undef117) <= (0 + undef113)) /\ ((1 + undef113) <= (0 + undef117)), par{oldX0^0 -> undef106, oldX1^0 -> undef111, oldX2^0 -> undef112, oldX3^0 -> undef113, oldX4^0 -> undef114, oldX5^0 -> undef115, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef117, x0^0 -> (0 + undef106), x1^0 -> (0 + undef111), x2^0 -> (0 + undef112), x3^0 -> (0 + undef113), x4^0 -> (0 + undef114), x5^0 -> (0 + undef115), x6^0 -> (1 + undef115)}>
<l6, l1, (undef127 = (0 + x0^0)) /\ (undef132 = (0 + x1^0)) /\ (undef133 = (0 + x2^0)) /\ (undef134 = (0 + x3^0)) /\ (undef135 = (0 + x4^0)) /\ (undef136 = (0 + x5^0)) /\ (undef138 = undef138) /\ ((1 + undef134) <= (0 + undef138)) /\ ((1 + undef138) <= (0 + undef134)), par{oldX0^0 -> undef127, oldX1^0 -> undef132, oldX2^0 -> undef133, oldX3^0 -> undef134, oldX4^0 -> undef135, oldX5^0 -> undef136, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef138, x0^0 -> (0 + undef127), x1^0 -> (0 + undef132), x2^0 -> (0 + undef133), x3^0 -> (0 + undef134), x4^0 -> (0 + undef135), x5^0 -> (0 + undef136), x6^0 -> (1 + undef136)}>
<l6, l1, (undef148 = (0 + x0^0)) /\ (undef153 = (0 + x1^0)) /\ (undef154 = (0 + x2^0)) /\ (undef155 = (0 + x3^0)) /\ (undef156 = (0 + x4^0)) /\ (undef157 = (0 + x5^0)) /\ (undef159 = undef159) /\ ((1 + undef155) <= (0 + undef159)) /\ ((1 + undef155) <= (0 + undef159)), par{oldX0^0 -> undef148, oldX1^0 -> undef153, oldX2^0 -> undef154, oldX3^0 -> undef155, oldX4^0 -> undef156, oldX5^0 -> undef157, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef159, x0^0 -> (0 + undef148), x1^0 -> (0 + undef153), x2^0 -> (0 + undef154), x3^0 -> (0 + undef155), x4^0 -> (0 + undef156), x5^0 -> (0 + undef157), x6^0 -> (1 + undef157)}>
<l6, l2, (undef169 = (0 + x0^0)) /\ (undef174 = (0 + x1^0)) /\ (undef175 = (0 + x2^0)) /\ (undef176 = (0 + x3^0)) /\ (undef178 = (0 + x5^0)) /\ (undef180 = undef180) /\ (undef181 = undef181) /\ ((1 + undef181) <= (0 + undef176)) /\ ((0 + undef176) <= (0 + undef181)) /\ ((0 + undef181) <= (0 + undef176)), par{oldX0^0 -> undef169, oldX1^0 -> undef174, oldX2^0 -> undef175, oldX3^0 -> undef176, oldX4^0 -> (0 + x4^0), oldX5^0 -> undef178, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef180, oldX8^0 -> undef181, x0^0 -> (0 + undef169), x1^0 -> (0 + undef174), x2^0 -> (0 + undef175), x3^0 -> (0 + undef176), x4^0 -> 1, x5^0 -> (1 + undef178), x6^0 -> (0 + undef180)}>
<l6, l2, (undef190 = (0 + x0^0)) /\ (undef195 = (0 + x1^0)) /\ (undef196 = (0 + x2^0)) /\ (undef197 = (0 + x3^0)) /\ (undef199 = (0 + x5^0)) /\ (undef201 = undef201) /\ (undef202 = undef202) /\ ((1 + undef197) <= (0 + undef202)) /\ ((0 + undef197) <= (0 + undef202)) /\ ((0 + undef202) <= (0 + undef197)), par{oldX0^0 -> undef190, oldX1^0 -> undef195, oldX2^0 -> undef196, oldX3^0 -> undef197, oldX4^0 -> (0 + x4^0), oldX5^0 -> undef199, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef201, oldX8^0 -> undef202, x0^0 -> (0 + undef190), x1^0 -> (0 + undef195), x2^0 -> (0 + undef196), x3^0 -> (0 + undef197), x4^0 -> 1, x5^0 -> (1 + undef199), x6^0 -> (0 + undef201)}>
<l6, l1, (undef211 = (0 + x0^0)) /\ (undef216 = (0 + x1^0)) /\ (undef217 = (0 + x2^0)) /\ (undef218 = (0 + x3^0)) /\ (undef219 = (0 + x4^0)) /\ (undef220 = (0 + x5^0)) /\ (undef222 = undef222) /\ ((0 + undef218) <= (0 + undef222)) /\ ((0 + undef222) <= (0 + undef218)) /\ ((1 + undef222) <= (0 + undef218)), par{oldX0^0 -> undef211, oldX1^0 -> undef216, oldX2^0 -> undef217, oldX3^0 -> undef218, oldX4^0 -> undef219, oldX5^0 -> undef220, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef222, x0^0 -> (0 + undef211), x1^0 -> (0 + undef216), x2^0 -> (0 + undef217), x3^0 -> (0 + undef218), x4^0 -> (0 + undef219), x5^0 -> (0 + undef220), x6^0 -> (0 + undef220)}>
<l6, l1, (undef232 = (0 + x0^0)) /\ (undef237 = (0 + x1^0)) /\ (undef238 = (0 + x2^0)) /\ (undef239 = (0 + x3^0)) /\ (undef240 = (0 + x4^0)) /\ (undef241 = (0 + x5^0)) /\ (undef243 = undef243) /\ ((0 + undef239) <= (0 + undef243)) /\ ((0 + undef243) <= (0 + undef239)) /\ ((1 + undef239) <= (0 + undef243)), par{oldX0^0 -> undef232, oldX1^0 -> undef237, oldX2^0 -> undef238, oldX3^0 -> undef239, oldX4^0 -> undef240, oldX5^0 -> undef241, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef243, x0^0 -> (0 + undef232), x1^0 -> (0 + undef237), x2^0 -> (0 + undef238), x3^0 -> (0 + undef239), x4^0 -> (0 + undef240), x5^0 -> (0 + undef241), x6^0 -> (0 + undef241)}>
<l6, l2, (undef253 = (0 + x0^0)) /\ (undef258 = (0 + x1^0)) /\ (undef259 = (0 + x2^0)) /\ (undef260 = (0 + x3^0)) /\ (undef262 = (0 + x5^0)) /\ (undef264 = undef264) /\ (undef265 = undef265) /\ ((0 + undef260) <= (0 + undef265)) /\ ((0 + undef265) <= (0 + undef260)) /\ ((0 + undef260) <= (0 + undef265)) /\ ((0 + undef265) <= (0 + undef260)), par{oldX0^0 -> undef253, oldX1^0 -> undef258, oldX2^0 -> undef259, oldX3^0 -> undef260, oldX4^0 -> (0 + x4^0), oldX5^0 -> undef262, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef264, oldX8^0 -> undef265, x0^0 -> (0 + undef253), x1^0 -> (0 + undef258), x2^0 -> (0 + undef259), x3^0 -> (0 + undef260), x4^0 -> 1, x5^0 -> (0 + undef262), x6^0 -> (0 + undef264)}>
<l2, l3, (undef274 = (0 + x0^0)) /\ (undef279 = (0 + x1^0)) /\ (undef280 = (0 + x2^0)) /\ (undef281 = (0 + x3^0)) /\ (undef282 = (0 + x4^0)) /\ (undef283 = (0 + x5^0)) /\ (undef285 = undef285) /\ (1 <= (0 + undef282)), par{oldX0^0 -> undef274, oldX1^0 -> undef279, oldX2^0 -> undef280, oldX3^0 -> undef281, oldX4^0 -> undef282, oldX5^0 -> undef283, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef285, x0^0 -> (0 + undef274), x1^0 -> (0 + undef279), x2^0 -> (0 + undef280), x3^0 -> (0 + undef281), x4^0 -> (0 + undef282), x5^0 -> (0 + undef283), x6^0 -> (0 + undef285)}>
<l2, l3, (undef295 = (0 + x0^0)) /\ (undef300 = (0 + x1^0)) /\ (undef301 = (0 + x2^0)) /\ (undef302 = (0 + x3^0)) /\ (undef303 = (0 + x4^0)) /\ (undef304 = (0 + x5^0)) /\ (undef306 = undef306) /\ ((1 + undef303) <= 0), par{oldX0^0 -> undef295, oldX1^0 -> undef300, oldX2^0 -> undef301, oldX3^0 -> undef302, oldX4^0 -> undef303, oldX5^0 -> undef304, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef306, x0^0 -> (0 + undef295), x1^0 -> (0 + undef300), x2^0 -> (0 + undef301), x3^0 -> (0 + undef302), x4^0 -> (0 + undef303), x5^0 -> (0 + undef304), x6^0 -> (0 + undef306)}>
<l2, l3, (undef316 = (0 + x0^0)) /\ (undef321 = (0 + x1^0)) /\ (undef322 = (0 + x2^0)) /\ (undef323 = (0 + x3^0)) /\ (undef324 = (0 + x4^0)) /\ (undef325 = (0 + x5^0)) /\ (undef327 = undef327) /\ ((0 + undef321) <= (0 + undef325)), par{oldX0^0 -> undef316, oldX1^0 -> undef321, oldX2^0 -> undef322, oldX3^0 -> undef323, oldX4^0 -> undef324, oldX5^0 -> undef325, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef327, x0^0 -> (0 + undef316), x1^0 -> (0 + undef321), x2^0 -> (0 + undef322), x3^0 -> (0 + undef323), x4^0 -> (0 + undef324), x5^0 -> (0 + undef325), x6^0 -> (0 + undef327)}>
<l2, l6, (undef337 = (0 + x0^0)) /\ (undef342 = (0 + x1^0)) /\ (undef343 = (0 + x2^0)) /\ (undef344 = (0 + x3^0)) /\ (undef345 = (0 + x4^0)) /\ (undef346 = (0 + x5^0)) /\ (undef348 = undef348) /\ ((1 + undef346) <= (0 + undef342)) /\ ((0 + undef345) <= 0) /\ (0 <= (0 + undef345)), par{oldX0^0 -> undef337, oldX1^0 -> undef342, oldX2^0 -> undef343, oldX3^0 -> undef344, oldX4^0 -> undef345, oldX5^0 -> undef346, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef348, x0^0 -> (0 + undef337), x1^0 -> (0 + undef342), x2^0 -> (0 + undef343), x3^0 -> (0 + undef344), x4^0 -> (0 + undef345), x5^0 -> (0 + undef346), x6^0 -> (0 + undef348)}>
<l7, l8, (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef359, oldX11^0 -> undef360, oldX12^0 -> undef361, oldX13^0 -> undef362, oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef369, oldX8^0 -> undef370, oldX9^0 -> undef371, x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l9, l2, (undef379 = (0 + x0^0)) /\ (undef384 = (0 + x1^0)) /\ (undef385 = (0 + x2^0)) /\ (undef390 = undef390) /\ (undef391 = undef391), par{oldX0^0 -> undef379, oldX1^0 -> undef384, oldX2^0 -> undef385, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef390, oldX8^0 -> undef391, x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l10, l7, (undef400 = (0 + x0^0)) /\ (undef405 = (0 + x1^0)) /\ (undef406 = (0 + x2^0)) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)), par{oldX0^0 -> undef400, oldX10^0 -> undef401, oldX1^0 -> undef405, oldX2^0 -> undef406, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef411, oldX8^0 -> undef412, oldX9^0 -> undef413, x0^0 -> (0 + undef400), x1^0 -> (0 + undef405), x2^0 -> (0 + undef406), x3^0 -> (0 + undef411), x4^0 -> (0 + undef412), x5^0 -> (0 + undef413), x6^0 -> (0 + undef401)}>
<l10, l9, (undef421 = (0 + x0^0)) /\ (undef426 = (0 + x1^0)) /\ (undef427 = (0 + x2^0)) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)), par{oldX0^0 -> undef421, oldX10^0 -> undef422, oldX1^0 -> undef426, oldX2^0 -> undef427, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef432, oldX8^0 -> undef433, oldX9^0 -> undef434, x0^0 -> (0 + undef421), x1^0 -> (0 + undef426), x2^0 -> (0 + undef427), x3^0 -> (0 + undef432), x4^0 -> (0 + undef433), x5^0 -> (0 + undef434), x6^0 -> (0 + undef422)}>
<l11, l10, (undef442 = (0 + x0^0)) /\ (undef447 = (0 + x1^0)) /\ (undef453 = undef453) /\ (undef454 = undef454) /\ (undef455 = undef455) /\ (undef443 = undef443), par{oldX0^0 -> undef442, oldX10^0 -> undef443, oldX1^0 -> undef447, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef453, oldX8^0 -> undef454, oldX9^0 -> undef455, x0^0 -> (0 + undef442), x1^0 -> (0 + undef447), x2^0 -> 0, x3^0 -> (0 + undef453), x4^0 -> (0 + undef454), x5^0 -> (0 + undef455), x6^0 -> (0 + undef443)}>
<l4, l10, (undef463 = (0 + x0^0)) /\ (undef468 = (0 + x1^0)) /\ (undef469 = (0 + x2^0)) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464), par{oldX0^0 -> undef463, oldX10^0 -> undef464, oldX1^0 -> undef468, oldX2^0 -> undef469, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef474, oldX8^0 -> undef475, oldX9^0 -> undef476, x0^0 -> (0 + undef463), x1^0 -> (0 + undef468), x2^0 -> (1 + undef469), x3^0 -> (0 + undef474), x4^0 -> (0 + undef475), x5^0 -> (0 + undef476), x6^0 -> (0 + undef464)}>
<l5, l4, (undef484 = (0 + x0^0)) /\ (undef489 = (0 + x1^0)) /\ (undef490 = (0 + x2^0)) /\ (undef491 = (0 + x3^0)) /\ (undef492 = (0 + x4^0)) /\ (undef493 = (0 + x5^0)) /\ (undef495 = undef495), par{oldX0^0 -> undef484, oldX1^0 -> undef489, oldX2^0 -> undef490, oldX3^0 -> undef491, oldX4^0 -> undef492, oldX5^0 -> undef493, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef495, x0^0 -> (0 + undef484), x1^0 -> (0 + undef489), x2^0 -> (0 + undef490), x3^0 -> (0 + undef491), x4^0 -> (0 + undef492), x5^0 -> (0 + undef493), x6^0 -> (0 + undef495)}>
<l12, l11, (undef505 = (0 + x0^0)) /\ (undef510 = (0 + x1^0)) /\ (undef516 = undef516) /\ (undef517 = undef517) /\ (undef518 = undef518) /\ (undef506 = undef506) /\ (undef507 = undef507), par{oldX0^0 -> undef505, oldX10^0 -> undef506, oldX11^0 -> undef507, oldX1^0 -> undef510, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef516, oldX8^0 -> undef517, oldX9^0 -> undef518, x0^0 -> (0 + undef505), x1^0 -> (0 + undef510), x2^0 -> (0 + undef516), x3^0 -> (0 + undef517), x4^0 -> (0 + undef518), x5^0 -> (0 + undef506), x6^0 -> (0 + undef507)}>
<l12, l1, true>
<l12, l3, true>
<l12, l6, true>
<l12, l2, true>
<l12, l7, true>
<l12, l9, true>
<l12, l10, true>
<l12, l11, true>
<l12, l8, true>
<l12, l4, true>
<l12, l5, true>
<l13, l12, true>

Fresh variables:
undef1, undef6, undef7, undef8, undef9, undef11, undef12, undef22, undef27, undef28, undef29, undef30, undef31, undef33, undef43, undef48, undef49, undef50, undef51, undef52, undef54, undef64, undef69, undef70, undef71, undef72, undef73, undef75, undef85, undef90, undef91, undef92, undef93, undef94, undef96, undef106, undef111, undef112, undef113, undef114, undef115, undef117, undef127, undef132, undef133, undef134, undef135, undef136, undef138, undef148, undef153, undef154, undef155, undef156, undef157, undef159, undef169, undef174, undef175, undef176, undef178, undef180, undef181, undef190, undef195, undef196, undef197, undef199, undef201, undef202, undef211, undef216, undef217, undef218, undef219, undef220, undef222, undef232, undef237, undef238, undef239, undef240, undef241, undef243, undef253, undef258, undef259, undef260, undef262, undef264, undef265, undef274, undef279, undef280, undef281, undef282, undef283, undef285, undef295, undef300, undef301, undef302, undef303, undef304, undef306, undef316, undef321, undef322, undef323, undef324, undef325, undef327, undef337, undef342, undef343, undef344, undef345, undef346, undef348, undef359, undef360, undef361, undef362, undef369, undef370, undef371, undef379, undef384, undef385, undef390, undef391, undef400, undef401, undef405, undef406, undef411, undef412, undef413, undef421, undef422, undef426, undef427, undef432, undef433, undef434, undef442, undef443, undef447, undef453, undef454, undef455, undef463, undef464, undef468, undef469, undef474, undef475, undef476, undef484, undef489, undef490, undef491, undef492, undef493, undef495, undef505, undef506, undef507, undef510, undef516, undef517, undef518, 

Undef variables:
undef1, undef6, undef7, undef8, undef9, undef11, undef12, undef22, undef27, undef28, undef29, undef30, undef31, undef33, undef43, undef48, undef49, undef50, undef51, undef52, undef54, undef64, undef69, undef70, undef71, undef72, undef73, undef75, undef85, undef90, undef91, undef92, undef93, undef94, undef96, undef106, undef111, undef112, undef113, undef114, undef115, undef117, undef127, undef132, undef133, undef134, undef135, undef136, undef138, undef148, undef153, undef154, undef155, undef156, undef157, undef159, undef169, undef174, undef175, undef176, undef178, undef180, undef181, undef190, undef195, undef196, undef197, undef199, undef201, undef202, undef211, undef216, undef217, undef218, undef219, undef220, undef222, undef232, undef237, undef238, undef239, undef240, undef241, undef243, undef253, undef258, undef259, undef260, undef262, undef264, undef265, undef274, undef279, undef280, undef281, undef282, undef283, undef285, undef295, undef300, undef301, undef302, undef303, undef304, undef306, undef316, undef321, undef322, undef323, undef324, undef325, undef327, undef337, undef342, undef343, undef344, undef345, undef346, undef348, undef359, undef360, undef361, undef362, undef369, undef370, undef371, undef379, undef384, undef385, undef390, undef391, undef400, undef401, undef405, undef406, undef411, undef412, undef413, undef421, undef422, undef426, undef427, undef432, undef433, undef434, undef442, undef443, undef447, undef453, undef454, undef455, undef463, undef464, undef468, undef469, undef474, undef475, undef476, undef484, undef489, undef490, undef491, undef492, undef493, undef495, undef505, undef506, undef507, undef510, undef516, undef517, undef518, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l8, (undef505 = (0 + x0^0)) /\ (undef510 = (0 + x1^0)) /\ (undef516 = undef516) /\ (undef517 = undef517) /\ (undef518 = undef518) /\ (undef506 = undef506) /\ (undef507 = undef507) /\ (undef442 = (0 + (0 + undef505))) /\ (undef447 = (0 + (0 + undef510))) /\ (undef453 = undef453) /\ (undef454 = undef454) /\ (undef455 = undef455) /\ (undef443 = undef443) /\ (undef400 = (0 + (0 + undef442))) /\ (undef405 = (0 + (0 + undef447))) /\ (undef406 = (0 + 0)) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef505 = (0 + x0^0)) /\ (undef510 = (0 + x1^0)) /\ (undef516 = undef516) /\ (undef517 = undef517) /\ (undef518 = undef518) /\ (undef506 = undef506) /\ (undef507 = undef507) /\ (undef442 = (0 + (0 + undef505))) /\ (undef447 = (0 + (0 + undef510))) /\ (undef453 = undef453) /\ (undef454 = undef454) /\ (undef455 = undef455) /\ (undef443 = undef443) /\ (undef421 = (0 + (0 + undef442))) /\ (undef426 = (0 + (0 + undef447))) /\ (undef427 = (0 + 0)) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l0, l2, (undef1 = (0 + x0^0)) /\ (undef6 = (0 + x1^0)) /\ (undef7 = (0 + x2^0)) /\ (undef8 = (0 + x3^0)) /\ (undef9 = (0 + x4^0)) /\ (undef11 = (0 + x6^0)) /\ (undef12 = undef12), par{x0^0 -> (0 + undef1), x1^0 -> (0 + undef6), x2^0 -> (0 + undef7), x3^0 -> (0 + undef8), x4^0 -> (0 + undef9), x5^0 -> (0 + undef11), x6^0 -> (0 + undef12)}>
<l0, l8, (undef22 = (0 + x0^0)) /\ (undef27 = (0 + x1^0)) /\ (undef28 = (0 + x2^0)) /\ (undef29 = (0 + x3^0)) /\ (undef30 = (0 + x4^0)) /\ (undef31 = (0 + x5^0)) /\ (undef33 = undef33) /\ (1 <= (0 + undef30)) /\ (undef463 = (0 + (0 + undef22))) /\ (undef468 = (0 + (0 + undef27))) /\ (undef469 = (0 + (0 + undef28))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef22 = (0 + x0^0)) /\ (undef27 = (0 + x1^0)) /\ (undef28 = (0 + x2^0)) /\ (undef29 = (0 + x3^0)) /\ (undef30 = (0 + x4^0)) /\ (undef31 = (0 + x5^0)) /\ (undef33 = undef33) /\ (1 <= (0 + undef30)) /\ (undef463 = (0 + (0 + undef22))) /\ (undef468 = (0 + (0 + undef27))) /\ (undef469 = (0 + (0 + undef28))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l0, l8, (undef43 = (0 + x0^0)) /\ (undef48 = (0 + x1^0)) /\ (undef49 = (0 + x2^0)) /\ (undef50 = (0 + x3^0)) /\ (undef51 = (0 + x4^0)) /\ (undef52 = (0 + x5^0)) /\ (undef54 = undef54) /\ ((1 + undef51) <= 0) /\ (undef463 = (0 + (0 + undef43))) /\ (undef468 = (0 + (0 + undef48))) /\ (undef469 = (0 + (0 + undef49))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef43 = (0 + x0^0)) /\ (undef48 = (0 + x1^0)) /\ (undef49 = (0 + x2^0)) /\ (undef50 = (0 + x3^0)) /\ (undef51 = (0 + x4^0)) /\ (undef52 = (0 + x5^0)) /\ (undef54 = undef54) /\ ((1 + undef51) <= 0) /\ (undef463 = (0 + (0 + undef43))) /\ (undef468 = (0 + (0 + undef48))) /\ (undef469 = (0 + (0 + undef49))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l0, l8, (undef64 = (0 + x0^0)) /\ (undef69 = (0 + x1^0)) /\ (undef70 = (0 + x2^0)) /\ (undef71 = (0 + x3^0)) /\ (undef72 = (0 + x4^0)) /\ (undef73 = (0 + x5^0)) /\ (undef75 = undef75) /\ ((0 + undef72) <= 0) /\ (0 <= (0 + undef72)) /\ (undef484 = (0 + (0 + undef64))) /\ (undef489 = (0 + (0 + undef69))) /\ (undef490 = (0 + (0 + undef70))) /\ (undef491 = (0 + (0 + undef71))) /\ (undef492 = (0 + (0 + undef72))) /\ (undef493 = (0 + (0 + undef73))) /\ (undef495 = undef495) /\ (undef463 = (0 + (0 + undef484))) /\ (undef468 = (0 + (0 + undef489))) /\ (undef469 = (0 + (0 + undef490))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef64 = (0 + x0^0)) /\ (undef69 = (0 + x1^0)) /\ (undef70 = (0 + x2^0)) /\ (undef71 = (0 + x3^0)) /\ (undef72 = (0 + x4^0)) /\ (undef73 = (0 + x5^0)) /\ (undef75 = undef75) /\ ((0 + undef72) <= 0) /\ (0 <= (0 + undef72)) /\ (undef484 = (0 + (0 + undef64))) /\ (undef489 = (0 + (0 + undef69))) /\ (undef490 = (0 + (0 + undef70))) /\ (undef491 = (0 + (0 + undef71))) /\ (undef492 = (0 + (0 + undef72))) /\ (undef493 = (0 + (0 + undef73))) /\ (undef495 = undef495) /\ (undef463 = (0 + (0 + undef484))) /\ (undef468 = (0 + (0 + undef489))) /\ (undef469 = (0 + (0 + undef490))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l0, l6, true>
<l0, l2, true>
<l0, l8, (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef379 = (0 + x0^0)) /\ (undef384 = (0 + x1^0)) /\ (undef385 = (0 + x2^0)) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l0, l8, (undef400 = (0 + x0^0)) /\ (undef405 = (0 + x1^0)) /\ (undef406 = (0 + x2^0)) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef421 = (0 + x0^0)) /\ (undef426 = (0 + x1^0)) /\ (undef427 = (0 + x2^0)) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l0, l8, (undef442 = (0 + x0^0)) /\ (undef447 = (0 + x1^0)) /\ (undef453 = undef453) /\ (undef454 = undef454) /\ (undef455 = undef455) /\ (undef443 = undef443) /\ (undef400 = (0 + (0 + undef442))) /\ (undef405 = (0 + (0 + undef447))) /\ (undef406 = (0 + 0)) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef442 = (0 + x0^0)) /\ (undef447 = (0 + x1^0)) /\ (undef453 = undef453) /\ (undef454 = undef454) /\ (undef455 = undef455) /\ (undef443 = undef443) /\ (undef421 = (0 + (0 + undef442))) /\ (undef426 = (0 + (0 + undef447))) /\ (undef427 = (0 + 0)) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l0, l8, true>
<l0, l8, (undef463 = (0 + x0^0)) /\ (undef468 = (0 + x1^0)) /\ (undef469 = (0 + x2^0)) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef463 = (0 + x0^0)) /\ (undef468 = (0 + x1^0)) /\ (undef469 = (0 + x2^0)) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l0, l8, (undef484 = (0 + x0^0)) /\ (undef489 = (0 + x1^0)) /\ (undef490 = (0 + x2^0)) /\ (undef491 = (0 + x3^0)) /\ (undef492 = (0 + x4^0)) /\ (undef493 = (0 + x5^0)) /\ (undef495 = undef495) /\ (undef463 = (0 + (0 + undef484))) /\ (undef468 = (0 + (0 + undef489))) /\ (undef469 = (0 + (0 + undef490))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l0, l2, (undef484 = (0 + x0^0)) /\ (undef489 = (0 + x1^0)) /\ (undef490 = (0 + x2^0)) /\ (undef491 = (0 + x3^0)) /\ (undef492 = (0 + x4^0)) /\ (undef493 = (0 + x5^0)) /\ (undef495 = undef495) /\ (undef463 = (0 + (0 + undef484))) /\ (undef468 = (0 + (0 + undef489))) /\ (undef469 = (0 + (0 + undef490))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l2, l8, (undef274 = (0 + x0^0)) /\ (undef279 = (0 + x1^0)) /\ (undef280 = (0 + x2^0)) /\ (undef281 = (0 + x3^0)) /\ (undef282 = (0 + x4^0)) /\ (undef283 = (0 + x5^0)) /\ (undef285 = undef285) /\ (1 <= (0 + undef282)) /\ (undef22 = (0 + (0 + undef274))) /\ (undef27 = (0 + (0 + undef279))) /\ (undef28 = (0 + (0 + undef280))) /\ (undef29 = (0 + (0 + undef281))) /\ (undef30 = (0 + (0 + undef282))) /\ (undef31 = (0 + (0 + undef283))) /\ (undef33 = undef33) /\ (1 <= (0 + undef30)) /\ (undef463 = (0 + (0 + undef22))) /\ (undef468 = (0 + (0 + undef27))) /\ (undef469 = (0 + (0 + undef28))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l2, l2, (undef274 = (0 + x0^0)) /\ (undef279 = (0 + x1^0)) /\ (undef280 = (0 + x2^0)) /\ (undef281 = (0 + x3^0)) /\ (undef282 = (0 + x4^0)) /\ (undef283 = (0 + x5^0)) /\ (undef285 = undef285) /\ (1 <= (0 + undef282)) /\ (undef22 = (0 + (0 + undef274))) /\ (undef27 = (0 + (0 + undef279))) /\ (undef28 = (0 + (0 + undef280))) /\ (undef29 = (0 + (0 + undef281))) /\ (undef30 = (0 + (0 + undef282))) /\ (undef31 = (0 + (0 + undef283))) /\ (undef33 = undef33) /\ (1 <= (0 + undef30)) /\ (undef463 = (0 + (0 + undef22))) /\ (undef468 = (0 + (0 + undef27))) /\ (undef469 = (0 + (0 + undef28))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l2, l8, (undef295 = (0 + x0^0)) /\ (undef300 = (0 + x1^0)) /\ (undef301 = (0 + x2^0)) /\ (undef302 = (0 + x3^0)) /\ (undef303 = (0 + x4^0)) /\ (undef304 = (0 + x5^0)) /\ (undef306 = undef306) /\ ((1 + undef303) <= 0) /\ (undef43 = (0 + (0 + undef295))) /\ (undef48 = (0 + (0 + undef300))) /\ (undef49 = (0 + (0 + undef301))) /\ (undef50 = (0 + (0 + undef302))) /\ (undef51 = (0 + (0 + undef303))) /\ (undef52 = (0 + (0 + undef304))) /\ (undef54 = undef54) /\ ((1 + undef51) <= 0) /\ (undef463 = (0 + (0 + undef43))) /\ (undef468 = (0 + (0 + undef48))) /\ (undef469 = (0 + (0 + undef49))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l2, l2, (undef295 = (0 + x0^0)) /\ (undef300 = (0 + x1^0)) /\ (undef301 = (0 + x2^0)) /\ (undef302 = (0 + x3^0)) /\ (undef303 = (0 + x4^0)) /\ (undef304 = (0 + x5^0)) /\ (undef306 = undef306) /\ ((1 + undef303) <= 0) /\ (undef43 = (0 + (0 + undef295))) /\ (undef48 = (0 + (0 + undef300))) /\ (undef49 = (0 + (0 + undef301))) /\ (undef50 = (0 + (0 + undef302))) /\ (undef51 = (0 + (0 + undef303))) /\ (undef52 = (0 + (0 + undef304))) /\ (undef54 = undef54) /\ ((1 + undef51) <= 0) /\ (undef463 = (0 + (0 + undef43))) /\ (undef468 = (0 + (0 + undef48))) /\ (undef469 = (0 + (0 + undef49))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l2, l8, (undef316 = (0 + x0^0)) /\ (undef321 = (0 + x1^0)) /\ (undef322 = (0 + x2^0)) /\ (undef323 = (0 + x3^0)) /\ (undef324 = (0 + x4^0)) /\ (undef325 = (0 + x5^0)) /\ (undef327 = undef327) /\ ((0 + undef321) <= (0 + undef325)) /\ (undef22 = (0 + (0 + undef316))) /\ (undef27 = (0 + (0 + undef321))) /\ (undef28 = (0 + (0 + undef322))) /\ (undef29 = (0 + (0 + undef323))) /\ (undef30 = (0 + (0 + undef324))) /\ (undef31 = (0 + (0 + undef325))) /\ (undef33 = undef33) /\ (1 <= (0 + undef30)) /\ (undef463 = (0 + (0 + undef22))) /\ (undef468 = (0 + (0 + undef27))) /\ (undef469 = (0 + (0 + undef28))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l2, l2, (undef316 = (0 + x0^0)) /\ (undef321 = (0 + x1^0)) /\ (undef322 = (0 + x2^0)) /\ (undef323 = (0 + x3^0)) /\ (undef324 = (0 + x4^0)) /\ (undef325 = (0 + x5^0)) /\ (undef327 = undef327) /\ ((0 + undef321) <= (0 + undef325)) /\ (undef22 = (0 + (0 + undef316))) /\ (undef27 = (0 + (0 + undef321))) /\ (undef28 = (0 + (0 + undef322))) /\ (undef29 = (0 + (0 + undef323))) /\ (undef30 = (0 + (0 + undef324))) /\ (undef31 = (0 + (0 + undef325))) /\ (undef33 = undef33) /\ (1 <= (0 + undef30)) /\ (undef463 = (0 + (0 + undef22))) /\ (undef468 = (0 + (0 + undef27))) /\ (undef469 = (0 + (0 + undef28))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l2, l8, (undef316 = (0 + x0^0)) /\ (undef321 = (0 + x1^0)) /\ (undef322 = (0 + x2^0)) /\ (undef323 = (0 + x3^0)) /\ (undef324 = (0 + x4^0)) /\ (undef325 = (0 + x5^0)) /\ (undef327 = undef327) /\ ((0 + undef321) <= (0 + undef325)) /\ (undef43 = (0 + (0 + undef316))) /\ (undef48 = (0 + (0 + undef321))) /\ (undef49 = (0 + (0 + undef322))) /\ (undef50 = (0 + (0 + undef323))) /\ (undef51 = (0 + (0 + undef324))) /\ (undef52 = (0 + (0 + undef325))) /\ (undef54 = undef54) /\ ((1 + undef51) <= 0) /\ (undef463 = (0 + (0 + undef43))) /\ (undef468 = (0 + (0 + undef48))) /\ (undef469 = (0 + (0 + undef49))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l2, l2, (undef316 = (0 + x0^0)) /\ (undef321 = (0 + x1^0)) /\ (undef322 = (0 + x2^0)) /\ (undef323 = (0 + x3^0)) /\ (undef324 = (0 + x4^0)) /\ (undef325 = (0 + x5^0)) /\ (undef327 = undef327) /\ ((0 + undef321) <= (0 + undef325)) /\ (undef43 = (0 + (0 + undef316))) /\ (undef48 = (0 + (0 + undef321))) /\ (undef49 = (0 + (0 + undef322))) /\ (undef50 = (0 + (0 + undef323))) /\ (undef51 = (0 + (0 + undef324))) /\ (undef52 = (0 + (0 + undef325))) /\ (undef54 = undef54) /\ ((1 + undef51) <= 0) /\ (undef463 = (0 + (0 + undef43))) /\ (undef468 = (0 + (0 + undef48))) /\ (undef469 = (0 + (0 + undef49))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l2, l8, (undef316 = (0 + x0^0)) /\ (undef321 = (0 + x1^0)) /\ (undef322 = (0 + x2^0)) /\ (undef323 = (0 + x3^0)) /\ (undef324 = (0 + x4^0)) /\ (undef325 = (0 + x5^0)) /\ (undef327 = undef327) /\ ((0 + undef321) <= (0 + undef325)) /\ (undef64 = (0 + (0 + undef316))) /\ (undef69 = (0 + (0 + undef321))) /\ (undef70 = (0 + (0 + undef322))) /\ (undef71 = (0 + (0 + undef323))) /\ (undef72 = (0 + (0 + undef324))) /\ (undef73 = (0 + (0 + undef325))) /\ (undef75 = undef75) /\ ((0 + undef72) <= 0) /\ (0 <= (0 + undef72)) /\ (undef484 = (0 + (0 + undef64))) /\ (undef489 = (0 + (0 + undef69))) /\ (undef490 = (0 + (0 + undef70))) /\ (undef491 = (0 + (0 + undef71))) /\ (undef492 = (0 + (0 + undef72))) /\ (undef493 = (0 + (0 + undef73))) /\ (undef495 = undef495) /\ (undef463 = (0 + (0 + undef484))) /\ (undef468 = (0 + (0 + undef489))) /\ (undef469 = (0 + (0 + undef490))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef400 = (0 + (0 + undef463))) /\ (undef405 = (0 + (0 + undef468))) /\ (undef406 = (0 + (1 + undef469))) /\ (undef411 = undef411) /\ (undef412 = undef412) /\ (undef413 = undef413) /\ (undef401 = undef401) /\ ((0 + undef400) <= (0 + undef406)) /\ (undef369 = undef369) /\ (undef370 = undef370) /\ (undef371 = undef371) /\ (undef359 = undef359) /\ (undef360 = undef360) /\ (undef361 = undef361) /\ (undef362 = undef362), par{x0^0 -> (0 + undef369), x1^0 -> (0 + undef370), x2^0 -> (0 + undef371), x3^0 -> (0 + undef359), x4^0 -> (0 + undef360), x5^0 -> (0 + undef361), x6^0 -> (0 + undef362)}>
<l2, l2, (undef316 = (0 + x0^0)) /\ (undef321 = (0 + x1^0)) /\ (undef322 = (0 + x2^0)) /\ (undef323 = (0 + x3^0)) /\ (undef324 = (0 + x4^0)) /\ (undef325 = (0 + x5^0)) /\ (undef327 = undef327) /\ ((0 + undef321) <= (0 + undef325)) /\ (undef64 = (0 + (0 + undef316))) /\ (undef69 = (0 + (0 + undef321))) /\ (undef70 = (0 + (0 + undef322))) /\ (undef71 = (0 + (0 + undef323))) /\ (undef72 = (0 + (0 + undef324))) /\ (undef73 = (0 + (0 + undef325))) /\ (undef75 = undef75) /\ ((0 + undef72) <= 0) /\ (0 <= (0 + undef72)) /\ (undef484 = (0 + (0 + undef64))) /\ (undef489 = (0 + (0 + undef69))) /\ (undef490 = (0 + (0 + undef70))) /\ (undef491 = (0 + (0 + undef71))) /\ (undef492 = (0 + (0 + undef72))) /\ (undef493 = (0 + (0 + undef73))) /\ (undef495 = undef495) /\ (undef463 = (0 + (0 + undef484))) /\ (undef468 = (0 + (0 + undef489))) /\ (undef469 = (0 + (0 + undef490))) /\ (undef474 = undef474) /\ (undef475 = undef475) /\ (undef476 = undef476) /\ (undef464 = undef464) /\ (undef421 = (0 + (0 + undef463))) /\ (undef426 = (0 + (0 + undef468))) /\ (undef427 = (0 + (1 + undef469))) /\ (undef432 = undef432) /\ (undef433 = undef433) /\ (undef434 = undef434) /\ (undef422 = undef422) /\ ((1 + undef427) <= (0 + undef421)) /\ (undef379 = (0 + (0 + undef421))) /\ (undef384 = (0 + (0 + undef426))) /\ (undef385 = (0 + (0 + undef427))) /\ (undef390 = undef390) /\ (undef391 = undef391), par{x0^0 -> (0 + undef379), x1^0 -> (0 + undef384), x2^0 -> (0 + undef385), x3^0 -> (0 + undef390), x4^0 -> 0, x5^0 -> 0, x6^0 -> (0 + undef391)}>
<l2, l6, (undef337 = (0 + x0^0)) /\ (undef342 = (0 + x1^0)) /\ (undef343 = (0 + x2^0)) /\ (undef344 = (0 + x3^0)) /\ (undef345 = (0 + x4^0)) /\ (undef346 = (0 + x5^0)) /\ (undef348 = undef348) /\ ((1 + undef346) <= (0 + undef342)) /\ ((0 + undef345) <= 0) /\ (0 <= (0 + undef345)), par{x0^0 -> (0 + undef337), x1^0 -> (0 + undef342), x2^0 -> (0 + undef343), x3^0 -> (0 + undef344), x4^0 -> (0 + undef345), x5^0 -> (0 + undef346), x6^0 -> (0 + undef348)}>
<l6, l2, (undef85 = (0 + x0^0)) /\ (undef90 = (0 + x1^0)) /\ (undef91 = (0 + x2^0)) /\ (undef92 = (0 + x3^0)) /\ (undef93 = (0 + x4^0)) /\ (undef94 = (0 + x5^0)) /\ (undef96 = undef96) /\ ((1 + undef96) <= (0 + undef92)) /\ ((1 + undef96) <= (0 + undef92)) /\ (undef1 = (0 + (0 + undef85))) /\ (undef6 = (0 + (0 + undef90))) /\ (undef7 = (0 + (0 + undef91))) /\ (undef8 = (0 + (0 + undef92))) /\ (undef9 = (0 + (0 + undef93))) /\ (undef11 = (0 + (1 + undef94))) /\ (undef12 = undef12), par{x0^0 -> (0 + undef1), x1^0 -> (0 + undef6), x2^0 -> (0 + undef7), x3^0 -> (0 + undef8), x4^0 -> (0 + undef9), x5^0 -> (0 + undef11), x6^0 -> (0 + undef12)}>
<l6, l2, (undef148 = (0 + x0^0)) /\ (undef153 = (0 + x1^0)) /\ (undef154 = (0 + x2^0)) /\ (undef155 = (0 + x3^0)) /\ (undef156 = (0 + x4^0)) /\ (undef157 = (0 + x5^0)) /\ (undef159 = undef159) /\ ((1 + undef155) <= (0 + undef159)) /\ ((1 + undef155) <= (0 + undef159)) /\ (undef1 = (0 + (0 + undef148))) /\ (undef6 = (0 + (0 + undef153))) /\ (undef7 = (0 + (0 + undef154))) /\ (undef8 = (0 + (0 + undef155))) /\ (undef9 = (0 + (0 + undef156))) /\ (undef11 = (0 + (1 + undef157))) /\ (undef12 = undef12), par{x0^0 -> (0 + undef1), x1^0 -> (0 + undef6), x2^0 -> (0 + undef7), x3^0 -> (0 + undef8), x4^0 -> (0 + undef9), x5^0 -> (0 + undef11), x6^0 -> (0 + undef12)}>
<l6, l2, (undef253 = (0 + x0^0)) /\ (undef258 = (0 + x1^0)) /\ (undef259 = (0 + x2^0)) /\ (undef260 = (0 + x3^0)) /\ (undef262 = (0 + x5^0)) /\ (undef264 = undef264) /\ (undef265 = undef265) /\ ((0 + undef260) <= (0 + undef265)) /\ ((0 + undef265) <= (0 + undef260)) /\ ((0 + undef260) <= (0 + undef265)) /\ ((0 + undef265) <= (0 + undef260)), par{x0^0 -> (0 + undef253), x1^0 -> (0 + undef258), x2^0 -> (0 + undef259), x3^0 -> (0 + undef260), x4^0 -> 1, x5^0 -> (0 + undef262), x6^0 -> (0 + undef264)}>

Fresh variables:
undef1, undef6, undef7, undef8, undef9, undef11, undef12, undef22, undef27, undef28, undef29, undef30, undef31, undef33, undef43, undef48, undef49, undef50, undef51, undef52, undef54, undef64, undef69, undef70, undef71, undef72, undef73, undef75, undef85, undef90, undef91, undef92, undef93, undef94, undef96, undef106, undef111, undef112, undef113, undef114, undef115, undef117, undef127, undef132, undef133, undef134, undef135, undef136, undef138, undef148, undef153, undef154, undef155, undef156, undef157, undef159, undef169, undef174, undef175, undef176, undef178, undef180, undef181, undef190, undef195, undef196, undef197, undef199, undef201, undef202, undef211, undef216, undef217, undef218, undef219, undef220, undef222, undef232, undef237, undef238, undef239, undef240, undef241, undef243, undef253, undef258, undef259, undef260, undef262, undef264, undef265, undef274, undef279, undef280, undef281, undef282, undef283, undef285, undef295, undef300, undef301, undef302, undef303, undef304, undef306, undef316, undef321, undef322, undef323, undef324, undef325, undef327, undef337, undef342, undef343, undef344, undef345, undef346, undef348, undef359, undef360, undef361, undef362, undef369, undef370, undef371, undef379, undef384, undef385, undef390, undef391, undef400, undef401, undef405, undef406, undef411, undef412, undef413, undef421, undef422, undef426, undef427, undef432, undef433, undef434, undef442, undef443, undef447, undef453, undef454, undef455, undef463, undef464, undef468, undef469, undef474, undef475, undef476, undef484, undef489, undef490, undef491, undef492, undef493, undef495, undef505, undef506, undef507, undef510, undef516, undef517, undef518, 

Undef variables:
undef1, undef6, undef7, undef8, undef9, undef11, undef12, undef22, undef27, undef28, undef29, undef30, undef31, undef33, undef43, undef48, undef49, undef50, undef51, undef52, undef54, undef64, undef69, undef70, undef71, undef72, undef73, undef75, undef85, undef90, undef91, undef92, undef93, undef94, undef96, undef106, undef111, undef112, undef113, undef114, undef115, undef117, undef127, undef132, undef133, undef134, undef135, undef136, undef138, undef148, undef153, undef154, undef155, undef156, undef157, undef159, undef169, undef174, undef175, undef176, undef178, undef180, undef181, undef190, undef195, undef196, undef197, undef199, undef201, undef202, undef211, undef216, undef217, undef218, undef219, undef220, undef222, undef232, undef237, undef238, undef239, undef240, undef241, undef243, undef253, undef258, undef259, undef260, undef262, undef264, undef265, undef274, undef279, undef280, undef281, undef282, undef283, undef285, undef295, undef300, undef301, undef302, undef303, undef304, undef306, undef316, undef321, undef322, undef323, undef324, undef325, undef327, undef337, undef342, undef343, undef344, undef345, undef346, undef348, undef359, undef360, undef361, undef362, undef369, undef370, undef371, undef379, undef384, undef385, undef390, undef391, undef400, undef401, undef405, undef406, undef411, undef412, undef413, undef421, undef422, undef426, undef427, undef432, undef433, undef434, undef442, undef443, undef447, undef453, undef454, undef455, undef463, undef464, undef468, undef469, undef474, undef475, undef476, undef484, undef489, undef490, undef491, undef492, undef493, undef495, undef505, undef506, undef507, undef510, undef516, undef517, undef518, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

*************************************************************
*******************************************************************************************
***********************       WORKING TRANSITION SYSTEM (DAG)       ***********************
*******************************************************************************************

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l2, l2, 1 <= undef30 /\ 1 <= undef282 /\ 1 + undef427 <= undef421 /\ x0^0 = undef274 /\ x1^0 = undef279 /\ x2^0 = undef280 /\ x3^0 = undef281 /\ x4^0 = undef282 /\ x5^0 = undef283 /\ undef22 = undef274 /\ undef22 = undef463 /\ undef27 = undef279 /\ undef27 = undef468 /\ undef28 = undef280 /\ undef28 = undef469 /\ undef29 = undef281 /\ undef30 = undef282 /\ undef31 = undef283 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l2, l2, 1 + undef51 <= 0 /\ 1 + undef303 <= 0 /\ 1 + undef427 <= undef421 /\ x0^0 = undef295 /\ x1^0 = undef300 /\ x2^0 = undef301 /\ x3^0 = undef302 /\ x4^0 = undef303 /\ x5^0 = undef304 /\ undef43 = undef295 /\ undef43 = undef463 /\ undef48 = undef300 /\ undef48 = undef468 /\ undef49 = undef301 /\ undef49 = undef469 /\ undef50 = undef302 /\ undef51 = undef303 /\ undef52 = undef304 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l2, l2, undef321 <= undef325 /\ 1 <= undef30 /\ 1 + undef427 <= undef421 /\ x0^0 = undef316 /\ x1^0 = undef321 /\ x2^0 = undef322 /\ x3^0 = undef323 /\ x4^0 = undef324 /\ x5^0 = undef325 /\ undef22 = undef316 /\ undef22 = undef463 /\ undef27 = undef321 /\ undef27 = undef468 /\ undef28 = undef322 /\ undef28 = undef469 /\ undef29 = undef323 /\ undef30 = undef324 /\ undef31 = undef325 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l2, l2, undef321 <= undef325 /\ 1 + undef51 <= 0 /\ 1 + undef427 <= undef421 /\ x0^0 = undef316 /\ x1^0 = undef321 /\ x2^0 = undef322 /\ x3^0 = undef323 /\ x4^0 = undef324 /\ x5^0 = undef325 /\ undef43 = undef316 /\ undef43 = undef463 /\ undef48 = undef321 /\ undef48 = undef468 /\ undef49 = undef322 /\ undef49 = undef469 /\ undef50 = undef323 /\ undef51 = undef324 /\ undef52 = undef325 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l2, l2, undef321 <= undef325 /\ 1 + undef427 <= undef421 /\ x0^0 = undef316 /\ x1^0 = undef321 /\ x2^0 = undef322 /\ x3^0 = undef323 /\ x4^0 = undef324 /\ x5^0 = undef325 /\ undef64 = undef316 /\ undef64 = undef484 /\ undef69 = undef321 /\ undef69 = undef489 /\ undef70 = undef322 /\ undef70 = undef490 /\ undef71 = undef323 /\ undef71 = undef491 /\ undef72 = 0 /\ undef72 = undef324 /\ undef72 = undef492 /\ undef73 = undef325 /\ undef73 = undef493 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef463 = undef484 /\ undef468 = undef489 /\ undef469 = undef490 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l2, l6, 1 + undef346 <= undef342 /\ x0^0 = undef337 /\ x1^0 = undef342 /\ x2^0 = undef343 /\ x3^0 = undef344 /\ x4^0 = undef345 /\ x5^0 = undef346 /\ undef345 = 0, {x0^0 -> undef337, x1^0 -> undef342, x2^0 -> undef343, x3^0 -> undef344, x4^0 -> undef345, x5^0 -> undef346, x6^0 -> undef348, rest remain the same}>
<l6, l2, 1 + undef96 <= undef92 /\ x0^0 = undef85 /\ x1^0 = undef90 /\ x2^0 = undef91 /\ x3^0 = undef92 /\ x4^0 = undef93 /\ x5^0 = undef94 /\ undef1 = undef85 /\ undef6 = undef90 /\ undef7 = undef91 /\ undef8 = undef92 /\ undef9 = undef93 /\ undef11 = 1 + undef94, {x0^0 -> undef1, x1^0 -> undef6, x2^0 -> undef7, x3^0 -> undef8, x4^0 -> undef9, x5^0 -> undef11, x6^0 -> undef12, rest remain the same}>
<l6, l2, 1 + undef155 <= undef159 /\ x0^0 = undef148 /\ x1^0 = undef153 /\ x2^0 = undef154 /\ x3^0 = undef155 /\ x4^0 = undef156 /\ x5^0 = undef157 /\ undef1 = undef148 /\ undef6 = undef153 /\ undef7 = undef154 /\ undef8 = undef155 /\ undef9 = undef156 /\ undef11 = 1 + undef157, {x0^0 -> undef1, x1^0 -> undef6, x2^0 -> undef7, x3^0 -> undef8, x4^0 -> undef9, x5^0 -> undef11, x6^0 -> undef12, rest remain the same}>
<l6, l2, x0^0 = undef253 /\ x1^0 = undef258 /\ x2^0 = undef259 /\ x3^0 = undef260 /\ x5^0 = undef262 /\ undef260 = undef265, {x0^0 -> undef253, x1^0 -> undef258, x2^0 -> undef259, x3^0 -> undef260, x4^0 -> 1, x5^0 -> undef262, x6^0 -> undef264, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0

Graph 2:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l2, 1 + undef427 <= undef421 /\ x0^0 = undef505 /\ x1^0 = undef510 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef442 /\ undef426 = undef447 /\ undef427 = 0 /\ undef442 = undef505 /\ undef447 = undef510, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l0, l2, x0^0 = undef1 /\ x1^0 = undef6 /\ x2^0 = undef7 /\ x3^0 = undef8 /\ x4^0 = undef9 /\ x6^0 = undef11, {x0^0 -> undef1, x1^0 -> undef6, x2^0 -> undef7, x3^0 -> undef8, x4^0 -> undef9, x5^0 -> undef11, x6^0 -> undef12, rest remain the same}>
<l0, l2, 1 <= undef30 /\ 1 + undef427 <= undef421 /\ x0^0 = undef22 /\ x1^0 = undef27 /\ x2^0 = undef28 /\ x3^0 = undef29 /\ x4^0 = undef30 /\ x5^0 = undef31 /\ undef22 = undef463 /\ undef27 = undef468 /\ undef28 = undef469 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l0, l2, 1 + undef51 <= 0 /\ 1 + undef427 <= undef421 /\ x0^0 = undef43 /\ x1^0 = undef48 /\ x2^0 = undef49 /\ x3^0 = undef50 /\ x4^0 = undef51 /\ x5^0 = undef52 /\ undef43 = undef463 /\ undef48 = undef468 /\ undef49 = undef469 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l0, l2, 1 + undef427 <= undef421 /\ x0^0 = undef64 /\ x1^0 = undef69 /\ x2^0 = undef70 /\ x3^0 = undef71 /\ x4^0 = undef72 /\ x5^0 = undef73 /\ undef64 = undef484 /\ undef69 = undef489 /\ undef70 = undef490 /\ undef71 = undef491 /\ undef72 = 0 /\ undef72 = undef492 /\ undef73 = undef493 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef463 = undef484 /\ undef468 = undef489 /\ undef469 = undef490 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l0, l6, true, {all remain the same}>
<l0, l2, true, {all remain the same}>
<l0, l2, x0^0 = undef379 /\ x1^0 = undef384 /\ x2^0 = undef385, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l0, l2, 1 + undef427 <= undef421 /\ x0^0 = undef421 /\ x1^0 = undef426 /\ x2^0 = undef427 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l0, l2, 1 + undef427 <= undef421 /\ x0^0 = undef442 /\ x1^0 = undef447 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef442 /\ undef426 = undef447 /\ undef427 = 0, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l0, l2, 1 + undef427 <= undef421 /\ x0^0 = undef463 /\ x1^0 = undef468 /\ x2^0 = undef469 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>
<l0, l2, 1 + undef427 <= undef421 /\ x0^0 = undef484 /\ x1^0 = undef489 /\ x2^0 = undef490 /\ x3^0 = undef491 /\ x4^0 = undef492 /\ x5^0 = undef493 /\ undef379 = undef421 /\ undef384 = undef426 /\ undef385 = undef427 /\ undef421 = undef463 /\ undef426 = undef468 /\ undef463 = undef484 /\ undef468 = undef489 /\ undef469 = undef490 /\ undef427 = 1 + undef469, {x0^0 -> undef379, x1^0 -> undef384, x2^0 -> undef385, x3^0 -> undef390, x4^0 -> 0, x5^0 -> 0, x6^0 -> undef391, rest remain the same}>

Graph 2
<l0, l8, undef400 <= undef406 /\ x0^0 = undef505 /\ x1^0 = undef510 /\ undef400 = undef442 /\ undef405 = undef447 /\ undef406 = 0 /\ undef442 = undef505 /\ undef447 = undef510, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l0, l8, undef400 <= undef406 /\ 1 <= undef30 /\ x0^0 = undef22 /\ x1^0 = undef27 /\ x2^0 = undef28 /\ x3^0 = undef29 /\ x4^0 = undef30 /\ x5^0 = undef31 /\ undef22 = undef463 /\ undef27 = undef468 /\ undef28 = undef469 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l0, l8, undef400 <= undef406 /\ 1 + undef51 <= 0 /\ x0^0 = undef43 /\ x1^0 = undef48 /\ x2^0 = undef49 /\ x3^0 = undef50 /\ x4^0 = undef51 /\ x5^0 = undef52 /\ undef43 = undef463 /\ undef48 = undef468 /\ undef49 = undef469 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l0, l8, undef400 <= undef406 /\ x0^0 = undef64 /\ x1^0 = undef69 /\ x2^0 = undef70 /\ x3^0 = undef71 /\ x4^0 = undef72 /\ x5^0 = undef73 /\ undef64 = undef484 /\ undef69 = undef489 /\ undef70 = undef490 /\ undef71 = undef491 /\ undef72 = 0 /\ undef72 = undef492 /\ undef73 = undef493 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef463 = undef484 /\ undef468 = undef489 /\ undef469 = undef490 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l0, l8, true, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l0, l8, undef400 <= undef406 /\ x0^0 = undef400 /\ x1^0 = undef405 /\ x2^0 = undef406, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l0, l8, undef400 <= undef406 /\ x0^0 = undef442 /\ x1^0 = undef447 /\ undef400 = undef442 /\ undef405 = undef447 /\ undef406 = 0, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l0, l8, true, {all remain the same}>
<l0, l8, undef400 <= undef406 /\ x0^0 = undef463 /\ x1^0 = undef468 /\ x2^0 = undef469 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l0, l8, undef400 <= undef406 /\ x0^0 = undef484 /\ x1^0 = undef489 /\ x2^0 = undef490 /\ x3^0 = undef491 /\ x4^0 = undef492 /\ x5^0 = undef493 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef463 = undef484 /\ undef468 = undef489 /\ undef469 = undef490 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l2, l8, undef400 <= undef406 /\ 1 <= undef30 /\ 1 <= undef282 /\ x0^0 = undef274 /\ x1^0 = undef279 /\ x2^0 = undef280 /\ x3^0 = undef281 /\ x4^0 = undef282 /\ x5^0 = undef283 /\ undef22 = undef274 /\ undef22 = undef463 /\ undef27 = undef279 /\ undef27 = undef468 /\ undef28 = undef280 /\ undef28 = undef469 /\ undef29 = undef281 /\ undef30 = undef282 /\ undef31 = undef283 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l2, l8, undef400 <= undef406 /\ 1 + undef51 <= 0 /\ 1 + undef303 <= 0 /\ x0^0 = undef295 /\ x1^0 = undef300 /\ x2^0 = undef301 /\ x3^0 = undef302 /\ x4^0 = undef303 /\ x5^0 = undef304 /\ undef43 = undef295 /\ undef43 = undef463 /\ undef48 = undef300 /\ undef48 = undef468 /\ undef49 = undef301 /\ undef49 = undef469 /\ undef50 = undef302 /\ undef51 = undef303 /\ undef52 = undef304 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l2, l8, undef321 <= undef325 /\ undef400 <= undef406 /\ 1 <= undef30 /\ x0^0 = undef316 /\ x1^0 = undef321 /\ x2^0 = undef322 /\ x3^0 = undef323 /\ x4^0 = undef324 /\ x5^0 = undef325 /\ undef22 = undef316 /\ undef22 = undef463 /\ undef27 = undef321 /\ undef27 = undef468 /\ undef28 = undef322 /\ undef28 = undef469 /\ undef29 = undef323 /\ undef30 = undef324 /\ undef31 = undef325 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l2, l8, undef321 <= undef325 /\ undef400 <= undef406 /\ 1 + undef51 <= 0 /\ x0^0 = undef316 /\ x1^0 = undef321 /\ x2^0 = undef322 /\ x3^0 = undef323 /\ x4^0 = undef324 /\ x5^0 = undef325 /\ undef43 = undef316 /\ undef43 = undef463 /\ undef48 = undef321 /\ undef48 = undef468 /\ undef49 = undef322 /\ undef49 = undef469 /\ undef50 = undef323 /\ undef51 = undef324 /\ undef52 = undef325 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>
<l2, l8, undef321 <= undef325 /\ undef400 <= undef406 /\ x0^0 = undef316 /\ x1^0 = undef321 /\ x2^0 = undef322 /\ x3^0 = undef323 /\ x4^0 = undef324 /\ x5^0 = undef325 /\ undef64 = undef316 /\ undef64 = undef484 /\ undef69 = undef321 /\ undef69 = undef489 /\ undef70 = undef322 /\ undef70 = undef490 /\ undef71 = undef323 /\ undef71 = undef491 /\ undef72 = 0 /\ undef72 = undef324 /\ undef72 = undef492 /\ undef73 = undef325 /\ undef73 = undef493 /\ undef400 = undef463 /\ undef405 = undef468 /\ undef463 = undef484 /\ undef468 = undef489 /\ undef469 = undef490 /\ undef406 = 1 + undef469, {x0^0 -> undef369, x1^0 -> undef370, x2^0 -> undef371, x3^0 -> undef359, x4^0 -> undef360, x5^0 -> undef361, x6^0 -> undef362, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 1 )
( 6 , 1 )
( 8 , 2 )

*******************************************************************************************
********************************    CHECKING ASSERTIONS    ********************************
*******************************************************************************************

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 0.056898

Checking conditional termination of SCC {l2, l6}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.020726s
Ranking function: -5 + (5 / 2)*x0^0 + (~(5) / 2)*x2^0
New Graphs: 
Transitions:
<l2, l2, 1 + undef96 <= undef92 /\ 1 + undef346 <= undef342 /\ x0^0 = undef337 /\ x1^0 = undef342 /\ x2^0 = undef343 /\ x3^0 = undef344 /\ x4^0 = undef345 /\ x5^0 = undef346 /\ undef1 = undef85 /\ undef6 = undef90 /\ undef7 = undef91 /\ undef8 = undef92 /\ undef9 = undef93 /\ undef85 = undef337 /\ undef90 = undef342 /\ undef91 = undef343 /\ undef92 = undef344 /\ undef93 = undef345 /\ undef94 = undef346 /\ undef345 = 0 /\ undef11 = 1 + undef94, {x0^0 -> undef1, x1^0 -> undef6, x2^0 -> undef7, x3^0 -> undef8, x4^0 -> undef9, x5^0 -> undef11, x6^0 -> undef12, rest remain the same}>
<l2, l2, 1 + undef155 <= undef159 /\ 1 + undef346 <= undef342 /\ x0^0 = undef337 /\ x1^0 = undef342 /\ x2^0 = undef343 /\ x3^0 = undef344 /\ x4^0 = undef345 /\ x5^0 = undef346 /\ undef1 = undef148 /\ undef6 = undef153 /\ undef7 = undef154 /\ undef8 = undef155 /\ undef9 = undef156 /\ undef148 = undef337 /\ undef153 = undef342 /\ undef154 = undef343 /\ undef155 = undef344 /\ undef156 = undef345 /\ undef157 = undef346 /\ undef345 = 0 /\ undef11 = 1 + undef157, {x0^0 -> undef1, x1^0 -> undef6, x2^0 -> undef7, x3^0 -> undef8, x4^0 -> undef9, x5^0 -> undef11, x6^0 -> undef12, rest remain the same}>
<l2, l2, 1 + undef346 <= undef342 /\ x0^0 = undef337 /\ x1^0 = undef342 /\ x2^0 = undef343 /\ x3^0 = undef344 /\ x4^0 = undef345 /\ x5^0 = undef346 /\ undef253 = undef337 /\ undef258 = undef342 /\ undef259 = undef343 /\ undef260 = undef265 /\ undef260 = undef344 /\ undef262 = undef346 /\ undef345 = 0, {x0^0 -> undef253, x1^0 -> undef258, x2^0 -> undef259, x3^0 -> undef260, x4^0 -> 1, x5^0 -> undef262, x6^0 -> undef264, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0
Checking conditional termination of SCC {l2}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004504s
Ranking function: 3*x1^0 - 3*x5^0
New Graphs: 
Transitions:
<l2, l2, 1 + undef346 <= undef342 /\ x0^0 = undef337 /\ x1^0 = undef342 /\ x2^0 = undef343 /\ x3^0 = undef344 /\ x4^0 = undef345 /\ x5^0 = undef346 /\ undef253 = undef337 /\ undef258 = undef342 /\ undef259 = undef343 /\ undef260 = undef265 /\ undef260 = undef344 /\ undef262 = undef346 /\ undef345 = 0, {x0^0 -> undef253, x1^0 -> undef258, x2^0 -> undef259, x3^0 -> undef260, x4^0 -> 1, x5^0 -> undef262, x6^0 -> undef264, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0
Checking conditional termination of SCC {l2}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001307s
Ranking function: -x4^0
New Graphs: 
Proving termination of subgraph 2
Analyzing SCC {l8}...
No cycles found.

Program Terminates