WORST_CASE(Omega(0),?)

Initial ITS
Start location: l8
   0: l0 -> l1 : na^0'=na^post0, ret_nPow17^0'=ret_nPow17^post0, np9^0'=np9^post0, nPow___010^0'=nPow___010^post0, nx18^0'=nx18^post0, ni21^0'=ni21^post0, tmp^0'=tmp^post0, nc^0'=nc^post0, nPow___020^0'=nPow___020^post0, ret_nPow12^0'=ret_nPow12^post0, np19^0'=np19^post0, tmp___1^0'=tmp___1^post0, nN^0'=nN^post0, ni16^0'=ni16^post0, nb^0'=nb^post0, ret_nPow22^0'=ret_nPow22^post0, nx13^0'=nx13^post0, nPow___015^0'=nPow___015^post0, nx8^0'=nx8^post0, np14^0'=np14^post0, tmp___0^0'=tmp___0^post0, ni11^0'=ni11^post0, (tmp^0-tmp^post0 == 0 /\ nPow___010^0-nPow___010^post0 == 0 /\ -np19^post0+np19^0 == 0 /\ -ni11^post0+ni11^0 == 0 /\ np9^0-np9^post0 == 0 /\ np14^0-np14^post0 == 0 /\ -tmp___0^post0+tmp___0^0 == 0 /\ -ni16^post0+ni16^0 == 0 /\ -nc^post0+nc^0 == 0 /\ -nb^post0+nb^0 == 0 /\ nx8^0-nx8^post0 == 0 /\ nN^0-nN^post0 == 0 /\ ni21^0-ni21^post0 == 0 /\ nx13^0-nx13^post0 == 0 /\ -ret_nPow22^post0+ret_nPow22^0 == 0 /\ na^0-na^post0 == 0 /\ -nPow___015^post0+nPow___015^0 == 0 /\ nPow___020^0-nPow___020^post0 == 0 /\ ret_nPow12^0-ret_nPow12^post0 == 0 /\ -ret_nPow17^post0+ret_nPow17^0 == 0 /\ -tmp___1^post0+tmp___1^0 == 0 /\ nx18^0-nx18^post0 == 0), cost: 1
   7: l1 -> l5 : na^0'=na^post7, ret_nPow17^0'=ret_nPow17^post7, np9^0'=np9^post7, nPow___010^0'=nPow___010^post7, nx18^0'=nx18^post7, ni21^0'=ni21^post7, tmp^0'=tmp^post7, nc^0'=nc^post7, nPow___020^0'=nPow___020^post7, ret_nPow12^0'=ret_nPow12^post7, np19^0'=np19^post7, tmp___1^0'=tmp___1^post7, nN^0'=nN^post7, ni16^0'=ni16^post7, nb^0'=nb^post7, ret_nPow22^0'=ret_nPow22^post7, nx13^0'=nx13^post7, nPow___015^0'=nPow___015^post7, nx8^0'=nx8^post7, np14^0'=np14^post7, tmp___0^0'=tmp___0^post7, ni11^0'=ni11^post7, (-nN^post7+nN^0 == 0 /\ -ret_nPow22^post7+ret_nPow22^0 == 0 /\ np9^0-ni11^0 <= 0 /\ na^0-na^post7 == 0 /\ -ni11^post7+ni11^0 == 0 /\ nPow___010^0-nPow___010^post7 == 0 /\ -ret_nPow12^post7+tmp^post7 == 0 /\ tmp___1^0-tmp___1^post7 == 0 /\ np19^0-np19^post7 == 0 /\ -1+nPow___015^post7 == 0 /\ nx18^0-nx18^post7 == 0 /\ ni21^0-ni21^post7 == 0 /\ nx13^post7-nb^0 == 0 /\ np14^post7-nN^0 == 0 /\ ni16^post7 == 0 /\ nc^0-nc^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ nb^0-nb^post7 == 0 /\ nPow___020^0-nPow___020^post7 == 0 /\ -nx8^post7+nx8^0 == 0 /\ -np9^post7+np9^0 == 0 /\ ret_nPow17^0-ret_nPow17^post7 == 0 /\ -nPow___010^0+ret_nPow12^post7 == 0), cost: 1
   8: l1 -> l0 : na^0'=na^post8, ret_nPow17^0'=ret_nPow17^post8, np9^0'=np9^post8, nPow___010^0'=nPow___010^post8, nx18^0'=nx18^post8, ni21^0'=ni21^post8, tmp^0'=tmp^post8, nc^0'=nc^post8, nPow___020^0'=nPow___020^post8, ret_nPow12^0'=ret_nPow12^post8, np19^0'=np19^post8, tmp___1^0'=tmp___1^post8, nN^0'=nN^post8, ni16^0'=ni16^post8, nb^0'=nb^post8, ret_nPow22^0'=ret_nPow22^post8, nx13^0'=nx13^post8, nPow___015^0'=nPow___015^post8, nx8^0'=nx8^post8, np14^0'=np14^post8, tmp___0^0'=tmp___0^post8, ni11^0'=ni11^post8, (0 == 0 /\ -nx8^post8+nx8^0 == 0 /\ -ni16^post8+ni16^0 == 0 /\ tmp___1^0-tmp___1^post8 == 0 /\ np9^0-np9^post8 == 0 /\ nc^0-nc^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -nx13^post8+nx13^0 == 0 /\ -ret_nPow12^post8+ret_nPow12^0 == 0 /\ nb^0-nb^post8 == 0 /\ -np19^post8+np19^0 == 0 /\ 1-np9^0+ni11^0 <= 0 /\ nPow___020^0-nPow___020^post8 == 0 /\ ni21^0-ni21^post8 == 0 /\ -nN^post8+nN^0 == 0 /\ -ret_nPow22^post8+ret_nPow22^0 == 0 /\ -1+ni11^post8-ni11^0 == 0 /\ na^0-na^post8 == 0 /\ ret_nPow17^0-ret_nPow17^post8 == 0 /\ -nPow___015^post8+nPow___015^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -np14^post8+np14^0 == 0 /\ nx18^0-nx18^post8 == 0), cost: 1
   1: l2 -> l3 : na^0'=na^post1, ret_nPow17^0'=ret_nPow17^post1, np9^0'=np9^post1, nPow___010^0'=nPow___010^post1, nx18^0'=nx18^post1, ni21^0'=ni21^post1, tmp^0'=tmp^post1, nc^0'=nc^post1, nPow___020^0'=nPow___020^post1, ret_nPow12^0'=ret_nPow12^post1, np19^0'=np19^post1, tmp___1^0'=tmp___1^post1, nN^0'=nN^post1, ni16^0'=ni16^post1, nb^0'=nb^post1, ret_nPow22^0'=ret_nPow22^post1, nx13^0'=nx13^post1, nPow___015^0'=nPow___015^post1, nx8^0'=nx8^post1, np14^0'=np14^post1, tmp___0^0'=tmp___0^post1, ni11^0'=ni11^post1, (ni16^0-ni16^post1 == 0 /\ -nb^post1+nb^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -nPow___020^post1+nPow___020^0 == 0 /\ -np14^post1+np14^0 == 0 /\ np19^0-np19^post1 == 0 /\ np9^0-np9^post1 == 0 /\ na^0-na^post1 == 0 /\ ret_nPow12^0-ret_nPow12^post1 == 0 /\ -nPow___015^post1+nPow___015^0 == 0 /\ -nx8^post1+nx8^0 == 0 /\ -nPow___020^0+ret_nPow22^post1 == 0 /\ -ni11^post1+ni11^0 == 0 /\ nPow___010^0-nPow___010^post1 == 0 /\ nx13^0-nx13^post1 == 0 /\ ret_nPow17^0-ret_nPow17^post1 == 0 /\ -nx18^post1+nx18^0 == 0 /\ tmp___1^post1-ret_nPow22^post1 == 0 /\ -nN^post1+nN^0 == 0 /\ -ni21^0+np19^0 <= 0 /\ nc^0-nc^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ -ni21^post1+ni21^0 == 0), cost: 1
   2: l2 -> l4 : na^0'=na^post2, ret_nPow17^0'=ret_nPow17^post2, np9^0'=np9^post2, nPow___010^0'=nPow___010^post2, nx18^0'=nx18^post2, ni21^0'=ni21^post2, tmp^0'=tmp^post2, nc^0'=nc^post2, nPow___020^0'=nPow___020^post2, ret_nPow12^0'=ret_nPow12^post2, np19^0'=np19^post2, tmp___1^0'=tmp___1^post2, nN^0'=nN^post2, ni16^0'=ni16^post2, nb^0'=nb^post2, ret_nPow22^0'=ret_nPow22^post2, nx13^0'=nx13^post2, nPow___015^0'=nPow___015^post2, nx8^0'=nx8^post2, np14^0'=np14^post2, tmp___0^0'=tmp___0^post2, ni11^0'=ni11^post2, (0 == 0 /\ -1-ni21^0+ni21^post2 == 0 /\ -ret_nPow22^post2+ret_nPow22^0 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ na^0-na^post2 == 0 /\ -ni11^post2+ni11^0 == 0 /\ nPow___010^0-nPow___010^post2 == 0 /\ -nx13^post2+nx13^0 == 0 /\ -nPow___015^post2+nPow___015^0 == 0 /\ np19^0-np19^post2 == 0 /\ nx18^0-nx18^post2 == 0 /\ 1+ni21^0-np19^0 <= 0 /\ -ret_nPow12^post2+ret_nPow12^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ nc^0-nc^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -nx8^post2+nx8^0 == 0 /\ nb^0-nb^post2 == 0 /\ -nN^post2+nN^0 == 0 /\ -ni16^post2+ni16^0 == 0 /\ -np9^post2+np9^0 == 0 /\ -np14^post2+np14^0 == 0 /\ ret_nPow17^0-ret_nPow17^post2 == 0), cost: 1
   6: l4 -> l2 : na^0'=na^post6, ret_nPow17^0'=ret_nPow17^post6, np9^0'=np9^post6, nPow___010^0'=nPow___010^post6, nx18^0'=nx18^post6, ni21^0'=ni21^post6, tmp^0'=tmp^post6, nc^0'=nc^post6, nPow___020^0'=nPow___020^post6, ret_nPow12^0'=ret_nPow12^post6, np19^0'=np19^post6, tmp___1^0'=tmp___1^post6, nN^0'=nN^post6, ni16^0'=ni16^post6, nb^0'=nb^post6, ret_nPow22^0'=ret_nPow22^post6, nx13^0'=nx13^post6, nPow___015^0'=nPow___015^post6, nx8^0'=nx8^post6, np14^0'=np14^post6, tmp___0^0'=tmp___0^post6, ni11^0'=ni11^post6, (nPow___015^0-nPow___015^post6 == 0 /\ -nx13^post6+nx13^0 == 0 /\ -np14^post6+np14^0 == 0 /\ np19^0-np19^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -nc^post6+nc^0 == 0 /\ -nPow___020^post6+nPow___020^0 == 0 /\ -ret_nPow22^post6+ret_nPow22^0 == 0 /\ -ret_nPow12^post6+ret_nPow12^0 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ ret_nPow17^0-ret_nPow17^post6 == 0 /\ na^0-na^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -nx8^post6+nx8^0 == 0 /\ ni16^0-ni16^post6 == 0 /\ np9^0-np9^post6 == 0 /\ -nx18^post6+nx18^0 == 0 /\ nb^0-nb^post6 == 0 /\ nPow___010^0-nPow___010^post6 == 0 /\ -ni11^post6+ni11^0 == 0 /\ -ni21^post6+ni21^0 == 0 /\ -nN^post6+nN^0 == 0), cost: 1
   3: l5 -> l6 : na^0'=na^post3, ret_nPow17^0'=ret_nPow17^post3, np9^0'=np9^post3, nPow___010^0'=nPow___010^post3, nx18^0'=nx18^post3, ni21^0'=ni21^post3, tmp^0'=tmp^post3, nc^0'=nc^post3, nPow___020^0'=nPow___020^post3, ret_nPow12^0'=ret_nPow12^post3, np19^0'=np19^post3, tmp___1^0'=tmp___1^post3, nN^0'=nN^post3, ni16^0'=ni16^post3, nb^0'=nb^post3, ret_nPow22^0'=ret_nPow22^post3, nx13^0'=nx13^post3, nPow___015^0'=nPow___015^post3, nx8^0'=nx8^post3, np14^0'=np14^post3, tmp___0^0'=tmp___0^post3, ni11^0'=ni11^post3, (-ni11^post3+ni11^0 == 0 /\ -ni16^post3+ni16^0 == 0 /\ nx18^0-nx18^post3 == 0 /\ ni21^0-ni21^post3 == 0 /\ nc^0-nc^post3 == 0 /\ ret_nPow17^0-ret_nPow17^post3 == 0 /\ na^0-na^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -np19^post3+np19^0 == 0 /\ nN^0-nN^post3 == 0 /\ nPow___020^0-nPow___020^post3 == 0 /\ -nb^post3+nb^0 == 0 /\ -nPow___010^post3+nPow___010^0 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ -nPow___015^post3+nPow___015^0 == 0 /\ ret_nPow22^0-ret_nPow22^post3 == 0 /\ ret_nPow12^0-ret_nPow12^post3 == 0 /\ np9^0-np9^post3 == 0 /\ -nx13^post3+nx13^0 == 0 /\ -np14^post3+np14^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -nx8^post3+nx8^0 == 0), cost: 1
   4: l6 -> l4 : na^0'=na^post4, ret_nPow17^0'=ret_nPow17^post4, np9^0'=np9^post4, nPow___010^0'=nPow___010^post4, nx18^0'=nx18^post4, ni21^0'=ni21^post4, tmp^0'=tmp^post4, nc^0'=nc^post4, nPow___020^0'=nPow___020^post4, ret_nPow12^0'=ret_nPow12^post4, np19^0'=np19^post4, tmp___1^0'=tmp___1^post4, nN^0'=nN^post4, ni16^0'=ni16^post4, nb^0'=nb^post4, ret_nPow22^0'=ret_nPow22^post4, nx13^0'=nx13^post4, nPow___015^0'=nPow___015^post4, nx8^0'=nx8^post4, np14^0'=np14^post4, tmp___0^0'=tmp___0^post4, ni11^0'=ni11^post4, (-ni16^0+np14^0 <= 0 /\ -np14^post4+np14^0 == 0 /\ -nx13^post4+nx13^0 == 0 /\ nN^0-nN^post4 == 0 /\ -nb^post4+nb^0 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ na^0-na^post4 == 0 /\ -nPow___015^post4+nPow___015^0 == 0 /\ -nx8^post4+nx8^0 == 0 /\ -nc^post4+nc^0 == 0 /\ ret_nPow22^0-ret_nPow22^post4 == 0 /\ ret_nPow17^post4-nPow___015^0 == 0 /\ -ni11^post4+ni11^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ nPow___010^0-nPow___010^post4 == 0 /\ ni21^post4 == 0 /\ np19^post4-nN^0 == 0 /\ -nc^0+nx18^post4 == 0 /\ ret_nPow12^0-ret_nPow12^post4 == 0 /\ -ret_nPow17^post4+tmp___0^post4 == 0 /\ np9^0-np9^post4 == 0 /\ -1+nPow___020^post4 == 0 /\ -ni16^post4+ni16^0 == 0), cost: 1
   5: l6 -> l5 : na^0'=na^post5, ret_nPow17^0'=ret_nPow17^post5, np9^0'=np9^post5, nPow___010^0'=nPow___010^post5, nx18^0'=nx18^post5, ni21^0'=ni21^post5, tmp^0'=tmp^post5, nc^0'=nc^post5, nPow___020^0'=nPow___020^post5, ret_nPow12^0'=ret_nPow12^post5, np19^0'=np19^post5, tmp___1^0'=tmp___1^post5, nN^0'=nN^post5, ni16^0'=ni16^post5, nb^0'=nb^post5, ret_nPow22^0'=ret_nPow22^post5, nx13^0'=nx13^post5, nPow___015^0'=nPow___015^post5, nx8^0'=nx8^post5, np14^0'=np14^post5, tmp___0^0'=tmp___0^post5, ni11^0'=ni11^post5, (0 == 0 /\ nPow___010^0-nPow___010^post5 == 0 /\ -nPow___020^post5+nPow___020^0 == 0 /\ np14^0-np14^post5 == 0 /\ np9^0-np9^post5 == 0 /\ -ni11^post5+ni11^0 == 0 /\ 1+ni16^0-np14^0 <= 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ -nb^post5+nb^0 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ ret_nPow12^0-ret_nPow12^post5 == 0 /\ nx8^0-nx8^post5 == 0 /\ -1-ni16^0+ni16^post5 == 0 /\ -ret_nPow22^post5+ret_nPow22^0 == 0 /\ nN^0-nN^post5 == 0 /\ ni21^0-ni21^post5 == 0 /\ np19^0-np19^post5 == 0 /\ nx18^0-nx18^post5 == 0 /\ na^0-na^post5 == 0 /\ -ret_nPow17^post5+ret_nPow17^0 == 0 /\ nx13^0-nx13^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ -nc^post5+nc^0 == 0), cost: 1
   9: l7 -> l0 : na^0'=na^post9, ret_nPow17^0'=ret_nPow17^post9, np9^0'=np9^post9, nPow___010^0'=nPow___010^post9, nx18^0'=nx18^post9, ni21^0'=ni21^post9, tmp^0'=tmp^post9, nc^0'=nc^post9, nPow___020^0'=nPow___020^post9, ret_nPow12^0'=ret_nPow12^post9, np19^0'=np19^post9, tmp___1^0'=tmp___1^post9, nN^0'=nN^post9, ni16^0'=ni16^post9, nb^0'=nb^post9, ret_nPow22^0'=ret_nPow22^post9, nx13^0'=nx13^post9, nPow___015^0'=nPow___015^post9, nx8^0'=nx8^post9, np14^0'=np14^post9, tmp___0^0'=tmp___0^post9, ni11^0'=ni11^post9, (-ni16^post9+ni16^0 == 0 /\ -nPow___015^post9+nPow___015^0 == 0 /\ -np14^post9+np14^0 == 0 /\ nc^0-nc^post9 == 0 /\ -nx13^post9+nx13^0 == 0 /\ -1+nPow___010^post9 == 0 /\ -nb^post9+nb^0 == 0 /\ ni21^0-ni21^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ nPow___020^0-nPow___020^post9 == 0 /\ ret_nPow22^0-ret_nPow22^post9 == 0 /\ tmp^0-tmp^post9 == 0 /\ na^0-na^post9 == 0 /\ ret_nPow17^0-ret_nPow17^post9 == 0 /\ nx18^0-nx18^post9 == 0 /\ np9^post9-nN^post9 == 0 /\ nx8^post9-na^0 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -3+nN^post9 == 0 /\ -np19^post9+np19^0 == 0 /\ ret_nPow12^0-ret_nPow12^post9 == 0 /\ ni11^post9 == 0), cost: 1
  10: l8 -> l7 : na^0'=na^post10, ret_nPow17^0'=ret_nPow17^post10, np9^0'=np9^post10, nPow___010^0'=nPow___010^post10, nx18^0'=nx18^post10, ni21^0'=ni21^post10, tmp^0'=tmp^post10, nc^0'=nc^post10, nPow___020^0'=nPow___020^post10, ret_nPow12^0'=ret_nPow12^post10, np19^0'=np19^post10, tmp___1^0'=tmp___1^post10, nN^0'=nN^post10, ni16^0'=ni16^post10, nb^0'=nb^post10, ret_nPow22^0'=ret_nPow22^post10, nx13^0'=nx13^post10, nPow___015^0'=nPow___015^post10, nx8^0'=nx8^post10, np14^0'=np14^post10, tmp___0^0'=tmp___0^post10, ni11^0'=ni11^post10, (tmp^0-tmp^post10 == 0 /\ nPow___010^0-nPow___010^post10 == 0 /\ -nx8^post10+nx8^0 == 0 /\ -ni11^post10+ni11^0 == 0 /\ ret_nPow17^0-ret_nPow17^post10 == 0 /\ np9^0-np9^post10 == 0 /\ -tmp___1^post10+tmp___1^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ -nb^post10+nb^0 == 0 /\ -ni16^post10+ni16^0 == 0 /\ -np14^post10+np14^0 == 0 /\ -ret_nPow22^post10+ret_nPow22^0 == 0 /\ np19^0-np19^post10 == 0 /\ ret_nPow12^0-ret_nPow12^post10 == 0 /\ nx18^0-nx18^post10 == 0 /\ nPow___020^0-nPow___020^post10 == 0 /\ ni21^0-ni21^post10 == 0 /\ -nPow___015^post10+nPow___015^0 == 0 /\ nN^0-nN^post10 == 0 /\ -nc^post10+nc^0 == 0 /\ na^0-na^post10 == 0 /\ -nx13^post10+nx13^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l8
   0: l0 -> l1 : na^0'=na^post0, ret_nPow17^0'=ret_nPow17^post0, np9^0'=np9^post0, nPow___010^0'=nPow___010^post0, nx18^0'=nx18^post0, ni21^0'=ni21^post0, tmp^0'=tmp^post0, nc^0'=nc^post0, nPow___020^0'=nPow___020^post0, ret_nPow12^0'=ret_nPow12^post0, np19^0'=np19^post0, tmp___1^0'=tmp___1^post0, nN^0'=nN^post0, ni16^0'=ni16^post0, nb^0'=nb^post0, ret_nPow22^0'=ret_nPow22^post0, nx13^0'=nx13^post0, nPow___015^0'=nPow___015^post0, nx8^0'=nx8^post0, np14^0'=np14^post0, tmp___0^0'=tmp___0^post0, ni11^0'=ni11^post0, (tmp^0-tmp^post0 == 0 /\ nPow___010^0-nPow___010^post0 == 0 /\ -np19^post0+np19^0 == 0 /\ -ni11^post0+ni11^0 == 0 /\ np9^0-np9^post0 == 0 /\ np14^0-np14^post0 == 0 /\ -tmp___0^post0+tmp___0^0 == 0 /\ -ni16^post0+ni16^0 == 0 /\ -nc^post0+nc^0 == 0 /\ -nb^post0+nb^0 == 0 /\ nx8^0-nx8^post0 == 0 /\ nN^0-nN^post0 == 0 /\ ni21^0-ni21^post0 == 0 /\ nx13^0-nx13^post0 == 0 /\ -ret_nPow22^post0+ret_nPow22^0 == 0 /\ na^0-na^post0 == 0 /\ -nPow___015^post0+nPow___015^0 == 0 /\ nPow___020^0-nPow___020^post0 == 0 /\ ret_nPow12^0-ret_nPow12^post0 == 0 /\ -ret_nPow17^post0+ret_nPow17^0 == 0 /\ -tmp___1^post0+tmp___1^0 == 0 /\ nx18^0-nx18^post0 == 0), cost: 1
   7: l1 -> l5 : na^0'=na^post7, ret_nPow17^0'=ret_nPow17^post7, np9^0'=np9^post7, nPow___010^0'=nPow___010^post7, nx18^0'=nx18^post7, ni21^0'=ni21^post7, tmp^0'=tmp^post7, nc^0'=nc^post7, nPow___020^0'=nPow___020^post7, ret_nPow12^0'=ret_nPow12^post7, np19^0'=np19^post7, tmp___1^0'=tmp___1^post7, nN^0'=nN^post7, ni16^0'=ni16^post7, nb^0'=nb^post7, ret_nPow22^0'=ret_nPow22^post7, nx13^0'=nx13^post7, nPow___015^0'=nPow___015^post7, nx8^0'=nx8^post7, np14^0'=np14^post7, tmp___0^0'=tmp___0^post7, ni11^0'=ni11^post7, (-nN^post7+nN^0 == 0 /\ -ret_nPow22^post7+ret_nPow22^0 == 0 /\ np9^0-ni11^0 <= 0 /\ na^0-na^post7 == 0 /\ -ni11^post7+ni11^0 == 0 /\ nPow___010^0-nPow___010^post7 == 0 /\ -ret_nPow12^post7+tmp^post7 == 0 /\ tmp___1^0-tmp___1^post7 == 0 /\ np19^0-np19^post7 == 0 /\ -1+nPow___015^post7 == 0 /\ nx18^0-nx18^post7 == 0 /\ ni21^0-ni21^post7 == 0 /\ nx13^post7-nb^0 == 0 /\ np14^post7-nN^0 == 0 /\ ni16^post7 == 0 /\ nc^0-nc^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ nb^0-nb^post7 == 0 /\ nPow___020^0-nPow___020^post7 == 0 /\ -nx8^post7+nx8^0 == 0 /\ -np9^post7+np9^0 == 0 /\ ret_nPow17^0-ret_nPow17^post7 == 0 /\ -nPow___010^0+ret_nPow12^post7 == 0), cost: 1
   8: l1 -> l0 : na^0'=na^post8, ret_nPow17^0'=ret_nPow17^post8, np9^0'=np9^post8, nPow___010^0'=nPow___010^post8, nx18^0'=nx18^post8, ni21^0'=ni21^post8, tmp^0'=tmp^post8, nc^0'=nc^post8, nPow___020^0'=nPow___020^post8, ret_nPow12^0'=ret_nPow12^post8, np19^0'=np19^post8, tmp___1^0'=tmp___1^post8, nN^0'=nN^post8, ni16^0'=ni16^post8, nb^0'=nb^post8, ret_nPow22^0'=ret_nPow22^post8, nx13^0'=nx13^post8, nPow___015^0'=nPow___015^post8, nx8^0'=nx8^post8, np14^0'=np14^post8, tmp___0^0'=tmp___0^post8, ni11^0'=ni11^post8, (0 == 0 /\ -nx8^post8+nx8^0 == 0 /\ -ni16^post8+ni16^0 == 0 /\ tmp___1^0-tmp___1^post8 == 0 /\ np9^0-np9^post8 == 0 /\ nc^0-nc^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -nx13^post8+nx13^0 == 0 /\ -ret_nPow12^post8+ret_nPow12^0 == 0 /\ nb^0-nb^post8 == 0 /\ -np19^post8+np19^0 == 0 /\ 1-np9^0+ni11^0 <= 0 /\ nPow___020^0-nPow___020^post8 == 0 /\ ni21^0-ni21^post8 == 0 /\ -nN^post8+nN^0 == 0 /\ -ret_nPow22^post8+ret_nPow22^0 == 0 /\ -1+ni11^post8-ni11^0 == 0 /\ na^0-na^post8 == 0 /\ ret_nPow17^0-ret_nPow17^post8 == 0 /\ -nPow___015^post8+nPow___015^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -np14^post8+np14^0 == 0 /\ nx18^0-nx18^post8 == 0), cost: 1
   2: l2 -> l4 : na^0'=na^post2, ret_nPow17^0'=ret_nPow17^post2, np9^0'=np9^post2, nPow___010^0'=nPow___010^post2, nx18^0'=nx18^post2, ni21^0'=ni21^post2, tmp^0'=tmp^post2, nc^0'=nc^post2, nPow___020^0'=nPow___020^post2, ret_nPow12^0'=ret_nPow12^post2, np19^0'=np19^post2, tmp___1^0'=tmp___1^post2, nN^0'=nN^post2, ni16^0'=ni16^post2, nb^0'=nb^post2, ret_nPow22^0'=ret_nPow22^post2, nx13^0'=nx13^post2, nPow___015^0'=nPow___015^post2, nx8^0'=nx8^post2, np14^0'=np14^post2, tmp___0^0'=tmp___0^post2, ni11^0'=ni11^post2, (0 == 0 /\ -1-ni21^0+ni21^post2 == 0 /\ -ret_nPow22^post2+ret_nPow22^0 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ na^0-na^post2 == 0 /\ -ni11^post2+ni11^0 == 0 /\ nPow___010^0-nPow___010^post2 == 0 /\ -nx13^post2+nx13^0 == 0 /\ -nPow___015^post2+nPow___015^0 == 0 /\ np19^0-np19^post2 == 0 /\ nx18^0-nx18^post2 == 0 /\ 1+ni21^0-np19^0 <= 0 /\ -ret_nPow12^post2+ret_nPow12^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ nc^0-nc^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -nx8^post2+nx8^0 == 0 /\ nb^0-nb^post2 == 0 /\ -nN^post2+nN^0 == 0 /\ -ni16^post2+ni16^0 == 0 /\ -np9^post2+np9^0 == 0 /\ -np14^post2+np14^0 == 0 /\ ret_nPow17^0-ret_nPow17^post2 == 0), cost: 1
   6: l4 -> l2 : na^0'=na^post6, ret_nPow17^0'=ret_nPow17^post6, np9^0'=np9^post6, nPow___010^0'=nPow___010^post6, nx18^0'=nx18^post6, ni21^0'=ni21^post6, tmp^0'=tmp^post6, nc^0'=nc^post6, nPow___020^0'=nPow___020^post6, ret_nPow12^0'=ret_nPow12^post6, np19^0'=np19^post6, tmp___1^0'=tmp___1^post6, nN^0'=nN^post6, ni16^0'=ni16^post6, nb^0'=nb^post6, ret_nPow22^0'=ret_nPow22^post6, nx13^0'=nx13^post6, nPow___015^0'=nPow___015^post6, nx8^0'=nx8^post6, np14^0'=np14^post6, tmp___0^0'=tmp___0^post6, ni11^0'=ni11^post6, (nPow___015^0-nPow___015^post6 == 0 /\ -nx13^post6+nx13^0 == 0 /\ -np14^post6+np14^0 == 0 /\ np19^0-np19^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -nc^post6+nc^0 == 0 /\ -nPow___020^post6+nPow___020^0 == 0 /\ -ret_nPow22^post6+ret_nPow22^0 == 0 /\ -ret_nPow12^post6+ret_nPow12^0 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ ret_nPow17^0-ret_nPow17^post6 == 0 /\ na^0-na^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -nx8^post6+nx8^0 == 0 /\ ni16^0-ni16^post6 == 0 /\ np9^0-np9^post6 == 0 /\ -nx18^post6+nx18^0 == 0 /\ nb^0-nb^post6 == 0 /\ nPow___010^0-nPow___010^post6 == 0 /\ -ni11^post6+ni11^0 == 0 /\ -ni21^post6+ni21^0 == 0 /\ -nN^post6+nN^0 == 0), cost: 1
   3: l5 -> l6 : na^0'=na^post3, ret_nPow17^0'=ret_nPow17^post3, np9^0'=np9^post3, nPow___010^0'=nPow___010^post3, nx18^0'=nx18^post3, ni21^0'=ni21^post3, tmp^0'=tmp^post3, nc^0'=nc^post3, nPow___020^0'=nPow___020^post3, ret_nPow12^0'=ret_nPow12^post3, np19^0'=np19^post3, tmp___1^0'=tmp___1^post3, nN^0'=nN^post3, ni16^0'=ni16^post3, nb^0'=nb^post3, ret_nPow22^0'=ret_nPow22^post3, nx13^0'=nx13^post3, nPow___015^0'=nPow___015^post3, nx8^0'=nx8^post3, np14^0'=np14^post3, tmp___0^0'=tmp___0^post3, ni11^0'=ni11^post3, (-ni11^post3+ni11^0 == 0 /\ -ni16^post3+ni16^0 == 0 /\ nx18^0-nx18^post3 == 0 /\ ni21^0-ni21^post3 == 0 /\ nc^0-nc^post3 == 0 /\ ret_nPow17^0-ret_nPow17^post3 == 0 /\ na^0-na^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -np19^post3+np19^0 == 0 /\ nN^0-nN^post3 == 0 /\ nPow___020^0-nPow___020^post3 == 0 /\ -nb^post3+nb^0 == 0 /\ -nPow___010^post3+nPow___010^0 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ -nPow___015^post3+nPow___015^0 == 0 /\ ret_nPow22^0-ret_nPow22^post3 == 0 /\ ret_nPow12^0-ret_nPow12^post3 == 0 /\ np9^0-np9^post3 == 0 /\ -nx13^post3+nx13^0 == 0 /\ -np14^post3+np14^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -nx8^post3+nx8^0 == 0), cost: 1
   4: l6 -> l4 : na^0'=na^post4, ret_nPow17^0'=ret_nPow17^post4, np9^0'=np9^post4, nPow___010^0'=nPow___010^post4, nx18^0'=nx18^post4, ni21^0'=ni21^post4, tmp^0'=tmp^post4, nc^0'=nc^post4, nPow___020^0'=nPow___020^post4, ret_nPow12^0'=ret_nPow12^post4, np19^0'=np19^post4, tmp___1^0'=tmp___1^post4, nN^0'=nN^post4, ni16^0'=ni16^post4, nb^0'=nb^post4, ret_nPow22^0'=ret_nPow22^post4, nx13^0'=nx13^post4, nPow___015^0'=nPow___015^post4, nx8^0'=nx8^post4, np14^0'=np14^post4, tmp___0^0'=tmp___0^post4, ni11^0'=ni11^post4, (-ni16^0+np14^0 <= 0 /\ -np14^post4+np14^0 == 0 /\ -nx13^post4+nx13^0 == 0 /\ nN^0-nN^post4 == 0 /\ -nb^post4+nb^0 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ na^0-na^post4 == 0 /\ -nPow___015^post4+nPow___015^0 == 0 /\ -nx8^post4+nx8^0 == 0 /\ -nc^post4+nc^0 == 0 /\ ret_nPow22^0-ret_nPow22^post4 == 0 /\ ret_nPow17^post4-nPow___015^0 == 0 /\ -ni11^post4+ni11^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ nPow___010^0-nPow___010^post4 == 0 /\ ni21^post4 == 0 /\ np19^post4-nN^0 == 0 /\ -nc^0+nx18^post4 == 0 /\ ret_nPow12^0-ret_nPow12^post4 == 0 /\ -ret_nPow17^post4+tmp___0^post4 == 0 /\ np9^0-np9^post4 == 0 /\ -1+nPow___020^post4 == 0 /\ -ni16^post4+ni16^0 == 0), cost: 1
   5: l6 -> l5 : na^0'=na^post5, ret_nPow17^0'=ret_nPow17^post5, np9^0'=np9^post5, nPow___010^0'=nPow___010^post5, nx18^0'=nx18^post5, ni21^0'=ni21^post5, tmp^0'=tmp^post5, nc^0'=nc^post5, nPow___020^0'=nPow___020^post5, ret_nPow12^0'=ret_nPow12^post5, np19^0'=np19^post5, tmp___1^0'=tmp___1^post5, nN^0'=nN^post5, ni16^0'=ni16^post5, nb^0'=nb^post5, ret_nPow22^0'=ret_nPow22^post5, nx13^0'=nx13^post5, nPow___015^0'=nPow___015^post5, nx8^0'=nx8^post5, np14^0'=np14^post5, tmp___0^0'=tmp___0^post5, ni11^0'=ni11^post5, (0 == 0 /\ nPow___010^0-nPow___010^post5 == 0 /\ -nPow___020^post5+nPow___020^0 == 0 /\ np14^0-np14^post5 == 0 /\ np9^0-np9^post5 == 0 /\ -ni11^post5+ni11^0 == 0 /\ 1+ni16^0-np14^0 <= 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ -nb^post5+nb^0 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ ret_nPow12^0-ret_nPow12^post5 == 0 /\ nx8^0-nx8^post5 == 0 /\ -1-ni16^0+ni16^post5 == 0 /\ -ret_nPow22^post5+ret_nPow22^0 == 0 /\ nN^0-nN^post5 == 0 /\ ni21^0-ni21^post5 == 0 /\ np19^0-np19^post5 == 0 /\ nx18^0-nx18^post5 == 0 /\ na^0-na^post5 == 0 /\ -ret_nPow17^post5+ret_nPow17^0 == 0 /\ nx13^0-nx13^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ -nc^post5+nc^0 == 0), cost: 1
   9: l7 -> l0 : na^0'=na^post9, ret_nPow17^0'=ret_nPow17^post9, np9^0'=np9^post9, nPow___010^0'=nPow___010^post9, nx18^0'=nx18^post9, ni21^0'=ni21^post9, tmp^0'=tmp^post9, nc^0'=nc^post9, nPow___020^0'=nPow___020^post9, ret_nPow12^0'=ret_nPow12^post9, np19^0'=np19^post9, tmp___1^0'=tmp___1^post9, nN^0'=nN^post9, ni16^0'=ni16^post9, nb^0'=nb^post9, ret_nPow22^0'=ret_nPow22^post9, nx13^0'=nx13^post9, nPow___015^0'=nPow___015^post9, nx8^0'=nx8^post9, np14^0'=np14^post9, tmp___0^0'=tmp___0^post9, ni11^0'=ni11^post9, (-ni16^post9+ni16^0 == 0 /\ -nPow___015^post9+nPow___015^0 == 0 /\ -np14^post9+np14^0 == 0 /\ nc^0-nc^post9 == 0 /\ -nx13^post9+nx13^0 == 0 /\ -1+nPow___010^post9 == 0 /\ -nb^post9+nb^0 == 0 /\ ni21^0-ni21^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ nPow___020^0-nPow___020^post9 == 0 /\ ret_nPow22^0-ret_nPow22^post9 == 0 /\ tmp^0-tmp^post9 == 0 /\ na^0-na^post9 == 0 /\ ret_nPow17^0-ret_nPow17^post9 == 0 /\ nx18^0-nx18^post9 == 0 /\ np9^post9-nN^post9 == 0 /\ nx8^post9-na^0 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -3+nN^post9 == 0 /\ -np19^post9+np19^0 == 0 /\ ret_nPow12^0-ret_nPow12^post9 == 0 /\ ni11^post9 == 0), cost: 1
  10: l8 -> l7 : na^0'=na^post10, ret_nPow17^0'=ret_nPow17^post10, np9^0'=np9^post10, nPow___010^0'=nPow___010^post10, nx18^0'=nx18^post10, ni21^0'=ni21^post10, tmp^0'=tmp^post10, nc^0'=nc^post10, nPow___020^0'=nPow___020^post10, ret_nPow12^0'=ret_nPow12^post10, np19^0'=np19^post10, tmp___1^0'=tmp___1^post10, nN^0'=nN^post10, ni16^0'=ni16^post10, nb^0'=nb^post10, ret_nPow22^0'=ret_nPow22^post10, nx13^0'=nx13^post10, nPow___015^0'=nPow___015^post10, nx8^0'=nx8^post10, np14^0'=np14^post10, tmp___0^0'=tmp___0^post10, ni11^0'=ni11^post10, (tmp^0-tmp^post10 == 0 /\ nPow___010^0-nPow___010^post10 == 0 /\ -nx8^post10+nx8^0 == 0 /\ -ni11^post10+ni11^0 == 0 /\ ret_nPow17^0-ret_nPow17^post10 == 0 /\ np9^0-np9^post10 == 0 /\ -tmp___1^post10+tmp___1^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ -nb^post10+nb^0 == 0 /\ -ni16^post10+ni16^0 == 0 /\ -np14^post10+np14^0 == 0 /\ -ret_nPow22^post10+ret_nPow22^0 == 0 /\ np19^0-np19^post10 == 0 /\ ret_nPow12^0-ret_nPow12^post10 == 0 /\ nx18^0-nx18^post10 == 0 /\ nPow___020^0-nPow___020^post10 == 0 /\ ni21^0-ni21^post10 == 0 /\ -nPow___015^post10+nPow___015^0 == 0 /\ nN^0-nN^post10 == 0 /\ -nc^post10+nc^0 == 0 /\ na^0-na^post10 == 0 /\ -nx13^post10+nx13^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : na^0'=na^post0, ret_nPow17^0'=ret_nPow17^post0, np9^0'=np9^post0, nPow___010^0'=nPow___010^post0, nx18^0'=nx18^post0, ni21^0'=ni21^post0, tmp^0'=tmp^post0, nc^0'=nc^post0, nPow___020^0'=nPow___020^post0, ret_nPow12^0'=ret_nPow12^post0, np19^0'=np19^post0, tmp___1^0'=tmp___1^post0, nN^0'=nN^post0, ni16^0'=ni16^post0, nb^0'=nb^post0, ret_nPow22^0'=ret_nPow22^post0, nx13^0'=nx13^post0, nPow___015^0'=nPow___015^post0, nx8^0'=nx8^post0, np14^0'=np14^post0, tmp___0^0'=tmp___0^post0, ni11^0'=ni11^post0, (tmp^0-tmp^post0 == 0 /\ nPow___010^0-nPow___010^post0 == 0 /\ -np19^post0+np19^0 == 0 /\ -ni11^post0+ni11^0 == 0 /\ np9^0-np9^post0 == 0 /\ np14^0-np14^post0 == 0 /\ -tmp___0^post0+tmp___0^0 == 0 /\ -ni16^post0+ni16^0 == 0 /\ -nc^post0+nc^0 == 0 /\ -nb^post0+nb^0 == 0 /\ nx8^0-nx8^post0 == 0 /\ nN^0-nN^post0 == 0 /\ ni21^0-ni21^post0 == 0 /\ nx13^0-nx13^post0 == 0 /\ -ret_nPow22^post0+ret_nPow22^0 == 0 /\ na^0-na^post0 == 0 /\ -nPow___015^post0+nPow___015^0 == 0 /\ nPow___020^0-nPow___020^post0 == 0 /\ ret_nPow12^0-ret_nPow12^post0 == 0 /\ -ret_nPow17^post0+ret_nPow17^0 == 0 /\ -tmp___1^post0+tmp___1^0 == 0 /\ nx18^0-nx18^post0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l4 : na^0'=na^post2, ret_nPow17^0'=ret_nPow17^post2, np9^0'=np9^post2, nPow___010^0'=nPow___010^post2, nx18^0'=nx18^post2, ni21^0'=ni21^post2, tmp^0'=tmp^post2, nc^0'=nc^post2, nPow___020^0'=nPow___020^post2, ret_nPow12^0'=ret_nPow12^post2, np19^0'=np19^post2, tmp___1^0'=tmp___1^post2, nN^0'=nN^post2, ni16^0'=ni16^post2, nb^0'=nb^post2, ret_nPow22^0'=ret_nPow22^post2, nx13^0'=nx13^post2, nPow___015^0'=nPow___015^post2, nx8^0'=nx8^post2, np14^0'=np14^post2, tmp___0^0'=tmp___0^post2, ni11^0'=ni11^post2, (0 == 0 /\ -1-ni21^0+ni21^post2 == 0 /\ -ret_nPow22^post2+ret_nPow22^0 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ na^0-na^post2 == 0 /\ -ni11^post2+ni11^0 == 0 /\ nPow___010^0-nPow___010^post2 == 0 /\ -nx13^post2+nx13^0 == 0 /\ -nPow___015^post2+nPow___015^0 == 0 /\ np19^0-np19^post2 == 0 /\ nx18^0-nx18^post2 == 0 /\ 1+ni21^0-np19^0 <= 0 /\ -ret_nPow12^post2+ret_nPow12^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ nc^0-nc^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -nx8^post2+nx8^0 == 0 /\ nb^0-nb^post2 == 0 /\ -nN^post2+nN^0 == 0 /\ -ni16^post2+ni16^0 == 0 /\ -np9^post2+np9^0 == 0 /\ -np14^post2+np14^0 == 0 /\ ret_nPow17^0-ret_nPow17^post2 == 0), cost: 1
New rule:
l2 -> l4 : ni21^0'=1+ni21^0, nPow___020^0'=nPow___020^post2, 1+ni21^0-np19^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l6 : na^0'=na^post3, ret_nPow17^0'=ret_nPow17^post3, np9^0'=np9^post3, nPow___010^0'=nPow___010^post3, nx18^0'=nx18^post3, ni21^0'=ni21^post3, tmp^0'=tmp^post3, nc^0'=nc^post3, nPow___020^0'=nPow___020^post3, ret_nPow12^0'=ret_nPow12^post3, np19^0'=np19^post3, tmp___1^0'=tmp___1^post3, nN^0'=nN^post3, ni16^0'=ni16^post3, nb^0'=nb^post3, ret_nPow22^0'=ret_nPow22^post3, nx13^0'=nx13^post3, nPow___015^0'=nPow___015^post3, nx8^0'=nx8^post3, np14^0'=np14^post3, tmp___0^0'=tmp___0^post3, ni11^0'=ni11^post3, (-ni11^post3+ni11^0 == 0 /\ -ni16^post3+ni16^0 == 0 /\ nx18^0-nx18^post3 == 0 /\ ni21^0-ni21^post3 == 0 /\ nc^0-nc^post3 == 0 /\ ret_nPow17^0-ret_nPow17^post3 == 0 /\ na^0-na^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -np19^post3+np19^0 == 0 /\ nN^0-nN^post3 == 0 /\ nPow___020^0-nPow___020^post3 == 0 /\ -nb^post3+nb^0 == 0 /\ -nPow___010^post3+nPow___010^0 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ -nPow___015^post3+nPow___015^0 == 0 /\ ret_nPow22^0-ret_nPow22^post3 == 0 /\ ret_nPow12^0-ret_nPow12^post3 == 0 /\ np9^0-np9^post3 == 0 /\ -nx13^post3+nx13^0 == 0 /\ -np14^post3+np14^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -nx8^post3+nx8^0 == 0), cost: 1
New rule:
l5 -> l6 : TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l4 : na^0'=na^post4, ret_nPow17^0'=ret_nPow17^post4, np9^0'=np9^post4, nPow___010^0'=nPow___010^post4, nx18^0'=nx18^post4, ni21^0'=ni21^post4, tmp^0'=tmp^post4, nc^0'=nc^post4, nPow___020^0'=nPow___020^post4, ret_nPow12^0'=ret_nPow12^post4, np19^0'=np19^post4, tmp___1^0'=tmp___1^post4, nN^0'=nN^post4, ni16^0'=ni16^post4, nb^0'=nb^post4, ret_nPow22^0'=ret_nPow22^post4, nx13^0'=nx13^post4, nPow___015^0'=nPow___015^post4, nx8^0'=nx8^post4, np14^0'=np14^post4, tmp___0^0'=tmp___0^post4, ni11^0'=ni11^post4, (-ni16^0+np14^0 <= 0 /\ -np14^post4+np14^0 == 0 /\ -nx13^post4+nx13^0 == 0 /\ nN^0-nN^post4 == 0 /\ -nb^post4+nb^0 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ na^0-na^post4 == 0 /\ -nPow___015^post4+nPow___015^0 == 0 /\ -nx8^post4+nx8^0 == 0 /\ -nc^post4+nc^0 == 0 /\ ret_nPow22^0-ret_nPow22^post4 == 0 /\ ret_nPow17^post4-nPow___015^0 == 0 /\ -ni11^post4+ni11^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ nPow___010^0-nPow___010^post4 == 0 /\ ni21^post4 == 0 /\ np19^post4-nN^0 == 0 /\ -nc^0+nx18^post4 == 0 /\ ret_nPow12^0-ret_nPow12^post4 == 0 /\ -ret_nPow17^post4+tmp___0^post4 == 0 /\ np9^0-np9^post4 == 0 /\ -1+nPow___020^post4 == 0 /\ -ni16^post4+ni16^0 == 0), cost: 1
New rule:
l6 -> l4 : ret_nPow17^0'=nPow___015^0, nx18^0'=nc^0, ni21^0'=0, nPow___020^0'=1, np19^0'=nN^0, tmp___0^0'=nPow___015^0, -ni16^0+np14^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : na^0'=na^post5, ret_nPow17^0'=ret_nPow17^post5, np9^0'=np9^post5, nPow___010^0'=nPow___010^post5, nx18^0'=nx18^post5, ni21^0'=ni21^post5, tmp^0'=tmp^post5, nc^0'=nc^post5, nPow___020^0'=nPow___020^post5, ret_nPow12^0'=ret_nPow12^post5, np19^0'=np19^post5, tmp___1^0'=tmp___1^post5, nN^0'=nN^post5, ni16^0'=ni16^post5, nb^0'=nb^post5, ret_nPow22^0'=ret_nPow22^post5, nx13^0'=nx13^post5, nPow___015^0'=nPow___015^post5, nx8^0'=nx8^post5, np14^0'=np14^post5, tmp___0^0'=tmp___0^post5, ni11^0'=ni11^post5, (0 == 0 /\ nPow___010^0-nPow___010^post5 == 0 /\ -nPow___020^post5+nPow___020^0 == 0 /\ np14^0-np14^post5 == 0 /\ np9^0-np9^post5 == 0 /\ -ni11^post5+ni11^0 == 0 /\ 1+ni16^0-np14^0 <= 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ -nb^post5+nb^0 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ ret_nPow12^0-ret_nPow12^post5 == 0 /\ nx8^0-nx8^post5 == 0 /\ -1-ni16^0+ni16^post5 == 0 /\ -ret_nPow22^post5+ret_nPow22^0 == 0 /\ nN^0-nN^post5 == 0 /\ ni21^0-ni21^post5 == 0 /\ np19^0-np19^post5 == 0 /\ nx18^0-nx18^post5 == 0 /\ na^0-na^post5 == 0 /\ -ret_nPow17^post5+ret_nPow17^0 == 0 /\ nx13^0-nx13^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ -nc^post5+nc^0 == 0), cost: 1
New rule:
l6 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : na^0'=na^post6, ret_nPow17^0'=ret_nPow17^post6, np9^0'=np9^post6, nPow___010^0'=nPow___010^post6, nx18^0'=nx18^post6, ni21^0'=ni21^post6, tmp^0'=tmp^post6, nc^0'=nc^post6, nPow___020^0'=nPow___020^post6, ret_nPow12^0'=ret_nPow12^post6, np19^0'=np19^post6, tmp___1^0'=tmp___1^post6, nN^0'=nN^post6, ni16^0'=ni16^post6, nb^0'=nb^post6, ret_nPow22^0'=ret_nPow22^post6, nx13^0'=nx13^post6, nPow___015^0'=nPow___015^post6, nx8^0'=nx8^post6, np14^0'=np14^post6, tmp___0^0'=tmp___0^post6, ni11^0'=ni11^post6, (nPow___015^0-nPow___015^post6 == 0 /\ -nx13^post6+nx13^0 == 0 /\ -np14^post6+np14^0 == 0 /\ np19^0-np19^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -nc^post6+nc^0 == 0 /\ -nPow___020^post6+nPow___020^0 == 0 /\ -ret_nPow22^post6+ret_nPow22^0 == 0 /\ -ret_nPow12^post6+ret_nPow12^0 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ ret_nPow17^0-ret_nPow17^post6 == 0 /\ na^0-na^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -nx8^post6+nx8^0 == 0 /\ ni16^0-ni16^post6 == 0 /\ np9^0-np9^post6 == 0 /\ -nx18^post6+nx18^0 == 0 /\ nb^0-nb^post6 == 0 /\ nPow___010^0-nPow___010^post6 == 0 /\ -ni11^post6+ni11^0 == 0 /\ -ni21^post6+ni21^0 == 0 /\ -nN^post6+nN^0 == 0), cost: 1
New rule:
l4 -> l2 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l5 : na^0'=na^post7, ret_nPow17^0'=ret_nPow17^post7, np9^0'=np9^post7, nPow___010^0'=nPow___010^post7, nx18^0'=nx18^post7, ni21^0'=ni21^post7, tmp^0'=tmp^post7, nc^0'=nc^post7, nPow___020^0'=nPow___020^post7, ret_nPow12^0'=ret_nPow12^post7, np19^0'=np19^post7, tmp___1^0'=tmp___1^post7, nN^0'=nN^post7, ni16^0'=ni16^post7, nb^0'=nb^post7, ret_nPow22^0'=ret_nPow22^post7, nx13^0'=nx13^post7, nPow___015^0'=nPow___015^post7, nx8^0'=nx8^post7, np14^0'=np14^post7, tmp___0^0'=tmp___0^post7, ni11^0'=ni11^post7, (-nN^post7+nN^0 == 0 /\ -ret_nPow22^post7+ret_nPow22^0 == 0 /\ np9^0-ni11^0 <= 0 /\ na^0-na^post7 == 0 /\ -ni11^post7+ni11^0 == 0 /\ nPow___010^0-nPow___010^post7 == 0 /\ -ret_nPow12^post7+tmp^post7 == 0 /\ tmp___1^0-tmp___1^post7 == 0 /\ np19^0-np19^post7 == 0 /\ -1+nPow___015^post7 == 0 /\ nx18^0-nx18^post7 == 0 /\ ni21^0-ni21^post7 == 0 /\ nx13^post7-nb^0 == 0 /\ np14^post7-nN^0 == 0 /\ ni16^post7 == 0 /\ nc^0-nc^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ nb^0-nb^post7 == 0 /\ nPow___020^0-nPow___020^post7 == 0 /\ -nx8^post7+nx8^0 == 0 /\ -np9^post7+np9^0 == 0 /\ ret_nPow17^0-ret_nPow17^post7 == 0 /\ -nPow___010^0+ret_nPow12^post7 == 0), cost: 1
New rule:
l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l0 : na^0'=na^post8, ret_nPow17^0'=ret_nPow17^post8, np9^0'=np9^post8, nPow___010^0'=nPow___010^post8, nx18^0'=nx18^post8, ni21^0'=ni21^post8, tmp^0'=tmp^post8, nc^0'=nc^post8, nPow___020^0'=nPow___020^post8, ret_nPow12^0'=ret_nPow12^post8, np19^0'=np19^post8, tmp___1^0'=tmp___1^post8, nN^0'=nN^post8, ni16^0'=ni16^post8, nb^0'=nb^post8, ret_nPow22^0'=ret_nPow22^post8, nx13^0'=nx13^post8, nPow___015^0'=nPow___015^post8, nx8^0'=nx8^post8, np14^0'=np14^post8, tmp___0^0'=tmp___0^post8, ni11^0'=ni11^post8, (0 == 0 /\ -nx8^post8+nx8^0 == 0 /\ -ni16^post8+ni16^0 == 0 /\ tmp___1^0-tmp___1^post8 == 0 /\ np9^0-np9^post8 == 0 /\ nc^0-nc^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -nx13^post8+nx13^0 == 0 /\ -ret_nPow12^post8+ret_nPow12^0 == 0 /\ nb^0-nb^post8 == 0 /\ -np19^post8+np19^0 == 0 /\ 1-np9^0+ni11^0 <= 0 /\ nPow___020^0-nPow___020^post8 == 0 /\ ni21^0-ni21^post8 == 0 /\ -nN^post8+nN^0 == 0 /\ -ret_nPow22^post8+ret_nPow22^0 == 0 /\ -1+ni11^post8-ni11^0 == 0 /\ na^0-na^post8 == 0 /\ ret_nPow17^0-ret_nPow17^post8 == 0 /\ -nPow___015^post8+nPow___015^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -np14^post8+np14^0 == 0 /\ nx18^0-nx18^post8 == 0), cost: 1
New rule:
l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l0 : na^0'=na^post9, ret_nPow17^0'=ret_nPow17^post9, np9^0'=np9^post9, nPow___010^0'=nPow___010^post9, nx18^0'=nx18^post9, ni21^0'=ni21^post9, tmp^0'=tmp^post9, nc^0'=nc^post9, nPow___020^0'=nPow___020^post9, ret_nPow12^0'=ret_nPow12^post9, np19^0'=np19^post9, tmp___1^0'=tmp___1^post9, nN^0'=nN^post9, ni16^0'=ni16^post9, nb^0'=nb^post9, ret_nPow22^0'=ret_nPow22^post9, nx13^0'=nx13^post9, nPow___015^0'=nPow___015^post9, nx8^0'=nx8^post9, np14^0'=np14^post9, tmp___0^0'=tmp___0^post9, ni11^0'=ni11^post9, (-ni16^post9+ni16^0 == 0 /\ -nPow___015^post9+nPow___015^0 == 0 /\ -np14^post9+np14^0 == 0 /\ nc^0-nc^post9 == 0 /\ -nx13^post9+nx13^0 == 0 /\ -1+nPow___010^post9 == 0 /\ -nb^post9+nb^0 == 0 /\ ni21^0-ni21^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ nPow___020^0-nPow___020^post9 == 0 /\ ret_nPow22^0-ret_nPow22^post9 == 0 /\ tmp^0-tmp^post9 == 0 /\ na^0-na^post9 == 0 /\ ret_nPow17^0-ret_nPow17^post9 == 0 /\ nx18^0-nx18^post9 == 0 /\ np9^post9-nN^post9 == 0 /\ nx8^post9-na^0 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -3+nN^post9 == 0 /\ -np19^post9+np19^0 == 0 /\ ret_nPow12^0-ret_nPow12^post9 == 0 /\ ni11^post9 == 0), cost: 1
New rule:
l7 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : na^0'=na^post10, ret_nPow17^0'=ret_nPow17^post10, np9^0'=np9^post10, nPow___010^0'=nPow___010^post10, nx18^0'=nx18^post10, ni21^0'=ni21^post10, tmp^0'=tmp^post10, nc^0'=nc^post10, nPow___020^0'=nPow___020^post10, ret_nPow12^0'=ret_nPow12^post10, np19^0'=np19^post10, tmp___1^0'=tmp___1^post10, nN^0'=nN^post10, ni16^0'=ni16^post10, nb^0'=nb^post10, ret_nPow22^0'=ret_nPow22^post10, nx13^0'=nx13^post10, nPow___015^0'=nPow___015^post10, nx8^0'=nx8^post10, np14^0'=np14^post10, tmp___0^0'=tmp___0^post10, ni11^0'=ni11^post10, (tmp^0-tmp^post10 == 0 /\ nPow___010^0-nPow___010^post10 == 0 /\ -nx8^post10+nx8^0 == 0 /\ -ni11^post10+ni11^0 == 0 /\ ret_nPow17^0-ret_nPow17^post10 == 0 /\ np9^0-np9^post10 == 0 /\ -tmp___1^post10+tmp___1^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ -nb^post10+nb^0 == 0 /\ -ni16^post10+ni16^0 == 0 /\ -np14^post10+np14^0 == 0 /\ -ret_nPow22^post10+ret_nPow22^0 == 0 /\ np19^0-np19^post10 == 0 /\ ret_nPow12^0-ret_nPow12^post10 == 0 /\ nx18^0-nx18^post10 == 0 /\ nPow___020^0-nPow___020^post10 == 0 /\ ni21^0-ni21^post10 == 0 /\ -nPow___015^post10+nPow___015^0 == 0 /\ nN^0-nN^post10 == 0 /\ -nc^post10+nc^0 == 0 /\ na^0-na^post10 == 0 /\ -nx13^post10+nx13^0 == 0), cost: 1
New rule:
l8 -> l7 : TRUE, cost: 1

Simplified rules
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  12: l2 -> l4 : ni21^0'=1+ni21^0, nPow___020^0'=nPow___020^post2, 1+ni21^0-np19^0 <= 0, cost: 1
  16: l4 -> l2 : TRUE, cost: 1
  13: l5 -> l6 : TRUE, cost: 1
  14: l6 -> l4 : ret_nPow17^0'=nPow___015^0, nx18^0'=nc^0, ni21^0'=0, nPow___020^0'=1, np19^0'=nN^0, tmp___0^0'=nPow___015^0, -ni16^0+np14^0 <= 0, cost: 1
  15: l6 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 1
  19: l7 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 1
  20: l8 -> l7 : TRUE, cost: 1


Eliminating location l7 by chaining:

Applied chaining
First rule:
l8 -> l7 : TRUE, cost: 1
Second rule:
l7 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 1
New rule:
l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2

Applied deletion
Removed the following rules: 19 20

Eliminating location l2 by chaining:

Applied chaining
First rule:
l4 -> l2 : TRUE, cost: 1
Second rule:
l2 -> l4 : ni21^0'=1+ni21^0, nPow___020^0'=nPow___020^post2, 1+ni21^0-np19^0 <= 0, cost: 1
New rule:
l4 -> l4 : ni21^0'=1+ni21^0, nPow___020^0'=nPow___020^post2, 1+ni21^0-np19^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 12 16

Eliminated locations on linear paths
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  22: l4 -> l4 : ni21^0'=1+ni21^0, nPow___020^0'=nPow___020^post2, 1+ni21^0-np19^0 <= 0, cost: 2
  13: l5 -> l6 : TRUE, cost: 1
  14: l6 -> l4 : ret_nPow17^0'=nPow___015^0, nx18^0'=nc^0, ni21^0'=0, nPow___020^0'=1, np19^0'=nN^0, tmp___0^0'=nPow___015^0, -ni16^0+np14^0 <= 0, cost: 1
  15: l6 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 1
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l4 -> l4 : ni21^0'=1+ni21^0, nPow___020^0'=nPow___020^post2, 1+ni21^0-np19^0 <= 0, cost: 2
New rule:
l4 -> l4 : ni21^0'=ni21^0+n, nPow___020^0'=nPow___020^post2, (-ni21^0+np19^0-n >= 0 /\ -1+n >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NljBPd.txt

Applied instantiation
Original rule:
l4 -> l4 : ni21^0'=ni21^0+n, nPow___020^0'=nPow___020^post2, (-ni21^0+np19^0-n >= 0 /\ -1+n >= 0), cost: 2*n
New rule:
l4 -> l4 : ni21^0'=np19^0, nPow___020^0'=nPow___020^post2, (0 >= 0 /\ -1-ni21^0+np19^0 >= 0), cost: -2*ni21^0+2*np19^0

Applied simplification
Original rule:
l4 -> l4 : ni21^0'=np19^0, nPow___020^0'=nPow___020^post2, (0 >= 0 /\ -1-ni21^0+np19^0 >= 0), cost: -2*ni21^0+2*np19^0
New rule:
l4 -> l4 : ni21^0'=np19^0, nPow___020^0'=nPow___020^post2, -1-ni21^0+np19^0 >= 0, cost: -2*ni21^0+2*np19^0

Applied deletion
Removed the following rules: 22

Accelerated simple loops
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  24: l4 -> l4 : ni21^0'=np19^0, nPow___020^0'=nPow___020^post2, -1-ni21^0+np19^0 >= 0, cost: -2*ni21^0+2*np19^0
  13: l5 -> l6 : TRUE, cost: 1
  14: l6 -> l4 : ret_nPow17^0'=nPow___015^0, nx18^0'=nc^0, ni21^0'=0, nPow___020^0'=1, np19^0'=nN^0, tmp___0^0'=nPow___015^0, -ni16^0+np14^0 <= 0, cost: 1
  15: l6 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 1
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l6 -> l4 : ret_nPow17^0'=nPow___015^0, nx18^0'=nc^0, ni21^0'=0, nPow___020^0'=1, np19^0'=nN^0, tmp___0^0'=nPow___015^0, -ni16^0+np14^0 <= 0, cost: 1
Second rule:
l4 -> l4 : ni21^0'=np19^0, nPow___020^0'=nPow___020^post2, -1-ni21^0+np19^0 >= 0, cost: -2*ni21^0+2*np19^0
New rule:
l6 -> l4 : ret_nPow17^0'=nPow___015^0, nx18^0'=nc^0, ni21^0'=nN^0, nPow___020^0'=nPow___020^post2, np19^0'=nN^0, tmp___0^0'=nPow___015^0, (-ni16^0+np14^0 <= 0 /\ -1+nN^0 >= 0), cost: 1+2*nN^0

Applied deletion
Removed the following rules: 24

Chained accelerated rules with incoming rules
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  13: l5 -> l6 : TRUE, cost: 1
  14: l6 -> l4 : ret_nPow17^0'=nPow___015^0, nx18^0'=nc^0, ni21^0'=0, nPow___020^0'=1, np19^0'=nN^0, tmp___0^0'=nPow___015^0, -ni16^0+np14^0 <= 0, cost: 1
  15: l6 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 1
  25: l6 -> l4 : ret_nPow17^0'=nPow___015^0, nx18^0'=nc^0, ni21^0'=nN^0, nPow___020^0'=nPow___020^post2, np19^0'=nN^0, tmp___0^0'=nPow___015^0, (-ni16^0+np14^0 <= 0 /\ -1+nN^0 >= 0), cost: 1+2*nN^0
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Removed unreachable locations and irrelevant leafs
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  13: l5 -> l6 : TRUE, cost: 1
  15: l6 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 1
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Eliminating location l6 by chaining:

Applied chaining
First rule:
l5 -> l6 : TRUE, cost: 1
Second rule:
l6 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 1
New rule:
l5 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 13 15

Eliminated locations on linear paths
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  26: l5 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 2
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l5 -> l5 : ni16^0'=1+ni16^0, nPow___015^0'=nPow___015^post5, 1+ni16^0-np14^0 <= 0, cost: 2
New rule:
l5 -> l5 : ni16^0'=n0+ni16^0, nPow___015^0'=nPow___015^post5, (-n0-ni16^0+np14^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bljfFd.txt

Applied instantiation
Original rule:
l5 -> l5 : ni16^0'=n0+ni16^0, nPow___015^0'=nPow___015^post5, (-n0-ni16^0+np14^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0
New rule:
l5 -> l5 : ni16^0'=np14^0, nPow___015^0'=nPow___015^post5, (0 >= 0 /\ -1-ni16^0+np14^0 >= 0), cost: -2*ni16^0+2*np14^0

Applied simplification
Original rule:
l5 -> l5 : ni16^0'=np14^0, nPow___015^0'=nPow___015^post5, (0 >= 0 /\ -1-ni16^0+np14^0 >= 0), cost: -2*ni16^0+2*np14^0
New rule:
l5 -> l5 : ni16^0'=np14^0, nPow___015^0'=nPow___015^post5, -1-ni16^0+np14^0 >= 0, cost: -2*ni16^0+2*np14^0

Applied deletion
Removed the following rules: 26

Accelerated simple loops
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  28: l5 -> l5 : ni16^0'=np14^0, nPow___015^0'=nPow___015^post5, -1-ni16^0+np14^0 >= 0, cost: -2*ni16^0+2*np14^0
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
Second rule:
l5 -> l5 : ni16^0'=np14^0, nPow___015^0'=nPow___015^post5, -1-ni16^0+np14^0 >= 0, cost: -2*ni16^0+2*np14^0
New rule:
l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=nN^0, nx13^0'=nb^0, nPow___015^0'=nPow___015^post5, np14^0'=nN^0, (np9^0-ni11^0 <= 0 /\ -1+nN^0 >= 0), cost: 1+2*nN^0

Applied deletion
Removed the following rules: 28

Chained accelerated rules with incoming rules
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=0, nx13^0'=nb^0, nPow___015^0'=1, np14^0'=nN^0, np9^0-ni11^0 <= 0, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  29: l1 -> l5 : tmp^0'=nPow___010^0, ret_nPow12^0'=nPow___010^0, ni16^0'=nN^0, nx13^0'=nb^0, nPow___015^0'=nPow___015^post5, np14^0'=nN^0, (np9^0-ni11^0 <= 0 /\ -1+nN^0 >= 0), cost: 1+2*nN^0
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Removed unreachable locations and irrelevant leafs
Start location: l8
  11: l0 -> l1 : TRUE, cost: 1
  18: l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 1
New rule:
l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 11 18

Eliminated locations on linear paths
Start location: l8
  30: l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 2
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=1+ni11^0, 1-np9^0+ni11^0 <= 0, cost: 2
New rule:
l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=n1+ni11^0, (-1+n1 >= 0 /\ np9^0-n1-ni11^0 >= 0), cost: 2*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_DjHNGp.txt

Applied instantiation
Original rule:
l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=n1+ni11^0, (-1+n1 >= 0 /\ np9^0-n1-ni11^0 >= 0), cost: 2*n1
New rule:
l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=np9^0, (0 >= 0 /\ -1+np9^0-ni11^0 >= 0), cost: 2*np9^0-2*ni11^0

Applied simplification
Original rule:
l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=np9^0, (0 >= 0 /\ -1+np9^0-ni11^0 >= 0), cost: 2*np9^0-2*ni11^0
New rule:
l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=np9^0, -1+np9^0-ni11^0 >= 0, cost: 2*np9^0-2*ni11^0

Applied deletion
Removed the following rules: 30

Accelerated simple loops
Start location: l8
  32: l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=np9^0, -1+np9^0-ni11^0 >= 0, cost: 2*np9^0-2*ni11^0
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2
Second rule:
l0 -> l0 : nPow___010^0'=nPow___010^post8, ni11^0'=np9^0, -1+np9^0-ni11^0 >= 0, cost: 2*np9^0-2*ni11^0
New rule:
l8 -> l0 : np9^0'=3, nPow___010^0'=nPow___010^post8, nN^0'=3, nx8^0'=na^0, ni11^0'=3, 2 >= 0, cost: 8

Applied deletion
Removed the following rules: 32

Chained accelerated rules with incoming rules
Start location: l8
  21: l8 -> l0 : np9^0'=3, nPow___010^0'=1, nN^0'=3, nx8^0'=na^0, ni11^0'=0, TRUE, cost: 2
  33: l8 -> l0 : np9^0'=3, nPow___010^0'=nPow___010^post8, nN^0'=3, nx8^0'=na^0, ni11^0'=3, 2 >= 0, cost: 8


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


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0