unknown

Initial ITS

Start location: [1]
Program variables: x y z
   0: [1] -> [2] : y'=nondet, T, cost: 1
   1: [2] -> [3] : z'=nondet1, T, cost: 1
   2: [3] -> [5] : (nondet2 < 0 \/ nondet2 > 0), cost: 1
   5: [3] -> [7] : (nondet2 <= 0 /\ nondet2 >= 0), cost: 1
   8: [4] -> [10] : x > 0, cost: 1
  11: [4] -> [12] : x <= 0, cost: 1
   3: [5] -> [6] : x'=1, T, cost: 1
   4: [6] -> [4] : T, cost: 1
   6: [7] -> [8] : x'=-1, T, cost: 1
   7: [8] -> [4] : T, cost: 1
  14: [9] -> [15] : x > 0, cost: 1
  17: [9] -> [17] : x <= 0, cost: 1
   9: [10] -> [11] : x'=1+x, T, cost: 1
  10: [11] -> [9] : T, cost: 1
  12: [12] -> [13] : x'=-1+x, T, cost: 1
  13: [13] -> [9] : T, cost: 1
  20: [14] -> [20] : x > 0, cost: 1
  23: [14] -> [22] : x <= 0, cost: 1
  15: [15] -> [16] : x'=1+x, T, cost: 1
  16: [16] -> [14] : T, cost: 1
  18: [17] -> [18] : x'=-1+x, T, cost: 1
  19: [18] -> [14] : T, cost: 1
  26: [19] -> [25] : x > 0, cost: 1
  29: [19] -> [27] : x <= 0, cost: 1
  21: [20] -> [21] : x'=1+x, T, cost: 1
  22: [21] -> [19] : T, cost: 1
  24: [22] -> [23] : x'=-1+x, T, cost: 1
  25: [23] -> [19] : T, cost: 1
  32: [24] -> [30] : x > 0, cost: 1
  35: [24] -> [32] : x <= 0, cost: 1
  27: [25] -> [26] : x'=1+x, T, cost: 1
  28: [26] -> [24] : T, cost: 1
  30: [27] -> [28] : x'=-1+x, T, cost: 1
  31: [28] -> [24] : T, cost: 1
  38: [29] -> [35] : x > 0, cost: 1
  41: [29] -> [37] : x <= 0, cost: 1
  33: [30] -> [31] : x'=1+x, T, cost: 1
  34: [31] -> [29] : T, cost: 1
  36: [32] -> [33] : x'=-1+x, T, cost: 1
  37: [33] -> [29] : T, cost: 1
  44: [34] -> [40] : x > 0, cost: 1
  47: [34] -> [42] : x <= 0, cost: 1
  39: [35] -> [36] : x'=1+x, T, cost: 1
  40: [36] -> [34] : T, cost: 1
  42: [37] -> [38] : x'=-1+x, T, cost: 1
  43: [38] -> [34] : T, cost: 1
  50: [39] -> [45] : x > 0, cost: 1
  53: [39] -> [47] : x <= 0, cost: 1
  45: [40] -> [41] : x'=1+x, T, cost: 1
  46: [41] -> [39] : T, cost: 1
  48: [42] -> [43] : x'=-1+x, T, cost: 1
  49: [43] -> [39] : T, cost: 1
  56: [44] -> [49] : (-100+z < 0 /\ -100+y < 0), cost: 1
  60: [44] -> [52] : (-100+z >= 0 \/ -100+y >= 0), cost: 1
  51: [45] -> [46] : x'=1+x, T, cost: 1
  52: [46] -> [44] : T, cost: 1
  54: [47] -> [48] : x'=-1+x, T, cost: 1
  55: [48] -> [44] : T, cost: 1
  57: [49] -> [50] : y'=x+y, T, cost: 1
  58: [50] -> [51] : z'=-x+z, T, cost: 1
  59: [51] -> [44] : T, cost: 1

Chained Linear Paths

Start location: [1]
Program variables: x y z
  61: [1] -> [3] : y'=nondet, z'=nondet1, T, cost: 1
  64: [3] -> [4] : x'=1, (nondet2 < 0 \/ nondet2 > 0), cost: 1
  65: [3] -> [4] : x'=-1, (nondet2 <= 0 /\ nondet2 >= 0), cost: 1
  68: [4] -> [9] : x'=1+x, x > 0, cost: 1
  69: [4] -> [9] : x'=-1+x, x <= 0, cost: 1
  72: [9] -> [14] : x'=1+x, x > 0, cost: 1
  73: [9] -> [14] : x'=-1+x, x <= 0, cost: 1
  76: [14] -> [19] : x'=1+x, x > 0, cost: 1
  77: [14] -> [19] : x'=-1+x, x <= 0, cost: 1
  80: [19] -> [24] : x'=1+x, x > 0, cost: 1
  81: [19] -> [24] : x'=-1+x, x <= 0, cost: 1
  84: [24] -> [29] : x'=1+x, x > 0, cost: 1
  85: [24] -> [29] : x'=-1+x, x <= 0, cost: 1
  88: [29] -> [34] : x'=1+x, x > 0, cost: 1
  89: [29] -> [34] : x'=-1+x, x <= 0, cost: 1
  92: [34] -> [39] : x'=1+x, x > 0, cost: 1
  93: [34] -> [39] : x'=-1+x, x <= 0, cost: 1
  96: [39] -> [44] : x'=1+x, x > 0, cost: 1
  97: [39] -> [44] : x'=-1+x, x <= 0, cost: 1
  60: [44] -> [52] : (-100+z >= 0 \/ -100+y >= 0), cost: 1
 100: [44] -> [44] : y'=x+y, z'=-x+z, (-100+z < 0 /\ -100+y < 0), cost: 1

	Eliminating location [2] by chaining:

	Applied chaining

	First rule:
	[1] -> [2] : y'=nondet, T, cost: 1
	Second rule:
	[2] -> [3] : z'=nondet1, T, cost: 1
	New rule:
	[1] -> [3] : y'=nondet, z'=nondet1, T, cost: 1
	
	Applied deletion

	Removed the following rules: 0 1
	
	Eliminating location [5] by chaining:

	Applied chaining

	First rule:
	[3] -> [5] : (nondet2 < 0 \/ nondet2 > 0), cost: 1
	Second rule:
	[5] -> [6] : x'=1, T, cost: 1
	New rule:
	[3] -> [6] : x'=1, (nondet2 < 0 \/ nondet2 > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 2 3
	
	Eliminating location [7] by chaining:

	Applied chaining

	First rule:
	[3] -> [7] : (nondet2 <= 0 /\ nondet2 >= 0), cost: 1
	Second rule:
	[7] -> [8] : x'=-1, T, cost: 1
	New rule:
	[3] -> [8] : x'=-1, (nondet2 <= 0 /\ nondet2 >= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 5 6
	
	Eliminating location [6] by chaining:

	Applied chaining

	First rule:
	[3] -> [6] : x'=1, (nondet2 < 0 \/ nondet2 > 0), cost: 1
	Second rule:
	[6] -> [4] : T, cost: 1
	New rule:
	[3] -> [4] : x'=1, (nondet2 < 0 \/ nondet2 > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 4 62
	
	Eliminating location [8] by chaining:

	Applied chaining

	First rule:
	[3] -> [8] : x'=-1, (nondet2 <= 0 /\ nondet2 >= 0), cost: 1
	Second rule:
	[8] -> [4] : T, cost: 1
	New rule:
	[3] -> [4] : x'=-1, (nondet2 <= 0 /\ nondet2 >= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 7 63
	
	Eliminating location [10] by chaining:

	Applied chaining

	First rule:
	[4] -> [10] : x > 0, cost: 1
	Second rule:
	[10] -> [11] : x'=1+x, T, cost: 1
	New rule:
	[4] -> [11] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 8 9
	
	Eliminating location [12] by chaining:

	Applied chaining

	First rule:
	[4] -> [12] : x <= 0, cost: 1
	Second rule:
	[12] -> [13] : x'=-1+x, T, cost: 1
	New rule:
	[4] -> [13] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 11 12
	
	Eliminating location [11] by chaining:

	Applied chaining

	First rule:
	[4] -> [11] : x'=1+x, x > 0, cost: 1
	Second rule:
	[11] -> [9] : T, cost: 1
	New rule:
	[4] -> [9] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 10 66
	
	Eliminating location [13] by chaining:

	Applied chaining

	First rule:
	[4] -> [13] : x'=-1+x, x <= 0, cost: 1
	Second rule:
	[13] -> [9] : T, cost: 1
	New rule:
	[4] -> [9] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 13 67
	
	Eliminating location [15] by chaining:

	Applied chaining

	First rule:
	[9] -> [15] : x > 0, cost: 1
	Second rule:
	[15] -> [16] : x'=1+x, T, cost: 1
	New rule:
	[9] -> [16] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 14 15
	
	Eliminating location [17] by chaining:

	Applied chaining

	First rule:
	[9] -> [17] : x <= 0, cost: 1
	Second rule:
	[17] -> [18] : x'=-1+x, T, cost: 1
	New rule:
	[9] -> [18] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 17 18
	
	Eliminating location [16] by chaining:

	Applied chaining

	First rule:
	[9] -> [16] : x'=1+x, x > 0, cost: 1
	Second rule:
	[16] -> [14] : T, cost: 1
	New rule:
	[9] -> [14] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 16 70
	
	Eliminating location [18] by chaining:

	Applied chaining

	First rule:
	[9] -> [18] : x'=-1+x, x <= 0, cost: 1
	Second rule:
	[18] -> [14] : T, cost: 1
	New rule:
	[9] -> [14] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 19 71
	
	Eliminating location [20] by chaining:

	Applied chaining

	First rule:
	[14] -> [20] : x > 0, cost: 1
	Second rule:
	[20] -> [21] : x'=1+x, T, cost: 1
	New rule:
	[14] -> [21] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 20 21
	
	Eliminating location [22] by chaining:

	Applied chaining

	First rule:
	[14] -> [22] : x <= 0, cost: 1
	Second rule:
	[22] -> [23] : x'=-1+x, T, cost: 1
	New rule:
	[14] -> [23] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 23 24
	
	Eliminating location [21] by chaining:

	Applied chaining

	First rule:
	[14] -> [21] : x'=1+x, x > 0, cost: 1
	Second rule:
	[21] -> [19] : T, cost: 1
	New rule:
	[14] -> [19] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 22 74
	
	Eliminating location [23] by chaining:

	Applied chaining

	First rule:
	[14] -> [23] : x'=-1+x, x <= 0, cost: 1
	Second rule:
	[23] -> [19] : T, cost: 1
	New rule:
	[14] -> [19] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 25 75
	
	Eliminating location [25] by chaining:

	Applied chaining

	First rule:
	[19] -> [25] : x > 0, cost: 1
	Second rule:
	[25] -> [26] : x'=1+x, T, cost: 1
	New rule:
	[19] -> [26] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 26 27
	
	Eliminating location [27] by chaining:

	Applied chaining

	First rule:
	[19] -> [27] : x <= 0, cost: 1
	Second rule:
	[27] -> [28] : x'=-1+x, T, cost: 1
	New rule:
	[19] -> [28] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 29 30
	
	Eliminating location [26] by chaining:

	Applied chaining

	First rule:
	[19] -> [26] : x'=1+x, x > 0, cost: 1
	Second rule:
	[26] -> [24] : T, cost: 1
	New rule:
	[19] -> [24] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 28 78
	
	Eliminating location [28] by chaining:

	Applied chaining

	First rule:
	[19] -> [28] : x'=-1+x, x <= 0, cost: 1
	Second rule:
	[28] -> [24] : T, cost: 1
	New rule:
	[19] -> [24] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 31 79
	
	Eliminating location [30] by chaining:

	Applied chaining

	First rule:
	[24] -> [30] : x > 0, cost: 1
	Second rule:
	[30] -> [31] : x'=1+x, T, cost: 1
	New rule:
	[24] -> [31] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 32 33
	
	Eliminating location [32] by chaining:

	Applied chaining

	First rule:
	[24] -> [32] : x <= 0, cost: 1
	Second rule:
	[32] -> [33] : x'=-1+x, T, cost: 1
	New rule:
	[24] -> [33] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 35 36
	
	Eliminating location [31] by chaining:

	Applied chaining

	First rule:
	[24] -> [31] : x'=1+x, x > 0, cost: 1
	Second rule:
	[31] -> [29] : T, cost: 1
	New rule:
	[24] -> [29] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 34 82
	
	Eliminating location [33] by chaining:

	Applied chaining

	First rule:
	[24] -> [33] : x'=-1+x, x <= 0, cost: 1
	Second rule:
	[33] -> [29] : T, cost: 1
	New rule:
	[24] -> [29] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 37 83
	
	Eliminating location [35] by chaining:

	Applied chaining

	First rule:
	[29] -> [35] : x > 0, cost: 1
	Second rule:
	[35] -> [36] : x'=1+x, T, cost: 1
	New rule:
	[29] -> [36] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 38 39
	
	Eliminating location [37] by chaining:

	Applied chaining

	First rule:
	[29] -> [37] : x <= 0, cost: 1
	Second rule:
	[37] -> [38] : x'=-1+x, T, cost: 1
	New rule:
	[29] -> [38] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 41 42
	
	Eliminating location [36] by chaining:

	Applied chaining

	First rule:
	[29] -> [36] : x'=1+x, x > 0, cost: 1
	Second rule:
	[36] -> [34] : T, cost: 1
	New rule:
	[29] -> [34] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 40 86
	
	Eliminating location [38] by chaining:

	Applied chaining

	First rule:
	[29] -> [38] : x'=-1+x, x <= 0, cost: 1
	Second rule:
	[38] -> [34] : T, cost: 1
	New rule:
	[29] -> [34] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 43 87
	
	Eliminating location [40] by chaining:

	Applied chaining

	First rule:
	[34] -> [40] : x > 0, cost: 1
	Second rule:
	[40] -> [41] : x'=1+x, T, cost: 1
	New rule:
	[34] -> [41] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 44 45
	
	Eliminating location [42] by chaining:

	Applied chaining

	First rule:
	[34] -> [42] : x <= 0, cost: 1
	Second rule:
	[42] -> [43] : x'=-1+x, T, cost: 1
	New rule:
	[34] -> [43] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 47 48
	
	Eliminating location [41] by chaining:

	Applied chaining

	First rule:
	[34] -> [41] : x'=1+x, x > 0, cost: 1
	Second rule:
	[41] -> [39] : T, cost: 1
	New rule:
	[34] -> [39] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 46 90
	
	Eliminating location [43] by chaining:

	Applied chaining

	First rule:
	[34] -> [43] : x'=-1+x, x <= 0, cost: 1
	Second rule:
	[43] -> [39] : T, cost: 1
	New rule:
	[34] -> [39] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 49 91
	
	Eliminating location [45] by chaining:

	Applied chaining

	First rule:
	[39] -> [45] : x > 0, cost: 1
	Second rule:
	[45] -> [46] : x'=1+x, T, cost: 1
	New rule:
	[39] -> [46] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 50 51
	
	Eliminating location [47] by chaining:

	Applied chaining

	First rule:
	[39] -> [47] : x <= 0, cost: 1
	Second rule:
	[47] -> [48] : x'=-1+x, T, cost: 1
	New rule:
	[39] -> [48] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 53 54
	
	Eliminating location [46] by chaining:

	Applied chaining

	First rule:
	[39] -> [46] : x'=1+x, x > 0, cost: 1
	Second rule:
	[46] -> [44] : T, cost: 1
	New rule:
	[39] -> [44] : x'=1+x, x > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 52 94
	
	Eliminating location [48] by chaining:

	Applied chaining

	First rule:
	[39] -> [48] : x'=-1+x, x <= 0, cost: 1
	Second rule:
	[48] -> [44] : T, cost: 1
	New rule:
	[39] -> [44] : x'=-1+x, x <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 55 95
	
	Eliminating location [49] by chaining:

	Applied chaining

	First rule:
	[44] -> [49] : (-100+z < 0 /\ -100+y < 0), cost: 1
	Second rule:
	[49] -> [50] : y'=x+y, T, cost: 1
	New rule:
	[44] -> [50] : y'=x+y, (-100+z < 0 /\ -100+y < 0), cost: 1
	
	Applied deletion

	Removed the following rules: 56 57
	
	Eliminating location [50] by chaining:

	Applied chaining

	First rule:
	[44] -> [50] : y'=x+y, (-100+z < 0 /\ -100+y < 0), cost: 1
	Second rule:
	[50] -> [51] : z'=-x+z, T, cost: 1
	New rule:
	[44] -> [51] : y'=x+y, z'=-x+z, (-100+z < 0 /\ -100+y < 0), cost: 1
	
	Applied deletion

	Removed the following rules: 58 98
	
	Eliminating location [51] by chaining:

	Applied chaining

	First rule:
	[44] -> [51] : y'=x+y, z'=-x+z, (-100+z < 0 /\ -100+y < 0), cost: 1
	Second rule:
	[51] -> [44] : T, cost: 1
	New rule:
	[44] -> [44] : y'=x+y, z'=-x+z, (-100+z < 0 /\ -100+y < 0), cost: 1
	
	Applied deletion

	Removed the following rules: 59 99

Simplified Transitions

Start location: [1]
Program variables: x y z
  61: [1] -> [3] : y'=nondet, z'=nondet1, T, cost: 1
  64: [3] -> [4] : x'=1, (nondet2 < 0 \/ nondet2 > 0), cost: 1
 101: [3] -> [4] : x'=-1, T, cost: 1
  68: [4] -> [9] : x'=1+x, x > 0, cost: 1
  69: [4] -> [9] : x'=-1+x, x <= 0, cost: 1
  72: [9] -> [14] : x'=1+x, x > 0, cost: 1
  73: [9] -> [14] : x'=-1+x, x <= 0, cost: 1
  76: [14] -> [19] : x'=1+x, x > 0, cost: 1
  77: [14] -> [19] : x'=-1+x, x <= 0, cost: 1
  80: [19] -> [24] : x'=1+x, x > 0, cost: 1
  81: [19] -> [24] : x'=-1+x, x <= 0, cost: 1
  84: [24] -> [29] : x'=1+x, x > 0, cost: 1
  85: [24] -> [29] : x'=-1+x, x <= 0, cost: 1
  88: [29] -> [34] : x'=1+x, x > 0, cost: 1
  89: [29] -> [34] : x'=-1+x, x <= 0, cost: 1
  92: [34] -> [39] : x'=1+x, x > 0, cost: 1
  93: [34] -> [39] : x'=-1+x, x <= 0, cost: 1
  96: [39] -> [44] : x'=1+x, x > 0, cost: 1
  97: [39] -> [44] : x'=-1+x, x <= 0, cost: 1
  60: [44] -> [52] : (-100+z >= 0 \/ -100+y >= 0), cost: 1
 100: [44] -> [44] : y'=x+y, z'=-x+z, (-100+z < 0 /\ -100+y < 0), cost: 1

	made implied equalities explicit

	Original rule:
	[3] -> [4] : x'=-1, (nondet2 <= 0 /\ nondet2 >= 0), cost: 1
	New rule:
	[3] -> [4] : x'=-1, (nondet2 <= 0 /\ nondet2 >= 0 /\ nondet2 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	[3] -> [4] : x'=-1, (nondet2 <= 0 /\ nondet2 >= 0 /\ nondet2 == 0), cost: 1
	New rule:
	[3] -> [4] : x'=-1, (0 <= 0 /\ 0 >= 0 /\ 0 == 0), cost: 1
	
		propagated equality nondet2 = 0
		
	Simplified Guard

	Original rule:
	[3] -> [4] : x'=-1, (0 <= 0 /\ 0 >= 0 /\ 0 == 0), cost: 1
	New rule:
	[3] -> [4] : x'=-1, T, cost: 1

Step with 61

	Trace

	61[T]
	
	Blocked

	[{}, {}]

Step with 64

	Trace

	61[T], 64[(nondet2 > 0)]
	
	Blocked

	[{}, {}, {}]

Step with 68

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)]
	
	Blocked

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

Step with 72

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)]
	
	Blocked

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

Step with 76

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)]
	
	Blocked

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

Step with 80

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)]
	
	Blocked

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

Step with 84

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)]
	
	Blocked

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

Step with 88

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)]
	
	Blocked

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

Step with 92

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)]
	
	Blocked

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

Step with 96

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

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

Step with 60

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 60[(-100+z >= 0)]
	
	Blocked

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

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[-100+z >= 0]}]

Step with 60

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 60[(-100+y >= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[-100+z >= 0]}, {}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[(-100+z >= 0 /\ -100+y >= 0)]}]

Step with 100

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 100[(-100+z < 0 /\ -100+y < 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[T]}, {}]

Accelerate

Start location: [1]
Program variables: x y z
  61: [1] -> [3] : y'=nondet, z'=nondet1, T, cost: 1
  64: [3] -> [4] : x'=1, (nondet2 < 0 \/ nondet2 > 0), cost: 1
 101: [3] -> [4] : x'=-1, T, cost: 1
  68: [4] -> [9] : x'=1+x, x > 0, cost: 1
  69: [4] -> [9] : x'=-1+x, x <= 0, cost: 1
  72: [9] -> [14] : x'=1+x, x > 0, cost: 1
  73: [9] -> [14] : x'=-1+x, x <= 0, cost: 1
  76: [14] -> [19] : x'=1+x, x > 0, cost: 1
  77: [14] -> [19] : x'=-1+x, x <= 0, cost: 1
  80: [19] -> [24] : x'=1+x, x > 0, cost: 1
  81: [19] -> [24] : x'=-1+x, x <= 0, cost: 1
  84: [24] -> [29] : x'=1+x, x > 0, cost: 1
  85: [24] -> [29] : x'=-1+x, x <= 0, cost: 1
  88: [29] -> [34] : x'=1+x, x > 0, cost: 1
  89: [29] -> [34] : x'=-1+x, x <= 0, cost: 1
  92: [34] -> [39] : x'=1+x, x > 0, cost: 1
  93: [34] -> [39] : x'=-1+x, x <= 0, cost: 1
  96: [39] -> [44] : x'=1+x, x > 0, cost: 1
  97: [39] -> [44] : x'=-1+x, x <= 0, cost: 1
  60: [44] -> [52] : (-100+z >= 0 \/ -100+y >= 0), cost: 1
 100: [44] -> [44] : y'=x+y, z'=-x+z, (-100+z < 0 /\ -100+y < 0), cost: 1
 102: [44] -> LoAT_sink : (-x <= 0 /\ x <= 0 /\ 100-z > 0 /\ 100-y > 0), cost: NONTERM
 103: [44] -> [44] : y'=x*n+y, z'=-x*n+z, (100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0), cost: 1

	Certificate of Non-Termination

	Original rule:
	[44] -> [44] : y'=x+y, z'=-x+z, (-100+z < 0 /\ -100+y < 0), cost: 1
	New rule:
	[44] -> LoAT_sink : (-x <= 0 /\ x <= 0 /\ 100-z > 0 /\ 100-y > 0), cost: NONTERM

		100-z > 0 [0]: eventual decrease yields (100-z+x*(-1+n) > 0 /\ 100-z > 0)
		
		100-z > 0 [1]: eventual increase yields (-x <= 0 /\ 100-z > 0)
		
		100-y > 0 [0]: eventual decrease yields (100-x*(-1+n)-y > 0 /\ 100-y > 0)
		
		100-y > 0 [1]: eventual increase yields (x <= 0 /\ 100-y > 0)
		
		Replacement map: {100-z > 0 -> (-x <= 0 /\ 100-z > 0), 100-y > 0 -> (x <= 0 /\ 100-y > 0)}

	Loop Acceleration

	Original rule:
	[44] -> [44] : y'=x+y, z'=-x+z, (-100+z < 0 /\ -100+y < 0), cost: 1
	New rule:
	[44] -> [44] : y'=x*n+y, z'=-x*n+z, (100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0), cost: 1

		100-z > 0 [0]: eventual decrease yields (100-z+x*(-1+n) > 0 /\ 100-z > 0)
		
		100-z > 0 [1]: eventual increase yields (-x <= 0 /\ 100-z > 0)
		
		100-y > 0 [0]: eventual decrease yields (100-x*(-1+n)-y > 0 /\ 100-y > 0)
		
		100-y > 0 [1]: eventual increase yields (x <= 0 /\ 100-y > 0)
		
		Replacement map: {100-z > 0 -> (100-z+x*(-1+n) > 0 /\ 100-z > 0), 100-y > 0 -> (100-x*(-1+n)-y > 0 /\ 100-y > 0)}

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[T]}, {100[T], 103[T]}]

Step with 60

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)], 60[(-100+y >= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[T]}, {100[T], 102[T], 103[T]}, {}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[T]}, {60[-100+y >= 0], 100[T], 102[T], 103[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[T], 103[T]}]

Step with 100

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 100[(-100+z < 0 /\ -100+y < 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[T], 103[T]}, {}]

Covered

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {}, {60[T], 100[T], 103[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {}, {96[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {}, {92[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}, {88[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {84[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {80[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)], 72[(x > 0)]
	
	Blocked

	[{}, {}, {}, {}, {76[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)], 68[(x > 0)]
	
	Blocked

	[{}, {}, {}, {72[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 > 0)]
	
	Blocked

	[{}, {}, {68[T]}]

Backtrack

	Trace

	61[T]
	
	Blocked

	[{}, {64[nondet2 > 0]}]

Step with 64

	Trace

	61[T], 64[(nondet2 < 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}]

Step with 68

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}]

Step with 72

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}]

Step with 76

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}]

Step with 80

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}]

Step with 84

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}]

Step with 88

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}]

Step with 92

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}]

Step with 96

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {}]

Step with 100

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 100[(-100+z < 0 /\ -100+y < 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {102[T]}, {}]

Covered

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {100[T], 102[T]}]

Step with 103

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {100[T], 102[T]}, {103[T]}]

Step with 60

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)], 60[(-100+y >= 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {100[T], 102[T]}, {102[T], 103[T]}, {}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {100[T], 102[T]}, {60[-100+y >= 0], 102[T], 103[T]}]

Step with 100

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)], 100[(-100+z < 0 /\ -100+y < 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {100[T], 102[T]}, {60[T], 102[T], 103[T]}, {}]

Covered

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {100[T], 102[T]}, {60[T], 100[T], 102[T], 103[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {100[T], 102[T], 103[T]}]

Step with 60

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 60[(-100+y >= 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {100[T], 102[T], 103[T]}, {}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {60[-100+y >= 0], 100[T], 102[T], 103[T]}]

Step with 60

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)], 60[(-100+z >= 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {60[-100+y >= 0], 100[T], 102[T], 103[T]}, {}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)], 96[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {}, {60[(-100+z >= 0 /\ -100+y >= 0)], 100[T], 102[T], 103[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)], 92[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {}, {96[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)], 88[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {}, {92[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)], 84[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {}, {88[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)], 80[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {}, {84[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)], 76[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {}, {80[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)], 72[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {}, {76[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)], 68[(x > 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {}, {72[T]}]

Backtrack

	Trace

	61[T], 64[(nondet2 < 0)]
	
	Blocked

	[{}, {64[nondet2 > 0]}, {68[T]}]

Backtrack

	Trace

	61[T]
	
	Blocked

	[{}, {64[(nondet2 < 0 /\ nondet2 > 0)]}]

Step with 101

	Trace

	61[T], 101[T]
	
	Blocked

	[{}, {64[T]}, {}]

Step with 69

	Trace

	61[T], 101[T], 69[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {}]

Step with 73

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {}]

Step with 77

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {}]

Step with 81

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {}]

Step with 85

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {}]

Step with 89

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {}]

Step with 93

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {}]

Step with 97

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {}]

Step with 60

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)], 60[(-100+z >= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {102[T]}, {}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[-100+z >= 0], 102[T]}]

Step with 60

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)], 60[(-100+y >= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[-100+z >= 0], 102[T]}, {}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[(-100+z >= 0 /\ -100+y >= 0)], 102[T]}]

Step with 100

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)], 100[(-100+z < 0 /\ -100+y < 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[T], 102[T]}, {}]

Covered

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[T], 100[T], 102[T]}]

Step with 103

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[T], 100[T], 102[T]}, {103[T]}]

Step with 60

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)], 60[(-100+z >= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[T], 100[T], 102[T]}, {102[T], 103[T]}, {}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[T], 100[T], 102[T]}, {60[-100+z >= 0], 102[T], 103[T]}]

Step with 100

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)], 100[(-100+z < 0 /\ -100+y < 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[T], 100[T], 102[T]}, {60[T], 102[T], 103[T]}, {}]

Covered

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)], 103[(100-z+x*(-1+n) > 0 /\ -1+n >= 0 /\ 100-x*(-1+n)-y > 0 /\ 100-z > 0 /\ 100-y > 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[T], 100[T], 102[T]}, {60[T], 100[T], 102[T], 103[T]}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)], 97[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T]}, {60[T], 100[T], 102[T], 103[T]}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)], 93[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T]}, {96[T], 97[T]}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)], 89[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T]}, {92[T], 93[T]}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)], 85[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T]}, {88[T], 89[T]}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)], 81[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T]}, {84[T], 85[T]}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)], 77[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T]}, {80[T], 81[T]}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)], 73[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T]}, {76[T], 77[T]}]

Backtrack

	Trace

	61[T], 101[T], 69[(x <= 0)]
	
	Blocked

	[{}, {64[T]}, {68[T]}, {72[T], 73[T]}]

Backtrack

	Trace

	61[T], 101[T]
	
	Blocked

	[{}, {64[T]}, {68[T], 69[T]}]

Backtrack

	Trace

	61[T]
	
	Blocked

	[{}, {64[T], 101[T]}]

Backtrack

	Trace

	Blocked

	[{61[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b