unknown

Initial ITS

Start location: __init
Program variables: arg1 arg2 arg3
   0: f1_0_main_Load -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg2 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p1 > 0 /\ arg1 > 0 /\ 2-arg3p1 == 0), cost: 1
   1: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (1+arg3-arg3p2 == 0 /\ -arg2p2+arg2 == 0 /\ -1-arg1p2+arg1 == 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -41+x7 > 0 /\ arg2 > 0), cost: 1
   2: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (2-arg3p3+arg3 == 0 /\ 1+arg1p3 > 0 /\ -42+x12 < 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1-arg2p3+arg2 == 0 /\ 1+x12 > 0 /\ arg2 > 0), cost: 1
   3: __init -> f1_0_main_Load : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, T, cost: 1

Chained Linear Paths

Start location: __init
Program variables: arg1 arg2 arg3
   1: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (1+arg3-arg3p2 == 0 /\ -arg2p2+arg2 == 0 /\ -1-arg1p2+arg1 == 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -41+x7 > 0 /\ arg2 > 0), cost: 1
   2: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (2-arg3p3+arg3 == 0 /\ 1+arg1p3 > 0 /\ -42+x12 < 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1-arg2p3+arg2 == 0 /\ 1+x12 > 0 /\ arg2 > 0), cost: 1
   4: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (arg1p4 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p4 > 0 /\ 1+arg2p1 > 0 /\ 2-arg3p1 == 0), cost: 1

	Eliminating location f1_0_main_Load by chaining:

	Applied chaining

	First rule:
	__init -> f1_0_main_Load : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, T, cost: 1
	Second rule:
	f1_0_main_Load -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg2 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p1 > 0 /\ arg1 > 0 /\ 2-arg3p1 == 0), cost: 1
	New rule:
	__init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (arg1p4 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p4 > 0 /\ 1+arg2p1 > 0 /\ 2-arg3p1 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 3

Simplified Transitions

Start location: __init
Program variables: arg1 arg2 arg3
   5: f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   6: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   7: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

	Propagated Equalities

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (1+arg3-arg3p2 == 0 /\ -arg2p2+arg2 == 0 /\ -1-arg1p2+arg1 == 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -41+x7 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, (0 == 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -41+x7 > 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg3p2 = 1+arg3
		
		propagated equality arg2p2 = arg2
		
		propagated equality arg1p2 = -1+arg1
		
	Simplified Guard

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, (0 == 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -41+x7 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ -41+x7 > 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ -41+x7 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
	
	Removed Trivial Updates

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

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (2-arg3p3+arg3 == 0 /\ 1+arg1p3 > 0 /\ -42+x12 < 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1-arg2p3+arg2 == 0 /\ 1+x12 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (0 == 0 /\ 1+arg1p3 > 0 /\ -42+x12 < 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+x12 > 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg3p3 = 2+arg3
		
		propagated equality arg2p3 = -1+arg2
		
	Simplified Guard

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (0 == 0 /\ 1+arg1p3 > 0 /\ -42+x12 < 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+x12 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ -42+x12 < 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+x12 > 0 /\ arg2 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ -42+x12 < 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+x12 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -41 <= 0 /\ arg2 > 0), cost: 1
	
	Simplified Guard

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

	Original rule:
	__init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (arg1p4 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p4 > 0 /\ 1+arg2p1 > 0 /\ 2-arg3p1 == 0), cost: 1
	New rule:
	__init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (0 == 0 /\ arg1p4 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p4 > 0 /\ 1+arg2p1 > 0), cost: 1
	
		propagated equality arg3p1 = 2
		
	Simplified Guard

	Original rule:
	__init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (0 == 0 /\ arg1p4 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p4 > 0 /\ 1+arg2p1 > 0), cost: 1
	New rule:
	__init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (arg1p4 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p4 > 0 /\ 1+arg2p1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	__init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (arg1p4 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p4 > 0 /\ 1+arg2p1 > 0), cost: 1
	New rule:
	__init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

Step with 7

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

	[{}, {}]

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   5: f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   6: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   8: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1, arg3'=arg3+n, (1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   7: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1, arg3'=arg3+n, (1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1

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

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   5: f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   6: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   8: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1, arg3'=arg3+n, (1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   9: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n2+arg2, arg3'=arg3+2*n2, (1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0), cost: 1
   7: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n2+arg2, arg3'=arg3+2*n2, (1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0), cost: 1

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

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {}, {5[T], 8[T]}, {6[T], 9[T]}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   5: f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   6: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   8: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1, arg3'=arg3+n, (1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   9: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n2+arg2, arg3'=arg3+2*n2, (1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0), cost: 1
  10: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n3*n2+arg2, arg3'=n3*n1+arg3+2*n3*n2, (1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0), cost: 1
   7: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n2+arg2, arg3'=arg3+n1+2*n2, (1+arg1p3 > 0 /\ 1+arg1-n1 > 0 /\ -1+n1 >= 0 /\ 1-n2+arg2 > 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n3*n2+arg2, arg3'=n3*n1+arg3+2*n3*n2, (1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0), cost: 1

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

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {}, {10[T]}]

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {10[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {}, {5[T], 10[T]}]

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {5[T], 10[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 10[T]}]

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 10[T]}, {8[T]}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   5: f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   6: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   8: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1, arg3'=arg3+n, (1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   9: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n2+arg2, arg3'=arg3+2*n2, (1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0), cost: 1
  10: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n3*n2+arg2, arg3'=n3*n1+arg3+2*n3*n2, (1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0), cost: 1
  11: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p33, arg2'=-n22*n5*n31+arg2, arg3'=n5*n31*n11+arg3+n*n5+2*n22*n5*n31, (1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0), cost: 1
   7: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p33, arg2'=-n22*n31+arg2, arg3'=n31*n11+arg3+n+2*n22*n31, (1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ 1-n22-(-1+n31)*n22+arg2 > 0 /\ -1+n31 >= 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -n22*n31+arg2 > 0 /\ -(-1+n31)*n22+arg2 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p33, arg2'=-n22*n5*n31+arg2, arg3'=n5*n31*n11+arg3+n*n5+2*n22*n5*n31, (1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0), cost: 1

		1+n31*n11+arg3+2*n22*n31 > 0 [0]: monotonic increase yields 1+n31*n11+arg3+2*n22*n31 > 0, dependencies: -1+n31 >= 0 -1+n >= 0 -1+n22 >= 0 1+arg3 > 0 -1+n11 >= 0
		
		1+n31*n11+arg3+2*n22*n31 > 0 [1]: montonic decrease yields 1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0, dependencies: -1+n31 >= 0 -1+n22 >= 0 1+arg3 > 0 -1+n11 >= 0
		
		1+n31*n11+arg3+2*n22*n31 > 0 [2]: eventual decrease yields (1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0)
		
		1+n31*n11+arg3+2*n22*n31 > 0 [3]: eventual increase yields (1+n31*n11+arg3+2*n22*n31 > 0 /\ -n31*n11-n-2*n22*n31 <= 0)
		
		arg1p33-n11 > 0 [0]: monotonic increase yields arg1p33-n11 > 0
		
		1+arg1p33-n11 > 0 [0]: monotonic increase yields 1+arg1p33-n11 > 0
		
		1-n22-(-1+n31)*n22+arg2 > 0 [0]: montonic decrease yields 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0, dependencies: -n22*n31+arg2 > 0
		
		1-n22-(-1+n31)*n22+arg2 > 0 [1]: eventual decrease yields (1-n22-(-1+n31)*n22+arg2 > 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0)
		
		1-n22-(-1+n31)*n22+arg2 > 0 [2]: eventual increase yields (1-n22-(-1+n31)*n22+arg2 > 0 /\ n22*n31 <= 0)
		
		-1+n31 >= 0 [0]: monotonic increase yields -1+n31 >= 0
		
		1-n+arg1p33 > 0 [0]: monotonic increase yields 1-n+arg1p33 > 0
		
		-1+n >= 0 [0]: monotonic increase yields -1+n >= 0
		
		1+arg1p33 > 0 [0]: monotonic increase yields 1+arg1p33 > 0
		
		1+arg3+n11 > 0 [0]: monotonic increase yields 1+arg3+n11 > 0, dependencies: 1+n31*n11+arg3+2*n22*n31 > 0 -1+n >= 0 -1+n11 >= 0
		
		1+arg3+n11 > 0 [1]: montonic decrease yields 1+arg3+n*(-1+n5)+n31*n11*(-1+n5)+2*n22*n31*(-1+n5)+n11 > 0, dependencies: 1+arg3 > 0 -1+n11 >= 0
		
		1+arg3+n11 > 0 [2]: eventual decrease yields (1+arg3+n*(-1+n5)+n31*n11*(-1+n5)+2*n22*n31*(-1+n5)+n11 > 0 /\ 1+arg3+n11 > 0)
		
		1+arg3+n11 > 0 [3]: eventual increase yields (-n31*n11-n-2*n22*n31 <= 0 /\ 1+arg3+n11 > 0)
		
		-1+n22 >= 0 [0]: monotonic increase yields -1+n22 >= 0
		
		1+arg3 > 0 [0]: monotonic increase yields 1+arg3 > 0, dependencies: 1+n31*n11+arg3+2*n22*n31 > 0 -1+n >= 0
		
		arg1p33 > 0 [0]: monotonic increase yields arg1p33 > 0
		
		-n22*n31+arg2 > 0 [0]: montonic decrease yields -n22*n31-n22*n31*(-1+n5)+arg2 > 0, dependencies: -1+n31 >= 0 -1+n22 >= 0
		
		-n22*n31+arg2 > 0 [1]: eventual increase yields (n22*n31 <= 0 /\ -n22*n31+arg2 > 0)
		
		-(-1+n31)*n22+arg2 > 0 [0]: montonic decrease yields -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0, dependencies: -1+n22 >= 0 -n22*n31+arg2 > 0
		
		-(-1+n31)*n22+arg2 > 0 [1]: eventual increase yields (n22*n31 <= 0 /\ -(-1+n31)*n22+arg2 > 0)
		
		arg1-n11 > 0 [0]: eventual decrease yields (-n+arg1p33-n11 > 0 /\ arg1-n11 > 0)
		
		arg1-n11 > 0 [1]: eventual increase yields (n+arg1-arg1p33 <= 0 /\ arg1-n11 > 0)
		
		-1+n11 >= 0 [0]: monotonic increase yields -1+n11 >= 0
		
		Replacement map: {1+n31*n11+arg3+2*n22*n31 > 0 -> (1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0), arg1p33-n11 > 0 -> arg1p33-n11 > 0, 1+arg1p33-n11 > 0 -> 1+arg1p33-n11 > 0, 1-n22-(-1+n31)*n22+arg2 > 0 -> 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0, -1+n31 >= 0 -> -1+n31 >= 0, 1-n+arg1p33 > 0 -> 1-n+arg1p33 > 0, -1+n >= 0 -> -1+n >= 0, 1+arg1p33 > 0 -> 1+arg1p33 > 0, 1+arg3+n11 > 0 -> 1+arg3+n11 > 0, -1+n22 >= 0 -> -1+n22 >= 0, 1+arg3 > 0 -> 1+arg3 > 0, arg1p33 > 0 -> arg1p33 > 0, -n22*n31+arg2 > 0 -> -n22*n31-n22*n31*(-1+n5)+arg2 > 0, -(-1+n31)*n22+arg2 > 0 -> -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0, arg1-n11 > 0 -> (-n+arg1p33-n11 > 0 /\ arg1-n11 > 0), -1+n11 >= 0 -> -1+n11 >= 0}

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {}, {11[T]}]

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {11[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {}, {5[T], 11[T]}]

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {5[T], 11[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 11[T]}]

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 11[T]}, {8[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 8[T], 11[T]}]

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 8[T], 11[T]}, {9[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 8[T], 9[T], 11[T]}]

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 8[T], 9[T], 11[T]}, {10[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T]}]

Backtrack

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

	[{}, {11[T]}]

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

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

Step with 11

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

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

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {11[T]}, {5[T], 10[T], 11[T]}]

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {11[T]}, {5[T], 10[T], 11[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {11[T]}, {5[T], 6[T], 10[T], 11[T]}]

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {11[T]}, {5[T], 6[T], 10[T], 11[T]}, {8[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {11[T]}, {5[T], 6[T], 8[T], 10[T], 11[T]}]

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {11[T]}, {5[T], 6[T], 8[T], 10[T], 11[T]}, {9[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {11[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T]}]

Backtrack

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

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

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

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

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

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

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   5: f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   6: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   8: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1, arg3'=arg3+n, (1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   9: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n2+arg2, arg3'=arg3+2*n2, (1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0), cost: 1
  10: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n3*n2+arg2, arg3'=n3*n1+arg3+2*n3*n2, (1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0), cost: 1
  11: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p33, arg2'=-n22*n5*n31+arg2, arg3'=n5*n31*n11+arg3+n*n5+2*n22*n5*n31, (1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0), cost: 1
  12: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n27*n10+arg2-n3*n10*n2, arg3'=arg3+2*n27*n10+n3*n10*n1+2*n3*n10*n2, (-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0), cost: 1
   7: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n27-n3*n2+arg2, arg3'=n3*n1+arg3+2*n27+2*n3*n2, (1+arg1p3 > 0 /\ 1-n27-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -n27-n2*(-1+n3)+arg2 > 0 /\ -1+n1 >= 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1-n27+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n27*n10+arg2-n3*n10*n2, arg3'=arg3+2*n27*n10+n3*n10*n1+2*n3*n10*n2, (-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0), cost: 1

		1+arg1p3 > 0 [0]: monotonic increase yields 1+arg1p3 > 0
		
		1-n27-n2-n2*(-1+n3)+arg2 > 0 [0]: montonic decrease yields 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0, dependencies: -1+n27 >= 0 1-n27+arg2 > 0
		
		1-n27-n2-n2*(-1+n3)+arg2 > 0 [1]: eventual decrease yields (1-n27-n2-n2*(-1+n3)+arg2 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0)
		
		1-n27-n2-n2*(-1+n3)+arg2 > 0 [2]: eventual increase yields (n27+n3*n2 <= 0 /\ 1-n27-n2-n2*(-1+n3)+arg2 > 0)
		
		1+arg3+2*n27+n1 > 0 [0]: monotonic increase yields 1+arg3+2*n27+n1 > 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 -1+n27 >= 0 1+arg3 > 0 -1+n3 >= 0
		
		1+arg3+2*n27+n1 > 0 [1]: montonic decrease yields 1+arg3+2*n27+2*n27*(-1+n10)+2*n3*n2*(-1+n10)+n1+n3*n1*(-1+n10) > 0, dependencies: -1+n1 >= 0 -1+n27 >= 0 1+arg3 > 0
		
		1+arg3+2*n27+n1 > 0 [2]: eventual decrease yields (1+arg3+2*n27+n1 > 0 /\ 1+arg3+2*n27+2*n27*(-1+n10)+2*n3*n2*(-1+n10)+n1+n3*n1*(-1+n10) > 0)
		
		1+arg3+2*n27+n1 > 0 [3]: eventual increase yields (1+arg3+2*n27+n1 > 0 /\ -n3*n1-2*n27-2*n3*n2 <= 0)
		
		-n27-n2*(-1+n3)+arg2 > 0 [0]: montonic decrease yields -n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0, dependencies: 1-n27-n2-n2*(-1+n3)+arg2 > 0 -1+n2 >= 0
		
		-n27-n2*(-1+n3)+arg2 > 0 [1]: eventual decrease yields (-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ -n27-n2*(-1+n3)+arg2 > 0)
		
		-n27-n2*(-1+n3)+arg2 > 0 [2]: eventual increase yields (n27+n3*n2 <= 0 /\ -n27-n2*(-1+n3)+arg2 > 0)
		
		-1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0
		
		arg1p3 > 0 [0]: monotonic increase yields arg1p3 > 0
		
		-1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0
		
		-1+n27 >= 0 [0]: monotonic increase yields -1+n27 >= 0
		
		arg1 > 0 [0]: monotonic increase yields arg1 > 0, dependencies: -1+n1 >= 0 arg1p3-n1 > 0
		
		arg1 > 0 [1]: eventual decrease yields (arg1p3 > 0 /\ arg1 > 0)
		
		arg1 > 0 [2]: eventual increase yields (arg1 > 0 /\ -arg1p3+arg1 <= 0)
		
		1+arg3+2*n27 > 0 [0]: monotonic increase yields 1+arg3+2*n27 > 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 -1+n27 >= 0 1+arg3 > 0 -1+n3 >= 0
		
		1+arg3+2*n27 > 0 [1]: montonic decrease yields 1+arg3+2*n27+2*n27*(-1+n10)+2*n3*n2*(-1+n10)+n3*n1*(-1+n10) > 0, dependencies: -1+n27 >= 0 1+arg3 > 0
		
		1+arg3+2*n27 > 0 [2]: eventual decrease yields (1+arg3+2*n27+2*n27*(-1+n10)+2*n3*n2*(-1+n10)+n3*n1*(-1+n10) > 0 /\ 1+arg3+2*n27 > 0)
		
		1+arg3+2*n27 > 0 [3]: eventual increase yields (-n3*n1-2*n27-2*n3*n2 <= 0 /\ 1+arg3+2*n27 > 0)
		
		1+arg3 > 0 [0]: monotonic increase yields 1+arg3 > 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 -1+n27 >= 0 -1+n3 >= 0
		
		1+arg3 > 0 [1]: eventual decrease yields (1+arg3 > 0 /\ 1+arg3+2*n27*(-1+n10)+2*n3*n2*(-1+n10)+n3*n1*(-1+n10) > 0)
		
		1+arg3 > 0 [2]: eventual increase yields (-n3*n1-2*n27-2*n3*n2 <= 0 /\ 1+arg3 > 0)
		
		-1+n3 >= 0 [0]: monotonic increase yields -1+n3 >= 0
		
		1-n27+arg2 > 0 [0]: montonic decrease yields 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0, dependencies: -1+n2 >= 0 -1+n27 >= 0 -1+n3 >= 0
		
		1-n27+arg2 > 0 [1]: eventual increase yields (n27+n3*n2 <= 0 /\ 1-n27+arg2 > 0)
		
		1+arg1p3-n1 > 0 [0]: monotonic increase yields 1+arg1p3-n1 > 0
		
		arg1p3-n1 > 0 [0]: monotonic increase yields arg1p3-n1 > 0
		
		Replacement map: {1+arg1p3 > 0 -> 1+arg1p3 > 0, 1-n27-n2-n2*(-1+n3)+arg2 > 0 -> 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0, 1+arg3+2*n27+n1 > 0 -> 1+arg3+2*n27+n1 > 0, -n27-n2*(-1+n3)+arg2 > 0 -> -n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0, -1+n1 >= 0 -> -1+n1 >= 0, arg1p3 > 0 -> arg1p3 > 0, -1+n2 >= 0 -> -1+n2 >= 0, -1+n27 >= 0 -> -1+n27 >= 0, arg1 > 0 -> arg1 > 0, 1+arg3+2*n27 > 0 -> 1+arg3+2*n27 > 0, 1+arg3 > 0 -> 1+arg3 > 0, -1+n3 >= 0 -> -1+n3 >= 0, 1-n27+arg2 > 0 -> 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0, 1+arg1p3-n1 > 0 -> 1+arg1p3-n1 > 0, arg1p3-n1 > 0 -> arg1p3-n1 > 0}

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

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

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

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

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 12[T]}]

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 12[T]}, {8[T]}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   5: f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   6: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   8: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1, arg3'=arg3+n, (1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   9: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n2+arg2, arg3'=arg3+2*n2, (1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0), cost: 1
  10: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n3*n2+arg2, arg3'=n3*n1+arg3+2*n3*n2, (1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0), cost: 1
  11: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p33, arg2'=-n22*n5*n31+arg2, arg3'=n5*n31*n11+arg3+n*n5+2*n22*n5*n31, (1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0), cost: 1
  12: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n27*n10+arg2-n3*n10*n2, arg3'=arg3+2*n27*n10+n3*n10*n1+2*n3*n10*n2, (-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0), cost: 1
  13: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p313, arg2'=-n17*n101*n271-n17*n35*n101*n29+arg2, arg3'=arg3+2*n17*n101*n271+n17*n+2*n17*n35*n101*n29+n15*n17*n35*n101, (-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0), cost: 1
   7: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p313, arg2'=-n101*n271-n35*n101*n29+arg2, arg3'=2*n101*n271+arg3+n+2*n35*n101*n29+n15*n35*n101, (1-n35*n29*(-1+n101)-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n15 >= 0 /\ 1+n15+arg3+2*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ 1-n35*n29*(-1+n101)-n29-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n >= 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -n35*n29*(-1+n101)-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -n101*n271-n35*n101*n29+arg2 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p313, arg2'=-n17*n101*n271-n17*n35*n101*n29+arg2, arg3'=arg3+2*n17*n101*n271+n17*n+2*n17*n35*n101*n29+n15*n17*n35*n101, (-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0), cost: 1

		1-n35*n29*(-1+n101)-n271+arg2-(-1+n101)*n271 > 0 [0]: montonic decrease yields 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0, dependencies: -1+n29 >= 0 -1+n35 >= 0 -n101*n271-n35*n101*n29+arg2 > 0
		
		1-n35*n29*(-1+n101)-n271+arg2-(-1+n101)*n271 > 0 [1]: eventual decrease yields (1-n35*n29*(-1+n101)-n271+arg2-(-1+n101)*n271 > 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0)
		
		1-n35*n29*(-1+n101)-n271+arg2-(-1+n101)*n271 > 0 [2]: eventual increase yields (1-n35*n29*(-1+n101)-n271+arg2-(-1+n101)*n271 > 0 /\ n101*n271+n35*n101*n29 <= 0)
		
		-1+n15 >= 0 [0]: monotonic increase yields -1+n15 >= 0
		
		1+n15+arg3+2*n271 > 0 [0]: monotonic increase yields 1+n15+arg3+2*n271 > 0, dependencies: -1+n15 >= 0 -1+n >= 0 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 -1+n271 >= 0
		
		1+n15+arg3+2*n271 > 0 [1]: montonic decrease yields 1+n15+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271+2*n271 > 0, dependencies: -1+n15 >= 0 1+arg3 > 0 -1+n271 >= 0
		
		1+n15+arg3+2*n271 > 0 [2]: eventual decrease yields (1+n15+arg3+2*n271 > 0 /\ 1+n15+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271+2*n271 > 0)
		
		1+n15+arg3+2*n271 > 0 [3]: eventual increase yields (1+n15+arg3+2*n271 > 0 /\ -2*n101*n271-n-2*n35*n101*n29-n15*n35*n101 <= 0)
		
		1-n15+arg1p313 > 0 [0]: monotonic increase yields 1-n15+arg1p313 > 0
		
		-1+n29 >= 0 [0]: monotonic increase yields -1+n29 >= 0
		
		1-n+arg1p313 > 0 [0]: monotonic increase yields 1-n+arg1p313 > 0
		
		-n15+arg1p313 > 0 [0]: monotonic increase yields -n15+arg1p313 > 0
		
		1-n35*n29*(-1+n101)-n29-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 [0]: montonic decrease yields 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0, dependencies: -n101*n271-n35*n101*n29+arg2 > 0
		
		1-n35*n29*(-1+n101)-n29-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 [1]: eventual decrease yields (1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n35*n29*(-1+n101)-n29-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0)
		
		1-n35*n29*(-1+n101)-n29-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 [2]: eventual increase yields (n101*n271+n35*n101*n29 <= 0 /\ 1-n35*n29*(-1+n101)-n29-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0)
		
		-1+n >= 0 [0]: monotonic increase yields -1+n >= 0
		
		-1+n35 >= 0 [0]: monotonic increase yields -1+n35 >= 0
		
		arg1 > 0 [0]: eventual decrease yields (-n+arg1p313 > 0 /\ arg1 > 0)
		
		arg1 > 0 [1]: eventual increase yields (arg1 > 0 /\ n+arg1-arg1p313 <= 0)
		
		1+arg3 > 0 [0]: monotonic increase yields 1+arg3 > 0, dependencies: -1+n >= 0 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0
		
		1+arg3 > 0 [1]: eventual decrease yields (1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+arg3 > 0)
		
		1+arg3 > 0 [2]: eventual increase yields (-2*n101*n271-n-2*n35*n101*n29-n15*n35*n101 <= 0 /\ 1+arg3 > 0)
		
		-n35*n29*(-1+n101)-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 [0]: montonic decrease yields -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0, dependencies: -1+n29 >= 0 -n101*n271-n35*n101*n29+arg2 > 0
		
		-n35*n29*(-1+n101)-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 [1]: eventual decrease yields (-n35*n29*(-1+n101)-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0)
		
		-n35*n29*(-1+n101)-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 [2]: eventual increase yields (n101*n271+n35*n101*n29 <= 0 /\ -n35*n29*(-1+n101)-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0)
		
		1+arg1p313 > 0 [0]: monotonic increase yields 1+arg1p313 > 0
		
		-1+n101 >= 0 [0]: monotonic increase yields -1+n101 >= 0
		
		arg1p313 > 0 [0]: monotonic increase yields arg1p313 > 0
		
		1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 [0]: monotonic increase yields 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0, dependencies: -1+n15 >= 0 -1+n29 >= 0 -1+n >= 0 -1+n35 >= 0 1+arg3 > 0 -1+n101 >= 0 -1+n271 >= 0
		
		1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 [1]: montonic decrease yields 1+2*(-1+n17)*n35*n101*n29+2*n101*n271+n15*(-1+n17)*n35*n101+arg3+2*n35*n101*n29+(-1+n17)*n+2*(-1+n17)*n101*n271+n15*n35*n101 > 0, dependencies: -1+n15 >= 0 -1+n29 >= 0 -1+n35 >= 0 1+arg3 > 0 -1+n101 >= 0 -1+n271 >= 0
		
		1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 [2]: eventual decrease yields (1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ 1+2*(-1+n17)*n35*n101*n29+2*n101*n271+n15*(-1+n17)*n35*n101+arg3+2*n35*n101*n29+(-1+n17)*n+2*(-1+n17)*n101*n271+n15*n35*n101 > 0)
		
		1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 [3]: eventual increase yields (-2*n101*n271-n-2*n35*n101*n29-n15*n35*n101 <= 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0)
		
		-n101*n271-n35*n101*n29+arg2 > 0 [0]: montonic decrease yields -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0, dependencies: -1+n29 >= 0 -1+n35 >= 0 -1+n101 >= 0 -1+n271 >= 0
		
		-n101*n271-n35*n101*n29+arg2 > 0 [1]: eventual decrease yields (-(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -n101*n271-n35*n101*n29+arg2 > 0)
		
		-n101*n271-n35*n101*n29+arg2 > 0 [2]: eventual increase yields (n101*n271+n35*n101*n29 <= 0 /\ -n101*n271-n35*n101*n29+arg2 > 0)
		
		-1+n271 >= 0 [0]: monotonic increase yields -1+n271 >= 0
		
		1+arg3+2*n271 > 0 [0]: monotonic increase yields 1+arg3+2*n271 > 0, dependencies: -1+n >= 0 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 -1+n271 >= 0
		
		Replacement map: {1-n35*n29*(-1+n101)-n271+arg2-(-1+n101)*n271 > 0 -> 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0, -1+n15 >= 0 -> -1+n15 >= 0, 1+n15+arg3+2*n271 > 0 -> 1+n15+arg3+2*n271 > 0, 1-n15+arg1p313 > 0 -> 1-n15+arg1p313 > 0, -1+n29 >= 0 -> -1+n29 >= 0, 1-n+arg1p313 > 0 -> 1-n+arg1p313 > 0, -n15+arg1p313 > 0 -> -n15+arg1p313 > 0, 1-n35*n29*(-1+n101)-n29-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 -> 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0, -1+n >= 0 -> -1+n >= 0, -1+n35 >= 0 -> -1+n35 >= 0, arg1 > 0 -> (-n+arg1p313 > 0 /\ arg1 > 0), 1+arg3 > 0 -> (1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+arg3 > 0), -n35*n29*(-1+n101)-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 -> -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0, 1+arg1p313 > 0 -> 1+arg1p313 > 0, -1+n101 >= 0 -> -1+n101 >= 0, arg1p313 > 0 -> arg1p313 > 0, 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 -> 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0, -n101*n271-n35*n101*n29+arg2 > 0 -> -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0, -1+n271 >= 0 -> -1+n271 >= 0, 1+arg3+2*n271 > 0 -> 1+arg3+2*n271 > 0}

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

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

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

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

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 13[T]}]

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 13[T]}, {8[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 13[T]}]

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 13[T]}, {9[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 9[T], 13[T]}]

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 9[T], 13[T]}, {10[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 13[T]}]

Step with 11

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 13[T]}, {11[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 13[T]}]

Step with 12

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 13[T]}, {12[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {10[T], 11[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 12[T], 13[T]}]

Backtrack

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

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

Step with 12

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

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

Step with 13

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

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

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

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

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

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

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {10[T], 11[T], 13[T]}, {5[T], 6[T], 12[T], 13[T]}, {8[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {10[T], 11[T], 13[T]}, {5[T], 6[T], 8[T], 12[T], 13[T]}]

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {10[T], 11[T], 13[T]}, {5[T], 6[T], 8[T], 12[T], 13[T]}, {9[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {10[T], 11[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 12[T], 13[T]}]

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {10[T], 11[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 12[T], 13[T]}, {10[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {10[T], 11[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 12[T], 13[T]}]

Step with 11

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {10[T], 11[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 12[T], 13[T]}, {11[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {10[T], 11[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 12[T], 13[T]}]

Backtrack

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

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

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

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

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

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

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

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

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T]}]

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T]}, {9[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T]}]

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T]}, {10[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T], 10[T]}]

Step with 11

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T], 10[T]}, {11[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T], 10[T], 11[T]}]

Step with 12

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T], 10[T], 11[T]}, {12[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T], 10[T], 11[T], 12[T]}]

Step with 13

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T], 10[T], 11[T], 12[T]}, {13[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T], 10[T], 11[T], 12[T], 13[T]}]

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {8[T], 9[T], 10[T], 11[T], 12[T], 13[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 8[T], 9[T], 10[T], 11[T], 12[T], 13[T]}]

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 8[T], 9[T], 10[T], 11[T], 12[T], 13[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 12[T], 13[T]}]

Backtrack

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}]

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T]}]

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T]}, {10[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T], 10[T]}]

Step with 11

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T], 10[T]}, {11[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T], 10[T], 11[T]}]

Step with 12

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T], 10[T], 11[T]}, {12[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T], 10[T], 11[T], 12[T]}]

Step with 13

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T], 10[T], 11[T], 12[T]}, {13[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T], 10[T], 11[T], 12[T], 13[T]}]

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {9[T], 10[T], 11[T], 12[T], 13[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 9[T], 10[T], 11[T], 12[T], 13[T]}]

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 9[T], 10[T], 11[T], 12[T], 13[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 9[T], 10[T], 11[T], 12[T], 13[T]}]

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 9[T], 10[T], 11[T], 12[T], 13[T]}, {8[T]}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3
   5: f368_0_main_LE -> f368_0_main_LE : arg1'=-1+arg1, arg3'=1+arg3, (arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   6: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-1+arg2, arg3'=2+arg3, (1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   8: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1, arg3'=arg3+n, (1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0), cost: 1
   9: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n2+arg2, arg3'=arg3+2*n2, (1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0), cost: 1
  10: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n3*n2+arg2, arg3'=n3*n1+arg3+2*n3*n2, (1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0), cost: 1
  11: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p33, arg2'=-n22*n5*n31+arg2, arg3'=n5*n31*n11+arg3+n*n5+2*n22*n5*n31, (1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0), cost: 1
  12: f368_0_main_LE -> f368_0_main_LE : arg1'=arg1p3, arg2'=-n27*n10+arg2-n3*n10*n2, arg3'=arg3+2*n27*n10+n3*n10*n1+2*n3*n10*n2, (-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0), cost: 1
  13: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p313, arg2'=-n17*n101*n271-n17*n35*n101*n29+arg2, arg3'=arg3+2*n17*n101*n271+n17*n+2*n17*n35*n101*n29+n15*n17*n35*n101, (-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0), cost: 1
  14: f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p328, arg2'=-n47*n219+arg2, arg3'=arg3+2*n47*n219+n*n47, (1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0), cost: 1
   7: __init -> f368_0_main_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=2, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p328, arg2'=-n219+arg2, arg3'=arg3+n+2*n219, (1-n+arg1p328 > 0 /\ 1-n219+arg2 > 0 /\ -n219+arg2 > 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0), cost: 1
	New rule:
	f368_0_main_LE -> f368_0_main_LE : arg1'=-n+arg1p328, arg2'=-n47*n219+arg2, arg3'=arg3+2*n47*n219+n*n47, (1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0), cost: 1

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

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {14[T]}]

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {14[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 14[T]}]

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 14[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 14[T]}]

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 14[T]}, {8[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 14[T]}]

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 14[T]}, {9[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 14[T]}]

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 14[T]}, {10[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 14[T]}]

Step with 11

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 14[T]}, {11[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 14[T]}]

Step with 12

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 14[T]}, {12[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 12[T], 14[T]}]

Step with 13

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 12[T], 14[T]}, {13[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}]

Backtrack

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}]

Step with 9

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T]}]

Step with 10

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 10[(1+arg1p3 > 0 /\ -1+n1 >= 0 /\ arg1-n1 > 0 /\ 1+arg3+n1 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ -n2*(-1+n3)+arg2 > 0 /\ 1-n2-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T]}, {10[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T]}]

Step with 11

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 11[(1+n31*n11+arg3+n*(-1+n5)+2*n22*n31+n31*n11*(-1+n5)+2*n22*n31*(-1+n5) > 0 /\ 1+n31*n11+arg3+2*n22*n31 > 0 /\ arg1p33-n11 > 0 /\ 1+arg1p33-n11 > 0 /\ -1+n31 >= 0 /\ 1-n22-(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n22*n31-n22*n31*(-1+n5)+arg2 > 0 /\ 1-n+arg1p33 > 0 /\ -1+n >= 0 /\ 1+arg1p33 > 0 /\ 1+arg3+n11 > 0 /\ -1+n22 >= 0 /\ 1+arg3 > 0 /\ arg1p33 > 0 /\ -(-1+n31)*n22-n22*n31*(-1+n5)+arg2 > 0 /\ -n+arg1p33-n11 > 0 /\ arg1-n11 > 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T]}, {11[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T], 11[T]}]

Step with 12

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 12[(-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2*(-1+n3)+arg2 > 0 /\ 1+arg1p3 > 0 /\ 1+arg3+2*n27+n1 > 0 /\ -1+n1 >= 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)+arg2 > 0 /\ arg1p3 > 0 /\ 1-n27-n27*(-1+n10)-n3*n2*(-1+n10)-n2-n2*(-1+n3)+arg2 > 0 /\ -1+n2 >= 0 /\ -1+n27 >= 0 /\ arg1 > 0 /\ 1+arg3+2*n27 > 0 /\ 1+arg3 > 0 /\ -1+n3 >= 0 /\ 1+arg1p3-n1 > 0 /\ arg1p3-n1 > 0 /\ -1+n10 >= 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T], 11[T]}, {12[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T], 11[T], 12[T]}]

Step with 13

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 13[(-1+n15 >= 0 /\ 1+2*(-1+n17)*n35*n101*n29+n15*(-1+n17)*n35*n101+arg3+(-1+n17)*n+2*(-1+n17)*n101*n271 > 0 /\ 1+n15+arg3+2*n271 > 0 /\ -(-1+n17)*n35*n101*n29-n101*n271-n35*n101*n29-(-1+n17)*n101*n271+arg2 > 0 /\ -1+n17 >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-n29-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1-n15+arg1p313 > 0 /\ -1+n29 >= 0 /\ 1-n+arg1p313 > 0 /\ -n+arg1p313 > 0 /\ -n15+arg1p313 > 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-n271+arg2-(-1+n101)*n271 > 0 /\ -1+n35 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ 1+arg1p313 > 0 /\ -1+n101 >= 0 /\ arg1p313 > 0 /\ -(-1+n17)*n35*n101*n29-n35*n29*(-1+n101)-(-1+n17)*n101*n271-(-1+n35)*n29-n271+arg2-(-1+n101)*n271 > 0 /\ 1+2*n101*n271+arg3+2*n35*n101*n29+n15*n35*n101 > 0 /\ -1+n271 >= 0 /\ 1+arg3+2*n271 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T], 11[T], 12[T]}, {13[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T], 11[T], 12[T], 13[T]}]

Step with 14

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 14[(1-n+arg1p328 > 0 /\ -(-1+n47)*n219-n219+arg2 > 0 /\ -n+arg1p328 > 0 /\ 1-(-1+n47)*n219-n219+arg2 > 0 /\ -1+n47 >= 0 /\ -1+n >= 0 /\ arg1p328 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ -1+n219 >= 0 /\ 1+arg3+2*n219 > 0 /\ 1+arg1p328 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T], 11[T], 12[T], 13[T]}, {14[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}]

Step with 5

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 5[(arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {5[T], 9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}]

Step with 6

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 6[(1+arg1p3 > 0 /\ arg1 > 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {5[T], 9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {5[T], 6[T], 9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}]

Step with 8

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)], 8[(1-n+arg1 > 0 /\ -1+n >= 0 /\ 1+arg3 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {5[T], 6[T], 9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {8[T]}]

Covered

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 9[(1+arg1p3 > 0 /\ 1-n2+arg2 > 0 /\ arg1p3 > 0 /\ -1+n2 >= 0 /\ arg1 > 0 /\ 1+arg3 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 10[T], 11[T], 12[T], 13[T], 14[T]}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}]

Backtrack

	Trace

	7[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)]
	
	Blocked

	[{}, {5[T], 6[T], 8[T], 9[T], 10[T], 11[T], 12[T], 13[T], 14[T]}]

Backtrack

	Trace

	Blocked

	[{7[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b