[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/Motor50.ts [runlim] start: Sun Nov 30 23:29:48 2014 [runlim] main pid: 25552 v_51 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_50 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-26>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_49 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-31>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_48 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-36>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_47 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-41>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_46 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-46>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_45 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-51>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_44 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-56>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_43 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-61>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_42 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-66>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_41 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-71>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_40 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-76>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_39 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-81>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_38 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-86>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_37 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-91>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_36 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-96>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_35 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-101>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_34 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-106>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_33 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-111>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_32 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-116>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_31 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-121>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_30 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-126>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_29 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-131>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_28 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-136>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_27 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-141>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_26 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-146>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_25 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-151>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_24 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-156>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_23 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-161>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_22 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-166>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_21 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-171>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_20 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-176>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_19 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-181>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_18 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-186>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_17 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-191>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_16 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-196>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_15 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-201>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_14 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-206>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_13 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-211>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_12 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-216>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_11 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-221>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_10 : [|t>=0; x_1-270>=0; x_10-226>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_9 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-231>=0|];; v_8 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-236>=0; x_9-230>=0|];; v_7 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-241>=0; x_8-235>=0; x_9-230>=0|];; v_6 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-246>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_5 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-251>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_4 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-256>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_3 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-261>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_2 : [|t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-266>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; v_1 : [| t>=0; x_1-270>=0; x_10-225>=0; x_11-220>=0; x_12-215>=0; x_13-210>=0; x_14-205>=0; x_15-200>=0; x_16-195>=0; x_17-190>=0; x_18-185>=0; x_19-180>=0; x_2-265>=0; x_20-175>=0; x_21-170>=0; x_22-165>=0; x_23-160>=0; x_24-155>=0; x_25-150>=0; x_26-145>=0; x_27-140>=0; x_28-135>=0; x_29-130>=0; x_3-260>=0; x_30-125>=0; x_31-120>=0; x_32-115>=0; x_33-110>=0; x_34-105>=0; x_35-100>=0; x_36-95>=0; x_37-90>=0; x_38-85>=0; x_39-80>=0; x_4-255>=0; x_40-75>=0; x_41-70>=0; x_42-65>=0; x_43-60>=0; x_44-55>=0; x_45-50>=0; x_46-45>=0; x_47-40>=0; x_48-35>=0; x_49-30>=0; x_5-250>=0; x_50-25>=0; x_6-245>=0; x_7-240>=0; x_8-235>=0; x_9-230>=0|];; [runlim] end: Sun Nov 30 23:29:52 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 4.04 seconds [runlim] time: 3.69 seconds [runlim] space: 188.1 MB [runlim] samples: 37