src/HOL/ex/SAT_Examples.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 19236 150e8b0fb991 child 19534 1724ec4032c5 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     1 (*  Title:      HOL/ex/SAT_Examples.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Alwen Tiu, Tjark Weber
```
```     4     Copyright   2005-2006
```
```     5 *)
```
```     6
```
```     7 header {* Examples for the 'sat' and 'satx' tactic *}
```
```     8
```
```     9 theory SAT_Examples imports Main
```
```    10
```
```    11 begin
```
```    12
```
```    13 ML {* set sat.trace_sat; *}
```
```    14 ML {* set quick_and_dirty; *}
```
```    15
```
```    16 lemma "True"
```
```    17 by sat
```
```    18
```
```    19 lemma "a | ~a"
```
```    20 by sat
```
```    21
```
```    22 lemma "(a | b) & ~a \<Longrightarrow> b"
```
```    23 by sat
```
```    24
```
```    25 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
```
```    26 apply (tactic {* cnf.cnf_rewrite_tac 1 *})
```
```    27 by sat
```
```    28
```
```    29 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
```
```    30 apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
```
```    31 apply (erule exE | erule conjE)+
```
```    32 by satx
```
```    33
```
```    34 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow>
```
```    35   (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
```
```    36 apply (tactic {* cnf.cnf_rewrite_tac 1 *})
```
```    37 by sat
```
```    38
```
```    39 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow>
```
```    40   (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
```
```    41 apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
```
```    42 apply (erule exE | erule conjE)+
```
```    43 by satx
```
```    44
```
```    45 lemma "P=P=P=P=P=P=P=P=P=P"
```
```    46 by sat
```
```    47
```
```    48 lemma "P=P=P=P=P=P=P=P=P=P"
```
```    49 by satx
```
```    50
```
```    51 lemma  "!! a b c. [| a | b | c | d ;
```
```    52 e | f | (a & d) ;
```
```    53 ~(a | (c & ~c)) | b ;
```
```    54 ~(b & (x | ~x)) | c ;
```
```    55 ~(d | False) | c ;
```
```    56 ~(c | (~p & (p | (q & ~q)))) |] ==> False"
```
```    57 by sat
```
```    58
```
```    59 lemma  "!! a b c. [| a | b | c | d ;
```
```    60 e | f | (a & d) ;
```
```    61 ~(a | (c & ~c)) | b ;
```
```    62 ~(b & (x | ~x)) | c ;
```
```    63 ~(d | False) | c ;
```
```    64 ~(c | (~p & (p | (q & ~q)))) |] ==> False"
```
```    65 by satx
```
```    66
```
```    67 ML {* reset sat.trace_sat; *}
```
```    68 ML {* reset quick_and_dirty; *}
```
```    69
```
```    70 ML {* Toplevel.profiling := 1; *}
```
```    71
```
```    72 (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
```
```    73
```
```    74 lemma assumes 1: "~x0"
```
```    75 and 2: "~x30"
```
```    76 and 3: "~x29"
```
```    77 and 4: "~x59"
```
```    78 and 5: "x1 | x31 | x0"
```
```    79 and 6: "x2 | x32 | x1"
```
```    80 and 7: "x3 | x33 | x2"
```
```    81 and 8: "x4 | x34 | x3"
```
```    82 and 9: "x35 | x4"
```
```    83 and 10: "x5 | x36 | x30"
```
```    84 and 11: "x6 | x37 | x5 | x31"
```
```    85 and 12: "x7 | x38 | x6 | x32"
```
```    86 and 13: "x8 | x39 | x7 | x33"
```
```    87 and 14: "x9 | x40 | x8 | x34"
```
```    88 and 15: "x41 | x9 | x35"
```
```    89 and 16: "x10 | x42 | x36"
```
```    90 and 17: "x11 | x43 | x10 | x37"
```
```    91 and 18: "x12 | x44 | x11 | x38"
```
```    92 and 19: "x13 | x45 | x12 | x39"
```
```    93 and 20: "x14 | x46 | x13 | x40"
```
```    94 and 21: "x47 | x14 | x41"
```
```    95 and 22: "x15 | x48 | x42"
```
```    96 and 23: "x16 | x49 | x15 | x43"
```
```    97 and 24: "x17 | x50 | x16 | x44"
```
```    98 and 25: "x18 | x51 | x17 | x45"
```
```    99 and 26: "x19 | x52 | x18 | x46"
```
```   100 and 27: "x53 | x19 | x47"
```
```   101 and 28: "x20 | x54 | x48"
```
```   102 and 29: "x21 | x55 | x20 | x49"
```
```   103 and 30: "x22 | x56 | x21 | x50"
```
```   104 and 31: "x23 | x57 | x22 | x51"
```
```   105 and 32: "x24 | x58 | x23 | x52"
```
```   106 and 33: "x59 | x24 | x53"
```
```   107 and 34: "x25 | x54"
```
```   108 and 35: "x26 | x25 | x55"
```
```   109 and 36: "x27 | x26 | x56"
```
```   110 and 37: "x28 | x27 | x57"
```
```   111 and 38: "x29 | x28 | x58"
```
```   112 and 39: "~x1 | ~x31"
```
```   113 and 40: "~x1 | ~x0"
```
```   114 and 41: "~x31 | ~x0"
```
```   115 and 42: "~x2 | ~x32"
```
```   116 and 43: "~x2 | ~x1"
```
```   117 and 44: "~x32 | ~x1"
```
```   118 and 45: "~x3 | ~x33"
```
```   119 and 46: "~x3 | ~x2"
```
```   120 and 47: "~x33 | ~x2"
```
```   121 and 48: "~x4 | ~x34"
```
```   122 and 49: "~x4 | ~x3"
```
```   123 and 50: "~x34 | ~x3"
```
```   124 and 51: "~x35 | ~x4"
```
```   125 and 52: "~x5 | ~x36"
```
```   126 and 53: "~x5 | ~x30"
```
```   127 and 54: "~x36 | ~x30"
```
```   128 and 55: "~x6 | ~x37"
```
```   129 and 56: "~x6 | ~x5"
```
```   130 and 57: "~x6 | ~x31"
```
```   131 and 58: "~x37 | ~x5"
```
```   132 and 59: "~x37 | ~x31"
```
```   133 and 60: "~x5 | ~x31"
```
```   134 and 61: "~x7 | ~x38"
```
```   135 and 62: "~x7 | ~x6"
```
```   136 and 63: "~x7 | ~x32"
```
```   137 and 64: "~x38 | ~x6"
```
```   138 and 65: "~x38 | ~x32"
```
```   139 and 66: "~x6 | ~x32"
```
```   140 and 67: "~x8 | ~x39"
```
```   141 and 68: "~x8 | ~x7"
```
```   142 and 69: "~x8 | ~x33"
```
```   143 and 70: "~x39 | ~x7"
```
```   144 and 71: "~x39 | ~x33"
```
```   145 and 72: "~x7 | ~x33"
```
```   146 and 73: "~x9 | ~x40"
```
```   147 and 74: "~x9 | ~x8"
```
```   148 and 75: "~x9 | ~x34"
```
```   149 and 76: "~x40 | ~x8"
```
```   150 and 77: "~x40 | ~x34"
```
```   151 and 78: "~x8 | ~x34"
```
```   152 and 79: "~x41 | ~x9"
```
```   153 and 80: "~x41 | ~x35"
```
```   154 and 81: "~x9 | ~x35"
```
```   155 and 82: "~x10 | ~x42"
```
```   156 and 83: "~x10 | ~x36"
```
```   157 and 84: "~x42 | ~x36"
```
```   158 and 85: "~x11 | ~x43"
```
```   159 and 86: "~x11 | ~x10"
```
```   160 and 87: "~x11 | ~x37"
```
```   161 and 88: "~x43 | ~x10"
```
```   162 and 89: "~x43 | ~x37"
```
```   163 and 90: "~x10 | ~x37"
```
```   164 and 91: "~x12 | ~x44"
```
```   165 and 92: "~x12 | ~x11"
```
```   166 and 93: "~x12 | ~x38"
```
```   167 and 94: "~x44 | ~x11"
```
```   168 and 95: "~x44 | ~x38"
```
```   169 and 96: "~x11 | ~x38"
```
```   170 and 97: "~x13 | ~x45"
```
```   171 and 98: "~x13 | ~x12"
```
```   172 and 99: "~x13 | ~x39"
```
```   173 and 100: "~x45 | ~x12"
```
```   174 and 101: "~x45 | ~x39"
```
```   175 and 102: "~x12 | ~x39"
```
```   176 and 103: "~x14 | ~x46"
```
```   177 and 104: "~x14 | ~x13"
```
```   178 and 105: "~x14 | ~x40"
```
```   179 and 106: "~x46 | ~x13"
```
```   180 and 107: "~x46 | ~x40"
```
```   181 and 108: "~x13 | ~x40"
```
```   182 and 109: "~x47 | ~x14"
```
```   183 and 110: "~x47 | ~x41"
```
```   184 and 111: "~x14 | ~x41"
```
```   185 and 112: "~x15 | ~x48"
```
```   186 and 113: "~x15 | ~x42"
```
```   187 and 114: "~x48 | ~x42"
```
```   188 and 115: "~x16 | ~x49"
```
```   189 and 116: "~x16 | ~x15"
```
```   190 and 117: "~x16 | ~x43"
```
```   191 and 118: "~x49 | ~x15"
```
```   192 and 119: "~x49 | ~x43"
```
```   193 and 120: "~x15 | ~x43"
```
```   194 and 121: "~x17 | ~x50"
```
```   195 and 122: "~x17 | ~x16"
```
```   196 and 123: "~x17 | ~x44"
```
```   197 and 124: "~x50 | ~x16"
```
```   198 and 125: "~x50 | ~x44"
```
```   199 and 126: "~x16 | ~x44"
```
```   200 and 127: "~x18 | ~x51"
```
```   201 and 128: "~x18 | ~x17"
```
```   202 and 129: "~x18 | ~x45"
```
```   203 and 130: "~x51 | ~x17"
```
```   204 and 131: "~x51 | ~x45"
```
```   205 and 132: "~x17 | ~x45"
```
```   206 and 133: "~x19 | ~x52"
```
```   207 and 134: "~x19 | ~x18"
```
```   208 and 135: "~x19 | ~x46"
```
```   209 and 136: "~x52 | ~x18"
```
```   210 and 137: "~x52 | ~x46"
```
```   211 and 138: "~x18 | ~x46"
```
```   212 and 139: "~x53 | ~x19"
```
```   213 and 140: "~x53 | ~x47"
```
```   214 and 141: "~x19 | ~x47"
```
```   215 and 142: "~x20 | ~x54"
```
```   216 and 143: "~x20 | ~x48"
```
```   217 and 144: "~x54 | ~x48"
```
```   218 and 145: "~x21 | ~x55"
```
```   219 and 146: "~x21 | ~x20"
```
```   220 and 147: "~x21 | ~x49"
```
```   221 and 148: "~x55 | ~x20"
```
```   222 and 149: "~x55 | ~x49"
```
```   223 and 150: "~x20 | ~x49"
```
```   224 and 151: "~x22 | ~x56"
```
```   225 and 152: "~x22 | ~x21"
```
```   226 and 153: "~x22 | ~x50"
```
```   227 and 154: "~x56 | ~x21"
```
```   228 and 155: "~x56 | ~x50"
```
```   229 and 156: "~x21 | ~x50"
```
```   230 and 157: "~x23 | ~x57"
```
```   231 and 158: "~x23 | ~x22"
```
```   232 and 159: "~x23 | ~x51"
```
```   233 and 160: "~x57 | ~x22"
```
```   234 and 161: "~x57 | ~x51"
```
```   235 and 162: "~x22 | ~x51"
```
```   236 and 163: "~x24 | ~x58"
```
```   237 and 164: "~x24 | ~x23"
```
```   238 and 165: "~x24 | ~x52"
```
```   239 and 166: "~x58 | ~x23"
```
```   240 and 167: "~x58 | ~x52"
```
```   241 and 168: "~x23 | ~x52"
```
```   242 and 169: "~x59 | ~x24"
```
```   243 and 170: "~x59 | ~x53"
```
```   244 and 171: "~x24 | ~x53"
```
```   245 and 172: "~x25 | ~x54"
```
```   246 and 173: "~x26 | ~x25"
```
```   247 and 174: "~x26 | ~x55"
```
```   248 and 175: "~x25 | ~x55"
```
```   249 and 176: "~x27 | ~x26"
```
```   250 and 177: "~x27 | ~x56"
```
```   251 and 178: "~x26 | ~x56"
```
```   252 and 179: "~x28 | ~x27"
```
```   253 and 180: "~x28 | ~x57"
```
```   254 and 181: "~x27 | ~x57"
```
```   255 and 182: "~x29 | ~x28"
```
```   256 and 183: "~x29 | ~x58"
```
```   257 and 184: "~x28 | ~x58"
```
```   258 shows "False"
```
```   259 using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
```
```   260 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
```
```   261 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
```
```   262 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
```
```   263 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
```
```   264 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
```
```   265 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
```
```   266 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
```
```   267 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
```
```   268 180 181 182 183 184
```
```   269 by sat
```
```   270
```
```   271 (* Translated from TPTP problem library: MSC007-1.008.dimacs *)
```
```   272
```
```   273 lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
```
```   274 and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"
```
```   275 and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20"
```
```   276 and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27"
```
```   277 and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34"
```
```   278 and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41"
```
```   279 and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48"
```
```   280 and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55"
```
```   281 and 9: "~x0 | ~x7"
```
```   282 and 10: "~x0 | ~x14"
```
```   283 and 11: "~x0 | ~x21"
```
```   284 and 12: "~x0 | ~x28"
```
```   285 and 13: "~x0 | ~x35"
```
```   286 and 14: "~x0 | ~x42"
```
```   287 and 15: "~x0 | ~x49"
```
```   288 and 16: "~x7 | ~x14"
```
```   289 and 17: "~x7 | ~x21"
```
```   290 and 18: "~x7 | ~x28"
```
```   291 and 19: "~x7 | ~x35"
```
```   292 and 20: "~x7 | ~x42"
```
```   293 and 21: "~x7 | ~x49"
```
```   294 and 22: "~x14 | ~x21"
```
```   295 and 23: "~x14 | ~x28"
```
```   296 and 24: "~x14 | ~x35"
```
```   297 and 25: "~x14 | ~x42"
```
```   298 and 26: "~x14 | ~x49"
```
```   299 and 27: "~x21 | ~x28"
```
```   300 and 28: "~x21 | ~x35"
```
```   301 and 29: "~x21 | ~x42"
```
```   302 and 30: "~x21 | ~x49"
```
```   303 and 31: "~x28 | ~x35"
```
```   304 and 32: "~x28 | ~x42"
```
```   305 and 33: "~x28 | ~x49"
```
```   306 and 34: "~x35 | ~x42"
```
```   307 and 35: "~x35 | ~x49"
```
```   308 and 36: "~x42 | ~x49"
```
```   309 and 37: "~x1 | ~x8"
```
```   310 and 38: "~x1 | ~x15"
```
```   311 and 39: "~x1 | ~x22"
```
```   312 and 40: "~x1 | ~x29"
```
```   313 and 41: "~x1 | ~x36"
```
```   314 and 42: "~x1 | ~x43"
```
```   315 and 43: "~x1 | ~x50"
```
```   316 and 44: "~x8 | ~x15"
```
```   317 and 45: "~x8 | ~x22"
```
```   318 and 46: "~x8 | ~x29"
```
```   319 and 47: "~x8 | ~x36"
```
```   320 and 48: "~x8 | ~x43"
```
```   321 and 49: "~x8 | ~x50"
```
```   322 and 50: "~x15 | ~x22"
```
```   323 and 51: "~x15 | ~x29"
```
```   324 and 52: "~x15 | ~x36"
```
```   325 and 53: "~x15 | ~x43"
```
```   326 and 54: "~x15 | ~x50"
```
```   327 and 55: "~x22 | ~x29"
```
```   328 and 56: "~x22 | ~x36"
```
```   329 and 57: "~x22 | ~x43"
```
```   330 and 58: "~x22 | ~x50"
```
```   331 and 59: "~x29 | ~x36"
```
```   332 and 60: "~x29 | ~x43"
```
```   333 and 61: "~x29 | ~x50"
```
```   334 and 62: "~x36 | ~x43"
```
```   335 and 63: "~x36 | ~x50"
```
```   336 and 64: "~x43 | ~x50"
```
```   337 and 65: "~x2 | ~x9"
```
```   338 and 66: "~x2 | ~x16"
```
```   339 and 67: "~x2 | ~x23"
```
```   340 and 68: "~x2 | ~x30"
```
```   341 and 69: "~x2 | ~x37"
```
```   342 and 70: "~x2 | ~x44"
```
```   343 and 71: "~x2 | ~x51"
```
```   344 and 72: "~x9 | ~x16"
```
```   345 and 73: "~x9 | ~x23"
```
```   346 and 74: "~x9 | ~x30"
```
```   347 and 75: "~x9 | ~x37"
```
```   348 and 76: "~x9 | ~x44"
```
```   349 and 77: "~x9 | ~x51"
```
```   350 and 78: "~x16 | ~x23"
```
```   351 and 79: "~x16 | ~x30"
```
```   352 and 80: "~x16 | ~x37"
```
```   353 and 81: "~x16 | ~x44"
```
```   354 and 82: "~x16 | ~x51"
```
```   355 and 83: "~x23 | ~x30"
```
```   356 and 84: "~x23 | ~x37"
```
```   357 and 85: "~x23 | ~x44"
```
```   358 and 86: "~x23 | ~x51"
```
```   359 and 87: "~x30 | ~x37"
```
```   360 and 88: "~x30 | ~x44"
```
```   361 and 89: "~x30 | ~x51"
```
```   362 and 90: "~x37 | ~x44"
```
```   363 and 91: "~x37 | ~x51"
```
```   364 and 92: "~x44 | ~x51"
```
```   365 and 93: "~x3 | ~x10"
```
```   366 and 94: "~x3 | ~x17"
```
```   367 and 95: "~x3 | ~x24"
```
```   368 and 96: "~x3 | ~x31"
```
```   369 and 97: "~x3 | ~x38"
```
```   370 and 98: "~x3 | ~x45"
```
```   371 and 99: "~x3 | ~x52"
```
```   372 and 100: "~x10 | ~x17"
```
```   373 and 101: "~x10 | ~x24"
```
```   374 and 102: "~x10 | ~x31"
```
```   375 and 103: "~x10 | ~x38"
```
```   376 and 104: "~x10 | ~x45"
```
```   377 and 105: "~x10 | ~x52"
```
```   378 and 106: "~x17 | ~x24"
```
```   379 and 107: "~x17 | ~x31"
```
```   380 and 108: "~x17 | ~x38"
```
```   381 and 109: "~x17 | ~x45"
```
```   382 and 110: "~x17 | ~x52"
```
```   383 and 111: "~x24 | ~x31"
```
```   384 and 112: "~x24 | ~x38"
```
```   385 and 113: "~x24 | ~x45"
```
```   386 and 114: "~x24 | ~x52"
```
```   387 and 115: "~x31 | ~x38"
```
```   388 and 116: "~x31 | ~x45"
```
```   389 and 117: "~x31 | ~x52"
```
```   390 and 118: "~x38 | ~x45"
```
```   391 and 119: "~x38 | ~x52"
```
```   392 and 120: "~x45 | ~x52"
```
```   393 and 121: "~x4 | ~x11"
```
```   394 and 122: "~x4 | ~x18"
```
```   395 and 123: "~x4 | ~x25"
```
```   396 and 124: "~x4 | ~x32"
```
```   397 and 125: "~x4 | ~x39"
```
```   398 and 126: "~x4 | ~x46"
```
```   399 and 127: "~x4 | ~x53"
```
```   400 and 128: "~x11 | ~x18"
```
```   401 and 129: "~x11 | ~x25"
```
```   402 and 130: "~x11 | ~x32"
```
```   403 and 131: "~x11 | ~x39"
```
```   404 and 132: "~x11 | ~x46"
```
```   405 and 133: "~x11 | ~x53"
```
```   406 and 134: "~x18 | ~x25"
```
```   407 and 135: "~x18 | ~x32"
```
```   408 and 136: "~x18 | ~x39"
```
```   409 and 137: "~x18 | ~x46"
```
```   410 and 138: "~x18 | ~x53"
```
```   411 and 139: "~x25 | ~x32"
```
```   412 and 140: "~x25 | ~x39"
```
```   413 and 141: "~x25 | ~x46"
```
```   414 and 142: "~x25 | ~x53"
```
```   415 and 143: "~x32 | ~x39"
```
```   416 and 144: "~x32 | ~x46"
```
```   417 and 145: "~x32 | ~x53"
```
```   418 and 146: "~x39 | ~x46"
```
```   419 and 147: "~x39 | ~x53"
```
```   420 and 148: "~x46 | ~x53"
```
```   421 and 149: "~x5 | ~x12"
```
```   422 and 150: "~x5 | ~x19"
```
```   423 and 151: "~x5 | ~x26"
```
```   424 and 152: "~x5 | ~x33"
```
```   425 and 153: "~x5 | ~x40"
```
```   426 and 154: "~x5 | ~x47"
```
```   427 and 155: "~x5 | ~x54"
```
```   428 and 156: "~x12 | ~x19"
```
```   429 and 157: "~x12 | ~x26"
```
```   430 and 158: "~x12 | ~x33"
```
```   431 and 159: "~x12 | ~x40"
```
```   432 and 160: "~x12 | ~x47"
```
```   433 and 161: "~x12 | ~x54"
```
```   434 and 162: "~x19 | ~x26"
```
```   435 and 163: "~x19 | ~x33"
```
```   436 and 164: "~x19 | ~x40"
```
```   437 and 165: "~x19 | ~x47"
```
```   438 and 166: "~x19 | ~x54"
```
```   439 and 167: "~x26 | ~x33"
```
```   440 and 168: "~x26 | ~x40"
```
```   441 and 169: "~x26 | ~x47"
```
```   442 and 170: "~x26 | ~x54"
```
```   443 and 171: "~x33 | ~x40"
```
```   444 and 172: "~x33 | ~x47"
```
```   445 and 173: "~x33 | ~x54"
```
```   446 and 174: "~x40 | ~x47"
```
```   447 and 175: "~x40 | ~x54"
```
```   448 and 176: "~x47 | ~x54"
```
```   449 and 177: "~x6 | ~x13"
```
```   450 and 178: "~x6 | ~x20"
```
```   451 and 179: "~x6 | ~x27"
```
```   452 and 180: "~x6 | ~x34"
```
```   453 and 181: "~x6 | ~x41"
```
```   454 and 182: "~x6 | ~x48"
```
```   455 and 183: "~x6 | ~x55"
```
```   456 and 184: "~x13 | ~x20"
```
```   457 and 185: "~x13 | ~x27"
```
```   458 and 186: "~x13 | ~x34"
```
```   459 and 187: "~x13 | ~x41"
```
```   460 and 188: "~x13 | ~x48"
```
```   461 and 189: "~x13 | ~x55"
```
```   462 and 190: "~x20 | ~x27"
```
```   463 and 191: "~x20 | ~x34"
```
```   464 and 192: "~x20 | ~x41"
```
```   465 and 193: "~x20 | ~x48"
```
```   466 and 194: "~x20 | ~x55"
```
```   467 and 195: "~x27 | ~x34"
```
```   468 and 196: "~x27 | ~x41"
```
```   469 and 197: "~x27 | ~x48"
```
```   470 and 198: "~x27 | ~x55"
```
```   471 and 199: "~x34 | ~x41"
```
```   472 and 200: "~x34 | ~x48"
```
```   473 and 201: "~x34 | ~x55"
```
```   474 and 202: "~x41 | ~x48"
```
```   475 and 203: "~x41 | ~x55"
```
```   476 and 204: "~x48 | ~x55"
```
```   477 shows "False"
```
```   478 using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
```
```   479 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
```
```   480 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
```
```   481 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
```
```   482 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
```
```   483 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
```
```   484 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
```
```   485 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
```
```   486 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
```
```   487 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
```
```   488 200 201 202 203 204
```
```   489 by sat
```
```   490
```
```   491 ML {* Toplevel.profiling := 0; *}
```
```   492
```
```   493 end
```