unknown

Initial ITS

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

Chained Linear Paths

Start location: [1]
Program variables: a b x y
  14: [1] -> [5] : a'=nondet, b'=nondet1, x'=nondet2, y'=nondet3, T, cost: 1
   4: [5] -> [7] : -b+a == 0, cost: 1
  11: [5] -> [6] : (-b+a < 0 \/ -b+a > 0), cost: 1
  16: [7] -> [6] : (y < 0 /\ x < 0), cost: 1
  18: [7] -> [7] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0 \/ x >= 0), cost: 1

	Eliminating location [2] by chaining:

	Applied chaining

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

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

	Applied chaining

	First rule:
	[1] -> [3] : a'=nondet, b'=nondet1, T, cost: 1
	Second rule:
	[3] -> [4] : x'=nondet2, T, cost: 1
	New rule:
	[1] -> [4] : a'=nondet, b'=nondet1, x'=nondet2, T, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[1] -> [4] : a'=nondet, b'=nondet1, x'=nondet2, T, cost: 1
	Second rule:
	[4] -> [5] : y'=nondet3, T, cost: 1
	New rule:
	[1] -> [5] : a'=nondet, b'=nondet1, x'=nondet2, y'=nondet3, T, cost: 1
	
	Applied deletion

	Removed the following rules: 3 13
	
	Eliminating location [8] by chaining:

	Applied chaining

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

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

	Applied chaining

	First rule:
	[7] -> [11] : (y < 0 /\ x < 0), cost: 1
	Second rule:
	[11] -> [6] : T, cost: 1
	New rule:
	[7] -> [6] : (y < 0 /\ x < 0), cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[7] -> [9] : x'=-1+x-b+a, (y >= 0 \/ x >= 0), cost: 1
	Second rule:
	[9] -> [10] : y'=-1+y+b-a, T, cost: 1
	New rule:
	[7] -> [10] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0 \/ x >= 0), cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[7] -> [10] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0 \/ x >= 0), cost: 1
	Second rule:
	[10] -> [7] : T, cost: 1
	New rule:
	[7] -> [7] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0 \/ x >= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 8 17

Step with 14

	Trace

	14[T]
	
	Blocked

	[{}, {}]

Step with 4

	Trace

	14[T], 4[(-b+a == 0)]
	
	Blocked

	[{}, {}, {}]

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

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

Backtrack

	Trace

	14[T], 4[(-b+a == 0)]
	
	Blocked

	[{}, {}, {16[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {}]

Accelerate

Start location: [1]
Program variables: a b x y
  14: [1] -> [5] : a'=nondet, b'=nondet1, x'=nondet2, y'=nondet3, T, cost: 1
   4: [5] -> [7] : -b+a == 0, cost: 1
  11: [5] -> [6] : (-b+a < 0 \/ -b+a > 0), cost: 1
  16: [7] -> [6] : (y < 0 /\ x < 0), cost: 1
  18: [7] -> [7] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0 \/ x >= 0), cost: 1
  19: [7] -> LoAT_sink : (y >= 0 /\ 1-b+a <= 0), cost: NONTERM
  20: [7] -> [7] : x'=n*a-n*b-n+x, y'=-n*a+y+n*b-n, (y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0), cost: 1

	Certificate of Non-Termination

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

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

	Loop Acceleration

	Original rule:
	[7] -> [7] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0), cost: 1
	New rule:
	[7] -> [7] : x'=n*a-n*b-n+x, y'=-n*a+y+n*b-n, (y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0), cost: 1

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

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {18[y >= 0], 20[T]}]

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

	[{}, {}, {16[T]}, {18[y >= 0], 19[T], 20[T]}, {}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {}]

Accelerate

Start location: [1]
Program variables: a b x y
  14: [1] -> [5] : a'=nondet, b'=nondet1, x'=nondet2, y'=nondet3, T, cost: 1
   4: [5] -> [7] : -b+a == 0, cost: 1
  11: [5] -> [6] : (-b+a < 0 \/ -b+a > 0), cost: 1
  16: [7] -> [6] : (y < 0 /\ x < 0), cost: 1
  18: [7] -> [7] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0 \/ x >= 0), cost: 1
  19: [7] -> LoAT_sink : (y >= 0 /\ 1-b+a <= 0), cost: NONTERM
  20: [7] -> [7] : x'=n*a-n*b-n+x, y'=-n*a+y+n*b-n, (y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0), cost: 1
  21: [7] -> LoAT_sink : (1+b-a <= 0 /\ x >= 0), cost: NONTERM
  22: [7] -> [7] : x'=n2*a-n2*b+x-n2, y'=-n2*a+y+n2*b-n2, (-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0), cost: 1

	Certificate of Non-Termination

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

		x >= 0 [0]: eventual decrease yields (1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)
		
		x >= 0 [1]: eventual increase yields (1+b-a <= 0 /\ x >= 0)
		
		Replacement map: {x >= 0 -> (1+b-a <= 0 /\ x >= 0)}

	Loop Acceleration

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

		x >= 0 [0]: eventual decrease yields (1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)
		
		x >= 0 [1]: eventual increase yields (1+b-a <= 0 /\ x >= 0)
		
		Replacement map: {x >= 0 -> (1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)}

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {18[x >= 0], 22[T]}]

Acceleration Failed

marked recursive suffix as redundant

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {18[x >= 0], 19[T], 21[T], 22[T]}, {}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[x >= 0], 19[T], 21[T], 22[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[x >= 0], 19[T], 21[T], 22[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[(y >= 0 /\ x >= 0)], 19[T], 21[T], 22[T]}]

Step with 20

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[T], 19[T], 21[T], 22[T]}, {20[T]}]

Accelerate

Start location: [1]
Program variables: a b x y
  14: [1] -> [5] : a'=nondet, b'=nondet1, x'=nondet2, y'=nondet3, T, cost: 1
   4: [5] -> [7] : -b+a == 0, cost: 1
  11: [5] -> [6] : (-b+a < 0 \/ -b+a > 0), cost: 1
  16: [7] -> [6] : (y < 0 /\ x < 0), cost: 1
  18: [7] -> [7] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0 \/ x >= 0), cost: 1
  19: [7] -> LoAT_sink : (y >= 0 /\ 1-b+a <= 0), cost: NONTERM
  20: [7] -> [7] : x'=n*a-n*b-n+x, y'=-n*a+y+n*b-n, (y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0), cost: 1
  21: [7] -> LoAT_sink : (1+b-a <= 0 /\ x >= 0), cost: NONTERM
  22: [7] -> [7] : x'=n2*a-n2*b+x-n2, y'=-n2*a+y+n2*b-n2, (-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0), cost: 1
  23: [7] -> [7] : x'=-n21*n5+x+n*n5*a-n*n5*b-n*n5+n21*n5*a-n21*n5*b, y'=-n21*n5+y-n*n5*a+n*n5*b-n*n5-n21*n5*a+n21*n5*b, (1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0), cost: 1

	Loop Acceleration

	Original rule:
	[7] -> [7] : x'=n*a-n*b-n21-n+x-n21*b+n21*a, y'=-n*a+y+n*b-n21-n+n21*b-n21*a, (-1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1-n21+x-(-1+n21)*b+(-1+n21)*a >= 0 /\ 1+y-n21-n+n21*b-n21*a+(-1+n)*b-(-1+n)*a >= 0), cost: 1
	New rule:
	[7] -> [7] : x'=-n21*n5+x+n*n5*a-n*n5*b-n*n5+n21*n5*a-n21*n5*b, y'=-n21*n5+y-n*n5*a+n*n5*b-n*n5-n21*n5*a+n21*n5*b, (1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0), cost: 1

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

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {23[T]}]

Acceleration Failed

marked recursive suffix as redundant

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {19[T], 21[T], 23[T]}, {}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 19[T], 21[T], 23[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 19[T], 21[T], 23[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 23[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 23[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[(y >= 0 /\ x >= 0)], 19[T], 21[T], 23[T]}]

Step with 20

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[T], 19[T], 21[T], 23[T]}, {20[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 23[T]}]

Step with 22

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 23[T]}, {22[T]}]

Accelerate

Start location: [1]
Program variables: a b x y
  14: [1] -> [5] : a'=nondet, b'=nondet1, x'=nondet2, y'=nondet3, T, cost: 1
   4: [5] -> [7] : -b+a == 0, cost: 1
  11: [5] -> [6] : (-b+a < 0 \/ -b+a > 0), cost: 1
  16: [7] -> [6] : (y < 0 /\ x < 0), cost: 1
  18: [7] -> [7] : x'=-1+x-b+a, y'=-1+y+b-a, (y >= 0 \/ x >= 0), cost: 1
  19: [7] -> LoAT_sink : (y >= 0 /\ 1-b+a <= 0), cost: NONTERM
  20: [7] -> [7] : x'=n*a-n*b-n+x, y'=-n*a+y+n*b-n, (y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0), cost: 1
  21: [7] -> LoAT_sink : (1+b-a <= 0 /\ x >= 0), cost: NONTERM
  22: [7] -> [7] : x'=n2*a-n2*b+x-n2, y'=-n2*a+y+n2*b-n2, (-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0), cost: 1
  23: [7] -> [7] : x'=-n21*n5+x+n*n5*a-n*n5*b-n*n5+n21*n5*a-n21*n5*b, y'=-n21*n5+y-n*n5*a+n*n5*b-n*n5-n21*n5*a+n21*n5*b, (1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0), cost: 1
  24: [7] -> [7] : x'=-n2*n9*b-n211*n51*n9*b-n211*n51*n9+n2*n9*a+n211*n51*n9*a+x-n51*n9*n6*b+n51*n9*n6*a-n51*n9*n6-n2*n9, y'=y+n2*n9*b+n211*n51*n9*b-n211*n51*n9-n2*n9*a-n211*n51*n9*a+n51*n9*n6*b-n51*n9*n6*a-n51*n9*n6-n2*n9, (-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0), cost: 1

	Loop Acceleration

	Original rule:
	[7] -> [7] : x'=n2*a-n2*b-n211*n51+n211*n51*a+x-n2+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b, y'=-n2*a+y+n2*b-n211*n51-n211*n51*a-n2-n51*n6*a+n211*n51*b-n51*n6+n51*n6*b, (-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n2 >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ n211*(-1+n51)*a-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b >= 0 /\ 1-n211*n51+n211*n51*a+x-n2+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b-(-1+n2)*b+(-1+n2)*a >= 0), cost: 1
	New rule:
	[7] -> [7] : x'=-n2*n9*b-n211*n51*n9*b-n211*n51*n9+n2*n9*a+n211*n51*n9*a+x-n51*n9*n6*b+n51*n9*n6*a-n51*n9*n6-n2*n9, y'=y+n2*n9*b+n211*n51*n9*b-n211*n51*n9-n2*n9*a-n211*n51*n9*a+n51*n9*n6*b-n51*n9*n6*a-n51*n9*n6-n2*n9, (-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0), cost: 1

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

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T]}, {24[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[y >= 0], 19[T], 20[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[(y >= 0 /\ x >= 0)], 19[T], 20[T], 24[T]}]

Step with 22

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {22[T]}]

Step with 23

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {19[T], 21[T], 22[T]}, {23[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {19[T], 21[T], 22[T], 23[T]}]

Step with 24

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {19[T], 21[T], 22[T], 23[T]}, {24[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {19[T], 21[T], 22[T], 23[T], 24[T]}]

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {19[T], 21[T], 22[T], 23[T], 24[T]}, {}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {16[T], 19[T], 21[T], 22[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {16[T], 19[T], 21[T], 22[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 22[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 22[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {16[T], 18[(y >= 0 /\ x >= 0)], 19[T], 21[T], 22[T], 23[T], 24[T]}]

Step with 20

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {16[T], 18[T], 19[T], 21[T], 22[T], 23[T], 24[T]}, {20[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 24[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 22[T], 23[T], 24[T]}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}]

Step with 23

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {23[T]}]

Step with 24

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {19[T], 21[T], 23[T]}, {24[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {19[T], 21[T], 23[T], 24[T]}]

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {19[T], 21[T], 23[T], 24[T]}, {}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 19[T], 21[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 19[T], 21[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 18[(y >= 0 /\ x >= 0)], 19[T], 21[T], 23[T], 24[T]}]

Step with 20

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 18[T], 19[T], 21[T], 23[T], 24[T]}, {20[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 23[T], 24[T]}]

Step with 22

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 23[T], 24[T]}, {22[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 24[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 22[T], 23[T], 24[T]}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {16[T], 18[T], 19[T], 20[T], 22[T], 23[T], 24[T]}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}]

Step with 22

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {22[T]}]

Step with 23

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {19[T], 21[T], 22[T]}, {23[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {19[T], 21[T], 22[T], 23[T]}]

Step with 24

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {19[T], 21[T], 22[T], 23[T]}, {24[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {19[T], 21[T], 22[T], 23[T], 24[T]}]

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {19[T], 21[T], 22[T], 23[T], 24[T]}, {}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {16[T], 19[T], 21[T], 22[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {16[T], 19[T], 21[T], 22[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 22[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 22[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {16[T], 18[(y >= 0 /\ x >= 0)], 19[T], 21[T], 22[T], 23[T], 24[T]}]

Step with 20

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {16[T], 18[T], 19[T], 21[T], 22[T], 23[T], 24[T]}, {20[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 22[T], 23[T], 24[T]}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}]

Step with 23

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {23[T]}]

Step with 24

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {19[T], 21[T], 23[T]}, {24[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {19[T], 21[T], 23[T], 24[T]}]

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {19[T], 21[T], 23[T], 24[T]}, {}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 19[T], 21[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 19[T], 21[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 18[(y >= 0 /\ x >= 0)], 19[T], 21[T], 23[T], 24[T]}]

Step with 20

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 18[T], 19[T], 21[T], 23[T], 24[T]}, {20[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 23[T], 24[T]}]

Step with 22

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 23[T], 24[T]}, {22[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 22[T], 23[T], 24[T]}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}]

Step with 24

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {24[T]}]

Step with 16

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)], 16[(y < 0 /\ x < 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {19[T], 21[T], 24[T]}, {}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 19[T], 21[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 19[T], 21[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[y >= 0], 19[T], 21[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[(y >= 0 /\ x >= 0)], 19[T], 21[T], 24[T]}]

Step with 20

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)], 20[(y >= 0 /\ 1+y-n+(-1+n)*b-(-1+n)*a >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[T], 19[T], 21[T], 24[T]}, {20[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 24[T]}]

Step with 22

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)], 22[(-1+n2 >= 0 /\ 1+x-n2-(-1+n2)*b+(-1+n2)*a >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 24[T]}, {22[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 22[T], 24[T]}]

Step with 23

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)], 23[(1-n21*(-1+n5)*b+n21*(-1+n5)*a-n21-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-(-1+n21)*b+(-1+n21)*a-n21*(-1+n5) >= 0 /\ -1+n5 >= 0 /\ -n21*(-1+n5)*b+n21*(-1+n5)*a-(-1+n5)*n*b-(-1+n5)*n+(-1+n5)*n*a+x-n21*(-1+n5) >= 0 /\ -1+n21 >= 0 /\ x >= 0 /\ y-n21+n21*b-n21*a >= 0 /\ -1+n >= 0 /\ 1+n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-n-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a+(-1+n)*b-(-1+n)*a-n21*(-1+n5) >= 0 /\ n21*(-1+n5)*b+y-n21*(-1+n5)*a-n21+(-1+n5)*n*b-(-1+n5)*n-(-1+n5)*n*a+n21*b-n21*a-n21*(-1+n5) >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 22[T], 24[T]}, {23[T]}]

Covered

	Trace

	14[T], 4[(-b+a == 0)], 24[(-1+n211 >= 0 /\ 1+n211*(-1+n51)*a-n211-n211*(-1+n51)*b-(-1+n51)*n6-n211*(-1+n51)+x+(-1+n51)*n6*a-(-1+n51)*n6*b+(-1+n211)*a-(-1+n211)*b >= 0 /\ -1+n9 >= 0 /\ -1+n2 >= 0 /\ -(-1+n9)*n51*n6-(-1+n9)*n2-n211*(-1+n9)*n51+x-(-1+n9)*n2*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n6-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -1+n6 >= 0 /\ x >= 0 /\ -(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ 1-n211*(-1+n51)*a-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6+n211*b-(-1+n6)*a+(-1+n6)*b-n211*(-1+n51)-(-1+n51)*n6*a+(-1+n51)*n6*b-n6 >= 0 /\ -(-1+n9)*n51*n6-n211*a-n211+y-(-1+n9)*n2+n211*b-n211*(-1+n9)*n51+(-1+n9)*n2*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0 /\ -n211*a-n211+y+n211*b >= 0 /\ 1-(-1+n9)*n51*n6-n211*n51-(-1+n9)*n2-n211*(-1+n9)*n51+n211*n51*a+x-n2+n51*n6*a-(-1+n9)*n2*b-n211*n51*b-n51*n6-n51*n6*b+(-1+n9)*n2*a-(-1+n2)*b+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b+(-1+n2)*a+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -1+n51 >= 0 /\ -n211*n51+n211*n51*a+x+n51*n6*a-n211*n51*b-n51*n6-n51*n6*b >= 0 /\ 1+n211*(-1+n51)*a-(-1+n9)*n51*n6-n211-n211*(-1+n51)*b-(-1+n51)*n6-(-1+n9)*n2-n211*(-1+n51)-n211*(-1+n9)*n51+x+(-1+n51)*n6*a-(-1+n9)*n2*b-(-1+n51)*n6*b+(-1+n9)*n2*a+(-1+n211)*a+n211*(-1+n9)*n51*a-(-1+n9)*n51*n6*b-(-1+n211)*b+(-1+n9)*n51*n6*a-n211*(-1+n9)*n51*b >= 0 /\ -n211*(-1+n51)*a-(-1+n9)*n51*n6-n211*a-n211+n211*(-1+n51)*b+y-(-1+n51)*n6-(-1+n9)*n2+n211*b-n211*(-1+n51)-n211*(-1+n9)*n51-(-1+n51)*n6*a+(-1+n9)*n2*b+(-1+n51)*n6*b-(-1+n9)*n2*a-n211*(-1+n9)*n51*a+(-1+n9)*n51*n6*b-(-1+n9)*n51*n6*a+n211*(-1+n9)*n51*b >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T]}, {16[T], 18[T], 19[T], 20[T], 21[T], 22[T], 23[T], 24[T]}]

Backtrack

	Trace

	14[T], 4[(-b+a == 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 18[(y >= 0)]
	
	Blocked

	[{}, {}, {16[T], 20[T], 22[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)]
	
	Blocked

	[{}, {}, {16[T], 18[y >= 0], 20[T], 22[T], 23[T], 24[T]}]

Step with 18

	Trace

	14[T], 4[(-b+a == 0)], 18[(x >= 0)]
	
	Blocked

	[{}, {}, {16[T], 18[y >= 0], 20[T], 22[T], 23[T], 24[T]}, {}]

Covered

	Trace

	14[T], 4[(-b+a == 0)]
	
	Blocked

	[{}, {}, {16[T], 18[(y >= 0 /\ x >= 0)], 20[T], 22[T], 23[T], 24[T]}]

Backtrack

	Trace

	14[T]
	
	Blocked

	[{}, {4[T]}]

Step with 11

	Trace

	14[T], 11[(-b+a > 0)]
	
	Blocked

	[{}, {4[T]}, {}]

Backtrack

	Trace

	14[T]
	
	Blocked

	[{}, {4[T], 11[-b+a > 0]}]

Step with 11

	Trace

	14[T], 11[(-b+a < 0)]
	
	Blocked

	[{}, {4[T], 11[-b+a > 0]}, {}]

Backtrack

	Trace

	14[T]
	
	Blocked

	[{}, {4[T], 11[(-b+a < 0 /\ -b+a > 0)]}]

Backtrack

	Trace

	Blocked

	[{14[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b