NO Initial ITS Start location: l12 0: l0 -> l1 : __rho_5_^0'=__rho_5_^post0, wakend^0'=wakend^post0, __rho_1_^0'=__rho_1_^post0, got_SIGHUP^0'=got_SIGHUP^post0, __rho_7_^0'=__rho_7_^post0, __rho_4_^0'=__rho_4_^post0, tt1^0'=tt1^post0, __const_1000^0'=__const_1000^post0, curtime^0'=curtime^post0, __rho_6_^0'=__rho_6_^post0, __rho_2_^0'=__rho_2_^post0, last_copy_time^0'=last_copy_time^post0, a22^0'=a22^post0, (-__rho_4_^post0+__rho_4_^0 == 0 /\ got_SIGHUP^0 <= 0 /\ curtime^0-curtime^post0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post0 == 0 /\ tt1^0-tt1^post0 == 0 /\ -a22^post0+a22^0 == 0 /\ -last_copy_time^post0+last_copy_time^0 == 0 /\ -__const_1000^post0+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ -__rho_2_^post0+__rho_2_^0 == 0 /\ -wakend^post0+wakend^0 == 0 /\ __rho_5_^0-__rho_5_^post0 == 0 /\ -__rho_6_^post0+__rho_6_^0 == 0 /\ __rho_7_^0-__rho_7_^post0 == 0), cost: 1 1: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=wakend^post1, __rho_1_^0'=__rho_1_^post1, got_SIGHUP^0'=got_SIGHUP^post1, __rho_7_^0'=__rho_7_^post1, __rho_4_^0'=__rho_4_^post1, tt1^0'=tt1^post1, __const_1000^0'=__const_1000^post1, curtime^0'=curtime^post1, __rho_6_^0'=__rho_6_^post1, __rho_2_^0'=__rho_2_^post1, last_copy_time^0'=last_copy_time^post1, a22^0'=a22^post1, (0 == 0 /\ -1+a22^post1 == 0 /\ tt1^post1-__rho_5_^post1 == 0 /\ wakend^0-wakend^post1 == 0 /\ curtime^0-curtime^post1 == 0 /\ -__const_1000^post1+__const_1000^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ got_SIGHUP^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ __rho_1_^0-__rho_1_^post1 == 0 /\ __rho_7_^0-__rho_7_^post1 == 0 /\ -__rho_4_^post1+__rho_4_^0 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ -__rho_6_^post1+__rho_6_^0 == 0), cost: 1 11: l1 -> l9 : __rho_5_^0'=__rho_5_^post11, wakend^0'=wakend^post11, __rho_1_^0'=__rho_1_^post11, got_SIGHUP^0'=got_SIGHUP^post11, __rho_7_^0'=__rho_7_^post11, __rho_4_^0'=__rho_4_^post11, tt1^0'=tt1^post11, __const_1000^0'=__const_1000^post11, curtime^0'=curtime^post11, __rho_6_^0'=__rho_6_^post11, __rho_2_^0'=__rho_2_^post11, last_copy_time^0'=last_copy_time^post11, a22^0'=a22^post11, (-__rho_4_^post11+__rho_4_^0 == 0 /\ wakend^0 <= 0 /\ -a22^post11+a22^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post11 == 0 /\ -__rho_6_^post11+__rho_6_^0 == 0 /\ tt1^0-tt1^post11 == 0 /\ curtime^0-curtime^post11 == 0 /\ __rho_2_^0-__rho_2_^post11 == 0 /\ __const_1000^0-__const_1000^post11 == 0 /\ -last_copy_time^post11+last_copy_time^0 == 0 /\ __rho_1_^0-__rho_1_^post11 == 0 /\ __rho_5_^0-__rho_5_^post11 == 0 /\ __rho_7_^0-__rho_7_^post11 == 0 /\ -wakend^post11+wakend^0 == 0), cost: 1 12: l1 -> l9 : __rho_5_^0'=__rho_5_^post12, wakend^0'=wakend^post12, __rho_1_^0'=__rho_1_^post12, got_SIGHUP^0'=got_SIGHUP^post12, __rho_7_^0'=__rho_7_^post12, __rho_4_^0'=__rho_4_^post12, tt1^0'=tt1^post12, __const_1000^0'=__const_1000^post12, curtime^0'=curtime^post12, __rho_6_^0'=__rho_6_^post12, __rho_2_^0'=__rho_2_^post12, last_copy_time^0'=last_copy_time^post12, a22^0'=a22^post12, (0 == 0 /\ tt1^0-tt1^post12 == 0 /\ __rho_5_^0-__rho_5_^post12 == 0 /\ wakend^post12 == 0 /\ -__rho_7_^post12+__rho_7_^0 == 0 /\ __rho_2_^0-__rho_2_^post12 == 0 /\ __const_1000^0-__const_1000^post12 == 0 /\ -a22^post12+a22^0 == 0 /\ -__rho_4_^post12+__rho_4_^0 == 0 /\ 1-wakend^0 <= 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ last_copy_time^post12-__rho_6_^post12 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ -curtime^post12+curtime^0 == 0), cost: 1 13: l2 -> l1 : __rho_5_^0'=__rho_5_^post13, wakend^0'=wakend^post13, __rho_1_^0'=__rho_1_^post13, got_SIGHUP^0'=got_SIGHUP^post13, __rho_7_^0'=__rho_7_^post13, __rho_4_^0'=__rho_4_^post13, tt1^0'=tt1^post13, __const_1000^0'=__const_1000^post13, curtime^0'=curtime^post13, __rho_6_^0'=__rho_6_^post13, __rho_2_^0'=__rho_2_^post13, last_copy_time^0'=last_copy_time^post13, a22^0'=a22^post13, (__rho_2_^0-__rho_2_^post13 == 0 /\ 1-tt1^0 <= 0 /\ curtime^0-curtime^post13 == 0 /\ -__rho_4_^post13+__rho_4_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post13 == 0 /\ -__rho_6_^post13+__rho_6_^0 == 0 /\ tt1^0-tt1^post13 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ -__const_1000^post13+__const_1000^0 == 0 /\ __rho_5_^0-__rho_5_^post13 == 0 /\ -wakend^post13+wakend^0 == 0 /\ -last_copy_time^post13+last_copy_time^0 == 0 /\ __rho_7_^0-__rho_7_^post13 == 0 /\ -a22^post13+a22^0 == 0), cost: 1 14: l2 -> l5 : __rho_5_^0'=__rho_5_^post14, wakend^0'=wakend^post14, __rho_1_^0'=__rho_1_^post14, got_SIGHUP^0'=got_SIGHUP^post14, __rho_7_^0'=__rho_7_^post14, __rho_4_^0'=__rho_4_^post14, tt1^0'=tt1^post14, __const_1000^0'=__const_1000^post14, curtime^0'=curtime^post14, __rho_6_^0'=__rho_6_^post14, __rho_2_^0'=__rho_2_^post14, last_copy_time^0'=last_copy_time^post14, a22^0'=a22^post14, (tt1^0-tt1^post14 == 0 /\ __rho_5_^0-__rho_5_^post14 == 0 /\ __rho_2_^0-__rho_2_^post14 == 0 /\ -last_copy_time^post14+last_copy_time^0 == 0 /\ -a22^post14+a22^0 == 0 /\ -__rho_7_^post14+__rho_7_^0 == 0 /\ tt1^0 <= 0 /\ -wakend^post14+wakend^0 == 0 /\ __rho_1_^0-__rho_1_^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -__rho_6_^post14+__rho_6_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post14 == 0 /\ __rho_4_^0-__rho_4_^post14 == 0 /\ __const_1000^0-__const_1000^post14 == 0), cost: 1 2: l3 -> l4 : __rho_5_^0'=__rho_5_^post2, wakend^0'=wakend^post2, __rho_1_^0'=__rho_1_^post2, got_SIGHUP^0'=got_SIGHUP^post2, __rho_7_^0'=__rho_7_^post2, __rho_4_^0'=__rho_4_^post2, tt1^0'=tt1^post2, __const_1000^0'=__const_1000^post2, curtime^0'=curtime^post2, __rho_6_^0'=__rho_6_^post2, __rho_2_^0'=__rho_2_^post2, last_copy_time^0'=last_copy_time^post2, a22^0'=a22^post2, (got_SIGHUP^0-got_SIGHUP^post2 == 0 /\ -__rho_7_^post2+__rho_7_^0 == 0 /\ __rho_2_^0-__rho_2_^post2 == 0 /\ tt1^0-tt1^post2 == 0 /\ __rho_5_^0-__rho_5_^post2 == 0 /\ curtime^0-curtime^post2 == 0 /\ -__rho_4_^post2+__rho_4_^0 == 0 /\ -__rho_6_^post2+__rho_6_^0 == 0 /\ -wakend^post2+wakend^0 == 0 /\ -last_copy_time^post2+last_copy_time^0 == 0 /\ -a22^post2+a22^0 == 0 /\ -__const_1000^post2+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post2 == 0), cost: 1 3: l5 -> l6 : __rho_5_^0'=__rho_5_^post3, wakend^0'=wakend^post3, __rho_1_^0'=__rho_1_^post3, got_SIGHUP^0'=got_SIGHUP^post3, __rho_7_^0'=__rho_7_^post3, __rho_4_^0'=__rho_4_^post3, tt1^0'=tt1^post3, __const_1000^0'=__const_1000^post3, curtime^0'=curtime^post3, __rho_6_^0'=__rho_6_^post3, __rho_2_^0'=__rho_2_^post3, last_copy_time^0'=last_copy_time^post3, a22^0'=a22^post3, (-__const_1000^post3+__const_1000^0 == 0 /\ -__rho_6_^post3+__rho_6_^0 == 0 /\ wakend^0-wakend^post3 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post3 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post3 == 0 /\ curtime^0-curtime^post3 == 0 /\ tt1^0-tt1^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -a22^post3+a22^0 == 0 /\ __rho_7_^0-__rho_7_^post3 == 0 /\ -__rho_4_^post3+__rho_4_^0 == 0), cost: 1 9: l6 -> l10 : __rho_5_^0'=__rho_5_^post9, wakend^0'=wakend^post9, __rho_1_^0'=__rho_1_^post9, got_SIGHUP^0'=got_SIGHUP^post9, __rho_7_^0'=__rho_7_^post9, __rho_4_^0'=__rho_4_^post9, tt1^0'=tt1^post9, __const_1000^0'=__const_1000^post9, curtime^0'=curtime^post9, __rho_6_^0'=__rho_6_^post9, __rho_2_^0'=__rho_2_^post9, last_copy_time^0'=last_copy_time^post9, a22^0'=a22^post9, (got_SIGHUP^0-got_SIGHUP^post9 == 0 /\ -__rho_7_^post9+__rho_7_^0 == 0 /\ curtime^0-curtime^post9 == 0 /\ tt1^0-tt1^post9 == 0 /\ wakend^0-wakend^post9 == 0 /\ -__rho_4_^post9+__rho_4_^0 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ -__rho_6_^post9+__rho_6_^0 == 0 /\ __const_1000^0-__const_1000^post9 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0 /\ -a22^post9+a22^0 == 0 /\ -last_copy_time^post9+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post9 == 0), cost: 1 4: l7 -> l5 : __rho_5_^0'=__rho_5_^post4, wakend^0'=wakend^post4, __rho_1_^0'=__rho_1_^post4, got_SIGHUP^0'=got_SIGHUP^post4, __rho_7_^0'=__rho_7_^post4, __rho_4_^0'=__rho_4_^post4, tt1^0'=tt1^post4, __const_1000^0'=__const_1000^post4, curtime^0'=curtime^post4, __rho_6_^0'=__rho_6_^post4, __rho_2_^0'=__rho_2_^post4, last_copy_time^0'=last_copy_time^post4, a22^0'=a22^post4, (0 == 0 /\ curtime^0-curtime^post4 == 0 /\ -__rho_7_^post4+__rho_7_^0 == 0 /\ -a22^post4+a22^0 == 0 /\ tt1^0-tt1^post4 == 0 /\ got_SIGHUP^0-got_SIGHUP^post4 == 0 /\ __rho_2_^0-__rho_2_^post4 == 0 /\ __rho_1_^0-__rho_1_^post4 == 0 /\ __const_1000^0-__const_1000^post4 == 0 /\ -__rho_6_^post4+__rho_6_^0 == 0 /\ -last_copy_time^post4+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post4 == 0 /\ -wakend^post4+wakend^0 == 0), cost: 1 5: l8 -> l7 : __rho_5_^0'=__rho_5_^post5, wakend^0'=wakend^post5, __rho_1_^0'=__rho_1_^post5, got_SIGHUP^0'=got_SIGHUP^post5, __rho_7_^0'=__rho_7_^post5, __rho_4_^0'=__rho_4_^post5, tt1^0'=tt1^post5, __const_1000^0'=__const_1000^post5, curtime^0'=curtime^post5, __rho_6_^0'=__rho_6_^post5, __rho_2_^0'=__rho_2_^post5, last_copy_time^0'=last_copy_time^post5, a22^0'=a22^post5, (__rho_5_^0-__rho_5_^post5 == 0 /\ tt1^0-tt1^post5 == 0 /\ -__rho_7_^post5+__rho_7_^0 == 0 /\ -__const_1000^post5+__const_1000^0 == 0 /\ -__rho_4_^post5+__rho_4_^0 == 0 /\ -last_copy_time^post5+last_copy_time^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ -a22^post5+a22^0 == 0 /\ wakend^0-wakend^post5 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ -__rho_6_^post5+__rho_6_^0 == 0 /\ __rho_1_^0-__rho_1_^post5 == 0 /\ got_SIGHUP^0-got_SIGHUP^post5 == 0 /\ 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0), cost: 1 6: l8 -> l7 : __rho_5_^0'=__rho_5_^post6, wakend^0'=wakend^post6, __rho_1_^0'=__rho_1_^post6, got_SIGHUP^0'=got_SIGHUP^post6, __rho_7_^0'=__rho_7_^post6, __rho_4_^0'=__rho_4_^post6, tt1^0'=tt1^post6, __const_1000^0'=__const_1000^post6, curtime^0'=curtime^post6, __rho_6_^0'=__rho_6_^post6, __rho_2_^0'=__rho_2_^post6, last_copy_time^0'=last_copy_time^post6, a22^0'=a22^post6, (__rho_2_^0-__rho_2_^post6 == 0 /\ -1+wakend^post6 == 0 /\ -__const_1000^post6+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ curtime^0-curtime^post6 == 0 /\ got_SIGHUP^0-got_SIGHUP^post6 == 0 /\ tt1^0-tt1^post6 == 0 /\ __rho_5_^0-__rho_5_^post6 == 0 /\ __const_1000^0-curtime^0+last_copy_time^0 <= 0 /\ __rho_7_^0-__rho_7_^post6 == 0 /\ -__rho_4_^post6+__rho_4_^0 == 0 /\ -__rho_6_^post6+__rho_6_^0 == 0 /\ -a22^post6+a22^0 == 0 /\ -last_copy_time^post6+last_copy_time^0 == 0), cost: 1 7: l9 -> l7 : __rho_5_^0'=__rho_5_^post7, wakend^0'=wakend^post7, __rho_1_^0'=__rho_1_^post7, got_SIGHUP^0'=got_SIGHUP^post7, __rho_7_^0'=__rho_7_^post7, __rho_4_^0'=__rho_4_^post7, tt1^0'=tt1^post7, __const_1000^0'=__const_1000^post7, curtime^0'=curtime^post7, __rho_6_^0'=__rho_6_^post7, __rho_2_^0'=__rho_2_^post7, last_copy_time^0'=last_copy_time^post7, a22^0'=a22^post7, (__rho_2_^0-__rho_2_^post7 == 0 /\ __rho_5_^0-__rho_5_^post7 == 0 /\ curtime^0-curtime^post7 == 0 /\ got_SIGHUP^0-got_SIGHUP^post7 == 0 /\ -__rho_4_^post7+__rho_4_^0 == 0 /\ tt1^0-tt1^post7 == 0 /\ -__rho_6_^post7+__rho_6_^0 == 0 /\ __rho_1_^0-__rho_1_^post7 == 0 /\ 1-wakend^0 <= 0 /\ -wakend^post7+wakend^0 == 0 /\ -a22^post7+a22^0 == 0 /\ -last_copy_time^post7+last_copy_time^0 == 0 /\ -__const_1000^post7+__const_1000^0 == 0 /\ __rho_7_^0-__rho_7_^post7 == 0), cost: 1 8: l9 -> l8 : __rho_5_^0'=__rho_5_^post8, wakend^0'=wakend^post8, __rho_1_^0'=__rho_1_^post8, got_SIGHUP^0'=got_SIGHUP^post8, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post8, tt1^0'=tt1^post8, __const_1000^0'=__const_1000^post8, curtime^0'=curtime^post8, __rho_6_^0'=__rho_6_^post8, __rho_2_^0'=__rho_2_^post8, last_copy_time^0'=last_copy_time^post8, a22^0'=a22^post8, (0 == 0 /\ curtime^post8-__rho_7_^post8 == 0 /\ -__rho_6_^post8+__rho_6_^0 == 0 /\ wakend^0 <= 0 /\ -__const_1000^post8+__const_1000^0 == 0 /\ wakend^0-wakend^post8 == 0 /\ got_SIGHUP^0-got_SIGHUP^post8 == 0 /\ -a22^post8+a22^0 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ tt1^0-tt1^post8 == 0 /\ -__rho_2_^post8+__rho_2_^0 == 0 /\ __rho_1_^0-__rho_1_^post8 == 0 /\ -__rho_4_^post8+__rho_4_^0 == 0 /\ __rho_5_^0-__rho_5_^post8 == 0), cost: 1 10: l10 -> l6 : __rho_5_^0'=__rho_5_^post10, wakend^0'=wakend^post10, __rho_1_^0'=__rho_1_^post10, got_SIGHUP^0'=got_SIGHUP^post10, __rho_7_^0'=__rho_7_^post10, __rho_4_^0'=__rho_4_^post10, tt1^0'=tt1^post10, __const_1000^0'=__const_1000^post10, curtime^0'=curtime^post10, __rho_6_^0'=__rho_6_^post10, __rho_2_^0'=__rho_2_^post10, last_copy_time^0'=last_copy_time^post10, a22^0'=a22^post10, (got_SIGHUP^0-got_SIGHUP^post10 == 0 /\ -last_copy_time^post10+last_copy_time^0 == 0 /\ -__rho_7_^post10+__rho_7_^0 == 0 /\ -__rho_6_^post10+__rho_6_^0 == 0 /\ -__const_1000^post10+__const_1000^0 == 0 /\ __rho_5_^0-__rho_5_^post10 == 0 /\ curtime^0-curtime^post10 == 0 /\ tt1^0-tt1^post10 == 0 /\ -__rho_2_^post10+__rho_2_^0 == 0 /\ -__rho_4_^post10+__rho_4_^0 == 0 /\ -a22^post10+a22^0 == 0 /\ wakend^0-wakend^post10 == 0 /\ __rho_1_^0-__rho_1_^post10 == 0), cost: 1 15: l11 -> l0 : __rho_5_^0'=__rho_5_^post15, wakend^0'=wakend^post15, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=got_SIGHUP^post15, __rho_7_^0'=__rho_7_^post15, __rho_4_^0'=__rho_4_^post15, tt1^0'=tt1^post15, __const_1000^0'=__const_1000^post15, curtime^0'=curtime^post15, __rho_6_^0'=__rho_6_^post15, __rho_2_^0'=__rho_2_^post15, last_copy_time^0'=last_copy_time^post15, a22^0'=a22^post15, (0 == 0 /\ -__rho_4_^post15+__rho_4_^0 == 0 /\ -a22^post15+a22^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ -__rho_2_^post15+__rho_2_^0 == 0 /\ -tt1^post15+tt1^0 == 0 /\ -1+wakend^post15 == 0 /\ __rho_7_^0-__rho_7_^post15 == 0 /\ -1+wakend^10 == 0 /\ curtime^0-curtime^post15 == 0 /\ __rho_5_^0-__rho_5_^post15 == 0 /\ got_SIGHUP^post15-__rho_2_^0 == 0 /\ __rho_6_^0-__rho_6_^post15 == 0 /\ -__const_1000^post15+__const_1000^0 == 0), cost: 1 16: l12 -> l11 : __rho_5_^0'=__rho_5_^post16, wakend^0'=wakend^post16, __rho_1_^0'=__rho_1_^post16, got_SIGHUP^0'=got_SIGHUP^post16, __rho_7_^0'=__rho_7_^post16, __rho_4_^0'=__rho_4_^post16, tt1^0'=tt1^post16, __const_1000^0'=__const_1000^post16, curtime^0'=curtime^post16, __rho_6_^0'=__rho_6_^post16, __rho_2_^0'=__rho_2_^post16, last_copy_time^0'=last_copy_time^post16, a22^0'=a22^post16, (__rho_5_^0-__rho_5_^post16 == 0 /\ -__rho_6_^post16+__rho_6_^0 == 0 /\ -last_copy_time^post16+last_copy_time^0 == 0 /\ -__rho_7_^post16+__rho_7_^0 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ -curtime^post16+curtime^0 == 0 /\ wakend^0-wakend^post16 == 0 /\ -a22^post16+a22^0 == 0 /\ __const_1000^0-__const_1000^post16 == 0 /\ __rho_1_^0-__rho_1_^post16 == 0 /\ __rho_4_^0-__rho_4_^post16 == 0 /\ got_SIGHUP^0-got_SIGHUP^post16 == 0 /\ tt1^0-tt1^post16 == 0), cost: 1 Removed unreachable rules and leafs Start location: l12 0: l0 -> l1 : __rho_5_^0'=__rho_5_^post0, wakend^0'=wakend^post0, __rho_1_^0'=__rho_1_^post0, got_SIGHUP^0'=got_SIGHUP^post0, __rho_7_^0'=__rho_7_^post0, __rho_4_^0'=__rho_4_^post0, tt1^0'=tt1^post0, __const_1000^0'=__const_1000^post0, curtime^0'=curtime^post0, __rho_6_^0'=__rho_6_^post0, __rho_2_^0'=__rho_2_^post0, last_copy_time^0'=last_copy_time^post0, a22^0'=a22^post0, (-__rho_4_^post0+__rho_4_^0 == 0 /\ got_SIGHUP^0 <= 0 /\ curtime^0-curtime^post0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post0 == 0 /\ tt1^0-tt1^post0 == 0 /\ -a22^post0+a22^0 == 0 /\ -last_copy_time^post0+last_copy_time^0 == 0 /\ -__const_1000^post0+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ -__rho_2_^post0+__rho_2_^0 == 0 /\ -wakend^post0+wakend^0 == 0 /\ __rho_5_^0-__rho_5_^post0 == 0 /\ -__rho_6_^post0+__rho_6_^0 == 0 /\ __rho_7_^0-__rho_7_^post0 == 0), cost: 1 1: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=wakend^post1, __rho_1_^0'=__rho_1_^post1, got_SIGHUP^0'=got_SIGHUP^post1, __rho_7_^0'=__rho_7_^post1, __rho_4_^0'=__rho_4_^post1, tt1^0'=tt1^post1, __const_1000^0'=__const_1000^post1, curtime^0'=curtime^post1, __rho_6_^0'=__rho_6_^post1, __rho_2_^0'=__rho_2_^post1, last_copy_time^0'=last_copy_time^post1, a22^0'=a22^post1, (0 == 0 /\ -1+a22^post1 == 0 /\ tt1^post1-__rho_5_^post1 == 0 /\ wakend^0-wakend^post1 == 0 /\ curtime^0-curtime^post1 == 0 /\ -__const_1000^post1+__const_1000^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ got_SIGHUP^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ __rho_1_^0-__rho_1_^post1 == 0 /\ __rho_7_^0-__rho_7_^post1 == 0 /\ -__rho_4_^post1+__rho_4_^0 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ -__rho_6_^post1+__rho_6_^0 == 0), cost: 1 11: l1 -> l9 : __rho_5_^0'=__rho_5_^post11, wakend^0'=wakend^post11, __rho_1_^0'=__rho_1_^post11, got_SIGHUP^0'=got_SIGHUP^post11, __rho_7_^0'=__rho_7_^post11, __rho_4_^0'=__rho_4_^post11, tt1^0'=tt1^post11, __const_1000^0'=__const_1000^post11, curtime^0'=curtime^post11, __rho_6_^0'=__rho_6_^post11, __rho_2_^0'=__rho_2_^post11, last_copy_time^0'=last_copy_time^post11, a22^0'=a22^post11, (-__rho_4_^post11+__rho_4_^0 == 0 /\ wakend^0 <= 0 /\ -a22^post11+a22^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post11 == 0 /\ -__rho_6_^post11+__rho_6_^0 == 0 /\ tt1^0-tt1^post11 == 0 /\ curtime^0-curtime^post11 == 0 /\ __rho_2_^0-__rho_2_^post11 == 0 /\ __const_1000^0-__const_1000^post11 == 0 /\ -last_copy_time^post11+last_copy_time^0 == 0 /\ __rho_1_^0-__rho_1_^post11 == 0 /\ __rho_5_^0-__rho_5_^post11 == 0 /\ __rho_7_^0-__rho_7_^post11 == 0 /\ -wakend^post11+wakend^0 == 0), cost: 1 12: l1 -> l9 : __rho_5_^0'=__rho_5_^post12, wakend^0'=wakend^post12, __rho_1_^0'=__rho_1_^post12, got_SIGHUP^0'=got_SIGHUP^post12, __rho_7_^0'=__rho_7_^post12, __rho_4_^0'=__rho_4_^post12, tt1^0'=tt1^post12, __const_1000^0'=__const_1000^post12, curtime^0'=curtime^post12, __rho_6_^0'=__rho_6_^post12, __rho_2_^0'=__rho_2_^post12, last_copy_time^0'=last_copy_time^post12, a22^0'=a22^post12, (0 == 0 /\ tt1^0-tt1^post12 == 0 /\ __rho_5_^0-__rho_5_^post12 == 0 /\ wakend^post12 == 0 /\ -__rho_7_^post12+__rho_7_^0 == 0 /\ __rho_2_^0-__rho_2_^post12 == 0 /\ __const_1000^0-__const_1000^post12 == 0 /\ -a22^post12+a22^0 == 0 /\ -__rho_4_^post12+__rho_4_^0 == 0 /\ 1-wakend^0 <= 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ last_copy_time^post12-__rho_6_^post12 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ -curtime^post12+curtime^0 == 0), cost: 1 13: l2 -> l1 : __rho_5_^0'=__rho_5_^post13, wakend^0'=wakend^post13, __rho_1_^0'=__rho_1_^post13, got_SIGHUP^0'=got_SIGHUP^post13, __rho_7_^0'=__rho_7_^post13, __rho_4_^0'=__rho_4_^post13, tt1^0'=tt1^post13, __const_1000^0'=__const_1000^post13, curtime^0'=curtime^post13, __rho_6_^0'=__rho_6_^post13, __rho_2_^0'=__rho_2_^post13, last_copy_time^0'=last_copy_time^post13, a22^0'=a22^post13, (__rho_2_^0-__rho_2_^post13 == 0 /\ 1-tt1^0 <= 0 /\ curtime^0-curtime^post13 == 0 /\ -__rho_4_^post13+__rho_4_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post13 == 0 /\ -__rho_6_^post13+__rho_6_^0 == 0 /\ tt1^0-tt1^post13 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ -__const_1000^post13+__const_1000^0 == 0 /\ __rho_5_^0-__rho_5_^post13 == 0 /\ -wakend^post13+wakend^0 == 0 /\ -last_copy_time^post13+last_copy_time^0 == 0 /\ __rho_7_^0-__rho_7_^post13 == 0 /\ -a22^post13+a22^0 == 0), cost: 1 14: l2 -> l5 : __rho_5_^0'=__rho_5_^post14, wakend^0'=wakend^post14, __rho_1_^0'=__rho_1_^post14, got_SIGHUP^0'=got_SIGHUP^post14, __rho_7_^0'=__rho_7_^post14, __rho_4_^0'=__rho_4_^post14, tt1^0'=tt1^post14, __const_1000^0'=__const_1000^post14, curtime^0'=curtime^post14, __rho_6_^0'=__rho_6_^post14, __rho_2_^0'=__rho_2_^post14, last_copy_time^0'=last_copy_time^post14, a22^0'=a22^post14, (tt1^0-tt1^post14 == 0 /\ __rho_5_^0-__rho_5_^post14 == 0 /\ __rho_2_^0-__rho_2_^post14 == 0 /\ -last_copy_time^post14+last_copy_time^0 == 0 /\ -a22^post14+a22^0 == 0 /\ -__rho_7_^post14+__rho_7_^0 == 0 /\ tt1^0 <= 0 /\ -wakend^post14+wakend^0 == 0 /\ __rho_1_^0-__rho_1_^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -__rho_6_^post14+__rho_6_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post14 == 0 /\ __rho_4_^0-__rho_4_^post14 == 0 /\ __const_1000^0-__const_1000^post14 == 0), cost: 1 3: l5 -> l6 : __rho_5_^0'=__rho_5_^post3, wakend^0'=wakend^post3, __rho_1_^0'=__rho_1_^post3, got_SIGHUP^0'=got_SIGHUP^post3, __rho_7_^0'=__rho_7_^post3, __rho_4_^0'=__rho_4_^post3, tt1^0'=tt1^post3, __const_1000^0'=__const_1000^post3, curtime^0'=curtime^post3, __rho_6_^0'=__rho_6_^post3, __rho_2_^0'=__rho_2_^post3, last_copy_time^0'=last_copy_time^post3, a22^0'=a22^post3, (-__const_1000^post3+__const_1000^0 == 0 /\ -__rho_6_^post3+__rho_6_^0 == 0 /\ wakend^0-wakend^post3 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post3 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post3 == 0 /\ curtime^0-curtime^post3 == 0 /\ tt1^0-tt1^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -a22^post3+a22^0 == 0 /\ __rho_7_^0-__rho_7_^post3 == 0 /\ -__rho_4_^post3+__rho_4_^0 == 0), cost: 1 9: l6 -> l10 : __rho_5_^0'=__rho_5_^post9, wakend^0'=wakend^post9, __rho_1_^0'=__rho_1_^post9, got_SIGHUP^0'=got_SIGHUP^post9, __rho_7_^0'=__rho_7_^post9, __rho_4_^0'=__rho_4_^post9, tt1^0'=tt1^post9, __const_1000^0'=__const_1000^post9, curtime^0'=curtime^post9, __rho_6_^0'=__rho_6_^post9, __rho_2_^0'=__rho_2_^post9, last_copy_time^0'=last_copy_time^post9, a22^0'=a22^post9, (got_SIGHUP^0-got_SIGHUP^post9 == 0 /\ -__rho_7_^post9+__rho_7_^0 == 0 /\ curtime^0-curtime^post9 == 0 /\ tt1^0-tt1^post9 == 0 /\ wakend^0-wakend^post9 == 0 /\ -__rho_4_^post9+__rho_4_^0 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ -__rho_6_^post9+__rho_6_^0 == 0 /\ __const_1000^0-__const_1000^post9 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0 /\ -a22^post9+a22^0 == 0 /\ -last_copy_time^post9+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post9 == 0), cost: 1 4: l7 -> l5 : __rho_5_^0'=__rho_5_^post4, wakend^0'=wakend^post4, __rho_1_^0'=__rho_1_^post4, got_SIGHUP^0'=got_SIGHUP^post4, __rho_7_^0'=__rho_7_^post4, __rho_4_^0'=__rho_4_^post4, tt1^0'=tt1^post4, __const_1000^0'=__const_1000^post4, curtime^0'=curtime^post4, __rho_6_^0'=__rho_6_^post4, __rho_2_^0'=__rho_2_^post4, last_copy_time^0'=last_copy_time^post4, a22^0'=a22^post4, (0 == 0 /\ curtime^0-curtime^post4 == 0 /\ -__rho_7_^post4+__rho_7_^0 == 0 /\ -a22^post4+a22^0 == 0 /\ tt1^0-tt1^post4 == 0 /\ got_SIGHUP^0-got_SIGHUP^post4 == 0 /\ __rho_2_^0-__rho_2_^post4 == 0 /\ __rho_1_^0-__rho_1_^post4 == 0 /\ __const_1000^0-__const_1000^post4 == 0 /\ -__rho_6_^post4+__rho_6_^0 == 0 /\ -last_copy_time^post4+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post4 == 0 /\ -wakend^post4+wakend^0 == 0), cost: 1 5: l8 -> l7 : __rho_5_^0'=__rho_5_^post5, wakend^0'=wakend^post5, __rho_1_^0'=__rho_1_^post5, got_SIGHUP^0'=got_SIGHUP^post5, __rho_7_^0'=__rho_7_^post5, __rho_4_^0'=__rho_4_^post5, tt1^0'=tt1^post5, __const_1000^0'=__const_1000^post5, curtime^0'=curtime^post5, __rho_6_^0'=__rho_6_^post5, __rho_2_^0'=__rho_2_^post5, last_copy_time^0'=last_copy_time^post5, a22^0'=a22^post5, (__rho_5_^0-__rho_5_^post5 == 0 /\ tt1^0-tt1^post5 == 0 /\ -__rho_7_^post5+__rho_7_^0 == 0 /\ -__const_1000^post5+__const_1000^0 == 0 /\ -__rho_4_^post5+__rho_4_^0 == 0 /\ -last_copy_time^post5+last_copy_time^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ -a22^post5+a22^0 == 0 /\ wakend^0-wakend^post5 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ -__rho_6_^post5+__rho_6_^0 == 0 /\ __rho_1_^0-__rho_1_^post5 == 0 /\ got_SIGHUP^0-got_SIGHUP^post5 == 0 /\ 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0), cost: 1 6: l8 -> l7 : __rho_5_^0'=__rho_5_^post6, wakend^0'=wakend^post6, __rho_1_^0'=__rho_1_^post6, got_SIGHUP^0'=got_SIGHUP^post6, __rho_7_^0'=__rho_7_^post6, __rho_4_^0'=__rho_4_^post6, tt1^0'=tt1^post6, __const_1000^0'=__const_1000^post6, curtime^0'=curtime^post6, __rho_6_^0'=__rho_6_^post6, __rho_2_^0'=__rho_2_^post6, last_copy_time^0'=last_copy_time^post6, a22^0'=a22^post6, (__rho_2_^0-__rho_2_^post6 == 0 /\ -1+wakend^post6 == 0 /\ -__const_1000^post6+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ curtime^0-curtime^post6 == 0 /\ got_SIGHUP^0-got_SIGHUP^post6 == 0 /\ tt1^0-tt1^post6 == 0 /\ __rho_5_^0-__rho_5_^post6 == 0 /\ __const_1000^0-curtime^0+last_copy_time^0 <= 0 /\ __rho_7_^0-__rho_7_^post6 == 0 /\ -__rho_4_^post6+__rho_4_^0 == 0 /\ -__rho_6_^post6+__rho_6_^0 == 0 /\ -a22^post6+a22^0 == 0 /\ -last_copy_time^post6+last_copy_time^0 == 0), cost: 1 7: l9 -> l7 : __rho_5_^0'=__rho_5_^post7, wakend^0'=wakend^post7, __rho_1_^0'=__rho_1_^post7, got_SIGHUP^0'=got_SIGHUP^post7, __rho_7_^0'=__rho_7_^post7, __rho_4_^0'=__rho_4_^post7, tt1^0'=tt1^post7, __const_1000^0'=__const_1000^post7, curtime^0'=curtime^post7, __rho_6_^0'=__rho_6_^post7, __rho_2_^0'=__rho_2_^post7, last_copy_time^0'=last_copy_time^post7, a22^0'=a22^post7, (__rho_2_^0-__rho_2_^post7 == 0 /\ __rho_5_^0-__rho_5_^post7 == 0 /\ curtime^0-curtime^post7 == 0 /\ got_SIGHUP^0-got_SIGHUP^post7 == 0 /\ -__rho_4_^post7+__rho_4_^0 == 0 /\ tt1^0-tt1^post7 == 0 /\ -__rho_6_^post7+__rho_6_^0 == 0 /\ __rho_1_^0-__rho_1_^post7 == 0 /\ 1-wakend^0 <= 0 /\ -wakend^post7+wakend^0 == 0 /\ -a22^post7+a22^0 == 0 /\ -last_copy_time^post7+last_copy_time^0 == 0 /\ -__const_1000^post7+__const_1000^0 == 0 /\ __rho_7_^0-__rho_7_^post7 == 0), cost: 1 8: l9 -> l8 : __rho_5_^0'=__rho_5_^post8, wakend^0'=wakend^post8, __rho_1_^0'=__rho_1_^post8, got_SIGHUP^0'=got_SIGHUP^post8, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post8, tt1^0'=tt1^post8, __const_1000^0'=__const_1000^post8, curtime^0'=curtime^post8, __rho_6_^0'=__rho_6_^post8, __rho_2_^0'=__rho_2_^post8, last_copy_time^0'=last_copy_time^post8, a22^0'=a22^post8, (0 == 0 /\ curtime^post8-__rho_7_^post8 == 0 /\ -__rho_6_^post8+__rho_6_^0 == 0 /\ wakend^0 <= 0 /\ -__const_1000^post8+__const_1000^0 == 0 /\ wakend^0-wakend^post8 == 0 /\ got_SIGHUP^0-got_SIGHUP^post8 == 0 /\ -a22^post8+a22^0 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ tt1^0-tt1^post8 == 0 /\ -__rho_2_^post8+__rho_2_^0 == 0 /\ __rho_1_^0-__rho_1_^post8 == 0 /\ -__rho_4_^post8+__rho_4_^0 == 0 /\ __rho_5_^0-__rho_5_^post8 == 0), cost: 1 10: l10 -> l6 : __rho_5_^0'=__rho_5_^post10, wakend^0'=wakend^post10, __rho_1_^0'=__rho_1_^post10, got_SIGHUP^0'=got_SIGHUP^post10, __rho_7_^0'=__rho_7_^post10, __rho_4_^0'=__rho_4_^post10, tt1^0'=tt1^post10, __const_1000^0'=__const_1000^post10, curtime^0'=curtime^post10, __rho_6_^0'=__rho_6_^post10, __rho_2_^0'=__rho_2_^post10, last_copy_time^0'=last_copy_time^post10, a22^0'=a22^post10, (got_SIGHUP^0-got_SIGHUP^post10 == 0 /\ -last_copy_time^post10+last_copy_time^0 == 0 /\ -__rho_7_^post10+__rho_7_^0 == 0 /\ -__rho_6_^post10+__rho_6_^0 == 0 /\ -__const_1000^post10+__const_1000^0 == 0 /\ __rho_5_^0-__rho_5_^post10 == 0 /\ curtime^0-curtime^post10 == 0 /\ tt1^0-tt1^post10 == 0 /\ -__rho_2_^post10+__rho_2_^0 == 0 /\ -__rho_4_^post10+__rho_4_^0 == 0 /\ -a22^post10+a22^0 == 0 /\ wakend^0-wakend^post10 == 0 /\ __rho_1_^0-__rho_1_^post10 == 0), cost: 1 15: l11 -> l0 : __rho_5_^0'=__rho_5_^post15, wakend^0'=wakend^post15, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=got_SIGHUP^post15, __rho_7_^0'=__rho_7_^post15, __rho_4_^0'=__rho_4_^post15, tt1^0'=tt1^post15, __const_1000^0'=__const_1000^post15, curtime^0'=curtime^post15, __rho_6_^0'=__rho_6_^post15, __rho_2_^0'=__rho_2_^post15, last_copy_time^0'=last_copy_time^post15, a22^0'=a22^post15, (0 == 0 /\ -__rho_4_^post15+__rho_4_^0 == 0 /\ -a22^post15+a22^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ -__rho_2_^post15+__rho_2_^0 == 0 /\ -tt1^post15+tt1^0 == 0 /\ -1+wakend^post15 == 0 /\ __rho_7_^0-__rho_7_^post15 == 0 /\ -1+wakend^10 == 0 /\ curtime^0-curtime^post15 == 0 /\ __rho_5_^0-__rho_5_^post15 == 0 /\ got_SIGHUP^post15-__rho_2_^0 == 0 /\ __rho_6_^0-__rho_6_^post15 == 0 /\ -__const_1000^post15+__const_1000^0 == 0), cost: 1 16: l12 -> l11 : __rho_5_^0'=__rho_5_^post16, wakend^0'=wakend^post16, __rho_1_^0'=__rho_1_^post16, got_SIGHUP^0'=got_SIGHUP^post16, __rho_7_^0'=__rho_7_^post16, __rho_4_^0'=__rho_4_^post16, tt1^0'=tt1^post16, __const_1000^0'=__const_1000^post16, curtime^0'=curtime^post16, __rho_6_^0'=__rho_6_^post16, __rho_2_^0'=__rho_2_^post16, last_copy_time^0'=last_copy_time^post16, a22^0'=a22^post16, (__rho_5_^0-__rho_5_^post16 == 0 /\ -__rho_6_^post16+__rho_6_^0 == 0 /\ -last_copy_time^post16+last_copy_time^0 == 0 /\ -__rho_7_^post16+__rho_7_^0 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ -curtime^post16+curtime^0 == 0 /\ wakend^0-wakend^post16 == 0 /\ -a22^post16+a22^0 == 0 /\ __const_1000^0-__const_1000^post16 == 0 /\ __rho_1_^0-__rho_1_^post16 == 0 /\ __rho_4_^0-__rho_4_^post16 == 0 /\ got_SIGHUP^0-got_SIGHUP^post16 == 0 /\ tt1^0-tt1^post16 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : __rho_5_^0'=__rho_5_^post0, wakend^0'=wakend^post0, __rho_1_^0'=__rho_1_^post0, got_SIGHUP^0'=got_SIGHUP^post0, __rho_7_^0'=__rho_7_^post0, __rho_4_^0'=__rho_4_^post0, tt1^0'=tt1^post0, __const_1000^0'=__const_1000^post0, curtime^0'=curtime^post0, __rho_6_^0'=__rho_6_^post0, __rho_2_^0'=__rho_2_^post0, last_copy_time^0'=last_copy_time^post0, a22^0'=a22^post0, (-__rho_4_^post0+__rho_4_^0 == 0 /\ got_SIGHUP^0 <= 0 /\ curtime^0-curtime^post0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post0 == 0 /\ tt1^0-tt1^post0 == 0 /\ -a22^post0+a22^0 == 0 /\ -last_copy_time^post0+last_copy_time^0 == 0 /\ -__const_1000^post0+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ -__rho_2_^post0+__rho_2_^0 == 0 /\ -wakend^post0+wakend^0 == 0 /\ __rho_5_^0-__rho_5_^post0 == 0 /\ -__rho_6_^post0+__rho_6_^0 == 0 /\ __rho_7_^0-__rho_7_^post0 == 0), cost: 1 New rule: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 Applied preprocessing Original rule: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=wakend^post1, __rho_1_^0'=__rho_1_^post1, got_SIGHUP^0'=got_SIGHUP^post1, __rho_7_^0'=__rho_7_^post1, __rho_4_^0'=__rho_4_^post1, tt1^0'=tt1^post1, __const_1000^0'=__const_1000^post1, curtime^0'=curtime^post1, __rho_6_^0'=__rho_6_^post1, __rho_2_^0'=__rho_2_^post1, last_copy_time^0'=last_copy_time^post1, a22^0'=a22^post1, (0 == 0 /\ -1+a22^post1 == 0 /\ tt1^post1-__rho_5_^post1 == 0 /\ wakend^0-wakend^post1 == 0 /\ curtime^0-curtime^post1 == 0 /\ -__const_1000^post1+__const_1000^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ got_SIGHUP^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ __rho_1_^0-__rho_1_^post1 == 0 /\ __rho_7_^0-__rho_7_^post1 == 0 /\ -__rho_4_^post1+__rho_4_^0 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ -__rho_6_^post1+__rho_6_^0 == 0), cost: 1 New rule: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+got_SIGHUP^0 >= 0, cost: 1 Applied preprocessing Original rule: l5 -> l6 : __rho_5_^0'=__rho_5_^post3, wakend^0'=wakend^post3, __rho_1_^0'=__rho_1_^post3, got_SIGHUP^0'=got_SIGHUP^post3, __rho_7_^0'=__rho_7_^post3, __rho_4_^0'=__rho_4_^post3, tt1^0'=tt1^post3, __const_1000^0'=__const_1000^post3, curtime^0'=curtime^post3, __rho_6_^0'=__rho_6_^post3, __rho_2_^0'=__rho_2_^post3, last_copy_time^0'=last_copy_time^post3, a22^0'=a22^post3, (-__const_1000^post3+__const_1000^0 == 0 /\ -__rho_6_^post3+__rho_6_^0 == 0 /\ wakend^0-wakend^post3 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post3 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post3 == 0 /\ curtime^0-curtime^post3 == 0 /\ tt1^0-tt1^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ -a22^post3+a22^0 == 0 /\ __rho_7_^0-__rho_7_^post3 == 0 /\ -__rho_4_^post3+__rho_4_^0 == 0), cost: 1 New rule: l5 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l7 -> l5 : __rho_5_^0'=__rho_5_^post4, wakend^0'=wakend^post4, __rho_1_^0'=__rho_1_^post4, got_SIGHUP^0'=got_SIGHUP^post4, __rho_7_^0'=__rho_7_^post4, __rho_4_^0'=__rho_4_^post4, tt1^0'=tt1^post4, __const_1000^0'=__const_1000^post4, curtime^0'=curtime^post4, __rho_6_^0'=__rho_6_^post4, __rho_2_^0'=__rho_2_^post4, last_copy_time^0'=last_copy_time^post4, a22^0'=a22^post4, (0 == 0 /\ curtime^0-curtime^post4 == 0 /\ -__rho_7_^post4+__rho_7_^0 == 0 /\ -a22^post4+a22^0 == 0 /\ tt1^0-tt1^post4 == 0 /\ got_SIGHUP^0-got_SIGHUP^post4 == 0 /\ __rho_2_^0-__rho_2_^post4 == 0 /\ __rho_1_^0-__rho_1_^post4 == 0 /\ __const_1000^0-__const_1000^post4 == 0 /\ -__rho_6_^post4+__rho_6_^0 == 0 /\ -last_copy_time^post4+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post4 == 0 /\ -wakend^post4+wakend^0 == 0), cost: 1 New rule: l7 -> l5 : __rho_4_^0'=__rho_4_^post4, 0 == 0, cost: 1 Applied preprocessing Original rule: l8 -> l7 : __rho_5_^0'=__rho_5_^post5, wakend^0'=wakend^post5, __rho_1_^0'=__rho_1_^post5, got_SIGHUP^0'=got_SIGHUP^post5, __rho_7_^0'=__rho_7_^post5, __rho_4_^0'=__rho_4_^post5, tt1^0'=tt1^post5, __const_1000^0'=__const_1000^post5, curtime^0'=curtime^post5, __rho_6_^0'=__rho_6_^post5, __rho_2_^0'=__rho_2_^post5, last_copy_time^0'=last_copy_time^post5, a22^0'=a22^post5, (__rho_5_^0-__rho_5_^post5 == 0 /\ tt1^0-tt1^post5 == 0 /\ -__rho_7_^post5+__rho_7_^0 == 0 /\ -__const_1000^post5+__const_1000^0 == 0 /\ -__rho_4_^post5+__rho_4_^0 == 0 /\ -last_copy_time^post5+last_copy_time^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ -a22^post5+a22^0 == 0 /\ wakend^0-wakend^post5 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ -__rho_6_^post5+__rho_6_^0 == 0 /\ __rho_1_^0-__rho_1_^post5 == 0 /\ got_SIGHUP^0-got_SIGHUP^post5 == 0 /\ 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0), cost: 1 New rule: l8 -> l7 : 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 1 Applied preprocessing Original rule: l8 -> l7 : __rho_5_^0'=__rho_5_^post6, wakend^0'=wakend^post6, __rho_1_^0'=__rho_1_^post6, got_SIGHUP^0'=got_SIGHUP^post6, __rho_7_^0'=__rho_7_^post6, __rho_4_^0'=__rho_4_^post6, tt1^0'=tt1^post6, __const_1000^0'=__const_1000^post6, curtime^0'=curtime^post6, __rho_6_^0'=__rho_6_^post6, __rho_2_^0'=__rho_2_^post6, last_copy_time^0'=last_copy_time^post6, a22^0'=a22^post6, (__rho_2_^0-__rho_2_^post6 == 0 /\ -1+wakend^post6 == 0 /\ -__const_1000^post6+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ curtime^0-curtime^post6 == 0 /\ got_SIGHUP^0-got_SIGHUP^post6 == 0 /\ tt1^0-tt1^post6 == 0 /\ __rho_5_^0-__rho_5_^post6 == 0 /\ __const_1000^0-curtime^0+last_copy_time^0 <= 0 /\ __rho_7_^0-__rho_7_^post6 == 0 /\ -__rho_4_^post6+__rho_4_^0 == 0 /\ -__rho_6_^post6+__rho_6_^0 == 0 /\ -a22^post6+a22^0 == 0 /\ -last_copy_time^post6+last_copy_time^0 == 0), cost: 1 New rule: l8 -> l7 : wakend^0'=1, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 1 Applied preprocessing Original rule: l9 -> l7 : __rho_5_^0'=__rho_5_^post7, wakend^0'=wakend^post7, __rho_1_^0'=__rho_1_^post7, got_SIGHUP^0'=got_SIGHUP^post7, __rho_7_^0'=__rho_7_^post7, __rho_4_^0'=__rho_4_^post7, tt1^0'=tt1^post7, __const_1000^0'=__const_1000^post7, curtime^0'=curtime^post7, __rho_6_^0'=__rho_6_^post7, __rho_2_^0'=__rho_2_^post7, last_copy_time^0'=last_copy_time^post7, a22^0'=a22^post7, (__rho_2_^0-__rho_2_^post7 == 0 /\ __rho_5_^0-__rho_5_^post7 == 0 /\ curtime^0-curtime^post7 == 0 /\ got_SIGHUP^0-got_SIGHUP^post7 == 0 /\ -__rho_4_^post7+__rho_4_^0 == 0 /\ tt1^0-tt1^post7 == 0 /\ -__rho_6_^post7+__rho_6_^0 == 0 /\ __rho_1_^0-__rho_1_^post7 == 0 /\ 1-wakend^0 <= 0 /\ -wakend^post7+wakend^0 == 0 /\ -a22^post7+a22^0 == 0 /\ -last_copy_time^post7+last_copy_time^0 == 0 /\ -__const_1000^post7+__const_1000^0 == 0 /\ __rho_7_^0-__rho_7_^post7 == 0), cost: 1 New rule: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 Applied preprocessing Original rule: l9 -> l8 : __rho_5_^0'=__rho_5_^post8, wakend^0'=wakend^post8, __rho_1_^0'=__rho_1_^post8, got_SIGHUP^0'=got_SIGHUP^post8, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post8, tt1^0'=tt1^post8, __const_1000^0'=__const_1000^post8, curtime^0'=curtime^post8, __rho_6_^0'=__rho_6_^post8, __rho_2_^0'=__rho_2_^post8, last_copy_time^0'=last_copy_time^post8, a22^0'=a22^post8, (0 == 0 /\ curtime^post8-__rho_7_^post8 == 0 /\ -__rho_6_^post8+__rho_6_^0 == 0 /\ wakend^0 <= 0 /\ -__const_1000^post8+__const_1000^0 == 0 /\ wakend^0-wakend^post8 == 0 /\ got_SIGHUP^0-got_SIGHUP^post8 == 0 /\ -a22^post8+a22^0 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ tt1^0-tt1^post8 == 0 /\ -__rho_2_^post8+__rho_2_^0 == 0 /\ __rho_1_^0-__rho_1_^post8 == 0 /\ -__rho_4_^post8+__rho_4_^0 == 0 /\ __rho_5_^0-__rho_5_^post8 == 0), cost: 1 New rule: l9 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 1 Applied preprocessing Original rule: l6 -> l10 : __rho_5_^0'=__rho_5_^post9, wakend^0'=wakend^post9, __rho_1_^0'=__rho_1_^post9, got_SIGHUP^0'=got_SIGHUP^post9, __rho_7_^0'=__rho_7_^post9, __rho_4_^0'=__rho_4_^post9, tt1^0'=tt1^post9, __const_1000^0'=__const_1000^post9, curtime^0'=curtime^post9, __rho_6_^0'=__rho_6_^post9, __rho_2_^0'=__rho_2_^post9, last_copy_time^0'=last_copy_time^post9, a22^0'=a22^post9, (got_SIGHUP^0-got_SIGHUP^post9 == 0 /\ -__rho_7_^post9+__rho_7_^0 == 0 /\ curtime^0-curtime^post9 == 0 /\ tt1^0-tt1^post9 == 0 /\ wakend^0-wakend^post9 == 0 /\ -__rho_4_^post9+__rho_4_^0 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ -__rho_6_^post9+__rho_6_^0 == 0 /\ __const_1000^0-__const_1000^post9 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0 /\ -a22^post9+a22^0 == 0 /\ -last_copy_time^post9+last_copy_time^0 == 0 /\ __rho_5_^0-__rho_5_^post9 == 0), cost: 1 New rule: l6 -> l10 : TRUE, cost: 1 Applied preprocessing Original rule: l10 -> l6 : __rho_5_^0'=__rho_5_^post10, wakend^0'=wakend^post10, __rho_1_^0'=__rho_1_^post10, got_SIGHUP^0'=got_SIGHUP^post10, __rho_7_^0'=__rho_7_^post10, __rho_4_^0'=__rho_4_^post10, tt1^0'=tt1^post10, __const_1000^0'=__const_1000^post10, curtime^0'=curtime^post10, __rho_6_^0'=__rho_6_^post10, __rho_2_^0'=__rho_2_^post10, last_copy_time^0'=last_copy_time^post10, a22^0'=a22^post10, (got_SIGHUP^0-got_SIGHUP^post10 == 0 /\ -last_copy_time^post10+last_copy_time^0 == 0 /\ -__rho_7_^post10+__rho_7_^0 == 0 /\ -__rho_6_^post10+__rho_6_^0 == 0 /\ -__const_1000^post10+__const_1000^0 == 0 /\ __rho_5_^0-__rho_5_^post10 == 0 /\ curtime^0-curtime^post10 == 0 /\ tt1^0-tt1^post10 == 0 /\ -__rho_2_^post10+__rho_2_^0 == 0 /\ -__rho_4_^post10+__rho_4_^0 == 0 /\ -a22^post10+a22^0 == 0 /\ wakend^0-wakend^post10 == 0 /\ __rho_1_^0-__rho_1_^post10 == 0), cost: 1 New rule: l10 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l9 : __rho_5_^0'=__rho_5_^post11, wakend^0'=wakend^post11, __rho_1_^0'=__rho_1_^post11, got_SIGHUP^0'=got_SIGHUP^post11, __rho_7_^0'=__rho_7_^post11, __rho_4_^0'=__rho_4_^post11, tt1^0'=tt1^post11, __const_1000^0'=__const_1000^post11, curtime^0'=curtime^post11, __rho_6_^0'=__rho_6_^post11, __rho_2_^0'=__rho_2_^post11, last_copy_time^0'=last_copy_time^post11, a22^0'=a22^post11, (-__rho_4_^post11+__rho_4_^0 == 0 /\ wakend^0 <= 0 /\ -a22^post11+a22^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post11 == 0 /\ -__rho_6_^post11+__rho_6_^0 == 0 /\ tt1^0-tt1^post11 == 0 /\ curtime^0-curtime^post11 == 0 /\ __rho_2_^0-__rho_2_^post11 == 0 /\ __const_1000^0-__const_1000^post11 == 0 /\ -last_copy_time^post11+last_copy_time^0 == 0 /\ __rho_1_^0-__rho_1_^post11 == 0 /\ __rho_5_^0-__rho_5_^post11 == 0 /\ __rho_7_^0-__rho_7_^post11 == 0 /\ -wakend^post11+wakend^0 == 0), cost: 1 New rule: l1 -> l9 : wakend^0 <= 0, cost: 1 Applied preprocessing Original rule: l1 -> l9 : __rho_5_^0'=__rho_5_^post12, wakend^0'=wakend^post12, __rho_1_^0'=__rho_1_^post12, got_SIGHUP^0'=got_SIGHUP^post12, __rho_7_^0'=__rho_7_^post12, __rho_4_^0'=__rho_4_^post12, tt1^0'=tt1^post12, __const_1000^0'=__const_1000^post12, curtime^0'=curtime^post12, __rho_6_^0'=__rho_6_^post12, __rho_2_^0'=__rho_2_^post12, last_copy_time^0'=last_copy_time^post12, a22^0'=a22^post12, (0 == 0 /\ tt1^0-tt1^post12 == 0 /\ __rho_5_^0-__rho_5_^post12 == 0 /\ wakend^post12 == 0 /\ -__rho_7_^post12+__rho_7_^0 == 0 /\ __rho_2_^0-__rho_2_^post12 == 0 /\ __const_1000^0-__const_1000^post12 == 0 /\ -a22^post12+a22^0 == 0 /\ -__rho_4_^post12+__rho_4_^0 == 0 /\ 1-wakend^0 <= 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ last_copy_time^post12-__rho_6_^post12 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ -curtime^post12+curtime^0 == 0), cost: 1 New rule: l1 -> l9 : wakend^0'=0, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 1 Applied preprocessing Original rule: l2 -> l1 : __rho_5_^0'=__rho_5_^post13, wakend^0'=wakend^post13, __rho_1_^0'=__rho_1_^post13, got_SIGHUP^0'=got_SIGHUP^post13, __rho_7_^0'=__rho_7_^post13, __rho_4_^0'=__rho_4_^post13, tt1^0'=tt1^post13, __const_1000^0'=__const_1000^post13, curtime^0'=curtime^post13, __rho_6_^0'=__rho_6_^post13, __rho_2_^0'=__rho_2_^post13, last_copy_time^0'=last_copy_time^post13, a22^0'=a22^post13, (__rho_2_^0-__rho_2_^post13 == 0 /\ 1-tt1^0 <= 0 /\ curtime^0-curtime^post13 == 0 /\ -__rho_4_^post13+__rho_4_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post13 == 0 /\ -__rho_6_^post13+__rho_6_^0 == 0 /\ tt1^0-tt1^post13 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ -__const_1000^post13+__const_1000^0 == 0 /\ __rho_5_^0-__rho_5_^post13 == 0 /\ -wakend^post13+wakend^0 == 0 /\ -last_copy_time^post13+last_copy_time^0 == 0 /\ __rho_7_^0-__rho_7_^post13 == 0 /\ -a22^post13+a22^0 == 0), cost: 1 New rule: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 Applied preprocessing Original rule: l2 -> l5 : __rho_5_^0'=__rho_5_^post14, wakend^0'=wakend^post14, __rho_1_^0'=__rho_1_^post14, got_SIGHUP^0'=got_SIGHUP^post14, __rho_7_^0'=__rho_7_^post14, __rho_4_^0'=__rho_4_^post14, tt1^0'=tt1^post14, __const_1000^0'=__const_1000^post14, curtime^0'=curtime^post14, __rho_6_^0'=__rho_6_^post14, __rho_2_^0'=__rho_2_^post14, last_copy_time^0'=last_copy_time^post14, a22^0'=a22^post14, (tt1^0-tt1^post14 == 0 /\ __rho_5_^0-__rho_5_^post14 == 0 /\ __rho_2_^0-__rho_2_^post14 == 0 /\ -last_copy_time^post14+last_copy_time^0 == 0 /\ -a22^post14+a22^0 == 0 /\ -__rho_7_^post14+__rho_7_^0 == 0 /\ tt1^0 <= 0 /\ -wakend^post14+wakend^0 == 0 /\ __rho_1_^0-__rho_1_^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -__rho_6_^post14+__rho_6_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post14 == 0 /\ __rho_4_^0-__rho_4_^post14 == 0 /\ __const_1000^0-__const_1000^post14 == 0), cost: 1 New rule: l2 -> l5 : tt1^0 <= 0, cost: 1 Applied preprocessing Original rule: l11 -> l0 : __rho_5_^0'=__rho_5_^post15, wakend^0'=wakend^post15, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=got_SIGHUP^post15, __rho_7_^0'=__rho_7_^post15, __rho_4_^0'=__rho_4_^post15, tt1^0'=tt1^post15, __const_1000^0'=__const_1000^post15, curtime^0'=curtime^post15, __rho_6_^0'=__rho_6_^post15, __rho_2_^0'=__rho_2_^post15, last_copy_time^0'=last_copy_time^post15, a22^0'=a22^post15, (0 == 0 /\ -__rho_4_^post15+__rho_4_^0 == 0 /\ -a22^post15+a22^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ -__rho_2_^post15+__rho_2_^0 == 0 /\ -tt1^post15+tt1^0 == 0 /\ -1+wakend^post15 == 0 /\ __rho_7_^0-__rho_7_^post15 == 0 /\ -1+wakend^10 == 0 /\ curtime^0-curtime^post15 == 0 /\ __rho_5_^0-__rho_5_^post15 == 0 /\ got_SIGHUP^post15-__rho_2_^0 == 0 /\ __rho_6_^0-__rho_6_^post15 == 0 /\ -__const_1000^post15+__const_1000^0 == 0), cost: 1 New rule: l11 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 1 Applied preprocessing Original rule: l12 -> l11 : __rho_5_^0'=__rho_5_^post16, wakend^0'=wakend^post16, __rho_1_^0'=__rho_1_^post16, got_SIGHUP^0'=got_SIGHUP^post16, __rho_7_^0'=__rho_7_^post16, __rho_4_^0'=__rho_4_^post16, tt1^0'=tt1^post16, __const_1000^0'=__const_1000^post16, curtime^0'=curtime^post16, __rho_6_^0'=__rho_6_^post16, __rho_2_^0'=__rho_2_^post16, last_copy_time^0'=last_copy_time^post16, a22^0'=a22^post16, (__rho_5_^0-__rho_5_^post16 == 0 /\ -__rho_6_^post16+__rho_6_^0 == 0 /\ -last_copy_time^post16+last_copy_time^0 == 0 /\ -__rho_7_^post16+__rho_7_^0 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ -curtime^post16+curtime^0 == 0 /\ wakend^0-wakend^post16 == 0 /\ -a22^post16+a22^0 == 0 /\ __const_1000^0-__const_1000^post16 == 0 /\ __rho_1_^0-__rho_1_^post16 == 0 /\ __rho_4_^0-__rho_4_^post16 == 0 /\ got_SIGHUP^0-got_SIGHUP^post16 == 0 /\ tt1^0-tt1^post16 == 0), cost: 1 New rule: l12 -> l11 : TRUE, cost: 1 Simplified rules Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+got_SIGHUP^0 >= 0, cost: 1 27: l1 -> l9 : wakend^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0'=0, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 19: l5 -> l6 : TRUE, cost: 1 25: l6 -> l10 : TRUE, cost: 1 20: l7 -> l5 : __rho_4_^0'=__rho_4_^post4, 0 == 0, cost: 1 21: l8 -> l7 : 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 1 26: l10 -> l6 : TRUE, cost: 1 31: l11 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 1 32: l12 -> l11 : TRUE, cost: 1 Eliminating location l11 by chaining: Applied chaining First rule: l12 -> l11 : TRUE, cost: 1 Second rule: l11 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 1 New rule: l12 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 2 Applied deletion Removed the following rules: 31 32 Eliminating location l10 by chaining: Applied chaining First rule: l6 -> l10 : TRUE, cost: 1 Second rule: l10 -> l6 : TRUE, cost: 1 New rule: l6 -> l6 : TRUE, cost: 2 Applied deletion Removed the following rules: 25 26 Eliminated locations on linear paths Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+got_SIGHUP^0 >= 0, cost: 1 27: l1 -> l9 : wakend^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0'=0, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 19: l5 -> l6 : TRUE, cost: 1 34: l6 -> l6 : TRUE, cost: 2 20: l7 -> l5 : __rho_4_^0'=__rho_4_^post4, 0 == 0, cost: 1 21: l8 -> l7 : 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 1 33: l12 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 2 Applied nonterm Original rule: l6 -> l6 : TRUE, cost: 2 New rule: l6 -> [13] : n >= 0, cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_KAPdOl.txt Applied deletion Removed the following rules: 34 Accelerated simple loops Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+got_SIGHUP^0 >= 0, cost: 1 27: l1 -> l9 : wakend^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0'=0, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 19: l5 -> l6 : TRUE, cost: 1 35: l6 -> [13] : n >= 0, cost: NONTERM 20: l7 -> l5 : __rho_4_^0'=__rho_4_^post4, 0 == 0, cost: 1 21: l8 -> l7 : 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 1 33: l12 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 2 Applied chaining First rule: l5 -> l6 : TRUE, cost: 1 Second rule: l6 -> [13] : n >= 0, cost: NONTERM New rule: l5 -> [13] : TRUE, cost: NONTERM Applied deletion Removed the following rules: 35 Chained accelerated rules with incoming rules Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+got_SIGHUP^0 >= 0, cost: 1 27: l1 -> l9 : wakend^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0'=0, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 19: l5 -> l6 : TRUE, cost: 1 36: l5 -> [13] : TRUE, cost: NONTERM 20: l7 -> l5 : __rho_4_^0'=__rho_4_^post4, 0 == 0, cost: 1 21: l8 -> l7 : 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 1 33: l12 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+got_SIGHUP^0 >= 0, cost: 1 27: l1 -> l9 : wakend^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0'=0, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 36: l5 -> [13] : TRUE, cost: NONTERM 20: l7 -> l5 : __rho_4_^0'=__rho_4_^post4, 0 == 0, cost: 1 21: l8 -> l7 : 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 1 33: l12 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 2 Eliminating location l0 by chaining: Applied chaining First rule: l12 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 2 Second rule: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 New rule: l12 -> l1 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, (0 == 0 /\ __rho_2_^0 <= 0), cost: 3 Applied simplification Original rule: l12 -> l1 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, (0 == 0 /\ __rho_2_^0 <= 0), cost: 3 New rule: l12 -> l1 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_2_^0 <= 0, cost: 3 Applied chaining First rule: l12 -> l0 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, 0 == 0, cost: 2 Second rule: l0 -> l2 : __rho_5_^0'=__rho_5_^post1, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+got_SIGHUP^0 >= 0, cost: 1 New rule: l12 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (0 == 0 /\ -1+__rho_2_^0 >= 0), cost: 3 Applied simplification Original rule: l12 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (0 == 0 /\ -1+__rho_2_^0 >= 0), cost: 3 New rule: l12 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+__rho_2_^0 >= 0, cost: 3 Applied deletion Removed the following rules: 17 18 33 Eliminating location l9 by chaining: Applied chaining First rule: l1 -> l9 : wakend^0 <= 0, cost: 1 Second rule: l9 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 1 New rule: l1 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 2 Applied chaining First rule: l1 -> l9 : wakend^0'=0, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 1 Second rule: l9 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 1 New rule: l1 -> l8 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (0 <= 0 /\ -1+wakend^0 >= 0), cost: 2 Applied simplification Original rule: l1 -> l8 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (0 <= 0 /\ -1+wakend^0 >= 0), cost: 2 New rule: l1 -> l8 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 2 Applied deletion Removed the following rules: 23 24 27 28 Eliminating location l7 by chaining: Applied chaining First rule: l8 -> l7 : 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 1 Second rule: l7 -> l5 : __rho_4_^0'=__rho_4_^post4, 0 == 0, cost: 1 New rule: l8 -> l5 : __rho_4_^0'=__rho_4_^post4, (0 == 0 /\ 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0), cost: 2 Applied simplification Original rule: l8 -> l5 : __rho_4_^0'=__rho_4_^post4, (0 == 0 /\ 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0), cost: 2 New rule: l8 -> l5 : __rho_4_^0'=__rho_4_^post4, 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 2 Applied chaining First rule: l8 -> l7 : wakend^0'=1, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 1 Second rule: l7 -> l5 : __rho_4_^0'=__rho_4_^post4, 0 == 0, cost: 1 New rule: l8 -> l5 : wakend^0'=1, __rho_4_^0'=__rho_4_^post4, (0 == 0 /\ __const_1000^0-curtime^0+last_copy_time^0 <= 0), cost: 2 Applied simplification Original rule: l8 -> l5 : wakend^0'=1, __rho_4_^0'=__rho_4_^post4, (0 == 0 /\ __const_1000^0-curtime^0+last_copy_time^0 <= 0), cost: 2 New rule: l8 -> l5 : wakend^0'=1, __rho_4_^0'=__rho_4_^post4, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 2 Applied deletion Removed the following rules: 20 21 22 Eliminated locations on tree-shaped paths Start location: l12 39: l1 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 2 40: l1 -> l8 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 2 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 36: l5 -> [13] : TRUE, cost: NONTERM 41: l8 -> l5 : __rho_4_^0'=__rho_4_^post4, 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 2 42: l8 -> l5 : wakend^0'=1, __rho_4_^0'=__rho_4_^post4, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 2 37: l12 -> l1 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_2_^0 <= 0, cost: 3 38: l12 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+__rho_2_^0 >= 0, cost: 3 Eliminating location l2 by chaining: Applied chaining First rule: l12 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+__rho_2_^0 >= 0, cost: 3 Second rule: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 New rule: l12 -> l1 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0), cost: 4 Applied chaining First rule: l12 -> l2 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, -1+__rho_2_^0 >= 0, cost: 3 Second rule: l2 -> l5 : tt1^0 <= 0, cost: 1 New rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ __rho_5_^post1 <= 0), cost: 4 Applied deletion Removed the following rules: 29 30 38 Eliminating location l8 by chaining: Applied chaining First rule: l1 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 2 Second rule: l8 -> l5 : __rho_4_^0'=__rho_4_^post4, 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 2 New rule: l1 -> l5 : __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, (wakend^0 <= 0 /\ 1-__const_1000^0-last_copy_time^0+__rho_7_^post8 <= 0), cost: 4 Applied chaining First rule: l1 -> l8 : __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, wakend^0 <= 0, cost: 2 Second rule: l8 -> l5 : wakend^0'=1, __rho_4_^0'=__rho_4_^post4, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 2 New rule: l1 -> l5 : wakend^0'=1, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, (wakend^0 <= 0 /\ __const_1000^0+last_copy_time^0-__rho_7_^post8 <= 0), cost: 4 Applied chaining First rule: l1 -> l8 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 2 Second rule: l8 -> l5 : __rho_4_^0'=__rho_4_^post4, 1-__const_1000^0+curtime^0-last_copy_time^0 <= 0, cost: 2 New rule: l1 -> l5 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 Applied chaining First rule: l1 -> l8 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, -1+wakend^0 >= 0, cost: 2 Second rule: l8 -> l5 : wakend^0'=1, __rho_4_^0'=__rho_4_^post4, __const_1000^0-curtime^0+last_copy_time^0 <= 0, cost: 2 New rule: l1 -> l5 : wakend^0'=1, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (__rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 Applied deletion Removed the following rules: 39 40 41 42 Eliminated locations on tree-shaped paths Start location: l12 45: l1 -> l5 : __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, (wakend^0 <= 0 /\ 1-__const_1000^0-last_copy_time^0+__rho_7_^post8 <= 0), cost: 4 46: l1 -> l5 : wakend^0'=1, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, (wakend^0 <= 0 /\ __const_1000^0+last_copy_time^0-__rho_7_^post8 <= 0), cost: 4 47: l1 -> l5 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 48: l1 -> l5 : wakend^0'=1, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (__rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 36: l5 -> [13] : TRUE, cost: NONTERM 37: l12 -> l1 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_2_^0 <= 0, cost: 3 43: l12 -> l1 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0), cost: 4 44: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ __rho_5_^post1 <= 0), cost: 4 Eliminating location l1 by chaining: Applied chaining First rule: l12 -> l1 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_2_^0 <= 0, cost: 3 Second rule: l1 -> l5 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 New rule: l12 -> l5 : wakend^0'=0, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (0 >= 0 /\ 1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ __rho_2_^0 <= 0), cost: 7 Applied simplification Original rule: l12 -> l5 : wakend^0'=0, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (0 >= 0 /\ 1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ __rho_2_^0 <= 0), cost: 7 New rule: l12 -> l5 : wakend^0'=0, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ __rho_2_^0 <= 0), cost: 7 Applied chaining First rule: l12 -> l1 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_2_^0 <= 0, cost: 3 Second rule: l1 -> l5 : wakend^0'=1, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (__rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 New rule: l12 -> l5 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (0 >= 0 /\ __rho_2_^0 <= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: 7 Applied simplification Original rule: l12 -> l5 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (0 >= 0 /\ __rho_2_^0 <= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: 7 New rule: l12 -> l5 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (__rho_2_^0 <= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: 7 Applied chaining First rule: l12 -> l1 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0), cost: 4 Second rule: l1 -> l5 : wakend^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 New rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=0, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, tt1^0'=__rho_5_^post1, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, a22^0'=1, (0 >= 0 /\ -1+__rho_2_^0 >= 0 /\ 1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+__rho_5_^post1 >= 0), cost: 8 Applied simplification Original rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=0, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, tt1^0'=__rho_5_^post1, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, a22^0'=1, (0 >= 0 /\ -1+__rho_2_^0 >= 0 /\ 1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+__rho_5_^post1 >= 0), cost: 8 New rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=0, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, tt1^0'=__rho_5_^post1, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ 1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+__rho_5_^post1 >= 0), cost: 8 Applied chaining First rule: l12 -> l1 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0), cost: 4 Second rule: l1 -> l5 : wakend^0'=1, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (__rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 New rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, tt1^0'=__rho_5_^post1, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, a22^0'=1, (0 >= 0 /\ -1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: 8 Applied simplification Original rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, tt1^0'=__rho_5_^post1, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, a22^0'=1, (0 >= 0 /\ -1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: 8 New rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, tt1^0'=__rho_5_^post1, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: 8 Applied deletion Removed the following rules: 37 43 45 46 47 48 Eliminating location l5 by chaining: Applied chaining First rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, tt1^0'=__rho_5_^post1, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ __rho_5_^post1 <= 0), cost: 4 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (-1+__rho_2_^0 >= 0 /\ __rho_5_^post1 <= 0), cost: NONTERM Applied chaining First rule: l12 -> l5 : wakend^0'=0, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ __rho_2_^0 <= 0), cost: 7 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ __rho_2_^0 <= 0), cost: NONTERM Applied chaining First rule: l12 -> l5 : wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=__rho_2_^0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, (__rho_2_^0 <= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: 7 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (__rho_2_^0 <= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: NONTERM Applied chaining First rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=0, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, tt1^0'=__rho_5_^post1, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ 1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+__rho_5_^post1 >= 0), cost: 8 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (-1+__rho_2_^0 >= 0 /\ 1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+__rho_5_^post1 >= 0), cost: NONTERM Applied chaining First rule: l12 -> l5 : __rho_5_^0'=__rho_5_^post1, wakend^0'=1, __rho_1_^0'=__rho_1_^post15, got_SIGHUP^0'=0, __rho_7_^0'=__rho_7_^post8, __rho_4_^0'=__rho_4_^post4, tt1^0'=__rho_5_^post1, curtime^0'=__rho_7_^post8, __rho_6_^0'=__rho_6_^post12, last_copy_time^0'=__rho_6_^post12, a22^0'=1, (-1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: 8 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (-1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: NONTERM Applied deletion Removed the following rules: 36 44 49 50 51 52 Eliminated locations on tree-shaped paths Start location: l12 53: l12 -> [13] : (-1+__rho_2_^0 >= 0 /\ __rho_5_^post1 <= 0), cost: NONTERM 54: l12 -> [13] : (1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ __rho_2_^0 <= 0), cost: NONTERM 55: l12 -> [13] : (__rho_2_^0 <= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: NONTERM 56: l12 -> [13] : (-1+__rho_2_^0 >= 0 /\ 1-__rho_6_^post12-__const_1000^0+__rho_7_^post8 <= 0 /\ -1+__rho_5_^post1 >= 0), cost: NONTERM 57: l12 -> [13] : (-1+__rho_2_^0 >= 0 /\ -1+__rho_5_^post1 >= 0 /\ __rho_6_^post12+__const_1000^0-__rho_7_^post8 <= 0), cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 53 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: (-1+__rho_2_^0 >= 0 /\ __rho_5_^post1 <= 0)