WORST_CASE(Omega(0),?)

Initial ITS
Start location: l6
   0: l0 -> l1 : res10^0'=res10^post0, nX4^0'=nX4^post0, tmp^0'=tmp^post0, ret_nBC18^0'=ret_nBC18^post0, nX^0'=nX^post0, nI6^0'=nI6^post0, tmp7^0'=tmp7^post0, res5^0'=res5^post0, nX9^0'=nX9^post0, tmp___0^0'=tmp___0^post0, ret_nBC211^0'=ret_nBC211^post0, (-tmp___0^post0+tmp___0^0 == 0 /\ -ret_nBC18^post0+ret_nBC18^0 == 0 /\ nX4^0-nX4^post0 == 0 /\ -tmp7^post0+tmp7^0 == 0 /\ -ret_nBC211^post0+ret_nBC211^0 == 0 /\ -nX9^post0+nX9^0 == 0 /\ -1-nI6^0+nI6^post0 == 0 /\ res10^0-res10^post0 == 0 /\ tmp^0-tmp^post0 == 0 /\ res5^post0-tmp7^0-res5^0 == 0 /\ nX^0-nX^post0 == 0), cost: 1
   5: l1 -> l3 : res10^0'=res10^post5, nX4^0'=nX4^post5, tmp^0'=tmp^post5, ret_nBC18^0'=ret_nBC18^post5, nX^0'=nX^post5, nI6^0'=nI6^post5, tmp7^0'=tmp7^post5, res5^0'=res5^post5, nX9^0'=nX9^post5, tmp___0^0'=tmp___0^post5, ret_nBC211^0'=ret_nBC211^post5, (nX^0-nX^post5 == 0 /\ res10^0-res10^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ tmp7^0-tmp7^post5 == 0 /\ -res5^post5+res5^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -nX9^post5+nX9^0 == 0 /\ -ret_nBC211^post5+ret_nBC211^0 == 0 /\ nX4^0-nX4^post5 == 0 /\ -nI6^post5+nI6^0 == 0 /\ ret_nBC18^0-ret_nBC18^post5 == 0), cost: 1
   1: l2 -> l0 : res10^0'=res10^post1, nX4^0'=nX4^post1, tmp^0'=tmp^post1, ret_nBC18^0'=ret_nBC18^post1, nX^0'=nX^post1, nI6^0'=nI6^post1, tmp7^0'=tmp7^post1, res5^0'=res5^post1, nX9^0'=nX9^post1, tmp___0^0'=tmp___0^post1, ret_nBC211^0'=ret_nBC211^post1, (res10^0-res10^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ -nX^post1+nX^0 == 0 /\ -nX9^post1+nX9^0 == 0 /\ ret_nBC18^0-ret_nBC18^post1 == 0 /\ tmp7^post1 == 0 /\ -nI6^post1+nI6^0 == 0 /\ nX4^0-nX4^post1 == 0 /\ res5^0-res5^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -ret_nBC211^post1+ret_nBC211^0 == 0), cost: 1
   2: l2 -> l0 : res10^0'=res10^post2, nX4^0'=nX4^post2, tmp^0'=tmp^post2, ret_nBC18^0'=ret_nBC18^post2, nX^0'=nX^post2, nI6^0'=nI6^post2, tmp7^0'=tmp7^post2, res5^0'=res5^post2, nX9^0'=nX9^post2, tmp___0^0'=tmp___0^post2, ret_nBC211^0'=ret_nBC211^post2, (nX^0-nX^post2 == 0 /\ -nI6^post2+nI6^0 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -1+tmp7^post2 == 0 /\ -ret_nBC211^post2+ret_nBC211^0 == 0 /\ -res5^post2+res5^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ nX4^0-nX4^post2 == 0 /\ res10^0-res10^post2 == 0 /\ -nX9^post2+nX9^0 == 0 /\ ret_nBC18^0-ret_nBC18^post2 == 0), cost: 1
   3: l3 -> l4 : res10^0'=res10^post3, nX4^0'=nX4^post3, tmp^0'=tmp^post3, ret_nBC18^0'=ret_nBC18^post3, nX^0'=nX^post3, nI6^0'=nI6^post3, tmp7^0'=tmp7^post3, res5^0'=res5^post3, nX9^0'=nX9^post3, tmp___0^0'=tmp___0^post3, ret_nBC211^0'=ret_nBC211^post3, (0 == 0 /\ nX4^0-nX4^post3 == 0 /\ tmp___0^post3-ret_nBC211^post3 == 0 /\ -tmp7^post3+tmp7^0 == 0 /\ -res10^post3+ret_nBC211^post3 == 0 /\ -nX^0+nX9^post3 == 0 /\ res10^10-nX9^post3 == 0 /\ -res5^0+ret_nBC18^post3 == 0 /\ res5^0-res5^post3 == 0 /\ nX^0-nX^post3 == 0 /\ 16-nI6^0 <= 0 /\ tmp^post3-ret_nBC18^post3 == 0 /\ -nI6^post3+nI6^0 == 0), cost: 1
   4: l3 -> l2 : res10^0'=res10^post4, nX4^0'=nX4^post4, tmp^0'=tmp^post4, ret_nBC18^0'=ret_nBC18^post4, nX^0'=nX^post4, nI6^0'=nI6^post4, tmp7^0'=tmp7^post4, res5^0'=res5^post4, nX9^0'=nX9^post4, tmp___0^0'=tmp___0^post4, ret_nBC211^0'=ret_nBC211^post4, (res10^0-res10^post4 == 0 /\ -15+nI6^0 <= 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -ret_nBC211^post4+ret_nBC211^0 == 0 /\ -nX^post4+nX^0 == 0 /\ -tmp7^post4+tmp7^0 == 0 /\ res5^0-res5^post4 == 0 /\ -nX9^post4+nX9^0 == 0 /\ nX4^0-nX4^post4 == 0 /\ -nI6^post4+nI6^0 == 0 /\ ret_nBC18^0-ret_nBC18^post4 == 0), cost: 1
   6: l5 -> l1 : res10^0'=res10^post6, nX4^0'=nX4^post6, tmp^0'=tmp^post6, ret_nBC18^0'=ret_nBC18^post6, nX^0'=nX^post6, nI6^0'=nI6^post6, tmp7^0'=tmp7^post6, res5^0'=res5^post6, nX9^0'=nX9^post6, tmp___0^0'=tmp___0^post6, ret_nBC211^0'=ret_nBC211^post6, (tmp^0-tmp^post6 == 0 /\ -nX9^post6+nX9^0 == 0 /\ -nX^0+nX4^post6 == 0 /\ res5^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ res10^0-res10^post6 == 0 /\ -ret_nBC211^post6+ret_nBC211^0 == 0 /\ -ret_nBC18^post6+ret_nBC18^0 == 0 /\ nX^0-nX^post6 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ nI6^post6 == 0), cost: 1
   7: l6 -> l5 : res10^0'=res10^post7, nX4^0'=nX4^post7, tmp^0'=tmp^post7, ret_nBC18^0'=ret_nBC18^post7, nX^0'=nX^post7, nI6^0'=nI6^post7, tmp7^0'=tmp7^post7, res5^0'=res5^post7, nX9^0'=nX9^post7, tmp___0^0'=tmp___0^post7, ret_nBC211^0'=ret_nBC211^post7, (-tmp7^post7+tmp7^0 == 0 /\ ret_nBC18^0-ret_nBC18^post7 == 0 /\ res10^0-res10^post7 == 0 /\ -ret_nBC211^post7+ret_nBC211^0 == 0 /\ nX4^0-nX4^post7 == 0 /\ res5^0-res5^post7 == 0 /\ -nX^post7+nX^0 == 0 /\ -nI6^post7+nI6^0 == 0 /\ -nX9^post7+nX9^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ tmp^0-tmp^post7 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l6
   0: l0 -> l1 : res10^0'=res10^post0, nX4^0'=nX4^post0, tmp^0'=tmp^post0, ret_nBC18^0'=ret_nBC18^post0, nX^0'=nX^post0, nI6^0'=nI6^post0, tmp7^0'=tmp7^post0, res5^0'=res5^post0, nX9^0'=nX9^post0, tmp___0^0'=tmp___0^post0, ret_nBC211^0'=ret_nBC211^post0, (-tmp___0^post0+tmp___0^0 == 0 /\ -ret_nBC18^post0+ret_nBC18^0 == 0 /\ nX4^0-nX4^post0 == 0 /\ -tmp7^post0+tmp7^0 == 0 /\ -ret_nBC211^post0+ret_nBC211^0 == 0 /\ -nX9^post0+nX9^0 == 0 /\ -1-nI6^0+nI6^post0 == 0 /\ res10^0-res10^post0 == 0 /\ tmp^0-tmp^post0 == 0 /\ res5^post0-tmp7^0-res5^0 == 0 /\ nX^0-nX^post0 == 0), cost: 1
   5: l1 -> l3 : res10^0'=res10^post5, nX4^0'=nX4^post5, tmp^0'=tmp^post5, ret_nBC18^0'=ret_nBC18^post5, nX^0'=nX^post5, nI6^0'=nI6^post5, tmp7^0'=tmp7^post5, res5^0'=res5^post5, nX9^0'=nX9^post5, tmp___0^0'=tmp___0^post5, ret_nBC211^0'=ret_nBC211^post5, (nX^0-nX^post5 == 0 /\ res10^0-res10^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ tmp7^0-tmp7^post5 == 0 /\ -res5^post5+res5^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -nX9^post5+nX9^0 == 0 /\ -ret_nBC211^post5+ret_nBC211^0 == 0 /\ nX4^0-nX4^post5 == 0 /\ -nI6^post5+nI6^0 == 0 /\ ret_nBC18^0-ret_nBC18^post5 == 0), cost: 1
   1: l2 -> l0 : res10^0'=res10^post1, nX4^0'=nX4^post1, tmp^0'=tmp^post1, ret_nBC18^0'=ret_nBC18^post1, nX^0'=nX^post1, nI6^0'=nI6^post1, tmp7^0'=tmp7^post1, res5^0'=res5^post1, nX9^0'=nX9^post1, tmp___0^0'=tmp___0^post1, ret_nBC211^0'=ret_nBC211^post1, (res10^0-res10^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ -nX^post1+nX^0 == 0 /\ -nX9^post1+nX9^0 == 0 /\ ret_nBC18^0-ret_nBC18^post1 == 0 /\ tmp7^post1 == 0 /\ -nI6^post1+nI6^0 == 0 /\ nX4^0-nX4^post1 == 0 /\ res5^0-res5^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -ret_nBC211^post1+ret_nBC211^0 == 0), cost: 1
   2: l2 -> l0 : res10^0'=res10^post2, nX4^0'=nX4^post2, tmp^0'=tmp^post2, ret_nBC18^0'=ret_nBC18^post2, nX^0'=nX^post2, nI6^0'=nI6^post2, tmp7^0'=tmp7^post2, res5^0'=res5^post2, nX9^0'=nX9^post2, tmp___0^0'=tmp___0^post2, ret_nBC211^0'=ret_nBC211^post2, (nX^0-nX^post2 == 0 /\ -nI6^post2+nI6^0 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -1+tmp7^post2 == 0 /\ -ret_nBC211^post2+ret_nBC211^0 == 0 /\ -res5^post2+res5^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ nX4^0-nX4^post2 == 0 /\ res10^0-res10^post2 == 0 /\ -nX9^post2+nX9^0 == 0 /\ ret_nBC18^0-ret_nBC18^post2 == 0), cost: 1
   4: l3 -> l2 : res10^0'=res10^post4, nX4^0'=nX4^post4, tmp^0'=tmp^post4, ret_nBC18^0'=ret_nBC18^post4, nX^0'=nX^post4, nI6^0'=nI6^post4, tmp7^0'=tmp7^post4, res5^0'=res5^post4, nX9^0'=nX9^post4, tmp___0^0'=tmp___0^post4, ret_nBC211^0'=ret_nBC211^post4, (res10^0-res10^post4 == 0 /\ -15+nI6^0 <= 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -ret_nBC211^post4+ret_nBC211^0 == 0 /\ -nX^post4+nX^0 == 0 /\ -tmp7^post4+tmp7^0 == 0 /\ res5^0-res5^post4 == 0 /\ -nX9^post4+nX9^0 == 0 /\ nX4^0-nX4^post4 == 0 /\ -nI6^post4+nI6^0 == 0 /\ ret_nBC18^0-ret_nBC18^post4 == 0), cost: 1
   6: l5 -> l1 : res10^0'=res10^post6, nX4^0'=nX4^post6, tmp^0'=tmp^post6, ret_nBC18^0'=ret_nBC18^post6, nX^0'=nX^post6, nI6^0'=nI6^post6, tmp7^0'=tmp7^post6, res5^0'=res5^post6, nX9^0'=nX9^post6, tmp___0^0'=tmp___0^post6, ret_nBC211^0'=ret_nBC211^post6, (tmp^0-tmp^post6 == 0 /\ -nX9^post6+nX9^0 == 0 /\ -nX^0+nX4^post6 == 0 /\ res5^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ res10^0-res10^post6 == 0 /\ -ret_nBC211^post6+ret_nBC211^0 == 0 /\ -ret_nBC18^post6+ret_nBC18^0 == 0 /\ nX^0-nX^post6 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ nI6^post6 == 0), cost: 1
   7: l6 -> l5 : res10^0'=res10^post7, nX4^0'=nX4^post7, tmp^0'=tmp^post7, ret_nBC18^0'=ret_nBC18^post7, nX^0'=nX^post7, nI6^0'=nI6^post7, tmp7^0'=tmp7^post7, res5^0'=res5^post7, nX9^0'=nX9^post7, tmp___0^0'=tmp___0^post7, ret_nBC211^0'=ret_nBC211^post7, (-tmp7^post7+tmp7^0 == 0 /\ ret_nBC18^0-ret_nBC18^post7 == 0 /\ res10^0-res10^post7 == 0 /\ -ret_nBC211^post7+ret_nBC211^0 == 0 /\ nX4^0-nX4^post7 == 0 /\ res5^0-res5^post7 == 0 /\ -nX^post7+nX^0 == 0 /\ -nI6^post7+nI6^0 == 0 /\ -nX9^post7+nX9^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ tmp^0-tmp^post7 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : res10^0'=res10^post0, nX4^0'=nX4^post0, tmp^0'=tmp^post0, ret_nBC18^0'=ret_nBC18^post0, nX^0'=nX^post0, nI6^0'=nI6^post0, tmp7^0'=tmp7^post0, res5^0'=res5^post0, nX9^0'=nX9^post0, tmp___0^0'=tmp___0^post0, ret_nBC211^0'=ret_nBC211^post0, (-tmp___0^post0+tmp___0^0 == 0 /\ -ret_nBC18^post0+ret_nBC18^0 == 0 /\ nX4^0-nX4^post0 == 0 /\ -tmp7^post0+tmp7^0 == 0 /\ -ret_nBC211^post0+ret_nBC211^0 == 0 /\ -nX9^post0+nX9^0 == 0 /\ -1-nI6^0+nI6^post0 == 0 /\ res10^0-res10^post0 == 0 /\ tmp^0-tmp^post0 == 0 /\ res5^post0-tmp7^0-res5^0 == 0 /\ nX^0-nX^post0 == 0), cost: 1
New rule:
l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : res10^0'=res10^post1, nX4^0'=nX4^post1, tmp^0'=tmp^post1, ret_nBC18^0'=ret_nBC18^post1, nX^0'=nX^post1, nI6^0'=nI6^post1, tmp7^0'=tmp7^post1, res5^0'=res5^post1, nX9^0'=nX9^post1, tmp___0^0'=tmp___0^post1, ret_nBC211^0'=ret_nBC211^post1, (res10^0-res10^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ -nX^post1+nX^0 == 0 /\ -nX9^post1+nX9^0 == 0 /\ ret_nBC18^0-ret_nBC18^post1 == 0 /\ tmp7^post1 == 0 /\ -nI6^post1+nI6^0 == 0 /\ nX4^0-nX4^post1 == 0 /\ res5^0-res5^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -ret_nBC211^post1+ret_nBC211^0 == 0), cost: 1
New rule:
l2 -> l0 : tmp7^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : res10^0'=res10^post2, nX4^0'=nX4^post2, tmp^0'=tmp^post2, ret_nBC18^0'=ret_nBC18^post2, nX^0'=nX^post2, nI6^0'=nI6^post2, tmp7^0'=tmp7^post2, res5^0'=res5^post2, nX9^0'=nX9^post2, tmp___0^0'=tmp___0^post2, ret_nBC211^0'=ret_nBC211^post2, (nX^0-nX^post2 == 0 /\ -nI6^post2+nI6^0 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -1+tmp7^post2 == 0 /\ -ret_nBC211^post2+ret_nBC211^0 == 0 /\ -res5^post2+res5^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ nX4^0-nX4^post2 == 0 /\ res10^0-res10^post2 == 0 /\ -nX9^post2+nX9^0 == 0 /\ ret_nBC18^0-ret_nBC18^post2 == 0), cost: 1
New rule:
l2 -> l0 : tmp7^0'=1, TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l2 : res10^0'=res10^post4, nX4^0'=nX4^post4, tmp^0'=tmp^post4, ret_nBC18^0'=ret_nBC18^post4, nX^0'=nX^post4, nI6^0'=nI6^post4, tmp7^0'=tmp7^post4, res5^0'=res5^post4, nX9^0'=nX9^post4, tmp___0^0'=tmp___0^post4, ret_nBC211^0'=ret_nBC211^post4, (res10^0-res10^post4 == 0 /\ -15+nI6^0 <= 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -ret_nBC211^post4+ret_nBC211^0 == 0 /\ -nX^post4+nX^0 == 0 /\ -tmp7^post4+tmp7^0 == 0 /\ res5^0-res5^post4 == 0 /\ -nX9^post4+nX9^0 == 0 /\ nX4^0-nX4^post4 == 0 /\ -nI6^post4+nI6^0 == 0 /\ ret_nBC18^0-ret_nBC18^post4 == 0), cost: 1
New rule:
l3 -> l2 : -15+nI6^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l3 : res10^0'=res10^post5, nX4^0'=nX4^post5, tmp^0'=tmp^post5, ret_nBC18^0'=ret_nBC18^post5, nX^0'=nX^post5, nI6^0'=nI6^post5, tmp7^0'=tmp7^post5, res5^0'=res5^post5, nX9^0'=nX9^post5, tmp___0^0'=tmp___0^post5, ret_nBC211^0'=ret_nBC211^post5, (nX^0-nX^post5 == 0 /\ res10^0-res10^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ tmp7^0-tmp7^post5 == 0 /\ -res5^post5+res5^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -nX9^post5+nX9^0 == 0 /\ -ret_nBC211^post5+ret_nBC211^0 == 0 /\ nX4^0-nX4^post5 == 0 /\ -nI6^post5+nI6^0 == 0 /\ ret_nBC18^0-ret_nBC18^post5 == 0), cost: 1
New rule:
l1 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l1 : res10^0'=res10^post6, nX4^0'=nX4^post6, tmp^0'=tmp^post6, ret_nBC18^0'=ret_nBC18^post6, nX^0'=nX^post6, nI6^0'=nI6^post6, tmp7^0'=tmp7^post6, res5^0'=res5^post6, nX9^0'=nX9^post6, tmp___0^0'=tmp___0^post6, ret_nBC211^0'=ret_nBC211^post6, (tmp^0-tmp^post6 == 0 /\ -nX9^post6+nX9^0 == 0 /\ -nX^0+nX4^post6 == 0 /\ res5^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ res10^0-res10^post6 == 0 /\ -ret_nBC211^post6+ret_nBC211^0 == 0 /\ -ret_nBC18^post6+ret_nBC18^0 == 0 /\ nX^0-nX^post6 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ nI6^post6 == 0), cost: 1
New rule:
l5 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : res10^0'=res10^post7, nX4^0'=nX4^post7, tmp^0'=tmp^post7, ret_nBC18^0'=ret_nBC18^post7, nX^0'=nX^post7, nI6^0'=nI6^post7, tmp7^0'=tmp7^post7, res5^0'=res5^post7, nX9^0'=nX9^post7, tmp___0^0'=tmp___0^post7, ret_nBC211^0'=ret_nBC211^post7, (-tmp7^post7+tmp7^0 == 0 /\ ret_nBC18^0-ret_nBC18^post7 == 0 /\ res10^0-res10^post7 == 0 /\ -ret_nBC211^post7+ret_nBC211^0 == 0 /\ nX4^0-nX4^post7 == 0 /\ res5^0-res5^post7 == 0 /\ -nX^post7+nX^0 == 0 /\ -nI6^post7+nI6^0 == 0 /\ -nX9^post7+nX9^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ tmp^0-tmp^post7 == 0), cost: 1
New rule:
l6 -> l5 : TRUE, cost: 1

Simplified rules
Start location: l6
   8: l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
  12: l1 -> l3 : TRUE, cost: 1
   9: l2 -> l0 : tmp7^0'=0, TRUE, cost: 1
  10: l2 -> l0 : tmp7^0'=1, TRUE, cost: 1
  11: l3 -> l2 : -15+nI6^0 <= 0, cost: 1
  13: l5 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 1
  14: l6 -> l5 : TRUE, cost: 1


Eliminating location l5 by chaining:

Applied chaining
First rule:
l6 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 1
New rule:
l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2

Applied deletion
Removed the following rules: 13 14

Eliminating location l3 by chaining:

Applied chaining
First rule:
l1 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l2 : -15+nI6^0 <= 0, cost: 1
New rule:
l1 -> l2 : -15+nI6^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 11 12

Eliminated locations on linear paths
Start location: l6
   8: l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
  16: l1 -> l2 : -15+nI6^0 <= 0, cost: 2
   9: l2 -> l0 : tmp7^0'=0, TRUE, cost: 1
  10: l2 -> l0 : tmp7^0'=1, TRUE, cost: 1
  15: l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2


Eliminating location l2 by chaining:

Applied chaining
First rule:
l1 -> l2 : -15+nI6^0 <= 0, cost: 2
Second rule:
l2 -> l0 : tmp7^0'=0, TRUE, cost: 1
New rule:
l1 -> l0 : tmp7^0'=0, -15+nI6^0 <= 0, cost: 3

Applied chaining
First rule:
l1 -> l2 : -15+nI6^0 <= 0, cost: 2
Second rule:
l2 -> l0 : tmp7^0'=1, TRUE, cost: 1
New rule:
l1 -> l0 : tmp7^0'=1, -15+nI6^0 <= 0, cost: 3

Applied deletion
Removed the following rules: 9 10 16

Eliminated locations on tree-shaped paths
Start location: l6
   8: l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
  17: l1 -> l0 : tmp7^0'=0, -15+nI6^0 <= 0, cost: 3
  18: l1 -> l0 : tmp7^0'=1, -15+nI6^0 <= 0, cost: 3
  15: l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2


Eliminating location l0 by chaining:

Applied chaining
First rule:
l1 -> l0 : tmp7^0'=0, -15+nI6^0 <= 0, cost: 3
Second rule:
l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
New rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, res5^0'=res5^0, -15+nI6^0 <= 0, cost: 4

Applied chaining
First rule:
l1 -> l0 : tmp7^0'=1, -15+nI6^0 <= 0, cost: 3
Second rule:
l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
New rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=1, res5^0'=1+res5^0, -15+nI6^0 <= 0, cost: 4

Applied deletion
Removed the following rules: 8 17 18

Eliminated locations on tree-shaped paths
Start location: l6
  19: l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, res5^0'=res5^0, -15+nI6^0 <= 0, cost: 4
  20: l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=1, res5^0'=1+res5^0, -15+nI6^0 <= 0, cost: 4
  15: l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2


Applied simplification
Original rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, res5^0'=res5^0, -15+nI6^0 <= 0, cost: 4
New rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, -15+nI6^0 <= 0, cost: 4

Simplified simple loops
Start location: l6
  20: l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=1, res5^0'=1+res5^0, -15+nI6^0 <= 0, cost: 4
  21: l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, -15+nI6^0 <= 0, cost: 4
  15: l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=1, res5^0'=1+res5^0, -15+nI6^0 <= 0, cost: 4
New rule:
l1 -> l1 : nI6^0'=n+nI6^0, tmp7^0'=1, res5^0'=n+res5^0, (16-n-nI6^0 >= 0 /\ -1+n >= 0), cost: 4*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mchkem.txt

Applied instantiation
Original rule:
l1 -> l1 : nI6^0'=n+nI6^0, tmp7^0'=1, res5^0'=n+res5^0, (16-n-nI6^0 >= 0 /\ -1+n >= 0), cost: 4*n
New rule:
l1 -> l1 : nI6^0'=16, tmp7^0'=1, res5^0'=16-nI6^0+res5^0, (0 >= 0 /\ 15-nI6^0 >= 0), cost: 64-4*nI6^0

Applied acceleration
Original rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, -15+nI6^0 <= 0, cost: 4
New rule:
l1 -> l1 : nI6^0'=nI6^0+n0, tmp7^0'=0, (-1+n0 >= 0 /\ 16-nI6^0-n0 >= 0), cost: 4*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ioBhLA.txt

Applied instantiation
Original rule:
l1 -> l1 : nI6^0'=nI6^0+n0, tmp7^0'=0, (-1+n0 >= 0 /\ 16-nI6^0-n0 >= 0), cost: 4*n0
New rule:
l1 -> l1 : nI6^0'=16, tmp7^0'=0, (0 >= 0 /\ 15-nI6^0 >= 0), cost: 64-4*nI6^0

Applied simplification
Original rule:
l1 -> l1 : nI6^0'=16, tmp7^0'=1, res5^0'=16-nI6^0+res5^0, (0 >= 0 /\ 15-nI6^0 >= 0), cost: 64-4*nI6^0
New rule:
l1 -> l1 : nI6^0'=16, tmp7^0'=1, res5^0'=16-nI6^0+res5^0, -15+nI6^0 <= 0, cost: 64-4*nI6^0

Applied simplification
Original rule:
l1 -> l1 : nI6^0'=16, tmp7^0'=0, (0 >= 0 /\ 15-nI6^0 >= 0), cost: 64-4*nI6^0
New rule:
l1 -> l1 : nI6^0'=16, tmp7^0'=0, -15+nI6^0 <= 0, cost: 64-4*nI6^0

Applied deletion
Removed the following rules: 20 21

Accelerated simple loops
Start location: l6
  24: l1 -> l1 : nI6^0'=16, tmp7^0'=1, res5^0'=16-nI6^0+res5^0, -15+nI6^0 <= 0, cost: 64-4*nI6^0
  25: l1 -> l1 : nI6^0'=16, tmp7^0'=0, -15+nI6^0 <= 0, cost: 64-4*nI6^0
  15: l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2
Second rule:
l1 -> l1 : nI6^0'=16, tmp7^0'=1, res5^0'=16-nI6^0+res5^0, -15+nI6^0 <= 0, cost: 64-4*nI6^0
New rule:
l6 -> l1 : nX4^0'=nX^0, nI6^0'=16, tmp7^0'=1, res5^0'=16, -15 <= 0, cost: 66

Applied chaining
First rule:
l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2
Second rule:
l1 -> l1 : nI6^0'=16, tmp7^0'=0, -15+nI6^0 <= 0, cost: 64-4*nI6^0
New rule:
l6 -> l1 : nX4^0'=nX^0, nI6^0'=16, tmp7^0'=0, res5^0'=0, -15 <= 0, cost: 66

Applied deletion
Removed the following rules: 24 25

Chained accelerated rules with incoming rules
Start location: l6
  15: l6 -> l1 : nX4^0'=nX^0, nI6^0'=0, res5^0'=0, TRUE, cost: 2
  26: l6 -> l1 : nX4^0'=nX^0, nI6^0'=16, tmp7^0'=1, res5^0'=16, -15 <= 0, cost: 66
  27: l6 -> l1 : nX4^0'=nX^0, nI6^0'=16, tmp7^0'=0, res5^0'=0, -15 <= 0, cost: 66


Removed unreachable locations and irrelevant leafs
Start location: l6
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0