unknown

Initial ITS

Start location: [1]
Program variables: r x y
   0: [1] -> [2] : x'=nondet, T, cost: 1
   1: [2] -> [3] : y'=nondet1, T, cost: 1
   2: [3] -> [5] : x < 0, cost: 1
   5: [3] -> [4] : x >= 0, cost: 1
   6: [4] -> [8] : y < 0, cost: 1
   9: [4] -> [7] : y >= 0, cost: 1
   3: [5] -> [6] : x'=-x, T, cost: 1
   4: [6] -> [4] : T, cost: 1
  10: [7] -> [10] : y > 0, cost: 1
  19: [7] -> [17] : y <= 0, cost: 1
   7: [8] -> [9] : y'=-y, T, cost: 1
   8: [9] -> [7] : T, cost: 1
  11: [10] -> [11] : r'=x, T, cost: 1
  12: [11] -> [12] : r-y >= 0, cost: 1
  15: [11] -> [14] : r-y < 0, cost: 1
  13: [12] -> [13] : r'=r-y, T, cost: 1
  14: [13] -> [11] : T, cost: 1
  16: [14] -> [15] : x'=y, T, cost: 1
  17: [15] -> [16] : y'=r, T, cost: 1
  18: [16] -> [7] : T, cost: 1

Chained Linear Paths

Start location: [1]
Program variables: r x y
  20: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   5: [3] -> [4] : x >= 0, cost: 1
  22: [3] -> [4] : x'=-x, x < 0, cost: 1
   9: [4] -> [7] : y >= 0, cost: 1
  24: [4] -> [7] : y'=-y, y < 0, cost: 1
  19: [7] -> [17] : y <= 0, cost: 1
  25: [7] -> [11] : r'=x, y > 0, cost: 1
  28: [11] -> [11] : r'=r-y, r-y >= 0, cost: 1
  30: [11] -> [7] : x'=y, y'=r, r-y < 0, cost: 1

	Eliminating location [2] by chaining:

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

	Removed the following rules: 8 23
	
	Eliminating location [10] by chaining:

	Applied chaining

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

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

	Applied chaining

	First rule:
	[11] -> [12] : r-y >= 0, cost: 1
	Second rule:
	[12] -> [13] : r'=r-y, T, cost: 1
	New rule:
	[11] -> [13] : r'=r-y, r-y >= 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[11] -> [14] : r-y < 0, cost: 1
	Second rule:
	[14] -> [15] : x'=y, T, cost: 1
	New rule:
	[11] -> [15] : x'=y, r-y < 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[11] -> [13] : r'=r-y, r-y >= 0, cost: 1
	Second rule:
	[13] -> [11] : T, cost: 1
	New rule:
	[11] -> [11] : r'=r-y, r-y >= 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[11] -> [15] : x'=y, r-y < 0, cost: 1
	Second rule:
	[15] -> [16] : y'=r, T, cost: 1
	New rule:
	[11] -> [16] : x'=y, y'=r, r-y < 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[11] -> [16] : x'=y, y'=r, r-y < 0, cost: 1
	Second rule:
	[16] -> [7] : T, cost: 1
	New rule:
	[11] -> [7] : x'=y, y'=r, r-y < 0, cost: 1
	
	Applied deletion

	Removed the following rules: 18 29

Step with 20

	Trace

	20[T]
	
	Blocked

	[{}, {}]

Step with 5

	Trace

	20[T], 5[(x >= 0)]
	
	Blocked

	[{}, {}, {}]

Step with 9

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)]
	
	Blocked

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

Step with 19

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 19[(y <= 0)]
	
	Blocked

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

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)]
	
	Blocked

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

Step with 25

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)]
	
	Blocked

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

Step with 28

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

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

Accelerate

Start location: [1]
Program variables: r x y
  20: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   5: [3] -> [4] : x >= 0, cost: 1
  22: [3] -> [4] : x'=-x, x < 0, cost: 1
   9: [4] -> [7] : y >= 0, cost: 1
  24: [4] -> [7] : y'=-y, y < 0, cost: 1
  19: [7] -> [17] : y <= 0, cost: 1
  25: [7] -> [11] : r'=x, y > 0, cost: 1
  28: [11] -> [11] : r'=r-y, r-y >= 0, cost: 1
  30: [11] -> [7] : x'=y, y'=r, r-y < 0, cost: 1
  31: [11] -> LoAT_sink : (r-y >= 0 /\ y <= 0), cost: NONTERM
  32: [11] -> [11] : r'=-n*y+r, (-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0), cost: 1

	Certificate of Non-Termination

	Original rule:
	[11] -> [11] : r'=r-y, (r-y >= 0), cost: 1
	New rule:
	[11] -> LoAT_sink : (r-y >= 0 /\ y <= 0), cost: NONTERM

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

	Loop Acceleration

	Original rule:
	[11] -> [11] : r'=r-y, (r-y >= 0), cost: 1
	New rule:
	[11] -> [11] : r'=-n*y+r, (-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0), cost: 1

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

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 32[T]}]

Step with 30

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 25

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 32

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {32[T]}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 28

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {25[T]}]

Step with 19

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {25[T]}, {}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 31[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)]
	
	Blocked

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

Step with 28

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

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

Covered

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}]

Step with 30

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 19

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {}, {}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}]

Step with 25

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {}]

Step with 32

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 25

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 32

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {32[T]}]

Covered

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {25[T]}]

Step with 19

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {25[T]}, {}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {}, {19[T]}, {28[T], 30[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 9[(y >= 0)]
	
	Blocked

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

Backtrack

	Trace

	20[T], 5[(x >= 0)]
	
	Blocked

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

Step with 24

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)]
	
	Blocked

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

Step with 25

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)]
	
	Blocked

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

Step with 28

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

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

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}]

Step with 30

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}]

Step with 25

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {}]

Step with 32

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Step with 25

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {}]

Step with 32

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {32[T]}]

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {25[T]}]

Step with 19

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {25[T]}, {}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {25[T]}]

Step with 19

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {25[T]}, {}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 31[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}]

Step with 32

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Step with 19

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}]

Step with 25

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {}]

Step with 32

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {}, {9[T]}, {19[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 5[(x >= 0)], 24[(y < 0)]
	
	Blocked

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

Backtrack

	Trace

	20[T], 5[(x >= 0)]
	
	Blocked

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

Backtrack

	Trace

	20[T]
	
	Blocked

	[{}, {5[T]}]

Step with 22

	Trace

	20[T], 22[(x < 0)]
	
	Blocked

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

Step with 24

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)]
	
	Blocked

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

Step with 25

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)]
	
	Blocked

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

Step with 28

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {31[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}]

Step with 30

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}]

Step with 25

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {}]

Step with 32

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Step with 25

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {}]

Step with 32

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {32[T]}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {25[T]}]

Step with 19

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {25[T]}, {}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 31[T]}, {25[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}]

Step with 32

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Step with 19

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}]

Step with 25

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {}]

Step with 32

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 24[(y < 0)]
	
	Blocked

	[{}, {5[T]}, {}, {25[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)]
	
	Blocked

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

Step with 9

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)]
	
	Blocked

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

Step with 25

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)]
	
	Blocked

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

Step with 28

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {31[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}]

Step with 30

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}]

Step with 25

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {}]

Step with 32

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Step with 25

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {}]

Step with 32

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T]}, {32[T]}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {25[T]}]

Step with 19

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {25[T]}, {}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 31[T]}, {25[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}]

Step with 32

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Step with 19

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}, {}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}]

Step with 25

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {}]

Step with 32

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}]

Step with 30

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T], 32[T]}]

Step with 28

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)], 28[(r-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {30[T], 31[T], 32[T]}, {}]

Covered

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)], 30[(r-y < 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 31[T], 32[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)], 32[(-1+n >= 0 /\ r-y >= 0 /\ r-(-1+n)*y-y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T]}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 25[(y > 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {}, {28[T], 30[T], 31[T], 32[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {25[T]}]

Step with 19

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)], 19[(y <= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {25[T]}, {}]

Backtrack

	Trace

	20[T], 22[(x < 0)], 9[(y >= 0)]
	
	Blocked

	[{}, {5[T]}, {24[T]}, {19[T], 25[T]}]

Backtrack

	Trace

	20[T], 22[(x < 0)]
	
	Blocked

	[{}, {5[T]}, {9[T], 24[T]}]

Backtrack

	Trace

	20[T]
	
	Blocked

	[{}, {5[T], 22[T]}]

Backtrack

	Trace

	Blocked

	[{20[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b