NO

Initial ITS

Start location: l14
Program variables: tmp1^0 witemsnum^0
   0: l0 -> l1 : tmp1^0'=tmp1^post1, witemsnum^0'=witemsnum^post1, (-witemsnum^post1+witemsnum^0 == 0 /\ -tmp1^post1+tmp1^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
   1: l0 -> l2 : tmp1^0'=tmp1^post2, witemsnum^0'=witemsnum^post2, (0 == 0 /\ -witemsnum^post2+witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
  11: l1 -> l5 : tmp1^0'=tmp1^post12, witemsnum^0'=witemsnum^post12, (-tmp1^post12+tmp1^0 == 0 /\ -witemsnum^post12+witemsnum^0 == 0), cost: 1
  14: l2 -> l1 : tmp1^0'=tmp1^post15, witemsnum^0'=witemsnum^post15, (tmp1^0 <= 0 /\ -tmp1^0 <= 0 /\ -witemsnum^post15+witemsnum^0 == 0 /\ tmp1^0-tmp1^post15 == 0), cost: 1
  15: l2 -> l12 : tmp1^0'=tmp1^post16, witemsnum^0'=witemsnum^post16, (witemsnum^0-witemsnum^post16 == 0 /\ 1-tmp1^0 <= 0 /\ tmp1^0-tmp1^post16 == 0), cost: 1
  16: l2 -> l12 : tmp1^0'=tmp1^post17, witemsnum^0'=witemsnum^post17, (1+tmp1^0 <= 0 /\ -witemsnum^post17+witemsnum^0 == 0 /\ -tmp1^post17+tmp1^0 == 0), cost: 1
   2: l3 -> l4 : tmp1^0'=tmp1^post3, witemsnum^0'=witemsnum^post3, (witemsnum^0-witemsnum^post3 == 0 /\ tmp1^0-tmp1^post3 == 0), cost: 1
   3: l4 -> l0 : tmp1^0'=tmp1^post4, witemsnum^0'=witemsnum^post4, (-witemsnum^post4+witemsnum^0 == 0 /\ -tmp1^post4+tmp1^0 == 0), cost: 1
   4: l5 -> l6 : tmp1^0'=tmp1^post5, witemsnum^0'=witemsnum^post5, (-witemsnum^post5+witemsnum^0 == 0 /\ tmp1^0-tmp1^post5 == 0), cost: 1
   7: l6 -> l3 : tmp1^0'=tmp1^post8, witemsnum^0'=witemsnum^post8, (tmp1^0-tmp1^post8 == 0 /\ witemsnum^0-witemsnum^post8 == 0 /\ -2+witemsnum^0 <= 0), cost: 1
   8: l6 -> l5 : tmp1^0'=tmp1^post9, witemsnum^0'=witemsnum^post9, (3-witemsnum^0 <= 0 /\ 1+witemsnum^post9-witemsnum^0 == 0 /\ -tmp1^post9+tmp1^0 == 0), cost: 1
   5: l7 -> l8 : tmp1^0'=tmp1^post6, witemsnum^0'=witemsnum^post6, (tmp1^0-tmp1^post6 == 0 /\ witemsnum^0-witemsnum^post6 == 0), cost: 1
   6: l9 -> l10 : tmp1^0'=tmp1^post7, witemsnum^0'=witemsnum^post7, (-witemsnum^post7+witemsnum^0 == 0 /\ -tmp1^post7+tmp1^0 == 0), cost: 1
   9: l10 -> l11 : tmp1^0'=tmp1^post10, witemsnum^0'=witemsnum^post10, (tmp1^0-tmp1^post10 == 0 /\ -witemsnum^post10+witemsnum^0 == 0), cost: 1
  10: l11 -> l10 : tmp1^0'=tmp1^post11, witemsnum^0'=witemsnum^post11, (tmp1^0-tmp1^post11 == 0 /\ witemsnum^0-witemsnum^post11 == 0), cost: 1
  12: l12 -> l4 : tmp1^0'=tmp1^post13, witemsnum^0'=witemsnum^post13, (tmp1^0-tmp1^post13 == 0 /\ -1-witemsnum^0+witemsnum^post13 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
  13: l12 -> l4 : tmp1^0'=tmp1^post14, witemsnum^0'=witemsnum^post14, (-tmp1^post14+tmp1^0 == 0 /\ -1+witemsnum^post14-witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
  17: l13 -> l3 : tmp1^0'=tmp1^post18, witemsnum^0'=witemsnum^post18, (0 == 0 /\ -tmp1^post18+tmp1^0 == 0), cost: 1
  18: l14 -> l13 : tmp1^0'=tmp1^post19, witemsnum^0'=witemsnum^post19, (tmp1^0-tmp1^post19 == 0 /\ witemsnum^0-witemsnum^post19 == 0), cost: 1

Chained Linear Paths

Start location: l14
Program variables: tmp1^0 witemsnum^0
   0: l0 -> l1 : tmp1^0'=tmp1^post1, witemsnum^0'=witemsnum^post1, (-witemsnum^post1+witemsnum^0 == 0 /\ -tmp1^post1+tmp1^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
   1: l0 -> l2 : tmp1^0'=tmp1^post2, witemsnum^0'=witemsnum^post2, (0 == 0 /\ -witemsnum^post2+witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
  11: l1 -> l5 : tmp1^0'=tmp1^post12, witemsnum^0'=witemsnum^post12, (-tmp1^post12+tmp1^0 == 0 /\ -witemsnum^post12+witemsnum^0 == 0), cost: 1
  14: l2 -> l1 : tmp1^0'=tmp1^post15, witemsnum^0'=witemsnum^post15, (tmp1^0 <= 0 /\ -tmp1^0 <= 0 /\ -witemsnum^post15+witemsnum^0 == 0 /\ tmp1^0-tmp1^post15 == 0), cost: 1
  15: l2 -> l12 : tmp1^0'=tmp1^post16, witemsnum^0'=witemsnum^post16, (witemsnum^0-witemsnum^post16 == 0 /\ 1-tmp1^0 <= 0 /\ tmp1^0-tmp1^post16 == 0), cost: 1
  16: l2 -> l12 : tmp1^0'=tmp1^post17, witemsnum^0'=witemsnum^post17, (1+tmp1^0 <= 0 /\ -witemsnum^post17+witemsnum^0 == 0 /\ -tmp1^post17+tmp1^0 == 0), cost: 1
   2: l3 -> l4 : tmp1^0'=tmp1^post3, witemsnum^0'=witemsnum^post3, (witemsnum^0-witemsnum^post3 == 0 /\ tmp1^0-tmp1^post3 == 0), cost: 1
   3: l4 -> l0 : tmp1^0'=tmp1^post4, witemsnum^0'=witemsnum^post4, (-witemsnum^post4+witemsnum^0 == 0 /\ -tmp1^post4+tmp1^0 == 0), cost: 1
   4: l5 -> l6 : tmp1^0'=tmp1^post5, witemsnum^0'=witemsnum^post5, (-witemsnum^post5+witemsnum^0 == 0 /\ tmp1^0-tmp1^post5 == 0), cost: 1
   7: l6 -> l3 : tmp1^0'=tmp1^post8, witemsnum^0'=witemsnum^post8, (tmp1^0-tmp1^post8 == 0 /\ witemsnum^0-witemsnum^post8 == 0 /\ -2+witemsnum^0 <= 0), cost: 1
   8: l6 -> l5 : tmp1^0'=tmp1^post9, witemsnum^0'=witemsnum^post9, (3-witemsnum^0 <= 0 /\ 1+witemsnum^post9-witemsnum^0 == 0 /\ -tmp1^post9+tmp1^0 == 0), cost: 1
   5: l7 -> l8 : tmp1^0'=tmp1^post6, witemsnum^0'=witemsnum^post6, (tmp1^0-tmp1^post6 == 0 /\ witemsnum^0-witemsnum^post6 == 0), cost: 1
   6: l9 -> l10 : tmp1^0'=tmp1^post7, witemsnum^0'=witemsnum^post7, (-witemsnum^post7+witemsnum^0 == 0 /\ -tmp1^post7+tmp1^0 == 0), cost: 1
   9: l10 -> l11 : tmp1^0'=tmp1^post10, witemsnum^0'=witemsnum^post10, (tmp1^0-tmp1^post10 == 0 /\ -witemsnum^post10+witemsnum^0 == 0), cost: 1
  10: l11 -> l10 : tmp1^0'=tmp1^post11, witemsnum^0'=witemsnum^post11, (tmp1^0-tmp1^post11 == 0 /\ witemsnum^0-witemsnum^post11 == 0), cost: 1
  12: l12 -> l4 : tmp1^0'=tmp1^post13, witemsnum^0'=witemsnum^post13, (tmp1^0-tmp1^post13 == 0 /\ -1-witemsnum^0+witemsnum^post13 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
  13: l12 -> l4 : tmp1^0'=tmp1^post14, witemsnum^0'=witemsnum^post14, (-tmp1^post14+tmp1^0 == 0 /\ -1+witemsnum^post14-witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
  19: l14 -> l3 : tmp1^0'=tmp1^post18, witemsnum^0'=witemsnum^post18, (0 == 0 /\ tmp1^0-tmp1^post19 == 0 /\ witemsnum^0-witemsnum^post19 == 0 /\ -tmp1^post18+tmp1^post19 == 0), cost: 1

	Eliminating location l13 by chaining:

	Applied chaining

	First rule:
	l14 -> l13 : tmp1^0'=tmp1^post19, witemsnum^0'=witemsnum^post19, (tmp1^0-tmp1^post19 == 0 /\ witemsnum^0-witemsnum^post19 == 0), cost: 1
	Second rule:
	l13 -> l3 : tmp1^0'=tmp1^post18, witemsnum^0'=witemsnum^post18, (0 == 0 /\ -tmp1^post18+tmp1^0 == 0), cost: 1
	New rule:
	l14 -> l3 : tmp1^0'=tmp1^post18, witemsnum^0'=witemsnum^post18, (0 == 0 /\ tmp1^0-tmp1^post19 == 0 /\ witemsnum^0-witemsnum^post19 == 0 /\ -tmp1^post18+tmp1^post19 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 17 18

Simplified Transitions

Start location: l14
Program variables: tmp1^0 witemsnum^0
  20: l0 -> l1 : 6-witemsnum^0 <= 0, cost: 1
  21: l0 -> l2 : tmp1^0'=tmp1^post2, -5+witemsnum^0 <= 0, cost: 1
  31: l1 -> l5 : T, cost: 1
  34: l2 -> l1 : (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
  35: l2 -> l12 : 1-tmp1^0 <= 0, cost: 1
  36: l2 -> l12 : 1+tmp1^0 <= 0, cost: 1
  22: l3 -> l4 : T, cost: 1
  23: l4 -> l0 : T, cost: 1
  24: l5 -> l6 : T, cost: 1
  27: l6 -> l3 : -2+witemsnum^0 <= 0, cost: 1
  28: l6 -> l5 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1
  25: l7 -> l8 : T, cost: 1
  26: l9 -> l10 : T, cost: 1
  29: l10 -> l11 : T, cost: 1
  30: l11 -> l10 : T, cost: 1
  32: l12 -> l4 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1
  33: l12 -> l4 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1
  37: l14 -> l3 : witemsnum^0'=witemsnum^post18, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : tmp1^0'=tmp1^post1, witemsnum^0'=witemsnum^post1, (-witemsnum^post1+witemsnum^0 == 0 /\ -tmp1^post1+tmp1^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
	
		propagated equality witemsnum^post1 = witemsnum^0
		
		propagated equality tmp1^post1 = tmp1^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 6-witemsnum^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 6-witemsnum^0 <= 0, cost: 1
	New rule:
	l0 -> l1 : 6-witemsnum^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l2 : tmp1^0'=tmp1^post2, witemsnum^0'=witemsnum^post2, (0 == 0 /\ -witemsnum^post2+witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
	New rule:
	l0 -> l2 : tmp1^0'=tmp1^post2, witemsnum^0'=witemsnum^0, (0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
	
		propagated equality witemsnum^post2 = witemsnum^0
		
	Simplified Guard

	Original rule:
	l0 -> l2 : tmp1^0'=tmp1^post2, witemsnum^0'=witemsnum^0, (0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
	New rule:
	l0 -> l2 : tmp1^0'=tmp1^post2, witemsnum^0'=witemsnum^0, -5+witemsnum^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l2 : tmp1^0'=tmp1^post2, witemsnum^0'=witemsnum^0, -5+witemsnum^0 <= 0, cost: 1
	New rule:
	l0 -> l2 : tmp1^0'=tmp1^post2, -5+witemsnum^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l4 : tmp1^0'=tmp1^post3, witemsnum^0'=witemsnum^post3, (witemsnum^0-witemsnum^post3 == 0 /\ tmp1^0-tmp1^post3 == 0), cost: 1
	New rule:
	l3 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	
		propagated equality witemsnum^post3 = witemsnum^0
		
		propagated equality tmp1^post3 = tmp1^0
		
	Simplified Guard

	Original rule:
	l3 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	New rule:
	l3 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	New rule:
	l3 -> l4 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l0 : tmp1^0'=tmp1^post4, witemsnum^0'=witemsnum^post4, (-witemsnum^post4+witemsnum^0 == 0 /\ -tmp1^post4+tmp1^0 == 0), cost: 1
	New rule:
	l4 -> l0 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	
		propagated equality witemsnum^post4 = witemsnum^0
		
		propagated equality tmp1^post4 = tmp1^0
		
	Simplified Guard

	Original rule:
	l4 -> l0 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	New rule:
	l4 -> l0 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l0 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	New rule:
	l4 -> l0 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l6 : tmp1^0'=tmp1^post5, witemsnum^0'=witemsnum^post5, (-witemsnum^post5+witemsnum^0 == 0 /\ tmp1^0-tmp1^post5 == 0), cost: 1
	New rule:
	l5 -> l6 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	
		propagated equality witemsnum^post5 = witemsnum^0
		
		propagated equality tmp1^post5 = tmp1^0
		
	Simplified Guard

	Original rule:
	l5 -> l6 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	New rule:
	l5 -> l6 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l6 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	New rule:
	l5 -> l6 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l8 : tmp1^0'=tmp1^post6, witemsnum^0'=witemsnum^post6, (tmp1^0-tmp1^post6 == 0 /\ witemsnum^0-witemsnum^post6 == 0), cost: 1
	New rule:
	l7 -> l8 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	
		propagated equality tmp1^post6 = tmp1^0
		
		propagated equality witemsnum^post6 = witemsnum^0
		
	Simplified Guard

	Original rule:
	l7 -> l8 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	New rule:
	l7 -> l8 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l8 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	New rule:
	l7 -> l8 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l10 : tmp1^0'=tmp1^post7, witemsnum^0'=witemsnum^post7, (-witemsnum^post7+witemsnum^0 == 0 /\ -tmp1^post7+tmp1^0 == 0), cost: 1
	New rule:
	l9 -> l10 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	
		propagated equality witemsnum^post7 = witemsnum^0
		
		propagated equality tmp1^post7 = tmp1^0
		
	Simplified Guard

	Original rule:
	l9 -> l10 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	New rule:
	l9 -> l10 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l9 -> l10 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	New rule:
	l9 -> l10 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l3 : tmp1^0'=tmp1^post8, witemsnum^0'=witemsnum^post8, (tmp1^0-tmp1^post8 == 0 /\ witemsnum^0-witemsnum^post8 == 0 /\ -2+witemsnum^0 <= 0), cost: 1
	New rule:
	l6 -> l3 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ -2+witemsnum^0 <= 0), cost: 1
	
		propagated equality tmp1^post8 = tmp1^0
		
		propagated equality witemsnum^post8 = witemsnum^0
		
	Simplified Guard

	Original rule:
	l6 -> l3 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ -2+witemsnum^0 <= 0), cost: 1
	New rule:
	l6 -> l3 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, -2+witemsnum^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l3 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, -2+witemsnum^0 <= 0, cost: 1
	New rule:
	l6 -> l3 : -2+witemsnum^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l5 : tmp1^0'=tmp1^post9, witemsnum^0'=witemsnum^post9, (3-witemsnum^0 <= 0 /\ 1+witemsnum^post9-witemsnum^0 == 0 /\ -tmp1^post9+tmp1^0 == 0), cost: 1
	New rule:
	l6 -> l5 : tmp1^0'=tmp1^0, witemsnum^0'=-1+witemsnum^0, (0 == 0 /\ 3-witemsnum^0 <= 0), cost: 1
	
		propagated equality witemsnum^post9 = -1+witemsnum^0
		
		propagated equality tmp1^post9 = tmp1^0
		
	Simplified Guard

	Original rule:
	l6 -> l5 : tmp1^0'=tmp1^0, witemsnum^0'=-1+witemsnum^0, (0 == 0 /\ 3-witemsnum^0 <= 0), cost: 1
	New rule:
	l6 -> l5 : tmp1^0'=tmp1^0, witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l5 : tmp1^0'=tmp1^0, witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1
	New rule:
	l6 -> l5 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l10 -> l11 : tmp1^0'=tmp1^post10, witemsnum^0'=witemsnum^post10, (tmp1^0-tmp1^post10 == 0 /\ -witemsnum^post10+witemsnum^0 == 0), cost: 1
	New rule:
	l10 -> l11 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	
		propagated equality tmp1^post10 = tmp1^0
		
		propagated equality witemsnum^post10 = witemsnum^0
		
	Simplified Guard

	Original rule:
	l10 -> l11 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	New rule:
	l10 -> l11 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l10 -> l11 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	New rule:
	l10 -> l11 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l11 -> l10 : tmp1^0'=tmp1^post11, witemsnum^0'=witemsnum^post11, (tmp1^0-tmp1^post11 == 0 /\ witemsnum^0-witemsnum^post11 == 0), cost: 1
	New rule:
	l11 -> l10 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	
		propagated equality tmp1^post11 = tmp1^0
		
		propagated equality witemsnum^post11 = witemsnum^0
		
	Simplified Guard

	Original rule:
	l11 -> l10 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	New rule:
	l11 -> l10 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l11 -> l10 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	New rule:
	l11 -> l10 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l5 : tmp1^0'=tmp1^post12, witemsnum^0'=witemsnum^post12, (-tmp1^post12+tmp1^0 == 0 /\ -witemsnum^post12+witemsnum^0 == 0), cost: 1
	New rule:
	l1 -> l5 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	
		propagated equality tmp1^post12 = tmp1^0
		
		propagated equality witemsnum^post12 = witemsnum^0
		
	Simplified Guard

	Original rule:
	l1 -> l5 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1
	New rule:
	l1 -> l5 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l5 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, T, cost: 1
	New rule:
	l1 -> l5 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l4 : tmp1^0'=tmp1^post13, witemsnum^0'=witemsnum^post13, (tmp1^0-tmp1^post13 == 0 /\ -1-witemsnum^0+witemsnum^post13 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
	New rule:
	l12 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=1+witemsnum^0, (0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
	
		propagated equality tmp1^post13 = tmp1^0
		
		propagated equality witemsnum^post13 = 1+witemsnum^0
		
	Simplified Guard

	Original rule:
	l12 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=1+witemsnum^0, (0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1
	New rule:
	l12 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1
	New rule:
	l12 -> l4 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l4 : tmp1^0'=tmp1^post14, witemsnum^0'=witemsnum^post14, (-tmp1^post14+tmp1^0 == 0 /\ -1+witemsnum^post14-witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
	New rule:
	l12 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=1+witemsnum^0, (0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
	
		propagated equality tmp1^post14 = tmp1^0
		
		propagated equality witemsnum^post14 = 1+witemsnum^0
		
	Simplified Guard

	Original rule:
	l12 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=1+witemsnum^0, (0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1
	New rule:
	l12 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l4 : tmp1^0'=tmp1^0, witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1
	New rule:
	l12 -> l4 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1
	
	made implied equalities explicit

	Original rule:
	l2 -> l1 : tmp1^0'=tmp1^post15, witemsnum^0'=witemsnum^post15, (tmp1^0 <= 0 /\ -tmp1^0 <= 0 /\ -witemsnum^post15+witemsnum^0 == 0 /\ tmp1^0-tmp1^post15 == 0), cost: 1
	New rule:
	l2 -> l1 : tmp1^0'=tmp1^post15, witemsnum^0'=witemsnum^post15, (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0 /\ -witemsnum^post15+witemsnum^0 == 0 /\ tmp1^0-tmp1^post15 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l1 : tmp1^0'=tmp1^post15, witemsnum^0'=witemsnum^post15, (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0 /\ -witemsnum^post15+witemsnum^0 == 0 /\ tmp1^0-tmp1^post15 == 0), cost: 1
	New rule:
	l2 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	
		propagated equality witemsnum^post15 = witemsnum^0
		
		propagated equality tmp1^post15 = tmp1^0
		
	Simplified Guard

	Original rule:
	l2 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	New rule:
	l2 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l2 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	New rule:
	l2 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l1 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	New rule:
	l2 -> l1 : (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l12 : tmp1^0'=tmp1^post16, witemsnum^0'=witemsnum^post16, (witemsnum^0-witemsnum^post16 == 0 /\ 1-tmp1^0 <= 0 /\ tmp1^0-tmp1^post16 == 0), cost: 1
	New rule:
	l2 -> l12 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1-tmp1^0 <= 0), cost: 1
	
		propagated equality witemsnum^post16 = witemsnum^0
		
		propagated equality tmp1^post16 = tmp1^0
		
	Simplified Guard

	Original rule:
	l2 -> l12 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1-tmp1^0 <= 0), cost: 1
	New rule:
	l2 -> l12 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 1-tmp1^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l12 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 1-tmp1^0 <= 0, cost: 1
	New rule:
	l2 -> l12 : 1-tmp1^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l12 : tmp1^0'=tmp1^post17, witemsnum^0'=witemsnum^post17, (1+tmp1^0 <= 0 /\ -witemsnum^post17+witemsnum^0 == 0 /\ -tmp1^post17+tmp1^0 == 0), cost: 1
	New rule:
	l2 -> l12 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1+tmp1^0 <= 0), cost: 1
	
		propagated equality witemsnum^post17 = witemsnum^0
		
		propagated equality tmp1^post17 = tmp1^0
		
	Simplified Guard

	Original rule:
	l2 -> l12 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1+tmp1^0 <= 0), cost: 1
	New rule:
	l2 -> l12 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 1+tmp1^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l12 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, 1+tmp1^0 <= 0, cost: 1
	New rule:
	l2 -> l12 : 1+tmp1^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l14 -> l3 : tmp1^0'=tmp1^post18, witemsnum^0'=witemsnum^post18, (0 == 0 /\ tmp1^0-tmp1^post19 == 0 /\ witemsnum^0-witemsnum^post19 == 0 /\ -tmp1^post18+tmp1^post19 == 0), cost: 1
	New rule:
	l14 -> l3 : tmp1^0'=tmp1^post19, witemsnum^0'=witemsnum^post18, (0 == 0 /\ tmp1^0-tmp1^post19 == 0 /\ witemsnum^0-witemsnum^post19 == 0), cost: 1
	
		propagated equality tmp1^post18 = tmp1^post19
		
	Propagated Equalities

	Original rule:
	l14 -> l3 : tmp1^0'=tmp1^post19, witemsnum^0'=witemsnum^post18, (0 == 0 /\ tmp1^0-tmp1^post19 == 0 /\ witemsnum^0-witemsnum^post19 == 0), cost: 1
	New rule:
	l14 -> l3 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^post18, 0 == 0, cost: 1
	
		propagated equality tmp1^post19 = tmp1^0
		
		propagated equality witemsnum^post19 = witemsnum^0
		
	Simplified Guard

	Original rule:
	l14 -> l3 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^post18, 0 == 0, cost: 1
	New rule:
	l14 -> l3 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^post18, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l14 -> l3 : tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^post18, T, cost: 1
	New rule:
	l14 -> l3 : witemsnum^0'=witemsnum^post18, T, cost: 1

Step with 37

	Trace

	37[T]
	
	Blocked

	[{}, {}]

Step with 22

	Trace

	37[T], 22[T]
	
	Blocked

	[{}, {}, {}]

Step with 23

	Trace

	37[T], 22[T], 23[T]
	
	Blocked

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

Step with 20

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)]
	
	Blocked

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

Step with 31

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T]
	
	Blocked

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

Step with 24

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 24[T]
	
	Blocked

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

Step with 28

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 24[T], 28[(3-witemsnum^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {27[T]}, {}]

Accelerate

Start location: l14
Program variables: tmp1^0 witemsnum^0
  20: l0 -> l1 : 6-witemsnum^0 <= 0, cost: 1
  21: l0 -> l2 : tmp1^0'=tmp1^post2, -5+witemsnum^0 <= 0, cost: 1
  31: l1 -> l5 : T, cost: 1
  34: l2 -> l1 : (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
  35: l2 -> l12 : 1-tmp1^0 <= 0, cost: 1
  36: l2 -> l12 : 1+tmp1^0 <= 0, cost: 1
  22: l3 -> l4 : T, cost: 1
  23: l4 -> l0 : T, cost: 1
  24: l5 -> l6 : T, cost: 1
  38: l5 -> l5 : witemsnum^0'=-n+witemsnum^0, (-2-n+witemsnum^0 >= 0 /\ -1+n >= 0), cost: 1
  27: l6 -> l3 : -2+witemsnum^0 <= 0, cost: 1
  28: l6 -> l5 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1
  25: l7 -> l8 : T, cost: 1
  26: l9 -> l10 : T, cost: 1
  29: l10 -> l11 : T, cost: 1
  30: l11 -> l10 : T, cost: 1
  32: l12 -> l4 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1
  33: l12 -> l4 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1
  37: l14 -> l3 : witemsnum^0'=witemsnum^post18, T, cost: 1

	Loop Acceleration

	Original rule:
	l5 -> l5 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1
	New rule:
	l5 -> l5 : witemsnum^0'=-n+witemsnum^0, (-2-n+witemsnum^0 >= 0 /\ -1+n >= 0), cost: 1

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

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}]

Step with 24

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {}]

Step with 28

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T], 28[(3-witemsnum^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {}, {}]

Covered

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {28[T]}]

Step with 27

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T], 27[(-2+witemsnum^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {28[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 22

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T], 27[(-2+witemsnum^0 <= 0)], 22[T]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {28[T]}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 23

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T], 27[(-2+witemsnum^0 <= 0)], 22[T], 23[T]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {28[T]}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 21

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T], 27[(-2+witemsnum^0 <= 0)], 22[T], 23[T], 21[(-5+witemsnum^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {28[T]}, {}, {}, {20[T]}, {}]

Step with 34

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T], 27[(-2+witemsnum^0 <= 0)], 22[T], 23[T], 21[(-5+witemsnum^0 <= 0)], 34[(tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {28[T]}, {}, {}, {20[T]}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 31

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 24[T], 27[(-2+witemsnum^0 <= 0)], 22[T], 23[T], 21[(-5+witemsnum^0 <= 0)], 34[(tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0)], 31[T]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {38[T]}, {28[T]}, {}, {}, {20[T]}, {}, {}, {}]

Nonterm

Start location: l14
Program variables: tmp1^0 witemsnum^0
  20: l0 -> l1 : 6-witemsnum^0 <= 0, cost: 1
  21: l0 -> l2 : tmp1^0'=tmp1^post2, -5+witemsnum^0 <= 0, cost: 1
  31: l1 -> l5 : T, cost: 1
  34: l2 -> l1 : (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
  35: l2 -> l12 : 1-tmp1^0 <= 0, cost: 1
  36: l2 -> l12 : 1+tmp1^0 <= 0, cost: 1
  22: l3 -> l4 : T, cost: 1
  23: l4 -> l0 : T, cost: 1
  24: l5 -> l6 : T, cost: 1
  38: l5 -> l5 : witemsnum^0'=-n+witemsnum^0, (-2-n+witemsnum^0 >= 0 /\ -1+n >= 0), cost: 1
  39: l5 -> LoAT_sink : (2-witemsnum^0 >= 0 /\ -1+n2 >= 0 /\ 5-witemsnum^0 >= 0), cost: NONTERM
  27: l6 -> l3 : -2+witemsnum^0 <= 0, cost: 1
  28: l6 -> l5 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1
  25: l7 -> l8 : T, cost: 1
  26: l9 -> l10 : T, cost: 1
  29: l10 -> l11 : T, cost: 1
  30: l11 -> l10 : T, cost: 1
  32: l12 -> l4 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1
  33: l12 -> l4 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1
  37: l14 -> l3 : witemsnum^0'=witemsnum^post18, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l5 -> l5 : tmp1^0'=0, (-2+witemsnum^0 <= 0 /\ -5+witemsnum^0 <= 0), cost: 1
	New rule:
	l5 -> LoAT_sink : (2-witemsnum^0 >= 0 /\ -1+n2 >= 0 /\ 5-witemsnum^0 >= 0), cost: NONTERM

		2-witemsnum^0 >= 0 [0]: monotonic increase yields 2-witemsnum^0 >= 0
		
		5-witemsnum^0 >= 0 [0]: monotonic increase yields 5-witemsnum^0 >= 0, dependencies: 2-witemsnum^0 >= 0
		
		Replacement map: {2-witemsnum^0 >= 0 -> 2-witemsnum^0 >= 0, 5-witemsnum^0 >= 0 -> 5-witemsnum^0 >= 0}

Step with 39

	Trace

	37[T], 22[T], 23[T], 20[(6-witemsnum^0 <= 0)], 31[T], 38[(-2-n+witemsnum^0 >= 0 /\ -1+n >= 0)], 39[(2-witemsnum^0 >= 0 /\ -1+n2 >= 0 /\ 5-witemsnum^0 >= 0)]
	
	Blocked

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

Refute

	Counterexample

	[ tmp1^0=0 witemsnum^0=6 ] 37 [ tmp1^0=0 witemsnum^0=6 ] 22 [ tmp1^0=0 witemsnum^0=6 ] 23 [ tmp1^0=0 witemsnum^0=6 ] 20 [ tmp1^0=0 witemsnum^0=6 ] 31 [ tmp1^0=0 witemsnum^0=2 ] 38 [ tmp1^0=0 witemsnum^0=witemsnum^0 ] 39
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b