text: //@ ltl invariant negative: (X (AP(x_1 - x_2 >= -20) && ([] AP(x_2 - x_8 >= -16))));
  float x_0;
  float x_1;
  float x_2;
  float x_3;
  float x_4;
  float x_5;
  float x_6;
  float x_7;
  float x_8;
  float x_9;
  float x_10;
  float x_11;
  int main()
  {
    float x_0_;
    float x_1_;
    float x_2_;
    float x_3_;
    float x_4_;
    float x_5_;
    float x_6_;
    float x_7_;
    float x_8_;
    float x_9_;
    float x_10_;
    float x_11_;
    while(1) {
  x_0_ = (((20.0 + x_1) > ((15.0 + x_2) > (20.0 + x_4)? (15.0 + x_2) : (20.0 + x_4))? (20.0 + x_1) : ((15.0 + x_2) > (20.0 + x_4)? (15.0 + x_2) : (20.0 + x_4))) > ((6.0 + x_5) > ((5.0 + x_9) > (11.0 + x_11)? (5.0 + x_9) : (11.0 + x_11))? (6.0 + x_5) : ((5.0 + x_9) > (11.0 + x_11)? (5.0 + x_9) : (11.0 + x_11)))? ((20.0 + x_1) > ((15.0 + x_2) > (20.0 + x_4)? (15.0 + x_2) : (20.0 + x_4))? (20.0 + x_1) : ((15.0 + x_2) > (20.0 + x_4)? (15.0 + x_2) : (20.0 + x_4))) : ((6.0 + x_5) > ((5.0 + x_9) > (11.0 + x_11)? (5.0 + x_9) : (11.0 + x_11))? (6.0 + x_5) : ((5.0 + x_9) > (11.0 + x_11)? (5.0 + x_9) : (11.0 + x_11))));
  x_1_ = (((15.0 + x_1) > ((11.0 + x_2) > (13.0 + x_3)? (11.0 + x_2) : (13.0 + x_3))? (15.0 + x_1) : ((11.0 + x_2) > (13.0 + x_3)? (11.0 + x_2) : (13.0 + x_3))) > ((3.0 + x_4) > ((4.0 + x_7) > (8.0 + x_8)? (4.0 + x_7) : (8.0 + x_8))? (3.0 + x_4) : ((4.0 + x_7) > (8.0 + x_8)? (4.0 + x_7) : (8.0 + x_8)))? ((15.0 + x_1) > ((11.0 + x_2) > (13.0 + x_3)? (11.0 + x_2) : (13.0 + x_3))? (15.0 + x_1) : ((11.0 + x_2) > (13.0 + x_3)? (11.0 + x_2) : (13.0 + x_3))) : ((3.0 + x_4) > ((4.0 + x_7) > (8.0 + x_8)? (4.0 + x_7) : (8.0 + x_8))? (3.0 + x_4) : ((4.0 + x_7) > (8.0 + x_8)? (4.0 + x_7) : (8.0 + x_8))));
  x_2_ = (((13.0 + x_3) > ((4.0 + x_4) > (9.0 + x_5)? (4.0 + x_4) : (9.0 + x_5))? (13.0 + x_3) : ((4.0 + x_4) > (9.0 + x_5)? (4.0 + x_4) : (9.0 + x_5))) > ((11.0 + x_6) > ((15.0 + x_7) > (8.0 + x_9)? (15.0 + x_7) : (8.0 + x_9))? (11.0 + x_6) : ((15.0 + x_7) > (8.0 + x_9)? (15.0 + x_7) : (8.0 + x_9)))? ((13.0 + x_3) > ((4.0 + x_4) > (9.0 + x_5)? (4.0 + x_4) : (9.0 + x_5))? (13.0 + x_3) : ((4.0 + x_4) > (9.0 + x_5)? (4.0 + x_4) : (9.0 + x_5))) : ((11.0 + x_6) > ((15.0 + x_7) > (8.0 + x_9)? (15.0 + x_7) : (8.0 + x_9))? (11.0 + x_6) : ((15.0 + x_7) > (8.0 + x_9)? (15.0 + x_7) : (8.0 + x_9))));
  x_3_ = (((1.0 + x_1) > ((20.0 + x_2) > (11.0 + x_3)? (20.0 + x_2) : (11.0 + x_3))? (1.0 + x_1) : ((20.0 + x_2) > (11.0 + x_3)? (20.0 + x_2) : (11.0 + x_3))) > ((5.0 + x_6) > ((13.0 + x_9) > (20.0 + x_11)? (13.0 + x_9) : (20.0 + x_11))? (5.0 + x_6) : ((13.0 + x_9) > (20.0 + x_11)? (13.0 + x_9) : (20.0 + x_11)))? ((1.0 + x_1) > ((20.0 + x_2) > (11.0 + x_3)? (20.0 + x_2) : (11.0 + x_3))? (1.0 + x_1) : ((20.0 + x_2) > (11.0 + x_3)? (20.0 + x_2) : (11.0 + x_3))) : ((5.0 + x_6) > ((13.0 + x_9) > (20.0 + x_11)? (13.0 + x_9) : (20.0 + x_11))? (5.0 + x_6) : ((13.0 + x_9) > (20.0 + x_11)? (13.0 + x_9) : (20.0 + x_11))));
  x_4_ = (((14.0 + x_0) > ((1.0 + x_1) > (1.0 + x_2)? (1.0 + x_1) : (1.0 + x_2))? (14.0 + x_0) : ((1.0 + x_1) > (1.0 + x_2)? (1.0 + x_1) : (1.0 + x_2))) > ((8.0 + x_6) > ((17.0 + x_10) > (15.0 + x_11)? (17.0 + x_10) : (15.0 + x_11))? (8.0 + x_6) : ((17.0 + x_10) > (15.0 + x_11)? (17.0 + x_10) : (15.0 + x_11)))? ((14.0 + x_0) > ((1.0 + x_1) > (1.0 + x_2)? (1.0 + x_1) : (1.0 + x_2))? (14.0 + x_0) : ((1.0 + x_1) > (1.0 + x_2)? (1.0 + x_1) : (1.0 + x_2))) : ((8.0 + x_6) > ((17.0 + x_10) > (15.0 + x_11)? (17.0 + x_10) : (15.0 + x_11))? (8.0 + x_6) : ((17.0 + x_10) > (15.0 + x_11)? (17.0 + x_10) : (15.0 + x_11))));
  x_5_ = (((16.0 + x_0) > ((2.0 + x_2) > (6.0 + x_4)? (2.0 + x_2) : (6.0 + x_4))? (16.0 + x_0) : ((2.0 + x_2) > (6.0 + x_4)? (2.0 + x_2) : (6.0 + x_4))) > ((7.0 + x_6) > ((5.0 + x_7) > (3.0 + x_11)? (5.0 + x_7) : (3.0 + x_11))? (7.0 + x_6) : ((5.0 + x_7) > (3.0 + x_11)? (5.0 + x_7) : (3.0 + x_11)))? ((16.0 + x_0) > ((2.0 + x_2) > (6.0 + x_4)? (2.0 + x_2) : (6.0 + x_4))? (16.0 + x_0) : ((2.0 + x_2) > (6.0 + x_4)? (2.0 + x_2) : (6.0 + x_4))) : ((7.0 + x_6) > ((5.0 + x_7) > (3.0 + x_11)? (5.0 + x_7) : (3.0 + x_11))? (7.0 + x_6) : ((5.0 + x_7) > (3.0 + x_11)? (5.0 + x_7) : (3.0 + x_11))));
  x_6_ = (((13.0 + x_0) > ((1.0 + x_1) > (6.0 + x_3)? (1.0 + x_1) : (6.0 + x_3))? (13.0 + x_0) : ((1.0 + x_1) > (6.0 + x_3)? (1.0 + x_1) : (6.0 + x_3))) > ((20.0 + x_6) > ((17.0 + x_7) > (1.0 + x_8)? (17.0 + x_7) : (1.0 + x_8))? (20.0 + x_6) : ((17.0 + x_7) > (1.0 + x_8)? (17.0 + x_7) : (1.0 + x_8)))? ((13.0 + x_0) > ((1.0 + x_1) > (6.0 + x_3)? (1.0 + x_1) : (6.0 + x_3))? (13.0 + x_0) : ((1.0 + x_1) > (6.0 + x_3)? (1.0 + x_1) : (6.0 + x_3))) : ((20.0 + x_6) > ((17.0 + x_7) > (1.0 + x_8)? (17.0 + x_7) : (1.0 + x_8))? (20.0 + x_6) : ((17.0 + x_7) > (1.0 + x_8)? (17.0 + x_7) : (1.0 + x_8))));
  x_7_ = (((17.0 + x_1) > ((20.0 + x_3) > (9.0 + x_5)? (20.0 + x_3) : (9.0 + x_5))? (17.0 + x_1) : ((20.0 + x_3) > (9.0 + x_5)? (20.0 + x_3) : (9.0 + x_5))) > ((15.0 + x_9) > ((19.0 + x_10) > (3.0 + x_11)? (19.0 + x_10) : (3.0 + x_11))? (15.0 + x_9) : ((19.0 + x_10) > (3.0 + x_11)? (19.0 + x_10) : (3.0 + x_11)))? ((17.0 + x_1) > ((20.0 + x_3) > (9.0 + x_5)? (20.0 + x_3) : (9.0 + x_5))? (17.0 + x_1) : ((20.0 + x_3) > (9.0 + x_5)? (20.0 + x_3) : (9.0 + x_5))) : ((15.0 + x_9) > ((19.0 + x_10) > (3.0 + x_11)? (19.0 + x_10) : (3.0 + x_11))? (15.0 + x_9) : ((19.0 + x_10) > (3.0 + x_11)? (19.0 + x_10) : (3.0 + x_11))));
  x_8_ = (((2.0 + x_0) > ((17.0 + x_2) > (12.0 + x_4)? (17.0 + x_2) : (12.0 + x_4))? (2.0 + x_0) : ((17.0 + x_2) > (12.0 + x_4)? (17.0 + x_2) : (12.0 + x_4))) > ((1.0 + x_7) > ((14.0 + x_9) > (2.0 + x_11)? (14.0 + x_9) : (2.0 + x_11))? (1.0 + x_7) : ((14.0 + x_9) > (2.0 + x_11)? (14.0 + x_9) : (2.0 + x_11)))? ((2.0 + x_0) > ((17.0 + x_2) > (12.0 + x_4)? (17.0 + x_2) : (12.0 + x_4))? (2.0 + x_0) : ((17.0 + x_2) > (12.0 + x_4)? (17.0 + x_2) : (12.0 + x_4))) : ((1.0 + x_7) > ((14.0 + x_9) > (2.0 + x_11)? (14.0 + x_9) : (2.0 + x_11))? (1.0 + x_7) : ((14.0 + x_9) > (2.0 + x_11)? (14.0 + x_9) : (2.0 + x_11))));
  x_9_ = (((13.0 + x_1) > ((6.0 + x_6) > (3.0 + x_7)? (6.0 + x_6) : (3.0 + x_7))? (13.0 + x_1) : ((6.0 + x_6) > (3.0 + x_7)? (6.0 + x_6) : (3.0 + x_7))) > ((10.0 + x_8) > ((16.0 + x_9) > (2.0 + x_11)? (16.0 + x_9) : (2.0 + x_11))? (10.0 + x_8) : ((16.0 + x_9) > (2.0 + x_11)? (16.0 + x_9) : (2.0 + x_11)))? ((13.0 + x_1) > ((6.0 + x_6) > (3.0 + x_7)? (6.0 + x_6) : (3.0 + x_7))? (13.0 + x_1) : ((6.0 + x_6) > (3.0 + x_7)? (6.0 + x_6) : (3.0 + x_7))) : ((10.0 + x_8) > ((16.0 + x_9) > (2.0 + x_11)? (16.0 + x_9) : (2.0 + x_11))? (10.0 + x_8) : ((16.0 + x_9) > (2.0 + x_11)? (16.0 + x_9) : (2.0 + x_11))));
  x_10_ = (((2.0 + x_0) > ((8.0 + x_3) > (5.0 + x_4)? (8.0 + x_3) : (5.0 + x_4))? (2.0 + x_0) : ((8.0 + x_3) > (5.0 + x_4)? (8.0 + x_3) : (5.0 + x_4))) > ((19.0 + x_5) > ((20.0 + x_7) > (12.0 + x_10)? (20.0 + x_7) : (12.0 + x_10))? (19.0 + x_5) : ((20.0 + x_7) > (12.0 + x_10)? (20.0 + x_7) : (12.0 + x_10)))? ((2.0 + x_0) > ((8.0 + x_3) > (5.0 + x_4)? (8.0 + x_3) : (5.0 + x_4))? (2.0 + x_0) : ((8.0 + x_3) > (5.0 + x_4)? (8.0 + x_3) : (5.0 + x_4))) : ((19.0 + x_5) > ((20.0 + x_7) > (12.0 + x_10)? (20.0 + x_7) : (12.0 + x_10))? (19.0 + x_5) : ((20.0 + x_7) > (12.0 + x_10)? (20.0 + x_7) : (12.0 + x_10))));
  x_11_ = (((12.0 + x_0) > ((12.0 + x_2) > (5.0 + x_6)? (12.0 + x_2) : (5.0 + x_6))? (12.0 + x_0) : ((12.0 + x_2) > (5.0 + x_6)? (12.0 + x_2) : (5.0 + x_6))) > ((11.0 + x_8) > ((8.0 + x_10) > (11.0 + x_11)? (8.0 + x_10) : (11.0 + x_11))? (11.0 + x_8) : ((8.0 + x_10) > (11.0 + x_11)? (8.0 + x_10) : (11.0 + x_11)))? ((12.0 + x_0) > ((12.0 + x_2) > (5.0 + x_6)? (12.0 + x_2) : (5.0 + x_6))? (12.0 + x_0) : ((12.0 + x_2) > (5.0 + x_6)? (12.0 + x_2) : (5.0 + x_6))) : ((11.0 + x_8) > ((8.0 + x_10) > (11.0 + x_11)? (8.0 + x_10) : (11.0 + x_11))? (11.0 + x_8) : ((8.0 + x_10) > (11.0 + x_11)? (8.0 + x_10) : (11.0 + x_11))));
  x_0 = x_0_;
  x_1 = x_1_;
  x_2 = x_2_;
  x_3 = x_3_;
  x_4 = x_4_;
  x_5 = x_5_;
  x_6 = x_6_;
  x_7 = x_7_;
  x_8 = x_8_;
  x_9 = x_9_;
  x_10 = x_10_;
  x_11 = x_11_;
    }
    return 0;
  }
  