text: //@ ltl invariant negative: (<> ((<> AP(x_2 - x_10 > -15)) U AP(x_1 - x_5 > 12)));
  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_ = (((7.0 + x_2) > ((16.0 + x_4) > (3.0 + x_6)? (16.0 + x_4) : (3.0 + x_6))? (7.0 + x_2) : ((16.0 + x_4) > (3.0 + x_6)? (16.0 + x_4) : (3.0 + x_6))) > ((7.0 + x_7) > ((19.0 + x_8) > (4.0 + x_10)? (19.0 + x_8) : (4.0 + x_10))? (7.0 + x_7) : ((19.0 + x_8) > (4.0 + x_10)? (19.0 + x_8) : (4.0 + x_10)))? ((7.0 + x_2) > ((16.0 + x_4) > (3.0 + x_6)? (16.0 + x_4) : (3.0 + x_6))? (7.0 + x_2) : ((16.0 + x_4) > (3.0 + x_6)? (16.0 + x_4) : (3.0 + x_6))) : ((7.0 + x_7) > ((19.0 + x_8) > (4.0 + x_10)? (19.0 + x_8) : (4.0 + x_10))? (7.0 + x_7) : ((19.0 + x_8) > (4.0 + x_10)? (19.0 + x_8) : (4.0 + x_10))));
  x_1_ = (((11.0 + x_1) > ((15.0 + x_3) > (3.0 + x_5)? (15.0 + x_3) : (3.0 + x_5))? (11.0 + x_1) : ((15.0 + x_3) > (3.0 + x_5)? (15.0 + x_3) : (3.0 + x_5))) > ((19.0 + x_6) > ((15.0 + x_7) > (8.0 + x_9)? (15.0 + x_7) : (8.0 + x_9))? (19.0 + x_6) : ((15.0 + x_7) > (8.0 + x_9)? (15.0 + x_7) : (8.0 + x_9)))? ((11.0 + x_1) > ((15.0 + x_3) > (3.0 + x_5)? (15.0 + x_3) : (3.0 + x_5))? (11.0 + x_1) : ((15.0 + x_3) > (3.0 + x_5)? (15.0 + x_3) : (3.0 + x_5))) : ((19.0 + x_6) > ((15.0 + x_7) > (8.0 + x_9)? (15.0 + x_7) : (8.0 + x_9))? (19.0 + x_6) : ((15.0 + x_7) > (8.0 + x_9)? (15.0 + x_7) : (8.0 + x_9))));
  x_2_ = (((8.0 + x_0) > ((17.0 + x_2) > (10.0 + x_3)? (17.0 + x_2) : (10.0 + x_3))? (8.0 + x_0) : ((17.0 + x_2) > (10.0 + x_3)? (17.0 + x_2) : (10.0 + x_3))) > ((4.0 + x_6) > ((2.0 + x_8) > (15.0 + x_10)? (2.0 + x_8) : (15.0 + x_10))? (4.0 + x_6) : ((2.0 + x_8) > (15.0 + x_10)? (2.0 + x_8) : (15.0 + x_10)))? ((8.0 + x_0) > ((17.0 + x_2) > (10.0 + x_3)? (17.0 + x_2) : (10.0 + x_3))? (8.0 + x_0) : ((17.0 + x_2) > (10.0 + x_3)? (17.0 + x_2) : (10.0 + x_3))) : ((4.0 + x_6) > ((2.0 + x_8) > (15.0 + x_10)? (2.0 + x_8) : (15.0 + x_10))? (4.0 + x_6) : ((2.0 + x_8) > (15.0 + x_10)? (2.0 + x_8) : (15.0 + x_10))));
  x_3_ = (((5.0 + x_1) > ((10.0 + x_3) > (3.0 + x_7)? (10.0 + x_3) : (3.0 + x_7))? (5.0 + x_1) : ((10.0 + x_3) > (3.0 + x_7)? (10.0 + x_3) : (3.0 + x_7))) > ((20.0 + x_8) > ((10.0 + x_9) > (19.0 + x_11)? (10.0 + x_9) : (19.0 + x_11))? (20.0 + x_8) : ((10.0 + x_9) > (19.0 + x_11)? (10.0 + x_9) : (19.0 + x_11)))? ((5.0 + x_1) > ((10.0 + x_3) > (3.0 + x_7)? (10.0 + x_3) : (3.0 + x_7))? (5.0 + x_1) : ((10.0 + x_3) > (3.0 + x_7)? (10.0 + x_3) : (3.0 + x_7))) : ((20.0 + x_8) > ((10.0 + x_9) > (19.0 + x_11)? (10.0 + x_9) : (19.0 + x_11))? (20.0 + x_8) : ((10.0 + x_9) > (19.0 + x_11)? (10.0 + x_9) : (19.0 + x_11))));
  x_4_ = (((16.0 + x_2) > ((2.0 + x_4) > (20.0 + x_6)? (2.0 + x_4) : (20.0 + x_6))? (16.0 + x_2) : ((2.0 + x_4) > (20.0 + x_6)? (2.0 + x_4) : (20.0 + x_6))) > ((7.0 + x_9) > ((5.0 + x_10) > (5.0 + x_11)? (5.0 + x_10) : (5.0 + x_11))? (7.0 + x_9) : ((5.0 + x_10) > (5.0 + x_11)? (5.0 + x_10) : (5.0 + x_11)))? ((16.0 + x_2) > ((2.0 + x_4) > (20.0 + x_6)? (2.0 + x_4) : (20.0 + x_6))? (16.0 + x_2) : ((2.0 + x_4) > (20.0 + x_6)? (2.0 + x_4) : (20.0 + x_6))) : ((7.0 + x_9) > ((5.0 + x_10) > (5.0 + x_11)? (5.0 + x_10) : (5.0 + x_11))? (7.0 + x_9) : ((5.0 + x_10) > (5.0 + x_11)? (5.0 + x_10) : (5.0 + x_11))));
  x_5_ = (((16.0 + x_1) > ((9.0 + x_3) > (9.0 + x_5)? (9.0 + x_3) : (9.0 + x_5))? (16.0 + x_1) : ((9.0 + x_3) > (9.0 + x_5)? (9.0 + x_3) : (9.0 + x_5))) > ((14.0 + x_6) > ((13.0 + x_8) > (7.0 + x_10)? (13.0 + x_8) : (7.0 + x_10))? (14.0 + x_6) : ((13.0 + x_8) > (7.0 + x_10)? (13.0 + x_8) : (7.0 + x_10)))? ((16.0 + x_1) > ((9.0 + x_3) > (9.0 + x_5)? (9.0 + x_3) : (9.0 + x_5))? (16.0 + x_1) : ((9.0 + x_3) > (9.0 + x_5)? (9.0 + x_3) : (9.0 + x_5))) : ((14.0 + x_6) > ((13.0 + x_8) > (7.0 + x_10)? (13.0 + x_8) : (7.0 + x_10))? (14.0 + x_6) : ((13.0 + x_8) > (7.0 + x_10)? (13.0 + x_8) : (7.0 + x_10))));
  x_6_ = (((4.0 + x_0) > ((14.0 + x_3) > (17.0 + x_5)? (14.0 + x_3) : (17.0 + x_5))? (4.0 + x_0) : ((14.0 + x_3) > (17.0 + x_5)? (14.0 + x_3) : (17.0 + x_5))) > ((12.0 + x_6) > ((5.0 + x_10) > (2.0 + x_11)? (5.0 + x_10) : (2.0 + x_11))? (12.0 + x_6) : ((5.0 + x_10) > (2.0 + x_11)? (5.0 + x_10) : (2.0 + x_11)))? ((4.0 + x_0) > ((14.0 + x_3) > (17.0 + x_5)? (14.0 + x_3) : (17.0 + x_5))? (4.0 + x_0) : ((14.0 + x_3) > (17.0 + x_5)? (14.0 + x_3) : (17.0 + x_5))) : ((12.0 + x_6) > ((5.0 + x_10) > (2.0 + x_11)? (5.0 + x_10) : (2.0 + x_11))? (12.0 + x_6) : ((5.0 + x_10) > (2.0 + x_11)? (5.0 + x_10) : (2.0 + x_11))));
  x_7_ = (((7.0 + x_0) > ((18.0 + x_3) > (12.0 + x_5)? (18.0 + x_3) : (12.0 + x_5))? (7.0 + x_0) : ((18.0 + x_3) > (12.0 + x_5)? (18.0 + x_3) : (12.0 + x_5))) > ((3.0 + x_6) > ((3.0 + x_9) > (8.0 + x_10)? (3.0 + x_9) : (8.0 + x_10))? (3.0 + x_6) : ((3.0 + x_9) > (8.0 + x_10)? (3.0 + x_9) : (8.0 + x_10)))? ((7.0 + x_0) > ((18.0 + x_3) > (12.0 + x_5)? (18.0 + x_3) : (12.0 + x_5))? (7.0 + x_0) : ((18.0 + x_3) > (12.0 + x_5)? (18.0 + x_3) : (12.0 + x_5))) : ((3.0 + x_6) > ((3.0 + x_9) > (8.0 + x_10)? (3.0 + x_9) : (8.0 + x_10))? (3.0 + x_6) : ((3.0 + x_9) > (8.0 + x_10)? (3.0 + x_9) : (8.0 + x_10))));
  x_8_ = (((11.0 + x_0) > ((15.0 + x_4) > (9.0 + x_6)? (15.0 + x_4) : (9.0 + x_6))? (11.0 + x_0) : ((15.0 + x_4) > (9.0 + x_6)? (15.0 + x_4) : (9.0 + x_6))) > ((18.0 + x_8) > ((17.0 + x_9) > (6.0 + x_11)? (17.0 + x_9) : (6.0 + x_11))? (18.0 + x_8) : ((17.0 + x_9) > (6.0 + x_11)? (17.0 + x_9) : (6.0 + x_11)))? ((11.0 + x_0) > ((15.0 + x_4) > (9.0 + x_6)? (15.0 + x_4) : (9.0 + x_6))? (11.0 + x_0) : ((15.0 + x_4) > (9.0 + x_6)? (15.0 + x_4) : (9.0 + x_6))) : ((18.0 + x_8) > ((17.0 + x_9) > (6.0 + x_11)? (17.0 + x_9) : (6.0 + x_11))? (18.0 + x_8) : ((17.0 + x_9) > (6.0 + x_11)? (17.0 + x_9) : (6.0 + x_11))));
  x_9_ = (((16.0 + x_1) > ((9.0 + x_3) > (10.0 + x_5)? (9.0 + x_3) : (10.0 + x_5))? (16.0 + x_1) : ((9.0 + x_3) > (10.0 + x_5)? (9.0 + x_3) : (10.0 + x_5))) > ((5.0 + x_6) > ((13.0 + x_7) > (4.0 + x_10)? (13.0 + x_7) : (4.0 + x_10))? (5.0 + x_6) : ((13.0 + x_7) > (4.0 + x_10)? (13.0 + x_7) : (4.0 + x_10)))? ((16.0 + x_1) > ((9.0 + x_3) > (10.0 + x_5)? (9.0 + x_3) : (10.0 + x_5))? (16.0 + x_1) : ((9.0 + x_3) > (10.0 + x_5)? (9.0 + x_3) : (10.0 + x_5))) : ((5.0 + x_6) > ((13.0 + x_7) > (4.0 + x_10)? (13.0 + x_7) : (4.0 + x_10))? (5.0 + x_6) : ((13.0 + x_7) > (4.0 + x_10)? (13.0 + x_7) : (4.0 + x_10))));
  x_10_ = (((7.0 + x_0) > ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6))? (7.0 + x_0) : ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6))) > ((14.0 + x_7) > ((3.0 + x_10) > (16.0 + x_11)? (3.0 + x_10) : (16.0 + x_11))? (14.0 + x_7) : ((3.0 + x_10) > (16.0 + x_11)? (3.0 + x_10) : (16.0 + x_11)))? ((7.0 + x_0) > ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6))? (7.0 + x_0) : ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6))) : ((14.0 + x_7) > ((3.0 + x_10) > (16.0 + x_11)? (3.0 + x_10) : (16.0 + x_11))? (14.0 + x_7) : ((3.0 + x_10) > (16.0 + x_11)? (3.0 + x_10) : (16.0 + x_11))));
  x_11_ = (((6.0 + x_3) > ((20.0 + x_4) > (18.0 + x_5)? (20.0 + x_4) : (18.0 + x_5))? (6.0 + x_3) : ((20.0 + x_4) > (18.0 + x_5)? (20.0 + x_4) : (18.0 + x_5))) > ((6.0 + x_7) > ((10.0 + x_10) > (2.0 + x_11)? (10.0 + x_10) : (2.0 + x_11))? (6.0 + x_7) : ((10.0 + x_10) > (2.0 + x_11)? (10.0 + x_10) : (2.0 + x_11)))? ((6.0 + x_3) > ((20.0 + x_4) > (18.0 + x_5)? (20.0 + x_4) : (18.0 + x_5))? (6.0 + x_3) : ((20.0 + x_4) > (18.0 + x_5)? (20.0 + x_4) : (18.0 + x_5))) : ((6.0 + x_7) > ((10.0 + x_10) > (2.0 + x_11)? (10.0 + x_10) : (2.0 + x_11))? (6.0 + x_7) : ((10.0 + x_10) > (2.0 + x_11)? (10.0 + x_10) : (2.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;
  }
  