unknown

Initial ITS

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   0: l0 -> l1 : ni6^0'=ni6^post1, nx4^0'=nx4^post1, nx9^0'=nx9^post1, nx^0'=nx^post1, res10^0'=res10^post1, res5^0'=res5^post1, ret_nbc18^0'=ret_nbc18^post1, ret_nbc211^0'=ret_nbc211^post1, tmp7^0'=tmp7^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (nx^0-nx^post1 == 0 /\ ret_nbc211^0-ret_nbc211^post1 == 0 /\ -ret_nbc18^post1+ret_nbc18^0 == 0 /\ -nx4^post1+nx4^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ res10^0-res10^post1 == 0 /\ -tmp7^0+res5^post1-res5^0 == 0 /\ nx9^0-nx9^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -tmp7^post1+tmp7^0 == 0 /\ -1+ni6^post1-ni6^0 == 0), cost: 1
   5: l1 -> l3 : ni6^0'=ni6^post6, nx4^0'=nx4^post6, nx9^0'=nx9^post6, nx^0'=nx^post6, res10^0'=res10^post6, res5^0'=res5^post6, ret_nbc18^0'=ret_nbc18^post6, ret_nbc211^0'=ret_nbc211^post6, tmp7^0'=tmp7^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-ret_nbc18^post6+ret_nbc18^0 == 0 /\ nx^0-nx^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -nx9^post6+nx9^0 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ -res5^post6+res5^0 == 0 /\ -ni6^post6+ni6^0 == 0 /\ res10^0-res10^post6 == 0 /\ ret_nbc211^0-ret_nbc211^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ nx4^0-nx4^post6 == 0), cost: 1
   1: l2 -> l0 : ni6^0'=ni6^post2, nx4^0'=nx4^post2, nx9^0'=nx9^post2, nx^0'=nx^post2, res10^0'=res10^post2, res5^0'=res5^post2, ret_nbc18^0'=ret_nbc18^post2, ret_nbc211^0'=ret_nbc211^post2, tmp7^0'=tmp7^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-nx^post2+nx^0 == 0 /\ -res5^post2+res5^0 == 0 /\ nx9^0-nx9^post2 == 0 /\ -ni6^post2+ni6^0 == 0 /\ -nx4^post2+nx4^0 == 0 /\ -ret_nbc18^post2+ret_nbc18^0 == 0 /\ tmp7^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -ret_nbc211^post2+ret_nbc211^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ res10^0-res10^post2 == 0), cost: 1
   2: l2 -> l0 : ni6^0'=ni6^post3, nx4^0'=nx4^post3, nx9^0'=nx9^post3, nx^0'=nx^post3, res10^0'=res10^post3, res5^0'=res5^post3, ret_nbc18^0'=ret_nbc18^post3, ret_nbc211^0'=ret_nbc211^post3, tmp7^0'=tmp7^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (-ni6^post3+ni6^0 == 0 /\ -res5^post3+res5^0 == 0 /\ -1+tmp7^post3 == 0 /\ ret_nbc211^0-ret_nbc211^post3 == 0 /\ nx^0-nx^post3 == 0 /\ -ret_nbc18^post3+ret_nbc18^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ nx4^0-nx4^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ res10^0-res10^post3 == 0 /\ -nx9^post3+nx9^0 == 0), cost: 1
   3: l3 -> l4 : ni6^0'=ni6^post4, nx4^0'=nx4^post4, nx9^0'=nx9^post4, nx^0'=nx^post4, res10^0'=res10^post4, res5^0'=res5^post4, ret_nbc18^0'=ret_nbc18^post4, ret_nbc211^0'=ret_nbc211^post4, tmp7^0'=tmp7^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (0 == 0 /\ -res5^post4+res5^0 == 0 /\ -tmp7^post4+tmp7^0 == 0 /\ tmp___0^post4-ret_nbc211^post4 == 0 /\ -nx^0+nx9^post4 == 0 /\ nx^0-nx^post4 == 0 /\ 16-ni6^0 <= 0 /\ ret_nbc18^post4-res5^0 == 0 /\ tmp^post4-ret_nbc18^post4 == 0 /\ res10^1-nx9^post4 == 0 /\ -ni6^post4+ni6^0 == 0 /\ nx4^0-nx4^post4 == 0 /\ ret_nbc211^post4-res10^post4 == 0), cost: 1
   4: l3 -> l2 : ni6^0'=ni6^post5, nx4^0'=nx4^post5, nx9^0'=nx9^post5, nx^0'=nx^post5, res10^0'=res10^post5, res5^0'=res5^post5, ret_nbc18^0'=ret_nbc18^post5, ret_nbc211^0'=ret_nbc211^post5, tmp7^0'=tmp7^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (tmp7^0-tmp7^post5 == 0 /\ -15+ni6^0 <= 0 /\ nx^0-nx^post5 == 0 /\ -ret_nbc211^post5+ret_nbc211^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -ret_nbc18^post5+ret_nbc18^0 == 0 /\ res10^0-res10^post5 == 0 /\ -res5^post5+res5^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ -ni6^post5+ni6^0 == 0 /\ nx9^0-nx9^post5 == 0 /\ -nx4^post5+nx4^0 == 0), cost: 1
   6: l5 -> l1 : ni6^0'=ni6^post7, nx4^0'=nx4^post7, nx9^0'=nx9^post7, nx^0'=nx^post7, res10^0'=res10^post7, res5^0'=res5^post7, ret_nbc18^0'=ret_nbc18^post7, ret_nbc211^0'=ret_nbc211^post7, tmp7^0'=tmp7^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (res10^0-res10^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ nx^0-nx^post7 == 0 /\ nx9^0-nx9^post7 == 0 /\ res5^post7 == 0 /\ -ret_nbc18^post7+ret_nbc18^0 == 0 /\ nx4^post7-nx^0 == 0 /\ ni6^post7 == 0 /\ -ret_nbc211^post7+ret_nbc211^0 == 0 /\ tmp7^0-tmp7^post7 == 0), cost: 1
   7: l6 -> l5 : ni6^0'=ni6^post8, nx4^0'=nx4^post8, nx9^0'=nx9^post8, nx^0'=nx^post8, res10^0'=res10^post8, res5^0'=res5^post8, ret_nbc18^0'=ret_nbc18^post8, ret_nbc211^0'=ret_nbc211^post8, tmp7^0'=tmp7^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (tmp^0-tmp^post8 == 0 /\ nx9^0-nx9^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -ret_nbc18^post8+ret_nbc18^0 == 0 /\ -res5^post8+res5^0 == 0 /\ ret_nbc211^0-ret_nbc211^post8 == 0 /\ -nx4^post8+nx4^0 == 0 /\ res10^0-res10^post8 == 0 /\ tmp7^0-tmp7^post8 == 0 /\ -nx^post8+nx^0 == 0 /\ -ni6^post8+ni6^0 == 0), cost: 1

Chained Linear Paths

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   0: l0 -> l1 : ni6^0'=ni6^post1, nx4^0'=nx4^post1, nx9^0'=nx9^post1, nx^0'=nx^post1, res10^0'=res10^post1, res5^0'=res5^post1, ret_nbc18^0'=ret_nbc18^post1, ret_nbc211^0'=ret_nbc211^post1, tmp7^0'=tmp7^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (nx^0-nx^post1 == 0 /\ ret_nbc211^0-ret_nbc211^post1 == 0 /\ -ret_nbc18^post1+ret_nbc18^0 == 0 /\ -nx4^post1+nx4^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ res10^0-res10^post1 == 0 /\ -tmp7^0+res5^post1-res5^0 == 0 /\ nx9^0-nx9^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -tmp7^post1+tmp7^0 == 0 /\ -1+ni6^post1-ni6^0 == 0), cost: 1
   5: l1 -> l3 : ni6^0'=ni6^post6, nx4^0'=nx4^post6, nx9^0'=nx9^post6, nx^0'=nx^post6, res10^0'=res10^post6, res5^0'=res5^post6, ret_nbc18^0'=ret_nbc18^post6, ret_nbc211^0'=ret_nbc211^post6, tmp7^0'=tmp7^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-ret_nbc18^post6+ret_nbc18^0 == 0 /\ nx^0-nx^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -nx9^post6+nx9^0 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ -res5^post6+res5^0 == 0 /\ -ni6^post6+ni6^0 == 0 /\ res10^0-res10^post6 == 0 /\ ret_nbc211^0-ret_nbc211^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ nx4^0-nx4^post6 == 0), cost: 1
   1: l2 -> l0 : ni6^0'=ni6^post2, nx4^0'=nx4^post2, nx9^0'=nx9^post2, nx^0'=nx^post2, res10^0'=res10^post2, res5^0'=res5^post2, ret_nbc18^0'=ret_nbc18^post2, ret_nbc211^0'=ret_nbc211^post2, tmp7^0'=tmp7^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-nx^post2+nx^0 == 0 /\ -res5^post2+res5^0 == 0 /\ nx9^0-nx9^post2 == 0 /\ -ni6^post2+ni6^0 == 0 /\ -nx4^post2+nx4^0 == 0 /\ -ret_nbc18^post2+ret_nbc18^0 == 0 /\ tmp7^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -ret_nbc211^post2+ret_nbc211^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ res10^0-res10^post2 == 0), cost: 1
   2: l2 -> l0 : ni6^0'=ni6^post3, nx4^0'=nx4^post3, nx9^0'=nx9^post3, nx^0'=nx^post3, res10^0'=res10^post3, res5^0'=res5^post3, ret_nbc18^0'=ret_nbc18^post3, ret_nbc211^0'=ret_nbc211^post3, tmp7^0'=tmp7^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (-ni6^post3+ni6^0 == 0 /\ -res5^post3+res5^0 == 0 /\ -1+tmp7^post3 == 0 /\ ret_nbc211^0-ret_nbc211^post3 == 0 /\ nx^0-nx^post3 == 0 /\ -ret_nbc18^post3+ret_nbc18^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ nx4^0-nx4^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ res10^0-res10^post3 == 0 /\ -nx9^post3+nx9^0 == 0), cost: 1
   3: l3 -> l4 : ni6^0'=ni6^post4, nx4^0'=nx4^post4, nx9^0'=nx9^post4, nx^0'=nx^post4, res10^0'=res10^post4, res5^0'=res5^post4, ret_nbc18^0'=ret_nbc18^post4, ret_nbc211^0'=ret_nbc211^post4, tmp7^0'=tmp7^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (0 == 0 /\ -res5^post4+res5^0 == 0 /\ -tmp7^post4+tmp7^0 == 0 /\ tmp___0^post4-ret_nbc211^post4 == 0 /\ -nx^0+nx9^post4 == 0 /\ nx^0-nx^post4 == 0 /\ 16-ni6^0 <= 0 /\ ret_nbc18^post4-res5^0 == 0 /\ tmp^post4-ret_nbc18^post4 == 0 /\ res10^1-nx9^post4 == 0 /\ -ni6^post4+ni6^0 == 0 /\ nx4^0-nx4^post4 == 0 /\ ret_nbc211^post4-res10^post4 == 0), cost: 1
   4: l3 -> l2 : ni6^0'=ni6^post5, nx4^0'=nx4^post5, nx9^0'=nx9^post5, nx^0'=nx^post5, res10^0'=res10^post5, res5^0'=res5^post5, ret_nbc18^0'=ret_nbc18^post5, ret_nbc211^0'=ret_nbc211^post5, tmp7^0'=tmp7^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (tmp7^0-tmp7^post5 == 0 /\ -15+ni6^0 <= 0 /\ nx^0-nx^post5 == 0 /\ -ret_nbc211^post5+ret_nbc211^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -ret_nbc18^post5+ret_nbc18^0 == 0 /\ res10^0-res10^post5 == 0 /\ -res5^post5+res5^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ -ni6^post5+ni6^0 == 0 /\ nx9^0-nx9^post5 == 0 /\ -nx4^post5+nx4^0 == 0), cost: 1
   8: l6 -> l1 : ni6^0'=ni6^post7, nx4^0'=nx4^post7, nx9^0'=nx9^post7, nx^0'=nx^post7, res10^0'=res10^post7, res5^0'=res5^post7, ret_nbc18^0'=ret_nbc18^post7, ret_nbc211^0'=ret_nbc211^post7, tmp7^0'=tmp7^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (tmp^0-tmp^post8 == 0 /\ nx9^0-nx9^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -ret_nbc211^post7+ret_nbc211^post8 == 0 /\ nx^post8-nx^post7 == 0 /\ tmp___0^post8-tmp___0^post7 == 0 /\ -ret_nbc18^post8+ret_nbc18^0 == 0 /\ res5^post7 == 0 /\ -res5^post8+res5^0 == 0 /\ -nx9^post7+nx9^post8 == 0 /\ -res10^post7+res10^post8 == 0 /\ nx4^post7-nx^post8 == 0 /\ tmp^post8-tmp^post7 == 0 /\ -tmp7^post7+tmp7^post8 == 0 /\ ret_nbc211^0-ret_nbc211^post8 == 0 /\ -nx4^post8+nx4^0 == 0 /\ res10^0-res10^post8 == 0 /\ ni6^post7 == 0 /\ tmp7^0-tmp7^post8 == 0 /\ ret_nbc18^post8-ret_nbc18^post7 == 0 /\ -nx^post8+nx^0 == 0 /\ -ni6^post8+ni6^0 == 0), cost: 1

	Eliminating location l5 by chaining:

	Applied chaining

	First rule:
	l6 -> l5 : ni6^0'=ni6^post8, nx4^0'=nx4^post8, nx9^0'=nx9^post8, nx^0'=nx^post8, res10^0'=res10^post8, res5^0'=res5^post8, ret_nbc18^0'=ret_nbc18^post8, ret_nbc211^0'=ret_nbc211^post8, tmp7^0'=tmp7^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (tmp^0-tmp^post8 == 0 /\ nx9^0-nx9^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -ret_nbc18^post8+ret_nbc18^0 == 0 /\ -res5^post8+res5^0 == 0 /\ ret_nbc211^0-ret_nbc211^post8 == 0 /\ -nx4^post8+nx4^0 == 0 /\ res10^0-res10^post8 == 0 /\ tmp7^0-tmp7^post8 == 0 /\ -nx^post8+nx^0 == 0 /\ -ni6^post8+ni6^0 == 0), cost: 1
	Second rule:
	l5 -> l1 : ni6^0'=ni6^post7, nx4^0'=nx4^post7, nx9^0'=nx9^post7, nx^0'=nx^post7, res10^0'=res10^post7, res5^0'=res5^post7, ret_nbc18^0'=ret_nbc18^post7, ret_nbc211^0'=ret_nbc211^post7, tmp7^0'=tmp7^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (res10^0-res10^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ nx^0-nx^post7 == 0 /\ nx9^0-nx9^post7 == 0 /\ res5^post7 == 0 /\ -ret_nbc18^post7+ret_nbc18^0 == 0 /\ nx4^post7-nx^0 == 0 /\ ni6^post7 == 0 /\ -ret_nbc211^post7+ret_nbc211^0 == 0 /\ tmp7^0-tmp7^post7 == 0), cost: 1
	New rule:
	l6 -> l1 : ni6^0'=ni6^post7, nx4^0'=nx4^post7, nx9^0'=nx9^post7, nx^0'=nx^post7, res10^0'=res10^post7, res5^0'=res5^post7, ret_nbc18^0'=ret_nbc18^post7, ret_nbc211^0'=ret_nbc211^post7, tmp7^0'=tmp7^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (tmp^0-tmp^post8 == 0 /\ nx9^0-nx9^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -ret_nbc211^post7+ret_nbc211^post8 == 0 /\ nx^post8-nx^post7 == 0 /\ tmp___0^post8-tmp___0^post7 == 0 /\ -ret_nbc18^post8+ret_nbc18^0 == 0 /\ res5^post7 == 0 /\ -res5^post8+res5^0 == 0 /\ -nx9^post7+nx9^post8 == 0 /\ -res10^post7+res10^post8 == 0 /\ nx4^post7-nx^post8 == 0 /\ tmp^post8-tmp^post7 == 0 /\ -tmp7^post7+tmp7^post8 == 0 /\ ret_nbc211^0-ret_nbc211^post8 == 0 /\ -nx4^post8+nx4^0 == 0 /\ res10^0-res10^post8 == 0 /\ ni6^post7 == 0 /\ tmp7^0-tmp7^post8 == 0 /\ ret_nbc18^post8-ret_nbc18^post7 == 0 /\ -nx^post8+nx^0 == 0 /\ -ni6^post8+ni6^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 6 7

Simplified Transitions

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   9: l0 -> l1 : ni6^0'=1+ni6^0, res5^0'=tmp7^0+res5^0, T, cost: 1
  14: l1 -> l3 : T, cost: 1
  10: l2 -> l0 : tmp7^0'=0, T, cost: 1
  11: l2 -> l0 : tmp7^0'=1, T, cost: 1
  12: l3 -> l4 : nx9^0'=nx^0, res10^0'=tmp___0^post4, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
  13: l3 -> l2 : -15+ni6^0 <= 0, cost: 1
  15: l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, res5^0'=0, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : ni6^0'=ni6^post1, nx4^0'=nx4^post1, nx9^0'=nx9^post1, nx^0'=nx^post1, res10^0'=res10^post1, res5^0'=res5^post1, ret_nbc18^0'=ret_nbc18^post1, ret_nbc211^0'=ret_nbc211^post1, tmp7^0'=tmp7^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (nx^0-nx^post1 == 0 /\ ret_nbc211^0-ret_nbc211^post1 == 0 /\ -ret_nbc18^post1+ret_nbc18^0 == 0 /\ -nx4^post1+nx4^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ res10^0-res10^post1 == 0 /\ -tmp7^0+res5^post1-res5^0 == 0 /\ nx9^0-nx9^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -tmp7^post1+tmp7^0 == 0 /\ -1+ni6^post1-ni6^0 == 0), cost: 1
	New rule:
	l0 -> l1 : ni6^0'=1+ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=tmp7^0+res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality nx^post1 = nx^0
		
		propagated equality ret_nbc211^post1 = ret_nbc211^0
		
		propagated equality ret_nbc18^post1 = ret_nbc18^0
		
		propagated equality nx4^post1 = nx4^0
		
		propagated equality tmp^post1 = tmp^0
		
		propagated equality res10^post1 = res10^0
		
		propagated equality res5^post1 = tmp7^0+res5^0
		
		propagated equality nx9^post1 = nx9^0
		
		propagated equality tmp___0^post1 = tmp___0^0
		
		propagated equality tmp7^post1 = tmp7^0
		
		propagated equality ni6^post1 = 1+ni6^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : ni6^0'=1+ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=tmp7^0+res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l0 -> l1 : ni6^0'=1+ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=tmp7^0+res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : ni6^0'=1+ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=tmp7^0+res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l0 -> l1 : ni6^0'=1+ni6^0, res5^0'=tmp7^0+res5^0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l0 : ni6^0'=ni6^post2, nx4^0'=nx4^post2, nx9^0'=nx9^post2, nx^0'=nx^post2, res10^0'=res10^post2, res5^0'=res5^post2, ret_nbc18^0'=ret_nbc18^post2, ret_nbc211^0'=ret_nbc211^post2, tmp7^0'=tmp7^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-nx^post2+nx^0 == 0 /\ -res5^post2+res5^0 == 0 /\ nx9^0-nx9^post2 == 0 /\ -ni6^post2+ni6^0 == 0 /\ -nx4^post2+nx4^0 == 0 /\ -ret_nbc18^post2+ret_nbc18^0 == 0 /\ tmp7^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -ret_nbc211^post2+ret_nbc211^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ res10^0-res10^post2 == 0), cost: 1
	New rule:
	l2 -> l0 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality nx^post2 = nx^0
		
		propagated equality res5^post2 = res5^0
		
		propagated equality nx9^post2 = nx9^0
		
		propagated equality ni6^post2 = ni6^0
		
		propagated equality nx4^post2 = nx4^0
		
		propagated equality ret_nbc18^post2 = ret_nbc18^0
		
		propagated equality tmp7^post2 = 0
		
		propagated equality tmp^post2 = tmp^0
		
		propagated equality ret_nbc211^post2 = ret_nbc211^0
		
		propagated equality tmp___0^post2 = tmp___0^0
		
		propagated equality res10^post2 = res10^0
		
	Simplified Guard

	Original rule:
	l2 -> l0 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l2 -> l0 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l0 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l2 -> l0 : tmp7^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l0 : ni6^0'=ni6^post3, nx4^0'=nx4^post3, nx9^0'=nx9^post3, nx^0'=nx^post3, res10^0'=res10^post3, res5^0'=res5^post3, ret_nbc18^0'=ret_nbc18^post3, ret_nbc211^0'=ret_nbc211^post3, tmp7^0'=tmp7^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (-ni6^post3+ni6^0 == 0 /\ -res5^post3+res5^0 == 0 /\ -1+tmp7^post3 == 0 /\ ret_nbc211^0-ret_nbc211^post3 == 0 /\ nx^0-nx^post3 == 0 /\ -ret_nbc18^post3+ret_nbc18^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ nx4^0-nx4^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ res10^0-res10^post3 == 0 /\ -nx9^post3+nx9^0 == 0), cost: 1
	New rule:
	l2 -> l0 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=1, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality ni6^post3 = ni6^0
		
		propagated equality res5^post3 = res5^0
		
		propagated equality tmp7^post3 = 1
		
		propagated equality ret_nbc211^post3 = ret_nbc211^0
		
		propagated equality nx^post3 = nx^0
		
		propagated equality ret_nbc18^post3 = ret_nbc18^0
		
		propagated equality tmp^post3 = tmp^0
		
		propagated equality nx4^post3 = nx4^0
		
		propagated equality tmp___0^post3 = tmp___0^0
		
		propagated equality res10^post3 = res10^0
		
		propagated equality nx9^post3 = nx9^0
		
	Simplified Guard

	Original rule:
	l2 -> l0 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=1, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l2 -> l0 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=1, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l0 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=1, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l2 -> l0 : tmp7^0'=1, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l4 : ni6^0'=ni6^post4, nx4^0'=nx4^post4, nx9^0'=nx9^post4, nx^0'=nx^post4, res10^0'=res10^post4, res5^0'=res5^post4, ret_nbc18^0'=ret_nbc18^post4, ret_nbc211^0'=ret_nbc211^post4, tmp7^0'=tmp7^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (0 == 0 /\ -res5^post4+res5^0 == 0 /\ -tmp7^post4+tmp7^0 == 0 /\ tmp___0^post4-ret_nbc211^post4 == 0 /\ -nx^0+nx9^post4 == 0 /\ nx^0-nx^post4 == 0 /\ 16-ni6^0 <= 0 /\ ret_nbc18^post4-res5^0 == 0 /\ tmp^post4-ret_nbc18^post4 == 0 /\ res10^1-nx9^post4 == 0 /\ -ni6^post4+ni6^0 == 0 /\ nx4^0-nx4^post4 == 0 /\ ret_nbc211^post4-res10^post4 == 0), cost: 1
	New rule:
	l3 -> l4 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx^0, nx^0'=nx^0, res10^0'=tmp___0^post4, res5^0'=res5^0, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp7^0'=tmp7^0, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, (0 == 0 /\ res10^1-nx^0 == 0 /\ 16-ni6^0 <= 0), cost: 1
	
		propagated equality res5^post4 = res5^0
		
		propagated equality tmp7^post4 = tmp7^0
		
		propagated equality ret_nbc211^post4 = tmp___0^post4
		
		propagated equality nx9^post4 = nx^0
		
		propagated equality nx^post4 = nx^0
		
		propagated equality ret_nbc18^post4 = res5^0
		
		propagated equality tmp^post4 = res5^0
		
		propagated equality ni6^post4 = ni6^0
		
		propagated equality nx4^post4 = nx4^0
		
		propagated equality res10^post4 = tmp___0^post4
		
	Propagated Equalities

	Original rule:
	l3 -> l4 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx^0, nx^0'=nx^0, res10^0'=tmp___0^post4, res5^0'=res5^0, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp7^0'=tmp7^0, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, (0 == 0 /\ res10^1-nx^0 == 0 /\ 16-ni6^0 <= 0), cost: 1
	New rule:
	l3 -> l4 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx^0, nx^0'=nx^0, res10^0'=tmp___0^post4, res5^0'=res5^0, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp7^0'=tmp7^0, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, (0 == 0 /\ 16-ni6^0 <= 0), cost: 1
	
		propagated equality res10^1 = nx^0
		
	Simplified Guard

	Original rule:
	l3 -> l4 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx^0, nx^0'=nx^0, res10^0'=tmp___0^post4, res5^0'=res5^0, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp7^0'=tmp7^0, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, (0 == 0 /\ 16-ni6^0 <= 0), cost: 1
	New rule:
	l3 -> l4 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx^0, nx^0'=nx^0, res10^0'=tmp___0^post4, res5^0'=res5^0, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp7^0'=tmp7^0, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l4 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx^0, nx^0'=nx^0, res10^0'=tmp___0^post4, res5^0'=res5^0, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp7^0'=tmp7^0, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
	New rule:
	l3 -> l4 : nx9^0'=nx^0, res10^0'=tmp___0^post4, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l2 : ni6^0'=ni6^post5, nx4^0'=nx4^post5, nx9^0'=nx9^post5, nx^0'=nx^post5, res10^0'=res10^post5, res5^0'=res5^post5, ret_nbc18^0'=ret_nbc18^post5, ret_nbc211^0'=ret_nbc211^post5, tmp7^0'=tmp7^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (tmp7^0-tmp7^post5 == 0 /\ -15+ni6^0 <= 0 /\ nx^0-nx^post5 == 0 /\ -ret_nbc211^post5+ret_nbc211^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -ret_nbc18^post5+ret_nbc18^0 == 0 /\ res10^0-res10^post5 == 0 /\ -res5^post5+res5^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ -ni6^post5+ni6^0 == 0 /\ nx9^0-nx9^post5 == 0 /\ -nx4^post5+nx4^0 == 0), cost: 1
	New rule:
	l3 -> l2 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -15+ni6^0 <= 0), cost: 1
	
		propagated equality tmp7^post5 = tmp7^0
		
		propagated equality nx^post5 = nx^0
		
		propagated equality ret_nbc211^post5 = ret_nbc211^0
		
		propagated equality tmp^post5 = tmp^0
		
		propagated equality ret_nbc18^post5 = ret_nbc18^0
		
		propagated equality res10^post5 = res10^0
		
		propagated equality res5^post5 = res5^0
		
		propagated equality tmp___0^post5 = tmp___0^0
		
		propagated equality ni6^post5 = ni6^0
		
		propagated equality nx9^post5 = nx9^0
		
		propagated equality nx4^post5 = nx4^0
		
	Simplified Guard

	Original rule:
	l3 -> l2 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -15+ni6^0 <= 0), cost: 1
	New rule:
	l3 -> l2 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -15+ni6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l2 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -15+ni6^0 <= 0, cost: 1
	New rule:
	l3 -> l2 : -15+ni6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l3 : ni6^0'=ni6^post6, nx4^0'=nx4^post6, nx9^0'=nx9^post6, nx^0'=nx^post6, res10^0'=res10^post6, res5^0'=res5^post6, ret_nbc18^0'=ret_nbc18^post6, ret_nbc211^0'=ret_nbc211^post6, tmp7^0'=tmp7^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-ret_nbc18^post6+ret_nbc18^0 == 0 /\ nx^0-nx^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -nx9^post6+nx9^0 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ -res5^post6+res5^0 == 0 /\ -ni6^post6+ni6^0 == 0 /\ res10^0-res10^post6 == 0 /\ ret_nbc211^0-ret_nbc211^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ nx4^0-nx4^post6 == 0), cost: 1
	New rule:
	l1 -> l3 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality ret_nbc18^post6 = ret_nbc18^0
		
		propagated equality nx^post6 = nx^0
		
		propagated equality tmp___0^post6 = tmp___0^0
		
		propagated equality nx9^post6 = nx9^0
		
		propagated equality tmp7^post6 = tmp7^0
		
		propagated equality res5^post6 = res5^0
		
		propagated equality ni6^post6 = ni6^0
		
		propagated equality res10^post6 = res10^0
		
		propagated equality ret_nbc211^post6 = ret_nbc211^0
		
		propagated equality tmp^post6 = tmp^0
		
		propagated equality nx4^post6 = nx4^0
		
	Simplified Guard

	Original rule:
	l1 -> l3 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l1 -> l3 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l3 : ni6^0'=ni6^0, nx4^0'=nx4^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=res5^0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l1 -> l3 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l1 : ni6^0'=ni6^post7, nx4^0'=nx4^post7, nx9^0'=nx9^post7, nx^0'=nx^post7, res10^0'=res10^post7, res5^0'=res5^post7, ret_nbc18^0'=ret_nbc18^post7, ret_nbc211^0'=ret_nbc211^post7, tmp7^0'=tmp7^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (tmp^0-tmp^post8 == 0 /\ nx9^0-nx9^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -ret_nbc211^post7+ret_nbc211^post8 == 0 /\ nx^post8-nx^post7 == 0 /\ tmp___0^post8-tmp___0^post7 == 0 /\ -ret_nbc18^post8+ret_nbc18^0 == 0 /\ res5^post7 == 0 /\ -res5^post8+res5^0 == 0 /\ -nx9^post7+nx9^post8 == 0 /\ -res10^post7+res10^post8 == 0 /\ nx4^post7-nx^post8 == 0 /\ tmp^post8-tmp^post7 == 0 /\ -tmp7^post7+tmp7^post8 == 0 /\ ret_nbc211^0-ret_nbc211^post8 == 0 /\ -nx4^post8+nx4^0 == 0 /\ res10^0-res10^post8 == 0 /\ ni6^post7 == 0 /\ tmp7^0-tmp7^post8 == 0 /\ ret_nbc18^post8-ret_nbc18^post7 == 0 /\ -nx^post8+nx^0 == 0 /\ -ni6^post8+ni6^0 == 0), cost: 1
	New rule:
	l6 -> l1 : ni6^0'=0, nx4^0'=nx^post8, nx9^0'=nx9^post8, nx^0'=nx^post8, res10^0'=res10^post8, res5^0'=0, ret_nbc18^0'=ret_nbc18^post8, ret_nbc211^0'=ret_nbc211^post8, tmp7^0'=tmp7^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (0 == 0 /\ tmp^0-tmp^post8 == 0 /\ nx9^0-nx9^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -ret_nbc18^post8+ret_nbc18^0 == 0 /\ -res5^post8+res5^0 == 0 /\ ret_nbc211^0-ret_nbc211^post8 == 0 /\ -nx4^post8+nx4^0 == 0 /\ res10^0-res10^post8 == 0 /\ tmp7^0-tmp7^post8 == 0 /\ -nx^post8+nx^0 == 0 /\ -ni6^post8+ni6^0 == 0), cost: 1
	
		propagated equality ret_nbc211^post7 = ret_nbc211^post8
		
		propagated equality nx^post7 = nx^post8
		
		propagated equality tmp___0^post7 = tmp___0^post8
		
		propagated equality res5^post7 = 0
		
		propagated equality nx9^post7 = nx9^post8
		
		propagated equality res10^post7 = res10^post8
		
		propagated equality nx4^post7 = nx^post8
		
		propagated equality tmp^post7 = tmp^post8
		
		propagated equality tmp7^post7 = tmp7^post8
		
		propagated equality ni6^post7 = 0
		
		propagated equality ret_nbc18^post7 = ret_nbc18^post8
		
	Propagated Equalities

	Original rule:
	l6 -> l1 : ni6^0'=0, nx4^0'=nx^post8, nx9^0'=nx9^post8, nx^0'=nx^post8, res10^0'=res10^post8, res5^0'=0, ret_nbc18^0'=ret_nbc18^post8, ret_nbc211^0'=ret_nbc211^post8, tmp7^0'=tmp7^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (0 == 0 /\ tmp^0-tmp^post8 == 0 /\ nx9^0-nx9^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -ret_nbc18^post8+ret_nbc18^0 == 0 /\ -res5^post8+res5^0 == 0 /\ ret_nbc211^0-ret_nbc211^post8 == 0 /\ -nx4^post8+nx4^0 == 0 /\ res10^0-res10^post8 == 0 /\ tmp7^0-tmp7^post8 == 0 /\ -nx^post8+nx^0 == 0 /\ -ni6^post8+ni6^0 == 0), cost: 1
	New rule:
	l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality tmp^post8 = tmp^0
		
		propagated equality nx9^post8 = nx9^0
		
		propagated equality tmp___0^post8 = tmp___0^0
		
		propagated equality ret_nbc18^post8 = ret_nbc18^0
		
		propagated equality res5^post8 = res5^0
		
		propagated equality ret_nbc211^post8 = ret_nbc211^0
		
		propagated equality nx4^post8 = nx4^0
		
		propagated equality res10^post8 = res10^0
		
		propagated equality tmp7^post8 = tmp7^0
		
		propagated equality nx^post8 = nx^0
		
		propagated equality ni6^post8 = ni6^0
		
	Simplified Guard

	Original rule:
	l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, nx9^0'=nx9^0, nx^0'=nx^0, res10^0'=res10^0, res5^0'=0, ret_nbc18^0'=ret_nbc18^0, ret_nbc211^0'=ret_nbc211^0, tmp7^0'=tmp7^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, res5^0'=0, T, cost: 1

Step with 15

	Trace

	15[T]
	
	Blocked

	[{}, {}]

Step with 14

	Trace

	15[T], 14[T]
	
	Blocked

	[{}, {}, {}]

Step with 13

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Step with 10

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Step with 9

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

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

Accelerate

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   9: l0 -> l1 : ni6^0'=1+ni6^0, res5^0'=tmp7^0+res5^0, T, cost: 1
  14: l1 -> l3 : T, cost: 1
  16: l1 -> l1 : ni6^0'=n+ni6^0, tmp7^0'=0, (-1+n >= 0 /\ 16-n-ni6^0 >= 0), cost: 1
  10: l2 -> l0 : tmp7^0'=0, T, cost: 1
  11: l2 -> l0 : tmp7^0'=1, T, cost: 1
  12: l3 -> l4 : nx9^0'=nx^0, res10^0'=tmp___0^post4, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
  13: l3 -> l2 : -15+ni6^0 <= 0, cost: 1
  15: l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, res5^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l1 -> l1 : ni6^0'=1+ni6^0, tmp7^0'=0, -15+ni6^0 <= 0, cost: 1
	New rule:
	l1 -> l1 : ni6^0'=n+ni6^0, tmp7^0'=0, (-1+n >= 0 /\ 16-n-ni6^0 >= 0), cost: 1

		15-ni6^0 >= 0 [0]: montonic decrease yields 16-n-ni6^0 >= 0
		
		15-ni6^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 15-ni6^0 >= 0)
		
		Replacement map: {15-ni6^0 >= 0 -> 16-n-ni6^0 >= 0}

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

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

Step with 14

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T]
	
	Blocked

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

Step with 13

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Step with 10

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Step with 9

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

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

Covered

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Backtrack

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Step with 11

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

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

Step with 9

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

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

Accelerate

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   9: l0 -> l1 : ni6^0'=1+ni6^0, res5^0'=tmp7^0+res5^0, T, cost: 1
  14: l1 -> l3 : T, cost: 1
  16: l1 -> l1 : ni6^0'=n+ni6^0, tmp7^0'=0, (-1+n >= 0 /\ 16-n-ni6^0 >= 0), cost: 1
  17: l1 -> l1 : ni6^0'=n2+ni6^0, res5^0'=n2+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0), cost: 1
  10: l2 -> l0 : tmp7^0'=0, T, cost: 1
  11: l2 -> l0 : tmp7^0'=1, T, cost: 1
  12: l3 -> l4 : nx9^0'=nx^0, res10^0'=tmp___0^post4, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
  13: l3 -> l2 : -15+ni6^0 <= 0, cost: 1
  15: l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, res5^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l1 -> l1 : ni6^0'=1+ni6^0, res5^0'=1+res5^0, tmp7^0'=1, -15+ni6^0 <= 0, cost: 1
	New rule:
	l1 -> l1 : ni6^0'=n2+ni6^0, res5^0'=n2+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0), cost: 1

		15-ni6^0 >= 0 [0]: montonic decrease yields 16-n2-ni6^0 >= 0
		
		15-ni6^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 15-ni6^0 >= 0)
		
		Replacement map: {15-ni6^0 >= 0 -> 16-n2-ni6^0 >= 0}

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {17[T]}]

Accelerate

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   9: l0 -> l1 : ni6^0'=1+ni6^0, res5^0'=tmp7^0+res5^0, T, cost: 1
  14: l1 -> l3 : T, cost: 1
  16: l1 -> l1 : ni6^0'=n+ni6^0, tmp7^0'=0, (-1+n >= 0 /\ 16-n-ni6^0 >= 0), cost: 1
  17: l1 -> l1 : ni6^0'=n2+ni6^0, res5^0'=n2+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0), cost: 1
  18: l1 -> l1 : ni6^0'=n3*n1+n2*n3+ni6^0, res5^0'=n2*n3+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0), cost: 1
  10: l2 -> l0 : tmp7^0'=0, T, cost: 1
  11: l2 -> l0 : tmp7^0'=1, T, cost: 1
  12: l3 -> l4 : nx9^0'=nx^0, res10^0'=tmp___0^post4, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
  13: l3 -> l2 : -15+ni6^0 <= 0, cost: 1
  15: l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, res5^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l1 -> l1 : ni6^0'=n2+n1+ni6^0, res5^0'=n2+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ -1+n1 >= 0 /\ 16-n1-ni6^0 >= 0 /\ 16-n2-n1-ni6^0 >= 0), cost: 1
	New rule:
	l1 -> l1 : ni6^0'=n3*n1+n2*n3+ni6^0, res5^0'=n2*n3+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0), cost: 1

		-1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0
		
		-1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0
		
		16-n1-ni6^0 >= 0 [0]: montonic decrease yields 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0, dependencies: -1+n2 >= 0 -1+n1 >= 0
		
		16-n1-ni6^0 >= 0 [1]: eventual increase yields (n2+n1 <= 0 /\ 16-n1-ni6^0 >= 0)
		
		16-n2-n1-ni6^0 >= 0 [0]: montonic decrease yields 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0, dependencies: -1+n2 >= 0 -1+n1 >= 0
		
		16-n2-n1-ni6^0 >= 0 [1]: eventual increase yields (n2+n1 <= 0 /\ 16-n2-n1-ni6^0 >= 0)
		
		Replacement map: {-1+n2 >= 0 -> -1+n2 >= 0, -1+n1 >= 0 -> -1+n1 >= 0, 16-n1-ni6^0 >= 0 -> 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0, 16-n2-n1-ni6^0 >= 0 -> 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0}

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {}, {18[T]}]

Step with 14

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T]
	
	Blocked

	[{}, {}, {18[T]}, {}]

Step with 13

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {}, {18[T]}, {}, {}]

Step with 11

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {}, {18[T]}, {}, {}, {}]

Step with 9

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {}, {18[T]}, {}, {}, {}, {}]

Covered

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

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

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Step with 10

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Step with 9

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

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

Covered

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T]
	
	Blocked

	[{}, {}, {18[T]}, {13[T]}]

Step with 12

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

	[{}, {}, {18[T]}, {13[T]}, {}]

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T]
	
	Blocked

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

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {}, {14[T], 18[T]}]

Step with 16

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {}, {14[T], 18[T]}, {16[T]}]

Accelerate

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   9: l0 -> l1 : ni6^0'=1+ni6^0, res5^0'=tmp7^0+res5^0, T, cost: 1
  14: l1 -> l3 : T, cost: 1
  16: l1 -> l1 : ni6^0'=n+ni6^0, tmp7^0'=0, (-1+n >= 0 /\ 16-n-ni6^0 >= 0), cost: 1
  17: l1 -> l1 : ni6^0'=n2+ni6^0, res5^0'=n2+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0), cost: 1
  18: l1 -> l1 : ni6^0'=n3*n1+n2*n3+ni6^0, res5^0'=n2*n3+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0), cost: 1
  19: l1 -> l1 : ni6^0'=n31*n11*n5+n*n5+n31*n22*n5+ni6^0, res5^0'=n31*n22*n5+res5^0, tmp7^0'=0, (16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0), cost: 1
  10: l2 -> l0 : tmp7^0'=0, T, cost: 1
  11: l2 -> l0 : tmp7^0'=1, T, cost: 1
  12: l3 -> l4 : nx9^0'=nx^0, res10^0'=tmp___0^post4, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
  13: l3 -> l2 : -15+ni6^0 <= 0, cost: 1
  15: l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, res5^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l1 -> l1 : ni6^0'=n31*n22+n+n31*n11+ni6^0, res5^0'=n31*n22+res5^0, tmp7^0'=0, (16-n11-n22-n11*(-1+n31)-(-1+n31)*n22-ni6^0 >= 0 /\ 16-n11-n11*(-1+n31)-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0), cost: 1
	New rule:
	l1 -> l1 : ni6^0'=n31*n11*n5+n*n5+n31*n22*n5+ni6^0, res5^0'=n31*n22*n5+res5^0, tmp7^0'=0, (16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0), cost: 1

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

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

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

Step with 14

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T]
	
	Blocked

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

Step with 12

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

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

Backtrack

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T]
	
	Blocked

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

Step with 13

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Step with 10

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Step with 9

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

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

Covered

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Backtrack

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Step with 11

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

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

Step with 9

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

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

Covered

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

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

Backtrack

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Backtrack

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 14[T]
	
	Blocked

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

Backtrack

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {}, {14[T], 19[T]}]

Step with 16

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {}, {14[T], 19[T]}, {16[T]}]

Covered

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {}, {14[T], 16[T], 19[T]}]

Step with 17

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {}, {14[T], 16[T], 19[T]}, {17[T]}]

Covered

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {}, {14[T], 16[T], 17[T], 19[T]}]

Step with 18

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {}, {14[T], 16[T], 17[T], 19[T]}, {18[T]}]

Covered

	Trace

	15[T], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {}, {14[T], 16[T], 17[T], 18[T], 19[T]}]

Backtrack

	Trace

	15[T]
	
	Blocked

	[{}, {19[T]}]

Step with 18

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {19[T]}, {18[T]}]

Step with 19

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {19[T]}, {18[T]}, {19[T]}]

Covered

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}]

Step with 14

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}]

Step with 13

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}, {}]

Step with 11

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}, {}, {}]

Step with 9

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}, {}, {}, {}]

Covered

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}, {}, {9[T]}]

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}, {11[T]}]

Step with 10

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}, {11[T]}, {}]

Step with 9

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}, {11[T]}, {}, {}]

Covered

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {}, {11[T]}, {9[T]}]

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {13[T]}]

Step with 12

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

	[{}, {19[T]}, {18[T], 19[T]}, {13[T]}, {}]

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 14[T]
	
	Blocked

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

Backtrack

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {19[T]}, {14[T], 18[T], 19[T]}]

Step with 16

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {19[T]}, {14[T], 18[T], 19[T]}, {16[T]}]

Covered

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {19[T]}, {14[T], 16[T], 18[T], 19[T]}]

Step with 17

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {19[T]}, {14[T], 16[T], 18[T], 19[T]}, {17[T]}]

Covered

	Trace

	15[T], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {19[T]}, {14[T], 16[T], 17[T], 18[T], 19[T]}]

Backtrack

	Trace

	15[T]
	
	Blocked

	[{}, {18[T], 19[T]}]

Step with 17

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

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

Step with 18

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

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

Accelerate

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   9: l0 -> l1 : ni6^0'=1+ni6^0, res5^0'=tmp7^0+res5^0, T, cost: 1
  14: l1 -> l3 : T, cost: 1
  16: l1 -> l1 : ni6^0'=n+ni6^0, tmp7^0'=0, (-1+n >= 0 /\ 16-n-ni6^0 >= 0), cost: 1
  17: l1 -> l1 : ni6^0'=n2+ni6^0, res5^0'=n2+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0), cost: 1
  18: l1 -> l1 : ni6^0'=n3*n1+n2*n3+ni6^0, res5^0'=n2*n3+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0), cost: 1
  19: l1 -> l1 : ni6^0'=n31*n11*n5+n*n5+n31*n22*n5+ni6^0, res5^0'=n31*n22*n5+res5^0, tmp7^0'=0, (16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0), cost: 1
  20: l1 -> l1 : ni6^0'=n2*n3*n10+n3*n10*n1+ni6^0+n10*n27, res5^0'=n2*n3*n10+n10*n27+res5^0, tmp7^0'=1, (16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0), cost: 1
  10: l2 -> l0 : tmp7^0'=0, T, cost: 1
  11: l2 -> l0 : tmp7^0'=1, T, cost: 1
  12: l3 -> l4 : nx9^0'=nx^0, res10^0'=tmp___0^post4, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
  13: l3 -> l2 : -15+ni6^0 <= 0, cost: 1
  15: l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, res5^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l1 -> l1 : ni6^0'=n3*n1+n2*n3+ni6^0+n27, res5^0'=n2*n3+n27+res5^0, tmp7^0'=1, (16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-ni6^0-n27 >= 0 /\ -1+n27 >= 0), cost: 1
	New rule:
	l1 -> l1 : ni6^0'=n2*n3*n10+n3*n10*n1+ni6^0+n10*n27, res5^0'=n2*n3*n10+n10*n27+res5^0, tmp7^0'=1, (16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0), cost: 1

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

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}]

Step with 14

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {}]

Step with 12

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {}, {}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T]
	
	Blocked

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

Step with 13

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Step with 10

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Step with 9

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

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

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {12[T]}, {}, {9[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {12[T]}, {10[T]}]

Step with 11

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {12[T]}, {10[T]}, {}]

Step with 9

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {12[T]}, {10[T]}, {}, {}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {12[T]}, {10[T]}, {9[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {12[T]}, {10[T], 11[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 14[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {20[T]}, {12[T], 13[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}]

Step with 16

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T]}]

Acceleration Failed

marked recursive suffix as redundant

Step with 17

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T]}, {17[T]}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T]}]

Step with 18

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T]}, {18[T]}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T]}]

Step with 19

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T]}, {19[T]}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T]}]

Step with 20

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T]}, {20[T]}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}]

Step with 14

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}]

Step with 13

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}]

Step with 11

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}, {}]

Step with 9

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}, {}, {}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}, {9[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {11[T]}]

Step with 10

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {11[T]}, {}]

Step with 9

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {11[T]}, {}, {}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {11[T]}, {9[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {10[T], 11[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {13[T]}]

Step with 12

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {13[T]}, {}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {12[T], 13[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 20[T]}, {14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}]

Backtrack

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 16[T], 20[T]}]

Step with 17

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 16[T], 20[T]}, {17[T]}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 16[T], 17[T], 20[T]}]

Step with 18

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 16[T], 17[T], 20[T]}, {18[T]}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 16[T], 17[T], 18[T], 20[T]}]

Step with 19

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 16[T], 17[T], 18[T], 20[T]}, {19[T]}]

Covered

	Trace

	15[T], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {18[T], 19[T]}, {14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}]

Backtrack

	Trace

	15[T]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}]

Step with 14

	Trace

	15[T], 14[T]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}, {}]

Step with 13

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

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

Step with 10

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

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

Step with 9

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

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

Covered

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}, {12[T]}, {}, {9[T]}]

Backtrack

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}, {12[T]}, {10[T]}]

Step with 11

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}, {12[T]}, {10[T]}, {}]

Step with 9

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}, {12[T]}, {10[T]}, {}, {}]

Covered

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}, {12[T]}, {10[T]}, {9[T]}]

Backtrack

	Trace

	15[T], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}, {12[T]}, {10[T], 11[T]}]

Backtrack

	Trace

	15[T], 14[T]
	
	Blocked

	[{}, {18[T], 19[T], 20[T]}, {12[T], 13[T]}]

Backtrack

	Trace

	15[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}]

Step with 16

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T]}]

Step with 17

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T]}, {17[T]}]

Covered

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T]}]

Step with 18

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T]}, {18[T]}]

Covered

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T]}]

Step with 19

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T]}, {19[T]}]

Covered

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T]}]

Step with 20

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T]}, {20[T]}]

Covered

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}]

Step with 14

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}]

Step with 13

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}]

Step with 11

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}, {}]

Step with 9

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}, {}, {}]

Covered

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}, {9[T]}]

Backtrack

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {11[T]}]

Step with 10

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {11[T]}, {}]

Step with 9

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {11[T]}, {}, {}]

Covered

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {11[T]}, {9[T]}]

Backtrack

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {10[T], 11[T]}]

Backtrack

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {13[T]}]

Step with 12

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {13[T]}, {}]

Backtrack

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {16[T], 17[T], 18[T], 19[T], 20[T]}, {12[T], 13[T]}]

Backtrack

	Trace

	15[T], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}]

Backtrack

	Trace

	15[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}]

Step with 17

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T]}]

Step with 18

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T]}, {18[T]}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T]}]

Step with 19

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T]}, {19[T]}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T]}]

Step with 20

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T]}, {20[T]}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}]

Step with 14

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {}]

Step with 12

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {}, {}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}]

Step with 13

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {}]

Step with 10

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {}, {}]

Step with 9

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {}, {}, {}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {}, {9[T]}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {10[T]}]

Step with 11

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {10[T]}, {}]

Step with 9

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {10[T]}, {}, {}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {10[T]}, {9[T]}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T]}, {10[T], 11[T]}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {17[T], 18[T], 19[T], 20[T]}, {12[T], 13[T]}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 17[T], 18[T], 19[T], 20[T]}]

Step with 16

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 17[T], 18[T], 19[T], 20[T]}, {16[T]}]

Accelerate

Start location: l6
Program variables: ni6^0 nx4^0 nx9^0 nx^0 res10^0 res5^0 ret_nbc18^0 ret_nbc211^0 tmp7^0 tmp^0 tmp___0^0
   9: l0 -> l1 : ni6^0'=1+ni6^0, res5^0'=tmp7^0+res5^0, T, cost: 1
  14: l1 -> l3 : T, cost: 1
  16: l1 -> l1 : ni6^0'=n+ni6^0, tmp7^0'=0, (-1+n >= 0 /\ 16-n-ni6^0 >= 0), cost: 1
  17: l1 -> l1 : ni6^0'=n2+ni6^0, res5^0'=n2+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0), cost: 1
  18: l1 -> l1 : ni6^0'=n3*n1+n2*n3+ni6^0, res5^0'=n2*n3+res5^0, tmp7^0'=1, (-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0), cost: 1
  19: l1 -> l1 : ni6^0'=n31*n11*n5+n*n5+n31*n22*n5+ni6^0, res5^0'=n31*n22*n5+res5^0, tmp7^0'=0, (16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0), cost: 1
  20: l1 -> l1 : ni6^0'=n2*n3*n10+n3*n10*n1+ni6^0+n10*n27, res5^0'=n2*n3*n10+n10*n27+res5^0, tmp7^0'=1, (16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0), cost: 1
  21: l1 -> l1 : ni6^0'=n218*n43+ni6^0+n43*n, res5^0'=n218*n43+res5^0, tmp7^0'=0, (-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0), cost: 1
  10: l2 -> l0 : tmp7^0'=0, T, cost: 1
  11: l2 -> l0 : tmp7^0'=1, T, cost: 1
  12: l3 -> l4 : nx9^0'=nx^0, res10^0'=tmp___0^post4, ret_nbc18^0'=res5^0, ret_nbc211^0'=tmp___0^post4, tmp^0'=res5^0, tmp___0^0'=tmp___0^post4, 16-ni6^0 <= 0, cost: 1
  13: l3 -> l2 : -15+ni6^0 <= 0, cost: 1
  15: l6 -> l1 : ni6^0'=0, nx4^0'=nx^0, res5^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l1 -> l1 : ni6^0'=n218+n+ni6^0, res5^0'=n218+res5^0, tmp7^0'=0, (16-n218-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-n-ni6^0 >= 0), cost: 1
	New rule:
	l1 -> l1 : ni6^0'=n218*n43+ni6^0+n43*n, res5^0'=n218*n43+res5^0, tmp7^0'=0, (-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0), cost: 1

		16-n218-ni6^0 >= 0 [0]: montonic decrease yields 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0, dependencies: -1+n218 >= 0 -1+n >= 0
		
		16-n218-ni6^0 >= 0 [1]: eventual decrease yields (16-n218-ni6^0 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0), dependencies: -1+n218 >= 0 -1+n >= 0
		
		16-n218-ni6^0 >= 0 [2]: eventual increase yields (16-n218-ni6^0 >= 0 /\ n218+n <= 0), dependencies: -1+n218 >= 0 -1+n >= 0
		
		-1+n218 >= 0 [0]: monotonic increase yields -1+n218 >= 0
		
		-1+n >= 0 [0]: monotonic increase yields -1+n >= 0
		
		16-n218-n-ni6^0 >= 0 [0]: montonic decrease yields 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0, dependencies: -1+n218 >= 0 -1+n >= 0
		
		16-n218-n-ni6^0 >= 0 [1]: eventual increase yields (n218+n <= 0 /\ 16-n218-n-ni6^0 >= 0), dependencies: -1+n218 >= 0 -1+n >= 0
		
		Replacement map: {16-n218-ni6^0 >= 0 -> 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0, -1+n218 >= 0 -> -1+n218 >= 0, -1+n >= 0 -> -1+n >= 0, 16-n218-n-ni6^0 >= 0 -> 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0}

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}]

Step with 14

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}]

Step with 13

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {}]

Step with 11

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {}, {}]

Step with 9

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {}, {}, {}]

Covered

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {}, {9[T]}]

Backtrack

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {11[T]}]

Step with 10

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {11[T]}, {}]

Step with 9

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {11[T]}, {}, {}]

Covered

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {11[T]}, {9[T]}]

Backtrack

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {}, {10[T], 11[T]}]

Backtrack

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {13[T]}]

Step with 12

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {13[T]}, {}]

Backtrack

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {21[T]}, {12[T], 13[T]}]

Backtrack

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 21[T]}]

Step with 16

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 21[T]}, {16[T]}]

Covered

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 21[T]}]

Step with 17

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 21[T]}, {17[T]}]

Covered

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 17[T], 21[T]}]

Step with 18

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 17[T], 21[T]}, {18[T]}]

Covered

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 17[T], 18[T], 21[T]}]

Step with 19

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 17[T], 18[T], 21[T]}, {19[T]}]

Covered

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 17[T], 18[T], 19[T], 21[T]}]

Step with 20

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 17[T], 18[T], 19[T], 21[T]}, {20[T]}]

Covered

	Trace

	15[T], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T]}, {14[T], 16[T], 17[T], 18[T], 19[T], 20[T], 21[T]}]

Backtrack

	Trace

	15[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}]

Step with 17

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T]}]

Step with 18

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 18[(-1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ 16-n2-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0 /\ 16-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3) >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T]}, {18[T]}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T]}]

Step with 19

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 19[(16-n11-n31*n22*(-1+n5)-n22-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n31 >= 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ 16-n11-n31*n22*(-1+n5)-n31*n11*(-1+n5)-n11*(-1+n31)-(-1+n5)*n-(-1+n31)*n22-ni6^0 >= 0 /\ -1+n5 >= 0 /\ 16-n31*n22-n-n31*n11-ni6^0 >= 0 /\ 16-n31*n22-n31*n22*(-1+n5)-n31*n11*(-1+n5)-(-1+n5)*n-n-n31*n11-ni6^0 >= 0 /\ -1+n22 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T]}, {19[T]}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T]}]

Step with 20

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 20[(16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2*(-1+n10)*n3-ni6^0-n27 >= 0 /\ -1+n1 >= 0 /\ 16-(-1+n10)*n3*n1-(-1+n10)*n27-n2-n2*(-1+n10)*n3-n1-n2*(-1+n3)-ni6^0-n1*(-1+n3)-n27 >= 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T]}, {20[T]}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T]}]

Step with 21

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 21[(-1+n43 >= 0 /\ 16-n218-(-1+n43)*n218-(-1+n43)*n-ni6^0 >= 0 /\ -1+n218 >= 0 /\ -1+n >= 0 /\ 16-n218-(-1+n43)*n218-n-(-1+n43)*n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T]}, {21[T]}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}]

Step with 14

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {}]

Step with 12

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 12[(16-ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {}, {}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}]

Step with 13

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {}]

Step with 10

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {}, {}]

Step with 9

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T], 9[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {}, {}, {}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 10[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {}, {9[T]}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {10[T]}]

Step with 11

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {10[T]}, {}]

Step with 9

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T], 9[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {10[T]}, {}, {}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)], 11[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {10[T]}, {9[T]}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T], 13[(-15+ni6^0 <= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T]}, {10[T], 11[T]}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 14[T]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {17[T], 18[T], 19[T], 20[T], 21[T]}, {12[T], 13[T]}]

Backtrack

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {14[T], 17[T], 18[T], 19[T], 20[T], 21[T]}]

Step with 16

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)], 16[(-1+n >= 0 /\ 16-n-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {14[T], 17[T], 18[T], 19[T], 20[T], 21[T]}, {16[T]}]

Covered

	Trace

	15[T], 17[(-1+n2 >= 0 /\ 16-n2-ni6^0 >= 0)]
	
	Blocked

	[{}, {14[T], 16[T], 18[T], 19[T], 20[T], 21[T]}, {14[T], 16[T], 17[T], 18[T], 19[T], 20[T], 21[T]}]

Backtrack

	Trace

	15[T]
	
	Blocked

	[{}, {14[T], 16[T], 17[T], 18[T], 19[T], 20[T], 21[T]}]

Backtrack

	Trace

	Blocked

	[{15[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b