NO

Initial ITS

Start location: l6
Program variables: __const_10^0 i^0 j^0 temp^0
   0: l0 -> l1 : __const_10^0'=__const_10^post1, i^0'=i^post1, j^0'=j^post1, temp^0'=temp^post1, (-temp^post1+temp^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -j^post1+j^0 == 0 /\ i^0-i^post1 == 0), cost: 1
   4: l1 -> l4 : __const_10^0'=__const_10^post5, i^0'=i^post5, j^0'=j^post5, temp^0'=temp^post5, (1-i^0+__const_10^0 <= 0 /\ -j^post5+j^0 == 0 /\ -__const_10^post5+__const_10^0 == 0 /\ -temp^post5+temp^0 == 0 /\ i^0-i^post5 == 0), cost: 1
   5: l1 -> l2 : __const_10^0'=__const_10^post6, i^0'=i^post6, j^0'=j^post6, temp^0'=temp^post6, (i^0-__const_10^0 <= 0 /\ temp^0-temp^post6 == 0 /\ i^0-i^post6 == 0 /\ j^post6-i^0 == 0 /\ -__const_10^post6+__const_10^0 == 0), cost: 1
   1: l2 -> l3 : __const_10^0'=__const_10^post2, i^0'=i^post2, j^0'=j^post2, temp^0'=temp^post2, (temp^0-temp^post2 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -j^post2+j^0 == 0 /\ -i^post2+i^0 == 0), cost: 1
   2: l3 -> l2 : __const_10^0'=__const_10^post3, i^0'=i^post3, j^0'=j^post3, temp^0'=temp^post3, (0 == 0 /\ 1+j^post3-j^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ i^0-i^post3 == 0), cost: 1
   3: l3 -> l0 : __const_10^0'=__const_10^post4, i^0'=i^post4, j^0'=j^post4, temp^0'=temp^post4, (-__const_10^post4+__const_10^0 == 0 /\ -j^post4+j^0 == 0 /\ -temp^post4+temp^0 == 0 /\ -1-i^0+i^post4 == 0), cost: 1
   6: l5 -> l0 : __const_10^0'=__const_10^post7, i^0'=i^post7, j^0'=j^post7, temp^0'=temp^post7, (-j^post7+j^0 == 0 /\ __const_10^0-__const_10^post7 == 0 /\ -2+i^post7 == 0 /\ temp^0-temp^post7 == 0), cost: 1
   7: l6 -> l5 : __const_10^0'=__const_10^post8, i^0'=i^post8, j^0'=j^post8, temp^0'=temp^post8, (-temp^post8+temp^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ i^0-i^post8 == 0), cost: 1

Chained Linear Paths

Start location: l6
Program variables: __const_10^0 i^0 j^0 temp^0
   0: l0 -> l1 : __const_10^0'=__const_10^post1, i^0'=i^post1, j^0'=j^post1, temp^0'=temp^post1, (-temp^post1+temp^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -j^post1+j^0 == 0 /\ i^0-i^post1 == 0), cost: 1
   4: l1 -> l4 : __const_10^0'=__const_10^post5, i^0'=i^post5, j^0'=j^post5, temp^0'=temp^post5, (1-i^0+__const_10^0 <= 0 /\ -j^post5+j^0 == 0 /\ -__const_10^post5+__const_10^0 == 0 /\ -temp^post5+temp^0 == 0 /\ i^0-i^post5 == 0), cost: 1
   5: l1 -> l2 : __const_10^0'=__const_10^post6, i^0'=i^post6, j^0'=j^post6, temp^0'=temp^post6, (i^0-__const_10^0 <= 0 /\ temp^0-temp^post6 == 0 /\ i^0-i^post6 == 0 /\ j^post6-i^0 == 0 /\ -__const_10^post6+__const_10^0 == 0), cost: 1
   1: l2 -> l3 : __const_10^0'=__const_10^post2, i^0'=i^post2, j^0'=j^post2, temp^0'=temp^post2, (temp^0-temp^post2 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -j^post2+j^0 == 0 /\ -i^post2+i^0 == 0), cost: 1
   2: l3 -> l2 : __const_10^0'=__const_10^post3, i^0'=i^post3, j^0'=j^post3, temp^0'=temp^post3, (0 == 0 /\ 1+j^post3-j^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ i^0-i^post3 == 0), cost: 1
   3: l3 -> l0 : __const_10^0'=__const_10^post4, i^0'=i^post4, j^0'=j^post4, temp^0'=temp^post4, (-__const_10^post4+__const_10^0 == 0 /\ -j^post4+j^0 == 0 /\ -temp^post4+temp^0 == 0 /\ -1-i^0+i^post4 == 0), cost: 1
   8: l6 -> l0 : __const_10^0'=__const_10^post7, i^0'=i^post7, j^0'=j^post7, temp^0'=temp^post7, (-temp^post8+temp^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ i^0-i^post8 == 0 /\ -2+i^post7 == 0 /\ -j^post7+j^post8 == 0 /\ __const_10^post8-__const_10^post7 == 0 /\ temp^post8-temp^post7 == 0), cost: 1

	Eliminating location l5 by chaining:

	Applied chaining

	First rule:
	l6 -> l5 : __const_10^0'=__const_10^post8, i^0'=i^post8, j^0'=j^post8, temp^0'=temp^post8, (-temp^post8+temp^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ i^0-i^post8 == 0), cost: 1
	Second rule:
	l5 -> l0 : __const_10^0'=__const_10^post7, i^0'=i^post7, j^0'=j^post7, temp^0'=temp^post7, (-j^post7+j^0 == 0 /\ __const_10^0-__const_10^post7 == 0 /\ -2+i^post7 == 0 /\ temp^0-temp^post7 == 0), cost: 1
	New rule:
	l6 -> l0 : __const_10^0'=__const_10^post7, i^0'=i^post7, j^0'=j^post7, temp^0'=temp^post7, (-temp^post8+temp^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ i^0-i^post8 == 0 /\ -2+i^post7 == 0 /\ -j^post7+j^post8 == 0 /\ __const_10^post8-__const_10^post7 == 0 /\ temp^post8-temp^post7 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 6 7

Simplified Transitions

Start location: l6
Program variables: __const_10^0 i^0 j^0 temp^0
   9: l0 -> l1 : T, cost: 1
  13: l1 -> l4 : 1-i^0+__const_10^0 <= 0, cost: 1
  14: l1 -> l2 : j^0'=i^0, i^0-__const_10^0 <= 0, cost: 1
  10: l2 -> l3 : T, cost: 1
  11: l3 -> l2 : j^0'=-1+j^0, temp^0'=temp^post3, T, cost: 1
  12: l3 -> l0 : i^0'=1+i^0, T, cost: 1
  15: l6 -> l0 : i^0'=2, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : __const_10^0'=__const_10^post1, i^0'=i^post1, j^0'=j^post1, temp^0'=temp^post1, (-temp^post1+temp^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -j^post1+j^0 == 0 /\ i^0-i^post1 == 0), cost: 1
	New rule:
	l0 -> l1 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, 0 == 0, cost: 1
	
		propagated equality temp^post1 = temp^0
		
		propagated equality __const_10^post1 = __const_10^0
		
		propagated equality j^post1 = j^0
		
		propagated equality i^post1 = i^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, 0 == 0, cost: 1
	New rule:
	l0 -> l1 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, T, cost: 1
	New rule:
	l0 -> l1 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l3 : __const_10^0'=__const_10^post2, i^0'=i^post2, j^0'=j^post2, temp^0'=temp^post2, (temp^0-temp^post2 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -j^post2+j^0 == 0 /\ -i^post2+i^0 == 0), cost: 1
	New rule:
	l2 -> l3 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, 0 == 0, cost: 1
	
		propagated equality temp^post2 = temp^0
		
		propagated equality __const_10^post2 = __const_10^0
		
		propagated equality j^post2 = j^0
		
		propagated equality i^post2 = i^0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, 0 == 0, cost: 1
	New rule:
	l2 -> l3 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, T, cost: 1
	New rule:
	l2 -> l3 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l2 : __const_10^0'=__const_10^post3, i^0'=i^post3, j^0'=j^post3, temp^0'=temp^post3, (0 == 0 /\ 1+j^post3-j^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ i^0-i^post3 == 0), cost: 1
	New rule:
	l3 -> l2 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=-1+j^0, temp^0'=temp^post3, 0 == 0, cost: 1
	
		propagated equality j^post3 = -1+j^0
		
		propagated equality __const_10^post3 = __const_10^0
		
		propagated equality i^post3 = i^0
		
	Simplified Guard

	Original rule:
	l3 -> l2 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=-1+j^0, temp^0'=temp^post3, 0 == 0, cost: 1
	New rule:
	l3 -> l2 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=-1+j^0, temp^0'=temp^post3, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l2 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=-1+j^0, temp^0'=temp^post3, T, cost: 1
	New rule:
	l3 -> l2 : j^0'=-1+j^0, temp^0'=temp^post3, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l0 : __const_10^0'=__const_10^post4, i^0'=i^post4, j^0'=j^post4, temp^0'=temp^post4, (-__const_10^post4+__const_10^0 == 0 /\ -j^post4+j^0 == 0 /\ -temp^post4+temp^0 == 0 /\ -1-i^0+i^post4 == 0), cost: 1
	New rule:
	l3 -> l0 : __const_10^0'=__const_10^0, i^0'=1+i^0, j^0'=j^0, temp^0'=temp^0, 0 == 0, cost: 1
	
		propagated equality __const_10^post4 = __const_10^0
		
		propagated equality j^post4 = j^0
		
		propagated equality temp^post4 = temp^0
		
		propagated equality i^post4 = 1+i^0
		
	Simplified Guard

	Original rule:
	l3 -> l0 : __const_10^0'=__const_10^0, i^0'=1+i^0, j^0'=j^0, temp^0'=temp^0, 0 == 0, cost: 1
	New rule:
	l3 -> l0 : __const_10^0'=__const_10^0, i^0'=1+i^0, j^0'=j^0, temp^0'=temp^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l0 : __const_10^0'=__const_10^0, i^0'=1+i^0, j^0'=j^0, temp^0'=temp^0, T, cost: 1
	New rule:
	l3 -> l0 : i^0'=1+i^0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l4 : __const_10^0'=__const_10^post5, i^0'=i^post5, j^0'=j^post5, temp^0'=temp^post5, (1-i^0+__const_10^0 <= 0 /\ -j^post5+j^0 == 0 /\ -__const_10^post5+__const_10^0 == 0 /\ -temp^post5+temp^0 == 0 /\ i^0-i^post5 == 0), cost: 1
	New rule:
	l1 -> l4 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, (0 == 0 /\ 1-i^0+__const_10^0 <= 0), cost: 1
	
		propagated equality j^post5 = j^0
		
		propagated equality __const_10^post5 = __const_10^0
		
		propagated equality temp^post5 = temp^0
		
		propagated equality i^post5 = i^0
		
	Simplified Guard

	Original rule:
	l1 -> l4 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, (0 == 0 /\ 1-i^0+__const_10^0 <= 0), cost: 1
	New rule:
	l1 -> l4 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, 1-i^0+__const_10^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l4 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=j^0, temp^0'=temp^0, 1-i^0+__const_10^0 <= 0, cost: 1
	New rule:
	l1 -> l4 : 1-i^0+__const_10^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l2 : __const_10^0'=__const_10^post6, i^0'=i^post6, j^0'=j^post6, temp^0'=temp^post6, (i^0-__const_10^0 <= 0 /\ temp^0-temp^post6 == 0 /\ i^0-i^post6 == 0 /\ j^post6-i^0 == 0 /\ -__const_10^post6+__const_10^0 == 0), cost: 1
	New rule:
	l1 -> l2 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=i^0, temp^0'=temp^0, (0 == 0 /\ i^0-__const_10^0 <= 0), cost: 1
	
		propagated equality temp^post6 = temp^0
		
		propagated equality i^post6 = i^0
		
		propagated equality j^post6 = i^0
		
		propagated equality __const_10^post6 = __const_10^0
		
	Simplified Guard

	Original rule:
	l1 -> l2 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=i^0, temp^0'=temp^0, (0 == 0 /\ i^0-__const_10^0 <= 0), cost: 1
	New rule:
	l1 -> l2 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=i^0, temp^0'=temp^0, i^0-__const_10^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l2 : __const_10^0'=__const_10^0, i^0'=i^0, j^0'=i^0, temp^0'=temp^0, i^0-__const_10^0 <= 0, cost: 1
	New rule:
	l1 -> l2 : j^0'=i^0, i^0-__const_10^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l0 : __const_10^0'=__const_10^post7, i^0'=i^post7, j^0'=j^post7, temp^0'=temp^post7, (-temp^post8+temp^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ i^0-i^post8 == 0 /\ -2+i^post7 == 0 /\ -j^post7+j^post8 == 0 /\ __const_10^post8-__const_10^post7 == 0 /\ temp^post8-temp^post7 == 0), cost: 1
	New rule:
	l6 -> l0 : __const_10^0'=__const_10^post8, i^0'=2, j^0'=j^post8, temp^0'=temp^post8, (0 == 0 /\ -temp^post8+temp^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ i^0-i^post8 == 0), cost: 1
	
		propagated equality i^post7 = 2
		
		propagated equality j^post7 = j^post8
		
		propagated equality __const_10^post7 = __const_10^post8
		
		propagated equality temp^post7 = temp^post8
		
	Propagated Equalities

	Original rule:
	l6 -> l0 : __const_10^0'=__const_10^post8, i^0'=2, j^0'=j^post8, temp^0'=temp^post8, (0 == 0 /\ -temp^post8+temp^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ i^0-i^post8 == 0), cost: 1
	New rule:
	l6 -> l0 : __const_10^0'=__const_10^0, i^0'=2, j^0'=j^0, temp^0'=temp^0, 0 == 0, cost: 1
	
		propagated equality temp^post8 = temp^0
		
		propagated equality j^post8 = j^0
		
		propagated equality __const_10^post8 = __const_10^0
		
		propagated equality i^post8 = i^0
		
	Simplified Guard

	Original rule:
	l6 -> l0 : __const_10^0'=__const_10^0, i^0'=2, j^0'=j^0, temp^0'=temp^0, 0 == 0, cost: 1
	New rule:
	l6 -> l0 : __const_10^0'=__const_10^0, i^0'=2, j^0'=j^0, temp^0'=temp^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l0 : __const_10^0'=__const_10^0, i^0'=2, j^0'=j^0, temp^0'=temp^0, T, cost: 1
	New rule:
	l6 -> l0 : i^0'=2, T, cost: 1

Step with 15

	Trace

	15[T]
	
	Blocked

	[{}, {}]

Step with 9

	Trace

	15[T], 9[T]
	
	Blocked

	[{}, {}, {}]

Step with 13

	Trace

	15[T], 9[T], 13[(1-i^0+__const_10^0 <= 0)]
	
	Blocked

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

Backtrack

	Trace

	15[T], 9[T]
	
	Blocked

	[{}, {}, {13[T]}]

Step with 14

	Trace

	15[T], 9[T], 14[(i^0-__const_10^0 <= 0)]
	
	Blocked

	[{}, {}, {13[T]}, {}]

Step with 10

	Trace

	15[T], 9[T], 14[(i^0-__const_10^0 <= 0)], 10[T]
	
	Blocked

	[{}, {}, {13[T]}, {}, {}]

Step with 11

	Trace

	15[T], 9[T], 14[(i^0-__const_10^0 <= 0)], 10[T], 11[T]
	
	Blocked

	[{}, {}, {13[T]}, {}, {}, {}]

Nonterm

Start location: l6
Program variables: __const_10^0 i^0 j^0 temp^0
   9: l0 -> l1 : T, cost: 1
  13: l1 -> l4 : 1-i^0+__const_10^0 <= 0, cost: 1
  14: l1 -> l2 : j^0'=i^0, i^0-__const_10^0 <= 0, cost: 1
  10: l2 -> l3 : T, cost: 1
  16: l2 -> LoAT_sink : -1+n >= 0, cost: NONTERM
  17: l2 -> l2 : j^0'=-n+j^0, temp^0'=temp^post3, -1+n >= 0, cost: 1
  11: l3 -> l2 : j^0'=-1+j^0, temp^0'=temp^post3, T, cost: 1
  12: l3 -> l0 : i^0'=1+i^0, T, cost: 1
  15: l6 -> l0 : i^0'=2, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l2 -> l2 : j^0'=-1+j^0, temp^0'=temp^post3, T, cost: 1
	New rule:
	l2 -> LoAT_sink : -1+n >= 0, cost: NONTERM

		Replacement map: {}

	Loop Acceleration

	Original rule:
	l2 -> l2 : j^0'=-1+j^0, temp^0'=temp^post3, T, cost: 1
	New rule:
	l2 -> l2 : j^0'=-n+j^0, temp^0'=temp^post3, -1+n >= 0, cost: 1

		Replacement map: {}

Step with 16

	Trace

	15[T], 9[T], 14[(i^0-__const_10^0 <= 0)], 16[-1+n >= 0]
	
	Blocked

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

Refute

	Counterexample

	[ __const_10^0=2 i^0=2 j^0=0 temp^0=0 ] 15 [ __const_10^0=2 i^0=2 j^0=0 temp^0=0 ] 9 [ __const_10^0=2 i^0=2 j^0=2 temp^0=0 ] 14 [ __const_10^0=2 i^0=i^0 j^0=0 temp^0=0 ] 16
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b