unknown

Initial ITS

Start location: [1]
Program variables: x y
   0: [1] -> [2] : x'=nondet, T, cost: 1
   1: [2] -> [3] : y'=nondet1, T, cost: 1
   2: [3] -> [4] : -y+x > 0, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
   3: [4] -> [5] : x'=y-x, T, cost: 1
   4: [5] -> [6] : y'=1+y, T, cost: 1
   5: [6] -> [3] : T, cost: 1

Chained Linear Paths

Start location: [1]
Program variables: x y
   7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
  10: [3] -> [3] : x'=y-x, y'=1+y, -y+x > 0, cost: 1

	Eliminating location [2] by chaining:

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

	Removed the following rules: 5 9

Unrolled Loops

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

	Unrolling

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

Step with 7

	Trace

	7[T]
	
	Blocked

	[{}, {}]

Step with 6

	Trace

	7[T], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	7[T]
	
	Blocked

	[{}, {6[T]}]

Step with 10

	Trace

	7[T], 10[(-y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {}]

Accelerate

Start location: [1]
Program variables: x y
   7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
  10: [3] -> [3] : x'=y-x, y'=1+y, -y+x > 0, cost: 1
  11: [3] -> [3] : x'=1+x, y'=2+y, (-1-x > 0 /\ -y+x > 0), cost: 1
  12: [3] -> [3] : x'=n+x, y'=2*n+y, (-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0), cost: 1

	unrolling

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

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

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

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {10[T], 12[T]}]

Step with 6

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {6[T]}, {10[T], 12[T]}, {}]

Backtrack

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 12[T]}]

Step with 11

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 12[T]}, {}]

Accelerate

Start location: [1]
Program variables: x y
   7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
  10: [3] -> [3] : x'=y-x, y'=1+y, -y+x > 0, cost: 1
  11: [3] -> [3] : x'=1+x, y'=2+y, (-1-x > 0 /\ -y+x > 0), cost: 1
  12: [3] -> [3] : x'=n+x, y'=2*n+y, (-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0), cost: 1
  13: [3] -> [3] : x'=n2+x, y'=2*n2+y, (-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0), cost: 1

	Loop Acceleration

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

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

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 12[T]}, {11[T], 13[T]}]

Accelerate

Start location: [1]
Program variables: x y
   7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
  10: [3] -> [3] : x'=y-x, y'=1+y, -y+x > 0, cost: 1
  11: [3] -> [3] : x'=1+x, y'=2+y, (-1-x > 0 /\ -y+x > 0), cost: 1
  12: [3] -> [3] : x'=n+x, y'=2*n+y, (-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0), cost: 1
  13: [3] -> [3] : x'=n2+x, y'=2*n2+y, (-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0), cost: 1
  14: [3] -> [3] : x'=n1*n3+n2*n3+x, y'=2*n1*n3+2*n2*n3+y, (-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0), cost: 1

	Loop Acceleration

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

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

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T]}, {14[T]}]

Step with 6

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {6[T]}, {14[T]}, {}]

Backtrack

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 14[T]}]

Step with 10

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 10[(-y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 14[T]}, {}]

Covered

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 14[T]}]

Step with 11

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 14[T]}, {}]

Covered

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 14[T]}]

Step with 12

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 14[T]}, {12[T]}]

Accelerate

Start location: [1]
Program variables: x y
   7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
  10: [3] -> [3] : x'=y-x, y'=1+y, -y+x > 0, cost: 1
  11: [3] -> [3] : x'=1+x, y'=2+y, (-1-x > 0 /\ -y+x > 0), cost: 1
  12: [3] -> [3] : x'=n+x, y'=2*n+y, (-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0), cost: 1
  13: [3] -> [3] : x'=n2+x, y'=2*n2+y, (-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0), cost: 1
  14: [3] -> [3] : x'=n1*n3+n2*n3+x, y'=2*n1*n3+2*n2*n3+y, (-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0), cost: 1
  15: [3] -> [3] : x'=n5*n31*n11+n5*n22*n31+n5*n+x, y'=2*n5*n31*n11+2*n5*n22*n31+2*n5*n+y, (1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0), cost: 1

	Loop Acceleration

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

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

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

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

Step with 6

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)], 6[(-y+x <= 0)]
	
	Blocked

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

Backtrack

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

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

Step with 10

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)], 10[(-y+x > 0)]
	
	Blocked

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

Covered

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

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

Step with 11

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

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

Covered

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 15[T]}]

Step with 12

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 15[T]}, {12[T]}]

Covered

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 15[T]}]

Step with 13

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 15[T]}, {13[T]}]

Covered

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 15[T]}]

Step with 14

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 15[T]}, {14[T]}]

Covered

	Trace

	7[T], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}]

Backtrack

	Trace

	7[T]
	
	Blocked

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

Step with 14

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

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

Step with 15

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

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

Covered

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

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

Step with 6

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 6[(-y+x <= 0)]
	
	Blocked

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

Backtrack

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

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

Step with 10

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 10[(-y+x > 0)]
	
	Blocked

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

Covered

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

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

Step with 11

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

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

Covered

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 14[T], 15[T]}]

Step with 12

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 14[T], 15[T]}, {12[T]}]

Covered

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T]}]

Step with 13

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T]}, {13[T]}]

Covered

	Trace

	7[T], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}]

Backtrack

	Trace

	7[T]
	
	Blocked

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

Step with 13

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

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

Step with 14

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

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

Accelerate

Start location: [1]
Program variables: x y
   7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
  10: [3] -> [3] : x'=y-x, y'=1+y, -y+x > 0, cost: 1
  11: [3] -> [3] : x'=1+x, y'=2+y, (-1-x > 0 /\ -y+x > 0), cost: 1
  12: [3] -> [3] : x'=n+x, y'=2*n+y, (-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0), cost: 1
  13: [3] -> [3] : x'=n2+x, y'=2*n2+y, (-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0), cost: 1
  14: [3] -> [3] : x'=n1*n3+n2*n3+x, y'=2*n1*n3+2*n2*n3+y, (-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0), cost: 1
  15: [3] -> [3] : x'=n5*n31*n11+n5*n22*n31+n5*n+x, y'=2*n5*n31*n11+2*n5*n22*n31+2*n5*n+y, (1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0), cost: 1
  16: [3] -> [3] : x'=n10*n2*n3+n10*n1*n3+n10*n27+x, y'=2*n10*n2*n3+2*n10*n1*n3+2*n10*n27+y, (-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0), cost: 1

	Loop Acceleration

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

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

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

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

Step with 6

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 6[(-y+x <= 0)]
	
	Blocked

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

Backtrack

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

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

Step with 10

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 10[(-y+x > 0)]
	
	Blocked

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

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 16[T]}]

Step with 11

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 16[T]}, {}]

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 16[T]}]

Step with 12

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 16[T]}, {12[T]}]

Accelerate

Start location: [1]
Program variables: x y
   7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
  10: [3] -> [3] : x'=y-x, y'=1+y, -y+x > 0, cost: 1
  11: [3] -> [3] : x'=1+x, y'=2+y, (-1-x > 0 /\ -y+x > 0), cost: 1
  12: [3] -> [3] : x'=n+x, y'=2*n+y, (-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0), cost: 1
  13: [3] -> [3] : x'=n2+x, y'=2*n2+y, (-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0), cost: 1
  14: [3] -> [3] : x'=n1*n3+n2*n3+x, y'=2*n1*n3+2*n2*n3+y, (-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0), cost: 1
  15: [3] -> [3] : x'=n5*n31*n11+n5*n22*n31+n5*n+x, y'=2*n5*n31*n11+2*n5*n22*n31+2*n5*n+y, (1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0), cost: 1
  16: [3] -> [3] : x'=n10*n2*n3+n10*n1*n3+n10*n27+x, y'=2*n10*n2*n3+2*n10*n1*n3+2*n10*n27+y, (-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0), cost: 1
  17: [3] -> [3] : x'=n271*n17*n101+n17*n+n17*n35*n101*n29+n15*n17*n35*n101+x, y'=2*n271*n17*n101+2*n17*n+2*n17*n35*n101*n29+2*n15*n17*n35*n101+y, (-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0), cost: 1

	Loop Acceleration

	Original rule:
	[3] -> [3] : x'=n271*n101+n15*n35*n101+n35*n101*n29+n+x, y'=2*n271*n101+2*n15*n35*n101+2*n35*n101*n29+2*n+y, (-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ 1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 /\ -1+n15 >= 0 /\ -n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ 1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-x > 0 /\ 1-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0 /\ -1+n >= 0 /\ -1+n101 >= 0), cost: 1
	New rule:
	[3] -> [3] : x'=n271*n17*n101+n17*n+n17*n35*n101*n29+n15*n17*n35*n101+x, y'=2*n271*n17*n101+2*n17*n+2*n17*n35*n101*n29+2*n15*n17*n35*n101+y, (-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0), cost: 1

		-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 [0]: montonic decrease yields -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0, dependencies: -n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0 -1+n >= 0
		
		-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 [1]: eventual decrease yields (-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0)
		
		-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 [2]: eventual increase yields (-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ n271*n101+n15*n35*n101+n35*n101*n29+n <= 0)
		
		-1+n271 >= 0 [0]: monotonic increase yields -1+n271 >= 0
		
		1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 [0]: montonic decrease yields 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0, dependencies: -1+n271 >= 0 -1+n15 >= 0 -1+n29 >= 0 -1+n35 >= 0 -1+n >= 0 -1+n101 >= 0
		
		1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 [1]: eventual decrease yields (1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0)
		
		1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 [2]: eventual increase yields (1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 /\ n271*n101+n15*n35*n101+n35*n101*n29+n <= 0)
		
		-1+n15 >= 0 [0]: monotonic increase yields -1+n15 >= 0
		
		-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 [0]: montonic decrease yields -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0, dependencies: -n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 -1+n29 >= 0
		
		-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 [1]: eventual decrease yields (-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0)
		
		-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 [2]: eventual increase yields (n271*n101+n15*n35*n101+n35*n101*n29+n <= 0 /\ -n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0)
		
		1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 [0]: montonic decrease yields 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0, dependencies: 1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 -1+n29 >= 0 -1+n >= 0
		
		1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 [1]: eventual decrease yields (1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0)
		
		1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 [2]: eventual increase yields (n271*n101+n15*n35*n101+n35*n101*n29+n <= 0 /\ 1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0)
		
		-1+n29 >= 0 [0]: monotonic increase yields -1+n29 >= 0
		
		1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 [0]: montonic decrease yields 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0, dependencies: 1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 -1+n >= 0
		
		1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 [1]: eventual decrease yields (1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ 1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0)
		
		1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 [2]: eventual increase yields (n271*n101+n15*n35*n101+n35*n101*n29+n <= 0 /\ 1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0)
		
		-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-x > 0 [0]: montonic decrease yields -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0, dependencies: -1+n15 >= 0 -1+n29 >= 0 -1+n35 >= 0 -n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0 -1+n >= 0
		
		-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-x > 0 [1]: eventual decrease yields (-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-x > 0)
		
		-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-x > 0 [2]: eventual increase yields (n271*n101+n15*n35*n101+n35*n101*n29+n <= 0 /\ -n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-x > 0)
		
		1-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-y+x > 0 [0]: montonic decrease yields 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0, dependencies: 1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 -1+n15 >= 0 -1+n29 >= 0 -1+n35 >= 0 -1+n >= 0
		
		1-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-y+x > 0 [1]: eventual decrease yields (1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ 1-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-y+x > 0)
		
		1-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-y+x > 0 [2]: eventual increase yields (n271*n101+n15*n35*n101+n35*n101*n29+n <= 0 /\ 1-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-y+x > 0)
		
		-1+n35 >= 0 [0]: monotonic increase yields -1+n35 >= 0
		
		-n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0 [0]: montonic decrease yields -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0, dependencies: -1+n271 >= 0 -1+n15 >= 0 -1+n29 >= 0 -1+n35 >= 0 -1+n >= 0 -1+n101 >= 0
		
		-n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0 [1]: eventual decrease yields (-n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)
		
		-n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0 [2]: eventual increase yields (n271*n101+n15*n35*n101+n35*n101*n29+n <= 0 /\ -n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0)
		
		-1+n >= 0 [0]: monotonic increase yields -1+n >= 0
		
		-1+n101 >= 0 [0]: monotonic increase yields -1+n101 >= 0
		
		Replacement map: {-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 -> -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0, -1+n271 >= 0 -> -1+n271 >= 0, 1-n271*n101-n15*n35*n101-n35*n101*n29-n-y+x > 0 -> 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0, -1+n15 >= 0 -> -1+n15 >= 0, -n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 -> -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0, 1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 -> 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0, -1+n29 >= 0 -> -1+n29 >= 0, 1-n271-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 -> 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0, -n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-x > 0 -> -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0, 1-n271-n271*(-1+n101)-n15*n35*(-1+n101)-n35*n29*(-1+n101)-y+x > 0 -> 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0, -1+n35 >= 0 -> -1+n35 >= 0, -n271*n101-n15*n35*n101-n35*n101*n29-n-x > 0 -> -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0, -1+n >= 0 -> -1+n >= 0, -1+n101 >= 0 -> -1+n101 >= 0}

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

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

Step with 6

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)], 6[(-y+x <= 0)]
	
	Blocked

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

Backtrack

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

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

Step with 10

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)], 10[(-y+x > 0)]
	
	Blocked

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

Covered

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 17[T]}]

Step with 11

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 17[T]}, {}]

Covered

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 17[T]}]

Step with 12

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 17[T]}, {12[T]}]

Covered

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 17[T]}]

Step with 13

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 17[T]}, {13[T]}]

Covered

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 17[T]}]

Step with 14

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 17[T]}, {14[T]}]

Covered

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 17[T]}]

Step with 15

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 17[T]}, {15[T]}]

Covered

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 17[T]}]

Step with 16

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 17[T]}, {16[T]}]

Covered

	Trace

	7[T], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Backtrack

	Trace

	7[T]
	
	Blocked

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

Step with 16

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {16[T]}]

Step with 17

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {16[T]}, {17[T]}]

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {16[T], 17[T]}]

Step with 6

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {16[T], 17[T]}, {}]

Backtrack

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 16[T], 17[T]}]

Step with 10

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 10[(-y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 16[T], 17[T]}, {}]

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 16[T], 17[T]}]

Step with 11

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 16[T], 17[T]}, {}]

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 16[T], 17[T]}]

Step with 12

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 16[T], 17[T]}, {12[T]}]

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 16[T], 17[T]}]

Step with 13

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 16[T], 17[T]}, {13[T]}]

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 16[T], 17[T]}]

Step with 14

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 16[T], 17[T]}, {14[T]}]

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 16[T], 17[T]}]

Step with 15

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 16[T], 17[T]}, {15[T]}]

Covered

	Trace

	7[T], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Backtrack

	Trace

	7[T]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 10

	Trace

	7[T], 10[(-y+x > 0)]
	
	Blocked

	[{}, {6[T], 14[T], 15[T], 16[T], 17[T]}, {}]

Covered

	Trace

	7[T]
	
	Blocked

	[{}, {6[T], 10[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 11

	Trace

	7[T], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 14[T], 15[T], 16[T], 17[T]}, {}]

Covered

	Trace

	7[T]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 12

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T]}]

Step with 13

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T]}, {13[T]}]

Covered

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T]}]

Step with 14

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T]}, {14[T]}]

Covered

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T]}]

Step with 15

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T]}, {15[T]}]

Covered

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T]}]

Step with 16

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T]}, {16[T]}]

Covered

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T], 16[T]}]

Step with 17

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T], 16[T]}, {17[T]}]

Covered

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 6

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}]

Backtrack

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 10

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 10[(-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}]

Covered

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 11

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}]

Covered

	Trace

	7[T], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Backtrack

	Trace

	7[T]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 13

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T]}]

Step with 14

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T]}, {14[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T]}]

Step with 15

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T]}, {15[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T]}]

Step with 16

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T]}, {16[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T], 16[T]}]

Step with 17

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T], 16[T]}, {17[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 6

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T], 16[T], 17[T]}, {}]

Backtrack

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 10

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 10[(-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 11

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 13[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 12

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {12[T]}]

Accelerate

Start location: [1]
Program variables: x y
   7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
   6: [3] -> [7] : -y+x <= 0, cost: 1
  10: [3] -> [3] : x'=y-x, y'=1+y, -y+x > 0, cost: 1
  11: [3] -> [3] : x'=1+x, y'=2+y, (-1-x > 0 /\ -y+x > 0), cost: 1
  12: [3] -> [3] : x'=n+x, y'=2*n+y, (-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0), cost: 1
  13: [3] -> [3] : x'=n2+x, y'=2*n2+y, (-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0), cost: 1
  14: [3] -> [3] : x'=n1*n3+n2*n3+x, y'=2*n1*n3+2*n2*n3+y, (-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0), cost: 1
  15: [3] -> [3] : x'=n5*n31*n11+n5*n22*n31+n5*n+x, y'=2*n5*n31*n11+2*n5*n22*n31+2*n5*n+y, (1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0), cost: 1
  16: [3] -> [3] : x'=n10*n2*n3+n10*n1*n3+n10*n27+x, y'=2*n10*n2*n3+2*n10*n1*n3+2*n10*n27+y, (-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0), cost: 1
  17: [3] -> [3] : x'=n271*n17*n101+n17*n+n17*n35*n101*n29+n15*n17*n35*n101+x, y'=2*n271*n17*n101+2*n17*n+2*n17*n35*n101*n29+2*n15*n17*n35*n101+y, (-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0), cost: 1
  18: [3] -> [3] : x'=n47*n+n47*n219+x, y'=2*n47*n+2*n47*n219+y, (-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0), cost: 1

	Loop Acceleration

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

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

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {18[T]}]

Step with 6

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {18[T]}, {}]

Backtrack

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 18[T]}]

Step with 10

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 10[(-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 18[T]}, {}]

Covered

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 18[T]}]

Step with 11

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 18[T]}, {}]

Covered

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 18[T]}]

Step with 12

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 18[T]}, {12[T]}]

Covered

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 18[T]}]

Step with 13

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 18[T]}, {13[T]}]

Covered

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 18[T]}]

Step with 14

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 18[T]}, {14[T]}]

Covered

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 18[T]}]

Step with 15

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 18[T]}, {15[T]}]

Covered

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 18[T]}]

Step with 16

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 18[T]}, {16[T]}]

Covered

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 18[T]}]

Step with 17

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 18[T]}, {17[T]}]

Covered

	Trace

	7[T], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}]

Backtrack

	Trace

	7[T]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}]

Step with 13

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T]}]

Step with 14

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 14[(-1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-n2-y+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-x > 0 /\ 1-n1-n2*(-1+n3)-n1*(-1+n3)-y+x > 0 /\ -1+n3 >= 0 /\ -n1-n2*(-1+n3)-n1*(-1+n3)-n2-x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T]}, {14[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T]}]

Step with 15

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 15[(1-(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -1+n5 >= 0 /\ 1-(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-y+x-n22*n31 > 0 /\ -1+n22 >= 0 /\ -(-1+n5)*n-n22-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ -(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-x > 0 /\ 1-(-1+n5)*n-(-1+n5)*n31*n11-(-1+n5)*n22*n31-n11*(-1+n31)-n11-n22*(-1+n31)-y+x > 0 /\ -(-1+n5)*n-n-n31*n11-(-1+n5)*n31*n11-(-1+n5)*n22*n31-x-n22*n31 > 0 /\ -1+n11 >= 0 /\ -1+n >= 0 /\ -1+n31 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T]}, {15[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T]}]

Step with 16

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 16[(-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-n27-x > 0 /\ -1+n2 >= 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-y-n27+x > 0 /\ 1-n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-y-n27+x > 0 /\ -1+n10 >= 0 /\ 1-(-1+n10)*n2*n3-n1*(-1+n10)*n3-(-1+n10)*n27-y-n27+x > 0 /\ -1+n1 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n27-x > 0 /\ -1+n27 >= 0 /\ -n1-n2*(-1+n3)-(-1+n10)*n2*n3-n1*(-1+n10)*n3-n1*(-1+n3)-(-1+n10)*n27-n2-n27-x > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T]}, {16[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T]}]

Step with 17

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 17[(-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-x > 0 /\ -1+n271 >= 0 /\ -1+n15 >= 0 /\ 1-n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-y+x > 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-y+x > 0 /\ -1+n29 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-n29-y+x > 0 /\ -n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-x > 0 /\ -1+n17 >= 0 /\ 1-n271-n271*n101*(-1+n17)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-y+x > 0 /\ -1+n35 >= 0 /\ -1+n >= 0 /\ -1+n101 >= 0 /\ -n271-n271*n101*(-1+n17)-n15-n29*(-1+n35)-n271*(-1+n101)-n15*n35*n101*(-1+n17)-n*(-1+n17)-n15*n35*(-1+n101)-n35*n101*(-1+n17)*n29-n35*n29*(-1+n101)-n15*(-1+n35)-x > 0 /\ -n271*n101-n15*n35*n101-n271*n101*(-1+n17)-n35*n101*n29-n15*n35*n101*(-1+n17)-n*(-1+n17)-n-n35*n101*(-1+n17)*n29-x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T]}, {17[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T], 17[T]}]

Step with 18

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 18[(-n*(-1+n47)-n219*(-1+n47)-n219-n-x > 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-n-y+x > 0 /\ -n*(-1+n47)-n219*(-1+n47)-n219-x > 0 /\ -n219-x > 0 /\ -1+n47 >= 0 /\ 1-n*(-1+n47)-n219*(-1+n47)-n219-y+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T], 17[T]}, {18[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}]

Step with 6

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 6[(-y+x <= 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {}]

Backtrack

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}]

Step with 10

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 10[(-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}]

Step with 11

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 11[(-1-x > 0 /\ -y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 11[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}]

Step with 12

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)], 12[(-n-x > 0 /\ -1+n >= 0 /\ 1-n-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 11[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {12[T]}]

Covered

	Trace

	7[T], 13[(-1+n2 >= 0 /\ -n2-x > 0 /\ 1-n2-y+x > 0)]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}]

Backtrack

	Trace

	7[T]
	
	Blocked

	[{}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}]

Backtrack

	Trace

	Blocked

	[{7[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b