## Cannot sample enough valid points. (more)

$0.0 \le x1 \le 6 \land 0.0 \le x2 \le 6 \land 1 \le x3 \le 5 \land 0.0 \le x4 \le 6 \land 0.0 \le x5 \le 6 \land 0.0 \le x6 \le 10 \land \left(\left(x3 - 3\right) \cdot \left(x3 - 3\right) + x4\right) - 4 \ge 0.0 \land \left(\left(x5 - 3\right) \cdot \left(x5 - 3\right) + x6\right) - 4 \ge 0.0 \land \left(2 - x1\right) + 3 \cdot x2 \ge 0.0 \land \left(2 + x1\right) - x2 \ge 0.0 \land \left(6 - x1\right) - x2 \ge 0.0 \land \left(x1 + x2\right) - 2 \ge 0.0$
$\left(\left(\left(\left(-25 \cdot \left(\left(x1 - 2\right) \cdot \left(x1 - 2\right)\right) - \left(x2 - 2\right) \cdot \left(x2 - 2\right)\right) - \left(x3 - 1\right) \cdot \left(x3 - 1\right)\right) - \left(x4 - 4\right) \cdot \left(x4 - 4\right)\right) - \left(x5 - 1\right) \cdot \left(x5 - 1\right)\right) - \left(x6 - 4\right) \cdot \left(x6 - 4\right)$
\left(\left(\left(\left(-25 \cdot \left(\left(x1 - 2\right) \cdot \left(x1 - 2\right)\right) - \left(x2 - 2\right) \cdot \left(x2 - 2\right)\right) - \left(x3 - 1\right) \cdot \left(x3 - 1\right)\right) - \left(x4 - 4\right) \cdot \left(x4 - 4\right)\right) - \left(x5 - 1\right) \cdot \left(x5 - 1\right)\right) - \left(x6 - 4\right) \cdot \left(x6 - 4\right)
double f(double x1, double x2, double x3, double x4, double x5, double x6) {
double r3768646 = -25.0;
double r3768647 = x1;
double r3768648 = 2.0;
double r3768649 = r3768647 - r3768648;
double r3768650 = r3768649 * r3768649;
double r3768651 = r3768646 * r3768650;
double r3768652 = x2;
double r3768653 = r3768652 - r3768648;
double r3768654 = r3768653 * r3768653;
double r3768655 = r3768651 - r3768654;
double r3768656 = x3;
double r3768657 = 1.0;
double r3768658 = r3768656 - r3768657;
double r3768659 = r3768658 * r3768658;
double r3768660 = r3768655 - r3768659;
double r3768661 = x4;
double r3768662 = 4.0;
double r3768663 = r3768661 - r3768662;
double r3768664 = r3768663 * r3768663;
double r3768665 = r3768660 - r3768664;
double r3768666 = x5;
double r3768667 = r3768666 - r3768657;
double r3768668 = r3768667 * r3768667;
double r3768669 = r3768665 - r3768668;
double r3768670 = x6;
double r3768671 = r3768670 - r3768662;
double r3768672 = r3768671 * r3768671;
double r3768673 = r3768669 - r3768672;
return r3768673;
}