WORST_CASE(Omega(0),?) Initial ITS Start location: l14 0: l0 -> l1 : a_264^0'=a_264^post0, l_27^0'=l_27^post0, i_187^0'=i_187^post0, t_32^0'=t_32^post0, rv_13^0'=rv_13^post0, y_20^0'=y_20^post0, a_158^0'=a_158^post0, x_195^0'=x_195^post0, i_98^0'=i_98^post0, h_15^0'=h_15^post0, r_57^0'=r_57^post0, r_135^0'=r_135^post0, x_140^0'=x_140^post0, st_16^0'=st_16^post0, a_76^0'=a_76^post0, a_239^0'=a_239^post0, x_21^0'=x_21^post0, l_203^0'=l_203^post0, i_115^0'=i_115^post0, rt_11^0'=rt_11^post0, r_37^0'=r_37^post0, a_123^0'=a_123^post0, x_17^0'=x_17^post0, t_24^0'=t_24^post0, f_190^0'=f_190^post0, a_290^0'=a_290^post0, nd_12^0'=nd_12^post0, i_28^0'=i_28^post0, tp_33^0'=tp_33^post0, rv_31^0'=rv_31^post0, a_204^0'=a_204^post0, x_19^0'=x_19^post0, l_143^0'=l_143^post0, h_30^0'=h_30^post0, r_92^0'=r_92^post0, r_183^0'=r_183^post0, x_14^0'=x_14^post0, st_29^0'=st_29^post0, ct_18^0'=ct_18^post0, (0 == 0 /\ -f_190^post0+f_190^0 == 0 /\ -a_204^post0+a_204^0 == 0 /\ -a_290^post0+a_290^0 == 0 /\ h_15^0-h_15^post0 == 0 /\ l_143^0-l_143^post0 == 0 /\ a_264^0-a_264^post0 == 0 /\ a_76^0-a_76^post0 == 0 /\ l_203^0-l_203^post0 == 0 /\ t_32^0-t_32^post0 == 0 /\ rv_13^post0-nd_12^10 == 0 /\ -st_16^post0+st_16^0 == 0 /\ -x_19^post0+x_19^0 == 0 /\ -h_30^post0 <= 0 /\ -tp_33^post0+tp_33^0 == 0 /\ i_28^post0 <= 0 /\ i_28^post0 == 0 /\ -a_239^post0+a_239^0 == 0 /\ -r_92^post0+r_92^0 == 0 /\ -st_29^post0+st_29^0 == 0 /\ -i_28^post0 <= 0 /\ r_135^0-r_135^post0 == 0 /\ -ct_18^post0+ct_18^0 == 0 /\ -a_123^post0+a_123^0 == 0 /\ i_115^0-i_115^post0 == 0 /\ -rv_13^post0+l_27^post0 <= 0 /\ -rv_13^post0+l_27^post0 == 0 /\ -r_183^post0+r_183^0 == 0 /\ a_158^0-a_158^post0 == 0 /\ x_140^0-x_140^post0 == 0 /\ -x_21^post0+x_21^0 == 0 /\ x_195^0-x_195^post0 == 0 /\ r_37^0-r_37^post0 == 0 /\ rv_13^post0-l_27^post0 <= 0 /\ h_30^post0 <= 0 /\ h_30^post0 == 0 /\ i_98^0-i_98^post0 == 0 /\ -x_17^post0+x_17^0 == 0 /\ -rt_11^post0+rt_11^0 == 0 /\ i_187^0-i_187^post0 == 0 /\ -t_24^post0+t_24^0 == 0 /\ -x_14^post0+x_14^0 == 0 /\ rv_31^0-rv_31^post0 == 0 /\ r_57^0-r_57^post0 == 0 /\ y_20^0-y_20^post0 == 0), cost: 1 18: l1 -> l3 : a_264^0'=a_264^post18, l_27^0'=l_27^post18, i_187^0'=i_187^post18, t_32^0'=t_32^post18, rv_13^0'=rv_13^post18, y_20^0'=y_20^post18, a_158^0'=a_158^post18, x_195^0'=x_195^post18, i_98^0'=i_98^post18, h_15^0'=h_15^post18, r_57^0'=r_57^post18, r_135^0'=r_135^post18, x_140^0'=x_140^post18, st_16^0'=st_16^post18, a_76^0'=a_76^post18, a_239^0'=a_239^post18, x_21^0'=x_21^post18, l_203^0'=l_203^post18, i_115^0'=i_115^post18, rt_11^0'=rt_11^post18, r_37^0'=r_37^post18, a_123^0'=a_123^post18, x_17^0'=x_17^post18, t_24^0'=t_24^post18, f_190^0'=f_190^post18, a_290^0'=a_290^post18, nd_12^0'=nd_12^post18, i_28^0'=i_28^post18, tp_33^0'=tp_33^post18, rv_31^0'=rv_31^post18, a_204^0'=a_204^post18, x_19^0'=x_19^post18, l_143^0'=l_143^post18, h_30^0'=h_30^post18, r_92^0'=r_92^post18, r_183^0'=r_183^post18, x_14^0'=x_14^post18, st_29^0'=st_29^post18, ct_18^0'=ct_18^post18, (0 == 0 /\ -y_20^130 <= 0 /\ -r_183^post18+r_183^0 == 0 /\ -x_19^130 <= 0 /\ -h_15^post18+x_17^110 <= 0 /\ -h_15^post18+x_17^110 == 0 /\ h_15^post18-x_14^post18 <= 0 /\ -r_37^post18+r_37^0 == 0 /\ r_135^0-r_135^post18 == 0 /\ a_123^0-a_123^post18 == 0 /\ -r_92^post18+r_92^0 == 0 /\ -x_17^110 <= 0 /\ a_204^0-a_204^post18 == 0 /\ a_158^0-a_158^post18 == 0 /\ rv_13^110 <= 0 /\ h_15^post18-rt_11^120 == 0 /\ -x_19^130+x_21^130 <= 0 /\ -x_19^130+x_21^130 == 0 /\ -y_20^130+x_21^130 <= 0 /\ -ct_18^13 <= 0 /\ h_15^post18 <= 0 /\ -a_290^post18+a_290^0 == 0 /\ h_15^post18-x_17^110 <= 0 /\ -h_15^post18+x_14^post18 <= 0 /\ -h_15^post18+x_14^post18 == 0 /\ r_57^0-r_57^post18 == 0 /\ -x_14^post18 <= 0 /\ -a_76^post18+a_76^0 == 0 /\ -h_15^post18 <= 0 /\ x_17^110 <= 0 /\ -a_239^post18+a_239^0 == 0 /\ st_16^0-st_16^post18 == 0 /\ x_19^130 <= 0 /\ y_20^130 <= 0 /\ x_19^130-x_21^130 <= 0 /\ y_20^130-x_21^130 <= 0 /\ a_264^0-a_264^post18 == 0 /\ rv_13^post18 <= 0 /\ f_190^0-f_190^post18 == 0 /\ -l_143^post18+l_143^0 == 0 /\ nd_12^0-nd_12^post18 == 0 /\ st_29^120-h_30^0 == 0 /\ -y_20^130+ct_18^13 <= 0 /\ -x_21^130 <= 0 /\ -x_17^110+x_19^130 <= 0 /\ -x_17^110+x_19^130 == 0 /\ rv_13^210 <= 0 /\ x_21^130 <= 0 /\ l_27^0-i_28^0 <= 0 /\ l_203^0-l_203^post18 == 0 /\ x_195^0-x_195^post18 == 0 /\ i_98^0-i_98^post18 == 0 /\ x_14^post18 <= 0 /\ -x_140^post18+x_140^0 == 0 /\ -st_29^120+rt_11^120 == 0 /\ y_20^130-ct_18^13 <= 0 /\ y_20^130-ct_18^13 == 0 /\ x_17^110-x_19^130 <= 0 /\ rt_11^post18-st_16^0 == 0 /\ -i_115^post18+i_115^0 == 0 /\ ct_18^13 <= 0 /\ ct_18^13 == 0 /\ i_187^0-i_187^post18 == 0), cost: 1 19: l1 -> l7 : a_264^0'=a_264^post19, l_27^0'=l_27^post19, i_187^0'=i_187^post19, t_32^0'=t_32^post19, rv_13^0'=rv_13^post19, y_20^0'=y_20^post19, a_158^0'=a_158^post19, x_195^0'=x_195^post19, i_98^0'=i_98^post19, h_15^0'=h_15^post19, r_57^0'=r_57^post19, r_135^0'=r_135^post19, x_140^0'=x_140^post19, st_16^0'=st_16^post19, a_76^0'=a_76^post19, a_239^0'=a_239^post19, x_21^0'=x_21^post19, l_203^0'=l_203^post19, i_115^0'=i_115^post19, rt_11^0'=rt_11^post19, r_37^0'=r_37^post19, a_123^0'=a_123^post19, x_17^0'=x_17^post19, t_24^0'=t_24^post19, f_190^0'=f_190^post19, a_290^0'=a_290^post19, nd_12^0'=nd_12^post19, i_28^0'=i_28^post19, tp_33^0'=tp_33^post19, rv_31^0'=rv_31^post19, a_204^0'=a_204^post19, x_19^0'=x_19^post19, l_143^0'=l_143^post19, h_30^0'=h_30^post19, r_92^0'=r_92^post19, r_183^0'=r_183^post19, x_14^0'=x_14^post19, st_29^0'=st_29^post19, ct_18^0'=ct_18^post19, (0 == 0 /\ -rv_31^post19+t_32^post19 <= 0 /\ -x_21^post19+x_21^0 == 0 /\ -x_14^post19+x_14^0 == 0 /\ r_57^0-r_57^post19 == 0 /\ -i_115^post19+i_115^0 == 0 /\ y_20^0-y_20^post19 == 0 /\ -x_195^post19+x_195^0 == 0 /\ l_143^0-l_143^post19 == 0 /\ -h_30^post19+t_32^post19 <= 0 /\ -1+i_28^post19-i_28^0 == 0 /\ h_30^post19-rv_31^post19 <= 0 /\ -a_290^post19+a_290^0 == 0 /\ -l_27^0+rv_13^post19 <= 0 /\ rv_31^post19-t_32^post19 <= 0 /\ a_76^0-a_76^post19 == 0 /\ -a_239^post19+a_239^0 == 0 /\ -st_29^post19+st_29^0 == 0 /\ -ct_18^post19+ct_18^0 == 0 /\ a_123^0-a_123^post19 == 0 /\ r_135^0-r_135^post19 == 0 /\ h_30^post19-t_32^post19 <= 0 /\ h_30^post19-t_32^post19 == 0 /\ -nd_12^post19+nd_12^0 == 0 /\ -h_30^post19+rv_31^post19 <= 0 /\ -st_16^post19+st_16^0 == 0 /\ -x_19^post19+x_19^0 == 0 /\ l_27^0-l_27^post19 == 0 /\ l_27^0-rv_13^post19 <= 0 /\ a_264^0-a_264^post19 == 0 /\ -r_92^post19+r_92^0 == 0 /\ -t_24^post19+t_24^0 == 0 /\ h_15^0-h_15^post19 == 0 /\ -r_37^post19+r_37^0 == 0 /\ i_98^0-i_98^post19 == 0 /\ x_17^0-x_17^post19 == 0 /\ x_140^0-x_140^post19 == 0 /\ -rt_11^post19+rt_11^0 == 0 /\ -f_190^post19+f_190^0 == 0 /\ -l_203^post19+l_203^0 == 0 /\ -tp_33^0+t_32^post19 == 0 /\ -r_183^post19+r_183^0 == 0 /\ 1-l_27^0 <= 0 /\ a_158^0-a_158^post19 == 0 /\ i_187^0-i_187^post19 == 0 /\ 1-i_28^post19 <= 0 /\ -1+i_28^post19 <= 0 /\ 1-l_27^0+i_28^0 <= 0 /\ -a_204^post19+a_204^0 == 0), cost: 1 1: l2 -> l3 : a_264^0'=a_264^post1, l_27^0'=l_27^post1, i_187^0'=i_187^post1, t_32^0'=t_32^post1, rv_13^0'=rv_13^post1, y_20^0'=y_20^post1, a_158^0'=a_158^post1, x_195^0'=x_195^post1, i_98^0'=i_98^post1, h_15^0'=h_15^post1, r_57^0'=r_57^post1, r_135^0'=r_135^post1, x_140^0'=x_140^post1, st_16^0'=st_16^post1, a_76^0'=a_76^post1, a_239^0'=a_239^post1, x_21^0'=x_21^post1, l_203^0'=l_203^post1, i_115^0'=i_115^post1, rt_11^0'=rt_11^post1, r_37^0'=r_37^post1, a_123^0'=a_123^post1, x_17^0'=x_17^post1, t_24^0'=t_24^post1, f_190^0'=f_190^post1, a_290^0'=a_290^post1, nd_12^0'=nd_12^post1, i_28^0'=i_28^post1, tp_33^0'=tp_33^post1, rv_31^0'=rv_31^post1, a_204^0'=a_204^post1, x_19^0'=x_19^post1, l_143^0'=l_143^post1, h_30^0'=h_30^post1, r_92^0'=r_92^post1, r_183^0'=r_183^post1, x_14^0'=x_14^post1, st_29^0'=st_29^post1, ct_18^0'=ct_18^post1, (0 == 0 /\ a_76^0-a_76^post1 == 0 /\ r_135^0-r_135^post1 == 0 /\ 2-rv_13^post1 <= 0 /\ -x_14^post1+x_14^0 == 0 /\ i_28^0-i_28^post1 == 0 /\ t_32^0-t_32^post1 == 0 /\ st_16^0-st_16^post1 == 0 /\ -l_203^post1+l_203^0 == 0 /\ 1-rv_13^post1 <= 0 /\ h_15^0-h_15^post1 == 0 /\ -st_16^0+rt_11^post1 == 0 /\ -r_92^post1+r_92^0 == 0 /\ -h_30^post1+h_30^0 == 0 /\ -st_29^post1+st_29^0 == 0 /\ f_190^0-f_190^post1 == 0 /\ -y_20^0+x_21^0 <= 0 /\ -x_195^post1+x_195^0 == 0 /\ -nd_12^post1+nd_12^0 == 0 /\ a_158^0-a_158^post1 == 0 /\ -i_187^post1+i_187^0 == 0 /\ i_115^0-i_115^post1 == 0 /\ tp_33^0-tp_33^post1 == 0 /\ l_27^0-l_27^post1 == 0 /\ -l_143^post1+l_143^0 == 0 /\ y_20^0-x_21^0 <= 0 /\ r_57^0-r_57^post1 == 0 /\ -a_204^post1+a_204^0 == 0 /\ -a_264^0 <= 0 /\ -r_183^post1+r_183^0 == 0 /\ a_239^0-a_239^post1 == 0 /\ a_290^0-a_290^post1 == 0 /\ a_264^0-a_264^post1 == 0 /\ i_98^0-i_98^post1 == 0 /\ x_140^0-x_140^post1 == 0 /\ -r_37^post1+r_37^0 == 0 /\ a_123^0-a_123^post1 == 0 /\ -rv_31^post1+rv_31^0 == 0), cost: 1 2: l2 -> l4 : a_264^0'=a_264^post2, l_27^0'=l_27^post2, i_187^0'=i_187^post2, t_32^0'=t_32^post2, rv_13^0'=rv_13^post2, y_20^0'=y_20^post2, a_158^0'=a_158^post2, x_195^0'=x_195^post2, i_98^0'=i_98^post2, h_15^0'=h_15^post2, r_57^0'=r_57^post2, r_135^0'=r_135^post2, x_140^0'=x_140^post2, st_16^0'=st_16^post2, a_76^0'=a_76^post2, a_239^0'=a_239^post2, x_21^0'=x_21^post2, l_203^0'=l_203^post2, i_115^0'=i_115^post2, rt_11^0'=rt_11^post2, r_37^0'=r_37^post2, a_123^0'=a_123^post2, x_17^0'=x_17^post2, t_24^0'=t_24^post2, f_190^0'=f_190^post2, a_290^0'=a_290^post2, nd_12^0'=nd_12^post2, i_28^0'=i_28^post2, tp_33^0'=tp_33^post2, rv_31^0'=rv_31^post2, a_204^0'=a_204^post2, x_19^0'=x_19^post2, l_143^0'=l_143^post2, h_30^0'=h_30^post2, r_92^0'=r_92^post2, r_183^0'=r_183^post2, x_14^0'=x_14^post2, st_29^0'=st_29^post2, ct_18^0'=ct_18^post2, (0 == 0 /\ -y_20^0+ct_18^post2 <= 0 /\ -a_239^post2+a_239^0 == 0 /\ -1+a_264^0-a_290^post2 <= 0 /\ t_32^0-t_32^post2 == 0 /\ r_57^0-r_57^post2 == 0 /\ 1-rv_13^post2 <= 0 /\ y_20^0 <= 0 /\ -x_195^post2+x_195^0 == 0 /\ y_20^0-y_20^post2 == 0 /\ ct_18^post2 <= 0 /\ -a_290^post2+a_264^post2 <= 0 /\ x_19^post2-x_17^post2 <= 0 /\ -r_183^post2+r_183^0 == 0 /\ x_19^post2-h_15^post2 <= 0 /\ -r_92^post2+r_92^0 == 0 /\ y_20^0-ct_18^post2 <= 0 /\ -x_21^post2+x_21^0 == 0 /\ x_140^0-x_140^post2 == 0 /\ 2-rv_13^post2 <= 0 /\ x_14^post2 <= 0 /\ -l_143^post2+l_143^0 == 0 /\ -i_115^post2+i_115^0 == 0 /\ -i_28^post2+i_28^0 == 0 /\ l_203^0-l_203^post2 == 0 /\ -x_14^post2 <= 0 /\ l_27^0-l_27^post2 == 0 /\ a_290^post2-a_264^post2 <= 0 /\ -x_19^post2+x_17^post2 <= 0 /\ a_76^0-a_76^post2 == 0 /\ -r_135^post2+r_135^0 == 0 /\ -x_19^post2+h_15^post2 <= 0 /\ -rt_11^post2+rt_11^0 == 0 /\ -x_17^post2+h_15^post2 <= 0 /\ -ct_18^post2 <= 0 /\ i_187^0-i_187^post2 == 0 /\ 1-a_264^0+a_290^post2 <= 0 /\ -y_20^0 <= 0 /\ rv_31^0-rv_31^post2 == 0 /\ -nd_12^post2+nd_12^0 == 0 /\ -a_204^post2+a_204^0 == 0 /\ -a_123^post2+a_123^0 == 0 /\ -st_16^post2+st_16^0 == 0 /\ i_98^0-i_98^post2 == 0 /\ f_190^0-f_190^post2 == 0 /\ x_17^post2-h_15^post2 <= 0 /\ a_158^0-a_158^post2 == 0 /\ -a_264^0 <= 0 /\ -tp_33^post2+tp_33^0 == 0 /\ -h_30^post2+h_30^0 == 0 /\ t_24^post2-x_21^0 == 0 /\ -st_29^post2+st_29^0 == 0), cost: 1 3: l4 -> l2 : a_264^0'=a_264^post3, l_27^0'=l_27^post3, i_187^0'=i_187^post3, t_32^0'=t_32^post3, rv_13^0'=rv_13^post3, y_20^0'=y_20^post3, a_158^0'=a_158^post3, x_195^0'=x_195^post3, i_98^0'=i_98^post3, h_15^0'=h_15^post3, r_57^0'=r_57^post3, r_135^0'=r_135^post3, x_140^0'=x_140^post3, st_16^0'=st_16^post3, a_76^0'=a_76^post3, a_239^0'=a_239^post3, x_21^0'=x_21^post3, l_203^0'=l_203^post3, i_115^0'=i_115^post3, rt_11^0'=rt_11^post3, r_37^0'=r_37^post3, a_123^0'=a_123^post3, x_17^0'=x_17^post3, t_24^0'=t_24^post3, f_190^0'=f_190^post3, a_290^0'=a_290^post3, nd_12^0'=nd_12^post3, i_28^0'=i_28^post3, tp_33^0'=tp_33^post3, rv_31^0'=rv_31^post3, a_204^0'=a_204^post3, x_19^0'=x_19^post3, l_143^0'=l_143^post3, h_30^0'=h_30^post3, r_92^0'=r_92^post3, r_183^0'=r_183^post3, x_14^0'=x_14^post3, st_29^0'=st_29^post3, ct_18^0'=ct_18^post3, (-r_92^post3+r_92^0 == 0 /\ -l_143^post3+l_143^0 == 0 /\ -r_135^post3+r_135^0 == 0 /\ rv_13^0-rv_13^post3 == 0 /\ -r_37^post3+r_37^0 == 0 /\ a_158^0-a_158^post3 == 0 /\ -i_28^post3+i_28^0 == 0 /\ st_16^0-st_16^post3 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ -t_24^post3+t_24^0 == 0 /\ l_27^0-l_27^post3 == 0 /\ r_57^0-r_57^post3 == 0 /\ l_203^0-l_203^post3 == 0 /\ -r_183^post3+r_183^0 == 0 /\ y_20^0-y_20^post3 == 0 /\ i_98^0-i_98^post3 == 0 /\ x_17^0-x_17^post3 == 0 /\ x_19^0-x_19^post3 == 0 /\ x_140^0-x_140^post3 == 0 /\ -a_204^post3+a_204^0 == 0 /\ h_15^0-h_15^post3 == 0 /\ -x_14^post3+x_14^0 == 0 /\ a_76^0-a_76^post3 == 0 /\ -x_21^post3+x_21^0 == 0 /\ -i_115^post3+i_115^0 == 0 /\ f_190^0-f_190^post3 == 0 /\ st_29^0-st_29^post3 == 0 /\ -a_123^post3+a_123^0 == 0 /\ i_187^0-i_187^post3 == 0 /\ -rv_31^post3+rv_31^0 == 0 /\ -a_290^post3+a_290^0 == 0 /\ -a_239^post3+a_239^0 == 0 /\ -h_30^post3+h_30^0 == 0 /\ -tp_33^post3+tp_33^0 == 0 /\ x_195^0-x_195^post3 == 0 /\ -ct_18^post3+ct_18^0 == 0 /\ -t_32^post3+t_32^0 == 0 /\ -nd_12^post3+nd_12^0 == 0 /\ a_264^0-a_264^post3 == 0), cost: 1 4: l5 -> l2 : a_264^0'=a_264^post4, l_27^0'=l_27^post4, i_187^0'=i_187^post4, t_32^0'=t_32^post4, rv_13^0'=rv_13^post4, y_20^0'=y_20^post4, a_158^0'=a_158^post4, x_195^0'=x_195^post4, i_98^0'=i_98^post4, h_15^0'=h_15^post4, r_57^0'=r_57^post4, r_135^0'=r_135^post4, x_140^0'=x_140^post4, st_16^0'=st_16^post4, a_76^0'=a_76^post4, a_239^0'=a_239^post4, x_21^0'=x_21^post4, l_203^0'=l_203^post4, i_115^0'=i_115^post4, rt_11^0'=rt_11^post4, r_37^0'=r_37^post4, a_123^0'=a_123^post4, x_17^0'=x_17^post4, t_24^0'=t_24^post4, f_190^0'=f_190^post4, a_290^0'=a_290^post4, nd_12^0'=nd_12^post4, i_28^0'=i_28^post4, tp_33^0'=tp_33^post4, rv_31^0'=rv_31^post4, a_204^0'=a_204^post4, x_19^0'=x_19^post4, l_143^0'=l_143^post4, h_30^0'=h_30^post4, r_92^0'=r_92^post4, r_183^0'=r_183^post4, x_14^0'=x_14^post4, st_29^0'=st_29^post4, ct_18^0'=ct_18^post4, (0 == 0 /\ -a_239^0 <= 0 /\ i_98^0-i_98^post4 == 0 /\ x_140^0-x_140^post4 == 0 /\ -r_183^post4+r_183^0 == 0 /\ -i_28^post4+i_28^0 == 0 /\ x_19^post4-x_17^post4 <= 0 /\ -ct_18^post4 <= 0 /\ -tp_33^post4+tp_33^0 == 0 /\ a_204^0-a_204^post4 == 0 /\ -a_239^post4+a_239^0 == 0 /\ i_187^0-i_187^post4 == 0 /\ a_158^0-a_158^post4 == 0 /\ y_20^0 <= 0 /\ -r_37^post4+r_37^0 == 0 /\ st_16^0-st_16^post4 == 0 /\ -r_92^post4+r_92^0 == 0 /\ h_15^post4-x_17^post4 <= 0 /\ -r_135^post4+r_135^0 == 0 /\ -x_21^post4+x_21^0 == 0 /\ -a_290^post4+a_290^0 == 0 /\ -x_19^post4+x_17^post4 <= 0 /\ -i_115^post4+i_115^0 == 0 /\ -l_143^post4+l_143^0 == 0 /\ ct_18^post4 <= 0 /\ r_57^0-r_57^post4 == 0 /\ a_76^0-a_76^post4 == 0 /\ l_203^0-l_203^post4 == 0 /\ -h_15^post4+x_17^post4 <= 0 /\ t_32^0-t_32^post4 == 0 /\ y_20^0-y_20^post4 == 0 /\ -y_20^0 <= 0 /\ x_14^post4 <= 0 /\ rv_31^0-rv_31^post4 == 0 /\ -h_30^post4+h_30^0 == 0 /\ -y_20^0+ct_18^post4 <= 0 /\ 2-rv_13^post4 <= 0 /\ -x_19^post4+h_15^post4 <= 0 /\ -st_29^post4+st_29^0 == 0 /\ -a_123^post4+a_123^0 == 0 /\ nd_12^0-nd_12^post4 == 0 /\ f_190^0-f_190^post4 == 0 /\ t_24^post4-x_21^0 == 0 /\ -l_27^post4+l_27^0 == 0 /\ y_20^0-ct_18^post4 <= 0 /\ a_264^0-a_264^post4 == 0 /\ -rt_11^post4+rt_11^0 == 0 /\ x_19^post4-h_15^post4 <= 0 /\ 1-rv_13^post4 <= 0 /\ x_195^0-x_195^post4 == 0 /\ -x_14^post4 <= 0), cost: 1 5: l5 -> l3 : a_264^0'=a_264^post5, l_27^0'=l_27^post5, i_187^0'=i_187^post5, t_32^0'=t_32^post5, rv_13^0'=rv_13^post5, y_20^0'=y_20^post5, a_158^0'=a_158^post5, x_195^0'=x_195^post5, i_98^0'=i_98^post5, h_15^0'=h_15^post5, r_57^0'=r_57^post5, r_135^0'=r_135^post5, x_140^0'=x_140^post5, st_16^0'=st_16^post5, a_76^0'=a_76^post5, a_239^0'=a_239^post5, x_21^0'=x_21^post5, l_203^0'=l_203^post5, i_115^0'=i_115^post5, rt_11^0'=rt_11^post5, r_37^0'=r_37^post5, a_123^0'=a_123^post5, x_17^0'=x_17^post5, t_24^0'=t_24^post5, f_190^0'=f_190^post5, a_290^0'=a_290^post5, nd_12^0'=nd_12^post5, i_28^0'=i_28^post5, tp_33^0'=tp_33^post5, rv_31^0'=rv_31^post5, a_204^0'=a_204^post5, x_19^0'=x_19^post5, l_143^0'=l_143^post5, h_30^0'=h_30^post5, r_92^0'=r_92^post5, r_183^0'=r_183^post5, x_14^0'=x_14^post5, st_29^0'=st_29^post5, ct_18^0'=ct_18^post5, (0 == 0 /\ -st_16^post5+st_16^0 == 0 /\ -a_239^0 <= 0 /\ -rv_31^post5+rv_31^0 == 0 /\ -nd_12^post5+nd_12^0 == 0 /\ x_140^0-x_140^post5 == 0 /\ a_158^0-a_158^post5 == 0 /\ 1-rv_13^post5 <= 0 /\ -st_29^post5+st_29^0 == 0 /\ rt_11^post5-st_16^0 == 0 /\ i_187^0-i_187^post5 == 0 /\ -h_30^post5+h_30^0 == 0 /\ i_28^0-i_28^post5 == 0 /\ -l_203^post5+l_203^0 == 0 /\ f_190^0-f_190^post5 == 0 /\ 2-rv_13^post5 <= 0 /\ a_123^0-a_123^post5 == 0 /\ -a_204^post5+a_204^0 == 0 /\ l_143^0-l_143^post5 == 0 /\ t_32^0-t_32^post5 == 0 /\ r_57^0-r_57^post5 == 0 /\ a_264^0-a_264^post5 == 0 /\ -y_20^0+x_21^0 <= 0 /\ -x_14^post5+x_14^0 == 0 /\ -r_37^post5+r_37^0 == 0 /\ -x_195^post5+x_195^0 == 0 /\ -r_183^post5+r_183^0 == 0 /\ -r_92^post5+r_92^0 == 0 /\ -tp_33^post5+tp_33^0 == 0 /\ -r_135^post5+r_135^0 == 0 /\ a_239^0-a_239^post5 == 0 /\ l_27^0-l_27^post5 == 0 /\ y_20^0-x_21^0 <= 0 /\ -a_290^post5+a_290^0 == 0 /\ a_76^0-a_76^post5 == 0 /\ -i_115^post5+i_115^0 == 0 /\ i_98^0-i_98^post5 == 0), cost: 1 6: l6 -> l2 : a_264^0'=a_264^post6, l_27^0'=l_27^post6, i_187^0'=i_187^post6, t_32^0'=t_32^post6, rv_13^0'=rv_13^post6, y_20^0'=y_20^post6, a_158^0'=a_158^post6, x_195^0'=x_195^post6, i_98^0'=i_98^post6, h_15^0'=h_15^post6, r_57^0'=r_57^post6, r_135^0'=r_135^post6, x_140^0'=x_140^post6, st_16^0'=st_16^post6, a_76^0'=a_76^post6, a_239^0'=a_239^post6, x_21^0'=x_21^post6, l_203^0'=l_203^post6, i_115^0'=i_115^post6, rt_11^0'=rt_11^post6, r_37^0'=r_37^post6, a_123^0'=a_123^post6, x_17^0'=x_17^post6, t_24^0'=t_24^post6, f_190^0'=f_190^post6, a_290^0'=a_290^post6, nd_12^0'=nd_12^post6, i_28^0'=i_28^post6, tp_33^0'=tp_33^post6, rv_31^0'=rv_31^post6, a_204^0'=a_204^post6, x_19^0'=x_19^post6, l_143^0'=l_143^post6, h_30^0'=h_30^post6, r_92^0'=r_92^post6, r_183^0'=r_183^post6, x_14^0'=x_14^post6, st_29^0'=st_29^post6, ct_18^0'=ct_18^post6, (0 == 0 /\ -a_290^post6+a_290^0 == 0 /\ ct_18^post6 <= 0 /\ 2-rv_13^post6 <= 0 /\ -x_195^post6+x_195^0 == 0 /\ -nd_12^post6+nd_12^0 == 0 /\ -x_17^post6+x_19^post6 <= 0 /\ y_20^0 <= 0 /\ -a_204^post6+a_204^0 == 0 /\ -st_16^post6+st_16^0 == 0 /\ a_76^0-a_76^post6 == 0 /\ t_24^post6-h_15^post6 <= 0 /\ x_14^post6 <= 0 /\ -r_92^post6+r_92^0 == 0 /\ t_32^0-t_32^post6 == 0 /\ -1-a_239^post6+l_143^post6 <= 0 /\ 1-rv_13^post6 <= 0 /\ r_135^0-r_135^post6 == 0 /\ l_27^0-l_27^post6 == 0 /\ -tp_33^post6+tp_33^0 == 0 /\ x_17^post6-x_19^post6 <= 0 /\ a_264^0-a_264^post6 == 0 /\ -st_29^post6+st_29^0 == 0 /\ t_24^post6-x_21^0 == 0 /\ -l_143^0 <= 0 /\ -t_24^post6+h_15^post6 <= 0 /\ -h_30^post6+h_30^0 == 0 /\ a_123^0-a_123^post6 == 0 /\ x_140^0-x_140^post6 == 0 /\ a_158^0-a_158^post6 == 0 /\ x_17^post6-h_15^post6 <= 0 /\ -y_20^0 <= 0 /\ i_115^0-i_115^post6 == 0 /\ l_203^0-l_203^post6 == 0 /\ -x_14^post6 <= 0 /\ -x_19^post6+h_15^post6 <= 0 /\ -a_264^0+a_239^post6 <= 0 /\ -r_183^post6+r_183^0 == 0 /\ i_28^0-i_28^post6 == 0 /\ i_98^0-i_98^post6 == 0 /\ -ct_18^post6+y_20^0 <= 0 /\ -r_37^post6+r_37^0 == 0 /\ -ct_18^post6 <= 0 /\ i_187^0-i_187^post6 == 0 /\ -x_17^post6+h_15^post6 <= 0 /\ rv_31^0-rv_31^post6 == 0 /\ 1+a_239^post6-l_143^post6 <= 0 /\ -f_190^post6+f_190^0 == 0 /\ y_20^0-y_20^post6 == 0 /\ r_57^0-r_57^post6 == 0 /\ x_19^post6-h_15^post6 <= 0 /\ a_264^0-a_239^post6 <= 0 /\ -x_21^post6+x_21^0 == 0 /\ ct_18^post6-y_20^0 <= 0 /\ -rt_11^post6+rt_11^0 == 0), cost: 1 7: l7 -> l3 : a_264^0'=a_264^post7, l_27^0'=l_27^post7, i_187^0'=i_187^post7, t_32^0'=t_32^post7, rv_13^0'=rv_13^post7, y_20^0'=y_20^post7, a_158^0'=a_158^post7, x_195^0'=x_195^post7, i_98^0'=i_98^post7, h_15^0'=h_15^post7, r_57^0'=r_57^post7, r_135^0'=r_135^post7, x_140^0'=x_140^post7, st_16^0'=st_16^post7, a_76^0'=a_76^post7, a_239^0'=a_239^post7, x_21^0'=x_21^post7, l_203^0'=l_203^post7, i_115^0'=i_115^post7, rt_11^0'=rt_11^post7, r_37^0'=r_37^post7, a_123^0'=a_123^post7, x_17^0'=x_17^post7, t_24^0'=t_24^post7, f_190^0'=f_190^post7, a_290^0'=a_290^post7, nd_12^0'=nd_12^post7, i_28^0'=i_28^post7, tp_33^0'=tp_33^post7, rv_31^0'=rv_31^post7, a_204^0'=a_204^post7, x_19^0'=x_19^post7, l_143^0'=l_143^post7, h_30^0'=h_30^post7, r_92^0'=r_92^post7, r_183^0'=r_183^post7, x_14^0'=x_14^post7, st_29^0'=st_29^post7, ct_18^0'=ct_18^post7, (0 == 0 /\ -a_290^post7+a_290^0 == 0 /\ -x_19^120+h_15^20 <= 0 /\ x_14^10-h_15^10 <= 0 /\ x_14^10-h_15^10 == 0 /\ -x_17^10+h_15^20 <= 0 /\ -st_16^0+rt_11^post7 == 0 /\ x_140^0-x_140^post7 == 0 /\ -x_19^20+x_17^20 <= 0 /\ -x_19^120+x_21^120 <= 0 /\ -x_19^120+x_21^120 == 0 /\ 1-rv_13^post7 <= 0 /\ -1+rv_13^post7 <= 0 /\ -st_29^10+rt_11^10 == 0 /\ -x_21^120 <= 0 /\ i_187^0-i_187^post7 == 0 /\ h_15^30-x_19^20 <= 0 /\ ct_18^12 <= 0 /\ ct_18^12 == 0 /\ -a_158^post7+a_158^0 == 0 /\ -y_20^120+x_21^120 <= 0 /\ x_17^10-x_19^120 <= 0 /\ ct_18^20 <= 0 /\ -x_14^10 <= 0 /\ x_19^120-h_15^20 <= 0 /\ -x_14^10+h_15^10 <= 0 /\ x_17^10-h_15^20 <= 0 /\ x_17^10-h_15^20 == 0 /\ x_14^10 <= 0 /\ t_24^120-x_21^120 == 0 /\ x_19^20-x_17^20 <= 0 /\ x_19^120-x_21^120 <= 0 /\ r_135^0-r_135^post7 == 0 /\ -y_20^120 <= 0 /\ -a_204^post7+a_204^0 == 0 /\ -h_15^30+x_19^20 <= 0 /\ st_16^0-st_16^post7 == 0 /\ y_20^120-x_21^120 <= 0 /\ -x_17^10+x_19^120 <= 0 /\ -x_17^10+x_19^120 == 0 /\ r_57^0-r_57^post7 == 0 /\ -ct_18^12 <= 0 /\ a_264^0-a_264^post7 == 0 /\ -a_76^post7+a_76^0 == 0 /\ -ct_18^20 <= 0 /\ ct_18^12-y_20^120 <= 0 /\ -x_195^post7+x_195^0 == 0 /\ h_15^30-x_17^20 <= 0 /\ l_27^0-i_28^0 <= 0 /\ x_14^post7 <= 0 /\ h_15^10-rt_11^10 == 0 /\ st_29^10-h_30^0 == 0 /\ h_15^20-x_21^120 <= 0 /\ -h_15^30+t_24^120 <= 0 /\ nd_12^0-nd_12^post7 == 0 /\ -ct_18^20+y_20^120 <= 0 /\ -x_14^post7 <= 0 /\ y_20^120 <= 0 /\ -f_190^post7+f_190^0 == 0 /\ -l_203^post7+l_203^0 == 0 /\ 1-rv_13^20 <= 0 /\ -1+rv_13^20 <= 0 /\ 1-rv_13^10 <= 0 /\ -1+rv_13^10 <= 0 /\ 1-rv_13^30 <= 0 /\ -1+rv_13^30 <= 0 /\ -ct_18^12+y_20^120 <= 0 /\ -ct_18^12+y_20^120 == 0 /\ -l_143^post7+l_143^0 == 0 /\ -i_115^post7+i_115^0 == 0 /\ -h_15^30+x_17^20 <= 0 /\ r_183^0-r_183^post7 == 0 /\ a_239^0-a_239^post7 == 0 /\ r_37^0-r_37^post7 == 0 /\ -h_15^20+x_21^120 <= 0 /\ h_15^30-t_24^120 <= 0 /\ i_98^0-i_98^post7 == 0 /\ -a_123^post7+a_123^0 == 0 /\ r_92^0-r_92^post7 == 0 /\ ct_18^20-y_20^120 <= 0 /\ x_21^120 <= 0), cost: 1 8: l7 -> l8 : a_264^0'=a_264^post8, l_27^0'=l_27^post8, i_187^0'=i_187^post8, t_32^0'=t_32^post8, rv_13^0'=rv_13^post8, y_20^0'=y_20^post8, a_158^0'=a_158^post8, x_195^0'=x_195^post8, i_98^0'=i_98^post8, h_15^0'=h_15^post8, r_57^0'=r_57^post8, r_135^0'=r_135^post8, x_140^0'=x_140^post8, st_16^0'=st_16^post8, a_76^0'=a_76^post8, a_239^0'=a_239^post8, x_21^0'=x_21^post8, l_203^0'=l_203^post8, i_115^0'=i_115^post8, rt_11^0'=rt_11^post8, r_37^0'=r_37^post8, a_123^0'=a_123^post8, x_17^0'=x_17^post8, t_24^0'=t_24^post8, f_190^0'=f_190^post8, a_290^0'=a_290^post8, nd_12^0'=nd_12^post8, i_28^0'=i_28^post8, tp_33^0'=tp_33^post8, rv_31^0'=rv_31^post8, a_204^0'=a_204^post8, x_19^0'=x_19^post8, l_143^0'=l_143^post8, h_30^0'=h_30^post8, r_92^0'=r_92^post8, r_183^0'=r_183^post8, x_14^0'=x_14^post8, st_29^0'=st_29^post8, ct_18^0'=ct_18^post8, (0 == 0 /\ -x_140^post8+x_140^0 == 0 /\ f_190^0-f_190^post8 == 0 /\ h_30^post8-t_32^post8 <= 0 /\ h_30^post8-t_32^post8 == 0 /\ r_135^0-r_135^post8 == 0 /\ -l_143^post8+l_143^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ -r_183^post8+r_183^0 == 0 /\ -1+i_28^10-i_28^0 == 0 /\ -2+i_28^post8 <= 0 /\ a_204^0-a_204^post8 == 0 /\ -h_30^post8+t_32^post8 <= 0 /\ x_195^0-x_195^post8 == 0 /\ r_37^0-r_37^post8 == 0 /\ x_21^0-x_21^post8 == 0 /\ a_264^0-a_264^post8 == 0 /\ a_239^0-a_239^post8 == 0 /\ l_27^0-rv_13^post8 <= 0 /\ -i_115^post8+i_115^0 == 0 /\ a_290^0-a_290^post8 == 0 /\ a_158^0-a_158^post8 == 0 /\ -x_14^post8+x_14^0 == 0 /\ h_30^post8-rv_31^post8 <= 0 /\ a_76^post8-i_28^post8 <= 0 /\ st_16^0-st_16^post8 == 0 /\ 2-l_27^0 <= 0 /\ l_203^0-l_203^post8 == 0 /\ t_24^0-t_24^post8 == 0 /\ -rv_31^post8+t_32^post8 <= 0 /\ l_27^0-l_27^post8 == 0 /\ 2-i_28^post8 <= 0 /\ i_187^0-i_187^post8 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ h_15^0-h_15^post8 == 0 /\ -l_27^0+rv_13^post8 <= 0 /\ -x_17^post8+x_17^0 == 0 /\ -x_19^post8+x_19^0 == 0 /\ 1-l_27^0 <= 0 /\ i_98^0-i_98^post8 == 0 /\ -h_30^post8+rv_31^post8 <= 0 /\ -r_92^post8+r_92^0 == 0 /\ t_32^post8-tp_33^0 == 0 /\ -a_76^post8+i_28^post8 <= 0 /\ -st_29^post8+st_29^0 == 0 /\ -ct_18^post8+ct_18^0 == 0 /\ -y_20^post8+y_20^0 == 0 /\ 1-l_27^0+i_28^0 <= 0 /\ rv_31^post8-t_32^post8 <= 0 /\ -a_123^post8+a_123^0 == 0), cost: 1 15: l8 -> l9 : a_264^0'=a_264^post15, l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, y_20^0'=y_20^post15, a_158^0'=a_158^post15, x_195^0'=x_195^post15, i_98^0'=i_98^post15, h_15^0'=h_15^post15, r_57^0'=r_57^post15, r_135^0'=r_135^post15, x_140^0'=x_140^post15, st_16^0'=st_16^post15, a_76^0'=a_76^post15, a_239^0'=a_239^post15, x_21^0'=x_21^post15, l_203^0'=l_203^post15, i_115^0'=i_115^post15, rt_11^0'=rt_11^post15, r_37^0'=r_37^post15, a_123^0'=a_123^post15, x_17^0'=x_17^post15, t_24^0'=t_24^post15, f_190^0'=f_190^post15, a_290^0'=a_290^post15, nd_12^0'=nd_12^post15, i_28^0'=i_28^post15, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, a_204^0'=a_204^post15, x_19^0'=x_19^post15, l_143^0'=l_143^post15, h_30^0'=h_30^post15, r_92^0'=r_92^post15, r_183^0'=r_183^post15, x_14^0'=x_14^post15, st_29^0'=st_29^post15, ct_18^0'=ct_18^post15, (0 == 0 /\ -a_158^0+i_28^post15 <= 0 /\ 1-rv_13^post15 <= 0 /\ -x_140^post15+x_140^0 == 0 /\ h_15^post15-x_14^post15 <= 0 /\ x_21^0-x_21^post15 == 0 /\ rv_13^post15-i_28^post15 <= 0 /\ -x_19^post15+x_19^0 == 0 /\ -l_203^post15+l_203^0 == 0 /\ a_264^0-a_264^post15 == 0 /\ -l_143^post15+l_143^0 == 0 /\ -a_204^post15+a_204^0 == 0 /\ -r_92^post15+r_92^0 == 0 /\ -f_190^post15+f_190^0 == 0 /\ a_158^0-i_28^post15 <= 0 /\ x_195^0-x_195^post15 == 0 /\ h_15^post15-rt_11^11 == 0 /\ -h_15^post15+x_14^post15 <= 0 /\ -h_15^post15+x_14^post15 == 0 /\ 2-rv_13^post15 <= 0 /\ -i_115^post15+i_115^0 == 0 /\ -l_143^0 <= 0 /\ -x_17^post15+x_17^0 == 0 /\ -r_57^post15+r_57^0 == 0 /\ -y_20^post15+y_20^0 == 0 /\ -ct_18^post15+ct_18^0 == 0 /\ st_29^110-h_30^0 == 0 /\ i_98^0-i_98^post15 == 0 /\ st_16^0-st_16^post15 == 0 /\ -r_135^post15+r_135^0 == 0 /\ a_158^0-a_158^post15 == 0 /\ l_27^0-i_28^0 <= 0 /\ a_239^0-a_239^post15 == 0 /\ -nd_12^post15+nd_12^0 == 0 /\ -i_28^0 <= 0 /\ -r_37^post15+r_37^0 == 0 /\ -r_183^post15+r_183^0 == 0 /\ -st_29^110+rt_11^11 == 0 /\ l_143^0 <= 0 /\ rv_13^post15-i_187^post15 <= 0 /\ a_76^0-a_76^post15 == 0 /\ t_24^0-t_24^post15 == 0 /\ a_290^0-a_290^post15 == 0 /\ a_123^0-a_123^post15 == 0), cost: 1 16: l8 -> l13 : a_264^0'=a_264^post16, l_27^0'=l_27^post16, i_187^0'=i_187^post16, t_32^0'=t_32^post16, rv_13^0'=rv_13^post16, y_20^0'=y_20^post16, a_158^0'=a_158^post16, x_195^0'=x_195^post16, i_98^0'=i_98^post16, h_15^0'=h_15^post16, r_57^0'=r_57^post16, r_135^0'=r_135^post16, x_140^0'=x_140^post16, st_16^0'=st_16^post16, a_76^0'=a_76^post16, a_239^0'=a_239^post16, x_21^0'=x_21^post16, l_203^0'=l_203^post16, i_115^0'=i_115^post16, rt_11^0'=rt_11^post16, r_37^0'=r_37^post16, a_123^0'=a_123^post16, x_17^0'=x_17^post16, t_24^0'=t_24^post16, f_190^0'=f_190^post16, a_290^0'=a_290^post16, nd_12^0'=nd_12^post16, i_28^0'=i_28^post16, tp_33^0'=tp_33^post16, rv_31^0'=rv_31^post16, a_204^0'=a_204^post16, x_19^0'=x_19^post16, l_143^0'=l_143^post16, h_30^0'=h_30^post16, r_92^0'=r_92^post16, r_183^0'=r_183^post16, x_14^0'=x_14^post16, st_29^0'=st_29^post16, ct_18^0'=ct_18^post16, (0 == 0 /\ l_27^0-l_27^post16 == 0 /\ 1+i_98^post16-i_28^post16 <= 0 /\ h_15^0-h_15^post16 == 0 /\ -rv_31^post16+rv_31^0 == 0 /\ t_24^0-t_24^post16 == 0 /\ x_195^0-x_195^post16 == 0 /\ -x_17^post16+x_17^0 == 0 /\ i_187^0-i_187^post16 == 0 /\ r_57^0-r_57^post16 == 0 /\ i_115^0-i_115^post16 == 0 /\ -1-i_28^0+i_28^post16 == 0 /\ -st_29^post16+st_29^0 == 0 /\ r_135^0-r_135^post16 == 0 /\ h_30^post16-t_32^post16 == 0 /\ -ct_18^post16+ct_18^0 == 0 /\ a_239^0-a_239^post16 == 0 /\ -r_183^post16+r_183^0 == 0 /\ -x_19^post16+x_19^0 == 0 /\ -nd_12^post16+nd_12^0 == 0 /\ -x_140^post16+x_140^0 == 0 /\ -a_204^post16+a_204^0 == 0 /\ -st_16^post16+st_16^0 == 0 /\ l_143^0-l_143^post16 == 0 /\ rv_13^0-rv_13^post16 == 0 /\ -1-i_98^post16+i_28^post16 <= 0 /\ -f_190^post16+f_190^0 == 0 /\ -tp_33^0+t_32^post16 == 0 /\ a_264^0-a_264^post16 == 0 /\ -r_37^post16+r_37^0 == 0 /\ 1+i_98^post16-l_27^0 <= 0 /\ x_21^0-x_21^post16 == 0 /\ -x_14^post16+x_14^0 == 0 /\ -i_28^0 <= 0 /\ -l_203^post16+l_203^0 == 0 /\ -a_76^post16+a_76^0 == 0 /\ rt_11^0-rt_11^post16 == 0 /\ a_290^0-a_290^post16 == 0 /\ a_158^0-a_158^post16 == 0 /\ a_123^0-a_123^post16 == 0 /\ y_20^0-y_20^post16 == 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 9: l9 -> l6 : a_264^0'=a_264^post9, l_27^0'=l_27^post9, i_187^0'=i_187^post9, t_32^0'=t_32^post9, rv_13^0'=rv_13^post9, y_20^0'=y_20^post9, a_158^0'=a_158^post9, x_195^0'=x_195^post9, i_98^0'=i_98^post9, h_15^0'=h_15^post9, r_57^0'=r_57^post9, r_135^0'=r_135^post9, x_140^0'=x_140^post9, st_16^0'=st_16^post9, a_76^0'=a_76^post9, a_239^0'=a_239^post9, x_21^0'=x_21^post9, l_203^0'=l_203^post9, i_115^0'=i_115^post9, rt_11^0'=rt_11^post9, r_37^0'=r_37^post9, a_123^0'=a_123^post9, x_17^0'=x_17^post9, t_24^0'=t_24^post9, f_190^0'=f_190^post9, a_290^0'=a_290^post9, nd_12^0'=nd_12^post9, i_28^0'=i_28^post9, tp_33^0'=tp_33^post9, rv_31^0'=rv_31^post9, a_204^0'=a_204^post9, x_19^0'=x_19^post9, l_143^0'=l_143^post9, h_30^0'=h_30^post9, r_92^0'=r_92^post9, r_183^0'=r_183^post9, x_14^0'=x_14^post9, st_29^0'=st_29^post9, ct_18^0'=ct_18^post9, (0 == 0 /\ t_32^0-t_32^post9 == 0 /\ -i_28^post9+i_28^0 == 0 /\ -l_203^post9+l_203^0 == 0 /\ -rv_31^post9+rv_31^0 == 0 /\ y_20^post9 <= 0 /\ x_19^post9-h_15^0 <= 0 /\ -r_183^post9+r_183^0 == 0 /\ t_24^0-t_24^post9 == 0 /\ -st_29^post9+st_29^0 == 0 /\ h_30^0-h_30^post9 == 0 /\ -r_92^post9+r_92^0 == 0 /\ -x_14^0 <= 0 /\ i_115^0-i_115^post9 == 0 /\ r_135^0-r_135^post9 == 0 /\ l_27^0-l_27^post9 == 0 /\ -x_19^post9+h_15^0 <= 0 /\ r_37^0-r_37^post9 == 0 /\ a_239^0-a_239^post9 == 0 /\ a_264^0-a_264^post9 == 0 /\ -l_143^post9+l_143^0 == 0 /\ -x_140^post9+x_140^0 == 0 /\ -x_14^post9+x_14^0 == 0 /\ x_195^0-x_195^post9 == 0 /\ -l_143^0 <= 0 /\ -a_204^post9+a_204^0 == 0 /\ -a_158^0 <= 0 /\ ct_18^post9 <= 0 /\ ct_18^post9 == 0 /\ -f_190^post9+f_190^0 == 0 /\ 2-rv_13^post9 <= 0 /\ i_98^0-i_98^post9 == 0 /\ tp_33^0-tp_33^post9 == 0 /\ -x_19^post9+x_17^post9 <= 0 /\ a_123^0-a_123^post9 == 0 /\ rt_11^0-rt_11^post9 == 0 /\ -h_15^0+x_17^post9 <= 0 /\ -h_15^0+x_17^post9 == 0 /\ i_187^0-i_187^post9 == 0 /\ a_158^0-a_158^post9 == 0 /\ -r_57^post9+r_57^0 == 0 /\ st_16^0-st_16^post9 == 0 /\ -h_15^0+x_21^post9 <= 0 /\ y_20^post9-ct_18^post9 <= 0 /\ y_20^post9-ct_18^post9 == 0 /\ -x_19^post9+x_21^post9 <= 0 /\ -x_19^post9+x_21^post9 == 0 /\ -y_20^post9 <= 0 /\ -a_76^post9+a_76^0 == 0 /\ -ct_18^post9 <= 0 /\ x_19^post9-x_17^post9 <= 0 /\ x_19^post9-x_17^post9 == 0 /\ h_15^0-h_15^post9 == 0 /\ h_15^0-x_17^post9 <= 0 /\ -a_290^post9+a_290^0 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ x_14^0 <= 0 /\ h_15^0-x_21^post9 <= 0 /\ -y_20^post9+ct_18^post9 <= 0 /\ 1-rv_13^post9 <= 0 /\ x_19^post9-x_21^post9 <= 0), cost: 1 10: l9 -> l10 : a_264^0'=a_264^post10, l_27^0'=l_27^post10, i_187^0'=i_187^post10, t_32^0'=t_32^post10, rv_13^0'=rv_13^post10, y_20^0'=y_20^post10, a_158^0'=a_158^post10, x_195^0'=x_195^post10, i_98^0'=i_98^post10, h_15^0'=h_15^post10, r_57^0'=r_57^post10, r_135^0'=r_135^post10, x_140^0'=x_140^post10, st_16^0'=st_16^post10, a_76^0'=a_76^post10, a_239^0'=a_239^post10, x_21^0'=x_21^post10, l_203^0'=l_203^post10, i_115^0'=i_115^post10, rt_11^0'=rt_11^post10, r_37^0'=r_37^post10, a_123^0'=a_123^post10, x_17^0'=x_17^post10, t_24^0'=t_24^post10, f_190^0'=f_190^post10, a_290^0'=a_290^post10, nd_12^0'=nd_12^post10, i_28^0'=i_28^post10, tp_33^0'=tp_33^post10, rv_31^0'=rv_31^post10, a_204^0'=a_204^post10, x_19^0'=x_19^post10, l_143^0'=l_143^post10, h_30^0'=h_30^post10, r_92^0'=r_92^post10, r_183^0'=r_183^post10, x_14^0'=x_14^post10, st_29^0'=st_29^post10, ct_18^0'=ct_18^post10, (0 == 0 /\ -f_190^post10+x_14^0 <= 0 /\ r_57^0-r_57^post10 == 0 /\ 2-rv_13^post10 <= 0 /\ t_32^0-t_32^post10 == 0 /\ tp_33^0-tp_33^post10 == 0 /\ -x_14^post10+x_14^0 == 0 /\ -x_19^post10+x_19^0 == 0 /\ x_21^0-x_21^post10 == 0 /\ r_135^0-r_135^post10 == 0 /\ 1+a_204^post10-a_158^0 <= 0 /\ -h_30^post10+h_30^0 == 0 /\ 1-rv_13^post10 <= 0 /\ a_290^0-a_290^post10 == 0 /\ -i_28^post10+i_28^0 == 0 /\ -st_29^post10+st_29^0 == 0 /\ f_190^post10-x_14^0 <= 0 /\ -x_17^post10+x_17^0 == 0 /\ i_115^0-i_115^post10 == 0 /\ -ct_18^post10+ct_18^0 == 0 /\ -r_92^post10+r_92^0 == 0 /\ l_27^0-l_27^post10 == 0 /\ -l_143^0 <= 0 /\ -a_123^post10+a_123^0 == 0 /\ a_239^0-a_239^post10 == 0 /\ 1+l_143^0-l_203^post10 <= 0 /\ t_24^0-t_24^post10 == 0 /\ -a_76^post10+a_76^0 == 0 /\ -a_158^0 <= 0 /\ -y_20^post10+y_20^0 == 0 /\ -a_204^post10+a_158^post10 <= 0 /\ -i_187^post10+i_187^0 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ -l_143^post10+l_203^post10 <= 0 /\ a_264^0-a_264^post10 == 0 /\ i_98^0-i_98^post10 == 0 /\ -x_140^post10+x_140^0 == 0 /\ -rv_31^post10+rv_31^0 == 0 /\ -1-a_204^post10+a_158^0 <= 0 /\ -r_183^post10+r_183^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ a_204^post10-a_158^post10 <= 0 /\ st_16^0-st_16^post10 == 0 /\ l_143^post10-l_203^post10 <= 0 /\ -1-l_143^0+l_203^post10 <= 0), cost: 1 11: l10 -> l9 : a_264^0'=a_264^post11, l_27^0'=l_27^post11, i_187^0'=i_187^post11, t_32^0'=t_32^post11, rv_13^0'=rv_13^post11, y_20^0'=y_20^post11, a_158^0'=a_158^post11, x_195^0'=x_195^post11, i_98^0'=i_98^post11, h_15^0'=h_15^post11, r_57^0'=r_57^post11, r_135^0'=r_135^post11, x_140^0'=x_140^post11, st_16^0'=st_16^post11, a_76^0'=a_76^post11, a_239^0'=a_239^post11, x_21^0'=x_21^post11, l_203^0'=l_203^post11, i_115^0'=i_115^post11, rt_11^0'=rt_11^post11, r_37^0'=r_37^post11, a_123^0'=a_123^post11, x_17^0'=x_17^post11, t_24^0'=t_24^post11, f_190^0'=f_190^post11, a_290^0'=a_290^post11, nd_12^0'=nd_12^post11, i_28^0'=i_28^post11, tp_33^0'=tp_33^post11, rv_31^0'=rv_31^post11, a_204^0'=a_204^post11, x_19^0'=x_19^post11, l_143^0'=l_143^post11, h_30^0'=h_30^post11, r_92^0'=r_92^post11, r_183^0'=r_183^post11, x_14^0'=x_14^post11, st_29^0'=st_29^post11, ct_18^0'=ct_18^post11, (l_27^0-l_27^post11 == 0 /\ f_190^0-f_190^post11 == 0 /\ -x_17^post11+x_17^0 == 0 /\ r_37^0-r_37^post11 == 0 /\ -nd_12^post11+nd_12^0 == 0 /\ a_239^0-a_239^post11 == 0 /\ x_195^0-x_195^post11 == 0 /\ -h_30^post11+h_30^0 == 0 /\ rv_13^0-rv_13^post11 == 0 /\ -a_123^post11+a_123^0 == 0 /\ r_57^0-r_57^post11 == 0 /\ i_115^0-i_115^post11 == 0 /\ -a_76^post11+a_76^0 == 0 /\ y_20^0-y_20^post11 == 0 /\ x_21^0-x_21^post11 == 0 /\ t_24^0-t_24^post11 == 0 /\ -l_143^post11+l_143^0 == 0 /\ -x_140^post11+x_140^0 == 0 /\ r_135^0-r_135^post11 == 0 /\ st_16^0-st_16^post11 == 0 /\ -r_183^post11+r_183^0 == 0 /\ -i_28^post11+i_28^0 == 0 /\ -rv_31^post11+rv_31^0 == 0 /\ a_264^0-a_264^post11 == 0 /\ -x_14^post11+x_14^0 == 0 /\ l_203^0-l_203^post11 == 0 /\ h_15^0-h_15^post11 == 0 /\ -a_204^post11+a_204^0 == 0 /\ -st_29^post11+st_29^0 == 0 /\ -r_92^post11+r_92^0 == 0 /\ i_187^0-i_187^post11 == 0 /\ -i_98^post11+i_98^0 == 0 /\ a_290^0-a_290^post11 == 0 /\ -ct_18^post11+ct_18^0 == 0 /\ rt_11^0-rt_11^post11 == 0 /\ tp_33^0-tp_33^post11 == 0 /\ a_158^0-a_158^post11 == 0 /\ -x_19^post11+x_19^0 == 0 /\ t_32^0-t_32^post11 == 0), cost: 1 12: l11 -> l6 : a_264^0'=a_264^post12, l_27^0'=l_27^post12, i_187^0'=i_187^post12, t_32^0'=t_32^post12, rv_13^0'=rv_13^post12, y_20^0'=y_20^post12, a_158^0'=a_158^post12, x_195^0'=x_195^post12, i_98^0'=i_98^post12, h_15^0'=h_15^post12, r_57^0'=r_57^post12, r_135^0'=r_135^post12, x_140^0'=x_140^post12, st_16^0'=st_16^post12, a_76^0'=a_76^post12, a_239^0'=a_239^post12, x_21^0'=x_21^post12, l_203^0'=l_203^post12, i_115^0'=i_115^post12, rt_11^0'=rt_11^post12, r_37^0'=r_37^post12, a_123^0'=a_123^post12, x_17^0'=x_17^post12, t_24^0'=t_24^post12, f_190^0'=f_190^post12, a_290^0'=a_290^post12, nd_12^0'=nd_12^post12, i_28^0'=i_28^post12, tp_33^0'=tp_33^post12, rv_31^0'=rv_31^post12, a_204^0'=a_204^post12, x_19^0'=x_19^post12, l_143^0'=l_143^post12, h_30^0'=h_30^post12, r_92^0'=r_92^post12, r_183^0'=r_183^post12, x_14^0'=x_14^post12, st_29^0'=st_29^post12, ct_18^0'=ct_18^post12, (0 == 0 /\ -st_29^post12+st_29^0 == 0 /\ x_195^0-x_195^post12 == 0 /\ x_19^post12-x_21^post12 <= 0 /\ h_15^0-x_21^post12 <= 0 /\ -x_17^post12+x_19^post12 <= 0 /\ -x_17^post12+x_19^post12 == 0 /\ r_57^0-r_57^post12 == 0 /\ -a_204^post12+a_204^0 == 0 /\ -nd_12^post12+nd_12^0 == 0 /\ l_27^0-l_27^post12 == 0 /\ -x_14^0 <= 0 /\ y_20^post12 <= 0 /\ i_28^0-i_28^post12 == 0 /\ st_16^0-st_16^post12 == 0 /\ -ct_18^post12 <= 0 /\ i_187^0-i_187^post12 == 0 /\ -x_19^post12+x_21^post12 <= 0 /\ -x_19^post12+x_21^post12 == 0 /\ -r_92^post12+r_92^0 == 0 /\ -h_15^0+x_21^post12 <= 0 /\ 1-l_143^0 <= 0 /\ -1+l_143^0 <= 0 /\ x_17^post12-x_19^post12 <= 0 /\ i_115^0-i_115^post12 == 0 /\ h_15^0-h_15^post12 == 0 /\ r_135^0-r_135^post12 == 0 /\ -h_30^post12+h_30^0 == 0 /\ a_239^0-a_239^post12 == 0 /\ -a_76^post12+a_76^0 == 0 /\ t_24^0-t_24^post12 == 0 /\ -y_20^post12+ct_18^post12 <= 0 /\ a_123^0 <= 0 /\ h_15^0-x_19^post12 <= 0 /\ 2-rv_13^post12 <= 0 /\ -x_140^post12+x_140^0 == 0 /\ a_290^0-a_290^post12 == 0 /\ x_14^0-x_14^post12 == 0 /\ rt_11^0-rt_11^post12 == 0 /\ -r_183^post12+r_183^0 == 0 /\ -y_20^post12 <= 0 /\ i_98^0-i_98^post12 == 0 /\ -h_15^0+x_17^post12 <= 0 /\ -h_15^0+x_17^post12 == 0 /\ tp_33^0-tp_33^post12 == 0 /\ l_203^0-l_203^post12 == 0 /\ -a_123^0 <= 0 /\ y_20^post12-ct_18^post12 <= 0 /\ y_20^post12-ct_18^post12 == 0 /\ -r_37^post12+r_37^0 == 0 /\ ct_18^post12 <= 0 /\ ct_18^post12 == 0 /\ -f_190^post12+f_190^0 == 0 /\ -rv_31^post12+rv_31^0 == 0 /\ t_32^0-t_32^post12 == 0 /\ -h_15^0+x_19^post12 <= 0 /\ -l_143^post12+l_143^0 == 0 /\ 1-rv_13^post12 <= 0 /\ a_264^0-a_264^post12 == 0 /\ x_14^0 <= 0 /\ a_158^0-a_158^post12 == 0 /\ h_15^0-x_17^post12 <= 0 /\ a_123^0-a_123^post12 == 0), cost: 1 13: l11 -> l9 : a_264^0'=a_264^post13, l_27^0'=l_27^post13, i_187^0'=i_187^post13, t_32^0'=t_32^post13, rv_13^0'=rv_13^post13, y_20^0'=y_20^post13, a_158^0'=a_158^post13, x_195^0'=x_195^post13, i_98^0'=i_98^post13, h_15^0'=h_15^post13, r_57^0'=r_57^post13, r_135^0'=r_135^post13, x_140^0'=x_140^post13, st_16^0'=st_16^post13, a_76^0'=a_76^post13, a_239^0'=a_239^post13, x_21^0'=x_21^post13, l_203^0'=l_203^post13, i_115^0'=i_115^post13, rt_11^0'=rt_11^post13, r_37^0'=r_37^post13, a_123^0'=a_123^post13, x_17^0'=x_17^post13, t_24^0'=t_24^post13, f_190^0'=f_190^post13, a_290^0'=a_290^post13, nd_12^0'=nd_12^post13, i_28^0'=i_28^post13, tp_33^0'=tp_33^post13, rv_31^0'=rv_31^post13, a_204^0'=a_204^post13, x_19^0'=x_19^post13, l_143^0'=l_143^post13, h_30^0'=h_30^post13, r_92^0'=r_92^post13, r_183^0'=r_183^post13, x_14^0'=x_14^post13, st_29^0'=st_29^post13, ct_18^0'=ct_18^post13, (0 == 0 /\ -x_14^post13+x_14^0 == 0 /\ -x_21^post13+x_21^0 == 0 /\ -a_76^post13+a_76^0 == 0 /\ t_24^0-t_24^post13 == 0 /\ st_16^0-st_16^post13 == 0 /\ a_123^0-a_123^post13 == 0 /\ i_115^0-i_115^post13 == 0 /\ -rv_31^post13+rv_31^0 == 0 /\ r_57^0-r_57^post13 == 0 /\ -ct_18^post13+ct_18^0 == 0 /\ -r_37^post13+r_37^0 == 0 /\ i_187^0-i_187^post13 == 0 /\ -x_19^post13+x_19^0 == 0 /\ -l_143^post13+l_143^0 == 0 /\ y_20^0-y_20^post13 == 0 /\ -a_290^post13+a_290^0 == 0 /\ t_32^0-t_32^post13 == 0 /\ -a_158^post13+a_158^0 == 0 /\ -f_190^post13+f_190^0 == 0 /\ 2-rv_13^post13 <= 0 /\ -a_123^0 <= 0 /\ -nd_12^post13+nd_12^0 == 0 /\ -tp_33^post13+tp_33^0 == 0 /\ a_239^0-a_239^post13 == 0 /\ r_183^0-r_183^post13 == 0 /\ a_264^0-a_264^post13 == 0 /\ l_27^0-l_27^post13 == 0 /\ 1-rv_13^post13 <= 0 /\ -h_30^post13+h_30^0 == 0 /\ -i_98^post13+i_98^0 == 0 /\ -st_29^post13+st_29^0 == 0 /\ x_195^0-x_195^post13 == 0 /\ -x_17^post13+x_17^0 == 0 /\ -l_203^post13+l_203^0 == 0 /\ i_28^0-i_28^post13 == 0 /\ -r_92^post13+r_92^0 == 0 /\ -a_204^post13+a_204^0 == 0 /\ rt_11^0-rt_11^post13 == 0), cost: 1 14: l12 -> l9 : a_264^0'=a_264^post14, l_27^0'=l_27^post14, i_187^0'=i_187^post14, t_32^0'=t_32^post14, rv_13^0'=rv_13^post14, y_20^0'=y_20^post14, a_158^0'=a_158^post14, x_195^0'=x_195^post14, i_98^0'=i_98^post14, h_15^0'=h_15^post14, r_57^0'=r_57^post14, r_135^0'=r_135^post14, x_140^0'=x_140^post14, st_16^0'=st_16^post14, a_76^0'=a_76^post14, a_239^0'=a_239^post14, x_21^0'=x_21^post14, l_203^0'=l_203^post14, i_115^0'=i_115^post14, rt_11^0'=rt_11^post14, r_37^0'=r_37^post14, a_123^0'=a_123^post14, x_17^0'=x_17^post14, t_24^0'=t_24^post14, f_190^0'=f_190^post14, a_290^0'=a_290^post14, nd_12^0'=nd_12^post14, i_28^0'=i_28^post14, tp_33^0'=tp_33^post14, rv_31^0'=rv_31^post14, a_204^0'=a_204^post14, x_19^0'=x_19^post14, l_143^0'=l_143^post14, h_30^0'=h_30^post14, r_92^0'=r_92^post14, r_183^0'=r_183^post14, x_14^0'=x_14^post14, st_29^0'=st_29^post14, ct_18^0'=ct_18^post14, (0 == 0 /\ -a_204^post14+a_204^0 == 0 /\ 2-rv_13^post14 <= 0 /\ -a_158^post14+a_158^0 == 0 /\ i_28^0-i_28^post14 == 0 /\ -a_158^0+a_123^post14 <= 0 /\ rt_11^0-rt_11^post14 == 0 /\ -1-a_123^post14+i_115^post14 <= 0 /\ x_140^0-x_140^post14 == 0 /\ t_32^0-t_32^post14 == 0 /\ -nd_12^post14+nd_12^0 == 0 /\ -x_17^post14+x_17^0 == 0 /\ st_16^0-st_16^post14 == 0 /\ -x_19^post14+x_19^0 == 0 /\ 1-l_143^0 <= 0 /\ -1+l_143^0 <= 0 /\ a_158^0-a_123^post14 <= 0 /\ -r_92^post14+r_92^0 == 0 /\ -h_30^post14+h_30^0 == 0 /\ -st_29^post14+st_29^0 == 0 /\ 1-rv_13^post14 <= 0 /\ -ct_18^post14+ct_18^0 == 0 /\ -a_76^post14+a_76^0 == 0 /\ -i_98^post14+i_98^0 == 0 /\ x_195^0-x_195^post14 == 0 /\ r_57^0-r_57^post14 == 0 /\ -t_24^post14+t_24^0 == 0 /\ tp_33^0-tp_33^post14 == 0 /\ 1+a_123^post14-i_115^post14 <= 0 /\ -i_115^10+rv_13^post14 <= 0 /\ -i_28^0 <= 0 /\ y_20^0-y_20^post14 == 0 /\ -l_203^post14+l_203^0 == 0 /\ x_21^0-x_21^post14 == 0 /\ -f_190^post14+f_190^0 == 0 /\ -rv_31^post14+rv_31^0 == 0 /\ a_290^0-a_290^post14 == 0 /\ -x_14^post14+x_14^0 == 0 /\ -i_187^post14+i_187^0 == 0 /\ l_27^0-l_27^post14 == 0 /\ r_135^0-r_135^post14 == 0 /\ a_239^0-a_239^post14 == 0 /\ -l_143^post14+l_143^0 == 0 /\ a_264^0-a_264^post14 == 0), cost: 1 17: l13 -> l8 : a_264^0'=a_264^post17, l_27^0'=l_27^post17, i_187^0'=i_187^post17, t_32^0'=t_32^post17, rv_13^0'=rv_13^post17, y_20^0'=y_20^post17, a_158^0'=a_158^post17, x_195^0'=x_195^post17, i_98^0'=i_98^post17, h_15^0'=h_15^post17, r_57^0'=r_57^post17, r_135^0'=r_135^post17, x_140^0'=x_140^post17, st_16^0'=st_16^post17, a_76^0'=a_76^post17, a_239^0'=a_239^post17, x_21^0'=x_21^post17, l_203^0'=l_203^post17, i_115^0'=i_115^post17, rt_11^0'=rt_11^post17, r_37^0'=r_37^post17, a_123^0'=a_123^post17, x_17^0'=x_17^post17, t_24^0'=t_24^post17, f_190^0'=f_190^post17, a_290^0'=a_290^post17, nd_12^0'=nd_12^post17, i_28^0'=i_28^post17, tp_33^0'=tp_33^post17, rv_31^0'=rv_31^post17, a_204^0'=a_204^post17, x_19^0'=x_19^post17, l_143^0'=l_143^post17, h_30^0'=h_30^post17, r_92^0'=r_92^post17, r_183^0'=r_183^post17, x_14^0'=x_14^post17, st_29^0'=st_29^post17, ct_18^0'=ct_18^post17, (-h_30^post17+h_30^0 == 0 /\ -ct_18^post17+ct_18^0 == 0 /\ -nd_12^post17+nd_12^0 == 0 /\ l_27^0-l_27^post17 == 0 /\ st_16^0-st_16^post17 == 0 /\ i_187^0-i_187^post17 == 0 /\ -l_143^post17+l_143^0 == 0 /\ -r_37^post17+r_37^0 == 0 /\ -x_140^post17+x_140^0 == 0 /\ r_57^0-r_57^post17 == 0 /\ i_115^0-i_115^post17 == 0 /\ h_15^0-h_15^post17 == 0 /\ -a_76^post17+a_76^0 == 0 /\ y_20^0-y_20^post17 == 0 /\ -st_29^post17+st_29^0 == 0 /\ -tp_33^post17+tp_33^0 == 0 /\ a_290^0-a_290^post17 == 0 /\ x_14^0-x_14^post17 == 0 /\ rv_13^0-rv_13^post17 == 0 /\ -x_19^post17+x_19^0 == 0 /\ -r_183^post17+r_183^0 == 0 /\ -a_204^post17+a_204^0 == 0 /\ -r_92^post17+r_92^0 == 0 /\ x_195^0-x_195^post17 == 0 /\ a_123^0-a_123^post17 == 0 /\ -t_24^post17+t_24^0 == 0 /\ a_158^0-a_158^post17 == 0 /\ t_32^0-t_32^post17 == 0 /\ x_21^0-x_21^post17 == 0 /\ r_135^0-r_135^post17 == 0 /\ -i_98^post17+i_98^0 == 0 /\ -f_190^post17+f_190^0 == 0 /\ rt_11^0-rt_11^post17 == 0 /\ -x_17^post17+x_17^0 == 0 /\ a_239^0-a_239^post17 == 0 /\ -rv_31^post17+rv_31^0 == 0 /\ a_264^0-a_264^post17 == 0 /\ -l_203^post17+l_203^0 == 0 /\ i_28^0-i_28^post17 == 0), cost: 1 20: l14 -> l0 : a_264^0'=a_264^post20, l_27^0'=l_27^post20, i_187^0'=i_187^post20, t_32^0'=t_32^post20, rv_13^0'=rv_13^post20, y_20^0'=y_20^post20, a_158^0'=a_158^post20, x_195^0'=x_195^post20, i_98^0'=i_98^post20, h_15^0'=h_15^post20, r_57^0'=r_57^post20, r_135^0'=r_135^post20, x_140^0'=x_140^post20, st_16^0'=st_16^post20, a_76^0'=a_76^post20, a_239^0'=a_239^post20, x_21^0'=x_21^post20, l_203^0'=l_203^post20, i_115^0'=i_115^post20, rt_11^0'=rt_11^post20, r_37^0'=r_37^post20, a_123^0'=a_123^post20, x_17^0'=x_17^post20, t_24^0'=t_24^post20, f_190^0'=f_190^post20, a_290^0'=a_290^post20, nd_12^0'=nd_12^post20, i_28^0'=i_28^post20, tp_33^0'=tp_33^post20, rv_31^0'=rv_31^post20, a_204^0'=a_204^post20, x_19^0'=x_19^post20, l_143^0'=l_143^post20, h_30^0'=h_30^post20, r_92^0'=r_92^post20, r_183^0'=r_183^post20, x_14^0'=x_14^post20, st_29^0'=st_29^post20, ct_18^0'=ct_18^post20, (a_204^0-a_204^post20 == 0 /\ -nd_12^post20+nd_12^0 == 0 /\ -st_29^post20+st_29^0 == 0 /\ l_27^0-l_27^post20 == 0 /\ r_57^0-r_57^post20 == 0 /\ -ct_18^post20+ct_18^0 == 0 /\ rv_13^0-rv_13^post20 == 0 /\ x_195^0-x_195^post20 == 0 /\ a_76^0-a_76^post20 == 0 /\ a_123^0-a_123^post20 == 0 /\ i_98^0-i_98^post20 == 0 /\ -st_16^post20+st_16^0 == 0 /\ x_17^0-x_17^post20 == 0 /\ x_19^0-x_19^post20 == 0 /\ -r_37^post20+r_37^0 == 0 /\ i_187^0-i_187^post20 == 0 /\ -rt_11^post20+rt_11^0 == 0 /\ y_20^0-y_20^post20 == 0 /\ r_135^0-r_135^post20 == 0 /\ x_140^0-x_140^post20 == 0 /\ h_15^0-h_15^post20 == 0 /\ -h_30^post20+h_30^0 == 0 /\ -r_183^post20+r_183^0 == 0 /\ i_115^0-i_115^post20 == 0 /\ -a_239^post20+a_239^0 == 0 /\ -tp_33^post20+tp_33^0 == 0 /\ a_264^0-a_264^post20 == 0 /\ l_203^0-l_203^post20 == 0 /\ -t_32^post20+t_32^0 == 0 /\ -r_92^post20+r_92^0 == 0 /\ a_158^0-a_158^post20 == 0 /\ -x_21^post20+x_21^0 == 0 /\ -t_24^post20+t_24^0 == 0 /\ -a_290^post20+a_290^0 == 0 /\ rv_31^0-rv_31^post20 == 0 /\ -x_14^post20+x_14^0 == 0 /\ -f_190^post20+f_190^0 == 0 /\ -i_28^post20+i_28^0 == 0 /\ -l_143^post20+l_143^0 == 0), cost: 1 Removed unreachable rules and leafs Start location: l14 0: l0 -> l1 : a_264^0'=a_264^post0, l_27^0'=l_27^post0, i_187^0'=i_187^post0, t_32^0'=t_32^post0, rv_13^0'=rv_13^post0, y_20^0'=y_20^post0, a_158^0'=a_158^post0, x_195^0'=x_195^post0, i_98^0'=i_98^post0, h_15^0'=h_15^post0, r_57^0'=r_57^post0, r_135^0'=r_135^post0, x_140^0'=x_140^post0, st_16^0'=st_16^post0, a_76^0'=a_76^post0, a_239^0'=a_239^post0, x_21^0'=x_21^post0, l_203^0'=l_203^post0, i_115^0'=i_115^post0, rt_11^0'=rt_11^post0, r_37^0'=r_37^post0, a_123^0'=a_123^post0, x_17^0'=x_17^post0, t_24^0'=t_24^post0, f_190^0'=f_190^post0, a_290^0'=a_290^post0, nd_12^0'=nd_12^post0, i_28^0'=i_28^post0, tp_33^0'=tp_33^post0, rv_31^0'=rv_31^post0, a_204^0'=a_204^post0, x_19^0'=x_19^post0, l_143^0'=l_143^post0, h_30^0'=h_30^post0, r_92^0'=r_92^post0, r_183^0'=r_183^post0, x_14^0'=x_14^post0, st_29^0'=st_29^post0, ct_18^0'=ct_18^post0, (0 == 0 /\ -f_190^post0+f_190^0 == 0 /\ -a_204^post0+a_204^0 == 0 /\ -a_290^post0+a_290^0 == 0 /\ h_15^0-h_15^post0 == 0 /\ l_143^0-l_143^post0 == 0 /\ a_264^0-a_264^post0 == 0 /\ a_76^0-a_76^post0 == 0 /\ l_203^0-l_203^post0 == 0 /\ t_32^0-t_32^post0 == 0 /\ rv_13^post0-nd_12^10 == 0 /\ -st_16^post0+st_16^0 == 0 /\ -x_19^post0+x_19^0 == 0 /\ -h_30^post0 <= 0 /\ -tp_33^post0+tp_33^0 == 0 /\ i_28^post0 <= 0 /\ i_28^post0 == 0 /\ -a_239^post0+a_239^0 == 0 /\ -r_92^post0+r_92^0 == 0 /\ -st_29^post0+st_29^0 == 0 /\ -i_28^post0 <= 0 /\ r_135^0-r_135^post0 == 0 /\ -ct_18^post0+ct_18^0 == 0 /\ -a_123^post0+a_123^0 == 0 /\ i_115^0-i_115^post0 == 0 /\ -rv_13^post0+l_27^post0 <= 0 /\ -rv_13^post0+l_27^post0 == 0 /\ -r_183^post0+r_183^0 == 0 /\ a_158^0-a_158^post0 == 0 /\ x_140^0-x_140^post0 == 0 /\ -x_21^post0+x_21^0 == 0 /\ x_195^0-x_195^post0 == 0 /\ r_37^0-r_37^post0 == 0 /\ rv_13^post0-l_27^post0 <= 0 /\ h_30^post0 <= 0 /\ h_30^post0 == 0 /\ i_98^0-i_98^post0 == 0 /\ -x_17^post0+x_17^0 == 0 /\ -rt_11^post0+rt_11^0 == 0 /\ i_187^0-i_187^post0 == 0 /\ -t_24^post0+t_24^0 == 0 /\ -x_14^post0+x_14^0 == 0 /\ rv_31^0-rv_31^post0 == 0 /\ r_57^0-r_57^post0 == 0 /\ y_20^0-y_20^post0 == 0), cost: 1 19: l1 -> l7 : a_264^0'=a_264^post19, l_27^0'=l_27^post19, i_187^0'=i_187^post19, t_32^0'=t_32^post19, rv_13^0'=rv_13^post19, y_20^0'=y_20^post19, a_158^0'=a_158^post19, x_195^0'=x_195^post19, i_98^0'=i_98^post19, h_15^0'=h_15^post19, r_57^0'=r_57^post19, r_135^0'=r_135^post19, x_140^0'=x_140^post19, st_16^0'=st_16^post19, a_76^0'=a_76^post19, a_239^0'=a_239^post19, x_21^0'=x_21^post19, l_203^0'=l_203^post19, i_115^0'=i_115^post19, rt_11^0'=rt_11^post19, r_37^0'=r_37^post19, a_123^0'=a_123^post19, x_17^0'=x_17^post19, t_24^0'=t_24^post19, f_190^0'=f_190^post19, a_290^0'=a_290^post19, nd_12^0'=nd_12^post19, i_28^0'=i_28^post19, tp_33^0'=tp_33^post19, rv_31^0'=rv_31^post19, a_204^0'=a_204^post19, x_19^0'=x_19^post19, l_143^0'=l_143^post19, h_30^0'=h_30^post19, r_92^0'=r_92^post19, r_183^0'=r_183^post19, x_14^0'=x_14^post19, st_29^0'=st_29^post19, ct_18^0'=ct_18^post19, (0 == 0 /\ -rv_31^post19+t_32^post19 <= 0 /\ -x_21^post19+x_21^0 == 0 /\ -x_14^post19+x_14^0 == 0 /\ r_57^0-r_57^post19 == 0 /\ -i_115^post19+i_115^0 == 0 /\ y_20^0-y_20^post19 == 0 /\ -x_195^post19+x_195^0 == 0 /\ l_143^0-l_143^post19 == 0 /\ -h_30^post19+t_32^post19 <= 0 /\ -1+i_28^post19-i_28^0 == 0 /\ h_30^post19-rv_31^post19 <= 0 /\ -a_290^post19+a_290^0 == 0 /\ -l_27^0+rv_13^post19 <= 0 /\ rv_31^post19-t_32^post19 <= 0 /\ a_76^0-a_76^post19 == 0 /\ -a_239^post19+a_239^0 == 0 /\ -st_29^post19+st_29^0 == 0 /\ -ct_18^post19+ct_18^0 == 0 /\ a_123^0-a_123^post19 == 0 /\ r_135^0-r_135^post19 == 0 /\ h_30^post19-t_32^post19 <= 0 /\ h_30^post19-t_32^post19 == 0 /\ -nd_12^post19+nd_12^0 == 0 /\ -h_30^post19+rv_31^post19 <= 0 /\ -st_16^post19+st_16^0 == 0 /\ -x_19^post19+x_19^0 == 0 /\ l_27^0-l_27^post19 == 0 /\ l_27^0-rv_13^post19 <= 0 /\ a_264^0-a_264^post19 == 0 /\ -r_92^post19+r_92^0 == 0 /\ -t_24^post19+t_24^0 == 0 /\ h_15^0-h_15^post19 == 0 /\ -r_37^post19+r_37^0 == 0 /\ i_98^0-i_98^post19 == 0 /\ x_17^0-x_17^post19 == 0 /\ x_140^0-x_140^post19 == 0 /\ -rt_11^post19+rt_11^0 == 0 /\ -f_190^post19+f_190^0 == 0 /\ -l_203^post19+l_203^0 == 0 /\ -tp_33^0+t_32^post19 == 0 /\ -r_183^post19+r_183^0 == 0 /\ 1-l_27^0 <= 0 /\ a_158^0-a_158^post19 == 0 /\ i_187^0-i_187^post19 == 0 /\ 1-i_28^post19 <= 0 /\ -1+i_28^post19 <= 0 /\ 1-l_27^0+i_28^0 <= 0 /\ -a_204^post19+a_204^0 == 0), cost: 1 2: l2 -> l4 : a_264^0'=a_264^post2, l_27^0'=l_27^post2, i_187^0'=i_187^post2, t_32^0'=t_32^post2, rv_13^0'=rv_13^post2, y_20^0'=y_20^post2, a_158^0'=a_158^post2, x_195^0'=x_195^post2, i_98^0'=i_98^post2, h_15^0'=h_15^post2, r_57^0'=r_57^post2, r_135^0'=r_135^post2, x_140^0'=x_140^post2, st_16^0'=st_16^post2, a_76^0'=a_76^post2, a_239^0'=a_239^post2, x_21^0'=x_21^post2, l_203^0'=l_203^post2, i_115^0'=i_115^post2, rt_11^0'=rt_11^post2, r_37^0'=r_37^post2, a_123^0'=a_123^post2, x_17^0'=x_17^post2, t_24^0'=t_24^post2, f_190^0'=f_190^post2, a_290^0'=a_290^post2, nd_12^0'=nd_12^post2, i_28^0'=i_28^post2, tp_33^0'=tp_33^post2, rv_31^0'=rv_31^post2, a_204^0'=a_204^post2, x_19^0'=x_19^post2, l_143^0'=l_143^post2, h_30^0'=h_30^post2, r_92^0'=r_92^post2, r_183^0'=r_183^post2, x_14^0'=x_14^post2, st_29^0'=st_29^post2, ct_18^0'=ct_18^post2, (0 == 0 /\ -y_20^0+ct_18^post2 <= 0 /\ -a_239^post2+a_239^0 == 0 /\ -1+a_264^0-a_290^post2 <= 0 /\ t_32^0-t_32^post2 == 0 /\ r_57^0-r_57^post2 == 0 /\ 1-rv_13^post2 <= 0 /\ y_20^0 <= 0 /\ -x_195^post2+x_195^0 == 0 /\ y_20^0-y_20^post2 == 0 /\ ct_18^post2 <= 0 /\ -a_290^post2+a_264^post2 <= 0 /\ x_19^post2-x_17^post2 <= 0 /\ -r_183^post2+r_183^0 == 0 /\ x_19^post2-h_15^post2 <= 0 /\ -r_92^post2+r_92^0 == 0 /\ y_20^0-ct_18^post2 <= 0 /\ -x_21^post2+x_21^0 == 0 /\ x_140^0-x_140^post2 == 0 /\ 2-rv_13^post2 <= 0 /\ x_14^post2 <= 0 /\ -l_143^post2+l_143^0 == 0 /\ -i_115^post2+i_115^0 == 0 /\ -i_28^post2+i_28^0 == 0 /\ l_203^0-l_203^post2 == 0 /\ -x_14^post2 <= 0 /\ l_27^0-l_27^post2 == 0 /\ a_290^post2-a_264^post2 <= 0 /\ -x_19^post2+x_17^post2 <= 0 /\ a_76^0-a_76^post2 == 0 /\ -r_135^post2+r_135^0 == 0 /\ -x_19^post2+h_15^post2 <= 0 /\ -rt_11^post2+rt_11^0 == 0 /\ -x_17^post2+h_15^post2 <= 0 /\ -ct_18^post2 <= 0 /\ i_187^0-i_187^post2 == 0 /\ 1-a_264^0+a_290^post2 <= 0 /\ -y_20^0 <= 0 /\ rv_31^0-rv_31^post2 == 0 /\ -nd_12^post2+nd_12^0 == 0 /\ -a_204^post2+a_204^0 == 0 /\ -a_123^post2+a_123^0 == 0 /\ -st_16^post2+st_16^0 == 0 /\ i_98^0-i_98^post2 == 0 /\ f_190^0-f_190^post2 == 0 /\ x_17^post2-h_15^post2 <= 0 /\ a_158^0-a_158^post2 == 0 /\ -a_264^0 <= 0 /\ -tp_33^post2+tp_33^0 == 0 /\ -h_30^post2+h_30^0 == 0 /\ t_24^post2-x_21^0 == 0 /\ -st_29^post2+st_29^0 == 0), cost: 1 3: l4 -> l2 : a_264^0'=a_264^post3, l_27^0'=l_27^post3, i_187^0'=i_187^post3, t_32^0'=t_32^post3, rv_13^0'=rv_13^post3, y_20^0'=y_20^post3, a_158^0'=a_158^post3, x_195^0'=x_195^post3, i_98^0'=i_98^post3, h_15^0'=h_15^post3, r_57^0'=r_57^post3, r_135^0'=r_135^post3, x_140^0'=x_140^post3, st_16^0'=st_16^post3, a_76^0'=a_76^post3, a_239^0'=a_239^post3, x_21^0'=x_21^post3, l_203^0'=l_203^post3, i_115^0'=i_115^post3, rt_11^0'=rt_11^post3, r_37^0'=r_37^post3, a_123^0'=a_123^post3, x_17^0'=x_17^post3, t_24^0'=t_24^post3, f_190^0'=f_190^post3, a_290^0'=a_290^post3, nd_12^0'=nd_12^post3, i_28^0'=i_28^post3, tp_33^0'=tp_33^post3, rv_31^0'=rv_31^post3, a_204^0'=a_204^post3, x_19^0'=x_19^post3, l_143^0'=l_143^post3, h_30^0'=h_30^post3, r_92^0'=r_92^post3, r_183^0'=r_183^post3, x_14^0'=x_14^post3, st_29^0'=st_29^post3, ct_18^0'=ct_18^post3, (-r_92^post3+r_92^0 == 0 /\ -l_143^post3+l_143^0 == 0 /\ -r_135^post3+r_135^0 == 0 /\ rv_13^0-rv_13^post3 == 0 /\ -r_37^post3+r_37^0 == 0 /\ a_158^0-a_158^post3 == 0 /\ -i_28^post3+i_28^0 == 0 /\ st_16^0-st_16^post3 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ -t_24^post3+t_24^0 == 0 /\ l_27^0-l_27^post3 == 0 /\ r_57^0-r_57^post3 == 0 /\ l_203^0-l_203^post3 == 0 /\ -r_183^post3+r_183^0 == 0 /\ y_20^0-y_20^post3 == 0 /\ i_98^0-i_98^post3 == 0 /\ x_17^0-x_17^post3 == 0 /\ x_19^0-x_19^post3 == 0 /\ x_140^0-x_140^post3 == 0 /\ -a_204^post3+a_204^0 == 0 /\ h_15^0-h_15^post3 == 0 /\ -x_14^post3+x_14^0 == 0 /\ a_76^0-a_76^post3 == 0 /\ -x_21^post3+x_21^0 == 0 /\ -i_115^post3+i_115^0 == 0 /\ f_190^0-f_190^post3 == 0 /\ st_29^0-st_29^post3 == 0 /\ -a_123^post3+a_123^0 == 0 /\ i_187^0-i_187^post3 == 0 /\ -rv_31^post3+rv_31^0 == 0 /\ -a_290^post3+a_290^0 == 0 /\ -a_239^post3+a_239^0 == 0 /\ -h_30^post3+h_30^0 == 0 /\ -tp_33^post3+tp_33^0 == 0 /\ x_195^0-x_195^post3 == 0 /\ -ct_18^post3+ct_18^0 == 0 /\ -t_32^post3+t_32^0 == 0 /\ -nd_12^post3+nd_12^0 == 0 /\ a_264^0-a_264^post3 == 0), cost: 1 6: l6 -> l2 : a_264^0'=a_264^post6, l_27^0'=l_27^post6, i_187^0'=i_187^post6, t_32^0'=t_32^post6, rv_13^0'=rv_13^post6, y_20^0'=y_20^post6, a_158^0'=a_158^post6, x_195^0'=x_195^post6, i_98^0'=i_98^post6, h_15^0'=h_15^post6, r_57^0'=r_57^post6, r_135^0'=r_135^post6, x_140^0'=x_140^post6, st_16^0'=st_16^post6, a_76^0'=a_76^post6, a_239^0'=a_239^post6, x_21^0'=x_21^post6, l_203^0'=l_203^post6, i_115^0'=i_115^post6, rt_11^0'=rt_11^post6, r_37^0'=r_37^post6, a_123^0'=a_123^post6, x_17^0'=x_17^post6, t_24^0'=t_24^post6, f_190^0'=f_190^post6, a_290^0'=a_290^post6, nd_12^0'=nd_12^post6, i_28^0'=i_28^post6, tp_33^0'=tp_33^post6, rv_31^0'=rv_31^post6, a_204^0'=a_204^post6, x_19^0'=x_19^post6, l_143^0'=l_143^post6, h_30^0'=h_30^post6, r_92^0'=r_92^post6, r_183^0'=r_183^post6, x_14^0'=x_14^post6, st_29^0'=st_29^post6, ct_18^0'=ct_18^post6, (0 == 0 /\ -a_290^post6+a_290^0 == 0 /\ ct_18^post6 <= 0 /\ 2-rv_13^post6 <= 0 /\ -x_195^post6+x_195^0 == 0 /\ -nd_12^post6+nd_12^0 == 0 /\ -x_17^post6+x_19^post6 <= 0 /\ y_20^0 <= 0 /\ -a_204^post6+a_204^0 == 0 /\ -st_16^post6+st_16^0 == 0 /\ a_76^0-a_76^post6 == 0 /\ t_24^post6-h_15^post6 <= 0 /\ x_14^post6 <= 0 /\ -r_92^post6+r_92^0 == 0 /\ t_32^0-t_32^post6 == 0 /\ -1-a_239^post6+l_143^post6 <= 0 /\ 1-rv_13^post6 <= 0 /\ r_135^0-r_135^post6 == 0 /\ l_27^0-l_27^post6 == 0 /\ -tp_33^post6+tp_33^0 == 0 /\ x_17^post6-x_19^post6 <= 0 /\ a_264^0-a_264^post6 == 0 /\ -st_29^post6+st_29^0 == 0 /\ t_24^post6-x_21^0 == 0 /\ -l_143^0 <= 0 /\ -t_24^post6+h_15^post6 <= 0 /\ -h_30^post6+h_30^0 == 0 /\ a_123^0-a_123^post6 == 0 /\ x_140^0-x_140^post6 == 0 /\ a_158^0-a_158^post6 == 0 /\ x_17^post6-h_15^post6 <= 0 /\ -y_20^0 <= 0 /\ i_115^0-i_115^post6 == 0 /\ l_203^0-l_203^post6 == 0 /\ -x_14^post6 <= 0 /\ -x_19^post6+h_15^post6 <= 0 /\ -a_264^0+a_239^post6 <= 0 /\ -r_183^post6+r_183^0 == 0 /\ i_28^0-i_28^post6 == 0 /\ i_98^0-i_98^post6 == 0 /\ -ct_18^post6+y_20^0 <= 0 /\ -r_37^post6+r_37^0 == 0 /\ -ct_18^post6 <= 0 /\ i_187^0-i_187^post6 == 0 /\ -x_17^post6+h_15^post6 <= 0 /\ rv_31^0-rv_31^post6 == 0 /\ 1+a_239^post6-l_143^post6 <= 0 /\ -f_190^post6+f_190^0 == 0 /\ y_20^0-y_20^post6 == 0 /\ r_57^0-r_57^post6 == 0 /\ x_19^post6-h_15^post6 <= 0 /\ a_264^0-a_239^post6 <= 0 /\ -x_21^post6+x_21^0 == 0 /\ ct_18^post6-y_20^0 <= 0 /\ -rt_11^post6+rt_11^0 == 0), cost: 1 8: l7 -> l8 : a_264^0'=a_264^post8, l_27^0'=l_27^post8, i_187^0'=i_187^post8, t_32^0'=t_32^post8, rv_13^0'=rv_13^post8, y_20^0'=y_20^post8, a_158^0'=a_158^post8, x_195^0'=x_195^post8, i_98^0'=i_98^post8, h_15^0'=h_15^post8, r_57^0'=r_57^post8, r_135^0'=r_135^post8, x_140^0'=x_140^post8, st_16^0'=st_16^post8, a_76^0'=a_76^post8, a_239^0'=a_239^post8, x_21^0'=x_21^post8, l_203^0'=l_203^post8, i_115^0'=i_115^post8, rt_11^0'=rt_11^post8, r_37^0'=r_37^post8, a_123^0'=a_123^post8, x_17^0'=x_17^post8, t_24^0'=t_24^post8, f_190^0'=f_190^post8, a_290^0'=a_290^post8, nd_12^0'=nd_12^post8, i_28^0'=i_28^post8, tp_33^0'=tp_33^post8, rv_31^0'=rv_31^post8, a_204^0'=a_204^post8, x_19^0'=x_19^post8, l_143^0'=l_143^post8, h_30^0'=h_30^post8, r_92^0'=r_92^post8, r_183^0'=r_183^post8, x_14^0'=x_14^post8, st_29^0'=st_29^post8, ct_18^0'=ct_18^post8, (0 == 0 /\ -x_140^post8+x_140^0 == 0 /\ f_190^0-f_190^post8 == 0 /\ h_30^post8-t_32^post8 <= 0 /\ h_30^post8-t_32^post8 == 0 /\ r_135^0-r_135^post8 == 0 /\ -l_143^post8+l_143^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ -r_183^post8+r_183^0 == 0 /\ -1+i_28^10-i_28^0 == 0 /\ -2+i_28^post8 <= 0 /\ a_204^0-a_204^post8 == 0 /\ -h_30^post8+t_32^post8 <= 0 /\ x_195^0-x_195^post8 == 0 /\ r_37^0-r_37^post8 == 0 /\ x_21^0-x_21^post8 == 0 /\ a_264^0-a_264^post8 == 0 /\ a_239^0-a_239^post8 == 0 /\ l_27^0-rv_13^post8 <= 0 /\ -i_115^post8+i_115^0 == 0 /\ a_290^0-a_290^post8 == 0 /\ a_158^0-a_158^post8 == 0 /\ -x_14^post8+x_14^0 == 0 /\ h_30^post8-rv_31^post8 <= 0 /\ a_76^post8-i_28^post8 <= 0 /\ st_16^0-st_16^post8 == 0 /\ 2-l_27^0 <= 0 /\ l_203^0-l_203^post8 == 0 /\ t_24^0-t_24^post8 == 0 /\ -rv_31^post8+t_32^post8 <= 0 /\ l_27^0-l_27^post8 == 0 /\ 2-i_28^post8 <= 0 /\ i_187^0-i_187^post8 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ h_15^0-h_15^post8 == 0 /\ -l_27^0+rv_13^post8 <= 0 /\ -x_17^post8+x_17^0 == 0 /\ -x_19^post8+x_19^0 == 0 /\ 1-l_27^0 <= 0 /\ i_98^0-i_98^post8 == 0 /\ -h_30^post8+rv_31^post8 <= 0 /\ -r_92^post8+r_92^0 == 0 /\ t_32^post8-tp_33^0 == 0 /\ -a_76^post8+i_28^post8 <= 0 /\ -st_29^post8+st_29^0 == 0 /\ -ct_18^post8+ct_18^0 == 0 /\ -y_20^post8+y_20^0 == 0 /\ 1-l_27^0+i_28^0 <= 0 /\ rv_31^post8-t_32^post8 <= 0 /\ -a_123^post8+a_123^0 == 0), cost: 1 15: l8 -> l9 : a_264^0'=a_264^post15, l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, y_20^0'=y_20^post15, a_158^0'=a_158^post15, x_195^0'=x_195^post15, i_98^0'=i_98^post15, h_15^0'=h_15^post15, r_57^0'=r_57^post15, r_135^0'=r_135^post15, x_140^0'=x_140^post15, st_16^0'=st_16^post15, a_76^0'=a_76^post15, a_239^0'=a_239^post15, x_21^0'=x_21^post15, l_203^0'=l_203^post15, i_115^0'=i_115^post15, rt_11^0'=rt_11^post15, r_37^0'=r_37^post15, a_123^0'=a_123^post15, x_17^0'=x_17^post15, t_24^0'=t_24^post15, f_190^0'=f_190^post15, a_290^0'=a_290^post15, nd_12^0'=nd_12^post15, i_28^0'=i_28^post15, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, a_204^0'=a_204^post15, x_19^0'=x_19^post15, l_143^0'=l_143^post15, h_30^0'=h_30^post15, r_92^0'=r_92^post15, r_183^0'=r_183^post15, x_14^0'=x_14^post15, st_29^0'=st_29^post15, ct_18^0'=ct_18^post15, (0 == 0 /\ -a_158^0+i_28^post15 <= 0 /\ 1-rv_13^post15 <= 0 /\ -x_140^post15+x_140^0 == 0 /\ h_15^post15-x_14^post15 <= 0 /\ x_21^0-x_21^post15 == 0 /\ rv_13^post15-i_28^post15 <= 0 /\ -x_19^post15+x_19^0 == 0 /\ -l_203^post15+l_203^0 == 0 /\ a_264^0-a_264^post15 == 0 /\ -l_143^post15+l_143^0 == 0 /\ -a_204^post15+a_204^0 == 0 /\ -r_92^post15+r_92^0 == 0 /\ -f_190^post15+f_190^0 == 0 /\ a_158^0-i_28^post15 <= 0 /\ x_195^0-x_195^post15 == 0 /\ h_15^post15-rt_11^11 == 0 /\ -h_15^post15+x_14^post15 <= 0 /\ -h_15^post15+x_14^post15 == 0 /\ 2-rv_13^post15 <= 0 /\ -i_115^post15+i_115^0 == 0 /\ -l_143^0 <= 0 /\ -x_17^post15+x_17^0 == 0 /\ -r_57^post15+r_57^0 == 0 /\ -y_20^post15+y_20^0 == 0 /\ -ct_18^post15+ct_18^0 == 0 /\ st_29^110-h_30^0 == 0 /\ i_98^0-i_98^post15 == 0 /\ st_16^0-st_16^post15 == 0 /\ -r_135^post15+r_135^0 == 0 /\ a_158^0-a_158^post15 == 0 /\ l_27^0-i_28^0 <= 0 /\ a_239^0-a_239^post15 == 0 /\ -nd_12^post15+nd_12^0 == 0 /\ -i_28^0 <= 0 /\ -r_37^post15+r_37^0 == 0 /\ -r_183^post15+r_183^0 == 0 /\ -st_29^110+rt_11^11 == 0 /\ l_143^0 <= 0 /\ rv_13^post15-i_187^post15 <= 0 /\ a_76^0-a_76^post15 == 0 /\ t_24^0-t_24^post15 == 0 /\ a_290^0-a_290^post15 == 0 /\ a_123^0-a_123^post15 == 0), cost: 1 16: l8 -> l13 : a_264^0'=a_264^post16, l_27^0'=l_27^post16, i_187^0'=i_187^post16, t_32^0'=t_32^post16, rv_13^0'=rv_13^post16, y_20^0'=y_20^post16, a_158^0'=a_158^post16, x_195^0'=x_195^post16, i_98^0'=i_98^post16, h_15^0'=h_15^post16, r_57^0'=r_57^post16, r_135^0'=r_135^post16, x_140^0'=x_140^post16, st_16^0'=st_16^post16, a_76^0'=a_76^post16, a_239^0'=a_239^post16, x_21^0'=x_21^post16, l_203^0'=l_203^post16, i_115^0'=i_115^post16, rt_11^0'=rt_11^post16, r_37^0'=r_37^post16, a_123^0'=a_123^post16, x_17^0'=x_17^post16, t_24^0'=t_24^post16, f_190^0'=f_190^post16, a_290^0'=a_290^post16, nd_12^0'=nd_12^post16, i_28^0'=i_28^post16, tp_33^0'=tp_33^post16, rv_31^0'=rv_31^post16, a_204^0'=a_204^post16, x_19^0'=x_19^post16, l_143^0'=l_143^post16, h_30^0'=h_30^post16, r_92^0'=r_92^post16, r_183^0'=r_183^post16, x_14^0'=x_14^post16, st_29^0'=st_29^post16, ct_18^0'=ct_18^post16, (0 == 0 /\ l_27^0-l_27^post16 == 0 /\ 1+i_98^post16-i_28^post16 <= 0 /\ h_15^0-h_15^post16 == 0 /\ -rv_31^post16+rv_31^0 == 0 /\ t_24^0-t_24^post16 == 0 /\ x_195^0-x_195^post16 == 0 /\ -x_17^post16+x_17^0 == 0 /\ i_187^0-i_187^post16 == 0 /\ r_57^0-r_57^post16 == 0 /\ i_115^0-i_115^post16 == 0 /\ -1-i_28^0+i_28^post16 == 0 /\ -st_29^post16+st_29^0 == 0 /\ r_135^0-r_135^post16 == 0 /\ h_30^post16-t_32^post16 == 0 /\ -ct_18^post16+ct_18^0 == 0 /\ a_239^0-a_239^post16 == 0 /\ -r_183^post16+r_183^0 == 0 /\ -x_19^post16+x_19^0 == 0 /\ -nd_12^post16+nd_12^0 == 0 /\ -x_140^post16+x_140^0 == 0 /\ -a_204^post16+a_204^0 == 0 /\ -st_16^post16+st_16^0 == 0 /\ l_143^0-l_143^post16 == 0 /\ rv_13^0-rv_13^post16 == 0 /\ -1-i_98^post16+i_28^post16 <= 0 /\ -f_190^post16+f_190^0 == 0 /\ -tp_33^0+t_32^post16 == 0 /\ a_264^0-a_264^post16 == 0 /\ -r_37^post16+r_37^0 == 0 /\ 1+i_98^post16-l_27^0 <= 0 /\ x_21^0-x_21^post16 == 0 /\ -x_14^post16+x_14^0 == 0 /\ -i_28^0 <= 0 /\ -l_203^post16+l_203^0 == 0 /\ -a_76^post16+a_76^0 == 0 /\ rt_11^0-rt_11^post16 == 0 /\ a_290^0-a_290^post16 == 0 /\ a_158^0-a_158^post16 == 0 /\ a_123^0-a_123^post16 == 0 /\ y_20^0-y_20^post16 == 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 9: l9 -> l6 : a_264^0'=a_264^post9, l_27^0'=l_27^post9, i_187^0'=i_187^post9, t_32^0'=t_32^post9, rv_13^0'=rv_13^post9, y_20^0'=y_20^post9, a_158^0'=a_158^post9, x_195^0'=x_195^post9, i_98^0'=i_98^post9, h_15^0'=h_15^post9, r_57^0'=r_57^post9, r_135^0'=r_135^post9, x_140^0'=x_140^post9, st_16^0'=st_16^post9, a_76^0'=a_76^post9, a_239^0'=a_239^post9, x_21^0'=x_21^post9, l_203^0'=l_203^post9, i_115^0'=i_115^post9, rt_11^0'=rt_11^post9, r_37^0'=r_37^post9, a_123^0'=a_123^post9, x_17^0'=x_17^post9, t_24^0'=t_24^post9, f_190^0'=f_190^post9, a_290^0'=a_290^post9, nd_12^0'=nd_12^post9, i_28^0'=i_28^post9, tp_33^0'=tp_33^post9, rv_31^0'=rv_31^post9, a_204^0'=a_204^post9, x_19^0'=x_19^post9, l_143^0'=l_143^post9, h_30^0'=h_30^post9, r_92^0'=r_92^post9, r_183^0'=r_183^post9, x_14^0'=x_14^post9, st_29^0'=st_29^post9, ct_18^0'=ct_18^post9, (0 == 0 /\ t_32^0-t_32^post9 == 0 /\ -i_28^post9+i_28^0 == 0 /\ -l_203^post9+l_203^0 == 0 /\ -rv_31^post9+rv_31^0 == 0 /\ y_20^post9 <= 0 /\ x_19^post9-h_15^0 <= 0 /\ -r_183^post9+r_183^0 == 0 /\ t_24^0-t_24^post9 == 0 /\ -st_29^post9+st_29^0 == 0 /\ h_30^0-h_30^post9 == 0 /\ -r_92^post9+r_92^0 == 0 /\ -x_14^0 <= 0 /\ i_115^0-i_115^post9 == 0 /\ r_135^0-r_135^post9 == 0 /\ l_27^0-l_27^post9 == 0 /\ -x_19^post9+h_15^0 <= 0 /\ r_37^0-r_37^post9 == 0 /\ a_239^0-a_239^post9 == 0 /\ a_264^0-a_264^post9 == 0 /\ -l_143^post9+l_143^0 == 0 /\ -x_140^post9+x_140^0 == 0 /\ -x_14^post9+x_14^0 == 0 /\ x_195^0-x_195^post9 == 0 /\ -l_143^0 <= 0 /\ -a_204^post9+a_204^0 == 0 /\ -a_158^0 <= 0 /\ ct_18^post9 <= 0 /\ ct_18^post9 == 0 /\ -f_190^post9+f_190^0 == 0 /\ 2-rv_13^post9 <= 0 /\ i_98^0-i_98^post9 == 0 /\ tp_33^0-tp_33^post9 == 0 /\ -x_19^post9+x_17^post9 <= 0 /\ a_123^0-a_123^post9 == 0 /\ rt_11^0-rt_11^post9 == 0 /\ -h_15^0+x_17^post9 <= 0 /\ -h_15^0+x_17^post9 == 0 /\ i_187^0-i_187^post9 == 0 /\ a_158^0-a_158^post9 == 0 /\ -r_57^post9+r_57^0 == 0 /\ st_16^0-st_16^post9 == 0 /\ -h_15^0+x_21^post9 <= 0 /\ y_20^post9-ct_18^post9 <= 0 /\ y_20^post9-ct_18^post9 == 0 /\ -x_19^post9+x_21^post9 <= 0 /\ -x_19^post9+x_21^post9 == 0 /\ -y_20^post9 <= 0 /\ -a_76^post9+a_76^0 == 0 /\ -ct_18^post9 <= 0 /\ x_19^post9-x_17^post9 <= 0 /\ x_19^post9-x_17^post9 == 0 /\ h_15^0-h_15^post9 == 0 /\ h_15^0-x_17^post9 <= 0 /\ -a_290^post9+a_290^0 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ x_14^0 <= 0 /\ h_15^0-x_21^post9 <= 0 /\ -y_20^post9+ct_18^post9 <= 0 /\ 1-rv_13^post9 <= 0 /\ x_19^post9-x_21^post9 <= 0), cost: 1 10: l9 -> l10 : a_264^0'=a_264^post10, l_27^0'=l_27^post10, i_187^0'=i_187^post10, t_32^0'=t_32^post10, rv_13^0'=rv_13^post10, y_20^0'=y_20^post10, a_158^0'=a_158^post10, x_195^0'=x_195^post10, i_98^0'=i_98^post10, h_15^0'=h_15^post10, r_57^0'=r_57^post10, r_135^0'=r_135^post10, x_140^0'=x_140^post10, st_16^0'=st_16^post10, a_76^0'=a_76^post10, a_239^0'=a_239^post10, x_21^0'=x_21^post10, l_203^0'=l_203^post10, i_115^0'=i_115^post10, rt_11^0'=rt_11^post10, r_37^0'=r_37^post10, a_123^0'=a_123^post10, x_17^0'=x_17^post10, t_24^0'=t_24^post10, f_190^0'=f_190^post10, a_290^0'=a_290^post10, nd_12^0'=nd_12^post10, i_28^0'=i_28^post10, tp_33^0'=tp_33^post10, rv_31^0'=rv_31^post10, a_204^0'=a_204^post10, x_19^0'=x_19^post10, l_143^0'=l_143^post10, h_30^0'=h_30^post10, r_92^0'=r_92^post10, r_183^0'=r_183^post10, x_14^0'=x_14^post10, st_29^0'=st_29^post10, ct_18^0'=ct_18^post10, (0 == 0 /\ -f_190^post10+x_14^0 <= 0 /\ r_57^0-r_57^post10 == 0 /\ 2-rv_13^post10 <= 0 /\ t_32^0-t_32^post10 == 0 /\ tp_33^0-tp_33^post10 == 0 /\ -x_14^post10+x_14^0 == 0 /\ -x_19^post10+x_19^0 == 0 /\ x_21^0-x_21^post10 == 0 /\ r_135^0-r_135^post10 == 0 /\ 1+a_204^post10-a_158^0 <= 0 /\ -h_30^post10+h_30^0 == 0 /\ 1-rv_13^post10 <= 0 /\ a_290^0-a_290^post10 == 0 /\ -i_28^post10+i_28^0 == 0 /\ -st_29^post10+st_29^0 == 0 /\ f_190^post10-x_14^0 <= 0 /\ -x_17^post10+x_17^0 == 0 /\ i_115^0-i_115^post10 == 0 /\ -ct_18^post10+ct_18^0 == 0 /\ -r_92^post10+r_92^0 == 0 /\ l_27^0-l_27^post10 == 0 /\ -l_143^0 <= 0 /\ -a_123^post10+a_123^0 == 0 /\ a_239^0-a_239^post10 == 0 /\ 1+l_143^0-l_203^post10 <= 0 /\ t_24^0-t_24^post10 == 0 /\ -a_76^post10+a_76^0 == 0 /\ -a_158^0 <= 0 /\ -y_20^post10+y_20^0 == 0 /\ -a_204^post10+a_158^post10 <= 0 /\ -i_187^post10+i_187^0 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ -l_143^post10+l_203^post10 <= 0 /\ a_264^0-a_264^post10 == 0 /\ i_98^0-i_98^post10 == 0 /\ -x_140^post10+x_140^0 == 0 /\ -rv_31^post10+rv_31^0 == 0 /\ -1-a_204^post10+a_158^0 <= 0 /\ -r_183^post10+r_183^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ a_204^post10-a_158^post10 <= 0 /\ st_16^0-st_16^post10 == 0 /\ l_143^post10-l_203^post10 <= 0 /\ -1-l_143^0+l_203^post10 <= 0), cost: 1 11: l10 -> l9 : a_264^0'=a_264^post11, l_27^0'=l_27^post11, i_187^0'=i_187^post11, t_32^0'=t_32^post11, rv_13^0'=rv_13^post11, y_20^0'=y_20^post11, a_158^0'=a_158^post11, x_195^0'=x_195^post11, i_98^0'=i_98^post11, h_15^0'=h_15^post11, r_57^0'=r_57^post11, r_135^0'=r_135^post11, x_140^0'=x_140^post11, st_16^0'=st_16^post11, a_76^0'=a_76^post11, a_239^0'=a_239^post11, x_21^0'=x_21^post11, l_203^0'=l_203^post11, i_115^0'=i_115^post11, rt_11^0'=rt_11^post11, r_37^0'=r_37^post11, a_123^0'=a_123^post11, x_17^0'=x_17^post11, t_24^0'=t_24^post11, f_190^0'=f_190^post11, a_290^0'=a_290^post11, nd_12^0'=nd_12^post11, i_28^0'=i_28^post11, tp_33^0'=tp_33^post11, rv_31^0'=rv_31^post11, a_204^0'=a_204^post11, x_19^0'=x_19^post11, l_143^0'=l_143^post11, h_30^0'=h_30^post11, r_92^0'=r_92^post11, r_183^0'=r_183^post11, x_14^0'=x_14^post11, st_29^0'=st_29^post11, ct_18^0'=ct_18^post11, (l_27^0-l_27^post11 == 0 /\ f_190^0-f_190^post11 == 0 /\ -x_17^post11+x_17^0 == 0 /\ r_37^0-r_37^post11 == 0 /\ -nd_12^post11+nd_12^0 == 0 /\ a_239^0-a_239^post11 == 0 /\ x_195^0-x_195^post11 == 0 /\ -h_30^post11+h_30^0 == 0 /\ rv_13^0-rv_13^post11 == 0 /\ -a_123^post11+a_123^0 == 0 /\ r_57^0-r_57^post11 == 0 /\ i_115^0-i_115^post11 == 0 /\ -a_76^post11+a_76^0 == 0 /\ y_20^0-y_20^post11 == 0 /\ x_21^0-x_21^post11 == 0 /\ t_24^0-t_24^post11 == 0 /\ -l_143^post11+l_143^0 == 0 /\ -x_140^post11+x_140^0 == 0 /\ r_135^0-r_135^post11 == 0 /\ st_16^0-st_16^post11 == 0 /\ -r_183^post11+r_183^0 == 0 /\ -i_28^post11+i_28^0 == 0 /\ -rv_31^post11+rv_31^0 == 0 /\ a_264^0-a_264^post11 == 0 /\ -x_14^post11+x_14^0 == 0 /\ l_203^0-l_203^post11 == 0 /\ h_15^0-h_15^post11 == 0 /\ -a_204^post11+a_204^0 == 0 /\ -st_29^post11+st_29^0 == 0 /\ -r_92^post11+r_92^0 == 0 /\ i_187^0-i_187^post11 == 0 /\ -i_98^post11+i_98^0 == 0 /\ a_290^0-a_290^post11 == 0 /\ -ct_18^post11+ct_18^0 == 0 /\ rt_11^0-rt_11^post11 == 0 /\ tp_33^0-tp_33^post11 == 0 /\ a_158^0-a_158^post11 == 0 /\ -x_19^post11+x_19^0 == 0 /\ t_32^0-t_32^post11 == 0), cost: 1 17: l13 -> l8 : a_264^0'=a_264^post17, l_27^0'=l_27^post17, i_187^0'=i_187^post17, t_32^0'=t_32^post17, rv_13^0'=rv_13^post17, y_20^0'=y_20^post17, a_158^0'=a_158^post17, x_195^0'=x_195^post17, i_98^0'=i_98^post17, h_15^0'=h_15^post17, r_57^0'=r_57^post17, r_135^0'=r_135^post17, x_140^0'=x_140^post17, st_16^0'=st_16^post17, a_76^0'=a_76^post17, a_239^0'=a_239^post17, x_21^0'=x_21^post17, l_203^0'=l_203^post17, i_115^0'=i_115^post17, rt_11^0'=rt_11^post17, r_37^0'=r_37^post17, a_123^0'=a_123^post17, x_17^0'=x_17^post17, t_24^0'=t_24^post17, f_190^0'=f_190^post17, a_290^0'=a_290^post17, nd_12^0'=nd_12^post17, i_28^0'=i_28^post17, tp_33^0'=tp_33^post17, rv_31^0'=rv_31^post17, a_204^0'=a_204^post17, x_19^0'=x_19^post17, l_143^0'=l_143^post17, h_30^0'=h_30^post17, r_92^0'=r_92^post17, r_183^0'=r_183^post17, x_14^0'=x_14^post17, st_29^0'=st_29^post17, ct_18^0'=ct_18^post17, (-h_30^post17+h_30^0 == 0 /\ -ct_18^post17+ct_18^0 == 0 /\ -nd_12^post17+nd_12^0 == 0 /\ l_27^0-l_27^post17 == 0 /\ st_16^0-st_16^post17 == 0 /\ i_187^0-i_187^post17 == 0 /\ -l_143^post17+l_143^0 == 0 /\ -r_37^post17+r_37^0 == 0 /\ -x_140^post17+x_140^0 == 0 /\ r_57^0-r_57^post17 == 0 /\ i_115^0-i_115^post17 == 0 /\ h_15^0-h_15^post17 == 0 /\ -a_76^post17+a_76^0 == 0 /\ y_20^0-y_20^post17 == 0 /\ -st_29^post17+st_29^0 == 0 /\ -tp_33^post17+tp_33^0 == 0 /\ a_290^0-a_290^post17 == 0 /\ x_14^0-x_14^post17 == 0 /\ rv_13^0-rv_13^post17 == 0 /\ -x_19^post17+x_19^0 == 0 /\ -r_183^post17+r_183^0 == 0 /\ -a_204^post17+a_204^0 == 0 /\ -r_92^post17+r_92^0 == 0 /\ x_195^0-x_195^post17 == 0 /\ a_123^0-a_123^post17 == 0 /\ -t_24^post17+t_24^0 == 0 /\ a_158^0-a_158^post17 == 0 /\ t_32^0-t_32^post17 == 0 /\ x_21^0-x_21^post17 == 0 /\ r_135^0-r_135^post17 == 0 /\ -i_98^post17+i_98^0 == 0 /\ -f_190^post17+f_190^0 == 0 /\ rt_11^0-rt_11^post17 == 0 /\ -x_17^post17+x_17^0 == 0 /\ a_239^0-a_239^post17 == 0 /\ -rv_31^post17+rv_31^0 == 0 /\ a_264^0-a_264^post17 == 0 /\ -l_203^post17+l_203^0 == 0 /\ i_28^0-i_28^post17 == 0), cost: 1 20: l14 -> l0 : a_264^0'=a_264^post20, l_27^0'=l_27^post20, i_187^0'=i_187^post20, t_32^0'=t_32^post20, rv_13^0'=rv_13^post20, y_20^0'=y_20^post20, a_158^0'=a_158^post20, x_195^0'=x_195^post20, i_98^0'=i_98^post20, h_15^0'=h_15^post20, r_57^0'=r_57^post20, r_135^0'=r_135^post20, x_140^0'=x_140^post20, st_16^0'=st_16^post20, a_76^0'=a_76^post20, a_239^0'=a_239^post20, x_21^0'=x_21^post20, l_203^0'=l_203^post20, i_115^0'=i_115^post20, rt_11^0'=rt_11^post20, r_37^0'=r_37^post20, a_123^0'=a_123^post20, x_17^0'=x_17^post20, t_24^0'=t_24^post20, f_190^0'=f_190^post20, a_290^0'=a_290^post20, nd_12^0'=nd_12^post20, i_28^0'=i_28^post20, tp_33^0'=tp_33^post20, rv_31^0'=rv_31^post20, a_204^0'=a_204^post20, x_19^0'=x_19^post20, l_143^0'=l_143^post20, h_30^0'=h_30^post20, r_92^0'=r_92^post20, r_183^0'=r_183^post20, x_14^0'=x_14^post20, st_29^0'=st_29^post20, ct_18^0'=ct_18^post20, (a_204^0-a_204^post20 == 0 /\ -nd_12^post20+nd_12^0 == 0 /\ -st_29^post20+st_29^0 == 0 /\ l_27^0-l_27^post20 == 0 /\ r_57^0-r_57^post20 == 0 /\ -ct_18^post20+ct_18^0 == 0 /\ rv_13^0-rv_13^post20 == 0 /\ x_195^0-x_195^post20 == 0 /\ a_76^0-a_76^post20 == 0 /\ a_123^0-a_123^post20 == 0 /\ i_98^0-i_98^post20 == 0 /\ -st_16^post20+st_16^0 == 0 /\ x_17^0-x_17^post20 == 0 /\ x_19^0-x_19^post20 == 0 /\ -r_37^post20+r_37^0 == 0 /\ i_187^0-i_187^post20 == 0 /\ -rt_11^post20+rt_11^0 == 0 /\ y_20^0-y_20^post20 == 0 /\ r_135^0-r_135^post20 == 0 /\ x_140^0-x_140^post20 == 0 /\ h_15^0-h_15^post20 == 0 /\ -h_30^post20+h_30^0 == 0 /\ -r_183^post20+r_183^0 == 0 /\ i_115^0-i_115^post20 == 0 /\ -a_239^post20+a_239^0 == 0 /\ -tp_33^post20+tp_33^0 == 0 /\ a_264^0-a_264^post20 == 0 /\ l_203^0-l_203^post20 == 0 /\ -t_32^post20+t_32^0 == 0 /\ -r_92^post20+r_92^0 == 0 /\ a_158^0-a_158^post20 == 0 /\ -x_21^post20+x_21^0 == 0 /\ -t_24^post20+t_24^0 == 0 /\ -a_290^post20+a_290^0 == 0 /\ rv_31^0-rv_31^post20 == 0 /\ -x_14^post20+x_14^0 == 0 /\ -f_190^post20+f_190^0 == 0 /\ -i_28^post20+i_28^0 == 0 /\ -l_143^post20+l_143^0 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : a_264^0'=a_264^post0, l_27^0'=l_27^post0, i_187^0'=i_187^post0, t_32^0'=t_32^post0, rv_13^0'=rv_13^post0, y_20^0'=y_20^post0, a_158^0'=a_158^post0, x_195^0'=x_195^post0, i_98^0'=i_98^post0, h_15^0'=h_15^post0, r_57^0'=r_57^post0, r_135^0'=r_135^post0, x_140^0'=x_140^post0, st_16^0'=st_16^post0, a_76^0'=a_76^post0, a_239^0'=a_239^post0, x_21^0'=x_21^post0, l_203^0'=l_203^post0, i_115^0'=i_115^post0, rt_11^0'=rt_11^post0, r_37^0'=r_37^post0, a_123^0'=a_123^post0, x_17^0'=x_17^post0, t_24^0'=t_24^post0, f_190^0'=f_190^post0, a_290^0'=a_290^post0, nd_12^0'=nd_12^post0, i_28^0'=i_28^post0, tp_33^0'=tp_33^post0, rv_31^0'=rv_31^post0, a_204^0'=a_204^post0, x_19^0'=x_19^post0, l_143^0'=l_143^post0, h_30^0'=h_30^post0, r_92^0'=r_92^post0, r_183^0'=r_183^post0, x_14^0'=x_14^post0, st_29^0'=st_29^post0, ct_18^0'=ct_18^post0, (0 == 0 /\ -f_190^post0+f_190^0 == 0 /\ -a_204^post0+a_204^0 == 0 /\ -a_290^post0+a_290^0 == 0 /\ h_15^0-h_15^post0 == 0 /\ l_143^0-l_143^post0 == 0 /\ a_264^0-a_264^post0 == 0 /\ a_76^0-a_76^post0 == 0 /\ l_203^0-l_203^post0 == 0 /\ t_32^0-t_32^post0 == 0 /\ rv_13^post0-nd_12^10 == 0 /\ -st_16^post0+st_16^0 == 0 /\ -x_19^post0+x_19^0 == 0 /\ -h_30^post0 <= 0 /\ -tp_33^post0+tp_33^0 == 0 /\ i_28^post0 <= 0 /\ i_28^post0 == 0 /\ -a_239^post0+a_239^0 == 0 /\ -r_92^post0+r_92^0 == 0 /\ -st_29^post0+st_29^0 == 0 /\ -i_28^post0 <= 0 /\ r_135^0-r_135^post0 == 0 /\ -ct_18^post0+ct_18^0 == 0 /\ -a_123^post0+a_123^0 == 0 /\ i_115^0-i_115^post0 == 0 /\ -rv_13^post0+l_27^post0 <= 0 /\ -rv_13^post0+l_27^post0 == 0 /\ -r_183^post0+r_183^0 == 0 /\ a_158^0-a_158^post0 == 0 /\ x_140^0-x_140^post0 == 0 /\ -x_21^post0+x_21^0 == 0 /\ x_195^0-x_195^post0 == 0 /\ r_37^0-r_37^post0 == 0 /\ rv_13^post0-l_27^post0 <= 0 /\ h_30^post0 <= 0 /\ h_30^post0 == 0 /\ i_98^0-i_98^post0 == 0 /\ -x_17^post0+x_17^0 == 0 /\ -rt_11^post0+rt_11^0 == 0 /\ i_187^0-i_187^post0 == 0 /\ -t_24^post0+t_24^0 == 0 /\ -x_14^post0+x_14^0 == 0 /\ rv_31^0-rv_31^post0 == 0 /\ r_57^0-r_57^post0 == 0 /\ y_20^0-y_20^post0 == 0), cost: 1 New rule: l0 -> l1 : l_27^0'=nd_12^10, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=0, h_30^0'=0, 0 == 0, cost: 1 Applied preprocessing Original rule: l2 -> l4 : a_264^0'=a_264^post2, l_27^0'=l_27^post2, i_187^0'=i_187^post2, t_32^0'=t_32^post2, rv_13^0'=rv_13^post2, y_20^0'=y_20^post2, a_158^0'=a_158^post2, x_195^0'=x_195^post2, i_98^0'=i_98^post2, h_15^0'=h_15^post2, r_57^0'=r_57^post2, r_135^0'=r_135^post2, x_140^0'=x_140^post2, st_16^0'=st_16^post2, a_76^0'=a_76^post2, a_239^0'=a_239^post2, x_21^0'=x_21^post2, l_203^0'=l_203^post2, i_115^0'=i_115^post2, rt_11^0'=rt_11^post2, r_37^0'=r_37^post2, a_123^0'=a_123^post2, x_17^0'=x_17^post2, t_24^0'=t_24^post2, f_190^0'=f_190^post2, a_290^0'=a_290^post2, nd_12^0'=nd_12^post2, i_28^0'=i_28^post2, tp_33^0'=tp_33^post2, rv_31^0'=rv_31^post2, a_204^0'=a_204^post2, x_19^0'=x_19^post2, l_143^0'=l_143^post2, h_30^0'=h_30^post2, r_92^0'=r_92^post2, r_183^0'=r_183^post2, x_14^0'=x_14^post2, st_29^0'=st_29^post2, ct_18^0'=ct_18^post2, (0 == 0 /\ -y_20^0+ct_18^post2 <= 0 /\ -a_239^post2+a_239^0 == 0 /\ -1+a_264^0-a_290^post2 <= 0 /\ t_32^0-t_32^post2 == 0 /\ r_57^0-r_57^post2 == 0 /\ 1-rv_13^post2 <= 0 /\ y_20^0 <= 0 /\ -x_195^post2+x_195^0 == 0 /\ y_20^0-y_20^post2 == 0 /\ ct_18^post2 <= 0 /\ -a_290^post2+a_264^post2 <= 0 /\ x_19^post2-x_17^post2 <= 0 /\ -r_183^post2+r_183^0 == 0 /\ x_19^post2-h_15^post2 <= 0 /\ -r_92^post2+r_92^0 == 0 /\ y_20^0-ct_18^post2 <= 0 /\ -x_21^post2+x_21^0 == 0 /\ x_140^0-x_140^post2 == 0 /\ 2-rv_13^post2 <= 0 /\ x_14^post2 <= 0 /\ -l_143^post2+l_143^0 == 0 /\ -i_115^post2+i_115^0 == 0 /\ -i_28^post2+i_28^0 == 0 /\ l_203^0-l_203^post2 == 0 /\ -x_14^post2 <= 0 /\ l_27^0-l_27^post2 == 0 /\ a_290^post2-a_264^post2 <= 0 /\ -x_19^post2+x_17^post2 <= 0 /\ a_76^0-a_76^post2 == 0 /\ -r_135^post2+r_135^0 == 0 /\ -x_19^post2+h_15^post2 <= 0 /\ -rt_11^post2+rt_11^0 == 0 /\ -x_17^post2+h_15^post2 <= 0 /\ -ct_18^post2 <= 0 /\ i_187^0-i_187^post2 == 0 /\ 1-a_264^0+a_290^post2 <= 0 /\ -y_20^0 <= 0 /\ rv_31^0-rv_31^post2 == 0 /\ -nd_12^post2+nd_12^0 == 0 /\ -a_204^post2+a_204^0 == 0 /\ -a_123^post2+a_123^0 == 0 /\ -st_16^post2+st_16^0 == 0 /\ i_98^0-i_98^post2 == 0 /\ f_190^0-f_190^post2 == 0 /\ x_17^post2-h_15^post2 <= 0 /\ a_158^0-a_158^post2 == 0 /\ -a_264^0 <= 0 /\ -tp_33^post2+tp_33^0 == 0 /\ -h_30^post2+h_30^0 == 0 /\ t_24^post2-x_21^0 == 0 /\ -st_29^post2+st_29^0 == 0), cost: 1 New rule: l2 -> l4 : a_264^0'=-1+a_264^0, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1+a_264^0, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 == 0 /\ -2+rv_13^post2 >= 0), cost: 1 Applied preprocessing Original rule: l4 -> l2 : a_264^0'=a_264^post3, l_27^0'=l_27^post3, i_187^0'=i_187^post3, t_32^0'=t_32^post3, rv_13^0'=rv_13^post3, y_20^0'=y_20^post3, a_158^0'=a_158^post3, x_195^0'=x_195^post3, i_98^0'=i_98^post3, h_15^0'=h_15^post3, r_57^0'=r_57^post3, r_135^0'=r_135^post3, x_140^0'=x_140^post3, st_16^0'=st_16^post3, a_76^0'=a_76^post3, a_239^0'=a_239^post3, x_21^0'=x_21^post3, l_203^0'=l_203^post3, i_115^0'=i_115^post3, rt_11^0'=rt_11^post3, r_37^0'=r_37^post3, a_123^0'=a_123^post3, x_17^0'=x_17^post3, t_24^0'=t_24^post3, f_190^0'=f_190^post3, a_290^0'=a_290^post3, nd_12^0'=nd_12^post3, i_28^0'=i_28^post3, tp_33^0'=tp_33^post3, rv_31^0'=rv_31^post3, a_204^0'=a_204^post3, x_19^0'=x_19^post3, l_143^0'=l_143^post3, h_30^0'=h_30^post3, r_92^0'=r_92^post3, r_183^0'=r_183^post3, x_14^0'=x_14^post3, st_29^0'=st_29^post3, ct_18^0'=ct_18^post3, (-r_92^post3+r_92^0 == 0 /\ -l_143^post3+l_143^0 == 0 /\ -r_135^post3+r_135^0 == 0 /\ rv_13^0-rv_13^post3 == 0 /\ -r_37^post3+r_37^0 == 0 /\ a_158^0-a_158^post3 == 0 /\ -i_28^post3+i_28^0 == 0 /\ st_16^0-st_16^post3 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ -t_24^post3+t_24^0 == 0 /\ l_27^0-l_27^post3 == 0 /\ r_57^0-r_57^post3 == 0 /\ l_203^0-l_203^post3 == 0 /\ -r_183^post3+r_183^0 == 0 /\ y_20^0-y_20^post3 == 0 /\ i_98^0-i_98^post3 == 0 /\ x_17^0-x_17^post3 == 0 /\ x_19^0-x_19^post3 == 0 /\ x_140^0-x_140^post3 == 0 /\ -a_204^post3+a_204^0 == 0 /\ h_15^0-h_15^post3 == 0 /\ -x_14^post3+x_14^0 == 0 /\ a_76^0-a_76^post3 == 0 /\ -x_21^post3+x_21^0 == 0 /\ -i_115^post3+i_115^0 == 0 /\ f_190^0-f_190^post3 == 0 /\ st_29^0-st_29^post3 == 0 /\ -a_123^post3+a_123^0 == 0 /\ i_187^0-i_187^post3 == 0 /\ -rv_31^post3+rv_31^0 == 0 /\ -a_290^post3+a_290^0 == 0 /\ -a_239^post3+a_239^0 == 0 /\ -h_30^post3+h_30^0 == 0 /\ -tp_33^post3+tp_33^0 == 0 /\ x_195^0-x_195^post3 == 0 /\ -ct_18^post3+ct_18^0 == 0 /\ -t_32^post3+t_32^0 == 0 /\ -nd_12^post3+nd_12^0 == 0 /\ a_264^0-a_264^post3 == 0), cost: 1 New rule: l4 -> l2 : TRUE, cost: 1 Applied preprocessing Original rule: l6 -> l2 : a_264^0'=a_264^post6, l_27^0'=l_27^post6, i_187^0'=i_187^post6, t_32^0'=t_32^post6, rv_13^0'=rv_13^post6, y_20^0'=y_20^post6, a_158^0'=a_158^post6, x_195^0'=x_195^post6, i_98^0'=i_98^post6, h_15^0'=h_15^post6, r_57^0'=r_57^post6, r_135^0'=r_135^post6, x_140^0'=x_140^post6, st_16^0'=st_16^post6, a_76^0'=a_76^post6, a_239^0'=a_239^post6, x_21^0'=x_21^post6, l_203^0'=l_203^post6, i_115^0'=i_115^post6, rt_11^0'=rt_11^post6, r_37^0'=r_37^post6, a_123^0'=a_123^post6, x_17^0'=x_17^post6, t_24^0'=t_24^post6, f_190^0'=f_190^post6, a_290^0'=a_290^post6, nd_12^0'=nd_12^post6, i_28^0'=i_28^post6, tp_33^0'=tp_33^post6, rv_31^0'=rv_31^post6, a_204^0'=a_204^post6, x_19^0'=x_19^post6, l_143^0'=l_143^post6, h_30^0'=h_30^post6, r_92^0'=r_92^post6, r_183^0'=r_183^post6, x_14^0'=x_14^post6, st_29^0'=st_29^post6, ct_18^0'=ct_18^post6, (0 == 0 /\ -a_290^post6+a_290^0 == 0 /\ ct_18^post6 <= 0 /\ 2-rv_13^post6 <= 0 /\ -x_195^post6+x_195^0 == 0 /\ -nd_12^post6+nd_12^0 == 0 /\ -x_17^post6+x_19^post6 <= 0 /\ y_20^0 <= 0 /\ -a_204^post6+a_204^0 == 0 /\ -st_16^post6+st_16^0 == 0 /\ a_76^0-a_76^post6 == 0 /\ t_24^post6-h_15^post6 <= 0 /\ x_14^post6 <= 0 /\ -r_92^post6+r_92^0 == 0 /\ t_32^0-t_32^post6 == 0 /\ -1-a_239^post6+l_143^post6 <= 0 /\ 1-rv_13^post6 <= 0 /\ r_135^0-r_135^post6 == 0 /\ l_27^0-l_27^post6 == 0 /\ -tp_33^post6+tp_33^0 == 0 /\ x_17^post6-x_19^post6 <= 0 /\ a_264^0-a_264^post6 == 0 /\ -st_29^post6+st_29^0 == 0 /\ t_24^post6-x_21^0 == 0 /\ -l_143^0 <= 0 /\ -t_24^post6+h_15^post6 <= 0 /\ -h_30^post6+h_30^0 == 0 /\ a_123^0-a_123^post6 == 0 /\ x_140^0-x_140^post6 == 0 /\ a_158^0-a_158^post6 == 0 /\ x_17^post6-h_15^post6 <= 0 /\ -y_20^0 <= 0 /\ i_115^0-i_115^post6 == 0 /\ l_203^0-l_203^post6 == 0 /\ -x_14^post6 <= 0 /\ -x_19^post6+h_15^post6 <= 0 /\ -a_264^0+a_239^post6 <= 0 /\ -r_183^post6+r_183^0 == 0 /\ i_28^0-i_28^post6 == 0 /\ i_98^0-i_98^post6 == 0 /\ -ct_18^post6+y_20^0 <= 0 /\ -r_37^post6+r_37^0 == 0 /\ -ct_18^post6 <= 0 /\ i_187^0-i_187^post6 == 0 /\ -x_17^post6+h_15^post6 <= 0 /\ rv_31^0-rv_31^post6 == 0 /\ 1+a_239^post6-l_143^post6 <= 0 /\ -f_190^post6+f_190^0 == 0 /\ y_20^0-y_20^post6 == 0 /\ r_57^0-r_57^post6 == 0 /\ x_19^post6-h_15^post6 <= 0 /\ a_264^0-a_239^post6 <= 0 /\ -x_21^post6+x_21^0 == 0 /\ ct_18^post6-y_20^0 <= 0 /\ -rt_11^post6+rt_11^0 == 0), cost: 1 New rule: l6 -> l2 : rv_13^0'=rv_13^post6, h_15^0'=x_21^0, a_239^0'=a_264^0, x_17^0'=x_21^0, t_24^0'=x_21^0, x_19^0'=x_21^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (y_20^0 == 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0), cost: 1 Applied preprocessing Original rule: l7 -> l8 : a_264^0'=a_264^post8, l_27^0'=l_27^post8, i_187^0'=i_187^post8, t_32^0'=t_32^post8, rv_13^0'=rv_13^post8, y_20^0'=y_20^post8, a_158^0'=a_158^post8, x_195^0'=x_195^post8, i_98^0'=i_98^post8, h_15^0'=h_15^post8, r_57^0'=r_57^post8, r_135^0'=r_135^post8, x_140^0'=x_140^post8, st_16^0'=st_16^post8, a_76^0'=a_76^post8, a_239^0'=a_239^post8, x_21^0'=x_21^post8, l_203^0'=l_203^post8, i_115^0'=i_115^post8, rt_11^0'=rt_11^post8, r_37^0'=r_37^post8, a_123^0'=a_123^post8, x_17^0'=x_17^post8, t_24^0'=t_24^post8, f_190^0'=f_190^post8, a_290^0'=a_290^post8, nd_12^0'=nd_12^post8, i_28^0'=i_28^post8, tp_33^0'=tp_33^post8, rv_31^0'=rv_31^post8, a_204^0'=a_204^post8, x_19^0'=x_19^post8, l_143^0'=l_143^post8, h_30^0'=h_30^post8, r_92^0'=r_92^post8, r_183^0'=r_183^post8, x_14^0'=x_14^post8, st_29^0'=st_29^post8, ct_18^0'=ct_18^post8, (0 == 0 /\ -x_140^post8+x_140^0 == 0 /\ f_190^0-f_190^post8 == 0 /\ h_30^post8-t_32^post8 <= 0 /\ h_30^post8-t_32^post8 == 0 /\ r_135^0-r_135^post8 == 0 /\ -l_143^post8+l_143^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ -r_183^post8+r_183^0 == 0 /\ -1+i_28^10-i_28^0 == 0 /\ -2+i_28^post8 <= 0 /\ a_204^0-a_204^post8 == 0 /\ -h_30^post8+t_32^post8 <= 0 /\ x_195^0-x_195^post8 == 0 /\ r_37^0-r_37^post8 == 0 /\ x_21^0-x_21^post8 == 0 /\ a_264^0-a_264^post8 == 0 /\ a_239^0-a_239^post8 == 0 /\ l_27^0-rv_13^post8 <= 0 /\ -i_115^post8+i_115^0 == 0 /\ a_290^0-a_290^post8 == 0 /\ a_158^0-a_158^post8 == 0 /\ -x_14^post8+x_14^0 == 0 /\ h_30^post8-rv_31^post8 <= 0 /\ a_76^post8-i_28^post8 <= 0 /\ st_16^0-st_16^post8 == 0 /\ 2-l_27^0 <= 0 /\ l_203^0-l_203^post8 == 0 /\ t_24^0-t_24^post8 == 0 /\ -rv_31^post8+t_32^post8 <= 0 /\ l_27^0-l_27^post8 == 0 /\ 2-i_28^post8 <= 0 /\ i_187^0-i_187^post8 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ h_15^0-h_15^post8 == 0 /\ -l_27^0+rv_13^post8 <= 0 /\ -x_17^post8+x_17^0 == 0 /\ -x_19^post8+x_19^0 == 0 /\ 1-l_27^0 <= 0 /\ i_98^0-i_98^post8 == 0 /\ -h_30^post8+rv_31^post8 <= 0 /\ -r_92^post8+r_92^0 == 0 /\ t_32^post8-tp_33^0 == 0 /\ -a_76^post8+i_28^post8 <= 0 /\ -st_29^post8+st_29^0 == 0 /\ -ct_18^post8+ct_18^0 == 0 /\ -y_20^post8+y_20^0 == 0 /\ 1-l_27^0+i_28^0 <= 0 /\ rv_31^post8-t_32^post8 <= 0 /\ -a_123^post8+a_123^0 == 0), cost: 1 New rule: l7 -> l8 : t_32^0'=tp_33^0, rv_13^0'=l_27^0, r_57^0'=r_57^post8, a_76^0'=2, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, (-2+l_27^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 Applied preprocessing Original rule: l9 -> l6 : a_264^0'=a_264^post9, l_27^0'=l_27^post9, i_187^0'=i_187^post9, t_32^0'=t_32^post9, rv_13^0'=rv_13^post9, y_20^0'=y_20^post9, a_158^0'=a_158^post9, x_195^0'=x_195^post9, i_98^0'=i_98^post9, h_15^0'=h_15^post9, r_57^0'=r_57^post9, r_135^0'=r_135^post9, x_140^0'=x_140^post9, st_16^0'=st_16^post9, a_76^0'=a_76^post9, a_239^0'=a_239^post9, x_21^0'=x_21^post9, l_203^0'=l_203^post9, i_115^0'=i_115^post9, rt_11^0'=rt_11^post9, r_37^0'=r_37^post9, a_123^0'=a_123^post9, x_17^0'=x_17^post9, t_24^0'=t_24^post9, f_190^0'=f_190^post9, a_290^0'=a_290^post9, nd_12^0'=nd_12^post9, i_28^0'=i_28^post9, tp_33^0'=tp_33^post9, rv_31^0'=rv_31^post9, a_204^0'=a_204^post9, x_19^0'=x_19^post9, l_143^0'=l_143^post9, h_30^0'=h_30^post9, r_92^0'=r_92^post9, r_183^0'=r_183^post9, x_14^0'=x_14^post9, st_29^0'=st_29^post9, ct_18^0'=ct_18^post9, (0 == 0 /\ t_32^0-t_32^post9 == 0 /\ -i_28^post9+i_28^0 == 0 /\ -l_203^post9+l_203^0 == 0 /\ -rv_31^post9+rv_31^0 == 0 /\ y_20^post9 <= 0 /\ x_19^post9-h_15^0 <= 0 /\ -r_183^post9+r_183^0 == 0 /\ t_24^0-t_24^post9 == 0 /\ -st_29^post9+st_29^0 == 0 /\ h_30^0-h_30^post9 == 0 /\ -r_92^post9+r_92^0 == 0 /\ -x_14^0 <= 0 /\ i_115^0-i_115^post9 == 0 /\ r_135^0-r_135^post9 == 0 /\ l_27^0-l_27^post9 == 0 /\ -x_19^post9+h_15^0 <= 0 /\ r_37^0-r_37^post9 == 0 /\ a_239^0-a_239^post9 == 0 /\ a_264^0-a_264^post9 == 0 /\ -l_143^post9+l_143^0 == 0 /\ -x_140^post9+x_140^0 == 0 /\ -x_14^post9+x_14^0 == 0 /\ x_195^0-x_195^post9 == 0 /\ -l_143^0 <= 0 /\ -a_204^post9+a_204^0 == 0 /\ -a_158^0 <= 0 /\ ct_18^post9 <= 0 /\ ct_18^post9 == 0 /\ -f_190^post9+f_190^0 == 0 /\ 2-rv_13^post9 <= 0 /\ i_98^0-i_98^post9 == 0 /\ tp_33^0-tp_33^post9 == 0 /\ -x_19^post9+x_17^post9 <= 0 /\ a_123^0-a_123^post9 == 0 /\ rt_11^0-rt_11^post9 == 0 /\ -h_15^0+x_17^post9 <= 0 /\ -h_15^0+x_17^post9 == 0 /\ i_187^0-i_187^post9 == 0 /\ a_158^0-a_158^post9 == 0 /\ -r_57^post9+r_57^0 == 0 /\ st_16^0-st_16^post9 == 0 /\ -h_15^0+x_21^post9 <= 0 /\ y_20^post9-ct_18^post9 <= 0 /\ y_20^post9-ct_18^post9 == 0 /\ -x_19^post9+x_21^post9 <= 0 /\ -x_19^post9+x_21^post9 == 0 /\ -y_20^post9 <= 0 /\ -a_76^post9+a_76^0 == 0 /\ -ct_18^post9 <= 0 /\ x_19^post9-x_17^post9 <= 0 /\ x_19^post9-x_17^post9 == 0 /\ h_15^0-h_15^post9 == 0 /\ h_15^0-x_17^post9 <= 0 /\ -a_290^post9+a_290^0 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ x_14^0 <= 0 /\ h_15^0-x_21^post9 <= 0 /\ -y_20^post9+ct_18^post9 <= 0 /\ 1-rv_13^post9 <= 0 /\ x_19^post9-x_21^post9 <= 0), cost: 1 New rule: l9 -> l6 : rv_13^0'=rv_13^post9, y_20^0'=0, x_21^0'=h_15^0, x_17^0'=h_15^0, x_19^0'=h_15^0, ct_18^0'=0, (-2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 1 Applied preprocessing Original rule: l9 -> l10 : a_264^0'=a_264^post10, l_27^0'=l_27^post10, i_187^0'=i_187^post10, t_32^0'=t_32^post10, rv_13^0'=rv_13^post10, y_20^0'=y_20^post10, a_158^0'=a_158^post10, x_195^0'=x_195^post10, i_98^0'=i_98^post10, h_15^0'=h_15^post10, r_57^0'=r_57^post10, r_135^0'=r_135^post10, x_140^0'=x_140^post10, st_16^0'=st_16^post10, a_76^0'=a_76^post10, a_239^0'=a_239^post10, x_21^0'=x_21^post10, l_203^0'=l_203^post10, i_115^0'=i_115^post10, rt_11^0'=rt_11^post10, r_37^0'=r_37^post10, a_123^0'=a_123^post10, x_17^0'=x_17^post10, t_24^0'=t_24^post10, f_190^0'=f_190^post10, a_290^0'=a_290^post10, nd_12^0'=nd_12^post10, i_28^0'=i_28^post10, tp_33^0'=tp_33^post10, rv_31^0'=rv_31^post10, a_204^0'=a_204^post10, x_19^0'=x_19^post10, l_143^0'=l_143^post10, h_30^0'=h_30^post10, r_92^0'=r_92^post10, r_183^0'=r_183^post10, x_14^0'=x_14^post10, st_29^0'=st_29^post10, ct_18^0'=ct_18^post10, (0 == 0 /\ -f_190^post10+x_14^0 <= 0 /\ r_57^0-r_57^post10 == 0 /\ 2-rv_13^post10 <= 0 /\ t_32^0-t_32^post10 == 0 /\ tp_33^0-tp_33^post10 == 0 /\ -x_14^post10+x_14^0 == 0 /\ -x_19^post10+x_19^0 == 0 /\ x_21^0-x_21^post10 == 0 /\ r_135^0-r_135^post10 == 0 /\ 1+a_204^post10-a_158^0 <= 0 /\ -h_30^post10+h_30^0 == 0 /\ 1-rv_13^post10 <= 0 /\ a_290^0-a_290^post10 == 0 /\ -i_28^post10+i_28^0 == 0 /\ -st_29^post10+st_29^0 == 0 /\ f_190^post10-x_14^0 <= 0 /\ -x_17^post10+x_17^0 == 0 /\ i_115^0-i_115^post10 == 0 /\ -ct_18^post10+ct_18^0 == 0 /\ -r_92^post10+r_92^0 == 0 /\ l_27^0-l_27^post10 == 0 /\ -l_143^0 <= 0 /\ -a_123^post10+a_123^0 == 0 /\ a_239^0-a_239^post10 == 0 /\ 1+l_143^0-l_203^post10 <= 0 /\ t_24^0-t_24^post10 == 0 /\ -a_76^post10+a_76^0 == 0 /\ -a_158^0 <= 0 /\ -y_20^post10+y_20^0 == 0 /\ -a_204^post10+a_158^post10 <= 0 /\ -i_187^post10+i_187^0 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ -l_143^post10+l_203^post10 <= 0 /\ a_264^0-a_264^post10 == 0 /\ i_98^0-i_98^post10 == 0 /\ -x_140^post10+x_140^0 == 0 /\ -rv_31^post10+rv_31^0 == 0 /\ -1-a_204^post10+a_158^0 <= 0 /\ -r_183^post10+r_183^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ a_204^post10-a_158^post10 <= 0 /\ st_16^0-st_16^post10 == 0 /\ l_143^post10-l_203^post10 <= 0 /\ -1-l_143^0+l_203^post10 <= 0), cost: 1 New rule: l9 -> l10 : rv_13^0'=rv_13^post10, a_158^0'=-1+a_158^0, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1+a_158^0, l_143^0'=1+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 1 Applied preprocessing Original rule: l10 -> l9 : a_264^0'=a_264^post11, l_27^0'=l_27^post11, i_187^0'=i_187^post11, t_32^0'=t_32^post11, rv_13^0'=rv_13^post11, y_20^0'=y_20^post11, a_158^0'=a_158^post11, x_195^0'=x_195^post11, i_98^0'=i_98^post11, h_15^0'=h_15^post11, r_57^0'=r_57^post11, r_135^0'=r_135^post11, x_140^0'=x_140^post11, st_16^0'=st_16^post11, a_76^0'=a_76^post11, a_239^0'=a_239^post11, x_21^0'=x_21^post11, l_203^0'=l_203^post11, i_115^0'=i_115^post11, rt_11^0'=rt_11^post11, r_37^0'=r_37^post11, a_123^0'=a_123^post11, x_17^0'=x_17^post11, t_24^0'=t_24^post11, f_190^0'=f_190^post11, a_290^0'=a_290^post11, nd_12^0'=nd_12^post11, i_28^0'=i_28^post11, tp_33^0'=tp_33^post11, rv_31^0'=rv_31^post11, a_204^0'=a_204^post11, x_19^0'=x_19^post11, l_143^0'=l_143^post11, h_30^0'=h_30^post11, r_92^0'=r_92^post11, r_183^0'=r_183^post11, x_14^0'=x_14^post11, st_29^0'=st_29^post11, ct_18^0'=ct_18^post11, (l_27^0-l_27^post11 == 0 /\ f_190^0-f_190^post11 == 0 /\ -x_17^post11+x_17^0 == 0 /\ r_37^0-r_37^post11 == 0 /\ -nd_12^post11+nd_12^0 == 0 /\ a_239^0-a_239^post11 == 0 /\ x_195^0-x_195^post11 == 0 /\ -h_30^post11+h_30^0 == 0 /\ rv_13^0-rv_13^post11 == 0 /\ -a_123^post11+a_123^0 == 0 /\ r_57^0-r_57^post11 == 0 /\ i_115^0-i_115^post11 == 0 /\ -a_76^post11+a_76^0 == 0 /\ y_20^0-y_20^post11 == 0 /\ x_21^0-x_21^post11 == 0 /\ t_24^0-t_24^post11 == 0 /\ -l_143^post11+l_143^0 == 0 /\ -x_140^post11+x_140^0 == 0 /\ r_135^0-r_135^post11 == 0 /\ st_16^0-st_16^post11 == 0 /\ -r_183^post11+r_183^0 == 0 /\ -i_28^post11+i_28^0 == 0 /\ -rv_31^post11+rv_31^0 == 0 /\ a_264^0-a_264^post11 == 0 /\ -x_14^post11+x_14^0 == 0 /\ l_203^0-l_203^post11 == 0 /\ h_15^0-h_15^post11 == 0 /\ -a_204^post11+a_204^0 == 0 /\ -st_29^post11+st_29^0 == 0 /\ -r_92^post11+r_92^0 == 0 /\ i_187^0-i_187^post11 == 0 /\ -i_98^post11+i_98^0 == 0 /\ a_290^0-a_290^post11 == 0 /\ -ct_18^post11+ct_18^0 == 0 /\ rt_11^0-rt_11^post11 == 0 /\ tp_33^0-tp_33^post11 == 0 /\ a_158^0-a_158^post11 == 0 /\ -x_19^post11+x_19^0 == 0 /\ t_32^0-t_32^post11 == 0), cost: 1 New rule: l10 -> l9 : TRUE, cost: 1 Applied preprocessing Original rule: l8 -> l9 : a_264^0'=a_264^post15, l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, y_20^0'=y_20^post15, a_158^0'=a_158^post15, x_195^0'=x_195^post15, i_98^0'=i_98^post15, h_15^0'=h_15^post15, r_57^0'=r_57^post15, r_135^0'=r_135^post15, x_140^0'=x_140^post15, st_16^0'=st_16^post15, a_76^0'=a_76^post15, a_239^0'=a_239^post15, x_21^0'=x_21^post15, l_203^0'=l_203^post15, i_115^0'=i_115^post15, rt_11^0'=rt_11^post15, r_37^0'=r_37^post15, a_123^0'=a_123^post15, x_17^0'=x_17^post15, t_24^0'=t_24^post15, f_190^0'=f_190^post15, a_290^0'=a_290^post15, nd_12^0'=nd_12^post15, i_28^0'=i_28^post15, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, a_204^0'=a_204^post15, x_19^0'=x_19^post15, l_143^0'=l_143^post15, h_30^0'=h_30^post15, r_92^0'=r_92^post15, r_183^0'=r_183^post15, x_14^0'=x_14^post15, st_29^0'=st_29^post15, ct_18^0'=ct_18^post15, (0 == 0 /\ -a_158^0+i_28^post15 <= 0 /\ 1-rv_13^post15 <= 0 /\ -x_140^post15+x_140^0 == 0 /\ h_15^post15-x_14^post15 <= 0 /\ x_21^0-x_21^post15 == 0 /\ rv_13^post15-i_28^post15 <= 0 /\ -x_19^post15+x_19^0 == 0 /\ -l_203^post15+l_203^0 == 0 /\ a_264^0-a_264^post15 == 0 /\ -l_143^post15+l_143^0 == 0 /\ -a_204^post15+a_204^0 == 0 /\ -r_92^post15+r_92^0 == 0 /\ -f_190^post15+f_190^0 == 0 /\ a_158^0-i_28^post15 <= 0 /\ x_195^0-x_195^post15 == 0 /\ h_15^post15-rt_11^11 == 0 /\ -h_15^post15+x_14^post15 <= 0 /\ -h_15^post15+x_14^post15 == 0 /\ 2-rv_13^post15 <= 0 /\ -i_115^post15+i_115^0 == 0 /\ -l_143^0 <= 0 /\ -x_17^post15+x_17^0 == 0 /\ -r_57^post15+r_57^0 == 0 /\ -y_20^post15+y_20^0 == 0 /\ -ct_18^post15+ct_18^0 == 0 /\ st_29^110-h_30^0 == 0 /\ i_98^0-i_98^post15 == 0 /\ st_16^0-st_16^post15 == 0 /\ -r_135^post15+r_135^0 == 0 /\ a_158^0-a_158^post15 == 0 /\ l_27^0-i_28^0 <= 0 /\ a_239^0-a_239^post15 == 0 /\ -nd_12^post15+nd_12^0 == 0 /\ -i_28^0 <= 0 /\ -r_37^post15+r_37^0 == 0 /\ -r_183^post15+r_183^0 == 0 /\ -st_29^110+rt_11^11 == 0 /\ l_143^0 <= 0 /\ rv_13^post15-i_187^post15 <= 0 /\ a_76^0-a_76^post15 == 0 /\ t_24^0-t_24^post15 == 0 /\ a_290^0-a_290^post15 == 0 /\ a_123^0-a_123^post15 == 0), cost: 1 New rule: l8 -> l9 : l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, h_15^0'=h_30^0, rt_11^0'=rt_11^post15, i_28^0'=a_158^0, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, h_30^0'=h_30^post15, x_14^0'=h_30^0, st_29^0'=st_29^post15, (-a_158^0+rv_13^post15 <= 0 /\ l_27^0-i_28^0 <= 0 /\ -i_28^0 <= 0 /\ l_143^0 == 0 /\ rv_13^post15-i_187^post15 <= 0 /\ -2+rv_13^post15 >= 0), cost: 1 Applied preprocessing Original rule: l8 -> l13 : a_264^0'=a_264^post16, l_27^0'=l_27^post16, i_187^0'=i_187^post16, t_32^0'=t_32^post16, rv_13^0'=rv_13^post16, y_20^0'=y_20^post16, a_158^0'=a_158^post16, x_195^0'=x_195^post16, i_98^0'=i_98^post16, h_15^0'=h_15^post16, r_57^0'=r_57^post16, r_135^0'=r_135^post16, x_140^0'=x_140^post16, st_16^0'=st_16^post16, a_76^0'=a_76^post16, a_239^0'=a_239^post16, x_21^0'=x_21^post16, l_203^0'=l_203^post16, i_115^0'=i_115^post16, rt_11^0'=rt_11^post16, r_37^0'=r_37^post16, a_123^0'=a_123^post16, x_17^0'=x_17^post16, t_24^0'=t_24^post16, f_190^0'=f_190^post16, a_290^0'=a_290^post16, nd_12^0'=nd_12^post16, i_28^0'=i_28^post16, tp_33^0'=tp_33^post16, rv_31^0'=rv_31^post16, a_204^0'=a_204^post16, x_19^0'=x_19^post16, l_143^0'=l_143^post16, h_30^0'=h_30^post16, r_92^0'=r_92^post16, r_183^0'=r_183^post16, x_14^0'=x_14^post16, st_29^0'=st_29^post16, ct_18^0'=ct_18^post16, (0 == 0 /\ l_27^0-l_27^post16 == 0 /\ 1+i_98^post16-i_28^post16 <= 0 /\ h_15^0-h_15^post16 == 0 /\ -rv_31^post16+rv_31^0 == 0 /\ t_24^0-t_24^post16 == 0 /\ x_195^0-x_195^post16 == 0 /\ -x_17^post16+x_17^0 == 0 /\ i_187^0-i_187^post16 == 0 /\ r_57^0-r_57^post16 == 0 /\ i_115^0-i_115^post16 == 0 /\ -1-i_28^0+i_28^post16 == 0 /\ -st_29^post16+st_29^0 == 0 /\ r_135^0-r_135^post16 == 0 /\ h_30^post16-t_32^post16 == 0 /\ -ct_18^post16+ct_18^0 == 0 /\ a_239^0-a_239^post16 == 0 /\ -r_183^post16+r_183^0 == 0 /\ -x_19^post16+x_19^0 == 0 /\ -nd_12^post16+nd_12^0 == 0 /\ -x_140^post16+x_140^0 == 0 /\ -a_204^post16+a_204^0 == 0 /\ -st_16^post16+st_16^0 == 0 /\ l_143^0-l_143^post16 == 0 /\ rv_13^0-rv_13^post16 == 0 /\ -1-i_98^post16+i_28^post16 <= 0 /\ -f_190^post16+f_190^0 == 0 /\ -tp_33^0+t_32^post16 == 0 /\ a_264^0-a_264^post16 == 0 /\ -r_37^post16+r_37^0 == 0 /\ 1+i_98^post16-l_27^0 <= 0 /\ x_21^0-x_21^post16 == 0 /\ -x_14^post16+x_14^0 == 0 /\ -i_28^0 <= 0 /\ -l_203^post16+l_203^0 == 0 /\ -a_76^post16+a_76^0 == 0 /\ rt_11^0-rt_11^post16 == 0 /\ a_290^0-a_290^post16 == 0 /\ a_158^0-a_158^post16 == 0 /\ a_123^0-a_123^post16 == 0 /\ y_20^0-y_20^post16 == 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 New rule: l8 -> l13 : t_32^0'=tp_33^0, i_98^0'=i_28^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^0, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 Applied preprocessing Original rule: l13 -> l8 : a_264^0'=a_264^post17, l_27^0'=l_27^post17, i_187^0'=i_187^post17, t_32^0'=t_32^post17, rv_13^0'=rv_13^post17, y_20^0'=y_20^post17, a_158^0'=a_158^post17, x_195^0'=x_195^post17, i_98^0'=i_98^post17, h_15^0'=h_15^post17, r_57^0'=r_57^post17, r_135^0'=r_135^post17, x_140^0'=x_140^post17, st_16^0'=st_16^post17, a_76^0'=a_76^post17, a_239^0'=a_239^post17, x_21^0'=x_21^post17, l_203^0'=l_203^post17, i_115^0'=i_115^post17, rt_11^0'=rt_11^post17, r_37^0'=r_37^post17, a_123^0'=a_123^post17, x_17^0'=x_17^post17, t_24^0'=t_24^post17, f_190^0'=f_190^post17, a_290^0'=a_290^post17, nd_12^0'=nd_12^post17, i_28^0'=i_28^post17, tp_33^0'=tp_33^post17, rv_31^0'=rv_31^post17, a_204^0'=a_204^post17, x_19^0'=x_19^post17, l_143^0'=l_143^post17, h_30^0'=h_30^post17, r_92^0'=r_92^post17, r_183^0'=r_183^post17, x_14^0'=x_14^post17, st_29^0'=st_29^post17, ct_18^0'=ct_18^post17, (-h_30^post17+h_30^0 == 0 /\ -ct_18^post17+ct_18^0 == 0 /\ -nd_12^post17+nd_12^0 == 0 /\ l_27^0-l_27^post17 == 0 /\ st_16^0-st_16^post17 == 0 /\ i_187^0-i_187^post17 == 0 /\ -l_143^post17+l_143^0 == 0 /\ -r_37^post17+r_37^0 == 0 /\ -x_140^post17+x_140^0 == 0 /\ r_57^0-r_57^post17 == 0 /\ i_115^0-i_115^post17 == 0 /\ h_15^0-h_15^post17 == 0 /\ -a_76^post17+a_76^0 == 0 /\ y_20^0-y_20^post17 == 0 /\ -st_29^post17+st_29^0 == 0 /\ -tp_33^post17+tp_33^0 == 0 /\ a_290^0-a_290^post17 == 0 /\ x_14^0-x_14^post17 == 0 /\ rv_13^0-rv_13^post17 == 0 /\ -x_19^post17+x_19^0 == 0 /\ -r_183^post17+r_183^0 == 0 /\ -a_204^post17+a_204^0 == 0 /\ -r_92^post17+r_92^0 == 0 /\ x_195^0-x_195^post17 == 0 /\ a_123^0-a_123^post17 == 0 /\ -t_24^post17+t_24^0 == 0 /\ a_158^0-a_158^post17 == 0 /\ t_32^0-t_32^post17 == 0 /\ x_21^0-x_21^post17 == 0 /\ r_135^0-r_135^post17 == 0 /\ -i_98^post17+i_98^0 == 0 /\ -f_190^post17+f_190^0 == 0 /\ rt_11^0-rt_11^post17 == 0 /\ -x_17^post17+x_17^0 == 0 /\ a_239^0-a_239^post17 == 0 /\ -rv_31^post17+rv_31^0 == 0 /\ a_264^0-a_264^post17 == 0 /\ -l_203^post17+l_203^0 == 0 /\ i_28^0-i_28^post17 == 0), cost: 1 New rule: l13 -> l8 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l7 : a_264^0'=a_264^post19, l_27^0'=l_27^post19, i_187^0'=i_187^post19, t_32^0'=t_32^post19, rv_13^0'=rv_13^post19, y_20^0'=y_20^post19, a_158^0'=a_158^post19, x_195^0'=x_195^post19, i_98^0'=i_98^post19, h_15^0'=h_15^post19, r_57^0'=r_57^post19, r_135^0'=r_135^post19, x_140^0'=x_140^post19, st_16^0'=st_16^post19, a_76^0'=a_76^post19, a_239^0'=a_239^post19, x_21^0'=x_21^post19, l_203^0'=l_203^post19, i_115^0'=i_115^post19, rt_11^0'=rt_11^post19, r_37^0'=r_37^post19, a_123^0'=a_123^post19, x_17^0'=x_17^post19, t_24^0'=t_24^post19, f_190^0'=f_190^post19, a_290^0'=a_290^post19, nd_12^0'=nd_12^post19, i_28^0'=i_28^post19, tp_33^0'=tp_33^post19, rv_31^0'=rv_31^post19, a_204^0'=a_204^post19, x_19^0'=x_19^post19, l_143^0'=l_143^post19, h_30^0'=h_30^post19, r_92^0'=r_92^post19, r_183^0'=r_183^post19, x_14^0'=x_14^post19, st_29^0'=st_29^post19, ct_18^0'=ct_18^post19, (0 == 0 /\ -rv_31^post19+t_32^post19 <= 0 /\ -x_21^post19+x_21^0 == 0 /\ -x_14^post19+x_14^0 == 0 /\ r_57^0-r_57^post19 == 0 /\ -i_115^post19+i_115^0 == 0 /\ y_20^0-y_20^post19 == 0 /\ -x_195^post19+x_195^0 == 0 /\ l_143^0-l_143^post19 == 0 /\ -h_30^post19+t_32^post19 <= 0 /\ -1+i_28^post19-i_28^0 == 0 /\ h_30^post19-rv_31^post19 <= 0 /\ -a_290^post19+a_290^0 == 0 /\ -l_27^0+rv_13^post19 <= 0 /\ rv_31^post19-t_32^post19 <= 0 /\ a_76^0-a_76^post19 == 0 /\ -a_239^post19+a_239^0 == 0 /\ -st_29^post19+st_29^0 == 0 /\ -ct_18^post19+ct_18^0 == 0 /\ a_123^0-a_123^post19 == 0 /\ r_135^0-r_135^post19 == 0 /\ h_30^post19-t_32^post19 <= 0 /\ h_30^post19-t_32^post19 == 0 /\ -nd_12^post19+nd_12^0 == 0 /\ -h_30^post19+rv_31^post19 <= 0 /\ -st_16^post19+st_16^0 == 0 /\ -x_19^post19+x_19^0 == 0 /\ l_27^0-l_27^post19 == 0 /\ l_27^0-rv_13^post19 <= 0 /\ a_264^0-a_264^post19 == 0 /\ -r_92^post19+r_92^0 == 0 /\ -t_24^post19+t_24^0 == 0 /\ h_15^0-h_15^post19 == 0 /\ -r_37^post19+r_37^0 == 0 /\ i_98^0-i_98^post19 == 0 /\ x_17^0-x_17^post19 == 0 /\ x_140^0-x_140^post19 == 0 /\ -rt_11^post19+rt_11^0 == 0 /\ -f_190^post19+f_190^0 == 0 /\ -l_203^post19+l_203^0 == 0 /\ -tp_33^0+t_32^post19 == 0 /\ -r_183^post19+r_183^0 == 0 /\ 1-l_27^0 <= 0 /\ a_158^0-a_158^post19 == 0 /\ i_187^0-i_187^post19 == 0 /\ 1-i_28^post19 <= 0 /\ -1+i_28^post19 <= 0 /\ 1-l_27^0+i_28^0 <= 0 /\ -a_204^post19+a_204^0 == 0), cost: 1 New rule: l1 -> l7 : t_32^0'=tp_33^0, rv_13^0'=l_27^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post19, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, (i_28^0 == 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 Applied preprocessing Original rule: l14 -> l0 : a_264^0'=a_264^post20, l_27^0'=l_27^post20, i_187^0'=i_187^post20, t_32^0'=t_32^post20, rv_13^0'=rv_13^post20, y_20^0'=y_20^post20, a_158^0'=a_158^post20, x_195^0'=x_195^post20, i_98^0'=i_98^post20, h_15^0'=h_15^post20, r_57^0'=r_57^post20, r_135^0'=r_135^post20, x_140^0'=x_140^post20, st_16^0'=st_16^post20, a_76^0'=a_76^post20, a_239^0'=a_239^post20, x_21^0'=x_21^post20, l_203^0'=l_203^post20, i_115^0'=i_115^post20, rt_11^0'=rt_11^post20, r_37^0'=r_37^post20, a_123^0'=a_123^post20, x_17^0'=x_17^post20, t_24^0'=t_24^post20, f_190^0'=f_190^post20, a_290^0'=a_290^post20, nd_12^0'=nd_12^post20, i_28^0'=i_28^post20, tp_33^0'=tp_33^post20, rv_31^0'=rv_31^post20, a_204^0'=a_204^post20, x_19^0'=x_19^post20, l_143^0'=l_143^post20, h_30^0'=h_30^post20, r_92^0'=r_92^post20, r_183^0'=r_183^post20, x_14^0'=x_14^post20, st_29^0'=st_29^post20, ct_18^0'=ct_18^post20, (a_204^0-a_204^post20 == 0 /\ -nd_12^post20+nd_12^0 == 0 /\ -st_29^post20+st_29^0 == 0 /\ l_27^0-l_27^post20 == 0 /\ r_57^0-r_57^post20 == 0 /\ -ct_18^post20+ct_18^0 == 0 /\ rv_13^0-rv_13^post20 == 0 /\ x_195^0-x_195^post20 == 0 /\ a_76^0-a_76^post20 == 0 /\ a_123^0-a_123^post20 == 0 /\ i_98^0-i_98^post20 == 0 /\ -st_16^post20+st_16^0 == 0 /\ x_17^0-x_17^post20 == 0 /\ x_19^0-x_19^post20 == 0 /\ -r_37^post20+r_37^0 == 0 /\ i_187^0-i_187^post20 == 0 /\ -rt_11^post20+rt_11^0 == 0 /\ y_20^0-y_20^post20 == 0 /\ r_135^0-r_135^post20 == 0 /\ x_140^0-x_140^post20 == 0 /\ h_15^0-h_15^post20 == 0 /\ -h_30^post20+h_30^0 == 0 /\ -r_183^post20+r_183^0 == 0 /\ i_115^0-i_115^post20 == 0 /\ -a_239^post20+a_239^0 == 0 /\ -tp_33^post20+tp_33^0 == 0 /\ a_264^0-a_264^post20 == 0 /\ l_203^0-l_203^post20 == 0 /\ -t_32^post20+t_32^0 == 0 /\ -r_92^post20+r_92^0 == 0 /\ a_158^0-a_158^post20 == 0 /\ -x_21^post20+x_21^0 == 0 /\ -t_24^post20+t_24^0 == 0 /\ -a_290^post20+a_290^0 == 0 /\ rv_31^0-rv_31^post20 == 0 /\ -x_14^post20+x_14^0 == 0 /\ -f_190^post20+f_190^0 == 0 /\ -i_28^post20+i_28^0 == 0 /\ -l_143^post20+l_143^0 == 0), cost: 1 New rule: l14 -> l0 : TRUE, cost: 1 Simplified rules Start location: l14 21: l0 -> l1 : l_27^0'=nd_12^10, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=0, h_30^0'=0, 0 == 0, cost: 1 32: l1 -> l7 : t_32^0'=tp_33^0, rv_13^0'=l_27^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post19, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, (i_28^0 == 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 22: l2 -> l4 : a_264^0'=-1+a_264^0, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1+a_264^0, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 == 0 /\ -2+rv_13^post2 >= 0), cost: 1 23: l4 -> l2 : TRUE, cost: 1 24: l6 -> l2 : rv_13^0'=rv_13^post6, h_15^0'=x_21^0, a_239^0'=a_264^0, x_17^0'=x_21^0, t_24^0'=x_21^0, x_19^0'=x_21^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (y_20^0 == 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0), cost: 1 25: l7 -> l8 : t_32^0'=tp_33^0, rv_13^0'=l_27^0, r_57^0'=r_57^post8, a_76^0'=2, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, (-2+l_27^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 29: l8 -> l9 : l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, h_15^0'=h_30^0, rt_11^0'=rt_11^post15, i_28^0'=a_158^0, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, h_30^0'=h_30^post15, x_14^0'=h_30^0, st_29^0'=st_29^post15, (-a_158^0+rv_13^post15 <= 0 /\ l_27^0-i_28^0 <= 0 /\ -i_28^0 <= 0 /\ l_143^0 == 0 /\ rv_13^post15-i_187^post15 <= 0 /\ -2+rv_13^post15 >= 0), cost: 1 30: l8 -> l13 : t_32^0'=tp_33^0, i_98^0'=i_28^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^0, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 26: l9 -> l6 : rv_13^0'=rv_13^post9, y_20^0'=0, x_21^0'=h_15^0, x_17^0'=h_15^0, x_19^0'=h_15^0, ct_18^0'=0, (-2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 1 27: l9 -> l10 : rv_13^0'=rv_13^post10, a_158^0'=-1+a_158^0, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1+a_158^0, l_143^0'=1+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 1 28: l10 -> l9 : TRUE, cost: 1 31: l13 -> l8 : TRUE, cost: 1 33: l14 -> l0 : TRUE, cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l14 -> l0 : TRUE, cost: 1 Second rule: l0 -> l1 : l_27^0'=nd_12^10, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=0, h_30^0'=0, 0 == 0, cost: 1 New rule: l14 -> l1 : l_27^0'=nd_12^10, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=0, h_30^0'=0, 0 == 0, cost: 2 Applied deletion Removed the following rules: 21 33 Eliminating location l1 by chaining: Applied chaining First rule: l14 -> l1 : l_27^0'=nd_12^10, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=0, h_30^0'=0, 0 == 0, cost: 2 Second rule: l1 -> l7 : t_32^0'=tp_33^0, rv_13^0'=l_27^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post19, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, (i_28^0 == 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 New rule: l14 -> l7 : l_27^0'=nd_12^10, t_32^0'=tp_33^0, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=1, tp_33^0'=tp_33^post19, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, (0 == 0 /\ 1-nd_12^10 <= 0), cost: 3 Applied simplification Original rule: l14 -> l7 : l_27^0'=nd_12^10, t_32^0'=tp_33^0, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=1, tp_33^0'=tp_33^post19, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, (0 == 0 /\ 1-nd_12^10 <= 0), cost: 3 New rule: l14 -> l7 : l_27^0'=nd_12^10, t_32^0'=tp_33^0, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=1, tp_33^0'=tp_33^post19, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, -1+nd_12^10 >= 0, cost: 3 Applied deletion Removed the following rules: 32 34 Eliminating location l7 by chaining: Applied chaining First rule: l14 -> l7 : l_27^0'=nd_12^10, t_32^0'=tp_33^0, rv_13^0'=nd_12^10, nd_12^0'=nd_12^post0, i_28^0'=1, tp_33^0'=tp_33^post19, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, -1+nd_12^10 >= 0, cost: 3 Second rule: l7 -> l8 : t_32^0'=tp_33^0, rv_13^0'=l_27^0, r_57^0'=r_57^post8, a_76^0'=2, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^0, h_30^0'=tp_33^0, (-2+l_27^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 New rule: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post19, rv_13^0'=nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post19, (-1+nd_12^10 >= 0 /\ 2-nd_12^10 <= 0 /\ -2+nd_12^10 >= 0), cost: 4 Applied simplification Original rule: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post19, rv_13^0'=nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post19, (-1+nd_12^10 >= 0 /\ 2-nd_12^10 <= 0 /\ -2+nd_12^10 >= 0), cost: 4 New rule: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post19, rv_13^0'=nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post19, -2+nd_12^10 >= 0, cost: 4 Applied deletion Removed the following rules: 25 35 Eliminating location l13 by chaining: Applied chaining First rule: l8 -> l13 : t_32^0'=tp_33^0, i_98^0'=i_28^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^0, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 1 Second rule: l13 -> l8 : TRUE, cost: 1 New rule: l8 -> l8 : t_32^0'=tp_33^0, i_98^0'=i_28^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^0, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 2 Applied deletion Removed the following rules: 30 31 Eliminating location l6 by chaining: Applied chaining First rule: l9 -> l6 : rv_13^0'=rv_13^post9, y_20^0'=0, x_21^0'=h_15^0, x_17^0'=h_15^0, x_19^0'=h_15^0, ct_18^0'=0, (-2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 1 Second rule: l6 -> l2 : rv_13^0'=rv_13^post6, h_15^0'=x_21^0, a_239^0'=a_264^0, x_17^0'=x_21^0, t_24^0'=x_21^0, x_19^0'=x_21^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (y_20^0 == 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0), cost: 1 New rule: l9 -> l2 : rv_13^0'=rv_13^post6, y_20^0'=0, h_15^0'=h_15^0, a_239^0'=a_264^0, x_21^0'=h_15^0, x_17^0'=h_15^0, t_24^0'=h_15^0, x_19^0'=h_15^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (0 == 0 /\ -2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 2 Applied simplification Original rule: l9 -> l2 : rv_13^0'=rv_13^post6, y_20^0'=0, h_15^0'=h_15^0, a_239^0'=a_264^0, x_21^0'=h_15^0, x_17^0'=h_15^0, t_24^0'=h_15^0, x_19^0'=h_15^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (0 == 0 /\ -2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 2 New rule: l9 -> l2 : rv_13^0'=rv_13^post6, y_20^0'=0, h_15^0'=h_15^0, a_239^0'=a_264^0, x_21^0'=h_15^0, x_17^0'=h_15^0, t_24^0'=h_15^0, x_19^0'=h_15^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (-2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 2 Applied deletion Removed the following rules: 24 26 Eliminating location l10 by chaining: Applied chaining First rule: l9 -> l10 : rv_13^0'=rv_13^post10, a_158^0'=-1+a_158^0, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1+a_158^0, l_143^0'=1+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 1 Second rule: l10 -> l9 : TRUE, cost: 1 New rule: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=-1+a_158^0, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1+a_158^0, l_143^0'=1+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 2 Applied deletion Removed the following rules: 27 28 Eliminating location l4 by chaining: Applied chaining First rule: l2 -> l4 : a_264^0'=-1+a_264^0, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1+a_264^0, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 == 0 /\ -2+rv_13^post2 >= 0), cost: 1 Second rule: l4 -> l2 : TRUE, cost: 1 New rule: l2 -> l2 : a_264^0'=-1+a_264^0, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1+a_264^0, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 == 0 /\ -2+rv_13^post2 >= 0), cost: 2 Applied deletion Removed the following rules: 22 23 Eliminated locations on linear paths Start location: l14 40: l2 -> l2 : a_264^0'=-1+a_264^0, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1+a_264^0, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 == 0 /\ -2+rv_13^post2 >= 0), cost: 2 29: l8 -> l9 : l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, h_15^0'=h_30^0, rt_11^0'=rt_11^post15, i_28^0'=a_158^0, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, h_30^0'=h_30^post15, x_14^0'=h_30^0, st_29^0'=st_29^post15, (-a_158^0+rv_13^post15 <= 0 /\ l_27^0-i_28^0 <= 0 /\ -i_28^0 <= 0 /\ l_143^0 == 0 /\ rv_13^post15-i_187^post15 <= 0 /\ -2+rv_13^post15 >= 0), cost: 1 37: l8 -> l8 : t_32^0'=tp_33^0, i_98^0'=i_28^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^0, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 2 38: l9 -> l2 : rv_13^0'=rv_13^post6, y_20^0'=0, h_15^0'=h_15^0, a_239^0'=a_264^0, x_21^0'=h_15^0, x_17^0'=h_15^0, t_24^0'=h_15^0, x_19^0'=h_15^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (-2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 2 39: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=-1+a_158^0, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1+a_158^0, l_143^0'=1+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 2 36: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post19, rv_13^0'=nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post19, -2+nd_12^10 >= 0, cost: 4 Applied acceleration Original rule: l2 -> l2 : a_264^0'=-1+a_264^0, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1+a_264^0, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 == 0 /\ -2+rv_13^post2 >= 0), cost: 2 New rule: l2 -> l2 : a_264^0'=a_264^0-n, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=a_264^0-n, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (y_20^0 >= 0 /\ -y_20^0 >= 0 /\ 1+a_264^0-n >= 0 /\ -2+rv_13^post2 >= 0 /\ -1+n >= 0), cost: 2*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_ODleoe.txt Applied instantiation Original rule: l2 -> l2 : a_264^0'=a_264^0-n, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=a_264^0-n, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (y_20^0 >= 0 /\ -y_20^0 >= 0 /\ 1+a_264^0-n >= 0 /\ -2+rv_13^post2 >= 0 /\ -1+n >= 0), cost: 2*n New rule: l2 -> l2 : a_264^0'=-1, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (0 >= 0 /\ a_264^0 >= 0 /\ y_20^0 >= 0 /\ -y_20^0 >= 0 /\ -2+rv_13^post2 >= 0), cost: 2+2*a_264^0 Applied simplification Original rule: l2 -> l2 : a_264^0'=-1, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (0 >= 0 /\ a_264^0 >= 0 /\ y_20^0 >= 0 /\ -y_20^0 >= 0 /\ -2+rv_13^post2 >= 0), cost: 2+2*a_264^0 New rule: l2 -> l2 : a_264^0'=-1, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 <= 0 /\ y_20^0 >= 0 /\ -2+rv_13^post2 >= 0), cost: 2+2*a_264^0 Applied deletion Removed the following rules: 40 Applied acceleration Original rule: l8 -> l8 : t_32^0'=tp_33^0, i_98^0'=i_28^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^0, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 2 New rule: l8 -> l8 : t_32^0'=tp_33^post16, i_98^0'=-1+n0+i_28^0, i_28^0'=n0+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ l_27^0-n0-i_28^0 >= 0 /\ -2+n0 >= 0), cost: 2*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_cHONkc.txt Applied instantiation Original rule: l8 -> l8 : t_32^0'=tp_33^post16, i_98^0'=-1+n0+i_28^0, i_28^0'=n0+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ l_27^0-n0-i_28^0 >= 0 /\ -2+n0 >= 0), cost: 2*n0 New rule: l8 -> l8 : t_32^0'=tp_33^post16, i_98^0'=-1+l_27^0, i_28^0'=l_27^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, (0 >= 0 /\ -2+l_27^0-i_28^0 >= 0 /\ i_28^0 >= 0), cost: 2*l_27^0-2*i_28^0 Applied simplification Original rule: l8 -> l8 : t_32^0'=tp_33^post16, i_98^0'=-1+l_27^0, i_28^0'=l_27^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, (0 >= 0 /\ -2+l_27^0-i_28^0 >= 0 /\ i_28^0 >= 0), cost: 2*l_27^0-2*i_28^0 New rule: l8 -> l8 : t_32^0'=tp_33^post16, i_98^0'=-1+l_27^0, i_28^0'=l_27^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, (-2+l_27^0-i_28^0 >= 0 /\ i_28^0 >= 0), cost: 2*l_27^0-2*i_28^0 Applied acceleration Original rule: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=-1+a_158^0, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1+a_158^0, l_143^0'=1+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 2 New rule: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=a_158^0-n1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=l_143^0+n1, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=a_158^0-n1, l_143^0'=l_143^0+n1, (-1+n1 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0 /\ 1+a_158^0-n1 >= 0), cost: 2*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_FNEnPo.txt Applied instantiation Original rule: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=a_158^0-n1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=l_143^0+n1, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=a_158^0-n1, l_143^0'=l_143^0+n1, (-1+n1 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0 /\ 1+a_158^0-n1 >= 0), cost: 2*n1 New rule: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=-1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+a_158^0+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1, l_143^0'=1+a_158^0+l_143^0, (0 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 2+2*a_158^0 Applied simplification Original rule: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=-1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+a_158^0+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1, l_143^0'=1+a_158^0+l_143^0, (0 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 2+2*a_158^0 New rule: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=-1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+a_158^0+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1, l_143^0'=1+a_158^0+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 2+2*a_158^0 Applied deletion Removed the following rules: 39 Accelerated simple loops Start location: l14 42: l2 -> l2 : a_264^0'=-1, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 <= 0 /\ y_20^0 >= 0 /\ -2+rv_13^post2 >= 0), cost: 2+2*a_264^0 29: l8 -> l9 : l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, h_15^0'=h_30^0, rt_11^0'=rt_11^post15, i_28^0'=a_158^0, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, h_30^0'=h_30^post15, x_14^0'=h_30^0, st_29^0'=st_29^post15, (-a_158^0+rv_13^post15 <= 0 /\ l_27^0-i_28^0 <= 0 /\ -i_28^0 <= 0 /\ l_143^0 == 0 /\ rv_13^post15-i_187^post15 <= 0 /\ -2+rv_13^post15 >= 0), cost: 1 37: l8 -> l8 : t_32^0'=tp_33^0, i_98^0'=i_28^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^0, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 2 44: l8 -> l8 : t_32^0'=tp_33^post16, i_98^0'=-1+l_27^0, i_28^0'=l_27^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, (-2+l_27^0-i_28^0 >= 0 /\ i_28^0 >= 0), cost: 2*l_27^0-2*i_28^0 38: l9 -> l2 : rv_13^0'=rv_13^post6, y_20^0'=0, h_15^0'=h_15^0, a_239^0'=a_264^0, x_21^0'=h_15^0, x_17^0'=h_15^0, t_24^0'=h_15^0, x_19^0'=h_15^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (-2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 2 46: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=-1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+a_158^0+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1, l_143^0'=1+a_158^0+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 2+2*a_158^0 36: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post19, rv_13^0'=nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post19, -2+nd_12^10 >= 0, cost: 4 Applied chaining First rule: l9 -> l2 : rv_13^0'=rv_13^post6, y_20^0'=0, h_15^0'=h_15^0, a_239^0'=a_264^0, x_21^0'=h_15^0, x_17^0'=h_15^0, t_24^0'=h_15^0, x_19^0'=h_15^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (-2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 2 Second rule: l2 -> l2 : a_264^0'=-1, rv_13^0'=rv_13^post2, h_15^0'=h_15^post2, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=x_21^0, a_290^0'=-1, x_19^0'=h_15^post2, x_14^0'=0, ct_18^0'=y_20^0, (a_264^0 >= 0 /\ y_20^0 <= 0 /\ y_20^0 >= 0 /\ -2+rv_13^post2 >= 0), cost: 2+2*a_264^0 New rule: l9 -> l2 : a_264^0'=-1, rv_13^0'=rv_13^post2, y_20^0'=0, h_15^0'=h_15^post2, a_239^0'=a_264^0, x_21^0'=h_15^0, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=h_15^0, a_290^0'=-1, x_19^0'=h_15^post2, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (a_264^0 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post2 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 4+2*a_264^0 Applied deletion Removed the following rules: 42 Applied chaining First rule: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post19, rv_13^0'=nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post19, -2+nd_12^10 >= 0, cost: 4 Second rule: l8 -> l8 : t_32^0'=tp_33^0, i_98^0'=i_28^0, i_28^0'=1+i_28^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^0, r_92^0'=r_92^post16, (i_28^0 >= 0 /\ 1-l_27^0+i_28^0 <= 0), cost: 2 New rule: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post8, rv_13^0'=nd_12^10, i_98^0'=2, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=3, tp_33^0'=tp_33^post16, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post8, r_92^0'=r_92^post16, -3+nd_12^10 >= 0, cost: 6 Applied chaining First rule: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post19, rv_13^0'=nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post19, -2+nd_12^10 >= 0, cost: 4 Second rule: l8 -> l8 : t_32^0'=tp_33^post16, i_98^0'=-1+l_27^0, i_28^0'=l_27^0, tp_33^0'=tp_33^post16, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, (-2+l_27^0-i_28^0 >= 0 /\ i_28^0 >= 0), cost: 2*l_27^0-2*i_28^0 New rule: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post16, rv_13^0'=nd_12^10, i_98^0'=-1+nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=nd_12^10, tp_33^0'=tp_33^post16, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, -4+nd_12^10 >= 0, cost: 2*nd_12^10 Applied deletion Removed the following rules: 37 44 Applied chaining First rule: l8 -> l9 : l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, h_15^0'=h_30^0, rt_11^0'=rt_11^post15, i_28^0'=a_158^0, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, h_30^0'=h_30^post15, x_14^0'=h_30^0, st_29^0'=st_29^post15, (-a_158^0+rv_13^post15 <= 0 /\ l_27^0-i_28^0 <= 0 /\ -i_28^0 <= 0 /\ l_143^0 == 0 /\ rv_13^post15-i_187^post15 <= 0 /\ -2+rv_13^post15 >= 0), cost: 1 Second rule: l9 -> l9 : rv_13^0'=rv_13^post10, a_158^0'=-1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+a_158^0+l_143^0, r_37^0'=r_37^post10, f_190^0'=x_14^0, a_204^0'=-1, l_143^0'=1+a_158^0+l_143^0, (a_158^0 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_143^0 >= 0), cost: 2+2*a_158^0 New rule: l8 -> l9 : l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post10, a_158^0'=-1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+a_158^0+l_143^0, rt_11^0'=rt_11^post15, r_37^0'=r_37^post10, f_190^0'=h_30^0, i_28^0'=a_158^0, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, a_204^0'=-1, l_143^0'=1+a_158^0+l_143^0, h_30^0'=h_30^post15, x_14^0'=h_30^0, st_29^0'=st_29^post15, (-2+a_158^0 >= 0 /\ -2+i_187^post15 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_27^0-i_28^0 <= 0 /\ -i_28^0 <= 0 /\ l_143^0 == 0), cost: 3+2*a_158^0 Applied deletion Removed the following rules: 46 Chained accelerated rules with incoming rules Start location: l14 29: l8 -> l9 : l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post15, h_15^0'=h_30^0, rt_11^0'=rt_11^post15, i_28^0'=a_158^0, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, h_30^0'=h_30^post15, x_14^0'=h_30^0, st_29^0'=st_29^post15, (-a_158^0+rv_13^post15 <= 0 /\ l_27^0-i_28^0 <= 0 /\ -i_28^0 <= 0 /\ l_143^0 == 0 /\ rv_13^post15-i_187^post15 <= 0 /\ -2+rv_13^post15 >= 0), cost: 1 50: l8 -> l9 : l_27^0'=l_27^post15, i_187^0'=i_187^post15, t_32^0'=t_32^post15, rv_13^0'=rv_13^post10, a_158^0'=-1, x_195^0'=x_195^post10, h_15^0'=h_15^post10, l_203^0'=1+a_158^0+l_143^0, rt_11^0'=rt_11^post15, r_37^0'=r_37^post10, f_190^0'=h_30^0, i_28^0'=a_158^0, tp_33^0'=tp_33^post15, rv_31^0'=rv_31^post15, a_204^0'=-1, l_143^0'=1+a_158^0+l_143^0, h_30^0'=h_30^post15, x_14^0'=h_30^0, st_29^0'=st_29^post15, (-2+a_158^0 >= 0 /\ -2+i_187^post15 >= 0 /\ -2+rv_13^post10 >= 0 /\ l_27^0-i_28^0 <= 0 /\ -i_28^0 <= 0 /\ l_143^0 == 0), cost: 3+2*a_158^0 38: l9 -> l2 : rv_13^0'=rv_13^post6, y_20^0'=0, h_15^0'=h_15^0, a_239^0'=a_264^0, x_21^0'=h_15^0, x_17^0'=h_15^0, t_24^0'=h_15^0, x_19^0'=h_15^0, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (-2+rv_13^post9 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post6 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 2 47: l9 -> l2 : a_264^0'=-1, rv_13^0'=rv_13^post2, y_20^0'=0, h_15^0'=h_15^post2, a_239^0'=a_264^0, x_21^0'=h_15^0, r_37^0'=r_37^post2, x_17^0'=h_15^post2, t_24^0'=h_15^0, a_290^0'=-1, x_19^0'=h_15^post2, l_143^0'=1+a_264^0, x_14^0'=0, ct_18^0'=0, (a_264^0 >= 0 /\ a_158^0 >= 0 /\ -2+rv_13^post2 >= 0 /\ l_143^0 >= 0 /\ x_14^0 == 0), cost: 4+2*a_264^0 36: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post19, rv_13^0'=nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=2, tp_33^0'=tp_33^post8, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post19, -2+nd_12^10 >= 0, cost: 4 48: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post8, rv_13^0'=nd_12^10, i_98^0'=2, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=3, tp_33^0'=tp_33^post16, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post8, r_92^0'=r_92^post16, -3+nd_12^10 >= 0, cost: 6 49: l14 -> l8 : l_27^0'=nd_12^10, t_32^0'=tp_33^post16, rv_13^0'=nd_12^10, i_98^0'=-1+nd_12^10, r_57^0'=r_57^post8, a_76^0'=2, nd_12^0'=nd_12^post0, i_28^0'=nd_12^10, tp_33^0'=tp_33^post16, rv_31^0'=tp_33^post19, h_30^0'=tp_33^post16, r_92^0'=r_92^post16, -4+nd_12^10 >= 0, cost: 2*nd_12^10 Removed unreachable locations and irrelevant leafs Start location: l14 Computing asymptotic complexity Proved the following lower bound Complexity: Unknown Cpx degree: ? Solved cost: 0 Rule cost: 0