NO

Initial ITS

Start location: l9
Program variables: __const_5^0 __rho_1_^0 __rho_2_^0 c^0 curr_serv^0 resp^0 servers^0
   0: l0 -> l1 : __const_5^0'=__const_5^post1, __rho_1_^0'=__rho_1_^post1, __rho_2_^0'=__rho_2_^post1, c^0'=c^post1, curr_serv^0'=curr_serv^post1, resp^0'=resp^post1, servers^0'=servers^post1, (__rho_1_^0-__rho_1_^post1 == 0 /\ -c^post1+c^0 == 0 /\ resp^0-resp^post1 == 0 /\ curr_serv^0-curr_serv^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ -servers^post1+servers^0 == 0), cost: 1
   6: l1 -> l6 : __const_5^0'=__const_5^post7, __rho_1_^0'=__rho_1_^post7, __rho_2_^0'=__rho_2_^post7, c^0'=c^post7, curr_serv^0'=curr_serv^post7, resp^0'=resp^post7, servers^0'=servers^post7, (0 == 0 /\ curr_serv^0-curr_serv^post7 == 0 /\ 1-curr_serv^0 <= 0 /\ -c^post7+c^0 == 0 /\ -resp^post7+resp^0 == 0 /\ servers^0-servers^post7 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ -__rho_2_^post7+__rho_2_^0 == 0), cost: 1
   7: l1 -> l4 : __const_5^0'=__const_5^post8, __rho_1_^0'=__rho_1_^post8, __rho_2_^0'=__rho_2_^post8, c^0'=c^post8, curr_serv^0'=curr_serv^post8, resp^0'=resp^post8, servers^0'=servers^post8, (__const_5^0-__const_5^post8 == 0 /\ curr_serv^0 <= 0 /\ -resp^post8+resp^0 == 0 /\ -__rho_1_^post8+__rho_1_^0 == 0 /\ servers^0-servers^post8 == 0 /\ c^0-c^post8 == 0 /\ -curr_serv^post8+curr_serv^0 == 0 /\ -__rho_2_^post8+__rho_2_^0 == 0), cost: 1
   1: l2 -> l3 : __const_5^0'=__const_5^post2, __rho_1_^0'=__rho_1_^post2, __rho_2_^0'=__rho_2_^post2, c^0'=c^post2, curr_serv^0'=curr_serv^post2, resp^0'=resp^post2, servers^0'=servers^post2, (-resp^post2+resp^0 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ -c^post2+c^0 == 0 /\ -__rho_2_^post2+__rho_2_^0 == 0 /\ servers^0-servers^post2 == 0 /\ curr_serv^0-curr_serv^post2 == 0 /\ __rho_1_^0-__rho_1_^post2 == 0), cost: 1
   2: l4 -> l5 : __const_5^0'=__const_5^post3, __rho_1_^0'=__rho_1_^post3, __rho_2_^0'=__rho_2_^post3, c^0'=c^post3, curr_serv^0'=curr_serv^post3, resp^0'=resp^post3, servers^0'=servers^post3, (-resp^post3+resp^0 == 0 /\ servers^0-servers^post3 == 0 /\ curr_serv^0-curr_serv^post3 == 0 /\ c^0-c^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1
   3: l5 -> l4 : __const_5^0'=__const_5^post4, __rho_1_^0'=__rho_1_^post4, __rho_2_^0'=__rho_2_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, (c^0-c^post4 == 0 /\ -curr_serv^post4+curr_serv^0 == 0 /\ __const_5^0-__const_5^post4 == 0 /\ -__rho_2_^post4+__rho_2_^0 == 0 /\ servers^0-servers^post4 == 0 /\ -__rho_1_^post4+__rho_1_^0 == 0 /\ -resp^post4+resp^0 == 0), cost: 1
   4: l6 -> l0 : __const_5^0'=__const_5^post5, __rho_1_^0'=__rho_1_^post5, __rho_2_^0'=__rho_2_^post5, c^0'=c^post5, curr_serv^0'=curr_serv^post5, resp^0'=resp^post5, servers^0'=servers^post5, (__const_5^0-__const_5^post5 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ servers^0-servers^post5 == 0 /\ 1-curr_serv^0+curr_serv^post5 == 0 /\ __rho_1_^0 <= 0 /\ c^0-c^post5 == 0 /\ -__rho_1_^post5+__rho_1_^0 == 0 /\ 1-curr_serv^0+c^0 <= 0 /\ -resp^post5+resp^0 == 0), cost: 1
   5: l6 -> l0 : __const_5^0'=__const_5^post6, __rho_1_^0'=__rho_1_^post6, __rho_2_^0'=__rho_2_^post6, c^0'=c^post6, curr_serv^0'=curr_serv^post6, resp^0'=resp^post6, servers^0'=servers^post6, (1-curr_serv^0+curr_serv^post6 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ -1-resp^0+resp^post6 == 0 /\ 1-__rho_1_^0 <= 0 /\ -__rho_2_^post6+__rho_2_^0 == 0 /\ -__const_5^post6+__const_5^0 == 0 /\ -servers^post6+servers^0 == 0 /\ 1+c^post6-c^0 == 0), cost: 1
   8: l7 -> l4 : __const_5^0'=__const_5^post9, __rho_1_^0'=__rho_1_^post9, __rho_2_^0'=__rho_2_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, (-__rho_2_^post9+__rho_2_^0 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ curr_serv^0-curr_serv^post9 == 0 /\ 1-c^0+__const_5^0 <= 0 /\ c^0-c^post9 == 0 /\ -resp^post9+resp^0 == 0 /\ -servers^post9+servers^0 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0), cost: 1
   9: l7 -> l0 : __const_5^0'=__const_5^post10, __rho_1_^0'=__rho_1_^post10, __rho_2_^0'=__rho_2_^post10, c^0'=c^post10, curr_serv^0'=curr_serv^post10, resp^0'=resp^post10, servers^0'=servers^post10, (__rho_1_^0-__rho_1_^post10 == 0 /\ __rho_2_^0-__rho_2_^post10 == 0 /\ -c^post10+c^0 == 0 /\ -__const_5^post10+__const_5^0 == 0 /\ c^0-__const_5^0 <= 0 /\ -servers^post10+servers^0 == 0 /\ resp^0-resp^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0), cost: 1
  10: l8 -> l7 : __const_5^0'=__const_5^post11, __rho_1_^0'=__rho_1_^post11, __rho_2_^0'=__rho_2_^post11, c^0'=c^post11, curr_serv^0'=curr_serv^post11, resp^0'=resp^post11, servers^0'=servers^post11, (0 == 0 /\ resp^post11 == 0 /\ -4+servers^post11 == 0 /\ -servers^post11+curr_serv^post11 == 0 /\ -__const_5^post11+__const_5^0 == 0 /\ -__rho_2_^post11+c^post11 == 0 /\ __rho_1_^0-__rho_1_^post11 == 0 /\ 1-c^post11 <= 0), cost: 1
  11: l9 -> l8 : __const_5^0'=__const_5^post12, __rho_1_^0'=__rho_1_^post12, __rho_2_^0'=__rho_2_^post12, c^0'=c^post12, curr_serv^0'=curr_serv^post12, resp^0'=resp^post12, servers^0'=servers^post12, (servers^0-servers^post12 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ curr_serv^0-curr_serv^post12 == 0 /\ -c^post12+c^0 == 0 /\ -__const_5^post12+__const_5^0 == 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -resp^post12+resp^0 == 0), cost: 1

Chained Linear Paths

Start location: l9
Program variables: __const_5^0 __rho_1_^0 __rho_2_^0 c^0 curr_serv^0 resp^0 servers^0
   0: l0 -> l1 : __const_5^0'=__const_5^post1, __rho_1_^0'=__rho_1_^post1, __rho_2_^0'=__rho_2_^post1, c^0'=c^post1, curr_serv^0'=curr_serv^post1, resp^0'=resp^post1, servers^0'=servers^post1, (__rho_1_^0-__rho_1_^post1 == 0 /\ -c^post1+c^0 == 0 /\ resp^0-resp^post1 == 0 /\ curr_serv^0-curr_serv^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ -servers^post1+servers^0 == 0), cost: 1
   6: l1 -> l6 : __const_5^0'=__const_5^post7, __rho_1_^0'=__rho_1_^post7, __rho_2_^0'=__rho_2_^post7, c^0'=c^post7, curr_serv^0'=curr_serv^post7, resp^0'=resp^post7, servers^0'=servers^post7, (0 == 0 /\ curr_serv^0-curr_serv^post7 == 0 /\ 1-curr_serv^0 <= 0 /\ -c^post7+c^0 == 0 /\ -resp^post7+resp^0 == 0 /\ servers^0-servers^post7 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ -__rho_2_^post7+__rho_2_^0 == 0), cost: 1
   7: l1 -> l4 : __const_5^0'=__const_5^post8, __rho_1_^0'=__rho_1_^post8, __rho_2_^0'=__rho_2_^post8, c^0'=c^post8, curr_serv^0'=curr_serv^post8, resp^0'=resp^post8, servers^0'=servers^post8, (__const_5^0-__const_5^post8 == 0 /\ curr_serv^0 <= 0 /\ -resp^post8+resp^0 == 0 /\ -__rho_1_^post8+__rho_1_^0 == 0 /\ servers^0-servers^post8 == 0 /\ c^0-c^post8 == 0 /\ -curr_serv^post8+curr_serv^0 == 0 /\ -__rho_2_^post8+__rho_2_^0 == 0), cost: 1
   1: l2 -> l3 : __const_5^0'=__const_5^post2, __rho_1_^0'=__rho_1_^post2, __rho_2_^0'=__rho_2_^post2, c^0'=c^post2, curr_serv^0'=curr_serv^post2, resp^0'=resp^post2, servers^0'=servers^post2, (-resp^post2+resp^0 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ -c^post2+c^0 == 0 /\ -__rho_2_^post2+__rho_2_^0 == 0 /\ servers^0-servers^post2 == 0 /\ curr_serv^0-curr_serv^post2 == 0 /\ __rho_1_^0-__rho_1_^post2 == 0), cost: 1
  13: l4 -> l4 : __const_5^0'=__const_5^post4, __rho_1_^0'=__rho_1_^post4, __rho_2_^0'=__rho_2_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, (-resp^post3+resp^0 == 0 /\ servers^0-servers^post3 == 0 /\ c^post3-c^post4 == 0 /\ curr_serv^0-curr_serv^post3 == 0 /\ c^0-c^post3 == 0 /\ __const_5^post3-__const_5^post4 == 0 /\ resp^post3-resp^post4 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -__rho_1_^post4+__rho_1_^post3 == 0 /\ __rho_2_^post3-__rho_2_^post4 == 0 /\ -curr_serv^post4+curr_serv^post3 == 0 /\ servers^post3-servers^post4 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1
   4: l6 -> l0 : __const_5^0'=__const_5^post5, __rho_1_^0'=__rho_1_^post5, __rho_2_^0'=__rho_2_^post5, c^0'=c^post5, curr_serv^0'=curr_serv^post5, resp^0'=resp^post5, servers^0'=servers^post5, (__const_5^0-__const_5^post5 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ servers^0-servers^post5 == 0 /\ 1-curr_serv^0+curr_serv^post5 == 0 /\ __rho_1_^0 <= 0 /\ c^0-c^post5 == 0 /\ -__rho_1_^post5+__rho_1_^0 == 0 /\ 1-curr_serv^0+c^0 <= 0 /\ -resp^post5+resp^0 == 0), cost: 1
   5: l6 -> l0 : __const_5^0'=__const_5^post6, __rho_1_^0'=__rho_1_^post6, __rho_2_^0'=__rho_2_^post6, c^0'=c^post6, curr_serv^0'=curr_serv^post6, resp^0'=resp^post6, servers^0'=servers^post6, (1-curr_serv^0+curr_serv^post6 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ -1-resp^0+resp^post6 == 0 /\ 1-__rho_1_^0 <= 0 /\ -__rho_2_^post6+__rho_2_^0 == 0 /\ -__const_5^post6+__const_5^0 == 0 /\ -servers^post6+servers^0 == 0 /\ 1+c^post6-c^0 == 0), cost: 1
   8: l7 -> l4 : __const_5^0'=__const_5^post9, __rho_1_^0'=__rho_1_^post9, __rho_2_^0'=__rho_2_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, (-__rho_2_^post9+__rho_2_^0 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ curr_serv^0-curr_serv^post9 == 0 /\ 1-c^0+__const_5^0 <= 0 /\ c^0-c^post9 == 0 /\ -resp^post9+resp^0 == 0 /\ -servers^post9+servers^0 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0), cost: 1
   9: l7 -> l0 : __const_5^0'=__const_5^post10, __rho_1_^0'=__rho_1_^post10, __rho_2_^0'=__rho_2_^post10, c^0'=c^post10, curr_serv^0'=curr_serv^post10, resp^0'=resp^post10, servers^0'=servers^post10, (__rho_1_^0-__rho_1_^post10 == 0 /\ __rho_2_^0-__rho_2_^post10 == 0 /\ -c^post10+c^0 == 0 /\ -__const_5^post10+__const_5^0 == 0 /\ c^0-__const_5^0 <= 0 /\ -servers^post10+servers^0 == 0 /\ resp^0-resp^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0), cost: 1
  12: l9 -> l7 : __const_5^0'=__const_5^post11, __rho_1_^0'=__rho_1_^post11, __rho_2_^0'=__rho_2_^post11, c^0'=c^post11, curr_serv^0'=curr_serv^post11, resp^0'=resp^post11, servers^0'=servers^post11, (0 == 0 /\ resp^post11 == 0 /\ -4+servers^post11 == 0 /\ servers^0-servers^post12 == 0 /\ -servers^post11+curr_serv^post11 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ curr_serv^0-curr_serv^post12 == 0 /\ -__const_5^post11+__const_5^post12 == 0 /\ -__rho_2_^post11+c^post11 == 0 /\ -__rho_1_^post11+__rho_1_^post12 == 0 /\ -c^post12+c^0 == 0 /\ -__const_5^post12+__const_5^0 == 0 /\ 1-c^post11 <= 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -resp^post12+resp^0 == 0), cost: 1

	Eliminating location l8 by chaining:

	Applied chaining

	First rule:
	l9 -> l8 : __const_5^0'=__const_5^post12, __rho_1_^0'=__rho_1_^post12, __rho_2_^0'=__rho_2_^post12, c^0'=c^post12, curr_serv^0'=curr_serv^post12, resp^0'=resp^post12, servers^0'=servers^post12, (servers^0-servers^post12 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ curr_serv^0-curr_serv^post12 == 0 /\ -c^post12+c^0 == 0 /\ -__const_5^post12+__const_5^0 == 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -resp^post12+resp^0 == 0), cost: 1
	Second rule:
	l8 -> l7 : __const_5^0'=__const_5^post11, __rho_1_^0'=__rho_1_^post11, __rho_2_^0'=__rho_2_^post11, c^0'=c^post11, curr_serv^0'=curr_serv^post11, resp^0'=resp^post11, servers^0'=servers^post11, (0 == 0 /\ resp^post11 == 0 /\ -4+servers^post11 == 0 /\ -servers^post11+curr_serv^post11 == 0 /\ -__const_5^post11+__const_5^0 == 0 /\ -__rho_2_^post11+c^post11 == 0 /\ __rho_1_^0-__rho_1_^post11 == 0 /\ 1-c^post11 <= 0), cost: 1
	New rule:
	l9 -> l7 : __const_5^0'=__const_5^post11, __rho_1_^0'=__rho_1_^post11, __rho_2_^0'=__rho_2_^post11, c^0'=c^post11, curr_serv^0'=curr_serv^post11, resp^0'=resp^post11, servers^0'=servers^post11, (0 == 0 /\ resp^post11 == 0 /\ -4+servers^post11 == 0 /\ servers^0-servers^post12 == 0 /\ -servers^post11+curr_serv^post11 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ curr_serv^0-curr_serv^post12 == 0 /\ -__const_5^post11+__const_5^post12 == 0 /\ -__rho_2_^post11+c^post11 == 0 /\ -__rho_1_^post11+__rho_1_^post12 == 0 /\ -c^post12+c^0 == 0 /\ -__const_5^post12+__const_5^0 == 0 /\ 1-c^post11 <= 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -resp^post12+resp^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 10 11
	
	Eliminating location l5 by chaining:

	Applied chaining

	First rule:
	l4 -> l5 : __const_5^0'=__const_5^post3, __rho_1_^0'=__rho_1_^post3, __rho_2_^0'=__rho_2_^post3, c^0'=c^post3, curr_serv^0'=curr_serv^post3, resp^0'=resp^post3, servers^0'=servers^post3, (-resp^post3+resp^0 == 0 /\ servers^0-servers^post3 == 0 /\ curr_serv^0-curr_serv^post3 == 0 /\ c^0-c^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1
	Second rule:
	l5 -> l4 : __const_5^0'=__const_5^post4, __rho_1_^0'=__rho_1_^post4, __rho_2_^0'=__rho_2_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, (c^0-c^post4 == 0 /\ -curr_serv^post4+curr_serv^0 == 0 /\ __const_5^0-__const_5^post4 == 0 /\ -__rho_2_^post4+__rho_2_^0 == 0 /\ servers^0-servers^post4 == 0 /\ -__rho_1_^post4+__rho_1_^0 == 0 /\ -resp^post4+resp^0 == 0), cost: 1
	New rule:
	l4 -> l4 : __const_5^0'=__const_5^post4, __rho_1_^0'=__rho_1_^post4, __rho_2_^0'=__rho_2_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, (-resp^post3+resp^0 == 0 /\ servers^0-servers^post3 == 0 /\ c^post3-c^post4 == 0 /\ curr_serv^0-curr_serv^post3 == 0 /\ c^0-c^post3 == 0 /\ __const_5^post3-__const_5^post4 == 0 /\ resp^post3-resp^post4 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -__rho_1_^post4+__rho_1_^post3 == 0 /\ __rho_2_^post3-__rho_2_^post4 == 0 /\ -curr_serv^post4+curr_serv^post3 == 0 /\ servers^post3-servers^post4 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 2 3

Simplified Transitions

Start location: l9
Program variables: __const_5^0 __rho_1_^0 __rho_2_^0 c^0 curr_serv^0 resp^0 servers^0
  14: l0 -> l1 : T, cost: 1
  18: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1
  19: l1 -> l4 : curr_serv^0 <= 0, cost: 1
  15: l2 -> l3 : T, cost: 1
  23: l4 -> l4 : T, cost: 1
  16: l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (__rho_1_^0 <= 0 /\ 1-curr_serv^0+c^0 <= 0), cost: 1
  17: l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1
  20: l7 -> l4 : 1-c^0+__const_5^0 <= 0, cost: 1
  21: l7 -> l0 : c^0-__const_5^0 <= 0, cost: 1
  22: l9 -> l7 : __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, 1-c^post11 <= 0, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : __const_5^0'=__const_5^post1, __rho_1_^0'=__rho_1_^post1, __rho_2_^0'=__rho_2_^post1, c^0'=c^post1, curr_serv^0'=curr_serv^post1, resp^0'=resp^post1, servers^0'=servers^post1, (__rho_1_^0-__rho_1_^post1 == 0 /\ -c^post1+c^0 == 0 /\ resp^0-resp^post1 == 0 /\ curr_serv^0-curr_serv^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ -servers^post1+servers^0 == 0), cost: 1
	New rule:
	l0 -> l1 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 0 == 0, cost: 1
	
		propagated equality __rho_1_^post1 = __rho_1_^0
		
		propagated equality c^post1 = c^0
		
		propagated equality resp^post1 = resp^0
		
		propagated equality curr_serv^post1 = curr_serv^0
		
		propagated equality __rho_2_^post1 = __rho_2_^0
		
		propagated equality __const_5^post1 = __const_5^0
		
		propagated equality servers^post1 = servers^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 0 == 0, cost: 1
	New rule:
	l0 -> l1 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, T, cost: 1
	New rule:
	l0 -> l1 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l3 : __const_5^0'=__const_5^post2, __rho_1_^0'=__rho_1_^post2, __rho_2_^0'=__rho_2_^post2, c^0'=c^post2, curr_serv^0'=curr_serv^post2, resp^0'=resp^post2, servers^0'=servers^post2, (-resp^post2+resp^0 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ -c^post2+c^0 == 0 /\ -__rho_2_^post2+__rho_2_^0 == 0 /\ servers^0-servers^post2 == 0 /\ curr_serv^0-curr_serv^post2 == 0 /\ __rho_1_^0-__rho_1_^post2 == 0), cost: 1
	New rule:
	l2 -> l3 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 0 == 0, cost: 1
	
		propagated equality resp^post2 = resp^0
		
		propagated equality __const_5^post2 = __const_5^0
		
		propagated equality c^post2 = c^0
		
		propagated equality __rho_2_^post2 = __rho_2_^0
		
		propagated equality servers^post2 = servers^0
		
		propagated equality curr_serv^post2 = curr_serv^0
		
		propagated equality __rho_1_^post2 = __rho_1_^0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 0 == 0, cost: 1
	New rule:
	l2 -> l3 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, T, cost: 1
	New rule:
	l2 -> l3 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l0 : __const_5^0'=__const_5^post5, __rho_1_^0'=__rho_1_^post5, __rho_2_^0'=__rho_2_^post5, c^0'=c^post5, curr_serv^0'=curr_serv^post5, resp^0'=resp^post5, servers^0'=servers^post5, (__const_5^0-__const_5^post5 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ servers^0-servers^post5 == 0 /\ 1-curr_serv^0+curr_serv^post5 == 0 /\ __rho_1_^0 <= 0 /\ c^0-c^post5 == 0 /\ -__rho_1_^post5+__rho_1_^0 == 0 /\ 1-curr_serv^0+c^0 <= 0 /\ -resp^post5+resp^0 == 0), cost: 1
	New rule:
	l6 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ __rho_1_^0 <= 0 /\ 1-curr_serv^0+c^0 <= 0), cost: 1
	
		propagated equality __const_5^post5 = __const_5^0
		
		propagated equality __rho_2_^post5 = __rho_2_^0
		
		propagated equality servers^post5 = servers^0
		
		propagated equality curr_serv^post5 = -1+curr_serv^0
		
		propagated equality c^post5 = c^0
		
		propagated equality __rho_1_^post5 = __rho_1_^0
		
		propagated equality resp^post5 = resp^0
		
	Simplified Guard

	Original rule:
	l6 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ __rho_1_^0 <= 0 /\ 1-curr_serv^0+c^0 <= 0), cost: 1
	New rule:
	l6 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (__rho_1_^0 <= 0 /\ 1-curr_serv^0+c^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (__rho_1_^0 <= 0 /\ 1-curr_serv^0+c^0 <= 0), cost: 1
	New rule:
	l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (__rho_1_^0 <= 0 /\ 1-curr_serv^0+c^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l0 : __const_5^0'=__const_5^post6, __rho_1_^0'=__rho_1_^post6, __rho_2_^0'=__rho_2_^post6, c^0'=c^post6, curr_serv^0'=curr_serv^post6, resp^0'=resp^post6, servers^0'=servers^post6, (1-curr_serv^0+curr_serv^post6 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ -1-resp^0+resp^post6 == 0 /\ 1-__rho_1_^0 <= 0 /\ -__rho_2_^post6+__rho_2_^0 == 0 /\ -__const_5^post6+__const_5^0 == 0 /\ -servers^post6+servers^0 == 0 /\ 1+c^post6-c^0 == 0), cost: 1
	New rule:
	l6 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, servers^0'=servers^0, (0 == 0 /\ 1-__rho_1_^0 <= 0), cost: 1
	
		propagated equality curr_serv^post6 = -1+curr_serv^0
		
		propagated equality __rho_1_^post6 = __rho_1_^0
		
		propagated equality resp^post6 = 1+resp^0
		
		propagated equality __rho_2_^post6 = __rho_2_^0
		
		propagated equality __const_5^post6 = __const_5^0
		
		propagated equality servers^post6 = servers^0
		
		propagated equality c^post6 = -1+c^0
		
	Simplified Guard

	Original rule:
	l6 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, servers^0'=servers^0, (0 == 0 /\ 1-__rho_1_^0 <= 0), cost: 1
	New rule:
	l6 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, servers^0'=servers^0, 1-__rho_1_^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, servers^0'=servers^0, 1-__rho_1_^0 <= 0, cost: 1
	New rule:
	l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l6 : __const_5^0'=__const_5^post7, __rho_1_^0'=__rho_1_^post7, __rho_2_^0'=__rho_2_^post7, c^0'=c^post7, curr_serv^0'=curr_serv^post7, resp^0'=resp^post7, servers^0'=servers^post7, (0 == 0 /\ curr_serv^0-curr_serv^post7 == 0 /\ 1-curr_serv^0 <= 0 /\ -c^post7+c^0 == 0 /\ -resp^post7+resp^0 == 0 /\ servers^0-servers^post7 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ -__rho_2_^post7+__rho_2_^0 == 0), cost: 1
	New rule:
	l1 -> l6 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^post7, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ 1-curr_serv^0 <= 0), cost: 1
	
		propagated equality curr_serv^post7 = curr_serv^0
		
		propagated equality c^post7 = c^0
		
		propagated equality resp^post7 = resp^0
		
		propagated equality servers^post7 = servers^0
		
		propagated equality __const_5^post7 = __const_5^0
		
		propagated equality __rho_2_^post7 = __rho_2_^0
		
	Simplified Guard

	Original rule:
	l1 -> l6 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^post7, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ 1-curr_serv^0 <= 0), cost: 1
	New rule:
	l1 -> l6 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^post7, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 1-curr_serv^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l6 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^post7, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 1-curr_serv^0 <= 0, cost: 1
	New rule:
	l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l4 : __const_5^0'=__const_5^post8, __rho_1_^0'=__rho_1_^post8, __rho_2_^0'=__rho_2_^post8, c^0'=c^post8, curr_serv^0'=curr_serv^post8, resp^0'=resp^post8, servers^0'=servers^post8, (__const_5^0-__const_5^post8 == 0 /\ curr_serv^0 <= 0 /\ -resp^post8+resp^0 == 0 /\ -__rho_1_^post8+__rho_1_^0 == 0 /\ servers^0-servers^post8 == 0 /\ c^0-c^post8 == 0 /\ -curr_serv^post8+curr_serv^0 == 0 /\ -__rho_2_^post8+__rho_2_^0 == 0), cost: 1
	New rule:
	l1 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ curr_serv^0 <= 0), cost: 1
	
		propagated equality __const_5^post8 = __const_5^0
		
		propagated equality resp^post8 = resp^0
		
		propagated equality __rho_1_^post8 = __rho_1_^0
		
		propagated equality servers^post8 = servers^0
		
		propagated equality c^post8 = c^0
		
		propagated equality curr_serv^post8 = curr_serv^0
		
		propagated equality __rho_2_^post8 = __rho_2_^0
		
	Simplified Guard

	Original rule:
	l1 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ curr_serv^0 <= 0), cost: 1
	New rule:
	l1 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, curr_serv^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, curr_serv^0 <= 0, cost: 1
	New rule:
	l1 -> l4 : curr_serv^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l4 : __const_5^0'=__const_5^post9, __rho_1_^0'=__rho_1_^post9, __rho_2_^0'=__rho_2_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, (-__rho_2_^post9+__rho_2_^0 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ curr_serv^0-curr_serv^post9 == 0 /\ 1-c^0+__const_5^0 <= 0 /\ c^0-c^post9 == 0 /\ -resp^post9+resp^0 == 0 /\ -servers^post9+servers^0 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0), cost: 1
	New rule:
	l7 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ 1-c^0+__const_5^0 <= 0), cost: 1
	
		propagated equality __rho_2_^post9 = __rho_2_^0
		
		propagated equality __const_5^post9 = __const_5^0
		
		propagated equality curr_serv^post9 = curr_serv^0
		
		propagated equality c^post9 = c^0
		
		propagated equality resp^post9 = resp^0
		
		propagated equality servers^post9 = servers^0
		
		propagated equality __rho_1_^post9 = __rho_1_^0
		
	Simplified Guard

	Original rule:
	l7 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ 1-c^0+__const_5^0 <= 0), cost: 1
	New rule:
	l7 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 1-c^0+__const_5^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 1-c^0+__const_5^0 <= 0, cost: 1
	New rule:
	l7 -> l4 : 1-c^0+__const_5^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l0 : __const_5^0'=__const_5^post10, __rho_1_^0'=__rho_1_^post10, __rho_2_^0'=__rho_2_^post10, c^0'=c^post10, curr_serv^0'=curr_serv^post10, resp^0'=resp^post10, servers^0'=servers^post10, (__rho_1_^0-__rho_1_^post10 == 0 /\ __rho_2_^0-__rho_2_^post10 == 0 /\ -c^post10+c^0 == 0 /\ -__const_5^post10+__const_5^0 == 0 /\ c^0-__const_5^0 <= 0 /\ -servers^post10+servers^0 == 0 /\ resp^0-resp^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0), cost: 1
	New rule:
	l7 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ c^0-__const_5^0 <= 0), cost: 1
	
		propagated equality __rho_1_^post10 = __rho_1_^0
		
		propagated equality __rho_2_^post10 = __rho_2_^0
		
		propagated equality c^post10 = c^0
		
		propagated equality __const_5^post10 = __const_5^0
		
		propagated equality servers^post10 = servers^0
		
		propagated equality resp^post10 = resp^0
		
		propagated equality curr_serv^post10 = curr_serv^0
		
	Simplified Guard

	Original rule:
	l7 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, (0 == 0 /\ c^0-__const_5^0 <= 0), cost: 1
	New rule:
	l7 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, c^0-__const_5^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l0 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, c^0-__const_5^0 <= 0, cost: 1
	New rule:
	l7 -> l0 : c^0-__const_5^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l7 : __const_5^0'=__const_5^post11, __rho_1_^0'=__rho_1_^post11, __rho_2_^0'=__rho_2_^post11, c^0'=c^post11, curr_serv^0'=curr_serv^post11, resp^0'=resp^post11, servers^0'=servers^post11, (0 == 0 /\ resp^post11 == 0 /\ -4+servers^post11 == 0 /\ servers^0-servers^post12 == 0 /\ -servers^post11+curr_serv^post11 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ curr_serv^0-curr_serv^post12 == 0 /\ -__const_5^post11+__const_5^post12 == 0 /\ -__rho_2_^post11+c^post11 == 0 /\ -__rho_1_^post11+__rho_1_^post12 == 0 /\ -c^post12+c^0 == 0 /\ -__const_5^post12+__const_5^0 == 0 /\ 1-c^post11 <= 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -resp^post12+resp^0 == 0), cost: 1
	New rule:
	l9 -> l7 : __const_5^0'=__const_5^post12, __rho_1_^0'=__rho_1_^post12, __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, (0 == 0 /\ servers^0-servers^post12 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ curr_serv^0-curr_serv^post12 == 0 /\ -c^post12+c^0 == 0 /\ -__const_5^post12+__const_5^0 == 0 /\ 1-c^post11 <= 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -resp^post12+resp^0 == 0), cost: 1
	
		propagated equality resp^post11 = 0
		
		propagated equality servers^post11 = 4
		
		propagated equality curr_serv^post11 = 4
		
		propagated equality __const_5^post11 = __const_5^post12
		
		propagated equality __rho_2_^post11 = c^post11
		
		propagated equality __rho_1_^post11 = __rho_1_^post12
		
	Propagated Equalities

	Original rule:
	l9 -> l7 : __const_5^0'=__const_5^post12, __rho_1_^0'=__rho_1_^post12, __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, (0 == 0 /\ servers^0-servers^post12 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ curr_serv^0-curr_serv^post12 == 0 /\ -c^post12+c^0 == 0 /\ -__const_5^post12+__const_5^0 == 0 /\ 1-c^post11 <= 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -resp^post12+resp^0 == 0), cost: 1
	New rule:
	l9 -> l7 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, (0 == 0 /\ 1-c^post11 <= 0), cost: 1
	
		propagated equality servers^post12 = servers^0
		
		propagated equality __rho_2_^post12 = __rho_2_^0
		
		propagated equality curr_serv^post12 = curr_serv^0
		
		propagated equality c^post12 = c^0
		
		propagated equality __const_5^post12 = __const_5^0
		
		propagated equality __rho_1_^post12 = __rho_1_^0
		
		propagated equality resp^post12 = resp^0
		
	Simplified Guard

	Original rule:
	l9 -> l7 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, (0 == 0 /\ 1-c^post11 <= 0), cost: 1
	New rule:
	l9 -> l7 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, 1-c^post11 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l9 -> l7 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, 1-c^post11 <= 0, cost: 1
	New rule:
	l9 -> l7 : __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, 1-c^post11 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l4 : __const_5^0'=__const_5^post4, __rho_1_^0'=__rho_1_^post4, __rho_2_^0'=__rho_2_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, (-resp^post3+resp^0 == 0 /\ servers^0-servers^post3 == 0 /\ c^post3-c^post4 == 0 /\ curr_serv^0-curr_serv^post3 == 0 /\ c^0-c^post3 == 0 /\ __const_5^post3-__const_5^post4 == 0 /\ resp^post3-resp^post4 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -__rho_1_^post4+__rho_1_^post3 == 0 /\ __rho_2_^post3-__rho_2_^post4 == 0 /\ -curr_serv^post4+curr_serv^post3 == 0 /\ servers^post3-servers^post4 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1
	New rule:
	l4 -> l4 : __const_5^0'=__const_5^post3, __rho_1_^0'=__rho_1_^post3, __rho_2_^0'=__rho_2_^post3, c^0'=c^post3, curr_serv^0'=curr_serv^post3, resp^0'=resp^post3, servers^0'=servers^post3, (0 == 0 /\ -resp^post3+resp^0 == 0 /\ servers^0-servers^post3 == 0 /\ curr_serv^0-curr_serv^post3 == 0 /\ c^0-c^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1
	
		propagated equality c^post4 = c^post3
		
		propagated equality __const_5^post4 = __const_5^post3
		
		propagated equality resp^post4 = resp^post3
		
		propagated equality __rho_1_^post4 = __rho_1_^post3
		
		propagated equality __rho_2_^post4 = __rho_2_^post3
		
		propagated equality curr_serv^post4 = curr_serv^post3
		
		propagated equality servers^post4 = servers^post3
		
	Propagated Equalities

	Original rule:
	l4 -> l4 : __const_5^0'=__const_5^post3, __rho_1_^0'=__rho_1_^post3, __rho_2_^0'=__rho_2_^post3, c^0'=c^post3, curr_serv^0'=curr_serv^post3, resp^0'=resp^post3, servers^0'=servers^post3, (0 == 0 /\ -resp^post3+resp^0 == 0 /\ servers^0-servers^post3 == 0 /\ curr_serv^0-curr_serv^post3 == 0 /\ c^0-c^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1
	New rule:
	l4 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 0 == 0, cost: 1
	
		propagated equality resp^post3 = resp^0
		
		propagated equality servers^post3 = servers^0
		
		propagated equality curr_serv^post3 = curr_serv^0
		
		propagated equality c^post3 = c^0
		
		propagated equality __rho_1_^post3 = __rho_1_^0
		
		propagated equality __rho_2_^post3 = __rho_2_^0
		
		propagated equality __const_5^post3 = __const_5^0
		
	Simplified Guard

	Original rule:
	l4 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, 0 == 0, cost: 1
	New rule:
	l4 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l4 : __const_5^0'=__const_5^0, __rho_1_^0'=__rho_1_^0, __rho_2_^0'=__rho_2_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, T, cost: 1
	New rule:
	l4 -> l4 : T, cost: 1

Step with 22

	Trace

	22[(1-c^post11 <= 0)]
	
	Blocked

	[{}, {}]

Step with 20

	Trace

	22[(1-c^post11 <= 0)], 20[(1-c^0+__const_5^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Step with 23

	Trace

	22[(1-c^post11 <= 0)], 20[(1-c^0+__const_5^0 <= 0)], 23[T]
	
	Blocked

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

Nonterm

Start location: l9
Program variables: __const_5^0 __rho_1_^0 __rho_2_^0 c^0 curr_serv^0 resp^0 servers^0
  14: l0 -> l1 : T, cost: 1
  18: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1
  19: l1 -> l4 : curr_serv^0 <= 0, cost: 1
  15: l2 -> l3 : T, cost: 1
  23: l4 -> l4 : T, cost: 1
  24: l4 -> LoAT_sink : -1+n >= 0, cost: NONTERM
  16: l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (__rho_1_^0 <= 0 /\ 1-curr_serv^0+c^0 <= 0), cost: 1
  17: l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1
  20: l7 -> l4 : 1-c^0+__const_5^0 <= 0, cost: 1
  21: l7 -> l0 : c^0-__const_5^0 <= 0, cost: 1
  22: l9 -> l7 : __rho_2_^0'=c^post11, c^0'=c^post11, curr_serv^0'=4, resp^0'=0, servers^0'=4, 1-c^post11 <= 0, cost: 1

	Certificate of Non-Termination

	Original rule:
	l4 -> l4 : T, cost: 1
	New rule:
	l4 -> LoAT_sink : -1+n >= 0, cost: NONTERM

		Replacement map: {}

Step with 24

	Trace

	22[(1-c^post11 <= 0)], 20[(1-c^0+__const_5^0 <= 0)], 24[-1+n >= 0]
	
	Blocked

	[{}, {}, {}, {24[T]}]

Refute

	Counterexample

	[ __const_5^0=0 __rho_1_^0=0 __rho_2_^0=1 c^0=1 curr_serv^0=4 resp^0=0 servers^0=4 ] 22 [ __const_5^0=0 __rho_1_^0=0 __rho_2_^0=1 c^0=1 curr_serv^0=4 resp^0=0 servers^0=4 ] 20 [ __const_5^0=0 __rho_1_^0=0 __rho_2_^0=__rho_2_^0 c^0=c^0 curr_serv^0=curr_serv^0 resp^0=resp^0 servers^0=servers^0 ] 24
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b