NO Initial ITS Start location: l10 0: l0 -> l1 : k_6^0'=k_6^post0, Result_4^0'=Result_4^post0, x_5^0'=x_5^post0, (x_5^0-x_5^post0 == 0 /\ Result_4^0-Result_4^post0 == 0 /\ k_6^0-k_6^post0 == 0), cost: 1 1: l1 -> l2 : k_6^0'=k_6^post1, Result_4^0'=Result_4^post1, x_5^0'=x_5^post1, (-x_5^0 <= 0 /\ x_5^0-x_5^post1 == 0 /\ Result_4^0-Result_4^post1 == 0 /\ k_6^0-k_6^post1 == 0 /\ x_5^0 <= 0), cost: 1 2: l1 -> l2 : k_6^0'=k_6^post2, Result_4^0'=Result_4^post2, x_5^0'=x_5^post2, (0 == 0 /\ -Result_4^post2+Result_4^0 == 0 /\ -1-x_5^10+x_5^post2 == 0 /\ -x_5^0 <= 0 /\ -x_5^post2 <= 0 /\ 1-x_5^0 <= 0 /\ k_6^0-k_6^post2 == 0 /\ x_5^post2 <= 0), cost: 1 3: l1 -> l2 : k_6^0'=k_6^post3, Result_4^0'=Result_4^post3, x_5^0'=x_5^post3, (0 == 0 /\ x_5^post3 <= 0 /\ 1+x_5^post3-x_5^11 == 0 /\ 1+x_5^0 <= 0 /\ -k_6^post3+k_6^0 == 0 /\ Result_4^0-Result_4^post3 == 0 /\ -x_5^post3 <= 0), cost: 1 4: l1 -> l3 : k_6^0'=k_6^post4, Result_4^0'=Result_4^post4, x_5^0'=x_5^post4, (0 == 0 /\ -1+x_5^post4-x_5^30 == 0 /\ -x_5^0 <= 0 /\ -x_5^20 <= 0 /\ 1-x_5^0 <= 0 /\ 1-x_5^20 <= 0 /\ -Result_4^post4+Result_4^0 == 0 /\ -1-x_5^12+x_5^20 == 0 /\ k_6^0-k_6^post4 == 0), cost: 1 6: l1 -> l4 : k_6^0'=k_6^post6, Result_4^0'=Result_4^post6, x_5^0'=x_5^post6, (0 == 0 /\ 1-x_5^310+x_5^post6 == 0 /\ k_6^0 <= 0 /\ -x_5^0 <= 0 /\ -1+x_5^210-x_5^13 == 0 /\ 1-x_5^0 <= 0 /\ Result_4^0-Result_4^post6 == 0 /\ k_6^0-k_6^post6 == 0 /\ 1+x_5^210 <= 0), cost: 1 8: l1 -> l5 : k_6^0'=k_6^post8, Result_4^0'=Result_4^post8, x_5^0'=x_5^post8, (0 == 0 /\ -1-x_5^14+x_5^220 == 0 /\ -x_5^0 <= 0 /\ 1+x_5^220 <= 0 /\ 1-x_5^0 <= 0 /\ 1-k_6^0 <= 0 /\ -Result_4^post8+Result_4^0 == 0 /\ k_6^0-k_6^post8 == 0 /\ -k_6^0+x_5^320 == 0 /\ 1+x_5^post8-x_5^40 == 0), cost: 1 10: l1 -> l6 : k_6^0'=k_6^post10, Result_4^0'=Result_4^post10, x_5^0'=x_5^post10, (0 == 0 /\ k_6^0-k_6^post10 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ 1+x_5^230-x_5^15 == 0 /\ -1-x_5^330+x_5^post10 == 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^230 <= 0 /\ -x_5^230 <= 0), cost: 1 12: l1 -> l7 : k_6^0'=k_6^post12, Result_4^0'=Result_4^post12, x_5^0'=x_5^post12, (0 == 0 /\ k_6^0 <= 0 /\ 1+x_5^240 <= 0 /\ 1+x_5^240-x_5^16 == 0 /\ 1+x_5^post12-x_5^340 == 0 /\ 1+x_5^0 <= 0 /\ -k_6^post12+k_6^0 == 0 /\ Result_4^0-Result_4^post12 == 0), cost: 1 14: l1 -> l8 : k_6^0'=k_6^post14, Result_4^0'=Result_4^post14, x_5^0'=x_5^post14, (0 == 0 /\ 1+x_5^250 <= 0 /\ -k_6^0+x_5^350 == 0 /\ Result_4^0-Result_4^post14 == 0 /\ 1+x_5^post14-x_5^410 == 0 /\ k_6^0-k_6^post14 == 0 /\ 1-k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^17+x_5^250 == 0), cost: 1 16: l2 -> l9 : k_6^0'=k_6^post16, Result_4^0'=Result_4^post16, x_5^0'=x_5^post16, (0 == 0 /\ k_6^0-k_6^post16 == 0 /\ -x_5^post16+x_5^0 == 0), cost: 1 5: l3 -> l1 : k_6^0'=k_6^post5, Result_4^0'=Result_4^post5, x_5^0'=x_5^post5, (x_5^0-x_5^post5 == 0 /\ Result_4^0-Result_4^post5 == 0 /\ k_6^0-k_6^post5 == 0), cost: 1 7: l4 -> l1 : k_6^0'=k_6^post7, Result_4^0'=Result_4^post7, x_5^0'=x_5^post7, (-Result_4^post7+Result_4^0 == 0 /\ k_6^0-k_6^post7 == 0 /\ -x_5^post7+x_5^0 == 0), cost: 1 9: l5 -> l1 : k_6^0'=k_6^post9, Result_4^0'=Result_4^post9, x_5^0'=x_5^post9, (-Result_4^post9+Result_4^0 == 0 /\ -k_6^post9+k_6^0 == 0 /\ -x_5^post9+x_5^0 == 0), cost: 1 11: l6 -> l1 : k_6^0'=k_6^post11, Result_4^0'=Result_4^post11, x_5^0'=x_5^post11, (Result_4^0-Result_4^post11 == 0 /\ -x_5^post11+x_5^0 == 0 /\ k_6^0-k_6^post11 == 0), cost: 1 13: l7 -> l1 : k_6^0'=k_6^post13, Result_4^0'=Result_4^post13, x_5^0'=x_5^post13, (-Result_4^post13+Result_4^0 == 0 /\ -x_5^post13+x_5^0 == 0 /\ k_6^0-k_6^post13 == 0), cost: 1 15: l8 -> l1 : k_6^0'=k_6^post15, Result_4^0'=Result_4^post15, x_5^0'=x_5^post15, (-Result_4^post15+Result_4^0 == 0 /\ -x_5^post15+x_5^0 == 0 /\ k_6^0-k_6^post15 == 0), cost: 1 17: l10 -> l0 : k_6^0'=k_6^post17, Result_4^0'=Result_4^post17, x_5^0'=x_5^post17, (-x_5^post17+x_5^0 == 0 /\ k_6^0-k_6^post17 == 0 /\ -Result_4^post17+Result_4^0 == 0), cost: 1 Removed unreachable rules and leafs Start location: l10 0: l0 -> l1 : k_6^0'=k_6^post0, Result_4^0'=Result_4^post0, x_5^0'=x_5^post0, (x_5^0-x_5^post0 == 0 /\ Result_4^0-Result_4^post0 == 0 /\ k_6^0-k_6^post0 == 0), cost: 1 4: l1 -> l3 : k_6^0'=k_6^post4, Result_4^0'=Result_4^post4, x_5^0'=x_5^post4, (0 == 0 /\ -1+x_5^post4-x_5^30 == 0 /\ -x_5^0 <= 0 /\ -x_5^20 <= 0 /\ 1-x_5^0 <= 0 /\ 1-x_5^20 <= 0 /\ -Result_4^post4+Result_4^0 == 0 /\ -1-x_5^12+x_5^20 == 0 /\ k_6^0-k_6^post4 == 0), cost: 1 6: l1 -> l4 : k_6^0'=k_6^post6, Result_4^0'=Result_4^post6, x_5^0'=x_5^post6, (0 == 0 /\ 1-x_5^310+x_5^post6 == 0 /\ k_6^0 <= 0 /\ -x_5^0 <= 0 /\ -1+x_5^210-x_5^13 == 0 /\ 1-x_5^0 <= 0 /\ Result_4^0-Result_4^post6 == 0 /\ k_6^0-k_6^post6 == 0 /\ 1+x_5^210 <= 0), cost: 1 8: l1 -> l5 : k_6^0'=k_6^post8, Result_4^0'=Result_4^post8, x_5^0'=x_5^post8, (0 == 0 /\ -1-x_5^14+x_5^220 == 0 /\ -x_5^0 <= 0 /\ 1+x_5^220 <= 0 /\ 1-x_5^0 <= 0 /\ 1-k_6^0 <= 0 /\ -Result_4^post8+Result_4^0 == 0 /\ k_6^0-k_6^post8 == 0 /\ -k_6^0+x_5^320 == 0 /\ 1+x_5^post8-x_5^40 == 0), cost: 1 10: l1 -> l6 : k_6^0'=k_6^post10, Result_4^0'=Result_4^post10, x_5^0'=x_5^post10, (0 == 0 /\ k_6^0-k_6^post10 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ 1+x_5^230-x_5^15 == 0 /\ -1-x_5^330+x_5^post10 == 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^230 <= 0 /\ -x_5^230 <= 0), cost: 1 12: l1 -> l7 : k_6^0'=k_6^post12, Result_4^0'=Result_4^post12, x_5^0'=x_5^post12, (0 == 0 /\ k_6^0 <= 0 /\ 1+x_5^240 <= 0 /\ 1+x_5^240-x_5^16 == 0 /\ 1+x_5^post12-x_5^340 == 0 /\ 1+x_5^0 <= 0 /\ -k_6^post12+k_6^0 == 0 /\ Result_4^0-Result_4^post12 == 0), cost: 1 14: l1 -> l8 : k_6^0'=k_6^post14, Result_4^0'=Result_4^post14, x_5^0'=x_5^post14, (0 == 0 /\ 1+x_5^250 <= 0 /\ -k_6^0+x_5^350 == 0 /\ Result_4^0-Result_4^post14 == 0 /\ 1+x_5^post14-x_5^410 == 0 /\ k_6^0-k_6^post14 == 0 /\ 1-k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^17+x_5^250 == 0), cost: 1 5: l3 -> l1 : k_6^0'=k_6^post5, Result_4^0'=Result_4^post5, x_5^0'=x_5^post5, (x_5^0-x_5^post5 == 0 /\ Result_4^0-Result_4^post5 == 0 /\ k_6^0-k_6^post5 == 0), cost: 1 7: l4 -> l1 : k_6^0'=k_6^post7, Result_4^0'=Result_4^post7, x_5^0'=x_5^post7, (-Result_4^post7+Result_4^0 == 0 /\ k_6^0-k_6^post7 == 0 /\ -x_5^post7+x_5^0 == 0), cost: 1 9: l5 -> l1 : k_6^0'=k_6^post9, Result_4^0'=Result_4^post9, x_5^0'=x_5^post9, (-Result_4^post9+Result_4^0 == 0 /\ -k_6^post9+k_6^0 == 0 /\ -x_5^post9+x_5^0 == 0), cost: 1 11: l6 -> l1 : k_6^0'=k_6^post11, Result_4^0'=Result_4^post11, x_5^0'=x_5^post11, (Result_4^0-Result_4^post11 == 0 /\ -x_5^post11+x_5^0 == 0 /\ k_6^0-k_6^post11 == 0), cost: 1 13: l7 -> l1 : k_6^0'=k_6^post13, Result_4^0'=Result_4^post13, x_5^0'=x_5^post13, (-Result_4^post13+Result_4^0 == 0 /\ -x_5^post13+x_5^0 == 0 /\ k_6^0-k_6^post13 == 0), cost: 1 15: l8 -> l1 : k_6^0'=k_6^post15, Result_4^0'=Result_4^post15, x_5^0'=x_5^post15, (-Result_4^post15+Result_4^0 == 0 /\ -x_5^post15+x_5^0 == 0 /\ k_6^0-k_6^post15 == 0), cost: 1 17: l10 -> l0 : k_6^0'=k_6^post17, Result_4^0'=Result_4^post17, x_5^0'=x_5^post17, (-x_5^post17+x_5^0 == 0 /\ k_6^0-k_6^post17 == 0 /\ -Result_4^post17+Result_4^0 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : k_6^0'=k_6^post0, Result_4^0'=Result_4^post0, x_5^0'=x_5^post0, (x_5^0-x_5^post0 == 0 /\ Result_4^0-Result_4^post0 == 0 /\ k_6^0-k_6^post0 == 0), cost: 1 New rule: l0 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l3 : k_6^0'=k_6^post4, Result_4^0'=Result_4^post4, x_5^0'=x_5^post4, (0 == 0 /\ -1+x_5^post4-x_5^30 == 0 /\ -x_5^0 <= 0 /\ -x_5^20 <= 0 /\ 1-x_5^0 <= 0 /\ 1-x_5^20 <= 0 /\ -Result_4^post4+Result_4^0 == 0 /\ -1-x_5^12+x_5^20 == 0 /\ k_6^0-k_6^post4 == 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 : k_6^0'=k_6^post5, Result_4^0'=Result_4^post5, x_5^0'=x_5^post5, (x_5^0-x_5^post5 == 0 /\ Result_4^0-Result_4^post5 == 0 /\ k_6^0-k_6^post5 == 0), cost: 1 New rule: l3 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l4 : k_6^0'=k_6^post6, Result_4^0'=Result_4^post6, x_5^0'=x_5^post6, (0 == 0 /\ 1-x_5^310+x_5^post6 == 0 /\ k_6^0 <= 0 /\ -x_5^0 <= 0 /\ -1+x_5^210-x_5^13 == 0 /\ 1-x_5^0 <= 0 /\ Result_4^0-Result_4^post6 == 0 /\ k_6^0-k_6^post6 == 0 /\ 1+x_5^210 <= 0), cost: 1 New rule: l1 -> l4 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 1 Applied preprocessing Original rule: l4 -> l1 : k_6^0'=k_6^post7, Result_4^0'=Result_4^post7, x_5^0'=x_5^post7, (-Result_4^post7+Result_4^0 == 0 /\ k_6^0-k_6^post7 == 0 /\ -x_5^post7+x_5^0 == 0), cost: 1 New rule: l4 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l5 : k_6^0'=k_6^post8, Result_4^0'=Result_4^post8, x_5^0'=x_5^post8, (0 == 0 /\ -1-x_5^14+x_5^220 == 0 /\ -x_5^0 <= 0 /\ 1+x_5^220 <= 0 /\ 1-x_5^0 <= 0 /\ 1-k_6^0 <= 0 /\ -Result_4^post8+Result_4^0 == 0 /\ k_6^0-k_6^post8 == 0 /\ -k_6^0+x_5^320 == 0 /\ 1+x_5^post8-x_5^40 == 0), cost: 1 New rule: l1 -> l5 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 1 Applied preprocessing Original rule: l5 -> l1 : k_6^0'=k_6^post9, Result_4^0'=Result_4^post9, x_5^0'=x_5^post9, (-Result_4^post9+Result_4^0 == 0 /\ -k_6^post9+k_6^0 == 0 /\ -x_5^post9+x_5^0 == 0), cost: 1 New rule: l5 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l6 : k_6^0'=k_6^post10, Result_4^0'=Result_4^post10, x_5^0'=x_5^post10, (0 == 0 /\ k_6^0-k_6^post10 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ 1+x_5^230-x_5^15 == 0 /\ -1-x_5^330+x_5^post10 == 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^230 <= 0 /\ -x_5^230 <= 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 : k_6^0'=k_6^post11, Result_4^0'=Result_4^post11, x_5^0'=x_5^post11, (Result_4^0-Result_4^post11 == 0 /\ -x_5^post11+x_5^0 == 0 /\ k_6^0-k_6^post11 == 0), cost: 1 New rule: l6 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l7 : k_6^0'=k_6^post12, Result_4^0'=Result_4^post12, x_5^0'=x_5^post12, (0 == 0 /\ k_6^0 <= 0 /\ 1+x_5^240 <= 0 /\ 1+x_5^240-x_5^16 == 0 /\ 1+x_5^post12-x_5^340 == 0 /\ 1+x_5^0 <= 0 /\ -k_6^post12+k_6^0 == 0 /\ Result_4^0-Result_4^post12 == 0), cost: 1 New rule: l1 -> l7 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 1 Applied preprocessing Original rule: l7 -> l1 : k_6^0'=k_6^post13, Result_4^0'=Result_4^post13, x_5^0'=x_5^post13, (-Result_4^post13+Result_4^0 == 0 /\ -x_5^post13+x_5^0 == 0 /\ k_6^0-k_6^post13 == 0), cost: 1 New rule: l7 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l8 : k_6^0'=k_6^post14, Result_4^0'=Result_4^post14, x_5^0'=x_5^post14, (0 == 0 /\ 1+x_5^250 <= 0 /\ -k_6^0+x_5^350 == 0 /\ Result_4^0-Result_4^post14 == 0 /\ 1+x_5^post14-x_5^410 == 0 /\ k_6^0-k_6^post14 == 0 /\ 1-k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1-x_5^17+x_5^250 == 0), cost: 1 New rule: l1 -> l8 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 1 Applied preprocessing Original rule: l8 -> l1 : k_6^0'=k_6^post15, Result_4^0'=Result_4^post15, x_5^0'=x_5^post15, (-Result_4^post15+Result_4^0 == 0 /\ -x_5^post15+x_5^0 == 0 /\ k_6^0-k_6^post15 == 0), cost: 1 New rule: l8 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l10 -> l0 : k_6^0'=k_6^post17, Result_4^0'=Result_4^post17, x_5^0'=x_5^post17, (-x_5^post17+x_5^0 == 0 /\ k_6^0-k_6^post17 == 0 /\ -Result_4^post17+Result_4^0 == 0), cost: 1 New rule: l10 -> l0 : TRUE, cost: 1 Simplified rules Start location: l10 18: l0 -> l1 : TRUE, cost: 1 19: l1 -> l3 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 1 21: l1 -> l4 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 1 23: l1 -> l5 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 1 25: l1 -> l6 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 1 27: l1 -> l7 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 1 29: l1 -> l8 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 1 20: l3 -> l1 : TRUE, cost: 1 22: l4 -> l1 : TRUE, cost: 1 24: l5 -> l1 : TRUE, cost: 1 26: l6 -> l1 : TRUE, cost: 1 28: l7 -> l1 : TRUE, cost: 1 30: l8 -> l1 : TRUE, cost: 1 31: l10 -> l0 : TRUE, cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l10 -> l0 : TRUE, cost: 1 Second rule: l0 -> l1 : TRUE, cost: 1 New rule: l10 -> l1 : TRUE, cost: 2 Applied deletion Removed the following rules: 18 31 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: 19 20 Eliminating location l4 by chaining: Applied chaining First rule: l1 -> l4 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -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, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 Applied deletion Removed the following rules: 21 22 Eliminating location l5 by chaining: Applied chaining First rule: l1 -> l5 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 1 Second rule: l5 -> l1 : TRUE, cost: 1 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 Applied deletion Removed the following rules: 23 24 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: 25 26 Eliminating location l7 by chaining: Applied chaining First rule: l1 -> l7 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 1 Second rule: l7 -> l1 : TRUE, cost: 1 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 Applied deletion Removed the following rules: 27 28 Eliminating location l8 by chaining: Applied chaining First rule: l1 -> l8 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 1 Second rule: l8 -> l1 : TRUE, cost: 1 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 Applied deletion Removed the following rules: 29 30 Eliminated locations on linear paths Start location: l10 33: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 34: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 35: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 36: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 37: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 38: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 32: l10 -> 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+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_EeeinA.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_PGGDbL.txt Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_pOmdGa.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_dAFnKG.txt Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_NNNPCg.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_fkoapf.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, (-1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_gfDKcc.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 New rule: l1 -> [11] : (-1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_PMpbGk.txt Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n3 Sub-proof via acceration calculus written to file:///tmp/tmpnam_GghmLL.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> [11] : (-1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_OHFOfF.txt Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n4 Sub-proof via acceration calculus written to file:///tmp/tmpnam_JcohBf.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_liHNmL.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 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+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n5 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0), cost: 4*n5 Sub-proof via acceration calculus written to file:///tmp/tmpnam_OpAfKI.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_aPKkfm.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+k_6^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^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-x_5^40 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n6 >= 0), cost: 4*n6 Sub-proof via acceration calculus written to file:///tmp/tmpnam_NFEonB.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^40 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_oiOJke.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^40 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -x_5^40 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 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+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n7 >= 0 /\ -2-x_5^30 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: 4*n7 Sub-proof via acceration calculus written to file:///tmp/tmpnam_iKCMFN.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_lhLDpC.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -2-x_5^30 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 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, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (-k_6^0 >= 0 /\ -1+n8 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0), cost: 4*n8 Sub-proof via acceration calculus written to file:///tmp/tmpnam_ocOMIf.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (-k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_AfbfhO.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [11] : (-k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -k_6^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^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -x_5^310 >= 0 /\ -1+n9 >= 0), cost: 4*n9 Sub-proof via acceration calculus written to file:///tmp/tmpnam_kjCncM.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^310-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_enecFA.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^310-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -x_5^310 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 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, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-2-x_5^30 >= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n10 >= 0), cost: 4*n10 Sub-proof via acceration calculus written to file:///tmp/tmpnam_iEliPm.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_MHMCfb.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -2-x_5^30 >= 0 /\ -1+x_5^0 >= 0 /\ -k_6^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^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-x_5^410 >= 0 /\ -1+n11 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: 4*n11 Sub-proof via acceration calculus written to file:///tmp/tmpnam_NlKEam.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_LfmfNb.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -x_5^410 >= 0 /\ -1+k_6^0 >= 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^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-k_6^0 >= 0 /\ -1+n12 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: 4*n12 Sub-proof via acceration calculus written to file:///tmp/tmpnam_GlCChM.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_oHJhPi.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 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^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n13 >= 0 /\ -x_5^40 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: 4*n13 Sub-proof via acceration calculus written to file:///tmp/tmpnam_jMfPeH.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^40 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_DAnena.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^40 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -x_5^40 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^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^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+n14 >= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -x_5^310 >= 0), cost: 4*n14 Sub-proof via acceration calculus written to file:///tmp/tmpnam_jIOGDg.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^310-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_gGbJHI.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^310-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -x_5^310 >= 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, (-2-x_5^30 >= 0 /\ -1+n15 >= 0 /\ -1-x_5^0 >= 0), cost: 4*n15 Sub-proof via acceration calculus written to file:///tmp/tmpnam_KCCFdO.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, 1+x_5^0 <= 0, cost: 4 New rule: l1 -> [11] : (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_IofCLH.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (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^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n16 >= 0 /\ -2+x_5^410 >= 0), cost: 4*n16 Sub-proof via acceration calculus written to file:///tmp/tmpnam_cpLNLD.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> [11] : (1+x_5^0-x_5^410 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_AenKch.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> [11] : (1+x_5^0-x_5^410 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^410 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^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 /\ -1+k_6^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+x_5^0 >= 0 /\ -1+k_6^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+k_6^0 >= 0 /\ -1+n17 >= 0), cost: 4*n17 Sub-proof via acceration calculus written to file:///tmp/tmpnam_ifPodl.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_oGdpnM.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ x_5^330 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^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 /\ -1+k_6^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n18 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: 4*n18 Sub-proof via acceration calculus written to file:///tmp/tmpnam_mlgbkF.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_OPjgDi.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-2+x_5^340 >= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -1+n19 >= 0), cost: 4*n19 Sub-proof via acceration calculus written to file:///tmp/tmpnam_momJHb.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ 1-x_5^340+x_5^0 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_EjHlcL.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ 1-x_5^340+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -2+x_5^340 >= 0 /\ -k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -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, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n20 >= 0 /\ x_5^330 >= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0), cost: 4*n20 Sub-proof via acceration calculus written to file:///tmp/tmpnam_idAGMK.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_jIDjhM.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ x_5^330 >= 0 /\ -k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -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, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n21 >= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ x_5^30 >= 0), cost: 4*n21 Sub-proof via acceration calculus written to file:///tmp/tmpnam_ignfOa.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_GmBDcP.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^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^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+x_5^0 >= 0 /\ -1+n22 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^410 >= 0), cost: 4*n22 Sub-proof via acceration calculus written to file:///tmp/tmpnam_GgGHNG.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> [11] : (1+x_5^0-x_5^410 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_IbKMio.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> [11] : (1+x_5^0-x_5^410 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^410 >= 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^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-2+x_5^340 >= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -1+n23 >= 0), cost: 4*n23 Sub-proof via acceration calculus written to file:///tmp/tmpnam_IapBne.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ 1-x_5^340+x_5^0 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_EKAlJL.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ 1-x_5^340+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -2+x_5^340 >= 0 /\ -k_6^0 >= 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^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+n24 >= 0 /\ x_5^330 >= 0 /\ -1+x_5^0 >= 0), cost: 4*n24 Sub-proof via acceration calculus written to file:///tmp/tmpnam_DlkHJo.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, -1+x_5^0 >= 0, cost: 4 New rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_PfPbke.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (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^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n25 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 4*n25 Sub-proof via acceration calculus written to file:///tmp/tmpnam_PaAahK.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_IEeLpD.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 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, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+x_5^0 >= 0 /\ -1+n26 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0), cost: 4*n26 Sub-proof via acceration calculus written to file:///tmp/tmpnam_NNPeMf.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 4 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_iFcDpP.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n2 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n29 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n29+2*n2*n29 Sub-proof via acceration calculus written to file:///tmp/tmpnam_lgCFKP.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_FhBkfI.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-x_5^410 >= 0 /\ -1+n30 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0), cost: 2*n30+2*n2*n30 Sub-proof via acceration calculus written to file:///tmp/tmpnam_kdPiBf.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_dKPLgf.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -x_5^410 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n2 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (-k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0 /\ -1+n33 >= 0), cost: 2*n33+2*n33*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_LcFhbB.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 New rule: l1 -> [11] : (-k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_KhEKlD.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n2 Second rule: l1 -> [11] : (-k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n34 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0), cost: 2*n34+2*n2*n34 Sub-proof via acceration calculus written to file:///tmp/tmpnam_cEjkak.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 New rule: l1 -> [11] : (-1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_bkFGHB.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 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^340, (-1+n3 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n3 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n3 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n3 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ -1+n38 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n3*n38+2*n38 Sub-proof via acceration calculus written to file:///tmp/tmpnam_dgbkNK.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n3 New rule: l1 -> [11] : (-1+n3 >= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_DOfpcC.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n3 Second rule: l1 -> [11] : (-1+n3 >= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+n3 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n3 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+n3 >= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n3 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n3 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n3 >= 0 /\ -1+n39 >= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0), cost: 2*n39+2*n39*n3 Sub-proof via acceration calculus written to file:///tmp/tmpnam_pBFJpD.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n3 New rule: l1 -> [11] : (-1+n3 >= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_fjFGOC.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [11] : (-1+n3 >= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+n3 >= 0 /\ -k_6^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^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n4 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: 2+2*n4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: 2+2*n4 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n40 >= 0), cost: 2*n40+2*n40*n4 Sub-proof via acceration calculus written to file:///tmp/tmpnam_HdHKmG.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: 2+2*n4 New rule: l1 -> [11] : (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_lFEhin.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n4 Second rule: l1 -> [11] : (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n4 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+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n4 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n4 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n41 >= 0), cost: 2*n41*n4+2*n41 Sub-proof via acceration calculus written to file:///tmp/tmpnam_niNfkc.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n4 New rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_bnKoMi.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^330, 1+x_5^0 <= 0, cost: 2 Second rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+n4 >= 0 /\ -1+k_6^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^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2+2*n Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2+2*n New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ -1+n42 >= 0 /\ x_5^30 >= 0), cost: 2*n42*n+2*n42 Sub-proof via acceration calculus written to file:///tmp/tmpnam_GHHAnH.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2+2*n New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_ECHBLA.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 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 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n Second rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: 2+2*n Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: 2+2*n New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n43 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ -2+x_5^40 >= 0), cost: 2*n*n43+2*n43 Sub-proof via acceration calculus written to file:///tmp/tmpnam_KIFnbD.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: 2+2*n New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_IPFkHD.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n New rule: l1 -> l1 : x_5^0'=1+x_5^30, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2+2*n Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2+2*n New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0 /\ -1+n46 >= 0 /\ x_5^30 >= 0), cost: 2*n46+2*n46*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_dllEIp.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2+2*n New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_mnlpfo.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -1+n >= 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 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0), cost: 2+2*n Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0), cost: 2+2*n New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0 /\ -1+n47 >= 0), cost: 2*n47*n+2*n47 Sub-proof via acceration calculus written to file:///tmp/tmpnam_oPPpfh.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0), cost: 2+2*n New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_OHfakm.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n >= 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 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+n50 >= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: 2*n50+2*n0*n50 Sub-proof via acceration calculus written to file:///tmp/tmpnam_HmhAiH.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_PkhfnH.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^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, (k_6^0 <= 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^30, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -1+n51 >= 0 /\ -1+n0 >= 0 /\ x_5^30 >= 0), cost: 2*n51+2*n51*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_DEMEMP.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_PCNbBN.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 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^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2*n1 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2+2*n1 Applied acceleration Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2+2*n1 New rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0 /\ -1+n52 >= 0), cost: 2*n52+2*n1*n52 Sub-proof via acceration calculus written to file:///tmp/tmpnam_jMCPaK.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2+2*n1 New rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_LhCEPK.txt Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2*n1 Second rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2*n1 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+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2+2*n1 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2+2*n1 New rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n53 >= 0 /\ x_5^30 >= 0), cost: 2*n53+2*n53*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_pEbgEF.txt Applied nonterm Original rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: 2+2*n1 New rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_KbnFpM.txt Applied chaining First rule: l1 -> l1 : x_5^0'=1+x_5^30, -1+x_5^0 >= 0, cost: 2 Second rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (0 <= 0 /\ -1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> l1 : x_5^0'=-1+x_5^310, (-1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: 2*n0 New rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: 2*n0 Applied simplification Original rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> l1 : x_5^0'=1+x_5^330, (-1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: 2*n2 New rule: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2*n2 Applied simplification Original rule: l1 -> [11] : (-1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n3 New rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: 2*n3 Applied simplification Original rule: l1 -> [11] : (-1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: 2*n4 New rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: 2*n4 Applied simplification Original rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2-x_5^330 >= 0), cost: NONTERM New rule: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^40 <= 0), cost: NONTERM New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^40 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -x_5^40 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^40 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -2-x_5^30 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2-x_5^330 >= 0), cost: NONTERM New rule: l1 -> [11] : (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^310-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^310-x_5^0 <= 0 /\ k_6^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -x_5^310 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ x_5^310 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ k_6^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -2-x_5^30 >= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -x_5^410 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -2-x_5^30 >= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^410 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^410 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ x_5^330 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (x_5^330 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ 1-x_5^340+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^340+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -2+x_5^340 >= 0 /\ -k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -2+x_5^340 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ x_5^330 >= 0 /\ -k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -x_5^410 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0 /\ x_5^410 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -2-x_5^330 >= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+n3 >= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+n3 >= 0 /\ -k_6^0 >= 0 /\ -x_5^340 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+n3 >= 0 /\ -k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+n3 >= 0 /\ -k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2-x_5^330 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n3 >= 0 /\ 2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -x_5^410 >= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2-x_5^330 >= 0), cost: NONTERM New rule: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -1+n >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -1+n0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+n0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+x_5^0 >= 0 /\ -k_6^0 >= 0 /\ -1+n0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [11] : (0 <= 0 /\ -1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM Applied deletion Removed the following rules: 33 34 35 36 37 38 Accelerated simple loops Start location: l10 39: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n 40: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0), cost: NONTERM 43: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2*n1 44: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM 55: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM 65: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM 67: l1 -> [11] : (1+x_5^0-x_5^410 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM 69: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM 71: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM 79: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 101: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM 113: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM 115: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: 2*n0 116: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0), cost: NONTERM 117: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2*n2 118: l1 -> [11] : (1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM 119: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: 2*n3 120: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM 121: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: 2*n4 122: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM 123: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM 124: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 125: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^40 <= 0), cost: NONTERM 126: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^40 <= 0), cost: NONTERM 127: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM 128: l1 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM 129: l1 -> [11] : (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 130: l1 -> [11] : (-1+x_5^310-x_5^0 <= 0 /\ k_6^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM 131: l1 -> [11] : (k_6^0 <= 0 /\ x_5^310 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 132: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ k_6^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM 133: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM 134: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: NONTERM 135: l1 -> [11] : (k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 136: l1 -> [11] : (-1+x_5^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM 137: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^410 >= 0), cost: NONTERM 138: l1 -> [11] : (x_5^330 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 139: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM 140: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^340+x_5^0 <= 0), cost: NONTERM 141: l1 -> [11] : (k_6^0 <= 0 /\ -2+x_5^340 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 142: l1 -> [11] : (k_6^0 <= 0 /\ -1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 143: l1 -> [11] : (k_6^0 <= 0 /\ x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 144: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0), cost: NONTERM 145: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM 146: l1 -> [11] : (x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 147: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM 148: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0), cost: NONTERM 149: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM 150: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM 151: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM 152: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0 /\ x_5^410 <= 0), cost: NONTERM 153: l1 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM 154: l1 -> [11] : (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM 155: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM 156: l1 -> [11] : (k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM 157: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM 158: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 159: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM 160: l1 -> [11] : (-1+n3 >= 0 /\ 2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 161: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM 162: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: NONTERM 163: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM 164: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 165: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM 166: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM 167: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM 168: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0), cost: NONTERM 169: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM 170: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -1+n >= 0), cost: NONTERM 171: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n >= 0), cost: NONTERM 172: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -1+n0 >= 0), cost: NONTERM 173: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: NONTERM 174: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+n0 >= 0), cost: NONTERM 175: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0 /\ x_5^30 >= 0), cost: NONTERM 176: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM 177: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM 178: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM 32: l10 -> l1 : TRUE, cost: 2 Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2*n New rule: l10 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2+2*n Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0), cost: NONTERM New rule: l10 -> [11] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2*n1 New rule: l10 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2+2*n1 Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (1+x_5^0-x_5^410 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: 2*n0 New rule: l10 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2*n2 New rule: l10 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: 2*n3 New rule: l10 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n3 Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=-1+x_5^410, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: 2*n4 New rule: l10 -> l1 : x_5^0'=-1+x_5^410, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: 2+2*n4 Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^40 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^40 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^310-x_5^0 <= 0 /\ k_6^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ x_5^310 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (1-x_5^0+x_5^30 <= 0 /\ k_6^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ 2+x_5^30 <= 0), cost: NONTERM New rule: l10 -> [11] : -1+x_5^0 >= 0, cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -2+x_5^410 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (x_5^330 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^340+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -2+x_5^340 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1-x_5^330+x_5^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (x_5^330 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : 1+x_5^0 <= 0, cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0 /\ x_5^410 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ -1+x_5^340-x_5^0 <= 0 /\ -1-x_5^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n3 >= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n3 >= 0 /\ 2+x_5^330 <= 0 /\ k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ -1-x_5^0+x_5^410 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ 1+x_5^330-x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (2+x_5^330 <= 0 /\ -1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM New rule: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -1+n >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+n >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -1+n >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ 1-x_5^310+x_5^0 <= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+x_5^0-x_5^30 <= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -1+n0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ 1+x_5^0-x_5^40 <= 0 /\ -1+k_6^0 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied chaining First rule: l10 -> l1 : TRUE, cost: 2 Second rule: l1 -> [11] : (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ x_5^30 >= 0), cost: NONTERM New rule: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM Applied deletion Removed the following rules: 39 40 43 44 55 65 67 69 71 79 101 113 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 Chained accelerated rules with incoming rules Start location: l10 32: l10 -> l1 : TRUE, cost: 2 179: l10 -> l1 : x_5^0'=1+x_5^30, (-1+x_5^0 >= 0 /\ -1+n >= 0 /\ x_5^30 >= 0), cost: 2+2*n 180: l10 -> [11] : -1+x_5^0 >= 0, cost: NONTERM 181: l10 -> l1 : x_5^0'=-1+x_5^40, (-1+n1 >= 0 /\ -1+x_5^0 >= 0 /\ -1+k_6^0 >= 0 /\ -2+x_5^40 >= 0), cost: 2+2*n1 182: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM 183: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 184: l10 -> [11] : 1+x_5^0 <= 0, cost: NONTERM 185: l10 -> l1 : x_5^0'=-1+x_5^310, (k_6^0 <= 0 /\ -1+x_5^0 >= 0 /\ -2+x_5^310 >= 0 /\ -1+n0 >= 0), cost: 2+2*n0 186: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 187: l10 -> l1 : x_5^0'=1+x_5^330, (2+x_5^330 <= 0 /\ 1+x_5^0 <= 0 /\ -1+n2 >= 0), cost: 2+2*n2 188: l10 -> l1 : x_5^0'=-1+x_5^340, (-1+n3 >= 0 /\ k_6^0 <= 0 /\ x_5^340 <= 0 /\ 1+x_5^0 <= 0), cost: 2+2*n3 189: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 190: l10 -> l1 : x_5^0'=-1+x_5^410, (-1+n4 >= 0 /\ -1+k_6^0 >= 0 /\ 1+x_5^0 <= 0 /\ x_5^410 <= 0), cost: 2+2*n4 Removed unreachable locations and irrelevant leafs Start location: l10 180: l10 -> [11] : -1+x_5^0 >= 0, cost: NONTERM 182: l10 -> [11] : (-1+x_5^0 >= 0 /\ -1+k_6^0 >= 0), cost: NONTERM 183: l10 -> [11] : (-1+k_6^0 >= 0 /\ 1+x_5^0 <= 0), cost: NONTERM 184: l10 -> [11] : 1+x_5^0 <= 0, cost: NONTERM 186: l10 -> [11] : (k_6^0 <= 0 /\ -1+x_5^0 >= 0), cost: NONTERM 189: l10 -> [11] : (k_6^0 <= 0 /\ 1+x_5^0 <= 0), cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 180 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