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