NO

Initial ITS

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   0: f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (1+arg1p1 > 0 /\ 1-arg3p1 == 0 /\ arg1 > 0 /\ -arg2p1+arg2 == 0 /\ arg2 > 0), cost: 1
   1: f1_0_main_Load -> f410_0_main_InvokeMethod : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0), cost: 1
   2: f1_0_main_Load -> f410_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1 > 0 /\ arg1p3 > 0 /\ -arg1+arg1p3 <= 0 /\ 1+x9 > 0 /\ arg2 > 0), cost: 1
   5: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (-arg1+arg1p6 <= 0 /\ -2+arg2p6 > 0 /\ arg1 > 0 /\ 1+x21 > 0 /\ arg1p6 > 0 /\ arg2 > 0), cost: 1
   6: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg1p7 > 0 /\ -2+arg2p7 > 0 /\ arg1 > 0 /\ 1+x27 > 0 /\ arg1p7-arg1 <= 0 /\ arg2 > 0), cost: 1
   7: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (-2+arg2p8 > 0 /\ -arg1+arg1p8 <= 0 /\ arg1 > 0 /\ 1+x33 > 0 /\ arg1p8 > 0 /\ arg2 > 0), cost: 1
   8: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (1+x39 > 0 /\ arg1 > 0 /\ arg1p9 > 0 /\ -arg1+arg1p9 <= 0 /\ -2+arg2p9 > 0 /\ arg2 > 0), cost: 1
   9: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (arg1 > 0 /\ -2+arg2p10 > 0 /\ -arg1+arg1p10 <= 0 /\ arg1p10 > 0 /\ 1+x45 > 0 /\ arg2 > 0), cost: 1
  10: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, (arg1 > 0 /\ arg1p11 > 0 /\ -2+arg2p11 > 0 /\ -arg1+arg1p11 <= 0 /\ 1+x51 > 0 /\ arg2 > 0), cost: 1
  11: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, (1+x57 > 0 /\ arg1p12 > 0 /\ arg1 > 0 /\ -2+arg2p12 > 0 /\ arg1p12-arg1 <= 0 /\ arg2 > 0), cost: 1
  12: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, (arg1 > 0 /\ -1+arg2p13 > 0 /\ -1+arg2p13-arg1 <= 0 /\ -arg1+arg1p13 <= 0 /\ 1+x63 > 0 /\ arg1p13 > 0 /\ arg2 > 0), cost: 1
  14: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1-arg1p15+arg1 == 0 /\ -arg2p15+arg2 == 0 /\ -43+x72 < 0 /\ -1 < 0 /\ 1+arg3-arg3p15 == 0 /\ 1+x72 > 0), cost: 1
  15: f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, (1-arg1p16 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ 1+x75 > 0 /\ arg3-arg2 < 0 /\ 1+arg3-arg4p16 == 0 /\ -arg3p16+arg2 == 0 /\ -43+x75 < 0 /\ 1-arg1 == 0 /\ -arg2p16 == 0), cost: 1
  16: f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ -arg3p17+arg2 == 0 /\ -1+arg1-arg2p17 == 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ 1+x80 > 0 /\ -43+x80 < 0 /\ -arg1p17+arg1 == 0 /\ -1 < 0), cost: 1
  21: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=arg1p22, arg2'=arg2p22, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg1-arg1p22 == 0 /\ -arg2p22+arg2 == 0 /\ -1+arg3p22 > 0 /\ 1+x101 > 0 /\ -43+x101 < 0 /\ -1 < 0), cost: 1
  23: f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -arg2p24 == 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0 /\ 1-arg1p24 == 0 /\ -arg3p24+arg2 == 0 /\ -43+x136 < 0 /\ 1+x136 > 0), cost: 1
  24: f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1p25, arg2'=arg2p25, arg3'=arg3p25, arg4'=arg4p25, (-arg3p25+arg2 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ -arg1p25+arg1 == 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg1-arg2p25 == 0 /\ -43+x115 < 0 /\ -1+x116 > 0 /\ -1 < 0 /\ 1+x115 > 0), cost: 1
  26: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=arg1p27, arg2'=arg2p27, arg3'=arg3p27, arg4'=arg4p27, (-arg2p27+arg2 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -1+x126 > 0 /\ -1+arg1-arg1p27 == 0 /\ -1 < 0 /\ 1+x125 > 0 /\ -43+x125 < 0), cost: 1
   4: f410_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0 /\ x13 > 0), cost: 1
   3: f192_0_createForm_Return -> f410_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (-arg1+arg1p4 <= 0 /\ arg1 > 0 /\ arg1p4 > 0), cost: 1
  27: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p28, arg2'=arg2p28, arg3'=arg3p28, arg4'=arg4p28, (1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0), cost: 1
  28: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p29, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0), cost: 1
  29: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p30, arg2'=arg2p30, arg3'=arg3p30, arg4'=arg4p30, (-2+arg1p30 > 0 /\ -2+arg1 > 0 /\ -2-arg1+arg1p30 <= 0), cost: 1
  30: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p31, arg2'=arg2p31, arg3'=arg3p31, arg4'=arg4p31, (2-arg1+arg1p31 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p31 > 0), cost: 1
  31: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p32, arg2'=arg2p32, arg3'=arg3p32, arg4'=arg4p32, (1+arg4p32 > 0 /\ 1+arg2p32 > 0 /\ -5+arg1p32 > 0 /\ -4-arg1+arg1p32 <= 0 /\ -1+arg1 > 0 /\ 2+arg2p32-arg1 <= 0 /\ 2-arg1+arg4p32 <= 0), cost: 1
  32: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p33, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (1+arg2p33 > 0 /\ 2+arg4p33-arg1 <= 0 /\ -5+arg1p33 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg2p33 <= 0 /\ 1+arg4p33 > 0 /\ -4+arg1p33-arg1 <= 0), cost: 1
  33: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p34, arg2'=arg2p34, arg3'=arg3p34, arg4'=arg4p34, (-5+arg1p34 > 0 /\ 2-arg1+arg2p34 <= 0 /\ 2+arg4p34-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg4p34 > 0 /\ -4-arg1+arg1p34 <= 0 /\ 1+arg2p34 > 0), cost: 1
  34: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p35, arg2'=arg2p35, arg3'=arg3p35, arg4'=arg4p35, (1+arg4p35 > 0 /\ 1+arg2p35 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg4p35 <= 0 /\ -5+arg1p35 > 0 /\ 2-arg1+arg2p35 <= 0), cost: 1
  35: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p36, arg2'=arg2p36, arg3'=arg3p36, arg4'=arg4p36, (2-arg1+arg4p36 <= 0 /\ -5+arg1p36 > 0 /\ -1+arg1 > 0 /\ 1+arg4p36 > 0 /\ 2+arg2p36-arg1 <= 0 /\ 1+arg2p36 > 0), cost: 1
  36: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p37, arg2'=arg2p37, arg3'=arg3p37, arg4'=arg4p37, (1+arg2p37 > 0 /\ 2-arg1+arg2p37 <= 0 /\ -1+arg1 > 0 /\ 2+arg4p37-arg1 <= 0 /\ 1+arg4p37 > 0 /\ -5+arg1p37 > 0), cost: 1
  37: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p38, arg2'=arg2p38, arg3'=arg3p38, arg4'=arg4p38, (-5+arg1p38 > 0 /\ 2-arg1+arg2p38 <= 0 /\ 1+arg4p38 > 0 /\ 1+arg2p38 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg4p38 <= 0), cost: 1
  38: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p39, arg2'=arg2p39, arg3'=arg3p39, arg4'=arg4p39, (1+arg2p39 > 0 /\ 2-arg1+arg4p39 <= 0 /\ -5+arg1p39 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg2p39 <= 0 /\ 1+arg4p39 > 0), cost: 1
  39: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p40, arg2'=arg2p40, arg3'=arg3p40, arg4'=arg4p40, (2+arg2p40-arg1 <= 0 /\ 1+arg4p40 > 0 /\ -3+arg1 > 0 /\ -3+arg1p40 > 0 /\ 1+arg2p40 > 0 /\ -arg1+arg1p40 <= 0 /\ 2-arg1+arg4p40 <= 0), cost: 1
  13: f1614_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, (x64 > 0 /\ arg1 > 0 /\ arg1p14 > 0 /\ -1+arg3 > 0 /\ arg1p14-arg2 <= 0 /\ arg2 > 0), cost: 1
  17: f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, (arg1 > 0 /\ arg4-arg3p18 == 0 /\ -1+arg4 > 0 /\ -arg1p18+arg2 == 0 /\ arg3-arg2p18 == 0 /\ -arg1+arg2 < 0), cost: 1
  18: f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, (-1+arg1-arg2p19 == 0 /\ -arg3p19+arg3 == 0 /\ -arg4p19+arg4 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ arg1-arg1p19 == 0 /\ -arg2 == 0), cost: 1
  19: f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, (arg3-arg3p20 == 0 /\ arg1-arg1p20 == 0 /\ arg1 > 0 /\ -1-arg2p20+arg1 == 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  22: f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, (-1+arg1-arg1p23 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -1 < 0 /\ -arg2p23+arg3 == 0 /\ -1+arg3p23 > 0 /\ -arg1+arg2 < 0), cost: 1
  20: f571_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, (-arg1p21+arg2 == 0 /\ arg3-arg2p21 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg3p21+arg4 == 0 /\ -arg1+arg2 < 0), cost: 1
  25: f1752_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg1p26, arg2'=arg2p26, arg3'=arg3p26, arg4'=arg4p26, (-arg2p26+arg3 == 0 /\ -arg3p26+arg4 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1p26+arg2 == 0 /\ -arg1+arg2 < 0), cost: 1
  40: f2738_0_norm_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p41, arg2'=arg2p41, arg3'=arg3p41, arg4'=arg4p41, (1+arg1p41 > 0 /\ arg1p41-arg2 <= 0 /\ 1+arg2 > 0 /\ -3+arg1 > 0 /\ 1+arg4 > 0 /\ arg1p41-arg4 <= 0 /\ 2-arg1+arg1p41 <= 0), cost: 1
  41: __init -> f1_0_main_Load : arg1'=arg1p42, arg2'=arg2p42, arg3'=arg3p42, arg4'=arg4p42, T, cost: 1

Simplified Transitions

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   1: f1_0_main_Load -> f410_0_main_InvokeMethod : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0), cost: 1
  42: f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg3'=1, arg4'=arg4p1, (1+arg1p1 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  43: f1_0_main_Load -> f410_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1 > 0 /\ arg1p3 > 0 /\ -arg1+arg1p3 <= 0 /\ arg2 > 0), cost: 1
  45: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (-arg1+arg1p6 <= 0 /\ -2+arg2p6 > 0 /\ arg1 > 0 /\ arg1p6 > 0 /\ arg2 > 0), cost: 1
  46: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg1p7 > 0 /\ -2+arg2p7 > 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0 /\ arg2 > 0), cost: 1
  47: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (-2+arg2p8 > 0 /\ -arg1+arg1p8 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ arg2 > 0), cost: 1
  48: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (arg1 > 0 /\ arg1p9 > 0 /\ -arg1+arg1p9 <= 0 /\ -2+arg2p9 > 0 /\ arg2 > 0), cost: 1
  49: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (arg1 > 0 /\ -2+arg2p10 > 0 /\ -arg1+arg1p10 <= 0 /\ arg1p10 > 0 /\ arg2 > 0), cost: 1
  50: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, (arg1 > 0 /\ arg1p11 > 0 /\ -2+arg2p11 > 0 /\ -arg1+arg1p11 <= 0 /\ arg2 > 0), cost: 1
  51: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, (arg1p12 > 0 /\ arg1 > 0 /\ -2+arg2p12 > 0 /\ arg1p12-arg1 <= 0 /\ arg2 > 0), cost: 1
  52: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, (arg1 > 0 /\ -1+arg2p13 > 0 /\ -1+arg2p13-arg1 <= 0 /\ -arg1+arg1p13 <= 0 /\ arg1p13 > 0 /\ arg2 > 0), cost: 1
  54: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
  55: f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1-arg1 == 0), cost: 1
  56: f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
  61: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0), cost: 1
  63: f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0), cost: 1
  64: f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
  66: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0), cost: 1
  44: f410_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0), cost: 1
   3: f192_0_createForm_Return -> f410_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (-arg1+arg1p4 <= 0 /\ arg1 > 0 /\ arg1p4 > 0), cost: 1
  27: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p28, arg2'=arg2p28, arg3'=arg3p28, arg4'=arg4p28, (1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0), cost: 1
  28: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p29, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0), cost: 1
  29: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p30, arg2'=arg2p30, arg3'=arg3p30, arg4'=arg4p30, (-2+arg1p30 > 0 /\ -2+arg1 > 0 /\ -2-arg1+arg1p30 <= 0), cost: 1
  30: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p31, arg2'=arg2p31, arg3'=arg3p31, arg4'=arg4p31, (2-arg1+arg1p31 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p31 > 0), cost: 1
  31: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p32, arg2'=arg2p32, arg3'=arg3p32, arg4'=arg4p32, (1+arg4p32 > 0 /\ 1+arg2p32 > 0 /\ -5+arg1p32 > 0 /\ -4-arg1+arg1p32 <= 0 /\ -1+arg1 > 0 /\ 2+arg2p32-arg1 <= 0 /\ 2-arg1+arg4p32 <= 0), cost: 1
  32: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p33, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (1+arg2p33 > 0 /\ 2+arg4p33-arg1 <= 0 /\ -5+arg1p33 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg2p33 <= 0 /\ 1+arg4p33 > 0 /\ -4+arg1p33-arg1 <= 0), cost: 1
  33: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p34, arg2'=arg2p34, arg3'=arg3p34, arg4'=arg4p34, (-5+arg1p34 > 0 /\ 2-arg1+arg2p34 <= 0 /\ 2+arg4p34-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg4p34 > 0 /\ -4-arg1+arg1p34 <= 0 /\ 1+arg2p34 > 0), cost: 1
  34: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p35, arg2'=arg2p35, arg3'=arg3p35, arg4'=arg4p35, (1+arg4p35 > 0 /\ 1+arg2p35 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg4p35 <= 0 /\ -5+arg1p35 > 0 /\ 2-arg1+arg2p35 <= 0), cost: 1
  35: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p36, arg2'=arg2p36, arg3'=arg3p36, arg4'=arg4p36, (2-arg1+arg4p36 <= 0 /\ -5+arg1p36 > 0 /\ -1+arg1 > 0 /\ 1+arg4p36 > 0 /\ 2+arg2p36-arg1 <= 0 /\ 1+arg2p36 > 0), cost: 1
  36: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p37, arg2'=arg2p37, arg3'=arg3p37, arg4'=arg4p37, (1+arg2p37 > 0 /\ 2-arg1+arg2p37 <= 0 /\ -1+arg1 > 0 /\ 2+arg4p37-arg1 <= 0 /\ 1+arg4p37 > 0 /\ -5+arg1p37 > 0), cost: 1
  37: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p38, arg2'=arg2p38, arg3'=arg3p38, arg4'=arg4p38, (-5+arg1p38 > 0 /\ 2-arg1+arg2p38 <= 0 /\ 1+arg4p38 > 0 /\ 1+arg2p38 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg4p38 <= 0), cost: 1
  38: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p39, arg2'=arg2p39, arg3'=arg3p39, arg4'=arg4p39, (1+arg2p39 > 0 /\ 2-arg1+arg4p39 <= 0 /\ -5+arg1p39 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg2p39 <= 0 /\ 1+arg4p39 > 0), cost: 1
  39: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p40, arg2'=arg2p40, arg3'=arg3p40, arg4'=arg4p40, (2+arg2p40-arg1 <= 0 /\ 1+arg4p40 > 0 /\ -3+arg1 > 0 /\ -3+arg1p40 > 0 /\ 1+arg2p40 > 0 /\ -arg1+arg1p40 <= 0 /\ 2-arg1+arg4p40 <= 0), cost: 1
  53: f1614_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, (arg1 > 0 /\ arg1p14 > 0 /\ -1+arg3 > 0 /\ arg1p14-arg2 <= 0 /\ arg2 > 0), cost: 1
  57: f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p18, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  58: f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg2'=-1+arg1, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg2 == 0), cost: 1
  59: f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg2'=-1+arg1, arg4'=arg4p20, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  62: f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg3, arg3'=arg3p23, arg4'=arg4p23, (arg1 > 0 /\ -1+arg4 > 0 /\ -1+arg3p23 > 0 /\ -arg1+arg2 < 0), cost: 1
  60: f571_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p21, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  65: f1752_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p26, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  40: f2738_0_norm_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p41, arg2'=arg2p41, arg3'=arg3p41, arg4'=arg4p41, (1+arg1p41 > 0 /\ arg1p41-arg2 <= 0 /\ 1+arg2 > 0 /\ -3+arg1 > 0 /\ 1+arg4 > 0 /\ arg1p41-arg4 <= 0 /\ 2-arg1+arg1p41 <= 0), cost: 1
  41: __init -> f1_0_main_Load : arg1'=arg1p42, arg2'=arg2p42, arg3'=arg3p42, arg4'=arg4p42, T, cost: 1

	Propagated Equalities

	Original rule:
	f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (1+arg1p1 > 0 /\ 1-arg3p1 == 0 /\ arg1 > 0 /\ -arg2p1+arg2 == 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg2'=arg2, arg3'=1, arg4'=arg4p1, (0 == 0 /\ 1+arg1p1 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg3p1 = 1
		
		propagated equality arg2p1 = arg2
		
	Simplified Guard

	Original rule:
	f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg2'=arg2, arg3'=1, arg4'=arg4p1, (0 == 0 /\ 1+arg1p1 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg2'=arg2, arg3'=1, arg4'=arg4p1, (1+arg1p1 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg2'=arg2, arg3'=1, arg4'=arg4p1, (1+arg1p1 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg3'=1, arg4'=arg4p1, (1+arg1p1 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f410_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1 > 0 /\ arg1p3 > 0 /\ -arg1+arg1p3 <= 0 /\ 1+x9 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f410_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1 > 0 /\ arg1p3 > 0 /\ -arg1+arg1p3 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f410_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0 /\ x13 > 0), cost: 1
	New rule:
	f410_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (-arg1+arg1p6 <= 0 /\ -2+arg2p6 > 0 /\ arg1 > 0 /\ 1+x21 > 0 /\ arg1p6 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (-arg1+arg1p6 <= 0 /\ -2+arg2p6 > 0 /\ arg1 > 0 /\ arg1p6 > 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg1p7 > 0 /\ -2+arg2p7 > 0 /\ arg1 > 0 /\ 1+x27 > 0 /\ arg1p7-arg1 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg1p7 > 0 /\ -2+arg2p7 > 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (-2+arg2p8 > 0 /\ -arg1+arg1p8 <= 0 /\ arg1 > 0 /\ 1+x33 > 0 /\ arg1p8 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (-2+arg2p8 > 0 /\ -arg1+arg1p8 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (1+x39 > 0 /\ arg1 > 0 /\ arg1p9 > 0 /\ -arg1+arg1p9 <= 0 /\ -2+arg2p9 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (arg1 > 0 /\ arg1p9 > 0 /\ -arg1+arg1p9 <= 0 /\ -2+arg2p9 > 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (arg1 > 0 /\ -2+arg2p10 > 0 /\ -arg1+arg1p10 <= 0 /\ arg1p10 > 0 /\ 1+x45 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (arg1 > 0 /\ -2+arg2p10 > 0 /\ -arg1+arg1p10 <= 0 /\ arg1p10 > 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, (arg1 > 0 /\ arg1p11 > 0 /\ -2+arg2p11 > 0 /\ -arg1+arg1p11 <= 0 /\ 1+x51 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, (arg1 > 0 /\ arg1p11 > 0 /\ -2+arg2p11 > 0 /\ -arg1+arg1p11 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, (1+x57 > 0 /\ arg1p12 > 0 /\ arg1 > 0 /\ -2+arg2p12 > 0 /\ arg1p12-arg1 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, (arg1p12 > 0 /\ arg1 > 0 /\ -2+arg2p12 > 0 /\ arg1p12-arg1 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, (arg1 > 0 /\ -1+arg2p13 > 0 /\ -1+arg2p13-arg1 <= 0 /\ -arg1+arg1p13 <= 0 /\ 1+x63 > 0 /\ arg1p13 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, (arg1 > 0 /\ -1+arg2p13 > 0 /\ -1+arg2p13-arg1 <= 0 /\ -arg1+arg1p13 <= 0 /\ arg1p13 > 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1614_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, (x64 > 0 /\ arg1 > 0 /\ arg1p14 > 0 /\ -1+arg3 > 0 /\ arg1p14-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f1614_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, (arg1 > 0 /\ arg1p14 > 0 /\ -1+arg3 > 0 /\ arg1p14-arg2 <= 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1-arg1p15+arg1 == 0 /\ -arg2p15+arg2 == 0 /\ -43+x72 < 0 /\ -1 < 0 /\ 1+arg3-arg3p15 == 0 /\ 1+x72 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4p15, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -43+x72 < 0 /\ -1 < 0 /\ 1+x72 > 0), cost: 1
	
		propagated equality arg1p15 = -1+arg1
		
		propagated equality arg2p15 = arg2
		
		propagated equality arg3p15 = 1+arg3
		
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4p15, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -43+x72 < 0 /\ -1 < 0 /\ 1+x72 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -43+x72 < 0 /\ 1+x72 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -43+x72 < 0 /\ 1+x72 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, (1-arg1p16 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ 1+x75 > 0 /\ arg3-arg2 < 0 /\ 1+arg3-arg4p16 == 0 /\ -arg3p16+arg2 == 0 /\ -43+x75 < 0 /\ 1-arg1 == 0 /\ -arg2p16 == 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ 1+x75 > 0 /\ arg3-arg2 < 0 /\ -43+x75 < 0 /\ 1-arg1 == 0), cost: 1
	
		propagated equality arg1p16 = 1
		
		propagated equality arg4p16 = 1+arg3
		
		propagated equality arg3p16 = arg2
		
		propagated equality arg2p16 = 0
		
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ 1+x75 > 0 /\ arg3-arg2 < 0 /\ -43+x75 < 0 /\ 1-arg1 == 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (arg3 > 0 /\ 1+arg2 > 0 /\ 1+x75 > 0 /\ arg3-arg2 < 0 /\ -43+x75 < 0 /\ 1-arg1 == 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (arg3 > 0 /\ 1+arg2 > 0 /\ 1+x75 > 0 /\ arg3-arg2 < 0 /\ -43+x75 < 0 /\ 1-arg1 == 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0 /\ 1-arg1 == 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0 /\ 1-arg1 == 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1-arg1 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ -arg3p17+arg2 == 0 /\ -1+arg1-arg2p17 == 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ 1+x80 > 0 /\ -43+x80 < 0 /\ -arg1p17+arg1 == 0 /\ -1 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ 1+x80 > 0 /\ -43+x80 < 0 /\ -1 < 0), cost: 1
	
		propagated equality arg3p17 = arg2
		
		propagated equality arg2p17 = -1+arg1
		
		propagated equality arg1p17 = arg1
		
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ 1+x80 > 0 /\ -43+x80 < 0 /\ -1 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ 1+x80 > 0 /\ -43+x80 < 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ 1+x80 > 0 /\ -43+x80 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, (arg1 > 0 /\ arg4-arg3p18 == 0 /\ -1+arg4 > 0 /\ -arg1p18+arg2 == 0 /\ arg3-arg2p18 == 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p18, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
		propagated equality arg3p18 = arg4
		
		propagated equality arg1p18 = arg2
		
		propagated equality arg2p18 = arg3
		
	Simplified Guard

	Original rule:
	f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p18, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p18, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, (-1+arg1-arg2p19 == 0 /\ -arg3p19+arg3 == 0 /\ -arg4p19+arg4 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ arg1-arg1p19 == 0 /\ -arg2 == 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg3, arg4'=arg4, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg2 == 0), cost: 1
	
		propagated equality arg2p19 = -1+arg1
		
		propagated equality arg3p19 = arg3
		
		propagated equality arg4p19 = arg4
		
		propagated equality arg1p19 = arg1
		
	Simplified Guard

	Original rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg3, arg4'=arg4, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg2 == 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg3, arg4'=arg4, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg2 == 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg3, arg4'=arg4, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg2 == 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg2'=-1+arg1, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg2 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, (arg3-arg3p20 == 0 /\ arg1-arg1p20 == 0 /\ arg1 > 0 /\ -1-arg2p20+arg1 == 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg3, arg4'=arg4p20, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
		propagated equality arg3p20 = arg3
		
		propagated equality arg1p20 = arg1
		
		propagated equality arg2p20 = -1+arg1
		
	Simplified Guard

	Original rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg3, arg4'=arg4p20, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg3, arg4'=arg4p20, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg3, arg4'=arg4p20, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg2'=-1+arg1, arg4'=arg4p20, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f571_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, (-arg1p21+arg2 == 0 /\ arg3-arg2p21 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg3p21+arg4 == 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f571_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p21, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
		propagated equality arg1p21 = arg2
		
		propagated equality arg2p21 = arg3
		
		propagated equality arg3p21 = arg4
		
	Simplified Guard

	Original rule:
	f571_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p21, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f571_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p21, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=arg1p22, arg2'=arg2p22, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg1-arg1p22 == 0 /\ -arg2p22+arg2 == 0 /\ -1+arg3p22 > 0 /\ 1+x101 > 0 /\ -43+x101 < 0 /\ -1 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ 1+x101 > 0 /\ -43+x101 < 0 /\ -1 < 0), cost: 1
	
		propagated equality arg1p22 = -1+arg1
		
		propagated equality arg2p22 = arg2
		
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ 1+x101 > 0 /\ -43+x101 < 0 /\ -1 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ 1+x101 > 0 /\ -43+x101 < 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ 1+x101 > 0 /\ -43+x101 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, (-1+arg1-arg1p23 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -1 < 0 /\ -arg2p23+arg3 == 0 /\ -1+arg3p23 > 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg3, arg3'=arg3p23, arg4'=arg4p23, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -1 < 0 /\ -1+arg3p23 > 0 /\ -arg1+arg2 < 0), cost: 1
	
		propagated equality arg1p23 = -1+arg1
		
		propagated equality arg2p23 = arg3
		
	Simplified Guard

	Original rule:
	f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg3, arg3'=arg3p23, arg4'=arg4p23, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -1 < 0 /\ -1+arg3p23 > 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg3, arg3'=arg3p23, arg4'=arg4p23, (arg1 > 0 /\ -1+arg4 > 0 /\ -1+arg3p23 > 0 /\ -arg1+arg2 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -arg2p24 == 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0 /\ 1-arg1p24 == 0 /\ -arg3p24+arg2 == 0 /\ -43+x136 < 0 /\ 1+x136 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0 /\ -43+x136 < 0 /\ 1+x136 > 0), cost: 1
	
		propagated equality arg2p24 = 0
		
		propagated equality arg1p24 = 1
		
		propagated equality arg3p24 = arg2
		
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0 /\ -43+x136 < 0 /\ 1+x136 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0 /\ -43+x136 < 0 /\ 1+x136 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0 /\ -43+x136 < 0 /\ 1+x136 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1p25, arg2'=arg2p25, arg3'=arg3p25, arg4'=arg4p25, (-arg3p25+arg2 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ -arg1p25+arg1 == 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg1-arg2p25 == 0 /\ -43+x115 < 0 /\ -1+x116 > 0 /\ -1 < 0 /\ 1+x115 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -43+x115 < 0 /\ -1+x116 > 0 /\ -1 < 0 /\ 1+x115 > 0), cost: 1
	
		propagated equality arg3p25 = arg2
		
		propagated equality arg1p25 = arg1
		
		propagated equality arg2p25 = -1+arg1
		
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -43+x115 < 0 /\ -1+x116 > 0 /\ -1 < 0 /\ 1+x115 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -43+x115 < 0 /\ -1+x116 > 0 /\ 1+x115 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -43+x115 < 0 /\ -1+x116 > 0 /\ 1+x115 > 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1752_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg1p26, arg2'=arg2p26, arg3'=arg3p26, arg4'=arg4p26, (-arg2p26+arg3 == 0 /\ -arg3p26+arg4 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1p26+arg2 == 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f1752_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p26, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
		propagated equality arg2p26 = arg3
		
		propagated equality arg3p26 = arg4
		
		propagated equality arg1p26 = arg2
		
	Simplified Guard

	Original rule:
	f1752_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p26, (0 == 0 /\ arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	New rule:
	f1752_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p26, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=arg1p27, arg2'=arg2p27, arg3'=arg3p27, arg4'=arg4p27, (-arg2p27+arg2 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -1+x126 > 0 /\ -1+arg1-arg1p27 == 0 /\ -1 < 0 /\ 1+x125 > 0 /\ -43+x125 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p27, arg4'=arg4p27, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -1+x126 > 0 /\ -1 < 0 /\ 1+x125 > 0 /\ -43+x125 < 0), cost: 1
	
		propagated equality arg2p27 = arg2
		
		propagated equality arg1p27 = -1+arg1
		
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p27, arg4'=arg4p27, (0 == 0 /\ arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -1+x126 > 0 /\ -1 < 0 /\ 1+x125 > 0 /\ -43+x125 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -1+x126 > 0 /\ 1+x125 > 0 /\ -43+x125 < 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -1+x126 > 0 /\ 1+x125 > 0 /\ -43+x125 < 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -42 <= 0), cost: 1
	
	Simplified Guard

	Original rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0 /\ -42 <= 0), cost: 1
	New rule:
	f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0), cost: 1

Step with 41

	Trace

	41[T]
	
	Blocked

	[{}, {}]

Step with 1

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {}]

Step with 44

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)]
	
	Blocked

	[{}, {}, {}, {}]

Step with 27

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 27

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}]

Covered

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {27[T]}]

Step with 28

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)], 28[(2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0)]
	
	Blocked

	[{}, {}, {}, {}, {27[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 28

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)], 28[(2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0)], 28[(2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0)]
	
	Blocked

	[{}, {}, {}, {}, {27[T]}, {}, {}]

Covered

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)], 28[(2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0)]
	
	Blocked

	[{}, {}, {}, {}, {27[T]}, {28[T]}]

Step with 29

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)], 28[(2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0)], 29[(-2+arg1p30 > 0 /\ -2+arg1 > 0 /\ -2-arg1+arg1p30 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {27[T]}, {28[T]}, {}]

Nonterm

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   1: f1_0_main_Load -> f410_0_main_InvokeMethod : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0), cost: 1
  42: f1_0_main_Load -> f421_0_createForm_LE : arg1'=arg1p1, arg3'=1, arg4'=arg4p1, (1+arg1p1 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  43: f1_0_main_Load -> f410_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1 > 0 /\ arg1p3 > 0 /\ -arg1+arg1p3 <= 0 /\ arg2 > 0), cost: 1
  45: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (-arg1+arg1p6 <= 0 /\ -2+arg2p6 > 0 /\ arg1 > 0 /\ arg1p6 > 0 /\ arg2 > 0), cost: 1
  46: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg1p7 > 0 /\ -2+arg2p7 > 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0 /\ arg2 > 0), cost: 1
  47: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (-2+arg2p8 > 0 /\ -arg1+arg1p8 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ arg2 > 0), cost: 1
  48: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (arg1 > 0 /\ arg1p9 > 0 /\ -arg1+arg1p9 <= 0 /\ -2+arg2p9 > 0 /\ arg2 > 0), cost: 1
  49: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (arg1 > 0 /\ -2+arg2p10 > 0 /\ -arg1+arg1p10 <= 0 /\ arg1p10 > 0 /\ arg2 > 0), cost: 1
  50: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, (arg1 > 0 /\ arg1p11 > 0 /\ -2+arg2p11 > 0 /\ -arg1+arg1p11 <= 0 /\ arg2 > 0), cost: 1
  51: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, (arg1p12 > 0 /\ arg1 > 0 /\ -2+arg2p12 > 0 /\ arg1p12-arg1 <= 0 /\ arg2 > 0), cost: 1
  52: f1_0_main_Load -> f1614_0_main_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, (arg1 > 0 /\ -1+arg2p13 > 0 /\ -1+arg2p13-arg1 <= 0 /\ -arg1+arg1p13 <= 0 /\ arg1p13 > 0 /\ arg2 > 0), cost: 1
  54: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=1+arg3, arg4'=arg4p15, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
  55: f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=1+arg3, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1-arg1 == 0), cost: 1
  56: f421_0_createForm_LE -> f534_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p17, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
  61: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p22, arg4'=arg4p22, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p22 > 0), cost: 1
  63: f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg3 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ -1+arg4p24 > 0 /\ 1-arg1 == 0), cost: 1
  64: f421_0_createForm_LE -> f1752_0_createForm_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=arg4p25, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0), cost: 1
  66: f421_0_createForm_LE -> f421_0_createForm_LE : arg1'=-1+arg1, arg3'=arg3p27, arg4'=arg4p27, (arg3 > 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ arg3-arg2 < 0 /\ -1+arg3p27 > 0), cost: 1
  44: f410_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0), cost: 1
   3: f192_0_createForm_Return -> f410_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (-arg1+arg1p4 <= 0 /\ arg1 > 0 /\ arg1p4 > 0), cost: 1
  27: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p28, arg2'=arg2p28, arg3'=arg3p28, arg4'=arg4p28, (1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0), cost: 1
  28: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p29, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0), cost: 1
  29: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p30, arg2'=arg2p30, arg3'=arg3p30, arg4'=arg4p30, (-2+arg1p30 > 0 /\ -2+arg1 > 0 /\ -2-arg1+arg1p30 <= 0), cost: 1
  30: f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p31, arg2'=arg2p31, arg3'=arg3p31, arg4'=arg4p31, (2-arg1+arg1p31 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p31 > 0), cost: 1
  31: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p32, arg2'=arg2p32, arg3'=arg3p32, arg4'=arg4p32, (1+arg4p32 > 0 /\ 1+arg2p32 > 0 /\ -5+arg1p32 > 0 /\ -4-arg1+arg1p32 <= 0 /\ -1+arg1 > 0 /\ 2+arg2p32-arg1 <= 0 /\ 2-arg1+arg4p32 <= 0), cost: 1
  32: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p33, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (1+arg2p33 > 0 /\ 2+arg4p33-arg1 <= 0 /\ -5+arg1p33 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg2p33 <= 0 /\ 1+arg4p33 > 0 /\ -4+arg1p33-arg1 <= 0), cost: 1
  33: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p34, arg2'=arg2p34, arg3'=arg3p34, arg4'=arg4p34, (-5+arg1p34 > 0 /\ 2-arg1+arg2p34 <= 0 /\ 2+arg4p34-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg4p34 > 0 /\ -4-arg1+arg1p34 <= 0 /\ 1+arg2p34 > 0), cost: 1
  34: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p35, arg2'=arg2p35, arg3'=arg3p35, arg4'=arg4p35, (1+arg4p35 > 0 /\ 1+arg2p35 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg4p35 <= 0 /\ -5+arg1p35 > 0 /\ 2-arg1+arg2p35 <= 0), cost: 1
  35: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p36, arg2'=arg2p36, arg3'=arg3p36, arg4'=arg4p36, (2-arg1+arg4p36 <= 0 /\ -5+arg1p36 > 0 /\ -1+arg1 > 0 /\ 1+arg4p36 > 0 /\ 2+arg2p36-arg1 <= 0 /\ 1+arg2p36 > 0), cost: 1
  36: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p37, arg2'=arg2p37, arg3'=arg3p37, arg4'=arg4p37, (1+arg2p37 > 0 /\ 2-arg1+arg2p37 <= 0 /\ -1+arg1 > 0 /\ 2+arg4p37-arg1 <= 0 /\ 1+arg4p37 > 0 /\ -5+arg1p37 > 0), cost: 1
  37: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p38, arg2'=arg2p38, arg3'=arg3p38, arg4'=arg4p38, (-5+arg1p38 > 0 /\ 2-arg1+arg2p38 <= 0 /\ 1+arg4p38 > 0 /\ 1+arg2p38 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg4p38 <= 0), cost: 1
  38: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p39, arg2'=arg2p39, arg3'=arg3p39, arg4'=arg4p39, (1+arg2p39 > 0 /\ 2-arg1+arg4p39 <= 0 /\ -5+arg1p39 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg2p39 <= 0 /\ 1+arg4p39 > 0), cost: 1
  39: f2239_0_norm_NONNULL -> f2738_0_norm_InvokeMethod : arg1'=arg1p40, arg2'=arg2p40, arg3'=arg3p40, arg4'=arg4p40, (2+arg2p40-arg1 <= 0 /\ 1+arg4p40 > 0 /\ -3+arg1 > 0 /\ -3+arg1p40 > 0 /\ 1+arg2p40 > 0 /\ -arg1+arg1p40 <= 0 /\ 2-arg1+arg4p40 <= 0), cost: 1
  67: f2239_0_norm_NONNULL -> LoAT_sink : (-2+arg1p30 > 0 /\ -2+arg1 > 0 /\ arg1-arg1p30 <= 0 /\ 2+arg1-arg1p30 >= 0), cost: NONTERM
  53: f1614_0_main_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, (arg1 > 0 /\ arg1p14 > 0 /\ -1+arg3 > 0 /\ arg1p14-arg2 <= 0 /\ arg2 > 0), cost: 1
  57: f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p18, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  58: f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg2'=-1+arg1, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg2 == 0), cost: 1
  59: f534_0_createForm_InvokeMethod -> f571_0_createForm_InvokeMethod : arg2'=-1+arg1, arg4'=arg4p20, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  62: f534_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=-1+arg1, arg2'=arg3, arg3'=arg3p23, arg4'=arg4p23, (arg1 > 0 /\ -1+arg4 > 0 /\ -1+arg3p23 > 0 /\ -arg1+arg2 < 0), cost: 1
  60: f571_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p21, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  65: f1752_0_createForm_InvokeMethod -> f421_0_createForm_LE : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p26, (arg1 > 0 /\ -1+arg4 > 0 /\ -arg1+arg2 < 0), cost: 1
  40: f2738_0_norm_InvokeMethod -> f2239_0_norm_NONNULL : arg1'=arg1p41, arg2'=arg2p41, arg3'=arg3p41, arg4'=arg4p41, (1+arg1p41 > 0 /\ arg1p41-arg2 <= 0 /\ 1+arg2 > 0 /\ -3+arg1 > 0 /\ 1+arg4 > 0 /\ arg1p41-arg4 <= 0 /\ 2-arg1+arg1p41 <= 0), cost: 1
  41: __init -> f1_0_main_Load : arg1'=arg1p42, arg2'=arg2p42, arg3'=arg3p42, arg4'=arg4p42, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	f2239_0_norm_NONNULL -> f2239_0_norm_NONNULL : arg1'=arg1p30, arg2'=arg2p30, arg3'=arg3p30, arg4'=arg4p30, (-2+arg1p30 > 0 /\ -2+arg1 > 0 /\ -2-arg1+arg1p30 <= 0), cost: 1
	New rule:
	f2239_0_norm_NONNULL -> LoAT_sink : (-2+arg1p30 > 0 /\ -2+arg1 > 0 /\ arg1-arg1p30 <= 0 /\ 2+arg1-arg1p30 >= 0), cost: NONTERM

		-2+arg1p30 > 0 [0]: monotonic increase yields -2+arg1p30 > 0
		
		-2+arg1 > 0 [0]: eventual decrease yields (-2+arg1p30 > 0 /\ -2+arg1 > 0)
		
		-2+arg1 > 0 [1]: eventual increase yields (-2+arg1 > 0 /\ arg1-arg1p30 <= 0)
		
		2+arg1-arg1p30 >= 0 [0]: monotonic increase yields 2+arg1-arg1p30 >= 0
		
		Replacement map: {-2+arg1p30 > 0 -> -2+arg1p30 > 0, -2+arg1 > 0 -> (-2+arg1 > 0 /\ arg1-arg1p30 <= 0), 2+arg1-arg1p30 >= 0 -> 2+arg1-arg1p30 >= 0}

Step with 67

	Trace

	41[T], 1[(arg1 > 0 /\ -arg1+arg1p2 <= 0 /\ arg1p2 > 0 /\ arg2 > 0)], 44[(arg1 > 0 /\ 1+arg1p5-arg1 <= 0 /\ 1+arg1p5 > 0)], 27[(1+arg1p28 > 0 /\ -1+arg1 > 0 /\ 2-arg1+arg1p28 <= 0)], 28[(2+arg1p29-arg1 <= 0 /\ -1+arg1 > 0 /\ 1+arg1p29 > 0)], 67[(-2+arg1p30 > 0 /\ -2+arg1 > 0 /\ arg1-arg1p30 <= 0 /\ 2+arg1-arg1p30 >= 0)]
	
	Blocked

	[{}, {}, {}, {}, {27[T]}, {28[T]}, {67[T]}]

Refute

	Counterexample

	[ arg1=8 arg2=1 arg3=0 arg4=0 ] 41 [ arg1=8 arg2=0 arg3=0 arg4=0 ] 1 [ arg1=7 arg2=0 arg3=0 arg4=0 ] 44 [ arg1=5 arg2=0 arg3=0 arg4=0 ] 27 [ arg1=3 arg2=0 arg3=0 arg4=0 ] 28 [ arg1=arg1 arg2=arg2 arg3=arg3 arg4=arg4 ] 67
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b