NO

Initial ITS

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

Chained Linear Paths

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

	Eliminating location l13 by chaining:

	Applied chaining

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

	Removed the following rules: 17 18

Simplified Transitions

Start location: l14
Program variables: __const_5^0 tmp1^0 witemsnum^0
  20: l0 -> l1 : 1+__const_5^0-witemsnum^0 <= 0, cost: 1
  21: l0 -> l2 : tmp1^0'=tmp1^post2, -__const_5^0+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, 1+__const_5^0-witemsnum^0 <= 0, cost: 1
  33: l12 -> l4 : witemsnum^0'=1+witemsnum^0, -__const_5^0+witemsnum^0 <= 0, cost: 1
  37: l14 -> l3 : witemsnum^0'=witemsnum^post18, T, cost: 1

	Propagated Equalities

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

	Original rule:
	l0 -> l1 : __const_5^0'=__const_5^0, tmp1^0'=tmp1^0, 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^0, 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^0, witemsnum^0'=witemsnum^0, 1+__const_5^0-witemsnum^0 <= 0, cost: 1
	New rule:
	l0 -> l1 : 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, (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^post2, witemsnum^0'=witemsnum^0, (0 == 0 /\ -__const_5^0+witemsnum^0 <= 0), cost: 1
	
		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^post2, 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^post2, 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^post2, witemsnum^0'=witemsnum^0, -__const_5^0+witemsnum^0 <= 0, cost: 1
	New rule:
	l0 -> l2 : tmp1^0'=tmp1^post2, -__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, (__const_5^0-__const_5^post3 == 0 /\ -witemsnum^post3+witemsnum^0 == 0 /\ -tmp1^post3+tmp1^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 __const_5^post3 = __const_5^0
		
		propagated equality witemsnum^post3 = witemsnum^0
		
		propagated equality tmp1^post3 = tmp1^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, (-witemsnum^post4+witemsnum^0 == 0 /\ __const_5^0-__const_5^post4 == 0 /\ -tmp1^post4+tmp1^0 == 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 witemsnum^post4 = witemsnum^0
		
		propagated equality __const_5^post4 = __const_5^0
		
		propagated equality tmp1^post4 = tmp1^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^post6+tmp1^0 == 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, (-witemsnum^post7+witemsnum^0 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ -tmp1^post7+tmp1^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 witemsnum^post7 = witemsnum^0
		
		propagated equality __const_5^post7 = __const_5^0
		
		propagated equality tmp1^post7 = tmp1^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:
	l6 -> l3 : __const_5^0'=__const_5^post8, tmp1^0'=tmp1^post8, witemsnum^0'=witemsnum^post8, (-2+witemsnum^0 <= 0 /\ -witemsnum^post8+witemsnum^0 == 0 /\ -tmp1^post8+tmp1^0 == 0 /\ -__const_5^post8+__const_5^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 witemsnum^post8 = witemsnum^0
		
		propagated equality tmp1^post8 = tmp1^0
		
		propagated equality __const_5^post8 = __const_5^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^post9, tmp1^0'=tmp1^post9, witemsnum^0'=witemsnum^post9, (-__const_5^post9+__const_5^0 == 0 /\ 3-witemsnum^0 <= 0 /\ -tmp1^post9+tmp1^0 == 0 /\ 1+witemsnum^post9-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^post9 = __const_5^0
		
		propagated equality tmp1^post9 = tmp1^0
		
		propagated equality witemsnum^post9 = -1+witemsnum^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
	
	Propagated Equalities

	Original rule:
	l10 -> l11 : __const_5^0'=__const_5^post10, tmp1^0'=tmp1^post10, witemsnum^0'=witemsnum^post10, (-tmp1^post10+tmp1^0 == 0 /\ -__const_5^post10+__const_5^0 == 0 /\ -witemsnum^post10+witemsnum^0 == 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 tmp1^post10 = tmp1^0
		
		propagated equality __const_5^post10 = __const_5^0
		
		propagated equality witemsnum^post10 = witemsnum^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^post11, tmp1^0'=tmp1^post11, witemsnum^0'=witemsnum^post11, (-__const_5^post11+__const_5^0 == 0 /\ -witemsnum^post11+witemsnum^0 == 0 /\ -tmp1^post11+tmp1^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^post11 = __const_5^0
		
		propagated equality witemsnum^post11 = witemsnum^0
		
		propagated equality tmp1^post11 = tmp1^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:
	l1 -> l5 : __const_5^0'=__const_5^post12, tmp1^0'=tmp1^post12, witemsnum^0'=witemsnum^post12, (-witemsnum^post12+witemsnum^0 == 0 /\ -__const_5^post12+__const_5^0 == 0 /\ -tmp1^post12+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, cost: 1
	
		propagated equality witemsnum^post12 = witemsnum^0
		
		propagated equality __const_5^post12 = __const_5^0
		
		propagated equality tmp1^post12 = tmp1^0
		
	Simplified Guard

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

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

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

	Original rule:
	l12 -> 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:
	l12 -> 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:
	l12 -> 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:
	l12 -> l4 : witemsnum^0'=1+witemsnum^0, 1+__const_5^0-witemsnum^0 <= 0, cost: 1
	
	Propagated Equalities

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

	Original rule:
	l12 -> 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:
	l12 -> 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:
	l12 -> 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:
	l12 -> l4 : witemsnum^0'=1+witemsnum^0, -__const_5^0+witemsnum^0 <= 0, cost: 1
	
	made implied equalities explicit

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

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

	Original rule:
	l2 -> l1 : __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:
	l2 -> l1 : __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:
	l2 -> l1 : __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:
	l2 -> l1 : __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:
	l2 -> l1 : __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:
	l2 -> l1 : (-tmp1^0 <= 0 /\ -tmp1^0 == 0 /\ tmp1^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l12 : __const_5^0'=__const_5^post16, tmp1^0'=tmp1^post16, witemsnum^0'=witemsnum^post16, (-witemsnum^post16+witemsnum^0 == 0 /\ -tmp1^post16+tmp1^0 == 0 /\ __const_5^0-__const_5^post16 == 0 /\ 1-tmp1^0 <= 0), cost: 1
	New rule:
	l2 -> l12 : __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^post16 = witemsnum^0
		
		propagated equality tmp1^post16 = tmp1^0
		
		propagated equality __const_5^post16 = __const_5^0
		
	Simplified Guard

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

	Original rule:
	l2 -> l12 : __const_5^0'=__const_5^0, tmp1^0'=tmp1^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1+tmp1^0 <= 0), cost: 1
	New rule:
	l2 -> l12 : __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:
	l2 -> l12 : __const_5^0'=__const_5^0, 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 : __const_5^0'=__const_5^post18, tmp1^0'=tmp1^post18, witemsnum^0'=witemsnum^post18, (0 == 0 /\ -witemsnum^post19+witemsnum^0 == 0 /\ -tmp1^post18+tmp1^post19 == 0 /\ -__const_5^post19+__const_5^0 == 0 /\ -tmp1^post19+tmp1^0 == 0 /\ -__const_5^post18+__const_5^post19 == 0), cost: 1
	New rule:
	l14 -> l3 : __const_5^0'=__const_5^post19, tmp1^0'=tmp1^post19, witemsnum^0'=witemsnum^post18, (0 == 0 /\ -witemsnum^post19+witemsnum^0 == 0 /\ -__const_5^post19+__const_5^0 == 0 /\ -tmp1^post19+tmp1^0 == 0), cost: 1
	
		propagated equality tmp1^post18 = tmp1^post19
		
		propagated equality __const_5^post18 = __const_5^post19
		
	Propagated Equalities

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

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

	Original rule:
	l14 -> l3 : __const_5^0'=__const_5^0, 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[(1+__const_5^0-witemsnum^0 <= 0)]
	
	Blocked

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

Step with 31

	Trace

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

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

Step with 24

	Trace

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

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

Step with 27

	Trace

	37[T], 22[T], 23[T], 20[(1+__const_5^0-witemsnum^0 <= 0)], 31[T], 24[T], 27[(-2+witemsnum^0 <= 0)]
	
	Blocked

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

Nonterm

Start location: l14
Program variables: __const_5^0 tmp1^0 witemsnum^0
  20: l0 -> l1 : 1+__const_5^0-witemsnum^0 <= 0, cost: 1
  21: l0 -> l2 : tmp1^0'=tmp1^post2, -__const_5^0+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
  38: l3 -> LoAT_sink : (-1+n >= 0 /\ 2-witemsnum^0 >= 0 /\ -1-__const_5^0+witemsnum^0 >= 0), cost: NONTERM
  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, 1+__const_5^0-witemsnum^0 <= 0, cost: 1
  33: l12 -> l4 : witemsnum^0'=1+witemsnum^0, -__const_5^0+witemsnum^0 <= 0, cost: 1
  37: l14 -> l3 : witemsnum^0'=witemsnum^post18, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l3 -> l3 : (-2+witemsnum^0 <= 0 /\ 1+__const_5^0-witemsnum^0 <= 0), cost: 1
	New rule:
	l3 -> LoAT_sink : (-1+n >= 0 /\ 2-witemsnum^0 >= 0 /\ -1-__const_5^0+witemsnum^0 >= 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 38

	Trace

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

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

Refute

	Counterexample

	[ __const_5^0=0 tmp1^0=0 witemsnum^0=1 ] 37 [ __const_5^0=0 tmp1^0=0 witemsnum^0=witemsnum^0 ] 38
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b