NO

Initial ITS
Start location: l6
   0: l0 -> l1 : sx^0'=sx^post0, ox^0'=ox^post0, z^0'=z^post0, sz^0'=sz^post0, oz^0'=oz^post0, c^0'=c^post0, y^0'=y^post0, sy^0'=sy^post0, oy^0'=oy^post0, x^0'=x^post0, (-sz^post0+sz^0 == 0 /\ ox^0-ox^post0 == 0 /\ c^0-c^post0 == 0 /\ y^0-y^post0 == 0 /\ -sy^post0+sy^0 == 0 /\ -x^post0+x^0 == 0 /\ sx^0-sx^post0 == 0 /\ -oy^post0+oy^0 == 0 /\ -oz^post0+oz^0 == 0 /\ z^0-z^post0 == 0), cost: 1
   1: l2 -> l0 : sx^0'=sx^post1, ox^0'=ox^post1, z^0'=z^post1, sz^0'=sz^post1, oz^0'=oz^post1, c^0'=c^post1, y^0'=y^post1, sy^0'=sy^post1, oy^0'=oy^post1, x^0'=x^post1, (y^0-y^post1 == 0 /\ sx^0 <= 0 /\ -oz^post1+oz^0 == 0 /\ -x^post1+x^0 == 0 /\ ox^0-ox^post1 == 0 /\ -sz^post1+sz^0 == 0 /\ c^0-c^post1 == 0 /\ -z^post1+z^0 == 0 /\ -sy^post1+sy^0 == 0 /\ sx^0-sx^post1 == 0 /\ -oy^post1+oy^0 == 0), cost: 1
   2: l2 -> l0 : sx^0'=sx^post2, ox^0'=ox^post2, z^0'=z^post2, sz^0'=sz^post2, oz^0'=oz^post2, c^0'=c^post2, y^0'=y^post2, sy^0'=sy^post2, oy^0'=oy^post2, x^0'=x^post2, (y^0-y^post2 == 0 /\ -oz^post2+oz^0 == 0 /\ -x^post2+x^0 == 0 /\ -sz^post2+sz^0 == 0 /\ c^0-c^post2 == 0 /\ ox^0-ox^post2 == 0 /\ -z^post2+z^0 == 0 /\ -sy^post2+sy^0 == 0 /\ sx^0-sx^post2 == 0 /\ ox^0-x^0 <= 0 /\ -oy^post2+oy^0 == 0), cost: 1
   3: l3 -> l4 : sx^0'=sx^post3, ox^0'=ox^post3, z^0'=z^post3, sz^0'=sz^post3, oz^0'=oz^post3, c^0'=c^post3, y^0'=y^post3, sy^0'=sy^post3, oy^0'=oy^post3, x^0'=x^post3, (x^post3-z^0 == 0 /\ 1+y^post3-y^0 == 0 /\ sx^0-sx^post3 == 0 /\ ox^0-ox^post3 == 0 /\ -c^post3+c^0 == 0 /\ sy^0-sy^post3 == 0 /\ -oy^post3+oy^0 == 0 /\ -z^post3+z^0 == 0 /\ oz^0-oz^post3 == 0 /\ sz^0-sz^post3 == 0), cost: 1
   4: l3 -> l4 : sx^0'=sx^post4, ox^0'=ox^post4, z^0'=z^post4, sz^0'=sz^post4, oz^0'=oz^post4, c^0'=c^post4, y^0'=y^post4, sy^0'=sy^post4, oy^0'=oy^post4, x^0'=x^post4, (-y^post4+y^0 == 0 /\ oz^0-oz^post4 == 0 /\ sz^0-sz^post4 == 0 /\ -c^post4+c^0 == 0 /\ -oy^post4+oy^0 == 0 /\ sy^0-sy^post4 == 0 /\ z^0-z^post4 == 0 /\ -sx^post4+sx^0 == 0 /\ ox^0-ox^post4 == 0 /\ 1+x^post4-x^0 == 0), cost: 1
   5: l4 -> l3 : sx^0'=sx^post5, ox^0'=ox^post5, z^0'=z^post5, sz^0'=sz^post5, oz^0'=oz^post5, c^0'=c^post5, y^0'=y^post5, sy^0'=sy^post5, oy^0'=oy^post5, x^0'=x^post5, (-y^post5+y^0 == 0 /\ -z^0+sz^post5 == 0 /\ -y^0+sy^post5 == 0 /\ -y^0+oy^post5 == 0 /\ -z^0+oz^post5 == 0 /\ sx^post5-x^0 == 0 /\ -1+c^post5 == 0 /\ ox^post5-x^0 == 0 /\ -x^post5+x^0 == 0 /\ z^0-z^post5 == 0), cost: 1
   6: l4 -> l2 : sx^0'=sx^post6, ox^0'=ox^post6, z^0'=z^post6, sz^0'=sz^post6, oz^0'=oz^post6, c^0'=c^post6, y^0'=y^post6, sy^0'=sy^post6, oy^0'=oy^post6, x^0'=x^post6, (oz^0-oz^post6 == 0 /\ -oy^post6+oy^0 == 0 /\ sz^0-sz^post6 == 0 /\ sx^0-sx^post6 == 0 /\ -ox^post6+ox^0 == 0 /\ -sy^post6+sy^0 == 0 /\ z^0-z^post6 == 0 /\ -c^post6+c^0 == 0 /\ -y^post6+y^0 == 0 /\ 1-c^0 <= 0 /\ -x^post6+x^0 == 0), cost: 1
   7: l4 -> l3 : sx^0'=sx^post7, ox^0'=ox^post7, z^0'=z^post7, sz^0'=sz^post7, oz^0'=oz^post7, c^0'=c^post7, y^0'=y^post7, sy^0'=sy^post7, oy^0'=oy^post7, x^0'=x^post7, (-sy^post7+sy^0 == 0 /\ 1-x^0 <= 0 /\ -c^post7+c^0 == 0 /\ sx^0-sx^post7 == 0 /\ z^0-z^post7 == 0 /\ ox^0-ox^post7 == 0 /\ oy^0-oy^post7 == 0 /\ oz^0-oz^post7 == 0 /\ -x^post7+x^0 == 0 /\ sz^0-sz^post7 == 0 /\ -y^post7+y^0 == 0), cost: 1
   8: l4 -> l3 : sx^0'=sx^post8, ox^0'=ox^post8, z^0'=z^post8, sz^0'=sz^post8, oz^0'=oz^post8, c^0'=c^post8, y^0'=y^post8, sy^0'=sy^post8, oy^0'=oy^post8, x^0'=x^post8, (1-x^0 <= 0 /\ sx^post8-x^0 == 0 /\ z^0-z^post8 == 0 /\ -x^post8+x^0 == 0 /\ oz^0-oz^post8 == 0 /\ -oy^post8+oy^0 == 0 /\ -y^post8+y^0 == 0 /\ -c^post8+c^0 == 0 /\ -z^0+sz^post8 == 0 /\ sy^post8-y^0 == 0 /\ -ox^post8+ox^0 == 0), cost: 1
   9: l5 -> l4 : sx^0'=sx^post9, ox^0'=ox^post9, z^0'=z^post9, sz^0'=sz^post9, oz^0'=oz^post9, c^0'=c^post9, y^0'=y^post9, sy^0'=sy^post9, oy^0'=oy^post9, x^0'=x^post9, (-y^post9+y^0 == 0 /\ -ox^post9+ox^0 == 0 /\ -x^post9+x^0 == 0 /\ c^post9 == 0 /\ z^0-z^post9 == 0 /\ oy^0-oy^post9 == 0 /\ sz^0-sz^post9 == 0 /\ oz^0-oz^post9 == 0 /\ sx^0-sx^post9 == 0 /\ -sy^post9+sy^0 == 0), cost: 1
  10: l6 -> l5 : sx^0'=sx^post10, ox^0'=ox^post10, z^0'=z^post10, sz^0'=sz^post10, oz^0'=oz^post10, c^0'=c^post10, y^0'=y^post10, sy^0'=sy^post10, oy^0'=oy^post10, x^0'=x^post10, (-sz^post10+sz^0 == 0 /\ sx^0-sx^post10 == 0 /\ -x^post10+x^0 == 0 /\ ox^0-ox^post10 == 0 /\ c^0-c^post10 == 0 /\ -sy^post10+sy^0 == 0 /\ y^0-y^post10 == 0 /\ oz^0-oz^post10 == 0 /\ -oy^post10+oy^0 == 0 /\ z^0-z^post10 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l6
   3: l3 -> l4 : sx^0'=sx^post3, ox^0'=ox^post3, z^0'=z^post3, sz^0'=sz^post3, oz^0'=oz^post3, c^0'=c^post3, y^0'=y^post3, sy^0'=sy^post3, oy^0'=oy^post3, x^0'=x^post3, (x^post3-z^0 == 0 /\ 1+y^post3-y^0 == 0 /\ sx^0-sx^post3 == 0 /\ ox^0-ox^post3 == 0 /\ -c^post3+c^0 == 0 /\ sy^0-sy^post3 == 0 /\ -oy^post3+oy^0 == 0 /\ -z^post3+z^0 == 0 /\ oz^0-oz^post3 == 0 /\ sz^0-sz^post3 == 0), cost: 1
   4: l3 -> l4 : sx^0'=sx^post4, ox^0'=ox^post4, z^0'=z^post4, sz^0'=sz^post4, oz^0'=oz^post4, c^0'=c^post4, y^0'=y^post4, sy^0'=sy^post4, oy^0'=oy^post4, x^0'=x^post4, (-y^post4+y^0 == 0 /\ oz^0-oz^post4 == 0 /\ sz^0-sz^post4 == 0 /\ -c^post4+c^0 == 0 /\ -oy^post4+oy^0 == 0 /\ sy^0-sy^post4 == 0 /\ z^0-z^post4 == 0 /\ -sx^post4+sx^0 == 0 /\ ox^0-ox^post4 == 0 /\ 1+x^post4-x^0 == 0), cost: 1
   5: l4 -> l3 : sx^0'=sx^post5, ox^0'=ox^post5, z^0'=z^post5, sz^0'=sz^post5, oz^0'=oz^post5, c^0'=c^post5, y^0'=y^post5, sy^0'=sy^post5, oy^0'=oy^post5, x^0'=x^post5, (-y^post5+y^0 == 0 /\ -z^0+sz^post5 == 0 /\ -y^0+sy^post5 == 0 /\ -y^0+oy^post5 == 0 /\ -z^0+oz^post5 == 0 /\ sx^post5-x^0 == 0 /\ -1+c^post5 == 0 /\ ox^post5-x^0 == 0 /\ -x^post5+x^0 == 0 /\ z^0-z^post5 == 0), cost: 1
   7: l4 -> l3 : sx^0'=sx^post7, ox^0'=ox^post7, z^0'=z^post7, sz^0'=sz^post7, oz^0'=oz^post7, c^0'=c^post7, y^0'=y^post7, sy^0'=sy^post7, oy^0'=oy^post7, x^0'=x^post7, (-sy^post7+sy^0 == 0 /\ 1-x^0 <= 0 /\ -c^post7+c^0 == 0 /\ sx^0-sx^post7 == 0 /\ z^0-z^post7 == 0 /\ ox^0-ox^post7 == 0 /\ oy^0-oy^post7 == 0 /\ oz^0-oz^post7 == 0 /\ -x^post7+x^0 == 0 /\ sz^0-sz^post7 == 0 /\ -y^post7+y^0 == 0), cost: 1
   8: l4 -> l3 : sx^0'=sx^post8, ox^0'=ox^post8, z^0'=z^post8, sz^0'=sz^post8, oz^0'=oz^post8, c^0'=c^post8, y^0'=y^post8, sy^0'=sy^post8, oy^0'=oy^post8, x^0'=x^post8, (1-x^0 <= 0 /\ sx^post8-x^0 == 0 /\ z^0-z^post8 == 0 /\ -x^post8+x^0 == 0 /\ oz^0-oz^post8 == 0 /\ -oy^post8+oy^0 == 0 /\ -y^post8+y^0 == 0 /\ -c^post8+c^0 == 0 /\ -z^0+sz^post8 == 0 /\ sy^post8-y^0 == 0 /\ -ox^post8+ox^0 == 0), cost: 1
   9: l5 -> l4 : sx^0'=sx^post9, ox^0'=ox^post9, z^0'=z^post9, sz^0'=sz^post9, oz^0'=oz^post9, c^0'=c^post9, y^0'=y^post9, sy^0'=sy^post9, oy^0'=oy^post9, x^0'=x^post9, (-y^post9+y^0 == 0 /\ -ox^post9+ox^0 == 0 /\ -x^post9+x^0 == 0 /\ c^post9 == 0 /\ z^0-z^post9 == 0 /\ oy^0-oy^post9 == 0 /\ sz^0-sz^post9 == 0 /\ oz^0-oz^post9 == 0 /\ sx^0-sx^post9 == 0 /\ -sy^post9+sy^0 == 0), cost: 1
  10: l6 -> l5 : sx^0'=sx^post10, ox^0'=ox^post10, z^0'=z^post10, sz^0'=sz^post10, oz^0'=oz^post10, c^0'=c^post10, y^0'=y^post10, sy^0'=sy^post10, oy^0'=oy^post10, x^0'=x^post10, (-sz^post10+sz^0 == 0 /\ sx^0-sx^post10 == 0 /\ -x^post10+x^0 == 0 /\ ox^0-ox^post10 == 0 /\ c^0-c^post10 == 0 /\ -sy^post10+sy^0 == 0 /\ y^0-y^post10 == 0 /\ oz^0-oz^post10 == 0 /\ -oy^post10+oy^0 == 0 /\ z^0-z^post10 == 0), cost: 1


Applied preprocessing
Original rule:
l3 -> l4 : sx^0'=sx^post3, ox^0'=ox^post3, z^0'=z^post3, sz^0'=sz^post3, oz^0'=oz^post3, c^0'=c^post3, y^0'=y^post3, sy^0'=sy^post3, oy^0'=oy^post3, x^0'=x^post3, (x^post3-z^0 == 0 /\ 1+y^post3-y^0 == 0 /\ sx^0-sx^post3 == 0 /\ ox^0-ox^post3 == 0 /\ -c^post3+c^0 == 0 /\ sy^0-sy^post3 == 0 /\ -oy^post3+oy^0 == 0 /\ -z^post3+z^0 == 0 /\ oz^0-oz^post3 == 0 /\ sz^0-sz^post3 == 0), cost: 1
New rule:
l3 -> l4 : y^0'=-1+y^0, x^0'=z^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l4 : sx^0'=sx^post4, ox^0'=ox^post4, z^0'=z^post4, sz^0'=sz^post4, oz^0'=oz^post4, c^0'=c^post4, y^0'=y^post4, sy^0'=sy^post4, oy^0'=oy^post4, x^0'=x^post4, (-y^post4+y^0 == 0 /\ oz^0-oz^post4 == 0 /\ sz^0-sz^post4 == 0 /\ -c^post4+c^0 == 0 /\ -oy^post4+oy^0 == 0 /\ sy^0-sy^post4 == 0 /\ z^0-z^post4 == 0 /\ -sx^post4+sx^0 == 0 /\ ox^0-ox^post4 == 0 /\ 1+x^post4-x^0 == 0), cost: 1
New rule:
l3 -> l4 : x^0'=-1+x^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l3 : sx^0'=sx^post5, ox^0'=ox^post5, z^0'=z^post5, sz^0'=sz^post5, oz^0'=oz^post5, c^0'=c^post5, y^0'=y^post5, sy^0'=sy^post5, oy^0'=oy^post5, x^0'=x^post5, (-y^post5+y^0 == 0 /\ -z^0+sz^post5 == 0 /\ -y^0+sy^post5 == 0 /\ -y^0+oy^post5 == 0 /\ -z^0+oz^post5 == 0 /\ sx^post5-x^0 == 0 /\ -1+c^post5 == 0 /\ ox^post5-x^0 == 0 /\ -x^post5+x^0 == 0 /\ z^0-z^post5 == 0), cost: 1
New rule:
l4 -> l3 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l3 : sx^0'=sx^post7, ox^0'=ox^post7, z^0'=z^post7, sz^0'=sz^post7, oz^0'=oz^post7, c^0'=c^post7, y^0'=y^post7, sy^0'=sy^post7, oy^0'=oy^post7, x^0'=x^post7, (-sy^post7+sy^0 == 0 /\ 1-x^0 <= 0 /\ -c^post7+c^0 == 0 /\ sx^0-sx^post7 == 0 /\ z^0-z^post7 == 0 /\ ox^0-ox^post7 == 0 /\ oy^0-oy^post7 == 0 /\ oz^0-oz^post7 == 0 /\ -x^post7+x^0 == 0 /\ sz^0-sz^post7 == 0 /\ -y^post7+y^0 == 0), cost: 1
New rule:
l4 -> l3 : -1+x^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l3 : sx^0'=sx^post8, ox^0'=ox^post8, z^0'=z^post8, sz^0'=sz^post8, oz^0'=oz^post8, c^0'=c^post8, y^0'=y^post8, sy^0'=sy^post8, oy^0'=oy^post8, x^0'=x^post8, (1-x^0 <= 0 /\ sx^post8-x^0 == 0 /\ z^0-z^post8 == 0 /\ -x^post8+x^0 == 0 /\ oz^0-oz^post8 == 0 /\ -oy^post8+oy^0 == 0 /\ -y^post8+y^0 == 0 /\ -c^post8+c^0 == 0 /\ -z^0+sz^post8 == 0 /\ sy^post8-y^0 == 0 /\ -ox^post8+ox^0 == 0), cost: 1
New rule:
l4 -> l3 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, -1+x^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l4 : sx^0'=sx^post9, ox^0'=ox^post9, z^0'=z^post9, sz^0'=sz^post9, oz^0'=oz^post9, c^0'=c^post9, y^0'=y^post9, sy^0'=sy^post9, oy^0'=oy^post9, x^0'=x^post9, (-y^post9+y^0 == 0 /\ -ox^post9+ox^0 == 0 /\ -x^post9+x^0 == 0 /\ c^post9 == 0 /\ z^0-z^post9 == 0 /\ oy^0-oy^post9 == 0 /\ sz^0-sz^post9 == 0 /\ oz^0-oz^post9 == 0 /\ sx^0-sx^post9 == 0 /\ -sy^post9+sy^0 == 0), cost: 1
New rule:
l5 -> l4 : c^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : sx^0'=sx^post10, ox^0'=ox^post10, z^0'=z^post10, sz^0'=sz^post10, oz^0'=oz^post10, c^0'=c^post10, y^0'=y^post10, sy^0'=sy^post10, oy^0'=oy^post10, x^0'=x^post10, (-sz^post10+sz^0 == 0 /\ sx^0-sx^post10 == 0 /\ -x^post10+x^0 == 0 /\ ox^0-ox^post10 == 0 /\ c^0-c^post10 == 0 /\ -sy^post10+sy^0 == 0 /\ y^0-y^post10 == 0 /\ oz^0-oz^post10 == 0 /\ -oy^post10+oy^0 == 0 /\ z^0-z^post10 == 0), cost: 1
New rule:
l6 -> l5 : TRUE, cost: 1

Simplified rules
Start location: l6
  11: l3 -> l4 : y^0'=-1+y^0, x^0'=z^0, TRUE, cost: 1
  12: l3 -> l4 : x^0'=-1+x^0, TRUE, cost: 1
  13: l4 -> l3 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, TRUE, cost: 1
  14: l4 -> l3 : -1+x^0 >= 0, cost: 1
  15: l4 -> l3 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, -1+x^0 >= 0, cost: 1
  16: l5 -> l4 : c^0'=0, TRUE, cost: 1
  17: l6 -> l5 : TRUE, cost: 1


Eliminating location l5 by chaining:

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

Applied deletion
Removed the following rules: 16 17

Eliminated locations on linear paths
Start location: l6
  11: l3 -> l4 : y^0'=-1+y^0, x^0'=z^0, TRUE, cost: 1
  12: l3 -> l4 : x^0'=-1+x^0, TRUE, cost: 1
  13: l4 -> l3 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, TRUE, cost: 1
  14: l4 -> l3 : -1+x^0 >= 0, cost: 1
  15: l4 -> l3 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, -1+x^0 >= 0, cost: 1
  18: l6 -> l4 : c^0'=0, TRUE, cost: 2


Eliminating location l3 by chaining:

Applied chaining
First rule:
l4 -> l3 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, TRUE, cost: 1
Second rule:
l3 -> l4 : y^0'=-1+y^0, x^0'=z^0, TRUE, cost: 1
New rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2

Applied chaining
First rule:
l4 -> l3 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, TRUE, cost: 1
Second rule:
l3 -> l4 : x^0'=-1+x^0, TRUE, cost: 1
New rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2

Applied chaining
First rule:
l4 -> l3 : -1+x^0 >= 0, cost: 1
Second rule:
l3 -> l4 : y^0'=-1+y^0, x^0'=z^0, TRUE, cost: 1
New rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2

Applied chaining
First rule:
l4 -> l3 : -1+x^0 >= 0, cost: 1
Second rule:
l3 -> l4 : x^0'=-1+x^0, TRUE, cost: 1
New rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2

Applied chaining
First rule:
l4 -> l3 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, -1+x^0 >= 0, cost: 1
Second rule:
l3 -> l4 : y^0'=-1+y^0, x^0'=z^0, TRUE, cost: 1
New rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2

Applied chaining
First rule:
l4 -> l3 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, -1+x^0 >= 0, cost: 1
Second rule:
l3 -> l4 : x^0'=-1+x^0, TRUE, cost: 1
New rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 11 12 13 14 15

Eliminated locations on tree-shaped paths
Start location: l6
  19: l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
  20: l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
  21: l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
  22: l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
  23: l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
  24: l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
  18: l6 -> l4 : c^0'=0, TRUE, cost: 2


Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> [7] : -2+n >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mdGLLc.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
New rule:
l4 -> [7] : -1+n0 >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mgIBeG.txt

Applied acceleration
Original rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mELgdn.txt

Applied nonterm
Original rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_DBHhIf.txt

Applied acceleration
Original rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : x^0'=-n2+x^0, (-n2+x^0 >= 0 /\ n2 >= 0), cost: 2*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_LHPHgF.txt

Applied instantiation
Original rule:
l4 -> l4 : x^0'=-n2+x^0, (-n2+x^0 >= 0 /\ n2 >= 0), cost: 2*n2
New rule:
l4 -> l4 : x^0'=0, (0 >= 0 /\ x^0 >= 0), cost: 2*x^0

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PnGPFd.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_hohjje.txt

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=1-n4+x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-n4+x^0, (-n4+x^0 >= 0 /\ -1+n4 >= 0), cost: 2*n4
Sub-proof via acceration calculus written to file:///tmp/tmpnam_eJhokf.txt

Applied instantiation
Original rule:
l4 -> l4 : sx^0'=1-n4+x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-n4+x^0, (-n4+x^0 >= 0 /\ -1+n4 >= 0), cost: 2*n4
New rule:
l4 -> l4 : sx^0'=1, sz^0'=z^0, sy^0'=y^0, x^0'=0, (0 >= 0 /\ -1+x^0 >= 0), cost: 2*x^0

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=-1+x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=-1+x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=-1+z^0, sz^0'=z^0, y^0'=y^0-n5, sy^0'=1+y^0-n5, x^0'=z^0, (-2+z^0 >= 0 /\ -2+n5 >= 0 /\ -2+x^0 >= 0), cost: 4*n5
Sub-proof via acceration calculus written to file:///tmp/tmpnam_aBlidl.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=-1+x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_lNffKp.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-n7+y^0, sy^0'=1-n7+y^0, x^0'=z^0, (-2+n7 >= 0 /\ -2+z^0 >= 0 /\ -2+x^0 >= 0), cost: 4*n7
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NjFNib.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_phhLnc.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=-1+x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=-1+x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=-1+z^0, ox^0'=-1+z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n9+y^0, sy^0'=1-n9+y^0, oy^0'=1-n9+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -2+n9 >= 0 /\ -1+z^0 >= 0), cost: 4*n9
Sub-proof via acceration calculus written to file:///tmp/tmpnam_fpKpBm.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=-1+x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_InAmHI.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-n10+y^0, sy^0'=-n10+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -1+n10 >= 0), cost: 4*n10
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PhCdeM.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_dklfpn.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> l4 : sx^0'=-1+z^0, sz^0'=z^0, y^0'=-n11+y^0, sy^0'=1-n11+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -2+n11 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0), cost: 4*n11
Sub-proof via acceration calculus written to file:///tmp/tmpnam_GeEfPa.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kipPhF.txt

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-2+y^0, sy^0'=y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-2+y^0, sy^0'=y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-2*n12+y^0, sy^0'=2-2*n12+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -2+n12 >= 0 /\ -1+z^0 >= 0), cost: 4*n12
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pmiHal.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-2+y^0, sy^0'=y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_CohEpf.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=-1+z^0, -1+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=-1+z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n13+y^0, sy^0'=-n13+y^0, oy^0'=-n13+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n13 >= 0 /\ -2+z^0 >= 0), cost: 4*n13
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mPGime.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=-1+z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_adncEO.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2*n14+y^0, sy^0'=1-2*n14+y^0, oy^0'=1-2*n14+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n14 >= 0 /\ -1+z^0 >= 0), cost: 4*n14
Sub-proof via acceration calculus written to file:///tmp/tmpnam_OJLnMk.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_BaFKob.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=-1+x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=-1+x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=-1+z^0, sz^0'=z^0, y^0'=-n16+y^0, sy^0'=1-n16+y^0, x^0'=z^0, (-2+z^0 >= 0 /\ -2+n16 >= 0 /\ -2+x^0 >= 0), cost: 4*n16
Sub-proof via acceration calculus written to file:///tmp/tmpnam_npMdeD.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=-1+x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_HalJfn.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : y^0'=-n17+y^0, x^0'=z^0, (-2+z^0 >= 0 /\ -1+n17 >= 0 /\ -2+x^0 >= 0), cost: 4*n17
Sub-proof via acceration calculus written to file:///tmp/tmpnam_oDCdbM.txt

Applied nonterm
Original rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_AemJoD.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=-1+x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=-1+x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=-1+z^0, ox^0'=-1+z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n19+y^0, sy^0'=1-n19+y^0, oy^0'=1-n19+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n19 >= 0), cost: 4*n19
Sub-proof via acceration calculus written to file:///tmp/tmpnam_keekcd.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=-1+x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_cHCfmM.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-n20+y^0, sy^0'=-n20+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -1+n20 >= 0), cost: 4*n20
Sub-proof via acceration calculus written to file:///tmp/tmpnam_gfHeff.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_jNjAEG.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-2+y^0, sy^0'=-1+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-2+y^0, sy^0'=-1+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-2*n21+y^0, sy^0'=1-2*n21+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n21 >= 0 /\ -1+z^0 >= 0), cost: 4*n21
Sub-proof via acceration calculus written to file:///tmp/tmpnam_MckDOp.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-2+y^0, sy^0'=-1+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_eddoKN.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4

Applied acceleration
Original rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> l4 : y^0'=-n22+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -1+n22 >= 0), cost: 4*n22
Sub-proof via acceration calculus written to file:///tmp/tmpnam_BklAdm.txt

Applied nonterm
Original rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bEgDMe.txt

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=-1+z^0, -1+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=-1+z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n23+y^0, sy^0'=-n23+y^0, oy^0'=-n23+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n23 >= 0 /\ -2+z^0 >= 0), cost: 4*n23
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PNnJoB.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=-1+z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_eBLkEk.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2*n24+y^0, sy^0'=1-2*n24+y^0, oy^0'=1-2*n24+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n24 >= 0 /\ -1+z^0 >= 0), cost: 4*n24
Sub-proof via acceration calculus written to file:///tmp/tmpnam_DEJiCG.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_blHpfe.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=-1+z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n26+y^0, sy^0'=1-n26+y^0, oy^0'=1-n26+y^0, x^0'=z^0, (-2+z^0 >= 0 /\ -2+n26 >= 0 /\ -2+x^0 >= 0), cost: 4*n26
Sub-proof via acceration calculus written to file:///tmp/tmpnam_Gafeba.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ANGdhh.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n28+y^0, sy^0'=1-n28+y^0, oy^0'=1-n28+y^0, x^0'=z^0, (-2+n28 >= 0 /\ -2+z^0 >= 0 /\ -2+x^0 >= 0), cost: 4*n28
Sub-proof via acceration calculus written to file:///tmp/tmpnam_EBKicp.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -2+x^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kaHpee.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=-1+x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 4

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=-1+x^0, ox^0'=-1+x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 4
New rule:
l4 -> [7] : -2+n29 >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_GCbbcJ.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : -2+n29 >= 0, cost: NONTERM
New rule:
l4 -> [7] : -2+n29 >= 0, cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=y^0, x^0'=-1+z^0, -1+z^0 >= 0, cost: 4

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=y^0, x^0'=-1+z^0, -1+z^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n30 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_IfLPbm.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n30 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n30 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=-1+y^0, oy^0'=y^0, x^0'=z^0, -1+z^0 >= 0, cost: 4

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=-1+y^0, oy^0'=y^0, x^0'=z^0, -1+z^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-2+n31 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_hjanjN.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-2+n31 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n31 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=-1+z^0, -1+z^0 >= 0, cost: 4

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=-1+z^0, -1+z^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n32 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_BFiFfl.txt

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n32 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n32 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+z^0 >= 0, cost: 4

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-2+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+z^0 >= 0, cost: 4
New rule:
l4 -> [7] : (-2+n33 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NhHJde.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-2+n33 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n33 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=-1+z^0, TRUE, cost: 4

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=-1+y^0, x^0'=-1+z^0, TRUE, cost: 4
New rule:
l4 -> [7] : -1+n34 >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_fHCbdP.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> [7] : -1+n34 >= 0, cost: NONTERM
New rule:
l4 -> [7] : -1+n34 >= 0, cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
New rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=y^0-n1, sy^0'=y^0, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=y^0-n1, sy^0'=y^0, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n35*n1, sy^0'=-(-1+n35)*n1+y^0, x^0'=z^0, (-1+n1 >= 0 /\ -2+n35 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2*n35+2*n35*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_iLpAfE.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=y^0-n1, sy^0'=y^0, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_hMmfaC.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n1, sy^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n1, sy^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n36*n1, sy^0'=-(-1+n36)*n1+y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+n36 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0), cost: 2*n36+2*n36*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PImPCC.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n1, sy^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_IJjaAi.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n38*n3, sy^0'=1+y^0-n3*(-1+n38)-n3, x^0'=z^0, (-2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0 /\ -1+n38 >= 0), cost: 2*n38+2*n38*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mhIdpn.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PmOiEj.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n39*n3, sy^0'=-(-1+n39)*n3+y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n39 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n39+2*n39*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_IiBHhK.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_OhMGJF.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, sy^0'=y^0, x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
New rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0-n1, sy^0'=y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0-n1, sy^0'=y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-n40+y^0-n40*n1, sy^0'=1-(-1+n40)*n1-n40+y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+n40 >= 0), cost: 2*n40+2*n40*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_CpgpoI.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0-n1, sy^0'=y^0, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_EhKgOb.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n1, sy^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n1, sy^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-n41+y^0-n41*n1, sy^0'=1-n41-(-1+n41)*n1+y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -1+n41 >= 0), cost: 2*n41+2*n41*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_KJIbFn.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n1, sy^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_FkNoAC.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
New rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : y^0'=-n1*n44+y^0, x^0'=z^0, (-1+n44 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2*n1*n44+2*n44
Sub-proof via acceration calculus written to file:///tmp/tmpnam_diHKcJ.txt

Applied nonterm
Original rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_HpkMHa.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : y^0'=-n45*n1+y^0, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+n45 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0), cost: 2*n45*n1+2*n45
Sub-proof via acceration calculus written to file:///tmp/tmpnam_CHbmPL.txt

Applied nonterm
Original rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_IGbDAL.txt

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n46*n3, sy^0'=1+y^0-n3-(-1+n46)*n3, x^0'=z^0, (-1+n46 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2*n46+2*n46*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_eLMjME.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_efCElD.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n47*n3, sy^0'=1+y^0-n3-(-1+n47)*n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -1+n47 >= 0), cost: 2*n47+2*n47*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_JGFFdc.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_IlECjg.txt

Applied chaining
First rule:
l4 -> l4 : x^0'=-1+x^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n3, sy^0'=y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n3, sy^0'=y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-n50+y^0-n50*n3, sy^0'=1-n50+y^0-(-1+n50)*n3-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n50 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n50+2*n50*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kpJGmm.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n3, sy^0'=y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_fgPDPj.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-n3*n51+y^0-n51, sy^0'=2+y^0-(-1+n51)*n3-n3-n51, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n51 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3*n51+2*n51
Sub-proof via acceration calculus written to file:///tmp/tmpnam_hcFcpe.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=-1+y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_FLiaMp.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=-1+y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
New rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n1, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n1, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n53*n1, sy^0'=-(-1+n53)*n1+y^0, oy^0'=-(-1+n53)*n1+y^0, x^0'=z^0, (-1+n1 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n53 >= 0 /\ -2+x^0 >= 0), cost: 2*n53+2*n53*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ImKEjf.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n1, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_HIgJoK.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n1, sy^0'=y^0-n1, oy^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n1, sy^0'=y^0-n1, oy^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n54*n1+y^0, sy^0'=-(-1+n54)*n1+y^0-n1, oy^0'=-(-1+n54)*n1+y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -1+n54 >= 0), cost: 2*n54+2*n54*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_fBnpFF.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n1, sy^0'=y^0-n1, oy^0'=y^0-n1, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bPlCia.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n3, sy^0'=1+y^0-n3, oy^0'=y^0, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n3, sy^0'=1+y^0-n3, oy^0'=y^0, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n57*n3+y^0, sy^0'=1-(-1+n57)*n3+y^0-n3, oy^0'=-(-1+n57)*n3+y^0, x^0'=z^0, (-2+n57 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2*n57*n3+2*n57
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kKbjBM.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n3, sy^0'=1+y^0-n3, oy^0'=y^0, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -2+x^0 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_KGnElE.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n3, sy^0'=y^0-n3, oy^0'=y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n3, sy^0'=y^0-n3, oy^0'=y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n58*n3+y^0, sy^0'=-(-1+n58)*n3+y^0-n3, oy^0'=-(-1+n58)*n3+y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+n58 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n58*n3+2*n58
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nalEMd.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n3, sy^0'=y^0-n3, oy^0'=y^0-n3, x^0'=-1+z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_OmAOHB.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, sy^0'=y^0, oy^0'=y^0, x^0'=-1+x^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
New rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n1, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n1, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, (-1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+n61 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_eeaKBB.txt

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+n61 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+n61 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n1, sy^0'=y^0-n1, oy^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n1, sy^0'=y^0-n1, oy^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n62-n62*n1, sy^0'=1-(-1+n62)*n1+y^0-n62-n1, oy^0'=1-(-1+n62)*n1+y^0-n62-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+n62 >= 0 /\ -1+z^0 >= 0), cost: 2*n62+2*n62*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pkaLMA.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n1, sy^0'=y^0-n1, oy^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_aacMaE.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : x^0'=0, (0 >= 0 /\ x^0 >= 0), cost: 2*x^0
New rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=0, z^0 >= 0, cost: 2+2*z^0

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=0, z^0 >= 0, cost: 2+2*z^0
New rule:
l4 -> [7] : (z^0 >= 0 /\ -2+n63 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_IbdncC.txt

Applied chaining
First rule:
l4 -> l4 : x^0'=0, (0 >= 0 /\ x^0 >= 0), cost: 2*x^0
Second rule:
l4 -> [7] : (z^0 >= 0 /\ -2+n63 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 >= 0 /\ z^0 >= 0 /\ -2+n63 >= 0 /\ x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : x^0'=0, (0 >= 0 /\ x^0 >= 0), cost: 2*x^0
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=0, ox^0'=0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, x^0 >= 0, cost: 2+2*x^0

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=0, ox^0'=0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, x^0 >= 0, cost: 2+2*x^0
New rule:
l4 -> l4 : sx^0'=0, ox^0'=0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n64+y^0, sy^0'=1-n64+y^0, oy^0'=1-n64+y^0, x^0'=z^0, (z^0 >= 0 /\ -1+n64 >= 0 /\ x^0 >= 0), cost: 2*n64+2*n64*z^0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_adnKaG.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=0, ox^0'=0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, x^0 >= 0, cost: 2+2*x^0
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ x^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mLenAJ.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n3, sy^0'=y^0-n3, oy^0'=y^0, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n3, sy^0'=y^0-n3, oy^0'=y^0, x^0'=z^0, (-1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n65 >= 0 /\ -2+n3 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kBJdNp.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n65 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n65 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n3, sy^0'=y^0-n3, oy^0'=y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n3, sy^0'=y^0-n3, oy^0'=y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-n66+y^0-n66*n3, sy^0'=1-n66+y^0-(-1+n66)*n3-n3, oy^0'=1-n66+y^0-(-1+n66)*n3-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -1+n66 >= 0), cost: 2*n66+2*n66*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ohiAIa.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=z^0, ox^0'=z^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0-n3, sy^0'=y^0-n3, oy^0'=y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nBlFEd.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=1, sz^0'=z^0, sy^0'=y^0, x^0'=0, (0 >= 0 /\ -1+x^0 >= 0), cost: 2*x^0
New rule:
l4 -> l4 : sx^0'=1, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=y^0, x^0'=0, -1+z^0 >= 0, cost: 2+2*z^0

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=1, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=-1+y^0, oy^0'=y^0, x^0'=0, -1+z^0 >= 0, cost: 2+2*z^0
New rule:
l4 -> [7] : (-2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mLoMfm.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=1, sz^0'=z^0, sy^0'=y^0, x^0'=0, (0 >= 0 /\ -1+x^0 >= 0), cost: 2*x^0
Second rule:
l4 -> [7] : (-2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 >= 0 /\ -1+x^0 >= 0 /\ -2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : sx^0'=1, sz^0'=z^0, sy^0'=y^0, x^0'=0, (0 >= 0 /\ -1+x^0 >= 0), cost: 2*x^0
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l4 -> l4 : sx^0'=0, ox^0'=0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2+2*x^0

Applied acceleration
Original rule:
l4 -> l4 : sx^0'=0, ox^0'=0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2+2*x^0
New rule:
l4 -> l4 : sx^0'=0, ox^0'=0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=y^0-n68, sy^0'=1+y^0-n68, oy^0'=1+y^0-n68, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n68 >= 0 /\ -1+z^0 >= 0), cost: 2*z^0*n68+2*n68
Sub-proof via acceration calculus written to file:///tmp/tmpnam_EHKFBf.txt

Applied nonterm
Original rule:
l4 -> l4 : sx^0'=0, ox^0'=0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2+2*x^0
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nDDgGD.txt

Applied chaining
First rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (0 <= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> l4 : x^0'=0, (0 >= 0 /\ x^0 >= 0), cost: 2*x^0
New rule:
l4 -> l4 : x^0'=0, x^0 >= 0, cost: 2*x^0

Applied simplification
Original rule:
l4 -> l4 : sx^0'=1, sz^0'=z^0, sy^0'=y^0, x^0'=0, (0 >= 0 /\ -1+x^0 >= 0), cost: 2*x^0
New rule:
l4 -> l4 : sx^0'=1, sz^0'=z^0, sy^0'=y^0, x^0'=0, -1+x^0 >= 0, cost: 2*x^0

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+n1 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+n1 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 >= 0 /\ z^0 >= 0 /\ -2+n63 >= 0 /\ x^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (z^0 >= 0 /\ -2+n63 >= 0 /\ x^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : z^0 >= 0, cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 <= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [7] : (0 >= 0 /\ -1+x^0 >= 0 /\ -2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 20 21 22 24

Accelerated simple loops
Start location: l6
  19: l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
  23: l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
  25: l4 -> [7] : -2+n >= 0, cost: NONTERM
  26: l4 -> [7] : -1+n0 >= 0, cost: NONTERM
  27: l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
  28: l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
  30: l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
  32: l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
  39: l4 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
  40: l4 -> [7] : -2+n29 >= 0, cost: NONTERM
  41: l4 -> [7] : (-1+z^0 >= 0 /\ -2+n30 >= 0), cost: NONTERM
  42: l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n30 >= 0), cost: NONTERM
  43: l4 -> [7] : (-2+n31 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  44: l4 -> [7] : (-1+x^0 >= 0 /\ -2+n31 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  45: l4 -> [7] : (-1+z^0 >= 0 /\ -2+n32 >= 0), cost: NONTERM
  46: l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n32 >= 0), cost: NONTERM
  47: l4 -> [7] : (-2+n33 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  48: l4 -> [7] : (-1+x^0 >= 0 /\ -2+n33 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  49: l4 -> [7] : -1+n34 >= 0, cost: NONTERM
  62: l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+n61 >= 0), cost: NONTERM
  63: l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+n61 >= 0), cost: NONTERM
  65: l4 -> [7] : (z^0 >= 0 /\ -2+n63 >= 0), cost: NONTERM
  67: l4 -> [7] : (-z^0+x^0 <= 0 /\ x^0 >= 0), cost: NONTERM
  69: l4 -> [7] : (-1+z^0 >= 0 /\ -2+n65 >= 0 /\ -2+n3 >= 0), cost: NONTERM
  70: l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n65 >= 0 /\ -2+n3 >= 0), cost: NONTERM
  72: l4 -> [7] : (-2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  74: l4 -> l4 : x^0'=0, x^0 >= 0, cost: 2*x^0
  75: l4 -> l4 : sx^0'=1, sz^0'=z^0, sy^0'=y^0, x^0'=0, -1+x^0 >= 0, cost: 2*x^0
  76: l4 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM
  77: l4 -> [7] : -1+z^0 >= 0, cost: NONTERM
  78: l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  79: l4 -> [7] : (-1+n1 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
  80: l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0), cost: NONTERM
  81: l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
  82: l4 -> [7] : (-2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
  83: l4 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
  84: l4 -> [7] : (-1+x^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
  85: l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
  86: l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  87: l4 -> [7] : (-1+x^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
  88: l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
  89: l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  90: l4 -> [7] : (z^0 >= 0 /\ -2+n63 >= 0 /\ x^0 >= 0), cost: NONTERM
  91: l4 -> [7] : z^0 >= 0, cost: NONTERM
  92: l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
  93: l4 -> [7] : (-1+x^0 >= 0 /\ -2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
  18: l6 -> l4 : c^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 2
New rule:
l6 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 4

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=x^0, sz^0'=z^0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 2
New rule:
l6 -> l4 : sx^0'=x^0, sz^0'=z^0, c^0'=0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : -2+n >= 0, cost: NONTERM
New rule:
l6 -> [7] : TRUE, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : -1+n0 >= 0, cost: NONTERM
New rule:
l6 -> [7] : TRUE, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> l4 : y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2*n1
New rule:
l6 -> l4 : c^0'=0, y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=z^0, sz^0'=z^0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2*n3
New rule:
l6 -> l4 : sx^0'=z^0, sz^0'=z^0, c^0'=0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : -2+n29 >= 0, cost: NONTERM
New rule:
l6 -> [7] : TRUE, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n30 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n30 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-2+n31 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n31 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n32 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n32 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-2+n33 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n33 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : -1+n34 >= 0, cost: NONTERM
New rule:
l6 -> [7] : TRUE, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+n61 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0 /\ -2+n61 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (z^0 >= 0 /\ -2+n63 >= 0), cost: NONTERM
New rule:
l6 -> [7] : z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-z^0+x^0 <= 0 /\ x^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-z^0+x^0 <= 0 /\ x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n65 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n65 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> l4 : x^0'=0, x^0 >= 0, cost: 2*x^0
New rule:
l6 -> l4 : c^0'=0, x^0'=0, x^0 >= 0, cost: 2+2*x^0

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> l4 : sx^0'=1, sz^0'=z^0, sy^0'=y^0, x^0'=0, -1+x^0 >= 0, cost: 2*x^0
New rule:
l6 -> l4 : sx^0'=1, sz^0'=z^0, c^0'=0, sy^0'=y^0, x^0'=0, -1+x^0 >= 0, cost: 2+2*x^0

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : -1+z^0 >= 0, cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+n1 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -2+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-2+n3 >= 0 /\ -z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n3 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n3 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+n1 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (z^0 >= 0 /\ -2+n63 >= 0 /\ x^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (z^0 >= 0 /\ x^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : z^0 >= 0, cost: NONTERM
New rule:
l6 -> [7] : z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+z^0 >= 0 /\ -2+n3 >= 0), cost: NONTERM
New rule:
l6 -> [7] : -1+z^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l6 -> l4 : c^0'=0, TRUE, cost: 2
Second rule:
l4 -> [7] : (-1+x^0 >= 0 /\ -2+n67 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
New rule:
l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 19 23 25 26 27 28 30 32 39 40 41 42 43 44 45 46 47 48 49 62 63 65 67 69 70 72 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93

Chained accelerated rules with incoming rules
Start location: l6
  18: l6 -> l4 : c^0'=0, TRUE, cost: 2
  94: l6 -> l4 : sx^0'=x^0, ox^0'=x^0, sz^0'=z^0, oz^0'=z^0, c^0'=1, y^0'=-1+y^0, sy^0'=y^0, oy^0'=y^0, x^0'=z^0, TRUE, cost: 4
  95: l6 -> l4 : sx^0'=x^0, sz^0'=z^0, c^0'=0, y^0'=-1+y^0, sy^0'=y^0, x^0'=z^0, -1+x^0 >= 0, cost: 4
  96: l6 -> [7] : TRUE, cost: NONTERM
  97: l6 -> l4 : c^0'=0, y^0'=y^0-n1, x^0'=z^0, (-1+x^0 >= 0 /\ -1+n1 >= 0 /\ -1+z^0 >= 0), cost: 2+2*n1
  98: l6 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
  99: l6 -> l4 : sx^0'=z^0, sz^0'=z^0, c^0'=0, y^0'=y^0-n3, sy^0'=1+y^0-n3, x^0'=z^0, (-1+x^0 >= 0 /\ -1+z^0 >= 0 /\ -2+n3 >= 0), cost: 2+2*n3
 100: l6 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
 101: l6 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
 102: l6 -> [7] : -1+z^0 >= 0, cost: NONTERM
 103: l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
 104: l6 -> [7] : z^0 >= 0, cost: NONTERM
 105: l6 -> [7] : (-z^0+x^0 <= 0 /\ x^0 >= 0), cost: NONTERM
 106: l6 -> l4 : c^0'=0, x^0'=0, x^0 >= 0, cost: 2+2*x^0
 107: l6 -> l4 : sx^0'=1, sz^0'=z^0, c^0'=0, sy^0'=y^0, x^0'=0, -1+x^0 >= 0, cost: 2+2*x^0
 108: l6 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM
 109: l6 -> [7] : (z^0 >= 0 /\ x^0 >= 0), cost: NONTERM


Removed unreachable locations and irrelevant leafs
Start location: l6
  96: l6 -> [7] : TRUE, cost: NONTERM
  98: l6 -> [7] : (-1+x^0 >= 0 /\ -z^0+x^0 <= 0), cost: NONTERM
 100: l6 -> [7] : (-z^0+x^0 <= 0 /\ -2+x^0 >= 0), cost: NONTERM
 101: l6 -> [7] : (-1+x^0 >= 0 /\ 1-z^0+x^0 <= 0), cost: NONTERM
 102: l6 -> [7] : -1+z^0 >= 0, cost: NONTERM
 103: l6 -> [7] : (-1+x^0 >= 0 /\ -1+z^0 >= 0), cost: NONTERM
 104: l6 -> [7] : z^0 >= 0, cost: NONTERM
 105: l6 -> [7] : (-z^0+x^0 <= 0 /\ x^0 >= 0), cost: NONTERM
 108: l6 -> [7] : (-1+x^0 >= 0 /\ -2+z^0 >= 0), cost: NONTERM
 109: l6 -> [7] : (z^0 >= 0 /\ x^0 >= 0), cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 96 via SMT.

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

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  TRUE