NO

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


Removed unreachable rules and leafs
Start location: l13
   0: l0 -> l1 : tmp1^0'=tmp1^post0, WItemsNum^0'=WItemsNum^post0, (0 == 0 /\ 6-WItemsNum^0 <= 0 /\ -WItemsNum^post0+WItemsNum^0 == 0), cost: 1
   1: l0 -> l2 : tmp1^0'=tmp1^post1, WItemsNum^0'=WItemsNum^post1, (WItemsNum^0-WItemsNum^post1 == 0 /\ -5+WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post1 == 0), cost: 1
  11: l1 -> l5 : tmp1^0'=tmp1^post11, WItemsNum^0'=WItemsNum^post11, (tmp1^0 <= 0 /\ -WItemsNum^post11+WItemsNum^0 == 0 /\ -tmp1^0 <= 0 /\ tmp1^0-tmp1^post11 == 0), cost: 1
  12: l1 -> l2 : tmp1^0'=tmp1^post12, WItemsNum^0'=WItemsNum^post12, (WItemsNum^0-WItemsNum^post12 == 0 /\ 1-tmp1^0 <= 0 /\ tmp1^0-tmp1^post12 == 0), cost: 1
  13: l1 -> l2 : tmp1^0'=tmp1^post13, WItemsNum^0'=WItemsNum^post13, (1+tmp1^0 <= 0 /\ -WItemsNum^post13+WItemsNum^0 == 0 /\ -tmp1^post13+tmp1^0 == 0), cost: 1
  14: l2 -> l4 : tmp1^0'=tmp1^post14, WItemsNum^0'=WItemsNum^post14, (6-WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post14 == 0 /\ -1-WItemsNum^0+WItemsNum^post14 == 0), cost: 1
  15: l2 -> l4 : tmp1^0'=tmp1^post15, WItemsNum^0'=WItemsNum^post15, (-1-WItemsNum^0+WItemsNum^post15 == 0 /\ -5+WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post15 == 0), cost: 1
   2: l3 -> l4 : tmp1^0'=tmp1^post2, WItemsNum^0'=WItemsNum^post2, (WItemsNum^0-WItemsNum^post2 == 0 /\ tmp1^0-tmp1^post2 == 0), cost: 1
   3: l4 -> l0 : tmp1^0'=tmp1^post3, WItemsNum^0'=WItemsNum^post3, (tmp1^0-tmp1^post3 == 0 /\ -WItemsNum^post3+WItemsNum^0 == 0), cost: 1
   4: l5 -> l6 : tmp1^0'=tmp1^post4, WItemsNum^0'=WItemsNum^post4, (tmp1^0-tmp1^post4 == 0 /\ WItemsNum^0-WItemsNum^post4 == 0), cost: 1
   9: l6 -> l3 : tmp1^0'=tmp1^post9, WItemsNum^0'=WItemsNum^post9, (-2+WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post9 == 0 /\ -WItemsNum^post9+WItemsNum^0 == 0), cost: 1
  10: l6 -> l5 : tmp1^0'=tmp1^post10, WItemsNum^0'=WItemsNum^post10, (tmp1^0-tmp1^post10 == 0 /\ 1+WItemsNum^post10-WItemsNum^0 == 0 /\ 3-WItemsNum^0 <= 0), cost: 1
  16: l12 -> l3 : tmp1^0'=tmp1^post16, WItemsNum^0'=WItemsNum^post16, (0 == 0 /\ tmp1^0-tmp1^post16 == 0), cost: 1
  17: l13 -> l12 : tmp1^0'=tmp1^post17, WItemsNum^0'=WItemsNum^post17, (tmp1^0-tmp1^post17 == 0 /\ WItemsNum^0-WItemsNum^post17 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : tmp1^0'=tmp1^post0, WItemsNum^0'=WItemsNum^post0, (0 == 0 /\ 6-WItemsNum^0 <= 0 /\ -WItemsNum^post0+WItemsNum^0 == 0), cost: 1
New rule:
l0 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : tmp1^0'=tmp1^post1, WItemsNum^0'=WItemsNum^post1, (WItemsNum^0-WItemsNum^post1 == 0 /\ -5+WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post1 == 0), cost: 1
New rule:
l0 -> l2 : -5+WItemsNum^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l4 : tmp1^0'=tmp1^post2, WItemsNum^0'=WItemsNum^post2, (WItemsNum^0-WItemsNum^post2 == 0 /\ tmp1^0-tmp1^post2 == 0), cost: 1
New rule:
l3 -> l4 : TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l0 : tmp1^0'=tmp1^post3, WItemsNum^0'=WItemsNum^post3, (tmp1^0-tmp1^post3 == 0 /\ -WItemsNum^post3+WItemsNum^0 == 0), cost: 1
New rule:
l4 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l6 : tmp1^0'=tmp1^post4, WItemsNum^0'=WItemsNum^post4, (tmp1^0-tmp1^post4 == 0 /\ WItemsNum^0-WItemsNum^post4 == 0), cost: 1
New rule:
l5 -> l6 : TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l3 : tmp1^0'=tmp1^post9, WItemsNum^0'=WItemsNum^post9, (-2+WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post9 == 0 /\ -WItemsNum^post9+WItemsNum^0 == 0), cost: 1
New rule:
l6 -> l3 : -2+WItemsNum^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : tmp1^0'=tmp1^post10, WItemsNum^0'=WItemsNum^post10, (tmp1^0-tmp1^post10 == 0 /\ 1+WItemsNum^post10-WItemsNum^0 == 0 /\ 3-WItemsNum^0 <= 0), cost: 1
New rule:
l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l5 : tmp1^0'=tmp1^post11, WItemsNum^0'=WItemsNum^post11, (tmp1^0 <= 0 /\ -WItemsNum^post11+WItemsNum^0 == 0 /\ -tmp1^0 <= 0 /\ tmp1^0-tmp1^post11 == 0), cost: 1
New rule:
l1 -> l5 : tmp1^0 == 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l2 : tmp1^0'=tmp1^post12, WItemsNum^0'=WItemsNum^post12, (WItemsNum^0-WItemsNum^post12 == 0 /\ 1-tmp1^0 <= 0 /\ tmp1^0-tmp1^post12 == 0), cost: 1
New rule:
l1 -> l2 : -1+tmp1^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l2 : tmp1^0'=tmp1^post13, WItemsNum^0'=WItemsNum^post13, (1+tmp1^0 <= 0 /\ -WItemsNum^post13+WItemsNum^0 == 0 /\ -tmp1^post13+tmp1^0 == 0), cost: 1
New rule:
l1 -> l2 : 1+tmp1^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l4 : tmp1^0'=tmp1^post14, WItemsNum^0'=WItemsNum^post14, (6-WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post14 == 0 /\ -1-WItemsNum^0+WItemsNum^post14 == 0), cost: 1
New rule:
l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -6+WItemsNum^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l4 : tmp1^0'=tmp1^post15, WItemsNum^0'=WItemsNum^post15, (-1-WItemsNum^0+WItemsNum^post15 == 0 /\ -5+WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post15 == 0), cost: 1
New rule:
l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l3 : tmp1^0'=tmp1^post16, WItemsNum^0'=WItemsNum^post16, (0 == 0 /\ tmp1^0-tmp1^post16 == 0), cost: 1
New rule:
l12 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l12 : tmp1^0'=tmp1^post17, WItemsNum^0'=WItemsNum^post17, (tmp1^0-tmp1^post17 == 0 /\ WItemsNum^0-WItemsNum^post17 == 0), cost: 1
New rule:
l13 -> l12 : TRUE, cost: 1

Simplified rules
Start location: l13
  18: l0 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 1
  19: l0 -> l2 : -5+WItemsNum^0 <= 0, cost: 1
  25: l1 -> l5 : tmp1^0 == 0, cost: 1
  26: l1 -> l2 : -1+tmp1^0 >= 0, cost: 1
  27: l1 -> l2 : 1+tmp1^0 <= 0, cost: 1
  28: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -6+WItemsNum^0 >= 0, cost: 1
  29: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 1
  20: l3 -> l4 : TRUE, cost: 1
  21: l4 -> l0 : TRUE, cost: 1
  22: l5 -> l6 : TRUE, cost: 1
  23: l6 -> l3 : -2+WItemsNum^0 <= 0, cost: 1
  24: l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1
  30: l12 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 1
  31: l13 -> l12 : TRUE, cost: 1


Eliminating location l12 by chaining:

Applied chaining
First rule:
l13 -> l12 : TRUE, cost: 1
Second rule:
l12 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 1
New rule:
l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2

Applied deletion
Removed the following rules: 30 31

Eliminated locations on linear paths
Start location: l13
  18: l0 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 1
  19: l0 -> l2 : -5+WItemsNum^0 <= 0, cost: 1
  25: l1 -> l5 : tmp1^0 == 0, cost: 1
  26: l1 -> l2 : -1+tmp1^0 >= 0, cost: 1
  27: l1 -> l2 : 1+tmp1^0 <= 0, cost: 1
  28: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -6+WItemsNum^0 >= 0, cost: 1
  29: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 1
  20: l3 -> l4 : TRUE, cost: 1
  21: l4 -> l0 : TRUE, cost: 1
  22: l5 -> l6 : TRUE, cost: 1
  23: l6 -> l3 : -2+WItemsNum^0 <= 0, cost: 1
  24: l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Eliminating location l0 by chaining:

Applied chaining
First rule:
l4 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 1
New rule:
l4 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 2

Applied chaining
First rule:
l4 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l2 : -5+WItemsNum^0 <= 0, cost: 1
New rule:
l4 -> l2 : -5+WItemsNum^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 18 19 21

Eliminating location l6 by chaining:

Applied chaining
First rule:
l5 -> l6 : TRUE, cost: 1
Second rule:
l6 -> l3 : -2+WItemsNum^0 <= 0, cost: 1
New rule:
l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2

Applied chaining
First rule:
l5 -> l6 : TRUE, cost: 1
Second rule:
l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1
New rule:
l5 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 22 23 24

Eliminated locations on tree-shaped paths
Start location: l13
  25: l1 -> l5 : tmp1^0 == 0, cost: 1
  26: l1 -> l2 : -1+tmp1^0 >= 0, cost: 1
  27: l1 -> l2 : 1+tmp1^0 <= 0, cost: 1
  28: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -6+WItemsNum^0 >= 0, cost: 1
  29: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 1
  20: l3 -> l4 : TRUE, cost: 1
  33: l4 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 2
  34: l4 -> l2 : -5+WItemsNum^0 <= 0, cost: 2
  35: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
  36: l5 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 2
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Applied acceleration
Original rule:
l5 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 2
New rule:
l5 -> l5 : WItemsNum^0'=-n+WItemsNum^0, (n >= 0 /\ -2-n+WItemsNum^0 >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PnLiHo.txt

Applied instantiation
Original rule:
l5 -> l5 : WItemsNum^0'=-n+WItemsNum^0, (n >= 0 /\ -2-n+WItemsNum^0 >= 0), cost: 2*n
New rule:
l5 -> l5 : WItemsNum^0'=2, (0 >= 0 /\ -2+WItemsNum^0 >= 0), cost: -4+2*WItemsNum^0

Applied simplification
Original rule:
l5 -> l5 : WItemsNum^0'=2, (0 >= 0 /\ -2+WItemsNum^0 >= 0), cost: -4+2*WItemsNum^0
New rule:
l5 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -4+2*WItemsNum^0

Applied deletion
Removed the following rules: 36

Accelerated simple loops
Start location: l13
  25: l1 -> l5 : tmp1^0 == 0, cost: 1
  26: l1 -> l2 : -1+tmp1^0 >= 0, cost: 1
  27: l1 -> l2 : 1+tmp1^0 <= 0, cost: 1
  28: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -6+WItemsNum^0 >= 0, cost: 1
  29: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 1
  20: l3 -> l4 : TRUE, cost: 1
  33: l4 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 2
  34: l4 -> l2 : -5+WItemsNum^0 <= 0, cost: 2
  35: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
  38: l5 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -4+2*WItemsNum^0
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Applied chaining
First rule:
l1 -> l5 : tmp1^0 == 0, cost: 1
Second rule:
l5 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -4+2*WItemsNum^0
New rule:
l1 -> l5 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ tmp1^0 == 0), cost: -3+2*WItemsNum^0

Applied deletion
Removed the following rules: 38

Chained accelerated rules with incoming rules
Start location: l13
  25: l1 -> l5 : tmp1^0 == 0, cost: 1
  26: l1 -> l2 : -1+tmp1^0 >= 0, cost: 1
  27: l1 -> l2 : 1+tmp1^0 <= 0, cost: 1
  39: l1 -> l5 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ tmp1^0 == 0), cost: -3+2*WItemsNum^0
  28: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -6+WItemsNum^0 >= 0, cost: 1
  29: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 1
  20: l3 -> l4 : TRUE, cost: 1
  33: l4 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 2
  34: l4 -> l2 : -5+WItemsNum^0 <= 0, cost: 2
  35: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Eliminating location l1 by chaining:

Applied chaining
First rule:
l4 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 2
Second rule:
l1 -> l5 : tmp1^0 == 0, cost: 1
New rule:
l4 -> l5 : tmp1^0'=tmp1^post0, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 3

Applied chaining
First rule:
l4 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 2
Second rule:
l1 -> l2 : -1+tmp1^0 >= 0, cost: 1
New rule:
l4 -> l2 : tmp1^0'=tmp1^post0, (-6+WItemsNum^0 >= 0 /\ -1+tmp1^post0 >= 0), cost: 3

Applied chaining
First rule:
l4 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 2
Second rule:
l1 -> l2 : 1+tmp1^0 <= 0, cost: 1
New rule:
l4 -> l2 : tmp1^0'=tmp1^post0, (1+tmp1^post0 <= 0 /\ -6+WItemsNum^0 >= 0), cost: 3

Applied chaining
First rule:
l4 -> l1 : tmp1^0'=tmp1^post0, -6+WItemsNum^0 >= 0, cost: 2
Second rule:
l1 -> l5 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ tmp1^0 == 0), cost: -3+2*WItemsNum^0
New rule:
l4 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -2+WItemsNum^0 >= 0 /\ -6+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0

Applied simplification
Original rule:
l4 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -2+WItemsNum^0 >= 0 /\ -6+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0
New rule:
l4 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0

Applied deletion
Removed the following rules: 25 26 27 33 39

Eliminating location l2 by chaining:

Applied chaining
First rule:
l4 -> l2 : -5+WItemsNum^0 <= 0, cost: 2
Second rule:
l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 1
New rule:
l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 3

Applied chaining
First rule:
l4 -> l2 : tmp1^0'=tmp1^post0, (-6+WItemsNum^0 >= 0 /\ -1+tmp1^post0 >= 0), cost: 3
Second rule:
l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -6+WItemsNum^0 >= 0, cost: 1
New rule:
l4 -> l4 : tmp1^0'=tmp1^post0, WItemsNum^0'=1+WItemsNum^0, (-6+WItemsNum^0 >= 0 /\ -1+tmp1^post0 >= 0), cost: 4

Applied chaining
First rule:
l4 -> l2 : tmp1^0'=tmp1^post0, (1+tmp1^post0 <= 0 /\ -6+WItemsNum^0 >= 0), cost: 3
Second rule:
l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, -6+WItemsNum^0 >= 0, cost: 1
New rule:
l4 -> l4 : tmp1^0'=tmp1^post0, WItemsNum^0'=1+WItemsNum^0, (1+tmp1^post0 <= 0 /\ -6+WItemsNum^0 >= 0), cost: 4

Applied deletion
Removed the following rules: 28 29 34 41 42

Eliminated locations on tree-shaped paths
Start location: l13
  20: l3 -> l4 : TRUE, cost: 1
  40: l4 -> l5 : tmp1^0'=tmp1^post0, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 3
  43: l4 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0
  44: l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 3
  45: l4 -> l4 : tmp1^0'=tmp1^post0, WItemsNum^0'=1+WItemsNum^0, (-6+WItemsNum^0 >= 0 /\ -1+tmp1^post0 >= 0), cost: 4
  46: l4 -> l4 : tmp1^0'=tmp1^post0, WItemsNum^0'=1+WItemsNum^0, (1+tmp1^post0 <= 0 /\ -6+WItemsNum^0 >= 0), cost: 4
  35: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Applied acceleration
Original rule:
l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, -5+WItemsNum^0 <= 0, cost: 3
New rule:
l4 -> l4 : WItemsNum^0'=n0+WItemsNum^0, (n0 >= 0 /\ 6-n0-WItemsNum^0 >= 0), cost: 3*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_eLldlB.txt

Applied instantiation
Original rule:
l4 -> l4 : WItemsNum^0'=n0+WItemsNum^0, (n0 >= 0 /\ 6-n0-WItemsNum^0 >= 0), cost: 3*n0
New rule:
l4 -> l4 : WItemsNum^0'=6, (0 >= 0 /\ 6-WItemsNum^0 >= 0), cost: 18-3*WItemsNum^0

Applied nonterm
Original rule:
l4 -> l4 : tmp1^0'=tmp1^post0, WItemsNum^0'=1+WItemsNum^0, (-6+WItemsNum^0 >= 0 /\ -1+tmp1^post0 >= 0), cost: 4
New rule:
l4 -> [15] : (-1+n1 >= 0 /\ -6+WItemsNum^0 >= 0 /\ -1+tmp1^post0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ghlaCo.txt

Applied nonterm
Original rule:
l4 -> l4 : tmp1^0'=tmp1^post0, WItemsNum^0'=1+WItemsNum^0, (1+tmp1^post0 <= 0 /\ -6+WItemsNum^0 >= 0), cost: 4
New rule:
l4 -> [15] : (-1-tmp1^post0 >= 0 /\ -6+WItemsNum^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_cbehNa.txt

Applied simplification
Original rule:
l4 -> l4 : WItemsNum^0'=6, (0 >= 0 /\ 6-WItemsNum^0 >= 0), cost: 18-3*WItemsNum^0
New rule:
l4 -> l4 : WItemsNum^0'=6, -6+WItemsNum^0 <= 0, cost: 18-3*WItemsNum^0

Applied simplification
Original rule:
l4 -> [15] : (-1-tmp1^post0 >= 0 /\ -6+WItemsNum^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM
New rule:
l4 -> [15] : (1+tmp1^post0 <= 0 /\ -6+WItemsNum^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 44 45 46

Accelerated simple loops
Start location: l13
  20: l3 -> l4 : TRUE, cost: 1
  40: l4 -> l5 : tmp1^0'=tmp1^post0, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 3
  43: l4 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0
  48: l4 -> [15] : (-1+n1 >= 0 /\ -6+WItemsNum^0 >= 0 /\ -1+tmp1^post0 >= 0), cost: NONTERM
  50: l4 -> l4 : WItemsNum^0'=6, -6+WItemsNum^0 <= 0, cost: 18-3*WItemsNum^0
  51: l4 -> [15] : (1+tmp1^post0 <= 0 /\ -6+WItemsNum^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM
  35: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Applied chaining
First rule:
l3 -> l4 : TRUE, cost: 1
Second rule:
l4 -> [15] : (-1+n1 >= 0 /\ -6+WItemsNum^0 >= 0 /\ -1+tmp1^post0 >= 0), cost: NONTERM
New rule:
l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l3 -> l4 : TRUE, cost: 1
Second rule:
l4 -> l4 : WItemsNum^0'=6, -6+WItemsNum^0 <= 0, cost: 18-3*WItemsNum^0
New rule:
l3 -> l4 : WItemsNum^0'=6, -6+WItemsNum^0 <= 0, cost: 19-3*WItemsNum^0

Applied chaining
First rule:
l3 -> l4 : TRUE, cost: 1
Second rule:
l4 -> [15] : (1+tmp1^post0 <= 0 /\ -6+WItemsNum^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM
New rule:
l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM

Applied deletion
Removed the following rules: 48 50 51

Chained accelerated rules with incoming rules
Start location: l13
  20: l3 -> l4 : TRUE, cost: 1
  52: l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM
  53: l3 -> l4 : WItemsNum^0'=6, -6+WItemsNum^0 <= 0, cost: 19-3*WItemsNum^0
  40: l4 -> l5 : tmp1^0'=tmp1^post0, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 3
  43: l4 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0
  35: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Eliminating location l4 by chaining:

Applied chaining
First rule:
l3 -> l4 : TRUE, cost: 1
Second rule:
l4 -> l5 : tmp1^0'=tmp1^post0, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 3
New rule:
l3 -> l5 : tmp1^0'=tmp1^post0, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 4

Applied chaining
First rule:
l3 -> l4 : TRUE, cost: 1
Second rule:
l4 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0
New rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2*WItemsNum^0

Applied chaining
First rule:
l3 -> l4 : WItemsNum^0'=6, -6+WItemsNum^0 <= 0, cost: 19-3*WItemsNum^0
Second rule:
l4 -> l5 : tmp1^0'=tmp1^post0, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 3
New rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=6, (0 >= 0 /\ tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 22-3*WItemsNum^0

Applied simplification
Original rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=6, (0 >= 0 /\ tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 22-3*WItemsNum^0
New rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=6, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 22-3*WItemsNum^0

Applied chaining
First rule:
l3 -> l4 : WItemsNum^0'=6, -6+WItemsNum^0 <= 0, cost: 19-3*WItemsNum^0
Second rule:
l4 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0
New rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (0 >= 0 /\ tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 30-3*WItemsNum^0

Applied simplification
Original rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (0 >= 0 /\ tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 30-3*WItemsNum^0
New rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 30-3*WItemsNum^0

Applied deletion
Removed the following rules: 20 40 43 53

Eliminated locations on tree-shaped paths
Start location: l13
  52: l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM
  54: l3 -> l5 : tmp1^0'=tmp1^post0, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 4
  55: l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2*WItemsNum^0
  56: l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=6, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 22-3*WItemsNum^0
  57: l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 30-3*WItemsNum^0
  35: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Eliminating location l5 by chaining:

Applied chaining
First rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2*WItemsNum^0
Second rule:
l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
New rule:
l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (0 <= 0 /\ tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2+2*WItemsNum^0

Applied simplification
Original rule:
l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (0 <= 0 /\ tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2+2*WItemsNum^0
New rule:
l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2+2*WItemsNum^0

Applied chaining
First rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 30-3*WItemsNum^0
Second rule:
l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2
New rule:
l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (0 <= 0 /\ tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 32-3*WItemsNum^0

Applied simplification
Original rule:
l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (0 <= 0 /\ tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 32-3*WItemsNum^0
New rule:
l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 32-3*WItemsNum^0

Applied partial deletion
Original rule:
l3 -> l5 : tmp1^0'=tmp1^post0, WItemsNum^0'=6, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 22-3*WItemsNum^0
New rule:
l3 -> [16] : (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 22-3*WItemsNum^0

Applied deletion
Removed the following rules: 35 54 55 56 57

Eliminated locations on tree-shaped paths
Start location: l13
  52: l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM
  58: l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2+2*WItemsNum^0
  59: l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 32-3*WItemsNum^0
  60: l3 -> [16] : (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 22-3*WItemsNum^0
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Applied pruning (of leafs and parallel rules):
Start location: l13
  52: l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM
  58: l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2+2*WItemsNum^0
  59: l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 32-3*WItemsNum^0
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Applied simplification
Original rule:
l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 >= 0), cost: 2+2*WItemsNum^0
New rule:
l3 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^0 >= 0, cost: 2+2*WItemsNum^0

Applied simplification
Original rule:
l3 -> l3 : tmp1^0'=tmp1^post0, WItemsNum^0'=2, (tmp1^post0 == 0 /\ -6+WItemsNum^0 <= 0), cost: 32-3*WItemsNum^0
New rule:
l3 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^0 <= 0, cost: 32-3*WItemsNum^0

Simplified simple loops
Start location: l13
  52: l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM
  61: l3 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^0 >= 0, cost: 2+2*WItemsNum^0
  62: l3 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^0 <= 0, cost: 32-3*WItemsNum^0
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Applied nonterm
Original rule:
l3 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^0 <= 0, cost: 32-3*WItemsNum^0
New rule:
l3 -> [17] : (6-WItemsNum^0 >= 0 /\ -1+n8 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nOognG.txt

Applied simplification
Original rule:
l3 -> [17] : (6-WItemsNum^0 >= 0 /\ -1+n8 >= 0), cost: NONTERM
New rule:
l3 -> [17] : (-6+WItemsNum^0 <= 0 /\ -1+n8 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 62

Accelerated simple loops
Start location: l13
  52: l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM
  61: l3 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^0 >= 0, cost: 2+2*WItemsNum^0
  64: l3 -> [17] : (-6+WItemsNum^0 <= 0 /\ -1+n8 >= 0), cost: NONTERM
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2


Applied chaining
First rule:
l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2
Second rule:
l3 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^0 >= 0, cost: 2+2*WItemsNum^0
New rule:
l13 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^post16 >= 0, cost: 4+2*WItemsNum^post16

Applied chaining
First rule:
l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2
Second rule:
l3 -> [17] : (-6+WItemsNum^0 <= 0 /\ -1+n8 >= 0), cost: NONTERM
New rule:
l13 -> [17] : 0 == 0, cost: NONTERM

Applied deletion
Removed the following rules: 61 64

Chained accelerated rules with incoming rules
Start location: l13
  52: l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM
  32: l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2
  65: l13 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^post16 >= 0, cost: 4+2*WItemsNum^post16
  66: l13 -> [17] : 0 == 0, cost: NONTERM


Eliminating location l3 by chaining:

Applied chaining
First rule:
l13 -> l3 : WItemsNum^0'=WItemsNum^post16, 0 == 0, cost: 2
Second rule:
l3 -> [15] : -6+WItemsNum^0 >= 0, cost: NONTERM
New rule:
l13 -> [15] : (0 == 0 /\ -6+WItemsNum^post16 >= 0), cost: NONTERM

Applied simplification
Original rule:
l13 -> [15] : (0 == 0 /\ -6+WItemsNum^post16 >= 0), cost: NONTERM
New rule:
l13 -> [15] : -6+WItemsNum^post16 >= 0, cost: NONTERM

Applied partial deletion
Original rule:
l13 -> l3 : tmp1^0'=0, WItemsNum^0'=2, -6+WItemsNum^post16 >= 0, cost: 4+2*WItemsNum^post16
New rule:
l13 -> [18] : -6+WItemsNum^post16 >= 0, cost: 4+2*WItemsNum^post16

Applied deletion
Removed the following rules: 32 52 65

Eliminated locations on tree-shaped paths
Start location: l13
  66: l13 -> [17] : 0 == 0, cost: NONTERM
  67: l13 -> [15] : -6+WItemsNum^post16 >= 0, cost: NONTERM
  68: l13 -> [18] : -6+WItemsNum^post16 >= 0, cost: 4+2*WItemsNum^post16


Computing asymptotic complexity
Proved nontermination of rule 66 via SMT.

Proved the following lower bound
Complexity:  Nonterm
Cpx degree: Nonterm

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  0 == 0