YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l13, true>
<l1, l2, (arg2 > 9) /\ (undef2 > 9) /\ ((arg6 + 5) <= arg2) /\ ((arg7 + 3) <= arg2), par{arg2 -> undef2, arg3 -> 0, arg4 -> 0, arg5 -> arg3, arg6 -> undef7, arg7 -> undef7, arg8 -> 0, arg9 -> 0, arg10 -> 0, arg11 -> undef11, arg12 -> undef12, arg13 -> undef13, arg14 -> undef14, arg15 -> arg3, arg16 -> arg4, arg17 -> arg4, arg18 -> undef18, arg19 -> arg5, arg20 -> arg6, arg21 -> undef21, arg22 -> undef22, arg23 -> arg7, arg24 -> undef24, arg25 -> undef25}>
<l3, l4, (undef47 > ~(1)) /\ (arg2 > 0) /\ (undef51 > ~(1)) /\ (arg1 > 0) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6), par{arg1 -> undef26, arg2 -> undef27, arg3 -> undef28, arg4 -> undef29, arg5 -> undef30, arg6 -> undef31, arg7 -> undef32, arg8 -> undef33, arg9 -> undef34, arg10 -> undef35, arg11 -> undef36, arg12 -> undef37, arg13 -> undef38, arg14 -> undef39, arg15 -> undef40, arg16 -> undef41, arg17 -> undef42, arg18 -> undef43, arg19 -> 0, arg20 -> undef45, arg21 -> undef46, arg22 -> undef47, arg23 -> undef48, arg24 -> undef49, arg25 -> undef50}>
<l5, l4, (arg1 > 6) /\ (arg4 > ~(1)) /\ (undef52 > 8) /\ (undef53 > 8) /\ (undef54 > 8) /\ (undef55 > 8) /\ (undef56 > 6) /\ ((arg4 + 5) <= arg1) /\ ((arg5 + 7) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg7 + 3) <= arg1), par{arg1 -> undef52, arg2 -> undef53, arg3 -> undef54, arg4 -> undef55, arg5 -> undef56, arg6 -> undef57, arg7 -> arg2, arg8 -> arg3, arg9 -> undef60, arg10 -> undef61, arg11 -> undef62, arg12 -> undef63, arg13 -> undef64, arg14 -> undef65, arg15 -> undef66, arg16 -> undef67, arg17 -> undef68, arg18 -> undef69, arg19 -> 0, arg20 -> undef71, arg21 -> undef72, arg22 -> arg4, arg23 -> undef74, arg24 -> undef75, arg25 -> arg7}>
<l4, l6, (arg7 > ~(1)) /\ (arg22 < arg6) /\ (undef102 < arg7) /\ (arg8 > undef103) /\ (undef103 > 0) /\ (arg8 > ~(1)) /\ (arg1 > 8) /\ (arg2 > 8) /\ (arg3 > 8) /\ (arg4 > 8) /\ (arg5 > 6) /\ (undef77 > 9) /\ (undef78 > 9) /\ ((arg22 + 7) <= arg1) /\ ((arg9 + 9) <= arg1) /\ ((arg10 + 9) <= arg1) /\ ((arg25 + 5) <= arg1) /\ ((arg22 + 7) <= arg2) /\ ((arg11 + 9) <= arg2) /\ ((arg12 + 9) <= arg2) /\ ((arg25 + 5) <= arg2) /\ ((arg22 + 7) <= arg3) /\ ((arg13 + 9) <= arg3) /\ ((arg14 + 9) <= arg3) /\ ((arg25 + 5) <= arg3) /\ ((arg15 + 4) <= arg3) /\ ((arg16 + 4) <= arg3) /\ ((arg22 + 7) <= arg4) /\ ((arg17 + 9) <= arg4) /\ ((arg18 + 9) <= arg4) /\ ((arg25 + 5) <= arg4) /\ ((arg20 + 4) <= arg4) /\ ((arg21 + 4) <= arg4) /\ ((arg22 + 5) <= arg5) /\ ((arg23 + 7) <= arg5) /\ ((arg24 + 7) <= arg5) /\ ((arg25 + 3) <= arg5) /\ (0 = arg19), par{arg1 -> undef77, arg2 -> undef78, arg3 -> undef79, arg4 -> arg22, arg5 -> undef81, arg6 -> 0, arg7 -> arg25, arg8 -> undef84, arg9 -> undef85, arg10 -> undef86, arg11 -> undef87, arg12 -> undef88, arg13 -> undef89, arg14 -> undef90, arg15 -> undef91, arg16 -> undef92, arg17 -> undef93, arg18 -> undef94, arg19 -> undef95, arg20 -> undef96, arg21 -> undef97, arg22 -> undef98, arg23 -> undef99, arg24 -> undef100, arg25 -> undef101}>
<l4, l7, (arg7 > ~(1)) /\ (arg22 < arg6) /\ (undef129 < arg7) /\ (arg8 > ~(1)) /\ (undef130 < arg8) /\ ((undef104 - 1) <= arg1) /\ ((undef104 - 1) <= arg2) /\ ((undef104 - 1) <= arg3) /\ ((undef104 - 1) <= arg4) /\ ((undef104 - 3) <= arg5) /\ ((undef105 - 1) <= arg1) /\ ((undef105 - 1) <= arg2) /\ ((undef105 - 1) <= arg3) /\ ((undef105 - 1) <= arg4) /\ ((undef105 - 3) <= arg5) /\ (arg1 > 8) /\ (arg2 > 8) /\ (arg3 > 8) /\ (arg4 > 8) /\ (arg5 > 6) /\ (undef104 > 9) /\ (undef105 > 9) /\ ((arg22 + 7) <= arg1) /\ ((arg9 + 9) <= arg1) /\ ((arg10 + 9) <= arg1) /\ ((arg25 + 5) <= arg1) /\ ((arg22 + 7) <= arg2) /\ ((arg11 + 9) <= arg2) /\ ((arg12 + 9) <= arg2) /\ ((arg25 + 5) <= arg2) /\ ((arg22 + 7) <= arg3) /\ ((arg13 + 9) <= arg3) /\ ((arg14 + 9) <= arg3) /\ ((arg25 + 5) <= arg3) /\ ((arg15 + 4) <= arg3) /\ ((arg16 + 4) <= arg3) /\ ((arg22 + 7) <= arg4) /\ ((arg17 + 9) <= arg4) /\ ((arg18 + 9) <= arg4) /\ ((arg25 + 5) <= arg4) /\ ((arg20 + 4) <= arg4) /\ ((arg21 + 4) <= arg4) /\ ((arg22 + 5) <= arg5) /\ ((arg23 + 7) <= arg5) /\ ((arg24 + 7) <= arg5) /\ ((arg25 + 3) <= arg5) /\ (0 = arg19), par{arg1 -> undef104, arg2 -> undef105, arg3 -> arg22, arg4 -> 0, arg5 -> arg25, arg6 -> undef109, arg7 -> undef110, arg8 -> undef111, arg9 -> undef112, arg10 -> undef113, arg11 -> undef114, arg12 -> undef115, arg13 -> undef116, arg14 -> undef117, arg15 -> undef118, arg16 -> undef119, arg17 -> undef120, arg18 -> undef121, arg19 -> undef122, arg20 -> undef123, arg21 -> undef124, arg22 -> undef125, arg23 -> undef126, arg24 -> undef127, arg25 -> undef128}>
<l4, l8, (arg7 > ~(1)) /\ (arg22 < arg6) /\ (undef133 < arg7) /\ (undef156 < arg8) /\ (arg8 > ~(1)) /\ (undef156 > 0) /\ (undef133 > 0) /\ (arg1 > 8) /\ (arg2 > 8) /\ (arg3 > 8) /\ (arg4 > 8) /\ (arg5 > 6) /\ (undef131 > 9) /\ (undef132 > 9) /\ ((arg22 + 7) <= arg1) /\ ((arg9 + 9) <= arg1) /\ ((arg10 + 9) <= arg1) /\ ((arg25 + 5) <= arg1) /\ ((arg22 + 7) <= arg2) /\ ((arg11 + 9) <= arg2) /\ ((arg12 + 9) <= arg2) /\ ((arg25 + 5) <= arg2) /\ ((arg22 + 7) <= arg3) /\ ((arg13 + 9) <= arg3) /\ ((arg14 + 9) <= arg3) /\ ((arg25 + 5) <= arg3) /\ ((arg15 + 4) <= arg3) /\ ((arg16 + 4) <= arg3) /\ ((arg22 + 7) <= arg4) /\ ((arg17 + 9) <= arg4) /\ ((arg18 + 9) <= arg4) /\ ((arg25 + 5) <= arg4) /\ ((arg20 + 4) <= arg4) /\ ((arg21 + 4) <= arg4) /\ ((arg22 + 5) <= arg5) /\ ((arg23 + 7) <= arg5) /\ ((arg24 + 7) <= arg5) /\ ((arg25 + 3) <= arg5) /\ (0 = arg19), par{arg1 -> undef131, arg2 -> undef132, arg3 -> undef133, arg4 -> 0, arg5 -> 0, arg6 -> 0, arg7 -> undef133, arg8 -> undef138, arg9 -> arg22, arg10 -> undef140, arg11 -> 0, arg12 -> arg25, arg13 -> undef143, arg14 -> undef144, arg15 -> undef145, arg16 -> undef146, arg17 -> undef147, arg18 -> undef148, arg19 -> undef149, arg20 -> undef150, arg21 -> undef151, arg22 -> undef152, arg23 -> undef153, arg24 -> undef154, arg25 -> undef155}>
<l4, l9, (arg7 > ~(1)) /\ (arg22 < arg6) /\ (undef159 < arg7) /\ (undef182 < arg8) /\ (undef159 > 0) /\ (arg8 > ~(1)) /\ (arg1 > 8) /\ (arg2 > 8) /\ (arg3 > 8) /\ (arg4 > 8) /\ (arg5 > 6) /\ (undef157 > 9) /\ (undef158 > 9) /\ ((arg22 + 7) <= arg1) /\ ((arg9 + 9) <= arg1) /\ ((arg10 + 9) <= arg1) /\ ((arg25 + 5) <= arg1) /\ ((arg22 + 7) <= arg2) /\ ((arg11 + 9) <= arg2) /\ ((arg12 + 9) <= arg2) /\ ((arg25 + 5) <= arg2) /\ ((arg22 + 7) <= arg3) /\ ((arg13 + 9) <= arg3) /\ ((arg14 + 9) <= arg3) /\ ((arg25 + 5) <= arg3) /\ ((arg15 + 4) <= arg3) /\ ((arg16 + 4) <= arg3) /\ ((arg22 + 7) <= arg4) /\ ((arg17 + 9) <= arg4) /\ ((arg18 + 9) <= arg4) /\ ((arg25 + 5) <= arg4) /\ ((arg20 + 4) <= arg4) /\ ((arg21 + 4) <= arg4) /\ ((arg22 + 5) <= arg5) /\ ((arg23 + 7) <= arg5) /\ ((arg24 + 7) <= arg5) /\ ((arg25 + 3) <= arg5) /\ (0 = arg19), par{arg1 -> undef157, arg2 -> undef158, arg3 -> undef159, arg4 -> 0, arg5 -> 0, arg6 -> 0, arg7 -> undef159, arg8 -> arg22, arg9 -> 0, arg10 -> arg25, arg11 -> undef167, arg12 -> undef168, arg13 -> undef169, arg14 -> undef170, arg15 -> undef171, arg16 -> undef172, arg17 -> undef173, arg18 -> undef174, arg19 -> undef175, arg20 -> undef176, arg21 -> undef177, arg22 -> undef178, arg23 -> undef179, arg24 -> undef180, arg25 -> undef181}>
<l6, l6, (arg6 > ~(1)) /\ (arg4 > arg6) /\ (undef183 <= arg1) /\ ((undef184 - 1) <= arg2) /\ (arg1 > 9) /\ (arg2 > 9) /\ (undef183 > 9) /\ (undef184 > 9) /\ ((arg4 + 7) <= arg1) /\ ((arg3 + 10) <= arg1) /\ ((arg7 + 5) <= arg1) /\ ((arg4 + 7) <= arg2) /\ ((arg5 + 10) <= arg2) /\ ((arg7 + 5) <= arg2) /\ ((arg8 + 5) <= arg2) /\ ((arg6 + 2) <= arg2), par{arg1 -> undef183, arg2 -> undef184, arg6 -> (arg6 + 1), arg9 -> undef191, arg10 -> undef192, arg11 -> undef193, arg12 -> undef194, arg13 -> undef195, arg14 -> undef196, arg15 -> undef197, arg16 -> undef198, arg17 -> undef199, arg18 -> undef200, arg19 -> undef201, arg20 -> undef202, arg21 -> undef203, arg22 -> undef204, arg23 -> undef205, arg24 -> undef206, arg25 -> undef207}>
<l7, l7, (arg4 > ~(1)) /\ (arg3 > arg4) /\ (undef208 <= arg1) /\ (undef208 <= arg2) /\ ((undef209 - 1) <= arg2) /\ (arg1 > 9) /\ (arg2 > 9) /\ (undef208 > 9) /\ (undef209 > 9) /\ ((arg3 + 7) <= arg1) /\ ((arg5 + 5) <= arg1) /\ ((arg3 + 7) <= arg2) /\ ((arg4 + 2) <= arg2) /\ ((arg5 + 5) <= arg2), par{arg1 -> undef208, arg2 -> undef209, arg4 -> (arg4 + 1), arg6 -> undef213, arg7 -> undef214, arg8 -> undef215, arg9 -> undef216, arg10 -> undef217, arg11 -> undef218, arg12 -> undef219, arg13 -> undef220, arg14 -> undef221, arg15 -> undef222, arg16 -> undef223, arg17 -> undef224, arg18 -> undef225, arg19 -> undef226, arg20 -> undef227, arg21 -> undef228, arg22 -> undef229, arg23 -> undef230, arg24 -> undef231, arg25 -> undef232}>
<l8, l8, (arg6 > 0) /\ (arg5 > 0) /\ (undef238 > arg6) /\ (arg6 < arg4) /\ (arg4 > 0) /\ (arg6 < arg3) /\ (undef237 < arg5) /\ (arg11 > ~(1)) /\ (arg9 > arg11) /\ (undef233 <= arg1) /\ (arg1 > 9) /\ (arg2 > 9) /\ (undef233 > 9) /\ (undef234 > 9) /\ ((arg9 + 7) <= arg1) /\ ((arg8 + 10) <= arg1) /\ ((arg12 + 5) <= arg1) /\ ((arg9 + 7) <= arg2) /\ ((arg10 + 10) <= arg2) /\ ((arg12 + 5) <= arg2) /\ ((arg13 + 5) <= arg2) /\ ((arg11 + 2) <= arg2), par{arg1 -> undef233, arg2 -> undef234, arg5 -> undef237, arg6 -> undef238, arg7 -> undef239, arg11 -> (arg11 + 1), arg14 -> undef246, arg15 -> undef247, arg16 -> undef248, arg17 -> undef249, arg18 -> undef250, arg19 -> undef251, arg20 -> undef252, arg21 -> undef253, arg22 -> undef254, arg23 -> undef255, arg24 -> undef256, arg25 -> undef257}>
<l8, l8, (undef264 < arg3) /\ (arg3 > ~(1)) /\ (undef262 < arg4) /\ (arg4 > ~(1)) /\ (arg9 > arg11) /\ (arg11 > ~(1)) /\ (undef258 <= arg1) /\ (arg1 > 11) /\ (arg2 > 11) /\ (undef258 > 11) /\ (undef259 > 11) /\ ((arg9 + 7) <= arg1) /\ ((arg8 + 10) <= arg1) /\ ((arg12 + 5) <= arg1) /\ ((arg9 + 7) <= arg2) /\ ((arg10 + 10) <= arg2) /\ ((arg12 + 5) <= arg2) /\ ((arg13 + 5) <= arg2) /\ ((arg11 + 2) <= arg2) /\ (arg3 = arg7), par{arg1 -> undef258, arg2 -> undef259, arg3 -> undef260, arg4 -> 0, arg5 -> undef262, arg6 -> 1, arg7 -> undef264, arg11 -> (arg11 + 1), arg14 -> undef271, arg15 -> undef272, arg16 -> undef273, arg17 -> undef274, arg18 -> undef275, arg19 -> undef276, arg20 -> undef277, arg21 -> undef278, arg22 -> undef279, arg23 -> undef280, arg24 -> undef281, arg25 -> undef282}>
<l9, l9, (arg6 > 0) /\ (arg5 > 0) /\ (undef288 > arg6) /\ (arg6 < arg4) /\ (arg4 > 0) /\ (arg6 < arg3) /\ (undef287 < arg5) /\ (arg9 > ~(1)) /\ (arg8 > arg9) /\ (undef283 <= arg1) /\ (arg1 > 9) /\ (arg2 > 9) /\ (undef283 > 9) /\ (undef284 > 9) /\ ((arg8 + 7) <= arg1) /\ ((arg10 + 5) <= arg1) /\ ((arg8 + 7) <= arg2) /\ ((arg9 + 2) <= arg2) /\ ((arg10 + 5) <= arg2), par{arg1 -> undef283, arg2 -> undef284, arg5 -> undef287, arg6 -> undef288, arg7 -> undef289, arg9 -> (arg9 + 1), arg11 -> undef293, arg12 -> undef294, arg13 -> undef295, arg14 -> undef296, arg15 -> undef297, arg16 -> undef298, arg17 -> undef299, arg18 -> undef300, arg19 -> undef301, arg20 -> undef302, arg21 -> undef303, arg22 -> undef304, arg23 -> undef305, arg24 -> undef306, arg25 -> undef307}>
<l9, l9, (undef314 < arg3) /\ (arg3 > ~(1)) /\ (undef312 < arg4) /\ (arg4 > ~(1)) /\ (arg8 > arg9) /\ (arg9 > ~(1)) /\ (undef308 <= arg1) /\ (arg1 > 11) /\ (arg2 > 11) /\ (undef308 > 11) /\ (undef309 > 11) /\ ((arg8 + 7) <= arg1) /\ ((arg10 + 5) <= arg1) /\ ((arg8 + 7) <= arg2) /\ ((arg9 + 2) <= arg2) /\ ((arg10 + 5) <= arg2) /\ (arg3 = arg7), par{arg1 -> undef308, arg2 -> undef309, arg3 -> undef310, arg4 -> 0, arg5 -> undef312, arg6 -> 1, arg7 -> undef314, arg9 -> (arg9 + 1), arg11 -> undef318, arg12 -> undef319, arg13 -> undef320, arg14 -> undef321, arg15 -> undef322, arg16 -> undef323, arg17 -> undef324, arg18 -> undef325, arg19 -> undef326, arg20 -> undef327, arg21 -> undef328, arg22 -> undef329, arg23 -> undef330, arg24 -> undef331, arg25 -> undef332}>
<l8, l10, (arg1 > 9) /\ (arg9 <= arg11) /\ (arg2 > 9) /\ (undef333 > 11) /\ ((arg9 + 7) <= arg1) /\ ((arg8 + 10) <= arg1) /\ ((arg12 + 5) <= arg1) /\ ((arg9 + 7) <= arg2) /\ ((arg10 + 10) <= arg2) /\ ((arg12 + 5) <= arg2) /\ ((arg13 + 5) <= arg2) /\ ((arg11 + 2) <= arg2), par{arg1 -> undef333, arg2 -> undef334, arg3 -> arg7, arg4 -> arg9, arg5 -> arg11, arg6 -> arg12, arg7 -> undef339, arg8 -> undef340, arg9 -> undef341, arg10 -> undef342, arg11 -> undef343, arg12 -> undef344, arg13 -> undef345, arg14 -> undef346, arg15 -> undef347, arg16 -> undef348, arg17 -> undef349, arg18 -> undef350, arg19 -> undef351, arg20 -> undef352, arg21 -> undef353, arg22 -> undef354, arg23 -> undef355, arg24 -> undef356, arg25 -> undef357}>
<l9, l10, (arg1 > 9) /\ (arg8 <= arg9) /\ (arg2 > 9) /\ (undef358 > 11) /\ ((arg8 + 7) <= arg1) /\ ((arg10 + 5) <= arg1) /\ ((arg8 + 7) <= arg2) /\ ((arg9 + 2) <= arg2) /\ ((arg10 + 5) <= arg2), par{arg1 -> undef358, arg2 -> undef359, arg3 -> arg7, arg4 -> arg8, arg5 -> arg9, arg6 -> arg10, arg7 -> undef364, arg8 -> undef365, arg9 -> undef366, arg10 -> undef367, arg11 -> undef368, arg12 -> undef369, arg13 -> undef370, arg14 -> undef371, arg15 -> undef372, arg16 -> undef373, arg17 -> undef374, arg18 -> undef375, arg19 -> undef376, arg20 -> undef377, arg21 -> undef378, arg22 -> undef379, arg23 -> undef380, arg24 -> undef381, arg25 -> undef382}>
<l4, l10, (arg1 > 8) /\ (arg22 >= arg6) /\ (arg2 > 8) /\ (arg3 > 8) /\ (arg4 > 8) /\ (arg5 > 6) /\ (undef383 > 10) /\ ((arg22 + 7) <= arg1) /\ ((arg9 + 9) <= arg1) /\ ((arg10 + 9) <= arg1) /\ ((arg25 + 5) <= arg1) /\ ((arg22 + 7) <= arg2) /\ ((arg11 + 9) <= arg2) /\ ((arg12 + 9) <= arg2) /\ ((arg25 + 5) <= arg2) /\ ((arg22 + 7) <= arg3) /\ ((arg13 + 9) <= arg3) /\ ((arg14 + 9) <= arg3) /\ ((arg25 + 5) <= arg3) /\ ((arg15 + 4) <= arg3) /\ ((arg16 + 4) <= arg3) /\ ((arg22 + 7) <= arg4) /\ ((arg17 + 9) <= arg4) /\ ((arg18 + 9) <= arg4) /\ ((arg25 + 5) <= arg4) /\ ((arg20 + 4) <= arg4) /\ ((arg21 + 4) <= arg4) /\ ((arg22 + 5) <= arg5) /\ ((arg23 + 7) <= arg5) /\ ((arg24 + 7) <= arg5) /\ ((arg25 + 3) <= arg5) /\ (0 = arg19), par{arg1 -> undef383, arg2 -> 0, arg3 -> 0, arg4 -> arg22, arg5 -> arg22, arg6 -> arg25, arg7 -> undef389, arg8 -> undef390, arg9 -> undef391, arg10 -> undef392, arg11 -> undef393, arg12 -> undef394, arg13 -> undef395, arg14 -> undef396, arg15 -> undef397, arg16 -> undef398, arg17 -> undef399, arg18 -> undef400, arg19 -> undef401, arg20 -> undef402, arg21 -> undef403, arg22 -> undef404, arg23 -> undef405, arg24 -> undef406, arg25 -> undef407}>
<l6, l10, (arg1 > 9) /\ (arg4 <= arg6) /\ (arg2 > 9) /\ (undef408 > 10) /\ ((arg4 + 7) <= arg1) /\ ((arg3 + 10) <= arg1) /\ ((arg7 + 5) <= arg1) /\ ((arg4 + 7) <= arg2) /\ ((arg5 + 10) <= arg2) /\ ((arg7 + 5) <= arg2) /\ ((arg8 + 5) <= arg2) /\ ((arg6 + 2) <= arg2), par{arg1 -> undef408, arg2 -> 0, arg3 -> 0, arg5 -> arg6, arg6 -> arg7, arg7 -> undef414, arg8 -> undef415, arg9 -> undef416, arg10 -> undef417, arg11 -> undef418, arg12 -> undef419, arg13 -> undef420, arg14 -> undef421, arg15 -> undef422, arg16 -> undef423, arg17 -> undef424, arg18 -> undef425, arg19 -> undef426, arg20 -> undef427, arg21 -> undef428, arg22 -> undef429, arg23 -> undef430, arg24 -> undef431, arg25 -> undef432}>
<l7, l10, (arg1 > 9) /\ (arg3 <= arg4) /\ (arg2 > 9) /\ (undef433 > 10) /\ ((arg3 + 7) <= arg1) /\ ((arg5 + 5) <= arg1) /\ ((arg3 + 7) <= arg2) /\ ((arg4 + 2) <= arg2) /\ ((arg5 + 5) <= arg2), par{arg1 -> undef433, arg2 -> 0, arg3 -> 0, arg4 -> arg3, arg5 -> arg4, arg6 -> arg5, arg7 -> undef439, arg8 -> undef440, arg9 -> undef441, arg10 -> undef442, arg11 -> undef443, arg12 -> undef444, arg13 -> undef445, arg14 -> undef446, arg15 -> undef447, arg16 -> undef448, arg17 -> undef449, arg18 -> undef450, arg19 -> undef451, arg20 -> undef452, arg21 -> undef453, arg22 -> undef454, arg23 -> undef455, arg24 -> undef456, arg25 -> undef457}>
<l10, l11, (arg1 > 9) /\ (arg5 > 0) /\ (undef458 > 9) /\ (undef459 > ~(1)) /\ ((undef460 + 8) <= arg1) /\ ((arg4 + 9) <= arg1) /\ ((undef462 + 10) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg5 + 4) <= arg1) /\ ((arg8 + 6) <= arg1) /\ ((arg7 + 6) <= arg1), par{arg1 -> undef458, arg2 -> undef459, arg3 -> undef460, arg5 -> undef462, arg6 -> (arg5 - 1), arg7 -> arg6, arg8 -> undef465, arg9 -> undef466, arg10 -> undef467, arg11 -> undef468, arg12 -> undef469, arg13 -> undef470, arg14 -> undef471, arg15 -> undef472, arg16 -> undef473, arg17 -> undef474, arg18 -> undef475, arg19 -> undef476, arg20 -> undef477, arg21 -> undef478, arg22 -> undef479, arg23 -> undef480, arg24 -> undef481, arg25 -> undef482}>
<l10, l11, (arg2 > 0) /\ (arg3 > 0) /\ (arg5 > 0) /\ (undef508 < arg3) /\ (undef509 > arg2) /\ (arg1 > 9) /\ (undef483 > 9) /\ (undef484 > ~(1)) /\ ((undef485 + 8) <= arg1) /\ ((arg4 + 9) <= arg1) /\ ((undef487 + 10) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg5 + 4) <= arg1) /\ ((arg8 + 6) <= arg1) /\ ((arg7 + 6) <= arg1), par{arg1 -> undef483, arg2 -> undef484, arg3 -> undef485, arg5 -> undef487, arg6 -> (arg5 - 1), arg7 -> arg6, arg8 -> undef490, arg9 -> undef491, arg10 -> undef492, arg11 -> undef493, arg12 -> undef494, arg13 -> undef495, arg14 -> undef496, arg15 -> undef497, arg16 -> undef498, arg17 -> undef499, arg18 -> undef500, arg19 -> undef501, arg20 -> undef502, arg21 -> undef503, arg22 -> undef504, arg23 -> undef505, arg24 -> undef506, arg25 -> undef507}>
<l11, l10, (arg1 > 9) /\ (arg2 > 0) /\ (undef510 > 9) /\ ((arg3 + 8) <= arg1) /\ ((arg4 + 9) <= arg1) /\ ((arg5 + 10) <= arg1) /\ ((arg7 + 7) <= arg1) /\ ((arg6 + 4) <= arg1), par{arg1 -> undef510, arg2 -> 0, arg3 -> 0, arg5 -> arg6, arg6 -> arg7, arg7 -> undef516, arg8 -> undef517, arg9 -> undef518, arg10 -> undef519, arg11 -> undef520, arg12 -> undef521, arg13 -> undef522, arg14 -> undef523, arg15 -> undef524, arg16 -> undef525, arg17 -> undef526, arg18 -> undef527, arg19 -> undef528, arg20 -> undef529, arg21 -> undef530, arg22 -> undef531, arg23 -> undef532, arg24 -> undef533, arg25 -> undef534}>
<l3, l1, (undef535 > ~(1)) /\ (arg2 > 0) /\ ((undef536 - 7) <= arg1) /\ (arg1 > 0) /\ (undef536 > 7), par{arg1 -> undef535, arg2 -> undef536, arg3 -> undef537, arg4 -> undef538, arg5 -> 1, arg6 -> 0, arg7 -> 0, arg8 -> undef542, arg9 -> undef543, arg10 -> undef544, arg11 -> undef545, arg12 -> undef546, arg13 -> undef547, arg14 -> undef548, arg15 -> undef549, arg16 -> undef550, arg17 -> undef551, arg18 -> undef552, arg19 -> undef553, arg20 -> undef554, arg21 -> undef555, arg22 -> undef556, arg23 -> undef557, arg24 -> undef558, arg25 -> undef559}>
<l2, l12, (arg2 > 11) /\ (undef560 > 11) /\ ((arg20 + 5) <= arg2) /\ ((arg21 + 9) <= arg2) /\ ((arg23 + 3) <= arg2) /\ ((arg22 + 9) <= arg2), par{arg1 -> undef560, arg2 -> arg1, arg3 -> arg13, arg4 -> arg11, arg5 -> arg7, arg6 -> arg12, arg7 -> arg6, arg8 -> undef567, arg9 -> arg3, arg10 -> arg14, arg11 -> arg5, arg12 -> 0, arg13 -> arg4, arg14 -> arg8, arg15 -> arg9, arg16 -> arg10, arg17 -> arg15, arg18 -> arg16, arg19 -> arg17, arg20 -> arg19, arg21 -> arg20, arg22 -> undef581, arg23 -> undef582, arg24 -> undef583, arg25 -> arg23}>
<l12, l12, (arg2 > 0) /\ (undef610 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef610) /\ (arg10 > 0) /\ (arg4 > 0) /\ (arg13 > 0) /\ (arg11 > 0) /\ (arg12 > 0) /\ (undef611 > ~(1)) /\ (arg9 > 0) /\ (arg5 > 0) /\ (arg19 > 0) /\ (arg14 > 0) /\ (arg18 > 0) /\ (arg17 > 0) /\ (arg15 > 0) /\ (arg16 > 0) /\ (arg25 > ~(1)) /\ (arg21 > ~(1)) /\ (arg1 > 9) /\ (undef585 > 9) /\ ((arg21 + 5) <= arg1) /\ ((arg22 + 9) <= arg1) /\ ((arg23 + 9) <= arg1) /\ ((arg25 + 3) <= arg1) /\ ((arg24 + 9) <= arg1), par{arg1 -> undef585, arg2 -> (arg2 - 1), arg4 -> undef588, arg5 -> undef589, arg9 -> undef593, arg11 -> undef595, arg13 -> undef597, arg14 -> undef598, arg15 -> undef599, arg16 -> undef600, arg17 -> undef601, arg18 -> undef602, arg19 -> undef603, arg20 -> (arg20 + 1), arg21 -> (arg21 + 1), arg22 -> undef606, arg23 -> undef607, arg24 -> undef608, arg25 -> (arg25 + 1)}>
<l12, l12, (arg2 > 0) /\ (undef637 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef637) /\ (arg10 > 0) /\ (arg12 > 0) /\ (undef638 > ~(1)) /\ (arg19 > 0) /\ (arg18 > 0) /\ (arg17 > 0) /\ (arg8 > 0) /\ (arg25 > ~(1)) /\ (arg21 > ~(1)) /\ (arg1 > 11) /\ (undef612 > 13) /\ ((arg21 + 5) <= arg1) /\ ((arg22 + 9) <= arg1) /\ ((arg23 + 9) <= arg1) /\ ((arg25 + 3) <= arg1) /\ ((arg24 + 9) <= arg1) /\ (arg8 = arg9) /\ (arg10 = arg11) /\ (arg12 = arg13) /\ (arg7 = arg16), par{arg1 -> undef612, arg2 -> (arg2 - 1), arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef617, arg7 -> undef618, arg9 -> undef620, arg11 -> undef622, arg13 -> 0, arg14 -> 2, arg15 -> undef626, arg16 -> undef627, arg17 -> undef628, arg18 -> undef629, arg19 -> undef630, arg20 -> (arg20 + 1), arg21 -> (arg21 + 1), arg22 -> undef633, arg23 -> undef634, arg24 -> undef635, arg25 -> (arg25 + 1)}>
<l13, l3, true, par{arg1 -> undef639, arg2 -> undef640, arg3 -> undef641, arg4 -> undef642, arg5 -> undef643, arg6 -> undef644, arg7 -> undef645, arg8 -> undef646, arg9 -> undef647, arg10 -> undef648, arg11 -> undef649, arg12 -> undef650, arg13 -> undef651, arg14 -> undef652, arg15 -> undef653, arg16 -> undef654, arg17 -> undef655, arg18 -> undef656, arg19 -> undef657, arg20 -> undef658, arg21 -> undef659, arg22 -> undef660, arg23 -> undef661, arg24 -> undef662, arg25 -> undef663}>

Fresh variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef21, undef22, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef71, undef72, undef74, undef75, undef77, undef78, undef79, undef81, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef96, undef97, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef138, undef140, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef213, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef221, undef222, undef223, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef237, undef238, undef239, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, undef262, undef264, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef284, undef287, undef288, undef289, undef293, undef294, undef295, undef296, undef297, undef298, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef309, undef310, undef312, undef314, undef318, undef319, undef320, undef321, undef322, undef323, undef324, undef325, undef326, undef327, undef328, undef329, undef330, undef331, undef332, undef333, undef334, undef339, undef340, undef341, undef342, undef343, undef344, undef345, undef346, undef347, undef348, undef349, undef350, undef351, undef352, undef353, undef354, undef355, undef356, undef357, undef358, undef359, undef364, undef365, undef366, undef367, undef368, undef369, undef370, undef371, undef372, undef373, undef374, undef375, undef376, undef377, undef378, undef379, undef380, undef381, undef382, undef383, undef389, undef390, undef391, undef392, undef393, undef394, undef395, undef396, undef397, undef398, undef399, undef400, undef401, undef402, undef403, undef404, undef405, undef406, undef407, undef408, undef414, undef415, undef416, undef417, undef418, undef419, undef420, undef421, undef422, undef423, undef424, undef425, undef426, undef427, undef428, undef429, undef430, undef431, undef432, undef433, undef439, undef440, undef441, undef442, undef443, undef444, undef445, undef446, undef447, undef448, undef449, undef450, undef451, undef452, undef453, undef454, undef455, undef456, undef457, undef458, undef459, undef460, undef462, undef465, undef466, undef467, undef468, undef469, undef470, undef471, undef472, undef473, undef474, undef475, undef476, undef477, undef478, undef479, undef480, undef481, undef482, undef483, undef484, undef485, undef487, undef490, undef491, undef492, undef493, undef494, undef495, undef496, undef497, undef498, undef499, undef500, undef501, undef502, undef503, undef504, undef505, undef506, undef507, undef508, undef509, undef510, undef516, undef517, undef518, undef519, undef520, undef521, undef522, undef523, undef524, undef525, undef526, undef527, undef528, undef529, undef530, undef531, undef532, undef533, undef534, undef535, undef536, undef537, undef538, undef542, undef543, undef544, undef545, undef546, undef547, undef548, undef549, undef550, undef551, undef552, undef553, undef554, undef555, undef556, undef557, undef558, undef559, undef560, undef567, undef581, undef582, undef583, undef585, undef588, undef589, undef593, undef595, undef597, undef598, undef599, undef600, undef601, undef602, undef603, undef606, undef607, undef608, undef610, undef611, undef612, undef617, undef618, undef620, undef622, undef626, undef627, undef628, undef629, undef630, undef633, undef634, undef635, undef637, undef638, undef639, undef640, undef641, undef642, undef643, undef644, undef645, undef646, undef647, undef648, undef649, undef650, undef651, undef652, undef653, undef654, undef655, undef656, undef657, undef658, undef659, undef660, undef661, undef662, undef663, 

Undef variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef21, undef22, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef71, undef72, undef74, undef75, undef77, undef78, undef79, undef81, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef96, undef97, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef138, undef140, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef213, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef221, undef222, undef223, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef237, undef238, undef239, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, undef262, undef264, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef284, undef287, undef288, undef289, undef293, undef294, undef295, undef296, undef297, undef298, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef309, undef310, undef312, undef314, undef318, undef319, undef320, undef321, undef322, undef323, undef324, undef325, undef326, undef327, undef328, undef329, undef330, undef331, undef332, undef333, undef334, undef339, undef340, undef341, undef342, undef343, undef344, undef345, undef346, undef347, undef348, undef349, undef350, undef351, undef352, undef353, undef354, undef355, undef356, undef357, undef358, undef359, undef364, undef365, undef366, undef367, undef368, undef369, undef370, undef371, undef372, undef373, undef374, undef375, undef376, undef377, undef378, undef379, undef380, undef381, undef382, undef383, undef389, undef390, undef391, undef392, undef393, undef394, undef395, undef396, undef397, undef398, undef399, undef400, undef401, undef402, undef403, undef404, undef405, undef406, undef407, undef408, undef414, undef415, undef416, undef417, undef418, undef419, undef420, undef421, undef422, undef423, undef424, undef425, undef426, undef427, undef428, undef429, undef430, undef431, undef432, undef433, undef439, undef440, undef441, undef442, undef443, undef444, undef445, undef446, undef447, undef448, undef449, undef450, undef451, undef452, undef453, undef454, undef455, undef456, undef457, undef458, undef459, undef460, undef462, undef465, undef466, undef467, undef468, undef469, undef470, undef471, undef472, undef473, undef474, undef475, undef476, undef477, undef478, undef479, undef480, undef481, undef482, undef483, undef484, undef485, undef487, undef490, undef491, undef492, undef493, undef494, undef495, undef496, undef497, undef498, undef499, undef500, undef501, undef502, undef503, undef504, undef505, undef506, undef507, undef508, undef509, undef510, undef516, undef517, undef518, undef519, undef520, undef521, undef522, undef523, undef524, undef525, undef526, undef527, undef528, undef529, undef530, undef531, undef532, undef533, undef534, undef535, undef536, undef537, undef538, undef542, undef543, undef544, undef545, undef546, undef547, undef548, undef549, undef550, undef551, undef552, undef553, undef554, undef555, undef556, undef557, undef558, undef559, undef560, undef567, undef581, undef582, undef583, undef585, undef588, undef589, undef593, undef595, undef597, undef598, undef599, undef600, undef601, undef602, undef603, undef606, undef607, undef608, undef610, undef611, undef612, undef617, undef618, undef620, undef622, undef626, undef627, undef628, undef629, undef630, undef633, undef634, undef635, undef637, undef638, undef639, undef640, undef641, undef642, undef643, undef644, undef645, undef646, undef647, undef648, undef649, undef650, undef651, undef652, undef653, undef654, undef655, undef656, undef657, undef658, undef659, undef660, undef661, undef662, undef663, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l6, (undef47 > ~(1)) /\ (undef640 > 0) /\ (undef51 > ~(1)) /\ (undef639 > 0) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef32 > ~(1)) /\ (undef47 < undef31) /\ (undef102 < undef32) /\ (undef33 > undef103) /\ (undef103 > 0) /\ (undef33 > ~(1)) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef77 > 9) /\ (undef78 > 9) /\ ((undef47 + 7) <= undef26) /\ ((undef34 + 9) <= undef26) /\ ((undef35 + 9) <= undef26) /\ ((undef50 + 5) <= undef26) /\ ((undef47 + 7) <= undef27) /\ ((undef36 + 9) <= undef27) /\ ((undef37 + 9) <= undef27) /\ ((undef50 + 5) <= undef27) /\ ((undef47 + 7) <= undef28) /\ ((undef38 + 9) <= undef28) /\ ((undef39 + 9) <= undef28) /\ ((undef50 + 5) <= undef28) /\ ((undef40 + 4) <= undef28) /\ ((undef41 + 4) <= undef28) /\ ((undef47 + 7) <= undef29) /\ ((undef42 + 9) <= undef29) /\ ((undef43 + 9) <= undef29) /\ ((undef50 + 5) <= undef29) /\ ((undef45 + 4) <= undef29) /\ ((undef46 + 4) <= undef29) /\ ((undef47 + 5) <= undef30) /\ ((undef48 + 7) <= undef30) /\ ((undef49 + 7) <= undef30) /\ ((undef50 + 3) <= undef30) /\ (0 = 0), par{arg1 -> undef77, arg2 -> undef78, arg3 -> undef79, arg4 -> undef47, arg5 -> undef81, arg6 -> 0, arg7 -> undef50, arg8 -> undef84, arg9 -> undef85, arg10 -> undef86, arg11 -> undef87, arg12 -> undef88, arg13 -> undef89, arg14 -> undef90, arg15 -> undef91, arg16 -> undef92, arg17 -> undef93, arg18 -> undef94, arg19 -> undef95, arg20 -> undef96, arg21 -> undef97, arg22 -> undef98, arg23 -> undef99, arg24 -> undef100, arg25 -> undef101}>
<l0, l7, (undef47 > ~(1)) /\ (undef640 > 0) /\ (undef51 > ~(1)) /\ (undef639 > 0) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef32 > ~(1)) /\ (undef47 < undef31) /\ (undef129 < undef32) /\ (undef33 > ~(1)) /\ (undef130 < undef33) /\ ((undef104 - 1) <= undef26) /\ ((undef104 - 1) <= undef27) /\ ((undef104 - 1) <= undef28) /\ ((undef104 - 1) <= undef29) /\ ((undef104 - 3) <= undef30) /\ ((undef105 - 1) <= undef26) /\ ((undef105 - 1) <= undef27) /\ ((undef105 - 1) <= undef28) /\ ((undef105 - 1) <= undef29) /\ ((undef105 - 3) <= undef30) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef104 > 9) /\ (undef105 > 9) /\ ((undef47 + 7) <= undef26) /\ ((undef34 + 9) <= undef26) /\ ((undef35 + 9) <= undef26) /\ ((undef50 + 5) <= undef26) /\ ((undef47 + 7) <= undef27) /\ ((undef36 + 9) <= undef27) /\ ((undef37 + 9) <= undef27) /\ ((undef50 + 5) <= undef27) /\ ((undef47 + 7) <= undef28) /\ ((undef38 + 9) <= undef28) /\ ((undef39 + 9) <= undef28) /\ ((undef50 + 5) <= undef28) /\ ((undef40 + 4) <= undef28) /\ ((undef41 + 4) <= undef28) /\ ((undef47 + 7) <= undef29) /\ ((undef42 + 9) <= undef29) /\ ((undef43 + 9) <= undef29) /\ ((undef50 + 5) <= undef29) /\ ((undef45 + 4) <= undef29) /\ ((undef46 + 4) <= undef29) /\ ((undef47 + 5) <= undef30) /\ ((undef48 + 7) <= undef30) /\ ((undef49 + 7) <= undef30) /\ ((undef50 + 3) <= undef30) /\ (0 = 0), par{arg1 -> undef104, arg2 -> undef105, arg3 -> undef47, arg4 -> 0, arg5 -> undef50, arg6 -> undef109, arg7 -> undef110, arg8 -> undef111, arg9 -> undef112, arg10 -> undef113, arg11 -> undef114, arg12 -> undef115, arg13 -> undef116, arg14 -> undef117, arg15 -> undef118, arg16 -> undef119, arg17 -> undef120, arg18 -> undef121, arg19 -> undef122, arg20 -> undef123, arg21 -> undef124, arg22 -> undef125, arg23 -> undef126, arg24 -> undef127, arg25 -> undef128}>
<l0, l8, (undef47 > ~(1)) /\ (undef640 > 0) /\ (undef51 > ~(1)) /\ (undef639 > 0) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef32 > ~(1)) /\ (undef47 < undef31) /\ (undef133 < undef32) /\ (undef156 < undef33) /\ (undef33 > ~(1)) /\ (undef156 > 0) /\ (undef133 > 0) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef131 > 9) /\ (undef132 > 9) /\ ((undef47 + 7) <= undef26) /\ ((undef34 + 9) <= undef26) /\ ((undef35 + 9) <= undef26) /\ ((undef50 + 5) <= undef26) /\ ((undef47 + 7) <= undef27) /\ ((undef36 + 9) <= undef27) /\ ((undef37 + 9) <= undef27) /\ ((undef50 + 5) <= undef27) /\ ((undef47 + 7) <= undef28) /\ ((undef38 + 9) <= undef28) /\ ((undef39 + 9) <= undef28) /\ ((undef50 + 5) <= undef28) /\ ((undef40 + 4) <= undef28) /\ ((undef41 + 4) <= undef28) /\ ((undef47 + 7) <= undef29) /\ ((undef42 + 9) <= undef29) /\ ((undef43 + 9) <= undef29) /\ ((undef50 + 5) <= undef29) /\ ((undef45 + 4) <= undef29) /\ ((undef46 + 4) <= undef29) /\ ((undef47 + 5) <= undef30) /\ ((undef48 + 7) <= undef30) /\ ((undef49 + 7) <= undef30) /\ ((undef50 + 3) <= undef30) /\ (0 = 0), par{arg1 -> undef131, arg2 -> undef132, arg3 -> undef133, arg4 -> 0, arg5 -> 0, arg6 -> 0, arg7 -> undef133, arg8 -> undef138, arg9 -> undef47, arg10 -> undef140, arg11 -> 0, arg12 -> undef50, arg13 -> undef143, arg14 -> undef144, arg15 -> undef145, arg16 -> undef146, arg17 -> undef147, arg18 -> undef148, arg19 -> undef149, arg20 -> undef150, arg21 -> undef151, arg22 -> undef152, arg23 -> undef153, arg24 -> undef154, arg25 -> undef155}>
<l0, l9, (undef47 > ~(1)) /\ (undef640 > 0) /\ (undef51 > ~(1)) /\ (undef639 > 0) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef32 > ~(1)) /\ (undef47 < undef31) /\ (undef159 < undef32) /\ (undef182 < undef33) /\ (undef159 > 0) /\ (undef33 > ~(1)) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef157 > 9) /\ (undef158 > 9) /\ ((undef47 + 7) <= undef26) /\ ((undef34 + 9) <= undef26) /\ ((undef35 + 9) <= undef26) /\ ((undef50 + 5) <= undef26) /\ ((undef47 + 7) <= undef27) /\ ((undef36 + 9) <= undef27) /\ ((undef37 + 9) <= undef27) /\ ((undef50 + 5) <= undef27) /\ ((undef47 + 7) <= undef28) /\ ((undef38 + 9) <= undef28) /\ ((undef39 + 9) <= undef28) /\ ((undef50 + 5) <= undef28) /\ ((undef40 + 4) <= undef28) /\ ((undef41 + 4) <= undef28) /\ ((undef47 + 7) <= undef29) /\ ((undef42 + 9) <= undef29) /\ ((undef43 + 9) <= undef29) /\ ((undef50 + 5) <= undef29) /\ ((undef45 + 4) <= undef29) /\ ((undef46 + 4) <= undef29) /\ ((undef47 + 5) <= undef30) /\ ((undef48 + 7) <= undef30) /\ ((undef49 + 7) <= undef30) /\ ((undef50 + 3) <= undef30) /\ (0 = 0), par{arg1 -> undef157, arg2 -> undef158, arg3 -> undef159, arg4 -> 0, arg5 -> 0, arg6 -> 0, arg7 -> undef159, arg8 -> undef47, arg9 -> 0, arg10 -> undef50, arg11 -> undef167, arg12 -> undef168, arg13 -> undef169, arg14 -> undef170, arg15 -> undef171, arg16 -> undef172, arg17 -> undef173, arg18 -> undef174, arg19 -> undef175, arg20 -> undef176, arg21 -> undef177, arg22 -> undef178, arg23 -> undef179, arg24 -> undef180, arg25 -> undef181}>
<l0, l10, (undef47 > ~(1)) /\ (undef640 > 0) /\ (undef51 > ~(1)) /\ (undef639 > 0) /\ (undef26 > 8) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef26 > 8) /\ (undef47 >= undef31) /\ (undef27 > 8) /\ (undef28 > 8) /\ (undef29 > 8) /\ (undef30 > 6) /\ (undef383 > 10) /\ ((undef47 + 7) <= undef26) /\ ((undef34 + 9) <= undef26) /\ ((undef35 + 9) <= undef26) /\ ((undef50 + 5) <= undef26) /\ ((undef47 + 7) <= undef27) /\ ((undef36 + 9) <= undef27) /\ ((undef37 + 9) <= undef27) /\ ((undef50 + 5) <= undef27) /\ ((undef47 + 7) <= undef28) /\ ((undef38 + 9) <= undef28) /\ ((undef39 + 9) <= undef28) /\ ((undef50 + 5) <= undef28) /\ ((undef40 + 4) <= undef28) /\ ((undef41 + 4) <= undef28) /\ ((undef47 + 7) <= undef29) /\ ((undef42 + 9) <= undef29) /\ ((undef43 + 9) <= undef29) /\ ((undef50 + 5) <= undef29) /\ ((undef45 + 4) <= undef29) /\ ((undef46 + 4) <= undef29) /\ ((undef47 + 5) <= undef30) /\ ((undef48 + 7) <= undef30) /\ ((undef49 + 7) <= undef30) /\ ((undef50 + 3) <= undef30) /\ (0 = 0), par{arg1 -> undef383, arg2 -> 0, arg3 -> 0, arg4 -> undef47, arg5 -> undef47, arg6 -> undef50, arg7 -> undef389, arg8 -> undef390, arg9 -> undef391, arg10 -> undef392, arg11 -> undef393, arg12 -> undef394, arg13 -> undef395, arg14 -> undef396, arg15 -> undef397, arg16 -> undef398, arg17 -> undef399, arg18 -> undef400, arg19 -> undef401, arg20 -> undef402, arg21 -> undef403, arg22 -> undef404, arg23 -> undef405, arg24 -> undef406, arg25 -> undef407}>
<l0, l12, (undef535 > ~(1)) /\ (undef640 > 0) /\ ((undef536 - 7) <= undef639) /\ (undef639 > 0) /\ (undef536 > 7) /\ (undef536 > 9) /\ (undef2 > 9) /\ ((0 + 5) <= undef536) /\ ((0 + 3) <= undef536) /\ (undef2 > 11) /\ (undef560 > 11) /\ ((0 + 5) <= undef2) /\ ((undef21 + 9) <= undef2) /\ ((0 + 3) <= undef2) /\ ((undef22 + 9) <= undef2), par{arg1 -> undef560, arg2 -> undef535, arg3 -> undef13, arg4 -> undef11, arg5 -> undef7, arg6 -> undef12, arg7 -> undef7, arg8 -> undef567, arg9 -> 0, arg10 -> undef14, arg11 -> undef537, arg12 -> 0, arg13 -> 0, arg14 -> 0, arg15 -> 0, arg16 -> 0, arg17 -> undef537, arg18 -> undef538, arg19 -> undef538, arg20 -> 1, arg21 -> 0, arg22 -> undef581, arg23 -> undef582, arg24 -> undef583, arg25 -> 0}>
<l6, l6, (arg6 > ~(1)) /\ (arg4 > arg6) /\ (undef183 <= arg1) /\ ((undef184 - 1) <= arg2) /\ (arg1 > 9) /\ (arg2 > 9) /\ (undef183 > 9) /\ (undef184 > 9) /\ ((arg4 + 7) <= arg1) /\ ((arg3 + 10) <= arg1) /\ ((arg7 + 5) <= arg1) /\ ((arg4 + 7) <= arg2) /\ ((arg5 + 10) <= arg2) /\ ((arg7 + 5) <= arg2) /\ ((arg8 + 5) <= arg2) /\ ((arg6 + 2) <= arg2), par{arg1 -> undef183, arg2 -> undef184, arg6 -> (arg6 + 1), arg9 -> undef191, arg10 -> undef192, arg11 -> undef193, arg12 -> undef194, arg13 -> undef195, arg14 -> undef196, arg15 -> undef197, arg16 -> undef198, arg17 -> undef199, arg18 -> undef200, arg19 -> undef201, arg20 -> undef202, arg21 -> undef203, arg22 -> undef204, arg23 -> undef205, arg24 -> undef206, arg25 -> undef207}>
<l6, l10, (arg1 > 9) /\ (arg4 <= arg6) /\ (arg2 > 9) /\ (undef408 > 10) /\ ((arg4 + 7) <= arg1) /\ ((arg3 + 10) <= arg1) /\ ((arg7 + 5) <= arg1) /\ ((arg4 + 7) <= arg2) /\ ((arg5 + 10) <= arg2) /\ ((arg7 + 5) <= arg2) /\ ((arg8 + 5) <= arg2) /\ ((arg6 + 2) <= arg2), par{arg1 -> undef408, arg2 -> 0, arg3 -> 0, arg5 -> arg6, arg6 -> arg7, arg7 -> undef414, arg8 -> undef415, arg9 -> undef416, arg10 -> undef417, arg11 -> undef418, arg12 -> undef419, arg13 -> undef420, arg14 -> undef421, arg15 -> undef422, arg16 -> undef423, arg17 -> undef424, arg18 -> undef425, arg19 -> undef426, arg20 -> undef427, arg21 -> undef428, arg22 -> undef429, arg23 -> undef430, arg24 -> undef431, arg25 -> undef432}>
<l7, l7, (arg4 > ~(1)) /\ (arg3 > arg4) /\ (undef208 <= arg1) /\ (undef208 <= arg2) /\ ((undef209 - 1) <= arg2) /\ (arg1 > 9) /\ (arg2 > 9) /\ (undef208 > 9) /\ (undef209 > 9) /\ ((arg3 + 7) <= arg1) /\ ((arg5 + 5) <= arg1) /\ ((arg3 + 7) <= arg2) /\ ((arg4 + 2) <= arg2) /\ ((arg5 + 5) <= arg2), par{arg1 -> undef208, arg2 -> undef209, arg4 -> (arg4 + 1), arg6 -> undef213, arg7 -> undef214, arg8 -> undef215, arg9 -> undef216, arg10 -> undef217, arg11 -> undef218, arg12 -> undef219, arg13 -> undef220, arg14 -> undef221, arg15 -> undef222, arg16 -> undef223, arg17 -> undef224, arg18 -> undef225, arg19 -> undef226, arg20 -> undef227, arg21 -> undef228, arg22 -> undef229, arg23 -> undef230, arg24 -> undef231, arg25 -> undef232}>
<l7, l10, (arg1 > 9) /\ (arg3 <= arg4) /\ (arg2 > 9) /\ (undef433 > 10) /\ ((arg3 + 7) <= arg1) /\ ((arg5 + 5) <= arg1) /\ ((arg3 + 7) <= arg2) /\ ((arg4 + 2) <= arg2) /\ ((arg5 + 5) <= arg2), par{arg1 -> undef433, arg2 -> 0, arg3 -> 0, arg4 -> arg3, arg5 -> arg4, arg6 -> arg5, arg7 -> undef439, arg8 -> undef440, arg9 -> undef441, arg10 -> undef442, arg11 -> undef443, arg12 -> undef444, arg13 -> undef445, arg14 -> undef446, arg15 -> undef447, arg16 -> undef448, arg17 -> undef449, arg18 -> undef450, arg19 -> undef451, arg20 -> undef452, arg21 -> undef453, arg22 -> undef454, arg23 -> undef455, arg24 -> undef456, arg25 -> undef457}>
<l8, l8, (arg6 > 0) /\ (arg5 > 0) /\ (undef238 > arg6) /\ (arg6 < arg4) /\ (arg4 > 0) /\ (arg6 < arg3) /\ (undef237 < arg5) /\ (arg11 > ~(1)) /\ (arg9 > arg11) /\ (undef233 <= arg1) /\ (arg1 > 9) /\ (arg2 > 9) /\ (undef233 > 9) /\ (undef234 > 9) /\ ((arg9 + 7) <= arg1) /\ ((arg8 + 10) <= arg1) /\ ((arg12 + 5) <= arg1) /\ ((arg9 + 7) <= arg2) /\ ((arg10 + 10) <= arg2) /\ ((arg12 + 5) <= arg2) /\ ((arg13 + 5) <= arg2) /\ ((arg11 + 2) <= arg2), par{arg1 -> undef233, arg2 -> undef234, arg5 -> undef237, arg6 -> undef238, arg7 -> undef239, arg11 -> (arg11 + 1), arg14 -> undef246, arg15 -> undef247, arg16 -> undef248, arg17 -> undef249, arg18 -> undef250, arg19 -> undef251, arg20 -> undef252, arg21 -> undef253, arg22 -> undef254, arg23 -> undef255, arg24 -> undef256, arg25 -> undef257}>
<l8, l8, (undef264 < arg3) /\ (arg3 > ~(1)) /\ (undef262 < arg4) /\ (arg4 > ~(1)) /\ (arg9 > arg11) /\ (arg11 > ~(1)) /\ (undef258 <= arg1) /\ (arg1 > 11) /\ (arg2 > 11) /\ (undef258 > 11) /\ (undef259 > 11) /\ ((arg9 + 7) <= arg1) /\ ((arg8 + 10) <= arg1) /\ ((arg12 + 5) <= arg1) /\ ((arg9 + 7) <= arg2) /\ ((arg10 + 10) <= arg2) /\ ((arg12 + 5) <= arg2) /\ ((arg13 + 5) <= arg2) /\ ((arg11 + 2) <= arg2) /\ (arg3 = arg7), par{arg1 -> undef258, arg2 -> undef259, arg3 -> undef260, arg4 -> 0, arg5 -> undef262, arg6 -> 1, arg7 -> undef264, arg11 -> (arg11 + 1), arg14 -> undef271, arg15 -> undef272, arg16 -> undef273, arg17 -> undef274, arg18 -> undef275, arg19 -> undef276, arg20 -> undef277, arg21 -> undef278, arg22 -> undef279, arg23 -> undef280, arg24 -> undef281, arg25 -> undef282}>
<l8, l10, (arg1 > 9) /\ (arg9 <= arg11) /\ (arg2 > 9) /\ (undef333 > 11) /\ ((arg9 + 7) <= arg1) /\ ((arg8 + 10) <= arg1) /\ ((arg12 + 5) <= arg1) /\ ((arg9 + 7) <= arg2) /\ ((arg10 + 10) <= arg2) /\ ((arg12 + 5) <= arg2) /\ ((arg13 + 5) <= arg2) /\ ((arg11 + 2) <= arg2), par{arg1 -> undef333, arg2 -> undef334, arg3 -> arg7, arg4 -> arg9, arg5 -> arg11, arg6 -> arg12, arg7 -> undef339, arg8 -> undef340, arg9 -> undef341, arg10 -> undef342, arg11 -> undef343, arg12 -> undef344, arg13 -> undef345, arg14 -> undef346, arg15 -> undef347, arg16 -> undef348, arg17 -> undef349, arg18 -> undef350, arg19 -> undef351, arg20 -> undef352, arg21 -> undef353, arg22 -> undef354, arg23 -> undef355, arg24 -> undef356, arg25 -> undef357}>
<l9, l9, (arg6 > 0) /\ (arg5 > 0) /\ (undef288 > arg6) /\ (arg6 < arg4) /\ (arg4 > 0) /\ (arg6 < arg3) /\ (undef287 < arg5) /\ (arg9 > ~(1)) /\ (arg8 > arg9) /\ (undef283 <= arg1) /\ (arg1 > 9) /\ (arg2 > 9) /\ (undef283 > 9) /\ (undef284 > 9) /\ ((arg8 + 7) <= arg1) /\ ((arg10 + 5) <= arg1) /\ ((arg8 + 7) <= arg2) /\ ((arg9 + 2) <= arg2) /\ ((arg10 + 5) <= arg2), par{arg1 -> undef283, arg2 -> undef284, arg5 -> undef287, arg6 -> undef288, arg7 -> undef289, arg9 -> (arg9 + 1), arg11 -> undef293, arg12 -> undef294, arg13 -> undef295, arg14 -> undef296, arg15 -> undef297, arg16 -> undef298, arg17 -> undef299, arg18 -> undef300, arg19 -> undef301, arg20 -> undef302, arg21 -> undef303, arg22 -> undef304, arg23 -> undef305, arg24 -> undef306, arg25 -> undef307}>
<l9, l9, (undef314 < arg3) /\ (arg3 > ~(1)) /\ (undef312 < arg4) /\ (arg4 > ~(1)) /\ (arg8 > arg9) /\ (arg9 > ~(1)) /\ (undef308 <= arg1) /\ (arg1 > 11) /\ (arg2 > 11) /\ (undef308 > 11) /\ (undef309 > 11) /\ ((arg8 + 7) <= arg1) /\ ((arg10 + 5) <= arg1) /\ ((arg8 + 7) <= arg2) /\ ((arg9 + 2) <= arg2) /\ ((arg10 + 5) <= arg2) /\ (arg3 = arg7), par{arg1 -> undef308, arg2 -> undef309, arg3 -> undef310, arg4 -> 0, arg5 -> undef312, arg6 -> 1, arg7 -> undef314, arg9 -> (arg9 + 1), arg11 -> undef318, arg12 -> undef319, arg13 -> undef320, arg14 -> undef321, arg15 -> undef322, arg16 -> undef323, arg17 -> undef324, arg18 -> undef325, arg19 -> undef326, arg20 -> undef327, arg21 -> undef328, arg22 -> undef329, arg23 -> undef330, arg24 -> undef331, arg25 -> undef332}>
<l9, l10, (arg1 > 9) /\ (arg8 <= arg9) /\ (arg2 > 9) /\ (undef358 > 11) /\ ((arg8 + 7) <= arg1) /\ ((arg10 + 5) <= arg1) /\ ((arg8 + 7) <= arg2) /\ ((arg9 + 2) <= arg2) /\ ((arg10 + 5) <= arg2), par{arg1 -> undef358, arg2 -> undef359, arg3 -> arg7, arg4 -> arg8, arg5 -> arg9, arg6 -> arg10, arg7 -> undef364, arg8 -> undef365, arg9 -> undef366, arg10 -> undef367, arg11 -> undef368, arg12 -> undef369, arg13 -> undef370, arg14 -> undef371, arg15 -> undef372, arg16 -> undef373, arg17 -> undef374, arg18 -> undef375, arg19 -> undef376, arg20 -> undef377, arg21 -> undef378, arg22 -> undef379, arg23 -> undef380, arg24 -> undef381, arg25 -> undef382}>
<l10, l10, (arg1 > 9) /\ (arg5 > 0) /\ (undef458 > 9) /\ (undef459 > ~(1)) /\ ((undef460 + 8) <= arg1) /\ ((arg4 + 9) <= arg1) /\ ((undef462 + 10) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg5 + 4) <= arg1) /\ ((arg8 + 6) <= arg1) /\ ((arg7 + 6) <= arg1) /\ (undef458 > 9) /\ (undef459 > 0) /\ (undef510 > 9) /\ ((undef460 + 8) <= undef458) /\ ((arg4 + 9) <= undef458) /\ ((undef462 + 10) <= undef458) /\ ((arg6 + 7) <= undef458) /\ (((arg5 - 1) + 4) <= undef458), par{arg1 -> undef510, arg2 -> 0, arg3 -> 0, arg5 -> (arg5 - 1), arg6 -> arg6, arg7 -> undef516, arg8 -> undef517, arg9 -> undef518, arg10 -> undef519, arg11 -> undef520, arg12 -> undef521, arg13 -> undef522, arg14 -> undef523, arg15 -> undef524, arg16 -> undef525, arg17 -> undef526, arg18 -> undef527, arg19 -> undef528, arg20 -> undef529, arg21 -> undef530, arg22 -> undef531, arg23 -> undef532, arg24 -> undef533, arg25 -> undef534}>
<l10, l10, (arg2 > 0) /\ (arg3 > 0) /\ (arg5 > 0) /\ (undef508 < arg3) /\ (undef509 > arg2) /\ (arg1 > 9) /\ (undef483 > 9) /\ (undef484 > ~(1)) /\ ((undef485 + 8) <= arg1) /\ ((arg4 + 9) <= arg1) /\ ((undef487 + 10) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg5 + 4) <= arg1) /\ ((arg8 + 6) <= arg1) /\ ((arg7 + 6) <= arg1) /\ (undef483 > 9) /\ (undef484 > 0) /\ (undef510 > 9) /\ ((undef485 + 8) <= undef483) /\ ((arg4 + 9) <= undef483) /\ ((undef487 + 10) <= undef483) /\ ((arg6 + 7) <= undef483) /\ (((arg5 - 1) + 4) <= undef483), par{arg1 -> undef510, arg2 -> 0, arg3 -> 0, arg5 -> (arg5 - 1), arg6 -> arg6, arg7 -> undef516, arg8 -> undef517, arg9 -> undef518, arg10 -> undef519, arg11 -> undef520, arg12 -> undef521, arg13 -> undef522, arg14 -> undef523, arg15 -> undef524, arg16 -> undef525, arg17 -> undef526, arg18 -> undef527, arg19 -> undef528, arg20 -> undef529, arg21 -> undef530, arg22 -> undef531, arg23 -> undef532, arg24 -> undef533, arg25 -> undef534}>
<l12, l12, (arg2 > 0) /\ (undef610 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef610) /\ (arg10 > 0) /\ (arg4 > 0) /\ (arg13 > 0) /\ (arg11 > 0) /\ (arg12 > 0) /\ (undef611 > ~(1)) /\ (arg9 > 0) /\ (arg5 > 0) /\ (arg19 > 0) /\ (arg14 > 0) /\ (arg18 > 0) /\ (arg17 > 0) /\ (arg15 > 0) /\ (arg16 > 0) /\ (arg25 > ~(1)) /\ (arg21 > ~(1)) /\ (arg1 > 9) /\ (undef585 > 9) /\ ((arg21 + 5) <= arg1) /\ ((arg22 + 9) <= arg1) /\ ((arg23 + 9) <= arg1) /\ ((arg25 + 3) <= arg1) /\ ((arg24 + 9) <= arg1), par{arg1 -> undef585, arg2 -> (arg2 - 1), arg4 -> undef588, arg5 -> undef589, arg9 -> undef593, arg11 -> undef595, arg13 -> undef597, arg14 -> undef598, arg15 -> undef599, arg16 -> undef600, arg17 -> undef601, arg18 -> undef602, arg19 -> undef603, arg20 -> (arg20 + 1), arg21 -> (arg21 + 1), arg22 -> undef606, arg23 -> undef607, arg24 -> undef608, arg25 -> (arg25 + 1)}>
<l12, l12, (arg2 > 0) /\ (undef637 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef637) /\ (arg10 > 0) /\ (arg12 > 0) /\ (undef638 > ~(1)) /\ (arg19 > 0) /\ (arg18 > 0) /\ (arg17 > 0) /\ (arg8 > 0) /\ (arg25 > ~(1)) /\ (arg21 > ~(1)) /\ (arg1 > 11) /\ (undef612 > 13) /\ ((arg21 + 5) <= arg1) /\ ((arg22 + 9) <= arg1) /\ ((arg23 + 9) <= arg1) /\ ((arg25 + 3) <= arg1) /\ ((arg24 + 9) <= arg1) /\ (arg8 = arg9) /\ (arg10 = arg11) /\ (arg12 = arg13) /\ (arg7 = arg16), par{arg1 -> undef612, arg2 -> (arg2 - 1), arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef617, arg7 -> undef618, arg9 -> undef620, arg11 -> undef622, arg13 -> 0, arg14 -> 2, arg15 -> undef626, arg16 -> undef627, arg17 -> undef628, arg18 -> undef629, arg19 -> undef630, arg20 -> (arg20 + 1), arg21 -> (arg21 + 1), arg22 -> undef633, arg23 -> undef634, arg24 -> undef635, arg25 -> (arg25 + 1)}>

Fresh variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef21, undef22, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef71, undef72, undef74, undef75, undef77, undef78, undef79, undef81, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef96, undef97, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef138, undef140, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef213, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef221, undef222, undef223, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef237, undef238, undef239, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, undef262, undef264, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef284, undef287, undef288, undef289, undef293, undef294, undef295, undef296, undef297, undef298, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef309, undef310, undef312, undef314, undef318, undef319, undef320, undef321, undef322, undef323, undef324, undef325, undef326, undef327, undef328, undef329, undef330, undef331, undef332, undef333, undef334, undef339, undef340, undef341, undef342, undef343, undef344, undef345, undef346, undef347, undef348, undef349, undef350, undef351, undef352, undef353, undef354, undef355, undef356, undef357, undef358, undef359, undef364, undef365, undef366, undef367, undef368, undef369, undef370, undef371, undef372, undef373, undef374, undef375, undef376, undef377, undef378, undef379, undef380, undef381, undef382, undef383, undef389, undef390, undef391, undef392, undef393, undef394, undef395, undef396, undef397, undef398, undef399, undef400, undef401, undef402, undef403, undef404, undef405, undef406, undef407, undef408, undef414, undef415, undef416, undef417, undef418, undef419, undef420, undef421, undef422, undef423, undef424, undef425, undef426, undef427, undef428, undef429, undef430, undef431, undef432, undef433, undef439, undef440, undef441, undef442, undef443, undef444, undef445, undef446, undef447, undef448, undef449, undef450, undef451, undef452, undef453, undef454, undef455, undef456, undef457, undef458, undef459, undef460, undef462, undef465, undef466, undef467, undef468, undef469, undef470, undef471, undef472, undef473, undef474, undef475, undef476, undef477, undef478, undef479, undef480, undef481, undef482, undef483, undef484, undef485, undef487, undef490, undef491, undef492, undef493, undef494, undef495, undef496, undef497, undef498, undef499, undef500, undef501, undef502, undef503, undef504, undef505, undef506, undef507, undef508, undef509, undef510, undef516, undef517, undef518, undef519, undef520, undef521, undef522, undef523, undef524, undef525, undef526, undef527, undef528, undef529, undef530, undef531, undef532, undef533, undef534, undef535, undef536, undef537, undef538, undef542, undef543, undef544, undef545, undef546, undef547, undef548, undef549, undef550, undef551, undef552, undef553, undef554, undef555, undef556, undef557, undef558, undef559, undef560, undef567, undef581, undef582, undef583, undef585, undef588, undef589, undef593, undef595, undef597, undef598, undef599, undef600, undef601, undef602, undef603, undef606, undef607, undef608, undef610, undef611, undef612, undef617, undef618, undef620, undef622, undef626, undef627, undef628, undef629, undef630, undef633, undef634, undef635, undef637, undef638, undef639, undef640, undef641, undef642, undef643, undef644, undef645, undef646, undef647, undef648, undef649, undef650, undef651, undef652, undef653, undef654, undef655, undef656, undef657, undef658, undef659, undef660, undef661, undef662, undef663, 

Undef variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef21, undef22, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef71, undef72, undef74, undef75, undef77, undef78, undef79, undef81, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef96, undef97, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef138, undef140, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef213, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef221, undef222, undef223, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef237, undef238, undef239, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, undef262, undef264, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef284, undef287, undef288, undef289, undef293, undef294, undef295, undef296, undef297, undef298, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef309, undef310, undef312, undef314, undef318, undef319, undef320, undef321, undef322, undef323, undef324, undef325, undef326, undef327, undef328, undef329, undef330, undef331, undef332, undef333, undef334, undef339, undef340, undef341, undef342, undef343, undef344, undef345, undef346, undef347, undef348, undef349, undef350, undef351, undef352, undef353, undef354, undef355, undef356, undef357, undef358, undef359, undef364, undef365, undef366, undef367, undef368, undef369, undef370, undef371, undef372, undef373, undef374, undef375, undef376, undef377, undef378, undef379, undef380, undef381, undef382, undef383, undef389, undef390, undef391, undef392, undef393, undef394, undef395, undef396, undef397, undef398, undef399, undef400, undef401, undef402, undef403, undef404, undef405, undef406, undef407, undef408, undef414, undef415, undef416, undef417, undef418, undef419, undef420, undef421, undef422, undef423, undef424, undef425, undef426, undef427, undef428, undef429, undef430, undef431, undef432, undef433, undef439, undef440, undef441, undef442, undef443, undef444, undef445, undef446, undef447, undef448, undef449, undef450, undef451, undef452, undef453, undef454, undef455, undef456, undef457, undef458, undef459, undef460, undef462, undef465, undef466, undef467, undef468, undef469, undef470, undef471, undef472, undef473, undef474, undef475, undef476, undef477, undef478, undef479, undef480, undef481, undef482, undef483, undef484, undef485, undef487, undef490, undef491, undef492, undef493, undef494, undef495, undef496, undef497, undef498, undef499, undef500, undef501, undef502, undef503, undef504, undef505, undef506, undef507, undef508, undef509, undef510, undef516, undef517, undef518, undef519, undef520, undef521, undef522, undef523, undef524, undef525, undef526, undef527, undef528, undef529, undef530, undef531, undef532, undef533, undef534, undef535, undef536, undef537, undef538, undef542, undef543, undef544, undef545, undef546, undef547, undef548, undef549, undef550, undef551, undef552, undef553, undef554, undef555, undef556, undef557, undef558, undef559, undef560, undef567, undef581, undef582, undef583, undef585, undef588, undef589, undef593, undef595, undef597, undef598, undef599, undef600, undef601, undef602, undef603, undef606, undef607, undef608, undef610, undef611, undef612, undef617, undef618, undef620, undef622, undef626, undef627, undef628, undef629, undef630, undef633, undef634, undef635, undef637, undef638, undef639, undef640, undef641, undef642, undef643, undef644, undef645, undef646, undef647, undef648, undef649, undef650, undef651, undef652, undef653, undef654, undef655, undef656, undef657, undef658, undef659, undef660, undef661, undef662, undef663, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l12, l12, 9 + arg22 <= arg1 /\ 9 + arg23 <= arg1 /\ 9 + arg24 <= arg1 /\ 5 + arg21 <= arg1 /\ 3 + arg25 <= arg1 /\ 0 <= arg20 /\ 0 <= arg21 /\ 0 <= arg25 /\ 0 <= undef610 /\ 0 <= undef611 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg4 /\ 1 <= arg5 /\ 1 <= arg6 /\ 1 <= arg9 /\ 1 <= arg10 /\ 1 <= arg11 /\ 1 <= arg12 /\ 1 <= arg13 /\ 1 <= arg14 /\ 1 <= arg15 /\ 1 <= arg16 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef610 /\ 10 <= arg1 /\ 10 <= undef585, {arg1 -> undef585, arg2 -> -1 + arg2, arg4 -> undef588, arg5 -> undef589, arg9 -> undef593, arg11 -> undef595, arg13 -> undef597, arg14 -> undef598, arg15 -> undef599, arg16 -> undef600, arg17 -> undef601, arg18 -> undef602, arg19 -> undef603, arg20 -> 1 + arg20, arg21 -> 1 + arg21, arg22 -> undef606, arg23 -> undef607, arg24 -> undef608, arg25 -> 1 + arg25, rest remain the same}>
<l12, l12, 9 + arg22 <= arg1 /\ 9 + arg23 <= arg1 /\ 9 + arg24 <= arg1 /\ 5 + arg21 <= arg1 /\ 3 + arg25 <= arg1 /\ 0 <= arg20 /\ 0 <= arg21 /\ 0 <= arg25 /\ 0 <= undef637 /\ 0 <= undef638 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg6 /\ 1 <= arg8 /\ 1 <= arg10 /\ 1 <= arg12 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef637 /\ 12 <= arg1 /\ 14 <= undef612 /\ arg7 = arg16 /\ arg8 = arg9 /\ arg10 = arg11 /\ arg12 = arg13, {arg1 -> undef612, arg2 -> -1 + arg2, arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef617, arg7 -> undef618, arg9 -> undef620, arg11 -> undef622, arg13 -> 0, arg14 -> 2, arg15 -> undef626, arg16 -> undef627, arg17 -> undef628, arg18 -> undef629, arg19 -> undef630, arg20 -> 1 + arg20, arg21 -> 1 + arg21, arg22 -> undef633, arg23 -> undef634, arg24 -> undef635, arg25 -> 1 + arg25, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23, arg24, arg25, arg7, arg8

Graph 2:
Transitions:
<l9, l9, 5 + arg10 <= arg1 /\ 5 + arg10 <= arg2 /\ undef283 <= arg1 /\ 0 <= arg9 /\ 1 + arg6 <= arg3 /\ 1 <= arg4 /\ 1 + arg6 <= arg4 /\ 1 <= arg5 /\ 1 + undef287 <= arg5 /\ 1 + arg6 <= undef288 /\ 1 <= arg6 /\ 1 + arg9 <= arg8 /\ 7 + arg8 <= arg1 /\ 7 + arg8 <= arg2 /\ 10 <= arg1 /\ 10 <= arg2 /\ 10 <= undef283 /\ 10 <= undef284 /\ 2 + arg9 <= arg2, {arg1 -> undef283, arg2 -> undef284, arg5 -> undef287, arg6 -> undef288, arg7 -> undef289, arg9 -> 1 + arg9, arg11 -> undef293, arg12 -> undef294, arg13 -> undef295, arg14 -> undef296, arg15 -> undef297, arg16 -> undef298, arg17 -> undef299, arg18 -> undef300, arg19 -> undef301, arg20 -> undef302, arg21 -> undef303, arg22 -> undef304, arg23 -> undef305, arg24 -> undef306, arg25 -> undef307, rest remain the same}>
<l9, l9, 5 + arg10 <= arg1 /\ 5 + arg10 <= arg2 /\ undef308 <= arg1 /\ 0 <= arg3 /\ 0 <= arg4 /\ 0 <= arg9 /\ 1 + undef314 <= arg3 /\ 1 + undef312 <= arg4 /\ 1 + arg9 <= arg8 /\ 7 + arg8 <= arg1 /\ 7 + arg8 <= arg2 /\ 2 + arg9 <= arg2 /\ 12 <= arg1 /\ 12 <= arg2 /\ 12 <= undef308 /\ 12 <= undef309 /\ arg3 = arg7, {arg1 -> undef308, arg2 -> undef309, arg3 -> undef310, arg4 -> 0, arg5 -> undef312, arg6 -> 1, arg7 -> undef314, arg9 -> 1 + arg9, arg11 -> undef318, arg12 -> undef319, arg13 -> undef320, arg14 -> undef321, arg15 -> undef322, arg16 -> undef323, arg17 -> undef324, arg18 -> undef325, arg19 -> undef326, arg20 -> undef327, arg21 -> undef328, arg22 -> undef329, arg23 -> undef330, arg24 -> undef331, arg25 -> undef332, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23, arg24, arg25

Graph 3:
Transitions:
<l8, l8, 5 + arg12 <= arg1 /\ 5 + arg12 <= arg2 /\ 5 + arg13 <= arg2 /\ undef233 <= arg1 /\ 0 <= arg11 /\ 1 + arg6 <= arg3 /\ 1 <= arg4 /\ 1 + arg6 <= arg4 /\ 1 <= arg5 /\ 1 + undef237 <= arg5 /\ 1 + arg6 <= undef238 /\ 1 <= arg6 /\ 1 + arg11 <= arg9 /\ 7 + arg9 <= arg1 /\ 7 + arg9 <= arg2 /\ 10 <= arg1 /\ 10 + arg8 <= arg1 /\ 10 <= arg2 /\ 10 + arg10 <= arg2 /\ 10 <= undef233 /\ 10 <= undef234 /\ 2 + arg11 <= arg2, {arg1 -> undef233, arg2 -> undef234, arg5 -> undef237, arg6 -> undef238, arg7 -> undef239, arg11 -> 1 + arg11, arg14 -> undef246, arg15 -> undef247, arg16 -> undef248, arg17 -> undef249, arg18 -> undef250, arg19 -> undef251, arg20 -> undef252, arg21 -> undef253, arg22 -> undef254, arg23 -> undef255, arg24 -> undef256, arg25 -> undef257, rest remain the same}>
<l8, l8, 5 + arg12 <= arg1 /\ 5 + arg12 <= arg2 /\ 5 + arg13 <= arg2 /\ undef258 <= arg1 /\ 0 <= arg3 /\ 0 <= arg4 /\ 0 <= arg11 /\ 1 + undef264 <= arg3 /\ 1 + undef262 <= arg4 /\ 1 + arg11 <= arg9 /\ 7 + arg9 <= arg1 /\ 7 + arg9 <= arg2 /\ 10 + arg8 <= arg1 /\ 10 + arg10 <= arg2 /\ 2 + arg11 <= arg2 /\ 12 <= arg1 /\ 12 <= arg2 /\ 12 <= undef258 /\ 12 <= undef259 /\ arg3 = arg7, {arg1 -> undef258, arg2 -> undef259, arg3 -> undef260, arg4 -> 0, arg5 -> undef262, arg6 -> 1, arg7 -> undef264, arg11 -> 1 + arg11, arg14 -> undef271, arg15 -> undef272, arg16 -> undef273, arg17 -> undef274, arg18 -> undef275, arg19 -> undef276, arg20 -> undef277, arg21 -> undef278, arg22 -> undef279, arg23 -> undef280, arg24 -> undef281, arg25 -> undef282, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23, arg24, arg25

Graph 4:
Transitions:
<l7, l7, 5 + arg5 <= arg1 /\ 5 + arg5 <= arg2 /\ undef208 <= arg1 /\ undef208 <= arg2 /\ 0 <= arg4 /\ 1 + arg4 <= arg3 /\ undef209 <= 1 + arg2 /\ 7 + arg3 <= arg1 /\ 7 + arg3 <= arg2 /\ 10 <= arg1 /\ 10 <= arg2 /\ 10 <= undef208 /\ 10 <= undef209 /\ 2 + arg4 <= arg2, {arg1 -> undef208, arg2 -> undef209, arg4 -> 1 + arg4, arg6 -> undef213, arg7 -> undef214, arg8 -> undef215, arg9 -> undef216, arg10 -> undef217, arg11 -> undef218, arg12 -> undef219, arg13 -> undef220, arg14 -> undef221, arg15 -> undef222, arg16 -> undef223, arg17 -> undef224, arg18 -> undef225, arg19 -> undef226, arg20 -> undef227, arg21 -> undef228, arg22 -> undef229, arg23 -> undef230, arg24 -> undef231, arg25 -> undef232, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23, arg24, arg25

Graph 5:
Transitions:
<l6, l6, 5 + arg7 <= arg1 /\ 5 + arg7 <= arg2 /\ 5 + arg8 <= arg2 /\ undef183 <= arg1 /\ 0 <= arg6 /\ 1 + arg6 <= arg4 /\ undef184 <= 1 + arg2 /\ 7 + arg4 <= arg1 /\ 7 + arg4 <= arg2 /\ 10 <= arg1 /\ 10 + arg3 <= arg1 /\ 10 <= arg2 /\ 10 + arg5 <= arg2 /\ 10 <= undef183 /\ 10 <= undef184 /\ 2 + arg6 <= arg2, {arg1 -> undef183, arg2 -> undef184, arg6 -> 1 + arg6, arg9 -> undef191, arg10 -> undef192, arg11 -> undef193, arg12 -> undef194, arg13 -> undef195, arg14 -> undef196, arg15 -> undef197, arg16 -> undef198, arg17 -> undef199, arg18 -> undef200, arg19 -> undef201, arg20 -> undef202, arg21 -> undef203, arg22 -> undef204, arg23 -> undef205, arg24 -> undef206, arg25 -> undef207, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23, arg24, arg25

Graph 6:
Transitions:
<l10, l10, 9 + arg4 <= arg1 /\ 9 + arg4 <= undef458 /\ 3 + arg5 <= undef458 /\ 1 <= arg5 /\ 1 <= undef459 /\ 8 + undef460 <= arg1 /\ 8 + undef460 <= undef458 /\ 6 + arg7 <= arg1 /\ 6 + arg8 <= arg1 /\ 7 + arg6 <= arg1 /\ 7 + arg6 <= undef458 /\ 4 + arg5 <= arg1 /\ 10 <= arg1 /\ 10 + undef462 <= arg1 /\ 10 <= undef458 /\ 10 + undef462 <= undef458 /\ 10 <= undef510, {arg1 -> undef510, arg2 -> 0, arg3 -> 0, arg5 -> -1 + arg5, arg7 -> undef516, arg8 -> undef517, arg9 -> undef518, arg10 -> undef519, arg11 -> undef520, arg12 -> undef521, arg13 -> undef522, arg14 -> undef523, arg15 -> undef524, arg16 -> undef525, arg17 -> undef526, arg18 -> undef527, arg19 -> undef528, arg20 -> undef529, arg21 -> undef530, arg22 -> undef531, arg23 -> undef532, arg24 -> undef533, arg25 -> undef534, rest remain the same}>
<l10, l10, 9 + arg4 <= arg1 /\ 9 + arg4 <= undef483 /\ 3 + arg5 <= undef483 /\ 1 + arg2 <= undef509 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef508 <= arg3 /\ 1 <= arg5 /\ 1 <= undef484 /\ 8 + undef485 <= arg1 /\ 8 + undef485 <= undef483 /\ 6 + arg7 <= arg1 /\ 6 + arg8 <= arg1 /\ 7 + arg6 <= arg1 /\ 7 + arg6 <= undef483 /\ 4 + arg5 <= arg1 /\ 10 <= arg1 /\ 10 + undef487 <= arg1 /\ 10 <= undef483 /\ 10 + undef487 <= undef483 /\ 10 <= undef510, {arg1 -> undef510, arg2 -> 0, arg3 -> 0, arg5 -> -1 + arg5, arg7 -> undef516, arg8 -> undef517, arg9 -> undef518, arg10 -> undef519, arg11 -> undef520, arg12 -> undef521, arg13 -> undef522, arg14 -> undef523, arg15 -> undef524, arg16 -> undef525, arg17 -> undef526, arg18 -> undef527, arg19 -> undef528, arg20 -> undef529, arg21 -> undef530, arg22 -> undef531, arg23 -> undef532, arg24 -> undef533, arg25 -> undef534, rest remain the same}>
Variables:
arg1, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23, arg24, arg25, arg2, arg3

Precedence: 
Graph 0

Graph 1
<l0, l12, 9 + undef21 <= undef2 /\ 9 + undef22 <= undef2 /\ 0 <= undef535 /\ 1 <= undef639 /\ 1 <= undef640 /\ 10 <= undef536 /\ undef536 <= 7 + undef639 /\ 12 <= undef2 /\ 12 <= undef560, {arg1 -> undef560, arg2 -> undef535, arg3 -> undef13, arg4 -> undef11, arg5 -> undef7, arg6 -> undef12, arg7 -> undef7, arg8 -> undef567, arg9 -> 0, arg10 -> undef14, arg11 -> undef537, arg12 -> 0, arg13 -> 0, arg14 -> 0, arg15 -> 0, arg16 -> 0, arg17 -> undef537, arg18 -> undef538, arg19 -> undef538, arg20 -> 1, arg21 -> 0, arg22 -> undef581, arg23 -> undef582, arg24 -> undef583, arg25 -> 0, rest remain the same}>

Graph 2
<l0, l9, 9 <= undef26 /\ 9 + undef34 <= undef26 /\ 9 + undef35 <= undef26 /\ 9 <= undef27 /\ 9 + undef36 <= undef27 /\ 9 + undef37 <= undef27 /\ 9 <= undef28 /\ 9 + undef38 <= undef28 /\ 9 + undef39 <= undef28 /\ 9 <= undef29 /\ 9 + undef42 <= undef29 /\ 9 + undef43 <= undef29 /\ 5 + undef50 <= undef26 /\ 5 + undef50 <= undef27 /\ 5 + undef50 <= undef28 /\ 5 + undef50 <= undef29 /\ 5 + undef47 <= undef30 /\ 3 + undef50 <= undef30 /\ 0 <= undef32 /\ 0 <= undef33 /\ 0 <= undef47 /\ 0 <= undef51 /\ 1 + undef47 <= undef31 /\ 1 + undef159 <= undef32 /\ 1 + undef182 <= undef33 /\ 1 <= undef159 /\ 1 <= undef639 /\ 1 <= undef640 /\ 7 + undef47 <= undef26 /\ 7 + undef47 <= undef27 /\ 7 + undef47 <= undef28 /\ 7 + undef47 <= undef29 /\ 7 <= undef30 /\ 7 + undef48 <= undef30 /\ 7 + undef49 <= undef30 /\ 4 + undef40 <= undef28 /\ 4 + undef41 <= undef28 /\ 4 + undef45 <= undef29 /\ 4 + undef46 <= undef29 /\ 10 <= undef157 /\ 10 <= undef158, {arg1 -> undef157, arg2 -> undef158, arg3 -> undef159, arg4 -> 0, arg5 -> 0, arg6 -> 0, arg7 -> undef159, arg8 -> undef47, arg9 -> 0, arg10 -> undef50, arg11 -> undef167, arg12 -> undef168, arg13 -> undef169, arg14 -> undef170, arg15 -> undef171, arg16 -> undef172, arg17 -> undef173, arg18 -> undef174, arg19 -> undef175, arg20 -> undef176, arg21 -> undef177, arg22 -> undef178, arg23 -> undef179, arg24 -> undef180, arg25 -> undef181, rest remain the same}>

Graph 3
<l0, l8, 9 <= undef26 /\ 9 + undef34 <= undef26 /\ 9 + undef35 <= undef26 /\ 9 <= undef27 /\ 9 + undef36 <= undef27 /\ 9 + undef37 <= undef27 /\ 9 <= undef28 /\ 9 + undef38 <= undef28 /\ 9 + undef39 <= undef28 /\ 9 <= undef29 /\ 9 + undef42 <= undef29 /\ 9 + undef43 <= undef29 /\ 5 + undef50 <= undef26 /\ 5 + undef50 <= undef27 /\ 5 + undef50 <= undef28 /\ 5 + undef50 <= undef29 /\ 5 + undef47 <= undef30 /\ 3 + undef50 <= undef30 /\ 0 <= undef32 /\ 0 <= undef33 /\ 0 <= undef47 /\ 0 <= undef51 /\ 1 + undef47 <= undef31 /\ 1 + undef133 <= undef32 /\ 1 + undef156 <= undef33 /\ 1 <= undef133 /\ 1 <= undef156 /\ 1 <= undef639 /\ 1 <= undef640 /\ 7 + undef47 <= undef26 /\ 7 + undef47 <= undef27 /\ 7 + undef47 <= undef28 /\ 7 + undef47 <= undef29 /\ 7 <= undef30 /\ 7 + undef48 <= undef30 /\ 7 + undef49 <= undef30 /\ 4 + undef40 <= undef28 /\ 4 + undef41 <= undef28 /\ 4 + undef45 <= undef29 /\ 4 + undef46 <= undef29 /\ 10 <= undef131 /\ 10 <= undef132, {arg1 -> undef131, arg2 -> undef132, arg3 -> undef133, arg4 -> 0, arg5 -> 0, arg6 -> 0, arg7 -> undef133, arg8 -> undef138, arg9 -> undef47, arg10 -> undef140, arg11 -> 0, arg12 -> undef50, arg13 -> undef143, arg14 -> undef144, arg15 -> undef145, arg16 -> undef146, arg17 -> undef147, arg18 -> undef148, arg19 -> undef149, arg20 -> undef150, arg21 -> undef151, arg22 -> undef152, arg23 -> undef153, arg24 -> undef154, arg25 -> undef155, rest remain the same}>

Graph 4
<l0, l7, 9 <= undef26 /\ 9 + undef34 <= undef26 /\ 9 + undef35 <= undef26 /\ 9 <= undef27 /\ 9 + undef36 <= undef27 /\ 9 + undef37 <= undef27 /\ 9 <= undef28 /\ 9 + undef38 <= undef28 /\ 9 + undef39 <= undef28 /\ 9 <= undef29 /\ 9 + undef42 <= undef29 /\ 9 + undef43 <= undef29 /\ 5 + undef50 <= undef26 /\ 5 + undef50 <= undef27 /\ 5 + undef50 <= undef28 /\ 5 + undef50 <= undef29 /\ 5 + undef47 <= undef30 /\ 3 + undef50 <= undef30 /\ 0 <= undef32 /\ 0 <= undef33 /\ 0 <= undef47 /\ 0 <= undef51 /\ 1 + undef47 <= undef31 /\ 1 + undef129 <= undef32 /\ 1 + undef130 <= undef33 /\ 1 <= undef639 /\ 1 <= undef640 /\ undef104 <= 1 + undef26 /\ undef105 <= 1 + undef26 /\ undef104 <= 1 + undef27 /\ undef105 <= 1 + undef27 /\ undef104 <= 1 + undef28 /\ undef105 <= 1 + undef28 /\ undef104 <= 1 + undef29 /\ undef105 <= 1 + undef29 /\ 7 + undef47 <= undef26 /\ 7 + undef47 <= undef27 /\ 7 + undef47 <= undef28 /\ 7 + undef47 <= undef29 /\ 7 <= undef30 /\ 7 + undef48 <= undef30 /\ 7 + undef49 <= undef30 /\ 4 + undef40 <= undef28 /\ 4 + undef41 <= undef28 /\ 4 + undef45 <= undef29 /\ 4 + undef46 <= undef29 /\ 10 <= undef104 /\ 10 <= undef105 /\ undef104 <= 3 + undef30 /\ undef105 <= 3 + undef30, {arg1 -> undef104, arg2 -> undef105, arg3 -> undef47, arg4 -> 0, arg5 -> undef50, arg6 -> undef109, arg7 -> undef110, arg8 -> undef111, arg9 -> undef112, arg10 -> undef113, arg11 -> undef114, arg12 -> undef115, arg13 -> undef116, arg14 -> undef117, arg15 -> undef118, arg16 -> undef119, arg17 -> undef120, arg18 -> undef121, arg19 -> undef122, arg20 -> undef123, arg21 -> undef124, arg22 -> undef125, arg23 -> undef126, arg24 -> undef127, arg25 -> undef128, rest remain the same}>

Graph 5
<l0, l6, 9 <= undef26 /\ 9 + undef34 <= undef26 /\ 9 + undef35 <= undef26 /\ 9 <= undef27 /\ 9 + undef36 <= undef27 /\ 9 + undef37 <= undef27 /\ 9 <= undef28 /\ 9 + undef38 <= undef28 /\ 9 + undef39 <= undef28 /\ 9 <= undef29 /\ 9 + undef42 <= undef29 /\ 9 + undef43 <= undef29 /\ 5 + undef50 <= undef26 /\ 5 + undef50 <= undef27 /\ 5 + undef50 <= undef28 /\ 5 + undef50 <= undef29 /\ 5 + undef47 <= undef30 /\ 3 + undef50 <= undef30 /\ 0 <= undef32 /\ 0 <= undef33 /\ 0 <= undef47 /\ 0 <= undef51 /\ 1 + undef47 <= undef31 /\ 1 + undef102 <= undef32 /\ 1 + undef103 <= undef33 /\ 1 <= undef103 /\ 1 <= undef639 /\ 1 <= undef640 /\ 7 + undef47 <= undef26 /\ 7 + undef47 <= undef27 /\ 7 + undef47 <= undef28 /\ 7 + undef47 <= undef29 /\ 7 <= undef30 /\ 7 + undef48 <= undef30 /\ 7 + undef49 <= undef30 /\ 4 + undef40 <= undef28 /\ 4 + undef41 <= undef28 /\ 4 + undef45 <= undef29 /\ 4 + undef46 <= undef29 /\ 10 <= undef77 /\ 10 <= undef78, {arg1 -> undef77, arg2 -> undef78, arg3 -> undef79, arg4 -> undef47, arg5 -> undef81, arg6 -> 0, arg7 -> undef50, arg8 -> undef84, arg9 -> undef85, arg10 -> undef86, arg11 -> undef87, arg12 -> undef88, arg13 -> undef89, arg14 -> undef90, arg15 -> undef91, arg16 -> undef92, arg17 -> undef93, arg18 -> undef94, arg19 -> undef95, arg20 -> undef96, arg21 -> undef97, arg22 -> undef98, arg23 -> undef99, arg24 -> undef100, arg25 -> undef101, rest remain the same}>

Graph 6
<l0, l10, 9 <= undef26 /\ 9 + undef34 <= undef26 /\ 9 + undef35 <= undef26 /\ 9 <= undef27 /\ 9 + undef36 <= undef27 /\ 9 + undef37 <= undef27 /\ 9 <= undef28 /\ 9 + undef38 <= undef28 /\ 9 + undef39 <= undef28 /\ 9 <= undef29 /\ 9 + undef42 <= undef29 /\ 9 + undef43 <= undef29 /\ 5 + undef50 <= undef26 /\ 5 + undef50 <= undef27 /\ 5 + undef50 <= undef28 /\ 5 + undef50 <= undef29 /\ 5 + undef47 <= undef30 /\ 3 + undef50 <= undef30 /\ undef31 <= undef47 /\ 0 <= undef47 /\ 0 <= undef51 /\ 1 <= undef639 /\ 1 <= undef640 /\ 7 + undef47 <= undef26 /\ 7 + undef47 <= undef27 /\ 7 + undef47 <= undef28 /\ 7 + undef47 <= undef29 /\ 7 <= undef30 /\ 7 + undef48 <= undef30 /\ 7 + undef49 <= undef30 /\ 4 + undef40 <= undef28 /\ 4 + undef41 <= undef28 /\ 4 + undef45 <= undef29 /\ 4 + undef46 <= undef29 /\ 11 <= undef383, {arg1 -> undef383, arg2 -> 0, arg3 -> 0, arg4 -> undef47, arg5 -> undef47, arg6 -> undef50, arg7 -> undef389, arg8 -> undef390, arg9 -> undef391, arg10 -> undef392, arg11 -> undef393, arg12 -> undef394, arg13 -> undef395, arg14 -> undef396, arg15 -> undef397, arg16 -> undef398, arg17 -> undef399, arg18 -> undef400, arg19 -> undef401, arg20 -> undef402, arg21 -> undef403, arg22 -> undef404, arg23 -> undef405, arg24 -> undef406, arg25 -> undef407, rest remain the same}>
<l6, l10, 5 + arg7 <= arg1 /\ 5 + arg7 <= arg2 /\ 5 + arg8 <= arg2 /\ arg4 <= arg6 /\ 7 + arg4 <= arg1 /\ 7 + arg4 <= arg2 /\ 10 <= arg1 /\ 10 + arg3 <= arg1 /\ 10 <= arg2 /\ 10 + arg5 <= arg2 /\ 2 + arg6 <= arg2 /\ 11 <= undef408, {arg1 -> undef408, arg2 -> 0, arg3 -> 0, arg5 -> arg6, arg6 -> arg7, arg7 -> undef414, arg8 -> undef415, arg9 -> undef416, arg10 -> undef417, arg11 -> undef418, arg12 -> undef419, arg13 -> undef420, arg14 -> undef421, arg15 -> undef422, arg16 -> undef423, arg17 -> undef424, arg18 -> undef425, arg19 -> undef426, arg20 -> undef427, arg21 -> undef428, arg22 -> undef429, arg23 -> undef430, arg24 -> undef431, arg25 -> undef432, rest remain the same}>
<l7, l10, 5 + arg5 <= arg1 /\ 5 + arg5 <= arg2 /\ arg3 <= arg4 /\ 7 + arg3 <= arg1 /\ 7 + arg3 <= arg2 /\ 10 <= arg1 /\ 10 <= arg2 /\ 2 + arg4 <= arg2 /\ 11 <= undef433, {arg1 -> undef433, arg2 -> 0, arg3 -> 0, arg4 -> arg3, arg5 -> arg4, arg6 -> arg5, arg7 -> undef439, arg8 -> undef440, arg9 -> undef441, arg10 -> undef442, arg11 -> undef443, arg12 -> undef444, arg13 -> undef445, arg14 -> undef446, arg15 -> undef447, arg16 -> undef448, arg17 -> undef449, arg18 -> undef450, arg19 -> undef451, arg20 -> undef452, arg21 -> undef453, arg22 -> undef454, arg23 -> undef455, arg24 -> undef456, arg25 -> undef457, rest remain the same}>
<l8, l10, 5 + arg12 <= arg1 /\ 5 + arg12 <= arg2 /\ 5 + arg13 <= arg2 /\ arg9 <= arg11 /\ 7 + arg9 <= arg1 /\ 7 + arg9 <= arg2 /\ 10 <= arg1 /\ 10 + arg8 <= arg1 /\ 10 <= arg2 /\ 10 + arg10 <= arg2 /\ 2 + arg11 <= arg2 /\ 12 <= undef333, {arg1 -> undef333, arg2 -> undef334, arg3 -> arg7, arg4 -> arg9, arg5 -> arg11, arg6 -> arg12, arg7 -> undef339, arg8 -> undef340, arg9 -> undef341, arg10 -> undef342, arg11 -> undef343, arg12 -> undef344, arg13 -> undef345, arg14 -> undef346, arg15 -> undef347, arg16 -> undef348, arg17 -> undef349, arg18 -> undef350, arg19 -> undef351, arg20 -> undef352, arg21 -> undef353, arg22 -> undef354, arg23 -> undef355, arg24 -> undef356, arg25 -> undef357, rest remain the same}>
<l9, l10, 5 + arg10 <= arg1 /\ 5 + arg10 <= arg2 /\ arg8 <= arg9 /\ 7 + arg8 <= arg1 /\ 7 + arg8 <= arg2 /\ 10 <= arg1 /\ 10 <= arg2 /\ 2 + arg9 <= arg2 /\ 12 <= undef358, {arg1 -> undef358, arg2 -> undef359, arg3 -> arg7, arg4 -> arg8, arg5 -> arg9, arg6 -> arg10, arg7 -> undef364, arg8 -> undef365, arg9 -> undef366, arg10 -> undef367, arg11 -> undef368, arg12 -> undef369, arg13 -> undef370, arg14 -> undef371, arg15 -> undef372, arg16 -> undef373, arg17 -> undef374, arg18 -> undef375, arg19 -> undef376, arg20 -> undef377, arg21 -> undef378, arg22 -> undef379, arg23 -> undef380, arg24 -> undef381, arg25 -> undef382, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 6 , 5 )
( 7 , 4 )
( 8 , 3 )
( 9 , 2 )
( 10 , 6 )
( 12 , 1 )

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

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 0.03952
Some transition disabled by a set of invariant(s):
Invariant at l12: arg12 + arg21 <= 0

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l12, l12, 9 + arg22 <= arg1 /\ 9 + arg23 <= arg1 /\ 9 + arg24 <= arg1 /\ 5 + arg21 <= arg1 /\ 3 + arg25 <= arg1 /\ 0 <= arg20 /\ 0 <= arg21 /\ 0 <= arg25 /\ 0 <= undef610 /\ 0 <= undef611 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg4 /\ 1 <= arg5 /\ 1 <= arg6 /\ 1 <= arg9 /\ 1 <= arg10 /\ 1 <= arg11 /\ 1 <= arg12 /\ 1 <= arg13 /\ 1 <= arg14 /\ 1 <= arg15 /\ 1 <= arg16 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef610 /\ 10 <= arg1 /\ 10 <= undef585, {arg1 -> undef585, arg2 -> -1 + arg2, arg4 -> undef588, arg5 -> undef589, arg9 -> undef593, arg11 -> undef595, arg13 -> undef597, arg14 -> undef598, arg15 -> undef599, arg16 -> undef600, arg17 -> undef601, arg18 -> undef602, arg19 -> undef603, arg20 -> 1 + arg20, arg21 -> 1 + arg21, arg22 -> undef606, arg23 -> undef607, arg24 -> undef608, arg25 -> 1 + arg25, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l12, l12, 9 + arg22 <= arg1 /\ 9 + arg23 <= arg1 /\ 9 + arg24 <= arg1 /\ 5 + arg21 <= arg1 /\ 3 + arg25 <= arg1 /\ 0 <= arg20 /\ 0 <= arg21 /\ 0 <= arg25 /\ 0 <= undef637 /\ 0 <= undef638 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg6 /\ 1 <= arg8 /\ 1 <= arg10 /\ 1 <= arg12 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef637 /\ 12 <= arg1 /\ 14 <= undef612 /\ arg7 = arg16 /\ arg8 = arg9 /\ arg10 = arg11 /\ arg12 = arg13, {arg1 -> undef612, arg2 -> -1 + arg2, arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef617, arg7 -> undef618, arg9 -> undef620, arg11 -> undef622, arg13 -> 0, arg14 -> 2, arg15 -> undef626, arg16 -> undef627, arg17 -> undef628, arg18 -> undef629, arg19 -> undef630, arg20 -> 1 + arg20, arg21 -> 1 + arg21, arg22 -> undef633, arg23 -> undef634, arg24 -> undef635, arg25 -> 1 + arg25, rest remain the same}>
Checking unfeasibility...
Time used: 4.6e-05

Analyzing SCC {l12}...
No cycles found.

Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.019967
Some transition disabled by a set of invariant(s):
Invariant at l9: arg4 <= 1

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l9, l9, 5 + arg10 <= arg1 /\ 5 + arg10 <= arg2 /\ undef283 <= arg1 /\ 0 <= arg9 /\ 1 + arg6 <= arg3 /\ 1 <= arg4 /\ 1 + arg6 <= arg4 /\ 1 <= arg5 /\ 1 + undef287 <= arg5 /\ 1 + arg6 <= undef288 /\ 1 <= arg6 /\ 1 + arg9 <= arg8 /\ 7 + arg8 <= arg1 /\ 7 + arg8 <= arg2 /\ 10 <= arg1 /\ 10 <= arg2 /\ 10 <= undef283 /\ 10 <= undef284 /\ 2 + arg9 <= arg2, {arg1 -> undef283, arg2 -> undef284, arg5 -> undef287, arg6 -> undef288, arg7 -> undef289, arg9 -> 1 + arg9, arg11 -> undef293, arg12 -> undef294, arg13 -> undef295, arg14 -> undef296, arg15 -> undef297, arg16 -> undef298, arg17 -> undef299, arg18 -> undef300, arg19 -> undef301, arg20 -> undef302, arg21 -> undef303, arg22 -> undef304, arg23 -> undef305, arg24 -> undef306, arg25 -> undef307, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l9, l9, 5 + arg10 <= arg1 /\ 5 + arg10 <= arg2 /\ undef308 <= arg1 /\ 0 <= arg3 /\ 0 <= arg4 /\ 0 <= arg9 /\ 1 + undef314 <= arg3 /\ 1 + undef312 <= arg4 /\ 1 + arg9 <= arg8 /\ arg4 <= 1 /\ 7 + arg8 <= arg1 /\ 7 + arg8 <= arg2 /\ 2 + arg9 <= arg2 /\ 12 <= arg1 /\ 12 <= arg2 /\ 12 <= undef308 /\ 12 <= undef309 /\ arg3 = arg7, {arg1 -> undef308, arg2 -> undef309, arg3 -> undef310, arg4 -> 0, arg5 -> undef312, arg6 -> 1, arg7 -> undef314, arg9 -> 1 + arg9, arg11 -> undef318, arg12 -> undef319, arg13 -> undef320, arg14 -> undef321, arg15 -> undef322, arg16 -> undef323, arg17 -> undef324, arg18 -> undef325, arg19 -> undef326, arg20 -> undef327, arg21 -> undef328, arg22 -> undef329, arg23 -> undef330, arg24 -> undef331, arg25 -> undef332, rest remain the same}>
Checking unfeasibility...
Time used: 0.009721

Checking conditional termination of SCC {l9}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002407s
Ranking function: arg7
New Graphs: 
Proving termination of subgraph 3
Checking unfeasibility...
Time used: 0.019777
Some transition disabled by a set of invariant(s):
Invariant at l8: arg4 <= 1

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l8, l8, 5 + arg12 <= arg1 /\ 5 + arg12 <= arg2 /\ 5 + arg13 <= arg2 /\ undef233 <= arg1 /\ 0 <= arg11 /\ 1 + arg6 <= arg3 /\ 1 <= arg4 /\ 1 + arg6 <= arg4 /\ 1 <= arg5 /\ 1 + undef237 <= arg5 /\ 1 + arg6 <= undef238 /\ 1 <= arg6 /\ 1 + arg11 <= arg9 /\ 7 + arg9 <= arg1 /\ 7 + arg9 <= arg2 /\ 10 <= arg1 /\ 10 + arg8 <= arg1 /\ 10 <= arg2 /\ 10 + arg10 <= arg2 /\ 10 <= undef233 /\ 10 <= undef234 /\ 2 + arg11 <= arg2, {arg1 -> undef233, arg2 -> undef234, arg5 -> undef237, arg6 -> undef238, arg7 -> undef239, arg11 -> 1 + arg11, arg14 -> undef246, arg15 -> undef247, arg16 -> undef248, arg17 -> undef249, arg18 -> undef250, arg19 -> undef251, arg20 -> undef252, arg21 -> undef253, arg22 -> undef254, arg23 -> undef255, arg24 -> undef256, arg25 -> undef257, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 5 + arg12 <= arg1 /\ 5 + arg12 <= arg2 /\ 5 + arg13 <= arg2 /\ undef258 <= arg1 /\ 0 <= arg3 /\ 0 <= arg4 /\ 0 <= arg11 /\ 1 + undef264 <= arg3 /\ 1 + undef262 <= arg4 /\ 1 + arg11 <= arg9 /\ arg4 <= 1 /\ 7 + arg9 <= arg1 /\ 7 + arg9 <= arg2 /\ 10 + arg8 <= arg1 /\ 10 + arg10 <= arg2 /\ 2 + arg11 <= arg2 /\ 12 <= arg1 /\ 12 <= arg2 /\ 12 <= undef258 /\ 12 <= undef259 /\ arg3 = arg7, {arg1 -> undef258, arg2 -> undef259, arg3 -> undef260, arg4 -> 0, arg5 -> undef262, arg6 -> 1, arg7 -> undef264, arg11 -> 1 + arg11, arg14 -> undef271, arg15 -> undef272, arg16 -> undef273, arg17 -> undef274, arg18 -> undef275, arg19 -> undef276, arg20 -> undef277, arg21 -> undef278, arg22 -> undef279, arg23 -> undef280, arg24 -> undef281, arg25 -> undef282, rest remain the same}>
Checking unfeasibility...
Time used: 0.009418

Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002589s
Ranking function: arg7
New Graphs: 
Proving termination of subgraph 4
Checking unfeasibility...
Time used: 0.008537

Checking conditional termination of SCC {l7}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002267s
Ranking function: -1 + arg3 - arg4
New Graphs: 
Proving termination of subgraph 5
Checking unfeasibility...
Time used: 0.00819

Checking conditional termination of SCC {l6}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002398s
Ranking function: -1 + arg4 - arg6
New Graphs: 
Proving termination of subgraph 6
Checking unfeasibility...
Time used: 0.016265

Checking conditional termination of SCC {l10}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006019s
Ranking function: 27 + arg5
New Graphs: 
Program Terminates