v8: [|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-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>=0; x2-x4>=0; x3-x4>=0; t+x5-40>=0; -x1+x5+40>=0; x1+x5-100>=0; -x2+x5+30>=0; x2+x5-95>=0; -x3+x5+20>=0; x3+x5-90>=0; -x4+x5+10>=0; x4+x5-85>=0; x5-40>=0; x1-x5>=0; x2-x5>=0; x3-x5>=0; x4-x5>=0; t+x6-35>=0; -x1+x6+50>=0; x1+x6-95>=0; -x2+x6+40>=0; x2+x6-90>=0; -x3+x6+30>=0; x3+x6-85>=0; -x4+x6+20>=0; x4+x6-80>=0; -x5+x6+10>=0; x5+x6-75>=0; x6-35>=0; x1-x6>=0; x2-x6>=0; x3-x6>=0; x4-x6>=0; x5-x6>=0; t+x7-30>=0; -x1+x7+60>=0; x1+x7-90>=0; -x2+x7+50>=0; x2+x7-85>=0; -x3+x7+40>=0; x3+x7-80>=0; -x4+x7+30>=0; x4+x7-75>=0; -x5+x7+20>=0; x5+x7-70>=0; -x6+x7+10>=0; x6+x7-65>=0; x7-30>=0; x1-x7>=0; x2-x7>=0; x3-x7>=0; x4-x7>=0; x5-x7>=0; x6-x7>=0; t+x8-26>=0; -x1+x8+70>=0; x1+x8-86>=0; -x2+x8+60>=0; x2+x8-81>=0; -x3+x8+50>=0; x3+x8-76>=0; -x4+x8+40>=0; x4+x8-71>=0; -x5+x8+30>=0; x5+x8-66>=0; -x6+x8+20>=0; x6+x8-61>=0; -x7+x8+10>=0; x7+x8-56>=0; x8-26>=0; x1-x8>=0; x2-x8>=0; x3-x8>=0; x4-x8>=0; x5-x8>=0; x6-x8>=0; x7-x8>=0|];; v7: [|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-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>=0; x2-x4>=0; x3-x4>=0; t+x5-40>=0; -x1+x5+40>=0; x1+x5-100>=0; -x2+x5+30>=0; x2+x5-95>=0; -x3+x5+20>=0; x3+x5-90>=0; -x4+x5+10>=0; x4+x5-85>=0; x5-40>=0; x1-x5>=0; x2-x5>=0; x3-x5>=0; x4-x5>=0; t+x6-35>=0; -x1+x6+50>=0; x1+x6-95>=0; -x2+x6+40>=0; x2+x6-90>=0; -x3+x6+30>=0; x3+x6-85>=0; -x4+x6+20>=0; x4+x6-80>=0; -x5+x6+10>=0; x5+x6-75>=0; x6-35>=0; x1-x6>=0; x2-x6>=0; x3-x6>=0; x4-x6>=0; x5-x6>=0; t+x7-31>=0; -x1+x7+60>=0; x1+x7-91>=0; -x2+x7+50>=0; x2+x7-86>=0; -x3+x7+40>=0; x3+x7-81>=0; -x4+x7+30>=0; x4+x7-76>=0; -x5+x7+20>=0; x5+x7-71>=0; -x6+x7+10>=0; x6+x7-66>=0; x7-31>=0; x1-x7>=0; x2-x7>=0; x3-x7>=0; x4-x7>=0; x5-x7>=0; x6-x7>=0; t+x8-25>=0; -x1+x8+70>=0; x1+x8-85>=0; -x2+x8+60>=0; x2+x8-80>=0; -x3+x8+50>=0; x3+x8-75>=0; -x4+x8+40>=0; x4+x8-70>=0; -x5+x8+30>=0; x5+x8-65>=0; -x6+x8+20>=0; x6+x8-60>=0; -x7+x8+10>=0; x7+x8-56>=0; x8-25>=0; x1-x8>=0; x2-x8>=0; x3-x8>=0; x4-x8>=0; x5-x8>=0; x6-x8>=0; x7-x8>=0|];; v6: [|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-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>=0; x2-x4>=0; x3-x4>=0; t+x5-40>=0; -x1+x5+40>=0; x1+x5-100>=0; -x2+x5+30>=0; x2+x5-95>=0; -x3+x5+20>=0; x3+x5-90>=0; -x4+x5+10>=0; x4+x5-85>=0; x5-40>=0; x1-x5>=0; x2-x5>=0; x3-x5>=0; x4-x5>=0; t+x6-36>=0; -x1+x6+50>=0; x1+x6-96>=0; -x2+x6+40>=0; x2+x6-91>=0; -x3+x6+30>=0; x3+x6-86>=0; -x4+x6+20>=0; x4+x6-81>=0; -x5+x6+10>=0; x5+x6-76>=0; x6-36>=0; x1-x6>=0; x2-x6>=0; x3-x6>=0; x4-x6>=0; x5-x6>=0; t+x7-30>=0; -x1+x7+60>=0; x1+x7-90>=0; -x2+x7+50>=0; x2+x7-85>=0; -x3+x7+40>=0; x3+x7-80>=0; -x4+x7+30>=0; x4+x7-75>=0; -x5+x7+20>=0; x5+x7-70>=0; -x6+x7+10>=0; x6+x7-66>=0; x7-30>=0; x1-x7>=0; x2-x7>=0; x3-x7>=0; x4-x7>=0; x5-x7>=0; x6-x7>=0; t+x8-25>=0; -x1+x8+70>=0; x1+x8-85>=0; -x2+x8+60>=0; x2+x8-80>=0; -x3+x8+50>=0; x3+x8-75>=0; -x4+x8+40>=0; x4+x8-70>=0; -x5+x8+30>=0; x5+x8-65>=0; -x6+x8+20>=0; x6+x8-61>=0; -x7+x8+10>=0; x7+x8-55>=0; x8-25>=0; x1-x8>=0; x2-x8>=0; x3-x8>=0; x4-x8>=0; x5-x8>=0; x6-x8>=0; x7-x8>=0|];; v5: [| 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-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>=0; x2-x4>=0; x3-x4>=0; t+x5-41>=0; -x1+x5+40>=0; x1+x5-101>=0; -x2+x5+30>=0; x2+x5-96>=0; -x3+x5+20>=0; x3+x5-91>=0; -x4+x5+10>=0; x4+x5-86>=0; x5-41>=0; x1-x5>=0; x2-x5>=0; x3-x5>=0; x4-x5>=0; t+x6-35>=0; -x1+x6+50>=0; x1+x6-95>=0; -x2+x6+40>=0; x2+x6-90>=0; -x3+x6+30>=0; x3+x6-85>=0; -x4+x6+20>=0; x4+x6-80>=0; -x5+x6+10>=0; x5+x6-76>=0; x6-35>=0; x1-x6>=0; x2-x6>=0; x3-x6>=0; x4-x6>=0; x5-x6>=0; t+x7-30>=0; -x1+x7+60>=0; x1+x7-90>=0; -x2+x7+50>=0; x2+x7-85>=0; -x3+x7+40>=0; x3+x7-80>=0; -x4+x7+30>=0; x4+x7-75>=0; -x5+x7+20>=0; x5+x7-71>=0; -x6+x7+10>=0; x6+x7-65>=0; x7-30>=0; x1-x7>=0; x2-x7>=0; x3-x7>=0; x4-x7>=0; x5-x7>=0; x6-x7>=0; t+x8-25>=0; -x1+x8+70>=0; x1+x8-85>=0; -x2+x8+60>=0; x2+x8-80>=0; -x3+x8+50>=0; x3+x8-75>=0; -x4+x8+40>=0; x4+x8-70>=0; -x5+x8+30>=0; x5+x8-66>=0; -x6+x8+20>=0; x6+x8-60>=0; -x7+x8+10>=0; x7+x8-55>=0; x8-25>=0; x1-x8>=0; x2-x8>=0; x3-x8>=0; x4-x8>=0; x5-x8>=0; x6-x8>=0; x7-x8>=0|];; 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; t+x5-40>=0; -x1+x5+40>=0; x1+x5-100>=0; -x2+x5+30>=0; x2+x5-95>=0; -x3+x5+20>=0; x3+x5-91>=0; -x4+x5+10>=0; x4+x5-85>=0; x5-40>=0; x1-x5>=0; x2-x5>=0; x3-x5>=0; x4-x5>=0; t+x6-35>=0; -x1+x6+50>=0; x1+x6-95>=0; -x2+x6+40>=0; x2+x6-90>=0; -x3+x6+30>=0; x3+x6-86>=0; -x4+x6+20>=0; x4+x6-80>=0; -x5+x6+10>=0; x5+x6-75>=0; x6-35>=0; x1-x6>=0; x2-x6>=0; x3-x6>=0; x4-x6>=0; x5-x6>=0; t+x7-30>=0; -x1+x7+60>=0; x1+x7-90>=0; -x2+x7+50>=0; x2+x7-85>=0; -x3+x7+40>=0; x3+x7-81>=0; -x4+x7+30>=0; x4+x7-75>=0; -x5+x7+20>=0; x5+x7-70>=0; -x6+x7+10>=0; x6+x7-65>=0; x7-30>=0; x1-x7>=0; x2-x7>=0; x3-x7>=0; x4-x7>=0; x5-x7>=0; x6-x7>=0; t+x8-25>=0; -x1+x8+70>=0; x1+x8-85>=0; -x2+x8+60>=0; x2+x8-80>=0; -x3+x8+50>=0; x3+x8-76>=0; -x4+x8+40>=0; x4+x8-70>=0; -x5+x8+30>=0; x5+x8-65>=0; -x6+x8+20>=0; x6+x8-60>=0; -x7+x8+10>=0; x7+x8-55>=0; x8-25>=0; x1-x8>=0; x2-x8>=0; x3-x8>=0; x4-x8>=0; x5-x8>=0; x6-x8>=0; x7-x8>=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; t+x5-40>=0; -x1+x5+40>=0; x1+x5-100>=0; -x2+x5+30>=0; x2+x5-95>=0; -x3+x5+20>=0; x3+x5-90>=0; -x4+x5+10>=0; x4+x5-85>=0; x5-40>=0; x1-x5-8>=0; x2-x5-6>=0; x3-x5-4>=0; x4-x5-2>=0; t+x6-35>=0; -x1+x6+50>=0; x1+x6-95>=0; -x2+x6+40>=0; x2+x6-90>=0; -x3+x6+30>=0; x3+x6-85>=0; -x4+x6+20>=0; x4+x6-80>=0; -x5+x6+10>=0; x5+x6-75>=0; x6-35>=0; x1-x6-10>=0; x2-x6-8>=0; x3-x6-6>=0; x4-x6-4>=0; x5-x6-2>=0; t+x7-30>=0; -x1+x7+60>=0; x1+x7-90>=0; -x2+x7+50>=0; x2+x7-85>=0; -x3+x7+40>=0; x3+x7-80>=0; -x4+x7+30>=0; x4+x7-75>=0; -x5+x7+20>=0; x5+x7-70>=0; -x6+x7+10>=0; x6+x7-65>=0; x7-30>=0; x1-x7-12>=0; x2-x7-10>=0; x3-x7-8>=0; x4-x7-6>=0; x5-x7-4>=0; x6-x7-2>=0; t+x8-25>=0; -x1+x8+70>=0; x1+x8-85>=0; -x2+x8+60>=0; x2+x8-80>=0; -x3+x8+50>=0; x3+x8-75>=0; -x4+x8+40>=0; x4+x8-70>=0; -x5+x8+30>=0; x5+x8-65>=0; -x6+x8+20>=0; x6+x8-60>=0; -x7+x8+10>=0; x7+x8-55>=0; x8-25>=0; x1-x8-14>=0; x2-x8-12>=0; x3-x8-10>=0; x4-x8-8>=0; x5-x8-6>=0; x6-x8-4>=0; x7-x8-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; t+x5-40>=0; -x1+x5+40>=0; x1+x5-100>=0; -x2+x5+30>=0; x2+x5-95>=0; -x3+x5+20>=0; x3+x5-90>=0; -x4+x5+10>=0; x4+x5-86>=0; x5-40>=0; x1-x5>=0; x2-x5>=0; x3-x5>=0; x4-x5>=0; t+x6-35>=0; -x1+x6+50>=0; x1+x6-95>=0; -x2+x6+40>=0; x2+x6-90>=0; -x3+x6+30>=0; x3+x6-85>=0; -x4+x6+20>=0; x4+x6-81>=0; -x5+x6+10>=0; x5+x6-75>=0; x6-35>=0; x1-x6>=0; x2-x6>=0; x3-x6>=0; x4-x6>=0; x5-x6>=0; t+x7-30>=0; -x1+x7+60>=0; x1+x7-90>=0; -x2+x7+50>=0; x2+x7-85>=0; -x3+x7+40>=0; x3+x7-80>=0; -x4+x7+30>=0; x4+x7-76>=0; -x5+x7+20>=0; x5+x7-70>=0; -x6+x7+10>=0; x6+x7-65>=0; x7-30>=0; x1-x7>=0; x2-x7>=0; x3-x7>=0; x4-x7>=0; x5-x7>=0; x6-x7>=0; t+x8-25>=0; -x1+x8+70>=0; x1+x8-85>=0; -x2+x8+60>=0; x2+x8-80>=0; -x3+x8+50>=0; x3+x8-75>=0; -x4+x8+40>=0; x4+x8-71>=0; -x5+x8+30>=0; x5+x8-65>=0; -x6+x8+20>=0; x6+x8-60>=0; -x7+x8+10>=0; x7+x8-55>=0; x8-25>=0; x1-x8>=0; x2-x8>=0; x3-x8>=0; x4-x8>=0; x5-x8>=0; x6-x8>=0; x7-x8>=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; t+x5-40>=0; -x1+x5+40>=0; x1+x5-100>=0; -x2+x5+30>=0; x2+x5-96>=0; -x3+x5+20>=0; x3+x5-90>=0; -x4+x5+10>=0; x4+x5-85>=0; x5-40>=0; x1-x5>=0; x2-x5>=0; x3-x5>=0; x4-x5>=0; t+x6-35>=0; -x1+x6+50>=0; x1+x6-95>=0; -x2+x6+40>=0; x2+x6-91>=0; -x3+x6+30>=0; x3+x6-85>=0; -x4+x6+20>=0; x4+x6-80>=0; -x5+x6+10>=0; x5+x6-75>=0; x6-35>=0; x1-x6>=0; x2-x6>=0; x3-x6>=0; x4-x6>=0; x5-x6>=0; t+x7-30>=0; -x1+x7+60>=0; x1+x7-90>=0; -x2+x7+50>=0; x2+x7-86>=0; -x3+x7+40>=0; x3+x7-80>=0; -x4+x7+30>=0; x4+x7-75>=0; -x5+x7+20>=0; x5+x7-70>=0; -x6+x7+10>=0; x6+x7-65>=0; x7-30>=0; x1-x7>=0; x2-x7>=0; x3-x7>=0; x4-x7>=0; x5-x7>=0; x6-x7>=0; t+x8-25>=0; -x1+x8+70>=0; x1+x8-85>=0; -x2+x8+60>=0; x2+x8-81>=0; -x3+x8+50>=0; x3+x8-75>=0; -x4+x8+40>=0; x4+x8-70>=0; -x5+x8+30>=0; x5+x8-65>=0; -x6+x8+20>=0; x6+x8-60>=0; -x7+x8+10>=0; x7+x8-55>=0; x8-25>=0; x1-x8>=0; x2-x8>=0; x3-x8>=0; x4-x8>=0; x5-x8>=0; x6-x8>=0; x7-x8>=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; t+x5-40>=0; x1+x5-100>=0; x2+x5-95>=0; x3+x5-90>=0; x4+x5-85>=0; x5-40>=0; t+x6-35>=0; x1+x6-95>=0; x2+x6-90>=0; x3+x6-85>=0; x4+x6-80>=0; x5+x6-75>=0; x6-35>=0; t+x7-30>=0; x1+x7-90>=0; x2+x7-85>=0; x3+x7-80>=0; x4+x7-75>=0; x5+x7-70>=0; x6+x7-65>=0; x7-30>=0; t+x8-25>=0; x1+x8-85>=0; x2+x8-80>=0; x3+x8-75>=0; x4+x8-70>=0; x5+x8-65>=0; x6+x8-60>=0; x7+x8-55>=0; x8-25>=0; x1-x8>=0; x2-x8>=0; x3-x8>=0; x4-x8>=0; x5-x8>=0; x6-x8>=0; x7-x8>=0|];; [runlim] end: Sat Nov 29 22:03:01 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 1.47 seconds [runlim] time: 1.00 seconds [runlim] space: 27.6 MB [runlim] samples: 10