NO

Initial ITS

Start location: __init
Program variables: arg1 arg2 arg3
   0: f1_0_main_ConstantStackPush -> f99_0_loop_aux_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg2 > 0 /\ -arg2p1 == 0 /\ -arg1p1 == 0 /\ arg1 > 0 /\ -arg3p1+10*arg2 == 0), cost: 1
   1: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (-arg2p2+arg3 == 0 /\ -10+arg3 < 0 /\ arg1-arg1p2 == 0 /\ -arg3p2+arg2 == 0 /\ -1+arg3 > 0), cost: 1
   2: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (-10+arg3 > 0 /\ -arg2p3+arg3 == 0 /\ arg1-arg1p3 == 0 /\ -arg3p3+arg2 == 0), cost: 1
   4: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, (1-arg1p5 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0 /\ 1-arg2p5 == 0 /\ 2-arg3p5 == 0), cost: 1
   5: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, (9-arg3p6 == 0 /\ -arg1p6 == 0 /\ 10-arg3 == 0 /\ -2+arg1 < 0 /\ -arg2p6 == 0), cost: 1
   3: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, (-arg2p4 == 0 /\ -arg3 == 0 /\ -1-arg3p4+arg2 == 0 /\ -arg1p4 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
   6: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, (1-arg1p7 == 0 /\ 1-arg3p7+arg2 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0 /\ 1-arg2p7 == 0 /\ -1+arg2 > 0), cost: 1
   7: __init -> f1_0_main_ConstantStackPush : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, T, cost: 1

Chained Linear Paths

Start location: __init
Program variables: arg1 arg2 arg3
   1: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (-arg2p2+arg3 == 0 /\ -10+arg3 < 0 /\ arg1-arg1p2 == 0 /\ -arg3p2+arg2 == 0 /\ -1+arg3 > 0), cost: 1
   2: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (-10+arg3 > 0 /\ -arg2p3+arg3 == 0 /\ arg1-arg1p3 == 0 /\ -arg3p3+arg2 == 0), cost: 1
   4: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, (1-arg1p5 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0 /\ 1-arg2p5 == 0 /\ 2-arg3p5 == 0), cost: 1
   5: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, (9-arg3p6 == 0 /\ -arg1p6 == 0 /\ 10-arg3 == 0 /\ -2+arg1 < 0 /\ -arg2p6 == 0), cost: 1
   3: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, (-arg2p4 == 0 /\ -arg3 == 0 /\ -1-arg3p4+arg2 == 0 /\ -arg1p4 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
   6: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, (1-arg1p7 == 0 /\ 1-arg3p7+arg2 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0 /\ 1-arg2p7 == 0 /\ -1+arg2 > 0), cost: 1
   8: __init -> f99_0_loop_aux_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (-arg2p1 == 0 /\ -arg3p1+10*arg2p8 == 0 /\ arg1p8 > 0 /\ 1+arg2p8 > 0 /\ -arg1p1 == 0), cost: 1

	Eliminating location f1_0_main_ConstantStackPush by chaining:

	Applied chaining

	First rule:
	__init -> f1_0_main_ConstantStackPush : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, T, cost: 1
	Second rule:
	f1_0_main_ConstantStackPush -> f99_0_loop_aux_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg2 > 0 /\ -arg2p1 == 0 /\ -arg1p1 == 0 /\ arg1 > 0 /\ -arg3p1+10*arg2 == 0), cost: 1
	New rule:
	__init -> f99_0_loop_aux_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (-arg2p1 == 0 /\ -arg3p1+10*arg2p8 == 0 /\ arg1p8 > 0 /\ 1+arg2p8 > 0 /\ -arg1p1 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 7

Simplified Transitions

Start location: __init
Program variables: arg1 arg2 arg3
   9: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, (-10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
  10: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, -10+arg3 > 0, cost: 1
  12: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2, (1-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  13: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=9, (10-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  11: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg2, (-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  14: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg2, (1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  15: __init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (1+arg2p8 > 0), cost: 1

	Propagated Equalities

	Original rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (-arg2p2+arg3 == 0 /\ -10+arg3 < 0 /\ arg1-arg1p2 == 0 /\ -arg3p2+arg2 == 0 /\ -1+arg3 > 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1, arg2'=arg3, arg3'=arg2, (0 == 0 /\ -10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
	
		propagated equality arg2p2 = arg3
		
		propagated equality arg1p2 = arg1
		
		propagated equality arg3p2 = arg2
		
	Simplified Guard

	Original rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1, arg2'=arg3, arg3'=arg2, (0 == 0 /\ -10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1, arg2'=arg3, arg3'=arg2, (-10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1, arg2'=arg3, arg3'=arg2, (-10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, (-10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (-10+arg3 > 0 /\ -arg2p3+arg3 == 0 /\ arg1-arg1p3 == 0 /\ -arg3p3+arg2 == 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1, arg2'=arg3, arg3'=arg2, (0 == 0 /\ -10+arg3 > 0), cost: 1
	
		propagated equality arg2p3 = arg3
		
		propagated equality arg1p3 = arg1
		
		propagated equality arg3p3 = arg2
		
	Simplified Guard

	Original rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1, arg2'=arg3, arg3'=arg2, (0 == 0 /\ -10+arg3 > 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1, arg2'=arg3, arg3'=arg2, -10+arg3 > 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg1'=arg1, arg2'=arg3, arg3'=arg2, -10+arg3 > 0, cost: 1
	New rule:
	f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, -10+arg3 > 0, cost: 1
	
	Propagated Equalities

	Original rule:
	f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, (-arg2p4 == 0 /\ -arg3 == 0 /\ -1-arg3p4+arg2 == 0 /\ -arg1p4 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
	New rule:
	f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg2, (0 == 0 /\ -arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
	
		propagated equality arg2p4 = 0
		
		propagated equality arg3p4 = -1+arg2
		
		propagated equality arg1p4 = 0
		
	Simplified Guard

	Original rule:
	f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg2, (0 == 0 /\ -arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
	New rule:
	f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg2, (-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, (1-arg1p5 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0 /\ 1-arg2p5 == 0 /\ 2-arg3p5 == 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2, (0 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0), cost: 1
	
		propagated equality arg1p5 = 1
		
		propagated equality arg2p5 = 1
		
		propagated equality arg3p5 = 2
		
	Simplified Guard

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2, (0 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2, (1-arg3 == 0 /\ -2+arg1 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, (9-arg3p6 == 0 /\ -arg1p6 == 0 /\ 10-arg3 == 0 /\ -2+arg1 < 0 /\ -arg2p6 == 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=9, (0 == 0 /\ 10-arg3 == 0 /\ -2+arg1 < 0), cost: 1
	
		propagated equality arg3p6 = 9
		
		propagated equality arg1p6 = 0
		
		propagated equality arg2p6 = 0
		
	Simplified Guard

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=9, (0 == 0 /\ 10-arg3 == 0 /\ -2+arg1 < 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=9, (10-arg3 == 0 /\ -2+arg1 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, (1-arg1p7 == 0 /\ 1-arg3p7+arg2 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0 /\ 1-arg2p7 == 0 /\ -1+arg2 > 0), cost: 1
	New rule:
	f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg2, (0 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
	
		propagated equality arg1p7 = 1
		
		propagated equality arg3p7 = 1+arg2
		
		propagated equality arg2p7 = 1
		
	Simplified Guard

	Original rule:
	f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg2, (0 == 0 /\ 1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
	New rule:
	f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg2, (1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	__init -> f99_0_loop_aux_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (-arg2p1 == 0 /\ -arg3p1+10*arg2p8 == 0 /\ arg1p8 > 0 /\ 1+arg2p8 > 0 /\ -arg1p1 == 0), cost: 1
	New rule:
	__init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (0 == 0 /\ arg1p8 > 0 /\ 1+arg2p8 > 0), cost: 1
	
		propagated equality arg2p1 = 0
		
		propagated equality arg3p1 = 10*arg2p8
		
		propagated equality arg1p1 = 0
		
	Simplified Guard

	Original rule:
	__init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (0 == 0 /\ arg1p8 > 0 /\ 1+arg2p8 > 0), cost: 1
	New rule:
	__init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (arg1p8 > 0 /\ 1+arg2p8 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	__init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (arg1p8 > 0 /\ 1+arg2p8 > 0), cost: 1
	New rule:
	__init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (1+arg2p8 > 0), cost: 1

Step with 15

	Trace

	15[(1+arg2p8 > 0)]
	
	Blocked

	[{}, {}]

Step with 10

	Trace

	15[(1+arg2p8 > 0)], 10[(-10+arg3 > 0)]
	
	Blocked

	[{}, {9[T]}, {}]

Step with 11

	Trace

	15[(1+arg2p8 > 0)], 10[(-10+arg3 > 0)], 11[(-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {9[T]}, {}, {}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   9: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, (-10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
  10: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, -10+arg3 > 0, cost: 1
  12: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2, (1-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  13: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=9, (10-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  16: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n, (-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1
  11: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg2, (-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  14: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg2, (1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  15: __init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (1+arg2p8 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg3, (-10+arg3 > 0 /\ -1+arg3 > 0 /\ -2+arg1 < 0 /\ -arg2 == 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n, (-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1

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

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)]
	
	Blocked

	[{}, {9[T]}, {16[T]}]

Step with 10

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 10[(-10+arg3 > 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 16[T]}, {}]

Step with 11

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 10[(-10+arg3 > 0)], 11[(-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 16[T]}, {}, {}]

Covered

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 10[(-10+arg3 > 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 16[T]}, {11[T]}]

Backtrack

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 16[T]}]

Step with 13

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 9

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {13[T], 16[T]}, {}]

Step with 11

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)], 11[(-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {13[T], 16[T]}, {}, {}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   9: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, (-10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
  10: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, -10+arg3 > 0, cost: 1
  12: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2, (1-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  13: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=9, (10-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  16: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n, (-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1
  17: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n2, (2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1
  11: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg2, (-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  14: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg2, (1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  15: __init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (1+arg2p8 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg3, (-10+arg3 < 0 /\ -1+arg3 > 0 /\ -2+arg1 < 0 /\ -arg2 == 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n2, (2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1

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

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {13[T], 16[T]}, {17[T]}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 9

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {13[T], 16[T]}, {17[T]}, {}]

Step with 11

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)], 11[(-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {13[T], 16[T]}, {17[T]}, {}, {}]

Covered

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {13[T], 16[T]}, {17[T]}, {11[T]}]

Backtrack

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {13[T], 16[T]}, {9[T], 17[T]}]

Step with 12

	Trace

	15[(1+arg2p8 > 0)], 16[(-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 12[(1-arg3 == 0 /\ -2+arg1 < 0)]
	
	Blocked

	[{}, {9[T]}, {9[T], 10[T], 12[T], 16[T]}, {13[T], 16[T]}, {9[T], 10[T], 17[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Restart

Step with 15

	Trace

	15[(1+arg2p8 > 0)]
	
	Blocked

	[{}, {}]

Step with 13

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)]
	
	Blocked

	[{}, {12[T]}, {}]

Step with 9

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)]
	
	Blocked

	[{}, {12[T]}, {10[T], 13[T]}, {}]

Step with 11

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)], 11[(-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {12[T]}, {10[T], 13[T]}, {}, {}]

Covered

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)]
	
	Blocked

	[{}, {12[T]}, {10[T], 13[T]}, {11[T]}]

Backtrack

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)]
	
	Blocked

	[{}, {12[T]}, {9[T], 10[T], 13[T]}]

Step with 17

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)]
	
	Blocked

	[{}, {12[T]}, {9[T], 10[T], 13[T]}, {17[T]}]

Step with 12

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 12[(1-arg3 == 0 /\ -2+arg1 < 0)]
	
	Blocked

	[{}, {12[T]}, {9[T], 10[T], 13[T]}, {16[T], 17[T]}, {}]

Step with 9

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 12[(1-arg3 == 0 /\ -2+arg1 < 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)]
	
	Blocked

	[{}, {12[T]}, {9[T], 10[T], 13[T]}, {16[T], 17[T]}, {10[T], 12[T], 13[T]}, {}]

Step with 14

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 12[(1-arg3 == 0 /\ -2+arg1 < 0)], 9[(-10+arg3 < 0 /\ -1+arg3 > 0)], 14[(1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0)]
	
	Blocked

	[{}, {12[T]}, {9[T], 10[T], 13[T]}, {16[T], 17[T]}, {10[T], 12[T], 13[T]}, {11[T]}, {}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   9: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, (-10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
  10: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, -10+arg3 > 0, cost: 1
  12: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2, (1-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  13: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=9, (10-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  16: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n, (-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1
  17: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n2, (2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1
  18: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=arg3+n3, (2-arg1 > 0 /\ -1+arg3 > 0 /\ 11-arg3-n3 > 0 /\ -1+n3 >= 0 /\ 1-arg2 >= 0 /\ -1+arg2 >= 0), cost: 1
  11: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg2, (-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  14: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg2, (1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  15: __init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (1+arg2p8 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg3, (-10+arg3 < 0 /\ -1+arg3 > 0 /\ -2+arg1 < 0 /\ 1-arg2 == 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=arg3+n3, (2-arg1 > 0 /\ -1+arg3 > 0 /\ 11-arg3-n3 > 0 /\ -1+n3 >= 0 /\ 1-arg2 >= 0 /\ -1+arg2 >= 0), cost: 1

		2-arg1 > 0 [0]: monotonic increase yields 2-arg1 > 0
		
		-1+arg3 > 0 [0]: monotonic increase yields -1+arg3 > 0
		
		10-arg3 > 0 [0]: montonic decrease yields 11-arg3-n3 > 0
		
		10-arg3 > 0 [1]: eventual increase yields (1 <= 0 /\ 10-arg3 > 0)
		
		1-arg2 >= 0 [0]: monotonic increase yields 1-arg2 >= 0
		
		-1+arg2 >= 0 [0]: monotonic increase yields -1+arg2 >= 0
		
		Replacement map: {2-arg1 > 0 -> 2-arg1 > 0, -1+arg3 > 0 -> -1+arg3 > 0, 10-arg3 > 0 -> 11-arg3-n3 > 0, 1-arg2 >= 0 -> 1-arg2 >= 0, -1+arg2 >= 0 -> -1+arg2 >= 0}

	Trace

	15[(1+arg2p8 > 0)], 13[(10-arg3 == 0 /\ -2+arg1 < 0)], 17[(2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0)], 12[(1-arg3 == 0 /\ -2+arg1 < 0)], 18[(2-arg1 > 0 /\ -1+arg3 > 0 /\ 11-arg3-n3 > 0 /\ -1+n3 >= 0 /\ 1-arg2 >= 0 /\ -1+arg2 >= 0)]
	
	Blocked

	[{}, {12[T]}, {9[T], 10[T], 13[T]}, {16[T], 17[T]}, {10[T], 12[T], 13[T]}, {18[T]}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Nonterm

Start location: __init
Program variables: arg1 arg2 arg3
   9: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, (-10+arg3 < 0 /\ -1+arg3 > 0), cost: 1
  10: f99_0_loop_aux_LE -> f128_0_loop_aux_EQ : arg2'=arg3, arg3'=arg2, -10+arg3 > 0, cost: 1
  12: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2, (1-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  13: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=9, (10-arg3 == 0 /\ -2+arg1 < 0), cost: 1
  16: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n, (-1+n >= 0 /\ 2-arg1 > 0 /\ -1+arg3 > 0 /\ -9+arg3-n > 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1
  17: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=arg3-n2, (2-arg1 > 0 /\ arg3-n2 > 0 /\ 10-arg3 > 0 /\ -1+n2 >= 0 /\ arg2 >= 0 /\ -arg2 >= 0), cost: 1
  18: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=arg3+n3, (2-arg1 > 0 /\ -1+arg3 > 0 /\ 11-arg3-n3 > 0 /\ -1+n3 >= 0 /\ 1-arg2 >= 0 /\ -1+arg2 >= 0), cost: 1
  19: f99_0_loop_aux_LE -> LoAT_sink : (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ -2+arg3-n3 <= 0 /\ 10-arg3 >= 0 /\ 9-n3 > 0 /\ -1+n3 >= 0), cost: NONTERM
  20: f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=10, (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 10-arg3 == 0), cost: 1
  11: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=-1+arg2, (-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  14: f128_0_loop_aux_EQ -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=1+arg2, (1-arg3 == 0 /\ -2+arg1 < 0 /\ -1+arg2 > 0), cost: 1
  15: __init -> f99_0_loop_aux_LE : arg1'=0, arg2'=0, arg3'=10*arg2p8, (1+arg2p8 > 0), cost: 1

	Certificate of Non-Termination

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2+n3, (10-arg3 == 0 /\ -2+arg1 < 0 /\ 9-n3 > 0 /\ -1+n3 >= 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> LoAT_sink : (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ -2+arg3-n3 <= 0 /\ 10-arg3 >= 0 /\ 9-n3 > 0 /\ -1+n3 >= 0), cost: NONTERM

		-10+arg3 >= 0 [0]: eventual decrease yields (-10+arg3 >= 0 /\ -8+n3 >= 0)
		
		-10+arg3 >= 0 [1]: eventual increase yields (-10+arg3 >= 0 /\ -2+arg3-n3 <= 0)
		
		2-arg1 > 0 [0]: monotonic increase yields 2-arg1 > 0
		
		10-arg3 >= 0 [0]: monotonic increase yields 10-arg3 >= 0, dependencies: 9-n3 > 0
		
		10-arg3 >= 0 [1]: eventual decrease yields (10-arg3 >= 0 /\ 8-n3 >= 0)
		
		10-arg3 >= 0 [2]: eventual increase yields (2-arg3+n3 <= 0 /\ 10-arg3 >= 0)
		
		9-n3 > 0 [0]: monotonic increase yields 9-n3 > 0
		
		-1+n3 >= 0 [0]: monotonic increase yields -1+n3 >= 0
		
		Replacement map: {-10+arg3 >= 0 -> (-10+arg3 >= 0 /\ -2+arg3-n3 <= 0), 2-arg1 > 0 -> 2-arg1 > 0, 10-arg3 >= 0 -> 10-arg3 >= 0, 9-n3 > 0 -> 9-n3 > 0, -1+n3 >= 0 -> -1+n3 >= 0}

	Loop Acceleration

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2+n3, (10-arg3 == 0 /\ -2+arg1 < 0 /\ 9-n3 > 0 /\ -1+n3 >= 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2+n3, (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 9-n3 > 0 /\ -8+n3 >= 0 /\ -1+n4 >= 0 /\ -1+n3 >= 0), cost: 1

		-10+arg3 >= 0 [0]: eventual decrease yields (-10+arg3 >= 0 /\ -8+n3 >= 0)
		
		-10+arg3 >= 0 [1]: eventual increase yields (-10+arg3 >= 0 /\ -2+arg3-n3 <= 0)
		
		2-arg1 > 0 [0]: monotonic increase yields 2-arg1 > 0
		
		10-arg3 >= 0 [0]: monotonic increase yields 10-arg3 >= 0, dependencies: 9-n3 > 0
		
		10-arg3 >= 0 [1]: eventual decrease yields (10-arg3 >= 0 /\ 8-n3 >= 0)
		
		10-arg3 >= 0 [2]: eventual increase yields (2-arg3+n3 <= 0 /\ 10-arg3 >= 0)
		
		9-n3 > 0 [0]: monotonic increase yields 9-n3 > 0
		
		-1+n3 >= 0 [0]: monotonic increase yields -1+n3 >= 0
		
		Replacement map: {-10+arg3 >= 0 -> (-10+arg3 >= 0 /\ -8+n3 >= 0), 2-arg1 > 0 -> 2-arg1 > 0, 10-arg3 >= 0 -> 10-arg3 >= 0, 9-n3 > 0 -> 9-n3 > 0, -1+n3 >= 0 -> -1+n3 >= 0}

	made implied equalities explicit

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2+n3, (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 9-n3 > 0 /\ -8+n3 >= 0 /\ -1+n4 >= 0 /\ -1+n3 >= 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2+n3, (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 10-arg3 == 0 /\ 9-n3 > 0 /\ -8+n3 >= 0 /\ -8+n3 == 0 /\ -1+n4 >= 0 /\ -1+n3 >= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=2+n3, (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 10-arg3 == 0 /\ 9-n3 > 0 /\ -8+n3 >= 0 /\ -8+n3 == 0 /\ -1+n4 >= 0 /\ -1+n3 >= 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=10, (0 >= 0 /\ 0 == 0 /\ -10+arg3 >= 0 /\ 1 > 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 10-arg3 == 0 /\ 7 >= 0 /\ -1+n4 >= 0), cost: 1
	
		propagated equality n3 = 8
		
	Simplified Guard

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=10, (0 >= 0 /\ 0 == 0 /\ -10+arg3 >= 0 /\ 1 > 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 10-arg3 == 0 /\ 7 >= 0 /\ -1+n4 >= 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=10, (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 10-arg3 == 0 /\ -1+n4 >= 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=10, (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 10-arg3 == 0 /\ -1+n4 >= 0), cost: 1
	New rule:
	f99_0_loop_aux_LE -> f99_0_loop_aux_LE : arg1'=1, arg2'=1, arg3'=10, (-10+arg3 >= 0 /\ 2-arg1 > 0 /\ 10-arg3 >= 0 /\ 10-arg3 == 0), cost: 1

Step with 19

	Trace

	15[(1+arg2p8 > 0)], 19[(-10+arg3 >= 0 /\ 2-arg1 > 0 /\ -2+arg3-n3 <= 0 /\ 10-arg3 >= 0 /\ 9-n3 > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {12[T]}, {19[T]}]

Refute

	Counterexample

	[ arg1=0 arg2=0 arg3=10 ] 15 [ arg1=arg1 arg2=arg2 arg3=arg3 ] 19
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b