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;