NO Initial ITS Start location: l6 0: l0 -> l1 : MIN^0'=MIN^post0, pid^0'=pid^post0, INCREASE^0'=INCREASE^post0, conditional^0'=conditional^post0, NUM_MIN^0'=NUM_MIN^post0, MAX_MIN^0'=MAX_MIN^post0, num^0'=num^post0, CRITICAL^0'=CRITICAL^post0, Q^0'=Q^post0, NONCRITICAL^0'=NONCRITICAL^post0, MAX^0'=MAX^post0, j_min^0'=j_min^post0, P^0'=P^post0, (0 == 0 /\ -MAX_MIN^post0+MAX_MIN^0 == 0 /\ Q^0-Q^post0 == 0 /\ num^0-num^post0 == 0 /\ -P^post0+P^0 == 0 /\ -j_min^post0+j_min^0 == 0 /\ -CRITICAL^post0+CRITICAL^0 == 0 /\ INCREASE^0-INCREASE^post0 == 0 /\ -1+conditional^0 <= 0 /\ -MAX^post0+MAX^0 == 0 /\ -pid^post0+pid^0 == 0 /\ MIN^0-MIN^post0 == 0 /\ -NONCRITICAL^post0+NONCRITICAL^0 == 0 /\ NUM_MIN^0-NUM_MIN^post0 == 0), cost: 1 1: l0 -> l1 : MIN^0'=MIN^post1, pid^0'=pid^post1, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=NUM_MIN^post1, MAX_MIN^0'=MAX_MIN^post1, num^0'=num^post1, CRITICAL^0'=CRITICAL^post1, Q^0'=Q^post1, NONCRITICAL^0'=NONCRITICAL^post1, MAX^0'=MAX^post1, j_min^0'=j_min^post1, P^0'=P^post1, (0 == 0 /\ pid^0-pid^post1 == 0 /\ j_min^post1-INCREASE^post1-j_min^0 == 0 /\ Q^0-Q^post1 == 0 /\ -CRITICAL^post1+CRITICAL^0 == 0 /\ 1-INCREASE^post1 <= 0 /\ num^0-num^post1 == 0 /\ -MAX^post1+MAX^0 == 0 /\ NUM_MIN^0-NUM_MIN^post1 == 0 /\ -MAX_MIN^post1+MAX_MIN^0 == 0 /\ -P^post1+P^0 == 0 /\ MIN^0-MIN^post1 == 0 /\ -NONCRITICAL^post1+NONCRITICAL^0 == 0 /\ 2-conditional^0 <= 0), cost: 1 6: l1 -> l3 : MIN^0'=MIN^post6, pid^0'=pid^post6, INCREASE^0'=INCREASE^post6, conditional^0'=conditional^post6, NUM_MIN^0'=NUM_MIN^post6, MAX_MIN^0'=MAX_MIN^post6, num^0'=num^post6, CRITICAL^0'=CRITICAL^post6, Q^0'=Q^post6, NONCRITICAL^0'=NONCRITICAL^post6, MAX^0'=MAX^post6, j_min^0'=j_min^post6, P^0'=P^post6, (0 == 0 /\ pid^0-pid^post6 == 0 /\ MAX^0-MAX^post6 == 0 /\ 1-pid^0+j_min^0 <= 0 /\ -CRITICAL^post6+CRITICAL^0 == 0 /\ INCREASE^0-INCREASE^post6 == 0 /\ MIN^0-num^0 <= 0 /\ Q^0-Q^post6 == 0 /\ num^0-num^post6 == 0 /\ MIN^0-MIN^post6 == 0 /\ NUM_MIN^0-NUM_MIN^post6 == 0 /\ -MAX_MIN^post6+MAX_MIN^0 == 0 /\ -NONCRITICAL^post6+NONCRITICAL^0 == 0 /\ -P^post6+P^0 == 0 /\ -j_min^post6+j_min^0 == 0), cost: 1 7: l1 -> l4 : MIN^0'=MIN^post7, pid^0'=pid^post7, INCREASE^0'=INCREASE^post7, conditional^0'=conditional^post7, NUM_MIN^0'=NUM_MIN^post7, MAX_MIN^0'=MAX_MIN^post7, num^0'=num^post7, CRITICAL^0'=CRITICAL^post7, Q^0'=Q^post7, NONCRITICAL^0'=NONCRITICAL^post7, MAX^0'=MAX^post7, j_min^0'=j_min^post7, P^0'=P^post7, (MAX^0-MAX^post7 == 0 /\ MIN^0-MIN^post7 == 0 /\ conditional^0-conditional^post7 == 0 /\ -MAX_MIN^post7+MAX_MIN^0 == 0 /\ num^0-num^post7 == 0 /\ -NONCRITICAL^post7+NONCRITICAL^0 == 0 /\ pid^0-j_min^0 <= 0 /\ P^post7 == 0 /\ INCREASE^0-INCREASE^post7 == 0 /\ -pid^post7+pid^0 == 0 /\ Q^post7 == 0 /\ -j_min^post7+j_min^0 == 0 /\ -1+CRITICAL^post7 == 0 /\ NUM_MIN^0-NUM_MIN^post7 == 0), cost: 1 8: l1 -> l4 : MIN^0'=MIN^post8, pid^0'=pid^post8, INCREASE^0'=INCREASE^post8, conditional^0'=conditional^post8, NUM_MIN^0'=NUM_MIN^post8, MAX_MIN^0'=MAX_MIN^post8, num^0'=num^post8, CRITICAL^0'=CRITICAL^post8, Q^0'=Q^post8, NONCRITICAL^0'=NONCRITICAL^post8, MAX^0'=MAX^post8, j_min^0'=j_min^post8, P^0'=P^post8, (1-MIN^0+num^0 <= 0 /\ -NONCRITICAL^post8+NONCRITICAL^0 == 0 /\ -1+CRITICAL^post8 == 0 /\ pid^0-pid^post8 == 0 /\ conditional^0-conditional^post8 == 0 /\ -j_min^post8+j_min^0 == 0 /\ P^post8 == 0 /\ num^0-num^post8 == 0 /\ -MAX^post8+MAX^0 == 0 /\ INCREASE^0-INCREASE^post8 == 0 /\ NUM_MIN^0-NUM_MIN^post8 == 0 /\ Q^post8 == 0 /\ -MAX_MIN^post8+MAX_MIN^0 == 0 /\ MIN^0-MIN^post8 == 0), cost: 1 2: l2 -> l0 : MIN^0'=MIN^post2, pid^0'=pid^post2, INCREASE^0'=INCREASE^post2, conditional^0'=conditional^post2, NUM_MIN^0'=NUM_MIN^post2, MAX_MIN^0'=MAX_MIN^post2, num^0'=num^post2, CRITICAL^0'=CRITICAL^post2, Q^0'=Q^post2, NONCRITICAL^0'=NONCRITICAL^post2, MAX^0'=MAX^post2, j_min^0'=j_min^post2, P^0'=P^post2, (0 == 0 /\ -1+P^post2 == 0 /\ -NUM_MIN^post2+NUM_MIN^0 == 0 /\ MAX^0-MAX^post2 == 0 /\ num^0-num^post2 == 0 /\ MIN^0-MIN^post2 == 0 /\ Q^0-Q^post2 == 0 /\ -MAX_MIN^post2+MAX_MIN^0 == 0 /\ -NONCRITICAL^post2+NONCRITICAL^0 == 0 /\ -1+conditional^0 <= 0 /\ -pid^post2+pid^0 == 0 /\ -j_min^post2+j_min^0 == 0 /\ -CRITICAL^post2+CRITICAL^0 == 0 /\ INCREASE^0-INCREASE^post2 == 0), cost: 1 3: l2 -> l1 : MIN^0'=MIN^post3, pid^0'=pid^post3, INCREASE^0'=INCREASE^post3, conditional^0'=conditional^post3, NUM_MIN^0'=NUM_MIN^post3, MAX_MIN^0'=MAX_MIN^post3, num^0'=num^post3, CRITICAL^0'=CRITICAL^post3, Q^0'=Q^post3, NONCRITICAL^0'=NONCRITICAL^post3, MAX^0'=MAX^post3, j_min^0'=j_min^post3, P^0'=P^post3, (0 == 0 /\ -INCREASE^post3+num^0 <= 0 /\ -CRITICAL^post3+CRITICAL^0 == 0 /\ -NONCRITICAL^post3+NONCRITICAL^0 == 0 /\ pid^0-pid^post3 == 0 /\ -MAX^post3+MAX^0 == 0 /\ -1+Q^post3 == 0 /\ INCREASE^post3-NUM_MIN^post3 <= 0 /\ MIN^0-num^0+NUM_MIN^post3 == 0 /\ MIN^0+MAX_MIN^post3-MAX^0 == 0 /\ num^0-num^post3 == 0 /\ -P^post3+P^0 == 0 /\ MIN^0+INCREASE^post3-MAX^0 <= 0 /\ 1-j_min^post3 <= 0 /\ -MIN^0-INCREASE^post3+MIN^post3 == 0 /\ 2-conditional^0 <= 0), cost: 1 4: l3 -> l2 : MIN^0'=MIN^post4, pid^0'=pid^post4, INCREASE^0'=INCREASE^post4, conditional^0'=conditional^post4, NUM_MIN^0'=NUM_MIN^post4, MAX_MIN^0'=MAX_MIN^post4, num^0'=num^post4, CRITICAL^0'=CRITICAL^post4, Q^0'=Q^post4, NONCRITICAL^0'=NONCRITICAL^post4, MAX^0'=MAX^post4, j_min^0'=j_min^post4, P^0'=P^post4, (0 == 0 /\ Q^0-Q^post4 == 0 /\ -NUM_MIN^post4+NUM_MIN^0 == 0 /\ -P^post4+P^0 == 0 /\ num^0-num^post4 == 0 /\ MAX^0-MAX^post4 == 0 /\ -MAX_MIN^post4+MAX_MIN^0 == 0 /\ -1+conditional^0 <= 0 /\ INCREASE^0-INCREASE^post4 == 0 /\ CRITICAL^0-CRITICAL^post4 == 0 /\ -NONCRITICAL^post4+NONCRITICAL^0 == 0 /\ -j_min^post4+j_min^0 == 0 /\ MIN^0-MIN^post4 == 0 /\ -pid^post4+pid^0 == 0), cost: 1 5: l3 -> l2 : MIN^0'=MIN^post5, pid^0'=pid^post5, INCREASE^0'=INCREASE^post5, conditional^0'=conditional^post5, NUM_MIN^0'=NUM_MIN^post5, MAX_MIN^0'=MAX_MIN^post5, num^0'=num^post5, CRITICAL^0'=CRITICAL^post5, Q^0'=Q^post5, NONCRITICAL^0'=NONCRITICAL^post5, MAX^0'=MAX^post5, j_min^0'=j_min^post5, P^0'=P^post5, (0 == 0 /\ MIN^0-MIN^post5 == 0 /\ 1-INCREASE^post5 <= 0 /\ num^0-num^post5 == 0 /\ -NUM_MIN^post5+NUM_MIN^0 == 0 /\ -CRITICAL^post5+CRITICAL^0 == 0 /\ -MAX_MIN^post5+MAX_MIN^0 == 0 /\ -j_min^post5+j_min^0 == 0 /\ Q^0-Q^post5 == 0 /\ -P^post5+P^0 == 0 /\ -INCREASE^post5+MAX^post5-MAX^0 == 0 /\ pid^0-pid^post5 == 0 /\ -NONCRITICAL^post5+NONCRITICAL^0 == 0 /\ 2-conditional^0 <= 0), cost: 1 9: l4 -> l1 : MIN^0'=MIN^post9, pid^0'=pid^post9, INCREASE^0'=INCREASE^post9, conditional^0'=conditional^post9, NUM_MIN^0'=NUM_MIN^post9, MAX_MIN^0'=MAX_MIN^post9, num^0'=num^post9, CRITICAL^0'=CRITICAL^post9, Q^0'=Q^post9, NONCRITICAL^0'=NONCRITICAL^post9, MAX^0'=MAX^post9, j_min^0'=j_min^post9, P^0'=P^post9, (conditional^0-conditional^post9 == 0 /\ -NUM_MIN^post9+NUM_MIN^0 == 0 /\ Q^0-Q^post9 == 0 /\ pid^0-pid^post9 == 0 /\ -MAX_MIN^post9+MAX_MIN^0 == 0 /\ -1+num^post9-MAX^0 == 0 /\ -1+NONCRITICAL^post9 == 0 /\ CRITICAL^post9 == 0 /\ INCREASE^0-INCREASE^post9 == 0 /\ -P^post9+P^0 == 0 /\ -j_min^post9+j_min^0 == 0 /\ -1-MAX^0+MAX^post9 == 0 /\ MIN^0-MIN^post9 == 0), cost: 1 10: l5 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, INCREASE^0'=INCREASE^post10, conditional^0'=conditional^post10, NUM_MIN^0'=NUM_MIN^post10, MAX_MIN^0'=MAX_MIN^post10, num^0'=num^post10, CRITICAL^0'=CRITICAL^post10, Q^0'=Q^post10, NONCRITICAL^0'=NONCRITICAL^post10, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=P^post10, (0 == 0 /\ conditional^0-conditional^post10 == 0 /\ -NUM_MIN^post10+NUM_MIN^0 == 0 /\ 1-MIN^post10 <= 0 /\ P^post10 == 0 /\ num^0-num^post10 == 0 /\ -MAX_MIN^post10+MAX_MIN^0 == 0 /\ CRITICAL^post10 == 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+NONCRITICAL^post10 == 0 /\ 1-pid^post10 <= 0 /\ 1-j_min^post10 <= 0 /\ Q^post10 == 0 /\ INCREASE^0-INCREASE^post10 == 0), cost: 1 11: l6 -> l5 : MIN^0'=MIN^post11, pid^0'=pid^post11, INCREASE^0'=INCREASE^post11, conditional^0'=conditional^post11, NUM_MIN^0'=NUM_MIN^post11, MAX_MIN^0'=MAX_MIN^post11, num^0'=num^post11, CRITICAL^0'=CRITICAL^post11, Q^0'=Q^post11, NONCRITICAL^0'=NONCRITICAL^post11, MAX^0'=MAX^post11, j_min^0'=j_min^post11, P^0'=P^post11, (-MAX_MIN^post11+MAX_MIN^0 == 0 /\ -P^post11+P^0 == 0 /\ conditional^0-conditional^post11 == 0 /\ -NONCRITICAL^post11+NONCRITICAL^0 == 0 /\ num^0-num^post11 == 0 /\ Q^0-Q^post11 == 0 /\ MAX^0-MAX^post11 == 0 /\ CRITICAL^0-CRITICAL^post11 == 0 /\ -j_min^post11+j_min^0 == 0 /\ INCREASE^0-INCREASE^post11 == 0 /\ MIN^0-MIN^post11 == 0 /\ NUM_MIN^0-NUM_MIN^post11 == 0 /\ -pid^post11+pid^0 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : MIN^0'=MIN^post0, pid^0'=pid^post0, INCREASE^0'=INCREASE^post0, conditional^0'=conditional^post0, NUM_MIN^0'=NUM_MIN^post0, MAX_MIN^0'=MAX_MIN^post0, num^0'=num^post0, CRITICAL^0'=CRITICAL^post0, Q^0'=Q^post0, NONCRITICAL^0'=NONCRITICAL^post0, MAX^0'=MAX^post0, j_min^0'=j_min^post0, P^0'=P^post0, (0 == 0 /\ -MAX_MIN^post0+MAX_MIN^0 == 0 /\ Q^0-Q^post0 == 0 /\ num^0-num^post0 == 0 /\ -P^post0+P^0 == 0 /\ -j_min^post0+j_min^0 == 0 /\ -CRITICAL^post0+CRITICAL^0 == 0 /\ INCREASE^0-INCREASE^post0 == 0 /\ -1+conditional^0 <= 0 /\ -MAX^post0+MAX^0 == 0 /\ -pid^post0+pid^0 == 0 /\ MIN^0-MIN^post0 == 0 /\ -NONCRITICAL^post0+NONCRITICAL^0 == 0 /\ NUM_MIN^0-NUM_MIN^post0 == 0), cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^post0, -1+conditional^0 <= 0, cost: 1 Applied preprocessing Original rule: l0 -> l1 : MIN^0'=MIN^post1, pid^0'=pid^post1, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=NUM_MIN^post1, MAX_MIN^0'=MAX_MIN^post1, num^0'=num^post1, CRITICAL^0'=CRITICAL^post1, Q^0'=Q^post1, NONCRITICAL^0'=NONCRITICAL^post1, MAX^0'=MAX^post1, j_min^0'=j_min^post1, P^0'=P^post1, (0 == 0 /\ pid^0-pid^post1 == 0 /\ j_min^post1-INCREASE^post1-j_min^0 == 0 /\ Q^0-Q^post1 == 0 /\ -CRITICAL^post1+CRITICAL^0 == 0 /\ 1-INCREASE^post1 <= 0 /\ num^0-num^post1 == 0 /\ -MAX^post1+MAX^0 == 0 /\ NUM_MIN^0-NUM_MIN^post1 == 0 /\ -MAX_MIN^post1+MAX_MIN^0 == 0 /\ -P^post1+P^0 == 0 /\ MIN^0-MIN^post1 == 0 /\ -NONCRITICAL^post1+NONCRITICAL^0 == 0 /\ 2-conditional^0 <= 0), cost: 1 New rule: l0 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, (-1+INCREASE^post1 >= 0 /\ -2+conditional^0 >= 0), cost: 1 Applied preprocessing Original rule: l2 -> l0 : MIN^0'=MIN^post2, pid^0'=pid^post2, INCREASE^0'=INCREASE^post2, conditional^0'=conditional^post2, NUM_MIN^0'=NUM_MIN^post2, MAX_MIN^0'=MAX_MIN^post2, num^0'=num^post2, CRITICAL^0'=CRITICAL^post2, Q^0'=Q^post2, NONCRITICAL^0'=NONCRITICAL^post2, MAX^0'=MAX^post2, j_min^0'=j_min^post2, P^0'=P^post2, (0 == 0 /\ -1+P^post2 == 0 /\ -NUM_MIN^post2+NUM_MIN^0 == 0 /\ MAX^0-MAX^post2 == 0 /\ num^0-num^post2 == 0 /\ MIN^0-MIN^post2 == 0 /\ Q^0-Q^post2 == 0 /\ -MAX_MIN^post2+MAX_MIN^0 == 0 /\ -NONCRITICAL^post2+NONCRITICAL^0 == 0 /\ -1+conditional^0 <= 0 /\ -pid^post2+pid^0 == 0 /\ -j_min^post2+j_min^0 == 0 /\ -CRITICAL^post2+CRITICAL^0 == 0 /\ INCREASE^0-INCREASE^post2 == 0), cost: 1 New rule: l2 -> l0 : conditional^0'=conditional^post2, P^0'=1, -1+conditional^0 <= 0, cost: 1 Applied preprocessing Original rule: l2 -> l1 : MIN^0'=MIN^post3, pid^0'=pid^post3, INCREASE^0'=INCREASE^post3, conditional^0'=conditional^post3, NUM_MIN^0'=NUM_MIN^post3, MAX_MIN^0'=MAX_MIN^post3, num^0'=num^post3, CRITICAL^0'=CRITICAL^post3, Q^0'=Q^post3, NONCRITICAL^0'=NONCRITICAL^post3, MAX^0'=MAX^post3, j_min^0'=j_min^post3, P^0'=P^post3, (0 == 0 /\ -INCREASE^post3+num^0 <= 0 /\ -CRITICAL^post3+CRITICAL^0 == 0 /\ -NONCRITICAL^post3+NONCRITICAL^0 == 0 /\ pid^0-pid^post3 == 0 /\ -MAX^post3+MAX^0 == 0 /\ -1+Q^post3 == 0 /\ INCREASE^post3-NUM_MIN^post3 <= 0 /\ MIN^0-num^0+NUM_MIN^post3 == 0 /\ MIN^0+MAX_MIN^post3-MAX^0 == 0 /\ num^0-num^post3 == 0 /\ -P^post3+P^0 == 0 /\ MIN^0+INCREASE^post3-MAX^0 <= 0 /\ 1-j_min^post3 <= 0 /\ -MIN^0-INCREASE^post3+MIN^post3 == 0 /\ 2-conditional^0 <= 0), cost: 1 New rule: l2 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (MIN^post3-MAX^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -2+conditional^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 1 Applied preprocessing Original rule: l3 -> l2 : MIN^0'=MIN^post4, pid^0'=pid^post4, INCREASE^0'=INCREASE^post4, conditional^0'=conditional^post4, NUM_MIN^0'=NUM_MIN^post4, MAX_MIN^0'=MAX_MIN^post4, num^0'=num^post4, CRITICAL^0'=CRITICAL^post4, Q^0'=Q^post4, NONCRITICAL^0'=NONCRITICAL^post4, MAX^0'=MAX^post4, j_min^0'=j_min^post4, P^0'=P^post4, (0 == 0 /\ Q^0-Q^post4 == 0 /\ -NUM_MIN^post4+NUM_MIN^0 == 0 /\ -P^post4+P^0 == 0 /\ num^0-num^post4 == 0 /\ MAX^0-MAX^post4 == 0 /\ -MAX_MIN^post4+MAX_MIN^0 == 0 /\ -1+conditional^0 <= 0 /\ INCREASE^0-INCREASE^post4 == 0 /\ CRITICAL^0-CRITICAL^post4 == 0 /\ -NONCRITICAL^post4+NONCRITICAL^0 == 0 /\ -j_min^post4+j_min^0 == 0 /\ MIN^0-MIN^post4 == 0 /\ -pid^post4+pid^0 == 0), cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^post4, -1+conditional^0 <= 0, cost: 1 Applied preprocessing Original rule: l3 -> l2 : MIN^0'=MIN^post5, pid^0'=pid^post5, INCREASE^0'=INCREASE^post5, conditional^0'=conditional^post5, NUM_MIN^0'=NUM_MIN^post5, MAX_MIN^0'=MAX_MIN^post5, num^0'=num^post5, CRITICAL^0'=CRITICAL^post5, Q^0'=Q^post5, NONCRITICAL^0'=NONCRITICAL^post5, MAX^0'=MAX^post5, j_min^0'=j_min^post5, P^0'=P^post5, (0 == 0 /\ MIN^0-MIN^post5 == 0 /\ 1-INCREASE^post5 <= 0 /\ num^0-num^post5 == 0 /\ -NUM_MIN^post5+NUM_MIN^0 == 0 /\ -CRITICAL^post5+CRITICAL^0 == 0 /\ -MAX_MIN^post5+MAX_MIN^0 == 0 /\ -j_min^post5+j_min^0 == 0 /\ Q^0-Q^post5 == 0 /\ -P^post5+P^0 == 0 /\ -INCREASE^post5+MAX^post5-MAX^0 == 0 /\ pid^0-pid^post5 == 0 /\ -NONCRITICAL^post5+NONCRITICAL^0 == 0 /\ 2-conditional^0 <= 0), cost: 1 New rule: l3 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^0 >= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 1 Applied preprocessing Original rule: l1 -> l3 : MIN^0'=MIN^post6, pid^0'=pid^post6, INCREASE^0'=INCREASE^post6, conditional^0'=conditional^post6, NUM_MIN^0'=NUM_MIN^post6, MAX_MIN^0'=MAX_MIN^post6, num^0'=num^post6, CRITICAL^0'=CRITICAL^post6, Q^0'=Q^post6, NONCRITICAL^0'=NONCRITICAL^post6, MAX^0'=MAX^post6, j_min^0'=j_min^post6, P^0'=P^post6, (0 == 0 /\ pid^0-pid^post6 == 0 /\ MAX^0-MAX^post6 == 0 /\ 1-pid^0+j_min^0 <= 0 /\ -CRITICAL^post6+CRITICAL^0 == 0 /\ INCREASE^0-INCREASE^post6 == 0 /\ MIN^0-num^0 <= 0 /\ Q^0-Q^post6 == 0 /\ num^0-num^post6 == 0 /\ MIN^0-MIN^post6 == 0 /\ NUM_MIN^0-NUM_MIN^post6 == 0 /\ -MAX_MIN^post6+MAX_MIN^0 == 0 /\ -NONCRITICAL^post6+NONCRITICAL^0 == 0 /\ -P^post6+P^0 == 0 /\ -j_min^post6+j_min^0 == 0), cost: 1 New rule: l1 -> l3 : conditional^0'=conditional^post6, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 1 Applied preprocessing Original rule: l1 -> l4 : MIN^0'=MIN^post7, pid^0'=pid^post7, INCREASE^0'=INCREASE^post7, conditional^0'=conditional^post7, NUM_MIN^0'=NUM_MIN^post7, MAX_MIN^0'=MAX_MIN^post7, num^0'=num^post7, CRITICAL^0'=CRITICAL^post7, Q^0'=Q^post7, NONCRITICAL^0'=NONCRITICAL^post7, MAX^0'=MAX^post7, j_min^0'=j_min^post7, P^0'=P^post7, (MAX^0-MAX^post7 == 0 /\ MIN^0-MIN^post7 == 0 /\ conditional^0-conditional^post7 == 0 /\ -MAX_MIN^post7+MAX_MIN^0 == 0 /\ num^0-num^post7 == 0 /\ -NONCRITICAL^post7+NONCRITICAL^0 == 0 /\ pid^0-j_min^0 <= 0 /\ P^post7 == 0 /\ INCREASE^0-INCREASE^post7 == 0 /\ -pid^post7+pid^0 == 0 /\ Q^post7 == 0 /\ -j_min^post7+j_min^0 == 0 /\ -1+CRITICAL^post7 == 0 /\ NUM_MIN^0-NUM_MIN^post7 == 0), cost: 1 New rule: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 Applied preprocessing Original rule: l1 -> l4 : MIN^0'=MIN^post8, pid^0'=pid^post8, INCREASE^0'=INCREASE^post8, conditional^0'=conditional^post8, NUM_MIN^0'=NUM_MIN^post8, MAX_MIN^0'=MAX_MIN^post8, num^0'=num^post8, CRITICAL^0'=CRITICAL^post8, Q^0'=Q^post8, NONCRITICAL^0'=NONCRITICAL^post8, MAX^0'=MAX^post8, j_min^0'=j_min^post8, P^0'=P^post8, (1-MIN^0+num^0 <= 0 /\ -NONCRITICAL^post8+NONCRITICAL^0 == 0 /\ -1+CRITICAL^post8 == 0 /\ pid^0-pid^post8 == 0 /\ conditional^0-conditional^post8 == 0 /\ -j_min^post8+j_min^0 == 0 /\ P^post8 == 0 /\ num^0-num^post8 == 0 /\ -MAX^post8+MAX^0 == 0 /\ INCREASE^0-INCREASE^post8 == 0 /\ NUM_MIN^0-NUM_MIN^post8 == 0 /\ Q^post8 == 0 /\ -MAX_MIN^post8+MAX_MIN^0 == 0 /\ MIN^0-MIN^post8 == 0), cost: 1 New rule: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 Applied preprocessing Original rule: l4 -> l1 : MIN^0'=MIN^post9, pid^0'=pid^post9, INCREASE^0'=INCREASE^post9, conditional^0'=conditional^post9, NUM_MIN^0'=NUM_MIN^post9, MAX_MIN^0'=MAX_MIN^post9, num^0'=num^post9, CRITICAL^0'=CRITICAL^post9, Q^0'=Q^post9, NONCRITICAL^0'=NONCRITICAL^post9, MAX^0'=MAX^post9, j_min^0'=j_min^post9, P^0'=P^post9, (conditional^0-conditional^post9 == 0 /\ -NUM_MIN^post9+NUM_MIN^0 == 0 /\ Q^0-Q^post9 == 0 /\ pid^0-pid^post9 == 0 /\ -MAX_MIN^post9+MAX_MIN^0 == 0 /\ -1+num^post9-MAX^0 == 0 /\ -1+NONCRITICAL^post9 == 0 /\ CRITICAL^post9 == 0 /\ INCREASE^0-INCREASE^post9 == 0 /\ -P^post9+P^0 == 0 /\ -j_min^post9+j_min^0 == 0 /\ -1-MAX^0+MAX^post9 == 0 /\ MIN^0-MIN^post9 == 0), cost: 1 New rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Applied preprocessing Original rule: l5 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, INCREASE^0'=INCREASE^post10, conditional^0'=conditional^post10, NUM_MIN^0'=NUM_MIN^post10, MAX_MIN^0'=MAX_MIN^post10, num^0'=num^post10, CRITICAL^0'=CRITICAL^post10, Q^0'=Q^post10, NONCRITICAL^0'=NONCRITICAL^post10, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=P^post10, (0 == 0 /\ conditional^0-conditional^post10 == 0 /\ -NUM_MIN^post10+NUM_MIN^0 == 0 /\ 1-MIN^post10 <= 0 /\ P^post10 == 0 /\ num^0-num^post10 == 0 /\ -MAX_MIN^post10+MAX_MIN^0 == 0 /\ CRITICAL^post10 == 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+NONCRITICAL^post10 == 0 /\ 1-pid^post10 <= 0 /\ 1-j_min^post10 <= 0 /\ Q^post10 == 0 /\ INCREASE^0-INCREASE^post10 == 0), cost: 1 New rule: l5 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 1 Applied preprocessing Original rule: l6 -> l5 : MIN^0'=MIN^post11, pid^0'=pid^post11, INCREASE^0'=INCREASE^post11, conditional^0'=conditional^post11, NUM_MIN^0'=NUM_MIN^post11, MAX_MIN^0'=MAX_MIN^post11, num^0'=num^post11, CRITICAL^0'=CRITICAL^post11, Q^0'=Q^post11, NONCRITICAL^0'=NONCRITICAL^post11, MAX^0'=MAX^post11, j_min^0'=j_min^post11, P^0'=P^post11, (-MAX_MIN^post11+MAX_MIN^0 == 0 /\ -P^post11+P^0 == 0 /\ conditional^0-conditional^post11 == 0 /\ -NONCRITICAL^post11+NONCRITICAL^0 == 0 /\ num^0-num^post11 == 0 /\ Q^0-Q^post11 == 0 /\ MAX^0-MAX^post11 == 0 /\ CRITICAL^0-CRITICAL^post11 == 0 /\ -j_min^post11+j_min^0 == 0 /\ INCREASE^0-INCREASE^post11 == 0 /\ MIN^0-MIN^post11 == 0 /\ NUM_MIN^0-NUM_MIN^post11 == 0 /\ -pid^post11+pid^0 == 0), cost: 1 New rule: l6 -> l5 : TRUE, cost: 1 Simplified rules Start location: l6 12: l0 -> l1 : conditional^0'=conditional^post0, -1+conditional^0 <= 0, cost: 1 13: l0 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, (-1+INCREASE^post1 >= 0 /\ -2+conditional^0 >= 0), cost: 1 18: l1 -> l3 : conditional^0'=conditional^post6, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 1 19: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 20: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 14: l2 -> l0 : conditional^0'=conditional^post2, P^0'=1, -1+conditional^0 <= 0, cost: 1 15: l2 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (MIN^post3-MAX^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -2+conditional^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 1 16: l3 -> l2 : conditional^0'=conditional^post4, -1+conditional^0 <= 0, cost: 1 17: l3 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^0 >= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 1 21: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 22: l5 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 1 23: l6 -> l5 : TRUE, cost: 1 Eliminating location l5 by chaining: Applied chaining First rule: l6 -> l5 : TRUE, cost: 1 Second rule: l5 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 1 New rule: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Applied deletion Removed the following rules: 22 23 Eliminated locations on linear paths Start location: l6 12: l0 -> l1 : conditional^0'=conditional^post0, -1+conditional^0 <= 0, cost: 1 13: l0 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, (-1+INCREASE^post1 >= 0 /\ -2+conditional^0 >= 0), cost: 1 18: l1 -> l3 : conditional^0'=conditional^post6, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 1 19: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 20: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 14: l2 -> l0 : conditional^0'=conditional^post2, P^0'=1, -1+conditional^0 <= 0, cost: 1 15: l2 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (MIN^post3-MAX^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -2+conditional^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 1 16: l3 -> l2 : conditional^0'=conditional^post4, -1+conditional^0 <= 0, cost: 1 17: l3 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^0 >= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 1 21: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Eliminating location l3 by chaining: Applied chaining First rule: l1 -> l3 : conditional^0'=conditional^post6, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 1 Second rule: l3 -> l2 : conditional^0'=conditional^post4, -1+conditional^0 <= 0, cost: 1 New rule: l1 -> l2 : conditional^0'=conditional^post4, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post6 <= 0), cost: 2 Applied chaining First rule: l1 -> l3 : conditional^0'=conditional^post6, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 1 Second rule: l3 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^0 >= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 1 New rule: l1 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 2 Applied deletion Removed the following rules: 16 17 18 Eliminating location l0 by chaining: Applied chaining First rule: l2 -> l0 : conditional^0'=conditional^post2, P^0'=1, -1+conditional^0 <= 0, cost: 1 Second rule: l0 -> l1 : conditional^0'=conditional^post0, -1+conditional^0 <= 0, cost: 1 New rule: l2 -> l1 : conditional^0'=conditional^post0, P^0'=1, (-1+conditional^0 <= 0 /\ -1+conditional^post2 <= 0), cost: 2 Applied chaining First rule: l2 -> l0 : conditional^0'=conditional^post2, P^0'=1, -1+conditional^0 <= 0, cost: 1 Second rule: l0 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, (-1+INCREASE^post1 >= 0 /\ -2+conditional^0 >= 0), cost: 1 New rule: l2 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (-2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^0 <= 0), cost: 2 Applied deletion Removed the following rules: 12 13 14 Eliminated locations on tree-shaped paths Start location: l6 19: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 20: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 25: l1 -> l2 : conditional^0'=conditional^post4, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post6 <= 0), cost: 2 26: l1 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 2 15: l2 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (MIN^post3-MAX^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -2+conditional^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 1 27: l2 -> l1 : conditional^0'=conditional^post0, P^0'=1, (-1+conditional^0 <= 0 /\ -1+conditional^post2 <= 0), cost: 2 28: l2 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (-2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^0 <= 0), cost: 2 21: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Eliminating location l2 by chaining: Applied chaining First rule: l1 -> l2 : conditional^0'=conditional^post4, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post6 <= 0), cost: 2 Second rule: l2 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (MIN^post3-MAX^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -2+conditional^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 1 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-2+conditional^post4 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+conditional^post6 <= 0), cost: 3 Applied chaining First rule: l1 -> l2 : conditional^0'=conditional^post4, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post6 <= 0), cost: 2 Second rule: l2 -> l1 : conditional^0'=conditional^post0, P^0'=1, (-1+conditional^0 <= 0 /\ -1+conditional^post2 <= 0), cost: 2 New rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post2 <= 0 /\ -1+conditional^post4 <= 0 /\ -1+conditional^post6 <= 0), cost: 4 Applied chaining First rule: l1 -> l2 : conditional^0'=conditional^post4, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post6 <= 0), cost: 2 Second rule: l2 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (-2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^0 <= 0), cost: 2 New rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^post4 <= 0 /\ -1+conditional^post6 <= 0), cost: 4 Applied chaining First rule: l1 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 2 Second rule: l2 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (MIN^post3-MAX^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -2+conditional^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 1 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^post5, Q^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -2+conditional^post5 >= 0 /\ -MAX^post5+MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 Applied chaining First rule: l1 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 2 Second rule: l2 -> l1 : conditional^0'=conditional^post0, P^0'=1, (-1+conditional^0 <= 0 /\ -1+conditional^post2 <= 0), cost: 2 New rule: l1 -> l1 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post0, MAX^0'=MAX^post5, P^0'=1, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post5 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -1+conditional^post2 <= 0), cost: 4 Applied chaining First rule: l1 -> l2 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post5, MAX^0'=MAX^post5, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 2 Second rule: l2 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (-2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^0 <= 0), cost: 2 New rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^post5 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 Applied deletion Removed the following rules: 15 25 26 27 28 Eliminated locations on tree-shaped paths Start location: l6 19: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 20: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 29: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-2+conditional^post4 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+conditional^post6 <= 0), cost: 3 30: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post2 <= 0 /\ -1+conditional^post4 <= 0 /\ -1+conditional^post6 <= 0), cost: 4 31: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^post4 <= 0 /\ -1+conditional^post6 <= 0), cost: 4 32: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^post5, Q^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -2+conditional^post5 >= 0 /\ -MAX^post5+MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 33: l1 -> l1 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post0, MAX^0'=MAX^post5, P^0'=1, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post5 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -1+conditional^post2 <= 0), cost: 4 34: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^post5 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 21: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Applied simplification Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-2+conditional^post4 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+conditional^post6 <= 0), cost: 3 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 Applied simplification Original rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post2 <= 0 /\ -1+conditional^post4 <= 0 /\ -1+conditional^post6 <= 0), cost: 4 New rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 Applied simplification Original rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^post4 <= 0 /\ -1+conditional^post6 <= 0), cost: 4 New rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 Applied simplification Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^post5, Q^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -2+conditional^post5 >= 0 /\ -MAX^post5+MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^post5, Q^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -MAX^post5+MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 Applied simplification Original rule: l1 -> l1 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post0, MAX^0'=MAX^post5, P^0'=1, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+conditional^post5 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -1+conditional^post2 <= 0), cost: 4 New rule: l1 -> l1 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post0, MAX^0'=MAX^post5, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 Applied simplification Original rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (-2+conditional^post6 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -2+conditional^post2 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+conditional^post5 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 New rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 Simplified simple loops Start location: l6 19: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 20: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 35: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 36: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 37: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 38: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^post5, Q^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -MAX^post5+MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 39: l1 -> l1 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post0, MAX^0'=MAX^post5, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 40: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 21: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Applied unrolling Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ num^0 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 6 Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ num^0 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 6 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_Mmcgei.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ num^0 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 6 New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_IpJigg.txt Applied nonterm Original rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -1+n0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_kDlloe.txt Applied acceleration Original rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 New rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1*n1+j_min^0, P^0'=1, (-MIN^0+num^0 >= 0 /\ -1+n1 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1-(-1+n1)*INCREASE^post1+pid^0-j_min^0 >= 0), cost: 4*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_jmAFNG.txt Applied instantiation Original rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1*n1+j_min^0, P^0'=1, (-MIN^0+num^0 >= 0 /\ -1+n1 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1-(-1+n1)*INCREASE^post1+pid^0-j_min^0 >= 0), cost: 4*n1 New rule: l1 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, j_min^0'=pid^0, P^0'=1, (0 >= 0 /\ -MIN^0+num^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 4*pid^0-4*j_min^0 Applied chaining First rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 Second rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (MIN^post3-MAX^0 <= 0 /\ 2-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 7 Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (MIN^post3-MAX^0 <= 0 /\ 2-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 7 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -2+n16 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 7*n16 Sub-proof via acceration calculus written to file:///tmp/tmpnam_iPaLBI.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (MIN^post3-MAX^0 <= 0 /\ 2-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 7 New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_kgbccM.txt Applied chaining First rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (0 <= 0 /\ -num^0 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 Second rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 7 Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 7 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2+n21 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 7*n21 Sub-proof via acceration calculus written to file:///tmp/tmpnam_meHNiK.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 7 New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_KeBmkO.txt Applied chaining First rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (0 <= 0 /\ -num^0 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 Second rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3+INCREASE^post1, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -1+INCREASE^post1 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 7 Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3+INCREASE^post1, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -1+INCREASE^post1 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 7 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3+INCREASE^post1, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -2+n25 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0 /\ -1-j_min^post3+pid^0-INCREASE^post1 >= 0), cost: 7*n25 Sub-proof via acceration calculus written to file:///tmp/tmpnam_ndbGlJ.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3+INCREASE^post1, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -1+INCREASE^post1 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 7 New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_gPeldc.txt Applied chaining First rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 Second rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post0, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 7 Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post0, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 7 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post0, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -2+n26 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 7*n26 Sub-proof via acceration calculus written to file:///tmp/tmpnam_emPiDE.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post0, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0), cost: 7 New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_LicknO.txt Applied chaining First rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 Second rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ 2-pid^0+j_min^0 <= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ 2-pid^0+j_min^0 <= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -1+n36 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 4*n36+6*n36*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_KkNlkN.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ 2-pid^0+j_min^0 <= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_ifokfA.txt Applied chaining First rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (0 <= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n Second rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3+INCREASE^post1, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3+INCREASE^post1, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3+INCREASE^post1, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1+n37 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0 /\ -1-j_min^post3+pid^0-INCREASE^post1 >= 0), cost: 6*n37*n+4*n37 Sub-proof via acceration calculus written to file:///tmp/tmpnam_ioKhbl.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3+INCREASE^post1, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_iKBcJh.txt Applied chaining First rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0), cost: 4 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 Second rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+n38 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 4*n38+6*n38*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_nNaBPb.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_EHpkkA.txt Applied chaining First rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (0 <= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied chaining First rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n Second rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post0, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n Applied acceleration Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post0, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n New rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post0, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-1+n39 >= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n39*n+4*n39 Sub-proof via acceration calculus written to file:///tmp/tmpnam_GpDPlI.txt Applied nonterm Original rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post0, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, P^0'=1, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ 1+j_min^post3-pid^0 <= 0 /\ num^0-MIN^post3 >= 0), cost: 4+6*n New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_DhPeKA.txt Applied chaining First rule: l1 -> l1 : conditional^0'=conditional^post0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0), cost: 4 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, j_min^0'=pid^0, P^0'=1, (0 >= 0 /\ -MIN^0+num^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 4*pid^0-4*j_min^0 New rule: l1 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, j_min^0'=pid^0, P^0'=1, (-MIN^0+num^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 4*pid^0-4*j_min^0 Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (0 <= 0 /\ -num^0 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ num^0 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (0 <= 0 /\ -num^0 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^post3-MAX^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ num^0 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0-num^0+MIN^post3 >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (0 <= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1+n >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (0 <= 0 /\ -MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM Applied simplification Original rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ 1-pid^0+j_min^0 <= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l1 -> [7] : (-MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM Applied deletion Removed the following rules: 35 36 37 Accelerated simple loops Start location: l6 19: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 20: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 38: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^post5, Q^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -MAX^post5+MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 39: l1 -> l1 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post0, MAX^0'=MAX^post5, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 40: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 41: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n 43: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -1+n0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 60: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 61: l1 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, j_min^0'=pid^0, P^0'=1, (-MIN^0+num^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 4*pid^0-4*j_min^0 62: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 63: l1 -> [7] : (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ num^0 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM 64: l1 -> [7] : (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ num^0 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM 65: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 66: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 67: l1 -> [7] : (-MIN^0-num^0+MIN^post3 >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 68: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 69: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM 70: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1+n >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 71: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 72: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 73: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM 74: l1 -> [7] : (-MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM 21: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=-MIN^0+num^0, MAX_MIN^0'=-MIN^0+MAX^post5, Q^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ 1-MAX^post5+MAX^0 <= 0 /\ -MAX^post5+MIN^post3 <= 0 /\ -num^0+MIN^post3 <= 0 /\ -1+j_min^post3 >= 0), cost: 3 New rule: l4 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^0+MAX^0, MAX_MIN^0'=-MIN^0+MAX^post5, num^0'=1+MAX^0, CRITICAL^0'=0, Q^0'=1, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ -1+MIN^post3-MAX^0 <= 0 /\ 1+MIN^0-MIN^post3+MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 4 Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> l1 : INCREASE^0'=MAX^post5-MAX^0, conditional^0'=conditional^post0, MAX^0'=MAX^post5, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 New rule: l4 -> l1 : INCREASE^0'=-1+MAX^post5-MAX^0, conditional^0'=conditional^post0, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ 1-MAX^post5+MAX^0 <= 0), cost: 4 New rule: l4 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=num^0-MIN^post3, MAX_MIN^0'=-MIN^post3+MAX^0, Q^0'=1, j_min^0'=j_min^post3, (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: 6*n New rule: l4 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^post3+MAX^0, MAX_MIN^0'=1-MIN^post3+MAX^0, num^0'=1+MAX^0, CRITICAL^0'=0, Q^0'=1, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=j_min^post3, (-1+n >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ 1-MIN^post3+MAX^0 >= 0 /\ -1-MIN^0+MIN^post3-MAX^0 >= 0 /\ -1-MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: 1+6*n Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -1+n0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM New rule: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, j_min^0'=pid^0, P^0'=1, (-MIN^0+num^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 4*pid^0-4*j_min^0 New rule: l4 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=1, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 1+4*pid^0-4*j_min^0 Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (-2+pid^0-j_min^0 >= 0 /\ 1-j_min^0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ num^0 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 3-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (1-pid^0+j_min^0 <= 0 /\ MIN^0-num^0 <= 0 /\ MIN^0+num^0-MIN^post3 <= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ num^0 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 2-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -2+j_min^0 >= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (2-pid^0+j_min^0 <= 0 /\ -1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0-num^0+MIN^post3 >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -2+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (-2+pid^0-j_min^0 >= 0 /\ 1-j_min^0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -2-j_min^post3+pid^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (-3+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ j_min^post3+INCREASE^post1-j_min^0 <= 0 /\ -1+n >= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -2+j_min^0 >= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-1+pid^0-INCREASE^post1-j_min^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (2-pid^0+j_min^0 <= 0 /\ -1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0+num^0 >= 0 /\ -MIN^0-num^0+MIN^post3 >= 0 /\ -num^0 >= 0 /\ -1+n >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0 /\ num^0-MIN^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (-2+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> [7] : (-MIN^0-num^0+MIN^post3 >= 0 /\ -1+n >= 0 /\ MIN^0-num^0 <= 0 /\ j_min^post3-j_min^0 <= 0 /\ -MIN^0+MIN^post3 <= 0 /\ -MIN^post3+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: NONTERM New rule: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM Applied deletion Removed the following rules: 38 39 40 41 43 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 Chained accelerated rules with incoming rules Start location: l6 19: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 20: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 21: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 75: l4 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^0+MAX^0, MAX_MIN^0'=-MIN^0+MAX^post5, num^0'=1+MAX^0, CRITICAL^0'=0, Q^0'=1, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ -1+MIN^post3-MAX^0 <= 0 /\ 1+MIN^0-MIN^post3+MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 4 76: l4 -> l1 : INCREASE^0'=-1+MAX^post5-MAX^0, conditional^0'=conditional^post0, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 77: l4 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 78: l4 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^post3+MAX^0, MAX_MIN^0'=1-MIN^post3+MAX^0, num^0'=1+MAX^0, CRITICAL^0'=0, Q^0'=1, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=j_min^post3, (-1+n >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ 1-MIN^post3+MAX^0 >= 0 /\ -1-MIN^0+MIN^post3-MAX^0 >= 0 /\ -1-MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: 1+6*n 79: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 80: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 81: l4 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=1, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 1+4*pid^0-4*j_min^0 82: l4 -> [7] : (-2+pid^0-j_min^0 >= 0 /\ 1-j_min^0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0), cost: NONTERM 83: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 3-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 84: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 2-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 85: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -2+j_min^0 >= 0), cost: NONTERM 86: l4 -> [7] : (2-pid^0+j_min^0 <= 0 /\ -1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 87: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 88: l4 -> [7] : (-3+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 89: l4 -> [7] : (-2+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Eliminating location l1 by chaining: Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 New rule: l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, P^0'=0, pid^0-j_min^0 <= 0, cost: 2 Applied chaining First rule: l4 -> l1 : num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, TRUE, cost: 1 Second rule: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, 1-MIN^0+num^0 <= 0, cost: 1 New rule: l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, P^0'=0, 2-MIN^0+MAX^0 <= 0, cost: 2 Applied chaining First rule: l4 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^0+MAX^0, MAX_MIN^0'=-MIN^0+MAX^post5, num^0'=1+MAX^0, CRITICAL^0'=0, Q^0'=1, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, (1-pid^0+j_min^0 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ -1+MIN^post3-MAX^0 <= 0 /\ 1+MIN^0-MIN^post3+MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 4 Second rule: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 New rule: l4 -> l4 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^0+MAX^0, MAX_MIN^0'=-MIN^0+MAX^post5, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ -j_min^post3+pid^0 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ -1+MIN^post3-MAX^0 <= 0 /\ 1+MIN^0-MIN^post3+MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 Applied chaining First rule: l4 -> l1 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=1, (1-pid^0+j_min^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 Second rule: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 New rule: l4 -> l4 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ pid^0-INCREASE^post1-j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 6 Applied simplification Original rule: l4 -> l4 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ -1+INCREASE^post1 >= 0 /\ pid^0-INCREASE^post1-j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 6 New rule: l4 -> l4 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ pid^0-INCREASE^post1-j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 6 Applied chaining First rule: l4 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=1, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 1+4*pid^0-4*j_min^0 Second rule: l1 -> l4 : CRITICAL^0'=1, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1 New rule: l4 -> l4 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=0, (0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 2+4*pid^0-4*j_min^0 Applied simplification Original rule: l4 -> l4 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=0, (0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 2+4*pid^0-4*j_min^0 New rule: l4 -> l4 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=0, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 2+4*pid^0-4*j_min^0 Applied partial deletion Original rule: l4 -> l1 : MIN^0'=MIN^post3, INCREASE^0'=0, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^post3+MAX^0, MAX_MIN^0'=1-MIN^post3+MAX^0, num^0'=1+MAX^0, CRITICAL^0'=0, Q^0'=1, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=j_min^post3, (-1+n >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ 1-MIN^post3+MAX^0 >= 0 /\ -1-MIN^0+MIN^post3-MAX^0 >= 0 /\ -1-MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: 1+6*n New rule: l4 -> [8] : (-1+n >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ 1-MIN^post3+MAX^0 >= 0 /\ -1-MIN^0+MIN^post3-MAX^0 >= 0 /\ -1-MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: 1+6*n Applied partial deletion Original rule: l4 -> l1 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=1, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 1+4*pid^0-4*j_min^0 New rule: l4 -> [8] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 1+4*pid^0-4*j_min^0 Applied deletion Removed the following rules: 19 20 21 75 76 77 78 81 Eliminated locations on tree-shaped paths Start location: l6 79: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 80: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 82: l4 -> [7] : (-2+pid^0-j_min^0 >= 0 /\ 1-j_min^0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0), cost: NONTERM 83: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 3-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 84: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 2-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 85: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -2+j_min^0 >= 0), cost: NONTERM 86: l4 -> [7] : (2-pid^0+j_min^0 <= 0 /\ -1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 87: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 88: l4 -> [7] : (-3+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 89: l4 -> [7] : (-2+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 90: l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, P^0'=0, pid^0-j_min^0 <= 0, cost: 2 91: l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, P^0'=0, 2-MIN^0+MAX^0 <= 0, cost: 2 92: l4 -> l4 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^0+MAX^0, MAX_MIN^0'=-MIN^0+MAX^post5, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ -j_min^post3+pid^0 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ -1+MIN^post3-MAX^0 <= 0 /\ 1+MIN^0-MIN^post3+MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 93: l4 -> l4 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ pid^0-INCREASE^post1-j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 6 94: l4 -> l4 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=0, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 2+4*pid^0-4*j_min^0 95: l4 -> [8] : (-1+n >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ -1-j_min^post3+pid^0 >= 0 /\ 1-MIN^post3+MAX^0 >= 0 /\ -1-MIN^0+MIN^post3-MAX^0 >= 0 /\ -1-MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+j_min^post3 >= 0), cost: 1+6*n 96: l4 -> [8] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 1+4*pid^0-4*j_min^0 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Applied pruning (of leafs and parallel rules): Start location: l6 79: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 80: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 82: l4 -> [7] : (-2+pid^0-j_min^0 >= 0 /\ 1-j_min^0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0), cost: NONTERM 83: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 3-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 84: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 2-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 85: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -2+j_min^0 >= 0), cost: NONTERM 86: l4 -> [7] : (2-pid^0+j_min^0 <= 0 /\ -1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 87: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 88: l4 -> [7] : (-3+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 89: l4 -> [7] : (-2+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 90: l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, P^0'=0, pid^0-j_min^0 <= 0, cost: 2 91: l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, P^0'=0, 2-MIN^0+MAX^0 <= 0, cost: 2 92: l4 -> l4 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^0+MAX^0, MAX_MIN^0'=-MIN^0+MAX^post5, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ -j_min^post3+pid^0 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ -1+MIN^post3-MAX^0 <= 0 /\ 1+MIN^0-MIN^post3+MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 93: l4 -> l4 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ pid^0-INCREASE^post1-j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 6 94: l4 -> l4 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=0, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 2+4*pid^0-4*j_min^0 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Applied nonterm Original rule: l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, P^0'=0, pid^0-j_min^0 <= 0, cost: 2 New rule: l4 -> [9] : (-pid^0+j_min^0 >= 0 /\ -1+n42 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_KiNooh.txt Applied acceleration Original rule: l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, P^0'=0, 2-MIN^0+MAX^0 <= 0, cost: 2 New rule: l4 -> l4 : num^0'=MAX^0+n43, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^0+n43, P^0'=0, (-1+n43 >= 0 /\ -1+MIN^0-MAX^0-n43 >= 0), cost: 2*n43 Sub-proof via acceration calculus written to file:///tmp/tmpnam_KAnBBb.txt Applied instantiation Original rule: l4 -> l4 : num^0'=MAX^0+n43, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^0+n43, P^0'=0, (-1+n43 >= 0 /\ -1+MIN^0-MAX^0-n43 >= 0), cost: 2*n43 New rule: l4 -> l4 : num^0'=-1+MIN^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=-1+MIN^0, P^0'=0, (0 >= 0 /\ -2+MIN^0-MAX^0 >= 0), cost: -2+2*MIN^0-2*MAX^0 Applied simplification Original rule: l4 -> l4 : num^0'=-1+MIN^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=-1+MIN^0, P^0'=0, (0 >= 0 /\ -2+MIN^0-MAX^0 >= 0), cost: -2+2*MIN^0-2*MAX^0 New rule: l4 -> l4 : num^0'=-1+MIN^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=-1+MIN^0, P^0'=0, -2+MIN^0-MAX^0 >= 0, cost: -2+2*MIN^0-2*MAX^0 Applied deletion Removed the following rules: 90 91 Accelerated simple loops Start location: l6 79: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 80: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 82: l4 -> [7] : (-2+pid^0-j_min^0 >= 0 /\ 1-j_min^0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0), cost: NONTERM 83: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 3-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 84: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 2-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 85: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -2+j_min^0 >= 0), cost: NONTERM 86: l4 -> [7] : (2-pid^0+j_min^0 <= 0 /\ -1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 87: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 88: l4 -> [7] : (-3+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 89: l4 -> [7] : (-2+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 92: l4 -> l4 : MIN^0'=MIN^post3, INCREASE^0'=-MIN^0+MIN^post3, conditional^0'=conditional^post3, NUM_MIN^0'=1-MIN^0+MAX^0, MAX_MIN^0'=-MIN^0+MAX^post5, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post3, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ -j_min^post3+pid^0 <= 0 /\ -1+j_min^post3 >= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ -1+MIN^post3-MAX^0 <= 0 /\ 1+MIN^0-MIN^post3+MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 5 93: l4 -> l4 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ pid^0-INCREASE^post1-j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 6 94: l4 -> l4 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=0, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 2+4*pid^0-4*j_min^0 97: l4 -> [9] : (-pid^0+j_min^0 >= 0 /\ -1+n42 >= 0), cost: NONTERM 99: l4 -> l4 : num^0'=-1+MIN^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=-1+MIN^0, P^0'=0, -2+MIN^0-MAX^0 >= 0, cost: -2+2*MIN^0-2*MAX^0 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Applied chaining First rule: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Second rule: l4 -> l4 : INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=INCREASE^post1+j_min^0, P^0'=0, (1-pid^0+j_min^0 <= 0 /\ pid^0-INCREASE^post1-j_min^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0 /\ 2-MAX^post5+MAX^0 <= 0), cost: 6 New rule: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^post10, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post10+INCREASE^post1, P^0'=0, (-j_min^post10+pid^post10-INCREASE^post1 <= 0 /\ -1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0 /\ 1+j_min^post10-pid^post10 <= 0 /\ 2-MAX^post5+MAX^post10 <= 0), cost: 8 Applied chaining First rule: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Second rule: l4 -> l4 : INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^0, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^0, j_min^0'=pid^0, P^0'=0, (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: 2+4*pid^0-4*j_min^0 New rule: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^post10, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^post10, j_min^0'=pid^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0), cost: 4-4*j_min^post10+4*pid^post10 Applied chaining First rule: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Second rule: l4 -> [9] : (-pid^0+j_min^0 >= 0 /\ -1+n42 >= 0), cost: NONTERM New rule: l6 -> [9] : TRUE, cost: NONTERM Applied deletion Removed the following rules: 92 93 94 97 99 Chained accelerated rules with incoming rules Start location: l6 79: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 80: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 82: l4 -> [7] : (-2+pid^0-j_min^0 >= 0 /\ 1-j_min^0 <= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0), cost: NONTERM 83: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 3-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 84: l4 -> [7] : (1-pid^0+j_min^0 <= 0 /\ 2-pid^0 <= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 85: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -2+j_min^0 >= 0), cost: NONTERM 86: l4 -> [7] : (2-pid^0+j_min^0 <= 0 /\ -1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 87: l4 -> [7] : (-1+j_min^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0 /\ -1+MIN^0-MAX^0 <= 0), cost: NONTERM 88: l4 -> [7] : (-3+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 89: l4 -> [7] : (-2+pid^0 >= 0 /\ 1-MIN^0+MAX^0 >= 0 /\ 1+MAX^0 <= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM 24: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 100: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, INCREASE^0'=INCREASE^post1, conditional^0'=conditional^post1, num^0'=1+MAX^post10, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post5, j_min^0'=j_min^post10+INCREASE^post1, P^0'=0, (-j_min^post10+pid^post10-INCREASE^post1 <= 0 /\ -1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0 /\ 1+j_min^post10-pid^post10 <= 0 /\ 2-MAX^post5+MAX^post10 <= 0), cost: 8 101: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^post10, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^post10, j_min^0'=pid^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0), cost: 4-4*j_min^post10+4*pid^post10 102: l6 -> [9] : TRUE, cost: NONTERM Eliminating location l4 by chaining: Applied chaining First rule: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, CRITICAL^0'=0, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=MAX^post10, j_min^0'=j_min^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: 2 Second rule: l4 -> [7] : (1-MIN^0+MAX^0 >= 0 /\ -1+pid^0-j_min^0 >= 0), cost: NONTERM New rule: l6 -> [7] : (1+MAX^post10-MIN^post10 >= 0 /\ -1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: NONTERM Applied simplification Original rule: l6 -> [7] : (1+MAX^post10-MIN^post10 >= 0 /\ -1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+pid^post10 >= 0 /\ -1+j_min^post10 >= 0), cost: NONTERM New rule: l6 -> [7] : (-1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0), cost: NONTERM Applied partial deletion Original rule: l6 -> l4 : MIN^0'=MIN^post10, pid^0'=pid^post10, INCREASE^0'=1, conditional^0'=conditional^post1, num^0'=1+MAX^post10, CRITICAL^0'=1, Q^0'=0, NONCRITICAL^0'=1, MAX^0'=1+MAX^post10, j_min^0'=pid^post10, P^0'=0, (-1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0), cost: 4-4*j_min^post10+4*pid^post10 New rule: l6 -> [10] : (-1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0), cost: 4-4*j_min^post10+4*pid^post10 Applied deletion Removed the following rules: 24 79 80 82 83 84 85 86 87 88 89 100 101 Eliminated locations on tree-shaped paths Start location: l6 102: l6 -> [9] : TRUE, cost: NONTERM 103: l6 -> [7] : (-1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0), cost: NONTERM 104: l6 -> [10] : (-1+MIN^post10 >= 0 /\ -1-j_min^post10+pid^post10 >= 0 /\ -MAX^post10+MIN^post10 <= 0 /\ -1+j_min^post10 >= 0), cost: 4-4*j_min^post10+4*pid^post10 Computing asymptotic complexity Proved nontermination of rule 102 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: TRUE