NO

Initial ITS

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5
   0: f1_0_main_Load -> f541_0_createList_GT : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, arg5'=arg5p1, (-arg1p1 == 0 /\ -arg3p1 == 0 /\ arg1 > 0 /\ -arg2p1 == 0 /\ -arg2 == 0), cost: 1
   1: f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, (-arg2p2 == 0 /\ arg1 > 0 /\ arg1p2 > 0 /\ arg2 > 0 /\ -arg1+arg1p2 <= 0), cost: 1
   2: f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, arg5'=arg5p3, (arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0), cost: 1
   5: f1_0_main_Load -> f1347_0_convert_NONNULL : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, (1+arg1p6-arg1 <= 0 /\ arg1 > 0 /\ 1+arg1p6 > 0 /\ -arg2 == 0), cost: 1
   9: f1_0_main_Load -> f1347_0_convert_NONNULL : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, (-1+arg1p10 > 0 /\ arg1 > 0 /\ -1+arg1p10-arg1 <= 0 /\ -arg2 == 0), cost: 1
  18: f541_0_createList_GT -> f541_0_createList_GT : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, arg5'=arg5p19, (1+arg2 > 0 /\ arg3-arg2 >= 0 /\ -arg2p19+arg2 == 0 /\ arg1 > 0 /\ -1 < 0 /\ arg3-arg3p19 == 0 /\ -1-arg1p19+arg1 == 0), cost: 1
  19: f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, arg5'=arg5p20, (-arg1p20+arg1 == 0 /\ -arg3p20+arg2 == 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0 /\ 1+arg3-arg4p20 == 0 /\ -1+arg1-arg2p20 == 0), cost: 1
  20: f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, arg5'=arg5p21, (1+x93 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ arg1-arg1p21 == 0 /\ -arg3p21+arg2 == 0 /\ 1+arg3 > 0 /\ arg1 > 0 /\ 1+arg3-arg4p21 == 0 /\ -1-arg2p21+arg1 == 0), cost: 1
   3: f88_0_main_InvokeMethod -> f541_0_createList_GT : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, arg5'=arg5p4, (arg2p4 > 0 /\ -arg1p4+arg2 == 0 /\ arg1 > 0 /\ 1-arg3p4 == 0), cost: 1
   6: f88_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0), cost: 1
   7: f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (arg1p8-arg1 <= 0 /\ -1+x110 > 0 /\ arg1p8 > 0 /\ arg1 > 0 /\ -arg2 == 0), cost: 1
   8: f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-arg1+arg1p9 <= 0 /\ 1+x114 > 0 /\ arg1 > 0 /\ arg1p9 > 0 /\ -1+x115 > 0 /\ -arg2 == 0), cost: 1
  10: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, (x27 > 0 /\ arg1p11-arg1 <= 0 /\ -arg3p11 == 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
  11: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, (x33 > 0 /\ arg1p12-arg1 <= 0 /\ arg1p12 > 0 /\ -2+arg2p12 > 0 /\ arg1 > 0), cost: 1
  12: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (x40 > 0 /\ -1+arg2p13 > 0 /\ arg1p13 > 0 /\ arg1p13-arg1 <= 0 /\ arg1 > 0), cost: 1
  13: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, (-1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ -arg3p14 == 0 /\ arg1 > 0 /\ x47 > 0 /\ -1+arg2p14 > 0), cost: 1
   4: f257_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, (1+arg1p5-arg1 <= 0 /\ -1+x11 > 0 /\ arg1 > 0 /\ 1+arg1p5 > 0), cost: 1
  22: f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, arg5'=arg5p23, (-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0 /\ -1+x101 < 0), cost: 1
  23: f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, arg5'=arg5p24, (arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0 /\ -1 < 0 /\ x105 > 0), cost: 1
  14: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, (arg1p15 > 0 /\ arg3-arg4p15 == 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg3p15-x52 >= 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
  15: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, (arg2p16-arg2 <= 0 /\ x61-x60 < 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ -arg4p16+arg3 == 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0 /\ 1+x61-arg3p16 == 0), cost: 1
  16: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, arg5'=arg5p17, (x69-x68 < 0 /\ 2+arg3-arg2 <= 0 /\ arg3-arg4p17 == 0 /\ 1+x76 > 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ 1-arg3p17+x69 == 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
  17: f1127_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (arg3 > 0 /\ x77 > 0 /\ 2+arg5-arg2 <= 0 /\ arg1p18 > 0 /\ arg1p18-arg2 <= 0 /\ 2+arg4-arg2 <= 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  21: f736_0_createList_InvokeMethod -> f541_0_createList_GT : arg1'=arg1p22, arg2'=arg2p22, arg3'=arg3p22, arg4'=arg4p22, arg5'=arg5p22, (arg3 > 0 /\ -arg3+arg4 <= 0 /\ -arg1+arg2 < 0 /\ arg1 > 0 /\ -arg1p22+arg2 == 0 /\ arg4-arg3p22 == 0 /\ arg4 > 0 /\ arg3-arg2p22 == 0), cost: 1
  24: __init -> f1_0_main_Load : arg1'=arg1p25, arg2'=arg2p25, arg3'=arg3p25, arg4'=arg4p25, arg5'=arg5p25, T, cost: 1

Simplified Transitions

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5
   2: f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, arg5'=arg5p3, (arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0), cost: 1
   5: f1_0_main_Load -> f1347_0_convert_NONNULL : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, (1+arg1p6-arg1 <= 0 /\ arg1 > 0 /\ 1+arg1p6 > 0 /\ -arg2 == 0), cost: 1
   9: f1_0_main_Load -> f1347_0_convert_NONNULL : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, (-1+arg1p10 > 0 /\ arg1 > 0 /\ -1+arg1p10-arg1 <= 0 /\ -arg2 == 0), cost: 1
  25: f1_0_main_Load -> f541_0_createList_GT : arg1'=0, arg2'=0, arg3'=0, arg4'=arg4p1, arg5'=arg5p1, (arg1 > 0 /\ -arg2 == 0), cost: 1
  26: f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p2, arg2'=0, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, (arg1 > 0 /\ arg1p2 > 0 /\ arg2 > 0 /\ -arg1+arg1p2 <= 0), cost: 1
  39: f541_0_createList_GT -> f541_0_createList_GT : arg1'=-1+arg1, arg4'=arg4p19, arg5'=arg5p19, (1+arg2 > 0 /\ arg3-arg2 >= 0 /\ arg1 > 0), cost: 1
  40: f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p20, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
  41: f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p21, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
   6: f88_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0), cost: 1
  27: f88_0_main_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg2p4, arg3'=1, arg4'=arg4p4, arg5'=arg5p4, (arg2p4 > 0 /\ arg1 > 0), cost: 1
  29: f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (arg1p8-arg1 <= 0 /\ arg1p8 > 0 /\ arg1 > 0 /\ -arg2 == 0), cost: 1
  30: f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-arg1+arg1p9 <= 0 /\ arg1 > 0 /\ arg1p9 > 0 /\ -arg2 == 0), cost: 1
  31: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=0, arg4'=arg4p11, arg5'=arg5p11, (arg1p11-arg1 <= 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
  32: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, (arg1p12-arg1 <= 0 /\ arg1p12 > 0 /\ -2+arg2p12 > 0 /\ arg1 > 0), cost: 1
  33: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (-1+arg2p13 > 0 /\ arg1p13 > 0 /\ arg1p13-arg1 <= 0 /\ arg1 > 0), cost: 1
  34: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=0, arg4'=arg4p14, arg5'=arg5p14, (-1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ arg1 > 0 /\ -1+arg2p14 > 0), cost: 1
  28: f257_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, (1+arg1p5-arg1 <= 0 /\ arg1 > 0 /\ 1+arg1p5 > 0), cost: 1
  43: f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, arg5'=arg5p23, (-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0), cost: 1
  44: f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, arg5'=arg5p24, (arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0), cost: 1
  35: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg3, arg5'=arg5p15, (arg1p15 > 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
  36: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=1+x61, arg4'=arg3, arg5'=arg5p16, (arg2p16-arg2 <= 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0), cost: 1
  37: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=1+x69, arg4'=arg3, arg5'=arg5p17, (2+arg3-arg2 <= 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
  38: f1127_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (arg3 > 0 /\ 2+arg5-arg2 <= 0 /\ arg1p18 > 0 /\ arg1p18-arg2 <= 0 /\ 2+arg4-arg2 <= 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  42: f736_0_createList_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p22, arg5'=arg5p22, (arg3 > 0 /\ -arg3+arg4 <= 0 /\ -arg1+arg2 < 0 /\ arg1 > 0 /\ arg4 > 0), cost: 1
  24: __init -> f1_0_main_Load : arg1'=arg1p25, arg2'=arg2p25, arg3'=arg3p25, arg4'=arg4p25, arg5'=arg5p25, T, cost: 1

	Propagated Equalities

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

	Original rule:
	f1_0_main_Load -> f541_0_createList_GT : arg1'=0, arg2'=0, arg3'=0, arg4'=arg4p1, arg5'=arg5p1, (0 == 0 /\ arg1 > 0 /\ -arg2 == 0), cost: 1
	New rule:
	f1_0_main_Load -> f541_0_createList_GT : arg1'=0, arg2'=0, arg3'=0, arg4'=arg4p1, arg5'=arg5p1, (arg1 > 0 /\ -arg2 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, (-arg2p2 == 0 /\ arg1 > 0 /\ arg1p2 > 0 /\ arg2 > 0 /\ -arg1+arg1p2 <= 0), cost: 1
	New rule:
	f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p2, arg2'=0, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, (0 == 0 /\ arg1 > 0 /\ arg1p2 > 0 /\ arg2 > 0 /\ -arg1+arg1p2 <= 0), cost: 1
	
		propagated equality arg2p2 = 0
		
	Simplified Guard

	Original rule:
	f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p2, arg2'=0, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, (0 == 0 /\ arg1 > 0 /\ arg1p2 > 0 /\ arg2 > 0 /\ -arg1+arg1p2 <= 0), cost: 1
	New rule:
	f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p2, arg2'=0, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, (arg1 > 0 /\ arg1p2 > 0 /\ arg2 > 0 /\ -arg1+arg1p2 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f88_0_main_InvokeMethod -> f541_0_createList_GT : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, arg5'=arg5p4, (arg2p4 > 0 /\ -arg1p4+arg2 == 0 /\ arg1 > 0 /\ 1-arg3p4 == 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg2p4, arg3'=1, arg4'=arg4p4, arg5'=arg5p4, (0 == 0 /\ arg2p4 > 0 /\ arg1 > 0), cost: 1
	
		propagated equality arg1p4 = arg2
		
		propagated equality arg3p4 = 1
		
	Simplified Guard

	Original rule:
	f88_0_main_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg2p4, arg3'=1, arg4'=arg4p4, arg5'=arg5p4, (0 == 0 /\ arg2p4 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg2p4, arg3'=1, arg4'=arg4p4, arg5'=arg5p4, (arg2p4 > 0 /\ arg1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

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

	Original rule:
	f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (arg1p8-arg1 <= 0 /\ -1+x110 > 0 /\ arg1p8 > 0 /\ arg1 > 0 /\ -arg2 == 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (arg1p8-arg1 <= 0 /\ arg1p8 > 0 /\ arg1 > 0 /\ -arg2 == 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-arg1+arg1p9 <= 0 /\ 1+x114 > 0 /\ arg1 > 0 /\ arg1p9 > 0 /\ -1+x115 > 0 /\ -arg2 == 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-arg1+arg1p9 <= 0 /\ arg1 > 0 /\ arg1p9 > 0 /\ -arg2 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, (x27 > 0 /\ arg1p11-arg1 <= 0 /\ -arg3p11 == 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=0, arg4'=arg4p11, arg5'=arg5p11, (0 == 0 /\ x27 > 0 /\ arg1p11-arg1 <= 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
	
		propagated equality arg3p11 = 0
		
	Simplified Guard

	Original rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=0, arg4'=arg4p11, arg5'=arg5p11, (0 == 0 /\ x27 > 0 /\ arg1p11-arg1 <= 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=0, arg4'=arg4p11, arg5'=arg5p11, (x27 > 0 /\ arg1p11-arg1 <= 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=0, arg4'=arg4p11, arg5'=arg5p11, (x27 > 0 /\ arg1p11-arg1 <= 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=0, arg4'=arg4p11, arg5'=arg5p11, (arg1p11-arg1 <= 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

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

	Original rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (x40 > 0 /\ -1+arg2p13 > 0 /\ arg1p13 > 0 /\ arg1p13-arg1 <= 0 /\ arg1 > 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (-1+arg2p13 > 0 /\ arg1p13 > 0 /\ arg1p13-arg1 <= 0 /\ arg1 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, (-1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ -arg3p14 == 0 /\ arg1 > 0 /\ x47 > 0 /\ -1+arg2p14 > 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=0, arg4'=arg4p14, arg5'=arg5p14, (0 == 0 /\ -1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ arg1 > 0 /\ x47 > 0 /\ -1+arg2p14 > 0), cost: 1
	
		propagated equality arg3p14 = 0
		
	Simplified Guard

	Original rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=0, arg4'=arg4p14, arg5'=arg5p14, (0 == 0 /\ -1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ arg1 > 0 /\ x47 > 0 /\ -1+arg2p14 > 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=0, arg4'=arg4p14, arg5'=arg5p14, (-1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ arg1 > 0 /\ x47 > 0 /\ -1+arg2p14 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=0, arg4'=arg4p14, arg5'=arg5p14, (-1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ arg1 > 0 /\ x47 > 0 /\ -1+arg2p14 > 0), cost: 1
	New rule:
	f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=0, arg4'=arg4p14, arg5'=arg5p14, (-1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ arg1 > 0 /\ -1+arg2p14 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, (arg1p15 > 0 /\ arg3-arg4p15 == 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg3p15-x52 >= 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg3, arg5'=arg5p15, (0 == 0 /\ arg1p15 > 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg3p15-x52 >= 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg4p15 = arg3
		
	Simplified Guard

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg3, arg5'=arg5p15, (0 == 0 /\ arg1p15 > 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg3p15-x52 >= 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg3, arg5'=arg5p15, (arg1p15 > 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg3p15-x52 >= 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg3, arg5'=arg5p15, (arg1p15 > 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg3p15-x52 >= 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg3, arg5'=arg5p15, (arg1p15 > 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, (arg2p16-arg2 <= 0 /\ x61-x60 < 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ -arg4p16+arg3 == 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0 /\ 1+x61-arg3p16 == 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=1+x61, arg4'=arg3, arg5'=arg5p16, (0 == 0 /\ arg2p16-arg2 <= 0 /\ x61-x60 < 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg4p16 = arg3
		
		propagated equality arg3p16 = 1+x61
		
	Simplified Guard

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=1+x61, arg4'=arg3, arg5'=arg5p16, (0 == 0 /\ arg2p16-arg2 <= 0 /\ x61-x60 < 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=1+x61, arg4'=arg3, arg5'=arg5p16, (arg2p16-arg2 <= 0 /\ x61-x60 < 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=1+x61, arg4'=arg3, arg5'=arg5p16, (arg2p16-arg2 <= 0 /\ x61-x60 < 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=1+x61, arg4'=arg3, arg5'=arg5p16, (arg2p16-arg2 <= 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, arg5'=arg5p17, (x69-x68 < 0 /\ 2+arg3-arg2 <= 0 /\ arg3-arg4p17 == 0 /\ 1+x76 > 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ 1-arg3p17+x69 == 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=1+x69, arg4'=arg3, arg5'=arg5p17, (0 == 0 /\ x69-x68 < 0 /\ 2+arg3-arg2 <= 0 /\ 1+x76 > 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg4p17 = arg3
		
		propagated equality arg3p17 = 1+x69
		
	Simplified Guard

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=1+x69, arg4'=arg3, arg5'=arg5p17, (0 == 0 /\ x69-x68 < 0 /\ 2+arg3-arg2 <= 0 /\ 1+x76 > 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=1+x69, arg4'=arg3, arg5'=arg5p17, (x69-x68 < 0 /\ 2+arg3-arg2 <= 0 /\ 1+x76 > 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=1+x69, arg4'=arg3, arg5'=arg5p17, (x69-x68 < 0 /\ 2+arg3-arg2 <= 0 /\ 1+x76 > 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=1+x69, arg4'=arg3, arg5'=arg5p17, (2+arg3-arg2 <= 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1127_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (arg3 > 0 /\ x77 > 0 /\ 2+arg5-arg2 <= 0 /\ arg1p18 > 0 /\ arg1p18-arg2 <= 0 /\ 2+arg4-arg2 <= 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f1127_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (arg3 > 0 /\ 2+arg5-arg2 <= 0 /\ arg1p18 > 0 /\ arg1p18-arg2 <= 0 /\ 2+arg4-arg2 <= 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

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

	Original rule:
	f541_0_createList_GT -> f541_0_createList_GT : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p19, arg5'=arg5p19, (0 == 0 /\ 1+arg2 > 0 /\ arg3-arg2 >= 0 /\ arg1 > 0 /\ -1 < 0), cost: 1
	New rule:
	f541_0_createList_GT -> f541_0_createList_GT : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p19, arg5'=arg5p19, (1+arg2 > 0 /\ arg3-arg2 >= 0 /\ arg1 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f541_0_createList_GT -> f541_0_createList_GT : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p19, arg5'=arg5p19, (1+arg2 > 0 /\ arg3-arg2 >= 0 /\ arg1 > 0), cost: 1
	New rule:
	f541_0_createList_GT -> f541_0_createList_GT : arg1'=-1+arg1, arg4'=arg4p19, arg5'=arg5p19, (1+arg2 > 0 /\ arg3-arg2 >= 0 /\ arg1 > 0), cost: 1
	
	Propagated Equalities

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

	Original rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p20, (0 == 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p20, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p20, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p20, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	
	Propagated Equalities

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

	Original rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p21, (0 == 0 /\ 1+x93 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p21, (1+x93 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p21, (1+x93 > 0 /\ 1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p21, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg1'=arg1, arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p21, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p21, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
	
	Propagated Equalities

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

	Original rule:
	f736_0_createList_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p22, arg5'=arg5p22, (0 == 0 /\ arg3 > 0 /\ -arg3+arg4 <= 0 /\ -arg1+arg2 < 0 /\ arg1 > 0 /\ arg4 > 0), cost: 1
	New rule:
	f736_0_createList_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p22, arg5'=arg5p22, (arg3 > 0 /\ -arg3+arg4 <= 0 /\ -arg1+arg2 < 0 /\ arg1 > 0 /\ arg4 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, arg5'=arg5p23, (-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0 /\ -1+x101 < 0), cost: 1
	New rule:
	f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, arg5'=arg5p23, (-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0), cost: 1
	
	Simplified Guard

	Original rule:
	f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, arg5'=arg5p24, (arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0 /\ -1 < 0 /\ x105 > 0), cost: 1
	New rule:
	f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, arg5'=arg5p24, (arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0 /\ x105 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, arg5'=arg5p24, (arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0 /\ x105 > 0), cost: 1
	New rule:
	f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, arg5'=arg5p24, (arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0), cost: 1

Step with 24

	Trace

	24[T]
	
	Blocked

	[{}, {}]

Step with 2

	Trace

	24[T], 2[(arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {}]

Step with 6

	Trace

	24[T], 2[(arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0)], 6[(1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0)]
	
	Blocked

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

Step with 43

	Trace

	24[T], 2[(arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0)], 6[(1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0)], 43[(-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0)]
	
	Blocked

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

Acceleration Failed

marked recursive suffix as redundant

Step with 43

	Trace

	24[T], 2[(arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0)], 6[(1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0)], 43[(-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0)], 43[(-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0)]
	
	Blocked

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

Covered

	Trace

	24[T], 2[(arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0)], 6[(1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0)], 43[(-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0)]
	
	Blocked

	[{}, {}, {}, {}, {43[T]}]

Step with 44

	Trace

	24[T], 2[(arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0)], 6[(1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0)], 43[(-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0)], 44[(arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0)]
	
	Blocked

	[{}, {}, {}, {}, {43[T]}, {}]

Nonterm

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5
   2: f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, arg5'=arg5p3, (arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0), cost: 1
   5: f1_0_main_Load -> f1347_0_convert_NONNULL : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, (1+arg1p6-arg1 <= 0 /\ arg1 > 0 /\ 1+arg1p6 > 0 /\ -arg2 == 0), cost: 1
   9: f1_0_main_Load -> f1347_0_convert_NONNULL : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, (-1+arg1p10 > 0 /\ arg1 > 0 /\ -1+arg1p10-arg1 <= 0 /\ -arg2 == 0), cost: 1
  25: f1_0_main_Load -> f541_0_createList_GT : arg1'=0, arg2'=0, arg3'=0, arg4'=arg4p1, arg5'=arg5p1, (arg1 > 0 /\ -arg2 == 0), cost: 1
  26: f1_0_main_Load -> f88_0_main_InvokeMethod : arg1'=arg1p2, arg2'=0, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, (arg1 > 0 /\ arg1p2 > 0 /\ arg2 > 0 /\ -arg1+arg1p2 <= 0), cost: 1
  39: f541_0_createList_GT -> f541_0_createList_GT : arg1'=-1+arg1, arg4'=arg4p19, arg5'=arg5p19, (1+arg2 > 0 /\ arg3-arg2 >= 0 /\ arg1 > 0), cost: 1
  40: f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p20, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
  41: f541_0_createList_GT -> f736_0_createList_InvokeMethod : arg2'=-1+arg1, arg3'=arg2, arg4'=1+arg3, arg5'=arg5p21, (1+arg2 > 0 /\ arg3-arg2 < 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1
   6: f88_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0), cost: 1
  27: f88_0_main_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg2p4, arg3'=1, arg4'=arg4p4, arg5'=arg5p4, (arg2p4 > 0 /\ arg1 > 0), cost: 1
  29: f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (arg1p8-arg1 <= 0 /\ arg1p8 > 0 /\ arg1 > 0 /\ -arg2 == 0), cost: 1
  30: f88_0_main_InvokeMethod -> f257_0_main_InvokeMethod : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-arg1+arg1p9 <= 0 /\ arg1 > 0 /\ arg1p9 > 0 /\ -arg2 == 0), cost: 1
  31: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p11, arg2'=arg2p11, arg3'=0, arg4'=arg4p11, arg5'=arg5p11, (arg1p11-arg1 <= 0 /\ -2+arg2p11 > 0 /\ arg1p11 > 0 /\ arg1 > 0), cost: 1
  32: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, (arg1p12-arg1 <= 0 /\ arg1p12 > 0 /\ -2+arg2p12 > 0 /\ arg1 > 0), cost: 1
  33: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (-1+arg2p13 > 0 /\ arg1p13 > 0 /\ arg1p13-arg1 <= 0 /\ arg1 > 0), cost: 1
  34: f88_0_main_InvokeMethod -> f972_0_random_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=0, arg4'=arg4p14, arg5'=arg5p14, (-1+arg2p14-arg1 <= 0 /\ arg1p14 > 0 /\ arg1p14-arg1 <= 0 /\ arg1 > 0 /\ -1+arg2p14 > 0), cost: 1
  28: f257_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, (1+arg1p5-arg1 <= 0 /\ arg1 > 0 /\ 1+arg1p5 > 0), cost: 1
  43: f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, arg5'=arg5p23, (-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0), cost: 1
  44: f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, arg5'=arg5p24, (arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0), cost: 1
  45: f1347_0_convert_NONNULL -> LoAT_sink : (arg1p24 > 0 /\ arg1 > 0 /\ -arg1p24+arg1 <= 0 /\ -arg1p24+arg1 >= 0), cost: NONTERM
  35: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg3, arg5'=arg5p15, (arg1p15 > 0 /\ arg1p15-arg1 <= 0 /\ 2+arg3-arg2 <= 0 /\ arg2p15 > 0 /\ 2+arg5p15-arg2 <= 0 /\ arg1 > 0 /\ arg1p15-arg2 <= 0 /\ arg2p15-arg2 <= 0 /\ arg2 > 0), cost: 1
  36: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p16, arg2'=arg2p16, arg3'=1+x61, arg4'=arg3, arg5'=arg5p16, (arg2p16-arg2 <= 0 /\ arg1p16 > 0 /\ 2+arg3-arg2 <= 0 /\ 1+x61 > 0 /\ arg2p16 > 0 /\ arg1p16-arg1 <= 0 /\ arg1 > 0 /\ 2+arg5p16-arg2 <= 0 /\ arg1p16-arg2 <= 0 /\ arg2 > 0), cost: 1
  37: f972_0_random_GT -> f1127_0_main_InvokeMethod : arg1'=arg1p17, arg2'=arg2p17, arg3'=1+x69, arg4'=arg3, arg5'=arg5p17, (2+arg3-arg2 <= 0 /\ 2+arg5p17-arg2 <= 0 /\ arg1p17-arg1 <= 0 /\ 1+x69 > 0 /\ arg1p17 > 0 /\ arg1 > 0 /\ arg1p17-arg2 <= 0 /\ arg2p17 > 0 /\ arg2p17-arg2 <= 0 /\ arg2 > 0), cost: 1
  38: f1127_0_main_InvokeMethod -> f1347_0_convert_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (arg3 > 0 /\ 2+arg5-arg2 <= 0 /\ arg1p18 > 0 /\ arg1p18-arg2 <= 0 /\ 2+arg4-arg2 <= 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  42: f736_0_createList_InvokeMethod -> f541_0_createList_GT : arg1'=arg2, arg2'=arg3, arg3'=arg4, arg4'=arg4p22, arg5'=arg5p22, (arg3 > 0 /\ -arg3+arg4 <= 0 /\ -arg1+arg2 < 0 /\ arg1 > 0 /\ arg4 > 0), cost: 1
  24: __init -> f1_0_main_Load : arg1'=arg1p25, arg2'=arg2p25, arg3'=arg3p25, arg4'=arg4p25, arg5'=arg5p25, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	f1347_0_convert_NONNULL -> f1347_0_convert_NONNULL : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, arg5'=arg5p24, (arg1p24 > 0 /\ arg1p24-arg1 <= 0 /\ arg1 > 0), cost: 1
	New rule:
	f1347_0_convert_NONNULL -> LoAT_sink : (arg1p24 > 0 /\ arg1 > 0 /\ -arg1p24+arg1 <= 0 /\ -arg1p24+arg1 >= 0), cost: NONTERM

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

Step with 45

	Trace

	24[T], 2[(arg1p3-arg1 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ 1+arg2p3 > 0 /\ arg2 > 0)], 6[(1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg1p7-arg1 <= 0 /\ -arg2 == 0)], 43[(-1-arg1p23+arg1 >= 0 /\ 1+arg1p23 > 0 /\ arg1 > 0)], 45[(arg1p24 > 0 /\ arg1 > 0 /\ -arg1p24+arg1 <= 0 /\ -arg1p24+arg1 >= 0)]
	
	Blocked

	[{}, {}, {}, {}, {43[T]}, {45[T]}]

Refute

	Counterexample

	[ arg1=3 arg2=1 arg3=0 arg4=0 arg5=0 ] 24 [ arg1=3 arg2=0 arg3=0 arg4=0 arg5=0 ] 2 [ arg1=2 arg2=0 arg3=0 arg4=0 arg5=0 ] 6 [ arg1=1 arg2=0 arg3=0 arg4=0 arg5=0 ] 43 [ arg1=arg1 arg2=arg2 arg3=arg3 arg4=arg4 arg5=arg5 ] 45
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b