NO

Initial ITS

Start location: [1]
Program variables: i j
   0: [1] -> [2] : i'=nondet, T, cost: 1
   1: [2] -> [3] : j'=nondet1, T, cost: 1
   2: [3] -> [4] : T, cost: 1
  11: [3] -> [11] : _|_, cost: 1
   3: [4] -> [6] : -j+i < 0, cost: 1
   6: [4] -> [8] : -j+i >= 0, cost: 1
  10: [5] -> [3] : T, cost: 1
   4: [6] -> [7] : i'=4+i, T, cost: 1
   5: [7] -> [5] : T, cost: 1
   7: [8] -> [9] : j'=1+j, T, cost: 1
   8: [9] -> [10] : i'=2+i, T, cost: 1
   9: [10] -> [5] : T, cost: 1

Chained Linear Paths

Start location: [1]
Program variables: i j
  12: [1] -> [3] : i'=nondet, j'=nondet1, T, cost: 1
   2: [3] -> [4] : T, cost: 1
  11: [3] -> [11] : _|_, cost: 1
  15: [4] -> [5] : i'=4+i, -j+i < 0, cost: 1
  17: [4] -> [5] : i'=2+i, j'=1+j, -j+i >= 0, cost: 1
  10: [5] -> [3] : T, 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 [6] by chaining:

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

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

	Applied chaining

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

	Removed the following rules: 9 16

Step with 12

	Trace

	12[T]
	
	Blocked

	[{}, {}]

Step with 2

	Trace

	12[T], 2[T]
	
	Blocked

	[{}, {11[T]}, {}]

Step with 15

	Trace

	12[T], 2[T], 15[(-j+i < 0)]
	
	Blocked

	[{}, {11[T]}, {}, {}]

Step with 10

	Trace

	12[T], 2[T], 15[(-j+i < 0)], 10[T]
	
	Blocked

	[{}, {11[T]}, {}, {}, {}]

Accelerate

Start location: [1]
Program variables: i j
  12: [1] -> [3] : i'=nondet, j'=nondet1, T, cost: 1
   2: [3] -> [4] : T, cost: 1
  11: [3] -> [11] : _|_, cost: 1
  18: [3] -> [3] : i'=4*n+i, (-1+n >= 0 /\ 4-4*n+j-i > 0), cost: 1
  15: [4] -> [5] : i'=4+i, -j+i < 0, cost: 1
  17: [4] -> [5] : i'=2+i, j'=1+j, -j+i >= 0, cost: 1
  10: [5] -> [3] : T, cost: 1

	Loop Acceleration

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

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

	Trace

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

	[{}, {11[T]}, {18[T]}]

Step with 2

	Trace

	12[T], 18[(-1+n >= 0 /\ 4-4*n+j-i > 0)], 2[T]
	
	Blocked

	[{}, {11[T]}, {11[T], 18[T]}, {}]

Step with 15

	Trace

	12[T], 18[(-1+n >= 0 /\ 4-4*n+j-i > 0)], 2[T], 15[(-j+i < 0)]
	
	Blocked

	[{}, {11[T]}, {11[T], 18[T]}, {}, {}]

Step with 10

	Trace

	12[T], 18[(-1+n >= 0 /\ 4-4*n+j-i > 0)], 2[T], 15[(-j+i < 0)], 10[T]
	
	Blocked

	[{}, {11[T]}, {11[T], 18[T]}, {}, {}, {}]

Covered

	Trace

	12[T], 18[(-1+n >= 0 /\ 4-4*n+j-i > 0)], 2[T], 15[(-j+i < 0)]
	
	Blocked

	[{}, {11[T]}, {11[T], 18[T]}, {}, {10[T]}]

Backtrack

	Trace

	12[T], 18[(-1+n >= 0 /\ 4-4*n+j-i > 0)], 2[T]
	
	Blocked

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

Step with 17

	Trace

	12[T], 18[(-1+n >= 0 /\ 4-4*n+j-i > 0)], 2[T], 17[(-j+i >= 0)]
	
	Blocked

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

Step with 10

	Trace

	12[T], 18[(-1+n >= 0 /\ 4-4*n+j-i > 0)], 2[T], 17[(-j+i >= 0)], 10[T]
	
	Blocked

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

Nonterm

Start location: [1]
Program variables: i j
  12: [1] -> [3] : i'=nondet, j'=nondet1, T, cost: 1
   2: [3] -> [4] : T, cost: 1
  11: [3] -> [11] : _|_, cost: 1
  18: [3] -> [3] : i'=4*n+i, (-1+n >= 0 /\ 4-4*n+j-i > 0), cost: 1
  19: [3] -> LoAT_sink : (-j+i >= 0 /\ -1+n2 >= 0), cost: NONTERM
  20: [3] -> [3] : i'=2*n2+i, j'=n2+j, (-j+i >= 0 /\ -1+n2 >= 0), cost: 1
  15: [4] -> [5] : i'=4+i, -j+i < 0, cost: 1
  17: [4] -> [5] : i'=2+i, j'=1+j, -j+i >= 0, cost: 1
  10: [5] -> [3] : T, cost: 1

	Certificate of Non-Termination

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

		-j+i >= 0 [0]: monotonic increase yields -j+i >= 0
		
		Replacement map: {-j+i >= 0 -> -j+i >= 0}

	Loop Acceleration

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

		-j+i >= 0 [0]: monotonic increase yields -j+i >= 0
		
		Replacement map: {-j+i >= 0 -> -j+i >= 0}

Step with 19

	Trace

	12[T], 18[(-1+n >= 0 /\ 4-4*n+j-i > 0)], 19[(-j+i >= 0 /\ -1+n2 >= 0)]
	
	Blocked

	[{}, {11[T]}, {11[T], 18[T]}, {19[T]}]

Refute

	Counterexample

	[ i=0 j=4 ] 12 [ i=4 j=4 ] 18 [ i=i j=j ] 19
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b