unknown

Initial ITS

Start location: [1]
Program variables: x y
   0: [1] -> [2] : x'=nondet, T, cost: 1
   1: [2] -> [3] : y'=nondet1, T, cost: 1
   2: [3] -> [4] : y+x > 0, cost: 1
  15: [3] -> [14] : y+x <= 0, cost: 1
   3: [4] -> [6] : -y+x > 0, cost: 1
   6: [4] -> [8] : -y+x <= 0, cost: 1
  14: [5] -> [3] : T, cost: 1
   4: [6] -> [7] : x'=-1+x, T, cost: 1
   5: [7] -> [5] : T, cost: 1
   7: [8] -> [10] : -y+x == 0, cost: 1
  10: [8] -> [12] : (-y+x < 0 \/ -y+x > 0), cost: 1
  13: [9] -> [5] : T, cost: 1
   8: [10] -> [11] : x'=-1+x, T, cost: 1
   9: [11] -> [9] : T, cost: 1
  11: [12] -> [13] : y'=-1+y, T, cost: 1
  12: [13] -> [9] : T, cost: 1

Chained Linear Paths

Start location: [1]
Program variables: x y
  16: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   2: [3] -> [4] : y+x > 0, cost: 1
  15: [3] -> [14] : y+x <= 0, cost: 1
   6: [4] -> [8] : -y+x <= 0, cost: 1
  18: [4] -> [5] : x'=-1+x, -y+x > 0, cost: 1
  14: [5] -> [3] : T, cost: 1
  21: [8] -> [9] : x'=-1+x, -y+x == 0, cost: 1
  22: [8] -> [9] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
  13: [9] -> [5] : T, 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 [6] by chaining:

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

	First rule:
	[8] -> [12] : (-y+x < 0 \/ -y+x > 0), cost: 1
	Second rule:
	[12] -> [13] : y'=-1+y, T, cost: 1
	New rule:
	[8] -> [13] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
	
	Applied deletion

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

	Applied chaining

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

	Removed the following rules: 9 19
	
	Eliminating location [13] by chaining:

	Applied chaining

	First rule:
	[8] -> [13] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
	Second rule:
	[13] -> [9] : T, cost: 1
	New rule:
	[8] -> [9] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 12 20

Step with 16

	Trace

	16[T]
	
	Blocked

	[{}, {}]

Step with 15

	Trace

	16[T], 15[(y+x <= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {15[T]}]

Step with 2

	Trace

	16[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {}]

Step with 6

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {}, {}]

Step with 21

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}]

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 2

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 6

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}, {}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 22

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

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

Accelerate

Start location: [1]
Program variables: x y
  16: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   2: [3] -> [4] : y+x > 0, cost: 1
  15: [3] -> [14] : y+x <= 0, cost: 1
   6: [4] -> [8] : -y+x <= 0, cost: 1
  18: [4] -> [5] : x'=-1+x, -y+x > 0, cost: 1
  14: [5] -> [3] : T, cost: 1
  21: [8] -> [9] : x'=-1+x, -y+x == 0, cost: 1
  22: [8] -> [9] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
  13: [9] -> [5] : T, cost: 1
  23: [9] -> [9] : y'=-n+y, (1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0), cost: 1

	Loop Acceleration

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

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

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}, {23[T]}]

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}, {23[T]}, {}, {}]

Accelerate

Start location: [1]
Program variables: x y
  16: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   2: [3] -> [4] : y+x > 0, cost: 1
  15: [3] -> [14] : y+x <= 0, cost: 1
  24: [3] -> [3] : x'=-n2+x, y'=-n1*n2+y, (1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0), cost: 1
   6: [4] -> [8] : -y+x <= 0, cost: 1
  18: [4] -> [5] : x'=-1+x, -y+x > 0, cost: 1
  14: [5] -> [3] : T, cost: 1
  21: [8] -> [9] : x'=-1+x, -y+x == 0, cost: 1
  22: [8] -> [9] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
  13: [9] -> [5] : T, cost: 1
  23: [9] -> [9] : y'=-n+y, (1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0), cost: 1

	Loop Acceleration

	Original rule:
	[3] -> [3] : x'=-1+x, y'=-n1+y, (-1+n1 >= 0 /\ 1+y-x >= 0 /\ -n1+y+x > 0 /\ -y+x <= 0 /\ -y+x == 0 /\ 2-n1+y-x > 0 /\ y+x > 0), cost: 1
	New rule:
	[3] -> [3] : x'=-n2+x, y'=-n1*n2+y, (1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0), cost: 1

		-1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0
		
		1+y-x >= 0 [0]: monotonic increase yields 1+y-x >= 0, dependencies: 2-n1+y-x > 0
		
		1+y-x >= 0 [1]: montonic decrease yields n2-n1*(-1+n2)+y-x >= 0, dependencies: y-x >= 0
		
		1+y-x >= 0 [2]: eventual decrease yields (1+y-x >= 0 /\ n2-n1*(-1+n2)+y-x >= 0), dependencies: -1+n1 >= 0
		
		1+y-x >= 0 [3]: eventual increase yields (-1+n1 <= 0 /\ 1+y-x >= 0)
		
		y-x >= 0 [0]: monotonic increase yields y-x >= 0, dependencies: 2-n1+y-x > 0
		
		y-x >= 0 [1]: montonic decrease yields -1+n2-n1*(-1+n2)+y-x >= 0, dependencies: -1+n1 >= 0
		
		y-x >= 0 [2]: eventual increase yields (-1+n1 <= 0 /\ y-x >= 0)
		
		-n1+y+x > 0 [0]: montonic decrease yields 1-n1-n2-n1*(-1+n2)+y+x > 0, dependencies: -1+n1 >= 0
		
		-n1+y+x > 0 [1]: eventual increase yields (-n1+y+x > 0 /\ 1+n1 <= 0), dependencies: -1+n1 >= 0
		
		-y+x >= 0 [0]: monotonic increase yields -y+x >= 0, dependencies: -1+n1 >= 0
		
		2-n1+y-x > 0 [0]: monotonic increase yields 2-n1+y-x > 0, dependencies: -y+x >= 0
		
		y+x > 0 [0]: montonic decrease yields 1-n2-n1*(-1+n2)+y+x > 0, dependencies: -1+n1 >= 0 -n1+y+x > 0
		
		y+x > 0 [1]: eventual increase yields (1+n1 <= 0 /\ y+x > 0), dependencies: -1+n1 >= 0
		
		Replacement map: {-1+n1 >= 0 -> -1+n1 >= 0, 1+y-x >= 0 -> 1+y-x >= 0, y-x >= 0 -> y-x >= 0, -n1+y+x > 0 -> 1-n1-n2-n1*(-1+n2)+y+x > 0, -y+x >= 0 -> -y+x >= 0, 2-n1+y-x > 0 -> 2-n1+y-x > 0, y+x > 0 -> 1-n2-n1*(-1+n2)+y+x > 0}

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

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

Step with 15

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 15[(y+x <= 0)]
	
	Blocked

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

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

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

Step with 2

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

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

Step with 6

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

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

Step with 21

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 2

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {}, {}, {}]

Step with 6

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {}, {}, {}, {}]

Step with 22

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {}, {}, {}, {21[T]}, {}]

Covered

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {}, {}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {}, {}, {6[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {}, {2[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {15[T], 24[T]}, {6[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {15[T]}, {2[T], 15[T], 24[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

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

Step with 2

	Trace

	16[T], 2[(y+x > 0)]
	
	Blocked

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

Step with 6

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

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

Step with 22

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

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

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

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

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T], 14[T]
	
	Blocked

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

Accelerate

Start location: [1]
Program variables: x y
  16: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   2: [3] -> [4] : y+x > 0, cost: 1
  15: [3] -> [14] : y+x <= 0, cost: 1
  24: [3] -> [3] : x'=-n2+x, y'=-n1*n2+y, (1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0), cost: 1
  25: [3] -> [3] : y'=-n4+y, (y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0), cost: 1
   6: [4] -> [8] : -y+x <= 0, cost: 1
  18: [4] -> [5] : x'=-1+x, -y+x > 0, cost: 1
  14: [5] -> [3] : T, cost: 1
  21: [8] -> [9] : x'=-1+x, -y+x == 0, cost: 1
  22: [8] -> [9] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
  13: [9] -> [5] : T, cost: 1
  23: [9] -> [9] : y'=-n+y, (1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0), cost: 1

	Loop Acceleration

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

		y-x > 0 [0]: montonic decrease yields 1-n4+y-x > 0
		
		y-x > 0 [1]: eventual increase yields (1 <= 0 /\ y-x > 0)
		
		y-x >= 0 [0]: monotonic increase yields y-x >= 0, dependencies: y-x > 0
		
		y+x > 0 [0]: montonic decrease yields 1-n4+y+x > 0
		
		y+x > 0 [1]: eventual increase yields (1 <= 0 /\ y+x > 0)
		
		Replacement map: {y-x > 0 -> 1-n4+y-x > 0, y-x >= 0 -> y-x >= 0, y+x > 0 -> 1-n4+y+x > 0}

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

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

Step with 15

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 15[(y+x <= 0)]
	
	Blocked

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

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

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

Step with 2

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

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

Step with 6

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

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

Step with 22

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

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

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

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

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T], 14[T]
	
	Blocked

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

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {}, {13[T]}]

Step with 23

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {22[-y+x < 0]}]

Step with 21

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 25[T]}, {}, {22[T]}, {}, {}, {}]

Accelerate

Start location: [1]
Program variables: x y
  16: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   2: [3] -> [4] : y+x > 0, cost: 1
  15: [3] -> [14] : y+x <= 0, cost: 1
  24: [3] -> [3] : x'=-n2+x, y'=-n1*n2+y, (1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0), cost: 1
  25: [3] -> [3] : y'=-n4+y, (y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0), cost: 1
  26: [3] -> [3] : x'=-n6+x, y'=1-n6+x, (y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0), cost: 1
   6: [4] -> [8] : -y+x <= 0, cost: 1
  18: [4] -> [5] : x'=-1+x, -y+x > 0, cost: 1
  14: [5] -> [3] : T, cost: 1
  21: [8] -> [9] : x'=-1+x, -y+x == 0, cost: 1
  22: [8] -> [9] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
  13: [9] -> [5] : T, cost: 1
  23: [9] -> [9] : y'=-n+y, (1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0), cost: 1

	Loop Acceleration

	Original rule:
	[3] -> [3] : x'=-1+x, y'=x, (y-x >= 0 /\ 1+2*x > 0 /\ 2*x > 0 /\ -1+y-x >= 0), cost: 1
	New rule:
	[3] -> [3] : x'=-n6+x, y'=1-n6+x, (y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0), cost: 1

		y-x >= 0 [0]: monotonic increase yields y-x >= 0
		
		1+2*x > 0 [0]: monotonic increase yields 1+2*x > 0, dependencies: 2*x > 0
		
		1+2*x > 0 [1]: montonic decrease yields 3-2*n6+2*x > 0, dependencies: 2*x > 0
		
		1+2*x > 0 [2]: eventual decrease yields (1+2*x > 0 /\ 3-2*n6+2*x > 0)
		
		1+2*x > 0 [3]: eventual increase yields (1+2*x > 0 /\ 2 <= 0)
		
		2*x > 0 [0]: montonic decrease yields 2-2*n6+2*x > 0
		
		2*x > 0 [1]: eventual increase yields (2*x > 0 /\ 2 <= 0)
		
		-1+y-x >= 0 [0]: monotonic increase yields -1+y-x >= 0
		
		Replacement map: {y-x >= 0 -> y-x >= 0, 1+2*x > 0 -> 1+2*x > 0, 2*x > 0 -> 2-2*n6+2*x > 0, -1+y-x >= 0 -> -1+y-x >= 0}

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {26[T]}]

Step with 2

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {}]

Step with 6

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {}, {}]

Step with 22

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {}, {21[T]}, {}]

Step with 13

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {}, {21[T]}, {}, {}]

Step with 14

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {}, {21[T]}, {}, {}, {}]

Covered

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {}, {21[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {}, {21[T]}, {13[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {15[T], 26[T]}, {6[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 26[T]}]

Step with 25

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {25[T]}]

Acceleration Failed

marked recursive suffix as redundant

Step with 15

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 15[(y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {25[T], 26[T]}, {}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}]

Step with 2

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}]

Step with 6

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}]

Step with 21

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {}]

Covered

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {6[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {2[T], 15[T], 25[T], 26[T]}]

Step with 24

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {2[T], 15[T], 25[T], 26[T]}, {24[T]}]

Covered

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 26[T]}, {2[T], 15[T], 24[T], 25[T], 26[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {15[T], 24[T]}, {2[T], 15[T], 24[T], 25[T], 26[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}]

Step with 25

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {25[T]}]

Step with 26

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {25[T]}, {26[T]}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {25[T], 26[T]}]

Step with 15

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 15[(y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {25[T], 26[T]}, {}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}]

Step with 2

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}]

Step with 6

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}]

Step with 21

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {13[T]}]

Step with 23

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}]

Step with 22

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T]}, {6[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {2[T], 15[T], 25[T], 26[T]}]

Step with 24

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {2[T], 15[T], 25[T], 26[T]}, {24[T]}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 26[T]}, {2[T], 15[T], 24[T], 25[T], 26[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}]

Step with 2

	Trace

	16[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}]

Step with 6

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}]

Step with 22

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {}]

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {}, {}, {}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {13[T]}]

Step with 23

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[-y+x < 0]}]

Step with 21

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {}]

Step with 2

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {}, {}]

Step with 6

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {}, {}, {}]

Step with 22

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {}, {}, {21[T]}, {}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {}, {6[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {2[T]}]

Step with 25

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T]}, {25[T]}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T]}]

Step with 26

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T]}, {26[T]}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 26[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {6[T]}]

Step with 18

	Trace

	16[T], 2[(y+x > 0)], 18[(-y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {6[T]}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 18[(-y+x > 0)], 14[T]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {6[T]}, {}, {}]

Accelerate

Start location: [1]
Program variables: x y
  16: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   2: [3] -> [4] : y+x > 0, cost: 1
  15: [3] -> [14] : y+x <= 0, cost: 1
  24: [3] -> [3] : x'=-n2+x, y'=-n1*n2+y, (1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0), cost: 1
  25: [3] -> [3] : y'=-n4+y, (y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0), cost: 1
  26: [3] -> [3] : x'=-n6+x, y'=1-n6+x, (y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0), cost: 1
  27: [3] -> [3] : x'=-n15+x, (1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0), cost: 1
   6: [4] -> [8] : -y+x <= 0, cost: 1
  18: [4] -> [5] : x'=-1+x, -y+x > 0, cost: 1
  14: [5] -> [3] : T, cost: 1
  21: [8] -> [9] : x'=-1+x, -y+x == 0, cost: 1
  22: [8] -> [9] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
  13: [9] -> [5] : T, cost: 1
  23: [9] -> [9] : y'=-n+y, (1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0), cost: 1

	Loop Acceleration

	Original rule:
	[3] -> [3] : x'=-1+x, (-y+x > 0 /\ y+x > 0), cost: 1
	New rule:
	[3] -> [3] : x'=-n15+x, (1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0), cost: 1

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

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {15[T], 24[T], 25[T], 26[T]}, {27[T]}]

Restart

Step with 16

	Trace

	16[T]
	
	Blocked

	[{}, {}]

Step with 15

	Trace

	16[T], 15[(y+x <= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {15[T]}]

Step with 2

	Trace

	16[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {}]

Step with 18

	Trace

	16[T], 2[(y+x > 0)], 18[(-y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 18[(-y+x > 0)], 14[T]
	
	Blocked

	[{}, {15[T]}, {}, {}, {}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 18[(-y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)]
	
	Blocked

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

Step with 6

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

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

Step with 22

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

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

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

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

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T], 14[T]
	
	Blocked

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

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

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

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

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

Step with 23

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

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

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

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

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

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

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

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

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

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

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[-y+x < 0]}]

Step with 21

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {}]

Step with 2

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {}, {}]

Step with 6

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {}, {}, {}]

Step with 22

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {}, {}, {21[T]}, {}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {}, {6[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {2[T]}]

Step with 25

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {2[T], 24[T], 27[T]}, {25[T]}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 27[T]}]

Step with 26

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 27[T]}, {26[T]}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 26[T], 27[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

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

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

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

Step with 23

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {15[T]}, {18[T]}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {15[T]}, {6[T], 18[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {2[T], 15[T]}]

Step with 26

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {26[T]}]

Step with 2

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {}]

Step with 6

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {}, {}]

Step with 22

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {}, {}, {}]

Step with 13

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {}, {}, {}, {}]

Step with 14

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {}, {}, {}, {}, {}]

Covered

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {}, {}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {}, {}, {13[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {}, {22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {15[T], 26[T]}, {6[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 26[T]}]

Step with 25

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {25[T]}]

Step with 15

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 15[(y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {25[T], 26[T]}, {}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}]

Step with 2

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}]

Step with 6

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {}]

Step with 21

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {}, {}, {}]

Covered

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {15[T], 25[T], 26[T]}, {6[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {2[T], 15[T], 25[T], 26[T]}]

Step with 24

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {2[T], 15[T], 25[T], 26[T]}, {24[T]}]

Covered

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 26[T], 27[T]}, {2[T], 15[T], 24[T], 25[T], 26[T]}]

Backtrack

	Trace

	16[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T]}, {2[T], 15[T], 24[T], 25[T], 26[T], 27[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}]

Step with 24

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {24[T]}]

Step with 15

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 15[(y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {24[T], 25[T], 26[T], 27[T]}, {}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}]

Step with 2

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}]

Step with 6

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}]

Step with 21

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}]

Step with 13

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}]

Step with 14

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {}]

Step with 2

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {}, {}]

Step with 6

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {}, {}, {}]

Step with 22

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {}, {}, {21[T]}, {}]

Covered

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {}, {6[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {2[T]}]

Step with 25

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {2[T], 24[T], 27[T]}, {25[T]}]

Covered

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {2[T], 24[T], 25[T], 27[T]}]

Step with 26

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {2[T], 24[T], 25[T], 27[T]}, {26[T]}]

Covered

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {}, {2[T], 24[T], 25[T], 26[T], 27[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {13[T]}]

Step with 23

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {}, {21[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {15[T], 24[T], 25[T], 26[T], 27[T]}, {6[T]}]

Backtrack

	Trace

	16[T], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 26[T]}, {2[T], 15[T], 24[T], 25[T], 26[T], 27[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}]

Step with 27

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {27[T]}]

Step with 15

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 15[(y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {25[T], 26[T], 27[T]}, {}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}]

Step with 2

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}]

Step with 6

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {}]

Step with 21

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 2

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {}, {}]

Step with 6

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {}, {}, {}]

Step with 22

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {}, {}, {21[T]}, {}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {}, {6[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {2[T]}]

Step with 25

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 27[T]}, {25[T]}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 27[T]}]

Step with 26

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 27[T]}, {26[T]}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 26[T], 27[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {6[T]}]

Step with 18

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 18[(-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {6[T]}, {}]

Step with 14

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 18[(-y+x > 0)], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {6[T]}, {}, {}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 18[(-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {6[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 25[T], 26[T], 27[T]}, {6[T], 18[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {2[T], 15[T], 25[T], 26[T], 27[T]}]

Step with 24

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {2[T], 15[T], 25[T], 26[T], 27[T]}, {24[T]}]

Accelerate

Start location: [1]
Program variables: x y
  16: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   2: [3] -> [4] : y+x > 0, cost: 1
  15: [3] -> [14] : y+x <= 0, cost: 1
  24: [3] -> [3] : x'=-n2+x, y'=-n1*n2+y, (1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0), cost: 1
  25: [3] -> [3] : y'=-n4+y, (y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0), cost: 1
  26: [3] -> [3] : x'=-n6+x, y'=1-n6+x, (y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0), cost: 1
  27: [3] -> [3] : x'=-n15+x, (1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0), cost: 1
  28: [3] -> [3] : x'=-n2+y, y'=-n2+y, (1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0), cost: 1
   6: [4] -> [8] : -y+x <= 0, cost: 1
  18: [4] -> [5] : x'=-1+x, -y+x > 0, cost: 1
  14: [5] -> [3] : T, cost: 1
  21: [8] -> [9] : x'=-1+x, -y+x == 0, cost: 1
  22: [8] -> [9] : y'=-1+y, (-y+x < 0 \/ -y+x > 0), cost: 1
  13: [9] -> [5] : T, cost: 1
  23: [9] -> [9] : y'=-n+y, (1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0), cost: 1

	rule cannot be iterated more than once
	
	made implied equalities explicit

	Original rule:
	[3] -> [3] : x'=-n2+y, y'=-n1*n2+y, (-1+n1 >= 0 /\ -1+n2 >= 0 /\ 2-n1 > 0 /\ 1+2*y > 0 /\ 1-n2-n1*(-1+n2)+2*y > 0 /\ -1-y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+2*y > 0), cost: 1
	New rule:
	[3] -> [3] : x'=-n2+y, y'=-n1*n2+y, (1-n1 == 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 2-n1 > 0 /\ 1+2*y > 0 /\ 1-n2-n1*(-1+n2)+2*y > 0 /\ -1-y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+2*y > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	[3] -> [3] : x'=-n2+y, y'=-n1*n2+y, (1-n1 == 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 2-n1 > 0 /\ 1+2*y > 0 /\ 1-n2-n1*(-1+n2)+2*y > 0 /\ -1-y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+2*y > 0), cost: 1
	New rule:
	[3] -> [3] : x'=-n2+y, y'=-n2+y, (0 >= 0 /\ 0 == 0 /\ 1 > 0 /\ 1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0), cost: 1
	
		propagated equality n1 = 1
		
	Simplified Guard

	Original rule:
	[3] -> [3] : x'=-n2+y, y'=-n2+y, (0 >= 0 /\ 0 == 0 /\ 1 > 0 /\ 1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0), cost: 1
	New rule:
	[3] -> [3] : x'=-n2+y, y'=-n2+y, (1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0), cost: 1

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {28[T]}]

Step with 15

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 15[(y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {28[T]}, {}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}]

Step with 2

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {}]

Step with 6

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {}]

Step with 21

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 2

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {}, {}]

Step with 6

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {}, {}, {}]

Step with 22

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {}, {}, {21[T]}, {}]

Covered

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {}, {6[T]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {2[T]}]

Step with 25

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {2[T], 24[T], 27[T]}, {25[T]}]

Covered

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 27[T]}]

Step with 26

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 27[T]}, {26[T]}]

Covered

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 26[T], 27[T]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {18[T]}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {15[T], 28[T]}, {6[T], 18[T]}]

Backtrack

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {2[T], 15[T], 28[T]}]

Step with 24

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {2[T], 15[T], 26[T], 28[T]}, {24[T]}]

Covered

	Trace

	16[T], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T]}, {2[T], 15[T], 24[T], 26[T], 28[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}]

Step with 27

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {27[T]}]

Step with 28

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 28[(1-2*n2+2*y > 0 /\ -1+n2 >= 0 /\ 2-2*n2+2*y > 0 /\ 1+2*y > 0 /\ -1-y+x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {25[T], 26[T], 27[T]}, {28[T]}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {25[T], 26[T], 27[T], 28[T]}]

Step with 15

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 15[(y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {25[T], 26[T], 27[T], 28[T]}, {}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 2

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}]

Step with 6

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {}]

Step with 21

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {}]

Step with 2

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {}, {}]

Step with 6

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {}, {}, {}]

Step with 22

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {}, {}, {21[T]}, {}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {}, {}, {21[T], 22[-y+x < 0]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {}, {6[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {2[T]}]

Step with 25

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 27[T]}, {25[T]}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 27[T]}]

Step with 26

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 27[T]}, {26[T]}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {}, {2[T], 24[T], 25[T], 26[T], 27[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {6[T]}]

Step with 18

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 18[(-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {6[T]}, {}]

Step with 14

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 18[(-y+x > 0)], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {6[T]}, {}, {}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)], 18[(-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {6[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {15[T], 25[T], 26[T], 27[T], 28[T]}, {6[T], 18[T]}]

Backtrack

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {2[T], 15[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 24

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {2[T], 15[T], 25[T], 26[T], 27[T], 28[T]}, {24[T]}]

Covered

	Trace

	16[T], 27[(1-n15+y+x > 0 /\ -1+n15 >= 0 /\ 1-n15-y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 28[T]}, {2[T], 15[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}]

Step with 25

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {25[T]}]

Step with 26

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 26[(y-x >= 0 /\ -1+n6 >= 0 /\ 1+2*x > 0 /\ 2-2*n6+2*x > 0 /\ -1+y-x >= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {25[T]}, {26[T]}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {25[T], 26[T]}]

Step with 15

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 15[(y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {25[T], 26[T], 28[T]}, {}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}]

Step with 2

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {}]

Step with 6

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}]

Step with 22

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {13[T]}]

Step with 23

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 22[(-y+x < 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[-y+x < 0]}]

Step with 21

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}]

Step with 23

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}]

Step with 13

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {}]

Step with 14

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T], 14[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {}, {}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)], 13[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {23[T]}, {14[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)], 23[(1-n+y-x > 0 /\ y-x >= 0 /\ -1+n >= 0 /\ 1-n+y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {13[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)], 21[(-y+x == 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {22[T]}, {13[T], 23[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {18[T]}, {21[T], 22[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 2[(y+x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {15[T], 25[T], 26[T], 28[T]}, {6[T], 18[T]}]

Backtrack

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {2[T], 15[T], 25[T], 26[T], 28[T]}]

Step with 24

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)], 24[(1-n2-n1*(-1+n2)+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1+y-x >= 0 /\ y-x >= 0 /\ -y+x >= 0 /\ 1-n1-n2-n1*(-1+n2)+y+x > 0 /\ 2-n1+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {2[T], 15[T], 25[T], 26[T], 28[T]}, {24[T]}]

Covered

	Trace

	16[T], 25[(y-x >= 0 /\ 1-n4+y+x > 0 /\ -1+n4 >= 0 /\ 1-n4+y-x > 0)]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 26[T], 27[T], 28[T]}, {2[T], 15[T], 24[T], 25[T], 26[T], 28[T]}]

Backtrack

	Trace

	16[T]
	
	Blocked

	[{}, {2[T], 15[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Backtrack

	Trace

	Blocked

	[{16[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b