NO

Initial ITS

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5
   0: f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, arg5'=arg5p1, (-2+arg1p1 > 0 /\ arg1 > 0 /\ 1+x4 > 0 /\ -arg3p1+arg2 == 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
   1: f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, (-1+arg1p2 > 0 /\ arg2p2-arg1 <= 0 /\ -arg3p2+arg2 == 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ -1+arg1p2-arg1 <= 0 /\ arg2 > 0), cost: 1
   4: f1_0_main_New -> f69_0__init__GT : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, (1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
   2: f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, arg5'=arg5p3, (-1+arg3 > 0 /\ -arg4p3+arg3 == 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
   3: f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, arg5'=arg5p4, (-1+arg3 > 0 /\ -arg1+arg2p4 <= 0 /\ 2+arg5p4-arg1 <= 0 /\ -2+arg3p4 > 0 /\ -arg4p4+arg3 == 0 /\ arg1p4-arg2 <= 0 /\ arg1p4 > 0 /\ 1+x23 > 0 /\ arg1 > 0 /\ arg2p4 > 0 /\ arg1p4-arg1 <= 0 /\ arg2 > 0), cost: 1
   5: f155_0_main_ArrayAccess -> f69_0__init__GT : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, (-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
   7: f201_0_main_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0), cost: 1
   6: f69_0__init__GT -> f69_0__init__GT : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (-1+arg1-arg1p7 == 0 /\ arg1 > 0 /\ -1 < 0), cost: 1
   8: f226_0_isZero_NONNULL -> f226_0_isZero_NONNULL : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0), cost: 1
   9: f226_0_isZero_NONNULL -> f534_0_div_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, (-1+arg3 > 0 /\ -3+arg2 > 0 /\ -2+arg1p10 > 0 /\ -2+arg1 > 0), cost: 1
  10: f226_0_isZero_NONNULL -> f534_0_div_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, (-1+arg3 > 0 /\ 1+arg1p11-arg1 <= 0 /\ -arg3+arg1p11 <= 0 /\ -1+arg1p11 > 0 /\ -3+arg2 > 0 /\ 2+arg1p11-arg2 <= 0 /\ -2+arg1 > 0), cost: 1
  12: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (-arg2+arg2p13 <= 0 /\ -5+arg2p13 > 0 /\ -5+arg2 > 0 /\ arg1p13 > 0 /\ -3-arg1+arg2p13 <= 0 /\ -2+arg1 > 0 /\ -3+arg3 > 0 /\ -2-arg3+arg2p13 <= 0), cost: 1
  13: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, (arg2p14-arg2 <= 0 /\ -2-arg3+arg2p14 <= 0 /\ arg1p14 > 0 /\ -6+arg2 > 0 /\ -4+arg3 > 0 /\ -6+arg2p14 > 0 /\ -2+arg1 > 0), cost: 1
  14: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, (arg2p15-arg2 <= 0 /\ -6+arg2 > 0 /\ 1-arg1+arg1p15 <= 0 /\ -4+arg3 > 0 /\ 3-arg3+arg1p15 <= 0 /\ 5+arg1p15-arg2 <= 0 /\ -1+arg1p15 > 0 /\ -2+arg1 > 0 /\ -6+arg2p15 > 0 /\ -2+arg2p15-arg3 <= 0), cost: 1
  16: f226_0_isZero_NONNULL -> f287_0_isZero_NONNULL : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, arg5'=arg5p17, (-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0), cost: 1
  11: f534_0_div_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, (arg1p12 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ arg1 > 0 /\ -3+arg2p12-arg1 <= 0 /\ arg1p12-arg1 <= 0 /\ -1-arg1+arg3p12 <= 0), cost: 1
  15: f555_0_div_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, (-4+arg2 > 0 /\ arg1p16 > 0 /\ arg2p16-arg2 <= 0 /\ arg1 > 0 /\ -4+arg2p16 > 0 /\ 2+arg3p16-arg2 <= 0 /\ arg1p16-arg1 <= 0 /\ -2+arg3p16 > 0), cost: 1
  17: f287_0_isZero_NONNULL -> f287_0_isZero_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0), cost: 1
  18: f287_0_isZero_NONNULL -> f321_0_copy_NONNULL : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, arg5'=arg5p19, (1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0), cost: 1
  19: f321_0_copy_NONNULL -> f321_0_copy_NONNULL : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, arg5'=arg5p20, (1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0), cost: 1
  20: __init -> f1_0_main_New : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, arg5'=arg5p21, T, cost: 1

Simplified Transitions

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5
   4: f1_0_main_New -> f69_0__init__GT : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, (1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  21: f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg2, arg4'=arg4p1, arg5'=arg5p1, (-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
  22: f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg2, arg4'=arg4p2, arg5'=arg5p2, (-1+arg1p2 > 0 /\ arg2p2-arg1 <= 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ -1+arg1p2-arg1 <= 0 /\ arg2 > 0), cost: 1
   5: f155_0_main_ArrayAccess -> f69_0__init__GT : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, (-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  23: f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg3, arg5'=arg5p3, (-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
  24: f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg3, arg5'=arg5p4, (-1+arg3 > 0 /\ -arg1+arg2p4 <= 0 /\ 2+arg5p4-arg1 <= 0 /\ -2+arg3p4 > 0 /\ arg1p4-arg2 <= 0 /\ arg1p4 > 0 /\ arg1 > 0 /\ arg2p4 > 0 /\ arg1p4-arg1 <= 0 /\ arg2 > 0), cost: 1
   7: f201_0_main_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0), cost: 1
  25: f69_0__init__GT -> f69_0__init__GT : arg1'=-1+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg1 > 0, cost: 1
   8: f226_0_isZero_NONNULL -> f226_0_isZero_NONNULL : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0), cost: 1
   9: f226_0_isZero_NONNULL -> f534_0_div_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, (-1+arg3 > 0 /\ -3+arg2 > 0 /\ -2+arg1p10 > 0 /\ -2+arg1 > 0), cost: 1
  10: f226_0_isZero_NONNULL -> f534_0_div_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, (-1+arg3 > 0 /\ 1+arg1p11-arg1 <= 0 /\ -arg3+arg1p11 <= 0 /\ -1+arg1p11 > 0 /\ -3+arg2 > 0 /\ 2+arg1p11-arg2 <= 0 /\ -2+arg1 > 0), cost: 1
  12: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (-arg2+arg2p13 <= 0 /\ -5+arg2p13 > 0 /\ -5+arg2 > 0 /\ arg1p13 > 0 /\ -3-arg1+arg2p13 <= 0 /\ -2+arg1 > 0 /\ -3+arg3 > 0 /\ -2-arg3+arg2p13 <= 0), cost: 1
  13: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, (arg2p14-arg2 <= 0 /\ -2-arg3+arg2p14 <= 0 /\ arg1p14 > 0 /\ -6+arg2 > 0 /\ -4+arg3 > 0 /\ -6+arg2p14 > 0 /\ -2+arg1 > 0), cost: 1
  14: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, (arg2p15-arg2 <= 0 /\ -6+arg2 > 0 /\ 1-arg1+arg1p15 <= 0 /\ -4+arg3 > 0 /\ 3-arg3+arg1p15 <= 0 /\ 5+arg1p15-arg2 <= 0 /\ -1+arg1p15 > 0 /\ -2+arg1 > 0 /\ -6+arg2p15 > 0 /\ -2+arg2p15-arg3 <= 0), cost: 1
  16: f226_0_isZero_NONNULL -> f287_0_isZero_NONNULL : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, arg5'=arg5p17, (-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0), cost: 1
  11: f534_0_div_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, (arg1p12 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ arg1 > 0 /\ -3+arg2p12-arg1 <= 0 /\ arg1p12-arg1 <= 0 /\ -1-arg1+arg3p12 <= 0), cost: 1
  15: f555_0_div_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, (-4+arg2 > 0 /\ arg1p16 > 0 /\ arg2p16-arg2 <= 0 /\ arg1 > 0 /\ -4+arg2p16 > 0 /\ 2+arg3p16-arg2 <= 0 /\ arg1p16-arg1 <= 0 /\ -2+arg3p16 > 0), cost: 1
  17: f287_0_isZero_NONNULL -> f287_0_isZero_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0), cost: 1
  18: f287_0_isZero_NONNULL -> f321_0_copy_NONNULL : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, arg5'=arg5p19, (1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0), cost: 1
  19: f321_0_copy_NONNULL -> f321_0_copy_NONNULL : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, arg5'=arg5p20, (1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0), cost: 1
  20: __init -> f1_0_main_New : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, arg5'=arg5p21, T, cost: 1

	Propagated Equalities

	Original rule:
	f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, arg5'=arg5p1, (-2+arg1p1 > 0 /\ arg1 > 0 /\ 1+x4 > 0 /\ -arg3p1+arg2 == 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg2, arg4'=arg4p1, arg5'=arg5p1, (0 == 0 /\ -2+arg1p1 > 0 /\ arg1 > 0 /\ 1+x4 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg3p1 = arg2
		
	Simplified Guard

	Original rule:
	f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg2, arg4'=arg4p1, arg5'=arg5p1, (0 == 0 /\ -2+arg1p1 > 0 /\ arg1 > 0 /\ 1+x4 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg2, arg4'=arg4p1, arg5'=arg5p1, (-2+arg1p1 > 0 /\ arg1 > 0 /\ 1+x4 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg2, arg4'=arg4p1, arg5'=arg5p1, (-2+arg1p1 > 0 /\ arg1 > 0 /\ 1+x4 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg2, arg4'=arg4p1, arg5'=arg5p1, (-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

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

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

	Original rule:
	f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, arg5'=arg5p3, (-1+arg3 > 0 /\ -arg4p3+arg3 == 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg3, arg5'=arg5p3, (0 == 0 /\ -1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg4p3 = arg3
		
	Simplified Guard

	Original rule:
	f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg3, arg5'=arg5p3, (0 == 0 /\ -1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg3, arg5'=arg5p3, (-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

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

	Original rule:
	f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg3, arg5'=arg5p4, (0 == 0 /\ -1+arg3 > 0 /\ -arg1+arg2p4 <= 0 /\ 2+arg5p4-arg1 <= 0 /\ -2+arg3p4 > 0 /\ arg1p4-arg2 <= 0 /\ arg1p4 > 0 /\ 1+x23 > 0 /\ arg1 > 0 /\ arg2p4 > 0 /\ arg1p4-arg1 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg3, arg5'=arg5p4, (-1+arg3 > 0 /\ -arg1+arg2p4 <= 0 /\ 2+arg5p4-arg1 <= 0 /\ -2+arg3p4 > 0 /\ arg1p4-arg2 <= 0 /\ arg1p4 > 0 /\ 1+x23 > 0 /\ arg1 > 0 /\ arg2p4 > 0 /\ arg1p4-arg1 <= 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg3, arg5'=arg5p4, (-1+arg3 > 0 /\ -arg1+arg2p4 <= 0 /\ 2+arg5p4-arg1 <= 0 /\ -2+arg3p4 > 0 /\ arg1p4-arg2 <= 0 /\ arg1p4 > 0 /\ 1+x23 > 0 /\ arg1 > 0 /\ arg2p4 > 0 /\ arg1p4-arg1 <= 0 /\ arg2 > 0), cost: 1
	New rule:
	f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg3, arg5'=arg5p4, (-1+arg3 > 0 /\ -arg1+arg2p4 <= 0 /\ 2+arg5p4-arg1 <= 0 /\ -2+arg3p4 > 0 /\ arg1p4-arg2 <= 0 /\ arg1p4 > 0 /\ arg1 > 0 /\ arg2p4 > 0 /\ arg1p4-arg1 <= 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f69_0__init__GT -> f69_0__init__GT : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (-1+arg1-arg1p7 == 0 /\ arg1 > 0 /\ -1 < 0), cost: 1
	New rule:
	f69_0__init__GT -> f69_0__init__GT : arg1'=-1+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (0 == 0 /\ arg1 > 0 /\ -1 < 0), cost: 1
	
		propagated equality arg1p7 = -1+arg1
		
	Simplified Guard

	Original rule:
	f69_0__init__GT -> f69_0__init__GT : arg1'=-1+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (0 == 0 /\ arg1 > 0 /\ -1 < 0), cost: 1
	New rule:
	f69_0__init__GT -> f69_0__init__GT : arg1'=-1+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg1 > 0, cost: 1

Step with 20

	Trace

	20[T]
	
	Blocked

	[{}, {}]

Step with 4

	Trace

	20[T], 4[(1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {}]

Step with 25

	Trace

	20[T], 4[(1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0)], 25[(arg1 > 0)]
	
	Blocked

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

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5
   4: f1_0_main_New -> f69_0__init__GT : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, (1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  21: f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg2, arg4'=arg4p1, arg5'=arg5p1, (-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
  22: f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg2, arg4'=arg4p2, arg5'=arg5p2, (-1+arg1p2 > 0 /\ arg2p2-arg1 <= 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ -1+arg1p2-arg1 <= 0 /\ arg2 > 0), cost: 1
   5: f155_0_main_ArrayAccess -> f69_0__init__GT : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, (-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  23: f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg3, arg5'=arg5p3, (-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
  24: f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg3, arg5'=arg5p4, (-1+arg3 > 0 /\ -arg1+arg2p4 <= 0 /\ 2+arg5p4-arg1 <= 0 /\ -2+arg3p4 > 0 /\ arg1p4-arg2 <= 0 /\ arg1p4 > 0 /\ arg1 > 0 /\ arg2p4 > 0 /\ arg1p4-arg1 <= 0 /\ arg2 > 0), cost: 1
   7: f201_0_main_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0), cost: 1
  25: f69_0__init__GT -> f69_0__init__GT : arg1'=-1+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg1 > 0, cost: 1
  26: f69_0__init__GT -> f69_0__init__GT : arg1'=-n+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (-1+n >= 0 /\ 1-n+arg1 > 0), cost: 1
   8: f226_0_isZero_NONNULL -> f226_0_isZero_NONNULL : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0), cost: 1
   9: f226_0_isZero_NONNULL -> f534_0_div_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, (-1+arg3 > 0 /\ -3+arg2 > 0 /\ -2+arg1p10 > 0 /\ -2+arg1 > 0), cost: 1
  10: f226_0_isZero_NONNULL -> f534_0_div_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, (-1+arg3 > 0 /\ 1+arg1p11-arg1 <= 0 /\ -arg3+arg1p11 <= 0 /\ -1+arg1p11 > 0 /\ -3+arg2 > 0 /\ 2+arg1p11-arg2 <= 0 /\ -2+arg1 > 0), cost: 1
  12: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (-arg2+arg2p13 <= 0 /\ -5+arg2p13 > 0 /\ -5+arg2 > 0 /\ arg1p13 > 0 /\ -3-arg1+arg2p13 <= 0 /\ -2+arg1 > 0 /\ -3+arg3 > 0 /\ -2-arg3+arg2p13 <= 0), cost: 1
  13: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, (arg2p14-arg2 <= 0 /\ -2-arg3+arg2p14 <= 0 /\ arg1p14 > 0 /\ -6+arg2 > 0 /\ -4+arg3 > 0 /\ -6+arg2p14 > 0 /\ -2+arg1 > 0), cost: 1
  14: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, (arg2p15-arg2 <= 0 /\ -6+arg2 > 0 /\ 1-arg1+arg1p15 <= 0 /\ -4+arg3 > 0 /\ 3-arg3+arg1p15 <= 0 /\ 5+arg1p15-arg2 <= 0 /\ -1+arg1p15 > 0 /\ -2+arg1 > 0 /\ -6+arg2p15 > 0 /\ -2+arg2p15-arg3 <= 0), cost: 1
  16: f226_0_isZero_NONNULL -> f287_0_isZero_NONNULL : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, arg5'=arg5p17, (-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0), cost: 1
  11: f534_0_div_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, (arg1p12 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ arg1 > 0 /\ -3+arg2p12-arg1 <= 0 /\ arg1p12-arg1 <= 0 /\ -1-arg1+arg3p12 <= 0), cost: 1
  15: f555_0_div_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, (-4+arg2 > 0 /\ arg1p16 > 0 /\ arg2p16-arg2 <= 0 /\ arg1 > 0 /\ -4+arg2p16 > 0 /\ 2+arg3p16-arg2 <= 0 /\ arg1p16-arg1 <= 0 /\ -2+arg3p16 > 0), cost: 1
  17: f287_0_isZero_NONNULL -> f287_0_isZero_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0), cost: 1
  18: f287_0_isZero_NONNULL -> f321_0_copy_NONNULL : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, arg5'=arg5p19, (1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0), cost: 1
  19: f321_0_copy_NONNULL -> f321_0_copy_NONNULL : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, arg5'=arg5p20, (1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0), cost: 1
  20: __init -> f1_0_main_New : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, arg5'=arg5p21, T, cost: 1

	Loop Acceleration

	Original rule:
	f69_0__init__GT -> f69_0__init__GT : arg1'=-1+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (arg1 > 0), cost: 1
	New rule:
	f69_0__init__GT -> f69_0__init__GT : arg1'=-n+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (-1+n >= 0 /\ 1-n+arg1 > 0), cost: 1

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

	Trace

	20[T], 4[(1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0)], 26[(-1+n >= 0 /\ 1-n+arg1 > 0)]
	
	Blocked

	[{}, {}, {}, {25[T], 26[T]}]

Backtrack

	Trace

	20[T], 4[(1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {26[T]}]

Step with 25

	Trace

	20[T], 4[(1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0)], 25[(arg1 > 0)]
	
	Blocked

	[{}, {}, {26[T]}, {}]

Covered

	Trace

	20[T], 4[(1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {25[T], 26[T]}]

Backtrack

	Trace

	20[T]
	
	Blocked

	[{}, {4[T]}]

Step with 21

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {}]

Step with 5

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 5[(-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {}, {}]

Step with 25

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 5[(-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0)], 25[(arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {}, {}, {}]

Covered

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 5[(-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {}, {25[T]}]

Step with 26

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 5[(-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0)], 26[(-1+n >= 0 /\ 1-n+arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {}, {25[T]}, {26[T]}]

Step with 25

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 5[(-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0)], 26[(-1+n >= 0 /\ 1-n+arg1 > 0)], 25[(arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {}, {25[T]}, {26[T]}, {}]

Covered

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 5[(-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0)], 26[(-1+n >= 0 /\ 1-n+arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {}, {25[T]}, {25[T], 26[T]}]

Backtrack

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 5[(-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {}, {25[T], 26[T]}]

Backtrack

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}]

Step with 23

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}]

Step with 7

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}]

Step with 16

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {}]

Step with 18

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {}, {}]

Step with 19

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)], 19[(1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 19

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)], 19[(1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0)], 19[(1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {}, {}, {}, {}]

Covered

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)], 19[(1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {}, {}, {19[T]}]

Backtrack

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {}, {19[T]}]

Backtrack

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}]

Step with 17

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 17

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {}, {}]

Covered

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {17[T]}]

Step with 18

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {17[T]}, {}]

Step with 19

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)], 19[(1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {17[T]}, {}, {}]

Step with 19

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)], 19[(1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0)], 19[(1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {17[T]}, {}, {}, {}]

Covered

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)], 19[(1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {17[T]}, {}, {19[T]}]

Backtrack

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)], 18[(1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {17[T]}, {19[T]}]

Backtrack

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)], 17[(-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {18[T]}, {17[T], 18[T]}]

Backtrack

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 16[(-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {}, {17[T], 18[T]}]

Backtrack

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {16[T]}]

Step with 8

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 8[(-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {16[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 8

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 8[(-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0)], 8[(-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {16[T]}, {}, {}]

Covered

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 8[(-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {16[T]}, {8[T]}]

Step with 9

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 8[(-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0)], 9[(-1+arg3 > 0 /\ -3+arg2 > 0 /\ -2+arg1p10 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {16[T]}, {8[T]}, {}]

Step with 11

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 8[(-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0)], 9[(-1+arg3 > 0 /\ -3+arg2 > 0 /\ -2+arg1p10 > 0 /\ -2+arg1 > 0)], 11[(arg1p12 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ arg1 > 0 /\ -3+arg2p12-arg1 <= 0 /\ arg1p12-arg1 <= 0 /\ -1-arg1+arg3p12 <= 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {16[T]}, {8[T]}, {}, {}]

Nonterm

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5
   4: f1_0_main_New -> f69_0__init__GT : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, (1+arg1p5 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  21: f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg2, arg4'=arg4p1, arg5'=arg5p1, (-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0), cost: 1
  22: f1_0_main_New -> f155_0_main_ArrayAccess : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg2, arg4'=arg4p2, arg5'=arg5p2, (-1+arg1p2 > 0 /\ arg2p2-arg1 <= 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ -1+arg1p2-arg1 <= 0 /\ arg2 > 0), cost: 1
   5: f155_0_main_ArrayAccess -> f69_0__init__GT : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, (-1+arg3 > 0 /\ 1+arg1p6 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  23: f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg3, arg5'=arg5p3, (-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
  24: f155_0_main_ArrayAccess -> f201_0_main_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg3, arg5'=arg5p4, (-1+arg3 > 0 /\ -arg1+arg2p4 <= 0 /\ 2+arg5p4-arg1 <= 0 /\ -2+arg3p4 > 0 /\ arg1p4-arg2 <= 0 /\ arg1p4 > 0 /\ arg1 > 0 /\ arg2p4 > 0 /\ arg1p4-arg1 <= 0 /\ arg2 > 0), cost: 1
   7: f201_0_main_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, (-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0), cost: 1
  25: f69_0__init__GT -> f69_0__init__GT : arg1'=-1+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg1 > 0, cost: 1
  26: f69_0__init__GT -> f69_0__init__GT : arg1'=-n+arg1, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, (-1+n >= 0 /\ 1-n+arg1 > 0), cost: 1
   8: f226_0_isZero_NONNULL -> f226_0_isZero_NONNULL : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, (-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0), cost: 1
   9: f226_0_isZero_NONNULL -> f534_0_div_InvokeMethod : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, (-1+arg3 > 0 /\ -3+arg2 > 0 /\ -2+arg1p10 > 0 /\ -2+arg1 > 0), cost: 1
  10: f226_0_isZero_NONNULL -> f534_0_div_InvokeMethod : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, (-1+arg3 > 0 /\ 1+arg1p11-arg1 <= 0 /\ -arg3+arg1p11 <= 0 /\ -1+arg1p11 > 0 /\ -3+arg2 > 0 /\ 2+arg1p11-arg2 <= 0 /\ -2+arg1 > 0), cost: 1
  12: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, (-arg2+arg2p13 <= 0 /\ -5+arg2p13 > 0 /\ -5+arg2 > 0 /\ arg1p13 > 0 /\ -3-arg1+arg2p13 <= 0 /\ -2+arg1 > 0 /\ -3+arg3 > 0 /\ -2-arg3+arg2p13 <= 0), cost: 1
  13: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, (arg2p14-arg2 <= 0 /\ -2-arg3+arg2p14 <= 0 /\ arg1p14 > 0 /\ -6+arg2 > 0 /\ -4+arg3 > 0 /\ -6+arg2p14 > 0 /\ -2+arg1 > 0), cost: 1
  14: f226_0_isZero_NONNULL -> f555_0_div_InvokeMethod : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, (arg2p15-arg2 <= 0 /\ -6+arg2 > 0 /\ 1-arg1+arg1p15 <= 0 /\ -4+arg3 > 0 /\ 3-arg3+arg1p15 <= 0 /\ 5+arg1p15-arg2 <= 0 /\ -1+arg1p15 > 0 /\ -2+arg1 > 0 /\ -6+arg2p15 > 0 /\ -2+arg2p15-arg3 <= 0), cost: 1
  16: f226_0_isZero_NONNULL -> f287_0_isZero_NONNULL : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, arg5'=arg5p17, (-2+arg2 > 0 /\ arg2p17 > 0 /\ 1+arg3p17 > 0 /\ 3+arg3p17-arg2 <= 0 /\ 2+arg2p17-arg2 <= 0 /\ arg3 > 0 /\ 2-arg1+arg1p17 <= 0 /\ 1+arg3p17-arg3 <= 0 /\ arg2p17-arg3 <= 0 /\ -2+arg1 > 0 /\ arg1p17 > 0), cost: 1
  27: f226_0_isZero_NONNULL -> LoAT_sink : (-1+arg3 > 0 /\ arg3-arg3p12 <= 0 /\ -arg2p12+arg2 <= 0 /\ arg1p12 > 0 /\ -3+arg2 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ -arg1p12+arg1 <= 0 /\ -2+arg1 > 0), cost: NONTERM
  11: f534_0_div_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, (arg1p12 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ arg1 > 0 /\ -3+arg2p12-arg1 <= 0 /\ arg1p12-arg1 <= 0 /\ -1-arg1+arg3p12 <= 0), cost: 1
  15: f555_0_div_InvokeMethod -> f226_0_isZero_NONNULL : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, (-4+arg2 > 0 /\ arg1p16 > 0 /\ arg2p16-arg2 <= 0 /\ arg1 > 0 /\ -4+arg2p16 > 0 /\ 2+arg3p16-arg2 <= 0 /\ arg1p16-arg1 <= 0 /\ -2+arg3p16 > 0), cost: 1
  17: f287_0_isZero_NONNULL -> f287_0_isZero_NONNULL : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, arg5'=arg5p18, (-2+arg2 > 0 /\ 2+arg2p18-arg2 <= 0 /\ -arg3+arg2p18 <= 0 /\ arg1p18 > 0 /\ 1+arg3p18-arg3 <= 0 /\ arg3 > 0 /\ 2+arg1p18-arg1 <= 0 /\ arg2p18 > 0 /\ 1+arg3p18 > 0 /\ 3+arg3p18-arg2 <= 0 /\ -2+arg1 > 0), cost: 1
  18: f287_0_isZero_NONNULL -> f321_0_copy_NONNULL : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, arg5'=arg5p19, (1+arg2p19-arg1 <= 0 /\ 1+arg2p19 > 0 /\ arg1 > 0 /\ -arg1+arg1p19 <= 0 /\ 1+arg3 > 0 /\ arg1p19 > 0 /\ -1+arg2 > 0), cost: 1
  19: f321_0_copy_NONNULL -> f321_0_copy_NONNULL : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, arg5'=arg5p20, (1+arg2p20 > 0 /\ 1+arg2p20-arg2 <= 0 /\ arg1p20-arg2 <= 0 /\ arg1p20 > 0 /\ 2+arg1p20-arg1 <= 0 /\ -2+arg1 > 0 /\ 3-arg1+arg2p20 <= 0 /\ arg2 > 0), cost: 1
  20: __init -> f1_0_main_New : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, arg5'=arg5p21, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	f226_0_isZero_NONNULL -> f226_0_isZero_NONNULL : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, (-1+arg3 > 0 /\ arg1p12 > 0 /\ -3+arg2 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ -2+arg1 > 0), cost: 1
	New rule:
	f226_0_isZero_NONNULL -> LoAT_sink : (-1+arg3 > 0 /\ arg3-arg3p12 <= 0 /\ -arg2p12+arg2 <= 0 /\ arg1p12 > 0 /\ -3+arg2 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ -arg1p12+arg1 <= 0 /\ -2+arg1 > 0), cost: NONTERM

		-1+arg3 > 0 [0]: eventual decrease yields (-1+arg3 > 0 /\ -1+arg3p12 > 0)
		
		-1+arg3 > 0 [1]: eventual increase yields (-1+arg3 > 0 /\ arg3-arg3p12 <= 0)
		
		arg1p12 > 0 [0]: monotonic increase yields arg1p12 > 0
		
		-3+arg2 > 0 [0]: eventual decrease yields (-3+arg2 > 0 /\ -3+arg2p12 > 0)
		
		-3+arg2 > 0 [1]: eventual increase yields (-arg2p12+arg2 <= 0 /\ -3+arg2 > 0)
		
		-3+arg2p12 > 0 [0]: monotonic increase yields -3+arg2p12 > 0
		
		-1+arg3p12 > 0 [0]: monotonic increase yields -1+arg3p12 > 0
		
		-2+arg1 > 0 [0]: eventual decrease yields (-2+arg1p12 > 0 /\ -2+arg1 > 0)
		
		-2+arg1 > 0 [1]: eventual increase yields (-arg1p12+arg1 <= 0 /\ -2+arg1 > 0)
		
		Replacement map: {-1+arg3 > 0 -> (-1+arg3 > 0 /\ arg3-arg3p12 <= 0), arg1p12 > 0 -> arg1p12 > 0, -3+arg2 > 0 -> (-arg2p12+arg2 <= 0 /\ -3+arg2 > 0), -3+arg2p12 > 0 -> -3+arg2p12 > 0, -1+arg3p12 > 0 -> -1+arg3p12 > 0, -2+arg1 > 0 -> (-arg1p12+arg1 <= 0 /\ -2+arg1 > 0)}

Step with 27

	Trace

	20[T], 21[(-2+arg1p1 > 0 /\ arg1 > 0 /\ arg2p1 > 0 /\ -arg1+arg2p1 <= 0 /\ arg2 > 0)], 23[(-1+arg3 > 0 /\ -arg1p3+arg1 >= 0 /\ -1+arg3p3 > 0 /\ -2+arg1-arg5p3 >= 0 /\ -1+arg3p3-arg2 <= 0 /\ arg1p3 > 0 /\ arg1 > 0 /\ arg1p3-arg2 <= 0 /\ arg1-arg2p3 >= 0 /\ 1-arg3p3+arg1 >= 0 /\ arg2p3 > 0 /\ arg2 > 0)], 7[(-1+arg4 > 0 /\ arg3 > 0 /\ 1+arg3p8-arg3 <= 0 /\ arg1 > 0 /\ arg1p8 > 0 /\ 1+arg3p8 > 0 /\ -arg3+arg2p8 <= 0 /\ arg1p8-arg2 <= 0 /\ arg2p8 > 0 /\ arg2 > 0 /\ 2+arg5-arg2 <= 0)], 8[(-4+arg2 > 0 /\ -1+arg1p9 > 0 /\ -4+arg2p9 > 0 /\ arg2p9-arg2 <= 0 /\ -2+arg3p9 > 0 /\ 3+arg1p9-arg2 <= 0 /\ -2+arg2p9-arg3 <= 0 /\ -arg3+arg3p9 <= 0 /\ -2+arg1 > 0 /\ 1+arg1p9-arg3 <= 0 /\ 1+arg1p9-arg1 <= 0 /\ 2+arg3p9-arg2 <= 0 /\ -2+arg3 > 0)], 27[(-1+arg3 > 0 /\ arg3-arg3p12 <= 0 /\ -arg2p12+arg2 <= 0 /\ arg1p12 > 0 /\ -3+arg2 > 0 /\ -3+arg2p12 > 0 /\ -1+arg3p12 > 0 /\ -arg1p12+arg1 <= 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {4[T]}, {5[T]}, {}, {16[T]}, {8[T]}, {27[T]}]

Refute

	Counterexample

	[ arg1=6 arg2=2 arg3=0 arg4=0 arg5=0 ] 20 [ arg1=9 arg2=6 arg3=2 arg4=0 arg5=0 ] 21 [ arg1=1 arg2=9 arg3=7 arg4=2 arg5=-1 ] 23 [ arg1=9 arg2=7 arg3=5 arg4=0 arg5=0 ] 7 [ arg1=3 arg2=5 arg3=3 arg4=0 arg5=0 ] 8 [ arg1=arg1 arg2=arg2 arg3=arg3 arg4=arg4 arg5=arg5 ] 27
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b