NO

Initial ITS
Start location: l4
   0: l0 -> l1 : n^0'=n^post0, __const_10^0'=__const_10^post0, e^0'=e^post0, __const_100^0'=__const_100^post0, __const_11^0'=__const_11^post0, (-__const_11^post0+__const_11^0 == 0 /\ 1-e^0 <= 0 /\ __const_100^0-__const_100^post0 == 0 /\ -__const_10^post0+__const_10^0 == 0 /\ -1-e^0+e^post0 == 0 /\ n^0-__const_100^0 <= 0 /\ -n^0-__const_11^0+n^post0 == 0), cost: 1
   2: l0 -> l2 : n^0'=n^post2, __const_10^0'=__const_10^post2, e^0'=e^post2, __const_100^0'=__const_100^post2, __const_11^0'=__const_11^post2, (-__const_10^post2+__const_10^0 == 0 /\ -__const_11^post2+__const_11^0 == 0 /\ 1-e^0 <= 0 /\ __const_100^0-__const_100^post2 == 0 /\ 1-e^0+e^post2 == 0 /\ -n^0+__const_10^0+n^post2 == 0 /\ 1-n^0+__const_100^0 <= 0), cost: 1
   1: l1 -> l0 : n^0'=n^post1, __const_10^0'=__const_10^post1, e^0'=e^post1, __const_100^0'=__const_100^post1, __const_11^0'=__const_11^post1, (-__const_100^post1+__const_100^0 == 0 /\ -e^post1+e^0 == 0 /\ -__const_11^post1+__const_11^0 == 0 /\ __const_10^0-__const_10^post1 == 0 /\ n^0-n^post1 == 0), cost: 1
   3: l2 -> l0 : n^0'=n^post3, __const_10^0'=__const_10^post3, e^0'=e^post3, __const_100^0'=__const_100^post3, __const_11^0'=__const_11^post3, (n^0-n^post3 == 0 /\ -__const_11^post3+__const_11^0 == 0 /\ __const_10^0-__const_10^post3 == 0 /\ e^0-e^post3 == 0 /\ -__const_100^post3+__const_100^0 == 0), cost: 1
   4: l3 -> l0 : n^0'=n^post4, __const_10^0'=__const_10^post4, e^0'=e^post4, __const_100^0'=__const_100^post4, __const_11^0'=__const_11^post4, (0 == 0 /\ __const_100^0-__const_100^post4 == 0 /\ -__const_11^post4+__const_11^0 == 0 /\ __const_10^0-__const_10^post4 == 0 /\ -1+e^post4 == 0), cost: 1
   5: l4 -> l3 : n^0'=n^post5, __const_10^0'=__const_10^post5, e^0'=e^post5, __const_100^0'=__const_100^post5, __const_11^0'=__const_11^post5, (__const_11^0-__const_11^post5 == 0 /\ n^0-n^post5 == 0 /\ -e^post5+e^0 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ __const_10^0-__const_10^post5 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : n^0'=n^post0, __const_10^0'=__const_10^post0, e^0'=e^post0, __const_100^0'=__const_100^post0, __const_11^0'=__const_11^post0, (-__const_11^post0+__const_11^0 == 0 /\ 1-e^0 <= 0 /\ __const_100^0-__const_100^post0 == 0 /\ -__const_10^post0+__const_10^0 == 0 /\ -1-e^0+e^post0 == 0 /\ n^0-__const_100^0 <= 0 /\ -n^0-__const_11^0+n^post0 == 0), cost: 1
New rule:
l0 -> l1 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 1

Applied preprocessing
Original rule:
l1 -> l0 : n^0'=n^post1, __const_10^0'=__const_10^post1, e^0'=e^post1, __const_100^0'=__const_100^post1, __const_11^0'=__const_11^post1, (-__const_100^post1+__const_100^0 == 0 /\ -e^post1+e^0 == 0 /\ -__const_11^post1+__const_11^0 == 0 /\ __const_10^0-__const_10^post1 == 0 /\ n^0-n^post1 == 0), cost: 1
New rule:
l1 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : n^0'=n^post2, __const_10^0'=__const_10^post2, e^0'=e^post2, __const_100^0'=__const_100^post2, __const_11^0'=__const_11^post2, (-__const_10^post2+__const_10^0 == 0 /\ -__const_11^post2+__const_11^0 == 0 /\ 1-e^0 <= 0 /\ __const_100^0-__const_100^post2 == 0 /\ 1-e^0+e^post2 == 0 /\ -n^0+__const_10^0+n^post2 == 0 /\ 1-n^0+__const_100^0 <= 0), cost: 1
New rule:
l0 -> l2 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : n^0'=n^post3, __const_10^0'=__const_10^post3, e^0'=e^post3, __const_100^0'=__const_100^post3, __const_11^0'=__const_11^post3, (n^0-n^post3 == 0 /\ -__const_11^post3+__const_11^0 == 0 /\ __const_10^0-__const_10^post3 == 0 /\ e^0-e^post3 == 0 /\ -__const_100^post3+__const_100^0 == 0), cost: 1
New rule:
l2 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l0 : n^0'=n^post4, __const_10^0'=__const_10^post4, e^0'=e^post4, __const_100^0'=__const_100^post4, __const_11^0'=__const_11^post4, (0 == 0 /\ __const_100^0-__const_100^post4 == 0 /\ -__const_11^post4+__const_11^0 == 0 /\ __const_10^0-__const_10^post4 == 0 /\ -1+e^post4 == 0), cost: 1
New rule:
l3 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l3 : n^0'=n^post5, __const_10^0'=__const_10^post5, e^0'=e^post5, __const_100^0'=__const_100^post5, __const_11^0'=__const_11^post5, (__const_11^0-__const_11^post5 == 0 /\ n^0-n^post5 == 0 /\ -e^post5+e^0 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ __const_10^0-__const_10^post5 == 0), cost: 1
New rule:
l4 -> l3 : TRUE, cost: 1

Simplified rules
Start location: l4
   6: l0 -> l1 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 1
   8: l0 -> l2 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 1
   7: l1 -> l0 : TRUE, cost: 1
   9: l2 -> l0 : TRUE, cost: 1
  10: l3 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 1
  11: l4 -> l3 : TRUE, cost: 1


Eliminating location l3 by chaining:

Applied chaining
First rule:
l4 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 1
New rule:
l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2

Applied deletion
Removed the following rules: 10 11

Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 1
Second rule:
l1 -> l0 : TRUE, cost: 1
New rule:
l0 -> l0 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 2

Applied deletion
Removed the following rules: 6 7

Eliminating location l2 by chaining:

Applied chaining
First rule:
l0 -> l2 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 1
Second rule:
l2 -> l0 : TRUE, cost: 1
New rule:
l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2

Applied deletion
Removed the following rules: 8 9

Eliminated locations on linear paths
Start location: l4
  13: l0 -> l0 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 2
  14: l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2
  12: l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2


Applied acceleration
Original rule:
l0 -> l0 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 2
New rule:
l0 -> l0 : n^0'=n^0+n*__const_11^0, e^0'=n+e^0, (n >= 0 /\ -1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_loHcJi.txt

Applied nonterm
Original rule:
l0 -> l0 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 2
New rule:
l0 -> [5] : (-1+e^0 >= 0 /\ __const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_lFFPCo.txt

Applied acceleration
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2
New rule:
l0 -> l0 : n^0'=n^0-__const_10^0*n0, e^0'=e^0-n0, (e^0-n0 >= 0 /\ -1+n^0-__const_10^0*(-1+n0)-__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ n0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_hMnIpP.txt

Applied instantiation
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0*n0, e^0'=e^0-n0, (e^0-n0 >= 0 /\ -1+n^0-__const_10^0*(-1+n0)-__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ n0 >= 0), cost: 2*n0
New rule:
l0 -> l0 : n^0'=n^0-__const_10^0*e^0, e^0'=0, (0 >= 0 /\ e^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -1+n^0-__const_100^0-(-1+e^0)*__const_10^0 >= 0), cost: 2*e^0

Applied chaining
First rule:
l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2
Second rule:
l0 -> l0 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 2
New rule:
l0 -> l0 : n^0'=n^0-__const_10^0+__const_11^0, (n^0-__const_10^0-__const_100^0 <= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 4

Applied acceleration
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0+__const_11^0, (n^0-__const_10^0-__const_100^0 <= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 4
New rule:
l0 -> l0 : n^0'=n^0+n1*__const_11^0-n1*__const_10^0, (-1+n^0+(-1+n1)*__const_11^0-__const_100^0-__const_10^0*(-1+n1) >= 0 /\ n1 >= 0 /\ -n^0-(-1+n1)*__const_11^0+__const_10^0+__const_100^0+__const_10^0*(-1+n1) >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -2+e^0 >= 0), cost: 4*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_JhCJPD.txt

Applied nonterm
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0+__const_11^0, (n^0-__const_10^0-__const_100^0 <= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 4
New rule:
l0 -> [5] : (-1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ -__const_10^0+__const_11^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_LempFP.txt

Applied chaining
First rule:
l0 -> l0 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 2
Second rule:
l0 -> [5] : (-1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ -__const_10^0+__const_11^0 <= 0), cost: NONTERM
New rule:
l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -n^0+__const_10^0+__const_100^0-__const_11^0 >= 0 /\ n^0-__const_100^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : n^0'=n^0+__const_11^0, e^0'=1+e^0, (-1+e^0 >= 0 /\ n^0-__const_100^0 <= 0), cost: 2
Second rule:
l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2
New rule:
l0 -> l0 : n^0'=n^0-__const_10^0+__const_11^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0-__const_11^0 <= 0 /\ n^0-__const_100^0 <= 0), cost: 4

Applied acceleration
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0+__const_11^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0-__const_11^0 <= 0 /\ n^0-__const_100^0 <= 0), cost: 4
New rule:
l0 -> l0 : n^0'=-__const_10^0*n2+n^0+n2*__const_11^0, (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ n2 >= 0 /\ -n^0+__const_10^0*(-1+n2)+__const_100^0-(-1+n2)*__const_11^0 >= 0 /\ -1+n^0-__const_10^0*(-1+n2)-__const_100^0+__const_11^0+(-1+n2)*__const_11^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: 4*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PCCKgB.txt

Applied nonterm
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0+__const_11^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0-__const_11^0 <= 0 /\ n^0-__const_100^0 <= 0), cost: 4
New rule:
l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ngoIpI.txt

Applied chaining
First rule:
l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2
Second rule:
l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
New rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_10^0-__const_100^0+__const_11^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ -__const_10^0+__const_11^0 <= 0 /\ 1-n^0+__const_100^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2
Second rule:
l0 -> l0 : n^0'=n^0+n*__const_11^0, e^0'=n+e^0, (n >= 0 /\ -1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: 2*n
New rule:
l0 -> l0 : n^0'=n^0-__const_10^0+n*__const_11^0, e^0'=-1+n+e^0, (n >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2+2*n

Applied acceleration
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0+n*__const_11^0, e^0'=-1+n+e^0, (n >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2+2*n
New rule:
l0 -> l0 : n^0'=n^0+n*n3*__const_11^0-__const_10^0*n3, e^0'=n*n3+e^0-n3, (n >= 0 /\ -1+n*(-1+n3)+e^0-n3 >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0+__const_10^0*(-1+n3)-n*(-1+n3)*__const_11^0 >= 0 /\ n3 >= 0 /\ -1+n^0-__const_100^0-__const_10^0*(-1+n3)+n*(-1+n3)*__const_11^0 >= 0 /\ -2+e^0 >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0+__const_10^0*(-1+n3)-n*(-1+n3)*__const_11^0 >= 0), cost: 2*n*n3+2*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_jGAoCc.txt

Applied instantiation
Original rule:
l0 -> l0 : n^0'=n^0+n*n3*__const_11^0-__const_10^0*n3, e^0'=n*n3+e^0-n3, (n >= 0 /\ -1+n*(-1+n3)+e^0-n3 >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0+__const_10^0*(-1+n3)-n*(-1+n3)*__const_11^0 >= 0 /\ n3 >= 0 /\ -1+n^0-__const_100^0-__const_10^0*(-1+n3)+n*(-1+n3)*__const_11^0 >= 0 /\ -2+e^0 >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0+__const_10^0*(-1+n3)-n*(-1+n3)*__const_11^0 >= 0), cost: 2*n*n3+2*n3
New rule:
l0 -> l0 : n^0'=n^0-(-1+e^0)*__const_10^0, e^0'=1, (0 >= 0 /\ -n^0+__const_10^0*(-2+e^0)+__const_10^0+__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ -1+n^0-__const_10^0*(-2+e^0)-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0+__const_11^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -n^0+__const_10^0*(-2+e^0)+__const_10^0+__const_100^0 >= 0 /\ -2+e^0 >= 0), cost: -2+2*e^0

Applied nonterm
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0+n*__const_11^0, e^0'=-1+n+e^0, (n >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2+2*n
New rule:
l0 -> [5] : (n >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ 1-n <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_OOkKeJ.txt

Applied chaining
First rule:
l0 -> l0 : n^0'=n^0+n*__const_11^0, e^0'=n+e^0, (n >= 0 /\ -1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: 2*n
Second rule:
l0 -> [5] : (n >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ 1-n <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0), cost: NONTERM
New rule:
l0 -> [5] : (n >= 0 /\ -1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0-n*__const_11^0 >= 0 /\ 1-n <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_10^0+__const_100^0-n*__const_11^0 >= 0 /\ -2+n+e^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : n^0'=n^0+n*__const_11^0, e^0'=n+e^0, (n >= 0 /\ -1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: 2*n
Second rule:
l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2
New rule:
l0 -> l0 : n^0'=n^0-__const_10^0+n*__const_11^0, e^0'=-1+n+e^0, (-1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ 1-n^0+__const_100^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: 2+2*n

Applied acceleration
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0+n*__const_11^0, e^0'=-1+n+e^0, (-1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ 1-n^0+__const_100^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: 2+2*n
New rule:
l0 -> l0 : n^0'=n^0+n*n4*__const_11^0-__const_10^0*n4, e^0'=n*n4+e^0-n4, (-1+n^0-__const_100^0+n*(-1+n4)*__const_11^0-__const_10^0*(-1+n4)+n*__const_11^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0-n*(-1+n4)*__const_11^0+__const_10^0*(-1+n4) >= 0 /\ -1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ n4 >= 0 /\ -n^0+__const_100^0-n*(-1+n4)*__const_11^0+__const_10^0*(-1+n4) >= 0 /\ -n^0+__const_100^0 >= 0), cost: 2*n*n4+2*n4
Sub-proof via acceration calculus written to file:///tmp/tmpnam_AmBDeI.txt

Applied nonterm
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0+n*__const_11^0, e^0'=-1+n+e^0, (-1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ 1-n^0+__const_100^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: 2+2*n
New rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_lOPGan.txt

Applied chaining
First rule:
l0 -> l0 : n^0'=n^0-__const_10^0, e^0'=-1+e^0, (-1+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: 2
Second rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
New rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_10^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> l0 : n^0'=n^0-__const_10^0*e^0, e^0'=0, (0 >= 0 /\ e^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -1+n^0-__const_100^0-(-1+e^0)*__const_10^0 >= 0), cost: 2*e^0
New rule:
l0 -> l0 : n^0'=n^0-__const_10^0*e^0, e^0'=0, (e^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -1+n^0-__const_100^0-(-1+e^0)*__const_10^0 >= 0), cost: 2*e^0

Applied simplification
Original rule:
l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -n^0+__const_10^0+__const_100^0-__const_11^0 >= 0 /\ n^0-__const_100^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0), cost: NONTERM
New rule:
l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ n^0-__const_100^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_10^0-__const_100^0+__const_11^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ -__const_10^0+__const_11^0 <= 0 /\ 1-n^0+__const_100^0 <= 0), cost: NONTERM
New rule:
l0 -> [5] : (-n^0+__const_10^0+__const_100^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ -__const_10^0+__const_11^0 <= 0 /\ 1-n^0+__const_100^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [5] : (n >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ 1-n <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0), cost: NONTERM
New rule:
l0 -> [5] : (-n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ -1+n >= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [5] : (n >= 0 /\ -1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0-n*__const_11^0 >= 0 /\ 1-n <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_10^0+__const_100^0-n*__const_11^0 >= 0 /\ -2+n+e^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
New rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0-n*__const_11^0 >= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_10^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: NONTERM
New rule:
l0 -> [5] : (-n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: NONTERM

Applied deletion
Removed the following rules: 13 14

Accelerated simple loops
Start location: l4
  15: l0 -> l0 : n^0'=n^0+n*__const_11^0, e^0'=n+e^0, (n >= 0 /\ -1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: 2*n
  16: l0 -> [5] : (-1+e^0 >= 0 /\ __const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
  18: l0 -> [5] : (-1+n^0-__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ -__const_10^0+__const_11^0 <= 0), cost: NONTERM
  20: l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
  24: l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
  26: l0 -> l0 : n^0'=n^0-__const_10^0*e^0, e^0'=0, (e^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -1+n^0-__const_100^0-(-1+e^0)*__const_10^0 >= 0), cost: 2*e^0
  27: l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ n^0-__const_100^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0), cost: NONTERM
  28: l0 -> [5] : (-n^0+__const_10^0+__const_100^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ -__const_10^0+__const_11^0 <= 0 /\ 1-n^0+__const_100^0 <= 0), cost: NONTERM
  29: l0 -> [5] : (-n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ -1+n >= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0), cost: NONTERM
  30: l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0-n*__const_11^0 >= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
  31: l0 -> [5] : (-n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_10^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -2+e^0 >= 0 /\ 1-n^0+__const_100^0 <= 0), cost: NONTERM
  12: l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2


Applied chaining
First rule:
l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2
Second rule:
l0 -> l0 : n^0'=n^0+n*__const_11^0, e^0'=n+e^0, (n >= 0 /\ -1+e^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -n^0+__const_100^0 >= 0), cost: 2*n
New rule:
l4 -> l0 : n^0'=n^post4+n*__const_11^0, e^0'=1+n, (n >= 0 /\ __const_100^0-n^post4 >= 0 /\ -(-1+n)*__const_11^0+__const_100^0-n^post4 >= 0), cost: 2+2*n

Applied chaining
First rule:
l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2
Second rule:
l0 -> [5] : (-1+e^0 >= 0 /\ __const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
New rule:
l4 -> [5] : __const_11^0 <= 0, cost: NONTERM

Applied chaining
First rule:
l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2
Second rule:
l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
New rule:
l4 -> [5] : (-1+__const_11^0 >= 0 /\ __const_10^0-__const_11^0 == 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2
Second rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -n^0-(-1+n)*__const_11^0+__const_100^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
New rule:
l4 -> [5] : (-1+n*__const_11^0 >= 0 /\ 1+(-1+n)*__const_11^0-n*__const_11^0 <= 0 /\ -__const_10^0+n*__const_11^0 == 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2
Second rule:
l0 -> l0 : n^0'=n^0-__const_10^0*e^0, e^0'=0, (e^0 >= 0 /\ -1+n^0-__const_100^0 >= 0 /\ -1+n^0-__const_100^0-(-1+e^0)*__const_10^0 >= 0), cost: 2*e^0
New rule:
l4 -> l0 : n^0'=-__const_10^0+n^post4, e^0'=0, -1-__const_100^0+n^post4 >= 0, cost: 4

Applied chaining
First rule:
l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2
Second rule:
l0 -> [5] : (-1+n^0-__const_100^0+__const_11^0 >= 0 /\ -1+e^0 >= 0 /\ __const_10^0-__const_11^0 <= 0 /\ n^0-__const_100^0 <= 0 /\ -__const_10^0+__const_11^0 <= 0), cost: NONTERM
New rule:
l4 -> [5] : (-1+__const_11^0 >= 0 /\ __const_10^0-__const_11^0 == 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2
Second rule:
l0 -> [5] : (-1+e^0 >= 0 /\ -1+n^0-__const_100^0+n*__const_11^0 >= 0 /\ -__const_10^0+n*__const_11^0 <= 0 /\ -n^0+__const_10^0-(-1+n)*__const_11^0+__const_100^0-n*__const_11^0 >= 0 /\ __const_10^0-n*__const_11^0 <= 0 /\ -n^0+__const_100^0 >= 0), cost: NONTERM
New rule:
l4 -> [5] : (-1+n*__const_11^0 >= 0 /\ 1-__const_10^0+(-1+n)*__const_11^0 <= 0 /\ -__const_10^0+n*__const_11^0 == 0), cost: NONTERM

Applied deletion
Removed the following rules: 15 16 18 20 24 26 27 28 29 30 31

Chained accelerated rules with incoming rules
Start location: l4
  12: l4 -> l0 : n^0'=n^post4, e^0'=1, 0 == 0, cost: 2
  32: l4 -> l0 : n^0'=n^post4+n*__const_11^0, e^0'=1+n, (n >= 0 /\ __const_100^0-n^post4 >= 0 /\ -(-1+n)*__const_11^0+__const_100^0-n^post4 >= 0), cost: 2+2*n
  33: l4 -> [5] : __const_11^0 <= 0, cost: NONTERM
  34: l4 -> [5] : (-1+__const_11^0 >= 0 /\ __const_10^0-__const_11^0 == 0), cost: NONTERM
  35: l4 -> [5] : (-1+n*__const_11^0 >= 0 /\ 1+(-1+n)*__const_11^0-n*__const_11^0 <= 0 /\ -__const_10^0+n*__const_11^0 == 0), cost: NONTERM
  36: l4 -> l0 : n^0'=-__const_10^0+n^post4, e^0'=0, -1-__const_100^0+n^post4 >= 0, cost: 4
  37: l4 -> [5] : (-1+n*__const_11^0 >= 0 /\ 1-__const_10^0+(-1+n)*__const_11^0 <= 0 /\ -__const_10^0+n*__const_11^0 == 0), cost: NONTERM


Removed unreachable locations and irrelevant leafs
Start location: l4
  33: l4 -> [5] : __const_11^0 <= 0, cost: NONTERM
  34: l4 -> [5] : (-1+__const_11^0 >= 0 /\ __const_10^0-__const_11^0 == 0), cost: NONTERM
  35: l4 -> [5] : (-1+n*__const_11^0 >= 0 /\ 1+(-1+n)*__const_11^0-n*__const_11^0 <= 0 /\ -__const_10^0+n*__const_11^0 == 0), cost: NONTERM
  37: l4 -> [5] : (-1+n*__const_11^0 >= 0 /\ 1-__const_10^0+(-1+n)*__const_11^0 <= 0 /\ -__const_10^0+n*__const_11^0 == 0), cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 33 via SMT.

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

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  __const_11^0 <= 0