[runlim] version: 1.7 [runlim] time limit: 3600 seconds [runlim] real time limit: 311040000 seconds [runlim] space limit: 4294967069 MB [runlim] argv[0]: /home/zhouyan/BACH/intertran-v1.0/interproc.opt [runlim] argv[1]: -domain [runlim] argv[2]: box [runlim] argv[3]: /home/zhouyan/BACH/temp/Motor60.ts [runlim] start: Sun Nov 30 23:29:52 2014 [runlim] main pid: 25555 v_61 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_60 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-26>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_59 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-31>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_58 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-36>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_57 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-41>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_56 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-46>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_55 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-51>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_54 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-56>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_53 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-61>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_52 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-66>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_51 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-71>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_50 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-76>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_49 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-81>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_48 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-86>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_47 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-91>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_46 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-96>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_45 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-101>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_44 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-106>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_43 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-111>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_42 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-116>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_41 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-121>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_40 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-126>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_39 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-131>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_38 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-136>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_37 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-141>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_36 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-146>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_35 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-151>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_34 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-156>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_33 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-161>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_32 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-166>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_31 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-171>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_30 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-176>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_29 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-181>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_28 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-186>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_27 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-191>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_26 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-196>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_25 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-201>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_24 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-206>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_23 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-211>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_22 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-216>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_21 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-221>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_20 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-226>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_19 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-231>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_18 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-236>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_17 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-241>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_16 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-246>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_15 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-251>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_14 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-256>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_13 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-261>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_12 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-266>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_11 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-271>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_10 : [| t>=0; x_1-320>=0; x_10-276>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_9 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-281>=0|];; v_8 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-286>=0; x_9-280>=0|];; v_7 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-291>=0; x_8-285>=0; x_9-280>=0|];; v_6 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-296>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_5 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-301>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_4 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-306>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_3 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-311>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_2 : [|t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-316>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; v_1 : [| t>=0; x_1-320>=0; x_10-275>=0; x_11-270>=0; x_12-265>=0; x_13-260>=0; x_14-255>=0; x_15-250>=0; x_16-245>=0; x_17-240>=0; x_18-235>=0; x_19-230>=0; x_2-315>=0; x_20-225>=0; x_21-220>=0; x_22-215>=0; x_23-210>=0; x_24-205>=0; x_25-200>=0; x_26-195>=0; x_27-190>=0; x_28-185>=0; x_29-180>=0; x_3-310>=0; x_30-175>=0; x_31-170>=0; x_32-165>=0; x_33-160>=0; x_34-155>=0; x_35-150>=0; x_36-145>=0; x_37-140>=0; x_38-135>=0; x_39-130>=0; x_4-305>=0; x_40-125>=0; x_41-120>=0; x_42-115>=0; x_43-110>=0; x_44-105>=0; x_45-100>=0; x_46-95>=0; x_47-90>=0; x_48-85>=0; x_49-80>=0; x_5-300>=0; x_50-75>=0; x_51-70>=0; x_52-65>=0; x_53-60>=0; x_54-55>=0; x_55-50>=0; x_56-45>=0; x_57-40>=0; x_58-35>=0; x_59-30>=0; x_6-295>=0; x_60-25>=0; x_7-290>=0; x_8-285>=0; x_9-280>=0|];; [runlim] end: Sun Nov 30 23:29:58 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 6.16 seconds [runlim] time: 6.08 seconds [runlim] space: 240.0 MB [runlim] samples: 61