unknown

Initial ITS

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

Chained Linear Paths

Start location: [1]
Program variables: a b c i j m n
  18: [1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
  12: [8] -> [13] : (-n+j >= 0 /\ -m+i >= 0), cost: 1
  22: [8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1

	Eliminating location [2] by chaining:

	Applied chaining

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

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

	Applied chaining

	First rule:
	[1] -> [3] : i'=nondet, j'=nondet1, T, cost: 1
	Second rule:
	[3] -> [4] : m'=nondet2, T, cost: 1
	New rule:
	[1] -> [4] : i'=nondet, j'=nondet1, m'=nondet2, T, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[1] -> [4] : i'=nondet, j'=nondet1, m'=nondet2, T, cost: 1
	Second rule:
	[4] -> [5] : n'=nondet3, T, cost: 1
	New rule:
	[1] -> [5] : i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[1] -> [5] : i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
	Second rule:
	[5] -> [6] : a'=i, T, cost: 1
	New rule:
	[1] -> [6] : a'=nondet, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[1] -> [6] : a'=nondet, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
	Second rule:
	[6] -> [7] : b'=j, T, cost: 1
	New rule:
	[1] -> [7] : a'=nondet, b'=nondet1, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[1] -> [7] : a'=nondet, b'=nondet1, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
	Second rule:
	[7] -> [8] : c'=0, T, cost: 1
	New rule:
	[1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[8] -> [9] : (-n+j < 0 \/ -m+i < 0), cost: 1
	Second rule:
	[9] -> [10] : i'=1+i, T, cost: 1
	New rule:
	[8] -> [10] : i'=1+i, (-n+j < 0 \/ -m+i < 0), cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[8] -> [10] : i'=1+i, (-n+j < 0 \/ -m+i < 0), cost: 1
	Second rule:
	[10] -> [11] : j'=1+j, T, cost: 1
	New rule:
	[8] -> [11] : i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[8] -> [11] : i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
	Second rule:
	[11] -> [12] : c'=1+c, T, cost: 1
	New rule:
	[8] -> [12] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[8] -> [12] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
	Second rule:
	[12] -> [8] : T, cost: 1
	New rule:
	[8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
	
	Applied deletion

	Removed the following rules: 11 21

Step with 18

	Trace

	18[T]
	
	Blocked

	[{}, {}]

Step with 12

	Trace

	18[T], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {12[T]}]

Step with 22

	Trace

	18[T], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T]}, {}]

Accelerate

Start location: [1]
Program variables: a b c i j m n
  18: [1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
  12: [8] -> [13] : (-n+j >= 0 /\ -m+i >= 0), cost: 1
  22: [8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
  23: [8] -> [8] : c'=c+n4, i'=n4+i, j'=n4+j, (-1+n4 >= 0 /\ 1+m-n4-i > 0), cost: 1

	Loop Acceleration

	Original rule:
	[8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-m+i < 0), cost: 1
	New rule:
	[8] -> [8] : c'=c+n4, i'=n4+i, j'=n4+j, (-1+n4 >= 0 /\ 1+m-n4-i > 0), cost: 1

		m-i > 0 [0]: montonic decrease yields 1+m-n4-i > 0
		
		m-i > 0 [1]: eventual increase yields (1 <= 0 /\ m-i > 0)
		
		Replacement map: {m-i > 0 -> 1+m-n4-i > 0}

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T]}, {22[-m+i < 0], 23[T]}]

Step with 12

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T]}, {22[-m+i < 0], 23[T]}, {}]

Backtrack

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[-m+i < 0], 23[T]}]

Step with 22

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[-m+i < 0], 23[T]}, {}]

Accelerate

Start location: [1]
Program variables: a b c i j m n
  18: [1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
  12: [8] -> [13] : (-n+j >= 0 /\ -m+i >= 0), cost: 1
  22: [8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
  23: [8] -> [8] : c'=c+n4, i'=n4+i, j'=n4+j, (-1+n4 >= 0 /\ 1+m-n4-i > 0), cost: 1
  24: [8] -> [8] : c'=c+n8, i'=n8+i, j'=n8+j, (-1+n8 >= 0 /\ 1+n-n8-j > 0), cost: 1

	Loop Acceleration

	Original rule:
	[8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0), cost: 1
	New rule:
	[8] -> [8] : c'=c+n8, i'=n8+i, j'=n8+j, (-1+n8 >= 0 /\ 1+n-n8-j > 0), cost: 1

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

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[-m+i < 0], 23[T]}, {22[-n+j < 0], 24[T]}]

Accelerate

Start location: [1]
Program variables: a b c i j m n
  18: [1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
  12: [8] -> [13] : (-n+j >= 0 /\ -m+i >= 0), cost: 1
  22: [8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
  23: [8] -> [8] : c'=c+n4, i'=n4+i, j'=n4+j, (-1+n4 >= 0 /\ 1+m-n4-i > 0), cost: 1
  24: [8] -> [8] : c'=c+n8, i'=n8+i, j'=n8+j, (-1+n8 >= 0 /\ 1+n-n8-j > 0), cost: 1
  25: [8] -> [8] : c'=c+n10*n41+n10*n8, i'=n10*n41+i+n10*n8, j'=n10*n41+j+n10*n8, (-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0), cost: 1

	Loop Acceleration

	Original rule:
	[8] -> [8] : c'=c+n41+n8, i'=n41+n8+i, j'=n41+n8+j, (-1+n41 >= 0 /\ 1+m-n41-i > 0 /\ -1+n8 >= 0 /\ 1+n-n41-n8-j > 0), cost: 1
	New rule:
	[8] -> [8] : c'=c+n10*n41+n10*n8, i'=n10*n41+i+n10*n8, j'=n10*n41+j+n10*n8, (-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0), cost: 1

		-1+n41 >= 0 [0]: monotonic increase yields -1+n41 >= 0
		
		1+m-n41-i > 0 [0]: montonic decrease yields 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0, dependencies: -1+n41 >= 0 -1+n8 >= 0
		
		1+m-n41-i > 0 [1]: eventual decrease yields (1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ 1+m-n41-i > 0)
		
		1+m-n41-i > 0 [2]: eventual increase yields (n41+n8 <= 0 /\ 1+m-n41-i > 0)
		
		-1+n8 >= 0 [0]: monotonic increase yields -1+n8 >= 0
		
		1+n-n41-n8-j > 0 [0]: montonic decrease yields 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0, dependencies: -1+n41 >= 0 -1+n8 >= 0
		
		1+n-n41-n8-j > 0 [1]: eventual increase yields (n41+n8 <= 0 /\ 1+n-n41-n8-j > 0)
		
		Replacement map: {-1+n41 >= 0 -> -1+n41 >= 0, 1+m-n41-i > 0 -> 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0, -1+n8 >= 0 -> -1+n8 >= 0, 1+n-n41-n8-j > 0 -> 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0}

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T]}, {25[T]}]

Step with 12

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T]}, {25[T]}, {}]

Backtrack

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 25[T]}]

Step with 22

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 25[T]}, {}]

Covered

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[-n+j < 0], 25[T]}]

Step with 22

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[-n+j < 0], 25[T]}, {}]

Covered

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 25[T]}]

Step with 23

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[T], 25[T]}, {23[T]}]

Accelerate

Start location: [1]
Program variables: a b c i j m n
  18: [1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
  12: [8] -> [13] : (-n+j >= 0 /\ -m+i >= 0), cost: 1
  22: [8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
  23: [8] -> [8] : c'=c+n4, i'=n4+i, j'=n4+j, (-1+n4 >= 0 /\ 1+m-n4-i > 0), cost: 1
  24: [8] -> [8] : c'=c+n8, i'=n8+i, j'=n8+j, (-1+n8 >= 0 /\ 1+n-n8-j > 0), cost: 1
  25: [8] -> [8] : c'=c+n10*n41+n10*n8, i'=n10*n41+i+n10*n8, j'=n10*n41+j+n10*n8, (-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0), cost: 1
  26: [8] -> [8] : c'=n411*n101*n16+c+n4*n16+n82*n101*n16, i'=n411*n101*n16+n4*n16+n82*n101*n16+i, j'=n411*n101*n16+n4*n16+n82*n101*n16+j, (-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0), cost: 1

	Loop Acceleration

	Original rule:
	[8] -> [8] : c'=c+n411*n101+n82*n101+n4, i'=n411*n101+n82*n101+n4+i, j'=n411*n101+n82*n101+n4+j, (-1+n411 >= 0 /\ 1-n411*n101+m-n82*n101-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-j-n411*(-1+n101) > 0 /\ -1+n82 >= 0 /\ 1-n411-n82*(-1+n101)+m-n411*(-1+n101)-i > 0), cost: 1
	New rule:
	[8] -> [8] : c'=n411*n101*n16+c+n4*n16+n82*n101*n16, i'=n411*n101*n16+n4*n16+n82*n101*n16+i, j'=n411*n101*n16+n4*n16+n82*n101*n16+j, (-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0), cost: 1

		-1+n411 >= 0 [0]: monotonic increase yields -1+n411 >= 0
		
		1-n411*n101+m-n82*n101-n4-i > 0 [0]: montonic decrease yields 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0, dependencies: -1+n411 >= 0 -1+n4 >= 0 -1+n101 >= 0 -1+n82 >= 0
		
		1-n411*n101+m-n82*n101-n4-i > 0 [1]: eventual decrease yields (1-n411*n101+m-n82*n101-n4-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0)
		
		1-n411*n101+m-n82*n101-n4-i > 0 [2]: eventual increase yields (1-n411*n101+m-n82*n101-n4-i > 0 /\ n411*n101+n82*n101+n4 <= 0)
		
		-1+n4 >= 0 [0]: monotonic increase yields -1+n4 >= 0
		
		-1+n101 >= 0 [0]: monotonic increase yields -1+n101 >= 0
		
		1-n411+n-n82*(-1+n101)-n82-j-n411*(-1+n101) > 0 [0]: montonic decrease yields 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0, dependencies: -1+n411 >= 0 -1+n4 >= 0 -1+n101 >= 0 -1+n82 >= 0
		
		1-n411+n-n82*(-1+n101)-n82-j-n411*(-1+n101) > 0 [1]: eventual decrease yields (1-n411+n-n82*(-1+n101)-n82-j-n411*(-1+n101) > 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)
		
		1-n411+n-n82*(-1+n101)-n82-j-n411*(-1+n101) > 0 [2]: eventual increase yields (n411*n101+n82*n101+n4 <= 0 /\ 1-n411+n-n82*(-1+n101)-n82-j-n411*(-1+n101) > 0)
		
		-1+n82 >= 0 [0]: monotonic increase yields -1+n82 >= 0
		
		1-n411-n82*(-1+n101)+m-n411*(-1+n101)-i > 0 [0]: montonic decrease yields 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0, dependencies: 1-n411*n101+m-n82*n101-n4-i > 0 -1+n4 >= 0 -1+n82 >= 0
		
		1-n411-n82*(-1+n101)+m-n411*(-1+n101)-i > 0 [1]: eventual increase yields (n411*n101+n82*n101+n4 <= 0 /\ 1-n411-n82*(-1+n101)+m-n411*(-1+n101)-i > 0)
		
		Replacement map: {-1+n411 >= 0 -> -1+n411 >= 0, 1-n411*n101+m-n82*n101-n4-i > 0 -> 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0, -1+n4 >= 0 -> -1+n4 >= 0, -1+n101 >= 0 -> -1+n101 >= 0, 1-n411+n-n82*(-1+n101)-n82-j-n411*(-1+n101) > 0 -> 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0, -1+n82 >= 0 -> -1+n82 >= 0, 1-n411-n82*(-1+n101)+m-n411*(-1+n101)-i > 0 -> 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0}

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T]}, {26[T]}]

Step with 12

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T]}, {26[T]}, {}]

Backtrack

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 26[T]}]

Step with 22

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 26[T]}, {}]

Covered

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[-m+i < 0], 26[T]}]

Step with 22

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[-m+i < 0], 26[T]}, {}]

Covered

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 26[T]}]

Step with 23

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[T], 26[T]}, {23[T]}]

Covered

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[T], 23[T], 26[T]}]

Step with 24

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[T], 23[T], 26[T]}, {24[T]}]

Covered

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[T], 23[T], 24[T], 26[T]}]

Step with 25

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[T], 23[T], 24[T], 26[T]}, {25[T]}]

Covered

	Trace

	18[T], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T]}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 26[T]}]

Step with 25

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {25[T]}]

Step with 26

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {25[T]}, {26[T]}]

Covered

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {25[T], 26[T]}]

Step with 12

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {25[T], 26[T]}, {}]

Backtrack

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 25[T], 26[T]}]

Step with 22

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 25[T], 26[T]}, {}]

Covered

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 22[-n+j < 0], 25[T], 26[T]}]

Step with 22

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 22[-n+j < 0], 25[T], 26[T]}, {}]

Covered

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 25[T], 26[T]}]

Step with 23

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 22[T], 25[T], 26[T]}, {23[T]}]

Covered

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 22[T], 23[T], 25[T], 26[T]}]

Step with 24

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 22[T], 23[T], 25[T], 26[T]}, {24[T]}]

Covered

	Trace

	18[T], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 26[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T]}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}]

Step with 24

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

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

Step with 25

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

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

Accelerate

Start location: [1]
Program variables: a b c i j m n
  18: [1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
  12: [8] -> [13] : (-n+j >= 0 /\ -m+i >= 0), cost: 1
  22: [8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
  23: [8] -> [8] : c'=c+n4, i'=n4+i, j'=n4+j, (-1+n4 >= 0 /\ 1+m-n4-i > 0), cost: 1
  24: [8] -> [8] : c'=c+n8, i'=n8+i, j'=n8+j, (-1+n8 >= 0 /\ 1+n-n8-j > 0), cost: 1
  25: [8] -> [8] : c'=c+n10*n41+n10*n8, i'=n10*n41+i+n10*n8, j'=n10*n41+j+n10*n8, (-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0), cost: 1
  26: [8] -> [8] : c'=n411*n101*n16+c+n4*n16+n82*n101*n16, i'=n411*n101*n16+n4*n16+n82*n101*n16+i, j'=n411*n101*n16+n4*n16+n82*n101*n16+j, (-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0), cost: 1
  27: [8] -> [8] : c'=c+n33*n87+n10*n33*n8+n10*n41*n33, i'=n33*n87+n10*n33*n8+n10*n41*n33+i, j'=n33*n87+n10*n33*n8+j+n10*n41*n33, (-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0), cost: 1

	Loop Acceleration

	Original rule:
	[8] -> [8] : c'=c+n10*n41+n87+n10*n8, i'=n10*n41+n87+i+n10*n8, j'=n10*n41+n87+j+n10*n8, (-1+n41 >= 0 /\ -1+n10 >= 0 /\ 1+n-n87-j > 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n8 >= 0 /\ -1+n87 >= 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-n87-i > 0), cost: 1
	New rule:
	[8] -> [8] : c'=c+n33*n87+n10*n33*n8+n10*n41*n33, i'=n33*n87+n10*n33*n8+n10*n41*n33+i, j'=n33*n87+n10*n33*n8+j+n10*n41*n33, (-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0), cost: 1

		-1+n41 >= 0 [0]: monotonic increase yields -1+n41 >= 0
		
		-1+n10 >= 0 [0]: monotonic increase yields -1+n10 >= 0
		
		1+n-n87-j > 0 [0]: montonic decrease yields 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0, dependencies: -1+n41 >= 0 -1+n10 >= 0 -1+n8 >= 0 -1+n87 >= 0
		
		1+n-n87-j > 0 [1]: eventual decrease yields (1+n-n87-j > 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0)
		
		1+n-n87-j > 0 [2]: eventual increase yields (n10*n41+n87+n10*n8 <= 0 /\ 1+n-n87-j > 0)
		
		1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-n87-j > 0 [0]: montonic decrease yields 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0, dependencies: 1+n-n87-j > 0 -1+n87 >= 0
		
		1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-n87-j > 0 [1]: eventual decrease yields (1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-n87-j > 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0)
		
		1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-n87-j > 0 [2]: eventual increase yields (n10*n41+n87+n10*n8 <= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-n87-j > 0)
		
		-1+n8 >= 0 [0]: monotonic increase yields -1+n8 >= 0
		
		-1+n87 >= 0 [0]: monotonic increase yields -1+n87 >= 0
		
		1-(-1+n10)*n41+m-n41-(-1+n10)*n8-n87-i > 0 [0]: montonic decrease yields 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0, dependencies: -1+n41 >= 0 -1+n10 >= 0 -1+n8 >= 0 -1+n87 >= 0
		
		1-(-1+n10)*n41+m-n41-(-1+n10)*n8-n87-i > 0 [1]: eventual increase yields (n10*n41+n87+n10*n8 <= 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-n87-i > 0)
		
		Replacement map: {-1+n41 >= 0 -> -1+n41 >= 0, -1+n10 >= 0 -> -1+n10 >= 0, 1+n-n87-j > 0 -> 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0, 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-n87-j > 0 -> 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0, -1+n8 >= 0 -> -1+n8 >= 0, -1+n87 >= 0 -> -1+n87 >= 0, 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-n87-i > 0 -> 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0}

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {27[T]}]

Step with 12

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {27[T]}, {}]

Backtrack

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 27[T]}]

Step with 22

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 27[T]}, {}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[-m+i < 0], 27[T]}]

Step with 22

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[-m+i < 0], 27[T]}, {}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 27[T]}]

Step with 23

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 27[T]}, {23[T]}]

Accelerate

Start location: [1]
Program variables: a b c i j m n
  18: [1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
  12: [8] -> [13] : (-n+j >= 0 /\ -m+i >= 0), cost: 1
  22: [8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
  23: [8] -> [8] : c'=c+n4, i'=n4+i, j'=n4+j, (-1+n4 >= 0 /\ 1+m-n4-i > 0), cost: 1
  24: [8] -> [8] : c'=c+n8, i'=n8+i, j'=n8+j, (-1+n8 >= 0 /\ 1+n-n8-j > 0), cost: 1
  25: [8] -> [8] : c'=c+n10*n41+n10*n8, i'=n10*n41+i+n10*n8, j'=n10*n41+j+n10*n8, (-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0), cost: 1
  26: [8] -> [8] : c'=n411*n101*n16+c+n4*n16+n82*n101*n16, i'=n411*n101*n16+n4*n16+n82*n101*n16+i, j'=n411*n101*n16+n4*n16+n82*n101*n16+j, (-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0), cost: 1
  27: [8] -> [8] : c'=c+n33*n87+n10*n33*n8+n10*n41*n33, i'=n33*n87+n10*n33*n8+n10*n41*n33+i, j'=n33*n87+n10*n33*n8+j+n10*n41*n33, (-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0), cost: 1
  28: [8] -> [8] : c'=c+n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415, i'=n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415+i, j'=n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415+j, (-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0), cost: 1

	Loop Acceleration

	Original rule:
	[8] -> [8] : c'=n871*n331+c+n105*n331*n415+n105*n331*n89+n4, i'=n871*n331+n105*n331*n415+n105*n331*n89+n4+i, j'=n871*n331+n105*n331*n415+n105*n331*n89+n4+j, (-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n871-n871*(-1+n331)-n105*n415*(-1+n331)-j > 0 /\ 1-n105*(-1+n331)*n89+n-(-1+n105)*n89-n871-(-1+n105)*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89 > 0 /\ 1-n871*n331-n105*n331*n415+m-n105*n331*n89-n4-i > 0 /\ 1-n105*(-1+n331)*n89-(-1+n105)*n89-n871-(-1+n105)*n415+m-n415-n871*(-1+n331)-n105*n415*(-1+n331)-i > 0 /\ -1+n415 >= 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ -1+n89 >= 0), cost: 1
	New rule:
	[8] -> [8] : c'=c+n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415, i'=n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415+i, j'=n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415+j, (-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0), cost: 1

		-1+n105 >= 0 [0]: monotonic increase yields -1+n105 >= 0
		
		1-n105*(-1+n331)*n89+n-n871-n871*(-1+n331)-n105*n415*(-1+n331)-j > 0 [0]: montonic decrease yields 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0, dependencies: -1+n105 >= 0 -1+n415 >= 0 -1+n871 >= 0 -1+n4 >= 0 -1+n331 >= 0 -1+n89 >= 0
		
		1-n105*(-1+n331)*n89+n-n871-n871*(-1+n331)-n105*n415*(-1+n331)-j > 0 [1]: eventual decrease yields (1-n105*(-1+n331)*n89+n-n871-n871*(-1+n331)-n105*n415*(-1+n331)-j > 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0)
		
		1-n105*(-1+n331)*n89+n-n871-n871*(-1+n331)-n105*n415*(-1+n331)-j > 0 [2]: eventual increase yields (1-n105*(-1+n331)*n89+n-n871-n871*(-1+n331)-n105*n415*(-1+n331)-j > 0 /\ n871*n331+n105*n331*n415+n105*n331*n89+n4 <= 0)
		
		1-n105*(-1+n331)*n89+n-(-1+n105)*n89-n871-(-1+n105)*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89 > 0 [0]: montonic decrease yields 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0, dependencies: -1+n105 >= 0 -1+n415 >= 0 -1+n871 >= 0 -1+n4 >= 0 -1+n331 >= 0 -1+n89 >= 0
		
		1-n105*(-1+n331)*n89+n-(-1+n105)*n89-n871-(-1+n105)*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89 > 0 [1]: eventual decrease yields (1-n105*(-1+n331)*n89+n-(-1+n105)*n89-n871-(-1+n105)*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89 > 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0)
		
		1-n105*(-1+n331)*n89+n-(-1+n105)*n89-n871-(-1+n105)*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89 > 0 [2]: eventual increase yields (1-n105*(-1+n331)*n89+n-(-1+n105)*n89-n871-(-1+n105)*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89 > 0 /\ n871*n331+n105*n331*n415+n105*n331*n89+n4 <= 0)
		
		1-n871*n331-n105*n331*n415+m-n105*n331*n89-n4-i > 0 [0]: montonic decrease yields 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0, dependencies: -1+n105 >= 0 -1+n415 >= 0 -1+n871 >= 0 -1+n4 >= 0 -1+n331 >= 0 -1+n89 >= 0
		
		1-n871*n331-n105*n331*n415+m-n105*n331*n89-n4-i > 0 [1]: eventual decrease yields (1-n871*n331-n105*n331*n415+m-n105*n331*n89-n4-i > 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0)
		
		1-n871*n331-n105*n331*n415+m-n105*n331*n89-n4-i > 0 [2]: eventual increase yields (1-n871*n331-n105*n331*n415+m-n105*n331*n89-n4-i > 0 /\ n871*n331+n105*n331*n415+n105*n331*n89+n4 <= 0)
		
		1-n105*(-1+n331)*n89-(-1+n105)*n89-n871-(-1+n105)*n415+m-n415-n871*(-1+n331)-n105*n415*(-1+n331)-i > 0 [0]: montonic decrease yields 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0, dependencies: 1-n871*n331-n105*n331*n415+m-n105*n331*n89-n4-i > 0 -1+n4 >= 0 -1+n89 >= 0
		
		1-n105*(-1+n331)*n89-(-1+n105)*n89-n871-(-1+n105)*n415+m-n415-n871*(-1+n331)-n105*n415*(-1+n331)-i > 0 [1]: eventual decrease yields (1-n105*(-1+n331)*n89-(-1+n105)*n89-n871-(-1+n105)*n415+m-n415-n871*(-1+n331)-n105*n415*(-1+n331)-i > 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0)
		
		1-n105*(-1+n331)*n89-(-1+n105)*n89-n871-(-1+n105)*n415+m-n415-n871*(-1+n331)-n105*n415*(-1+n331)-i > 0 [2]: eventual increase yields (1-n105*(-1+n331)*n89-(-1+n105)*n89-n871-(-1+n105)*n415+m-n415-n871*(-1+n331)-n105*n415*(-1+n331)-i > 0 /\ n871*n331+n105*n331*n415+n105*n331*n89+n4 <= 0)
		
		-1+n415 >= 0 [0]: monotonic increase yields -1+n415 >= 0
		
		-1+n871 >= 0 [0]: monotonic increase yields -1+n871 >= 0
		
		-1+n4 >= 0 [0]: monotonic increase yields -1+n4 >= 0
		
		-1+n331 >= 0 [0]: monotonic increase yields -1+n331 >= 0
		
		-1+n89 >= 0 [0]: monotonic increase yields -1+n89 >= 0
		
		Replacement map: {-1+n105 >= 0 -> -1+n105 >= 0, 1-n105*(-1+n331)*n89+n-n871-n871*(-1+n331)-n105*n415*(-1+n331)-j > 0 -> 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0, 1-n105*(-1+n331)*n89+n-(-1+n105)*n89-n871-(-1+n105)*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89 > 0 -> 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0, 1-n871*n331-n105*n331*n415+m-n105*n331*n89-n4-i > 0 -> 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0, 1-n105*(-1+n331)*n89-(-1+n105)*n89-n871-(-1+n105)*n415+m-n415-n871*(-1+n331)-n105*n415*(-1+n331)-i > 0 -> 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0, -1+n415 >= 0 -> -1+n415 >= 0, -1+n871 >= 0 -> -1+n871 >= 0, -1+n4 >= 0 -> -1+n4 >= 0, -1+n331 >= 0 -> -1+n331 >= 0, -1+n89 >= 0 -> -1+n89 >= 0}

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {28[T]}]

Step with 12

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {28[T]}, {}]

Backtrack

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 28[T]}]

Step with 22

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 28[T]}, {}]

Covered

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[-m+i < 0], 28[T]}]

Step with 22

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[-m+i < 0], 28[T]}, {}]

Covered

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 28[T]}]

Step with 23

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 28[T]}, {23[T]}]

Covered

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 28[T]}]

Step with 24

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 28[T]}, {24[T]}]

Covered

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 24[T], 28[T]}]

Step with 25

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 24[T], 28[T]}, {25[T]}]

Covered

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 28[T]}]

Step with 26

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 28[T]}, {26[T]}]

Covered

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 28[T]}]

Step with 27

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 28[T]}, {27[T]}]

Covered

	Trace

	18[T], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}]

Step with 27

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {27[T]}]

Step with 28

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {27[T]}, {28[T]}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {27[T], 28[T]}]

Step with 12

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {27[T], 28[T]}, {}]

Backtrack

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 27[T], 28[T]}]

Step with 22

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 27[T], 28[T]}, {}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[-m+i < 0], 27[T], 28[T]}]

Step with 22

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[-m+i < 0], 27[T], 28[T]}, {}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 27[T], 28[T]}]

Step with 23

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[T], 27[T], 28[T]}, {23[T]}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[T], 23[T], 27[T], 28[T]}]

Step with 24

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[T], 23[T], 27[T], 28[T]}, {24[T]}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 27[T], 28[T]}]

Step with 25

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 27[T], 28[T]}, {25[T]}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 27[T], 28[T]}]

Step with 26

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 27[T], 28[T]}, {26[T]}]

Covered

	Trace

	18[T], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 22

	Trace

	18[T], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 25[T], 26[T], 27[T], 28[T]}, {}]

Covered

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 22[-n+j < 0], 25[T], 26[T], 27[T], 28[T]}]

Step with 22

	Trace

	18[T], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 22[-n+j < 0], 25[T], 26[T], 27[T], 28[T]}, {}]

Covered

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 25[T], 26[T], 27[T], 28[T]}]

Step with 23

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T]}]

Step with 24

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T]}, {24[T]}]

Covered

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T]}]

Step with 25

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T]}, {25[T]}]

Covered

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T], 25[T]}]

Step with 26

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T], 25[T]}, {26[T]}]

Covered

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T], 25[T], 26[T]}]

Step with 27

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T], 25[T], 26[T]}, {27[T]}]

Covered

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T], 25[T], 26[T], 27[T]}]

Step with 28

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T], 25[T], 26[T], 27[T]}, {28[T]}]

Covered

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 12

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}, {}]

Backtrack

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 22

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}, {}]

Covered

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[-m+i < 0], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 22

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[-m+i < 0], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}, {}]

Covered

	Trace

	18[T], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 24

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T]}]

Step with 25

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T]}, {25[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T], 25[T]}]

Step with 26

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T], 25[T]}, {26[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T], 25[T], 26[T]}]

Step with 27

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T], 25[T], 26[T]}, {27[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T], 25[T], 26[T], 27[T]}]

Step with 28

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T], 25[T], 26[T], 27[T]}, {28[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 12

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {24[T], 25[T], 26[T], 27[T], 28[T]}, {}]

Backtrack

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 22

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 24[T], 25[T], 26[T], 27[T], 28[T]}, {}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[-n+j < 0], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 22

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[-n+j < 0], 24[T], 25[T], 26[T], 27[T], 28[T]}, {}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 24[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 23

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 24[T], 25[T], 26[T], 27[T], 28[T]}, {23[T]}]

Accelerate

Start location: [1]
Program variables: a b c i j m n
  18: [1] -> [8] : a'=nondet, b'=nondet1, c'=0, i'=nondet, j'=nondet1, m'=nondet2, n'=nondet3, T, cost: 1
  12: [8] -> [13] : (-n+j >= 0 /\ -m+i >= 0), cost: 1
  22: [8] -> [8] : c'=1+c, i'=1+i, j'=1+j, (-n+j < 0 \/ -m+i < 0), cost: 1
  23: [8] -> [8] : c'=c+n4, i'=n4+i, j'=n4+j, (-1+n4 >= 0 /\ 1+m-n4-i > 0), cost: 1
  24: [8] -> [8] : c'=c+n8, i'=n8+i, j'=n8+j, (-1+n8 >= 0 /\ 1+n-n8-j > 0), cost: 1
  25: [8] -> [8] : c'=c+n10*n41+n10*n8, i'=n10*n41+i+n10*n8, j'=n10*n41+j+n10*n8, (-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0), cost: 1
  26: [8] -> [8] : c'=n411*n101*n16+c+n4*n16+n82*n101*n16, i'=n411*n101*n16+n4*n16+n82*n101*n16+i, j'=n411*n101*n16+n4*n16+n82*n101*n16+j, (-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0), cost: 1
  27: [8] -> [8] : c'=c+n33*n87+n10*n33*n8+n10*n41*n33, i'=n33*n87+n10*n33*n8+n10*n41*n33+i, j'=n33*n87+n10*n33*n8+j+n10*n41*n33, (-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0), cost: 1
  28: [8] -> [8] : c'=c+n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415, i'=n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415+i, j'=n871*n331*n39+n39*n4+n105*n331*n39*n89+n105*n331*n39*n415+j, (-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0), cost: 1
  29: [8] -> [8] : c'=c+n819*n95+n95*n4, i'=n819*n95+n95*n4+i, j'=n819*n95+n95*n4+j, (1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0), cost: 1

	Loop Acceleration

	Original rule:
	[8] -> [8] : c'=c+n819+n4, i'=n819+n4+i, j'=n819+n4+j, (1-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ 1+n-n819-j > 0), cost: 1
	New rule:
	[8] -> [8] : c'=c+n819*n95+n95*n4, i'=n819*n95+n95*n4+i, j'=n819*n95+n95*n4+j, (1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0), cost: 1

		1-n819+m-n4-i > 0 [0]: montonic decrease yields 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0, dependencies: -1+n4 >= 0 -1+n819 >= 0
		
		1-n819+m-n4-i > 0 [1]: eventual decrease yields (1-n819+m-n4-i > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0)
		
		1-n819+m-n4-i > 0 [2]: eventual increase yields (1-n819+m-n4-i > 0 /\ n819+n4 <= 0)
		
		-1+n4 >= 0 [0]: monotonic increase yields -1+n4 >= 0
		
		-1+n819 >= 0 [0]: monotonic increase yields -1+n819 >= 0
		
		1+n-n819-j > 0 [0]: montonic decrease yields 1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0, dependencies: -1+n4 >= 0 -1+n819 >= 0
		
		1+n-n819-j > 0 [1]: eventual increase yields (n819+n4 <= 0 /\ 1+n-n819-j > 0)
		
		Replacement map: {1-n819+m-n4-i > 0 -> 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0, -1+n4 >= 0 -> -1+n4 >= 0, -1+n819 >= 0 -> -1+n819 >= 0, 1+n-n819-j > 0 -> 1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0}

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {29[T]}]

Step with 12

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {29[T]}, {}]

Backtrack

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 29[T]}]

Step with 22

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 29[T]}, {}]

Covered

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[-n+j < 0], 29[T]}]

Step with 22

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[-n+j < 0], 29[T]}, {}]

Covered

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 29[T]}]

Step with 23

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 29[T]}, {23[T]}]

Covered

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 29[T]}]

Step with 24

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 29[T]}, {24[T]}]

Covered

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 29[T]}]

Step with 25

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 29[T]}, {25[T]}]

Covered

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 29[T]}]

Step with 26

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 29[T]}, {26[T]}]

Covered

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 29[T]}]

Step with 27

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 29[T]}, {27[T]}]

Covered

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 27[T], 29[T]}]

Step with 28

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 27[T], 29[T]}, {28[T]}]

Covered

	Trace

	18[T], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}]

Step with 24

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T]}]

Step with 25

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 25[(-1+n41 >= 0 /\ 1-(-1+n10)*n41+n-n41-(-1+n10)*n8-n8-j > 0 /\ 1-(-1+n10)*n41+m-n41-(-1+n10)*n8-i > 0 /\ -1+n10 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T]}, {25[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T]}]

Step with 26

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 26[(-1+n411 >= 0 /\ -1+n4 >= 0 /\ -1+n101 >= 0 /\ 1-n411-n82*(-1+n101)-n82*(-1+n16)*n101+m-(-1+n16)*n4-n411*(-1+n101)-n411*(-1+n16)*n101-i > 0 /\ 1-n411*n101-n82*(-1+n16)*n101+m-n82*n101-n4-(-1+n16)*n4-n411*(-1+n16)*n101-i > 0 /\ -1+n16 >= 0 /\ -1+n82 >= 0 /\ 1-n411+n-n82*(-1+n101)-n82-n82*(-1+n16)*n101-(-1+n16)*n4-j-n411*(-1+n101)-n411*(-1+n16)*n101 > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T]}, {26[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T], 26[T]}]

Step with 27

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 27[(-1+n41 >= 0 /\ -1+n33 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8-(-1+n33)*n87+m-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n87-i > 0 /\ -1+n10 >= 0 /\ 1-n10*(-1+n33)*n8+n-(-1+n33)*n87-n10*(-1+n33)*n41-n87-j > 0 /\ -1+n8 >= 0 /\ 1-(-1+n10)*n41-n10*(-1+n33)*n8+n-(-1+n33)*n87-n41-n10*(-1+n33)*n41-(-1+n10)*n8-n8-n87-j > 0 /\ -1+n87 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T], 26[T]}, {27[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T], 26[T], 27[T]}]

Step with 28

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 28[(-1+n105 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-n871-(-1+n39)*n871*n331-n105*(-1+n39)*n331*n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-(-1+n39)*n4 > 0 /\ -1+n39 >= 0 /\ 1-n105*(-1+n331)*n89-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415+m-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-(-1+n39)*n4-i > 0 /\ -1+n415 >= 0 /\ 1-n105*(-1+n331)*n89+n-n105*(-1+n39)*n331*n89-(-1+n105)*n89-n871-(-1+n39)*n871*n331-(-1+n105)*n415-n105*(-1+n39)*n331*n415-n415-n871*(-1+n331)-n105*n415*(-1+n331)-j-n89-(-1+n39)*n4 > 0 /\ -1+n871 >= 0 /\ -1+n4 >= 0 /\ -1+n331 >= 0 /\ 1-n871*n331-n105*n331*n415-n105*(-1+n39)*n331*n89-(-1+n39)*n871*n331+m-n105*(-1+n39)*n331*n415-n105*n331*n89-n4-(-1+n39)*n4-i > 0 /\ -1+n89 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T], 26[T], 27[T]}, {28[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T], 26[T], 27[T], 28[T]}]

Step with 29

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 29[(1-n4*(-1+n95)+n-n819*(-1+n95)-n819-j > 0 /\ 1-n4*(-1+n95)-n819*(-1+n95)-n819+m-n4-i > 0 /\ -1+n4 >= 0 /\ -1+n819 >= 0 /\ -1+n95 >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T], 26[T], 27[T], 28[T]}, {29[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}]

Step with 12

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 12[(-n+j >= 0 /\ -m+i >= 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {}]

Backtrack

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {12[T], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}]

Step with 22

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 22[(-n+j < 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {12[T], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {12[T], 22[-n+j < 0], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}]

Step with 22

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 22[(-m+i < 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {12[T], 22[-n+j < 0], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {12[T], 22[(-n+j < 0 /\ -m+i < 0)], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}]

Step with 23

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)], 23[(-1+n4 >= 0 /\ 1+m-n4-i > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {12[T], 22[T], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {23[T]}]

Covered

	Trace

	18[T], 24[(-1+n8 >= 0 /\ 1+n-n8-j > 0)]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 25[T], 26[T], 27[T], 28[T], 29[T]}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {12[T], 22[T], 23[T], 24[T], 25[T], 26[T], 27[T], 28[T], 29[T]}]

Backtrack

	Trace

	Blocked

	[{18[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b