NO Initial ITS Start location: l8 0: l0 -> l1 : x_5^0'=x_5^post0, Result_4^0'=Result_4^post0, (-Result_4^post0+Result_4^0 == 0 /\ -x_5^post0+x_5^0 == 0), cost: 1 1: l1 -> l2 : x_5^0'=x_5^post1, Result_4^0'=Result_4^post1, (x_5^0 <= 0 /\ Result_4^0-Result_4^post1 == 0 /\ x_5^0-x_5^post1 == 0 /\ -x_5^0 <= 0), cost: 1 2: l1 -> l2 : x_5^0'=x_5^post2, Result_4^0'=Result_4^post2, (0 == 0 /\ -x_5^post2 <= 0 /\ x_5^post2 <= 0 /\ Result_4^0-Result_4^post2 == 0 /\ -x_5^0 <= 0 /\ -1+x_5^post2-x_5^10 == 0 /\ 1-x_5^0 <= 0), cost: 1 3: l1 -> l2 : x_5^0'=x_5^post3, Result_4^0'=Result_4^post3, (0 == 0 /\ x_5^post3 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^post3-x_5^11 == 0 /\ -x_5^post3 <= 0 /\ -Result_4^post3+Result_4^0 == 0), cost: 1 4: l1 -> l3 : x_5^0'=x_5^post4, Result_4^0'=Result_4^post4, (0 == 0 /\ -1-x_5^12+x_5^20 == 0 /\ -x_5^0 <= 0 /\ 1-x_5^20 <= 0 /\ 1-x_5^0 <= 0 /\ -1+x_5^post4-x_5^30 == 0 /\ -x_5^20 <= 0 /\ -Result_4^post4+Result_4^0 == 0), cost: 1 6: l1 -> l4 : x_5^0'=x_5^post6, Result_4^0'=Result_4^post6, (0 == 0 /\ Result_4^0-Result_4^post6 == 0 /\ -x_5^0 <= 0 /\ 1-x_5^0 <= 0 /\ 1+x_5^post6-x_5^310 == 0 /\ 1+x_5^210 <= 0 /\ -1-x_5^13+x_5^210 == 0), cost: 1 8: l1 -> l5 : x_5^0'=x_5^post8, Result_4^0'=Result_4^post8, (0 == 0 /\ -x_5^220 <= 0 /\ 1-x_5^220 <= 0 /\ -1+x_5^post8-x_5^320 == 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^14+x_5^220 == 0 /\ Result_4^0-Result_4^post8 == 0), cost: 1 10: l1 -> l6 : x_5^0'=x_5^post10, Result_4^0'=Result_4^post10, (0 == 0 /\ 1+x_5^230-x_5^15 == 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^230 <= 0 /\ 1+x_5^post10-x_5^330 == 0 /\ -Result_4^post10+Result_4^0 == 0), cost: 1 12: l2 -> l7 : x_5^0'=x_5^post12, Result_4^0'=Result_4^post12, (0 == 0 /\ x_5^0-x_5^post12 == 0), cost: 1 5: l3 -> l1 : x_5^0'=x_5^post5, Result_4^0'=Result_4^post5, (Result_4^0-Result_4^post5 == 0 /\ x_5^0-x_5^post5 == 0), cost: 1 7: l4 -> l1 : x_5^0'=x_5^post7, Result_4^0'=Result_4^post7, (Result_4^0-Result_4^post7 == 0 /\ x_5^0-x_5^post7 == 0), cost: 1 9: l5 -> l1 : x_5^0'=x_5^post9, Result_4^0'=Result_4^post9, (x_5^0-x_5^post9 == 0 /\ -Result_4^post9+Result_4^0 == 0), cost: 1 11: l6 -> l1 : x_5^0'=x_5^post11, Result_4^0'=Result_4^post11, (x_5^0-x_5^post11 == 0 /\ -Result_4^post11+Result_4^0 == 0), cost: 1 13: l8 -> l0 : x_5^0'=x_5^post13, Result_4^0'=Result_4^post13, (-Result_4^post13+Result_4^0 == 0 /\ -x_5^post13+x_5^0 == 0), cost: 1 Removed unreachable rules and leafs Start location: l8 0: l0 -> l1 : x_5^0'=x_5^post0, Result_4^0'=Result_4^post0, (-Result_4^post0+Result_4^0 == 0 /\ -x_5^post0+x_5^0 == 0), cost: 1 4: l1 -> l3 : x_5^0'=x_5^post4, Result_4^0'=Result_4^post4, (0 == 0 /\ -1-x_5^12+x_5^20 == 0 /\ -x_5^0 <= 0 /\ 1-x_5^20 <= 0 /\ 1-x_5^0 <= 0 /\ -1+x_5^post4-x_5^30 == 0 /\ -x_5^20 <= 0 /\ -Result_4^post4+Result_4^0 == 0), cost: 1 6: l1 -> l4 : x_5^0'=x_5^post6, Result_4^0'=Result_4^post6, (0 == 0 /\ Result_4^0-Result_4^post6 == 0 /\ -x_5^0 <= 0 /\ 1-x_5^0 <= 0 /\ 1+x_5^post6-x_5^310 == 0 /\ 1+x_5^210 <= 0 /\ -1-x_5^13+x_5^210 == 0), cost: 1 8: l1 -> l5 : x_5^0'=x_5^post8, Result_4^0'=Result_4^post8, (0 == 0 /\ -x_5^220 <= 0 /\ 1-x_5^220 <= 0 /\ -1+x_5^post8-x_5^320 == 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^14+x_5^220 == 0 /\ Result_4^0-Result_4^post8 == 0), cost: 1 10: l1 -> l6 : x_5^0'=x_5^post10, Result_4^0'=Result_4^post10, (0 == 0 /\ 1+x_5^230-x_5^15 == 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^230 <= 0 /\ 1+x_5^post10-x_5^330 == 0 /\ -Result_4^post10+Result_4^0 == 0), cost: 1 5: l3 -> l1 : x_5^0'=x_5^post5, Result_4^0'=Result_4^post5, (Result_4^0-Result_4^post5 == 0 /\ x_5^0-x_5^post5 == 0), cost: 1 7: l4 -> l1 : x_5^0'=x_5^post7, Result_4^0'=Result_4^post7, (Result_4^0-Result_4^post7 == 0 /\ x_5^0-x_5^post7 == 0), cost: 1 9: l5 -> l1 : x_5^0'=x_5^post9, Result_4^0'=Result_4^post9, (x_5^0-x_5^post9 == 0 /\ -Result_4^post9+Result_4^0 == 0), cost: 1 11: l6 -> l1 : x_5^0'=x_5^post11, Result_4^0'=Result_4^post11, (x_5^0-x_5^post11 == 0 /\ -Result_4^post11+Result_4^0 == 0), cost: 1 13: l8 -> l0 : x_5^0'=x_5^post13, Result_4^0'=Result_4^post13, (-Result_4^post13+Result_4^0 == 0 /\ -x_5^post13+x_5^0 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : x_5^0'=x_5^post0, Result_4^0'=Result_4^post0, (-Result_4^post0+Result_4^0 == 0 /\ -x_5^post0+x_5^0 == 0), cost: 1 New rule: l0 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l3 : x_5^0'=x_5^post4, Result_4^0'=Result_4^post4, (0 == 0 /\ -1-x_5^12+x_5^20 == 0 /\ -x_5^0 <= 0 /\ 1-x_5^20 <= 0 /\ 1-x_5^0 <= 0 /\ -1+x_5^post4-x_5^30 == 0 /\ -x_5^20 <= 0 /\ -Result_4^post4+Result_4^0 == 0), cost: 1 New rule: l1 -> l3 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 1 Applied preprocessing Original rule: l3 -> l1 : x_5^0'=x_5^post5, Result_4^0'=Result_4^post5, (Result_4^0-Result_4^post5 == 0 /\ x_5^0-x_5^post5 == 0), cost: 1 New rule: l3 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l4 : x_5^0'=x_5^post6, Result_4^0'=Result_4^post6, (0 == 0 /\ Result_4^0-Result_4^post6 == 0 /\ -x_5^0 <= 0 /\ 1-x_5^0 <= 0 /\ 1+x_5^post6-x_5^310 == 0 /\ 1+x_5^210 <= 0 /\ -1-x_5^13+x_5^210 == 0), cost: 1 New rule: l1 -> l4 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 1 Applied preprocessing Original rule: l4 -> l1 : x_5^0'=x_5^post7, Result_4^0'=Result_4^post7, (Result_4^0-Result_4^post7 == 0 /\ x_5^0-x_5^post7 == 0), cost: 1 New rule: l4 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l5 : x_5^0'=x_5^post8, Result_4^0'=Result_4^post8, (0 == 0 /\ -x_5^220 <= 0 /\ 1-x_5^220 <= 0 /\ -1+x_5^post8-x_5^320 == 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^14+x_5^220 == 0 /\ Result_4^0-Result_4^post8 == 0), cost: 1 New rule: l1 -> l5 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 1 Applied preprocessing Original rule: l5 -> l1 : x_5^0'=x_5^post9, Result_4^0'=Result_4^post9, (x_5^0-x_5^post9 == 0 /\ -Result_4^post9+Result_4^0 == 0), cost: 1 New rule: l5 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l6 : x_5^0'=x_5^post10, Result_4^0'=Result_4^post10, (0 == 0 /\ 1+x_5^230-x_5^15 == 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^230 <= 0 /\ 1+x_5^post10-x_5^330 == 0 /\ -Result_4^post10+Result_4^0 == 0), cost: 1 New rule: l1 -> l6 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 1 Applied preprocessing Original rule: l6 -> l1 : x_5^0'=x_5^post11, Result_4^0'=Result_4^post11, (x_5^0-x_5^post11 == 0 /\ -Result_4^post11+Result_4^0 == 0), cost: 1 New rule: l6 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l8 -> l0 : x_5^0'=x_5^post13, Result_4^0'=Result_4^post13, (-Result_4^post13+Result_4^0 == 0 /\ -x_5^post13+x_5^0 == 0), cost: 1 New rule: l8 -> l0 : TRUE, cost: 1 Simplified rules Start location: l8 14: l0 -> l1 : TRUE, cost: 1 15: l1 -> l3 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 1 17: l1 -> l4 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 1 19: l1 -> l5 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 1 21: l1 -> l6 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 1 16: l3 -> l1 : TRUE, cost: 1 18: l4 -> l1 : TRUE, cost: 1 20: l5 -> l1 : TRUE, cost: 1 22: l6 -> l1 : TRUE, cost: 1 23: l8 -> l0 : TRUE, cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l8 -> l0 : TRUE, cost: 1 Second rule: l0 -> l1 : TRUE, cost: 1 New rule: l8 -> l1 : TRUE, cost: 2 Applied deletion Removed the following rules: 14 23 Eliminating location l3 by chaining: Applied chaining First rule: l1 -> l3 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 1 Second rule: l3 -> l1 : TRUE, cost: 1 New rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Applied deletion Removed the following rules: 15 16 Eliminating location l4 by chaining: Applied chaining First rule: l1 -> l4 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 1 Second rule: l4 -> l1 : TRUE, cost: 1 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Applied deletion Removed the following rules: 17 18 Eliminating location l5 by chaining: Applied chaining First rule: l1 -> l5 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 1 Second rule: l5 -> l1 : TRUE, cost: 1 New rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Applied deletion Removed the following rules: 19 20 Eliminating location l6 by chaining: Applied chaining First rule: l1 -> l6 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 1 Second rule: l6 -> l1 : TRUE, cost: 1 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Applied deletion Removed the following rules: 21 22 Eliminated locations on linear paths Start location: l8 25: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 26: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 27: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 28: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 24: l8 -> l1 : TRUE, cost: 2 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_ILCLDJ.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_CmdCjN.txt Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_dFDIHL.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_eIfEBh.txt Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^320 >= 0), cost: 2*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_acbegO.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_HFjeJp.txt Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_kfdgKK.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_BhEHPe.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1-x_5^0 >= 0 /\ -1+n3 >= 0 /\ -2-x_5^320 >= 0), cost: 4*n3 Sub-proof via acceration calculus written to file:///tmp/tmpnam_EmDEdM.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_cEfgCb.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ 1+x_5^0 <= 0 /\ -2-x_5^320 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, 1+x_5^0 <= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+n4 >= 0 /\ -1-x_5^0 >= 0 /\ -x_5^310 >= 0), cost: 4*n4 Sub-proof via acceration calculus written to file:///tmp/tmpnam_jCbOJJ.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^310 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_cEPHFF.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^310 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -x_5^310 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^30, 1+x_5^0 <= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n5 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^30 >= 0), cost: 4*n5 Sub-proof via acceration calculus written to file:///tmp/tmpnam_hDbCJJ.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> [9] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_IHBlCJ.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [9] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -2-x_5^30 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-x_5^330 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n6 >= 0), cost: 4*n6 Sub-proof via acceration calculus written to file:///tmp/tmpnam_AJlbAk.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_eKNenB.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, 1+x_5^0 <= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1-x_5^0 >= 0 /\ -x_5^310 >= 0 /\ -1+n7 >= 0), cost: 4*n7 Sub-proof via acceration calculus written to file:///tmp/tmpnam_cJfMCO.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^310 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_IGjoJj.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^310 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -x_5^310 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^30, 1+x_5^0 <= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1-x_5^0 >= 0 /\ -2-x_5^30 >= 0 /\ -1+n8 >= 0), cost: 4*n8 Sub-proof via acceration calculus written to file:///tmp/tmpnam_NOlbln.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> [9] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_KdNOcA.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [9] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -2-x_5^30 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, -1+x_5^0 >= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n9 >= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^330 >= 0), cost: 4*n9 Sub-proof via acceration calculus written to file:///tmp/tmpnam_kGCfNP.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^330 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_fggbMg.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^330 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^330 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^320, -1+x_5^0 >= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^320, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (x_5^320 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n10 >= 0), cost: 4*n10 Sub-proof via acceration calculus written to file:///tmp/tmpnam_BFNMcB.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^320, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^320 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_ncnchA.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^320 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ 1+x_5^0 <= 0 /\ x_5^320 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n11 >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 4*n11 Sub-proof via acceration calculus written to file:///tmp/tmpnam_mJcCMM.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_GcFnka.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, -1+x_5^0 >= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n12 >= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^330 >= 0), cost: 4*n12 Sub-proof via acceration calculus written to file:///tmp/tmpnam_ldDlkM.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^330 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_HBaBpL.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^330 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^330 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^320, -1+x_5^0 >= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^320, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (x_5^320 >= 0 /\ -1+n13 >= 0 /\ -1+x_5^0 >= 0), cost: 4*n13 Sub-proof via acceration calculus written to file:///tmp/tmpnam_PdODoG.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^320, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^320 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_ELfdNO.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^320 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ 1+x_5^0 <= 0 /\ x_5^320 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n14 >= 0), cost: 4*n14 Sub-proof via acceration calculus written to file:///tmp/tmpnam_LaHkGf.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_GFLOmn.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -2+x_5^310 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^320 >= 0), cost: 2*n1 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n1 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n1 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n17 >= 0 /\ -2-x_5^320 >= 0), cost: 2*n17+2*n17*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_klfdkb.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n1 New rule: l1 -> [9] : (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0 /\ -2-x_5^320 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_biNEAo.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^320 >= 0), cost: 2*n1 Second rule: l1 -> [9] : (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0 /\ -2-x_5^320 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^320 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^320 >= 0), cost: 2*n1 Second rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n1 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n1 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n1 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n1 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-x_5^330 >= 0 /\ -1+n18 >= 0 /\ -1+n1 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n1*n18+2*n18 Sub-proof via acceration calculus written to file:///tmp/tmpnam_oKJapg.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n1 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n1 New rule: l1 -> [9] : (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_PKAbAJ.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [9] : (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -x_5^330 >= 0 /\ -1+n1 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n2 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: 2+2*n2 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: 2+2*n2 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n21 >= 0), cost: 2*n21+2*n2*n21 Sub-proof via acceration calculus written to file:///tmp/tmpnam_iJKKMn.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: 2+2*n2 New rule: l1 -> [9] : (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_ECCbkM.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n2 Second rule: l1 -> [9] : (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n2 Second rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n2 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n2 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n2 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n2 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n2 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n22 >= 0 /\ -2-x_5^320 >= 0), cost: 2*n22+2*n22*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_meeejd.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n2 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n2 New rule: l1 -> [9] : (-1+n2 >= 0 /\ -1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_jLAnLJ.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^320, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [9] : (-1+n2 >= 0 /\ -1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ -2-x_5^320 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2*n New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2+2*n Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2+2*n New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0 /\ -1+n23 >= 0), cost: 2*n23*n+2*n23 Sub-proof via acceration calculus written to file:///tmp/tmpnam_GHmmhA.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2+2*n New rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_LGffkO.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2*n Second rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2*n Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+n >= 0 /\ -1+x_5^0 >= 0), cost: 2+2*n Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+n >= 0 /\ -1+x_5^0 >= 0), cost: 2+2*n New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+n24 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: 2*n*n24+2*n24 Sub-proof via acceration calculus written to file:///tmp/tmpnam_fEOmpE.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+n >= 0 /\ -1+x_5^0 >= 0), cost: 2+2*n New rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_Iiiaji.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -2+x_5^310 >= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n27 >= 0 /\ -1+n0 >= 0), cost: 2*n27+2*n27*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_gncfHN.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 New rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ 1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_mNHDIa.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 Second rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ 1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n28 >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0 /\ -1+n0 >= 0), cost: 2*n0*n28+2*n28 Sub-proof via acceration calculus written to file:///tmp/tmpnam_JNNjOm.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 New rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_pOKGMk.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [9] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0 /\ -1+n0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^320 >= 0), cost: 2*n1 New rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: 2*n1 Applied simplification Original rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM New rule: l1 -> [9] : (1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n2 New rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: 2*n2 Applied simplification Original rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l1 -> [9] : (1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ 1+x_5^0 <= 0 /\ -2-x_5^320 >= 0), cost: NONTERM New rule: l1 -> [9] : (2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (-1-x_5^0 >= 0 /\ -1-x_5^0+x_5^310 <= 0), cost: NONTERM New rule: l1 -> [9] : (1+x_5^0 <= 0 /\ -1-x_5^0+x_5^310 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -x_5^310 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^310 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -2-x_5^30 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (2+x_5^30 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [9] : (1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^330 >= 0), cost: NONTERM New rule: l1 -> [9] : (1+x_5^0 <= 0 /\ -2+x_5^330 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ 1+x_5^0 <= 0 /\ x_5^320 >= 0), cost: NONTERM New rule: l1 -> [9] : (1+x_5^0 <= 0 /\ x_5^320 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -2+x_5^310 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0 /\ -2-x_5^320 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^320 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (-1+n1 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -x_5^330 >= 0 /\ -1+n1 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (-1+n2 >= 0 /\ -1-x_5^0 >= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ -2-x_5^320 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n2 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -2+x_5^310 >= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ 1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [9] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^30 >= 0 /\ -1+n0 >= 0), cost: NONTERM Applied deletion Removed the following rules: 25 26 27 28 Accelerated simple loops Start location: l8 29: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2*n 30: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 31: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 32: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 40: l1 -> [9] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM 43: l1 -> [9] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^330 <= 0), cost: NONTERM 45: l1 -> [9] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^320 <= 0), cost: NONTERM 59: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 63: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM 65: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: 2*n1 66: l1 -> [9] : (1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM 67: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: 2*n2 68: l1 -> [9] : (1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM 69: l1 -> [9] : (2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 70: l1 -> [9] : (1+x_5^0 <= 0 /\ -1-x_5^0+x_5^310 <= 0), cost: NONTERM 71: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^310 <= 0), cost: NONTERM 72: l1 -> [9] : (2+x_5^30 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 73: l1 -> [9] : (1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM 74: l1 -> [9] : (1+x_5^0 <= 0 /\ -2+x_5^330 >= 0), cost: NONTERM 75: l1 -> [9] : (1+x_5^0 <= 0 /\ x_5^320 >= 0), cost: NONTERM 76: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM 77: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 78: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM 79: l1 -> [9] : (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 80: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM 81: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM 82: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM 83: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM 84: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM 85: l1 -> [9] : (-1+n2 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 86: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 87: l1 -> [9] : (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM 88: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 89: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM 90: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM 91: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^30 >= 0 /\ -1+n0 >= 0), cost: NONTERM 24: l8 -> l1 : TRUE, cost: 2 Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2*n New rule: l8 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2+2*n Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 New rule: l8 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^330 <= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^320 <= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: 2*n1 New rule: l8 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n1 Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^330, (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: 2*n2 New rule: l8 -> l1 : x_5^0'=-1+x_5^330, (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: 2+2*n2 Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0 <= 0 /\ -1-x_5^0+x_5^310 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^310 <= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (2+x_5^30 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0 <= 0 /\ -2+x_5^330 >= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0 <= 0 /\ x_5^320 >= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n1 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^330 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^0+x_5^320 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n2 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+n >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (1+x_5^0-x_5^310 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l8 -> l1 : TRUE, cost: 2 Second rule: l1 -> [9] : (-1+x_5^0 >= 0 /\ x_5^30 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM Applied deletion Removed the following rules: 29 30 31 32 40 43 45 59 63 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 Chained accelerated rules with incoming rules Start location: l8 24: l8 -> l1 : TRUE, cost: 2 92: l8 -> l1 : x_5^0'=1+x_5^30, (-1+n >= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: 2+2*n 93: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM 94: l8 -> l1 : x_5^0'=-1+x_5^310, (-2+x_5^310 >= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 95: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM 96: l8 -> l1 : x_5^0'=1+x_5^320, (-1+n1 >= 0 /\ 2+x_5^320 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n1 97: l8 -> l1 : x_5^0'=-1+x_5^330, (-1+n2 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^330 <= 0), cost: 2+2*n2 Removed unreachable locations and irrelevant leafs Start location: l8 93: l8 -> [9] : -1+x_5^0 >= 0, cost: NONTERM 95: l8 -> [9] : 1+x_5^0 <= 0, cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 93 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: -1+x_5^0 >= 0