NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l6, true>
<l1, l2, (undef7 > ~(1)) /\ (arg2 > 3) /\ (undef8 > ~(1)) /\ (undef9 > ~(1)) /\ ((undef9 - (2 * undef10)) = 1) /\ ((undef11 - (2 * undef12)) = 0) /\ (undef11 > ~(1)) /\ (arg1 > 0), par{arg3 -> undef3, arg4 -> undef4, arg5 -> undef5, arg6 -> undef6}>
<l2, l3, (undef15 > ~(1)) /\ (arg2 > 3) /\ (undef19 > ~(1)) /\ (undef20 > ~(1)) /\ ((undef20 - (2 * undef21)) = 1) /\ ((undef22 - (2 * undef23)) = 0) /\ (undef22 > ~(1)) /\ (arg1 > 0) /\ ((undef20 - (2 * undef21)) >= 0) /\ ((undef20 - (2 * undef21)) < 2) /\ ((undef22 - (2 * undef23)) < 2) /\ ((undef22 - (2 * undef23)) >= 0), par{arg1 -> (0 - undef19), arg2 -> (0 - undef19), arg3 -> undef15, arg4 -> (0 - undef19), arg5 -> undef17, arg6 -> undef18}>
<l1, l2, (undef30 > ~(1)) /\ (arg2 > 3) /\ (undef31 > ~(1)) /\ (undef32 > ~(1)) /\ ((undef32 - (2 * undef33)) = 1) /\ ((undef34 - (2 * undef35)) = 1) /\ (undef34 > ~(1)) /\ (arg1 > 0), par{arg3 -> undef26, arg4 -> undef27, arg5 -> undef28, arg6 -> undef29}>
<l2, l4, (undef36 > ~(1)) /\ (arg2 > 3) /\ (undef37 > ~(1)) /\ (undef42 > ~(1)) /\ ((undef42 - (2 * undef43)) = 1) /\ ((undef44 - (2 * undef45)) = 1) /\ (undef44 > ~(1)) /\ (arg1 > 0) /\ ((undef42 - (2 * undef43)) >= 0) /\ ((undef42 - (2 * undef43)) < 2) /\ ((undef44 - (2 * undef45)) < 2) /\ ((undef44 - (2 * undef45)) >= 0), par{arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37}>
<l3, l3, (arg2 < 1) /\ (arg1 < 1) /\ (arg3 > arg2) /\ (arg2 = arg4), par{arg2 -> (arg2 + arg1), arg4 -> (arg2 + arg1), arg5 -> undef50, arg6 -> undef51}>
<l1, l2, (undef58 > ~(1)) /\ (arg2 > 3) /\ (undef59 > ~(1)) /\ (undef60 > ~(1)) /\ ((undef60 - (2 * undef61)) = 0) /\ ((undef62 - (2 * undef63)) = 1) /\ (undef62 > ~(1)) /\ (arg1 > 0), par{arg3 -> undef54, arg4 -> undef55, arg5 -> undef56, arg6 -> undef57}>
<l2, l5, (undef70 > ~(1)) /\ (arg2 > 3) /\ (undef65 > ~(1)) /\ (undef71 > ~(1)) /\ ((undef71 - (2 * undef72)) = 0) /\ ((undef73 - (2 * undef74)) = 1) /\ (undef73 > ~(1)) /\ (arg1 > 0) /\ ((undef71 - (2 * undef72)) >= 0) /\ ((undef71 - (2 * undef72)) < 2) /\ ((undef73 - (2 * undef74)) < 2) /\ ((undef73 - (2 * undef74)) >= 0), par{arg1 -> (0 - undef70), arg2 -> undef65, arg3 -> (0 - undef70), arg4 -> undef65, arg5 -> (0 - undef70), arg6 -> undef65}>
<l1, l2, (undef81 > ~(1)) /\ (arg2 > 3) /\ (undef82 > ~(1)) /\ (undef83 > ~(1)) /\ ((undef83 - (2 * undef84)) = 0) /\ ((undef85 - (2 * undef86)) = 0) /\ (undef85 > ~(1)) /\ (arg1 > 0), par{arg3 -> undef77, arg4 -> undef78, arg5 -> undef79, arg6 -> undef80}>
<l2, l5, (undef93 > ~(1)) /\ (arg2 > 3) /\ (undef94 > ~(1)) /\ (undef95 > ~(1)) /\ ((undef95 - (2 * undef96)) = 0) /\ ((undef97 - (2 * undef98)) = 0) /\ (undef97 > ~(1)) /\ (arg1 > 0) /\ ((undef95 - (2 * undef96)) >= 0) /\ ((undef95 - (2 * undef96)) < 2) /\ ((undef97 - (2 * undef98)) < 2) /\ ((undef97 - (2 * undef98)) >= 0), par{arg1 -> (0 - undef93), arg2 -> (0 - undef94), arg3 -> (0 - undef93), arg4 -> (0 - undef94), arg5 -> (0 - undef93), arg6 -> (0 - undef94)}>
<l4, l4, (arg3 > ~(1)) /\ (arg1 > ~(1)) /\ (arg4 > arg3) /\ (arg3 = arg5) /\ (arg4 = arg6), par{arg3 -> (arg3 + arg1), arg5 -> (arg3 + arg1), arg6 -> arg4}>
<l4, l4, (arg4 > ~(1)) /\ (arg2 > ~(1)) /\ (arg4 < arg3) /\ (arg3 = arg5) /\ (arg4 = arg6), par{arg4 -> (arg4 + arg2), arg5 -> arg3, arg6 -> (arg4 + arg2)}>
<l5, l5, (arg3 < 1) /\ (arg1 < 1) /\ (arg4 > arg3) /\ (arg3 = arg5) /\ (arg4 = arg6), par{arg3 -> (arg3 + arg1), arg5 -> (arg3 + arg1), arg6 -> arg4}>
<l5, l5, (arg4 < arg3) /\ (arg3 = arg5) /\ (arg4 = arg6), par{arg4 -> (arg4 + arg2), arg5 -> arg3, arg6 -> (arg4 + arg2)}>
<l6, l1, true, par{arg1 -> undef123, arg2 -> undef124, arg3 -> undef125, arg4 -> undef126, arg5 -> undef127, arg6 -> undef128}>

Fresh variables:
undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef15, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef42, undef43, undef44, undef45, undef50, undef51, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef65, undef70, undef71, undef72, undef73, undef74, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef93, undef94, undef95, undef96, undef97, undef98, undef123, undef124, undef125, undef126, undef127, undef128, 

Undef variables:
undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef15, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef42, undef43, undef44, undef45, undef50, undef51, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef65, undef70, undef71, undef72, undef73, undef74, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef93, undef94, undef95, undef96, undef97, undef98, undef123, undef124, undef125, undef126, undef127, undef128, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l3, (undef7 > ~(1)) /\ (undef124 > 3) /\ (undef8 > ~(1)) /\ (undef9 > ~(1)) /\ ((undef9 - (2 * undef10)) = 1) /\ ((undef11 - (2 * undef12)) = 0) /\ (undef11 > ~(1)) /\ (undef123 > 0) /\ (undef15 > ~(1)) /\ (undef124 > 3) /\ (undef19 > ~(1)) /\ (undef20 > ~(1)) /\ ((undef20 - (2 * undef21)) = 1) /\ ((undef22 - (2 * undef23)) = 0) /\ (undef22 > ~(1)) /\ (undef123 > 0) /\ ((undef20 - (2 * undef21)) >= 0) /\ ((undef20 - (2 * undef21)) < 2) /\ ((undef22 - (2 * undef23)) < 2) /\ ((undef22 - (2 * undef23)) >= 0), par{arg1 -> (0 - undef19), arg2 -> (0 - undef19), arg3 -> undef15, arg4 -> (0 - undef19), arg5 -> undef17, arg6 -> undef18}>
<l0, l4, (undef7 > ~(1)) /\ (undef124 > 3) /\ (undef8 > ~(1)) /\ (undef9 > ~(1)) /\ ((undef9 - (2 * undef10)) = 1) /\ ((undef11 - (2 * undef12)) = 0) /\ (undef11 > ~(1)) /\ (undef123 > 0) /\ (undef36 > ~(1)) /\ (undef124 > 3) /\ (undef37 > ~(1)) /\ (undef42 > ~(1)) /\ ((undef42 - (2 * undef43)) = 1) /\ ((undef44 - (2 * undef45)) = 1) /\ (undef44 > ~(1)) /\ (undef123 > 0) /\ ((undef42 - (2 * undef43)) >= 0) /\ ((undef42 - (2 * undef43)) < 2) /\ ((undef44 - (2 * undef45)) < 2) /\ ((undef44 - (2 * undef45)) >= 0), par{arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37}>
<l0, l5, (undef7 > ~(1)) /\ (undef124 > 3) /\ (undef8 > ~(1)) /\ (undef9 > ~(1)) /\ ((undef9 - (2 * undef10)) = 1) /\ ((undef11 - (2 * undef12)) = 0) /\ (undef11 > ~(1)) /\ (undef123 > 0) /\ (undef70 > ~(1)) /\ (undef124 > 3) /\ (undef65 > ~(1)) /\ (undef71 > ~(1)) /\ ((undef71 - (2 * undef72)) = 0) /\ ((undef73 - (2 * undef74)) = 1) /\ (undef73 > ~(1)) /\ (undef123 > 0) /\ ((undef71 - (2 * undef72)) >= 0) /\ ((undef71 - (2 * undef72)) < 2) /\ ((undef73 - (2 * undef74)) < 2) /\ ((undef73 - (2 * undef74)) >= 0), par{arg1 -> (0 - undef70), arg2 -> undef65, arg3 -> (0 - undef70), arg4 -> undef65, arg5 -> (0 - undef70), arg6 -> undef65}>
<l0, l5, (undef7 > ~(1)) /\ (undef124 > 3) /\ (undef8 > ~(1)) /\ (undef9 > ~(1)) /\ ((undef9 - (2 * undef10)) = 1) /\ ((undef11 - (2 * undef12)) = 0) /\ (undef11 > ~(1)) /\ (undef123 > 0) /\ (undef93 > ~(1)) /\ (undef124 > 3) /\ (undef94 > ~(1)) /\ (undef95 > ~(1)) /\ ((undef95 - (2 * undef96)) = 0) /\ ((undef97 - (2 * undef98)) = 0) /\ (undef97 > ~(1)) /\ (undef123 > 0) /\ ((undef95 - (2 * undef96)) >= 0) /\ ((undef95 - (2 * undef96)) < 2) /\ ((undef97 - (2 * undef98)) < 2) /\ ((undef97 - (2 * undef98)) >= 0), par{arg1 -> (0 - undef93), arg2 -> (0 - undef94), arg3 -> (0 - undef93), arg4 -> (0 - undef94), arg5 -> (0 - undef93), arg6 -> (0 - undef94)}>
<l0, l3, (undef30 > ~(1)) /\ (undef124 > 3) /\ (undef31 > ~(1)) /\ (undef32 > ~(1)) /\ ((undef32 - (2 * undef33)) = 1) /\ ((undef34 - (2 * undef35)) = 1) /\ (undef34 > ~(1)) /\ (undef123 > 0) /\ (undef15 > ~(1)) /\ (undef124 > 3) /\ (undef19 > ~(1)) /\ (undef20 > ~(1)) /\ ((undef20 - (2 * undef21)) = 1) /\ ((undef22 - (2 * undef23)) = 0) /\ (undef22 > ~(1)) /\ (undef123 > 0) /\ ((undef20 - (2 * undef21)) >= 0) /\ ((undef20 - (2 * undef21)) < 2) /\ ((undef22 - (2 * undef23)) < 2) /\ ((undef22 - (2 * undef23)) >= 0), par{arg1 -> (0 - undef19), arg2 -> (0 - undef19), arg3 -> undef15, arg4 -> (0 - undef19), arg5 -> undef17, arg6 -> undef18}>
<l0, l4, (undef30 > ~(1)) /\ (undef124 > 3) /\ (undef31 > ~(1)) /\ (undef32 > ~(1)) /\ ((undef32 - (2 * undef33)) = 1) /\ ((undef34 - (2 * undef35)) = 1) /\ (undef34 > ~(1)) /\ (undef123 > 0) /\ (undef36 > ~(1)) /\ (undef124 > 3) /\ (undef37 > ~(1)) /\ (undef42 > ~(1)) /\ ((undef42 - (2 * undef43)) = 1) /\ ((undef44 - (2 * undef45)) = 1) /\ (undef44 > ~(1)) /\ (undef123 > 0) /\ ((undef42 - (2 * undef43)) >= 0) /\ ((undef42 - (2 * undef43)) < 2) /\ ((undef44 - (2 * undef45)) < 2) /\ ((undef44 - (2 * undef45)) >= 0), par{arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37}>
<l0, l5, (undef30 > ~(1)) /\ (undef124 > 3) /\ (undef31 > ~(1)) /\ (undef32 > ~(1)) /\ ((undef32 - (2 * undef33)) = 1) /\ ((undef34 - (2 * undef35)) = 1) /\ (undef34 > ~(1)) /\ (undef123 > 0) /\ (undef70 > ~(1)) /\ (undef124 > 3) /\ (undef65 > ~(1)) /\ (undef71 > ~(1)) /\ ((undef71 - (2 * undef72)) = 0) /\ ((undef73 - (2 * undef74)) = 1) /\ (undef73 > ~(1)) /\ (undef123 > 0) /\ ((undef71 - (2 * undef72)) >= 0) /\ ((undef71 - (2 * undef72)) < 2) /\ ((undef73 - (2 * undef74)) < 2) /\ ((undef73 - (2 * undef74)) >= 0), par{arg1 -> (0 - undef70), arg2 -> undef65, arg3 -> (0 - undef70), arg4 -> undef65, arg5 -> (0 - undef70), arg6 -> undef65}>
<l0, l5, (undef30 > ~(1)) /\ (undef124 > 3) /\ (undef31 > ~(1)) /\ (undef32 > ~(1)) /\ ((undef32 - (2 * undef33)) = 1) /\ ((undef34 - (2 * undef35)) = 1) /\ (undef34 > ~(1)) /\ (undef123 > 0) /\ (undef93 > ~(1)) /\ (undef124 > 3) /\ (undef94 > ~(1)) /\ (undef95 > ~(1)) /\ ((undef95 - (2 * undef96)) = 0) /\ ((undef97 - (2 * undef98)) = 0) /\ (undef97 > ~(1)) /\ (undef123 > 0) /\ ((undef95 - (2 * undef96)) >= 0) /\ ((undef95 - (2 * undef96)) < 2) /\ ((undef97 - (2 * undef98)) < 2) /\ ((undef97 - (2 * undef98)) >= 0), par{arg1 -> (0 - undef93), arg2 -> (0 - undef94), arg3 -> (0 - undef93), arg4 -> (0 - undef94), arg5 -> (0 - undef93), arg6 -> (0 - undef94)}>
<l0, l3, (undef58 > ~(1)) /\ (undef124 > 3) /\ (undef59 > ~(1)) /\ (undef60 > ~(1)) /\ ((undef60 - (2 * undef61)) = 0) /\ ((undef62 - (2 * undef63)) = 1) /\ (undef62 > ~(1)) /\ (undef123 > 0) /\ (undef15 > ~(1)) /\ (undef124 > 3) /\ (undef19 > ~(1)) /\ (undef20 > ~(1)) /\ ((undef20 - (2 * undef21)) = 1) /\ ((undef22 - (2 * undef23)) = 0) /\ (undef22 > ~(1)) /\ (undef123 > 0) /\ ((undef20 - (2 * undef21)) >= 0) /\ ((undef20 - (2 * undef21)) < 2) /\ ((undef22 - (2 * undef23)) < 2) /\ ((undef22 - (2 * undef23)) >= 0), par{arg1 -> (0 - undef19), arg2 -> (0 - undef19), arg3 -> undef15, arg4 -> (0 - undef19), arg5 -> undef17, arg6 -> undef18}>
<l0, l4, (undef58 > ~(1)) /\ (undef124 > 3) /\ (undef59 > ~(1)) /\ (undef60 > ~(1)) /\ ((undef60 - (2 * undef61)) = 0) /\ ((undef62 - (2 * undef63)) = 1) /\ (undef62 > ~(1)) /\ (undef123 > 0) /\ (undef36 > ~(1)) /\ (undef124 > 3) /\ (undef37 > ~(1)) /\ (undef42 > ~(1)) /\ ((undef42 - (2 * undef43)) = 1) /\ ((undef44 - (2 * undef45)) = 1) /\ (undef44 > ~(1)) /\ (undef123 > 0) /\ ((undef42 - (2 * undef43)) >= 0) /\ ((undef42 - (2 * undef43)) < 2) /\ ((undef44 - (2 * undef45)) < 2) /\ ((undef44 - (2 * undef45)) >= 0), par{arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37}>
<l0, l5, (undef58 > ~(1)) /\ (undef124 > 3) /\ (undef59 > ~(1)) /\ (undef60 > ~(1)) /\ ((undef60 - (2 * undef61)) = 0) /\ ((undef62 - (2 * undef63)) = 1) /\ (undef62 > ~(1)) /\ (undef123 > 0) /\ (undef70 > ~(1)) /\ (undef124 > 3) /\ (undef65 > ~(1)) /\ (undef71 > ~(1)) /\ ((undef71 - (2 * undef72)) = 0) /\ ((undef73 - (2 * undef74)) = 1) /\ (undef73 > ~(1)) /\ (undef123 > 0) /\ ((undef71 - (2 * undef72)) >= 0) /\ ((undef71 - (2 * undef72)) < 2) /\ ((undef73 - (2 * undef74)) < 2) /\ ((undef73 - (2 * undef74)) >= 0), par{arg1 -> (0 - undef70), arg2 -> undef65, arg3 -> (0 - undef70), arg4 -> undef65, arg5 -> (0 - undef70), arg6 -> undef65}>
<l0, l5, (undef58 > ~(1)) /\ (undef124 > 3) /\ (undef59 > ~(1)) /\ (undef60 > ~(1)) /\ ((undef60 - (2 * undef61)) = 0) /\ ((undef62 - (2 * undef63)) = 1) /\ (undef62 > ~(1)) /\ (undef123 > 0) /\ (undef93 > ~(1)) /\ (undef124 > 3) /\ (undef94 > ~(1)) /\ (undef95 > ~(1)) /\ ((undef95 - (2 * undef96)) = 0) /\ ((undef97 - (2 * undef98)) = 0) /\ (undef97 > ~(1)) /\ (undef123 > 0) /\ ((undef95 - (2 * undef96)) >= 0) /\ ((undef95 - (2 * undef96)) < 2) /\ ((undef97 - (2 * undef98)) < 2) /\ ((undef97 - (2 * undef98)) >= 0), par{arg1 -> (0 - undef93), arg2 -> (0 - undef94), arg3 -> (0 - undef93), arg4 -> (0 - undef94), arg5 -> (0 - undef93), arg6 -> (0 - undef94)}>
<l0, l3, (undef81 > ~(1)) /\ (undef124 > 3) /\ (undef82 > ~(1)) /\ (undef83 > ~(1)) /\ ((undef83 - (2 * undef84)) = 0) /\ ((undef85 - (2 * undef86)) = 0) /\ (undef85 > ~(1)) /\ (undef123 > 0) /\ (undef15 > ~(1)) /\ (undef124 > 3) /\ (undef19 > ~(1)) /\ (undef20 > ~(1)) /\ ((undef20 - (2 * undef21)) = 1) /\ ((undef22 - (2 * undef23)) = 0) /\ (undef22 > ~(1)) /\ (undef123 > 0) /\ ((undef20 - (2 * undef21)) >= 0) /\ ((undef20 - (2 * undef21)) < 2) /\ ((undef22 - (2 * undef23)) < 2) /\ ((undef22 - (2 * undef23)) >= 0), par{arg1 -> (0 - undef19), arg2 -> (0 - undef19), arg3 -> undef15, arg4 -> (0 - undef19), arg5 -> undef17, arg6 -> undef18}>
<l0, l4, (undef81 > ~(1)) /\ (undef124 > 3) /\ (undef82 > ~(1)) /\ (undef83 > ~(1)) /\ ((undef83 - (2 * undef84)) = 0) /\ ((undef85 - (2 * undef86)) = 0) /\ (undef85 > ~(1)) /\ (undef123 > 0) /\ (undef36 > ~(1)) /\ (undef124 > 3) /\ (undef37 > ~(1)) /\ (undef42 > ~(1)) /\ ((undef42 - (2 * undef43)) = 1) /\ ((undef44 - (2 * undef45)) = 1) /\ (undef44 > ~(1)) /\ (undef123 > 0) /\ ((undef42 - (2 * undef43)) >= 0) /\ ((undef42 - (2 * undef43)) < 2) /\ ((undef44 - (2 * undef45)) < 2) /\ ((undef44 - (2 * undef45)) >= 0), par{arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37}>
<l0, l5, (undef81 > ~(1)) /\ (undef124 > 3) /\ (undef82 > ~(1)) /\ (undef83 > ~(1)) /\ ((undef83 - (2 * undef84)) = 0) /\ ((undef85 - (2 * undef86)) = 0) /\ (undef85 > ~(1)) /\ (undef123 > 0) /\ (undef70 > ~(1)) /\ (undef124 > 3) /\ (undef65 > ~(1)) /\ (undef71 > ~(1)) /\ ((undef71 - (2 * undef72)) = 0) /\ ((undef73 - (2 * undef74)) = 1) /\ (undef73 > ~(1)) /\ (undef123 > 0) /\ ((undef71 - (2 * undef72)) >= 0) /\ ((undef71 - (2 * undef72)) < 2) /\ ((undef73 - (2 * undef74)) < 2) /\ ((undef73 - (2 * undef74)) >= 0), par{arg1 -> (0 - undef70), arg2 -> undef65, arg3 -> (0 - undef70), arg4 -> undef65, arg5 -> (0 - undef70), arg6 -> undef65}>
<l0, l5, (undef81 > ~(1)) /\ (undef124 > 3) /\ (undef82 > ~(1)) /\ (undef83 > ~(1)) /\ ((undef83 - (2 * undef84)) = 0) /\ ((undef85 - (2 * undef86)) = 0) /\ (undef85 > ~(1)) /\ (undef123 > 0) /\ (undef93 > ~(1)) /\ (undef124 > 3) /\ (undef94 > ~(1)) /\ (undef95 > ~(1)) /\ ((undef95 - (2 * undef96)) = 0) /\ ((undef97 - (2 * undef98)) = 0) /\ (undef97 > ~(1)) /\ (undef123 > 0) /\ ((undef95 - (2 * undef96)) >= 0) /\ ((undef95 - (2 * undef96)) < 2) /\ ((undef97 - (2 * undef98)) < 2) /\ ((undef97 - (2 * undef98)) >= 0), par{arg1 -> (0 - undef93), arg2 -> (0 - undef94), arg3 -> (0 - undef93), arg4 -> (0 - undef94), arg5 -> (0 - undef93), arg6 -> (0 - undef94)}>
<l3, l3, (arg2 < 1) /\ (arg1 < 1) /\ (arg3 > arg2) /\ (arg2 = arg4), par{arg2 -> (arg2 + arg1), arg4 -> (arg2 + arg1), arg5 -> undef50, arg6 -> undef51}>
<l4, l4, (arg3 > ~(1)) /\ (arg1 > ~(1)) /\ (arg4 > arg3) /\ (arg3 = arg5) /\ (arg4 = arg6), par{arg3 -> (arg3 + arg1), arg5 -> (arg3 + arg1), arg6 -> arg4}>
<l4, l4, (arg4 > ~(1)) /\ (arg2 > ~(1)) /\ (arg4 < arg3) /\ (arg3 = arg5) /\ (arg4 = arg6), par{arg4 -> (arg4 + arg2), arg5 -> arg3, arg6 -> (arg4 + arg2)}>
<l5, l5, (arg3 < 1) /\ (arg1 < 1) /\ (arg4 > arg3) /\ (arg3 = arg5) /\ (arg4 = arg6), par{arg3 -> (arg3 + arg1), arg5 -> (arg3 + arg1), arg6 -> arg4}>
<l5, l5, (arg4 < arg3) /\ (arg3 = arg5) /\ (arg4 = arg6), par{arg4 -> (arg4 + arg2), arg5 -> arg3, arg6 -> (arg4 + arg2)}>

Fresh variables:
undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef15, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef42, undef43, undef44, undef45, undef50, undef51, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef65, undef70, undef71, undef72, undef73, undef74, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef93, undef94, undef95, undef96, undef97, undef98, undef123, undef124, undef125, undef126, undef127, undef128, 

Undef variables:
undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef15, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef42, undef43, undef44, undef45, undef50, undef51, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef65, undef70, undef71, undef72, undef73, undef74, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef93, undef94, undef95, undef96, undef97, undef98, undef123, undef124, undef125, undef126, undef127, undef128, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
<l5, l5, 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6, arg2

Graph 2:
Transitions:
<l4, l4, 1 + arg3 <= arg4 /\ 0 <= arg1 /\ 0 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
<l4, l4, 1 + arg4 <= arg3 /\ 0 <= arg2 /\ 0 <= arg4 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6, arg2

Graph 3:
Transitions:
<l3, l3, 1 + arg2 <= arg3 /\ arg1 <= 0 /\ arg2 <= 0 /\ arg2 = arg4, {arg2 -> arg1 + arg2, arg4 -> arg1 + arg2, arg5 -> undef50, arg6 -> undef51, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6

Precedence: 
Graph 0

Graph 1
<l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

Graph 2
<l0, l4, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef36 /\ 0 <= undef37 /\ 0 <= undef42 /\ 0 <= undef44 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef42 = 1 + 2*undef43 /\ undef44 = 1 + 2*undef45 /\ undef11 = 2*undef12, {arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37, rest remain the same}>
<l0, l4, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef36 /\ 0 <= undef37 /\ 0 <= undef42 /\ 0 <= undef44 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef42 = 1 + 2*undef43 /\ undef44 = 1 + 2*undef45, {arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37, rest remain the same}>
<l0, l4, 1 <= undef123 /\ 0 <= undef36 /\ 0 <= undef37 /\ 0 <= undef42 /\ 0 <= undef44 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 4 <= undef124 /\ undef42 = 1 + 2*undef43 /\ undef44 = 1 + 2*undef45 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61, {arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37, rest remain the same}>
<l0, l4, 1 <= undef123 /\ 0 <= undef36 /\ 0 <= undef37 /\ 0 <= undef42 /\ 0 <= undef44 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef42 = 1 + 2*undef43 /\ undef44 = 1 + 2*undef45 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> undef36, arg2 -> undef37, arg3 -> undef36, arg4 -> undef37, arg5 -> undef36, arg6 -> undef37, rest remain the same}>

Graph 3
<l0, l3, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef15 /\ 0 <= undef19 /\ 0 <= undef20 /\ 0 <= undef22 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef20 = 1 + 2*undef21 /\ undef11 = 2*undef12 /\ undef22 = 2*undef23, {arg1 -> -undef19, arg2 -> -undef19, arg3 -> undef15, arg4 -> -undef19, arg5 -> undef17, arg6 -> undef18, rest remain the same}>
<l0, l3, 1 <= undef123 /\ 0 <= undef15 /\ 0 <= undef19 /\ 0 <= undef20 /\ 0 <= undef22 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 4 <= undef124 /\ undef20 = 1 + 2*undef21 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef22 = 2*undef23, {arg1 -> -undef19, arg2 -> -undef19, arg3 -> undef15, arg4 -> -undef19, arg5 -> undef17, arg6 -> undef18, rest remain the same}>
<l0, l3, 1 <= undef123 /\ 0 <= undef15 /\ 0 <= undef19 /\ 0 <= undef20 /\ 0 <= undef22 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 4 <= undef124 /\ undef20 = 1 + 2*undef21 /\ undef62 = 1 + 2*undef63 /\ undef22 = 2*undef23 /\ undef60 = 2*undef61, {arg1 -> -undef19, arg2 -> -undef19, arg3 -> undef15, arg4 -> -undef19, arg5 -> undef17, arg6 -> undef18, rest remain the same}>
<l0, l3, 1 <= undef123 /\ 0 <= undef15 /\ 0 <= undef19 /\ 0 <= undef20 /\ 0 <= undef22 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef20 = 1 + 2*undef21 /\ undef22 = 2*undef23 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef19, arg2 -> -undef19, arg3 -> undef15, arg4 -> -undef19, arg5 -> undef17, arg6 -> undef18, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 3 , 3 )
( 4 , 2 )
( 5 , 1 )

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

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

Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001185s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003524s
Trying to remove transition: <l5, l5, 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007328s
Time used: 0.007037
Trying to remove transition: <l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007204s
Time used: 0.0066
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.034934s
Time used: 0.034134
Improving Solution with cost 4 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.046850s
Time used: 0.046847

LOG: SAT solveNonLinear - Elapsed time: 0.081784s
Cost: 4; Total time: 0.080981
Failed at location 5: arg3 <= arg4
Failed at location 5: arg3 <= arg4
Failed at location 5: arg3 <= arg4
Failed at location 5: arg3 <= arg4
Before Improving: 
Quasi-invariant at l5: arg3 <= arg4
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006465s
Remaining time after improvement: 0.997257
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg3 <= arg4
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
New Graphs: 
Transitions:
<l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6
Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000456s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001519s
Trying to remove transition: <l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004471s
Time used: 0.004361
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018718s
Time used: 0.018244
Improving Solution with cost 8 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.021417s
Time used: 0.021415

LOG: SAT solveNonLinear - Elapsed time: 0.040135s
Cost: 8; Total time: 0.039659
Failed at location 5: arg6 <= arg1 + arg5
Failed at location 5: arg6 <= arg1 + arg5
Failed at location 5: arg6 <= arg1 + arg5
Failed at location 5: arg6 <= arg1 + arg5
Failed at location 5: arg6 <= arg1 + arg5
Failed at location 5: arg6 <= arg1 + arg5
Failed at location 5: arg6 <= arg1 + arg5
Failed at location 5: arg6 <= arg1 + arg5
Before Improving: 
Quasi-invariant at l5: arg6 <= arg1 + arg5
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002795s
Remaining time after improvement: 0.998702
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg6 <= arg1 + arg5
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
New Graphs: 
Calling Safety with literal arg3 <= arg4 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg3 <= arg4 - Process 1
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg3 <= arg4

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000596s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000693s
Calling Safety with literal arg3 <= arg4 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg3 <= arg4 - Process 2
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg3 <= arg4

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000597s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000693s
Calling Safety with literal arg3 <= arg4 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg3 <= arg4 - Process 3
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg3 <= arg4

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000526s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000620s
Calling Safety with literal arg3 <= arg4 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg3 <= arg4 - Process 4
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg3 <= arg4

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000505s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000598s
INVARIANTS: 
5: 
Quasi-INVARIANTS to narrow Graph: 
5: arg3 <= arg4 , 
Calling Safety with literal arg6 <= arg1 + arg5 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>

LOG: CALL check - Post:arg6 <= arg1 + arg5 - Process 5
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
* Postcondition  : arg6 <= arg1 + arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000511s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000610s
Calling Safety with literal arg6 <= arg1 + arg5 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg6 <= arg1 + arg5 - Process 6
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg6 <= arg1 + arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000509s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000605s
Calling Safety with literal arg6 <= arg1 + arg5 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>

LOG: CALL check - Post:arg6 <= arg1 + arg5 - Process 7
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
* Postcondition  : arg6 <= arg1 + arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000519s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000616s
Calling Safety with literal arg6 <= arg1 + arg5 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg6 <= arg1 + arg5 - Process 8
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg6 <= arg1 + arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000513s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000608s
Calling Safety with literal arg6 <= arg1 + arg5 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>

LOG: CALL check - Post:arg6 <= arg1 + arg5 - Process 9
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
* Postcondition  : arg6 <= arg1 + arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000516s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000615s
Calling Safety with literal arg6 <= arg1 + arg5 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg6 <= arg1 + arg5 - Process 10
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg6 <= arg1 + arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000525s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000620s
Calling Safety with literal arg6 <= arg1 + arg5 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>

LOG: CALL check - Post:arg6 <= arg1 + arg5 - Process 11
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
* Postcondition  : arg6 <= arg1 + arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000509s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000604s
Calling Safety with literal arg6 <= arg1 + arg5 and entry <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg6 <= arg1 + arg5 - Process 12
* Exit transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg6 <= arg1 + arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000506s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000604s
INVARIANTS: 
5: 
Quasi-INVARIANTS to narrow Graph: 
5: arg6 <= arg1 + arg5 , 
Narrowing transition: 
<l5, l5, 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

LOG: Narrow transition size 2
Narrowing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: Narrow transition size 2
invGraph after Narrowing: 
Transitions:
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
<l5, l5, 1 + arg4 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6, arg2
Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001083s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005810s
Trying to remove transition: <l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013440s
Time used: 0.012887
Trying to remove transition: <l5, l5, 1 + arg4 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010870s
Time used: 0.009669
Trying to remove transition: <l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009162s
Time used: 0.007962
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.151185s
Time used: 0.149758
Improving Solution with cost 4 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.171558s
Time used: 0.171555

LOG: SAT solveNonLinear - Elapsed time: 0.322743s
Cost: 4; Total time: 0.321313
Failed at location 5: arg3 <= arg6
Failed at location 5: arg3 <= arg6
Failed at location 5: arg3 <= arg6
Failed at location 5: arg3 <= arg6
Before Improving: 
Quasi-invariant at l5: arg3 <= arg6
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.012201s
Remaining time after improvement: 0.995116
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg3 <= arg6
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
New Graphs: 
Transitions:
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6
Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000507s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001944s
Trying to remove transition: <l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005865s
Time used: 0.005741
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048711s
Time used: 0.048049
Improving Solution with cost 8 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.035043s
Time used: 0.035041

LOG: SAT solveNonLinear - Elapsed time: 0.083754s
Cost: 8; Total time: 0.08309
Failed at location 5: arg4 <= arg5
Failed at location 5: arg4 <= arg5
Failed at location 5: arg4 <= arg5
Failed at location 5: arg4 <= arg5
Failed at location 5: arg4 <= arg5
Failed at location 5: arg4 <= arg5
Failed at location 5: arg4 <= arg5
Failed at location 5: arg4 <= arg5
Before Improving: 
Quasi-invariant at l5: arg4 <= arg5
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004554s
Remaining time after improvement: 0.997353
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg4 <= arg5
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
New Graphs: 
Calling Safety with literal arg3 <= arg6 and entry <l0, l5, 1 + undef93 <= undef94 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg3 <= arg6 - Process 13
* Exit transition: <l0, l5, 1 + undef93 <= undef94 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg3 <= arg6

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000799s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000901s
Calling Safety with literal arg3 <= arg6 and entry <l0, l5, 1 + undef93 <= undef94 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg3 <= arg6 - Process 14
* Exit transition: <l0, l5, 1 + undef93 <= undef94 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg3 <= arg6

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000791s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000894s
Calling Safety with literal arg3 <= arg6 and entry <l0, l5, 1 + undef93 <= undef94 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg3 <= arg6 - Process 15
* Exit transition: <l0, l5, 1 + undef93 <= undef94 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg3 <= arg6

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000704s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000807s
Calling Safety with literal arg3 <= arg6 and entry <l0, l5, 1 + undef93 <= undef94 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg3 <= arg6 - Process 16
* Exit transition: <l0, l5, 1 + undef93 <= undef94 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg3 <= arg6

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000675s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000780s
INVARIANTS: 
5: 
Quasi-INVARIANTS to narrow Graph: 
5: arg3 <= arg6 , 
Calling Safety with literal arg4 <= arg5 and entry <l0, l5, 1 <= undef65 + 2*undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>

LOG: CALL check - Post:arg4 <= arg5 - Process 17
* Exit transition: <l0, l5, 1 <= undef65 + 2*undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
* Postcondition  : arg4 <= arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000581s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000682s
Calling Safety with literal arg4 <= arg5 and entry <l0, l5, 1 + undef94 <= 2*undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ undef94 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg4 <= arg5 - Process 18
* Exit transition: <l0, l5, 1 + undef94 <= 2*undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ undef94 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg4 <= arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000578s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000683s
Calling Safety with literal arg4 <= arg5 and entry <l0, l5, 1 <= undef65 + 2*undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>

LOG: CALL check - Post:arg4 <= arg5 - Process 19
* Exit transition: <l0, l5, 1 <= undef65 + 2*undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
* Postcondition  : arg4 <= arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000567s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000672s
Calling Safety with literal arg4 <= arg5 and entry <l0, l5, 1 + undef94 <= 2*undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ undef94 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg4 <= arg5 - Process 20
* Exit transition: <l0, l5, 1 + undef94 <= 2*undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ undef94 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg4 <= arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000560s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000665s
Calling Safety with literal arg4 <= arg5 and entry <l0, l5, 1 <= undef65 + 2*undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>

LOG: CALL check - Post:arg4 <= arg5 - Process 21
* Exit transition: <l0, l5, 1 <= undef65 + 2*undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
* Postcondition  : arg4 <= arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000553s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000657s
Calling Safety with literal arg4 <= arg5 and entry <l0, l5, 1 + undef94 <= 2*undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ undef94 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg4 <= arg5 - Process 22
* Exit transition: <l0, l5, 1 + undef94 <= 2*undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ undef94 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg4 <= arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000589s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000694s
Calling Safety with literal arg4 <= arg5 and entry <l0, l5, 1 <= undef65 + 2*undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>

LOG: CALL check - Post:arg4 <= arg5 - Process 23
* Exit transition: <l0, l5, 1 <= undef65 + 2*undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
* Postcondition  : arg4 <= arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000565s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000670s
Calling Safety with literal arg4 <= arg5 and entry <l0, l5, 1 + undef94 <= 2*undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ undef94 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

LOG: CALL check - Post:arg4 <= arg5 - Process 24
* Exit transition: <l0, l5, 1 + undef94 <= 2*undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ undef94 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
* Postcondition  : arg4 <= arg5

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000573s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.000676s
INVARIANTS: 
5: 
Quasi-INVARIANTS to narrow Graph: 
5: arg4 <= arg5 , 
Narrowing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

LOG: Narrow transition size 2
Narrowing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: Narrow transition size 2
Narrowing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: Narrow transition size 2
invGraph after Narrowing: 
Transitions:
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
<l5, l5, 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6, arg2
Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001290s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006779s
Trying to remove transition: <l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013263s
Time used: 0.012561
Trying to remove transition: <l5, l5, 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011346s
Time used: 0.009982
Trying to remove transition: <l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010837s
Time used: 0.009508
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.136841s
Time used: 0.1352
Improving Solution with cost 4 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.134039s
Time used: 0.134036

LOG: SAT solveNonLinear - Elapsed time: 0.270880s
Cost: 4; Total time: 0.269236
Failed at location 5: arg5 <= arg4
Failed at location 5: arg5 <= arg4
Failed at location 5: arg5 <= arg4
Failed at location 5: arg5 <= arg4
Before Improving: 
Quasi-invariant at l5: arg5 <= arg4
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.012834s
Remaining time after improvement: 0.994573
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg5 <= arg4
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
New Graphs: 
Transitions:
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6
Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000557s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002154s
Trying to remove transition: <l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005884s
Time used: 0.005753
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.070249s
Time used: 0.069802
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001488s
Time used: 4.00005
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007370s
Time used: 1.00015
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022767s
Time used: 0.014432

Proving non-termination of subgraph 1
Transitions:
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>
<l5, l5, 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6, arg2

Checking conditional non-termination of SCC {l5}...
EXIT TRANSITIONS:
<l5, end, 1 <= arg1 /\ 1 + arg4 <= arg6 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg3 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg3 = arg4 /\ arg4 = arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg4 <= arg6 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg5 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg3 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg4 <= arg6 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg3 /\ arg4 <= arg5 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg3 <= arg5 /\ 1 + arg4 <= arg6 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg3 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg3 = arg4 /\ arg4 = arg6, {all remain the same}>
<l5, end, 1 + arg4 <= arg3 /\ 1 + arg4 <= arg6 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg3 = arg5, {all remain the same}>
<l5, end, arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg3 = arg4 /\ arg3 = arg5 /\ arg4 = arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg5 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg3 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg4 <= arg6 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg3 /\ arg4 <= arg5 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg5 <= arg3 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg3, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg3 = arg4 /\ arg4 = arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg3, {all remain the same}>
<l5, end, 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg3, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg4 <= arg6 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg3 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg4 <= arg6 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg4 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg6 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg3 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg3 = arg4 /\ arg4 = arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg4 <= arg6 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg5 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg1 <= 0 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg4 <= arg3 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg4 <= arg6 /\ arg1 <= 0 /\ arg4 <= arg5 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg4 <= arg3 /\ arg4 <= arg5 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ arg1 <= 0 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg5 <= arg3 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg3 <= arg6 /\ arg4 <= arg3, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg3 <= arg6 /\ arg3 = arg4 /\ arg4 = arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg4 <= arg3, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg4 <= arg6 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.006252s
Time used: 5.00492
Improving Solution with cost 67 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.051460s
Time used: 0.051457

LOG: SAT solveNonLinear - Elapsed time: 5.057712s
Cost: 67; Total time: 5.05638
Failed at location 5: 1 + arg3 <= arg4
Failed at location 5: 1 + arg3 <= arg4
Failed at location 5: 1 + arg3 <= arg4
Failed at location 5: 1 + arg3 <= arg4
Failed at location 5: 1 + arg3 <= arg4
Failed at location 5: 1 + arg3 <= arg4
Failed at location 5: 1 + arg3 <= arg4
Failed at location 5: 1 + arg3 <= arg4
Before Improving: 
Quasi-invariant at l5: 1 + arg3 <= arg4
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.019770s
Remaining time after improvement: 0.984168
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: 1 + arg3 <= arg4

Strengthening and disabling EXIT transitions...
Closed exits from l5: 40
Strengthening exit transition (result): 
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg4 <= arg6 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg4 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg6 <= arg1 + arg5 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg4 <= arg3 /\ 1 + arg6 <= arg3 /\ arg3 = arg5 /\ arg4 = arg6, {arg4 -> arg2 + arg4, arg5 -> arg3, arg6 -> arg2 + arg4, rest remain the same}>

Checking conditional non-termination of SCC {l5}...
EXIT TRANSITIONS:
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg6 <= arg1 + arg5, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg6 <= arg1 + arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg4 <= arg6 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg6 <= arg3 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 + arg6 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.777429s
Time used: 0.776427
Improving Solution with cost 20 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.759119s
Time used: 0.759113

LOG: SAT solveNonLinear - Elapsed time: 1.536547s
Cost: 20; Total time: 1.53554
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg4 <= arg6

Strengthening and disabling EXIT transitions...
Closed exits from l5: 23
Strengthening exit transition (result): 
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg4 <= arg6 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

Checking conditional non-termination of SCC {l5}...
EXIT TRANSITIONS:
<l5, end, 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg6 <= arg1 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg4 <= arg6 /\ arg3 <= arg6 /\ arg4 <= arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.086599s
Time used: 0.086103
Improving Solution with cost 9 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.136953s
Time used: 0.136951

LOG: SAT solveNonLinear - Elapsed time: 0.223552s
Cost: 9; Total time: 0.223054
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg1 + arg5 <= arg3

Strengthening and disabling EXIT transitions...
Closed exits from l5: 5
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

Checking conditional non-termination of SCC {l5}...
EXIT TRANSITIONS:
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 <= arg1 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg4 <= arg6 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg3 = arg5, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.031594s
Time used: 0.031165
Improving Solution with cost 4 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.053486s
Time used: 0.053484

LOG: SAT solveNonLinear - Elapsed time: 0.085080s
Cost: 4; Total time: 0.084649
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg3 + arg6 <= arg4 + arg5

Strengthening and disabling EXIT transitions...
Closed exits from l5: 4
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

Checking conditional non-termination of SCC {l5}...
EXIT TRANSITIONS:
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg5 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg3 <= arg5 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.017695s
Time used: 0.01734
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015364s
Time used: 0.015362

LOG: SAT solveNonLinear - Elapsed time: 0.033058s
Cost: 1; Total time: 0.032702
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg5 <= arg3

Strengthening and disabling EXIT transitions...
Closed exits from l5: 2
Strengthening exit transition (result): 
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6 /\ arg3 = arg5, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 <= 0 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

Checking conditional non-termination of SCC {l5}...
EXIT TRANSITIONS:
<l5, end, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 <= arg3 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg4 <= arg6 /\ arg3 = arg5, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011643s
Time used: 0.011569

LOG: SAT solveNonLinear - Elapsed time: 0.011643s
Cost: 0; Total time: 0.011569
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l5: arg3 + arg4 <= arg1 + arg6

Strengthening and disabling EXIT transitions...
Closed exits from l5: 1

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l5, 1 + arg1 + arg5 <= arg6 /\ 1 + arg3 <= arg4 /\ 1 + arg5 <= arg4 /\ arg1 <= 0 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 <= 0 /\ arg3 + arg6 <= arg4 + arg5 /\ arg3 <= arg6 /\ arg3 = arg5 /\ arg4 = arg6, {arg3 -> arg1 + arg3, arg5 -> arg1 + arg3, arg6 -> arg4, rest remain the same}>

Calling reachability with...
Transition: <l5, end, true, {all remain the same}>
Conditions: 1 + arg3 <= arg4, arg4 <= arg6, arg1 + arg5 <= arg3, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, 
Transition: <l5, end, true, {all remain the same}>
Conditions: 1 + arg3 <= arg4, arg4 <= arg6, arg1 + arg5 <= arg3, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, 
Transition: <l5, end, true, {all remain the same}>
Conditions: 1 + arg3 <= arg4, arg4 <= arg6, arg1 + arg5 <= arg3, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, 
Transition: <l5, end, true, {all remain the same}>
Conditions: 1 + arg3 <= arg4, arg4 <= arg6, arg1 + arg5 <= arg3, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, 
Transition: <l5, end, true, {all remain the same}>
Conditions: 1 + arg3 <= arg4, arg4 <= arg6, arg1 + arg5 <= arg3, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, 
Transition: <l5, end, true, {all remain the same}>
Conditions: 1 + arg3 <= arg4, arg4 <= arg6, arg1 + arg5 <= arg3, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, 
Transition: <l5, end, true, {all remain the same}>
Conditions: 1 + arg3 <= arg4, arg4 <= arg6, arg1 + arg5 <= arg3, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, 
Transition: <l5, end, true, {all remain the same}>
Conditions: 1 + arg3 <= arg4, arg4 <= arg6, arg1 + arg5 <= arg3, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, 
OPEN EXITS: 
<l5, end, 1 + arg3 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 + arg6 <= arg4 + arg5 /\ arg5 <= arg3 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 + arg6 <= arg4 + arg5 /\ arg5 <= arg3 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 + arg6 <= arg4 + arg5 /\ arg5 <= arg3 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 + arg6 <= arg4 + arg5 /\ arg5 <= arg3 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 + arg6 <= arg4 + arg5 /\ arg5 <= arg3 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 + arg6 <= arg4 + arg5 /\ arg5 <= arg3 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 + arg6 <= arg4 + arg5 /\ arg5 <= arg3 /\ arg4 <= arg6, {all remain the same}>
<l5, end, 1 + arg3 <= arg4 /\ arg1 + arg5 <= arg3 /\ arg3 + arg4 <= arg1 + arg6 /\ arg3 + arg6 <= arg4 + arg5 /\ arg5 <= arg3 /\ arg4 <= arg6, {all remain the same}>

--- Reachability graph ---
> Graph without transitions.

Calling reachability with...
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
Transition: <l0, l5, 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
Conditions: 1 + arg3 <= arg4, arg1 + arg5 <= arg3, arg3 + arg4 <= arg1 + arg6, arg3 + arg6 <= arg4 + arg5, arg5 <= arg3, arg4 <= arg6, 
OPEN EXITS: 
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef73 = 1 + 2*undef74 /\ undef11 = 2*undef12 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef7 /\ 0 <= undef8 /\ 0 <= undef9 /\ 0 <= undef11 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef9 = 1 + 2*undef10 /\ undef11 = 2*undef12 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef30 /\ 0 <= undef31 /\ 0 <= undef32 /\ 0 <= undef34 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef32 = 1 + 2*undef33 /\ undef34 = 1 + 2*undef35 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef73 = 1 + 2*undef74 /\ undef60 = 2*undef61 /\ undef71 = 2*undef72, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef58 /\ 0 <= undef59 /\ 0 <= undef60 /\ 0 <= undef62 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef62 = 1 + 2*undef63 /\ undef60 = 2*undef61 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>
<l0, l5, 1 <= undef65 + undef70 /\ 1 <= undef123 /\ 0 <= undef65 /\ 0 <= undef70 /\ 0 <= undef71 /\ 0 <= undef73 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 4 <= undef124 /\ undef73 = 1 + 2*undef74 /\ undef71 = 2*undef72 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86, {arg1 -> -undef70, arg2 -> undef65, arg3 -> -undef70, arg4 -> undef65, arg5 -> -undef70, arg6 -> undef65, rest remain the same}>
<l0, l5, 1 + undef94 <= undef93 /\ 1 <= undef123 /\ 0 <= undef81 /\ 0 <= undef82 /\ 0 <= undef83 /\ 0 <= undef85 /\ 0 <= undef93 /\ 0 <= undef94 /\ 0 <= undef95 /\ 0 <= undef97 /\ 4 <= undef124 /\ undef83 = 2*undef84 /\ undef85 = 2*undef86 /\ undef95 = 2*undef96 /\ undef97 = 2*undef98, {arg1 -> -undef93, arg2 -> -undef94, arg3 -> -undef93, arg4 -> -undef94, arg5 -> -undef93, arg6 -> -undef94, rest remain the same}>

> Conditions are reachable!

Program does NOT terminate