unknown

Initial ITS

Start location: l12
Program variables: i^0 j^0 y4^0 y6^0 y8^0
   0: l0 -> l1 : i^0'=i^post1, j^0'=j^post1, y4^0'=y4^post1, y6^0'=y6^post1, y8^0'=y8^post1, (y8^0-y8^post1 == 0 /\ -i^post1+i^0 == 0 /\ -y6^post1+y6^0 == 0 /\ j^0-j^post1 == 0 /\ -y4^post1+y4^0 == 0), cost: 1
  11: l1 -> l10 : i^0'=i^post12, j^0'=j^post12, y4^0'=y4^post12, y6^0'=y6^post12, y8^0'=y8^post12, (-y4^post12+y4^0 == 0 /\ -i^post12+i^0 == 0 /\ y8^0-y8^post12 == 0 /\ j^0-j^post12 == 0 /\ y6^post12-i^0 == 0), cost: 1
   1: l2 -> l3 : i^0'=i^post2, j^0'=j^post2, y4^0'=y4^post2, y6^0'=y6^post2, y8^0'=y8^post2, (y8^0-y8^post2 == 0 /\ -100+j^post2 == 0 /\ y6^0-y6^post2 == 0 /\ 100-i^0 <= 0 /\ -y4^post2+y4^0 == 0 /\ i^0-i^post2 == 0), cost: 1
   2: l2 -> l0 : i^0'=i^post3, j^0'=j^post3, y4^0'=y4^post3, y6^0'=y6^post3, y8^0'=y8^post3, (-99+i^0 <= 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
   8: l3 -> l7 : i^0'=i^post9, j^0'=j^post9, y4^0'=y4^post9, y6^0'=y6^post9, y8^0'=y8^post9, (-y4^post9+y4^0 == 0 /\ -i^post9+i^0 == 0 /\ y8^0-y8^post9 == 0 /\ -y6^post9+y6^0 == 0 /\ j^0-j^post9 == 0), cost: 1
   3: l4 -> l3 : i^0'=i^post4, j^0'=j^post4, y4^0'=y4^post4, y6^0'=y6^post4, y8^0'=y8^post4, (y8^0-y8^post4 == 0 /\ y6^0-y6^post4 == 0 /\ -y4^post4+y4^0 == 0 /\ i^0-i^post4 == 0 /\ -1+j^post4-j^0 == 0), cost: 1
   4: l5 -> l2 : i^0'=i^post5, j^0'=j^post5, y4^0'=y4^post5, y6^0'=y6^post5, y8^0'=y8^post5, (y8^0-y8^post5 == 0 /\ j^0-j^post5 == 0 /\ -i^post5+i^0 == 0 /\ -y4^post5+y4^0 == 0 /\ -y6^post5+y6^0 == 0), cost: 1
   5: l6 -> l4 : i^0'=i^post6, j^0'=j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (y6^0-y6^post6 == 0 /\ -y8^post6+y8^0 == 0 /\ i^0-i^post6 == 0 /\ -y4^post6+y4^0 == 0 /\ -j^post6+j^0 == 0), cost: 1
   6: l7 -> l8 : i^0'=i^post7, j^0'=j^post7, y4^0'=y4^post7, y6^0'=y6^post7, y8^0'=y8^post7, (j^0-j^post7 == 0 /\ y4^0-y4^post7 == 0 /\ -i^post7+i^0 == 0 /\ -y6^post7+y6^0 == 0 /\ y8^0-y8^post7 == 0 /\ 200-j^0 <= 0), cost: 1
   7: l7 -> l6 : i^0'=i^post8, j^0'=j^post8, y4^0'=y4^post8, y6^0'=y6^post8, y8^0'=y8^post8, (-199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y6^0-y6^post8 == 0 /\ j^0-j^post8 == 0), cost: 1
   9: l9 -> l5 : i^0'=i^post10, j^0'=j^post10, y4^0'=y4^post10, y6^0'=y6^post10, y8^0'=y8^post10, (-y4^post10+y4^0 == 0 /\ -y6^post10+y6^0 == 0 /\ y8^0-y8^post10 == 0 /\ j^0-j^post10 == 0 /\ -1+i^post10-i^0 == 0), cost: 1
  10: l10 -> l9 : i^0'=i^post11, j^0'=j^post11, y4^0'=y4^post11, y6^0'=y6^post11, y8^0'=y8^post11, (i^0-i^post11 == 0 /\ y8^0-y8^post11 == 0 /\ -y4^post11+y4^0 == 0 /\ -j^post11+j^0 == 0 /\ y6^0-y6^post11 == 0), cost: 1
  12: l11 -> l5 : i^0'=i^post13, j^0'=j^post13, y4^0'=y4^post13, y6^0'=y6^post13, y8^0'=y8^post13, (i^post13 == 0 /\ -y4^post13+y4^0 == 0 /\ y8^0-y8^post13 == 0 /\ y6^0-y6^post13 == 0 /\ j^0-j^post13 == 0), cost: 1
  13: l12 -> l11 : i^0'=i^post14, j^0'=j^post14, y4^0'=y4^post14, y6^0'=y6^post14, y8^0'=y8^post14, (y8^0-y8^post14 == 0 /\ -i^post14+i^0 == 0 /\ y6^0-y6^post14 == 0 /\ -y4^post14+y4^0 == 0 /\ -j^post14+j^0 == 0), cost: 1

Chained Linear Paths

Start location: l12
Program variables: i^0 j^0 y4^0 y6^0 y8^0
   1: l2 -> l3 : i^0'=i^post2, j^0'=j^post2, y4^0'=y4^post2, y6^0'=y6^post2, y8^0'=y8^post2, (y8^0-y8^post2 == 0 /\ -100+j^post2 == 0 /\ y6^0-y6^post2 == 0 /\ 100-i^0 <= 0 /\ -y4^post2+y4^0 == 0 /\ i^0-i^post2 == 0), cost: 1
  18: l2 -> l5 : i^0'=i^post10, j^0'=j^post10, y4^0'=y4^post10, y6^0'=y6^post10, y8^0'=y8^post10, (-1+i^post10-i^post11 == 0 /\ -99+i^0 <= 0 /\ y8^post11-y8^post10 == 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ y4^post11-y4^post10 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ y6^post12-y6^post11 == 0 /\ i^post12-i^post11 == 0 /\ -y8^post11+y8^post12 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ -j^post11+j^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ j^post11-j^post10 == 0 /\ y4^post12-y4^post11 == 0 /\ -y4^post1+y4^post3 == 0 /\ -y6^post10+y6^post11 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
   8: l3 -> l7 : i^0'=i^post9, j^0'=j^post9, y4^0'=y4^post9, y6^0'=y6^post9, y8^0'=y8^post9, (-y4^post9+y4^0 == 0 /\ -i^post9+i^0 == 0 /\ y8^0-y8^post9 == 0 /\ -y6^post9+y6^0 == 0 /\ j^0-j^post9 == 0), cost: 1
   4: l5 -> l2 : i^0'=i^post5, j^0'=j^post5, y4^0'=y4^post5, y6^0'=y6^post5, y8^0'=y8^post5, (y8^0-y8^post5 == 0 /\ j^0-j^post5 == 0 /\ -i^post5+i^0 == 0 /\ -y4^post5+y4^0 == 0 /\ -y6^post5+y6^0 == 0), cost: 1
   6: l7 -> l8 : i^0'=i^post7, j^0'=j^post7, y4^0'=y4^post7, y6^0'=y6^post7, y8^0'=y8^post7, (j^0-j^post7 == 0 /\ y4^0-y4^post7 == 0 /\ -i^post7+i^0 == 0 /\ -y6^post7+y6^0 == 0 /\ y8^0-y8^post7 == 0 /\ 200-j^0 <= 0), cost: 1
  20: l7 -> l3 : i^0'=i^post4, j^0'=j^post4, y4^0'=y4^post4, y6^0'=y6^post4, y8^0'=y8^post4, (y4^post6-y4^post4 == 0 /\ -y6^post6+y6^post8 == 0 /\ -199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y8^post6+y8^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y8^post6-y8^post4 == 0 /\ y6^0-y6^post8 == 0 /\ -y4^post6+y4^post8 == 0 /\ -j^post6+j^post8 == 0 /\ j^0-j^post8 == 0 /\ -1-j^post6+j^post4 == 0 /\ -y6^post4+y6^post6 == 0 /\ i^post6-i^post4 == 0 /\ -i^post6+i^post8 == 0), cost: 1
  14: l12 -> l5 : i^0'=i^post13, j^0'=j^post13, y4^0'=y4^post13, y6^0'=y6^post13, y8^0'=y8^post13, (i^post13 == 0 /\ y6^post14-y6^post13 == 0 /\ y8^0-y8^post14 == 0 /\ -i^post14+i^0 == 0 /\ y6^0-y6^post14 == 0 /\ y4^post14-y4^post13 == 0 /\ -y4^post14+y4^0 == 0 /\ -j^post14+j^0 == 0 /\ j^post14-j^post13 == 0 /\ -y8^post13+y8^post14 == 0), cost: 1

	Eliminating location l11 by chaining:

	Applied chaining

	First rule:
	l12 -> l11 : i^0'=i^post14, j^0'=j^post14, y4^0'=y4^post14, y6^0'=y6^post14, y8^0'=y8^post14, (y8^0-y8^post14 == 0 /\ -i^post14+i^0 == 0 /\ y6^0-y6^post14 == 0 /\ -y4^post14+y4^0 == 0 /\ -j^post14+j^0 == 0), cost: 1
	Second rule:
	l11 -> l5 : i^0'=i^post13, j^0'=j^post13, y4^0'=y4^post13, y6^0'=y6^post13, y8^0'=y8^post13, (i^post13 == 0 /\ -y4^post13+y4^0 == 0 /\ y8^0-y8^post13 == 0 /\ y6^0-y6^post13 == 0 /\ j^0-j^post13 == 0), cost: 1
	New rule:
	l12 -> l5 : i^0'=i^post13, j^0'=j^post13, y4^0'=y4^post13, y6^0'=y6^post13, y8^0'=y8^post13, (i^post13 == 0 /\ y6^post14-y6^post13 == 0 /\ y8^0-y8^post14 == 0 /\ -i^post14+i^0 == 0 /\ y6^0-y6^post14 == 0 /\ y4^post14-y4^post13 == 0 /\ -y4^post14+y4^0 == 0 /\ -j^post14+j^0 == 0 /\ j^post14-j^post13 == 0 /\ -y8^post13+y8^post14 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 12 13
	
	Eliminating location l0 by chaining:

	Applied chaining

	First rule:
	l2 -> l0 : i^0'=i^post3, j^0'=j^post3, y4^0'=y4^post3, y6^0'=y6^post3, y8^0'=y8^post3, (-99+i^0 <= 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	Second rule:
	l0 -> l1 : i^0'=i^post1, j^0'=j^post1, y4^0'=y4^post1, y6^0'=y6^post1, y8^0'=y8^post1, (y8^0-y8^post1 == 0 /\ -i^post1+i^0 == 0 /\ -y6^post1+y6^0 == 0 /\ j^0-j^post1 == 0 /\ -y4^post1+y4^0 == 0), cost: 1
	New rule:
	l2 -> l1 : i^0'=i^post1, j^0'=j^post1, y4^0'=y4^post1, y6^0'=y6^post1, y8^0'=y8^post1, (-99+i^0 <= 0 /\ -y6^post1+y6^post3 == 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -y4^post1+y4^post3 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 2
	
	Eliminating location l1 by chaining:

	Applied chaining

	First rule:
	l2 -> l1 : i^0'=i^post1, j^0'=j^post1, y4^0'=y4^post1, y6^0'=y6^post1, y8^0'=y8^post1, (-99+i^0 <= 0 /\ -y6^post1+y6^post3 == 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -y4^post1+y4^post3 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	Second rule:
	l1 -> l10 : i^0'=i^post12, j^0'=j^post12, y4^0'=y4^post12, y6^0'=y6^post12, y8^0'=y8^post12, (-y4^post12+y4^0 == 0 /\ -i^post12+i^0 == 0 /\ y8^0-y8^post12 == 0 /\ j^0-j^post12 == 0 /\ y6^post12-i^0 == 0), cost: 1
	New rule:
	l2 -> l10 : i^0'=i^post12, j^0'=j^post12, y4^0'=y4^post12, y6^0'=y6^post12, y8^0'=y8^post12, (-99+i^0 <= 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ -y4^post1+y4^post3 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 11 15
	
	Eliminating location l10 by chaining:

	Applied chaining

	First rule:
	l2 -> l10 : i^0'=i^post12, j^0'=j^post12, y4^0'=y4^post12, y6^0'=y6^post12, y8^0'=y8^post12, (-99+i^0 <= 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ -y4^post1+y4^post3 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	Second rule:
	l10 -> l9 : i^0'=i^post11, j^0'=j^post11, y4^0'=y4^post11, y6^0'=y6^post11, y8^0'=y8^post11, (i^0-i^post11 == 0 /\ y8^0-y8^post11 == 0 /\ -y4^post11+y4^0 == 0 /\ -j^post11+j^0 == 0 /\ y6^0-y6^post11 == 0), cost: 1
	New rule:
	l2 -> l9 : i^0'=i^post11, j^0'=j^post11, y4^0'=y4^post11, y6^0'=y6^post11, y8^0'=y8^post11, (-99+i^0 <= 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ y6^post12-y6^post11 == 0 /\ i^post12-i^post11 == 0 /\ -y8^post11+y8^post12 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ -j^post11+j^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ y4^post12-y4^post11 == 0 /\ -y4^post1+y4^post3 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 10 16
	
	Eliminating location l9 by chaining:

	Applied chaining

	First rule:
	l2 -> l9 : i^0'=i^post11, j^0'=j^post11, y4^0'=y4^post11, y6^0'=y6^post11, y8^0'=y8^post11, (-99+i^0 <= 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ y6^post12-y6^post11 == 0 /\ i^post12-i^post11 == 0 /\ -y8^post11+y8^post12 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ -j^post11+j^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ y4^post12-y4^post11 == 0 /\ -y4^post1+y4^post3 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	Second rule:
	l9 -> l5 : i^0'=i^post10, j^0'=j^post10, y4^0'=y4^post10, y6^0'=y6^post10, y8^0'=y8^post10, (-y4^post10+y4^0 == 0 /\ -y6^post10+y6^0 == 0 /\ y8^0-y8^post10 == 0 /\ j^0-j^post10 == 0 /\ -1+i^post10-i^0 == 0), cost: 1
	New rule:
	l2 -> l5 : i^0'=i^post10, j^0'=j^post10, y4^0'=y4^post10, y6^0'=y6^post10, y8^0'=y8^post10, (-1+i^post10-i^post11 == 0 /\ -99+i^0 <= 0 /\ y8^post11-y8^post10 == 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ y4^post11-y4^post10 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ y6^post12-y6^post11 == 0 /\ i^post12-i^post11 == 0 /\ -y8^post11+y8^post12 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ -j^post11+j^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ j^post11-j^post10 == 0 /\ y4^post12-y4^post11 == 0 /\ -y4^post1+y4^post3 == 0 /\ -y6^post10+y6^post11 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 9 17
	
	Eliminating location l6 by chaining:

	Applied chaining

	First rule:
	l7 -> l6 : i^0'=i^post8, j^0'=j^post8, y4^0'=y4^post8, y6^0'=y6^post8, y8^0'=y8^post8, (-199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y6^0-y6^post8 == 0 /\ j^0-j^post8 == 0), cost: 1
	Second rule:
	l6 -> l4 : i^0'=i^post6, j^0'=j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (y6^0-y6^post6 == 0 /\ -y8^post6+y8^0 == 0 /\ i^0-i^post6 == 0 /\ -y4^post6+y4^0 == 0 /\ -j^post6+j^0 == 0), cost: 1
	New rule:
	l7 -> l4 : i^0'=i^post6, j^0'=j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (-y6^post6+y6^post8 == 0 /\ -199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y8^post6+y8^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y6^0-y6^post8 == 0 /\ -y4^post6+y4^post8 == 0 /\ -j^post6+j^post8 == 0 /\ j^0-j^post8 == 0 /\ -i^post6+i^post8 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 5 7
	
	Eliminating location l4 by chaining:

	Applied chaining

	First rule:
	l7 -> l4 : i^0'=i^post6, j^0'=j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (-y6^post6+y6^post8 == 0 /\ -199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y8^post6+y8^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y6^0-y6^post8 == 0 /\ -y4^post6+y4^post8 == 0 /\ -j^post6+j^post8 == 0 /\ j^0-j^post8 == 0 /\ -i^post6+i^post8 == 0), cost: 1
	Second rule:
	l4 -> l3 : i^0'=i^post4, j^0'=j^post4, y4^0'=y4^post4, y6^0'=y6^post4, y8^0'=y8^post4, (y8^0-y8^post4 == 0 /\ y6^0-y6^post4 == 0 /\ -y4^post4+y4^0 == 0 /\ i^0-i^post4 == 0 /\ -1+j^post4-j^0 == 0), cost: 1
	New rule:
	l7 -> l3 : i^0'=i^post4, j^0'=j^post4, y4^0'=y4^post4, y6^0'=y6^post4, y8^0'=y8^post4, (y4^post6-y4^post4 == 0 /\ -y6^post6+y6^post8 == 0 /\ -199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y8^post6+y8^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y8^post6-y8^post4 == 0 /\ y6^0-y6^post8 == 0 /\ -y4^post6+y4^post8 == 0 /\ -j^post6+j^post8 == 0 /\ j^0-j^post8 == 0 /\ -1-j^post6+j^post4 == 0 /\ -y6^post4+y6^post6 == 0 /\ i^post6-i^post4 == 0 /\ -i^post6+i^post8 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 3 19

Simplified Transitions

Start location: l12
Program variables: i^0 j^0 y4^0 y6^0 y8^0
  21: l2 -> l3 : j^0'=100, 100-i^0 <= 0, cost: 1
  26: l2 -> l5 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1
  24: l3 -> l7 : T, cost: 1
  22: l5 -> l2 : T, cost: 1
  23: l7 -> l8 : 200-j^0 <= 0, cost: 1
  27: l7 -> l3 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1
  25: l12 -> l5 : i^0'=0, T, cost: 1

	Propagated Equalities

	Original rule:
	l2 -> l3 : i^0'=i^post2, j^0'=j^post2, y4^0'=y4^post2, y6^0'=y6^post2, y8^0'=y8^post2, (y8^0-y8^post2 == 0 /\ -100+j^post2 == 0 /\ y6^0-y6^post2 == 0 /\ 100-i^0 <= 0 /\ -y4^post2+y4^0 == 0 /\ i^0-i^post2 == 0), cost: 1
	New rule:
	l2 -> l3 : i^0'=i^0, j^0'=100, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, (0 == 0 /\ 100-i^0 <= 0), cost: 1
	
		propagated equality y8^post2 = y8^0
		
		propagated equality j^post2 = 100
		
		propagated equality y6^post2 = y6^0
		
		propagated equality y4^post2 = y4^0
		
		propagated equality i^post2 = i^0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : i^0'=i^0, j^0'=100, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, (0 == 0 /\ 100-i^0 <= 0), cost: 1
	New rule:
	l2 -> l3 : i^0'=i^0, j^0'=100, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 100-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : i^0'=i^0, j^0'=100, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 100-i^0 <= 0, cost: 1
	New rule:
	l2 -> l3 : j^0'=100, 100-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l2 : i^0'=i^post5, j^0'=j^post5, y4^0'=y4^post5, y6^0'=y6^post5, y8^0'=y8^post5, (y8^0-y8^post5 == 0 /\ j^0-j^post5 == 0 /\ -i^post5+i^0 == 0 /\ -y4^post5+y4^0 == 0 /\ -y6^post5+y6^0 == 0), cost: 1
	New rule:
	l5 -> l2 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1
	
		propagated equality y8^post5 = y8^0
		
		propagated equality j^post5 = j^0
		
		propagated equality i^post5 = i^0
		
		propagated equality y4^post5 = y4^0
		
		propagated equality y6^post5 = y6^0
		
	Simplified Guard

	Original rule:
	l5 -> l2 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1
	New rule:
	l5 -> l2 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l2 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1
	New rule:
	l5 -> l2 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l8 : i^0'=i^post7, j^0'=j^post7, y4^0'=y4^post7, y6^0'=y6^post7, y8^0'=y8^post7, (j^0-j^post7 == 0 /\ y4^0-y4^post7 == 0 /\ -i^post7+i^0 == 0 /\ -y6^post7+y6^0 == 0 /\ y8^0-y8^post7 == 0 /\ 200-j^0 <= 0), cost: 1
	New rule:
	l7 -> l8 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, (0 == 0 /\ 200-j^0 <= 0), cost: 1
	
		propagated equality j^post7 = j^0
		
		propagated equality y4^post7 = y4^0
		
		propagated equality i^post7 = i^0
		
		propagated equality y6^post7 = y6^0
		
		propagated equality y8^post7 = y8^0
		
	Simplified Guard

	Original rule:
	l7 -> l8 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, (0 == 0 /\ 200-j^0 <= 0), cost: 1
	New rule:
	l7 -> l8 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 200-j^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l8 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 200-j^0 <= 0, cost: 1
	New rule:
	l7 -> l8 : 200-j^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l7 : i^0'=i^post9, j^0'=j^post9, y4^0'=y4^post9, y6^0'=y6^post9, y8^0'=y8^post9, (-y4^post9+y4^0 == 0 /\ -i^post9+i^0 == 0 /\ y8^0-y8^post9 == 0 /\ -y6^post9+y6^0 == 0 /\ j^0-j^post9 == 0), cost: 1
	New rule:
	l3 -> l7 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1
	
		propagated equality y4^post9 = y4^0
		
		propagated equality i^post9 = i^0
		
		propagated equality y8^post9 = y8^0
		
		propagated equality y6^post9 = y6^0
		
		propagated equality j^post9 = j^0
		
	Simplified Guard

	Original rule:
	l3 -> l7 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1
	New rule:
	l3 -> l7 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l7 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1
	New rule:
	l3 -> l7 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l5 : i^0'=i^post13, j^0'=j^post13, y4^0'=y4^post13, y6^0'=y6^post13, y8^0'=y8^post13, (i^post13 == 0 /\ y6^post14-y6^post13 == 0 /\ y8^0-y8^post14 == 0 /\ -i^post14+i^0 == 0 /\ y6^0-y6^post14 == 0 /\ y4^post14-y4^post13 == 0 /\ -y4^post14+y4^0 == 0 /\ -j^post14+j^0 == 0 /\ j^post14-j^post13 == 0 /\ -y8^post13+y8^post14 == 0), cost: 1
	New rule:
	l12 -> l5 : i^0'=0, j^0'=j^post14, y4^0'=y4^post14, y6^0'=y6^post14, y8^0'=y8^post14, (0 == 0 /\ y8^0-y8^post14 == 0 /\ -i^post14+i^0 == 0 /\ y6^0-y6^post14 == 0 /\ -y4^post14+y4^0 == 0 /\ -j^post14+j^0 == 0), cost: 1
	
		propagated equality i^post13 = 0
		
		propagated equality y6^post13 = y6^post14
		
		propagated equality y4^post13 = y4^post14
		
		propagated equality j^post13 = j^post14
		
		propagated equality y8^post13 = y8^post14
		
	Propagated Equalities

	Original rule:
	l12 -> l5 : i^0'=0, j^0'=j^post14, y4^0'=y4^post14, y6^0'=y6^post14, y8^0'=y8^post14, (0 == 0 /\ y8^0-y8^post14 == 0 /\ -i^post14+i^0 == 0 /\ y6^0-y6^post14 == 0 /\ -y4^post14+y4^0 == 0 /\ -j^post14+j^0 == 0), cost: 1
	New rule:
	l12 -> l5 : i^0'=0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1
	
		propagated equality y8^post14 = y8^0
		
		propagated equality i^post14 = i^0
		
		propagated equality y6^post14 = y6^0
		
		propagated equality y4^post14 = y4^0
		
		propagated equality j^post14 = j^0
		
	Simplified Guard

	Original rule:
	l12 -> l5 : i^0'=0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1
	New rule:
	l12 -> l5 : i^0'=0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l5 : i^0'=0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1
	New rule:
	l12 -> l5 : i^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l5 : i^0'=i^post10, j^0'=j^post10, y4^0'=y4^post10, y6^0'=y6^post10, y8^0'=y8^post10, (-1+i^post10-i^post11 == 0 /\ -99+i^0 <= 0 /\ y8^post11-y8^post10 == 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ y4^post11-y4^post10 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ y6^post12-y6^post11 == 0 /\ i^post12-i^post11 == 0 /\ -y8^post11+y8^post12 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ -j^post11+j^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ j^post11-j^post10 == 0 /\ y4^post12-y4^post11 == 0 /\ -y4^post1+y4^post3 == 0 /\ -y6^post10+y6^post11 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	New rule:
	l2 -> l5 : i^0'=1+i^post11, j^0'=j^post11, y4^0'=y4^post11, y6^0'=y6^post11, y8^0'=y8^post11, (0 == 0 /\ -99+i^0 <= 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ y6^post12-y6^post11 == 0 /\ i^post12-i^post11 == 0 /\ -y8^post11+y8^post12 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ -j^post11+j^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ y4^post12-y4^post11 == 0 /\ -y4^post1+y4^post3 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	
		propagated equality i^post10 = 1+i^post11
		
		propagated equality y8^post10 = y8^post11
		
		propagated equality y4^post10 = y4^post11
		
		propagated equality j^post10 = j^post11
		
		propagated equality y6^post10 = y6^post11
		
	Propagated Equalities

	Original rule:
	l2 -> l5 : i^0'=1+i^post11, j^0'=j^post11, y4^0'=y4^post11, y6^0'=y6^post11, y8^0'=y8^post11, (0 == 0 /\ -99+i^0 <= 0 /\ i^post1-i^post12 == 0 /\ -y6^post1+y6^post3 == 0 /\ -y4^post12+y4^post1 == 0 /\ j^post1-j^post12 == 0 /\ -i^0+y4^post3 == 0 /\ -i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ y6^post12-y6^post11 == 0 /\ i^post12-i^post11 == 0 /\ -y8^post11+y8^post12 == 0 /\ -j^post1+j^post3 == 0 /\ -y8^post1+y8^post3 == 0 /\ -i^post1+y6^post12 == 0 /\ -j^post11+j^post12 == 0 /\ y8^post1-y8^post12 == 0 /\ y4^post12-y4^post11 == 0 /\ -y4^post1+y4^post3 == 0 /\ -i^post1+i^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ y8^0-y8^post3 == 0), cost: 1
	New rule:
	l2 -> l5 : i^0'=1+i^0, j^0'=j^0, y4^0'=i^0, y6^0'=i^0, y8^0'=y8^0, (0 == 0 /\ -99+i^0 <= 0), cost: 1
	
		propagated equality i^post1 = i^post12
		
		propagated equality y6^post1 = y6^post3
		
		propagated equality y4^post1 = y4^post12
		
		propagated equality j^post1 = j^post12
		
		propagated equality y4^post3 = i^0
		
		propagated equality i^post3 = i^0
		
		propagated equality j^post3 = j^0
		
		propagated equality y6^post11 = y6^post12
		
		propagated equality i^post11 = i^post12
		
		propagated equality y8^post11 = y8^post12
		
		propagated equality j^post12 = j^0
		
		propagated equality y8^post1 = y8^post3
		
		propagated equality i^post12 = y6^post12
		
		propagated equality j^post11 = j^0
		
		propagated equality y8^post12 = y8^post3
		
		propagated equality y4^post11 = y4^post12
		
		propagated equality y4^post12 = i^0
		
		propagated equality y6^post12 = i^0
		
		propagated equality y6^post3 = y6^0
		
		propagated equality y8^post3 = y8^0
		
	Simplified Guard

	Original rule:
	l2 -> l5 : i^0'=1+i^0, j^0'=j^0, y4^0'=i^0, y6^0'=i^0, y8^0'=y8^0, (0 == 0 /\ -99+i^0 <= 0), cost: 1
	New rule:
	l2 -> l5 : i^0'=1+i^0, j^0'=j^0, y4^0'=i^0, y6^0'=i^0, y8^0'=y8^0, -99+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l5 : i^0'=1+i^0, j^0'=j^0, y4^0'=i^0, y6^0'=i^0, y8^0'=y8^0, -99+i^0 <= 0, cost: 1
	New rule:
	l2 -> l5 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l3 : i^0'=i^post4, j^0'=j^post4, y4^0'=y4^post4, y6^0'=y6^post4, y8^0'=y8^post4, (y4^post6-y4^post4 == 0 /\ -y6^post6+y6^post8 == 0 /\ -199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y8^post6+y8^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y8^post6-y8^post4 == 0 /\ y6^0-y6^post8 == 0 /\ -y4^post6+y4^post8 == 0 /\ -j^post6+j^post8 == 0 /\ j^0-j^post8 == 0 /\ -1-j^post6+j^post4 == 0 /\ -y6^post4+y6^post6 == 0 /\ i^post6-i^post4 == 0 /\ -i^post6+i^post8 == 0), cost: 1
	New rule:
	l7 -> l3 : i^0'=i^post6, j^0'=1+j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (0 == 0 /\ -y6^post6+y6^post8 == 0 /\ -199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y8^post6+y8^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y6^0-y6^post8 == 0 /\ -y4^post6+y4^post8 == 0 /\ -j^post6+j^post8 == 0 /\ j^0-j^post8 == 0 /\ -i^post6+i^post8 == 0), cost: 1
	
		propagated equality y4^post4 = y4^post6
		
		propagated equality y8^post4 = y8^post6
		
		propagated equality j^post4 = 1+j^post6
		
		propagated equality y6^post4 = y6^post6
		
		propagated equality i^post4 = i^post6
		
	Propagated Equalities

	Original rule:
	l7 -> l3 : i^0'=i^post6, j^0'=1+j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (0 == 0 /\ -y6^post6+y6^post8 == 0 /\ -199+j^0 <= 0 /\ y8^post8-j^0 == 0 /\ i^0-i^post8 == 0 /\ -y8^post6+y8^post8 == 0 /\ -y4^post8+y4^0 == 0 /\ y6^0-y6^post8 == 0 /\ -y4^post6+y4^post8 == 0 /\ -j^post6+j^post8 == 0 /\ j^0-j^post8 == 0 /\ -i^post6+i^post8 == 0), cost: 1
	New rule:
	l7 -> l3 : i^0'=i^0, j^0'=1+j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=j^0, (0 == 0 /\ -199+j^0 <= 0), cost: 1
	
		propagated equality y6^post6 = y6^post8
		
		propagated equality y8^post8 = j^0
		
		propagated equality i^post8 = i^0
		
		propagated equality y8^post6 = j^0
		
		propagated equality y4^post8 = y4^0
		
		propagated equality y6^post8 = y6^0
		
		propagated equality y4^post6 = y4^0
		
		propagated equality j^post6 = j^post8
		
		propagated equality j^post8 = j^0
		
		propagated equality i^post6 = i^0
		
	Simplified Guard

	Original rule:
	l7 -> l3 : i^0'=i^0, j^0'=1+j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=j^0, (0 == 0 /\ -199+j^0 <= 0), cost: 1
	New rule:
	l7 -> l3 : i^0'=i^0, j^0'=1+j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l3 : i^0'=i^0, j^0'=1+j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1
	New rule:
	l7 -> l3 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1

Step with 25

	Trace

	25[T]
	
	Blocked

	[{}, {}]

Step with 22

	Trace

	25[T], 22[T]
	
	Blocked

	[{}, {}, {}]

Step with 26

	Trace

	25[T], 22[T], 26[(-99+i^0 <= 0)]
	
	Blocked

	[{}, {}, {21[T]}, {}]

Accelerate

Start location: l12
Program variables: i^0 j^0 y4^0 y6^0 y8^0
  21: l2 -> l3 : j^0'=100, 100-i^0 <= 0, cost: 1
  26: l2 -> l5 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1
  24: l3 -> l7 : T, cost: 1
  22: l5 -> l2 : T, cost: 1
  28: l5 -> l5 : i^0'=n+i^0, y4^0'=-1+n+i^0, y6^0'=-1+n+i^0, (-1+n >= 0 /\ 100-n-i^0 >= 0), cost: 1
  23: l7 -> l8 : 200-j^0 <= 0, cost: 1
  27: l7 -> l3 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1
  25: l12 -> l5 : i^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l5 -> l5 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1
	New rule:
	l5 -> l5 : i^0'=n+i^0, y4^0'=-1+n+i^0, y6^0'=-1+n+i^0, (-1+n >= 0 /\ 100-n-i^0 >= 0), cost: 1

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

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)]
	
	Blocked

	[{}, {}, {28[T]}]

Step with 22

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T]
	
	Blocked

	[{}, {}, {28[T]}, {}]

Step with 26

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 26[(-99+i^0 <= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {}, {}]

Covered

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T]
	
	Blocked

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

Step with 21

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)]
	
	Blocked

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

Step with 24

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 24[T]
	
	Blocked

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

Step with 27

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 24[T], 27[(-199+j^0 <= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {}, {23[T]}, {}]

Accelerate

Start location: l12
Program variables: i^0 j^0 y4^0 y6^0 y8^0
  21: l2 -> l3 : j^0'=100, 100-i^0 <= 0, cost: 1
  26: l2 -> l5 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1
  24: l3 -> l7 : T, cost: 1
  29: l3 -> l3 : j^0'=n2+j^0, y8^0'=-1+n2+j^0, (-1+n2 >= 0 /\ 200-n2-j^0 >= 0), cost: 1
  22: l5 -> l2 : T, cost: 1
  28: l5 -> l5 : i^0'=n+i^0, y4^0'=-1+n+i^0, y6^0'=-1+n+i^0, (-1+n >= 0 /\ 100-n-i^0 >= 0), cost: 1
  23: l7 -> l8 : 200-j^0 <= 0, cost: 1
  27: l7 -> l3 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1
  25: l12 -> l5 : i^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l3 -> l3 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1
	New rule:
	l3 -> l3 : j^0'=n2+j^0, y8^0'=-1+n2+j^0, (-1+n2 >= 0 /\ 200-n2-j^0 >= 0), cost: 1

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

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 29[(-1+n2 >= 0 /\ 200-n2-j^0 >= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {}, {29[T]}]

Step with 24

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 29[(-1+n2 >= 0 /\ 200-n2-j^0 >= 0)], 24[T]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {}, {29[T]}, {}]

Step with 27

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 29[(-1+n2 >= 0 /\ 200-n2-j^0 >= 0)], 24[T], 27[(-199+j^0 <= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {}, {29[T]}, {}, {}]

Covered

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 29[(-1+n2 >= 0 /\ 200-n2-j^0 >= 0)], 24[T]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {}, {29[T]}, {27[T]}]

Step with 23

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 29[(-1+n2 >= 0 /\ 200-n2-j^0 >= 0)], 24[T], 23[(200-j^0 <= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {}, {29[T]}, {27[T]}, {}]

Backtrack

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 29[(-1+n2 >= 0 /\ 200-n2-j^0 >= 0)], 24[T]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {}, {29[T]}, {23[T], 27[T]}]

Backtrack

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 29[(-1+n2 >= 0 /\ 200-n2-j^0 >= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {}, {24[T], 29[T]}]

Backtrack

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {29[T]}]

Step with 24

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 24[T]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {29[T]}, {}]

Step with 27

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 24[T], 27[(-199+j^0 <= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {29[T]}, {23[T]}, {}]

Covered

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)], 24[T]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {29[T]}, {23[T], 27[T]}]

Backtrack

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T], 21[(100-i^0 <= 0)]
	
	Blocked

	[{}, {}, {28[T]}, {26[T]}, {24[T], 29[T]}]

Backtrack

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)], 22[T]
	
	Blocked

	[{}, {}, {28[T]}, {21[T], 26[T]}]

Backtrack

	Trace

	25[T], 28[(-1+n >= 0 /\ 100-n-i^0 >= 0)]
	
	Blocked

	[{}, {}, {22[T], 28[T]}]

Backtrack

	Trace

	25[T]
	
	Blocked

	[{}, {28[T]}]

Step with 22

	Trace

	25[T], 22[T]
	
	Blocked

	[{}, {28[T]}, {}]

Step with 26

	Trace

	25[T], 22[T], 26[(-99+i^0 <= 0)]
	
	Blocked

	[{}, {28[T]}, {21[T]}, {}]

Covered

	Trace

	25[T], 22[T]
	
	Blocked

	[{}, {28[T]}, {21[T], 26[T]}]

Backtrack

	Trace

	25[T]
	
	Blocked

	[{}, {22[T], 28[T]}]

Backtrack

	Trace

	Blocked

	[{25[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b