text: 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 _J1308, _x__J1308;
  bool _J1299, _x__J1299;
  bool _EL_U_1281, _x__EL_U_1281;
  float x_12, _x_x_12;
  float x_15, _x_x_15;
  float x_3, _x_x_3;
  bool _EL_U_1279, _x__EL_U_1279;
  float x_16, _x_x_16;
  float x_10, _x_x_10;
  float x_18, _x_x_18;
  float x_13, _x_x_13;
  float x_0, _x_x_0;
  float x_1, _x_x_1;
  float x_2, _x_x_2;
  float x_4, _x_x_4;
  float x_5, _x_x_5;
  float x_6, _x_x_6;
  float x_7, _x_x_7;
  float x_14, _x_x_14;
  float x_17, _x_x_17;
  float x_19, _x_x_19;
  float x_9, _x_x_9;
  float x_8, _x_x_8;
  float x_11, _x_x_11;
  
    int __steps_to_fair = __VERIFIER_nondet_int();
    _J1308 = __VERIFIER_nondet_bool();
    _J1299 = __VERIFIER_nondet_bool();
    _EL_U_1281 = __VERIFIER_nondet_bool();
    x_12 = __VERIFIER_nondet_float();
    x_15 = __VERIFIER_nondet_float();
    x_3 = __VERIFIER_nondet_float();
    _EL_U_1279 = __VERIFIER_nondet_bool();
    x_16 = __VERIFIER_nondet_float();
    x_10 = __VERIFIER_nondet_float();
    x_18 = __VERIFIER_nondet_float();
    x_13 = __VERIFIER_nondet_float();
    x_0 = __VERIFIER_nondet_float();
    x_1 = __VERIFIER_nondet_float();
    x_2 = __VERIFIER_nondet_float();
    x_4 = __VERIFIER_nondet_float();
    x_5 = __VERIFIER_nondet_float();
    x_6 = __VERIFIER_nondet_float();
    x_7 = __VERIFIER_nondet_float();
    x_14 = __VERIFIER_nondet_float();
    x_17 = __VERIFIER_nondet_float();
    x_19 = __VERIFIER_nondet_float();
    x_9 = __VERIFIER_nondet_float();
    x_8 = __VERIFIER_nondet_float();
    x_11 = __VERIFIER_nondet_float();
  
    bool __ok = (1 && (((((12.0 <= (x_0 + (-1.0 * x_13))) || (((x_10 + (-1.0 * x_16)) <= -2.0) && _EL_U_1279)) || (((x_3 + (-1.0 * x_12)) <= 19.0) && _EL_U_1281)) && ( !_J1299)) && ( !_J1308)));
    while (__steps_to_fair >= 0 && __ok) {
      if ((_J1299 && _J1308)) {
        __steps_to_fair = __VERIFIER_nondet_int();
      } else {
        __steps_to_fair--;
      }
      _x__J1308 = __VERIFIER_nondet_bool();
      _x__J1299 = __VERIFIER_nondet_bool();
      _x__EL_U_1281 = __VERIFIER_nondet_bool();
      _x_x_12 = __VERIFIER_nondet_float();
      _x_x_15 = __VERIFIER_nondet_float();
      _x_x_3 = __VERIFIER_nondet_float();
      _x__EL_U_1279 = __VERIFIER_nondet_bool();
      _x_x_16 = __VERIFIER_nondet_float();
      _x_x_10 = __VERIFIER_nondet_float();
      _x_x_18 = __VERIFIER_nondet_float();
      _x_x_13 = __VERIFIER_nondet_float();
      _x_x_0 = __VERIFIER_nondet_float();
      _x_x_1 = __VERIFIER_nondet_float();
      _x_x_2 = __VERIFIER_nondet_float();
      _x_x_4 = __VERIFIER_nondet_float();
      _x_x_5 = __VERIFIER_nondet_float();
      _x_x_6 = __VERIFIER_nondet_float();
      _x_x_7 = __VERIFIER_nondet_float();
      _x_x_14 = __VERIFIER_nondet_float();
      _x_x_17 = __VERIFIER_nondet_float();
      _x_x_19 = __VERIFIER_nondet_float();
      _x_x_9 = __VERIFIER_nondet_float();
      _x_x_8 = __VERIFIER_nondet_float();
      _x_x_11 = __VERIFIER_nondet_float();
  
      __ok = ((((((((((((((((((((((((x_19 + (-1.0 * _x_x_0)) <= -1.0) && (((x_18 + (-1.0 * _x_x_0)) <= -14.0) && (((x_17 + (-1.0 * _x_x_0)) <= -3.0) && (((x_16 + (-1.0 * _x_x_0)) <= -19.0) && (((x_15 + (-1.0 * _x_x_0)) <= -16.0) && (((x_13 + (-1.0 * _x_x_0)) <= -10.0) && (((x_12 + (-1.0 * _x_x_0)) <= -11.0) && (((x_9 + (-1.0 * _x_x_0)) <= -8.0) && (((x_1 + (-1.0 * _x_x_0)) <= -6.0) && ((x_3 + (-1.0 * _x_x_0)) <= -9.0)))))))))) && (((x_19 + (-1.0 * _x_x_0)) == -1.0) || (((x_18 + (-1.0 * _x_x_0)) == -14.0) || (((x_17 + (-1.0 * _x_x_0)) == -3.0) || (((x_16 + (-1.0 * _x_x_0)) == -19.0) || (((x_15 + (-1.0 * _x_x_0)) == -16.0) || (((x_13 + (-1.0 * _x_x_0)) == -10.0) || (((x_12 + (-1.0 * _x_x_0)) == -11.0) || (((x_9 + (-1.0 * _x_x_0)) == -8.0) || (((x_1 + (-1.0 * _x_x_0)) == -6.0) || ((x_3 + (-1.0 * _x_x_0)) == -9.0))))))))))) && ((((x_19 + (-1.0 * _x_x_1)) <= -15.0) && (((x_15 + (-1.0 * _x_x_1)) <= -8.0) && (((x_14 + (-1.0 * _x_x_1)) <= -16.0) && (((x_12 + (-1.0 * _x_x_1)) <= -14.0) && (((x_9 + (-1.0 * _x_x_1)) <= -15.0) && (((x_7 + (-1.0 * _x_x_1)) <= -13.0) && (((x_5 + (-1.0 * _x_x_1)) <= -15.0) && (((x_4 + (-1.0 * _x_x_1)) <= -17.0) && (((x_0 + (-1.0 * _x_x_1)) <= -7.0) && ((x_3 + (-1.0 * _x_x_1)) <= -14.0)))))))))) && (((x_19 + (-1.0 * _x_x_1)) == -15.0) || (((x_15 + (-1.0 * _x_x_1)) == -8.0) || (((x_14 + (-1.0 * _x_x_1)) == -16.0) || (((x_12 + (-1.0 * _x_x_1)) == -14.0) || (((x_9 + (-1.0 * _x_x_1)) == -15.0) || (((x_7 + (-1.0 * _x_x_1)) == -13.0) || (((x_5 + (-1.0 * _x_x_1)) == -15.0) || (((x_4 + (-1.0 * _x_x_1)) == -17.0) || (((x_0 + (-1.0 * _x_x_1)) == -7.0) || ((x_3 + (-1.0 * _x_x_1)) == -14.0)))))))))))) && ((((x_17 + (-1.0 * _x_x_2)) <= -7.0) && (((x_16 + (-1.0 * _x_x_2)) <= -16.0) && (((x_14 + (-1.0 * _x_x_2)) <= -16.0) && (((x_13 + (-1.0 * _x_x_2)) <= -9.0) && (((x_9 + (-1.0 * _x_x_2)) <= -17.0) && (((x_6 + (-1.0 * _x_x_2)) <= -15.0) && (((x_4 + (-1.0 * _x_x_2)) <= -19.0) && (((x_3 + (-1.0 * _x_x_2)) <= -20.0) && (((x_0 + (-1.0 * _x_x_2)) <= -6.0) && ((x_1 + (-1.0 * _x_x_2)) <= -18.0)))))))))) && (((x_17 + (-1.0 * _x_x_2)) == -7.0) || (((x_16 + (-1.0 * _x_x_2)) == -16.0) || (((x_14 + (-1.0 * _x_x_2)) == -16.0) || (((x_13 + (-1.0 * _x_x_2)) == -9.0) || (((x_9 + (-1.0 * _x_x_2)) == -17.0) || (((x_6 + (-1.0 * _x_x_2)) == -15.0) || (((x_4 + (-1.0 * _x_x_2)) == -19.0) || (((x_3 + (-1.0 * _x_x_2)) == -20.0) || (((x_0 + (-1.0 * _x_x_2)) == -6.0) || ((x_1 + (-1.0 * _x_x_2)) == -18.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_3)) <= -13.0) && (((x_14 + (-1.0 * _x_x_3)) <= -15.0) && (((x_13 + (-1.0 * _x_x_3)) <= -6.0) && (((x_9 + (-1.0 * _x_x_3)) <= -19.0) && (((x_8 + (-1.0 * _x_x_3)) <= -17.0) && (((x_7 + (-1.0 * _x_x_3)) <= -6.0) && (((x_6 + (-1.0 * _x_x_3)) <= -18.0) && (((x_5 + (-1.0 * _x_x_3)) <= -20.0) && (((x_0 + (-1.0 * _x_x_3)) <= -5.0) && ((x_2 + (-1.0 * _x_x_3)) <= -7.0)))))))))) && (((x_19 + (-1.0 * _x_x_3)) == -13.0) || (((x_14 + (-1.0 * _x_x_3)) == -15.0) || (((x_13 + (-1.0 * _x_x_3)) == -6.0) || (((x_9 + (-1.0 * _x_x_3)) == -19.0) || (((x_8 + (-1.0 * _x_x_3)) == -17.0) || (((x_7 + (-1.0 * _x_x_3)) == -6.0) || (((x_6 + (-1.0 * _x_x_3)) == -18.0) || (((x_5 + (-1.0 * _x_x_3)) == -20.0) || (((x_0 + (-1.0 * _x_x_3)) == -5.0) || ((x_2 + (-1.0 * _x_x_3)) == -7.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_4)) <= -11.0) && (((x_16 + (-1.0 * _x_x_4)) <= -6.0) && (((x_15 + (-1.0 * _x_x_4)) <= -10.0) && (((x_14 + (-1.0 * _x_x_4)) <= -18.0) && (((x_13 + (-1.0 * _x_x_4)) <= -10.0) && (((x_12 + (-1.0 * _x_x_4)) <= -9.0) && (((x_11 + (-1.0 * _x_x_4)) <= -6.0) && (((x_10 + (-1.0 * _x_x_4)) <= -3.0) && (((x_0 + (-1.0 * _x_x_4)) <= -16.0) && ((x_5 + (-1.0 * _x_x_4)) <= -5.0)))))))))) && (((x_19 + (-1.0 * _x_x_4)) == -11.0) || (((x_16 + (-1.0 * _x_x_4)) == -6.0) || (((x_15 + (-1.0 * _x_x_4)) == -10.0) || (((x_14 + (-1.0 * _x_x_4)) == -18.0) || (((x_13 + (-1.0 * _x_x_4)) == -10.0) || (((x_12 + (-1.0 * _x_x_4)) == -9.0) || (((x_11 + (-1.0 * _x_x_4)) == -6.0) || (((x_10 + (-1.0 * _x_x_4)) == -3.0) || (((x_0 + (-1.0 * _x_x_4)) == -16.0) || ((x_5 + (-1.0 * _x_x_4)) == -5.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_5)) <= -18.0) && (((x_18 + (-1.0 * _x_x_5)) <= -4.0) && (((x_16 + (-1.0 * _x_x_5)) <= -7.0) && (((x_15 + (-1.0 * _x_x_5)) <= -9.0) && (((x_14 + (-1.0 * _x_x_5)) <= -17.0) && (((x_12 + (-1.0 * _x_x_5)) <= -4.0) && (((x_10 + (-1.0 * _x_x_5)) <= -7.0) && (((x_9 + (-1.0 * _x_x_5)) <= -16.0) && (((x_0 + (-1.0 * _x_x_5)) <= -6.0) && ((x_2 + (-1.0 * _x_x_5)) <= -5.0)))))))))) && (((x_19 + (-1.0 * _x_x_5)) == -18.0) || (((x_18 + (-1.0 * _x_x_5)) == -4.0) || (((x_16 + (-1.0 * _x_x_5)) == -7.0) || (((x_15 + (-1.0 * _x_x_5)) == -9.0) || (((x_14 + (-1.0 * _x_x_5)) == -17.0) || (((x_12 + (-1.0 * _x_x_5)) == -4.0) || (((x_10 + (-1.0 * _x_x_5)) == -7.0) || (((x_9 + (-1.0 * _x_x_5)) == -16.0) || (((x_0 + (-1.0 * _x_x_5)) == -6.0) || ((x_2 + (-1.0 * _x_x_5)) == -5.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_6)) <= -17.0) && (((x_17 + (-1.0 * _x_x_6)) <= -4.0) && (((x_16 + (-1.0 * _x_x_6)) <= -8.0) && (((x_13 + (-1.0 * _x_x_6)) <= -3.0) && (((x_7 + (-1.0 * _x_x_6)) <= -4.0) && (((x_6 + (-1.0 * _x_x_6)) <= -4.0) && (((x_5 + (-1.0 * _x_x_6)) <= -8.0) && (((x_3 + (-1.0 * _x_x_6)) <= -20.0) && (((x_1 + (-1.0 * _x_x_6)) <= -2.0) && ((x_2 + (-1.0 * _x_x_6)) <= -19.0)))))))))) && (((x_19 + (-1.0 * _x_x_6)) == -17.0) || (((x_17 + (-1.0 * _x_x_6)) == -4.0) || (((x_16 + (-1.0 * _x_x_6)) == -8.0) || (((x_13 + (-1.0 * _x_x_6)) == -3.0) || (((x_7 + (-1.0 * _x_x_6)) == -4.0) || (((x_6 + (-1.0 * _x_x_6)) == -4.0) || (((x_5 + (-1.0 * _x_x_6)) == -8.0) || (((x_3 + (-1.0 * _x_x_6)) == -20.0) || (((x_1 + (-1.0 * _x_x_6)) == -2.0) || ((x_2 + (-1.0 * _x_x_6)) == -19.0)))))))))))) && ((((x_17 + (-1.0 * _x_x_7)) <= -16.0) && (((x_16 + (-1.0 * _x_x_7)) <= -17.0) && (((x_15 + (-1.0 * _x_x_7)) <= -16.0) && (((x_13 + (-1.0 * _x_x_7)) <= -6.0) && (((x_12 + (-1.0 * _x_x_7)) <= -5.0) && (((x_11 + (-1.0 * _x_x_7)) <= -6.0) && (((x_9 + (-1.0 * _x_x_7)) <= -4.0) && (((x_4 + (-1.0 * _x_x_7)) <= -7.0) && (((x_1 + (-1.0 * _x_x_7)) <= -12.0) && ((x_3 + (-1.0 * _x_x_7)) <= -3.0)))))))))) && (((x_17 + (-1.0 * _x_x_7)) == -16.0) || (((x_16 + (-1.0 * _x_x_7)) == -17.0) || (((x_15 + (-1.0 * _x_x_7)) == -16.0) || (((x_13 + (-1.0 * _x_x_7)) == -6.0) || (((x_12 + (-1.0 * _x_x_7)) == -5.0) || (((x_11 + (-1.0 * _x_x_7)) == -6.0) || (((x_9 + (-1.0 * _x_x_7)) == -4.0) || (((x_4 + (-1.0 * _x_x_7)) == -7.0) || (((x_1 + (-1.0 * _x_x_7)) == -12.0) || ((x_3 + (-1.0 * _x_x_7)) == -3.0)))))))))))) && ((((x_18 + (-1.0 * _x_x_8)) <= -2.0) && (((x_15 + (-1.0 * _x_x_8)) <= -12.0) && (((x_14 + (-1.0 * _x_x_8)) <= -16.0) && (((x_12 + (-1.0 * _x_x_8)) <= -8.0) && (((x_11 + (-1.0 * _x_x_8)) <= -2.0) && (((x_10 + (-1.0 * _x_x_8)) <= -11.0) && (((x_6 + (-1.0 * _x_x_8)) <= -13.0) && (((x_4 + (-1.0 * _x_x_8)) <= -10.0) && (((x_2 + (-1.0 * _x_x_8)) <= -3.0) && ((x_3 + (-1.0 * _x_x_8)) <= -15.0)))))))))) && (((x_18 + (-1.0 * _x_x_8)) == -2.0) || (((x_15 + (-1.0 * _x_x_8)) == -12.0) || (((x_14 + (-1.0 * _x_x_8)) == -16.0) || (((x_12 + (-1.0 * _x_x_8)) == -8.0) || (((x_11 + (-1.0 * _x_x_8)) == -2.0) || (((x_10 + (-1.0 * _x_x_8)) == -11.0) || (((x_6 + (-1.0 * _x_x_8)) == -13.0) || (((x_4 + (-1.0 * _x_x_8)) == -10.0) || (((x_2 + (-1.0 * _x_x_8)) == -3.0) || ((x_3 + (-1.0 * _x_x_8)) == -15.0)))))))))))) && ((((x_18 + (-1.0 * _x_x_9)) <= -5.0) && (((x_15 + (-1.0 * _x_x_9)) <= -6.0) && (((x_14 + (-1.0 * _x_x_9)) <= -18.0) && (((x_10 + (-1.0 * _x_x_9)) <= -10.0) && (((x_9 + (-1.0 * _x_x_9)) <= -2.0) && (((x_5 + (-1.0 * _x_x_9)) <= -19.0) && (((x_4 + (-1.0 * _x_x_9)) <= -5.0) && (((x_3 + (-1.0 * _x_x_9)) <= -6.0) && (((x_0 + (-1.0 * _x_x_9)) <= -20.0) && ((x_2 + (-1.0 * _x_x_9)) <= -12.0)))))))))) && (((x_18 + (-1.0 * _x_x_9)) == -5.0) || (((x_15 + (-1.0 * _x_x_9)) == -6.0) || (((x_14 + (-1.0 * _x_x_9)) == -18.0) || (((x_10 + (-1.0 * _x_x_9)) == -10.0) || (((x_9 + (-1.0 * _x_x_9)) == -2.0) || (((x_5 + (-1.0 * _x_x_9)) == -19.0) || (((x_4 + (-1.0 * _x_x_9)) == -5.0) || (((x_3 + (-1.0 * _x_x_9)) == -6.0) || (((x_0 + (-1.0 * _x_x_9)) == -20.0) || ((x_2 + (-1.0 * _x_x_9)) == -12.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_10)) <= -14.0) && (((x_17 + (-1.0 * _x_x_10)) <= -12.0) && (((x_15 + (-1.0 * _x_x_10)) <= -6.0) && (((x_13 + (-1.0 * _x_x_10)) <= -7.0) && (((x_12 + (-1.0 * _x_x_10)) <= -5.0) && (((x_11 + (-1.0 * _x_x_10)) <= -19.0) && (((x_7 + (-1.0 * _x_x_10)) <= -15.0) && (((x_6 + (-1.0 * _x_x_10)) <= -14.0) && (((x_0 + (-1.0 * _x_x_10)) <= -10.0) && ((x_2 + (-1.0 * _x_x_10)) <= -13.0)))))))))) && (((x_19 + (-1.0 * _x_x_10)) == -14.0) || (((x_17 + (-1.0 * _x_x_10)) == -12.0) || (((x_15 + (-1.0 * _x_x_10)) == -6.0) || (((x_13 + (-1.0 * _x_x_10)) == -7.0) || (((x_12 + (-1.0 * _x_x_10)) == -5.0) || (((x_11 + (-1.0 * _x_x_10)) == -19.0) || (((x_7 + (-1.0 * _x_x_10)) == -15.0) || (((x_6 + (-1.0 * _x_x_10)) == -14.0) || (((x_0 + (-1.0 * _x_x_10)) == -10.0) || ((x_2 + (-1.0 * _x_x_10)) == -13.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_11)) <= -12.0) && (((x_17 + (-1.0 * _x_x_11)) <= -20.0) && (((x_15 + (-1.0 * _x_x_11)) <= -10.0) && (((x_12 + (-1.0 * _x_x_11)) <= -10.0) && (((x_11 + (-1.0 * _x_x_11)) <= -4.0) && (((x_9 + (-1.0 * _x_x_11)) <= -4.0) && (((x_8 + (-1.0 * _x_x_11)) <= -2.0) && (((x_4 + (-1.0 * _x_x_11)) <= -13.0) && (((x_0 + (-1.0 * _x_x_11)) <= -10.0) && ((x_2 + (-1.0 * _x_x_11)) <= -5.0)))))))))) && (((x_19 + (-1.0 * _x_x_11)) == -12.0) || (((x_17 + (-1.0 * _x_x_11)) == -20.0) || (((x_15 + (-1.0 * _x_x_11)) == -10.0) || (((x_12 + (-1.0 * _x_x_11)) == -10.0) || (((x_11 + (-1.0 * _x_x_11)) == -4.0) || (((x_9 + (-1.0 * _x_x_11)) == -4.0) || (((x_8 + (-1.0 * _x_x_11)) == -2.0) || (((x_4 + (-1.0 * _x_x_11)) == -13.0) || (((x_0 + (-1.0 * _x_x_11)) == -10.0) || ((x_2 + (-1.0 * _x_x_11)) == -5.0)))))))))))) && ((((x_18 + (-1.0 * _x_x_12)) <= -17.0) && (((x_17 + (-1.0 * _x_x_12)) <= -2.0) && (((x_16 + (-1.0 * _x_x_12)) <= -11.0) && (((x_14 + (-1.0 * _x_x_12)) <= -9.0) && (((x_13 + (-1.0 * _x_x_12)) <= -5.0) && (((x_11 + (-1.0 * _x_x_12)) <= -10.0) && (((x_9 + (-1.0 * _x_x_12)) <= -16.0) && (((x_8 + (-1.0 * _x_x_12)) <= -7.0) && (((x_4 + (-1.0 * _x_x_12)) <= -20.0) && ((x_7 + (-1.0 * _x_x_12)) <= -17.0)))))))))) && (((x_18 + (-1.0 * _x_x_12)) == -17.0) || (((x_17 + (-1.0 * _x_x_12)) == -2.0) || (((x_16 + (-1.0 * _x_x_12)) == -11.0) || (((x_14 + (-1.0 * _x_x_12)) == -9.0) || (((x_13 + (-1.0 * _x_x_12)) == -5.0) || (((x_11 + (-1.0 * _x_x_12)) == -10.0) || (((x_9 + (-1.0 * _x_x_12)) == -16.0) || (((x_8 + (-1.0 * _x_x_12)) == -7.0) || (((x_4 + (-1.0 * _x_x_12)) == -20.0) || ((x_7 + (-1.0 * _x_x_12)) == -17.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_13)) <= -15.0) && (((x_17 + (-1.0 * _x_x_13)) <= -17.0) && (((x_15 + (-1.0 * _x_x_13)) <= -16.0) && (((x_14 + (-1.0 * _x_x_13)) <= -20.0) && (((x_12 + (-1.0 * _x_x_13)) <= -1.0) && (((x_11 + (-1.0 * _x_x_13)) <= -3.0) && (((x_9 + (-1.0 * _x_x_13)) <= -19.0) && (((x_8 + (-1.0 * _x_x_13)) <= -12.0) && (((x_1 + (-1.0 * _x_x_13)) <= -10.0) && ((x_6 + (-1.0 * _x_x_13)) <= -1.0)))))))))) && (((x_19 + (-1.0 * _x_x_13)) == -15.0) || (((x_17 + (-1.0 * _x_x_13)) == -17.0) || (((x_15 + (-1.0 * _x_x_13)) == -16.0) || (((x_14 + (-1.0 * _x_x_13)) == -20.0) || (((x_12 + (-1.0 * _x_x_13)) == -1.0) || (((x_11 + (-1.0 * _x_x_13)) == -3.0) || (((x_9 + (-1.0 * _x_x_13)) == -19.0) || (((x_8 + (-1.0 * _x_x_13)) == -12.0) || (((x_1 + (-1.0 * _x_x_13)) == -10.0) || ((x_6 + (-1.0 * _x_x_13)) == -1.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_14)) <= -5.0) && (((x_18 + (-1.0 * _x_x_14)) <= -4.0) && (((x_17 + (-1.0 * _x_x_14)) <= -16.0) && (((x_15 + (-1.0 * _x_x_14)) <= -3.0) && (((x_14 + (-1.0 * _x_x_14)) <= -19.0) && (((x_10 + (-1.0 * _x_x_14)) <= -14.0) && (((x_4 + (-1.0 * _x_x_14)) <= -7.0) && (((x_3 + (-1.0 * _x_x_14)) <= -3.0) && (((x_0 + (-1.0 * _x_x_14)) <= -13.0) && ((x_2 + (-1.0 * _x_x_14)) <= -20.0)))))))))) && (((x_19 + (-1.0 * _x_x_14)) == -5.0) || (((x_18 + (-1.0 * _x_x_14)) == -4.0) || (((x_17 + (-1.0 * _x_x_14)) == -16.0) || (((x_15 + (-1.0 * _x_x_14)) == -3.0) || (((x_14 + (-1.0 * _x_x_14)) == -19.0) || (((x_10 + (-1.0 * _x_x_14)) == -14.0) || (((x_4 + (-1.0 * _x_x_14)) == -7.0) || (((x_3 + (-1.0 * _x_x_14)) == -3.0) || (((x_0 + (-1.0 * _x_x_14)) == -13.0) || ((x_2 + (-1.0 * _x_x_14)) == -20.0)))))))))))) && ((((x_17 + (-1.0 * _x_x_15)) <= -17.0) && (((x_16 + (-1.0 * _x_x_15)) <= -3.0) && (((x_11 + (-1.0 * _x_x_15)) <= -17.0) && (((x_10 + (-1.0 * _x_x_15)) <= -8.0) && (((x_9 + (-1.0 * _x_x_15)) <= -6.0) && (((x_8 + (-1.0 * _x_x_15)) <= -7.0) && (((x_3 + (-1.0 * _x_x_15)) <= -15.0) && (((x_2 + (-1.0 * _x_x_15)) <= -3.0) && (((x_0 + (-1.0 * _x_x_15)) <= -9.0) && ((x_1 + (-1.0 * _x_x_15)) <= -15.0)))))))))) && (((x_17 + (-1.0 * _x_x_15)) == -17.0) || (((x_16 + (-1.0 * _x_x_15)) == -3.0) || (((x_11 + (-1.0 * _x_x_15)) == -17.0) || (((x_10 + (-1.0 * _x_x_15)) == -8.0) || (((x_9 + (-1.0 * _x_x_15)) == -6.0) || (((x_8 + (-1.0 * _x_x_15)) == -7.0) || (((x_3 + (-1.0 * _x_x_15)) == -15.0) || (((x_2 + (-1.0 * _x_x_15)) == -3.0) || (((x_0 + (-1.0 * _x_x_15)) == -9.0) || ((x_1 + (-1.0 * _x_x_15)) == -15.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_16)) <= -15.0) && (((x_17 + (-1.0 * _x_x_16)) <= -17.0) && (((x_15 + (-1.0 * _x_x_16)) <= -13.0) && (((x_12 + (-1.0 * _x_x_16)) <= -13.0) && (((x_11 + (-1.0 * _x_x_16)) <= -4.0) && (((x_9 + (-1.0 * _x_x_16)) <= -19.0) && (((x_8 + (-1.0 * _x_x_16)) <= -5.0) && (((x_4 + (-1.0 * _x_x_16)) <= -13.0) && (((x_2 + (-1.0 * _x_x_16)) <= -20.0) && ((x_3 + (-1.0 * _x_x_16)) <= -12.0)))))))))) && (((x_19 + (-1.0 * _x_x_16)) == -15.0) || (((x_17 + (-1.0 * _x_x_16)) == -17.0) || (((x_15 + (-1.0 * _x_x_16)) == -13.0) || (((x_12 + (-1.0 * _x_x_16)) == -13.0) || (((x_11 + (-1.0 * _x_x_16)) == -4.0) || (((x_9 + (-1.0 * _x_x_16)) == -19.0) || (((x_8 + (-1.0 * _x_x_16)) == -5.0) || (((x_4 + (-1.0 * _x_x_16)) == -13.0) || (((x_2 + (-1.0 * _x_x_16)) == -20.0) || ((x_3 + (-1.0 * _x_x_16)) == -12.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_17)) <= -2.0) && (((x_17 + (-1.0 * _x_x_17)) <= -3.0) && (((x_15 + (-1.0 * _x_x_17)) <= -4.0) && (((x_14 + (-1.0 * _x_x_17)) <= -16.0) && (((x_13 + (-1.0 * _x_x_17)) <= -13.0) && (((x_7 + (-1.0 * _x_x_17)) <= -20.0) && (((x_6 + (-1.0 * _x_x_17)) <= -2.0) && (((x_5 + (-1.0 * _x_x_17)) <= -10.0) && (((x_0 + (-1.0 * _x_x_17)) <= -18.0) && ((x_4 + (-1.0 * _x_x_17)) <= -8.0)))))))))) && (((x_19 + (-1.0 * _x_x_17)) == -2.0) || (((x_17 + (-1.0 * _x_x_17)) == -3.0) || (((x_15 + (-1.0 * _x_x_17)) == -4.0) || (((x_14 + (-1.0 * _x_x_17)) == -16.0) || (((x_13 + (-1.0 * _x_x_17)) == -13.0) || (((x_7 + (-1.0 * _x_x_17)) == -20.0) || (((x_6 + (-1.0 * _x_x_17)) == -2.0) || (((x_5 + (-1.0 * _x_x_17)) == -10.0) || (((x_0 + (-1.0 * _x_x_17)) == -18.0) || ((x_4 + (-1.0 * _x_x_17)) == -8.0)))))))))))) && ((((x_18 + (-1.0 * _x_x_18)) <= -8.0) && (((x_16 + (-1.0 * _x_x_18)) <= -17.0) && (((x_15 + (-1.0 * _x_x_18)) <= -18.0) && (((x_14 + (-1.0 * _x_x_18)) <= -15.0) && (((x_12 + (-1.0 * _x_x_18)) <= -16.0) && (((x_10 + (-1.0 * _x_x_18)) <= -9.0) && (((x_8 + (-1.0 * _x_x_18)) <= -7.0) && (((x_6 + (-1.0 * _x_x_18)) <= -2.0) && (((x_2 + (-1.0 * _x_x_18)) <= -3.0) && ((x_5 + (-1.0 * _x_x_18)) <= -19.0)))))))))) && (((x_18 + (-1.0 * _x_x_18)) == -8.0) || (((x_16 + (-1.0 * _x_x_18)) == -17.0) || (((x_15 + (-1.0 * _x_x_18)) == -18.0) || (((x_14 + (-1.0 * _x_x_18)) == -15.0) || (((x_12 + (-1.0 * _x_x_18)) == -16.0) || (((x_10 + (-1.0 * _x_x_18)) == -9.0) || (((x_8 + (-1.0 * _x_x_18)) == -7.0) || (((x_6 + (-1.0 * _x_x_18)) == -2.0) || (((x_2 + (-1.0 * _x_x_18)) == -3.0) || ((x_5 + (-1.0 * _x_x_18)) == -19.0)))))))))))) && ((((x_19 + (-1.0 * _x_x_19)) <= -19.0) && (((x_17 + (-1.0 * _x_x_19)) <= -19.0) && (((x_16 + (-1.0 * _x_x_19)) <= -10.0) && (((x_14 + (-1.0 * _x_x_19)) <= -7.0) && (((x_7 + (-1.0 * _x_x_19)) <= -2.0) && (((x_6 + (-1.0 * _x_x_19)) <= -16.0) && (((x_5 + (-1.0 * _x_x_19)) <= -7.0) && (((x_3 + (-1.0 * _x_x_19)) <= -10.0) && (((x_0 + (-1.0 * _x_x_19)) <= -13.0) && ((x_2 + (-1.0 * _x_x_19)) <= -4.0)))))))))) && (((x_19 + (-1.0 * _x_x_19)) == -19.0) || (((x_17 + (-1.0 * _x_x_19)) == -19.0) || (((x_16 + (-1.0 * _x_x_19)) == -10.0) || (((x_14 + (-1.0 * _x_x_19)) == -7.0) || (((x_7 + (-1.0 * _x_x_19)) == -2.0) || (((x_6 + (-1.0 * _x_x_19)) == -16.0) || (((x_5 + (-1.0 * _x_x_19)) == -7.0) || (((x_3 + (-1.0 * _x_x_19)) == -10.0) || (((x_0 + (-1.0 * _x_x_19)) == -13.0) || ((x_2 + (-1.0 * _x_x_19)) == -4.0)))))))))))) && ((((_EL_U_1279 == ((_x__EL_U_1279 && ((_x_x_10 + (-1.0 * _x_x_16)) <= -2.0)) || (12.0 <= (_x_x_0 + (-1.0 * _x_x_13))))) && (_EL_U_1281 == (((_x__EL_U_1279 && ((_x_x_10 + (-1.0 * _x_x_16)) <= -2.0)) || (12.0 <= (_x_x_0 + (-1.0 * _x_x_13)))) || (_x__EL_U_1281 && ((_x_x_3 + (-1.0 * _x_x_12)) <= 19.0))))) && (_x__J1299 == (( !(_J1299 && _J1308)) && ((_J1299 && _J1308) || (((12.0 <= (x_0 + (-1.0 * x_13))) || ( !((12.0 <= (x_0 + (-1.0 * x_13))) || (((x_10 + (-1.0 * x_16)) <= -2.0) && _EL_U_1279)))) || _J1299))))) && (_x__J1308 == (( !(_J1299 && _J1308)) && ((_J1299 && _J1308) || ((((12.0 <= (x_0 + (-1.0 * x_13))) || (((x_10 + (-1.0 * x_16)) <= -2.0) && _EL_U_1279)) || ( !(((12.0 <= (x_0 + (-1.0 * x_13))) || (((x_10 + (-1.0 * x_16)) <= -2.0) && _EL_U_1279)) || (((x_3 + (-1.0 * x_12)) <= 19.0) && _EL_U_1281)))) || _J1308))))));
      _J1308 = _x__J1308;
      _J1299 = _x__J1299;
      _EL_U_1281 = _x__EL_U_1281;
      x_12 = _x_x_12;
      x_15 = _x_x_15;
      x_3 = _x_x_3;
      _EL_U_1279 = _x__EL_U_1279;
      x_16 = _x_x_16;
      x_10 = _x_x_10;
      x_18 = _x_x_18;
      x_13 = _x_x_13;
      x_0 = _x_x_0;
      x_1 = _x_x_1;
      x_2 = _x_x_2;
      x_4 = _x_x_4;
      x_5 = _x_x_5;
      x_6 = _x_x_6;
      x_7 = _x_x_7;
      x_14 = _x_x_14;
      x_17 = _x_x_17;
      x_19 = _x_x_19;
      x_9 = _x_x_9;
      x_8 = _x_x_8;
      x_11 = _x_x_11;
  
    }
  }
  