v3: [|t>=0; t+x1-60>=0; x1-60>=0; t+x2-55>=0; -x1+x2+10>=0; x1+x2-115>=0; x2-55>=0; x1-x2>=0; t+x3-51>=0; -x1+x3+20>=0; x1+x3-111>=0; -x2+x3+10>=0; x2+x3-106>=0; x3-51>=0; x1-x3>=0; x2-x3>=0; t+x4-45>=0; -x1+x4+30>=0; x1+x4-105>=0; -x2+x4+20>=0; x2+x4-100>=0; -x3+x4+10>=0; x3+x4-96>=0; x4-45>=0; x1-x4>=0; x2-x4>=0; x3-x4>=0|];; v1: [|t>=0; t+x1-60>=0; x1-60>=0; t+x2-55>=0; -x1+x2+10>=0; x1+x2-115>=0; x2-55>=0; x1-x2-2>=0; t+x3-50>=0; -x1+x3+20>=0; x1+x3-110>=0; -x2+x3+10>=0; x2+x3-105>=0; x3-50>=0; x1-x3-4>=0; x2-x3-2>=0; t+x4-45>=0; -x1+x4+30>=0; x1+x4-105>=0; -x2+x4+20>=0; x2+x4-100>=0; -x3+x4+10>=0; x3+x4-95>=0; x4-45>=0; x1-x4-6>=0; x2-x4-4>=0; x3-x4-2>=0|];; v4: [| t>=0; t+x1-60>=0; x1-60>=0; t+x2-55>=0; -x1+x2+10>=0; x1+x2-115>=0; x2-55>=0; x1-x2>=0; t+x3-50>=0; -x1+x3+20>=0; x1+x3-110>=0; -x2+x3+10>=0; x2+x3-105>=0; x3-50>=0; x1-x3>=0; x2-x3>=0; t+x4-46>=0; -x1+x4+30>=0; x1+x4-106>=0; -x2+x4+20>=0; x2+x4-101>=0; -x3+x4+10>=0; x3+x4-96>=0; x4-46>=0; x1-x4>=0; x2-x4>=0; x3-x4>=0|];; v2: [|t>=0; t+x1-60>=0; x1-60>=0; t+x2-56>=0; -x1+x2+10>=0; x1+x2-116>=0; x2-56>=0; x1-x2>=0; t+x3-50>=0; -x1+x3+20>=0; x1+x3-110>=0; -x2+x3+10>=0; x2+x3-106>=0; x3-50>=0; x1-x3>=0; x2-x3>=0; t+x4-45>=0; -x1+x4+30>=0; x1+x4-105>=0; -x2+x4+20>=0; x2+x4-101>=0; -x3+x4+10>=0; x3+x4-95>=0; x4-45>=0; x1-x4>=0; x2-x4>=0; x3-x4>=0|];; err: [|t>=0; t+x1-60>=0; x1-60>=0; t+x2-55>=0; x1+x2-115>=0; x2-55>=0; t+x3-50>=0; x1+x3-110>=0; x2+x3-105>=0; x3-50>=0; t+x4-45>=0; x1+x4-105>=0; x2+x4-100>=0; x3+x4-95>=0; x4-45>=0|];; [runlim] end: Sat Nov 29 19:34:52 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 0.88 seconds [runlim] time: 0.09 seconds [runlim] space: 6.1 MB [runlim] samples: 1