[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/Motor20.ts [runlim] start: Sun Nov 30 23:29:44 2014 [runlim] main pid: 25546 v_21 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_20 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-26>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_19 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-31>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_18 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-36>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_17 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-41>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_16 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-46>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_15 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-51>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_14 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-56>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_13 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-61>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_12 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-66>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_11 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-71>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_10 : [| t>=0; x_1-120>=0; x_10-76>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_9 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-81>=0|];; v_8 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-86>=0; x_9-80>=0|];; v_7 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-91>=0; x_8-85>=0; x_9-80>=0|];; v_6 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-96>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_5 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-101>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_4 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-106>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_3 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-111>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_2 : [| t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-116>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; v_1 : [|t>=0; x_1-120>=0; x_10-75>=0; x_11-70>=0; x_12-65>=0; x_13-60>=0; x_14-55>=0; x_15-50>=0; x_16-45>=0; x_17-40>=0; x_18-35>=0; x_19-30>=0; x_2-115>=0; x_20-25>=0; x_3-110>=0; x_4-105>=0; x_5-100>=0; x_6-95>=0; x_7-90>=0; x_8-85>=0; x_9-80>=0|];; [runlim] end: Sun Nov 30 23:29:45 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 1.17 seconds [runlim] time: 0.39 seconds [runlim] space: 33.0 MB [runlim] samples: 4