[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/Motor40.ts [runlim] start: Sun Nov 30 23:29:46 2014 [runlim] main pid: 25550 v_41 : [|t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_40 : [|t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-26>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_39 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-31>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_38 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-36>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_37 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-41>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_36 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-46>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_35 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-51>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_34 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-56>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_33 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-61>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_32 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-66>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_31 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-71>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_30 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-76>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_29 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-81>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_28 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-86>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_27 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-91>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_26 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-96>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_25 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-101>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_24 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-106>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_23 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-111>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_22 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-116>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_21 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-121>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_20 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-126>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_19 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-131>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_18 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-136>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_17 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-141>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_16 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-146>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_15 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-151>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_14 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-156>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_13 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-161>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_12 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-166>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_11 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-171>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_10 : [| t>=0; x_1-220>=0; x_10-176>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_9 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-181>=0|];; v_8 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-186>=0; x_9-180>=0|];; v_7 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-191>=0; x_8-185>=0; x_9-180>=0|];; v_6 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-196>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_5 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-201>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_4 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-206>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_3 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-211>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_2 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-216>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; v_1 : [| t>=0; x_1-220>=0; x_10-175>=0; x_11-170>=0; x_12-165>=0; x_13-160>=0; x_14-155>=0; x_15-150>=0; x_16-145>=0; x_17-140>=0; x_18-135>=0; x_19-130>=0; x_2-215>=0; x_20-125>=0; x_21-120>=0; x_22-115>=0; x_23-110>=0; x_24-105>=0; x_25-100>=0; x_26-95>=0; x_27-90>=0; x_28-85>=0; x_29-80>=0; x_3-210>=0; x_30-75>=0; x_31-70>=0; x_32-65>=0; x_33-60>=0; x_34-55>=0; x_35-50>=0; x_36-45>=0; x_37-40>=0; x_38-35>=0; x_39-30>=0; x_4-205>=0; x_40-25>=0; x_5-200>=0; x_6-195>=0; x_7-190>=0; x_8-185>=0; x_9-180>=0|];; [runlim] end: Sun Nov 30 23:29:48 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 2.31 seconds [runlim] time: 2.00 seconds [runlim] space: 138.6 MB [runlim] samples: 20