test/regress/regress0/uf20-03.cvc

   1 % EXPECT: invalid
   2 x_1 : BOOLEAN;
   3 x_2 : BOOLEAN;
   4 x_3 : BOOLEAN;
   5 x_4 : BOOLEAN;
   6 x_5 : BOOLEAN;
   7 x_6 : BOOLEAN;
   8 x_7 : BOOLEAN;
   9 x_8 : BOOLEAN;
  10 x_9 : BOOLEAN;
  11 x_10 : BOOLEAN;
  12 x_11 : BOOLEAN;
  13 x_12 : BOOLEAN;
  14 x_13 : BOOLEAN;
  15 x_14 : BOOLEAN;
  16 x_15 : BOOLEAN;
  17 x_16 : BOOLEAN;
  18 x_17 : BOOLEAN;
  19 x_18 : BOOLEAN;
  20 x_19 : BOOLEAN;
  21 x_20 : BOOLEAN;
  22 ASSERT NOT x_9 OR x_3 OR NOT x_15;
  23 ASSERT NOT x_12 OR NOT x_4 OR NOT x_15;
  24 ASSERT x_6 OR x_14 OR NOT x_17;
  25 ASSERT x_10 OR x_16 OR x_11;
  26 ASSERT NOT x_15 OR x_20 OR NOT x_7;
  27 ASSERT NOT x_1 OR x_10 OR x_16;
  28 ASSERT x_13 OR x_17 OR NOT x_7;
  29 ASSERT NOT x_2 OR NOT x_14 OR NOT x_13;
  30 ASSERT x_13 OR NOT x_6 OR x_15;
  31 ASSERT NOT x_9 OR x_3 OR x_16;
  32 ASSERT NOT x_20 OR NOT x_13 OR x_4;
  33 ASSERT NOT x_7 OR x_15 OR NOT x_14;
  34 ASSERT NOT x_15 OR NOT x_16 OR x_6;
  35 ASSERT x_5 OR NOT x_18 OR x_20;
  36 ASSERT NOT x_16 OR NOT x_19 OR x_7;
  37 ASSERT x_20 OR NOT x_18 OR NOT x_2;
  38 ASSERT x_10 OR NOT x_19 OR NOT x_14;
  39 ASSERT x_16 OR NOT x_7 OR x_12;
  40 ASSERT x_6 OR NOT x_5 OR NOT x_1;
  41 ASSERT NOT x_9 OR x_11 OR x_15;
  42 ASSERT x_19 OR NOT x_6 OR x_7;
  43 ASSERT NOT x_11 OR x_17 OR NOT x_19;
  44 ASSERT x_9 OR NOT x_16 OR x_6;
  45 ASSERT x_15 OR NOT x_20 OR x_10;
  46 ASSERT x_9 OR NOT x_1 OR NOT x_11;
  47 ASSERT NOT x_8 OR NOT x_19 OR x_5;
  48 ASSERT NOT x_19 OR x_11 OR x_20;
  49 ASSERT NOT x_12 OR x_13 OR NOT x_3;
  50 ASSERT NOT x_7 OR NOT x_17 OR NOT x_19;
  51 ASSERT x_17 OR x_6 OR NOT x_11;
  52 ASSERT NOT x_7 OR NOT x_17 OR x_10;
  53 ASSERT NOT x_14 OR x_9 OR x_20;
  54 ASSERT x_1 OR NOT x_18 OR NOT x_16;
  55 ASSERT NOT x_2 OR NOT x_15 OR x_20;
  56 ASSERT x_14 OR x_18 OR NOT x_1;
  57 ASSERT NOT x_8 OR NOT x_4 OR x_1;
  58 ASSERT x_13 OR x_3 OR NOT x_9;
  59 ASSERT x_5 OR x_7 OR x_8;
  60 ASSERT x_9 OR x_4 OR NOT x_20;
  61 ASSERT NOT x_18 OR NOT x_15 OR NOT x_10;
  62 ASSERT x_10 OR x_3 OR NOT x_20;
  63 ASSERT x_20 OR NOT x_14 OR x_16;
  64 ASSERT x_20 OR NOT x_3 OR NOT x_11;
  65 ASSERT NOT x_12 OR x_19 OR NOT x_16;
  66 ASSERT NOT x_3 OR x_5 OR x_10;
  67 ASSERT x_8 OR x_13 OR NOT x_7;
  68 ASSERT NOT x_2 OR NOT x_15 OR x_10;
  69 ASSERT NOT x_3 OR x_9 OR x_16;
  70 ASSERT NOT x_12 OR NOT x_16 OR NOT x_18;
  71 ASSERT x_3 OR x_1 OR NOT x_12;
  72 ASSERT NOT x_18 OR x_13 OR x_5;
  73 ASSERT x_1 OR x_3 OR NOT x_19;
  74 ASSERT NOT x_19 OR NOT x_5 OR x_6;
  75 ASSERT NOT x_20 OR x_8 OR NOT x_2;
  76 ASSERT x_17 OR NOT x_8 OR NOT x_13;
  77 ASSERT x_7 OR NOT x_11 OR NOT x_12;
  78 ASSERT NOT x_10 OR NOT x_14 OR NOT x_20;
  79 ASSERT NOT x_1 OR x_16 OR NOT x_12;
  80 ASSERT x_5 OR NOT x_3 OR x_9;
  81 ASSERT NOT x_18 OR x_8 OR x_14;
  82 ASSERT x_1 OR x_16 OR x_12;
  83 ASSERT x_20 OR NOT x_1 OR NOT x_16;
  84 ASSERT x_5 OR x_10 OR NOT x_13;
  85 ASSERT x_9 OR NOT x_10 OR x_6;
  86 ASSERT NOT x_12 OR x_10 OR NOT x_14;
  87 ASSERT NOT x_13 OR x_1 OR x_4;
  88 ASSERT NOT x_20 OR NOT x_7 OR x_3;
  89 ASSERT x_12 OR x_1 OR NOT x_10;
  90 ASSERT NOT x_1 OR NOT x_16 OR x_7;
  91 ASSERT x_11 OR NOT x_6 OR NOT x_4;
  92 ASSERT x_1 OR x_16 OR NOT x_20;
  93 ASSERT x_9 OR x_7 OR x_15;
  94 ASSERT NOT x_6 OR x_17 OR x_10;
  95 ASSERT x_8 OR x_9 OR x_17;
  96 ASSERT x_18 OR x_11 OR x_10;
  97 ASSERT x_7 OR x_1 OR NOT x_8;
  98 ASSERT NOT x_5 OR NOT x_12 OR x_18;
  99 ASSERT NOT x_6 OR x_2 OR x_15;
 100 ASSERT x_2 OR x_18 OR x_1;
 101 ASSERT NOT x_7 OR NOT x_13 OR x_16;
 102 ASSERT x_18 OR x_19 OR x_9;
 103 ASSERT x_9 OR NOT x_14 OR x_18;
 104 ASSERT x_14 OR x_12 OR NOT x_5;
 105 ASSERT NOT x_13 OR NOT x_7 OR NOT x_14;
 106 ASSERT NOT x_1 OR x_8 OR NOT x_16;
 107 ASSERT NOT x_11 OR x_4 OR x_7;
 108 ASSERT NOT x_4 OR x_20 OR x_5;
 109 ASSERT NOT x_5 OR x_2 OR x_12;
 110 ASSERT NOT x_5 OR x_13 OR NOT x_18;
 111 ASSERT NOT x_18 OR x_9 OR x_1;
 112 ASSERT x_10 OR NOT x_11 OR x_16;
 113
 114
 115 QUERY FALSE;