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