[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/Motor30.ts [runlim] start: Sun Nov 30 23:29:45 2014 [runlim] main pid: 25548 v_31 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_30 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-26>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_29 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-31>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_28 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-36>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_27 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-41>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_26 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-46>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_25 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-51>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_24 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-56>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_23 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-61>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_22 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-66>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_21 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-71>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_20 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-76>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_19 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-81>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_18 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-86>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_17 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-91>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_16 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-96>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_15 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-101>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_14 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-106>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_13 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-111>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_12 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-116>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_11 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-121>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_10 : [| t>=0; x_1-170>=0; x_10-126>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_9 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-131>=0|];; v_8 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-136>=0; x_9-130>=0|];; v_7 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-141>=0; x_8-135>=0; x_9-130>=0|];; v_6 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-146>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_5 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-151>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_4 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-156>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_3 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-161>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_2 : [| t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-166>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; v_1 : [|t>=0; x_1-170>=0; x_10-125>=0; x_11-120>=0; x_12-115>=0; x_13-110>=0; x_14-105>=0; x_15-100>=0; x_16-95>=0; x_17-90>=0; x_18-85>=0; x_19-80>=0; x_2-165>=0; x_20-75>=0; x_21-70>=0; x_22-65>=0; x_23-60>=0; x_24-55>=0; x_25-50>=0; x_26-45>=0; x_27-40>=0; x_28-35>=0; x_29-30>=0; x_3-160>=0; x_30-25>=0; x_4-155>=0; x_5-150>=0; x_6-145>=0; x_7-140>=0; x_8-135>=0; x_9-130>=0|];; [runlim] end: Sun Nov 30 23:29:46 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 1.22 seconds [runlim] time: 1.00 seconds [runlim] space: 75.2 MB [runlim] samples: 10