NO

Initial ITS

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

Chained Linear Paths

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

	Eliminating location l12 by chaining:

	Applied chaining

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

	Removed the following rules: 16 17

Simplified Transitions

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

	Propagated Equalities

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

	Original rule:
	l6 -> l3 : __const_5^0'=__const_5^0, 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 : __const_5^0'=__const_5^post11, tmp1^0'=tmp1^post11, witemsnum^0'=witemsnum^post11, (-__const_5^post11+__const_5^0 == 0 /\ 1+witemsnum^post11-witemsnum^0 == 0 /\ tmp1^0-tmp1^post11 == 0 /\ 3-witemsnum^0 <= 0), cost: 1
	New rule:
	l6 -> l5 : __const_5^0'=__const_5^0, tmp1^0'=tmp1^0, witemsnum^0'=-1+witemsnum^0, (0 == 0 /\ 3-witemsnum^0 <= 0), cost: 1
	
		propagated equality __const_5^post11 = __const_5^0
		
		propagated equality witemsnum^post11 = -1+witemsnum^0
		
		propagated equality tmp1^post11 = tmp1^0
		
	Simplified Guard

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

	Original rule:
	l6 -> l5 : __const_5^0'=__const_5^0, 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
	
	made implied equalities explicit

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

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

	Original rule:
	l1 -> l5 : __const_5^0'=__const_5^0, tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	New rule:
	l1 -> l5 : __const_5^0'=__const_5^0, 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:
	l1 -> l5 : __const_5^0'=__const_5^0, tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	New rule:
	l1 -> l5 : __const_5^0'=__const_5^0, tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
	
	Removed Trivial Updates

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

	Original rule:
	l13 -> l3 : __const_5^0'=__const_5^0, tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^post17, T, cost: 1
	New rule:
	l13 -> l3 : witemsnum^0'=witemsnum^post17, T, cost: 1

Step with 35

	Trace

	35[T]
	
	Blocked

	[{}, {}]

Step with 21

	Trace

	35[T], 21[T]
	
	Blocked

	[{}, {}, {}]

Step with 22

	Trace

	35[T], 21[T], 22[T]
	
	Blocked

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

Step with 19

	Trace

	35[T], 21[T], 22[T], 19[(1+__const_5^0-witemsnum^0 <= 0)]
	
	Blocked

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

Step with 30

	Trace

	35[T], 21[T], 22[T], 19[(1+__const_5^0-witemsnum^0 <= 0)], 30[(tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0)]
	
	Blocked

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

Step with 23

	Trace

	35[T], 21[T], 22[T], 19[(1+__const_5^0-witemsnum^0 <= 0)], 30[(tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0)], 23[T]
	
	Blocked

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

Step with 28

	Trace

	35[T], 21[T], 22[T], 19[(1+__const_5^0-witemsnum^0 <= 0)], 30[(tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0)], 23[T], 28[(-2+witemsnum^0 <= 0)]
	
	Blocked

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

Nonterm

Start location: l13
Program variables: __const_5^0 tmp1^0 witemsnum^0
  19: l0 -> l1 : tmp1^0'=tmp1^post1, 1+__const_5^0-witemsnum^0 <= 0, cost: 1
  20: l0 -> l2 : -__const_5^0+witemsnum^0 <= 0, cost: 1
  30: l1 -> l5 : (tmp1^0 <= 0 /\ tmp1^0 == 0 /\ -tmp1^0 <= 0), cost: 1
  31: l1 -> l2 : 1-tmp1^0 <= 0, cost: 1
  32: l1 -> l2 : 1+tmp1^0 <= 0, cost: 1
  33: l2 -> l4 : witemsnum^0'=1+witemsnum^0, 1+__const_5^0-witemsnum^0 <= 0, cost: 1
  34: l2 -> l4 : witemsnum^0'=1+witemsnum^0, -__const_5^0+witemsnum^0 <= 0, cost: 1
  21: l3 -> l4 : T, cost: 1
  36: l3 -> LoAT_sink : (2-witemsnum^0 >= 0 /\ -1-__const_5^0+witemsnum^0 >= 0 /\ -1+n >= 0), cost: NONTERM
  22: l4 -> l0 : T, cost: 1
  23: l5 -> l6 : T, cost: 1
  28: l6 -> l3 : -2+witemsnum^0 <= 0, cost: 1
  29: l6 -> l5 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1
  24: l7 -> l8 : T, cost: 1
  25: l9 -> l10 : T, cost: 1
  26: l10 -> l11 : T, cost: 1
  27: l11 -> l10 : T, cost: 1
  35: l13 -> l3 : witemsnum^0'=witemsnum^post17, T, cost: 1

	Certificate of Non-Termination

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

		2-witemsnum^0 >= 0 [0]: monotonic increase yields 2-witemsnum^0 >= 0
		
		-1-__const_5^0+witemsnum^0 >= 0 [0]: monotonic increase yields -1-__const_5^0+witemsnum^0 >= 0
		
		Replacement map: {2-witemsnum^0 >= 0 -> 2-witemsnum^0 >= 0, -1-__const_5^0+witemsnum^0 >= 0 -> -1-__const_5^0+witemsnum^0 >= 0}

Step with 36

	Trace

	35[T], 36[(2-witemsnum^0 >= 0 /\ -1-__const_5^0+witemsnum^0 >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {36[T]}]

Refute

	Counterexample

	[ __const_5^0=0 tmp1^0=0 witemsnum^0=1 ] 35 [ __const_5^0=0 tmp1^0=0 witemsnum^0=witemsnum^0 ] 36
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b