Ytukyg

I have the following system of inequalities of real variables

sys = 0.383706 x1 + 0.720204 x2 + 1.4568 x3 - 0.000244875 y >   0 && -0.0941312 x1 - 0.176681 x2 - 0.357383 x3 + 0.0000592689 y >   0 && 1.41819 x1 + 3.079 x2 + 2.53801 x3 - 0.00182772 y >   0 && -0.00258971 x1 - 0.00562247 x2 - 0.00463458 x3 +    3.93843*10^-6 y > 0 &&  0.129511 x1 + 0.214698 x2 + 0.286739 x3 - 0.0000795243 y >   0 && -0.660462 x1 - 1.09489 x2 - 1.46227 x3 + 0.000405426 y > 0 &&  0.351966 x1 + 3.44019 x2 + 7.59863 x3 + 0.00257072 y >   0 && -0.00265509 x1 - 0.0259514 x2 - 0.0573209 x3 -    0.0000199557 y > 0 &&  1.34471 x1 + 2.58639 x2 + 3.39561 x3 + 0.0000742173 y >   0 && -0.0314846 x1 - 0.0605571 x2 - 0.079504 x3 - 1.69328*10^-6 y >   0

I want to Reduce the system in order to see if it admits solutions or not. However, the command Reduce takes too much time and gets stuck. How can you check if this system admits solutions?

I have tried with FindInstance[sys,{x1,x2,x3,y},Reals] which returns {}. However, I am not sure this is a fully proof that the system does not admit solution. Indeed, If I run the command on a subsystem of inequalities I experience the following behaviour

FindInstance[sys[[1 ;; 4]], {x1, x2, x3, y}, Reals]

(* {} *)

but If I ask for more instances, Mathematica found the points

FindInstance[sys[[1 ;; 4]], {x1, x2, x3, y}, Reals, 2]

(*{{x1 -> -33., x2 -> 13.5619, x3 -> 1.98727, y -> 0.255564}, {x1 -> -51., x2 -> 20.9595, x3 -> 3.07117, y -> 0.601467}}*)

So, the subsystem [[1;;4]] admits at least a solution. I have run FindInstance[sys, {x1, x2, x3, y}, Reals, 2] for all the night and got the output {}. Still, is this a proof that the system does not admits solution?

Reduce[Rationalize[sys, 2^-12], {x1, x2, x3, y}, Reals] // RepeatedTiming

{0.24878, False}

RegionIntersection @@ (ImplicitRegion[#, {x1, x2, x3, y}] & /@ (List @@ sys)) // 

   RepeatedTiming

{0.0152, EmptyRegion[4]}