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 /\ CRITICAL^post7 == 0 /\ INCREASE^0-INCREASE^post7 == 0 /\ -pid^post7+pid^0 == 0 /\ Q^post7 == 0 /\ -j_min^post7+j_min^0 == 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 /\ 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 /\ CRITICAL^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 /\ CRITICAL^post7 == 0 /\ INCREASE^0-INCREASE^post7 == 0 /\ -pid^post7+pid^0 == 0 /\ Q^post7 == 0 /\ -j_min^post7+j_min^0 == 0 /\ NUM_MIN^0-NUM_MIN^post7 == 0), cost: 1
New rule:
l1 -> l4 : CRITICAL^0'=0, 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 /\ 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 /\ CRITICAL^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'=0, 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'=0, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1
  20: l1 -> l4 : CRITICAL^0'=0, 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'=0, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1
  20: l1 -> l4 : CRITICAL^0'=0, 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'=0, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1
  20: l1 -> l4 : CRITICAL^0'=0, 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'=0, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1
  20: l1 -> l4 : CRITICAL^0'=0, 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'=0, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1
  20: l1 -> l4 : CRITICAL^0'=0, 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_EPpGKC.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_cbPegB.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_EfGGpd.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_LCHKFb.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_dfBjPg.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_fbCaHM.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_DoNBKN.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_mLEOHo.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_jKHCBp.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_jnIFLG.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_hFnpNc.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_Kmdijh.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_PdlPkE.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_kcDpee.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_ddMbPc.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_bikafG.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_HbiMiJ.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_OlhFNm.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_JkhEmD.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_oBMJNa.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'=0, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1
  20: l1 -> l4 : CRITICAL^0'=0, 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'=0, Q^0'=0, P^0'=0, pid^0-j_min^0 <= 0, cost: 1
  20: l1 -> l4 : CRITICAL^0'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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_hJBPLC.txt

Applied acceleration
Original rule:
l4 -> l4 : num^0'=1+MAX^0, CRITICAL^0'=0, 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'=0, 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_cnOcOh.txt

Applied instantiation
Original rule:
l4 -> l4 : num^0'=MAX^0+n43, CRITICAL^0'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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'=0, 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