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()
{
float x_12, _x_x_12;
bool _J881, _x__J881;
bool _J875, _x__J875;
bool _EL_U_853, _x__EL_U_853;
float x_10, _x_x_10;
float x_9, _x_x_9;
float x_7, _x_x_7;
float x_2, _x_x_2;
bool _EL_U_855, _x__EL_U_855;
float x_5, _x_x_5;
float x_1, _x_x_1;
float x_4, _x_x_4;
float x_8, _x_x_8;
float x_11, _x_x_11;
float x_14, _x_x_14;
float x_15, _x_x_15;
float x_13, _x_x_13;
float x_0, _x_x_0;
float x_3, _x_x_3;
float x_6, _x_x_6;

  int __steps_to_fair = __VERIFIER_nondet_int();
  x_12 = __VERIFIER_nondet_float();
  _J881 = __VERIFIER_nondet_bool();
  _J875 = __VERIFIER_nondet_bool();
  _EL_U_853 = __VERIFIER_nondet_bool();
  x_10 = __VERIFIER_nondet_float();
  x_9 = __VERIFIER_nondet_float();
  x_7 = __VERIFIER_nondet_float();
  x_2 = __VERIFIER_nondet_float();
  _EL_U_855 = __VERIFIER_nondet_bool();
  x_5 = __VERIFIER_nondet_float();
  x_1 = __VERIFIER_nondet_float();
  x_4 = __VERIFIER_nondet_float();
  x_8 = __VERIFIER_nondet_float();
  x_11 = __VERIFIER_nondet_float();
  x_14 = __VERIFIER_nondet_float();
  x_15 = __VERIFIER_nondet_float();
  x_13 = __VERIFIER_nondet_float();
  x_0 = __VERIFIER_nondet_float();
  x_3 = __VERIFIER_nondet_float();
  x_6 = __VERIFIER_nondet_float();

  bool __ok = (1 && ((( !(_EL_U_855 || ( !(( !(( !(-6.0 <= (x_2 + (-1.0 * x_7)))) && ( !((x_9 + (-1.0 * x_10)) <= 4.0)))) || _EL_U_853)))) && ( !_J875)) && ( !_J881)));
  while (__steps_to_fair >= 0 && __ok) {
    if ((_J875 && _J881)) {
      __steps_to_fair = __VERIFIER_nondet_int();
    } else {
      __steps_to_fair--;
    }
    _x_x_12 = __VERIFIER_nondet_float();
    _x__J881 = __VERIFIER_nondet_bool();
    _x__J875 = __VERIFIER_nondet_bool();
    _x__EL_U_853 = __VERIFIER_nondet_bool();
    _x_x_10 = __VERIFIER_nondet_float();
    _x_x_9 = __VERIFIER_nondet_float();
    _x_x_7 = __VERIFIER_nondet_float();
    _x_x_2 = __VERIFIER_nondet_float();
    _x__EL_U_855 = __VERIFIER_nondet_bool();
    _x_x_5 = __VERIFIER_nondet_float();
    _x_x_1 = __VERIFIER_nondet_float();
    _x_x_4 = __VERIFIER_nondet_float();
    _x_x_8 = __VERIFIER_nondet_float();
    _x_x_11 = __VERIFIER_nondet_float();
    _x_x_14 = __VERIFIER_nondet_float();
    _x_x_15 = __VERIFIER_nondet_float();
    _x_x_13 = __VERIFIER_nondet_float();
    _x_x_0 = __VERIFIER_nondet_float();
    _x_x_3 = __VERIFIER_nondet_float();
    _x_x_6 = __VERIFIER_nondet_float();

    __ok = ((((((((((((((((((((x_14 + (-1.0 * _x_x_0)) <= -7.0) && (((x_13 + (-1.0 * _x_x_0)) <= -17.0) && (((x_11 + (-1.0 * _x_x_0)) <= -9.0) && (((x_9 + (-1.0 * _x_x_0)) <= -18.0) && (((x_8 + (-1.0 * _x_x_0)) <= -19.0) && (((x_7 + (-1.0 * _x_x_0)) <= -1.0) && (((x_1 + (-1.0 * _x_x_0)) <= -12.0) && ((x_3 + (-1.0 * _x_x_0)) <= -20.0)))))))) && (((x_14 + (-1.0 * _x_x_0)) == -7.0) || (((x_13 + (-1.0 * _x_x_0)) == -17.0) || (((x_11 + (-1.0 * _x_x_0)) == -9.0) || (((x_9 + (-1.0 * _x_x_0)) == -18.0) || (((x_8 + (-1.0 * _x_x_0)) == -19.0) || (((x_7 + (-1.0 * _x_x_0)) == -1.0) || (((x_1 + (-1.0 * _x_x_0)) == -12.0) || ((x_3 + (-1.0 * _x_x_0)) == -20.0))))))))) && ((((x_15 + (-1.0 * _x_x_1)) <= -9.0) && (((x_13 + (-1.0 * _x_x_1)) <= -11.0) && (((x_11 + (-1.0 * _x_x_1)) <= -2.0) && (((x_8 + (-1.0 * _x_x_1)) <= -14.0) && (((x_7 + (-1.0 * _x_x_1)) <= -7.0) && (((x_6 + (-1.0 * _x_x_1)) <= -14.0) && (((x_3 + (-1.0 * _x_x_1)) <= -9.0) && ((x_5 + (-1.0 * _x_x_1)) <= -16.0)))))))) && (((x_15 + (-1.0 * _x_x_1)) == -9.0) || (((x_13 + (-1.0 * _x_x_1)) == -11.0) || (((x_11 + (-1.0 * _x_x_1)) == -2.0) || (((x_8 + (-1.0 * _x_x_1)) == -14.0) || (((x_7 + (-1.0 * _x_x_1)) == -7.0) || (((x_6 + (-1.0 * _x_x_1)) == -14.0) || (((x_3 + (-1.0 * _x_x_1)) == -9.0) || ((x_5 + (-1.0 * _x_x_1)) == -16.0)))))))))) && ((((x_13 + (-1.0 * _x_x_2)) <= -18.0) && (((x_12 + (-1.0 * _x_x_2)) <= -5.0) && (((x_11 + (-1.0 * _x_x_2)) <= -13.0) && (((x_10 + (-1.0 * _x_x_2)) <= -6.0) && (((x_9 + (-1.0 * _x_x_2)) <= -2.0) && (((x_8 + (-1.0 * _x_x_2)) <= -18.0) && (((x_1 + (-1.0 * _x_x_2)) <= -13.0) && ((x_3 + (-1.0 * _x_x_2)) <= -9.0)))))))) && (((x_13 + (-1.0 * _x_x_2)) == -18.0) || (((x_12 + (-1.0 * _x_x_2)) == -5.0) || (((x_11 + (-1.0 * _x_x_2)) == -13.0) || (((x_10 + (-1.0 * _x_x_2)) == -6.0) || (((x_9 + (-1.0 * _x_x_2)) == -2.0) || (((x_8 + (-1.0 * _x_x_2)) == -18.0) || (((x_1 + (-1.0 * _x_x_2)) == -13.0) || ((x_3 + (-1.0 * _x_x_2)) == -9.0)))))))))) && ((((x_14 + (-1.0 * _x_x_3)) <= -18.0) && (((x_11 + (-1.0 * _x_x_3)) <= -14.0) && (((x_10 + (-1.0 * _x_x_3)) <= -4.0) && (((x_8 + (-1.0 * _x_x_3)) <= -17.0) && (((x_7 + (-1.0 * _x_x_3)) <= -5.0) && (((x_6 + (-1.0 * _x_x_3)) <= -20.0) && (((x_2 + (-1.0 * _x_x_3)) <= -7.0) && ((x_4 + (-1.0 * _x_x_3)) <= -7.0)))))))) && (((x_14 + (-1.0 * _x_x_3)) == -18.0) || (((x_11 + (-1.0 * _x_x_3)) == -14.0) || (((x_10 + (-1.0 * _x_x_3)) == -4.0) || (((x_8 + (-1.0 * _x_x_3)) == -17.0) || (((x_7 + (-1.0 * _x_x_3)) == -5.0) || (((x_6 + (-1.0 * _x_x_3)) == -20.0) || (((x_2 + (-1.0 * _x_x_3)) == -7.0) || ((x_4 + (-1.0 * _x_x_3)) == -7.0)))))))))) && ((((x_15 + (-1.0 * _x_x_4)) <= -7.0) && (((x_13 + (-1.0 * _x_x_4)) <= -2.0) && (((x_11 + (-1.0 * _x_x_4)) <= -13.0) && (((x_9 + (-1.0 * _x_x_4)) <= -4.0) && (((x_8 + (-1.0 * _x_x_4)) <= -14.0) && (((x_6 + (-1.0 * _x_x_4)) <= -7.0) && (((x_0 + (-1.0 * _x_x_4)) <= -12.0) && ((x_4 + (-1.0 * _x_x_4)) <= -18.0)))))))) && (((x_15 + (-1.0 * _x_x_4)) == -7.0) || (((x_13 + (-1.0 * _x_x_4)) == -2.0) || (((x_11 + (-1.0 * _x_x_4)) == -13.0) || (((x_9 + (-1.0 * _x_x_4)) == -4.0) || (((x_8 + (-1.0 * _x_x_4)) == -14.0) || (((x_6 + (-1.0 * _x_x_4)) == -7.0) || (((x_0 + (-1.0 * _x_x_4)) == -12.0) || ((x_4 + (-1.0 * _x_x_4)) == -18.0)))))))))) && ((((x_13 + (-1.0 * _x_x_5)) <= -9.0) && (((x_12 + (-1.0 * _x_x_5)) <= -17.0) && (((x_10 + (-1.0 * _x_x_5)) <= -13.0) && (((x_8 + (-1.0 * _x_x_5)) <= -6.0) && (((x_6 + (-1.0 * _x_x_5)) <= -19.0) && (((x_4 + (-1.0 * _x_x_5)) <= -6.0) && (((x_0 + (-1.0 * _x_x_5)) <= -20.0) && ((x_1 + (-1.0 * _x_x_5)) <= -7.0)))))))) && (((x_13 + (-1.0 * _x_x_5)) == -9.0) || (((x_12 + (-1.0 * _x_x_5)) == -17.0) || (((x_10 + (-1.0 * _x_x_5)) == -13.0) || (((x_8 + (-1.0 * _x_x_5)) == -6.0) || (((x_6 + (-1.0 * _x_x_5)) == -19.0) || (((x_4 + (-1.0 * _x_x_5)) == -6.0) || (((x_0 + (-1.0 * _x_x_5)) == -20.0) || ((x_1 + (-1.0 * _x_x_5)) == -7.0)))))))))) && ((((x_14 + (-1.0 * _x_x_6)) <= -18.0) && (((x_11 + (-1.0 * _x_x_6)) <= -15.0) && (((x_7 + (-1.0 * _x_x_6)) <= -15.0) && (((x_5 + (-1.0 * _x_x_6)) <= -10.0) && (((x_4 + (-1.0 * _x_x_6)) <= -6.0) && (((x_2 + (-1.0 * _x_x_6)) <= -3.0) && (((x_0 + (-1.0 * _x_x_6)) <= -15.0) && ((x_1 + (-1.0 * _x_x_6)) <= -15.0)))))))) && (((x_14 + (-1.0 * _x_x_6)) == -18.0) || (((x_11 + (-1.0 * _x_x_6)) == -15.0) || (((x_7 + (-1.0 * _x_x_6)) == -15.0) || (((x_5 + (-1.0 * _x_x_6)) == -10.0) || (((x_4 + (-1.0 * _x_x_6)) == -6.0) || (((x_2 + (-1.0 * _x_x_6)) == -3.0) || (((x_0 + (-1.0 * _x_x_6)) == -15.0) || ((x_1 + (-1.0 * _x_x_6)) == -15.0)))))))))) && ((((x_13 + (-1.0 * _x_x_7)) <= -19.0) && (((x_12 + (-1.0 * _x_x_7)) <= -15.0) && (((x_10 + (-1.0 * _x_x_7)) <= -18.0) && (((x_7 + (-1.0 * _x_x_7)) <= -15.0) && (((x_6 + (-1.0 * _x_x_7)) <= -7.0) && (((x_4 + (-1.0 * _x_x_7)) <= -11.0) && (((x_1 + (-1.0 * _x_x_7)) <= -18.0) && ((x_3 + (-1.0 * _x_x_7)) <= -17.0)))))))) && (((x_13 + (-1.0 * _x_x_7)) == -19.0) || (((x_12 + (-1.0 * _x_x_7)) == -15.0) || (((x_10 + (-1.0 * _x_x_7)) == -18.0) || (((x_7 + (-1.0 * _x_x_7)) == -15.0) || (((x_6 + (-1.0 * _x_x_7)) == -7.0) || (((x_4 + (-1.0 * _x_x_7)) == -11.0) || (((x_1 + (-1.0 * _x_x_7)) == -18.0) || ((x_3 + (-1.0 * _x_x_7)) == -17.0)))))))))) && ((((x_15 + (-1.0 * _x_x_8)) <= -11.0) && (((x_14 + (-1.0 * _x_x_8)) <= -15.0) && (((x_11 + (-1.0 * _x_x_8)) <= -12.0) && (((x_8 + (-1.0 * _x_x_8)) <= -19.0) && (((x_7 + (-1.0 * _x_x_8)) <= -13.0) && (((x_3 + (-1.0 * _x_x_8)) <= -20.0) && (((x_0 + (-1.0 * _x_x_8)) <= -15.0) && ((x_2 + (-1.0 * _x_x_8)) <= -6.0)))))))) && (((x_15 + (-1.0 * _x_x_8)) == -11.0) || (((x_14 + (-1.0 * _x_x_8)) == -15.0) || (((x_11 + (-1.0 * _x_x_8)) == -12.0) || (((x_8 + (-1.0 * _x_x_8)) == -19.0) || (((x_7 + (-1.0 * _x_x_8)) == -13.0) || (((x_3 + (-1.0 * _x_x_8)) == -20.0) || (((x_0 + (-1.0 * _x_x_8)) == -15.0) || ((x_2 + (-1.0 * _x_x_8)) == -6.0)))))))))) && ((((x_15 + (-1.0 * _x_x_9)) <= -5.0) && (((x_14 + (-1.0 * _x_x_9)) <= -12.0) && (((x_13 + (-1.0 * _x_x_9)) <= -4.0) && (((x_11 + (-1.0 * _x_x_9)) <= -10.0) && (((x_8 + (-1.0 * _x_x_9)) <= -8.0) && (((x_6 + (-1.0 * _x_x_9)) <= -9.0) && (((x_3 + (-1.0 * _x_x_9)) <= -9.0) && ((x_5 + (-1.0 * _x_x_9)) <= -11.0)))))))) && (((x_15 + (-1.0 * _x_x_9)) == -5.0) || (((x_14 + (-1.0 * _x_x_9)) == -12.0) || (((x_13 + (-1.0 * _x_x_9)) == -4.0) || (((x_11 + (-1.0 * _x_x_9)) == -10.0) || (((x_8 + (-1.0 * _x_x_9)) == -8.0) || (((x_6 + (-1.0 * _x_x_9)) == -9.0) || (((x_3 + (-1.0 * _x_x_9)) == -9.0) || ((x_5 + (-1.0 * _x_x_9)) == -11.0)))))))))) && ((((x_14 + (-1.0 * _x_x_10)) <= -10.0) && (((x_12 + (-1.0 * _x_x_10)) <= -12.0) && (((x_11 + (-1.0 * _x_x_10)) <= -20.0) && (((x_9 + (-1.0 * _x_x_10)) <= -12.0) && (((x_7 + (-1.0 * _x_x_10)) <= -6.0) && (((x_6 + (-1.0 * _x_x_10)) <= -4.0) && (((x_0 + (-1.0 * _x_x_10)) <= -18.0) && ((x_1 + (-1.0 * _x_x_10)) <= -6.0)))))))) && (((x_14 + (-1.0 * _x_x_10)) == -10.0) || (((x_12 + (-1.0 * _x_x_10)) == -12.0) || (((x_11 + (-1.0 * _x_x_10)) == -20.0) || (((x_9 + (-1.0 * _x_x_10)) == -12.0) || (((x_7 + (-1.0 * _x_x_10)) == -6.0) || (((x_6 + (-1.0 * _x_x_10)) == -4.0) || (((x_0 + (-1.0 * _x_x_10)) == -18.0) || ((x_1 + (-1.0 * _x_x_10)) == -6.0)))))))))) && ((((x_12 + (-1.0 * _x_x_11)) <= -6.0) && (((x_11 + (-1.0 * _x_x_11)) <= -12.0) && (((x_10 + (-1.0 * _x_x_11)) <= -19.0) && (((x_8 + (-1.0 * _x_x_11)) <= -15.0) && (((x_6 + (-1.0 * _x_x_11)) <= -4.0) && (((x_3 + (-1.0 * _x_x_11)) <= -19.0) && (((x_1 + (-1.0 * _x_x_11)) <= -18.0) && ((x_2 + (-1.0 * _x_x_11)) <= -18.0)))))))) && (((x_12 + (-1.0 * _x_x_11)) == -6.0) || (((x_11 + (-1.0 * _x_x_11)) == -12.0) || (((x_10 + (-1.0 * _x_x_11)) == -19.0) || (((x_8 + (-1.0 * _x_x_11)) == -15.0) || (((x_6 + (-1.0 * _x_x_11)) == -4.0) || (((x_3 + (-1.0 * _x_x_11)) == -19.0) || (((x_1 + (-1.0 * _x_x_11)) == -18.0) || ((x_2 + (-1.0 * _x_x_11)) == -18.0)))))))))) && ((((x_14 + (-1.0 * _x_x_12)) <= -20.0) && (((x_11 + (-1.0 * _x_x_12)) <= -20.0) && (((x_9 + (-1.0 * _x_x_12)) <= -5.0) && (((x_7 + (-1.0 * _x_x_12)) <= -15.0) && (((x_3 + (-1.0 * _x_x_12)) <= -7.0) && (((x_2 + (-1.0 * _x_x_12)) <= -2.0) && (((x_0 + (-1.0 * _x_x_12)) <= -16.0) && ((x_1 + (-1.0 * _x_x_12)) <= -3.0)))))))) && (((x_14 + (-1.0 * _x_x_12)) == -20.0) || (((x_11 + (-1.0 * _x_x_12)) == -20.0) || (((x_9 + (-1.0 * _x_x_12)) == -5.0) || (((x_7 + (-1.0 * _x_x_12)) == -15.0) || (((x_3 + (-1.0 * _x_x_12)) == -7.0) || (((x_2 + (-1.0 * _x_x_12)) == -2.0) || (((x_0 + (-1.0 * _x_x_12)) == -16.0) || ((x_1 + (-1.0 * _x_x_12)) == -3.0)))))))))) && ((((x_15 + (-1.0 * _x_x_13)) <= -15.0) && (((x_14 + (-1.0 * _x_x_13)) <= -19.0) && (((x_9 + (-1.0 * _x_x_13)) <= -5.0) && (((x_5 + (-1.0 * _x_x_13)) <= -16.0) && (((x_4 + (-1.0 * _x_x_13)) <= -15.0) && (((x_3 + (-1.0 * _x_x_13)) <= -18.0) && (((x_0 + (-1.0 * _x_x_13)) <= -19.0) && ((x_1 + (-1.0 * _x_x_13)) <= -1.0)))))))) && (((x_15 + (-1.0 * _x_x_13)) == -15.0) || (((x_14 + (-1.0 * _x_x_13)) == -19.0) || (((x_9 + (-1.0 * _x_x_13)) == -5.0) || (((x_5 + (-1.0 * _x_x_13)) == -16.0) || (((x_4 + (-1.0 * _x_x_13)) == -15.0) || (((x_3 + (-1.0 * _x_x_13)) == -18.0) || (((x_0 + (-1.0 * _x_x_13)) == -19.0) || ((x_1 + (-1.0 * _x_x_13)) == -1.0)))))))))) && ((((x_11 + (-1.0 * _x_x_14)) <= -6.0) && (((x_10 + (-1.0 * _x_x_14)) <= -4.0) && (((x_8 + (-1.0 * _x_x_14)) <= -11.0) && (((x_4 + (-1.0 * _x_x_14)) <= -16.0) && (((x_3 + (-1.0 * _x_x_14)) <= -12.0) && (((x_2 + (-1.0 * _x_x_14)) <= -5.0) && (((x_0 + (-1.0 * _x_x_14)) <= -18.0) && ((x_1 + (-1.0 * _x_x_14)) <= -18.0)))))))) && (((x_11 + (-1.0 * _x_x_14)) == -6.0) || (((x_10 + (-1.0 * _x_x_14)) == -4.0) || (((x_8 + (-1.0 * _x_x_14)) == -11.0) || (((x_4 + (-1.0 * _x_x_14)) == -16.0) || (((x_3 + (-1.0 * _x_x_14)) == -12.0) || (((x_2 + (-1.0 * _x_x_14)) == -5.0) || (((x_0 + (-1.0 * _x_x_14)) == -18.0) || ((x_1 + (-1.0 * _x_x_14)) == -18.0)))))))))) && ((((x_15 + (-1.0 * _x_x_15)) <= -6.0) && (((x_14 + (-1.0 * _x_x_15)) <= -15.0) && (((x_11 + (-1.0 * _x_x_15)) <= -15.0) && (((x_9 + (-1.0 * _x_x_15)) <= -5.0) && (((x_8 + (-1.0 * _x_x_15)) <= -14.0) && (((x_4 + (-1.0 * _x_x_15)) <= -20.0) && (((x_1 + (-1.0 * _x_x_15)) <= -4.0) && ((x_2 + (-1.0 * _x_x_15)) <= -15.0)))))))) && (((x_15 + (-1.0 * _x_x_15)) == -6.0) || (((x_14 + (-1.0 * _x_x_15)) == -15.0) || (((x_11 + (-1.0 * _x_x_15)) == -15.0) || (((x_9 + (-1.0 * _x_x_15)) == -5.0) || (((x_8 + (-1.0 * _x_x_15)) == -14.0) || (((x_4 + (-1.0 * _x_x_15)) == -20.0) || (((x_1 + (-1.0 * _x_x_15)) == -4.0) || ((x_2 + (-1.0 * _x_x_15)) == -15.0)))))))))) && ((((_EL_U_853 == (_x__EL_U_853 || ( !(( !((_x_x_9 + (-1.0 * _x_x_10)) <= 4.0)) && ( !(-6.0 <= (_x_x_2 + (-1.0 * _x_x_7)))))))) && (_EL_U_855 == (_x__EL_U_855 || ( !(_x__EL_U_853 || ( !(( !((_x_x_9 + (-1.0 * _x_x_10)) <= 4.0)) && ( !(-6.0 <= (_x_x_2 + (-1.0 * _x_x_7))))))))))) && (_x__J875 == (( !(_J875 && _J881)) && ((_J875 && _J881) || ((( !(( !(-6.0 <= (x_2 + (-1.0 * x_7)))) && ( !((x_9 + (-1.0 * x_10)) <= 4.0)))) || ( !(( !(( !(-6.0 <= (x_2 + (-1.0 * x_7)))) && ( !((x_9 + (-1.0 * x_10)) <= 4.0)))) || _EL_U_853))) || _J875))))) && (_x__J881 == (( !(_J875 && _J881)) && ((_J875 && _J881) || ((( !(( !(( !(-6.0 <= (x_2 + (-1.0 * x_7)))) && ( !((x_9 + (-1.0 * x_10)) <= 4.0)))) || _EL_U_853)) || ( !(_EL_U_855 || ( !(( !(( !(-6.0 <= (x_2 + (-1.0 * x_7)))) && ( !((x_9 + (-1.0 * x_10)) <= 4.0)))) || _EL_U_853))))) || _J881))))));
    x_12 = _x_x_12;
    _J881 = _x__J881;
    _J875 = _x__J875;
    _EL_U_853 = _x__EL_U_853;
    x_10 = _x_x_10;
    x_9 = _x_x_9;
    x_7 = _x_x_7;
    x_2 = _x_x_2;
    _EL_U_855 = _x__EL_U_855;
    x_5 = _x_x_5;
    x_1 = _x_x_1;
    x_4 = _x_x_4;
    x_8 = _x_x_8;
    x_11 = _x_x_11;
    x_14 = _x_x_14;
    x_15 = _x_x_15;
    x_13 = _x_x_13;
    x_0 = _x_x_0;
    x_3 = _x_x_3;
    x_6 = _x_x_6;

  }
}
