NO

Initial ITS

Start location: l4
Program variables: a^0 dobreak^0 n^0 r^0
   0: l0 -> l1 : a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (0 == 0 /\ n^0 <= 0 /\ r^post1 == 0 /\ -n^post1+n^0 == 0 /\ r^1 == 0 /\ -a^post1+a^0 == 0), cost: 1
   1: l0 -> l2 : a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (dobreak^0-dobreak^post2 == 0 /\ 1-n^0 <= 0 /\ -a^post2+a^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-n^0+n^post2 == 0), cost: 1
   3: l1 -> l0 : a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (dobreak^0 <= 0 /\ -1+a^1 == 0 /\ -n^post4+n^0 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ -r^post4+r^0 == 0 /\ a^post4 == 0), cost: 1
   2: l2 -> l0 : a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (n^0-n^post3 == 0 /\ -a^post3+a^0 == 0 /\ -r^post3+r^0 == 0 /\ dobreak^0-dobreak^post3 == 0), cost: 1
   4: l3 -> l1 : a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (0 == 0 /\ a^post5 == 0 /\ r^post5 == 0), cost: 1
   5: l4 -> l3 : a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (-r^post6+r^0 == 0 /\ n^0-n^post6 == 0 /\ dobreak^0-dobreak^post6 == 0 /\ -a^post6+a^0 == 0), cost: 1

Chained Linear Paths

Start location: l4
Program variables: a^0 dobreak^0 n^0 r^0
   0: l0 -> l1 : a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (0 == 0 /\ n^0 <= 0 /\ r^post1 == 0 /\ -n^post1+n^0 == 0 /\ r^1 == 0 /\ -a^post1+a^0 == 0), cost: 1
   7: l0 -> l0 : a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (dobreak^0-dobreak^post2 == 0 /\ 1-n^0 <= 0 /\ n^post2-n^post3 == 0 /\ dobreak^post2-dobreak^post3 == 0 /\ -a^post2+a^0 == 0 /\ -r^post2+r^0 == 0 /\ a^post2-a^post3 == 0 /\ r^post2-r^post3 == 0 /\ 1-n^0+n^post2 == 0), cost: 1
   3: l1 -> l0 : a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (dobreak^0 <= 0 /\ -1+a^1 == 0 /\ -n^post4+n^0 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ -r^post4+r^0 == 0 /\ a^post4 == 0), cost: 1
   6: l4 -> l1 : a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (0 == 0 /\ a^post5 == 0 /\ -r^post6+r^0 == 0 /\ n^0-n^post6 == 0 /\ dobreak^0-dobreak^post6 == 0 /\ r^post5 == 0 /\ -a^post6+a^0 == 0), cost: 1

	Eliminating location l3 by chaining:

	Applied chaining

	First rule:
	l4 -> l3 : a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (-r^post6+r^0 == 0 /\ n^0-n^post6 == 0 /\ dobreak^0-dobreak^post6 == 0 /\ -a^post6+a^0 == 0), cost: 1
	Second rule:
	l3 -> l1 : a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (0 == 0 /\ a^post5 == 0 /\ r^post5 == 0), cost: 1
	New rule:
	l4 -> l1 : a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (0 == 0 /\ a^post5 == 0 /\ -r^post6+r^0 == 0 /\ n^0-n^post6 == 0 /\ dobreak^0-dobreak^post6 == 0 /\ r^post5 == 0 /\ -a^post6+a^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 4 5
	
	Eliminating location l2 by chaining:

	Applied chaining

	First rule:
	l0 -> l2 : a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (dobreak^0-dobreak^post2 == 0 /\ 1-n^0 <= 0 /\ -a^post2+a^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-n^0+n^post2 == 0), cost: 1
	Second rule:
	l2 -> l0 : a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (n^0-n^post3 == 0 /\ -a^post3+a^0 == 0 /\ -r^post3+r^0 == 0 /\ dobreak^0-dobreak^post3 == 0), cost: 1
	New rule:
	l0 -> l0 : a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (dobreak^0-dobreak^post2 == 0 /\ 1-n^0 <= 0 /\ n^post2-n^post3 == 0 /\ dobreak^post2-dobreak^post3 == 0 /\ -a^post2+a^0 == 0 /\ -r^post2+r^0 == 0 /\ a^post2-a^post3 == 0 /\ r^post2-r^post3 == 0 /\ 1-n^0+n^post2 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 1 2

Simplified Transitions

Start location: l4
Program variables: a^0 dobreak^0 n^0 r^0
   8: l0 -> l1 : dobreak^0'=dobreak^post1, r^0'=0, n^0 <= 0, cost: 1
  11: l0 -> l0 : n^0'=-1+n^0, 1-n^0 <= 0, cost: 1
   9: l1 -> l0 : a^0'=0, dobreak^0 <= 0, cost: 1
  10: l4 -> l1 : a^0'=0, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=0, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (0 == 0 /\ n^0 <= 0 /\ r^post1 == 0 /\ -n^post1+n^0 == 0 /\ r^1 == 0 /\ -a^post1+a^0 == 0), cost: 1
	New rule:
	l0 -> l1 : a^0'=a^0, dobreak^0'=dobreak^post1, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0 /\ r^1 == 0), cost: 1
	
		propagated equality r^post1 = 0
		
		propagated equality n^post1 = n^0
		
		propagated equality a^post1 = a^0
		
	Propagated Equalities

	Original rule:
	l0 -> l1 : a^0'=a^0, dobreak^0'=dobreak^post1, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0 /\ r^1 == 0), cost: 1
	New rule:
	l0 -> l1 : a^0'=a^0, dobreak^0'=dobreak^post1, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0), cost: 1
	
		propagated equality r^1 = 0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : a^0'=a^0, dobreak^0'=dobreak^post1, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : a^0'=a^0, dobreak^0'=dobreak^post1, n^0'=n^0, r^0'=0, n^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : a^0'=a^0, dobreak^0'=dobreak^post1, n^0'=n^0, r^0'=0, n^0 <= 0, cost: 1
	New rule:
	l0 -> l1 : dobreak^0'=dobreak^post1, r^0'=0, n^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l0 : a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (dobreak^0 <= 0 /\ -1+a^1 == 0 /\ -n^post4+n^0 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ -r^post4+r^0 == 0 /\ a^post4 == 0), cost: 1
	New rule:
	l1 -> l0 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0), cost: 1
	
		propagated equality n^post4 = n^0
		
		propagated equality dobreak^post4 = dobreak^0
		
		propagated equality r^post4 = r^0
		
		propagated equality a^post4 = 0
		
	Propagated Equalities

	Original rule:
	l1 -> l0 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0), cost: 1
	New rule:
	l1 -> l0 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0), cost: 1
	
		propagated equality a^1 = 1
		
	Simplified Guard

	Original rule:
	l1 -> l0 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0), cost: 1
	New rule:
	l1 -> l0 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, dobreak^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l0 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, dobreak^0 <= 0, cost: 1
	New rule:
	l1 -> l0 : a^0'=0, dobreak^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l1 : a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (0 == 0 /\ a^post5 == 0 /\ -r^post6+r^0 == 0 /\ n^0-n^post6 == 0 /\ dobreak^0-dobreak^post6 == 0 /\ r^post5 == 0 /\ -a^post6+a^0 == 0), cost: 1
	New rule:
	l4 -> l1 : a^0'=0, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=0, (0 == 0 /\ -r^post6+r^0 == 0 /\ n^0-n^post6 == 0 /\ dobreak^0-dobreak^post6 == 0 /\ -a^post6+a^0 == 0), cost: 1
	
		propagated equality a^post5 = 0
		
		propagated equality r^post5 = 0
		
	Propagated Equalities

	Original rule:
	l4 -> l1 : a^0'=0, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=0, (0 == 0 /\ -r^post6+r^0 == 0 /\ n^0-n^post6 == 0 /\ dobreak^0-dobreak^post6 == 0 /\ -a^post6+a^0 == 0), cost: 1
	New rule:
	l4 -> l1 : a^0'=0, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=0, 0 == 0, cost: 1
	
		propagated equality r^post6 = r^0
		
		propagated equality n^post6 = n^0
		
		propagated equality dobreak^post6 = dobreak^0
		
		propagated equality a^post6 = a^0
		
	Simplified Guard

	Original rule:
	l4 -> l1 : a^0'=0, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=0, 0 == 0, cost: 1
	New rule:
	l4 -> l1 : a^0'=0, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l0 : a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (dobreak^0-dobreak^post2 == 0 /\ 1-n^0 <= 0 /\ n^post2-n^post3 == 0 /\ dobreak^post2-dobreak^post3 == 0 /\ -a^post2+a^0 == 0 /\ -r^post2+r^0 == 0 /\ a^post2-a^post3 == 0 /\ r^post2-r^post3 == 0 /\ 1-n^0+n^post2 == 0), cost: 1
	New rule:
	l0 -> l0 : a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (0 == 0 /\ dobreak^0-dobreak^post2 == 0 /\ 1-n^0 <= 0 /\ -a^post2+a^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-n^0+n^post2 == 0), cost: 1
	
		propagated equality n^post3 = n^post2
		
		propagated equality dobreak^post3 = dobreak^post2
		
		propagated equality a^post3 = a^post2
		
		propagated equality r^post3 = r^post2
		
	Propagated Equalities

	Original rule:
	l0 -> l0 : a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (0 == 0 /\ dobreak^0-dobreak^post2 == 0 /\ 1-n^0 <= 0 /\ -a^post2+a^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-n^0+n^post2 == 0), cost: 1
	New rule:
	l0 -> l0 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=-1+n^0, r^0'=r^0, (0 == 0 /\ 1-n^0 <= 0), cost: 1
	
		propagated equality dobreak^post2 = dobreak^0
		
		propagated equality a^post2 = a^0
		
		propagated equality r^post2 = r^0
		
		propagated equality n^post2 = -1+n^0
		
	Simplified Guard

	Original rule:
	l0 -> l0 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=-1+n^0, r^0'=r^0, (0 == 0 /\ 1-n^0 <= 0), cost: 1
	New rule:
	l0 -> l0 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=-1+n^0, r^0'=r^0, 1-n^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l0 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=-1+n^0, r^0'=r^0, 1-n^0 <= 0, cost: 1
	New rule:
	l0 -> l0 : n^0'=-1+n^0, 1-n^0 <= 0, cost: 1

Step with 10

	Trace

	10[T]
	
	Blocked

	[{}, {}]

Step with 9

	Trace

	10[T], 9[(dobreak^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Step with 8

	Trace

	10[T], 9[(dobreak^0 <= 0)], 8[(n^0 <= 0)]
	
	Blocked

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

Nonterm

Start location: l4
Program variables: a^0 dobreak^0 n^0 r^0
   8: l0 -> l1 : dobreak^0'=dobreak^post1, r^0'=0, n^0 <= 0, cost: 1
  11: l0 -> l0 : n^0'=-1+n^0, 1-n^0 <= 0, cost: 1
   9: l1 -> l0 : a^0'=0, dobreak^0 <= 0, cost: 1
  12: l1 -> LoAT_sink : (-dobreak^0 >= 0 /\ -n^0 >= 0 /\ dobreak^post1-dobreak^0 <= 0), cost: NONTERM
  10: l4 -> l1 : a^0'=0, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=0, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l1 -> l1 : a^0'=0, dobreak^0'=dobreak^post1, r^0'=0, (dobreak^0 <= 0 /\ n^0 <= 0), cost: 1
	New rule:
	l1 -> LoAT_sink : (-dobreak^0 >= 0 /\ -n^0 >= 0 /\ dobreak^post1-dobreak^0 <= 0), cost: NONTERM

		-dobreak^0 >= 0 [0]: eventual decrease yields (-dobreak^post1 >= 0 /\ -dobreak^0 >= 0)
		
		-dobreak^0 >= 0 [1]: eventual increase yields (-dobreak^0 >= 0 /\ dobreak^post1-dobreak^0 <= 0)
		
		-n^0 >= 0 [0]: monotonic increase yields -n^0 >= 0
		
		Replacement map: {-dobreak^0 >= 0 -> (-dobreak^0 >= 0 /\ dobreak^post1-dobreak^0 <= 0), -n^0 >= 0 -> -n^0 >= 0}

Step with 12

	Trace

	10[T], 12[(-dobreak^0 >= 0 /\ -n^0 >= 0 /\ dobreak^post1-dobreak^0 <= 0)]
	
	Blocked

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

Refute

	Counterexample

	[ a^0=0 dobreak^0=0 n^0=0 r^0=0 ] 10 [ a^0=a^0 dobreak^0=dobreak^0 n^0=n^0 r^0=r^0 ] 12
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b