extern float __VERIFIER_nondet_float(void);
extern int __VERIFIER_nondet_int(void);
typedef enum {false, true} bool;
bool __VERIFIER_nondet_bool(void) {
  return __VERIFIER_nondet_int() != 0;
}

int main()
{
bool _EL_U_3833, _x__EL_U_3833;
float x_16, _x_x_16;
float x_0, _x_x_0;
float x_11, _x_x_11;
bool _EL_X_3825, _x__EL_X_3825;
float x_3, _x_x_3;
float x_33, _x_x_33;
float x_2, _x_x_2;
float x_15, _x_x_15;
float x_1, _x_x_1;
float x_4, _x_x_4;
float x_17, _x_x_17;
float x_7, _x_x_7;
float x_5, _x_x_5;
float x_6, _x_x_6;
float x_10, _x_x_10;
float x_8, _x_x_8;
float x_9, _x_x_9;
float x_31, _x_x_31;
float x_12, _x_x_12;
float x_13, _x_x_13;
float x_18, _x_x_18;
float x_14, _x_x_14;
float x_19, _x_x_19;
float x_22, _x_x_22;
float x_23, _x_x_23;
float x_20, _x_x_20;
float x_21, _x_x_21;
float x_24, _x_x_24;
float x_30, _x_x_30;
float x_25, _x_x_25;
float x_34, _x_x_34;
float x_26, _x_x_26;
float x_27, _x_x_27;
float x_28, _x_x_28;
float x_29, _x_x_29;
float x_35, _x_x_35;
float x_32, _x_x_32;

  int __steps_to_fair = __VERIFIER_nondet_int();
  _EL_U_3833 = __VERIFIER_nondet_bool();
  x_16 = __VERIFIER_nondet_float();
  x_0 = __VERIFIER_nondet_float();
  x_11 = __VERIFIER_nondet_float();
  _EL_X_3825 = __VERIFIER_nondet_bool();
  x_3 = __VERIFIER_nondet_float();
  x_33 = __VERIFIER_nondet_float();
  x_2 = __VERIFIER_nondet_float();
  x_15 = __VERIFIER_nondet_float();
  x_1 = __VERIFIER_nondet_float();
  x_4 = __VERIFIER_nondet_float();
  x_17 = __VERIFIER_nondet_float();
  x_7 = __VERIFIER_nondet_float();
  x_5 = __VERIFIER_nondet_float();
  x_6 = __VERIFIER_nondet_float();
  x_10 = __VERIFIER_nondet_float();
  x_8 = __VERIFIER_nondet_float();
  x_9 = __VERIFIER_nondet_float();
  x_31 = __VERIFIER_nondet_float();
  x_12 = __VERIFIER_nondet_float();
  x_13 = __VERIFIER_nondet_float();
  x_18 = __VERIFIER_nondet_float();
  x_14 = __VERIFIER_nondet_float();
  x_19 = __VERIFIER_nondet_float();
  x_22 = __VERIFIER_nondet_float();
  x_23 = __VERIFIER_nondet_float();
  x_20 = __VERIFIER_nondet_float();
  x_21 = __VERIFIER_nondet_float();
  x_24 = __VERIFIER_nondet_float();
  x_30 = __VERIFIER_nondet_float();
  x_25 = __VERIFIER_nondet_float();
  x_34 = __VERIFIER_nondet_float();
  x_26 = __VERIFIER_nondet_float();
  x_27 = __VERIFIER_nondet_float();
  x_28 = __VERIFIER_nondet_float();
  x_29 = __VERIFIER_nondet_float();
  x_35 = __VERIFIER_nondet_float();
  x_32 = __VERIFIER_nondet_float();

  bool __ok = (1 && ( !(_EL_X_3825 || ( !(((x_11 + (-1.0 * x_16)) <= 17.0) || _EL_U_3833)))));
  while (__steps_to_fair >= 0 && __ok) {
    if ((((x_11 + (-1.0 * x_16)) <= 17.0) || ( !(((x_11 + (-1.0 * x_16)) <= 17.0) || _EL_U_3833)))) {
      __steps_to_fair = __VERIFIER_nondet_int();
    } else {
      __steps_to_fair--;
    }
    _x__EL_U_3833 = __VERIFIER_nondet_bool();
    _x_x_16 = __VERIFIER_nondet_float();
    _x_x_0 = __VERIFIER_nondet_float();
    _x_x_11 = __VERIFIER_nondet_float();
    _x__EL_X_3825 = __VERIFIER_nondet_bool();
    _x_x_3 = __VERIFIER_nondet_float();
    _x_x_33 = __VERIFIER_nondet_float();
    _x_x_2 = __VERIFIER_nondet_float();
    _x_x_15 = __VERIFIER_nondet_float();
    _x_x_1 = __VERIFIER_nondet_float();
    _x_x_4 = __VERIFIER_nondet_float();
    _x_x_17 = __VERIFIER_nondet_float();
    _x_x_7 = __VERIFIER_nondet_float();
    _x_x_5 = __VERIFIER_nondet_float();
    _x_x_6 = __VERIFIER_nondet_float();
    _x_x_10 = __VERIFIER_nondet_float();
    _x_x_8 = __VERIFIER_nondet_float();
    _x_x_9 = __VERIFIER_nondet_float();
    _x_x_31 = __VERIFIER_nondet_float();
    _x_x_12 = __VERIFIER_nondet_float();
    _x_x_13 = __VERIFIER_nondet_float();
    _x_x_18 = __VERIFIER_nondet_float();
    _x_x_14 = __VERIFIER_nondet_float();
    _x_x_19 = __VERIFIER_nondet_float();
    _x_x_22 = __VERIFIER_nondet_float();
    _x_x_23 = __VERIFIER_nondet_float();
    _x_x_20 = __VERIFIER_nondet_float();
    _x_x_21 = __VERIFIER_nondet_float();
    _x_x_24 = __VERIFIER_nondet_float();
    _x_x_30 = __VERIFIER_nondet_float();
    _x_x_25 = __VERIFIER_nondet_float();
    _x_x_34 = __VERIFIER_nondet_float();
    _x_x_26 = __VERIFIER_nondet_float();
    _x_x_27 = __VERIFIER_nondet_float();
    _x_x_28 = __VERIFIER_nondet_float();
    _x_x_29 = __VERIFIER_nondet_float();
    _x_x_35 = __VERIFIER_nondet_float();
    _x_x_32 = __VERIFIER_nondet_float();

    __ok = ((((((((((((((((((((((((((((((((((((((((x_35 + (-1.0 * _x_x_0)) <= -7.0) && (((x_34 + (-1.0 * _x_x_0)) <= -17.0) && (((x_31 + (-1.0 * _x_x_0)) <= -2.0) && (((x_27 + (-1.0 * _x_x_0)) <= -17.0) && (((x_25 + (-1.0 * _x_x_0)) <= -16.0) && (((x_24 + (-1.0 * _x_x_0)) <= -12.0) && (((x_23 + (-1.0 * _x_x_0)) <= -17.0) && (((x_20 + (-1.0 * _x_x_0)) <= -6.0) && (((x_18 + (-1.0 * _x_x_0)) <= -19.0) && (((x_14 + (-1.0 * _x_x_0)) <= -9.0) && (((x_13 + (-1.0 * _x_x_0)) <= -1.0) && (((x_10 + (-1.0 * _x_x_0)) <= -4.0) && (((x_7 + (-1.0 * _x_x_0)) <= -20.0) && (((x_6 + (-1.0 * _x_x_0)) <= -3.0) && (((x_5 + (-1.0 * _x_x_0)) <= -6.0) && (((x_4 + (-1.0 * _x_x_0)) <= -11.0) && (((x_1 + (-1.0 * _x_x_0)) <= -7.0) && ((x_2 + (-1.0 * _x_x_0)) <= -7.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_0)) == -7.0) || (((x_34 + (-1.0 * _x_x_0)) == -17.0) || (((x_31 + (-1.0 * _x_x_0)) == -2.0) || (((x_27 + (-1.0 * _x_x_0)) == -17.0) || (((x_25 + (-1.0 * _x_x_0)) == -16.0) || (((x_24 + (-1.0 * _x_x_0)) == -12.0) || (((x_23 + (-1.0 * _x_x_0)) == -17.0) || (((x_20 + (-1.0 * _x_x_0)) == -6.0) || (((x_18 + (-1.0 * _x_x_0)) == -19.0) || (((x_14 + (-1.0 * _x_x_0)) == -9.0) || (((x_13 + (-1.0 * _x_x_0)) == -1.0) || (((x_10 + (-1.0 * _x_x_0)) == -4.0) || (((x_7 + (-1.0 * _x_x_0)) == -20.0) || (((x_6 + (-1.0 * _x_x_0)) == -3.0) || (((x_5 + (-1.0 * _x_x_0)) == -6.0) || (((x_4 + (-1.0 * _x_x_0)) == -11.0) || (((x_1 + (-1.0 * _x_x_0)) == -7.0) || ((x_2 + (-1.0 * _x_x_0)) == -7.0))))))))))))))))))) && ((((x_32 + (-1.0 * _x_x_1)) <= -20.0) && (((x_31 + (-1.0 * _x_x_1)) <= -11.0) && (((x_28 + (-1.0 * _x_x_1)) <= -2.0) && (((x_22 + (-1.0 * _x_x_1)) <= -19.0) && (((x_19 + (-1.0 * _x_x_1)) <= -7.0) && (((x_18 + (-1.0 * _x_x_1)) <= -18.0) && (((x_17 + (-1.0 * _x_x_1)) <= -17.0) && (((x_15 + (-1.0 * _x_x_1)) <= -6.0) && (((x_14 + (-1.0 * _x_x_1)) <= -18.0) && (((x_13 + (-1.0 * _x_x_1)) <= -18.0) && (((x_12 + (-1.0 * _x_x_1)) <= -7.0) && (((x_11 + (-1.0 * _x_x_1)) <= -14.0) && (((x_8 + (-1.0 * _x_x_1)) <= -16.0) && (((x_7 + (-1.0 * _x_x_1)) <= -10.0) && (((x_5 + (-1.0 * _x_x_1)) <= -11.0) && (((x_4 + (-1.0 * _x_x_1)) <= -7.0) && (((x_2 + (-1.0 * _x_x_1)) <= -5.0) && ((x_3 + (-1.0 * _x_x_1)) <= -19.0)))))))))))))))))) && (((x_32 + (-1.0 * _x_x_1)) == -20.0) || (((x_31 + (-1.0 * _x_x_1)) == -11.0) || (((x_28 + (-1.0 * _x_x_1)) == -2.0) || (((x_22 + (-1.0 * _x_x_1)) == -19.0) || (((x_19 + (-1.0 * _x_x_1)) == -7.0) || (((x_18 + (-1.0 * _x_x_1)) == -18.0) || (((x_17 + (-1.0 * _x_x_1)) == -17.0) || (((x_15 + (-1.0 * _x_x_1)) == -6.0) || (((x_14 + (-1.0 * _x_x_1)) == -18.0) || (((x_13 + (-1.0 * _x_x_1)) == -18.0) || (((x_12 + (-1.0 * _x_x_1)) == -7.0) || (((x_11 + (-1.0 * _x_x_1)) == -14.0) || (((x_8 + (-1.0 * _x_x_1)) == -16.0) || (((x_7 + (-1.0 * _x_x_1)) == -10.0) || (((x_5 + (-1.0 * _x_x_1)) == -11.0) || (((x_4 + (-1.0 * _x_x_1)) == -7.0) || (((x_2 + (-1.0 * _x_x_1)) == -5.0) || ((x_3 + (-1.0 * _x_x_1)) == -19.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_2)) <= -7.0) && (((x_33 + (-1.0 * _x_x_2)) <= -7.0) && (((x_31 + (-1.0 * _x_x_2)) <= -1.0) && (((x_28 + (-1.0 * _x_x_2)) <= -11.0) && (((x_26 + (-1.0 * _x_x_2)) <= -12.0) && (((x_24 + (-1.0 * _x_x_2)) <= -20.0) && (((x_23 + (-1.0 * _x_x_2)) <= -3.0) && (((x_22 + (-1.0 * _x_x_2)) <= -15.0) && (((x_21 + (-1.0 * _x_x_2)) <= -12.0) && (((x_20 + (-1.0 * _x_x_2)) <= -11.0) && (((x_17 + (-1.0 * _x_x_2)) <= -18.0) && (((x_15 + (-1.0 * _x_x_2)) <= -9.0) && (((x_10 + (-1.0 * _x_x_2)) <= -4.0) && (((x_5 + (-1.0 * _x_x_2)) <= -8.0) && (((x_4 + (-1.0 * _x_x_2)) <= -14.0) && (((x_3 + (-1.0 * _x_x_2)) <= -14.0) && (((x_1 + (-1.0 * _x_x_2)) <= -12.0) && ((x_2 + (-1.0 * _x_x_2)) <= -1.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_2)) == -7.0) || (((x_33 + (-1.0 * _x_x_2)) == -7.0) || (((x_31 + (-1.0 * _x_x_2)) == -1.0) || (((x_28 + (-1.0 * _x_x_2)) == -11.0) || (((x_26 + (-1.0 * _x_x_2)) == -12.0) || (((x_24 + (-1.0 * _x_x_2)) == -20.0) || (((x_23 + (-1.0 * _x_x_2)) == -3.0) || (((x_22 + (-1.0 * _x_x_2)) == -15.0) || (((x_21 + (-1.0 * _x_x_2)) == -12.0) || (((x_20 + (-1.0 * _x_x_2)) == -11.0) || (((x_17 + (-1.0 * _x_x_2)) == -18.0) || (((x_15 + (-1.0 * _x_x_2)) == -9.0) || (((x_10 + (-1.0 * _x_x_2)) == -4.0) || (((x_5 + (-1.0 * _x_x_2)) == -8.0) || (((x_4 + (-1.0 * _x_x_2)) == -14.0) || (((x_3 + (-1.0 * _x_x_2)) == -14.0) || (((x_1 + (-1.0 * _x_x_2)) == -12.0) || ((x_2 + (-1.0 * _x_x_2)) == -1.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_3)) <= -1.0) && (((x_34 + (-1.0 * _x_x_3)) <= -12.0) && (((x_33 + (-1.0 * _x_x_3)) <= -19.0) && (((x_32 + (-1.0 * _x_x_3)) <= -17.0) && (((x_31 + (-1.0 * _x_x_3)) <= -20.0) && (((x_27 + (-1.0 * _x_x_3)) <= -2.0) && (((x_24 + (-1.0 * _x_x_3)) <= -5.0) && (((x_23 + (-1.0 * _x_x_3)) <= -15.0) && (((x_21 + (-1.0 * _x_x_3)) <= -14.0) && (((x_18 + (-1.0 * _x_x_3)) <= -8.0) && (((x_14 + (-1.0 * _x_x_3)) <= -15.0) && (((x_13 + (-1.0 * _x_x_3)) <= -15.0) && (((x_11 + (-1.0 * _x_x_3)) <= -11.0) && (((x_6 + (-1.0 * _x_x_3)) <= -18.0) && (((x_4 + (-1.0 * _x_x_3)) <= -7.0) && (((x_2 + (-1.0 * _x_x_3)) <= -20.0) && (((x_0 + (-1.0 * _x_x_3)) <= -17.0) && ((x_1 + (-1.0 * _x_x_3)) <= -10.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_3)) == -1.0) || (((x_34 + (-1.0 * _x_x_3)) == -12.0) || (((x_33 + (-1.0 * _x_x_3)) == -19.0) || (((x_32 + (-1.0 * _x_x_3)) == -17.0) || (((x_31 + (-1.0 * _x_x_3)) == -20.0) || (((x_27 + (-1.0 * _x_x_3)) == -2.0) || (((x_24 + (-1.0 * _x_x_3)) == -5.0) || (((x_23 + (-1.0 * _x_x_3)) == -15.0) || (((x_21 + (-1.0 * _x_x_3)) == -14.0) || (((x_18 + (-1.0 * _x_x_3)) == -8.0) || (((x_14 + (-1.0 * _x_x_3)) == -15.0) || (((x_13 + (-1.0 * _x_x_3)) == -15.0) || (((x_11 + (-1.0 * _x_x_3)) == -11.0) || (((x_6 + (-1.0 * _x_x_3)) == -18.0) || (((x_4 + (-1.0 * _x_x_3)) == -7.0) || (((x_2 + (-1.0 * _x_x_3)) == -20.0) || (((x_0 + (-1.0 * _x_x_3)) == -17.0) || ((x_1 + (-1.0 * _x_x_3)) == -10.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_4)) <= -15.0) && (((x_30 + (-1.0 * _x_x_4)) <= -14.0) && (((x_27 + (-1.0 * _x_x_4)) <= -2.0) && (((x_25 + (-1.0 * _x_x_4)) <= -16.0) && (((x_23 + (-1.0 * _x_x_4)) <= -14.0) && (((x_22 + (-1.0 * _x_x_4)) <= -13.0) && (((x_18 + (-1.0 * _x_x_4)) <= -6.0) && (((x_17 + (-1.0 * _x_x_4)) <= -13.0) && (((x_16 + (-1.0 * _x_x_4)) <= -19.0) && (((x_11 + (-1.0 * _x_x_4)) <= -9.0) && (((x_8 + (-1.0 * _x_x_4)) <= -14.0) && (((x_7 + (-1.0 * _x_x_4)) <= -20.0) && (((x_6 + (-1.0 * _x_x_4)) <= -14.0) && (((x_5 + (-1.0 * _x_x_4)) <= -12.0) && (((x_4 + (-1.0 * _x_x_4)) <= -1.0) && (((x_2 + (-1.0 * _x_x_4)) <= -12.0) && (((x_0 + (-1.0 * _x_x_4)) <= -15.0) && ((x_1 + (-1.0 * _x_x_4)) <= -19.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_4)) == -15.0) || (((x_30 + (-1.0 * _x_x_4)) == -14.0) || (((x_27 + (-1.0 * _x_x_4)) == -2.0) || (((x_25 + (-1.0 * _x_x_4)) == -16.0) || (((x_23 + (-1.0 * _x_x_4)) == -14.0) || (((x_22 + (-1.0 * _x_x_4)) == -13.0) || (((x_18 + (-1.0 * _x_x_4)) == -6.0) || (((x_17 + (-1.0 * _x_x_4)) == -13.0) || (((x_16 + (-1.0 * _x_x_4)) == -19.0) || (((x_11 + (-1.0 * _x_x_4)) == -9.0) || (((x_8 + (-1.0 * _x_x_4)) == -14.0) || (((x_7 + (-1.0 * _x_x_4)) == -20.0) || (((x_6 + (-1.0 * _x_x_4)) == -14.0) || (((x_5 + (-1.0 * _x_x_4)) == -12.0) || (((x_4 + (-1.0 * _x_x_4)) == -1.0) || (((x_2 + (-1.0 * _x_x_4)) == -12.0) || (((x_0 + (-1.0 * _x_x_4)) == -15.0) || ((x_1 + (-1.0 * _x_x_4)) == -19.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_5)) <= -12.0) && (((x_34 + (-1.0 * _x_x_5)) <= -19.0) && (((x_29 + (-1.0 * _x_x_5)) <= -5.0) && (((x_26 + (-1.0 * _x_x_5)) <= -10.0) && (((x_25 + (-1.0 * _x_x_5)) <= -11.0) && (((x_24 + (-1.0 * _x_x_5)) <= -7.0) && (((x_23 + (-1.0 * _x_x_5)) <= -14.0) && (((x_22 + (-1.0 * _x_x_5)) <= -15.0) && (((x_16 + (-1.0 * _x_x_5)) <= -4.0) && (((x_15 + (-1.0 * _x_x_5)) <= -4.0) && (((x_13 + (-1.0 * _x_x_5)) <= -10.0) && (((x_12 + (-1.0 * _x_x_5)) <= -11.0) && (((x_11 + (-1.0 * _x_x_5)) <= -15.0) && (((x_10 + (-1.0 * _x_x_5)) <= -14.0) && (((x_7 + (-1.0 * _x_x_5)) <= -14.0) && (((x_6 + (-1.0 * _x_x_5)) <= -17.0) && (((x_0 + (-1.0 * _x_x_5)) <= -16.0) && ((x_1 + (-1.0 * _x_x_5)) <= -13.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_5)) == -12.0) || (((x_34 + (-1.0 * _x_x_5)) == -19.0) || (((x_29 + (-1.0 * _x_x_5)) == -5.0) || (((x_26 + (-1.0 * _x_x_5)) == -10.0) || (((x_25 + (-1.0 * _x_x_5)) == -11.0) || (((x_24 + (-1.0 * _x_x_5)) == -7.0) || (((x_23 + (-1.0 * _x_x_5)) == -14.0) || (((x_22 + (-1.0 * _x_x_5)) == -15.0) || (((x_16 + (-1.0 * _x_x_5)) == -4.0) || (((x_15 + (-1.0 * _x_x_5)) == -4.0) || (((x_13 + (-1.0 * _x_x_5)) == -10.0) || (((x_12 + (-1.0 * _x_x_5)) == -11.0) || (((x_11 + (-1.0 * _x_x_5)) == -15.0) || (((x_10 + (-1.0 * _x_x_5)) == -14.0) || (((x_7 + (-1.0 * _x_x_5)) == -14.0) || (((x_6 + (-1.0 * _x_x_5)) == -17.0) || (((x_0 + (-1.0 * _x_x_5)) == -16.0) || ((x_1 + (-1.0 * _x_x_5)) == -13.0)))))))))))))))))))) && ((((x_33 + (-1.0 * _x_x_6)) <= -16.0) && (((x_31 + (-1.0 * _x_x_6)) <= -6.0) && (((x_30 + (-1.0 * _x_x_6)) <= -11.0) && (((x_29 + (-1.0 * _x_x_6)) <= -2.0) && (((x_28 + (-1.0 * _x_x_6)) <= -13.0) && (((x_27 + (-1.0 * _x_x_6)) <= -6.0) && (((x_26 + (-1.0 * _x_x_6)) <= -11.0) && (((x_25 + (-1.0 * _x_x_6)) <= -4.0) && (((x_24 + (-1.0 * _x_x_6)) <= -3.0) && (((x_22 + (-1.0 * _x_x_6)) <= -13.0) && (((x_18 + (-1.0 * _x_x_6)) <= -15.0) && (((x_17 + (-1.0 * _x_x_6)) <= -10.0) && (((x_13 + (-1.0 * _x_x_6)) <= -15.0) && (((x_11 + (-1.0 * _x_x_6)) <= -15.0) && (((x_9 + (-1.0 * _x_x_6)) <= -8.0) && (((x_4 + (-1.0 * _x_x_6)) <= -5.0) && (((x_0 + (-1.0 * _x_x_6)) <= -17.0) && ((x_2 + (-1.0 * _x_x_6)) <= -4.0)))))))))))))))))) && (((x_33 + (-1.0 * _x_x_6)) == -16.0) || (((x_31 + (-1.0 * _x_x_6)) == -6.0) || (((x_30 + (-1.0 * _x_x_6)) == -11.0) || (((x_29 + (-1.0 * _x_x_6)) == -2.0) || (((x_28 + (-1.0 * _x_x_6)) == -13.0) || (((x_27 + (-1.0 * _x_x_6)) == -6.0) || (((x_26 + (-1.0 * _x_x_6)) == -11.0) || (((x_25 + (-1.0 * _x_x_6)) == -4.0) || (((x_24 + (-1.0 * _x_x_6)) == -3.0) || (((x_22 + (-1.0 * _x_x_6)) == -13.0) || (((x_18 + (-1.0 * _x_x_6)) == -15.0) || (((x_17 + (-1.0 * _x_x_6)) == -10.0) || (((x_13 + (-1.0 * _x_x_6)) == -15.0) || (((x_11 + (-1.0 * _x_x_6)) == -15.0) || (((x_9 + (-1.0 * _x_x_6)) == -8.0) || (((x_4 + (-1.0 * _x_x_6)) == -5.0) || (((x_0 + (-1.0 * _x_x_6)) == -17.0) || ((x_2 + (-1.0 * _x_x_6)) == -4.0)))))))))))))))))))) && ((((x_33 + (-1.0 * _x_x_7)) <= -10.0) && (((x_29 + (-1.0 * _x_x_7)) <= -15.0) && (((x_27 + (-1.0 * _x_x_7)) <= -6.0) && (((x_25 + (-1.0 * _x_x_7)) <= -13.0) && (((x_22 + (-1.0 * _x_x_7)) <= -8.0) && (((x_21 + (-1.0 * _x_x_7)) <= -13.0) && (((x_20 + (-1.0 * _x_x_7)) <= -10.0) && (((x_18 + (-1.0 * _x_x_7)) <= -16.0) && (((x_17 + (-1.0 * _x_x_7)) <= -3.0) && (((x_15 + (-1.0 * _x_x_7)) <= -20.0) && (((x_14 + (-1.0 * _x_x_7)) <= -18.0) && (((x_13 + (-1.0 * _x_x_7)) <= -16.0) && (((x_9 + (-1.0 * _x_x_7)) <= -18.0) && (((x_8 + (-1.0 * _x_x_7)) <= -4.0) && (((x_4 + (-1.0 * _x_x_7)) <= -20.0) && (((x_3 + (-1.0 * _x_x_7)) <= -17.0) && (((x_1 + (-1.0 * _x_x_7)) <= -8.0) && ((x_2 + (-1.0 * _x_x_7)) <= -5.0)))))))))))))))))) && (((x_33 + (-1.0 * _x_x_7)) == -10.0) || (((x_29 + (-1.0 * _x_x_7)) == -15.0) || (((x_27 + (-1.0 * _x_x_7)) == -6.0) || (((x_25 + (-1.0 * _x_x_7)) == -13.0) || (((x_22 + (-1.0 * _x_x_7)) == -8.0) || (((x_21 + (-1.0 * _x_x_7)) == -13.0) || (((x_20 + (-1.0 * _x_x_7)) == -10.0) || (((x_18 + (-1.0 * _x_x_7)) == -16.0) || (((x_17 + (-1.0 * _x_x_7)) == -3.0) || (((x_15 + (-1.0 * _x_x_7)) == -20.0) || (((x_14 + (-1.0 * _x_x_7)) == -18.0) || (((x_13 + (-1.0 * _x_x_7)) == -16.0) || (((x_9 + (-1.0 * _x_x_7)) == -18.0) || (((x_8 + (-1.0 * _x_x_7)) == -4.0) || (((x_4 + (-1.0 * _x_x_7)) == -20.0) || (((x_3 + (-1.0 * _x_x_7)) == -17.0) || (((x_1 + (-1.0 * _x_x_7)) == -8.0) || ((x_2 + (-1.0 * _x_x_7)) == -5.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_8)) <= -8.0) && (((x_34 + (-1.0 * _x_x_8)) <= -13.0) && (((x_33 + (-1.0 * _x_x_8)) <= -13.0) && (((x_31 + (-1.0 * _x_x_8)) <= -9.0) && (((x_29 + (-1.0 * _x_x_8)) <= -10.0) && (((x_26 + (-1.0 * _x_x_8)) <= -4.0) && (((x_25 + (-1.0 * _x_x_8)) <= -15.0) && (((x_24 + (-1.0 * _x_x_8)) <= -11.0) && (((x_22 + (-1.0 * _x_x_8)) <= -7.0) && (((x_20 + (-1.0 * _x_x_8)) <= -3.0) && (((x_19 + (-1.0 * _x_x_8)) <= -12.0) && (((x_16 + (-1.0 * _x_x_8)) <= -20.0) && (((x_15 + (-1.0 * _x_x_8)) <= -13.0) && (((x_11 + (-1.0 * _x_x_8)) <= -5.0) && (((x_10 + (-1.0 * _x_x_8)) <= -8.0) && (((x_6 + (-1.0 * _x_x_8)) <= -7.0) && (((x_1 + (-1.0 * _x_x_8)) <= -4.0) && ((x_3 + (-1.0 * _x_x_8)) <= -4.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_8)) == -8.0) || (((x_34 + (-1.0 * _x_x_8)) == -13.0) || (((x_33 + (-1.0 * _x_x_8)) == -13.0) || (((x_31 + (-1.0 * _x_x_8)) == -9.0) || (((x_29 + (-1.0 * _x_x_8)) == -10.0) || (((x_26 + (-1.0 * _x_x_8)) == -4.0) || (((x_25 + (-1.0 * _x_x_8)) == -15.0) || (((x_24 + (-1.0 * _x_x_8)) == -11.0) || (((x_22 + (-1.0 * _x_x_8)) == -7.0) || (((x_20 + (-1.0 * _x_x_8)) == -3.0) || (((x_19 + (-1.0 * _x_x_8)) == -12.0) || (((x_16 + (-1.0 * _x_x_8)) == -20.0) || (((x_15 + (-1.0 * _x_x_8)) == -13.0) || (((x_11 + (-1.0 * _x_x_8)) == -5.0) || (((x_10 + (-1.0 * _x_x_8)) == -8.0) || (((x_6 + (-1.0 * _x_x_8)) == -7.0) || (((x_1 + (-1.0 * _x_x_8)) == -4.0) || ((x_3 + (-1.0 * _x_x_8)) == -4.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_9)) <= -14.0) && (((x_31 + (-1.0 * _x_x_9)) <= -17.0) && (((x_30 + (-1.0 * _x_x_9)) <= -6.0) && (((x_27 + (-1.0 * _x_x_9)) <= -18.0) && (((x_26 + (-1.0 * _x_x_9)) <= -15.0) && (((x_25 + (-1.0 * _x_x_9)) <= -1.0) && (((x_22 + (-1.0 * _x_x_9)) <= -17.0) && (((x_20 + (-1.0 * _x_x_9)) <= -2.0) && (((x_19 + (-1.0 * _x_x_9)) <= -10.0) && (((x_17 + (-1.0 * _x_x_9)) <= -8.0) && (((x_16 + (-1.0 * _x_x_9)) <= -14.0) && (((x_15 + (-1.0 * _x_x_9)) <= -14.0) && (((x_13 + (-1.0 * _x_x_9)) <= -11.0) && (((x_10 + (-1.0 * _x_x_9)) <= -14.0) && (((x_8 + (-1.0 * _x_x_9)) <= -18.0) && (((x_7 + (-1.0 * _x_x_9)) <= -14.0) && (((x_3 + (-1.0 * _x_x_9)) <= -5.0) && ((x_4 + (-1.0 * _x_x_9)) <= -11.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_9)) == -14.0) || (((x_31 + (-1.0 * _x_x_9)) == -17.0) || (((x_30 + (-1.0 * _x_x_9)) == -6.0) || (((x_27 + (-1.0 * _x_x_9)) == -18.0) || (((x_26 + (-1.0 * _x_x_9)) == -15.0) || (((x_25 + (-1.0 * _x_x_9)) == -1.0) || (((x_22 + (-1.0 * _x_x_9)) == -17.0) || (((x_20 + (-1.0 * _x_x_9)) == -2.0) || (((x_19 + (-1.0 * _x_x_9)) == -10.0) || (((x_17 + (-1.0 * _x_x_9)) == -8.0) || (((x_16 + (-1.0 * _x_x_9)) == -14.0) || (((x_15 + (-1.0 * _x_x_9)) == -14.0) || (((x_13 + (-1.0 * _x_x_9)) == -11.0) || (((x_10 + (-1.0 * _x_x_9)) == -14.0) || (((x_8 + (-1.0 * _x_x_9)) == -18.0) || (((x_7 + (-1.0 * _x_x_9)) == -14.0) || (((x_3 + (-1.0 * _x_x_9)) == -5.0) || ((x_4 + (-1.0 * _x_x_9)) == -11.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_10)) <= -13.0) && (((x_34 + (-1.0 * _x_x_10)) <= -9.0) && (((x_33 + (-1.0 * _x_x_10)) <= -19.0) && (((x_32 + (-1.0 * _x_x_10)) <= -4.0) && (((x_30 + (-1.0 * _x_x_10)) <= -18.0) && (((x_27 + (-1.0 * _x_x_10)) <= -7.0) && (((x_25 + (-1.0 * _x_x_10)) <= -14.0) && (((x_24 + (-1.0 * _x_x_10)) <= -6.0) && (((x_23 + (-1.0 * _x_x_10)) <= -1.0) && (((x_21 + (-1.0 * _x_x_10)) <= -7.0) && (((x_20 + (-1.0 * _x_x_10)) <= -2.0) && (((x_18 + (-1.0 * _x_x_10)) <= -4.0) && (((x_16 + (-1.0 * _x_x_10)) <= -17.0) && (((x_14 + (-1.0 * _x_x_10)) <= -19.0) && (((x_8 + (-1.0 * _x_x_10)) <= -20.0) && (((x_7 + (-1.0 * _x_x_10)) <= -3.0) && (((x_3 + (-1.0 * _x_x_10)) <= -11.0) && ((x_4 + (-1.0 * _x_x_10)) <= -11.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_10)) == -13.0) || (((x_34 + (-1.0 * _x_x_10)) == -9.0) || (((x_33 + (-1.0 * _x_x_10)) == -19.0) || (((x_32 + (-1.0 * _x_x_10)) == -4.0) || (((x_30 + (-1.0 * _x_x_10)) == -18.0) || (((x_27 + (-1.0 * _x_x_10)) == -7.0) || (((x_25 + (-1.0 * _x_x_10)) == -14.0) || (((x_24 + (-1.0 * _x_x_10)) == -6.0) || (((x_23 + (-1.0 * _x_x_10)) == -1.0) || (((x_21 + (-1.0 * _x_x_10)) == -7.0) || (((x_20 + (-1.0 * _x_x_10)) == -2.0) || (((x_18 + (-1.0 * _x_x_10)) == -4.0) || (((x_16 + (-1.0 * _x_x_10)) == -17.0) || (((x_14 + (-1.0 * _x_x_10)) == -19.0) || (((x_8 + (-1.0 * _x_x_10)) == -20.0) || (((x_7 + (-1.0 * _x_x_10)) == -3.0) || (((x_3 + (-1.0 * _x_x_10)) == -11.0) || ((x_4 + (-1.0 * _x_x_10)) == -11.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_11)) <= -5.0) && (((x_33 + (-1.0 * _x_x_11)) <= -5.0) && (((x_30 + (-1.0 * _x_x_11)) <= -16.0) && (((x_28 + (-1.0 * _x_x_11)) <= -4.0) && (((x_27 + (-1.0 * _x_x_11)) <= -4.0) && (((x_25 + (-1.0 * _x_x_11)) <= -13.0) && (((x_24 + (-1.0 * _x_x_11)) <= -19.0) && (((x_23 + (-1.0 * _x_x_11)) <= -2.0) && (((x_22 + (-1.0 * _x_x_11)) <= -11.0) && (((x_21 + (-1.0 * _x_x_11)) <= -12.0) && (((x_17 + (-1.0 * _x_x_11)) <= -20.0) && (((x_11 + (-1.0 * _x_x_11)) <= -9.0) && (((x_10 + (-1.0 * _x_x_11)) <= -7.0) && (((x_7 + (-1.0 * _x_x_11)) <= -10.0) && (((x_6 + (-1.0 * _x_x_11)) <= -10.0) && (((x_5 + (-1.0 * _x_x_11)) <= -5.0) && (((x_3 + (-1.0 * _x_x_11)) <= -13.0) && ((x_4 + (-1.0 * _x_x_11)) <= -15.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_11)) == -5.0) || (((x_33 + (-1.0 * _x_x_11)) == -5.0) || (((x_30 + (-1.0 * _x_x_11)) == -16.0) || (((x_28 + (-1.0 * _x_x_11)) == -4.0) || (((x_27 + (-1.0 * _x_x_11)) == -4.0) || (((x_25 + (-1.0 * _x_x_11)) == -13.0) || (((x_24 + (-1.0 * _x_x_11)) == -19.0) || (((x_23 + (-1.0 * _x_x_11)) == -2.0) || (((x_22 + (-1.0 * _x_x_11)) == -11.0) || (((x_21 + (-1.0 * _x_x_11)) == -12.0) || (((x_17 + (-1.0 * _x_x_11)) == -20.0) || (((x_11 + (-1.0 * _x_x_11)) == -9.0) || (((x_10 + (-1.0 * _x_x_11)) == -7.0) || (((x_7 + (-1.0 * _x_x_11)) == -10.0) || (((x_6 + (-1.0 * _x_x_11)) == -10.0) || (((x_5 + (-1.0 * _x_x_11)) == -5.0) || (((x_3 + (-1.0 * _x_x_11)) == -13.0) || ((x_4 + (-1.0 * _x_x_11)) == -15.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_12)) <= -7.0) && (((x_34 + (-1.0 * _x_x_12)) <= -15.0) && (((x_33 + (-1.0 * _x_x_12)) <= -14.0) && (((x_30 + (-1.0 * _x_x_12)) <= -18.0) && (((x_27 + (-1.0 * _x_x_12)) <= -15.0) && (((x_24 + (-1.0 * _x_x_12)) <= -2.0) && (((x_23 + (-1.0 * _x_x_12)) <= -1.0) && (((x_22 + (-1.0 * _x_x_12)) <= -20.0) && (((x_21 + (-1.0 * _x_x_12)) <= -14.0) && (((x_15 + (-1.0 * _x_x_12)) <= -6.0) && (((x_14 + (-1.0 * _x_x_12)) <= -6.0) && (((x_13 + (-1.0 * _x_x_12)) <= -2.0) && (((x_12 + (-1.0 * _x_x_12)) <= -2.0) && (((x_10 + (-1.0 * _x_x_12)) <= -20.0) && (((x_7 + (-1.0 * _x_x_12)) <= -13.0) && (((x_4 + (-1.0 * _x_x_12)) <= -5.0) && (((x_1 + (-1.0 * _x_x_12)) <= -8.0) && ((x_3 + (-1.0 * _x_x_12)) <= -17.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_12)) == -7.0) || (((x_34 + (-1.0 * _x_x_12)) == -15.0) || (((x_33 + (-1.0 * _x_x_12)) == -14.0) || (((x_30 + (-1.0 * _x_x_12)) == -18.0) || (((x_27 + (-1.0 * _x_x_12)) == -15.0) || (((x_24 + (-1.0 * _x_x_12)) == -2.0) || (((x_23 + (-1.0 * _x_x_12)) == -1.0) || (((x_22 + (-1.0 * _x_x_12)) == -20.0) || (((x_21 + (-1.0 * _x_x_12)) == -14.0) || (((x_15 + (-1.0 * _x_x_12)) == -6.0) || (((x_14 + (-1.0 * _x_x_12)) == -6.0) || (((x_13 + (-1.0 * _x_x_12)) == -2.0) || (((x_12 + (-1.0 * _x_x_12)) == -2.0) || (((x_10 + (-1.0 * _x_x_12)) == -20.0) || (((x_7 + (-1.0 * _x_x_12)) == -13.0) || (((x_4 + (-1.0 * _x_x_12)) == -5.0) || (((x_1 + (-1.0 * _x_x_12)) == -8.0) || ((x_3 + (-1.0 * _x_x_12)) == -17.0)))))))))))))))))))) && ((((x_32 + (-1.0 * _x_x_13)) <= -14.0) && (((x_31 + (-1.0 * _x_x_13)) <= -3.0) && (((x_30 + (-1.0 * _x_x_13)) <= -12.0) && (((x_29 + (-1.0 * _x_x_13)) <= -4.0) && (((x_24 + (-1.0 * _x_x_13)) <= -20.0) && (((x_23 + (-1.0 * _x_x_13)) <= -5.0) && (((x_19 + (-1.0 * _x_x_13)) <= -20.0) && (((x_18 + (-1.0 * _x_x_13)) <= -16.0) && (((x_16 + (-1.0 * _x_x_13)) <= -8.0) && (((x_15 + (-1.0 * _x_x_13)) <= -17.0) && (((x_14 + (-1.0 * _x_x_13)) <= -18.0) && (((x_12 + (-1.0 * _x_x_13)) <= -4.0) && (((x_11 + (-1.0 * _x_x_13)) <= -4.0) && (((x_10 + (-1.0 * _x_x_13)) <= -4.0) && (((x_6 + (-1.0 * _x_x_13)) <= -10.0) && (((x_5 + (-1.0 * _x_x_13)) <= -8.0) && (((x_2 + (-1.0 * _x_x_13)) <= -3.0) && ((x_3 + (-1.0 * _x_x_13)) <= -14.0)))))))))))))))))) && (((x_32 + (-1.0 * _x_x_13)) == -14.0) || (((x_31 + (-1.0 * _x_x_13)) == -3.0) || (((x_30 + (-1.0 * _x_x_13)) == -12.0) || (((x_29 + (-1.0 * _x_x_13)) == -4.0) || (((x_24 + (-1.0 * _x_x_13)) == -20.0) || (((x_23 + (-1.0 * _x_x_13)) == -5.0) || (((x_19 + (-1.0 * _x_x_13)) == -20.0) || (((x_18 + (-1.0 * _x_x_13)) == -16.0) || (((x_16 + (-1.0 * _x_x_13)) == -8.0) || (((x_15 + (-1.0 * _x_x_13)) == -17.0) || (((x_14 + (-1.0 * _x_x_13)) == -18.0) || (((x_12 + (-1.0 * _x_x_13)) == -4.0) || (((x_11 + (-1.0 * _x_x_13)) == -4.0) || (((x_10 + (-1.0 * _x_x_13)) == -4.0) || (((x_6 + (-1.0 * _x_x_13)) == -10.0) || (((x_5 + (-1.0 * _x_x_13)) == -8.0) || (((x_2 + (-1.0 * _x_x_13)) == -3.0) || ((x_3 + (-1.0 * _x_x_13)) == -14.0)))))))))))))))))))) && ((((x_33 + (-1.0 * _x_x_14)) <= -8.0) && (((x_31 + (-1.0 * _x_x_14)) <= -12.0) && (((x_30 + (-1.0 * _x_x_14)) <= -1.0) && (((x_28 + (-1.0 * _x_x_14)) <= -3.0) && (((x_25 + (-1.0 * _x_x_14)) <= -5.0) && (((x_24 + (-1.0 * _x_x_14)) <= -4.0) && (((x_23 + (-1.0 * _x_x_14)) <= -16.0) && (((x_22 + (-1.0 * _x_x_14)) <= -18.0) && (((x_19 + (-1.0 * _x_x_14)) <= -12.0) && (((x_17 + (-1.0 * _x_x_14)) <= -10.0) && (((x_16 + (-1.0 * _x_x_14)) <= -20.0) && (((x_13 + (-1.0 * _x_x_14)) <= -16.0) && (((x_11 + (-1.0 * _x_x_14)) <= -11.0) && (((x_10 + (-1.0 * _x_x_14)) <= -3.0) && (((x_8 + (-1.0 * _x_x_14)) <= -3.0) && (((x_7 + (-1.0 * _x_x_14)) <= -3.0) && (((x_4 + (-1.0 * _x_x_14)) <= -18.0) && ((x_6 + (-1.0 * _x_x_14)) <= -18.0)))))))))))))))))) && (((x_33 + (-1.0 * _x_x_14)) == -8.0) || (((x_31 + (-1.0 * _x_x_14)) == -12.0) || (((x_30 + (-1.0 * _x_x_14)) == -1.0) || (((x_28 + (-1.0 * _x_x_14)) == -3.0) || (((x_25 + (-1.0 * _x_x_14)) == -5.0) || (((x_24 + (-1.0 * _x_x_14)) == -4.0) || (((x_23 + (-1.0 * _x_x_14)) == -16.0) || (((x_22 + (-1.0 * _x_x_14)) == -18.0) || (((x_19 + (-1.0 * _x_x_14)) == -12.0) || (((x_17 + (-1.0 * _x_x_14)) == -10.0) || (((x_16 + (-1.0 * _x_x_14)) == -20.0) || (((x_13 + (-1.0 * _x_x_14)) == -16.0) || (((x_11 + (-1.0 * _x_x_14)) == -11.0) || (((x_10 + (-1.0 * _x_x_14)) == -3.0) || (((x_8 + (-1.0 * _x_x_14)) == -3.0) || (((x_7 + (-1.0 * _x_x_14)) == -3.0) || (((x_4 + (-1.0 * _x_x_14)) == -18.0) || ((x_6 + (-1.0 * _x_x_14)) == -18.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_15)) <= -5.0) && (((x_30 + (-1.0 * _x_x_15)) <= -5.0) && (((x_29 + (-1.0 * _x_x_15)) <= -13.0) && (((x_28 + (-1.0 * _x_x_15)) <= -13.0) && (((x_26 + (-1.0 * _x_x_15)) <= -8.0) && (((x_25 + (-1.0 * _x_x_15)) <= -16.0) && (((x_24 + (-1.0 * _x_x_15)) <= -9.0) && (((x_23 + (-1.0 * _x_x_15)) <= -15.0) && (((x_19 + (-1.0 * _x_x_15)) <= -14.0) && (((x_17 + (-1.0 * _x_x_15)) <= -19.0) && (((x_15 + (-1.0 * _x_x_15)) <= -12.0) && (((x_13 + (-1.0 * _x_x_15)) <= -16.0) && (((x_9 + (-1.0 * _x_x_15)) <= -11.0) && (((x_8 + (-1.0 * _x_x_15)) <= -5.0) && (((x_7 + (-1.0 * _x_x_15)) <= -3.0) && (((x_5 + (-1.0 * _x_x_15)) <= -5.0) && (((x_1 + (-1.0 * _x_x_15)) <= -5.0) && ((x_2 + (-1.0 * _x_x_15)) <= -20.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_15)) == -5.0) || (((x_30 + (-1.0 * _x_x_15)) == -5.0) || (((x_29 + (-1.0 * _x_x_15)) == -13.0) || (((x_28 + (-1.0 * _x_x_15)) == -13.0) || (((x_26 + (-1.0 * _x_x_15)) == -8.0) || (((x_25 + (-1.0 * _x_x_15)) == -16.0) || (((x_24 + (-1.0 * _x_x_15)) == -9.0) || (((x_23 + (-1.0 * _x_x_15)) == -15.0) || (((x_19 + (-1.0 * _x_x_15)) == -14.0) || (((x_17 + (-1.0 * _x_x_15)) == -19.0) || (((x_15 + (-1.0 * _x_x_15)) == -12.0) || (((x_13 + (-1.0 * _x_x_15)) == -16.0) || (((x_9 + (-1.0 * _x_x_15)) == -11.0) || (((x_8 + (-1.0 * _x_x_15)) == -5.0) || (((x_7 + (-1.0 * _x_x_15)) == -3.0) || (((x_5 + (-1.0 * _x_x_15)) == -5.0) || (((x_1 + (-1.0 * _x_x_15)) == -5.0) || ((x_2 + (-1.0 * _x_x_15)) == -20.0)))))))))))))))))))) && ((((x_29 + (-1.0 * _x_x_16)) <= -11.0) && (((x_27 + (-1.0 * _x_x_16)) <= -17.0) && (((x_26 + (-1.0 * _x_x_16)) <= -12.0) && (((x_25 + (-1.0 * _x_x_16)) <= -5.0) && (((x_24 + (-1.0 * _x_x_16)) <= -19.0) && (((x_21 + (-1.0 * _x_x_16)) <= -15.0) && (((x_18 + (-1.0 * _x_x_16)) <= -14.0) && (((x_17 + (-1.0 * _x_x_16)) <= -12.0) && (((x_15 + (-1.0 * _x_x_16)) <= -18.0) && (((x_14 + (-1.0 * _x_x_16)) <= -12.0) && (((x_12 + (-1.0 * _x_x_16)) <= -4.0) && (((x_10 + (-1.0 * _x_x_16)) <= -12.0) && (((x_9 + (-1.0 * _x_x_16)) <= -6.0) && (((x_7 + (-1.0 * _x_x_16)) <= -2.0) && (((x_4 + (-1.0 * _x_x_16)) <= -10.0) && (((x_3 + (-1.0 * _x_x_16)) <= -15.0) && (((x_0 + (-1.0 * _x_x_16)) <= -10.0) && ((x_2 + (-1.0 * _x_x_16)) <= -10.0)))))))))))))))))) && (((x_29 + (-1.0 * _x_x_16)) == -11.0) || (((x_27 + (-1.0 * _x_x_16)) == -17.0) || (((x_26 + (-1.0 * _x_x_16)) == -12.0) || (((x_25 + (-1.0 * _x_x_16)) == -5.0) || (((x_24 + (-1.0 * _x_x_16)) == -19.0) || (((x_21 + (-1.0 * _x_x_16)) == -15.0) || (((x_18 + (-1.0 * _x_x_16)) == -14.0) || (((x_17 + (-1.0 * _x_x_16)) == -12.0) || (((x_15 + (-1.0 * _x_x_16)) == -18.0) || (((x_14 + (-1.0 * _x_x_16)) == -12.0) || (((x_12 + (-1.0 * _x_x_16)) == -4.0) || (((x_10 + (-1.0 * _x_x_16)) == -12.0) || (((x_9 + (-1.0 * _x_x_16)) == -6.0) || (((x_7 + (-1.0 * _x_x_16)) == -2.0) || (((x_4 + (-1.0 * _x_x_16)) == -10.0) || (((x_3 + (-1.0 * _x_x_16)) == -15.0) || (((x_0 + (-1.0 * _x_x_16)) == -10.0) || ((x_2 + (-1.0 * _x_x_16)) == -10.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_17)) <= -19.0) && (((x_33 + (-1.0 * _x_x_17)) <= -15.0) && (((x_32 + (-1.0 * _x_x_17)) <= -8.0) && (((x_30 + (-1.0 * _x_x_17)) <= -4.0) && (((x_29 + (-1.0 * _x_x_17)) <= -19.0) && (((x_27 + (-1.0 * _x_x_17)) <= -19.0) && (((x_21 + (-1.0 * _x_x_17)) <= -12.0) && (((x_20 + (-1.0 * _x_x_17)) <= -14.0) && (((x_17 + (-1.0 * _x_x_17)) <= -18.0) && (((x_14 + (-1.0 * _x_x_17)) <= -14.0) && (((x_13 + (-1.0 * _x_x_17)) <= -16.0) && (((x_10 + (-1.0 * _x_x_17)) <= -8.0) && (((x_8 + (-1.0 * _x_x_17)) <= -5.0) && (((x_7 + (-1.0 * _x_x_17)) <= -1.0) && (((x_5 + (-1.0 * _x_x_17)) <= -1.0) && (((x_4 + (-1.0 * _x_x_17)) <= -14.0) && (((x_0 + (-1.0 * _x_x_17)) <= -20.0) && ((x_1 + (-1.0 * _x_x_17)) <= -1.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_17)) == -19.0) || (((x_33 + (-1.0 * _x_x_17)) == -15.0) || (((x_32 + (-1.0 * _x_x_17)) == -8.0) || (((x_30 + (-1.0 * _x_x_17)) == -4.0) || (((x_29 + (-1.0 * _x_x_17)) == -19.0) || (((x_27 + (-1.0 * _x_x_17)) == -19.0) || (((x_21 + (-1.0 * _x_x_17)) == -12.0) || (((x_20 + (-1.0 * _x_x_17)) == -14.0) || (((x_17 + (-1.0 * _x_x_17)) == -18.0) || (((x_14 + (-1.0 * _x_x_17)) == -14.0) || (((x_13 + (-1.0 * _x_x_17)) == -16.0) || (((x_10 + (-1.0 * _x_x_17)) == -8.0) || (((x_8 + (-1.0 * _x_x_17)) == -5.0) || (((x_7 + (-1.0 * _x_x_17)) == -1.0) || (((x_5 + (-1.0 * _x_x_17)) == -1.0) || (((x_4 + (-1.0 * _x_x_17)) == -14.0) || (((x_0 + (-1.0 * _x_x_17)) == -20.0) || ((x_1 + (-1.0 * _x_x_17)) == -1.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_18)) <= -10.0) && (((x_33 + (-1.0 * _x_x_18)) <= -7.0) && (((x_32 + (-1.0 * _x_x_18)) <= -14.0) && (((x_31 + (-1.0 * _x_x_18)) <= -12.0) && (((x_28 + (-1.0 * _x_x_18)) <= -9.0) && (((x_26 + (-1.0 * _x_x_18)) <= -2.0) && (((x_24 + (-1.0 * _x_x_18)) <= -2.0) && (((x_21 + (-1.0 * _x_x_18)) <= -19.0) && (((x_20 + (-1.0 * _x_x_18)) <= -13.0) && (((x_19 + (-1.0 * _x_x_18)) <= -13.0) && (((x_18 + (-1.0 * _x_x_18)) <= -14.0) && (((x_17 + (-1.0 * _x_x_18)) <= -12.0) && (((x_10 + (-1.0 * _x_x_18)) <= -17.0) && (((x_7 + (-1.0 * _x_x_18)) <= -5.0) && (((x_6 + (-1.0 * _x_x_18)) <= -18.0) && (((x_5 + (-1.0 * _x_x_18)) <= -3.0) && (((x_1 + (-1.0 * _x_x_18)) <= -13.0) && ((x_3 + (-1.0 * _x_x_18)) <= -16.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_18)) == -10.0) || (((x_33 + (-1.0 * _x_x_18)) == -7.0) || (((x_32 + (-1.0 * _x_x_18)) == -14.0) || (((x_31 + (-1.0 * _x_x_18)) == -12.0) || (((x_28 + (-1.0 * _x_x_18)) == -9.0) || (((x_26 + (-1.0 * _x_x_18)) == -2.0) || (((x_24 + (-1.0 * _x_x_18)) == -2.0) || (((x_21 + (-1.0 * _x_x_18)) == -19.0) || (((x_20 + (-1.0 * _x_x_18)) == -13.0) || (((x_19 + (-1.0 * _x_x_18)) == -13.0) || (((x_18 + (-1.0 * _x_x_18)) == -14.0) || (((x_17 + (-1.0 * _x_x_18)) == -12.0) || (((x_10 + (-1.0 * _x_x_18)) == -17.0) || (((x_7 + (-1.0 * _x_x_18)) == -5.0) || (((x_6 + (-1.0 * _x_x_18)) == -18.0) || (((x_5 + (-1.0 * _x_x_18)) == -3.0) || (((x_1 + (-1.0 * _x_x_18)) == -13.0) || ((x_3 + (-1.0 * _x_x_18)) == -16.0)))))))))))))))))))) && ((((x_31 + (-1.0 * _x_x_19)) <= -19.0) && (((x_29 + (-1.0 * _x_x_19)) <= -6.0) && (((x_27 + (-1.0 * _x_x_19)) <= -13.0) && (((x_25 + (-1.0 * _x_x_19)) <= -5.0) && (((x_24 + (-1.0 * _x_x_19)) <= -4.0) && (((x_23 + (-1.0 * _x_x_19)) <= -3.0) && (((x_20 + (-1.0 * _x_x_19)) <= -19.0) && (((x_19 + (-1.0 * _x_x_19)) <= -12.0) && (((x_17 + (-1.0 * _x_x_19)) <= -18.0) && (((x_16 + (-1.0 * _x_x_19)) <= -18.0) && (((x_13 + (-1.0 * _x_x_19)) <= -10.0) && (((x_10 + (-1.0 * _x_x_19)) <= -12.0) && (((x_9 + (-1.0 * _x_x_19)) <= -9.0) && (((x_8 + (-1.0 * _x_x_19)) <= -8.0) && (((x_5 + (-1.0 * _x_x_19)) <= -6.0) && (((x_4 + (-1.0 * _x_x_19)) <= -13.0) && (((x_1 + (-1.0 * _x_x_19)) <= -3.0) && ((x_3 + (-1.0 * _x_x_19)) <= -13.0)))))))))))))))))) && (((x_31 + (-1.0 * _x_x_19)) == -19.0) || (((x_29 + (-1.0 * _x_x_19)) == -6.0) || (((x_27 + (-1.0 * _x_x_19)) == -13.0) || (((x_25 + (-1.0 * _x_x_19)) == -5.0) || (((x_24 + (-1.0 * _x_x_19)) == -4.0) || (((x_23 + (-1.0 * _x_x_19)) == -3.0) || (((x_20 + (-1.0 * _x_x_19)) == -19.0) || (((x_19 + (-1.0 * _x_x_19)) == -12.0) || (((x_17 + (-1.0 * _x_x_19)) == -18.0) || (((x_16 + (-1.0 * _x_x_19)) == -18.0) || (((x_13 + (-1.0 * _x_x_19)) == -10.0) || (((x_10 + (-1.0 * _x_x_19)) == -12.0) || (((x_9 + (-1.0 * _x_x_19)) == -9.0) || (((x_8 + (-1.0 * _x_x_19)) == -8.0) || (((x_5 + (-1.0 * _x_x_19)) == -6.0) || (((x_4 + (-1.0 * _x_x_19)) == -13.0) || (((x_1 + (-1.0 * _x_x_19)) == -3.0) || ((x_3 + (-1.0 * _x_x_19)) == -13.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_20)) <= -15.0) && (((x_31 + (-1.0 * _x_x_20)) <= -11.0) && (((x_28 + (-1.0 * _x_x_20)) <= -11.0) && (((x_26 + (-1.0 * _x_x_20)) <= -4.0) && (((x_24 + (-1.0 * _x_x_20)) <= -19.0) && (((x_23 + (-1.0 * _x_x_20)) <= -19.0) && (((x_21 + (-1.0 * _x_x_20)) <= -14.0) && (((x_20 + (-1.0 * _x_x_20)) <= -5.0) && (((x_19 + (-1.0 * _x_x_20)) <= -1.0) && (((x_18 + (-1.0 * _x_x_20)) <= -6.0) && (((x_16 + (-1.0 * _x_x_20)) <= -7.0) && (((x_13 + (-1.0 * _x_x_20)) <= -4.0) && (((x_11 + (-1.0 * _x_x_20)) <= -19.0) && (((x_10 + (-1.0 * _x_x_20)) <= -11.0) && (((x_9 + (-1.0 * _x_x_20)) <= -17.0) && (((x_7 + (-1.0 * _x_x_20)) <= -6.0) && (((x_2 + (-1.0 * _x_x_20)) <= -20.0) && ((x_3 + (-1.0 * _x_x_20)) <= -20.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_20)) == -15.0) || (((x_31 + (-1.0 * _x_x_20)) == -11.0) || (((x_28 + (-1.0 * _x_x_20)) == -11.0) || (((x_26 + (-1.0 * _x_x_20)) == -4.0) || (((x_24 + (-1.0 * _x_x_20)) == -19.0) || (((x_23 + (-1.0 * _x_x_20)) == -19.0) || (((x_21 + (-1.0 * _x_x_20)) == -14.0) || (((x_20 + (-1.0 * _x_x_20)) == -5.0) || (((x_19 + (-1.0 * _x_x_20)) == -1.0) || (((x_18 + (-1.0 * _x_x_20)) == -6.0) || (((x_16 + (-1.0 * _x_x_20)) == -7.0) || (((x_13 + (-1.0 * _x_x_20)) == -4.0) || (((x_11 + (-1.0 * _x_x_20)) == -19.0) || (((x_10 + (-1.0 * _x_x_20)) == -11.0) || (((x_9 + (-1.0 * _x_x_20)) == -17.0) || (((x_7 + (-1.0 * _x_x_20)) == -6.0) || (((x_2 + (-1.0 * _x_x_20)) == -20.0) || ((x_3 + (-1.0 * _x_x_20)) == -20.0)))))))))))))))))))) && ((((x_33 + (-1.0 * _x_x_21)) <= -3.0) && (((x_31 + (-1.0 * _x_x_21)) <= -8.0) && (((x_30 + (-1.0 * _x_x_21)) <= -13.0) && (((x_29 + (-1.0 * _x_x_21)) <= -8.0) && (((x_26 + (-1.0 * _x_x_21)) <= -12.0) && (((x_25 + (-1.0 * _x_x_21)) <= -12.0) && (((x_24 + (-1.0 * _x_x_21)) <= -19.0) && (((x_23 + (-1.0 * _x_x_21)) <= -8.0) && (((x_20 + (-1.0 * _x_x_21)) <= -17.0) && (((x_19 + (-1.0 * _x_x_21)) <= -17.0) && (((x_18 + (-1.0 * _x_x_21)) <= -11.0) && (((x_13 + (-1.0 * _x_x_21)) <= -8.0) && (((x_11 + (-1.0 * _x_x_21)) <= -6.0) && (((x_10 + (-1.0 * _x_x_21)) <= -15.0) && (((x_8 + (-1.0 * _x_x_21)) <= -17.0) && (((x_6 + (-1.0 * _x_x_21)) <= -3.0) && (((x_1 + (-1.0 * _x_x_21)) <= -11.0) && ((x_4 + (-1.0 * _x_x_21)) <= -16.0)))))))))))))))))) && (((x_33 + (-1.0 * _x_x_21)) == -3.0) || (((x_31 + (-1.0 * _x_x_21)) == -8.0) || (((x_30 + (-1.0 * _x_x_21)) == -13.0) || (((x_29 + (-1.0 * _x_x_21)) == -8.0) || (((x_26 + (-1.0 * _x_x_21)) == -12.0) || (((x_25 + (-1.0 * _x_x_21)) == -12.0) || (((x_24 + (-1.0 * _x_x_21)) == -19.0) || (((x_23 + (-1.0 * _x_x_21)) == -8.0) || (((x_20 + (-1.0 * _x_x_21)) == -17.0) || (((x_19 + (-1.0 * _x_x_21)) == -17.0) || (((x_18 + (-1.0 * _x_x_21)) == -11.0) || (((x_13 + (-1.0 * _x_x_21)) == -8.0) || (((x_11 + (-1.0 * _x_x_21)) == -6.0) || (((x_10 + (-1.0 * _x_x_21)) == -15.0) || (((x_8 + (-1.0 * _x_x_21)) == -17.0) || (((x_6 + (-1.0 * _x_x_21)) == -3.0) || (((x_1 + (-1.0 * _x_x_21)) == -11.0) || ((x_4 + (-1.0 * _x_x_21)) == -16.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_22)) <= -20.0) && (((x_34 + (-1.0 * _x_x_22)) <= -11.0) && (((x_33 + (-1.0 * _x_x_22)) <= -10.0) && (((x_32 + (-1.0 * _x_x_22)) <= -17.0) && (((x_30 + (-1.0 * _x_x_22)) <= -19.0) && (((x_29 + (-1.0 * _x_x_22)) <= -3.0) && (((x_26 + (-1.0 * _x_x_22)) <= -1.0) && (((x_24 + (-1.0 * _x_x_22)) <= -7.0) && (((x_23 + (-1.0 * _x_x_22)) <= -9.0) && (((x_21 + (-1.0 * _x_x_22)) <= -19.0) && (((x_20 + (-1.0 * _x_x_22)) <= -16.0) && (((x_17 + (-1.0 * _x_x_22)) <= -5.0) && (((x_11 + (-1.0 * _x_x_22)) <= -11.0) && (((x_9 + (-1.0 * _x_x_22)) <= -5.0) && (((x_8 + (-1.0 * _x_x_22)) <= -6.0) && (((x_6 + (-1.0 * _x_x_22)) <= -8.0) && (((x_4 + (-1.0 * _x_x_22)) <= -14.0) && ((x_5 + (-1.0 * _x_x_22)) <= -7.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_22)) == -20.0) || (((x_34 + (-1.0 * _x_x_22)) == -11.0) || (((x_33 + (-1.0 * _x_x_22)) == -10.0) || (((x_32 + (-1.0 * _x_x_22)) == -17.0) || (((x_30 + (-1.0 * _x_x_22)) == -19.0) || (((x_29 + (-1.0 * _x_x_22)) == -3.0) || (((x_26 + (-1.0 * _x_x_22)) == -1.0) || (((x_24 + (-1.0 * _x_x_22)) == -7.0) || (((x_23 + (-1.0 * _x_x_22)) == -9.0) || (((x_21 + (-1.0 * _x_x_22)) == -19.0) || (((x_20 + (-1.0 * _x_x_22)) == -16.0) || (((x_17 + (-1.0 * _x_x_22)) == -5.0) || (((x_11 + (-1.0 * _x_x_22)) == -11.0) || (((x_9 + (-1.0 * _x_x_22)) == -5.0) || (((x_8 + (-1.0 * _x_x_22)) == -6.0) || (((x_6 + (-1.0 * _x_x_22)) == -8.0) || (((x_4 + (-1.0 * _x_x_22)) == -14.0) || ((x_5 + (-1.0 * _x_x_22)) == -7.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_23)) <= -16.0) && (((x_34 + (-1.0 * _x_x_23)) <= -20.0) && (((x_32 + (-1.0 * _x_x_23)) <= -6.0) && (((x_31 + (-1.0 * _x_x_23)) <= -1.0) && (((x_30 + (-1.0 * _x_x_23)) <= -9.0) && (((x_27 + (-1.0 * _x_x_23)) <= -19.0) && (((x_26 + (-1.0 * _x_x_23)) <= -15.0) && (((x_25 + (-1.0 * _x_x_23)) <= -3.0) && (((x_23 + (-1.0 * _x_x_23)) <= -9.0) && (((x_22 + (-1.0 * _x_x_23)) <= -6.0) && (((x_20 + (-1.0 * _x_x_23)) <= -1.0) && (((x_12 + (-1.0 * _x_x_23)) <= -18.0) && (((x_11 + (-1.0 * _x_x_23)) <= -19.0) && (((x_10 + (-1.0 * _x_x_23)) <= -3.0) && (((x_9 + (-1.0 * _x_x_23)) <= -10.0) && (((x_6 + (-1.0 * _x_x_23)) <= -14.0) && (((x_1 + (-1.0 * _x_x_23)) <= -7.0) && ((x_3 + (-1.0 * _x_x_23)) <= -19.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_23)) == -16.0) || (((x_34 + (-1.0 * _x_x_23)) == -20.0) || (((x_32 + (-1.0 * _x_x_23)) == -6.0) || (((x_31 + (-1.0 * _x_x_23)) == -1.0) || (((x_30 + (-1.0 * _x_x_23)) == -9.0) || (((x_27 + (-1.0 * _x_x_23)) == -19.0) || (((x_26 + (-1.0 * _x_x_23)) == -15.0) || (((x_25 + (-1.0 * _x_x_23)) == -3.0) || (((x_23 + (-1.0 * _x_x_23)) == -9.0) || (((x_22 + (-1.0 * _x_x_23)) == -6.0) || (((x_20 + (-1.0 * _x_x_23)) == -1.0) || (((x_12 + (-1.0 * _x_x_23)) == -18.0) || (((x_11 + (-1.0 * _x_x_23)) == -19.0) || (((x_10 + (-1.0 * _x_x_23)) == -3.0) || (((x_9 + (-1.0 * _x_x_23)) == -10.0) || (((x_6 + (-1.0 * _x_x_23)) == -14.0) || (((x_1 + (-1.0 * _x_x_23)) == -7.0) || ((x_3 + (-1.0 * _x_x_23)) == -19.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_24)) <= -17.0) && (((x_33 + (-1.0 * _x_x_24)) <= -9.0) && (((x_32 + (-1.0 * _x_x_24)) <= -4.0) && (((x_27 + (-1.0 * _x_x_24)) <= -20.0) && (((x_26 + (-1.0 * _x_x_24)) <= -20.0) && (((x_25 + (-1.0 * _x_x_24)) <= -14.0) && (((x_24 + (-1.0 * _x_x_24)) <= -18.0) && (((x_23 + (-1.0 * _x_x_24)) <= -12.0) && (((x_21 + (-1.0 * _x_x_24)) <= -3.0) && (((x_20 + (-1.0 * _x_x_24)) <= -15.0) && (((x_19 + (-1.0 * _x_x_24)) <= -19.0) && (((x_17 + (-1.0 * _x_x_24)) <= -16.0) && (((x_15 + (-1.0 * _x_x_24)) <= -15.0) && (((x_14 + (-1.0 * _x_x_24)) <= -4.0) && (((x_13 + (-1.0 * _x_x_24)) <= -3.0) && (((x_9 + (-1.0 * _x_x_24)) <= -1.0) && (((x_3 + (-1.0 * _x_x_24)) <= -11.0) && ((x_7 + (-1.0 * _x_x_24)) <= -17.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_24)) == -17.0) || (((x_33 + (-1.0 * _x_x_24)) == -9.0) || (((x_32 + (-1.0 * _x_x_24)) == -4.0) || (((x_27 + (-1.0 * _x_x_24)) == -20.0) || (((x_26 + (-1.0 * _x_x_24)) == -20.0) || (((x_25 + (-1.0 * _x_x_24)) == -14.0) || (((x_24 + (-1.0 * _x_x_24)) == -18.0) || (((x_23 + (-1.0 * _x_x_24)) == -12.0) || (((x_21 + (-1.0 * _x_x_24)) == -3.0) || (((x_20 + (-1.0 * _x_x_24)) == -15.0) || (((x_19 + (-1.0 * _x_x_24)) == -19.0) || (((x_17 + (-1.0 * _x_x_24)) == -16.0) || (((x_15 + (-1.0 * _x_x_24)) == -15.0) || (((x_14 + (-1.0 * _x_x_24)) == -4.0) || (((x_13 + (-1.0 * _x_x_24)) == -3.0) || (((x_9 + (-1.0 * _x_x_24)) == -1.0) || (((x_3 + (-1.0 * _x_x_24)) == -11.0) || ((x_7 + (-1.0 * _x_x_24)) == -17.0)))))))))))))))))))) && ((((x_33 + (-1.0 * _x_x_25)) <= -18.0) && (((x_32 + (-1.0 * _x_x_25)) <= -13.0) && (((x_30 + (-1.0 * _x_x_25)) <= -6.0) && (((x_29 + (-1.0 * _x_x_25)) <= -9.0) && (((x_26 + (-1.0 * _x_x_25)) <= -5.0) && (((x_24 + (-1.0 * _x_x_25)) <= -4.0) && (((x_20 + (-1.0 * _x_x_25)) <= -13.0) && (((x_19 + (-1.0 * _x_x_25)) <= -14.0) && (((x_18 + (-1.0 * _x_x_25)) <= -15.0) && (((x_17 + (-1.0 * _x_x_25)) <= -9.0) && (((x_15 + (-1.0 * _x_x_25)) <= -8.0) && (((x_14 + (-1.0 * _x_x_25)) <= -9.0) && (((x_12 + (-1.0 * _x_x_25)) <= -10.0) && (((x_11 + (-1.0 * _x_x_25)) <= -15.0) && (((x_10 + (-1.0 * _x_x_25)) <= -8.0) && (((x_2 + (-1.0 * _x_x_25)) <= -17.0) && (((x_0 + (-1.0 * _x_x_25)) <= -15.0) && ((x_1 + (-1.0 * _x_x_25)) <= -11.0)))))))))))))))))) && (((x_33 + (-1.0 * _x_x_25)) == -18.0) || (((x_32 + (-1.0 * _x_x_25)) == -13.0) || (((x_30 + (-1.0 * _x_x_25)) == -6.0) || (((x_29 + (-1.0 * _x_x_25)) == -9.0) || (((x_26 + (-1.0 * _x_x_25)) == -5.0) || (((x_24 + (-1.0 * _x_x_25)) == -4.0) || (((x_20 + (-1.0 * _x_x_25)) == -13.0) || (((x_19 + (-1.0 * _x_x_25)) == -14.0) || (((x_18 + (-1.0 * _x_x_25)) == -15.0) || (((x_17 + (-1.0 * _x_x_25)) == -9.0) || (((x_15 + (-1.0 * _x_x_25)) == -8.0) || (((x_14 + (-1.0 * _x_x_25)) == -9.0) || (((x_12 + (-1.0 * _x_x_25)) == -10.0) || (((x_11 + (-1.0 * _x_x_25)) == -15.0) || (((x_10 + (-1.0 * _x_x_25)) == -8.0) || (((x_2 + (-1.0 * _x_x_25)) == -17.0) || (((x_0 + (-1.0 * _x_x_25)) == -15.0) || ((x_1 + (-1.0 * _x_x_25)) == -11.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_26)) <= -6.0) && (((x_34 + (-1.0 * _x_x_26)) <= -10.0) && (((x_32 + (-1.0 * _x_x_26)) <= -14.0) && (((x_31 + (-1.0 * _x_x_26)) <= -13.0) && (((x_30 + (-1.0 * _x_x_26)) <= -18.0) && (((x_29 + (-1.0 * _x_x_26)) <= -6.0) && (((x_27 + (-1.0 * _x_x_26)) <= -16.0) && (((x_25 + (-1.0 * _x_x_26)) <= -19.0) && (((x_23 + (-1.0 * _x_x_26)) <= -15.0) && (((x_19 + (-1.0 * _x_x_26)) <= -13.0) && (((x_18 + (-1.0 * _x_x_26)) <= -11.0) && (((x_13 + (-1.0 * _x_x_26)) <= -5.0) && (((x_10 + (-1.0 * _x_x_26)) <= -2.0) && (((x_9 + (-1.0 * _x_x_26)) <= -6.0) && (((x_8 + (-1.0 * _x_x_26)) <= -10.0) && (((x_6 + (-1.0 * _x_x_26)) <= -17.0) && (((x_1 + (-1.0 * _x_x_26)) <= -1.0) && ((x_3 + (-1.0 * _x_x_26)) <= -4.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_26)) == -6.0) || (((x_34 + (-1.0 * _x_x_26)) == -10.0) || (((x_32 + (-1.0 * _x_x_26)) == -14.0) || (((x_31 + (-1.0 * _x_x_26)) == -13.0) || (((x_30 + (-1.0 * _x_x_26)) == -18.0) || (((x_29 + (-1.0 * _x_x_26)) == -6.0) || (((x_27 + (-1.0 * _x_x_26)) == -16.0) || (((x_25 + (-1.0 * _x_x_26)) == -19.0) || (((x_23 + (-1.0 * _x_x_26)) == -15.0) || (((x_19 + (-1.0 * _x_x_26)) == -13.0) || (((x_18 + (-1.0 * _x_x_26)) == -11.0) || (((x_13 + (-1.0 * _x_x_26)) == -5.0) || (((x_10 + (-1.0 * _x_x_26)) == -2.0) || (((x_9 + (-1.0 * _x_x_26)) == -6.0) || (((x_8 + (-1.0 * _x_x_26)) == -10.0) || (((x_6 + (-1.0 * _x_x_26)) == -17.0) || (((x_1 + (-1.0 * _x_x_26)) == -1.0) || ((x_3 + (-1.0 * _x_x_26)) == -4.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_27)) <= -11.0) && (((x_34 + (-1.0 * _x_x_27)) <= -13.0) && (((x_33 + (-1.0 * _x_x_27)) <= -8.0) && (((x_32 + (-1.0 * _x_x_27)) <= -20.0) && (((x_23 + (-1.0 * _x_x_27)) <= -15.0) && (((x_21 + (-1.0 * _x_x_27)) <= -10.0) && (((x_19 + (-1.0 * _x_x_27)) <= -12.0) && (((x_18 + (-1.0 * _x_x_27)) <= -13.0) && (((x_16 + (-1.0 * _x_x_27)) <= -14.0) && (((x_15 + (-1.0 * _x_x_27)) <= -17.0) && (((x_12 + (-1.0 * _x_x_27)) <= -15.0) && (((x_10 + (-1.0 * _x_x_27)) <= -8.0) && (((x_8 + (-1.0 * _x_x_27)) <= -9.0) && (((x_7 + (-1.0 * _x_x_27)) <= -18.0) && (((x_4 + (-1.0 * _x_x_27)) <= -7.0) && (((x_3 + (-1.0 * _x_x_27)) <= -11.0) && (((x_0 + (-1.0 * _x_x_27)) <= -3.0) && ((x_1 + (-1.0 * _x_x_27)) <= -15.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_27)) == -11.0) || (((x_34 + (-1.0 * _x_x_27)) == -13.0) || (((x_33 + (-1.0 * _x_x_27)) == -8.0) || (((x_32 + (-1.0 * _x_x_27)) == -20.0) || (((x_23 + (-1.0 * _x_x_27)) == -15.0) || (((x_21 + (-1.0 * _x_x_27)) == -10.0) || (((x_19 + (-1.0 * _x_x_27)) == -12.0) || (((x_18 + (-1.0 * _x_x_27)) == -13.0) || (((x_16 + (-1.0 * _x_x_27)) == -14.0) || (((x_15 + (-1.0 * _x_x_27)) == -17.0) || (((x_12 + (-1.0 * _x_x_27)) == -15.0) || (((x_10 + (-1.0 * _x_x_27)) == -8.0) || (((x_8 + (-1.0 * _x_x_27)) == -9.0) || (((x_7 + (-1.0 * _x_x_27)) == -18.0) || (((x_4 + (-1.0 * _x_x_27)) == -7.0) || (((x_3 + (-1.0 * _x_x_27)) == -11.0) || (((x_0 + (-1.0 * _x_x_27)) == -3.0) || ((x_1 + (-1.0 * _x_x_27)) == -15.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_28)) <= -16.0) && (((x_33 + (-1.0 * _x_x_28)) <= -7.0) && (((x_29 + (-1.0 * _x_x_28)) <= -10.0) && (((x_28 + (-1.0 * _x_x_28)) <= -7.0) && (((x_24 + (-1.0 * _x_x_28)) <= -17.0) && (((x_22 + (-1.0 * _x_x_28)) <= -6.0) && (((x_21 + (-1.0 * _x_x_28)) <= -1.0) && (((x_19 + (-1.0 * _x_x_28)) <= -18.0) && (((x_15 + (-1.0 * _x_x_28)) <= -4.0) && (((x_12 + (-1.0 * _x_x_28)) <= -12.0) && (((x_10 + (-1.0 * _x_x_28)) <= -7.0) && (((x_9 + (-1.0 * _x_x_28)) <= -18.0) && (((x_8 + (-1.0 * _x_x_28)) <= -13.0) && (((x_7 + (-1.0 * _x_x_28)) <= -4.0) && (((x_6 + (-1.0 * _x_x_28)) <= -16.0) && (((x_4 + (-1.0 * _x_x_28)) <= -14.0) && (((x_1 + (-1.0 * _x_x_28)) <= -19.0) && ((x_3 + (-1.0 * _x_x_28)) <= -2.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_28)) == -16.0) || (((x_33 + (-1.0 * _x_x_28)) == -7.0) || (((x_29 + (-1.0 * _x_x_28)) == -10.0) || (((x_28 + (-1.0 * _x_x_28)) == -7.0) || (((x_24 + (-1.0 * _x_x_28)) == -17.0) || (((x_22 + (-1.0 * _x_x_28)) == -6.0) || (((x_21 + (-1.0 * _x_x_28)) == -1.0) || (((x_19 + (-1.0 * _x_x_28)) == -18.0) || (((x_15 + (-1.0 * _x_x_28)) == -4.0) || (((x_12 + (-1.0 * _x_x_28)) == -12.0) || (((x_10 + (-1.0 * _x_x_28)) == -7.0) || (((x_9 + (-1.0 * _x_x_28)) == -18.0) || (((x_8 + (-1.0 * _x_x_28)) == -13.0) || (((x_7 + (-1.0 * _x_x_28)) == -4.0) || (((x_6 + (-1.0 * _x_x_28)) == -16.0) || (((x_4 + (-1.0 * _x_x_28)) == -14.0) || (((x_1 + (-1.0 * _x_x_28)) == -19.0) || ((x_3 + (-1.0 * _x_x_28)) == -2.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_29)) <= -4.0) && (((x_34 + (-1.0 * _x_x_29)) <= -10.0) && (((x_30 + (-1.0 * _x_x_29)) <= -5.0) && (((x_29 + (-1.0 * _x_x_29)) <= -15.0) && (((x_27 + (-1.0 * _x_x_29)) <= -17.0) && (((x_25 + (-1.0 * _x_x_29)) <= -9.0) && (((x_23 + (-1.0 * _x_x_29)) <= -10.0) && (((x_21 + (-1.0 * _x_x_29)) <= -11.0) && (((x_19 + (-1.0 * _x_x_29)) <= -6.0) && (((x_18 + (-1.0 * _x_x_29)) <= -12.0) && (((x_17 + (-1.0 * _x_x_29)) <= -17.0) && (((x_16 + (-1.0 * _x_x_29)) <= -7.0) && (((x_14 + (-1.0 * _x_x_29)) <= -11.0) && (((x_12 + (-1.0 * _x_x_29)) <= -19.0) && (((x_8 + (-1.0 * _x_x_29)) <= -2.0) && (((x_7 + (-1.0 * _x_x_29)) <= -12.0) && (((x_4 + (-1.0 * _x_x_29)) <= -10.0) && ((x_5 + (-1.0 * _x_x_29)) <= -12.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_29)) == -4.0) || (((x_34 + (-1.0 * _x_x_29)) == -10.0) || (((x_30 + (-1.0 * _x_x_29)) == -5.0) || (((x_29 + (-1.0 * _x_x_29)) == -15.0) || (((x_27 + (-1.0 * _x_x_29)) == -17.0) || (((x_25 + (-1.0 * _x_x_29)) == -9.0) || (((x_23 + (-1.0 * _x_x_29)) == -10.0) || (((x_21 + (-1.0 * _x_x_29)) == -11.0) || (((x_19 + (-1.0 * _x_x_29)) == -6.0) || (((x_18 + (-1.0 * _x_x_29)) == -12.0) || (((x_17 + (-1.0 * _x_x_29)) == -17.0) || (((x_16 + (-1.0 * _x_x_29)) == -7.0) || (((x_14 + (-1.0 * _x_x_29)) == -11.0) || (((x_12 + (-1.0 * _x_x_29)) == -19.0) || (((x_8 + (-1.0 * _x_x_29)) == -2.0) || (((x_7 + (-1.0 * _x_x_29)) == -12.0) || (((x_4 + (-1.0 * _x_x_29)) == -10.0) || ((x_5 + (-1.0 * _x_x_29)) == -12.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_30)) <= -16.0) && (((x_32 + (-1.0 * _x_x_30)) <= -3.0) && (((x_29 + (-1.0 * _x_x_30)) <= -5.0) && (((x_28 + (-1.0 * _x_x_30)) <= -3.0) && (((x_24 + (-1.0 * _x_x_30)) <= -3.0) && (((x_23 + (-1.0 * _x_x_30)) <= -3.0) && (((x_21 + (-1.0 * _x_x_30)) <= -2.0) && (((x_20 + (-1.0 * _x_x_30)) <= -19.0) && (((x_18 + (-1.0 * _x_x_30)) <= -7.0) && (((x_16 + (-1.0 * _x_x_30)) <= -19.0) && (((x_12 + (-1.0 * _x_x_30)) <= -16.0) && (((x_11 + (-1.0 * _x_x_30)) <= -16.0) && (((x_10 + (-1.0 * _x_x_30)) <= -12.0) && (((x_9 + (-1.0 * _x_x_30)) <= -19.0) && (((x_3 + (-1.0 * _x_x_30)) <= -19.0) && (((x_2 + (-1.0 * _x_x_30)) <= -17.0) && (((x_0 + (-1.0 * _x_x_30)) <= -6.0) && ((x_1 + (-1.0 * _x_x_30)) <= -5.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_30)) == -16.0) || (((x_32 + (-1.0 * _x_x_30)) == -3.0) || (((x_29 + (-1.0 * _x_x_30)) == -5.0) || (((x_28 + (-1.0 * _x_x_30)) == -3.0) || (((x_24 + (-1.0 * _x_x_30)) == -3.0) || (((x_23 + (-1.0 * _x_x_30)) == -3.0) || (((x_21 + (-1.0 * _x_x_30)) == -2.0) || (((x_20 + (-1.0 * _x_x_30)) == -19.0) || (((x_18 + (-1.0 * _x_x_30)) == -7.0) || (((x_16 + (-1.0 * _x_x_30)) == -19.0) || (((x_12 + (-1.0 * _x_x_30)) == -16.0) || (((x_11 + (-1.0 * _x_x_30)) == -16.0) || (((x_10 + (-1.0 * _x_x_30)) == -12.0) || (((x_9 + (-1.0 * _x_x_30)) == -19.0) || (((x_3 + (-1.0 * _x_x_30)) == -19.0) || (((x_2 + (-1.0 * _x_x_30)) == -17.0) || (((x_0 + (-1.0 * _x_x_30)) == -6.0) || ((x_1 + (-1.0 * _x_x_30)) == -5.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_31)) <= -17.0) && (((x_32 + (-1.0 * _x_x_31)) <= -19.0) && (((x_31 + (-1.0 * _x_x_31)) <= -15.0) && (((x_29 + (-1.0 * _x_x_31)) <= -7.0) && (((x_27 + (-1.0 * _x_x_31)) <= -20.0) && (((x_26 + (-1.0 * _x_x_31)) <= -18.0) && (((x_23 + (-1.0 * _x_x_31)) <= -10.0) && (((x_22 + (-1.0 * _x_x_31)) <= -16.0) && (((x_20 + (-1.0 * _x_x_31)) <= -1.0) && (((x_17 + (-1.0 * _x_x_31)) <= -8.0) && (((x_16 + (-1.0 * _x_x_31)) <= -1.0) && (((x_14 + (-1.0 * _x_x_31)) <= -20.0) && (((x_9 + (-1.0 * _x_x_31)) <= -17.0) && (((x_8 + (-1.0 * _x_x_31)) <= -8.0) && (((x_7 + (-1.0 * _x_x_31)) <= -15.0) && (((x_5 + (-1.0 * _x_x_31)) <= -3.0) && (((x_3 + (-1.0 * _x_x_31)) <= -5.0) && ((x_4 + (-1.0 * _x_x_31)) <= -17.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_31)) == -17.0) || (((x_32 + (-1.0 * _x_x_31)) == -19.0) || (((x_31 + (-1.0 * _x_x_31)) == -15.0) || (((x_29 + (-1.0 * _x_x_31)) == -7.0) || (((x_27 + (-1.0 * _x_x_31)) == -20.0) || (((x_26 + (-1.0 * _x_x_31)) == -18.0) || (((x_23 + (-1.0 * _x_x_31)) == -10.0) || (((x_22 + (-1.0 * _x_x_31)) == -16.0) || (((x_20 + (-1.0 * _x_x_31)) == -1.0) || (((x_17 + (-1.0 * _x_x_31)) == -8.0) || (((x_16 + (-1.0 * _x_x_31)) == -1.0) || (((x_14 + (-1.0 * _x_x_31)) == -20.0) || (((x_9 + (-1.0 * _x_x_31)) == -17.0) || (((x_8 + (-1.0 * _x_x_31)) == -8.0) || (((x_7 + (-1.0 * _x_x_31)) == -15.0) || (((x_5 + (-1.0 * _x_x_31)) == -3.0) || (((x_3 + (-1.0 * _x_x_31)) == -5.0) || ((x_4 + (-1.0 * _x_x_31)) == -17.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_32)) <= -19.0) && (((x_33 + (-1.0 * _x_x_32)) <= -1.0) && (((x_30 + (-1.0 * _x_x_32)) <= -6.0) && (((x_28 + (-1.0 * _x_x_32)) <= -12.0) && (((x_27 + (-1.0 * _x_x_32)) <= -5.0) && (((x_24 + (-1.0 * _x_x_32)) <= -19.0) && (((x_23 + (-1.0 * _x_x_32)) <= -4.0) && (((x_22 + (-1.0 * _x_x_32)) <= -9.0) && (((x_21 + (-1.0 * _x_x_32)) <= -15.0) && (((x_20 + (-1.0 * _x_x_32)) <= -15.0) && (((x_14 + (-1.0 * _x_x_32)) <= -11.0) && (((x_12 + (-1.0 * _x_x_32)) <= -6.0) && (((x_11 + (-1.0 * _x_x_32)) <= -1.0) && (((x_8 + (-1.0 * _x_x_32)) <= -3.0) && (((x_6 + (-1.0 * _x_x_32)) <= -16.0) && (((x_4 + (-1.0 * _x_x_32)) <= -17.0) && (((x_2 + (-1.0 * _x_x_32)) <= -19.0) && ((x_3 + (-1.0 * _x_x_32)) <= -18.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_32)) == -19.0) || (((x_33 + (-1.0 * _x_x_32)) == -1.0) || (((x_30 + (-1.0 * _x_x_32)) == -6.0) || (((x_28 + (-1.0 * _x_x_32)) == -12.0) || (((x_27 + (-1.0 * _x_x_32)) == -5.0) || (((x_24 + (-1.0 * _x_x_32)) == -19.0) || (((x_23 + (-1.0 * _x_x_32)) == -4.0) || (((x_22 + (-1.0 * _x_x_32)) == -9.0) || (((x_21 + (-1.0 * _x_x_32)) == -15.0) || (((x_20 + (-1.0 * _x_x_32)) == -15.0) || (((x_14 + (-1.0 * _x_x_32)) == -11.0) || (((x_12 + (-1.0 * _x_x_32)) == -6.0) || (((x_11 + (-1.0 * _x_x_32)) == -1.0) || (((x_8 + (-1.0 * _x_x_32)) == -3.0) || (((x_6 + (-1.0 * _x_x_32)) == -16.0) || (((x_4 + (-1.0 * _x_x_32)) == -17.0) || (((x_2 + (-1.0 * _x_x_32)) == -19.0) || ((x_3 + (-1.0 * _x_x_32)) == -18.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_33)) <= -3.0) && (((x_31 + (-1.0 * _x_x_33)) <= -14.0) && (((x_30 + (-1.0 * _x_x_33)) <= -16.0) && (((x_26 + (-1.0 * _x_x_33)) <= -4.0) && (((x_25 + (-1.0 * _x_x_33)) <= -4.0) && (((x_23 + (-1.0 * _x_x_33)) <= -13.0) && (((x_21 + (-1.0 * _x_x_33)) <= -5.0) && (((x_19 + (-1.0 * _x_x_33)) <= -12.0) && (((x_17 + (-1.0 * _x_x_33)) <= -10.0) && (((x_16 + (-1.0 * _x_x_33)) <= -3.0) && (((x_15 + (-1.0 * _x_x_33)) <= -14.0) && (((x_13 + (-1.0 * _x_x_33)) <= -18.0) && (((x_12 + (-1.0 * _x_x_33)) <= -10.0) && (((x_8 + (-1.0 * _x_x_33)) <= -1.0) && (((x_7 + (-1.0 * _x_x_33)) <= -20.0) && (((x_4 + (-1.0 * _x_x_33)) <= -6.0) && (((x_0 + (-1.0 * _x_x_33)) <= -10.0) && ((x_1 + (-1.0 * _x_x_33)) <= -15.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_33)) == -3.0) || (((x_31 + (-1.0 * _x_x_33)) == -14.0) || (((x_30 + (-1.0 * _x_x_33)) == -16.0) || (((x_26 + (-1.0 * _x_x_33)) == -4.0) || (((x_25 + (-1.0 * _x_x_33)) == -4.0) || (((x_23 + (-1.0 * _x_x_33)) == -13.0) || (((x_21 + (-1.0 * _x_x_33)) == -5.0) || (((x_19 + (-1.0 * _x_x_33)) == -12.0) || (((x_17 + (-1.0 * _x_x_33)) == -10.0) || (((x_16 + (-1.0 * _x_x_33)) == -3.0) || (((x_15 + (-1.0 * _x_x_33)) == -14.0) || (((x_13 + (-1.0 * _x_x_33)) == -18.0) || (((x_12 + (-1.0 * _x_x_33)) == -10.0) || (((x_8 + (-1.0 * _x_x_33)) == -1.0) || (((x_7 + (-1.0 * _x_x_33)) == -20.0) || (((x_4 + (-1.0 * _x_x_33)) == -6.0) || (((x_0 + (-1.0 * _x_x_33)) == -10.0) || ((x_1 + (-1.0 * _x_x_33)) == -15.0)))))))))))))))))))) && ((((x_34 + (-1.0 * _x_x_34)) <= -15.0) && (((x_30 + (-1.0 * _x_x_34)) <= -12.0) && (((x_27 + (-1.0 * _x_x_34)) <= -2.0) && (((x_24 + (-1.0 * _x_x_34)) <= -12.0) && (((x_23 + (-1.0 * _x_x_34)) <= -3.0) && (((x_22 + (-1.0 * _x_x_34)) <= -5.0) && (((x_20 + (-1.0 * _x_x_34)) <= -16.0) && (((x_19 + (-1.0 * _x_x_34)) <= -15.0) && (((x_16 + (-1.0 * _x_x_34)) <= -4.0) && (((x_13 + (-1.0 * _x_x_34)) <= -2.0) && (((x_12 + (-1.0 * _x_x_34)) <= -20.0) && (((x_11 + (-1.0 * _x_x_34)) <= -4.0) && (((x_10 + (-1.0 * _x_x_34)) <= -17.0) && (((x_9 + (-1.0 * _x_x_34)) <= -4.0) && (((x_8 + (-1.0 * _x_x_34)) <= -11.0) && (((x_7 + (-1.0 * _x_x_34)) <= -16.0) && (((x_1 + (-1.0 * _x_x_34)) <= -19.0) && ((x_4 + (-1.0 * _x_x_34)) <= -12.0)))))))))))))))))) && (((x_34 + (-1.0 * _x_x_34)) == -15.0) || (((x_30 + (-1.0 * _x_x_34)) == -12.0) || (((x_27 + (-1.0 * _x_x_34)) == -2.0) || (((x_24 + (-1.0 * _x_x_34)) == -12.0) || (((x_23 + (-1.0 * _x_x_34)) == -3.0) || (((x_22 + (-1.0 * _x_x_34)) == -5.0) || (((x_20 + (-1.0 * _x_x_34)) == -16.0) || (((x_19 + (-1.0 * _x_x_34)) == -15.0) || (((x_16 + (-1.0 * _x_x_34)) == -4.0) || (((x_13 + (-1.0 * _x_x_34)) == -2.0) || (((x_12 + (-1.0 * _x_x_34)) == -20.0) || (((x_11 + (-1.0 * _x_x_34)) == -4.0) || (((x_10 + (-1.0 * _x_x_34)) == -17.0) || (((x_9 + (-1.0 * _x_x_34)) == -4.0) || (((x_8 + (-1.0 * _x_x_34)) == -11.0) || (((x_7 + (-1.0 * _x_x_34)) == -16.0) || (((x_1 + (-1.0 * _x_x_34)) == -19.0) || ((x_4 + (-1.0 * _x_x_34)) == -12.0)))))))))))))))))))) && ((((x_35 + (-1.0 * _x_x_35)) <= -2.0) && (((x_28 + (-1.0 * _x_x_35)) <= -19.0) && (((x_27 + (-1.0 * _x_x_35)) <= -4.0) && (((x_26 + (-1.0 * _x_x_35)) <= -3.0) && (((x_25 + (-1.0 * _x_x_35)) <= -6.0) && (((x_24 + (-1.0 * _x_x_35)) <= -20.0) && (((x_21 + (-1.0 * _x_x_35)) <= -10.0) && (((x_20 + (-1.0 * _x_x_35)) <= -8.0) && (((x_19 + (-1.0 * _x_x_35)) <= -10.0) && (((x_14 + (-1.0 * _x_x_35)) <= -5.0) && (((x_13 + (-1.0 * _x_x_35)) <= -13.0) && (((x_9 + (-1.0 * _x_x_35)) <= -8.0) && (((x_8 + (-1.0 * _x_x_35)) <= -14.0) && (((x_6 + (-1.0 * _x_x_35)) <= -15.0) && (((x_5 + (-1.0 * _x_x_35)) <= -8.0) && (((x_4 + (-1.0 * _x_x_35)) <= -3.0) && (((x_2 + (-1.0 * _x_x_35)) <= -20.0) && ((x_3 + (-1.0 * _x_x_35)) <= -19.0)))))))))))))))))) && (((x_35 + (-1.0 * _x_x_35)) == -2.0) || (((x_28 + (-1.0 * _x_x_35)) == -19.0) || (((x_27 + (-1.0 * _x_x_35)) == -4.0) || (((x_26 + (-1.0 * _x_x_35)) == -3.0) || (((x_25 + (-1.0 * _x_x_35)) == -6.0) || (((x_24 + (-1.0 * _x_x_35)) == -20.0) || (((x_21 + (-1.0 * _x_x_35)) == -10.0) || (((x_20 + (-1.0 * _x_x_35)) == -8.0) || (((x_19 + (-1.0 * _x_x_35)) == -10.0) || (((x_14 + (-1.0 * _x_x_35)) == -5.0) || (((x_13 + (-1.0 * _x_x_35)) == -13.0) || (((x_9 + (-1.0 * _x_x_35)) == -8.0) || (((x_8 + (-1.0 * _x_x_35)) == -14.0) || (((x_6 + (-1.0 * _x_x_35)) == -15.0) || (((x_5 + (-1.0 * _x_x_35)) == -8.0) || (((x_4 + (-1.0 * _x_x_35)) == -3.0) || (((x_2 + (-1.0 * _x_x_35)) == -20.0) || ((x_3 + (-1.0 * _x_x_35)) == -19.0)))))))))))))))))))) && ((_EL_U_3833 == (_x__EL_U_3833 || ((_x_x_11 + (-1.0 * _x_x_16)) <= 17.0))) && (_EL_X_3825 == (-18.0 <= (_x_x_10 + (-1.0 * _x_x_26))))));
    _EL_U_3833 = _x__EL_U_3833;
    x_16 = _x_x_16;
    x_0 = _x_x_0;
    x_11 = _x_x_11;
    _EL_X_3825 = _x__EL_X_3825;
    x_3 = _x_x_3;
    x_33 = _x_x_33;
    x_2 = _x_x_2;
    x_15 = _x_x_15;
    x_1 = _x_x_1;
    x_4 = _x_x_4;
    x_17 = _x_x_17;
    x_7 = _x_x_7;
    x_5 = _x_x_5;
    x_6 = _x_x_6;
    x_10 = _x_x_10;
    x_8 = _x_x_8;
    x_9 = _x_x_9;
    x_31 = _x_x_31;
    x_12 = _x_x_12;
    x_13 = _x_x_13;
    x_18 = _x_x_18;
    x_14 = _x_x_14;
    x_19 = _x_x_19;
    x_22 = _x_x_22;
    x_23 = _x_x_23;
    x_20 = _x_x_20;
    x_21 = _x_x_21;
    x_24 = _x_x_24;
    x_30 = _x_x_30;
    x_25 = _x_x_25;
    x_34 = _x_x_34;
    x_26 = _x_x_26;
    x_27 = _x_x_27;
    x_28 = _x_x_28;
    x_29 = _x_x_29;
    x_35 = _x_x_35;
    x_32 = _x_x_32;

  }
}
