unknown Initial ITS Start location: l8 Program variables: na^0 nb^0 nc^0 ni11^0 ni16^0 ni21^0 nn^0 np14^0 np19^0 np9^0 npow___010^0 npow___015^0 npow___020^0 nx13^0 nx18^0 nx8^0 ret_npow12^0 ret_npow17^0 ret_npow22^0 tmp^0 tmp___0^0 tmp___1^0 0: l0 -> l1 : na^0'=na^post1, nb^0'=nb^post1, nc^0'=nc^post1, ni11^0'=ni11^post1, ni16^0'=ni16^post1, ni21^0'=ni21^post1, nn^0'=nn^post1, np14^0'=np14^post1, np19^0'=np19^post1, np9^0'=np9^post1, npow___010^0'=npow___010^post1, npow___015^0'=npow___015^post1, npow___020^0'=npow___020^post1, nx13^0'=nx13^post1, nx18^0'=nx18^post1, nx8^0'=nx8^post1, ret_npow12^0'=ret_npow12^post1, ret_npow17^0'=ret_npow17^post1, ret_npow22^0'=ret_npow22^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (tmp^0-tmp^post1 == 0 /\ tmp___0^0-tmp___0^post1 == 0 /\ ni11^0-ni11^post1 == 0 /\ -nx13^post1+nx13^0 == 0 /\ ni16^0-ni16^post1 == 0 /\ -nn^post1+nn^0 == 0 /\ np9^0-np9^post1 == 0 /\ ret_npow17^0-ret_npow17^post1 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -ni21^post1+ni21^0 == 0 /\ -nx8^post1+nx8^0 == 0 /\ nb^0-nb^post1 == 0 /\ na^0-na^post1 == 0 /\ -np14^post1+np14^0 == 0 /\ -np19^post1+np19^0 == 0 /\ -npow___015^post1+npow___015^0 == 0 /\ ret_npow12^0-ret_npow12^post1 == 0 /\ -npow___020^post1+npow___020^0 == 0 /\ npow___010^0-npow___010^post1 == 0 /\ -nc^post1+nc^0 == 0 /\ -ret_npow22^post1+ret_npow22^0 == 0 /\ -nx18^post1+nx18^0 == 0), cost: 1 7: l1 -> l5 : na^0'=na^post8, nb^0'=nb^post8, nc^0'=nc^post8, ni11^0'=ni11^post8, ni16^0'=ni16^post8, ni21^0'=ni21^post8, nn^0'=nn^post8, np14^0'=np14^post8, np19^0'=np19^post8, np9^0'=np9^post8, npow___010^0'=npow___010^post8, npow___015^0'=npow___015^post8, npow___020^0'=npow___020^post8, nx13^0'=nx13^post8, nx18^0'=nx18^post8, nx8^0'=nx8^post8, ret_npow12^0'=ret_npow12^post8, ret_npow17^0'=ret_npow17^post8, ret_npow22^0'=ret_npow22^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, (-tmp___1^post8+tmp___1^0 == 0 /\ -ret_npow22^post8+ret_npow22^0 == 0 /\ -nn^0+np14^post8 == 0 /\ -1+npow___015^post8 == 0 /\ -npow___010^0+ret_npow12^post8 == 0 /\ npow___010^0-npow___010^post8 == 0 /\ -ni11^0+np9^0 <= 0 /\ nx18^0-nx18^post8 == 0 /\ -np19^post8+np19^0 == 0 /\ np9^0-np9^post8 == 0 /\ -npow___020^post8+npow___020^0 == 0 /\ nx13^post8-nb^0 == 0 /\ ret_npow17^0-ret_npow17^post8 == 0 /\ tmp^post8-ret_npow12^post8 == 0 /\ -nn^post8+nn^0 == 0 /\ -nc^post8+nc^0 == 0 /\ -ni21^post8+ni21^0 == 0 /\ ni16^post8 == 0 /\ -nx8^post8+nx8^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ ni11^0-ni11^post8 == 0 /\ nb^0-nb^post8 == 0 /\ na^0-na^post8 == 0), cost: 1 8: l1 -> l0 : na^0'=na^post9, nb^0'=nb^post9, nc^0'=nc^post9, ni11^0'=ni11^post9, ni16^0'=ni16^post9, ni21^0'=ni21^post9, nn^0'=nn^post9, np14^0'=np14^post9, np19^0'=np19^post9, np9^0'=np9^post9, npow___010^0'=npow___010^post9, npow___015^0'=npow___015^post9, npow___020^0'=npow___020^post9, nx13^0'=nx13^post9, nx18^0'=nx18^post9, nx8^0'=nx8^post9, ret_npow12^0'=ret_npow12^post9, ret_npow17^0'=ret_npow17^post9, ret_npow22^0'=ret_npow22^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, (0 == 0 /\ -np9^post9+np9^0 == 0 /\ -np14^post9+np14^0 == 0 /\ -npow___020^post9+npow___020^0 == 0 /\ tmp___1^0-tmp___1^post9 == 0 /\ nc^0-nc^post9 == 0 /\ -npow___015^post9+npow___015^0 == 0 /\ -ret_npow12^post9+ret_npow12^0 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ na^0-na^post9 == 0 /\ -ni16^post9+ni16^0 == 0 /\ 1+ni11^0-np9^0 <= 0 /\ -nx8^post9+nx8^0 == 0 /\ ret_npow17^0-ret_npow17^post9 == 0 /\ nx18^0-nx18^post9 == 0 /\ ni21^0-ni21^post9 == 0 /\ np19^0-np19^post9 == 0 /\ ret_npow22^0-ret_npow22^post9 == 0 /\ -nx13^post9+nx13^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ -nb^post9+nb^0 == 0 /\ -1-ni11^0+ni11^post9 == 0 /\ -nn^post9+nn^0 == 0), cost: 1 1: l2 -> l3 : na^0'=na^post2, nb^0'=nb^post2, nc^0'=nc^post2, ni11^0'=ni11^post2, ni16^0'=ni16^post2, ni21^0'=ni21^post2, nn^0'=nn^post2, np14^0'=np14^post2, np19^0'=np19^post2, np9^0'=np9^post2, npow___010^0'=npow___010^post2, npow___015^0'=npow___015^post2, npow___020^0'=npow___020^post2, nx13^0'=nx13^post2, nx18^0'=nx18^post2, nx8^0'=nx8^post2, ret_npow12^0'=ret_npow12^post2, ret_npow17^0'=ret_npow17^post2, ret_npow22^0'=ret_npow22^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (nc^0-nc^post2 == 0 /\ -np19^post2+np19^0 == 0 /\ -nb^post2+nb^0 == 0 /\ tmp___1^post2-ret_npow22^post2 == 0 /\ npow___020^0-npow___020^post2 == 0 /\ np14^0-np14^post2 == 0 /\ na^0-na^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -ni16^post2+ni16^0 == 0 /\ -ni21^0+np19^0 <= 0 /\ ni11^0-ni11^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ -nx8^post2+nx8^0 == 0 /\ ret_npow17^0-ret_npow17^post2 == 0 /\ nn^0-nn^post2 == 0 /\ ret_npow22^post2-npow___020^0 == 0 /\ ret_npow12^0-ret_npow12^post2 == 0 /\ np9^0-np9^post2 == 0 /\ -npow___015^post2+npow___015^0 == 0 /\ -npow___010^post2+npow___010^0 == 0 /\ ni21^0-ni21^post2 == 0 /\ nx13^0-nx13^post2 == 0 /\ -nx18^post2+nx18^0 == 0), cost: 1 2: l2 -> l4 : na^0'=na^post3, nb^0'=nb^post3, nc^0'=nc^post3, ni11^0'=ni11^post3, ni16^0'=ni16^post3, ni21^0'=ni21^post3, nn^0'=nn^post3, np14^0'=np14^post3, np19^0'=np19^post3, np9^0'=np9^post3, npow___010^0'=npow___010^post3, npow___015^0'=npow___015^post3, npow___020^0'=npow___020^post3, nx13^0'=nx13^post3, nx18^0'=nx18^post3, nx8^0'=nx8^post3, ret_npow12^0'=ret_npow12^post3, ret_npow17^0'=ret_npow17^post3, ret_npow22^0'=ret_npow22^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (0 == 0 /\ -nx13^post3+nx13^0 == 0 /\ -ret_npow22^post3+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ 1+ni21^0-np19^0 <= 0 /\ ni16^0-ni16^post3 == 0 /\ nx18^0-nx18^post3 == 0 /\ -np19^post3+np19^0 == 0 /\ ni11^0-ni11^post3 == 0 /\ np9^0-np9^post3 == 0 /\ ret_npow17^0-ret_npow17^post3 == 0 /\ ret_npow12^0-ret_npow12^post3 == 0 /\ -nc^post3+nc^0 == 0 /\ na^0-na^post3 == 0 /\ -nb^post3+nb^0 == 0 /\ -tmp___1^post3+tmp___1^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -nn^post3+nn^0 == 0 /\ -1+ni21^post3-ni21^0 == 0 /\ -nx8^post3+nx8^0 == 0 /\ -npow___015^post3+npow___015^0 == 0 /\ -np14^post3+np14^0 == 0), cost: 1 6: l4 -> l2 : na^0'=na^post7, nb^0'=nb^post7, nc^0'=nc^post7, ni11^0'=ni11^post7, ni16^0'=ni16^post7, ni21^0'=ni21^post7, nn^0'=nn^post7, np14^0'=np14^post7, np19^0'=np19^post7, np9^0'=np9^post7, npow___010^0'=npow___010^post7, npow___015^0'=npow___015^post7, npow___020^0'=npow___020^post7, nx13^0'=nx13^post7, nx18^0'=nx18^post7, nx8^0'=nx8^post7, ret_npow12^0'=ret_npow12^post7, ret_npow17^0'=ret_npow17^post7, ret_npow22^0'=ret_npow22^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, (-nb^post7+nb^0 == 0 /\ ret_npow12^0-ret_npow12^post7 == 0 /\ nc^0-nc^post7 == 0 /\ ret_npow17^0-ret_npow17^post7 == 0 /\ -ni16^post7+ni16^0 == 0 /\ na^0-na^post7 == 0 /\ -nx13^post7+nx13^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -npow___020^post7+npow___020^0 == 0 /\ ni11^0-ni11^post7 == 0 /\ -nn^post7+nn^0 == 0 /\ -nx8^post7+nx8^0 == 0 /\ np19^0-np19^post7 == 0 /\ -ret_npow22^post7+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ ni21^0-ni21^post7 == 0 /\ -np9^post7+np9^0 == 0 /\ -npow___015^post7+npow___015^0 == 0 /\ -nx18^post7+nx18^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ -np14^post7+np14^0 == 0), cost: 1 3: l5 -> l6 : na^0'=na^post4, nb^0'=nb^post4, nc^0'=nc^post4, ni11^0'=ni11^post4, ni16^0'=ni16^post4, ni21^0'=ni21^post4, nn^0'=nn^post4, np14^0'=np14^post4, np19^0'=np19^post4, np9^0'=np9^post4, npow___010^0'=npow___010^post4, npow___015^0'=npow___015^post4, npow___020^0'=npow___020^post4, nx13^0'=nx13^post4, nx18^0'=nx18^post4, nx8^0'=nx8^post4, ret_npow12^0'=ret_npow12^post4, ret_npow17^0'=ret_npow17^post4, ret_npow22^0'=ret_npow22^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (-tmp___1^post4+tmp___1^0 == 0 /\ -ret_npow22^post4+ret_npow22^0 == 0 /\ -ret_npow17^post4+ret_npow17^0 == 0 /\ ni16^0-ni16^post4 == 0 /\ -np14^post4+np14^0 == 0 /\ -np19^post4+np19^0 == 0 /\ npow___015^0-npow___015^post4 == 0 /\ np9^0-np9^post4 == 0 /\ -nx18^post4+nx18^0 == 0 /\ -nx8^post4+nx8^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ npow___010^0-npow___010^post4 == 0 /\ -nc^post4+nc^0 == 0 /\ -nx13^post4+nx13^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ nb^0-nb^post4 == 0 /\ ret_npow12^0-ret_npow12^post4 == 0 /\ -npow___020^post4+npow___020^0 == 0 /\ -ni21^post4+ni21^0 == 0 /\ ni11^0-ni11^post4 == 0 /\ -nn^post4+nn^0 == 0 /\ na^0-na^post4 == 0), cost: 1 4: l6 -> l4 : na^0'=na^post5, nb^0'=nb^post5, nc^0'=nc^post5, ni11^0'=ni11^post5, ni16^0'=ni16^post5, ni21^0'=ni21^post5, nn^0'=nn^post5, np14^0'=np14^post5, np19^0'=np19^post5, np9^0'=np9^post5, npow___010^0'=npow___010^post5, npow___015^0'=npow___015^post5, npow___020^0'=npow___020^post5, nx13^0'=nx13^post5, nx18^0'=nx18^post5, nx8^0'=nx8^post5, ret_npow12^0'=ret_npow12^post5, ret_npow17^0'=ret_npow17^post5, ret_npow22^0'=ret_npow22^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (-ni16^0+np14^0 <= 0 /\ ni11^0-ni11^post5 == 0 /\ ret_npow12^0-ret_npow12^post5 == 0 /\ ni21^post5 == 0 /\ ni16^0-ni16^post5 == 0 /\ -npow___015^post5+npow___015^0 == 0 /\ -nn^post5+nn^0 == 0 /\ -nx8^post5+nx8^0 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -np14^post5+np14^0 == 0 /\ nb^0-nb^post5 == 0 /\ na^0-na^post5 == 0 /\ ret_npow17^post5-npow___015^0 == 0 /\ -nx13^post5+nx13^0 == 0 /\ np9^0-np9^post5 == 0 /\ nx18^post5-nc^0 == 0 /\ np19^post5-nn^0 == 0 /\ -ret_npow17^post5+tmp___0^post5 == 0 /\ -ret_npow22^post5+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post5 == 0 /\ -1+npow___020^post5 == 0 /\ -nc^post5+nc^0 == 0), cost: 1 5: l6 -> l5 : na^0'=na^post6, nb^0'=nb^post6, nc^0'=nc^post6, ni11^0'=ni11^post6, ni16^0'=ni16^post6, ni21^0'=ni21^post6, nn^0'=nn^post6, np14^0'=np14^post6, np19^0'=np19^post6, np9^0'=np9^post6, npow___010^0'=npow___010^post6, npow___015^0'=npow___015^post6, npow___020^0'=npow___020^post6, nx13^0'=nx13^post6, nx18^0'=nx18^post6, nx8^0'=nx8^post6, ret_npow12^0'=ret_npow12^post6, ret_npow17^0'=ret_npow17^post6, ret_npow22^0'=ret_npow22^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (0 == 0 /\ -1+ni16^post6-ni16^0 == 0 /\ tmp^0-tmp^post6 == 0 /\ -nn^post6+nn^0 == 0 /\ -ret_npow22^post6+ret_npow22^0 == 0 /\ nx18^0-nx18^post6 == 0 /\ npow___010^0-npow___010^post6 == 0 /\ -tmp___1^post6+tmp___1^0 == 0 /\ -nx13^post6+nx13^0 == 0 /\ 1+ni16^0-np14^0 <= 0 /\ -npow___020^post6+npow___020^0 == 0 /\ -ni21^post6+ni21^0 == 0 /\ -ret_npow12^post6+ret_npow12^0 == 0 /\ -nx8^post6+nx8^0 == 0 /\ nb^0-nb^post6 == 0 /\ -nc^post6+nc^0 == 0 /\ -np14^post6+np14^0 == 0 /\ ret_npow17^0-ret_npow17^post6 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ ni11^0-ni11^post6 == 0 /\ np9^0-np9^post6 == 0 /\ na^0-na^post6 == 0 /\ np19^0-np19^post6 == 0), cost: 1 9: l7 -> l0 : na^0'=na^post10, nb^0'=nb^post10, nc^0'=nc^post10, ni11^0'=ni11^post10, ni16^0'=ni16^post10, ni21^0'=ni21^post10, nn^0'=nn^post10, np14^0'=np14^post10, np19^0'=np19^post10, np9^0'=np9^post10, npow___010^0'=npow___010^post10, npow___015^0'=npow___015^post10, npow___020^0'=npow___020^post10, nx13^0'=nx13^post10, nx18^0'=nx18^post10, nx8^0'=nx8^post10, ret_npow12^0'=ret_npow12^post10, ret_npow17^0'=ret_npow17^post10, ret_npow22^0'=ret_npow22^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, (ni11^post10 == 0 /\ ret_npow12^0-ret_npow12^post10 == 0 /\ nc^0-nc^post10 == 0 /\ -npow___015^post10+npow___015^0 == 0 /\ -tmp___1^post10+tmp___1^0 == 0 /\ np19^0-np19^post10 == 0 /\ -ret_npow17^post10+ret_npow17^0 == 0 /\ -na^0+nx8^post10 == 0 /\ ni21^0-ni21^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ -ni16^post10+ni16^0 == 0 /\ na^0-na^post10 == 0 /\ -nn^post10+np9^post10 == 0 /\ -nx13^post10+nx13^0 == 0 /\ -nx18^post10+nx18^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -np14^post10+np14^0 == 0 /\ -nb^post10+nb^0 == 0 /\ -1+npow___010^post10 == 0 /\ -npow___020^post10+npow___020^0 == 0 /\ -3+nn^post10 == 0 /\ -ret_npow22^post10+ret_npow22^0 == 0), cost: 1 10: l8 -> l7 : na^0'=na^post11, nb^0'=nb^post11, nc^0'=nc^post11, ni11^0'=ni11^post11, ni16^0'=ni16^post11, ni21^0'=ni21^post11, nn^0'=nn^post11, np14^0'=np14^post11, np19^0'=np19^post11, np9^0'=np9^post11, npow___010^0'=npow___010^post11, npow___015^0'=npow___015^post11, npow___020^0'=npow___020^post11, nx13^0'=nx13^post11, nx18^0'=nx18^post11, nx8^0'=nx8^post11, ret_npow12^0'=ret_npow12^post11, ret_npow17^0'=ret_npow17^post11, ret_npow22^0'=ret_npow22^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, (ret_npow17^0-ret_npow17^post11 == 0 /\ nx18^0-nx18^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ -ret_npow22^post11+ret_npow22^0 == 0 /\ np9^0-np9^post11 == 0 /\ -nx13^post11+nx13^0 == 0 /\ -ni21^post11+ni21^0 == 0 /\ -nc^post11+nc^0 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ ni16^0-ni16^post11 == 0 /\ ret_npow12^0-ret_npow12^post11 == 0 /\ -nn^post11+nn^0 == 0 /\ -np19^post11+np19^0 == 0 /\ -np14^post11+np14^0 == 0 /\ -npow___020^post11+npow___020^0 == 0 /\ -npow___015^post11+npow___015^0 == 0 /\ npow___010^0-npow___010^post11 == 0 /\ nb^0-nb^post11 == 0 /\ tmp^0-tmp^post11 == 0 /\ na^0-na^post11 == 0 /\ ni11^0-ni11^post11 == 0 /\ -nx8^post11+nx8^0 == 0), cost: 1 Chained Linear Paths Start location: l8 Program variables: na^0 nb^0 nc^0 ni11^0 ni16^0 ni21^0 nn^0 np14^0 np19^0 np9^0 npow___010^0 npow___015^0 npow___020^0 nx13^0 nx18^0 nx8^0 ret_npow12^0 ret_npow17^0 ret_npow22^0 tmp^0 tmp___0^0 tmp___1^0 0: l0 -> l1 : na^0'=na^post1, nb^0'=nb^post1, nc^0'=nc^post1, ni11^0'=ni11^post1, ni16^0'=ni16^post1, ni21^0'=ni21^post1, nn^0'=nn^post1, np14^0'=np14^post1, np19^0'=np19^post1, np9^0'=np9^post1, npow___010^0'=npow___010^post1, npow___015^0'=npow___015^post1, npow___020^0'=npow___020^post1, nx13^0'=nx13^post1, nx18^0'=nx18^post1, nx8^0'=nx8^post1, ret_npow12^0'=ret_npow12^post1, ret_npow17^0'=ret_npow17^post1, ret_npow22^0'=ret_npow22^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (tmp^0-tmp^post1 == 0 /\ tmp___0^0-tmp___0^post1 == 0 /\ ni11^0-ni11^post1 == 0 /\ -nx13^post1+nx13^0 == 0 /\ ni16^0-ni16^post1 == 0 /\ -nn^post1+nn^0 == 0 /\ np9^0-np9^post1 == 0 /\ ret_npow17^0-ret_npow17^post1 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -ni21^post1+ni21^0 == 0 /\ -nx8^post1+nx8^0 == 0 /\ nb^0-nb^post1 == 0 /\ na^0-na^post1 == 0 /\ -np14^post1+np14^0 == 0 /\ -np19^post1+np19^0 == 0 /\ -npow___015^post1+npow___015^0 == 0 /\ ret_npow12^0-ret_npow12^post1 == 0 /\ -npow___020^post1+npow___020^0 == 0 /\ npow___010^0-npow___010^post1 == 0 /\ -nc^post1+nc^0 == 0 /\ -ret_npow22^post1+ret_npow22^0 == 0 /\ -nx18^post1+nx18^0 == 0), cost: 1 7: l1 -> l5 : na^0'=na^post8, nb^0'=nb^post8, nc^0'=nc^post8, ni11^0'=ni11^post8, ni16^0'=ni16^post8, ni21^0'=ni21^post8, nn^0'=nn^post8, np14^0'=np14^post8, np19^0'=np19^post8, np9^0'=np9^post8, npow___010^0'=npow___010^post8, npow___015^0'=npow___015^post8, npow___020^0'=npow___020^post8, nx13^0'=nx13^post8, nx18^0'=nx18^post8, nx8^0'=nx8^post8, ret_npow12^0'=ret_npow12^post8, ret_npow17^0'=ret_npow17^post8, ret_npow22^0'=ret_npow22^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, (-tmp___1^post8+tmp___1^0 == 0 /\ -ret_npow22^post8+ret_npow22^0 == 0 /\ -nn^0+np14^post8 == 0 /\ -1+npow___015^post8 == 0 /\ -npow___010^0+ret_npow12^post8 == 0 /\ npow___010^0-npow___010^post8 == 0 /\ -ni11^0+np9^0 <= 0 /\ nx18^0-nx18^post8 == 0 /\ -np19^post8+np19^0 == 0 /\ np9^0-np9^post8 == 0 /\ -npow___020^post8+npow___020^0 == 0 /\ nx13^post8-nb^0 == 0 /\ ret_npow17^0-ret_npow17^post8 == 0 /\ tmp^post8-ret_npow12^post8 == 0 /\ -nn^post8+nn^0 == 0 /\ -nc^post8+nc^0 == 0 /\ -ni21^post8+ni21^0 == 0 /\ ni16^post8 == 0 /\ -nx8^post8+nx8^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ ni11^0-ni11^post8 == 0 /\ nb^0-nb^post8 == 0 /\ na^0-na^post8 == 0), cost: 1 8: l1 -> l0 : na^0'=na^post9, nb^0'=nb^post9, nc^0'=nc^post9, ni11^0'=ni11^post9, ni16^0'=ni16^post9, ni21^0'=ni21^post9, nn^0'=nn^post9, np14^0'=np14^post9, np19^0'=np19^post9, np9^0'=np9^post9, npow___010^0'=npow___010^post9, npow___015^0'=npow___015^post9, npow___020^0'=npow___020^post9, nx13^0'=nx13^post9, nx18^0'=nx18^post9, nx8^0'=nx8^post9, ret_npow12^0'=ret_npow12^post9, ret_npow17^0'=ret_npow17^post9, ret_npow22^0'=ret_npow22^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, (0 == 0 /\ -np9^post9+np9^0 == 0 /\ -np14^post9+np14^0 == 0 /\ -npow___020^post9+npow___020^0 == 0 /\ tmp___1^0-tmp___1^post9 == 0 /\ nc^0-nc^post9 == 0 /\ -npow___015^post9+npow___015^0 == 0 /\ -ret_npow12^post9+ret_npow12^0 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ na^0-na^post9 == 0 /\ -ni16^post9+ni16^0 == 0 /\ 1+ni11^0-np9^0 <= 0 /\ -nx8^post9+nx8^0 == 0 /\ ret_npow17^0-ret_npow17^post9 == 0 /\ nx18^0-nx18^post9 == 0 /\ ni21^0-ni21^post9 == 0 /\ np19^0-np19^post9 == 0 /\ ret_npow22^0-ret_npow22^post9 == 0 /\ -nx13^post9+nx13^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ -nb^post9+nb^0 == 0 /\ -1-ni11^0+ni11^post9 == 0 /\ -nn^post9+nn^0 == 0), cost: 1 1: l2 -> l3 : na^0'=na^post2, nb^0'=nb^post2, nc^0'=nc^post2, ni11^0'=ni11^post2, ni16^0'=ni16^post2, ni21^0'=ni21^post2, nn^0'=nn^post2, np14^0'=np14^post2, np19^0'=np19^post2, np9^0'=np9^post2, npow___010^0'=npow___010^post2, npow___015^0'=npow___015^post2, npow___020^0'=npow___020^post2, nx13^0'=nx13^post2, nx18^0'=nx18^post2, nx8^0'=nx8^post2, ret_npow12^0'=ret_npow12^post2, ret_npow17^0'=ret_npow17^post2, ret_npow22^0'=ret_npow22^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (nc^0-nc^post2 == 0 /\ -np19^post2+np19^0 == 0 /\ -nb^post2+nb^0 == 0 /\ tmp___1^post2-ret_npow22^post2 == 0 /\ npow___020^0-npow___020^post2 == 0 /\ np14^0-np14^post2 == 0 /\ na^0-na^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -ni16^post2+ni16^0 == 0 /\ -ni21^0+np19^0 <= 0 /\ ni11^0-ni11^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ -nx8^post2+nx8^0 == 0 /\ ret_npow17^0-ret_npow17^post2 == 0 /\ nn^0-nn^post2 == 0 /\ ret_npow22^post2-npow___020^0 == 0 /\ ret_npow12^0-ret_npow12^post2 == 0 /\ np9^0-np9^post2 == 0 /\ -npow___015^post2+npow___015^0 == 0 /\ -npow___010^post2+npow___010^0 == 0 /\ ni21^0-ni21^post2 == 0 /\ nx13^0-nx13^post2 == 0 /\ -nx18^post2+nx18^0 == 0), cost: 1 2: l2 -> l4 : na^0'=na^post3, nb^0'=nb^post3, nc^0'=nc^post3, ni11^0'=ni11^post3, ni16^0'=ni16^post3, ni21^0'=ni21^post3, nn^0'=nn^post3, np14^0'=np14^post3, np19^0'=np19^post3, np9^0'=np9^post3, npow___010^0'=npow___010^post3, npow___015^0'=npow___015^post3, npow___020^0'=npow___020^post3, nx13^0'=nx13^post3, nx18^0'=nx18^post3, nx8^0'=nx8^post3, ret_npow12^0'=ret_npow12^post3, ret_npow17^0'=ret_npow17^post3, ret_npow22^0'=ret_npow22^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (0 == 0 /\ -nx13^post3+nx13^0 == 0 /\ -ret_npow22^post3+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ 1+ni21^0-np19^0 <= 0 /\ ni16^0-ni16^post3 == 0 /\ nx18^0-nx18^post3 == 0 /\ -np19^post3+np19^0 == 0 /\ ni11^0-ni11^post3 == 0 /\ np9^0-np9^post3 == 0 /\ ret_npow17^0-ret_npow17^post3 == 0 /\ ret_npow12^0-ret_npow12^post3 == 0 /\ -nc^post3+nc^0 == 0 /\ na^0-na^post3 == 0 /\ -nb^post3+nb^0 == 0 /\ -tmp___1^post3+tmp___1^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -nn^post3+nn^0 == 0 /\ -1+ni21^post3-ni21^0 == 0 /\ -nx8^post3+nx8^0 == 0 /\ -npow___015^post3+npow___015^0 == 0 /\ -np14^post3+np14^0 == 0), cost: 1 6: l4 -> l2 : na^0'=na^post7, nb^0'=nb^post7, nc^0'=nc^post7, ni11^0'=ni11^post7, ni16^0'=ni16^post7, ni21^0'=ni21^post7, nn^0'=nn^post7, np14^0'=np14^post7, np19^0'=np19^post7, np9^0'=np9^post7, npow___010^0'=npow___010^post7, npow___015^0'=npow___015^post7, npow___020^0'=npow___020^post7, nx13^0'=nx13^post7, nx18^0'=nx18^post7, nx8^0'=nx8^post7, ret_npow12^0'=ret_npow12^post7, ret_npow17^0'=ret_npow17^post7, ret_npow22^0'=ret_npow22^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, (-nb^post7+nb^0 == 0 /\ ret_npow12^0-ret_npow12^post7 == 0 /\ nc^0-nc^post7 == 0 /\ ret_npow17^0-ret_npow17^post7 == 0 /\ -ni16^post7+ni16^0 == 0 /\ na^0-na^post7 == 0 /\ -nx13^post7+nx13^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -npow___020^post7+npow___020^0 == 0 /\ ni11^0-ni11^post7 == 0 /\ -nn^post7+nn^0 == 0 /\ -nx8^post7+nx8^0 == 0 /\ np19^0-np19^post7 == 0 /\ -ret_npow22^post7+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ ni21^0-ni21^post7 == 0 /\ -np9^post7+np9^0 == 0 /\ -npow___015^post7+npow___015^0 == 0 /\ -nx18^post7+nx18^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ -np14^post7+np14^0 == 0), cost: 1 3: l5 -> l6 : na^0'=na^post4, nb^0'=nb^post4, nc^0'=nc^post4, ni11^0'=ni11^post4, ni16^0'=ni16^post4, ni21^0'=ni21^post4, nn^0'=nn^post4, np14^0'=np14^post4, np19^0'=np19^post4, np9^0'=np9^post4, npow___010^0'=npow___010^post4, npow___015^0'=npow___015^post4, npow___020^0'=npow___020^post4, nx13^0'=nx13^post4, nx18^0'=nx18^post4, nx8^0'=nx8^post4, ret_npow12^0'=ret_npow12^post4, ret_npow17^0'=ret_npow17^post4, ret_npow22^0'=ret_npow22^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (-tmp___1^post4+tmp___1^0 == 0 /\ -ret_npow22^post4+ret_npow22^0 == 0 /\ -ret_npow17^post4+ret_npow17^0 == 0 /\ ni16^0-ni16^post4 == 0 /\ -np14^post4+np14^0 == 0 /\ -np19^post4+np19^0 == 0 /\ npow___015^0-npow___015^post4 == 0 /\ np9^0-np9^post4 == 0 /\ -nx18^post4+nx18^0 == 0 /\ -nx8^post4+nx8^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ npow___010^0-npow___010^post4 == 0 /\ -nc^post4+nc^0 == 0 /\ -nx13^post4+nx13^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ nb^0-nb^post4 == 0 /\ ret_npow12^0-ret_npow12^post4 == 0 /\ -npow___020^post4+npow___020^0 == 0 /\ -ni21^post4+ni21^0 == 0 /\ ni11^0-ni11^post4 == 0 /\ -nn^post4+nn^0 == 0 /\ na^0-na^post4 == 0), cost: 1 4: l6 -> l4 : na^0'=na^post5, nb^0'=nb^post5, nc^0'=nc^post5, ni11^0'=ni11^post5, ni16^0'=ni16^post5, ni21^0'=ni21^post5, nn^0'=nn^post5, np14^0'=np14^post5, np19^0'=np19^post5, np9^0'=np9^post5, npow___010^0'=npow___010^post5, npow___015^0'=npow___015^post5, npow___020^0'=npow___020^post5, nx13^0'=nx13^post5, nx18^0'=nx18^post5, nx8^0'=nx8^post5, ret_npow12^0'=ret_npow12^post5, ret_npow17^0'=ret_npow17^post5, ret_npow22^0'=ret_npow22^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (-ni16^0+np14^0 <= 0 /\ ni11^0-ni11^post5 == 0 /\ ret_npow12^0-ret_npow12^post5 == 0 /\ ni21^post5 == 0 /\ ni16^0-ni16^post5 == 0 /\ -npow___015^post5+npow___015^0 == 0 /\ -nn^post5+nn^0 == 0 /\ -nx8^post5+nx8^0 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -np14^post5+np14^0 == 0 /\ nb^0-nb^post5 == 0 /\ na^0-na^post5 == 0 /\ ret_npow17^post5-npow___015^0 == 0 /\ -nx13^post5+nx13^0 == 0 /\ np9^0-np9^post5 == 0 /\ nx18^post5-nc^0 == 0 /\ np19^post5-nn^0 == 0 /\ -ret_npow17^post5+tmp___0^post5 == 0 /\ -ret_npow22^post5+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post5 == 0 /\ -1+npow___020^post5 == 0 /\ -nc^post5+nc^0 == 0), cost: 1 5: l6 -> l5 : na^0'=na^post6, nb^0'=nb^post6, nc^0'=nc^post6, ni11^0'=ni11^post6, ni16^0'=ni16^post6, ni21^0'=ni21^post6, nn^0'=nn^post6, np14^0'=np14^post6, np19^0'=np19^post6, np9^0'=np9^post6, npow___010^0'=npow___010^post6, npow___015^0'=npow___015^post6, npow___020^0'=npow___020^post6, nx13^0'=nx13^post6, nx18^0'=nx18^post6, nx8^0'=nx8^post6, ret_npow12^0'=ret_npow12^post6, ret_npow17^0'=ret_npow17^post6, ret_npow22^0'=ret_npow22^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (0 == 0 /\ -1+ni16^post6-ni16^0 == 0 /\ tmp^0-tmp^post6 == 0 /\ -nn^post6+nn^0 == 0 /\ -ret_npow22^post6+ret_npow22^0 == 0 /\ nx18^0-nx18^post6 == 0 /\ npow___010^0-npow___010^post6 == 0 /\ -tmp___1^post6+tmp___1^0 == 0 /\ -nx13^post6+nx13^0 == 0 /\ 1+ni16^0-np14^0 <= 0 /\ -npow___020^post6+npow___020^0 == 0 /\ -ni21^post6+ni21^0 == 0 /\ -ret_npow12^post6+ret_npow12^0 == 0 /\ -nx8^post6+nx8^0 == 0 /\ nb^0-nb^post6 == 0 /\ -nc^post6+nc^0 == 0 /\ -np14^post6+np14^0 == 0 /\ ret_npow17^0-ret_npow17^post6 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ ni11^0-ni11^post6 == 0 /\ np9^0-np9^post6 == 0 /\ na^0-na^post6 == 0 /\ np19^0-np19^post6 == 0), cost: 1 11: l8 -> l0 : na^0'=na^post10, nb^0'=nb^post10, nc^0'=nc^post10, ni11^0'=ni11^post10, ni16^0'=ni16^post10, ni21^0'=ni21^post10, nn^0'=nn^post10, np14^0'=np14^post10, np19^0'=np19^post10, np9^0'=np9^post10, npow___010^0'=npow___010^post10, npow___015^0'=npow___015^post10, npow___020^0'=npow___020^post10, nx13^0'=nx13^post10, nx18^0'=nx18^post10, nx8^0'=nx8^post10, ret_npow12^0'=ret_npow12^post10, ret_npow17^0'=ret_npow17^post10, ret_npow22^0'=ret_npow22^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, (ret_npow17^0-ret_npow17^post11 == 0 /\ tmp^post11-tmp^post10 == 0 /\ npow___020^post11-npow___020^post10 == 0 /\ ni11^post10 == 0 /\ nx18^0-nx18^post11 == 0 /\ nx13^post11-nx13^post10 == 0 /\ ret_npow22^post11-ret_npow22^post10 == 0 /\ ni21^post11-ni21^post10 == 0 /\ -ni16^post10+ni16^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ -ret_npow22^post11+ret_npow22^0 == 0 /\ np9^0-np9^post11 == 0 /\ -nx13^post11+nx13^0 == 0 /\ -ni21^post11+ni21^0 == 0 /\ -nc^post11+nc^0 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ ni16^0-ni16^post11 == 0 /\ ret_npow12^0-ret_npow12^post11 == 0 /\ -nn^post11+nn^0 == 0 /\ tmp___0^post11-tmp___0^post10 == 0 /\ ret_npow12^post11-ret_npow12^post10 == 0 /\ nc^post11-nc^post10 == 0 /\ npow___015^post11-npow___015^post10 == 0 /\ -nx18^post10+nx18^post11 == 0 /\ -nb^post10+nb^post11 == 0 /\ -nn^post10+np9^post10 == 0 /\ -np19^post11+np19^0 == 0 /\ -np14^post11+np14^0 == 0 /\ np19^post11-np19^post10 == 0 /\ -npow___020^post11+npow___020^0 == 0 /\ -1+npow___010^post10 == 0 /\ -npow___015^post11+npow___015^0 == 0 /\ npow___010^0-npow___010^post11 == 0 /\ nb^0-nb^post11 == 0 /\ tmp___1^post11-tmp___1^post10 == 0 /\ tmp^0-tmp^post11 == 0 /\ -na^post10+na^post11 == 0 /\ na^0-na^post11 == 0 /\ nx8^post10-na^post11 == 0 /\ -ret_npow17^post10+ret_npow17^post11 == 0 /\ ni11^0-ni11^post11 == 0 /\ -3+nn^post10 == 0 /\ -np14^post10+np14^post11 == 0 /\ -nx8^post11+nx8^0 == 0), cost: 1 Eliminating location l7 by chaining: Applied chaining First rule: l8 -> l7 : na^0'=na^post11, nb^0'=nb^post11, nc^0'=nc^post11, ni11^0'=ni11^post11, ni16^0'=ni16^post11, ni21^0'=ni21^post11, nn^0'=nn^post11, np14^0'=np14^post11, np19^0'=np19^post11, np9^0'=np9^post11, npow___010^0'=npow___010^post11, npow___015^0'=npow___015^post11, npow___020^0'=npow___020^post11, nx13^0'=nx13^post11, nx18^0'=nx18^post11, nx8^0'=nx8^post11, ret_npow12^0'=ret_npow12^post11, ret_npow17^0'=ret_npow17^post11, ret_npow22^0'=ret_npow22^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, (ret_npow17^0-ret_npow17^post11 == 0 /\ nx18^0-nx18^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ -ret_npow22^post11+ret_npow22^0 == 0 /\ np9^0-np9^post11 == 0 /\ -nx13^post11+nx13^0 == 0 /\ -ni21^post11+ni21^0 == 0 /\ -nc^post11+nc^0 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ ni16^0-ni16^post11 == 0 /\ ret_npow12^0-ret_npow12^post11 == 0 /\ -nn^post11+nn^0 == 0 /\ -np19^post11+np19^0 == 0 /\ -np14^post11+np14^0 == 0 /\ -npow___020^post11+npow___020^0 == 0 /\ -npow___015^post11+npow___015^0 == 0 /\ npow___010^0-npow___010^post11 == 0 /\ nb^0-nb^post11 == 0 /\ tmp^0-tmp^post11 == 0 /\ na^0-na^post11 == 0 /\ ni11^0-ni11^post11 == 0 /\ -nx8^post11+nx8^0 == 0), cost: 1 Second rule: l7 -> l0 : na^0'=na^post10, nb^0'=nb^post10, nc^0'=nc^post10, ni11^0'=ni11^post10, ni16^0'=ni16^post10, ni21^0'=ni21^post10, nn^0'=nn^post10, np14^0'=np14^post10, np19^0'=np19^post10, np9^0'=np9^post10, npow___010^0'=npow___010^post10, npow___015^0'=npow___015^post10, npow___020^0'=npow___020^post10, nx13^0'=nx13^post10, nx18^0'=nx18^post10, nx8^0'=nx8^post10, ret_npow12^0'=ret_npow12^post10, ret_npow17^0'=ret_npow17^post10, ret_npow22^0'=ret_npow22^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, (ni11^post10 == 0 /\ ret_npow12^0-ret_npow12^post10 == 0 /\ nc^0-nc^post10 == 0 /\ -npow___015^post10+npow___015^0 == 0 /\ -tmp___1^post10+tmp___1^0 == 0 /\ np19^0-np19^post10 == 0 /\ -ret_npow17^post10+ret_npow17^0 == 0 /\ -na^0+nx8^post10 == 0 /\ ni21^0-ni21^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ -ni16^post10+ni16^0 == 0 /\ na^0-na^post10 == 0 /\ -nn^post10+np9^post10 == 0 /\ -nx13^post10+nx13^0 == 0 /\ -nx18^post10+nx18^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -np14^post10+np14^0 == 0 /\ -nb^post10+nb^0 == 0 /\ -1+npow___010^post10 == 0 /\ -npow___020^post10+npow___020^0 == 0 /\ -3+nn^post10 == 0 /\ -ret_npow22^post10+ret_npow22^0 == 0), cost: 1 New rule: l8 -> l0 : na^0'=na^post10, nb^0'=nb^post10, nc^0'=nc^post10, ni11^0'=ni11^post10, ni16^0'=ni16^post10, ni21^0'=ni21^post10, nn^0'=nn^post10, np14^0'=np14^post10, np19^0'=np19^post10, np9^0'=np9^post10, npow___010^0'=npow___010^post10, npow___015^0'=npow___015^post10, npow___020^0'=npow___020^post10, nx13^0'=nx13^post10, nx18^0'=nx18^post10, nx8^0'=nx8^post10, ret_npow12^0'=ret_npow12^post10, ret_npow17^0'=ret_npow17^post10, ret_npow22^0'=ret_npow22^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, (ret_npow17^0-ret_npow17^post11 == 0 /\ tmp^post11-tmp^post10 == 0 /\ npow___020^post11-npow___020^post10 == 0 /\ ni11^post10 == 0 /\ nx18^0-nx18^post11 == 0 /\ nx13^post11-nx13^post10 == 0 /\ ret_npow22^post11-ret_npow22^post10 == 0 /\ ni21^post11-ni21^post10 == 0 /\ -ni16^post10+ni16^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ -ret_npow22^post11+ret_npow22^0 == 0 /\ np9^0-np9^post11 == 0 /\ -nx13^post11+nx13^0 == 0 /\ -ni21^post11+ni21^0 == 0 /\ -nc^post11+nc^0 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ ni16^0-ni16^post11 == 0 /\ ret_npow12^0-ret_npow12^post11 == 0 /\ -nn^post11+nn^0 == 0 /\ tmp___0^post11-tmp___0^post10 == 0 /\ ret_npow12^post11-ret_npow12^post10 == 0 /\ nc^post11-nc^post10 == 0 /\ npow___015^post11-npow___015^post10 == 0 /\ -nx18^post10+nx18^post11 == 0 /\ -nb^post10+nb^post11 == 0 /\ -nn^post10+np9^post10 == 0 /\ -np19^post11+np19^0 == 0 /\ -np14^post11+np14^0 == 0 /\ np19^post11-np19^post10 == 0 /\ -npow___020^post11+npow___020^0 == 0 /\ -1+npow___010^post10 == 0 /\ -npow___015^post11+npow___015^0 == 0 /\ npow___010^0-npow___010^post11 == 0 /\ nb^0-nb^post11 == 0 /\ tmp___1^post11-tmp___1^post10 == 0 /\ tmp^0-tmp^post11 == 0 /\ -na^post10+na^post11 == 0 /\ na^0-na^post11 == 0 /\ nx8^post10-na^post11 == 0 /\ -ret_npow17^post10+ret_npow17^post11 == 0 /\ ni11^0-ni11^post11 == 0 /\ -3+nn^post10 == 0 /\ -np14^post10+np14^post11 == 0 /\ -nx8^post11+nx8^0 == 0), cost: 1 Applied deletion Removed the following rules: 9 10 Simplified Transitions Start location: l8 Program variables: na^0 nb^0 nc^0 ni11^0 ni16^0 ni21^0 nn^0 np14^0 np19^0 np9^0 npow___010^0 npow___015^0 npow___020^0 nx13^0 nx18^0 nx8^0 ret_npow12^0 ret_npow17^0 ret_npow22^0 tmp^0 tmp___0^0 tmp___1^0 12: l0 -> l1 : T, cost: 1 19: l1 -> l5 : ni16^0'=0, np14^0'=nn^0, npow___015^0'=1, nx13^0'=nb^0, ret_npow12^0'=npow___010^0, tmp^0'=npow___010^0, -ni11^0+np9^0 <= 0, cost: 1 20: l1 -> l0 : ni11^0'=1+ni11^0, npow___010^0'=npow___010^post9, 1+ni11^0-np9^0 <= 0, cost: 1 13: l2 -> l3 : ret_npow22^0'=npow___020^0, tmp___1^0'=npow___020^0, -ni21^0+np19^0 <= 0, cost: 1 14: l2 -> l4 : ni21^0'=1+ni21^0, npow___020^0'=npow___020^post3, 1+ni21^0-np19^0 <= 0, cost: 1 18: l4 -> l2 : T, cost: 1 15: l5 -> l6 : T, cost: 1 16: l6 -> l4 : ni21^0'=0, np19^0'=nn^0, npow___020^0'=1, nx18^0'=nc^0, ret_npow17^0'=npow___015^0, tmp___0^0'=npow___015^0, -ni16^0+np14^0 <= 0, cost: 1 17: l6 -> l5 : ni16^0'=1+ni16^0, npow___015^0'=npow___015^post6, 1+ni16^0-np14^0 <= 0, cost: 1 21: l8 -> l0 : ni11^0'=0, nn^0'=3, np9^0'=3, npow___010^0'=1, nx8^0'=na^0, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : na^0'=na^post1, nb^0'=nb^post1, nc^0'=nc^post1, ni11^0'=ni11^post1, ni16^0'=ni16^post1, ni21^0'=ni21^post1, nn^0'=nn^post1, np14^0'=np14^post1, np19^0'=np19^post1, np9^0'=np9^post1, npow___010^0'=npow___010^post1, npow___015^0'=npow___015^post1, npow___020^0'=npow___020^post1, nx13^0'=nx13^post1, nx18^0'=nx18^post1, nx8^0'=nx8^post1, ret_npow12^0'=ret_npow12^post1, ret_npow17^0'=ret_npow17^post1, ret_npow22^0'=ret_npow22^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (tmp^0-tmp^post1 == 0 /\ tmp___0^0-tmp___0^post1 == 0 /\ ni11^0-ni11^post1 == 0 /\ -nx13^post1+nx13^0 == 0 /\ ni16^0-ni16^post1 == 0 /\ -nn^post1+nn^0 == 0 /\ np9^0-np9^post1 == 0 /\ ret_npow17^0-ret_npow17^post1 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -ni21^post1+ni21^0 == 0 /\ -nx8^post1+nx8^0 == 0 /\ nb^0-nb^post1 == 0 /\ na^0-na^post1 == 0 /\ -np14^post1+np14^0 == 0 /\ -np19^post1+np19^0 == 0 /\ -npow___015^post1+npow___015^0 == 0 /\ ret_npow12^0-ret_npow12^post1 == 0 /\ -npow___020^post1+npow___020^0 == 0 /\ npow___010^0-npow___010^post1 == 0 /\ -nc^post1+nc^0 == 0 /\ -ret_npow22^post1+ret_npow22^0 == 0 /\ -nx18^post1+nx18^0 == 0), cost: 1 New rule: l0 -> l1 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 propagated equality tmp^post1 = tmp^0 propagated equality tmp___0^post1 = tmp___0^0 propagated equality ni11^post1 = ni11^0 propagated equality nx13^post1 = nx13^0 propagated equality ni16^post1 = ni16^0 propagated equality nn^post1 = nn^0 propagated equality np9^post1 = np9^0 propagated equality ret_npow17^post1 = ret_npow17^0 propagated equality tmp___1^post1 = tmp___1^0 propagated equality ni21^post1 = ni21^0 propagated equality nx8^post1 = nx8^0 propagated equality nb^post1 = nb^0 propagated equality na^post1 = na^0 propagated equality np14^post1 = np14^0 propagated equality np19^post1 = np19^0 propagated equality npow___015^post1 = npow___015^0 propagated equality ret_npow12^post1 = ret_npow12^0 propagated equality npow___020^post1 = npow___020^0 propagated equality npow___010^post1 = npow___010^0 propagated equality nc^post1 = nc^0 propagated equality ret_npow22^post1 = ret_npow22^0 propagated equality nx18^post1 = nx18^0 Simplified Guard Original rule: l0 -> l1 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 New rule: l0 -> l1 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : na^0'=na^post2, nb^0'=nb^post2, nc^0'=nc^post2, ni11^0'=ni11^post2, ni16^0'=ni16^post2, ni21^0'=ni21^post2, nn^0'=nn^post2, np14^0'=np14^post2, np19^0'=np19^post2, np9^0'=np9^post2, npow___010^0'=npow___010^post2, npow___015^0'=npow___015^post2, npow___020^0'=npow___020^post2, nx13^0'=nx13^post2, nx18^0'=nx18^post2, nx8^0'=nx8^post2, ret_npow12^0'=ret_npow12^post2, ret_npow17^0'=ret_npow17^post2, ret_npow22^0'=ret_npow22^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (nc^0-nc^post2 == 0 /\ -np19^post2+np19^0 == 0 /\ -nb^post2+nb^0 == 0 /\ tmp___1^post2-ret_npow22^post2 == 0 /\ npow___020^0-npow___020^post2 == 0 /\ np14^0-np14^post2 == 0 /\ na^0-na^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -ni16^post2+ni16^0 == 0 /\ -ni21^0+np19^0 <= 0 /\ ni11^0-ni11^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ -nx8^post2+nx8^0 == 0 /\ ret_npow17^0-ret_npow17^post2 == 0 /\ nn^0-nn^post2 == 0 /\ ret_npow22^post2-npow___020^0 == 0 /\ ret_npow12^0-ret_npow12^post2 == 0 /\ np9^0-np9^post2 == 0 /\ -npow___015^post2+npow___015^0 == 0 /\ -npow___010^post2+npow___010^0 == 0 /\ ni21^0-ni21^post2 == 0 /\ nx13^0-nx13^post2 == 0 /\ -nx18^post2+nx18^0 == 0), cost: 1 New rule: l2 -> l3 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=npow___020^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=npow___020^0, (0 == 0 /\ -ni21^0+np19^0 <= 0), cost: 1 propagated equality nc^post2 = nc^0 propagated equality np19^post2 = np19^0 propagated equality nb^post2 = nb^0 propagated equality ret_npow22^post2 = tmp___1^post2 propagated equality npow___020^post2 = npow___020^0 propagated equality np14^post2 = np14^0 propagated equality na^post2 = na^0 propagated equality tmp^post2 = tmp^0 propagated equality ni16^post2 = ni16^0 propagated equality ni11^post2 = ni11^0 propagated equality tmp___0^post2 = tmp___0^0 propagated equality nx8^post2 = nx8^0 propagated equality ret_npow17^post2 = ret_npow17^0 propagated equality nn^post2 = nn^0 propagated equality tmp___1^post2 = npow___020^0 propagated equality ret_npow12^post2 = ret_npow12^0 propagated equality np9^post2 = np9^0 propagated equality npow___015^post2 = npow___015^0 propagated equality npow___010^post2 = npow___010^0 propagated equality ni21^post2 = ni21^0 propagated equality nx13^post2 = nx13^0 propagated equality nx18^post2 = nx18^0 Simplified Guard Original rule: l2 -> l3 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=npow___020^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=npow___020^0, (0 == 0 /\ -ni21^0+np19^0 <= 0), cost: 1 New rule: l2 -> l3 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=npow___020^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=npow___020^0, -ni21^0+np19^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=npow___020^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=npow___020^0, -ni21^0+np19^0 <= 0, cost: 1 New rule: l2 -> l3 : ret_npow22^0'=npow___020^0, tmp___1^0'=npow___020^0, -ni21^0+np19^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l4 : na^0'=na^post3, nb^0'=nb^post3, nc^0'=nc^post3, ni11^0'=ni11^post3, ni16^0'=ni16^post3, ni21^0'=ni21^post3, nn^0'=nn^post3, np14^0'=np14^post3, np19^0'=np19^post3, np9^0'=np9^post3, npow___010^0'=npow___010^post3, npow___015^0'=npow___015^post3, npow___020^0'=npow___020^post3, nx13^0'=nx13^post3, nx18^0'=nx18^post3, nx8^0'=nx8^post3, ret_npow12^0'=ret_npow12^post3, ret_npow17^0'=ret_npow17^post3, ret_npow22^0'=ret_npow22^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (0 == 0 /\ -nx13^post3+nx13^0 == 0 /\ -ret_npow22^post3+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ 1+ni21^0-np19^0 <= 0 /\ ni16^0-ni16^post3 == 0 /\ nx18^0-nx18^post3 == 0 /\ -np19^post3+np19^0 == 0 /\ ni11^0-ni11^post3 == 0 /\ np9^0-np9^post3 == 0 /\ ret_npow17^0-ret_npow17^post3 == 0 /\ ret_npow12^0-ret_npow12^post3 == 0 /\ -nc^post3+nc^0 == 0 /\ na^0-na^post3 == 0 /\ -nb^post3+nb^0 == 0 /\ -tmp___1^post3+tmp___1^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -nn^post3+nn^0 == 0 /\ -1+ni21^post3-ni21^0 == 0 /\ -nx8^post3+nx8^0 == 0 /\ -npow___015^post3+npow___015^0 == 0 /\ -np14^post3+np14^0 == 0), cost: 1 New rule: l2 -> l4 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=1+ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^post3, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+ni21^0-np19^0 <= 0), cost: 1 propagated equality nx13^post3 = nx13^0 propagated equality ret_npow22^post3 = ret_npow22^0 propagated equality npow___010^post3 = npow___010^0 propagated equality tmp^post3 = tmp^0 propagated equality ni16^post3 = ni16^0 propagated equality nx18^post3 = nx18^0 propagated equality np19^post3 = np19^0 propagated equality ni11^post3 = ni11^0 propagated equality np9^post3 = np9^0 propagated equality ret_npow17^post3 = ret_npow17^0 propagated equality ret_npow12^post3 = ret_npow12^0 propagated equality nc^post3 = nc^0 propagated equality na^post3 = na^0 propagated equality nb^post3 = nb^0 propagated equality tmp___1^post3 = tmp___1^0 propagated equality tmp___0^post3 = tmp___0^0 propagated equality nn^post3 = nn^0 propagated equality ni21^post3 = 1+ni21^0 propagated equality nx8^post3 = nx8^0 propagated equality npow___015^post3 = npow___015^0 propagated equality np14^post3 = np14^0 Simplified Guard Original rule: l2 -> l4 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=1+ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^post3, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+ni21^0-np19^0 <= 0), cost: 1 New rule: l2 -> l4 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=1+ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^post3, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 1+ni21^0-np19^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l4 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=1+ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^post3, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 1+ni21^0-np19^0 <= 0, cost: 1 New rule: l2 -> l4 : ni21^0'=1+ni21^0, npow___020^0'=npow___020^post3, 1+ni21^0-np19^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l6 : na^0'=na^post4, nb^0'=nb^post4, nc^0'=nc^post4, ni11^0'=ni11^post4, ni16^0'=ni16^post4, ni21^0'=ni21^post4, nn^0'=nn^post4, np14^0'=np14^post4, np19^0'=np19^post4, np9^0'=np9^post4, npow___010^0'=npow___010^post4, npow___015^0'=npow___015^post4, npow___020^0'=npow___020^post4, nx13^0'=nx13^post4, nx18^0'=nx18^post4, nx8^0'=nx8^post4, ret_npow12^0'=ret_npow12^post4, ret_npow17^0'=ret_npow17^post4, ret_npow22^0'=ret_npow22^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (-tmp___1^post4+tmp___1^0 == 0 /\ -ret_npow22^post4+ret_npow22^0 == 0 /\ -ret_npow17^post4+ret_npow17^0 == 0 /\ ni16^0-ni16^post4 == 0 /\ -np14^post4+np14^0 == 0 /\ -np19^post4+np19^0 == 0 /\ npow___015^0-npow___015^post4 == 0 /\ np9^0-np9^post4 == 0 /\ -nx18^post4+nx18^0 == 0 /\ -nx8^post4+nx8^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ npow___010^0-npow___010^post4 == 0 /\ -nc^post4+nc^0 == 0 /\ -nx13^post4+nx13^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ nb^0-nb^post4 == 0 /\ ret_npow12^0-ret_npow12^post4 == 0 /\ -npow___020^post4+npow___020^0 == 0 /\ -ni21^post4+ni21^0 == 0 /\ ni11^0-ni11^post4 == 0 /\ -nn^post4+nn^0 == 0 /\ na^0-na^post4 == 0), cost: 1 New rule: l5 -> l6 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 propagated equality tmp___1^post4 = tmp___1^0 propagated equality ret_npow22^post4 = ret_npow22^0 propagated equality ret_npow17^post4 = ret_npow17^0 propagated equality ni16^post4 = ni16^0 propagated equality np14^post4 = np14^0 propagated equality np19^post4 = np19^0 propagated equality npow___015^post4 = npow___015^0 propagated equality np9^post4 = np9^0 propagated equality nx18^post4 = nx18^0 propagated equality nx8^post4 = nx8^0 propagated equality tmp___0^post4 = tmp___0^0 propagated equality npow___010^post4 = npow___010^0 propagated equality nc^post4 = nc^0 propagated equality nx13^post4 = nx13^0 propagated equality tmp^post4 = tmp^0 propagated equality nb^post4 = nb^0 propagated equality ret_npow12^post4 = ret_npow12^0 propagated equality npow___020^post4 = npow___020^0 propagated equality ni21^post4 = ni21^0 propagated equality ni11^post4 = ni11^0 propagated equality nn^post4 = nn^0 propagated equality na^post4 = na^0 Simplified Guard Original rule: l5 -> l6 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 New rule: l5 -> l6 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 New rule: l5 -> l6 : T, cost: 1 Propagated Equalities Original rule: l6 -> l4 : na^0'=na^post5, nb^0'=nb^post5, nc^0'=nc^post5, ni11^0'=ni11^post5, ni16^0'=ni16^post5, ni21^0'=ni21^post5, nn^0'=nn^post5, np14^0'=np14^post5, np19^0'=np19^post5, np9^0'=np9^post5, npow___010^0'=npow___010^post5, npow___015^0'=npow___015^post5, npow___020^0'=npow___020^post5, nx13^0'=nx13^post5, nx18^0'=nx18^post5, nx8^0'=nx8^post5, ret_npow12^0'=ret_npow12^post5, ret_npow17^0'=ret_npow17^post5, ret_npow22^0'=ret_npow22^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (-ni16^0+np14^0 <= 0 /\ ni11^0-ni11^post5 == 0 /\ ret_npow12^0-ret_npow12^post5 == 0 /\ ni21^post5 == 0 /\ ni16^0-ni16^post5 == 0 /\ -npow___015^post5+npow___015^0 == 0 /\ -nn^post5+nn^0 == 0 /\ -nx8^post5+nx8^0 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -np14^post5+np14^0 == 0 /\ nb^0-nb^post5 == 0 /\ na^0-na^post5 == 0 /\ ret_npow17^post5-npow___015^0 == 0 /\ -nx13^post5+nx13^0 == 0 /\ np9^0-np9^post5 == 0 /\ nx18^post5-nc^0 == 0 /\ np19^post5-nn^0 == 0 /\ -ret_npow17^post5+tmp___0^post5 == 0 /\ -ret_npow22^post5+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post5 == 0 /\ -1+npow___020^post5 == 0 /\ -nc^post5+nc^0 == 0), cost: 1 New rule: l6 -> l4 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=nn^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=1, nx13^0'=nx13^0, nx18^0'=nc^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=npow___015^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=npow___015^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ -ni16^0+np14^0 <= 0), cost: 1 propagated equality ni11^post5 = ni11^0 propagated equality ret_npow12^post5 = ret_npow12^0 propagated equality ni21^post5 = 0 propagated equality ni16^post5 = ni16^0 propagated equality npow___015^post5 = npow___015^0 propagated equality nn^post5 = nn^0 propagated equality nx8^post5 = nx8^0 propagated equality tmp___1^post5 = tmp___1^0 propagated equality tmp^post5 = tmp^0 propagated equality np14^post5 = np14^0 propagated equality nb^post5 = nb^0 propagated equality na^post5 = na^0 propagated equality ret_npow17^post5 = npow___015^0 propagated equality nx13^post5 = nx13^0 propagated equality np9^post5 = np9^0 propagated equality nx18^post5 = nc^0 propagated equality np19^post5 = nn^0 propagated equality tmp___0^post5 = npow___015^0 propagated equality ret_npow22^post5 = ret_npow22^0 propagated equality npow___010^post5 = npow___010^0 propagated equality npow___020^post5 = 1 propagated equality nc^post5 = nc^0 Simplified Guard Original rule: l6 -> l4 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=nn^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=1, nx13^0'=nx13^0, nx18^0'=nc^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=npow___015^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=npow___015^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ -ni16^0+np14^0 <= 0), cost: 1 New rule: l6 -> l4 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=nn^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=1, nx13^0'=nx13^0, nx18^0'=nc^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=npow___015^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=npow___015^0, tmp___1^0'=tmp___1^0, -ni16^0+np14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l4 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=nn^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=1, nx13^0'=nx13^0, nx18^0'=nc^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=npow___015^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=npow___015^0, tmp___1^0'=tmp___1^0, -ni16^0+np14^0 <= 0, cost: 1 New rule: l6 -> l4 : ni21^0'=0, np19^0'=nn^0, npow___020^0'=1, nx18^0'=nc^0, ret_npow17^0'=npow___015^0, tmp___0^0'=npow___015^0, -ni16^0+np14^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l5 : na^0'=na^post6, nb^0'=nb^post6, nc^0'=nc^post6, ni11^0'=ni11^post6, ni16^0'=ni16^post6, ni21^0'=ni21^post6, nn^0'=nn^post6, np14^0'=np14^post6, np19^0'=np19^post6, np9^0'=np9^post6, npow___010^0'=npow___010^post6, npow___015^0'=npow___015^post6, npow___020^0'=npow___020^post6, nx13^0'=nx13^post6, nx18^0'=nx18^post6, nx8^0'=nx8^post6, ret_npow12^0'=ret_npow12^post6, ret_npow17^0'=ret_npow17^post6, ret_npow22^0'=ret_npow22^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (0 == 0 /\ -1+ni16^post6-ni16^0 == 0 /\ tmp^0-tmp^post6 == 0 /\ -nn^post6+nn^0 == 0 /\ -ret_npow22^post6+ret_npow22^0 == 0 /\ nx18^0-nx18^post6 == 0 /\ npow___010^0-npow___010^post6 == 0 /\ -tmp___1^post6+tmp___1^0 == 0 /\ -nx13^post6+nx13^0 == 0 /\ 1+ni16^0-np14^0 <= 0 /\ -npow___020^post6+npow___020^0 == 0 /\ -ni21^post6+ni21^0 == 0 /\ -ret_npow12^post6+ret_npow12^0 == 0 /\ -nx8^post6+nx8^0 == 0 /\ nb^0-nb^post6 == 0 /\ -nc^post6+nc^0 == 0 /\ -np14^post6+np14^0 == 0 /\ ret_npow17^0-ret_npow17^post6 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ ni11^0-ni11^post6 == 0 /\ np9^0-np9^post6 == 0 /\ na^0-na^post6 == 0 /\ np19^0-np19^post6 == 0), cost: 1 New rule: l6 -> l5 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=1+ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^post6, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+ni16^0-np14^0 <= 0), cost: 1 propagated equality ni16^post6 = 1+ni16^0 propagated equality tmp^post6 = tmp^0 propagated equality nn^post6 = nn^0 propagated equality ret_npow22^post6 = ret_npow22^0 propagated equality nx18^post6 = nx18^0 propagated equality npow___010^post6 = npow___010^0 propagated equality tmp___1^post6 = tmp___1^0 propagated equality nx13^post6 = nx13^0 propagated equality npow___020^post6 = npow___020^0 propagated equality ni21^post6 = ni21^0 propagated equality ret_npow12^post6 = ret_npow12^0 propagated equality nx8^post6 = nx8^0 propagated equality nb^post6 = nb^0 propagated equality nc^post6 = nc^0 propagated equality np14^post6 = np14^0 propagated equality ret_npow17^post6 = ret_npow17^0 propagated equality tmp___0^post6 = tmp___0^0 propagated equality ni11^post6 = ni11^0 propagated equality np9^post6 = np9^0 propagated equality na^post6 = na^0 propagated equality np19^post6 = np19^0 Simplified Guard Original rule: l6 -> l5 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=1+ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^post6, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+ni16^0-np14^0 <= 0), cost: 1 New rule: l6 -> l5 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=1+ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^post6, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 1+ni16^0-np14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l5 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=1+ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^post6, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 1+ni16^0-np14^0 <= 0, cost: 1 New rule: l6 -> l5 : ni16^0'=1+ni16^0, npow___015^0'=npow___015^post6, 1+ni16^0-np14^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l2 : na^0'=na^post7, nb^0'=nb^post7, nc^0'=nc^post7, ni11^0'=ni11^post7, ni16^0'=ni16^post7, ni21^0'=ni21^post7, nn^0'=nn^post7, np14^0'=np14^post7, np19^0'=np19^post7, np9^0'=np9^post7, npow___010^0'=npow___010^post7, npow___015^0'=npow___015^post7, npow___020^0'=npow___020^post7, nx13^0'=nx13^post7, nx18^0'=nx18^post7, nx8^0'=nx8^post7, ret_npow12^0'=ret_npow12^post7, ret_npow17^0'=ret_npow17^post7, ret_npow22^0'=ret_npow22^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, (-nb^post7+nb^0 == 0 /\ ret_npow12^0-ret_npow12^post7 == 0 /\ nc^0-nc^post7 == 0 /\ ret_npow17^0-ret_npow17^post7 == 0 /\ -ni16^post7+ni16^0 == 0 /\ na^0-na^post7 == 0 /\ -nx13^post7+nx13^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -npow___020^post7+npow___020^0 == 0 /\ ni11^0-ni11^post7 == 0 /\ -nn^post7+nn^0 == 0 /\ -nx8^post7+nx8^0 == 0 /\ np19^0-np19^post7 == 0 /\ -ret_npow22^post7+ret_npow22^0 == 0 /\ npow___010^0-npow___010^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ ni21^0-ni21^post7 == 0 /\ -np9^post7+np9^0 == 0 /\ -npow___015^post7+npow___015^0 == 0 /\ -nx18^post7+nx18^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ -np14^post7+np14^0 == 0), cost: 1 New rule: l4 -> l2 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 propagated equality nb^post7 = nb^0 propagated equality ret_npow12^post7 = ret_npow12^0 propagated equality nc^post7 = nc^0 propagated equality ret_npow17^post7 = ret_npow17^0 propagated equality ni16^post7 = ni16^0 propagated equality na^post7 = na^0 propagated equality nx13^post7 = nx13^0 propagated equality tmp___0^post7 = tmp___0^0 propagated equality npow___020^post7 = npow___020^0 propagated equality ni11^post7 = ni11^0 propagated equality nn^post7 = nn^0 propagated equality nx8^post7 = nx8^0 propagated equality np19^post7 = np19^0 propagated equality ret_npow22^post7 = ret_npow22^0 propagated equality npow___010^post7 = npow___010^0 propagated equality tmp___1^post7 = tmp___1^0 propagated equality ni21^post7 = ni21^0 propagated equality np9^post7 = np9^0 propagated equality npow___015^post7 = npow___015^0 propagated equality nx18^post7 = nx18^0 propagated equality tmp^post7 = tmp^0 propagated equality np14^post7 = np14^0 Simplified Guard Original rule: l4 -> l2 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 New rule: l4 -> l2 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l2 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 New rule: l4 -> l2 : T, cost: 1 Propagated Equalities Original rule: l1 -> l5 : na^0'=na^post8, nb^0'=nb^post8, nc^0'=nc^post8, ni11^0'=ni11^post8, ni16^0'=ni16^post8, ni21^0'=ni21^post8, nn^0'=nn^post8, np14^0'=np14^post8, np19^0'=np19^post8, np9^0'=np9^post8, npow___010^0'=npow___010^post8, npow___015^0'=npow___015^post8, npow___020^0'=npow___020^post8, nx13^0'=nx13^post8, nx18^0'=nx18^post8, nx8^0'=nx8^post8, ret_npow12^0'=ret_npow12^post8, ret_npow17^0'=ret_npow17^post8, ret_npow22^0'=ret_npow22^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, (-tmp___1^post8+tmp___1^0 == 0 /\ -ret_npow22^post8+ret_npow22^0 == 0 /\ -nn^0+np14^post8 == 0 /\ -1+npow___015^post8 == 0 /\ -npow___010^0+ret_npow12^post8 == 0 /\ npow___010^0-npow___010^post8 == 0 /\ -ni11^0+np9^0 <= 0 /\ nx18^0-nx18^post8 == 0 /\ -np19^post8+np19^0 == 0 /\ np9^0-np9^post8 == 0 /\ -npow___020^post8+npow___020^0 == 0 /\ nx13^post8-nb^0 == 0 /\ ret_npow17^0-ret_npow17^post8 == 0 /\ tmp^post8-ret_npow12^post8 == 0 /\ -nn^post8+nn^0 == 0 /\ -nc^post8+nc^0 == 0 /\ -ni21^post8+ni21^0 == 0 /\ ni16^post8 == 0 /\ -nx8^post8+nx8^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ ni11^0-ni11^post8 == 0 /\ nb^0-nb^post8 == 0 /\ na^0-na^post8 == 0), cost: 1 New rule: l1 -> l5 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=nn^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=1, npow___020^0'=npow___020^0, nx13^0'=nb^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=npow___010^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=npow___010^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ -ni11^0+np9^0 <= 0), cost: 1 propagated equality tmp___1^post8 = tmp___1^0 propagated equality ret_npow22^post8 = ret_npow22^0 propagated equality np14^post8 = nn^0 propagated equality npow___015^post8 = 1 propagated equality ret_npow12^post8 = npow___010^0 propagated equality npow___010^post8 = npow___010^0 propagated equality nx18^post8 = nx18^0 propagated equality np19^post8 = np19^0 propagated equality np9^post8 = np9^0 propagated equality npow___020^post8 = npow___020^0 propagated equality nx13^post8 = nb^0 propagated equality ret_npow17^post8 = ret_npow17^0 propagated equality tmp^post8 = npow___010^0 propagated equality nn^post8 = nn^0 propagated equality nc^post8 = nc^0 propagated equality ni21^post8 = ni21^0 propagated equality ni16^post8 = 0 propagated equality nx8^post8 = nx8^0 propagated equality tmp___0^post8 = tmp___0^0 propagated equality ni11^post8 = ni11^0 propagated equality nb^post8 = nb^0 propagated equality na^post8 = na^0 Simplified Guard Original rule: l1 -> l5 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=nn^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=1, npow___020^0'=npow___020^0, nx13^0'=nb^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=npow___010^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=npow___010^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ -ni11^0+np9^0 <= 0), cost: 1 New rule: l1 -> l5 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=nn^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=1, npow___020^0'=npow___020^0, nx13^0'=nb^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=npow___010^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=npow___010^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, -ni11^0+np9^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l5 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=ni11^0, ni16^0'=0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=nn^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^0, npow___015^0'=1, npow___020^0'=npow___020^0, nx13^0'=nb^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=npow___010^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=npow___010^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, -ni11^0+np9^0 <= 0, cost: 1 New rule: l1 -> l5 : ni16^0'=0, np14^0'=nn^0, npow___015^0'=1, nx13^0'=nb^0, ret_npow12^0'=npow___010^0, tmp^0'=npow___010^0, -ni11^0+np9^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l0 : na^0'=na^post9, nb^0'=nb^post9, nc^0'=nc^post9, ni11^0'=ni11^post9, ni16^0'=ni16^post9, ni21^0'=ni21^post9, nn^0'=nn^post9, np14^0'=np14^post9, np19^0'=np19^post9, np9^0'=np9^post9, npow___010^0'=npow___010^post9, npow___015^0'=npow___015^post9, npow___020^0'=npow___020^post9, nx13^0'=nx13^post9, nx18^0'=nx18^post9, nx8^0'=nx8^post9, ret_npow12^0'=ret_npow12^post9, ret_npow17^0'=ret_npow17^post9, ret_npow22^0'=ret_npow22^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, (0 == 0 /\ -np9^post9+np9^0 == 0 /\ -np14^post9+np14^0 == 0 /\ -npow___020^post9+npow___020^0 == 0 /\ tmp___1^0-tmp___1^post9 == 0 /\ nc^0-nc^post9 == 0 /\ -npow___015^post9+npow___015^0 == 0 /\ -ret_npow12^post9+ret_npow12^0 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ na^0-na^post9 == 0 /\ -ni16^post9+ni16^0 == 0 /\ 1+ni11^0-np9^0 <= 0 /\ -nx8^post9+nx8^0 == 0 /\ ret_npow17^0-ret_npow17^post9 == 0 /\ nx18^0-nx18^post9 == 0 /\ ni21^0-ni21^post9 == 0 /\ np19^0-np19^post9 == 0 /\ ret_npow22^0-ret_npow22^post9 == 0 /\ -nx13^post9+nx13^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ -nb^post9+nb^0 == 0 /\ -1-ni11^0+ni11^post9 == 0 /\ -nn^post9+nn^0 == 0), cost: 1 New rule: l1 -> l0 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=1+ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^post9, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+ni11^0-np9^0 <= 0), cost: 1 propagated equality np9^post9 = np9^0 propagated equality np14^post9 = np14^0 propagated equality npow___020^post9 = npow___020^0 propagated equality tmp___1^post9 = tmp___1^0 propagated equality nc^post9 = nc^0 propagated equality npow___015^post9 = npow___015^0 propagated equality ret_npow12^post9 = ret_npow12^0 propagated equality tmp___0^post9 = tmp___0^0 propagated equality na^post9 = na^0 propagated equality ni16^post9 = ni16^0 propagated equality nx8^post9 = nx8^0 propagated equality ret_npow17^post9 = ret_npow17^0 propagated equality nx18^post9 = nx18^0 propagated equality ni21^post9 = ni21^0 propagated equality np19^post9 = np19^0 propagated equality ret_npow22^post9 = ret_npow22^0 propagated equality nx13^post9 = nx13^0 propagated equality tmp^post9 = tmp^0 propagated equality nb^post9 = nb^0 propagated equality ni11^post9 = 1+ni11^0 propagated equality nn^post9 = nn^0 Simplified Guard Original rule: l1 -> l0 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=1+ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^post9, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+ni11^0-np9^0 <= 0), cost: 1 New rule: l1 -> l0 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=1+ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^post9, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 1+ni11^0-np9^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=1+ni11^0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=nn^0, np14^0'=np14^0, np19^0'=np19^0, np9^0'=np9^0, npow___010^0'=npow___010^post9, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=nx8^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 1+ni11^0-np9^0 <= 0, cost: 1 New rule: l1 -> l0 : ni11^0'=1+ni11^0, npow___010^0'=npow___010^post9, 1+ni11^0-np9^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l0 : na^0'=na^post10, nb^0'=nb^post10, nc^0'=nc^post10, ni11^0'=ni11^post10, ni16^0'=ni16^post10, ni21^0'=ni21^post10, nn^0'=nn^post10, np14^0'=np14^post10, np19^0'=np19^post10, np9^0'=np9^post10, npow___010^0'=npow___010^post10, npow___015^0'=npow___015^post10, npow___020^0'=npow___020^post10, nx13^0'=nx13^post10, nx18^0'=nx18^post10, nx8^0'=nx8^post10, ret_npow12^0'=ret_npow12^post10, ret_npow17^0'=ret_npow17^post10, ret_npow22^0'=ret_npow22^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, (ret_npow17^0-ret_npow17^post11 == 0 /\ tmp^post11-tmp^post10 == 0 /\ npow___020^post11-npow___020^post10 == 0 /\ ni11^post10 == 0 /\ nx18^0-nx18^post11 == 0 /\ nx13^post11-nx13^post10 == 0 /\ ret_npow22^post11-ret_npow22^post10 == 0 /\ ni21^post11-ni21^post10 == 0 /\ -ni16^post10+ni16^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ -ret_npow22^post11+ret_npow22^0 == 0 /\ np9^0-np9^post11 == 0 /\ -nx13^post11+nx13^0 == 0 /\ -ni21^post11+ni21^0 == 0 /\ -nc^post11+nc^0 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ ni16^0-ni16^post11 == 0 /\ ret_npow12^0-ret_npow12^post11 == 0 /\ -nn^post11+nn^0 == 0 /\ tmp___0^post11-tmp___0^post10 == 0 /\ ret_npow12^post11-ret_npow12^post10 == 0 /\ nc^post11-nc^post10 == 0 /\ npow___015^post11-npow___015^post10 == 0 /\ -nx18^post10+nx18^post11 == 0 /\ -nb^post10+nb^post11 == 0 /\ -nn^post10+np9^post10 == 0 /\ -np19^post11+np19^0 == 0 /\ -np14^post11+np14^0 == 0 /\ np19^post11-np19^post10 == 0 /\ -npow___020^post11+npow___020^0 == 0 /\ -1+npow___010^post10 == 0 /\ -npow___015^post11+npow___015^0 == 0 /\ npow___010^0-npow___010^post11 == 0 /\ nb^0-nb^post11 == 0 /\ tmp___1^post11-tmp___1^post10 == 0 /\ tmp^0-tmp^post11 == 0 /\ -na^post10+na^post11 == 0 /\ na^0-na^post11 == 0 /\ nx8^post10-na^post11 == 0 /\ -ret_npow17^post10+ret_npow17^post11 == 0 /\ ni11^0-ni11^post11 == 0 /\ -3+nn^post10 == 0 /\ -np14^post10+np14^post11 == 0 /\ -nx8^post11+nx8^0 == 0), cost: 1 New rule: l8 -> l0 : na^0'=na^post11, nb^0'=nb^post11, nc^0'=nc^post11, ni11^0'=0, ni16^0'=ni16^post11, ni21^0'=ni21^post11, nn^0'=3, np14^0'=np14^post11, np19^0'=np19^post11, np9^0'=3, npow___010^0'=1, npow___015^0'=npow___015^post11, npow___020^0'=npow___020^post11, nx13^0'=nx13^post11, nx18^0'=nx18^post11, nx8^0'=na^post11, ret_npow12^0'=ret_npow12^post11, ret_npow17^0'=ret_npow17^post11, ret_npow22^0'=ret_npow22^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, (0 == 0 /\ ret_npow17^0-ret_npow17^post11 == 0 /\ nx18^0-nx18^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ -ret_npow22^post11+ret_npow22^0 == 0 /\ np9^0-np9^post11 == 0 /\ -nx13^post11+nx13^0 == 0 /\ -ni21^post11+ni21^0 == 0 /\ -nc^post11+nc^0 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ ni16^0-ni16^post11 == 0 /\ ret_npow12^0-ret_npow12^post11 == 0 /\ -nn^post11+nn^0 == 0 /\ -np19^post11+np19^0 == 0 /\ -np14^post11+np14^0 == 0 /\ -npow___020^post11+npow___020^0 == 0 /\ -npow___015^post11+npow___015^0 == 0 /\ npow___010^0-npow___010^post11 == 0 /\ nb^0-nb^post11 == 0 /\ tmp^0-tmp^post11 == 0 /\ na^0-na^post11 == 0 /\ ni11^0-ni11^post11 == 0 /\ -nx8^post11+nx8^0 == 0), cost: 1 propagated equality tmp^post10 = tmp^post11 propagated equality npow___020^post10 = npow___020^post11 propagated equality ni11^post10 = 0 propagated equality nx13^post10 = nx13^post11 propagated equality ret_npow22^post10 = ret_npow22^post11 propagated equality ni21^post10 = ni21^post11 propagated equality ni16^post10 = ni16^post11 propagated equality tmp___0^post10 = tmp___0^post11 propagated equality ret_npow12^post10 = ret_npow12^post11 propagated equality nc^post10 = nc^post11 propagated equality npow___015^post10 = npow___015^post11 propagated equality nx18^post10 = nx18^post11 propagated equality nb^post10 = nb^post11 propagated equality nn^post10 = np9^post10 propagated equality np19^post10 = np19^post11 propagated equality npow___010^post10 = 1 propagated equality tmp___1^post10 = tmp___1^post11 propagated equality na^post10 = na^post11 propagated equality nx8^post10 = na^post11 propagated equality ret_npow17^post10 = ret_npow17^post11 propagated equality np9^post10 = 3 propagated equality np14^post10 = np14^post11 Propagated Equalities Original rule: l8 -> l0 : na^0'=na^post11, nb^0'=nb^post11, nc^0'=nc^post11, ni11^0'=0, ni16^0'=ni16^post11, ni21^0'=ni21^post11, nn^0'=3, np14^0'=np14^post11, np19^0'=np19^post11, np9^0'=3, npow___010^0'=1, npow___015^0'=npow___015^post11, npow___020^0'=npow___020^post11, nx13^0'=nx13^post11, nx18^0'=nx18^post11, nx8^0'=na^post11, ret_npow12^0'=ret_npow12^post11, ret_npow17^0'=ret_npow17^post11, ret_npow22^0'=ret_npow22^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, (0 == 0 /\ ret_npow17^0-ret_npow17^post11 == 0 /\ nx18^0-nx18^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ -ret_npow22^post11+ret_npow22^0 == 0 /\ np9^0-np9^post11 == 0 /\ -nx13^post11+nx13^0 == 0 /\ -ni21^post11+ni21^0 == 0 /\ -nc^post11+nc^0 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ ni16^0-ni16^post11 == 0 /\ ret_npow12^0-ret_npow12^post11 == 0 /\ -nn^post11+nn^0 == 0 /\ -np19^post11+np19^0 == 0 /\ -np14^post11+np14^0 == 0 /\ -npow___020^post11+npow___020^0 == 0 /\ -npow___015^post11+npow___015^0 == 0 /\ npow___010^0-npow___010^post11 == 0 /\ nb^0-nb^post11 == 0 /\ tmp^0-tmp^post11 == 0 /\ na^0-na^post11 == 0 /\ ni11^0-ni11^post11 == 0 /\ -nx8^post11+nx8^0 == 0), cost: 1 New rule: l8 -> l0 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=3, np14^0'=np14^0, np19^0'=np19^0, np9^0'=3, npow___010^0'=1, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=na^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 propagated equality ret_npow17^post11 = ret_npow17^0 propagated equality nx18^post11 = nx18^0 propagated equality tmp___0^post11 = tmp___0^0 propagated equality ret_npow22^post11 = ret_npow22^0 propagated equality np9^post11 = np9^0 propagated equality nx13^post11 = nx13^0 propagated equality ni21^post11 = ni21^0 propagated equality nc^post11 = nc^0 propagated equality tmp___1^post11 = tmp___1^0 propagated equality ni16^post11 = ni16^0 propagated equality ret_npow12^post11 = ret_npow12^0 propagated equality nn^post11 = nn^0 propagated equality np19^post11 = np19^0 propagated equality np14^post11 = np14^0 propagated equality npow___020^post11 = npow___020^0 propagated equality npow___015^post11 = npow___015^0 propagated equality npow___010^post11 = npow___010^0 propagated equality nb^post11 = nb^0 propagated equality tmp^post11 = tmp^0 propagated equality na^post11 = na^0 propagated equality ni11^post11 = ni11^0 propagated equality nx8^post11 = nx8^0 Simplified Guard Original rule: l8 -> l0 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=3, np14^0'=np14^0, np19^0'=np19^0, np9^0'=3, npow___010^0'=1, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=na^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 New rule: l8 -> l0 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=3, np14^0'=np14^0, np19^0'=np19^0, np9^0'=3, npow___010^0'=1, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=na^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l0 : na^0'=na^0, nb^0'=nb^0, nc^0'=nc^0, ni11^0'=0, ni16^0'=ni16^0, ni21^0'=ni21^0, nn^0'=3, np14^0'=np14^0, np19^0'=np19^0, np9^0'=3, npow___010^0'=1, npow___015^0'=npow___015^0, npow___020^0'=npow___020^0, nx13^0'=nx13^0, nx18^0'=nx18^0, nx8^0'=na^0, ret_npow12^0'=ret_npow12^0, ret_npow17^0'=ret_npow17^0, ret_npow22^0'=ret_npow22^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 New rule: l8 -> l0 : ni11^0'=0, nn^0'=3, np9^0'=3, npow___010^0'=1, nx8^0'=na^0, T, cost: 1 Step with 21 Trace 21[T] Blocked [{}, {}] Step with 12 Trace 21[T], 12[T] Blocked [{}, {}, {}] Step with 20 Trace 21[T], 12[T], 20[(1+ni11^0-np9^0 <= 0)] Blocked [{}, {}, {19[T]}, {}] Accelerate Start location: l8 Program variables: na^0 nb^0 nc^0 ni11^0 ni16^0 ni21^0 nn^0 np14^0 np19^0 np9^0 npow___010^0 npow___015^0 npow___020^0 nx13^0 nx18^0 nx8^0 ret_npow12^0 ret_npow17^0 ret_npow22^0 tmp^0 tmp___0^0 tmp___1^0 12: l0 -> l1 : T, cost: 1 22: l0 -> l0 : ni11^0'=ni11^0+n, npow___010^0'=npow___010^post9, (-ni11^0+np9^0-n >= 0 /\ -1+n >= 0), cost: 1 19: l1 -> l5 : ni16^0'=0, np14^0'=nn^0, npow___015^0'=1, nx13^0'=nb^0, ret_npow12^0'=npow___010^0, tmp^0'=npow___010^0, -ni11^0+np9^0 <= 0, cost: 1 20: l1 -> l0 : ni11^0'=1+ni11^0, npow___010^0'=npow___010^post9, 1+ni11^0-np9^0 <= 0, cost: 1 13: l2 -> l3 : ret_npow22^0'=npow___020^0, tmp___1^0'=npow___020^0, -ni21^0+np19^0 <= 0, cost: 1 14: l2 -> l4 : ni21^0'=1+ni21^0, npow___020^0'=npow___020^post3, 1+ni21^0-np19^0 <= 0, cost: 1 18: l4 -> l2 : T, cost: 1 15: l5 -> l6 : T, cost: 1 16: l6 -> l4 : ni21^0'=0, np19^0'=nn^0, npow___020^0'=1, nx18^0'=nc^0, ret_npow17^0'=npow___015^0, tmp___0^0'=npow___015^0, -ni16^0+np14^0 <= 0, cost: 1 17: l6 -> l5 : ni16^0'=1+ni16^0, npow___015^0'=npow___015^post6, 1+ni16^0-np14^0 <= 0, cost: 1 21: l8 -> l0 : ni11^0'=0, nn^0'=3, np9^0'=3, npow___010^0'=1, nx8^0'=na^0, T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : ni11^0'=1+ni11^0, npow___010^0'=npow___010^post9, 1+ni11^0-np9^0 <= 0, cost: 1 New rule: l0 -> l0 : ni11^0'=ni11^0+n, npow___010^0'=npow___010^post9, (-ni11^0+np9^0-n >= 0 /\ -1+n >= 0), cost: 1 -1-ni11^0+np9^0 >= 0 [0]: montonic decrease yields -ni11^0+np9^0-n >= 0 -1-ni11^0+np9^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-ni11^0+np9^0 >= 0) Replacement map: {-1-ni11^0+np9^0 >= 0 -> -ni11^0+np9^0-n >= 0} Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {22[T]}] Step with 12 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T] Blocked [{}, {}, {22[T]}, {}] Step with 20 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 20[(1+ni11^0-np9^0 <= 0)] Blocked [{}, {}, {22[T]}, {}, {}] Covered Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T] Blocked [{}, {}, {22[T]}, {20[T]}] Step with 19 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}] Step with 15 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 15[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {}] Step with 17 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 15[T], 17[(1+ni16^0-np14^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {16[T]}, {}] Accelerate Start location: l8 Program variables: na^0 nb^0 nc^0 ni11^0 ni16^0 ni21^0 nn^0 np14^0 np19^0 np9^0 npow___010^0 npow___015^0 npow___020^0 nx13^0 nx18^0 nx8^0 ret_npow12^0 ret_npow17^0 ret_npow22^0 tmp^0 tmp___0^0 tmp___1^0 12: l0 -> l1 : T, cost: 1 22: l0 -> l0 : ni11^0'=ni11^0+n, npow___010^0'=npow___010^post9, (-ni11^0+np9^0-n >= 0 /\ -1+n >= 0), cost: 1 19: l1 -> l5 : ni16^0'=0, np14^0'=nn^0, npow___015^0'=1, nx13^0'=nb^0, ret_npow12^0'=npow___010^0, tmp^0'=npow___010^0, -ni11^0+np9^0 <= 0, cost: 1 20: l1 -> l0 : ni11^0'=1+ni11^0, npow___010^0'=npow___010^post9, 1+ni11^0-np9^0 <= 0, cost: 1 13: l2 -> l3 : ret_npow22^0'=npow___020^0, tmp___1^0'=npow___020^0, -ni21^0+np19^0 <= 0, cost: 1 14: l2 -> l4 : ni21^0'=1+ni21^0, npow___020^0'=npow___020^post3, 1+ni21^0-np19^0 <= 0, cost: 1 18: l4 -> l2 : T, cost: 1 15: l5 -> l6 : T, cost: 1 23: l5 -> l5 : ni16^0'=ni16^0+n2, npow___015^0'=npow___015^post6, (-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0), cost: 1 16: l6 -> l4 : ni21^0'=0, np19^0'=nn^0, npow___020^0'=1, nx18^0'=nc^0, ret_npow17^0'=npow___015^0, tmp___0^0'=npow___015^0, -ni16^0+np14^0 <= 0, cost: 1 17: l6 -> l5 : ni16^0'=1+ni16^0, npow___015^0'=npow___015^post6, 1+ni16^0-np14^0 <= 0, cost: 1 21: l8 -> l0 : ni11^0'=0, nn^0'=3, np9^0'=3, npow___010^0'=1, nx8^0'=na^0, T, cost: 1 Loop Acceleration Original rule: l5 -> l5 : ni16^0'=1+ni16^0, npow___015^0'=npow___015^post6, 1+ni16^0-np14^0 <= 0, cost: 1 New rule: l5 -> l5 : ni16^0'=ni16^0+n2, npow___015^0'=npow___015^post6, (-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0), cost: 1 -1-ni16^0+np14^0 >= 0 [0]: montonic decrease yields -ni16^0-n2+np14^0 >= 0 -1-ni16^0+np14^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-ni16^0+np14^0 >= 0) Replacement map: {-1-ni16^0+np14^0 >= 0 -> -ni16^0-n2+np14^0 >= 0} Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}] Step with 15 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {}] Step with 17 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 17[(1+ni16^0-np14^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {}, {}] Covered Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}] Step with 16 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}] Step with 18 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 18[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {}] Step with 14 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 18[T], 14[(1+ni21^0-np19^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {13[T]}, {}] Accelerate Start location: l8 Program variables: na^0 nb^0 nc^0 ni11^0 ni16^0 ni21^0 nn^0 np14^0 np19^0 np9^0 npow___010^0 npow___015^0 npow___020^0 nx13^0 nx18^0 nx8^0 ret_npow12^0 ret_npow17^0 ret_npow22^0 tmp^0 tmp___0^0 tmp___1^0 12: l0 -> l1 : T, cost: 1 22: l0 -> l0 : ni11^0'=ni11^0+n, npow___010^0'=npow___010^post9, (-ni11^0+np9^0-n >= 0 /\ -1+n >= 0), cost: 1 19: l1 -> l5 : ni16^0'=0, np14^0'=nn^0, npow___015^0'=1, nx13^0'=nb^0, ret_npow12^0'=npow___010^0, tmp^0'=npow___010^0, -ni11^0+np9^0 <= 0, cost: 1 20: l1 -> l0 : ni11^0'=1+ni11^0, npow___010^0'=npow___010^post9, 1+ni11^0-np9^0 <= 0, cost: 1 13: l2 -> l3 : ret_npow22^0'=npow___020^0, tmp___1^0'=npow___020^0, -ni21^0+np19^0 <= 0, cost: 1 14: l2 -> l4 : ni21^0'=1+ni21^0, npow___020^0'=npow___020^post3, 1+ni21^0-np19^0 <= 0, cost: 1 18: l4 -> l2 : T, cost: 1 24: l4 -> l4 : ni21^0'=ni21^0+n3, npow___020^0'=npow___020^post3, (-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0), cost: 1 15: l5 -> l6 : T, cost: 1 23: l5 -> l5 : ni16^0'=ni16^0+n2, npow___015^0'=npow___015^post6, (-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0), cost: 1 16: l6 -> l4 : ni21^0'=0, np19^0'=nn^0, npow___020^0'=1, nx18^0'=nc^0, ret_npow17^0'=npow___015^0, tmp___0^0'=npow___015^0, -ni16^0+np14^0 <= 0, cost: 1 17: l6 -> l5 : ni16^0'=1+ni16^0, npow___015^0'=npow___015^post6, 1+ni16^0-np14^0 <= 0, cost: 1 21: l8 -> l0 : ni11^0'=0, nn^0'=3, np9^0'=3, npow___010^0'=1, nx8^0'=na^0, T, cost: 1 Loop Acceleration Original rule: l4 -> l4 : ni21^0'=1+ni21^0, npow___020^0'=npow___020^post3, 1+ni21^0-np19^0 <= 0, cost: 1 New rule: l4 -> l4 : ni21^0'=ni21^0+n3, npow___020^0'=npow___020^post3, (-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0), cost: 1 -1-ni21^0+np19^0 >= 0 [0]: montonic decrease yields -ni21^0+np19^0-n3 >= 0 -1-ni21^0+np19^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-ni21^0+np19^0 >= 0) Replacement map: {-1-ni21^0+np19^0 >= 0 -> -ni21^0+np19^0-n3 >= 0} Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 24[(-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {24[T]}] Step with 18 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 24[(-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0)], 18[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {24[T]}, {}] Step with 14 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 24[(-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0)], 18[T], 14[(1+ni21^0-np19^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {24[T]}, {}, {}] Covered Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 24[(-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0)], 18[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {24[T]}, {14[T]}] Step with 13 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 24[(-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0)], 18[T], 13[(-ni21^0+np19^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {24[T]}, {14[T]}, {}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 24[(-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0)], 18[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {24[T]}, {13[T], 14[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 24[(-1+n3 >= 0 /\ -ni21^0+np19^0-n3 >= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {}, {18[T], 24[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {24[T]}] Step with 18 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 18[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {24[T]}, {}] Step with 14 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 18[T], 14[(1+ni21^0-np19^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {24[T]}, {13[T]}, {}] Covered Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)], 18[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {24[T]}, {13[T], 14[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T], 16[(-ni16^0+np14^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {17[T]}, {18[T], 24[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)], 15[T] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {23[T]}, {16[T], 17[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 23[(-1+n2 >= 0 /\ -ni16^0-n2+np14^0 >= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {}, {15[T], 23[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {23[T]}] Step with 15 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 15[T] Blocked [{}, {}, {22[T]}, {20[T]}, {23[T]}, {}] Step with 17 Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 15[T], 17[(1+ni16^0-np14^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {23[T]}, {16[T]}, {}] Covered Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)], 15[T] Blocked [{}, {}, {22[T]}, {20[T]}, {23[T]}, {16[T], 17[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T], 19[(-ni11^0+np9^0 <= 0)] Blocked [{}, {}, {22[T]}, {20[T]}, {15[T], 23[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)], 12[T] Blocked [{}, {}, {22[T]}, {19[T], 20[T]}] Backtrack Trace 21[T], 22[(-ni11^0+np9^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {12[T], 22[T]}] Backtrack Trace 21[T] Blocked [{}, {22[T]}] Step with 12 Trace 21[T], 12[T] Blocked [{}, {22[T]}, {}] Step with 20 Trace 21[T], 12[T], 20[(1+ni11^0-np9^0 <= 0)] Blocked [{}, {22[T]}, {19[T]}, {}] Covered Trace 21[T], 12[T] Blocked [{}, {22[T]}, {19[T], 20[T]}] Backtrack Trace 21[T] Blocked [{}, {12[T], 22[T]}] Backtrack Trace Blocked [{21[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b