NO

Initial ITS

Start location: [1]
Program variables: i j
   0: [1] -> [2] : i'=nondet, T, cost: 1
   1: [2] -> [3] : j'=i, T, cost: 1
   2: [3] -> [4] : i > 0, cost: 1
  39: [3] -> [34] : i <= 0, cost: 1
   3: [4] -> [6] : -j+i >= 0, cost: 1
  18: [4] -> [18] : -j+i < 0, cost: 1
  38: [5] -> [3] : T, cost: 1
   4: [6] -> [7] : i'=1+i, T, cost: 1
   5: [7] -> [9] : -5+j < 0, cost: 1
  14: [7] -> [16] : -5+j >= 0, cost: 1
  17: [8] -> [5] : T, cost: 1
   6: [9] -> [10] : j'=1+j, T, cost: 1
   7: [10] -> [12] : -2-j+i > 0, cost: 1
  10: [10] -> [14] : -2-j+i <= 0, cost: 1
  13: [11] -> [8] : T, cost: 1
   8: [12] -> [13] : i'=1+i, T, cost: 1
   9: [13] -> [11] : T, cost: 1
  11: [14] -> [15] : j'=1+j, T, cost: 1
  12: [15] -> [11] : T, cost: 1
  15: [16] -> [17] : j'=-1+j, T, cost: 1
  16: [17] -> [8] : T, cost: 1
  19: [18] -> [20] : (j < 0 /\ i > 0), cost: 1
  28: [18] -> [27] : (j >= 0 \/ i <= 0), cost: 1
  37: [19] -> [5] : T, cost: 1
  20: [20] -> [21] : i'=-1+i, T, cost: 1
  21: [21] -> [23] : 1+j < 0, cost: 1
  24: [21] -> [25] : 1+j >= 0, cost: 1
  27: [22] -> [19] : T, cost: 1
  22: [23] -> [24] : j'=1+j, T, cost: 1
  23: [24] -> [22] : T, cost: 1
  25: [25] -> [26] : i'=1+i, T, cost: 1
  26: [26] -> [22] : T, cost: 1
  29: [27] -> [28] : i'=1+i, T, cost: 1
  30: [28] -> [30] : 2*j-i > 0, cost: 1
  33: [28] -> [32] : 2*j-i <= 0, cost: 1
  36: [29] -> [19] : T, cost: 1
  31: [30] -> [31] : j'=-1+j, T, cost: 1
  32: [31] -> [29] : T, cost: 1
  34: [32] -> [33] : j'=1+j, T, cost: 1
  35: [33] -> [29] : T, cost: 1

Chained Linear Paths

Start location: [1]
Program variables: i j
  40: [1] -> [3] : i'=nondet, j'=nondet, T, cost: 1
   2: [3] -> [4] : i > 0, cost: 1
  39: [3] -> [34] : i <= 0, cost: 1
  18: [4] -> [18] : -j+i < 0, cost: 1
  41: [4] -> [7] : i'=1+i, -j+i >= 0, cost: 1
  38: [5] -> [3] : T, cost: 1
  42: [7] -> [10] : j'=1+j, -5+j < 0, cost: 1
  44: [7] -> [8] : j'=-1+j, -5+j >= 0, cost: 1
  17: [8] -> [5] : T, cost: 1
  47: [10] -> [11] : i'=1+i, -2-j+i > 0, cost: 1
  48: [10] -> [11] : j'=1+j, -2-j+i <= 0, cost: 1
  13: [11] -> [8] : T, cost: 1
  49: [18] -> [21] : i'=-1+i, (j < 0 /\ i > 0), cost: 1
  50: [18] -> [28] : i'=1+i, (j >= 0 \/ i <= 0), cost: 1
  37: [19] -> [5] : T, cost: 1
  53: [21] -> [22] : j'=1+j, 1+j < 0, cost: 1
  54: [21] -> [22] : i'=1+i, 1+j >= 0, cost: 1
  27: [22] -> [19] : T, cost: 1
  57: [28] -> [29] : j'=-1+j, 2*j-i > 0, cost: 1
  58: [28] -> [29] : j'=1+j, 2*j-i <= 0, cost: 1
  36: [29] -> [19] : T, cost: 1

	Eliminating location [2] by chaining:

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

	First rule:
	[7] -> [9] : -5+j < 0, cost: 1
	Second rule:
	[9] -> [10] : j'=1+j, T, cost: 1
	New rule:
	[7] -> [10] : j'=1+j, -5+j < 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[7] -> [16] : -5+j >= 0, cost: 1
	Second rule:
	[16] -> [17] : j'=-1+j, T, cost: 1
	New rule:
	[7] -> [17] : j'=-1+j, -5+j >= 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[7] -> [17] : j'=-1+j, -5+j >= 0, cost: 1
	Second rule:
	[17] -> [8] : T, cost: 1
	New rule:
	[7] -> [8] : j'=-1+j, -5+j >= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 16 43
	
	Eliminating location [12] by chaining:

	Applied chaining

	First rule:
	[10] -> [12] : -2-j+i > 0, cost: 1
	Second rule:
	[12] -> [13] : i'=1+i, T, cost: 1
	New rule:
	[10] -> [13] : i'=1+i, -2-j+i > 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[10] -> [14] : -2-j+i <= 0, cost: 1
	Second rule:
	[14] -> [15] : j'=1+j, T, cost: 1
	New rule:
	[10] -> [15] : j'=1+j, -2-j+i <= 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[10] -> [13] : i'=1+i, -2-j+i > 0, cost: 1
	Second rule:
	[13] -> [11] : T, cost: 1
	New rule:
	[10] -> [11] : i'=1+i, -2-j+i > 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[10] -> [15] : j'=1+j, -2-j+i <= 0, cost: 1
	Second rule:
	[15] -> [11] : T, cost: 1
	New rule:
	[10] -> [11] : j'=1+j, -2-j+i <= 0, cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	[18] -> [20] : (j < 0 /\ i > 0), cost: 1
	Second rule:
	[20] -> [21] : i'=-1+i, T, cost: 1
	New rule:
	[18] -> [21] : i'=-1+i, (j < 0 /\ i > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 19 20
	
	Eliminating location [27] by chaining:

	Applied chaining

	First rule:
	[18] -> [27] : (j >= 0 \/ i <= 0), cost: 1
	Second rule:
	[27] -> [28] : i'=1+i, T, cost: 1
	New rule:
	[18] -> [28] : i'=1+i, (j >= 0 \/ i <= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 28 29
	
	Eliminating location [23] by chaining:

	Applied chaining

	First rule:
	[21] -> [23] : 1+j < 0, cost: 1
	Second rule:
	[23] -> [24] : j'=1+j, T, cost: 1
	New rule:
	[21] -> [24] : j'=1+j, 1+j < 0, cost: 1
	
	Applied deletion

	Removed the following rules: 21 22
	
	Eliminating location [25] by chaining:

	Applied chaining

	First rule:
	[21] -> [25] : 1+j >= 0, cost: 1
	Second rule:
	[25] -> [26] : i'=1+i, T, cost: 1
	New rule:
	[21] -> [26] : i'=1+i, 1+j >= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 24 25
	
	Eliminating location [24] by chaining:

	Applied chaining

	First rule:
	[21] -> [24] : j'=1+j, 1+j < 0, cost: 1
	Second rule:
	[24] -> [22] : T, cost: 1
	New rule:
	[21] -> [22] : j'=1+j, 1+j < 0, cost: 1
	
	Applied deletion

	Removed the following rules: 23 51
	
	Eliminating location [26] by chaining:

	Applied chaining

	First rule:
	[21] -> [26] : i'=1+i, 1+j >= 0, cost: 1
	Second rule:
	[26] -> [22] : T, cost: 1
	New rule:
	[21] -> [22] : i'=1+i, 1+j >= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 26 52
	
	Eliminating location [30] by chaining:

	Applied chaining

	First rule:
	[28] -> [30] : 2*j-i > 0, cost: 1
	Second rule:
	[30] -> [31] : j'=-1+j, T, cost: 1
	New rule:
	[28] -> [31] : j'=-1+j, 2*j-i > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 30 31
	
	Eliminating location [32] by chaining:

	Applied chaining

	First rule:
	[28] -> [32] : 2*j-i <= 0, cost: 1
	Second rule:
	[32] -> [33] : j'=1+j, T, cost: 1
	New rule:
	[28] -> [33] : j'=1+j, 2*j-i <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 33 34
	
	Eliminating location [31] by chaining:

	Applied chaining

	First rule:
	[28] -> [31] : j'=-1+j, 2*j-i > 0, cost: 1
	Second rule:
	[31] -> [29] : T, cost: 1
	New rule:
	[28] -> [29] : j'=-1+j, 2*j-i > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 32 55
	
	Eliminating location [33] by chaining:

	Applied chaining

	First rule:
	[28] -> [33] : j'=1+j, 2*j-i <= 0, cost: 1
	Second rule:
	[33] -> [29] : T, cost: 1
	New rule:
	[28] -> [29] : j'=1+j, 2*j-i <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 35 56

Step with 40

	Trace

	40[T]
	
	Blocked

	[{}, {}]

Step with 39

	Trace

	40[T], 39[(i <= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	40[T]
	
	Blocked

	[{}, {39[T]}]

Step with 2

	Trace

	40[T], 2[(i > 0)]
	
	Blocked

	[{}, {39[T]}, {}]

Step with 41

	Trace

	40[T], 2[(i > 0)], 41[(-j+i >= 0)]
	
	Blocked

	[{}, {39[T]}, {18[T]}, {}]

Step with 42

	Trace

	40[T], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)]
	
	Blocked

	[{}, {39[T]}, {18[T]}, {}, {}]

Step with 48

	Trace

	40[T], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)]
	
	Blocked

	[{}, {39[T]}, {18[T]}, {}, {47[T]}, {}]

Step with 13

	Trace

	40[T], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)], 13[T]
	
	Blocked

	[{}, {39[T]}, {18[T]}, {}, {47[T]}, {}, {}]

Step with 17

	Trace

	40[T], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)], 13[T], 17[T]
	
	Blocked

	[{}, {39[T]}, {18[T]}, {}, {47[T]}, {}, {}, {}]

Step with 38

	Trace

	40[T], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)], 13[T], 17[T], 38[T]
	
	Blocked

	[{}, {39[T]}, {18[T]}, {}, {47[T]}, {}, {}, {}, {}]

Accelerate

Start location: [1]
Program variables: i j
  40: [1] -> [3] : i'=nondet, j'=nondet, T, cost: 1
   2: [3] -> [4] : i > 0, cost: 1
  39: [3] -> [34] : i <= 0, cost: 1
  59: [3] -> [3] : i'=n+i, j'=2*n+j, (1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0), cost: 1
  18: [4] -> [18] : -j+i < 0, cost: 1
  41: [4] -> [7] : i'=1+i, -j+i >= 0, cost: 1
  38: [5] -> [3] : T, cost: 1
  42: [7] -> [10] : j'=1+j, -5+j < 0, cost: 1
  44: [7] -> [8] : j'=-1+j, -5+j >= 0, cost: 1
  17: [8] -> [5] : T, cost: 1
  47: [10] -> [11] : i'=1+i, -2-j+i > 0, cost: 1
  48: [10] -> [11] : j'=1+j, -2-j+i <= 0, cost: 1
  13: [11] -> [8] : T, cost: 1
  49: [18] -> [21] : i'=-1+i, (j < 0 /\ i > 0), cost: 1
  50: [18] -> [28] : i'=1+i, (j >= 0 \/ i <= 0), cost: 1
  37: [19] -> [5] : T, cost: 1
  53: [21] -> [22] : j'=1+j, 1+j < 0, cost: 1
  54: [21] -> [22] : i'=1+i, 1+j >= 0, cost: 1
  27: [22] -> [19] : T, cost: 1
  57: [28] -> [29] : j'=-1+j, 2*j-i > 0, cost: 1
  58: [28] -> [29] : j'=1+j, 2*j-i <= 0, cost: 1
  36: [29] -> [19] : T, cost: 1

	Loop Acceleration

	Original rule:
	[3] -> [3] : i'=1+i, j'=2+j, (-5+j < 0 /\ -2-j+i <= 0 /\ -j+i >= 0 /\ i > 0), cost: 1
	New rule:
	[3] -> [3] : i'=n+i, j'=2*n+j, (1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0), cost: 1

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

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)]
	
	Blocked

	[{}, {39[T]}, {59[T]}]

Step with 2

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 2[(i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {}]

Step with 18

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 2[(i > 0)], 18[(-j+i < 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {41[T]}, {}]

Step with 50

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 2[(i > 0)], 18[(-j+i < 0)], 50[(j >= 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {41[T]}, {49[T]}, {}]

Step with 57

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 2[(i > 0)], 18[(-j+i < 0)], 50[(j >= 0)], 57[(2*j-i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {41[T]}, {49[T]}, {}, {}]

Step with 36

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 2[(i > 0)], 18[(-j+i < 0)], 50[(j >= 0)], 57[(2*j-i > 0)], 36[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {41[T]}, {49[T]}, {}, {}, {}]

Step with 37

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 2[(i > 0)], 18[(-j+i < 0)], 50[(j >= 0)], 57[(2*j-i > 0)], 36[T], 37[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {41[T]}, {49[T]}, {}, {}, {}, {}]

Step with 38

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 2[(i > 0)], 18[(-j+i < 0)], 50[(j >= 0)], 57[(2*j-i > 0)], 36[T], 37[T], 38[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {41[T]}, {49[T]}, {}, {}, {}, {}, {}]

Accelerate

Start location: [1]
Program variables: i j
  40: [1] -> [3] : i'=nondet, j'=nondet, T, cost: 1
   2: [3] -> [4] : i > 0, cost: 1
  39: [3] -> [34] : i <= 0, cost: 1
  59: [3] -> [3] : i'=n+i, j'=2*n+j, (1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0), cost: 1
  60: [3] -> [3] : i'=n2+i, j'=-n2+j, (-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0), cost: 1
  18: [4] -> [18] : -j+i < 0, cost: 1
  41: [4] -> [7] : i'=1+i, -j+i >= 0, cost: 1
  38: [5] -> [3] : T, cost: 1
  42: [7] -> [10] : j'=1+j, -5+j < 0, cost: 1
  44: [7] -> [8] : j'=-1+j, -5+j >= 0, cost: 1
  17: [8] -> [5] : T, cost: 1
  47: [10] -> [11] : i'=1+i, -2-j+i > 0, cost: 1
  48: [10] -> [11] : j'=1+j, -2-j+i <= 0, cost: 1
  13: [11] -> [8] : T, cost: 1
  49: [18] -> [21] : i'=-1+i, (j < 0 /\ i > 0), cost: 1
  50: [18] -> [28] : i'=1+i, (j >= 0 \/ i <= 0), cost: 1
  37: [19] -> [5] : T, cost: 1
  53: [21] -> [22] : j'=1+j, 1+j < 0, cost: 1
  54: [21] -> [22] : i'=1+i, 1+j >= 0, cost: 1
  27: [22] -> [19] : T, cost: 1
  57: [28] -> [29] : j'=-1+j, 2*j-i > 0, cost: 1
  58: [28] -> [29] : j'=1+j, 2*j-i <= 0, cost: 1
  36: [29] -> [19] : T, cost: 1

	Loop Acceleration

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

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

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {60[T]}]

Acceleration Failed

marked recursive suffix as redundant

Step with 2

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {}]

Step with 41

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}]

Step with 42

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {}]

Step with 48

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {}, {}]

Step with 13

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)], 13[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {}, {}, {}]

Step with 17

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)], 13[T], 17[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {}, {}, {}, {}]

Step with 38

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)], 13[T], 17[T], 38[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {}, {}, {}, {}, {}]

Covered

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)], 13[T], 17[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {}, {}, {}, {38[T]}]

Backtrack

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)], 13[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {}, {}, {17[T]}]

Backtrack

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 48[(-2-j+i <= 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {}, {13[T]}]

Backtrack

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {}, {48[T]}]

Backtrack

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {42[T]}]

Step with 44

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 44[(-5+j >= 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {42[T]}, {}]

Step with 17

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 44[(-5+j >= 0)], 17[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {42[T]}, {}, {}]

Step with 38

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 44[(-5+j >= 0)], 17[T], 38[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {18[T]}, {42[T]}, {}, {}, {}]

Accelerate

Start location: [1]
Program variables: i j
  40: [1] -> [3] : i'=nondet, j'=nondet, T, cost: 1
   2: [3] -> [4] : i > 0, cost: 1
  39: [3] -> [34] : i <= 0, cost: 1
  59: [3] -> [3] : i'=n+i, j'=2*n+j, (1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0), cost: 1
  60: [3] -> [3] : i'=n2+i, j'=-n2+j, (-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0), cost: 1
  61: [3] -> [3] : i'=n3+i, j'=-n3+j, (-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0), cost: 1
  18: [4] -> [18] : -j+i < 0, cost: 1
  41: [4] -> [7] : i'=1+i, -j+i >= 0, cost: 1
  38: [5] -> [3] : T, cost: 1
  42: [7] -> [10] : j'=1+j, -5+j < 0, cost: 1
  44: [7] -> [8] : j'=-1+j, -5+j >= 0, cost: 1
  17: [8] -> [5] : T, cost: 1
  47: [10] -> [11] : i'=1+i, -2-j+i > 0, cost: 1
  48: [10] -> [11] : j'=1+j, -2-j+i <= 0, cost: 1
  13: [11] -> [8] : T, cost: 1
  49: [18] -> [21] : i'=-1+i, (j < 0 /\ i > 0), cost: 1
  50: [18] -> [28] : i'=1+i, (j >= 0 \/ i <= 0), cost: 1
  37: [19] -> [5] : T, cost: 1
  53: [21] -> [22] : j'=1+j, 1+j < 0, cost: 1
  54: [21] -> [22] : i'=1+i, 1+j >= 0, cost: 1
  27: [22] -> [19] : T, cost: 1
  57: [28] -> [29] : j'=-1+j, 2*j-i > 0, cost: 1
  58: [28] -> [29] : j'=1+j, 2*j-i <= 0, cost: 1
  36: [29] -> [19] : T, cost: 1

	Loop Acceleration

	Original rule:
	[3] -> [3] : i'=1+i, j'=-1+j, (-5+j >= 0 /\ -j+i >= 0 /\ i > 0), cost: 1
	New rule:
	[3] -> [3] : i'=n3+i, j'=-n3+j, (-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0), cost: 1

		-5+j >= 0 [0]: montonic decrease yields -4-n3+j >= 0
		
		-5+j >= 0 [1]: eventual increase yields (1 <= 0 /\ -5+j >= 0)
		
		-j+i >= 0 [0]: monotonic increase yields -j+i >= 0
		
		i > 0 [0]: monotonic increase yields i > 0, dependencies: -5+j >= 0 -j+i >= 0
		
		Replacement map: {-5+j >= 0 -> -4-n3+j >= 0, -j+i >= 0 -> -j+i >= 0, i > 0 -> i > 0}

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {61[T]}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 2

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)], 2[(i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {39[T], 61[T]}, {}]

Step with 41

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {39[T], 61[T]}, {}, {}]

Step with 42

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {39[T], 61[T]}, {}, {44[T]}, {}]

Step with 47

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 47[(-2-j+i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {39[T], 61[T]}, {}, {44[T]}, {48[T]}, {}]

Step with 13

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 47[(-2-j+i > 0)], 13[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {39[T], 61[T]}, {}, {44[T]}, {48[T]}, {}, {}]

Step with 17

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 47[(-2-j+i > 0)], 13[T], 17[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {39[T], 61[T]}, {}, {44[T]}, {48[T]}, {}, {}, {}]

Step with 38

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)], 2[(i > 0)], 41[(-j+i >= 0)], 42[(-5+j < 0)], 47[(-2-j+i > 0)], 13[T], 17[T], 38[T]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {39[T], 61[T]}, {}, {44[T]}, {48[T]}, {}, {}, {}, {}]

Accelerate

Start location: [1]
Program variables: i j
  40: [1] -> [3] : i'=nondet, j'=nondet, T, cost: 1
   2: [3] -> [4] : i > 0, cost: 1
  39: [3] -> [34] : i <= 0, cost: 1
  59: [3] -> [3] : i'=n+i, j'=2*n+j, (1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0), cost: 1
  60: [3] -> [3] : i'=n2+i, j'=-n2+j, (-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0), cost: 1
  61: [3] -> [3] : i'=n3+i, j'=-n3+j, (-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0), cost: 1
  62: [3] -> [3] : i'=2*n4+i, j'=j+n4, (-2-j+i > 0 /\ 6-j-n4 > 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ i > 0), cost: 1
  18: [4] -> [18] : -j+i < 0, cost: 1
  41: [4] -> [7] : i'=1+i, -j+i >= 0, cost: 1
  38: [5] -> [3] : T, cost: 1
  42: [7] -> [10] : j'=1+j, -5+j < 0, cost: 1
  44: [7] -> [8] : j'=-1+j, -5+j >= 0, cost: 1
  17: [8] -> [5] : T, cost: 1
  47: [10] -> [11] : i'=1+i, -2-j+i > 0, cost: 1
  48: [10] -> [11] : j'=1+j, -2-j+i <= 0, cost: 1
  13: [11] -> [8] : T, cost: 1
  49: [18] -> [21] : i'=-1+i, (j < 0 /\ i > 0), cost: 1
  50: [18] -> [28] : i'=1+i, (j >= 0 \/ i <= 0), cost: 1
  37: [19] -> [5] : T, cost: 1
  53: [21] -> [22] : j'=1+j, 1+j < 0, cost: 1
  54: [21] -> [22] : i'=1+i, 1+j >= 0, cost: 1
  27: [22] -> [19] : T, cost: 1
  57: [28] -> [29] : j'=-1+j, 2*j-i > 0, cost: 1
  58: [28] -> [29] : j'=1+j, 2*j-i <= 0, cost: 1
  36: [29] -> [19] : T, cost: 1

	Loop Acceleration

	Original rule:
	[3] -> [3] : i'=2+i, j'=1+j, (-5+j < 0 /\ -2-j+i > 0 /\ -j+i >= 0 /\ i > 0), cost: 1
	New rule:
	[3] -> [3] : i'=2*n4+i, j'=j+n4, (-2-j+i > 0 /\ 6-j-n4 > 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ i > 0), cost: 1

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

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 61[(-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0)], 62[(-2-j+i > 0 /\ 6-j-n4 > 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {39[T], 61[T]}, {62[T]}]

Nonterm

Start location: [1]
Program variables: i j
  40: [1] -> [3] : i'=nondet, j'=nondet, T, cost: 1
   2: [3] -> [4] : i > 0, cost: 1
  39: [3] -> [34] : i <= 0, cost: 1
  59: [3] -> [3] : i'=n+i, j'=2*n+j, (1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0), cost: 1
  60: [3] -> [3] : i'=n2+i, j'=-n2+j, (-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0), cost: 1
  61: [3] -> [3] : i'=n3+i, j'=-n3+j, (-1+n3 >= 0 /\ -4-n3+j >= 0 /\ -j+i >= 0 /\ i > 0), cost: 1
  62: [3] -> [3] : i'=2*n4+i, j'=j+n4, (-2-j+i > 0 /\ 6-j-n4 > 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ i > 0), cost: 1
  63: [3] -> LoAT_sink : (-1+n31 >= 0 /\ n31-n4 <= 0 /\ 6+n31-j-n4 > 0 /\ -2+2*n31-j+i > 0 /\ 2*n31-j+i >= 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ n31+i > 0 /\ -4-n31+j >= 0 /\ i > 0), cost: NONTERM
  64: [3] -> [3] : i'=n31*n5+2*n5*n4+i, j'=-n31*n5+j+n5*n4, (-1+n31 >= 0 /\ -1+n5 >= 0 /\ 6+n31-j-n4 > 0 /\ -2+2*n31-j+i > 0 /\ -4-n31+(-1+n5)*n4+j-n31*(-1+n5) >= 0 /\ 2*n31-j+i >= 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ n31+i > 0 /\ -4-n31+j >= 0 /\ i > 0), cost: 1
  18: [4] -> [18] : -j+i < 0, cost: 1
  41: [4] -> [7] : i'=1+i, -j+i >= 0, cost: 1
  38: [5] -> [3] : T, cost: 1
  42: [7] -> [10] : j'=1+j, -5+j < 0, cost: 1
  44: [7] -> [8] : j'=-1+j, -5+j >= 0, cost: 1
  17: [8] -> [5] : T, cost: 1
  47: [10] -> [11] : i'=1+i, -2-j+i > 0, cost: 1
  48: [10] -> [11] : j'=1+j, -2-j+i <= 0, cost: 1
  13: [11] -> [8] : T, cost: 1
  49: [18] -> [21] : i'=-1+i, (j < 0 /\ i > 0), cost: 1
  50: [18] -> [28] : i'=1+i, (j >= 0 \/ i <= 0), cost: 1
  37: [19] -> [5] : T, cost: 1
  53: [21] -> [22] : j'=1+j, 1+j < 0, cost: 1
  54: [21] -> [22] : i'=1+i, 1+j >= 0, cost: 1
  27: [22] -> [19] : T, cost: 1
  57: [28] -> [29] : j'=-1+j, 2*j-i > 0, cost: 1
  58: [28] -> [29] : j'=1+j, 2*j-i <= 0, cost: 1
  36: [29] -> [19] : T, cost: 1

	Certificate of Non-Termination

	Original rule:
	[3] -> [3] : i'=n31+2*n4+i, j'=-n31+j+n4, (-1+n31 >= 0 /\ 6+n31-j-n4 > 0 /\ -2+2*n31-j+i > 0 /\ 2*n31-j+i >= 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ n31+i > 0 /\ -4-n31+j >= 0 /\ i > 0), cost: 1
	New rule:
	[3] -> LoAT_sink : (-1+n31 >= 0 /\ n31-n4 <= 0 /\ 6+n31-j-n4 > 0 /\ -2+2*n31-j+i > 0 /\ 2*n31-j+i >= 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ n31+i > 0 /\ -4-n31+j >= 0 /\ i > 0), cost: NONTERM

		-1+n31 >= 0 [0]: monotonic increase yields -1+n31 >= 0
		
		6+n31-j-n4 > 0 [0]: monotonic increase yields 6+n31-j-n4 > 0, dependencies: -1+n31 >= 0 -4-n31+j >= 0
		
		6+n31-j-n4 > 0 [1]: eventual decrease yields (6+n31-(-1+n5)*n4-j-n4+n31*(-1+n5) > 0 /\ 6+n31-j-n4 > 0)
		
		6+n31-j-n4 > 0 [2]: eventual increase yields (-n31+n4 <= 0 /\ 6+n31-j-n4 > 0)
		
		-2+2*n31-j+i > 0 [0]: monotonic increase yields -2+2*n31-j+i > 0, dependencies: -1+n31 >= 0 -1+n4 >= 0
		
		-2+2*n31-j+i > 0 [1]: eventual decrease yields (-2+2*n31+(-1+n5)*n4-j+2*n31*(-1+n5)+i > 0 /\ -2+2*n31-j+i > 0)
		
		-2+2*n31-j+i > 0 [2]: eventual increase yields (-2*n31-n4 <= 0 /\ -2+2*n31-j+i > 0)
		
		2*n31-j+i >= 0 [0]: monotonic increase yields 2*n31-j+i >= 0, dependencies: -1+n31 >= 0 -2+2*n31-j+i > 0 -1+n4 >= 0
		
		2*n31-j+i >= 0 [1]: montonic decrease yields 2*n31+(-1+n5)*n4-j+2*n31*(-1+n5)+i >= 0, dependencies: -2+2*n31-j+i > 0
		
		2*n31-j+i >= 0 [2]: eventual increase yields (-2*n31-n4 <= 0 /\ 2*n31-j+i >= 0)
		
		-1+n4 >= 0 [0]: monotonic increase yields -1+n4 >= 0
		
		-j+i >= 0 [0]: monotonic increase yields -j+i >= 0, dependencies: -2+2*n31-j+i > 0 -1+n4 >= 0
		
		n31+i > 0 [0]: monotonic increase yields n31+i > 0, dependencies: -1+n31 >= 0 -1+n4 >= 0
		
		-4-n31+j >= 0 [0]: eventual decrease yields (-4-n31+(-1+n5)*n4+j-n31*(-1+n5) >= 0 /\ -4-n31+j >= 0)
		
		-4-n31+j >= 0 [1]: eventual increase yields (n31-n4 <= 0 /\ -4-n31+j >= 0)
		
		i > 0 [0]: monotonic increase yields i > 0, dependencies: -1+n4 >= 0 n31+i > 0
		
		Replacement map: {-1+n31 >= 0 -> -1+n31 >= 0, 6+n31-j-n4 > 0 -> 6+n31-j-n4 > 0, -2+2*n31-j+i > 0 -> -2+2*n31-j+i > 0, 2*n31-j+i >= 0 -> 2*n31-j+i >= 0, -1+n4 >= 0 -> -1+n4 >= 0, -j+i >= 0 -> -j+i >= 0, n31+i > 0 -> n31+i > 0, -4-n31+j >= 0 -> (n31-n4 <= 0 /\ -4-n31+j >= 0), i > 0 -> i > 0}

	Loop Acceleration

	Original rule:
	[3] -> [3] : i'=n31+2*n4+i, j'=-n31+j+n4, (-1+n31 >= 0 /\ 6+n31-j-n4 > 0 /\ -2+2*n31-j+i > 0 /\ 2*n31-j+i >= 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ n31+i > 0 /\ -4-n31+j >= 0 /\ i > 0), cost: 1
	New rule:
	[3] -> [3] : i'=n31*n5+2*n5*n4+i, j'=-n31*n5+j+n5*n4, (-1+n31 >= 0 /\ -1+n5 >= 0 /\ 6+n31-j-n4 > 0 /\ -2+2*n31-j+i > 0 /\ -4-n31+(-1+n5)*n4+j-n31*(-1+n5) >= 0 /\ 2*n31-j+i >= 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ n31+i > 0 /\ -4-n31+j >= 0 /\ i > 0), cost: 1

		-1+n31 >= 0 [0]: monotonic increase yields -1+n31 >= 0
		
		6+n31-j-n4 > 0 [0]: monotonic increase yields 6+n31-j-n4 > 0, dependencies: -1+n31 >= 0 -4-n31+j >= 0
		
		6+n31-j-n4 > 0 [1]: eventual decrease yields (6+n31-(-1+n5)*n4-j-n4+n31*(-1+n5) > 0 /\ 6+n31-j-n4 > 0)
		
		6+n31-j-n4 > 0 [2]: eventual increase yields (-n31+n4 <= 0 /\ 6+n31-j-n4 > 0)
		
		-2+2*n31-j+i > 0 [0]: monotonic increase yields -2+2*n31-j+i > 0, dependencies: -1+n31 >= 0 -1+n4 >= 0
		
		-2+2*n31-j+i > 0 [1]: eventual decrease yields (-2+2*n31+(-1+n5)*n4-j+2*n31*(-1+n5)+i > 0 /\ -2+2*n31-j+i > 0)
		
		-2+2*n31-j+i > 0 [2]: eventual increase yields (-2*n31-n4 <= 0 /\ -2+2*n31-j+i > 0)
		
		2*n31-j+i >= 0 [0]: monotonic increase yields 2*n31-j+i >= 0, dependencies: -1+n31 >= 0 -2+2*n31-j+i > 0 -1+n4 >= 0
		
		2*n31-j+i >= 0 [1]: montonic decrease yields 2*n31+(-1+n5)*n4-j+2*n31*(-1+n5)+i >= 0, dependencies: -2+2*n31-j+i > 0
		
		2*n31-j+i >= 0 [2]: eventual increase yields (-2*n31-n4 <= 0 /\ 2*n31-j+i >= 0)
		
		-1+n4 >= 0 [0]: monotonic increase yields -1+n4 >= 0
		
		-j+i >= 0 [0]: monotonic increase yields -j+i >= 0, dependencies: -2+2*n31-j+i > 0 -1+n4 >= 0
		
		n31+i > 0 [0]: monotonic increase yields n31+i > 0, dependencies: -1+n31 >= 0 -1+n4 >= 0
		
		-4-n31+j >= 0 [0]: eventual decrease yields (-4-n31+(-1+n5)*n4+j-n31*(-1+n5) >= 0 /\ -4-n31+j >= 0)
		
		-4-n31+j >= 0 [1]: eventual increase yields (n31-n4 <= 0 /\ -4-n31+j >= 0)
		
		i > 0 [0]: monotonic increase yields i > 0, dependencies: -1+n4 >= 0 n31+i > 0
		
		Replacement map: {-1+n31 >= 0 -> -1+n31 >= 0, 6+n31-j-n4 > 0 -> 6+n31-j-n4 > 0, -2+2*n31-j+i > 0 -> -2+2*n31-j+i > 0, 2*n31-j+i >= 0 -> 2*n31-j+i >= 0, -1+n4 >= 0 -> -1+n4 >= 0, -j+i >= 0 -> -j+i >= 0, n31+i > 0 -> n31+i > 0, -4-n31+j >= 0 -> (-4-n31+(-1+n5)*n4+j-n31*(-1+n5) >= 0 /\ -4-n31+j >= 0), i > 0 -> i > 0}

Step with 63

	Trace

	40[T], 59[(1-n-j+i >= 0 /\ 7-2*n-j > 0 /\ 2+j-i >= 0 /\ -1+n >= 0 /\ i > 0)], 60[(-1+n2 >= 0 /\ 2-3*n2+2*j-i > 0 /\ j >= 0 /\ 2-2*n2+j-i > 0 /\ i > 0)], 63[(-1+n31 >= 0 /\ n31-n4 <= 0 /\ 6+n31-j-n4 > 0 /\ -2+2*n31-j+i > 0 /\ 2*n31-j+i >= 0 /\ -1+n4 >= 0 /\ -j+i >= 0 /\ n31+i > 0 /\ -4-n31+j >= 0 /\ i > 0)]
	
	Blocked

	[{}, {39[T]}, {39[T], 59[T]}, {39[T], 60[T]}, {63[T]}]

Refute

	Counterexample

	[ i=4 j=4 ] 40 [ i=5 j=6 ] 59 [ i=6 j=5 ] 60 [ i=i j=j ] 63
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b