NO Initial ITS Start location: __init 0: f193_0_createTree_Return -> f295_0_main_InvokeMethod : arg2'=arg2P0, arg4'=arg4P0, arg1'=arg1P0, arg3'=arg3P0, (arg2-arg2P0 == 0 /\ arg1 > 0 /\ arg1P0 > 0 /\ -arg1+arg1P0 <= 0), cost: 1 4: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0 /\ arg1 > 0), cost: 1 7: f295_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P7, arg4'=arg4P7, arg1'=arg1P7, arg3'=arg3P7, (arg2 > 0 /\ 1+x350 > 0 /\ arg1 > 0), cost: 1 16: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ x920 > 0 /\ 1-arg1+arg3P16 <= 0 /\ arg1 > 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 1: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1 > 0 /\ arg1P1 > 0), cost: 1 2: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg1 > 0 /\ arg2P2 > 0), cost: 1 6: f1_0_main_Load -> f548_0_random_ArrayAccess : arg2'=arg2P6, arg4'=arg4P6, arg1'=arg1P6, arg3'=arg3P6, (1+arg2 > 0 /\ arg1 > 0), cost: 1 8: f2292_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P8, arg4'=arg4P8, arg1'=arg1P8, arg3'=arg3P8, (arg2 > 0 /\ 1+x380 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0), cost: 1 18: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ arg2 > 0 /\ x1080 > 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg1 > 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 19: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ arg2 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 3: f508_0_createTree_Return -> f2292_0_main_InvokeMethod : arg2'=arg2P3, arg4'=arg4P3, arg1'=arg1P3, arg3'=arg3P3, (1-arg2+arg1P3 <= 0 /\ arg1P3 > 0 /\ arg1P3-arg1 <= 0 /\ -arg3P3+arg3 == 0 /\ -1+arg2P3 > 0 /\ arg1 > 0 /\ -arg4P3+arg4 == 0 /\ -1+arg2 > 0 /\ 2-arg2+arg4 <= 0 /\ -arg2+arg2P3 <= 0), cost: 1 17: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ arg1 > 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 5: f509_0_createTree_Return -> f2302_0_main_InvokeMethod : arg2'=arg2P5, arg4'=arg4P5, arg1'=arg1P5, arg3'=arg3P5, (1-arg2+arg1P5 <= 0 /\ arg3-arg3P5 == 0 /\ -1+arg2P5 > 0 /\ 2-arg2+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ -arg1+arg1P5 <= 0 /\ arg1P5 > 0 /\ -arg2+arg2P5 <= 0), cost: 1 9: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=arg4P9, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ 1-arg4P9+x430 == 0 /\ -1+arg2P9 > 0), cost: 1 10: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=arg4P10, arg1'=arg1P10, arg3'=arg3P10, (1+arg4-arg4P10 == 0 /\ arg2P10 > 0 /\ -2+arg2 > 0 /\ arg1 > 0 /\ 2-arg2+arg2P10 <= 0 /\ -1+arg3-arg3P10 == 0 /\ arg1P10 > 0 /\ -arg1+arg1P10 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 11: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=arg4P11, arg1'=arg1P11, arg3'=arg3P11, (arg2P11 > 0 /\ 1+arg4-arg4P11 == 0 /\ -2+arg2 > 0 /\ arg1P11-arg1 <= 0 /\ x590 > 0 /\ arg1P11 > 0 /\ arg1 > 0 /\ 2+arg2P11-arg2 <= 0 /\ arg3 > 0 /\ -1+arg3-arg3P11 == 0 /\ 1+arg4 > 0), cost: 1 12: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4P12, arg1'=arg1P12, arg3'=arg3P12, (1-arg4P12+arg4 == 0 /\ -1-arg3P12+arg3 == 0 /\ x660 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 13: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4P13, arg1'=arg1P13, arg3'=arg3P13, (-1-arg3P13+arg3 == 0 /\ arg1P13 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg3 > 0 /\ 1+arg4 > 0 /\ arg2P13 > 0 /\ 1-arg4P13+arg4 == 0), cost: 1 14: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4P14, arg1'=arg1P14, arg3'=arg3P14, (-2+arg2P14-arg1 <= 0 /\ -3+arg1P14 > 0 /\ -2-arg2+arg1P14 <= 0 /\ -2+arg2P14-arg2 <= 0 /\ -3+arg2P14 > 0 /\ -2+arg1P14-arg1 <= 0 /\ -1+arg2 > 0 /\ 1+arg4-arg4P14 == 0 /\ -1+arg3-arg3P14 == 0 /\ arg3 > 0 /\ -1+arg1 > 0 /\ 1+arg4 > 0), cost: 1 15: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4P15, arg1'=arg1P15, arg3'=arg3P15, (-2-arg1+arg2P15 <= 0 /\ 1+arg4-arg4P15 == 0 /\ x850 > 0 /\ -2-arg2+arg2P15 <= 0 /\ -2+arg1P15-arg1 <= 0 /\ -1+arg2 > 0 /\ -3+arg1P15 > 0 /\ arg3 > 0 /\ -2-arg2+arg1P15 <= 0 /\ -1+arg1 > 0 /\ -1-arg3P15+arg3 == 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: 1 20: f1394_0_less_leaves_NULL -> f1268_0_append_NONNULL : arg2'=arg2P20, arg4'=arg4P20, arg1'=arg1P20, arg3'=arg3P20, (1+arg1P20-arg3 <= 0 /\ arg2 > 0 /\ 1-arg1+arg1P20 <= 0 /\ arg1 > 0 /\ 1+arg1P20 > 0 /\ arg3 > 0), cost: 1 21: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg2 > 0 /\ arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 22: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ arg2 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 26: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P26, arg4'=arg4P26, arg1'=arg1P26, arg3'=arg3P26, (arg1P26 > 0 /\ 1+arg2P26 > 0 /\ 2+arg3P26-arg1 <= 0 /\ arg1 > 0 /\ arg1P26-arg1 <= 0 /\ 1-arg1+arg2P26 <= 0), cost: 1 23: f1554_0_less_leaves_InvokeMethod -> f1268_0_append_NONNULL : arg2'=arg2P23, arg4'=arg4P23, arg1'=arg1P23, arg3'=arg3P23, (-arg2+arg1P23 <= 0 /\ 1+arg1 > 0 /\ 1+arg1P23 > 0 /\ 1+arg2 > 0), cost: 1 24: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg1 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 25: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ 1+arg1 > 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 27: f1410_0_append_NULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (2-arg1+arg3 <= 0 /\ -2+arg1 > 0 /\ 2-arg2+arg3P27 <= 0 /\ arg2 > 0 /\ arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 1-arg2+arg2P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ -arg2+arg1P27 <= 0 /\ 1+arg2P27 > 0), cost: 1 28: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Removed unreachable rules and leafs Start location: __init 4: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0 /\ arg1 > 0), cost: 1 7: f295_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P7, arg4'=arg4P7, arg1'=arg1P7, arg3'=arg3P7, (arg2 > 0 /\ 1+x350 > 0 /\ arg1 > 0), cost: 1 16: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ x920 > 0 /\ 1-arg1+arg3P16 <= 0 /\ arg1 > 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 1: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1 > 0 /\ arg1P1 > 0), cost: 1 2: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg1 > 0 /\ arg2P2 > 0), cost: 1 6: f1_0_main_Load -> f548_0_random_ArrayAccess : arg2'=arg2P6, arg4'=arg4P6, arg1'=arg1P6, arg3'=arg3P6, (1+arg2 > 0 /\ arg1 > 0), cost: 1 8: f2292_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P8, arg4'=arg4P8, arg1'=arg1P8, arg3'=arg3P8, (arg2 > 0 /\ 1+x380 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0), cost: 1 18: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ arg2 > 0 /\ x1080 > 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg1 > 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 19: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ arg2 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 17: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ arg1 > 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 9: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=arg4P9, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ 1-arg4P9+x430 == 0 /\ -1+arg2P9 > 0), cost: 1 10: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=arg4P10, arg1'=arg1P10, arg3'=arg3P10, (1+arg4-arg4P10 == 0 /\ arg2P10 > 0 /\ -2+arg2 > 0 /\ arg1 > 0 /\ 2-arg2+arg2P10 <= 0 /\ -1+arg3-arg3P10 == 0 /\ arg1P10 > 0 /\ -arg1+arg1P10 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 11: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=arg4P11, arg1'=arg1P11, arg3'=arg3P11, (arg2P11 > 0 /\ 1+arg4-arg4P11 == 0 /\ -2+arg2 > 0 /\ arg1P11-arg1 <= 0 /\ x590 > 0 /\ arg1P11 > 0 /\ arg1 > 0 /\ 2+arg2P11-arg2 <= 0 /\ arg3 > 0 /\ -1+arg3-arg3P11 == 0 /\ 1+arg4 > 0), cost: 1 12: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4P12, arg1'=arg1P12, arg3'=arg3P12, (1-arg4P12+arg4 == 0 /\ -1-arg3P12+arg3 == 0 /\ x660 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 13: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4P13, arg1'=arg1P13, arg3'=arg3P13, (-1-arg3P13+arg3 == 0 /\ arg1P13 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg3 > 0 /\ 1+arg4 > 0 /\ arg2P13 > 0 /\ 1-arg4P13+arg4 == 0), cost: 1 14: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4P14, arg1'=arg1P14, arg3'=arg3P14, (-2+arg2P14-arg1 <= 0 /\ -3+arg1P14 > 0 /\ -2-arg2+arg1P14 <= 0 /\ -2+arg2P14-arg2 <= 0 /\ -3+arg2P14 > 0 /\ -2+arg1P14-arg1 <= 0 /\ -1+arg2 > 0 /\ 1+arg4-arg4P14 == 0 /\ -1+arg3-arg3P14 == 0 /\ arg3 > 0 /\ -1+arg1 > 0 /\ 1+arg4 > 0), cost: 1 15: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4P15, arg1'=arg1P15, arg3'=arg3P15, (-2-arg1+arg2P15 <= 0 /\ 1+arg4-arg4P15 == 0 /\ x850 > 0 /\ -2-arg2+arg2P15 <= 0 /\ -2+arg1P15-arg1 <= 0 /\ -1+arg2 > 0 /\ -3+arg1P15 > 0 /\ arg3 > 0 /\ -2-arg2+arg1P15 <= 0 /\ -1+arg1 > 0 /\ -1-arg3P15+arg3 == 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: 1 20: f1394_0_less_leaves_NULL -> f1268_0_append_NONNULL : arg2'=arg2P20, arg4'=arg4P20, arg1'=arg1P20, arg3'=arg3P20, (1+arg1P20-arg3 <= 0 /\ arg2 > 0 /\ 1-arg1+arg1P20 <= 0 /\ arg1 > 0 /\ 1+arg1P20 > 0 /\ arg3 > 0), cost: 1 21: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg2 > 0 /\ arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 22: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ arg2 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 26: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P26, arg4'=arg4P26, arg1'=arg1P26, arg3'=arg3P26, (arg1P26 > 0 /\ 1+arg2P26 > 0 /\ 2+arg3P26-arg1 <= 0 /\ arg1 > 0 /\ arg1P26-arg1 <= 0 /\ 1-arg1+arg2P26 <= 0), cost: 1 23: f1554_0_less_leaves_InvokeMethod -> f1268_0_append_NONNULL : arg2'=arg2P23, arg4'=arg4P23, arg1'=arg1P23, arg3'=arg3P23, (-arg2+arg1P23 <= 0 /\ 1+arg1 > 0 /\ 1+arg1P23 > 0 /\ 1+arg2 > 0), cost: 1 24: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg1 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 25: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ 1+arg1 > 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 27: f1410_0_append_NULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (2-arg1+arg3 <= 0 /\ -2+arg1 > 0 /\ 2-arg2+arg3P27 <= 0 /\ arg2 > 0 /\ arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 1-arg2+arg2P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ -arg2+arg1P27 <= 0 /\ 1+arg2P27 > 0), cost: 1 28: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Applied preprocessing Original rule: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1 > 0 /\ arg1P1 > 0), cost: 1 New rule: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1P1 > 0), cost: 1 Applied preprocessing Original rule: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg1 > 0 /\ arg2P2 > 0), cost: 1 New rule: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg2P2 > 0), cost: 1 Applied preprocessing Original rule: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0 /\ arg1 > 0), cost: 1 New rule: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0), cost: 1 Applied preprocessing Original rule: f295_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P7, arg4'=arg4P7, arg1'=arg1P7, arg3'=arg3P7, (arg2 > 0 /\ 1+x350 > 0 /\ arg1 > 0), cost: 1 New rule: f295_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P7, arg4'=arg4P7, arg1'=arg1P7, arg3'=arg3P7, (arg2 > 0 /\ arg1 > 0), cost: 1 Applied preprocessing Original rule: f2292_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P8, arg4'=arg4P8, arg1'=arg1P8, arg3'=arg3P8, (arg2 > 0 /\ 1+x380 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0), cost: 1 New rule: f2292_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P8, arg4'=arg4P8, arg1'=arg1P8, arg3'=arg3P8, (arg2 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0), cost: 1 Applied preprocessing Original rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=arg4P9, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ 1-arg4P9+x430 == 0 /\ -1+arg2P9 > 0), cost: 1 New rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 Applied preprocessing Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=arg4P10, arg1'=arg1P10, arg3'=arg3P10, (1+arg4-arg4P10 == 0 /\ arg2P10 > 0 /\ -2+arg2 > 0 /\ arg1 > 0 /\ 2-arg2+arg2P10 <= 0 /\ -1+arg3-arg3P10 == 0 /\ arg1P10 > 0 /\ -arg1+arg1P10 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=1+arg4, arg1'=arg1P10, arg3'=-1+arg3, (arg2P10 > 0 /\ 2-arg2+arg2P10 <= 0 /\ arg1P10 > 0 /\ -arg1+arg1P10 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 Applied preprocessing Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=arg4P11, arg1'=arg1P11, arg3'=arg3P11, (arg2P11 > 0 /\ 1+arg4-arg4P11 == 0 /\ -2+arg2 > 0 /\ arg1P11-arg1 <= 0 /\ x590 > 0 /\ arg1P11 > 0 /\ arg1 > 0 /\ 2+arg2P11-arg2 <= 0 /\ arg3 > 0 /\ -1+arg3-arg3P11 == 0 /\ 1+arg4 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=1+arg4, arg1'=arg1P11, arg3'=-1+arg3, (arg2P11 > 0 /\ arg1P11-arg1 <= 0 /\ arg1P11 > 0 /\ 2+arg2P11-arg2 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 Applied preprocessing Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4P12, arg1'=arg1P12, arg3'=arg3P12, (1-arg4P12+arg4 == 0 /\ -1-arg3P12+arg3 == 0 /\ x660 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=1+arg4, arg1'=arg1P12, arg3'=-1+arg3, (arg1 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 Applied preprocessing Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4P13, arg1'=arg1P13, arg3'=arg3P13, (-1-arg3P13+arg3 == 0 /\ arg1P13 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg3 > 0 /\ 1+arg4 > 0 /\ arg2P13 > 0 /\ 1-arg4P13+arg4 == 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=1+arg4, arg1'=arg1P13, arg3'=-1+arg3, (arg1P13 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg3 > 0 /\ 1+arg4 > 0 /\ arg2P13 > 0), cost: 1 Applied preprocessing Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4P14, arg1'=arg1P14, arg3'=arg3P14, (-2+arg2P14-arg1 <= 0 /\ -3+arg1P14 > 0 /\ -2-arg2+arg1P14 <= 0 /\ -2+arg2P14-arg2 <= 0 /\ -3+arg2P14 > 0 /\ -2+arg1P14-arg1 <= 0 /\ -1+arg2 > 0 /\ 1+arg4-arg4P14 == 0 /\ -1+arg3-arg3P14 == 0 /\ arg3 > 0 /\ -1+arg1 > 0 /\ 1+arg4 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=1+arg4, arg1'=arg1P14, arg3'=-1+arg3, (-2+arg2P14-arg1 <= 0 /\ -3+arg1P14 > 0 /\ -2-arg2+arg1P14 <= 0 /\ -2+arg2P14-arg2 <= 0 /\ -3+arg2P14 > 0 /\ -2+arg1P14-arg1 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 Applied preprocessing Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4P15, arg1'=arg1P15, arg3'=arg3P15, (-2-arg1+arg2P15 <= 0 /\ 1+arg4-arg4P15 == 0 /\ x850 > 0 /\ -2-arg2+arg2P15 <= 0 /\ -2+arg1P15-arg1 <= 0 /\ -1+arg2 > 0 /\ -3+arg1P15 > 0 /\ arg3 > 0 /\ -2-arg2+arg1P15 <= 0 /\ -1+arg1 > 0 /\ -1-arg3P15+arg3 == 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=1+arg4, arg1'=arg1P15, arg3'=-1+arg3, (-2-arg1+arg2P15 <= 0 /\ -2-arg2+arg2P15 <= 0 /\ -2+arg1P15-arg1 <= 0 /\ -3+arg1P15 > 0 /\ arg3 > 0 /\ -2-arg2+arg1P15 <= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: 1 Applied preprocessing Original rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ x920 > 0 /\ 1-arg1+arg3P16 <= 0 /\ arg1 > 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 New rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Applied preprocessing Original rule: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ arg1 > 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 New rule: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 Applied preprocessing Original rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ arg2 > 0 /\ x1080 > 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg1 > 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 New rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Applied preprocessing Original rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ arg2 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 New rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Applied preprocessing Original rule: f1394_0_less_leaves_NULL -> f1268_0_append_NONNULL : arg2'=arg2P20, arg4'=arg4P20, arg1'=arg1P20, arg3'=arg3P20, (1+arg1P20-arg3 <= 0 /\ arg2 > 0 /\ 1-arg1+arg1P20 <= 0 /\ arg1 > 0 /\ 1+arg1P20 > 0 /\ arg3 > 0), cost: 1 New rule: f1394_0_less_leaves_NULL -> f1268_0_append_NONNULL : arg2'=arg2P20, arg4'=arg4P20, arg1'=arg1P20, arg3'=arg3P20, (1+arg1P20-arg3 <= 0 /\ arg2 > 0 /\ 1-arg1+arg1P20 <= 0 /\ 1+arg1P20 > 0), cost: 1 Applied preprocessing Original rule: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg2 > 0 /\ arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 New rule: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 Applied preprocessing Original rule: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ arg2 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 New rule: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 Applied preprocessing Original rule: f1554_0_less_leaves_InvokeMethod -> f1268_0_append_NONNULL : arg2'=arg2P23, arg4'=arg4P23, arg1'=arg1P23, arg3'=arg3P23, (-arg2+arg1P23 <= 0 /\ 1+arg1 > 0 /\ 1+arg1P23 > 0 /\ 1+arg2 > 0), cost: 1 New rule: f1554_0_less_leaves_InvokeMethod -> f1268_0_append_NONNULL : arg2'=arg2P23, arg4'=arg4P23, arg1'=arg1P23, arg3'=arg3P23, (-arg2+arg1P23 <= 0 /\ 1+arg1 > 0 /\ 1+arg1P23 > 0), cost: 1 Applied preprocessing Original rule: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg1 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 New rule: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 Applied preprocessing Original rule: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ 1+arg1 > 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 New rule: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 Applied preprocessing Original rule: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P26, arg4'=arg4P26, arg1'=arg1P26, arg3'=arg3P26, (arg1P26 > 0 /\ 1+arg2P26 > 0 /\ 2+arg3P26-arg1 <= 0 /\ arg1 > 0 /\ arg1P26-arg1 <= 0 /\ 1-arg1+arg2P26 <= 0), cost: 1 New rule: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P26, arg4'=arg4P26, arg1'=arg1P26, arg3'=arg3P26, (arg1P26 > 0 /\ 1+arg2P26 > 0 /\ 2+arg3P26-arg1 <= 0 /\ arg1P26-arg1 <= 0 /\ 1-arg1+arg2P26 <= 0), cost: 1 Applied preprocessing Original rule: f1410_0_append_NULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (2-arg1+arg3 <= 0 /\ -2+arg1 > 0 /\ 2-arg2+arg3P27 <= 0 /\ arg2 > 0 /\ arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 1-arg2+arg2P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ -arg2+arg1P27 <= 0 /\ 1+arg2P27 > 0), cost: 1 New rule: f1410_0_append_NULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (2-arg1+arg3 <= 0 /\ 2-arg2+arg3P27 <= 0 /\ arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 1-arg2+arg2P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ -arg2+arg1P27 <= 0 /\ 1+arg2P27 > 0), cost: 1 Simplified rules Start location: __init 31: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0), cost: 1 32: f295_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P7, arg4'=arg4P7, arg1'=arg1P7, arg3'=arg3P7, (arg2 > 0 /\ arg1 > 0), cost: 1 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 6: f1_0_main_Load -> f548_0_random_ArrayAccess : arg2'=arg2P6, arg4'=arg4P6, arg1'=arg1P6, arg3'=arg3P6, (1+arg2 > 0 /\ arg1 > 0), cost: 1 29: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1P1 > 0), cost: 1 30: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg2P2 > 0), cost: 1 33: f2292_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P8, arg4'=arg4P8, arg1'=arg1P8, arg3'=arg3P8, (arg2 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0), cost: 1 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 42: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 34: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 35: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=1+arg4, arg1'=arg1P10, arg3'=-1+arg3, (arg2P10 > 0 /\ 2-arg2+arg2P10 <= 0 /\ arg1P10 > 0 /\ -arg1+arg1P10 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 36: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=1+arg4, arg1'=arg1P11, arg3'=-1+arg3, (arg2P11 > 0 /\ arg1P11-arg1 <= 0 /\ arg1P11 > 0 /\ 2+arg2P11-arg2 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 37: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=1+arg4, arg1'=arg1P12, arg3'=-1+arg3, (arg1 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 38: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=1+arg4, arg1'=arg1P13, arg3'=-1+arg3, (arg1P13 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg3 > 0 /\ 1+arg4 > 0 /\ arg2P13 > 0), cost: 1 39: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=1+arg4, arg1'=arg1P14, arg3'=-1+arg3, (-2+arg2P14-arg1 <= 0 /\ -3+arg1P14 > 0 /\ -2-arg2+arg1P14 <= 0 /\ -2+arg2P14-arg2 <= 0 /\ -3+arg2P14 > 0 /\ -2+arg1P14-arg1 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 40: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=1+arg4, arg1'=arg1P15, arg3'=-1+arg3, (-2-arg1+arg2P15 <= 0 /\ -2-arg2+arg2P15 <= 0 /\ -2+arg1P15-arg1 <= 0 /\ -3+arg1P15 > 0 /\ arg3 > 0 /\ -2-arg2+arg1P15 <= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: 1 45: f1394_0_less_leaves_NULL -> f1268_0_append_NONNULL : arg2'=arg2P20, arg4'=arg4P20, arg1'=arg1P20, arg3'=arg3P20, (1+arg1P20-arg3 <= 0 /\ arg2 > 0 /\ 1-arg1+arg1P20 <= 0 /\ 1+arg1P20 > 0), cost: 1 46: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 47: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 51: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P26, arg4'=arg4P26, arg1'=arg1P26, arg3'=arg3P26, (arg1P26 > 0 /\ 1+arg2P26 > 0 /\ 2+arg3P26-arg1 <= 0 /\ arg1P26-arg1 <= 0 /\ 1-arg1+arg2P26 <= 0), cost: 1 48: f1554_0_less_leaves_InvokeMethod -> f1268_0_append_NONNULL : arg2'=arg2P23, arg4'=arg4P23, arg1'=arg1P23, arg3'=arg3P23, (-arg2+arg1P23 <= 0 /\ 1+arg1 > 0 /\ 1+arg1P23 > 0), cost: 1 49: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 50: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 52: f1410_0_append_NULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (2-arg1+arg3 <= 0 /\ 2-arg2+arg3P27 <= 0 /\ arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 1-arg2+arg2P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ -arg2+arg1P27 <= 0 /\ 1+arg2P27 > 0), cost: 1 28: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Applied acceleration Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=1+arg4, arg1'=arg1P12, arg3'=-1+arg3, (arg1 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4+n1, arg1'=arg1P12, arg3'=-n1+arg3, (1-n1+arg3 > 0 /\ arg1 > 0 /\ -1+arg2P12 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ -1+n1 >= 0 /\ 1+arg4 > 0), cost: n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_lOCiKp.txt Applied instantiation Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4+n1, arg1'=arg1P12, arg3'=-n1+arg3, (1-n1+arg3 > 0 /\ arg1 > 0 /\ -1+arg2P12 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ -1+n1 >= 0 /\ 1+arg4 > 0), cost: n1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4+arg3, arg1'=arg1P12, arg3'=0, (1 > 0 /\ -1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2P12 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ 1+arg4 > 0), cost: arg3 Applied acceleration Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=1+arg4, arg1'=arg1P13, arg3'=-1+arg3, (arg1P13 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ arg3 > 0 /\ 1+arg4 > 0 /\ arg2P13 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4+n2, arg1'=arg1P13, arg3'=-n2+arg3, (-1+arg2P13 > 0 /\ 1-n2+arg3 > 0 /\ arg1P13 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ -1+n2 >= 0 /\ 1+arg4 > 0 /\ arg2P13 > 0), cost: n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_jJmkmL.txt Applied instantiation Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4+n2, arg1'=arg1P13, arg3'=-n2+arg3, (-1+arg2P13 > 0 /\ 1-n2+arg3 > 0 /\ arg1P13 > 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ -1+n2 >= 0 /\ 1+arg4 > 0 /\ arg2P13 > 0), cost: n2 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4+arg3, arg1'=arg1P13, arg3'=0, (1 > 0 /\ -1+arg2P13 > 0 /\ arg1P13 > 0 /\ -1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ 1+arg4 > 0 /\ arg2P13 > 0), cost: arg3 Applied acceleration Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=1+arg4, arg1'=arg1P14, arg3'=-1+arg3, (-2+arg2P14-arg1 <= 0 /\ -3+arg1P14 > 0 /\ -2-arg2+arg1P14 <= 0 /\ -2+arg2P14-arg2 <= 0 /\ -3+arg2P14 > 0 /\ -2+arg1P14-arg1 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4+n3, arg1'=arg1P14, arg3'=-n3+arg3, (2-arg2P14+arg1P14 >= 0 /\ 2-arg2P14+arg1 >= 0 /\ -1+n3 >= 0 /\ -3+arg1P14 > 0 /\ 2+arg2-arg1P14 >= 0 /\ 2-arg2P14+arg2 >= 0 /\ 2+arg2P14-arg1P14 >= 0 /\ -3+arg2P14 > 0 /\ 2-arg1P14+arg1 >= 0 /\ 1+arg4 > 0 /\ 1-n3+arg3 > 0), cost: n3 Sub-proof via acceration calculus written to file:///tmp/tmpnam_EdANBa.txt Applied instantiation Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4+n3, arg1'=arg1P14, arg3'=-n3+arg3, (2-arg2P14+arg1P14 >= 0 /\ 2-arg2P14+arg1 >= 0 /\ -1+n3 >= 0 /\ -3+arg1P14 > 0 /\ 2+arg2-arg1P14 >= 0 /\ 2-arg2P14+arg2 >= 0 /\ 2+arg2P14-arg1P14 >= 0 /\ -3+arg2P14 > 0 /\ 2-arg1P14+arg1 >= 0 /\ 1+arg4 > 0 /\ 1-n3+arg3 > 0), cost: n3 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4+arg3, arg1'=arg1P14, arg3'=0, (2-arg2P14+arg1P14 >= 0 /\ 2-arg2P14+arg1 >= 0 /\ 1 > 0 /\ -3+arg1P14 > 0 /\ 2+arg2-arg1P14 >= 0 /\ 2-arg2P14+arg2 >= 0 /\ 2+arg2P14-arg1P14 >= 0 /\ -1+arg3 >= 0 /\ -3+arg2P14 > 0 /\ 2-arg1P14+arg1 >= 0 /\ 1+arg4 > 0), cost: arg3 Applied acceleration Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=1+arg4, arg1'=arg1P15, arg3'=-1+arg3, (-2-arg1+arg2P15 <= 0 /\ -2-arg2+arg2P15 <= 0 /\ -2+arg1P15-arg1 <= 0 /\ -3+arg1P15 > 0 /\ arg3 > 0 /\ -2-arg2+arg1P15 <= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: 1 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4+n4, arg1'=arg1P15, arg3'=-n4+arg3, (-1+n4 >= 0 /\ 2+arg1P15-arg2P15 >= 0 /\ 2+arg1-arg2P15 >= 0 /\ 2-arg1P15+arg2P15 >= 0 /\ 2+arg2-arg2P15 >= 0 /\ 2-arg1P15+arg1 >= 0 /\ 1-n4+arg3 > 0 /\ -3+arg1P15 > 0 /\ 2+arg2-arg1P15 >= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: n4 Sub-proof via acceration calculus written to file:///tmp/tmpnam_DPcGcp.txt Applied instantiation Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4+n4, arg1'=arg1P15, arg3'=-n4+arg3, (-1+n4 >= 0 /\ 2+arg1P15-arg2P15 >= 0 /\ 2+arg1-arg2P15 >= 0 /\ 2-arg1P15+arg2P15 >= 0 /\ 2+arg2-arg2P15 >= 0 /\ 2-arg1P15+arg1 >= 0 /\ 1-n4+arg3 > 0 /\ -3+arg1P15 > 0 /\ 2+arg2-arg1P15 >= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: n4 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4+arg3, arg1'=arg1P15, arg3'=0, (2+arg1P15-arg2P15 >= 0 /\ 2+arg1-arg2P15 >= 0 /\ 1 > 0 /\ 2-arg1P15+arg2P15 >= 0 /\ -1+arg3 >= 0 /\ 2+arg2-arg2P15 >= 0 /\ 2-arg1P15+arg1 >= 0 /\ -3+arg1P15 > 0 /\ 2+arg2-arg1P15 >= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: arg3 Applied simplification Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4+arg3, arg1'=arg1P12, arg3'=0, (1 > 0 /\ -1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2P12 > 0 /\ -1+arg2 > 0 /\ arg2P12 > 0 /\ arg1P12 > 0 /\ 1+arg4 > 0), cost: arg3 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4+arg3, arg1'=arg1P12, arg3'=0, (-1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2P12 > 0 /\ -1+arg2 > 0 /\ arg1P12 > 0 /\ 1+arg4 > 0), cost: arg3 Applied simplification Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4+arg3, arg1'=arg1P13, arg3'=0, (1 > 0 /\ -1+arg2P13 > 0 /\ arg1P13 > 0 /\ -1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ 1+arg4 > 0 /\ arg2P13 > 0), cost: arg3 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4+arg3, arg1'=arg1P13, arg3'=0, (-1+arg2P13 > 0 /\ arg1P13 > 0 /\ -1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ 1+arg4 > 0), cost: arg3 Applied simplification Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4+arg3, arg1'=arg1P14, arg3'=0, (2-arg2P14+arg1P14 >= 0 /\ 2-arg2P14+arg1 >= 0 /\ 1 > 0 /\ -3+arg1P14 > 0 /\ 2+arg2-arg1P14 >= 0 /\ 2-arg2P14+arg2 >= 0 /\ 2+arg2P14-arg1P14 >= 0 /\ -1+arg3 >= 0 /\ -3+arg2P14 > 0 /\ 2-arg1P14+arg1 >= 0 /\ 1+arg4 > 0), cost: arg3 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4+arg3, arg1'=arg1P14, arg3'=0, (2-arg2P14+arg1P14 >= 0 /\ 2-arg2P14+arg1 >= 0 /\ -3+arg1P14 > 0 /\ 2+arg2-arg1P14 >= 0 /\ 2-arg2P14+arg2 >= 0 /\ 2+arg2P14-arg1P14 >= 0 /\ -1+arg3 >= 0 /\ -3+arg2P14 > 0 /\ 2-arg1P14+arg1 >= 0 /\ 1+arg4 > 0), cost: arg3 Applied simplification Original rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4+arg3, arg1'=arg1P15, arg3'=0, (2+arg1P15-arg2P15 >= 0 /\ 2+arg1-arg2P15 >= 0 /\ 1 > 0 /\ 2-arg1P15+arg2P15 >= 0 /\ -1+arg3 >= 0 /\ 2+arg2-arg2P15 >= 0 /\ 2-arg1P15+arg1 >= 0 /\ -3+arg1P15 > 0 /\ 2+arg2-arg1P15 >= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: arg3 New rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4+arg3, arg1'=arg1P15, arg3'=0, (2+arg1P15-arg2P15 >= 0 /\ 2+arg1-arg2P15 >= 0 /\ 2-arg1P15+arg2P15 >= 0 /\ -1+arg3 >= 0 /\ 2+arg2-arg2P15 >= 0 /\ 2-arg1P15+arg1 >= 0 /\ -3+arg1P15 > 0 /\ 2+arg2-arg1P15 >= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: arg3 Applied deletion Removed the following rules: 37 38 39 40 Accelerated simple loops Start location: __init 31: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0), cost: 1 32: f295_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P7, arg4'=arg4P7, arg1'=arg1P7, arg3'=arg3P7, (arg2 > 0 /\ arg1 > 0), cost: 1 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 6: f1_0_main_Load -> f548_0_random_ArrayAccess : arg2'=arg2P6, arg4'=arg4P6, arg1'=arg1P6, arg3'=arg3P6, (1+arg2 > 0 /\ arg1 > 0), cost: 1 29: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1P1 > 0), cost: 1 30: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg2P2 > 0), cost: 1 33: f2292_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P8, arg4'=arg4P8, arg1'=arg1P8, arg3'=arg3P8, (arg2 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0), cost: 1 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 42: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 34: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 35: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=1+arg4, arg1'=arg1P10, arg3'=-1+arg3, (arg2P10 > 0 /\ 2-arg2+arg2P10 <= 0 /\ arg1P10 > 0 /\ -arg1+arg1P10 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 36: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=1+arg4, arg1'=arg1P11, arg3'=-1+arg3, (arg2P11 > 0 /\ arg1P11-arg1 <= 0 /\ arg1P11 > 0 /\ 2+arg2P11-arg2 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 57: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4+arg3, arg1'=arg1P12, arg3'=0, (-1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2P12 > 0 /\ -1+arg2 > 0 /\ arg1P12 > 0 /\ 1+arg4 > 0), cost: arg3 58: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4+arg3, arg1'=arg1P13, arg3'=0, (-1+arg2P13 > 0 /\ arg1P13 > 0 /\ -1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ 1+arg4 > 0), cost: arg3 59: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4+arg3, arg1'=arg1P14, arg3'=0, (2-arg2P14+arg1P14 >= 0 /\ 2-arg2P14+arg1 >= 0 /\ -3+arg1P14 > 0 /\ 2+arg2-arg1P14 >= 0 /\ 2-arg2P14+arg2 >= 0 /\ 2+arg2P14-arg1P14 >= 0 /\ -1+arg3 >= 0 /\ -3+arg2P14 > 0 /\ 2-arg1P14+arg1 >= 0 /\ 1+arg4 > 0), cost: arg3 60: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4+arg3, arg1'=arg1P15, arg3'=0, (2+arg1P15-arg2P15 >= 0 /\ 2+arg1-arg2P15 >= 0 /\ 2-arg1P15+arg2P15 >= 0 /\ -1+arg3 >= 0 /\ 2+arg2-arg2P15 >= 0 /\ 2-arg1P15+arg1 >= 0 /\ -3+arg1P15 > 0 /\ 2+arg2-arg1P15 >= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: arg3 45: f1394_0_less_leaves_NULL -> f1268_0_append_NONNULL : arg2'=arg2P20, arg4'=arg4P20, arg1'=arg1P20, arg3'=arg3P20, (1+arg1P20-arg3 <= 0 /\ arg2 > 0 /\ 1-arg1+arg1P20 <= 0 /\ 1+arg1P20 > 0), cost: 1 46: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 47: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 51: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P26, arg4'=arg4P26, arg1'=arg1P26, arg3'=arg3P26, (arg1P26 > 0 /\ 1+arg2P26 > 0 /\ 2+arg3P26-arg1 <= 0 /\ arg1P26-arg1 <= 0 /\ 1-arg1+arg2P26 <= 0), cost: 1 48: f1554_0_less_leaves_InvokeMethod -> f1268_0_append_NONNULL : arg2'=arg2P23, arg4'=arg4P23, arg1'=arg1P23, arg3'=arg3P23, (-arg2+arg1P23 <= 0 /\ 1+arg1 > 0 /\ 1+arg1P23 > 0), cost: 1 49: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 50: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 52: f1410_0_append_NULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (2-arg1+arg3 <= 0 /\ 2-arg2+arg3P27 <= 0 /\ arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 1-arg2+arg2P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ -arg2+arg1P27 <= 0 /\ 1+arg2P27 > 0), cost: 1 28: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Applied chaining First rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 Second rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=1+arg4, arg1'=arg1P10, arg3'=-1+arg3, (arg2P10 > 0 /\ 2-arg2+arg2P10 <= 0 /\ arg1P10 > 0 /\ -arg1+arg1P10 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 New rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=2+x430, arg1'=arg1P10, arg3'=-1+arg3P9, (arg2P10 > 0 /\ 1+x430 > 0 /\ arg3P9 > 0 /\ arg1P10 > 0), cost: 2 Applied chaining First rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 Second rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=1+arg4, arg1'=arg1P11, arg3'=-1+arg3, (arg2P11 > 0 /\ arg1P11-arg1 <= 0 /\ arg1P11 > 0 /\ 2+arg2P11-arg2 <= 0 /\ arg3 > 0 /\ 1+arg4 > 0), cost: 1 New rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=2+x430, arg1'=arg1P11, arg3'=-1+arg3P9, (arg2P11 > 0 /\ 1+x430 > 0 /\ arg3P9 > 0 /\ arg1P11 > 0), cost: 2 Applied chaining First rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 Second rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=arg4+arg3, arg1'=arg1P12, arg3'=0, (-1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2P12 > 0 /\ -1+arg2 > 0 /\ arg1P12 > 0 /\ 1+arg4 > 0), cost: arg3 New rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=1+arg3P9+x430, arg1'=arg1P12, arg3'=0, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg2P12 > 0 /\ arg1P12 > 0), cost: 1+arg3P9 Applied chaining First rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 Second rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=arg4+arg3, arg1'=arg1P13, arg3'=0, (-1+arg2P13 > 0 /\ arg1P13 > 0 /\ -1+arg3 >= 0 /\ arg1 > 0 /\ -1+arg2 > 0 /\ 1+arg4 > 0), cost: arg3 New rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=1+arg3P9+x430, arg1'=arg1P13, arg3'=0, (-1+arg2P13 > 0 /\ 1+x430 > 0 /\ arg1P13 > 0 /\ arg3P9 > 0), cost: 1+arg3P9 Applied chaining First rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 Second rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=arg4+arg3, arg1'=arg1P14, arg3'=0, (2-arg2P14+arg1P14 >= 0 /\ 2-arg2P14+arg1 >= 0 /\ -3+arg1P14 > 0 /\ 2+arg2-arg1P14 >= 0 /\ 2-arg2P14+arg2 >= 0 /\ 2+arg2P14-arg1P14 >= 0 /\ -1+arg3 >= 0 /\ -3+arg2P14 > 0 /\ 2-arg1P14+arg1 >= 0 /\ 1+arg4 > 0), cost: arg3 New rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=1+arg3P9+x430, arg1'=arg1P14, arg3'=0, (2-arg2P14+arg1P14 >= 0 /\ -3+arg1P14 > 0 /\ 2+arg2P14-arg1P14 >= 0 /\ 1+x430 > 0 /\ arg3P9 > 0 /\ -3+arg2P14 > 0), cost: 1+arg3P9 Applied chaining First rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 Second rule: f2274_0_createTree_LE -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=arg4+arg3, arg1'=arg1P15, arg3'=0, (2+arg1P15-arg2P15 >= 0 /\ 2+arg1-arg2P15 >= 0 /\ 2-arg1P15+arg2P15 >= 0 /\ -1+arg3 >= 0 /\ 2+arg2-arg2P15 >= 0 /\ 2-arg1P15+arg1 >= 0 /\ -3+arg1P15 > 0 /\ 2+arg2-arg1P15 >= 0 /\ 1+arg4 > 0 /\ -3+arg2P15 > 0), cost: arg3 New rule: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=1+arg3P9+x430, arg1'=arg1P15, arg3'=0, (2+arg1P15-arg2P15 >= 0 /\ 2-arg1P15+arg2P15 >= 0 /\ 1+x430 > 0 /\ arg3P9 > 0 /\ -3+arg1P15 > 0 /\ -3+arg2P15 > 0), cost: 1+arg3P9 Applied deletion Removed the following rules: 35 36 57 58 59 60 Applied chaining First rule: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P26, arg4'=arg4P26, arg1'=arg1P26, arg3'=arg3P26, (arg1P26 > 0 /\ 1+arg2P26 > 0 /\ 2+arg3P26-arg1 <= 0 /\ arg1P26-arg1 <= 0 /\ 1-arg1+arg2P26 <= 0), cost: 1 Second rule: f1410_0_append_NULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (2-arg1+arg3 <= 0 /\ 2-arg2+arg3P27 <= 0 /\ arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 1-arg2+arg2P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ -arg2+arg1P27 <= 0 /\ 1+arg2P27 > 0), cost: 1 New rule: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ 1+arg2P27 > 0), cost: 2 Applied deletion Removed the following rules: 52 Chained accelerated rules with incoming rules Start location: __init 31: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0), cost: 1 32: f295_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P7, arg4'=arg4P7, arg1'=arg1P7, arg3'=arg3P7, (arg2 > 0 /\ arg1 > 0), cost: 1 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 6: f1_0_main_Load -> f548_0_random_ArrayAccess : arg2'=arg2P6, arg4'=arg4P6, arg1'=arg1P6, arg3'=arg3P6, (1+arg2 > 0 /\ arg1 > 0), cost: 1 29: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1P1 > 0), cost: 1 30: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg2P2 > 0), cost: 1 33: f2292_0_main_InvokeMethod -> f548_0_random_ArrayAccess : arg2'=arg2P8, arg4'=arg4P8, arg1'=arg1P8, arg3'=arg3P8, (arg2 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0), cost: 1 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 42: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 34: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P9, arg4'=1+x430, arg1'=arg1P9, arg3'=arg3P9, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg1P9 > 0 /\ -1+arg2P9 > 0), cost: 1 61: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P10, arg4'=2+x430, arg1'=arg1P10, arg3'=-1+arg3P9, (arg2P10 > 0 /\ 1+x430 > 0 /\ arg3P9 > 0 /\ arg1P10 > 0), cost: 2 62: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P11, arg4'=2+x430, arg1'=arg1P11, arg3'=-1+arg3P9, (arg2P11 > 0 /\ 1+x430 > 0 /\ arg3P9 > 0 /\ arg1P11 > 0), cost: 2 63: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P12, arg4'=1+arg3P9+x430, arg1'=arg1P12, arg3'=0, (1+x430 > 0 /\ arg3P9 > 0 /\ -1+arg2P12 > 0 /\ arg1P12 > 0), cost: 1+arg3P9 64: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P13, arg4'=1+arg3P9+x430, arg1'=arg1P13, arg3'=0, (-1+arg2P13 > 0 /\ 1+x430 > 0 /\ arg1P13 > 0 /\ arg3P9 > 0), cost: 1+arg3P9 65: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P14, arg4'=1+arg3P9+x430, arg1'=arg1P14, arg3'=0, (2-arg2P14+arg1P14 >= 0 /\ -3+arg1P14 > 0 /\ 2+arg2P14-arg1P14 >= 0 /\ 1+x430 > 0 /\ arg3P9 > 0 /\ -3+arg2P14 > 0), cost: 1+arg3P9 66: f548_0_random_ArrayAccess -> f2274_0_createTree_LE : arg2'=arg2P15, arg4'=1+arg3P9+x430, arg1'=arg1P15, arg3'=0, (2+arg1P15-arg2P15 >= 0 /\ 2-arg1P15+arg2P15 >= 0 /\ 1+x430 > 0 /\ arg3P9 > 0 /\ -3+arg1P15 > 0 /\ -3+arg2P15 > 0), cost: 1+arg3P9 45: f1394_0_less_leaves_NULL -> f1268_0_append_NONNULL : arg2'=arg2P20, arg4'=arg4P20, arg1'=arg1P20, arg3'=arg3P20, (1+arg1P20-arg3 <= 0 /\ arg2 > 0 /\ 1-arg1+arg1P20 <= 0 /\ 1+arg1P20 > 0), cost: 1 46: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 47: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 51: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P26, arg4'=arg4P26, arg1'=arg1P26, arg3'=arg3P26, (arg1P26 > 0 /\ 1+arg2P26 > 0 /\ 2+arg3P26-arg1 <= 0 /\ arg1P26-arg1 <= 0 /\ 1-arg1+arg2P26 <= 0), cost: 1 67: f1268_0_append_NONNULL -> f1410_0_append_NULL : arg2'=arg2P27, arg4'=arg4P27, arg1'=arg1P27, arg3'=arg3P27, (arg1P27 > 0 /\ 3-arg1+arg2P27 <= 0 /\ 4-arg1+arg3P27 <= 0 /\ 2+arg1P27-arg1 <= 0 /\ 1+arg2P27 > 0), cost: 2 48: f1554_0_less_leaves_InvokeMethod -> f1268_0_append_NONNULL : arg2'=arg2P23, arg4'=arg4P23, arg1'=arg1P23, arg3'=arg3P23, (-arg2+arg1P23 <= 0 /\ 1+arg1 > 0 /\ 1+arg1P23 > 0), cost: 1 49: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 50: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 28: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Removed unreachable locations and irrelevant leafs Start location: __init 31: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0), cost: 1 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 29: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1P1 > 0), cost: 1 30: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg2P2 > 0), cost: 1 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 42: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 46: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 47: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 49: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 50: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 28: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Eliminating location f2302_0_main_InvokeMethod by chaining: Applied chaining First rule: f295_0_main_InvokeMethod -> f2302_0_main_InvokeMethod : arg2'=arg2P4, arg4'=arg4P4, arg1'=arg1P4, arg3'=arg3P4, (arg2P4 > 0 /\ arg2 > 0 /\ arg1P4-arg1 <= 0 /\ arg1P4 > 0), cost: 1 Second rule: f2302_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (1+arg1P17 > 0 /\ -arg2+arg2P17 <= 0 /\ 2-arg2+arg3 <= 0 /\ 1+arg1P17-arg1 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1-arg2+arg3P17 <= 0 /\ 1+arg1P17-arg2 <= 0 /\ 1+arg3P17-arg1 <= 0), cost: 1 New rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2P4 > 0 /\ arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ arg1P4 > 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Applied simplification Original rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2P4 > 0 /\ arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ arg1P4 > 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 New rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Applied deletion Removed the following rules: 31 42 Eliminated locations on linear paths Start location: __init 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 68: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 29: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1P1 > 0), cost: 1 30: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg2P2 > 0), cost: 1 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 46: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 47: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 49: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 50: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 28: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Eliminating location f1_0_main_Load by chaining: Applied chaining First rule: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Second rule: f1_0_main_Load -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1+arg1P1 <= 0 /\ arg1P1 > 0), cost: 1 New rule: __init -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P28+arg1P1 <= 0 /\ arg1P1 > 0), cost: 2 Applied chaining First rule: __init -> f1_0_main_Load : arg2'=arg2P28, arg4'=arg4P28, arg1'=arg1P28, arg3'=arg3P28, TRUE, cost: 1 Second rule: f1_0_main_Load -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1 >= 0 /\ arg2P2 > 0), cost: 1 New rule: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 Applied deletion Removed the following rules: 28 29 30 Eliminating location f1554_0_less_leaves_InvokeMethod by chaining: Applied chaining First rule: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 Second rule: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ -arg1P21+arg3P24 <= 0 /\ arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P21 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ arg1P24-arg1P21 <= 0 /\ 1+arg2P21 > 0), cost: 2 Applied simplification Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ -arg1P21+arg3P24 <= 0 /\ arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P21 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ arg1P24-arg1P21 <= 0 /\ 1+arg2P21 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ -arg1P21+arg3P24 <= 0 /\ arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ arg1P24-arg1P21 <= 0 /\ 1+arg2P21 > 0), cost: 2 Applied chaining First rule: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P21, arg4'=arg4P21, arg1'=arg1P21, arg3'=arg3P21, (arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 1 Second rule: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ -arg1P21+arg1P25 <= 0 /\ 1+arg3P25 > 0 /\ arg3P25-arg1P21 <= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 2 Applied simplification Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ -arg1P21+arg1P25 <= 0 /\ 1+arg3P25 > 0 /\ arg3P25-arg1P21 <= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg1P21 > 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ -arg1P21+arg1P25 <= 0 /\ 1+arg3P25 > 0 /\ arg3P25-arg1P21 <= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ 1-arg2+arg2P21 <= 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 2 Applied chaining First rule: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 Second rule: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ 1+arg2 > 0 /\ -arg1+arg3P24 <= 0 /\ arg1P24-arg1 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0), cost: 1 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1+arg2P24 > 0 /\ -arg1P22+arg1P24 <= 0 /\ -arg1P22+arg3P24 <= 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 Applied chaining First rule: f1394_0_less_leaves_NULL -> f1554_0_less_leaves_InvokeMethod : arg2'=arg2P22, arg4'=arg4P22, arg1'=arg1P22, arg3'=arg3P22, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ arg3 > 0), cost: 1 Second rule: f1554_0_less_leaves_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25-arg1 <= 0 /\ -arg1+arg1P25 <= 0 /\ 1+arg2 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ 1+arg1P25 > 0), cost: 1 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ -arg1P22+arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -arg1P22+arg3P25 <= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ arg3 > 0), cost: 2 Applied deletion Removed the following rules: 46 47 49 50 Eliminated locations on tree-shaped paths Start location: __init 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 68: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 71: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ -arg1P21+arg3P24 <= 0 /\ arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ arg1P24-arg1P21 <= 0 /\ 1+arg2P21 > 0), cost: 2 72: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ -arg1P21+arg1P25 <= 0 /\ 1+arg3P25 > 0 /\ arg3P25-arg1P21 <= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ 1-arg2+arg2P21 <= 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 2 73: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1+arg2P24 > 0 /\ -arg1P22+arg1P24 <= 0 /\ -arg1P22+arg3P24 <= 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 74: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ -arg1P22+arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -arg1P22+arg3P25 <= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ arg3 > 0), cost: 2 69: __init -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P28+arg1P1 <= 0 /\ arg1P1 > 0), cost: 2 70: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 Applied simplification Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ -arg1P21+arg3P24 <= 0 /\ arg1 > 0 /\ 1-arg2+arg2P21 <= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ arg1P24-arg1P21 <= 0 /\ 1+arg2P21 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 Applied simplification Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ -arg1P21+arg1P25 <= 0 /\ 1+arg3P25 > 0 /\ arg3P25-arg1P21 <= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ 1-arg2+arg2P21 <= 0 /\ arg3 > 0 /\ 1+arg2P21 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 Applied simplification Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1+arg2P24 > 0 /\ -arg1P22+arg1P24 <= 0 /\ -arg1P22+arg3P24 <= 0 /\ 1-arg2+arg2P22 <= 0 /\ arg1 > 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 Applied simplification Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg1P22 > 0 /\ 1+arg2P22 > 0 /\ 1-arg2+arg2P22 <= 0 /\ -arg1P22+arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -arg1P22+arg3P25 <= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 Simplified simple loops Start location: __init 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 68: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 75: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 76: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 69: __init -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P28+arg1P1 <= 0 /\ arg1P1 > 0), cost: 2 70: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 Applied acceleration Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 Sub-proof via acceration calculus written to file:///tmp/tmpnam_oGBpFg.txt Applied nonterm Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> [16] : (1+arg2P24 > 0 /\ -arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_fnoipJ.txt Applied acceleration Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 Sub-proof via acceration calculus written to file:///tmp/tmpnam_GcFMdp.txt Applied nonterm Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_HbDogd.txt Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 4 Applied acceleration Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 4 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n58 >= 0), cost: 4*n58 Sub-proof via acceration calculus written to file:///tmp/tmpnam_PjcKjb.txt Applied nonterm Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 4 New rule: f1394_0_less_leaves_NULL -> [16] : (1+arg2P24 > 0 /\ -arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_LOMiAK.txt Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (1+arg2P24 > 0 /\ -arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ 1+arg2P24 > 0 /\ arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 4 Applied acceleration Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 4 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ -1+n59 >= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: 4*n59 Sub-proof via acceration calculus written to file:///tmp/tmpnam_ipFJdp.txt Applied nonterm Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 4 New rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_BjNBAM.txt Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ -1+arg2P25 >= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2+2*n56 Applied acceleration Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2+2*n56 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (-1+n60 >= 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56*n60+2*n60 Sub-proof via acceration calculus written to file:///tmp/tmpnam_eEPoog.txt Applied nonterm Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2+2*n56 New rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_JIcnAm.txt Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ 1+arg2P24 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2+2*n56 Applied acceleration Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2+2*n56 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ -1+n61 >= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: 2*n61+2*n56*n61 Sub-proof via acceration calculus written to file:///tmp/tmpnam_LLNccK.txt Applied nonterm Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2+2*n56 New rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_GIFAPl.txt Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ -1+arg2P25 >= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2+2*n57 Applied acceleration Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2+2*n57 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ -1+n62 >= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n62+2*n57*n62 Sub-proof via acceration calculus written to file:///tmp/tmpnam_oniADA.txt Applied nonterm Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2+2*n57 New rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_PNgJmF.txt Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ -1+arg2P25 >= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: NONTERM Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+n57 >= 0), cost: 2+2*n57 Applied acceleration Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+n57 >= 0), cost: 2+2*n57 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n63 >= 0 /\ -1+n57 >= 0), cost: 2*n63+2*n57*n63 Sub-proof via acceration calculus written to file:///tmp/tmpnam_geEegj.txt Applied nonterm Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+n57 >= 0), cost: 2+2*n57 New rule: f1394_0_less_leaves_NULL -> [16] : (1+arg2P24 > 0 /\ -arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_DpiFJB.txt Applied chaining First rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (1+arg2P24 > 0 /\ -arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ 1+arg2P24 > 0 /\ arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n57 >= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (1+arg2P24 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (1+arg2P24 > 0 /\ -arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 New rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ 1+arg2P24 > 0 /\ arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ -1+arg2P25 >= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ 1+arg2P24 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ -1+arg2P25 >= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ -1+arg2P25 >= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ 1+arg3P25 > 0 /\ arg1 > 0 /\ 1+arg1P25 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (1+arg2P24 > 0 /\ -arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM Applied simplification Original rule: f1394_0_less_leaves_NULL -> [16] : (0 <= 0 /\ 1+arg2P24 > 0 /\ arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 1+arg3P24 > 0 /\ arg3P24 > 0 /\ 1+arg1P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n57 >= 0), cost: NONTERM Applied deletion Removed the following rules: 75 76 Accelerated simple loops Start location: __init 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 68: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 91: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 92: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM 93: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 94: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM 95: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM 96: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM 97: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM 98: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM 99: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM 100: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM 101: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM 102: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: NONTERM 103: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM 104: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n57 >= 0), cost: NONTERM 69: __init -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P28+arg1P1 <= 0 /\ arg1P1 > 0), cost: 2 70: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 New rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (-2+arg1 >= 0 /\ arg2 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg3P24 > 0 /\ -1+arg2P24 >= 0), cost: 1+2*n56 Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 New rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (-2+arg1 >= 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ 2-arg2+arg4 <= 0 /\ arg3P24 > 0 /\ -1+arg2P24 >= 0 /\ 2-arg2 <= 0), cost: 1+2*n56 Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 New rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0 /\ arg3P24 > 0 /\ -1+arg2P24 >= 0), cost: 1+2*n56 Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: 2*n56 New rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (-2+arg1 >= 0 /\ arg2 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg3P24 > 0 /\ -1+arg2P24 >= 0), cost: 2+2*n56 Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 New rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (-2+arg1 >= 0 /\ arg3P25 > 0 /\ arg2 > 0 /\ arg2P25 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 1+2*n57 Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 New rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (-2+arg1 >= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ 2-arg2+arg4 <= 0 /\ arg1P25 > 0 /\ -1+n57 >= 0 /\ 2-arg2 <= 0), cost: 1+2*n57 Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 New rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 1+2*n57 Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2*n57 New rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (-2+arg1 >= 0 /\ arg3P25 > 0 /\ arg2 > 0 /\ arg2P25 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2+2*n57 Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1-arg1P25 <= 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg3P25+arg3 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (-arg1P24+arg1 <= 0 /\ -arg3P24+arg3 <= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3 > 0 /\ -1+n57 >= 0 /\ -arg2P24+arg2 <= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM Applied chaining First rule: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM Applied chaining First rule: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 Second rule: f1394_0_less_leaves_NULL -> [16] : (arg1P24 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ arg3P24 > 0 /\ arg3 > 0 /\ -1+arg2P24 >= 0 /\ -1+n57 >= 0), cost: NONTERM New rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM Applied deletion Removed the following rules: 91 92 93 94 95 96 97 98 99 100 101 102 103 104 Chained accelerated rules with incoming rules Start location: __init 41: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P16, arg4'=arg4P16, arg1'=arg1P16, arg3'=arg3P16, (1+arg2P16 > 0 /\ arg2 > 0 /\ 1+arg1P16-arg1 <= 0 /\ 1-arg1+arg3P16 <= 0 /\ 1+arg3P16 > 0 /\ 1+arg1P16 > 0 /\ 1+arg2P16-arg1 <= 0), cost: 1 68: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P17, arg4'=arg4P17, arg1'=arg1P17, arg3'=arg3P17, (arg2 > 0 /\ 1-arg2P4+arg3P17 <= 0 /\ 1+arg3P17-arg1P4 <= 0 /\ 1+arg1P17 > 0 /\ arg1P4-arg1 <= 0 /\ 2-arg2P4+arg3P4 <= 0 /\ 1+arg1P17-arg1P4 <= 0 /\ 1+arg3P17 > 0 /\ arg2P17 > 0 /\ 1+arg1P17-arg2P4 <= 0 /\ -arg2P4+arg2P17 <= 0), cost: 2 105: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (-2+arg1 >= 0 /\ arg2 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg3P24 > 0 /\ -1+arg2P24 >= 0), cost: 1+2*n56 108: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (-2+arg1 >= 0 /\ arg2 > 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ arg3P24 > 0 /\ -1+arg2P24 >= 0), cost: 2+2*n56 109: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM 112: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (-2+arg1 >= 0 /\ arg3P25 > 0 /\ arg2 > 0 /\ arg2P25 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 1+2*n57 115: f295_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (-2+arg1 >= 0 /\ arg3P25 > 0 /\ arg2 > 0 /\ arg2P25 > 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 2+2*n57 43: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P18, arg4'=arg4P18, arg1'=arg1P18, arg3'=arg3P18, (1-arg1+arg2P18 <= 0 /\ -arg2+arg3P18 <= 0 /\ -arg2+arg1P18 <= 0 /\ arg3P18 > 0 /\ 1-arg2+arg2P18 <= 0 /\ 2-arg2+arg4 <= 0 /\ 1+arg2P18 > 0 /\ arg1P18 > 0), cost: 1 44: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P19, arg4'=arg4P19, arg1'=arg1P19, arg3'=arg3P19, (arg2P19 > 0 /\ -arg2+arg1P19 <= 0 /\ arg1P19 > 0 /\ arg1 > 0 /\ 2-arg2+arg4 <= 0 /\ arg3P19 > 0 /\ -arg2+arg3P19 <= 0), cost: 1 106: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (-2+arg1 >= 0 /\ arg1P24 > 0 /\ -1+n56 >= 0 /\ 2-arg2+arg4 <= 0 /\ arg3P24 > 0 /\ -1+arg2P24 >= 0 /\ 2-arg2 <= 0), cost: 1+2*n56 107: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P24, arg4'=arg4P24, arg1'=arg1P24, arg3'=arg3P24, (arg1P24 > 0 /\ -1+n56 >= 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0 /\ arg3P24 > 0 /\ -1+arg2P24 >= 0), cost: 1+2*n56 110: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM 111: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM 113: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (-2+arg1 >= 0 /\ arg3P25 > 0 /\ arg2P25 > 0 /\ 2-arg2+arg4 <= 0 /\ arg1P25 > 0 /\ -1+n57 >= 0 /\ 2-arg2 <= 0), cost: 1+2*n57 114: f2292_0_main_InvokeMethod -> f1394_0_less_leaves_NULL : arg2'=arg2P25, arg4'=arg4P25, arg1'=arg1P25, arg3'=arg3P25, (arg3P25 > 0 /\ arg2P25 > 0 /\ arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0 /\ arg1P25 > 0 /\ -1+n57 >= 0), cost: 1+2*n57 69: __init -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P28+arg1P1 <= 0 /\ arg1P1 > 0), cost: 2 70: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 Removed unreachable locations and irrelevant leafs Start location: __init 109: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM 110: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM 111: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM 69: __init -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P28+arg1P1 <= 0 /\ arg1P1 > 0), cost: 2 70: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 Eliminating location f295_0_main_InvokeMethod by chaining: Applied chaining First rule: __init -> f295_0_main_InvokeMethod : arg2'=arg2P1, arg4'=arg4P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P28+arg1P1 <= 0 /\ arg1P1 > 0), cost: 2 Second rule: f295_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ arg2 > 0), cost: NONTERM New rule: __init -> [16] : (-arg1P28+arg1P1 <= 0 /\ arg2P1 > 0 /\ -2+arg1P1 >= 0 /\ arg1P1 > 0), cost: NONTERM Applied simplification Original rule: __init -> [16] : (-arg1P28+arg1P1 <= 0 /\ arg2P1 > 0 /\ -2+arg1P1 >= 0 /\ arg1P1 > 0), cost: NONTERM New rule: __init -> [16] : (-arg1P28+arg1P1 <= 0 /\ arg2P1 > 0 /\ -2+arg1P1 >= 0), cost: NONTERM Applied deletion Removed the following rules: 69 109 Eliminated locations on linear paths Start location: __init 110: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM 111: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM 70: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 116: __init -> [16] : (-arg1P28+arg1P1 <= 0 /\ arg2P1 > 0 /\ -2+arg1P1 >= 0), cost: NONTERM Eliminating location f2292_0_main_InvokeMethod by chaining: Applied chaining First rule: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 Second rule: f2292_0_main_InvokeMethod -> [16] : (-2+arg1 >= 0 /\ 2-arg2+arg4 <= 0 /\ 2-arg2 <= 0), cost: NONTERM New rule: __init -> [16] : (arg1P2 > 0 /\ -2+arg1P2 >= 0 /\ 2+arg4P2-arg2P2 <= 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0 /\ 2-arg2P2 <= 0), cost: NONTERM Applied simplification Original rule: __init -> [16] : (arg1P2 > 0 /\ -2+arg1P2 >= 0 /\ 2+arg4P2-arg2P2 <= 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0 /\ 2-arg2P2 <= 0), cost: NONTERM New rule: __init -> [16] : (-2+arg1P2 >= 0 /\ 2+arg4P2-arg2P2 <= 0 /\ -arg1P2+arg1P28 >= 0 /\ 2-arg2P2 <= 0), cost: NONTERM Applied chaining First rule: __init -> f2292_0_main_InvokeMethod : arg2'=arg2P2, arg4'=arg4P2, arg1'=arg1P2, arg3'=arg3P2, (arg1P2 > 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: 2 Second rule: f2292_0_main_InvokeMethod -> [16] : (arg1 > 0 /\ -1+arg2 >= 0 /\ 2-arg2+arg4 <= 0), cost: NONTERM New rule: __init -> [16] : (arg1P2 > 0 /\ 2+arg4P2-arg2P2 <= 0 /\ -arg1P2+arg1P28 >= 0 /\ -1+arg2P2 >= 0 /\ arg2P2 > 0), cost: NONTERM Applied simplification Original rule: __init -> [16] : (arg1P2 > 0 /\ 2+arg4P2-arg2P2 <= 0 /\ -arg1P2+arg1P28 >= 0 /\ -1+arg2P2 >= 0 /\ arg2P2 > 0), cost: NONTERM New rule: __init -> [16] : (arg1P2 > 0 /\ 2+arg4P2-arg2P2 <= 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: NONTERM Applied deletion Removed the following rules: 70 110 111 Eliminated locations on tree-shaped paths Start location: __init 116: __init -> [16] : (-arg1P28+arg1P1 <= 0 /\ arg2P1 > 0 /\ -2+arg1P1 >= 0), cost: NONTERM 117: __init -> [16] : (-2+arg1P2 >= 0 /\ 2+arg4P2-arg2P2 <= 0 /\ -arg1P2+arg1P28 >= 0 /\ 2-arg2P2 <= 0), cost: NONTERM 118: __init -> [16] : (arg1P2 > 0 /\ 2+arg4P2-arg2P2 <= 0 /\ -arg1P2+arg1P28 >= 0 /\ arg2P2 > 0), cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 116 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: (-arg1P28+arg1P1 <= 0 /\ arg2P1 > 0 /\ -2+arg1P1 >= 0)